An Introduction to Redex with Abstracting Abstract Machines (v0.6)

David Van Horn <dvanhorn@cs.umd.edu>

Last updated: Monday, May 4th, 2020

1 Introduction

This is a “living” artifact: please submit bug reports and pull requests whenever you spot problems in this document. https://github.com/dvanhorn/redex-aam-tutorial/

This article provides a brief introduction to the Redex programming language for semantic modelling. It does so by developing several semantic models of a simple programming language and then showing how to construct a program analyzer for this language using the “Abstracting Abstract Machines” method (Van Horn and Might 2010).

So this tutorial aims to accomplish two goals:

• (1) to introduce semantic engineers (programming language researchers, language designers and implementors, analysis and tool builders, etc.) to the Redex programming language;

• (2) to demonstrate the method of building abstract interpreters known as AAM.

You could read this tutorial for either purpose. If you want to learn Redex, this tutorial will build a bunch of standard semantic systems: reduction relations, type judgments, evaluators, machines, and finally a program analyzer. If you want an explicit and approachable introduction to the AAM method, this tutorial will walk you through a detailed construction.

1.1 What is Redex?

Redex (Felleisen et al. 2009) is a scripting language and set of associated tools supporting the conception, design, construction, and testing of semantic systems such as programming languages, type systems, program logics, and program analyses. As a scripting language, it enables an engineer to create executable specifications of common semantic elements such as grammars, reduction relations, judgments, and metafunctions; the basic elements of formal systems. It includes a number of software engineering inspired features to make models robust and includes tools for typesetting models and generating algebraic steppers for exploring program behaviors. In brief, Redex supports all phases of the semantic engineering life-cycle.

For an excellent talk motivating Redex, see the video of Robby Findler’s Run Your Research talk at POPL 2012  (Klein et al. 2012).

I have used Redex since its first release and it has played a critical role in several of my research projects. It has allowed me to rapidly explore new ideas, hypothesize claims, and—typically—refute these claims and refine the ideas. In some cases, Redex has eased the development of research; I can go from idea to result much faster and more effectively than I could without Redex. In other cases, using Redex has illuminated problems I did not know existed, leading to new results and research. But in other cases, I simply could not have accomplished my research without Redex.

Redex has become such an integral tool in my research that I cannot imagine my research path without it. It has changed the way I approach and think about problems.

1.2 What is Abstracting Abstract Machines?

Abstracting Abstract Machines (or AAM, for short) is a method for systematically constructing sound program analyzers. The central idea is that a programming language’s semantics can be transformed, by a simple turn-the-crank construction, into an analysis for soundly reasoning about programs written in that language. It has been used to analyze a number of language features often considered beyond the pale of existing analysis approaches. A key advantage of the approach is that ideas from programming language design and implementation can be directly imported and applied to the design and implementation of abstract interpreters.

1.3 Prerequisites

This tutorial assumes you have some experience with programming language semantic artifacts such as grammars, reduction relations, evaluation relations, typing judgments. If you have never seen these before, you should probably start with a graduate PL text book (e.g. (Felleisen et al. 2009)). It does not assume you have a background in program analysis or abstract interpretation.

This tutorial also assumes you have some experience with programming in a Lisp-like language. In particular, you should be comfortable with the concepts behind quote, quasiquote, and unquote. Having programmed with pattern matching would also help.

You will need Racket, which is very easy to install and works on all major operating systems. At the time of writing, version 6.9 is the latest release.

You can download the source code for this tutorial here: https://github.com/dvanhorn/redex-aam-tutorial/archive/master.zip.

2 Warmup

Redex, at its core, is a language for defining and operating on s-expressions that is equiped with a powerful pattern matching mechanism.

To follow along with this tutorial, you must ‘(require redex)‘ immediately below your ‘#lang racket‘ definition in DrRacket.

An s-expression is a potentially nested piece of data that may include numbers, booleans, symbols, and lists of s-expressions. Before getting in to how to model semantics with Redex, let’s just play with some simple examples.

If you’ve ever programmed with a language in the LISP family, you can first think of term as being synonymous with quote.

A language is a set of s-expressions, defined by the define-language form. For example:

> (define-language L     (M ::= N F (M ...))     (F ::= fred wilma)     (N ::= 2 7))

This defines the language L. The language L is inductively defined as the smallest set such that 2, 7, fred, and wilma are in L, and if some values x0 through xn are in L, then the list containing x0 through xn is in L.

The use of capital letters for non-terminals is just a convention I follow and not a requirement of Redex.

The definition of L takes the familiar form of a BNF-like grammar. The “...” postfix operator indicates zero or more repetitions of the preceding pattern.

In addition to L, this grammar also carves out subsets of L defined by the non-terminals of the grammar, namely M, F, and N. The non-terminal names are significant because they become pattern variables which can be used to match against elements of the language.

We can also define functions on terms, called metafunctions using the define-metafunction form. A metafunction is given by an ordered sequence of pattern and template clauses. For example, here is a function that swaps occurrences of fred and wilma:

> (define-metafunction L     swap : M -> M     [(swap fred) wilma]     [(swap wilma) fred]     [(swap (M ...)) ((swap M) ...)]     [(swap M) M])

There are two imporant things to notice in this example: (1) the clauses of metafunction definitions are ordered, so the last clause matches only if the first three do not; (2) the use of “...” can also occur on the right-hand side of clauses, so the third clause distributes the swap call to all of the elements of the list.

It’s important to note that metafunction exist within Redex terms and are not functions in the host language. Refering to metafunctions outside of term causes a syntax error:

> (swap wilma)

eval:20:0: swap: illegal use of syntax

in: (swap wilma)

value at phase 1: #<term-fn>

Now that we have seen the basics, we can move on to a real example.

3 PCF

Let’s start by building a model of a very simple, typed functional programming language based on the PCF language (Plotkin 1977). Although simple, PCF contains all the essential elements of a real programming language. Scaling the approach of these notes up to a more sophisticated language is just a small matter of semantic hacking.

PCF is a core typed functional programming language. For values, it includes natural numbers, functions, and primitive operations. Terms include variables, values, applications, conditionals, and recursive functions.

> (define-language PCF     (M ::=        N O X L        (μ (X : T) L)        (M M ...)        (if0 M M M))     (X ::= variable-not-otherwise-mentioned)     (L ::= (λ ([X : T] ...) M))     (V ::= N O L)     (N ::= number)     (O ::= O1 O2)     (O1 ::= add1 sub1)     (O2 ::= + *)     (T ::= num (T ... -> T)))

Greek symbols: you can enter Greek symbols in the DrRacket IDE by typing many common LaTeX commands followed by Control-\ (in OS X). For example “\sigma” plus Control-\ will enter “σ”. To make things easier, you can type a unique prefix, so “\sig” plus Control-\ will also enter a “σ” as well.

Compared with the warmup example, there’s really not much to point other than the use of variable-not-otherwise-mentioned, which is just a shorthand way of saying what’s not a variable name; in particular, any symbol mentioned in the grammar cannot be a variable name, so for example λ, μ, if0, :, etc., cannot be used as variable names. (Had we just used variable instead of variable-not-otherwise-mentioned, nothing would break (yet), but it would be ambiguous as to whether some expressions were applications or lambda abstractions. Down the line, that probably will break some of the claims we expect to hold on the language.)

One thing that is missing from the grammar is the requirement that λ-bound variables are distinct. We could express this side condition in the grammar, but instead we’ll defer this requirement to the typing judgment (which we’ll see next).

As an example PCF program, here is a program that computes the factorial of 5:

> (define-term fact-5     ((μ (fact : (num -> num))         (λ ([n : num])           (if0 n                1                (* n (fact (sub1 n))))))      5))

(The define-term form is way to bind a name interpreted within term.)

3.1 Typing judgement

Let’s now define a typing relation for PCF programs. The typing relation will, as usual, be defined in terms of a typing environment, which is missing from the PCF grammar. Rather than revising the grammar, we can define a language extension as follows:

> (define-extended-language PCFT PCF     (Γ ::= ((X T) ...)))

The PCFT language includes everything in the PCF language, plus a notion of type environments Γ, which are sequences of variable and type pairs. (Language extensions can also replace or augment existing non-terminals, as we’ll see later.)

Let’s first take a detour to develop some useful, general purpose helper functions.

Association lists, like Γ, come up again and again, so let’s define a few operations for them. Since association lists are more general than type environments, we’ll want to define generic versions of this operations. In order to be generic, we should only use the built-in patterns of Redex and not the metavariables of languages we define. To accomodate this, we first define the language of built-in patterns:

> (define-language REDEX)

This definition introduces no non-terminals, so it includes only the built-in patterns like number, variable, ..., etc. When we define generic operations, we will define them in the language of REDEX.

First, let’s write a straightforward recursive judgment form that relates a given key to all its associations:

> (define-judgment-form REDEX     #:mode (lookup I I O)     #:contract (lookup ((any any) ...) any any)     [(lookup (_ ... (any any_0) _ ...) any any_0)])

This relation makes use of the any pattern, which ranges over all values. It also uses the _ pattern, which like any, will match anything, but unlike any it is not a binder and therefore (1) it cannot be used on the right hand side and (2) multiple occurrences of _ on the left hand side are not constrained to match the same thing.

The clause uses a non-linear pattern to require a binding to match the given key (notice the two left-hand occurrences of any).

> (judgment-holds (lookup ((x 1) (y 2) (x 3)) x 1))

#t

> (judgment-holds (lookup ((x 1) (y 2) (x 3)) x 2))

#f

> (judgment-holds (lookup ((x 1) (y 2) (x 3)) x 3))

#t

> (judgment-holds (lookup ((x 1) (y 2) (x 3)) x any) any)

'(1 3)

In addition to looking up an association, we need an operation to extend an association list. A simple definition that allows for an association to be extended with an arbitrary number of key-value pairs is then:

> (define-metafunction REDEX     ext1 : ((any any) ...) (any any) -> ((any any) ...)     [(ext1 (any_0 ... (any_k any_v0) any_1 ...) (any_k any_v1))      (any_0 ... (any_k any_v1) any_1 ...)]     [(ext1 (any_0 ...) (any_k any_v1))      ((any_k any_v1) any_0 ...)])

> (define-metafunction REDEX     ext : ((any any) ...) (any any) ... -> ((any any) ...)     [(ext any) any]     [(ext any any_0 any_1 ...)      (ext1 (ext any any_1 ...) any_0)])

The ext metafunction overrides an existing association, if there is one; otherwise it prepends the new association to the list.

Lastly, we will want to assert that λ-bound variables are unique, so let’s define a unique predicate, which holds when its arguments are distinct:

> (define-metafunction REDEX     unique : (any ...) -> boolean     [(unique (any_!_1 ...)) #t]     [(unique (_ ...)) #f])

This defines a unique metafunction that takes a list of any number of elements and produces #t when they are unique and #f otherwise. This uses a new kind of pattern, which uses the _! naming prefix. The meaning of this pattern is that repeated uses of it must be distinct, thus any_!_1 ... matches disjoint sequences.

> (term (unique ()))

#t

> (term (unique (1)))

#t

> (term (unique (1 2)))

#t

> (term (unique (1 2 3 2)))

#f

There is a kind of short-hand for defining predicates (metafunctions that produce either true or false), called, confusingly enough, define-relation:

> (define-relation REDEX     unique ⊆ (any ...)     [(unique (any_!_1 ...))])

With these generic operations in place, we can now define the typing relation “⊢”:

> (define-judgment-form PCFT     #:mode (⊢ I I I O)     #:contract (⊢ Γ M : T)     [(lookup Γ X T)      -------------- var      (⊢ Γ X : T)]     [------------- num      (⊢ Γ N : num)]     [----------------------- op1      (⊢ Γ O1 : (num -> num))]     [--------------------------- op2      (⊢ Γ O2 : (num num -> num))]     [(⊢ Γ M_1 : num)      (⊢ Γ M_2 : T)      (⊢ Γ M_3 : T)      --------------------------- if0      (⊢ Γ (if0 M_1 M_2 M_3) : T)]     [(⊢ (ext Γ (X T)) L : T)      ----------------------- μ      (⊢ Γ (μ (X : T) L) : T)]     [(⊢ Γ M_0 : (T_1 ..._1 -> T))      (⊢ Γ M_1 : T_1) ...      ----------------------- app      (⊢ Γ (M_0 M_1 ..._1) : T)]     [(unique (X ...))      (⊢ (ext Γ (X T) ...) M : T_n)      ------------------------------------------ λ      (⊢ Γ (λ ([X : T] ...) M) : (T ... -> T_n))])

The define-judgment-form specifies a relation. Conceptually, a relation in Redex is a function from inputs to sets of outputs and the definition of a relation must specify which positions of the relation are inputs and which are outputs, as seen in the #:mode spec. This relation has three inputs (although the last one is always the constant “:” to make the form easier to read) and one output. The two real inputs are the type environment and term; the output is the type. The #:contract annotation specifies the signature of the relation.

A relation is specifed by a number of clauses. Each clause has some number of hypotheses (calls to this or other judgments) and side conditions (noted with where), followed by a line, an optional name, and a conclusion. Unlike metafunctions, the clauses are unordered and therefore may overlap.

Judgments must be “well-moded”. If some variable appears in an output position of a conclusion but cannot be determined based on inputs or outputs of hypotheses, a static error will be signalled.

Judgments can be used either with the judgment-holds form or from other judgment definitions or metafunctions. The judgment-holds form works as follows:

> (judgment-holds (⊢ () (λ ([x : num]) x) : (num -> num)))

#t

This use specifies a type (num -> num) and verifies this type is in the typing relation.

Alternatively, we can use a metavariable in the type position in order to compute all of the types this term has. This metavariable is bound to these types in the scope of the following term which, in this case is just T. Consequently the result is the list of types for this program.

> (judgment-holds (⊢ () (λ ([x : num]) x) : T) T)

'((num -> num))

> (judgment-holds (⊢ () fact-5 : T) T)

'(num)

It’s possible to illustrate judgments as follows:

> (show-derivations    (build-derivations     (⊢ () (λ ([x : num]) (add1 x)) : T)))

We can verify that ill-formed lambda-abstractions have no type:

> (judgment-holds (⊢ () (λ ([x : num] [x : num]) x) : T) T)

'()

Enough types, let’s calculate!

3.2 The calculus of PCF

To calculate with PCF programs, we start by formulating a reduction relation that captures the axioms of reduction for PCF:

> (define r     (reduction-relation      PCF #:domain M      (--> (μ (X : T) M)           (subst (X (μ (X : T) M)) M)           μ)         (--> ((λ ([X : T] ...) M_0) M ...)           (subst (X M) ... M_0)           β)         (--> (O N_0 ...) N_1           (judgment-holds (δ (O N_0 ...) N_1))           δ)         (--> (if0 0 M_1 M_2) M_1 if-t)      (--> (if0 N M_1 M_2) M_2           (side-condition (not (zero? (term N))))           if-f)))

A reduction relation defines a binary relation on terms in a given domain, in this case terms M. A reduction relation is defined by a number of clauses, noted with -->, which consist of a left-hand side, a right-hand side, any number of side conditions, and optional name. The order of clauses is irrelevant and like judgments, clauses may overlap.

Even though reduction relations are relations, and conceptually can be thought of as a judgment with #:mode (r I O) and #:contract (r M M), they are considered different from Redex’s point of view and support different operations.

This definition relies on two auxilary definitions: a δ relation for interpreting primitive operations and a subst metafunction which implements substitution.

> (define-judgment-form PCF     #:mode (δ I O)     #:contract (δ (O N ...) N)     [(δ (+ N_0 N_1) ,(+ (term N_0) (term N_1)))]     [(δ (* N_0 N_1) ,(* (term N_0) (term N_1)))]     [(δ (sub1 N) ,(sub1 (term N)))]     [(δ (add1 N) ,(add1 (term N)))])

Note that this judgment omits the horizontal lines, which are in fact optional (but conclusions precede hypotheses when omitted; of course it makes no difference when there are no hypotheses as is the case with δ). It also uses unquote, written “,” to escape out of Redex and into Racket. Thus the interpration of PCF’s + is given by Racket’s + function, and likewise for the rest of the operations.

> (require redex-aam-tutorial/subst)

> (term (subst (x 5) (y 7) (+ x y)))

'(+ 5 7)

The second example shows that apply-reduction-relation only takes one step of computation since clearly (add1 5) can reduce further. The third example shows that reduction can only occur at the outermost term; despite having multiple redexes inside the term, the term itself does not reduce.

Of course, the reflexive, transitive closure of r, which is what apply-reduction-relation* computes, still does not enable reductions within terms, so the last example does not reduce.

We could define another reduction relation which incorporates progress rules. Alternatively, we can use operations to compute such a relation from r:

> (compatible-closure r PCF M)

#<reduction-relation>

This example of the compatible-closure operation computes a new relation that allows r to be applied anywhere within a term M:

> (define -->r (compatible-closure r PCF M))

> (apply-reduction-relation* -->r (term ((λ ([x : num]) x) (add1 5))))

'(6)

> (apply-reduction-relation* -->r (term (sub1 ((λ ([x : num]) x) (add1 5)))))

'(5)

It’s also possible to visualize each step of reduction using the traces function, which launches a window showing each path of reduction. For example:

> (traces -->r (term ((λ ([x : num]) x) (add1 5))))

produces:

Notice that the traces window visualizes all possible reduction sequences.

3.3 Call-by-value and call-by-name: Strategies, contexts, and axioms

It is possible to consider reduction strategies which fix a deterministic order to reductions. One way to represent such a strategy is to define a grammar of evaluation contexts that restrict where the reduction relation r may be applied.

Now using context-closure, we can compute a relation that does the left-most, outer-most call-by-name reduction.

> (define -->n     (context-closure r PCFn E))

> (traces -->n (term ((λ ([x : num]) x) (add1 5))))

Unlike -->r, we can use -->n to calculate fact-5:

> (apply-reduction-relation* -->n (term fact-5))

'(120)

While we can’t use apply-reduction-relation* to compute fact-5 with -->r, we can test -->r with test-->>∃, which tests for reachability:

> (test-->>∃ -->r (term fact-5) 120)

Why doesn’t (apply-reduction-relation* -->r (term fact-5)) produce an answer?

In addition to call-by-name, we can also characterize left-most, outer-most call-by-value reduction with the following strategy and a restriction of the β axiom:

> (define-extended-language PCFv PCF     (E ::= hole        (V ... E M ...)        (if0 E M M)))

> (define v     (extend-reduction-relation      r PCF #:domain M      (--> ((λ ([X : T] ...) M_0) V ...)           (subst (X V) ... M_0)           β)))

> (define -->v     (context-closure v PCFv E))

Notice that v is defined as an extended-reduction-relation of r. An extension of a reduction relation can add additional reduction cases or override existing ones, as is the case here, by providing a new rule with the same name as an existing one.

Like -->n, the -->v relation defines a deterministic reduction strategy, but it differs from -->n in where it reduces and what it reduces:

> (traces -->v (term ((λ ([x : num]) x) (add1 5))))

If the relations -->n and -->v produce answers, they are consistent with each other, but the -->n relation produces more answers than -->v as the following examples demonstrate:

> (define-term Ω     ((μ (loop : (num -> num))         (λ ([x : num])           (loop x)))      0))

> (apply-reduction-relation* -->n (term ((λ ([x : num]) 0) Ω)))

'(0)

> (apply-reduction-relation* -->v (term ((λ ([x : num]) 0) Ω)))

'()

These examples also show that Redex terminates, even when the reduction of a term has a cycle in it.

3.4 Evaluation

As an alternative to the reduction-based approach of the previous subsection, computation is often characterized by a compositional evaluation function. This approach avoids substitution and instead represents substitutions lazily with a closure, which is a term paired with an environment mapping variable names to values:

> (define-extended-language PCF⇓ PCF     (V ::= N O (L ρ) ((μ (X : T) L) ρ))     (ρ ::= ((X V) ...)))

Like type environments, value environments are instances of association lists, so we will use the generic lookup and ext operations.

The evaluation function ⇓ can now be defined as a judgment as follows:

> (define-judgment-form PCF⇓     #:mode (⇓ I I I O)     #:contract (⇓ M ρ : V)        [(⇓ N ρ : N)]     [(⇓ O ρ : O)]     [(⇓ L ρ : (L ρ))]     [(⇓ (μ (X_f : T_f) L) ρ : ((μ (X_f : T_f) L) ρ))]        [(lookup ρ X V)      --------------      (⇓ X ρ : V)]        [(⇓ M_0 ρ : N)      (where M ,(if (zero? (term N)) (term M_1) (term M_2)))      (⇓ M ρ : V)      ---------------------------      (⇓ (if0 M_0 M_1 M_2) ρ : V)]        [(⇓ M_0 ρ : O)      (⇓ M_1 ρ : N)      ...      (δ (O N ...) N_1)      -----------------------      (⇓ (M_0 M_1 ...) ρ : N_1)]        [(⇓ M_0 ρ : ((λ ([X_1 : T] ...) M) ρ_1))      (⇓ M_1 ρ : V_1)      ...      (⇓ M (ext ρ_1 (X_1 V_1) ...) : V)      -----------------------------------      (⇓ (M_0 M_1 ...) ρ : V)]        [(⇓ M_0 ρ : (name f ((μ (X_f : T_f) (λ ([X_1 : T] ...) M)) ρ_1)))      (⇓ M_1 ρ : V_1)      ...      (⇓ M (ext ρ_1 (X_f f) (X_1 V_1) ...) : V)      -----------------------------------------      (⇓ (M_0 M_1 ...) ρ : V)])

We can use it to compute examples:

> (judgment-holds (⇓ fact-5 () : V) V)

'(120)

3.5 A brief aside on the caveats of language extensions

Redex, as we’ve seen, has some powerful features to support extension, and this tutorial uses them, well, extensively. However, there are some gothchas worth being aware of.

One of the most prominent gotchas is the mixing of reduction relation extensions and metafunctions (or relations).

When a reduction relation is extended, the original relation is reinterpreted over the new language; thus the original pattern variables of the original definition may take on new meaning. So for example, consider this simple language and reduction relation:

> (define-language L0 (M ::= number))

> (define r0 (reduction-relation L0 (--> M 5)))

> (apply-reduction-relation r0 (term 7))

'(5)

Suppose we then extend L0 by overriding the meaning of M to include strings:

> (define-extended-language L1 L0 (M ::= .... string))

We can create an extension of r0 that is the reinterpretation of r0 over this new meaning of M:

> (define r0′ (extend-reduction-relation r0 L1))

This works just fine and r0′ reduces as expected when applied to strings:

> (apply-reduction-relation r0′ "seven")

'(5)

However, let’s consider an alternative, seemingly equivalent development of the base relation that involves a metafunction:

> (define-metafunction L0     to-five : M -> M     [(to-five M) 5])

> (define r1 (reduction-relation L0 (--> M (to-five M))))

> (apply-reduction-relation r1 (term 7))

'(5)

> (define r1′ (extend-reduction-relation r1 L1))

You might expect that the extension of r1 to L1 would also reinterpret the definition of to-five, but it does not. Consequently, applying r1′ to a string results in a run-time domain error from applying to-five to a string:

> (apply-reduction-relation r1′ "seven")

to-five: (to-five "seven") is not in my domain

Relaxing the contract on to-five is no help either; using a more relaxed contract such as any -> any would shift the error to a failure to match since the M in the definition of to-five is still an M in L0 and thus doesn’t match strings.

But isn’t there a mechanism for extending metafunctions? Yes. There is define-metafunction/extension, which allows you to define a L1 compatible version of to-five:

> (define-metafunction/extension to-five L1     to-five/L1 : M -> M)

> (term (to-five/L1 "seven"))

5

This defines a new metafunction, to-five/L1, which reinterprets the definition of to-five over L1. (We could aslo have added clauses to this definition, which are conceptually prepended to those of to-five, but there’s no need in this case.) However, this has no effect on the original definition of to-five, which is what is used within r1 and its extension r1′. So the problem remains.

We could have used to-five/L1 in the original definition of r1, but this puts the cart before the horse since we have to anticipate all extensions before writing the base relation.

We could have named and then overridden this case of the relation in r1′, but this just subverts the original goal of extension, which is to enable a single point of control; this approach duplicates code and inflicts all the problems that follow.

The approach we take in this tutorial is to avoid all language-specific metafunction, relations, and judgments when defining reduction relations. We use instead only metafunctions, relations, and judgments that are either (1) defined only in terms of Redex’s built in patterns (for example, lookup, ext, and unique); or (2) defined only for some subset of the language which doesn’t change in extensions (for example, δ). It is a compromise, but short of better extension mechanisms in Redex, it seems to be a reasonable practice.

3.6 Explicit substitutions

As an intermediary between the compositional evaluation function based on value environments and closures and the reduction system based on substitution, we can also formulate computation as a reduction system based on environments that is substitution-free. Such a reduction semantics is known as an explicit substitution semantics since the meta-theoretic notion of substitution is represented explicitly in the system (Abadi et al. 1991).

> (define-extended-language PCFρ PCF⇓     (C ::= V (M ρ) (if0 C C C) (C C ...))     (E ::= hole (V ... E C ...) (if0 E C C)))

Values are just as in the PCF⇓ language, but closures are generalized to either terms with environments, or conditionals or applications with closure sub-terms. The reduction relation is now defined on the domain of closures:

> (define vρ     (reduction-relation      PCFρ #:domain C      (--> ((if0 M ...) ρ) (if0 (M ρ) ...) ρ-if)      (--> ((M ...) ρ) ((M ρ) ...) ρ-app)      (--> (O ρ) O ρ-op)      (--> (N ρ) N ρ-num)      (--> (X ρ) V           (judgment-holds (lookup ρ X V))           ρ-x)         (--> (((λ ([X : T] ...) M) ρ) V ...)           (M (ext ρ (X V) ...))           β)         (--> ((name f ((μ (X_f : T_f) (λ ([X : T] ...) M)) ρ)) V ...)           (M (ext ρ (X_f f) (X V) ...))           rec-β)         (--> (O V ...) V_1           (judgment-holds (δ (O V ...) V_1))           δ)         (--> (if0 0 C_1 C_2) C_1 if-t)      (--> (if0 N C_1 C_2) C_2           (side-condition (not (equal? 0 (term N))))           if-f)))

The ρ-if and ρ-app rules distribute environments to sub-terms of conditionals and applications, respectively. The ρ-op and ρ-num rules drop needless environments from primitives and numbers. The ρ-x rule looks up the value of a variable in an environment. The remaining cases are straightforward adaptations of the v relation to the domain of closures.

> (define -->vρ     (context-closure vρ PCFρ E))

One of the nice properties of this explicit substitution formulation is that we don’t need a substitution metafunction, which is good since substitution is both tedious to write and easy to get wrong.

3.7 Eval/Continue/Apply machine

Explicit substitutions explicate the handling of variable bindings and take a principled step from a theoretical calculus toward a realistic language implementation. But the -->vρ relation of the previous section still leaves implicit the process of decomposing a program into an evaluation context and a redex, then plugging the contractum back into the context to obtain the new state of the program. In this section, we develop a stack machine that makes explicit the mechanism for finding redexes, thus eliminating the need for the context-closure operation.

> (define-extended-language PCFς PCFρ     (F ::= (V ... [] C ...) (if0 [] C C))     (K ::= (F ...))     (S ::= ; serious terms S ∩ V = ∅, C = S ∪ V        (N ρ)        (O ρ)        (X ρ)        ((M M ...) ρ)        ((if0 M M M) ρ)        (if0 C C C)        (C C ...))     (ς ::= (C K) V))

We start by formulating a representation of the context. An evaluation context will be represented as a continuation: a list of frames, where a frame is a single flat evaluation context, i.e. either a conditional or application context with no nested evaluation context inside (the hole will be represented by []). Conceptually, the continuation is a stack of actions that remain to be done. It’s also easy to see that continuations and evaluation contexts are inter-convertible: the inner-most part of an evaluation context is the first frame of a continuation; the outer-most part of the context corresponds to the final frame of a continuation; an empty context is represented by an empty list of frames.

Computation is defined over the domain of states, which are closures paired with a continuation; the final state of a computation is just a value.

The transitions of this machine break down into three categories: apply transitions, which actually perform closure reduction; eval transitions, which push actions on to the continuation; and continue transitions which pop actions of the continuation and search for the next redex.

In order to determine when a frame should be pushed on the stack, we define a category of serious terms S, which are non-value closures. If a conditional or application contains a serious term, a frame is pushed. If the closure component of the state is a value, the top frame is popped and the value is plugged into its hole; if the stack is empty, the value is the final result of the computation. If the closure component is a redex, it is reduced using vρ.

The apply transitions are obtained by lifting vρ to operate on states; here we use the (context-closure vρ PCFς (hole K)) to obtain this relation. The eval and continue transitions are straightforward and make explicit as reductions what context-closure computes.

> (define -->vς     (extend-reduction-relation      ; Apply      (context-closure vρ PCFς (hole K))      PCFς      ; Eval      (--> ((if0 S_0 C_1 C_2) (F ...))           (S_0 ((if0 [] C_1 C_2) F ...))           ev-if)         (--> ((V ... S C ...) (F ...))           (S ((V ... [] C ...) F ...))           ev-app)         ; Continue      (--> (V ()) V halt)         (--> (V ((if0 [] C_1 C_2) F ...))           ((if0 V C_1 C_2) (F ...))           co-if)         (--> (V ((V_0 ... [] C_0 ...) F ...))           ((V_0 ... V C_0 ...) (F ...))           co-app)))

Again, we define an injection into initial configurations:

> (define-metafunction PCFς     injς : M -> ς     [(injς M) ((injρ M) ())])

We can verify the machine computes the expected results:

> (apply-reduction-relation* -->vς (term (injς fact-5)))

'(120)

If we examine the reduction graph for a program, what we see is that the graph for a -->vς computation is just like -->vρ computation, but with more transitions corresponding to the decomposition and recomposition of programs into evaluation contexts and redexes.

> (traces -->vς (term (injς ((λ ([x : num]) x) (add1 5)))))

3.8 Heap-allocated bindings

In order to model imperative features such as references, arrays, or mutable variables—or even just to give an object-level account of memory allocation, rather than an implicit meta-level account—we need to incorporate a heap, a mapping from addresses (or pointers, or locations, etc.) to values. Our language doesn’t have any imperative features, however as we’ll see using a heap-based machine model is an important component of the AAM approach to constructing analyses. We will now add a heap and use it to account for the memory used to bind variables when a function is applied.

In this model, we create a level of indirection in variable bindings so that environments will now map from variable names to addresses and the heap will resolve these addresses to values.

> (define-extended-language PCFσ PCFς     (ρ ::= ((X A) ...))     (Σ ::= ((A V) ...))     (A ::= any)     (σ ::= (ς Σ) V))

The reduction relation -->vσ will consist of -->vς, lifted to operate within the context (hole Σ), but then overriding the variable binding and dereference rules to allocate and dereference bindings via the heap:

> (define -->vσ     (extend-reduction-relation      (context-closure -->vς PCFσ (hole Σ))      PCFσ      (--> (N Σ) N discard-Σ-N)      (--> (O Σ) O discard-Σ-O)      (--> (((X ρ) K) Σ) ((V K) Σ)           (judgment-holds (lookup ρ X A))           (judgment-holds (lookup Σ A V))           ρ-x)         (--> (name σ (((((λ ([X : T] ...) M) ρ) V ...) K) Σ))           (((M (ext ρ (X A) ...)) K) (ext Σ (A V) ...))           (where (A ...) (alloc σ))           β)         (--> (name σ ((((name f ((μ (X_f : T_f) (λ ([X : T] ...) M)) ρ)) V ...) K) Σ))           (((M (ext ρ (X_f A_f) (X A) ...)) K) (ext Σ (A_f f) (A V) ...))           (where (A_f A ...) (alloc σ))           rec-β)))

We’ve also added two rules for discarding the heap for final states that consist of numbers or primitive operations since the heap is irrelevant. For function results though, we’ll need to keep the heap to make sense of any environments inside the result.

The -->vσ relation relies on a helper metafunction alloc, which allocates address for variables bindings. First, we define a metafunction for extracting formal parameter names:

> (define-metafunction PCFσ     formals : M -> (X ...)     [(formals (λ ([X : T] ...) M)) (X ...)]     [(formals (μ (X_f : T_f) L)) (X_f X ...)      (where (X ...) (formals L))])

The alloc metafunction consumes a state representing a β or rec-β redex and it produces a fresh address for each formal parameter name:

> (define-metafunction PCFσ     alloc : ((C K) Σ) -> (A ...)     [(alloc ((((M ρ) V ...) K) Σ))      ,(map (λ (x) (list x (gensym x)))            (term (formals M)))])

A transgression has just occurred. Can you spot it?

For example:

> (term (alloc (((((λ ([y : num] [z : num]) y) ()) 5 7) ()) ())))

'((y y17799) (z z17800))