Lambda Animator graphically demonstrates a number of
alternative reductions strategies for the λ-calculus.
The strategies call-by-name/value/need control the reduction of arguments.
The strategies substitute-by-name/value/need control the reduction of functions.
Call-by-value and call-by-need are used by eager and lazy languages respectively.
Substitute-by-value and substitute-by-need
are used to implement eager-specialization and lazy-specialization respectively.
- Go to the Examples tab,
- click on an example hyperlink
- go to the Reductions tab,
- step through the reductions:
- use the up/down cursor keys to step through reductions,
- use a left mouse button drag to move the graph
- use a vertical right mouse button drag (or scroll wheel) to zoom in and out.
The input language is a curried dialect of Scheme. The following constructs are used:
( func arg1 ... argn )
application is curried so
( func arg1 arg2 )
has the same meaning as
( ( func arg1 ) arg2 )
- Lambda Abstraction
( lambda ( var1 ... varn ) body )
similarly, abstraction is curried so
( lambda ( var1 var2 ) body )
has the same meaning as
( lambda ( var1 ) ( lambda ( var2 ) body ) )
- Letrec Binding
( letrec ( ( name1 defn1 ) ... ( namen defnn ) ) body )
The letrec keyword introduces mutually recursive bindings.
( quote expr )
The quote keyword quotes data.
( define name defn )
The define keyword introduces top-level definitions, the current definition and all (non-shadowed) previous definitions are visible in the body of the current definition.
a variable referes to the nearest enclosing lambda or letrec bound variable, or if none, the most recent prior definition, and failing that a built-in primitive.
On the input tab, the following options may be set:
A value is a term which will be reduced no further.
Setting the value form controls how far arguments will be reduced when using call-by-value,
how far functions will be reduced when using substitute-by-value,
and how far the whole term is reduced.
- Argument Strategy
- copies the argument including any redexes within the argument.
- reduces the argument to a value, and then either copies or shares it.
- shares the argument, delays reduction until needed.
- Function Strategy
- copies the function body including and redexes within the body.
- reduces the function to a value and then copies the body.
- shares the function body by delaying the substitution of redexes until they are needed.
- Value Form
- a term is in HS if it is an abstraction, variable, pair whose head and tail parts are in HS, literal value, or an irreducible application.
- weak head normal form
- A term is in WHNF if it is an abstraction, variable, pair, literal value, or an irreducible application whose function part is in WHNF.
- weak normal form
- a term is in WNF if it is an abstraction, variable, pair whose head and tail parts are in WNF, literal value, or an irreducible application whose function and argument parts are in WNF.
- head normal form
- a term is in HNF if it is an abstraction whose body is in HNF, variable, pair, literal value, or an irreducible application whose function part is in HNF.
- normal form
- a term is in NF if it contains no reducible expressions.
The graph contains the following node types:
The function and argument strategy is shown to the left and right of applications nodes.
The strategy is either name, value or need.
In the case of value the form of that value can be either HNF or NF for functions,
and one of HS, WHNF, WNF, HNF and NF for arguments.
Lambda bound variables are identified by integers in the graph representation.
The scope of a function body is shown with a rectangular box.
Letrec bound variables are shown as sharing in the graph.
| application || |
|strategy @ strategy|
| abstraction || || \n |
| variable || || _n |
| literal value || || 1, 2, 3, true, false, 'symbol, '() |
| pair || || cons |
| primitive || || +, -, *, =, head, tail, if |
| substitution || || n-> |
The following primitives are supported:
cons, head, tail, car, cdr, if, pair?, null?, equal?, number?, symbol?, +, -, *, =, <, undefined, true, false, seq, hyper-seq, apply-strategy.
To run from the command line, type one of:
Alternatively, copy the JAR file from the website and run:
- javaws http://thyer.name/lambda-animator/sandbox.jnlp
- javaws http://thyer.name/lambda-animator/trusted.jnlp
- java -jar lambda-animator.jar