Namespaces
Variants
Actions

Difference between revisions of "Lambda-calculus"

From Encyclopedia of Mathematics
Jump to: navigation, search
(Importing text file)
 
m (AUTOMATIC EDIT (latexlist): Replaced 3 formulas out of 3 by TEX code with an average confidence of 2.0 and a minimal confidence of 2.0.)
 
(4 intermediate revisions by 3 users not shown)
Line 1: Line 1:
 +
<!--This article has been texified automatically. Since there was no Nroff source code for this article,
 +
the semi-automatic procedure described at https://encyclopediaofmath.org/wiki/User:Maximilian_Janisch/latexlist
 +
was used.
 +
If the TeX and formula formatting is correct, please remove this message and the {{TEX|semi-auto}} category.
 +
 +
Out of 3 formulas, 3 were replaced by TEX code.-->
 +
 +
{{TEX|semi-auto}}{{TEX|done}}
 +
{{TEX|auto}}
 +
{{TEX|done}}
 +
 
''lambda calculus.''
 
''lambda calculus.''
  
 
==Introduction.==
 
==Introduction.==
The lambda calculus was introduced in 1932–1933 by A. Church
+
The lambda calculus was introduced in 1932–1933 by A. Church (1903-1995) as part of a theory intended as a foundation for mathematics. This foundational theory consisted of a part dealing with logical symbols and rules and a part dealing with algorithms operating on these symbols. After it was shown by S.C. Kleene and J.B. Rosser [[#References|[a7]]] that this foundational system was inconsistent, the part dealing with algorithms only was isolated as the (type-free) lambda calculus. It turned out to be quite successful in capturing the intuitive notion of [[computable function]]. Kleene [[#References|[a6]]] showed that exactly the recursive functions (cf. [[Recursive function]]) are lambda definable in the sense given below. Then A.M. Turing [[#References|[a10]]] introduced his machines (cf. [[Turing machine]]) and showed that Turing computable and lambda definable are equivalent notions. These are arguments for the Church–Turing thesis that the intuitive notion of computable is correctly formalised as lambda definable, Turing computable or recursive (cf. also [[Church thesis]]). Although many programming languages are based on the computational model of Turing (imperative programming), presently the model of Church enjoys a lot of attention in the form of functional programming.
 
 
as part of a theory intended as a foundation for mathematics. This foundational theory consisted of a part dealing with logical symbols and rules and a part dealing with algorithms operating on these symbols. After it was shown by S.C. Kleene and J.B. Rosser [[#References|[a7]]] that this foundational system was inconsistent, the part dealing with algorithms only was isolated as the (type-free) lambda calculus. It turned out to be quite successful in capturing the intuitive notion of [[Computable function|computable function]]. Kleene [[#References|[a6]]] showed that exactly the recursive functions (cf. [[Recursive function|Recursive function]]) are lambda definable in the sense given below. Then A.M. Turing [[#References|[a10]]] introduced his machines (cf. [[Turing machine|Turing machine]]) and showed that Turing computable and lambda definable are equivalent notions. These are arguments for the Church–Turing thesis that the intuitive notion of computable is correctly formalised as lambda definable, Turing computable or recursive (cf. also [[Church thesis|Church thesis]]). Although many programming languages are based on the computational model of Turing (imperative programming), presently the model of Church enjoys a lot of attention in the form of functional programming.
 
  
 
==Lambda terms.==
 
==Lambda terms.==
Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570002.png" /> be an infinite set of variables. The set of lambda terms, notation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570003.png" />, is the least set satisfying: if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570004.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570005.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570006.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570007.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570008.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l0570009.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700010.png" />. The term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700011.png" /> has as intended meaning: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700012.png" /> considered as function applied to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700013.png" /> considered as argument; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700014.png" /> stands for the intuitive function that assigns to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700015.png" /> the value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700016.png" /> (possibly containing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700017.png" />). One uses <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700018.png" /> for syntactic equality between terms. So <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700019.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700020.png" />. Examples of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700021.png" />-terms are: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700022.png" />, the identity; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700023.png" />, the function with constant value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700024.png" />; and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700025.png" />, the function with constant value <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700026.png" />. Self-application is allowed: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700027.png" /> is a correct <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700028.png" />-term. In the expression <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700029.png" /> the occurrences of the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700030.png" /> are said to be bound by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700031.png" />. If a variable occurrence is not bound, then it is said to be free in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700032.png" />. A <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700033.png" />-term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700034.png" /> is closed if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700036.png" />. E.g. in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700037.png" /> the variable <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700038.png" /> occurs free and bound and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700039.png" /> occurs free; <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700040.png" /> is a closed term. Terms that differ only in the names of bound variables are identified; e.g. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700041.png" />.
+
Let $  V $
 +
be an infinite set of variables. The set of lambda terms, notation $  \Lambda $,  
 +
is the least set satisfying: if $  x \in V $,  
 +
then $  x \in \Lambda $;  
 +
if $  M, N \in \Lambda $,  
 +
then $  ( MN) \in \Lambda $;  
 +
if $  M \in \Lambda $
 +
and $  x \in \Lambda $,  
 +
then $  ( \lambda x M) \in \Lambda $.  
 +
The term $  MN $
 +
has as intended meaning: $  M $
 +
considered as function applied to $  N $
 +
considered as argument; $  \lambda x M $
 +
stands for the intuitive function that assigns to $  x $
 +
the value $  M $(
 +
possibly containing $  x $).  
 +
One uses $  \equiv $
 +
for syntactic equality between terms. So $  \lambda xx \equiv \lambda xx \not\equiv \lambda xy $
 +
and $  ( \lambda xx) a \not\equiv a $.  
 +
Examples of $  \lambda $-
 +
terms are: $  \mathbf I \equiv \lambda xx $,  
 +
the identity; $  \lambda xy $,  
 +
the function with constant value $  y $;  
 +
and $  \lambda x \mathbf I $,  
 +
the function with constant value $  \mathbf I $.  
 +
Self-application is allowed: $  \lambda x ( xx) $
 +
is a correct $  \lambda $-
 +
term. In the expression $  \lambda x M $
 +
the occurrences of the variable $  x $
 +
are said to be bound by $  \lambda $.  
 +
If a variable occurrence is not bound, then it is said to be free in $  M $.  
 +
A $  \lambda $-
 +
term $  M $
 +
is closed if $  FV ( M) = \emptyset $.  
 +
E.g. in $  ( \lambda xx) yx $
 +
the variable $  x $
 +
occurs free and bound and $  y $
 +
occurs free; $  \mathbf I $
 +
is a closed term. Terms that differ only in the names of bound variables are identified; e.g. $  y ( \lambda zz) \equiv y ( \lambda xx) \not\equiv w ( \lambda xx) $.
  
 
==Conversion.==
 
==Conversion.==
Following the intended meaning of the lambda expressions, the following so-called <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700043.png" />-rule is postulated as axiom: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700044.png" />, or, more generally, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700045.png" />, where the right-hand side stands for the result of substituting <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700046.png" /> for the free occurrences of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700047.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700048.png" />. When performing a substitution <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700049.png" />, care should be taken that no free variable in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700050.png" /> becomes bound. This can be accomplished by renaming all bound variables of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700051.png" />. E.g. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700052.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700053.png" />. If an equation <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700054.png" /> is provable from the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700055.png" />-rule alone, then one says that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700056.png" /> is convertible to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700057.png" />.
+
Following the intended meaning of the lambda expressions, the following so-called $  \beta $-
 +
rule is postulated as axiom: $  ( \lambda x M) x = M $,  
 +
or, more generally, $  ( \lambda x M) N = M [ x: = N] $,  
 +
where the right-hand side stands for the result of substituting $  N $
 +
for the free occurrences of $  x $
 +
in $  M $.  
 +
When performing a substitution $  M [ x: = N] $,  
 +
care should be taken that no free variable in $  N $
 +
becomes bound. This can be accomplished by renaming all bound variables of $  M $.  
 +
E.g. $  ( \lambda z ( xz)) [ x: = zz] \equiv ( \lambda z  ^  \prime  . ( xz  ^  \prime  )) [ x: = zz] \equiv ( \lambda z  ^  \prime  (( zz) z  ^  \prime  )) \not\equiv $
 +
$  \lambda z (( zz) z) $.  
 +
If an equation $  M = N $
 +
is provable from the $  \beta $-
 +
rule alone, then one says that $  M $
 +
is convertible to $  N $.
  
 
==Currying.==
 
==Currying.==
Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700058.png" /> is a term such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700059.png" />. (To make notation easier, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700060.png" /> stands for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700061.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700062.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700063.png" />. Then one may write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700064.png" />.) The method is due to M. Schönfinkel [[#References|[a9]]] but is called currying after H.B. Curry who made it popular.
+
Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example $  F \equiv ( \lambda x ( \lambda y ( yx))) $
 +
is a term such that $  ( FA) B = BA $.  
 +
(To make notation easier, $  \lambda x _ {1} \dots x _ {n} .M $
 +
stands for $  ( \lambda x _ {1} ( \lambda x _ {2} \dots ( \lambda x _ {n} M) \dots )) $
 +
and $  FA _ {1} \dots A _ {n} $
 +
for $  ( \dots (( FA _ {1} ) A _ {2} ) \dots A _ {n} ) $.  
 +
Then one may write $  ( \lambda xy.yx) AB = BA $.)  
 +
The method is due to M. Schönfinkel [[#References|[a9]]] but is called [[currying]] after H.B. Curry who made it popular.
  
 
==Representing computations.==
 
==Representing computations.==
From the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700065.png" />-rule one can prove the following fixed-point theorem. For all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700066.png" />-terms <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700067.png" /> there exists a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700068.png" />-term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700069.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700070.png" />. (Indeed, a proof is as follows. Take <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700071.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700072.png" />. Then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700073.png" />.) This result will be used to represent recursion. Write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700074.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700075.png" />. Define for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700076.png" /> (the set of natural numbers) the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700077.png" />-term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700078.png" />. The <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700079.png" /> are called Church numerals. A function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700080.png" /> is said to be <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700082.png" />-definable if there exists a <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700083.png" />-term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700084.png" /> such that for all <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700085.png" /> one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700086.png" />. This definition is extended to functions of more arguments by requiring e.g. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700087.png" />. Integer addition is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700088.png" />-definable using the term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700089.png" />. The predecessor function is <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700090.png" />-defined by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700091.png" />. Write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700092.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700093.png" />. Write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700094.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700095.png" />. Then  "i fBthenXelseY"  can be represented by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700096.png" />. Write <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700097.png" />. Then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700098.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l05700099.png" />. Now suppose <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000100.png" /> is defined by recursion, e.g. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000101.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000102.png" />. Then it is possible to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000103.png" />-define <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000104.png" /> as follows. One wants an <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000105.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000106.png" />. This holds if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000107.png" />. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000108.png" />. Now <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000109.png" /> can be found using the fixed-point theorem. In a similar way minimalization (searching) can be represented by <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000110.png" />-terms.
+
From the $  \beta $-
 +
rule one can prove the following fixed-point theorem. For all $  \lambda $-
 +
terms $  F $
 +
there exists a $  \lambda $-
 +
term $  X $
 +
such that $  FX = X $.  
 +
(Indeed, a proof is as follows. Take $  W \equiv \lambda x.F ( xx) $
 +
and $  X \equiv WW $.  
 +
Then  $  X \equiv ( \lambda x.F ( xx)) W = F ( WW) \equiv FX $.)  
 +
This result will be used to represent recursion. Write $  M  ^ {0} N \equiv N $
 +
and $  M ^ {k + 1 } N \equiv M ( M  ^ {k} N) $.  
 +
Define for $  k \in \mathbf N $(
 +
the set of natural numbers) the $  \lambda $-
 +
term $  \mathbf c _ {k} \equiv \lambda fx.f ^ { k } x $.  
 +
The $  \mathbf c _ {k} $
 +
are called Church numerals. A function $  f: \mathbf N \rightarrow \mathbf N $
 +
is said to be $  \lambda $-
 +
definable if there exists a $  \lambda $-
 +
term $  F $
 +
such that for all $  k \in \mathbf N $
 +
one has $  F \mathbf c _ {k} = \mathbf c _ {f ( k) }  $.  
 +
This definition is extended to functions of more arguments by requiring e.g. $  F \mathbf c _ {k _ {1}  } \mathbf c _ {k _ {2}  } = \mathbf c _ {f ( k _ {1}  , k _ {2} ) } $.  
 +
Integer addition is $  \lambda $-
 +
definable using the term $  \mathbf{Plus} \equiv \lambda pqfx.pf ( qfx) $.  
 +
The predecessor function is $  \lambda $-
 +
defined by $  Q \equiv \lambda pfx.p ( \lambda ab.b ( af  )) ( \lambda q.x) \mathbf I $.  
 +
Write $  \mathbf I $
 +
for $  Qx $.  
 +
Write $  \mathbf{true} \equiv \lambda xy.x $
 +
and $  \mathbf{false} \equiv \lambda xy.y $.  
 +
Then  "i fBthenXelseY"  can be represented by $  BXY $.  
 +
Write $  \mathbf{zero} _ {?} \equiv \lambda p.p ( \lambda x. \mathbf{false} ) \mathbf{true} $.  
 +
Then $  \mathbf{zero} _ {?}  \mathbf c _ {0} = \mathbf{true} $
 +
and $  \mathbf{zero} _ {?}  \mathbf c _ {k + 1 }  = \mathbf{false} $.  
 +
Now suppose $  f $
 +
is defined by recursion, e.g. $  f ( 0, x) = 0 $,
 +
$  f ( k + 1, x) = f ( k, x) + x $.  
 +
Then it is possible to $  \lambda $-
 +
define $  f $
 +
as follows. One wants an $  F $
 +
such that $  Fkx = {\mathbf{i f }  zero } _ {?}  k  {\mathbf{then}  c } _ {0}  {\mathbf{else} }  ( {\mathbf{Plus} } ( F k  ^ {-} x) x) $.  
 +
This holds if $  F = \lambda kx $.
 +
$  {\mathbf{i f }  zero } _ {?}  k  {\mathbf{then}  c } _ {0}  {\mathbf{else} }  ( {\mathbf{Plus} } ( F k  ^ {-} x) x) = ( \lambda fkx. {\mathbf{i f }  zero } _ {?}  k  {\mathbf{then}  c } _ {0}  {\mathbf{else} }  ( {\mathbf{Plus} } ( f  k  ^ {-} x) x)) F $.  
 +
Now $  F $
 +
can be found using the fixed-point theorem. In a similar way minimalization (searching) can be represented by $  \lambda $-
 +
terms.
  
 
==Reduction strategies.==
 
==Reduction strategies.==
If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000111.png" /> <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000112.png" />-defines a function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000113.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000114.png" /> can be computed by evaluating <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000115.png" />. Several strategies can be used in order to evaluate this <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000116.png" />-term by giving priorities to the subexpressions <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000117.png" /> to be rewritten to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000118.png" />. (This replacement is called reduction.) If first the innermost such expressions are computed, then one has eager evaluation; if the outermost expressions are treated first, then one has lazy evaluation. For these and other reduction strategies, theoretical properties are given in [[#References|[a1]]], Chapt. 13, and implementation issues are treated in [[#References|[a4]]], Chapt. 9.
+
If $  F $
 +
$  \lambda $-
 +
defines a function $  f $,  
 +
then $  f ( k) $
 +
can be computed by evaluating $  F \mathbf c _ {k} $.  
 +
Several strategies can be used in order to evaluate this $  \lambda $-
 +
term by giving priorities to the subexpressions $  ( \lambda x.M) N $
 +
to be rewritten to $  M [ x: = N] $.  
 +
(This replacement is called reduction.) If first the innermost such expressions are computed, then one has eager evaluation; if the outermost expressions are treated first, then one has lazy evaluation. For these and other reduction strategies, theoretical properties are given in [[#References|[a1]]], Chapt. 13, and implementation issues are treated in [[#References|[a4]]], Chapt. 9.
  
 
==Types.==
 
==Types.==
While <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000122.png" />-terms can be used to represent algorithms, types serve to keep an order in these representing terms. (A similar role is played by dimensions of physical entities.) Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000123.png" /> be a set of symbols considered as atomic types (<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000124.png" /> may e.g. contain nat and bool). Types form the least set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000125.png" /> such that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000126.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000127.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000128.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000129.png" />. A statement is of the form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000130.png" /> with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000131.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000132.png" />. The term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000133.png" /> is the subject and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000134.png" /> is the predicate of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000135.png" />. A basis is a set of statements with only distinct variables as subjects. If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000136.png" /> is a basis, then the notion <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000137.png" /> (read: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000138.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000139.png" /> is derivable from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000140.png" />; or: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000141.png" /> yields <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000142.png" /> in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000143.png" />) is the least relation satisfying: If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000144.png" />, if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000145.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000146.png" />, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000147.png" />; if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000148.png" />; then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000149.png" />. Examples of valid derivable statements are the following: <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000150.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000151.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000152.png" />, and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000153.png" />. The term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000154.png" /> cannot be typed.
+
While $  \lambda $-
 +
terms can be used to represent algorithms, types serve to keep an order in these representing terms. (A similar role is played by dimensions of physical entities.) Let $  \mathbf V $
 +
be a set of symbols considered as atomic types ( $  \mathbf V $
 +
may e.g. contain nat and bool). Types form the least set $  \mathbf T $
 +
such that if $  \alpha \in \mathbf V $,  
 +
then $  \alpha \in \mathbf T $;  
 +
if $  \sigma , \tau \in \mathbf T $,  
 +
then $  ( \sigma \rightarrow \tau ) \in \mathbf T $.  
 +
A statement is of the form $  M : \sigma $
 +
with $  M \in \Lambda $
 +
and $  \sigma \in \mathbf T $.  
 +
The term $  M $
 +
is the subject and $  \sigma $
 +
is the predicate of $  M: \sigma $.  
 +
A basis is a set of statements with only distinct variables as subjects. If $  \Gamma $
 +
is a basis, then the notion $  \Gamma \vdash M : \sigma $(
 +
read: $  M $
 +
in $  \sigma $
 +
is derivable from $  \Gamma $;  
 +
or: $  \Gamma $
 +
yields $  M $
 +
in $  \sigma $)  
 +
is the least relation satisfying: If $  ( x: \sigma ) \in \Gamma \vdash x: \sigma $,  
 +
if $  \Gamma \vdash M: ( \sigma \rightarrow \tau ) $
 +
and $  \Gamma \vdash N: \sigma $,  
 +
then $  \Gamma \vdash ( MN): \tau $;  
 +
if $  \Gamma \cup \{ x: \sigma \} \vdash M:  \tau $;  
 +
then $  \Gamma \vdash ( \lambda x.M): ( \sigma \rightarrow \tau ) $.  
 +
Examples of valid derivable statements are the following: $  \{ x :  \sigma \} \vdash x: \sigma $,
 +
$  \vdash ( \lambda x.x):  ( \sigma \rightarrow \sigma ) $,  
 +
$  \vdash ( \lambda xy.x): ( \sigma \rightarrow ( \tau \rightarrow \sigma )) $,  
 +
and $  \vdash ( \lambda xy.y): ( \sigma \rightarrow ( \tau \rightarrow \tau )) $.  
 +
The term $  \lambda x.xx $
 +
cannot be typed.
  
The following theorems hold: 1) If <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000155.png" />, then all reductions starting with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000156.png" /> are terminating. 2) It is decidable whether, given a term <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000157.png" />, there are <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000158.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000159.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000160.png" />; moreover, these <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000161.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000162.png" /> can be constructed if they exist. See e.g. [[#References|[a5]]] for proofs.
+
The following theorems hold: 1) If $  \Gamma \vdash M: \sigma $,  
 +
then all reductions starting with $  M $
 +
are terminating. 2) It is decidable whether, given a term $  M $,  
 +
there are $  \Gamma $
 +
and $  \sigma $
 +
such that $  \Gamma \vdash M: \sigma $;  
 +
moreover, these $  \Gamma $
 +
and $  \sigma $
 +
can be constructed if they exist. See e.g. [[#References|[a5]]] for proofs.
  
The programming language <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000163.png" />, see [[#References|[a8]]], is based on the type-free lambda calculus in which to some terms types are assigned as above. The second theorem above makes it possible that the programmer does not need to write types: a compiler can construct them.
+
The programming language $  ML $,  
 +
see [[#References|[a8]]], is based on the type-free lambda calculus in which to some terms types are assigned as above. The second theorem above makes it possible that the programmer does not need to write types: a compiler can construct them.
  
 
==Semantics.==
 
==Semantics.==
Since <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000164.png" />-terms act at the same time as a function and as an argument, one would like to have a set <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000165.png" /> such that its function space <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000166.png" /> is in a one-to-one correspondence with <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000167.png" /> in order to give a semantics to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000168.png" />-terms. This is impossible for cardinality reasons. D.S. Scott constructed models for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000169.png" />-terms by restricting <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000170.png" /> to the space of continuous functions from <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000171.png" /> to <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000172.png" /> (for an appropriate notion of continuity) which has the same cardinality as <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000173.png" />. A simple model in this style has been constructed by E. Engeler as follows. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000174.png" /> be a non-empty set. Let <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000175.png" /> be the smallest set containing <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000176.png" /> such that for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000177.png" /> and finite <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000178.png" /> one has <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000179.png" />. Take <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000180.png" /> the collection of all subsets of <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000181.png" />. A function <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000182.png" /> is called continuous if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000184.png" />. For such <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000185.png" /> define <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000186.png" />. In order to reconstruct <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000187.png" />, form <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000188.png" />, define for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000189.png" /> the application <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000190.png" />. Then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000191.png" />. Now <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000192.png" />-terms can be interpreted in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000193.png" />. Let a mapping <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000194.png" /> be given (environment). Define for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000196.png" /> the element <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000197.png" />, <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000198.png" />, where <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000199.png" /> is the environment <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000200.png" /> such that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000201.png" /> and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000202.png" /> for <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000203.png" />. In order that this definition makes sense it should be verified that <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000204.png" /> depends continuously on <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000205.png" />. This is the case because the application function is continuous in each of its variables. <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000206.png" /> is a model of the <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000207.png" />-calculus in the sense that if <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000208.png" /> is provable, then <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000209.png" /> for each <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000210.png" />. It can be shown that terms with little computational effect, like <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000211.png" />, have as image in <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000212.png" /> the empty set.
+
Since $  \lambda $-
 +
terms act at the same time as a function and as an argument, one would like to have a set $  D $
 +
such that its function space $  D \rightarrow D $
 +
is in a one-to-one correspondence with $  D $
 +
in order to give a semantics to $  \lambda $-
 +
terms. This is impossible for cardinality reasons. D.S. Scott constructed models for $  \lambda $-
 +
terms by restricting $  D \rightarrow D $
 +
to the space of continuous functions from $  D $
 +
to $  D $(
 +
for an appropriate notion of continuity) which has the same cardinality as $  D $.  
 +
A simple model in this style has been constructed by E. Engeler as follows. Let $  A $
 +
be a non-empty set. Let $  B $
 +
be the smallest set containing $  A $
 +
such that for $  b \in B $
 +
and finite $  \beta \in B $
 +
one has $  ( b, \beta ) \in B $.  
 +
Take $  D _ {A} $
 +
the collection of all subsets of $  B $.  
 +
A function $  f: D _ {A} \rightarrow D _ {A} $
 +
is called continuous if $  f ( d) = \cup \{ {f ( \beta ) } : {\beta \subseteq d, \beta  \textrm{ finite } } \} $.  
 +
For such $  f $
 +
define  $  \lambda x.f ( x) = \{ {( b, \beta ) } : {b \in f ( \beta ) } \} \in D _ {A} $.  
 +
In order to reconstruct $  f $,  
 +
form $  \lambda x.f ( x) $,  
 +
define for $  d, e \in D _ {A} $
 +
the application $  d.e = \{ {b \in B } : {\exists \beta \subseteq e ( b, \beta ) \in d } \} $.  
 +
Then  $  ( \lambda x.f ( x)) .e = f ( e) $.  
 +
Now $  \lambda $-
 +
terms can be interpreted in $  D _ {A} $.  
 +
Let a mapping $  \rho : V \rightarrow D _ {A} $
 +
be given (environment). Define for $  M \in \Lambda $
 +
the element $  [[ M ]] _  \rho  = [[ M ]] _  \rho  [ [ N ] ] _  \rho  $,
 +
$  [ [ \lambda x.M ] ] _  \rho  = \lambda d [ [ M ] ] _ {\rho ( x: = d) }  $,  
 +
where $  \rho ( x: = d) $
 +
is the environment $  \rho  ^  \prime  $
 +
such that $  \rho  ^  \prime  ( x) = d $
 +
and $  \rho  ^  \prime  ( y) = \rho ( y) $
 +
for $  y \not\equiv x $.  
 +
In order that this definition makes sense it should be verified that $  [ [ M ] ] _ {\rho ( x: = d) }  $
 +
depends continuously on $  d $.  
 +
This is the case because the application function is continuous in each of its variables. $  D _ {A} $
 +
is a model of the $  \lambda $-
 +
calculus in the sense that if $  M = N $
 +
is provable, then $  [ [ M ] ] _  \rho  = [ [ N ] ] _  \rho  $
 +
for each $  \rho $.  
 +
It can be shown that terms with little computational effect, like $  ( \lambda x.xx) ( \lambda x.xx) $,  
 +
have as image in $  D _ {A} $
 +
the empty set.
  
 
====References====
 
====References====
<table><TR><TD valign="top">[a1]</TD> <TD valign="top">  H.P. Barendrecht,  "The lambda-calculus, its syntax and semantics" , North-Holland  (1984)</TD></TR><TR><TD valign="top">[a2]</TD> <TD valign="top">  H.P. Barendregt,  "Lambda calculi with types" , ''Handbook of Logic in Computer Science'' , Oxford Univ. Press  (To appear (1990))</TD></TR><TR><TD valign="top">[a3a]</TD> <TD valign="top">  A. Church,  "A set of postulates for the foundation of logic"  ''Ann. of Math. (2)'' , '''33'''  (1932)  pp. 346–366</TD></TR><TR><TD valign="top">[a3b]</TD> <TD valign="top">  A. Church,  "A set of postulates for the foundation of logic"  ''Ann. of Math. (2)'' , '''34'''  (1933)  pp. 839–864</TD></TR><TR><TD valign="top">[a4]</TD> <TD valign="top">  A.J. Field,  P.G. Harrison,  "Functional programming" , Addison-Wesley  (1988)</TD></TR><TR><TD valign="top">[a5]</TD> <TD valign="top">  J.R. Hindley,  J.P. Seldin,  "Introduction to combinators and lambda calculus" , Cambridge Univ. Press  (1986)</TD></TR><TR><TD valign="top">[a6]</TD> <TD valign="top">  S.C. Kleene,  "<img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000213.png" />-definability and recursiveness"  ''Duke Math. J.'' , '''2'''  (1936)  pp. 340–353</TD></TR><TR><TD valign="top">[a7]</TD> <TD valign="top">  S.C. Kleene,  J.B. Rosser,  "The inconsistency of certain formal logics"  ''Ann. of Math. (2)'' , '''36'''  (1935)  pp. 630–636</TD></TR><TR><TD valign="top">[a8]</TD> <TD valign="top">  R. Milner,  "A proposal for standard <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000214.png" />" , ''Proc. ACM Symp. on LISP and Functional Programming (Austin)''  (1984)  pp. 184–197</TD></TR><TR><TD valign="top">[a9]</TD> <TD valign="top">  M. Schönfinkel,  "Ueber die Bausteine der mathematische Logik"  ''Math. Ann.'' , '''92'''  (1924)  pp. 305–316</TD></TR><TR><TD valign="top">[a10]</TD> <TD valign="top">  A. Turing,  "On computable numbers with an application to the Entscheidungsproblem"  ''Proc. London Math. Soc.'' , '''42'''  (1936)  pp. 230–265</TD></TR><TR><TD valign="top">[a11]</TD> <TD valign="top">  A. Turing,  "Computability and <img align="absmiddle" border="0" src="https://www.encyclopediaofmath.org/legacyimages/l/l057/l057000/l057000215.png" />-definability"  ''J. Symbolic Logic'' , '''2'''  (1937)  pp. 153–163</TD></TR></table>
+
<table><tr><td valign="top">[a1]</td> <td valign="top">  H.P. Barendregt,  "The lambda-calculus, its syntax and semantics" , North-Holland  (1984)</td></tr><tr><td valign="top">[a2]</td> <td valign="top">  H.P. Barendregt,  "Lambda calculi with types" , ''Handbook of Logic in Computer Science'' , Oxford Univ. Press  (To appear (1990))</td></tr><tr><td valign="top">[a3a]</td> <td valign="top">  A. Church,  "A set of postulates for the foundation of logic"  ''Ann. of Math. (2)'' , '''33'''  (1932)  pp. 346–366</td></tr><tr><td valign="top">[a3b]</td> <td valign="top">  A. Church,  "A set of postulates for the foundation of logic"  ''Ann. of Math. (2)'' , '''34'''  (1933)  pp. 839–864</td></tr><tr><td valign="top">[a4]</td> <td valign="top">  A.J. Field,  P.G. Harrison,  "Functional programming" , Addison-Wesley  (1988)</td></tr><tr><td valign="top">[a5]</td> <td valign="top">  J.R. Hindley,  J.P. Seldin,  "Introduction to combinators and lambda calculus" , Cambridge Univ. Press  (1986)</td></tr><tr><td valign="top">[a6]</td> <td valign="top">  S.C. Kleene,  "$\lambda$-definability and recursiveness"  ''Duke Math. J.'' , '''2'''  (1936)  pp. 340–353</td></tr><tr><td valign="top">[a7]</td> <td valign="top">  S.C. Kleene,  J.B. Rosser,  "The inconsistency of certain formal logics"  ''Ann. of Math. (2)'' , '''36'''  (1935)  pp. 630–636</td></tr><tr><td valign="top">[a8]</td> <td valign="top">  R. Milner,  "A proposal for standard $M L$" , ''Proc. ACM Symp. on LISP and Functional Programming (Austin)''  (1984)  pp. 184–197</td></tr><tr><td valign="top">[a9]</td> <td valign="top">  M. Schönfinkel,  "Ueber die Bausteine der mathematische Logik"  ''Math. Ann.'' , '''92'''  (1924)  pp. 305–316</td></tr><tr><td valign="top">[a10]</td> <td valign="top">  A. Turing,  "On computable numbers with an application to the Entscheidungsproblem"  ''Proc. London Math. Soc.'' , '''42'''  (1936)  pp. 230–265</td></tr><tr><td valign="top">[a11]</td> <td valign="top">  A. Turing,  "Computability and $\lambda$-definability"  ''J. Symbolic Logic'' , '''2'''  (1937)  pp. 153–163</td></tr></table>

Latest revision as of 16:57, 1 July 2020


lambda calculus.

Introduction.

The lambda calculus was introduced in 1932–1933 by A. Church (1903-1995) as part of a theory intended as a foundation for mathematics. This foundational theory consisted of a part dealing with logical symbols and rules and a part dealing with algorithms operating on these symbols. After it was shown by S.C. Kleene and J.B. Rosser [a7] that this foundational system was inconsistent, the part dealing with algorithms only was isolated as the (type-free) lambda calculus. It turned out to be quite successful in capturing the intuitive notion of computable function. Kleene [a6] showed that exactly the recursive functions (cf. Recursive function) are lambda definable in the sense given below. Then A.M. Turing [a10] introduced his machines (cf. Turing machine) and showed that Turing computable and lambda definable are equivalent notions. These are arguments for the Church–Turing thesis that the intuitive notion of computable is correctly formalised as lambda definable, Turing computable or recursive (cf. also Church thesis). Although many programming languages are based on the computational model of Turing (imperative programming), presently the model of Church enjoys a lot of attention in the form of functional programming.

Lambda terms.

Let $ V $ be an infinite set of variables. The set of lambda terms, notation $ \Lambda $, is the least set satisfying: if $ x \in V $, then $ x \in \Lambda $; if $ M, N \in \Lambda $, then $ ( MN) \in \Lambda $; if $ M \in \Lambda $ and $ x \in \Lambda $, then $ ( \lambda x M) \in \Lambda $. The term $ MN $ has as intended meaning: $ M $ considered as function applied to $ N $ considered as argument; $ \lambda x M $ stands for the intuitive function that assigns to $ x $ the value $ M $( possibly containing $ x $). One uses $ \equiv $ for syntactic equality between terms. So $ \lambda xx \equiv \lambda xx \not\equiv \lambda xy $ and $ ( \lambda xx) a \not\equiv a $. Examples of $ \lambda $- terms are: $ \mathbf I \equiv \lambda xx $, the identity; $ \lambda xy $, the function with constant value $ y $; and $ \lambda x \mathbf I $, the function with constant value $ \mathbf I $. Self-application is allowed: $ \lambda x ( xx) $ is a correct $ \lambda $- term. In the expression $ \lambda x M $ the occurrences of the variable $ x $ are said to be bound by $ \lambda $. If a variable occurrence is not bound, then it is said to be free in $ M $. A $ \lambda $- term $ M $ is closed if $ FV ( M) = \emptyset $. E.g. in $ ( \lambda xx) yx $ the variable $ x $ occurs free and bound and $ y $ occurs free; $ \mathbf I $ is a closed term. Terms that differ only in the names of bound variables are identified; e.g. $ y ( \lambda zz) \equiv y ( \lambda xx) \not\equiv w ( \lambda xx) $.

Conversion.

Following the intended meaning of the lambda expressions, the following so-called $ \beta $- rule is postulated as axiom: $ ( \lambda x M) x = M $, or, more generally, $ ( \lambda x M) N = M [ x: = N] $, where the right-hand side stands for the result of substituting $ N $ for the free occurrences of $ x $ in $ M $. When performing a substitution $ M [ x: = N] $, care should be taken that no free variable in $ N $ becomes bound. This can be accomplished by renaming all bound variables of $ M $. E.g. $ ( \lambda z ( xz)) [ x: = zz] \equiv ( \lambda z ^ \prime . ( xz ^ \prime )) [ x: = zz] \equiv ( \lambda z ^ \prime (( zz) z ^ \prime )) \not\equiv $ $ \lambda z (( zz) z) $. If an equation $ M = N $ is provable from the $ \beta $- rule alone, then one says that $ M $ is convertible to $ N $.

Currying.

Although abstraction is provided only to form unary functions, also functions of more arguments can be represented in lambda calculus by iterated abstraction. For example $ F \equiv ( \lambda x ( \lambda y ( yx))) $ is a term such that $ ( FA) B = BA $. (To make notation easier, $ \lambda x _ {1} \dots x _ {n} .M $ stands for $ ( \lambda x _ {1} ( \lambda x _ {2} \dots ( \lambda x _ {n} M) \dots )) $ and $ FA _ {1} \dots A _ {n} $ for $ ( \dots (( FA _ {1} ) A _ {2} ) \dots A _ {n} ) $. Then one may write $ ( \lambda xy.yx) AB = BA $.) The method is due to M. Schönfinkel [a9] but is called currying after H.B. Curry who made it popular.

Representing computations.

From the $ \beta $- rule one can prove the following fixed-point theorem. For all $ \lambda $- terms $ F $ there exists a $ \lambda $- term $ X $ such that $ FX = X $. (Indeed, a proof is as follows. Take $ W \equiv \lambda x.F ( xx) $ and $ X \equiv WW $. Then $ X \equiv ( \lambda x.F ( xx)) W = F ( WW) \equiv FX $.) This result will be used to represent recursion. Write $ M ^ {0} N \equiv N $ and $ M ^ {k + 1 } N \equiv M ( M ^ {k} N) $. Define for $ k \in \mathbf N $( the set of natural numbers) the $ \lambda $- term $ \mathbf c _ {k} \equiv \lambda fx.f ^ { k } x $. The $ \mathbf c _ {k} $ are called Church numerals. A function $ f: \mathbf N \rightarrow \mathbf N $ is said to be $ \lambda $- definable if there exists a $ \lambda $- term $ F $ such that for all $ k \in \mathbf N $ one has $ F \mathbf c _ {k} = \mathbf c _ {f ( k) } $. This definition is extended to functions of more arguments by requiring e.g. $ F \mathbf c _ {k _ {1} } \mathbf c _ {k _ {2} } = \mathbf c _ {f ( k _ {1} , k _ {2} ) } $. Integer addition is $ \lambda $- definable using the term $ \mathbf{Plus} \equiv \lambda pqfx.pf ( qfx) $. The predecessor function is $ \lambda $- defined by $ Q \equiv \lambda pfx.p ( \lambda ab.b ( af )) ( \lambda q.x) \mathbf I $. Write $ \mathbf I $ for $ Qx $. Write $ \mathbf{true} \equiv \lambda xy.x $ and $ \mathbf{false} \equiv \lambda xy.y $. Then "i fBthenXelseY" can be represented by $ BXY $. Write $ \mathbf{zero} _ {?} \equiv \lambda p.p ( \lambda x. \mathbf{false} ) \mathbf{true} $. Then $ \mathbf{zero} _ {?} \mathbf c _ {0} = \mathbf{true} $ and $ \mathbf{zero} _ {?} \mathbf c _ {k + 1 } = \mathbf{false} $. Now suppose $ f $ is defined by recursion, e.g. $ f ( 0, x) = 0 $, $ f ( k + 1, x) = f ( k, x) + x $. Then it is possible to $ \lambda $- define $ f $ as follows. One wants an $ F $ such that $ Fkx = {\mathbf{i f } zero } _ {?} k {\mathbf{then} c } _ {0} {\mathbf{else} } ( {\mathbf{Plus} } ( F k ^ {-} x) x) $. This holds if $ F = \lambda kx $. $ {\mathbf{i f } zero } _ {?} k {\mathbf{then} c } _ {0} {\mathbf{else} } ( {\mathbf{Plus} } ( F k ^ {-} x) x) = ( \lambda fkx. {\mathbf{i f } zero } _ {?} k {\mathbf{then} c } _ {0} {\mathbf{else} } ( {\mathbf{Plus} } ( f k ^ {-} x) x)) F $. Now $ F $ can be found using the fixed-point theorem. In a similar way minimalization (searching) can be represented by $ \lambda $- terms.

Reduction strategies.

If $ F $ $ \lambda $- defines a function $ f $, then $ f ( k) $ can be computed by evaluating $ F \mathbf c _ {k} $. Several strategies can be used in order to evaluate this $ \lambda $- term by giving priorities to the subexpressions $ ( \lambda x.M) N $ to be rewritten to $ M [ x: = N] $. (This replacement is called reduction.) If first the innermost such expressions are computed, then one has eager evaluation; if the outermost expressions are treated first, then one has lazy evaluation. For these and other reduction strategies, theoretical properties are given in [a1], Chapt. 13, and implementation issues are treated in [a4], Chapt. 9.

Types.

While $ \lambda $- terms can be used to represent algorithms, types serve to keep an order in these representing terms. (A similar role is played by dimensions of physical entities.) Let $ \mathbf V $ be a set of symbols considered as atomic types ( $ \mathbf V $ may e.g. contain nat and bool). Types form the least set $ \mathbf T $ such that if $ \alpha \in \mathbf V $, then $ \alpha \in \mathbf T $; if $ \sigma , \tau \in \mathbf T $, then $ ( \sigma \rightarrow \tau ) \in \mathbf T $. A statement is of the form $ M : \sigma $ with $ M \in \Lambda $ and $ \sigma \in \mathbf T $. The term $ M $ is the subject and $ \sigma $ is the predicate of $ M: \sigma $. A basis is a set of statements with only distinct variables as subjects. If $ \Gamma $ is a basis, then the notion $ \Gamma \vdash M : \sigma $( read: $ M $ in $ \sigma $ is derivable from $ \Gamma $; or: $ \Gamma $ yields $ M $ in $ \sigma $) is the least relation satisfying: If $ ( x: \sigma ) \in \Gamma \vdash x: \sigma $, if $ \Gamma \vdash M: ( \sigma \rightarrow \tau ) $ and $ \Gamma \vdash N: \sigma $, then $ \Gamma \vdash ( MN): \tau $; if $ \Gamma \cup \{ x: \sigma \} \vdash M: \tau $; then $ \Gamma \vdash ( \lambda x.M): ( \sigma \rightarrow \tau ) $. Examples of valid derivable statements are the following: $ \{ x : \sigma \} \vdash x: \sigma $, $ \vdash ( \lambda x.x): ( \sigma \rightarrow \sigma ) $, $ \vdash ( \lambda xy.x): ( \sigma \rightarrow ( \tau \rightarrow \sigma )) $, and $ \vdash ( \lambda xy.y): ( \sigma \rightarrow ( \tau \rightarrow \tau )) $. The term $ \lambda x.xx $ cannot be typed.

The following theorems hold: 1) If $ \Gamma \vdash M: \sigma $, then all reductions starting with $ M $ are terminating. 2) It is decidable whether, given a term $ M $, there are $ \Gamma $ and $ \sigma $ such that $ \Gamma \vdash M: \sigma $; moreover, these $ \Gamma $ and $ \sigma $ can be constructed if they exist. See e.g. [a5] for proofs.

The programming language $ ML $, see [a8], is based on the type-free lambda calculus in which to some terms types are assigned as above. The second theorem above makes it possible that the programmer does not need to write types: a compiler can construct them.

Semantics.

Since $ \lambda $- terms act at the same time as a function and as an argument, one would like to have a set $ D $ such that its function space $ D \rightarrow D $ is in a one-to-one correspondence with $ D $ in order to give a semantics to $ \lambda $- terms. This is impossible for cardinality reasons. D.S. Scott constructed models for $ \lambda $- terms by restricting $ D \rightarrow D $ to the space of continuous functions from $ D $ to $ D $( for an appropriate notion of continuity) which has the same cardinality as $ D $. A simple model in this style has been constructed by E. Engeler as follows. Let $ A $ be a non-empty set. Let $ B $ be the smallest set containing $ A $ such that for $ b \in B $ and finite $ \beta \in B $ one has $ ( b, \beta ) \in B $. Take $ D _ {A} $ the collection of all subsets of $ B $. A function $ f: D _ {A} \rightarrow D _ {A} $ is called continuous if $ f ( d) = \cup \{ {f ( \beta ) } : {\beta \subseteq d, \beta \textrm{ finite } } \} $. For such $ f $ define $ \lambda x.f ( x) = \{ {( b, \beta ) } : {b \in f ( \beta ) } \} \in D _ {A} $. In order to reconstruct $ f $, form $ \lambda x.f ( x) $, define for $ d, e \in D _ {A} $ the application $ d.e = \{ {b \in B } : {\exists \beta \subseteq e ( b, \beta ) \in d } \} $. Then $ ( \lambda x.f ( x)) .e = f ( e) $. Now $ \lambda $- terms can be interpreted in $ D _ {A} $. Let a mapping $ \rho : V \rightarrow D _ {A} $ be given (environment). Define for $ M \in \Lambda $ the element $ [[ M ]] _ \rho = [[ M ]] _ \rho [ [ N ] ] _ \rho $, $ [ [ \lambda x.M ] ] _ \rho = \lambda d [ [ M ] ] _ {\rho ( x: = d) } $, where $ \rho ( x: = d) $ is the environment $ \rho ^ \prime $ such that $ \rho ^ \prime ( x) = d $ and $ \rho ^ \prime ( y) = \rho ( y) $ for $ y \not\equiv x $. In order that this definition makes sense it should be verified that $ [ [ M ] ] _ {\rho ( x: = d) } $ depends continuously on $ d $. This is the case because the application function is continuous in each of its variables. $ D _ {A} $ is a model of the $ \lambda $- calculus in the sense that if $ M = N $ is provable, then $ [ [ M ] ] _ \rho = [ [ N ] ] _ \rho $ for each $ \rho $. It can be shown that terms with little computational effect, like $ ( \lambda x.xx) ( \lambda x.xx) $, have as image in $ D _ {A} $ the empty set.

References

[a1] H.P. Barendregt, "The lambda-calculus, its syntax and semantics" , North-Holland (1984)
[a2] H.P. Barendregt, "Lambda calculi with types" , Handbook of Logic in Computer Science , Oxford Univ. Press (To appear (1990))
[a3a] A. Church, "A set of postulates for the foundation of logic" Ann. of Math. (2) , 33 (1932) pp. 346–366
[a3b] A. Church, "A set of postulates for the foundation of logic" Ann. of Math. (2) , 34 (1933) pp. 839–864
[a4] A.J. Field, P.G. Harrison, "Functional programming" , Addison-Wesley (1988)
[a5] J.R. Hindley, J.P. Seldin, "Introduction to combinators and lambda calculus" , Cambridge Univ. Press (1986)
[a6] S.C. Kleene, "$\lambda$-definability and recursiveness" Duke Math. J. , 2 (1936) pp. 340–353
[a7] S.C. Kleene, J.B. Rosser, "The inconsistency of certain formal logics" Ann. of Math. (2) , 36 (1935) pp. 630–636
[a8] R. Milner, "A proposal for standard $M L$" , Proc. ACM Symp. on LISP and Functional Programming (Austin) (1984) pp. 184–197
[a9] M. Schönfinkel, "Ueber die Bausteine der mathematische Logik" Math. Ann. , 92 (1924) pp. 305–316
[a10] A. Turing, "On computable numbers with an application to the Entscheidungsproblem" Proc. London Math. Soc. , 42 (1936) pp. 230–265
[a11] A. Turing, "Computability and $\lambda$-definability" J. Symbolic Logic , 2 (1937) pp. 153–163
How to Cite This Entry:
Lambda-calculus. Encyclopedia of Mathematics. URL: http://encyclopediaofmath.org/index.php?title=Lambda-calculus&oldid=17754
This article was adapted from an original article by H.P. Barendregt (originator), which appeared in Encyclopedia of Mathematics - ISBN 1402006098. See original article