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)|
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 ((x1 v1) ... (x2 v2) (x3 v3) ...) E[x2]) ↦|
|(store ((x1 v1) ... (x2 v2) (x3 v3) ...) E[v2])|
|(store ((x1 v1) ... (x2 v2) (x3 v3) ...) E[(set! x2 v4)]) ↦|
|(store ((x1 v1) ... (x2 v4) (x3 v3) ...) E[v4])|
|(store ((x1 v1) ...) E[(let ((x2 v2)) e)]) ↦|
|(store ((x1 v1) ... (x3 v2)) E[e[x2 := x3]]) where x3 is fresh|
|if e ↦ e' then P[e] → P[e']|
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 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.