In mathematical logic and theoretical computer science, a rewrite system has the normalization property if every term is strongly normalizing ; that is, if every sequence of rewrites eventually terminates to a term in normal form.

The pure untyped lambda calculus is not strongly normalizing. Consider the term lambda x . x x x. It has the following rewrite rule: For any term t ,

: (mathbf{lambda} x . x x x) t ightarrow t t t

But consider what happens when we apply lambda x . x x x to itself:

Therefore the term (lambda x . x x x) (lambda x . x x x) is not strongly normalizing.

Various systems of the typed lambda calculus including the typed lambda calculus, Jean-Yves Girard s System F, and Thierry Coquand s calculus of constructions have the normalization property.

A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program . That means that there are computable functions that cannot be defined in the simply typed lambda calculus (and similarly there are computable functions that cannot be defined in the calculus of constructions or system F).

=See also=