In trying to understand the Halting Problem better, I am trying to come up with classes of provably non-terminating programs.
For example, any program (including input) which leads to a finite-length infinite loop (with perfectly repeating state+tape) should be detectable. That leaves mostly induction/search problems like "get the first non-Goldbach even number above 4" as candidates.
Clearly, some of these halt, and some can be proven non-halting (eg we know "find $n$ such that $n\cdot 0=5$ " and "find a proof that the Poincare Conjecture is false" would not halt). More generally, it seems every non-halting problem corresponds to a Diophantine equation which (provably or not) has no solutions. This leads to a seemingly fairly general algorithm to find many non-halting programs:
- Convert Turing machine to corresponding Diophantine equation with one unknown
- Feed the equation, along with First-Order Peano Arithmetic, to Prolog/Isabelle/your favorite proof assistant
- Assert the existence of a solution
- Derive 0=1
So, my questions:
Is there a more natural way to search for such contradictions using the formalism of Turing Machines (or some other more conventional model of computation), without converting to Diophantine equations?
Are there provably non-terminating functions that can be found using some other algorithm, but not this one? What algorithm(s)? Would that require a "stronger" version of arithmetic?
If there are such algorithms, is there any notion of a "biggest" class of provably non-halting programs, or would that somehow lead to solving the Halting Problem (or some other contradiction)?
Are there any good references/keywords for this? I've searched for "provably non-terminating functions", but haven't come up with much
PS Feel free to fix/reformat anything, alert me to obvious theoretical mistakes, or let me know if this is a bad question.
EDIT: Some points to address responses so far:
I know that it's "easy" to prove that a program halts--just run it until it does; the challenge is to prove that a program does not halt, which obviously isn't always possible.
Re: D.W.♦, I know we can't enumerate all non-halting programs, and I know we can come up with many provable examples of non-terminating functions, I'm asking if there's a most general method of finding all non-halting programs that can be found/proven
I am aware of the Curry-Howard correspondance that directly relates programs and mathematical proofs. However, because of the halting problem there can be no type for "non-terminating programs", and it's not immediately obvious how to type "provably non-terminating" either
@chi's answer is exactly what I am looking for. To make sure I understand fully, let me restate my understanding of your enumeration of non-terminating programs, using the simplest possible axioms I can think of:
- Start with a basic definition of "strings" in pure First-Order Logic: 0,1,add0,add1,equality
- Define Turing machines using a rewrite relation on strings that captures the mechanics of a calculation step (ie, eval)
- Define big-step calculation $\rightarrow$ as the transitive closure of one-step eval
- Define a halting predicate as the existence of a fixed point
- For a given program $x$, prove $\forall y.x\rightarrow y\Rightarrow \exists z\ne y.y\rightarrow z$
So, would the above work? Is it equivalent to my Diophantine equation scheme? Is there a yet simpler version? Would more axioms (eg using naturals under Peano Arithmetic to encode the machines) be able to prove more non-terminating programs than this version, ie is there a more general method?