Lambda calculus

[ intro | basic | lists | recursion | download ]

This page is all about my lambda computer -- a program that computes in the lambda calculus. For fun, I also did a Turing machine in lambda calculus (fairly trivial representation).


The lambda calculus is basically function theory, there are only three things available in the pure lambda calculus, these are:

Variablesathe variable a
Applications(a b)a applied to b
Abstractions\x.efunction e with argument x

Dispite not being very much here, the expressive power is quite suprising. Using these three simple things, numbers, lists, recursion and much more can be defined.

This page is not intended to be an introduction to the lambda calculus; there are lots of good books for that. One excellent one is Barendregt's "The Lambda Calculus : its syntax and semantics". ISBN: 0444875085 (paper-back) and 0444867481 (hard-back). It's rather mathematically extreme though...

Here is a picture of the program running.

Setting up

  1. First, download the right file. These are at the bottom of this page.
  2. Gunzip and un-tar the archive into wherever you want it.
  3. Compile the software, unless you downloaded one of the binary images.
  4. Copy the file lambdarc to your home directory as .lambdarc.
  5. Run it :)

Basic terms

There are some fairly basic terms in the lambda calculus, which turn out to be quite useful:

    K = \xy.x
    F = \xy.y

K is true, F is false. This can be seen through reduction, where applying (K a b) reduces to a, and (F a b) to b. The useful bit is that you can write terms that reduce to either K or F. When, for example, a and b are applied to such a term, a ``if-then-else'' mechanism is produced.


Several (well, infinite) ways of representing lists in the lambda calculus exist, a nice on is:

    "cons" = \xys.(sxy)
    "nil" = \x.K
    "isnil" = \p.(p (\xy.F))
    "hd" = \p.(pK)
    "tl" = \p.(pF)

This is all we need, since:

    ("hd" ("cons" a "nil")) -> a
    ("tl" ("cons" a "nil")) -> "nil"
    ("isnil" "nil") -> K
    ("isnil" ("cons" a "nil")) -> F


Recursion in the lambda calculus can be done with a fixpoint operator. A nice one is Turing's:

    "fix" = (\xy.(y (xxy)) \xy.(y (xxy)))

Applying f reduces thus:

    ("fix" f) -> (\y.(y ("fix" y)) f)
              -> (f ("fix" f))

To define a function, say map, we could write it as:

    map f [] = []
    map f (a::x) = (f a)::(map f x)

But we don't have the :: operator:

    map f [] = []
    map f l = cons (f (hd l)) (map f (tl l))

Pattern matching doesn't exist either:

    map f l = (isnil l) l (cons (f (hd l)) (map f (tl l)))

We still have map defined in terms of itself, which is not allowed, but we can make map a parameter:

    mapping map' f l = (isnil l) l (cons (f (hd l)) (map' f (tl l)))

Turning this into lambda is fairly straight-forward:

    "mapping" = \mfl.(("isnil" l) l ("cons" (f ("hd" l)) (m f ("tl" l))))

And apply the fixpoint operator to provide the real function:

    "map" = ("fix" "mapping")

Suprisingly enough, this works, and if some extra functions are defined:

    "timestwo" = \x.("CM" '2 x)
    "numlist" = ("cons" '1 ("cons" '2 ("cons" '3 "nil")))

Then we can use map for something useful:

    :("map" "timestwo" "numlist")
    = ("cons" '2 ("cons" '4 ("cons" '6 "nil")))

It takes quite a while to get there (300+ reductions), but it does work.


Last modified: 2007-08-06 15:58:55.000000000 +0100 by Fred Barnes.