A Verified Compiler for Pure PreScheme: Final Report for Contract Number F19628-89-C-001

Dino P. Oliva oliva@corwin.ccs.northeastern.edu Mitchell Wand wand@flora.ccs.northeastern.edu College Of Computer Science Northeastern University 360 Huntington Avenue, 161CN Boston, MA 02115, USA September 23, 1991

Contents

1 Introduction 3 2 Obtaining an executable Scheme semantics 3 3 Refining the PreScheme semantics 4 4 Development of the PreScheme Byte-Code Compiler 7 5 Development of the Assembler 9 6 Conclusions and Further Work 10 7 Language Overview 11 8 The Semantics 11

8.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 8.2 Value Domains . . . . . . . . . . . . . . . . . . . . . . . . . . 13 8.3 Semantic Functions . . . . . . . . . . . . . . . . . . . . . . . . 14

8.3.1 Auxiliary Valuations . . . . . . . . . . . . . . . . . . . 14 8.3.2 Main Valuations . . . . . . . . . . . . . . . . . . . . . 15

8.4 Auxiliary Functions . . . . . . . . . . . . . . . . . . . . . . . 20

9 The Compiler 22 9.1 Compiler Syntactic Domains . . . . . . . . . . . . . . . . . . 23 9.2 Compiler Value Domains . . . . . . . . . . . . . . . . . . . . . 23 9.3 Compiler Semantic Functions . . . . . . . . . . . . . . . . . . 23

9.3.1 Auxiliary Valuations . . . . . . . . . . . . . . . . . . . 24 9.3.2 Main Valuations . . . . . . . . . . . . . . . . . . . . . 25

9.4 Machine Instructions . . . . . . . . . . . . . . . . . . . . . . . 30

10 Correctness of the PurePreScheme Compiler 33

11 The Assembler 48 11.1 Representation of the Abstract Machine . . . . . . . . . . . . 48 11.2 The Initial Environment . . . . . . . . . . . . . . . . . . . . . 49

11.2.1 Globals . . . . . . . . . . . . . . . . . . . . . . . . . . 49 11.2.2 Procedures . . . . . . . . . . . . . . . . . . . . . . . . 49

11.3 Representation Of Data . . . . . . . . . . . . . . . . . . . . . 49 11.4 Assembling Bytecode . . . . . . . . . . . . . . . . . . . . . . . 50

11.4.1 Assemble . . . . . . . . . . . . . . . . . . . . . . . . . 50 11.4.2 Assemble-proc-code . . . . . . . . . . . . . . . . . . . 55 11.4.3 Assemble-proc-rep . . . . . . . . . . . . . . . . . . . . 55

Abstract

This document gives a summary of activities under MITRE Contract Number F19628-89-C-001. It gives a detailed denotational specification of the language Pure PreScheme. A bytecode compiler, derived from the semantics, is presented, followed by proofs of correctness of the compiler with respect to the semantics. Finally, an assembler from the bytecode to an actual machine architecture is shown.

1 Introduction

The goal of this project was to develop a verified compiler for the PreScheme programming language. PreScheme is a restricted dialect of Scheme. It is simpler than Scheme in the data types it supports, in its treatment of procedure objects, and because it makes very limited use of the run-time stack.

This report is divided into two parts. Sections 1 through 6 give a chronologically-organized summary of the workplan and the activities performed under this contract. Sections 7 through 11 then give the technical details and the proof of correctness of the Pure PreScheme compiler.

The workplan was divided into three parts:

1. Analysis of the syntax and semantics of PreScheme. Our activities here are discussed in Sections 2–3. The detailed syntax and semantics are presented in Sections 7–8.

2. Development and verification of a translator from Pure PreScheme into an abstract assembly language. This activity is discussed in Section 4. The compiler is presented in Section 9, and the proofs are presented in Section 10.

3. Development of a translator from the abstract assembly language to the final target language. This activity is discussed in Section 4, and the details of the assembler are presented in Section 11.

The executable versions of the compiler and assembler, coded in Scheme, have been electronically delivered and are now being tested by MITRE, Inc.

2 Obtaining an executable Scheme semantics

Our first undertaking was the translation of the denotational semantics of Scheme into SPS, a type-checked variant of Scheme [11]. The purpose of this exercise was to obtain a version of the Scheme semantics which could be checked and manipulated by machine.

To do this, we obtained from Jonathan Rees a copy of the executable version of the denotational semantics of Scheme given in Section 7.2 of [7]. We then modified it to fit in the semantic framework given by SPS. The resulting interpreter was run on a number of examples.

This exercise confirmed that in general, the Section 7.2 semantics was consistent (i.e., it contained no type errors). However it did reveal a few shortcomings of the Section 7.2 semantics and the Clinger-Rees executable semantics (CRES):

• concrete syntax: this is specified in the Report, but it is not included in the CRES. SPS requires that concrete syntax be fully specified, and we have done this.

• non-compositionality: the treatment of permute in the Report is somewhat non-compositional, as it works on lists of expressions, rather than lists of denotations. This is fixed in our version.

• storage allocation for constants: the report is silent on whether storage for constants is allocated at read time or at evaluation time. We have chosen the latter.

A more detailed discussion of our findings can be found in [6]. We also developed some tools to translate a grammar in SPS format to Latex and to preview the grammar in a window.

3 Refining the PreScheme semantics

Originally, PreScheme was defined as the set of programs which a particular program (the PreScheme compiler) could translate into C. This definition was necessarily imprecise. Therefore, our first major task was to produce a more precise syntax and semantics for PreScheme. We undertook this task by interviewing the participants (mostly Richard Kelsey) and by examining the corpus of PreScheme code in the Virtual Machine definition.

As a result of these discussions, we have refined PreScheme into three levels:

1. Full PreScheme. This includes the code in the VM, essentially unchanged, including macro definitions. This dialect is unmanageable because the language of macro definitions is full Scheme.

2. Macro-Free PreScheme (MFPS). This is obtained from Full Pre-Scheme by expanding all macros.

3. Pure PreScheme (PPS). This is a tail-recursive, closure-free dialect of PreScheme, obtained from MFPS by hoisting lambda-expressions and beta-expansion. This dialect is semantically tractable and was the focus of our compiler development efforts.

We continued our discussions with Richard Kelsey, John Ramsdell, and Joshua Guttman to agree on the primitives and syntax of Pure PreScheme. Here we list the primary conclusions of those discussions, along with some of the implications of those decisions:

1. Pure PreScheme programs are tail-recursive. The original conception of PreScheme allowed bounded non-tail recursion; however, we agreed that the restriction to pure tail recursion was acceptable. This requires some minor recoding of the VM, since there are some calls to the garbage collector which are not tail recursive. However, since there are no nested calls, this recoding should be easy.

2. Pure PreScheme programs are closure-free: that is, closures are never created at run-time. All lambda-expressions can, at least in principle, be hoisted to a top-level scope. John Ramsdell has written a translator from MFPS to Pure PreScheme that performs this hoisting.

The global structure of a PPS program consists of some global variables (including mutable globals, lexically distinguishable by names of the form *name*), followed by a large letrec containing all the mutually recursive procedures.

In particular, this means that the primitive goto has been dropped. Both global procedures and those which are given by a local recursion will be called as ordinary procedures. This distinction was an artifact of the C implementation of PreScheme.

3. Local variables of procedures are not mutable.

4. Procedures will no longer be storable. The semantic overhead of this facility was considerable. It is used in only one place in the VM, to build a dispatch table for the opcode interpreter. This dispatch table, an array of procedures, was built once at VM initialization time, and never modified. This will be replaced by a computed-goto expression called choose. This also requires some recoding in the VM.

Eliminating procedures as storables considerably simplifies the semantics of the heap, which will be approximately that of C. Heap primitives perform something like malloc to create vectors, and vector indices are pointers.

5. The following are the primitives of PreScheme:

not
unassigned
error
%+ %- %* %< %<= %= %>= %> %quotient %remainder %abs
%adjoin-bits %low-bits %high-bits
%bitwise-not %bitwise-and %bitwise-ior %bitwise-xor
%ashl %ashr
%ascii->char %char->ascii
%char=? %char<?
%useful-bits-per-word
%make-vector %vector-ref %vector-set! %vector-length
%vector-posq %vector-fill!
%make-string %{\bf string-set}!   ;for extract-string
%string-length %string-ref
%make-byte-vector
%byte-vector-fill!
%byte-vector-ref      %byte-vector-set!
%byte-vector-word-ref %byte-vector-word-set!
%make-byte-vector-pointer
%byte-vector-pointer-ref
%byte-vector-pointer-set!
%byte-vector-pointer-word-ref

4 DEVELOPMENT OF THE PRESCHEME BYTE-CODE COMPILER7

%byte-vector-pointer-word-set!
;; I/O
%read-char %write-char %write-string
%newline
%eof-object?
%open-input-file    %open-output-file
%close-input-port   %close-output-port
%current-input-port %current-output-port
%force-output
;; Used only by READ-IMAGE and WRITE-IMAGE
%write-number %read-number
%write-page   %read-page
%write-byte   %read-byte    %bits-per-io-byte
%call-with-output-file %call-with-input-file ;ditto

These will be treated as keywords, so they will not be shadowable by lambda-bindings. The Pure PreScheme compiler will not necessarily deal with all these primitives, but will implement a subset large enough to handle the VM as recoded by the MITRE group.

The following were treated as PreScheme primitives in the original version of the VM, but were removed as primitives in light of our discussions:

goto computed-goto label run-machine halt-machine
make-dispatch-table define-dispatch! dispatch

The grammar and semantics for PPS programs is shown in Section 8. The semantics was developed by retrofitting the SPS Scheme semantics to the restrictions listed above.

4 Development of the PreScheme Byte-Code Compiler

The next stage was the development of a translator from Pure PreScheme to a combinator-based (byte-code) abstract assembly language. Byte code appeared to be a suitable target language for this compiler because the quantities manipulated by the byte code abstract machine were sufficiently close to ordinary machine quantities that the translation from byte code to machine code would be straightforward. This is in contrast with the situation for full Scheme, in which the representation of these quantities was one of the major difficulties.

The compiler was developed using the Wand-Clinger compiler development methodology [2, 8, 9, 10]. In this methodology, the denotational semantics of the source language is taken as a concrete semantics: a translation into some lambda-calculus. This translation is then modified to produce terms in a combinatory calculus. The operational semantics of the lambdacalculus, given by reduction, then yields an operational semantics for the target language.

This approach is made feasible by the observation that for suitable choices of combinators, the reduction sequences mimic precisely the behavior of ordinary machines. In the original papers [8, 9, 10], the correctness of the compiler was just equality between the combinator semantics and the original semantics. Clinger [2] showed how to produce a specification relating the combinator semantics and the original semantics in which the combinator terms clearly resembled ordinary byte codes; this avoided the linearization or distribution step in the original version.

The development of the Pure PreScheme Byte-Code Compiler had three main steps:

1. Development of the induction hypotheses. An induction hypothesis was developed for each non-terminal in the Pure PreScheme grammar. These were obtained by retrofitting the hypotheses in [2] to the restrictions of the Pure PreScheme architecture. In particular, we needed to eliminate the run-time recursion stack and to distinguish non-terminals that are executed for effect only. In our implementation, a small stack is still used for handling local variables, but this could be replaced by a register file.

2. Derivation of the byte codes. In this development method, the induction hypotheses serve as the specification for the compiler. One can then substitute the semantic equations for each production and essentially solve the equations to derive the behavior of the needed opcodes. This notion of derivation is not shown in this report, but the results are presented in the opcode definitions of Section 9.4.

3. Implementation of the translator proper. This was a straightforward programming exercise in Scheme.

We also implemented an interpreter for the byte-code language, using the definitions of the byte codes as Scheme definitions. Thus the interpreter came essentially for free from the theory.

5 Development of the Assembler

In order to make this compiler a usable tool, two more items were needed:

1. A hoister-expander to translate from MFPS to PPS. This task was accomplished by John Ramsdell.

2. A translator from byte code to real assembly language.

We implemented the byte code machine by designing a fairly straightforward representation scheme for the quantities in the byte code machine, and writing a translator that emitted MC68020 code to simulate its action. Because the quantities in Pure PreScheme, and therefore in the byte codes, were relatively simple, this was easy.

We used a tagged architecture to aid with debugging and because the PreScheme semantics might demand it. [The semantics does not completely specify the behavior of a program in the presence of a run-time type error. In most cases, run-time type errors invoke the continuation wrong, which is not specified in the semantics. If wrong is interpreted to return a don’t-care value, then any behavior is acceptable, and a tagged architecture is unnecessary. If the value of wrong is deemed significant, then the implementation must test for run-time type errors. We chose to be conservative and take the latter interpretation.]

Another part of the translator was the implementation of the primitives. We chose to implement the following primitives, which were representative of the entire list:

%abort %zero? %= %> %< %<= %+ %- %*
%make-vector %vector-ref %vector-set!

For each primitive, it was necessary to emit assembly code that performed the operation.

The major complication was representing global procedures, which are the only closures in the system. This is discussed in Section 11.

6 Conclusions and Further Work

We have specified the semantics of Pure PreScheme and proved the correctness of a compiler from Pure PreScheme to a byte code. The correctness proof consists of a straightforward structural induction whose individual steps are accomplished in the lambda-calculus. The complete proof is given in this report. The byte-code to assembly-language translation is viewed as straightforward and self-evidently correct, though such a judgement is of course subject to debate.

As of this writing, the compiler is being tested using on a small virtual machine definition for the pure lambda-calculus. Once that is completed, work can progress on using it to compile the Scheme48 VM.

We currently envision extensions of this work in at least four directions, each of which will serve the overall goal of increasing the reliability and trustworthiness of compilers:

1. Machine support for checking or generating proofs of the form displayed here. We are working on this at the present time [1]

2. Formalizing the semantics of the target machine and the correctness of the representation strategies used to implement the byte-code machine. This was a major problem for the VM correctness proof. Some work is underway on this elsewhere [3], but we believe that our methods may lead to significant advances on this problem.

3. Extending the Wand-Clinger methodology to compilers that perform significant optimizations. Some first steps toward this are reported in [5] and [12].

4. Compiling Scheme by translating Scheme programs to Pure PreScheme programs.

7 Language Overview

This section begins the technical portion of this document. It begins with an overview of the Pure PreScheme language. Section 8 gives the syntax and denotational semantics of the language. Section 9 presents the compiler, and Section 10 presents the correctness proof. Last, Section 11 describes the assembler from byte codes to assembly language.

Pure PreScheme is a descendent of the language PreScheme, invented by Jonathan Rees and Richard Kelsey for the Scheme48 compiler. A Pure PreScheme program consists of an initial declaration of global variables, top level procedure declarations, and a body. All global variables are enclosed within asterisks (e.g. *global*) and are the only variables which can be affected imperatively. The syntax of PurePreScheme has been designed so that all procedures and the main body are tail-recursive. Nested procedure calls can occur in ‘simple’ expressions where it can be assured that no recursion will occur, that is, wherever it would be safe to expand the procedure call in-line. Procedures can be passed upwards and downwards but cannot be cannot be created dynamically. Other expressed values available in PurePreScheme are integers, characters, booleans, and byte pointers.

8 The Semantics

The specification of PurePreScheme is a straightforward exercise in denotational semantics.

The only unusual aspect has to do with the environments. Specifically, they can contain either pointers into the store for globals or expressible values for locals; this must be taken into account. We use the notation ρ[−/−] for the simultaneous extension of an environment by a list of bindings; the usual one-point environment update is therefore written as ρ[⟨δ⟩/⟨I⟩]. The behavior of extension when the list of identifiers contains duplicates is unspecified. We also need a notion of sequential environment extension. This notion and notation are defined by the following axioms:

ρ[⟨ ⟩/⟨ ⟩]^{∗} = ρ
ρ[(δ :: δ^{∗})/(I :: I^{∗})]^{∗} = (ρ[⟨δ⟩/⟨I⟩])[δ^{∗}/I^{∗}]^{∗}

Here ⟨ ⟩ denotes an empty sequence and (α :: α^{∗}) denotes adding α to a sequence of α′s, α^{∗}. Similarly, (α_{0}^{∗} : α_{1}^{∗}) denotes the concatenation of two sequences of α′s.

8.1 Syntax

The input to the language is assumed to be a list structure; therefore the lexical structure of the language is unspecified, except that global identifiers are Scheme symbols distinguished by being surrounded by asterisks (e.g. *global-variable*). The nonterminals of the language are as follows:

L ∈ LocIde local identifiers G ∈ GloIde global identifiers I ∈ Ide local & global identifiers K ∈ Con constants P ∈ Prim primitives LSD ∈ LocSimDec local simple declarations GSD ∈ GloSimDec global simple declarations LPD ∈ LocProcDec local procedure declarations S ∈ Simple simple expressions & commands T ∈ Tre tail-recursive expressions E ∈ Pgm programs

The starting symbol is Pgm.

The productions are:

LSD ::= (L S)^{∗}
GSD ::= (G S)^{∗}
LPD ::= (L (lambda (L^{∗}) T))^{∗}

S ::= K

    |  L
    |  G
    |  (if S_{0} S_{1} S_{2})
    |  (choose S (S^{∗}))
    |  (set! G S)

    |  (P S^{∗})

T ::= S

    |  (if S T_{0} T_{1})
    |  (begin S^{∗} T)
    |  (let (LSD) T)
    |  (let* (LSD) T)
    |  (S S^{∗})

E ::= (let* (GSD) (letrec (LPD) T))

8.2 Value Domains

α ∈ L locations/denoted values ν ∈ N small integers

T = {false, true} truth values H characters

ϕ ∈ F = E^{∗} → C procedures β ∈ B byte pointers υ ∈ P = E^{∗} → K → C primitives ω ∈ O = U → F openers χ ∈ X error messages ϵ ∈ E = N + T + H + F + B expressed/stored values σ ∈ S = L → E stores δ ∈ D = L + E denoted values ρ ∈ U = Ide → D environments θ ∈ C = S → A command continuations κ ∈ K = E → C expression continuations

A answers

These domains are all standard, except for the domain of openers; these are procedures (closures) that are waiting to receive the environment in which they will be closed.

A distinguishing characteristic of these domains is that all the expressed values can naturally fit in one machine word, except for procedures, which must be represented by pointers. Note also that procedures do not take continuations, since they are tail-recursive.

8.3 Semantic Functions

The semantic functions include three auxiliary functions for analyzing declarations, and one main valuation for each syntactic category. Note that T does not take a continuation argument, since these are tail-recursive expressions, which do not use a run-time stack.

GL :  LocSimDec → LocIde^{∗}
GP :  LocProcDec → LocIde^{∗}
GG :  GloSimDec → GloIde^{∗}

K : Con → E

P :  Prim → P

DL : LocSimDec → U → (E^{∗} → C) → C SDL : LocSimDec → U → (E^{∗} → C) → C SDG : GloSimDec → U → (L^{∗} → C) → C

RP : LocProcDec → LocIde^{∗} → U → E^{∗} → E^{∗}

RDP : LocProcDec → U → (E^{∗} → C) → C SE : Simple → U → K → C SE^{∗} : Simple^{∗} → U → (E^{∗} → C) → C SEC^{∗} : Simple^{∗} → N → U → K → C SC : Simple → U → C → C SC^{∗} : Simple^{∗} → U → C → C SCC^{∗} : Simple^{∗} → N → U → C → C T : Tre → U → C E : Pgm → U → C

8.3.1 Auxiliary Valuations

These valuations extract sequences of identifiers from various declarations.

GL : LocSimDec → LocIde^{∗}

Get Locals. Extracts local identifiers from local simple declarations.

GL[[ ]] = ⟨ ⟩

GL[[(L S) LSD]] = (L :: GL[[LSD]])

8 THE SEMANTICS 15

GP : LocProcDec → LocIde^{∗}

Get Procedures. Extracts procedure identifiers from local procedure declarations. GP[[ ]] = ⟨ ⟩

GP[[(L (lambda (L^{∗}) T)) LPD]] = (L :: GP[[LPD]])
GG : GloSimDec → GloIde^{∗}

Get Globals. Extracts global identifiers from global simple declarations. GG[[ ]] = ⟨ ⟩ GG[[(G S) GSD]] = (G :: GG[[GSD]])

8.3.2 Main Valuations K : Con → E

Constants. [definition deliberately omitted]

P : Prim → P

Primitives. [definition deliberately omitted]

DL : LocSimDec → U → (E^{∗} → C) → C 8 THE SEMANTICS 16

Declare Locals. Takes a sequence of local simple declarations and returns a corresponding sequence of values of the simple expressions. DL[[ ]] = λρψ . ψ ⟨ ⟩ DL[[(L S) LSD]] = λρψ . DL[[LSD]]ρ(λϵ^{∗} . SE[[S]]ρ(λϵ . ψ (ϵ :: ϵ^{∗})))

SDL : LocSimDec → U → (E^{∗} → C) → C

Sequentially Declare Locals. Takes a sequence of local simple declarations and returns a corresponding sequence of values of the simple expressions. The environment is updated as each simple expression is evaluated. SDL[[ ]] = λρψ . ψ ⟨ ⟩ SDL[[(L S) LSD]] = λρψ . SE[[S]]ρ(λϵ . SDL[[LSD]]ρ[⟨ϵ in D⟩/⟨L⟩]

(λϵ^{∗} . ψ (ϵ :: ϵ^{∗})))

SDG : GloSimDec → U → (L^{∗} → C) → C

Sequentially Declare Globals. Takes a sequence of global simple declarations and returns a corresponding sequence of locations in the store where values of the simple expressions are located. SDG[[ ]] = λρξ . ξ ⟨ ⟩ SDG[[(G S) GSD]] = λρξ . SE[[S]]ρ(λϵ . (tieval (λα . SDG[[GSD]]ρ[⟨α in D⟩/⟨G⟩]

(λα^{∗} . ξ (α :: α^{∗})))

ϵ))

RP : LocProcDec → LocIde^{∗} → U → E^{∗} → E^{∗}

Recursive Procedures. Takes a sequence of procedure declarations and returns a corresponding sequence of recursive procedures (when used in conjunction with RDP). More precisely, given a sequence of procedure declarations, a list of local identifiers L_{0}^{∗} (the names of the procedures in the recursive declaration), an environment ρ (the environment on entrance to the declaration), and a list of expressed values ϵ_{0}^{∗} (the values of those procedures) , it returns a list of expressed values. Each expressed value is a procedure, obtained by closing the corresponding lambda expression in the environment obtained by extending ρ by binding the identifiers in L_{0}^{∗} to the corresponding values in ϵ_{0}^{∗}.

This is used in conjunction with RDP, which uses a fixpoint operator to set up the appropriate fixpoint equation.

As noted above, the behavior of extension when the list of identifiers contains duplicates is unspecified. Therefore the behavior of RP is unspecified when either L or L_{0}^{∗} contains duplicates.

RP[[ ]] = λL^{∗}ρϵ^{∗} . ⟨ ⟩

RP[[(L (lambda (L^{∗}) T)) LPD]] =

λL_{0}^{∗}ρϵ_{0}^{∗} . (((λϵ^{∗} . T [[T]](ρ[(map (in D) ϵ_{0}^{∗})/L_{0}^{∗}])

[(map (in D) ϵ^{∗})/(reverse L^{∗})] ) in E)
:: RP[[LPD]]L_{0}^{∗}ρϵ_{0}^{∗})

RDP : LocProcDec → U → (E^{∗} → C) → C

Recursively Declare Procedures. Takes a sequence of procedure declarations and returns a corresponding sequence recursive procedures. (GP[[LPD]] calculates the list of procedure names declared in LPD, corresponding to the argument L_{0}^{∗} in the definition of RP. ρ is the environment enclosing the declaration, as in RP. Thus the argument to the fixpoint operator corresponds to λϵ^{∗} ….; the value of the fixpoint is a sequence of expressed values, which are passed to the continuation.

RDP[[LPD]] = λρψ . ψ(fix (RP[[LPD]](GP[[LPD]])ρ))

SE : Simple → U → K → C 8 THE SEMANTICS 18

Simple Expressions. Evaluates the expression and passes the value to the expression continuation. SE[[K]] = λρκ . κ(K[[K]]) SE[[L]] = λρκ . (ρL) e E → κ((ρL) | E),

(wrong “Local variable given storage.”)

SE[[G]] = λρκ . (ρG) e L → (hold ((ρG) | L) κ),

(wrong “Global variable not given storage.”)

SE[[(if S_{0} S_{1} S_{2})]] = λρκ . SE[[S_{0}]]ρ(λϵ . (ϵ | T) = false → SE[[S_{2}]]ρκ,

SE[[S_{1}]]ρκ)

SE[[(choose S (S^{∗}))]] = λρκ . SE[[S]]ρ(λϵ . ϵ e N → SEC^{∗}[[S^{∗}]](ϵ | N)ρκ

(wrong “Non-numeric argument.”))

SE[[(set! G S)]] = λρκ . SE[[S]]ρ(λϵ . (ρG) e L →(assign ((ρG) | L) ϵ (κ ϵ)),

(wrong

“Can’t assign to a local variable.”))

SE[[(P S^{∗})]] = λρκ . SE^{∗}[[S^{∗}]]ρ(λϵ^{∗} . apply-primitive P[[P]] ϵ^{∗} κ)

SE^{∗} : Simple^{∗} → U → (E^{∗} → C) → C

Simple Expression sequences. Evaluates the sequence of simple expressions and passes the sequence of values to the continuation. SE^{∗}[[ ]] = λρψ . ψ ⟨ ⟩ SE^{∗}[[S S^{∗}]] = λρψ . SE[[S]]ρ(λϵ . SE^{∗}[[S^{∗}]]ρ(λϵ^{∗} . ψ (ϵ^{∗} : ⟨ϵ⟩)))

SEC^{∗} : Simple^{∗} → N → U → K → C

Simple Expression Choose sequences. Returns the value of the simple expression in the sequence of simple expressions corresponding to the numeric choice, ν. If there is no corresponding choice an error is signaled.

SEC^{∗}[[ ]] = λνρκ . wrong “Choose: index out of bounds.” SEC^{∗}[[S S^{∗}]] = λνρκ . ν = 0 → SE[[S]]ρκ, SEC^{∗}[[S^{∗}]](ν − 1)ρκ

SC : Simple → U → C → C

Simple Commands. Evaluates the expression and but ignores the return value. SC[[K]] = λρθ . θ SC[[L]] = λρθ . θ SC[[G]] = λρθ . θ SC[[(if S_{0} S_{1} S_{2})]] = λρθ . SE[[S_{0}]]ρ(λϵ . (ϵ | T) = false → SC[[S_{2}]]ρθ,

SC[[S_{1}]]ρθ)

SC[[(choose S (S^{∗}))]] = λρθ . SE[[S]]ρ

(λϵ . ϵ e N → SCC^{∗}[[S^{∗}]](ϵ | N)ρθ,

(wrong “Non-numeric argument.”))

SC[[(set! G S)]] = λρθ . SE[[S]]ρ(λϵ . (ρG) e L →(assign ((ρG) | L) ϵ θ),

(wrong

“Can’t assign to a local variable.”))

SC[[(P S^{∗})]] = λρθ . SE^{∗}[[S^{∗}]]ρ(λϵ^{∗} . apply-primitive/ignore P[[P]] ϵ^{∗} θ)

SC^{∗} : Simple^{∗} → U → C → C

Simple Command sequences. Evaluates the sequence of simple expressions ignoring the values. SC^{∗}[[ ]] = λρθ . θ SC^{∗}[[S S^{∗}]] = λρθ . SC[[S]]ρ(SC^{∗}[[S^{∗}]]ρθ)

SCC^{∗} : Simple^{∗} → N → U → C → C

Simple Command Choose sequences. Evaluates of the simple expression in the sequence of simple expressions corresponding to the numeric choice, ν, ignoring the value. If there is no corresponding choice an error is signaled. SCC^{∗}[[ ]] = λνρθ . wrong “Choose: index out of bounds.” SCC^{∗}[[S S^{∗}]] = λνρκ . ν = 0 → SC[[S]]ρθ, SCC^{∗}[[S^{∗}]](ν − 1)ρθ

Tail-recursive expressions. Evaluates the tail-recursive expression and returns the value. As the expressions are tail-recursive, no continuation is necessary. κ_{0} is the initial continuation for the program. This is unspecified. T : Tre → U → C T [[S]] = λρ . SE[[S]]ρκ_{0} T [[(if S T_{0} T_{1})]] = λρ . SE[[S]]ρ(λϵ . (ϵ | T) = false → T [[T_{1}]]ρ, T [[T_{0}]]ρ) T [[(begin S^{∗} T)]] = λρ . SC[[S^{∗}]]ρ(T [[T]]ρ) T [[(let (LSD) T)]] = λρ . DL[[LSD]]ρ(λϵ^{∗} . T [[T]]ρ[(map (in D) ϵ^{∗})/GL[[LSD]]]) T [[(let* (LSD) T)]] = λρ . SDL[[LSD]]ρ

(λϵ^{∗} . T [[T]]ρ[(map (in D) ϵ^{∗})/GL[[LSD]]]^{∗})

T [[(S S^{∗})]] = λρ . SE^{∗}[[S^{∗}]]ρ(λϵ^{∗} . SE[[S]]ρ(λϵ . (tail-apply ϵ ϵ^{∗})))

E : Pgm → U → C

Expressions. Sequentially declares any globals, then recursively defines any procedures in the updated environment, and finally evaluates the tail recursive body in the resulting environment.

E[[(let* (GSD) (letrec (LPD) T))]] =

λρ . SDG[[GSD]]ρ

(λα^{∗} . RDP[[LPD]]ρ[(map (in D) α^{∗})/GG[[GSD]]]^{∗}
(λϵ^{∗} . T [[T]](ρ[(map (in D) α^{∗})/GG[[GSD]]]^{∗})
[(map (in D) ϵ^{∗})/GP[[LPD]]]))

8 THE SEMANTICS 21

8.4 Auxiliary Functions

wrong : X → C [definition deliberately omitted]

new : S → L [definition deliberately omitted]

hold : L → K → C hold = λακ . λσ . κ(σ α)σ

update : L → E → S → S update = λαϵσ . λα_{0} . α_{0} = α → ϵ, σα_{0}

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

tieval : (L → C) → E → C tieval = λξϵ . λσ . ξ(new σ)(update (new σ) ϵ σ)

apply-primitive : P → E^{∗} → K → C apply-primitive = λυϵ^{∗}κ . υϵ^{∗}κ

apply-primitive/ignore : P → E^{∗} → C → C apply-primitive/ignore = λυϵ^{∗}θ . υϵ^{∗}(λϵ . θ)

tail-apply : F → E^{∗} → C tail-apply = λϵϵ^{∗} . ϵ e F → (ϵ | F)ϵ^{∗}, (wrong “Non-function to apply”)

9 The Compiler

The compiler for PurePreScheme produces code for an abstract machine consisting of a runtime environment, μ, and stack, ζ. The stack is used only for the storage of temporaries within an expression, and is not used for control purposes. A byte-code program is a term π of type Q = U_{r} → E^{∗} → C. Hence a typical machine configuration is a term of the form πμζ.

Though the machine is defined denotationally, machine configurations are given an operational semantics by inheritance from the operational semantics (that is, the reduction behavior) of the lambda-calculus. The bytecode terms are carefully defined so that if π is a legal bytecode program, then πμζ reduces to a term π′μ′ζ′ in some small number of reduction steps. Furthermore, since all these terms are in continuation-passing style, there is essentially only one such reduction that is possible. Therefore we can interpret this reduction sequence as a step in the operational semantics of the machine: πμζ ⇒ π′μ′ζ′. This notion of operational semantics is familiar to any Scheme programmer and in fact goes back at least 30 years to McCarthy, who first recognized the relation between tail-recursive program schemes and ordinary iteration [4].

For tail-recursive expressions, the compiler takes a symbol table γ and produces code. In the case of non tail-recursive constructs, the compiler takes not only γ but also a code continuation π, consisting of the code to follow the code generated.

We assume the existence of functions for extending run-time and compiletime environments. A runtime environment μ and a symbol table γ form a representation (distributed across different times!) of an environment (μ ∘ γ). We need to ensure that the run-time and compile-time extension functions behave consistently. The behavior of these functions must satisfy the following for any μ and γ:

((μ ∘ γ))[(map (in D) ϵ^{∗})/L^{∗}] = ((extends_{r l} μ ϵ^{∗}) ∘ (extends_{c l} γ L^{∗}))

((μ ∘ γ))[(map (in D) ϵ^{∗})/L^{∗}]^{∗} = ((extends_{r l}^{∗} μ ϵ^{∗}) ∘ (extends_{c l}^{∗} γ L^{∗}))

((μ ∘ γ))[(map (in D) α^{∗})/G^{∗}]^{∗} = ((extends_{r g}^{∗} μ α^{∗}) ∘ (extends_{c g}^{∗} γ G^{∗}))

The standard implementation of lexical addresses satisfies these axioms.

In addition, the procedures top, take-first, and pop-first are used to manipulate the runtime stack. These are assumed to satisfy the following:

(top (ϵ :: ζ)) = ϵ

(take-first 0 ζ) = ⟨ ⟩

(take-first (n + 1 + (ϵ :: ζ)) = (ϵ :: (take-first n ζ))

(pop-first 0 ζ) = ζ

(pop-first (n + 1) (ϵ :: ζ)) = (pop-first n ζ)

The compiler itself is presented in terms of its semantics. Thus we write:

CSDL[[ ]] = λγπ . π

CSDL[[(L S) LSD]] = λγπ . CSE[[S]]γ

(add-to-env* (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π))

However, as we did for the semantics, we envision this as a concrete semantics, yielding combinator terms of type Q rather than values in Q. For this translation, we assume that all arguments to compiler procedures (in this case, the syntactic argument, γ, and π) are compile-time values, and all results of compiler procedures (always of type Q) are run-time values, that is, at compile-time they appear as terms of type Q. Thus, using the back-quote convention of Lisp, we might translate the fragment above into code like the following:

(define csdl
  (lambda (locsimdec gamma pi)
    (record-case locsimdec
      (empty-locsimdec () pi)
      (composite-locsimdec (l s lsd)
(cse s gamma
     (add-to-env*
       (csdl lsd (extends*-cl gamma (list l)) pi)))))))

This code might be pure semantics, but we can specify a pass separation by revealing the definition of add-to-env* as:

(define add-to-env*
  (lambda (q)
    `(add-to-env* ,q)))

or equivalently

(define add-to-env*
  (lambda (q)
    (list 'add-to-env* q)))

This specifies that the output of this program is a term: a byte-code program. We obtain a compiler by assuming that each of the procedures listed as a machine instruction below is implemented by such a back-quote procedure. The semantics of the resulting byte-code program is given by replacing each byte-code symbol by its semantics.

9.1 Compiler Syntactic Domains

The syntactic domains for the compiler are the same as those for the semantics.

9.2 Compiler Value Domains

α ∈ L locations/denoted values ν ∈ N small integers

T = {false, true} truth values H characters

ϕ ∈ F = E^{∗} → C procedures β ∈ B byte pointers υ ∈ P = E^{∗} → K → C primitives ω ∈ O = U → F openers χ ∈ X error messages ϵ ∈ E = N + T + H + F + B expressed/stored values σ ∈ S = L → E stores δ ∈ D = L + E denoted values ι ∈ D_{c} lexical values γ ∈ U_{c} = Ide → D_{c} compiler environments μ ∈ U_{r} = D_{c} → D runtime environments ρ ∈ U = Ide → D environments θ ∈ C = S → A command continuations κ ∈ K = E → C expression continuations π ∈ Q = U_{r} → E^{∗} → C byte code A answers

These are all the same as in the semantics, except for the new domains of compiler environments (symbol tables), runtime environments (displays), lexical values (or lexical addresses)

9.3 Compiler Semantic Functions

GL :  LocSimDec → LocIde^{∗}
GP :  LocProcDec → LocIde^{∗}
GG :  GloSimDec → GloIde^{∗}

K : Con → E

P :  Prim → P

CDL : LocSimDec → U_{c} → Q → Q CSDL : LocSimDec → U_{c} → Q → Q CSDG : GloSimDec → U_{c} → Q → Q

CRP LocProcDec → LocIde^{∗} → O

CRDP : LocProcDec → U_{c} → Q → Q CSE : Simple → U_{c} → Q → Q CSE^{∗} : Simple^{∗} → U_{c} → Q → Q CSEC^{∗} : Simple^{∗} → U_{c} → Q → Q CSC : Simple → U_{c} → Q → Q CSC^{∗} : Simple^{∗} → U_{c} → Q → Q CSCC^{∗} : Simple^{∗} → U_{c} → Q → Q CT : Tre → U_{c} → Q CE : Pgm → U_{c} → Q

9.3.1 Auxiliary Valuations

GL : LocSimDec → LocIde^{∗}

[definition same as for semantics]

GP : LocProcDec → LocIde^{∗}

[definition same as for semantics]

GG : GloSimDec → GloIde^{∗}

[definition same as for semantics]

9.3.2 Main Valuations K : Con → E

[definition same as for semantics]

P : Prim → P

[definition same as for semantics]

CDL : LocSimDec → U_{c} → Q → Q

Compile Declare Locals. Takes a sequence of local simple declarations and generates code which pushes onto the runtime stack the corresponding sequence of values of the simple expressions. CDL[[ ]] = λγπ . π CDL[[(L S) LSD]] = λγπ . CDL[[LSD]]γ(CSE[[S]]γπ)

CSDL : LocSimDec → U_{c} → Q → Q

Compile Sequentially Declare Locals. Takes a sequence of local simple declarations and generates code which pushes onto the runtime stack the corresponding sequence of values of the simple expressions. The environment is updated as each simple expression is evaluated.

CSDL[[ ]] = λγπ . π

CSDL[[(L S) LSD]] = λγπ . CSE[[S]]γ

(add-to-env* (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π))

CSDG : GloSimDec → U_{c} → Q → Q

Compile Sequentially Declare Globals. Takes a sequence of global simple declarations and generates code which pushes onto the runtime stack a corresponding sequence of locations in the store where values of the simple expressions are located.

CSDG[[ ]] = λγπ . π

CSDG[[(G S) GSD]] = λγπ . CSE[[S]]γ

(add-global-to-env* (CSDG[[GSD]](extends_{c g}^{∗} γ ⟨G⟩) π))

CRP : LocProcDec → LocIde^{∗} → U_{c} → O

Compile Recursive Procedures. Takes a sequence of procedure declarations and generates code which pushes onto the runtime stack the corresponding sequence recursive procedures (when used in conjunction with CRDP).

CRP[[ ]] = λL^{∗}γ . empty-openers

CRP[[(L (lambda (L^{∗}) T)) LPD]] =

λL_{0}^{∗}γ . openers (#L^{∗}) (CT [[T]](extends_{c l} (extends_{c l} γ (reverse L^{∗})) L_{0}^{∗}))

(CRP[[LPD]]L_{0}^{∗}γ)

CRDP : LocProcDec → U_{c} → Q → Q 9 THE COMPILER 28

Compile Recursively Declare Procedures. Takes a sequence of procedure declarations and generates code which pushes onto the runtime stack a corresponding sequence recursive procedures. CRDP[[LPD]] = λγπ.closerecs (CRP[[LPD]](GP[[LPD]])γ) π

CSE : Simple → U_{c} → Q → Q

Compile Simple Expressions. Generates code which evaluates the expression and pushes the value onto the runtime stack. CSE[[K]] = λγπ . constant (K[[K]]) π CSE[[L]] = λγπ . fetch-local (γ L) π CSE[[G]] = λγπ . fetch-global (γ G) π CSE[[(if S_{0} S_{1} S_{2})]] = λγπ . CSE[[S_{0}]]γ(brf (CSE[[S_{1}]]γπ) (CSE[[S_{2}]]γπ)) CSE[[(choose S (S^{∗}))]] = λγπ . CSE[[S]]γ(numeric? (CSCE^{∗}[[S^{∗}]]γπ)) CSE[[(set! G S)]] = λγπ . CSE[[S]]γ(update-store (γ G) π) CSE[[(P S^{∗})]] = λγπ . CSE^{∗}[[S^{∗}]]γ(prim-apply #S^{∗} P[[P]] π)

CSE^{∗} : Simple^{∗} → U_{c} → Q → Q

Compile Simple Expression sequences. Evaluates the sequence of simple expressions and pushes the sequence of values onto the runtime stack. CSE^{∗}[[ ]] = λγπ . π CSE^{∗}[[S S^{∗}]] = λγπ . CSE[[S]]γ(CSE^{∗}[[S^{∗}]]γπ)

9 THE COMPILER 29 CSEC^{∗} : Simple^{∗} → U_{c} → Q → Q

Compile Simple Expression Choose sequences. Pushes the value of the simple expression in the sequence of simple expressions corresponding to the numeric choice, ν, onto the runtime stack. If there is no corresponding choice an error is signaled. CSEC^{∗}[[ ]] = λγπ . out-of-bounds CSEC^{∗}[[S S^{∗}]] = λγπ . pick (CSE[[S]]γπ) (CSEC^{∗}[[S^{∗}]]γπ)

CSC : Simple → U_{c} → Q → Q

Compile Simple Commands. Evaluates the expression and but does not push the value onto the runtime stack. CSC[[K]] = λγπ . π CSC[[L]] = λγπ . π CSC[[G]] = λγπ . π CSC[[(if S_{0} S_{1} S_{2})]] = λγπ . CSE[[S_{0}]]γ(brf (CSC[[S_{1}]]γπ) (CSC[[S_{2}]]γπ)) CSC[[(choose S (S^{∗}))]] = λγπ . CSE[[S]]γ(numeric? (CSCC^{∗}[[S^{∗}]]γπ)) CSC[[(set! G S)]] = λγπ . CSE[[S]]γ(update-store/ignore (γ G) π) CSC[[(P S^{∗})]] = λγπ . CSE^{∗}[[S^{∗}]]γ(prim-apply/ignore #S^{∗} P[[P]] π)

CSC^{∗} : Simple^{∗} → U_{c} → Q → Q

Compile Simple Command sequences. Evaluates the sequence of simple expressions ignoring the values.

CSC^{∗}[[ ]] = λγπ . π CSC^{∗}[[S S^{∗}]] = λγπ . CSC[[S]]γ(CSC^{∗}[[S^{∗}]]γπ)

CSCC^{∗} : Simple^{∗} → U_{c} → Q → Q

Compile Simple Command Choose sequences. Evaluates of the simple expression in the sequence of simple expressions corresponding to the numeric choice, ν, ignoring the value. If there is no corresponding choice an error is signaled. CSCC^{∗}[[ ]] = λγπ . out-of-bounds CSCC^{∗}[[S S^{∗}]] = λγπ . pick (CSC[[S]]γπ) (CSCC^{∗}[[S^{∗}]]γπ)

CT : Tre → U_{c} → Q

Compile Tail-recursive expressions. Generates code which evaluates the tail-recursive expression and pushes the value onto the runtime stack. As the expressions are tail-recursive, no code continuation is necessary for compilation. CT [[S]] = λγ . CSE[[S]]γ(halt) CT [[(if S T_{0} T_{1})]] = λγ . CSE[[S]]γ(brf (CT [[T_{0}]]γ) (CT [[T_{1}]]γ)) CT [[(begin S^{∗} T)]] = λγ . CSC[[S^{∗}]]γ(CT [[T]]γ) CT [[(let (LSD) T)]] = λγ . CDL[[LSD]]γ

(add-to-env (CT [[T]](extends_{c l} γ (GL[[LSD]]))))

CT [[(let* (LSD) T)]] = λγ . CSDL[[LSD]]γ(CT [[T]](extends_{c l}^{∗} γ (GL[[LSD]]))) CT [[(S S^{∗})]] = λγ . CSE^{∗}[[S^{∗}]]γ(CSE[[S]]γ(tail-call))

CE : Pgm → U_{c} → Q

Compile Expressions. Generates code which sequentially adds any globals to the runtime environment, then generates code using a properly updated symbol table which adds recursively defined procedures to the updated runtime environment, and finally generates code in the further updated symbol table which executes the tail recursive body in the resulting runtime environment.

CE[[(let* (GSD) (letrec (LPD) T))]] =

λγ . CSDG[[GSD]]γ(CRDP[[LPD]](extends_{c g}^{∗} γ GG[[GSD]]) (CT [[T]](extends_{c l} (extends_{c g}^{∗} γ GG[[GSD]]) GP[[LPD]])))

9.4 Machine Instructions

In this section, we specify the semantics of each machine instruction. As noted above, a compiler is obtained instead if we replace each of these procedures by a procedure that emits the appropriate code.

constant : E → Q → Q

constant = λϵπ . λμζ . (πμ(ϵ :: ζ))

fetch-local : D_{c} → Q → Q

fetch-local = λιπ . λμζ . (μ ι) e E → πμ(((μ ι) | E) :: ζ)), (wrong “Local variable given storage.”)

fetch-global : D_{c} → Q → Q

fetch-global = λιπ . λμζ . (μ ι) e L → (hold ((μ ι) | L) (λϵ.πμ(ϵ :: ζ))), (wrong “Global variable not given storage.”)

9 THE COMPILER 32 brf : Q → Q → Q brf = λπ_{0}π_{1}λμζ . ((top ζ) | T) = false → (π_{1}μ(pop-first 1 ζ)), (π_{0}μ(pop-first 1 ζ))

numeric? : Q → Q numeric? = λμζ . (top ζ) e N → (πμζ), (wrong “Non-numeric argument.”))

update-store : D_{c} → Q → Q update-store = λιπ . λμζ . (μ ι) e L →

(assign (μ ι) | L) (top ζ) (πμζ)),

(wrong “Can’t assign to a local variable”)

prim-apply : N → P → Q → Q prim-apply = λνυπ . λμζ . (apply-primitive υ (take-first ν ζ) (λϵ . πμ(ϵ :: (pop-first ν ζ))))

update-store/ignore : D_{c} → Q → Q update-store/ignore =

λιπ . λμζ . (μ ι) e L →(assign ((μ ι) | L)(top ζ) (πμ(pop-first 1 ζ))), (wrong “Can’t assign to a local variable”)

out-of-bounds : Q out-of-bounds = λμζ . wrong “Choose: index out of bounds.”

pick : Q → Q → Q pick = λπ_{0}π_{1} . λμζ . ((top ζ) | N) = 0 →

(π_{0}μ(pop-first 1 ζ)),

(π_{1}μ((((top ζ) | N − 1) | E) :: (pop-first 1 ζ)))

9 THE COMPILER 33

prim-apply/ignore : N → P → Q → Q prim-apply/ignore = λνυπ . λμζ . (apply-primitive υ (take-first ν ζ) (λϵ . πμ(pop-first ν ζ)))

halt : Q halt = λμζ . κ_{0}(top ζ)

add-to-env : Q → Q add-to-env = λπ . λμζ . π(extends_{r l} μ ζ)⟨ ⟩

add-to-env* : Q → Q add-to-env* = λπ . λμζ . π(extends_{r l}^{∗} μ ⟨(top ζ)⟩)(pop-first 1 ζ)

add-global-to-env* : Q → Q add-global-to-env* =

λπ . λμζ . tieval (λα . π(extends_{r g}^{∗} μ ⟨α⟩)(pop-first 1 ζ)) (top ζ)

empty-openers : O empty-openers = λμ . λϵ^{∗} . ⟨ ⟩

openers : N → Q → O → O openers =

λνπω . λμ . λϵ_{0}^{∗} . ((λϵ^{∗} . π(extends_{r l} (extends_{r l} μ ϵ^{∗}) ϵ_{0}^{∗})⟨ ⟩) in E :: (ωμϵ^{∗}))

tail-call : Q tail-call = λμζ . (tail-apply (top ζ) (pop-first 1 ζ))

closerecs : O → Q → Q closerecs = λωπ . λμζ . π(extends_{r l} μ (fix (ωμ)))ζ

10 Correctness of the PurePreScheme Compiler

The main statement of the correctness proof is

(CE[[PGM]]γ)μ⟨ ⟩ = E[[PGM]](μ ∘ γ)

This asserts that when the code CE[[PGM]]γ produced by compiling PGM in symbol table γ is run on the machine, starting with run-time environment μ and empty stack, the result will be the same as that of applying the semantics of E[[PGM]] of PGM to the environment (μ ∘ γ) obtained by composing μ and γ.

The proof is a tedious but straightforward structural induction. There are a total of 13 simultaneous induction hypotheses, one for each function in the compiler. Each induction hypothesis specifies the behavior of one compiler function relative to a suitable semantic valuation.

These specifications generally fall into two categories. The first flavor relates semantic valuations which do not take expression continuations to their corresponding compiler valuations. The main statement above falls into this category. The corresponding compiler functions do not take a continuation argument π. Furthermore, these program phrases run only when the run-time stack ζ is empty.

The second of induction hypothesis deals with semantic valuations which do take expression continuations. In this case code is compiled using a symbol table and the code to follow the given code, π. A typical induction hypothesis in this category is

(CSE[[S]]γπ)μζ = SE[[S]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

This asserts that when the code CSE[[S]]γπ, produced by compiling S in symbol table γ and code continuation π, is run on the machine, starting with run-time environment μ and stack ζ, the result is the same as evaluating the semantics of S with environment (μ ∘ γ) and a continuation which places the value ϵ on the stack ζ and then runs the code continuation π. Informally, this is read as “the code for S puts its result on the stack and continues with π.”

When sequences are involved, the push operation :: is typically replaced by an append operation : .

Induction Hypothesis 0 (CDL[[LSD]]γπ)μζ = DL[[LSD]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

The induction hypothesis states that running local declarations compiled using symbol table γ with the code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation which executes π in the same runtime environment but with all the values pushed onto the runtime stack.

(CDL[[ ]]γπ)μζ

= πμζ

= DL[[ ]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

(CDL[[(L S) LSD]]γπ)μζ

= (CDL[[LSD]]γ(CSE[[S]]γπ)μζ

= DL[[LSD]](μ ∘ γ)(λϵ^{∗} . (CSE[[S]]γπ)μ(ϵ^{∗} : ζ))

= DL[[LSD]](μ ∘ γ)(λϵ^{∗} . SE[[S]](μ ∘ γ)(λϵ . πμ((ϵ :: ϵ^{∗}) : ζ)))

= DL[[(L S) LSD]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

Induction Hypothesis 1

(CSDL[[LSD]]γπ)μ⟨ ⟩ = SDL[[LSD]](μ ∘ γ)(λϵ^{∗} . π(extends_{r l}^{∗} μ ϵ^{∗})⟨ ⟩)

The induction hypothesis states that running local sequential declarations compiled using symbol table γ with the code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation which executes π in with the runtime environment extended with the values and the same runtime stack.

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 36 (CSDL[[ ]]γπ)μ⟨ ⟩ = πμ⟨ ⟩ = SDL[[ ]](μ ∘ γ)(λϵ^{∗} . π(extends_{r l}^{∗} μ ϵ^{∗})⟨ ⟩)

(CSDL[[(L S) LSD]]γπ)μ⟨ ⟩ = (CSE[[S]]γ(add-to-env* (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π))μ⟨ ⟩ = SE[[S]](μ ∘ γ)(λϵ . (add-to-env* (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π))μ(ϵ :: ⟨ ⟩)) = SE[[S]](μ ∘ γ)(λϵ . (add-to-env* (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π))μ(ϵ :: ⟨ ⟩)) = SE[[S]](μ ∘ γ)(λϵ . (CSDL[[LSD]](extends_{c l}^{∗} γ ⟨L⟩)π)(extends_{r l}^{∗} μ ⟨ϵ⟩)⟨ ⟩) = SE[[S]](μ ∘ γ)(λϵ . SDL[[LSD]](μ ∘ γ)[ϵ in D/L]

(λϵ^{∗} . π(extends_{r l}^{∗} μ (ϵ :: ϵ^{∗}))⟨ ⟩))

= SDL[[LSD]](μ ∘ γ)(λϵ^{∗} . π(extends_{r l} μ ϵ^{∗})⟨ ⟩)

Induction Hypothesis 2 (CSDG[[GSD]]γπ)μ⟨ ⟩ = SDG[[GSD]](μ ∘ γ)(λα^{∗} . π(extends_{r g}^{∗} μ α^{∗})⟨ ⟩)

The induction hypothesis states that running global declarations compiled using symbol table γ with code to follow π in runtime environment μ with an empty runtime stack is the same as the semantics using composition of μ and γ for an environment with a continuation which executes π in with the runtime environment extended with the new locations and the same empty runtime stack. (CSDG[[ ]]γπ)μ⟨ ⟩ = πμ⟨ ⟩ = SDG[[ ]](μ ∘ γ)(λα^{∗} . π(extends_{r g}^{∗} μ α^{∗})⟨ ⟩)

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 37 (CSDG[[(G S) GSD]]γπ)μ⟨ ⟩ = (CSE[[S]]γ(add-global-to-env* (CSDG[[GSD]](extends_{c g}^{∗} γ ⟨G⟩) π)))μ⟨ ⟩ = SE[[S]](μ ∘ γ)

(λϵ . (add-global-to-env* (CSDG[[GSD]](extends_{c g}^{∗} γ ⟨G⟩) π))μ(ϵ :: ⟨ ⟩)) = SE[[S]](μ ∘ γ)

(λϵ . tieval (λα . (CSDG[[GSD]](extends_{c g}^{∗} γ ⟨G⟩) π)(extends_{r g}^{∗} μ ⟨α⟩)⟨ ⟩) ϵ) = SE[[S]](μ ∘ γ)

(λϵ . tieval (λα . SDG[[GSD]](μ ∘ γ)[α in D/G]

(λα^{∗} . π(extends_{r g}^{∗} μ (α :: α^{∗}))⟨ ⟩)) ϵ)

= SDG[[(G S)GSD]](μ ∘ γ)(λα^{∗} . π(extends_{r g}^{∗} μ α^{∗})⟨ ⟩)

Induction Hypothesis 3 (CRP[[LPD]]L^{∗}γ)μϵ^{∗} = RP[[LPD]]L^{∗}(μ ∘ γ)ϵ^{∗}

The induction hypothesis states that recursive procedure declarations compiled using symbol table γ running in runtime environment μ with is the same as the semantics using composition of μ and γ for an environment. (CRP[[ ]]L^{∗}γ)μϵ^{∗} = empty-openers μ ϵ^{∗} = ⟨ ⟩ = RP[[ ]]L^{∗}(μ ∘ γ)ϵ^{∗}

(CRP[[(L (lambda (L^{∗}) T)) LPD]]L_{0}^{∗}γ)μϵ_{0}^{∗} =(openers

(CT [[T]](extends_{c l} (extends_{c l} γ (reverse L^{∗})) L_{0}^{∗}))

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 38

(CRP[[LPD]]L_{0}^{∗}γ))μϵ^{∗} =(((λϵ^{∗} . (CT [[T]](extends_{c l} (extends_{c l} γ (reverse L^{∗})) L_{0}^{∗}))

(extends_{r l} (extends_{r l} μ ϵ^{∗}) ϵ_{0}^{∗})⟨ ⟩) in E)

:: (CRP[[LPD]]L_{0}^{∗}γ)μϵ^{∗})

=(((λϵ^{∗} . T [[T]]((μ ∘ γ)[(map (in D) ϵ^{∗})/reverse L^{∗}])[(map (in D) ϵ_{0}^{∗})/L_{0}^{∗}]) in E)

:: RP[[LPD]]L_{0}^{∗}(μ ∘ γ)ϵ^{∗}

= RP[[(L (lambda (L^{∗}) T)) LPD]]L_{0}^{∗}(μ ∘ γ)ϵ^{∗}

Induction Hypothesis 4 (CRDP[[LPD]]γπ)μ⟨ ⟩ = RDP[[LPD]](μ ∘ γ)(λϵ^{∗} . π(extends_{r l} μ ϵ^{∗})⟨ ⟩)

The induction hypothesis states that running recursive procedure declarations compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the runtime environment extended with the procedure and the same runtime stack. (CRDP[[LPD]]γπ)μ⟨ ⟩ = (closerecs (CRP[[LPD]](GP[[LPD]])γ) π)μ⟨ ⟩ = π(extends_{r l} μ (fix ((CRP[[LPD]](GP[[LPD]])γ)μ)))⟨ ⟩ = π(extends_{r l} μ (fix (RP[[LPD]](GP[[LPD]])(μ ∘ γ))))⟨ ⟩ = RDP[[LPD]](μ ∘ γ)(λϵ^{∗} . π(extends_{r l} μ ϵ^{∗})⟨ ⟩)

Induction Hypothesis 5 (CSE[[S]]γπ)μζ = SE[[S]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 39

The induction hypothesis states that running simple expressions compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment but with the result pushed onto the runtime stack. (CSE[[K]]γπ)μζ = (constant (K[[K]]) π)μζ = πμ((K[[K]]) :: ζ) = SE[[K]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

(CSE[[L]]γπ)μζ = (fetch-local (γ L) π)μζ = ((μ ∘ γ)L) e E →πμ((((μ ∘ γ)L) | E) :: ζ),

(wrong “Local variable given storage.”)

= SE[[L]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

(CSE[[G]]γπ)μζ = (fetch-global (γ G) π)μζ = ((μ ∘ γ)G) e L →(hold (((μ ∘ γ)G) | L) (λϵ.πμ(ϵ :: ζ))),

(wrong “Global variable not given storage.”)

= SE[[G]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

(CSE[[(if S_{0} S_{1} S_{2})]]γπ)μζ = (CSE[[S_{0}]]γ(brf (CSE[[S_{1}]]γπ) (CSE[[S_{2}]]γπ)))μζ = SE[[S_{0}]](μ ∘ γ)(λϵ . (brf (CSE[[S_{1}]]γπ) (CSE[[S_{2}]]γπ))μ(ϵ :: ζ)) = SE[[S_{0}]](μ ∘ γ)(λϵ . (ϵ | T) = false →((CSE[[S_{2}]]γπ)μζ),

((CSE[[S_{1}]]γπ)μζ))

= SE[[S_{0}]](μ ∘ γ)(λϵ . (ϵ | T) = false →SE[[S_{2}]](μ ∘ γ)(λϵ . πμ(ϵ :: γ))

SE[[S_{1}]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ)))

= SE[[(if S_{0} S_{1} S_{2})]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

(CSE[[(choose S (S^{∗}))]]γπ)μζ = (CSE[[S]]γ(numeric? (CSCE^{∗}[[S^{∗}]]γπ))μζ) = SE[[S]](μ ∘ γ)(λϵ . (numeric? (CSCE^{∗}[[S^{∗}]]γπ))μ(ϵ :: ζ)) = SE[[S]](μ ∘ γ)(λϵ . ϵ e N → (CSCE^{∗}[[S^{∗}]]γπ)μ(ϵ :: ζ),

(wrong “Non-numeric argument.”))

= SE[[S]](μ ∘ γ)(λϵ . ϵ e N → SCE^{∗}[[S^{∗}]](ϵ | N)(μ ∘ γ)(λϵ . πμ(ϵ :: ζ)),

(wrong “Non-numeric argument.”))

= SE[[(choose S (S^{∗}))]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ)) (CSE[[(set! G S)]]γπ)μζ = (CSE[[S]]γ(update-store (γ G) π))μζ = SE[[S]](μ ∘ γ)(λϵ . (update-store (γ G) π)μ(ϵ :: ζ)) = SE[[S]](μ ∘ γ)(λϵ . ((μ ∘ γ)G) e L →(assign (((μ ∘ γ)G) | L) ϵ (πμ(ϵ :: ζ))),

(wrong “Can’t assign to a local variable”))

= SE[[(set! G S)]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 41 (CSE[[(P S^{∗})]]γπ)μζ = (CSE^{∗}[[S^{∗}]]γ(prim-apply #S^{∗} P[[P]] π))μζ = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . (prim-apply #S^{∗} P[[P]] π)μ(ϵ^{∗} : ζ)) = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . apply-primitive P[[P]] (take-first #S^{∗} (ϵ^{∗} : ζ))

(λϵ . πμ(ϵ :: (pop-first #S^{∗} (ϵ^{∗} : ζ)))))

= SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . apply-primitive P[[P]] ϵ^{∗} (λϵ . πμ(ϵ :: ζ))) = SE[[(P S^{∗})]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

Induction Hypothesis 6 (CSE^{∗}[[S^{∗}]]γπ)μζ = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

The induction hypothesis states that running simple expression sequences compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment but with the resulting values pushed onto the runtime stack. (CSE^{∗}[[ ]]γπ)μζ = πμζ = SE^{∗}[[ ]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

(CSE^{∗}[[S S^{∗}]]γπ)μζ = (CSE[[S]]γ(CSE^{∗}[[S^{∗}]]γπ))μζ = SE[[S]](μ ∘ γ)(λϵ . (CSE^{∗}[[S^{∗}]]γπ)μ(ϵ :: ζ))

= SE[[S]](μ ∘ γ)(λϵ . SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : (ϵ :: ζ)))) = SE^{∗}[[S S^{∗}]](μ ∘ γ)(λϵ^{∗} . πμ(ϵ^{∗} : ζ))

Induction Hypothesis 7 (CSEC^{∗}[[S^{∗}]]γπ)μ(ϵ :: ζ) = SEC^{∗}[[S^{∗}]](ϵ | N)(μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

The induction hypothesis states that running simple expressions choose sequences compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment but with the result pushed onto the runtime stack. (CSEC^{∗}[[ ]]γπ)μ(ϵ :: ζ) = (out-of-bounds)μ(ϵ :: ζ) = wrong “Choose: index out of bounds.” = SEC^{∗}[[ ]](ϵ | N)(μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

(CSEC^{∗}[[S S^{∗}]]γπ)μ(ϵ :: ζ) = (pick (CSE[[S]]γπ) (CSEC^{∗}[[S^{∗}]]γπ))μ(ϵ :: ζ) = ((ϵ | N) = 0) → (CSE[[S]]γπ)μζ, (CSEC^{∗}[[S^{∗}]]γπ)μ(((ϵ | N − 1) | E) :: ζ) = ((ϵ | N) = 0) → SE[[S]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ)),

(CSEC^{∗}[[S^{∗}]]γπ)μ(((ϵ | N − 1) | E) :: ζ)

= ((ϵ | N) = 0) → SE[[S]](μ ∘ γ)(λϵ . πμ(ϵ :: ζ)),

SEC^{∗}[[S^{∗}]](ϵ | N − 1)(μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

= SEC^{∗}[[S S^{∗}]](ϵ | N)(μ ∘ γ)(λϵ . πμ(ϵ :: ζ))

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 43 Induction Hypothesis 8 (CSC[[S]]γπ)μζ = SC[[S]](μ ∘ γ)(πμζ)

The induction hypothesis states that running simple commands compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment and stack (i.e. the value is ignored). (CSC[[K]]γπ)μζ = πμζ = SC[[K]](μ ∘ γ)(πμζ)

(CSC[[L]]γπ)μζ = πμζ = SC[[L]](μ ∘ γ)(πμζ)

(CSC[[G]]γπ)μζ = πμζ = SC[[G]](μ ∘ γ)(πμζ)

(CSC[[(if S_{0} S_{1} S_{2})]]γπ)μζ = (CSE[[S_{0}]]γ(brf (CSC[[S_{1}]]γπ) (CSC[[S_{2}]]γπ)))μζ = SE[[S_{0}]](μ ∘ γ)(λϵ . (brf (CSC[[S_{1}]]γπ) (CSC[[S_{2}]]γπ))μ(ϵ :: ζ)) = SE[[S_{0}]](μ ∘ γ)(λϵ . (ϵμT) = false → ((CSC[[S_{2}]]γπ)μζ), ((CSC[[S_{1}]]γπ)μζ))

= SE[[S_{0}]](μ ∘ γ)(λϵ . (ϵμT) = false →SC[[S_{2}]](μ ∘ γ)(πμζ),

SC[[S_{1}]](μ ∘ γ)(πμζ))

= SC[[(if S_{0} S_{1} S_{2})]](μ ∘ γ)(πμζ)

(CSC[[(choose S (S^{∗}))]]γπ)μζ = (CSC[[S]]γ(numeric? (CSCC^{∗}[[S^{∗}]]γπ))μζ) = SE[[S]](μ ∘ γ)(λϵ . (numeric? (CSCC^{∗}[[S^{∗}]]γπ))μ(ϵ :: ζ)) = SE[[S]](μ ∘ γ)(λϵ . ϵ e N → (CSCC^{∗}[[S^{∗}]]γπ)μ(ϵ :: ζ),

(wrong “Non-numeric argument.”))

= SE[[S]](μ ∘ γ)(λϵ . ϵ e N → SCC^{∗}[[S^{∗}]](ϵ | N)(μ ∘ γ)(πμζ),

(wrong “Non-numeric argument.”))

= SC[[(choose S (S^{∗}))]](μ ∘ γ)(πμζ) (CSC[[(set! G S)]]γπ)μζ = (CSE[[S]]γ(update-store/ignore (γ G) π))μζ = SE[[S]](μ ∘ γ)(λϵ . (update-store (γ G) π)μ(ϵ :: ζ)) = SE[[S]](μ ∘ γ)(λϵ . ((μ ∘ γ)G) e L →(assign (((μ ∘ γ)G) | L) ϵ (πμζ)),

(wrong “Can’t assign to a local variable”))

= SE[[(set! G S)]](μ ∘ γ)(πμζ)

(CSC[[(P S^{∗})]]γπ)μζ = (CSE^{∗}[[S^{∗}]]γ(prim-apply/ignore #S^{∗} P[[P]] π))μζ = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . (prim-apply/ignore #S^{∗} P[[P]] π)μ(ϵ^{∗} : ζ))

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 45 = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . apply-primitive/ignore P[[P]] (take-first #S^{∗} (ϵ^{∗} : ζ))

(πμ(pop-first #S^{∗} (ϵ^{∗} : ζ))))

= SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . apply-primitive/ignore P[[P]] ϵ^{∗} (πμζ)) = SC[[(P S^{∗})]](μ ∘ γ)(πμζ)

Induction Hypothesis 9 (CSC^{∗}[[S^{∗}]]γπ)μζ = SC^{∗}[[S^{∗}]](μ ∘ γ)(πμζ)

The induction hypothesis states that running simple command sequences compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment and stack (i.e. the value is ignored). (CSC^{∗}[[ ]]γπ)μζ = πμζ = SC^{∗}[[ ]](μ ∘ γ)(πμζ)

(CSC^{∗}[[S S^{∗}]]γπ)μζ = (CSC[[S]]γ(CSC^{∗}[[S^{∗}]]γπ))μζ = SC[[S]](μ ∘ γ)((CSC^{∗}[[S^{∗}]]γπ)μζ) = SC[[S]](μ ∘ γ)(SC^{∗}[[S^{∗}]](μ ∘ γ)(πμζ)) = SC^{∗}[[S S^{∗}]](μ ∘ γ)(πμζ)

Induction Hypothesis 10 (CSCC^{∗}[[S^{∗}]]γπ)μ(ϵ :: ζ) = SCC^{∗}[[S^{∗}]](ϵ | N)(μ ∘ γ)(πμζ)

10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 46

The induction hypothesis states that running simple command choose sequences compiled using symbol table γ with code to follow π in runtime environment μ with runtime stack ζ is the same as the semantics using composition of μ and γ for an environment with a continuation executing π in with the same runtime environment and stack (i.e. the value is ignored). (CSCC^{∗}[[ ]]γπ)μ(ϵ :: ζ) = (out-of-bounds)μ(ϵ :: ζ) = wrong “Choose: index out of bounds.” = SCC^{∗}[[ ]](ϵ | N)(μ ∘ γ)(πμζ)

(CSCC^{∗}[[S S^{∗}]]γπ)μ(ϵ :: ζ) = (pick (CSC[[S]]γπ) (CSCC^{∗}[[S^{∗}]]γπ))μ(ϵ :: ζ) = (ϵ | N) = 0 → (CSC[[S]]γπ)μζ, (CSCC^{∗}[[S^{∗}]]γπ)μ(((ϵ | N − 1) | E) :: ζ) = (ϵ | N) = 0 → SC[[S]](μ ∘ γ)(πμζ), (CSCC^{∗}[[S^{∗}]]γπ)μ(((ϵ | N − 1) | E) :: ζ) = (ϵ | N) = 0 → SC[[S]](μ ∘ γ)(πμζ), SCC^{∗}[[S^{∗}]](ϵ | N − 1)(μ ∘ γ)(πμζ) = SCC^{∗}[[S S^{∗}]](ϵ | N)(μ ∘ γ)(πμζ)

Induction Hypothesis 11 (CT [[T]]γ)μ⟨ ⟩ = T [[T]](μ ∘ γ)

The induction hypothesis states that running tail recursive expressions compiled using symbol table γ in runtime environment μ with an empty runtime stack is the same as the semantics using composition of μ and γ for an environment. (CT [[S]]γ)μ⟨ ⟩ = (CSE[[S]]γ(halt))μ⟨ ⟩ = SE[[S]](μ ∘ γ)(λϵ . (halt)μ(ϵ :: ⟨ ⟩)) = SE[[S]](μ ∘ γ)(λϵ . κ_{0}ϵ) = T [[S]](μ ∘ γ)

(CT [[(if S T_{0} T_{1})]]γ)μ⟨ ⟩ = (CSE[[S]]γ(brf (CT [[T_{0}]]γ) (CT [[T_{1}]]γ)))μ⟨ ⟩ = SE[[S]](μ ∘ γ)(λϵ . (brf (CT [[T_{0}]]γ) (CT [[T_{1}]]γ))μ(ϵ :: ⟨ ⟩)) = SE[[S]](μ ∘ γ)(λϵ . (ϵ | T) = false → ((CT [[T_{1}]]γ)μ⟨ ⟩), ((CT [[T_{0}]]γ)μ⟨ ⟩)) = SE[[S]](μ ∘ γ)(λϵ . (ϵ | T) = false → T [[T_{1}]](μ ∘ γ), T [[T_{0}]](μ ∘ γ)) = T [[(if S T_{0} T_{0})]](μ ∘ γ)

(CT [[(begin S^{∗} T)]]γ)μ⟨ ⟩ = (CSC[[S^{∗}]]γ(CT [[T]]γ))μ⟨ ⟩ = SC[[S^{∗}]](μ ∘ γ)((CT [[T]]γ)μ⟨ ⟩) = SC[[S^{∗}]](μ ∘ γ)(T [[T]](μ ∘ γ)) = T [[(begin S^{∗} T)]](μ ∘ γ)

(CT [[(let (LSD) T)]]γ)μ⟨ ⟩ = (CDL[[LSD]]γ(add-to-env (CT [[T]](extends_{c l} γ (GL[[LSD]])))))μ⟨ ⟩ 10 CORRECTNESS OF THE PUREPRESCHEME COMPILER 48 = DL[[LSD]](μ ∘ γ)(λϵ^{∗} . (add-to-env (CT [[T]](extends_{c l} γ (GL[[LSD]]))))μ(ϵ^{∗} : ⟨ ⟩)) = DL[[LSD]](μ ∘ γ)(λϵ^{∗} . (CT [[T]](extends_{c l} γ (GL[[LSD]])))(extends_{r l} μ ϵ^{∗})⟨ ⟩) = DL[[LSD]](μ ∘ γ)(λϵ^{∗} . T [[T]](μ ∘ γ)[(map (in D) ϵ^{∗})/GL[[LSD]]]) = T [[(let (LSD) T)]](μ ∘ γ)

(CT [[(let* (LSD) T)]]γ)μ⟨ ⟩ = (CSDL[[LSD]]γ(CT [[T]](extends_{c l}^{∗} γ (GL[[LSD]]))))μ⟨ ⟩ = SDL[[LSD]](μ ∘ γ)(λϵ^{∗} . (CT [[T]](extends_{c l}^{∗} γ (GL[[LSD]])))(extends_{r l}^{∗} μ ϵ^{∗})⟨ ⟩) = SDL[[LSD]](μ ∘ γ)(λϵ^{∗} . T [[T]](μ ∘ γ)[(map (in D) ϵ^{∗})/GL[[LSD]]]^{∗}) = T [[(let* (LSD) T)]](μ ∘ γ)

(CT [[(S S^{∗})]]γ)μ⟨ ⟩ = (CSE^{∗}[[S^{∗}]]γ(CSE[[S]]γ(tail-call)))μ⟨ ⟩ = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . (CSE[[S]]γ(tail-call))μ(ϵ^{∗} : ⟨ ⟩)) = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . SE[[S]](μ ∘ γ)(λϵ^{∗} . (tail-call)μ(ϵ :: (ϵ^{∗} : ⟨ ⟩)))) = SE^{∗}[[S^{∗}]](μ ∘ γ)(λϵ^{∗} . SE[[S]](μ ∘ γ)(λϵ^{∗} . tail-apply ϵ ϵ^{∗})) = T [[(S S^{∗})]](μ ∘ γ) Induction Hypothesis 12 (CE[[PGM]]γ)μ⟨ ⟩ = E[[PGM]](μ ∘ γ)

The induction hypothesis states that running a program compiled using symbol table γ in runtime environment μ with an empty runtime stack is the same as the semantics using composition of μ and γ for an environment.

(CE[[(let* (GSD) (letrec (LPD) T))]]γ)μ⟨ ⟩

= (CSDG[[GSD]]γ

(CRDP[[LPD]](extends_{c g}^{∗} γ GG[[GSD]])

(CT [[T]](extends_{c l} (extends_{c g}^{∗} γ GG[[GSD]]) GP[[LPD]]))))μ⟨ ⟩

= SDG[[GSD]](μ ∘ γ)

(λα^{∗} . (CRDP[[LPD]](extends_{c g}^{∗} γ GG[[GSD]])

(CT [[T]](extends_{c l} (extends_{c g}^{∗} γ GG[[GSD]]) GP[[LPD]])))(extends_{r g}^{∗} μ α^{∗})⟨ ⟩)

= SDG[[GSD]](μ ∘ γ)

(λα^{∗} . RDP[[LPD]](μ ∘ γ)[(map (in D) α^{∗})/GG[[GSD]]]^{∗})

(λϵ^{∗} . (CT [[T]](extends_{c l} (extends_{c g}^{∗} γ GG[[GSD]]) GP[[LPD]]))
(extends_{r l} (extends_{r g}^{∗} μ α^{∗}) ϵ^{∗})⟨ ⟩))

= SDG[[GSD]](μ ∘ γ)

(λα^{∗} . RDP[[LPD]](μ ∘ γ)[(map (in D) α^{∗})/GG[[GSD]]]^{∗}) (λϵ^{∗} . T [[T]]((μ ∘ γ)[(map (in D) α^{∗})/GG[[GSD]]]^{∗}[(map (in D) ϵ^{∗})/GP[[LPD]]]))

 = E[[(let* (GSD) (letrec (LPD) T))]](μ ∘ γ)

11 The Assembler

A method for translating PurePreScheme bytecode into assembly language for a 32 bit microprocessor is now described. This methodology has been used to generate code for the Motorola MC68020 and is being used to generate code for the Motorola MC88100 risc chip.

11.1 Representation of the Abstract Machine

The abstract machine uses storage for global procedures and a small stack for temporaries inside an expression. For simplicity, we have chosen to represent these using a single small stack. Note that the size of this stack is linear in the size of the input program, and therefore all stack references could have been statically allocated. This is not the usual run-time recursion stack, which may grow unboundedly depending on the input to the program.

The initial environment, containing the globals and procedure declarations, is pushed onto the stack at program startup and remains the same throughout. The runtime environment environment, π, is built on top of the initial environment, and the runtime stack, ζ, is built on top of μ. Three global registers are used in this scheme. The first is a pointer to the initial environment, the second is a pointer to top of the runtime environment μ, and the third is a pointer to the top of the runtime stack ζ. Some bytecodes also use additional temporary registers for some intermediate values but no assumptions are about the values in these registers.

11.2 The Initial Environment

11.2.1 Globals

Globals are just represented as tagged data which is pushed onto the stack at program instantiation.

11.2.2 Procedures

Procedures are represented by a code pointer, an argument count, and an offset from the initial environment of telling where the procedure representation exists on the stack. This offset is tagged and used as the runtime representation of the procedure.

Tagged Offset Argument Count Code Pointer

11.3 Representation Of Data

For simplicity, all data is represented by 4 bytes. The current semantics of PurePreScheme necessitates runtime type tags. Tags are kept in the lower order bits:

1. Tag B = 1  byte pointers
2. Tag N = 00  small integers
3. Tag T = 0010 truth values
4. Tag H = 0110 characters
5. Tag F = 1010 global procedures

There are several advantages to this scheme. First, byte pointers only need one bit for the tag field, allowing the other 31 bits for address space. Second, numeric operations can be done with little or no tag coding/decoding. Third, as all tag bits are in the low order bits, most operations on them can be done quickly. The actual representation of data with these tags given by:

1. Representation B = B * 2 + 1

2. Representation N = N * 4

3. Representation T = true = 18, T = false = 2

4. Representation H = ascii(H) * 16 + 6

5. Representation F = (offset from top of initial env) * 16 + 10

11.4 Assembling Bytecode

Shown here is each bytecode and the corresponding translation into assembly. For basic functions are necessary for this translation. The first, generate labels, is assumed to generate labels in some sequential manner. The second, emit-i, emits assembly instructions. Similarly, the third, emit-l, emits labels, and finally, the assembler can make recursive calls to itself. Two auxiliary functions, assemble-proc-code and assemble-proc-rep, are also used for assembling the top level procedures and placing their representation in the initial environment.

The generic assembly language instructions used here are straightforward. The stack is assumed to grow in a negative fashion, i.e. the stack pointer is decremented when something is pushed on the stack. The three global registers for the initial environment, runtime environment, and local stack are referred to as μ_{0}, μ, and ζ respectively. Additional registers are refered to as r_{0} ... r_{N}. Register values can be accessed directly by naming the register, r_{0}, or can be dereferenced as pointer using the @ operator, r_{0}@(4). Constant decimal values are prefixed by a # such as #18.

11.4.1 Assemble

assemble((constant ϵ π))

;; Push value on the stack. emit-i(push ϵ,ζ) assemble(π)

assemble((fetch-local ι π))

;; Find the local in the environment μ ;; and push its value on the stack. emit-i(move μ@(ι),r_{0}) emit-i(push r_{0},ζ) assemble(π)

assemble((fetch-global ι π))

;; Find the global in the environment μ ;; and push its value on the stack. emit-i(move μ@(ι),r_{0}) emit-i(push r_{0},ζ) assemble(π)

assemble((brf π_{0} π_{1}))

generate labels l_{0}, l_{1} emit-i(pop ζ,r_{0}) ;; Test against false. emit-i(cmp #18,r_{1}) emit-i(jeq l_{0}) ;; Generate code for the true branch. assemble(π_{0}) emit-i(goto l_{1}) ;; Label & generate code for the false branch. emit-l(l_{0}) assemble(π_{1}) emit-l(l_{1})

assemble((pick π^{∗}))

generate #π^{∗} + 1 labels - wlog assume l_{n} is first. emit-i(pop ζ,r_{0}) check-numeric(r_{0}) ;; Pick a label to transfer program control. emit-i(computed-goto r_{0},labels) ;; Label and generate code for 0th option. emit-l(l_{n}) assemble(π^{∗}.0) emit-i(jmp l_{#π^{∗}})

⋮

;; Label and generate code the last option. emit-l(l_{n+#π^{∗}−1}) assemble(π^{∗}.(#π^{∗}-1)) emit-l(l_{n+#π^{∗}})

assemble((update-store ι π))

;; Get value and move to global in environment. emit-i(move ζ@(0),μ@(ι)) assemble(π)

assemble((prim-apply ν υ π))

;; Generate code for primitive. inline-primitive(ν,υ) assemble(π)

assemble((update-store/ignore ι π))

;; Get value and move to global in environment, ;; pop off stack so value is not returned. emit-i(pop ζ,r_{0}) emit-i(move r_{0},μ@(ι)) assemble(π)

assemble((prim-apply/ignore ν υ π))

;; Generate code for primitive such that ;; value is not returned. inline-primitive/ignore(ν,υ)

assemble(π)

assemble((halt))

emit-i(jmp exit)

assemble((add-to-env π))

;; Add stuff in ζ to μ. emit-i(move ζ,μ) assemble(π)

assemble((add-to-env* π))

;; Add one item in ζ to μ. emit-i(sub #4,μ) assemble(π)

assemble((add-global-to-env* π))

;; Add one item in ζ to μ. emit-i(sub #4,μ) assemble(π)

assemble((tail-call))

generate labels l_{0} & l_{1} emit-i(move μ_{0},r_{3}) emit-i(pop ζ,r_{0}) check-function(r_{0}) ;; Get rid of type flag. emit-i(shr #4,r_{0}) ;; Find function in init env. emit-i(add r_{0},r_{3}) emit-i(move ζ,r_{4}) ;; Get # of args. emit-i(move r_{3}@(4),r_{0}) ;; Check # of args. emit-i(shl #2,r_{0}) emit-i(move μ,r_{1}) emit-i(move ζ,r_{2}) emit-i(sub r_{2},r_{1}) emit-i(cmp r_{1},r_{0}) error(tail-call-error1) emit-l(l_{0}) ;; Reset initial env for call. emit-i(move μ_{0},μ) emit-i(move μ_{0},ζ) emit-i(add r_{0},r_{4}) ;; Get code address. emit-i(move r_{3}@(8),r_{3}) emit-i(sub r_{0},ζ) ;; Copy args and go. emit-l(l_{1}) emit-i(cmp #0,r_{0}) emit-i(jeq r_{3}@(0)) emit-i(move r_{4}@(0),μ@) emit-i(sub #4,μ) emit-i(sub #4,r_{4}) emit-i(sub #4,r_{0}) emit-i(jmp l_{1})

assemble((closerecs ω π))

generate #ω+1 labels - wlog assume l_{n} is first. ;; jump over generated code for procs. emit-i(jmp l_{n+#ω}) Generate code for procs. assemble-proc-code(ω l_{n} l_{n+#ω−1}) emit-l(l_{n+#ω}) emit-i(push l_{n},ζ) ;; Push procedure representations on stack. assemble-proc-rep(ω l_{n} l_{n+#ω−1}) ;; Set up initial environment. emit-i(move ζ,μ_{0}) emit-i(move ζ,μ) assemble(π)

11.4.2 Assemble-proc-code

assemble-proc-code((empty-openers) l_{n} l_{m})

;; Do nothing.

assemble-proc-code((openers ν π ω) l_{n} l_{m})

;; Emit label for proc to be assembled. emit-l(l_{n}) ;; Assemble proc. assemble(π) ;; Assemble remaining procedures. assemble-proc-code(ω l_{n+1} l_{m})

11.4.3 Assemble-proc-rep

assemble-proc-rep((empty-openers) l_{n} l_{m})

;; Do nothing.

assemble-proc-rep((openers ν π ω) l_{n} l_{m})

;; Push code address. emit-i(push l_{n},ζ) ;; Push arg count. emit-i(push ν,ζ) ;; Push offset from top. emit-i(push m-n,ζ) assemble-proc-rep(ω l_{n+1} l_{m})

References

[1] Cieselski, B., and Wand, M. “Using Isabelle to Prove the Correctness of a Compiler,” in preparation.

[2] Clinger, W. “The Scheme 311 Compiler: An Exercise in Denotational Semantics,” Conf. Rec. 1984 ACM Symposium on Lisp and Functional Programming (August, 1984), 356–364.

[3] Hannan, J. “Making Abstract Machines Less Abstract,” Proc. ACM Symp. on Functional Programming, Languages, and Architecture (1991), to appear.

[4] McCarthy, J. “Towards a Mathematical Science of Computation,” Information Processing 62 (Popplewell, ed.) Amsterdam:North Holland, 1962, 21–28.

[5] Montneyohl, M., and Wand, M. “Incorporating Static Analysis in a Semantics-Based Compiler,” Information and Computation 82 (1989) 151–184.

[6] Oliva, Dino P., and Wand, M. “The Semantic Specification of Scheme via SPS,” NU CCS Technical Report, to appear.

[7] Rees, J., and Clinger, W., eds. “Revised^{3}.99 Report on the Algorithmic Language Scheme,” electronic manuscript on altdorf.ai.mit.edu.

[8] Wand, M. “Semantics-Directed Machine Architecture” Conf. Rec. 9th ACM Symp. on Principles of Prog. Lang. (1982), 234–241.

[9] Wand, M. “Deriving Target Code as a Representation of Continuation Semantics” ACM Trans. on Prog. Lang. and Systems 4, 3 (July, 1982) 496–517.

[10] Wand, M. “Loops in Combinator-Based Compilers,” Info. and Control 57,2–3 (May/June, 1983), 148–164.

[11] Wand, M. “A Semantic Prototyping System,” Proc. ACM SIGPLAN ’84 Compiler Construction Conference (1984) 213–221.

[12] Wand, M., and Wang, Z.-Y. “Conditional Lambda-Theories and the Verification of Static Properties of Programs,” Proc. 5th IEEE Symposium on Logic in Computer Science (1990), 321–332