Termination Checking and the Price of Consistency

A type theory that is used as a logic must be consistent, and consistency follows from normalisation: if every term of the empty type reduces to a value, and the empty type has no values, then no closed term inhabits it. General recursion destroys the argument. A recursive definition with no decreasing measure can produce a term of any type, and once that is possible the logic collapses. Every language that wants both computation and consistency has to restrict recursion, and every restriction rejects programs that a human can see terminate.

Why the fixpoint is the problem

In the untyped lambda calculus, the term (λx. x x)(λx. x x) reduces to itself. In a typed calculus, the same divergence is available through a fixpoint operator with type (A → A) → A, which is the typing of a recursive definition. If that operator is available for every A, then in particular it is available for the empty type, and the language has a closed term of the empty type.

The point is not that divergence is inconvenient. It is that divergence and inconsistency are the same fact, seen from two sides. In a proof-relevant reading, a term of type A is a proof of A, and a term of the empty type is a proof of falsehood. Under the correspondence of Proof Terms, non-termination and the ability to prove anything are one phenomenon.

The converse is not automatic. A language whose every definable term terminates may still be inconsistent for other reasons, such as an inconsistent axiom or a universe rule that allows a type to contain itself. Termination is necessary for consistency in this setting, not sufficient.

Structural recursion and the size of a constructor

The simplest restriction is structural recursion: a recursive call is permitted only on a syntactic subterm of the argument, and the argument must be an inductive value whose constructors are known. The checker compares the arguments of the recursive call with those of the enclosing definition, position by position, and accepts if one argument is a subterm of the corresponding argument and no other argument is larger.

For natural numbers, the constructor suc contains its predecessor, so a call on the predecessor is a call on a subterm. For lists, the tail of a cons cell is a subterm. For a parameterised structure the checker must handle parameters and indices: a call on a structurally smaller element of an index is not a subterm of the argument unless the index is itself a subterm, which is why indexed structures need more than the basic rule.

The check is conservative in both directions. It accepts definitions that are not structurally decreasing on paper but happen to be written so that a syntactic argument shrinks, and it rejects definitions that decrease in a way the syntax does not expose, such as a function that divides its argument by two before recursing. The rejection is not a bug; deciding termination of arbitrary recursive definitions is undecidable, so any checker must reject some terminating programs.

Lexicographic and size-change orders

The first extension beyond single-argument structural descent is a lexicographic order on several arguments. Under the lexicographic order on tuples, a later argument may decrease provided every earlier one is unchanged, and an earlier argument may decrease regardless of what happens to the later ones, because the earlier position decides the comparison. The order corresponds to the termination argument for Ackermann-style functions, where the recursion decreases one argument, or decreases a later argument after an earlier one has been reset upward.

The general form of this idea is the size-change principle. For each call, the checker records for each pair of positions whether that parameter of the caller is larger, equal to, or smaller than that parameter of the callee, and whether it is unknown: the relation between two positions, not just the relation of a position to itself, because a parameter can be passed into a different slot. A program terminates if every infinite call sequence would produce an infinitely descending chain of values. The check is decidable, and it is carried out by composing the size-change graphs along call paths and testing whether the result is idempotent — a condition that forces any infinite sequence of calls to decrease a value infinitely often. The formulation is the one established by Lee, Jones and Ben-Amram.

Size-change termination is strictly more general than lexicographic descent and still decidable, and it is still incomplete. It reasons about sizes, not about values, so a function that recurses on a number derived by arithmetic the analysis cannot relate to a parameter’s size is rejected even if it terminates. This is the standard situation with division-based algorithms and with functions over integers represented as differences.

Guardedness and coinduction

The dual problem appears with infinite structures. A definition that produces an infinite stream cannot be structurally recursive on its output, because the output has no constructors to descend into. The check is instead that every recursive call is guarded: the recursive reference must occur under a constructor former, so that evaluating the result one observation’s worth forces the recursive step no more directly than through a constructor. Productivity pairs the guard with the requirement that the recursive call is reachable at all, since a definition whose recursive reference sits inside a branch that is never taken passes the syntactic guard check while producing nothing.

Guardedness and termination are different conditions and neither implies the other. A stream definition that is productive but not terminating, such as one that computes each element by a divergent function, is guarded and useless. A terminating definition that produces a stream without a guard is rejected because the checker cannot see that the stream is productive. The two checks are typically implemented by different analyses, and a language that supports both has to keep them apart.

The interaction with dependent types is where the analyses become delicate. A coinductive type indexed by a size, as in sized types, lets the checker track how many observations remain, which makes some definitions guarded that the syntactic check rejects. The mechanism is a type-level annotation of sizes, and it is a design commitment: it changes the surface language, not only the checker.

What the restriction costs the programmer

Three costs are routine.

Refactoring for the checker. A definition that recurses on a value computed from the argument is rewritten to carry an explicit counter or an accessibility proof. The rewritten version is longer and its relation to the original is a lemma, which the programmer must prove. The cost is real and it is paid at every such boundary.

Loss of convenient idioms. Mutual recursion between functions over different types requires either a combined inductive type or a size-change argument that the checker can follow. Some natural formulations are rejected, and the alternatives are less readable.

Proof obligations at the boundary. A function defined by well-founded recursion is total, and its type does not record which well-founded relation justifies it, so a caller cannot recover the measure from the signature. Conversely, a function defined by general recursion and then proved terminating by an external argument cannot be used in types, because the checker’s evaluator does not know it terminates. The boundary between the two worlds has to be crossed explicitly, usually by providing a well-founded relation and a proof that the recursion respects it.

The alternatives and what they assume

A language can avoid the restriction by giving up consistency. Most programming languages do this: general recursion is available, types are not treated as propositions, and the type system’s guarantees are about runtime behaviour rather than about truth. This is a coherent design, and it is the right one when the goal is to write programs rather than to prove theorems.

A language can also keep general recursion and recover consistency by restricting where recursive definitions may appear. Terms in types must be total, terms in values may diverge, and the checker distinguishes the two by a modality or by a separate syntactic class. This is the arrangement in systems that separate programs from proofs, and its cost is a duplicative language with two notions of function.

A third option is to accept the checker’s incompleteness and provide an escape hatch: a declaration that a definition terminates, trusted rather than checked. The hatch is useful and it moves the definition into the trusted base, exactly as an axiom does. Agda’s TERMINATING pragma is this escape hatch, and it is unavailable in --safe mode, so a library that promises to stay within safe mode cannot use it. Because the declaration is trusted rather than tracked like an axiom, dependencies on it do not surface in the same way axiom dependencies do in The De Bruijn Criterion; keeping it out of shared libraries is the usual discipline that compensates.

The choice between these options is not a matter of taste. It follows from what the language is for. A proof assistant needs totality in types, and pays the refactoring cost. A general-purpose language needs general recursion, and gives up the logical reading. A system that wants both ends up with two languages and a boundary between them, which is the most honest arrangement and the most work to maintain.