Normal form

This article does not cite any references or sources. Please help improve this article by adding citations to reliable sources. Unsourced material may be challenged and removed. (August 2009)

This article may require cleanup to meet Wikipedia's quality standards. Please improve this article if you can. (August 2009)

In considering rewriting systems, a normal form is an element of the system which cannot be rewritten any further.

Consider the basic term rewriting system with reduction rule ρ : g(x, y) → x. The term g(g(4, 2), g(3, 1)) has the following reduction sequence, according to the usual outermost strategy, that is, if the reduction rule is applied to each outermost occurrence of g:

There is no rule that permits us to rewrite 4, so 4 is a normal form for this term rewriting system.

Related concepts are related to the possibility of rewriting an element into normal form. Weak normalization is defined as the possibility that some element can be rewritten into a normal form. Strong normalization is defined as any reduction sequence starting from some element terminates. We say that the system is weakly normalizing (or strongly normalizing) if all elements are weakly normalizing (resp. strongly normalizing).

Newman's lemma states that if an abstract reduction system A is strongly normalizing and is weakly confluent, then A is in fact confluent. The result enables us to further generalize the critical pair lemma.

This mathematical logic-related article is a stub. You can help Wikipedia by expanding it. v • d • e