#jsDisabledContent { display:none; } My Account | Register | Help

# Explicit substitution

Article Id: WHEBN0016874985
Reproduction Date:

 Title: Explicit substitution Author: World Heritage Encyclopedia Language: English Subject: Collection: Publisher: World Heritage Encyclopedia Publication Date:

### Explicit substitution

In computer science, lambda calculi are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution. This is in contrast to the standard lambda calculus where substitutions are performed by beta reductions in an implicit manner which is not expressed within the calculus. The concept of explicit substitutions has become notorious (despite a large number of published calculi of explicit substitutions in the literature with quite different characteristics) because the notion often turns up (implicitly and explicitly) in formal descriptions and implementation of all the mathematical forms of substitution involving variables such as in abstract machines, predicate logic, and symbolic computation.

• Basics 1
• History 2
• References 4

## Basics

A simple example of a lambda calculus with explicit substitution is "λx", which adds one new form of term to the lambda calculus, namely the form M〈x:=N〉, which reads "M where x will be substituted by N". (The meaning of the new term is the same as the common idiom let x:=N in M from many programming languages.) λx can be written with the following rewriting rules:

1. (λx.M) N → M〈x:=N〉
2. x〈x:=N〉 → N
3. x〈y:=N〉 → x (x≠y)
4. (M1M2) 〈x:=N〉 → (M1〈x:=N〉) (M2〈x:=N〉)
5. (λx.M) 〈y:=N〉 → λx.(M〈y:=N〉) (x≠y)

While making substitution explicit, this formulation still retains the complexity of the lambda calculus "variable convention", requiring arbitrary renaming of variables during reduction to ensure that the "(x≠y)" condition on the last rule is always satisfied before applying the rule. Therefore many calculi of explicit substitution avoid variable names altogether by using a so-called "name-free" De Bruijn index notation.

## History

Explicit substitutions were sketched in the preface of Curry's book on Combinatory logic[1] and grew out of an ‘implementation trick’ used, for example, by AUTOMATH, and became a respectable syntactic theory in lambda calculus and rewriting theory. Despite it should actually be credited to de Bruijn,[2] the idea of a specific calculus where substitutions are part of the object language, and not of the informal meta-theory, is traditionally credited to Abadi, Cardelli, Curien, and Levy. Their seminal paper[3] 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,[4] 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.[5][6][7]

## References

1. ^
2. ^ N. G. de Bruijn: A namefree lambda calculus with facilities for internal definition of expressions and segments. Technological University Eindhoven, Netherlands, Department of Mathematics, (1978), (TH-Report), Number 78-WSK-03.
3. ^ M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375–416.
4. ^ P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328–334
5. ^ P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60–69.
6. ^ K. H. Rose, Explicit Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 (ps.gz).
7. ^ Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)
This article was sourced from Creative Commons Attribution-ShareAlike License; additional terms may apply. World Heritage Encyclopedia content is assembled from numerous content providers, Open Access Publishing, and in compliance with The Fair Access to Science and Technology Research Act (FASTR), Wikimedia Foundation, Inc., Public Library of Science, The Encyclopedia of Life, Open Book Publishers (OBP), PubMed, U.S. National Library of Medicine, National Center for Biotechnology Information, U.S. National Library of Medicine, National Institutes of Health (NIH), U.S. Department of Health & Human Services, and USA.gov, which sources content from all federal, state, local, tribal, and territorial government publication portals (.gov, .mil, .edu). Funding for USA.gov and content contributors is made possible from the U.S. Congress, E-Government Act of 2002.

Crowd sourced content that is contributed to World Heritage Encyclopedia is peer reviewed and edited by our editorial staff to ensure quality scholarly research articles.