The VLISP Flattener

J. D. Guttman  L. G. Monk  J. D. Ramsdell
W. M. Farmer  V. Swarup

The MITRE Corporation^{∗} M92B094 September 1992

∗Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. \begin{matrix}c \\ ◯ \end{matrix}1992 The MITRE Corporation. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the MITRE copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of the MITRE Corporation.

Abstract

The Verified Programming Language Implementation project has developed a formally verified implementation of the Scheme programming language. This report documents the flattener, which linearizes a tree-structured byte-code. It contains detailed proofs that the operational semantics of the flattened output matches the operational semantics of the input.

Contents

1 Introduction 1 1.1 Notation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 1

2 State Transition Machines in General 3

3 Tabular Byte Code State Machines 5 3.1 Tabular Byte Code . . . . . . . . . . . . . . . . . . . . . . . . 5 3.2 The Augmented Byte Code Language . . . . . . . . . . . . . 7 3.3 States and Actions . . . . . . . . . . . . . . . . . . . . . . . . 8

3.3.1 Auxiliary Functions . . . . . . . . . . . . . . . . . . . 9 3.3.2 Presentation Format for Pure Rules . . . . . . . . . . 10 3.3.3 Return-like Rules . . . . . . . . . . . . . . . . . . . . . 11 3.3.4 Branch Rules . . . . . . . . . . . . . . . . . . . . . . . 13 3.3.5 Other Basic Rules . . . . . . . . . . . . . . . . . . . . 14 3.3.6 Primitive Operation Rules . . . . . . . . . . . . . . . . 17

4 Flattened Byte Code State Machines 21 4.1 Syntax of the Flattened Byte Code Language . . . . . . . . . 21 4.2 The Augmented Flattened Byte Code Language . . . . . . . 22 4.3 States and Actions . . . . . . . . . . . . . . . . . . . . . . . . 22

4.3.1 Return-like Rules . . . . . . . . . . . . . . . . . . . . . 23 4.3.2 Jump-like Rules . . . . . . . . . . . . . . . . . . . . . 25 4.3.3 Other Basic Rules . . . . . . . . . . . . . . . . . . . . 26 4.3.4 Primitive Operation Rules . . . . . . . . . . . . . . . . 29

5 The Flattener Algorithm 33 5.1 The Flattener Proper . . . . . . . . . . . . . . . . . . . . . . 33 5.2 Auxiliary Procedures . . . . . . . . . . . . . . . . . . . . . . . 34 5.3 The Code Sequence Data Type . . . . . . . . . . . . . . . . . 35

6 Establishing Correspondence of Code 37

7 Preservation of State Correspondence 45

8 Correctness of the Flattener 54

References 56

1 Introduction

The primary purpose of this paper is to present and justify the vlisp passage from tree-structured code to code which is essentially linear, using an operational semantics. As the flattener is a convenient mid-point in the overall vlisp program [2], this paper also serves as a reference, giving some official definitions for other parts of the program. Specifically, this paper presents:

(1) the vlisp approach to operational semantics via state machines,

(2) the syntax and operational semantics for the vlisp Tabular Byte Code (tbc),

(3) the syntax and operational semantics for the vlisp Flattened Byte Code (fbc),

(4) the flattener algorithm for passing from tbc programs to fbc programs, and

(5) an extension of the flattener to a map from initial tbc states to initial fbc states that produce the same answers, with a proof of this fact.

We define (tabular) byte code state machines and flattened byte code state machines below as kinds of deterministic state transition machines with concrete states, in accordance with a general formalism for state machines and their computations. This formalism allows for programs to result in answers, as in the denotational semantics, and also for a later, more refined view of programs as operators that take input streams to output streams. The byte code machines’ states are vectors of syntactic objects of expediently augmented languages that are formed from the tabular byte code and the flattened byte code by adding syntactic constructors for terms for environments, closures, continuations, etc. Each of the various kinds of state transitions is motivated by a possible combination of equational reductions in the denotational semantics of the underlying byte code.

1.1 Notation

We identify natural numbers with finite von Neumann ordinals, so that each natural number is actually the set of all smaller natural numbers. A finite sequence is a function with a natural number as its domain, which is the same as its length. Thus, in our usage, when s is a finite sequence, s(2) is the third element of s, if s has length at least three, and is undefined if the length of s is strictly less than three. We use angle brackets to indicate sequence formation, with spaces (and sometimes, for clarity, commas) separating elements, and reserve ordinary parentheses for various other traditional uses.

Asterisk is usually used as an operator for finite sequence formation, thus X^{∗} means the set of all finite sequences from X, but asterisks are also sometimes just used as mnemonics in variable names for variables that range over sets of finite sequences.

In contrast to some uses of bnf, there is no implicit concatenation of finite sequence terms inside angle brackets; for instance, every element of ⟨A B^{∗} C^{∗}⟩, which means the same as ⟨A, B^{∗}, C^{∗}⟩, is a sequence of length exactly three.

We will also use the following notation:

#s  the length of sequence s
s^{⌢}t  the concatenation of sequences s and t
x:: s  ⟨x⟩^{⌢}s (“mathematical cons”)
s † k  the result of dropping the first k members from sequence s
s ‡ k  the sequence of only the first k members of s
a → b, c if a then b else c

2 State Transition Machines in General

We choose one convenient way of pinning down details among many which would suffice. First we define (possibly non-deterministic) state transition machines, these are septuples

⟨states, halt states, inputs, null-input, outputs, null-output, actions⟩,

such that

(a) states, inputs, and outputs are disjoint sets with halt states ⊆ states, null-input ∈ inputs, and null-output ∈ outputs,

(b) actions ⊆ (states × inputs) × (states × outputs), and

(c) For no pair ⟨s, i⟩ in the domain of actions is s ∈ halt states.

Given such a machine M, let C be a non-empty, finite or infinite sequence of elements of states × inputs × outputs. Then C_{S} (the state history), C_{I} (the input history), and C_{O} (the output history), of C are, respectively, the derived sequences of states, inputs, and outputs components of C. C is a computation if C_{O}(0) = null-output, and, for every i such that C(i + 1) is defined,

⟨⟨C_{S}(i), C_{I}(i)⟩, ⟨C_{S}(i + 1), C_{O}(i + 1)⟩⟩ ∈ actions.

We think of a transition according to an action as taking a pair of a current state and a current input and producing a next state and a next output; the initial output should be null.

Call a state-input pair proceedable if it is in the domain of actions. A computation is maximal if it is infinite or its last state and last input comprise a non-proceedable pair. A finite, maximal computation is successful if its last state is in halt states; other finite, maximal computations are erroneous. We also call a state-input pair erroneous if it is not proceedable, but the state is not in halt states; thus a computation C is erroneous if and only if, for some i, ⟨C_{S}(i), C_{I}(i)⟩ is erroneous. We allow for the possibility that some states are erroneous when paired with some inputs and not with others.

A computation is inputless if every element of its input history is null; it is outputless if every element of its output history is null; it is pure if it is both inputless and outputless. The output of a computation is the sequence of non-null elements of its output history. The input history and output history of a computation are not to be thought of as identical to the input stream and output stream. The connection depends on the run-time behavior of the program and requires definition by recursion on computations, using the additional notions of read and write operations. If actions is actually a function, then the machine is deterministic.

3 Tabular Byte Code State Machines

This section presents first the syntax of the Tabular Byte Code and an expansion of the Tabular Byte Code called the Augmented Byte Code. The Augmented Byte Code is then used to define the states of Tabular Byte Code State Machines. Finally, the action relation of these machines is presented as a union of subfunctions called rules. We may also call them abc rules, or even tbc rules, to distinguish from the rules for the flattened code, to be defined later.

3.1 Tabular Byte Code

The Tabular Byte Code (or tbc) provides crude tables (just sequences of entries) that allow the code in templates to refer to constants, global variables (identifiers), and other templates indirectly by indexing. Otherwise it is almost exactly the same as the bbc described in the accompanying Vlisp report on the Byte Code Compiler [1].

The tokens of the tbc are the same as those of the bbc, with the addition of constant, and global-variable, and with lap being replaced by template. We adapt and extend the variable conventions of bbc. Thus z stands here for a (tbc) neutral instruction (or the class of neutral instructions), and so on for all of the tbc syntactic classes, including two new classes: d is used for (tbc) table entries (or template literals), and e for (tbc) template tables. The defining productions (given in Table 1) are very similar to the ones given for bbc, but note that:

• in a template, the block now precedes an important table, instead of following an unimportant constant, and

   • literal, closure, global, and set-global! take integer arguments

here.

We will use n-like variables for natural numbers, i-like variables for identifiers, and c-like variables for constants. Similarly for the classes defined by the grammar, with

z for (tbc) neutral instructions,

m for (tbc) (machine) instructions,

b for (tbc) closed instruction lists (conjecturally < Eng. block),

y for (tbc) open instruction lists,

z ::= ⟨unless-false y_{1} y_{2}⟩
    | ⟨literal n⟩ | ⟨closure n⟩
    | ⟨global n⟩ | ⟨local n_{1} n_{2}⟩
    | ⟨set-global! n⟩ | ⟨set-local! n_{1} n_{2}⟩
    | ⟨push⟩ | ⟨make-env n⟩
    | ⟨make-rest-list n⟩ | ⟨unspecified⟩
    | ⟨checkargs= n⟩ | ⟨checkargs>= n⟩

| ⟨i⟩

m ::= z | ⟨return⟩ | ⟨call n⟩ | ⟨unless-false b_{1} b_{2}⟩
    | ⟨make-cont w_{1} n⟩

b ::= ⟨⟨return⟩⟩ | ⟨⟨call n⟩⟩ | ⟨⟨unless-false b_{1} b_{2}⟩⟩

| ⟨make-cont b_{1} n⟩:: b_{2} | z:: b_{1} y ::= ⟨make-cont y_{1} n⟩:: b | ⟨make-cont ⟨⟩ n⟩:: b | z:: y_{1} | ⟨z⟩ w ::= b | y

d ::= ⟨constant c⟩ | ⟨global-variable i⟩ | t

e ::= d^{∗}

t ::= ⟨template b e⟩

Table 1: Grammar for the Tabular Byte Code

w for (tbc) (general) instruction lists, d for (tbc) template literals, e for (tbc) template literal tables, and t for (tbc) templates.

In the flattener algorithm, we treat open and closed instruction lists differently. In particular, in an unless-false with open instruction lists y_{1} and y_{2}, the flattener must insert an unconditional jump at the end of the true branch, while this would be redundant in the case of an unless-false with closed instruction lists. Instructions of the form ⟨i⟩ are used only for “primop” identifiers (like %%cons) associated with a small set of denotationally specified Scheme primitives.

Given an open instruction list y and any instruction list w, we will sometimes need to refer to their open-adjoin, written y^{⌣}w and defined as follows:

⟨z⟩^{⌣}w = z:: w;
(z:: y)^{⌣}w = z:: (y^{⌣}w);

(⟨make-cont y n⟩:: b)^{⌣}w = ⟨make-cont y^{⌣}w n⟩:: b; and
(⟨make-cont ⟨⟩ n⟩:: b)^{⌣}w = ⟨make-cont w n⟩:: b.

It may help to note, first, that a closed instruction list can contain no instruction of the form ⟨make-cont y n⟩ or ⟨make-cont ⟨⟩ n⟩, and, hence, that an open instruction list is either a list of neutral instructions or contains exactly one instruction of this form. Open-adjoin proceeds recursively inwards from its first argument through the code lists of such instructions until it reaches one which is just a (possibly empty) list of neutral instructions and then it concatenates w to the “open” end of that list.

Lemma 1 Properties of open-adjoin. For all y, w, y_{1}, and b,

(1) y^{⌣}w is well-defined by the above recursion and is an instruction list;

(2) y^{⌣}y_{1} is open, and y^{⌣}b is closed; and

(3) y^{⌣}(y_{1}^{⌣}w) = (y^{⌣}y_{1})^{⌣}w (associativity).

Proof. Observe first that the four expressions used to define productions of open instruction lists define injective functions (of the variables occurring in them) with disjoint ranges, so the definition of y^{⌣}w is a legitimate recursion on y. The rest of (1) and (2) follow by easy inductions on y. With these established, (3) follows by induction on y, with an inner induction on y_{1}. QED.

3.2 The Augmented Byte Code Language

The Augmented Byte Code (abc) provides the syntactic objects that are the components of the state of the byte code state machine. It is formed by expanding the Tabular Byte Code defined above to allow terms for environments, closures, continuations, etc. As we will eventually use the byte code state machine, these constructors do not occur in the code coming from Scheme programs that it runs, but are put in its initial store or are generated in the course of its computation.

The new abc tokens are locations (which are actually the same as natural numbers, but which for clarity we indicate by l-like variables when used as locations) and the following constructors: closure, escape, mutable-pair, vector, string, undefined, not-specified, empty-env, env, halt, and cont.

The new abc syntactic categories to be defined by bnf are

v for (abc) values,

a for (abc) argument stacks u for (abc) environments, k for (abc) continuations, and s for (abc) stores.

All of the categories (templates, blocks etc.) and productions given for tbc are included here, but the extensions of the syntax we are making here do not feed back into the recursive construction of the old categories, so their extensions in the abc are exactly the same as in the tbc. The new productions are

v ::= c | ⟨closure t u l⟩ | ⟨escape k l⟩

| ⟨mutable-pair l_{1} l_{2}⟩ | ⟨string l^{∗}⟩ | ⟨vector l^{∗}⟩ | not-specified | undefined

a ::= v^{∗}

u ::= empty-env | ⟨env u l^{∗}⟩
k ::= halt | ⟨cont t b a u k⟩
s ::= v^{∗}

3.3 States and Actions

The states of a byte code state machine are the sequences of the form

⟨t, b, v, a, u, k, s⟩,

with the abuse of notation that b is allowed to be ⟨⟩. The components of a state are called, in order, its template, code, value, argument stack, environment, continuation, and store, and we may informally speak of them as being held in registers. The halt states are the states such that b = ⟨⟩.

The rules depend on a parameter, called globals, which can be thought of as a kind of environment, ultimately to be built by the compiler; officially it is a function from some finite set of identifiers into locations. An alternative would be to make globals a slightly less concrete component of the machine state that is not changed by any action.

We present actions as the union of subfunctions called (action) rules. The action rules are functions from disjoint subsets of states × inputs into states × outputs. A rule is pure if all pairs in its domain have input equal to null-input, and all pairs in its range have output equal to null-output; other rules are called port rules. We will only specify pure rules at this level of vlisp, and some correctness assertions assume that all state transitions are according to one of the rules explicitly specified here.

3.3.1 Auxiliary Functions

As # yields the length of a list, given any abc store s, #s is the domain of s and is also the least l such that s(l) is not defined. s^{⌢}x is another store if x is a sequence of values. Also, s + {l ↦ v} means the function whose domain is #s ∪ {l} and which takes on the value v at l; this is a store if and only if l ≤ #s; it may or may not be compatible with s.

The ternary function env-reference is defined recursively for some triples of an abc environment and two natural numbers by

1. env-reference (⟨env u l^{∗}⟩, 0, n_{1} + 1) = l^{∗}(n_{1}), and

2. env-reference (⟨env u l^{∗}⟩, n_{0} + 1, n_{1}) = env-reference (u, n_{0}, n_{1})

One might say that env-reference is 1-based in its last argument. Note that env-reference (empty-env, n_{0}, n_{1}) is never defined.

To build increasingly complex abc environment terms, the ternary function add-layer is useful. For n_{1} > 0,

add-layer(u, n_{0}, n_{1}) = ⟨env u ⟨n_{0} … (n_{0}+n_{1}−1)⟩⟩,

and add-layer(u, n_{0}, 0) = ⟨env u ⟨⟩⟩.

For make-rest-list we need two functions: mrl-value and mrl-store. Both take four arguments: a natural number, a value, an argument stack, and a store; both assume that their first argument is at most the length of their third argument; and both are defined by similar recursions:

mrl-value (0, v, a, s) = v, and mrl-value (n + 1, v, a, s) =

mrl-value (n, ⟨mutable-pair #s (#s + 1)⟩, a † 1, s^{⌢}⟨a(0), v⟩).

mrl-store (0, v, a, s) = s, and mrl-store (n + 1, v, a, s) =

mrl-store (n, ⟨mutable-pair #s (#s + 1)⟩, a † 1, s^{⌢}⟨a(0), v⟩).

Note that mrl-value (n, v, a, s) does not really depend on anything about a and s other than their lengths, that is, there is a function mrl-value′ such that, for all n, v, a, and s,

mrl-value (n, v, a, s) = mrl-value′ (n, v, #a, #s).

We will also need a function app-stack for constructing a list of arguments for %%apply. The arguments to app-stack are a value, an argument stack, and a store. It uses the stack in the same “reverse” order as the compiler does when it pushes arguments when constructing calls. This is the first time we have needed a function that actually must look inside Scheme constants – it needs to know about immutable-pair, as well as about the Scheme constant null. The recursive definition has three cases:

app-stack (null, a, s) = a,

app-stack (⟨mutable-pair l_{1} l_{2}⟩, a, s) =

app-stack (s(l_{2}), s(l_{1}) :: a, s), and app-stack (⟨immutable-pair v_{1} v_{2}⟩, a, s) =

app-stack (v_{2}, v_{1} :: a, s).

The Primitive ADD rule allows an argument stack to have arbitrarily many arguments, including none. For it we use the auxiliary function n-ary-sum, which is defined at an argument a if and only if a is a list of numbers, in which case its value is just the sum of all elements of a.

3.3.2 Presentation Format for Pure Rules

For each pure rule we give a name, one or more conditions determining when the rule is applicable (and possibly introducing new locally bound variables for later use), and a specification of the new values of some registers. Often the domain is specified by equations giving “the form” of certain registers, especially the code. In all specifications the original values of the various registers are designated by conventional variables used exactly as in the above definition of a state: t, b, v, a, u, k, and s. Call these the original register variables. The new values of the registers are indicated by the same variables with primes attached: t′, b′, v′, a′, u′, k′, and s′. Call these the new register variables. New register variables occur only as the left hand sides of equations specifiying new register values. Registers for which no new value is given are tacitly asserted to remain unchanged. Additionally, we use e for t(2); thus e must always be a template table no matter what the original state is, just because it is a valid state. Input and output must both be null.

It may help to be more precise about the use of local bindings derived from pattern matching. The domain conditions may involve the original register variables and may introduce new variables (other than e and not among the new or old register variables). If we call these new, “auxiliary” variables x_{1}, …, x_{j}, then the domain conditions define a relation of j + 7 places

(†) R(t, b, v, a, u, k, s, x_{1}, …, x_{j}).

The domain condition really is this: the rule can be applied in a given state if there exist x_{1}, …, x_{j} such that (†). Furthermore, in the change specifications we assume for these auxiliary variables a local binding such that (†). Independence of the new values on the exact choice (if there is any choice) of the local bindings will be unproblematic.

3.3.3 Return-like Rules

Rule 1: Return-Halt Domain conditions:

   b = ⟨⟨return⟩⟩

k = halt Changes:

b′ = ⟨⟩

Rule 2: Return Domain conditions:

   b = ⟨⟨return⟩⟩

k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ Changes:

t′ = t_{1}

b′ = b_{1}

a′ = a_{1}

u′ = u_{1}

k′ = k_{1} Rule 3: Call Domain conditions:

b = ⟨⟨call #a⟩⟩ v = ⟨closure t_{1} u_{1} l_{1}⟩ t_{1} = ⟨template b_{1} e_{1}⟩

Changes:

t′ = t_{1} b′ = b_{1} u′ = u_{1}

Rule 4: Escape-Halt Domain conditions:

b = ⟨⟨call 1⟩⟩ v = ⟨escape halt l⟩

Changes:

b′ = ⟨⟩

Rule 5: Escape Domain conditions:

b = ⟨⟨call 1⟩⟩ v = ⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l⟩ a = ⟨v_{1}⟩

Changes:

t′ = t_{1} b′ = b_{1} v′ = v_{1} a′ = a_{1} u′ = u_{1} k′ = k_{1} 3.3.4 Branch Rules

Rule 6: Closed Branch/True Domain conditions:

   b = ⟨⟨unless-false b_{1} b_{2}⟩⟩

v ≠ false Changes:

b′ = b_{1}

Rule 7: Closed Branch/False Domain conditions:

   b = ⟨⟨unless-false b_{1} b_{2}⟩⟩

v = false Changes:

b′ = b_{2}

Rule 8: Open Branch/True Domain conditions:

   b = ⟨unless-false y_{1} y_{2}⟩:: b_{1}

v ≠ false Changes:

b′ = y_{1}^{⌣}b_{1}

Rule 9: Open Branch/False Domain conditions:

   b = ⟨unless-false y_{1} y_{2}⟩:: b_{1}

v = false Changes:

3.3.5 Other Basic Rules

b′ = y_{2}^{⌣}b_{1} Rule 10: Make Continuation Domain conditions:

b = ⟨make-cont b_{1} #a⟩:: b_{2} Changes:

b′ = b_{2} a′ = ⟨⟩ k′ = ⟨cont t b_{1} a u k⟩

Rule 11: Literal Domain conditions:

b = ⟨literal n⟩:: b_{1}

e(n) = ⟨constant c⟩

Changes:

b′ = b_{1} v′ = c

Rule 12: Closure Domain conditions:

b = ⟨closure n⟩:: b_{1} e(n) = ⟨template b_{2} e_{2}⟩

Changes:

b′ = b_{1} v′ = ⟨closure e(n) u #s⟩ s′ = s^{⌢}⟨not-specified⟩

Rule 13: Global Domain conditions:

b = ⟨global n⟩:: b_{1}

e(n) = ⟨global-variable i⟩

globals(i) = l v_{1} = s(l) v_{1} ≠ undefined

Changes:

b′ = b_{1} v′ = v_{1} Rule 14: Set Global Domain conditions:

b = ⟨set-global! n⟩:: b_{1}
e(n) = ⟨global-variable i⟩

l = globals(i) l ≤ #s

Changes:

b′ = b_{1} v′ = not-specified s′ = s + {l ↦ v}

Rule 15: Local Domain conditions:

b = ⟨local n_{1} n_{2}⟩:: b_{1} l = env-reference(u, n_{1}, n_{2}) v_{1} = s(l) v_{1} ≠ undefined

Changes:

b′ = b_{1} v′ = v_{1}

Rule 16: Set Local Domain conditions:

b = ⟨set-local! n_{1} n_{2}⟩:: b_{1} l = env-reference(u, n_{1}, n_{2}) l ≤ #s

Changes:

b′ = b_{1} v′ = not-specified s′ = s + {l ↦ v}

Rule 17: Push Domain Conditions:

b = ⟨push⟩:: b_{1} Changes:

b′ = b_{1} a′ = v:: a Rule 18: Make Environment Domain Conditions:

b = ⟨make-env #a⟩:: b_{1} Changes:

b′ = b_{1} a′ = ⟨⟩ u′ = add-layer(u, #s, #a) s′ = s^{⌢}a

Rule 19: Make Rest List Domain Conditions:

b = ⟨make-rest-list n_{1}⟩:: b_{1}

n_{1} + n_{2} = #a Changes:

b′ = b_{1} v′ = mrl-value (n_{2}, null, a, s) a′ = a † n_{2} s′ = mrl-store (n_{2}, null, a, s)

Rule 20: Unspecified Domain Conditions:

b = ⟨unspecified⟩:: b_{1}

Changes:

b′ = b_{1} v′ = not-specified

Rule 21: Check Args = Domain Conditions:

b = ⟨checkargs= n⟩:: b_{1}

#a = n Changes:

b′ = b_{1}

Rule 22: Check Args >= Domain Conditions:

b = ⟨checkargs>= n⟩:: b_{1}

#a ≥ n Changes:

3.3.6 Primitive Operation Rules

b′ = b_{1} Rule 23: Primitive CWCC Domain Conditions:

b = ⟨%%cwcc⟩:: b_{1} a = ⟨v_{1}⟩ v_{1} = ⟨closure t_{1} u_{1} l_{1}⟩

Changes:

t′ = t_{1} b′ = t_{1}(1) v′ = v_{1} a′ = ⟨⟨escape k #s⟩⟩ u′ = u_{1} s′ = s^{⌢}⟨not-specified⟩

Rule 24: Primitive CWCC-Escape Domain Conditions:

b = ⟨%%cwcc⟩:: b_{0} a = ⟨⟨escape ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩⟩

Changes:

t′ = t_{1} b′ = b_{1} v′ = ⟨escape k #s⟩ a′ = a_{1} u′ = u_{1} k′ = k_{1} s′ = s^{⌢}⟨not-specified⟩

Rule 25: Primitive CWCC-Escape-Halt Domain Conditions:

b = ⟨%%cwcc⟩:: b_{1} a = ⟨⟨escape halt l⟩⟩

Changes:

b′ = ⟨⟩ v′ = ⟨escape k #s⟩ Rule 26: Primitive Cons Domain Conditions:

b = ⟨%%cons⟩:: b_{1} a = ⟨v_{1} v_{2}⟩^{⌢}a_{1}

Changes:

b′ = b_{1} v′ = ⟨mutable-pair #s (1 + #s)⟩ a′ = ⟨⟩ s′ = s^{⌢}⟨v_{2} v_{1}⟩

Rule 27: Primitive Car-Immutable Pair Domain Conditions:

b = ⟨%%car⟩:: b_{1}

a = ⟨immutable-pair c_{1} c_{2}⟩:: a_{1}

Changes:

b′ = b_{1} v′ = c_{1} a′ = ⟨⟩

Rule 28: Primitive Car-Mutable Pair Domain Conditions:

b = ⟨%%car⟩:: b_{1} a = ⟨mutable-pair l_{1} l_{2}⟩:: a_{1} v_{1} = s(l_{1})

Changes:

b′ = b_{1} v′ = v_{1} a′ = ⟨⟩

Rule 29: Primitive Set-Car! Domain Conditions:

b = ⟨%%set-car!⟩:: b_{1}

a = ⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1} l_{1} < #s

Changes:

b′ = b_{1} v′ = not-specified a′ = ⟨⟩ s′ = s + {l_{1} ↦ v_{1}} Rule 30: Primitive Apply-Closure Domain Conditions:

b = ⟨%%apply⟩:: b_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨closure t_{1} u_{1} l_{1}⟩ t_{1} = ⟨template b_{2} e_{2}⟩ a_{2} = app-stack (v_{1}, a_{1}, s)

Changes:

t′ = t_{1} b′ = b_{2} v′ = v_{2} a′ = a_{2} u′ = u_{1}

Rule 31: Primitive Apply-Escape Domain Conditions:

b = ⟨%%apply⟩:: b_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨escape k_{1} l_{1}⟩ k_{1} = ⟨cont t_{2} b_{2} a_{2} u_{2} k_{2}⟩ ⟨v_{3}⟩ = app-stack (v_{1}, a_{1}, s)

Changes:

t′ = t_{2} b′ = b_{2} v′ = v_{3} a′ = a_{2} u′ = u_{2} k′ = k_{2}

Rule 32: Primitive Apply-Escape-Halt Domain Conditions:

b = ⟨%%apply⟩:: b_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨escape halt l_{1}⟩

Changes:

b′ = ⟨⟩ v′ = v_{2} Rule 33: Primitive Eqv Domain Conditions:

b = ⟨%%eqv⟩:: b_{1} a = ⟨v_{1} v_{2}⟩^{⌢}a_{1}

Changes:

b′ = b_{1} v′ = ((v_{1} = v_{2}) → true, false) a′ = ⟨⟩

Rule 34: Primitive Add Domain Conditions:

b = ⟨%%add⟩:: b_{1} m = n-ary-sum (a)

Changes:

b′ = b_{1} v′ = m a′ = ⟨⟩

4 Flattened Byte Code State Machines

The purpose of this section is to present the fbc and give it an (operational) semantics in a style very similar to the presentation above of the operational semantics of the tbc.

4.1 Syntax of the Flattened Byte Code Language

The Flattened Byte Code (fbc) is a modification of the Tabular Byte Code that uses exclusively unnested linear sequences of tokens for the code part of its templates. Instead of the tbc conditional instruction unless-false, fbc has jumpf and jump, both of which take a pair of numeric operands that together indicate an offset to another location in the instruction sequence. The syntax of make-cont has been altered so that it too can use numeric offsets.

Conventional base variables for the fbc syntactic classes to be defined by bnf are:

t for (fbc) templates, e for (fbc) tables, o for (fbc) table entries (or template literals), m for (fbc) instructions (an operator with its operands), and w for (fbc) code sequences (concatenations of instructions).

The bnf definitions of these classes follows.

 t ::= ⟨template w e⟩

e ::= o∗

 o ::= ⟨constant c⟩ | ⟨global-variable i⟩ | t

w ::= ⟨⟩ | m^{⌢}w

m ::= ⟨call n⟩ | ⟨return⟩ | ⟨make-cont n_{0} n_{1} n_{2}⟩ | ⟨literal n⟩
    | ⟨closure n⟩ | ⟨global n⟩ | ⟨local n_{0} n_{1}⟩ | ⟨set-global! n⟩
    | ⟨set-local! n_{0} n_{1}⟩ | ⟨push⟩ | ⟨make-env n⟩ | ⟨make-rest-list n⟩
    | ⟨unspecified⟩ | ⟨jump n_{0} n_{1}⟩ | ⟨jumpf n_{0} n_{1}⟩
    | ⟨checkargs= n⟩ | ⟨checkargs>= n⟩ | ⟨i⟩

We no longer need the categories of blocks and of r-instructions, and m includes all kinds of instructions. Furthermore, comparing two uses of w, fbc code sequences are simpler than abc instruction lists. Note that, here in fbc, every member of w is a sequence, of which each element is either a token representing the name of a byte code operation or a number. In the vlisp implementation, these numbers are all small enough unsigned integers to be stored in a single byte (i.e., less than 256).

4.2 The Augmented Flattened Byte Code Language

The purpose of the Augmented Flattened Byte Code Language afbc is similar to that of the abc, namely to extend the programming language to contain terms that can be used to describe the states of an fbc state machine, and to define its possible transitions.

As for the unflattened languages, all of the categories (templates, blocks etc.) and productions given for programming language (fbc) are included for the augmented language (afbc), and the extensions of the bnf for the augmented language do not feed back into the recursive construction of the old categories, so their extensions in the afbc are exactly the same as in the fbc.

The afbc tokens not in fbc are the same as those of abc not in tbc. The afbc syntactic categories not in fbc correspond exactly to those of abc not in tbc; here they are called (afbc) values, (afbc) argument stacks, etc. They use the same variable conventions as in abc. The productions for the augmented categories v, a, u, and s are the same as in the abc, but continuations are slightly different, the relevant bnf production is:

k ::= halt | ⟨cont t n a u k⟩

4.3 States and Actions

fbc states differ from tbc states in that they contain a template belonging to the fbc language rather than the tbc language. In addition, instead of having a “code register” they have a numerical “program counter.” It is interpreted as an offset into the code sequence of the template.

Officially, the states of an fbc state machine are the sequences of the form

⟨t, n, v, a, u, k, s⟩.

The components of a state are called, in order, its template, offset, value, argument stack, environment, continuation, and store, and we may informally speak of them as being held in registers. We will use the variable w to refer to the code sequence (or just the code) of a state, i.e., w = t(1). Note that, with our conventions, w(n) is the first element of w † n, if 0 ≤ n < #w. The halt states are the states such that n = #w (so w†n = ⟨⟩).

Again, we present the actions relation for fbc state machines as the union of subfunctions called (action) rules, or fbc or afbc rules to distinguish from tbc rules. The various rules are functions from pairwise disjoint subsets of states×inputs into states×outputs. The same distinction between pure rules and port rules is made as with the tbc rules, but, again, only pure rules will be specified at this level.

Each fbc machine also has an associated function globals, which still must be a function from some finite set of identifiers into locations.

We need another auxiliary function, compute-offset, which takes two integers and returns an integer representing an offset they are together coding. Keeping the size of a byte secret doesn’t seem worth the trouble, so for 0 ≤ n_{0}, n_{1},

compute-offset (n_{0}, n_{1}) = (256 ∗ n_{0}) + n_{1}.

We will usually write n_{0} ⊕ n_{1} for compute-offset (n_{0}, n_{1}).

Note that, if one is very careful, three auxiliary functions, mrl-store, mrl-value, and app-stack, that were defined for tbc must be changed slightly for the fbc, because fbc values are slightly different. As the new definitions would look exactly the same, they are omitted, and we will use the same names for the fbc versions of these functions without danger of confusion.

The presentation of the pure rules for the fbc will use the same conventions as were used for the tbc, except that here n stands for the offset of the ingoing state, n′ for the offset of the state produced, and w for t(1), the code sequence of the template of the ingoing state.

4.3.1 Return-like Rules

Rule 1: Return-Halt Domain conditions:

w†n = ⟨return⟩^{⌢}w_{1}

k = halt Changes:

n′ = #w Rule 2: Return Domain conditions:

w†n = ⟨return⟩^{⌢}w_{1} k = ⟨cont t_{1} n_{1} a_{1} u_{1} k_{1}⟩

Changes:

t′ = t_{1} n′ = n_{1} a′ = a_{1} u′ = u_{1} k′ = k_{1}

Rule 3: Call Domain conditions:

w†n = ⟨call #a⟩^{⌢}w_{1} v = ⟨closure t_{1} u_{1} l_{1}⟩

Changes:

t′ = t_{1} n′ = 0 u′ = u_{1}

Rule 4: Escape-Halt Domain conditions:

w†n = ⟨call 1⟩^{⌢}w_{1} v = ⟨escape halt l⟩

Changes:

n′ = #w Rule 5: Escape Domain conditions:

w†n = ⟨call 1⟩^{⌢}w_{1} v = ⟨escape ⟨cont t_{1} n_{1} a_{1} u_{1} k_{1}⟩ l⟩ a = ⟨v_{1}⟩

Changes:

t′ = t_{1} n′ = n_{1} v′ = v_{1} a′ = a_{1} u′ = u_{1} k′ = k_{1}

4.3.2 Jump-like Rules

Rule 6: Jumpf/True Domain conditions:

w†n = ⟨jumpf n_{1} n_{2}⟩^{⌢}w_{1} v ≠ false

Changes:

n′ = n + 3

Rule 7: Jumpf/False Domain conditions:

w†n = ⟨jumpf n_{1} n_{2}⟩^{⌢}w_{1} v = false

Changes:

n′ = n + 3 + (n_{1} ⊕ n_{2})

Rule 8: Jump Domain conditions:

w†n = ⟨jump n_{1} n_{2}⟩^{⌢}w_{1} Changes:

n′ = n + 3 + (n_{1} ⊕ n_{2})

Rule 9: Make Continuation Domain conditions:

w†n = ⟨make-cont n_{1} n_{2} #a⟩^{⌢}w_{1} Changes:

n′ = n + 4 a′ = ⟨⟩ k′ = ⟨cont t (n + 4 + (n_{1} ⊕ n_{2})) a u k⟩

Rule 10: Literal Domain conditions:

w†n = ⟨literal n_{1}⟩^{⌢}w_{1} e(n_{1}) = ⟨constant c⟩

Changes:

n′ = n + 2 v′ = c

Rule 11: Closure Domain conditions:

w†n = ⟨closure n_{1}⟩^{⌢}w_{1} e(n_{1}) = ⟨template b_{2} e_{2}⟩

Changes:

n′ = n + 2 v′ = ⟨closure e(n_{1}) u #s⟩ s′ = s^{⌢}⟨not-specified⟩

Rule 12: Global Domain conditions:

w†n = ⟨global n_{1}⟩^{⌢}w_{1}

e(n_{1}) = ⟨global-variable i⟩

l = globals(i) v_{1} = s(l) v_{1} ≠ undefined

Changes:

n′ = n + 2 v′ = v_{1} Rule 13: Set Global Domain conditions:

w†n = ⟨set-global! n_{1}⟩^{⌢}w_{1}
e(n_{1}) = ⟨global-variable i⟩

l = globals(i) l ≤ #s

Changes:

n′ = n + 2 v′ = not-specified s′ = s + {l ↦ v}

Rule 14: Local Domain conditions:

w†n = ⟨local n_{1} n_{2}⟩^{⌢}w_{1} l = env-reference(u, n_{1}, n_{2}) v_{1} = s(l) v_{1} ≠ undefined

Changes:

n′ = n + 3 v′ = v_{1}

Rule 15: Set Local Domain conditions:

w†n = ⟨set-local! n_{1} n_{2}⟩^{⌢}w_{1} l = env-reference(u, n_{1}, n_{2}) l ≤ #s

Changes:

n′ = n + 3 v′ = not-specified s′ = s + {l ↦ v}

Rule 16: Push Domain Conditions:

w†n = ⟨push⟩^{⌢}w_{1} Changes:

n′ = n + 1 a′ = v:: a Rule 17: Make Environment Domain Conditions:

w†n = ⟨make-env #a⟩^{⌢}w_{1} Changes:

n′ = n + 2 a′ = ⟨⟩ u′ = add-layer(u, #s, #a) s′ = s^{⌢}a

Rule 18: Make Rest List Domain Conditions:

w†n = ⟨make-rest-list n_{1}⟩^{⌢}w_{1}

n_{1} + n_{2} = #a Changes:

n′ = n + 2 v′ = mrl-value (n_{2}, nil, a, s) a′ = a † n_{2} s′ = mrl-store (n_{2}, nil, a, s)

Rule 19: Unspecified Domain Conditions:

w†n = ⟨unspecified⟩^{⌢}w_{1}

Changes:

n′ = n + 1 v′ = not-specified

Rule 20: Check Args = Domain Conditions:

w†n = ⟨checkargs= n_{1}⟩^{⌢}w_{1} #a = n_{1}

Changes:

n′ = n + 2

Rule 21: Check Args >= Domain Conditions:

w†n = ⟨checkargs= n_{1}⟩^{⌢}w_{1} #a ≥ n_{1}

Changes:

n′ = n + 2 Rule 22: Primitive CWCC Domain Conditions:

w†n = ⟨%%cwcc⟩^{⌢}w_{1} a = ⟨v_{1}⟩ v_{1} = ⟨closure t_{1} u_{1} l_{1}⟩

Changes:

t′ = t_{1} n′ = 0 v′ = v_{1} a′ = ⟨⟨escape k #s⟩⟩ u′ = u_{1} s′ = s^{⌢}⟨not-specified⟩

Rule 23: Primitive CWCC-Escape Domain Conditions:

w†n = ⟨%%cwcc⟩^{⌢}w_{1} a = ⟨⟨escape ⟨cont t_{1} n_{1} a_{1} u_{1} k_{1}⟩ l_{1}⟩⟩

Changes:

t′ = t_{1} n′ = n_{1} v′ = ⟨escape k #s⟩ a′ = a_{1} u′ = u_{1} k′ = k_{1} s′ = s^{⌢}⟨not-specified⟩

Rule 24: Primitive CWCC-Escape-Halt Domain Conditions:

w†n = ⟨%%cwcc⟩^{⌢}w_{1} a = ⟨⟨escape halt l⟩⟩

Changes:

n′ = #w v′ = ⟨escape k #s⟩ Rule 25: Primitive Cons Domain Conditions:

w†n = ⟨%%cons⟩^{⌢}w_{1} a = ⟨v_{1} v_{2}⟩^{⌢}a_{1}

Changes:

n′ = n + 1 v′ = ⟨mutable-pair #s (1 + #s)⟩ a′ = ⟨⟩ s′ = s^{⌢}⟨v_{2} v_{1}⟩

Rule 26: Primitive Car-Immutable Pair Domain Conditions:

w†n = ⟨%%car⟩^{⌢}w_{1}

a = ⟨immutable-pair c_{1} c_{2}⟩:: a_{1}

Changes:

n′ = n + 1 v′ = c_{1} a′ = ⟨⟩

Rule 27: Primitive Car-Mutable Pair Domain Conditions:

w†n = ⟨%%car⟩^{⌢}w_{1} a = ⟨mutable-pair l_{1} l_{2}⟩:: a_{1} v_{1} = s(l_{1})

Changes:

n′ = n + 1 v′ = v_{1} a′ = ⟨⟩

Rule 28: Primitive Set-Car! Domain Conditions:

w†n = ⟨%%set-car!⟩^{⌢}w_{1}

a = ⟨v_{1} ⟨mutable-pair l_{1} l_{2}⟩⟩^{⌢}a_{1} l_{1} < #s

Changes:

n′ = n + 1 v′ = not-specified a′ = ⟨⟩ s′ = s + {l_{1} ↦ v_{1}} Rule 29: Primitive Apply-Closure Domain Conditions:

w†n = ⟨%%apply⟩^{⌢}w_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨closure t_{1} u_{1} l_{1}⟩ t_{1} = ⟨template b_{2} e_{2}⟩ a_{2} = app-stack (v_{1}, a_{1}, s)

Changes:

t′ = t_{1} n′ = 0 v′ = v_{2} a′ = a_{2} u′ = u_{1}

Rule 30: Primitive Apply-Escape Domain Conditions:

w†n = ⟨%%apply⟩^{⌢}w_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨escape k_{1} l_{1}⟩ k_{1} = ⟨cont t_{2} n_{2} a_{2} u_{2} k_{2}⟩ ⟨v_{3}⟩ = app-stack (v_{1}, a_{1}, s)

Changes:

t′ = t_{2} n′ = n_{2} v′ = v_{3} a′ = a_{2} u′ = u_{2} k′ = k_{2}

Rule 31: Primitive Apply-Escape-Halt Domain Conditions:

w†n = ⟨%%apply⟩^{⌢}w_{1} a = ⟨v_{1}⟩^{⌢}a_{1}^{⌢}⟨v_{2}⟩ v_{2} = ⟨closure t_{1} u_{1} l_{1}⟩ v_{2} = ⟨escape halt l_{1}⟩

Changes:

n′ = #w v′ = v_{2} Rule 32: Primitive Eqv Domain Conditions:

w†n = ⟨%%eqv⟩^{⌢}w_{1} a = ⟨v_{1} v_{2}⟩^{⌢}a_{1}

Changes:

n′ = n + 1 v′ = ((v_{1} = v_{2}) → true, false) a′ = ⟨⟩

Rule 33: Primitive Add Domain Conditions:

w†n = ⟨%%add⟩^{⌢}w_{1} m = n-ary-sum (a)

Changes:

n′ = n + 1 v′ = m a′ = ⟨⟩

5 The Flattener Algorithm

In this section, we present the applicative Scheme code that implements the flattener. In addition, we also consider it as a (perhaps slightly unusual) way to present a mathematical function.

5.1 The Flattener Proper

(define (flatten-template tem)
`(template
,(raw-code (flatten-code (cadr tem) 'closed))
,(flatten-table (caddr tem))))
(define (flatten-table table)
(map (lambda (entry)
(if (tbc-template? entry)
(flatten-template entry)
entry))
table))
(define (flatten-code code category)
(if (null? code)
empty-code-sequence
(let ((instr (car code))
(after-code (cdr code)))
(case (operator instr)
((make-cont)
(flatten-make-cont (first-operand instr)
(second-operand instr)
after-code
category))
((unless-false)
(if (and (eq? category 'closed)
(null? after-code))
(flatten-if-not-false (first-operand instr)
(second-operand instr))
(flatten-unless-false (first-operand instr)
(second-operand instr)
after-code
category)))
(else
(flatten-normal-instruction instr
  after-code
  category))))))

(define (flatten-normal-instruction instr after category)
(let ((after-code-sequence (flatten-code after category)))
(prepend-instruction instr after-code-sequence)))
(define (flatten-make-cont
    saved-code nargs after-code
    category)
(let ((after-code (flatten-code after-code 'closed))
   (saved-code (flatten-code saved-code category)))
(add-offset+byte-instruction
'make-cont
(code-length after-code)
nargs
(adjoin-code-sequences after-code saved-code))))
(define (flatten-if-not-false true-branch false-branch)
(let ((con (flatten-code true-branch 'closed))
   (alt (flatten-code false-branch 'closed)))
(add-offset-instruction
'jump-if-false
(code-length con)
(adjoin-code-sequences con alt))))
(define (flatten-unless-false
    true-code false-code after-code
    category)
(let ((con (flatten-code true-code 'open))
   (alt (flatten-code false-code 'open))
   (after-code (flatten-code after-code category)))
(add-offset-instruction
'jump-if-false

(+ 3 ; length of jump instr

   (code-length con))
(adjoin-code-sequences
 con
 (add-offset-instruction
  'jump (code-length alt)
  (adjoin-code-sequences alt after-code))))))

5.2 Auxiliary Procedures

(define (first-operand instr) (cadr instr))
(define (second-operand instr) (caddr instr))
(define (operator instr) (car instr))

(define (add-offset-instruction name offset after-code)
  (prepend-instruction
  `(,name ,@(expand-offset offset))
   after-code))
(define (add-offset+byte-instruction name offset
                                     byte after-code)
  (prepend-instruction
  `(,name ,@(expand-offset offset) ,byte)
   after-code))
(define byte-limit 256)
(define (tbc-template? entry)
  (and (pair? entry)
       (eq? (car entry) 'template)))
(define (expand-offset offset)
  (list (quotient offset byte-limit)
        (remainder offset byte-limit)))

Correctness depends on the fact that expand-offset and ⊕ are effectively inverses:

Lemma 2 Expand-offset/⊕. Let ⟨n_{0}, n_{1}⟩ be the result of applying expand-offset to n. Then n_{0}⊕n_{1} = n.

5.3 The Code Sequence Data Type

The following five identifiers implement the data type of code sequences.

(define empty-code-sequence 'declared)
(define prepend-instruction 'declared)
(define adjoin-code-sequences 'declared)
(define raw-code 'declared)
(define code-length 'declared)
(let ((code-sequence-marker (list 'code-sequence-marker)))
  (let ((make-code-sequence
         (lambda (raw-code len)
           (list code-sequence-marker raw-code len)))
        (code-sequence?
         (lambda (cs)
           (and (pair? cs)

           (eq? (car cs) code-sequence-marker)))))
(set! empty-code-sequence (make-code-sequence '() 0))
(set!
prepend-instruction
(lambda (instr after-code)
  (make-code-sequence
   (append instr (raw-code after-code))
   (+ (length instr) (code-length after-code)))))
(set!
adjoin-code-sequences
(lambda (first second)
  (make-code-sequence
   (append (raw-code first)
           (raw-code second))
   (+ (code-length first)
      (code-length second)))))
(set!
raw-code
(lambda (code-sequence)
  (if (code-sequence? code-sequence)
      (cadr code-sequence)
      (compiler-error
       "raw-code -- bad code sequence"
       code-sequence))))
(set!
code-length
(lambda (code-sequence)
  (if (code-sequence? code-sequence)
      (caddr code-sequence)
      (compiler-error
       "code-length -- bad code sequence"
       code-sequence))))))

If s is a code sequence, the length of the raw code contained in s is equal to the code-length of s. This holds true of the empty code sequence. Moreover, it is preserved under the operations of prepending an instruction and adjoining sequences, because the length of the result of appending a number of lists is equal to the sum of their lengths.

6 Establishing Correspondence of Code

We shall eventually give the notion of correspondence between states in terms of a preliminary “code correspondence” relation ≃. This is really a four-place relation on a tbc instruction list, a tbc table, a fbc code sequence, and a fbc table. We think of it as a binary correspondence between the pair of its first two arguments and the pair of its last two arguments, written, for instance,

(w, e) ≃ (w_{F} , e_{F}).

It is defined as the least relation satisfying the conditions summarized in Table 2. One fine point in the definition concerns expressions of the form w†n: when we make an atomic assertion about w†n, we are implicitly asserting that it is well defined, so that n ≤ #w.

We will repeatedly use a fact about sequences:

Lemma 3 drop/adjoin. When n ≤ #w_{0}, (w_{0}†n)^{⌢}w_{1} = (w_{0}^{⌢}w_{1})†n.

For closed instruction lists, adding code to the end of a flattened version does not destroy the ≃ relation:

Lemma 4 ≃/adjoin. If (b_{0}, e) ≃ (w_{0}, e^{F}), then for any w_{1}:

(b_{0}, e) ≃ (w_{0}^{⌢}w_{1}, e^{F}).

Proof. We will assume that w_{0} is not of the form ⟨jump n_{0} n_{1}⟩^{⌢}w_{2}, and thus that (b_{0}, e) ≃ (w_{0}^{⌢}w_{1}, e^{F}) is not true in virtue of clause 6. For otherwise, (b_{0}, e) ≃ (w_{2}†(n_{0} ⊕ n_{1}), e^{F}), and we may apply the lemma^{1} to infer that

(b_{0}, e) ≃ (w_{2}†(n_{0} ⊕ n_{1})^{⌢}w_{1}, e^{F}).

Since w_{2}†(n_{0} ⊕ n_{1})^{⌢}w_{1} = w_{2}^{⌢}w_{1}†(n_{0} ⊕ n_{1}), we may apply clause 6 to infer:

(b_{0}, e) ≃ (⟨jump n_{0} n_{1}⟩^{⌢}(w_{2}^{⌢}w_{1}), e^{F}).

By the associativity of ^{⌢}, the desired conclusion holds in this case also. The proof is by induction mirroring the inductive definition of ≃.

1. Suppose b_{0} = ⟨m⟩ = ⟨⟨return⟩⟩ or ⟨⟨call n⟩⟩, and w_{0} = ⟨m⟩^{⌢}w. By the associativity of ^{⌢}, (⟨m⟩^{⌢}w)^{⌢}w_{1} = ⟨m⟩^{⌢}(w^{⌢}w_{1}), which is also an instance of clause 1.

1Naturally, w_{2}†(n_{0} ⊕ n_{1}) might begin with a jump, but this may be repeated only a finite number of times.

1. For m = ⟨return⟩ or ⟨call n⟩, (⟨m⟩, e) ≃ (m^{⌢}w_{F} , e_{F}).

2. For atomic z, (z:: m∗, e) ≃ (z^{⌢}w_{F} , e_{F}) if, first, either m∗ = w_{F} = ⟨⟩ or (m∗, e) ≃ (w_{F} , e_{F}), and second, depending on the form of z:

(a) if z = ⟨literal n⟩, ⟨global n⟩, or ⟨set-global! n⟩, then e(n) = e_{F} (n);

(b) if z = ⟨closure n⟩, then:

i. e(n) is of the form ⟨template b_{1} e_{1}⟩, and ii. e_{F} (n) is of the form ⟨template w_{2} e_{2}⟩, where iii. (b_{1}, e_{1}) ≃ (w_{2}, e_{2}).

3. (⟨make-cont w n⟩:: b, e) ≃ (⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} , e_{F}) if: (a) (b, e) ≃ (w_{F} , e_{F}); and

(b) (w, e) ≃ (w_{F} †(n_{0} ⊕ n_{1}), e_{F}). 3′. (⟨make-cont ⟨⟩ n⟩:: b, e) ≃ (⟨make-cont n_{0} n_{1} n⟩^{⌢}w_{F} , e_{F}) if:

(a) (b, e) ≃ (w_{F} , e_{F}); and

(b) #w_{F} = n_{0} ⊕ n_{1}.

4. (⟨⟨unless-false b_{1} b_{2}⟩⟩, e) ≃ (⟨jumpf n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) if:

(a) (b_{1}, e) ≃ (w_{F} , e_{F}); and

(b) (b_{2}, e) ≃ (w_{F} †(n_{0} ⊕ n_{1}), e_{F}).

5. (⟨unless-false y_{1} y_{2}⟩:: w, e) ≃ (⟨jumpf n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) if: (a) (y_{1}^{⌣}w, e) ≃ (w_{F} , e_{F});

(b) (y_{2}^{⌣}w, e) ≃ (w_{F} †(n_{0} ⊕ n_{1}), e_{F}).

6. (w, e) ≃ (⟨jump n_{0} n_{1}⟩^{⌢}w_{F} , e_{F}) if (w, e) ≃ (w_{F} †(n_{0} ⊕ n_{1}), e_{F}).

Table 2: Recursive Conditions for ≃.

2. Suppose that b_{0} = z:: b, w_{0} = z^{⌢}w. (The syntax ensures that m∗ really is of the form b.) Assume inductively that (b, e) ≃ (w^{⌢}w_{1}, e_{F}). Then we simply apply clause 2 to w^{⌢}w_{1}. The subclauses dealing with e and e_{F} are unaffected.

3. If b_{0} = ⟨make-cont b_{1} n⟩:: b, and w_{0} = ⟨make-cont n_{0} n_{1} n_{2}⟩^{⌢}w: As-

sume inductively:

(b, e) ≃ (w^{⌢}w_{1}, e_{F})

and

(b_{1}, e) ≃ (w†(n_{0} ⊕ n_{1})^{⌢}w_{1}, e_{F}).

By the drop/adjoin lemma, we may apply clause 3 with w^{⌢}w_{1} in place of w.

3′. A closed instruction sequence b_{0} is not of this form.

4. Similar to 3.

5. Similar to 3, using the fact that y_{i}^{⌣}b forms a closed instruction list b_{2}.

6. Similar to 3. QED.

On the other hand, for open instruction lists, adding code to the end of a flattened version corresponds to ^{⌣}:

Lemma 5 ≃/open-adjoin. If (y, e) ≃ (w_{0}, e^{F}) and (w, e) ≃ (w_{1}, e^{F}), then

(y^{⌣}w, e) ≃ (w_{0}^{⌢}w_{1}, e^{F}).

Proof. As in the previous proof, we may assume that w_{0} is not of the form ⟨jump n_{0} n_{1}⟩^{⌢}w_{2}, and thus that the correspondence does not hold in virtue of clause 6.

The proof is by an induction on y. We will arrange the cases to correspond to the clauses in the inductive definition of ≃, although the syntax of y entails that only the clauses 2, 3, 5, and 6 are relevant. We divide clause 2 into two subcases, depending whether m∗ = ⟨⟩ or m∗ = y_{0}. N. B. In this proof, subscripted variables w_{i} range over fbc instruction lists. The unsubscripted w ranges over tbc instruction lists.

2a. Assume y = ⟨z⟩. Then w_{0} = z, so clause 2 (applied to z:: w) guarantees the conclusion. The subclauses hold for z:: w for the same reason they hold for ⟨z⟩.

2b. Assume y = z:: y_{0}. Then w_{0} = z^{⌢}w_{2}, and by the IH,

(y_{0}^{⌣}w, e) ≃ (w_{2}^{⌢}w_{1}, e^{F}).

But (z:: y_{0})^{⌣}w = z:: (y_{0}^{⌣}w) , so we may again apply clause 2.

3. Assume y = ⟨make-cont y_{0} n⟩:: b; so

y^{⌣}w = ⟨make-cont y_{0}^{⌣}w n⟩:: b.

Moreover, w_{0} = ⟨make-cont n_{0} n_{1} n_{2}⟩^{⌢}w_{2}. By the ≃/adjoin lemma, (b, e) ≃ (w_{2}, e^{F}) entails that (b, e) ≃ (w_{2}^{⌢}w_{1}, e^{F}). By the IH and the drop/adjoin lemma, (y_{0}, e) ≃ (w_{2}†(n_{0} ⊕ n_{1}), e^{F}) implies

(y_{0}^{⌣}w, e) ≃ ((w_{2}^{⌢}w_{1})†(n_{0} ⊕ n_{1}), e^{F}).

3′. Assume y = ⟨make-cont ⟨⟩ n⟩:: b; so

y^{⌣}w = ⟨make-cont w n⟩:: b.

So w_{0} = ⟨make-cont n_{0} n_{1} n_{2}⟩^{⌢}w_{2}. We will show that y^{⌣}w and w_{0}^{⌢}w_{1} satisfy Clause 3 rather than Clause 3′.

As in the preceeding case, by the ≃/adjoin lemma, (b, e) ≃ (w_{2}, e^{F}) entails that (b, e) ≃ (w_{2}^{⌢}w_{1}, e^{F}). So Clause 3(a) is satisfied.

Because (y, e) ≃ (w_{0}, e^{F}), we may apply Clause 3′(b) to conclude that n_{0} ⊕ n_{1} = #w_{2}. Hence w_{2}^{⌢}w_{1}†(n_{0} ⊕ n_{1}) = w_{1}, so Clause 3(b) is also satisfied.

5. Assume y = ⟨unless-false y_{1} y_{2}⟩:: y_{3}. So w_{0} = ⟨jumpf n_{0} n_{1}⟩^{⌢}w_{2}. Apply the IH to y_{1}^{⌣}y_{3} and y_{2}^{⌣}y_{3}, using the drop/adjoin lemma.

6. As before. QED.

The flattener is intended to apply only to templates ⟨template b e⟩ that have been generated by the tabulator. These have the property that whenever we encounter an instruction ⟨closure n⟩, then e(n) is in fact a template. Conversely, when we encounter an instruction ⟨literal n⟩, ⟨global n⟩, or ⟨set-global! n⟩, then e(n) is not a template.

Definition 6 An instruction m occurs in an instruction sequence w if:

1. w = ⟨m⟩; 2. w = m_{1} :: w_{1} and either m = m_{1} or m occurs in w_{1};

3. w = ⟨⟨unless-false b_{1} b_{2}⟩⟩ or w = ⟨make-cont b_{1} n⟩:: b_{2}, and m occurs in b_{1} or b_{2};

4. w = ⟨make-cont y_{1} n⟩:: b and m occurs in y_{1} or b.

If z is a tbc neutral instruction, then z respects the template table e if:

1. if z = ⟨closure n⟩, then e(n) is a template ⟨template b_{1} e_{1}⟩, and moreover b_{1} (recursively) respects the template table e_{1};

2. if z = ⟨literal n⟩, then e(n) is a literal of the form ⟨constant c⟩; and

3. if z = ⟨global n⟩ or ⟨set-global! n⟩, then e(n) is a global of the form ⟨global i⟩.

A tbc closed or open instruction sequence w respects the template table e if every z that occurs in w respects e.

If t is a template ⟨template b e⟩, we will say that t respects its table, or that t is self-respecting, if b respects the template table e.

If t is a template ⟨template b e⟩, we will say that t respects its table, or that t is self-respecting, if b respects the template table e.

In the treatment of the tabulator, we have proved a lemma that states that the output of the tabulator always has this property. That is, if the result of the tabulator is a tbc template ⟨template b e⟩, then b respects the template table e. This provides the justification for proving the correctness of the flattener only for input templates with this property.

We will use F (w) to abbreviate the result of applying flatten-code to w and closed, if w is of the form b, and for the result of applying flatten-code to w and open, if w is of the form y. Similarly, we will use F (e) as an abbreviation for the result of applying flatten-table to e, and we will use F (t) to mean the result of applying flatten-template to t. Observe from the code that F (⟨template b e⟩) is ⟨template F (b) F (e)⟩.

Lemma 7 No initial jumps. F (w) is not of the form ⟨jump n_{0} n_{1}⟩^{⌢}w_{1}.

Proof. The flattener code ensures:

1. If w begins with a make-cont, then the first instruction of F (w) is a

     make-cont;

2. If w begins with an unless-false, then the first instruction of F (w)

     is a jumpf;

3. Otherwise, F (w) begins with the same instruction as w. QED.

Theorem 8 Flattener establishes ≃. Suppose that w respects the template table e.

A. (w, e) ≃ (F (w), F (e));

B. If n occurs in w and e(n) is of the form ⟨template b_{1} e_{1}⟩, then

(b_{1}, e_{1}) ≃ (F (w_{1}), F (e_{1})).

Proof. The proof is by simultaneous induction on the structure of w and the depth (in nested templates) of e.

A. (w, e) ≃ (F (w), F (e)): We assume inductively that:

1. Part B holds true for e;

2. If w is of the form ⟨⟨unless-false b_{1} b_{2}⟩⟩, then Part A holds true for b_{1} and b_{2} (together with the same e, naturally);

3. If w is of the form m:: w_{0}, then Part A holds true for w_{0}, and moreover:

(a) if m is of the form ⟨make-cont w_{1} n⟩, then Part A holds true for w_{1};

(b) If m is of the form ⟨unless-false w_{1} w_{2}⟩, then Part A holds true for w_{1} and w_{2}.

The proof is by cases on the grammar of w. However, we will list them in the order corresponding to the first five clauses of the definition of ≃. By Lemma 7, the initial instruction of F (w_{0}) is never of the form jump. Hence, a correspondence involving an expression of this form is never true in virtue of clause 6.

1. w = m = ⟨⟨return⟩⟩ or ⟨⟨call n⟩⟩. Then, by the algorithm, F (w) = m, satisfying clause 1.

2. w = ⟨z⟩, for atomic z. Then F (w) = z^{⌢}⟨⟩ = z, and we may apply clause 2, noting:

(a) Suppose z = ⟨literal n⟩: Then, because w respects e, e(n) is of the form ⟨constant c⟩, and the code of flatten-table ensures that e(n) = F (e)(n).

(b) Suppose z = ⟨global n⟩ or ⟨set-global! n⟩: Then, because w respects e, e(n) is of the form ⟨global i⟩, and the code of flatten-table ensures that e(n) = F (e)(n).

(c) Suppose z = ⟨closure n⟩: Then, because n occurs in w and w respects e, e(n) is of the form ⟨template b_{1} e_{1}⟩. Hence,

F (e)(n) = ⟨template F (b_{1}) F (e_{1})⟩.

So part 1 of the IH entails that clause 2b of ≃ is satisfied.

2′. w = z:: w_{0}, for atomic z. Then F (w) = z^{⌢}F (w_{0}). By the IH and the same observations we made in the previous case, we may again apply clause 2.

3. w = ⟨make-cont w_{1} n⟩:: b_{0}. Then

F (w) = ⟨make-cont n_{0} n_{1} n⟩^{⌢}F (b_{0})^{⌢}F (w_{1}),

where ⟨n_{0}, n_{1}⟩ = expand-offset(#F (b_{0})).

(a) IH 3 ensures (b_{0}, e) ≃ (F (b_{0}), F (e)), and ≃/adjoin allows us to infer (b_{0}, e) ≃ (F (b_{0})^{⌢}F (w_{1}), F (e)). Hence clause 3a in ≃ is satisfied.

(b) Using the expand-offset/⊕ lemma, (F (b_{0})^{⌢}F (w_{1}))†(n_{0} ⊕ n_{1}) = F (w_{1}). Hence, by IH part 3a, clause 3b in ≃ is satisfied.

3′. w = ⟨make-cont ⟨⟩ n⟩:: b_{0}. Then

F (w) = ⟨make-cont n_{0} n_{1} n⟩^{⌢}F (b_{0})^{⌢}⟨⟩,

where ⟨n_{0}, n_{1}⟩ = expand-offset(#F (b_{0})).

(a) IH 3 ensures (b_{0}, e) ≃ (F (b_{0}), F (e)), and ≃/adjoin allows us to infer (b_{0}, e) ≃ (F (b_{0})^{⌢}F (w_{1}), F (e)). Hence clause 3′(a) in ≃ is satisfied.

(b) n_{0} ⊕ n_{1} = #F (b_{0}) by Lemma expand-offset/⊕.

4. w = ⟨⟨unless-false b_{1} b_{2}⟩⟩. Then

F (w) = ⟨jumpf n_{0} n_{1}⟩^{⌢}F (b_{1})^{⌢}F (b_{2}),

where ⟨n_{0}, n_{1}⟩ = expand-offset(#F (b_{1})).

(a) IH part 2 gives (b_{1}, e) ≃ (F (b_{1}), F (e)). The ≃/adjoin lemma entails that (b_{1}, e) ≃ (F (b_{1})^{⌢}F (b_{2}), F (e)), satisfying clause 4a in ≃.

(b) Using the expand-offset/⊕ lemma, F (b_{1})^{⌢}F (b_{2})†(n_{0} ⊕ n_{1}) = F (b_{2}), so IH part 2 ensures that clause 4b in ≃ is satisfied.

5. w = ⟨unless-false y_{1} y_{2}⟩:: w_{1}. Then

F (w) = ⟨jumpf n_{0} n_{1}⟩^{⌢}F (y_{1})^{⌢}⟨jump n_{2} n_{3}⟩^{⌢}F (y_{2})^{⌢}F (w_{1}),

where n_{0} ⊕n_{1} = 3+#F (y_{1}), and n_{2} ⊕n_{3} = #F (y_{2}). IH part 3 ensures that (w_{1}, e) ≃ (F (w_{1}), F (e)).

(a) Clause 6 entails:

(w_{1}, e) ≃ (⟨jump n_{2} n_{3}⟩^{⌢}F (y_{2})^{⌢}F (w_{1}), F (e)).

IH part 3b ensures that (y_{1}, e) ≃ (F (y_{1}), F (e)), so by ≃/openadjoin,

(y_{1}^{⌣}w_{1}, e) ≃ (F (y_{1})^{⌢}⟨jump n_{2} n_{3}⟩^{⌢}F (y_{2})^{⌢}F (w_{1}), F (e)).

(b) IH part 3b ensures that (y_{2}, e) ≃ (F (y_{2}), F (e)), so by ≃/open-

adjoin,

(y_{2}^{⌣}w_{1}, e) ≃ (F (y_{2})^{⌢}F (w_{1}), F (e)).

Since n_{0} ⊕ n_{1} = #(F (y_{1})^{⌢}⟨jump n_{2} n_{3}⟩), we are done.

B. Here we assume inductively that Part A holds for all w_{1}, and all less deeply nested e_{1}, and that n occurs in w.

But if e(n) is of the form ⟨template b_{1} e_{1}⟩, then e_{1} is less deeply nested. Thus, applying Part A to b_{1} and e_{1}, (b_{1}, e_{1}) ≃ (F (b_{1}), F (e_{1})), as desired. QED.

7 Preservation of State Correspondence

Based on the underlying “code correspondence” relation ≃, we will define a binary “miscellaneous correspondence” relation ∼ between various kinds of syntactic objects of abc on the left and ones of afbc on the right, building up to a notion of correspondence between tbc states and fbc states that is preserved by state transitions.

We take advantage of the inessential fact that the two languages share some syntactic objects to simplify the definition. Thus some of the syntactic objects that are shared by the two languages are to be called self corresponding, namely, the halt continuation; all environments; undefined; not-specified; all constants; and all values beginning with mutable-pair, string, or vector. The relation ∼ is then defined recursively, as the least set of pairs whose left element is a member of one of the abc classes t, v, a, u, k or s, or is an abc state, and which satisfies the closure conditions given in Table 3. Note especially clauses (6) and (7), which reflect differences in how, and even in which registers, the two machines store “active” code. Also, case (4) applies to both argument stacks and stores.

The following easy lemma shortens the proof of the preservation theorem somewhat and justifies a looser way of thinking about computations of tbc and fbc state machines. One can talk about what they do (or would do under given circumstances), not just about what they might do.

Lemma 9 Determinacy of Pure Transitions. If M is either a tbc machine or an fbc machine, and M is in state S, then there is at most one state S′ such that M can proceed by one pure rule transition from S to S′.

Proof. The domain conditions for the different rules (of the same machine) are pairwise mutually incompatible, as can be seen by looking just at the required form of the code register, except for a few cases when one must also consider the value register or the argument register. Given a particular pure rule and a state, there is always at most one way of binding the variables of the domain equations so that they are satisfied. The next state is clearly determined by the rule, the ingoing state, and these bindings. QED.

Clearly the tbc rules are closely paralleled by the fbc rules – let us say that a tbc rule A corresponds to an fbc rule B if A and B have the same name, also that Closed Branch/True and Open Branch/True both correspond to Jumpf/True, and finally that Closed Branch/False and Open Branch/False (1) x ∼ x, if x is self corresponding

(2) ⟨closure t_{1} u l⟩ ∼ ⟨closure t_{2} u l⟩, if t_{1} ∼ t_{2}

(3) ⟨escape k_{1} l⟩ ∼ ⟨escape k_{2} l⟩, if k_{1} ∼ k_{2}

(4) v_{1}^{∗} ∼ v_{2}^{∗}, if #v_{1}^{∗} = #v_{2}^{∗} and, for every n < #v_{1}^{∗}, v_{1}^{∗}(n) ∼ v_{2}^{∗}(n)

(5) ⟨template b e_{1}⟩ ∼ ⟨template w e_{2}⟩, if (b, e_{1}) ≃ (w, e_{2})

(6) ⟨cont t_{1} b a_{1} u k_{1}⟩ ∼ ⟨cont t_{2} n a_{2} u k_{2}⟩, if (i) (b, t_{1}(2)) ≃ (t_{2}(1) † n, t_{2}(2)), and (ii) a_{1} ∼ a_{2} and k_{1} ∼ k_{2}

(7) ⟨t_{1}, b, v_{1}, a_{1}, u, k_{1}, s_{1}⟩ ∼ ⟨t_{2}, n, v_{2}, a_{2}, u, k_{2}, s_{2}⟩, if (i) (b, t_{1}(2)) ≃ (t_{2}(1) † n, t_{2}(2)), and (ii) v_{1} ∼ v_{2}, a_{1} ∼ a_{2}, k_{1} ∼ k_{2}, and s_{1} ∼ s_{2}

(8) S ∼ S_{F}, if S is any tbc halt state and S_{F} is any fbc halt state.

Table 3: Closure Conditions for ∼. both correspond to Jumpf/False. No tbc rule corresponds to Jump. A branch rule means one whose name ends in /True or /False – four for tbc and two for fbc.

The definitions of ≃ and ∼ have been constructed so that the next theorem can be proved by a straightforward, albeit lengthy argument. The reader is warned that there is a physical problem seemingly inherent in reading the body of the proof: five separate pages of this document need to be simultaneously displayed before one, namely the two tables defining ∼ and ≃, the presentations of two rules being compared, and the argument of the proof itself. We have found no better solution than a table and an unstapler.

Theorem 10 (Preservation of State Correspondence) Let M be a tbc machine and M_{F} be a fbc machine with the same globals as M. Let S be the state of M and S_{F} the state of M_{F}, and assume that S ∼ S_{F}. Then

(1) if M_{F} proceeds by the Jump rule to state S′_{F}, then S ∼ S′_{F}, and

(2) if M_{F} cannot proceed by the Jump rule, then, if either machine proceeds, then the other machine proceeds by a corresponding rule, and the resulting states correspond.

Proof. We can assume S = ⟨t b v a u k s⟩, and S_{F} = ⟨t_{F} n v_{F} a_{F} u k_{F} s_{F} ⟩, where t = ⟨template b_{0} e⟩, and t_{F} = ⟨template w e_{F} ⟩. From S ∼ S_{F} we have two facts that will be cited throughout the proof:

(i) (b, e) ≃ (w † n, e_{F}), and

(ii) v ∼ v_{F}, a ∼ a_{F}, k ∼ k_{F}, and s ∼ s_{F}.

\underline{For part (1)}, assume M_{F} can proceed by the Jump rule to state S′_{F}. We can thus assume that w † n = ⟨jump n_{1} n_{2}⟩^{⌢}w_{1}, and we know that S′_{F} is the same as S_{F}, except that the new offset is n + 3 + (n_{1} ⊕ n_{2}). Only the last clause in the definition of ≃ can give (i) when w † n begins with jump. From the applicability of that clause it follows that

(b, e) ≃ (w_{1} † (n_{1} ⊕ n_{2}), e_{F}).

But w_{1} = (w † n) † 3, so

w_{1} † (n_{1} ⊕ n_{2}) = ((w † n) † 3) † (n_{1} ⊕ n_{2}) = w † (n + 3 + (n_{1} ⊕ n_{2})).

Thus we have

(b, e) ≃ (w † (n + 3 + (n_{1} ⊕ n_{2})), e_{F}).

Given (ii), this is all that’s needed for S ∼ S′_{F}. QED part (1).

\underline{For part (2)}, assume that M_{F} cannot proceed by the Jump rule. We must consider the possible applicability of each rule for each machine, but there are helpful regularities in the cases. The more complicated cases generally are those where more components of the state change, but the branch rules seem more to the point of flattening, so we start with the branch rules for M in (2A), dispense with the non-branch rules for M_{F} relatively easily in (2B), slog through the non-branch rules for M in (2C), and coast through the non-branch rules for M_{F} in (2D). Most cases are named by a specific rule of one of the machines. Such cases tacitly assume that the named rule is applicable in the appropriate machine’s ingoing state.

Preservation (2A): Branch Rules for M

Case: Closed Branch/True

Assume b = ⟨⟨unless-false b_{1} b_{2}⟩⟩. As M_{F} cannot Jump, there is only one way that (i) can arise in the recursive definition of ≃, namely that w † n is of the form ⟨jumpf n_{0} n_{1}⟩^{⌢}w_{1}. The definition of ∼ ensures that a constant on the either side is ∼ only to itself. We have v ∼ v_{F}, so if v_{F} were the constant false it would follow that v = false, which contradicts the domain conditions of the rule. Hence M_{F} can apply Jumpf/True.

Thus M proceeds to a state S′ which is the same as S, except that its code register is b_{1}, and M_{F} proceeds to a state S′_{F} which is the same as S_{F}, except that its offset is n + 3. The first requirement for S′ ∼ S′_{F} becomes

(b_{1}, e) ≃ (w † (n + 3), e_{F}).

From (i), the form of b, and the definition of ≃, we have

(b_{1}, e) ≃ (w_{1}, e_{F}).

But w_{1} = (w † n) † 3 = w † (n + 3), and the other requirements for S′ ∼ S′_{F} hold over from S ∼ S_{F}, so we are done. QED Case.

Case: Closed Branch/False

Again assume b = ⟨⟨unless-false b_{1} b_{2}⟩⟩. As in the previous case, we can assume w † n is ⟨jumpf n_{0} n_{1}⟩^{⌢}w_{1}, and can see that M_{F} proceeds by the corresponding rule, Jumpf/False. Only the code register of S and the offset of S_{F} are changed, to b_{2} and n + 3 + (n_{0} ⊕ n_{1}) respectively, so the resulting states correspond if

(b_{2}, e) ≃ (w † (n + 3), e_{F}).

From (i), the form of b, and the definition of ≃, we have

(b_{2}, e) ≃ (w_{1} † (n_{0} ⊕ n_{1}), e_{F}).

But w_{1} † (n_{0} ⊕ n_{1}) = w † (n + 3 + (n_{0} ⊕ n_{1})). QED Case.

Case: Open Branch/True

This case is similar to that for Closed Branch/True – the essential point is that the definition of ≃ properly reflects the rules’ difference in treatment of Closed versus Open branches.

Arguing as above, we can assume that

b = ⟨unless-false y_{1} y_{2}⟩:: b_{1},

w † n = ⟨jumpf n_{0} n_{1}⟩^{⌢}w_{1}, and

v ≠ false ≠ v_{F}.

Thus M_{F} proceeds by Jumpf/True. From the rules, the definition of ∼ and the holdover facts (ii), the only thing needed to ensure that the resulting states correspond is

(y_{1}^{⌣}b_{1}, e) ≃ (w † (n + 3), e_{F}).

Here (i) has become

(⟨unless-false y_{1}, y_{2}⟩:: b_{1}, e) ≃ (⟨jumpf n_{0} n_{1}⟩^{⌢}w_{1}, e_{F}).

Only one case of the definition of ≃ can yield this, and its applicability implies that

(y_{1}^{⌣}b_{1}, e) ≃ (w_{1}, e_{F}),

which follows, because w_{1} = (w † n) † 3 = w † (n + 3). QED Case.

Case: Open Branch/False

This case is to the previous as that for Closed Branch/False is to that for Closed Branch/True. QED Case.

Preservation (2B): Branch Rules for M_{F}

Case: Jumpf/True

By the determinacy of pure computations and previous cases, it suffices to show is that M proceeds by one of the corresponding rules (Closed Branch/True or Open Branch/True). The two possibly applicable cases of the definition of ≃ each yield the applicability of one of theses rules for M. QED Case.

Case: Inner Branch Right Similar to the above case. QED Case.

Preservation (2C): Non-Branch Rules for M

Case: Return-Halt, Escape Halt, and Primitive CWCC-Escape-Halt

From the definition of ∼, if x is halt or of the form ⟨escape halt l⟩, then for all y, x ∼ y iff x = y. Then (i) and (ii) clearly imply that if any one of these rules is applicable for M then the corresponding rule is for M_{F} in S_{F}. In all cases the outgoing states are halt states of the respective machines and hence correspond. QEd Case.

Case: Return

Here we have easily that w † n is of the form ⟨return⟩^{⌢}w_{1}. The second domain equation for M_{F} just asserts that k_{F} is of a certain form (actually, any non-halt continuation). We know that k is of this form from the second domain equation for Return for M; (ii) says k ∼ k_{F}, and so the definition of ∼ then ensures that k_{F} is of the required form too. So M_{F} can Return.

In fact, the definition of k ∼ k_{F} implies that we can write

(a) k = ⟨cont t_{1} b_{1} a_{1} u_{1} k_{1}⟩, and

(b) k_{F} = ⟨cont t_{2} n_{2} a_{2} u_{1} k_{2}⟩, where

(c) (b_{1}, t_{1}(2)) ≃ (t_{2}(1) † n_{2}, t_{2}(2)), and (d) a_{1} ∼ a_{2} and k_{1} ∼ k_{2}.

The resulting states are

S′ = ⟨t_{1} b_{1} v a_{1} u_{1} k_{1} s⟩ and
S′_{F} = ⟨t_{2} n_{2} v_{F} a_{2} u_{1} k_{2} s_{F} ⟩.

The first condition on S′ ∼ S′_{F} becomes just (c). The second requires that v ∼ v_{F} (which is part of (ii)), that a_{1} ∼ a_{2} (part of (d)), that k_{1} ∼ k_{2} (again see (d)), and that s ∼ s_{F} (part of (ii)). QED Case.

Case: Call

As in the case for Return, the first domain equation for an M_{F} Call follows from the first domain equation for this M Call, together with the assumption that M_{F} cannot Jump and the fact that #a = #a_{F}, which follows from a ∼ a_{F} and the definition of ∼.

It also follows from the applicability of Call for M that we can assume v = ⟨closure t_{1} u_{1} l_{1}⟩, where t_{1} = ⟨template b_{1} e_{1}⟩. The definition of v ∼ v_{F} then implies that v_{F} = ⟨closure t_{2} u_{1} l_{1}⟩, where t_{1} ∼ t_{2}. Thus M_{F} can also apply Call, and the resulting states are

S′ = ⟨t_{1} b_{1} v a u_{1} k s⟩ and
S′_{F} = ⟨t_{2} 0 v_{F} a_{F} u_{1} k_{F} s_{F} ⟩.

The first condition for their correspondence becomes

(b_{1}, e_{1}) ≃ (t_{2}(1) † 0, t_{2}(2)),

which is equivalent to the established fact t_{1} ∼ t_{2}. The other conditions for S′ ∼ S′_{F} amount just to (ii). QED.

Case: Escape

This case is extremely similar to the Return case, using the escape clause of the definition of ∼. QED Case.

Case: Make Continuation

From (i), the domain equation for Make Continuation for M, the definitions of ≃ and ∼, and the fact that M_{F} can’t jump, we can assume

(a) b = ⟨⟨make-cont b_{0} #a⟩⟩^{⌢}b_{1} (b) w † n = ⟨make-cont n_{0} n_{1} #a⟩^{⌢}w_{1}

(c) (b_{1}, e) ≃ (w_{1}, e_{F}), and

(d) (b_{0}, e) ≃ (w_{1} † (n_{0} ⊕ n_{1}), e_{F})

Thus M_{F} can also apply Make Continuation, and we can call the resulting states S′ and S′_{F}, where S′ is the same as S except that it has code b_{1}, arguments ⟨⟩, and continuation

k′ = ⟨cont t b_{0} a u k⟩,

and S′_{F} is the same as S_{F}, except that it has offset n + 4, arguments ⟨⟩, and continuation

k′_{F} = ⟨cont t_{F} n_{2} a_{F} u k_{F} ⟩, where
n_{2} = n + 4 + (n_{0} † n_{1}).

The first requirement for S′ ≃ S′_{F} becomes

(b_{1}, e) ≃ (w † (n + 4), e_{F}),

which follows from (c), as (b) implies that w_{1} = w † (n + 4). The second requirement becomes: v ∼ v_{F} (holds over, see (ii)); ⟨⟩ ∼ ⟨⟩ (directly from the definition of ∼); k′ ∼ k′_{F} (see below); and s ∼ s_{F} (from (ii)). For k′ ∼ k′_{F} we need a ∼ s_{F} (see (ii)), k ∼ k_{F} (see (ii)), and

(b_{0}, e) ≃ (w † n_{2}, e_{F}),

which follows from (d) and w_{1} = w † (n + 4). QED Case.

Case: Other tbc Rules

All other rules follow in approximately the same way as the above ones. Several observations are in order to point out rough spots and where various wrinkles of the definitions come into play.

1. Literal, Global, and Set Global use the extra stipulation in the definition of ≃ that e(n) = e_{F} (n) (this is really just a displaced part of the code).

2. Global and Set Global use the fact that M and M_{F} have the same globals.

3. Closure needs the extra stipulations specified for its case in the definition of ≃; here 2.b.iii gives exactly what is needed according to the definition of ∼ to conclude that the two templates of the created closures actually correspond.

4. Make Rest List needs a lemma proved by simultaneous induction, namely that if f is either of mrl-value or mrl-store, v_{1} ∼ v_{2}, a_{1} ∼ a_{2}, and s_{1} ∼ s_{2}, then

f(n, v_{1}, a_{1}, s_{1}) ∼ f(n, v_{2}, a_{2}, s_{2}).

5. Primitive Apply-Closure and Primitive Apply-Escape both need a similar inductively established lemma about app-stack, namely that

app-stack (v_{1}, a_{1}, s_{1}) ∼ app-stack (v_{2}, a_{2}, s_{2}),

if v_{1} ∼ v_{2}, a_{1} ∼ a_{2}, and s_{1} ∼ s_{2}.

QED Case.

Preservation (2D): Non-Branch Rules for M_{F}

By now it should be a routine matter to check that if any one of these rules is applicable, then the corresponding one is for M. Again, because of determinacy and the previous case, this is all that is needed. QED Preservation Theorem.

8 Correctness of the Flattener

We extend the operational semantics given so far by specifying answer functions for tbc and fbc. In order to give a more general formulation of the correctness theorem, we use ternary answer functions A_{T BC} (t, s, globals) and A_{F BC} (t, s, globals), which take as arguments a template, an initial store, and a global locator function. As the last two arguments are often understood, either or both may be suppressed. We use an artificial error value so that the answer functions are total.

Given a tbc template t, store s, and global locator globals, let C be the unique tbc computation from the initial state

⟨t, t(1), undefined, ⟨⟩, empty-env, halt, s⟩.

If C is successful and ends with a number n in the value register, then we define A_{T BC} (t, s, globals) = n; otherwise A_{T BC} (t, s, globals) = ⊥.

Given an fbc template t, store s, and global locator globals, A_{F BC} (t, s, globals) is defined in the same way, except starting from the initial state

⟨t, 0, undefined, ⟨⟩, empty-env, halt s⟩.

Recall that F (t) means the result of applying the flattener to a tbc template t. We need one more concept for the correctness theorem. Call a tbc store codeless if none of its elements begins with closure or escape. Note that a codeless tbc store is also an fbc store; for our current purposes, it is essentially flattened already, even though there is some residual tree structure (especially in the Scheme constants).

Theorem 11 Correctness of the Flattener If t is any self-respecting tbc template, s is any codeless store, and globals is any global locator, then

A_{T BC} (t, s, globals) = A_{F BC} (F (t), s, globals).

Proof. Assuming t, s, and globals are as hypothesized, let H be the tbc state history generated from the initial state

⟨t, t(1), undefined, ⟨⟩, empty-env, halt, s⟩,

and H_{F} the fbc state history generated from the initial state

⟨F (t), 0, undefined, ⟨⟩, empty-env, halt s⟩.

By the fact that t is self-respecting and the theorem on the establishment of ≃,

(t(1), t(2)) ≃ (F (t(1)), F (t(2))).

Furthermore, F (t) = ⟨template F (t(1)) F (t(2))⟩, so the first requirement for H(0) ∼ H_{F} (0) holds. The other requirements are immediate, except for s ∼ s, which holds because s is codeless, so the initial states correspond.

Lemma 12 For every i in the domain of H there is a j in the domain of H_{F} such that i ≤ j and H(i) ∼ H_{F} (j).

Proof of lemma. We already have this for i = 0. It is enough to show that there is some j′ > j such that H(i + 1) ∼ H_{F} (j′), assuming H(i + 1) is defined, i ≤ j, and H(i) ∼ H_{F} (j).

Note that an fbc computation can only apply the Jump rule finitely many times in a row, because it increases the offset register by at least three. Using this fact and the first part of the preservation theorem, we can find a j′′ such that i ≤ j′′, H(i) ∼ H_{F} (j′′), and the Jump rule is not applicable in state H_{F} (j′′).

Now the second part of the preservation theorem applies, and we have that H(i + 1) ∼ H_{F} (j′′ + 1) and j′′ + 1 > j. QED Lemma.

If H is an infinite sequence, then H_{F} must be (by the i ≤ j part of the lemma), and both answers are ⊥.

Assume no rule is applicable to H(i), and let j be such that H(i) ∼ H_{F} (j), by the lemma. If H(i) is not a halt state, then H_{F} (j) cannot be (by the definitions of halt states and state correspondence), and both answers are ⊥. If H(i) is a halt state, then H_{F} (j) is too, and the contents of their value registers correspond. The only thing corresponding to 0 is 0, and the only thing corresponding to 1 is 1, so the answers are equal. QED Theorem.

Note on Extensions: We have presented tbc and fbc machines with a limited set of rules for definiteness and to save effort, but one should keep in mind that the set of rules available to the two kinds of machines can clearly be augmented without destroying the correctness theorem. It is mainly necessary to make sure that the preservation theorem is preserved, but that is easy for, say, additional primitives that might be used to manipulate strings and vectors.

References

[1] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp byte-code compiler. M 92B092, The MITRE Corporation, 1992.

[2] J. D. Guttman, L. G. Monk, J. D. Ramsdell, W. M. Farmer, and V. Swarup. A guide to vlisp, a verified programming language implementation. M 92B091, The MITRE Corporation, 1992.