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.
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'.
The following reduction tracers are available: