Can we enumerate provably non-terminating functions?

Question

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:

1. Convert Turing machine to corresponding Diophantine equation with one unknown
2. Feed the equation, along with First-Order Peano Arithmetic, to Prolog/Isabelle/your favorite proof assistant
3. Assert the existence of a solution
4. 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:

  1. Start with a basic definition of "strings" in pure First-Order Logic: 0,1,add0,add1,equality
  2. Define Turing machines using a rewrite relation on strings that captures the mechanics of a calculation step (ie, eval)
  3. Define big-step calculation $\rightarrow$ as the transitive closure of one-step eval
  4. Define a halting predicate as the existence of a fixed point
  5. 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?

Answer 1

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?

You do not need this conversion. One can directly formalize what a Turing machine is in Coq/Isabelle/... and directly define its semantics there.

That is, it is possible to define a function eval (tm: TuringMachine) (input: nat) (steps: nat) which returns the Turing machine configuration (state & tape) obtained by running tm with an initial tape carrying the input for that many steps. From this, defining non-termination is simple.

Note, however, that enumerating non-terminating Turing machines in this way will generate the same set of machines as if you converted to Diophantine equations. Indeed, if you can prove the soundness and completeness of the conversion in your proof system, then a direct proof of non-termination exists iff a proof for no-solution in the Diophantine system exists. This is because the conversion theorem allows to transform one proof into the other.

Answer 2

Here is a simple non-terminating function:

while (true):
    do nothing

This certainly does not terminate.

On the other hand, it is not possible to enumerate all non-terminating functions. The halting problem is recursively enumerable but not decidable, from which it follows that the complement of the halting problem is not recursively enumerable (if it were, the halting problem would be decidable). See https://en.wikipedia.org/wiki/Recursively_enumerable_language and https://en.wikipedia.org/wiki/RE_%28complexity%29.