Lambda calculus

The small lambda , the eleventh letter of the Greek alphabet , is used as a symbol for the lambda calculus .

The lambda calculus is a formal language for studying functions . It describes the definition of functions and bound parameters and was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s . Today it is an important construct for theoretical computer science , higher level logic and linguistics .

history

Alonzo Church used the lambda calculus in 1936 to give both a negative answer to the decision problem and to find a foundation for a logical system, such as the Principia Mathematica by Bertrand Russell and Alfred North Whitehead . Using the untyped lambda calculus, it is possible to clearly define what a calculable function is. The question of whether two lambda expressions (see below) are equivalent can generally not be decided algorithmically. In its typified form, the calculus can be used to represent higher level logic. The lambda calculus has significantly influenced the development of functional programming languages , research into type systems of programming languages ​​in general and modern sub-disciplines in logic such as type theory .

The milestones of the development were in detail:

• After the introduction, the early discovery that everything can be expressed with the lambda calculus that can be expressed with a Turing machine . In other words: In terms of the concept of predictability , both are equally powerful.
• Konrad Zuse incorporated ideas from the Lambda calculus from 1942 to 1946 into his plan calculus .
• John McCarthy used them in the late 1950s to define the minimal functions of the Lisp programming language .
• The typified variants of the lambda calculus led to modern programming languages ​​such as ML or Haskell .
• The idea of using expressions of the typified lambda calculus to represent terms of a logic as a basis, i.e. to use the lambda calculus as meta-logic, proved to be extremely fruitful . First presented by Church in 1940 in his Theory of Simple Types , on the one hand it led to modern theorem provers for higher-level logics and ...
• on the other hand, in the 1970s and 1980s, to logics with increasingly powerful type systems, in which e.g. B. logical evidence in itself can be represented as a lambda expression.
• Based on the lambda calculus, the Pi calculus was developed by Robin Milner in the 1990s to describe concurrent processes .

The untyped lambda calculus

motivation

Based on a mathematical expression, for example , can be formed, which is a function on maps. One also writes . The first step in the lambda calculus is to formalize such function formations in terms of language. In the lambda calculus, instead of the term ${\displaystyle x+2}$ ${\displaystyle x}$ ${\displaystyle x+2}$ ${\displaystyle x\mapsto x+2}$ ${\displaystyle x\mapsto x+2}$

• ${\displaystyle \lambda x.x+2}$

write. It is said that the free variable is bound by λ abstraction . The variable link also occurs in mathematics in other areas: ${\displaystyle x}$

• Set theory : ${\displaystyle \{x\mid \Phi (x)\}}$
• Logic : and ${\displaystyle \forall x\;\Phi (x)}$ ${\displaystyle \exists x\;\Phi (x)}$
• Analysis : ${\displaystyle \int _{0}^{1}f(x)\;dx}$

The abstracted variable does not necessarily have to appear in the term, e.g. B. . This λ-expression then referred to the function of each on maps. The function that is constant is a bit more general . If you subsequently abstract, you get a formalization of the function, which assigns the constant function to each value . The expression thus represents a function-valued function. In the lambda calculus, however, functions can also be expressed whose arguments are already functions. If one takes, for example, the function that assigns a different function to each function , which is created in such a way that it is applied twice, the λ term is used to represent and the assignment is shown by . ${\displaystyle \lambda x.2}$ ${\displaystyle x}$ ${\displaystyle 2}$ ${\displaystyle \lambda x.y}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle \lambda y.\lambda x.y}$ ${\displaystyle y}$ ${\displaystyle y}$ ${\displaystyle \lambda y.\lambda x.y}$ ${\displaystyle f}$ ${\displaystyle f^{2}}$ ${\displaystyle f}$ ${\displaystyle f^{2}}$ ${\displaystyle \lambda x.f(f(x))}$ ${\displaystyle f\mapsto f^{2}}$ ${\displaystyle \lambda f.\lambda x.f(f(x))}$

Since λ-terms are seen as functions, they can be applied to an argument. One speaks of application and tends to write instead of in the lambda calculation . Parentheses can group terms. The application as a connection principle of terms is by definition left-associative , i.e. H. means . You would write here in the usual mathematical notation . If you now apply a lambda term to an argument , that is , the result is calculated by replacing every occurrence of the variable in the term with . This derivation rule is called β-conversion . ${\displaystyle f~x}$ ${\displaystyle f(x)}$ ${\displaystyle f~x~y}$ ${\displaystyle (f~x)~y}$ ${\displaystyle (f(x))(y)}$ ${\displaystyle \lambda x.\theta }$ ${\displaystyle a}$ ${\displaystyle (\lambda x.\theta )~a}$ ${\displaystyle \theta }$ ${\displaystyle x}$ ${\displaystyle a}$

λ-terms formulate more general principles of mathematics and do not so much designate objects of the usual mathematical universe. For example, the assignment principle formulates the identical mapping , but this is always related to a given set as a definition set . A universal identity as a function is not defined in the set-theoretical formulation of mathematics. The lambda calculus in the strict sense should therefore be seen more as a new draft of mathematics in which the basic objects are understood as universal functions, in contrast to the axiomatic set theory , whose basic objects are sets. ${\displaystyle \lambda x.x}$

Numbers and terms like are initially not part of a pure lambda calculus. Similar to set theory, in which numbers and arithmetic can be constructed from the concept of sets alone, it is also possible in the lambda calculus to define the arithmetic on the basis of λ abstraction and application. Since every term in the lambda calculus is understood as a one-digit function, an addition must be understood as the function that assigns the (one-digit) function to each number that adds the value to each number (see currying ). ${\displaystyle x+2}$ ${\displaystyle y}$ ${\displaystyle x}$ ${\displaystyle y}$

Lambda terms without free variables are also known as combiners . The combinatorial logic (or combinator calculus) can be seen as an alternative approach to the lambda calculus.

Formal definition

In its simplest, yet complete form, there are three types of terms in the lambda calculus, here in the Backus-Naur form :

Term ::= a (Variable) | (Term Term) (Applikation) | λa. Term (Abstraktion)

where stands for any symbol from an at least countable-infinite set of variable symbols (short: variables). For practical purposes, the lambda calculus is usually extended by another type of term, the constant symbols. ${\displaystyle a}$

The set of free variables can be defined inductively over the structure of a λ-term as follows: ${\displaystyle FV(T)}$ ${\displaystyle T}$

1. ${\displaystyle FV(a)=\{a\}}$If the term is a variable is ${\displaystyle a}$
2. ${\displaystyle FV(T_{1}~T_{2})=FV(T_{1})\cup FV(T_{2})}$ for applications, and
3. ${\displaystyle FV(\lambda a.T)=FV(T)\setminus \{a\}}$if the term is an abstraction, its free variables are the free variables of except . ${\displaystyle T}$ ${\displaystyle a}$

The set of bound variables of a term is also calculated inductively: ${\displaystyle B(T)}$ ${\displaystyle T}$

1. ${\displaystyle B(a)=\emptyset }$If the term is a variable is ${\displaystyle a}$
2. ${\displaystyle B(T_{1}~T_{2})=B(T_{1})\cup B(T_{2})}$ for applications, and
3. ${\displaystyle B(\lambda a.T)=B(T)\cup \{a\}}$if the term is an abstraction, its bound variables are the bound variables of the unified . ${\displaystyle T}$ ${\displaystyle a}$

By defining free and bound variables, the concept of (free) variable substitution (substitution) can now be inductively defined by:

1. ${\displaystyle a[x\leftarrow T]=a}$if variable is not equal ${\displaystyle x}$ ${\displaystyle a}$
2. ${\displaystyle a[a\leftarrow T]=T}$
3. ${\displaystyle (T_{1}~T_{2})[x\leftarrow T]=(T_{1}[x\leftarrow T]~T_{2}[x\leftarrow T])}$
4. ${\displaystyle (\lambda a.T')[a\leftarrow T]=(\lambda a.T')}$
5. ${\displaystyle (\lambda a.T')[x\leftarrow T]=(\lambda a.T'[x\leftarrow T])}$if variable is not equal and if disjoint from . ${\displaystyle x}$ ${\displaystyle a}$ ${\displaystyle FV(T)}$ ${\displaystyle B(\lambda a.T')}$

Note: stands for: in which the free variable has been replaced by (if it does not exist, nothing is replaced). ${\displaystyle S[x\leftarrow T]}$ ${\displaystyle S}$ ${\displaystyle x}$ ${\displaystyle T}$ ${\displaystyle x}$ ${\displaystyle S}$

Note that the substitution is only partially defined; if necessary, bound variables must be renamed appropriately (see α-congruence in the following) so that a free variable is never bound in a substitute by substituting it for a variable.

Congruence rules (written here Kon) can now be defined over the set of λ-terms , which formally grasp the intuition that two expressions describe the same function. These relations are covered by the so-called α-conversion , the β-conversion and the η-conversion .

Congruence rules

α conversion

The α-conversion rule formalizes the idea that the names of bound variables are “smoke and mirrors”; z. B. describe and the same function. However, the details are not quite as simple as they first appear: A number of restrictions must be observed when replacing bound variables with other bound variables. ${\displaystyle \lambda x.x}$ ${\displaystyle \lambda y.y}$

Formally, the rule is as follows:

${\displaystyle \lambda V.E~\equiv ~\lambda W.E[V\leftarrow W]}$

if in free and occurs anywhere in is not bound there, where there is a replaced. Since a rule of congruence applies to every sub-term, it allows the derivation that is equal . ${\displaystyle W}$ ${\displaystyle E}$ ${\displaystyle W}$ ${\displaystyle E}$ ${\displaystyle V}$ ${\displaystyle \lambda x.(\lambda x.x)~x}$ ${\displaystyle \lambda y.(\lambda x.x)~y}$

β conversion

The β-conversion rule formalizes the concept of “function application”. If it is only applied from left to right, it is also called β-reduction. Formally, it lets itself through

${\displaystyle ((\lambda V.E)~E')~\equiv ~E[V\leftarrow E']}$

describe, whereby all free variables in in must remain free (see secondary conditions for the substitution definition). ${\displaystyle E'}$ ${\displaystyle E[V\leftarrow E']}$

A term is called in β-normal form if a β-reduction is no longer applicable (a β-normal form does not exist for all terms; see below ). A profound result from Church and Rosser on the λ-calculus says that the order of α-conversions and β-reductions does not matter in a certain sense: if one derives a term to two terms and , there is always a possibility, and each to derive a common term . ${\displaystyle T_{1}}$ ${\displaystyle T_{2}}$ ${\displaystyle T_{1}}$ ${\displaystyle T_{2}}$ ${\displaystyle T_{3}}$

η conversion

The η-conversion can optionally be added to the calculus. It formalizes the concept of extensionality , i. This means that two functions are equal if and only if they give the same result for all arguments. Formally the η-conversion is described by:

${\displaystyle \lambda x.f~x~\equiv ~f}$if is not a free variable of . ${\displaystyle x}$ ${\displaystyle f}$

Remarks

• A β-normal form does not exist for all terms. For example, you can apply β-reduction to the term , but you get the same term back as the result. ${\displaystyle (\lambda x.x~x)(\lambda x.x~x)}$
• Every term that satisfies the condition of the β-rule is called β-reducible.
• The β-reduction is generally ambiguous; There can be several starting points (so-called β-redexes, from English reducible expression ) for the application of the β-rule, because the rule application is possible in all sub-terms.
• If several sequences of β-reductions are possible and several of them lead to a non-β-reducible term, then these terms are the same except for α-congruence.
• If, however, an order of β leads to a non-β-reducible term (a result), so does the Standard Reduction Order , in which the first lambda in the term is used first.
• In an alternative notation, the variable names are replaced by De Bruijn indices. These indices correspond to the number of lambda terms between the variable and its binding lambda expression. This representation is often used in computer programs because it makes α-conversion obsolete and significantly simplifies β-reduction.

Further examples

• The term is one of many ways of representing the logical function . For this one understands as an abbreviation for and as an abbreviation for . The term fulfills all the requirements that are placed on the function . ${\displaystyle \lambda x.\lambda y.(x~y~\operatorname {falsch} )}$ ${\displaystyle \operatorname {und} }$ ${\displaystyle \operatorname {wahr} }$ ${\displaystyle \lambda x.\lambda y.x}$ ${\displaystyle \operatorname {falsch} }$ ${\displaystyle \lambda x.\lambda y.y}$ ${\displaystyle \operatorname {und} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {wahr} ~\operatorname {wahr} ~{\overset {\mathrm {def} }{\equiv }}~(\lambda x.\lambda y.(x~y~\operatorname {falsch} ))~\operatorname {wahr} ~\operatorname {wahr} ~{\overset {\beta \beta }{\equiv }}~\operatorname {wahr} ~\operatorname {wahr} ~\operatorname {falsch} ~{\overset {\mathrm {def} }{\equiv }}~(\lambda x.\lambda y.x)~\operatorname {wahr} ~\operatorname {falsch} ~{\overset {\beta }{\equiv }}~(\lambda y.\operatorname {wahr} )~\operatorname {falsch} ~{\overset {\beta }{\equiv }}~\operatorname {wahr} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~\operatorname {wahr} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~(\lambda y.\operatorname {falsch} )~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {falsch} ~\operatorname {wahr} ~\equiv ~\operatorname {falsch} ~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~(\lambda x.\lambda y.y)~\operatorname {wahr} ~\operatorname {falsch} ~\equiv ~(\lambda y.y)~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
  • ${\displaystyle \operatorname {und} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\operatorname {falsch} ~\operatorname {falsch} ~\operatorname {falsch} ~\equiv ~\ldots ~\equiv ~(\lambda y.y)~\operatorname {falsch} ~\equiv ~\operatorname {falsch} }$
• Numbers, tuples and lists can be coded in a similar way in λ-expressions (e.g. using so-called Church numerals )
• Any recursive functions can be represented by the fixed point combiner . ${\displaystyle \mathbf {Y} =\lambda g.(\lambda x.g~(x~x))(\lambda x.g~(x~x))}$

Typed lambda calculus

The central idea of ​​the typed lambda calculus is to only consider lambda expressions to which a type can be assigned using a system of type inference rules. The simplest type system, which was presented by Church in 1940 in his Theory of Simple Types , provides for the types that are generated by the following grammar in Backus-Naur form :

TT ::= I (Individuen) | O (Wahrheitswerte) | (TT → TT) (Funktionstypen)

The type can be thought of as numbers, is used for Boolean values ​​such as True and False . ${\displaystyle I}$ ${\displaystyle O}$

In addition, an environment is defined; this is a function that maps variable symbols to types . ${\displaystyle \Gamma }$ ${\displaystyle TT}$

A triple from an environment , an expression and a type written a will type judgment called. ${\displaystyle \Gamma }$ ${\displaystyle E}$ ${\displaystyle T}$ ${\displaystyle \Gamma \vdash E:T}$

Now the inference rules can establish relationships between expressions, their types and type judgments:

${\displaystyle {{} \over \Gamma \vdash v:\Gamma (v)}\qquad {\rm {(Variable)}}}$

${\displaystyle {\Gamma \vdash t_{1}:(\tau _{1}\rightarrow \tau _{2})\quad \Gamma \vdash t_{2}:\tau _{1} \over \Gamma \vdash (t_{1}~t_{2}):\tau _{2}}\qquad ({\rm {Applikation)}}}$

${\displaystyle {\Gamma [a\mapsto \tau _{1}]\vdash t:\tau _{2} \over \Gamma \vdash \lambda a.t:\tau _{1}\rightarrow \tau _{2}}\qquad ({\rm {Abstraktion)}}}$

Here is the function that assigns the type at the point and is otherwise the function . (In other words: the parameter of the function is of the type and it is precisely this information that is added to the environment.) ${\displaystyle \Gamma [a\mapsto \tau _{1}]}$ ${\displaystyle a}$ ${\displaystyle \tau _{1}}$ ${\displaystyle \Gamma }$ ${\displaystyle a}$ ${\displaystyle \tau _{1}}$

By introducing a second environment, constant symbols can also be handled; Another important extension is to allow the category of type variables etc. or type constructors such as , etc. in types : this creates very powerful functional or logical core languages. is, for example, a function that maps any type to the type “set, whose elements are of type ”; analogous; written and , whereby the brackets may be missing as usual. The concept can easily be abstracted further by using a variable instead of a concrete type constructor, e.g. B. . Type constructors can generally have several arguments, such as the arrow: The type is nothing other than , but better shows that the arrow is a type constructor in two variables. In particular, currying is also possible with type constructors and is a type constructor in a variable. ${\displaystyle \alpha ,\beta ,\gamma }$ ${\displaystyle \operatorname {Menge} }$ ${\displaystyle \operatorname {Liste} }$ ${\displaystyle \operatorname {Menge} }$ ${\displaystyle \alpha }$ ${\displaystyle \alpha }$ ${\displaystyle \operatorname {Liste} }$ ${\displaystyle \operatorname {Menge} (\alpha )}$ ${\displaystyle \operatorname {Liste} (\beta )}$ ${\displaystyle \Phi (\alpha )}$ ${\displaystyle \operatorname {Pfeil} \;\alpha \;\beta }$ ${\displaystyle \alpha \rightarrow \beta }$ ${\displaystyle \operatorname {Pfeil} \;\alpha }$

It can be decided whether an untyped term can be typed, even if the environment is unknown (a variant with type variables and type constructors is the Hindley-Milner algorithm ). ${\displaystyle \Gamma }$

The set of typable expressions is a real subset of the untyped lambda calculus; z. B. the Y-combiner cannot be typed. On the other hand, for typed expressions the equality between two functions modulo α- and β-conversions can be decided. It is known that the matching problem is decidable on lambda expressions up to the fourth order. The unification problem is undecidable; however, there are practically useful approximate algorithms.

Application in semantics

Semantics is the branch of linguistics that analyzes the meaning of natural language expressions. For this purpose, formal semantics initially uses simple means of predicate logic and set theory. These are expanded to include the fundamentals of the lambda calculus, for example to represent propositions as properties using lambda abstraction and to be able to represent more complex noun phrases, adjective phrases and some verb phrases. The basis is, for example, a model-theoretical semantic interpretation of Richard Montague's intensional logic .

Application in computer science

The lambda calculus is also the formal basis for many programming languages, such as B. Scheme or Lisp . Some programming languages ​​offer concepts such as anonymous functions to which some of the rules of the lambda calculus apply. However, the programming languages ​​usually allow more than the pure lambda calculation such as side effects .

See also

• Computability theory
• Combinatorial Logic

literature

• Stephen Kleene : A theory of positive integers in formal logic. In: American Journal of Mathematics. 57, 1935, ISSN  0002-9327 , pp. 153-173 and 219-244.
• Alonzo Church : An unsolvable problem of elementary number theory. In: American Journal of Mathematics. 58, 1936, pp. 345-363.
• Alonzo Church : The Calculi of Lambda Conversion
• Henk P. Barendregt: The lambda calculus. Its syntax and semantics. Revised edition. North Holland, Amsterdam a. a. 1984, ISBN 0-444-87508-5 ( Studies in logic and the foundations of mathematics 103).
• Guo-Qiang Zhang: Logic of Domains. Birkhäuser, Boston a. a. 1991, ISBN 0-8176-3570-X ( Progress in theoretical computer science 4), (Also: Cambridge, Univ., Diss., 1989).
• Roberto M. Amadio, Pierre-Louis Curien: Domains and Lambda-Calculi. Cambridge University Press, Cambridge u. a. 1998, ISBN 0-521-62277-8 ( Cambridge tracts in theoretical computer science 46).
• Samson Abramsky (Ed.): Typed Lambda Calculi and Applications. 5th international conference, Kraków, Poland, May 2 - 5, 2001. Proceedings. Springer, Berlin a. a. 2001, ISBN 3-540-41960-8 ( Lecture notes in computer science 2044).

Web links

• Klaus Aehlig, Thomas Fischbacher: Introduction to the λ-calculus. Lecture notes (103 pages, PS document).
• Fabian Nilius: The dreaded lambda calculation. Presentation slides (58 slides as PS document).
• Bret Victor: Alligator Eggs! An introduction to the working of the λ-calculus disguised as a colorful game (from 8 years).
• Jim Larson: An Introduction to Lambda Calculus and Scheme. ( Memento of July 13, 2015 in the Internet Archive ) A simple introduction for programmers.
• Jesse Alama:  The Lambda Calculus. In: Edward N. Zalta (Ed.): Stanford Encyclopedia of Philosophy .
• Shane Steinert-Threlkeld:  Lambda Calculi. In: Internet Encyclopedia of Philosophy .

Individual evidence

1. ^ Church: The Calculi of Lambda Conversion . Princeton University Press, Princeton 1941 (Retrieved April 14, 2020).