0
$\begingroup$

The halting problem is semi-decidable, which means that if a program terminates then it will always be able to be determined.

Some programs can be proven to terminate without running them, with say:

  • induction
  • typed theories, such as typed lambda calculus.
  • Ackermann function

Are there some programs for which there is no other proof system except for the computation itself, where no properties of the program is know in advanced? And hence if so, it would make sense that some non-terminating programs, even though it can be proven to terminate eventually, we don't know how long that proof would take to compute, because it would not be known if the program simply needs to run for longer, because as stated above, not even the property of how long the program should run before we can determine if it should have terminated yet, is known in advanced.

Are there some programs for which the only proof of termination, is the actual running of the program, and waiting to see if it stops, no matter how long it takes to complete?

Improve this question
$\endgroup$
3
  • $\begingroup$ I suspect you can prove this as yes, for Turing machines, using something very similar to the halting problem uncomputability proof $\endgroup$
    – user253751
    Oct 11, 2022 at 14:11
  • $\begingroup$ A problem with your question seems to be that "proof" depends on the theory (axioms and derivation rules) that you choose. If you fix the theory you may well be able to show the existence of programs for which there is no proof of termination (in the chosen axiomatic system). The question then reminds one a little of Godels incompleteness results. I don't think your question as stated can be answered because of the lack of a specific theory in which your proofs are developed. $\endgroup$
    – Michel
    Oct 11, 2022 at 14:43
  • $\begingroup$ In my previous comment, I was referring to proving that no program can determine that some programs halt in n steps, using less than n steps - which is a more exact specification than the question $\endgroup$
    – user253751
    Oct 11, 2022 at 14:44

2 Answers 2

Reset to default
1
$\begingroup$

"Are there some programs for which there is no other proof system except for the computation itself, where no properties of the program is know in advanced?" No. For a Turing machine T and input X such that T(X) halts, there is a formal system consisting of the appropriate Turing machine axioms and the axiom "T(X) halts" that proves T(X) halts.

To really answer this question, you'd need a defined formal system and definition for computation versus other forms of proof.

Improve this answer
$\endgroup$
2
  • $\begingroup$ I don't believe that that is a proof that T(X) halts. That is just a claim [which may or may not be true) without any evidence. $\endgroup$
    – RFV
    Oct 11, 2022 at 15:52
  • 1
    $\begingroup$ @RFV That's what axioms are, just claims. The Axiom of the Empty Set, that a set without any elements exists, is just as much a claim without any evidence. Sometimes formal systems are proven inconsistent, as was New Foundations with the Axiom of Choice. It's possible "T(X) halts" + axioms for Turing machines is inconsistent, but within that system, it's provable that T(X) halts. $\endgroup$
    – prosfilaes
    Oct 11, 2022 at 16:22
1
$\begingroup$

Since for all programs with a set of possible inputs which are countably infinite [except 0-arry functions i.e. constant functions], it would not be possible even to run the program until it terminates for all inputs.

Therefor it would not even be possible to prove termination by simply running the program until it terminates.

Improve this answer
$\endgroup$

Your Answer

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

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