The VLISP PreScheme Front End

John D. Ramsdell  Willian M. Farmer
Joshua D. Guttman Leonard G. Monk Vipin Swarup

The MITRE Corporation^{1} M92B098 September 1992

1This work was supported by Rome Laboratories of the United States Air Force, contract No. F19628-89-C-0001. Authors’ address: The MITRE Corporation, 202 Burlington Road, Bedford MA, 01730-1420. \begin{matrix}c \\ ◯ \end{matrix}1992 The MITRE Corporation. Permission to copy without fee all or part of this material is granted provided that the copies are not made or distributed for direct commercial advantage, the MITRE copyright notice and the title of the publication and its date appear, and notice in given that copying is by permission of the MITRE Corporation.

Abstract

The Verified Programming Language Implementation project has developed a formally verified implementation of the Scheme programming language. This report documents the vlisp PreScheme language, used to program the vlisp Virtual Machine (interpreter). It contains detailed proofs that a set of transformations preserve the meanings of vlisp PreScheme programs.

Contents

1 Introduction 1

2 VLISP PreScheme 2 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 3 2.2 Standard Procedures . . . . . . . . . . . . . . . . . . . . . . . 3 2.3 Formal Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 6

2.3.1 Abstract Syntax . . . . . . . . . . . . . . . . . . . . . . 6 2.3.2 Domain Equations . . . . . . . . . . . . . . . . . . . . 7 2.3.3 Semantic Functions . . . . . . . . . . . . . . . . . . . . 8 2.3.4 Auxiliary Functions . . . . . . . . . . . . . . . . . . . . 10

2.4 Compiler Restrictions . . . . . . . . . . . . . . . . . . . . . . . 10

3 Macro-free PreScheme 11 3.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3.2 Semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12 3.3 Static Semantics . . . . . . . . . . . . . . . . . . . . . . . . . 12

4 Simple PreScheme 14

5 The Design 14

5.1 Transformation Rules . . . . . . . . . . . . . . . . . . . . . . . 15 5.1.1 Syntactic Predicates . . . . . . . . . . . . . . . . . . . 17 5.1.2 The List of Rules . . . . . . . . . . . . . . . . . . . . . 19

5.2 Usage of the Rules . . . . . . . . . . . . . . . . . . . . . . . . 24 5.3 Justification of the Rules . . . . . . . . . . . . . . . . . . . . . 25

5.3.1 if in an if’s Consequence . . . . . . . . . . . . . . . . 28 5.3.2 lambda Simplification . . . . . . . . . . . . . . . . . . . 29 5.3.3 β-substitution . . . . . . . . . . . . . . . . . . . . . . . 30 5.3.4 letrec Lifting . . . . . . . . . . . . . . . . . . . . . . 34 5.3.5 letrec Expression Merging . . . . . . . . . . . . . . . 34 5.3.6 letrec Simplification . . . . . . . . . . . . . . . . . . . 36 5.3.7 letrec Binding Merging . . . . . . . . . . . . . . . . . 36 5.3.8 Rotate Combinations . . . . . . . . . . . . . . . . . . . 39 5.3.9 Defined Constant Substitution . . . . . . . . . . . . . . 40

6 Results 40 7 Conclusion 41

A The C Header File vps.h 41

B The Facile PreScheme Compiler 51

B.1 Compilation . . . . . . . . . . . . . . . . . . . . . . . . . . . . 52 B.1.1 Additional Domain Equations . . . . . . . . . . . . . . 53 B.1.2 Compiler Semantic Functions . . . . . . . . . . . . . . 53 B.1.3 Machine Instruction Auxiliary Functions . . . . . . . . 55 B.1.4 Additional Auxiliary Functions . . . . . . . . . . . . . 56

B.2 Correctness . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56

List of Figures

1 Pre-defined Procedures . . . . . . . . . . . . . . . . . . . . . . 4 2 Case Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11 3 Typing Rules . . . . . . . . . . . . . . . . . . . . . . . . . . . 13 4 Defined Constant Substitution . . . . . . . . . . . . . . . . . . 23 5 Stack Layout . . . . . . . . . . . . . . . . . . . . . . . . . . . 52

1 Introduction

It might seem desirable to implement systems programming tasks in Scheme. Scheme’s expressivity, simplicity, and regularity draw programmers. Scheme implementations usually provide a highly interactive programming environment with dynamic linking and powerful debugging tools.

There is a problem with this use of Scheme. Scheme implementations provide an extensive run-time system which includes automatic storage reclamation, first class procedures, and many other advanced features. Most systems programming tasks cannot afford the overhead of this run-time system.

PreScheme is a restricted dialect of Scheme intended for systems programming. It was invented by Jonathan Rees and Richard Kelsey [6]. The language was defined so that programs can be executed using only a Clike run-time system. A compiler for this language will reject any program that requires run-time type checking and need 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.

The vlisp project has constructed a verified design of a Scheme system, and then implemented that design [2]. The design is based on Scheme48 [4], whose byte-code interpreter is written in PreScheme.

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 or macros, or compiler directives. The only other difference is 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 produces a new program by expanding most of vlisp PreScheme’s derived syntax. The second stage translates the macro-free program into an equivalent program by using meaning preserving 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 Mitch Wand. They are creating a verified compiler for Pure PreScheme [10]. A straightforward translation is all that is required to convert a Simple PreScheme program into a Pure PreScheme program. Note that the current version of the Pure PreScheme compiler allows only tail-recursive calls, that is, all calls are reguarded as goto’s which pass parameters and which never return.

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.

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 [6]. Furthermore, this compiler is essentially a transformational compiler [5].

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.

The contribution reported within 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.

2 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.

2.1 Syntax

The syntax of the vlisp PreScheme language is identical to the syntax of the language defined in the Scheme standard [3, 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 lambda expression, variables can also be defined using the syntax

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

When ⟨variable⟩ is 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.

2.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

       (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 1: Pre-defined Procedures

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 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

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.3 Formal Semantics

The formal semantics of vlisp PreScheme is presented in a form that very closely resembles Scheme’s semantics [3, Appendix A]. It uses the same mathematical conventions, and many of the standard’s definitions without repeating them here. I strongly suggested you have a copy of the standard in hand while 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. 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})

2.3.1 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. 2.3.2 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

2.3.3 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

Definition of K deliberately omitted.

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

E[[K]] = See [3, Appendix A] E[[I]] = See [3, Appendix A] E[[(E E∗)]] = See [3, 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 [3, Appendix A] E[[(if E E)]] = See [3, 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 all other identifiers to undefined. It maps no identifier to a location.

2.3.4 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.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: 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. The effect of providing a key which is not one of the selection criteria is undefined. This allows the omission of run-time range checks.

3 Macro-free PreScheme

Macro-free PreScheme (mfps) programs result from vlisp PreScheme programs by expanding all derived syntax except the case expression, identifying which variables refer to standard procedures, 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 N-ary standard procedures must be used at one fixed arity.

3.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)∗)

3.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.

3.3 Static Semantics

Macro-free PreScheme programs may be strongly typed. As in Standard ML [9], 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 3. When a type is unconstrained by the rules, the expression is assigned the integer type. ρ ⊢ 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 3: Typing Rules

4 Simple PreScheme

Simple PreScheme programs are syntactically restricted, strongly typed Macrofree 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)
| (set! I S) | (O S∗) | (case S C)
Cls ⟶ ((K) S)∗

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

Appendix B contains a compiler for a subset of Simple PreScheme. All Simple PreScheme programs are easily transformed into this subset.

5 The Design

There are five phases in the translation of vlisp PreScheme into Pure Pre-Scheme.

Parse: Expands usages of derived syntax by rules consistent with those presented in the Scheme standard. In addition, the program’s variables are renamed 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: Each reference to a vlisp PreScheme standard procedure is replaced by its code.

Apply transformation rules: Translates a Macro-free PreScheme program into a Simple PreScheme one using meaning preserving 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 [8]. The unifier is based on a published program by Laurence Paulson [11, p. 381].

Print: Translates the internal representation of a strongly typed Simple Pre-Scheme program into Pure PreScheme syntax.

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 preserving rules. The rules are meaning preserving in a sense to be made precise in Section 5.3.

The selection and application of rules is performed by a complex 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 only been introduced by bad rules. Therefore, the verification effort focused solely on the transformation rules.

5.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_{0}[ ] and C_{1}[ ] are contexts, then so is (if C_{0}[ ] C_{1}[ ]).

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

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.

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.

5.1.1 Syntactic Predicates Transformation rule applicability may be predicated on syntactic properties in addition to the matching of the rule’s pattern. A common predicate tests if a variable is free in an expression. The definition of three other predicates follow. Definition 4 An expression is side effect free if it returns a value without modifying the store.

• 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}) …). A side effect free expression can be eliminated when its value is ignored. Definition 5 An expression is invariable if it is side effect free and its value does not depend on modifiable variables.

• 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}) …). When an invariable expression is evaluated later during the execution of a program, its value remains the same. Definition 6 An expression is almost side effect free if it does not modify the store until its last action.

• 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.

5.1.2 The List of Rules

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

1. Simplification of some primitive expressions.

• 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)

• Associative operators are moved 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. Simplification of conditional expressions (if and case).

• Evaluate when 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 combinations in tests.

(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 begin’s in tests.

(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 if in an if’s test.

(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 if in an if’s consequence.

(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 and so 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 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. Rotate combinations.

(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 4: Defined Constant Substitution

15. Rotate begin’s.

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

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.

5.2 Usage of the Rules

The rules result in program transformations similar to those produced by other compilers [7, 5]. The rules for conditionals are the same, and the rules for β-reduction 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 [12]. 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 (compute-log-bytes-per-word x a)
       (if (<= x 1)
           a
           (compute-log-bytes-per-word (ashr x 1) (+ 1 a))))
     (define log-bytes-per-word
       (compute-log-bytes-per-word bytes-per-word 0))
     (if (not (= (ashl 1 log-bytes-per-word) bytes-per-word))
         (err 1 "Word size not a power of two"))

5.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 3. 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

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 meaning preserving 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 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 preserve 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 an if’s consequence 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.

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

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.

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}

5.3.1 if in an if’s Consequence 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})]]ρκσ

5.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.

5.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 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⟩⟨ϵ⟩)κσ.

5.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]))]]ρκσ

5.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}.

5.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}.

5.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 letrec’s 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}.

5.3.8 Rotate Combinations

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 first author was unable to write a vlisp PreScheme program with bottom denotation which is transformed by this rule into one which produces a non-bottom answer. Can you?

5.3.9 Defined Constant Substitution

Theorem 12 The rule shown in Figure 4 is meaning preserving.

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}]]ρκσ.

6 Results

The transformation rules provide a foundation for a Scheme program called vps which translates vlisp PreScheme into Pure PreScheme.^{2} vps has been used to translate the vlisp Virtual Machine (vvm) [13], 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.

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.

2For debugging purposes, vps can also translate vlisp PreScheme into C.

7 Conclusion

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 that perform the first translation, and Dino Oliva and Mitchell Wand [10] have produced a verified compiler which performs the second translation. The result is a verified compiler for vlisp PreScheme. One can build transformational compilers which use rules whose justification is based firmly in the formal semantics of the programming language being compiled.

Acknowledgements

John Ramsdell wrote this paper. 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. Vipin Swarup proofread the final version.

A The C Header File vps.h

This is vps.h version 4.1 of 92/19/13. 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
  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);
}

B The Facile PreScheme Compiler

Facile PreScheme programs are syntactically restricted, strongly typed Macrofree PreScheme programs. All Facile PreScheme programs are Simple Pre-Scheme 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

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

Figure 5: Stack Layout

Pgm ⟶ (define I)∗ E
Exp ⟶ (letrec (B) S)
Bnd ⟶ (I (lambda (I∗) S))∗
Smpl ⟶ K | I | (I I∗) | ((lambda (I∗) S) S∗)
| (begin S∗ S) | (if S S S) | (if #f #f)
| (set! I S) | (O I∗) | (case S C)
Cls ⟶ ((K) S)∗

There are further syntactic restrictions. Notice that only variables may be the elements of combinations and the arguments of primitive invocations. Each of these variables must be bound by a lambda expression. Furthermore, 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. See Figure 2 on page 11.

Facile PreScheme’s semantics are inherited from Macro-free PreScheme’s semantics.

B.1 Compilation

Facile PreScheme was designed to execute on an abstract machine which has only one stack for temporary storage. Both the local environment, temporary values, and the continuation are placed on the same stack. Facile Pre-Scheme’s syntactic restrictions on combinations and primitive invocations make this possible.

Figure 5 shows a potential layout for the stack. The stack grows rightward in the figure. The compiler translates a reference to a lambda bound variable into an offset used to reference the variable’s value on the stack relative to the frame pointer.

The compiler is presented as an alternate semantics for Facile PreScheme.

B.1.1 Additional Domain Equations

D_{c} = N + D compiler denoted values
γ ∈ U_{c} = Ide → D_{c} compiler environments
π ∈ Q = E → F expression instructions

B.1.2 Compiler Semantic Functions

CL : Exp → U_{c} → N → Q → F
CB : Bnd → Ide∗ → U → E∗ → E∗
CS : Smpl → U_{c} → N → Q → F
CC : Cls → U_{c} → N → Q → F ∗
CS∗ : Smpl∗ → U_{c} → N → F → F
CE : Exp → U → F
CD : Pgm → U → K → C
CP : Pgm → A

CL[[(lambda (I∗) S)]] =

λγνπ. CS[[S]]\begin{matrix}(extends_{c} γI∗ν) \\ (ν + #I∗) \\ (π = return → π, dispose #I∗π) \end{matrix}

CS[[K]] = λγνπ. literal(K[[K]])π

CS[[I]] = λγνπ. γI ∈ N → local(γI | N)π, global(γI | D)π

CS[[(I I∗)]] = λγνπ. π = return → call(γI | N)(map(λI. γI | N)I∗), makecont νπ(CS[[(I I∗)]]γν return)

CS[[((lambda (I∗) S) S∗)]] = λγνπ. reserve #I∗(CS∗[[S∗]]γ(ν + #I∗)(CL[[(lambda (I∗) S)]]γνπ))

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

CS[[(begin S S∗ S_{0})]] = λγνπ. CS[[S]]γν(ignore(CS[[(begin S∗ S_{0})]]γνπ))

CS[[(if S_{0} S_{1} S_{2})]] = λγνπ. CS[[S_{0}]]γν(jumpfalse(CS[[S_{1}]]γνπ)(CS[[S_{2}]]γνπ))

CS[[(if #f #f)]] = λγνπ. literal unspecified π CS[[(set! I S)]] = λγνπ. CS[[S]]γν(setglobal(γI | D)π) CS[[(+ I_{0} I_{1})]] = λγνπ. add(γI_{0} | N)(γI_{1} | N)π CS[[(case S C)]] = λγνπ. CS[[S]]γν(dispatch(CC[[C]]γνπ)) CC[[ ]] = λγνπ. ⟨⟩ CC[[((K) S) C]] = λγνπ. ⟨CS[[S]]γνπ⟩ § CC[[C]]γνπ CS∗[[ ]] = λγνϕ. ϕ CS∗[[S S∗]] =

λγνϕ. CS[[S]]γν(setlocal(ν − #S∗ − 1)(CS∗[[S∗]]γνϕ)) CB[[ ]] = λI∗ρϵ∗. ⟨⟩ CB[[(I (lambda (I∗) S)) B]] =

λI∗_{0}ρϵ∗.

⟨CL[[(lambda (I∗) S)]](λδ. δ in D_{c} ∘ extends ρI∗_{0}ϵ∗)0 return inE⟩

§ B[[B]]I∗_{0}ρϵ∗

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

λρ. CS[[S]]\begin{matrix}(λδ. δ in D_{c} ∘ extends ρ(I[[B]])(fix(CB[[B]](I[[B]])ρ))) \\ 0 \\ return \end{matrix}

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

λρκσ. CD[[P]](ρ[(new σ) in D/I])κ(update(new σ) undefined σ) CP[[P]] = CD[[P]]ρ_{0}κ_{0}σ_{0} B.1.3 Machine Instruction Auxiliary Functions

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

local : N → Q → F local = λνπ. λϵ∗κ. π(stackref ϵ∗ν)ϵ∗κ

setlocal : N → F → Q setlocal = λνϕ. λϵϵ∗κ. ϕ(takefirst ϵ∗ν § ⟨ϵ⟩ § dropfirst ϵ∗(ν + 1))κ

global : D → Q → F global = λδπ. λϵ∗κ. hold δλϵ. πϵϵ∗κ

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

ignore : F → Q ignore = λϕ. λϵϵ∗κ. ϕϵ∗κ

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

dispatch : F ∗ → Q dispatch = λϕ∗. λϵϵ∗κ. (ϕ∗ ↓ (1 + ϵ | R))ϵ∗κ

call : N → N∗ → F call = λνν∗. λϵ∗κ. applicate(stackref ϵ∗ν)(map(stackref ϵ∗)ν∗)κ

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

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

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

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

add : N → N → Q → F add = λν_{0}ν_{1}π. λϵ∗κ. π(stackref ϵ∗ν_{0} | R + stackref ϵ∗ν_{1} | R)ϵ∗κ B.1.4 Additional Auxiliary Functions

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

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

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

extends_{c} : D_{c} → Ide∗ → N → D_{c} extends_{c} =

λγI∗ν. #I∗ = 0 → γ, extends_{c}(λI. I = I∗ ↓ 1 → ν in D_{c}, γI)(I∗ † 1)(ν + 1)

B.2 Correctness

The correctness of the Facile PreScheme compiler has not yet been demonstrated. It would involve proving CP[[P]] = P[[P]] by appealing to the following conjectures. The correctness of the conjectures depends on the fact that Facile PreScheme programs are strongly typed.

Definition 11 compose = λγϵ∗I. γI ∈ N → stackref ϵ∗(γI | N) in D, γI | D

Conjecture 1 Assume compose γϵ∗ = compose γ(ϵ∗ § ϵ∗_{0}).

CS[[S]]γ#ϵ∗πϵ∗κ = E[[S]](compose γϵ∗)λϵ. πϵϵ∗κ

Conjecture 2 Assume compose γϵ∗ = compose γ(ϵ∗ § ϵ∗_{0}).

CS∗[[S∗]]γ(#ϵ∗ + #S∗)ϕ(ϵ∗ § unspecs #S∗)κ

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

Conjecture 3 Assume #ϵ∗ ≥ #I∗ and let ν = #ϵ∗ − #I∗.

compose γ(takefirst ϵ∗ν) = compose γ((takefirst ϵ∗ν) § ϵ∗_{0})

implies

CL[[(lambda (I∗) S)]]γνπϵ∗κ = applicate (L[[(lambda (I∗) S)]](compose γ(takefirst ϵ∗ν))) (dropfirst ϵ∗ν) λϵ. πϵ(takefirst ϵ∗ν)κ The previous three conjectures could be proved using simultaneous structural induction on simple expressions.

Conjecture 4

CL[[(lambda (I∗) S)]](λδ. δ in D_{c} ∘ ρ)0 return inE = L[[(lambda (I∗) S)]]ρ

Conjecture 5 BP[[B]] = B[[B]]

Conjecture 6 CE[[E]]ρ⟨⟩κσ = E[[E]]ρκσ

Conjecture 7 CD[[P]] = D[[P]]

Conjecture 8 CP[[P]] = P[[P]]

References

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

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

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

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

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

[6] Richard A. Kelsey. PreScheme: A Scheme dialect for systems programming. Submitted for publication, 1992.

[7] D. Kranz, R. Kelsey, J. Rees, P. Hudak, J. Philbin, and N. Adams. orbit: An optimizing compiler for Scheme. In sigplan Notices, volume 21, pages 219–233, 1986. Proceedings of the ’86 Symposium on Compiler Construction.

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

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

[10] 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.

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

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

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