The VLISP Byte-Code Compiler

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

The MITRE Corporation^{1} M92B092 September 1992

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. 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 provides a detailed presentation of the byte-code compiler and its proof of correctness. iv

Contents

1 Formal Syntax 1 1.1 Scheme Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . 2 1.2 The Basic Byte Code Syntax . . . . . . . . . . . . . . . . . . 3 1.3 The Tabular Byte Code Syntax . . . . . . . . . . . . . . . . . 5

2 Denotational Semantics 7

2.1 Scheme Denotational Semantics . . . . . . . . . . . . . . . . . 7 2.1.1 Domain equations . . . . . . . . . . . . . . . . . . . . 10 2.1.2 Semantic functions . . . . . . . . . . . . . . . . . . . . 11 2.1.3 Auxiliary functions . . . . . . . . . . . . . . . . . . . . 13

2.2 Byte Code Denotational Semantics . . . . . . . . . . . . . . . 15 2.2.1 Domain equations . . . . . . . . . . . . . . . . . . . . 15 2.2.2 Semantic functions . . . . . . . . . . . . . . . . . . . . 16 2.2.3 Auxiliary functions . . . . . . . . . . . . . . . . . . . . 17

2.3 Tabular Byte Code Denotational Semantics . . . . . . . . . . 19 2.3.1 Semantic functions . . . . . . . . . . . . . . . . . . . . 19

3 Byte Code Compiler Algorithm 25 3.1 Expressions . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.2 Commands . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.3 Arguments . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 3.4 Byte Code Data Type . . . . . . . . . . . . . . . . . . . . . . 30 3.5 Environments . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.6 Opcode Table and Compiler Support for Primitives . . . . . . 32

4 Compiler Correctness 36 4.1 Syntactic Correctness . . . . . . . . . . . . . . . . . . . . . . 36 4.2 Semantic Correctness . . . . . . . . . . . . . . . . . . . . . . . 45

4.2.1 Single-valued Scheme Semantics . . . . . . . . . . . . 50 4.2.2 Compiler Correctness for Single-valued Semantics … 55

5 The Tabulator Algorithm 60 5.1 Tabulate and Related Procedures . . . . . . . . . . . . . . . . 60 5.2 Probe and Inverse Tables . . . . . . . . . . . . . . . . . . . . 64

5.2.1 Implementation of Probe . . . . . . . . . . . . . . . . 65 6 Correctness of the Tabulator Algorithm 67

6.1 Syntactic Correctness . . . . . . . . . . . . . . . . . . . . . . 67 6.2 Semantic Correctness . . . . . . . . . . . . . . . . . . . . . . . 76

References 80

List of Tables

1 Some Notation . . . . . . . . . . . . . . . . . . . . . . . . . . 2 2 Scheme Abstract Syntax . . . . . . . . . . . . . . . . . . . . . 3 3 Grammar for the Basic Byte Code . . . . . . . . . . . . . . . 4 4 Grammar for the Tabular Byte Code . . . . . . . . . . . . . . 6 5 Domains for the Semantics of Scheme . . . . . . . . . . . . . 10 6 Pure Procedure Objects . . . . . . . . . . . . . . . . . . . . . 46

1 Formal Syntax

In this section we present the abstract formal syntax for Scheme and for the byte code language (bbc) to which we will compile it. The semantics of these languages will follow in the next section.

The style of our grammars is somewhat different from that found in the Scheme Standard [2]. Some of these differences are purely incidental. The others are intended to make explicit our conception of the formal content conveyed by the Backus-Naur form clauses. Although these clauses are sometimes used to build up homogeneous strings of symbols from a given alphabet, we shall instead use them to build up more structured, tree-like objects. The latter seems more in tune with our interest in an abstract syntax or “derivation trees” [4].

With this convention, a bnf form such as p ::= ⟨lambda i* e⟩ allows a p to be a sequence s of length three, whose second element may itself be a sequence of any length. It does not mean a sequence of any length greater than or equal to two, where all but the first and last elements are is. We would write the latter as p ::= ⟨lambda⟩^{⌢}i*^{⌢}⟨e⟩.

For the sake of definiteness, we mention that we identify natural numbers with finite von Neumann ordinals, so that each number is the set of all smaller ones. We take a finite sequence to be a function with a natural number as its domain. Thus, an object s ∈ X* is a function s : n → X for some n ∈ ω, and an object s ∈ X^{+} is a function s : n → X for some non-zero n ∈ ω. Moreover, s(m) is the mth element of the (zero-based) sequence s, if the length of s is greater than m, and is undefined otherwise.

Thus, we regard every non-terminal value in the language defined by a bnf as being a nested finite sequence. Hence, we may define the rank of any value in a language:

Definition 1 (Rank)

The rank of a token (terminal) in a grammar is 0. The rank of a nonterminal finite sequence s is 1 + sup{rank(e) : e ∈ ran(s)}.

We will also use the notation contained in Table 1. In the last three items, which concern type coercions, x and y should be thought of as expressions with an explicit syntactic type. Many concepts and most of the rest of the notation used here are described in [5].

⟨ … ⟩  finite sequence formation, commas optional
#s  length of sequence s
⟨ x … ⟩  sequence s with s(0) = x
⟨ … x ⟩  sequence s with s(#s − 1) = x
rev s  reverse of the sequence s
s^{⌢}t  concatenation of sequences s and t
s † k  drop the first k members of sequence s
s ‡ k  the sequence of only the first k members of s
p → a, b  if p then a else b
ρ[x/i]  the function which is the same as ρ

except that it takes the value x at i

x in D  injection of x into domain D
x | D  projection of x to domain D
x, y, …: D true if the type of x, y, … is a disjoint sum

and x, y, … are injected from elements of D

Table 1: Some Notation

1.1 Scheme Syntax

In this section, we present a grammar for Scheme comparable to the one given in the Scheme Standard [2]. The syntactic objects are built from the following tokens:

• Scheme identifiers i;

• Scheme constants c;

  • The tokens: quote, begin, lambda, dotted lambda, set!, and if.

The bnf syntax is presented in Table 2.

Sequenced forms ⟨begin⟩^{⌢}e^{+} are not normally part of the underlying abstract syntax of Scheme. We have decided to include them, and to restrict primitive lambda-expressions to those containing a single body-form. We find this trade-off slightly more natural. For instance, Scheme source code of the form:

  (if test
      (begin form 1 ... form n)
      else clause)

must be translated into the form:

e, E ::= i | c_{sq} | ⟨quote c⟩ | e^{+} | ⟨begin⟩^{⌢}e^{+}

            | ⟨lambda i* e⟩ | ⟨dotted lambda i^{+} e⟩

| ⟨if e_{1} e_{2} e_{3}⟩ | ⟨if e_{1} e_{2}⟩ | ⟨set! i e⟩
c, K ::= c_{pr} | strings | lists, dotted lists, and vectors of c
c_{pr} ::= numbers, booleans, characters, symbols and nil
c_{sq} ::= numbers, booleans, characters and strings
i, I ::= identifiers (variables)
Γ ::= e  (commands)

Table 2: Scheme Abstract Syntax

   (if test
       ((lambda () form 1 ... form n))
       else clause)

to be represented in the official abstract syntax. This simply makes the compilation task a little more complicated, as we would need to eliminate the call to the lambda-form.

We have also syntactically assimilated Scheme procedures of the form:

   (lambda var body)

to those of the form:

   (lambda ( . var) body)

This is their treatment in the denotational semantics anyway.

Within the category of constants c, we distinguish primitive constants from compound constants. Primitive constants are those that are not represented in the semantics by allocating locations in the store, while compound constants do require storage.

1.2 The Basic Byte Code Syntax

This section presents the syntax of the vlisp Basic Byte Code. Expressions of the Basic Byte Code language (bbc) are nested lists constructed according to the bnf grammar given in Table 3 from the following tokens:

z ::= ⟨unless-false y_{1} y_{2}⟩
| ⟨literal c⟩ | ⟨closure t⟩
| ⟨global i⟩ | ⟨local n_{1} n_{2}⟩
| ⟨set-global! i⟩ | ⟨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
t ::= ⟨lap c b⟩

Table 3: Grammar for the Basic Byte Code

• natural numbers, Scheme identifiers, Scheme constants;

• “key-words”: lap, call, return, make-cont, literal,
closure, global, local, set-global!, set-local!,
push, make-env, make-rest-list, unspecified,
unless-false, checkargs=, and checkargs>=.

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 (bbc) neutral instructions, m for (bbc) (machine) instructions, b for (bbc) closed instruction lists (conjecturally < Eng. block), y for (bbc) open instruction lists, w for (bbc) (general) instruction lists, and t for (bbc) templates.

We will prove later that the result of the byte-code compiler is always a closed instruction list b. In the flattener algorithm, we treat open and closed instruction lists differently. Instructions of the form ⟨i⟩ are used only for “primop” identifiers (like %%cons) associated with a small set of denotationally specified Scheme primitives.

1.3 The Tabular Byte Code Syntax

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.

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 4) 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.

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 4: Grammar for the Tabular Byte Code

2 Denotational Semantics

2.1 Scheme Denotational Semantics

This section is a slightly modified version of an appendix to the proposed ieee Scheme standard. As such, it is primarily the work of William Clinger and Jonathan Rees. It provides a formal denotational semantics for the primitive expressions of Scheme and selected built-in procedures. The version here differs from the standard version in three ways.

• We have reformulated some definitions using different notation or conventions. These changes are largely cosmetic.

• The domains have been made somewhat more concrete. In particular, L has been identified with N, and S has been identified with E*. Note that this entails that, at the current level of modeling, memory is conceived as unbounded.

• We have removed tests from the semantics to check whether a new storage location can be allocated in S. The official Scheme semantics uses conditionals that raise an “out of memory” error if there is no unallocated location. However, if memory is conceived as unbounded, this situation will not arise. Moreover, it does not seem that all situations in which a real Scheme interpreter can run out of memory are represented in the official semantics. Thus, we have chosen to represent all memory exhaustion errors uniformly at a much lower level in the formal specification.

• The constraints on K given in the section on Semantics of Constants has been added. It was needed in our work on the faithfulness of an operational semantics for the bbc to its denotational semantics.

We wish to rely as much as possible on standard usage for the theory of denotational semantics, but some clarifications and non-standard extensions are in order to keep our more complex semantical manipulations from becoming obscure or suspect.

Denotational domains are always taken to be pointed cpo’s, with ordering and minimum element indicated as usual by ⊑ and ⊥ respectively, possibly with disambiguating subscripts. Four domain constructors will be of particular importance:

1. Given two domains A and B, the “arrow domain” A → B has as elements all of the continuous functions from A to B. No new bottom is added: ⊥_{A→B} = (λx. ⊥_{B}). Note that with this approach D is never equal to, say, D → D, although the two may be isomorphic by a notationally suppressed isomorphism.

2. Given a sequence of denotational domains (of any ordinal length greater than one), their disjoint union (or disjoint sum^{1}) is constructed in some standard way; a new bottom is added. For definiteness, we will take the non-bottom elements of the disjoint union of ⟨D_{i} | i < β⟩ to be the set of pairs ⟨i, x_{i}⟩ such that x_{i} ∈ D_{i}. In this case there are associated injections and projections, as well as typing predicates, as mentioned in the table of notation above. Note that if D_{i} is a direct summand of D, then ⊥_{D} : D_{i} is false.

3. Given a domain D, D^{∗} is the domain of finite sequences from D. A new bottom is added, for which length is undefined, and which is different from the sequence of length 0. All other elements have finite lengths and can be applied to numbers less than their lengths. Sequences of defined, but different lengths are always incompatible in the ordering. Two sequences of the same length are ordered pointwise. Note that the domain version of D^{∗} differs from the pure set of finite sequences from D, for which we use the same notation.

4. Cartesian products, usually of length two, but allowably of any ordinal length greater than one, have elements which are all sequences of the same length. Component extraction is by application to indices. No new bottom is added, as the sequence of bottoms of the components suffices.

We will have no need for a genuine direct sum construction, as opposed to a direct product; they are essentially different only for infinite sequences of arguments.

Call these four constructors basic, and a domain D produced by a basic constructor decomposable. Each basic constructor can be thought of as producing a domain from a sequence of arguments. We assume that the details are arranged so that these contructions are reversible, that is, that a decomposable domain has a unique basic constructor and argument sequence.

1This is not to be confused with a genuine direct sum nor with an ordinary union of domains which happen to be pairwise disjoint.

Thus we can speak of five disjoint classes of domains: arrow domains, disjoint sums, finite sequence domains, direct (or Cartesian) products, and indecomposable domains. Say that an indecomposable domain has an empty argument list.

An operation of functional lifting^{2} will be useful to simplify certain fixed point constructions. Suppose that the arguments of D are the sequence of D_{i} for i less than β, and that for each i less than β, f_{i} : D_{i} → D_{i}. (Here, and usually with denotational domains, → implies continuity. Also, association of application is usually to the left.) We define the lifting of these functionals to a function f on D. It should be easy to verify that f : D → D. Assume x is an arbitrary non-bottom element of D, then:

1. If D is D_{0} → D_{1} and y ∈ D_{0}, then fxy = f_{1}(x(f_{0}(y))).

2. If D is a disjoint sum and x = ⟨i, x_{i}⟩, then fx = ⟨i, f_{i}(x_{i})⟩. Also, f is strict, i.e., f⊥_{D} = ⊥_{D}.

3. If D = D_{0}^{∗} and x = ⟨x_{k} : D_{0} | k < n⟩, then fx = ⟨f_{0}(x_{k}) | k < n⟩; f is strict.

4. If D is a Cartesian product and x = ⟨x_{i} : D_{i} | i < β⟩, then fx = ⟨f_{i}(x_{i}) | i < β⟩.

We turn now to a few more detailed comments on the Scheme semantics. The reason that expression continuations take sequences of values instead

of single values is to simplify the formal treatment of procedure calls and to make it easy to add multiple return values.

The order of evaluation within a call is unspecified in the official Scheme semantics. In the compiler algorithm, however, we will select a single value for the permutations permute and unpermute applied to the arguments in a call before and after they are evaluated. The correctness proof will make use of this value.

We will also use Ide, Con, Exp, and Com to refer to the syntactic classes of identifiers i, constants c, expressions e, and commands (identical with expressions e), respectively.

The semantics of constants, given by a function K, will not be completely defined. Rather, we will give constraints on this function. In essence, we consider its actual value to be a parameter to the semantics of Scheme.

2Not to be confused with what is sometimes called the lifting of a domain by adding a new bottom.

α ^{∈} L = N  locations
ρ ^{∈} U = Ide → L  environments
ν ^{∈} N  natural numbers
T = {false, true}  booleans
T_{L} = {mutable, immutable} mutability flags
Q  symbols
H  characters
R  numbers
E_{p} = L × L × T_{L}  pairs
E_{v} = L* × T_{L}  vectors
E_{s} = L* × T_{L}  strings
M = T + T_{L} + {null, empty, unspecified}

miscellaneous

ϕ ^{∈} F = L × (E* → K → C)  procedure values
ϵ ^{∈} E  ≅ Q + H + R + E_{p} + E_{v} + E_{s} + M + F

expressed values

σ ^{∈} S = E*  stores
θ ^{∈} C = S → A  command continuations
κ ^{∈} K = E* → C  expression continuations
A  answers
X  errors

Table 5: Domains for the Semantics of Scheme

2.1.1 Domain equations

The domains used in the denotational semantics of Scheme are presented in Table 5.

Note that exactly one domain equation is actually not an equation. It implicitly introduces an isomorphism between E (which we assume to be indecomposable) and a disjoint sum, say ψ_{E} : E ≅ E_{Σ}. This justifies an extension of the notations for projection, injection, and typing introduced above for disjoint sums. Thus, if D is an argument (component) of E_{Σ}, e ∈ E, and d ∈ D, then

e | D = ψ_{E}(e) | D;

(d in E) = ψ_{E}^{−}1(d in E_{Σ}); and

e : D iff ψ_{E}(e) : D.

2.1.2 Semantic functions

K_{0} : c_{pr} → E
K : Con → E
E : Exp → U → K → C
E* : Exp* → U → K → C
C : Com* → U → C → C

Semantics of Constants We first define K_{0}. Suppose that c is a number, character, or symbol. Then K_{0}[[c]] = c. In addition:

K_{0}[[nil]] = null in E

K_{0}[[#f]] = false in E

K_{0}[[#t]] = true in E

We require that K_{0} ⊑ K and several other conditions. First,

1. If c is a string of length n, and K[[c]] is a non-bottom value ϵ, then ϵ : E_{s}, and #(ϵ | E_{s} 0) = n;

2. If c is a vector of length n, and K[[c]] is a non-bottom value ϵ, then ϵ : E_{v}, and #(ϵ | E_{v} 0) = n;

3. If c is a pair (and thus also if it is list or dotted list), and K[[c]] is a non-bottom value ϵ, then ϵ : E_{p}.

Second, if c is a string or vector, and K[[c]] is a non-bottom value ϵ, then (ϵ | D) 1 = immutable, where D is either E_{s}or E_{v}. Similarly, if c is a pair, and K[[c]] is a non-bottom value ϵ, then (ϵ | E_{p}) 2 = immutable.

Finally, if c_{0} is a vector or pair, and K[[c_{0}]] is a non-bottom value ϵ, and c_{1} is a subexpression of c_{0}, then K[[c_{1}]] is also non-bottom.

As a consequence of these conditions, we may infer that in no case does K[[c]] : F hold. It also follows that the only real freedom in the definition of K concerns which locations are occupied by what storage-requiring objects such as lists and vectors.

Semantics of Expressions

E[[K]] = λρκ . send (K[[K]]) κ

E[[I]] = λρκ . hold (lookup ρ I)

(single(λϵ . ϵ = empty in E→

wrong “undefined variable”, send ϵ κ))

E[[⟨E_{0}⟩^{⌢}E*]] =

λρκ . E*(permute(⟨E_{0}⟩^{⌢}E*)) ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) κ)

(unpermute ϵ*)))

E[[⟨lambda I* E_{0}⟩]] =

λρκ . λσ .

send (⟨new σ,

λϵ*κ′ . #ϵ* = #I* →

tievals(λα* . (λρ′ . E[[E_{0}]]ρ′κ′)

(extend ρ I* α*))
ϵ*,

wrong “wrong number of arguments”⟩ in E)

κ

(update (new σ) (unspecified in E) σ)

E[[⟨dotted lambda I*^{⌢}⟨I⟩ E_{0}⟩]] =

λρκ . λσ .

send (⟨new σ,

λϵ*κ′ . #ϵ* ≥ #I* →

tievalsrest

(λα* . (λρ′ . E[[E_{0}]]ρ′κ′)

(extend ρ (I*^{⌢}⟨I⟩) α*)) ϵ* (#I*),

wrong “too few arguments”⟩ in E)

κ

(update (new σ) (unspecified in E) σ)

E[[⟨if E_{0} E_{1} E_{2}⟩]] =

λρκ . E[[E_{0}]] ρ (single (λϵ . truish ϵ → E[[E_{1}]]ρκ, E[[E_{2}]]ρκ))

E[[⟨if E_{0} E_{1}⟩]] =

λρκ . E[[E_{0}]] ρ (single (λϵ . truish ϵ → E[[E_{1}]]ρκ, send (unspecified in E) κ))

Here and elsewhere, any expressed value other than empty could have been used in place of unspecified.

E[[⟨set! I E⟩]] =

λρκ . E[[E]] ρ (single(λϵ . assign (lookup ρ I)

ϵ

(send (unspecified in E) κ)))

E[[begin :: Γ*^{⌢}⟨E_{0}⟩]] = λρκ . C[[Γ*]]ρ(E[[E_{0}]]ρκ)

Semantics of Argument Lists and Command Lists

E*[[⟨⟩]] = λρκ . κ⟨ ⟩

E*[[E_{0} :: E*]] = λρκ . E[[E_{0}]] ρ (single(λϵ_{0} . E*[[E*]] ρ (λϵ* . κ (⟨ϵ_{0}⟩^{⌢}ϵ*))))

C[[⟨⟩]] = λρθ . θ

C[[Γ_{0} :: Γ*]] = λρθ . E[[Γ_{0}]] ρ (λϵ* . C[[Γ*]]ρθ)

2.1.3 Auxiliary functions

lookup : U → Ide → L lookup = λρI . ρI

extend : U → Ide* → L* → U extend =

λρI*α* . #I* = 0 → ρ, extend (ρ[(α* 0)/(I* 0)]) (I* † 1) (α* † 1)

wrong : X → C [implementation-dependent] send : E → K → C send = λϵκ . κ⟨ϵ⟩

single : (E → C) → K single =

λψϵ* . #ϵ* = 1 → ψ(ϵ* 0),

wrong “wrong number of return values”

The store is a sequence of expressed values indexed by the natural numbers less than the length of the store. The function new returns the smallest index corresponding to a location not in the store.

new : S → L new = λσ . #σ

hold : L → K → C hold = λακσ . α < #σ → send (σα)κσ, empty in E

assign : L → E → C → C assign = λαϵθσ . θ(update αϵσ)

update : L → E → S → S

The value of updateαϵσ is the finite sequence σ′ of length #σ′ = max(α+ 1, #σ) such that, for any α′ < #σ′,

α′ = α → ϵ, α′ < #σ → σ α, empty in E

tievals : (L* → C) → E* → C tievals =

λξϵ*σ . #ϵ* = 0 → ξ⟨ ⟩σ,

tievals (λα* . ξ(⟨new σ ⟩^{⌢}α*)) (ϵ* † 1) (update (new σ)(ϵ* 0)σ)

tievalsrest : (L* → C) → E* → N → C tievalsrest =

λξϵ*ν . list (ϵ* † ν)

(single(λϵ . tievals ξ ((ϵ* ‡ ν)^{⌢}⟨ϵ⟩))) truish : E → T truish = λϵ . (ϵ = false in E) → false, true

The auxiliary perm, used to define permute and unpermute, is not defined in the semantics. It is a function that, given a number ν, returns a permutation of the natural numbers less than ν. In the Vlisp implementation, we take permν, for any ν > 0, to be the permutation that given an argument ν_{0} < ν − 1, returns ν_{0} + 1, and which returns 0 when applied to ν − 1.

permute : Exp* → Exp* permute = λe* . λν . e*((perm #e*) ν)

unpermute : E* → E* unpermute = λϵ* . λν . ϵ*((perm #ϵ*)^{−1} ν)

applicate : E → E* → K → C applicate =

λϵϵ*κ . ϵ : F → ((ϵ | F) 1)ϵ*κ, wrong “bad procedure”

twoarg : (E → E → K → C) → (E* → K → C) twoarg =

λζϵ*κ . #ϵ* = 2 → ζ(ϵ* 0)(ϵ* 1)κ,

wrong “wrong number of arguments”

list : E* → K → C list =

λϵ*κ . #ϵ* = 0 → send (null in E) κ, list (ϵ* † 1)(single(λϵ . cons⟨(ϵ* 0), ϵ⟩κ))

cons : E* → K → C cons =

twoarg (λϵ_{1}ϵ_{2}κσ . (λσ′ . send (⟨new σ, new σ′, mutable⟩ in E) κ

(update(new σ′)ϵ_{2}σ′)
(update(new σ)ϵ_{1}σ)))

2.2 Byte Code Denotational Semantics

2.2.1 Domain equations

ψ ^{∈} K_{1} = E → C  one argument expression continuations
ρ_{R} ^{∈} U_{R} = N → N → L runtime environments
π ^{∈} P = E → E* → U_{R} → K_{1} → C

code segments

One can understand a byte code program as operating on a state with four “registers”, so to speak. These are a value register, containing an element of E, an argument stack, an environment register, and a continuation register, where the continuations here take only a single value, unlike the multiple value continuations of the official Scheme semantics. A program, when applied to values of these four kinds, yields a command continuation θ ∈ C. This in turn, if given a store σ, determines an answer. Thus, a code segment determines a computational answer if four registers and a store are given. 2.2.2 Semantic functions

B : b ∪ {⟨⟩} → U → P
Z : z → U → P → P
Y : y ∪ {⟨⟩} → U → P → P  (The variable y′ will range over y ∪ {⟨⟩})
T : t → U → P

Semantic Clauses for Core Instructions B[[⟨⟩]] = λρϵϵ*ρ_{R}ψσ . ϵ : R → ϵ | R in A, ⊥ B[[⟨⟨return⟩⟩]] = λρ . return B[[⟨⟨call n⟩⟩]] = λρ . call n B[[⟨⟨unless-false b_{1} b_{2}⟩⟩]] = λρ . if truish(B[[b_{1}]]ρ)(B[[b_{2}]]ρ) B[[⟨make-cont b_{1} n⟩:: b_{2}]] = λρ . make cont (B[[b_{1}]]ρ)n(B[[b_{2}]]ρ) B[[z:: b]] = λρ . Z[[z]]ρ (B[[b]]ρ) Z[[⟨unless-false y_{1} y_{2}⟩]] = λρπ . if truish(Y[[y_{1}]]ρπ)(Y[[y_{2}]]ρπ) Z[[⟨literal c⟩]] = λρ . literal (K[[c]]) Z[[⟨closure t⟩]] = λρ . closure (T [[t]]ρ) Z[[⟨global i⟩]] = λρ . global (lookup ρ i) Z[[⟨local n_{0} n_{1}⟩]] = λρ . local n_{0} n_{1} Z[[⟨set-global! i⟩]] = λρ . set global (lookup ρ i)

Z[[⟨set-local! n_{0} n_{1}⟩]] = λρ . set local n_{0} n_{1}

Z[[⟨push⟩]] = λρ . push

Z[[⟨make-env n⟩]] = λρ . make env n

Z[[⟨make-rest-list n⟩]] = λρ . make rest list n

Z[[⟨unspecified⟩]] = λρ . literal unspecified in E

Z[[⟨checkargs= n⟩]] = λρ . check args eq n

Z[[⟨checkargs>= n⟩]] = λρ . check args ge n

Y[[⟨make-cont y′ n⟩:: b]] = λρπ . make cont (Y[[y′]]ρπ) n (B[[b]]ρ)

Y[[z:: y′]] = λρπ . Z[[z]]ρ (Y[[y′]]ρπ)

Y[[⟨⟩]] = λρπ . π

T [[⟨lap c b⟩]] = B[[b]]

Semantic Clauses for Data Manipulation Primitives The clauses above do not specify the semantics for instructions z of the form ⟨i⟩. These instructions are considered to be data manipulation primitives. Since the standard data manipulation procedures of Scheme are not formally specified in the semantics, we have not thought it worthwhile to define them here.

However, in the formal semantics of the tabular byte code tbc below, we have specified several of these primitives. We have done so to demonstrate that it is straightforward to do so for a wide variety of primitives. Moreover, the proof that the operational semantics is faithful to the denotational semantics takes account of these primtives also.

2.2.3 Auxiliary functions

extend_{R} : U_{R} → L* → U_{R} extend_{R} =

λρ_{R}α* . λν_{1}ν_{2} . ν_{1} = 0 → rev(α*) (ν_{2} − 1), ρ_{R}(ν_{1} − 1)ν_{2}

call : N → P call = λν . λϵϵ*ρ_{R}ψ . #ϵ* = ν → applicate ϵϵ*(single ψ),

wrong “bad stack”

return : P return = λϵϵ*ρ_{R}ψ . ψϵ

make cont : P → N → P → P make cont =

λπ′νπ . λϵϵ*ρ_{R}ψ . #ϵ* = ν → πϵ⟨⟩ρ_{R}(λϵ . π′ϵϵ*ρ_{R}ψ),

wrong “bad stack”

literal : E → P → P literal = λϵ′π . λϵϵ*ρ_{R}ψ . πϵ′ϵ*ρ_{R}ψ

closure : P → P → P closure =

λπ′π . λϵϵ*ρ_{R}ψσ .

π(fix(λϵ . ⟨new σ, λϵ*κ . π′ϵϵ*ρ_{R}(λϵ . κ⟨ϵ⟩)⟩ in E)) ϵ*ρ_{R}ψ(update(new σ) (unspecified in E) σ)

global : L → P → P global =

λαπ . λϵϵ*ρ_{R}ψ .

hold α

(single (λϵ . ϵ ≠ empty in E→ πϵϵ*ρ_{R}ψ,

wrong “undefined variable”))

local : N → N → P → P local =

λν_{1}ν_{2}π . λϵϵ*ρ_{R}ψ .

hold (ρ_{R}ν_{1}ν_{2})

(single (λϵ . ϵ ≠ empty in E→ πϵϵ*ρ_{R}ψ,

wrong “undefined variable”))

set global : L → P → P set global =

λαπ . λϵϵ*ρ_{R}ψ .

assign α ϵ (π (unspecified in E) ϵ*ρ_{R}ψ)

set local : N → N → P → P set local =

λν_{1}ν_{2}π . λϵϵ*ρ_{R}ψ .

assign (ρ_{R}ν_{1}ν_{2}) ϵ (π (unspecified in E) ϵ*ρ_{R}ψ) push : P → P push = λπ . λϵϵ*ρ_{R}ψ . πϵ(ϵ*^{⌢}⟨ϵ⟩)ρ_{R}ψ

make env : N → P → P make env =

λνπ . λϵϵ*ρ_{R}ψ . #ϵ* = ν → tievals (λα* . πϵ⟨⟩(extend_{R} ρ_{R}α*)ψ) ϵ*,

wrong “bad stack”

make rest list : N → P → P make rest list =

λνπ . λϵϵ*ρ_{R}ψ .

#ϵ* ≥ ν →

list (ϵ* † ν)
(single λϵ . πϵ((ϵ*‡ν))ρ_{R}ψ),
wrong “bad stack”

if truish : P → P → P if truish =

λπ_{1}π_{2} . λϵϵ*ρ_{R}ψ . truish ϵ → π_{1}ϵϵ*ρ_{R}ψ, π_{2}ϵϵ*ρ_{R}ψ

check args eq : N → P → P check args eq =

λνπ . λϵϵ*ρ_{R}ψ .

#ϵ* = ν → πϵϵ*ρ_{R}ψ, wrong “bad arg count”

check args ge : N → P → P check args ge =

λνπ . λϵϵ*ρ_{R}ψ .

#ϵ* ≥ ν → πϵϵ*ρ_{R}ψ, wrong “bad arg count”

2.3 Tabular Byte Code Denotational Semantics

In this section, we specify denotational semantics for the Tabular Byte Code tbc.

2.3.1 Semantic functions

Types of the Functions The semantics of the tbc make use of four main semantic functions:

B_{τ} : b ∪ {⟨⟩} → e → U → P
Z_{τ} : z → e → U → P → P
Y_{τ} : y ∪ {⟨⟩} → U → P → P  (The variable y′ ranges over y ∪ {⟨⟩})
T_{τ} : t → U → P

Semantic Clauses for Core Instructions In several of these clauses, we refer to a value in the template table. In the instructions:

     literal, global, and set-global!,

we expect the relevant template table entry to be of one of the forms:

     ⟨constant c⟩ or ⟨global-variable i⟩.

Naturally, it is the value c or i that interests us. Since the tag is the zeroth item in the sequence, we can extract the value by applying the sequence to the argument 1. Hence, these clauses use the expression (e(n))(1) to extract the value from the template table. B_{τ} [[⟨⟩]] = λeρϵϵ*ρ_{R}ψσ . ϵ : R → ϵ | R in A, ⊥ B_{τ} [[⟨⟨return⟩⟩]] == λeρ . return B_{τ} [[⟨⟨call n⟩⟩]] = λeρ . call n B_{τ} [[⟨⟨unless-false b_{1} b_{2}⟩⟩]] = λeρ . if truish(B_{τ} [[b_{1}]]eρ)(B_{τ} [[b_{2}]]eρ) B_{τ} [[⟨make-cont b_{1} n⟩:: b_{2}]] = λeρ . make cont (B_{τ} [[b_{1}]]eρ)n(B_{τ} [[b_{2}]]eρ) B_{τ} [[z:: b]] = λeρ . Z_{τ} [[z]]eρ (B_{τ} [[b]]eρ) Z_{τ} [[⟨unless-false y_{1} y_{2}⟩]] = λeρπ . if truish(Y_{τ} [[y_{1}]]eρπ)(Y_{τ} [[y_{2}]]eρπ) Z_{τ} [[⟨literal n⟩]] = λeρ . literal (K[[(e(n))(1)]]) Z_{τ} [[⟨closure n⟩]] = λeρ . closure (T_{τ} [[e(n)]]ρ) Z_{τ} [[⟨global n⟩]] = λeρ . global (lookup ρ (e(n))(1)) Z_{τ} [[⟨local n_{0} n_{1}⟩]] = λeρ . local n_{0} n_{1} Z_{τ} [[⟨set-global! n⟩]] = λeρ . set global (lookup ρ (e(n))(1))

Z_{τ} [[⟨set-local! n_{0} n_{1}⟩]] = λeρ . set local n_{0} n_{1} Z_{τ} [[⟨push⟩]] = λeρ . push Z_{τ} [[⟨make-env n⟩]] = λeρ . make env n Z_{τ} [[⟨make-rest-list n⟩]] = λeρ . make rest list n Z_{τ} [[⟨unspecified⟩]] = λeρ . literal unspecified in E Z_{τ} [[⟨checkargs= n⟩]] = λeρ . check args eq n Z_{τ} [[⟨checkargs>= n⟩]] = λeρ . check args ge n Y_{τ} [[⟨make-cont y′ n⟩:: b]] = λeρπ . make cont (Y_{τ} [[y′]]eρπ) n (B_{τ} [[b]]eρ) Y_{τ} [[z:: y′]] = λeρπ . Z_{τ} [[z]]eρ (Y_{τ} [[y′]]eρπ) Y_{τ} [[⟨⟩]] = λeρπ . π T_{τ} [[⟨template b e⟩]] = B_{τ} [[b]]e Semantic Clauses for Primitives We will specify the denotational semantics for the most important data manipulation primitives. These are:

     %%cwcc, %%apply, %%eqv, %%set-car!,
     %%car, %%add, and %%cons.

Some other primitives, such as the vector and string primitives, can be easily handled in the same style. However, others, such as the I/O primitives read-char and write-char, are not so easily handled. This is because the official Scheme semantics, from which we have derived our byte code semantics, has not specified how I/O is to be handled. We consider I/O to be easier and more natural to express in the operational framework. In the operational context, the sequence of atomic actions makes it easier to specify the succession of I/O events. Z_{τ} [[⟨%%add⟩]] =

λeρπ . λϵϵ*ρ_{R}ψ .

(λϵ* .

π(sum vals ϵ*)⟨⟩ρ_{R}ψ)

(rev ϵ*)

Z_{τ} [[⟨%%eqv⟩]] = λeρπ . λϵϵ*ρ_{R}ψ . (λϵ* . #ϵ* ≥ 2 →

π((ϵ* 0 = ϵ* 1 → true, false) in E)

⟨⟩ρ_{R}ψ, wrong “bad arg count”)

(rev ϵ*)

Z_{τ} [[⟨%%car⟩]] = λeρπ . λϵϵ*ρ_{R}ψσ . (λϵ* . #ϵ* ≥ 1 →

ϵ* 0 : E_{p} →

π(σ((ϵ* 0 | E_{p})0)) ⟨⟩ρ_{R}ψσ,

wrong “attempt to take car of non-pair”σ, wrong “bad arg count”σ)

(rev ϵ*)

Z_{τ} [[⟨%%cdr⟩]] = λeρπ . λϵϵ*ρ_{R}ψσ . (λϵ* . #ϵ* ≥ 1 →

ϵ* 0 : E_{p} →

π(σ((ϵ* 0 | E_{p})1)) ⟨⟩ρ_{R}ψσ,

wrong “attempt to take cdr of non-pair”σ, wrong “bad arg count”σ)

(rev ϵ*)

Z_{τ} [[⟨%%set-car!⟩]] =

λeρπ . λϵϵ*ρ_{R}ψ . (λϵ* . #ϵ* ≥ 2 →

ϵ* 1 : E_{p} →

(ϵ* 1 | E_{p}) 2 = mutable →

assign((ϵ* 1 | E_{p}) 0)(ϵ* 0)
(π(unspecified in E)⟨⟩ρ_{R}ψ),

wrong “attempt to set car of immutable pair”, wrong “attempt to set car of non-pair”,

wrong “bad arg count”) (rev ϵ*)

Z_{τ} [[⟨%%set-cdr!⟩]] =

λeρπ . λϵϵ*ρ_{R}ψ . (λϵ* . #ϵ* ≥ 2 →

ϵ* 1 : E_{p} →

(ϵ* 1 | E_{p}) 2 = mutable →

assign((ϵ* 1 | E_{p}) 1)(ϵ* 0)

(π(unspecified in E)⟨⟩ρ_{R}ψ), wrong “attempt to set cdr of immutable pair”,

wrong “attempt to set cdr of non-pair”, wrong “bad arg count”)

(rev ϵ*)

Z_{τ} [[⟨%%cons⟩]] = λeρπ . λϵϵ*ρ_{R}ψσ . (λϵ* . #ϵ* ≥ 2 →

(λσ′ .

π⟨new σ, new σ′, mutable⟩ in E

⟨⟩ρ_{R}ψ(update(new σ′)(ϵ* 0)σ′)) (update(new σ)(ϵ* 1)σ),

wrong “bad arg count”σ) (rev ϵ*)

Z_{τ} [[⟨%%apply⟩]] = λeρπ . λϵϵ*ρ_{R}ψσ . (λϵ* . #ϵ* ≥ 2 →

(λϵ*ϵ . call(#ϵ*)ϵϵ*ρ_{R}ψσ)

(list to seq (ϵ* 0) (ϵ* † 1)‡#ϵ* − 2 σ)(ϵ* (#ϵ* − 1)), wrong “bad arg count”σ)

(rev ϵ*)

Z_{τ} [[⟨%%cwcc⟩]] = λeρπ . λϵϵ*ρ_{R}ψσ .

#ϵ* = 1 →

call 1 (ϵ* 0)⟨make escape ψ σ⟩ ρ_{R}ψ

(update (new σ) (unspecified in E) σ), wrong “bad arg count”σ

Auxiliary Functions

sum vals : E* → E sum vals =

fix λf . λϵ* . #ϵ* = 0 → 0, f(ϵ* † 1) + (ϵ* 0) | R

For the definition of the apply primitive operator, we need an auxiliary function list to seq, and for the treatment of call/cc we need make escape.

list to seq : E → E* → S → E* list to seq =

fix λf . λϵϵ*σ .

ϵ = null in E→ ϵ*, ϵ : E_{p} →

f(σ((ϵ | E_{p})1))(σ((ϵ | E_{p})0)) :: ϵ*σ, wrong “apply with improper list”σ

make escape : K_{1} → S → F make escape =

λψσ . ⟨new σ, single arg(λϵκ . ψ ϵ)⟩ in E

single arg : (E → K → C) → (E* → K → C) single arg =

λζϵ*κ . #ϵ* = 1 → ζ(ϵ* 0)κ,

wrong “wrong number of arguments”

3 Byte Code Compiler Algorithm

In this section, we present the algorithm for the compiler, expressed as a translation in a style reminiscent of natural semantics. Interspersed with the translation, we include the Scheme procedures that implement the compiler. We use two programs to maintain the TEX source for this chapter and the Scheme source for the compiler from a single file, following the general approach of Knuth’s “literate programming” [3]. The Scheme programs appear in typewriter font.

The compiler algorithm picks one value for the permute and unpermute functions used in the semantics of Scheme: namely, it uses the function that evaluates arguments left-to-right and then evaluates the procedure last. So permute is the cyclic permutation that advances each sequence element after the first, and places the first element at the end. The unpermute function is its inverse: it places the last element of its argument at the head, and shifts each other lelement back one place. As a result, in operational terms, the argument stack will have the rightmost operand of a combination at its top when the combination’s operator is invoked.

In this chapter, we will use a bar to distinguish variables over the targets of a translation, which are elements of the byte code syntax such as ē, from variables over source expressions, which are Scheme expressions such as e.

We will also refer to syntactic entities in a more concrete and traditional notation that facilitates comparing the clauses of the algorithm with the applicative Scheme procedures that implement it.

(define (compile exp)
  (emit-lap #f (comp-body exp mt-cenv #f)))
(define (compile-library library-exp)
  (emit-lap
   #f
   (append
    primop-initialization-code
    (comp-body library-exp mt-cenv #f))))
(define (comp-body exp cenv name)
  (comp exp cenv 0 name return-code))
(define (comp exp cenv nargs name after)
  (cond ((id? exp)
         (compile-id exp cenv nargs name after))

((self-quoting-constant? exp)
(compile-constant exp cenv nargs name after))
((pair? exp)
(case (car exp)
  ((quote)
   (compile-quote exp cenv nargs name after))
  ((begin)
   (compile-begin (cdr exp) cenv nargs name after))
  ((lambda)
   (compile-lambda exp cenv nargs name after))
  ((if)
   (compile-if exp cenv nargs name after))
  ((set!)
   (compile-set exp cenv nargs name after))
  (else
   (compile-application exp cenv nargs name after))))
(else
(compiler-error 'comp "unrecognized expression" exp))))

3.1 Expressions

(define (compile-constant exp cenv nargs name after)
(compiler-prepend-instruction
(make-instruction 'literal exp)
after))
(define (compile-quote exp cenv nargs name after)
(compiler-prepend-instruction
(make-instruction 'literal (cadr exp))
after))
(define (compile-id exp cenv nargs name after)
(let ((local-ref (lookup exp cenv)))
(if (pair? local-ref)
(compiler-prepend-instruction
(make-instruction 'local (car local-ref) (cdr local-ref))
after)
(compiler-prepend-instruction
(make-instruction 'global exp)
after))))
(define (compile-application exp cenv nargs name after)
(if (return? after)
(let* ((proc (car exp))

     (args (cdr exp))
     (nargs (length args)))
(comp-args args cenv 0 name
           (comp proc cenv nargs name
                 (instruction->code-sequence
                  (make-instruction 'call nargs)))))
(compiler-prepend-instruction
(make-instruction 'make-cont after nargs)
(compile-application exp cenv 0 name return-code))))
(define (compile-lambda exp cenv nargs name after)
(compiler-prepend-instruction
(make-instruction
'closure
(emit-lap
name
(cond ((thunk? exp)
    (compile-thunk exp cenv nargs name))
   ((undotted-lambda? exp)
    (compile-undotted-lambda exp cenv nargs name))
   ((dotted-lambda? exp)
    (compile-dotted-lambda exp cenv nargs name))
   (else (compiler-error
          'compile-lambda "bogus lambda" exp)))))
after))
(define (compile-thunk exp cenv nargs name)
(let ((body (caddr exp)))  ; body is a single form
(comp-entry
0

(comp-body body cenv ; avoid changing environment

        name))))
(define (compile-undotted-lambda exp cenv nargs name)
(let ((formals (cadr exp))

(body (caddr exp))) ; body is a single form

(let ((rev-formals
   (reverse formals)))
(comp-entry
(length rev-formals)
(comp-body
body
(extend-cenv cenv rev-formals)
name)))))

(define (compile-dotted-lambda exp cenv nargs name)
(let ((formals (cadr exp))
(body (caddr exp)))
(let ((rev-formals
   (reverse-proper-or-improper-list formals)))
(comp-rest-entry
(- (length rev-formals)  ; required args
  1)
(comp-body
body
(extend-cenv cenv rev-formals)
name)))))
(define (comp-entry nargs after)
(if (= nargs 0)
(compiler-prepend-instruction
(make-instruction 'check-args= nargs)
after)
(compiler-prepend-instruction
(make-instruction 'check-args= nargs)
(compiler-prepend-instruction
(make-instruction 'make-env nargs)
after))))
(define (comp-rest-entry nargs after)
(let ((unchecked-code
 (compiler-prepend-instruction
  (make-instruction 'make-rest-list nargs)
  (compiler-prepend-instruction
   (make-instruction 'push)
   (compiler-prepend-instruction
    (make-instruction 'make-env (+ 1 nargs))
    after)))))
(if (= nargs 0)

unchecked-code ; no point checking nargs

(compiler-prepend-instruction
 (make-instruction 'check-args>= nargs)
 unchecked-code))))
(define (compile-if exp cenv nargs name after)
(compile-if-or-when
(cadr exp)
(caddr exp)
(cdddr exp)
cenv nargs name after))

(define (compile-alt alt cenv nargs name after)
(if (null? alt)
(compiler-prepend-instruction
(make-instruction 'unspecified)
after)
(comp (car alt) cenv nargs name after)))
(define (compile-if-or-when test con alt
              cenv nargs name after)
(comp test cenv nargs name
(if (return? after)
(instruction->code-sequence
(make-instruction
'unless-false
(comp con cenv nargs name after)
(compile-alt alt cenv nargs name after)))
(compiler-prepend-instruction
(make-instruction
'unless-false
(comp
 con cenv nargs name empty-open-code-sequence)
(compile-alt
 alt cenv nargs name empty-open-code-sequence))
after))))
(define (compile-set exp cenv nargs ignored after)
(let ((name (cadr exp))
(exp (caddr exp)))
(if
(id? name)
(let ((local-ref (lookup name cenv)))
(comp exp cenv nargs name
(if (pair? local-ref)
   (compiler-prepend-instruction
    (make-instruction
     'set-local!
     (car local-ref)
     (cdr local-ref))
    after)
   (compiler-prepend-instruction
    (make-instruction 'set-global! name)
    after))))
(compiler-error
'compile-set "target to set! not identifier: " name))))

3.2 Commands

(define (compile-begin commands cenv nargs name after)
  (let ((first-command (car commands))
        (remaining-commands (cdr commands)))
    (comp first-command cenv nargs name
          (if (null? remaining-commands)
              after
              (compile-begin
               remaining-commands
               cenv nargs name after)))))

3.3 Arguments

(define (comp-args args cenv nargs name after)
  (if (null? args)
      after
      (comp (car args)
            cenv nargs name
            (compiler-prepend-instruction
             (make-instruction 'push)
             (comp-args (cdr args) cenv
                        (+ 1 nargs)
                        name after)))))

3.4 Byte Code Data Type

(define (emit-lap name after) `(lap ,name . ,after))
(define return-code '((return)))
(define empty-open-code-sequence '())
(define (return? code)
  (and (pair? code)
       (eq? (caar code) 'return)))
(define compiler-prepend-instruction cons)
(define make-instruction list)
(define (instruction->code-sequence instruction)
  (list instruction))

3.5 Environments

(define (lookup exp cenv)
  (cond ((not (id? exp))
         (compiler-error
          'lookup
          "expression not an identifier"
          exp))
        ((keyword? exp)
         (compiler-error
          'lookup
          "keyword used as a variable"
          exp))
        (else (lookup-loop exp cenv 0))))
(define (lookup-loop id cenv back)
  (if (null? cenv)
      'not-lexical
      (let loop ((rib (cdr cenv)) (over 1))
        (cond ((null? rib)
               (lookup-loop id (car cenv) (+ 1 back)))
              ((eq? id (car rib)) (cons back over))
              (else (loop (cdr rib) (+ 1 over)))))))
(define extend-cenv cons)
(define mt-cenv '())

A few auxiliary procedures are still needed:

(define (thunk? lambda-exp)
  (null? (cadr lambda-exp)))
(define (undotted-lambda? lambda-exp)
  (proper-list? (cadr lambda-exp)))
(define (dotted-lambda? lambda-exp)
  (not (proper-list? (cadr lambda-exp))))
(define (reverse-proper-or-improper-list p)
  (let loop ((accum '())
             (p p))
    (cond ((pair? p) (loop (cons (car p) accum) (cdr p)))
          ((null? p) accum)
          (else (cons p accum)))))

(define (proper-list? p)
  (or (null? p)
      (and (pair? p)
           (proper-list? (cdr p)))))
(define (keyword? id)
  (memq id '(=> and begin case cond define do else if lambda
             let let* letrec or quasiquote quote set! unquote
             unquote-splicing)))
(define (self-quoting-constant? exp)
  (or (number? exp)
      (boolean? exp)
      (char? exp)
      (string? exp)))
(define (id? exp)
  (and (symbol? exp)
       (not (keyword? exp))))

3.6 Opcode Table and Compiler Support for Primitives

The system needs a table to summarize various pieces of information about the bbc instructions. We also associate a small integer with each operation name; the running image actually contains these integers (each represented in one byte) rather than the operation names.

(define *opcode-info* (make-vector 256 '(error 0)))
(define (define-opcode-info opcode opname num-params)
  (vector-set! *opcode-info* opcode (list opname num-params)))
(define instr-start 0)
(define-opcode-info 0  'call 1)
(define-opcode-info 1  'return 0)
(define-opcode-info 2  'make-cont 3)
(define-opcode-info 3  'literal 1)
(define-opcode-info 4  'closure 1)
(define-opcode-info 5  'global 1)
(define-opcode-info 6  'local 2)
(define-opcode-info 7  'set-global! 1)
(define-opcode-info 8  'set-local! 2)
(define-opcode-info 9  'push 0)
(define-opcode-info 10 'make-env 1)
(define-opcode-info 11 'make-rest-list 1)
(define-opcode-info 12 'unspecified 0)

(define-opcode-info 13 'jump 2)
(define-opcode-info 14 'jump-if-false 2)
(define-opcode-info 15 'check-args= 1)
(define-opcode-info 16 'check-args>= 1)
(define-opcode-info 17 'primitive-throw 0)
(define-opcode-info 18 'empty 0)
(define instr-end 18)
(define prim-start 22)
(define-opcode-info
  22 '%%call-with-current-continuation '(check-args= 1))
(define-opcode-info 23 '%%force-output '(check-args= 1))
(define-opcode-info 24 '%%find-symbol-table '(check-args= 0))
(define-opcode-info 25 '%%* '(check-args>= 0))
(define-opcode-info 26 '%%+ '(check-args>= 0))
(define-opcode-info 27 '%%- '(check-args>= 1))
(define-opcode-info 28 '%%< '(check-args>= 2))
(define-opcode-info 29 '%%= '(check-args>= 2))
(define-opcode-info 30 '%%apply '(check-args>= 2))
(define-opcode-info 31 '%%car '(check-args= 1))
(define-opcode-info 32 '%%cdr '(check-args= 1))
(define-opcode-info 33 '%%char->integer '(check-args= 1))
(define-opcode-info 34 '%%char<? '(check-args= 2))
(define-opcode-info 35 '%%char=? '(check-args= 2))
(define-opcode-info 36 '%%char? '(check-args= 1))
(define-opcode-info 37 '%%close-input-port '(check-args= 1))
(define-opcode-info 38 '%%close-output-port '(check-args= 1))
(define-opcode-info 39 '%%procedure? '(check-args= 1))
(define-opcode-info 40 '%%cons '(check-args= 2))
(define-opcode-info 41 '%%current-input-port '(check-args= 0))
(define-opcode-info 42 '%%current-output-port '(check-args= 0))
(define-opcode-info 43 '%%eof-object? '(check-args= 1))
(define-opcode-info 44 '%%eq? '(check-args= 2))
(define-opcode-info 45 '%%abort '(check-args= 0))
(define-opcode-info 46 '%%integer? '(check-args= 1))
(define-opcode-info 47 '%%input-port? '(check-args= 1))
(define-opcode-info 48 '%%integer->char '(check-args= 1))
(define-opcode-info 49 '%%make-string '(check-args>= 1))
(define-opcode-info 50 '%%make-symbol '(check-args= 1))
(define-opcode-info 51 '%%make-vector '(check-args>= 1))
(define-opcode-info 52 '%%open-input-file '(check-args= 1))
(define-opcode-info 53 '%%open-output-file '(check-args= 1))
(define-opcode-info 54 '%%output-port? '(check-args= 1))
(define-opcode-info 55 '%%pair? '(check-args= 1))
(define-opcode-info 56 '%%peek-char '(check-args>= 0))

(define-opcode-info 57 '%%quotient '(check-args= 2))
(define-opcode-info 58 '%%read-char '(check-args>= 0))
(define-opcode-info 59 '%%remainder '(check-args= 2))
(define-opcode-info 60 '%%set-car! '(check-args= 2))
(define-opcode-info 61 '%%set-cdr! '(check-args= 2))
(define-opcode-info 62 '%%string-length '(check-args= 1))
(define-opcode-info 63 '%%string-ref '(check-args= 2))
(define-opcode-info 64 '%%string-set! '(check-args= 3))
(define-opcode-info 65 '%%string=? '(check-args= 2))
(define-opcode-info 66 '%%string? '(check-args= 1))
(define-opcode-info 67 '%%symbol->string '(check-args= 1))
(define-opcode-info 68 '%%symbol? '(check-args= 1))
(define-opcode-info 69 '%%unspecified '(check-args= 0))
(define-opcode-info 70 '%%error '(check-args= 0))
(define-opcode-info 71 '%%error '(check-args= 0))
(define-opcode-info 72 '%%vector-length '(check-args= 1))
(define-opcode-info 73 '%%vector-ref '(check-args= 2))
(define-opcode-info 74 '%%vector-set! '(check-args= 3))
(define-opcode-info 75 '%%vector? '(check-args= 1))
(define-opcode-info 76 '%%write-char '(check-args>= 1))
(define-opcode-info 77 '%%write-string '(check-args= 2))
(define prim-end 77)

A few auxiliary procedures are used to access the opcode information in the table.

(define (vector-search vector key start end)
  (if (> start end) #f
      (let ((elem (vector-ref vector start)))
        (if (eq? key (car elem))
            (cons start elem)
            (vector-search vector key (+ start 1) end)))))
(define (opname->opcode name)
  (let ((info
         (vector-search *opcode-info* name instr-start prim-end)))
    (if info (car info)
        (compiler-error 'image-builder 'opname->opcode
                        "invalid instruction name" name))))
(define (opcode->opname opcode)
  (car (vector-ref *opcode-info* opcode)))
(define (num-of-opcode-args opcode)
  (if (> opcode instr-end) 0
      (cadr (vector-ref *opcode-info* opcode))))

(define (opcode->argument-checking-code opcode)
(if (and (<= prim-start opcode)
    (<= opcode prim-end))
(cadr (vector-ref *opcode-info* opcode))
(compiler-error
'opcode->argument-checking-code
"opcode out of bounds:" opcode)))

Finally, the compiler uses two procedures to generate the code for the primitives. This code consists of closure instructions that provide the initial procedure values for the Scheme identifiers that access virtual machine primitive operations.

(define (opcode->standard-lap opcode)
(let* ((opname (opcode->opname opcode))
  (argument-checking-code
   (opcode->argument-checking-code opcode)))
`((closure
(lap ,opname ,argument-checking-code (,opname) (return)))
(set-global! ,opname))))
(define primop-initialization-code
(do ((i prim-start (+ i 1))
(primop-initialization-code
 '()
 (append
  (opcode->standard-lap i)
  primop-initialization-code)))
((= i (+ prim-end 1))
primop-initialization-code)))

4 Compiler Correctness

4.1 Syntactic Correctness

In this section, we prove that if the byte code compiler is applied to a syntactically correct Scheme input program, its output is a syntactically correct basic byte code template.

If e is a Scheme expression, we will use C(e) to refer to the result of calling the procedure compile on e. We will also use C(e, ρ_{C}, n, i, w) to refer to the result of calling the procedure comp on e together with the compile-time environment ρ_{C}, the natural number n, the name i, and the after-code w (assumed to be a bbc instruction sequence). We will refer to the empty compile-time environment as mt_{C}. It is the function λν_{1}ν_{2} . not lexical.

Theorem 2 (Compiler syntactic correctness)

1. C(e) is a bbc template t;

2. C(e, ρ_{C}, n, i, b_{0}) is a bbc closed instruction sequence b_{1};

3. C(e, ρ_{C}, n, i, y_{0}) is a bbc open instruction sequence y_{1};

4. C(e, ρ_{C}, n, i, ⟨⟩) is a bbc open instruction sequence y_{1}.

Proof. The proof is by simultaneous structural induction on the Scheme syntax.

1. Since the return code, ⟨⟨return⟩⟩, is a closed instruction list b_{0},

C(e) = ⟨lap false C(e, mt_{C}, false, b_{0})⟩

IH clause 2 entails that C(e, mt_{C}, false, b_{0}) is a closed instruction list b_{1}, so ⟨lap false b_{1}⟩ is a syntactically correct template.

2. C(e, ρ_{C}, n, i, b_{0}) is the result of calling one of eight procedures on the same arguments (or in the case of compile-begin, on the embedded sequence of commands). Hence the case follows from the eight lemmas below.

3. C(e, ρ_{C}, n, i, y_{0}) is the result of calling one of eight procedures on the same arguments (or in the case of compile-begin, on the embedded sequence of commands). Hence the case follows from the eight lemmas below.

4. C(e, ρ_{C}, n, i, ⟨⟩) is the result of calling one of eight procedures on the same arguments (or in the case of compile-begin, on the embedded sequence of commands). Hence the case follows from the eight lemmas below.

In the following eight lemmas, we will use Ccategory to refer to the result, for suitable arguments, of applying the compilation procedure for a particular syntactic category. For instance, Cid is the procedure to compile an identifier, with auxiliary arguments ρ_{C}, n, i, w_{0} or ρ_{C}, n, i, ⟨⟩. We will slightly abuse notation by letting w_{0} stand for any open or closed instruction sequence or else ⟨⟩. By “the right syntactic category,” we will mean a closed instruction list if the last argument is a closed instruction list, and an open instruction list if the last argument is either a closed instruction list or else ⟨⟩.

Lemma 3 (Compile Identifier)

1. Cid(i, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cid(i, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cid(i, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof. Since lookup returns a pair ⟨n_{1}, n_{2}⟩ of natural numbers if it returns a pair, ⟨local n_{1} n_{2}⟩ is a neutral instruction z. ⟨global i⟩ is also a neutral instruction z. So the result is an instruction sequence of the right syntactic class, namely (respectively):

1. z:: b_{0};

2. z:: y_{0};

3. z:: ⟨⟩ = ⟨z⟩.

Lemma 4 (Compile Constant)

1. Cconstant(c_{sq}, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cconstant(c_{sq}, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cconstant(c_{sq}, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}

Proof. Similar.

Lemma 5 (Compile Quote)

1. Cquote(⟨quote c⟩, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cquote(⟨quote c⟩, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cquote(⟨quote c⟩, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof. Similar.

Lemma 6 (Compile Begin)

Suppose that Theorem 2 holds for all proper subexpressions of

e = ⟨begin⟩^{⌢}e^{+},

and all instruction sequences b_{0}, y_{0}, or ⟨⟩. Then:

1. Cbegin(e^{+}, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cbegin(e^{+}, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cbegin(e^{+}, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1};

Proof. The proof is by induction on e^{+}.

The base case e* = ⟨e_{0}⟩ holds:

Cbegin(⟨e_{0}⟩, ρ_{C}, n, i, w_{0}) = C(e_{0}, ρ_{C}, n, i, w_{0}),

which by the assumption that Theorem 2 holds is of the right syntactic category.

Otherwise, e* = e_{0} :: e_{1}^{+}, and the induction hypothesis is that

Cbegin(e_{1}^{+}, ρ_{C}, n, i, w_{0})

is of the same syntactic class as w_{0}. But

Cbegin(e_{0} :: e_{1}^{+}, ρ_{C}, n, i, w_{0}) = C(e_{0}, ρ_{C}, n, i, Cbegin(e_{1}^{+}, ρ_{C}, n, i, w_{0})).

Hence, applying clause 2 or 3 of Theorem 2 to the proper subexpression e_{0}, we may infer that this belongs to the same syntactic class as its last argument, which by the induction hypothesis is the right syntactic class.

Lemma 7 (Compile Lambda)

Suppose that Theorem 2 holds for all proper subexpressions of

e = ⟨lambda i* e_{0}⟩,

all values ρ′_{C}, and all instruction sequences w. Then:

1. Cλ(e, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cλ(e, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cλ(e, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof. Since Cλ simply prepends a closure instruction to its last argument, it suffices to ensure that each branch of the embedded conditional returns a closed instruction list b_{λ} when called with arguments e, ρ_{C}, n, i.

First note that if comp-entry or comp-rest-entry is called with a natural number and after code w_{0}, then it returns a code sequence w_{1} of the right syntactic category. This is because the procedures simply prepend neutral instructions.

1. e is a thunk (i.e. a procedure with zero parameters) ⟨lambda ⟨⟩ e_{0}⟩:

In this case we call comp-entry on the result of calling comp-body with arguments e_{0}, ρ_{C}, i. As the latter returns C(e_{0}, ρ_{C}, 0, i, ⟨⟨return⟩⟩), we may apply Theorem 2 to the subexpression e_{0}.

2. e is an undotted lambda expression ⟨lambda I* e_{0}⟩:

Similar, except that a different lexical environment argument ρ′_{C} is passed into comp-body.

3. e is a dotted lambda expression ⟨dotted lambda I^{+} e_{0}⟩:

Similar to the preceding, except that that comp-rest-entry is called, and the reversed formals and number of arguments are computed slightly differently.

Lemma 8 (Compile If)

Suppose that Theorem 2 holds for all proper subexpressions of

e = ⟨if⟩^{⌢}e*,

and all instruction sequences w. Then:

1. Cif(e, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cif(e, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cif(e, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof.

1. We will divide this into four cases, depending whether the conditional has an alternative, and whether the after-code b_{0} = ⟨⟨return⟩⟩ or not.

(a) Consider first the case in which e = ⟨if e_{0} e_{1} e_{2}⟩ and b_{0} =

⟨⟨return⟩⟩.

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨e_{2}⟩, ρ_{C}, n, i, b_{0})
= C(e_{0}, ρ_{C}, n, i,

                        ⟨⟨unless-false

C(e_{1}, ρ_{C}, n, i, b_{0})

Calt(⟨e_{2}⟩, ρ_{C}, n, i, b_{0})⟩⟩)

= C(e_{0}, ρ_{C}, n, i,

                        ⟨⟨unless-false

C(e_{1}, ρ_{C}, n, i, b_{0}) C(e_{2}, ρ_{C}, n, i, b_{0})⟩⟩)

We now apply Theorem 2 Case 2 to the subexpressions e_{1} and e_{2}, inferring that

⟨⟨unless-false C(e_{1}, ρ_{C}, n, i, b_{0}) C(e_{2}, ρ_{C}, n, i, b_{0})⟩⟩

is a closed instruction sequence b_{1}. We next apply the theorem (again, Case 2) to e_{0} (and the after-code b_{1}).

(b) Consider next the case in which e = ⟨if e_{0} e_{1} e_{2}⟩, but b_{0} ≠

⟨⟨return⟩⟩.

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨e_{2}⟩, ρ_{C}, n, i, b_{0})
= C(e_{0}, ρ_{C}, n, i,

                        ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩)

Calt(⟨e_{2}⟩, ρ_{C}, n, i, ⟨⟩)⟩ :: b_{0})

= C(e_{0}, ρ_{C}, n, i,

                        ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩) C(e_{2}, ρ_{C}, n, i, ⟨⟩)⟩

:: b_{0})

We now apply Theorem 2 Case 4 to the subexpressions e_{1} and e_{2}, inferring that

⟨unless-false C(e_{1}, ρ_{C}, n, i, ⟨⟩) C(e_{2}, ρ_{C}, n, i, ⟨⟩)⟩

is a neutral instruction z, so that z:: b_{0} is a closed instruction sequence b_{1}. We next apply the theorem (again, Case 2) to e_{0} (and the after-code b_{1}).

(c) Consider next the case in which e = ⟨if e_{0} e_{1}⟩, and b_{0} =

⟨⟨return⟩⟩.

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨⟩, ρ_{C}, n, i, b_{0})
= C(e_{0}, ρ_{C}, n, i,

                         ⟨⟨unless-false

C(e_{1}, ρ_{C}, n, i, b_{0}) Calt(⟨⟩, ρ_{C}, n, i, b_{0})⟩⟩)

= C(e_{0}, ρ_{C}, n, i,

                         ⟨⟨unless-false

C(e_{1}, ρ_{C}, n, i, b_{0})

                           ⟨unspecified⟩:: b_{0}⟩⟩)

The remainder of this case is similar to 1(a).

(d) Consider finally the case in which e = ⟨if e_{0} e_{1}⟩, and b_{0} ≠

⟨⟨return⟩⟩.

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨⟩, ρ_{C}, n, i, b_{0})
= C(e_{0}, ρ_{C}, n, i,

                         ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩) Calt(⟨⟩, ρ_{C}, n, i, ⟨⟩)⟩

:: b_{0})

= C(e_{0}, ρ_{C}, n, i,

                             ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩)

                               ⟨⟨unspecified⟩⟩⟩

:: b_{0})

The remainder of this case is similar to 1(b).

2,3. In the remaining cases, in which the after-code w_{0} is either an open instruction sequence y_{0} or else ⟨⟩, we need not consider the possibility that w_{0} = ⟨⟨return⟩⟩. Thus when e = ⟨if e_{0} e_{1} e_{2}⟩, we have:

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨e_{2}⟩, ρ_{C}, n, i, w_{0})
= C(e_{0}, ρ_{C}, n, i,

                          ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩) Calt(⟨e_{2}⟩, ρ_{C}, n, i, ⟨⟩)⟩

:: w_{0})

= C(e_{0}, ρ_{C}, n, i,

                          ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩) C(e_{2}, ρ_{C}, n, i, ⟨⟩)⟩

:: w_{0})

We now apply Theorem 2 Case 4 to the subexpressions e_{1} and e_{2}, inferring that

⟨unless-false C(e_{1}, ρ_{C}, n, i, ⟨⟩) C(e_{2}, ρ_{C}, n, i, ⟨⟩)⟩

is a neutral instruction z, so that z:: w_{0} is an open instruction sequence y_{0}. We apply Clause 3 of the theorem. Finally, when e = ⟨if e_{0} e_{1} e_{2}⟩:

Cif(e, ρ_{C}, n, i, w_{0}) = Cif-or-when(e_{0}, e_{1}, ⟨⟩, ρ_{C}, n, i, w_{0})

= C(e_{0}, ρ_{C}, n, i,

                                ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩) Calt(⟨⟩, ρ_{C}, n, i, ⟨⟩)⟩

:: w_{0})

= C(e_{0}, ρ_{C}, n, i,

                                ⟨unless-false

C(e_{1}, ρ_{C}, n, i, ⟨⟩)

                                  ⟨⟨unspecified⟩⟩⟩

:: w_{0})

Since ⟨unless-false C(e_{1}, ρ_{C}, n, i, ⟨⟩) ⟨⟨unspecified⟩⟩⟩ is a neutral instruction z, z:: w_{0} is an open instruction sequence y_{0}. We again apply Clause 3 of the theorem.

Lemma 9 (Compile Set!)

Suppose that Theorem 2 holds for all proper subexpressions of

e = ⟨set! i e_{0}⟩,

and all instruction sequences w. Then:

1. Cset!(e, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Cset!(e, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Cset!(e, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof. Since lookup returns a pair ⟨n_{1}, n_{2}⟩ of natural numbers if it returns a pair, ⟨set-local! n_{1} n_{2}⟩ is a neutral instruction z. ⟨set-global! i⟩ is also a neutral instruction z. So z:: w_{0} is an instruction sequence of the right syntactic class. Hence, we may apply Clause 2 or Clause 3 of Theorem 2 to the subexpression e with the aftercode z:: w_{0}.

Lemma 10 (Compile Application)

Suppose that Theorem 2 holds for all proper subexpressions of

e = e_{0} :: e*,

and all instruction sequences w. Then:

1. Capplication(e, ρ_{C}, n, i, b_{0}) is a closed instruction list b_{1};

2. Capplication(e, ρ_{C}, n, i, y_{0}) is an open instruction list y_{1};

3. Capplication(e, ρ_{C}, n, i, ⟨⟩) is an open instruction list y_{1}.

Proof. First assume that the after-code w_{0} = ⟨⟨call n⟩⟩. Since the latter is a closed instruction sequence, we may apply Theorem 2, Clause 2 to infer that C(e_{0}, ρ_{C}, n, i, ⟨⟨call n⟩⟩) is a closed instruction list b. To prove that Cargs(e*, ρ_{C}, n, i, b) is a closed instruction list, we argue by induction on e*.

Cargs(⟨⟩, ρ_{C}, n, i, b) = b.

Moreover, let e* = e_{1} :: e_{1}*. Then

Cargs(e_{1} :: e_{1}*, ρ_{C}, n, i, b) = C(e_{1}, ρ_{C}, n, i, ⟨push⟩:: Cargs(e_{1}*, ρ_{C}, n + 1, i, b)).

Inductively, the latter is of the form C(e_{1}, ρ_{C}, n, i, ⟨push⟩:: b′), so we may apply Theorem 2, Clause 2.

Next suppose that the after-code w_{0} is an instruction sequence other than ⟨⟨call n⟩⟩. Then

Capplication(e, ρ_{C}, n, i, w_{0})

is of the form:

⟨make-cont w_{0} n⟩:: Capplication(e, ρ_{C}, 0, i, ⟨⟨call n⟩⟩).

Since we have just seen that the latter evaluates to a closed instruction list b_{1}, we may infer that ⟨make-cont w_{0} n⟩:: b_{1} is an instruction list, and of the same syntactic class as w_{0}.

Finally, suppose the after-code is ⟨⟩. Then Capplication(e, ρ_{C}, n, i, w_{0}) is of the form:

⟨make-cont ⟨⟩ n⟩:: Capplication(e, ρ_{C}, 0, i, ⟨⟨call n⟩⟩).

We may again infer that the latter is of the form b_{1}, so that

                       ⟨make-cont ⟨⟩ n⟩:: b_{1}

is an open instruction list.

4.2 Semantic Correctness

In this section, we prove that the byte code compiler preserves meaning.

Unfortunately, there is a sort of semantic mismatch between Scheme and the bbc language. The official semantics for Scheme allows a procedure to return several values to its caller, as would be needed to model the Common Lisp (values ...) construct or the T (return ...) form. However, Scheme has no construct that allows a programmer to construct a procedure that would return more than one value. Assuming that a program is started with an initial store that hides no “multiple value returners,” then an implementation may assume that there will never be any in the course of execution. Moreover, the Scheme standard procedures as defined in ieee report [2], which are the natural procedures to supply as denizens of the initial store, do not involve anything of that kind. So many implementations of Scheme, among them Vlisp, do not support multiple return values.

Still, it is far from trivial to formalize reasoning that justifies an implementation in assuming it need implement only “single-valued” objects, and make no provision for multiple value returns. In this section, we will attempt to do so.

In essence our approach is to introduce a new, “smaller” semantics for Scheme. In this semantics, it is clear that there is no mechanism for multiple return values. The semantics is “smaller” in the sense that domains, such as the domain of expressed values, are subsets of the corresponding domains in the official semantics. They contain only the objects needed for singlevalue returning procedures. Although we will formally express the semantic functions of the alternate semantics in terms of the same domains that the standard semantics uses, it will be clear that the alternate semantics really only depends on the smaller domains of “single-valued” objects. We use the old domains in the definitions in order to facilitate a comparison between the two semantic theories.

With this alternate semantics in place, there are two separate facts that must be proved to justify the compiler algorithm.

1. The alternate semantics is faithful to the standard semantics, at least in the intended case in which the initial givens harbor no multiple value returns:

E[[e]]ρ κ σ = (sva E)[[e]]ρ κ σ,

when κ and σ, the halt continuation and the initial store respectively, are unproblematic, single-valued objects in a sense to be defined below.

ϕ_{p} ^{∈} F_{p} = E* → K → C pure (untagged) procedure values

Table 6: Pure Procedure Objects

2. The compiled byte code is faithful to the alternate semantics, in the

sense that

(sva E)[[e]]ρ and B[[C(e)]]ρ

yield the same computational answer when applied to suitable initial values.

We will also (for convenience) introduce a new explicitly defined domain of pure procedure objects. Unlike the procedure objects in F (which equals L × (E* → K → C)), those in F_{p} contain only the function-like part (namely E* → K → C), without the location that serves as a tag (see Table 6). The location tags are used to decide whether two procedure objects are the same in the sense of the Scheme standard procedure eqv?. So F = L × F_{p}. It will also be convenient to define a few auxiliary functions:

Definition 11 (Auxiliaries)

1. zeroth : E* → E is the strict function returning ⊥_{E} if its argument ϵ* is either ⊥_{_{E}*} or ⟨⟩, and which returns (ϵ* 0) otherwise.

2. truncate : E* → E* is the non-strict function which takes its argument ϵ* to ⟨zeroth ϵ*⟩. Hence #(truncate ϵ*) = 1, even for ϵ* = ⊥_{_{E}*}.

3. one arg : K → K_{1} is defined to equal λκϵ . κ⟨ϵ⟩

4. multiple : K_{1} → K is defined to equal λψϵ* . ψ(zeroth ϵ*)

The auxiliaries one arg and multiple coerce from K to K_{1} and back. The name truncate is quite long, and we sometimes prefer to truncate it as trunc. Expanding the definitions, we have:

Lemma 12 1. one arg(multiple ψ) = ψ;

2. multiple(one arg κ) = λϵ* . κ(truncate ϵ*).

We define next the function sva, which, given any object in Ω, returns the single-valued object that approximates it. As we will soon see, sva ω always belongs to the same summand of Ω as ω. Moreover, sva is idempotent, so that we can think of its range as determining the single-valued objects. We will extend sva immediately after defining it so that it may be applied to elements of the disjoint summands of Ω, in addition to the elements of Ω itself.

The heart of sva is its behavior on pure procedure objects ϕ_{p}. A pure procedure object ϕ_{p} is altered to another function ϕ′_{p}, such that ϕ′_{p} calls ϕ_{p} with the same expressed value arguments and the same store. Only the continuation argument is altered, to ensure that the modified continuation can access only one expressed value, and only a single-valued approximation to that. Similarly, in virtue of the clause for functional objects including expression continuations, only a single-valued approximation to the contents of the new store is made available. Crudely put, ϕ′_{p} cannot pass anything infected with multiple values to its continuation, whether in the store, or by making available more than one return value itself, or by hiding it in a procedure value that would later, when applied, make more than one value available to its continuation.

As for the uncontroversially given domains that do not involve E, sva is the identity. For all other domains, sva commutes in the obvious way with the constructor of the domain.

Recall that we assume E to be indecomposable, and F = L×F_{p}. We define Ω to be the disjoint sum (in any order) of a set C_{Ω} of domains, where C_{Ω} is the least set containing all of the Scheme denotational domains (including E_{Σ}) and such that

1. every argument of every element of C_{Ω} is an element of C_{Ω}, and

2. if D is constructed by a basic constructor from a finite sequence of arguments in C_{Ω}, then D is an element of C_{Ω}.

Given f : Ω → Ω, say that f respects types if f is strict and for every D in C_{Ω} and every x in Ω such that x : D, we have fx : D; also, for each D in C_{Ω}, let f^{D} : D → D be defined, for d ∈ D, to be

f^{D}d = (f(d in Ω)) |D.

As a preliminary step towards single-valued approximations, define an operator α : (Ω → Ω) → (Ω → Ω) as follows. Let f : Ω → Ω and ω ∈ Ω be arbitrary. Then αfω is (a) if ω = ⊥_{Ω}, then ω

(b) if ω : D for an indecomposable D other than E, then ω,

(c) if ω : E, then

(ψE^{−1}(f(ψ_{E}(ω|E) in Ω)|E_{Σ})) in Ω,

(d) if ω : D for a decomposable D other than F_{p}, then associate with each argument D_{i} of D the functional f^{D_{i}} : D_{i} → D_{i}, lift these to g : D → D, and take g(ω|D) in Ω, and

(e) if ω : F_{p}, then

(λϵ*κ . (ω | F_{p}) (f^{^{E}*} ϵ*) (λϵ* . (f^{C}(κ (truncate (f^{E} ∘ ϵ*)))))) in Ω,

(here (f^{E} ∘ ϵ*) is taken to be ⊥_{_{E}*} for ϵ* = ⊥_{_{E}*})

Note that all of the real work of α is done by the truncation in the last case. It is important to note that in all cases if ω : D, then αfω : D; as αf is strict we see that for all f : Ω → Ω, αf respects types.

Definition 13 (Single-valued approximation) sva : Ω → Ω is the least fixed point of the above α.

For D ∈ C_{Ω} and d ∈ D, we will abuse notation by writing sva d for sva^{D} d, i.e., for (f(d in Ω)|D).

Lemma 14 sva is idempotent.

Proof. If we let f_{0} = ⊥_{Ω→Ω}, and f_{n+1} = αf_{n}, then sva is the supremum of the f_{n} for n ∈ N. Define a strict g_{0} : Ω → Ω by letting g_{0} ω = ⊥_{D} in Ω whenever ω : D (so each g_{0}^{D} = ⊥_{D→D}). Then g_{0} is least type-respecting element of Ω → Ω.

Since f_{1} respects types, f_{0} ⊑ g_{0} ⊑ f_{1}. Also let g_{n+1} = αg_{n}. As g_{1} respects types, g_{0} ⊑ g_{1}. Hence each g_{n} ⊑ g_{n+1}, and the supremum of the g_{n}’s is also sva.

For h : Ω → Ω, let P (h) mean that

(i) h respects types;

(ii) each h^{D} is strict; and

(iii) h is idempotent.

It is easy to see that the supremum of idempotent elements of Ω → Ω is idempotent, and that P (g_{0}) holds. It suffices to establish that α preserves the property P.

Take an arbitrary f such that P (f) and let h be αf. We already know that (i) holds.

For (ii) consider cases on D. The case of an indecomposable D other than E is trivial. To compute h^{E}⊥_{E} we apply case (c) of the definition of αf with ω = ⊥_{E} in Ω. Projecting this ω to E yields ⊥_{E}; applying ψ^{−1} to that yields ⊥_{E_{Σ}}. We now use the assumption that f is strict on E_{Σ}, and end up with ⊥_{E}. For D decomposable other than F_{p}, the definition of lifting shows that a strict functional is produced if all the arguments’ functionals are strict, which is the case here. The case of ⊥_{F_{p}} is easy from the explicit λ term used in this case of the definition of α. This establishes that (ii) of P holds for h.

For idempotence of h, pick an arbitrary ω ∈ Ω, and consider the various cases in the definition of hω. For (a) and (b) there is no problem. For (c) we need to use the fact that f respects types. Each of the subcases of (d) is easy.

For (e), let ω : F_{p}; we must show that (α f)(α f ω) = (α f ω). By (e), the former (projected into F_{p} for convenience) equals:

λϵ*κ . (λϵ*κ . (ω | F_{p})(f^{^{E}*}ϵ*)(λϵ_{0}* . f^{C}(κ(trunc(f^{E} ∘ ϵ_{0}*)))))

(f^{^{E}*}ϵ*)(λϵ_{1}* . f^{C}(κ(trunc(f^{E} ∘ ϵ_{1}*))))
= λϵ*κ . (ω | F_{p})(f^{^{E}*}(f^{^{E}*}ϵ*))

(λϵ_{0}* . f^{C}((λϵ_{1}* . f^{C}(κ(trunc(f^{E} ∘ ϵ_{1}*))))(trunc(f^{E} ∘ ϵ_{0}*))))

= λϵ*κ . (ω | F_{p})(f^{^{E}*}(f^{^{E}*}ϵ*))
(λϵ_{0}* . f^{C}(f^{C}(κ(trunc(f^{E} ∘ (trunc(f^{E} ∘ ϵ_{0}*)))))))
= λϵ*κ . (ω | F_{p})(f^{^{E}*}ϵ*)
(λϵ_{0}* . f^{C}(κ(trunc(f^{E} ∘ (trunc(f^{E} ∘ ϵ_{0}*)))))),

We have used β-reduction in the first two steps, and the idempotence of f and therefore also f^{D} in the third. So it suffices to prove that

trunc(f^{E} ∘ (trunc(f^{E} ∘ ϵ_{0}*))) = trunc(f^{E} ∘ ϵ_{0}*)

Now if 0 < #ϵ_{0}*, the idempotency of f and therefore also f^{E} suffices, as the equation reduces to

⟨f^{E}(f^{E}(ϵ_{0}* 0))⟩ = trunc(f^{E} ∘ ϵ_{0}*)

On the other hand if ϵ_{0}* is either ⊥_{_{E}*} or ⟨⟩, then we have:

trunc(f^{E} ∘ (trunc⊥_{_{E}*})) = trunc(f^{E} ∘ ⟨⊥_{E}⟩)
= trunc⟨⊥_{E}⟩
= ⟨⊥_{E}⟩

using the definitions of α and of truncate, and the strictness of f^{E} (clause (ii) of P). Moreover,

trunc(f^{E} ∘ ⊥_{_{E}*}) = trunc⊥_{_{E}*}
= ⟨⊥_{E}⟩

QED.

4.2.1 Single-valued Scheme Semantics

By the convention that (sva x) = x when x belongs to a syntactic domain such as the Scheme expressions, we may apply sva to the semantic functions K, E, E*, and C. Since Scheme has no syntax for constants denoting procedure objects, both c and K[[c]] are necessarily single-valued, so that (sva K) = K. However, the remaining semantic functions are not single valued, and the alternative semantics consists in replacing them with their single-valued approximations (sva E), (sva E*), and (sva C).

Faithfulness of the Alternative Semantics The alternative semantics is faithful in the sense that, for every Scheme expression e, it delivers the same computational answer as the official semantics, provided that a singlevalued initial continuation and store are supplied. As mentioned previously, it is reasonable for a Scheme implementation to provide a single-valued store. Moreover, many natural initial continuations (which, intuitively, say how to extract the computational answer if the program finally halts) are singlevalued. For instance, the Vlisp operational semantics for the Tabular Byte Code Machine is justified against the denotational semantics using the initial continuation:

halt = λϵ*σ . (ϵ* 0) : R → (ϵ* 0) | R in A, ⊥

which is single-valued.

Theorem 15 (Faithfulness of Alternative Semantics)

1. For all Scheme expressions e, environments ρ, expression continuations κ, and stores σ,

(sva E)[[e]]ρ κ σ = E[[e]]ρ (sva κ) (sva σ)  (1)

2. Let κ = sva κ and σ = sva σ. Then

E[[e]]ρ κ σ = (sva E)[[e]]ρ κ σ

Proof. 1. We simply use the definition of sva, together with the fact that the domain of Scheme expressions, the domain of environments, and the domain of answers do not involve E:

(sva E)[[e]]ρ κ σ = (sva(E[[sva e]]))ρ κ σ
= (sva(E[[e]](sva ρ))) κ σ
= (sva(E[[e]]ρ (sva κ))) σ
= (sva(E[[e]]ρ (sva κ) (sva σ)))
= (E[[e]]ρ (sva κ) (sva σ))

2. We use the assumption that κ and sigma are single-valued, followed by Equation 1, from right to left:

E[[e]]ρ κ σ = E[[e]]ρ (sva κ) (sva σ)
= (sva E)[[e]]ρ κ σ

QED

Corollary 16 For all values of e, ρ, κ, and σ:

(sva E)[[e]]ρ κ σ = (sva E)[[e]]ρ (sva κ) σ
= (sva E)[[e]]ρ κ (sva σ)
= (sva E)[[e]]ρ (sva κ) (sva σ)

Proof. Using Equation 1, the idempotence of sva on continuations, and then Equation 1 again, from right to left, we have:

(sva E)[[e]]ρ κ σ = E[[e]]ρ (sva κ) (sva σ)
= E[[e]]ρ (sva (sva κ)) (sva σ)
= (sva E)[[e]]ρ (sva κ) σ

The other assertions are similar, using also the idempotence of sva on stores. QED Corollary 17 For all values of e, ρ, κ, and σ, if κ ∼ κ′ and σ ∼ σ′, then

(sva E)[[e]]ρ κ σ = (sva E)[[e]]ρ κ′ σ′

Proof of Corollary 17. Simply apply Corollary 16 to each of κ, σ and κ′, σ′, and use the facts that (svaκ) = (svaκ′) and (svaσ) = (svaσ′). QED

Truncating Continuations and eliminating “Single” A further partial justification for the single-valued semantics that we have introduced is that it allows us to eliminate the operator single from the semantic clauses in which it occurs, and to truncate any continuation. These two facts are intuitively significant, as they amount to saying that the meaning of a Scheme expression, if it invokes its expression continuation at all, applies it to a sequence ⟨ϵ⟩ of length 1. Hence they justify the claim that the alternate semantics ensures that procedures never return multiple values.

Theorem 18 (Truncate Continuations)

(sva E)[[E]]ρ κ = (sva E)[[E]]ρ (λϵ* . κ (truncate ϵ*))

Proof. The proof is by induction on E. The cases where E is a constant, an identifier, a lambda expression, a dotted lambda expression, or an assignment are immediate from the definitions of send and hold. The cases for two- and three-expression if, and for begin, are immediate from the induction hypothesis. Hence the only case of interest is for procedure call, which is as it should be.

To prove

(sva E)[[⟨E_{0}⟩^{⌢}E*]]ρ κ = (sva E)[[⟨E_{0}⟩^{⌢}E*]]ρ (λϵ* . κ (truncate ϵ*))

we must show that

(sva E*)(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) κ)

(unpermute ϵ*)))

equals

(sva E*)(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) (λϵ* . κ (truncate ϵ*)))

(unpermute ϵ*))).

Pushing svas through the left hand side, we obtain:

E*(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (svaκ)(truncate ϵ*))))

(sva(unpermute (svaϵ*)))))

On the right hand side, we obtain:

E*(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (λϵ* . sva(κ (sva(truncate ϵ*))))

(truncate ϵ*))))

(sva(unpermute (svaϵ*))))).

For these two expressions to be equal, it certainly suffices that for all κ,

λϵ* . (svaκ)(truncate ϵ*) = λϵ* . (λϵ* . sva(κ (sva(truncate ϵ*))))(truncate ϵ*)

Using the definition of sva, we have:

λϵ* . (svaκ)(truncate ϵ*) = λϵ* . sva(κ(sva(truncate ϵ*)))

On the other hand,

λϵ* . (λϵ* . sva(κ (sva(truncate ϵ*))))(truncate ϵ*)

= λϵ* . sva(κ (sva(truncate (truncate ϵ*))))
= λϵ* . sva(κ (sva(truncate ϵ*)))

QED.

Theorem 19 (“Single” eliminable)

(sva E)[[E]]ρ (single ψ) = (sva E)[[E]]ρ (λϵ* . ψ (ϵ* 0))

Proof. The (very similar) proof is by induction on E. The cases where E is a constant, an identifier, a lambda expression, a dotted lambda expression, or an assignment are immediate from the definitions of send and hold. The cases for two- and three-expression if, and for begin, are immediate from the induction hypothesis. Hence the only case of interest is for procedure call, which again is as it should be.

To prove

(sva E)[[⟨E_{0}⟩^{⌢}E*]]ρ (single ψ) = (sva E)[[⟨E_{0}⟩^{⌢}E*]]ρ (λϵ* . ψ (ϵ* 0)) we must show that (sva E*)(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) (single ψ))

(unpermute ϵ*)))

equals (sva E*)(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . applicate (ϵ* 0) (ϵ* † 1) (λϵ* . ψ (ϵ* 0)))

(unpermute ϵ*))).

Pushing svas through the left hand side, we obtain: E*(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (sva(single ψ))(truncate ϵ*))))

(sva(unpermute (svaϵ*)))))

On the right hand side, we obtain: E*(permute(⟨E_{0}⟩^{⌢}E*))

ρ

(λϵ* . ((λϵ* . sva(applicate (sva(ϵ* 0)) (sva(ϵ* † 1))

(λϵ* . (λϵ* . sva(ψ (sva(ϵ* 0))))(truncate ϵ*))))

(sva(unpermute (svaϵ*))))).

For these two expressions to be equal, it certainly suffices that for all ϵ, ϵ* and ψ, λϵ*.(sva(singleψ))(truncateϵ*) = λϵ*.(λϵ*.sva(ψ (sva(ϵ*0))))(truncateϵ*) By β-reduction, the right hand side equals:

(λϵ* . sva(ψ (sva((truncate ϵ*) 0))))

Using the definitions of single and sva, and then β-reduction, we have, for the left hand side (using w to abbreviate (svawrong“”)):

(λϵ* . (sva(single ψ))(truncate ϵ*))

= (λϵ* . (sva(λ ϵ* . #ϵ* = 1 → ψ(ϵ* 0), wrong“”))(truncate ϵ*))
= (λϵ* . (λ ϵ* . #svaϵ* = 1 → sva(ψ((svaϵ*) 0)), w)(truncate ϵ*))
= (λϵ* . #(sva(truncate ϵ*)) = 1 → sva(ψ((sva(truncate ϵ*)) 0)), w)

Since truncate always returns a sequence of length 1, and sva does not affect length, the body of the latter equals sva(ψ((sva(truncateϵ*))0)). The proof is complete, because ((sva(truncate ϵ*)) 0) = sva((truncate ϵ*) 0). QED

4.2.2 Compiler Correctness for Single-valued Semantics

We will prove that if e is any Scheme program and b is the result of compiling it, then e and b are equivalent in the following sense:

Definition 20 (Computational equivalence ≡)

A Scheme program e and a byte code program b are computationally equivalent if, for every environment ρ and expression continuation κ,

(sva E)[[e]]ρκ = (svaB)[[b]]ρ unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

Definition 21 (Environment Composition)

Suppose ρ is an environment,

ρ_{C} : Ide → (N × N ∪ {not lexical})

is a “compile-time environment,” and

ρ_{R} : N → N → L

is a “run-time environment.”

Then their environment composition ρ◁_{ρ_{C}}^{ρ_{R}} is the environment:

λi . ρ_{C} i = not lexical → ρ i, (λp . ρ_{R} (p 0)(p 1))(ρ_{C} i)

Lemma 22 ρ◁mt_{C}^{ρ_{R}} = ρ.

Proof. For all i, mt_{C} i = not lexical. Hence, ρ◁mt_{C}^{ρ_{R}} i = ρ i, and, by extensionality, ρ◁mt_{C}^{ρ_{R}} = ρ. QED

We state the main theorem next, and we will give its (short) proof using Lemma 25, which is due to Will Clinger [1]. The bulk of the (long) proof of Clinger’s lemma, for the Vlisp compiler, is given below.

Theorem 23 (Compiler correctness)

For any Scheme expression e and environment ρ,

e ≡ C(e).

Proof. The theorem is a direct consequence of Clinger’s lemma (Lemma 25 below), Clause 1. Since

C(e) = C(e, mt_{C}, 0, false, ⟨⟨return⟩⟩),

we let (svaB)[[C(e)]]ρ = π_{2}, (svaB)[[⟨⟨return⟩⟩]]ρ = return = π_{1}, and ψ = one arg κ. Substituting the initial values in the right hand side, we infer:

(svaE)[[e]] (ρ◁mt_{C}^{ρ_{R}}) (multiple λϵ . return ϵ⟨⟩ρ_{R}(one arg κ))

= π_{2} unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

Since return = λϵϵ*ρ_{R}ψ . ψϵ,

λϵ . return ϵ⟨⟩ρ_{R}(one arg κ) = λϵ . (one arg κ)ϵ
= (one arg κ),

and it follows that

(svaE)[[e]] (ρ◁mt_{C}^{ρ_{R}}) (multiple (one arg κ))
= π_{2} unspecified ⟨⟩ (λν_{1}ν_{2} . ⊥) (one arg κ).

By Lemmas 12 and 22, the left hand side equals:

(svaE)[[e]] ρ (λϵ* . κ(truncate ϵ*))

By Theorem 18, the latter equals (svaE)[[e]] ρ κ. QED.

Lemma 24 (Compiled expressions set value register)

1. Let π = (svaB)[[C(e, ρ_{C}, n, i, b)]]ρ. For all ϵ, ϵ′,

πϵ = πϵ′.

2. Let π = (svaY)[[C(e, ρ_{C}, n, i, y)]]ρπ_{0}. For all ϵ, ϵ′,

πϵ = πϵ′.

3. Let π = (svaB)[[Cargs(e*, ρ_{C}, n, i, b)]]ρ, and let π_{1}(svaB)[[b]]ρ. If for all ϵ, ϵ′, π_{1}ϵ = π_{1}ϵ′, then for all ϵ, ϵ′,

πϵ = πϵ′.

Proof. The proof is by simultaneous induction on e and e*. We show one case from the (very routine) induction.

Clause 3: If e* = ⟨⟩, then Cargs(e*, ρ_{C}, n, i, b) = b. Otherwise, it is of the form:

C(e, ρ_{C}, n, i, ⟨push⟩:: Cargs(e_{1}*, ρ_{C}, n + 1, i, b)),

so that the result follows by Clause 1.

Lemma 25 (Clinger’s Lemma)

1. Consider any Scheme expression e, bbc closed instruction list b, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial value ϵ.

Let π_{1} = (svaB)[[b]]ρ and π_{2} = (svaB)[[C(e, ρ_{C}, #ϵ*, i, b)]]ρ. Then

(svaE)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (multiple λϵ . π_{1}ϵϵ*ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ

2. Consider any Scheme expression e, bbc open instruction list y, segment π, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial value ϵ.

Let π_{1} = (svaY)[[y]]ρπ and π_{2} = (svaY)[[C(e, ρ_{C}, #ϵ*, i, y)]]ρπ. Then

(svaE)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (multiple λϵ . π_{1}ϵϵ*ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ

3. Consider any sequence of Scheme expressions e*, bbc closed instruction list b, environment ρ, compile-time environment ρ_{C}, value sequence ϵ*, run-time environment ρ_{R}, and initial values ϵ and ϵ_{1}.

Let π_{1} = (svaB)[[b]]ρ and π_{2} = (svaB)[[Cargs(e*, ρ_{C}, #ϵ*, i, b)]]ρ.

Suppose that the after code sets the value register before it reads it, in the sense that, for all values ϵ′,

π_{1} ϵ = π_{1} ϵ′.

Then

(svaE*)[[e*]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ) = π_{2}ϵϵ*ρ_{R}ψ

Proof. The proof is by a simultaneous induction on e and e*. That is, in proving 1 and 2, we assume that 1 and 2 hold for any proper subexpression of e, and that 3 holds when each expression in e* is a proper subexpression of e. When proving 3, we assume that 1 and 2 hold for each e occurring in e*, and that 3 holds of any proper subsequence of e*. To emphasize the treatment of the single-valued semantics, we give the proof of clause 3 in detail; the proofs of clauses 1 and 2 are very similar in manner to Clinger’s original proof [1].

3. Here we argue by induction on e*, assuming that 1 and 2 hold of the expressions occurring in e*.

Base Case Suppose that e* = ⟨⟩. Then, by the semantic clause for E*,

(svaE*)[[⟨⟩]](ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)
= sva((λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)⟨⟩)
= sva(π_{1}ϵ_{1}(ϵ*^{⌢}⟨⟩)ρ_{R}ψ)
= sva(π_{1}ϵ_{1}ϵ*ρ_{R}ψ).

Since π_{1} is single-valued, the latter equals π_{1}ϵ_{1}ϵ*ρ_{R}ψ. Examining the compiler’s code, Cargs(⟨⟩, ρ_{C}, #ϵ*, i, b) = b, so that π_{1} = π_{2}. Since, by assumption, π_{1} ϵ = π_{1} ϵ_{1}, the case is complete.

Induction Step Suppose that 3 holds for e* and and 1 holds for e, and consider e:: e*. Using the semantic clause for E*, and writing κ for λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ, the left hand side of our goal takes the form:

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} .(sva E)*[[e*]](ρ◁_{ρ_{C}}^{ρ_{R}})(λϵ*.κ(⟨ϵ_{0}⟩^{⌢}ϵ*))))

Applying κ,

(λϵ_{1}* . π_{1}ϵ_{1}(ϵ*^{⌢}ϵ_{1}*)ρ_{R}ψ)(⟨ϵ_{0}⟩^{⌢}ϵ*)
= π_{1}ϵ_{1}(ϵ*^{⌢}(⟨ϵ_{0}⟩^{⌢}ϵ*))ρ_{R}ψ
= π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ

Hence, the left hand side equals:

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple

(λϵ_{0} . (sva E*)[[e*]] (ρ◁_{ρ_{C}}^{ρ_{R}}) (λϵ* . π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ)))

Applying the induction hypothesis with (ϵ*^{⌢}⟨ϵ_{0}⟩) in place of ϵ*, with the other variables unchanged, and letting

π_{3} = (svaB)[[Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ,

Lemma 24 shows (for all ϵ_{0}): (sva E*)[[e*]](ρ◁_{ρ_{C}}^{ρ_{R}})(λϵ*.π_{1}ϵ_{1}((ϵ*^{⌢}⟨ϵ_{0}⟩)^{⌢}ϵ*)ρ_{R}ψ) = π_{3}ϵ(ϵ*^{⌢}⟨ϵ_{0}⟩)ρ_{R}ψ. Using this, followed by the assumption that Lemma 24 establishes, and then the definition of push, and the semantics of push, we have:

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . π_{3} ϵ (ϵ*^{⌢}⟨ϵ_{0}⟩) ρ_{R} ψ))

= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . π_{3} ϵ_{0} (ϵ*^{⌢}⟨ϵ_{0}⟩) ρ_{R} ψ))
= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} . (push π_{3}) ϵ_{0} ϵ* ρ_{R} ψ))
= (sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})(multiple(λϵ_{0} .
(svaB)[[⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ
ϵ_{0} ϵ* ρ_{R} ψ))

We will apply Clause 1 with

b = ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b),

and thus with π_{2} = (svaB)[[C(e, ρ_{C}, #ϵ*, i, ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b))]]ρ. Hence,

(sva E)[[e]] (ρ◁_{ρ_{C}}^{ρ_{R}})

(multiple(λϵ_{0} . (svaB)[[⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)]]ρ

ϵ_{0} ϵ* ρ_{R} ψ))
= π_{2} ϵ ϵ* ρ_{R} ψ

But, by the code for Cargs, π_{2} is in fact equal to

(svaB)[[Cargs(e:: e*, ρ_{C}, #ϵ*, i, b)]],

as the latter is the code:

C(e, ρ_{C}, #ϵ*, i, ⟨push⟩:: Cargs(e*, ρ_{C}, #ϵ* + 1, i, b)).

5 The Tabulator Algorithm

The purpose of the tabulator is to translate programs from the basic byte code bbc into the tabular byte code tbc. In the former, the instructions:

     closure, literal, global, and set-global!

contain their argument literally within themselves. In the case of closure, this is a full, syntactic template; in the case of literal, it is a constant, for instance a large nested list; in the remaining cases it is an identifier. When the code is actually running on the virtual machine, however, we want there to be a single kind of fixed width item in the instruction stream.

We achieve this by replacing the item with a small (one-byte) integer, which is used as index into a table making up the template itself. Indeed, the instruction stream is itself contained in this table as its zeroth item. For this reason, and because we can not actually store the instruction stream there until we have linearized the code, the tabulator ensures that the zeroth item in the table it generates is not used. We will say that these four instructions use the template table.

The main content of the tabulator algorithm is contained in Section 5.1, while supplementary procedures (also used in the linker algorithm) are gathered in Section 5.2.

5.1 Tabulate and Related Procedures

Given a bbc template t = ⟨lap c b⟩, the tabulator treats c as the name of the template and b as the code from which literals are to be gleaned.

The algorithm uses a data structure called an inverse table. An inverse table is a bijection—implemented by an association list of tbc literals and integer values—whose range is a finite initial segment of the natural numbers; it represents a template table.

Inverse tables are extended, and their values are accessed, by a function probe, called with a tbc literal ℓ and an inverse table f. It returns a pair (i.e. cons) of values, the first of which is an index i and the second of which is an inverse table f′. If f is defined for ℓ, then f′ = f and i = f(ℓ). Otherwise, i is the least integer not in the range of f, and f′ = f ⊕ {ℓ ↦ i}. Thus, the new inverse table differs from the given one at most in its behavior for ℓ.

The algorithm first initializes an inverse table with the name of the given template as its entry at position 1, and with a dummy value that cannot possibly occur as a literal in the code at position 0. For this purpose we use the given template itself, which is surely too large to occur inside itself. The main recursive descent algorithm is then called with the byte code b and the initialized inverse table. Finally the resulting code and inverse table are returned; these are destructured, and the inverse table is converted into a list of its literals in the proper order. The big nasty dummy value is relaced with a small, convenient dummy value, namely 0. Finally, the tbc template ⟨template b′ e⟩ is returned.

(define (tabulate-top bbc-template)
  (let ((name (cadr bbc-template))
        (b    (cddr bbc-template)))
    (let ((inv-table
           (probe-fun
            (probe
             `(constant ,name)
             (probe-fun
              (probe

;; dummy for code seq slot ;;

               `(constant ,bbc-template)
               null-inv-table))))))
      (let ((code+inv-table (tabulate b inv-table)))
        `(template
          ,(car code+inv-table)  ; code
          ((constant 0)

. ; put safe dummy ,(cdr ; in first spot

             (invert-inv-table  ; in table
              (cdr code+inv-table)))))))))

The main recursive procedure tabulate takes a piece of bbc code w and a partially constructed inverse table f. It returns a pair (i.e. cons) consisting of the corresponding tbc code w̄, together with an extended table f′. The main correctness condition is that the semantics of w should be equal to that of w̄ (with respect to f′). The algorithm is, in case w is non-empty, first to tabulate all but the first instruction, obtaining code together with an extended inverse table. Then the first instruction is tabulated with respect to the extended inverse table. If w is empty, then no code is returned, represented by (), together with the given inverse table.

(define (tabulate bbc inv-table)

(if (null? bbc)
  (cons '() inv-table)
  (let ((instr (car bbc))
        (code+inv-table (tabulate (cdr bbc) inv-table)))
    (let ((after-code (car code+inv-table))
          (inv-table  (cdr code+inv-table)))
      (let ((instr+inv-table
             (tabulate-instruction instr inv-table)))
        (cons
         (cons (car instr+inv-table) after-code)
         (cdr instr+inv-table)))))))

The main content of the tabulator is to ensure that each individual instruction is properly treated. If the instruction uses the template table, then we must probe the table to get an index and a new table; the index is then inserted in place of the literal item. On the other hand, for closure, make-cont, and conditional instructions, a recursive call is needed to tabulate the nested code.

(define (tabulate-instruction instr inv-table)
(case (car instr)

;; Must recursively tabulate ;; the embedded template

((closure)
 (tabulate-closure-instruction instr inv-table))

;; replace literal ;; by index

((literal global set-global!)
 (tabulate-template-instruction instr inv-table))

;; Must recursively ;; tabulate both branches

((unless-false)
 (tabulate-conditional (cadr instr) (caddr instr) inv-table))

;; Must recursively ;; tabulate return code

((make-cont)
 (tabulate-make-cont (cadr instr) (caddr instr) inv-table))

;; No change needed

(else
(cons instr inv-table))))

For a closure instruction, we first tabulate the embedded template, and then probe with the converted value.

(define (tabulate-closure-instruction instr inv-table)
(let ((index+inv-table
   (probe (tabulate-top (cadr instr)) inv-table)))
`((closure ,(probe-val index+inv-table))
.
,(probe-fun index+inv-table))))

For the other instructions using the template table, we simply probe with the instruction literal.

(define (tabulate-template-instruction instr inv-table)
(let ((index+inv-table
   (probe
    (instruction-literal instr)
    inv-table)))
`((,(car instr) ,(probe-val index+inv-table))
.
,(probe-fun index+inv-table))))

For conditionals, we tabulate the nested code. The consequent and alternative must be done in some fixed order, so that the table resulting from tabulating the first may be supplied when the second is tabulated.

(define (tabulate-conditional conseq0 alt0 inv-table)
(let ((alt+inv-table
   (tabulate alt0 inv-table)))
(let ((conseq+inv-table
     (tabulate conseq0 (cdr alt+inv-table))))
`((unless-false ,(car conseq+inv-table) ,(car alt+inv-table))
  .
  ,(cdr conseq+inv-table)))))

For a make-cont instruction we simply tabulate the nested code.

(define (tabulate-make-cont nested0 n inv-table)
(let ((nested+inv-table
   (tabulate nested0 inv-table)))
`((make-cont ,(car nested+inv-table) ,n)
  .
  ,(cdr nested+inv-table))))

The instruction-literal procedure “wraps up” what literally occurs in a byte code instruction with a word tagging whether it is a global variable or a constant. Templates extracted from the closure instruction need no tag, as the syntax of a template identifies it as such. We shall use the phrase “the instruction literal of an instruction” to refer to the value returned by this procedure. We will say that an instruction literal occurs in a source byte code expression without template a under the same recursive condition we used for occurrence of an index n in a byte expression with template.

(define (instruction-literal instr)
  (let ((literal-content (cadr instr)))
    (case (car instr)
      ((literal)     `(constant        ,literal-content))
      ((global)      `(global-variable ,literal-content))
      ((set-global!) `(global-variable ,literal-content))
      ((closure)     literal-content)
      (else          '#f))))

5.2 Probe and Inverse Tables

If f is a partial function with range included in N, then by sup f we mean the maximum value (if any) that f takes on. That is, sup f = n if and only if there is an argument a such that fa = n, and for all b, if fb is well-defined, then fb ≤ n.

probe : (d × (d → N)) → (N × (d → N)) probe(d, f) = ⟨j, g⟩ where

g(d) = j and

if f(d) ↓ then g = f, otherwise g = f + {d ↦ 1 + sup f}

One consequence of the definition of probe is that it does not alter the behavior of the function on arguments for which it is already defined:

f(d) ↓ ∧ g = probe fun(probe(d′, f)) ⇒ f(d) = g(d).

When we say of two (partial) functions f and g that g extends f, we mean that g(x) = f(x) whenever the latter is defined. So g extends f.

A second fact about probe is that it preserves the property of being inverse to a finite sequence:

finite seq(f^{−1}) ⇒ finite seq((probe fun(probe(d′, f)))^{−1}).

Thus, if f^{−1}^{∈}e, then so is the inverse of the function resulting from a probe.

We will introduce aliases for the pair-destructuring operators first and second:

probe val : N × (d → N) → N probe val(⟨j, g⟩) = j

probe fun : N × (d → N) → (d → N) probe fun(⟨j, g⟩) = g

5.2.1 Implementation of Probe

To implement inverse tables, we use Scheme lists containing cons cells. We will call a list an inv-table if:

• The car of each such pair represents a template literal, and the cdr is a number;

• No two pairs have the same car;

• The numbers occurring in the cdrs are in strictly decreasing order and coincide with an initial segment of the natural numbers.

Hence, each inv-table represents an inverse table, when the operation of applying an inverse table to a literal is implemented by the procedure seek-probe-value below. Conversely, every inverse table, being finite, may be represented by an inv-table (in a large enough heap), simply by providing a cons cell for each ⟨literal, value⟩ pair in the function, and building a list containing them in decreasing order of the values.

To implement probe relative to this representation, we use the following procedures:

(define (probe o inv-tab)
  (let ((v (seek-probe-value inv-tab o)))
    (if (fail? v)
        (let ((new-inv-tab (expand-inv-table inv-tab o)))
          (cons (seek-probe-value new-inv-tab o)
                new-inv-tab))
        (cons v inv-tab))))
(define (expand-inv-table inv-tab o)
  (if (eq? inv-tab null-inv-table)

      (list (cons o 0))  ; single entry
      (let ((new-val  (+ (cdar inv-tab) 1)))
        (cons (cons o new-val)  ; new entry

inv-tab)))) ; before old table

(define (seek-probe-value inv-tab o)
  (let iter ((inv-tab inv-tab))
    (cond ((null? inv-tab) (fail))  ; not there
          ((equal? o (caar inv-tab))  ; first entry
           (cdar inv-tab))
          (else (iter (cdr inv-tab))))))  ; seek further
(define null-inv-table '())

We also introduce aliases for car and cdr:

(define probe-val car)
(define probe-fun cdr)

The next applicative Scheme procedure allows us to generate a representation of a template table from an inv-table table. The operation of applying the resulting table e to an integer argument n is given by the Scheme form (nth e n).

(define (invert-inv-table inv-tab)

;;

;; convert from decreasing order to increasing order

  (reverse
   (map

;; extract just the template literals

    car
    inv-tab)))

Two final auxiliaries are:

(define (fail) 'fail)
(define (fail? value) (eq? value 'fail))

6 Correctness of the Tabulator Algorithm

In this section, we will use a bar to distinguish variables over the targets of a translation, which belong to the tabular byte code tbc, such as z̄, from variables over source expressions, which belong to the basic byte code bbc, such as z.

We will also write:

• T (t), when t is a bbc template, to refer to the result t̄ of calling

tabulate-template on t;

• T (w, f), when w is a bbc (open or closed) instruction sequence, to refer to the result ⟨w̄, f′⟩ of calling tabulate on w and f;

• T (m, f), when m is a bbc instruction, to refer to the result ⟨m̄, f′⟩ of calling tabulate on m and f.

6.1 Syntactic Correctness

Theorem 26 (Tabulator Syntactic Correctness)

1. If t is a bbc template and t̄= T (t), then t̄ is a tbc template.

2. Suppose b is a bbc closed instruction list and f is an inverse table. If ⟨b̄, f′⟩ = T (b, f), then b̄ is a tbc closed instruction list and f′ is an inverse table.

3. Suppose y is a bbc open instruction list and f is an inverse table. If ⟨ȳ, f′⟩ = T (y, f), then ȳ is a tbc open instruction list and f′ is an inverse table.

4. Suppose z is a bbc instruction and f is an inverse table. If ⟨z̄, f′⟩ = T (m, f), then z̄ is a tbc instruction and f′ is an inverse table.

Proof. The proof is by simultaneous structural induction on the bbc syntax.

1. t is ⟨lap c b⟩. Apply 2. to b and the inverse table

f = {[(constant t) ↦ 0], [c ↦ 1]},

obtaining ⟨b̄, f′⟩. Assuming that inv-table represents f′, the following code returns a template table e.

`((constant 0)
.                             ; put safe dummy
,(cdr                         ; in first spot
(invert-inv-table           ; in table
inv-table)))

So tabulate-template returns the tbc template ⟨template b̄ e⟩.

2. Consider the different syntactic cases for b:

(a) If b is ⟨⟨return⟩⟩ or ⟨⟨call n⟩⟩, then T (b, f) = ⟨b, f⟩, and b belongs to the tbc syntax.

(b) Suppose b is ⟨⟨unless-false b_{1} b_{2}⟩⟩. By the inductive hypothesis (clause 2), T (b_{2}, f) is a syntactically correct pair ⟨b̄_{2}, f_{2}⟩, as is T (b_{1}, f_{2}) = ⟨b̄_{1}, f′⟩. Hence, ⟨⟨unless-false b̄_{1} b̄_{2}⟩⟩ is a closed tbc instruction list, and f′ is an inverse table.

(c) Suppose b is ⟨⟨make-cont b_{1} n⟩:: b_{2}⟩. By the inductive hypothesis (clause 2), T (b_{2}, f) is a syntactically correct pair ⟨b̄_{2}, f_{2}⟩, as is T (b_{1}, f_{2}) = ⟨b̄_{1}, f′⟩. Hence, ⟨⟨make-cont b̄_{1} n⟩:: b̄_{2}⟩ is a closed tbc instruction list, and f′ is an inverse table.

(d) Suppose b is z:: b_{1}. Using the inductive hypothesis (clause 2), T (b_{1}, f) is a syntactically correct pair ⟨b̄_{1}, f_{1}⟩. Similarly, using clause 4, T (z, f_{1}) is a syntactically correct pair ⟨z̄, f′⟩. Hence, ⟨z̄:: b̄_{1}, f′⟩ is syntactically correct.

3. Consider the different syntactic cases for y:

(a) Suppose y is ⟨⟨make-cont y_{1} n⟩:: b_{2}⟩. By the inductive hypothesis (clause 2), T (b_{2}, f) = ⟨b̄_{2}, f_{2}⟩ is syntactically correct. By clause 3, T (y_{1}, f_{2}) = ⟨ȳ_{1}, f′⟩ is a syntactically correct pair. Hence, ⟨⟨make-cont ȳ_{1} n⟩:: b̄_{2}⟩ is a closed tbc instruction list, and f′ is an inverse table.

(b) Suppose y is ⟨⟨make-cont ⟨⟩ n⟩:: b_{2}⟩. As before, T (b_{2}, f) = ⟨b̄_{2}, f_{2}⟩ is syntactically correct. Examining the code, T (⟨⟩, f_{2}) = ⟨⟨⟩, f_{2}⟩. Hence, T (y, f) is the syntactically correct

⟨⟨⟨make-cont ⟨⟩ n⟩:: b̄_{2}⟩, f_{2}⟩.

(c) Suppose y is z:: y_{1}. By the inductive hypothesis (clause 3), T (y_{1}, f) = ⟨ȳ_{1}, f_{1}⟩ is a syntactically correct pair. Similarly, using clause 4, T (z, f_{1}) = ⟨z̄, f′⟩ is a syntactically correct pair. Hence, ⟨z̄:: ȳ_{1}, f′⟩ is syntactically correct.

(d) Suppose y is ⟨z⟩. Using clause 4, T (z, f) = ⟨z̄, f′⟩ is a syntactically correct pair. Hence, ⟨z̄, f′⟩ is syntactically correct.

4. This is the only real case in the proof. Consider the different syntactic cases for z:

(a) Suppose z is ⟨unless-false y_{1} y_{2}⟩. By the inductive hypothesis (clause 3), T (y_{2}, f) = ⟨ȳ_{2}, f_{2}⟩ is a syntactically correct pair. T (y_{1}, f_{2}) = ⟨ȳ_{1}, f′⟩ is a syntactically correct pair. Hence, ⟨unless-false ȳ_{1} ȳ_{2}⟩ is a neutral instruction, and f′ is an inverse table.

(b) Suppose z is ⟨literal c⟩. Then instruction-literal of z is

d = (constant c). If probe(d, f) is ⟨n, f′⟩, then T returns the syntactically correct value ⟨⟨literal n⟩, f′⟩.

(c) Suppose z is ⟨closure t⟩. By the inductive hypothesis (clause 1), T (t) is a syntactically correct tbc template t̄. So probe(t̄, f) = ⟨n, f′⟩, and the final value returned is ⟨⟨closure n⟩, f′⟩.

(d) Suppose z is ⟨global i⟩ or ⟨set-global! i⟩. Then the procedure

instruction-literal, applied to z, yields d = (global i). If

probe(d, f) is ⟨n, f′⟩, then T returns the syntactically correct value ⟨⟨global n⟩, f′⟩ or ⟨⟨set-global! n⟩, f′⟩.

(e) Otherwise, z is a tbc neutral instruction, and T returns ⟨z, f⟩.

Lemma 27 (Tabulator extends inverse tables.)

1. If T (b, f) = ⟨b̄, f′⟩, then f′ extends f;

2. If T (y, f) = ⟨ȳ, f′⟩, then f′ extends f;

3. If T (z, f) = ⟨z̄, f′⟩, then f′ extends f.

Proof. The proof is by simultaneous induction on the bnf for b, y, and z.

1. Consider the syntactic cases for b:

(a) b = ⟨⟨return⟩⟩ or b = ⟨⟨call n⟩⟩: Then T (b, f) = ⟨b, f⟩, and f extends itself.

(b) Suppose b is ⟨⟨unless-false b_{1} b_{2}⟩⟩. Let T (b_{2}, f) = ⟨b̄_{2}, f_{2}⟩ and T (b_{1}, f_{2}) = ⟨b̄_{2}, f′⟩. By the induction hypothesis (clause 1), f_{2} extends f, and f′ extends f_{2}. So f′ extends f.

(c) If b is ⟨⟨make-cont b_{1} n⟩:: b_{2}⟩, the argument is similar to the previous case.

(d) Suppose b is ⟨z:: b_{1}⟩. Then by IH (clause 1), if T (b_{1}, f) = ⟨b̄_{1}, f_{1}⟩, then f_{1} extends f. So applying IH (clause 3) to z and f_{1}, the resulting inverse table extends f.

2. The syntactic cases for y are very similar to those for b.

3. Consider the syntactic cases for z:

(a) z = ⟨unless-false y_{1} y_{2}⟩: Apply IH (clause 2) twice and the transitivity of extends.

(b) z = ⟨literal c⟩: f′ is probe(⟨constant c⟩, f), which extends f.

(c) z = ⟨closure t⟩: f′ is probe(t, f), which extends f.

(d) z = ⟨global i⟩ or z = ⟨set-global! i⟩: likewise.

(e) Otherwise f′ = f.

The flattener algorithm also requires that a special syntactic property holds of the output of the tabulator algorithm. To define that property, we first need various notions of occurrence in an instruction or instruction list.

Definition 28 (occurs in)

In the bbc or tbc, 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 ℓ is a bbc constant c, identifier i, or template t, we say that ℓ occurs in the bbc neutral instruction z if z is of the form ⟨i ℓ⟩, where i is literal,

global, set-global!, or closure.

We will also say that n occurs as a template index in the tbc neutral instruction z if z is of the form ⟨i n⟩, where i is literal, global,

set-global!, or closure.

If ℓ is a bbc constant c, identifier i, or template t, we say that ℓ occurs in the bbc code sequence w if there is a z such that z occurs in w and ℓ occurs in z.

Similarly, n occurs as a template index in the tbc code sequence w if there is a z such that z occurs in w and n occurs as a template index in z.

Lemma 29 t does not occur as a constant c in any instruction ⟨literal c⟩ contained in t.

Proof. If z = ⟨literal c⟩ is an instruction appearing in t, then the rank(c) < rank(z) < rank(t).

Lemma 30 Let ℓ be a bbc literal with f(ℓ) = n.^{3}

1. Suppose that ℓ does not occur in z; and suppose that T (z, f) = ⟨z̄, f′⟩. Then n does not occur as a template index in z̄.

2. Suppose that ℓ does not occur in w; and suppose that T (w, f) = ⟨w̄, f′⟩. Then n does not occur as a template index in w̄.

Proof. The proof is by simultaneous structural induction on the bnf for the bbc.

1. Consider the different syntactic cases for z:

(a) z = ⟨unless-false y_{1} y_{2}⟩, and z̄ = ⟨unless-false ȳ_{1} ȳ_{2}⟩. By the induction hypothesis (clause 2), n does not occur as a template index in ȳ_{1} or in ȳ_{2}; hence it does not occur in z̄.

(b) z = ⟨literal c⟩, and c ≠ ℓ. Let ⟨n′, f′⟩ = probe(⟨constant c⟩, f) where f′((constant c)) = n′. Since f, being an inverse table, is a bijection, n′ ≠ n. Moreover, T (z, f) = ⟨⟨literal n′⟩, f′⟩, so n does not occur as a template index in the instruction.

(c) z = ⟨closure t⟩. Let t̄ = T (t), and let ⟨n′, f′⟩ = probe(t̄, f), where f′(t) = n′. Since f, being an inverse table, is a bijection, n′ ≠ n. Moreover, T (z, f) = ⟨⟨closure n′⟩, f′⟩, so n does not occur as a template index in the instruction.

3So ℓ is a constant c or identifier i. If ℓ were a bbc template t, then f would not be defined for ℓ: bbc templates are disjoint from tbc templates.

(d) z = ⟨global i⟩ [or z = ⟨set-global! i⟩]. Let

⟨n′, f′⟩ = probe((global-variable i), f),

where f′((global-variable i)) = n′. Since f, being an inverse table, is a bijection, n′ ≠ n. Moreover, T (z, f) = ⟨⟨global n′⟩, f′⟩ [or ⟨set-global! n′⟩], so n does not occur as a template index in the instruction.

(e) Otherwise z̄ = z, and no n′ occurs as a template index in it.

2. Routine enumeration of syntactic cases.

Corollary 31 (Template table entry 0)

If T (t) = t̄, then 0 does not occur as a template table entry in t̄.

Proof. The procedure tabulate-template calls tabulate with an f such that f(t) = 0. So apply Lemmas 29 and 30.

Lemma 32 (Tabulator output defined for occurrences)

1. If T (b, f) = ⟨b̄, f′⟩, and if n occurs as a template index in b, then n is in the range of f′;

2. If T (y, f) = ⟨ȳ, f′⟩, and if n occurs as a template index in y, then n is in the range of f′;

3. If T (z, f) = ⟨z̄, f′⟩, and if n occurs as a template index in z, then n is in the range of f′.

As a consequence, if T (t) = ⟨template b̄ e⟩, and if n occurs as a template index in b, then e is defined at n.

Proof. By the usual syntactic induction:

1. Take cases on the syntactic form of b:

(a) b = ⟨⟨return⟩⟩ and b = ⟨⟨call n⟩⟩ have no occurrences.

(b) b = ⟨⟨unless-false⟩ b_{1} b_{2}⟩ or b = ⟨⟨make-cont b_{1} n⟩:: b_{2}⟩: The occurrences in b are precisely those in b_{1} or b_{2}. Moreover, by the IH clause 1 together with Lemma 27, the range of f′ includes the occurrences of each separately.

(c) b = z:: b_{1}: The occurrences in b are precisely those in b_{1} or z. Moreover, by the IH clauses 1 and 3, together with Lemma 27, the range of f′ includes the occurrences of each separately.

2. Take cases on the syntactic form of y:

(a) y = ⟨⟨make-cont y_{1} n⟩:: b⟩: Similar to case 1(b), but using IH clauses 1 and 2.

(b) y = ⟨⟨make-cont ⟨⟩ n⟩:: b⟩: The occurrences in y are precisely those in b. Hence it suffices to apply IH, Clause 1.

(c) y = z:: y_{1}: Similar to case 1(c), but using IH clauses 2 and 3.

(d) y = ⟨z⟩: Immediate from IH clause 2.

3. Take cases on the syntactic form of z:

(a) z = ⟨⟨unless-false⟩ y_{1} y_{2}⟩: Similar to case 1(b), but using IH clause 2.

(b) z = ⟨literal c⟩: Let probe(⟨constant c⟩, f) = ⟨n, f′⟩, so that T (z, f) = ⟨⟨literal n⟩, f′⟩. By the definition of probe, n is in the range of f′.

(c) z = ⟨closure t⟩: Assume that T (t) = t̄. Let probe(t, f) = ⟨n, f′⟩, so that T (z, f) = ⟨⟨closure n⟩, f′⟩. By the definition of probe, n is in the range of f′.

(d) z = ⟨global i⟩ or z = ⟨set-global! i⟩: Let

probe(⟨global-variable i⟩, f) = ⟨n, f′⟩,

so that T (z, f) = ⟨⟨global n⟩, f′⟩ or ⟨⟨set-global! n⟩, f′⟩. By the definition of probe, n is in the range of f′.

(e) Otherwise z has no occurrences.

Definition 33 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.

We will say that an instruction or sequence respects an inverse table f if it respects the template table f^{−1}.

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.

Lemma 34 Suppose w respects the template table e = ⟨d_{0}, … d_{n}, … d_{j}⟩; suppose n does not occur as a template index in w; and suppose d′_{n} is not a template. Then w respects e′ = ⟨d_{0}, … d′_{n}, … d_{j}⟩.

Proof. For n, each of the four clauses of the definition of respect is vacuously fulfilled. Moreover, for n′ ≠ n, e′(n′) = e(n′), so the clauses are fulfilled for e′ assuming that they held for e.

Lemma 35 If w respects the inverse table f, and f_{1} is an inverse table that extends f (i.e. f is a subfunction of f_{1}), then w respects f_{1}.

Proof. Since f_{1} is an inverse table, f_{1}^{−1} is defined and extends f^{−1}. Hence, for each n occurring in w, since f^{−1} was defined for n, f_{1}^{−1} is also defined for n and has the same value.

Theorem 36 (Tabulate Elicits Respect)

1. If t = ⟨lap c b⟩ is a bbc template, then T (t) is self-respecting.

2. Suppose that b is a bbc closed instruction list and f is an inverse table. If T (b, f) = ⟨b̄, f′⟩, then b̄ respects f′.

3. Suppose that y is a bbc open instruction list and f is an inverse table. If T (y, f) = ⟨ȳ, f′⟩, then ȳ respects f′.

4. Suppose that z is a bbc neutral instruction and f is an inverse table. If T (z, f) = ⟨z̄, f′⟩, then z̄ respects f′.

Proof. The proof is by simultaneous induction on the syntactic structure of the bbc. For convenience we will say that a pair is self-respecting if its first element respects its second element.

1. Let f_{0} be the empty (everywhere undefined) inverse table. Let f_{1} be:

probe fun(probe(⟨constant c⟩, probe fun(probe(⟨constant b⟩, f_{0})))).

Apply induction hypothesis (Clause 2) to b and f_{1}, concluding that T (b, f_{1}) = ⟨b̄, f⟩ is self-respecting. By Corollary 31, 0 has no occurrence in b̄. Hence, by Lemma 34, b̄ still respects f^{−1} with ⟨constant 0⟩ in place of the zeroth entry of f^{−1}, which we may call e. Hence t̄= ⟨template b̄ e⟩ is self-respecting.

2. Consider the syntactic possibilities for b:

(a) b = ⟨⟨return⟩⟩ or b = ⟨⟨call n⟩⟩: Then T (b, f) = ⟨b, f⟩ and respect is vacuous.

(b) b = ⟨⟨unless-false⟩ b_{1} b_{2}⟩: Then by the induction hypothesis (clause 2), T (b_{2}, f) = ⟨b̄_{2}, f_{2}⟩ is self-respecting, as is T (b_{1}, f_{2}) = ⟨b̄_{1}, f′⟩. We may apply Lemmas 27 and 35 to infer that ⟨b̄_{2}, f′⟩ is also self-respecting. However, since the instructions z occurring in ⟨⟨unless-false⟩ b̄_{1} b̄_{2}⟩ are pecisely those occurring in either b̄_{1} or b̄_{2}, T (b, f) is self-respecting.

(c) b = ⟨⟨make-cont b_{1} n⟩:: b_{2}⟩ is similar.

(d) b = z:: b_{1}: Then by the induction hypothesis (clause 2),

T (b_{1}, f) = ⟨b̄_{1}, f_{1}⟩

is self-respecting, and by clause 3, T (z, f_{1}) = ⟨z̄, f′⟩ is self respecting. The remainder of the argument is like case (b).

3. The syntactic possibilities for y are similar to those of b.

4. Consider the syntactic possibilities for z:

(a) z = ⟨⟨unless-false⟩ y_{1} y_{2}⟩: Similar to case 2(b), except that clause 3 is cited.

(b) z = ⟨literal c⟩: T (⟨literal c⟩, f) = ⟨⟨literal n⟩, f′⟩, is selfrespecting if f′(n) = ⟨constant c⟩. This is guaranteed because probe(⟨constant c⟩, f) = ⟨n, f′⟩.

(c) z = ⟨closure t⟩: T (⟨closure t⟩, f) = ⟨⟨closure n⟩, f′⟩, is selfrespecting if f′(n) = t. This is guaranteed because probe(t, f) = ⟨n, f′⟩.

(d) z = ⟨global i⟩ or z = ⟨set-global! i⟩: likewise.

(e) Otherwise respect is vacuous.

6.2 Semantic Correctness

The main correctness theorem states that the procedure tabulate-top and tabulate are correct in the sense that their output has the same denotation as their (expression) input.

Lemma 37 1. If e(n) = e′(n) for every n occurring in b, then B_{τ} [[b]]e = B_{τ} [[b]]e′;

2. If e(n) = e′(n) for every n occurring in y, then Y_{τ} [[y]]e = Y_{τ} [[y]]e′;

3. If e(n) = e′(n) for every n occurring in z, then Z_{τ} [[z]]e = Z_{τ} [[z]]e′.

Proof. The proof is by the usual simultaneous induction.

1. In each case, use the inductive hypotheses and substitute equals for equals in the semantic clauses.

2. As in case 1.

3. Here we show the syntactic cases for z:

(a) z = ⟨⟨unless-false⟩ y_{1} y_{2}⟩. Since every occurrence in y_{1} or y_{2} is an occurrence in z, IH clause 2 implies:

Y_{τ} [[y_{1}]]e = Y_{τ} [[y_{1}]]e′ and Y_{τ} [[y_{2}]]e = Y_{τ} [[y_{2}]]e′.

Thus:

Z_{τ} [[z]]e = λeρπ . if truish(Y_{τ} [[y_{1}]]eρπ)(Y_{τ} [[y_{2}]]eρπ)
= λeρπ . if truish(Y_{τ} [[y_{1}]]e′ρπ)(Y_{τ} [[y_{2}]]e′ρπ)
= Z_{τ} [[z]]e′.
(b) z = ⟨literal n⟩: As n occurs, e(n) = e′(n).
Z_{τ} [[z]]e = λρ . literal (K[[(e(n))(1)]])
= λρ . literal (K[[(e′(n))(1)]])
= Z_{τ} [[z]]e′.

(c) z = ⟨closure n⟩: Again, n occurs, so e(n) = e′(n).

Z_{τ} [[z]]e = λρ . closure (T_{τ} [[e(n)]]ρ)
= λρ . closure (T_{τ} [[e′(n)]]ρ)
= Z_{τ} [[z]]e′.

(d) z = ⟨global n⟩: Again e(n) = e′(n).

Z_{τ} [[z]]e = λρ . global (lookup ρ (e(n))(1))
= λρ . global (lookup ρ (e′(n))(1))
= Z_{τ} [[z]]e′.

(e) z = ⟨set-global! n⟩: Again e(n) = e′(n).

Z_{τ} [[z]]e = λρ . set global (lookup ρ (e(n))(1))
= λρ . set global (lookup ρ (e′(n))(1))
= Z_{τ} [[z]]e′.

(f) In all other cases, e occurs vacuously in the semantic clause.

Lemma 38 (Meaning stable)

Let T (b, f) = ⟨b̄, f_{1}⟩, and assume T (w_{1}, f_{1}) = ⟨w̄, f_{2}⟩ or T (z_{1}, f_{1}) = ⟨z̄, f_{2}⟩. Then

B_{τ} [[b]]f_{1}^{−1} = B_{τ} [[b]]f_{2}^{−1}.

Let T (y, f) = ⟨ȳ, f_{1}⟩, and assume T (w_{1}, f_{1}) = ⟨w̄, f_{2}⟩ or T (z_{1}, f_{1}) = ⟨z̄, f_{2}⟩. Then

Y_{τ} [[y]]f_{1}^{−1} = Y_{τ} [[y]]f_{2}^{−1}.

Similarly, let T (z, f) = ⟨z̄, f_{1}⟩, and assume T (w_{1}, f_{1}) = ⟨w̄, f_{2}⟩ or T (z_{1}, f_{1}) = ⟨z̄_{1}, f_{2}⟩. Then

Z_{τ} [[z]]f_{1}^{−1} = Z_{τ} [[z]]f_{2}^{−1}.

Proof. Because f_{2} extends f_{1} (Lemma 27), and because f_{1} is defined for indices occurring in the tbc expression (Lemma 32), Lemma 37 ensures that the denotations are equal.

Theorem 39 (Semantic Correctness of the Tabulator)

1. T [[t]] = T_{τ} [[T (t)]]; 2. For any inverse table f_{0}, T (b, f_{0}) = ⟨b̄, f⟩ implies

B[[b]] = B_{τ} [[b̄]]f^{−1};

3. For any inverse table f_{0}, T (y, f_{0}) = ⟨ȳ, f⟩ implies Y[[y]] = Y_{τ} [[ȳ]]f^{−1};

4. For any inverse table f_{0}, T (z, f_{0}) = ⟨z̄, f⟩ implies

Z[[z]] = Z_{τ} [[z̄]]f^{−1};

Proof. The proof is by the usual simultaneous induction.

1. Suppose t = ⟨lap c b⟩. Let

f_{t} = {[(constant t) ↦ 0], [c ↦ 1]}

and let T (b, f_{t}) = ⟨b̄, f′_{t}⟩. Then using the semantic definition and IH clause 2,

T [[t]] = B[[b]]
= B_{τ} [[b̄]]e,

where e = (f′_{t})^{−1}. Moreover, by Lemmas 29 and 30, 0 does not occur as a template index in b̄. By Lemma 37, letting e′ be e with [(constant 0) ↦ 0], it follows that

B_{τ} [[b̄]]e = B_{τ} [[b̄]]e′
= B_{τ} [[b̄]]e′
= T_{τ} [[⟨template b̄ e′⟩]],

which is T (⟨lap c b⟩).

2. Take cases on the syntactic form of b:

(a) b = ⟨⟨return⟩⟩ or b = ⟨⟨call n⟩⟩: b̄ = b, and the semantic clauses ensure that B[[b]] = B_{τ} [[b]]e, for all e.

(b) b = ⟨⟨unless-false b_{1} b_{2}⟩⟩: Let T (b_{2}, f) = ⟨b̄_{2}, f_{2}⟩, and let T (b_{1}, f_{2}) = ⟨b̄_{1}, f′⟩, so that

T (b, f) = ⟨⟨⟨unless-false b̄_{1} b̄_{2}⟩⟩, f′⟩.

Let e be (f′)^{−1}. By Lemma 38, B_{τ} [[b̄_{2}]]e = B_{τ} [[b̄_{2}]]f_{2}^{−1}. Hence, using the semantic clauses and IH, clause 2:

B_{τ} [[⟨⟨unless-false  b̄_{1} b̄_{2}⟩⟩]]e
= λρ . if truish(B_{τ} [[b̄_{1}]]eρ)(B_{τ} [[b̄_{2}]]eρ)
= λρ . if truish(B_{τ} [[b_{1}]]ρ)(B_{τ} [[b_{2}]]ρ)
= B[[⟨⟨unless-false b_{1} b_{2}⟩⟩]]

(c) b = ⟨make-cont b_{1} n⟩:: b_{2} is similar.

(d) Suppose b = z:: b_{1}. Let T (b_{1}, f) = ⟨b̄_{1}, f_{1}⟩, and let T (z, f_{1}) =

⟨z̄, f′⟩, so that

T (b, f) = ⟨z̄:: b̄_{1}, f′⟩.

Let e be (f′)^{−1}. Citing Lemma 38, the semantic clauses, and IH, clauses 2 and 4:

B_{τ} [[z̄:: b̄_{1}]]e = λρ . Z_{τ} [[z̄]]eρ (B_{τ} [[b̄_{1}]]eρ)
= λρ . Z[[z]]ρ (B[[b]]ρ)
= B[[z:: b]]

3. Open instruction lists y are similar to closed ones. We wiull show only one case:

(b) y = ⟨make-cont ⟨⟩ n⟩:: b: Let T (b, f) = ⟨b̄, f′⟩, so that

T (y, f) = ⟨⟨make-cont ⟨⟩ n⟩:: b̄, f′⟩.

Let e be (f′)^{−1}. Hence, using the semantic clauses, and IH, Clause 2:

Y_{τ} [[ȳ]]eρπ = make cont (π) n (B_{τ} [[b̄]]eρ)
= make cont (π) n (B[[b]]ρ)
= Y[[y]]ρπ

4. Neutral machine instructions z:

(a) z = ⟨unless-false y_{1} y_{2}⟩: Let T (y_{2}, f) = ⟨ȳ_{2}, f_{2}⟩, and let T (y_{1}, f_{2}) = ⟨ȳ_{1}, f′⟩, so that

T (z, f) = ⟨⟨⟨unless-false ȳ_{1} ȳ_{2}⟩⟩, f′⟩.

Citing Lemma 38, the semantic clauses, and IH, clause 3,

Z_{τ} [[⟨unless-false  ȳ_{1} ȳ_{2}⟩]]e
= λρπ . if truish(Y_{τ} [[ȳ_{1}]]eρπ)(Y_{τ} [[ȳ_{2}]]eρπ)
= λρ . if truish(Y[[y_{1}]]ρ)(Y[[y_{2}]]ρ)
= Z[[⟨⟨unless-false y_{1} y_{2}⟩⟩]]

(b) z = ⟨literal c⟩: So, letting probe(⟨constant c⟩, f) = ⟨n, f′⟩, and let (f′)^{−1} = e. So

T (z, f) = ⟨⟨literal n⟩, f′⟩

and f′(⟨constant c⟩) = n. Hence e(n)(1) = c, and

Z[[z]] = λρ . literal (K[[c]])
= λρ . literal (K[[e(n)(1)]])
= Z_{τ} [[⟨literal n⟩]]e

(c) z = ⟨closure t⟩: Let T (t) = t̄; by the IH, clause 1, T [[t]] = T_{τ} [[t̄]]. Let probe(t, f) = ⟨n, f′⟩, and let (f′)^{−1} = e. So

T (z, f) = ⟨⟨closure n⟩, f′⟩,

and f′(t) = n. Hence

Z[[z]] = λρ . closure (T [[t]]ρ)
= λρ . closure (T_{τ} [[e(n)]]ρ)
= Z_{τ} [[⟨closure n⟩]]e

(d) global and set-global! are similar to literal.

(e) In all other cases, T (z, f) = ⟨z, f⟩, and the semantic for tbc simply ignore their argument e, and return the same value as the corresponding clause for bbc.

References

[1] Will Clinger. The Scheme 311 compiler: An exercise in denotational semantics. In 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, New York, August 1984. The Association for Computing Machinery, Inc.

[2] IEEE Std 1178-1990. IEEE Standard for the Scheme Programming Language. Institute of Electrical and Electronic Engineers, Inc., New York, NY, 1991.

[3] D. E. Knuth. Literate programming. The Computer Journal, 27(2), 1984.

[4] David A. Schmidt. Denotational Semantics: A Methodology for Language Development. Wm. C. Brown, Dubuque, IA, 1986.

[5] Joseph E. Stoy. Denotational Semantics: The Scott-Strachey Approach to Programming Language Theory. MIT Press, Cambridge, MA, 1977.