Why PLT Redex?

In his seminal paper on the relationship among abstract machines, interpreters and the λ-calculus, Plotkin shows that an evaluator specified via an abstract machine defines the same function as an evaluator specified via a recursive interpreter. Furthermore, the standard reduction theorem for a λ-calculus generated from properly restricted reduction relations is also equivalent to this function. As Plotkin indicated, the latter definition is by far the most concise and the easiest to use for many proofs.

e	=	(e e) \| x \| v		((λ (x) e) v) ↦ e[x:=v]	(β_v)
v	=	(λ (x) e) \| f		(f v) ↦ δ(f,v)	(δ_v)

Plotkin

e ↦ e'

e → e'

(v e) → (v e')

e → e'

(e e'') → (e' e'')

Felleisen/Hieb

E = (E e) | (v E) | []

if e ↦ e' then E[e] → E[e']

The box above presents Plotkin's λ-calculus. The top portion defines expressions, values, and the two basic relations (β_v and δ_v). The rules below on the left are his specification of the strategy for applying those two basic rules in a leftmost-outermost manner.

In a 1989 paper, Felleisen and Hieb develop an alternate presentation of Plotkin's λ-calculi. Like Plotkin, they use β_v and δ_v as primitive rewriting rules. Instead of inference rules, however, they specify a set of evaluation contexts. Roughly speaking, an evaluation context is a term with a hole at the point where the next rewriting step must take place. Placing a term in the hole is equivalent to the textual substitution of the hole by the term. The right side of the bottom half of the above figure shows how to specify Plotkin's evaluator function with evaluation contexts.

While the two specifications of a call-by-value evaluator are similar at first glance, Felleisen and Hieb's is more suitable for extensions with non-functional constructs (assignment, exceptions, control, threads, etc).

p	=	(store ((x v) ...) e)
e	=	⋯ as before ⋯ \| (let ((x e)) e) \| (set! x e)
P	=	(store (x v) ... E)
E	=	⋯ as before ⋯ \| (let ((x E)) e) \| (set! x E)

(store ((x₁ v₁) ... (x₂ v₂) (x₃ v₃) ...) E[x₂]) ↦

(store ((x₁ v₁) ... (x₂ v₂) (x₃ v₃) ...) E[v₂])

(store ((x₁ v₁) ... (x₂ v₂) (x₃ v₃) ...) E[(set! x₂ v₄)]) ↦

(store ((x₁ v₁) ... (x₂ v₄) (x₃ v₃) ...) E[v₄])

(store ((x₁ v₁) ...) E[(let ((x₂ v₂)) e)]) ↦

(store ((x₁ v₁) ... (x₃ v₂)) E[e[x₂ := x₃]]) where x₃ is fresh

if e ↦ e' then P[e] → P[e']

The figure just above shows how easy it is to extend the system of the first figure (right) with assignable variables. Each program now contains a store and an expression. The bindings in the store introduce the mutable variables and bind free variables in the expression. When a dereference expression for a store variable appears in the hole of an evaluation context, it is replaced with its value. When an assignment with a value on the right-hand side appears in the hole, the let-bindings are modified to capture the effect of the assignment statement. The entire extension consists of three rules, with the original two rules included verbatim. Felleisen and Hieb also showed that this system can be turned into a conventional context-free calculus like the λ-calculus.

Context-sensitive term-rewriting systems are ideally suited for proving the type soundness of programming languages. Wright and Felleisen showed how this works for imperative extensions of the λ-calculus and a large number of people have adapted the technique to other languages since then, including Guha, Saftoiu and Krishnamurthi who show how to use a reduction semantics for JavaScript and Flatt, Krishnamurthi, and Felleisen, who show how to use a reduction semantics for Java.

Not surprisingly, though, as researchers have modelled more and more complex languages with these systems, they have found it more and more difficult to model them accurately. To help with this problem, we designed PLT Redex, a domain-specific language for developing and debugging such systems. The language is an extension of Racket, and programmers can escape to this host language if they so wish. Redex comes with an IDE (DrRacket) and with visualization tools.