Introduction

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

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.

Syntax

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

Application
( func arg₁ ... arg_n )
application is curried so ( func arg₁ arg₂ ) has the same meaning as ( ( func arg₁ ) arg₂ )
Lambda Abstraction
( lambda ( var₁ ... var_n ) body )
similarly, abstraction is curried so ( lambda ( var₁ var₂ ) body ) has the same meaning as ( lambda ( var₁ ) ( lambda ( var₂ ) body ) )
Letrec Binding
( letrec ( ( name₁ defn₁ ) ... ( name_n defn_n ) ) body )
The letrec keyword introduces mutually recursive bindings.
Quote
( quote expr )
The quote keyword quotes data.
Define
( 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.
Variable
var
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.

Options

On the input tab, the following options may be set:

Argument Strategy

call-by-name
copies the argument including any redexes within the argument.
call-by-value
reduces the argument to a value, and then either copies or shares it.
call-by-need
shares the argument, delays reduction until needed.
Function Strategy

substitute-by-name
copies the function body including and redexes within the body.
substitute-by-value
reduces the function to a value and then copies the body.
substitute-by-need
shares the function body by delaying the substitution of redexes until they are needed.
Value Form

hyper-strict
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.

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:

application
   
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.

Primitives

The following primitives are supported:

cons, head, tail, car, cdr, if, pair?, null?, equal?, number?, symbol?, +, -, *, =, <, undefined, true, false, seq, hyper-seq, apply-strategy.

Usage

To run from the command line, type one of:

javaws http://thyer.name/lambda-animator/sandbox.jnlp
javaws http://thyer.name/lambda-animator/trusted.jnlp

Alternatively, copy the JAR file from the website and run:

java -jar lambda-animator.jar

application		strategy `@` strategy
abstraction		`\n`
variable		`_n`
literal value		`1`, `2`, `3`, `true`, `false`, `'symbol`, `'()`
pair		`cons`
primitive		`+`, `-`, `*`, `=`, `head`, `tail`, `if`
substitution		`n->`