Lambda calculus

In computer science, the lambda calculus is a formal system designed to investigate function definition, function application, and recursion. It was introduced by Alonzo Church and Stephen Cole Kleene in the 1930s; Church used the lambda calculus in 1936 to give a negative answer to the Entscheidungsproblem. The calculus can be used to cleanly define what is a computable function. The question of whether two lambda calculus expressions are equivalent cannot be solved by a general algorithm, and this was the first question, even before the halting problem, for which undecidability could be proved. Lambda calculus has greatly influenced functional programming languages, especially Lisp.

Logic and predicates

By convention, the following two definitions (known as Church booleans) are used for the boolean values TRUE and FALSE:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: TRUE := λ x. λ y. x

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: FALSE := λ x. λ y. y

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

::(Note that FALSE is equivalent to the Church numeral zero defined above)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Then, with these two λ-terms, we can define some logic operators:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: AND := λ p. λ q. p q FALSE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: OR := λ p. λ q. p TRUE q

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: NOT := λ p. p FALSE TRUE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: IFTHENELSE := λ p. λ x. λ y. p x y

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

We are now able to compute some logic functions, as for example:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: AND TRUE FALSE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

::≡ (λ p. λ q. p q FALSE) TRUE FALSE →β TRUE FALSE FALSE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

::≡ (λ x. λ y. x) FALSE FALSE →β FALSE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

and we see that AND TRUE FALSE is equivalent to FALSE.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

A predicate is a function which returns a boolean value. The most fundamental predicate is ISZERO which returns TRUE if and only if its argument is the Church numeral 0:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: ISZERO := λ n. n (λ x. FALSE) TRUE

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The availability of predicates and the above definition of TRUE and FALSE make it convenient to write "if-then-else" statements in lambda calculus.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~