Category:Total

A total programming language is one in which all programs are guaranteed to terminate. As such, such languages are not Turing complete. Self-interpretation in a total language is traditionally blocked by the normalization barrier, which states that total languages cannot compute their own normal forms. The normalization barrier can be circumvented in some cases but remains a standard example of the limitations of total languages.^[1] Nevertheless, total languages can express the most powerful finite-state machines possible. Additionally, programs which run indefinitely can be expressed as a sequence of total computations which each individually halt, simplifying proofs about their behavior.

For any Turing-complete language, there is a total language where each halting program is annotated with a proof that it halts. Proofs can be embedded into source code, computed using tactics, or synthesized using search, as long as the length of the proof is finite and it can be checked in polynomial time.

References