It was written as a teaching tool, and allows you to reduce lambda expressions one step at a time. It can automatically choose a reduction and explain it to you, or you can manually choose the reduction to apply and the subexpression to which to apply it (by selecting with the mouse).
It's written in the latest and greatest technology for the time: a Java 1.1 application. I just gave it a shot on OpenJDK 1.7, and it (mostly) works, although it does crash occasionally. The write-up is available in PDF form at LambdaThesis.pdf. It's overlong, but provides a reasonable overview of Lambda Calculus for anyone who is interested.
Running the Interpreter
In order to run it, download LambdaTeacher.zip and unzip it (this stuff is so old that compressed JAR files weren't well supported at the time). In order to run it, install Java and execute:
java -cp LambdaTeacher.jar LambdaTeacher
(Note that the switch is -cp, not -jar ; JAR manifests didn't exist at the time). After executing it, you can use the file menu to open defines.jar to load all the bindings.
How It Works
(Note: this section is copied verbatim from a 13 year old web-page, so you can chuckle at historical details)
This interpreter uses string (as opposed to graph) reduction, and as such is very slow. On my Pentium 233, fibonacci two takes about 20 seconds to evaluate (2013 note: it's instantaneous on my 6 core Xeon with 32GB RAM ☺). It does this so the user can reduce one step at a time, and get a feel for different reduction orders.
- Name capture detection. When a name clash is detected, it will prompt the user to type in a new name.
- Any reduction order can be attempted. It has buttons for normal and applicative order. Other sub-expressions for reduction can be selected using a sub-expression selection dialog, where the expression to be reduced is clicked on.
- All reductions are explained in explanation dialog boxes as they are performed.
- Names can be bound to Lambda expressions, using let <name> = <expression>. Names aren't removed during a reduction unless the expression they refer to is modified in any way. Users can select names for removal at any time.
- Files with definitions (name - expression bindings using the let syntax) can be read in.
- Error messages for invalid expressions - it attempts to tell you (kind of) where the expression went wrong. If you are reading in a file, it tells you what line the problem occured on.
- Single threaded. This means that while interpreting, you can't interact with the current application. If you give the interpreter a large or non-terminating expression, you'll have to kill it (Control C on the Java console should do the trick). I know this isn't user friendly, but if you're learning lambda calculus, you should be able to kill a looping process.
SyntaxThe syntax is:
<Prog> ::= <Expr> | let <Variable> = <Expr>
<Expr> ::= <Variable>
| \ <Variable> . <Expr>
| ( <Expr> )
| <Expr1> <Expr2>
<Variable> ::= Any string of letters.
<Number> ::= Any integer.