1. [ ] is represented by mt;

2. E[([ ]e)] is represented by ar(e′, r, k) where r closes e′ to represent e and k represents E; and

3. E[(v[ ])] is represented by fn(v′, r, k) where r closes v′ to represent v and k represents E.

 

In this way, evaluation contexts form a program stack: mt is the empty stack, and ar and fn are frames.

States of the CEK machine are triples consisting of an expression, an environment that closes the control string, and a continuation:

ς ∈ å = Exp × Env × Cont
v ∈ Val = (λx.e)
r ∈ Env = Var →fin Val × Env
k ∈ Cont = mt | ar(e, r, k) | fn(v, r, k).

The transition function for the CEK machine is defined in Figure 1. The initial machine state for a program e is given by the injCEK function:

injCEK (e) = áe, 0/, mtñ.

Evaluation is defined by the reflexive, transitive closure of the machine transition relation and a “real” function (p. 129 of Plotkin19) that maps closures to the term represented:

evalCEK (e) = real (v, r), where injCEK (e) →v áv, r,;mtñ,
which is equivalent to the eval function of Section 2.1:
Lemma 1 (CEK Correctness7) evalCEK = eval.

We have now established a correct low-level evaluator for our prototypical language that is extensionally equivalent to the high-level reduction semantics. However, program analysis is not just concerned with the result of a computation, but also with how it was produced, i.e., analysis should predict intensional properties of the machine as it runs a program. We therefore adopt a reachable states semantics that relates a program to the set of all its intermediate steps:

CEK(e) = {ς;| injCEK (e) → CEK ς}.

Membership in the set of reachable states is straightforwardly undecidable. The goal of analysis, then, is to construct an abstract interpretation4 that is a sound and computable approximation of the CEK function.

figure 1. CeK machine.

;x, ρ, κ; ;(e0e1), ρ, κ; ;v, ρ, ar(e, ρ;, κ); ;v, ρ, fn((λx.e), ρ;, κ);

ς →CEKς; − ; ;v,ρ;,κ; where ρ(x) = (v, ρ; )

;e0, ρ, ar(e1, ρ, κ); ;e, ρ;, fn(v, ρ, κ); ;e, ρ;[x ;→ (v, ρ)], κ;

We can do this by constructing a machine that is similar in structure to the CEK machine: it is defined by an abstract state transition relation, CEK, which operates over abstract states, åˆ, that approximate states of the CEK machine. Abstract evaluation is then defined as

CEK(e) = {ς ˆ| injCEK (e) CEK ς ˆ}.

1. Soundness is achieved by showing transitions preserves approximation, so that if ς;CEK ς ¢ and ς ˆ approximates ς, then there exists an abstract state ς ˆ¢ such that ς ˆ CEK ς ˆ¢ and ς ˆ¢ approximates ς ¢.

2. Decidability is achieved by constructing the approximation in such a way that the state space of the abstracted machine is finite, which guarantees that for any program e, the set CEK(e) is finite.

 

an attempt at approximation: A simple approach to abstracting the machine’s state space is to apply a structural abstraction, which lifts approximation across the structure of a machine state, i.e., expressions, environments, and continuations. The problem with the structural abstraction approach for the CEK machine is that both environments and continuations are recursive structures. As a result, the abstraction yields objects in an abstract state space with recursive structure, implying the space is infinite.

Focusing on recursive structure as the source of the problem, our course of action is to add a level of indirection, forcing recursive structure to pass through explicitly allocated addresses. Doing so unhinges the recursion in the machine’s data structures, enabling structural abstraction via a single point of approximation: the store.

The next section covers the first of the two steps for refactoring the CEK machine into its computable approximation: a store component is introduced to machine states and variable bindings and continuations are redirected through the store. This step introduces no approximation and the constructed machine operates in lock-step with the CEK machine. However, the machine is amenable to a direct structural abstraction.

2. 3. CesK* machine

The states of the CESK* machine extend those of the CEK machine to include a store, which provides a level of indirection for variable bindings and continuations to pass through. The store is a finite map from addresses to storable values, which includes closures and continuations, and environments are changed to map variables to addresses. When a variable’s value is looked-up by the machine, it is now accomplished by using the environment to look up the variable’s address, which is then used to look up the value. To bind a variable to a value, a fresh location in the store is allocated and mapped to the value; the environment is extended to map the variable to that address.

To untie the recursive structure associated with continuations, we likewise add a level of indirection through the store and replace the continuation component of the machine with a pointer to a continuation in the store. We term the resulting machine the CESK* (control, environment, store,