2
$\begingroup$

If you are a computer and you are given a program $P$ (with no input parameter) that doesn't halt, how would you try proving it doesn't halt ? (here proving means convincing ourselves that it is true)

I guess most people would say to translate the statement " $P$ doesn't halt " into an arithmetic sentence $\forall n, S(n) \ne 0$ (where $S(n+1) = P(S(n))$ is the $n$-th state of the program) and enumerate the theorems of PA until it proves the sentence. Or is there a more elegant way ?

Ie. how would you try (and success in) solving the halting problem, except in a few pathological cases ?

Then I'd like to get some intuition on how to visualize (and solve) those pathological cases arising from undecidable problems (in PA). Is there a way to solve them (except in a $\scriptstyle\text{fewer}$ pathological cases) using a new routine enumerating the theorems of a meta-theory (which one) ?

Finally, is it hard to write the concrete code of all this, will it be readable and useful for teaching and for the intuition ?

Concretely I'm asking if this is the algorithm I'm supposed to think to, in that case can I find the concrete code of it somewhere :

Input : a program $P$ with no arguments. Let $ S(n+1) = P(S(n))$ be its sequence of states.

Compute $S(n),n=1,2,\ldots$. If for some $n ,S(n)=0$ then output "$P$ halts".

In the same time enumerate the parenthesized and annotated sentences of PA, where the annotation indicates which inference rules to apply, thus it is trivial to check if a given sentence is a valid theorem of PA and if it proves $\forall n, S(n+1) = P(S(n)) \land S(n) \ne 0$, in that case output "$P$ doesn't halt".

The other cases ($P$ doesn't halt but PA doesn't prove it) are said pathological.

Improve this question
$\endgroup$
17
  • $\begingroup$ If you have just a few references and keywords I would appreciate. $\endgroup$
    – user1952009
    Oct 21, 2017 at 6:27
  • $\begingroup$ You might want to concertize your question. Nevertheless, the standard way of proving termination is to show that you have a decreasing function along the program's run (a measure). E.g. for WHILE C DO P, one shows there's a function F that decreases for each execution of P and is bounded from below. Doing this automatically is very hard. There's a lot of papers, you could start here $\endgroup$
    – Mikolas
    Oct 21, 2017 at 9:44
  • $\begingroup$ @Mikolas Hi, I would like to understand how (theoretically, ie. no matter if it takes billion of years of computation) we can prove non-termination, as proving termination is trivial for programs without input arguments. My goal is really the last sentence : can you show an algorithm for solving the halting problem (expect in some pathological cases) and show how those pathological cases can be partially solved using a longer algorithm. $\endgroup$
    – user1952009
    Oct 21, 2017 at 18:16
  • $\begingroup$ Feel free to tell me how I should edit or concretize my question to make it easier to read. $\endgroup$
    – user1952009
    Oct 21, 2017 at 18:33
  • 1
    $\begingroup$ I'm not sure what you mean that termination is trivial, it's undecidable with or without arguments. It's true that it's semidecidable and the set of terminating programs is recursively enumerable. To prove non-termination, you could try to come up with a unbouded function that is a lower bound on the number of loops in your program (for instance). Note that the set of non-terminating programs is not recursively enumerable. It's unclear what you mean by pathological cases. $\endgroup$
    – Mikolas
    Oct 21, 2017 at 18:40

2 Answers 2

Reset to default
2
$\begingroup$

In contradiction with Gurkenglas' answer, there actually is a community of scientists who work on proving non-termination of programs in various language and formalisms.

An obvious approach would be to check for looping non-termination: for a given program $w$, pick an input $x$ and check to see if the same state is reached twice with the same data.

Non-looping non-termination is obviously more complex, but has been studied, e.g. in Emmes & al Proving Non-Looping Non-Termination Automatically or Endrullis & al Proving Looping and Non-Looping Termination by Finite Automata.

Improve this answer
$\endgroup$
1
$\begingroup$

Since the Halting problem is undecidable, whatever approach I use to answer the question must eventually be unhelpful in the real world.

There's a sequence of sets of programs such that each set is contained in the next, their union contains all programs, and for the nth set there's a program of length in O(n) that decides haltingness in it.

Proof: The nth set is the set of programs of length at most n, the nth program contains a specification of that program of length at most n which runs the longest and then halts, and it decides haltingness by checking whether the longest-running-and-then-halting program in the set runs longer than the program to decide haltingness on.

I asked a more general question just before yours, by the way. What does the set of promises for which the halting problem is decidable look like?

Improve this answer
$\endgroup$
5
  • $\begingroup$ Hi, I'm really asking about the idea of "enumerating the theorems of some theories to solve the halting problem for many TM". The answer isn't "that doesn't solve the halting problem" but "that does solve the halting problem for many TM (which ones ?)" $\endgroup$
    – user1952009
    Oct 21, 2017 at 20:51
  • $\begingroup$ In your Proof you are referring to the busy beaver function, so what ? $\endgroup$
    – user1952009
    Oct 21, 2017 at 21:03
  • $\begingroup$ What does "many" mean? Each of these programs solves the halting problem for a successively larger set, the limit being all programs. You can see these as adding axioms of form "P is the longest-running-and-then-halting program of length at most n" - enumerating all theorems that follow is a trivial modification. $\endgroup$
    – Gurkenglas
    Oct 21, 2017 at 21:13
  • $\begingroup$ Yes I know that, so ? Many means "those whose (non)-termination is provable in PA", but I can't say much more. $\endgroup$
    – user1952009
    Oct 21, 2017 at 21:19
  • $\begingroup$ Afteralll we have : halting problem for every TM $=$ busy beaver for every $n$ = a sequence of axiomatic theories (whose theorems are enumerable) solving the halting problem for all TM. It doesn't change that we don't know $bb$ but we know strategies to compute $bb(n)$ for $n$ small, for example by using PA to solve the halting problem for TM of length $1,2,3\ldots$ (this program enumerating TM and theorems of PA doesn't terminate but it does output some correct values of $bb(n)$) $\endgroup$
    – user1952009
    Oct 22, 2017 at 1:03

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.