Normal forms and neutral terms

When working with or studying simply-typed \lambda-calculi we often wish to normalize their terms, usually in order to compute or decide some equational theory on terms. The objects which are the target of normalization are called normal forms.

The structure of normal forms depends on the particular theory. For example, for the theory of the simply-typed \lambda-calculus under \beta-equality, the normal forms must not contain any redexes, i.e. reducible expressions of the form (\lambda x. M)N.

However, for many subtle semantic purposes - such as normalization by evaluation - a finer analysis of normal forms is required. This leads to identifying a subset of normal forms, the so-called neutral terms. This leads to an inductive characterisation of normal forms.

Intuitively, neutral terms contain a free variable at a 'head' position. Thus, they cannot be reduced any further without instantiating that variable. For example, the term xN where N is a normal form is a neutral term: it cannot be reduced unless we instantiate x with a \lambda-abstraction.

In simply-typed \lambda-calculus

In simply-typed \lambda-calculus with only function types, the neutral terms and the normal forms are generated in a mutually inductive manner by the following rules.

\frac{
}{
	\Gamma, x : A, \Gamma' \vdash_{\textsf{ne}} x : A
}
\quad
\frac{
	\Gamma \vdash_{\textsf{ne}} M : A
}{
	\Gamma \vdash_{\textsf{nf}} M : A
}

\quad
\frac{
	\Gamma, x : A \vdash_{\textsf{nf}} M : B
}{
	\Gamma \vdash_{\textsf{nf}} \lambda x. M : A \to B
}
\quad
\frac{
	\Gamma \vdash_{\textsf{ne}} M : A \to B
  \quad
  \Gamma \vdash_{\textsf{nf}} N : A
}{
  \Gamma \vdash_{\textsf{ne}} MN : B
}

Proof-theoretically

Proof-theoretically, the neutral terms are the terms obtained by a series of elimination rules from some assumption, but where every other proof involved in normal.

This characterisation implicitly comes up in the original treatment of natural deduction by Prawitz, where normal forms are characterised as proceeding from assumptions through a series of eliminations, and then followed by introductions.

Relationship to polarization and bidirectional systems

Please expand.

Girard's neutral terms

The notion of neutrality here is very common in programming languages. It should not be confused with Girard's notion of neutrality, which is used in strong normalization proofs using reducibility candidates.

Girard's concept - which can broadly be described as "not an introduction form" - shares the property that substitution of a neutral for a variable does not create a redex.

See Proofs and Types, §6.2, for an occurrence of this concept in Girard's writings.

References

• The notion of neutral terms seems to originate in §3.3 of

@inproceedings{altenkirch_1995,
	address = {Berlin, Heidelberg},
	series = {Lecture {Notes} in {Computer} {Science}},
	title = {Categorical reconstruction of a reduction free normalization proof},
	volume = {953},
	doi = {10.1007/3-540-60164-3_27},
	booktitle = {Category {Theory} and {Computer} {Science}},
	publisher = {Springer Berlin Heidelberg},
	author = {Altenkirch, Thorsten and Hofmann, Martin and Streicher, Thomas},
	editor = {Pitt, David and Rydeheard, David E. and Johnstone, Peter},
	year = {1995},
	pages = {182--199}
}