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.

Recursion

Recursion is the definition of a function using the function itself; on the face of it, lambda calculus does not allow this. However, this impression is misleading. Consider for instance the factorial function f(n) recursively defined by

Related Topics:
Recursion - Factorial

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:f(n) = 1, if n = 0; and n·f(n-1), if n>0.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

In lambda calculus, one cannot define a function which includes itself. To get around this, one may start by defining a function, here called g, which takes a function f as an argument and returns another function that takes n as an argument:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:g := λ f. λ n. (1, if n = 0; and n·f(n-1), if n>0).

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

The function that g returns either returns the constant 1, or returns n times the application of the function f to n-1. Using the ISZERO predicate, and boolean and algebraic definitions described above, the function g can be defined in lambda calculus.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

However, g by itself is still not recursive; in order to use g to create the recursive factorial function, the function passed to g as f must have specific properties. Namely, the function passed as f must expand to the function g called with one argument -- and that argument must be the function that was passed as f again!

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

In other words, f must expand to g(f). This call to g will then expand to the above factorial function and calculate down to another level of recursion. In that expansion the function f will appear again, and will again expand to g(f) and continue the recursion. This kind of function, where f = g(f), is called a fixed-point of g, and it turns out that it can be implemented in the lambda calculus using what is known as the paradoxical operator or fixed-point operator and is represented as Y -- the Y combinator:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:Y = λ g. (λ x. g (x x)) (λ x. g (x x))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

In the lambda calculus, Y g is a fixed-point of g, as it expands to g (Y g). Now, to complete our recursive call to the factorial function, we would simply call  g (Y g) n,  where n is the number we are calculating the factorial of.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

Given n = 5, for example, this expands to:

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:(λ n.(1, if n = 0; and n·((Y g)(n-1)), if n>0)) 5

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:1, if 5 = 0; and 5·(g(Y g)(5-1)), if 5>0

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(g(Y g) 4)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 4)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(1, if 4 = 0; and 4·(g(Y g)(4-1)), if 4>0)

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(4·(g(Y g) 3))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(4·(λ n. (1, if n = 0; and n·((Y g)(n-1)), if n>0) 3))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(4·(1, if 3 = 0; and 3·(g(Y g)(3-1)), if 3>0))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

:5·(4·(3·(g(Y g) 2)))

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

: ...

~ ~ ~ ~ ~ ~ ~ ~ ~ ~

And so on, evaluating the structure of the algorithm recursively. Every recursively defined function can be seen as a fixed point of some other suitable function, and therefore, using Y, every recursively defined function can be expressed as a lambda expression. In particular, we can now cleanly define the subtraction, multiplication and comparison predicate of natural numbers recursively.

~ ~ ~ ~ ~ ~ ~ ~ ~ ~