History
Explicit substitutions grew out of an ‘implementation trick’ used, for example, by AUTOMATH, and became a respectable syntactic theory in lambda calculus and rewriting theory. The idea of a specific calculus where substitutions are part of the object language, and not of the informal meta-theory, is credited to Abadi, Cardelli, Curien, and Levy. Their seminal paper on the λσ calculus explains that implementations of lambda calculus need to be very careful when dealing with substitutions. Without sophisticated mechanisms for structure-sharing, substitutions can cause a size explosion, and therefore, in practice, substitutions are delayed and explicitly recorded. This makes the correspondence between the theory and the implementation highly non-trivial and correctness of implementations can be hard to establish. One solution is to make the substitutions part of the calculus, that is, to have a calculus of explicit substitutions.
Once substitution has been made explicit, however, the basic properties of substitution change from being semantic to syntactic properties. One most important example is the "substitution lemma", which with the notation of λx becomes
- (M〈x:=N〉)〈y:=P〉 = (M〈y:=P〉)〈x:=(N〈y:=P〉)〉 (where x≠y and x not free in P)
A surprising counterexample, due to Melliès, shows that the way this rule is encoded in the original calculus of explicit substitutions is not strongly normalizing. Following this, a multitude of calculi were described trying to offer the best compromise between syntactic properties of explicit substitution calculi.
Read more about this topic: Explicit Substitution
Famous quotes containing the word history:
“A man will not need to study history to find out what is best for his own culture.”
—Henry David Thoreau (1817–1862)
“A poet’s object is not to tell what actually happened but what could or would happen either probably or inevitably.... For this reason poetry is something more scientific and serious than history, because poetry tends to give general truths while history gives particular facts.”
—Aristotle (384–323 B.C.)
“Whenever we read the obscene stories, the voluptuous debaucheries, the cruel and torturous executions, the unrelenting vindictiveness, with which more than half the Bible is filled, it would be more consistent that we called it the word of a demon than the Word of God. It is a history of wickedness that has served to corrupt and brutalize mankind.”
—Thomas Paine (1737–1809)