Lambda-calculus

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