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.

Arithmetic in lambda calculus

There are several possible ways to define the natural numbers in lambda calculus, but by far the most common are the Church numerals, which can be defined as follows:

Related Topics:
Natural number - Church numeral

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: 0 := λ f. λ x. x

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: 1 := λ f. λ x. f x

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: 2 := λ f. λ x. f (f x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: 3 := λ f. λ x. f (f (f x))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

and so on. Intuitively, the number n in lambda calculus is a function that takes a function f as argument and returns the n-th power of f. That is to say, a Church numeral is a higher-order function -- it takes a single-argument function f, and returns another single-argument function.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

(Note that in Church's original lambda calculus, the formal parameter of a lambda expression was required to occur at least once in the function body, which made the above definition of 0 impossible.)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Given this definition of the Church numerals, we can define a successor function, which takes a number n and returns n + 1:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: SUCC := λ n. λ f. λ x. f (n f x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Addition is defined as follows:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: PLUS := λ m. λ n. λ f. λ x. m f (n f x)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

PLUS can be thought of as a function taking two natural numbers as arguments and returning a natural number; it is fun to verify that

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: PLUS 2 3    and    5

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

are equivalent lambda expressions. Multiplication can then be defined as

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: MULT := λ m. λ n. m (PLUS n) 0,

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

the idea being that multiplying m and n is the same as m times adding n to zero.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Alternatively

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: MULT = λ m. λ n. λ f. m (n f)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The predecessor  PRED n = n - 1  of a positive integer n is more difficult:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: PRED := λ n. λ f. λ x. n (λ g. λ h. h (g f)) (λ u. x) (λ u. u) 

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

or alternatively

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: PRED = λ n. n (λ g. λ k. (g 1) (λ u. PLUS (g k) 1) k) (λ v. 0) 0

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Note the trick (g 1) (λ u. PLUS (g k) 1) k which evaluates to k if g(1) is zero and to g(k) + 1 otherwise.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~