lambda evaluator

This lambda evaluator will allow you to write lambda terms and evaluate (that is, normalize) them, and inspect the results. (This won't work in Racket, because Racket doesn't even try to represent the internal structure of a function in a human-readable way.)

Lambda terms: lambda terms are written with a backslash, thus: ((\x (\y x)) z).

If you click "Normalize", the system will try to produce a normal-form lambda expression that your original term reduces to (~~>). So ((\x (\y x)) z) reduces to (\y z).

Let: in order to make building a more elaborate set of terms easier, it is possible to define values using let. In this toy system, lets should only be used at the beginning of a file. If we have, for intance,

let true = (\x (\y x)) in
let false = (\x (\y y)) in
((true yes) no)

the result is yes.

Comments: anything following a semicolon to the end of the line is ignored. Blank lines are fine.

Abbreviations: In an earlier version, you couldn't use abbreviations. \x y. y x x had to be written (\x (\y ((y x) x))). We've upgraded the parser though, so now it should be able to understand any lambda term that you can.

Constants: The combinators S, K, I, C, B, W, T, M (aka ω) and L are pre-defined to their standard values. Also, integers will automatically be converted to Church numerals. (0 is \s z. z, 1 is \s z. s z, and so on.)

Variables: Variables must start with a letter and can continue with any sequence of letters, numbers, _, -, or /. They may optionally end with ? or !. When the evaluator does alpha-conversion, it may change x into x' or x'' and so on. But you should not attempt to use primed variable names yourself.

let true = \x y. x in let false = \x y. y in let and = \l r. l r false in ( (and true true yes no) (and true false yes no) (and false true yes no) (and false false yes no) ) do eta-reductions too

Under the hood

The interpreter is written in JavaScript and runs inside your browser. So if you decide to reduce a term that does not terminate (such as ((\x (x x)) (\x (x x)))), it will be your browser that stops responding, not the wiki server.

The main code is here. Suggestions for improvements welcome.

The code is based on:

Chris Barker's JavaScript lambda calculator
Oleg Kiselyov's Haskell lambda calculator.
The top-down JavaScript lexer and parser at http://javascript.crockford.com/tdop/index.html.

Improvements we hope to add:

detecting some common cases of non-normalizing terms (the problem of determining in general whether a term will normalize is undecidable)
returning results in combinator form (the evaluator already accepts combinators as input)
displaying reductions one step at a time
specifying the reduction order and depth
allow other binders such as ∀ and ∃ (though these won't be interpreted as doing anything other than binding variables)

Other Lambda Evaluators/Calculutors

Peter Sestoft's Lambda Calculus Reducer: Very nice! Allows you to select different evaluation strategies, and shows stepwise reductions.
Chris Barker's Lambda Tutorial
Penn Lambda Calculator: Pedagogical software developed by Lucas Champollion, Josh Tauberer and Maribel Romero. Linguistically oriented. Requires installing Java (Mac users will probably already have it installed).
Mike Thyer's Lambda Animator: Graphical tool for experimenting with different reduction strategies. Also requires installing Java, and Graphviz.
Matt Might's Lambda Evaluator in Scheme (R5RS and Racket).