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:
“The history of literature—take the net result of Tiraboshi, Warton, or Schlegel,—is a sum of a very few ideas, and of very few original tales,—all the rest being variation of these.”
—Ralph Waldo Emerson (1803–1882)
“The true theater of history is therefore the temperate zone.”
—Georg Wilhelm Friedrich Hegel (1770–1831)
“There is one great fact, characteristic of this our nineteenth century, a fact which no party dares deny. On the one hand, there have started into life industrial and scientific forces which no epoch of former human history had ever suspected. On the other hand, there exist symptoms of decay, far surpassing the horrors recorded of the latter times of the Roman empire. In our days everything seems pregnant with its contrary.”
—Karl Marx (1818–1883)