Lambda calculus reduction workbench

This system implements and visualizes various reduction strategies for the pure untyped lambda calculus. It is intended as a pedagogical tool, and as an experiment in the programming of visual user interfaces using Standard ML and HTML.

Syntax

The letter lambda is written as a backslash `\'; otherwise the syntax is the usual one:

Lambda expression:

        e ::= x                         Variable
           |  (\x.e)                    Abstraction
           |  (e e)                     Application

Abbreviation:  

        b ::= x = e                     Bind e to x

Program:
        p ::= e                         Expression to evaluate
           |  let b1; ...; bn in e      Abbreviations and expression

Syntactically, a variable is a sequence of letters, digits and underscores, starting with a letter. Variables which stand for abbreviations are displayed with a leading dollar sign `$'. Parentheses may be left out; they are reinserted as follows:

        \x.e1 e2        means   (\x.(e1 e2))
        \x1.\x2.e       means   (\x1.(\x2.e))
        e1 e2 e3        means   ((e1 e2) e3)

Nested abstractions \x1.\x2. ... \xn.e may be written \x1 x2 ... xn.e.

Bindings introduce abbreviations for lambda expressions, which must be closed, except for previously defined abbreviations. This example illustrates the use of abbreviations:

	let 
	   S = \f g x. f x (g x);
	   K = \x y. x
	in 
	   S K K

In fact, there are several predefined abbreviations. The lambda reducer will display the predefined abbreviations if you choose `print abbreviations' and click on `Do it'.

Reduction strategies and tracers

The following reduction strategies are implemented:

The following reduction tracers are available:


Peter Sestoft (sestoft@itu.dk) 1996-10-07, 2001-03-31, 2013-01-06