principleMajor
Halting problem theory vs. practice
Viewed 0 times
theoryproblemhaltingpractice
Problem
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.
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.
Solution
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.
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.
Context
StackExchange Computer Science Q#125560, answer score: 20
Revisions (0)
No revisions yet.