A λ-Toolbox in Haskell
I've been recently a teaching assistent for functional programming in Haskell, in which - among other things - the lambda calculus (quick tutorial) was discussed. Typical excercises included naming free variables, reducing to normal form, etc.
In order to work with lambda calculus in an explanatory way I built a Lambda-Interpreter which is capable of tracing complete reductions to normal form, α- and η-conversion, and support for user-definable macros - i.e. it is capable of both substituing as well as recognizing known structures in a lamba expression.
Note for Windows users: Since the Windows console does not support UTF-8, some characters may look quirky or may not show up at all. Most prominent characters like λ are translated to similar looking symbols, like “\”. If you do not have the Haskell Platform, there is also a pre-built windows binary available. Use it like this:
The program has been tested using GHC 7 on Mac OS X 10.6, Ubuntu 10.04+, Windows XP, and Windows 7.
Once you fired up the toolbox you can start entering a lambda expression (for clarity user-supplied input is prefixed by “$”, generated output by “>”):
> Welcome to lambda calculus! Type "help" for help. $ (λuab.u(ab))(λnz.n(n(n(z))))(λnz.n(n(z))) > (λuab.u(ab))(λnz.n(n(nz)))(λnz.n(nz))
The program will respond with a canonical version of the expression. You may note that for example “n(z)” has been simplified to “nz”.
We can work with the lambda-expression now, reduce it, analyze it, etc. For example we can substitute known macros:
$ subst > *32
This expression is the multiplication of 3 and 2! Let’s turn it back into a pure lambda expression and reduce it to normal form:
$ expand > (λuab.u(ab))(λnz.n(n(nz)))(λnz.n(nz)) $ trace > (λuab.u(ab))(λnz.n(n(nz)))(λnz.n(nz)) > -β-> (λab.(λnz.n(n(nz)))(ab))(λnz.n(nz)) > -β-> λb.(λnz.n(n(nz)))((λnz.n(nz))b) > -β-> λbz.((λnz.n(nz))b)(((λnz.n(nz))b)(((λnz.n(nz))b)z)) > -β-> λbz.(λz.b(bz))(((λnz.n(nz))b)(((λnz.n(nz))b)z)) > -β-> λbz.b(b(((λnz.n(nz))b)(((λnz.n(nz))b)z))) > -β-> λbz.b(b((λz.b(bz))(((λnz.n(nz))b)z))) > -β-> λbz.b(b(b(b(((λnz.n(nz))b)z)))) > -β-> λbz.b(b(b(b((λz.b(bz))z)))) > -β-> λbz.b(b(b(b(b(bz))))) > ≡ 6 >
“trace” allows us to perform beta reduction until no reduction is possible and see the intermediate steps. Most commands have a shortcut, for trace this is a simple dot: “.”. An alternative to “trace” is “eval” (shortcut “,” – a comma). “eval” will perform the expansion of macros and do a trace - while replacing all known macros in each steps (so the output is shorter and easier to understand).
I leave the exploration of the full program to you, have fun with it!
If you want to comment on this, drop me an e-mail.
Updated: 2012-02-21, 2012-03-09