Hereditary substitution

From The Twelf Project
Jump to: navigation, search

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.

This article or section needs citations of said type theories..

Example

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.

This article or section needs an explanation of the hereditary substitution algorithm and its metatheory..

See also


This page is incomplete. We should expand it.