Explicit substitution
Encyclopedia
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 machine
s, predicate logic
, and symbolic computation
.
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:
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.
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
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.
Computer science
Computer science or computing science is the study of the theoretical foundations of information and computation and of practical techniques for their implementation and application in computer systems...
, lambda calculi
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
are said to have explicit substitutions if they pay special attention to the formalization of the process of substitution
Substitution
Substitution may refer to:- Sciences :* Substitution , a syntactic transformation on strings of symbols of a formal language* Substitution of variables* Substitution cipher, a method of encryption...
. This is in contrast to the standard lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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
Substitution
Substitution may refer to:- Sciences :* Substitution , a syntactic transformation on strings of symbols of a formal language* Substitution of variables* Substitution cipher, a method of encryption...
involving variables such as in abstract machine
Abstract machine
An abstract machine, also called an abstract computer, is a theoretical model of a computer hardware or software system used in automata theory...
s, predicate logic
Predicate logic
In mathematical logic, predicate logic is the generic term for symbolic formal systems like first-order logic, second-order logic, many-sorted logic or infinitary logic. This formal system is distinguished from other systems in that its formulae contain variables which can be quantified...
, and symbolic computation
Symbolic computation
Symbolic computation or algebraic computation, relates to the use of machines, such as computers, to manipulate mathematical equations and expressions in symbolic form, as opposed to manipulating the approximations of specific numerical quantities represented by those symbols...
.
Basics
A simple example of a lambda calculusLambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
with explicit substitution is "λx", which adds one new form of term to the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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
Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
rules:
- (λx.M) N → M⟨x:=N⟩
- x⟨x:=N⟩ → N
- x⟨y:=N⟩ → x (x≠y)
- (M1M2) ⟨x:=N⟩ → (M1⟨x:=N⟩) (M2⟨x:=N⟩)
- (λx.M) ⟨y:=N⟩ → λx.(M⟨y:=N⟩) (x≠y)
While making substitution explicit, this formulation still retains the complexity of the lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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
De Bruijn index
In mathematical logic, the De Bruijn index is a notation invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms in the λ calculus with the purpose of eliminating the names of the variable from the notation. Terms written using these indexes are invariant with respect...
notation.
History
Explicit substitutions grew out of an ‘implementation trick’ used, for example, by AUTOMATH, and became a respectable syntactic theory in lambda calculusLambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped lambda calculus...
and rewriting
Rewriting
In mathematics, computer science, and logic, rewriting covers a wide range of methods of replacing subterms of a formula with other terms. What is considered are rewriting systems...
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
Martín Abadi
Martín Abadi is an argentinian computer scientist, currently working at the University of California, Santa Cruz and Microsoft Research. He earned his Ph.D...
, Cardelli
Luca Cardelli
Luca Cardelli is an Italian computer scientist who is currently an Assistant Director at Microsoft Research in Cambridge, UK. Cardelli is well-known for his research in type theory and operational semantics. Among other contributions he implemented the first compiler for the functional programming...
, Curien, and Levy. Their seminal paper on the λσ calculus explains that implementations of lambda calculus
Lambda calculus
In mathematical logic and computer science, lambda calculus, also written as λ-calculus, is a formal system for function definition, function application and recursion. The portion of lambda calculus relevant to computation is now called the untyped 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⟩)⟩ (x≠y)
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.