Fred's Home Page

Main
About me
Crumble
csh is bad
Debian
FredCam
Guppy
Hardware
Help out
Java-glossary
Job-control
KRoC/Linux (old)
Lambda
Life-stuff
Links
Linux
Mesh
Misc
Music
occam
occam upgrades
occam tutorial
OpenUPSd
Pictures
Programming
Projects (PhD)
Publications
Quick gdb
RAPP
RMoX
Software
UNIX crashcourse
UWG
UWGBuilder
WG / WGBuilder
XDM-Choose
XHPD

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).

Introduction

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...

  • Acknowledgement: Most of the terms here are from the CO611 (types and computation) course at Kent Uni, kindly taught by Stefan Kahrs and Simon Thompson. The type-theory computing program may happen at some point too.. :-)

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.

Lists

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

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.

Download

Last modified: 2007-08-06 15:58:55.000000000 +0100 by Fred Barnes [ds] [plain]
Page generated: Sun Apr 28 11:39:33 2013
Valid XHTML 1.0! Valid CSS!