Quick Start Syntax Options Graph Notation Primitives Usage


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.

Quick Start

  1. Go to the Examples tab,
  2. click on an example hyperlink
  3. go to the Reductions tab,
  4. step through the reductions:


The input language is a curried dialect of Scheme. The following constructs are used:


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.

Graph Notation

The graph contains the following node types:
strategy @ strategy
abstraction \n
variable _n
literal value 1, 2, 3, true, false, 'symbol, '()
pair cons
primitive +, -, *, =, head, tail, if
substitution n->
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.


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: