Normalisation by Evaluation for Conversion Checking

A type checker for a dependent type theory must decide when two terms are definitionally equal, and the standard way to do that is to reduce both to normal form and compare. The straightforward implementation substitutes the body of a function for its variable on every application, and that operation copies the body and every argument passed into it. Under nested binders the copying compounds: each level repeats the work of the level below, and the checker’s cost grows faster than the size of the term it is checking. Normalisation by evaluation takes a different route: it evaluates terms into a semantic domain, reads back, and compares.

The problem with repeated substitution

Take a term with nested applications under binders, such as a Church numeral applied to a function. Reducing (λf. λx. f (f (f x))) g by substitution produces λx. g (g (g x)), which is fine. If the result is then passed to a function that duplicates and applies it again, as in (λh. h (h z)) ((λf. λx. f (f (f x))) g), the argument is copied at each use and each copy has to be normalised again, so the work multiplies with the nesting depth. When the argument is itself a term containing a binder, the copy duplicates the binder and the names inside it must be renamed to avoid capture.

The copying is not the only cost. Name-based substitution requires freshness checks: when a variable is substituted under a binder that binds the same name, the bound occurrences must be renamed. A naive implementation scans the body to find free occurrences, and the scan is repeated at each level, giving a cost that grows with the product of term depth and substitution count. De Bruijn indices remove the freshness problem by making binders anonymous and positions explicit, at the price of shifting indices when terms move under binders. The shifting operation is itself a traversal.

Neither approach is asymptotically comfortable, and both are hard to get right. The classical alternative is to avoid substitution entirely and work with environments.

Evaluate into a semantic domain

Normalisation by evaluation separates two operations that substitution conflates: computing the value of a term, and displaying that value as syntax.

The evaluator maps a term and an environment to a value. Values are not syntax; they are elements of a domain chosen so that functions can be represented as metalanguage functions. A lambda abstraction evaluates to a closure: a pair of the unevaluated body and the environment it was closed over. An application evaluates the function position to a closure, applies the metalanguage function to the evaluated argument, and continues. A free variable evaluates by lookup in the environment.

Because the domain contains metalanguage functions, the evaluator can apply a function to an argument without ever inspecting or copying its body. The body is evaluated only when the closure is applied, and the argument is passed as a value rather than as a syntactic term to be substituted.

The second operation is readback, which turns a value back into syntax. Readback on a closure must produce a lambda abstraction, so it invents a fresh variable, applies the closure’s function to the value corresponding to that variable, and reads back the result. Readback on a neutral value reconstructs the corresponding application or variable.

Normalisation is then evaluate followed by readback, and equality is comparison of the two readback results. The round trip through the domain is where the work is saved: the domain holds functions, so the evaluator never needs to duplicate syntax.

Neutral values and stuck terms

The domain needs a third kind of element. A term such as x y, where x is a free variable, cannot reduce: no rule applies because x is not a lambda. Such a term is neutral, and it must be represented as such rather than as a closure.

A neutral value is a head variable together with a spine of eliminations, each elimination being an application argument or a projection. Evaluation of a neutral function applied to an argument extends the spine rather than reducing. Readback of a neutral reconstructs the syntax of the head applied to the readback of each spine element.

The distinction between a closure and a neutral is what makes the algorithm correct for open terms. During conversion checking under a binder, the checker must compare bodies that mention a variable which is not yet known. The variable is represented as a neutral, and two bodies that manipulate it in the same way will read back to the same syntax. Two bodies that differ will read back differently, and the checker reports a mismatch rather than looping.

Conversion checking under binders

Checking that two types are equal proceeds by evaluating both in the current environment and comparing the resulting values. Comparison is structural and proceeds by type: two closures are compared by applying both to a fresh neutral variable and comparing the results; two neutrals are compared by comparing heads and spines; two constructors are compared by comparing their arguments.

The fresh-variable step is the essential trick. Instead of comparing the syntax of two function bodies, the checker applies both functions to a variable that stands for an arbitrary input and compares the outputs. If the outputs agree for a symbolic input, the functions agree for all inputs, because the comparison is performed in a context where nothing is known about the variable. This is eta-expansion for functions, performed lazily and only when needed.

A subtlety arises with types that are not functions. Comparing two values of a base type reduces to comparing their readback syntax, and that comparison is syntactic. Two neutral terms with the same head and the same spine arguments are equal; anything else is not. This is why the definitional equality of a type theory is a syntactic relation after normalisation, even though the algorithm that decides it is semantic.

Cost

The algorithm evaluates each term once. Closures share their environments, so an argument passed to several applications is not copied. Under the standard representation the evaluator runs in time proportional to the size of the term, and readback in time proportional to the size of the normal form, which can be exponentially larger than the original if the term contains heavy sharing. The blow-up is inherent to normal forms rather than to the algorithm, and it is the same phenomenon that makes cut-free proofs large.

Practical checkers do not normalise whole terms eagerly. They compare lazily, forcing evaluation only where the two values differ in constructor, and they cache evaluation results for subterms that are compared repeatedly. The combination keeps the common case cheap, where two types differ at the outermost constructor and the comparison fails without either being evaluated further.

The algorithm is often called normalisation by evaluation. It also has to handle definitions. A defined constant is evaluated by unfolding its body in an environment that binds its parameters, and the unfolding is recorded so that it is not repeated. Recursive definitions cannot be unfolded eagerly, since the unfolding does not terminate; they are unfolded only when the recursion is structurally decreasing on a constructor, which is why totality checking and conversion checking are implemented together rather than separately.

Where the approach breaks

Three limitations recur.

Non-terminating terms. If the language permits general recursion, evaluation of a term in a type may not terminate, and the checker hangs. Systems either restrict what may appear in types, or run evaluation under a step limit and treat exceeding it as a non-equal result, which makes type checking depend on an arbitrary bound.

Impredicative universes. In a system with a type of all types, the semantic domain cannot be constructed in the metalanguage without a corresponding impredicative construction. Implementations work around this by treating the universe as a special case and by restricting what can be computed at universe level, but the theoretical justification is less direct than for predicative systems.

Effects and exceptions. The domain must represent every value the language can produce. A language with exceptions needs a neutral or error element, and a language with mutable state needs the domain to be a monad or to be indexed by a store. Each addition complicates the readback function and the proof that readback of evaluate is the identity on normal forms.

Why the algorithm is the specification

The equality relation a type checker implements is not an abstract relation with many possible algorithms. It is the relation induced by a particular evaluation strategy, and different strategies give different answers for terms that are not strongly normalising. Publishing the algorithm is therefore part of publishing the language. A user who wants to know whether a program typechecks is asking about a specific operational behaviour, not about a mathematical ideal.

That is also why systems differ on whether eta-equality holds, whether definitions unfold in types, and whether proofs are compared by structure or by irrelevance. Each choice changes the set of programs that typecheck, and the algorithm’s cost is only one of the considerations. The dominant one is predictability: a checker whose answer a programmer can forecast from the definition of the program is more useful than a faster one whose answer depends on evaluation order. Where the boundary between computed and proved equality is drawn is the subject of Definitional and Propositional Equality, and the way an unsolved metavariable surfaces as a failure to convert is what Elaboration has to explain to the programmer.