22
$\begingroup$

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.

Improve this question
$\endgroup$
9
  • 1
    $\begingroup$ You don't need the programming language to force totality of the program. What you need for mission-critical code is a sufficiently simple programming language coupled with a proof verifier, where you can provide a proof of termination that can be verified. Programming languages that only allow total programs would be just a very restrictive kind (i.e. no termination proof required). But it is far more useful to have a general-purpose programming language that allows human proofs of program termination. Such programming languages and verifiers do exist, but I am not an expert in this. $\endgroup$
    – user21820
    Commented May 12, 2020 at 7:34
  • $\begingroup$ A related, and also interesting (and limiting) theorem: Rice's Theorem $\endgroup$
    – Polygnome
    Commented May 12, 2020 at 10:13
  • 4
    $\begingroup$ Well, one could say that in practice, every program terminates as it eventually runs out of space or time. $\endgroup$
    – IS4
    Commented May 12, 2020 at 10:58
  • $\begingroup$ @user21820 I think it's useful to have total code, total functions, a total sub-language, so that you can concentrate on the rest. In the same way you have const, final, notnull, etc. keywords to restrict your code. Restricted is good (for the particular tasks that can be implemented, of course). :-) $\endgroup$
    – Pablo H
    Commented May 12, 2020 at 16:31
  • $\begingroup$ @PabloH: I think you're saying exactly the same thing as I did. =) A general-purpose programming language that allows termination proofs can do so via both static verification (such as for a restricted sublanguage) and human-assisted verification. Off-topic, but I always found Java's final keyword slightly annoying because it did not prevent performing operations on that final object, which means that immutable data structures implemented as generic classes are only immutable if the inputs are themselves immutable. $\endgroup$
    – user21820
    Commented May 12, 2020 at 16:38

6 Answers 6

Reset to default
20
$\begingroup$

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.

Improve this answer
$\endgroup$
5
  • 3
    $\begingroup$ Dhall also falls into this category, but is not a proof assistent kind of language, for one. It explicitely makes totality a goal for safety reasons. $\endgroup$
    – phipsgabler
    Commented May 12, 2020 at 6:56
  • $\begingroup$ eBPF is another example in practical use. It allows user programs to submit small pieces of code to be run by the kernel when certain events occur, and one of the restrictions on the instruction set is that all branches must be forward. Basically it only accepts provably-halting programs. $\endgroup$
    – hobbs
    Commented May 12, 2020 at 16:39
  • $\begingroup$ Formality is a (kinda) procedural language that forbids infinite loops (when you use the type checker). Last I checked, you satisfied the requirement by either specifying a max recursion depth, or by providing a proof that your code does indeed terminate. It's still a pretty beta-stage language, still in flux I think, but it has some nifty ideas, and (last I checked) it's quite operational. $\endgroup$
    – Erhannis
    Commented May 12, 2020 at 18:30
  • $\begingroup$ Languages that are guaranteed to halt are somewhat of a red herring because a generalization of the haling theorem ("bounded halting"), with an almost equivalent proof, applies to them as well, which means that proving properties about them is also O(|state space|), as in the "Turing-complete" case. While the effort in those cases is always finite, it can be arbitrarily large. Those languages are, therefore, no easier to verify in the general case, and they don't help in some "common case", whatever it may be. $\endgroup$
    – pron
    Commented Jun 4, 2020 at 13:29
  • $\begingroup$ That's a strong point! Also not only do you pay the price of no verification but you also pay an additional development price of some programs being exponentially longer to write due to Blum's theorem. You better really need it for some kind of property like soundness if you take it, but in all the cases I mentioned, low and behold you do in fact need that. So it's not a red hearing unless you have a different goal in mind. $\endgroup$
    – Jake
    Commented Jun 4, 2020 at 19:38
2
$\begingroup$

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:

Improve this answer
$\endgroup$
1
$\begingroup$

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.

Improve this answer
$\endgroup$
2
  • 1
    $\begingroup$ T2? en.wikipedia.org/wiki/T2_Temporal_Prover $\endgroup$
    – cody
    Commented May 12, 2020 at 19:32
  • $\begingroup$ Nice! Good to know about this. I might give this a try and see how useful it is in practice. I wonder if this isn't a lot more useful in practice than the functional stuff I'm aware of. $\endgroup$
    – Jake
    Commented May 13, 2020 at 17:31
1
$\begingroup$

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:

enter image description here

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$
0
$\begingroup$

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.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.