14
$\begingroup$
A standalone statement of my question

Given a program that takes no argument, we are interested in whether the program will eventually terminate. My question is this:

Theoretically speaking, can we always find a proof of the termination/non-termination of a program?

Clarification

Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it allows the proof to depend on the specified program. It is thus a much weaker version.

There are obviously some proofs for some terminations and some non-terminations, and there are cases that remain unknown to this day (such as the evaluation of incrementing a number until finding a counter example of Collatz conjecture).

But more generally, is there any result on this? Is it always possible to prove whether the program terminates or not? Or is it provable that some programs cannot be proved either ways?

(Note that the answer to this question does not require solving, say, Collatz conjecture because it will only say there is a proof maybe that it terminates or maybe that it does not)

What I have thought about?

Cases that are easy are these two:

  1. If it terminates, we just run the program and the termination proves itself.
  2. If it falls into some repetitive periods, we track the history of all variables and we can prove that it does not terminate by remarking that it goes into a loop after certain step.

One case remains where the non-termination will never fall into periods and keep visiting new states. In this case, my first thought is that it comes down (almost) to prove the unboundedness (of some sort) of a sequence (of some kind of structures) defined by a program. So maybe a weaker version of my question would be: Is the unboundedness of a sequence of natural numbers (generated by the program) always provable?

Improve this question
$\endgroup$
6
  • 1
    $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. Please don't use the comments to suggest an answer to the question, or to debate the answer. Instead, I encourage you to write an answer an explain your reasoning, if you believe you can answer the question. Thank you! $\endgroup$
    – D.W. ♦
    Commented Jun 8, 2022 at 19:41
  • 1
    $\begingroup$ Folks who are coming here might also be interested in cs.stackexchange.com/questions/49793/… $\endgroup$
    – D.W. ♦
    Commented Jun 8, 2022 at 19:55
  • $\begingroup$ @D.W.: Just to point out, the linked post has a very very different phenomenon. The program M there (which is specific to some chosen formal system T) halts on every input, and (since we of course assume T is reasonable) T can prove ( M halts on X ) for every X. What T cannot prove is ( M halts on every X ). I had mentioned a similar phenomenon in this comment, with a much simpler proof (not relying on the recursion theorem). $\endgroup$
    – user21820
    Commented Jun 8, 2022 at 20:01
  • 1
    $\begingroup$ "Is it always possible to prove whether the program terminates or not? Or is it provable that some programs cannot be proved either ways?" Your wording implies these are the two options, but I believe that it's possible to have a model in which there are programs that can't be proven to halt, but it's impossible to prove (within the model) that it's impossible to prove whether they halt. $\endgroup$
    – Acccumulation
    Commented Jun 12, 2022 at 17:27
  • $\begingroup$ @Acccumulation: You should use the term "theory" rather than "model" since the latter is already a standard term for something not what you're asking about. And there is an answer to your question: there is a true Σ1-sentence C such that PA ⊬ ◻︎C∨◻︎¬C∨◻︎¬(◻︎C∨◻︎¬C). The proof relativizes; there is such a sentence for any theory that interprets PA. And Σ1-sentences correspond to sentences about program halting. $\endgroup$
    – user21820
    Commented Jul 7, 2022 at 13:59

5 Answers 5

Reset to default
31
$\begingroup$

Actually this is no different from the halting problem unsolvability. If you have any formal system T with a proof verifier program V that can reason about programs (as you desire in your question), then let H be the program that does the following on input (P,X):
  For each string s in length-lexicographic order:
    If V( "Program P halts on input X." , s ) then output "true".
    If V( "Program P does not halt on input X." , s ) then output "false".
Here V(Q,s) outputs "true" if s is a valid proof of Q and "false" otherwise. V always halts, because that is what it means for T to have a proof verifier program. (And we cannot use and do not care about formal systems that do not.)

Now, if for every (P,X) there is always a proof over T of either "Program P halts on input X." or its negation, then H solves the halting problem (because H eventually checks each possible proof), which is impossible.

Here I am assuming that your T is sound for program halting (i.e. does not prove a false statement about program halting). Otherwise, it is possible that T proves the wrong thing and hence H fails to solve the halting problem.

By the way, unsolvability of the halting problem and another computability question called the zero-guessing problem are very important facts that can be used to easily prove the generalized incompleteness theorem, by essentially the same kind of reasoning. Incidentally, Godel proved his incompleteness theorem for PA under an assumption called ω-consistency, which is essentially equivalent to PA being sound for program halting. Rosser removed that assumption by a clever trick. But Rosser's version also can be proven easily using the zero-guessing problem instead of the halting problem.

Improve this answer
$\endgroup$
2
  • 10
    $\begingroup$ This answer directly addresses the question. The OP thought uniformity (one program generates proofs for all programs) and non-uniformity (there exists a proof for each program, not necessarily generated by one program) were different. This answer explains why they are actually the same. Negative comments expect this answer to delve into extreme pedantry, which is unnecessary and beside the point. $\endgroup$
    – Reinstate Monica
    Commented Jun 6, 2022 at 19:31
  • $\begingroup$ Comments are not for extended discussion; this conversation has been moved to chat. $\endgroup$
    – D.W. ♦
    Commented Jun 8, 2022 at 19:43
5
$\begingroup$

Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it allows the proof to depend on the specified program. It is thus a much weaker version.

The general halting problem already allows such program-specific proofs. Your stated problem is in fact completely identical to the general halting problem. Perhaps you have underestimated the potential complexity of what you call "mechanical procedures"? It is theoretically possible, though incredibly difficult, to create a "mechanical procedure" that duplicates the full capabilities of an expert living sapient human mathematician.

Or is it provable that some programs cannot be proved either ways?

If a program does halt, then it can be proven by simply running it until it halts. Any proof that a program cannot be proven to halt is therefore inherently a proof that it does not halt. "Cannot be proven either way" is a self-contradictory and thus invalid result of a proof about whether a particular program halts.

Improve this answer
$\endgroup$
2
  • 2
    $\begingroup$ Just to clarify: your statement that a mechanical procedure can duplicate a human is basically a form of the Church-Turing thesis, which empirically seems to be true, but is not logically true. It's possible that there is no computable emulation of the "true" physics on which our universe runs, for example, and in such a world it's possible that human thought makes essential use of this noncomputability. It seems very unlikely that this is the case, but it's not impossible. $\endgroup$
    – Patrick Stevens
    Commented Jun 6, 2022 at 21:29
  • $\begingroup$ @PatrickStevens: You're correct. There is a funny catch though. There seems to be no way to usefully utilize any uncomputable phenomenon except for RNG use. Suppose humans discover a real-world phenomenon that can be utilized to get a function that appears uncomputable. The problem is that absolutely nobody can verify it, so it remains useless. For example, even if someone claims to have found a real-world halting oracle, nobody can verify that it is not simply something that behaves like a deterministic human and takes 2^k seconds to answer "Does P halt on X" where k = len(P)+len(X). =) $\endgroup$
    – user21820
    Commented Jun 7, 2022 at 12:50
0
$\begingroup$

When you make an informal statement like "Is it provably true/false that for a program, there exists a proof whether it halts or not?", the "a" article is interpreted as a universal quantifier: if we increase the formality of the question it becomes: for every program P, is there a halting proof?

And this is what the Halting Problem informs us that there isn't, with careful definitions of what is meant by program and proof.

Unlike the general halting problem, this problem does not require a mechanical procedure to generate a proof for each program which can potentially depend on the procedure itself, but instead, it allows the proof to depend on the specified program

Here you seem to be expressing a belief that mechanical generation is qualitatively different from human generation: that if we allow a human to inspect every one of the infinite set of programs, the human may be able to decide halting every case, without it being possible to replicate what the human is doing by an algorithm, because the human isn't simply mechanical but "super mechanical".

Even if that were the case, it would mean that the human is somehow more powerful than a Turing machine. You would then have to carefully articulate the domain which is covered in your claim: that your claim isn't whether a Turing machine can decide halting over the domain of Turing machines, but whether a Human machine (possessing some magic oracle powers that transcend the power of Turing machines) can decide halting over the domain of Turing machines.

If we rephrase the statement along these lines, the answer is a resounding yes: machines from a domain more powerful than Turing machines can decide halting of all Turing machines.

Practically speaking, all we have is computers that are (not even quite) Turing machines. So the Turing machine set is of particular interest, because the results inform us about the limitations of the computers that we have.

If something cannot be "mechanically", you're not going to program your PC into solving it.

Given a program that takes no argument

This "no argument" requirement is a red herring; if you believe it makes any difference, you have to readjust your thinking.

We can take any program P which has an external input that is given to it as an argument, into an equivalent program Q which embeds that input and then takes no argument.

The set of all programs P with no arguments is exactly the same as the set of programs Q(I), which have inputs, for all possible inputs I. All the possible Q(I) pairs can each be combined into a single program image P.

Consider that the machine which Turing used to explore this problem domain doesn't have any arguments either: it is a combination of a simple mechanism, and a tape that loaded with some initial contents.

A program P with no arguments loaded into a machine is exactly the same thing as a Turing tape loaded into a tape machine; we can replace "given a program with no argument" with "given a Turing tape".

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ Thank you for the answer. I very much agree that my question originates from the gap of my understanding that differentiates programmatically generating proofs and elaborating proofs manually for a given problem. This gap is very well explained (away) by the accepted answer by pointing out that existence of a proof means exactly we can find that proof programmatically. $\endgroup$
    – DatoClement
    Commented Jun 7, 2022 at 2:07
  • 3
    $\begingroup$ For the "no argument" part. When posting the question, I have in mind that the proof being elaborated thus could not be passed as an argument of the tested program. This thought turns out incorrect by thinking about a proof verifier + a proof search is (almost) exactly that specific proof assuming consistency (so that the first proof that is found proves the same truthfulness/falsity as the hypothetical elaborated proof). But if not for the enumerability of the proofs (because they can be represented as strings), I think there COULD be different between "no argument" and otherwise. $\endgroup$
    – DatoClement
    Commented Jun 7, 2022 at 2:23
  • $\begingroup$ @DatoClement: That's correct! If you are interested in seeing phenomena where there is a crucial difference between having and not having inputs, here is one. Take your favourite foundational system T. Let B be the program that on input X sets V := "0" and goes through every proof of length at most len(X) and, for each such proof that verifies "P is total (i.e. halts on every input)" for some program P, sets V := V+P(X), and finally returns V. Now, suppose you believe that T is sound (does not prove false sentences). Then you must also believe that B is total. But T cannot prove that! $\endgroup$
    – user21820
    Commented Jun 7, 2022 at 10:32
  • $\begingroup$ (The reason is quite simple; if there is a proof W of "B is total" over T, then B(W) will find that proof and will output something longer than B(W)!) Although T cannot prove "B is total", T can prove "B(X) halts" for each string X! So T can prove halting of B for each input non-uniformly but cannot prove halting of B for all inputs uniformly. (Slight correction: B "goes through every proof over T of length at most len(X)".) Good? =) $\endgroup$
    – user21820
    Commented Jun 7, 2022 at 10:36
  • $\begingroup$ @DatoClement: I prefer the "no argument" version because I know I don't have to exclude the adler loop. (An ancient bug where the program went into an infinite loop waiting for further input that would never arrive because it blocked the ability to send said input; but another program could intervene and provide it.) $\endgroup$
    – Joshua
    Commented Jun 7, 2022 at 20:09
-2
$\begingroup$

If you're really asking about every program then of course not. Such proof would need to consider every possible outcome of every choice within the most complex program imaginable… which would make the proof more complex than the program, which would spin on its own axis until it ceased to matter.

If "for a program…" doesn't mean "for any and all programs" then what does it mean?

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ Thank you. ""If "for a program…" doesn't mean "for any and all programs" then what does it mean?"" Here I intended to mean one proof for each program. So what I had in mind is the case where we are given a program $P$ and we would like to determine whether this particular $P$ halts or not, with in mind that this proof might only works for $P$. But I think this remains equivalent to the general halting problem as answered by @user21820 $\endgroup$
    – DatoClement
    Commented Jun 6, 2022 at 2:02
  • $\begingroup$ @DatoClement Thanks and is that the same as what you first Posted? $\endgroup$
    – Robbie Goodwin
    Commented Jun 9, 2022 at 19:47
  • $\begingroup$ I am not sure if I fully understand the "that" in "is that the same as what you first Posted?", but the intention I talked about in the first comment is what I have when first posted. I like the wording of @Reinstate Monica in the comment of the accepted answer, which is clearer than what I said: "This answer directly addresses the question. The OP thought uniformity (one program generates proofs for all programs) and non-uniformity (there exists a proof for each program, not necessarily generated by one program) were different. [...]" $\endgroup$
    – DatoClement
    Commented Jun 10, 2022 at 3:05
-3
$\begingroup$

This is basically the Church-Turing hypothesis.

We know there are programs P such that no program X can prove that P halts, or that P doesn't halt. That's not what you asked. You asked "can we prove..." The Church-Turing hypothesis claims that everything "we" can do, some program could do. If the Church-Turing hypothesis is correct, then "we" cannot prove for every program that it halts. If it is incorrect, then "we" might be able to prove it for every program.

I can easily write a program that halts if it finds a counter-example to Fermat's Last Theorem, and that will eventually find a counter-example if one exists. "We" (or rather Andrew Wiles) proved that this program doesn't halt. It's not at all obvious that a computer program could have found this proof. Church-Turing says "yes".

Just for fun: If that FLT-counter-example-finder halts, then there is actually a very simple proof that it halts. (The proof would look like "The program will halt with a = xxx, b = xxx, c = xxx, n = xxx". ). So if there is no proof that it halts or doesn't halt, then it doesn't halt, but we might not have a proof for it.

Improve this answer
$\endgroup$
3
  • 1
    $\begingroup$ I agree that if we consider the reduction to the halting problem the easy part, then it sounds like a CT hypothesis. But can you clarify what you mean by "It's not at all obvious that a computer program could have found this proof."? Theoretically, the proof verifier program for ZFC can be trivially turned into a program that will find that proof. Do you doubt that? Or do you think that the waiting time is infeasible? I think it would be good to be clear on that since the asker seems to be thinking of ideal programs rather than real-world ones. Thanks! $\endgroup$
    – user21820
    Commented Jun 7, 2022 at 13:04
  • $\begingroup$ (By the way, I am not the downvoter.) $\endgroup$
    – user21820
    Commented Jun 7, 2022 at 13:23
  • $\begingroup$ A computer program could have found the proof. The best known algorithm iterates over all strings until it finds a proof for what is asked for, but it spins if there is no answer. $\endgroup$
    – Joshua
    Commented Jun 7, 2022 at 20:11

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.