Lambda calculus

From CSWiki

The lambda calculus or λ-calculus is another way of defining computability, equivalent to Turing machines and partial recursive functions.

1 Definition
- 1.1 Formal definition of computation
- 1.2 Simplified notation
2 Power of the λ-calculus

[edit]

Definition

A lambda-expression is any expression generated by the following context-free grammar:

E -> V E -> (λ V . E) E -> (E E) V ->any of an infinite set of symbols

More intuitively, the lambda-expressions consist of:

single variables
expressions similar to unary Scheme lambda-expressions, using a syntax in which (λ x . y) is roughly equivalent to the Scheme expression (lambda (x) y).
procedure application: (A B) means pretty much the same as it does in Scheme: the result of running the procedure A on input B. It is important to note that procedures described by lambda-expressions are unary and accept other lambda-expressions as their parameters, not numbers or any other data type. Such data must be encoded as lambda-expressions (a few such encodings are developed later).

[edit]

Formal definition of computation

In a lambda-expression consisting of a single symbol v, say that this v is a free occurrence.
In a lambda-expression of the form (λ u . E), where u is not equal to v and E is a lambda-expression, the free occurrences of vare the free occurrences of v in E.
In a lambda-expression of the form (E E'), where E and E' are lambda-expressions, the free occurrences of v are the free occurrences in either subexpression.

Also, let E[a/b] denote the lambda-expression E with all free occurrences of the symbol a replaced by b.

Then the equivalence of lambda-expressions can be defined as follows:

(λ a . E) == (λ b . E[V/b]) for any symbol a, lambda-expression E, and symbol b that does not occur (freely or otherwise) in E (i.e., variable names may be substituted)
((λ v . E) E') == E[v/E'] for any symbol v and lambda-expressions E and E', where all free occurrences in E' are also free occurrences in E[v/E'] (this captures the idea of evaluating a procedure with a given argument by substituting the argument for all instances of the parameter variable)

[edit]

Simplified notation

We will adopt the convention that procedure application is left-associative when parentheses are omitted, that is, f g x == f (g x) == (f (g x))

Additionally, if the parentheses are omitted around a λ-expression, the body extends as far rightward as possible. So λ x . x y is the same as λ x . (x y), not (λ x . x) y.

[edit]

Power of the λ-calculus

[edit]

n-ary functions

The (λ V . E) syntax only allows unary procedures, but there is a simple remedy for this: encode n-ary procedures as higher-order procedures. For example, if we wanted a binary procedure (λ xy . x y), which takes two procedures x and y as its parameters and returns the result of applying the first to the second, we can write it as follows: (λ x . (λ y . x y)). To give it parameters, just put them after it in order: (λ x . (λ y . x y)) f g == (λ y . f y) == (f g), the desired result.

In the remainder of this page, the shorthand notation (λ abc...z . E) will be used in place of the longer (λ a . (λ b . (λ c ....(λ z . E)...))). Note that this means a zeroary procedure (λ . E) is just E.

[edit]

Boolean functions

Boolean functions are a nice entry point for getting used to the λ-calculus.

Adopt the following encodings of TRUE and FALSE:
TRUE = (λ xy . x) (the binary function that returns its first parameter)
FALSE = (λ xy . y) (the binary function that returns its second parameter)

Then
AND = (λ ab . a b FALSE) (this returns b if a is TRUE, and FALSE if a is FALSE.)
OR = (λ ab . a TRUE b) (this returns TRUE if a is TRUE, and b if a is FALSE.)
NOT = (λ a . a FALSE TRUE) (if a is TRUE, returns the first parameter, which is FALSE. If a is FALSE, returns the second parameter, which is TRUE.

For later convenience, define
IF = (λ pab . p a b)
This returns a if p is TRUE, and b if it is FALSE.

[edit]

The recursion theorem

Let t be a binary lambda-expression (in the sense described in the section on n-ary procedures). Then there is a unary lambda-expression r such that, for any lambda-expression w, r w = t r w.

Proof:
Let the Y combinator be defined as follows:
Y = (λ f . (λ x . f (x x)) (λ x . f (x x)))

Lemma 1: the Y combinator has the property that Y g == g (Y g).
Proof:
Y g == (λ x . g (x x)) (λ x . g (x x)) == g ((λ x . g (x x)) (λ x . g (x x)))) == g (Y g)

Thus, a construction for the recursion theorem is to let r = Y t, as this means r w == Y t w == t (Y t) w == t r w.

[edit]

Utility of the recursion theorem: an example

Suppose we had an encoding of the natural numbers and ways of testing their equality to zero and performing simple arithmetic (these will be developed later), and wished to write the factorial function. We cannot write
factorial = (λ n. IF (zero? n) 1 (* n (factorial (- n 1)))),
as this definition is circular. But the recursion theorem saves us, as we can instead write:
f = (λ gn. IF (zero? n) 1 (* n (g (- n 1))))
factorial = Y f
so factorial == f (Y f) == (f factorial) == (λ n. IF (zero? n) 1 (* n (factorial (- n 1)))), making the above circular definition valid.

[edit]

Equivalence to partial recursive functions

[edit]

Expressing the partial recursive functions in the λ-calculus

[edit]

Primitive functions

To encode the natural numbers in the lambda calculus, let
zero = λ f x . x
successor = λ n f x . f ((n f) x)

This results in the following encoding of the natural numbers (the "Church numerals"):
0 == λ f x . x
1 == λ f x . f x
2 == λ f x . f (f x)
3 == λ f x . f (f (f x))
4 == λ f x . f (f (f (f x)))
...

Using our existing encoding of n-ary functions, we can also define
= λ $x 0$ ... $x n - 1$ . $x m$

[edit]

A few definitions

The following predicate tests whether a number is zero:
zero? = λ n . n (λ x . FALSE) TRUE

In order to define recursion (below), it will be useful to first define pairs. Let λ z . z a b be our encoding of the pair (a, b). Then
cons = λ ab . (λ z . z a b)
car = λ p . p TRUE
cdr = λ p . p FALSE

A bit of thought will verify that these definitions work.

We can now define a function successorpair that, given a pair (n, <anything>), produces the pair (n + 1, n):
successorpair = λ p . cons (successor (car p)) (car p)

According to the definition of our encoding of the natural numbers, (n successorpair (cons zero zero)) takes the n'th-composition of successorpair and applies it to the input (0, 0). The result is the pair (n, n-1). Thus, we can define the predecessor function:
predecessor = cdr (n successorpair (cons zero zero))

[edit]

Composition

[ f $g 0$ ... $g m - 1$ ] = λ $x 0$ ... $x n - 1$ . f ( $g 0$ $x 0$ ... $x n - 1$ ) ... ( $g m - 1$ $x 0$ ... $x n - 1$ )

[edit]

Recursion

[ $v n$ f g] = λ $x 0$ ... $x n - 1$ t . IF (zero? t) (f $x 0$ ... $x n - 1$ ) (g (predecessor t) ([ $v n$ f g] $x 0$ ... $x n - 1$ (predecessor t)) $x 0$ ... $x n - 1$ )
The circularity of this definition may be removed using the recursion theorem, as was done above for the factorial function.