scravy.net / blog

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.

Get it

The sources are available. After you downloaded the source, run it like this (provided the the Haskell Platform is installed on your system):

runhaskell Lambda.hs

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:

C:\the_folder_you_downloaded_the_binary_to\> LambdaToolbox

The program has been tested using GHC 7 on Mac OS X 10.6, Ubuntu 10.04+, Windows XP, and Windows 7.

Use it

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.

Written: 2012-02-20
Updated: 2012-02-21, 2012-03-09

^