BRICS

Basic Research in Computer Science

Inter-Deriving Semantic Artifacts for Object-Oriented Programming

Olivier Danvy Jacob Johannsen BRICS Report Series RS-08-5 ISSN 0909-0878 June 2008 BRICS RS-08-5 Danvy & Johannsen: Inter-Deriving Semantic Artifacts for Object-Oriented Programming Copyright \begin{matrix}c \\ ◯ \end{matrix} 2008, Olivier Danvy & Jacob Johannsen.

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 IT-parken, Aabogade 34 DK–8200 Aarhus N Denmark

Telephone: +45 8942 9300
Telefax: +45 8942 5601
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/08/5/

Inter-Deriving Semantic Artifacts for Object-Oriented Programming

Olivier Danvy and Jacob Johannsen Department of Computer Science University of Aarhus^{∗}

June 12, 2007

Abstract

We present a new abstract machine for Abadi and Cardelli’s untyped calculus of objects. What is special about this semantic artifact (i.e., man-made construct) is that is mechanically corresponds to both the reduction semantics (i.e., small-step operational semantics) and the natural semantics (i.e., big-step operational semantics) specified in Abadi and Cardelli’s monograph. This abstract machine therefore embodies the soundness of Abadi and Cardelli’s reduction semantics and natural semantics relative to each other.

To move closer to actual implementations, which use environments rather than actual substitutions, we then represent object methods as closures and in the same inter-derivational spirit, we present three new semantic artifacts: a reduction semantics for a version of Abadi and Cardelli’s untyped calculus of objects with explicit substitutions, an environment-based abstract machine, and a natural semantics (i.e., an interpreter) with environments. These three new semantic artifacts mechanically correspond to each other, and furthermore, they are coherent with the previous ones since as we show, the two abstract machines are bisimilar. Overall, though, the significance of these artifacts lies in them not having been designed from scratch and then proved correct: instead, they were mechanically inter-derived.

∗ IT-parken, Aabogade 34, DK-8200 Aarhus N, Denmark.

Email: {danvy,cnn}@daimi.au.dk

Contents

1 Introduction 1 1.1 Background and first contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Further background and contributions . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.3 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3

2 Abadi and Cardelli’s untyped calculus of objects: the ς-calculus 4 2.1 A reduction semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 2.2 The corresponding abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.3 The corresponding natural semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.4 Summary and conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

3 Object methods as closures: the ςρ-calculus 6 3.1 A natural semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 6 3.2 The corresponding abstract machine . . . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.3 The corresponding reduction semantics . . . . . . . . . . . . . . . . . . . . . . . . . 7 3.4 Summary and conclusion . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

4 Coherence between the ς-calculus and the ςρ-calculus 9 4.1 From closures to terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 4.2 A bisimulation between the two abstract machines . . . . . . . . . . . . . . . . . . . 9

5 Related work 10

6 Conclusion and issues 10

1 Introduction

Our goal here is to apply Danvy et al.’s ‘syntactic correspondence’ and ‘functional correspondence’ [3, 8, 12, 21, 37–39], which were developed for the λ-calculus with effects, to Abadi and Cardelli’s untyped calculus of objects [1, Chapter 6].

1.1 Background and first contribution

The syntactic correspondence between reduction semantics and abstract machines: This correspondence mechanically links a reduction semantics (i.e., a small-step operational semantics with an explicit representation of reduction contexts [27, 28]) to an abstract machine. In such a reduction semantics, evaluation is implemented by iterated reduction, and the corresponding reduction sequence can be depicted as follows:

[figure: ∘; decompose; reduction step; ∘; decompose; reduction step; ∘; decompose; ∘; contract; ∘; plug; ∘; contract; ∘; plug; ∘; contract]

At each step, a non-value term is decomposed into a reduction context and a potential redex. If the potential redex is an actual one (i.e., if it is not stuck), it is contracted. The contractum is then plugged into the context, yielding the next term in the reduction sequence.

At each step, the function plug therefore constructs an intermediate term. In the course of evaluation, this term is then immediately decomposed by the subsequent call to decompose. The composition of plug and decompose can thus be replaced by a more efficient function, refocus, that directly goes from redex site to redex site in the reduction sequence:

[figure: ∘; decompose; ∘; decompose; ∘; decompose; ∘; contract; ∘; plug; refocus; ∘; contract; ∘; plug; refocus; ∘; contract]

As shown by Danvy and Nielsen [25], refocus can take the form of a state-transition function. Therefore, together with contract, the result is an abstract machine. And what is remarkable here is that the abstract machines obtained by refocusing are not unnatural ones.

In fact, this syntactic correspondence between reduction semantics and abstract machines has made it possible to obtain a variety of abstract machines for the λ-calculus, be it pure or with effects. Some of these machines were independently known and some others are new [10, 11]. Symmetrically, it also has made it possible to exhibit the calculi and the reduction strategies (in the form of reduction semantics) corresponding to pre-existing abstract machines.

The functional correspondence between natural semantics and abstract machines: This correspondence mechanically links a natural semantics (i.e., a big-step operational semantics, as implemented by an interpreter [32, 40]) to an abstract machine. It is based on the framework initiated by Reynolds in his seminal article “Definitional Interpreters for Higher-Order Programming Languages” [41]. In a nutshell, successively transforming an interpreter using closure conversion, transformation into continuation-passing style (CPS), and defunctionalization yields an abstract machine [4]. And what is remarkable here is that the abstract machines obtained by CPS transformation and defunctionalization are not unnnatural ones.

In fact, this functional correspondence between natural semantics and abstract machines has made it possible to obtain a variety of abstract machines for the λ-calculus, be it pure or with effects. Some of these machines were independently known and some others are new [5, 6, 9].

Symmetrically, it also has made it possible to exhibit the interpreter (in the form of a natural semantics) corresponding to pre-existing abstract machines.

Our starting point here: Together, the syntactic and the functional correspondences make it possible to connect three semantic artifacts (i.e., man-made constructs) soundly: reduction semantics, abstract machines, and natural semantics. Better: the correspondence make it possible to inter-derive these semantics (or more precisely, their representation as functional programs), mechanically. This inter-derivation contrasts with defining several semantics, which requires work, and proving their soundness relative to each other, which requires more work. As Rod Burstall soberly put it once, “theory should be call by need.” Our goal here is to apply these two correspondences to Abadi and Cardelli’s untyped calculus of objects.

Abadi and Cardelli’s untyped calculus of objects: Abadi and Cardelli’s monograph “A Theory of Objects” is a landmark. Nowadays it provides standard course material about object-oriented languages and programming. Of interest to us here is its Chapter 6 where an untyped calculus of objects, the ς-calculus, is developed in the same spirit as its predecessor, the λ-calculus [7, 14], which was initially developed as an untyped calculus of functions. The ς-calculus is specified with a reduction semantics, for a given reduction order, and with a natural semantics, for a given evaluation order. A soundness theorem (Proposition 6.2-3, page 64) links the two semantics. Operational reduction is also shown to be complete with respect to many-step reduction with a completeness theorem (Theorem 6.2-4, page 65). Soundness matters because it shows that the interpreter implementing the natural semantics is faithful to the reduction semantics and vice versa. Completeness matters because it shows that the reductions may be meaningfully reordered, thus enabling practical optimizations such as constant propagation and more generally partial evaluation [15, 31].

First contribution: Using the syntactic correspondence, we exhibit an abstract machine that embodies the reduction semantics of the ς-calculus and its reduction strategy. Using the functional correspondence, we exhibit an abstract machine that embodies the natural semantics of the ς-calculus and its evaluation strategy. The two abstract machines are identical. This abstract machine, which is new, therefore mediates between the reduction semantics and the natural semantics, and practically confirms the soundness theorem:

[figure: reduction ; semantics ; for the ; ς-calculus; syntactic; correspondence; abstract ; machine ; for the ; ς-calculus; natural ; semantics ; for the ; ς-calculus; functional; correspondence]

1.2 Further background and contributions

Substitutions vs. environments: Practical implementations of the λ-calculus do not use actual substitutions. Instead, they use ‘environments,’ which are mappings representing delayed substitutions, and represent functions with ‘closures,’ which are pairs of terms and environments [34]. In such practical implementations, an identifier is not a thing to be substituted by a term, but a thing to be looked up in the current environment. At the turn of the 1990’s [17], Curien proposed a ‘calculus of closures,’ the λρ-calculus, to account for this implementation strategy of the λ-calculus, and explicit substitutions were born [2, 18, 43]. Both the syntactic and the functional correspondences have been applied to calculi of explicit substitutions, environment-based abstract machines, and natural semantics using environments [4, 10].

Abadi and Cardelli’s untyped calculus of objects with methods as closures: We present a version of the ς-calculus with explicit substitutions, the ςρ-calculus. Instead of performing substitution when invoking a method, we represent methods as closures. We state three semantic artifacts for the ςρ-calculus: a natural semantics, an abstract machine, and a reduction semantics.

Contributions: Using the syntactic correspondence, we exhibit an environment-based abstract machine that embodies the reduction semantics of the ςρ-calculus and its reduction strategy. Using the functional correspondence, we exhibit an environment-based abstract machine that embodies the natural semantics of the ςρ-calculus and its evaluation strategy. Again, the two abstract machines are identical, which establishes the soundness of the reduction semantics and of the natural semantics for the ςρ-calculus relative to each other. We then show that this environmentbased abstract machine and the abstract machine with actual substitutions from Section 1.1 are bisimilar, which establishes the coherence of the ςρ-calculus with respect to the ς-calculus:

[figure: reduction ; semantics ; for the ; ς-calculus; syntactic; correspondence; abstract ; machine ; for the ; ς-calculus; bisimilarity; natural ; semantics ; for the ; ς-calculus; functional; correspondence; reduction ; semantics ; for the ; ςρ-calculus; syntactic; correspondence; abstract ; machine ; for the ; ςρ-calculus; natural ; semantics ; for the ; ςρ-calculus; functional; correspondence]

As for having a completeness theorem for the ςρ-calculus, Melliès’s proof applies mutatis mutandis [1, Theorem 6.2-4, page 65].

1.3 Overview

In Section 2, we remind the reader of the ς-calculus (Section 2.1) and we present its reduction semantics; through the syntactic correspondence, we obtain the corresponding abstract machine (Section 2.2). Through the functional correspondence, we then present the natural semantics corresponding to this abstract machine (Section 2.3). This natural semantics coincides with Abadi and Cardelli’s. In Section 3, we introduce the ςρ-calculus, which is a version of the ς-calculus with explicit substitutions where methods are represented with closures, and we specify it with a natural semantics that uses environments (Section 3.1); through the functional correspondence, we obtain the corresponding abstract machine (Section 3.2). Through the syntactic correspondence, we then present the reduction semantics corresponding to this abstract machine (Section 3.3). In Section 4.1, we present a mapping from ςρ-closures to ς-terms that performs the actual substitutions that were delayed by the given environments in the given terms. In Section 4.2, using this mapping, we show that the two abstract machines are bisimilar, which establishes a coherence between the three semantic artifacts for the ς-calculus and the three semantic artifacts for the ςρ-calculus. We then review related work in Section 5 and conclude in Section 6.

Prerequisites: We assume the reader to be mildly familiar with Sections 6.1 and 6.2 of Abadi and Cardelli’s monograph [1] and with the concepts of reduction semantics (BNF of terms and of reduction contexts, notion of redex, one-step reduction, evaluation as iterated reduction), of abstract machines (initial, intermediate, and final states, and state-transition functions), of natural semantics (interpreters as evaluation functions), and of bisimulation. As for the syntactic and functional correspondences, the unfamiliar reader can just flip through Danvy’s invited paper at WRS’04 [20] or through Danvy and Millikin’s recent note about small-step and big-step abstract machines [23] for what is not self-explanatory.

2 Abadi and Cardelli’s untyped calculus of objects: the ς-calculus

We consider in turn a reduction semantics for the ς-calculus (Section 2.1), the corresponding abstract machine (Section 2.2), and the corresponding natural semantics (Section 2.3).

2.1 A reduction semantics

BNF of terms and of values: An object is a collection of named attributes. Names are labels and all labels are distinct within each object. All attributes are methods with a bound variable representing self (and to be bound to the host object at invocation time) and a body whose execution yields a result.

(Term)  t ::= x | [l = ς(x)t, …, l = ς(x)t] | t.l | t.l ⇐ ς(x)t
(Value)  v ::= [l = ς(x)t, …, l = ς(x)t]

This grammar for terms defines the same language as in Abadi and Cardelli’s book but it uses a more uniform naming convention.

NB: Occasionally, we index a value by its number of methods, as in v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}].

Notion of redex: Methods can be invoked or updated [1, Definition 6.2-1 (1)]. Here is the grammar of potential redexes:

pr ::= v.l | v.l ⇐ ς(x)t

The contraction rules read as follows:

v^{n}.l_{j} ↣ t_{j}{v^{n}/x_{j}}
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}]
v^{n}.l_{j} ⇐ ς(x)t ↣ [l_{j} = ς(x)t, l_{i} = ς(x_{i})t_{i}^{i∈{1..n}\{j}}]
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}]

A potential redex is an actual one when its side conditions are satisfied, and contraction can take place. Otherwise, the potential redex is stuck.

BNF of reduction contexts: The following grammar for reduction contexts does not occur in Abadi and Cardelli’s book but it plausibly reflects the ‘evaluation strategy of the sort commonly used in programming languages’ [1, Section 6.2.4, page 63]:

(Context)  C ::= [ ] | C[[ ].l] | C[[ ].l ⇐ ς(x)t]

Lemma 1 (Unique decomposition). Any term which is not a value can be uniquely decomposed into a reduction context and a potential redex.

One is then in position to define a decomposition function mapping a term to either a value or to a reduction context and a potential redex, a contraction function mapping an actual redex to its contractum, and a plug function mapping a reduction context and a term to a term. Thus equipped, one can define a one-step reduction function (noted → below) and then an evaluation function as the iteration of the one-step reduction function (noted →^{∗} below). We have implemented and copiously tested this reduction semantics (as well as all the other semantic artifacts of this article) in Standard ML.

2.2 The corresponding abstract machine

Applying the syntactic correspondence (i.e., calculating the refocus function) yields the following eval/apply abstract machine [36]:

⟨v, C⟩ ⇒_{S} ⟨C, v⟩
⟨t.l, C⟩ ⇒_{S} ⟨t, C[[ ].l]⟩
⟨t.l ⇐ ς(x)t′, C⟩ ⇒_{S} ⟨t, C[[ ].l ⇐ ς(x)t′]⟩
⟨[ ], v ⟩ ⇒_{S} v
⟨C[[ ].l_{j}], v^{n}⟩ ⇒_{S} ⟨t_{j}{v^{n}/x_{j}}, C⟩
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}]
⟨C[[ ].l_{j} ⇐ ς(x)t], v^{n}⟩ ⇒_{S} ⟨C, [l_{j} = ς(x)t, l_{i} = ς(x_{i})t_{i}^{i∈{1..n}\{j}}]⟩
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}]

This machine evaluates a closed term t by starting in the configuration ⟨t, [ ]⟩ and by iterating ⇒_{S} (noted ⇒_{S}^{∗} below). It halts with a value v if it reaches a configuration ⟨[ ], v⟩ It becomes stuck if it reaches either of the configurations ⟨C[[ ].l], v⟩ or ⟨C[[ ].l ⇐ ς(x)t], v⟩ and v does not contain a method with the label l.

The following proposition is a corollary of the soundness of refocusing:

Proposition 1 (Full correctness). For any closed term t, t →^{∗} v if and only if ⟨t, [ ]⟩ ⇒_{S}^{∗} v.

2.3 The corresponding natural semantics

In Section 2.2, the function implementing the abstract machine is in defunctionalized form [24]. Refunctionalizing it [22] yields an evaluation function in continuation-passing style (CPS). Writing this evaluation function in direct style [19] yields an evaluation function that implements the following natural semantics:

(INV_{ς})  \frac{⊢ t ⇝ v^{n} ⊢ t_{j}\{v^{n}/x_{j}\} ⇝ v}{⊢ t.l_{j} ⇝ v}  \begin{matrix}if 1 ≤ j ≤ n, where \\ v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈\{1..n\}}] \end{matrix}

(UPD_{ς}) \frac{⊢ t ⇝ v^{n}}{⊢ t.l_{j} ⇐ ς(x)t′ ⇝ [\begin{matrix}l_{j} = ς(x)t′, \\ l_{i} = ς(x_{i})t_{i}^{i∈\{1..n\}\\{j\}}] \end{matrix}} \begin{matrix}if 1 ≤ j ≤ n, where \\ v^{n} = [l_{i} = ς(x_{i})t_{i}^{i∈\{1..n\}}] \end{matrix}

This natural semantics coincides with Abadi and Cardelli’s [1, Section 6.2.4, page 64].

The following proposition is a corollary of the soundness of the CPS transformation and of defunctionalization:

Proposition 2 (Full correctness). For any closed term t, ⟨t, [ ]⟩ ⇒_{S}^{∗} v if and only if ⊢ t ⇝ v.

2.4 Summary and conclusion

Using the syntactic correspondence and the functional correspondence, we have mechanically derived an abstract machine that mediates between Abadi and Cardelli’s reduction semantics and natural semantics for the ς-calculus and the ‘evaluation strategy of the sort commonly used in programming languages.’ The two derivations confirm (1) the soundness of the two semantics relative to each other and (2) the BNF of the reduction contexts we put forward in Section 2.1. They also pave the way to using closures, which we do next.

3 Object methods as closures: the ςρ-calculus

We consider in turn a natural semantics for the ς-calculus with environments (Section 3.1), the corresponding environment-based abstract machine (Section 3.2), and the corresponding reduction semantics (Section 3.3). The resulting calculus is one of explicit substitutions, the ςρ-calculus.

3.1 A natural semantics

Let us adapt the natural semantics of Section 2.3 to operate with environments. Three changes take place:

1. the category of values changes to objects where each method holds its own environment

(noted ‘e’):

(Value)  v ::= [l = (ς(x)t)[e], …, l = (ς(x)t)[e]]

2. the environment is defined as an association list:

(Environment)  e ::= • | (x, v) · e

and an auxiliary function lookupis used to look up an identifier in the current environment.

3. the evaluation judgment now reads as follows:

e ⊢ t ⇝ v

Again, we occasionally index a value with the number of its methods.

The two rules from Section 2.3 are then straightforwardly adapted:

(INV_{ςρ}) \frac{e ⊢ t ⇝ v^{n} (x_{j}, v^{n}) · e_{j} ⊢ t_{j} ⇝ v}{e ⊢ t.l_{j} ⇝ v} \begin{matrix}if 1 ≤ j ≤ n, where \\ v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈\{1..n\}}] \end{matrix}

(UPD_{ςρ}) \frac{e ⊢ t ⇝ v^{n}}{e ⊢ t.l_{j} ⇐ ς(x)t′ ⇝ v} if 1 ≤ j ≤ n, where

v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}] and

v = [\begin{matrix}l_{j} = (ς(x)t′)[e], \\ l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈\{1..n\}\\{j\}}] \end{matrix}

We also need the following rule to convert the methods of an object literal to method closures:

(CLO_{ςρ}) \overline{e ⊢ [l_{i} = ς(x_{i})t_{i}^{i∈\{1..n\}}] ⇝ [l_{i} = (ς(x_{i})t_{i})[e]^{i∈\{1..n\}}]}

In addition, we need the following new rule to look up variables in the current environment:

(VAR-L_{ςρ}) \overline{e ⊢ x ⇝ v}  if lookup(x, e) = v

Alternatively, and as done, e.g., in the Categorical Abstract Machine [16], one could use two rules to incrementally peel off the environment. For closed terms, x always occurs in e. For open terms, evaluation would become stuck here.

3.2 The corresponding abstract machine

To apply the functional correspondence, we successively CPS-transform and defunctionalize the evaluation function implementing the natural semantics of Section 3.1. The grammar of evaluation contexts now reads as follows:

(Context)  C ::= [ ] | C[[ ].l] | C[[ ].l ⇐ (ς(x)t)[e]]

All in all, the functional correspondence yields the following eval/apply abstract machine:

⟨x, e, C⟩ ⇒_{E} ⟨C, v⟩

if lookup(x, e) = v

⟨[l_{i} = ς(x_{i})t_{i}^{i∈{1..n}}], e, C⟩ ⇒_{E} ⟨C, [l_{i} = (ς(x_{i})t_{i})[e]^{i∈{1..n}}]⟩
⟨t.l, e, C⟩ ⇒_{E} ⟨t, e, C[[ ].l]⟩
⟨t.l ⇐ ς(x)t′, e, C⟩ ⇒_{E} ⟨t, e, C[[ ].l ⇐ (ς(x)t′)[e]]⟩
⟨[ ], v ⟩ ⇒_{E} v
⟨C[[ ].l_{j}], v^{n}⟩ ⇒_{E} ⟨t_{j}, (x_{j}, v^{n}) · e_{j}, C⟩

if 1 ≤ j ≤ n, where

v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}]

⟨C[[ ].l_{j} ⇐ (ς(x)t)[e]], v^{n}⟩ ⇒_{E} ⟨C, [l_{j} = (ς(x)t)[e], l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}\{j}}]⟩

if 1 ≤ j ≤ n, where

v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}]

This machine evaluates a closed term t by starting in the configuration ⟨t, •, [ ]⟩ and by iterating ⇒_{E} (noted ⇒_{E}^{∗} below). It halts with a value v if it reaches a configuration ⟨[ ], v⟩. It becomes stuck if it reaches either of the configurations ⟨C[[ ].l], v⟩ or ⟨C[[ ].l ⇐ (ς(x)t)[e]], v⟩ and v does not contain a method with the label l.

The following proposition is a corollary of the soundness of the CPS transformation and of defunctionalization:

Proposition 3 (Full correctness). For any closed term t, • ⊢ t ⇝ v if and only if ⟨t, •, [ ]⟩ ⇒_{E}^{∗} v.

3.3 The corresponding reduction semantics

BNF of terms, of values, and of closures: The BNF of terms does not change. The BNF of values is as in Section 3.1. In addition, as in Curien’s λρ-calculus compared to the λ-calculus, a new syntactic category appears, that of closures:

(Closure) c ::= t[e] | [l = (ς(x)t)[e], …, l = (ς(x)t)[e]] | c.l | c.l ⇐ (ς(x)t)[e]

Notion of redex: The two original contraction rules are adapted to closures as follows:

v^{n}.l_{j} ↣ t_{j}[(x_{j}, v^{n}) · e_{j}]
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}]
v^{n}.l_{j} ⇐ (ς(x)t)[e] ↣ [l_{j} = (ς(x)t)[e], l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}\{j}}]
if 1 ≤ j ≤ n, where v^{n} = [l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}]

As could be expected, there is also a contraction rule for looking variables up in the environment:

x[e] ↣ v

if lookup(x, e) = v In addition, we need three contraction rules to propagate the environment inside the terms:

\begin{matrix}[l_{i} = ς(x_{i})t_{i}^{i∈\{1..n\}}][e] & ↣ & [l_{i} = (ς(x_{i})t_{i})[e]^{i∈\{1..n\}}] \\ (t.l)[e] & ↣ & t[e].l \\ (t.l ⇐ ς(x)t′)[e] & ↣ & t[e].l ⇐ (ς(x)t′)[e] \end{matrix}

The grammar of potential redexes therefore reads as follows:

\begin{aligned}pr & ::= & v.l | v.l ⇐ (ς(x)t)[e] | \\ & & x[e] | [l = ς(x)t, …, l = ς(x)t][e] | (t.l)[e] | (t.l ⇐ ς(x)t′)[e] \end{aligned}

BNF of reduction contexts: The grammar for reduction contexts is the same as in Section 3.2.

Lemma 2 (Unique decomposition). Any closure which is not a value can be uniquely decomposed into a reduction context and a potential redex.

One is then in position to define a decomposition function mapping a closure to either a value or to a reduction context and a potential redex, a contraction function mapping an actual redex to its contractum, and a plug function mapping a reduction context and a closure to a closure. Thus equipped, one can define a one-step reduction function (noted → below) and then an evaluation function as the iteration of the one-step reduction function (noted →^{∗} below).

Applying the syntactic correspondence yields the abstract machine from Section 3.2.

The following proposition is a corollary of the soundness of refocusing:

Proposition 4 (Full correctness). For any closed term t, ⟨t, •, [ ]⟩ ⇒_{E}^{∗} v if and only if t[•] →^{∗} v.

3.4 Summary and conclusion

On the ground that practical implementations do not use actual substitutions, we have presented an analogue of the ς-calculus, the ςρ-calculus, that uses explicit substitutions. We have interderived three semantics artifacts for the ςρ-calculus: a natural semantics, an abstract machine, and a reduction semantics. These specifications are more suitable to support the formalization of a compiler since programs do not change (through substitution) in the course of execution. One is then free to change their representation, e.g., by compiling them.

On the other hand, environments open the issue of space leaks since some of their bindings may become obsolete but can only be recycled when the environment itself it recycled. In functional programming, “flat” closures [13] (or again “display” closures [26]) are used instead: closures whose environment is restricted to the free variables of the term in the closure, which can be computed at compile time. The ς-calculus, however, is too dynamic in general for free variables to be computable at compile time: they need to be computed at run time. One could thus consider another possibility: to represent environments as a lightweight dictionary where each variable only occurs once.

4 Coherence between the ς-calculus and the ςρ-calculus

We establish the coherence between the ς-calculus and the ςρ-calculus by showing that their abstract machines are bisimilar (Section 4.2). To this end, we first introduce substitution functions mapping constructs from the ςρ-calculus to the ς-calculus (Section 4.1).

4.1 From closures to terms

We define by simultaneous induction three substitution functions that respectively map ςρ-values to ς-values, ςρ method closures to ς-methods, and ςρ-terms to ς-terms:

sub_{V}([l_{i} = (ς(x_{i})t_{i})[e_{i}]^{i∈{1..n}}]) = [l_{i} = sub_{M}(ς(x_{i})t_{i}, e_{i})^{i∈{1..n}}]
sub_{M}(ς(x)t, e) = ς(x)t{sub_{V}(v_{i})/x_{i}} ∀x_{i} ∈ F V (t) \ {x},
where lookup(x_{i}, e) = v_{i}
sub_{T}(t, e) = t{sub_{V}(v_{i})/x_{i}} ∀x_{i} ∈ F V (t),
where lookup(x_{i}, e) = v_{i}

Here, we have extended the notation for substitutions to account for the simultaneous substitution of multiple values for multiple variables. F V (t) denotes the set of free variables in t, as defined by Abadi and Cardelli [1, page 61]

Let us also define a substitution function sub_{C} that maps ςρ-contexts to ς-contexts:

\begin{aligned}sub_{C}([ ]) & = & [ ] \\ sub_{C}(C[[ ].l]) & = & (sub_{C}(C))[[ ].l] \\ sub_{C}(C[[ ].l ⇐ (ς(x)t)[e]]) & = & (sub_{C}(C))[[ ].l ⇐ ς(x)sub_{M}(ς(x)t, e)] \end{aligned}

4.2 A bisimulation between the two abstract machines

Definition 1. Let ST_{ςρ} denote the set of states of the abstract machine for the ςρ-calculus, and ST_{ς} denote the set of states of the abstract machine for the ς-calculus. The substitution relation ≃_{S}: ST_{ςρ} × ST_{ς} is defined as follows:

\begin{aligned}⟨t, e, C⟩ & ≃_{S} & ⟨sub_{T}(t, e), sub_{C}(C)⟩ \\ ⟨C, v⟩ & ≃_{S} & ⟨sub_{C}(C), sub_{V}(v)⟩ \\ v & ≃_{S} & sub_{V}(v) \end{aligned}

Theorem 1. The abstract machines from Sections 2.2 and 3.2 are strongly bisimilar with respect to ≃_{S}.

Proof. By co-induction on the execution of the abstract machine for the ςρ-calculus [30].

5 Related work

The ς-calculus has already proved a fruitful playground. For example, Kesner and López [33] have defined a set of contraction rules for the ς-calculus based on explicit substitutions and flat closures. Due to the dynamic nature of the ς-calculus, and as already pointed out in Section 3.4, managing flat closures requires the evaluator to recompute sets of free variables dynamically during evaluation. In contrast, we opted for deep closures here. For another example, Gordon, Hankin and Lassen [29] have considered an imperative version of the ς-calculus extended with λ-terms. They have defined a natural semantics based on explicit substitutions for their extended calculus, and proved it equivalent to substitution-based big-step and small-step semantics. In addition, they also provided a compiler to and a decompiler from a ZINC-like virtual machine [35]. Our approach is more inter-derivational and mechanical.

6 Conclusion and issues

We have presented an abstract machine that mediates between Abadi and Cardelli’s reduction semantics and natural semantics for the ς-calculus. We have then presented a version of the ς-calculus with explicit substitutions, the ςρ-calculus, and inter-derived a natural semantics, an abstract machine, and a reduction semantics for it. By construction, each of these three semantic artifacts is sound with respect to the two others. We have also shown that the abstract machines for the ς-calculus and for the ςρ-calculus are bisimilar, thereby establishing a coherence between the ς-calculus and the ςρ-calculus.

In the conclusion of “A Syntactic Correspondence between Context-Sensitive Calculi and Abstract Machines” [11], Biernacka and Danvy listed 16 distinct, independently published specifications of the control operator call/cc, and candidly asked whether all these artifacts define the same call/cc. It is the authors’ belief that inter-deriving these artifacts using correct transformations puts one in position to answer this question.

As a side benefit, the nature of each inter-derivation makes it possible to pinpoint the specific goodness of each of the semantic artifacts. For example, a calculus in the form of a reduction semantics makes it possible to state equations to reason about programs; an abstract machine gives one some idea about the implementation requirements of a run-time system; and an interpreter in the form of a natural semantics is well suited for prototyping. We have illustrated these issues here with Abadi and Cardelli’s untyped calculus of objects.

Acknowledgments: This article was written while the first author was visiting the PPS lab at the Université Paris 7 – Denis Diderot on a ‘poste rouge’ from the CNRS, in the winter of 2007– 2008. The first author is grateful to his office mate at PPS, Paul-André Melliès, for insightful discussions and for the description of his completeness proof of the ς-calculus.

This work is partly supported by the Danish Natural Science Research Council, Grant no. 21-03-0545.

References

[1] Martín Abadi and Luca Cardelli. A Theory of Objects. Monographs in Computer Science. Springer, 1996.

[2] Martín Abadi, Luca Cardelli, Pierre-Louis Curien, and Jean-Jacques Lévy. Explicit substitutions. Journal of Functional Programming, 1(4):375–416, 1991. A preliminary version was presented at the Seventeenth Annual ACM Symposium on Principles of Programming Languages (POPL 1990).

[3] Mads Sig Ager. Partial Evaluation of String Matchers & Constructions of Abstract Machines. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, January 2006.

[4] Mads Sig Ager, Dariusz Biernacki, Olivier Danvy, and Jan Midtgaard. A functional correspondence between evaluators and abstract machines. In Dale Miller, editor, Proceedings of the Fifth ACM-SIGPLAN International Conference on Principles and Practice of Declarative Programming (PPDP’03), pages 8–19, Uppsala, Sweden, August 2003. ACM Press.

[5] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between call-by-need evaluators and lazy abstract machines. Information Processing Letters, 90(5):223– 232, 2004. Extended version available as the research report BRICS RS-04-3.

[6] Mads Sig Ager, Olivier Danvy, and Jan Midtgaard. A functional correspondence between monadic evaluators and abstract machines for languages with computational effects. Theoretical Computer Science, 342(1):149–172, 2005. Extended version available as the research report BRICS RS-04-28.

[7] Henk Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundation of Mathematics. North-Holland, revised edition, 1984.

[8] Ma�gorzata Biernacka. A Derivational Approach to the Operational Semantics of Functional Languages. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, January 2006.

[9] Ma�gorzata Biernacka, Dariusz Biernacki, and Olivier Danvy. An operational foundation for delimited continuations in the CPS hierarchy. Logical Methods in Computer Science, 1(2:5):1– 39, November 2005. A preliminary version was presented at the Fourth ACM SIGPLAN Workshop on Continuations (CW’04).

[10] Ma�gorzata Biernacka and Olivier Danvy. A concrete framework for environment machines. ACM Transactions on Computational Logic, 9(1):1–30, 2007. Article #6. Extended version available as the research report BRICS RS-06-3.

[11] Ma�gorzata Biernacka and Olivier Danvy. A syntactic correspondence between contextsensitive calculi and abstract machines. Theoretical Computer Science, 375(1-3):76–108, 2007. Extended version available as the research report BRICS RS-06-18.

[12] Dariusz Biernacki. The Theory and Practice of Programming Languages with Delimited Continuations. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, December 2005.

[13] Luca Cardelli. Compiling a functional language. In Guy L. Steele Jr., editor, Conference Record of the 1984 ACM Symposium on Lisp and Functional Programming, pages 208–217, Austin, Texas, August 1984. ACM Press.

[14] Alonzo Church. The Calculi of Lambda-Conversion. Princeton University Press, 1941.

[15] Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In Susan L. Graham, editor, Proceedings of the Twentieth Annual ACM Symposium on Principles of Programming Languages, pages 493–501, Charleston, South Carolina, January 1993. ACM Press.

[16] Guy Cousineau, Pierre-Louis Curien, and Michel Mauny. The Categorical Abstract Machine. Science of Computer Programming, 8(2):173–202, 1987.

[17] Pierre-Louis Curien. An abstract framework for environment machines. Theoretical Computer Science, 82:389–402, 1991.

[18] Pierre-Louis Curien, Thérèse Hardin, and Jean-Jacques Lévy. Confluence properties of weak and strong calculi of explicit substitutions. Journal of the ACM, 43(2):362–397, 1996.

[19] Olivier Danvy. Back to direct style. Science of Computer Programming, 22(3):183–195, 1994. A preliminary version was presented at the Fourth European Symposium on Programming (ESOP 1992).

[20] Olivier Danvy. From reduction-based to reduction-free normalization. In Sergio Antoy and Yoshihito Toyama, editors, Proceedings of the Fourth International Workshop on Reduction Strategies in Rewriting and Programming (WRS’04), volume 124(2) of Electronic Notes in Theoretical Computer Science, pages 79–100, Aachen, Germany, May 2004. Elsevier Science. Invited talk.

[21] Olivier Danvy. An Analytical Approach to Program as Data Objects. DSc thesis, Department of Computer Science, University of Aarhus, Aarhus, Denmark, October 2006.

[22] Olivier Danvy and Kevin Millikin. Refunctionalization at work. Science of Computer Programming, 200? In press. A preliminary version is available as the research report BRICS RS-07-7.

[23] Olivier Danvy and Kevin Millikin. On the equivalence between small-step and big-step abstract machines: a simple application of lightweight fusion. Information Processing Letters, 106(3):100–109, 2008.

[24] Olivier Danvy and Lasse R. Nielsen. Defunctionalization at work. In Harald Søndergaard, editor, Proceedings of the Third International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP’01), pages 162–174, Firenze, Italy, September 2001. ACM Press. Extended version available as the research report BRICS RS-01-23.

[25] Olivier Danvy and Lasse R. Nielsen. Refocusing in reduction semantics. Research Report BRICS RS-04-26, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, November 2004. A preliminary version appeared in the informal proceedings of the Second International Workshop on Rule-Based Programming (RULE 2001), Electronic Notes in Theoretical Computer Science, Vol. 59.4.

[26] R. Kent Dybvig. The development of Chez Scheme. In Julia L. Lawall, editor, Proceedings of the 2006 ACM SIGPLAN International Conference on Functional Programming (ICFP’06), SIG-PLAN Notices, Vol. 41, No. 9, pages 1–12, Portland, Oregon, September 2006. ACM Press. Keynote talk.

[27] Matthias Felleisen. The Calculi of λ-v-CS Conversion: A Syntactic Theory of Control and State in Imperative Higher-Order Programming Languages. PhD thesis, Computer Science Department, Indiana University, Bloomington, Indiana, August 1987.

[28] Matthias Felleisen and Matthew Flatt. Programming languages and lambda calculi. Unpub-

lished lecture notes available at <http://www.ccs.neu.edu/home/matthias/3810-w02/readings.

html> and last accessed in April 2008, 1989-2001.

[29] Andrew D. Gordon, Paul D. Hankin, and Søren B. Lassen. Compilation and equivalence of imperative objects. Journal of Functional Programming, 9(4):373–426, 1999. Extended version available as the technical report BRICS RS-97-19.

[30] Jacob Johannsen. An investigation of Abadi and Cardelli’s untyped calculus of objects. Master’s thesis, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, June 2008.

[31] Neil D. Jones, Carsten K. Gomard, and Peter Sestoft. Partial Evaluation and Automatic Program Generation. Prentice-Hall International, London, UK, 1993. Available online at <http://www.

dina.kvl.dk/\homedirsestoft/pebook/>.

[32] Gilles Kahn. Natural semantics. In Franz-Josef Brandenburg, Guy Vidal-Naquet, and Martin Wirsing, editors, Proceedings of the 4th Annual Symposium on Theoretical Aspects of Computer Science, number 247 in Lecture Notes in Computer Science, pages 22–39, Passau, Germany, February 1987. Springer-Verlag.

[33] Delia Kesner and Pablo E. Martínez López. Explicit substitutions for objects and functions. Journal of Functional and Logic Programming, Special issue 2, 1999. A preliminary version was presented at PLILP’98/ALP’98.

[34] Peter J. Landin. The mechanical evaluation of expressions. The Computer Journal, 6(4):308– 320, 1964.

[35] Xavier Leroy. The Zinc experiment: an economical implementation of the ML language. Rapport Technique 117, INRIA Rocquencourt, Le Chesnay, France, February 1990.

[36] Simon Marlow and Simon L. Peyton Jones. Making a fast curry: push/enter vs. eval/apply for higher-order languages. In Kathleen Fisher, editor, Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP’04), SIGPLAN Notices, Vol. 39, No. 9, pages 4–15, Snowbird, Utah, September 2004. ACM Press.

[37] Jan Midtgaard. Transformation, Analysis, and Interpretation of Higher-Order Procedural Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, June 2007.

[38] Kevin Millikin. A Structured Approach to the Transformation, Normalization and Execution of Computer Programs. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, May 2007.

[39] Lasse R. Nielsen. A study of defunctionalization and continuation-passing style. PhD thesis, BRICS PhD School, University of Aarhus, Aarhus, Denmark, July 2001. BRICS DS-01-7.

[40] Hanne Riis Nielson and Flemming Nielson. Semantics with Applications, a formal introduction. Wiley Professional Computing. John Wiley and Sons, 1992.

[41] John C. Reynolds. Definitional interpreters for higher-order programming languages. In Proceedings of 25th ACM National Conference, pages 717–740, Boston, Massachusetts, 1972. Reprinted in Higher-Order and Symbolic Computation 11(4):363–397, 1998, with a foreword [42].

[42] John C. Reynolds. Definitional interpreters revisited. Higher-Order and Symbolic Computation, 11(4):355–361, 1998.

[43] Kristoffer H. Rose. Explicit substitution – tutorial & survey. BRICS Lecture Series LS-96-3, DAIMI, Department of Computer Science, University of Aarhus, Aarhus, Denmark, September 1996.

Recent BRICS Report Series Publications

RS-08-5 Olivier Danvy and Jacob Johannsen. Inter-Deriving Semantic Artifacts for Object-Oriented Programming. June 2008. ii+13 pp. Extended version of a paper to appear in WoLLIC 2008.

RS-08-4 Olivier Danvy and Kevin Millikin. Refunctionalization at Work. June 2008. ii+25 pp. To appear in Science of Computer Programming. A preliminary version is available as the research report BRICS RS-07-7.

RS-08-3 Johan Munk. A Study of Syntactic and Semantic Artifacts and its Application to Lambda Definability, Strong Normalization, and Weak Normalization in the Presence of State. April 2008. xi+144 pp.

RS-08-2 Gudmund Skovbjerg Frandsen and Piotr Sankowski. Dynamic Normal Forms and Dynamic Characteristic Polynomial. April 2008. 21 pp. To appear in ICALP ’08.

RS-08-1 Anders Møller. Static Analysis for Event-Based XML Processing. jan 2008. 23 pp. Appears in PLAN-X ’08.

RS-07-18 Jan Midtgaard. Control-Flow Analysis of Functional Programs. December 2007. iii+38 pp.

RS-07-17 Luca Aceto, Willem Jan Fokkink, and Anna Ingólfsdóttir. A Cancellation Theorem for 7BCCSP. December 2007. 30 pp.

RS-07-16 Olivier Danvy and Kevin Millikin. On the Equivalence between Small-Step and Big-Step Abstract Machines: A Simple Application of Lightweight Fusion. November 2007. ii+11 pp. To appear in Information Processing Letters (extended version). Supersedes BRICS RS-07-8.

RS-07-15 Jooyong Lee. A Case for Dynamic Reverse-code Generation. August 2007. ii+10 pp.

RS-07-14 Olivier Danvy and Michael Spivey. On Barron and Strachey’s Cartesian Product Function. July 2007. ii+14 pp.

RS-07-13 Martin Lange. Temporal Logics Beyond Regularity. July 2007. 82 pp.

RS-07-12 Gerth Stølting Brodal, Rolf Fagerberg, Allan Grønlund Jørgensen, Gabriel Moruz, and Thomas Mølhave. Optimal Resilient Dynamic Dictionaries. July 2007.