Explicit substitution

Explicit substitution

In computer science, Explicit substitution is an umbrella term used to describe several calculi based on the Lambda calculus that pay special attention to the formalization of the process of substitution. The concept of explicit substitutions has become notorious not just because of a large number of published calculi of explicit substitutions in the literature with quite different characteristics but also 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

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:
# (λ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⟨x:=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 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 [M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375-416.] 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⟩)⟩ (x≠y)A surprising counterexample, due to Melliès, [P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328-334] 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. [P. Lescanne, From λσ to λν:a journey through calculi of explicit substitutions, POPL 1994, pp. 60-69.] [K. H. Rose, Explicit Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 ( [http://www.brics.dk/LS/96/3/BRICS-LS-96-3.ps.gz ps.gz] ).]

See also

* Substitution instance

References

----


Wikimedia Foundation. 2010.

Игры ⚽ Нужно решить контрольную?

Look at other dictionaries:

  • Substitution matrix — In evolutionary biology, a substitution matrix describes the rate at which one character in a sequence changes to other character states over time. Substitution matrices are usually seen in the context of amino acid or DNA sequence alignments,… …   Wikipedia

  • import substitution —   the establishment and/or explicit government support for an industry producing goods that were formally exclusively, or nearly exclusively, imported. Usually used in the ELDW to try and add value to domestic raw materials and reduce the flow of …   Geography glossary

  • Lambda calculus — In mathematical logic and computer science, lambda calculus, also written as λ calculus, is a formal system designed to investigate function definition, function application and recursion. It was introduced by Alonzo Church and Stephen Cole… …   Wikipedia

  • Multiple sequence alignment — A multiple sequence alignment (MSA) is a sequence alignment of three or more biological sequences, generally protein, DNA, or RNA. In many cases, the input set of query sequences are assumed to have an evolutionary relationship by which they… …   Wikipedia

  • Unification (computer science) — Unification, in computer science and logic, is an algorithmic process by which one attempts to solve the satisfiability problem. The goal of unification is to find a substitution which demonstrates that two seemingly different terms are in fact… …   Wikipedia

  • Director string — In mathematics, in the area of lambda calculus and computation, directors or director strings are a mechanism for keeping track of the free variables in a term. Director strings were introduced by Kennaway and Sleep in 1982 and further developed… …   Wikipedia

  • Automath theorem prover — Automath (automating mathematics) is a formal language, devised by Nicolaas Govert de Bruijn starting in 1967, for expressing complete mathematical theories in such a way that an included automated proof checker can verify the correctness. The… …   Wikipedia

  • De Bruijn notation — For the representation of variables with natural numbers, see De Bruijn index. In mathematical logic, the De Bruijn notation is a syntax for terms in the λ calculus invented by the Dutch mathematician Nicolaas Govert de Bruijn.[1] It can be seen… …   Wikipedia

  • Categorical abstract machine — (CAM) is the model of computation of a program [ Cousineau G., Curien P. L., Mauny M. The categorical abstract machine. LNCS, 201, Functional programming languages computer architecture. 1985, pp. 50 64.] , which preserves the abilities of… …   Wikipedia

  • Natural deduction — In logic and proof theory, natural deduction is a kind of proof calculus in which logical reasoning is expressed by inference rules closely related to the natural way of reasoning. This contrasts with the axiomatic systems which instead use… …   Wikipedia

Share the article and excerpts

Direct link
Do a right-click on the link above
and select “Copy Link”