Hereditary substitution

LF is defined so that only canonical forms exist. However, canonical forms are not closed under substitution. Hereditary substitution is an algorithm that directly computes the canonical result of an ordinary substiution of one canonical form into another. This algorithm has been applied in several additional type theories as well.

Example

Substitution $\mathsf{}[M'/x]M$ of one canonical form into another does not necessarily produce a canonical result. For example:

$\mathsf{}[\lambda y.y/x](x \; z) \; = \;(\lambda y.y) \; z$

Even though both terms are canonical forms, the result is beta-reducible.

However, hereditary substitution directly computes the canonical result of an ordinary substitution. When ordinary substitution would return a non-canonical form, hereditary substitution continues to reduce by substituting the argument into the body of the function. In the above example, the hereditary substitution

$\mathsf{}[\lambda y.y/x](x \; z) \; = \; [z/y] y \; = \; z$

Whenever we use the notation $\mathsf{}[M'/x]M$ for LF, we mean hereditary substitution.

See also

• The tutorial on hereditary substitution for the STLC formalizes the hereditary substitution algorithm for a simply typed lambda-calculus in STELF.