Triviality of partial halting problem solutions

[bernerbrau]

Hey XKCD fans!

So, I'm a CS grad, class of '03. I know that the following program cannot exist:

Code: Select all

H(P,I) => "Y" if P terminates on input I
       => "N" if P never terminates on input I

Because the following program does the opposite of what H says it does, invalidating the existence of H(P,I) via reductio ad absurdum:

Code: Select all

T(P) => LOOP() if H(P,P)

But something's been plaguing me for years now. What if we tweaked the requirements of the above program thus (I'll call it the Relaxed Halting Problem)?

Code: Select all

H(P,I) => "Y" or "?" if P terminates on input I
       => "N" or "?" if P never terminates on input I

It's trivial to show such a program exists:

Code: Select all

H(P,I) => "?"

Of course, I also know that a general algorithm that detects whether such a program is correct can be reduced to the halting problem, and is therefore also undecidable.

But lately I've been wondering about how complete a correct implementation can be written and manually verified. Here are a few implementations that are obviously correct:

Code: Select all

H(P,I) => "?" if P has loops or recursion, including nested recursion
       => "N" if P has obviously infinite loops, e.g. while(1)
       => "Y" otherwise

Code: Select all

H(P,I) => "Y" if P terminates after 1000 steps of simulation
       => "?" otherwise

I've thought about the possibility of "everything" variables that you could use in a simulation in order to to whittle down valid inputs and possible outcomes in order to deduce, among other things, loops that are more complex than just while(1).

My thinking is that, while not a complete HP solution, such a tool, being sufficiently well-featured, could be useful in catching potential programming errors. My gut instinct, however, tells me that if such a program could be useful, someone smarter than me would have thought of it and built it already. Moreover, I've not been able to come up with anything more substantive than these musings. Is this because of a fundamental limit on what answers this type of program can provide? Are there proofs of this? I seriously doubt I'm the first person to propose such a modification.

Thoughts?

[Likpok]

Compilers do this all the time. A discussion of determining termination is here: http://blog.regehr.org/archives/140. There is a fair amount of work in what you can prove terminates, and it depends heavily on the logical system.

If you want to play around with this, try playing with Coq or Isabelle, both (should) let you define functions, and you can see how they do the termination proofs.

[radams]

Hi everyone. Thought I'd wade in here for my first post. Brief introduction: my name's Robin, I'm in the UK, and I'm a lecturer in Computer Science.

Code: Select all

    H(P,I) => "Y" or "?" if P terminates on input I
           => "N" or "?" if P never terminates on input I

You can do better than this. Termination is semi-decidable; that is, we can write a program that fits this specification:

Code: Select all

    H(P,I) => "Y" if P terminates on input I
           => "?" if P never terminates on input I

The program works just by simulating the execution of P.

More generally, we can take a set S, a subset of the set of all programs, and sometimes write a program that satisfies this specification:

Code: Select all

    H(P,I) => "Y" if P terminates on input I
 => "N" if P is in S and does not terminate on input I
 => "?" if P is not in S and never terminates on input I

But the program H can't be in the set S itself. And the larger the set S is, the more complicated a program you need.

Coq and other type theories are my field of research. They do something different. They don't find a proof themselves that a program terminates. Rather, we use a fact that we've proved on paper: every function definable in their language always terminates.

In Coq, you cannot define every recursive function. When you define a recursive function, Coq checks whether the value on which you are recursing decreases. The set of functions definable in Coq is smaller than the recursive functions, but larger than the primitive recursive functions (you can define the Ackermann function, for example). It's still an open problem exactly which functions are definable in Coq.

[Berengal]

Code: Select all

    H(P,I) => "Y" if P terminates on input I
           => "?" if P never terminates on input I

I assume that by "?" you mean bottom (aka. infinite loop, "doesn't return", undefined and other non-values), not the actual symbol "?".

Coq and other type theories are my field of research. They do something different. They don't find a proof themselves that a program terminates. Rather, we use a fact that we've proved on paper: every function definable in their language always terminates.

If you've looked at Agda, which is very much in the same niche as Coq, you'd seen that it actually has a termination checker. That is, not every function definable in the language is guaranteed to terminate, but the compiler will chuck a wobbly if it can't prove they are. (And you can make it compile the program anyway if you beat it with a long stick, but your emacs buffer will still be full of ugly colours and you've sort of missed the point of using the language.)

Anyway, the termination checker is a partial halting oracle. It sort of looks like

Code: Select all

H(P) => "Y" if P terminates on all inputs
     => "N" if P doesn't terminate on all inputs, and sometimes even if it does

It's still an open problem exactly which functions are definable in Coq.

It's an interesting problem. One thing I find heartening is that every generally recursive function can be defined as a structurally recursive function taking an extra argument that is a proof that all the other arguments are in the domain of the function. This provides a sort of upper-bound on the effort we have to expend to turn our programs written in turing-complete languages into programs written in non-turing-complete languages that we can prove much more about. At the moment it's still a pain in some cases, but I believe we'll have some pretty neat new languages in not too many years.

[Likpok]

Coq and other type theories are my field of research. They do something different. They don't find a proof themselves that a program terminates. Rather, we use a fact that we've proved on paper: every function definable in their language always terminates.

In Coq, you cannot define every recursive function. When you define a recursive function, Coq checks whether the value on which you are recursing decreases. The set of functions definable in Coq is smaller than the recursive functions, but larger than the primitive recursive functions (you can define the Ackermann function, for example). It's still an open problem exactly which functions are definable in Coq.

Other theorem provers are not so limited. In Isabelle you can define recursive functions which do not follow any simple termination order. Primitive recursion and the lexicographic termination order can be proved automatically, but that doesn't preclude a more complex function where you have to do the work yourself.

[bernerbrau]

Hi everyone. Thought I'd wade in here for my first post. Brief introduction: my name's Robin, I'm in the UK, and I'm a lecturer in Computer Science.

Code: Select all

 H(P,I) => "Y" or "?" if P terminates on input I
=> "N" or "?" if P never terminates on input I

You can do better than this. Termination is semi-decidable; that is, we can write a program that fits this specification:

Code: Select all

 H(P,I) => "Y" if P terminates on input I
=> "?" if P never terminates on input I

The program works just by simulating the execution of P.

Yep, I get this. My use of "?" is the literal symbol, used to indicate that the program couldn't determine a value.

More generally, we can take a set S, a subset of the set of all programs, and sometimes write a program that satisfies this specification:

Code: Select all

 H(P,I) => "Y" if P terminates on input I
=> "N" if P is in S and does not terminate on input I
=> "?" if P is not in S and never terminates on input I

But the program H can't be in the set S itself. And the larger the set S is, the more complicated a program you need.

I'm thinking you need the "?" if P is not in S and terminates, because if it returns "Y" for all P that terminate on I, then a ? implies that the answer is N and your formulation is HP complete.

So if your definition is:

Code: Select all

 H(P,I) => "Y" if P is in S and terminates on input I
=> "N" if P is in S and does not terminate on input I
=> "?" if P is not in S

Where H alwats halts and ? is a literal return value, this is basically restating my initial question.

To restate my question in those terms, then, let me propose a set S*, whose members are all sets S with a corresponding function H that correctly determines halting on all members of that set. What is currently known about the membership of S*, aside from trivial sets like bounded-loop functions, loopless/nonrecursive functions, the null set, etc.?

It seems that people are saying Coq is a language whose functions are all guaranteed to terminate, but it's an open question as to what can be implemented in it. Is the set of all Coq functions a member of S* then? What else do we know about S*? What's still an open question?

[tomtom2357]

Code: Select all

    H(P,I) => "Y" if P terminates on input I
           => "?" if P never terminates on input I

The program works just by simulating the execution of P.

Is there a program that can work faster than just simulating the execution of P?