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.
Substitution of one canonical form into another does not necessarily produce a canonical result. For example:
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
Whenever we use the notation for LF, we mean hereditary substitution.
- The tutorial on hereditary substitution for the STLC formalizes the hereditary substitution algorithm for a simply typed lambda-calculus in Twelf.
This page is incomplete. We should expand it.