i

The Category of Functors from State Shapes to Bottomless CPOs is Adequate for Block

Structure

Arthur Franklin Lent Masachusetts Institute of Technology

Laboratory for Computer Science February 12, 1993

Abstract

We present a programming language EoA, which embodies what Reynolds has described as the “essence of Algol.” In particular, EoA allows higher-order procedures and the declaration of block structured local variables. We develop a Plotkin-style Structured Operational Semantics for EoA. We present Tennent had developed a denotational model which aims to capture the semantics of stack allocated local variables. Tennent’s denotational model for EoA, which, although not fully-abstract, appears to be the best model of block structure developed to this date. Tennent’s model is based a category of functors from a collection of store shapes (possible worlds) to the category of bottomless cpos. The model is based on ideas pioneered in the early 1980’s by Reynolds and Oles. The main result of this thesis is to prove that Tennent’s model is adequate for EoA. We then abstract away some of the details of Tennent’s model and state sufficient conditions for a functor category to be adequate for EoA. This thesis concludes with a comparison of the best known models of block structure, and discusses where Tennent’s model fails to reach full abstraction.

Keywords: Algol, operational semantics, denotational semantics, adequate, fully abstract

Acknowledgments

I would first like to thank my advisor, Albert R. Meyer for suggesting the project and for his time spent discussing the research and suggestions for improving this thesis. I would also like to thank P. O’Hearn, K. Sieber, R. Tennent, and D. Wald for their comments on drafts of this thesis and many helpful technical discussions. I would also like to thank D. Jones and D. Wald for helpful comments regarding the formatting of this thesis. I would especially like to thank my wife, Nicole Sherry Skinner, for providing moral support when I needed it. Finally, I gratefully acknowledge the financial support of an ONR graduate fellowship.

Remarks

This is a slightly revised version of [8]. In particular, Section 4.3 had been added, some notation has been changed, and numerous typos have been corrected.

Contents

1 Introduction 1 1.1 Algol-like Languages . . . . . . . . . . . . . . . . . . . . . . . . 1 1.2 Reynolds’s “Essence of Algol” . . . . . . . . . . . . . . . . . . . 2

1.2.1 Imperative Types . . . . . . . . . . . . . . . . . . . . . . . 2 1.2.2 Kernel Syntax . . . . . . . . . . . . . . . . . . . . . . . . 4 1.2.3 Syntactic Sugar . . . . . . . . . . . . . . . . . . . . . . . . 5

2 Definition of EoA 7 2.1 Differences Between EoA and Reynolds’s Essence of Algol … 7 2.2 Kernel Syntax . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9

2.2.1 Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 9 2.2.2 Identifiers and Terms . . . . . . . . . . . . . . . . . . . . . 10 2.2.3 Free and Bound Identifiers, Substitution, and Closed Terms 12

2.3 Assigning Operational Semantics . . . . . . . . . . . . . . . . . . 14 2.4 Properties of →_{L} . . . . . . . . . . . . . . . . . . . . . . . . . . . 16 2.5 Observations . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17

3 Defining the Denotational Model 23 3.1 Functor Category Models of Simply Typed Lambda Calculi … 24 3.2 The Category D . . . . . . . . . . . . . . . . . . . . . . . . . . . 26 3.3 Constructing the C.C.C. . . . . . . . . . . . . . . . . . . . . . . . 26 3.4 A Model of EoA . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3.4.1 The Category of Possible Worlds, W . . . . . . . . . . . . 29 3.4.2 Interpreting Types . . . . . . . . . . . . . . . . . . . . . . 30 3.4.3 Interpreting Constants and Terms . . . . . . . . . . . . . 33

3.5 Definitions Needed for Adequacy . . . . . . . . . . . . . . . . . . 36 3.5.1 A Sequence of Worlds . . . . . . . . . . . . . . . . . . . . 36 3.5.2 Meanings for Bindings: Environments . . . . . . . . . . . 37 3.5.3 Interpreting Configurations . . . . . . . . . . . . . . . . . 38 4 Adequacy 39

4.1 Soundness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 40 4.2 The Computability Relation . . . . . . . . . . . . . . . . . . . . . 41

4.2.1 Proving All Lterms Computable . . . . . . . . . . . . . . 43 4.2.2 Handling Y . . . . . . . . . . . . . . . . . . . . . . . . . . 46

4.3 A General Adequacy Theorem for Functor Category Models … 48

5 Comparing Models of Block Structure 51 5.1 Advanced Models of Block Structure . . . . . . . . . . . . . . . . 51 5.2 The Meyer-Sieber Examples . . . . . . . . . . . . . . . . . . . . . 52 5.3 Failure of Full Abstraction . . . . . . . . . . . . . . . . . . . . . . 58

6 Conclusion 60

Chapter 1

Introduction

The goal of this thesis is to present a language which embodies many of the essential features of an a Algol-like language which we call EoA. The language EoA is a minor variant of Reynolds’s “essence of Algol[20]”. In Chapter 2 we define the syntax of EoA and develop a Plotkin-style Structured Operational Semantics for EoA [19]. In Chapter 3 we present Tennent’s denotational semantics for EoA [12–14, 24, 25], which, although not fully-abstract, appears to be the best semantics of EoA developed to this date. Tennent’s model is based on ideas pioneered in the early 1980’s by Reynolds and Oles [15–17, 21]. The model uses the category of functors from a collection of store shapes (possible worlds) to the category of bottomless cpo’s. Chapter 4 contains the main technical result of this thesis—a proof that Tennent’s model is adequate for EoA. We then abstract away some of the details of Tennent’s model and state some sufficient conditions for a functor category model to be adequate for EoA. Chapter 5 includes a discussion of how the Tennent model handles the Meyer-Sieber Examples [9], and discusses two counterexamples to full abstraction.

The remainder of this Chapter provides a general description of the criteria for “Algol-like languages” and presents a quick overview of Reynolds’s “essence of Algol.”

1.1 Algol-like Languages

We follow the work of Reynolds [20] and Halpern, Meyer and Trakhtenbrot [4, 26] in taking the following four principles as characterizing the class of Algol-like languages:

1. There is a consistent distinction between commands (or programs) which alter the store but do not return values, and expressions which return values but have no side-effects on the store.

2. The only explicit calling mechanism is by-name. (For parameters of basic data types, other mechanisms such as by-value or by-reference are available by simulation (syntactic sugaring).)

3. The language is fully typed. Higher-order procedures of all finite types (in Algol jargon, modes) are allowed. There is a clear distinction between locations and storable values.

4. The stack discipline is an explicit aspect of the semantics. Note that this discipline should be understood as a language design principle encouraging modularity in program construction rather than as an implementation technique for efficient storage management. It is better called the local storage discipline to avoid misunderstanding, and we do so henceforth.

—Trakhtenbrot, Halpern, and Meyer[26]

1.2 Reynolds’s “Essence of Algol”

A key observation embodied in Reynolds’s essence of Algol is that Algol is essentially a simply-typed functional language. With a careful understanding of types and call-by-name as the only built in parameter-passing mechanism, we can see that β-equivalence is a sound reasoning principle for Algol! Consequently, the kernel syntax of Reynolds’s essence of Algol is a simply typed λ-calculus over the appropriate base types and constants required to capture the imperative features of Algol. Although the only parameter passing mechanism explicitly present in the essence of Algol is call-by-name, the mechanisms of call-by-value and call-by-reference for storable data types can easily be simulated.

1.2.1 Imperative Types

To understand Reynolds’s essence of Algol, we must understand his view of imperative types. Since the local storage discipline is essentially incompatible with storing state-dependent objects, there is a clear distinction between data and phrase types. Essentially, data types are those primitive entities which we can “store” (i.e. those which are kept track of in the state), whereas phrase types are the types which code can take on. Some examples of plausible data types are real, integer, and boolean. Some examples of plausible phrase types are real thunks, integer thunks, and commands. For an Algol-like language, the data types are “state independent,” whereas all of the phrase types implicitly involve the state in some way.

For each data type, there corresponds a phrase type for talking about such values. Reynolds takes as primitive data types: real, integer, and boolean, so the base phrase types corresponding to these basic data types are: exp[real], exp[integer], and exp[boolean]. For example, an object of type exp[real] is a “real exp(ressor)”—something which manages to read a real from the state. From the point of view of this thesis and in spite of our suggestive notation, exp[ ·] is not to be considered a general type constructor. Code can not take on the type integer. Code takes on the type exp[integer]. From the point of view of programming in “essence of Algol,” the phrase type integer does not exist. All “expressions” in an imperative language have an implicit ability to depend on the state. It would be possible to augment our collection of phrase types by a type which corresponded to “pure” (state-independent) integers. Most code, however, is actually written to expect the more general (state-dependent) expressions. Moreover, since expressions are side-effect free, there seems to be little motivation to make a distinction between the integer “5” and the thunk “\underline{5}” which in any state evaluates to the integer 5.

Another base phrase type is comm. We have already noted that a fundamental criterion for being an “Algol-like language,” is that expressions return values, but do not have side-effects on the state. All side-effects are restricted to occur at the type comm. Terms of type comm correspond to statements in the more traditional jargon.

The most fundamental notion of an imperative language is the variable.^{1} Many authors model variables by locations. Some authors make the location-like behavior of variables an explicit part of the syntax of the languages (sometimes introducing a type “location” in place of the type “variable”). We follow the view that it is best not to commit to such representation issues at the level of the language design (Note: we will be modeling variables by locations). A variable has within it the ability to either write an element of a data type in the state, or read an element of a data type from the state. Consequently, we have the phrase types: var[real], var[integer], and var[boolean]. In fact we can view a variable as consisting of two separate components: a reading component, and a writing component. The reading component of a variable of type var[τ] (which corresponds to what is often called the r-value), would have type exp[τ]. The writing component of a variable (which corresponds to what is often called the l-value), could be viewed as type exp[τ] → comm. The writing component is a state-to-state mapping which is parameterized by a state-dependent element of the data type τ. Reynolds calls the writing component of a variable an acceptor, and gives acceptors their own phrase type. So, essentially a var[τ] is a exp[τ] paired with an acc[τ].

Reynolds also addresses the issue of subtyping of data types in his definition of the essence of Algol. Since we feel that the issues of subtyping data types and implicit coercions are largely orthogonal to the issue of local variables, from here on we will describe Reynolds’s essence of Algol as though it does not have the data type real. We also feel that having the data type boolean does not raise any substantial issues in the context of local variables; we will also drop it from our discussion. The fact that we only have a single storable data type will allow us to simplify syntax in several ways. For example, we can now use exp for exp[integer], acc for acc[integer], and var for var[integer]. It will also allow us to simplify the syntax of local-variable-declaration blocks, as all of our local variables will be for the data type integer.

1We break with somewhat traditional terminology in programming language semantics, and use “variable” in the traditional programming sense—something which allows the state to be accessed or changed. We use “identifier” in the sense in which logicians have traditionally used variable, i.e. to denote a place holder in a term. So in this thesis, a variable is something we read from or write to, whereas an identifier appears free in a term, or is bound by a λ or some other binding construct.

1.2.2 Kernel Syntax

Now, given this intuitive understanding of types, we can understand the kernel syntax of Reynolds’s essence of Algol as a simply typed λ-calculus with base types exp, acc, var, and comm, with appropriate typed constants and a few extra term constructors. When talking informally, we will write our binary operators in infix notation, e.g. writing c_{0} ; c_{1} instead of ((seq c_{0}) c_{1}). For our proofs however, we restrict ourself to the “correct” syntax.

The constants of type exp are simply the numerals, namely 0, 1, 2, … At type comm, there is only one constant—the do nothing command skip. There are no constants of type acc or var. There are also a variety of constants of higher type. For example, conditionals are uniformly available at all types. We will write the conditional constant for type θ as IFexp_{θ}; it has type exp → θ → θ → θ. The intended semantics of IFexp_{θ} will be that if the exp evaluates to 0 then the first consequent of the conditional will be used, if the exp evaluates to a non-zero integer then the second consequent of the conditional will be used.

There are also assignment operators, :=, for the types acc and var. The intended semantics of the command a := e is the command which assigns the value of expressor e in the current store to the variable whose updating component is a. The intended semantics of v := e is the command which assigns the value of expressor e in the current store to the variable v.

We also have curried versions of the standard arithmetic operations, which operate on types just built up from exp.^{2} For example we have succ : exp → exp, and plus : exp → (exp → exp).

The standard λ-calculus term constructors of application and λ-abstraction (λ ι : θ ▪ M) are a part of the essence of Algol. There is also a term constructor rec which behaves like a least fixpoint operator. Finally, there is also an operator newvar of type var → comm → comm which is used for local variable declarations.

2Due to the availability of implicit conversions they can also operate on var arguments.

1.2.3 Syntactic Sugar

The full version of Reynolds’s essence of Algol is the kernel language augmented by six sugaring constructs: higher-order conditionals, multiple abstraction, multiple application, let, letrec, and New v in B. For completeness, we provide the sugared and desugared constructs, even though this is now fairly well established in the literature. Our treatment is largely taken from that of Tennent [24].

Our first bit of sugar is higher-order conditionals. Since our the intended parameter passing mechanism is call-by-name, we can define IFexp_{θ→θ′} as follows:

IFexp_{θ→θ′} =_{df} λe:exp▪λp_{1} :θ → θ′▪λp_{2} :θ → θ′▪λq:θ▪(IFexp_{θ′} e (p_{1}q) (p_{2}q))

When there is ambiguity about parenthesis, we assume application associates to the left.

The next sugaring construct allows multi-parameter procedures (and thus also applications of multi-parameter procedures) via currying:

\frac{π[ι_{1} :θ_{1}, … ι_{n}:θ_{n}] ⊢ P:θ}{λ(ι_{1} :θ_{1}, …, ι_{n}:θ_{n})▪P:θ_{1} × ⋯ × θ_{n} → θ}

\frac{π ⊢ P:(θ_{1} × ⋯ × θ_{n}) → θ π ⊢ Q_{1} :θ_{1} ⋯ π ⊢ Q_{n}:θ_{n}}{π ⊢ P (Q_{1}, …, Q_{n}):θ}

So our desugaring is:

λ(ι_{1} :θ_{1}, …, ι_{n}:θ_{n})▪P =_{df} λι_{1} :θ_{1}▪ … ▪λι_{n}:θ_{n}▪P
P (Q_{1}, …, Q_{n}) =_{df} P (Q_{1}) ⋯ (Q_{n})

Reynolds’s essence of Algol uses a convenient notation for making (nonrecursive) local definitions in programs which was suggested by Landin [7]:

\frac{π[ι_{1} :θ_{1}, …, ι_{n}:θ_{n}] ⊢ Q:θ π ⊢ P_{i}:θ_{i}(for i = 1, 2, …, n)}{π ⊢ let ι_{1} be P_{1} & ⋯ & ι_{n} be P_{n} in Q:θ}

The let does not bind ι_{1}, …, ι_{n} in any of P_{1}, …, P_{n}. A let creates a nonrecursive set of declarations, in which Q gets evaluated (the letrec construct, which will be described shortly is used for setting up a possibly mutually recursive set of declarations in which Q can be evaluated). Also, since our premises are of the form π ⊢ P_{i}:θ_{i}, rather than π[ι_{1} : θ_{1}, …, ι_{n}:θ_{n}], we did not need to include the types of ι_{1}, …, ι_{n} explicitly in the let construct; these types can be inferred by looking at the P_{i}’s.

Our desugaring is:

let ι_{1} be P_{1} & ⋯ & ι_{n} be P_{n} in Q =_{df} (λι_{1} :θ_{1}▪, ⋯ λι_{n}:θ_{n}▪Q)(P_{1}) ⋯ (P_{n})

Reynolds’s essence of Algol also uses a convenient notation for making possibly recursive local definitions in programs (also from Landin):

\frac{π[ι_{1} :θ_{1}, …, ι_{n}:θ_{n}] ⊢ Q:θ π[ι_{1} :θ_{1}, …, ι_{n}:θ_{n}] ⊢ P_{i}:θ_{i}(for i = 1, 2, …, n)}{π ⊢ letrec ι_{1} :θ_{1} be P_{1} & ⋯ & ι_{n}:θ_{n} be P_{n} in Q:θ}

The letrec construct does bind ι_{1}, …, ι_{n} in all of P_{1}, …, P_{n} (and also, of course, Q). Also, it is no longer possible to infer θ_{i} merely from π and P_{i}; consequently the θ_{i}’s must appear explicitly in the letrec construct.

Desugaring a letrec is a little harder. We first show how to desugar the case when n = 1. Then we reduce the case of n > 1 to the case of n = 1. For the non-multiple case (n = 1), we have:

letrec ι_{1} :θ_{1} be P_{1} in Q =_{df} (λι_{1} :θ_{1}▪Q)(rec λι_{1} :θ_{1}▪P_{1})

We reduce the case of multiple cases to the single case by using Bekić’s theorem [2, 27]. In our notation, Bekić’s theorem reads as follows:

Theorem 1 (Bekić)

letrec ι_{1} :θ_{1} be P_{1} & ι_{2} :θ_{2} be P_{1} in Q
= letrec ι_{1} :θ_{1} be (letrec ι_{2} :θ_{2} be P_{2} in P_{1})
in (letrec ι_{2} :θ_{2} be P_{2} in Q)

Bekić’s theorem obviously generalizes to handle n ≥ 3 as follows:

letrec ι_{1} :θ_{1} be P_{1} & ι_{2} :θ_{2} be P_{2} & ⋯ & ι_{n}:θ_{n} be P_{n} in Q

= letrec ι_{1} :θ_{1}be (letrec ι_{2} :θ_{2} be P_{2} & ⋯ & ι_{n}:θ_{n} be P_{n} in P_{1})

in (letrec ι_{2} :θ_{2} be P_{2} & ⋯ & ι_{n}:θ_{n} be P_{n} in Q)

The final piece of sugar in Reynolds’s essence of Algol which is worth mentioning here is variable declaration blocks. The syntax of such a block is:

\frac{π[ι:var[τ]] ⊢ P:comm}{π ⊢ New[τ] ι in P:comm}

Formally, we could let the binding be done by a λ-expression, and then introduce a typed constant newvar_{τ} into the language in order to capture the rest of the intention of the declaration. This then gives us the following desugaring:

New[τ]ι in P =_{df} newvar_{τ} (λι:var[τ]▪P).

Note: since we have dropped all data types other than integer, we do not even need to explicitly mention τ in the declaration, thus giving New ι in P, and the desugaring newvar (λι:var▪P) instead.

Definition of EoA

The language EoA is built upon a simply typed λ-calculus over base types exp and comm. In addition to the standard λ-calculus term constructors of λ-abstraction and application, EoA contains a term constructor New for expressing local-variable declaration blocks. EoA contains typed constants for basic arithmetic operations on exp. Recursion is uniformly available at all types. Conditionals are provided for the base types, and are uniformly definable for higher types. The “do nothing” command skip is available, as is sequencing of commands. For simplicity there is only one basic data type, which we assume to be the non-negative integers; it should be a routine exercise to modify the results here to extend EoA with additional basic data types (such as booleans or characters).

2.1 Differences Between EoA and Reynolds’s Essence of Algol

There are three fundamental differences EoA between and Reynolds’s essence of Algol. First, the only storable data type of EoA is integer, whereas Reynolds also considers real and boolean. We do not consider the data type real, because our primary interest is in understanding the nature of block structured local variables, and we believe that the issue of subtyping and implicit coercions is largely orthogonal to the issue of block structured local variables. For simplicity, we also do not have boolean as a basic data type. We expect that it would be a routine exercise to extend the work here to handle additional basic data types.^{1}

The second fundamental difference is the lack of the type var(iable) in EoA, although we do retain acc(eptor) and exp(ressor). The technical justifications for eliminating var appear in Section 2.2.1. EoA treats acc as a type synonym for exp → comm. A fundamental consequence of the lack of var and the change to acc is that we no longer need coercions (implicit or explicit) from var to acc or exp. Reynolds’s essence of Algol provides an implicit coercion from the type var to exp. When we think of acc as merely a type synonym for exp → comm, we see that the assignment operator := merely functions as an explicit coercion from var to (exp → comm). Of course, there will be some minor syntactic modifications to new-variable blocks. For example, in the sugared language the New structure will now need to take two identifiers in addition to the block-body as argument (where one identifier will be tied to the writing component of the newly allocated variable, and the other tied to its reading component).

1Although we expect it to be simple to extend the language with other basic data types, we have not thought carefully about extending our results for a version of EoA extended with a rich structure of subtypes and implicit coercions.

The final substantial difference between EoA and Reynolds’s essence of Algol is that in EoA, identifiers come explicitly with types—as opposed to using a simply-typed lambda calculus based on untyped identifiers. Specifically, Reynold’s essence of Algol uses typing judgments of the form π ⊢ M : θ, and lambda abstraction takes the form λx : θ▪M. In EoA, typing judgments are unnecessary, and lambda abstraction looks like λx▪M, where x, by definition, has some specified type. We make this simplification for expository reasons. A suitable version of the adequacy result also holds for the version with untyped identifiers, but some substantial changes do need to be made to the definitions for it to work.

There are two other minor differences between EoA and Reynolds’s essence of Algol, both existing to simplify our exposition. For reasons which arise when defining the operational semantics of EoA, we find it more convenient not to use Reynolds’s desugaring of new variable declarations. Thus we leave New as a term constructor in EoA. Moreover, since we keep New structures in our kernel language, we do not bother to introduce the constant newvar. There is one additional change to the New structure. We find it useful to include a fourth component in a New structure—an argument of type exp which will provide the initial value of the newly allocated location. So, if E is a term of type exp, P a term of type comm, ι an identifier of type acc, and κ an identifier of type exp, then (New ι, κ ← E in P) is a term of type comm.

Finally, we introduce a collection of recursion constants Y_{θ}, one for each type θ. The constant Y_{θ}, has type (θ → θ) → θ. These constants enable us to discard the term constructor rec. Specifically if M is a term of type θ → θ, then in EoA we use (Y_{θ} M), instead of (rec M).

The rest of this Chapter consists of a formal definition of the syntax and operational semantics of EoA and a precise statement of our definition of adequacy.

2.2 Kernel Syntax

2.2.1 Types

The base types of EoA are exp (for expressor) and comm (for command). The type exp contains integer thunks—objects which when given a state evaluate to an integer. The type comm contains imperative commands—objects which when given a state evaluate to a new state (e.g. storing 5 in location x). The full set of types is defined inductively from the base types such that: if θ and τ are types then θ → τ is a type (corresponding to the type of functions from θ to τ).

EoA does not have integer as a base type. Consequently, we can not have integers as constants in our language. But we can have constants of type exp which behave like integer constants. In particular, if n is an integer, we could write \underline{n} to denote the constant thunk which in any state produces the integer n. There is a subtle, but fundamental, difference between constants in the language and constant thunks. In EoA we generally think of an abstract meaning associated with a piece of code. Usually this meaning is a function on states. Such state-dependent objects are termed thunks. A constant thunk is a thunk that always gives the same result regardless of the state. The notion of a “constant thunk” is unrelated to the notion of being a linguistic constant. For example, (plus 1 1) is a constant thunk, but is clearly not a syntactic constant in the language EoA. Similarly it is plausible to introduce into EoA linguistic constants which do depend on the state. We have simply chosen not to do so.

The most commonly used function type is exp → comm. Frequently we will use acc to abbreviate exp → comm. Some authors would also like to have available a type which would correspond to that of integer → comm. When this type is available, it, rather than exp → comm, is typically used for acc. The type var is also occasionally introduced as a base type to correspond to the type acc × exp. Now that we have a better understanding of the nature of local variables, these types are not as necessary. For example, we can simulate the term M:integer → comm by the term (δ M):exp → comm, where δ is:

δ ≡ λι▪ λκ▪ (New ι′, κ′ ← κ in (M κ′))

To see how this works, consider

C ≡ λκ▪(seq (l_{1}^{acc} (succ κ))
(l_{2}^{acc} (succ κ)))

in (C l_{1}^{exp}) and ((δ C) l_{1}^{exp}), assuming that l_{i}^{exp} and l_{i}^{acc} are identifiers properly bound to the reading and writing components of location i. Consider executing these two commands in a state where location 1 has the value 10 and location 2 has the value 100. The term (C l_{1}^{exp}) results in 11 in location 1 and 12 in location 2. The term ((δ C) l_{1}^{exp}) results in 11 in both locations 1 and 2.

The type var is also unnecessary. We can eliminate var by referring to a location via two distinct identifiers, one whose job is to represent the r-value part (the reading part) and the other whose job is to represent the l-value part (the updating part). Since we do not use var, we no longer need the explicit coercions cont:var → exp, and := which has type var → acc. Depending on one’s choice of semantics, the traditional assignment operator, :=, might be used as more than just an explicit coercion—it may also be used to pass an argument to an acceptor “by value.” The choice is between evaluating the argument in the current state and then passing the resulting constant thunk to the acceptor (by-value), or passing the unevaluated, potentially non-constant thunk to the acceptor (the way EoA does it). The by-value version can be expressed in EoA using the term δ defined above.

For example, consider a New block in a language with the type var, and where New blocks have an argument slot for the initial value of the new location. Specifically, we consider a block of code to allocate two variables (the first initialized to 0 and the second initialized to 1) with a body which assigns the value stored in the location pointed to by the second variable to value stored in the location pointed to by the first variable:

New fst ← 0 in (New snd ← 1 in (:= fst snd)).

The translation of the block into EoA where “:=” is only doing an explicit conversion looks like

New fstL, fstR ← 0 in (New sndL, sndR ← 1 in (fstL sndR))

When “:=” is both doing a coercion and forcing a call-by-value application the translation looks like

New fstL, fstR ← 0 in (New sndL, sndR ← 1 in (δ fstL sndR)).

2.2.2 Identifiers and Terms

We assume that we have an infinite set of identifiers of each type. We let α^{θ} be a metavariable ranging over identifiers of type θ (we’ll just write α when we need a metavariable ranging over identifiers, but the type is unimportant). We let ι be a metavariable ranging over identifiers of type acc ≡ exp → comm, and κ range over identifiers of type exp. The set of constants from which we build up EoA is shown in Figure 2.1. The set of EoA terms, denoted by L, is built up from these constants by the usual inductive definition—augmented with one extra case for new blocks:

• α^{θ} is term of type θ;

• c^{θ} ∈ Const is a term of type θ;

n  exp  skip comm
IFexp_{exp}  exp → exp → exp → exp  seq comm → comm → comm
IFexp_{comm} exp → comm → comm → comm Y_{θ} (θ → θ) → θ
succ  exp → exp  plus exp → exp → exp

Figure 2.1: Const, the set of constants of EoA and their types.

• (M N) is a term of type τ if M has type θ → τ and N has type θ;

• (λα^{θ}▪ M) is a term of type θ → τ if M has type τ;

• (New ι, κ ← E in P) is a term of type comm if E has type exp and P has type comm.

We abbreviate the phrase “M is a term of type θ” by writing M:θ.

We adopt the following conventions about associativity and the extent of binding operators which allow us to drop certain parenthesis without introducing ambiguity.

• All applications are parenthesized to the left so the expressions (M_{1} M_{2} M_{3}) or M_{1} M_{2} M_{3} can be written for ((M_{1} M_{2}) M_{3}).

• The body of a λ-expression or New declaration extends to the first unmatched right parenthesis.

• Although readability is usually enhanced by dropping unneeded parentheses, we feel free to leave in any parenthesis that will enhance readability.

For types, we assume that → associates to the right, so that we may also drop unnecessary parenthesis in type expressions. For example, we can write τ_{1} → τ_{2} → τ_{3} in place of (τ_{1} → (τ_{2} → τ_{3})). In addition, in informal discussion, we may write binary operators in infix notation (e.g. c_{1} ; c_{2} instead of (seqc_{1} c_{2}), and e_{1} + e_{2} instead of (plus e_{1} e_{2})).

The intended semantics of a term constructed with New is not obvious. Consider the term

New ι, κ ← E in P .

The intended semantics is to evaluate E in the current state to an integer n. Then, extend the state by a new location whose initial value is n. Finally, evaluate P in a manner in which the identifier ι is bound to the writing component of this new location, and the identifier κ is bound to the reading component of this new location. There are several important details to note about this construct. First, the order of the identifiers is important to remember—the writing component (the acceptor) comes first, and the reading component (the expressor) comes second. In addition, the choice of the names of these identifiers in no way affects the evaluation of E; however, the choice of the names of these identifiers has a major impact upon the evaluation of P. In other words, the New binds ι and κ the term P, but not in the term E.

2.2.3 Free and Bound Identifiers, Substitution, and Closed Terms

The standard λ-calculus concepts of free and bound identifiers, closed and open terms, and substitution make sense for EoA. When we say “free identifier” we are really talking about the standard λ-calculus notion of “free variable.” Unfortunately, in the setting of an Algol-like language, it is necessary to co-opt the meaning of “variable.” Instead of using “variable” in the “logical” sense we use it in the “programming sense”—variables are how we introduce side-effects and dependence on a state. To remain consistent with the usual definitions, we will write “FV(M)” and “BV(M)” to denote the free identifiers of M and bound identifiers of M respectively.

Since we have an extra term constructor (New) we need to modify the usual definitions to fit EoA. This requires some care, since, like λ-abstraction, New is a binding construct. We adapt most of the standard conventions and definitions of Barendregt [1] to EoA.

The set FV(M) of free identifiers of M is defined inductively on the structure of M as follows:

FV(c) = ∅, for all constants c. FV(α) = {α}, for all identifiers α. FV(MN) = F V (M) ⋃ FV(N). FV(λα▪M) = FV(M) − {α}. FV(New ι, κ ← E in P) = FV(E) ⋃ (FV(P) − {ι, κ}).

Note that either ι or κ (or both) can be free in New ι, κ ← E in P iff it appears free in E.

The set BV(M) of bound identifiers of M is defined inductively on the structure of M as follows:

BV(c) = ∅, for all constants c. BV(α) = ∅, for all identifiers α. BV(MN) = BV (M) ⋃ BV(N). BV(λα▪M) = BV(M) ⋃ {α}. BV(New ι, κ ← E in P) = BV(E) ⋃ BV(P) ⋃ {ι, κ}.

It is perfectly reasonable for an identifier to appear both free and bound in the same term (e.g. α in (x (λα▪ α) α)).

Definition 2 A term M is closed iff F V (M) = ∅.

Barendregt defines a change of bound identifiers in M as the replacement of a part (λα▪ N) of M by (λα′▪ N[α′/α]), where α′ does not occur (at all) in N. Since α′ is fresh we can syntactically replace all occurrences of α in N by α′ without the usual dangers. For EoA, we must also allow for the change of identifiers bound by New. In particular, a change of bound identifiers in M can be of the above form, or of the following form— the replacement of a part (New ι, κ ← E in C) of M by either:

• (New ι, κ′ ← E in C[κ′/κ]) where κ′ does not occur (at all) in C, or

• (New ι′, κ ← E in C[ι′/ι]) where ι′ does not occur (at all) in C.

We can now define α-congruence (≡_{α}) for EoA terms by saying: M ≡_{α} N, if N results from M by a series of changes of bound identifiers. We adopt the convention that terms that are α-congruent are identified. We also adopt the further identifier convention: If M_{1}, …, M_{n} occur in a certain mathematical context (e.g. definition, proof), then in these terms all bound identifiers are chosen to be different from the free identifiers.

Since the binding constructs in EoA are somewhat different from the pure simply-typed λ-calculus, it is worth providing the full definition of the substitution operator in order to avoid confusion. Specifically we write M[N/α] to represent the result of substituting N for all free occurrences of α in M. We define M[N/α] by induction on the structure of M as follows:

α[N/α] = N
α′[N/α] = α′ for α′ any identifier other than α
c[N/α] = c for c any constant
(P Q)[N/α] = (P [N/α])(Q[N/α])
(λα′▪ M)[N/α] = (λα′▪ M[N/α])

In the above clause it is not necessary to say “provided that α′ ≢ α and α′ ∉ FV(N),” as the identifier convention insures that this is the case. Finally we have the case for New which is again simplified by adopting the identifier convention.

(New ι, κ ← E in C)[N/α]
= (New ι, κ ← (E[N/α]) in C[N/α])

So long as N:θ then it is obvious from the definition of M[N/α^{θ}] that the result is a term which has the same type as M.

2.3 Assigning Operational Semantics

An ability to read from and write to the state is a fundamental aspect of imperative programming. What distinguishes EoA from other languages which combine imperative programming and the higher-order functionality of the simplytyped lambda calculus is its variable allocation mechanism. This allocation occurs via New blocks. Intuitively we think of the process of executing a New block as: upon entrance, extending the state by another “location”; then evaluating the body of the block in an “environment” where the “block identifiers” are appropriately bound to this new location; and finally, at the end of the block removing this “new” location from the state. This informal description points out three elements which are crucial to defining our operational semantics:

• We need a way of representing the state.

• We need a notion of “location,” a way of extending the state by a new location, and a way of removing a location from the state.

• We need a way to evaluate the body of a block where the block identifiers are properly tied to a new location.

Given that we will only be storing integers in the state, a very simple representation of states and locations arises naturally. Specifically, a state will simply be a finite sequence of integers. A location can be an index into such a sequence. To extend a state by a new location, we simply need to append the initial value for the new location onto the state. To remove the last location from the state, we simply strip the last value off the sequence.

In order to evaluate the body of a block we need a way to tie terms to states. There are two plausible approaches. On the one hand, we could introduce location constants into the language. This would enable us to determine the behavior of a New block by looking at the behavior of the body of the block when we instantiate the block identifiers by appropriate location constants (one constant for the acceptor and a different constant for the expressor). On the other hand, we could introduce the notion of binding—to variables. The purpose of a binding would be to tie the block identifiers properly to the new location. Thus, to determine the behavior of a New block under a binding B, we look at the behavior of the body of the block under a binding B′ (which is exactly like B except B′ ties the block identifiers properly to the new location). We choose the second approach.

We now make this precise with a few definitions. A state is a finite sequence of integers. The collection of all possible states, written S, is ℕ^{∗}. We will typically use the metavariable σ to range over states. The following five items are important for manipulating states:

• length: S → ℕ.

• proj(σ, k): the k-th component of σ.

• update(σ, k, n): returns a state just like σ except the k-th component is set to n.

• EmptyState: denotes the zero-length state.

• s_{1}▪s_{2} is used to denote the concatenation of two states, s_{1} and s_{2}. More formally,

⟨v_{1}, …, v_{k}⟩▪⟨v′_{1}, … v′_{k′}⟩ ≡ ⟨v_{1}, … v_{k}, v′_{1}, … v′_{k′}⟩.

Often we will write the integer v when we really mean the state ⟨v⟩; however, the intended interpretation should always be clear from the context.

A binding—to variables, henceforth called binding, is a finite function from identifiers of type exp or acc to ℕ. We call the collection of all bindings B. The purpose of a binding is to tie a term M to a state σ via its free identifiers of type exp and acc. Specifically, a binding explains how to use an identifier of type exp to read from a location in the state and it also explains how to use an identifier of type acc to write to a location in the state.

Definition 3 The index of a non-empty binding B (written index(B)) is the greatest integer i in the range of B. The index of the empty binding, EmptyBind, is 0.

Definition 4 An lterm is a pair [M, B] ∈ (L×B) (recall that L is the set of all (open and closed) EoA terms). We extend the notion of free identifiers to lterms in the following way: FV([M, B]) = FV(M)−Dom(B) (note: our identifier convention allows us to assume that bound identifiers of M are also not in Dom(B)). A closed lterm is an lterm [M, B] such that FV([M, B]) = ∅. An instantiation [L, B] of a closed lterm [M, B] is the result of a sequence substitutions of a term N_{1} : θ_{1}, …, N_{k}: θ_{k} for an sequence of identifiers α_{1}^{θ_{1}}, … α_{k}^{θ_{k}} ∉ Dom(B) to obtain the term L. A closed instantiation of a closed lterm [M, B] is an instantiation of [M, B] which is a closed lterm.

We will explain the behavior of EoA code by defining the behavior of closed lterms via a Structured Operational Semantics (SOS) in the style of [19]. Before we go into the definition we first note that EoA is somewhat unconventional. EoA combines two very different notions. On the one hand, it has the full type structure of the simply typed lambda calculus, the intended semantics for the functional fragment of EoA is the call-by-name lambda calculus, and the functional fragment can be handled by term rewriting. On the other hand, the evaluation of base type expressions involving imperative features requires a full fledged SOS involving configurations.

Consequently, our operational semantics is a hybrid of these two schemes. The configuration rewriting does not even apply for higher order terms—we directly restrict ourselves to the base types comm and exp for configuration rewriting. All evaluation of higher order terms is handled via the term rewriting rules (as we will see in Figure 2.3). The method of evaluation of base type terms depends on the principal operator of the term. If it is of the functional sort (a lambda abstraction) then term rewriting will be used to determine how the configuration behaves. If it is of an imperative sort (e.g. an assignment, or the evaluation of an expression) then the rules for the imperative features kick in.

We define a configuration to be a triple ⟨Q, B, σ⟩ ∈ (L × B × S) such that [Q, B] is a closed lterm of base type, and index(B) ≤ length(σ). We call the collection of all configurations C. Formally we define a binary relation, →_{L}, on C ∪L. The intended interpretation of ⟨Q, B, σ⟩→_{L}⟨Q′, B′, σ′⟩ is that in one step of the evaluation of Q (tied to state σ by binding B) results in Q′ (tied to state σ′ by binding B′). The intended interpretation of M→_{L}M′ is the usual one. We then make the further definition of ↠_{L} as the reflexive transitive closure of →_{L}. Figure 2.2 lists the metavariable conventions which we make in giving the operational semantics. We attempt to follow them throughout the rest of this thesis. The full set of rules defining →_{L} appear in Figures 2.3, 2.4 and 2.5.

θ  arbitrary types
β  base types (exp or comm)
M, N terms of arbitrary type
E  terms of type exp
P  terms of type comm
Q terms of base type (exp or comm)
α  (typed) identifiers of arbitrary type
α^{θ} identifiers of type θ
ι  identifiers of type acc
κ  identifiers of type exp

Figure 2.2: Metavariable conventions.

2.4 Properties of →_{L}

There are some quite simple, but quite important properties of →_{L} which we will use later. All but the last are verified by a simple induction on the structure of terms. In stating the properties, we assume that ⟨Q, B, σ⟩ is an arbitrary element of C.

1. →_{L} is deterministic, viz. it is the graph of a partial function on C ∪ L.

2. If ⟨Q, B, σ⟩→_{L}⟨Q′, B′, σ′⟩ then B = B′, length(σ) = length(σ′), and Q and Q′ have the same type.

(λα▪ M)N→_{L}M[N/α]  (beta)
\frac{M→_{L}M′}{(MN)→_{L}(M′N)}  (eval-operator)
Y_{θ}M→_{L}M(Y_{θ}M)  (rec-unwind)
\frac{Q→_{L}Q′}{⟨Q, B, σ⟩→_{L}⟨Q′, B, σ⟩}  (interaction)

Figure 2.3: Functional rules.

3. If Q is not of type comm, then if ⟨Q, B, σ⟩→_{L}⟨Q′, B′, σ′⟩ then σ = σ′ (i.e. only commands can have side effects).

4. Let α ∉ FV(Q) and i ≤ length(σ), then

⟨Q, B, σ⟩→_{L}⟨Q′, B, σ′⟩ iff ⟨Q, B[i/α], σ⟩→_{L}⟨Q′, B[i/α], σ′⟩

i.e. for α ∉ FV(Q), B(α) does not affect the behavior of the configuration ⟨Q, B, σ⟩.

5. If P is of type comm, then either

⟨P, B, σ⟩↠_{L}⟨skip, B, σ′⟩ for some σ′
or ⟨P, B, σ⟩→_{L}⟨P_{1}, B, σ_{1}⟩→_{L}⟨P_{2}, B, σ_{2}⟩→_{L} ⋯

In the first case we say “P (with binding B in state σ) converges.” In the second case we say “P (with binding B in state σ) diverges.”

The last property can be verified by defining an appropriate notion of normal form for closed lterms and noticing that the only normal forms of type comm have term part skip.

2.5 Observations

Now that we have defined our operational semantics and established some consistency properties of this semantics, we can introduce some notions of “behaviors” of programs. Of course, we first need to decide what a program is.

Definition 5 An EoA program is an EoA command whose free variables are of type exp or acc.

A binding provides the mechanism for linking a program to the state, possibly introducing sharing. We can view our operational semantics as specifying how

⟨succ n, B, σ⟩→_{L}⟨n + 1, B, σ⟩  (succ-do)

⟨E, B, σ⟩→_{L}⟨E′, B, σ⟩ ; ⟨succ E, B, σ⟩→_{L}⟨succ E′, B, σ⟩

(succ-eval-arg)

⟨(plus n_{1} n_{2}), B, σ⟩→_{L}⟨n_{1} + n_{2}, B, σ⟩  (plus-do)

⟨E_{1}, B, σ⟩→_{L}⟨E′_{1}, B, σ⟩ ; ⟨(plus E_{1} E_{2}), B, σ⟩→_{L}⟨(plus E′_{1} E_{2}), B, σ⟩

(plus-eval-arg1)

⟨E_{2}, B, σ⟩→_{L}⟨E′_{2}, B, σ⟩ ; ⟨(plus n E_{2}), B, σ⟩→_{L}⟨(plus n E′_{2}), B, σ⟩

(plus-eval-arg2)

⟨(IFexp_{β} 0 Q_{1} Q_{2}), B, σ⟩→_{L}⟨Q_{1}, B, σ⟩  (IFexp-true)
⟨(IFexp_{β} n + 1 Q_{1} Q_{2}), B, σ⟩→_{L}⟨Q_{2}, B, σ⟩  (IFexp-false)

⟨E, B, σ⟩→_{L}⟨E′, B, σ⟩ ; ⟨(IFexp_{β} E Q_{1} Q_{2}), B, σ⟩→_{L}⟨(IFexp_{β} E′ Q_{1} Q_{2}), B, σ⟩

(IFexp-eval-guard)

Figure 2.4: Plotkin Style SOS rules defining the operational semantics of EoA for ordinary non-imperative terms.

⟨(ι n), B, σ⟩→_{L}⟨skip, B, update(σ, B(ι), n)⟩  (variable-write)
⟨κ, B, σ⟩→_{L}⟨σ_{B(κ)}, B, σ⟩  (variable-read)
\begin{aligned}⟨E, B, σ⟩ & →_{L} & ⟨E′, B, σ⟩ \\ ⟨(ι E), B, σ⟩ & →_{L} & ⟨(ι E′), B, σ⟩ \end{aligned}  (assign-eval-arg)
⟨(seq skip P), B, σ⟩→_{L}⟨P, B, σ⟩  (seq-discharge)
\begin{aligned}⟨P_{1}, B, σ⟩ & →_{L} & ⟨P′_{1}, B, σ′⟩ \\ ⟨(seq P_{1} P_{2}), B, σ⟩ & →_{L} & ⟨(seq P′_{1} P_{2}), B, σ′⟩ \end{aligned}  (seq-eval-arg1)
⟨(New ι, κ ← n in skip), B, σ⟩→_{L}⟨skip, B, σ⟩  (New-discharge)

⟨E, B, σ⟩→_{L}⟨E′, B, σ⟩ ; ⟨(New ι, κ ← E in P), B, σ⟩→_{L}⟨(New ι, κ ← E′ in P), B, σ⟩

(New-init)

⟨P, B′, σ▪n⟩→_{L}⟨P′, B′, σ′▪n′⟩ ; ⟨(New ι, κ ← n in P), B, σ⟩→_{L}⟨(New ι, κ ← n′ in P′), B, σ′⟩

(New-eval)

where l = 1 + length(σ) and B′ = B[l/ι, l/κ].

Figure 2.5: The new rules which need to be introduced in order to capture imperative features. to associate with each closed lterm of type comm a partial function on states. Note that a closed lterm of type comm is merely a program P paired with a binding B such that F V (P) ⊆ Dom(B). Specifically, the partial function f_{[P,B]} associated with [P, B] is defined by:

f_{[P,B]}(σ) = \{ \begin{matrix}σ′ & if ⟨P, B, σ⟩↠_{L}⟨skip, B, σ′⟩, \\ undefined & if P with binding B diverges in state σ, \\ undefined & if length(σ) < index(B) \\ & (viz. the state is not “large enough” to fit with B). \end{matrix}

It is the closed lterm [P, B] which most closely coincides with the traditional notion of Algol-like program, with the binding B linking the program P to the state via the free exp and acc identifiers in P. There is a natural notion of equivalence between programs, ≈obs^{p}, which we formally define as follows

Definition 6 Let P_{1}, P_{2} be programs. Define P_{1} ≈obs^{p} P_{2} by the condition:

For all B such that [P_{1}, B] and [P_{2}, B] are both closed lterms, f_{[P_{1},B]} = f_{[P_{2},B]}.

It requires a little bit of proof (using the previously mentioned properties of →_{L}) to show that ≈obs^{p} is actually an equivalence relation. Unfortunately, the relation ≈obs^{p} is not a congruence on programs, as free acceptors can be instantiated by “bad” variables (they could have side-effects). For example while

(ι 1) ≈obs^{p} (ι 9) ; (ι 1),

it is not hard to see how to write a term M of type acc such that in some binding B, we have f_{[(M 1),B]} ≠ f_{[(M 9) ; (M 1),B]} and so

(M 1) ≉obs^{p} (M 9) ; (M 1).

Given such a term M, the context C[·] = (λι▪[·])M (a context is merely a term with a “hole”) will obviously distinguish (ι 1) from (ι 9) ; (ι 1).

Definition 7 Let ≡obs^{p} be the congruence on terms generated by ≈obs^{p}. Specifically, M ≡obs^{p} N iff for all contexts C[·] such that C[M] and C[N] are programs,

C[M] ≈obs^{p} C[N]

It again requires a little proof to show that ≡obs^{p} is in fact an equivalence relation, but requires no new ideas.

On the other hand one could make the argument that ≈obs^{p} does not match with Reynolds’s goal of eliminating locations from explicitly appearing in an Algol-like language. Essentially our notion of program amounts to observing open commands in a very special set of contexts. From a technical point of view, one might have expected a definition of completely closed command, viz. a command P such that FV(P) = ∅. Our observation would then simply be termination of a completely closed command. We now generate a definition of observational equivalence and observational congruence based on observing termination.

Definition 8 Let P_{1}, P_{2} be completely closed commands, define P_{1} ≈obs^{c} P_{2} by the condition:

⟨P_{1}, EmptyBind, EmptyState⟩↠_{L}⟨skip, EmptyBind, EmptyState⟩
iff ⟨P_{2}, EmptyBind, EmptyState⟩↠_{L}⟨skip, EmptyBind, EmptyState⟩.

The relation ≈obs^{c} is obviously an equivalence relation; it is also a congruence on completely closed commands. We can generalize ≈obs^{c} to a congruence on terms, by defining M ≡obs^{c} N by the condition that whenever C[M] and C[N] are completely closed commands, C[M] ≈obs^{c} C[N]. (It again requires a little proof to show that ≡obs^{c} is an equivalence relation.)

We have now defined two seemingly different notions of observational congruence, ≡obs^{p} and ≡obs^{c}. We would like to claim that restricting observations to completely closed commands, rather than observing programs directly, does not change the congruence generated. In other words ≡obs^{p} and ≡obs^{c} define the same relation on terms. We prove this as the following theorem, which then justifies the use of the notation ≡_{obs}.

Theorem 9 M ≡obs^{p} N iff M ≡obs^{c} N.

Proof: The “only if” (⇒) direction is obvious. The proof of the “if” (⇐) direction requires the following further uniformity property of →_{L} and the analogous version for acc, both of which are proven by a straightforward structural induction.

Lemma 10 Suppose B(α_{1}^{exp}) = B(α_{2}^{exp}). Let N ≡ M[α_{2}^{exp}/α_{1}^{exp}].

If ⟨M, B, σ⟩→_{L}⟨M′, B, σ′⟩ then ⟨N, B, σ⟩→_{L}⟨M′[α_{2}^{exp}/α_{1}^{exp}], B, σ′⟩.

Conversely, if ⟨N, B, σ⟩→_{L}⟨N′, B, σ′⟩ then there exists an M′ such that

N′ = M′[α_{2}^{exp}/α_{1}^{exp}] and ⟨M, B, σ⟩→_{L}⟨M′, B, σ′⟩.

We now show sketch the proof that M ≢obs^{p} N implies M ≢obs^{c} N. Let C[·] be a program context distinguishing M and N. Let B be a binding and σ a state demonstrating this distinction. Without loss of generality, suppose

⟨C[M], B, σ⟩↠_{L}⟨skip, B, σ′⟩ but ⟨C[N], B, σ⟩ ↠̸_{L}⟨skip, B, σ′⟩

From the context C[·] we will construct a completely closing command context C′[·] which will allocate length(σ) variables such that the ith allocation is initialized to the ith component of σ. The body will consist of an execution of C[·] in a manner such that the binding B is encoded by tying the free identifiers of C[·] to the variables allocated above. After properly executing [·], we check that the resulting state is σ′, if it is the term halts, if it is not the term diverges.

To construct this context C′[·], let

{α_{1}^{exp}, …, α_{k}^{exp}, α_{1}^{acc}, …, α_{l}^{acc}} = Dom(B),
n = length(σ),
ι_{1}, …, ι_{n} be fresh acceptors,
and  κ_{1}, …, κ_{n} be fresh expressors.

We take the context C′[·] to be:

New ι_{1}, κ_{1} ← proj(σ, 1) in New ι_{2}, κ_{2} ← proj(σ, 2)

in

⋮
New ι_{n}, κ_{n} ← proj(σ, n)

in (λα_{1}^{exp} … α_{k}^{exp}, α_{1}^{acc}, … α_{l}^{acc}▪C[·]) κ_{B(α_{1}^{exp})} ⋯ κ_{B(α_{k}^{exp})} ι_{B(α_{1}^{acc})} ⋯ ι_{B(α_{l}^{acc})} ;

(IFexp_{comm} (κ_{1} ≠ proj(σ′, 1)) diverge
(IFexp_{comm} (κ_{2} ≠ proj(σ′, 2)) diverge
⋮
(IFexp_{comm} (κ_{n} ≠ proj(σ′, n)) diverge skip) ⋯))

The completely closed command C′[M] will always converge, whereas the completely closed command C′[N] will always diverge, thus M ≢obs^{c} N.

Now that we have a satisfactory notion of observational congruence, we address what we mean when we say that a model is adequate for this notion of observational congruence. Jim and Meyer [6] provide a discussion of the basic principles behind the definitions of observations, observational congruence, adequacy and full abstraction. They also give some Lemmas which provide alternative characterizations of adequacy when a model possesses various special properties. The rest of this Section is adapted from that discussion.

A meaning function for EoA is a function [[·]] from terms M to values in some space (for the Tennent model these values will be natural transformations between functors from a category of possible worlds to the category of (possibly) bottomless cpos). A meaning function is compositional iff for all terms M, N and contexts C[·], if [[M]] = [[N]] then [[C[M]]] = [[C[N]]].

Definition 11 A meaning function is adequate for a definition of observational congruence, ≡_{obs}, if for all terms M,N

[[M]] = [[N]] implies M ≡_{obs} N.

Equality on adequate meanings may be strictly finer than observational congruence; in the ideal situation, known as full abstraction, the two relations coincide:

Definition 12 Let [[·]] be a meaning function for EoA. It is fully abstract if for all M and N,

[[M]] = [[N]] iff M ≡_{obs} N

The main result of this thesis (proven in Chapter 4) is to show that the model of Tennent presented in Section 3.4 is adequate for EoA.

Defining the Denotational Model

O’Hearn and Tennent [12] provide a good exposition of the methods of “possible worlds” models of block structure. This idea of using a category-theoretic form of possible worlds to model block structure was pioneered in the early 1980’s by Reynolds and Oles [15, 17, 20]. The model of Reynolds and Oles provided great insight into the nature of local variable declarations. Later Tennent and O’Hearn [12–14, 23, 25] modified the Oles model in an effort to incorporate the notion of non-interference. Tennent incorporated this model of EoA which understood non-interference into a larger model of Reynolds’s Specification Logic [22] for the Essence of Algol. Our focus right now is Tennent’s original model of EoA which captures non-interference. In Chapter 5 we discuss some examples of equivalences of EoA code which O’Hearn and Tennent have shown [12, 13] that this model validates. These examples demonstrate the substantial power of the model; however, we also also show some counterexamples to full abstraction [12, 13].

We begin this Chapter by giving a review of the basic concepts of these possible worlds models of Algol and the definition of the Tennent model; a more comprehensive discussion is found in [12], Chapter 9 of [24] and in [14]. Section 3.5 contains a collection of definitions which we will need for our proof of adequacy in Chapter 4. We focus our discussion on the model of Tennent [24, 25]. This model incorporates several substantial modifications to Oles’s original model. The Tennent model provides some simplifications in description and some improvements in power. In particular Tennent separated the issue of implicit coercions from the issue of block structure, which had been intertwined in the model of Oles. Tennent also found a few other technical simplifications of the category of state shapes which were used for modeling block structure. In addition, to properly model interference (which helps in understanding how higher order objects behave) Tennent slightly modified the category of state shapes, and chose an “ad hoc” definition for [[comm]], rather than taking the functor S ⇀ S.

Later, we will also be interested in the O’Hearn-Tennent model [13]. This model arose from an attempt to model a principle of “non-interference abstraction.” Technically it is obtained by slightly perturbing the category of state shapes used in [24, 25], and modifying the definition of [[comm]]. Most of the definitions and results of this paper make sense and hold for both the Tennent and O’Hearn-Tennent models; we will specifically point out when a definition or result is specific to one or the other. When we abstract away the specifica of Tennent’s model and state our general adequacy Theorem it will be obvious that the O’Hearn-Tennent model is also adequate. It should be a routine exercise to varify that the the model of Reynolds and Oles (for a language without implicit coercions) also satisfies the sufficient conditions for adequacy.

3.1 Functor Category Models of Simply Typed Lambda Calculi

Given two categories A and B, we define the functor category from A to B (B^{A}) to be the category whose objects are all covariant functors from A to B and whose morphisms are all natural transformations between covariant functors from A to B. Composition in B^{A} is the standard composition of natural transformations, and the identity morphism is simply the identity natural transformation. Note that some authors write A → B for B^{A}.

Let D be to the category of possibly-bottomless cpo’s; a careful definition of D is given in Section 3.2. We will take advantage of the fact that for any small category X, the functor category D^{X} is cartesian closed. In [11] Nelson proves this for any complete cartesian closed category in the place of D. The case of D was explicitly treated by Oles [15]. D^{X} is also closed under denumerable products, a fact that makes life simpler, as there will be a single environment object, Env (rather than merely an environment object for each finite set of typed identifiers). Our ability to take advantage of denumerables products in this way is a consequence of identifiers coming explicitly with types. If the category were not closed by denumerable products we would have to count identifiers and introduce finite environments relative to a finite set of identifiers. Berry, Curien and Lévy provide a quick summary of the general methods of c.c.c. models of simply-typed lambda calculi and what they look like when we take advantage of the single environment object [3, Section 6]. Going along the general lines of interpreting a simply typed λ-calculus in a c.c.c., we interpret types by objects of the functor category via a function [[·]]_{type} (remember, these objects are functors from X to D). We can generate the function [[·]]_{type} merely by specifying [[β]]_{type} for all of our base types β (for EoA, this is simply for β ∈ {comm, exp}).

In contrast to an interpretation of the simply typed lambda calculus in a category of sets with structure, there is a lot more to the meaning of a type than a (structured) set of elements of that type. In this case a type is a functor from a category to a (potentially bottomless) cpo. It no longer makes sense to think of an element of the type T, per se. We can however, make sense of the notion of a global element (constant) of type T. It is a morphism, m, from the terminal object (1_{D^{X}}) of D^{X} to [[T]]_{type}. So m is a natural transformation from 1_{D^{X}} to [[T]]_{type}. By definition, this is a function that assigns to every X-object w, a morphism in D, m_{w} : 1_{D^{X}}(w) → T (w), which satisfies certain uniformity properties. As we will see, 1_{D^{X}}(w) will simply turn out to be the one-element cpo {∗}, so we can in fact just think of m as a method of selecting a single element from each cpo T (w). But the D-morphisms which m picks for each X-object w cannot be unrelated. In fact, we must have for any f : w⟶^{X}w′, that

m(w′) = T (f); m(w),

where “;” denotes composition in “diagrammatic” order. Since each type is a functor into D (which is a category of sets with structure), it does make sense to talk about an element of a type T at a world w.

Half of the meaning of a type T is its behavior on objects, w ∈ obj(X), essentially telling us the collection of meanings appropriate to type T at world w. As mentioned above, the meanings for different worlds are not completely unrelated. The other half of the meaning of a type tells us this relation. Specifically, given f : w⟶^{X}w′, the function T (f) tells us how to transform meanings appropriate to world w into meanings appropriate to world w′. Since there may be many morphisms from w to w′, there might in fact be many different ways to transform the space of meanings appropriate to world w into the space of meanings appropriate to world w′. As we will see in Section 3.5.2 this provides us with greater flexibility than we had with the “global elements of type T.”

We also have an indexed product object

Env = ∏_{α^{θ}∈Identifiers}[[θ]]_{type},

useful for providing meanings for the free identifiers of a term M. Since Env is a functor, it is incorrect to think of it as a set of environments. Nevertheless, it does make sense to think of an element of Env at a world w, viz. an environment at world w. As with types, the behavior of Env on morphisms, Env(f : w⟶^{X}w′) : Env(w)⟶^{D}Env(w′), tells how to transform (along f) an environment at w into an environment at w′.

We now look to the general method of c.c.c. interpretations to see what we should do with terms. We interpret a term M : θ as a morphism in D^{X} from Env to the object [[θ]]_{type}. In our framework, this will be a natural transformation from the functor Env to the functor [[θ]]_{type}, which will give us a nice commutative diagram which, for any X-morphism f : w → w′, looks like:

w  Env(w) ⟶^{[[M]]w} [[θ]]_{type}w
f↓  ^{Envf}↓  ↓^{[[θ]]_{type}f}
w′  Env(w′) ⟶^{[[M]]w′} [[θ]]_{type}w′

3.2 The Category D

We now review the basic structure of D, the category whose objects are directedcomplete, partially ordered, possibly bottomless sets (dcpos), and whose morphisms are continuous functions. Composition of morphisms is simply functional composition and the identity morphism on a dcpo A is simply the identity function on A.

The terminal objects of D are precisely the dcpos with exactly one element. We fix our attention on {∗} which we refer to as 1_{D}. The product of two dcpos ⟨A, ⊑_{A} ⟩ and ⟨B, ⊑_{B} ⟩ is the cartesian product of A and B ordered componentwise, i.e. ⟨A×B, ⊑_{A×B} ⟩, where A×B = {(a, b) | a ∈ A and b ∈ B} and (a, b) ⊑_{A×B} (a′, b′) iff a ⊑_{A} a′ and b ⊑_{B} b′. The exponent ⟨A, ⊑_{A} ⟩ → ⟨B, ⊑_{B} ⟩ is defined to be ⟨A →_{c} B, ⊑_{A→_{c}B} ⟩, where A →_{c} B is the set of continuous (wrt. ⊑_{A} and ⊑_{B}) functions from A to B, and ⊑_{A→_{c}B} is the standard “pointwise ordering”—namely f ⊑_{A→_{c}B} g iff for all a ∈ A, f(a) ⊑_{B} g(a). From now on we write → for →_{c}, A for the dcpo ⟨A, ⊑_{A} ⟩, and when obvious from the context, we drop the A from ⊑_{A}.

Two other constructions in D that we will later be using are:

• Lifting: A_{⊥} is an copy of A augmented by a new least element ⊥

• Partial exponentiation: A ⇀ B is the set of all continuous partial functions from A to B, ordered pointwise. Note that in D, A ⇀ B is isomorphic to A → B_{⊥}.

3.3 Constructing the C.C.C.

We now define the analogous constructions in the category D^{X}. These definitions are taken almost directly from [24, Chapter 9], although throughout the presentations we are careful to maintain the distinction between → (a morphism in some category) and ⇒ (the internal hom-functor of some category). In this Section we decorate → with the category in which it lies, e.g. f : x⟶^{X}y is a morphism in the category X from x to y. We also decorate ⇒ with the category in which it lies, e.g. A⇒_{D}B is the object of D which is the cpo of continuous functions from A to B. After this Section, we will typically drop the decorations on → and ⇒, and may in fact even use → for ⇒ when it can easily be disambiguated from the context. When working in D, we will also leave implicit the isomorphism between f : d_{1}⟶^{D}d_{2} as a continuous function from d_{1} to d_{2}, and f ∈ (d_{1}⇒_{D}d_{2}) an element of the cpo which is the exponential object.

Much of the structure of these constructions in D^{X} is inherited from that of D. Take F, G ∈ obj(D^{X}), namely functors from X to D; x, y, z ∈ obj(X), namely arbitrary possible worlds; and let f : x⟶^{X}y, g : y⟶^{X}z be arbitrary Xmorphisms from x to y and y to z, respectively. The constructions are then as follows:

• Terminal object, 1_{D^{X}} (remember 1_{D} ≡ {∗}): The behavior on worlds is 1_{D^{X}}(x) = 1_{D} ≡ {∗} and the behavior on morphisms is 1_{D^{X}}(f) = id_{1_{D}} ≡ id_{{∗}}.

• The product object, F ×_{D^{X}}G: On objects (F ×_{D^{X}}G)(x) = F (x)×_{D}G(x), ordered componentwise. On morphisms, we have

(F ×_{D^{X}}G)(f)[⟨d, d′⟩ ∈ F (x)×_{D}G(x)] = ⟨F (f)d, G(f)d′⟩.

• The exponential object, F ⇒_{D^{X}}G:

(F ⇒_{D^{X}}G)(x)

= \{m ∈ ∏_{f:x⟶^{X}y}[F (y)⇒_{D}G(y)] | \begin{matrix}for all f : x⟶^{X}y and g : y⟶^{X}z, \\ m(f); G(g) = F (g); m(f; g) \end{matrix} \}

ordered pointwise (i.e. m_{1} ⊑ m_{2} iff m_{1}(f) ⊑ m_{2}(f) for every f : x → y), where

∏_{f:x⟶^{X}y} ⋯ y ⋯

here and in later definitions is an abuse of notation which stands for

∏_{f∈X(x,·)} ⋯ codom f ⋯,

where X(x, ·) is the set of all X-morphisms with domain x. The behavior of this construction on X-morphisms, f : x⟶^{X}y, is defined to be:

(F ⇒_{D^{X}}G)(f : x⟶^{X}y)(m ∈ [F ⇒_{D^{X}}G]x)(g : y⟶^{X}z) = m(f; g)

Tennent provides the following motivation for the exponential construction:

To motivate the ⇒ construction, consider that a procedure defined in possible world x might be called in any possible world y accessible from x using any X-morphism f : x⟶^{X}y, and it is the domain structure determined by y which should be in effect when the procedure body is executed. This suggests that we cannot just define (F ⇒_{D^{X}}G)(x) to be F (x)⇒_{D}G(x); the meaning of a procedure defined in possible world x must be a family of functions, indexed by X-morphisms f : x⟶^{X}y. But such families of functions must be appropriately uniform; … [24].

The uniformity condition is the commutativity of all diagrams (in D) of the form

\begin{matrix}F (y) & ⟶^{m(f:x→^{X}y)} & G(y) \\ _{F (g:y→^{X}z)}↓ & & ↓_{G(g:y→^{X}z)} \\ F (z) & ⟶^{m((f;g):x→^{X}z)} & G(z) \end{matrix} (3.1)

There are several other useful constructions, which are not directly a part of the c.c.c. structure of D^{X}. For example, we have the lifted object, F_{⊥_{D^{X}}} :

F_{⊥_{D^{X}}} (x) = [F (x)]_{⊥_{D}}
F_{⊥_{D^{X}}} (f)[d ∈ F_{⊥_{D}}(x)] = \{ \begin{matrix}⊥, & if d = ⊥, \\ F (f)(d) in F_{⊥_{D}}(y) & otherwise. \end{matrix}

We also have a construction for partial exponentiation, which will be similar to the construction for (total) exponentiation; however, the uniformity condition on elements of the resulting cpo will not be as stringent. Specifically, we have

(F⇀_{D^{X}} G)(x)

= \{m ∈ ∏_{f:x⟶^{X}y}[F (y) ⇀_{D} G(y)] | \begin{matrix}for all f : x⟶^{X}y and g : y⟶^{X}z, \\ m(f); G(g) ⊆ F (g); m(f; g) \end{matrix} \}

ordered pointwise (i.e. m_{1} ⊑ m_{2} iff m_{1}(f) ⊑ m_{2}(f) for every f : x → y). Notice the two differences in the definition of ⇀_{D^{X}} from the definition of ⇒_{D^{X}}: we do comprehension over the underlying set of partial continuous functions from F (x) to G(x), and we have changed the “=” to a “⊆” in giving the constraint m(f); G(g) ⊆ F (g); m(f; g). The effect of this second change is to weaken the uniformity condition suggested in Diagram 3.1 to only require commutativity when the result of the partial mapping along the top of the Diagram is defined, giving Diagram 3.2.

\begin{matrix}F (y) & ⟶^{m(f:x→^{X}y)} & G(y) \\ F (g : y →^{X} z)↓ & ⊆ & ↓G(g : y →^{X} z) \\ F (z) & ⟶^{m((f;g):x→^{X}z)} & G(z) \end{matrix} (3.2)

Note that, even though in D, A⇒B_{⊥} is isomorphic to A ⇀ B, this is not generally the case in D^{X}.

Similarly, we can introduce indexed products. Specifically, if I is a denumerable set and for every i ∈ I, F [i] is a functor from X to D, then we can define the object, ∏_{i∈I}^{D^{X}} D_{i}, by

(\begin{matrix}∏ & D^{X} \\ i∈I \end{matrix}F [i]) (x ∈ obj(X)) = \begin{matrix}∏ & D \\ i∈I \end{matrix}(F [i]w)

(\begin{matrix}∏ & D^{X} \\ i∈I \end{matrix}F [i]) (f : x⟶^{X}x′) = \begin{matrix}∏ & D \\ i∈I \end{matrix}(F [i]f)

3.4 A Model of EoA

3.4.1 The Category of Possible Worlds, W

The intuition behind the category of Possible Worlds is to provide the “shape of the state” (i.e. the set of allowable states) during program execution, and to show how one state shape evolves into another. The category of possible worlds has state shapes as objects and “store evolutions” as morphisms. There are two principle kinds of operations performed on state shapes in Tennent’s work (although many others are allowed). The first is an “expansion” to correspond to allocating a new variable. The other is a “restriction” operation by which we restrict the set of allowable states to include only those states which satisfy a certain property.

For our model of EoA we will use as the category of possible worlds, W, a category of state shapes. Specifically, an object of W is any subset of ℕ^{n} for any integer n. The set of objects of W is closed under subset, intersection and product (if we interpret product as concatenation of sequences). A morphism from the world X to the world Y is a pair (f, Q), where

1. f is a function from the set Y to the set X.

2. Q is an equivalence relation on the set Y.

3. f restricted to any Q-equivalence class is injective; i.e., for all y, y′ ∈ Y if yQy′ and f(y) = f(y′) then y = y′.

When (f, Q) is describing a pure “restriction” operation, Y will be a subset of X. Furthermore, Q will turn out to be T_{Y} (the everywhere-true binary relation on Y), and f will simply be the injection of Y into X. When (f, Q) describes a new variable allocation, Y will be X × ℕ, Q will be defined so that

(x_{0}▪n_{0})Q(x_{1}▪n_{1}) iff n_{0} = n_{1},

and f(x▪n) = x. Intuitively, f extracts the old portion of the stack which is embedded in the new one, and Q relates new stacks which have the same “new components” (but possibly differ on the old part).

We define composition (in diagrammatic order) of W-morphisms, (f, Q) : X → Y, and (g, R) : Y → Z as follows: (f, Q); (g, R) = (h, P) where:

• h(z) = f(g(z)),

• z_{0}P z_{1} iff z_{0}Rz_{1} and g(z_{0})Qg(z_{1}).

Thus the identity morphism of W at world X, id_{X} : X → X, will be (I_{X}, T_{X}), where I_{X} is the identity function on X, and T_{X} is the everywhere-true binary relation on X.

We introduce the following useful notation for abbreviating some common restriction morphisms. Specifically, if X′ is a subset of a world X, we have the state-set restriction morphism, ⌈X′ : X → X′, defined to be (f, T_{X′}), where f is the inclusion function from X′ to X and T_{X′} is the everywhere-true relation on X′ (The notation ⌈X′ does not completely specify a morphism of W, as it also depends on the object X. Thus we will make sure that the X in question will always be clear from context). Similarly we introduce a useful notation for abbreviating some common expansion morphisms. Specifically, we define morphisms ×ℕ : X → X × ℕ, for which the function part is the projection from X × ℕ to X, and the equivalence relation part relates x_{0}▪n_{0} and x_{1}▪n_{1} iff n_{0} = n_{1}. As with our notation for ⌈X′, although the notation ×ℕ does not identify a morphism uniquely (as we need to know which object X is), the intended morphism will always be evident from the context. In future discussions, we will let the metavariables X, Y, Z, … range over objects of W, and we will let x_{0}, x_{1}, … range over X, etc.

3.4.2 Interpreting Types

The base types of EoA are exp and comm. An integer thunk (exp) is essentially a function which given a store, returns an integer—or is undefined. A command is essentially a function which given a store returns another store—or is undefined. Notice that in describing both of our base types, we have functions of stores arising. In fact, in our semantics it is only in the definition of the base types that functions on stores arise directly. Given our intuitive description of exp and comm it seems that we should first describe a meaning for stores and for integers, and then we are looking for something like: [[exp]] = S⇒ℕ, [[comm]] = S⇒S, and for higher types: [[θ → τ]] = [[θ]]⇒[[τ]].

So what are the functors S and ℕ? S is the contravariant functor which, given a store shape X, gives a discretely-ordered dcpo with X as its underlying set. In order to avoid getting bogged down in notation, we will often simply write X to denote S(X). To define S on morphisms, we take S(f, Q : X⟶^{W}Y) = f : S(Y)⟶^{D}S(X), the projection from Y to X along f. The functor ℕ is the constant functor which in any world returns the set of non-negative integers, considered as a discrete dcpo. ℕ applied to any morphism simply returns the identity on the natural numbers.

Note that since S is a contravariant functor, it is not an object of D^{W}. O’Hearn and Tennent [12, Section 4] give a good explanation of why we need S to be a contravariant functor. We adapt the conclusion of their discussion to our setting. There is a variant of the exponential construction used in D^{W} which works on contravariant functors to yield a covariant functor (which is an object in D^{W}). The definition of the contra-exponentiation for S ⇒ ℕ_{⊥} is defined just like the usual exponential, but with a reversal of vertical arrows in uniformity diagrams to account for contravariance. That is, e(·) ∈ (S ⇒ ℕ_{⊥})X is a family of functions, indexed by morphisms out of X, such that

Y ⟶^{e(f)} ℕ_{⊥}
S(g)↑  ↑^{id}_{ℕ_{⊥}}
Z ⟶^{e(f;g)} ℕ_{⊥}

commutes, where f : X → Y, g : Y → Z. The morphism part manages to be defined as before, namely (S ⇒ ℕ_{⊥})fmg = m(f; g), thereby yielding a covariant functor.

We could try doing the analogous flipping of the arrows of Diagram 3.2 for defining [[comm]] = S ⇀ S, giving the following:

\begin{matrix}Y & ⟶^{m(f:x→^{X}y)} & Y \\ S(g : y →^{X} z)↑ & ⊇ & ↑S(g : y →^{X} z) \\ Z & ⟶^{m((f;g):x→^{X}z)} & Z \end{matrix} (3.3)

Unfortunately, as discussed in [13], this does not impose enough uniformity constraints on the behavior of command meanings. On the other hand, using S⇒S_{⊥} imposes uniformity constraints that are too strong. They find a good compromise by making [[comm]] a subfunctor of S ⇀ S as follows:

[[comm]](X) = {c ∈ (S ⇀ S)(X) | for all (f, Q) : X⟶^{W}Y, and (g, R) : Y ⟶^{W}Z, and z ∈ Z,

S(⌈Z′); c((f, Q); (g, R)) = c((f, Q); (g, R); ⌈Z′); S(⌈Z′),

where Z′ = {z′ | zRz′}}.

The extra condition above enforces an additional commutativity requirement arising from the equivalence-class component of the morphisms. Specifically, for any (f, Q) : X → Y, and y ∈ Y, let

Y′ = {y′ ∈ S(Y) | yQy′}

(the set of states Q-equivalent to y); then

Y  ⟶^{c(f,Q)} Y
S(⌈Y′)↑  ↑^{S(⌈Y′)}
Y′ ⟶^{c((f,Q);⌈Y′)} Y′

must commute (and not just semi-commute). This insures that, when it is defined, c(f, Q) preserves the Q-equivalence class of its argument.

For the behavior of [[comm]] on morphisms, we still have:

[[comm]](f)(c)(g) = c(f; g)

There is one other important special case of the commutativity property for elements of [[comm]]X, which is a consequence of the “semi-commutativity” of (S ⇀ S)X. This special case is expressed by the following Lemma.

Lemma 13 Let c ∈ ([[comm]])(X) or, more generally, c ∈ (S ⇀ S)X. Let (f, Q) : X → Y. Finally, let (g, R) : Y → Z be an isomorphism in the category of possible worlds (then g is a bijection from Z to Y, and R is T_{Z}—the everywhere-true binary relation on Z). The following diagram commutes:

Y ⟶^{c(f,Q)} Y
S(g,R)=g↑  ↑^{S(g,R)=g}
Z ⟶^{c(f,Q;g,R)} Z

In other words, c(f, Q)(g(z)) = g(c(f, Q; g, R)z).

Since g is a bijection, the constraint expressed by the commutative diagram can also be expressed as c((f, Q); (g, R))z = g^{−1}(c(f, Q)(g(z))).

3.4.3 Interpreting Constants and Terms

In Chapter 2, we defined the syntax of EoA by giving some constants and three primary ways of constructing new terms from old: λ-abstraction, application, and new-variable declaration. To define our semantics we will need to provide the meaning of the constants, and we will also need to provide a way of finding the meaning of terms constructed using λ-abstraction, application and newvariable declarations. The general methods of providing these interpretations using c.c.c.’s is very well established, except for the case of new-variable declarations. For concreteness, we show specifically what all of these look like for our model of EoA.

The meaning of a term of type θ is a morphism from Env to [[θ]]. For

the meanings of constants we directly give [[n]] : Env⟶^{D^{W}}[[exp]] and [[skip]] :

Env⟶^{D^{W}}[[comm]]. Assuming X and Y are arbitrary worlds, u ∈ Env(X), f : X⟶^{W}Y and y ∈ Y, the definitions are

[[n]]Xufy = n
[[skip]]Xufy = y.

We uncurry all of the other constants in order to simplify the presentation. For a constant c of type θ_{1} → ⋯ → θ_{n} → τ, we indirectly give its meaning (which is a morphism from Env to θ_{1} → ⋯ → θ_{n} → τ) by providing a morphism from θ_{1}× ⋯ ×θ_{n} to τ. These interpretations are shown in Figure 3.1, where X and Y are arbitrary worlds, f : X⟶^{W}Y is arbitrary, and y is an arbitrary element of Y.

To obtain

[[c^{θ_{1}→···→θ_{n}→τ}]] : Env → [[θ_{1} → ⋯ → θ_{n} → τ]]

from

[[c^{θ_{1}→···→θ_{n}→τ}]]_{uncurry} : ([[θ_{1}]] × [[θ_{n}]]) → [[τ]]

we take advantage of the curry isomorphism, between the hom sets hom([[θ_{1}]] × ⋯ × [[θ_{n}]], [[τ]]) and hom(1, [[θ_{1}]] ⇒ ⋯ [[θ_{n}]] ⇒ [[τ]]). So, we will end up with

[[c^{θ}]] =!Env; (curry([[c^{θ}]]_{uncurry})).

For concreteness, we show how to obtain [[plus]] from [[plus]]_{uncurry}.

[[plus]](X)(u)(f)(e_{1})(g)(e_{2}) = [[plus]]_{uncurry}Z⟨[[exp]](f; g)e_{1}, [[exp(g)e_{2}]]⟩,

and so

[[plus]](X)(u)(f)(e_{1})(g)(e_{2})(h)(w)
= [[plus]]_{uncurry}Z⟨[[exp]](f; g)e_{1}, [[exp(g)e_{2}]]⟩hw
= \{ \begin{matrix}n + m & if e_{1}(f; g; h)w = n and e_{2}(g; h)w = m, \\ ⊥ & if e_{1}(f; g; h)w = ⊥ or e_{2}(g; h)w = ⊥, \end{matrix}

[[IFexp_{exp}]]_{uncurry}X⟨e_{0}, e_{1}, e_{2}⟩fy = \{ \begin{matrix}e_{1}fy, & if e_{0}fy = 0, \\ e_{2}fy, & if e_{0}fy = n + 1, \\ ⊥, & otherwise. \end{matrix}

[[IFexp_{comm}]]_{uncurry}X⟨e, c_{1}, c_{2}⟩fy = \{ \begin{matrix}c_{1}fy, & if efy = 0, \\ c_{2}fy, & if efy = n + 1, \\ undefined, & otherwise. \end{matrix}

[[succ]]_{uncurry}Xefy = \{ \begin{matrix}n + 1, & if efy = n, \\ ⊥ & if efy = ⊥. \end{matrix}
[[plus]]_{uncurry}X⟨e_{1}, e_{2}⟩fy = \{ \begin{matrix}n + m, & if e_{1}fy = n and e_{2}fy = m, \\ ⊥ & if e_{1}fy = ⊥ or e_{2}fy = ⊥. \end{matrix}
[[seq]]_{uncurry}X⟨c_{1}, c_{2}⟩fy = \{ \begin{matrix}c_{2}fy′, & if c_{1}fy = y′, \\ undefined, & if c_{1}fy is undefined. \end{matrix}
[[Y_{θ}]]_{uncurry}Xm = the least fixed point of m(id_{X}).

Figure 3.1: Meanings of EoA constants

In the case of Y_{θ} it is not obvious that the specified least fixed points always exist, as the objects of D^{W} are arbitrary functors into D. Since many objects of D are bottomless, it is definitely not the case for every element m of an arbitrary functor F at an arbitrary world X that m(id_{X}) has a least fixed point. Moreover, it is not necessarily the case for arbitrary worlds X and Y that the fixed points if they were to exist would fit together well enough for [[Y_{F}]] to be a natural transformation (a morphism in D^{W}). In [14, pages 26-28], it is argued that for all of the types we use (and some more), all of the necessary least fixed points do exist, and they do fit together naturally.

Application and abstraction are understood using the standard c.c.c. structure of D^{W}. When M : θ → τ and N : θ, [[(M N)]] is a natural transformation from Env to [[τ]]. Specifically, for an arbitrary world X and u ∈ Env(X), then

[[(M N)]]Xu = [[M]]xu id_{x}([[N]]Xu).

We can see how this comes from the c.c.c. structure of D^{W} by observing that

the definition of eval_{A,B} : [A⇒B]×A⟶^{D^{W}}B, is:

eval_{A,B} X⟨f, a⟩ = f id_{X} a.

The meaning of the term (λα^{θ}▪ M):θ → τ is a natural transformation from Env to [[θ → τ]]. Taking X and u as before, f : X → Y and v ∈ [[θ]]Y, we have:

[[(λα^{θ}▪ M)]]Xufv = [[M]]Y ((Env(f)u)[v/α^{θ}]).

We do a little bit of preliminary work before giving the valuation for New blocks. First, we define the new acceptor and expressor which are allocated in world X. Formally we define the functions:

a_{new} : obj(W) → ⋃_{X∈obj(W)}[[acc]](X × ℕ)
e_{new} : obj(W) → ⋃_{X∈obj(W)}[[exp]](X × ℕ)

Given arbitrary worlds X, Y, Z, and arbitrary morphisms (f, Q) : X → Y, (g, R) : Y → Z, and given states y ∈ Y, z ∈ Z, we let

a_{new}(X)(f, Q)(e)(g, R)z = z′
e_{new}(X)(f, Q)y = v where g(y) = x▪v.

In the definition of a_{new}, z′ is the unique element of Z such that

1. f(g(z′)) = x▪(e(g, R)z), provided x▪n = f(g(z)). If e(g, R)z = ⊥ then a_{new} is undefined.

2. zRz′ and g(z)Qg(z′).

There need not be a state z′ satisfying the above two conditions, in which case the result is undefined; however, if such a state does exist, it must be unique by the injectivity property of (f, Q); (g, R).

We further abuse the notation “×ℕ” and define it as a function from Wmorphisms to W-morphisms. Recall that we also use the notation ×ℕ as a function from W-objects to W-objects. We also have morphisms ×ℕ : X → X × ℕ for which the function part is the projection from X × ℕ to X, and the equivalence relation part relates x_{0}▪n_{0} and x_{1}▪n_{1} iff n_{0} = n_{1}. These three aspects fit together quite closely; in fact, if we just viewed ×ℕ via its behavior on W-objects and W-morphisms, then ×ℕ would be a functor from W to W. Given (f, Q) : X → Y, we define (f, Q) × ℕ = (f′, Q′), where f′(x▪n) = x, and ⟨x_{0}▪n_{0}⟩Q′⟨x_{1}▪n_{1}⟩ iff x_{0}Qx_{1}. A valuable property of how they fit together is that for any W-morphism (f, Q) : X → Y, the following diagram commutes:

X ⟶^{×ℕ} X × ℕ
(f,Q)↓  ↓^{(f,Q)×ℕ}
Y ⟶^{×ℕ} Y × ℕ

The valuation for New blocks is then:

[[New ι, κ ← E in P]]Xufy = S(×ℕ)([[P]](X × ℕ)u′(f × ℕ)(y▪([[E]]Xufy)))

where u′ = (Env(×ℕ)u)[a_{new}(X)/ι, e_{new}(X)/κ].

This definition is essentially the same as that of [25], except there is a little bit of extra work here. The extra work arises from two particular aspects of EoA which are different from Reynolds’s essence of Algol: the initial value for the location given by E and taking acc as a type synonym for exp → comm rather than taking it in such a way as to have [[acc]] = ℕ → [[comm]].

3.5 Definitions Needed for Adequacy

Given our style of operational semantics for EoA, we will also need to assign meanings to configurations. This will require several more steps. The state in the configuration provides us with two important pieces of semantic information. First, the possible world in which to interpret the term part of the configuration will depend on the length of the state. Second, the state component of the configuration gives us the semantic state to which we apply the meaning of the term part of the configuration. We then show how to turn a binding into its semantic analogue—an environment. In the last Section, we show how to combine these extra semantic pieces of information with the meaning of the term in order to figure out the denotation of the configuration.

3.5.1 A Sequence of Worlds

We first define a sequence of possible worlds X_{i} such that X_{i} is the smallest world useful for finding the meanings of all closed lterms [M, B] : comm where index(B) ≤ i. We let X_{n} = ℕ^{n} = {states of length n}. Alternatively, if we had viewed X_{i} as the smallest world appropriate for finding the meanings of all configurations whose state part has exactly length i, we would have reached the same definition.

We will let e_{k}^{i} denote the expressor for world X_{i} which reads from the k-th location. So

e_{k}^{i} = λ(f, Q) : X_{i} → Y ▪λy ∈ Y ▪ proj(f(y), k).

To see that this works right in a simple case, we observe: e_{k}^{i}(id_{X_{i}})(x) = proj(x, k).

Similarly, we define a_{k}^{i} to be the acceptor for world X_{i} which writes to the k-th location:

a_{k}^{i} = λ(f, Q) : X_{i} → Y ▪ λe ∈ [[exp]]Y ▪ λ(g, R) : Y → Z▪ λz ∈ Z▪ z′

where z′ is the unique element of Z such that update(f(gz), k, e(g, R)z) = f(gz′) if it exists. It is possible that no such z′ exists. If one exists, however, it is guaranteed to be unique by the injectivity aspect of W morphisms. As a sanity check, we see that:

a_{k}^{i}(id_{X_{i}})(e) id_{X_{i}}(x) = update(x, k, e(id_{X_{i}})x).

The following Lemma shows how a_{k}^{k} lines up with a_{new} and how e_{k}^{k} lines up with e_{new}. It is easily justified from the definitions.

Lemma 14 Let k ≥ 1 then a_{k}^{k} = a_{new}(X_{k−1}), and e_{k}^{k} = e_{new}(X_{k−1})

The final important consistency property for a_{k}^{i} and e_{k}^{i} (which also comes by examining the definitions) is given by the following Lemma.

Lemma 15 Let 1 ≤ k < i. Let (f, Q) = \overbrace{×ℕ × ⋯ × ℕ}^{i−k} then a_{k}^{i} = [[acc]](f, Q) a_{k}^{k} and similarly e_{k}^{i} = [[acc]](f, Q) e_{k}^{k}.

3.5.2 Meanings for Bindings: Environments

There is one technical difficulty in defining the denotations of bindings. The meaning of a binding, B, cannot be a global element of Env (viz. a natural transformation from 1 to Env). To see this, we consider the binding B which maps κ (an identifier of type exp) to 1. Thus [[B]] should be such that: [[B]]X_{2}κ = e_{1}^{2} . Now consider the endomorphism f, Q : X_{2}⟶^{W}X_{2}, where f(⟨x, y⟩) = ⟨y, x⟩, and Q = Δ_{X_{2}}—the equality relation on X_{2}. If [[B]] were natural, then we would have to have

[[exp]](f, Q)([[B]]X_{2}κ) = e_{1}^{2} .

But, as the left hand side is equal to e_{2}^{2}, we have a contradiction.

On the other hand, the meaning of a binding cannot be world-independent. We observe that the only time in which we use the meaning of a binding is to find the meaning of a configuration. Furthermore, the meanings for configurations are defined in worlds of a very special form (an X_{i} for some i). It is therefore not surprising that we will only be needing the meaning of an environment in one of the X_{i}’s. Moreover, for any of these worlds it is quite clear what the “right” meaning of the above B is at κ.. The right meaning is e_{1}^{i}. We therefore take the meaning of B to be a function from ℕ to ⋃_{i} Env(X_{i})—actually the domain of [[B]] is {n | n ≥ index(B)} rather than ℕ. [[B]] will have the property that [[B]]i ∈ Env(X_{i}). Specifically, we define [[B]]i, for all i ≥ index(B) as follows:

[[B]]i(α^{θ}) = \{ \begin{matrix}e_{j}^{i} & if B(α^{θ}) = j and θ = exp, \\ a_{j}^{i} & if B(α^{θ}) = j and θ = acc, \\ ⊥_{[[θ]]X_{i}} & otherwise. \end{matrix}

We conclude this Section by mentioning the following important Lemma about [[B]] which follows immediately from Lemma 15.

Lemma 16 Suppose i ≥ index(B), then

[[B]](i + m) = Env(\overbrace{×ℕ × ⋯ × ℕ}^{m})([[B]]i).

3.5.3 Interpreting Configurations

We have a natural transformation from worlds to cpo’s to interpret terms. We have a way to choose the world appropriate to any given state. We are able to think of a state as a semantic entity. We have a function which takes a binding and state length (world) to give an environment. How do we put these together to interpret a configuration ⟨M, B, σ⟩ with length(σ) = i by:

[[M]]X_{i}([[B]]i)  for M of higher type,
[[M]]X_{i}([[B]]i) id_{X_{i}} σ for M of base type.

The following Lemma provides an important consistency result between our interpretation of configurations and the way the model interprets New blocks.

Lemma 17 Let ⟨New ι, κ ← E in P , B, σ⟩ be a program configuration l = 1 + length(σ), and B′ = B[l/ι, l/κ]. Furthermore, suppose [[⟨E, B, σ⟩]] = n ≠ ⊥. Then the following always holds:

[[⟨New ι, κ ← E in P , B, σ⟩]] = S(×ℕ)([[⟨P, B′, σ▪n⟩]])

Proof:

[[⟨New ι, κ ← n in P , B, σ⟩]]

= [[New ι, κ ← n in P]](X_{l−1})([[B]](l − 1))(id_{X_{l−1}})(σ) (def of [[⟨·, ·, ·⟩]])
= S(×ℕ)([[P]](X × ℕ)(u′)(id_{X_{l−1}} ×ℕ)(σ▪n))  (def of [[New ⋯]])
= S(×ℕ)([[P]](X × ℕ)([[B′]]l)(id_{X_{l}})(σ▪n))  (see below)
= S(×ℕ)([[⟨P, B′, σ▪n⟩]])  (def of [[⟨·, ·, ·⟩]])

We have id_{X_{l−1}} ×ℕ = id_{X_{l}} simply by virtue of the definitions of X_{l} = X_{l} × ℕ and the behavior of ×ℕ on W-morphisms. For [[B′]]l = u′, we first note that u′ is defined to be

(Env(×ℕ)([[B]](l − 1)))[a_{new}(X_{l−1})/ι, e_{new}(X_{l−1})/κ].

By definition of B′, [[B′]]l = ([[B]]l)[a_{l}^{l} /ι, e_{l}^{l} /κ]. So, by Lemma 16 we have

[[B′]]l = (Env(×ℕ)([[B]](l − 1)))[a_{l}^{l} /ι, e_{l}^{l} /κ]

Lemma 14 gives a_{l}^{l} = a_{new}(X_{l−1}) and e_{l}^{l} = e_{new}(X_{l−1}), from which we can conclude [[B′]]l = u′ as required.

Adequacy

In this thesis, we have formally defined EoA, an Algol-like language which is a variant of Reynolds’s essence of Algol. We have given two different definitions of the semantics for EoA. In Section 2.3 we gave an operational semantics for EoA via a set of Plotkin-style SOS rules. In Section 3.4 we gave a denotational semantics for EoA using the category of functors from state shapes to bottomless cpos. Each semantics carries with it a natural notion of equality between terms in EoA. It should be relatively clear that our operational semantics for EoA is “correct” (in the sense that it matches how we expect EoA code to behave). It is not nearly so clear that the denotational semantics for EoA is “correct.” Thus to show the “correctness” of our denotational model we need to tie its behavior to the behavior of our operational model in a mathematically rigorous way. Ideally, we would like for this connection to be that equality in our denotational semantics coincides with equality in our operational semantics (observational congruence). When we have this correspondence exactly, we call the denotational model fully abstract with respect to the operational model. Unfortunately the semantics of variable allocation (for either block structured allocation or dynamic allocation) has resisted several attempts for fully abstract models. Meyer and Sieber [9] provide a good summary of this difficulty. Although, as we discuss in Chapter 5, some progress has been made towards full abstraction, it looks like we are still quite far away. For example, the denotational model considered here is not fully abstract for EoA [13].

A denotational model which is adequate, but not fully abstract, can still be very useful for deducing observational congruences and other properties of code. Any equalities between terms which we are able to prove using such an adequate denotational model are also observational congruences between terms. Thus, if we establish that our denotational model is adequate, then at least we can say that any equalities which we prove denotationally are “correct.” Unfortunately, since the denotational model is not fully abstract, it will not be possible to prove all observational congruences denotationally.

Section 2.5 contains the precise definition of observational congruence (≡_{obs}) for EoA. The goal of this Chapter is to prove the following theorem

Theorem 18 (Adequacy) The Tennent model defined in Section 3.4 is adequate for EoA. That is, for all EoA terms M, N,

[[M]] = [[N]] implies M ≡_{obs} N

Since the Tennent model is compositional, we need only prove: for all completely closed EoA commands P_{1}, P_{2}, [[P_{1}]] = [[P_{2}]] implies P_{1} ≡_{obs} P_{2}.

We will prove this theorem in two steps. First we will show that the evaluation relation preserves denotation (soundness), that is, if γ ∈ C ∪ L and γ→_{L}γ′ then [[γ]] = [[γ′]]. Then we will prove that (at least for programs) denotation determines the final result of evaluation. That is, if [[⟨P, B, σ⟩]] = σ′ then ⟨P, B, σ⟩↠_{L}⟨skip, B, σ′⟩. This result combined with the fact that →_{L} is the graph of a function gives the result that meaning determines observation, the key property of adequacy. It is then a simple task to prove the precise statement of Theorem 18.

4.1 Soundness

Technically we only need the result of soundness for program configurations (configurations whose term part is a program), however the proof requires a somewhat more general induction hypothesis which is captured by the following Theorem.

Theorem 19 (Soundness) Let γ ∈ C ∪ L. Suppose γ→_{L}γ′ then [[γ]] = [[γ′]].

Proof: The proof divides into two separate cases, depending on whether γ ∈ C or γ ∈ L. The case of γ ∈ L is a simple induction on the derivation of γ→_{L}γ′, (see Figure 2.3 on page 17). The subcases of the rules (beta) and (eval-operator) fall right out by the standard ccc properties of the model. The subcase of (rec-unwind) is slightly more complicated than usual, but still easy.

The case of γ ≡ ⟨Q, B, σ⟩ ∈ C is also a simple induction on the derivation of γ→_{L}γ′ (see Figures 2.4 and 2.5 on page 18, and also the rule (interaction)). The subcase of (interaction) comes directly from the preceding case for γ ∈ L. We will show the case of the rule (New-eval). The other cases are uninteresting.

Recall the rule (New-eval):

⟨P, B′, σ▪n⟩→_{L}⟨P′, B′, σ′▪n′⟩ ; ⟨New ι, κ ← n in P , B, σ⟩→_{L}⟨New ι, κ ← n′ in P′, B, σ′⟩

where l = 1 + length(σ) and B′ = B[l/ι, l/κ]. So suppose

⟨New ι, κ ← n in P , B, σ⟩→_{L}⟨New ι, κ ← n′ in P′, B, σ′⟩,

because ⟨P, B′, σ▪n⟩→_{L}⟨P′, B′, σ′▪n′⟩. Then,

[[⟨New ι, κ ← n in P , B, σ⟩]]
= S(×ℕ)([[⟨P, B′, σ▪n⟩]])  (Lemma 17)
= S(×ℕ)([[⟨P′, B′, σ′▪n′⟩]])  (induction)
= [[⟨New ι, κ ← n′ in P′, B, σ′⟩]] (Lemma 17)

exactly as required.

4.2 The Computability Relation

The following Theorem expresses the other half of the adequacy proof. To prove this Theorem we use the method of Logical Relations, following very much along Plotkin’s lines for PCF [18]. The proof we give uses a syntactic unary logical relation on lterms. The modern trend in adequacy proofs (see [10]) has been to use a inclusive binary logical relation between elements of the denotational model and syntax. We have also proven the Theorem using this modern method. There are various tradeoffs between the two methods. The unary relation requires substantial syntactic work to handle the constants Y_{θ}. On the other hand, parameterizing the model by worlds and extending terms to lterms complicates the relationship between the model and syntax. We are thus unable to come up with a single binary relation between the denotational model and syntax. Instead we require a distinct relation for every possible binding.

Theorem 20 For all Program configurations ⟨P, B, σ⟩,

if [[⟨P, B, σ⟩]] = σ′ then ⟨P, B, σ⟩↠_{L}⟨skip, B, σ′⟩.

We prove this by induction on the structure of terms. The induction hypothesis is stated in the form of a Logical Relation. More precisely, by induction on types we define a series of predicates on lterms which we will call comp_{θ}. Our goal will then be to prove by induction on the structure of terms that all lterms of type θ have the property comp_{θ}.

The task remaining is to find an appropriate definition of comp_{θ} (for all types θ) and then to prove that all lterms [M, B]:θ has the property comp_{θ}. If [M, B]:θ has the property comp_{θ} then we call [M, B] computable. We define the relation comp_{θ} on lterms [M, B] by induction on types as follows:

1. We have two subcases for closed lterms [Q, B] of base type:

(a) [Q, B] : comm. Let i = index(B). [Q, B] has property comp_{comm} iff ∀σ ∈ X_{i} :

[[⟨Q, B, σ⟩]] = σ′ implies ⟨Q, B, σ⟩↠_{L}⟨skip, B, σ′⟩

(b) [Q, B] : exp. Let i = index(B). [Q, B] has property comp_{exp} iff ∀σ ∈ X_{i} :

[[⟨Q, B, σ⟩]]σ = n ≠ ⊥ implies ⟨Q, B, σ⟩↠_{L}⟨n, B, σ⟩

2. [M, B]:θ → τ is closed. [M, B] has property comp_{θ→τ} iff For any closed lterm [N, B]:θ, the closed lterm [(M N), B] has property comp_{τ}.

3. [M, B] : θ is open. Let Dom(π) − Dom B = {α_{1}^{θ_{1}}, …, α_{k}^{θ_{k}}}. [M, B] has

property comp_{θ} iff For all sequences of closed lterms [N_{1}, B] : θ_{1}, … [N_{k}, B] : θ_{k} having properties comp_{θ_{1}}, …, comp_{θ_{k}} respectively, the closed lterm [M[N_{1}/α_{1}^{θ_{1}}] ⋯ [N_{k}/α_{k}^{θ_{k}}], B] has property comp_{θ}.

In other words, [M, B] has property comp_{θ} if all closed instantiations of [M, B] by computable closed lterms is computable.

Of course, in order for this to be useful, we make sure in selecting the definition of comp, that if the closed lterm [P, B] has property comp_{comm} then, for all states σ, σ′ (with length ≥ index(B))

[[⟨P, B, σ⟩]] = σ′ implies ⟨P, B, σ⟩↠_{L}⟨skip, B, σ′⟩.

This requires one extra step from the definition of comp_{comm} in the event that length(σ) > index(B). This extra step can be done either purely operationally or via a combination of denotational and operational reasoning. We choose the latter. Specifically, let κ be a fresh exp identifier, i = length(σ) and B′ = B[i/κ]. Since κ ∉ F V (P),

[[⟨P, B, σ⟩]] = [[⟨P, B′, σ⟩]] = σ′.

If we could also show that the closed lterm [P, B′] has the property comp_{comm}, then ⟨P, B′, σ⟩↠_{L}σ′. Finally, by Property 4 of →_{L} which was

Let α ∉ FV(Q) and i ≤ length(σ), then

⟨Q, B, σ⟩→_{L}⟨Q′, B, σ′⟩ iff ⟨Q, B[i/α], σ⟩→_{L}⟨Q′, B[i/α], σ′⟩.

We can relate the behavior of ⟨P, B′, σ⟩ back to the behavior of ⟨P, B, σ⟩, getting

⟨P, B, σ⟩↠_{L}σ′

as required.

4.2.1 Proving All Lterms Computable

We prove by induction on the structure of terms, that all lterms are computable. We now carefully present the most interesting cases in the proof (although we defer the case for Y_{θ} to the next section). The base cases in a proof by structural induction are identifiers and constants. The inductive cases are applications, λabstractions, and New-variable declarations.

Identifiers come in three flavors. They are: an identifier appearing free in a lterm, an exp identifier appearing in the domain of the binding, and an acc identifier appearing in the domain of the binding. Consider an arbitrary such lterm [α^{θ}, B]. We have:

[α^{θ} ∉ Dom(B)] Any instantiation of the lterm [α^{θ}, B] by a closed computable lterm [N, B]:θ is [N, B] which has property comp_{θ} (by definition).

[θ = exp and B(α^{exp}) = i] Let j = index(B) and σ ∈ X_{j}. In this case we have [[⟨α^{exp}, B, σ⟩]] = proj(σ, i) because

[[⟨α^{exp}, B, σ⟩]] = [[α^{exp}]]X_{j}([[B]]j) id_{X_{j}} σ (def of [[⟨·, ·, ·⟩]])
= (e_{i}^{j} id_{X_{j}})σ  (def of [[B]])
= σ_{i}  (def of e_{i}^{j}).

Operationally, the rule (variable-read) gives the desired result:

⟨α^{exp}, B, σ⟩→_{L}⟨proj(σ, i), B, σ⟩.

[θ = acc and B(α^{acc}) = i] Remember that acc is an abbreviation for exp → comm. We need to show for all closed lterms [E, B] of type exp, that the lterm [(α^{acc} E), B] has property comp_{comm}. Let j = index(B) and σ ∈ X_{j}. We must show that:

[[⟨(α^{acc} E), B, σ⟩]] = σ′ implies ⟨(α^{acc} E), B, σ⟩↠_{L}⟨skip, B, σ′⟩

As

[[⟨α^{acc}, B, σ⟩]]  = [[(α^{acc} E)]]X_{j}([[B]]j) id_{X_{j}} σ (def of [[⟨·, ·, ·⟩]])
[[(α^{acc} E)]]X_{j}([[B]]j) = a_{i}^{j} id_{X_{j}}([[E]]X_{j}([[B]]j))

(def of application and [[B]]),

we have σ′ = a_{i}^{j} id_{X_{j}}([[E]]X_{j}([[B]]j)) id_{X_{j}} σ. The definition of a_{i}^{j} implies that there is an n ∈ ℕ such that [[E]]X_{j}([[B]]j) id_{X_{j}} σ = n and σ′ = update(σ, i, n). We assumed that [E, B] was a computable closed lterm with property comp_{exp}, so ⟨E, B, σ⟩↠_{L}⟨n, B, σ⟩. Finally by a simple induction on the length of the rewriting sequence (using the rule (assigneval-arg)), followed by an application of the rule (variable-write) we have

⟨(α^{acc} E), B, σ⟩↠_{L}⟨α^{acc} n, B, σ⟩→_{L}⟨skip, B, update(σ, i, n)⟩

giving ⟨(α^{acc} E), B, σ⟩↠_{L}⟨skip, B, update(σ, i, n)⟩.

Constants other than Y_{θ} are also relatively straightforward to handle. The following examples represent all of the interesting issues.

[n, B] Let i = index(B) and σ ∈ X_{i}. Since [[⟨n, B, σ⟩]] = [[n]]X_{i}([[B]]i) id_{X_{i}} σ = n,

and ⟨n, B, σ⟩→_{L}^{0}⟨n, B, σ⟩ we are done.

[seq, B] Let i = index(B) and σ ∈ X_{i}. We need to show for all closed computable lterms [P_{1}, B] : comm and [P_{2}, B] : comm that the closed lterm [(seq P_{1} P_{2}), B] has property comp_{comm}. Specifically,

[[⟨(seq P_{1} P_{2}), B, σ⟩]] = σ′ implies ⟨(seq P_{1} P_{2}), B, σ⟩↠_{L}⟨skip, B, σ′⟩.

Suppose [[(seq P_{1} P_{2})]]X_{i}([[B]]i) id_{X_{i}} σ = σ′. From the definition of [[seq]] we can conclude that there is a σ′′ ∈ X_{i} such that [[P_{1}]]X_{i}([[B]]i) id_{X_{i}} σ = σ′′ and [[P_{2}]]X_{i}([[B]]i) id_{X_{i}} σ′′ = σ′. Our original assumption was that both [P_{1}, B] and [P_{2}, B] were closed lterms with property comp_{comm}. Thus, ⟨P_{1}, B, σ⟩↠_{L}⟨skip, B, σ′′⟩ and ⟨P_{2}, B, σ′′⟩↠_{L}⟨skip, B, σ′⟩ An easy induction on the length of the first rewriting sequence (using the rule (seq-eval-arg1)) followed by an application of the rule (seq-discharge) then gives

⟨(seq P_{1} P_{2}), B, σ⟩↠_{L}⟨(seq skip P_{2}), B, σ′′⟩→_{L}⟨P_{2}, B, σ′′⟩↠_{L}⟨skip, B, σ⟩,

giving ⟨(seq P_{1} P_{2}), B, σ⟩↠_{L}⟨skip, B, σ′⟩.

[plus, B] Let i = index(B) and σ ∈ X_{i}. We need to show that for all closed computable lterms [E_{1}, B] : exp and [E_{2}, B] : exp that the closed lterm (plus E_{1} E_{2}) has property comp_{exp}. Specifically, [[⟨(plus E_{1} E_{2}), B, σ⟩]] = n ≠ ⊥ implies ⟨(plus E_{1} E_{2}), B, σ⟩↠_{L}⟨n, B, σ⟩. So, suppose

[[(plus E_{1} E_{2})]]X_{i}([[B]]i) id_{X_{i}} σ = n.

By the definition of [[plus]], we know that there must be n_{1}, n_{2} ∈ ℕ such that:

[[E_{1}]]X_{i}([[B]]i) id_{X_{i}} σ = n_{1}
[[E_{2}]]X_{i}([[B]]i) id_{X_{i}} σ = n_{2}
n_{1} + n_{2} = n

As [E_{1}, B] and [E_{2}, B] are computable, we have ⟨E_{1}, B, σ⟩↠_{L}⟨n_{1}, B, σ⟩ and ⟨E_{2}, B, σ⟩↠_{L}⟨n_{2}, B, σ⟩ Another two simple inductions on the length of these rewriting sequences (one using the rule (plus-eval-arg1) and the other using (plus-eval-arg2)) followed by an application of the rule (plusdo) give

⟨(plus E_{1} E_{2}), B, σ⟩↠_{L}⟨n, B, σ⟩.

Applications fall out easily from comp_{θ} being a logical relation. The case of [(M N), B] closed is immediate. If [(M N), B] is open, Let M : θ → τ and N:θ and let [L, B] be a closed instantiation of [(M N), B] by terms N_{1}, …, N_{k} such that each [N_{j}, B] (for 1 ≤ j ≤ k) is computable. L must have the form (M′ N′) where M′ and N′ are instantiations of M and N respectively such that both [M′, B] and [N′, B] are closed lterms. By induction [M, B] and [N, B] were computable, and so [M′, B] has the property comp_{θ→τ} and [N′, B] has the property comp_{θ}. By definition of comp_{θ→τ}, [(M′ N′), B] has property comp_{τ} exactly as required.

λ-abstractions, [(λα^{θ}▪ M), B]:θ → τ. Let [L, B] be an arbitrary closed instantiation of [(λα^{θ}▪M), B] by computable closed lterms (same general methodology as applications). In order to show that [L, B] has the property comp_{θ→τ} we observe that L ≡ (λα^{θ}▪M′) where M′ is an instantiation of all of the free identifiers of [M, B] other than α^{θ}. The type θ → τ can be uniquely rewritten to be of the form θ_{0} → θ_{1} → … θ_{k} → β for some k ≥ 0 and β ∈ {exp, comm}. To show that [L, B] is computable, it suffices to show, for arbitrary computable closed lterms [N_{0}, B] : θ_{0}, …, [N_{k}, B] : θ_{k}, that the ground term [(L N_{0} N_{1} … N_{k}), B] has the property comp_{β}. For concreteness, we show the result for β = exp. Let i = index(B) and σ ∈ X_{i}. Suppose [[L N_{0} ⋯ N_{k}]]X_{i}([[B]]i) id_{X_{i}} σ = n ≠ ⊥, then by Soundness

[[(M′[N_{0}/α^{θ}]) N_{1} ⋯ N_{k}]]X_{i}([[B]]i) id_{X_{i}} σ = [[L N_{0} ⋯ N_{k}]]X_{i}([[B]]i) id_{X_{i}} σ = n.

But [M′[N_{0}/α^{θ}], B] is a computable closed lterm, therefore the closed lterm [((M′[N_{0}/α^{θ}]) N_{1} ⋯ N_{k}), B] is also computable. We now have:

⟨L N_{0} ⋯ N_{k}, B, σ⟩→_{L}⟨(M′[N_{0}/α^{θ}]) N_{1} ⋯ N_{k}, B, σ⟩↠_{L}⟨n, B, σ⟩.

New-declarations, [(New ι, κ ← E in P), B]. Without loss of generality, suppose this lterm is closed. Let i = index(B) and σ ∈ X_{i}. By the identifier convention we may assume that ι ∉ Dom(B) and κ ∉ Dom(B). We must show that

[[⟨New ι, κ ← E in P , B, σ⟩]] = σ′

implies ⟨New ι, κ ← E in P , σ⟩↠_{L}⟨skip, σ′⟩.

We make the following abbreviations:

B′ = B[(i + 1)/ι, (i + 1)/κ]
n = [[E]]X_{i}([[B]]i) id_{X_{i}} σ = [[⟨E, B, σ⟩]]

Suppose [[⟨New ι, κ ← E in P , B, σ⟩]] = σ′. The fact that the New-block is defined tells us that n ≠ ⊥. By induction [E, B] has property comp_{exp}. Since [E, B] is a closed lterm, we have ⟨E, B, σ⟩↠_{L}⟨n, B, σ⟩. Then

⟨New ι, κ ← E in P , B, σ⟩↠_{L}⟨New ι, κ ← n in P , B, σ⟩.

By soundness, [[⟨New ι, κ ← E in P , B, σ⟩]] = [[⟨New ι, κ ← n in P , B, σ⟩]] = σ′. By Lemma 17,

[[⟨New ι, κ ← n in P , B, σ⟩]] = S(×ℕ)[[⟨P, B′, σ▪n⟩]] = σ′.

By definition of S(×ℕ), there must exist an n′ such that

[[⟨P, B′, σ▪n⟩]] = σ′▪n′.

But [P, B′] is a closed lterm with property comp_{comm}. Note that we were not doing an induction on the structure of lterms, but an induction on the structure of (ordinary) terms. As, P is subterm of (New ι, κ ← E in P), this is a sound application of our induction hypothesis. Thus using the computability of [P, B′], we have that:

⟨P, B′, σ▪n⟩↠_{L}⟨skip, B′, σ′▪n′⟩

An easy induction on the length of the rewriting sequence (using the rule (Neweval)) followed by an application of the rule (New-discharge) gives

⟨New ι, κ ← E in P , B, σ⟩ ↠_{L} ⟨New ι, κ ← n in P , B, σ⟩
↠_{L} ⟨New ι, κ ← n′ in skip, B, σ′⟩
→_{L} ⟨skip, B, σ⟩

4.2.2 Handling Y

As with PCF [18], the main difficulty in proving all terms computable is caused by the recursion operators, Y_{θ}. Before we handle this last case, we need to do some substantial preliminary work.

We make the obvious generalization of Plotkin’s work to EoA. We approximate Y_{θ} by terms Y_{θ}^{(n)}, (for n ≥ 0). To do so we first define terms Ω_{exp} ≡ Y_{exp}(λα^{exp}▪α^{exp}), Ω_{comm} ≡ Y_{comm}(λα^{comm}▪α^{comm}), and Ω_{θ→τ} = (λα^{θ}▪Ω_{τ}). We then define Y_{θ}^{(n)} by induction on n as follows:

Y_{θ}^{(0)} ≡ Ω_{(θ→θ)→θ} and Y_{θ}^{(n+1)} ≡ (λα^{θ→θ}▪ (α^{θ→θ} (Y_{θ}^{(n)} α^{θ→θ})))

We then have the following useful combinatorial properties for all W-worlds X, W-morphisms f : X → Y, u ∈ Env(X), and m ∈ [[θ → θ]]Y

[[Y_{θ}]]Xufm = ⨆_{n≥0} (m id_{Y})^{n} (⊥_{[[θ]]X}),
[[Ω_{θ}]]Xu = ⊥_{[[θ]]X},
[[Y_{θ}^{(n)}]]Xufm = (m id_{Y})^{n} (⊥_{[[θ]]X}),
[[Y_{θ}]]Xu = ⨆ {[[Y_{θ}^{(n)}]]Xu : n ≥ 0}.

We define ⪯ to be the least relation between terms such that:

• Ω_{θ} ⪯ M:θ and Y_{θ}^{(n)} ⪯ Y_{θ} for all θ, n ≥ 0,

• M ⪯ M,

• If M : (θ → τ) ⪯ M′ : (θ → τ) and N : θ ⪯ N′ : θ then (λα^{θ′}▪ N) ⪯ (λα^{θ′}▪ N′), and (MN) ⪯ (M′N′),

• If E:exp ⪯ E′:exp and P:comm ⪯ P′:comm then

(New ι, κ ← E in P) ⪯ (New ι, κ ← E′ in P′).

The following is the appropriate analogue of Plotkin’s Lemma 3.2 [18]

Lemma 21 If M ⪯ N, ⟨M, B, σ⟩ ∈ C and ⟨M, B, σ⟩→_{L}⟨M′, B, σ′⟩ then either M′ ⪯ N and σ = σ′ or else for some N′ and σ′, ⟨N, B, σ⟩→_{L}⟨N′, B, σ′⟩ and M′ ⪯ N′.^{1}

Proof: In order to prove the above Lemma we must first establish the analogous result for M→_{L}M′, specifically

If M ⪯ N, M→_{L}M′ then either M′ ⪯ N or else for some N′

N→_{L}N′ and M′ ⪯ N′.

The proof of the above result for M→_{L}M′ is a simple induction on the derivation of M ⪯ M′. The proof of the Lemma itself is then merely a tedious induction on the derivation of ⟨M, B, σ⟩→_{L}⟨M′, B, σ′⟩, with the case of (interaction) coming directly from the preceding result.

We are now ready to prove that all lterms with term part of the form Y_{θ} have the property comp_{(θ→θ)→θ}. Let [Y_{θ}, B] be an arbitrary such lterm. We start by observing that any type θ is of the form τ_{1} → τ_{2} → ⋯ → τ_{k} → β, where β ∈ {exp, comm}. To show that [Y_{θ}, B] has the property comp_{(θ→θ)→θ}, it is enough to show that for arbitrary computable closed lterms [N_{0}, B] : θ → θ, [N_{1}, B] : τ_{1}, …, [N_{k}, B], the closed lterm [(Y_{θ}N_{0} ⋯ N_{k}), B] has property comp_{β}. The two cases for β are essentially similar; we argue the case of β = exp.

Let i = index(B), and σ ∈ X_{i}. We must show that

[[(Y_{θ}N_{0} ⋯ N_{k})]]X_{i}([[B]]i) id_{X_{i}} σ = c ≠ ⊥

implies that

⟨(Y_{θ}N_{0} ⋯ N_{k}), B, σ⟩↠_{L}⟨c, B, σ⟩.

So assuming the hypothesis, we have:

[[Y_{θ}]]X_{i}([[B]]i) id_{X_{i}} m_{0} id_{X_{i}} ⋯ id_{X_{i}} m_{k} id_{X_{i}} σ = c

1In order to avoid an endless profusion of “primes” and subscripts, we temporarily abandon our metavariable convention (for M and N) for the statement and proof of this Lemma.

Where m_{j} = [[N_{j}]]X_{i}([[B]]i) (for 0 ≤ j ≤ k). We remarked earlier that

[[Y_{θ}]]X_{i}([[B]]i) = ⨆_{n≥0}[[Y_{θ}^{(n)}]]X_{i}([[B]]i).

This will give us the following:

( ⨆_{n≥0}[[Y_{θ}^{(n)}]]X_{i}([[B]]i)) id_{X_{i}} m_{0} id_{X_{i}} ⋯ id_{X_{i}} m_{k} id_{X_{i}} σ = c

⨆_{n≥0} {[[Y_{θ}^{(n)}]]X_{i}([[B]]i) id_{X_{i}} m_{0} id_{X_{i}} ⋯ id_{X_{i}} m_{k} id_{X_{i}} σ} = c

Since c ∈ ℕ, and ℕ is flat, then there is a least n such that:

[[Y_{θ}^{(n)}]]X_{i}([[B]]i) id_{X_{i}} m_{0} id_{X_{i}} ⋯ id_{X_{i}} m_{k} id_{X_{i}} σ = c
[[Y_{θ}^{(n)}N_{0} ⋯ N_{k}]]X_{i}([[B]]i)σ = c

All lterms with term part Y_{θ}^{(n)} are computable. A simple induction on n shows why. For the basis we have that [Y_{θ}^{(0)}, B] ≡ [Ω_{(θ→θ)→θ}, B] is computable (for any binding B), since Ω_{(θ→θ)→θ} denotes ⊥_{[[(θ→θ)→θ]]}. For the inductive case, [Y_{θ}^{(n+1)}, B] ≡ [(λα^{θ→θ}▪ (α^{θ→θ}(Y_{θ}^{(n)}α^{θ→θ}))), B], we use the earlier cases in proving that all terms are computable (applications and λ-abstractions) to show that if [Y_{θ}^{(n)}, B] is computable, then so is [Y_{θ}^{(n+1)}, B].

Consequently, (Y_{θ}^{(n)}N_{0} ⋯ N_{k}) has property comp_{exp}. Thus,

⟨Y_{θ}^{(n)}N_{0} ⋯ N_{k}, B, σ⟩↠_{L}⟨c, B, σ⟩

Finally, we apply Lemma 21 and so we can say that:

⟨Y_{θ}N_{0} ⋯ N_{k}, B, σ⟩↠_{L}⟨c, B, σ⟩

and thus conclude that [Y_{θ}, B] is computable.

4.3 A General Adequacy Theorem for Functor Category Models

Until now we have focused our attention to Tennent’s model of EoA. We abstract away the details of Tennent’s model and decribe those properties of the model upon which the adequacy proof of the preceeding Sections depended. We limit our attention to models of EoA which use a functor category of the form D^{A} where A is now permitted to be any small category. We assume [[·]] is standard c.c.c. interpretation of EoA in D^{A}. That is it is a specification of the category, objects for the meanings of base types, and morphisms for the meanings of constants. We assume that [[θ → τ]] is the exponent object [[θ]] ⇒ [[τ]]. We assume that meanings for applications and λ-abstractions are found in the standard ways.

Our conditions will provide constraints on what [[exp]] and [[comm]] must look like, and how the constants must fit together. It will also place some constraints between the interpretation of New blocks and the meanings for base type. Finally, we must also be able to find appropriate entites in the model to interpret bindings and states so that everything will fit together.

Our first condition is a restriction on A. We must be able to find an appropriate sequence of worlds in A to model configurations with state part of length 0, and length 1 and length 2, … To state this precisely we define the category NAT = ⟨ℕ, ≥⟩. NAT has ℕ as objects, and for n greather than or equal to m, it has a morphism n ≥ m : m → n. We require that there exist a covariant functor L : NAT → A, in order to get off the ground. All of our constraints will be phrased in terms of L. In a generalized adequacy proof, we would use the object L(i) of A wherever we used the object X_{i} of W in the old proof. In place the morphism ×ℕ^{k} : X_{i} → X_{i+k}, we now use the morphism L(i + k ≥ i) : L(i) → L(i + k).

We require that [[exp]](L(i)) “looks like” ℕ^{i} → ℕ_{⊥}, and that [[comm]](L(i)) looks like ℕ^{i} → ℕ_{⊥}^{i}. So we require that ap_{exp}⟨e, σ⟩, when viewed as a function of σ, is isomorphic to ℕ^{i} → ℕ_{⊥} (wlog we assume it is equal). Similarly we require that ap_{comm}⟨c, σ⟩, when viewed as a function of σ, is isomorphic to ℕ^{i} → ℕ_{⊥}^{i} (wlog we assume it is equal). We should really index ap_{exp} and ap_{comm} by the world L(i) in which the first argument lives, but this should always be evident from context. We also require that [[exp]](L(m ≥ n)) and [[comm]](L(m ≥ n)) behave sensibly. Specifically, we require:

ap_{exp}⟨[[exp]](L(m ≥ n))(e), ⟨v_{1}, … v_{m}⟩⟩ = ap_{exp}⟨e, ⟨v_{1}, … v_{n}⟩⟩,

and

ap_{comm}⟨[[exp]](L(m ≥ n))(c), ⟨v_{1}, … v_{m}⟩⟩
= \{ \begin{matrix}⟨v′_{1}, … v′_{n}, v_{n+1}, … v_{m}⟩ & if ap_{exp}⟨c, ⟨v_{1}, … v_{n}⟩⟩ = ⟨v′_{1}, …, v′_{n}⟩ \\ ⊥ & otherwise. \end{matrix}

We require that all of the constants other than Y_{θ} (n, skip, IFexp_{exp}, seq, IFexp_{comm}, succ, and plus) satisfy the obvious equations. For Y_{θ}, we require that

[[Y_{θ}]](L(i))(f) = ⨆_{n≥0}(f id_{L(i)})^{n}(⊥_{[[θ]](L(i))}).

Finally, we must be able to find “locations” in the model which fit together properly with each other and with L. For each i and k ≤ i we need to find an acceptor a_{k}^{i} ∈ [[acc]](L(i)) which corresponds to the acceptor for the k-th component of the state. Similarly we need an expressor e_{k}^{i} ∈ [[exp]](L(i)). These must fit together as they did for Tennent’s model, specifically,

a_{k}^{i} = [[acc]](L(i ≥ k)) a_{k}^{k},
e_{k}^{i} = [[exp]](L(i ≥ k)) e_{k}^{k} .

Finally, not only must they fit together properly, but they must behave like the right locations. The following condition is sufficient:

ap_{comm}⟨ap_{acc}L(k)⟨a_{k}^{k}, e⟩, σ⟩ = \{ \begin{matrix}update(σ, n, k) & if ap_{exp}⟨e, σ⟩ = n ≠ ⊥, \\ ⊥ & otherwise \end{matrix}
ap_{exp}⟨e_{k}^{k}, σ⟩ = proj(σ, k)

We can then define the meanings for bindings as in Section 3.5.2. Finally we define the meaning of a configuration ⟨M, B, σ⟩ with length(σ) = i as follows:

[[M]](L(i))([[B]]i)  for M of higher type,
[[M]](L(i))([[B]]i) id_{X_{i}} σ for M of base type.

Lastly we need the appropriate analogue of Lemma 17, which is: for all program configurations ⟨New ι, κ ← E in P , B, σ⟩, if [[⟨E, B, σ⟩]] = n ≠ ⊥, l = 1 + length(σ), and B′ = B[l/ι, l/κ].

[[⟨New ι, κ ← E in P , B, σ⟩]]
= \{ \begin{matrix}⟨v_{1}, …, v_{l}⟩ & if [[⟨P, B′, σ▪n⟩]] = ⟨v_{1}, …, v_{l}, v_{l+1}⟩, \\ ⊥ & otherwise. \end{matrix}

And that’s all.

Comparing Models of Block Structure

Although the field of denotational semantics has made many strides in its history, there is still great difficulty in finding reasonable models of imperative features and variable allocation. The most commonly used model of imperative features is the “marked store” model, which is little more than an encoding of the usual operational semantics—providing little added insight to justify the additional technical background required to understand the denotational semantics. A guiding concern in the design of a denotational semantics is for the semantics to be “fully abstract.” A fully abstract semantics would by definition, contain precisely the information about a term that we require in order to understand its behavior in all contexts. In other words we would have “abstracted away” from all of the irrelevant details. As discussed in [9] the marked stores model fails very early on in the quest to full abstraction for block structured local variables. The failure results from an inability to fully understand the behavior of commands.

5.1 Advanced Models of Block Structure

During the 1980’s several more promising models of block structure have been presented. Reynolds and Oles developed a model of block structure based on a category of functors from a category of state shapes to a category of bottomless cpos [15–17, 21]. The work of Reynolds and Oles has been simplified in Tennent’s model of Reynolds’s Specification Logic [25]. Tennent separated the issues of implicit coercions and block structure, which had been intertwined in the model of Reynolds and Oles. Tennent also found a few other technical simplifications of the appropriate category of state shapes which should be used for modeling block structure. In addition, to properly model interference (which helps in understanding how higher order objects behave) Tennent further modified the category of state shapes and chose an “ad hoc” definition for [[comm]], rather than taking the functor S ⇀ S. Finally, in order to model a principle of “noninterference abstraction,” Tennent and O’Hearn [13] adjusted the category of state shapes which Tennent originally used in [25].

Along a different line, Halpern, Meyer and Trakhtenbrot developed a model [5] (now referred to as the HMT store model), which Meyer and Sieber [9] summarize as follows:

Halpern-Meyer-Trakhtenbrot proposed a formal definition of the support of a function from Stores to Stores. Intuitively the support of a store transformation p is the set of locations which p can read or write. In the HMT store model [5], Prog [comm] is taken to be the set of p with finite support. To model local variables, the notion of support is extended to the type Loc → Prog of block bodies regarded as a function of their free location identifier. The semantical space used to interpret such block body functions is again restricted to be the elements in Loc_{⊥}→_{c}P rog with finite support. Since there are an infinite number of locations, this restriction guarantees that a location can be found which is not in the support of any given block body. Then local storage allocation for a block begin new x; body end is (uniquely) determined by the rule that x be bound to any location not in the support of the function denoted by λx.body.

Meyer and Sieber developed what they called “The invariant-preserving model,” which is now coming to be called the Meyer-Sieber model. This model validates the following reasoning principle:

Let Q be of type comm → comm, and P of type comm. Let r be a property of states such that support(r) ∩ support(Q) = ∅. If r is an invariant of P, then r is also an invariant of Q(P).

None of the above models is fully abstract for EoA. We will now examine the relative merits of later models—the Tennent model, the O’Hearn-Tennent model and the Meyer-Sieber model. It is not obvious whether the Tennent model and the O’Hearn-Tennent differ in their equational theory. In fact it is not obvious which, if either, has the stronger equational theory.

5.2 The Meyer-Sieber Examples

Our discussion focuses on the Meyer-Sieber Examples [9]. Specifically, we examine the statement of these examples in EoA and address how the Tennent and O’Hearn-Tennent models handle them. All but the last of the Meyer-Sieber Examples hold for the Meyer-Sieber model. All of the examples which can be stated in EoA hold for the Tennent and O’Hearn-Tennent models. Since Example 6 critically uses the fact that the sample language is based on locations rather than variables, this example cannot be translated into EoA and thus it is not handled by the Tennent and O’Hearn-Tennent models. We will see in Section 5.3, slight perturbations of the problems will lead to either open questions or outright failures.

Example 1 The block below is replaceable simply by the call P.

begin new x; P; % P is declared elsewhere

end

The translation of this block into EoA would something like:

New ι, κ ← 0 in P

Contrary to the claim at the end of [25, p. 158], the Tennent model (and also the Tennent-O’Hearn model) does satisfy this equivalence—without additional constraints on command meanings. A discussion of this equality appears in [13, §5, Example 1], the bulk of the justification being a proof of our Lemma 13.

Example 2 The block below always diverges.

begin new x; x := 0; P; % P is declared elsewhere if contents(x) = 0 then diverge fi

end

The translation of this block into EoA would be something like:

New ι, κ ← 0 in

P; % P is declared elsewhere

IFexp_{exp}(κ = 0) diverge skip

This Example is not explicitly discussed in [13], but it is quite simple to prove. Specifically, let C be the above EoA command. We show for arbitrary worlds X and Y, environments u ∈ Env(X), morphisms f : X → Y and states y ∈ Y, that [[C]]Xufy is undefined. Let p = u(P). Since ×ℕ; f × ℕ = f; ×ℕ, we have p(×ℕ; f × ℕ) = p(f; ×ℕ). Suppose that p(f; ×ℕ)(y▪0), is defined, say it is y′▪n. We must show that n is 0. Let Y′ = Y × {0}. By the uniformity condition on elements of [[comm]]:

\underbrace{(S(⌈Y′); p(f; ×ℕ))(y▪0)}_{y′▪n^{∥}} = (p(f; ×ℕ; ⌈Y′); S(⌈Y′))y▪0.

Any state which is equal to the right hand side must lie in the set Y′. Thus, y′▪n is of the form y′▪0, and so n = 0.

Example 3 The blocks

begin new x; new y; x := 0; y := 0; Q(x, y) end

and

begin new x; new y; x := 0; y := 0; Q(y, x) end

are equivalent.

The EoA version of the first block is:

New ι_{1}, κ_{1} ← 0 in (New ι_{2}, κ_{2} ← 0 in Q(ι_{1})(κ_{1})(ι_{2})(κ_{2}))

The EoA version of the second block is:

New ι_{1}, κ_{1} ← 0 in (New ι_{2}, κ_{2} ← 0 in Q(ι_{2})(κ_{2})(ι_{1})(κ_{1}))

where Q is an identifier of type acc → exp → acc → exp → comm. This equality was also discussed in [13, §5, Example 2]. They say: “The equivalence can be shown by a straightforward calculation using an endomorphism that exchanges the two ℕ-valued components in a world of the form X × ℕ × ℕ, thus exchanging the declared variables.” Properly using this endomorphism will require repeatedly moving it across the commutativity conditions required by the functor ⇒. We then observe that this endomorphism is also an isomorphism in the category of possible worlds, thus we can use Lemma 13 to move the endomorphism across the command.

Example 4 The block below always diverges.

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

end For the translation of this block into EoA, we beta-reduce the desugared version of the procedure declaration to get:

New ι_{1}, κ_{1} ← 0 in
New ι_{2}, κ_{2} ← 0 in
Q(ι_{2} (2 ∗ κ_{2})) ;
IFexp_{comm}(κ_{1} = 0) diverge skip

This example is more complicated than the earlier ones, and is not specifically addressed in [13], but it is easily handled using the methods developed there. Specifically it is handled by the semantic definition of non-interference (#) which they give in Section 3. One merely needs to formalize the usual intuition. We have the following:

Q#κ_{1}  (since Q is non-local)
ι_{2}(2 ∗ κ_{2})#κ_{1}  (obvious)
Q(ι_{2}(2 ∗ κ_{2}))#κ_{1}

where the last step comes from the semantic version of the following “procedurecall law”: if C: θ → θ′ and an identifier c is not free in C or E then C#E ⇒ (∀c:θ.c#E → C(c)#E). From this we can conclude that after the execution of Q(ι_{2}(2 ∗ κ_{2})) the value of κ_{1} is unchanged, namely 0.

Example 5 The block below always diverges.

begin new x; procedure Add 2; %Add 2 is the ability to add 2 to x

begin x := contents(x) + 2 end x := 0; Q(Add 2); % Q is declared elsewhere if contents(x) mod 2 = 0 then diverge fi

end

For the translation of this block into EoA we again beta-reduce the desugared version of the procedure declaration getting:

New ι, κ ← 0 in

Q(ι (κ + 2)) ;

IFexp_{exp}(κ mod 2 = 0) diverge skip

O’Hearn and Tennent also discuss this example in [13, §6]. Their argument uses specification logic, rather than a direct semantic proof. Moreover, their argument relies on the principle of non-interference abstraction. Whether or not this principle is sound for the Tennent model is an open question. The O’Hearn-Tennent model was introduced specifically to overcome this shortcoming. There does, however, exist a semantic proof of this equality for the original Tennent model. Furthermore, the reasoning carries over directly to the O’Hearn-Tennent model. To see how to prove this in the Tennent model, we make the informal observation that

Q(ι (κ + 2))#(κ mod 2).

The additional constraint on elements of [[comm]], requires the equivalence class component of the endomorphism [κ mod 2] must be respected by [[Q(ι (κ + 2))]]. Thus the resulting state (if any) of Q(ι (κ + 1)) must have the same value of (κ mod 2) as the initial state.

As we discuss in the next Section, there is a slight perturbation of the above block whose divergence (in the Tennent model) is an open question.

Example 6 The block

begin new x; procedure AlmostAdd 2; begin if z = x then x := 1 else x :=contents(x) + 2 fi end x := 0; Q(Add 2); % Q is declared elsewhere if contents(x) mod 2 = 0 then diverge fi

end

always diverges.

A test for equality of locations is not a part of EoA, nor is it possible to simulate such a test in EoA. Therefore Example 6 is not relevant to EoA.

Example 7 The block

begin new x; procedure Add 1; begin x := Contents(x) + 1 end; P (Add 1) end

is observationally congruent to the block

begin new x; procedure Add 2; begin x := Contents(x) + 2 end; P (Add 2) end.

The desugared EoA encodings of these blocks are:

New ι, κ ← 0 in (λAdd 1▪ P (Add 1))(ι (κ + 1))

and

New ι, κ ← 0 in (λAdd 2▪ P (Add 2))(ι (κ + 2)).

To see why this equality holds, we let V = ℕ and V′ = {n ∈ ℕ | n is even}. Given any world X, we can define a W-isomorphism (i, T_{X×V′}) : X × V → X × V′, where i(x▪n) = x▪(2n), and T_{X×V′} is the universally true binary relation on X × V′. As with the argument for Example 5, we know that P (Add 2)#Parity(κ), thus the behavior of P (Add 2) in world X × V′ completely projects into its behavior on states of the form x▪2n in world X × V. In other words, for the u that arises in interpreting the second block, we have:

[[P (Add 2)]](X × V)(u)(id_{X×V})(x▪n) = [[P (Add 2)]](X × V)(u_{2}))(id_{X×V′})(x▪n)

where u_{2} = Env(⌈(X × V′))u. From this we need to show:

[[P (Add 1)]](X × V)(u_{1})(id_{X×V})(x▪n) = [[P (Add 2)]](X × V)(u_{2})(id_{X×V′})(x▪2n)

using

u_{1}(P) = [[comm → comm]](×ℕ)p = p_{1}
u_{2}(P) = [[comm → comm]](×ℕ; ⌈(X × V′)) = p_{2}
c_{1} = u_{1}(Add 1)
c_{2} = u_{2}(Add 2).

It is sufficient to prove the following equality, which follows via an argument analogous to that for Example 3, using the isomorphism (i, T_{X×V′}).

p (id_{×ℕ}) (c_{1})(id_{X×V})(x▪n) = p (id_{×ℕ;⌈(X×V′)}) (c_{2})(id_{X×V′})(x▪2n)

There is one other example of an equivalence which the Tennent model satisfies, which is interesting[13, §5,Example 3]. This does not appear as one of the Meyer-Sieber examples, and Sieber claims that this example fails in the Meyer-Sieber model. It is essentially

Example 8 The following blocks are equivalent:

begin new x; x := 1; P (x); % P is declared elsewhere

end

and

P (1)

Operationally, the idea is that P does not have write access to X, so that whenever x is evaluated as part of the call P (x), x must produce 1.

5.3 Failure of Full Abstraction

The fact that the Tennent and O’Hearn-Tennent models correctly handle all of the relevant Meyer-Sieber examples demonstrates the substantial power of these models. Looking at these examples alone, however, is quite misleading. There are slight perturbations of the Meyer-Sieber examples which the Tennent or O’Hearn-Tennent models do not handle (or where their performance is an open problem). Furthermore, there is a simple example which the Meyer-Sieber model (and most other models) handles but the Tennent and O’Hearn-Tennent models do not.

We start with the Example due to O’Hearn [13] which first showed the failure of full abstraction (for both the Tennent and O’Hearn-Tennent models) [13].

Example 9 The block

begin new x; P (skip) end

is observationally congruent to the block

begin new x; procedure Add 1; begin x := Contents(x) + 1 end; P (Add 1) end.

This is just a slight perturbation of Example 7. Intuitively the Tennent and O’Hearn Tennent models fail because even though P does not have complete access to x from Add 1, P can check whether or not Add 1 has a side-effect on x. Specifically, they let p ∈ [[comm → comm]]X be defined as follows: for any f : X⟶^{W}Y, c ∈ [[comm]], g : Y ⟶^{W}Z, and s ∈ S(Z),

pfcgs = \{ \begin{matrix}s & if cgs = s, \\ undefined, & otherwise. \end{matrix}

Then

p(id_{X})([[skip]]Xu)(id_{X})(s) = s,

whereas

p(×ℕ)([[x := x + 1]](X × ℕ)(u′))(id_{X×V})(s▪0)

is undefined, where u and u′ are the appropriate non-local and local environments, respectively.

From O’Hearn’s counterexample to full abstraction, we manage to construct an example which is handled by most other models, but neither the Tennent model nor the O’Hearn-Tennent model handle.

Example 10 The block

begin new x; P (x := x + 1; x := x + 1) end

is observationally congruent to the block

begin new x; P (x := x + 2) end

Intuitively, this failure is because these models are sensitive to intermediate states encountered during program execution. Specifically, we modify the proof for the preceding example and take instead

pfcgs = c(g; ⌈{z, c(g)z})z.

Then we have

p(×ℕ)([[x := x + 2]](X × ℕ)(u))(id_{X×V})(s▪0) = s▪2

whereas

p(×ℕ)([[x := x + 1; x := x + 1]](X × ℕ)(u))(id_{X×V})(s▪0)

is undefined, where u is the appropriate local environment.

Finally, we have a perturbation of Example 5 which is handled by the O’Hearn-Tennent model, but whether or not the Tennent model handles is it an open problem.

Example 11 The block below always diverges.

begin new x; procedure Add 2; %Add 2 is the ability to add 2 to x begin x :=contents(x) + 1; x :=contents(x) + 1; end

x := 0;

Q(Add 2); % Q is declared elsewhere

if contents(x) mod 2 = 0 then diverge fi end

O’Hearn and Tennent justified this example by showing that the O’Hearn-Tennent model satisfies a principle called “Non-Interference Abstraction,” which has the following as a special case

P #R & {R}C{R} ⇒ {R}P (C){R}.

In English, this says that if P does not interfere with property R and property R is preserved by C, then property R is preserved by the call P (C). This principle is sufficient to justify the above Example.

It is an open problem as to whether or not the Tennent model satisfies the principle of Non-Interference Abstraction. It is also an open problem as to whether or not the Tennent model and the O’Hearn-Tennent model have the same equational theories. Furthermore, in the event that the equational theories differ, it is not obvious whether one must be stronger than the other, or if they could be incomparable.

Conclusion

We have given the first complete exposition of a Structured Operational Semantics for an Algol-like language, and have shown that the Tennent and O’Hearn-Tennent functor category models are adequate with respect to this semantics. As the Tennent and O’Hearn-Tennent models were themselves designed to provide a model of Reynolds’s Specification Logic [22], the adequacy result of this thesis can be taken to be an adequacy result for Specification Logic. Thus this thesis provides a concrete connection between Specification Logic and our operational understanding of how Algol-like code should behave.

One novel feature used in defining the operational semantics is the handling of New-blocks. Specifically, the use of the initialization for the new variable and the rule (New-eval) seemed to make the technical work in the Adequacy proof flow cleanly.

Having established the adequacy of these models, the next question to ask is “Are they fully-abstract?” Section 5.3 shows that they are not. Another reasonable question to ask is how close do they come? In other words, what “partial full-abstraction” results hold. For example, the model is fully abstract for the equational theory of EoA commands with free identifiers restricted to be of type exp or comm. On the other hand, the counterexamples of Section 5.3 reflect a failure of full abstraction for the equational theory of EoA terms with free identifiers restricted to be of type comm → comm or below. Related to lower-order full abstraction results are “half-full abstraction” results. Specifically, for what collection of C (if any) is the model fully abstract for equalities of the form C = P where P is a program? What about when P is a closed command?

Aside from taxonomy, the natural question is to ask as to whether or not we can “repair” these models so as to either achieve full abstraction, or at least come closer to it. It might be possible to obtain models with equational theories closer to full abstraction by perturbing the model in subtle ways. The generalization of the adequacy proof given in Section 4.3 provides some loose conditions on these perturbations to insure that they preserve adequacy.

61

Bibliography

[1] Henk P. Barendregt. The Lambda Calculus: Its Syntax and Semantics, volume 103 of Studies in Logic and the Foundations of Mathematics. North-Holland Publishing Co., Amsterdam, second edition, 1984.

[2] H. Bekic. Definable operations in general algebras and the theory of automata and flowcharts. Technical report, IBM Laboratory, Vienna, 1969. Also, pp. 30-55 in Programming Languages and their Definition, H. Bekic (ed. C. B. Jones), Lecture Notes in Computer Science 177, Springer-Verlag, Berlin (1984).

[3] G. Berry, P.-L. Curien, and J.-J. Lévy. Full abstraction for sequential languages: the state of the art. In Maurice Nivat and John C. Reynolds, editors, Algebraic Methods in Semantics, chapter 3, pages 89–132. Cambridge Univ. Press, 1985.

[4] Joseph Y. Halpern, Albert R. Meyer, and Boris A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? In Conference Record of the Eleventh ACM Symposium on Principles of Programming Languages, pages 245–257, 1983.

[5] Joseph Y. Halpern, Albert R. Meyer, and Boris A. Trakhtenbrot. The semantics of local storage, or what makes the free-list free? Technical Report MIT/LCS/TM-258, Massachusetts Institute of Technology, April 1984.

[6] Trevor Jim and Albert R. Meyer. Full abstraction and the context lemma. Technical report, MIT Laboratory for Computer Science, 1991.

[7] Peter J. Landin. A correspondence between Algol 60 and Church’s lambda notation. Communications of the ACM, 8:89–101; 158–165, 1965.

[8] Arthur F. Lent. The category of functors from state shapes to bottomless cpos is adequate for block structure. Master’s thesis, Massachusetts Institute of Technology, February 1992.

[9] Albert R. Meyer and Kurt Sieber. Towards fully abstract semantics for local variables: Preliminary report. In Conference Record of the Fifteenth Annual ACM Symposium on Principles of Programming Languages, pages 191–203, 1988.

[10] Peter D. Mosses and Gordon D. Plotkin. On proving limiting completeness. SIAM Journal on Computing, 16:179–194, 1987.

[11] Evelyn Nelson. On exponentiating exponentiation. Journal of Pure and Applied Algebra, 20:79–91, 1981.

[12] Peter O’Hearn and Robert Tennent. Semantics of local variables. In P.T. Johnstone M.P. Fourman and A.M.Pitts, editors, Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1992. Conference held in 1991.

[13] Peter O’Hearn and Robert Tennent. Semantical analysis of specification logic: Part 2. Information and Computation, 1993. In Press.

[14] Peter W. O’Hearn. The Semantics of Non-Interference: a Natural Approach. PhD thesis, Queen’s University, Kingston, Canada, 1990.

[15] Frank J. Oles. A category-theoretic approach to the semantics of programming languages. PhD thesis, Syracuse Univ., 1982.

[16] Frank J. Oles. Type algebras, functor categories, and block structure. Technical Report DAIMI PB-156, Aarhus Univ., Computer Science Dept., Denmark, 1982. Proc. U.S.-French Joint Symp. Applications of Algebra to Language Definition and Compilation, to appear.

[17] Frank J. Oles. Type algebras, functor categories, and block structure. In Maurice Nivat and John C. Reynolds, editors, Algebraic Methods in Semantics, chapter 15, pages 543–573. Cambridge Univ. Press, 1985.

[18] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Science, 5(3):223–256, December 1977.

[19] Gordon D. Plotkin. A structural approach to operational semantics. Technical Report DAIMI FN-19, Aarhus Univ., Computer Science Dept., Denmark, 1981.

[20] John C. Reynolds. The Craft of Programming. Prentice-Hall, Inc., 1981.

[21] John C. Reynolds. The essence of Algol. In Jaco W. de Bakker and van Vliet, editors, Int’l. Symp. Algorithmic Languages, pages 345–372. IFIP, North-Holland, 1981.

[22] John C. Reynolds. Idealized Algol and its specification logic. In D. Néel, editor, Tools and Notions for Program Construction, pages 121–161. Cambridge University Press, 1982.

[23] R. D. Tennent. Semantical analysis of specification logic (preliminary report). In Rohit Parikh, editor, Logics of Programs: Proceedings, volume 193 of Lecture Notes in Computer Science, pages 373–386. Springer-Verlag, 1985.

[24] R. D. Tennent. Semantics of Programming Languages. Prentice Hall, 1991.

[25] Robert Tennent. Semantical analysis of specification logic. Information and Computation, 85(2):135–162, April 1990.

[26] Boris A. Trakhtenbrot, Joseph Y. Halpern, and Albert R. Meyer. From denotational to operational and axiomatic semantics for Algol-like languages: an overview. In Edmund Clarke and Dexter Kozen, editors, Logics of Programs: Workshop, volume 164 of Lecture Notes in Computer Science, pages 474–500. Springer-Verlag, 1984. Conference held in 1983.

[27] Glynn Winskel. Introduction to the formal semantics of programming languages. Unpublished Manuscript, 1991.