Normalization

One way of deciding an equational theory is through normalizing its terms.

Take any equational theory with judgments of the form

\Gamma \vdash M = N : \tau

This judgment states that the terms M and N, which are both of type \tau, are equal. The context \Gamma may contain typing assumptions, e.g. of the form x : \sigma, which are needed to infer that M and N have type \tau. Thus, the terms M and N can be open, i.e. have free variables. This kind of judgment subsumes most type theories, e.g.

• simply-typed \lambda-calculus with \beta\eta-convertibility for the equational theory
• System T
• System F
• Martin-Löf type theory
  and so on.

Given terms \Gamma \vdash M : \tau and \Gamma \vdash N : \tau, we would like an algorithm that decides whether the judgment \Gamma \vdash M = N : \tau is derivable in this equational theory. One way to do so is to normalize the terms of the calculus: we do so by mapping every term to some mathematical object that canonically represents its equivalence class under equality. Deciding whether M is equal to N then amounts to computing whether M and N are mapped to the same representative.

We can capture this axiomatically. Let

\mathsf{Tm}_\tau(\Gamma) = \{ M \mid \Gamma \vdash M : \tau \}

be the set of terms of type \tau in context \Gamma. Moreover, let \mathsf{Nf}_\tau(\Gamma) be an abstract set of "normal forms" in context \Gamma. A normalizer is then a collection of functions

\{\textsf{nf}_{\Gamma, \tau} : \mathsf{Tm}_\tau(\Gamma) \to \mathsf{Nf}_\tau(\Gamma)\}_{\Gamma, \tau}

which map each term \Gamma \vdash M : \tau to a normal form, such that

\Gamma \vdash M = N : \tau\ \Longleftrightarrow \textsf{nf}_{\Gamma, \tau}(M) \equiv \textsf{nf}_{\Gamma, \tau}(N)
\tag{*}

where \equiv refers to syntactic identity (possibly up to \alpha-equivalence).

That is: to decide whether two terms are equal, it suffices to compute their normal forms, and check if they are syntactically identical. This is computable precisely when (a) computing the normal forms, and (b) deciding their equality is.

If the normal forms are a subset of terms, i.e. if \mathfrak{N}_\tau(\Gamma) \subseteq \mathfrak{L}_\tau(\Gamma), the following axioms suffice:

1. Preservation of equational theory. \Gamma \vdash M = N : \tau\ \Longrightarrow \textsf{nf}_{\Gamma, \tau}(M) \equiv \textsf{nf}_{\Gamma, \tau}(N)
2. Equality with normal form. If \Gamma \vdash M : \tau then \Gamma \vdash M = \textsf{nf}_{\Gamma, \tau}(M) : A.
3. Idempotence. If M \in \mathfrak{N}_\tau(\Gamma) then M \equiv\textsf{nf}_{\Gamma, \tau}(M).

We have used \equiv for syntactic equality. These axioms imply (*). The left-to-right implication is simply Axiom 1. From right-to-left: we have the chain of equalities \Gamma \vdash M = \textsf{nf}_{\Gamma, \tau}(M) \equiv \textsf{nf}_{\Gamma, \tau}(N) = N: A by using Axiom 2 twice. Axiom 3 is superfluous, but usually satsfied by well-behaved notions of normal form.

Note, however, that normal forms need not be a subset of terms: complicated type theories may require mathematically complicated notions of normal form.

Canonicity

A type theory satisfies the canonicity property exactly when there are normalization functions at closed terms of ground type.

In terms of the previous definition, we only need a collection of functions

\{\textsf{nf}_b : \mathsf{Tm}_b \to \mathsf{Nf}_b\}_{b}

satisfying (*), where

• b ranges over the ground types of the system, e.g. \textsf{Nat}, \textsf{Bool}, etc.
• \mathsf{Tm}_b = \{ M \mid \cdot\vdash M : b \} is the set of closed terms of ground type b
• \mathsf{Nf}_b usually consists of the normal forms of ground type b

\mathsf{Nf}_b consists of the closed introduction forms of ground type. For example, \mathsf{Nf}_\textsf{Nat} consist of all terms of the form \textsf{succ}^n(\textsf{zero}).

Normalization by Rewriting

Normalization is a property of an abstract rewriting system that every term will eventually be rewritten as an irreducible term, called a normal form.
Strong normalization, or termination requires for all sequences of rewriting will leads to a normal form, and weak normalization only requires one such sequence to exist.

Normalization by Evaluation

Normalization by evaluation refers to a 'semantic' technique for normalizing terms. In short, terms are interpreted in some sort of semantic structure. This structure is chosen cleverly so as to enable the extraction of normal forms from its elements. See the main article for more.

See also

• Canonicity

References

• The normalization axioms given above come from

@inproceedings{fiore_semantic_2002,
	address = {Pittsburgh, PA, USA},
	title = {Semantic analysis of normalisation by evaluation for typed lambda calculus},
	isbn = {978-1-58113-528-2},
	doi = {10.1145/571157.571161},
	language = {en},
	booktitle = {Proceedings of the 4th {ACM} {SIGPLAN} international conference on {Principles} and {Practice} of {Declarative} {Programming} - {PPDP} '02},
	publisher = {ACM Press},
	author = {Fiore, Marcelo},
	year = {2002},
	pages = {26--37}