Explicit substitution

Last updated

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 "freshness" conditions in such implicit calculi are a notorious source of errors. [1] The concept has appeared in a large number of published papers in quite different fields, such as in abstract machines, predicate logic, and symbolic computation.

Contents

Overview

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 and x not free in N)

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 and x not free in N)" 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 [2] and grew out of an ‘implementation trick’ used, for example, by AUTOMATH, and became a respectable syntactic theory in lambda calculus and rewriting theory. Though it actually originated with de Bruijn, [3] 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 Lévy. Their seminal paper [4] 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, [5] 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. [6] [7] [8]

See also

Related Research Articles

Lambda calculus is a formal system in mathematical logic for expressing computation based on function abstraction and application using variable binding and substitution. It is a universal model of computation that can be used to simulate any Turing machine. It was introduced by the mathematician Alonzo Church in the 1930s as part of his research into the foundations of mathematics.

In mathematics, logic, and computer science, a type theory is the formal presentation of a specific type system, and in general type theory is the academic study of type systems. Some type theories serve as alternatives to set theory as a foundation of mathematics. Two influential type theories that were proposed as foundations are Alonzo Church's typed λ-calculus and Per Martin-Löf's intuitionistic type theory. Most computerized proof-writing systems use a type theory for their foundation. A common one is Thierry Coquand's Calculus of Inductive Constructions.

In logic and computer science, unification is an algorithmic process of solving equations between symbolic expressions.

In mathematics, and in other disciplines involving formal languages, including mathematical logic and computer science, a free variable is a notation (symbol) that specifies places in an expression where substitution may take place and is not a parameter of this or any container expression. Some older books use the terms real variable and apparent variable for free variable and bound variable, respectively. The idea is related to a placeholder, or a wildcard character that stands for an unspecified symbol.

Combinatory logic is a notation to eliminate the need for quantified variables in mathematical logic. It was introduced by Moses Schönfinkel and Haskell Curry, and has more recently been used in computer science as a theoretical model of computation and also as a basis for the design of functional programming languages. It is based on combinators, which were introduced by Schönfinkel in 1920 with the idea of providing an analogous way to build up functions—and to remove any mention of variables—particularly in predicate logic. A combinator is a higher-order function that uses only function application and earlier defined combinators to define a result from its arguments.

In mathematics and computer science in general, a fixed point of a function is a value that is mapped to itself by the function.

Curry's paradox is a paradox in which an arbitrary claim F is proved from the mere existence of a sentence C that says of itself "If C, then F", requiring only a few apparently innocuous logical deduction rules. Since F is arbitrary, any logic having these rules allows one to prove everything. The paradox may be expressed in natural language and in various logics, including certain forms of set theory, lambda calculus, and combinatory logic.

In programming language theory and proof theory, the Curry–Howard correspondence is the direct relationship between computer programs and mathematical proofs.

Categorial grammar is a family of formalisms in natural language syntax that share the central assumption that syntactic constituents combine as functions and arguments. Categorial grammar posits a close relationship between the syntax and semantic composition, since it typically treats syntactic categories as corresponding to semantic types. Categorial grammars were developed in the 1930s by Kazimierz Ajdukiewicz and in the 1950s by Yehoshua Bar-Hillel and Joachim Lambek. It saw a surge of interest in the 1970s following the work of Richard Montague, whose Montague grammar assumed a similar view of syntax. It continues to be a major paradigm, particularly within formal semantics.

The SKI combinator calculus is a combinatory logic system and a computational system. It can be thought of as a computer programming language, though it is not convenient for writing software. Instead, it is important in the mathematical theory of algorithms because it is an extremely simple Turing complete language. It can be likened to a reduced version of the untyped lambda calculus. It was introduced by Moses Schönfinkel and Haskell Curry.

In mathematical logic, the De Bruijn index is a tool invented by the Dutch mathematician Nicolaas Govert de Bruijn for representing terms of lambda calculus without naming the bound variables. Terms written using these indices are invariant with respect to α-conversion, so the check for α-equivalence is the same as that for syntactic equality. Each De Bruijn index is a natural number that represents an occurrence of a variable in a λ-term, and denotes the number of binders that are in scope between that occurrence and its corresponding binder. The following are some examples:

In mathematical logic, the De Bruijn notation is a syntax for terms in the λ calculus invented by the Dutch mathematician Nicolaas Govert de Bruijn. It can be seen as a reversal of the usual syntax for the λ calculus where the argument in an application is placed next to its corresponding binder in the function instead of after the latter's body.

In programming language semantics, normalisation by evaluation (NBE) is a style of obtaining the normal form of terms in the λ-calculus by appealing to their denotational semantics. A term is first interpreted into a denotational model of the λ-term structure, and then a canonical (β-normal and η-long) representative is extracted by reifying the denotation. Such an essentially semantic, reduction-free, approach differs from the more traditional syntactic, reduction-based, description of normalisation as reductions in a term rewrite system where β-reductions are allowed deep inside λ-terms.

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. Loosely speaking, they can be understood as a kind of memoization for free variables; that is, as an optimization technique for rapidly locating the free variables in a term algebra or in a lambda expression. Director strings were introduced by Kennaway and Sleep in 1982 and further developed by Sinot, Fernández and Mackie as a mechanism for understanding and controlling the computational complexity cost of beta reduction.

The categorical abstract machine (CAM) is a model of computation for programs that preserves the abilities of applicative, functional, or compositional style. It is based on the techniques of applicative computing.

In the study of denotational semantics of the lambda calculus, Böhm trees, Lévy-Longo trees, and Berarducci trees are tree-like mathematical objects that capture the "meaning" of a term up to some set of "meaningless" terms.

A Hindley–Milner (HM) type system is a classical type system for the lambda calculus with parametric polymorphism. It is also known as Damas–Milner or Damas–Hindley–Milner. It was first described by J. Roger Hindley and later rediscovered by Robin Milner. Luis Damas contributed a close formal analysis and proof of the method in his PhD thesis.

Computable topology is a discipline in mathematics that studies the topological and algebraic structure of computation. Computable topology is not to be confused with algorithmic or computational topology, which studies the application of computation to topology.

In rewriting, a reduction strategy or rewriting strategy is a relation specifying a rewrite for each object or term, compatible with a given reduction relation. Some authors use the term to refer to an evaluation strategy.

<span class="mw-page-title-main">Krivine machine</span> Abstract machine

In theoretical computer science, the Krivine machine is an abstract machine. As an abstract machine, it shares features with Turing machines and the SECD machine. The Krivine machine explains how to compute a recursive function. More specifically it aims to define rigorously head normal form reduction of a lambda term using call-by-name reduction. Thanks to its formalism, it tells in details how a kind of reduction works and sets the theoretical foundation of the operational semantics of functional programming languages. On the other hand, Krivine machine implements call-by-name because it evaluates the body of a β-redex before it applies the body to its parameter. In other words, in an expression u it evaluates first λx. t before applying it to u. In functional programming, this would mean that in order to evaluate a function applied to a parameter, it evaluates first the function before applying it to the parameter.

References

  1. ↑ Clouston, Ranald; Bizjak, Aleš; Grathwohl, Hans; Birkedal, Lars (27 April 2017). "The Guarded Lambda-Calculus: Programming and Reasoning with Guarded Recursion for Coinductive Types". Logical Methods in Computer Science. 12 (3): 36. arXiv: 1606.09455 . doi:10.2168/LMCS-12(3:7)2016.
  2. ↑ Curry, Haskell; Feys, Robert (1958). Combinatory Logic Volume I. Amsterdam: North-Holland Publishing Company.
  3. ↑ 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.
  4. ↑ M. Abadi, L. Cardelli, P-L. Curien and J-J. Levy, Explicit Substitutions, Journal of Functional Programming 1, 4 (October 1991), 375–416.
  5. ↑ P-A. Melliès: Typed lambda-calculi with explicit substitutions may not terminate. TLCA 1995: 328–334
  6. ↑ P. Lescanne, From λσ to λυ: a journey through calculi of explicit substitutions, POPL 1994, pp. 60–69.
  7. ↑ K. H. Rose, Explicit Substitution – Tutorial & Survey, BRICS LS-96-3, September 1996 (ps.gz).
  8. ↑ Delia Kesner: A Theory of Explicit Substitutions with Safe and Full Composition. Logical Methods in Computer Science 5(3) (2009)
This page is based on this Wikipedia article
Text is available under the CC BY-SA 4.0 license; additional terms may apply.
Images, videos and audio are available under their respective licenses.