Combinatory logic

:This article is about a topic in mathematical logic and theoretical computer science, and is not to be confused with combinatorial logic, a topic in electronics.

Summary of the lambda calculus

For complete details about the lambda calculus, see the article

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

under that head. We will summarize here. 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.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

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.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~