normal form

**natural deduction** metalanguage, practical foundations

**type theory** (dependent, intensional, observational type theory, homotopy type theory)

**computational trinitarianism** = **propositions as types** +**programs as proofs** +**relation type theory/category theory**

**constructive mathematics**, **realizability**, **computability**

propositions as types, proofs as programs, computational trinitarianism

In a rewriting system, a term is said to be of **normal form** if it does not admit any further rewrites.

In type theory, a canonical form is a normal form, but the converse need not hold.

A term is weakly normalizing if there exists at least one particular sequence of rewrites that eventually yields a normal form. A rewrite has weak normalization if every term has this property.

A term is strongly normalizing if every sequence of rewrites eventually terminates with a normal form. If every term has this property, the rewrite system has strong normalization.

In the untyped lambda calculus the term $(\lambda x . x x x) (\lambda x . x x x)$ is neither strongly nor weakly normalizing.

Last revised on June 11, 2018 at 15:44:39. See the history of this page for a list of all contributions to it.