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

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

<p>Non-looping non-termination is obviously more complex, but has been studied, e.g. in Emmes &amp; al <a href="https://verify.rwth-aachen.de/giesl/papers/IJCAR12.pdf" rel="nofollow noreferrer">Proving Non-Looping Non-Termination Automatically</a> or Endrullis &amp; al <a href="https://arxiv.org/pdf/1505.00478.pdf" rel="nofollow noreferrer">Proving Looping and Non-Looping Termination by Finite Automata</a>.</p>

CC BY-SA 3.0
2018-01-11T23:14:53.923Z
2018-01-11T23:14:53.923Z
cody
<p>Since the Halting problem is undecidable, whatever approach I use to answer the question must eventually be unhelpful in the real world.</p>

<p>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.</p>

<p><em>Proof</em>: 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.</p>

<p>I asked a more general question just before yours, by the way. <a href="https://cstheory.stackexchange.com/questions/39344/what-does-the-set-of-promises-for-which-the-halting-problem-is-decidable-look-li">What does the set of promises for which the halting problem is decidable look like?</a></p>

CC BY-SA 3.0
2017-10-21T20:51:12.870Z
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 ?)"*
user1952009
CC BY-SA 3.0
2017-10-21T21:03:43.627Z
In your *Proof* you are referring to the busy beaver function, so what ?
user1952009
CC BY-SA 3.0
2017-10-21T21:13:02.180Z
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.
Gurkenglas
CC BY-SA 3.0
2017-10-21T21:19:32.523Z
Yes I know that, so ? Many means "those whose (non)-termination is provable in PA", but I can't say much more.
user1952009
CC BY-SA 3.0
2017-10-22T01:03:37.330Z
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)$)
user1952009
CC BY-SA 3.0
2017-10-21T20:33:26.567Z
2017-10-21T20:47:59.333Z
2017-10-21T20:47:59.333Z
Gurkenglas
<p>If you are a computer and you are given a program <span class="math-container">$P$</span> (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)</p>
<p>I guess most people would say to translate the statement <em>&quot; <span class="math-container">$P$</span> doesn't halt &quot;</em> into an arithmetic sentence <span class="math-container">$\forall n, S(n) \ne 0$</span> (where <span class="math-container">$S(n+1) = P(S(n))$</span> is the <span class="math-container">$n$</span>-th state of the program) and enumerate the theorems of <a href="https://en.wikipedia.org/wiki/Peano_axioms" rel="noreferrer">PA</a> until it proves the sentence.  Or is there a more elegant way ?</p>
<p>Ie. how would you try (and success in) solving the halting problem, <strong>except</strong> in a few pathological cases  ?</p>
<p>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 <span class="math-container">$\scriptstyle\text{fewer}$</span> pathological cases) using a new routine enumerating the theorems of a meta-theory (which one) ?</p>
<p>Finally, is it hard to write the concrete code of all this, will it be readable and useful for teaching and for the intuition ?</p>
<hr />
<p><strong>Concretely</strong> 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 :</p>
<blockquote>
<p>Input : a program <span class="math-container">$P$</span> with no arguments. Let <span class="math-container">$ S(n+1) = P(S(n))$</span> be its sequence of states.</p>
<p>Compute <span class="math-container">$S(n),n=1,2,\ldots$</span>. If for some <span class="math-container">$n ,S(n)=0$</span> then output &quot;<span class="math-container">$P$</span> halts&quot;.</p>
<p>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 <span class="math-container">$\forall n, S(n+1) = P(S(n)) \land S(n) \ne 0$</span>, in that case output &quot;<span class="math-container">$P$</span> doesn't halt&quot;.</p>
<p>The other cases (<span class="math-container">$P$</span> doesn't halt but PA doesn't prove it) are said pathological.</p>
</blockquote>

CC BY-SA 3.0
2017-10-21T06:27:06.707Z
If you have just a few references and keywords I would appreciate.
user1952009
CC BY-SA 3.0
2017-10-21T09:44:15.497Z
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](https://scholar.google.pt/citations?user=pF27eLMAAAAJ&hl=en&oi=ao)
Mikolas
CC BY-SA 3.0
2017-10-21T18:16:35.280Z
@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.
user1952009
CC BY-SA 3.0
2017-10-21T18:33:40.693Z
Feel free to tell me how I should edit or concretize my question to make it easier to read.
user1952009
CC BY-SA 3.0
2017-10-21T18:40:32.870Z
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.
Mikolas
CC BY-SA 3.0
2017-10-21T18:46:58.143Z
@Mikolas If a program with no arguments terminates just run it until it does. The problem is if the program doesn't terminate. Yes I agree pathological cases is unclear (and that class of programs for which PA doesn't prove their non-termination is even more not recursively enumerable) that's part of my question : give some intuition on them.
user1952009
CC BY-SA 3.0
2017-10-21T18:48:52.087Z
@Mikolas Your linked papers are not of my level as they seem to be about implementing optimized algorithms for real life application, not just writing a simple algorithm and explaining why it may or may not work.
user1952009
CC BY-SA 3.0
2017-10-21T18:54:58.750Z
right, you can run it until is stops and if it doesn't you didn't prove anything, i.e. it's semidecidable. I would not call that trivial. It's still unclear to me what your question is. Maybe you could look into recursively approximable functions but that work's quite theoretical AFAIK.
Mikolas
CC BY-SA 3.0
2017-10-21T19:02:45.507Z
@Mikolas Why not enumerate the theorems of PA ? I think it can be done like this : when parenthesized and annotated correctly (apply inference rule $1$, inference rule $3$..) it is trivial to check if a given sentence in PA is a valid theorem. Thus we can enumerate the annotated sentences of PA and for each one, check if they are valid theorems, and check if it is proving $\forall n,S(n+1)=P(S(n))\land S(n)\ne0$, in that case the program doesn't terminate. In the same time, compute $S(n)$ for each $n$ and if you find $S(n)=0$ then the program terminates. The other cases are said pathological.
user1952009
CC BY-SA 3.0
2017-10-22T05:53:48.977Z
I very much doubt you can find the code for searching through all PA proofs to find the one you want. That sounds like an especially horribly inefficient way to find a proof of something.
Sasho Nikolov
CC BY-SA 3.0
2017-10-22T18:18:59.743Z
@SashoNikolov Sure, but efficiency isn't the point. If you have a better idea than enumerating the theorems of some axiomatic theory I would be glad to know it, that's part of my question.
user1952009
CC BY-SA 3.0
2017-10-23T10:13:17.003Z
A simple (intuitive, but exponential time and totally useless :-) ) algorithm for proving that a program $P$ halts based on the **promise** that $P \in LBA$ (see [Linear Bounded Automata](https://en.wikipedia.org/wiki/Linear_bounded_automaton)) is: run $P$ until it halts or it enters the same $\langle \text{ head position, state, tape content}\rangle$ configuration. Note that all real programs that run on real computers are actually $LBA$s.
Marzio De Biasi
CC BY-SA 3.0
2017-10-23T15:48:08.033Z
@user1952009 BTW it seems to me that your formulation only searches for a loop of length 1, but you might have longer loops. Also note that you might have a Turing machine that just keeps on writing 1's onto the tape, without ever stopping but the content of the tape is never the same, i.e. there's no loop in states.  Anyhow, obviously you could enumerate provably non-terminating programs but it's not clear why it would be interesting.
Mikolas
CC BY-SA 3.0
2017-10-24T00:07:53.503Z
@Mikolas What formulation ? Do you understand what means "proving that a given TM doesn't halt" ? Do you see why the Goldbach conjecture is equivalent to that a given TM doesn't halt ?
user1952009
CC BY-SA 3.0
2017-10-24T08:53:30.597Z
@user1952009 It wasn't clear to me you're going the Goldbach conj. I'd probably look for a function that would give an unbounded lower bound on the number steps of the progam. Anyhow, as I said, you can enumerate provably non-halting programs. It just doesn't seem very interesting.
Mikolas
CC BY-SA 3.0
2017-10-24T09:02:52.023Z
@Mikolas What is not interesting ? Do you understand now the point of enumerating the theorems of an axiomatic theory ? In general the non-decreasing invariant showing the program doesn't halt has no reason to be obvious, see the program encoding the Goldbach conjecture.
user1952009
CC BY-SA 3.0
2017-11-07T20:01:32.777Z
@jkabrg No I didn't. Isn't this mainly about the problem of designing programming languages (CoQ is in some sense one of those ?) such that the programmer writes his program and in same time a proof of its termination ?
user1952009
<lo.logic><automated-theorem-proving><halting-problem>
Automated proving that a program doesn't halt
user1952009
# Automated proving that a program doesn't halt

(Asked by: username_0 on 2017-10-21)

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](https://en.wikipedia.org/wiki/Peano_axioms) 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.

**Tags:** lo.logic, automated-theorem-proving, halting-problem
> **Comments:**
> **username_0**: If you have just a few references and keywords I would appreciate.  
> **username_1**: 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](https://scholar.google.pt/citations?user=pF27eLMAAAAJ&hl=en&oi=ao)  
> **username_0**: @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.  
> **username_0**: Feel free to tell me how I should edit or concretize my question to make it easier to read.  
> **username_1**: 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.  
> **username_0**: @Mikolas If a program with no arguments terminates just run it until it does. The problem is if the program doesn't terminate. Yes I agree pathological cases is unclear (and that class of programs for which PA doesn't prove their non-termination is even more not recursively enumerable) that's part of my question : give some intuition on them.  
> **username_0**: @Mikolas Your linked papers are not of my level as they seem to be about implementing optimized algorithms for real life application, not just writing a simple algorithm and explaining why it may or may not work.  
> **username_1**: right, you can run it until is stops and if it doesn't you didn't prove anything, i.e. it's semidecidable. I would not call that trivial. It's still unclear to me what your question is. Maybe you could look into recursively approximable functions but that work's quite theoretical AFAIK.  
> **username_0**: @Mikolas Why not enumerate the theorems of PA ? I think it can be done like this : when parenthesized and annotated correctly (apply inference rule $1$, inference rule $3$..) it is trivial to check if a given sentence in PA is a valid theorem. Thus we can enumerate the annotated sentences of PA and for each one, check if they are valid theorems, and check if it is proving $\forall n,S(n+1)=P(S(n))\land S(n)\ne0$, in that case the program doesn't terminate. In the same time, compute $S(n)$ for each $n$ and if you find $S(n)=0$ then the program terminates. The other cases are said pathological.  
> **username_2**: I very much doubt you can find the code for searching through all PA proofs to find the one you want. That sounds like an especially horribly inefficient way to find a proof of something.  
> **username_0**: @SashoNikolov Sure, but efficiency isn't the point. If you have a better idea than enumerating the theorems of some axiomatic theory I would be glad to know it, that's part of my question.  
> **username_3**: A simple (intuitive, but exponential time and totally useless :-) ) algorithm for proving that a program $P$ halts based on the **promise** that $P \in LBA$ (see [Linear Bounded Automata](https://en.wikipedia.org/wiki/Linear_bounded_automaton)) is: run $P$ until it halts or it enters the same $\langle \text{ head position, state, tape content}\rangle$ configuration. Note that all real programs that run on real computers are actually $LBA$s.  
> **username_1**: @user1952009 BTW it seems to me that your formulation only searches for a loop of length 1, but you might have longer loops. Also note that you might have a Turing machine that just keeps on writing 1's onto the tape, without ever stopping but the content of the tape is never the same, i.e. there's no loop in states.  Anyhow, obviously you could enumerate provably non-terminating programs but it's not clear why it would be interesting.  
> **username_0**: @Mikolas What formulation ? Do you understand what means "proving that a given TM doesn't halt" ? Do you see why the Goldbach conjecture is equivalent to that a given TM doesn't halt ?  
> **username_1**: @user1952009 It wasn't clear to me you're going the Goldbach conj. I'd probably look for a function that would give an unbounded lower bound on the number steps of the progam. Anyhow, as I said, you can enumerate provably non-halting programs. It just doesn't seem very interesting.  
> **username_0**: @Mikolas What is not interesting ? Do you understand now the point of enumerating the theorems of an axiomatic theory ? In general the non-decreasing invariant showing the program doesn't halt has no reason to be obvious, see the program encoding the Goldbach conjecture.  
> **username_0**: @jkabrg No I didn't. Isn't this mainly about the problem of designing programming languages (CoQ is in some sense one of those ?) such that the programmer writes his program and in same time a proof of its termination ?  

---

## 2 answers

### Answer by username_4 on 2018-01-11. Score: 2

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](https://verify.rwth-aachen.de/giesl/papers/IJCAR12.pdf) or Endrullis & al [Proving Looping and Non-Looping Termination by Finite Automata](https://arxiv.org/pdf/1505.00478.pdf).


---

### Answer by username_5 on 2017-10-21. Score: 1

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?](https://cstheory.stackexchange.com/questions/39344/what-does-the-set-of-promises-for-which-the-halting-problem-is-decidable-look-li)

> **Comments:**
> **username_0**: 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 ?)"*  
> **username_0**: In your *Proof* you are referring to the busy beaver function, so what ?  
> **username_5**: 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.  
> **username_0**: Yes I know that, so ? Many means "those whose (non)-termination is provable in PA", but I can't say much more.  
> **username_0**: 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)$)  

---

