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.

• Start lambda calculus reducer. The lambda calculus reducer scripts now run on a tiny Raspberry Pi Linux server.

• Here is the implementation source code as a zip file.

• There is an old draft report describing the implementation, in PDF (645 KB).

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

• call-by-name
• head spine reduction
• normal order
• call-by-value
• applicative order
• hybrid reduction

The following reduction tracers are available:

• normalize the expression, and count the number of beta reductions
• trace the normalization process, highlighting current redex
• trace the normalization process, marking all redexes and descendants
• singlestep through the normalization process