Intuitive explanation/overview of non-looping non-termination proofs

Question

Looping non-termination is intuitively easy to understand and demonstrate, by finding/showing a sequence of transformations that cycles back itself. Say, using the rewriting system:

Rule1: A=>B
Rule2: B=>A

starting with the term A leads to this cycle of repeated rewrite rule applications:

Rule1 -> Rule2
^____________|

A => B => A => B => A => ...

Also, without manually analyzing a system/program, one could keep track of all relevant state to the control flow at runtime and check if it re-enters a previously visited configuration, thus demonstrating the existence of an infinite loop.

I have not encountered a similarly simple example/explanation of non-looping non-termination and how one would prove it. Does one (or more?) generally used technique exist?

If so, can it prove all instances of non-looping non-termination given enough computation time and space?

Answer 1

Here's an intuitive explanation: if there's an infinite reduction/execution of a finite program, then there must be a program transition that is taken an infinite number of times. This is true for looping and non-looping termination for simple reasons (pigeonhole, I guess).

So it suffices to show is that a certain program transition with a certain state shape must eventually lead to taking that same program transition again, ideally with the same shape. In the case of looping termination that shape is always some concrete state, but it can be abstract. E.g. in D.W.'s answer the program transition is (say) the execution of the while block, and the abstract state is $$ i \mapsto \{v\}$$

where $v$ is any integer. One example technique is that of "pattern rules" used by Emmes, Enger and Giesl in Proving Non-Looping Non-Termination Automatically.

Answer 2

Checking termination is undecidable in many systems, so there is no systematic procedure that will always work.

Here is a very simple example of non-looping non-termination:

i = 0;
while (True) {
    i = i+1;
}

This will run forever without ever re-entering any previously visited configuration, incrementing $i$ each time (thus entering a new configuration each time).

Trivially, if you have a while-loop where we can prove that the condition is always True and where there is no other way to exit the loop, then the loop will run forever.

However there are some non-terminating programs that can't be proven to run forever by this method. Indeed, the undecidability of the halting problem tells us that there is no procedure you can use that will always allow you to prove every non-halting program doesn't halt.