Normal form (abstract rewriting)

In abstract rewriting,^[1] an object is in normal form if it cannot be rewritten any further, i.e. it is irreducible. Depending on the rewriting system, an object may rewrite to several normal forms or none at all. Many properties of rewriting systems relate to normal forms.

Definitions []

Stated formally, if (A,→) is an abstract rewriting system, x∈A is in normal form if no y∈A exists such that x→y, i.e. x is an irreducible term.

An object a is weakly normalizing if there exists at least one particular sequence of rewrites starting from a that eventually yields a normal form. A rewriting system has the weak normalization property or is (weakly) normalizing (WN) if every object is weakly normalizing. An object a is strongly normalizing if every sequence of rewrites starting from a eventually terminates with a normal form. An abstract rewriting system is strongly normalizing, terminating, noetherian, or has the (strong) normalization property (SN), if each of its objects is strongly normalizing.^[2]

A rewriting system has the normal form property (NF) if for all objects a and normal forms b, b can be reached from a by a series of rewrites and inverse rewrites only if a reduces to b. A rewriting system has the unique normal form property (UN) if for all normal forms a, b ∈ S, a can be reached from b by a series of rewrites and inverse rewrites only if a is equal to b. A rewriting system has the unique normal form property with respect to reduction (UN^→) if for every term reducing to normal forms a and b, a is equal to b.^[3]

Results[]

This section presents some well known results. First, SN implies WN.^[4]

Confluence (abbreviated CR) implies NF implies UN implies UN^→.^[3] The reverse implications do not generally hold. {a→b,a→c,c→c,d→c,d→e} is UN^→ but not UN as b=e and b,e are normal forms. {a→b,a→c,b→b} is UN but not NF as b=c, c is a normal form, and b does not reduce to c. {a→b,a→c,b→b,c→c} is NF as there are no normal forms, but not CR as a reduces to b and c, and b,c have no common reduct.

WN and UN^→ imply confluence. Hence CR, NF, UN, and UN^→ coincide if WN holds.^[5]

Examples[]

For example, using the term rewriting system with a single rule g(x,y)→x, the term g(g(4,2),g(3,1)) can be rewritten as follows, applying the rule to the outermost occurrence ^{[note 1]} of g:

g(g(4,2),g(3,1)) → g(4,2) → 4.

Since no rule applies to the last term, 4, it cannot be rewritten any further, and hence is a normal form of the term g(g(4,2),g(3,1)) with respect to this term rewriting system. The rule system is strongly normalizing, since each rule application properly decreases term size and hence there cannot be an infinite rewrite sequence starting from any term. In contrast, the two-rule system { g(x,y) → x, g(x,x) → g(3,x) } is weakly, ^{[note 2]} but not strongly ^{[note 3]} normalizing, although each term not containing g(3,3) is strongly normalizing. ^{[note 4]} The term g(4,4) has two normal forms in this system, viz. g(4,4) → 4 and g(4,4) → g(3,4) → 3, hence the system is not confluent.

Another example: The single-rule system { r(x,y) → r(y,x) } has no normalizing properties (not weakly or strongly), since from any term, e.g. r(4,2) a single rewrite sequence starts, viz. r(4,2) → r(2,4) → r(4,2) → r(2,4) → ..., which is infinitely long.

Untyped lambda calculus[]

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}$ (application is left associative). 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 \ \cdots \,\end{aligned}}}$

Therefore the term ${\displaystyle (\lambda x.xxx)(\lambda x.xxx)}$ is not strongly normalizing. And this is the only reduction sequence, hence it is not weakly normalizing either.

Typed lambda calculus[]

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, otherwise one could solve the halting problem by seeing if the program type-checks. 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), for example a self-interpreter.^[6]

See also[]

• Canonical form
• Typed lambda calculus
• Rewriting
• Total functional programming
• Barendregt–Geuvers–Klop conjecture
• Newman's lemma
• Normalization by evaluation

Notes[]

References[]