BRICS RS-98-55 Gordon et al.: Compilation and Equivalence of Imperative Objects BRICS

Basic Research in Computer Science

Compilation and Equivalence of Imperative Objects

(Revised Report)

Andrew D. Gordon Paul D. Hankin Søren B. Lassen

BRICS Report Series RS-98-55 ISSN 0909-0878 December 1998 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1998, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/98/55/

Compilation and Equivalence of Imperative Objects (Revised Report)^{∗}

Andrew D. Gordon^{†} University of Cambridge Computer Laboratory

Paul D. Hankin University of Cambridge Computer Laboratory

Søren B. Lassen^{‡} BRICS^{§} Department of Computer Science University of Aarhus

December 1998

∗This is a revision of Technical Report 429, University of Cambridge Computer Laboratory, June 1997, which also appeared as BRICS Report RS-97-19, BRICS, Department of Computer Science, University of Aarhus, July 1997. A shorter version (Gordon, Hankin, and Lassen 1997) was presented at Foundations of Software Technology and Theoretical Computer Science, 17th Conference, Kharagpur, India, December 1997.

†Current affiliation: Microsoft Research.

‡Current affiliation: University of Cambridge Computer Laboratory.

§Basic Research in Computer Science, Centre of the Danish National Research Foundation.

Abstract

We adopt the untyped imperative object calculus of Abadi and Cardelli as a minimal setting in which to study problems of compilation and program equivalence that arise when compiling objectoriented languages. We present both a big-step and a small-step substitution-based operational semantics for the calculus. Our first two results are theorems asserting the equivalence of our substitutionbased semantics with a closure-based semantics like that given by Abadi and Cardelli. Our third result is a direct proof of the correctness of compilation to a stack-based abstract machine via a small-step decompilation algorithm. Our fourth result is that contextual equivalence of objects coincides with a form of Mason and Talcott’s CIU equivalence; the latter provides a tractable means of establishing operational equivalences. Finally, we prove correct an algorithm, used in our prototype compiler, for statically resolving method offsets. This is the first study of correctness of an object-oriented abstract machine, and of operational equivalence for the imperative object calculus.

Contents

1 Introduction 1

2 An Imperative Object Calculus 2 2.1 Syntax of the Calculus . . . . . . . . . . . . . . . . . . . . . . 2 2.2 Small-Step Substitution-Based Semantics . . . . . . . . . . . . 5 2.3 Big-Step Substitution-Based Semantics . . . . . . . . . . . . . 10 2.4 Big-Step Closure-Based Semantics . . . . . . . . . . . . . . . . 12 2.5 Discussion and Related Work . . . . . . . . . . . . . . . . . . 19

3 Compilation to an Abstract Machine 19 3.1 The Abstract Machine . . . . . . . . . . . . . . . . . . . . . . 20 3.2 Examples of Compilation and Execution . . . . . . . . . . . . 24 3.3 The Unloading Machine . . . . . . . . . . . . . . . . . . . . . 27 3.4 Examples of Unloading . . . . . . . . . . . . . . . . . . . . . . 29 3.5 Correctness of the Abstract Machine . . . . . . . . . . . . . . 33 3.6 Discussion and Related Work . . . . . . . . . . . . . . . . . . 44

4 Operational Equivalence 44 4.1 Experimental Equivalence . . . . . . . . . . . . . . . . . . . . 45 4.2 Operational Equivalence . . . . . . . . . . . . . . . . . . . . . 48 4.3 Laws of Operational Equivalence . . . . . . . . . . . . . . . . 50 4.4 Congruence . . . . . . . . . . . . . . . . . . . . . . . . . . . . 54 4.5 Contextual Equivalence . . . . . . . . . . . . . . . . . . . . . . 56 4.6 Discussion and Related Work . . . . . . . . . . . . . . . . . . 58

5 A Refinement: Static Resolution of Labels 61 5.1 Integer Offsets . . . . . . . . . . . . . . . . . . . . . . . . . . . 61 5.2 A Static Resolution Algorithm . . . . . . . . . . . . . . . . . . 63 5.3 Example of Static Resolution . . . . . . . . . . . . . . . . . . 64 5.4 Verification of the Algorithm . . . . . . . . . . . . . . . . . . . 64 5.5 Discussion and Related Work . . . . . . . . . . . . . . . . . . 70

6 Conclusions 70

1 Introduction

This paper collates and extends a variety of operational techniques for describing and reasoning about programming languages and their implementation. We focus on implementation of imperative object-oriented programs, expressed in an imperative object calculus. We examine different forms of structural operational semantics for the calculus, specify an implementation in terms of an object-oriented abstract machine, and develop a theory of operational equivalence between programs which we use to specify and verify a simple compiler optimisation. Many of our semantic techniques originate in earlier studies of the λ-calculus. This paper is their first application to an object calculus and shows they may easily be re-used in an object-oriented setting.

The language we describe is essentially the untyped imperative object calculus of Abadi and Cardelli (1995a, 1995b, 1996), a small but extremely rich language that directly accommodates object-oriented, imperative and functional programming styles. Abadi and Cardelli invented the calculus to serve as a foundation for understanding object-oriented programming; in particular, they use the calculus to develop a range of increasingly sophisticated type systems for object-oriented programming. We have implemented the calculus as part of a broader project to investigate object-oriented languages. Other work considers a concurrent variant of the imperative object calculus (Gordon and Hankin 1998). This paper develops formal foundations and verification methods to document and better understand various aspects of our implementation.

Our system compiles the imperative object calculus to bytecodes for an abstract machine, implemented in C, based on the ZAM^{1} of Leroy’s CAML Light (Leroy 1990). We also implemented a closure-based interpreter for the calculus. A type-checker enforces the system of primitive self types of Abadi and Cardelli. Since the results of the paper are independent of this type system, we will say no more about it.

The rest of the paper is organised as follows:

• In Section 2 we present our source language, the imperative object calculus, together with three forms of operational semantics (Plotkin 1981; Martin-Löf 1983; Felleisen and Friedman 1986; Kahn 1987). Theorem 1 and Theorem 2 assert the consistence of these semantics.

• Our target language is the instruction set of an object-oriented abstract machine, a simplification of the machine used in our implementation, and analogous to abstract machines for functional languages. Section 3 presents a formal description of our abstract machine, and a compiler from the object calculus to instructions for the abstract machine. We prove a compiler correctness result, Theorem 3, by adapting an idea of Rittri (1990) to cope with state and objects.

1“ZAM” is an acronym for “Zinc Abstract Machine”, where “Zinc” is an acronym for “Zinc is not Caml”.

• Given the formal description of our source language, we may express correctness of source-to-source transformations via operational equivalence. In Section 4, we adapt the contextual equivalence of Morris (1968), which has become the standard for studies of λ-calculi, to the imperative object calculus. Our fourth result, Theorem 4, characterises contextual equivalence using the CIU equivalence of Mason and Talcott (1991).

• In Section 5, we exercise operational equivalence by specifying a simple optimisation that resolves at compile-time certain method labels to integer offsets. Theorem 5 states the correctness of the optimisation.

We discuss related work at the ends of Sections 2, 3, 4 and 5. Finally, we review the contributions of the paper in Section 6.

Anyone desiring to experiment with our implementation is asked to contact the authors.

2 An Imperative Object Calculus

In this section, we present the syntax of an imperative object calculus, together with three forms of operational semantics, which we prove to be consistent with one another.

2.1 Syntax of the Calculus

We begin with the syntax of an untyped imperative object calculus, the impς calculus of Abadi and Cardelli (1996) augmented to include store locations as terms. Let x, y, and z range over an infinite collection of variables, ℓ range over an infinite collection of method labels, and ι range over an infinite collection of locations, the addresses of objects in the store.

The set of terms of the calculus is given as follows:

a, b ::= term x variable ι location [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] object (ℓ_{i} distinct) a.ℓ method selection a.ℓ ⇐ ς(x)b method update clone(a) cloning let x = a in b let

Informally, when an object is created, it is put at a fresh location, ι, in the store, and referenced thereafter by ι. Method selection runs the body of the method with the self parameter (the x in ς(x)b) bound to the location of the object containing the method. Method update allows an existing method in a stored object to be updated. Cloning makes a fresh copy of an object in the store at a new location. The reader unfamiliar with object calculi is encouraged to consult the book of Abadi and Cardelli (1996) for many examples and a discussion of the design choices that led to this calculus.

Here are the scoping rules for variables: in a method ς(x)b, variable x is bound in b; in let x = a in b, variable x is bound in b. If ϕ is a phrase of syntax we write fv(ϕ) for the set of variables that occur free in ϕ. We say phrase ϕ is closed if fv(ϕ) = ∅. We write ϕ{{ψ/x}} for the substitution of phrase ψ for each free occurrence of variable x in phrase ϕ. We identify all phrases of syntax up to alpha-conversion; hence a = b, for instance, means that we can obtain term b from term a by systematic renaming of bound variables. Let o range over objects, terms of the form [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}]. In general, the notation ϕ_{i} ^{i∈1..n} means ϕ_{1}, …, ϕ_{n}.

Unlike Abadi and Cardelli, we do not identify objects up to re-ordering of methods. This is because the order of methods in an object is significant for an application of our techniques presented in Section 5. Moreover, we include locations in the syntax of terms. This is so we may express the dynamic behaviour of the calculus using a substitution-based operational semantics. In Abadi and Cardelli’s closure-based semantics, locations appear only in closures and not in terms. If ϕ is a phrase of syntax, let locs(ϕ) be the set of locations that occur in ϕ. Let a term a be a static term if locs(a) = ∅. The static terms correspond to the source syntax accepted by our compiler. Terms containing locations arise during reduction.

As a first example of programming in the imperative object calculus, here is how to express pairs of terms as objects with fst and snd methods for accessing the two components and a swap method for interchanging the first and second components:

pair(a, b) =^{def} [\begin{matrix}fst = ς(s)a, \\ snd = ς(s)b, \\ swap = ς(s)\begin{matrix}let x = s.fst in \\ let y = s.snd in \\ (s.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x] \end{matrix} \\ for s ∉ fv(a) ∪ fv(b) \end{matrix}

The next example makes use of the imperative nature of the calculus to express updateable references as objects with a single ref method:

ref (a) =^{def} let x = a in [ref = ς(y)x]
a:= b =^{def} let x = b in a.ref ⇐ ς(y)x
!a =^{def} a.ref

As a third example, here is an encoding of the call-by-value λ-calculus:

λ(x)b =^{def} [arg = ς(z)z.arg, val = ς(s)let x = s.arg in b]
b(a) =^{def} let y = a in (b.arg ⇐ ς(z)y).val

where y ≠ z, and s and y do not occur free in b. It is like an encoding from Abadi and Cardelli’s book but with right-to-left evaluation of function application. Given updateable methods, we can easily extend this encoding to express an ML-style call-by-value λ-calculus with updateable references.

Although functions are derivable, for the purpose of the operational semantics of this section and the abstract machine and compiler in the next, Section 3, we consider an extended calculus that includes functions and function application. This is partly because an efficient implementation would include functions (procedures) as primitive, and partly to demonstrate the applicability of the techniques of these sections to a λ-calculus with state. We do not use this extended calculus in Section 4 or in Section 5. The techniques used in the study of operational equivalence in Section 4 are well understood for λ-calculi with state. The optimisation of method access in Section 5 is independent of the presence of primitive functions.

The syntax of the extended calculus is given by:

a, b ::= terms … as previously λ(x)b function b(a) application In a function λ(x)b, variable x is bound in b. Unlike Abadi and Cardelli’s imperative λ-calculus, the impλ calculus, our extended calculus does not permit assignments to bound variables.

Throughout this paper, and in our implementation, we adopt the convention that a function application b(a) is evaluated right-to-left; a is evaluated before b. In making this choice we are following Leroy (1990), who proposes it on grounds of efficiency. Adopting a left-to-right evaluation order would have little effect on the contents of this paper, but would adversely affect the performance of our implementation.

We finish this section by fixing notation for finite lists and finite maps. We write finite lists in the form [ϕ_{1}, …, ϕ_{n}], which we usually write as [ϕ_{i} ^{i∈1..n}]. Let ψ:: [ϕ_{i} ^{i∈1..n}] = [ψ, ϕ_{i} ^{i∈1..n}]. Let [ϕ_{i} ^{i∈1..m}]@[ψ_{j} ^{j∈1..n}] = [ϕ_{i} ^{i∈1..m}, ψ_{j} ^{j∈1..n}].

Let a finite map, f, be a list of the form [x_{i} ↦ ϕ_{i} ^{i∈1..n}], where the x_{i} are distinct. When f = [x_{i} ↦ ϕ_{i} ^{i∈1..n}] is a finite map, let dom(f) = {x_{i} ^{i∈1..n}}. For the finite map f = f′@[x ↦ ϕ]@f′′, let f(x) = ϕ. When f is a finite map, let the map f + (x ↦ ϕ), be f′@[x ↦ ϕ]@f′′ if f = f′@[x ↦ ψ]@f′′, otherwise (x ↦ ϕ) :: f.

2.2 Small-Step Substitution-Based Semantics

The goal of this section is to specify a relation, c → d, where c and d are each configurations consisting of a closed term paired with an object store. Intuitively, c → d means that the program state represented by c takes a single computation step to reach d. We present this operational semantics using reduction contexts introduced in the study of imperative λ-calculi by Felleisen and Friedman (1986). We say this is a small-step semantics because it defines individual steps of computation. We say it is substitution-based because it is defined in terms of the substitution primitive, −{{v/x}}, that substitutes values for variables. We use this semantics in Section 3 to prove correctness of compilation. In the course of this paper, we use the symbol → for several small-step relations; we refer to such relations as reduction or transition relations.

Let a store, σ, be a finite map from locations to objects. Each stored object consists of a collection of labelled methods. The methods may be updated individually. Abadi and Cardelli use a method store, a finite map from locations to methods, in their operational semantics of imperative objects. We prefer to use an object store, as it explicitly represents the grouping of methods in objects. We discuss the connection between our semantics and that of Abadi and Cardelli in Section 4.6.

σ ::= [ι_{i} ↦ o_{i} ^{i∈1..n}] object store (ι_{i} distinct) c, d ::= (a, σ) configuration

We write ⊢ σ ok, to mean that a store σ is well formed, if and only if fv(σ(ι)) = ∅ and locs(σ(ι)) ⊆ dom(σ) for each ι ∈ dom(σ). We write ⊢ (a, σ) ok, to mean that a configuration (a, σ) is well formed, if and only if fv(a) = ∅, locs(a) ⊆ dom(σ) and ⊢ σ ok.

To define the reduction relation we need the syntactic concepts of values and reduction contexts. A value is either a location or a function. A reduction context, R, is a term given by the following grammar, with one free occurrence of a distinguished variable, •, which represents ‘the point of execution’ in R.

u, v ::= ι | λ(x)b value R ::= • | R.ℓ | R.ℓ ⇐ ς(x)b reduction context

| clone(R) | let x = R in b

| a(R) | R(v)

Since there is exactly one free occurrence of • in any reduction context, if R.ℓ ⇐ ς(x)b is a reduction context, • ∉ fv(b) − {x}. For the same reason, if let x = R in b, a(R), and R(v) are reduction contexts, • ∉ fv(b) − {x},

• ∉ fv(a) and • ∉ fv(v), respectively. We write R[a] for the outcome of substituting term a (not necessarily a value) for the single occurrence of the hole • in a reduction context R. No variables are ever captured by this operation, since the hole in a reduction context does not appear in the scope of any bound variables.

Let the small-step substitution-based reduction relation, c → d, be the least relation satisfying the following axiom schemes.

(Red Object) (R[o], σ) → (R[ι], σ′) if σ′ = (ι ↦ o) :: σ and ι ∉ dom(σ).

(Red Select) (R[ι.ℓ_{j}], σ) → (R[b_{j}{{ι/x_{j}}}], σ)

if σ(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] and j ∈ 1..n.

(Red Update) (R[ι.ℓ_{j} ⇐ ς(x)b], σ) → (R[ι], σ′)

if σ(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}], j ∈ 1..n, and

σ′ = σ + (ι ↦ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..j−1}, ℓ_{j} = ς(x)b, ℓ_{i} = ς(x_{i})b_{i} ^{i∈j+1..n}]).

(Red Clone) (R[clone(ι)], σ) → (R[ι′], σ′)

if σ(ι) = o, σ′ = (ι′ ↦ o) :: σ and ι′ ∉ dom(σ).

(Red Let) (R[let x = v in b], σ) → (R[b{{v/x}}], σ).

(Red Appl) (R[(λ(x)b)(v)], σ) → (R[b{{v/x}}], σ).

The outcome of reducing a well formed configuration is itself a well formed configuration. Moreover, reduction may increase, but not decrease, the domain of the store of a configuration:

Lemma 1 Suppose ⊢ (a, σ) ok and (a, σ) → (a′, σ′). Then ⊢ (a′, σ′) ok and dom(σ) ⊆ dom(σ′).

Proof By inspection of the reduction rules. □

Let a configuration c be terminal if and only if there is a store σ and a value v such that c = (v, σ). We say that a configuration c converges, c↓, if and only if there is a terminal configuration d such that c →^{∗} d. We say that a configuration c diverges if and only if there is an infinite sequence of configurations c_{1}, c_{2}, … such that c → c_{1} → c_{2} → · · ·.

For instance, consider the configuration:

(pair(ι_{1}, ι_{2}).swap, σ)

where σ is a well formed store of the form [ι_{1} ↦ o_{1}, ι_{2} ↦ o_{2}] and pair is as defined in Section 2.1. This is not a terminal configuration, but it converges because of the following reduction sequence (in which we assume ι ∉ dom(σ)).

(pair(ι_{1}, ι_{2}).swap, σ)

→ (ι.swap, (ι ↦ pair(ι_{1}, ι_{2})) :: σ)
→ (\begin{matrix}let x = ι.fst in let y = ι.snd in (ι.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x, \\ (ι ↦ pair(ι_{1}, ι_{2})) :: σ) \end{matrix}
→ (\begin{matrix}let x = ι_{1} in let y = ι.snd in (ι.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x, \\ (ι ↦ pair(ι_{1}, ι_{2})) :: σ) \end{matrix}
→ (\begin{matrix}let y = ι.snd in (ι.fst ⇐ ς(s′)y).snd ⇐ ς(s′)ι_{1}, \\ (ι ↦ pair(ι_{1}, ι_{2})) :: σ) \end{matrix}
→ (\begin{matrix}let y = ι_{2} in (ι.fst ⇐ ς(s′)y).snd ⇐ ς(s′)ι_{1}, \\ (ι ↦ pair(ι_{1}, ι_{2})) :: σ) \end{matrix}
→ ((ι.fst ⇐ ς(s′)ι_{2}).snd ⇐ ς(s′)ι_{1}, (ι ↦ pair(ι_{1}, ι_{2})) :: σ)
→ (ι.snd ⇐ ς(s′)ι_{1}, (ι ↦ pair(ι_{2}, ι_{2})) :: σ)
→ (ι, (ι ↦ pair(ι_{2}, ι_{1})) :: σ)

Consider now the following configuration:

([ℓ = ς(s)s.ℓ].ℓ, [])

It diverges because of the following reduction sequence.

([ℓ = ς(s)s.ℓ].ℓ, []) → (ι.ℓ, [ι ↦ [ℓ = ς(s)s.ℓ]])
→ (ι.ℓ, [ι ↦ [ℓ = ς(s)s.ℓ]])
→ ⋯

Next we show that reduction, →, is deterministic up to the choice of freshly allocated locations in rules (Red Object) and (Red Clone). To state this precisely, we need a couple of definitions. First, we define a predicate which asserts that the domain of the store of a configuration includes a set w of locations: let the predicate ⊢_{w} (a, σ) ok hold if and only if ⊢ (a, σ) ok and w ⊆ dom(σ). Second, we define structural equivalence at w, ≡_{w}, for any finite set w of locations, as the least relation on configurations closed under the following rules.

(Struct Refl)

\frac{⊢_{w} c ok}{c ≡_{w} c}

(Struct Trans)

\frac{c ≡_{w} c′ c′ ≡_{w} c′′}{c ≡_{w} c′′}

(Struct Rename)

\frac{⊢_{w} (a, σ) ok ι ∈ dom(σ) − w ι′ ∉ dom(σ)}{(a, σ) ≡_{w} (a\{\{ι′/ι\}\}, σ\{\{ι′/ι\}\})}

In this definition the notation a{{ι′/ι}} denotes the outcome of replacing every occurrence of location ι in a by ι′; and σ{{ι′/ι}} denotes the outcome of renaming location ι of store σ to ι′, and applying this substitution to each of the objects in the store. An easy induction establishes that c ≡_{w} d implies that ⊢_{w} c ok and ⊢_{w} d ok. Roughly, c ≡_{w} d means that the locations in w are all included in the domains of the stores of both c and d, and that c may be obtained from d by a series of renamings of the locations outside w.

Lemma 2 Relation ≡_{w} is symmetric, and hence is an equivalence relation.

Proof Suppose c ≡_{w} c′, then c′ ≡_{w} c follows by an induction on the derivation of c ≡_{w} c′. Cases (Struct Refl) and (Struct Trans) are easy. In the case of (Struct Rename), we must show (a{{ι′/ι}}, σ{{ι′/ι}}) ≡_{w} (a, σ) when (a, σ) ≡_{w} (a{{ι′/ι}}, σ{{ι′/ι}}) derives from ⊢_{w} (a, σ) ok, ι ∈ dom(σ) − w and ι′ ∉ dom(σ). From ⊢_{w} (a, σ) ok it follows that locs(a)∪locs(σ)∪w ⊆ dom(σ). Therefore ι′ ∉ locs(a) ∪ locs(σ). Hence we have:

a{{ι′/ι}}{{ι/ι′}} = a  (1)
σ{{ι′/ι}}{{ι/ι′}} = σ  (2)

From (a, σ) ≡_{w} (a{{ι′/ι}}, σ{{ι′/ι}}) it follows that ⊢_{w} (a{{ι′/ι}}, σ{{ι′/ι}}) ok. We have ι′ ∉ dom(σ) and w ⊆ dom(σ), and ι ∈ dom(σ) − w, that is, ι ∈ dom(σ) but ι ∉ w. Therefore ι′ ∈ dom(σ{{ι′/ι}}) but ι′ ∉ w, that is, ι′ ∈ dom(σ{{ι′/ι}})− w. Moreover ι ∉ dom(σ{{ι′/ι}}), since we may conclude that ι ≠ ι′ from ι ∈ dom(σ) but ι′ ∉ dom(σ). By (Struct Rename), ⊢_{w} (a{{ι′/ι}}, σ{{ι′/ι}}) ok, ι′ ∈ dom(σ{{ι′/ι}}) − w and ι ∉ dom(σ{{ι′/ι}}) together imply

(a{{ι′/ι}}, σ{{ι′/ι}}) ≡_{w} (a{{ι′/ι}}{{ι/ι′}}, σ{{ι′/ι}}{{ι/ι′}})
= (a, σ)

the desired equation, where the second step appeals to equations (1) and (2).

□

The → relation is deterministic up to structural equivalence:

Proposition 1 Suppose ⊢_{w} c ok. Then c → c′ and c → c′′ imply c′ ≡_{w} c′′.

Proof By case analysis of the derivation of c → c′. Here is one case:

(Red Object) Here c = (R[o], σ) and c′ = (R[ι′], σ′) where σ′ = (ι′ ↦ o) :: σ and ι′ ∉ dom(σ). Since ⊢_{w} c ok, c is well formed and therefore ι′ ∉ locs(R). Only (Red Object) may derive c → c′′, so c′′ = (R[ι′′], σ′′) where σ′′ = (ι′′ ↦ o)::σ and ι′′ ∉ dom(σ). If ι′ = ι′′, c′ ≡_{w} c′′ by (Struct Refl). Otherwise, ι′ ≠ ι′′, so ι′′ ∉ dom(σ′). Since w ⊆ dom(σ) and ι′ ∉ dom(σ), ι′ ∈ dom(σ′)−w. By (Struct Rename), using ι′ ∉ locs(R),

(R[ι′], σ′) ≡_{w} (R[ι′]{{ι′′/ι′}}, σ′{{ι′′/ι′}}) = (R[ι′′], σ′′),

that is, c′ ≡_{w} c′′.

The case for (Red Clone) is similar. If c → c′ was derived using any of the other rules, and c → c′′, then in fact c′ = c′′; hence c′ ≡_{w} c′′. □

Let a configuration c be stuck if and only if c is not terminal, but there is no d with c → d. Examples are (ι.ℓ, [ι ↦ []]) and (ι.ℓ, []). We say that a configuration, c, goes wrong if and only if there is a stuck configuration, d, such that c →^{∗} d.

Configurations related by structural equivalence at w possess the following properties:

Lemma 3 Suppose c ≡_{w} c′.

(1) c is terminal implies c′ is terminal.

(2) c is stuck implies c′ is stuck.

(3) c → d implies there exists d′ such that c′ → d′ and d ≡_{w} d′.

Proof Parts (1) and (3) follow by inductions on the derivation of c ≡_{w} c′. Part (2) follows from (1), (3) and the symmetry of ≡_{w}, Lemma 2. □

Proposition 1 and Lemma 3 imply that whenever (a, σ) is well formed and (a, σ) →^{∗} d, the configuration d is unique up to structural equivalence at dom(σ), that is, up to the renaming of any newly generated locations in the store component of d. Furthermore, whenever c ≡_{w} c′, (1) c converges just if c′ converges, (2) c goes wrong just if c′ goes wrong, and (3) c diverges just if c′ diverges.

Proposition 2 For any well formed configuration c, exactly one of the following holds:

(1) c converges,

(2) c goes wrong,

(3) c diverges.

Proof If there is no computation c →^{∗} d to a terminal or stuck configuration d, then every reduction sequence from c is infinite (or extends to an infinite sequence), so (3) holds and (1) and (2) are false.

Otherwise, there is a least n such that c →^{n} d, for some terminal or stuck configuration d. Suppose d is terminal—the case when d is stuck is analogous. Then (1) holds. By induction on n we prove that (2) and (3) are false. If n = 0, (2) and (3) are false because a terminal configuration is not stuck and because there is no reduction d → d′ from a terminal configuration. If n > 0, there is c′ such that c → c′ and c′ →^{n−1} d. By induction hypothesis, c′ does not go wrong and does not diverge. For any other reduction c → c′′, we have c′ ≡_{∅} c′′, by Proposition 1. As a consequence of Lemma 3, if c′′ goes wrong or diverges, so does c′. Therefore there is no reduction c → c′′ such that c′′ goes wrong or diverges. Since c is not stuck, we get that c cannot go wrong or diverge, that is, (2) and (3) are false, as required. □

2.3 Big-Step Substitution-Based Semantics

In this section, we specify a relation, c ⇓ d, where again c and d are configurations, but this time with the intuition that d is the final outcome of many computation steps starting from c. We say this is a big-step semantics because it relates a configuration to the final outcome of taking many individual steps of computation. It is defined in terms of the substitution primitive, −{{v/x}}, like the small-step relation, →, of the previous section. Unlike the → relation, the ⇓ relation is defined inductively. We exploit its induction principle in the proof of Proposition 15, the crux of Section 5. In the course of this paper, we use the symbol ⇓ for several big-step relations; we often refer to such relations as evaluation relations.

Let the big-step substitution-based evaluation relation, c ⇓ d, be the relation on configurations inductively defined by the following rules.

(Subst Value)

\overline{(v, σ) ⇓ (v, σ)} (Subst Object)

\frac{σ_{1} = (ι ↦ o) :: σ_{0} ι ∉ dom(σ_{0})}{(o, σ_{0}) ⇓ (ι, σ_{1})}

(Subst Select) (where j ∈ 1..n)

\frac{(a, σ_{0}) ⇓ (ι, σ_{1}) σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] (b_{j}\{\{ι/x_{j}\}\}, σ_{1}) ⇓ (v, σ_{2})}{(a.ℓ_{j}, σ_{0}) ⇓ (v, σ_{2})}

(Subst Update) (where j ∈ 1..n)

\frac{\begin{matrix}(a, σ_{0}) ⇓ (ι, σ_{1}) σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] \\ σ_{2} = σ_{1} + (ι ↦ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..j−1}, ℓ_{j} = ς(x)b, ℓ_{i} = ς(x_{i})b_{i} ^{i∈j+1..n}]) \end{matrix}}{(a.ℓ_{j} ⇐ ς(x)b, σ_{0}) ⇓ (ι, σ_{2})}

(Subst Clone)

\frac{(a, σ_{0}) ⇓ (ι, σ_{1}) σ_{1}(ι) = o σ_{2} = (ι′ ↦ o) :: σ_{1} ι′ ∉ dom(σ_{1})}{(clone(a), σ_{0}) ⇓ (ι′, σ_{2})}

(Subst Let)

\frac{(a, σ_{0}) ⇓ (v, σ_{1}) (b\{\{v/x\}\}, σ_{1}) ⇓ (u, σ_{2})}{(let x = a in b, σ_{0}) ⇓ (u, σ_{2})}

(Subst Appl)

\frac{(a, σ_{0}) ⇓ (u, σ_{1}) (b, σ_{1}) ⇓ (λ(x)b′, σ_{2}) (b′\{\{u/x\}\}, σ_{2}) ⇓ (v, σ_{3})}{(b(a), σ_{0}) ⇓ (v, σ_{3})}

We define c ↘ d to mean that c →^{∗} d and d is terminal. The big-step and small-step substitution semantics are consistent with one another in the following sense:

Theorem 1

(1) Whenever c ⇓ d, c ↘ d.

(2) Whenever c ↘ d, c ⇓ d.

Proof

(1) By induction on the derivation of c ⇓ d. The details are routine.

(2) One can prove by induction on n that c ⇓ d whenever c →^{n} d and d is terminal. Again, the details are routine. □

The big-step relation, ⇓, is deterministic in the following sense:

Proposition 3 Whenever ⊢_{w} c ok, c ⇓ c′ and c ⇓ c′′ imply c′ ≡_{w} c′′.

Proof Suppose that c ⇓ c′ and c ⇓ c′′. By Theorem 1(1), both c′ and c′′ are terminal and there are m and n such that c →^{m} c′ and c →^{n} c′′. Without loss of generality, suppose that m ≤ n. There must be d such that c →^{m} d and d →^{n−m} c′′. By Proposition 1 and Lemma 3(3), c′ ≡_{w} d. It follows, by Lemma 3, that d is terminal, and therefore that c′′ = d. Hence we have that c′ ≡_{w} c′′. □

2.4 Big-Step Closure-Based Semantics

In this section we present an operational semantics for the imperative object calculus, based on the one in Chapter 10 of Abadi and Cardelli (1996) but with the addition of functions. It is in the same style as the dynamic semantics of expressions in the definition of Standard ML (Milner, Tofte, and Harper 1990). Unlike the semantics of the previous sections, it uses closures, rather than a substitution primitive, to link variables to their values. Like the semantics of the previous section, it is a big-step semantics, an evaluation relation, denoted by ⇓. The main result of this section is a proof of consistency between the closure-based semantics and the substitution-based semantics of the previous section.

U, V ::= closure-based value ι location (S, λ(x)b) function closure

S ::= [x_{i} ↦ V_{i} ^{i∈1..n}] stack (x_{i} distinct) O ::= [ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈1..n}] object value Σ ::= [ι_{i} ↦ O_{i} ^{i∈1..n}] store C, D ::= configuration

((S, a), Σ) initial configuration (V, Σ) terminal configuration

A stack (of bindings) S = [x_{i} ↦ V_{i} ^{i∈1..n}] is a finite map that binds variables to their values. A value is either a location, ι, or a closure of the form (S, λ(x)b) where the stack S maps each variable free in b to a value. A store Σ is a finite map sending locations to object values, which are of the form O = [ℓ_{i} = (S_{i}, ς(x_{i})b_{i}) ^{i∈1..n}], where for each i, stack S_{i} maps each variable free in the method ς(x_{i})b_{i} to its value. An initial configuration consists of a closure (S, a), together with a store Σ that maps locations occurring in (S, a) to object values. A terminal configuration is simply a value paired with a store. A configuration of the form (V, Σ) where V = (S, λ(x)b) is both initial and terminal.

Our syntax admits stores and configurations that include dangling pointers and unbound variables. We could make an explicit definition of those well formed stores and configurations that do not include such errors. Instead, it is more convenient, later on in this section, to make an implicit definition of well formed stores and configurations in terms of an unloading relation.

We use uppercase metavariables for the entities used in our closure-based semantics; they mostly correspond to lowercase metavariables ranging over corresponding entities used in the substitution-based semantics. For example, σ is a store used in the two substitution-based semantics, and Σ is a store used in the closure-based semantics. We refer to both entities as stores, relying on the case of the metavariable to indicate which kind of store is meant.

Let the big-step closure-based evaluation relation, C ⇓ D, be the relation on configurations inductively defined by the following rules.

(Closure x)

\frac{S(x) = V}{((S, x), Σ) ⇓ (V, Σ)}

(Closure Value)

\overline{((S, λ(x)b), Σ) ⇓ ((S, λ(x)b), Σ)}

(Closure Select)

\frac{((S, a), Σ_{0}) ⇓ (ι, Σ_{1}) Σ_{1}(ι) = [ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈1..n}] j ∈ 1..n x_{j} ∉ dom(S_{j}) (((x_{j} ↦ ι) :: S_{j}, b_{j}), Σ_{1}) ⇓ (V, Σ_{2})}{((S, a.ℓ_{j}), Σ_{0}) ⇓ (V, Σ_{2})}

(Closure Update)

\frac{\begin{matrix}((S, a), Σ_{0}) ⇓ (ι, Σ_{1}) Σ_{1}(ι) = [ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈1..n}] j ∈ 1..n \\ O = [ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈1..j−1}, ℓ_{j} = (S, ς(x)b), ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈j+1..n}] \end{matrix}}{((S, a.ℓ_{j} ⇐ ς(x)b), Σ_{0}) ⇓ (ι, (ι ↦ O) + Σ_{1})}

(Closure Object)

\frac{Σ_{1} = (ι ↦ [ℓ_{i} = (S, ς(x_{i})b_{i})^{i∈1..n}]) :: Σ_{0} ι ∉ dom(Σ_{0})}{((S, [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}]), Σ_{0}) ⇓ (ι, Σ_{1})}

(Closure Clone)

\frac{((S, a), Σ_{0}) ⇓ (ι, Σ_{1}) Σ_{1}(ι) = O Σ_{2} = (ι′ ↦ O) :: Σ_{1} ι′ ∉ dom(Σ_{1})}{((S, clone(a)), Σ_{0}) ⇓ (ι′, Σ_{2})}

(Closure Let)

\frac{((S, a), Σ_{0}) ⇓ (V, Σ_{1}) x ∉ dom(S) (((x ↦ V) :: S, b), Σ_{1}) ⇓ (U, Σ_{2})}{((S, let x = a in b), Σ_{0}) ⇓ (U, Σ_{2})}

(Closure Appl)

\frac{((S, a), Σ_{0}) ⇓ (U, Σ_{1}) ((S, b), Σ_{1}) ⇓ ((S′, λ(x)b′), Σ_{2}) x ∉ dom(S′) (((x ↦ U) :: S′, b′), Σ_{2}) ⇓ (V, Σ_{3})}{((S, b(a)), Σ_{0}) ⇓ (V, Σ_{3})}

These rules are almost identical to the ones from Chapter 10 of Abadi and Cardelli (1996), except for the inclusion of functions and except that locations contain objects in our semantics but methods in theirs, as discussed earlier (and in Section 4.6).

The semantics does indeed relate initial and terminal configurations:

Lemma 4 Whenever C ⇓ D, C is an initial configuration and D is a terminal configuration.

Proof By induction on the derivation of C ⇓ D. □

To establish a correspondence between this closure-based semantics and the substitution-based semantics of Section 2.3, we introduce several relations that unload the entities used in the closure-based semantics by turning closures into substitutions. Let s range over a substitution of the form [v^{i}/x_{i}^{i∈1..n}] where the x_{i} are distinct and each v_{i} is closed. We use the symbol ⇝ for each of five unloading relations.

V ⇝ v value unloading S ⇝ s stack unloading O ⇝ o object unloading Σ ⇝ σ store unloading C ⇝ c configuration unloading (Value ι) \overline{ι ⇝ ι} (Value Fun)

\frac{S ⇝ s x ∉ dom(S) fv(b) ⊆ dom(S) ∪ \{x\} locs(b) = ∅}{(S, λ(x)b) ⇝ λ(x)(b\{\{s\}\})}

(Stack []) \overline{[] ⇝ []} (Stack Object)

\frac{V ⇝ v x ∉ dom(S) S ⇝ s}{((x ↦ V) :: S) ⇝ (v/x:: s)}

(Object Unload) (where ℓ_{i} distinct)

\frac{S_{i} ⇝ s_{i} x_{i} ∉ dom(S_{i}) fv(b_{i}) ⊆ dom(S_{i}) ∪ \{x_{i}\} locs(b_{i}) = ∅ ∀i ∈ 1..n}{[ℓ_{i} = (S_{i}, ς(x_{i})b_{i})^{i∈1..n}] ⇝ [ℓ_{i} = ς(x_{i})(b_{i}\{\{s_{i}\}\})^{i∈1..n}]}

(Store Unload) (where Σ = [ι_{i} ↦ O_{i} ^{i∈1..n}], ι_{i} distinct)

\frac{O_{i} ⇝ o_{i} ∀i ∈ 1..n}{Σ ⇝ [ι_{i} ↦ o_{i} ^{i∈1..n}]}

(Config Initial)

\frac{S ⇝ s Σ ⇝ σ fv(a) ⊆ dom(S) locs(a) = ∅}{((S, a), Σ) ⇝ (a\{\{s\}\}, σ)}

(Config Terminal)

\frac{V ⇝ v Σ ⇝ σ}{(V, Σ) ⇝ (v, σ)}

We later need the following properties of the unloading relations. Proposition 4

(1) Whenever V ⇝ v, v is a closed value.

(2) Whenever S ⇝ s there are distinct variables x_{i} and closed values v_{i} such that s = [v^{i}/x_{i} ^{i∈1..n}] and dom(S) = {x_{i} ^{i∈1..n}}.

(3) Whenever O ⇝ o, object o is closed.

(4) Whenever Σ ⇝ σ, both dom(Σ) = dom(σ) and ⊢ σ ok.

(5) Whenever C ⇝ c, ⊢ c ok. Proof By simultaneous induction on the derivation of the unloading predicates. □

The side conditions concerning free and bound variables in (Value Fun), (Stack Object), (Object Unload) and (Config Initial) are needed to ensure property (2). This property allows the substitutions that arise from closures to be manipulated easily in later proofs. All the terms manipulated by the closure-based evaluator are static terms; the side conditions concerning locations in (Value Fun), (Object Unload) and (Config Initial) ensure that only static terms arise in configurations.

We consider a store Σ to be well formed if and only if there is a store σ such that Σ ⇝ σ. Similarly, we consider a configuration C to be well formed if and only if there is a configuration c such that C ⇝ c. The only occurrences of locations in a well formed configuration are in the domain of the store and in the range of any stacks occurring in the configuration.

The unloading relations are in fact functional:

Proposition 5 Whenever ϕ ⇝ ψ′ and ϕ ⇝ ψ′′, then ψ′ = ψ′′.

Proof By induction on the derivation of ϕ ⇝ ψ′. The only interesting cases are (Config Initial) and (Config Terminal).

(Config Initial) Here ϕ = ((S, a), Σ) and ψ′ = (a{{s′}}, σ′) where S ⇝ s′, Σ ⇝ σ′, fv(a) ⊆ dom(S) and locs(a) = ∅. The derivation of ϕ ⇝ ϕ′′ can only have used (Config Initial) or (Config Terminal). In the former case ψ′ = ψ′′ follows easily from the induction hypothesis. The latter case can only arise when ϕ is a terminal configuration, that is, a is of the form λ(x)b. We have ψ′′ = (v′′, σ′′) where λ(x)b ⇝ v′′ and Σ ⇝ σ′′. The former judgment can only arise from (Value Fun). Taking alpha-conversion into account, we may assume there is a variable x′ ∉ fv(b) − {x}, so that λ(x)b = λ(x′)(b{{x′/x}}) and that λ(x)b ⇝ v′′ = λ(x′)(b{{x′/x}}{{s′′}}) derives by (Value Fun) from S ⇝ s′′ given that x′ ∉ dom(S), fv(b{{x′/x}}) ⊆ dom(S) ∪ {x′} and locs(b{{x′/x}}) = ∅. By induction hypothesis, σ′ = σ′′ and s′ = s′′. By Proposition 4(2), there are distinct x_{i} and closed values v_{i} such that s′ = [v^{i}/x_{i} ^{i∈1..n}] and dom(S) = {x_{i} ^{i∈1..n}}. Since x′ ∉ dom(S), x′ ≠ x_{i} for each i. Therefore we can calculate the following,

v′′ = λ(x′)(b{{x′/x}}{{v^{i}/x_{i} ^{i∈1..n}}})
= λ(x′)(b{{x′/x}}){{v^{i}/x_{i} ^{i∈1..n}}}
= a{{s′}}

which shows that ψ′′ = (v′′, σ′′) = (a{{s′}}, σ′) = ψ′, as required.

Case (Config Terminal) is similar. The other cases are simpler. □

To prove Theorem 2, which asserts the consistency of the two big-step operational semantics, we need the following two lemmas.

Lemma 5 If C ⇝ c and C ⇓ C′ there is c′ such that C′ ⇝ c′ and c ⇓ c′.

Proof By induction on the derivation of C ⇓ C′. We show three typical cases.

(Closure Select) Here C = ((S, a.ℓ_{j}), Σ_{0}), C′ = (V, Σ_{2}) and we have

((S, a), Σ_{0}) ⇓ (ι, Σ_{1})  (3)
Σ_{1}(ι) = [ℓ_{i} = (S_{i}, ς(x_{j})b_{i})^{i∈1..n}]  (4)
(((x_{j} ↦ ι) :: S_{j}, b_{j}), Σ_{1}) ⇓ (V, Σ_{2})  (5)

with j ∈ 1..n and x_{j} ∉ dom(S_{j}). From C ⇝ c it follows there is σ_{0} and s such that Σ_{0} ⇝ σ_{0}, S ⇝ s and c = (a{{s}}.ℓ_{j}, σ_{0}). So ((S, a), Σ_{0}) ⇝ (a{{s}}, σ_{0}). By the induction hypothesis and (3) there is c′_{1} such that

(a{{s}}, σ_{0}) ⇓ c′_{1}  (6)

and (ι, Σ_{1}) ⇝ c′_{1}. From the latter, there must be σ_{1} with Σ_{1} ⇝ σ_{1} and c′_{1} = (ι, σ_{1}). From (4) we know that ι ∈ dom(Σ_{1}); from Σ_{1} ⇝ σ_{1}, it follows that ι ∈ dom(σ_{1}) and Σ_{1}(ι) ⇝ σ_{1}(ι). It must be then that Σ_{1}(ι) ⇝ σ_{1}(ι), using (Object Unload). Given (4), for each i ∈ 1..n there is s_{i} such that S_{i} ⇝ s_{i} and

σ_{1}(ι) = [ℓ_{i} = ς(x_{i})(b_{i}{{s_{i}}})^{i∈1..n}]  (7)

Therefore (((x_{j} ↦ ι) :: S_{j}, b_{j}), Σ_{1}) ⇝ (b_{j}{{ι/x_{j}}}{{s_{j}}}, σ_{1}). Since x_{j} ∉ dom(S_{j}) and S_{j} ⇝ s_{j}, b_{j}{{ι/x_{j}}}{{s_{j}}} = b_{j}{{s_{j}}}{{ι/x_{j}}}. By the induction hypothesis and (5) there is c′ such that

(b_{i}{{s_{j}}}{{ι/x_{j}}}, σ_{1}) ⇓ c′  (8)

and (V, Σ_{2}) ⇝ c′. Finally, by (Subst Select) we may derive c ⇓ c′ using (6), (7) and (8).

(Closure Object) Here C = ((S, a), Σ_{0}) and C′ = (ι, Σ_{1}) with a = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}], ι ∉ dom(Σ_{0}), no x_{i} ∈ dom(S) and

Σ_{1} = (ι ↦ [ℓ_{i} = (S, ς(x_{i})b_{i})^{i∈1..n}]) :: Σ_{0}.

So c = (a{{s}}, σ_{0}) where Σ_{0} ⇝ σ_{0} and S ⇝ s. Since the variables x_{i} are bound, we may assume that no x_{i} ∈ dom(S). Therefore we can derive c ⇓ c′ where c′ = (ι, σ_{1}) and

σ_{1} = (ι ↦ [ℓ_{i} = ς(x_{i})(b_{i}{{s}})^{i∈1..n}]) :: σ_{0}

and Σ_{1} ⇝ σ_{1}.

(Closure x) Here C = ((S, x), Σ) and C′ = (V, Σ), with S(x) = V. From C ⇝ c it follows that c = (v, σ) with Σ ⇝ σ,and S(x) ⇝ v. So set c′ = c and we have c ⇓ c′ and C′ ⇝ c′.

The other cases are similar. □

Lemma 6 Suppose C is an initial configuration. Whenever C ⇝ c and c ⇓ c′ there is terminal C′ such that C′ ⇝ c′ and C ⇓ C′.

Proof By induction on the derivation of c ⇓ c′. Either the term in C is a variable, x say, or not. If so, suppose C = ((S, x), Σ). We must have S ⇝ s and Σ ⇝ σ with x ∈ dom(S), and say S(x) = V ⇝ v, so that c = (v, σ) = c′. By (Closure x) we have ((S, x), Σ) ⇓ (V, Σ) as required. Otherwise, the term in C is not a variable and exactly one of the (Subst −) rules applies. Each needs to be considered in turn; we show just one case.

(Subst Select) Here c = (a.ℓ_{j}, σ_{0}) and c′ = (v, σ_{2}) such that

(a, σ_{0}) ⇓ (ι, σ_{1})  (9)
σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}]  (10)
(b_{j}{{ι/x_{j}}}, σ_{1}) ⇓ c′  (11)

with j ∈ 1..n. From C ⇝ c it follows that C = ((S, a′.ℓ_{j}), Σ_{0}) with S ⇝ s, Σ_{0} ⇝ σ_{0} and a = a′{{s}}. By induction hypothesis and (9), there is terminal C_{1} such that

((S, a′), Σ_{0}) ⇓ C_{1}  (12)

and C_{1} ⇝ (ι, σ_{1}). We must have C_{1} = (ι, Σ_{1}) with Σ_{1} ⇝ σ_{1}. By (10), Σ_{1}(ι) ⇝ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] and therefore

Σ_{1}(ι) = [ℓ_{i} = (S_{i}, ς(x_{i})b′_{i})^{i∈1..n}]  (13)

with S_{j} ⇝ s_{j}, b_{j} = b′_{j}{{s_{j}}} and x_{j} ∉ dom(S_{j}). Now since we may derive (((x_{j} ↦ ι) :: S_{j}, b′_{j}), Σ_{1}) ⇝ (b′_{j}{{ι/x_{j}}}, σ_{1}), the induction hypothesis and (11) imply there is C′ with

(((x_{j} ↦ ι) :: S_{j}, b′_{j}), Σ_{1}) ⇓ C′  (14)

and C′ ⇝ c′. Combining (12), (13) and (14) using (Closure Select) we obtain C ⇓ C′ as required.

The other cases are similar. □

Theorem 2 Suppose C and C′ are initial and terminal configurations respectively, and that C ⇝ c and C′ ⇝ c′. Then C ⇓ C′ if and only if c ⇓ c′.

Proof Suppose C ⇓ C′. By Lemma 5 there is c′′ with C′ ⇝ c′′ and c ⇓ c′′. By Proposition 5, c′ = c′′. On the other hand, suppose c ⇓ c′. By Lemma 6, there is a terminal configuration C′′ such that C′′ ⇝ c′ and C ⇓ C′′. By Proposition 5, C′ = C′′. □

2.5 Discussion and Related Work

A big-step closure-based semantics, as in Section 2.4 or, say, the definition of Standard ML, is attractive as a language definition because it directly yields an efficient algorithm for interpreting the calculus. For instance, Cardelli (1995) implements Obliq in this way. On the other hand, substitution-based semantics are simpler to work with when reasoning about program equivalence; we apply the substitution-based semantics of Sections 2.2 and 2.3 in Sections 4 and 5 respectively. In fact, either substitution-based semantics would do alone; we include both for the sake of completeness.

We do not present a small-step closure-based semantics for the imperative object calculus; this would amount to an SECD machine (Landin 1964) for the calculus. The next section, however, contains a small-step closure-based semantics for an object-oriented abstract machine to which we compile the object calculus.

The technique used to prove Theorem 1, the consistency of the two substitution-based semantics is well-known. An analogous result is proved by Plotkin (Plotkin 1975), who also proves the consistency with the SECD machine of what amounts to a big-step substitution-based operational semantics. On the other hand, the proof technique of Theorem 2, the consistency of the substitution-based and closure-based big-step semantics, appears to be new, though the idea of unloading a closure to a term goes back to Plotkin (Plotkin 1975). There is a proof by Felleisen and Friedman (Felleisen and Friedman 1989) of the equivalence of substitution-based and closure-based semantics for an imperative λ-calculus, but they work with small-step rather than bigstep semantics.

3 Compilation to an Abstract Machine

In this section we present an abstract machine, based on the ZAM (Leroy 1990), for the extended calculus of imperative objects, a compiler sending the object calculus to the instruction set of the abstract machine and a correctness result, Theorem 3. The proof depends on an unloading procedure which converts configurations of the abstract machine back into configurations of the object calculus from Section 2. The unloading procedure depends on a modified abstract machine whose argument stack and environment contain object calculus terms as well as locations.

3.1 The Abstract Machine

The machine defined here is based on Leroy’s ZAM. The ZAM was designed for efficient evaluation of curried functions. The machine configuration consists of a state paired with a store. A store is a finite map from locations to stored objects. A state is a quadruple, (ops, AS, E, RS), consisting of a list of instructions (or operations), ops, an argument stack, AS, an environment, E, and a return stack, RS. The instruction list is obtained from compiling some source term. Each item on the argument stack is either a value, V, or a mark, ♢. A value is either the location, ι, of an object in the store, or a closure, (ops, E), which is an operation list ops paired with an environment E. A mark is a special tag introduced by Leroy for efficient evaluation of functions. An environment is a list of values that represents the runtime values assumed by variables free in the original source term. The return stack is a list of frames representing the currently active method invocations and function calls. A frame is simply a closure.

To call a function a mark is pushed onto the stack, the arguments are evaluated and pushed onto the stack and the code for the function body is called. The body of the function can read in (curried) arguments off the stack, and discovers when it has consumed all its arguments when it finds the mark. If the function returns (on executing a return instruction) and there are more arguments to consume, the result of the function (which must itself be a function if execution is to proceed) is called, and will consume the extra arguments that are available.

The instruction set of our abstract machine consists of the following operations.

op ::= operation access i variable access object[(ℓ_{i}, ops_{i})^{i∈1..n}] object construction select ℓ method invocation update(ℓ, ops) method update let ops let cur ops build function closure apply apply function grab get curried argument pushmark push mark onto stack return return from function

ops ::= [] | op :: ops

We describe the workings of our machine informally as follows:

• The instruction access i fetches the ith value in the current environment, and pushes it onto the argument stack. It is used for looking up the value of a variable.

• The instruction object[(ℓ_{i}, ops_{i})^{i∈1..n}] creates a new object in the store, and pushes the location of the newly created object onto the argument stack. The ℓ_{i} are method labels and the ops_{i} are the corresponding compiled methods.

• The instruction selectℓ pops the location of an object off the argument stack, and loads from the object the method closure (ops, E) labelled ℓ. The current operation list and environment are saved by pushing them as a pair onto the return stack, and then are replaced by the new operation list ops and the new environment E.

• The instruction update(ℓ, ops) pops the location of an object off the argument stack, and updates the method closure labelled ℓ in that object with the closure (ops, E), where E is the current environment.

• The instruction let ops pops a value off the argument stack, and adds it to the environment. The instructions ops are then executed in the new environment. A frame built from the remainder of the operation list and the current environment is pushed onto the return stack, to be executed once the instructions ops have been completed.

• The instruction cur ops pushes a function closure onto the argument stack. The closure is built by pairing the compiled function body, ops, with the current environment.

• The instruction apply pops a function closure and value off the argument stack. The current operation list and environment are pushed as a frame onto the return stack, and the closure is executed with the value (the argument to the function) added to its environment.

• The instruction pushmark pushes a mark, ♢, onto the argument stack. This instruction is used to delimit a series of curried arguments to a function.

• The instruction grab examines the top of the argument stack. If the top of the argument stack is a mark, ♢, the grab instruction builds the current state into a closure and returns to the function caller by popping a frame off the return stack. Otherwise, if the top of the argument stack is a value, the value is added to the environment and the execution of the function proceeds. The grab instruction starts the compiled form of a nested function. For example, in the term λ(x)λ(y)a, the compilation of the λ(y)a term will start with a grab instruction.

• The instruction return can be considered a dual to grab. When return is executed (at the end of a function call), the value the function is returning is on the top of the argument stack. If the return value is a function, and this function is being applied directly to an argument, the value will be second on the argument stack. In this case, return will perform the function application without returning to the original function caller. On the other hand, if the return value is not being applied to an argument, a mark, ♢, will be second on the argument stack. In this case, the mark is removed and the function caller is popped back off the return stack.

We now give a formal definition of the abstract machine. An abstract machine configuration, C or D, is a pair (P, Σ), where P is a state and Σ is a store, given as follows:

P, Q ::= (ops, E, AS, RS) machine state U, V ::= ι | fun(ops, E) value U^{♢}, V^{♢} ::= U | ♢ value or mark E ::= [U_{i} ^{i∈1..n}] environment AS ::= [U_{i}^{♢} ^{i∈1..n}] argument stack RS ::= [F_{i} ^{i∈1..n}] return stack F ::= (ops, E) closure or frame O ::= [(ℓ_{i}, F_{i})^{i∈1..n}] stored object (ℓ_{i} distinct) Σ ::= [ι_{i} ↦ O_{i} ^{i∈1..n}] store (ι_{i} distinct)

In a configuration ((ops, E, AS, RS), Σ), ops is the current program. Environment E contains variable bindings. Argument stack AS contains results of evaluating terms and control flow information in the form of marks, ♢. Return stack RS holds return addresses during function calls and method invocations. Store Σ associates locations with objects.

Two transition relations, given next, represent execution of the abstract machine. A β-transition, P ⟶^{β} Q, corresponds directly to a reduction in the object calculus. A τ-transition, P ⟶^{τ} Q, is an internal step of the abstract machine, for example a method return or a variable lookup. Lemma 17 relates reductions of the object calculus and transitions of the abstract machine. (τ Return) (([], E, AS, (ops, E′) :: RS), Σ) ⟶^{τ} ((ops, E′, AS, RS), Σ). (τ Function Return) (([return], E, U :: ♢:: AS, (ops, E′) :: RS), Σ) ⟶^{τ}

((ops, E′, U :: AS, RS), Σ). (β Function Return) (([return], E, fun(ops, E′) :: U :: AS, RS), Σ) ⟶^{β}

((ops, U :: E′, AS, RS), Σ). (τ Grab) ((grab :: ops, E, ♢:: AS, (ops′, E′) :: RS), Σ) ⟶^{τ}

((ops′, E′, fun(ops, E) :: AS, RS), Σ). (β Grab) ((grab :: ops, E, U :: AS, RS), Σ) ⟶^{β} ((ops, U :: E, AS, RS), Σ). (τ Access) ((access j :: ops, E, AS, RS), Σ) ⟶^{τ} ((ops, E, U_{j} :: AS, RS), Σ)

if E = [U_{i} ^{i∈1..n}] and j ∈ 1..n. (τ Pushmark)

((pushmark :: ops, E, AS, RS), Σ) ⟶^{τ} ((ops, E, ♢:: AS, RS), Σ). (τ Cur) ((cur ops :: ops′, E, AS, RS), Σ) ⟶^{τ}

((ops′, E, fun(ops, E) :: AS, RS), Σ). (β Clone) ((clone :: ops, E, ι:: AS, RS), Σ) ⟶^{β} ((ops, E, ι′ :: AS, RS), Σ′)

if Σ(ι) = O and Σ′ = (ι′ ↦ O) :: Σ and ι′ ∉ dom(Σ). (β Object) ((object[(ℓ_{i}, ops_{i})^{i∈1..n}] :: ops, E, AS, RS), Σ) ⟶^{β}

((ops, E, ι:: AS, RS), (ι ↦ [(ℓ_{i}(ops_{i}, E))^{i∈1..n}]) :: Σ) if ι ∉ dom(Σ). (β Select) ((select ℓ_{j} :: ops, E, ι:: AS, RS), Σ) ⟶^{β}

((ops_{j}, ι:: E_{j}, AS, (ops, E) :: RS), Σ)

if Σ(ι) = [(ℓ_{i}, (ops_{i}, E_{i}))^{i∈1..n}] and j ∈ 1..n.

(β Update)

((update(ℓ, ops′) :: ops, E, ι:: AS, RS), Σ) ⟶^{β} ((ops, E, ι:: AS, RS), Σ′) if Σ(ι) = O@[(ℓ, F)]@O′ and Σ′ = Σ + (ι ↦ O@[(ℓ, (ops′, E))]@O′).

(β Let) ((let ops′ :: ops, E, U :: AS, RS), Σ) ⟶^{β} ((ops′, U :: E, AS, (ops, E) :: RS), Σ).

(β Apply) ((apply :: ops, E, fun(ops′, E′) :: U :: AS, RS), Σ) ⟶^{β} ((ops′, U :: E′, AS, (ops, E) :: RS), Σ).

Let C ⟶^{βτ} D if C ⟶^{β} D or C ⟶^{τ} D.

We now describe compilation of the object calculus to the instruction set of our abstract machine. We use the notation grab^{n} for the list [grab, grab, …, grab] consisting of n grab instructions, and the notation λ(x_{1}x_{2} … x_{n})a for the term λ(x_{1})λ(x_{2}) … λ(x_{n})a when n > 0 and a when n = 0. We represent compilation of a term a to an operation list ops by the judgment xs ⊢ a ⇒ ops, defined by the following rules. The variable list xs includes all the free variables of a; it is needed to compute the de Bruijn index of each variable occurring in a.

(Trans Var) [x_{i} ^{i∈1..n}] ⊢ x_{j} ⇒ [access j] if j ∈ 1..n.

(Trans Object) xs ⊢ [ℓ_{i} = ς(y_{i})a_{i} ^{i∈1..n}] ⇒ [object[(ℓ_{i}, ops_{i})^{i∈1..n}]] if y_{i} :: xs ⊢ a_{i} ⇒ ops_{i} and y_{i} ∉ xs for all i ∈ 1..n.

(Trans Select) xs ⊢ a.ℓ ⇒ ops@[select ℓ] if xs ⊢ a ⇒ ops.

(Trans Update) xs ⊢ (a.ℓ ⇐ ς(x)a′) ⇒ ops@[update(ℓ, ops′)] if xs ⊢ a ⇒ ops and x:: xs ⊢ a′ ⇒ ops′ and x ∉ xs.

(Trans Clone) xs ⊢ clone(a) ⇒ ops@[clone] if xs ⊢ a ⇒ ops.

(Trans Let) xs ⊢ let x = a in a′ ⇒ ops@[let ops′] if xs ⊢ a ⇒ ops and x:: xs ⊢ a′ ⇒ ops′ and x ∉ xs.

(Trans Apply) xs ⊢ (a_{1}a_{2} … a_{n}) ⇒ pushmark :: ops_{n} @ ops_{n−1} @ … @ ops_{1}@[apply] if xs ⊢ a_{i} ⇒ ops_{i} for all i ∈ 1..n and a_{1} is not a function application.

(Trans Function) xs ⊢ λ(x_{n+1}x_{n} … x_{1})a ⇒ [cur(grab^{n} @ ops @ [return])] if x_{i} ∉ xs for all i ∈ 1..n + 1, all the x_{i} are distinct, a is not a λ

abstraction and [x_{i} ^{i∈1..n+1}]@xs ⊢ a ⇒ ops.

3.2 Examples of Compilation and Execution

We illustrate compilation and execution via three examples.

Example 1: Method invocation

As a first example, let the term a = pair([], []).fst, (pair was defined in Section 2.1). We have [] ⊢ a ⇒ ops, where the operation list ops is given by:

ops = [object[(fst, ops_{1}), (snd, ops_{2}), (swap, ops_{3})], select fst]
ops_{1} = [object[]]
ops_{2} = [object[]]
ops_{3} = [access 1, select fst, let ops_{4}]
ops_{4} = [access 2, select snd, let ops_{5}]

   ops_{5} = [access 3, update(fst, [access 2]), update(snd, [access 3])]

If we load ops into an empty machine configuration we get the following computation.

((ops, [], [], []), [])

⟶^{β} (([select fst], [], [ι_{1}], []), Σ_{1}) by (β Object)
where Σ_{1} = [ι_{1} ↦ [(fst, ops_{1}), (snd, ops_{2}), (swap, ops_{3})]]
⟶^{β} ((ops_{1}, [ι_{1}], [], [([], [])]), Σ_{1}) by (β Select)
⟶^{β} (([], [ι_{1}], [ι_{2}], [([], [])]), Σ_{2}) by (β Object)
where Σ_{2} = (ι_{2} ↦ []) :: Σ_{1}
⟶^{τ} (([], [], [ι_{2}], []), Σ_{2}) by (τ Return)

When the abstract machine terminates, the answer to the computation can be found as the single item on the argument stack. In this case, the terminal configuration (([], [], [ι_{2}], []), Σ_{2}). The location ι_{2} returned on the argument stack references an empty object in the store.

Example 2: ZAM-Style Function Call

As a second example, let the term a = (λ(x)x)(λ(x)[])[]. We have [] ⊢ a ⇒ ops, where the operation list ops is given by:

         ops = [pushmark, object[], cur ops_{2}, cur ops_{1}, apply]
        ops_{1} = [access 1, return]
        ops_{2} = [object[], return]

If we load ops into an empty machine configuration we get the following computation.

((ops, [], [], []), [])

⟶^{τ} (([object[], cur ops_{2}, cur ops_{1}, apply], [], [♢], []), [])

by (τ Pushmark)

⟶^{τ} (([cur ops_{2}, cur ops_{1}, apply], [], [ι_{1}, ♢], []), Σ_{1} =^{def} [ι_{1} ↦ []])

by (β Object)

⟶^{τ} (([cur ops_{1}, apply], [], [fun(ops_{2}, []), ι_{1}, ♢], []), Σ_{1})

by (τ Cur)

⟶^{τ} (([apply], [], [fun(ops_{1}, []), fun(ops_{2}, []), ι_{1}, ♢], []), Σ_{1})

by (τ Cur)

⟶^{β} ((ops_{1}, [fun(ops_{2}, [])], [ι_{1}, ♢], [([], [])]), Σ_{1}) by (β Apply)
⟶^{τ} (([return], [fun(ops_{2}, [])], [fun(ops_{2}, []), ι_{1}, ♢], [([], [])]), Σ_{1})

by (τ Access)

⟶^{β} ((ops_{2}, [ι_{1}], [♢], [([], [])]), Σ_{1}) by (β Function Return)
⟶^{τ} (([return], [ι_{1}], [ι_{2}, ♢], [([], [])]), Σ_{2} =^{def} (ι_{2} ↦ []) :: Σ_{1})

by (β Object)

⟶^{τ} (([], [], [ι_{2}], []), Σ_{2}) by (τ Function Return)

We see in this example the mechanism for function application, and in particular how, like the ZAM, our abstract machine uses a mark on the stack to delimit a series of arguments to a function.

The function call begins with the (τ Pushmark) τ-transition. The abstract machine evaluates applications in a right-to-left fashion, pushing the results of evaluating the arguments onto the argument stack. The closure representing the function to be called is pushed onto the argument stack, and the (β Apply) β-transition starts the body of the function λ(x)x applied to the first argument and pushes an entry on the return stack. During the (β Function Return) β-transition, which does not touch the return stack, the outcome of this application gets applied to the second curried argument. The (τ Function Return) τ-transition completes the application by popping the entry off the return stack.

In the terminal configuration, (([], [], [ι_{2}], []), Σ_{2}) we have a location ι_{2} on the argument stack. At location ι_{2} in the store Σ_{2} is an empty object []. This evaluation produces some garbage in the store, at location ι_{1}.

Example 3: ZAM-Style Curried Function Call

As a third example, let the term a = (λ(xyz)x)[][]. We have [] ⊢ a ⇒ ops, where the operation list ops is given by:

        ops = [pushmark, object[], object[], cur(ops_{1}), apply]
       ops_{1} = [grab, grab, access 3, return]

If we load ops into an empty machine configuration we get the following computation.

((ops, [], [], []), [])

⟶^{τ} (([object[], object[], cur(ops_{1}), apply], [], [♢], []), [])

by (τ Pushmark)

⟶^{β} (([object[], cur(ops_{1}), apply], [], [ι_{1}, ♢], []), Σ_{1}) by (β Object)

where Σ_{1} = [ι_{1} ↦ []]

⟶^{β} (([cur(ops_{1}), apply], [], [ι_{2}, ι_{1}, ♢], []), Σ_{2}) by (β Object)

where Σ_{2} = [ι_{1} ↦ [], ι_{2} ↦ []]

⟶^{τ} (([apply], [], [fun(ops_{1}, []), ι_{2}, ι_{1}, ♢], []), Σ_{2}) by (τ Cur)
⟶^{β} ((ops_{1}, [ι_{2}], [ι_{1}, ♢], [([], [])]), Σ_{2}) by (β Apply)
⟶^{β} (([grab, access 3, return], [ι_{1}, ι_{2}], [♢], [([], [])]), Σ_{2}) by (β Grab)
⟶^{τ} (([], [], [fun([access 3, return], [ι_{1}, ι_{2}])], []), Σ_{2}) by (τ Grab)

Consider the transitions corresponding to the application of the function λ(xyz)x to its two curried arguments [] and []. The curried call begins with the (τ Pushmark) τ-transition, which pushes a mark, ♢, onto the argument stack. After the two arguments have been evaluated, the (β Apply) β-transition starts the body of the function λ(xyz)x applied to the first curried argument, [], and pushes an entry on the return stack. The (β Grab) β-transition applies the curried function λ(yz)x to the second argument, []. The second grab instruction finds a mark on the stack indicating there are no more arguments to be consumed, so causes a (τ Grab) τ-transition, which builds a closure and returns, popping an entry off the return stack.

The terminal configuration is:

(([], [], [fun([access 3, return], [ι_{1}, ι_{2}])], []), Σ_{2})

We will show formally in Section 3.4 that the function closure returned on the argument stack, fun([access 3, return], [ι_{1}, ι_{2}]), represents the function λ(z)ι_{2}.

3.3 The Unloading Machine

To prove the abstract machine and compiler correct, we need to convert back from a machine state to an object calculus term. To do so, we load the state into a modified abstract machine, the unloading machine, and when this unloading machine terminates, its argument stack contains a single term that is a decompiled version of the original state.

The unloading machine is like the abstract machine, except that instead of executing each instruction, it reconstructs the corresponding source term. Since no store lookups or updates are performed, the unloading machine does not act on a store. An unloading machine state is like an abstract machine state, except that values are generalised to arbitrary terms. Let an unloading machine state, p or q, be a quadruple (ops, e, as, RS) where e and as are defined as follows:

e ::= [a_{i} ^{i∈1..n}] unloading environment a^{♢}, b^{♢} ::= a | ♢ term or mark as ::= [a_{i}^{♢} ^{i∈1..n}] unloading stack

Next we make a simultaneous inductive definition of a u-transition relation p ⟶^{u} p′, and three unloading relations: (ops, e) ⇝ (x)b, that unloads a method closure to a method, fun(ops, e) ⇝ λ(x)b, that unloads a function closure to a λ-abstraction and [U_{i}^{♢} ^{i∈1..n}] ⇝ [a_{i}^{♢} ^{i∈1..n}], that unloads a list.

(u Access) (access j :: ops′, e, as, RS) ⟶^{u} (ops′, e, a_{j} :: as, RS) if j ∈ 1..n and e = [a_{i} ^{i∈1..n}].

(u Object) (object[(ℓ_{i}, ops_{i})^{i∈1..n}] :: ops′, e, as, RS) ⟶^{u} (ops′, e, [ℓ_{i} = ς(x_{i})b_{i}^{i∈1..n}]::as, RS) if (ops_{i}, e) ⇝ (x_{i})b_{i} for each i ∈ 1..n.

(u Clone) (clone :: ops′, e, a:: as, RS) ⟶^{u} (ops′, e, (clone(a)) :: as, RS).

(u Select) (select ℓ:: ops′, e, a:: as, RS) ⟶^{u} (ops′, e, (a.ℓ) :: as, RS).

(u Update) (update(ℓ, ops) :: ops′, e, a:: as, RS) ⟶^{u} (ops′, e, (a.ℓ ⇐ ς(x)b) :: as, RS) if (ops, e) ⇝ (x)b.

(u Let) (let(ops′)::ops′′, e, a::as, RS) ⟶^{u} (ops′′, e, (let x = a in b)::as, RS) if (ops′, e) ⇝ (x)b.

(u Return) ([], e, as, (ops, E) :: RS) ⟶^{u} (ops, e′, as, RS)

if E ⇝ e′.

(u Cur) (cur ops :: ops′, e, as, RS) ⟶^{u} (ops′, e, (λ(x)a) :: as, RS) if fun(ops, e) ⇝ λ(x)a.

(u Function Return) ([return], e, [a_{i} ^{i∈1..n}]@[♢]@as, RS) ⟶^{u} ([], e, (a_{1}(a_{2}) ⋯ (a_{n})) :: as, RS).

(u Grab) (grab :: ops, e, as, RS) ⟶^{u} ([return], e, (λ(x)a) :: as, RS) if fun(ops, e) ⇝ λ(x)a.

(u Apply) (apply :: ops, e, [a_{i} ^{i∈1..n}]@[♢]@as, RS) ⟶^{u} (ops, e, (a_{1}a_{2} … a_{n}) :: as, RS).

(u Pushmark) (pushmark :: ops, e, as, RS) ⟶^{u} (ops, e, ♢:: as, RS).

(Unload Abstraction) (ops, e) ⇝ (x)b if x ∉ fv(e) and (ops, x:: e, [], []) ⟶^{u}^{∗} ([], e′, [b], []).

(Unload Closure) fun(ops, e) ⇝ λ(x)b if x ∉ fv(e) and (ops, x:: e, [♢], []) ⟶^{u}^{∗} ([], e′, [b], []).

(Unload List Empty) [] ⇝ [].

(Unload List Loc) ι:: [U_{i}^{♢} ^{i∈1..n}] ⇝ ι:: [a_{i}^{♢} ^{i∈1..n}] if [U_{i}^{♢} ^{i∈1..n}] ⇝ [a_{i}^{♢} ^{i∈1..n}].

(Unload List Closure) fun(ops, E) :: [U_{i}^{♢} ^{i∈1..n}] ⇝ (λ(x)a) :: [a_{i}^{♢} ^{i∈1..n}] if [U_{i}^{♢} ^{i∈1..n}] ⇝ [a_{i}^{♢} ^{i∈1..n}], E ⇝ e and fun(ops, e) ⇝ λ(x)a.

(Unload List Mark) ♢:: [U_{i}^{♢} ^{i∈1..n}] ⇝ ♢:: [a_{i}^{♢} ^{i∈1..n}] if [U_{i}^{♢} ^{i∈1..n}] ⇝ [a_{i}^{♢} ^{i∈1..n}].

We complete the machine with the following unloading relations: O ⇝ o (on objects), Σ ⇝ σ (on stores) and C ⇝ c (on configurations).

(Unload Object) [(ℓ_{i}, (ops_{i}, E_{i}))^{i∈1..n}] ⇝ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] if E_{i} ⇝ e_{i} and (ops_{i}, e_{i}) ⇝ (x_{i})b_{i} for all i ∈ 1..n.

(Unload Store) [ι_{i} ↦ O_{i} ^{i∈1..n}] ⇝ [ι_{i} ↦ o_{i} ^{i∈1..n}] if O_{i} ⇝ o_{i} for all i ∈ 1..n.

(Unload Config) ((ops, E, AS, RS), Σ) ⇝ (a, σ)

if Σ ⇝ σ, E ⇝ e, AS ⇝ as and (ops, e, as, RS) ⟶^{u}^{∗} ([], e′, [a], []).

Let p ⇝ a if and only if there is e such that p ⟶^{u}^{∗} ([], e, [a], []). We say P ↓ p if P = (ops, E, AS, RS), p = (ops, e, as, RS), E ⇝ e and AS ⇝ as. Therefore (P, Σ) ⇝ (a, σ) if and only if P ↓ p, p ⇝ a and Σ ⇝ σ.

3.4 Examples of Unloading

To clarify the workings of the unloading machine, we present some examples. We unload some of the abstract machine states of the examples in Section 3.2.

Example 1: Unloading a Compiled Term

Recall from Example 3 of Section 3.2 the configuration ((ops, [], [], []), []), where

        ops = [pushmark, object[], object[], cur(ops_{1}), apply]
       ops_{1} = [grab, grab, access 3, return]

We know already that [] ⊢ (λ(xyz)x)[][] ⇒ ops.

We aim to prove ((ops, [], [], []), []) ⇝ ((λ(xyz)x)[][], []). We build up to this result in four steps. The first step corresponds to unloading the body of the function λ(xyz)x and each subsequent step will build a function whose body is the result of the previous step. Bound names are lost in translation, but since we identify terms up to alpha conversion, we choose variables in this example so that the unloaded term is the same as the original term.

(1) We compute:

([access 3, return], [z, y, x], [♢], [])
⟶^{u} ([return], [z, y, x], [x, ♢], []) by (u Access)
⟶^{u} ([], [z, y, x], [x], []) by (u Function Return)

By rule (Unload Closure), we get:

fun([access 3, return], [y, x]) ⇝ λ(z)x

(2) Hence, we compute:

([grab, access 3, return], [y, x], [♢], [])
⟶^{u} ([return], [y, x], [λ(z)x, ♢], []) by (u Grab)
⟶^{u} ([], [y, x], [λ(z)x], []) by (u Function Return)

By (Unload Closure), we get:

fun([grab, access 3, return], [x]) ⇝ λ(yz)x

(3) Hence, we compute:

(ops_{1}, [x], [♢], [])
⟶^{u} ([return], [x], [(λ(yz)x), ♢], []) by (u Grab)
⟶^{u} ([], [x], [λ(yz)x], []) by (u Function Return)

Again by (Unload Closure), we get:

fun([grab, grab, access 3, return], []) ⇝ λ(xyz)x (4) Below, the result of step (3) is used in the (u Cur) step:

(ops, [], [], [])

⟶^{u} ([object[], object[], cur(ops_{1}), apply], [], [♢], [])

by (u Pushmark)

⟶^{u} ([object[], cur(ops_{1}), apply], [], [[], ♢], []) by (u Object)
⟶^{u} ([cur(ops_{1}), apply], [], [[], [], ♢], []) by (u Object)
⟶^{u} ([apply], [], [(λ(xyz)x), [], [], ♢], []) by (u Cur)
⟶^{u} ([], [], [(λ(xyz)x)[][]], []) by (u Apply)

The terminal configuration of the unloading machine has our original expression (λ(xyz)x)[][] on the stack. Hence by (Unload Config) we have ((ops, [], [], []), []) ⇝ ((λ(xyz)x)[][], []) as desired.

Example 2: Unloading a Terminal Configuration

For the next example, we unload the terminal configuration of Example 3 of Section 3.2, (([], [], [fun([access 3, return], [ι_{1}, ι_{2}])], []), Σ_{2}), where Σ_{2} = [ι_{1} ↦ [], ι_{2} ↦ []].

From rule (Unload Store) we have Σ_{2} ⇝ σ_{2} = [ι_{1} ↦ [], ι_{2} ↦ []]. To unload the closure fun([access 3, return], [ι_{1}, ι_{2}]), we calculate:

([access 3, return], [z, ι_{1}, ι_{2}], [♢], [])
⟶^{u} ([return], [z, ι_{1}, ι_{2}], [ι_{2}, ♢], []) by (u Access)
⟶^{u} ([], [z, ι_{1}, ι_{2}], [ι_{2}], []) by (u Function Return)

By rule (Unload Closure) we get:

fun([access 3, return], [ι_{1}, ι_{2}]) ⇝ λ(z)ι_{2}

From rules (Unload List Closure) and (Unload List Empty) we get that the argument stack unloads as follows:

[fun([access 3, return], [ι_{1}, ι_{2}])] ⇝ [λ(z)ι_{2}]

Finally, by (Unload Config) we deduce:

(([], [], [fun([access 3, return], [ι_{1}, ι_{2}])], []), Σ_{2}) ⇝ (λ(z)ι_{2}, σ_{2})

Combining the working from this section and Section 3.2, we have shown that unloading the outcome of compiling and executing the term (λ(xyz)x)[][], yields the configuration (λ(z)ι_{2}, [ι_{1} ↦ [], ι_{2} ↦ []]).

Example 3: Unloading an Intermediate Configuration

For a final example, we consider an intermediate configuration obtained from the evaluation of (λ(x)x.ℓ)[ℓ = ς(s)λ(y)y][] in the abstract machine. The configuration we will unload is:

(([select ℓ, return], [ι_{2}], [ι_{2}, ι_{1}, ♢], [([], [])]), Σ_{2})

where

Σ_{2} = [ι_{1} ↦ [], ι_{2} ↦ [(ℓ, ([cur([access 1, return])], []))]]

We first unload the store:

• We compute:

([access 1, return], [y, s], [♢], [])
⟶^{u} ([return], [y, s], [y, ♢], []) by (u Access)
⟶^{u} ([], [y, s], [y], []) by (u Function Return)

So by rule (Unload Closure), fun([access 1, return], [s]) ⇝ λ(y)y.

• Hence, we get:

([cur([access 1, return])], [s], [], []) ⟶^{u} ([], [s], [λ(y)y], [])

By (Unload Abstraction) we get:

([cur([access 1, return])], []) ⇝ (s)λ(y)y

• Hence by rule (Unload Store):

Σ_{2} ⇝ [ι_{1} ↦ [], ι_{2} ↦ [ℓ = ς(s)λ(y)y]]

To unload the other component of the configuration, we compute:

([select ℓ, return], [ι_{2}], [ι_{2}, ι_{1}, ♢], [([], [])])
⟶^{u} ([return], [ι_{2}], [ι_{2}.ℓ, ι_{1}, ♢], [([], [])]) by (u Select)
⟶^{u} ([], [ι_{2}], [(ι_{2}.ℓ)ι_{1}], [([], [])]) by (u Function Return)
⟶^{u} ([], [], [(ι_{2}.ℓ)ι_{1}], []) by (u Return)

By rule (Unload Config) we deduce:

(([select ℓ, return], [ι_{2}], [ι_{2}, ι_{1}, ♢], [([], [])]), Σ_{2})
⇝ ((ι_{2}.ℓ)ι_{1}, [ι_{1} ↦ [], ι_{2} ↦ [ℓ = ς(s)λ(y)y]])

3.5 Correctness of the Abstract Machine

We start with a lemma which shows that the unloading machine is independent of the terms in its environment and on its stack. Define the shape of (ops, e, as′, RS) to be the quadruple (ops, |e|, |as|, RS), and write shape p for the shape of p. We say two stacks [a_{i}^{♢}^{i∈1..n}] and [b_{i}^{♢}^{i∈1..m}] are mark-equivalent if and only if n = m and a_{j}^{♢} = ♢ if and only if b_{j}^{♢} = ♢. We say p and q are shape-mark-equivalent if shape p = shape q and the argument stack of p is mark-equivalent to that of q.

Lemma 7 If p ⟶^{u} p′ and p is shape-mark-equivalent to q then there is a q′ with q ⟶^{u} q′ and p′ is shape-mark-equivalent to q′.

Proof This is proved by induction on the derivation of p ⟶^{u} p′. For example, if p = (let ops′:: ops′′, e, a:: as, RS) then p′ = (ops′′, e, [let x = a in b] :: as, RS) where (ops′′, e) ⇝ (x)b. Let q = (letops′::ops′′, e′, a′::as′, RS) where |e′| = |e|, |as| = |as′| and as is mark-equivalent to as′. (ops′′, e) ⇝ (x)b means that there are p_{j} for j ∈ 1..n with p_{1} = (ops′′, x :: e, [], []), p_{n} = ([], e′′, [b], []) and for all j ∈ 1..n − 1 p_{j} ⟶^{u} p_{j+1}. Then we can apply the inductive hypothesis to get q_{i} for j ∈ 1..n with q_{1} = (ops′′, x:: e′, [], []), q_{n} = ([], e′′′, [b′], []) and for all j ∈ 1..n − 1 q_{j} ⟶^{u} q_{j+1}. Hence (ops′′, e′) ⇝ (x)b′. By (u Let) q ⟶^{u} q′ = (ops′′, e′, [let x = a′ in b′] :: as′, RS) and p′ is shapemark-equivalent to q′. □

A corollary of Lemma 7 is the following:

Lemma 8 If p ⇝ a then for all q with p and q shape-mark-equivalent, there is an a′ with q ⇝ a′.

Proof p ⇝ a means that there is a sequence of reductions

p ⟶^{u} p_{1} ⟶^{u} ⋯ ⟶^{u} p_{n}

where p_{n} is of the form ([], e, [a], []). Applying Lemma 7 inductively to this chain gives a new chain of reductions

q ⟶^{u} q_{1} ⟶^{u} ⋯ ⟶^{u} q_{n}

where q_{n} is of the form ([], e′, [a′], []), and hence q ⇝ a′. □

The following lemma describes some of the behaviour of the stacks of the unloading machine.

Lemma 9

(1) If (ops, e, as, []) ⟶^{u} (ops′, e′, as′, []) then for all as′′ and for all RS,

(ops, e, as@as′′, RS) ⟶^{u} (ops′, e′, as′@as′′, RS).

(2) For all ops and op ≠ grab, ([op], e, as, []) ⟶^{u} ([], e′, as′, []) if and only if we have the transition (op :: ops, e, as, []) ⟶^{u} (ops, e′, as′, []).

(3) If ([op_{i}^{i∈1..n}], e, as, [])⟶^{u}^{∗} ([], e_{1}, as_{1}, []) and op_{i} = grab for no i ∈ 1..n,

then ([op_{i} ^{i∈1..n}]@ops′, e, as, []) ⟶^{u}^{∗} (ops′, e, as_{1}, []).

Proof Inspecting the rules for u transitions gives (1) and (2). To prove (3), we note that no u-transition increases RS, and induct on n, applying (2). □

To assist in the use of part (3) of the previous lemma, we have a lemma limiting the occurrences of grab instructions. In particular, it says no grab instruction can occur at the top level.

Lemma 10 If xs ⊢ a ⇒ [op_{i} ^{i∈1..n}] then op_{i} = grab for no i ∈ 1..n.

Proof Immediate from the definition of the xs ⊢ a ⇒ ops predicate. □

We aim to show that unloading is an inverse to compilation. We prove a more general fact first.

Lemma 11 If x_{i} ^{i∈1..n} ⊢ a ⇒ ops then for all b_{i} ^{i∈1..n}

(ops, [b_{i} ^{i∈1..n}], [], []) ⟶^{u}^{∗} ([], [b_{i} ^{i∈1..n}], [a{{b^{i}/x_{i}^{i∈1..n}}}], [])

Proof We prove this by induction on the derivation of x_{i} ^{i∈1..n} ⊢ a ⇒ ops, considering each of the Trans rules individually. Consider any terms b_{1} … b_{n}.

(Trans Var) Here a = x_{j}, where j ∈ 1..n. Then x_{i} ^{i∈1..n} ⊢ a ⇒ [access j] and ([access j], [b_{i} ^{i∈1..n}], [], []) ⟶^{u} ([], [b_{i} ^{i∈1..n}], [b_{j}], [])

(Trans Select) Here a = a′.ℓ. We have an ops′ with x_{i} ^{i∈1..n} ⊢ a′ ⇒ ops′. Then x_{i} ^{i∈1..n} ⊢ a ⇒ ops′@[select ℓ]. By rule induction we have that

(ops′, [b_{i} ^{i∈1..n}], [], []) ⟶^{u}^{∗} ([], [b_{i} ^{i∈1..n}], [a′′], []), where a′′ = a′{{b^{i}/x_{i}^{i∈1..n}}}.

We calculate:

(ops′@[select ℓ], [b_{i} ^{i∈1..n}], [], [])

⟶^{u}^{∗} ([select ℓ], [b_{i} ^{i∈1..n}], [a′′], []) by Lemmas 9(3) and 10
⟶^{u} ([], [b_{i} ^{i∈1..n}], [a′′.ℓ], []) by (u Select)

This suffices, since we have a′′.ℓ = (a′{{b^{i}/x_{i}^{i∈1..n}}}).ℓ = (a′.ℓ){{b^{i}/x_{i}^{i∈1..n}}}.

(Trans Let) Here a = (let x = a_{1} in a_{2}). Since x is bound, we may assume x ∉ fv(b_{i}) for each i. We have ops_{1}, ops_{2} with x_{i} ^{i∈1..n} ⊢ a_{1} ⇒ ops_{1} and x:: [x_{i} ^{i∈1..n}] ⊢ a_{2} ⇒ ops_{2} (where x ∉ {x_{i} ^{i∈1..n}}). Then x_{i} ^{i∈1..n} ⊢ a ⇒ ops_{1}@[let(ops_{2})]. From the induction hypothesis, [x_{i} ^{i∈1..n}] ⊢ a_{1} ⇒ ops_{1} implies (ops_{1}, [b_{i} ^{i∈1..n}], [], []) ⟶^{u}^{∗} ([], [b_{i} ^{i∈1..n}], [a′_{1}], []) where a′_{1} = a_{1}{{b^{i}/x_{i}^{i∈1..n}}}. The induction hypothesis applied to x:: [x_{i} ^{i∈1..n}] ⊢ a_{2} ⇒ ops_{2} gives (ops_{2}, x::[b_{i}^{i∈1..n}], [], [])⟶^{u}^{∗}([], x::[b_{i}^{i∈1..n}], [a′_{2}], []) where a′_{2} = a_{2}{{x/x}}{{b^{i}/x_{i}^{i∈1..n}}}. By (Unload Abstraction), (ops_{2}, [b_{i} ^{i∈1..n}]) ⇝ (x)a′_{2}. Applying Lemma 9(3) and Lemma 10, we can derive:

(ops_{1}@[let(ops_{2})], [b_{i} ^{i∈1..n}], [], [])
⟶^{u}^{∗} ([let(ops_{2})], [b_{i} ^{i∈1..n}], [a′_{1}], [])
⟶^{u} ([], [b_{i} ^{i∈1..n}], [let x = a′_{1} in a′_{2}], []) by (u Let)

This is sufficient, since (let x = a′_{1} in a′_{2}) = a{{b^{i}/x_{i}^{i∈1..n}}}, because x ∉ fv(b_{i}) for all i.

(Trans Clone) Here a = clone(a′). This follows in the same way as the (Trans Select) case.

(Trans Update) Here a = (a_{1}.ℓ ⇐ ς(x)a_{2}). Derived from x_{i} ^{i∈1..n} ⊢ a_{1} ⇒ ops_{1} and x :: [x_{i} ^{i∈1..n}] ⊢ a_{2} ⇒ ops_{2}, where x ∉ xs, we have x_{i} ^{i∈1..n} ⊢ a ⇒ ops_{1}@[update(ℓ, ops_{2})]. Via reasoning similar to the case of (Trans Let), we calculate: (ops_{1}@[update(ℓ, ops_{2})], [b_{i} ^{i∈1..n}], [], []) ⟶^{u}^{∗} ([], [b_{i} ^{i∈1..n}], [(a′_{1}ℓ ⇐ ς(x)a′_{2})], []) where a′_{1} = a_{1}{{b^{i}/x_{i}^{i∈1..n}}} and a′_{2} = a_{2}{{x:: [b^{i} ^{i∈1..n}]/x:: [x_{i} ^{i∈1..n}]}}. This is sufficient, since a{{b^{i}/x_{i}^{i∈1..n}}} = (a′_{1}.ℓ ⇐ ς(x)a′_{2}).

(Trans Object) Here a = [(ℓ_{i}, ς(y_{i})a_{i})^{i∈1..n}]. If y_{i} :: [x_{i} ^{i∈1..n}] ⊢ a_{i} ⇒ ops_{i} then x_{i} ^{i∈1..n} ⊢ a ⇒ [object[(ℓ_{i}, ops_{i})^{i∈1..n}]]. By rule induction we have that for all i, (ops_{i}, y_{i}::[b_{j} ^{j∈1..n}]) ⇝ (y_{i})a′_{i} where a′_{i} = a_{i}{{b^{j}/x_{j}^{j∈1..n}}} and hence that ([object[(ℓ_{i}, ops_{i})^{i∈1..n}]], [b_{i}^{i∈1..n}], [], []) ⟶^{u} ([], [b_{i}^{i∈1..n}], [ℓ_{i} = ς(y_{i})a′_{i}], []) as required.

(Trans Function) Here a = λ(y_{m+1} … y_{1})b where b is not a function, y_{i} ∉ {x_{j} ^{j∈1..n}} for each i ∈ 1..m + 1, [y_{i} ^{i∈1..m+1}] @ xs ⊢ b ⇒ ops and xs ⊢ a ⇒ [cur(grab^{m} @ ops @ [return])], where xs = [x_{i} ^{i∈1..n}].

Let bs = [b_{i} ^{i∈1..n}] and e_{k} = [y_{i} ^{i∈k..m+1}]@bs for each k ∈ 1..m + 1. We prove by an inner induction on k that for k ∈ 0..m,

([grab^{k} @ ops @ [return]], e_{k+1}, [♢], []) ⟶^{u}^{∗} ([], e_{k+1}, [λ(y_{k} … y_{1})b′], [])

Base case, k = 0: By the outer induction hypothesis of the lemma, [y_{i} ^{i∈1..m+1}] @ xs ⊢ b ⇒ ops implies

(ops, e_{1}, [], []) ⟶^{u}^{∗} ([], e_{1}, [b′], [])

where b′ = b{{y^{i}/y_{i}^{i∈1..m+1}}}{{b^{j}/x_{j}^{j∈1..n}}} = b{{b^{j}/x_{j}^{j∈1..n}}}. We calculate:

(ops @ [return], e_{1}, [♢], [])

⟶^{u}^{∗} ([return], e_{1}, [b′, ♢], []) by Lemma 9(1 and 3)
⟶^{u} ([], e_{1}, [b′], []) by (u Function Return)

Induction case: We assume for the induction, that ([grab^{k} @ ops @

[return]], e_{k+1}, [♢], []) ⟶^{u}^{∗} ([], e_{k+1}, [λ(y_{k} … y_{1})b′], []).

Now, e_{k+1} = y_{k+1} :: e_{k+2}, so by (Unload Closure):

fun([grab^{k} @ ops @ [return]], e_{k+2}) ⇝ λ(y_{k+1})λ(y_{k} … y_{1})b′

Hence

([grab^{k+1} @ ops @ [return]], e_{k+2}, [♢], [])

⟶^{u} ([return], e_{k+2}, [λ(y_{k+1} … y_{1})b′, ♢], []) by (u Grab)
⟶^{u} ([], e_{k+2}, [λ(y_{k+1} … y_{1})b′], []) by (u Function Return)

The k = m case gives ([grab^{m} @ ops @ [return]], y_{m+1} :: bs, [♢], []) ⟶^{u}^{∗} ([], y_{m+1}::bs, [λ(y_{m} … y_{1})b′], []) , so by (u Cur) we deduce ([cur[grab^{m}@ ops, [return]]], bs, [], []) ⟶^{u} ([], bs, [λ(y_{m+1} … y_{1})b′], []) as required.

(Trans Apply) Here a = (a_{1}a_{2} … a_{m}), and [x_{i} ^{i∈1..n}] ⊢ a ⇒ pushmark :: ops_{m}@ops_{m−1}@ … @ops_{1} @ [apply] where for each j ∈ 1..m [x_{i} ^{i∈1..n}] ⊢ a_{j} ⇒ ops_{j}. The induction hypothesis says that for each j ∈ 1..m we have (ops_{j}, [b_{i} ^{i∈1..n}], [], []) ⇝ a_{j}{{b^{i}/x_{i}^{i∈1..n}}}. Lemmas 9(1) and 9(3) give that (pushmark :: ops_{m} @ … @ ops_{1} @ [apply], [b_{i} ^{i∈1..n}], [], []) ⟶^{u}^{∗} p =

([apply], [b_{i} ^{i∈1..n}], [a′_{1}, …, a′_{m}, ♢], []) where a′_{j} = a_{j}{{b^{i}/x_{i}^{i∈1..n}}}. p ⟶^{u}

([], [b_{i} ^{i∈1..n}], [a′], []) where a′ = a{{b^{i}/x_{i}^{i∈1..n}}} as required. □

As a corollary we have that unloading is an inverse to compilation:

Proposition 6 Whenever [] ⊢ a ⇒ ops then ((ops, [], [], []), []) ⇝ (a, []).

The unloading machine preserves substitutions:

Lemma 12 If p ⟶^{u} q then p{{a/x}} ⟶^{u} q{{a/x}}.

Proof By inspecting the u-transition rules. For example, if p = (access j::

ops, [a_{i}^{i∈1..n}], as, RS) and p ⟶^{u} q = (ops, [a_{i}^{i∈1..n}], a_{j}::as, RS), then p{{a/x}} =

(access j :: ops, [a_{i}{{a/x}} ^{i∈1..n}], as{{a/x}}, RS) and by (u Access), p{{a/x}} ⟶^{u}

q{{a/x}} = (ops, [a_{i}{{a/x}}^{i∈1..n}], (a_{j}{{a/x}}) :: as{{a/x}}, RS). □

Lemma 13

(1) If p ⟶^{u} q then fv(q) ⊆ fv(p).

(2) If (ops, e) ⇝ (x)b then fv(b) − {x} ⊆ fv(e).

(3) If fun(ops, e) ⇝ λ(x)b then fv(b) − {x} ⊆ fv(e).

Proof We prove these simultaneously by inducting on the derivation of p ⟶^{u} q, (ops, e) ⇝ (x)b or fun(ops, e) ⇝ λ(x)b. For example, if p = (let ops :: ops′, e, a:: as, RS) and p ⟶^{u} q = (ops′, e, (let x = a in b) :: as, RS) where (ops, e) ⇝ (x)b then by induction, fv(b) − {x} ⊆ fv(e), and so fv(q) = fv(as) ∪ fv(e) ∪ fv(let x = a in b) ⊆ fv(as)fv(e) ∪ fv(a) = fv(p). □

Next, we show that no u transition can prevent unloading, and that the unloading relation ⇝ is deterministic.

Lemma 14 Suppose p ⟶^{u} q. Then for all a, p ⇝ a if and only if q ⇝ a.

Proof By determinacy of ⟶^{u}. □

Lemma 15 Whenever p ⇝ a and p ⇝ a′, a = a′.

Proof Assume p ⇝ a and p ⇝ a′. p ⇝ a′ means p ⟶^{u}^{∗} q = ([], e, [a′], []). By Lemma 14, q ⇝ a. But q cannot perform a u-transition (by inspection of the u-transition rules) and so q ⇝ a′ only. Hence a = a′. □

We now show that the unloading machine preserves reduction contexts under certain conditions. We use u^{♢} and v^{♢} to stand for terms which are either locations, functions or marks (♢).

Lemma 16 If (ops, e, as, RS) ⟶^{u} (ops′, e′, as′, RS′) and as = [a_{i}^{♢} ^{i∈1..n}, R,

u_{j}^{♢} ^{i∈1..m}] where • ∉ fv(e) then • ∉ fv(e′) and as′ = [b_{i}^{♢} ^{i∈1..n′}, R′, v_{j}^{♢} ^{j∈1..m′}] for some R′, b_{i}^{♢} and v_{j}^{♢} (with i ∈ 1..n′, j ∈ 1..m′).

Proof We consider each u-transition in turn.

(u Access) This step pushes a term onto the front of the argument stack, leaving the environment and the remainder of the stack unchanged.

(u Object), (u Cur), (u Pushmark), (u Grab) Similar to (u Access).

(u Clone) Here ops = clone :: ops′. If n = 0, so as = [R, u_{1}^{♢}, …, u_{m}^{♢}] then (ops, e, as, RS) ⟶^{u} (ops′, e, [clone(R), u_{1}^{♢}, …, u_{m}^{♢}], RS) and since clone(R) is a reduction context this satisfies the conditions of the lemma. Otherwise, in the case n > 0, we have that (ops, e, as, RS) ⟶^{u} (ops′, e, [clone(a_{1}^{♢}), a_{2}^{♢}, …, a_{n}^{♢}, R, u_{j}^{♢} ^{j∈1..m}], RS).

(u Select) Here ops = select ℓ:: ops′. Similarly to the (u Clone) case, if n > 0 the conditions are easily satisfied. Otherwise, when n = 0, as =

[R, u_{1}^{♢}, …, u_{m}^{♢}] and (ops, e, as, RS) ⟶^{u} (ops′, e, [R.ℓ, u_{1}^{♢}, …, u_{m}^{♢}], RS),

sufficient since R.ℓ is a reduction context.

(u Let) Here ops = let ops′ :: ops′′. Again, for the n = 0 case, by (u Let) we have (ops′, e) ⇝ (x)b, and as′ = [let x = R in b, u_{1}^{♢}, …, u_{m}^{♢}]. This is sufficient, because (let x = R in b) is a reduction context, since • ∉ fv(b) by Lemma 13.

(u Update) Similar to (u Let).

(u Return) The reduction ([], e, as, (ops, E′) :: RS) ⟶^{u} (ops, e′, as, RS) (where E′ ⇝ e′) leaves the argument stack unchanged, and • ∉ fv(e′) by Lemma 13.

(u Function Return) Let p = ([return], e, as, RS) where we have as = [a_{i}^{♢} ^{i∈1..n}, R, u_{j}^{♢} ^{j∈1..m}]. If a_{k}^{♢} = ♢ and a_{i}^{♢} ≠ ♢ for i < k, then we have

that p ⟶^{u} p′ = ([], e, (a_{1}^{♢} … a_{k−1}^{♢}) :: [u_{k+1}^{♢}, u_{k+2}^{♢}, …, R, u_{j}^{♢} ^{j∈1..m}], RS).

The conditions of the lemma are satisfied by p′.

Otherwise, if a_{i}^{♢} ≠ ♢ for each i ∈ 1..n, then it must be that u_{k}^{♢} = ♢ for some k ∈ 1..m since we are assuming (u Function Return) can be applied to p. We can pick the least such k, so that u_{i}^{♢} ≠ ♢ for i < k

and u_{k}^{♢} = ♢. Now, p ⟶^{u} p′ = ([], e, as′ = (a_{1}^{♢} … a_{n}^{♢}Ru_{1}^{♢} … u_{k−1}^{♢}) ::

[u_{k+1}^{♢}, …, u_{m}^{♢}], RS). The term at the head of as′ is a reduction context (since we evaluate right-to-left in applications), so the conditions of the lemma are satisfied.

(u Apply) Similar to (u Function Return) □

We now show that the head of the argument stack corresponds to the part of the source expression which is currently evaluating.

Proposition 7 Whenever (ops, e, a :: [u_{i}^{♢} ^{i∈1..n}], RS) ⇝ b, where • ∉ fv(e), there is a reduction context, R, such that (ops, e, a′:: [u_{i}^{♢} ^{i∈1..n}], RS) ⇝ R[a′] for any a′.

Proof If (ops, e, a:: [u_{i}^{♢} ^{i∈1..n}], RS) ⇝ b there is a b′ such that (ops, e, •::

[u_{i}^{♢}^{i∈1..n}], RS) ⇝ b′ (by Lemma 8). This means (ops, e, •::[u_{i}^{♢}^{i∈1..n}], RS)⟶^{u}^{k}

([], e′, [b′], []) for some k. Since • is a reduction context, applying Lemma 16 k times tells us that b′ = R for some R. Since • ∉ fv(e), Lemma 12 implies (ops, e, a′::[u_{i}^{♢}^{i∈1..n}], RS) ⇝ R[a′] (because a′ = •{{a′/•}} and R[a′] = R{{a′/•}}).

□

We show that β transitions of the abstract machine correspond to reductions in our extended object calculus, and that τ transitions are not reflected in the source level reductions:

Lemma 17

(1) If C ⇝ c and C ⟶^{τ} D then D ⇝ c.

(2) If C ⇝ c and C ⟶^{β} D then there is a d such that D ⇝ d and c → d.

Proof

(1) The proof for each of the τ transitions is similar. We detail only the (τ Access) case.

(τ Access) Here C = (P, Σ), where P = (access j:: ops, E, AS, RS),

E = [U_{i} ^{i∈1..n}], j ∈ 1..n, C ⇝ c = (a, σ) and C ⟶^{τ} D = (Q, Σ)

where Q = (ops, E, U_{j} :: AS, RS). Now, P ↓ p = (access j :: ops, e, as, RS) where E ⇝ e, e = [a_{i} ^{i∈1..n}], U_{i} ⇝ a_{i} and AS ⇝ as. Similarly Q ↓ q = (ops, e, a_{j} :: as, RS). Since C ⇝ (a, σ), and p is unique, p ⇝ a (from the definition of (Unload Config)). By (u Access), p ⟶^{u} q, so by Lemma 14 and p ⇝ a we have q ⇝ a. So D ⇝ (a, σ) as required.

(2) We examine each rule that may derive C ⟶^{β} D.

(β Clone) Here C = (P, Σ), where P = (clone :: ops, E, ι:: AS, RS), and C ⟶^{β} D = (Q, Σ′) where Q = (ops, E, ι′ :: AS, RS), Σ′ = (ι′ ↦ Σ(ι)) :: Σ and ι′ ∉ dom(Σ). We have C ⇝ c = (a, σ) also, where P ↓ p = (clone::ops, e, ι::as, RS), E ⇝ e, AS ⇝ as, p ⇝ a and Σ ⇝ σ. By (u Clone), p ⟶^{u} (ops, e, (clone(ι)) :: as, RS). Hence by Lemma 14, (ops, e, (clone(ι)) :: as, RS) ⇝ a. Therefore by Proposition 7, there is a reduction context R such that for all a′, (ops, e, a′::as, RS) ⇝ R[a′]; by Lemma 15, a = R[clone(ι)] and q = (ops, e, ι′ :: as, RS) ⇝ R[ι′]. Let σ′ = (ι′ ↦ σ(ι)) :: σ so that Σ′ ⇝ σ′ by (Unload Store). Let d = (R[ι′], σ′). Q ↓ q ⇝ R[ι′], so D = (Q, Σ′) ⇝ d. Finally, we have c → d using (Red Clone).

(β Object), (β Update) These cases work similarly.

(β Select) Here C = (P, Σ), and C ⟶^{β} D = (Q, Σ) where P = (select ℓ_{j} :: ops, E, ι:: AS, RS), Q = (ops_{j}, ι:: E_{j}, AS, (ops, E) :: bRS) and Σ(ι) = [(ℓ_{i}, (ops_{i}, E_{i}))^{i∈1..n}]. We have C ⇝ c = (a, σ) also, where C ↓ (p, σ), p = (select ℓ_{j} :: ops, e, ι:: as, RS), E ⇝ e, AS ⇝ as, p ⇝ a and Σ ⇝ σ. Also, D ↓ (q, σ) where q = (ops_{j}, ι:: e_{j}, as, (ops, E) :: RS) and E_{j} ⇝ e_{j}.

By (u Select), p ⟶^{u} p′ where p′ = (ops, e, (ι.ℓ_{j}) :: as, RS). By (Unload Object), Σ ⇝ σ and Σ(ι) = [(ℓ_{i}, (ops_{i}, E_{i}))^{i∈1..n}] we have that E_{j} ⇝ e_{j} and (ops_{j}, e_{j}) ⇝ (y_{j})a_{j} for some a_{j}. By (Unload Abstraction) this means (ops_{j}, y_{j} :: e_{j}, [], []) ⟶^{u}^{∗} ([], e′, [a_{j}], []) for some e′. Hence by Lemma 12 we have (ops_{j}, ι :: e_{j}, [], []) ⟶^{u}^{∗}

([], e′{{ι/y_{i}}}, [a_{i}{{ι/y_{i}}}], RS). By Lemma 9(1) we have q ⟶^{u}^{∗} q′′ =

([], e′{{ι/y_{j}}}, (a_{j}{{ι/y_{j}}})::as, (ops, E)::RS) and by (τ Return) q′′ ⟶^{u}

q′ = (ops, e, (a_{j}{{ι/y_{j}}}) :: as, RS) where E ⇝ e. By Proposition 7 there is a reduction context R such that for all a′, (ops, e, a′ :: as, RS) ⇝ R[a′]. Applying this to p′ and q′ we get p′ ⇝ R[ι.ℓ_{j}] and q′ ⇝ R[a_{j}{{ι/y_{j}}}]. Since p ⟶^{u} p′, Lemmas 15 and 14 give us a = R[ι.ℓ_{j}]. Let d = (R[a_{j}{{ι/y_{j}}}], σ). Then c → d and D ⇝ d.

(β Function Return), (β Apply), (β Let), (β Grab)

These work in a similar way to (β Select). □

To prove that the abstract machine simulates the object calculus semantics, we first need to prove some technical lemmas. We show that the number of τ transitions is bounded for a given state, that if a state unloads to a value then its form is restricted, and that if the abstract machine is stuck then so is its unloaded source term.

Lemma 18 For all configurations C there is a D with C ⟶^{τ}^{∗} D and not

D ⟶^{τ}.

Proof Every ⟶^{τ} step either decreases |RS| or keeps RS constant, and consumes an instruction.

The function f : (ops, E, AS, RS) ↦ (|RS|, |ops|) from states to ℕ × ℕ is such that if C ⟶^{τ} D then f(D) < f(C) in the lexicographic ordering on ℕ × ℕ, namely (x, y) < (x′, y′) if x < x′ or x = x′ and y < y′. An infinite chain C_{1} ⟶^{τ} C_{2} ⟶^{τ} ... would give an infinite descending chain in ℕ × ℕ, a contradiction since the lexicographic ordering is a well-ordering. □

Lemma 19

(1) If D ⇝ (ι, σ) and not D ⟶^{τ} then D = (([], E, [ι], []), Σ) for some E, Σ.

(2) If D ⇝ (λ(x)a, σ) and not D ⟶^{τ} then D = (([], E, [fun(ops, E′)], []), Σ) for some E, Σ and some ops, E′ such that fun(ops, E′) ⇝ λ(x)a.

Proof

(1) We have that not D ⟶^{β} since by Lemma 17 we would have a c with (ι, σ) → c. Suppose D = ((ops, E, AS, RS), Σ). By (Unload Config)

we have Σ ⇝ σ, E ⇝ e, AS ⇝ as and (ops, e, as, RS) ⟶^{u}^{∗} ([], e′, [ι], [])

for some e′. First we note that ops = [] since otherwise (by examining cases) either D would not unload, or could make a β or a τ reduction. Similarly, RS = [] since otherwise (since ops = []) D could make a (τ Return) transition. Now, ([], e, as, []) cannot perform a u transition, but ([], e, as, []) ⟶^{u}^{∗} ([], e′, [ι], []).Hence, e = e′ and as = ι. Since AS ⇝ as = [ι] we have AS = [ι] by (Unload List Location). Hence D = (([], E, [ι], []), Σ).

(2) A similar argument shows that D = (([], E, [fun(ops, E′)], []), Σ) where Σ ⇝ σ and fun(ops, E′) ⇝ λ(x)a. □

Lemma 20 If C ⇝ c and there is no D with C ⟶^{βτ} D then there is no d with c → d.

Proof Let C = (P, Σ), where P = (ops, E, AS, RS). Now, C ⇝ c means P ↓ p, Σ ⇝ σ, p ⟶^{u}^{∗} ([], e′, [a], []) (for some e′), and c = (a, σ).

For a contradiction, suppose that there is no D such that C ⟶^{βτ} D, but there is d such that c → d. Given that p ⟶^{u}^{∗} ([], e′, [a], []), either (1) p = ([], e′, [a], []) or (2) there is p′ such that p ⟶^{u} p′ and p′ ⟶^{u}^{∗} ([], e′, [a], []).

In case (1), a must either be a function or a location, from the definition of AS ⇝ as which forms part of the P ↓ p judgment. Then c = (a, σ) is a value, so there is no d with c → d.

In case (2), we consider two of the rules capable of deriving p ⟶^{u} p′. The cases for the other rules are similar.

(u Access) Here p = (access j::ops, e, as, RS) and p′ = (ops, e, u_{j}::as, RS) where e = [u_{i} ^{i∈1..n}] and j ∈ 1..n. Now, P ↓ p means P = (access j :: ops, [U_{i} ^{i∈1..n}], AS, RS), U_{i} ⇝ u_{i} for i ∈ 1..n and AS ⇝ as. But then C = (P, Σ) ⟶^{τ} ((ops, [U_{i} ^{i∈1..n}], U_{j} :: AS, RS), Σ) by rule (τ Access) contradicting the non-existence of D with C ⟶^{βτ} D.

(u Select) Here p = (select ℓ:: ops, e, u:: as′, RS) and p′ = (ops, e, (u.ℓ) :: as′, RS). Now, p′ →^{∗} ([], e′, [a], []) means p′ ⇝ a. From P ↓ p, we deduce E ⇝ e. We note that none of the unloading rules introduces a free variable without binding it, so fv(e) = ∅; in particular this implies • ∉ fv(e). Hence we may apply Proposition 7 to p′ = (ops, e, (u.ℓ) :: as′, RS) to infer the existence of a reduction context R such that p′ ⇝ R[u.ℓ]. Lemma 14 with p′ ⇝ R[u.ℓ] and p′ ⇝ a implies a = R[u.ℓ] and c = (R[u.ℓ], σ). If c → d then the only rule that can apply is (Red Select); hence u = ι and σ(ι) = o@[ℓ = ς(x)b]@o′. From P ↓ p we derive AS ⇝ ι:: as′ and E ⇝ e. From AS ⇝ ι:: as′ and (Unload List Loc) we see that AS = ι :: AS′ where AS′ ⇝ as′. From Σ ⇝ σ, σ(ι) = o@[ℓ = ς(x)b]@o′, (Unload Store) and (Unload Object) we deduce Σ(ι) = O@[ℓ = (ops′, E′′)]@O′ where E′′ ⇝ e′′ and (ops′, e′′) ⇝ (x)b. Hence C = ((select ℓ:: ops, E, ι:: AS′, RS), Σ). Finally, by rule (β Select), we may derive C ⟶^{β} ((ops′, ι:: E′′, AS′, RS), Σ) and hence a contradiction. □

We are now in a position to show that the abstract machine semantics simulates the semantics of the object calculus:

Lemma 21 If C ⇝ c and c → d then there are D, D′ with C ⟶^{τ}^{∗} D′,

D′ ⟶^{β} D and D ⇝ d.

Proof By Lemma 18 we have a D′ with C ⟶^{τ}^{∗} D′ and not D′ ⟶^{τ}. If there is no D′′ with D′ ⟶^{β} D′′ then by Lemma 20 there is no d with c → d, contradicting the assumption of this lemma. So D′ ⟶^{β} D′′ for some D′′. We consider each of the β-transitions in turn.

(β Select) Here D′ = ((select ℓ :: ops, E, ι :: AS, RS), Σ) where Σ(ι) = O @ [(ℓ, (ops′, E′))] @ O′. Moreover, D′ ↓ (p, σ) where p = (select ℓ::

ops, e, ι:: as, RS), E ⇝ e, AS ⇝ as, Σ ⇝ σ. Then p ⟶^{u} (ops, e, (ι.ℓ) ::

as, RS), and by Proposition 7 there is a reduction context R such that p ⇝ R[ι.ℓ]. Hence, c = (R[ι.ℓ], σ) and if c → d′ then d = d′, since (Red Select) is the unique rule which can derive c → d′ and gives a unique d′.

(β Let), (β Update), (β Function Return), (β Apply), (β Grab) Similar to (β Select).

(β Clone) Here D′ = (P, Σ) = ((clone :: ops, E, ι :: AS, RS), Σ) where Σ(ι) = O. By (u Clone), (Unload Store) and Proposition 7, D′ ⇝ c = (R[clone(ι)], σ) where σ(ι) = o and O ⇝ o. Now d = (R[ι′], σ + (ι′ ↦ o)) where ι′ ∉ dom(σ). By (Unload Store) ι′ ∉ dom(Σ) so by (β Clone) D′ ⟶^{β} D = ((ops, E, ι′ :: AS, RS), Σ + (ι′ ↦ O)). Invoking Proposition 7 again, we get D ⇝ (R[ι′], σ + (ι′ ↦ o)) = d as required.

(β Object) Similar to (β Clone). □

We combine Lemmas 17 and 21 to show that the semantics of the abstract machine and that of our extended object calculus are related via the unloading relation.

Let C ↘ D if C ⟶^{βτ}^{∗} D and D is of the form (([], E, [V], []), Σ) for some E, V and Σ. Such a D we call terminal.

Lemma 22

(1) If C ⇝ c and C ↘ D then there is a d with D ⇝ d and c ↘ d.

(2) If C ⇝ c and c ↘ d then there is a D with D ⇝ d and C ↘ D.

Proof For Part (1) we note that if C →^{∗} D and C ⇝ c then by repeated application of Lemma 17 we have that D ⇝ d and c →^{∗} d. It remains to note that if C ↘ D then D is a terminal configuration, and (since it unloads) it unloads to a value, so c ↘ d.

For (2), we note that c ↘ d means c →^{∗} d and d = (v, σ). By Lemma 21, we have a D′ with C →^{∗} D′ and D′ ⇝ (v, σ). By Lemma 18 there is a D such that D′ ⟶^{τ}^{∗} D and not D ⟶^{τ}. By Lemma 17(1) we know D ⇝ (v, σ) = d, and by Lemma 19 we get that D is of the form ([], E, [V], []), Σ) for some E, V, Σ as required for C ↘ D. □

We are now in a position to prove the main result:

Theorem 3 Suppose that [] ⊢ a ⇒ ops. Then, for all d, (a, []) ↘ d if and only if there is a D with ((ops, [], [], []), []) ↘ D and D ⇝ d.

Proof Given [] ⊢ a ⇒ ops, Proposition 6 implies that ((ops, [], [], []), []) ⇝ (a, []). Suppose (a, []) ↘ d. By Lemma 22(2), there is D such that D ⇝ d and ((ops, [], [], []), []) ↘ D. Conversely, consider a D with ((ops, [], [], []), []) ↘ D and D ⇝ d. By Lemma 22(1), there is d′ such that D ⇝ d′ and (a, []) ↘ d′. A corollary of Lemma 15 is that D ⇝ d and D ⇝ d′ imply that d = d′. Therefore, we have (a, []) ↘ d, as desired. □

3.6 Discussion and Related Work

We have proved correct a machine based on the machine used in our implementation. The machine could be described as a ZAM (Leroy 1990) plus objects, but without some of the ZAM’s tail-recursion optimisations. Because of this, the proof given here can be considered as a correctness proof of a simplified ZAM, and we are sure that the proof could be scaled up to the full ZAM.

There is a large literature on proofs of interpreters based on abstract machines, such as Landin’s SECD machine (Hannan and Miller 1992; Plotkin 1975; Sestoft 1997). Since no compiled machine code is involved, unloading such abstract machines is easier than unloading an abstract machine based on compiled code. The VLISP project (Guttman, Swarup, and Ramsdell 1995), using denotational semantics as a metalanguage, is the most ambitious verification to date of a compiler-based abstract machine. Other work on compilers deploys metalanguages such as calculi of explicit substitutions (Hardin, Maranget, and Pagano 1998) or process calculi (Wand 1995). Rather than introduce a metalanguage, we prove correctness of our abstract machine directly from its operational semantics. We adopted Rittri’s idea (Rittri 1990) of unloading a machine state to a term via a specialised unloading machine. Rittri uses a generic framework based on bisimulation to prove correctness of both a machine for evaluating arithmetic expressions, and the SECD machine. Our work goes beyond Rittri’s by dealing with state and objects. We found it simpler to write a direct proof than to appeal to his generic framework.

There are differences, of course, between our formal model of the abstract machine and our actual implementation. One difference is that we have modelled programs as finitely branching trees, whereas in the implementation programs are bytecode arrays indexed by a program counter. Another difference is that our model omits garbage collection, which is essential to the implementation. Therefore Theorem 3 only implies that the compilation strategy is correct; bugs may remain in its implementation.

4 Operational Equivalence

We now develop a theory of operational equivalence for the imperative object calculus. We consider only the core object calculus, not the calculus extended with functions. The standard definition of operational equivalence between terms is that of contextual equivalence (Morris 1968; Plotkin 1977): two terms are equivalent if and only if they are interchangeable in any program context without any observable difference; the observations are typically the programs’ termination behaviour. Contextual equivalence is the largest congruence relation that distinguishes observably different programs. Terms are equivalent if and only if no amount of programming can tell them apart. This is a robust and reasonable definition of semantic equivalence.

Mason and Talcott (1991) have shown a useful context lemma for functional languages with state. It asserts that contextual equivalence coincides with so-called CIU (“Closed Instances of Use”) equivalence. Informally, to prove two terms are CIU equivalent, one needs to show that they have identical termination behaviour when placed in the redex position in an arbitrary configuration and locations are substituted for the free variables. Although contextual equivalence and CIU equivalence are the same relation, the definition of the latter is typically easier to use in proofs.

We take CIU equivalence as our definition of operational equivalence for imperative objects and we establish some useful equivalence laws. Furthermore, we show that operational equivalence is a congruence, allowing compositional equational reasoning and a proof that it coincides with contextual equivalence. The congruence proof is adapted from the corresponding congruence proof for a λ-calculus with references by Honsell, Mason, Smith, and Talcott (1993).

We take a modular approach to formulating CIU equivalence. In Section 4.1, we introduce experimental equivalence, an auxiliary relation on configurations. In Section 4.2, we phrase our definition of operational equivalence in terms of experimental equivalence, but prove our formulation is equivalent to the one of Mason and Talcott (1991). We derive a variety of equational laws for imperative objects in Section 4.3. Section 4.4 contains our congruence proof for operational equivalence, which we use in Section 4.5 to show that operational and contextual equivalence are the same.

4.1 Experimental Equivalence

For configurations c and c′, we write c ↕ c′ to mean that either both converge or neither of them converges, that is, c↓ if and only if c′↓.

We define a family of relations on configurations, called experimental equivalence. Recall that w ranges over finite sets of locations. Two configurations (a, σ) and (a′, σ′) are experimentally equivalent at index set w, written (a, σ) ∼_{w} (a′, σ′), if and only if ⊢_{w} (a, σ) ok, ⊢_{w} (a′, σ′) ok and, for all reduction contexts with locs(R) ⊆ w and fv(R) = {•}, (R[a], σ) ↕ (R[a′], σ′).

We may regard experimental equivalence at w as a kind of testing equivalence. Let a w-test be a reduction context R such that locs(R) ⊆ w and fv(R) = {•}. Let a configuration (a, σ) pass a w-test, R, if and only if (R[a], σ)↓. Then two configurations c and c′ are experimentally equivalent at w if and only if ⊢_{w} c ok, ⊢_{w} c′ ok and they pass the same w-tests.

The index set w is a view into the configurations: the locations in the stores that R may directly inspect. Other locations in the stores may only be inspected indirectly.

For every index set w, experimental equivalence is an equivalence relation (reflexive, transitive and symmetric) on configurations, and it is antimonotone in the index set w:

(∼ Refl) ; \frac{⊢_{w} c ok}{c ∼_{w} c} (∼ Trans) ; \frac{c ∼_{w} c′′ c′′ ∼_{w} c′}{c ∼_{w} c′} (∼ Symm) ; \frac{c ∼_{w} c′}{c′ ∼_{w} c} (∼ Anti) ; \frac{c ∼_{w′} c′ w ⊆ w′}{c ∼_{w} c′}

The following, easily proved facts about the interaction between reduction contexts and reduction facilitate operational arguments involving reduction contexts.

Lemma 23 For every closed reduction context R with locs(R) ⊆ dom(σ),

(1) (a, σ) → (a′, σ′) if and only if (R[a], σ) → (R[a′], σ′), if a is not a value, and

(2) (R[a], σ) →^{∗} (v, σ′) if and only if there is a configuration (v′, σ′′) such that (a, σ) →^{∗} (v′, σ′′) and (R[v′], σ′′) →^{∗} (v, σ′).

Part (2) implies that if (a, σ) goes wrong or diverges, so does (R[a], σ).

We can prove that reduction is sound with respect to experimental equivalence:

Lemma 24 If ⊢_{w} c ok and c → c′, then c ∼_{w} c′.

Proof Suppose ⊢_{w} (a, σ) ok and (a, σ) → (a′, σ′). Then ⊢_{w} (a′, σ′) ok holds by Lemma 1. Further, suppose locs(R) ⊆ w and fv(R) = {•}. From Lemma 23(1) we get that (R[a], σ) → (R[a′], σ′). Clearly, (R[a′], σ′)↓ implies (R[a], σ)↓ because any converging reduction sequence from (R[a′], σ′) extends to a converging reduction sequence from (R[a], σ). The reverse implication follows because reduction is deterministic up to structural equivalence at w, that is, by a combination of Proposition 1 and Lemma 3. We conclude (a, σ) ∼_{w} (a′, σ′), as required. □

Moreover, up to experimental equivalence, all that matters about a configuration is whether it converges, and if so, to which terminal configuration it converges:

Lemma 25 Suppose ⊢_{w} c ok and ⊢_{w} c′ ok. Then c ∼_{w} c′ if and only if either

(1) both c and c′ converge, that is, there are terminal d and d′ such that c →^{∗} d and c′ →^{∗} d′, and moreover d ∼_{w} d′, or

(2) neither c nor c′ converges.

Proof For the forwards direction, suppose c = (a, σ) and c′ = (a′, σ′). We proceed by considering whether or not c converges, that is, whether or not there is a terminal d with c →^{∗} d. If so, let R = • so that (R[a], σ) = c. Since (R[a], σ)↓, c ∼_{w} c′ implies c′ = (R[a′], σ′)↓, that is, there is terminal d′ with c′ →^{∗} d′. Lemma 24 implies that c ∼_{w} d and c′ ∼_{w} d′. These two equivalences together with c ∼_{w} c′ imply d ∼_{w} d′ by (∼ Symm) and (∼ Trans). On the other hand, if c does not converge, neither does c′, since c ∼_{w} c′ implies that if c′ converges so does c. In all, we have shown that condition (1) holds if c converges, and that condition (2) holds if c does not.

For the backwards implication, we must show that conditions (1) and (2) both imply that c ∼_{w} c′. Given condition (1), Lemma 24 asserts that c ∼_{w} d and c′ ∼_{w} d′. These two equivalences, with d ∼_{w} d′, (∼ Symm) and (∼ Trans) imply c ∼_{w} c′. Finally, condition (2) implies c ∼_{w} c′ by definition of experimental equivalence and Lemma 23(2). □

It is possible to formulate garbage collection principles for unused objects in terms of experimental equivalences. We call a location ι garbage in (a, σ@[ι ↦ o]@σ′) if the configuration is well formed, ⊢ (a, σ@[ι ↦ o]@σ′) ok, and it is also well formed without (ι ↦ o) in the store, ⊢ (a, σ@σ′) ok; that is, a and σ@σ′ make no reference to ι. Reduction is independent of garbage:

Lemma 26 Suppose ι is garbage in (a, σ@[ι ↦ o]@σ′). Then (a, σ@[ι ↦ o]@σ′) →^{n} (v, σ_{n}@[ι ↦ o_{n}]@σ′_{n}) if and only if o = o_{n}, ι ∉ dom(σ_{n}@σ′_{n}), and (a, σ@σ′) →^{n} (v, σ_{n}@σ′_{n}).

Proof By inspection of the reduction rules we see that (a, σ@[ι ↦ o]@σ′) → (a_{1}, σ_{1}@[ι ↦ o_{1}]@σ′_{1}) if and only if o = o_{1}, ι ∉ dom(σ_{1}@σ′_{1}), and (a, σ@σ′) → (a_{1}, σ_{1}@σ′_{1}). Furthermore, for any such transition, ι is again garbage in (a_{1}, σ_{1}@[ι ↦ o_{1}]@σ′_{1}). The result follows by induction on the length of the computations. □

We use the lemma to obtain the following garbage collection law which says that if ι is garbage in a configuration c, it can be garbage collected up to experimental equivalence at any w such that ⊢_{w} c ok and ι ∉ w.

Lemma 27 Suppose ι is garbage in (a, σ@[ι ↦ o]@σ′). If ⊢_{w} (a, σ@σ′) ok then (a, σ@[ι ↦ o]@σ′) ∼_{w} (a, σ@σ′).

Proof For every R with locs(R) ⊆ w and fv(R) = {•}, ι is garbage in (R[a], σ@[ι ↦ o]@σ′). Therefore (R[a], σ@[ι ↦ o]@σ′) ↕ (R[a], σ@σ′) follows from the preceding lemma. □

Experimental equivalence is only an auxiliary relation. Our main interest is operational equivalence for static terms which we introduce below. However, the experimental equivalence relation on configurations is useful because some facts about reduction, such as Lemmas 24, 25 and 27, are best expressed as equivalences between configurations.

4.2 Operational Equivalence

From experimental equivalence on configurations we derive an equivalence relation on static terms, operational equivalence. First, let a substitution, ρ, be a finite map from variables to locations; we write ρ : {x_{1}, …, x_{n}} → w whenever ρ = [x_{i} ↦ ι_{i} ^{i∈1..n}] and ι_{i} ∈ w for all i ∈ 1..n. Let aρ be the term obtained from a static term a by substituting ρ(x) for x for every x ∈ dom(ρ). (These substitutions denoted by ρ are a special case of the substitutions denoted by s in Section 2.4.) Now, we define two static terms a and a′ to be operationally equivalent, written a ≈ a′, if and only if (aρ, σ) ∼_{dom(σ)} (a′ρ, σ) holds for all well formed stores σ and substitutions ρ : fv(a) ∪ fv(a′) → dom(σ).

Operational equivalence is an equivalence relation on static terms:

(≈ Refl) ; \frac{locs(a) = ∅}{a ≈ a} (≈ Trans) ; \frac{a ≈ a′′ a′′ ≈ a′}{a ≈ a′} (≈ Symm) ; \frac{a ≈ a′}{a′ ≈ a}

We define operational equivalence only for static terms because we want to study program equivalences that programmers can use for manipulations of program text. Also, most automatic program transformations, as may take place in compilers, deal with static program text or code. Locations are dynamic entities, created during reduction of configurations. A location only carries meaning in the context of a particular store. Therefore we only consider locations in connection with configurations and experimental equivalence. Our modular formulation of operational equivalence on static terms via experimental equivalence on configurations is often convenient for proofs: after instantiation of static terms a and a′ into configurations (aρ, σ) and (a′ρ, σ), one can apply the simpler theory of experimental equivalence.

The following lemma asserts that operational equivalence is Mason and Talcott’s CIU equivalence: static terms a and a′ are equivalent if and only if all ‘closed instantiations’ (variable substitutions ρ and stores σ) of all ‘uses’ (reduction contexts R) either both converge or neither converges.

Lemma 28 For all static terms a and a′, a ≈ a′ if and only if (R[a]ρ, σ) ↕ (R[a′]ρ, σ), for all static reduction contexts R, well formed stores σ, and substitutions ρ : fv(R[a]) ∪ fv(R[a′]) → dom(σ).

Proof Follows straightforwardly from the definition of ≈ and ∼. For the forward implication, we use the fact that R[a]ρ = (Rρ)[aρ] and Rρ is again a reduction context. For the reverse implication, note that any reduction context R′ can be written in the form Rρ, for some static reduction context R and substitution ρ. □

An easy consequence of Lemma 28 is that operational equivalence is preserved by static reduction contexts:

Lemma 29 If a ≈ a′ then R[a] ≈ R[a′], for all static reduction contexts R.

So equivalent terms in identical static reduction contexts are again equivalent. Conversely, identical static terms in equivalent reduction contexts are also equivalent:

Lemma 30 If R[x] ≈ R′[x] and x ∉ fv(R) ∪ fv(R′), then R[a] ≈ R′[a], for all static terms a.

Proof We must show

(R[a]ρ, σ) ∼_{dom(σ)} (R′[a]ρ, σ)  (15)

whenever ⊢ σ ok and ρ : fv(R[a]) ∪ fv(R′[a]) → dom(σ). Note that R[a]ρ = (Rρ)[aρ] and R′[a]ρ = (R′ρ)[aρ].

If (aρ, σ)↓ does not hold, then both (R[a]ρ, σ)↓ and (R′[a]ρ, σ)↓ are false, by Lemma 23(2), hence (15) holds by Lemma 25.

Otherwise assume (aρ, σ) →^{∗} (ι, σ′), for some ι and σ′. Then (R[a]ρ, σ) →^{∗} ((Rρ)[ι], σ′) and (R′[a]ρ, σ) →^{∗} ((R′ρ)[ι], σ′). Now (15) follows by repeated applications of Lemma 24 if

((Rρ)[ι], σ′) ∼_{dom(σ)} ((R′ρ)[ι], σ′)  (16)

But note that (Rρ)[ι] = R[x]ρ′ and (R′ρ)[ι] = R′[x]ρ′ if ρ′ = (x ↦ ι) :: ρ. Therefore, by the assumption R[x] ≈ R′[x] and by definition of ≈, we have

(R[x]ρ′, σ′) ∼_{dom(σ′)} (R′[x]ρ′, σ′)

hence also (16) holds, by Lemma 1 and (∼ Anti). □

4.3 Laws of Operational Equivalence

From Lemma 30 and the definition of operational equivalence, combined with the laws for experimental equivalence above, it is possible to show a multitude of laws of operational equivalence for the constructs of the calculus. We now show a selection of such laws and we give an equational proof of β_{v}-reduction for the encoding of call-by-value functions from Section 2.

The let construct satisfies laws corresponding to those of Moggi’s computational λ-calculus (Moggi 1989), presented here in the form given by Talcott (1998):

Proposition 8

(1) (let x = y in b) ≈ b{{y/x}}

(2) (let x = a in R[x]) ≈ R[a], if x ∉ fv(R)

Proof Part (1) is immediate from definition of ≈ and Lemma 24. For (2), by Lemma 30 it suffices to show (let x = x in R[x]) ≈ R[x] which is immediate from (1). □

Moggi’s eta law is just Proposition 8(2) with R = •. To prove associativity:

let x = a in (let x = a′ in b) ≈ let x = (let x = a in a′) in b (17)

we first use Proposition 8(1), Lemma 29 and Lemma 30 to rewrite the left hand side to

let x = a in (let x = (let x = x in a′) in b)

which, by Proposition 8(2) with R = (let x = (let x = • in a′) in b), rewrites to the right hand side of (17).

The effect of invoking a method that has just been updated is the same as running the method body of the update with the self parameter bound to the updated object:

Proposition 9

(let x = a.ℓ ⇐ ς(x)b in R[x.ℓ]) ≈ (let x = a.ℓ ⇐ ς(x)b in R[b])

Proof By Lemma 30 it suffices to show the law for some y ∉ fv(b) in place of a. This case holds by definition of ≈ and, if y is instantiated to a location pointing to an object with an ℓ method, by five applications of Lemma 24; if the object has no ℓ method, neither side of the equation converges. □

There are laws for object constants and their interaction with the other constructs of the calculus:

Proposition 10 Suppose o = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] and j ∈ 1..n.

(1) (let x_{j} = o in R[x_{j}.ℓ_{j}]) ≈ (let x_{j} = o in R[b_{j}])

(2) o.ℓ_{j} ≈ (let x_{j} = o in b_{j})

(3) (o.ℓ_{j} ⇐ ς(x)b) ≈ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..j−1}, ℓ_{j} = ς(x)b, ℓ_{i} = ς(x_{i})b_{i} ^{i∈j+1..n}]

(4) clone(o) ≈ o

(5) (let x = o in R[clone(x)]) ≈ (let x = o in R[o]), if x ∉ fv(o)

(6) (let x = o in b) ≈ b, if x ∉ fv(b)

(7) (let x = a in let y = o in b) ≈ (let y = o in let x = a in b), if x ∉ fv(o) and y ∉ fv(a)

Proof Parts (3) and (5) are immediate from definition of ≈ and a few applications of Lemma 24.

Part (1) is established by Proposition 9 together with (3) and Lemma 29:

let x_{j} = o in R[x_{j}.ℓ_{j}] ≈ let x_{j} = o.ℓ_{j} ⇐ ς(x_{j})b_{j} in R[x_{j}.ℓ_{j}]
≈ let x_{j} = o.ℓ_{j} ⇐ ς(x_{j})b_{j} in R[b_{j}]
≈ let x_{j} = o in R[b_{j}]

Part (2) is immediate from (1) and Proposition 8(2).

Part (4) follows from Proposition 8(2), (5) and (6):

clone(o) ≈ let x = o in clone(x) where x ∉ fv(o)
≈ let x = o in o
≈ o

Part (6) is direct from the definition of ≈, Lemma 24 and Lemma 27. Part (7) requires a more elaborate argument, first expanding the definition

of ≈ and then analysing the possible reduction sequences of arbitrary closed instances, exploiting that reduction is independent of garbage, Lemma 26. Suppose ⊢ σ ok and ρ : fv(let x = a in let y = o in b) → dom(σ). We must show

((let x = a in let y = o in b)ρ, σ) ∼_{dom(σ)} ((let y = o in let x = a in b)ρ, σ)

First observe that

((let y = o in let x = a in b)ρ, σ) → ((let x = a in b)ρ′, (ι ↦ oρ) :: σ)

where ρ′ = (y ↦ ι) :: ρ, for some ι ∉ dom(σ). Note that aρ′ = aρ and ι is garbage in (aρ, (ι ↦ oρ) :: σ). Therefore, by Lemma 26, either both (aρ′, (ι ↦ oρ) :: σ) and (aρ, σ) go wrong or diverge, or (aρ′, (ι ↦ oρ) :: σ) →^{n} (ι′, σ_{n}@[ι ↦ oρ]@σ′_{n}) and (aρ, σ) →^{n} (ι′, σ_{n}@σ′_{n}), for some n, ι′, σ_{n} and σ′_{n}. If they go wrong or diverge, (18) holds by Lemma 23(2) and Lemma 25. Otherwise, again by Lemma 23,

((let x = a in b)ρ′, (ι ↦ oρ) :: σ) →^{n} ((let x = ι′ in b)ρ′, σ_{n}@[ι ↦ oρ]@σ′_{n})

((let x = a in let y = o in b)ρ, σ) →^{n} ((let x = ι′ in let y = o in b)ρ, σ_{n}@σ′_{n})

Each reduces further to (bρ′′, σ_{n}@[ι ↦ oρ]@σ′_{n}), where ρ′′ = (x ↦ ι′) :: ρ′. By repeated applications of Lemma 24, we conclude (18). □

The next proposition gives laws for method update and its interaction with method selection and cloning.

Proposition 11 Let notation a;b abbreviate let x = a in b where x ∉ fv(b).

(1) (let x = a.ℓ ⇐ ς(x)b in R[x]) ≈ (let x = a in R[x.ℓ ⇐ ς(x)b])

(2) (a.ℓ ⇐ ς(x)b).ℓ ⇐ ς(x′)b′ ≈ a.ℓ ⇐ ς(x′)b′

(3) (y.ℓ ⇐ ς(x)b); (z.ℓ′ ⇐ ς(x′)b′); a ≈ (z.ℓ′ ⇐ ς(x′)b′); (y.ℓ ⇐ ς(x)b); a, if ℓ ≠ ℓ′

(4) clone(y.ℓ ⇐ ς(x)b) ≈ (let z = clone(y) in (y.ℓ ⇐ ς(x)b); z.ℓ ⇐ ς(x)b)

Proof Similar to the proof of Proposition 9. □

Let us look at two examples of equational reasoning using the laws above.

Example 1: Pairs

Recall that pair(a, b) is the object:

[fst = ς(s)a, snd = ς(s)b, swap = ς(s)\begin{matrix}let x = s.fst in let y = s.snd in \\ (s.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x] \end{matrix}

for some s ∉ fv(a) ∪ fv(b). First, let us prove that the fst and snd methods work as projections:

pair(a, b).fst ≈ let s = pair(a, b) in a by Prop. 10(2)
≈ a  by Prop. 10(6)

Analogously, we derive that pair(a, b).snd ≈ b.

To show that the swap method indeed swaps the components of a pair, we can argue as follows:

pair(x, y).swap

≈ let s = pair(x, y) in

let x′ = s.fst in let y′ = s.snd in

(s.fst ⇐ ς(s′)y′).snd ⇐ ς(s′)x′  by Prop. 10(2)
≈ let s = pair(x, y) in

let x′ = x in let y′ = s.snd in

(s.fst ⇐ ς(s′)y′).snd ⇐ ς(s′)x′  by Prop. 10(1)
≈ let s = pair(x, y) in

let y′ = s.snd in

(s.fst ⇐ ς(s′)y′).snd ⇐ ς(s′)x  by Prop. 10(7) and 8(1)
≈ let s = pair(x, y) in

let y′ = y in

(s.fst ⇐ ς(s′)y′).snd ⇐ ς(s′)x  by Prop. 10(1)
≈ let s = pair(x, y) in
(s.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x  by Prop. 10(7) and 8(1)
≈ (pair(x, y).fst ⇐ ς(s′)y).snd ⇐ ς(s′)x by Prop. 8(2)
≈ pair(y, y).snd ⇐ ς(s′)x  by Prop. 10(3)
≈ pair(y, x)  by Prop. 10(3)

We note that pair(a, b).swap ≈ pair(b, a) fails in general, for instance if a or b diverges, because a and b are evaluated in the course of the swap on the left hand side and they are not evaluated on the right hand side. However, by an elaboration of the previous derivation, we can show:

pair(a, b).swap ≈ let x = a in let y = b in pair(y, x)

for arbitrary static terms a and b with x ∉ fv(b).

Example 2: Functions

For the second example, recall the encoding of call-by-value functions from Section 2.1:

λ(x)b =^{def} [arg = ς(z)z.arg, val = ς(s)let x = s.arg in b]
b(a) =^{def} let y = a in (b.arg ⇐ ς(z)y).val

where s, y ∉ fv(b) and y ≠ z ∉ fv(a). From the laws for let and for object constants, we can show that β_{v}-reduction is valid:

(λ(x)b)(y) ≈ b{{y/x}}  (19)

Let o = [arg = ς(z)y, val = ς(s)let x = s.arg in b], then

(λ(x)b)(y)

≈ ((λ(x)b).arg ⇐ ς(z)y).val  by Prop. 8(1)
≈ o.val  by Prop. 10(3) and Lemma 29
≈ let s = o in let x = s.arg in b by Prop. 10(2)
≈ let x = o.arg in b  by Prop. 8(2)
≈ let x = (let z = o in y) in b by Prop. 10(2) and Lemma 29
≈ let x = y in b  by Prop. 10(6) and Lemma 29
≈ b{{y/x}}  by Prop. 8(1)

These examples as well as the derivations of some of the laws above suggest the usefulness of equational reasoning for understanding and manipulating imperative object programs.

4.4 Congruence

The derivation of (19) used the fact that operational equivalence is preserved by reduction contexts, Lemma 29. More generally, in order to exercise compositional equational reasoning it is necessary that operational equivalence is preserved by arbitrary term constructs. This property can be formalised in terms of compatible refinement (Gordon 1994). Given a relation on terms S, its compatible refinement, Ŝ, relates terms with identical outermost syntactic constructors and with immediate subterms pairwise related by S, as defined by the following axiom schemes.

(Comp x) x Ŝ x.

(Comp Object) [ℓ_{i} = ς(x_{i})b_{i}^{i∈1..n}]Ŝ[ℓ_{i} = ς(x_{i})b′_{i}^{i∈1..n}] if b_{i} S b′_{i} for i ∈ 1..n.

(Comp Select) a.ℓ Ŝ a′.ℓ if a S a′.

(Comp Update) a.ℓ ⇐ ς(x)b Ŝ a′.ℓ ⇐ ς(x)b′ if a S a′ and b S b′.

(Comp Clone) clone(a) Ŝ clone(a′) if a S a′.

(Comp Let) let x = a in b Ŝ let x = a′ in b′ if a S a′ and b S b′.

Let a relation be compatible if and only if it contains its compatible refinement. Let a congruence be a compatible equivalence relation.

Proposition 12 Operational equivalence is a congruence.

Proof Operational equivalence is an equivalence relation, so it remains to show that it is compatible, that is, a ˆ≈a′ implies a ≈ a′. The proof is adapted from the corresponding congruence proof for a λ-calculus with references in (Honsell, Mason, Smith, and Talcott 1993). We prove a ≈ a′ by case analysis of the derivation of a ˆ≈ a′.

(Comp x) Here a = a′ = x, for some variable x, and a ≈ a′ holds because ≈ is reflexive, (≈ Refl).

(Comp Clone) Here a = clone(a_{0}), a′ = clone(a′_{0}), and a_{0} ≈ a′_{0}. But then a ≈ a′ is immediate from Lemma 29 with R = clone(•).

(Comp Select) Immediate from Lemma 29 as in the previous case.

(Comp Update) Here a = a_{0}.ℓ ⇐ ς(x)b, a′ = a′_{0}.ℓ ⇐ ς(x)b′, a_{0} ≈ a′_{0} and b ≈ b′. By Lemma 29, a_{0} ≈ a′_{0} implies a_{0}.ℓ ⇐ ς(x)b ≈ a′_{0}.ℓ ⇐ ς(x)b. Because ≈ is transitive the result follows if a′_{0}.ℓ ⇐ ς(x)b ≈ a′_{0}.ℓ ⇐ ς(x)b′. By Lemma 30, this again follows if

y.ℓ ⇐ ς(x)b ≈ y.ℓ ⇐ ς(x)b′

for some y ∉ fv(b). Consider any σ and ρ such that ⊢ σ ok and ρ : ({y} ∪ fv(b) ∪ fv(b′) − {x}) → dom(σ). We must show that

(ι.ℓ ⇐ ς(x)bρ, σ) ∼_{dom(σ)} (ι.ℓ ⇐ ς(x)b′ρ, σ)

where ι = ρ(y). If the object σ(ι) has no ℓ method, both configurations are stuck and the equivalence holds by Lemma 25. Otherwise it follows by Lemma 24 if

(ι, σ_{1}) ∼_{dom(σ)} (ι, σ′_{1})

where σ_{1} and σ′_{1} are the updated stores obtained from σ by replacing the method at label ℓ in σ(ι) by methods ℓ = ς(x)bρ and ℓ = ς(x)b′ρ, respectively. To prove this, we must show that

(R[ι], σ_{1}) ↕ (R[ι], σ′_{1})

for all R with locs(R) ⊆ dom(σ) and fv(R) = {•}. Let relation T relate stores with identical domains and with objects pairwise identical or having ℓ methods ℓ = ς(x)bρ and ℓ = ς(x)b′ρ, respectively, and all other methods identical. In particular, σ_{1} T σ′_{1}. We shall argue that

(a, σ) ↕ (a, σ′) for all a, σ and σ′ such that σ T σ′

Suppose (a, σ)↓, that is, there exist n and a terminal configuration d such that (a, σ) →^{n} d. We show (a, σ′)↓ by induction on n:

If n = 0, (a, σ) is a terminal configuration, that is, a is a value, and then (a, σ′) is terminal too.

Otherwise there exists (a_{1}, σ_{1}) such that (a, σ) → (a_{1}, σ_{1}) →^{n−1} d. By inspection of the reduction rules we see that (a, σ′) → (a_{1}, σ′_{1}) with σ_{1} T σ′_{1}, unless a is of the form a = R[ι.ℓ] where σ(ι) and σ′(ι) have methods ℓ = ς(x)bρ and ℓ = ς(x)b′ρ, respectively. In that case (a_{1}, σ_{1}) = (R[bρ′], σ) and (a, σ′) → (R[b′ρ′], σ′) where ρ′ = (x ↦ ι) :: ρ. Since (R[bρ′], σ) →^{n−1} d in one less step than (a, σ) →^{n} d, we get (R[bρ′], σ′)↓ by the induction hypothesis. Moreover, b ≈ b′ implies (bρ′, σ′) ∼_{dom(σ′)} (b′ρ′, σ′). Hence (R[bρ′], σ′) ↕ (R[b′ρ′], σ′) and we obtain (R[b′ρ′], σ′)↓ and (a, σ′)↓, as required.

This completes the induction on n and we conclude that (a, σ)↓ implies (a, σ′)↓. The reverse implication is symmetrical. So (a, σ) ↕ (a, σ′), as required.

(Comp Object) Follows from case (Comp Update) by repeated applications of Proposition 10(3).

(Comp Let) Here a = (let x = a_{0} in b), a′ = (let x = a′_{0} in b′), a_{0} ≈ a′_{0} and b ≈ b′. Firstly, a_{0} ≈ a′_{0} implies (let x = a_{0} in b) ≈ (let x = a′_{0} in b), by Lemma 29. Next, b ≈ b′ implies (let x = x in b) ≈ (let x = x in b′) and (let x = a′_{0} in b) ≈ (let x = a′_{0} in b′), by Proposition 8(1) and Lemma 30. Finally, a ≈ a′ because ≈ is transitive, (≈ Trans). □

4.5 Contextual Equivalence

We call a relation S on static terms adequate if and only if a S a′ implies (a, []) ↕ (a′, []), for all closed terms a and a′.

Proposition 13 Operational equivalence is adequate.

Proof Immediate from the definition of operational and experimental equivalence, by taking the empty substitution, empty store, and empty reduction context. □

Proposition 14 Operational equivalence is the largest compatible and adequate relation on static terms.

Proof We must show that any compatible and adequate relation S is included in ≈.

Suppose a S a′. By appeal to Lemma 28, a ≈ a′ holds if

(R[a]ρ, σ) ↕ (R[a′]ρ, σ)  (20)

for any given static reduction context R and any σ and ρ such that ⊢ σ ok and ρ : fv(R[a]) ∪ fv(R[a′]) → dom(σ).

Suppose σ = [ι_{i} ↦ o_{i} ^{i∈1..n}], o_{i} = [ℓ_{ij} = ς(x_{ij})a_{ij} ^{j∈1..q_{i}}], and ρ = [x_{h} ↦ ι_{i_{h}} ^{h∈1..m}] with {i_{1} … i_{m}} ⊆ {1 … n}. Then let ω_{i} = [ℓ_{ij} = ς(x)x.ℓ_{ij} ^{j∈1..q_{i}}], pick n distinct variables z_{1} … z_{n}, and let b_{ij} be obtained from a_{ij} by replacing every occurrence of location ι_{k} by variable z_{k} for k ∈ 1..n, for all j ∈ 1..q_{i} and i ∈ 1..n. Let

b =

let z_{1} = ω_{1} in … let z_{n} = ω_{n} in
(...(z_{1}.ℓ_{11} ⇐ ς(x_{11})b_{11})...).ℓ_{1q_{1}} ⇐ ς(x_{1q_{1}})b_{1q_{1}};
⋮
(...(z_{n}.ℓ_{n1} ⇐ ς(x_{n1})b_{n1})...).ℓ_{nq_{n}} ⇐ ς(x_{nq_{n}})b_{nq_{n}};
let x_{1} = z_{i_{1}} in … let x_{m} = z_{i_{m}} in R[a]

and let b′ be the same as b but with a′ in place of a (notation a; b abbreviates let x = a in b where x ∉ fv(b)). Then b S b′ holds, since a S a′ and S is compatible, and therefore (b, []) ↕ (b′, []), since S is adequate. One can check that (b, []) →^{∗} (R[a]ρ, σ) and (b′, []) →^{∗} (R[a′]ρ, σ). By determinacy of reduction, it follows, as in the proof of Lemma 24, that (aρ, σ) ↕ (b, []) and (b′, []) ↕ (a′ρ, σ). Finally, we conclude (20), as required, because the relation ↕ is transitive. □

Clearly, operational equivalence is also the largest adequate congruence on static terms. It follows that it coincides with Morris-style contextual equivalence, sometimes known as observational congruence (Meyer and Cosmadakis 1988), where we take convergence of programs as our means of observation. Instead of the usual definition of contextual equivalence in terms of variable capturing contexts, one can equivalently define it as the relation between static terms which are related by a compatible and adequate relation; more concretely, for any two terms a and a′, let {(a, a′)}^{c} be the least compatible relation that relates them, defined inductively by the rules:

(Ctx a a′) ; \overline{a \{(a, a′)\}^{c} a′} (Ctx Comp) ; \frac{b { \atop \{(a, a′)\}^{c}} b′}{b \{(a, a′)\}^{c} b′}

Then a and a′ are contextually equivalent if and only if {(a, a′)}^{c} is adequate. The coincidence between operational and contextual equivalence reads as follows:

Theorem 4 Operational (CIU) equivalence coincides with contextual equivalence.

Proof We must prove that a ≈ a′ if and only if {(a, a′)}^{c} is adequate. The ‘if’ direction is immediate from the previous proposition because a {(a, a′)}^{c} a′ and {(a, a′)}^{c} is compatible and adequate. Conversely, {(a, a′)}^{c} is contained in ≈, by induction on the definition of {(a, a′)}^{c}, since ≈ is closed under (Ctx a a′) and (Ctx Comp) by the assumption a ≈ a′ and by (≈ Comp). Therefore {(a, a′)}^{c} is adequate since ≈ is adequate. □

The definitions of experimental equivalence and operational equivalence are formulated in terms of reduction contexts, stores and substitutions. That makes it easy to relate experimental and operational equivalence to the substitution-based operational semantics in equivalence proofs. In contrast, the definition of contextual equivalence is robust and abstract because it is not dependent on details of the operational semantics: it only refers to static terms and adequacy (convergence). Theorems 1, 2, and 3 imply that adequacy can equivalently be defined on the basis of any of the three operational semantics of Section 2 or the abstract machine of Section 3. Furthermore, the definition of adequacy is unaffected by the choice of store model for the operational semantics (see the discussion below).

4.6 Discussion and Related Work

The store model

The object store model is well-suited for operational reasoning because it makes clear that method updates are not shared between different labels and different objects. For example, it was easy to prove Proposition 11(3):

(y.ℓ ⇐ ς(x)b); (z.ℓ′ ⇐ ς(x′)b′); a ≈ (z.ℓ′ ⇐ ς(x′)b′); (y.ℓ ⇐ ς(x)b); a

In the method store model of Abadi and Cardelli (Abadi and Cardelli 1996), object values are of the form [ℓ_{i} ↦ ι_{i} ^{i∈1..n}], and stores map locations to methods. A static term would be instantiated to a configuration by applying a substitution of free variables to object values and by pairing the resulting term with an associated method store. The definition of CIU equivalence would have to constrain the object values and method store used in instantiations: the resulting configuration would need to be such that different occurrences of object values do not share methods unless the occurrences are identical. For example, without this constraint, there is a closing instantiation of the above equation such that one side converges while the other diverges. Take b = x, b′ = x′.ℓ′, and a = z.ℓ′, and substitute the object [ℓ ↦ ι] for y, and the object [ℓ′ ↦ ι] for z, two objects that share the method ι but that are not identical. Now, if we run each side in the method store [ι ↦ ς(x)[]], we find that the left hand side diverges, whereas the right hand side converges to ([ℓ′ ↦ ι], [ι ↦ ς(x)x]).

On the other hand, one advantage of the method store model is that it makes it easy to verify that different copies of the empty object are equivalent, for instance,

let x = [] in [ℓ = ς(s)x] ≈ [ℓ = ς(s)[]]  (21)

is an instance of Proposition 8(1) because [] is a value. In our object store model, the proof of (21) becomes somewhat involved and requires a tedious argument analogous to that of Lemma 27.

Functions

To keep the exposition simple and focused on imperative objects, the theory of operational equivalence is only presented for the core calculus. The definition of operational equivalence and the results for the core calculus can be extended to the full calculus with functions considered in the previous sections, along the lines of the similar work on a λ-calculus with references by Honsell, Mason, Smith, and Talcott (Honsell et al. 1993). All the laws in Section 4.3 remain valid for the full calculus. Nonetheless, the extension of the theory of operational equivalence is not conservative; for instance, (let y = clone(z) in []) ≈ [] is a valid equation in the theory for the core calculus, where every value is an object location, but not in the theory for the full calculus, where z may be instantiated to a function value λ(x)b and (let y = clone(λ(x)b) in [], σ) is stuck whereas ([], σ) terminates for any store σ.

Related work

The congruence proof we have presented, based on that of Honsell, Mason, Smith, and Talcott (1993), is quite simple, considering that the imperative object calculus is a higher-order, state-based language. Alternatively, it is possible to adapt Howe’s general method for proving congruence of simulation orderings (Howe 1996) to CIU equivalence; see Gordon (1998) for an example of this for the stateless object calculus of Abadi and Cardelli (1996). Talcott (1998) presents another proof method based on a notion of uniform computation. These proof methods scale up more smoothly when, for example, functions are added to the calculus, but for the core calculus our direct approach is simpler.

Some transformations for rearranging side effects are rather cumbersome to express in terms of equational laws as they depend on variables being bound to distinct locations. We have not pursued this issue in great depth. For further study it would be interesting to consider program logics such as VTLoE (Honsell, Mason, Smith, and Talcott 1993) or specification logic (Reynolds 1982; Reddy 1998) where it is possible to express such conditions directly.

Earlier work on operational equivalence for object calculi has been concerned with stateless objects. For instance, Gordon and Rees (1996) and Gordon (1998) characterise contextual equivalence exactly via forms of bisimilarity induced by the primitive operational semantics of objects. See Stark (1997) for an account of the difficulties of defining bisimulation in the presence of imperative effects.

In recent work, Kleist and Sangiorgi (1998) translate the first-order typed imperative object calculus into a typed π-calculus. Among other results, they verify typed versions of some of our laws by translation into bisimilar π-calculus processes. In comparison, working directly with the operational semantics as we do seems to be simpler than establishing and reasoning about an encoding.

The main influence on this section has been the literature on operational theories for functional languages with state. Our experience is that existing techniques for functional languages with state scale up well to deal with the object-oriented features of the imperative object calculus. CIU equivalence was introduced by Mason and Talcott (1991) and has been the topic of much research; see Talcott (1998) for an overview of this work as well as a more general presentation of the theory. Functional languages with state accommodate imperative object-oriented programming styles; see for example Abelson and Sussman (1985). Operational equivalences of imperative objects in this style have been studied using CIU equivalence by Mason and Talcott (1991, 1992, 1995). But program equivalences for imperative object-oriented languages do not seem to have received much study so far. Our results are a first step and indicate an interesting algebra of imperative objects. Many subtleties of the theory of operational equivalence are shared with theories for functional languages with state, including the examples of Meyer and Sieber (1988). These subleties have been addressed by advanced operational methods (Honsell, Mason, Smith, and Talcott 1993; Pitts and Stark 1998) which should be interesting to study for objects too, but we have not explored these issues here in any depth.

Several authors have studied operational equivalences for languages with concurrent objects (Agha, Mason, Smith, and Talcott 1997; Jones 1996; Walker 1995; Sangiorgi 1997), but the technique of CIU equivalence was not used in these studies.

5 A Refinement: Static Resolution of Labels

In Section 3 we showed how to compile the imperative object calculus to an abstract machine that represents objects as finite lists of labels paired with method closures. In each pair, the first component is the label, and the second component is the method closure. A frequent operation is to resolve a method label, that is, to compute the offset of the method with that label from the beginning of the list. This operation is needed to implement both method select and method update. In general, resolution of method labels needs to be carried out dynamically since one cannot in general compute statically the object to which a select or an update will apply. However, when the select or update is performed on a newly created object, or to self, it is possible to resolve method labels statically. The purpose of this section is to exercise our framework by presenting an algorithm for statically resolving method labels in these situations, and proving its correctness, Theorem 5.

We begin in Section 5.1 by extending our calculus to allow method selects and method updates with respect to integer offsets as well as labels. We present the optimisation algorithm in Section 5.2, give an example in Section 5.3, and prove the correctness of the algorithm in Section 5.4. We discuss related work in Section 5.5.

5.1 Integer Offsets

To represent our intermediate language, we begin by extending the syntax of terms so that selects and updates may be performed on (positive) integer offsets, i or j.

a, b ::= … | a.j | a.j ⇐ ς(x)b terms, 0 < j

As before, we say that a term, a, of this extended language is a static term if and only if locs(a) = ∅.

The intention is that at runtime, a resolved select o.j proceeds by running the jth method of object o. If the jth method of object o has label ℓ, this will have the same effect as o.ℓ. Similarly, an update o.j ⇐ ς(x)b proceeds by updating the jth method of object o with method ς(x)b. If the jth method of object o has label ℓ, this will have the same effect as o.ℓ ⇐ ς(x)b.

To make this precise, the operational semantics of Section 2 and the abstract machine and compiler of Section 3 may easily be extended with integer offsets. We suppress all the details apart from the following.

We extend the reduction contexts of Section 2.2 as follows:

R ::= … | R.j | R.j ⇐ ς(x)b reduction context

We extend the small-step substitution-based semantics of Section 2.2 and the big-step substitution-based semantics of Section 2.3 with these axioms and rules:

(Red Offset Select) (R[ι.j], σ) → (R[b_{j}{{ι/x_{j}}}], σ)

if σ(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] and j ∈ 1..n.

(Red Offset Update) (R[ι.j ⇐ ς(x)b], σ) → (R[ι], σ′)

if σ(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}], j ∈ 1..n and

σ′ = σ + (ι ↦ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..j−1}, ℓ_{j} = ς(x)b, ℓ_{i} = ς(x_{i})b_{i} ^{i∈j+1..n}]).

(Subst Offset Select)

\frac{(a, σ_{0}) ⇓ (ι, σ_{1}) σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] j ∈ 1..n (b_{j}\{\{ι/x_{j}\}\}, σ_{1}) ⇓ (v, σ_{2})}{(a.j, σ_{0}) ⇓ (v, σ_{2})}

(Subst Offset Update)

\frac{\begin{matrix}(a, σ_{0}) ⇓ (ι, σ_{1}) σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}] j ∈ 1..n \\ σ_{2} = σ_{1} + (ι ↦ [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..j−1}, ℓ_{j} = ς(x)b, ℓ_{i} = ς(x_{i})b_{i} ^{i∈j+1..n}]) \end{matrix}}{(a.j ⇐ ς(x)b, σ_{0}) ⇓ (ι, σ_{2})}

All the results proved in Sections 2 and 3 remain true for this extended language.

The reduction contexts used in the definition of experimental equivalence now include include selects and updates with integer offsets. By enriching the syntax with integer offsets we make both experimental equivalence and operational equivalence finer grained. For instance, in the original language the order of methods in an object may be permuted without affecting operational equivalence. For example, if a = [ℓ_{1} = [], ℓ_{2} = ς(s)s.ℓ_{2}] and b = [ℓ_{2} = ς(s)s.ℓ_{2}, ℓ_{1} = []], then a ≈ b. But this equation fails in the presence of reduction contexts with integer offsets, since, for instance, (a.1, []) converges but (b.1, []) diverges. Although the equivalences are finer grained, all the results proved in Section 4 hold for the extended calculus.

5.2 A Static Resolution Algorithm

We need the following definitions to express the static resolution algorithm.

A, B ::= [ℓ_{i} ^{i∈1..n}] layout type, ℓ_{i} distinct E ::= [x_{i} ↦ A_{i} ^{i∈1..n}] environment, x_{i} distinct

For an object o = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}], let layout(o) = [ℓ_{i} ^{i∈1..n}].

The algorithm infers a layout type, A, for each term it encounters. If the layout type A is [ℓ_{i} ^{i∈1..n}], with n > 0, the term must evaluate to an object o with layout(o) = A. On the other hand, if the layout type A is [], nothing has been determined about the layout of the object to which the term will evaluate. An environment E is a finite map that associates layout types to the free variables of a term.

We express the algorithm as the following recursive routine resolve(E, a), which takes an environment E and a static term a with fv(a) ⊆ dom(E), and produces a pair (a′, A), where static term a′ is the residue of a after resolution of labels known from layout types to integer offsets, and A is the layout type of both a and a′. We use p to range over both labels and integer offsets.

resolve(E, x) =^{def} (x, E(x)) where x ∈ dom(E)

resolve(E, [ℓ_{i} = ς(x_{i})a_{i} ^{i∈1..n}]) =^{def} ([ℓ_{i} = ς(x_{i})a′_{i} ^{i∈1..n}], A)

where A = [ℓ_{i} ^{i∈1..n}]

and (a′_{i}, B_{i}) = resolve((x_{i} ↦ A) :: E, a_{i}), x_{i} ∉ dom(E), for each i ∈ 1..n resolve(E, a.p) =^{def}

\{ \begin{matrix}(a′.j, []) & if j ∈ 1..n and p = ℓ_{j} \\ (a′.p, []) & otherwise \end{matrix}
where (a′, [ℓ_{i} ^{i∈1..n}]) = resolve(E, a)

resolve(E, a.p ⇐ ς(x)b) =^{def}

\{ \begin{matrix}(a′.j ⇐ ς(x)b′, A) & if j ∈ 1..n and p = ℓ_{j} \\ (a′.p ⇐ ς(x)b′, A) & otherwise \end{matrix}
where (a′, A) = resolve(E, a), A = [ℓ_{i} ^{i∈1..n}]
and (b′, B) = resolve((x ↦ A) :: E, b), x ∉ dom(E)

resolve(E, clone(a)) =^{def} (clone(a′), A) where (a′, A) = resolve(E, a) resolve(E, let x = a in b) =^{def} (let x = a′ in b′, B)

where (a′, A) = resolve(E, a)

and (b′, B) = resolve((x ↦ A) :: E, b), x ∉ dom(E)

5.3 Example of Static Resolution

To illustrate the algorithm in action, consider the object pair(x, y):

[fst = ς(s)x, snd = ς(s)y, swap = ς(s)\begin{matrix}let x = s.fst in let y = s.snd in \\ (s.fst ⇐ ς(s′)y).snd ⇐ ς(s′)x] \end{matrix}

Then, for arbitrary layout types A and B,

resolve([x ↦ A, y ↦ B], pair(x, y)) = (pair′(x, y), [fst, snd, swap])

where pair′(x, y) denotes the object:

[fst = ς(s)x, snd = ς(s)y, swap = ς(s)\begin{matrix}let x = s.1 in let y = s.2 in \\ (s.1 ⇐ ς(s′)y).2 ⇐ ς(s′)x] \end{matrix}

All method selects and method updates in the object have been statically resolved. The layout type [fst, snd, swap] asserts that pair(x, y) and pair′(x, y) will evaluate to objects with this layout. This means, not surprisingly, that any select or update of fst, snd or swap on pair(x, y) are statically resolved. For instance:

resolve([x ↦ A, y ↦ B], pair(x, y).swap) = (pair′(x, y).3, [])

Here, the empty layout type [] asserts that nothing is known about the layout of the objects returned by pair(x, y).swap and pair′(x, y).3. So, if we select swap twice, the second method select is not resolved:

resolve([x ↦ A, y ↦ B], pair(x, y).swap.swap) = (pair′(x, y).3.swap, [])

5.4 Verification of the Algorithm

To allow proofs by induction on derivations, we begin by representing the algorithm by an inductively defined relation, ↔. We need an auxiliary notion of a store type, a finite map sending locations to layout types:

Σ ::= [ι_{i} ↦ A_{i} ^{i∈1..n}] store type, ι_{i} distinct

By the following rules, we define a resolution relation on terms, (E, Σ) ⊢ a ↔ a′ : A, intended to mean that in environment E and store type Σ, and at layout type A, term a may be resolved to term a′ by turning some of the labels in a into integer offsets in a′.

(Layout x)

\frac{x ∈ dom(E)}{(E, Σ) ⊢ x ↔ x : E(x)}

(Layout ι)

\frac{ι ∈ dom(Σ)}{(E, Σ) ⊢ ι ↔ ι : Σ(ι)}

(Layout Object) (where B = [ℓ_{i} ^{i∈1..n}] and x_{i} ∉ dom(E))

\frac{((x_{i} ↦ B) :: E, Σ) ⊢ a_{i} ↔ a′_{i} : A_{i} ∀i ∈ 1..n}{(E, Σ) ⊢ [ℓ_{i} = ς(x_{i})a_{i} ^{i∈1..n}] ↔ [ℓ_{i} = ς(x_{i})a′_{i} ^{i∈1..n}] : B}

(Layout Select 1)

\frac{(E, Σ) ⊢ a ↔ a′ : A}{(E, Σ) ⊢ a.ℓ ↔ a′.ℓ : []}

(Layout Select 2)

\frac{(E, Σ) ⊢ a ↔ a′ : A}{(E, Σ) ⊢ a.j ↔ a′.j : []}

(Layout Select 3) (where j ∈ 1..n)

\frac{(E, Σ) ⊢ a ↔ a′ : [ℓ_{i} ^{i∈1..n}]}{(E, Σ) ⊢ a.ℓ_{j} ↔ a′.j : []}

(Layout Update 1) (where x ∉ dom(E))

\frac{(E, Σ) ⊢ a ↔ a′ : A ((x ↦ A) :: E, Σ) ⊢ b ↔ b′ : B}{(E, Σ) ⊢ a.ℓ ⇐ ς(x)b ↔ a′.ℓ ⇐ ς(x)b′ : A}

(Layout Update 2) (where x ∉ dom(E))

\frac{(E, Σ) ⊢ a ↔ a′ : A ((x ↦ A) :: E, Σ) ⊢ b ↔ b′ : B}{(E, Σ) ⊢ a.j ⇐ ς(x)b ↔ a′.j ⇐ ς(x)b′ : A}

(Layout Update 3) (where x ∉ dom(E), A = [ℓ_{i} ^{i∈1..n}] and j ∈ 1..n)

\frac{(E, Σ) ⊢ a ↔ a′ : A ((x ↦ A) :: E, Σ) ⊢ b ↔ b′ : B}{(E, Σ) ⊢ a.ℓ_{j} ⇐ ς(x)b ↔ a′.j ⇐ ς(x)b′ : A}

(Layout Clone)

\frac{(E, Σ) ⊢ a ↔ a′ : A}{(E, Σ) ⊢ clone(a) ↔ clone(a′) : A}

(Layout Let) (where x ∉ dom(E))

\frac{(E, Σ) ⊢ a ↔ a′ : A ((x ↦ A) :: E, Σ) ⊢ b ↔ b′ : B}{(E, Σ) ⊢ let x = a in b ↔ let x = a′ in b′ : B}

We need the (Layout ι) rule and store types so that the resolution relation is defined on arbitrary terms. Even though the resolve(E, a) routine takes a static term a as its input, we cannot simply define the resolution relation on static terms. If we did so, we would not be able to prove Proposition 15, which relates resolution and evaluation, since terms containing locations may arise from evaluation of static terms.

This resolution relation on terms includes all the possible outcomes of running the algorithm:

Lemma 31 Suppose that a is a static term and E is an environment with fv(a) ⊆ dom(E). If routine resolve(E, a) returns (a′, A), then the judgment (E, []) ⊢ a ↔ a′ : A is derivable.

Proof By induction on the number of recursive calls made by the routine resolve(E, a), using all the rules but (Layout ι). □

For illustration, let us revisit the pair example from Section 5.1. Via (Layout Object), (Layout x), (Layout Let), (Layout Select 3) and (Layout Update 3) we may derive:

([x ↦ A, y ↦ B], []) ⊢ pair(x, y) ↔ pair′(x, y) : [fst, snd, swap]

Further, via (Layout Select 3) and (Layout Select 1) we derive:

([x ↦ A, y ↦ B], []) ⊢ pair(x, y).swap ↔ pair′(x, y).3 : []

([x ↦ A, y ↦ B], []) ⊢ pair(x, y).swap.swap ↔ pair′(x, y).3.swap : []

We will make precise the connection between evaluation and resolution in Proposition 15. Since evaluation is defined on configurations, to state the proposition we first need need to extend the resolution relation to stores and configurations. By the following rules, we define a resolution relation, ⊢ σ ↔ σ′ : Σ, on store pairs, and another, ⊢ c ↔ c′ : (A, Σ), on configuration pairs:

(Layout Store) (where dom(Σ) = dom(σ) = dom(σ′))

\frac{Σ(ι) = layout(σ(ι)) = layout(σ′(ι)) ([], Σ) ⊢ σ(ι) ↔ σ′(ι) : Σ(ι) ∀ι ∈ dom(Σ)}{⊢ σ ↔ σ′ : Σ}

(Layout Config)

\frac{([], Σ) ⊢ a ↔ a′ : A Σ ⊢ σ ↔ σ′}{⊢ (a, σ) ↔ (a′, σ′) : (A, Σ)}

For example, consider the store σ = [ι_{1} ↦ o_{1}, ι_{2} ↦ o_{2}] and a store type Σ = [ι_{1} ↦ A_{1}, ι_{2} ↦ A_{2}] such that ⊢ σ ↔ σ : Σ. Then, using the rules above, we may derive:

⊢ (pair(ι_{1}, ι_{2}).swap, σ) ↔ (pair′(ι_{1}, ι_{2}).3, σ) : ([], Σ)

where pair′(ι_{1}, ι_{2}) is the object pair(ι_{1}, ι_{2}) with all labels resolved, as in the previous example. Given the set of rules defining the resolution relation, we cannot derive a layout type other than [] for pair(ι_{1}, ι_{2}).swap and pair′(ι_{1}, ι_{2}).3.

To see the effect of evaluation on the layout type of these configurations, we derive:

(pair(x, y).swap, σ) ⇓ (ι, (ι ↦ pair(ι_{2}, ι_{1})) :: σ)

and

(pair′(x, y).3, σ) ⇓ (ι, (ι ↦ pair′(ι_{2}, ι_{1})) :: σ)

where ι ∉ dom(σ), by the evaluation rules from Section 2.3 and Section 5.1. Moreover, using the rules above, we may derive:

⊢ (ι, (ι ↦ pair(ι_{2}, ι_{1})) :: σ) ↔ (ι, (ι ↦ pair′(ι_{2}, ι_{1})) :: σ) : (A, (ι ↦ A) :: Σ)

where A = [fst, snd, swap].

This example shows that, as one might expect, evaluation increases the accuracy of the layout types derivable for a configuration. In seeking to verify the resolve routine, we introduced the resolution relation because it includes all the results of running resolve, Lemma 31, but also because we can prove that resolution is preserved by evaluation, Proposition 15. We first need the following substitution lemma.

Lemma 32 (E′@[x ↦ A]@E′′, Σ) ⊢ a ↔ a′ : B, ι ∈ dom(Σ) and Σ(ι) = A imply (E′@E′′, Σ) ⊢ a{{ι/x}} ↔ a′{{ι/x}} : B.

Proof A routine induction on the derivation of the judgment (E′@[x ↦ A]@E′′, Σ) ⊢ a ↔ a′ : B. □

If Σ and Σ′ are store types, let Σ ≤ Σ′ if and only if dom(Σ) ⊆ dom(Σ′) and Σ(ι) = Σ′(ι) for each ι ∈ dom(Σ).

Proposition 15 Suppose that ⊢ c ↔ c′ : (A, Σ).

(1) Whenever c ⇓ d there are d′, A′ and Σ′ such that c′ ⇓ d′, ⊢ d ↔ d′ : (A′, Σ′) and Σ ≤ Σ′. Moreover, A ≠ [] implies A = A′.

(2) Whenever c′ ⇓ d′ there are d, A′ and Σ′ such that c ⇓ d and ⊢ d ↔ d′ : (A′, Σ′) and Σ ≤ Σ′. Moreover, A ≠ [] implies A = A′.

Proof We shall prove part (1); part (2) follows by an almost symmetric argument. The proof proceeds by induction on the derivation of c ⇓ d.

We show the case for (Subst Select).

(Subst Select) In this case c = (a.ℓ_{j}, σ_{0}), (a, σ_{0}) ⇓ (ι, σ_{1}), σ_{1}(ι) = [ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}], j ∈ 1..n and (b_{j}{{ι/x_{j}}}, σ_{1}) ⇓ d. Only (Layout Config) can derive ⊢ (a.ℓ_{j}, σ_{0}) ↔ c′ : (A, Σ), so c′ must take the form (b′, σ′_{0}) with ([], Σ) ⊢ a.ℓ_{j} ↔ b′ : A and ⊢ σ_{0} ↔ σ′_{0} : Σ. Either (Layout Select 1), (Layout Select 2) or (Layout Select 3) can derive ([], Σ) ⊢ a.ℓ_{j} ↔ b′ : A. We shall consider the latter case:

(Layout Select 3) Here b′ = a′.j and A = [], with ([], Σ) ⊢ a ↔ a′ : B, j ∈ 1..m and ℓ′_{j} = ℓ where B = [ℓ′_{i} ^{i∈1..m}]. Since j ∈ 1..m, B ≠ []. By (Layout Config), ⊢ σ_{0} ↔ σ′_{0} : Σ and ([], Σ) ⊢ a ↔ a′ : B imply ⊢ (a, σ_{0}) ↔ (a′, σ′_{0}) : (B, Σ). Hence, by induction hypothesis, (a, σ_{0}) ⇓ (ι, σ_{1}) and B ≠ [] imply there is a configuration d_{1} and a store type Σ_{1} such that (a′, σ′_{0}) ⇓ d_{1}, ⊢ (ι, σ_{1}) ↔ d_{1} : (B, Σ_{1}) and Σ ≤ Σ_{1}. Hence d_{1} = (ι, σ′_{1}) with ([], Σ_{1}) ⊢ ι ↔ ι : B, which implies that ι ∈ dom(Σ_{1}), Σ_{1}(ι) = B and ⊢ σ_{1} ↔ σ′_{1} : Σ_{1}. By the latter, ([], Σ_{1}) ⊢ σ_{1}(ι) ↔ σ′_{1}(ι) : B. The latter implies that layout([ℓ_{i} = ς(x_{i})b_{i} ^{i∈1..n}]) = B, and therefore that B = [ℓ_{i} ^{i∈1..n}], m = n and each ℓ_{i} = ℓ′_{i}. It also implies there is o′ with σ′_{1}(ι) = o′ and o′ = [ℓ_{i} = ς(x_{i})b′_{i} ^{i∈1..n}]. By (Layout Object), there is A_{j} with ([x_{j} ↦ B], Σ_{1}) ⊢ b_{j} ↔ b′_{j} : A_{j}. By Lemma 32, ι ∈ dom(Σ_{1}) implies ([], Σ_{1}) ⊢ b_{j}{{ι/x_{j}}} ↔ b′_{j}{{ι/x_{j}}} : A_{j}. By (Layout Config), ⊢ (b_{j}{{ι/x_{j}}}, σ_{1}) ↔ (b′_{j}{{ι/x_{j}}}, σ′_{1}) : (A_{j}, Σ_{1}). By induction hypothesis, the latter and (b_{j}{{ι/x_{j}}}, σ_{1}) ⇓ c′ imply there are d′, A′ and Σ′ such that (b′_{j}{{ι/x_{j}}}, σ′_{1}) ⇓ d′, ⊢ c′ ↔ d′ : (A′, Σ′) and Σ_{1} ≤ Σ′. By (Subst Offset Select), we have c′ = (a′.j, σ′_{0}) ⇓ d′. We have Σ ≤ Σ′ from Σ ≤ Σ_{1} and Σ_{1} ≤ Σ′, since ≤ is clearly transitive. Finally, A ≠ [] implies A = A′ holds vacuously, since A = [].

The cases for (Layout Select 1) and (Layout Select 2) are very similar.

We omit the remaining cases, which are no harder than the one shown. The case for (Subst Update) is similar to the one shown. The cases for (Subst Offset Select) and (Subst Offset Update) are slightly simpler than (Subst Select) and (Subst Update) respectively. The remaining cases are routine. □

Lemma 33 Suppose ([x_{i} ↦ [] ^{i∈1..n}], []) ⊢ a ↔ a′ : A. Consider any reduction context R with locs(R) = ∅ such that fv(R) − {•, x_{1}, …, x_{n}} = {x_{n+1}, …, x_{n+m}}. Then ([x_{i} ↦ []^{i∈1..n+m}], []) ⊢ R[a] ↔ R[a′] : B for some B.

Proof By induction on the size of the reduction context R, with appeal to rules (Layout Select 1), (Layout Select 2), (Layout Update 1), (Layout Update 2), (Layout Clone) and (Layout Let). Moreover, we need the facts that the ↔ relation is reflexive (if locs(a) ⊆ dom(Σ) and fv(a) ⊆ dom(E) then (E, Σ) ⊢ a ↔ a : A holds for some A) and satisfies environment weakening (if dom(E) ⊆ dom(E′) and E(x) = E′(x) for each x ∈ dom(E), then (E, Σ) ⊢ a ↔ a′ : A implies (E′, Σ) ⊢ a ↔ a′ : A). □

Lemma 34 Given ([x_{i} ↦ [] ^{i∈1..n}], []) ⊢ a ↔ a′ : B, a store type Σ and a substitution ρ : {x_{1}, …, x_{n}} → dom(Σ), there is B′ such that ([], Σ) ⊢ aρ ↔ a′ρ : B′. Moreover, B ≠ [] implies B = B′.

Proof By induction on the derivation of ([x_{i} ↦ []^{i∈1..n}], []) ⊢ a ↔ a′ : B. □

Theorem 5 Suppose a is a static term with free variables x_{1},…,x_{n}. If routine resolve([x_{i} ↦ []^{i∈1..n}], a) returns (a′, A), then a ≈ a′.

Proof By Lemma 28, to show a ≈ a′, it suffices to prove (R[a]ρ, σ) ↕ (R[a′]ρ, σ), for all static reduction contexts R, well formed stores σ, and substitutions ρ : fv(R[a]) ∪ fv(R[a′]) → dom(σ). Consider any static reduction context R, any well formed store σ and any substitution ρ : fv(R[a]) ∪ fv(R[a′]) → dom(σ). Let E = [x_{i} ↦ [] ^{i∈1..n}] and E′ = [x_{i} ↦ [] ^{i∈1..n+m}] where {x_{n+1}, …, x_{n+m}} = fv(R) − {•, x_{1}, …, x_{n}}. By Lemma 31, we may derive (E, []) ⊢ a ↔ a′ : A. By Lemma 33, (E, []) ⊢ a ↔ a′ : A implies (E′, []) ⊢ R[a] ↔ R[a′] : B for some B. If σ = [ι_{i} = o_{i} ^{i∈1..n}], let Σ = [ι_{i} = layout(o_{i})^{i∈1..n}]. By Lemma 34, (E′, []) ⊢ R[a] ↔ R[a′] : B and ρ : {x_{1}, …, x_{n+m}} → dom(Σ) imply ([], Σ) ⊢ R[a]ρ ↔ R[a′]ρ : B′ for some B′. By (Layout Store), Σ ⊢ σ ↔ σ. Hence by (Layout Config), we have ⊢ (R[a]ρ, σ) ↔ (R[a′]ρ, σ). Suppose that (R[a]ρ, σ)↓. By Theorem 1 there is c with (R[a]ρ, σ) ⇓ c. By Proposition 15(1), ⊢ (R[a]ρ, σ) ↔ (R[a′]ρ, σ) implies there is c′ such that (R[a′]ρ, σ) ⇓ c′, and therefore (R[a′]ρ, σ)↓, again by Theorem 1. Similarly, by Proposition 15(2) and ⊢ (R[a]ρ, σ) ↔ (R[a′]ρ, σ), (R[a′]ρ, σ)↓ implies (R[a]ρ, σ)↓. Therefore (R[a]ρ, σ) ↕ (R[a′]ρ, σ), as required to establish that a ≈ a′. □

Our prototype implementation of the imperative object calculus optimises any closed static term a by running the routine resolve([], a) to obtain an optimised term a′ paired with a layout type A. By the theorem, this optimisation is correct in the sense that a′ is operationally equivalent to a. In fact the theorem applies to applications of the resolve routine to open terms. Inasmuch as we may regard a module as a term with free variables, the theorem would justify use of resolve during separate compilation of modules.

On a limited set of test programs, the algorithm converts a majority of selects and updates into the optimised form. However, the speedup ranges from modest (10%) to negligible; the interpretive overhead in our bytecodebased system tends to swamp the effect of optimisations such as this. It is likely to be more effective in a native code implementation.

5.5 Discussion and Related Work

In general, there are many algorithms for optimising access to objects; see Chambers (1992), for instance, for examples and a literature survey. The idea of statically resolving labels to integer offsets is found also in the work of Ohori (1992), who presents a λ-calculus with records and a polymorphic type system such that a compiler may compute integer offsets for all uses of record labels. Our system is rather different, in that it exploits objectoriented references to self.

In contrast to Ohori’s type system, we have not integrated our layout types with a conventional type system that guarantees the absence of unchecked runtime errors. Our system of layout types could probably be integrated with one or other of Abadi and Cardelli’s type systems for the imperative object calculus, to obtain a unified type system that avoided unchecked runtime errors and moreover could determine statically the layout of certain objects. Instead, our implementation checks programs using one of Abadi and Cardelli’s type systems in one pass, and in a separate pass uses the algorithm from this section to optimise updates and selects. This separation avoids the complications of a unified type system.

Two alternative approaches to program analysis for untyped object calculi are the abstract flow logic control flow analysis for the imperative object calculus by Nielson and Nielson (1998) and the set-based control flow analysis for a concurrent, imperative object calculus by di Blasio, Fisher, and Talcott (1997). Both should be adaptable to the problem of statically resolving method offsets. These approaches are rather more complex than ours but may lead to more precise results.

6 Conclusions

In this paper, we have collated and extended a range of operational techniques in order to verify aspects of the implementation of a small object-oriented programming language, Abadi and Cardelli’s imperative object calculus.

First, we presented both a big-step and a small-step substitution-based operational semantics for the calculus and proved them equivalent to a closurebased operational semantics like that given by Abadi and Cardelli (Theorem 1 and Theorem 2).

Next, we designed an object-oriented abstract machine as a straightforward extension of Leroy’s abstract machine with instructions for manipulating objects. Our third result is a correctness proof for the abstract machine and its compiler (Theorem 3). Such results are rather more difficult than proofs of interpretive abstract machines. Our contribution is a direct proof method which avoids the need for any metalanguage—such as a calculus of explicit substitutions.

Our fourth result is that Mason and Talcott’s CIU equivalence coincides with Morris-style contextual equivalence (Theorem 4). This is the first result about program equivalence for the imperative object calculus, a topic left unexplored by Abadi and Cardelli’s book. The selection of laws of program equivalence that we establish is a first step towards an algebra of imperative objects that may be useful for future work on imperative object-oriented languages. Already, typed versions of some of our laws have been verified for a typed imperative object calculus (Kleist and Sangiorgi 1998).

One benefit of CIU equivalence is that it allows the verification of compiler optimisations. We illustrate this by proving that an optimisation algorithm from our implementation preserves contextual equivalence (Theorem 5).

Acknowledgements

Martín Abadi, Greg Sullivan, Carolyn Talcott and several anonymous referees commented on previous versions of this paper. Arthur Nunes pointed out an error in the unloading machine in Section 3. During the course of this work, Gordon held a Royal Society University Research Fellowship and Hankin held an EPSRC Research Studentship. Lassen was supported by a grant from the Danish Natural Science Research Council.

References

Abadi, M. and L. Cardelli (1995a). An imperative object calculus. In Proceedings TAPSOFT’95, Volume 915 of Lecture Notes in Computer Science, pp. 471–485. Springer-Verlag.

Abadi, M. and L. Cardelli (1995b). An imperative object calculus: Basic typing and soundness. In Proceedings SIPL’95. Technical Report UIUCDCS-R-95-1900, Department of Computer Science, University of Illinois at Urbana-Champaign.

Abadi, M. and L. Cardelli (1996). A Theory of Objects. Springer-Verlag.

Abelson, H. and G. Sussman (1985). Structure and Interpretation of Computer Programs. MIT Press, Cambridge, Mass.

Agha, G., I. Mason, S. Smith, and C. Talcott (1997). A foundation for actor computation. Journal of Functional Programming 7 (1), 1–72.

Cardelli, L. (1995). A language with distributed scope. Computing Systems 8 (1), 27–59.

Chambers, C. (1992). The Design and Implementation of the Self Compiler, an Optimizing Compiler for Object-Oriented Programming Languages. Ph. D. thesis, Computer Science Department, Stanford University.

di Blasio, P., K. Fisher, and C. Talcott (1997). Analysis for concurrent objects. In H. Bowman and J. Derrick (Eds.), Proceedings FMOODS’97, Canterbury, UK. Chapman and Hall.

Felleisen, M. and D. Friedman (1986). Control operators, the SECDmachine, and the λ-calculus. In Formal Description of Programming Concepts III, pp. 193–217. North-Holland.

Felleisen, M. and D. Friedman (1989). A syntactic theory of sequential state. Theoretical Computer Science 69, 243–287.

Gordon, A. (1994). Functional Programming and Input/Output. Cambridge University Press.

Gordon, A. (1998). Operational equivalences for untyped and polymorphic object calculi. See Gordon and Pitts (1998).

Gordon, A. and P. Hankin (1998). A concurrent object calculus: Reduction and typing. In Proceedings HLCL’98, ENTCS. Elsevier.

Gordon, A. and A. Pitts (Eds.) (1998). Higher Order Operational Techniques in Semantics. Publications of the Newton Institute. Cambridge University Press.

Gordon, A. and G. Rees (1996). Bisimilarity for a first-order calculus of objects with subtyping. In Proceedings POPL’96, pp. 386–395. ACM. Accepted for publication in Information and Computation.

Gordon, A. D., P. Hankin, and S. B. Lassen (1997). Compilation and equivalence of imperative objects. In S. Ramesh and G. Sivakumar (Eds.), Proc. 17th FST&TCS Conference, Kharagpur, India, December 1997, Volume 1346 of Lecture Notes in Computer Science, pp. 74–87. Springer-Verlag.

Guttman, J., V. Swarup, and J. Ramsdell (1995). The VLISP verified Scheme system. Lisp and Symbolic Computation 8 (1/2), 33–110.

Hannan, J. and D. Miller (1992). From operational semantics to abstract machines. Mathematical Structures in Computer Science 4 (2), 415– 489.

Hardin, T., L. Maranget, and B. Pagano (1998). Functional runtime systems within the lambda-sigma calculus. Journal of Functional Programming 8 (2), 131–176.

Honsell, F., I. Mason, S. Smith, and C. Talcott (1993). A variable typed logic of effects. Information and Computation 119 (1), 55–90.

Howe, D. (1996). Proving congruence of bisimulation in functional programming languages. Information and Computation 124 (2), 103–112.

Jones, C. (1996). Accommodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design 8 (2), 105–122.

Kahn, G. (1987). Natural semantics. In Proceedings STACS’87, Volume 247 of Lecture Notes in Computer Science, pp. 22–39. Springer-Verlag.

Kleist, J. and D. Sangiorgi (1998). Imperative objects and mobile processes. In Proceedings PROCOMET’98, Shelter Island, New York.

Landin, P. (1964). The mechanical evaluation of expressions. Computer Journal 6, 308–320.

Leroy, X. (1990). The ZINC experiment: an economical implementation of the ML language. Technical Report 117, INRIA, Rocquencourt.

Martin-Löf, P. (1983). Notes on the domain interpretation of type theory. Proceedings of the Workshop on Semantics of Programming Languages, Chalmers, 1983. See also Nordström, Petersson, and Smith (Nordström et al. 1990).

Mason, I. and C. Talcott (1991). Equivalence in functional languages with effects. Journal of Functional Programming 1 (3), 287–327.

Mason, I. and C. Talcott (1992). References, local variables and operational reasoning. In Proceedings LICS’92.

Mason, I. and C. Talcott (1995). Reasoning about object systems in VT-LoE. International Journal of Foundations of Computer Science 6 (3), 265–298.

Meyer, A. and S. Cosmadakis (1988). Semantical paradigms: Notes for an invited lecture. In Proceedings LICS’88, pp. 236–253.

Meyer, A. and K. Sieber (1988). Towards fully abstract semantics for local variables. In Proceedings POPL’88, pp. 236–253.

Milner, R., M. Tofte, and R. Harper (1990). The Definition of Standard ML. MIT Press, Cambridge, Mass.

Moggi, E. (1989). Notions of computations and monads. Information and Computation 93, 55–92. Earlier version in Proceedings LICS’89.

Morris, J. (1968). Lambda-Calculus Models of Programming Languages. Ph. D. thesis, MIT.

Nielson, F. and H. Nielson (1998). The flow logic of imperative objects. In Proceedings MFCS’98, Lecture Notes in Computer Science. Springer-Verlag.

Nordström, B., K. Petersson, and J. Smith (1990). Programming in Martin-Löf’s Type Theory, Volume 7 of The International Series of Monographs in Computer Science. Clarendon Press, Oxford.

Ohori, A. (1992). A compilation method for ML-style polymorphic record calculi. In Proceedings POPL’92, pp. 154–165. ACM.

Pitts, A. and I. Stark (1998). Operational reasoning for functions with local state. See Gordon and Pitts (1998), pp. 227–273.

Plotkin, G. (1975). Call-by-name, call-by-value and the lambda calculus. Theoretical Computer Science 1, 125–159.

Plotkin, G. (1977). LCF considered as a programming language. Theoretical Computer Science 5, 223–255.

Plotkin, G. (1981). A structural approach to operational semantics. Technical Report FN–19, DAIMI, Aarhus University.

Reddy, U. S. (1998). Objects and classes in Algol-like languages. In Proceedings FOOL’98.

Reynolds, J. C. (1982). Idealized Algol and its specification logic. In D. Néel (Ed.), Tools and Notions for Program Construction, pp. 121– 161. Cambridge University Press. (Reprinted as Chapter 6 of O’Hearn and Tennent (eds.) Algol-like Languages, Birkhäuser, Boston, 1997.).

Rittri, M. (1990). Proving compiler correctness by bisimulation. Ph. D. thesis, Chalmers.

Sangiorgi, D. (1997). Typed π-calculus at work: a proof of Jones’ parallelisation transformation on concurrent objects. In Proceedings FOOL’97.

Sestoft, P. (1997). Deriving a lazy abstract machine. Journal of Functional Programming 3 (7), 231–264.

Stark, I. (1997). Names, equations, relations: Practical ways to reason about new. In Proceedings TLCA’97, Number 1210 in LNCS, pp. 336– 353. Springer.

Talcott, C. (1998). Reasoning about functions with effects. See Gordon and Pitts (1998), pp. 347–390.

Walker, D. (1995). Objects in the pi-calculus. Information and Computation 116 (2), 253–271.

Wand, M. (1995). Compiler correctness for parallel languages. In Proceedings FPCA’95, pp. 120–134. ACM.

Recent BRICS Report Series Publications

RS-98-55 Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and Equivalence of Imperative Objects (Revised Report). December 1998. iv+75 pp. This is a revision of Technical Report 429, University of Cambridge Computer Laboratory, June 1997, and the earlier BRICS report RS-97-19, July 1997. Appears in Ramesh and Sivakumar, editors, Foundations of Software Technology and Theoretical Computer Science: 17th Conference, FST&TCS ’97 Proceedings, LNCS 1346, 1997, pages 74–87.

RS-98-54 Olivier Danvy and Ulrik P. Schultz. Lambda-Dropping: Transforming Recursive Equations into Programs with Block Structure. December 1998. 55 pp. To appear in Theoretical Computer Science.

RS-98-53 Julian C. Bradfield. Fixpoint Alternation: Arithmetic, Transition Systems, and the Binary Tree. December 1998. 20 pp.

RS-98-52 Josva Kleist and Davide Sangiorgi. Imperative Objects and Mobile Processes. December 1998. 22 pp. Appears in Gries and de Roever, editors, IFIP Working Conference on Programming Concepts and Methods, PROCOMET ’98 Proceedings, 1998, pages 285–303.

RS-98-51 Peter Krogsgaard Jensen. Automated Modeling of Real-Time Implementation. December 1998. 9 pp. Aapears in The 13th IEEE Conference on Automated Software Engineering, ASE ’98 Doctoral Symposium Proceedings, 1998, pages 17–20.

RS-98-50 Luca Aceto and Anna Ingólfsdóttir. Testing Hennessy-Milner Logic with Recursion. December 1998. 15 pp. Appears in Thomas, editor, Foundations of Software Science and Computation Structures: Second International Conference, FoSSaCS ’99 Proceedings, LNCS 1578, 1999, pages 41–55.

RS-98-49 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Cook’s Tour of Equational Axiomatizations for Prefix Iteration. December 1998. 14 pp. Appears in Nivat, editor, Foundations of Software Science and Computation Structures: First International Conference, FoSSaCS ’98 Proceedings, LNCS 1378, 1998, pages 20–34.