Lambda-calculus

lambda calculus.

Introduction.

The lambda calculus was introduced in 1932–1933 by A. Church

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 be an infinite set of variables. The set of lambda terms, notation , is the least set satisfying: if , then ; if , then ; if and , then . The term has as intended meaning: considered as function applied to considered as argument; stands for the intuitive function that assigns to the value (possibly containing ). One uses for syntactic equality between terms. So and . Examples of -terms are: , the identity; , the function with constant value ; and , the function with constant value . Self-application is allowed: is a correct -term. In the expression the occurrences of the variable are said to be bound by . If a variable occurrence is not bound, then it is said to be free in . A -term is closed if . E.g. in the variable occurs free and bound and occurs free; is a closed term. Terms that differ only in the names of bound variables are identified; e.g. .

Conversion.

Following the intended meaning of the lambda expressions, the following so-called -rule is postulated as axiom: , or, more generally, , where the right-hand side stands for the result of substituting for the free occurrences of in . When performing a substitution , care should be taken that no free variable in becomes bound. This can be accomplished by renaming all bound variables of . E.g. . If an equation is provable from the -rule alone, then one says that is convertible to .

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 is a term such that . (To make notation easier, stands for and for . Then one may write .) 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 -rule one can prove the following fixed-point theorem. For all -terms there exists a -term such that . (Indeed, a proof is as follows. Take and . Then .) This result will be used to represent recursion. Write and . Define for (the set of natural numbers) the -term . The are called Church numerals. A function is said to be -definable if there exists a -term such that for all one has . This definition is extended to functions of more arguments by requiring e.g. . Integer addition is -definable using the term . The predecessor function is -defined by . Write for . Write and . Then "i fBthenXelseY" can be represented by . Write . Then and . Now suppose is defined by recursion, e.g. , . Then it is possible to -define as follows. One wants an such that . This holds if . . Now can be found using the fixed-point theorem. In a similar way minimalization (searching) can be represented by -terms.

Reduction strategies.

If -defines a function , then can be computed by evaluating . Several strategies can be used in order to evaluate this -term by giving priorities to the subexpressions to be rewritten to . (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 -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 be a set of symbols considered as atomic types ( may e.g. contain nat and bool). Types form the least set such that if , then ; if , then . A statement is of the form with and . The term is the subject and is the predicate of . A basis is a set of statements with only distinct variables as subjects. If is a basis, then the notion (read: in is derivable from ; or: yields in ) is the least relation satisfying: If , if and , then ; if ; then . Examples of valid derivable statements are the following: , , , and . The term cannot be typed.

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

The programming language , 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 -terms act at the same time as a function and as an argument, one would like to have a set such that its function space is in a one-to-one correspondence with in order to give a semantics to -terms. This is impossible for cardinality reasons. D.S. Scott constructed models for -terms by restricting to the space of continuous functions from to (for an appropriate notion of continuity) which has the same cardinality as . A simple model in this style has been constructed by E. Engeler as follows. Let be a non-empty set. Let be the smallest set containing such that for and finite one has . Take the collection of all subsets of . A function is called continuous if . For such define . In order to reconstruct , form , define for the application . Then . Now -terms can be interpreted in . Let a mapping be given (environment). Define for the element , , where is the environment such that and for . In order that this definition makes sense it should be verified that depends continuously on . This is the case because the application function is continuous in each of its variables. is a model of the -calculus in the sense that if is provable, then for each . It can be shown that terms with little computational effect, like , have as image in 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, "-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 " , 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 -definability" J. Symbolic Logic , 2 (1937) pp. 153–163