A simple, general method for constructing termination proofs involves associating a measure with each step of an algorithm.
However, it may halt when executed on a physical machine due to arithmetic overflow: either leading to an exception or causing the counter to wrap to a negative value and enabling the loop condition to be fulfilled.
There is, however, no general procedure for determining whether an expression involving looping instructions will halt, even when humans are tasked with the inspection.
The theoretical reason for this is the undecidability of the Halting Problem: there cannot exist some algorithm which determines whether any given program stops after finitely many computation steps.
In practice one fails to show termination (or non-termination) because every algorithm works with a finite set of methods being able to extract relevant information out of a given program.
Termination check is very important in dependently typed programming language and theorem proving systems like Coq and Agda.
However, it was found later that describing a program via a recursively defined function with pattern matching is a more natural way of proving than using induction principles directly.
Unfortunately, allowing non-terminating definitions leads to logical inconsistency in type theories[citation needed], which is why Agda and Coq have termination checkers built-in.
The research community also works on new methods to analyze termination behavior of programs written in imperative languages like C and Java.