Normalization property (abstract rewriting)

The pure untyped lambda calculus does not satisfy the strong normalization property, and not even the weak normalization property. Consider the term ${\displaystyle \lambda x.xxx}$. It has the following rewrite rule: For any term ${\displaystyle t}$,

${\displaystyle (\mathbf {\lambda } x.xxx)t\rightarrow ttt}$

But consider what happens when we apply ${\displaystyle \lambda x.xxx}$ to itself:

${\displaystyle {\begin{aligned}(\mathbf {\lambda } x.xxx)(\lambda x.xxx)&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow (\mathbf {\lambda } x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)(\lambda x.xxx)\\&\rightarrow \ \ldots \,\end{aligned}}}$

Therefore the term ${\displaystyle (\lambda x.xxx)(\lambda x.xxx)}$ is neither strongly nor weakly normalizing.

Various systems of typed lambda calculus including the simply typed lambda calculus, Jean-Yves Girard's System F, and Thierry Coquand's calculus of constructions are strongly normalizing.

A lambda calculus system with the normalization property can be viewed as a programming language with the property that every program terminates. Although this is a very useful property, it has a drawback: a programming language with the normalization property cannot be Turing complete.[1] 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 computed in the calculus of constructions or System F). As an example, it is impossible to define a self-interpreter in any of the calculi cited above.[2][3][4]