The Revised VLISP PreScheme Front End

John D. Ramsdell^{1} M 93B0000095 The MITRE Corporation

August, 1993

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. Author’s address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. E-mail: ramsdell@mitre.org. \begin{matrix}c \\ ◯ \end{matrix}1993 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 developed a formally verified implementation of the Scheme programming language. It used a systems programming dialect of Scheme, called vlisp PreScheme, to program the vlisp Virtual Machine, a byte-code interpreter. The original compiler only accepted programs that specify iterative processes. This document describes a revision of the language and its compiler. The most important change is the compiler provides a stack to save control information for procedure calls so programs that specify recursive processes are accepted. The revision expands the systems programming tasks for which vlisp Pre-Scheme can be used and simplifies the task of matching an algorithm with its code.

Acknowledgements

Leonard Monk and Vipin Swarup made important suggestions on justifying transformation rules. Jonathan Rees provided many helpful comments on an early draft of this paper. Joshua Guttman commented on the final version.

Contents

1 Introduction 1

2 The PreScheme Language Family 4

2.1 VLISP PreScheme . . . . . . . . . . . . . . . . . . . . . . . . 4 2.1.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 5 2.1.2 Standard Procedures . . . . . . . . . . . . . . . . . . . 6 2.1.3 Formal Semantics . . . . . . . . . . . . . . . . . . . . . 8 2.1.4 Compiler Restrictions . . . . . . . . . . . . . . . . . . . 12

2.2 Macro-Free PreScheme . . . . . . . . . . . . . . . . . . . . . . 13 2.2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.3 Static Semantics . . . . . . . . . . . . . . . . . . . . . 14

2.3 Simple PreScheme . . . . . . . . . . . . . . . . . . . . . . . . 15

3 The Transformational Compiler 18

3.1 Transformation Rules . . . . . . . . . . . . . . . . . . . . . . . 19 3.1.1 Syntactic Predicates . . . . . . . . . . . . . . . . . . . 21 3.1.2 The List of Rules . . . . . . . . . . . . . . . . . . . . . 23

3.2 Usage of the Rules . . . . . . . . . . . . . . . . . . . . . . . . 28 3.3 Justification of the Rules . . . . . . . . . . . . . . . . . . . . . 29

3.3.1 if in the Consequence of an if . . . . . . . . . . . . . 36 3.3.2 lambda Simplification . . . . . . . . . . . . . . . . . . . 37 3.3.3 β-substitution . . . . . . . . . . . . . . . . . . . . . . . 38 3.3.4 letrec Lifting . . . . . . . . . . . . . . . . . . . . . . 41 3.3.5 letrec Expression Merging . . . . . . . . . . . . . . . 42 3.3.6 letrec Simplification . . . . . . . . . . . . . . . . . . . 44 3.3.7 letrec Binding Merging . . . . . . . . . . . . . . . . . 44 3.3.8 Combination in a Combination Rotation . . . . . . . . 46 3.3.9 Defined Constant Substitution . . . . . . . . . . . . . . 48

4 PreScheme Assembly Language 49 4.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . 51 4.2 Additional Domain Equation . . . . . . . . . . . . . . . . . . . 51 4.3 Semantic Functions . . . . . . . . . . . . . . . . . . . . . . . . 52 4.4 Machine Instruction Auxiliary Functions . . . . . . . . . . . . 53 4.5 Additional Auxiliary Functions . . . . . . . . . . . . . . . . . 55

5 The Syntax-Directed Compiler 56 5.1 Auxiliary Compiler Functions . . . . . . . . . . . . . . . . . . 60 5.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 61

5.2.1 Code Linearity . . . . . . . . . . . . . . . . . . . . . . 61 5.2.2 Compile-Time Environments . . . . . . . . . . . . . . . 63 5.2.3 Simple Expressions . . . . . . . . . . . . . . . . . . . . 66 5.2.4 Defined and letrec-Bound Variables . . . . . . . . . . 74

6 Results, Future Work, and Conclusions 77

A Operators in C 80

List of Figures

2.1 Predefined Procedures . . . . . . . . . . . . . . . . . . . . . . 6 2.2 Case Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 2.3 Typing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 16

3.1 Defined Constant Substitution . . . . . . . . . . . . . . . . . . 27 3.2 Example vlisp PreScheme Program . . . . . . . . . . . . . . . 30 3.3 Expand into Macro-Free PreScheme . . . . . . . . . . . . . . . 30 3.4 Name Anonymous Lambda Expressions . . . . . . . . . . . . . 31 3.5 Closure Hoisting . . . . . . . . . . . . . . . . . . . . . . . . . 31 3.6 Constant Folding . . . . . . . . . . . . . . . . . . . . . . . . . 32 3.7 Inline Non-Tail-Recursive Procedure Calls . . . . . . . . . . . 32 3.8 Eliminate Unused Lambda Expressions and Initializers …. 33

4.1 Machine Stack Layout . . . . . . . . . . . . . . . . . . . . . . 50

5.1 Code Generators . . . . . . . . . . . . . . . . . . . . . . . . . 60 viii

Chapter 1

Introduction

The vlisp Project developed an architecture for the specification and implementation of verified optimizing compilers. Source programs are translated into an intermediate representation based on the lambda calculus with an implicit store. The intermediate representation is transformed until it meets syntactic restrictions. These restrictions allow the generation of efficient code using a syntax-directed compiler.

The architecture assumes the source language and the intermediate representation have a formal denotational semantics. The correctness of each transformation of the program is justified relative to this semantics.

The abstract machine language which is produced by the syntax-directed compiler also has a denotational semantics expressed using the same domains as the source language. The correctness of the syntax-directed compiler is also justified relative to the denotational semantics.

At this stage, the abstract machine language is given an operational semantics which is faithful to the denotational semantics. The operational semantics is used to justify its translation into machine language.

The vlisp Project successfully used this architecture to produce a compiler for a systems programming language. It was used to compile a byte-code interpreter for a Scheme system. The vlisp Project constructed a verified design of this Scheme system, and then implemented that design [3]. The design is based on Scheme48 [5], whose byte-code interpreter is written in PreScheme.

PreScheme is a restricted dialect of Scheme intended for systems programming. It was invented by Jonathan Rees and Richard Kelsey [7]. The language was defined so that programs can be executed using only a C-like run-time system. A compiler for this language will reject any program that requires run-time type checking, and the run-time system usually will not provide automatic storage reclamation.

PreScheme was carefully designed so that it syntactically looks like Scheme and has similar semantics. With a little care, PreScheme programs can be run and debugged as if they were ordinary Scheme programs.

This paper describes vlisp PreScheme, which is our systems programming oriented Scheme dialect inspired by PreScheme. The major syntactic difference between the two dialects of PreScheme is that vlisp PreScheme has no user-defined syntax (macros) or compiler directives. The only other major difference is that they each provide a different set of standard procedures.

The compiler for vlisp PreScheme does not accept the entire language. Compilation occurs in three stages. The first stage translates the program into a language called Macro-Free PreScheme by expanding most of vlisp PreScheme’s derived syntax and changing bound variables. The second stage translates the Macro-Free program into an equivalent program by using meaning-refining transformations. If the translation succeeds, the program is in a very restricted subset called Simple PreScheme. This subset has properties that make it easy to compile. The final stage of compilation translates Simple PreScheme into machine language.

The Simple PreScheme language was inspired by Pure PreScheme, a language defined by Dino Oliva and Mitchell Wand. They created a verified compiler for Pure PreScheme [12]. A straightforward translation is all that is required to convert a Simple PreScheme program into a Pure PreScheme program, however, the current version of the Pure PreScheme compiler only compiles programs that specify iterative processes.

This paper describes the vlisp PreScheme language, the Macro-Free Pre-Scheme language, and finally the Simple PreScheme language. The paper concludes by giving the design and verification of our program which attempts to translate Macro-Free PreScheme programs into Simple PreScheme ones, and a syntax-directed compiler for Simple PreScheme which produces a high-level assembly language called PreScheme Assembly Language. The syntax-directed compiler accepts Simple PreScheme programs that specify recursive processes.

This paper does not describe the translation of PreScheme Assembly Language into machine language. There are two missing components: a proof that the control structures and variable environment of PreScheme Assembly Language can be correctly implemented using one machine stack and a register allocator along with its correctness proof. These topics have been addressed by Dino Oliva [11] for a closely related programming language.

This work is most closely related to the work of Richard Kelsey. The designs of both vlisp PreScheme and Pure PreScheme were strongly influenced by the design of PreScheme [7]. Furthermore, a major part of this compiler is a transformational compiler [6].

The differences between these two dialects of PreScheme reflect the differing goals of their designers. PreScheme is targeted to high-performance systems programming while vlisp PreScheme is targeted to verified compilation of state machines.

This paper revises the original paper on vlisp PreScheme [14] in several ways. The most important change is the presentation of the Simple PreScheme compiler which provides a stack to save control information for procedure calls. Procedure calls can now return to the location at which they were invoked.

The most important contribution of the previous report on vlisp Pre-Scheme is the identification of a collection of transformation rules that can both be verified relative to the formal semantics of the source language, and form the basis of a practical optimizing compiler. This report includes a few new transformation rules, such as raising begin’s in an if’s test, which improve the quality of generated code.

The language has been changed in several small ways. The abort primitive has been renamed to exit, and the assert primitive has been removed. The most important change to the language is the addition of a new definition form define-integrable for naming lambda abstractions. This form directs the compiler to replace references to the defined variable with its definition when the variable is in the operator position of a combination. The algorithms that control the application of transformation rules have also been changed to make allowances for the syntax-directed compiler.

The PreScheme Language Family

This chapter describes our systems programming oriented Scheme dialect vlisp PreScheme and various related dialects used in the vlisp project. Programs are written in vlisp PreScheme. Macro-Free PreScheme is the language manipulated by the transformational compiler. Simple PreScheme is a restricted subset of Macro-Free PreScheme which is the source language of the syntax-directed compiler.

2.1 VLISP PreScheme

vlisp PreScheme programs manipulate data objects that fit in machine words. The type of each data object is an integer, a character, a boolean, a string, a port, a pointer to an integer, or a procedure—really a pointer to a procedure. A compiler must ensure that operators are not applied to data of the wrong type without the use of run-time checks.

A running vlisp PreScheme program can only manipulate pointers to a restricted class of procedures. The free variables of these procedures must be allocatable at compile time. The restriction eliminates the need to represent closures at run-time. A vlisp PreScheme program may contain procedures with free variables that are lambda-bound. A compiler must transform these programs so that they meet the run-time restriction.

As with Scheme, implementations of PreScheme are required to be tailrecursive, which means that iterative processes can be expressed by means of procedure calls. When the last action taken by a PreScheme procedure is a call, tail-recursive implementations are required to eliminate the control information of the calling procedure so that the order of space growth of iterative processes is constant. Tail-recursive calls will be the name given to procedure calls which are the last action performed by in a procedure.

2.1.1 Syntax

The syntax of the vlisp PreScheme language is identical to the syntax of the language defined in the Scheme standard [4, Chapter 7] with the following exceptions:

• Every defined procedure takes a fixed number of arguments.

• The only variables that can be modified are those introduced at top level using the syntax

(define ⟨variable⟩ ⟨expression⟩),

and whose name begins and ends with an asterisk and is at least three characters long. Variables so defined are called mutable variables. Note that a variable introduced at other than top level may have a name which begins and ends with an asterisk, but this practice is discouraged.

• If ⟨expression⟩ is a lambda expression, variables can also be defined using the syntax

(define-integrable ⟨variable⟩ ⟨expression⟩).

When ⟨variable⟩ occurs in the operator position of a combination, compilers must replace it with ⟨expression⟩.

• No variable may be defined more than once.

• letrec is not a derived expression. The initializer for each variable bound by a letrec expression must be a lambda expression.

• Constants are restricted to integers, characters, booleans, and strings.

• Finally, a different set of the standard procedures has been specified.

(define (not x) (if x #f #t))
(define (zero? x) (= 0 x))
(define (positive? x) (< 0 x))
(define (negative? x) (> 0 x))
(define (ashr x y) (ashl x (- y)))
(define (char<= x y) (not (char< y x)))
(define (char> x y) (char< y x))
(define (char>= x y) (char<= y x))
(define (addr<= x y) (not (addr< y x)))
(define (addr> x y) (addr< y x))
(define (addr>= x y) (addr<= y x))

Figure 2.1: Predefined Procedures

2.1.2 Standard Procedures

Most vlisp PreScheme standard procedures are listed following this paragraph. The text on the left of each entry gives the procedure’s name and its type at one fixed arity. A pointer to an integer is ⋆ Int; the other notation is standard. The text on the right describes the arity of the primitive. The semantics of each procedure is roughly defined by giving an implementation in C. Appendix A contains the header file that was once included into C code generated by the vlisp PreScheme Front End. The remaining primitives are defined in Figure 2.1.

< : Int × Int → Bool 2 or more <= : Int × Int → Bool 2 or more = : Int × Int → Bool 2 or more >= : Int × Int → Bool 2 or more > : Int × Int → Bool 2 or more abs : Int → Int 1 + : Int × Int → Int any - : Int × Int → Int 1 or 2 * : Int × Int → Int any quotient : Int × Int → Int 2 remainder : Int × Int → Int 2 ashl : Int × Int → Int 2 low-bits : Int × Int → Int 2

integer->char : Int → Chr  1
char->integer : Chr → Int  1

char=? : Chr × Chr → Bool 2 char<? : Chr × Chr → Bool 2

make-vector : Int → ⋆ Int  1

vector-ref : ⋆ Int × Int → Int 2 vector-set! : ⋆ Int × Int × Int → Int 3

vector-byte-ref : ⋆ Int × Int → Int  2

vector-byte-set! : ⋆ Int × Int × Int → Int 3 addr< : ⋆ Int × ⋆ Int → Bool 2 addr= : ⋆ Int × ⋆ Int → Bool 2 addr+ : ⋆ Int × Int → ⋆ Int 2 addr- : ⋆ Int × ⋆ Int → Int 2

addr->integer : ⋆ Int → Int  1
integer->addr : Int → ⋆ Int  1

addr->string : ⋆ Int → String 1 string->addr : String → ⋆ Int 1

port->integer : Port → Int  1
integer->port : Int → Port  1

read-char : Port → Chr 0 or 1 peek-char : Port → Chr 0 or 1

eof-object? : Chr → Bool  1

write-char : Chr × Port → Int 1 or 2 write-int : Int × Port → Int 1 or 2 write : String × Port → Int 1 or 2 newline : Port → Int 0 or 1 force-output : Port → Int 0 or 1 null-port? : Port → Bool 1

open-input-file : String → Port  1
close-input-port : Port → Int  1
open-output-file : String → Port  1
close-output-port : Port → Int  1
current-input-port : → Port  0
current-output-port : → Port  0

read-image : ⋆ Int × Int × Port → Int 3 write-image : ⋆ Int × Int × Port → Int 3

     bytes-per-word : Int  –
     useful-bits-per-word : Int  –

exit : ∀α, Int → α 1 err : ∀α, Int × String → α 2

2.1.3 Formal Semantics

The formal semantics of vlisp PreScheme is presented in a form that very closely resembles Scheme’s semantics [4, Appendix A]. It uses the same mathematical conventions and many of the standard’s definitions without repeating them here. I strongly suggest you have a copy of the standard in hand as you read the rest of this section.

The vlisp PreScheme formal semantics differs from Scheme’s in a small number of ways. All variables must be defined before they are referenced or assigned and no variable may be defined more than once. vlisp PreScheme procedure values do not have a location associated with them because there is no comparison operator for procedures. Lambda bound variables are immutable so a location need not be allocated for each actual parameter of an invoked procedure. Procedures always return exactly one value, so expression continuations map a single expressed value to a command continuation. vlisp PreScheme letrec is no longer a derived expression because the immutability of lambda bound variables would make Scheme’s definition of letrec useless. The answer domain is the flat domain of integers. Finally, memory is assumed to be infinite so the storage allocator new always returns a location.

A vlisp PreScheme program is a sequence of definitions and expressions. The meaning of a program is defined via the following transformation into vlisp PreScheme’s abstract syntax.

(define I_{1} E_{1}) … E_{i} … (define I_{n} E_{n}) E_{0}

⟹

     (define I_{1}) . . . (define I_{n})

(begin (set! I_{1} E_{1}) … E_{i} … (set! I_{n} E_{n}) E_{0})

Abstract Syntax

K ∈ Con constants
I ∈ Ide variables
E ∈ Exp expressions
B ∈ Bnd bindings
P ∈ Pgm programs
Pgm ⟶ (define I)∗ E
Bnd ⟶ (I (lambda (I∗) E))∗
Exp ⟶ K | I | (E E∗) | (lambda (I∗) E)
| (begin E∗ E) | (letrec (B) E)
| (if E E E) | (if E E) | (set! I E)

The variables bound by a letrec expression must be distinct. Domain Equations

α ∈ L  locations
ν ∈ N  natural numbers
T = {false, true}  booleans
H  characters
R  integers
E_{v}  vectors
E_{s}  strings
E_{p}  ports
M = {unspecified, undefined} miscellaneous
ϕ ∈ F = E∗ → K → C  procedure values
ϵ ∈ E = T + H + R + E_{v} + E_{s} + E_{p} + M + F

expressed values

σ ∈ S = L → (E × T)  stores
δ ∈ D = L + E  denoted values
ρ ∈ U = Ide → D  environments
θ ∈ C = S → A  command continuations
κ ∈ K = E → C  expression continuations
A = R  answers
χ ∈ X  errors

Semantic Functions

K : Con → E
L : Exp → U → E
I : Bnd → Ide∗
B : Bnd → Ide∗ → U → E∗ → E∗
E : Exp → U → K → C
E∗ : Exp∗ → U → (E∗ → C) → C
D : Pgm → U → K → C
P : Pgm → A

The definition of K is deliberately omitted.

L[[(lambda (I∗) E)]] = λρ. (λϵ∗κ. #ϵ∗ = #I∗ → E[[E]](extends ρI∗ϵ∗)κ, wrong “wrong number of arguments”) in E

E[[K]] = See [4, Appendix A] E[[I]] = See [4, Appendix A] E[[(E E∗)]] = See [4, Appendix A] E[[(lambda (I∗) E)]] = λρκ. send(L[[(lambda (I∗) E)]]ρ)κ E[[(begin E)]] = E[[E]] E[[(begin E E∗ E_{0})]] = λρκ. E[[E]]ρλϵ. E[[(begin E∗ E_{0})]]ρκ E[[(letrec (B) E)]] = λρκ. E[[E]](extends ρ(I[[B]])(fix(B[[B]](I[[B]])ρ)))κ E[[(if E E E)]] = See [4, Appendix A] E[[(if E E)]] = See [4, Appendix A]

Assignment for identifiers whose name begins and ends with an asterisk and is at least three characters long is defined using assign.

E[[(set! I E)]] = λρκ. E[[E]]ρ(single λϵ. assign(lookup ρI)ϵ(send unspecified κ))

Assignment for all other identifiers is defined using initialize.

E[[(set! I E)]] =

λρκ. E[[E]]ρ(single λϵ. initialize(lookup ρI)ϵ(send unspecified κ)) E∗[[ ]] = λρψ. ψ⟨⟩ E∗[[E E∗]] = λρψ. E[[E]]ρ(single λϵ. E∗[[E∗]]ρλϵ∗. ψ(⟨ϵ⟩ § ϵ∗)) I[[ ]] = ⟨⟩ I[[(I (lambda (I∗) E)) B]] = ⟨I⟩ § I[[B]] B[[ ]] = λI∗ρϵ∗. ⟨⟩ B[[(I (lambda (I∗) E)) B]] =

λI∗_{0}ρϵ∗. ⟨L[[(lambda (I∗) E)]](extends ρI∗_{0}ϵ∗)⟩ § B[[B]]I∗_{0}ρϵ∗ D[[E]] = E[[E]] D[[(define I) P]] =

λρκσ. D[[P]](ρ[(new σ) in D/I])κ(update(new σ) undefined σ) P[[P]] = D[[P]]ρ_{0}κ_{0}σ_{0} κ_{0} = λϵσ. ϵ ∈ R → ϵ | R, wrong “result not an integer”σ

The environment ρ_{0} maps the name of each standard procedure to its value and maps all other identifiers to undefined. It maps no identifier to a location.

Auxiliary Functions

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

extends : U → Ide∗ → E∗ → U extends = λρI∗ϵ∗. #I∗ = 0 → ρ, extends(ρ[ϵ∗ ↓ 1 in D/I∗ ↓ 1])(I∗ † 1)(ϵ∗ † 1)

send : E → K → C send = λϵκ. κϵ

single : K → K single = λκ. κ

new : S → L [implementation-dependent] new satisfies ∀σ, σ(new σ) ↓ 2 = false

hold : D → K → C hold = λδκσ. δ ∈ E → send(δ | E)κσ, send(σ((δ | L) ↓ 1))κσ

assign : D → E → C → C assign = λδϵθσ. δ ∈ L → θ(update(δ | L)ϵσ), wrong “assignment of an immutable variable”σ

initialize : D → E → C → C initialize =

λδϵθσ. δ ∈ L ∧ σ(δ | L) ↓ 1 = undefined → θ(update(δ | L)ϵσ), wrong “assignment of an immutable variable”σ

applicate : E → E∗ → K → C applicate = λϵϵ∗κ. ϵ ∈ F → (ϵ | F)ϵ∗κ, wrong “bad procedure”

2.1.4 Compiler Restrictions

Our compiler places the following additional restrictions on the syntax of vlisp PreScheme programs.

(case ⟨key⟩

((0) ⟨sequence_{1}⟩)

⋮

((⟨n − 1⟩) ⟨sequence_{n}⟩))

Figure 2.2: Case Syntax

• All references to standard procedures must be in the operator position of an application.

• The case derived expression is restricted so as to become essentially a computed goto. There must be exactly one integer given as the selection criterion for each clause. The first selection criteria must be zero and the selection criteria for other clauses must be the successor of the previous clause’s selection criterion as shown in Figure 2.2.

The case expression is normally expanded into a nested sequence of conditionals, and the semantics of case is derived from this expansion.

2.2 Macro-Free PreScheme

Macro-Free PreScheme (mfps) programs result from vlisp PreScheme programs by expanding all derived syntax except the case expression, changing each bound variable if it is the variable of a standard procedure, and replacing single armed conditionals (if E E) with (if E E (if #f #f)). These programs resemble a vlisp PreScheme program after it has been translated into its abstract syntax. mfps programs must also satisfy the restriction that each n-ary standard procedure must be used at one fixed arity. For example, calls to + must have exactly two operands so vlisp PreScheme programs with calls to + using more than two operands must be translated into a combination of calls using only a binary version of +.

2.2.1 Syntax

K ∈ Con constants
I ∈ Ide variables
O ∈ Op primitive operators
E ∈ Exp expressions
B ∈ Bnd bindings
P ∈ Pgm programs
Pgm ⟶ (define I)∗ E
Bnd ⟶ (I (lambda (I∗) E))∗
Exp ⟶ K | I | (E E∗) | (lambda (I∗) E)
| (begin E∗ E) | (letrec (B) E)
| (if E E E) | (if #f #f) | (set! I E)
| (O E∗) | (case E ((K) E)∗ ((K) E))

2.2.2 Semantics

The semantics of mfps is given by the same equations as is vlisp Pre-Scheme’s. A mfps program’s abstract syntax is derived by expanding case expressions as described in the Scheme standard. As with vlisp PreScheme, the formal definition of each primitive has been deliberately omitted.

2.2.3 Static Semantics

Macro-Free PreScheme programs may be strongly typed. As in Standard ML [10], types are inferred, not declared, but unlike Standard ML, there are no polymorphic variables. All expressions are monomorphic except (if #f #f) and (set! I E).

• The base types are Int, Chr, Bool, String, and Port.

• If τ is a type, then so is ⋆ τ.

• If τ_{1}, …, τ_{n}, and τ are types, then so is τ_{1} × ⋯ × τ_{n} → τ.

Type ⋆ τ is the type of a pointer, and τ_{1} × ⋯ × τ_{n} → τ is the type of a procedure.

The rules used to assign types to mfps abstract syntax expressions are given in Figure 2.3. When a type is unconstrained by the rules, the expression is assigned the integer type.

2.3 Simple PreScheme

Simple PreScheme programs are syntactically restricted, strongly typed Macro-Free PreScheme programs. The syntax is as follows:

K ∈ Con constants
I ∈ Ide variables
O ∈ Op primitive operators
C ∈ Cls case clauses
S ∈ Smpl simple expressions
B ∈ Bnd bindings
E ∈ Exp top level expressions
P ∈ Pgm programs
Pgm ⟶ (define I)∗ E
Exp ⟶ (letrec (B) S)
Bnd ⟶ (I (lambda (I∗) S))∗
Smpl ⟶ K | I | (S S∗) | ((lambda (I∗) S) S∗)
| (begin S∗ S) | (if S S S) | (if #f #f)
| (case S C) | (O S∗) | (set! I S)
Cls ⟶ ((K) S)∗ ((K) S)

There is a further syntactic restriction. The first selection criteria of a case clause must be zero and the selection criteria for other clauses must be the successor of the previous clause’s selection criterion. The case derived expression is restricted so as to allow it to be compiled into a computed goto. See Figure 2.2 on page 13.

The syntactic restrictions used to define Simple PreScheme imply that these programs will meet all of the run-time conditions of a vlisp PreScheme program presented at the beginning of this section. Simple PreScheme programs are strongly typed so no operator will be applied to data of the wrong type. lambda expressions in Simple PreScheme programs may occur only ρ ⊢ K : type of (K)

ρ, I : τ ⊢ I : τ

\frac{ρ ⊢ I : τ}{ρ, I_{0} : τ_{0} ⊢ I : τ} (I_{0} ≠ I)

\frac{ρ ⊢ E_{0} : τ_{1} × ⋯ × τ_{n} → τ ρ ⊢ E_{1} : τ_{1} … ρ ⊢ E_{n} : τ_{n}}{ρ ⊢ (E_{0} E_{1} … E_{n}) : τ}

\frac{ρ, I_{1} : τ_{1}, …, I_{n} : τ_{n} ⊢ E : τ}{ρ ⊢ (lambda (I_{1} … I_{n}) E) : τ_{1} × ⋯ × τ_{n} → τ}

\frac{ρ ⊢ E : τ}{ρ ⊢ (begin E) : τ}

\frac{ρ ⊢ E_{0} : τ_{0} ρ ⊢ (begin E∗ E) : τ}{ρ ⊢ (begin E_{0} E∗ E) : τ}

\frac{ρ, I_{1} : τ_{1}, …, I_{n} : τ_{n} ⊢ E_{1} : τ_{1} ⋮ ρ, I_{1} : τ_{1}, …, I_{n} : τ_{n} ⊢ E_{n} : τ_{n} ρ, I_{1} : τ_{1}, …, I_{n} : τ_{n} ⊢ E : τ}{ρ ⊢ (letrec ((I_{1} E_{1}) … (I_{n} E_{n})) E) : τ}

\frac{ρ ⊢ E_{0} : Bool ρ ⊢ E_{1} : τ ρ ⊢ E_{2} : τ}{ρ ⊢ (if E_{0} E_{1} E_{2}) : τ}

ρ ⊢ (if #f #f) : τ

\frac{ρ ⊢ I : τ_{0} ρ ⊢ E : τ_{0}}{ρ ⊢ (set! I E) : τ}

\frac{ρ, I_{1} : τ_{1}, …, I_{n} : τ_{n} ⊢ E : Int}{ρ ⊢ (define I_{1}) … (define I_{n}) E : Int}

Figure 2.3: Typing Rules as initializers in top-level letrec bindings or in the operator position of a procedure call. As a result, there is no need to represent closures at run-time.

Simple PreScheme’s semantics are inherited from Macro-Free PreScheme’s semantics.

The Transformational Compiler

There are five phases in the translation of vlisp PreScheme into Simple PreScheme.

Parse: Expands usages of derived syntax by rules consistent with those presented in the Scheme standard. In addition, the program’s bound variables are changed so that no variable occurs both bound and free, and no variable is bound more than once. Other syntactic checks are made.

Inline standard procedures: A variable bound in a program is changed if it is also bound to a standard procedure. Consequently, every occurrence of a variable bound to a standard procedure refers to that procedure. The result is a Macro-Free PreScheme program.

Apply transformation rules: Translates a Macro-Free PreScheme program into a Simple PreScheme one using meaning-refining transformations. More will be said about this phase later.

Type check: Ensures that a Simple PreScheme program is strongly typed. This phase implements Algorithm W. That algorithm’s correctness was demonstrated by Robin Milner [9]. The unifier is based on a published program by Laurence Paulson [13, p. 381].

Linearize: Translates the internal representation of a strongly typed Simple PreScheme program into a PreScheme Assembly Language using a syntax-directed compiler as described in Chapter 5.

Compilers for vlisp PreScheme do not accept all syntactically correct programs because many Macro-Free PreScheme programs cannot be translated into Simple PreScheme. Furthermore, the set of Macro-Free programs that can be translated by a particular compiler depends on the transformation rules used by that compiler.

While there is no precise characterization of what constitutes a vlisp PreScheme program, knowledgeable programmers know one when they see one. Their intuition is based on an understanding of the run-time conditions and the knowledge that existing compilers perform β-conversion, procedure inlining, and closure hoisting.

The most complex and error prone phase of the vlisp PreScheme Front End translates Macro-Free PreScheme programs into Simple PreScheme ones. The program is transformed by applying meaning-refining rules. The rules are meaning-refining in a sense made precise in Section 3.3.

The selection and application of rules is performed by an intricate set of procedures, however, the only way a program can be modified is by the application of some rules. For some inputs, the control procedures will run forever, but when these procedures terminate successfully, errors could have been introduced only by bad rules. Therefore, the verification effort focused solely on the transformation rules.

3.1 Transformation Rules

Each rule is a conditional rewrite rule. It has a pattern, a predicate, and a replacement. An expression matches a pattern if there is an assignment of pattern variables which makes the two expressions equal. The rewrite is performed if the matching expression satisfies the predicate. A rule with pattern E_{0} and replacement E_{1} is written E_{0} ⟹ E_{1}, and its predicate is given in the text. The predicate for rules with no restrictions given in the text is always satisfied.

In many systems using rewrite rules, the replacing expression is derived from the replacement by instantiating its pattern variables using the assignment of pattern variables produced during matching. This system avoids name conflicts by ensuring all expressions are α-converted. Definition 1 An expression is α-converted if no variable occurs both bound and free, and no variable is bound more than once. The system avoids name conflicts by a change of bound variables in each instantiation of a pattern variable during the construction of the replacing expression. Contexts are often used in rule presentations to help express the renaming requirement. Definition 2 A context, C[ ], is an expression with some holes.

• [ ] is a context.

• K is a context.

• I is a context.

• If C_{0}[ ], …, C_{n}[ ] are contexts, then so is (C_{0}[ ] … C_{n}[ ]).

• If C[ ] is a context, then so is (lambda (I∗) C[ ]).

• If C_{0}[ ], …, C_{n}[ ] are contexts, then so is (begin C_{0}[ ] … C_{n}[ ]).

• If C_{0}[ ], …, C_{n}[ ] are contexts, then so is (letrec ((I_{1} (lambda (I∗) C_{1}[ ])) …) C_{0}[ ]).

• If C_{0}[ ], C_{1}[ ], and C_{2}[ ] are contexts, then so is (if C_{0}[ ] C_{1}[ ] C_{2}[ ]).

• If C[ ] is a context, then so is (set! I C[ ]).

In this definition,the expression (if #f #f) is considered to be a constant. This slight abuse of the notation will be repeated in the remainder of the text. Definition 3 A context substitution, C[E], is a context in which each hole in C[ ] has been replaced with a copy of E in which every bound variable has been renamed using a fresh variable.

As a consequence, if both C[ ] and E are α-converted and they share no bound variables, then C[E] is α-converted.^{1}

Another way to avoid name conflicts is to use de Bruijn’s nameless terms [1, Appendix C]. Their use was considered too late in the project to be taken seriously.

3.1.1 Syntactic Predicates

Transformation rule applicability may be predicated on syntactic properties in addition to matching the rule’s pattern. A common predicate tests if a variable is free in an expression. The definition of three other predicates follow.

A side-effect free expressions returns a value without modifying the store so it can be eliminated when its value is ignored.

Definition 4 The side-effect free expressions are defined inductively by the following rules:

• K is side-effect free.

• I is side-effect free.

• If O is side-effect free, and E_{1} … E_{n} are side-effect free, then so is (O E_{1} … E_{n}).

• (lambda (I∗) E) is side-effect free.

• If E_{0}, …, E_{n} are side-effect free, then so is (begin E_{0} … E_{n}).

• If E is side-effect free, then so is (letrec (B) E).

• If E_{0}, E_{1}, and E_{2} are side-effect free, then so is (if E_{0} E_{1} E_{2}).

• If E_{0}, …, E_{n} are side-effect free, then so is (case E_{0} ((K) E_{1}) …).

An expression is invariable if it is side-effect free and its value does not depend on modifiable variables. When an invariable expression is evaluated later during the execution of a program, its value remains the same.

1In the compiler, each variable is identified by a unique integer. Renaming a bound variable is implemented by reserving an unused integer for the new variable.

Definition 5 The invariable expressions are defined inductively by the following rules:

• K is invariable.

• If I is immutable, it is invariable.

• If O is invariable, and E_{1} … E_{n} are invariable, then so is (O E_{1} … E_{n}).

• (lambda (I∗) E) is invariable.

• If E_{0}, …, E_{n} are invariable, then so is (begin E_{0} … E_{n}).

• If E is invariable, then so is (letrec (B) E).

• If E_{0}, E_{1}, and E_{2} are invariable, then so is (if E_{0} E_{1} E_{2}).

• If E_{0}, …, E_{n} are invariable, then so is (case E_{0} ((K) E_{1}) …). An expression is almost side-effect free if it does not modify the store

until its last action. Definition 6 The almost side-effect free expressions are defined inductively by the following rules:

• K is almost side-effect free.

• I is almost side-effect free.

• If E_{1} … E_{n} are side-effect free, then (O E_{1} … E_{n}) is almost side-effect free.

• If E_{0} is almost side-effect free, and E_{1}, …, E_{n} are side-effect free, then ((lambda (I_{1} … I_{n}) E_{0}) E_{1} … E_{n}) is almost side-effect free.

• (lambda (I∗) E) is almost side-effect free.

• If E_{0}, …, E_{n−1} are side-effect free, and E_{n} is almost side-effect free, then (begin E_{0} … E_{n}) is almost side-effect free.

• If E is almost side-effect free, then so is (letrec (B) E).

• If E_{0} is side-effect free, and E_{1} and E_{2} are almost side-effect free, then (if E_{0} E_{1} E_{2}) is almost side-effect free.

• If E_{0} is side-effect free, and E_{1}, …, E_{2} are almost side-effect free, then (case E_{0} ((K) E_{1}) …) is almost side-effect free.

• If E is side-effect free, then (set! I E) is almost side-effect free.

3.1.2 The List of Rules

Here is a list of the implemented rules. The rules assume that all expressions are α-converted.

1. Primitive expression simplification.

• Evaluate constant expressions.

• Simplify operations applied to identity elements.

\begin{matrix}(+ 0 E) ⟹ E \\ (∗ 1 E) ⟹ E \end{matrix}

• Move constants to first operand for commutative operators.

(O E K) ⟹ (O K E)

• Move associative operators to the first operand.

(O E_{0} (O E_{1} E_{2})) ⟹ (O (O E_{0} E_{1}) E_{2})

• Use special rules for difference, arithmetic shift, and address arith-

metic. The rule for vector-set! is not shown.

(− E K) ⟹ (+ E −K) (ashl (ashl E_{0} E_{1}) E_{2}) ⟹ (ashl E_{0} (+ E_{1} E_{2})) (addr+ (addr+ E_{0} E_{1}) E_{2}) ⟹ (addr+ E_{0} (+ E_{1} E_{2}))

(vector-ref (addr+ E_{0} E_{1}) E_{2})

⟹ (vector-ref E_{0} (+ E_{1} E_{2})) (addr+ E 0) ⟹ E

• Introduce a let for some primitives.

(O E∗) ⟹ ((lambda (I∗) (O I∗)) E∗)

when E∗ contains a combination or a begin expression.

2. Conditional expression simplification (if and case).

• Select branch when the test is a constant. (if K E_{1} E_{2}) ⟹ E_{2} if K is false, else E_{1} (case K … ((i) E_{i}) …) ⟹ E_{i} if K is i

• Raise a combination in a test.

(if (E_{0} E∗) E_{1} E_{2})

⟹ ((lambda (I) (if I E_{1} E_{2})) (E_{0} E∗)) (case (E E∗) …)

⟹ ((lambda (I) (case I …)) (E E∗))

• Raise a begin in a test.

(if (begin E∗ E_{0}) E_{1} E_{2})

⟹ ((lambda (I) (if I E_{1} E_{2})) (begin E∗ E_{0})) (case (begin E∗ E) …)

⟹ ((lambda (I) (case I …)) (begin E∗ E))

• Simplify an if in the test of an if.

(if (if E_{0} E_{1} E_{2}) E_{3} E_{4})

⟹ (if E_{0} (if E_{1} E_{3} E_{4}) (if E_{2} E_{3} E_{4}))

Used when both E_{3} and E_{4} are constants or variables.

• Simplify an if in the consequence of an if.

(if E_{0} (if E_{0} E_{1} E_{2}) E_{3}) ⟹ (if E_{0} E_{1} E_{3}) (if E_{0} E_{1} (if E_{0} E_{2} E_{3})) ⟹ (if E_{0} E_{1} E_{3})

when E_{0} is side-effect free.

3. begin introduction.

((lambda (I) E_{1}) E_{0}) ⟹ (begin E_{0} E_{1})

when I is not free in E_{1}.

4. begin simplification.

(begin E∗_{0} (begin E∗_{1}) E∗_{2}) ⟹ (begin E∗_{0} E∗_{1} E∗_{2}) (begin E_{0} … E_{i} … E_{n}) ⟹ (begin E_{0} … E_{i−1} E_{i+1} … E_{n})

when E_{i} is side-effect free and i < n.

5. lambda expression naming. Name anonymous lambda expressions which are not in the operator position of a combination.

(lambda (I∗) E) ⟹ (letrec ((I (lambda (I∗) E))) I)

where I is a fresh variable so it is not free in E.

6. β-substitution. Substitute for a variable when it is lambda-bound to an invariable expression. Alternatively, substitute for a variable when it is lambda-bound in a call in which all of the arguments are side-effect free and the body is almost side-effect free.

The rule is used when the variable is bound to a constant, another variable, or when the variable is referenced at most once.

((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})
⟹ ((lambda (I_{1} … I_{i} … I_{n}) C[E_{i}]) E_{1} … E_{i} … E_{n})

when either E_{i} is invariable, or when E_{1}, …, E_{n} are side-effect free and C[I_{i}] is almost side-effect free.

7. lambda simplification.

((lambda () E)) ⟹ E

and

((lambda (I_{1} … I_{i} … I_{n}) E) E_{1} … E_{i} … E_{n})
⟹ ((lambda (I_{1} … I_{i−1} I_{i+1} … I_{n}) E) E_{1} … E_{i−1} E_{i+1} … E_{n})

when E_{i} is side-effect free and I_{i} is not free in E.

8. letrec substitution.

(letrec (B_{0} (I E) B_{1}) C[I])

⟹ (letrec (B_{0} (I E) B_{1}) C[E])

(letrec (B_{0} (I_{i} E_{i}) B_{1} (I_{j} C[I_{i}]) B_{2}) E_{0})

⟹ (letrec (B_{0} (I_{i} E_{i}) B_{1} (I_{j} C[E_{i}]) B_{2}) E_{0})

9. letrec simplification.

(letrec () E) ⟹ E and

(letrec (B_{0} (I_{i} (lambda (I∗) E_{i})) B_{1}) E)
⟹ (letrec (B_{0} B_{1}) E)

when I_{i} is referenced nowhere except in E_{i}.

10. letrec lifting.

C[(letrec (B) E)] ⟹ (letrec (B) C[E]) when C[ ] has one hole and binds no free variables of B. Since C[ ] has only one hole, there is no need to perform variable renaming.

11. letrec binding merging.

(letrec (B_{0} (I (lambda (I∗) (letrec (B_{1}) E))) B_{2}) E_{0})

⟹ (letrec (B_{0} (I (lambda (I∗) E)) B_{1} B_{2}) E_{0})

when I∗ are not free in B_{1}.

12. letrec expression merging.

(letrec (B_{0}) (letrec (B_{1}) E)) ⟹ (letrec (B_{0} B_{1}) E)

13. letrec elimination.

(letrec ((I E)) I) ⟹ E when I is not free in E. Used when the expression is in the operator position of a combination.

14. Combination in a combination rotation.

(E_{0} ((lambda (I∗) E_{1}) E∗)) ⟹ ((lambda (I∗) (E_{0} E_{1})) E∗) when E_{0} is invariable.

(define I_{1}) . . . (define I_{i}) . . . (define I_{n})

(letrec ((I_{n+1} C_{n+1}[I_{i}]) …)

(begin

(set! I_{1} C_{1}[I_{i}])

⋮ (set! I_{i} E_{i})

⋮ (set! I_{n} C_{n}[I_{i}]) C_{0}[I_{i}]))

⟹

(define I_{1}) . . . (define I_{i}) . . . (define I_{n})

(letrec ((I_{n+1} C_{n+1}[E_{i}]) …)

(begin

(set! I_{1} C_{1}[E_{i}])

⋮ (set! I_{i} E_{i})

⋮ (set! I_{n} C_{n}[E_{i}]) C_{0}[E_{i}]))

when I_{i} is immutable and E_{i} is a constant or an immutable variable reference.

Figure 3.1: Defined Constant Substitution

15. begin in a combination rotation.

(E_{0} (begin E∗ E)) ⟹ (begin E∗ (E_{0} E))

when E_{0} is invariable.

16. Defined constant substitution. If an immutable variable is defined to be a constant or another immutable variable, the value is universally substituted. See Figure 3.1.

17. Unused initializer elimination. If a defined immutable variable is never referenced and it is initialized with a side-effect free expression, the initialization can be eliminated.

3.2 Usage of the Rules

The rules result in program transformations similar to those produced by other compilers [8, 6]. The rules for conditionals are the same, and the rules for β-conversion look different only to facilitate correctness proofs. The letrec rules implement the inlining of procedures and closure hoisting.

One major difference between this compiler and the others is it does not convert the program into continuation-passing style [15]. As a result, the rotate combinations rule was added. Here is a common example of its use.

(let ((I_{0} (let ((I_{1} E_{1}) …) E∗ I_{1}))) E_{0})

⟹ (let ((I_{1} E_{1}) …) (let ((I_{0} I_{1})) E∗ E_{0}))

The rules are used as follows. With the exception of the letrec substitution rule and the defined constant substitution rule, all of the rules are applied by an expression simplifier. The simplifier always terminates. After the initial simplification, expressions are maintained in simplified form by the use of expression constructors that invoke the simplifier.

The next step is to repeatedly try defined constant substitution until there is no place it can be applied. This is followed by letrec substitution. If the letrec substitution phase applies no rules, the process terminates, otherwise, a new cycle of defined constant and letrec substitution is initiated.

letrec substitution replaces a letrec bound variable which occurs in the operator position of a combination with its binding. The letrec substitution phase has two modes. It substitutes any binding which binds a lambda expression containing a letrec expression. In these bindings, the letrec lifting rule has failed to hoist a closure so the substitution is required.

In the second mode, it substitutes any binding which binds a lambda expression with a simple body or one which has been marked by the use of a define-integrable form. A simple lambda body is a constant, a variable, a combination in which the operator is a variable and the operands are either variables or constants, or a primitive in which the arguments are either variables or constants.

Programmers beware: the letrec substitution phase may never terminate as the following program demonstrates.

     (define *x* 2)
     (define-integrable (loop x)
       (if (positive? x) (loop (- x 1)) x))
     (loop *x*)

However, the letrec substitution phase may be used to force computations at compile time. The loop in the following example must be unwound by all compilers.

     (define-integrable (floor-log2 x a)
       (if (<= x 1)
           a
           (floor-log2 (ashr x 1) (+ 1 a))))
     (define log-bytes-per-word
       (floor-log2 bytes-per-word 0))
     (if (not (= (ashl 1 log-bytes-per-word) bytes-per-word))
         (err 1 "Word size not a power of two"))

As an example, consider the even-odd program given in Figure 3.2. It specifies a simple iterative process. Figures 3.3 through 3.8 show how this program might be translated into Simple PreScheme using transformations implemented in the Front End.

3.3 Justification of the Rules

The application of a rule is justified if it transforms a Macro-Free PreScheme program into another and both programs have the same meaning as given by the semantics in Section 2.2. Some of the rules have another interesting property—they can transform a program which has bottom denotation into a program which produces a non-bottom answer. For example, the program

     (define two (+ 1 one))
     (define one 1)
     two

(define number 77)                      ; This program
(define (dec x) (- x 1))                ; produces zero
(define (even x)                        ; if NUMBER is even
  (if (zero? x)                         ; and non-negative,
      0                                 ; otherwise it
      (odd (dec x))))                   ; produces one.
(define (odd x)
  (if (zero? x)
      1
      (even (dec x))))
(if (negative? number)
    1
    (even number))

Figure 3.2: Example vlisp PreScheme Program

(define number)
(define dec)
(define even)
(define odd)
(begin
  (set! number 77)
  (set! dec (lambda (x) (- x 1)))
  (set! even (lambda (y) (if (= 0 y) 0 (odd (dec y)))))
  (set! odd (lambda (z) (if (= 0 z) 1 (even (dec z)))))
  (if (> 0 number) 1 (even number)))

Figure 3.3: Expand into Macro-Free PreScheme

(define number) (define dec) (define even) (define odd)
(begin
(set! number 77)
(set! dec (letrec ((dec-0 (lambda (x) (- x 1))) dec-0)))
(set! even (letrec ((even-0 (lambda (y)
                             (if (= 0 y)
                                 0
                                 (odd (dec y)))))
                    even-0)))
(set! odd (letrec ((odd-0 (lambda (z)
                           (if (= 0 z)
                               1
                               (even (dec z)))))
                   odd-0)))
(if (> 0 number) 1 (even number)))

Figure 3.4: Name Anonymous Lambda Expressions

(define number) (define dec) (define even) (define odd)
(letrec
  ((dec-0 (lambda (x) (- x 1)))
   (even-0 (lambda (y) (if (= 0 y) 0 (odd (dec y)))))
   (odd-0 (lambda (z) (if (= 0 z) 1 (even (dec z))))))
(begin
  (set! number 77)
  (set! dec dec-0)
  (set! even even-0)
  (set! odd odd-0)
  (if (> 0 number) 1 (even number))))

Figure 3.5: Closure Hoisting

(define number) (define dec) (define even) (define odd)
(letrec
((dec-0 (lambda (x) (- x 1)))
 (even-0 (lambda (y) (if (= 0 y) 0 (odd-0 (dec-0 y)))))
 (odd-0 (lambda (z) (if (= 0 z) 1 (even-0 (dec-0 z))))))
(begin
(set! number 77) (set! dec dec-0)
(set! even even-0) (set! odd odd-0)
(if (> 0 77)                        ; Which simplifies
    1                               ; to (even-0 77).
    (even-0 77))))

Figure 3.6: Constant Folding

(define number) (define dec) (define even) (define odd)
(letrec
((dec-0 (lambda (x) (- x 1)))
 (even-0 (lambda (y) (if (= 0 y) 0 (odd-0 (- y 1)))))
 (odd-0 (lambda (z) (if (= 0 z) 1 (even-0 (- z 1))))))
(begin
(set! number 77) (set! dec dec-0)
(set! even even-0) (set! odd odd-0)
(even-0 77)))

Figure 3.7: Inline Non-Tail-Recursive Procedure Calls

(define number) (define dec) (define even) (define odd)
(letrec
    ((even-0 (lambda (y) (if (= 0 y) 0 (odd-0 (- y 1)))))
     (odd-0 (lambda (z) (if (= 0 z) 1 (even-0 (- z 1))))))
  (begin
    (set! number 0) (set! dec 0)
    (set! even 0) (set! odd 0)
    (even-0 77)))

Figure 3.8: Eliminate Unused Lambda Expressions and Initializers

is transformed into a program which produces the answer 2!

This odd behavior is tolerated so as to allow constant propagation without performing a dependency analysis. In the above example, 1 is substituted for the occurrence of the immutable variable one even though undefined should have been substituted. In summary, the application of a rule is justified if it does not affect non-bottom computational results.

Definition 7 A P-context is a program with some holes. If C[ ] is a context, then (define I_{1}) … (define I_{n}) C[ ] is a P-context.

Definition 8 Assume ∀χσ, wrong χσ = ⊥_{A}. A transformation rule is meaningrefining if for all P-contexts, P [ ], and for all expressions E_{0} and E_{1}, if P [E_{0}] and P [E_{1}] are α-converted and the rule rewrites E_{0} into E_{1}, then P[[P [E_{0}]]] ⊑ P[[P [E_{1}]]].

The proof that a rule is meaning-refining usually has the following form. Suppose E_{1} is the expression that results from applying the rule to expression E_{0}. The proof shows that E[[E_{0}]]ρκσ ⊑ E[[E_{1}]]ρκσ.

The reason the proof shows that a rule is meaning-refining follows. In vlisp PreScheme, the answer domain is the integers. Let P_{1} be a program which results from the application of the rule to an expression in program P_{0} and let P be the semantic function for programs. The proof implies that P[[P_{0}]] ⊑ P[[P_{1}]] because the semantic functions are compositional which implies the rule is meaning-refining, because the answer domain is flat.

The purpose of justifying a rule is to gain confidence in the correctness of the compiler. Justifications focus on aspects of rules which are likely to cause problems. For example, several proposed rules were shown to have predicates which enable their application in contexts which did not refine the meaning of a program. These rules were modified or eliminated.

Justifications do not focus on all aspects of a rule. The compiler avoids name conflicts by using α-converted expressions. Therefore, issues arising from name conflicts are not addressed. A formal semantics for each primitive has not been provided, therefore, the rules specific to primitives have not been justified. When the justification of a rule is too obvious, it has been omitted, with the exception of the justification of the if in the consequence of an if rule.

The justification of many rules employs structural induction involving a large number of cases. The complete proof is sketched by providing a detailed analysis of the most interesting cases.

The formal semantics of vlisp PreScheme require that the order of evaluation within a call is constant throughout a program for any given number of arguments. Most proofs assume arguments are evaluated left-to-right, and then the operator is evaluated. The reader will observe that the order of evaluation is relevant only in the rotate combinations rule.

The justification of rules with non-trivial predicates requires associating semantics properties with syntactic ones. Side-effect free expressions have property Π.

Definition 9 Π(E) is ∀ρσ, ∃ϵ, ∀κ, E[[E]]ρκσ = (ϵ = undefined → ⊥_{A}, κϵσ).

To understand this definition, ignore the case in which ϵ = undefined. Notice the store given to the command continuation on the lhs is the same as the one given to the command continuation on the rhs. In other words, the command continuation on the lhs is the composition of the identity function and command continuation representing the rest of the computation. This characterizes the meaning of side-effect free expressions in a form useful for proofs.

Theorem 1 E is side-effect free implies Π(E).

Proof sketch: This is proved by structural induction on side-effect free expressions. The cases of E being I and (if E_{0} E_{1} E_{2}) are shown.

Case E = I. Let ϵ = ρI ∈ E → ρI | E, σ(ρI | L)↓1. Expanding definitions gives

E[[I]]ρκσ = (ϵ = undefined → ⊥_{A}, κϵσ).

Notice ϵ is independent of κ so

∀κ, E[[I]]ρκσ = (ϵ = undefined → ⊥_{A}, κϵσ).

Case E = (if E_{0} E_{1} E_{2}). By the induction hypothesis, there is at least one ϵ_{0} such that

∀κ, E[[E_{0}]]ρκσ = (ϵ_{0} = undefined → ⊥_{A}, κϵ_{0}σ).

If ϵ_{0} = undefined, the result is immediate, otherwise,

E[[(if E_{0} E_{1} E_{2})]]ρκσ
= E[[E_{0}]]ρ(λϵ. truish ϵ → E[[E_{1}]]ρκ, E[[E_{2}]]ρκ)σ
= truish ϵ_{0} → E[[E_{1}]]ρκσ, E[[E_{2}]]ρκσ.

When ϵ_{0} = false,

E[[(if E_{0} E_{1} E_{2})]]ρκσ = E[[E_{2}]]ρκσ,

otherwise,

E[[(if E_{0} E_{1} E_{2})]]ρκσ = E[[E_{1}]]ρκσ.

Use of the induction hypothesis verifies both alternatives.

Invariable expressions have property Σ.

Definition 10 Σ(E) is ∀ρσ, ∃ϵ, ∀σ′,

(∀I ∈ F V (E), ρI ∈ L implies σ(ρI | L) ↓ 1 = σ′(ρI | L) ↓ 1)
implies ∀κ, E[[E]]ρκσ′ = (ϵ = undefined → ⊥_{A}, κϵσ′).

Theorem 2 E is invariable implies Σ(E).

Proof sketch: The proof is identical to that of Theorem 1, except for the case of variables. As before

∀κ, E[[I]]ρκσ = (ϵ = undefined → ⊥_{A}, κϵσ),

with ϵ = ρI ∈ E → ρI | E, σ(ρI | L) ↓ 1. For all σ′ such that

ρI ∈ L implies σ(ρI | L) ↓ 1 = σ′(ρI | L) ↓ 1,

ϵ = ρI ∈ E → ρI | E, σ′(ρI | L) ↓ 1, so E[[I]]ρκσ = E[[I]]ρκσ′.

The following obvious lemmas aid in the proofs of the rules. Lemma 1 Σ(E) implies Π(E). Lemma 2 When I∗_{0} § I∗_{1} are distinct,

extends(extends ρI∗_{0}ϵ∗_{0})I∗_{1}ϵ∗_{1} = extends ρ(I∗_{0} § I∗_{1})(ϵ∗_{0} § ϵ∗_{1}). Lemma 3

B[[B_{0}B_{1}]](I[[B_{0}B_{1}]])ρ

= λϵ∗. B[[B_{0}]]\begin{matrix}(I[[B_{0}]]) \\ (extends ρ(I[[B_{1}]])(dropfirst ϵ∗#B_{0})) \\ (takefirst ϵ∗#B_{0}) \end{matrix} § B[[B_{1}]]\begin{matrix}(I[[B_{1}]]) \\ (extends ρ(I[[B_{0}]])(takefirst ϵ∗#B_{0})) \\ (dropfirst ϵ∗#B_{0}) \end{matrix}

3.3.1 if in the Consequence of an if

Theorem 3 When E_{0} is side-effect free,

E[[(if E_{0} (if E_{0} E_{1} E_{2}) E_{3})]]ρκσ = E[[(if E_{0} E_{1} E_{3})]]ρκσ. Proof: By Theorem 1, there exists an ϵ_{0} such that

∀κ, E[[E_{0}]]ρκσ = (ϵ_{0} = undefined → ⊥_{A}, κϵ_{0}σ). If ϵ_{0} = undefined, the proof is immediate, so assume ϵ_{0} ≠ undefined.

E[[(if E_{0} (if E_{0} E_{1} E_{2}) E_{3})]]ρκσ = E[[E_{0}]]ρ(λϵ. truish ϵ → E[[(if E_{0} E_{1} E_{2})]]ρκ, E[[E_{3}]]ρκ)σ = truish ϵ_{0} → E[[(if E_{0} E_{1} E_{2})]]ρκσ, E[[E_{3}]]ρκσ = truish ϵ_{0} → E[[E_{0}]]ρ(λϵ. truish ϵ → E[[E_{1}]]ρκ, E[[E_{2}]]ρκ)σ, E[[E_{3}]]ρκσ = truish ϵ_{0} → truish ϵ_{0} → E[[E_{1}]]ρκσ, E[[E_{2}]]ρκσ, E[[E_{3}]]ρκσ = truish ϵ_{0} → E[[E_{1}]]ρκσ, E[[E_{3}]]ρκσ = E[[E_{0}]]ρ(λϵ. truish ϵ → E[[E_{1}]]ρκ, E[[E_{3}]]ρκ)σ = E[[(if E_{0} E_{1} E_{3})]]ρκσ

3.3.2 lambda Simplification

Theorem 4 When E_{i} is side-effect free and I_{i} is not free in E,

E[[((lambda (I_{1} … I_{i} … I_{n}) E) E_{1} … E_{i} … E_{n})]]ρκσ

⊑ E[[((lambda (I_{1} … I_{i−1} I_{i+1} … I_{n}) E) E_{1} … E_{i−1} E_{i+1} … E_{n})]]ρκσ.

Proof: Pick a permutation for the application. Shown is the case in which the arguments are evaluated left-to-right and then the operator is evaluated.

E[[((lambda (I∗) E) E∗)]]ρκσ
= E∗[[E∗]]ρ(λϵ∗. applicate(L[[(lambda (I∗) E)]]ρ)ϵ∗κ)σ

Consider the case in which there exists κ′ and σ′ such that

E[[E_{i}]]ρκ′σ′ = E[[((lambda (I_{1} … I_{i} … I_{n}) E) E_{1} … E_{i} … E_{n})]]ρκσ,

and ϵ_{i} such that

∀κ, E[[E_{i}]]ρκσ′ = (ϵ_{i} = undefined → ⊥_{A}, κϵ_{i}σ′).

If ϵ_{i} = undefined, the proof is immediate, so assume that ϵ_{i} ≠ undefined. Also assume there exists ϵ_{1} … ϵ_{i−1}ϵ_{i+1} … ϵ_{n}, σ′′, and ψ such that,

E∗[[E_{1} … E_{i} … E_{n}]]ρψσ = ψ⟨ϵ_{1} … ϵ_{i} … ϵ_{n}⟩σ′′.

This corresponds to the case in which the evaluation of each of E_{1} … E_{n} invokes their continuation with a value; for when they do not, the proof is again immediate. Notice that the evaluation of E_{i} does not change the store so

E∗[[E_{1} … E_{i−1} E_{i+1} … E_{n}]]ρψ′σ = ψ′⟨ϵ_{1} … ϵ_{i−1}ϵ_{i+1} … ϵ_{n}⟩σ′′.

In the case in which the computation continues, the proof is concluded by showing

applicate(L[[(lambda (I_{1} … I_{i} … I_{n}) E)]]ρ)⟨ϵ_{1} … ϵ_{i} … ϵ_{n}⟩κσ′′
= applicate (L[[(lambda (I_{1} … I_{i−1} I_{i+1} … I_{n}) E)]]ρ) ⟨ϵ_{1} … ϵ_{i−1}ϵ_{i+1} … ϵ_{n}⟩κσ′′.

Expanding the definitions gives

E[[E]](extends ρ⟨I_{1} … I_{i} … I_{n}⟩⟨ϵ_{1} … ϵ_{i} … ϵ_{n}⟩)κσ′′
= E[[E]](extends ρ⟨I_{1} … I_{i−1} I_{i+1} … I_{n}⟩⟨ϵ_{1} … ϵ_{i−1}ϵ_{i+1} … ϵ_{n}⟩)κσ′′.

This is proved by structural induction on E assuming I_{i} is not free in E.

3.3.3 β-substitution

There are two cases for β-substitution. The expressions substituted can be invariable or side-effect free.

β-substitution of invariable expressions

Theorem 5 When E_{i} is invariable,

E[[((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ
⊑ E[[((lambda (I_{1} … I_{i} … I_{n}) C[E_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ.

Note the rhs must be α-converted so I_{i} cannot be free in E_{i}. The theorem is proved by appealing to Lemma 4 and Lemma 5 which follow.

Lemma 4 When E_{i} is invariable,

E[[((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ

⊑ E[[(\begin{matrix}(lambda (I_{1} … I_{i} … I_{n}) \\ ((lambda (I_{i}) C[I_{i}]) E_{i})) \\ E_{1} … E_{i} … E_{n})]]ρκσ. \end{matrix}

Proof: For the same reasons employed in Theorem 4, consider only values κ′ and σ′ such that

E[[E_{i}]]ρκ′σ′ = E[[((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ,

and ϵ_{1} … ϵ_{n}, σ′′, and ψ such that ϵ_{i} ≠ undefined, and

E∗[[E_{1} … E_{i} … E_{n}]]ρψσ = ψ⟨ϵ_{1} … ϵ_{i} … ϵ_{n}⟩σ′′.

Let ρ′ = expand ρ⟨I_{1} … I_{i} … I_{n}⟩⟨ϵ_{1} … ϵ_{i} … ϵ_{n}⟩. Expanding definitions gives

E[[(\begin{matrix}(lambda (I_{1} … I_{i} … I_{n}) \\ ((lambda (I_{i}) C[I_{i}]) E_{i})) \\ E_{1} … E_{i} … E_{n})]]ρκσ \end{matrix}

= E[[((lambda (I_{i}) C[I_{i}]) E_{i})]]ρ′κσ′′

= E[[E_{i}]]ρ′(λϵ. applicate(L[[(lambda (I_{i}) C[I_{i}])]]ρ′)κ)σ′′ = E[[E_{i}]]ρ(λϵ. applicate(L[[(lambda (I_{i}) C[I_{i}])]]ρ′)κ)σ′′

because none of I_{1} … I_{n} are free in E_{i}.

∀κ, E[[E_{i}]]ρκσ′′ = κϵ_{i}σ′′, for if not, then at least one of the free variables of E_{i} was initialized. Let I_{0} be one. The semantics allow only a change from a value of undefined, so σ′(ρI_{0} | L) ↓ 1 = undefined. Therefore, E_{i} must ignore the value of I_{0} and the values of variables referenced by E_{i} must agree in both stores.

E[[E_{i}]]ρ(λϵ. applicate(L[[(lambda (I_{i}) C[I_{i}])]]ρ′)κ)σ′′
= E[[C[I_{i}]]](extends ρ′⟨I_{i}⟩⟨ϵ_{i}⟩)κσ′′
= E[[C[I_{i}]]]ρ′κσ

because ρ′ = extends ρ′⟨I_{i}⟩⟨ϵ_{i}⟩.

Lemma 5 When E is invariable,

(∃ϵ, ϵ ≠ undefined ∧∀κ, E[[E]]ρκσ = κϵσ)
implies E[[((lambda (I) C[I]) E)]]ρκσ = E[[C[E]]]ρκσ.

Proof sketch: Proved by induction on contexts. The cases of C[ ] being [ ] and (begin C_{0}[ ] C_{1}[ ]) are shown. Assume there exists an ϵ_{0} ≠ undefined such that ∀κ, E[[E]]ρκσ = κϵ_{0}σ. Pick a permutation for the application. Shown is the case in which the argument is evaluated before the operator.

E[[((lambda (I) C[I]) E)]]ρκσ

= E[[E]]ρ(λϵ′. E[[(lambda (I) C[I])]]ρ(λϵ. applicate ϵ⟨ϵ′⟩κ))σ
= E[[(lambda (I) C[I])]]ρ(λϵ. applicate ϵ⟨ϵ_{0}⟩κ)σ
= applicate(L[[(lambda (I) C[I])]]ρ)⟨ϵ_{0}⟩κσ
= E[[C[I]]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κσ

Case of C[ ] = [ ]: E[[C[I]]] = E[[I]]. The proof follows from the semantics of variable reference.

Case of C[ ] = (begin C_{0}[ ] C_{1}[ ]): To be shown is

E[[(begin C_{0}[I] C_{1}[I])]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κσ

= E[[(begin C_{0}[E] C_{1}[E])]]ρκσ.

Expanding begin’s definition gives

E[[(begin C_{0}[E] C_{1}[E])]]ρκσ = E[[C_{0}[E]]]ρ(λϵ. E[[C_{1}[E]]]ρκ)σ

and

E[[(begin C_{0}[I] C_{1}[I])]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κσ
= E[[C_{0}[I]]](extends ρ⟨I⟩⟨ϵ_{0}⟩)(λϵ. E[[C_{1}[I]]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κ)σ
= E[[C_{0}[E]]]ρ(λϵ. E[[C_{1}[I]]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κ)σ

using the induction hypothesis for the last equality.

Assume there exists a σ′ such that

E[[C_{1}[E]]]ρκσ′ = E[[C_{0}[E]]]ρ(λϵ. E[[C_{1}[E]]]ρκ)σ

which corresponds to the case in which the evaluation of C_{0}[E] invokes its continuation with a value. ∀κ, E[[E]]ρκσ′ = κϵ_{0}σ′, for if not, then at least one of the free variables of E was initialized. Let I_{0} be one. The semantics allow only a change from a value of undefined, so σ(ρI_{0} | L) ↓ 1 = undefined. Therefore, E must ignore the value of I_{0} and the values of variables referenced by E must agree in both stores.

The proof is completed by use of the induction hypothesis to show

E[[C_{1}[E]]]ρκσ′ = E[[C_{1}[I]]](extends ρ⟨I⟩⟨ϵ_{0}⟩)κσ′.

β-substitution of side-effect free expressions

Theorem 6 When E_{1} … E_{i} … E_{n} are side-effect free and C[I_{i}] is almost side-effect free,

E[[((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ
= E[[((lambda (I_{1} … I_{i} … I_{n}) C[E_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ.

Note the rhs must be α-converted so I_{i} cannot be free in E_{i}. The theorem is proved by appealing to Lemma 6 and Lemma 7 which follow.

Lemma 6 When E_{1} … E_{i} … E_{n} are side-effect free,

E[[((lambda (I_{1} … I_{i} … I_{n}) C[I_{i}]) E_{1} … E_{i} … E_{n})]]ρκσ

= E[[(\begin{matrix}(lambda (I_{1} … I_{i} … I_{n}) \\ ((lambda (I_{i}) C[I_{i}]) E_{i})) \\ E_{1} … E_{i} … E_{n})]]ρκσ. \end{matrix}

The proof is identical to that of Lemma 4 except that the store never changes, i.e., σ′′ = σ′ = σ.

Lemma 7 When E_{i} is side-effect free and C[I_{i}] is almost side-effect free,

(∃ϵ, ϵ ≠ undefined ∧∀κ, E[[E]]ρκσ = κϵσ)
implies E[[((lambda (I) C[I]) E)]]ρκσ = E[[C[E]]]ρκσ.

Proof sketch: The proof is very similar to the proof of Lemma 5, except that the store remains the same. Consider the case of C[ ] being (begin C_{0}[ ] C_{1}[ ]) and all ϵ ≠ undefined such that ∀κ, E[[E]]ρκσ = κϵσ. Because C[E] is almost side-effect free, C_{0}[E] is side-effect free. In the case in which the evaluation of C_{0}[E] invokes its continuation with a value,

E[[C_{1}[E]]]ρκσ = E[[C_{0}[E]]]ρ(λϵ. E[[C_{1}[E]]]ρκ)σ.

The proof is completed by use of the induction hypothesis to show

E[[C_{1}[E]]]ρκσ = E[[C_{1}[I]]](extends ρ⟨I⟩⟨ϵ⟩)κσ.

3.3.4 letrec Lifting

Theorem 7 When C[ ] has one hole,

E[[C[(letrec (B) E)]]]ρκσ = E[[(letrec (B) C[E])]]ρκσ.

Note the rhs must be α-converted so C[ ] cannot bind any free variables bound by B. Proof sketch: Shown is the case in which C[ ] = (lambda (I∗) C_{0}[ ]).

E[[C[(letrec (B) E)]]]ρκσ
= E[[(lambda (I∗) C_{0}[(letrec (B) E)])]]ρκσ
= κ(L[[(lambda (I∗) C_{0}[(letrec (B) E)])]]ρ)σ
= κ(L[[(lambda (I∗) (letrec (B) C_{0}[E]))]]ρ)σ

by the induction hypothesis.

L[[(lambda (I∗) (letrec (B) C_{0}[E]))]]ρ
= (λϵ∗κ. #ϵ∗ = #I∗ → E[[(letrec (B) C_{0}[E])]]ρ′κ, λσ. ⊥_{A}) in E
= (λϵ∗κ. #ϵ∗ = #I∗ → E[[C_{0}[E]]]ρ′′κ, λσ. ⊥_{A}) in E

where ρ′ = extends ρI∗ϵ∗ and ρ′′ = extends ρ′(I[[B]])(fix(B[[B]](I[[B]])ρ′)). Since C[ ] binds no free variables of B, it binds none of I∗ and

ρ′′ = extends ρ′(I[[B]])(fix(B[[B]](I[[B]])ρ))

Furthermore, because all expressions are α-converted, ρ′′ = extends ρ′′′I∗ϵ∗, where ρ′′′ = extends ρ(I[[B]])(fix(B[[B]](I[[B]])ρ)).

L[[(lambda (I∗) (letrec (B) C_{0}[E]))]]ρ
= L[[(lambda (I∗) C_{0}[E])]]ρ′′′
E[[(lambda (I∗) C_{0}[E])]]ρ′′′κσ
= E[[(letrec (B) (lambda (I∗) C_{0}[E]))]]ρκσ

3.3.5 letrec Expression Merging

Theorem 8

E[[(letrec (B_{0}) (letrec (B_{1}) E))]]ρκσ
= E[[(letrec (B_{0} B_{1}) E)]]ρκσ.

Note the lhs must be α-converted so no binding in B_{0} can reference a variable bound by B_{1}. Proof: Let f_{0} = B[[B_{0}]](I[[B_{0}]])ρ, ρ′ = extends ρ(I[[B_{0}]])(fix f_{0}), f_{1} = B[[B_{1}]](I[[B_{1}]])ρ′.

E[[(letrec (B_{0}) (letrec (B_{1}) E))]]ρκσ
= E[[(letrec (B_{1}) E)]]ρ′κσ
= E[[E]](extends ρ′(I[[B_{1}]])(fix f_{1}))κσ

Because expressions are α-converted,

extends ρ′(I[[B_{1}]])(fix f_{1})
= extends ρ(I[[B_{0}B_{1}]])(fix f_{0} § fix f_{1}).

Let f_{01} = B[[B_{0}B_{1}]](I[[B_{0}B_{1}]])ρ.

E[[(letrec (B_{0} B_{1}) E)]]ρκσ
= E[[E]](extends ρ(I[[B_{0}B_{1}]])(fix f_{01}))κσ

The proof is completed by showing fix f_{01} = fix f_{0} § fix f_{1}.

f_{01} = λϵ∗. B[[B_{0}]]\begin{matrix}(I[[B_{0}]]) \\ (extends ρ(I[[B_{1}]])(dropfirst ϵ∗#B_{0})) \\ (takefirst ϵ∗#B_{0}) \end{matrix} § B[[B_{1}]]\begin{matrix}(I[[B_{1}]]) \\ (extends ρ(I[[B_{0}]])(takefirst ϵ∗#B_{0})) \\ (dropfirst ϵ∗#B_{0}) \end{matrix}

= λϵ∗. B[[B_{0}]](I[[B_{0}]])ρ(takefirst ϵ∗#B_{0}) § B[[B_{1}]]\begin{matrix}(I[[B_{1}]]) \\ (extends ρ(I[[B_{0}]])(takefirst ϵ∗#B_{0})) \\ (dropfirst ϵ∗#B_{0}) \end{matrix}

= λϵ∗. f_{0}(takefirst ϵ∗#B_{0}) § B[[B_{1}]]\begin{matrix}(I[[B_{1}]]) \\ (extends ρ(I[[B_{0}]])(takefirst ϵ∗#B_{0})) \\ (dropfirst ϵ∗#B_{0}) \end{matrix}

because no binding in B_{0} references a variable bound by B_{1}.

Let g = λϵ∗. f_{0}(takefirst ϵ∗#B_{0}) § dropfirst ϵ∗#B_{0}. Superscripts will denote function iteration: f^{0} = λϵ∗. ϵ∗ and f^{n+1} = f ∘ f^{n}. Observe that f_{01}^{n}(fix g) = fix f_{0} § f_{1}^{n}⊥, therefore, ⨆{f_{01}^{n}(fix g)} = fix f_{0} § fix f_{1}.

fix f_{0} § fix f_{1} is a fixed point of f_{01} because

f_{01}(fix f_{0} § fix f_{1})

= f_{01}(⨆{f_{01}^{n}(fix g)})
= ⨆{f_{01}^{n+1}(fix g)}  by continuity
= ⨆{f_{01}^{n}(fix g)}  as fix g ⊑ f_{01}(fix g)
= fix f_{0} § fix f_{1}.

fix f_{0}§fix f_{1} is the least fixed point of f_{01} because, by construction, g^{m}⊥ ⊑ f_{01}^{m}⊥ so f_{01}^{n}(g^{m}⊥) ⊑ f_{01}^{m+n}⊥.

\begin{matrix}f_{01}^{n}(fix g) = f_{01}^{n}(⨆\{g^{m}⊥\}) = ⨆\{f_{01}^{n}(g^{m}⊥)\} \\ ⊑ ⨆\{f_{01}^{n}(f_{01}^{m}⊥)\} = f_{01}^{n}(fix f_{01}) = fix f_{01} \end{matrix}

Therefore f_{01}^{n}(fix g) ⊑ fix f_{01} and fix f_{01} = fix f_{0} § fix f_{1}.

3.3.6 letrec Simplification

Theorem 9 When I is referenced nowhere except in E,

E[[(letrec (B (I (lambda (I∗) E))) E_{0})]]ρκσ
= E[[(letrec (B) E_{0})]]ρκσ.

Proof: By Theorem 7,

E[[(letrec (B (I (lambda (I∗) E))) E_{0})]]ρκσ = E[[(letrec (B) (letrec ((I (lambda (I∗) E))) E_{0}))]]ρκσ.

E[[(letrec ((I (lambda (I∗) E))) E_{0})]]ρκσ = E[[E_{0}]](extends ρ⟨I⟩(fix B[[(I (lambda (I∗) E))]]⟨I⟩ρ))κσ = E[[E_{0}]]ρκσ

because I is not free in E_{0}.

3.3.7 letrec Binding Merging

Theorem 10

E[[(letrec ((I (lambda (I∗) (letrec (B_{0}) E))) B_{1}) E_{0})]]ρκσ
= E[[(letrec (B_{0} (I (lambda (I∗) E)) B_{1}) E_{0})]]ρκσ.

Note the lhs must be α-converted so no binding in B_{1} can reference a variable bound by B_{0}. Proof: Define the bar operator on bindings as follows.

\overline{(I (lambda (I∗) E)) B} = (I (lambda (I∗) (letrec (B_{0}) E))) \overline{B}

In words, it adds a letrec of B_{0} into all the lambda expressions being bound. As was shown in Theorem 9,

E[[(letrec (\overline{B_{0}}) E_{0})]] = E[[E_{0}]],

therefore by use of Theorem 7,

E[[(letrec ((I (lambda (I∗) (letrec (B_{0}) E))) B_{1}) E_{0})]]
= E[[(letrec (\overline{B_{0}} (I (lambda (I∗) (letrec (B_{0}) E))) B_{1}) E_{0})]]
= E[[(letrec (\overline{B_{0} (I (lambda (I∗) E)) B_{1}}) E_{0})]].

Let

B = B_{0} (I (lambda (I∗) E)) B_{1},
f = B[[B]](I[[B]])ρ,
g = B[[\overline{B}]](I[[\overline{B}]])ρ.

The proof is completed by showing fix f = fix g.

f = B[[B_{0} (I (lambda (I∗) E)) B_{1}]](I[[B]])ρ
= λϵ∗. ⟨… L[[(lambda (I∗) E)]](extends ρ(I[[B]])ϵ∗) …⟩
g = B[[\overline{B_{0}} (I (lambda (I∗) (letrec (B_{0}) E))) \overline{B_{1}}]](I[[B]])ρ
= λϵ∗. ⟨… L[[(lambda (I∗) (letrec (B_{0}) E))]] (extends ρ(I[[B]])ϵ∗) …⟩

= λϵ∗. ⟨… L[[(lambda (I∗) E)]] (extends (extends ρ(I[[B]])ϵ∗) (I[[B_{0}]]) (fix(B[[B_{0}]](I[[B]]_{0})(extends ρ(I[[B]])ϵ∗)))) …⟩

Define g_{n} as follows so that g = ⨆{g_{n}}.

h_{n} = λρ. ((B[[\overline{B_{0}}]](I[[\overline{B_{0}}]])ρ)^{n}⊥)
g_{n} = λϵ∗. ⟨… L[[(lambda (I∗) E)]] (extends (extends ρ(I[[B]])ϵ∗) (I[[B_{0}]]) (h_{n}(extends ρ(I[[B]])ϵ∗))) …⟩

fix f ⊑ fix g is proved by showing f^{n+1}⊥ = g_{n}(f^{n}⊥) which implies f^{n+1}⊥ ⊑ g_{n}^{n+1}⊥. The definitions of f and g_{n} suggest that the environments used to evaluate the lambda expressions will be compared. Using Lemma 2, and the fact that h_{n} does not reference any of the variables in I[[B_{0}]] allows a simplification of g_{n}’s environment.

extends (extends ρ(I[[B]])ϵ∗) (I[[B_{0}]]) (h_{n}(extends ρ(I[[B]])ϵ∗))

= extends ρ (I[[B]]) (h_{n}(extends ρ(I[[B]])ϵ∗) § dropfirst ϵ∗#B_{0})

= extends ρ (I[[B]]) (\begin{matrix}h_{n}(extends ρ(⟨I⟩ § I[[B_{1}]])(dropfirst ϵ∗#B_{0})) \\ § dropfirst ϵ∗#B_{0}) \end{matrix}

As a result, showing f^{n+1}⊥ = g_{n}(f^{n}⊥) is the same as showing

f^{n}⊥ = h_{n}(extends ρ(⟨I⟩ § I[[B_{1}]])(dropfirst(f^{n}⊥)#B_{0})) § dropfirst(f^{n}⊥)#B_{0},

which is proved by induction on n.

fix g ⊑ fix f is proved by showing g_{m}^{n}⊥ ⊑ f^{n+m}⊥. Following the same reasoning as before, the proof reduces to showing

f^{n+m}⊥ ⊒ h_{m}(extends ρ(⟨I⟩ § I[[B_{1}]])(dropfirst(f^{n+m}⊥)#B_{0})) § dropfirst(f^{n+m}⊥)#B_{0}.

Induction on m completes the proof because

f(\begin{matrix}h_{m}(extends ρ(⟨I⟩ § I[[B_{1}]])(dropfirst(f^{n+m}⊥)#B_{0})) \\ § dropfirst(f^{n+m}⊥)#B_{0}) \end{matrix}

⊒ h_{m+1}(extends ρ(⟨I⟩ § I[[B_{1}]])(dropfirst(f^{n+m+1}⊥)#B_{0})) § dropfirst(f^{n+m+1}⊥)#B_{0}.

3.3.8 Combination in a Combination Rotation

Theorem 11 When E_{0} is invariable,

E[[(E_{0} ((lambda (I∗) E_{1}) E∗))]]ρκσ
⊑ E[[((lambda (I∗) (E_{0} E_{1})) E∗)]]ρκσ.

Note the lhs must be α-converted so none of I∗ can be free in E_{0}. Proof: Pick a permutation for the applications. Shown is the case in which the arguments are evaluated left-to-right and then the operator is evaluated.

E[[((lambda (I∗) (E_{0} E_{1})) E∗)]]ρκσ

= E∗[[E∗]]ρ(λϵ. applicate(L[[(lambda (I∗) (E_{0} E_{1}))]]ρ)ϵ∗κ)σ

For the same reasons employed in Theorem 4, assume there exists ϵ∗, σ′, and ψ such that E∗[[E∗]]ρψσ = ψϵ∗σ′. Let ρ′ = expand ρI∗ϵ∗. Expanding definitions gives

E[[((lambda (I∗) (E_{0} E_{1})) E∗)]]ρκσ
= E[[(E_{0} E_{1})]]ρ′κσ′
= E[[E_{1}]]ρ′(λϵ. E[[E_{0}]]ρ′(λϵ′. applicate ϵ′⟨ϵ⟩κ))σ′
= E[[E_{1}]]ρ′(λϵ. E[[E_{0}]]ρ(λϵ′. applicate ϵ′⟨ϵ⟩κ))σ′

because none of I∗ are free in E_{0}. Let κ′ = λϵ. E[[E_{0}]]ρ(λϵ′. applicate ϵ′⟨ϵ⟩κ).

E[[E_{1}]]ρ′κ′σ′

= applicate(L[[(lambda (I∗) E_{1})]]ρ)ϵ∗κ′σ′
= E∗[[E∗]]ρ(λϵ∗. applicate(L[[(lambda (I∗) E_{1})]]ρ)ϵ∗κ′)σ
= E[[((lambda (I∗) E_{1}) E∗)]]ρκ′σ
= E[[((lambda (I∗) E_{1}) E∗)]]ρ(λϵ. E[[E_{0}]]ρ(λϵ′. applicate ϵ′⟨ϵ⟩κ))σ
= E[[(E_{0} ((lambda (I∗) E_{1}) E∗))]]ρκσ

Now assume that the operator is evaluated before the arguments. The proof is much like the previous one except now there is the possibility of the rule transforming an erroneous program into one that produces an answer. The situation occurs when the evaluation of one of the arguments to the lambda expression invokes the exit primitive.

The author was unable to write a vlisp PreScheme program with bottom denotation which is transformed by this rule into one which produces a nonbottom answer. Can you?

3.3.9 Defined Constant Substitution

Theorem 12 The rule shown in Figure 3.1 is meaning-refining.

Proof: The compiler rejects programs which contain assignments to immutable variables. The immutable variable I_{i} can be modified only during its initialization. Therefore, for ρ and σ in the program,

ρI_{i} ∈ E → ρI_{i} | E, σ(ρI_{i} | L) ↓ 1

is either undefined or some other value ϵ_{i}.

When E_{i} is a constant, ϵ_{i} = K[[E_{i}]], so E[[I_{i}]]ρκσ ⊑ E[[E_{i}]]ρκσ. When E_{i} is an immutable variable which is undefined at the time of I_{i}’s initialization, the program is erroneous, therefore I_{i} must be defined whenever E_{i} is defined so E[[I_{i}]]ρκσ ⊑ E[[E_{i}]]ρκσ.

PreScheme Assembly Language

PreScheme Assembly Language is a linear assembly language for a stack machine. It is designed to be the target of a translation from Simple Pre-Scheme so many properties of Simple PreScheme are reflected in the language. The language is introduced by giving an informal description of an abstract machine which might execute the language. A formal denotational semantics follows the introduction.

The abstract machine’s state is captured by five terms: a code sequence, a value, a stack, a continuation, and a store. The stack is a sequence of values as is the store. A continuation stores a return point for a non-tail-recursive call. It contains a code sequence, a stack, and another continuation.

There are three types of variables in Simple PreScheme programs: defined variables, letrec bound variables, and lambda bound variables, but only the values of lambda bound variables are placed on the stack. A reference to a lambda bound variable is translated into a stack reference by giving an offset from the stack bottom.

A tail-recursive call is translated into an instruction which simply shuffles the values on the stack and proceeds. A call which must return to the location at which is was invoked must save the return information as a continuation. The make-cont instructions saves the code sequence to be executed after the call, the stack, and the current continuation as a continuation. When a return occurs, the computed result is the value, and the old code sequence,

[figure: …; ϵ∗; κ; frame pointer; return address]

Figure 4.1: Machine Stack Layout

stack, and continuation are replaced by the information saved in the current continuation.

PreScheme Assembly Language was designed to allow translation into very efficient assembly language for a real machine. The defined variables and letrec bound variables can be allocated statically. The continuations and the stack can be allocated on a single machine stack. The machine stack consists of a sequence of frames adjoined to a sequence of values which make up the abstract machine’s stack. A frame pointer marks the beginning of the sequence of values that make up the stack. These values represent the current bindings of lambda bound variables. A reference to a lambda bound variable is translated into a stack reference by giving an offset from the frame pointer as shown in Figure 4.1. In this diagram, the stack grows rightward. The syntactic restrictions of Simple PreScheme allow this simple variable reference scheme.

Each frame on the machine stack stores a continuation. A frame consists of a saved stack, the address of the beginning of the stack, and a return address. For the top continuation, these two addresses are at a fixed offset from the frame pointer. As a result, only one register is needed to maintain both the continuation and the stack. The syntactic restrictions of Simple PreScheme allow stack allocation of continuations.

PreScheme Assembly Language is fairly traditional in all aspects except one: the target of jump instructions are given as offsets rather than labels. The use of offsets easied the task of verifying the Simple PreScheme compiler.

4.1 Abstract Syntax

N ∈ Num natural numbers (Nat = N)
K ∈ Con constants
I ∈ Ide variables
W ∈ Ref variables or natural numbers
Q ∈ Code machine instructions
B′ ∈ Bnd′ bindings
E′ ∈ Exp′ top level expressions
P′ ∈ Pgm′ programs
Pgm′ ⟶ (define I)∗ E′
Exp′ ⟶ (letrec (B′) Q∗)
Bnd′ ⟶ (I Q∗)∗
Ref ⟶ I | N

Code ⟶ (literal K) | (unspecified) | (ignore)
| (fetch W) | (assign W) | (wrong)
| (jump N) | (jump-if-false N) | (dispatch N∗)
| (call W∗) | (return) | (make-cont N N)
| (entry N) | (reserve N) | (dispose N)

| (add W W) | ⋯

4.2 Additional Domain Equation

π ∈ Q = E → F expression instructions
ω ∈ W = D + N instruction denoted values

4.3 Semantic Functions

G : Code∗ → N → Code∗
W : Ref → U → W
F : Code∗ → U → F
Q : Code∗ → U → Q
I′ : Bnd′ → Ide∗
B′ : Bnd′ → Ide∗ → U → E∗ → E∗
E′ : Exp′ → U → F
D′ : Pgm′ → U → K → C
P′ : Pgm′ → A

G[[Q∗]] = λν. dropfirst Q∗ν

W[[I]] = λρ. lookup ρI in W W[[N]] = λρ. N in W

F[[(literal K) Q∗]] = λρ. literal(K[[K]])(Q[[Q∗]]ρ) F[[(unspecified) Q∗]] = λρ. literal unspecified(Q[[Q∗]]ρ) F[[(fetch W) Q∗]] = λρ. fetch(W[[W]]ρ)(Q[[Q∗]]ρ) F[[(make-cont N_{0} N_{1}) Q∗]]

= λρ. makecont N_{0}(Q(G[[Q∗]]N_{1})ρ)(F[[Q∗]]ρ) F[[(entry N) Q∗]] = λρ. entry N(F[[Q∗]]ρ) F[[(reserve N) Q∗]] = λρ. reserve N(F[[Q∗]]ρ) F[[(add W_{0} W_{1}) Q∗]] = λρ. add(W[[W_{0}]]ρ)(W[[W_{1}]]ρ)(Q[[Q∗]]ρ)

Q[[(ignore) Q∗]] = λρ. ignore(F[[Q∗]]ρ) Q[[(assign N) Q∗]] = λρ. setlocal N(Q[[Q∗]]ρ) Q[[(assign I) Q∗]]

= λρ. ismutable I → setglobal(lookup ρI)(Q[[Q∗]]ρ), initglobal(lookup ρI)(Q[[Q∗]]ρ)

Q[[(wrong) Q∗]]

= λρ. λϵϵ∗κ. wrong “assignment of an immutable variable” Q[[(jump N) Q∗]] = Q(G[[Q∗]]N) Q[[(jump-if-false N) Q∗]] = λρ. jumpfalse(F[[Q∗]]ρ)(F(G[[Q∗]]N)ρ) Q[[(dispatch N∗) Q∗]]

= λρ. dispatch(map(λν. F(G[[Q∗]]ν)ρ)N∗)(F[[Q∗]]ρ) Q[[(call W∗) Q∗]] = λρ. call(W∗[[W∗]]ρ) Q[[(return) Q∗]] = λρ. return Q[[(dispose N) Q∗]] = λρ. dispose N(Q[[Q∗]]ρ)

\begin{matrix}I′[[ ]] = ⟨⟩ \\ I′[[(I Q∗) B′]] = ⟨I⟩ § I′[[B′]] \end{matrix}

B′[[ ]] = λI∗ρϵ∗. ⟨⟩ B′[[(I Q∗) B′]] =

λI∗_{0}ρϵ∗. ⟨(F[[Q∗]](extends ρI∗_{0}ϵ∗)) in E⟩ § B′[[B′]]I∗_{0}ρϵ∗

E′[[(letrec (B′) Q∗)]] = λρ. F[[Q∗]](extends ρ(I[[B′]])(fix(B′[[B′]](I′[[B′]])ρ)))

D′[[E′]] = λρκσ. E′[[E′]]ρ⟨⟩κσ D′[[(define I) P′]] =

λρκσ. D′[[P′]](ρ[(new σ) in D/I])κ(update(new σ) undefined σ)

P′[[P′]] = D′[[P′]]ρ_{0}κ_{0}σ_{0}

4.4 Machine Instruction Auxiliary Functions

literal : E → Q → F literal = λϵπ. λϵ∗κ. πϵϵ∗κ

ignore : F → Q ignore = λϕ. λϵϵ∗κ. ϕϵ∗κ fetch : W → Q → F fetch = λωπ. λϵ∗κ. get ωϵ∗λϵ. πϵϵ∗κ

setlocal : N → Q → Q setlocal =

λνπ. λϵϵ∗κ. π unspecified(takefirst ϵ∗ν § ⟨ϵ⟩ § dropfirst ϵ∗(ν + 1))κ

initglobal : D → Q → Q initglobal = λδπ. λϵϵ∗κ. initialize δϵ(π unspecified ϵ∗κ)

setglobal : D → Q → Q setglobal = λδπ. λϵϵ∗κ. assign δϵ(π unspecified ϵ∗κ)

jumpfalse : F → F → Q jumpfalse = λϕ_{0}ϕ_{1}. λϵϵ∗κ. ϵ = false → ϕ_{1}ϵ∗κ, ϕ_{0}ϵ∗κ

dispatch : F ∗ → F → Q dispatch =

\begin{matrix}λϕ∗ϕ. λϵϵ∗κ. \\ (0 ≤ ϵ | R) ∧ (ϵ | R < #ϕ∗) → (ϕ∗ ↓ (1 + ϵ | R))ϵ∗κ, ϕϵ∗κ \end{matrix}

call : W ∗ → Q call = λω∗. λϵϵ∗κ. obtain ω∗ϵ∗λϵ∗. applicate ϵϵ∗κ

return : Q return = λϵϵ∗κ. κϵ

makecont : N → Q → F → F makecont = λνπϕ. λϵ∗κ. ν = #ϵ∗ → ϕϵ∗λϵ. πϵϵ∗κ, wrong “bad stack”

entry : N → F → F entry = λνϕ. λϵ∗κ. ν = #ϵ∗ → ϕϵ∗κ, wrong “bad stack”

reserve : N → F → F reserve = λνϕ. λϵ∗κ. ϕ(ϵ∗ § unspecs ν)κ

dispose : N → Q → Q dispose = λνπ. λϵϵ∗κ. πϵ(takefirst ϵ∗(#ϵ∗ − ν))κ add : W → W → Q → F add =

λω_{0}ω_{1}π.

λϵ∗κ. get ω_{0}ϵ∗λϵ_{0}. get ω_{1}ϵ∗λϵ_{1}. π((ϵ_{0} | R + ϵ_{1} | R) in E)ϵ∗κ

4.5 Additional Auxiliary Functions

stackref : E∗ → N → E stackref = λϵ∗ν. ϵ∗ ↓ (ν + 1)

get : W → E∗ → K → C get = λωϵ∗κ. ω ∈ D → hold(ω | D)κ, send(stackref ϵ∗(ω | N))κ

obtain : W ∗ → E∗ → (E∗ → C) → C obtain =

λω∗ϵ∗ψ. ω∗ = ⟨⟩ → ψ⟨⟩, get(ω∗ ↓ 1)ϵ∗λϵ. obtain(ω∗ † 1)ϵ∗λϵ∗. ψ(⟨ϵ⟩ § ϵ∗)

unspecs : N → E∗ unspecs = λν. ν = 0 → ⟨⟩, ⟨unspecified⟩ § unspecs(ν − 1)

map = λψν∗. ν∗ = ⟨⟩ → ⟨⟩, ⟨ψ(ν∗ ↓ 1)⟩ § map ψ(ν∗ † 1)

ismutable : Ide → T ismutable = Definition follows.

The function ismutable I = true if and only if I is an identifier whose name begins and ends with an asterisk and is at least three characters long.

The Syntax-Directed Compiler

The syntax-directed compiler is given as a function which maps Simple Pre-Scheme programs into PreScheme Assembly Language. The function is presented using the same notation used to map syntactic phrases into semantic values. A syntactic domain is viewed as a kind of semantic domain which always has a countable number of elements. The compiler maps syntactic phrases into a syntactic kind of semantic domain.

The BNF used to define abstract syntax is viewed as another notation for specifying denotational domains. It specifies domains that are constructed using the product and disjoint sum operators. For example, the following fragment from the vlisp PreScheme semantics

Exp ⟶ K | I | (E E∗) | (lambda (I∗) E) | …

is interpreted as

Exp = Con + Ide + App + Lam + ⋯
App = Exp × Exp∗
Lam = Ide∗ × Exp
⋮

The semantic brackets [[·]] allow a familiar BNF-like notation for specifying elements of syntactic domains. For example, E[[(lambda (I∗) E)]] stands for E((I∗, E) in Exp).

The precise mapping from the BNF notation into domain elements is not given, however, for PreScheme Assembly Language, the semantic brackets [[·]] usually denote elements in Code∗ so the following makes sense.

[[(return) Q∗]] = [[(return)]] § Q∗

The functions which define the heart of the compiler^{1} take four arguments. The first argument is the expression being compiled. The second argument is the compile-time environment which records the variables that are allocated on the stack along with their offset. The third argument gives the number of locations on the stack that are already in use or have been reserved for future use. The fourth argument is the code to be appended after the code for the current expression.

CL : Smpl → U_{c} → N → Code∗ → Code∗
CS : Smpl → U_{c} → N → Code∗ → Code∗
CC : Cls → U_{c} → N → Code∗ → Code∗∗
CS∗ : Smpl∗ → U_{c} → N → Code∗ → Code∗
CB : Bnd → Bnd′
CE : Exp → Exp′
CP : Pgm → Pgm′

CL[[(lambda (I∗) S)]]γνQ∗ = CS[[S]]\begin{matrix}(extends_{c} γI∗ν) \\ (ν + #I∗) \\ (isreturn Q∗ → Q∗, mkdispose #I∗Q∗) \end{matrix}

CS[[K]]γνQ∗ = mkliteral KQ∗

CS[[I]]γνQ∗ = mkfetch(varref γI)Q∗

When I∗ contains only lambda bound variables,

CS[[(S I∗)]]γν[[(return) Q∗]] = CS[[S]]γν(mkcall(map(varref γ)I∗)Q∗)

1The Simple PreScheme compiler is very similar to the vlisp byte-code compiler described in [2]. Both compilers have nearly the same architecture, however, their correctness proofs are different.

When S∗ contains something other than lambda bound variables,

CS[[(S S∗)]]γν[[(return) Q∗]] = CS[[((lambda (I∗) (S I∗)) S∗)]]γν[[(return) Q∗]]

where the identifiers I∗ are chosen so that none are free in S.^{2}

CS[[(S S∗)]]γνQ∗ =

let

Q∗_{0} = CS[[(S S∗)]]γν[[(return) Q∗]] in

mkmakecont ν(#Q∗_{0} − #Q∗)Q∗_{0} when isreturn Q∗ = false

CS[[((lambda (I∗) S) S∗)]]γνQ∗ = mkreserve #I∗(CS∗[[S∗]]γ(ν + #I∗)(CL[[(lambda (I∗) S)]]γνQ∗))

CS[[(begin S)]] = CS[[S]]

CS[[(begin S S∗ S_{0})]]γνQ∗ = CS[[S]]γν(mkignore(CS[[(begin S∗ S_{0})]]γνQ∗))

CS[[(if S_{0} S_{1} S_{2})]]γνQ∗ =

let

Q∗_{2} = CS[[S_{2}]]γνQ∗

Q∗_{1} = CS[[S_{1}]]γν(maybemkjump Q∗_{2}Q∗) in

CS[[S_{0}]]γν(mkjumpfalse(#Q∗_{1} − #Q∗_{2})Q∗_{1})

CS[[(if #f #f)]]γνQ∗ = mkunspecfied Q∗

CS[[(case S C)]]γνQ∗ =

let Q∗∗ = CC[[C]]γνQ∗

Q∗_{1} = Q∗∗ ↓ 1

Q∗_{0} = mkunspecified(maybemkjump Q∗_{1}Q∗) in

CS[[S]]γν(mkdispatch(map(λQ∗. #Q∗_{0} − #Q∗)Q∗∗)Q∗_{0})

2The actual compiler allocates a fresh variable only for a simple expression which is not a lambda bound variable.

CS[[(set! I S)]]γνQ∗ = CS[[S]]γν(islocal γI → mkwrong Q∗, mkassign IQ∗)

For lambda bound variables I_{0} and I_{1},

CS[[(+ I_{0} I_{1})]]γνQ∗ = mkadd(varref γI_{0})(varref γI_{1})Q∗

When S_{0} or S_{1} is something other than a lambda bound variable,^{2}

CS[[(+ S_{0} S_{1})]]γνQ∗ = CS[[((lambda (I_{0} I_{1}) (+ I_{0} I_{1})) S_{0} S_{1})]]γQ∗

CS∗[[ ]]γνQ∗ = Q∗

CS∗[[S S∗]]γνQ∗ = CS[[S]]γν(mkassign(ν − #S − 1)(mkignore(CS∗[[S∗]]γνQ∗)))

CC[[((K) S)]]γνQ∗ = ⟨CS[[S]]γνQ∗⟩

CC[[((K) S) C]]γνQ∗ =

let

\begin{matrix}Q∗∗ = CC[[C]]γνQ∗ \\ Q∗_{1} = Q∗∗ ↓ 1 \end{matrix}

in ⟨CS[[S]]γν(maybemkjump Q∗_{1}Q∗)⟩ § Q∗∗

CB[[ ]] = ⟨⟩

CB[[(I (lambda (I∗) S)) B]] =

let

Q∗ = mkentry #I∗(CL[[(lambda (I∗) S)]]γ_{0}0[[(return)]]) in

[[(I Q∗)]] § CB[[B]]

CE[[(letrec (B) S)]] =

let B′ = CB[[B]] Q∗ = mkentry 0(CS[[S]]γ_{0}0[[(return)]])

in [[(letrec (B′) Q∗)]]

CP[[(letrec (B) S)]] = CE[[(letrec (B) S)]]

CP[[(define I) P]] = [[(define I)]] § CP[[P]]

mkliteral KQ∗  = [[(literal K) Q∗]]
mkunspecified Q∗ = [[(unspecified) Q∗]]
mkignore Q∗  = [[(ignore) Q∗]]
mkfetch WQ∗  = [[(fetch W) Q∗]]
mkassign WQ∗  = [[(assign W) Q∗]]
mkwrong IQ∗  = [[(wrong) Q∗]]
mkjump NQ∗  = [[(jump N) Q∗]]
mkjumpfalse NQ∗ = [[(jump-if-false N) Q∗]]
mkdispatch N∗Q∗ = [[(dispatch N∗) Q∗]]
mkcall W∗Q∗  = [[(call W∗) Q∗]]
mkreturn Q∗  = [[(return) Q∗]]
mkmakecont N_{0}N_{1}Q∗ = [[(make-cont N_{0} N_{1}) Q∗]]
mkentry NQ∗  = [[(entry N) Q∗]]
mkreserve NQ∗  = [[(reserve N) Q∗]]
mkdispose NQ∗  = [[(dispose N) Q∗]]
mkadd W_{0}W_{1}Q∗  = [[(add W_{0} W_{1}) Q∗]]

Figure 5.1: Code Generators

5.1 Auxiliary Compiler Functions

This section gives the properties of compile-time environments and defines the function isreturn and maybemkjump. The definition of code generators are given in Figure 5.1.

γ_{0} : U_{c}

extends_{c} : U_{c} → Ide∗ → N → U_{c} extends_{c} γ⟨⟩ν = γ extends_{c} γ(⟨I⟩ § I∗)ν = extends_{c}(extends_{c} γ⟨I⟩ν)I∗(ν + 1)

islocal : U_{c} → Ide → T islocal γ_{0}I_{0} = false islocal(extends_{c} γ⟨I⟩ν)I_{0} = (I = I_{0} ∨ islocal γI_{0}) varref : U_{c} → Ide → Ref varref γ_{0}I_{0} = I_{0} varref (extends_{c} γ⟨I⟩ν)I_{0} = (I = I_{0} → ν, varref γI_{0})

isreturn : Code∗ → T

isreturn = λQ∗. ⟨Q∗ ↓ 1⟩ = [[(return)]]

maybemkjump : Code∗ → Code∗ → Code∗

maybemkjump = λQ∗_{1}Q∗_{0}. isreturn Q∗_{0} → mkreturn Q∗_{1}, mkjump(#Q∗_{1} − #Q∗_{0})Q∗_{1}

5.2 Correctness

The Simple PreScheme compiler is shown to be correct by proving that the denotation of a translated program is the same as the denotation of its source, i.e., P′(CP[[P]]) = P[[P]]. The correctness of this theorem depends on the fact that Simple PreScheme programs are strongly typed. For example, in light of strong typing, one can assume that all procedures receive the correct number of arguments.

An overview of the theorems in this section follows. Theorems 13 through 15 show that the offset computed for branch instructions will cause a jump to the intended location. Theorem 16 shows the correctness of the environment created by a let expression. Theorem 17 and Theorem 18 show the correctness of the compiler on simple and sequences of simple expressions. Theorems 19 through 22 show the correctness of the parts of the compiler which compose multiple sequences of instructions into a complete program.

5.2.1 Code Linearity

Theorem 13 If isreturn Q∗ = false then Q∗ is a suffix of CS[[S]]γνQ∗.

Proof: Inspection of each function involved with the compilation of a simple expression shows that all append their results to the after code Q∗, with one exception: the case of compiling a tail-recursive call. By assumption, the after code does not begin with a return instruction, so the result of compiling a combination is a make-cont instruction appended to a sequence of instructions followed by a call instruction appended to Q∗.

Theorem 14 Q∗ is a suffix of CS[[S]]γν[[(return) Q∗]].

Proof: Inspection of each function involved with the compilation of a simple expression shows that all append their results to the after code [[(return) Q∗]], with one exception: the case of compiling a tail-recursive call. In this case, the return instruction is replaced by a call instruction and Q∗ is still a suffix.

Theorem 15 isreturn(CS[[S]]γνQ∗) = false.

Proof: Inspection of each function involved with the compilation of a simple expression shows that the first instruction produced is never a return instruction.

The following lemma is used to show the correctness of the code generated for conditional expressions. For example, the alternative or else part of an if expression is preceded by the code generated by maybemkjump.

Lemma 8

λϵ. Q(maybemkjump(CS[[S]]γνQ∗)Q∗)ρϵϵ∗κ = λϵ. Q[[Q∗]]ρϵϵ∗κ

Proof: Let Q∗_{0} = CS[[S]]γνQ∗. Assume isreturn Q∗ = true.

λϵ. Q(maybemkjump Q∗_{0}Q∗)ρϵϵ∗κ

= λϵ. Q(mkreturn Q∗_{0})ρϵϵ∗κ
= λϵ. return ϵϵ∗κ
= λϵ. Q[[Q∗]]ρϵϵ∗κ

Assume isreturn Q∗ = false.

λϵ. Q(maybemkjump Q∗_{0}Q∗)ρϵϵ∗κ = λϵ. Q(mkjump(#Q∗_{0} − #Q∗)Q∗_{0})ρϵϵ∗κ

= λϵ. Q(G[[Q∗_{0}]](#Q∗_{0} − #Q∗))ρϵϵ∗κ

= λϵ. Q[[Q∗]]ρϵϵ∗κ

where step two is by use of Theorem 13, using the fact that when Q∗ is a suffix of Q∗_{0}, dropfirst Q∗_{0}(#Q∗_{0} − #Q∗) = Q∗.

5.2.2 Compile-Time Environments

Definition 11

compose = λργϵ∗I. islocal γI → stackref ϵ∗(varref γI) in D, ρI

The compose function combines an environment for lambda bound variables which are on the stack ϵ∗ and in the compile-time environment γ with an environment for defined and letrec bound variables ρ. Lemma 9 shows that the composition of extending a compile time environment is equivalent to extending an environment with some items on the stack.

Lemma 9

compose ρ(extends_{c} γI∗#ϵ∗)(ϵ∗ § ϵ∗_{0})

= extends(compose ργ(ϵ∗ § ϵ∗_{0}))I∗ϵ∗_{0}

Proof: Proved by induction on I∗. The case in which I∗ = ⟨⟩ is trivial, so consider the case in which there is at least one identifier in I∗ and one value

in ϵ∗_{0}.

compose ρ(extends_{c} γ(⟨I⟩ § I∗)#ϵ∗)(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})

= compose ρ(extends_{c}(extends_{c} γ⟨I⟩#ϵ∗)I∗(#ϵ∗ + 1))(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})

= extends(compose ρ(extends_{c} γ⟨I⟩#ϵ∗)(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0}))I∗ϵ∗_{0}
= extends(compose ργ(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})[ϵ in D/I])I∗ϵ∗_{0}
= extends(compose ργ(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0}))(⟨I⟩ § I∗)(⟨ϵ⟩ § ϵ∗_{0})

where step one is by the definition of extends_{c}, step two is by use of the induction hypothesis, step three is by use of the definition of compose, and the final step is a property of extends.

The compile-time environments of interest during compilation contain bindings for a finite number of identifiers. There is a natural number, call it size γ, which gives the largest stack that matters when composing an environment using the compile-time environment γ. A stack ϵ∗ can be truncated to a length of size γ without changing the composed environment. Lemma 10 formalizes this idea.

Definition 12 size : U_{c} → N

size γ_{0} = 0
size(extends_{c} γ⟨I⟩ν) = max(ν + 1, size γ)

Lemma 10 compose ργϵ∗ = compose ργ(takefirst ϵ∗(size γ))

Proof: Consider the expression compose ργϵ∗I. When islocal γI = false, the lemma is trivial, so assume islocal γI = true and assume varref γI = ν. By the definition of size, ν < size γ. Let ν_{0} = size γ − ν − 1.

compose ργ(takefirst ϵ∗(size γ))I = stackref (takefirst ϵ∗(size γ))ν = takefirst ϵ∗(size γ) ↓ (ν + 1) = takefirst ϵ∗(ν_{0} + ν + 1) ↓ (ν + 1) = (⟨ϵ∗ ↓ 1⟩ § ⋯ § ⟨ϵ∗ ↓ (ν + 1)⟩ § takefirst(dropfirst ϵ∗(ν + 1))ν_{0}) ↓ (ν + 1)

= ϵ∗ ↓ (ν + 1) = stackref ϵ∗ν = compose ργϵ∗I

Lemma 11 size γ ≤ ν implies size(extends_{c} γI∗ν) ≤ #I∗ + ν.

Proof: Proved by induction on I∗. When I∗ = ⟨⟩, the proof is trivial, so assume there is at least one identifier.

size(extends_{c} γ(⟨I⟩ § I∗)ν)
= size(extends_{c}(extends_{c} γ⟨I⟩ν)I∗(ν + 1))

The result follows from the use of the induction hypothesis given its assumption is satisfied.

size(extends_{c} γ⟨I⟩ν) ≤ ν + 1

The definition of size shows the assumption is satisfied.

Theorem 16 shows that the correct environment is produced when compiling a let expression.

Theorem 16 Assume #ϵ∗ ≥ #I∗. Let ν = #ϵ∗ − #I∗ and assume size γ ≤ ν.

F(CS[[S]](extends_{c} γI∗ν)#ϵ∗Q∗)ρϵ∗κ
= E[[S]](compose ρ(extends_{c} γI∗ν)ϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

implies

F(CL[[(lambda (I∗) S)]]γνQ∗)ρϵ∗κ = applicate (L[[(lambda (I∗) S)]](compose ργ(takefirst ϵ∗ν))) (dropfirst ϵ∗ν) λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ

Proof: Expanding the lhs of the equation gives

F(CL[[(lambda (I∗) S)]]γνQ∗)ρϵ∗κ = F(CS[[S]]\begin{matrix}(extends_{c} γI∗ν) \\ (ν + #I∗) \\ (isreturn Q∗ → Q∗, mkdispose #I∗Q∗))ρϵ∗κ \end{matrix}

= E[[S]]\begin{matrix}(compose ρ(extends_{c} γI∗ν)ϵ∗) \\ λϵ. Q(isreturn Q∗ → Q∗, mkdispose #I∗Q∗)ρϵϵ∗κ \end{matrix}

by definition of CL and use of an assumption.

Expanding the rhs of the equation gives.

applicate (L[[(lambda (I∗) S)]](compose ργ(takefirst ν)ϵ∗)) (dropfirst ϵ∗ν) λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ

= E[[S]]\begin{matrix}(extends(compose ργ(takefirst ϵ∗ν))I∗(dropfirst ϵ∗ν)) \\ λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ \end{matrix}

= E[[S]]\begin{matrix}(extends(compose ργϵ∗)I∗(dropfirst ϵ∗ν)) \\ λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ \end{matrix}

by definition of L and use of Lemma 10. Appealing to Lemma 9 shows that the environment on both sides of the equation are equal, so the proof is completed by showing that the continuations on both sides are the same.

Assume isreturn Q∗ = true. Let Q∗ = [[(return) Q∗_{0}]].

λϵ. Q(isreturn Q∗ → Q∗, mkdispose #I∗Q∗)ρϵϵ∗κ = λϵ. Q[[Q∗]]ρϵϵ∗κ

= λϵ. Q[[(return) Q∗_{0}]]ρϵϵ∗κ

= λϵ. return ϵϵ∗κ = κ = λϵ. return ϵ(takefirst ϵ∗ν)κ = λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ Assume isreturn Q∗ = false.

λϵ. Q(isreturn Q∗ → Q∗, mkdispose #I∗Q∗)ρϵϵ∗κ = λϵ. Q(mkdispose #I∗Q∗)ρϵϵ∗κ = λϵ. dispose #I∗(Q[[Q∗]]ρ)ϵϵ∗κ = λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗(#ϵ∗ − #I∗))κ = λϵ. Q[[Q∗]]ρϵ(takefirst ϵ∗ν)κ

5.2.3 Simple Expressions

Before the main theorems are presented, a useful lemma about variable reference is given.

Lemma 12

get(W(varref γI)ρ)ϵ∗κ = E[[I]](compose ργϵ∗)κ

Proof: Assume islocal γI = true, and varref γI = ν.

get(ν in W)ϵ∗κ = send(stackref ϵ∗ν)κ = hold(stackref ϵ∗ν in D)κ = hold(compose ργϵ∗I)κ = E[[I]](compose ργϵ∗)κ

Assume islocal γI = false, and varref γI = I.

get(lookup ρI in W)ϵ∗κ = get(ρI in W)ϵ∗κ = hold(ρI)κ = hold(compose ργϵ∗I)κ = E[[I]](compose ργϵ∗)κ

Theorem 17 Assume size γ ≤ #ϵ∗.

F(CS[[S]]γ#ϵ∗Q∗)ρϵ∗κ = E[[S]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ Theorem 18 Assume size γ ≤ #ϵ∗.

F(CS∗[[S∗]]γ(#ϵ∗ + #S∗)Q∗)ρ(ϵ∗ § unspecs #S∗)κ

= E∗[[S∗]](compose ργϵ∗)λϵ∗_{0}. F[[Q∗]]ρ(ϵ∗ § ϵ∗_{0})κ

Proof: The previous two theorems are proved using simultaneous structural induction on simple expressions.

The case of sequences of simple expressions is proved by induction on the sequence of expressions. When there are no expressions, the result is obvious, so consider the case in which there is at least one expression:

Let Q∗_{0} = CS∗[[S∗]]γ(#ϵ∗ + 1 + #S∗)Q∗

F(CS∗[[S S∗]]γ(#ϵ∗ + 1 + #S∗)Q∗)ρ(ϵ∗ § unspecs(1 + #S∗))κ = F(CS[[S]]γ(#ϵ∗ + 1 + #S∗)(mkassign #ϵ∗(mkignore Q∗_{0}))) ρ(ϵ∗ § unspecs(1 + #S∗))κ

= E[[S]]\begin{matrix}(compose ργ(ϵ∗ § unspecs(1 + #S∗)) \\ λϵ. Q(mkassign #ϵ∗(mkignore Q∗_{0})) ρϵ(ϵ∗ § unspecs(1 + #S∗))κ \end{matrix}

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. Q(mkassign #ϵ∗(mkignore Q∗_{0})) ρϵ(ϵ∗ § unspecs(1 + #S∗))κ \end{matrix}

where step one is by definition of CS∗, step two is by use of Theorem 17 as an induction hypothesis, and step three is by use of Lemma 10.

By use of the definition of E∗, the rhs of Theorem 18 becomes

E∗[[S S∗]](compose ργϵ∗)(λϵ∗_{0}. F[[Q∗]]ρ(ϵ∗ § ϵ∗_{0})κ)

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. E∗[[S∗]](compose ργϵ∗)λϵ∗_{0}. F[[Q∗]]ρ(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})κ) \end{matrix}

The lhs and the rhs are equal when their continuations are the same.

λϵ. Q(mkassign #ϵ∗(mkignore Q∗_{0}))ρϵ(ϵ∗ § unspecs(1 + #S∗))κ = λϵ. setlocal #ϵ∗(Q(mkignore Q∗_{0})ρ)ϵ(ϵ∗ § unspecs(1 + #S∗))κ = λϵ. Q(mkignore Q∗_{0})ρ unspecified(ϵ∗ § ⟨ϵ⟩ § unspecs #S∗)κ = λϵ. ignore(F[[Q∗_{0}]]ρ) unspecified(ϵ∗ § ⟨ϵ⟩ § unspecs #S∗)κ = λϵ. F[[Q∗_{0}]]ρ(ϵ∗ § ⟨ϵ⟩ § unspecs #S∗)κ

= λϵ. E∗[[S∗]](compose ργ(ϵ∗ § ⟨ϵ⟩))λϵ∗_{0}. F[[Q∗]]ρ(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})κ

= λϵ. E∗[[S∗]](compose ργϵ∗)λϵ∗_{0}. F[[Q∗]]ρ(ϵ∗ § ⟨ϵ⟩ § ϵ∗_{0})κ

where step one is by definition of mkassign, step two is by definition of setlocal, step three is by definition of mkignore, step four is by definition of ignore, step five is by use of Theorem 18 as an induction hypothesis, and step six is by use of Lemma 10.

Theorem 17 is demonstrated by performing an exhaustive case analysis on each type of simple expression.

Case of constants:

F(CS[[K]]γ#ϵ∗Q∗)ρϵ∗κ = F(mkliteral KQ∗)ρϵ∗κ = literal(K[[K]])(Q[[Q∗]]ρ)ϵ∗κ = Q[[Q∗]]ρ(K[[K]])ϵ∗κ = E[[K]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

Case of variables:

F(CS[[I]]γ#ϵ∗Q∗)ρϵ∗κ = F(mkfetch(varref γI)Q∗)ρϵ∗κ = fetch(W(varref γI)ρ)(Q[[Q∗]]ρ)ϵ∗κ = get(W(varref γI)ρ)ϵ∗λϵ. Q[[Q∗]]ρϵϵ∗κ = E[[I]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

where the last step is by Lemma 12.

Case of a tail-recursive call: The operands of a combination are evaluated left-to-right and then the operator is evaluated, which means that:

E[[(S S∗)]]ρκ = E∗[[S∗]]ρλϵ∗. E[[S]]ρλϵ. applicate ϵϵ∗κ

The order in which the compiler evaluates the operands is determined by the case of a let expression, so for now, assume the operands are all lambda bound variables.

F(CS[[(S I∗)]]γ#ϵ∗[[(return) Q∗]])ρϵ∗κ = F(CS[[S]]γ#ϵ∗(mkcall(map(varref γ)I∗)Q∗))ρϵ∗κ = E[[S]](compose ργϵ∗)λϵ. Q[[mkcall(map(varref γ)I∗)Q∗]]ρϵϵ∗κ

E[[(S I∗)]](compose ργϵ∗)λϵ. Q[[(return) Q∗]]ρϵϵ∗κ = E[[(S I∗)]](compose ργϵ∗)λϵ. return ϵϵ∗κ = E[[(S I∗)]](compose ργϵ∗)κ = E∗[[I∗]](compose ργϵ∗)λϵ∗. E[[S]](compose ργϵ∗)λϵ. applicate ϵϵ∗κ = E[[S]](compose ργϵ∗)λϵ. E∗[[I∗]](compose ργϵ∗)λϵ∗. applicate ϵϵ∗κ where the last step is justified because lambda bound variables are invariable.

The lhs and the rhs are equal when their continuations are the same.

λϵ. Q[[mkcall(map(varref γ)I∗)Q∗]]ρϵϵ∗κ = λϵ. call(W∗(map(varref γ)I∗)ρ)ϵϵ∗κ = λϵ. obtain(W∗(map(varref γ)I∗)ρ)ϵ∗λϵ∗. applicate ϵϵ∗κ = λϵ. E∗[[I∗]](compose ργϵ∗)λϵ∗. applicate ϵϵ∗κ

where step three is by an easy to prove lemma which is analogous to Lemma 12. Case of a non-tail-recursive call (isreturn Q∗ = false):

Let Q∗_{0} = CS[[(S S∗)]]γ#ϵ∗[[(return) Q∗]] F(CS[[(S S∗)]]γ#ϵ∗Q∗)ρϵ∗κ

= F(mkmakecont #ϵ∗(#Q∗_{0} − #Q∗)Q∗_{0})ρϵ∗κ = makecont #ϵ∗(Q(G[[Q∗_{0}]](#Q∗_{0} − #Q∗))ρ)(F[[Q∗_{0}]]ρ)ϵ∗κ = makecont #ϵ∗(Q[[Q∗]]ρ)(F[[Q∗_{0}]]ρ)ϵ∗κ

= F[[Q∗_{0}]]ρϵ∗λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[(S S∗)]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

where step three is true because Q∗_{0} is the result of appending a tail-recursive call to Q∗.

Case of a let expression:

Let Q∗_{0} = CL[[(lambda (I∗) S)]]γ#ϵ∗Q∗ F(CS[[((lambda (I∗) S) S∗)]]γ#ϵ∗Q∗)ρϵ∗κ

= F(mkreserve #I∗(CS∗[[S∗]]γ(#ϵ∗ + #I∗)Q∗_{0}))ρϵ∗κ = F(mkreserve #S∗(CS∗[[S∗]]γ(#ϵ∗ + #S∗)Q∗_{0}))ρϵ∗κ = reserve #S∗(F(CS∗[[S∗]]γ(#ϵ∗ + #S∗)Q∗_{0})ρ)ϵ∗κ = F(CS∗[[S∗]]γ(#ϵ∗ + #S∗)Q∗_{0})ρ(ϵ∗ § unspec #S∗)κ

= E∗[[S∗]](compose ργϵ∗)λϵ∗_{0}. F[[Q∗_{0}]]ρ(ϵ∗ § ϵ∗_{0})κ

= E∗[[S∗]]\begin{matrix}(compose ργϵ∗) \\ λϵ∗_{0}. applicate (L[[(lambda (I∗) S)]](compose ργϵ∗)) ϵ∗_{0} λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix}

= E∗[[S∗]]\begin{matrix}(compose ργϵ∗) \\ λϵ∗_{0}. E[[(lambda (I∗) S)]]\begin{matrix}(compose ργϵ∗) \\ λϵ. applicate ϵϵ∗_{0}λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix} \end{matrix}

= E[[((lambda (I∗) S) S∗)]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ where step one is by the definition of CS, step two uses the fact that a Simple PreScheme program is strongly typed to conclude that #I∗ = #S∗, step three is by definition of mkreserve, step four is by use of Theorem 18 as an induction hypothesis, step five is by use of Theorem 16 and Lemma 11 to prove one of the assumptions of Theorem 16, step six uses the definition lambda abstraction, and step seven uses the definition of application.

The case of a begin expression with one expression is trivial so consider only the case in which there is more than one expression:

F(CS[[(begin S S∗ S_{0})]]γ#ϵ∗Q∗)ρϵ∗κ = F(CS[[S]]γ#ϵ∗(mkignore(CS[[(begin S∗ S_{0})]]γ#ϵ∗Q∗)))ρϵ∗κ

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. Q(mkignore(CS[[(begin S∗ S_{0})]]γ#ϵ∗Q∗))ρϵϵ∗κ \end{matrix}

The rhs of Theorem 17 becomes

E[[(begin S S∗ S_{0})]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. E[[(begin S∗ S_{0})]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix}

The lhs and the rhs are equal when their continuations are the same.

λϵ. Q(mkignore(CS[[(begin S∗ S_{0})]]γ#ϵ∗Q∗))ρϵϵ∗κ

= λϵ. ignore(F(CS[[(begin S∗ S_{0})]]γ#ϵ∗Q∗)ρ)ϵϵ∗κ
= λϵ. F(CS[[(begin S∗ S_{0})]]γ#ϵ∗Q∗)ρϵ∗κ
= λϵ. E[[(begin S∗ S_{0})]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

where the last step is another use of an induction hypothesis.

Case of an if expression:

Let Q∗_{2} = CS[[S_{2}]]γ#ϵ∗Q∗

Q∗_{1} = CS[[S_{1}]]γ#ϵ∗(maybemkjump Q∗_{2}Q∗) F(CS[[(if S_{0} S_{1} S_{2})]]γ#ϵ∗Q∗)ρϵ∗κ

= F(CS[[S_{0}]]γ#ϵ∗(mkjumpfalse(#Q∗_{1} − #Q∗_{2})Q∗_{1}))ρϵ∗κ

= E[[S_{0}]](compose ργϵ∗)λϵ. Q(mkjumpfalse(#Q∗_{1} − #Q∗_{2})Q∗_{1})ρϵϵ∗κ

E[[(if S_{0} S_{1} S_{2})]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[S_{0}]]\begin{matrix}(compose ργϵ∗) \\ λϵ. ϵ = false → E[[S_{2}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ, E[[S_{1}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix}

The lhs and the rhs are equal when their continuations are the same.

λϵ. Q(mkjumpfalse(#Q∗_{1} − #Q∗_{2})Q∗_{1})ρϵϵ∗κ = λϵ. jumpfalse(F[[Q∗_{1}]]ρ)(F(G[[Q∗_{1}]](#Q∗_{1} − #Q∗_{2}))ρ)ϵϵ∗κ = λϵ. jumpfalse(F[[Q∗_{1}]]ρ)(F[[Q∗_{2}]]ρ)ϵϵ∗κ

= λϵ. ϵ = false → F[[Q∗_{2}]]ρϵ∗κ, F[[Q∗_{1}]]ρϵ∗κ

where step two is justified by use of Theorem 13. It is applicable because by Theorem 15, the compiler for simple expressions CS can never generate a code sequence which begins with the return instruction.

The fact that

F[[Q∗_{2}]]ρϵ∗κ = E[[Q∗_{2}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

follows from an induction hypothesis as does

F[[Q∗_{1}]]ρϵ∗κ

= E[[Q∗_{1}]](compose ργϵ∗)λϵ. Q(maybemkjump Q∗_{2}Q∗)ρϵϵ∗κ = E[[Q∗_{1}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

where the last step is by use of Lemma 8.

Case of unspecified:

F(CS[[(if #f #f)]]γ#ϵ∗Q∗)ρϵ∗κ = F(mkunspecified Q∗)ρϵ∗κ = literal unspecified(Q[[Q∗]]ρ)ϵ∗κ = Q[[Q∗]]ρ unspecified ϵ∗κ = send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[#f]]\begin{matrix}(compose ργϵ∗) \\ λϵ. ϵ = false → send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ, E[[#f]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix}

= E[[(if #f #f)]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

Case of case expressions:

Let Q∗∗ = CC[[((0) S_{0}) … ((ν) S_{ν})]]γ#ϵ∗Q∗

Q∗_{1} = Q∗∗ ↓ 1

Q∗_{0} = mkunspecified(maybemkjump Q∗_{1}Q∗) F(CS[[(case S ((0) S_{0}) … ((ν) S_{ν}))]]γ#ϵ∗Q∗)ρϵ∗κ

= F(CS[[S]]γ#ϵ∗(mkdispatch(map(λQ∗. #Q∗_{0} − #Q∗)Q∗∗)Q∗_{0})) ρϵ∗κ

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. Q(mkdispatch(map(λQ∗. #Q∗_{0} − #Q∗)Q∗∗)Q∗_{0})ρϵϵ∗κ \end{matrix}

A case expression is a derived expression which is defined in terms of a sequence of if expressions so that

E[[(case S ((0) S_{0}) … ((ν) S_{ν}))]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. ϵ | R = 0 → E[[S_{0}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ, ⋮ ϵ | R = ν → E[[S_{ν}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ, send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ \end{matrix}

The lhs and the rhs are equal when their continuations are the same, however, before investigating the continuations, the case clauses are considered.

F(Q∗∗ ↓ (ν + 1))ρϵ∗κ
= F(CS[[S_{ν}]]γ#ϵ∗Q∗)ρϵ∗κ
= E[[S_{ν}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

For ν_{0} < ν

F(Q∗∗ ↓ (ν_{0} + 1))ρϵ∗κ = F(CS[[S_{ν_{0}}]]γ#ϵ∗(maybemkjump(Q∗∗ ↓ (ν_{0} + 2))Q∗))ρϵ∗κ

= E[[S_{ν_{0}}]]\begin{matrix}(compose ργϵ∗) \\ λϵ. Q(maybemkjump(Q∗∗ ↓ (ν_{0} + 2))Q∗)ρϵϵ∗κ \end{matrix}

= E[[S_{ν_{0}}]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

where the last step follows directly from Theorem 13 only when ν_{0} = ν − 1. When there are at least three clauses, Q∗∗ ↓ (ν + 1) is a suffix of Q∗∗ ↓ ν, but since Q∗ is a suffix of Q∗∗ ↓ (ν + 1), it is also a suffix of Q∗∗ ↓ ν as the suffix relation is transitive. This argument can be repeated for each ν_{0} < ν justifying the last proof step.

F[[Q∗_{0}]]ρϵ∗κ

= F(mkunspecified(maybemkjump Q∗_{1}Q∗))ρϵ∗κ = literal unspecified(Q(maybemkjump Q∗_{1}Q∗)ρ)ϵ∗κ = Q(maybemkjump Q∗_{1}Q∗)ρ unspecified ϵ∗κ = send unspecified λϵ. Q(maybemkjump Q∗_{1}Q∗)ρϵϵ∗κ = send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ

where the last step follows from an argument similar to the one used for the clauses.

The next step is to show that the computed offsets are correct, that is, for ν_{0} ≤ ν

G[[Q∗_{0}]](#Q∗_{0} − #(Q∗∗ ↓ (ν_{0} + 1))) = Q∗∗ ↓ (ν_{0} + 1).

For ν_{0} = 0, it is obvious that Q∗∗ ↓ 1 is a suffix of Q∗_{0}. For 0 < ν_{0} ≤ ν, CC precedes Q∗∗ ↓(ν_{0} +1) with either a return, call, or a jump instruction and Q∗∗ ↓ (ν_{0} + 1) itself cannot begin with a return instruction by Theorem 15. Therefore, Q∗∗ ↓ (ν_{0} + 1) is a suffix of Q∗_{0}.

Case of assignment for identifiers whose name begins and ends with an asterisk and is at least three characters long (ismutable I = true):

F(CS[[(set! I S)]]γ#ϵ∗Q∗)ρϵ∗κ

= F(CS[[S]]γ#ϵ∗(islocal γI → mkwrong Q∗, mkassign IQ∗))ρϵ∗κ
= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. Q(islocal γI → mkwrong Q∗, mkassign IQ∗)ρϵϵ∗κ \end{matrix}

E[[(set! I S)]](compose ργϵ∗)λϵ. Q[[Q∗]]ρϵϵ∗κ

= E[[S]]\begin{matrix}(compose ργϵ∗) \\ λϵ. assign (lookup(compose ργϵ∗)I) ϵ (send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ) \end{matrix}

The lhs and the rhs are equal when their continuations are the same. Assume islocal γI = true and varref γI = ν.

λϵ. Q(islocal γI → mkwrong Q∗, mkassign IQ∗)ρϵϵ∗κ = λϵ. Q(mkwrong Q∗)ρϵϵ∗κ = λϵ. wrong “assignment of an immutable variable” = λϵ. assign(stackref ϵ∗ν in D)ϵ(send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ) = λϵ. assign (lookup(compose ργϵ∗)I) ϵ (send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ)

where step two is justified by the fact that (stackref ϵ∗ν in D) ∉ L.

Assume islocal γI = false.

λϵ. Q(islocal γI → mkwrong Q∗, mkassign IQ∗)ρϵϵ∗κ = λϵ. Q(mkassign IQ∗)ρϵϵ∗κ = λϵ. setglobal(lookup ρI)(Q[[Q∗]]ρ)ϵϵ∗κ = λϵ. assign(lookup ρI)ϵ(Q[[Q∗]]ρ unspecified ϵ∗κ) = λϵ. assign(lookup ρI)ϵ(send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ) = λϵ. assign (lookup(compose ργϵ∗)I) ϵ (send unspecified λϵ. Q[[Q∗]]ρϵϵ∗κ)

The case of ismutable I = false is similar.

5.2.4 Defined and letrec-Bound Variables

Lemma 13

F(CL[[(lambda (I∗) S)]]γ_{0}0[[(return)]])ρ in E = L[[(lambda (I∗) S)]]ρ

Proof:

L[[(lambda (I∗) S)]]ρ | F = λϵ∗κ. #ϵ∗ = #I∗ → E[[S]](extends ρI∗ϵ∗)κ, wrong “wrong number of arguments”

= λϵ∗κ. E[[S]](extends ρI∗ϵ∗)κ = λϵ∗κ. E[[S]](extends(compose ργ_{0}ϵ∗)I∗ϵ∗)κ = λϵ∗κ. E[[S]](compose ρ(extends_{c} γ_{0}I∗0)ϵ∗)κ = λϵ∗κ. F(CS[[S]](extends_{c} γ_{0}I∗0)#I∗[[(return)]])ρϵ∗κ = F(CS[[S]](extends_{c} γ_{0}I∗0)#I∗[[(return)]])ρ = F(CL[[(lambda (I∗) S)]]γ_{0}0[[(return)]])ρ

where step two is by use of Lemma 13 and the fact that Simple PreScheme programs are strongly typed so procedures will always receive the correct number of arguments, step four is by Lemma 9, and step five is by Theorem 17.

Theorem 19 B′(CB[[B]]) = B[[B]] Proof: Induction on the length of B proves the theorem. The case when [[B]] = ⟨⟩ is trivial, so consider the following.

Let Q∗ = mkentry #I∗(CL[[(lambda (I∗) S)]]γ_{0}0[[(return)]]) B′(CB[[(I (lambda (I∗) S)) B]])

= B′([[(I Q∗)]] § CB[[B]]) = λI∗_{0}ρϵ∗. ⟨(F[[Q∗]](extends ρI∗_{0}ϵ∗)) in E⟩ § B′(CB[[B]])I∗_{0}ρϵ∗ = λI∗_{0}ρϵ∗. ⟨(F[[Q∗]](extends ρI∗_{0}ϵ∗)) in E⟩ § B[[B]]I∗_{0}ρϵ∗ = λI∗_{0}ρϵ∗. ⟨(L[[(lambda (I∗) S)]](extends ρI∗_{0}ϵ∗)) in E⟩ § B[[B]]I∗_{0}ρϵ∗ = B[[(I (lambda (I∗) S)) B]]

where step three is by use of the induction hypothesis and step four is by use of Lemma 13 and the fact that Simple PreScheme programs are strongly typed so that one can ignore the entry instruction.

Theorem 20 E′(CE[[E]])ρ⟨⟩κ = E[[E]]ρκ

Let B′ = CB[[B]]

Q∗ = mkentry 0(CS[[S]]γ_{0}0[[(return)]]) E′(CE[[(letrec (B) S)]])ρ⟨⟩κ

= E′[[(letrec (B′) Q∗)]]ρ⟨⟩κ = F[[Q∗]](extends ρ(I[[B′]])(fix(B′[[B′]](I′[[B′]])ρ)))⟨⟩κ = F[[Q∗]](extends ρ(I[[B]])(fix(B[[B]](I[[B]])ρ)))⟨⟩κ

where the last step is justified by Theorem 19.

Let ρ′ = extends ρ(I[[B]])(fix(B[[B]](I[[B]])ρ)) F[[Q∗]]ρ′⟨⟩κ

= F(mkentry 0(CS[[S]]γ_{0}0[[(return)]]))ρ′⟨⟩κ = entry 0(F(CS[[S]]γ_{0}0[[(return)]])ρ′)⟨⟩κ = F(CS[[S]]γ_{0}0[[(return)]])ρ′⟨⟩κ = E[[S]](compose ρ′γ_{0}⟨⟩)λϵ. Q[[(return)]]ρ′ϵ⟨⟩κ = E[[S]]ρ′λϵ. Q[[(return)]]ρ′ϵ⟨⟩κ = E[[S]]ρ′κ = E[[(letrec (B) S)]]ρκ

where step four is by use of Theorem 17.

Theorem 21 D′(CP[[P]]) = D[[P]] Proof:

D′(CP[[(letrec (B) S)]])ρκ = E′(CP[[(letrec (B) S)]])ρ⟨⟩κ = E[[(letrec (B) S)]]ρκ = D[[(letrec (B) S)]]ρκ

where step two is by Theorem 20.

D′(CP[[(define I) P]])ρκσ = D′([[(define I)]] § CP[[P]])ρκσ = D′(CP[[P]])(ρ[(new σ) in D/I])κ(update(new σ) undefined σ) = D[[P]](ρ[(new σ) in D/I])κ(update(new σ) undefined σ) = D[[(define I) P]]

where step three is by use of the induction hypothesis.

Theorem 22 P′(CP[[P]]) = P[[P]]

Proof: By use of Theorem 21.

P′(CP[[P]]) = D′(CP[[P]])ρ_{0}κ_{0}σ_{0} = D[[P]]ρ_{0}κ_{0}σ_{0} = P[[P]]

Results, Future Work, and Conclusions

The transformation rules presented in Chapter 3 provide a foundation for a Scheme program called vps which translates vlisp PreScheme into Pure PreScheme. vps was used to compile the vlisp Virtual Machine (vvm) [16], which is a byte-code interpreter. The vvm source is about 2200 lines of code and makes extensive use of the various features of the vps program. Indeed, the features provided by vps were mostly motivated by the vvm.

The original source for the vvm specified an iterative process because of a limitation of the Pure PreScheme compiler. The interpreter’s garbage collector is naturally written as a subroutine which returns to the point at which it was called. The interpreter was expressed as an iterative process by writing code which explicitly saved the information required by the garbage collector to restart the interpreter upon completion of garbage collection.

The source for the vvm was rewritten as a recursive process. This version more closely matched the algorithmic specification of the vvm and was accepted by the revised vps which translates vlisp PreScheme into PreScheme Assembly Language or, for debugging purposes, C. While the C code is unverified as is its compiler, practice has shown that it provides a useful gauge of run-time performance. Measurements showed the recursive version of the vvm was slightly faster than the iterative one.

John Ramsdell and Vipin Swarup spent a considerable amount of time studying the vvm and its translation into Pure PreScheme. Our subjective analysis concluded the optimizations performed were comparable to the ones performed by other optimizing transformational compilers. There were several times in which we thought the generated PreScheme was in error, only to realize later that vps had simply performed more optimizations than we expected which obscured the correctness of the translation!

While vps has been used to compile only one substantial program, it should perform well on most other vlisp PreScheme programs because its transformations are similar to those used by other successful compilers. There may be a few missing rules, such as some rules about arithmetic comparisons, but these rules can easily be added when identified. One note of caution: vps is not of production quality. It has yet to be subjected to any code review by peers or independent referees.

Future Work

There are three tasks which would improve our verified compiler vps. First, a verified assembler for PreScheme Assembly Language must be written. As mentioned before, its construction should be straightforward due to the work of Mitchell Wand and Dino Oliva [17, 11]. Second, confidence in the compiler could be increased by formally specifying the primitive operators and verifying their translation. Finally, the vlisp PreScheme language would be more useful as a systems programming language if facilities were provided to allow separate compilation. The first task is by far the most important one, and we plan to produce a verified assembler in FY94.

Conclusions

This paper defines the vlisp PreScheme language, a Scheme dialect useful for systems programming. The definition includes a formal denotational semantics.

The language can be compiled by transforming the program into a syntactically restricted subset of vlisp PreScheme, which then can be compiled using a syntax-directed compiler. This combination seems to produce reasonably good assembly code.

This paper gives a proof of the correctness of a set of transformation rules which perform the first translation and of a syntax-directed compiler which performs the second translation. The result is a verified compiler that translates vlisp PreScheme into PreScheme Assembly Language. One can build transformational compilers which use rules whose justification is based firmly in the formal semantics of the programming language being compiled along with syntax-direct compilers justified relative to those same formal semantics.

Appendix A

Operators in C

This is vps.h version 5.5 of 93/09/28. It is the header file which is included into C code generated from Vlisp PreScheme by the Vlisp PreScheme Front End.

#include <stdlib.h>
#include <stdio.h>
#include <limits.h>

typedef long Int; /* At least a 32-bit number. */ /* Make sure the format used */

                               /* in write int agrees. */
typedef int Chr;                /* The result type of getc. */
typedef int Bool;               /* The result type of ==. */
typedef char *String;           /* Arg type of open input file. */
typedef FILE *Port;             /* The arg type of getc. */
typedef unsigned char Byte;     /* The type of an element in */

/* a byte array. */

#define TRUE ((Bool) 1)
#define FALSE ((Bool) 0)
#if !defined __GNUC__/* When not using GCC, scratch */

#define inline /* inline directives. The */ #endif /* resulting code is ANSI C. */

A function is marked invariable if its use is side-effect free and its value does not depend on modifiable values.

static inline Bool
  less(Int n0, Int n1)          /* invariable */
{
  return n0 < n1;
}
static inline Bool
  leq(Int n0, Int n1)           /* invariable */
{
  return n0 <= n1;
}
static inline Bool
  eq(Int n0, Int n1)            /* invariable */
{
  return n0 == n1;
}
static inline Bool
  geq(Int n0, Int n1)           /* invariable */
{
  return n0 >= n1;
}
static inline Bool
  greater(Int n0, Int n1)       /* invariable */
{
  return n0 > n1;
}
static inline Int               /* abs or magnitude. */
  mag(Int n)                    /* invariable */
{
  return n >= 0 ? n : -n;
}

static inline Int
  plus(Int n0, Int n1)          /* invariable */
{
  return n0 + n1;
}
static inline Int
  difference(Int n0, Int n1)    /* invariable */
{
  return n0 - n1;
}
static inline Int
  times(Int n0, Int n1)         /* invariable */
{
  return n0 * n1;
}
static inline Int               /* Note: the result of / */
  quotient(Int n0, Int n1)      /* has unpredictable sign. */

{ /* invariable */

  Int n2 = mag(n0) / mag(n1);
  return (n0 >= 0) == (n1 >= 0) ? n2 : -n2;
}
static inline Int               /* Note: the result of % */
  remainder(Int n0, Int n1)     /* has unpredictable sign. */

{ /* invariable */

  Int n2 = mag(n0) % mag(n1);
  return n0 >= 0 ? n2 : -n2;
}
static inline Int
  ashl(Int n0, Int n1)          /* invariable */
{
  Int n2 = n1 >= 0 ? mag(n0) << n1 : mag(n0) >> -n1;
  return n0 >= 0 ? n2 : -n2;
}

static inline Int
  low_bits(Int n0, Int n1)      /* invariable */
{
  return n0 & ~(~0 << n1);
}
static inline Chr
  int2chr(Int n)                /* invariable */
{
  return (Chr) n;
}
static inline Int
  chr2int(Chr c)                /* invariable */
{
  return (Int) c;
}
static inline Bool
  is_char_eq(Chr c0, Chr c1)    /* invariable */
{
  return c0 == c1;
}
static inline Bool
  is_char_less(Chr c0, Chr c1)  /* invariable */
{
  return c0 < c1;
}
static Int *
  make_vector(Int n)            /* changes store */
{
  void *vec = malloc(sizeof(Int) * n);
  if (vec == NULL) {
    fprintf(stderr, "Could not allocate %ld words.\n", n);
    abort();
  }
  return (Int *) vec;
}

static inline Int
  vector_ref(Int *v, Int n)     /* side-effect free */
{
  return v[n];
}
static inline Int
  do_vector_set(Int *v, Int n, Int o) /* changes store */
{
  v[n] = o;

return 0; /* Result unspecified. */

}
static inline Int
  vector_byte_ref(Int *v, Int n) /* side-effect free */
{
  return ((Int) ((Byte *) v)[n]);
}
static inline Int
  do_vector_byte_set(Int *v, Int n, Int o) /* changes store */
{
  ((Byte *) v)[n] = (Byte) o;

return 0; /* Result unspecified. */

}
static inline Bool
  addr_less(Int *v0, Int *v1)   /* invariable */
{
  return v0 < v1;
}
static inline Bool
  addr_eq(Int *v0, Int *v1)     /* invariable */
{
  return v0 == v1;
}

static inline Int *
  addr_plus(Int *v, Int n)      /* invariable */
{
  return v + n;
}
static inline Int
  addr_difference(Int *v0, Int *v1) /* invariable */
{
  return v0 - v1;
}
static inline Int
  addr2int(Int *v)              /* invariable */
{
  return (Int) v;
}
static inline Int *
  int2addr(Int n)               /* invariable */
{
  return (Int *) n;
}
static inline String
  addr2string(Int *v)           /* side-effect free */
{
  return (String) v;
}
static inline Int *
  string2addr(String s)         /* side-effect free */
{
  return (Int *) s;
}

static inline Int
  port2int(Port p)              /* invariable */
{
  return (Int) p;
}
static inline Port
  int2port(Int n)               /* invariable */
{
  return (Port) n;
}
static Chr
  read_char(Port p)             /* changes store */
{
  if (feof(p)) return EOF;
  else return getc(p);
}
static Chr
  peek_char(Port p)             /* changes store */
{
  if (feof(p)) return EOF;
  else return ungetc(getc(p), p);
}
static inline Bool
  is_eof_object(Chr c)          /* invariable */
{
  return c == EOF;
}
static inline Int
  write_char(Chr c, Port p)     /* changes store */
{
  return fputc(c, p) == EOF ? -1 : 0;
}

static inline Int
  write_int(Int n, Port p)      /* changes store */
{
  return fprintf(p, "%ld",  n) == EOF ? -1 : 0;
}
static inline Int
  write(String s, Port p)       /* changes store */
{
  return fputs(s, p) == EOF ? -1 : 0;
}
static inline Int
  newline(Port p)               /* changes store */
{
  return write_char('\n', p);
}
static inline Int
  force_output(Port p)          /* changes store */
{
  return fflush(p);
}
static inline Bool
  is_null_port(Port p)          /* invariable */
{
  return p == NULL;
}
static inline Port
  open_input_file(String s)     /* changes store */
{
  return fopen(s, "r");
}

static inline Int
  close_input_port(Port p)      /* changes store */
{
  return fclose(p);
}
static inline Port
  open_output_file(String s)    /* changes store */
{
  return fopen(s, "w");
}
static inline Int
  close_output_port(Port p)     /* changes store */
{
  return fclose(p);
}
static inline Port
  current_input_port(void)      /* side-effect free */
{
  return stdin;
}
static inline Port
  current_output_port(void)     /* side-effect free */
{
  return stdout;
}
static Int
  read_image(Int *v, Int n, Port p) /* changes store */
{
  n = fread(v, sizeof(Int), n, p);
  if (ferror(p)) {
    fprintf(stderr, "Error in read_image.\n");
    abort(1);
  }
  return n;
}

static Int
write_image(Int *v, Int n, Port p) /* changes store */
{
n = fwrite(v, sizeof(Int), n, p);
if (ferror(p)) {
  fprintf(stderr, "Error in write_image.\n");
  abort(1);
}
return n;
}
#define bytes_per_word (sizeof(Int))
#define useful_bits_per_word (CHAR_BIT * sizeof(Int))
static inline Int               /* The type really is */
quit(Int n)                   /* ∀α, Int → α. */

{ /* changes store */

exit(n);
}
#define err(n, s) \
report_err((n), (s), __FILE__, __LINE__))
static Int
report_err(Int n, String s, char *f, int l) /* changes store */
{
(void) write(s, stderr);
(void) newline(stderr);
(void) fprintf(stderr,
               "Error detected in file %s on line %d.\n",
               f, l);
exit(n);
}

Bibliography

[1] H. P. Barendregt. The Lambda Calculus, Its Syntax and Semantics. North-Holland, Amsterdam, revised edition, 1984.

[2] J. D. Guttman, L. G. Monk, W. M. Farmer, J. D. Ramsdell, and V. Swarup. The vlisp byte-code compiler. Technical Report M92B092, The MITRE Corporation, 1992.

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

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

[5] Richard Kelsey and Jonathan Rees. Scheme48 progress report. Manuscript in preparation, 1992.

[6] Richard A. Kelsey. Realistic compilation by program transformation. In Conf. Rec. 16th Ann. ACM Symp. on Principles of Programming Languages. ACM, 1989.

[7] Richard A. Kelsey. PreScheme: a scheme dialect for systems programming. Submitted for publication, 1992.

[8] D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. ORBIT: An optimizing compiler for scheme. SIGPLAN Notices, 21:219– 233, 1986. Proceedings of the ’86 Symposium on Compiler Construction.

[9] Robin Milner. A theory of type polymorphism in programming. Journal of Computer and System Sciences, 17:348–375, 1978.

[10] Robin Milner, Mads Tofte, and Robert Harper. The Definition of Standard ML. The MIT Press, Cambridge, MA, 1990.

[11] Dino P. Oliva. Advice on structuring compiler back ends and proving them correct. Technical Report NU-CCS-93, Northeastern University College of Computer Science, June 1993.

[12] Dino P. Oliva and Mitchell Wand. A verified compiler for pure prescheme. Technical Report NU-CCS-92-5, Northeastern University College of Computer Science, February 1992.

[13] Laurence C. Paulson. ML for the Working Programmer. Cambridge University Press, Cambridge, Great Britain, 1991.

[14] J. D. Ramsdell, W. M. Farmer, J. D. Guttman, L. G. Monk, and V. Swarup. The vlisp PreScheme front end. Technical Report M92B098, The MITRE Corporation, 1992.

[15] Guy L. Steele. Rabbit: A compiler for Scheme. Technical Report 474, MIT AI Laboratory, 1978.

[16] V. Swarup, W. M. Farmer, J. D. Guttman, L. G. Monk, and J. D. Ramsdell. The vlisp byte-code interpreter. Technical Report M92B097, The MITRE Corporation, 1992.

[17] M. Wand and D. P. Oliva. Proving the correctness of storage representations. In Proceedings of the 1992 ACM Conference on Lisp and Functional Programming, pages 151–160, New York, 1992. ACM Press.