Combinatory Logic - Summary of The Lambda Calculus

Summary of The Lambda Calculus

The lambda calculus is concerned with objects called lambda-terms, which are strings of symbols of one of the following forms:

• v
• λv.E1
• (E1 E2)

where v is a variable name drawn from a predefined infinite set of variable names, and E1 and E2 are lambda-terms.

Terms of the form λv.E1 are called abstractions. The variable v is called the formal parameter of the abstraction, and E1 is the body of the abstraction. The term λv.E1 represents the function which, applied to an argument, binds the formal parameter v to the argument and then computes the resulting value of E1---that is, it returns E1, with every occurrence of v replaced by the argument.

Terms of the form (E1 E2) are called applications. Applications model function invocation or execution: the function represented by E1 is to be invoked, with E2 as its argument, and the result is computed. If E1 (sometimes called the applicand) is an abstraction, the term may be reduced: E2, the argument, may be substituted into the body of E1 in place of the formal parameter of E1, and the result is a new lambda term which is equivalent to the old one. If a lambda term contains no subterms of the form ((λv.E1) E2) then it cannot be reduced, and is said to be in normal form.

The expression E represents the result of taking the term E and replacing all free occurrences of v with a. Thus we write

(λv.E a) => E

By convention, we take (a b c d ... z) as short for (...(((a b) c) d) ... z). (i.e., application is left associative.)

The motivation for this definition of reduction is that it captures the essential behavior of all mathematical functions. For example, consider the function that computes the square of a number. We might write

The square of x is x*x

(Using "*" to indicate multiplication.) x here is the formal parameter of the function. To evaluate the square for a particular argument, say 3, we insert it into the definition in place of the formal parameter:

The square of 3 is 3*3

To evaluate the resulting expression 3*3, we would have to resort to our knowledge of multiplication and the number 3. Since any computation is simply a composition of the evaluation of suitable functions on suitable primitive arguments, this simple substitution principle suffices to capture the essential mechanism of computation. Moreover, in the lambda calculus, notions such as '3' and '*' can be represented without any need for externally defined primitive operators or constants. It is possible to identify terms in the lambda calculus, which, when suitably interpreted, behave like the number 3 and like the multiplication operator, q.v. Church encoding.

The lambda calculus is known to be computationally equivalent in power to many other plausible models for computation (including Turing machines); that is, any calculation that can be accomplished in any of these other models can be expressed in the lambda calculus, and vice versa. According to the Church-Turing thesis, both models can express any possible computation.

It is perhaps surprising that lambda-calculus can represent any conceivable computation using only the simple notions of function abstraction and application based on simple textual substitution of terms for variables. But even more remarkable is that abstraction is not even required. Combinatory logic is a model of computation equivalent to the lambda calculus, but without abstraction. The advantage of this is that evaluating expressions in lambda calculus is quite complicated because the semantics of substitution must be specified with great care to avoid variable capture problems. In contrast, evaluating expressions in combinatory logic is much simpler, because there is no notion of substitution.