Halting problem theory vs. practice

Question

It is often asserted that the halting problem is undecidable. And proving it is indeed trivial.

But that only applies to an arbitrary program.

Has there been any study regarding classes of programs humans usually make?

It can sometimes be easy to analyze a program and enumerate all of its degrees of freedom and conclude that it will halt.

For example, has there ever been an effort to create a programming language (scripting really) that guarantees halting? It would not be widely applicable but could still be useful for mission critical modules.

Answer 1

Languages that are guaranteed to halt have seen wide spread use. Languages like Coq/Agda/Idris are all in this category. Many many type systems are in fact ensured to halt such as System F or any of its variants for instance. It's common for the soundness of a type system to boil down to proving that all programs normalize in it. Strong normalization is a very desirable property in general in programming languages research.

I haven't seen a lot of success in catching infinite loops in practice however "Ensuring Termination in ESFP" by Telford and Turner shows a more robust termination checker that was able to prove that Euclid's algorithm always terminated and handles partial cases. Euclid's algorithm is a famously tricky example of a primitive recursive function that isn't straightforwardly provable to be primitive recursive. It fails checkers that simply look for a decreasing parameter (or some simple pattern of decreasing parameters like Foetus termination checker). To implement this using primitive recursive combinators you have to encode a proof of termination for the algorithm as a parameter in the function essentially.

I can't think of any results for procedural languages off the top of my head and most results in functional languages use some kind of restriction that makes the obviously terminate rather than trying to perform some kind of complex analysis to ensure that more natural programs terminate.

Answer 2

There is past and current research on this. Such problem is called Termination Analysis, and a quick look on Google (Scholar) provides several old as well as new publications on this:

1. 2005, Termination Analysis of Higher-Order Functional Programs;
2. 2006, Automated Termination Analysis for Haskell;
3. 2008, Termination Analysis of Logic Programs based on Dependency Graphs;
4. 2010, Loop summarization and termination analysis;
5. 2014, Termination Analysis by Learning Terminating Programs;
6. 2015, Termination analysis with recursive calling graphs;
7. 2019, Static Termination Analysis for Event-driven Distributed Algorithms;
8. 2019, Implementing termination analysis on quantum programming;

Including existing languages with in-built mechanisms for that such as:

• Mercury;
• Idris, Coq, Agda;

Answer 3

Microsoft has developed a practical code checker (whose name escapes me at the moment) which performs halt-testing. It exploits the fact that the code it checks is human-written and not arbitrary, just as you suggest. More importantly, it bypasses the impossibility proof by being allowed to return the answer 'Cannot decide' if it runs into code too difficult to check.

Answer 4

There are only 2 types of infinite programs:

1. Those that repeat their own state after a point (cyclical)
2. Those that grow indefinitely in used memory

Those in 1st type, follow this pattern:

Where there is a pair of distinct indices i and j such that xi = xj, and after which the cycle repeats itself again (thanks to the deterministic nature of programs). In this case the inputs x, contain the whole memory and variables used by the algorithm, plus the current instruction pointer.

Cycle detection algorithms work very well in practice for this type and can prove that a given cyclical program will never finish, usually after a small number of steps, for most random programs.

Proving those in the 2nd type is where the challenge is. One could argue that type 2 can never exist in reality (as all computers have finite memory) but that is not very useful in practice because the memory used may grow very slowly for a regular computer to ever be full. A simple example of that is a binary counter that never stops and never repeats its full state completely.

Answer 5

There is a huge class of functions that are trivially guaranteed to halt: Everything with a finite number of loops, with an upper limit for the number of iterations for each loop determined before the loop is started.

If you have a random program, it can be difficult to prove whether or not it halts. Programs that are written for a purpose are usually much easier.

Answer 6

The smart contracts functions in the Ethereum blockchain are an example of a system that needs the guarantee of halting, not to stall the whole chain.

Every function has a gas cost, and the gas cost translates into real Ethereum coins. A transaction fee must be paid to call the contract. If the gas used in the contract exceed the gas paid with the transaction fee, the computation terminates immediately.