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:
Variables  a  the variable a 
Applications  (a b)  a applied to b 
Abstractions  \x.e  function 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 (paperback) and 0444867481 (hardback). 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 typetheory computing program may happen at some point too.. :)
Here is a picture of the program running.
Setting up
 First, download the right file. These are at the bottom of this page.
 Gunzip and untar the archive into wherever you want it.
 Compile the software, unless you downloaded one of the binary images.
 Copy the file lambdarc to your home directory as .lambdarc.
 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
``ifthenelse'' 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 straightforward:
"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
