OPERATIONALLY-BASED MODELS

OF HIGHER-ORDER IMPERATIVE PROGRAMMING LANGUAGES

A Thesis

Presented to the Faculty of the Graduate School

of the College of Computer Science

of Northeastern University

in Partial Fulfillment of the Requirements for the Degree of Doctor of Philosophy

by

Gregory T. Sullivan ^{1} College of Computer Science

Northeastern University 360 Huntington Avenue, 161CN

Boston, MA 02115, USA

gregs@ccs.neu.edu

http://www.ccs.neu.edu/home/gregs/

August 1997

\begin{matrix}c \\ ◯ \end{matrix} Gregory T. Sullivan ^{2} College of Computer Science

Northeastern University 360 Huntington Avenue, 161CN

Boston, MA 02115, USA

gregs@ccs.neu.edu

http://www.ccs.neu.edu/home/gregs/, 1997

ALL RIGHTS RESERVED

Abstract

We present a typed metalanguage with support for higher-order functions, a global store, and input-output. An operational, small-step semantics is given for the metalanguage, with the operations on the global store and for I/O restricted to continuation passing style. We develop, based solely on the operational semantics, a theory of term equivalence in the metalanguage, notably an Extensionality Theorem (also known as a context lemma). By considering equivalence classes of operationally equivalent metalanguage terms, we construct a term model which we then use as the target for denotational semantics of imperative programming languages. As an in-depth application of our methods, we prove correct a number of source-to-source transformations used in a compiler for Scheme. iv

Acknowledgements

I would like to thank Mitch Wand both for his prodigious knowledge and for his endless patience in attempting to impart some small portion of it to me. While Mitch provided the academic enlightenment, my wonderful wife Ann gave me unflagging support, encouragement, and love. For all these things and more, I am eternally grateful. For providing joyous distraction, I thank my daughter Melissa, and for providing a powerful motivation to finish, I thank my son Jay, who was born the day after my defense. I am grateful to my committee of, in addition to Mitch Wand: Carolyn Talcott, Will Clinger, and Karl Lieberherr. Their careful reading and thoughtful comments on earlier drafts have enormously improved both the accuracy and the readability of this thesis. Thanks to all those that made my time at Northeastern as fruitful and enjoyable as it was, especially: Linda Seiter, Mike Cleary, Dave Gladstein, Paul Steckler, Nacho Silva-Lepe, Walter Hürsch, Ian Holland, Remy Évard, Deans Finkelstein and Chan, Richard Kelsey and Luc Longpré. Thanks also to fellow Boston semantics seminarians Bob Muller and Allyn Dimock. And thanks to my family: Mom, Tom, Barb, and Beez, for humoring and supporting me throughout my life, and to my Dad, whose spirit still guides me. vi

Contents

Abstract . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . iii Acknowledgements . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . v List of Definitions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 2

1 Introduction 3 1.1 Functional Programming Languages . . . . . . . . . . . . . . . . . . . . . . 3 1.2 Imperative Features . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.3 Contribution . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 4 1.4 Related Research . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 5

1.4.1 On Reading the Proofs . . . . . . . . . . . . . . . . . . . . . . . . . . 9 1.4.2 Some History . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 11

1.5 Outline . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 12

2 Term Model 13 2.1 Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2 Semantics of the Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . 17 2.3 State Equivalence – Bisimulation . . . . . . . . . . . . . . . . . . . . . . . . 20

2.3.1 Bisimulation in a Deterministic Setting . . . . . . . . . . . . . . . . 22 2.4 Term Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25

2.4.1 Contextual Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 25 2.4.2 Extensional Equivalence . . . . . . . . . . . . . . . . . . . . . . . . . 26

2.5 Theory of the Metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.5.1 Simulations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 2.5.2 Properties of the Extended PCF Functional Sublanguage . . . . . . 33 2.5.3 Subject Reduction for Metalanguage . . . . . . . . . . . . . . . . . . 35 2.5.4 Simulation up to Location Renaming . . . . . . . . . . . . . . . . . . 35 2.5.5 PCF Reduction Preserves Simulation (Full Beta) . . . . . . . . . . . 37 2.5.6 Completeness of Leftmost Reduction . . . . . . . . . . . . . . . . . . 41 2.5.7 Substitution Lemma for PCF . . . . . . . . . . . . . . . . . . . . . . 43 2.5.8 Contextual Equivalence with Empty Stores . . . . . . . . . . . . . . 44

2.6 Substitution Lemmas for the Metalanguage . . . . . . . . . . . . . . . . . . 45 2.7 Precongruence of the Extensional Preorder . . . . . . . . . . . . . . . . . . 52 2.8 The Extensionality Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . 54

2.8.1 Extensional Equivalence at Sum Types . . . . . . . . . . . . . . . . . 55

3 Examples from the Literature 57

3.1 Some Meyer-Sieber Examples . . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.1.1 Meyer-Sieber Example 1 . . . . . . . . . . . . . . . . . . . . . . . . . 57 3.1.2 Meyer-Sieber Example 4 . . . . . . . . . . . . . . . . . . . . . . . . . 59

3.2 Examples from Ian Stark . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62

3.2.1 Count-up, Count-down . . . . . . . . . . . . . . . . . . . . . . . . . . 62

4 Twobit Optimizations 65 4.1 Motivation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 66 4.2 Overview . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 67 4.3 Translation from Scheme to Metalanguage . . . . . . . . . . . . . . . . . . . 68 4.4 Equivalence of Scheme Expressions . . . . . . . . . . . . . . . . . . . . . . . 72 4.5 Why Types are Needed in Target Metalanguage . . . . . . . . . . . . . . . . 73

5 Assignment Elimination 77 5.1 Intermediate Language Scheme_{cell} . . . . . . . . . . . . . . . . . . . . . . . 77 5.2 The Assignment Elimination Transformation . . . . . . . . . . . . . . . . . 81 5.3 Correctness of Assignment Elimination . . . . . . . . . . . . . . . . . . . . . 83

5.3.1 The Assignment Elimination Simulation Relation . . . . . . . . . . . 90

6 Lambda Lifting 101 6.1 The Lambda-Lifting Transformation . . . . . . . . . . . . . . . . . . . . . . 102 6.2 Correctness of Lambda Lifting . . . . . . . . . . . . . . . . . . . . . . . . . 107

7 Conclusions and Open Problems 123 7.1 Open Problems – Future Work . . . . . . . . . . . . . . . . . . . . . . . . . 123

List of Definitions

→_{pcf} – PCF reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 18 →_{sto} – store reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 locs(M) – locations in a term M . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19

→^{α}_{io} – I/O reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

[−]_{bisim} – bisimulation generator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .20 [−]_{sim} – simulation generator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 21 ≲_{∀C} – contextual preorder . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 ≅ – contextual equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 T_{τ} [−]:o – type contexts . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .27 ≅_{o}^{•} – extensional equivalence for closed terms at base type . . . . . . . . . . . . . . . . . . . . . . . . . . . . 27 ≅_{ext}^{•} – extensional equivalence, complex types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ≲_{o}^{•} – extensional preorder, base types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .28 ≲_{ext}^{•} – extensional preorder, complex types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 28 ≅_{ext} – extensional equivalence, open terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .29 ≲_{ext} – extensional preorder on open terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 [−]_{ext} – extensional simulation generator . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .30 simulation up to . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32 →_{left,pcf}^{∗} – leftmost PCF reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .34 α_{loc} – equal up to location renaming . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .36 =_{pcf} term – PCF equality between terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 =_{pcf} state – PCF equality between states . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .38 →_{left,sto}^{∗} – leftmost store reduction . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 41 [[−]]_{scm} – translation from Scheme to metalanguage . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 ≅_{∀C}^{scm} – operational equivalence for Scheme . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .72 ≅_{scm} – simplified Scheme equivalence . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .72 [[−]]_{cell} – Schemecell to metalanguage translation . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .80 AE – Assignment Elimination . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 82 L_{i}, R_{i} macros . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

⇝^{AE}_{V} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 87

⇝^{AE}_{V |Z} for metalanguage terms) . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

⇝^{AE}_{V |Z} for stores . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 90

Lambda Liftable . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 104 LL – Lambda Lifting . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . .106 LL_{body} . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 106

⇝^{LL_{body}} on terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 114

Chapter 1

Introduction

The following sections give a brief overview of the important concepts mentioned in the thesis abstract. We try to position both the problems we address, and also the methods we use, within the broader sphere of programming language research.

1.1 Functional Programming Languages

The unifying feature of programming languages described as “functional” is that functions are first-class entities: that is, functions may be passed as arguments to other functions and associated with variables. Another term for describing such programming languages is “higher-order.” There seems little question that making functions first class adds power and expressiveness to a programming language. This extra functionality and abstraction also make the efficient implementation of functional programming languages more challenging. The goal of having well-performing implementations of functional programming languages has spawned an active area of research in analysis and compilation of functional programs. An important aspect of functional programming languages is that they are amenable to formal analysis. The abstract, functional nature of these languages allows for the development of formal semantics and techniques and tools to reason about programs written in the language. Applications of these techniques include proving the correctness of source-to-source transformations (optimizations), compilers, garbage collectors, and sophisticated analyses, such as data and control flow analyses, which provide data to the other tools.

1.2 Imperative Features

The term “imperative” refers both to a set of programming language features, notably assignment and I/O, and also to a style of programming. Typical programs written in imperative programming languages such as Pascal or C have a function consisting of a sequence of statements, many of which assign values to variables, and finishing with a statement to return the value of the function. Another typically imperative feature, related to the notion of assignment, is that of a global store, or heap, and operations on it. The “functional” languages which have enjoyed the most popularity – Scheme, other Lisp dialects, ML – have imperative features, and it is rare to find a large program in one of these languages that does not make use of some “impure” language features. From the imperative camp, object-oriented languages are evolving more high-level, abstract features reminiscent of the functional paradigm. The relatively new object-oriented programming language Java features garbage collection, which is a hallmark of functional languages.

1.3 Contribution

The work presented in this thesis is of interest for both its theoretical and its practical content. We present a metalanguage, its formal syntax and semantics, and a model based on the operational semantics. The language and theory include the following features:

• higher-order functions,

• I/O operators,

• a global store (heap), and side-effecting operators (assignment), • recursive types (as well as base, process, function, sum, and product types),

• possibly-infinite meaningful behavior,

• an Extensionality Theorem for the metalanguage,

• coinduction principles for reasoning both about possibly infinite types and about possibly non-terminating programs.

The noteworthy aspect of the preceding list is that we are able to combine many appealing but typically problematic features into a language that also supports powerful reasoning principles such as extensionality and coinduction. It is also notable that the entire theory is developed operationally, thus requiring a relatively small set of mathematical and logical concepts to understand. After developing the syntax, semantics, and theory of the metalanguage, we then demonstrate the application of the theory to a number of examples drawn both from the literature and also from an actual compiler for the Scheme programming language. These applications include the first known proof of correctness of assignment elimination, an important transformation for Scheme compilers. The examples presented demonstrate that the framework we have set up is reasonable for application to actual optimizing compilers for modern higher-order functional languages with imperative features.

1.4 Related Research

There has been extensive research into issues related to imperative features of programming languages – particularly those having to do with assignment and side-effects. One line of research has explored stack-based imperative languages such as Algol. Reynolds’ “Essence of Algol” [Rey81] is similar syntactically to the metalanguages on which our own research focuses. The stack discipline of Algol has spawned much research, notably [Rey83, MS88, OT95]. The research presented in this thesis does not address stack discipline. The paper by Meyer and Sieber, [MS88], has been influential not only for its contribution to denotational semantics for Algol-like languages, but also for its presentation of a suite of “problematic” code fragments, referred to hereafter as the “Meyer-Sieber examples,” which have been used as examples in numerous later papers by other authors. Rather than starting with imperative languages, another line of research has been investigating adding store operations to functional languages. One approach to “cleanly” adding stores to functional languages has been to treat the store as a finite function and (implicitly) pass the store from function to function, exemplified by [Wad92, PJW93]. In [RV95], the purity of the functional sublanguage is preserved by saving the state before any side-effecting subprogram is executed, and restoring the state afterwards. The Imperative Lambda Calculus (ILC) presented in [SRI91] uses the type system to restrict interaction between pure functional and imperative program phrases. Similar to the metalanguages presented in this thesis, the imperative operations operate in continuation passing style (CPS). A few researchers have identified the concept of “names” as central to reasoning about assignment, though with widely varying results. Odersky [Ode94] writes:

In a sense, names are the greatest common denominator of all programming languages that are not purely functional.

The λν calculus presented in [Ode94] is a purely syntactic, conservative extension of the (untyped) λ-calculus [Bar81]. The new syntactic elements, names, have dynamic scope and can be compared for equality. The nu-calculus of Pitts and Stark [PS93] takes a similar approach, extending the (simply typed) λ-calculus with names and a test for name equality. The operational semantics of the nu-calculus, unlike that of the λν calculus, allows names to escape the local scope in which they were declared. The difference between these two “calculi of names” is demonstrated by their different behavior on the term νn.n. Odersky’s λν calculus takes no steps on the term, whereas in the nu-calculus of Pitts and Stark, the term allocates a fresh name and returns it. The nu-calculus semantics, where the ν constructor has “run-time” reduction behavior, is closer to the semantics for our metalanguage, and has more of the flavor of memory allocation operators in actual programming languages. Pitts and Stark show that the nu-calculus, even without a global store or mutation, is not extensional – terms that give the same result in all applicative contexts may be differentiated by non-applicative contexts. In [RP95], Ritter and Pitts describe a translation between Standard ML and a λ-calculus with reference types. They use Howe’s method [How96] to show their translation fully abstract. Our metalanguage also has reference types. Research by Talcott et al., especially [HMST95, MT91] overlaps quite a bit with our own. Like us, they use only operational semantics to develop a robust theory of a language with side-effects and a global store. Most differences between our research and theirs stem from different objectives: Talcott et al. study a sort of “minimal imperative language” which reflects the call-by-value, non-extensional nature of languages such as Scheme [IEE91] or ML [MTH89], whereas we have designed our metalanguage as the target of a translation from “real” programming languages and as the basis for a term model. As in Felleisen et al. [FH92], the language presented by Talcott et al. uses a syntactic representation of state, and syntactic manipulations of the store and store operations suffuse both the semantics and the proofs. Our metalanguage specifies stores as finite functions with no particular syntactic representation. An important theorem in Talcott et al.’s work is their ciu theorem, which states that terms are equivalent in all reduction contexts, à la [FF86], iff they are contextually equivalent (equivalent in all contexts). Their ciu theorem plays the same fundamental role in developing a theory for their language as does our Extensionality Theorem in developing the theory for our metalanguage. The contexts required by our Extensionality Theorem are somewhat more simple, but those differences from Talcott et al.’s ciu theorem are the result of the languages in question being designed for different purposes. The language presented in Talcott et al. is untyped and reduction is call-by-value, whereas our metalanguage has types and and supports full β-reasoning. In [HMST95], Honsell, Mason, Smith, and Talcott extend their results to a logic with which they verify the Meyer-Sieber examples, which we also prove using our setup. The mathematical and logical tools used in this thesis draw from many sources. Observational or contextual equivalence for programming languages was introduced by [Plo77], adapting the work of Morris [Mor68] for the λ-calculus. Also in [Plo77], Plotkin gives the syntax and typing rules of PCF, which our metalanguage extends. Operationallybased term models were introduced in [TW96], for the (untyped) λ-calculus with I/O (but no heap). Our Extensionality Theorem corresponds to what is often called a context lemma. A wellknown example of a context lemma is Milner’s context lemma for PCF and other typed lambda calculi in [Mil77]. Milner’s context lemma for PCF was proven operationally. Generalizations of Milner’s results are discussed in [JM91]. Bisimulation was introduced by [HM85]. In an untyped setting, the Lazy Lambda-Calculus paper by Abramsky [Abr90] presents a context lemma as well as defining the notion of applicative bisimulation. Abramsky’s work, while ground breaking, requires a strong background in domain theory to follow adequately, and his observables are very different from ours. See also [EHR91] and [Plo75]. One standard approach to proving that applicative equivalence coincides with contextual equivalence is to show first that applicative equivalence is a congruence – that is, closed under the term constructors of the language. Techniques for proving the congruence of bisimulation relations appear in [How89] and are further developed in [How96] and [How95]. We do not directly use Howe’s method for proving congruence, but his work has been very influential in this area of research. Andrew Pitts [Pit99] and his colleagues have done much to advance the use of techniques such as bisimulation and coinduction to develop theories based on operational semantics. In [Gor94b], Gordon investigates another typically imperative feature, I/O, using the same core techniques, such as bisimulation and coinduction, as we do. These techniques are generalized and presented more tutorially in [Gor95]. The languages explored by Gordon include recursive types in addition to I/O. The general idea of a relation preserved under computation recurs often in the literature. It was used to prove program equivalence in [MT91, WO92, ORW95]; [Sta94] uses a similar notion extended to become a logical relation. Many of the optimizations we prove correct later in the thesis are from Clinger and Hansen’s “Twobit” Scheme compiler and are discussed in [CH94]. A good introduction to the implementation of functional programming languages can be found in [PJ87], although the languages discussed there do not support side-effects. Assignment elimination was introduced in the Orbit compiler [KKR^{+}86] and used in [KH89, CH94]. It was omitted from [GSR95] because the authors were unable to prove its correctness [Ram96].

1.4.1 On Reading the Proofs

The proofs are presented in a stylized manner which takes some getting used to. We use the pf style provided by Lesley Lamport and discussed in [Lam93]. Suppose that in order to prove a proposition one needs three subgoals to be proven first. The proof structure would be:

1. first subgoal

2. second subgoal

3. third subgoal

Q.E.D. use first three subgoals to finish

The proofs of each subgoal might involve sequences of steps also. Suppose that two steps are needed to prove the first subgoal. Our proof structure then looks like:

1. first subgoal 1.1. first step in subproof 1.2. second step in subproof

Q.E.D. tie up proof of first subgoal 2. second subgoal 3. third subgoal Q.E.D.

In general, a proof step numbered x.y.z. labels the zth subgoal in the proof of the yth subgoal of the proof of the xth step in the proof of the top-level proposition. We use a more compact numbering scheme, with proof steps labelled, for example, ⟨5⟩2. A step labelled ⟨x⟩y. presents the statement of the yth step in the proof of a subgoal nested x layers deep. If our proof has the following structure:

1. first subgoal 1.1. first step in subproof 1.2. second step in subproof

1.2.1. first step in subsubproof 1.2.2. second step in subsubproof

1.2.2.1. first step in subsubsubproof Q.E.D.

1.2.3. third step in subsubproof Q.E.D.

1.3. third step in subproof 1.3.1. first step in subsubproof Q.E.D.

Q.E.D.

2. second subgoal 3. third subgoal Q.E.D.

then the compacted labels look like the following:

⟨1⟩1. first subgoal ⟨2⟩1. first step in subproof ⟨2⟩2. second step in subproof

⟨3⟩1. first step in subsubproof ⟨3⟩2. second step in subsubproof

⟨4⟩1. first step in subsubsubproof Q.E.D.

⟨3⟩3. third step in subsubproof Q.E.D.

⟨2⟩3. third step in subproof ⟨3⟩1. first step in subsubproof Q.E.D.

Q.E.D. ⟨1⟩2. second subgoal ⟨1⟩3. third subgoal Q.E.D.

Thus the proof step labels become shorter, but they are no longer unique. This loss of uniqueness is acceptable, because the subproof steps can logically never be used outside their “scope.” One further note on the labels in the pf style. While the reader may be used to the string Q.E.D. delineating the end of the proof, in the pf style, Q.E.D. labels the final subgoal of a proof, which may in turn involve a sub-proof which ties together any preceding steps in order to entail the current (sub)goal.

1.4.2 Some History

Originally, we proved substitution and context lemmas for an untyped version of the metalanguage. This, however, was not sufficient to prove equivalences for a source language such as Scheme. Adding the types to the metalanguage, and thence to the translations from Scheme, restricted the possible initial continuations enough to get us the desired equivalences. Section 4.5 works out a simple example of a pair of terms which are equivalent under a typed translation but not under an untyped one. Also, some early attempts tried making location constants related if they referenced related terms in the store (rather than requiring simple equality as we currently do). This added too much generality to the setup, and we were not able to prove, for example, a decent substitution lemma.

1.5 Outline

Chapter 2 presents the syntax for our metalanguage and its operational semantics. A term model is then developed, and various reasoning principles are derived – notably an extensionality theorem. Chapter 3 uses the theory of the metalanguage to prove a number of equivalences from the literature. Chapter 4 introduces a translation from the programming language Scheme to our metalanguage. Chapter 5 defines and then proves correct the assignment elimination optimization used in many Scheme compilers. Chapter 6 defines and proves correct the lambda lifting transformation, used in compilers for Scheme and other functional languages. We conclude in Chapter 7 with a discussion of open problems and future work.

An Operationally-Based Term

Model

We present the syntax and operational semantics of a typed metalanguage. The metalanguage extends the type system of PCF by adding recursive, reference, sum and product types and extends the operations of PCF by adding I/O and store operators. As in PCF, the rules for evaluation of terms are lazy (as opposed to call-by-value). We turn the operational semantics of the metalanguage into a term model for a typed lambda calculus by considering equivalence classes of terms with the same observable behavior. The observable behavior we consider is interaction via the I/O operators in the metalanguage. Finally, we prove a number of useful properties of the metalanguage. In particular, we show that the metalanguage is extensional: in order to prove two terms are contextually equivalent, one need only consider a restricted set of “extensional” contexts. We are able to add imperative operations to PCF while maintaining a nice operational theory by restricting the evaluation of the I/O and store operators to leftmost-outermost position. The I/O and store operators are in continuation passing style (CPS), and therefore the effects of those operators can only be passed along to their continuations.

2.1 Syntax

The types in the metalanguage, ranged over by τ, are potentially infinite trees which respect the following structure:

o ::= unit | bool | int | ref (τ) | pr τ ::= o | τ→τ | τ+τ | τ×τ

The base types o include int for integers, bool for booleans, ref (τ) for locations with contents of type τ, and unit for the singleton type. Type pr is for processes, which may do I/O. We allow infinite types, so we will need to define operations on types coinductively instead of inductively. We write τ^{∗} for the infinite type

unit + (τ × (unit + (τ × …)))

of lists of elements of type τ. The syntax of our metalanguage is given by the following grammar:

M ::= x | n | c | l^{τ} | λx:τ.M | MM

with x ranging over a countably infinite set of variables, Vars, and l ranging over a countably infinite set of location constants, Locs. Locations l^{τ} are annotated with types and are assigned type ref (τ). The types of the constants c of the metalanguage are given in Figure 1. A substitution σ is a finite map from variables to metalanguage terms. If [x ↦ M] ∈ σ, then applying the substitution to a term N, denoted Nσ, does any α-renaming necessary to avoid capture of free variables in M by binders (λ-expressions) in N. A typing judgement Γ ⊢ M:τ is a triple consisting of a type environment Γ, a metalanguage term M, and a type τ. Type environments map variables to types. The judgement Γ ⊢ M:τ can be read as stating that type environment Γ proves that term M has type τ if every

∀ types α, β, γ, τ,
pred :int→int, succ :int→int,  predecessor and successor
true :bool, false :bool,  boolean constants
if^{τ}:bool→τ→τ→τ,  conditional
zero? :int→bool,  true if int is zero
Y^{τ} :(τ→τ)→τ,  fixed point combinator
pair_{α,β}:α→β→(α×β)  pair constructor
π_{1}_{α,β}:(α×β)→α  first projection
π_{2}_{α,β}:(α×β)→β  second projection
1:unit  single element of unit type
inl_{α,β}:α→(α+β)  left injection
inr_{α,β}:β→(α+β)  right injection
case_{α,β}^{γ}:(α+β)→(α→γ)→(β→γ)→γ  sum unboxing
write :int→pr→pr,  write an integer to stdout
read :(int→pr)→pr,  read integer from stdin
stop :pr, stopped :pr,  halt
new^{τ}:τ→(ref (τ)→pr)→pr,  get fresh loc, initialize to 1st arg
deref^{τ}:ref (τ)→(τ→pr)→pr,  dereference a location
update^{τ}:ref (τ)→τ→pr→pr,  update a location
eq?_{loc}^{τ}:ref (τ)→ref (τ)→bool  compare locations for equality

Figure 1: Metalanguage Constants

Γ ⊢ x:Γ(x)  Γ ⊢ n:int  Γ ⊢ l^{τ}:ref (τ)

Γ ⊢ c:τ where c:τ from Figure 1

\frac{Γ ⊢ M:τ′→τ, Γ ⊢ N:τ′}{Γ ⊢ MN:τ}

\frac{Γ, x:τ′ ⊢ M:τ}{Γ ⊢ (λx:τ′.M):τ′→τ}

Figure 2: Typing Rules

free variable x ∈ fv(M) is assigned type Γ(x). If Γ ⊢ M:τ, then a closing substitution σ maps the free variables x_{i} of M to closed terms P_{i} respecting the type environment Γ – i.e. if Γ(x_{i}) = τ_{i}, then ∅ ⊢ P_{i}:τ_{i}. Thus a closing substitution σ instantiates all free variables: fv(Mσ) = ∅. For closed well-typed terms, we often write M:τ rather than ∅ ⊢ M:τ. The rules for deriving type judgements are standard, and are given in Figure 2 for completeness. Programs are closed terms of type pr. Contexts are generated by the same grammar as terms, but with an additional production for a typed hole:

C ::= [−_{τ}] | x | n | c | l^{τ} | λx:τ.C | CC

A context C[−_{τ}] respects a type assignment Γ if for every variable binding x:τ′ in effect at the hole in C, Γ(x) = τ′. A state, denoted ⟨⟨M ; Σ⟩⟩, is a term-store pair where M is a program (a closed term of type pr) and store Σ is a finite map from locations to terms. A store must be well-formed in that all locations l^{τ} in the domain of Σ must map to closed terms of type τ.

2.2 Semantics of the Metalanguage

We define the operational semantics of the metalanguage in three steps. The reduction semantics of the PCF fragment of the metalanguage defines a relation →_{pcf} between closed well-typed terms. The reduction relation →_{sto} is defined on states, includes PCF reduction within term components, and gives transition rules for states with store operations in head position. Finally, we define a labeled transition relation, →^{α}_{io}, between states which reduce under →_{sto}^{∗} to states headed by I/O operations. Figure 3 presents the standard transition rules for the PCF fragment of the metalanguage, augmented with operations on sums and products. PCF reduction is only defined on welltyped terms – thus we omit the type annotations on the operators and locations. Substitution in the β rule is careful not to capture free variables in N, as usual. We define all of the redexes using the →_{1} relation, and then use one rule of inference to define →_{pcf} as reduction in any context. Some presentations of PCF (e.g. [Gun92]) do not allow reduction under a λ or within the operand of an application. We choose to allow reduction in all contexts, often referred to as “full β,” and we will later appeal to the Church-Rosser property of PCF to prove a standardization theorem. This choice is consistent with our goal of using the metalanguage to reason about other programs – not as an example programming language itself. Note that reduction is lazy – operands do not need to reduce to a value before an operator transition is taken. Recursion is supported by the Y operator. As a simple example of its use, following is the definition of a plus function:

plus =^{def} (Y^{int→int→int}(λP:int→int→int.λx:int.λy:int.

if(zero? y)x(P (succ x) (pred y)))

The term plus has type int→int→int, as it should. Figure 4 defines the transition relation →_{sto} between states. The first rule incorporates PCF reduction into →_{sto}; if the term component of a state may take a single PCF transition, the state pair may take the corresponding transition. The new operator allocates a new

(λx.M)N →_{1} M[N/x] (β)
YM →_{1} M(YM)
pred 0 →_{1} 0
pred n →_{1} n′, if n > 0 and n = n′ + 1
zero? 0 →_{1} true
zero? n →_{1} false, if n ≠ 0
if true MN →_{1} M
if false MN →_{1} N
eq?_{loc} l_{1}l_{2} →_{1} true, if l_{1} = l_{2}
eq?_{loc} l_{1}l_{2} →_{1} false, if l_{1} ≠ l_{2}
π_{1}(pair MN) →_{1} M
π_{2}(pair MN) →_{1} N
case(inl M)NP →_{1} (NM)
case(inr M)NP →_{1} (P M)

\frac{M →_{1} N}{C[M] →_{pcf} C[N]}

Figure 3: PCF Reduction Rules

location in the store, initializes the fresh location to its first argument, and invokes its second argument with the new location. The deref operator invokes its second argument with the value in the store at the location given by its first argument. The update operator destructively updates the location given by its first argument to be the term given by its second argument and then invokes its third argument. Like PCF reduction, store operations are “lazy” in that store update is done with terms that are not necessarily in normal form. The reflexive, transitive closure of →_{sto} is denoted by →_{sto}^{∗}. If a state ⟨⟨M ; Σ⟩⟩ takes n steps to state ⟨⟨M′ ; Σ′⟩⟩, we write ⟨⟨M ; Σ⟩⟩ →^{n}_{sto} ⟨⟨M′ ; Σ′⟩⟩. The domain (a set of locations) and range (a set of terms) of a store Σ are denoted by dom(Σ) and rng(Σ), respectively. The meta-operation locs(M) simply returns any locations referenced in M and is easily defined via structural induction:

M →_{pcf} M′ ⇒ ⟨⟨M ; Σ⟩⟩ →_{sto} ⟨⟨M′ ; Σ⟩⟩
⟨⟨new^{τ} M N ; Σ⟩⟩ →_{sto} ⟨⟨N l^{τ} ; Σ[l^{τ} ↦ M]⟩⟩, if
l^{τ} ∉ dom(Σ) ∪ locs(rng(Σ), M, N)
⟨⟨deref^{τ} l^{τ} M ; Σ⟩⟩ →_{sto} ⟨⟨M N ; Σ⟩⟩ if Σ(l^{τ}) = N
⟨⟨update^{τ} l^{τ} M N ; Σ⟩⟩ →_{sto} ⟨⟨N ; Σ[l^{τ} ↦ M]⟩⟩ if l^{τ} ∈ dom(Σ)

Figure 4: Operational Semantics for Store Operators

Definition 2.2.1

1. if M = l, locs(M) = {l},

2. if M = (M_{1} M_{2}), locs(M) = locs(M_{1}) ∪ locs(M_{2}), and

3. if M = (λx:τ.M_{1}), locs(M) = locs(M_{1}),

4. otherwise, locs(M) = ∅.

When applied to a set S of terms,

locs(S) = ⋃_{M∈S} locs(M)

Also,

locs(M_{1}, …, M_{n}) = locs(M_{1}) ∪ … ∪ locs(M_{n})

A labeled transition system →^{α}_{io} for the I/O operators is defined in Figure 5. The write operator writes its integer argument and invokes its continuation. The read operator reads an integer and invokes its continuation with the number read. The stop operator takes a √ transition to the stopped state ⟨⟨stopped ; Σ′⟩⟩, from which there are no transitions. Note that the write I/O operator, and the deref and update store operators, are strict in their first arguments.

\frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨write n M′ ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{!n}_{io} ⟨⟨M′ ; Σ′⟩⟩}  \frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨read M′ ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{?n}_{io} ⟨⟨M′ n ; Σ′⟩⟩}

\frac{⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨stop ; Σ′⟩⟩}{⟨⟨M ; Σ⟩⟩ →^{√}_{io} ⟨⟨stopped ; Σ′⟩⟩}

Figure 5: Semantics for I/O Operators

2.3 State Equivalence – Bisimulation

A standard notion of equivalence for labeled transition systems is that of strong bisimulation. For a good introduction to bisimulation, see [Mil90]. It is interesting to note that labeled transition systems and various notions of bisimulation have historically been the basic tools used to reason about concurrent processes and languages. Researchers into sequential languages, notably Abramsky [Abr90], Pitts [PS93, RP95] and Gordon [Gor94b, Gor94a, Gor95], have adapted these techniques for sequential, and usually deterministic, settings. Two states are strongly bisimilar if they can always take the same sequence of labeled transitions. We say that a relation between states is a strong bisimulation if whenever two states are in the relation, they can take the same action (labeled transition) and stay in the relation. In the following definitions, we let α range over the set of actions, Act = {?n,!n, √}, pronounced “read n”, “write n”, and “halt,” for all integers n.

Definition 2.3.1 ([−]_{bisim}) Given R a relation on states, we define a relation [R]_{bisim} on states as follows.

⟨⟨M ; Σ_{M}⟩⟩ [R]_{bisim} ⟨⟨N ; Σ_{N}⟩⟩

iff for all α ∈ Act,

1. if ⟨⟨M ; Σ_{M}⟩⟩ →^{α}_{io} ⟨⟨M′ ; Σ_{M′}⟩⟩, then ∃N′, Σ_{N′} s.t. ⟨⟨N ; Σ_{N}⟩⟩ →^{α}_{io} ⟨⟨N′ ; Σ_{N′}⟩⟩ and

⟨⟨M′ ; Σ_{M′}⟩⟩ R ⟨⟨N′ ; Σ_{N′}⟩⟩

2. if ⟨⟨N ; Σ_{N}⟩⟩ →^{α}_{io} ⟨⟨N′ ; Σ_{N′}⟩⟩, then ∃M′, Σ_{M′} s.t. ⟨⟨M ; Σ_{M}⟩⟩ →^{α}_{io} ⟨⟨M′ ; Σ_{M′}⟩⟩ and

⟨⟨M′ ; Σ_{M′}⟩⟩ R ⟨⟨N′ ; Σ_{N′}⟩⟩

The symmetry in the above definition is clear, and we will usually focus only on one direction, simulation:

Definition 2.3.2 ([−]_{sim} – simulation generator) Given R a relation on states, we define a relation [R]_{sim} on states as follows.

⟨⟨M ; Σ_{M}⟩⟩ [R]_{sim} ⟨⟨N ; Σ_{N}⟩⟩

iff for all α ∈ Act,

if ⟨⟨M ; Σ_{M}⟩⟩ →^{α}_{io} ⟨⟨M′ ; Σ_{M′}⟩⟩, then ∃N′, Σ_{N′} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →^{α}_{io} ⟨⟨N′ ; Σ_{N′}⟩⟩ and

⟨⟨M′ ; Σ_{M′}⟩⟩ R ⟨⟨N′ ; Σ_{N′}⟩⟩

We can unwind the definition of the transition relation →^{α}_{io} to get an equivalent definition of the simulation generator [−]_{sim} in terms of the store semantics transition relation →_{sto}, as follows.

Lemma 2.3.3 Given R a relation on states, ⟨⟨M ; Σ_{M}⟩⟩ [R]_{sim} ⟨⟨N ; Σ_{N}⟩⟩ iff

1. if ⟨⟨M ; Σ_{M}⟩⟩ →_{sto}^{∗} ⟨⟨write nM′ ; Σ′_{M}⟩⟩, then ∃N′, Σ′_{N} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →_{sto}^{∗} ⟨⟨write nN′ ; Σ′_{N}⟩⟩ and ⟨⟨M′ ; Σ′_{M}⟩⟩ R ⟨⟨N′ ; Σ′_{N}⟩⟩,

2. if ⟨⟨M ; Σ_{M}⟩⟩ →_{sto}^{∗} ⟨⟨read M′ ; Σ′_{M}⟩⟩, then ∃N′, Σ′_{N} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →_{sto}^{∗} ⟨⟨read N′ ; Σ′_{N}⟩⟩ and ∀n.⟨⟨M′ n ; Σ′_{M}⟩⟩ R ⟨⟨N′ n ; Σ′_{N}⟩⟩, 3. if ⟨⟨M ; Σ_{M}⟩⟩ →_{sto}^{∗} ⟨⟨stop ; Σ′_{M}⟩⟩, then ∃Σ′_{N} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →_{sto}^{∗} ⟨⟨stop ; Σ′_{N}⟩⟩ and ⟨⟨stopped ; Σ′_{M}⟩⟩ R ⟨⟨stopped ; Σ′_{N}⟩⟩.

Proof: By unwinding the definition of →^{α}_{io}.

Most of our proofs of simulation will be based on Lemma 2.3.3. Actually, the cases for each I/O operator are always quite similar, so most proofs will do only one case for reduction under →_{sto} to a “generic” I/O operator, io, which is considered to take a single continuation term. The fact that the write operator requires its first argument to reduce to an integer first does not affect any of our proofs, as only PCF reductions are allowed in that position, and PCF reduction preserves simulation. As with bisimulation relations, we call a binary relation between states a simulation if whenever two states are in the relation, they can take the same action and stay within the relation. More formally, a relation R is called a simulation relation iff R ⊆ [R]_{sim}. The largest simulation relation is called, not surprisingly, simulation, and it is denoted by ≲_{sim}. We take membership in ≲_{sim} to be our basic notion of (preordered) equivalence between states. The largest bisimulation relation, called bisimulation, is denoted ≈_{sim}. Simulation, ≲_{sim} is therefore the union of all simulation relations,

≲_{sim}= ⋃{R | R ⊆[R]_{sim}}

which is easily shown to be the greatest fixed point of [−]_{sim}. From this definition of ≲_{sim} as the greatest fixed point of the operator [−]_{sim} on relations, we get the following principle of coinduction:

R ⊆ [R]_{sim} ⇒ R ⊆ ≲_{sim}

This principle of coinduction forms the basis for most of our proofs of simulation.

2.3.1 Bisimulation in a Deterministic Setting

The reduction rules for our metalanguage are deterministic up to the choice of location constants returned by the new operator. In Section 2.5.4, we prove that metalanguage states that differ only up to a consistent renaming of locations (denoted α_{loc}) are bisimilar. When stating that our metalanguage is deterministic, then, we use the following definition of determinism:

Definition 2.3.4 (Deterministic Transition System) A transition system →^{α} is deterministic if, for any state A,

if A →^{α} B and A →^{α} B′, then

B ≈_{sim} B′

Given a deterministic transition system, one can prove bisimulation of two states using symmetric simulation subproofs:

Lemma 2.3.5 For simulation ≲_{sim} and bisimulation ≈_{sim} defined based on a deterministic transition system,

if A ≲_{sim} B and B ≲_{sim} A, then
A ≈_{sim} B

Proof: By coinduction. Let: S =^{def} {(A, B) | A ≲_{sim} B and B ≲_{sim} A} We must show that S ⊆ [S]_{bisim}. That is, given (A, B) ∈ S, we must show:

1. If A →^{α} A′, then ∃B′ s.t. B →^{α} B′ and A′ S B′, and

2. If B →^{α} B′, then ∃A′ s.t. A →^{α} A′ and B′ S A′.

⟨1⟩1. if A →^{α} A′, then ∃B′ s.t. B →^{α} B′ and A′ S B′

Proof:

⟨2⟩1. ∃B′ s.t. B →^{α} B′ and A′ ≲_{sim} B′

By (A, B) ∈ S ⇒ A ≲_{sim} B.

⟨2⟩2. ∃A′′ s.t. A →^{α} A′′ and B′ ≲_{sim} A′′

By (A, B) ∈ S ⇒ B ≲_{sim} A. ⟨2⟩3. A′ ≈_{sim} A′′

By determinism. ⟨2⟩4. B′ ≲_{sim} A′

By B′ ≲_{sim} A′′ ≈_{sim} A′ and (≲_{sim} ∘ ≈_{sim}) ⊆ ≲_{sim} (a simple coinduction).

⟨1⟩2. if B →^{α} B′, then ∃A′ s.t. A →^{α} A′ and B′ S A′

Proof:

By the same line of reasoning as in the first case.

Thus most of our proofs of bisimulation consist of two proofs of simulation. Furthermore, in most cases the two simulation proofs are nearly identical, and we will only present one direction in detail. Whenever the other simulation proof would be different (or impossible), we point that out. It should be noted that in a nondeterministic setting the preceding lemma does not hold. Consider a nondeterministic transition system with a single action (so we omit the arrow labels in the diagrams) and two processes, A and B, with transition diagrams as follows:

The labels {a, b, c, d} represent states. We show that A ≲_{sim} B by defining the relation R on states,

R =^{def} {(a, a), (b, b), (c, c), (d, b)}

and then proving that R ⊆ [R]_{sim}. Likewise, we can show that B ≲_{sim} A by defining the relation S on states,

S =^{def} {(a, a), (b, b), (c, c)}

and showing that S ⊆ [S]_{sim}. However, clearly A ≉_{sim} B, because when A takes a transition to state d, B can only transition to state b. While state b can take all of the actions that d can (none), it is not true that d can take all of the actions that b can.

2.4 Term Equivalence

Bisimulation defines when two states (i.e. program-store pairs) have the same behavior. Often we are interested in comparing two terms for equivalence, and the two terms may not be programs. We use a standard notion of equivalence between terms, contextual equivalence, which formalizes when two terms are indistinguishable.

2.4.1 Contextual Equivalence

We say that two terms are contextually equivalent if they have the same I/O behavior when inserted into every possible program context. We define contextual equivalence on open terms, as contexts may capture free variables.

Definition 2.4.1 (contextual preorder, ≲_{∀C}) If Γ ⊢ M, N:τ, then

Γ ⊢ M ≲_{∀C} N:τ

iff for all closing contexts C[−_{τ}] of type pr that respect Γ, and for all stores Σ,

⟨⟨C[M] ; Σ⟩⟩ ≲_{sim} ⟨⟨C[N] ; Σ⟩⟩

Contextual equivalence, ≅_{∀C}, is the symmetrization of ≲_{∀C}:

Definition 2.4.2 (contextual equivalence, ≅_{∀C}) If Γ ⊢ M, N:τ, then

Γ ⊢ M ≅_{∀C} N:τ

iff for all closing contexts C[−_{τ}] of type pr that respect Γ, and for all stores Σ,

⟨⟨C[M] ; Σ⟩⟩ ≈_{sim} ⟨⟨C[N] ; Σ⟩⟩

The contextual preorder and contextual equivalence are, by definition, congruences – that is, both relations are preserved by all term constructors of the language. Contextual equivalence is the relation we are most interested in between terms. However, the quantification over all contexts makes ≅_{∀C} difficult to establish directly, and we expend considerable effort developing methods to ease this proof burden. The most important tool is a “context lemma” which states that two terms are similar in a limited set of contexts if and only if they are contextually equivalent. We will call equivalence in this restricted class of contexts extensional equivalence.

2.4.2 Extensional Equivalence

For each type constructor (→, +, ×), there is a natural way of determining whether two terms of such a type “behave the same way”. At function types α→β, two terms are extensionally equal if they take every term of type α to equivalent terms of type β. For product types, both projections should be equivalent, and for sum types, the case operator should produce equivalent terms. We can view these type-based contexts (application, projection, and case) as type deconstructors, as they decompose complex types into terms of their component types.

T_{o}[−]:o ::= [−] – base types T_{α→β}[−]:o ::= T_{β}[([−] M)]:o – ∀ closed M:α T_{α×β}[−]:o ::= T_{α}[π_{1}[−]]:o | T_{β}[π_{2}[−]]:o T_{α+β}[−]:o ::= T_{(α→γ)→(β→γ)→γ}[case_{α,β}^{γ}[−]]:o – ∀ types γ

Figure 6: Grammar for Type Contexts

While contextual equivalence is defined to be equivalence under all term constructors, extensional equivalence is defined to be equivalence under all type deconstructors, as described above. Figure 6 gives the grammar for type contexts. Type contexts T_{α}[−]:o are contexts with a single hole of type α which produce base type o. The type contexts with holes of base type are simply the empty context. That is,

T_{int}[−]:int ≡ … ≡ T_{pr}[−]:pr ≡ [−]

There are no type contexts such as T_{o}[−]:o′ for different base types o and o′. Extensional equivalence for closed terms at base types is defined simply. For base types other than pr, terms must PCF-reduce to the same constant. Equivalent terms of type pr must be in ≈_{sim} for all stores Σ. We use the superscript • to indicate relations on closed terms.

Definition 2.4.3 (extensional equivalence for closed terms at base type, ≅_{o}^{•}) For closed terms M and N,

(int) M ≅_{int}^{•} N iff M →_{pcf}^{∗} n ⇔ N →_{pcf}^{∗} n.

(bool) M ≅_{bool}^{•} N iff M →_{pcf}^{∗} b ⇔ N →_{pcf}^{∗} b, b ∈ {true, false}.

(ref (τ)) M ≅_{ref (τ)}^{•} N iff M →_{pcf}^{∗} l^{τ} ⇔ N →_{pcf}^{∗} l^{τ}.

(pr) M ≅_{pr}^{•} N iff ∀Σ . ⟨⟨M ; Σ⟩⟩ ≈_{sim} ⟨⟨N ; Σ⟩⟩.

Extensional equivalence at complex types is defined in terms of type contexts and equivalence at base types.

Definition 2.4.4 (extensional equivalence, complex types, ≅_{ext}^{•})

M ≅_{ext}^{•} N:τ

iff M, N:τ and for all base types o,

∀T_{τ} [−]:o . T_{τ} [M] ≅_{o}^{•} T_{τ} [N].

The definition of the extensional preorder, ≲_{ext}^{•} has exactly the same structure as for ≅_{ext}^{•}, except that in the previous two definitions, the ⇔’s are replaced by ⇒ and ≲_{sim} is used for equivalence at pr type:

Definition 2.4.5 (extensional preorder, base types, ≲_{o}^{•}) For closed terms M and N,

(int) M ≲_{int}^{•} N iff M →_{pcf}^{∗} n ⇒ N →_{pcf}^{∗} n.

(bool) M ≲_{bool}^{•} N iff M →_{pcf}^{∗} b ⇒ N →_{pcf}^{∗} b, b ∈ {true, false}.

(ref (τ)) M ≲_{ref (τ)}^{•} N iff M →_{pcf}^{∗} l^{τ} ⇒ N →_{pcf}^{∗} l^{τ}.

(pr) M ≲_{pr}^{•} N iff ∀Σ . ⟨⟨M ; Σ⟩⟩ ≲_{sim} ⟨⟨N ; Σ⟩⟩.

Definition 2.4.6 (extensional preorder, complex types, ≲_{ext}^{•}) M ≲_{ext}^{•} N:τ iff M, N:τ and for all base types o,

∀T_{τ} [−]:o . T_{τ} [M] ≲_{o}^{•} T_{τ} [N].

2.4. TERM EQUIVALENCE 29 The following simple proposition about ≲_{ext}^{•} is used frequently: Proposition 2.4.7 If M ≲_{ext}^{•} N:τ and (MP_{1} … P_{k}):τ′ for k ≥ 0, then (MP_{1} … P_{k}) ≲_{ext}^{•} (NP_{1} … P_{k}):τ′. Proof: Easy induction on k. We extend the definitions of extensional equivalence to open terms by quantifying over closing substitutions. Definition 2.4.8 (≅_{ext}) If Γ ⊢ M, N:τ, then

Γ ⊢ M ≅_{ext} N:τ

iff for all closing substitutions σ that respect Γ, Mσ ≅_{ext}^{•} Nσ:τ

And similarly for the extensional preorder on open terms, ≲_{ext}: Definition 2.4.9 (≲_{ext}) If Γ ⊢ M, N:τ, then

Γ ⊢ M ≲_{ext} N:τ

iff for all closing substitutions σ that respect Γ, Mσ ≲_{ext}^{•} Nσ:τ 2.4.2.1 Coinductive Definition of Extensional Equivalence

Following is an equivalent, coinductive definition of extensional equivalence. It is this definition that is used to structure proofs of extensional equivalence, because we cannot use induction on recursive types. First we define the extensional simulation generator, [−]_{ext}, which operates on type-indexed families of relations between closed well-typed terms.

Definition 2.4.10 ([−]_{ext}) Given R a type-indexed family of relations on closed terms, R = {R_{τ} | τ a type}, define

[R]_{ext} =^{def} {[R]_{ext}^{τ}| τ a type}

where

M [R]_{ext}^{o} N ⇔ M ≲_{o}^{•} N
M [R]_{ext}^{α→β} N ⇔ ∀P:α . (MP) R_{β} (NP)  – P closed
M [R]_{ext}^{α×β} N ⇔ (π_{1} M) R_{α} (π_{1} N) and (π_{2} M) R_{β} (π_{2} N)
M [R]_{ext}^{α+β} N ⇔ ∀γ . (case M) R_{(α→γ)→(β→γ)→γ} (case N)

For now we denote the greatest fixed point of [−]_{ext} as ≲_{ext}^{∗}, until we prove that in fact ≲_{ext}^{∗} = ≲_{ext}^{•}. Following are properties that the relation ≲_{ext}^{∗} satisfies as a fixed point of [−]_{ext}:

1. M ≲_{ext}^{∗} N:o ⇔ M ≲_{o}^{•} N

2. M ≲_{ext}^{∗} N:α→β ⇔ ∀P:α . (MP) ≲_{ext}^{∗} (NP):β – P closed

3. M ≲_{ext}^{∗} N:α×β ⇔ (π_{1} M) ≲_{ext}^{∗} (π_{1} N):α, and (π_{2} M) ≲_{ext}^{∗} (π_{2} N):β

4. M ≲_{ext}^{∗} N:α+β ⇔ ∀γ, P_{1}:α→γ, P_{2}:β→γ . – P_{1}, P_{2} closed (case MP_{1}P_{2}) ≲_{ext}^{∗} (case NP_{1}P_{2}):γ

Proposition 2.4.11

≲_{ext}^{∗} = ≲_{ext}^{•}

Proof: ⟨1⟩1. (⊇)

Proof sketch: use coinduction – show that ≲_{ext}^{•} ⊆ [≲_{ext}^{•}]_{ext} Assume: M ≲_{ext}^{•} N:τ Prove: M [≲_{ext}^{•}]_{ext} N Proof: Cases of τ: ⟨2⟩1. Case: base types o

Immediate. ⟨2⟩2. Case: α→β

Immediate from Proposition 2.4.7. ⟨2⟩3. Case: Other type constructions are similar

⟨1⟩2. (⊆)

Assume: M ≲_{ext}^{∗} N:τ Prove: ∀o . ∀T_{τ} [−]:o . T_{τ} [M] ≲_{o}^{•} T_{τ} [N] Proof: Structural induction on T_{τ} [−]:o: ⟨2⟩1. Case: T_{o} = [−], M, N:o

Proof: Immediate. ⟨2⟩2. Case: T = T′_{β}[([−] P)]:o, P:α, with M, N:α→β

Proof: By M ≲_{ext}^{∗} N:(α→β), we have ∀P:α . (M P) ≲_{ext}^{∗} (N P):β. By IH(T′), we have T′[(M P)] ≲_{o}^{•} T′[(N P)], so we are done.

⟨2⟩3. Case: Other constructions for T are similar.

All of the basic relations we use are easily shown to enjoy reflexivity and transitivity:

Lemma 2.4.12 The relations ≲_{sim}, ≲_{∀C}, ≲_{ext}, ≲_{ext}^{•}, and their symmetrizations (≈_{sim}, ≅_{∀C}, ≅_{ext}, ≅_{ext}^{•}), are preorders.

Lemma 2.4.13 Given a preorder S on states, [S]_{sim} is a preorder.

Lemma 2.4.14 Given a type-indexed family of relations on terms, R, [R]_{ext} is a preorder.

2.5 Theory of the Metalanguage

The main theoretical result in this section is an Extensionality Theorem which states that extensional equivalence coincides with contextual equivalence, i.e.,

∀Γ, M, N . Γ ⊢ M ≅_{ext} N:τ ⇔ Γ ⊢ M ≅_{∀C} N:τ

We get this extensionality result by showing that the extensional preorder is a precongruence, namely that ≲_{ext} is preserved by the term constructors of the metalanguage. To prove the precongruence lemma, we need a substitution lemma, stating that substitution of a variable by ≲_{ext}^{•}-related terms produces ≲_{ext}^{•}-related terms. The proof of the substitution lemma is the most involved. Before we can get to the big, important proofs, we need to establish a number of supporting properties of the metalanguage. The reader is invited to skim this section, noting the lemmas given, and referring back to this section as needed whilst poring over the more interesting proofs later.

2.5.1 Simulations

The typical structure of a proof of simulation in our metalanguage is to use coinduction at the outermost level and to use induction to prove the individual cases. Given a monotonic relational operator such as [−]_{sim}, and a candidate simulation relation S, a standard coinductive argument is to show that S ⊆ [S]_{sim} and that therefore S ⊆ ≲_{sim}. Often, though, it is more straightforward to show something such as S ⊆ [≲_{sim} ∘ S ∘ ≲_{sim}]_{sim}, thus requiring a supporting lemma that [≲_{sim} ∘ S ∘ ≲_{sim}]_{sim} ⊆ ≲_{sim}. These supporting lemmas are usually easy to prove, and are often referred to as “Simulation up to”, as presented in [Mil90, Propositions 3.4.2 and 3.4.3]. We give the basic lemmas, mutatis mutandis for our notation, here.

Definition 2.5.1 A relation S over states is a simulation up to ≲_{sim} if (≲_{sim} ∘ S ∘ ≲_{sim}) is a simulation.

Because ≲_{sim} is defined as the greatest fixed point of [−]_{sim}, the way we show that (≲_{sim} ∘ S ∘ ≲_{sim}) is a simulation (i.e., is contained in ≲_{sim}) is to show that

(≲_{sim} ∘ S ∘ ≲_{sim}) ⊆ [≲_{sim} ∘ S ∘ ≲_{sim}]_{sim}

Lemma 2.5.2 (Milner) If S is a simulation up to ≲_{sim}, then S ⊆ ≲_{sim}.

Proof: Let P S Q. Then by reflexivity of ≲_{sim}, P (≲_{sim} ∘ S ∘ ≲_{sim}) Q. So P ≲_{sim} Q since ≲_{sim} ∘ S ∘ ≲_{sim} ⊆ ≲_{sim}.

Lemma 2.5.3 (Milner) Given a relation S over states, if S ⊆ [≲_{sim} ∘ S ∘ ≲_{sim}]_{sim}, then S ⊆ ≲_{sim}.

Proof: By Lemma 2.5.2, it is enough to show that (≲_{sim} ∘ S ∘ ≲_{sim}) ⊆ [≲_{sim} ∘ S ∘ ≲_{sim}]_{sim} (i.e. that S is a simulation up to ≲_{sim}). For this purpose, let P (≲_{sim} ∘ S ∘ ≲_{sim}) Q – i.e. there exists P_{1}, Q_{1} such that P ≲_{sim} P_{1} S Q_{1} ≲_{sim} Q. Suppose P →^{α}_{io} P′; we wish to find Q′ so that Q →^{α}_{io} Q′ and P′ (≲_{sim} ∘ S ∘ ≲_{sim}) Q′. This is done by filling in the bottom row of the following diagram from left to right, starting with the given P′:

P ≲_{sim} P_{1}  S  Q_{1} ≲_{sim} Q
↓  ↓  ↓  ↓
P′ ≲_{sim} P′_{1} ≲_{sim}∘ S ∘≲_{sim} Q′_{1} ≲_{sim} Q′

2.5.2 Properties of the Extended PCF Functional Sublanguage

Several properties of PCF, proved elsewhere in the literature, are used to get results about our metalanguage, which is an extension of PCF. Because PCF has been extensively studied, we present only the statements of the PCF properties we need. For a good introduction to PCF, and for detailed proofs including confluence, subject reduction, and standardization, see [Mit96]. Recursive types are not a standard part of PCF and are more reminiscent of FPC, as presented in textbooks by Gunter [Gun92] or Winskel [Win93]. In [Gor95], Andrew Gordon presents a bisimilarity-based theory of FPC, including extensionality.

Lemma 2.5.4 (Subject Reduction for PCF) If M:τ and M →_{pcf} N, then N:τ.

Lemma 2.5.5 (Confluence for PCF) If M →_{pcf}^{∗} N and M →_{pcf}^{∗} N′, then ∃P such that N →_{pcf}^{∗} P and N′ →_{pcf}^{∗} P.

The confluence property is also known as the “Church-Rosser” (CR) property or the “Diamond” property, after the commuting diagram used to illustrate confluence:

It is fundamental that if a term PCF-reduces to a constant, then a leftmost reduction strategy will reduce to the same constant. See [JM91] for a detailed proof of standardization for PCF-like reduction systems.

Definition 2.5.6 (→_{left,pcf}^{∗}) The transition relation →_{left,pcf} always chooses the leftmost PCF reduction.

Lemma 2.5.7 (Completeness of Leftmost Reduction for PCF) For all constants c of type int, bool, or ref (τ), If M →_{pcf}^{∗} c, then M →_{left,pcf}^{∗} c.

2.5. THEORY OF THE METALANGUAGE 35 2.5.3 Subject Reduction for Metalanguage Lemma 2.5.8 (Subject Reduction)

1. If ⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨M′ ; Σ′⟩⟩, then ∅ ⊢ M′:pr.

2. If ⟨⟨M ; Σ⟩⟩ →^{a}_{io} ⟨⟨M′ ; Σ′⟩⟩, then ∅ ⊢ M′:pr. Proof: Easy by inspection of reduction rules. 2.5.4 Simulation up to Location Renaming A property that is used in nearly every simulation proof is that a consistent renaming of locations between states maintains ≲_{sim}. Two states are equal up to a renaming of location constants, denoted α_{loc}, if there is a partial bijection^{1} Θ between locations that satisfies several properties: Definition 2.5.9 (α_{loc})

⟨⟨M ; Σ_{M}⟩⟩ α_{loc} ⟨⟨N ; Σ_{N}⟩⟩

iff ∃Θ ⊆ Locs × Locs s.t.

1. Θ is a partial bijection

2. MΘ = N

3. locs(M) ⊆ dom(Θ)

4. if (l, l′) ∈ Θ then either (a) l ∉ dom(Σ_{M}) and l′ ∉ dom(Σ_{N}) or

(b) Σ_{M}(l)Θ = Σ_{N}(l′) and locs(Σ_{M}(l)) ⊆ dom(Θ)

1Θ is a partial bijection iff Θ has the property that if (i, j) ∈ Θ and (i′, j′) ∈ Θ, then (i = i′ ⇔ j = j′).

Lemma 2.5.10 If ⟨⟨M ; Σ_{M}⟩⟩ α_{loc} ⟨⟨N ; Σ_{N}⟩⟩ and ⟨⟨M ; Σ_{M}⟩⟩ →^{n}_{sto} ⟨⟨M′ ; Σ′_{M}⟩⟩, then ∃N′, Σ′_{N} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →^{n}_{sto} ⟨⟨N′ ; Σ′_{N}⟩⟩

and ⟨⟨M′ ; Σ′_{M}⟩⟩ α_{loc} ⟨⟨N′ ; Σ′_{N}⟩⟩.

Proof: Induction on n.

Lemma 2.5.11 (α_{loc})

α_{loc} ⊆ ≲_{sim}

Proof: Proof sketch: Use coinduction. ⟨1⟩1. α_{loc} ⊆ [α_{loc}]_{sim}

Assume: 1. ⟨⟨M ; Σ_{M}⟩⟩ α_{loc} ⟨⟨N ; Σ_{N}⟩⟩, witnessed by 2. Θ ⊆ dom(Σ_{M}) × dom(Σ_{N}) a partial bijection

3. ⟨⟨M ; Σ_{M}⟩⟩ →^{n}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

Prove: ∃N′, Σ′_{N} s.t.

⟨⟨N ; Σ_{N}⟩⟩ →_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ and

⟨⟨M′ ; Σ′_{M}⟩⟩ α_{loc} ⟨⟨N′ ; Σ′_{N}⟩⟩.

Proof: Induction on n.

⟨2⟩1. Case: n = 0 If n = 0, it must be that both sides are headed by the same I/O operator and that they stay (after 0 steps) in α_{loc}.

⟨2⟩2. Case: n > 0 Note that the left- and right-hand sides must have the same term structure, differing only in the actual location constants. Therefore, for each step that the left-hand side takes, the right-hand side may take a corresponding step. Consider the first step in the reduction of the left-hand side:

⟨⟨M ; Σ_{M}⟩⟩ →^{1}_{sto} ⟨⟨M′′ ; Σ′′_{M}⟩⟩ →^{n−1}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

Either the first step is an internal PCF reduction, a head PCF reduction, or a head store operation reduction. It is clear that PCF reductions do not affect α_{loc} – the same Θ remains valid after both sides take the same step. For head store reductions, deref and update both maintain α_{loc} with the same Θ. This leaves new as the only interesting case: ⟨3⟩1. Case: M = new M_{1}M_{2}

⟨4⟩1. lhs = ⟨⟨new M_{1} M_{2} ; Σ_{M}⟩⟩

→^{1}_{sto} ⟨⟨(M_{2} l) ; Σ_{M}[l ↦ M_{1}]⟩⟩ l fresh

=^{def} lhs′
→^{j<n}_{left,sto} ⟨⟨io M′′ ; Σ′′_{M}⟩⟩

⟨4⟩2. rhs = ⟨⟨new N_{1} N_{2} ; Σ_{N}⟩⟩

→^{1}_{sto} ⟨⟨(N_{2} l′) ; Σ_{N}[l′ ↦ N_{1}]⟩⟩ l′fresh

=^{def} rhs′
⟨4⟩3. lhs′ α_{loc} rhs′

Proof: Construct new partial bijection Θ′ = Θ ∪ {(l, l′)}. ⟨4⟩4. Q.E.D.

Proof: by IH(j).

2.5.5 PCF Reduction Preserves Simulation (Full Beta)

We can do fully lazy PCF reduction (a.k.a. “full β”) without affecting the observable behavior of states. First we define PCF-equality for terms (=_{pcf} term) and states (=_{pcf} state). Generally it will be obvious whether we are referring to =_{pcf} between terms or states, and we will usually omit the superscript.

Definition 2.5.12 (=_{pcf} term)

M =_{pcf} term N

iff ∃P s.t.

M →_{pcf}^{∗} P and N →_{pcf}^{∗} P.

Definition 2.5.13 (=_{pcf} state)

⟨⟨M ; Σ_{M}⟩⟩ =_{pcf} state ⟨⟨N ; Σ_{N}⟩⟩

iff 1. M =_{pcf} term N, and

2. dom(Σ_{M}) = dom(Σ_{N}), and

3. ∀l ∈ dom(Σ_{M}) . Σ_{M}(l) =_{pcf} term Σ_{N}(l)

Lemma 2.5.14 (=_{pcf} term is a congruence) =_{pcf} term is a congruence. That is, if M =_{pcf} term N and M, N:τ, then for all contexts C[−_{τ}]:τ′,

C[M] =_{pcf} term C[N]

Proof: Easy induction on structure of C. Lemma 2.5.15 (full β for states) If ⟨⟨M ; Σ_{M}⟩⟩ =_{pcf} state ⟨⟨N ; Σ_{N}⟩⟩, then

⟨⟨M ; Σ_{M}⟩⟩ ≲_{sim} ⟨⟨N ; Σ_{N}⟩⟩.

Proof:

Assume: ⟨⟨M ; Σ_{M}⟩⟩ →^{n}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

Prove: ∃N′, Σ′_{N} s.t. ⟨⟨N ; Σ_{N}⟩⟩ →_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ and ⟨⟨M′ ; Σ′_{M}⟩⟩(≲_{sim} ∘ =_{pcf} state ∘ ≲_{sim})⟨⟨N′ ; Σ′_{N}⟩⟩ by induction on n.

⟨1⟩1. Case: n = 0 Proof: By M =_{pcf} N and M = io M′, it must be that ∃N′ s.t. N →_{pcf}^{∗} io N′ and M′ =_{pcf} N′.

⟨1⟩2. Case: n > 0 Consider the first step in the sequence of reductions. ⟨2⟩1. Case: First step is a PCF reduction

Clearly both sides stay in =_{pcf} , so result follows from IH(n − 1). ⟨2⟩2. Case: First step is a store operator

Consider new case:

⟨3⟩1. Case: M = new M_{1} M_{2}

⟨4⟩1. lhs =^{def} ⟨⟨M ; Σ_{M}⟩⟩ = ⟨⟨new M_{1} M_{2} ; Σ_{M}⟩⟩

→^{1}_{sto} ⟨⟨(M_{2} l) ; Σ_{M}[l ↦ M_{1}]⟩⟩ l fresh w.r.t. {M_{1}, M_{2}, Σ_{M}}

=^{def} lhs′
→^{j<n}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨4⟩2. ∃N_{1}, N_{2} s.t. N →_{pcf}^{∗} new N_{1} N_{2} and M_{1} =_{pcf} N_{1} and M_{2} =_{pcf} N_{2}

Proof: By M =_{pcf} N and M = new M_{1}M_{2}.

⟨4⟩3. rhs =^{def} ⟨⟨N ; Σ_{N}⟩⟩

→_{pcf}^{∗} ⟨⟨new N_{1} N_{2} ; Σ_{N}⟩⟩ by Step ⟨4⟩2

→^{1}_{sto} ⟨⟨(N_{2} l′) ; Σ_{N}[l′ ↦ N_{1}]⟩⟩ l′ fresh w.r.t. {N_{1}, N_{2}, Σ_{N}}

=^{def} rhs′

Let: l′′ be fresh w.r.t. {M_{1}, M_{2}, N_{1}, N_{2}, Σ_{M}, Σ_{N}}.

⟨4⟩4. ⟨⟨(M_{2} l) ; Σ_{M}[l ↦ M_{1}]⟩⟩ α_{loc} ⟨⟨(M_{2} l′′) ; Σ_{M}[l′′ ↦ M_{1}]⟩⟩
⟨4⟩5. ⟨⟨(N_{2} l′) ; Σ_{N}[l′ ↦ N_{1}]⟩⟩ α_{loc} ⟨⟨(N_{2} l′′) ; Σ_{N}[l′′ ↦ N_{1}]⟩⟩

⟨4⟩6. ∃M′′, Σ′′_{M} s.t. ⟨⟨(M_{2} l′′) ; Σ_{M}[l′′ ↦ M_{1}]⟩⟩ →^{j<n}_{sto} ⟨⟨io M′′ ; Σ′′_{M}⟩⟩

s.t. ⟨⟨M′ ; Σ′_{M}⟩⟩ α_{loc} ⟨⟨M′′ ; Σ′′_{M}⟩⟩

By Lemma 2.5.10.

⟨4⟩7. ⟨⟨(M_{2} l′′) ; Σ_{M}[l′′ ↦ M_{1}]⟩⟩ =_{pcf} ⟨⟨(N_{2} l′′) ; Σ_{N}[l′′ ↦ N_{1}]⟩⟩

By Step ⟨4⟩2. ⟨4⟩8. ∃N′′, Σ′′_{N} s.t. ⟨⟨(N_{2} l′′) ; Σ_{N}[l′′ ↦ N_{1}]⟩⟩ →_{sto}^{∗} ⟨⟨io N′′ ; Σ′′_{N}⟩⟩ and ⟨⟨M′′ ; Σ′′_{M}⟩⟩ (≲_{sim} ∘ =_{pcf} ∘ ≲_{sim})

⟨⟨N′′ ; Σ′′_{N}⟩⟩ Proof: By steps ⟨4⟩6 and ⟨4⟩7 and IH(j).

⟨4⟩9. ∃N′, Σ′_{N} s.t. ⟨⟨(N_{2} l′) ; Σ_{N}[l′ ↦ N_{1}]⟩⟩ →_{sto}^{∗} ⟨⟨N′ ; Σ′_{N}⟩⟩ and ⟨⟨N′′ ; Σ′′_{N}⟩⟩ ≲_{sim}

⟨⟨N′ ; Σ′_{N}⟩⟩ Proof: By steps ⟨4⟩8 and ⟨4⟩5 and Lemma 2.5.11, i.e. α_{loc} ⊆ ≲_{sim}.

⟨4⟩10. Q.E.D.

Proof: We have

⟨⟨M′ ; Σ′_{M}⟩⟩ α_{loc} ⟨⟨M′′ ; Σ′′_{M}⟩⟩ (≲_{sim} ∘ =_{pcf} ∘ ≲_{sim}) ⟨⟨N′′ ; Σ′′_{N}⟩⟩ ≲_{sim} ⟨⟨N′′ ; Σ′′_{N}⟩⟩

and α_{loc} ⊆ ≲_{sim} so we are done. ⟨3⟩2. Case: deref and update cases

are similar to the new case, without the need to use α_{loc}. We do need the property, which follows directly from confluence, that if M =_{pcf} N and M, N:ref (τ), then M →_{pcf}^{∗} l ⇒ N →_{pcf}^{∗} l.

Corollary 2.5.16 (full β for terms) If M =_{pcf} term N, M, N:τ, then M ≅_{∀C} N.

Proof: Immediate from Lemma 2.5.14.

It is easy to show that PCF reduction preserves extensional equivalence.

Lemma 2.5.17 =_{pcf} term ⊆ ≲_{ext}^{•} An easy coinduction.

2.5.6 Completeness of Leftmost Reduction

We show that if a state can reduce under unrestricted →_{sto}^{∗} to an I/O operation, then there is a leftmost reduction sequence which will get us to the same I/O operation, and the continuations will be in ≲_{sim}.

Definition 2.5.18 (→_{left,sto}^{∗}) The reduction operator →_{left,sto} always chooses the leftmost redex, if any. In particular, it will always choose to take a deref, update, or new step if it can.

We prove a slightly more general lemma, allowing start states to be within a sequence of PCF reductions of each other.

Lemma 2.5.19 If ⟨⟨M ; Σ_{M}⟩⟩ =_{pcf} state ⟨⟨N ; Σ_{N}⟩⟩ and ⟨⟨M ; Σ_{M}⟩⟩ →_{sto}^{∗} ⟨⟨io M′ ; Σ′_{M}⟩⟩, then ∃N′, Σ′_{N} such that

⟨⟨N ; Σ_{N}⟩⟩ →_{left,sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩, and
⟨⟨M′ ; Σ′_{M}⟩⟩ ≲_{sim} ⟨⟨N′ ; Σ′_{N}⟩⟩

Proof: By induction on the number of →_{sto} steps in the reduction sequence ⟨⟨M ; Σ_{M}⟩⟩ →_{sto}^{∗} ⟨⟨io M′ ; Σ′_{M}⟩⟩. ⟨1⟩1. Case: n = 0

Immediate by Lemma 2.5.15, i.e. =_{pcf} state ⊆ ≲_{sim}. ⟨1⟩2. Case: n > 0

Consider first step of lhs:

⟨⟨M ; Σ_{M}⟩⟩ →^{1}_{sto} ⟨⟨M′′ ; Σ′′_{M}⟩⟩ →^{n−1}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩:

⟨2⟩1. Case: first step is a PCF reduction

⟨⟨M′′ ; Σ′′_{M}⟩⟩ =_{pcf} ⟨⟨N ; Σ_{N}⟩⟩, and we get the desired result by IH(n − 1). ⟨2⟩2. Case: first step is leftmost store op ⟨3⟩1. Case: M = deref l M_{1} Assume: 1. Σ_{M}(l) = Q

2. Σ_{N}(l) = Q′

⟨3⟩2. Q =_{pcf} Q′

By ⟨⟨M ; Σ_{M}⟩⟩ =_{pcf} state ⟨⟨N ; Σ_{N}⟩⟩. ⟨3⟩3.

lhs =^{def} ⟨⟨deref l M_{1} ; Σ_{M}⟩⟩
→^{1}_{sto} ⟨⟨M_{1} Q ; Σ_{M}⟩⟩
→^{n−1}_{sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨3⟩4. ∃N′_{1} s.t. ⟨⟨N ; Σ_{N}⟩⟩ →_{pcf}^{∗} ⟨⟨deref l N′_{1} ; Σ_{N}⟩⟩ and M_{1} =_{pcf} N′_{1}

By M =_{pcf} N. ⟨3⟩5. ∃N_{1} s.t. ⟨⟨N ; Σ_{N}⟩⟩ →_{left,pcf}^{∗} ⟨⟨deref l N_{1} ; Σ_{N}⟩⟩ and M_{1} =_{pcf} N_{1}

By completeness of leftmost reduction for PCF and transitivity of =_{pcf} .

⟨3⟩6. rhs =^{def} ⟨⟨N ; Σ_{N}⟩⟩

→_{left,pcf}^{∗} ⟨⟨deref l N_{1} ; Σ_{N}⟩⟩
→^{1}_{left,sto} ⟨⟨N_{1} Q′ ; Σ_{N}⟩⟩
→_{left,sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ s.t.
⟨⟨M′ ; Σ′_{M}⟩⟩ ≲_{sim} ⟨⟨N′ ; Σ′_{N}⟩⟩

By IH(n − 1). ⟨2⟩3. Case: other leftmost store ops

are similar to deref case.

Lemma 2.5.20 (completeness of →_{left,sto}^{∗} w.r.t. ≲_{sim}) If ⟨⟨M ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨io M′ ; Σ′⟩⟩, then ∃M′′, Σ′′ such that

⟨⟨M ; Σ⟩⟩ →_{left,sto}^{∗} ⟨⟨io M′′ ; Σ′′⟩⟩, and

⟨⟨M′ ; Σ′⟩⟩ ≲_{sim} ⟨⟨M′′ ; Σ′′⟩⟩

Proof: immediate from preceding Lemma 2.5.19 and reflexivity of =_{pcf} .

2.5.7 Substitution Lemma for PCF

A substitution lemma for PCF is used in [Pit99] and proved in [JM91]. Given standardization, the proof of the substitution lemma is a straightforward induction on the number of steps by the left-hand side in a standard reduction to a constant.

Lemma 2.5.21 (Substitution Lemma for PCF and ≲_{ext}^{•}) For non-pr base type o, closed terms M, N of type τ and open term P such that x:τ ⊢ P:o, if M ≲_{ext}^{•} N:τ, then

P [M/x] ≲_{ext}^{•} P [N/x]:o.

Proof: Recall that at base types other than pr, two terms are in ≲_{ext}^{•} iff they PCF-reduce to the same constant. We use induction on the length of a standard reduction to a constant, by considering all possible forms of P. The induction hypothesis is:

IH(n) = if P [M/x] →^{n}_{left,pcf} c, then P [N/x] →_{pcf}^{∗} c

We give a few of the cases: ⟨1⟩1. Case: P = c. Immediate. ⟨1⟩2. Case: P = x

It must be that τ = o, so by M ≲_{ext}^{•} N:τ, we have co-PCF-reduction to the same constant. ⟨1⟩3. Case: P = (λy.P_{0}) P_{1} … P_{k}, y ≠ x

⟨2⟩1. lhs \begin{matrix}→_{β} P_{0}[P_{1}[M/x]/y] P_{2}[M/x] … P_{k}[M/x] \\ = (P_{0}[P_{1}/y] P_{2} … P_{k})[M/x] \\ →^{n−1}_{left,pcf} c \end{matrix}

⟨2⟩2. rhs \begin{matrix}→_{β} P_{0}[P_{1}[N/x]/y] P_{2}[N/x] … P_{k}[N/x] \\ = (P_{0}[P_{1}/y] P_{2} … P_{k})[N/x] \\ →_{pcf}^{∗} c \end{matrix}

by IH(n − 1).

Other cases are similarly straightforward.

2.5.8 Contextual Equivalence with Empty Stores

If the terms we are considering are location-free, it suffices to show (bi)simulation starting with an empty store.

Lemma 2.5.22 If Γ ⊢ M, N:τ and if M and N contain no locations, then Γ ⊢ M ≅_{∀C} N:τ iff for all closing contexts C[−_{τ}] of type pr that respect Γ,

⟨⟨C[M] ; ∅⟩⟩ ≈_{sim} ⟨⟨C[N] ; ∅⟩⟩

Proof:

(⇒) Immediate from the definition of ≅_{∀C}.

(⇐) Suppose the lemma is not true. In that case, we have that for all closing contexts

C[−_{τ}] of type pr that respect Γ,

⟨⟨C[M] ; ∅⟩⟩ ≈_{sim} ⟨⟨C[N] ; ∅⟩⟩

yet there must exist some context C′ and store Σ such that

⟨⟨C′[M] ; Σ⟩⟩ ≉_{sim} ⟨⟨C′[N] ; Σ⟩⟩

Let the locations in Σ be {l_{1}, …, l_{n}} with contents {M_{1}, …, M_{n}}. Let {z_{1}, …, z_{n}} be n fresh variables of the appropriate types. Define a context C′′ as follows:

C′′ =^{def} new Ω_{1} (λz_{1}…. new Ω_{n} (λz_{n}. update z_{1} M_{1}(… update z_{n} M_{n} C′′′[−_{τ}]) …))

where Ω_{i} has the type of M_{i} and where C′′′[] is obtained from C′[] by replacing every occurrence of l_{i} in C′[] by z_{i}. After about 2n steps, ⟨⟨C′′[M] ; ∅⟩⟩ gets into a state which is identical to ⟨⟨C′[M] ; Σ⟩⟩ (recall that new can choose the location returned, as long as the location is fresh). The same reasoning holds for the right-hand side, ⟨⟨C′′[N] ; ∅⟩⟩. Thus the state context ⟨⟨C′′[] ; ∅⟩⟩ distinguishes M and N – contradiction.

Note that if M and N have locations in them, this lemma does not hold. It could be that the only way to distinguish some such M and N is with a store with exactly those locations set which occur in M and N. Attempting to create such a store from the empty store cannot work, because locations created by new are guaranteed not to occur in the terms.

2.6 Substitution Lemmas for the Metalanguage

We are now ready to prove two substitution lemmas for the metalanguage – one for substitution within states and one for substitution on terms. We present the proofs of these lemmas in quite a lot of detail, for several reasons:

1. The substitution lemmas are important, and we want a high degree of confidence that they have been correctly proven,

2. Both the coinductive and inductive steps in the proofs are very similar to steps used in many other proofs in this thesis. In later sections, we may give proofs in less detail, referring to the following proofs for guidance.

3. This is, after all, a doctoral thesis, and we are more concerned with completeness and correctness than brevity.

Lemma 2.6.1 (Substitution in States) If x:τ′ ⊢ Q:pr and M ≲_{ext}^{•} N:τ′, then for all stores Σ,

⟨⟨Q[M/x] ; Σ⟩⟩ ≲_{sim} ⟨⟨Q[N/x] ; Σ⟩⟩.

Proof sketch: We define a relation S_{pr}^{∗} on metalanguage states and show that S_{pr}^{∗} ⊆ ≲_{sim}. What we actually show is that

S_{pr}^{∗} ⊆ [≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}]_{sim},

which implies S_{pr}^{∗} ⊆ ≲_{sim} by Lemma 2.5.3.

Proof: Let:

S_{pr}^{∗} =^{def} \{(⟨⟨P ; Σ⟩⟩[M/x], ⟨⟨P ; Σ⟩⟩[N/x]) | \begin{matrix}x:τ′ ⊢ P:pr and \\ fv(rng(Σ)) ⊆ \{x\} \end{matrix}

} for all terms P and stores Σ

where substitution is extended to stores by mapping a substitution over the range of a store. ⟨1⟩1. S_{pr}^{∗} ⊆ [≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}]_{sim}

Assume: 1. (⟨⟨P ; Σ⟩⟩[M/x], ⟨⟨P ; Σ⟩⟩[N/x]) ∈ S_{pr}^{∗}

2. ⟨⟨P ; Σ⟩⟩[M/x] →_{sto}^{∗} ⟨⟨io P′ ; Σ′⟩⟩

Prove: ∃P′′, Σ′′ such that 1. ⟨⟨P ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩, and

2. ⟨⟨P′ ; Σ′⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩.

⟨2⟩1. ∃n, P^{3}, Σ^{3} such that

⟨⟨P ; Σ⟩⟩[M/x] →^{n}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩ and
⟨⟨P′ ; Σ′⟩⟩ ≲_{sim} ⟨⟨P^{3} ; Σ^{3}⟩⟩

Proof: by Lemma 2.5.20, completeness of leftmost reduction. ⟨2⟩2. ∃P′′, Σ′′ such that

1. ⟨⟨P ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩, and

2. ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩. Proof sketch: We construct an induction measure (n, b) where n is the number of steps in the leftmost reduction sequence and b = 0 if the head of P is x and b = 1 otherwise. (n, b) < (n′, b′) if either n < n′ or (n = n′ and b < b′). Let:

IH(n, b) =^{def} if ⟨⟨P ; Σ⟩⟩[M/x] →^{n,b}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩
then ∃P′′, Σ′′ s.t.
∧ ⟨⟨P ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩
∧ ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

We prove the induction hypothesis by considering all possible forms of P (which necessarily covers cases where n = 0, n > 0, b = 0, and b = 1). The possible forms of P are:

1. xP_{1} … P_{k}, k >= 0  2. (λy.P_{0})P_{1} … P_{k}, k > 0
3. io P_{1}  4. new P_{1}P_{2}
5. deref P_{1}P_{2}  6. update P_{1}P_{2}P_{3}

7. other PCF head redexes

⟨3⟩1. Case: P = xP_{1} … P_{k}, k >= 0

Given: ⟨⟨xP_{1} … P_{k} ; Σ⟩⟩[M/x] →^{n,1}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

Prove: ∃P′′, Σ′′ s.t. ⟨⟨xP_{1} … P_{k} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩

and ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: ⟨4⟩1. left-hand side reduces:

⟨⟨x P_{1} … P_{k} ; Σ⟩⟩[M/x] = ⟨⟨M P_{1} … P_{k} ; Σ⟩⟩[M/x]

→^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

⟨4⟩2. ∃P^{4}, Σ^{4} such that ⟨⟨MP_{1} … P_{k} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P^{4} ; Σ^{4}⟩⟩

and ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P^{4} ; Σ^{4}⟩⟩ Proof: by IH(n, 0) and ⟨4⟩1.

⟨4⟩3. ∃P′′, Σ′′ such that ⟨⟨NP_{1} … P_{k} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩

and ⟨⟨P^{4} ; Σ^{4}⟩⟩ ≲_{sim} ⟨⟨P′′ ; Σ′′⟩⟩ Proof: By M ≲_{ext}^{•} N:τ′.

⟨4⟩4. Q.E.D.

Note that ⟨⟨xP_{1} … P_{k} ; Σ⟩⟩[N/x] = ⟨⟨NP_{1} … P_{k} ; Σ⟩⟩[N/x].

We have:

⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P^{4} ; Σ^{4}⟩⟩ ≲_{sim} ⟨⟨P′′ ; Σ′′⟩⟩

⟨3⟩2. Case: P = (λy.P_{0})P_{1} … P_{k}, k > 0

Given: ⟨⟨(λy.P_{0})P_{1} … P_{k} ; Σ⟩⟩[M/x] →^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

Prove: ∃P′′, Σ′′ such that ⟨⟨(λy.P_{0})P_{1} … P_{k} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩ and

⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: ⟨4⟩1. Left-hand side reduces:

⟨⟨(λy.P_{0})P_{1} … P_{k} ; Σ⟩⟩[M/x] = ⟨⟨(λy.P_{0}[M/x])P_{1}[M/x] … P_{k}[M/x] ; Σ[M/x]⟩⟩

→^{1}_{left,sto} ⟨⟨(P_{0}[M/x][P_{1}/y])P_{2}[M/x] … P_{k}[M/x] ;
Σ[M/x]⟩⟩

= ⟨⟨(P_{0}[P_{1}/y])P_{2} … P_{k} ; Σ⟩⟩[M/x]

→^{n−1,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

Note that in the future we will generally omit the distribution and abstraction of substitutions, explicitly shown in the second and fourth lines above, when there is no interesting interaction between substitution and other calculations.

⟨4⟩2. Right-hand side reduces:

\begin{matrix}⟨⟨(λy.P_{0})P_{1} … P_{k} ; Σ⟩⟩[N/x] \\ →_{pcf}^{1} & ⟨⟨(P_{0}[P_{1}/y])P_{2} … P_{k} ; Σ⟩⟩[N/x] \end{matrix}

⟨4⟩3. Q.E.D.

Proof: by IH(n − 1, 0). ⟨3⟩3. Case: P = io P_{1}

Given: ⟨⟨io P_{1} ; Σ⟩⟩[M/x] →^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩ Prove: ∃P′′, Σ′′ such that ⟨⟨io P_{1} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩

and ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: Immediate. The only steps that the left-hand side can take are internal PCF reductions, and by Lemma 2.5.15, ⟨⟨io P^{3} ; Σ^{3}⟩⟩ ≲_{sim} ⟨⟨io P_{1} ; Σ⟩⟩[M/x]. Choose P′′ = P_{1} and we have ⟨⟨io P^{3} ; Σ^{3}⟩⟩ ≲_{sim} ⟨⟨io P_{1} ; Σ⟩⟩[M/x] S_{pr}^{∗} ⟨⟨io P′′ ; Σ⟩⟩[N/x].

⟨3⟩4. Case: P = new P_{1}P_{2} Given: ⟨⟨new P_{1}P_{2} ; Σ⟩⟩[M/x] →^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩ Prove: ∃P′′, Σ′′ such that ⟨⟨new P_{1}P_{2} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩

and ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: ⟨4⟩1. Left-hand side reduces:

⟨⟨new P_{1}P_{2} ; Σ⟩⟩[M/x]

→^{1}_{left,sto} ⟨⟨(P_{2}l) ; Σ[l ↦ P_{1}]⟩⟩[M/x], l fresh w.r.t. M, P_{1}, P_{2}, Σ

→^{j<n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

⟨4⟩2. Let: l′ be fresh w.r.t. M, N, P_{1}, P_{2}, Σ

⟨4⟩3. ⟨⟨(P_{2}l) ; Σ[l ↦ P_{1}]⟩⟩[M/x]

α_{loc} ⟨⟨(P_{2}l′) ; Σ[l′ ↦ P_{1}]⟩⟩[M/x]
→^{j}_{left,sto} ⟨⟨io P^{4} ; Σ^{4}⟩⟩ s.t.
⟨⟨io P^{3} ; Σ^{3}⟩⟩ α_{loc} ⟨⟨io P^{4} ; Σ^{4}⟩⟩

By Lemma 2.5.10. ⟨4⟩4. Right-hand side reduces:

⟨⟨new P_{1}P_{2} ; Σ⟩⟩[N/x]

→_{sto} ⟨⟨(P_{2}l′) ; Σ[l′ ↦ P_{1}]⟩⟩[N/x]
→_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩ s.t.
⟨⟨P^{4} ; Σ^{4}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

By Step ⟨4⟩3 and IH(j). ⟨4⟩5. Q.E.D.

We have

⟨⟨P^{3} ; Σ^{3}⟩⟩ ≲_{sim} ⟨⟨P^{4} ; Σ^{4}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

by Lemma 2.5.11 (α_{loc} ⊆ ≲_{sim}). ⟨3⟩5. Case: P = deref P_{1}P_{2}

Given: ⟨⟨deref P_{1}P_{2} ; Σ⟩⟩[M/x] →^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩ Prove: ∃P′′, Σ′′ s.t. ⟨⟨deref P_{1}P_{2} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩

and ⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: ⟨4⟩1. Left-hand side reduces:

⟨⟨deref P_{1}P_{2} ; Σ⟩⟩[M/x] →_{pcf}^{∗} ⟨⟨deref lP_{2} ; Σ⟩⟩[M/x] for some l →^{1}_{left,sto} ⟨⟨(P_{2}Q) ; Σ⟩⟩[M/x], assuming Σ(l) = Q

→^{j<n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

⟨4⟩2. if P_{1}[M/x] →_{left,pcf}^{∗} l, then P_{1}[N/x] →_{pcf}^{∗} l Proof: By substitution lemma for PCF, Lemma 2.5.21. At ref types, ≲_{ext}^{•}-related terms coreduce to the same location constant.

⟨4⟩3. Right-hand side reduces:

⟨⟨deref P_{1}P_{2} ; Σ⟩⟩[N/x]

→_{pcf}^{∗} ⟨⟨deref lP_{2} ; Σ⟩⟩[N/x] by ⟨4⟩2
→_{sto} ⟨⟨(P_{2}Q) ; Σ⟩⟩[N/x]

⟨4⟩4. Q.E.D.

Proof: by IH(j, 0). ⟨3⟩6. Case: P = update P_{1}P_{2}P_{3}

Given: ⟨⟨update P_{1}P_{2}P_{3} ; Σ⟩⟩[M/x] →^{n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩ Prove: ∃P′′, Σ′′ such that

⟨⟨update P_{1}P_{2}P_{3} ; Σ⟩⟩[N/x] →_{sto}^{∗} ⟨⟨io P′′ ; Σ′′⟩⟩ and

⟨⟨P^{3} ; Σ^{3}⟩⟩ (≲_{sim} ∘ S_{pr}^{∗} ∘ ≲_{sim}) ⟨⟨P′′ ; Σ′′⟩⟩

Proof: ⟨4⟩1. Left-hand side reduces:

⟨⟨update P_{1}P_{2}P_{3} ; Σ⟩⟩[M/x]

→_{pcf}^{∗} ⟨⟨update lP_{2}P_{3} ; Σ⟩⟩[M/x]
→^{1}_{left,sto} ⟨⟨P_{3} ; Σ[l ↦ P_{2}]⟩⟩[M/x]
→^{j<n,0}_{left,sto} ⟨⟨io P^{3} ; Σ^{3}⟩⟩

⟨4⟩2. if P_{1}[M/x] →_{left,pcf}^{∗} l, then P_{1}[N/x] →_{pcf}^{∗} l

Proof: Again, by the substitution lemma for PCF, Lemma 2.5.21. ⟨4⟩3. Right-hand side reduces:

⟨⟨update P_{1}P_{2}P_{3} ; Σ⟩⟩[N/x]

→_{pcf}^{∗} ⟨⟨update lP_{2}P_{3} ; Σ⟩⟩[N/x] by ⟨4⟩2
→_{sto} ⟨⟨P_{3} ; Σ[l ↦ P_{2}]⟩⟩[N/x]

⟨4⟩4. Q.E.D.

Proof: by IH(j, 0). ⟨3⟩7. Case: other PCF head redexes

Are all similar to β case, step ⟨3⟩2. ⟨1⟩2. (⟨⟨Q[M/x] ; Σ⟩⟩, ⟨⟨Q[N/x] ; Σ⟩⟩) ∈ S_{pr}^{∗}

Because fv(rng(Σ)) = ∅ for any store component Σ of a well-formed state.

Lemma 2.6.2 (Substitution on Terms) If x:τ′ ⊢ Q:τ′′ and M ≲_{ext}^{•} N:τ′, then

Q[M/x] ≲_{ext}^{•} Q[N/x]:τ′′.

Proof sketch: We define a type-indexed family of relations S. We then show that for all types τ, S_{τ} ⊆ [S]_{ext} which implies that S ⊆ ≲_{ext}^{•}. Finally, we show that (Q[M/x], Q[N/x]) ∈ S. Proof: Let: S_{τ} =^{def} {(P [M/x], P [N/x]) | x:τ′ ⊢ P:τ}, for all types τ and terms P

S =^{def} ⋃_{τ} S_{τ}.

⟨1⟩1. S_{τ} ⊆ [S]_{ext}, for all τ Proof:

Consider the cases of type τ. For each τ, consider any pair,

(P [M/x], P [N/x]) ∈ S_{τ} :

⟨2⟩1. Case: int, bool, ref (τ′′)

Proof: We can show that P [M/x] ≲_{ext}^{•} P [N/x]:τ by appealing to the substitution lemma for PCF, Lemma 2.5.21.

⟨2⟩2. Case: α×β, α+β, α→β Proof: All three cases follow immediately from the definition of S. In particular, if M ≲_{ext}^{•} N:τ′, then it is immediate that:

(π_{1} P [M/x]) S_{α} (π_{1} P [N/x]),  for x:τ′ ⊢ P:α×β
(π_{2} P [M/x]) S_{β} (π_{2} P [N/x]),  for x:τ′ ⊢ P:α×β
(case P [M/x] P_{1} P_{2}) S_{γ} (case P [N/x] P_{1} P_{2}), for x:τ′ ⊢ P:α+β, and
(P [M/x] R) S_{β} (P [N/x] R)  for x:τ′ ⊢ P:α→β

for closed terms P_{1}, P_{2}, and R.

⟨2⟩3. Case: pr

By the definitions of S_{pr} and [−]_{ext}^{pr}, we must show: for all P s.t. x:τ′ ⊢ P:pr, for all stores Σ,

⟨⟨P [M/x] ; Σ⟩⟩ ≲_{sim} ⟨⟨P [N/x] ; Σ⟩⟩,

which is immediate by Lemma 2.6.1. ⟨1⟩2. S ⊆ ≲_{ext}^{•}

Proof: By coinduction. ⟨1⟩3. (Q[M/x], Q[N/x]) ∈ S ⟨1⟩4. Q.E.D.

2.7 Precongruence of the Extensional Preorder

Using the substitution lemma, we can prove the following precongruence property:

Lemma 2.7.1 (precongruence of ≲_{ext}) ≲_{ext} is a precongruence – that is, if Γ ⊢ M ≲_{ext} N:τ, then for all contexts C[−_{τ}] which respect Γ, if ∃Γ′, τ′ s.t. Γ′ ⊢ C[M], C[N]:τ′, then

Γ′ ⊢ C[M] ≲_{ext} C[N]:τ′.

Proof: To prove that ≲_{ext} is a precongruence, we need to show that ≲_{ext} is a preorder and is preserved by the six productions of the grammar for the metalanguage presented on Page 14: ⟨1⟩1. ≲_{ext} is a preorder

By Lemma 2.4.12. ⟨1⟩2. Case: Γ ⊢ n ≲_{ext} n:int ∀Γ, n

By reflexivity of ≲_{ext}. ⟨1⟩3. Case: Γ ⊢ l^{τ} ≲_{ext} l^{τ}:ref (τ) ∀Γ, l^{τ}

By reflexivity of ≲_{ext}.

⟨1⟩4. Case: if c:τ, then Γ ⊢ c ≲_{ext} c:τ ∀Γ

By reflexivity of ≲_{ext}. ⟨1⟩5. Case: if Γ ⊢ x:τ, then Γ ⊢ x ≲_{ext} x:τ

By reflexivity of ≲_{ext}. ⟨1⟩6. Case: if Γ, x:τ′ ⊢ M ≲_{ext} N:τ, then

Γ ⊢ (λx:τ′.M) ≲_{ext} (λx:τ′.N):τ′→τ

From the definition of ≲_{ext} and Lemma 2.5.17, namely that PCF reduction preserves extensional equivalence. closing substitutions.

⟨1⟩7. Case: if Γ ⊢ M ≲_{ext} M′:τ′→τ and Γ ⊢ N ≲_{ext} N′:τ′, then

Γ ⊢ (MN) ≲_{ext} (M′N′):τ.

We split this case into two subcases: ⟨2⟩1. Case: if Γ ⊢ M ≲_{ext} M′:τ′→τ, then for all closed N of type τ′,

Γ ⊢ (M N) ≲_{ext} (M′ N):τ

Follows from definition of ≲_{ext} at function type. ⟨2⟩2. Case: if Γ ⊢ N ≲_{ext} N′:τ′, then for all closed M′ of type τ′→τ,

Γ ⊢ (M′ N) ≲_{ext} (M′ N′):τ

Let: σ be a closing substitution for both sides.

Prove: (M′ N)σ ≲_{ext}^{•} (M′ N′)σ:τ

⟨3⟩1. Nσ ≲_{ext}^{•} N′σ:τ

By Γ ⊢ N ≲_{ext} N′:τ′.

⟨3⟩2. (M′ x)[(Nσ)/x] ≲_{ext}^{•} (M′ x)[(N′σ)/x]

By Substitution Lemma for terms, Lemma 2.6.2. ⟨3⟩3. Q.E.D.

Do substitution for x in step ⟨3⟩2 and lift σ outside application (M′ is closed). ⟨2⟩3. Q.E.D.

By transitivity of ≲_{ext}.

2.8 The Extensionality Theorem

Given that ≲_{ext} is a precongruence, the extensionality result we have been aiming for follows easily.

Theorem 2.8.1 (Extensionality)

Γ ⊢ M ≲_{ext} N:τ ⇔ Γ ⊢ M ≲_{∀C} N:τ

Proof: ⟨1⟩1. ⇒

Assume Γ ⊢ M ≲_{ext} N:τ. By the precongruence of ≲_{ext}, Lemma 2.7.1, for all contexts C[−_{τ}] of type pr which respect Γ, Γ ⊢ C[M] ≲_{ext} C[N]:pr. By the definition of ≲_{ext} at type pr, the result follows.

⟨1⟩2. ⇐ Assume: Γ ⊢ M ≲_{∀C} N:τ

That is, for all contexts C[−_{τ}]:pr and all stores Σ,

⟨⟨C[M] ; Σ⟩⟩ ≲_{sim} ⟨⟨C[N] ; Σ⟩⟩.

Prove: Γ ⊢ M ≲_{ext} N:τ

That is, for all closing substitutions σ,

Mσ ≲_{ext}^{•} Nσ:τ. That is, for all base types o, and type contexts T_{τ} [−]:o,

T_{τ} [Mσ] ≲_{o}^{•} T_{τ} [Nσ].

⟨2⟩1. For any closing substitution σ, ∃C_{σ} s.t.

(Mσ) ≲_{ext}^{•} (Nσ):τ ⇔ C_{σ}[M] ≲_{ext}^{•} C_{σ}[N]:τ

Proof: It is easy to construct contexts to capture free variables with the same terms (after β) as σ. By Lemma 2.5.17, β-reduction preserves ≲_{ext}^{•}.

⟨2⟩2. C_{σ}[M] ≲_{∀C} C_{σ}[N]:τ

Proof: By Γ ⊢ M ≲_{∀C} N:τ and the fact that ≲_{∀C} is a precongruence (by definition). ⟨2⟩3. C_{σ}[M] ≲_{∀C} C_{σ}[N]:τ ⇒ C_{σ}[M] ≲_{ext}^{•} C_{σ}[N]:τ Assume: For all contexts C[−_{τ}]:pr and stores Σ,

⟨⟨C[C_{σ}[M]] ; Σ⟩⟩ ≲_{sim} ⟨⟨C[C_{σ}[N]] ; Σ⟩⟩

Prove: For all base types o and type contexts T_{τ} [−]:o,

T_{τ} [C_{σ}[M]] ≲_{o}^{•} T_{τ} [C_{σ}[N]]

Proof: For o = pr, result is immediate. For other base types, we must construct contexts of type pr which distinguish PCF reduction to different base values. Consider int type:

Let: C_{int} =^{def}

{(if (n =_{int} C_{σ}[−])(write 1 stop)(write 0 stop)) | n an integer} ⟨3⟩1. For any T_{τ} [−]:int

T_{τ} [C_{σ}[M]] ≲_{int}^{•} T_{τ} [C_{σ}[N]] ⇔
∀C_{n} ∈ C_{int}, Σ . ⟨⟨C_{n}[M] ; Σ⟩⟩ ≲_{sim} ⟨⟨C_{n}[N] ; Σ⟩⟩

Proof: which is true by assumption. Other base types are similar to int. For ref (τ) types, we can distinguish different location constants with eq?_{loc}^{τ}.

We now present a useful property of the metalanguage which follows easily from extensionality and other previous results.

2.8.1 Extensional Equivalence at Sum Types

At sum types, there is an alternative method for showing extensional equivalence, using the injection operators rather than case.

Proposition 2.8.2 If M, N:α+β, then M ≲_{ext}^{•} N:α+β iff

1. if M →_{pcf}^{∗} (inl M′), then ∃N′ s.t. N →_{pcf}^{∗} (inl N′) and M′ ≲_{ext}^{•} N′:α, and 2. if M →_{pcf}^{∗} (inr M′), then ∃N′ s.t. N →_{pcf}^{∗} (inr N′) and

M′ ≲_{ext}^{•} N′:β.

Proof:

(⇒) In each case, N must reduce to the correct form, (inl N′) or (inr N′), as it easy to construct a counterexample to the assumption that the terms are in ≲_{ext}^{•} (e.g. at type γ = pr) otherwise. Result follows from Extensionality (Theorem 2.8.1) and from the fact that PCF reduction preserves ≅_{∀C} (Lemma 2.5.16).

(⇐) Consider each type γ. Result follows by precongruence of ≲_{ext}, Lemma 2.7.1. For example, in pr case we end up needing to show ⟨⟨P_{1}M′ ; Σ⟩⟩ ≲_{sim} ⟨⟨P_{1}N′ ; Σ⟩⟩ with M′ ≲_{ext} N′, which follows from precongruence of ≲_{ext}. As another example, in the function case, we end up needing to show something like ((P_{1}M′)P_{3}) ≲_{ext} ((P_{1}N′)P_{3}), which again follows from the precongruence of ≲_{ext}.

Examples from the Literature

In this chapter, we work through some examples from the literature. The exercise of doing these examples serves two main purposes: first, it allows our methods to be compared to others; second, these examples are short and provide a good introduction in preparation for the more substantial applications presented in following chapters.

3.1 Some Meyer-Sieber Examples

The paper by Meyer and Sieber, [MS88], has long been a source of good test cases for proving the observable equivalence of program fragments in an imperative language. While much of the research which follows the Meyer-Sieber paper focuses on formalizing the stack discipline of Algol, e.g. [OT95], the examples given are suitable if only a heap is assumed for storage. We present the proofs of equivalence for two of their examples to demonstrate the application of our techniques.

3.1.1 Meyer-Sieber Example 1

The first example given by Meyer and Sieber is as follows:

The block below is replaceable simply by the call P. begin

new x;

P; % P is declared elsewhere end A straightforward CPS translation from this fragment of Algol to our metalanguage, where all blocks get translated to terms of type pr→pr, yields the following term for the block above:

[[lhs]] = (λκ:pr. new 0 (λx:ref (int).P κ)) The term takes a run-time continuation κ, allocates a fresh location, initializes the location to 0, binds the new location to x, and invokes the closed metalanguage term P with continuation κ. P must have type pr→pr. The translation of a call to P is simply P. The Extensionality Theorem says that to prove the two translations operationally equivalent we need only show that for all stores Σ and all closed terms K of type pr,

⟨⟨(λκ. new 0 (λx.P κ)) K ; Σ⟩⟩ ≈_{sim} ⟨⟨P K ; Σ⟩⟩

Because →_{sto}^{∗} preserves ≈_{sim}, we may reduce the left-hand side of the above equation:

[[lhs]] →_{sto}^{∗} ⟨⟨(P K)[l/x] ; Σ[l ↦ 0]⟩⟩  (l fresh)
= ⟨⟨(P K) ; Σ[l ↦ 0]⟩⟩  (P and K are closed)

which is the same as ⟨⟨P K ; Σ⟩⟩, up to a consistent renaming of locations (i.e. in α_{loc}, with partial bijection Θ = ∅). By Lemma 2.5.11, the two blocks are equivalent. Thus we are able to prove the equivalence of the first Meyer-Sieber example by simple calculation and direct use of a few properties of the metalanguage.

3.1.2 Meyer-Sieber Example 4

Example 4 from [MS88] is given as:

The block below always diverges. begin

new x; new y; procedure Twice; begin y := 2 ∗ contents(y) end; x:= 0; y:= 0; Q(T wice); % Q is declared elsewhere if contents(x) = 0 then diverge fi

end In a language with I/O, the above block is not necessarily equivalent to diverge, as the procedure Q might do I/O. So we will undertake to prove the equivalence of the following two blocks: begin

new x; new y; procedure Twice; begin y := 2 ∗ contents(y) end; x:= 0; y:= 0; Q(T wice); % Q is declared elsewhere if contents(x) = 0 then skip else diverge fi

end is operationally equivalent to: begin

new x; new y; procedure Twice; begin y := 2 ∗ contents(y) end; x:= 0; y:= 0; Q(T wice); % Q is declared elsewhere

end where skip does nothing.

A translation from Algol to our metalanguage gives us the following metalanguage term for the original block:

[[orig]] = (λκ:pr. new 0 (λx:ref (int). new 0 (λy:ref (int).
f_{Q} Twice (deref x (λv_{x}. zero? v_{x} κ Ω)))))

where Twice is defined as:

Twice =^{def} (λκ′:pr. deref y (λv_{y}. update y (∗ 2 v_{y}) κ′)) and where f_{Q} is a variable of type (pr→pr)→pr→pr. The [[orig]] term takes a run-time continuation κ, allocates fresh locations for x and y, initializes them to 0, and then continues with x and y bound to the fresh locations. The body of the block invokes whatever procedure is bound to f_{Q}, sending it Twice and a continuation which checks if x is zero, continues with κ if so and diverges if not. Twice, in which y will be bound to a location at run-time, takes a run-time continuation κ′, gets the current value of y, binds the value to v_{y}, then updates y with (2 ∗ v_{y}) and continues with κ′. The entire block has type pr→pr. The translation of the replacement block, [[repl]], is exactly the same as [[orig]], except that the (deref x …) continuation is replaced by simply κ. To prove that the two translations are operationally equivalent, we appeal to the Extensionality Theorem and set out to prove that for all terms K of type pr→pr, all closing substitutions [Q/f_{q}] and all stores Σ,

⟨⟨[[orig]][Q/f_{q}] K ; Σ⟩⟩ ≈_{sim} ⟨⟨[[repl]][Q/f_{q}] K ; Σ⟩⟩

The left-hand side of the above equation will take a number of steps to the following state: ⟨⟨(Q Twice (deref x (λv_{x}. zero? v_{x} K Ω)))[l_{x}/x, l_{y}/y] ;

Σ[l_{x} ↦ 0, l_{y} ↦ 0]⟩⟩ (l_{x}, l_{y} fresh) Similarly, the right-hand side goes to:

\begin{matrix}⟨⟨(Q Twice K)[l_{x}/x, l_{y}/y] ; \\ Σ[l_{x} ↦ 0, l_{y} ↦ 0]⟩⟩ \end{matrix}

Actually, the locations might be different on the two sides but the metalanguage theory allows us to ignore differences up to α_{loc}. We now construct a candidate simulation relation S, which includes the two states above, and we prove that S is indeed a simulation.

S =^{def} { (⟨⟨M ; Σ⟩⟩σ_{1}, ⟨⟨M ; Σ⟩⟩σ_{2}) |
fv(M, rng(Σ)) ⊆ {z},
σ_{1} = (deref l_{x} (λv_{x}. zero? v_{x} K Ω))/z,
σ_{2} = K/z,
Σ(l_{x}) = 0,
l_{x} ∉ locs(M, K, rng(Σ)) }

The pair of states in which we are interested is clearly in S, with M = (QTwice z). Because l_{x} is allocated fresh, we know that Q and K contain no references to l_{x}. The proof that S is indeed a simulation is a straightforward coinduction – namely, we prove that S ⊆ [S]_{sim}. The proof of inclusion for each clause in the definition of [−]_{sim} is by induction on the length of a standard reduction of the left-hand side to an I/O operator. The cases where M is of the form (update M_{1}M_{2}M_{3}) or (deref M_{1}M_{2}), and M_{1} PCF-reduces to a location constant l, are handled by appealing to the definition of S to show that l ≠ l_{x}. In the new and update cases, the (deref l_{x} …) term on the left-hand side can make its way into the store, which necessitates allowing z in the free variables of the store and applying the substitutions to the store as well as the term. For the case where M is headed by the free variable z, both sides reduce quickly to K. The simulation S characterizes the relevant aspects of the Meyer-Seiber example being considered – namely that x’s location l_{x} is never updated (or, more exactly, that the only references to l_{x} are within a term of the form (deref l_{x} …)). The fact that Twice sets y to twice its current value is unimportant, as is whether or not Q actually calls Twice or whether Q modifies other locations in the store.

3.2 Examples from Ian Stark

In his thesis, [Sta94], Ian Stark outlines a small language called the nu-calculus which adds dynamic names to the simply-typed lambda calculus. A rich theory of the nu-calculus is developed, using category theory and logical relations. The methods for reasoning within the nu-calculus are then applied to a more realistic language called Reduced ML, which supports integer reference types, and several example equivalences are presented. Many of the Reduced ML examples are inspired by the Meyer-Sieber examples. We work through one of the more interesting examples, which we call “count-up-count-down”.

3.2.1 Count-up, Count-down

Example 10 in [Sta94][Ch. 5, Sec. 4] is similar to an example used by O’Hearn and Tennent in [OT95] and demonstrates representation independence – in this case of a simple counter. let val r = ref 0 in

fn(x : int) ⇒ (r :=!r + x; !r) end is operationally equivalent at type int → int to: let val r = ref 0 in

fn(x : int) ⇒ (r :=!r − x; −!r) end Both blocks return a function which maintains a running total of the integers to which it has been applied. The second implementation, though, perversely maintains its counter as a negative value. Barring issues of signed integer representations and overflow, the two implementations should be operationally equivalent.

A straightforward CPS translation from the first Reduced ML fragment above yields the following metalanguage term:

[[orig]] =(λκ. new 0 (λr.κ (λxκ′. deref r
(λv_{r}. update r (v_{r} + x) (deref r κ′)))))

whereas the translation of the negatively-disposed fragment gives us:

[[repl]] =(λκ. new 0 (λr.κ (λxκ′. deref r
(λv_{r}. update r (v_{r} − x) (deref r (λv_{r}.κ′ (−v_{r})))))))

For all continuation terms K and all stores Σ, the two terms behave as follows: ⟨⟨[[orig]] K ; Σ⟩⟩ →_{left,sto}^{∗} ⟨⟨K L ; Σ[l_{r} ↦ 0]⟩⟩, where L = (λxκ′. deref r(λv_{r}. update r (v_{r} + x) (deref r κ′))) and ⟨⟨[[repl]] K ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨K R ; Σ[l_{r} ↦ 0]⟩⟩, where R = (λxκ′. deref r(λv_{r}. update r (v_{r} − x)(deref r (λv_{r}.κ′ (−v_{r}))))) The obvious candidate simulation relation which characterizes the relationship maintained between the two sides as they run is as follows:

S =^{def} {(⟨⟨M ; Σ_{1}⟩⟩σ_{1}, ⟨⟨M ; Σ_{2}⟩⟩σ_{2}) |
σ_{1} = [L/z], σ_{2} = [R/z], fv(M, rng(Σ_{1}, Σ_{2})) ⊆ {z}
l_{r} ∉ locs(M, rng(Σ_{1}, Σ_{2})),
Σ_{1}(l_{r}) = −Σ_{2}(l_{r})}

The states we are interested in are clearly in S, with M = (Kz), and it is a straightforward to prove S a simulation. The only interesting case is when M = z M_{1} M_{2}, with M_{1}:int, and in this case both sides clearly stay in S. It is also easy to show that all ref-typed subterms never PCF-reduce to l_{r}, by the constraint on locations in the definition of S.

64 CHAPTER 3. EXAMPLES FROM THE LITERATURE

Twobit Optimizations: An Exercise

in Almost Denotational Semantics

Many well-known and widely studied transformation methods have not been proved to be correct, and it seems that the correctness problem has received little attention because of an implicit (and incorrect) assumption that it is sufficient to argue the correctness at the level of the basic steps.

– David Sands [San96]

In this and the two following chapters, we detail the use of our metalanguage to prove the correctness of several source-to-source transformations for the Scheme programming language. The transformations we consider are representative of a wide class of optimizations used in compilers for Scheme and for other functional programming languages. The Twobit Scheme compiler [CH94] by Will Clinger and Lars Hansen provides the actual code we use as a basis for our definitions of the transformations.

4.1 Motivation

One of Scheme’s most notable features is a long-standing and well-developed denotational semantics for the language [Cli84, CR91, IEE91]. The denotational semantics, which we will refer to as the R^{n}RS semantics, has been useful in providing a formal basis to guide implementors of the language. However, many universally accepted contextual equivalences are false in the standard denotational semantics [CR91, Section 7.2]. There are several reasons that the denotational semantics for Scheme cannot equate such contextual equivalences:

1. The initial continuation for evaluation of Scheme programs is not defined,

2. The domain of answers is undefined,

3. The evaluation of constants is not defined.

As a simple example, consider the Scheme expressions

\begin{matrix}e_{1} = ((lambda (x) x) e) \\ e_{2} = e \end{matrix}

which we would expect to be contextually equivalent. In the R^{n}RS semantics, a Scheme expression e evaluates to E[[e]], which is a function from environments ρ, expression continuations κ, and stores σ, to answers. According to the R^{n}RS semantics, E[[e_{1}]] evaluates e, getting an expressed value, say v, then puts that v in the store at some location, say α, then retrieves v from the store at address α and sends it to the expression’s continuation. E[[e_{2}]], on the other hand, evaluates e and sends the value to the continuation, doing no store allocation or access (for x anyway). The important thing to keep in mind is that the continuation of E[[e_{1}]] is run in a different store than the continuation of E[[e_{2}]]. A sufficiently nasty continuation can distinguish the two situations:

κ = (λϵ^{∗}σ.(σ(α | L) ↓ 2) → wrong, unspecified)

The continuation κ looks at the “initialized” flag of the specific location α, and if it has been initialized it halts. Of course it may be that the evaluation of e to v allocates location α in both sides, in which case the two sides will behave the same. However, in the case where α is the location allocated for the x in e_{1}, the two sides will be different and are therefore not equivalent.

4.2 Overview

A notable aspect of the set of optimizations we prove correct is that they are orderdependent. That is, later optimizations rely on earlier optimizations having taken place. We factor the suite of optimizations into a series of source-to-source and language-to-language transformations. Each transformation is shown to preserve operational behavior. The optimizations we prove correct – in particular assignment elimination – translate the source Scheme program into a different intermediate language. This is representative of many, if not all, compiler implementations. Intermediate languages chosen for translation from source languages will typically have the following characteristics:

1. Redundant constructions in the source language will map to the same intermediate language construct, and

2. There will be specialized constructs in the intermediate language whose use represents derived information about the input program. For example, if the source language supports generic arithmetic but the compiler knows that two values will always be integers, the intermediate language might support integer-specific arithmetic functions. In assignment elimination, the intermediate language Scheme_{cell} distinguishes between value-bound and location-bound variables, whereas the source language, Scheme, does not.

The framework presented in this chapter handles this important technique of translation from the source programming language to an intermediate language, and then possibly to another intermediate language, and so on. The task of proving a sequence of transformations and translations correct can be presented abstractly as follows. Suppose that we have a set of languages, L_{1}, …, L_{n}, with L_{1} being the source programming language. We have a corresponding series of language-to-language transformations, xform_{i,j} which transform language L_{i} into language L_{j}. Finally, for each language L_{i}, we have a translation [[−]]_{i} from L_{i} into our metalanguage. We must show that the following diagram commutes:

[figure: L_{1}; [[−]]_{1}; _{xform_{1,2}}; metalanguage; _{≅_{∀C}}; L_{2}; [[−]]_{2}; _{xform_{2,3}}; metalanguage; _{≅_{∀C}}; L_{3}; [[−]]_{3}; metalanguage]

Twobit makes clever use of Scheme as its own intermediate code, with successive passes and optimizations producing correct, runnable Scheme. The use of a single syntax for multiple intermediate languages reduces the number of data structures that must be manipulated by a compiler, but has no theoretical significance. In our case, we are free to use successive intermediate languages, each with its own semantics (i.e. translation to the metalanguage), for successive transformations, so we need no such cleverness.

4.3 Translation from Scheme to Metalanguage

The syntax of the subset of Scheme with which we will be concerned initially is given by the grammar in Figure 7. The language consists of expressions e and programs p. Figure 8 contains a compositional, call-by-value translation from the Scheme subset into the metalanguage. The resulting metalanguage terms are in continuation passing style (CPS). The translation is a standard CPS translation – see [FWH92, App92, Sto77] for introductions to CPS. We use a “natural” model, without an explicit environment. Free variables in expressions are left free in the translation, with type ref (Val). As demonstrated

e ::= x | n | (lambda (x …) e) | (e e …) expressions
| (set! x e) | (letrec ((x e) …) e)
p ::= run e  programs

where x ranges over identifiers and n ranges over integers.

Figure 7: A subset of Scheme

in [Wan90], this setup is equivalent to the more common environment model, such as is used in [Cli84], where the type of an environment would be Locs→ref (Val). We use ⟨−, …, −⟩ and listref_{i} for the evident list operations. The helper function checkargs :int→Val^{∗}→pr→pr checks that the list of values is of the correct length and stops if not. The type Val of expressed values is the recursive sum type of expressed values:

Val = N + F  expressed values
N = int  integers
F = Val^{∗}→(Val→pr)→pr procedures

The denoted values are of type ref (Val). For each summand S of the Val type, we include CPS injection and extraction combinators, in_{S} :S→(Val→pr)→pr and out_{S} :Val→(S→pr)→pr. For example, the in_{N} function can be defined as:

in_{N} =^{def} (λn:int.λκ:Val→pr.κ (inl_{N+F} n))

The out_{S} functions invoke an error (print a number and halt) if the argument is not of the correct type (checked with the case construction). For example, the out_{N} function can be defined as:

out_{N} =^{def} (λv:Val.λκ:int→pr. case v κ (λf:F. error))

The rule for integers in Figure 8 simply injects the appropriate integer into the Val type. The rule for an abstraction (lambda (x_{1} … x_{n}) e) injects into the Val type a closure which takes a list of values v and a continuation κ′. When the closure is invoked at function [[n]]_{scm} = λκ:Val→pr. in_{N} n κ [[x]]_{scm} = λκ:Val→pr. deref x κ [[(lambda (x_{1} … x_{n}) e)]]_{scm} = λκ:Val→pr.

in_{F} (λv^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs n v^{∗})

new^{Val}(listref_{1} v^{∗}) (λx_{1}:ref (Val). · · ·

new^{Val}(listref_{n} v^{∗}) (λx_{n}:ref (Val).[[e]]_{scm} κ′) …)) κ

[[(e_{0} e_{1} … e_{n})]]_{scm} = λκ:Val→pr.[[e_{0}]]_{scm}(λf:Val.

[[e_{1}]]_{scm}(λv_{1}:Val. · · ·

[[e_{n}]]_{scm}(λv_{n}:Val.
out_{F} f (λf′:Val^{∗}→(Val→pr)→pr.
f′ ⟨v_{1}, …, v_{n}⟩ κ)) …))

[[(set! x e)]]_{scm} = λκ:Val→pr.[[e]]_{scm}(λv:Val. update x v (κ Ω_{Val})) [[(letrec ((x_{1} e_{1}) … (x_{n} e_{n})) e)]]_{scm} = λκ:Val→pr.

new Ω_{Val}(λx_{1}:ref (Val)…. new Ω_{Val}(λx_{n}:ref (Val).

[[e_{1}]]_{scm}(λv_{1}:Val. update x_{1}v_{1} ⋯

[[e_{n}]]_{scm}(λv_{n}:Val. update x_{n}v_{n} ([[e]]_{scm}κ) ⋯))))

[[(run e)]]_{scm} = ⟨⟨C_{0}[[[e]]_{scm}] ; ∅⟩⟩ Figure 8: CPS translation from Scheme subset to metalanguage application time, n new locations are allocated, each fresh location is initialized to an element of v and bound to the corresponding identifier x_{i}, and the body of the closure is run with κ′ as its continuation. The arguments x_{i} correspond to locations in memory in order to allow for later assignments to x_{i} via expressions of the form set! x_{i} . . .. It is the elimination of this allocation overhead whenever possible which is the goal of the assignment elimination transformation. The rule for application (e_{0} e_{2} … e_{n}) first extracts the closure from the value of [[e_{0}]]_{scm} and then sends to that closure the list of values ⟨v_{1}, …, v_{n}⟩ resulting from [[e_{1}]]_{scm}, …, [[e_{n}]]_{scm} as well as the current continuation, κ. The rule for assignment, (set! x e), updates the location bound to x with the value of [[e]]_{scm}. The Scheme semantics calls for the continuation to be invoked with an undefined value, for which we use Ω_{Val}, the canonical nonterminating term^{1}. The rule for recursive definitions, (letrec ((x_{1} e_{1}) … (x_{n} e_{n})) e) first allocates all required locations, initializing them to a dummy value, and then updates all of the locations with their contents within a scope which includes bindings from all mutually recursive identifiers (x_{1} … x_{n}) to their newly allocated locations. This definition follows the official semantics, which initializes the variables to undefined values while building up the scope (var/loc pairs) and then destructively updates the variables to their correct values. Because the expressions e_{1}, …, e_{n} may have side effects, letrec cannot be implemented using the Y operator. Evaluation of a program, (run e), runs the expression e with an empty store and in a context, C_{0}, which loads the values of Scheme primitives into the store, binds the primop identifiers to the fresh locations, and then runs e in an initial continuation, such as (λv:Val.print_{Val}v stop), for a suitable function print_{Val}. This definition is sufficiently general to handle primitives which do I/O or non-local jumps, such as call-cc. The translation of any expression has type (Val→pr)→pr, given that all the free variables have type ref (Val):

1for example, (Y^{Val}(λx:Val.x))

Lemma 4.3.1 For a Scheme expression e and a type assignment Γ such that if x ∈ fv(e) then Γ(x) = ref (Val),

Γ ⊢ [[e]]_{scm}:(Val→pr)→pr

Proof: Structural induction on e.

4.4 Equivalence of Scheme Expressions

For an optimization which replaces Scheme expression e_{1} by e_{2} to be correct in general, we must show that the two expressions behave the same in all Scheme program contexts. From the definition in Figure 8 of what it means to run a Scheme program, we get the following definition:

Definition 4.4.1 (≅_{∀C}^{scm}) Scheme expressions e_{1} and e_{2} are operationally equivalent, denoted e_{1} ≅_{∀C}^{scm} e_{2} iff for all Scheme contexts C_{scm}[−], and for all initial contexts C_{0}.

⟨⟨C_{0}[[[C_{scm}[e_{1}]]]_{scm}] ; ∅⟩⟩ ≈_{sim} ⟨⟨C_{0}[[[C_{scm}[e_{2}]]]_{scm}] ; ∅⟩⟩  (1)

We will generally use the following relation to prove the equivalence of two Scheme expressions:

Definition 4.4.2 (≅_{scm}) For Scheme expressions e_{1} and e_{2}, e_{1} ≅_{scm} e_{2} iff for all closing substitutions σ, all closed terms K of type Val→pr, and all stores Σ,

⟨⟨([[e_{1}]]_{scm}σ) K ; Σ⟩⟩ ≈_{sim} ⟨⟨([[e_{2}]]_{scm}σ) K ; Σ⟩⟩

It is a straightforward calculation to show that the two relations are equivalent:

Lemma 4.4.3 For Scheme expressions e_{1} and e_{2},

e_{1} ≅_{∀C}^{scm} e_{2} ⇔ e_{1} ≅_{scm} e_{2}

Proof:

e_{1} ≅_{∀C}^{scm} e_{2} ⇔ ∀C_{0}, C_{scm} .

⟨⟨C_{0}[[[C_{scm}[e_{1}]]]_{scm}] ; ∅⟩⟩ ≈_{sim} ⟨⟨C_{0}[[[C_{scm}[e_{2}]]]_{scm}] ; ∅⟩⟩

by Definition 4.4.1

⇔ ∀C[−_{(Val→pr)→pr}]:pr .
⟨⟨C[[[e_{1}]]_{scm}] ; ∅⟩⟩ ≈_{sim} ⟨⟨C[[[e_{2}]]_{scm}] ; ∅⟩⟩

because C_{0} is unspecified

⇔ ∀C, Σ . ⟨⟨C[[[e_{1}]]_{scm}] ; Σ⟩⟩ ≈_{sim} ⟨⟨C[[[e_{2}]]_{scm}] ; Σ⟩⟩ by Lemma 2.5.22

⇔ ∀closing σ, K:Val→pr, stores Σ .

⟨⟨([[e_{1}]]_{scm}σ) K ; Σ⟩⟩ ≈_{sim} ⟨⟨([[e_{2}]]_{scm}σ) K ; Σ⟩⟩

by Extensionality Theorem, Theorem 2.8.1

⇔ e_{1} ≅_{scm} e_{2}

by Definition 4.4.2.

4.5 Why Types are Needed in Target Metalanguage

It is instructive to try a translation from Scheme to an untyped version of our metalanguage and see what happens. Scheme is a dynamically-typed language, and the R^{n}RS denotational semantics is given in an untyped lambda calculus, so it would seem natural to use an untyped extended lambda calculus as the target metalanguage. This is in fact what we did originally, and we were able to prove extensionality for an untyped variant of the metalanguage used in this thesis. We were disappointed, though, to find that some simple desired equivalences did not turn out to be equivalences using our untyped metalanguage. Following is a simple example of an equivalence which should, but does not, hold after translation to an untyped metalanguage. The two source expressions we wish to show equal are e_{1} and e_{2}, defined below:

e_{1} =^{def} 42

e_{2} =^{def} ((lambda (x) 42) 0)

The untyped metalanguage has integer constants, and the translation of an integer n is simply (λκ.κ n). So the translation of e_{1} is (λκ.κ 42). The translation of e_{2} is β-equal to:

(λκ. new 0 (λx.κ 42))

In order to prove operational equivalence, we invoke extensionality and attempt to show both translations equivalent in all applicative contexts. Consider the applicative context [−] (λvκ.κ v) (λv. write v stop): The translation of e_{1}, inserted into the above context, proceeds as follows, in a state with store Σ: ⟨⟨(λκ.κ 42) (λvκ.κ v) (λv. write v stop) ; Σ⟩⟩ →_{pcf}^{∗} ⟨⟨write 42 stop ; Σ⟩⟩ →^{!42,√}_{io} ⟨⟨stopped ; Σ⟩⟩ The translation of e_{2} proceeds as follows, starting with store Σ: ⟨⟨(λκ. new 0 (λx.κ 42)) (λvκ.κ v) (λv. write v stop) ; Σ⟩⟩ →_{pcf}^{∗} ⟨⟨new 0 (λx.(λκ.κ 42)) (λv. write v stop) ; Σ⟩⟩ and there is no transition for states with a term component of the form

new n M_{1} M_{2}

so the state “hangs”. Thus the two sides are not operationally equivalent. This comes about, in a sense, because the continuation terms are not of the right form for the translation we use. This problem is addressed by adding types to the metalanguage and insisting that all extensional contexts be well-typed. When we use the typed version of the metalanguage, and the translation [[−]]_{scm} given in Figure 8, the translation of e_{1} is:

[[e_{1}]]_{scm} = λκ:Val→pr. in_{N} n κ

The translation of e_{2} β-reduces to the following:

[[e_{2}]]_{scm} →_{pcf}^{∗} λκ:Val→pr. new 0 (λx:ref (Val).κ 42)

By Extensionality, Theorem 2.8.1, to show [[e_{1}]]_{scm} ≅_{∀C} [[e_{2}]]_{scm} we must show that for all closed metalanguage terms K of type Val→pr and for all stores Σ,

⟨⟨[[e_{1}]]_{scm} K ; Σ⟩⟩ ≲_{sim} ⟨⟨[[e_{2}]]_{scm} K ; Σ⟩⟩

Assuming that integers are put into the left summand of the Val type, the translation of e_{1} reduces as follows:

⟨⟨[[e_{1}]]_{scm} K ; Σ⟩⟩ →_{pcf}^{∗} ⟨⟨K (inl 42) ; Σ⟩⟩

The translation of e_{2} does some (useless) store allocation and reduces as follows:

⟨⟨[[e_{2}]]_{scm} K ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨K (inl 42) ; Σ[l ↦ 0]⟩⟩

with location l fresh w.r.t. [[e_{2}]]_{scm}, K, and Σ. The two states are easily shown to be in α_{loc} (with an empty partial bijection), and by Lemma 2.5.11 (α_{loc} ⊆ ≲_{sim}), we get the desired equivalence.

76 CHAPTER 4. TWOBIT OPTIMIZATIONS

Assignment Elimination – A

Language-to-Language Translation

In Scheme, all bound variables may be side-effected, and therefore the Scheme semantics [CR91] allocates storage for all bound variables. Many Scheme compilers, e.g. [KKR^{+}86], perform a pass called Assignment Elimination in order to avoid unnecessary allocation of storage for variables which are never mutated. Assignment elimination identifies those variables which may be side-effected, explicitly allocates “cells” for those variables, and replaces all operations on those variables with cell operations. All variables deemed immutable are then bound to expressed values at run-time. We need a language in which we can distinguish value-bound (immutable) and cell-bound (mutable) variables, and for that purpose we introduce the intermediate language Scheme_{cell}.

5.1 Intermediate Language Scheme_{cell}

The target language of assignment elimination is an intermediate language we call Scheme_{cell}, whose syntax is given in Figure 9. Scheme_{cell} has no set! operation but does have operations for cell creation, reference, and update. This language is similar to the untyped example

e ::= x | n | (lambda (x …) e) | (e e …)
| (let ((x rhs) …) e)
| (letrec ((x e) …) e)
| (cell-ref x) | (cell-set! x e)
rhs ::= x | (make-cell e)

Figure 9: Syntax of Scheme_{cell}

language featured in the work by Talcott et al. [HMST95], which has explicit cell operations. The storage model, where location-bound variables are explicit, is similar to that of ML. There is only one syntactic class of variables, but the variables themselves will be bound to either values or cells. We impose a simple type-checking system to ensure that variables are used consistently – i.e., if a variable is cell-bound, then all references and updates to it are encased in cell-ref and cell-set! constructions. Figure 10 gives the typing rules for Scheme_{cell}. The rule for a lambda-expression shows that we treat lambda-bound variables as immutable values. The last two rules guarantee the consistency of the let-bound variables and their uses in the let-bodies. Note that the let of Figure 9 corresponds to let* in Scheme. The semantics of Scheme_{cell} are given by a translation into our metalanguage. Figure 11 defines the translation [[−]]_{cell} from Scheme_{cell} to the metalanguage. Expressed values are still of type Val; identifiers denote either values of type Val or cells, which are of type ref (Val). The rule for variables no longer needs to dereference a location. The rule for abstraction no longer allocates storage for parameters. The rules for let state that binding a variable to another variable is simply renaming, whereas binding a variable to the result of a (make-cell e) operation does allocation at run-time, storing the result of [[e]]_{cell} in the fresh location. The rules for integers, application, and letrec are the same as in [[−]]_{scm}. We can be assured that if we apply the translation [[−]]_{cell} to well-typed Scheme_{cell} terms,

Γ ⊢_{cell} n:ok  \frac{Γ(x) = ref (Val) Γ ⊢_{cell} e:ok}{Γ ⊢_{cell} (cell-set! x e):ok}

\frac{Γ[x_{i}:Val]_{i=1}^{n} ⊢_{cell} e:ok}{Γ ⊢_{cell} (lambda (x_{1} … x_{n}) e):ok}

\frac{Γ ⊢_{cell} e_{1}:ok … Γ ⊢_{cell} e_{n}:ok}{Γ ⊢_{cell} (e_{1} … e_{n}):ok}

\frac{Γ(x) = ref (Val)}{Γ ⊢_{cell} (cell-ref x):ok}  \frac{Γ(x) = Val}{Γ ⊢_{cell} x:ok}
\frac{Γ ⊢_{cell} e:ok}{Γ ⊢_{cell} (let () e):ok}

\frac{Γ(x) = Val Γ[x_{1}:Val] ⊢_{cell} (let ((x_{2} rhs_{2}) … (x_{n} rhs_{n})) e):ok}{Γ ⊢_{cell} (let ((x_{1} x) (x_{2} rhs_{2}) … (x_{n} rhs_{n})) e):ok}

\frac{Γ ⊢_{cell} e_{1}:ok Γ[x_{1}:ref (Val)] ⊢_{cell} (let ((x_{2} rhs_{2}) … (x_{n} rhs_{n})) e):ok}{Γ ⊢_{cell} (let ((x_{1} (make-cell e_{1})) (x_{2} rhs_{2}) … (x_{n} rhs_{n})) e):ok}

Figure 10: Type Checking for Scheme_{cell} [[x]]_{cell} = λκ:Val→pr.κ x [[(lambda (x_{1} … x_{n}) e)]]_{cell} = λκ:Val→pr.

in_{F} (λv^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs n v^{∗})

[[e]]_{cell}[(listref_{1} v^{∗})/x_{1}, …, (listref_{n} v^{∗})/x_{n}] κ′) κ

[[(let ((x_{1} x) (x_{2} rhs_{2}) … (x_{n} rhs_{n})) e)]]_{cell} =

[[(let ((x_{2} rhs_{2}) … (x_{n} rhs_{n})) e)]]_{cell}[x/x_{1}]

[[(let ((x_{1} (make-cell e_{1})) (x_{2} rhs_{2}) … (x_{n} rhs_{n})) e)]]_{cell} =

[[e_{1}]]_{cell}(λv_{1}:Val. new v_{1} (λx_{1}:ref (Val).

[[(let ((x_{2} rhs_{2}) … (x_{n} rhs_{n})) e)]]_{cell}))

[[(let () e)]]_{cell} = [[e]]_{cell} [[(cell-ref x)]]_{cell} = λκ:Val→pr. deref x κ [[(cell-set! x e)]]_{cell} = λκ:Val→pr.[[e]]_{cell}(λv:Val. update x v (κ Ω)))

Figure 11: CPS translation from Scheme_{cell} to metalanguage

the resultant metalanguage terms will be well-typed:

Lemma 5.1.1 For a Scheme_{cell} term e, and a type assumption Γ mapping variables to {Val, ref (Val)},

Γ ⊢_{cell} e:ok ⇒ Γ ⊢ [[e]]_{cell}:(Val→pr)→pr

Proof: Structural induction on ⊢_{cell}.

It should be noted that it is straightforward to write implementations of make-cell, cell-ref, and cell-set! in the original Scheme dialect which are operationally equivalent in the original semantics to the same operators in Scheme_{cell} under the second translation. By supplying such function definitions, the Twobit Scheme compiler is able to produce runnable Scheme code as it transforms the original Scheme code into the new Scheme_{cell} language. This trick is useful for debugging, among other things, but is not relevant to our correctness proofs.

5.2 The Assignment Elimination Transformation

Figure 12 defines the assignment-elimination transformation. The transformation AE(e) takes a Scheme expression e and produces a Scheme_{cell} expression. As AE(e) transforms expression e, a set V is maintained of the variables which will correspond to {V}aluebound (i.e. never side-effected) values in the output Scheme_{cell} term. So AE(V, e) is the translation of Scheme expression e assuming that the variables in V will be treated as immutable values at run-time and do not need to be stored in cells. The translation of a top-level expression assumes no immutable variables have yet been discovered, so AE(e) = AE(∅, e). An invariant of the transformation is that for every AE(V, e′) encountered during a transformation AE(e) of a Scheme expression e, V ⊆ fv(e′). The translation of a value-bound (immutable) variable x (i.e., x ∈ V) is simply x. However, if x is not in V, x is assumed mutable and thus a reference to x must be translated to (cell-ref x). An update of a variable x is translated to (cell-set! x …). Because membership in V by x is based on the absence of set! x subexpressions, and because we start the AE transformation with an empty V, we expect that if the rule for AE(V, (set! x e)) applies, then x ∉ V. The rule for a lambda expression first determines which of its bound variables are updated in its body, using the sv function. For each mutable local variable x_{i} returned by sv, AE emits a let (x_{i} (make-cell x_{i})) binding. Immutable local variables (i.e. those not returned by sv) are added to the V used to transform the body of the lambda, so that references to those variables will not be surrounded by cell operations. Finally, the rule for letrec treats all letrec-bound variables as mutable. Note that in the simple case that e = (lambda (x) e′), V ⊇ fv(e), and there are no set!’s or letrec’s in e, then AE(V, e) is the identity transformation (up to some let ((x x)) bindings). If, however, e contains some updates to x, the transformation of e will bind x to (make-cell x) and all references and updates of x will be enclosed in (cell-ref x) and (cell-set! x) constructions. More formally, we can prove that for any Scheme expression e, AE(e) produces a Definition 5.2.1 (Assignment Elimination (AE)) Let sv(e) be the set of free variables of e that appear in e as the left-hand side of a set! expression. Define AE(e) to be AE(∅, e), where AE(V, e) is defined as follows. Here V is the set of free variables that are to be bound to values rather than locations.

AE(V, x) = \{ \begin{matrix}x & if x ∈ V \\ (cell-ref x) & if x ∉ V \end{matrix}
AE(V, (set! x e)) = (cell-set! x AE(V, e))
AE(V, (e_{0} e_{1} … e_{n})) = (AE(V, e_{0}) AE(V, e_{1}) … AE(V, e_{n}))
AE(V, (lambda (x_{1} … x_{n}) e))
= (lambda (x_{1} … x_{n}) (let ((x_{1} r_{1}) … (x_{n} r_{n})) AE(V′, e)))

where \{ \begin{matrix}r_{i} = \{ \begin{matrix}(make-cell x_{i}) & if x_{i} ∈ sv(e) \\ x_{i} & if x_{i} ∉ sv(e) \end{matrix} \\ V′ = V ∪ \{x_{i} | x_{i} ∉ sv(e)\} − \{x_{i} | x_{i} ∈ sv(e)\} \end{matrix}

AE(V, (letrec ((x_{1} e_{1}) … (x_{n} e_{n})) e))
= (letrec ((x_{1} AE(V′, e_{1})) … (x_{n} AE(V′, e_{n})))
AE(V′, e)) where V′ = V − {x_{1}, …, x_{n}}

Figure 12: Assignment Elimination well-typed Scheme_{cell} expression:

Lemma 5.2.2 For any Scheme expression e, and for a type assignment Γ such that if x ∈ fv(e) then Γ(x) = ref (Val),

Γ ⊢_{cell} AE(e):ok

Proof: Structural induction on e.

For any given Scheme program, there is some number, say n, of lambda-expressions: (lambda (x_{1,1}, …, x_{1,m_{1}}) e_{1})

⋯ (lambda (x_{n,1}, …, x_{n,m_{n}}) e_{n}) In the following sections, we use the following notation to refer to the relevant parts of each lambda-expression:

X_{i} = ⟨x_{i,1}, …, x_{i,m_{i}}⟩  (sequence of parameters)
C_{i} = sv(e_{i}) ∩ X_{i}  (set of {C}ell-bound local variables)
V_{i} = X_{i} − C_{i}  (set of {V}alue-bound local variables)

For the length of a sequence X we write #X. For the j^{th} element of a sequence X we write X_{(j)}; for a sequence such as X_{i}, we write X_{i(j)}.

5.3 Correctness of Assignment Elimination

We prove the assignment elimination transformation is meaning-preserving. That is, for any Scheme expression e,

[[e]]_{scm} ≅_{∀C} [[AE(e)]]_{cell}

Our goal is to build a candidate simulation relation between metalanguage states which characterizes the syntactic differences between (non-transformed) Scheme programs and those programs after assignment elimination, as they reduce under →^{α}_{io}. In the ensuing analysis, we find that there are several different ways in which corresponding subterms can differ:

1. The translations of Scheme lambda-expressions will differ in the bodies of their closures. The original closure body will contain new operators for all local parameters, whereas the transformed body will only allocate storage for mutable local parameters. In the original, references to local variables always involve store lookup with the deref operator, whereas after transformation, references to immutable variables will not do store lookup, as the variable will get its value via substitution.

2. When subterms corresponding to lambda-expressions are applied to a run-time continuation, they are injected into the F summand of the Val type and sent to the continuation.

3. When the closures are used at run-time (i.e., applied to arguments), they are extracted from the Val type and applied to their application-time argument list and continuation. At this point, the differences between the closure bodies are “exposed”, and we see different storage behavior.

4. As the exposed bodies of corresponding closures reduce, the original term allocates storage for all local variables, whereas the transformed term only allocates storage for mutable local variables. For immutable local variables, in the original term we have a substitution [l_{i}/x_{i}] for each immutable variable x_{i} (and mutable too, for that matter). In the transformed term, for the immutable variables x_{i}, we see value substitutions [(listref_{i} v^{∗})/x_{i}], where the variable v^{∗} contains the list of incoming arguments.

Figure 13 presents specifications for, and definitions of, macros to capture the syntactic differences described in items 1-3 above. The macros L_{1} and R_{1} express the initial differences between the translations of a lambda-expression and of its transformed version.

Initial Translation:

[[(lambda (x_{1} … x_{m}) e)]]_{scm} = L_{1}⟨x_{1} … x_{m}⟩[[ [[e]]_{scm} ]] [[AE(V, (lambda (x_{1} … x_{m}) e))]]_{cell} = R_{1}(V′, C)[[ [[AE(V′, e)]]_{cell} ]], with

V′ = V ∪ \begin{matrix}\{x_{i} | x_{i} ∉ sv(e)\}− \\ \{x_{i} | x_{i} ∈ sv(e)\} \end{matrix}

C = {x_{i} | x_{i} ∈ sv(e)}

L_{1}⟨x_{1} … x_{m}⟩[[P]] =^{def}

(λκ:Val→pr. in_{F} (λv^{∗}:Val^{∗}.

λκ′:Val→pr.(checkargs m v^{∗})

new^{Val}(listref_{1} v^{∗}) (λx_{1}:ref (Val).

⋯

new^{Val}(listref_{m} v^{∗}) (λx_{m}:ref (Val). (P κ′)) …)) κ)

R_{1}(V, C)[[P]] =^{def}

(λκ:Val→pr. in_{F} (λv^{∗}:Val^{∗}.

λκ′:Val→pr.(checkargs m v^{∗})

\begin{matrix}new^{Val}(listref_{i} v^{∗}) \\ (λx_{i}:ref (Val). \end{matrix}\} \begin{matrix}for each \\ x_{i} ∈ C \end{matrix}

((P [(listref_{i} v^{∗})/x_{i}]_{x_{i}∈V}) κ′) …)) κ)

Applied to a continuation K:

\begin{matrix}⟨⟨(L_{1}⟨x_{1} … x_{m}⟩[[P]] K) ; Σ⟩⟩ →_{pcf}^{∗} \\ ⟨⟨(K L_{2}⟨x_{1} … x_{m}⟩[[P]]) ; Σ⟩⟩ \end{matrix}  \begin{matrix}⟨⟨(R_{1}(V, C)[[P]] K) ; Σ⟩⟩ →_{pcf}^{∗} \\ ⟨⟨(K R_{2}(V, C)[[P]]) ; Σ⟩⟩ \end{matrix}

L_{2}⟨x_{1} … x_{m}⟩[[P]] =^{def}

inr(λv^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m v^{∗})

new^{Val}(listref_{1} v^{∗}) (λx_{1}:ref (Val).

⋯ new^{Val}(listref_{m} v^{∗}) (λx_{m}:ref (Val).

(P κ′) …)))

R_{2}(V, C)[[P]] =^{def}

inr(λv^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m v^{∗})

\begin{matrix}new^{Val}(listref_{i} v^{∗}) \\ (λx_{i}:ref (Val). \end{matrix}\} \begin{matrix}for each \\ x_{i} ∈ C \end{matrix}

((P [(listref_{i} v^{∗})/x_{i}]_{x_{i}∈V}) κ′) …))

Closure Applied to an Argument List Q:

⟨⟨ out_{F} (L_{2}⟨x_{1} … x_{m}⟩[[P]])

(λf:Val^{∗}→(Val→pr)→pr.

f Q K) ; Σ⟩⟩ where Q:Val^{∗} and K:Val→pr →_{pcf}^{∗} ⟨⟨L_{3}⟨x_{1} … x_{m}⟩[[P, Q, K]] ; Σ⟩⟩ ⟨⟨ out_{F} (R_{2}(V, C)[[P]])

(λf:Val^{∗}→(Val→pr)→pr.

f Q K) ; Σ⟩⟩ where Q:Val^{∗} and K:Val→pr →_{pcf}^{∗} ⟨⟨R_{3}(V, C)[[P, Q, K]] ; Σ⟩⟩

L_{3}⟨x_{1} … x_{m}⟩[[P_{1}, P_{2}, P_{3}]] =^{def}

new^{Val}(listref_{1} P_{2}) (λx_{1}:ref (Val).

⋯ new^{Val}(listref_{m} P_{2}) (λx_{m}:ref (Val).

(P_{1} P_{3}) …)))

R_{3}(V, C)[[P_{1}, P_{2}, P_{3}]] =^{def}

\begin{matrix}new^{Val}(listref_{i} P_{2}) \\ (λx_{i}:ref (Val). \end{matrix}\} \begin{matrix}for each \\ x_{i} ∈ C \end{matrix}

((P_{1} [(listref_{i} P_{2})/x_{i}]_{x_{i}∈V}) P_{3}) …)

Figure 13: Definitions of L_{i}, R_{i} macros The macros L_{2} and R_{2} express the syntactic forms of the original and transformed terms after having been applied to a continuation term K. The definitions of L_{2} and R_{2} assume that closures go into the right summand of the Val type. Macros L_{3} and R_{3} describe the two versions of the lambda-expression after having been applied to an argument list Q of type Val^{∗} and a continuation K of type Val→pr. For two states where the head redexes of the term components of both states correspond to L_{3} and R_{3} terms, we can see that the left-hand side will allocate new locations for each local parameter x_{1}, …, x_{m}. The right-hand side, however, will allocate new storage only for the mutable local variables (listed in C) and will use substitution for the immutable variables (listed in V). Thus, at run-time, the storage behavior of the two sides will differ, with the right-hand side doing potentially less memory allocation than the left-hand side. All of the macro definitions, L_{i}, R_{i} (i = 1, 2, 3), are parameterized by the metalanguage terms for the closure bodies. The terms for closure bodies will differ at subterms that correspond to references to immutable parameters. In the original term, all references correspond to a store lookup, whereas in the transformed term, references to immutable variables are translated as variables that are substituted-for at closure application time. The relation ⇝^{AE}_{V}, defined in Figure 14, between metalanguage terms formalizes the differences between translations of immutable variable references. The subscript V is a list of variables that are treated as values in the transformed term. The Γ in the judgement Γ ⊢ M ⇝^{AE}_{V} N:τ corresponds to the type environment needed to prove that M has type τ. Two metalanguage terms related by ⇝^{AE}_{V} will differ only in their treatment of non-mutated bound variables, specified by the set V, and if every assignment in Γ of x ∈ V to ref (Val) is replaced by an assignment x:Val, the term N will have type τ as well. In other words:

5.3. CORRECTNESS OF ASSIGNMENT ELIMINATION 87

⇝^{AE}_{V} is the least relation between metalanguage terms closed under the following rules

Γ ⊢ n ⇝^{AE}_{V} n:int (cong-int)
Γ ⊢ c ⇝^{AE}_{V} c:τ  (τ from Figure 1) (cong-const)
Γ ⊢ l^{τ} ⇝^{AE}_{V} l^{τ}:ref (τ) (cong-loc)
\frac{Γ[x:τ′] ⊢ M ⇝^{AE}_{V} N:τ x ∉ V}{Γ ⊢ (λx:τ′.M) ⇝^{AE}_{V} (λx:τ′.N):τ′→τ} (cong-abs)
\frac{Γ ⊢ M ⇝^{AE}_{V} M′:τ′→τ Γ ⊢ N ⇝^{AE}_{V} N′:τ′}{Γ ⊢ (M N) ⇝^{AE}_{V} (M′ N′):τ} (cong-app)
\frac{x ∉ V Γ(x) = τ}{Γ ⊢ x ⇝^{AE}_{V} x:τ} (mutable-var)
\frac{Γ ⊢ M ⇝^{AE}_{V} N:Val→pr x ∈ V Γ(x) = ref (Val)}{Γ ⊢ (deref x M) ⇝^{AE}_{V} (N x):pr} (immutable-var)
Figure 14: Definition of ⇝^{AE}_{V}

Lemma 5.3.1 If V = {x_{1}, …, x_{n}} and Γ[x_{i}:ref (Val)]_{i=1}^{n} ⊢ M:τ, then

Γ[x_{i}:ref (Val)]_{i=1}^{n} ⊢ M ⇝^{AE}_{V} N:τ ⇒ Γ[x_{i}:Val]_{i=1}^{n} ⊢ N:τ

Proof: By induction on the structure of M.

The notation Γ[x_{i}:τ]_{i=1}^{n} is shorthand for the type environment Γ[x_{1}:τ, …, x_{n}:τ]. The relation ⇝^{AE}_{V} between terms is preserved by substitution by (⇝^{AE}_{V})-related terms for variables not in V:

Lemma 5.3.2 If Γ[x:τ′] ⊢ M ⇝^{AE}_{V} N:τ and Γ ⊢ P ⇝^{AE}_{V} P′:τ′ and x ∉ V, then

Γ ⊢ M[P/x] ⇝^{AE}_{V} N[P′/x]:τ

Proof:

Assume: Γ ⊢ P ⇝^{AE}_{V} P′:τ′

Proceed by induction on the structure of the proof of

Γ ⊢ M[P/x] ⇝^{AE}_{V} N[P′/x]:τ.

⟨1⟩1. Case: immutable-var

Assume: 1. M ≡ deref y M′ 2. N ≡ N′ y

3. y ∈ V

4. Γ[x:τ′] ⊢ M′ ⇝^{AE}_{V} N′:Val→pr

5. Γ(y) = ref (Val)

⟨2⟩1. Γ[x:τ′] ⊢ M′[P/x] ⇝^{AE}_{V} N′[P′/x]:Val→pr

By IH.

⟨2⟩2. Γ ⊢ M[P/x] ⇝^{AE}_{V} N[P′/x]:pr

By immutable-var. ⟨1⟩2. Case: (cong-app)

Assume: 1. M ≡ M′ M′′

2. N ≡ N′ N′′

⟨2⟩1. Γ ⊢ M′[P/x] ⇝^{AE}_{V} N′[P′/x]:α→β

By IH.

⟨2⟩2. Γ ⊢ M′′[P/x] ⇝^{AE}_{V} N′′[P′/x]:α

By IH.

⟨2⟩3. Γ ⊢ M[P/x] ⇝^{AE}_{V} N[P′/x]:β

By (cong-app). ⟨1⟩3. All other cases are similarly straightforward.

Consider a pair of states in which the term component of the left-hand side is L_{3}(X)[[P_{1}, P_{2}, P_{3}]], and on the right-hand side we have R_{3}(V′, C)[[P′_{1}, P′_{2}, P′_{3}]]. Further assume that the corresponding “closure body” terms are related by ⇝^{AE}_{V}; that is, Γ ⊢ P_{i} ⇝^{AE}_{V} P′_{i}:pr for 1 ≤ i ≤ 3, where V′ ⊆ V and C ∩ X = ∅. As the states reduce, both sides will do allocation – the left-hand side will allocate storage for all of its local variables, and the right-hand side will only allocate storage for its mutable local variables. The term components start in ⇝^{AE}_{V} but do not stay in ⇝^{AE}_{V}. On the left-hand side, the immutable variables x_{i} will be replaced by location constants, whereas on the right-hand side, the immutable variables will be replaced by actual values. Thus, where we started with ⇝^{AE}_{V} -related terms such as Γ ⊢ (deref x M) ⇝^{AE}_{V} (N x):pr, we now have terms such as (deref l_{x} M) ⇝̸^{AE}_{V} (N Q_{x}), where in the store component of the left-hand side, at location l_{x}, we expect a term related to Q_{x}. The relation ⇝^{AE}_{V |Z} between metalanguage terms, defined in Figure 15, characterizes the differences between terms which were originally related by ⇝^{AE}_{V} but which have been subjected to run-time substitutions – of locations for variables on the left-hand side and of values for variables on the right-hand side.

Definition 5.3.3 (⇝^{AE}_{V |Z} for metalanguage terms) For V = ⟨x_{1}, …, x_{n}⟩, Z = ⟨(l_{1}, P_{1}), …, (l_{k}, P_{k})⟩,

Γ ⊢ M ⇝^{AE}_{V |Z} N:τ ⇔

∧ k ≤ n

∧ Γ(x_{i}) = ref (Val), for 1 ≤ i ≤ n
∧ P_{i}:Val, for 1 ≤ i ≤ k
∧ ∃M′, N′ s.t.

∧ M = M′[l_{1}/x_{1}, …, l_{k}/x_{k}] ∧ N = N′[P_{1}/x_{1}, …, P_{k}/x_{k}]

∧ Γ ⊢ M′ ⇝^{AE}_{V} N′:τ

Definition 5.3.4 (⇝^{AE}_{V |Z} for stores)

Γ ⊢ Σ′_{M} ⇝^{AE}_{V |Z} Σ_{N} ⇔

∧ dom(Σ′_{M}) = dom(Σ_{N})

∧ ∀τ, l^{τ} ∈ dom(Σ′_{M}) . Γ ⊢ Σ′_{M}(l) ⇝^{AE}_{V |Z} Σ_{N}(l):τ

Figure 15: The Relations ⇝^{AE}_{V |Z} between Terms and Stores

5.3.1 The Assignment Elimination Simulation Relation

Figure 16 defines a candidate simulation relation, S_{AE} , by abstracting over corresponding pairs of terms which differ as outlined earlier. Each of the distinct ways in which corresponding metalanguage subterms might differ is handled by a substitution pair (σ_{L}^{i}, σ_{R}^{i}). The substitutions σ_{L}^{i} and σ_{R}^{i} have domains {u_{1}^{i}, …, u_{#σ^{i}}^{i}}, for 1 ≤ i ≤ 3. In σ_{L}^{1}, each u_{i}^{1} maps to a metalanguage term of the form L_{1}(X_{i}^{1})[[M_{i}^{1}]], whereas in σ_{R}^{1}, each u_{i}^{1} maps to a metalanguage term of the form R_{1}(V_{i}^{1}, C_{i}^{1})[[N_{i}^{1}]]. The terms corresponding to the closure bodies, M_{i}^{1} and N_{i}^{1}, must be related by ⇝^{AE}_{V |Z}. The substitution pairs (σ_{L}^{2}, σ_{R}^{2}) and (σ_{L}^{3}, σ_{R}^{3}) are similar, but abstract over pairs of terms of the forms (L_{2}, R_{2}), (L_{3}, R_{3}). The last section of the definition of S_{AE} requires all of the closure bodies to be ⇝^{AE}_{V |Z}- related. In order to simplify the notation, we assume that all of the bound variables in the states we consider are distinct. This allows us to have a single ⇝^{AE}_{V |Z} relation for the whole

S_{AE} =^{def} {(⟨⟨M_{0} ; Σ_{M}⟩⟩σ_{L}, ⟨⟨N_{0} ; Σ_{N}⟩⟩σ_{R}) | ∃Γ, Σ′_{M}, V, Z s.t.

σ_{L} = σ_{L}^{1} ∪ σ_{L}^{2} ∪ σ_{L}^{3}

σ_{R} = σ_{R}^{1} ∪ σ_{R}^{2} ∪ σ_{R}^{3}

fv(M_{0}, N_{0}, rng(Σ_{M}), rng(Σ_{N})) ⊆ {u_{1}^{1}, …, u_{n_{1}}^{1}, u_{1}^{2}, …, u_{n_{2}}^{2}, u_{1}^{3}, …, u_{n_{3}}^{3}}

\begin{matrix}(L_{1}, R_{1}) \\ pairs \end{matrix} \{ \begin{matrix}σ_{L}^{1} = [u_{1}^{1} ↦ L_{1}(X_{1}^{1})[[M_{1}^{1}]], …, u_{n_{1}}^{1} ↦ L_{1}(X_{n_{1}}^{1})[[M_{n_{1}}^{1}]]] \\ σ_{R}^{1} = [u_{1}^{1} ↦ R_{1}(V_{1}^{1}, C_{1}^{1})[[N_{1}^{1}]], …, u_{n_{1}}^{1} ↦ R_{1}(V_{n_{1}}^{1}, C_{n_{1}}^{1})[[N_{n_{1}}^{1}]]] \\ n_{1} = #σ_{L}^{1} = #σ_{R}^{1} \end{matrix}

\begin{matrix}(L_{2}, R_{2}) \\ pairs \end{matrix} \{ \begin{matrix}σ_{L}^{2} = [u_{1}^{2} ↦ L_{2}(X_{1}^{2})[[M_{1}^{2}]], …, u_{n_{2}}^{2} ↦ L_{2}(X_{n_{2}}^{2})[[M_{n_{2}}^{2}]]] \\ σ_{R}^{2} = [u_{1}^{2} ↦ R_{2}(V_{1}^{2}, C_{1}^{2})[[N_{1}^{2}]], …, u_{n_{2}}^{2} ↦ R_{2}(V_{n_{2}}^{2}, C_{n_{2}}^{2})[[N_{n_{2}}^{2}]]] \\ n_{2} = #σ_{L}^{2} = #σ_{R}^{2} \end{matrix}

\begin{matrix}(L_{3}, R_{3}) \\ pairs \end{matrix} \{ \begin{matrix}σ_{L}^{3} = [\begin{matrix}u_{1}^{3} ↦ L_{3}(X_{1}^{3})[[M_{1,1}^{3}, M_{1,2}^{3}, M_{1,3}^{3}]], …, \\ u_{n_{3}}^{3} ↦ L_{3}(X_{n_{3}}^{3})[[M_{n_{3},1}^{3}, M_{n_{3},2}^{3}, M_{n_{3},3}^{3}]]] \end{matrix} \\ σ_{R}^{3} = [\begin{matrix}u_{1}^{3} ↦ R_{3}(V_{1}^{3}, C_{1}^{3})[[N_{1,1}^{3} N_{1,2}^{3} N_{1,3}^{3}]], …, \\ u_{n_{3}}^{3} ↦ R_{3}(V_{n_{3}}^{3}, C_{n_{3}}^{3})[[N_{n_{3},1}^{3}, N_{n_{3},2}^{3}, N_{n_{3},3}^{3}]]] \end{matrix} \\ n_{3} = #σ_{L}^{3} = #σ_{R}^{3} \end{matrix}

Γ(u_{i}^{1}) = (Val→pr)→pr, Γ(u_{i}^{2}) = Val, Γ(u_{i}^{3}) = pr ∧ V = ⟨x_{1}, …, x_{n}⟩ ∧ Z = ⟨(l_{1}, P_{1}), …, (l_{k}, P_{k})⟩, k ≤ n s.t.

for each(M, N) ∈ {(M_{j}^{i}, N_{j}^{i})} ∪ {(M_{0}, N_{0})},

∧ Γ ⊢ M ⇝^{AE}_{V |Z} N:τ

∧ Σ_{M} = Σ′_{M}[l_{1} ↦ P′_{1}, …, l_{k} ↦ P′_{k}]

∧ Γ ⊢ Σ′_{M} ⇝^{AE}_{V |Z} Σ_{N}

∧ Γ ⊢ P′_{i} ⇝^{AE}_{V |Z} P_{i}:Val, 1 ≤ i ≤ k

}

Figure 16: Definition of S_{AE} simulation relation, rather than different V ’s and Z’s for different closures. We show that S_{AE} includes the translations of Scheme expressions before and after assignment elimination:

Lemma 5.3.5 For any Scheme expression e, any type assumption Γ such that Γ ⊢ [[e]]_{scm}:(Val→pr)→pr, any metalanguage context C[−_{(Val→pr)→pr}]:pr which respects Γ, and any store Σ,

⟨⟨C[[[e]]_{scm}] ; Σ⟩⟩ S_{AE} ⟨⟨C[[[AE(e)]]_{cell}] ; Σ⟩⟩

Proof: The Z in the ⇝^{AE}_{V |Z} relation will be ⟨⟩ (the empty sequence). The σ^{2} and σ^{3} substitutions will both be empty, and the σ^{1} substitutions will have elements for the translation of each lambda expression in e. The V in ⇝^{AE}_{V} will contain the immutable local variables of the lambda-expressions in e.

Before proving that S_{AE} is a simulation, we need a lemma about ref-typed terms:

Lemma 5.3.6 If Γ ⊢ M ⇝^{AE}_{V |Z} N:ref (τ), and (M, N) ∉ Z, then

M →_{pcf}^{∗} l ⇔ N →_{pcf}^{∗} l

Proof sketch: Let: 1. V = ⟨x_{1} … x_{n}⟩

2. Z = ⟨(l_{1}, P_{1}) … (l_{k}, P_{k})⟩, k ≤ n

3. Γ ⊢ M′ ⇝^{AE}_{V} N′:ref (Val) s.t.
4. M = M′[l_{i}/x_{i}]_{i=1}^{k}, N = N′[P_{i}/x_{i}]_{i=1}^{k}
5. M →^{s}_{left,pcf} l (by PCF standardization, Lemma 2.5.7)

We use induction on the length s of the leftmost reduction of M to a location l, considering all possible forms of M′. Most cases are ruled out: ⟨1⟩1. Case: M′ = x_{i}

is ruled out by (M, N) ∉ Z. ⟨1⟩2. Case: M′ = (deref …), or (update …) or (io …)

are ruled out by types. ⟨1⟩3. Case: M′ = l

By Γ ⊢ M′ ⇝^{AE}_{V} N′:ref (Val), and by (cong-loc) rule, we must have N′ = l = N. ⟨1⟩4. Case: all other cases

The “interesting” rule of Figure 14 is ruled out by the type of Γ ⊢ M′ ⇝^{AE}_{V} N′:ref (τ). Thus M′ and N′ are in ⇝^{AE}_{V}, at the top level, via a congruence rule. Because all of the store and I/O operators have been ruled out, that leaves head PCF redexes. We give the β redex case as an example. ⟨2⟩1. Case: M′ = (λx:τ′.M_{0}) M_{1} … M_{k}

We know that τ′ = τ_{1}→ … →τ_{k} and that Γ[x:τ′] ⊢ M_{0}:ref (τ). By repeated use of types, we argue that only (cong-app) and (cong-abs) rules apply and that therefore

Γ ⊢ M′ ⇝^{AE}_{V} N′:ref (Val) implies that N′ = (λx:τ′.N_{0})N_{1} … N_{k}, with Γ ⊢ M_{i} ⇝^{AE}_{V} N_{i}:τ_{i}

for 0 ≤ i ≤ k. So we have:

⟨3⟩1. \begin{aligned}lhs & = (λx.M_{0}) M_{1} … M_{k} \\ & =_{β} M_{0}[M_{1}/x] M_{2} … M_{k} \end{aligned}
⟨3⟩2. \begin{aligned}rhs & = (λx.N_{0}) N_{1} … N_{k} \\ & =_{β} N_{0}[N_{1}/x] N_{2} … N_{k} \end{aligned}

⟨3⟩3. Q.E.D.

By Lemma 5.3.2, and by the assumptions Γ ⊢ M_{i} ⇝^{AE}_{V} N_{i}:τ_{i} for 0 ≤ i ≤ k, we have that both sides are in ⇝^{AE}_{V}.

We are now ready to prove that the S_{AE} relation is contained in ≲_{sim}. What we actually prove is that

S_{AE} ⊆ [≲_{sim} ∘ S_{AE} ∘ ≲_{sim}]_{sim}  (2)

For example, it is often the case that we argue that two states are in S_{AE} up to α_{loc}. But by Lemma 2.5.11, we know that α_{loc} ⊆ ≲_{sim}, so we satisfy equation 2.

Lemma 5.3.7

S_{AE} ⊆ [≲_{sim} ∘ S_{AE} ∘ ≲_{sim}]_{sim}

Proof: Let: 1. (⟨⟨M ; Σ_{M}⟩⟩σ_{L}, ⟨⟨N ; Σ_{N}⟩⟩σ_{R}) ∈ S_{AE} ,

2. ⟨⟨M ; Σ_{M}⟩⟩σ_{L} →^{s}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

Prove: ∃N′, Σ′_{N} s.t. ⟨⟨N ; Σ′_{N}⟩⟩σ_{R} →_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ and

⟨⟨M′ ; Σ′_{M}⟩⟩ S_{AE} ⟨⟨N′ ; Σ′_{N}⟩⟩

Proof sketch: Use induction on length s of leftmost reduction, by considering all possible cases of (M, N). Most of the interesting cases correspond to M and N headed by a variable u_{j}^{i}. The other interesting case corresponds to a reference to an immutable variable.

1. M = (u_{j}^{1} M_{κ}), N = (u_{j}^{1} N_{κ}),

2. M = (case u_{j}^{2} M_{1} (λf.f M_{Q} M_{K})), N = (case u_{j}^{2} N_{1}(λf.f N_{Q} N_{K}))

3. M = u_{j}^{3}, N = u_{j}^{3}

4. M = (deref M_{1} M_{2}), N = (N_{1} N_{2})

5. M = (deref M_{1} M_{2}), N = (deref N_{1} N_{2})

6. M = (update M_{1} M_{2} M_{3}), N = (update N_{1} N_{2} N_{3})

7. M = (new M_{1} M_{2}), N = (new N_{1} N_{2})

8. M = (io M_{1}), N = (io N_{1})

9. M = ((λx.M_{0}) M_{1} … M_{k}), N = ((λx.N_{0}) N_{1} … N_{k})

10. other PCF head redexes ⟨1⟩1. Case: M = (u_{j}^{1} M_{κ}), N = (u_{j}^{1} N_{κ})

Let: 1. σ_{L}^{1}(j) = L_{1}(X_{j}^{1})[[M_{j}^{1}]]

2. σ_{R}^{1}(j) = R_{1}(V_{j}^{1}, C_{j}^{1})[[N_{j}^{1}]]

⟨2⟩1. lhs = ⟨⟨(L_{1}(X_{j}^{1})[[M_{j}^{1}]] M_{κ}) ; Σ_{M}⟩⟩σ_{L}

→_{left,pcf}^{∗} ⟨⟨(M_{κ} L_{2}(X_{j}^{1})[[M_{j}^{1}]]) ; Σ_{M}⟩⟩σ_{L}

⟨2⟩2. rhs = ⟨⟨(R_{1}(V_{j}^{1}, C_{j}^{1})[[N_{j}^{1}]] N_{κ}) ; Σ_{N}⟩⟩σ_{R}

→_{pcf}^{∗} ⟨⟨(N_{κ} R_{2}(X_{j}^{1})[[N_{j}^{1}]]) ; Σ_{N}⟩⟩σ_{R}

⟨2⟩3. Q.E.D.

Both sides stay in S_{AE} by adding corresponding new elements to σ_{L}^{2} and σ_{R}^{2}. For example, assume the variable u_{n}^{2} is fresh. To σ_{L}^{2}, we add the pair (u_{n}^{2}, (L_{2}(X_{j}^{1})[[M_{j}^{1}]])), and to σ_{R}^{2}, we add the pair (u_{n}^{2}, (R_{2}(X_{j}^{1})[[N_{j}^{1}]])). We assume that Γ ⊢ M_{κ} ⇝^{AE}_{V |Z} N_{κ}:Val→pr, and so the pair (⟨⟨(M_{κ} u_{n}^{2}) ; Σ_{M}⟩⟩σ_{L}, ⟨⟨(N_{κ} u_{n}^{2}) ; Σ_{N}⟩⟩σ_{R}) is in S_{AE} .

⟨1⟩2. Case: M = (case u_{j}^{2} M_{1} (λf.f M_{Q} M_{K})), N = (case u_{j}^{2} N_{1}(λf.f N_{Q} N_{K})) Same as Step ⟨1⟩1, in that both sides take β steps to stay in S_{AE} . For this step, we add corresponding new elements to σ^{3}L and σ^{3}R.

⟨1⟩3. Case: M = u_{j}^{3}, N = u_{j}^{3}

Let: 1. σ_{L}^{3}(j) = L_{3}(X_{j}^{3})[[M_{j,1}^{3}, M_{j,2}^{3}, M_{j,3}^{3}]],

2. σ_{R}^{3}(j) = R_{3}(V_{j}^{3}, C_{j}^{3})[[N_{j,1}^{3}, N_{j,2}^{3}, N_{j,3}^{3}]]

Assume: Γ ⊢ M_{j,i}^{3} ⇝^{AE}_{V} N_{j,i}^{3}:τ, 1 ≤ i ≤ 3

⟨2⟩1. lhs = ⟨⟨\begin{matrix}new^{Val}(listref_{1} M_{j,2}^{3}) (λx_{1}:ref (Val). · · · \\ new^{Val}(listref_{m} M_{j,2}^{3}) (λx_{m}:ref (Val). \\ (M_{j,1}^{3} M_{j,3}^{3}) …)) ; Σ_{M}⟩⟩σ_{L} \end{matrix}

if X_{j}^{3} = ⟨x_{1}, …, x_{m}⟩
→^{>0}_{left,sto} ⟨⟨(M_{j,1}^{3} M_{j,3}^{3})[l_{i}/x_{i}]_{i=1}^{m} ;
Σ_{M}[l_{i} ↦ (listref_{i} M_{j,2}^{3})]_{i=1}^{m}
= lhs′

⟨2⟩2.

rhs = ⟨⟨\begin{matrix}new^{Val}(listref_{i} N_{j,2}^{3}) \\ (λx_{i}:ref (Val). \end{matrix} \} for each x_{i} ∈ C_{j}^{3}
(N_{j,1}^{3} [(listref_{i} N_{j,2}^{3})/x_{i}]_{x_{i}∈V_{j}^{3}} N_{j,3}^{3}) …) ; Σ_{N}⟩⟩σ_{R}
→_{sto}^{∗} ⟨⟨(N_{j,1}^{3} [(listref_{i} N_{j,2}^{3})/x_{i}]_{x_{i}∈V_{j}^{3}} [l_{i}/x_{i}]_{x_{i}∈C_{j}^{3}} N_{j,3}^{3}) ;
Σ_{N}[l_{i} ↦ (listref_{i} N_{j,2}^{3})]_{i∈C_{j}^{3}}⟩⟩σ_{R}
= rhs′

⟨2⟩3. Q.E.D.

To get (lhs′, rhs′) in S_{AE} , we need to add some pairs to the Z component of the ⇝^{AE}_{V |Z} relation. Specifically, add the following pairs to Z:

{(l_{i}, (listref N_{j,2}^{3})) | x_{i} ∈ V_{j}^{3}}

⟨1⟩4. Case: M = (deref M_{1} M_{2}), N = (N_{1} N_{2})

It must be that we have a case of the ([[x]], x immutable) rule from Figure 14. Let: 1. M = M′′[l_{i}/x_{i}]_{i=1}^{k}, N = N′′[P_{i}/x_{i}]_{i=1}^{k},

for x_{i} ∈ X and (l_{i}, P_{i}) ∈ Z, 1 ≤ i ≤ k.

2. M′′ = (deref x_{i} M′′_{2}) and N′′ = (N′′_{1} x_{i}),

3. Γ ⊢ M′′_{2} ⇝^{AE}_{V} N′′_{1}:Val→pr

4. Σ_{M}(l_{i}) = P′_{i} s.t. P′_{i} ⇝^{AE}_{V |Z} P_{i}

So, we have Γ ⊢ M′′ ⇝^{AE}_{V} N′′:pr by rule ([[x]], x immutable). ⟨2⟩1.

lhs = ⟨⟨deref l_{i} M_{2} ; Σ_{M}⟩⟩σ_{L}
→^{1}_{left,sto} ⟨⟨(M_{1} P′_{i}) ; Σ_{M}⟩⟩σ_{L}
→^{<s}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨2⟩2. rhs = ⟨⟨(N_{1} P_{i}) ; Σ_{N}⟩⟩σ_{R}

→_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ by IH(< s) and (cong-app)

⟨1⟩5. Case: M = (deref M_{1} M_{2}), N = (deref N_{1}N_{2})

We have Γ ⊢ M′ ⇝^{AE}_{V} N′:pr by rule (cong-const) for the deref constant, for M = M′σ_{L} and N = N′σ_{R}.

Let: 1. Γ ⊢ M_{1} ⇝^{AE}_{V |Z} N_{1}:ref (τ)

2. Γ ⊢ M_{2} ⇝^{AE}_{V |Z} N_{2}:τ→pr

⟨2⟩1.

lhs = ⟨⟨deref M_{1} M_{2} ; Σ_{M}⟩⟩σ_{L}
→_{left,pcf}^{∗} ⟨⟨deref l M_{2} ; Σ_{M}⟩⟩σ_{L}
→^{1}_{left,sto} ⟨⟨(M_{2} P′) ; Σ_{M}⟩⟩σ_{L}  assuming Σ_{M}(l) = P′
→^{<s}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨2⟩2.

rhs = ⟨⟨deref N_{1} N_{2} ; Σ_{N}⟩⟩σ_{R}
→_{pcf}^{∗} ⟨⟨deref l N_{2} ; Σ_{N}⟩⟩σ_{R}  by Lemma 5.3.6

→^{1}_{sto} ⟨⟨(N_{2} P′′) ; Σ_{N}⟩⟩σ_{R} with P′ ⇝^{AE}_{V |Z} P′′

→_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ by IH(< s) and (cong-app) To use Lemma 5.3.6, we must show that M_{1} ∉ dom(Z). We know this because the deref expression was built with the (cong-const) rule for c = deref, and the locations in Z correspond to those in the first deref case. Furthermore, those variables x which are replaced at runtime by the locations in Z are excluded from the (cong-var) rule.

⟨1⟩6. Case: M = (update M_{1} M_{2} M_{3}), (N = update N_{1} N_{2} N_{3})

We have Γ ⊢ M′ ⇝^{AE}_{V} N′:pr by rule (cong-const) for the update constant. Proof: We again want to use Lemma 5.3.6 to show that M_{1} and N_{1} reduce to the same location, and so we need to show that (M_{1}, N_{1}) ∉ Z. Assume for the moment that (M_{1}, N_{1}) is in Z; then M_{1} must be a location, l. However, the locations in Z are a record of substitutions for variables in the list V, and V is a list of variables which never occur as the argument to update – contradiction. Thus M_{1} cannot be in the domain of Z, and we can use Lemma 5.3.6 to get M_{1} →_{pcf}^{∗} l and N_{1} →_{pcf}^{∗} l. Now both sides can then take a single step and remain in S_{AE} . We can then invoke the induction hypothesis at j < s to get the result.

⟨1⟩7. Case: M = (new M_{1} M_{2}), N = (new N_{1} N_{2})

We have Γ ⊢ M′ ⇝^{AE}_{V} N′:pr by rule (cong-const) for the new constant.

⟨2⟩1. lhs = ⟨⟨new M_{1} M_{2} ; Σ_{M}⟩⟩σ_{L}

→^{1}_{left,sto} ⟨⟨(M_{2} l) ; Σ_{M}[l ↦ M_{1}]⟩⟩σ_{L}
→^{j<s}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨2⟩2. rhs = ⟨⟨new N_{1} N_{2} ; Σ_{N}⟩⟩σ_{R}

→_{sto} ⟨⟨(N_{2} l′) ; Σ_{N}[l′ ↦ N_{1}]⟩⟩σ_{R}
→_{sto}^{∗} ⟨⟨io N′ ; Σ′_{N}⟩⟩ by α_{loc} and IH(j)

Proof: We really have to show that rhs is in α_{loc} with ⟨⟨(N_{2} l) ; Σ_{N}[l ↦ N_{1}]⟩⟩, and we can invoke IH on that term. Lemma 2.5.11 says that α_{loc} preserves ≲_{sim}, so we are OK. This line of reasoning is carried out more painstakingly in the proof of the new case in the substitution lemma.

⟨1⟩8. Case: M = io M_{1}

Proof: Immediate. ⟨1⟩9. Case: M = (λx.M_{0}) M_{1} … M_{k}, N = (λx.N_{0}) N_{1} … N_{k}

We have Γ ⊢ M′ ⇝^{AE}_{V} N′:pr by rule (cong-abs).

Proof: Both sides can take a β step and stay in S_{AE} . We can then invoke IH(s − 1). ⟨1⟩10. Case: Other PCF head redexes are all straightforward.

Corollary 5.3.8

S_{AE} ⊆ ≲_{sim}

Now we are ready to use the S_{AE} simulation to prove the correctness of assignment elimination. Recall that by Lemma 4.3.1 we know that, for Γ mapping free variables of e to ref (Val),

Γ ⊢ [[e]]_{scm}:(Val→pr)→pr  (3)

By Lemma 5.2.2, for Γ mapping e’s free variables to ref (Val), we know that

Γ ⊢_{cell} AE(e):ok

And by Lemma 5.1.1, we can deduce that

Γ ⊢ [[AE(e)]]_{cell}:(Val→pr)→pr  (4)

Thus the statement of the correctness of assignment elimination is as follows:

Theorem 5.3.9 (Correctness of Assignment Elimination) For any Scheme expression e, and any Γ mapping the free variables of [[e]]_{scm} and [[AE(e)]]_{cell} to ref (Val),

Γ ⊢ [[e]]_{scm} ≅_{∀C} [[AE(e)]]_{cell}:(Val→pr)→pr

Proof:

1. By the Extensionality Theorem, 2.8.1, it suffices to show that for all closing substitutions σ mapping free variables to closed terms of type ref (Val), all closed terms K of type Val→pr, and all stores Σ,

⟨⟨([[e]]_{scm}σ) K ; Σ⟩⟩ ≲_{sim} ⟨⟨([[AE(e)]]_{cell}σ) K ; Σ⟩⟩

2. The effects of any closing substitution σ can be duplicated by using a closing context C_{σ}[−] such that the identifiers in scope at the hole correspond to the domain of σ and such that the binders of those identifiers are applied to the same elements as in the range of σ.

3. By Lemma 5.3.5,

⟨⟨C_{σ}[[[e]]_{scm}] K ; Σ⟩⟩ S_{AE} ⟨⟨C_{σ}[[[AE(e)]]_{cell}] K ; Σ⟩⟩

for C = (C_{σ}[−] K).

4. By Corollary 5.3.8, S_{AE} ⊆ ≲_{sim}, and we are done.

100 CHAPTER 5. ASSIGNMENT ELIMINATION

Lambda Lifting – A Complex

Source-to-Source Transformation

Lambda lifting transforms lambda abstractions with free variables into lambda abstractions with fewer free variables by adding those free variables to the parameter lists of the lifted abstractions. Once the free variables of a nested procedure have been converted to arguments, the nested procedure can be lifted out of the scope of the bindings of those variables. Lambda-lifting is done in the hope that lifting a procedure to a more global scope will reduce the number of times a closure will have to be created for that procedure. Further, it is hoped that the savings in reduced closure allocation will make up for the overhead of having to pass additional arguments to the lifted procedure. Traditional lambda lifting lifts procedures to the outermost scope, adding all free variables of a procedure to its argument list. The Twobit Scheme compiler of Clinger and Hansen [CH94] implements incremental lambda lifting, which lifts nested procedures up one level – out of an enclosing abstraction. Only variables which are free in the nested procedure and bound by the enclosing abstraction are added to the procedure’s argument list. The process of incremental lambda lifting can be performed repeatedly in order to bring a deeply-nested procedure to the top level, as would be done with traditional lambda lifting. However, being able to lift only one level at a time gives the compiler added flexibility. In order for the lambda-lifting transformation to be correct, clearly all calls to a lifted procedure must pass any new parameters. This requires that all call sites be known, which rules out lifting procedures that may escape their scope of definition. Also, there can be no side-effects to the once-free-now-bound variables within a lifted procedure, as the sideeffects would, as specified in the Scheme semantics, be modifying a different cell in the lambda-lifted body than in the original. We prove the correctness of incremental lambda lifting as a transformation on Scheme_{cell} terms. Therefore, we may assume that [[−]]_{cell} is the translation into the metalanguage. In particular, no storage is allocated for arguments to an abstraction, so there is no danger of a bad interaction between store updates and store allocation for parameter passing. Thus what we actually prove is the correctness of lambda lifting composed with a meaningpreserving translation from Scheme to Scheme_{cell}, such as assignment elimination.

6.1 The Lambda-Lifting Transformation

The lambda-lifting transformation operates on a Scheme_{cell} term of the form (lambda (x_{1} … x_{m_{0}}) (letrec

((f_{1} (lambda (y_{1} … y_{m_{1}}) e_{1})) …

(f_{n} (lambda (y_{1} … y_{m_{n}}) e_{n})))

e_{0})) where each of the f_{1} … f_{n} procedures may be lifted out of the scope of the enclosing lambda (x_{1} … x_{m_{0}}). Recall that the Scheme letrec is not a fixpoint operator – it is a macro for a sequence of set!’s to the identifiers for the procedures being defined. After lambda lifting, each lifted procedure may have additional arguments, taken from the list x_{1} … x_{m_{0}}. We use the following notation to denote the different sequences of identifiers:

X_{0} = ⟨x_{1}, …, x_{m_{0}}⟩
F = ⟨f_{1}, …, f_{n}⟩
Y_{i} = ⟨y_{1}, …, y_{m_{i}}⟩, 1 ≤ i ≤ n
X_{i} = {x_{j} | x_{j} ∈ X_{0} must be added to the argument list of f_{i}},
1 ≤ i ≤ n
𝕏 = ⟨X_{1}, …, X_{n}⟩
𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩

So, X_{0} is the list of arguments to the outermost lambda expression; F is the list of local procedure identifiers; Y_{i} is the list of original arguments to the i^{th} local procedure, f_{i}; and X_{i} is the set of identifiers to be added to the argument list of f_{i}. Each X_{i} is a subset of the list X_{0}. We denote the collection of all X_{i} sequences by the symbol 𝕏, and the collection of the local procedure identifiers and their signatures by 𝔽. The length of a sequence Q is denoted by #Q. Sometimes we treat sequences as their underlying sets; allowing, for example, Q_{1} ∪ Q_{2}. The i^{th} element of a sequence Q is denoted by Q_{(i)}; for the i^{th} element of a sequence such as X_{k}, we write X_{k(i)}. To indicate the splicing of a sequence into a larger sequence, we use the notation [x_{i}]_{∈ Q}. For example, if X_{5} = ⟨x_{1}, x_{3}, x_{7}⟩,

(M [x_{i}]_{∈ X_{5}} N) rewrites to (M x_{1} x_{3} x_{7} N) When the splicing operation is obvious, we may simply refer to the sequence. For example, lambda (Y_{k}) is shorthand for lambda (y_{1} … y_{m_{k}}). The lambda-lifting transformation is defined in several steps. Figure 17 defines the conditions under which lambda lifting may be performed – i.e., when a Scheme_{cell} term e is lambda liftable with respect to a list of lists 𝕏. We disallow any conflicts of bound variables – all binding constructs within the procedure bodies e_{i}, for 0 ≤ i ≤ n, must bind variables distinct from the identifiers

x_{1} … x_{m_{0}}, f_{1}, … f_{n}, y_{1} … y_{m_{i}}, for 1 ≤ i ≤ n

This requirement can be satisfied by alpha-renaming, which can easily be proved correct Definition 6.1.1 (Lambda Liftable) Let e be an expression in Scheme_{cell}, let Γ be a map from the free variables of e to {Val, ref (Val)}, and let 𝕏 be a list of lists of variables. Then e is lambda-liftable with respect to Γ and 𝕏 iff:

1. Γ ⊢_{cell} e:ok

2. e = (lambda (X_{0}) e′), X_{0} = x_{1} … x_{m_{0}}, and

3. e′ = (letrec

((f_{1} (lambda (Y_{1}) e_{1})), Y_{1} = y_{1} … y_{m_{1}}
…
(f_{n} (lambda (Y_{n}) e_{n})), Y_{n} = y_{1} … y_{m_{n}}
e_{0})

4. The variables x_{i}, y_{j}, f_{k} are disjoint, for 1 ≤ i ≤ m_{0}, 1 ≤ j ≤ max(m_{k}), 1 ≤ k ≤ n. Also, all binding constructs within e_{0} and the e_{k} bind identifiers distinct from the x_{i}, y_{j}, and f_{k}.

5. All occurrences of each f_{k} in e_{0}, e_{1}, …, e_{n} are in operator position, for 1 ≤ k ≤ n. That is, the f_{k} cannot be assigned to or passed out of their scope.

6. The list of lists of variables, 𝕏, has n elements, X_{1}, …, X_{n}. Letting k range from 1 to n, and treating each X_{k} as a set, we require that for each k,

(a) X_{k} ⊆ {x_{1}, …, x_{m_{0}}}

(b) X_{k} ⊇ (fv(e_{k}) ∩ X_{0}) ∪ (⋃{X_{j} | f_{k} calls f_{j}})

Figure 17: Lambda Liftable separately. We require the bound variables to be distinct in order to avoid scenarios such as the following, where procedure f_{2} shadows the variable x, confounding the transform of a call to f_{1}: (lambda (x)

(letrec ((f_{1} (lambda (y) … x …))
(f_{2} (lambda (x) … (f_{1} 42) …)))
… (f_{1} 6) … (f_{2} 7) …))

gets stuck at:

(letrec ((f_{1} (lambda (x y) … x …))
(f_{2} (lambda (x) … (f_{1} ?? 42) …)))
(lambda (x) … (f_{1} x 6) … (f_{2} 7) …))

Clearly there are various workarounds to the above problem, and we choose simply to require that the bound variables all be distinct. The nested procedures which we are lifting, f_{1} … f_{n}, must be known local procedures. That is, the procedures are never passed out of the scope of the outer lambda(x_{1} … x_{m_{0}}), and the identifiers f_{1} … f_{n} are never assigned to except by the first letrec. We enforce the restriction that the f_{k} be local by requiring that all occurrences of the f_{k} be in operator position. More sophisticated analyses are possible, but that is another research topic. We require that, for a given f_{k}, the arguments to be added are in a solution to (a fixed point of) a set of constraints. Before lifting f_{k} outside the scope of lambda (x_{1} … x_{m_{0}}), any of the x_{i} referenced in e_{k} must be added to f_{k}’s parameter list. More subtly, if f_{k} calls f_{j}, i.e. if an application (f_{j} e_{1} … e_{m_{j}}) is a subterm of e_{k}, then the new parameters which must be sent to the lifted f_{j} must be added (if not already there) to the incoming parameters of f_{k}. Adding these newly required parameters to f_{k} may have an effect on the parameters added to any f_{i}’s which, in turn, call f_{k} – and so on. Eventually a fixed point will be reached. The list of arguments to the outer lambda, ⟨x_{1}, …, x_{m_{0}}⟩ is always a solution to the set of constraints, though not necessarily the smallest solution.

Definition 6.1.2 (Lambda Lifting (LL)) If Scheme_{cell} expression e is lambda-liftable with respect to a list of lists of arguments to be added 𝕏, then the Lambda-lift of e with respect to 𝕏 is defined as: LL(𝕏, e) =^{def} (letrec

(\begin{matrix}(f_{1} (lambda ([x_{i}]_{∈ X_{1}} y_{1} … y_{m_{1}}) \\ LL_{body}(F, 𝕏, e_{1}))) \\ … \\ (f_{n} (lambda ([x_{i}]_{∈ X_{n}} y_{1} … y_{m_{n}}) \\ LL_{body}(F, 𝕏, e_{n})))) \end{matrix}

(lambda (x_{1} … x_{m_{0}}) LL_{body}(F, 𝕏, e_{0})))

where F = {f_{1}, …, f_{n}} and where LL_{body} is defined as follows:

Definition 6.1.3 (LL_{body}) LL_{body}(F, 𝕏, x) = x LL_{body}(F, 𝕏, n) = n LL_{body}(F, 𝕏, (cell-ref x)) = (cell-ref x) LL_{body}(F, 𝕏, (cell-set! x e)) = (cell-set! x LL_{body}(F, 𝕏, e)) LL_{body}(F, 𝕏, (f_{k} e_{1} … e_{m_{k}})) =

(f_{k} [x_{i}]_{∈ X_{k}} LL_{body}(F, 𝕏, e_{1}) … LL_{body}(F, 𝕏, e_{m_{k}}))

if f_{k} ∈ F

LL_{body}(F, 𝕏, (e_{1} … e_{p})) =

(LL_{body}(F, 𝕏, e_{1}) … LL_{body}(F, 𝕏, e_{p})) if e_{1} ∉ F LL_{body}(F, 𝕏, (lambda (y_{1} … y_{p}) e)) =

(lambda (y_{1} … y_{p}) LL_{body}(F, 𝕏, e)) LL_{body}(F, 𝕏, (let ((y_{1} rhs_{1}) … (y_{p} rhs_{p})) e)) =

(let ((y_{1} LL_{body}(F, 𝕏, rhs_{1})) … (y_{p} LL_{body}(F, 𝕏, rhs_{p}))) LL_{body}(F, 𝕏, e)) LL_{body}(F, 𝕏, (letrec ((y_{1} e_{1}) … (y_{p} e_{p})) e)) =

(letrec ((y_{1} LL_{body}(F, 𝕏, e_{1})) … (y_{p} LL_{body}(F, 𝕏, e_{p}))) LL_{body}(F, 𝕏, e))

Figure 18: Lambda Lifting The lambda-lifting transformation, once we have a liftable e and 𝕏, is given in Figure 18. Definition 6.1.2 shows how the function definitions are rewritten to take added parameters, and how the various f_{k} are now defined outside the scope of the lambda (x_{1} … x_{m_{0}}) procedure. Definition 6.1.3 defines how the individual call sites are rewritten to be consistent with the revised function definitions. The only interesting rule is the fifth, where an application of an f_{k} must have the new arguments added. The remaining rules push the transformation down the Scheme_{cell} syntax tree.

6.2 Correctness of Lambda Lifting

Our goal is to prove that incremental lambda lifting preserves the meaning of Scheme_{cell} terms. That is, for any Scheme_{cell} term e and type assumption Γ mapping the free variables of e to ref (Val), if Γ ⊢ e:ok and e is lambda-liftable with respect to a list of lists of variables 𝕏, then

Γ ⊢ [[e]]_{cell} ≅_{∀C} [[LL(𝕏, e)]]_{cell}:(Val→pr)→pr

Of course, for lambda-lifting to be a correct transformation for Scheme expressions, there first needs to be a meaning-preserving transformation from Scheme to Scheme_{cell}, such as assignment elimination. It is important that the metalanguage terms we are concerned with are well-typed. Recall that by Lemma 5.1.1, for a Scheme_{cell} term e, and a type assumption Γ,

Γ ⊢_{cell} e:ok ⇒ Γ ⊢ [[e]]_{cell}:(Val→pr)→pr.

A similar condition holds after lambda lifting:

Lemma 6.2.1 For a Scheme_{cell} term e and a type assumption Γ mapping variables to {Val, ref (Val)}, if e is lambda-liftable with respect to a list of variable lists 𝕏,

Γ ⊢_{cell} e:ok ⇒ Γ ⊢ [[LL(𝕏, e)]]_{cell}:(Val→pr)→pr

Structural induction on ⊢_{cell}. The most interesting case is when we have a variable reference x in e. Either x is in the free variables of e, in which case Γ(x) = ref (Val), or it occurs within some lambda (… x …) binding. We must show that x is still bound by an enclosing lambda (… x …) in LL(𝕏, e). If x ∈ X_{0} and the reference to x is in a lifted local procedure f_{i}, then criterion (6b) in Figure 17 guarantees that x will be bound by the enclosing lambda ([x_{i}]_{∈ X_{n}} y_{1} … y_{m_{n}})

The translation of a Scheme_{cell} expression e, when e is lambda-liftable with respect to a list of variable lists 𝕏 according to Definition 6.1.1, is as follows:

[[e]]_{cell} = λκ:Val→pr. in_{F} (λx^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{0} x^{∗})[[e′]]_{cell}[(listref_{i} x^{∗})/x_{i}]_{i=1}^{m_{0}} κ′) κ

where [[e′]]_{cell} =λκ:Val→pr. new Ω_{Val}(λf_{1}:ref (Val). · · · new Ω_{Val}(λf_{n}:ref (Val). [[(lambda (Y_{1}) e_{1})]]_{cell}(λv_{1}:Val. update f_{1}v_{1} ⋯ [[(lambda (Y_{n}) e_{n})]]_{cell}(λv_{n}:Val. update f_{n}v_{n} ([[e_{0}]]_{cell} κ)) ⋯)))

Recall that [[(lambda (Y_{k}) e_{k})]]_{cell} = λκ:Val→pr. in_{F} (λy^{∗}:Val^{∗}.λκ′:Val→pr. (checkargs m_{k} y^{∗})[[e_{k}]]_{cell}[(listref_{i} y^{∗})/y_{i}]_{i=1}^{m_{k}} κ′) κ

We may do a few β-reductions to get the following metalanguage term:

lhs =^{def} λκ:Val→pr. in_{F} (λx^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{0} x^{∗})
new Ω_{Val}(λf_{1}:ref (Val). · · · new Ω_{Val}(λf_{n}:ref (Val).
update f_{1}(inl(λy^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{1} y^{∗})[[e_{1}]]_{cell}σ_{1} κ′)) ⋯
update f_{n}(inl(λy^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{n} y^{∗})[[e_{n}]]_{cell}σ_{n} κ′))
([[e_{0}]]_{cell} κ′)) ⋯)σ_{0}) κ

where σ_{0} = [(listref_{i} x^{∗})/x_{i}]_{i=1}^{m_{0}}, and σ_{k} = [(listref_{i} y^{∗})/y_{i}]_{i=1}^{m_{k}}, for 1 ≤ k ≤ n. The translation of LL(𝕏, e), on the other hand, is β-equal to the following:

rhs =^{def} λκ:Val→pr.
new Ω_{Val}(λf_{1}:ref (Val). · · · new Ω_{Val}(λf_{n}:ref (Val).
update f_{1}(inl(λy^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{1} y^{∗})[[LL_{body}(F, 𝕏, e_{1})]]_{cell}σ′_{1} κ′)) ⋯
update f_{n}(inl(λy^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{n} y^{∗})[[LL_{body}(F, 𝕏, e_{n})]]_{cell}σ′_{n} κ′))
in_{F} (λx^{∗}:Val^{∗}.λκ′:Val→pr.
(checkargs m_{0} x^{∗})([[LL_{body}(F, 𝕏, e_{0})]]_{cell} κ′)σ_{0}) κ) ⋯)

where σ′_{k} = [(listref_{i} y^{∗})/X_{k(i)}]_{i=1}^{#X_{k}} [(listref_{#X_{k}+j} y^{∗})/y_{j}]_{j=1}^{m_{k}}

for 1 ≤ k ≤ n Recall that each X_{k(i)} ∈ {x_{1}, …, x_{m_{0}}}. The pre-lifted translation, lhs, returns a closure which will allocate and store closures for f_{1} … f_{n} whenever called. The translation of the lifted term, rhs, allocates and stores the f_{1} … f_{n} closures first, then returns a closure with the identifiers f_{1} … f_{n} bound to the new locations and which merely invokes its (lifted) body e_{0} whenever called. Note that on the pre-lifted side, the translation of a local procedure f_{k} is a closure with body (λy^{∗}κ′.[[e_{k}]]_{cell}σ_{k} κ′), which may have free variables x_{i} ∈ {x_{1}, …, x_{m_{0}}}. These free variables are substituted-for at runtime by the σ_{0} substitution, which binds the variables x_{1} … x_{m_{0}} to the corresponding elements of x^{∗}. On the lambda-lifted side, however, these free variables have been put into the local argument lists y^{∗} and are no longer free in the local procedure’s closure. The σ_{0} substitution is the same, but the scope of σ_{0} covers only the innermost closure – i.e. σ_{0} does not apply to any of the (λy^{∗} κ′.[[LL_{body}(F, 𝕏, e_{k})]]_{cell}σ′_{k} κ′) closures. To reiterate the motivation for the lambda-lifting transformation: lambda lifting is done in the hope that not having to allocate (as much) storage for the f_{1} … f_{n} closures makes up for the overhead of passing additional arguments to the local procedures. Good register allocation may even reduce the overhead of added argument passing to zero. By the Extensionality Theorem, Theorem 2.8.1, and by the preceding calculations, in order to prove [[e]]_{cell} ≅_{∀C} [[LL(𝕏, e)]]_{cell} at type (Val→pr)→pr, we need to show that the lhs and rhs terms are bisimilar when applied to a continuation in a state. For a continuation K:Val→pr and a store Σ, the original term simply injects the closure into the Val type (we assume the procedure component is the right summand) and invokes the continuation, having done no new allocation: ⟨⟨lhs K ; Σ⟩⟩ →_{pcf}^{∗} ⟨⟨K L(X_{0}, 𝔽)[[ [[e_{0}]]_{cell}, …, [[e_{n}]]_{cell} ]] ; Σ⟩⟩, where L(X_{0}, 𝔽)[[P_{0}, …, P_{n}]] = (inr(λx^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{0} x^{∗}) new Ω_{Val}(λf_{1}:ref (Val). · · · new Ω_{Val}(λf_{n}:ref (Val). update f_{1} C(Y_{1})[[P_{1}]] ⋯ update f_{n} C(Y_{n})[[P_{n}]] (P_{0} κ′)) ⋯)σ_{0})), and

C(Y_{k})[[P]] = (inr(λy^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{k} y^{∗})(P σ_{k})κ′)) The substitutions σ_{0}, σ_{1}, …, σ_{n} are as defined on page 109. Substitution σ_{0} is derived from the signature X_{0} of the outer lambda, and the σ_{k} are derived from the signatures Y_{k} contained in 𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩. The L macro defines the structure of the metalanguage term corresponding to the translation under [[−]]_{cell} of a lambda-liftable Scheme_{cell} expression. The P_{k} parameters to L correspond to the translations of the procedure bodies e_{0}, e_{1}, …, e_{n}. The macro C(Y_{k})[[−]] corresponds to the closure corresponding to the translation under [[−]]_{cell} of the k^{th} local procedure (lambda (Y_{k})e_{k}). The lifted term allocates new locations l_{1}, …, l_{k} and stores its procedure closures in these locations before returning the closure for the lambda (X_{0}) procedure:

⟨⟨rhs K ; Σ⟩⟩ →_{sto}^{∗} ⟨⟨(K R(X_{0})[[ [[LL_{body}(F, 𝕏, e_{0})]]_{cell} ]])[l_{k}/f_{k}]_{k=1}^{n} ; Σ′⟩⟩, where R(X_{0})[[P]] = (inr(λx^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{0} x^{∗})(P κ′)σ_{0})),

Σ′ =Σ[l_{1} ↦ C′(X_{1}, Y_{1})[[ [[LL_{body}(F, 𝕏, e_{1})]]_{cell}σ′_{1} ]][l_{k}/f_{k}]_{k=1}^{n}, …
l_{n} ↦ C′(X_{n}, Y_{n})[[ [[LL_{body}(F, 𝕏, e_{n})]]_{cell}σ′_{n}]][l_{k}/f_{k}]_{k=1}^{n}],

C′(X_{k}, Y_{k})[[P]] = (inr(λy^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{k} y^{∗})(P σ′_{k})κ′)) Again, σ_{0}, σ′_{1}, …, σ′_{n} are as defined on page 109. The substitutions σ′_{k} require both the original signatures Y_{k} and also the added parameters X_{k}. The R macro corresponds to the translation of a lambda-lifted Scheme_{cell} expression. The P parameter to R corresponds to the translation of the lambda-lifted body of the e_{0} procedure body. We next consider what happens at runtime when the closures returned by the original and lifted terms are actually used. In the original Scheme_{cell} terms, this would correspond to the application of the abstraction returned from evaluation of e to m_{0} arguments. The nonlifted metalanguage term allocates n fresh locations, storing new instances of the closures for its local procedures at these locations. The run-time behavior will look like the following: ⟨⟨(out_{F} L(X_{0}, 𝔽)[[[[e_{0}]]_{cell}, …, [[e_{n}]]_{cell}]](λf:Val^{∗}→(Val→pr)→pr.

(f ⟨M_{1}, …, M_{m_{0}}⟩ M_{κ}))) ; Σ⟩⟩

→_{sto}^{∗} ⟨⟨([[e_{0}]]_{cell} M_{κ})σ_{0}^{M}[l_{i}/f_{i}]_{i=1}^{n} ; Σ′′⟩⟩ where

Σ′′(l_{k}) = C(Y_{k})[[[[e_{k}]]_{cell}]]σ_{0}[l_{i}/f_{i}]_{i=1}^{n}

σ_{0}^{M} =^{def} [M_{i}/x_{i}]_{i=1}^{m_{0}}

The substitution σ_{0}^{M} is the “instantiation” of the σ_{0} substitution, with metalanguage terms taking the place of list references. An important aspect of the preceding calculation is that the σ_{0}^{M} substitution, which substitutes elements of x^{∗} (namely M_{1} … M_{m_{0}}) for x_{i}, 1 ≤ i ≤ m_{0}, is in effect during the allocation for, and storage of, the local procedure closures. Thus any references to the x_{i} variables in the procedure bodies e_{k} are captured by the σ_{0}^{M} substitution before the closure is put in the store. Recall that in the lifted metalanguage term the closures for the local procedures are stored earlier. Specifically, the closures for the local procedures are stored when the closure for the lambda (X_{0}) procedure is created, but before that closure is ever applied. Thus, in the lambda-lifted term, much less happens when the closure for lambda (X_{0}) is actually applied. We are assured that there will already be a substitution active, [l_{i}/f_{i}]_{i=1}^{n}, mapping the procedure identifiers to locations: ⟨⟨(out_{F} R(X_{0})[[[[e_{0}]]_{cell}]][l_{i}/f_{i}]_{i=1}^{n} (λf:Val^{∗}→(Val→pr)→pr.

(f ⟨N_{1}, …, N_{m_{0}}⟩ N_{κ}))) ; Σ′⟩⟩

→_{pcf}^{∗} ⟨⟨([[e_{0}]]_{cell} N_{κ})σ_{0}^{N}[l_{i}/f_{i}]_{i=1}^{n} ; Σ′⟩⟩ where

Σ′(l_{k}) = C′(X_{k}, Y_{k})[[ [[LL_{body}(F, 𝕏, e_{k})]]_{cell} ]][l_{i}/f_{i}]_{i=1}^{n}

σ_{0}^{N} =^{def} [N_{i}/x_{i}]_{i=1}^{m_{0}}

Finally, let us consider what happens at runtime when a local procedure f_{k} is applied. In the original Scheme_{cell} term, an application such as (f_{k} e_{1} … e_{m_{k}}) will translate into a standard form in the metalanguage, for which we define the A macro: [[(f_{k} e_{1} … e_{m_{k}})]]_{cell} = (λκ:Val→pr.A[[ f_{k}, [[e_{1}]]_{cell}, … [[e_{m_{k}}]]_{cell}, κ]]) where A[[f, P_{1}, …, P_{n}, P_{κ}]] =

(deref f (λv_{f}:Val.P_{1} (λv_{1}:Val … P_{n} (λv_{n}.

out_{F} v_{f} (λf′:Val^{∗}→(Val→pr)→pr.
f′ ⟨v_{1}, …, v_{n}⟩ P_{κ})))))

That is, the closure for the procedure is retrieved from the store (at run-time, the identifier f_{k} will be bound to a location), each of the arguments to the procedure is evaluated, and finally the body of the closure is invoked with a tuple of arguments and a continuation.

On the lambda-lifted side, the added arguments must be passed, and so we will see a term such as: A′[[ f_{k}, X_{k}, [[e_{1}]]_{cell}, … [[e_{m_{k}}]]_{cell}, κ]] where A′[[f, X_{k}, P_{1}, …, P_{n}, P_{κ}]] =

(deref f (λv_{f}:Val.P_{1} (λv_{1}:Val … P_{n} (λv_{n}.

out_{F} v_{f} (λf′:Val^{∗}→(Val→pr)→pr.
f′ ⟨ [x_{i}]_{∈ X_{k}} v_{1}, …, v_{n}⟩ P_{κ})))))

The differences between [[e]]_{cell} and [[LL_{body}(F, 𝕏, e)]]_{cell} are characterized by the relation ⇝^{LL_{body}}, defined in Figure 19. The only interesting rule, (app-f_{k}), corresponds to the translation of an application of a known local procedure, where the additional parameters, X_{k}, are inserted into the call. The rule cong-var rules out the special case which is handled by the (app-f_{k}) rule. 𝔽 is used not only to match the procedure identifiers f_{k} but also to specify the m_{k}’s (the number of parameters for each local procedure). We can prove that the ⇝^{LL_{body}} relation captures the effect of the LL_{body} transformation on the translations into the metalanguage. In the following, after stating that a Scheme expression e is lambda-liftable with respect to a list of variable lists 𝕏, references to metavariables F, e_{k}, e′ and so forth refer to the sub-parts of e as in Figure 18. Also, the ⊂ operator denotes the subterm relation: e′ ⊂ e means that e′ is a subterm of e.

Lemma 6.2.2 If e is lambda-liftable with respect to 𝕏, and if e′ ⊂ e such that Γ ⊢ [[e′]]_{cell}:τ, then

Γ, 𝕏, 𝔽 ⊢ [[e′]]_{cell} ⇝^{LL_{body}} [[LL_{body}(F, 𝕏, e′)]]_{cell}:τ

Proof: Structural induction on e′.

114 CHAPTER 6. LAMBDA LIFTING Given 𝕏 = ⟨X_{1}, …, X_{n}⟩ and 𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩, ⇝^{LL_{body}} is the least relation closed under the following rules:

Γ[x:τ], 𝕏, 𝔽 ⊢ x ⇝^{LL_{body}} x:τ, x ∉ dom(𝔽) (cong-var)
Γ, 𝕏, 𝔽 ⊢ c ⇝^{LL_{body}} c:τ  (τ from Figure 1) (cong-const)
Γ, 𝕏, 𝔽 ⊢ l^{τ} ⇝^{LL_{body}} l^{τ}:ref (τ) (cong-loc)
\frac{Γ, 𝕏, 𝔽 ⊢ M ⇝^{LL_{body}} N:τ′→τ Γ ⊢ M′ ⇝^{LL_{body}} N′:τ′}{Γ, 𝕏, 𝔽 ⊢ (M M′) ⇝^{LL_{body}} (N N′):τ} (cong-app)

Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:(Val→pr)→pr, 1 ≤ i ≤ m_{k}

Γ, 𝕏, 𝔽 ⊢ M_{κ} ⇝^{LL_{body}} N_{κ}:Val→pr

M = A[[f_{k}, M_{1}, …, M_{m_{k}}, M_{κ}]]

N = A′[[f_{k}, X_{k}, N_{1}, …, N_{m_{k}}, N_{κ}]]

Γ, 𝕏, 𝔽 ⊢ M ⇝^{LL_{body}} N:pr

(app-f_{k})

Figure 19: Definition of ⇝^{LL_{body}} on Terms The relation ⇝^{LL_{body}} is closed under substitution by ⇝^{LL_{body}}-related terms:

Lemma 6.2.3 If Γ[x:τ′], 𝕏, 𝔽 ⊢ M ⇝^{LL_{body}} N:τ and if Γ, 𝕏, 𝔽 ⊢ M′ ⇝^{LL_{body}} N′:τ′, then

Γ, 𝕏, 𝔽 ⊢ M[M′/x] ⇝^{LL_{body}} N[N′/x]:τ

Proof: Structural induction on M.

We are now ready to prove the correctness of the incremental lambda lifting transformation on Scheme_{cell} terms. We have already started the process by appealing to the Extensionality Theorem 2.8.1 and reducing both sides in a state with a continuation of the correct type. We now construct a candidate simulation and show that the two sides always stay in the simulation relation (up to other simulation relations, as usual). Figure 20 defines the candidate simulation S_{LL}. The substitution pairs (σ_{u}, σ′_{u}) and (σ_{v}, σ′_{v}) abstract out the “interesting” subterms using placeholders u_{1} … u_{#u} and v_{1} … v_{#v}. The terms substituted for the u_{i} variables correspond to \underline{u}nevaluated translations of the (lambda (X_{0}) …) expressions – on the left-hand side the local procedure bodies remain in the term component of the state, whereas on the right-hand side the procedure bodies have already been put in the store. The corresponding procedure bodies are related by ⇝^{LL_{body}}. The terms substituted for the v_{i} variables correspond to e\underline{v}aluated [[(lambda (X_{0}) …)]]_{cell} terms. For each side, this means an active substitution for the x_{i} ∈ X_{0} parameters, and on the left-hand side, there is also a new set of bindings for newly-stored closures, [l_{k}^{i}/f_{k}]_{k=1}^{n}. Again, all of the corresponding procedure bodies are related by ⇝^{LL_{body}}.

Lemma 6.2.5 S_{LL} is a simulation.

116 CHAPTER 6. LAMBDA LIFTING Definition 6.2.4 (S_{LL}) Given 𝕏 = ⟨X_{1}, …, X_{n}⟩ and 𝔽 = ⟨(f_{1}, Y_{1}), …, (f_{n}, Y_{n})⟩,

S_{LL} =^{def} {(⟨⟨M ; Σ⟩⟩σ, ⟨⟨M ; Σ′⟩⟩σ′) |

preamble \{ \begin{matrix}∃u, v ∈ Var^{∗} s.t. \\ fv(M, rng(Σ), rng(Σ′)) ⊆ u ∪ v \\ σ = σ_{u} ∪ σ_{v} \\ σ′ = σ′_{u} ∪ σ′_{v} \\ ∃Σ_{0} s.t. dom(Σ_{0}) ⊆ dom(Σ), and dom(Σ_{0}) ⊆ dom(Σ′) \\ (Γ ⊢ M:pr) ⇒ (Γ(u_{i}) = Val, Γ(v_{i}) = pr) \end{matrix}
unevaluated ; lambda (X) ; closures \{ \begin{matrix}∃M_{0}^{i}, M_{1}^{i}, …, M_{n}^{i}, N_{0}^{i}, N_{1}, …, N_{n}, for 1 ≤ i ≤ #u s.t. \\ σ_{u} = [ u_{i} ↦ (L(X_{0}, 𝔽)[[M_{0}^{i}, …, M_{n}^{i}]]) ]_{i=1}^{#u} \\ σ′_{u} = [u_{i} ↦ (R(X_{0})[[N_{0}^{i}]][l_{k}/f_{k}]_{k=1}^{n}) ]_{i=1}^{#u} \\ Σ′ = Σ_{0}[l_{j} ↦ (C′(X_{j}, Y_{j})[[N_{j}]][l_{k}/f_{k}]_{k=1}^{n}) ]_{j=1}^{n} \\ \begin{matrix}Γ, 𝕏, 𝔽 ⊢ M_{0}^{i} ⇝^{LL_{body}} N_{0}^{i}:(Val→pr)→pr \\ Γ, 𝕏, 𝔽 ⊢ M_{k}^{i} ⇝^{LL_{body}} N_{k}:(Val→pr)→pr \end{matrix} \} & \begin{matrix}1 ≤ i ≤ #u \\ 1 ≤ k ≤ n \end{matrix} \end{matrix}
evaluated ; lambda (X) ; closures \{ \begin{matrix}∃M_{i}, M_{x_{1}}^{i}, …, M_{x_{m_{0}}}^{i} , N_{i}, N_{x_{1}}^{i}, …, N_{x_{m_{0}}}^{i} , for 1 ≤ i ≤ #v s.t. \\ σ_{v} = [v_{i} ↦ M_{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ]_{i=1}^{#v} \\ σ′_{v} = [v_{i} ↦ N_{i}[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} [l_{k}/f_{k}]_{k=1}^{n}]_{i=1}^{#v} \\ Σ = Σ_{0}[l_{h}^{i} ↦ (C(Y_{h})[[M_{h}^{i}]][l_{k}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) ]_{i=1,h=1}^{#v, n} \\ Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:pr, for 1 ≤ i ≤ #v \\ Γ, 𝕏, 𝔽 ⊢ M_{x_{j}}^{i} ⇝^{LL_{body}} N_{x_{j}}^{i}:Val, for 1 ≤ i ≤ #v, 1 ≤ j ≤ m_{0} \end{matrix}
}

Figure 20: The S_{LL} Candidate Simulation ⟨1⟩1. S_{LL} ⊆ [≲_{sim} ∘ S_{LL} ∘ ≲_{sim}]_{sim}

Proof sketch: By induction on the number of steps in the leftmost reduction of the lefthand side to an I/O operator, by considering the possible forms of the term component M:

1. M = (case u_{i} (λf.f M_{Q} M_{K}) M_{int})

2. M = v_{i}

3. M = (deref M_{1} M_{2})

4. M = (update M_{1} M_{2} M_{3})

5. M = (new M_{1} M_{2})

6. M = (io M_{1})

7. M = ((λx.M_{0}) M_{1} … M_{k})

8. other PCF head redexes The first two cases are the most interesting. ⟨2⟩1. Case: M = (case u_{i} (λf.f M_{Q} M_{K}) M_{int})

Assume: Γ ⊢ M_{Q}:Val^{∗}, M_{K}:Val→pr, M_{int}:int→pr

M_{Q} = ⟨M_{1}, …, M_{m_{0}}⟩

This case corresponds to the (lambda (X_{0}) …) in question having been applied to a set of arguments, e_{1} … e_{m_{0}}. The translations of the argument expressions correspond to the M_{j} metalanguage terms, for 1 ≤ j ≤ m_{0}. We can expect the left-hand side to store a new set of closures for its local procedures before evaluating its body, whereas the right-hand side gets right to its body: ⟨3⟩1. Left-hand side reduces:

⟨⟨(case u_{i} (λf.f M_{Q} M_{K}) M_{int}) ; Σ⟩⟩σ

= ⟨⟨(case (L(X_{0}, 𝔽)[[M_{0}^{i}, …, M_{n}^{i}]])(λf.f M_{Q} M_{K}) M_{int})

; Σ⟩⟩σ = ⟨⟨(case (inr(λx^{∗}:Val^{∗}.λκ′:Val→pr.

new Ω_{Val}(λf_{1}:ref (Val). · · · new Ω_{Val}(λf_{n}:ref (Val).

update f_{1} C(Y_{1})[[M_{1}^{i}]] ⋯ update f_{n} C(Y_{n})[[M_{n}^{i}]]
(checkargs m_{0} x^{∗})(M_{0}^{i} κ′)) ⋯)σ_{0}))
(λf. f ⟨M_{1} … M_{m_{0}}⟩ M_{K}) M_{int})
; Σ⟩⟩σ

=_{pcf} ⟨⟨(new Ω (λf_{1}. · · · new Ω (λf_{n}.

update f_{1} C(Y_{1})[[(M_{1}^{i}σ)]] ⋯ update f_{n} C(Y_{n})[[M_{n}^{i}σ]]

(M_{0}^{i} M_{K})σ) ⋯)[(M_{j}σ)/x_{j}]_{j=1}^{m_{0}}) ; Σ⟩⟩σ

→_{left,sto}^{∗} ⟨⟨(M_{0}^{i}[(M_{j}σ)/x_{j}]_{j=1}^{m_{0}} [l_{k}^{i}/f_{k}]_{k=1}^{n} M_{K})σ ;

Σ[l_{k}^{i} ↦ (C(Y_{k})[[M_{k}^{i}]][(M_{j}σ)/x_{j}]_{j=1}^{m_{0}} [l_{k}^{i}/f_{k}]_{k=1}^{n}) ]_{k=1}^{n}σ⟩⟩ = ⟨⟨(M_{0}^{i}[M_{j}/x_{j}]_{j=1}^{m_{0}} [l_{k}^{i}/f_{k}]_{k=1}^{n} M_{K}) ;

Σ[l_{k}^{i} ↦ (C(Y_{k})[[M_{k}^{i}]][M_{j}/x_{j}]_{j=1}^{m_{0}} [l_{k}^{i}/f_{k}]_{k=1}^{n}) ]_{k=1}^{n}⟩⟩σ =^{def} lhs′ →^{<n}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

Note the substitution of M_{j} terms for x_{j} variables in the range of Σ. It is this substitution that is replaced by passing x_{j} arguments explicitly in the lambda-lifted term on the right-hand side.

⟨3⟩2. Right-hand side reduces:

⟨⟨(case u_{i} (λf.f M_{Q} M_{K}) M_{int}) ; Σ′⟩⟩σ′

= ⟨⟨(case(R(X_{0})[[N_{0}^{i}]][l_{i}/f_{i}]_{i=1}^{n}) (λf.f M_{Q} M_{K}) M_{int})

; Σ′⟩⟩σ′ = ⟨⟨(case(inr(λx^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{0} x^{∗})(N_{0}^{i} κ′)σ_{0})[l_{i}/f_{i}]_{i=1}^{n})

(λf.f ⟨M_{1} … M_{m_{0}}⟩ M_{K}) M_{int})

; Σ′⟩⟩σ′

=_{pcf} ⟨⟨(N_{0}^{i} M_{K})[(M_{j}σ′)/x_{j}]_{j=1}^{m_{0}}[l_{i}/f_{i}]_{i=1}^{n} ; Σ′⟩⟩σ′

= ⟨⟨(N_{0}^{i}[M_{j}/x_{j}]_{j=1}^{m_{0}}[l_{i}/f_{i}]_{i=1}^{n} M_{K}) ; Σ′⟩⟩σ′

=^{def} rhs′

⟨3⟩3. Q.E.D.

To get (lhs′, rhs′) into S_{LL}, we have to add new entries to the σ_{v} and σ′_{v} substitutions (which track of the applications of the closures for the outer (lambda (X_{0}) …)). We use fresh variable v_{#v+1}, and note that no x_{j} is in the domain of σ or σ′, so we have:

\begin{matrix}lhs′ = & ⟨⟨(v_{#v+1} M_{K}) ; …⟩⟩ \\ σ[v_{#v+1} ↦ M_{0}^{i}[M_{j}/x_{j}]_{j=1}^{m_{0}}[l_{k}^{i}/f_{k}]_{k=1}^{n}] \end{matrix}

and similarly with the right-hand side. The two sides are easily seen to be in S_{LL}, with augmented σ_{v} and σ′_{v}’s, because we assume that Γ, 𝕏, 𝔽 ⊢ M_{0}^{i} ⇝^{LL_{body}} N_{0}^{i}:(Val→pr)→pr, and Lemma 6.2.3 allows us to substitute ⇝^{LL_{body}}-related terms and remain ⇝^{LL_{body}}-related.

⟨2⟩2. Case: M = v_{i}

Assume: ∧ σ_{v}(v_{i}) = M_{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}

∧ σ′_{v}(v_{i}) = N_{i}[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} [l_{i}/f_{i}]_{i=1}^{n}

∧ Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:pr,

∧ Σ(l_{k}^{i}) = (C(Y_{k})[[M_{k}^{i}]][l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}), for 1 ≤ k ≤ n

∧ Γ, 𝕏, 𝔽 ⊢ M_{x_{j}}^{i} ⇝^{LL_{body}} N_{x_{j}}^{i}:Val, for 1 ≤ j ≤ m_{0}

For this substep, we use induction on the derivation of Γ, 𝕏, 𝔽 ⊢ M_{i} ⇝^{LL_{body}} N_{i}:pr. The only interesting case is when the last step in the derivation is a use of the (app-f_{k}) rule:

120 CHAPTER 6. LAMBDA LIFTING

⟨3⟩1. Case: M_{i} = A[[f_{k}, M_{y_{1}}, …, M_{y_{m_{k}}} , M_{κ}]]

Assume: ∧ N_{i} = A′[[f_{k}, X_{k}, N_{y_{1}}, …, N_{y_{m_{k}}} , N_{κ}]]

∧ Γ, 𝕏, 𝔽 ⊢ M_{y_{j}} ⇝^{LL_{body}} N_{y_{j}}:(Val→pr)→pr, 1 ≤ j ≤ m_{k}

∧ Γ, 𝕏, 𝔽 ⊢ M_{κ} ⇝^{LL_{body}} N_{κ}:Val→pr

⟨4⟩1. Left-hand side reduces:

⟨⟨(deref l_{k}^{i} (λv_{f_{k}}:Val.M_{y_{1}} (λv_{1}:Val. … M_{y_{m_{k}}} (λv_{m_{k}}:Val.

out_{F} v_{f_{k}} (λf′:Val^{∗}→(Val→pr)→pr.

f′ ⟨v_{1} … v_{m_{k}}⟩ M_{κ}) …)))[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) ; Σ⟩⟩σ

→^{>0}_{left,sto} ⟨⟨M_{y_{1}} (λv_{1}…. M_{y_{m_{k}}} (λv_{m_{k}}.

out_{F} (C(Y_{k})[[M_{k}^{i}]][l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}})

(λf′.f′ ⟨v_{1} … v_{m_{k}}⟩ M_{κ}) …))

[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ⟩⟩σ

=_{pcf} ⟨⟨M_{1} (λv_{1}…. M_{m_{k}} (λv_{m_{k}}.

(λy^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{k} y^{∗})(M_{k}^{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) σ_{k} κ′)

⟨v_{1} … v_{m_{k}}⟩ M_{κ}) …)

[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ⟩⟩σ

=_{pcf} ⟨⟨M_{1} (λy_{1}…. M_{m_{k}} (λy_{m_{k}}.

(M_{k}^{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) M_{κ}) ⋯)

[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ⟩⟩σ = ⟨⟨M_{1} (λy_{1}…. M_{m_{k}} (λy_{m_{k}}.

(M_{k}^{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}}) M_{κ}) ⋯) ; Σ⟩⟩σ =^{def} lhs′ →^{<n}_{left,sto} ⟨⟨io M′ ; Σ′_{M}⟩⟩

⟨4⟩2. Right-hand side reduces:

= ⟨⟨(deref l_{k} (λv_{f_{k}}:Val.N_{y_{1}} (λv_{1}:Val. … N_{y_{m_{k}}} (λv_{m_{k}}:Val.

out_{F} v_{f_{k}} (λf′:Val^{∗}→(Val→pr)→pr.

f′ ⟨[x_{i}]_{∈ X_{k}} v_{1} … v_{m_{k}}⟩ N_{κ}) …))))[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ′⟩⟩σ′

→_{sto}^{∗} ⟨⟨N_{y_{1}} (λv_{1}…. N_{y_{m_{k}}} (λv_{m_{k}}.

out_{F} C′(X_{k}, Y_{k})[[N_{k}]][l_{i}/f_{i}]_{i=1}^{n}

(λf′.f′ ⟨[x_{i}]_{∈ X_{k}} v_{1} … v_{m_{k}}⟩ N_{κ}) …))[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ′⟩⟩σ′

=_{pcf} ⟨⟨N_{1} (λv_{1}…. N_{m_{k}} (λv_{m_{k}}.

(λy^{∗}:Val^{∗}.λκ′:Val→pr.(checkargs m_{k} y^{∗})N_{k}σ′_{k} κ′)[l_{i}/f_{i}]_{i=1}^{n}

⟨[x_{i}]_{∈ X_{k}} v_{1} … v_{m_{k}}⟩ N_{κ}) …)[N_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}} ; Σ′⟩⟩σ′

=_{pcf} ⟨⟨N_{1} (λy_{1}…. N_{m_{k}} (λy_{m_{k}}.

N_{k} N_{κ}) …)[l_{i}/f_{i}]_{i=1}^{n}[N_{x_{j}}^{i}/x_{j}]_{x_{j}∈X_{k}} ; Σ′⟩⟩σ′

=^{def} rhs′

The last =_{pcf} equality depends on the fact that the vector of values passed in matches the σ′_{k} substitution applied to the body of the closure. In particular, the first #X_{k} elements of the value vector correspond to the x_{j}’s that were added by lambda-lifting, and the values given by [N_{x_{j}}^{i}/x_{j}]_{x_{j}∈X_{k}} make their way into the closure.

⟨4⟩3. Q.E.D. (lhs′, rhs′) ∈ S_{LL} by adding elements to σ_{v} and σ′_{v}. To make this clear, we rewrite lhs′ as follows:

\begin{matrix}lhs′ = & ⟨⟨M_{1} (λy_{1}…. M_{m_{k}} (λy_{m_{k}}. \\ (v_{#v+1} M_{κ}) ⋯) ; Σ⟩⟩σ′′ \end{matrix}

Where σ′′ = σ[v_{#v+1} ↦ (M_{k}^{i}[l_{k}^{i}/f_{k}]_{k=1}^{n}[M_{x_{j}}^{i}/x_{j}]_{j=1}^{m_{0}})] and likewise for the right-hand side.

⟨2⟩3. All other cases Are easy, as the locations involved will never be the crucial l_{k} constants.

The correctness result we want follows easily:

Theorem 6.2.6 (Correctness of Incremental Lambda Lifting) For any Scheme_{cell} expression e and list of lists of variables 𝕏 such that e is lambda-liftable with respect to 𝕏, and any Γ mapping the free variables of e to ref (Val), if Γ ⊢_{cell} e:ok, then

Γ ⊢ [[e]]_{cell} ≅_{∀C} [[LL(𝕏, e)]]_{cell}:(Val→pr)→pr

Proof:

1. By the Extensionality Theorem, Theorem 2.8.1, and the definition of ≅_{ext}, it suffices to show that for all closing substitutions σ mapping free variables to closed terms of type ref (Val), all closed terms K of type Val→pr, and all stores Σ,

⟨⟨([[e]]_{cell}σ) K ; Σ⟩⟩ ≈_{sim} ⟨⟨([[LL(𝕏, e)]]_{cell}σ) K ; Σ⟩⟩

2. It is easy to show that for all K and Σ,

(⟨⟨([[e]]_{cell}σ) K ; Σ⟩⟩, ⟨⟨([[LL(𝕏, e)]]_{cell}σ) K ; Σ⟩⟩) ∈S_{LL}

as S_{LL} was defined exactly for this purpose.

3. By Lemma 6.2.5 and steps 1 and 2, the correctness result follows.

Conclusions and Open Problems

In [RP95], Ritter and Pitts write:

It remains an open problem to find a co-inductive characterization of observational equivalence for languages like SML that combine higher order functions and local state.

We have solved this open problem with the metalanguage defined in this thesis. As such, the results obtained so far are of independent interest. Additionally, we have applied the metalanguage and its theory to substantial applications from an actual compiler for the programming language Scheme, producing the first known proofs of correctness of two subtle transformations.

7.1 Open Problems – Future Work

The actual proofs given in Chapters 5 and 6 might appear somewhat inscrutable to some readers^{1}. It has been our experience that, despite the syntactic complexity of the proofs, the process of (1) devising an appropriate candidate simulation relation, and (2) doing the ensuing coinductive proof, is fairly predictable. As such, it seems that the methods we use might be amenable to automation. With a good theorem prover and a well-developed set of examples and previous proofs, it may be possible to hide much of the detail and make proofs of correctness such as those presented in this thesis accessible to a wider audience of programmers and compiler writers. Similarly, we believe that some of the predictability and repetitiveness of the proofs can be encompassed by a more robust metatheory for the metalanguage. It would be interesting to add polymorphism to the type system in order to apply our methods to languages such as ML and object-oriented languages. A first-order exploration of bisimilarity in an object calculus is presented in [GR96]. Generalizing our method to be parameterized by the notion of observation, and extending the framework to handle concurrency, would also be fruitful areas of research. A starting point for this avenue of research is [San94].

1or, more likely, complete gibberish to all readers

Bibliography

[Abr90] Samson Abramsky. The lazy lambda calculus. In David A. Turner, editor, Research Topics in Functional Programming, pages 65–116. Addison-Wesley, 1990.

[App92] Andrew W. Appel. Compiling with Continuations. Cambridge University Press, Cambridge, 1992.

[Bar81] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics. North-Holland, Amsterdam, 1981.

[CH94] William D. Clinger and Lars Thomas Hansen. Lambda, the ultimate label, or a simple optimizing compiler for scheme. In Proc. 1994 ACM Symposium on Lisp and Functional Programming, pages 128–139, 1994.

[Cli84] William Clinger. The scheme 311 compiler: An exercise in denotational semantics. In Proc. 1984 ACM Symposium on Lisp and Functional Programming, pages 356–364, August 1984.

[CR91] William Clinger and Jonathan A. Rees. The revised^{4} report on the algorithmic language scheme. ACM LISP Pointers, 4(3), 1991.

[EHR91] L. Egidi, F. Honsell, and S. Ronchi della Rocca. The lazy call-by-value λcalculus. In proceedings of MFCS ’91 Lecture Notes in Computer Science, 1991.

[FF86] M. Felleisen and D. Friedman. Control operators, the SECD machine and the λ-calculus. In Formal Description of Programming Concepts III, pages 131–141. North-Holland, 1986.

[FH92] M. Felleisen and R. Hieb. The revised report on the syntactic theories of sequential control and state. Theoretical Computer Science, 103:235–271, 1992.

[FWH92] Daniel P. Friedman, Mitchell Wand, and Christopher T. Haynes. Essentials of Programming Languages. MIT Press, Cambridge, MA, 1992. Also McGraw-Hill, Chicago, 1992.

[Gor94a] Andrew Gordon. A tutorial on co-induction and functional programming. In Proceedings of the 1994 Glasgow Workshop on Functional Programming, pages 78–95. Springer Workshops in Computing, 1994.

[Gor94b] Andrew D. Gordon. Functional Programming and Input/Output. Cambridge University Press, Cambridge, 1994.

[Gor95] Andrew D. Gordon. Bisimilarity as a theory of functional programming. In Proceedings of 11th Conference on Mathematical Foundations of Programming Semantics, 1995.

[GR96] Andrew D. Gordon and Gareth D. Rees. Bisimilarity for a first-order calculus of objects with subtyping. In Conf. Rec. 23rd ACM Symposium on Principles of Programming Languages, pages 386–395, 1996.

[GSR95] J. D. Guttman, V. Swarup, and J. Ramsdell. The VLISP verified scheme system. Lisp and Symbolic Computation, 8(1/2):33–110, 1995.

[Gun92] Carl A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, Cambridge, MA, 1992.

[HM85] Matthew Hennessy and Robin Milner. Algebraic laws for nondeterminism and concurrency. Journal of the ACM, 32:137–161, 1985.

[HMST95] Furio Honsell, Ian A. Mason, Scott Smith, and Carolyn Talcott. A variable typed logic of effects. Information and Computation, 119:55–90, 1995.

[How89] Douglas J. Howe. Equality in lazy computation systems. In Proc. 4th IEEE Symposium on Logic in Computer Science, pages 198–203, 1989.

[How95] Douglas J. Howe. A note on proving congruence of bisimulation in a generalized lambda calculus. unpublished manuscript, 1995.

[How96] Douglas J. Howe. Proving congruence of bisimulation in functional programming languages. to appear in Information and Computation, 1996.

[IEE91] IEEE Computer Society, New York. IEEE Standard for the Scheme Programming Language, IEEE standard 1178-1990 edition, 1991.

[JM91] Trevor Jim and Albert R. Meyer. Full abstraction and the context lemma. Technical Report MIT/LCS/TR-524, MIT Laboratory for Computer Science, December 1991.

[KH89] Richard Kelsey and Paul Hudak. Realistic compilation by program transformation. In Conf. Rec. 16th ACM Symposium on Principles of Programming Languages, pages 281–292, 1989.

[KKR^{+}86] David A. Kranz, Richard Kelsey, Jonathan A. Rees, Paul Hudak, James Philbin, and Norman I. Adams. Orbit: An optimizing compiler for scheme. In Proceedings SIGPLAN ’86 Symposium on Compiler Construction, 1986. SIGPLAN Notices 21 (7), July, 1986, 219-223.

[Lam93] Leslie Lamport. How to write a proof. Technical Report SRC-094, Digital Systems Research Center, feb 1993. Available by FTP from gatekeeper.dec.com

in the directory /archive/pub/DEC/SRC/research-reports. It is file
SRC-094.ps.Z.

[Mil77] Robin Milner. Fully abstract models of typed lambda-calculi. Theoretical Computer Science, 4:1–22, 1977.

[Mil90] Robin Milner. Operational and algebraic semantics of concurrent processes. In Jan van Leeuwen, editor, Handbook of Theoretical Computer Science, pages 1201–1242. MIT Press/Elsevier, 1990.

[Mit96] John C. Mitchell. Foundations for Programming Languages. MIT Press, Cambridge, MA, 1996.

[Mor68] James H. Morris, Jr. Lambda Calculus Models of Programming Languages. PhD thesis, MIT, Cambridge, MA, 1968.

[MS88] Albert R. Meyer and Kurt Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Conf. Rec. 15th ACM Symposium on Principles of Programming Languages, pages 191–203, 1988.

[MT91] Ian A. Mason and Carolyn L. Talcott. Equivalence in functional languages with effects. Journal of Functional Programming, 1:287–327, 1991.

[MTH89] Robin Milner, Mads Tofte, and Robert Harper. The Definitiion of Standard ML. MIT Press, Cambridge, MA, 1989.

[Ode94] Martin Odersky. A functional theory of local names. In Conference Record of POPL ’94: 21st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 48–59, 1994.

[ORW95] Dino P. Oliva, John D. Ramsdell, and Mitchell Wand. The VLISP verified prescheme compiler. Lisp and Symbolic Computation, 8(1/2):111–182, 1995.

[OT95] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. Journal of the ACM, 42(3):658–709, May 1995.

[Pit99] A. M. Pitts. Operationally-based theories of program equivalence. In P. Dybjer and A. M. Pitts, editors, Semantics and Logics of Computation. Cambridge University Press, 199? Based on lectures given at the CLICS-II Summer School on Semantics and Logics of Computation, Isaac Newton Institute for Mathematical Sciences, Cambridge UK, September 1995.

[PJ87] Simon L. Peyton Jones. The Implementation of Functional Programming Languages. Prentice-Hall International, 1987.

[PJW93] Simon L. Peyton Jones and Philip L. Wadler. Imperative functional programming. In Proceedings 20th Annual ACM Symposium on Programming Languages, pages 71–84, 1993.

[Plo75] Gordon D. Plotkin. Call-by-name, call-by-value and the λ-calculus. Theoretical Computer Science, 1:125–159, 1975.

[Plo77] Gordon D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5:223–255, 1977.

[PS93] A. M. Pitts and I. D. B. Stark. Observable properties of higher order functions that dynamically create local names, or: What’s new? In Mathematical Foundations of Computer Science, Proc. 18th Int. Symp., Gdańsk, 1993, volume 711 of Lecture Notes in Computer Science, pages 122–141. Springer-Verlag, Berlin, 1993.

[Ram96] John D. Ramsdell. personal communication, July 1996.

[Rey81] John C. Reynolds. The essence of Algol. In J. W. deBakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372. North-Holland, Amsterdam, 1981.

[Rey83] John C. Reynolds. Types, abstractions, and parametric polymorphism. In Proceedings IFIP 83, 1983.

[RP95] E. Ritter and A. M. Pitts. A fully abstract translation between a λ-calculus with reference types and Standard ML. In 2nd Int. Conf. on Typed Lambda Calculus and Applications, Edinburgh, 1995, volume 902 of Lecture Notes in Computer Science, pages 397–413. Springer-Verlag, Berlin, 1995.

[RV95] Jon G. Riecke and Ramesh Viswanathan. Isolating side effects in sequential languages. In Conf. Rec. 22nd ACM Symposium on Principles of Programming Languages, pages 1–12, 1995.

[San94] Davide Sangiorgi. The lazy lambda calculus in a concurrency scenario. Information and Computation, 111(1):120–153, May 1994.

[San96] David Sands. Total correctness by local improvement in the transformation of functional programs. ACM Transactions on Programming Languages and Systems, 18:175–234, march 1996.

[SRI91] Vipin Swarup, Uday S. Reddy, and Evan Ireland. Assignments for applicative languages. Lecture Notes in Computer Science, 523:192–??, 1991.

[Sta94] Ian Stark. Names and Higher-Order Functions. PhD thesis, University of Cambridge, December 1994. Also published as Technical Report 363, University of Cambridge Computer Laboratory.

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

[TW96] Jerzy Tiuryn and Mitchell Wand. Untyped lambda-calculus with input-output. In H. Kirchner, editor, Trees in Algebra and Programming: CAAP’96, Proc. 21st International Colloquium, volume 1059 of Lecture Notes in Computer Science, pages 317–329, Berlin, Heidelberg, and New York, April 1996. Springer-Verlag.

[Wad92] Philip Wadler. Comprehending monads. Mathematical Structures in Computer Science, 2(4):461–493, December 1992.

[Wan90] Mitchell Wand. A short proof of the lexical addressing algorithm. Information Processing Letters, 35:1–5, 1990.

[Win93] Glynn Winskel. The Formal Semantics of Programming Languages. MIT Press, Cambridge, MA, 1993.

[WO92] Mitchell Wand and Dino P. Oliva. Proving the correctness of storage representations. In Proc. 1992 ACM Symposium on Lisp and Functional Programming, pages 151–160, 1992.