From Algol to Polymorphic Linear Lambda-calculus

Peter W. O’Hearn Queen Mary & Westfield College and John C. Reynolds Carnegie Mellon University

In a linearly-typed functional language one can define functions that consume their arguments in the process of computing their results. This is reminiscent of state transformations in imperative languages, where execution of an assignment statement alters the contents of the store. We explore this connection by translating two variations on Algol 60 into a purely functional language with polymorphic linear types. On one hand the translations lead to a semantic analysis of Algol-like programs, in terms of a model of the linear language. On the other hand they demonstrate that a linearly-typed functional language can be at least as expressive as Algol.

Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory—semantics; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages—denotational semantics

General Terms: Languages, Theory

Additional Key Words and Phrases: Parametric polymorphism, logical relations, local state, linear logic

Contents

1 Introduction 2 1.1 Linear Typing and State Transformations . . . . . . . . . . . . . . . 4 1.2 Polymorphism, Data Abstraction and Store Shapes . . . . . . . . . . 6

2 Two Variations on Algol 8 2.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 8

Name: P.W. O’Hearn Address: Department of Computer Science, Queen Mary and Westfield College, London E1 4NS, UK. e-mail: ohearn@dcs.qmw.ac.uk Name: J.C. Reynolds Address: School of Computer Science, Carnegie Mellon University, Pittsburgh PA 15213-3891, USA. e-mail: john.reynolds@cs.cmu.edu

Permission to make digital or hard copies of part or all of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or direct commercial advantage and that copies show this notice on the first page or initial screen of a display along with the full citation. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, to republish, to post on servers, to redistribute to lists, or to use any component of this work in other works, requires prior specific permission and/or a fee. Permissions may be requested from Publications Dept, ACM Inc., 1515 Broadway, New York, NY 10036 USA, fax +1 (212) 869-0481, or permissions@acm.org.

2 · P.W. O’Hearn and J.C. Reynolds

2.2 Basic SCI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 10

3 A Polymorphic Linear λ-calculus 11

4 Translations of Types 14 4.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 4.2 Basic SCI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 15

5 Translations of Terms 16 5.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 17 5.2 Expansions . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 19 5.3 Basic SCI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 20

6 The Strict Parametricity Model 22 6.1 Semantics of Types . . . . . . . . . . . . . . . . . . . . . . . . . . . . 22 6.2 Semantics of Terms . . . . . . . . . . . . . . . . . . . . . . . . . . . . 24

7 Working With the Model 25 7.1 Snapback . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 25 7.2 Sample Type Analyses . . . . . . . . . . . . . . . . . . . . . . . . . . 27 7.3 A Limitation of Binary, Strict Parametricity . . . . . . . . . . . . . . 29

8 Relation to Functor Models 30 8.1 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 8.2 Basic SCI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 34

9 On Naturality and Parametricity 36 9.1 Basic SCI . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 36 9.2 Idealized Algol . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 37 9.3 Technical Lemmas . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38

10 Resumptions and Idealized Algol 40 10.1 A Representation Theorem . . . . . . . . . . . . . . . . . . . . . . . 40 10.2 Proof of the Theorem . . . . . . . . . . . . . . . . . . . . . . . . . . 41 10.3 A Full Abstraction Result . . . . . . . . . . . . . . . . . . . . . . . . 48

11 Related Work 50

12 Discussion 52

1. INTRODUCTION

Traditional denotational semantics models imperative languages using state-to-state functions [Scott and Strachey 1971; Tennent 1991]. This approach successfully accounts for the fact that storage variables take on different values at different times during computation, but it does not cope nearly as well with the idea that a state change destructively alters the contents of the store.

From Algol to Polymorphic Linear Lambda-calculus · 3

To see the difficulty, suppose we use a function p : States → States × Values to model the behaviour of an expression with side effects. Because a state is treated as a value like any other we are free, in the semantics, to manipulate any such function in a decidedly non-imperative manner. For instance, we can define a function

snap : (States → States × Values) → (States → States × Values)

as follows:

snap(p)s = [s, v], where ps = [s′, v].

(Here we are ignoring issues of non-termination.) This snap operator is a perfectly reasonable mathematical function, but if we try to read it in an imperative fashion it contradicts the intuitive understanding of a state transformation as altering the store. Instead, it displays a “snapback” effect; snap(p) proceeds by executing p, producing a new state s′ and value v, and then snapping the state back to its initial value s. The use of p here does not destroy the initial state s.

In this paper we present an approach that better captures the imperative character of state transformations. The approach is based on a combination of linear typing and parametric polymorphism, and is given, formally, via syntactic translations from two variations on Algol 60 into a linear polymorphic λ-calculus. The translations are based on the idea that a program is linearly polymorphic in the type of the state; this allows for a subtle interplay between the copyability of specific values put into the store, and the inability of a program to copy the entire store. We analyze the translations using a model of the target language.

Although our analysis mainly focuses on the resulting semantics of the source languages, the translations can be regarded as well as indicating the imperative nature of the target language. That is, although the linear polymorphic calculus is a purely functional language, the translations can be regarded as providing an imperative reading of a range of types in the functional target.

Before continuing we would like to stress that the “problem” with the traditional semantics should be understood in its historical context. Indeed, Strachey on a number of occasions emphasized the fundamentally different way that the state and environment are used. For example:

“The state transformation produced by obeying a command is essentially irreversible and it is, by the nature of the computers we use, impossible to have more than one version of [the state] available at any one time.”

C. Strachey [1972]

And Scott identified the non-copyability of state as crucial:

“We will be tempted to copy ρ [the environment], but we will never generally feel free to ask for a copy of the whole computer store – there is just no room for that.” D.S. Scott [1972]

But, while Scott and Strachey’s prose vividly distinguished the state from the environment, in 1972 the theoretical techniques were not yet in place to allow for a precise description of the imperative, or irreversible, nature of state change, as expressed informally by them.

In 1975, one of the authors (Reynolds) attempted to use the polymorphic λcalculus [Girard 1972; Reynolds 1974] to describe Algol, discovering much of the translation we will exhibit in Sections 4.1, 5.1, and 5.2. At the time, this seemed to be a quixotic effort to define a well-understood language in terms of a less understood one. (The author overlooked the fact that the translation avoided impredicativity.)

The intervening years, however, have seen the development of a relational semantics of polymorphism [Reynolds 1983]; possible world semantics of imperative languages [Reynolds 1981b; Oles 1982]; a connection between polymorphism and local state [O’Hearn and Tennent 1995]; and linear logic [Girard 1987]. Drawing upon all of these developments, we are now able to give a refined translation of Algol-like languages into the linear polymorphic λ-calculus that, when coupled with a relational semantics for the latter language, gives a more abstract description of Algol that earlier formulations of its semantics.

The translations are essentially a recasting of the the functor-category semantics developed by Reynolds [1981b] and Oles [1982] in the early eighties, using a linear polymorphic λ-calculus in place of a functor category. Their store shapes are replaced by type variables, natural transformations are replaced by polymorphic functions, and state-to-state functions are replaced by linear functions. This use of polymorphism is as in the parametric-functor semantics of O’Hearn and Tennent [1995], but refined by the use of linearity.

In the remainder of this Introduction we give an extended, informal, description of the main elements underlying our approach.

1.1 Linear Typing and State Transformations

The central idea, on which linear logic hinges, is that of a linear function. The guiding intuition is that a linear function “uses” its argument exactly once; as a result, it cannot freely copy or ignore its argument, because doing so would violate the use criterion. One often speaks also of a linear function as “consuming” its argument in the process of producing its result. The connection between use and consumption is that, after a linear function has used its argument once, the argument is no longer available, because to use it again would constitute two uses. The problem with snapback is that it uses the initial state twice, once when producing an intermediate result and again when producing a final answer. Thus, it is not linear in its state argument.

Linear logic is based on Girard’s identification of the structural rules of logic as a source of discarding and copying data [Girard 1987]:

{Γ ⊢ A \atop Γ, B ⊢ A} Weakening  {Γ, B, B ⊢ A \atop Γ, B ⊢ A} Contraction.

Weakening introduces a dummy assumption: In computational terms it may be understood as transforming a computation depending on Γ into a computation depending on Γ and B, but which ignores B. In Girard’s resource description of logical rules, the ignoring of the B component involves the discarding of a datum of type B. Similarly, Contraction involves copying: From a computation depending on two B-typed values a computation depending on only one can be obtained, if we have the ability to duplicate that value and supply the two copies to the original computation.

Linear logic is a refinement of traditional logic which arises by restricting the use of Weakening and Contraction. When the logic is used as a type system for a programming language, this control over structural rules translates into restrictions on the occurrences of identifiers within terms [Abramsky 1993; Wadler 1991; Benton et al. 1993]. These restrictions result in a type A−∘ B of linear functions, which cannot discard or duplicate their arguments through free use of Weakening or Contraction.

To connect these ideas back to imperative computation, let us try to write snap in a programming notation:

snap(p) = λs. let [s′, v] be p s in [s, v].

This term uses both Contraction and Weakening: Contraction corresponds to the two non-binding occurrences of the initial state s in the body of the λ-expression, and Weakening to the absence of s′ in [s, v]. As a result, if we were to use States−∘ States ⊗ Values as the type of side-effecting expressions (where States ⊗ Values is a type of “eager pairs”) then snap(p) would fail to typecheck; snapback is excluded by linear typing.

There is thus a tantalizing analogy between linear functions and imperative state transformations. So it is natural to ask whether, or the extent to which, linear logic can give rise to an improved semantic treatment of state.

As a first test of the analogy, we might translate a basic imperative language, such as the language of while programs, into a linear functional language. It is clear that one could express typical constructs, such as sequencing, assignment and iteration, in terms of linear functions.

This is all well and good, but it only connects up imperative and linear functional programming on a basic level, for an imperative language without procedures. And such a language does not in fact provide a satisfactory test. For, basic sequential imperative languages, without procedures, already possess a satisfactory foundation, with simple semantic models based on partial functions on states and logics based on Hoare triples or weakest preconditions. It is difficult to see how this understanding could be improved by phrasing the semantics in terms of linear types.

How can this be? We began by describing problems in traditional semantics based on state-to-state functions, and the language of while programs uses precisely that kind of semantics. Consider again the snapback example: snap is a function from state transformations to state transformations; in imperative terms it is a procedure that expects an expression thunk as an argument. It takes an arbitrary state transformation, runs it, and then restores the state to its initial value. The whole discussion of snapback and irreversibility hinged on having procedures, which are missing from the language of while programs.

We can go further still if we use local variables: We can then write programs whose observable behaviour is sensitive to whether or not snapback is present in the semantics:

snaptester = λp. new x. x := 0; p(x := x + 1); if x > 0 then diverge.

The termination/nontermination behaviour of snaptester is equivalent to that of λp. p(diverge). The reason is that if p executes its argument at all then the value of x on termination of p(x := x + 1) will be greater than 0, since there is no way for p to alter the value of x other than by using its argument. Snapback contradicts this informal reasoning, since snaptester(snap) converges while snaptester(diverge) diverges.

Thus, it makes sense to consider imperative languages that have procedures and local state, in addition to assignment. In this paper we consider two such languages, based on Idealized Algol [Reynolds 1981b].

1.2 Polymorphism, Data Abstraction and Store Shapes

It is evident how to model state transformations with linear functions, but now we must consider how to model procedures and local state. We might attempt to do so directly in a simply-typed linear language, using −∘ to model state transformations and a conventional function type → to model procedures, but there is a further problem: It is not obvious how we might account for the interaction of procedures and local state (as given, for example, in snaptester).

To expand on this last last point, consider how a “counter class” can be programmed in an Algol-like language using procedures and local state [Reynolds 1978]:

newcounter = λp. new x. x := 0; p(x := x + 1, x).

This code works by declaring a local variable x, and then passing the ability to increment and read x to the procedure p. (The second argument x of p is implicitly dereferenced from a variable to an expression, so that it cannot be assigned to by p.). Because the procedure p can never access the local variable x we are assured, for example, that the value of x can never be decremented. This illustrates how a form of data abstraction results from the combination of procedures and local state; it is hard to see how this phenomenon could be modelled in a simply typed version of linear λ-calculus.

This discussion has been leading toward our choice of target language. We can account for data abstraction and local state using polymorphic types [Reynolds 1974; O’Hearn and Tennent 1995], so our target language will be a linearly-typed, polymorphic λ-calculus.

We can now sketch the main ideas behind the translations. The starting point is to allow for multiple state types instead of only one. In terms of the polymorphic target language we regard type variables as ranging over various “store shapes” or state types, so that in a type α−∘ α of state transformations the type variable α can be instantiated to a variety of different representations of the state. The basic idea is that programs working with different store shapes act on separate parts of the store.

To see how this works recall the counter class above. An argument p to newcounter is a procedure that accepts a command and an expression as arguments, and produces a command as a result. We assign p the polymorphic type

∀β.(β−∘ β)&(β−∘ β ⊗ nat) → (α ⊗ β−∘ α ⊗ β).

The idea is that the state in use when p is called is partitioned into the α-typed part, which p may access directly, and the β-typed part, about which p knows nothing. The argument type β−∘ β corresponds to a command for changing this unknown state, and β−∘ β ⊗ nat to a natural number-valued expression (possibly with side effects).

The type constructors & and → here are for conventional product and function types; they are not subject to linearity restrictions. The mixing of linear and nonlinear type constructors in the type of p implies that it is only the state that must be used linearly; the two arguments, of types β−∘ β and β−∘ β ⊗ nat, may be used zero, one, or many times, as is common in imperative languages.

Now, if we apply the counter class to such a p, i.e., newcounter(p), we obtain a function of type α−∘ α:

\underline{λ}s : α. let [s′, n′] be p[nat]⟨\underline{λ}n. n + 1, \underline{λ}n. [n, n]⟩[s, 0]
in s′.

We can see from this how the β-component in the type of p is regarded as ranging over possible pieces of local state. What a local-variable declaration does first is extend the state s to [s, 0], i.e., a state with an additional component initialized to 0. In this process of initialization the type of the state changes from α to α⊗nat, with nat being the type of the values that can be held by the local variable. Instantiating the β component to nat allows p to work in this enlarged state: Communication between local state and non-local procedures is achieved through polymorphic instantiation. Intuitively, the independence of non-local procedures from local state corresponds to the parametricity of a polymorphic function whose type argument ranges over possible pieces of local state [Reynolds 1983; O’Hearn and Tennent 1995].

This example also illustrates how the move from simple to polymorphic types has an additional effect, beyond enabling a treatment of data abstraction. To see this, consider that we have used Contraction and Weakening of nat-typed identifiers: Contraction is used for dereferencing, in λn. [n, n], and Weakening of n′ is used to model deallocation of the local variable on block exit. (We also sometimes need Weakening to model updates.) These uses of Contraction and Weakening do not contradict the intuitive connection between linearity and state change, because the polymorphic uses of nat by p (obtained by instantiating β) will still all be linear. This point deserves careful consideration, and we will return to it several times, but the general idea is that polymorphic instantiation mediates between the linear way that state is manipulated, and the use of non-linear values to make up specific states.

Local-variable declarations are a special mechanism for ensuring absence of interference through shared variables. We can also use polymorphic typing to treat non-interference more generally. For example, consider the type

∀β ∀γ. (β−∘ β)&(γ−∘ γ ⊗ nat) → (α ⊗ β ⊗ γ−∘ α ⊗ β ⊗ γ).

In imperative terms, a procedure of this type accepts two arguments, one a command and the other a side-effecting expression. If q is such a procedure then in an application q[A][B]⟨c, e⟩ it is never possible to use c to change the state in a way that affects a future use of e. This is because, in q, using c produces a β-typed value, while e expects a γ-typed value, and these types do not match up. So the use of different type variables for the arguments means that the output state of one cannot be used as the input state of the other. Again in imperative terms, we take this to mean that the two arguments c and e don’t interfere.

We now proceed to present the translations, and the semantics. Our two source languages are Idealized Algol [Reynolds 1981b] (without jumps or coercions, and with side effects in expressions) and syntactic control of interference [Reynolds 1978] (without passivity). The target language is based on the −∘, ⊗, &, → (or “!”) fragment of intuitionistic linear logic [Girard 1987; Barber and Plotkin 1997], extended with a fixed-point operator and a predicative form of polymorphism. The semantic model of the target language is based on strict continuous functions and binary relational parametricity [Reynolds 1983]. We analyze the model by looking at sample equivalences, and by characterizing the structure of first-order types in terms of domain equations for resumptions.

In Section 8 we will describe the connection to functor-category semantics in some detail, but for the most part we will work directly with the polymorphic language and its model.

2. TWO VARIATIONS ON ALGOL

Our imperative languages are based on the analysis of Algol 60 given in [Reynolds 1978; Reynolds 1981b]. The one, substantial, caveat is that our languages do not account for passivity. Thus, evaluation of a natural-number expression can produce a side effect, and we do not consider a concept of passive type [Reynolds 1978] (also, [O’Hearn et al. 1999]).

Both languages use the following grammar of types:

φ ::= exp | acc | comm primitive types
θ ::= φ | θ × θ′ | θ → θ′  types

The primitive type exp is the type of natural-number expressions, acc is the type of acceptors, and comm is the type of commands. Commands change the state of the store but do not produce values, and an acceptor changes the state when it is supplied with an integer. The type var of storage variables is an abbreviation for acc × exp. The factors of var give the basic capabilities of updating and accessing a storage variable.

2.1 Idealized Algol

The typing rules for Idealized Algol follow. A typing context Γ is a finite list of assumptions x : θ pairing identifiers with types, with the proviso that no identifier appears twice.

Γ, x : θ ⊢ x : θ  {Γ ⊢ M : θ \atop Γ̃ ⊢ M : θ} where Γ̃ is a permutation of Γ

{Γ, x : θ ⊢ M : θ′ \atop Γ ⊢ λx : θ. M : θ → θ′}  \begin{matrix}Γ ⊢ M : θ → θ′ & Γ ⊢ N : θ \\ Γ ⊢ MN : θ′ \end{matrix}

{Γ ⊢ M : θ_{1} × θ_{2} \atop Γ ⊢ π_{i} M : θ_{i}} where i is 1 or 2  \begin{matrix}Γ ⊢ M : θ & Γ ⊢ N : θ′ \\ Γ ⊢ ⟨M, N⟩ : θ × θ′ \end{matrix}

Γ ⊢ 0 : exp

Γ ⊢ N_{1} : exp Γ ⊢ N_{i} : φ , i = 2, 3
Γ ⊢ if N_{1} = 0 then N_{2} else N_{3} : φ

Γ ⊢ M : exp Γ ⊢ succ M : exp

Γ ⊢ M : exp Γ ⊢ pred M : exp

{Γ ⊢ M : θ → θ \atop Γ ⊢ Y_{θ} M : θ} Γ ⊢ M : var → φ

Γ ⊢ new_{φ} M : φ

Γ ⊢ skip : comm  \begin{matrix}Γ ⊢ M : comm & Γ ⊢ N : φ \\ Γ ⊢ M; N : φ \end{matrix}

Γ ⊢ M : exp → comm Γ ⊢ byvalue M : acc

Γ ⊢ M : acc Γ ⊢ N : exp
Γ ⊢ M := N : comm

Idealized Algol contains the functional constructs of PCF [Plotkin 1977]. Of the imperative constructs, new(λx. C) works by binding x to a local storage variable that is initialized to 0, “;” is sequential composition, skip is the do-nothing command, and assignment supplies an integer value to an acceptor.

Acceptors were originally introduced as part of a generalized approach to variables [Reynolds 1981b], in which an acceptor was considered simply as a function from data values to commands. On this view acceptors are similar to functions of type exp → comm, except that they accept integer values rather than expressionthunks as arguments; they are thus a form of call-by-value procedures. The byvalue construct converts a thunk-expecting procedure to an acceptor using a coercion from natural-number values to expressions. (It would be conceivable to provide instead an alternate binding form for call-by-value, as was done in Algol 60 using the keyword value with a formal parameter.)

We will often use syntactic sugar in an informal, but hopefully clear, way. For instance, newcounter is rendered formally as

λp : (comm × exp → comm) → comm. new_{comm} (λx : var. (π_{1}x) := 0; p⟨(π_{1}x) := (succ π_{2}x), π_{2}x⟩).

Generally, we omit mention of types in new or on λ-bound identifiers, we omit the projections when using a term of type var, and we write new x. M instead of new (λx. M).

An important difference with the original Idealized Algol is that a sequential composition of the form M; N when N : exp may result in an “active expression,” which may return different natural numbers on different uses. For example, if x : var is a declared variable then x := x + 1; x returns successive natural numbers on successive uses.

We have not attempted to produce an irredundant collection of basic constructs. For instance, the expression new_{acc} P of type acc could be eliminated, as it is equivalent to byvalue (λy : exp. new_{comm} z. P z := y).

It is worth considering how the inclusion of side effects in expressions impacts the coding of arithmetic operations. A typical functional encoding of addition is

plus = Y (λ plus. λ x. λy. if x = 0 then y else plus (pred x) (succ y)).

In Idealized Algol (with side effects) an evaluation of plus e_{1} e_{2} will evaluate e_{1} and e_{2} multiple times, perhaps changing the state each time. For example,

new_{exp} z. z := 1; (plus (z := z + 1; z) 2)

diverges since z is incremented each time pred is evaluated.

Using new we can program a version of addition that evaluates its arguments once each, left followed by right, and adds the resulting values together:

leftadd = λx. λy. new x′. new y′. x′ := x; y′ := y; plus (x′) (y′).

We can also define rightadd = λx. λy. leftadd y x.

2.2 Basic SCI

Basic SCI (for syntactic control of interference) is similar to Idealized Algol, but for a few modifications. First, it uses the affine λ-calculus as its type system, whereas Idealized Algol uses the full simply-typed calculus. The affine calculus is just the usual simply-typed calculus, except that the rule for procedure application is restricted so that procedure and argument have no free identifiers in common. (This is another way of saying that the calculus does not have Contraction.) This restriction prevents interference between different identifiers. For instance, y and z are aliases in ((λyλz. · · · y := a ⋯ z := b ⋯)x)x if x denotes a storage variable. But a term of this form cannot typecheck in Basic SCI because there is an occurrence of x in a procedure and its argument.

Second, the rule for recursion is restricted to procedures with no free identifiers. This restriction is needed because otherwise a recursive unwinding Y(F) ⊳ F (Y(F)) would violate the disjointness between procedure and argument that is characteristic of Basic SCI.

Third, in Basic SCI we have a determinate form of parallelism, where the parallel composition M ∥ N is allowed if the free identifiers of M and N are disjoint. This illustrates the difference with Idealized Algol, where the same construct would (because of interference) lead to indeterminacy.

These modifications and additions to Idealized Algol are summed up in the following rules:

\begin{matrix}Γ ⊢ M : θ → θ′ & Γ′ ⊢ N : θ \\ Γ, Γ′ ⊢ MN : θ′ \end{matrix} Γ ⊢ M : comm Γ′ ⊢ N : comm

Γ, Γ′ ⊢ M ∥ N : comm

{⊢ M : θ → θ \atop ⊢ Y_{θ} M : θ}

To illustrate further the difference between SCI and Idealized Algol consider the addition operations leftadd, rightadd : exp → exp → exp. In Idealized Algol these operations are inequivalent because of interfering side-effects. For example, in a state where the contents of storage variable x is 5, evaluation of leftadd(succ x)(x := succ x; x) returns value 12, whereas rightadd(succ x)(x := succ x; x) returns value 13. In contrast, in SCI the arguments to these functions never interfere: The typing rules ensure that in a procedure call leftadd(e_{1})(e_{2}) the procedure leftadd(e_{1}) and argument e_{2} have disjoint sets of free identifiers. As a result, even though we allow side effects in expressions, leftadd and rightadd are equivalent in SCI.

An interfering version of addition can be programmed in SCI using the type exp × exp → exp instead of exp → exp → exp. The point is that SCI types can be used to specify both potential dependence and necessary independence between program parts.

3. A POLYMORPHIC LINEAR λ-CALCULUS

Now we introduce the polymorphic target language. We follow the version of linear type theory formulated by Barber and Plotkin [1997], where two zones are used in a typing context to keep track of intuitionistic and linear assumptions. The basic idea is that linear assumptions are used once, while intuitionistic assumptions can be used multiple times in a term. (We refer to [Abramsky 1993; Benton et al. 1993; Wadler 1990; Wadler 1991] for further discussions of linear λ-calculi.)

The kind of polymorphism we need for interpreting Algol is predicative in nature, so we work with the following stratification of types:

σ ::= α | nat | σ ⊗ σ | I  Level 1
A ::= σ | ∀α. A | A−∘ A | A → A | A &A |!A Level 2

Type variables are denoted by α (or other Greek letters β, γ). The essence of the stratification is that the ∀ quantifier ranges over only Level 1 types. This is significant because it makes the construction of models much easier than for impredicative calculi.

This stratification is possible because of the distinction between data types and phrase types (or between storable and denotable values) in Algol. The Level 1 types correspond, intuitively, to store shapes in the sense of Reynolds and Oles, whereas Level 2 types are, after translation, types of phrases in the imperative languages.

It would be possible to define A → B as !A−∘ B. But since, for the purpose of the two translations, the only significant uses of “!” would be in this encoding we prefer to work explicitly with both function types −∘ and →. For emphasis we use two binding forms, \underline{λ}x : A. t and λx : A. t, one for each function type. We will use the same syntax for applying both kinds of function (in effect leaving dereliction implicit in →); no confusion is likely to arise from this.

The system uses typing judgements of the form

Γ; Δ ⊢ t : A,

where the context is broken into an intuitionistic zone Γ and a linear zone Δ.

12 · P.W. O’Hearn and J.C. Reynolds

Identity

{Γ; Δ ⊢ t : A \atop Γ̃; Δ̃ ⊢ t : A} where Γ̃, Δ̃ are permutations of Γ, Δ
Γ, x : A; ⊢ x : A  Γ; x : A ⊢ x : A

Additives

\begin{matrix}Γ; Δ ⊢ t : A & Γ; Δ ⊢ u : B \\ Γ; Δ ⊢ ⟨t, u⟩ : A &B \end{matrix}

{Γ; Δ ⊢ t : A &B \atop Γ; Δ ⊢ π_{1} t : A}  {Γ; Δ ⊢ t : A &B \atop Γ; Δ ⊢ π_{2} t : B}
{Γ, x : A; Δ ⊢ t : B \atop Γ; Δ ⊢ λx : A. t : A → B} \begin{matrix}Γ; Δ ⊢ t : A → B & Γ; ⊢ u : A \\ Γ; Δ ⊢ t u : B \end{matrix}

Multiplicatives

Γ; ⊢ ∗ : I

Γ; Δ_{1} ⊢ t : I Γ; Δ_{2} ⊢ u : A
Γ; Δ_{1}, Δ_{2} ⊢ let ∗ be t in u : A
Γ; Δ_{1} ⊢ u : A ⊗ B Γ; Δ_{2}, x : A, y : B ⊢ t : C

Γ; Δ_{1}, Δ_{2} ⊢ let [x, y] be u in t : C

\begin{matrix}Γ; Δ_{1} ⊢ t : A & Γ; Δ_{2} ⊢ u : B \\ Γ; Δ_{1}, Δ_{2} ⊢ [t, u] : A ⊗ B \end{matrix}

{Γ; Δ, x : A ⊢ t : B \atop Γ; Δ ⊢ \underline{λ}x : A. t : A−∘ B} \begin{matrix}Γ; Δ_{1} ⊢ t : A−∘ B & Γ; Δ_{2} ⊢ u : A \\ Γ; Δ_{1}, Δ_{2} ⊢ t u : B \end{matrix}

{Γ; ⊢ t : A \atop Γ; ⊢!t : !A} Γ; Δ_{1} ⊢ u : !A Γ, x : A; Δ_{2} ⊢ t : B

Γ; Δ_{1}, Δ_{2} ⊢ let !x be u in t : B

Polymorphism

{Γ; Δ ⊢ t : ∀α.A \atop Γ; Δ ⊢ t[σ] : A[σ/α]} {Γ; Δ ⊢ t : A \atop Γ; Δ ⊢ Λα.t : ∀α.A} α ^{∉} fv(Γ, Δ)

Natural Numbers and Recursion

Γ; ⊢ 0 : nat  {Γ; ⊢ t : A → A \atop Γ; ⊢ Y_{A} t : A}

Γ; Δ ⊢ t : nat Γ; Δ ⊢ succ t : nat

Γ; Δ ⊢ t : nat Γ; Δ ⊢ pred t : nat

Γ; Δ ⊢ t : nat

Γ; Δ ⊢ copy t : nat ⊗ nat

Γ; Δ ⊢ t : nat Γ; Δ ⊢ discard t : I

Γ; Δ_{1} ⊢ u_{1} : nat Γ; Δ_{2} ⊢ u_{2} : A Γ; Δ_{2} ⊢ u_{3} : A
Γ; Δ_{1}, Δ_{2} ⊢ if u_{1} = 0 then u_{2} else u_{3} : A

In this formulation of linear typing we have introduction and elimination rules for each type constructor. However, we do not have to add explicit rules that permit Weakening and Contraction of “!”-typed identifiers; this is because of the use of two zones, which allows Weakening and Contraction in the intuitionistic zone to be left implicit, as is the case in simply-typed λ-calculus. This allows for a particularly smooth treatment of the intuitionistic function type →, which is attractive for our purposes: We will have need for →, but not explicitly for “!.”

The characteristic feature of the additive rules is the sharing of typing contexts. For instance, in the introduction rule for &, the linear zone Δ is shared between both premises. On the other hand, the characteristic feature of the multiplicatives is the splitting of typing contexts in the linear zone. For instance, in the introduction rule for ⊗, the contexts Δ_{1} and Δ_{2} must be made up of disjoint collections of identifiers. The absence of Contraction is reflected in this splitting of contexts in the multiplicative rules, and the absence of Weakening is reflected in the rules for identifiers; the linear zone is empty when an identifier from the intuitionistic zone is typed, and of length one when a linear identifier is typed.

One point to notice is the presence of explicit terms for copying and discarding natural numbers. Using these and the rules for I we can define appropriate copying and discarding terms of types σ−∘ σ ⊗ σ and σ−∘ I, for any closed Level 1 type σ. But we do not have copying or discarding of Level 1 types available generically, as terms of type ∀α. α−∘ α ⊗ α or ∀α. α−∘ I. This distinction between specific and generic copying/discarding is related to the following idea in Idealized Algol: A state change effected by a command on any fixed finite number of storage variables could be reversed by using local variables to store and restore the values. But we cannot program a general snapback mechanism that reverses state changes for every possible shape of the store.

We have used [s, t] as notation for ⊗-pairs, reserving f ⊗ g for the functorial action of ⊗, where

f ⊗ g = λx : A ⊗ B. let [y, z] be x in [fy, gz],

when f : A−∘ A′ and g : B−∘ B′.

We use Ω_{A} to abbreviate Y_{A}(λx : A.x). In a fully polymorphic language Y would have type ∀α. (α → α) → α, but in the predicative sublanguage this type is not sufficient because α does not range over all types.

4. TRANSLATIONS OF TYPES

In this section we give the translations on the level of types. We consider terms by treating a few examples, leaving the detailed translation to the next section. In presenting examples we will be somewhat liberal in the use of syntactic sugar and the application of (meaning-preserving) syntactic simplifications in the linear calculus.

4.1 Idealized Algol

The translation takes a judgement

x_{1} : θ_{1}, …, x_{n} : θ_{n} ⊢ M : θ

in Idealized Algol to a judgement

x_{1} : θ_{1}^{⋆}α, …, x_{n} : θ_{n}^{⋆}α; ⊢ M^{⋆}α : θ^{⋆}α

in polymorphic linear λ-calculus, where

comm^{⋆}α = α−∘ α
acc^{⋆}α = α ⊗ nat−∘ α
exp^{⋆}α = α−∘ α ⊗ nat
(θ × θ′)^{⋆}α = θ^{⋆}α & θ^{′⋆}α
(θ → θ′)^{⋆}α = ∀β. θ^{⋆}(α ⊗ β) → θ′^{⋆}(α ⊗ β).

The translation θ^{⋆} of an Idealized Algol type is a type with a “hole” that can be filled by substituting type variables and other Level 1 types. For instance, comm^{⋆}(α ⊗ β) is α ⊗ β−∘ α ⊗ β. Similarly, a term M gets mapped to a term M^{⋆} with a type variable hole that can be filled with various type variables or Level 1 types: M^{∗}σ, M^{∗}σ′... and so on. (The translation could be arranged so that each M^{⋆} was a polymorphic function of type ∀α. θ_{1}^{⋆}α & ⋯ & θ_{n}^{⋆}α → θ^{⋆}α. We prefer, however, to use the term-with-hole representation in order to minimize explicit manipulations of environments.)

The only essential uses of linearity involve primitive types and states. In particular, the translations of Algol types always appear in the intuitionistic zone of a typing judgement.

In the informal translation of newcounter in the Introduction we used Weakening and Contraction of nat-typed identifiers. With our linear language, however, we have to be more explicit, using copy and discard. Also, a slight adjustment is needed because the translation of procedure types in Idealized Algol allows α to appear to the left of →, whereas the type for the procedure p in the Introduction used the SCI interpretation (see below) where α does not appear to the left. So p now has type

∀β. (α ⊗ β−∘ α ⊗ β) × (α ⊗ β−∘ α ⊗ β ⊗ nat) → (α ⊗ β−∘ α ⊗ β),

and the translation of newcounter(p) is the following function of type α−∘ α:

\underline{λ}s : α. let [s′, n′] be p[nat]⟨(id_{α} ⊗ \underline{λ}n. succ n), (id_{α} ⊗ \underline{λ}n. copy n)⟩[s, 0]

in (let ∗ be (discard n′) in s′),

where id_{α} is \underline{λ}s : α. s.

Some equivalences between Idealized Algol terms can be proven using basic laws of polymorphic λ-calculus. For example, the equivalence (new λ x. c) ≡ c, for an identifier c : comm, follows from basic equivalences of polymorphic λ-calculus together with the assumption that discard and copy give nat a comonoid structure. Typically, the basic equations that are valid in models where ∀ is interpreted simply as an indexed product are sufficient for reasoning about new blocks whose only free identifiers are of primitive type, but parametricity is needed when there are free identifiers of procedural type.

In the Introduction we discussed snapback in the context of a single collection States of states. In the polymorphic language snapback would ostensibly be given by a term

Λα. \underline{λ}s : α. let [s′, n] be c s in [s, n]

of type ∀α. (α−∘ α⊗nat) → (α−∘ α⊗nat) which (given the isomorphism α ≅ I ⊗α) would determine a closed term of type (exp → exp)^{⋆}I. But this term does not have the indicated type because it uses Contraction of s and Weakening of s′, where s and s′ are α-typed values. This does not show that no other term produces the behaviour of snapback – for that we will appeal to a semantic model – but it illustrates that it is the general, or polymorphic, snapback that we expect control of structural rules to forbid.

4.2 Basic SCI

We translate

x_{1} : θ_{1}, …, x_{n} : θ_{n} ⊢ M : θ

in Basic SCI to a judgement

x_{1} : θ_{1}^{∘}α_{1}, …, x_{n} : θ_{n}^{∘}α_{n}; ⊢ M^{∘}(α_{1}, …, α_{n}) : θ^{∘}(α_{1} ⊗ ⋯ ⊗ α_{n})

in polymorphic linear λ-calculus, where

comm^{∘}α = α−∘ α
acc^{∘}α = α ⊗ nat−∘ α
exp^{∘}α = α−∘ α ⊗ nat
(θ × θ′)^{∘}α = θ^{∘}α & θ^{′∘}α
(θ → θ′)^{∘}α = ∀β. θ^{∘}β → θ′^{∘}(α ⊗ β).

Compared to the other translation, each identifier x_{i} is now associated with a separate state-type α_{i}; the idea is that each identifier has a separate piece of the store that it acts upon. The other difference is that the procedure type uses θ^{∘}β in the argument position instead of θ^{∘}(α ⊗ β). The result is that the procedure and argument types no longer share type variable α, mirroring the restricted rule for application in SCI which ensures that procedures and their arguments don’t interfere.

For example, the type comm → exp → comm translates as

∀β. (β−∘ β) → (∀γ. (γ−∘ γ ⊗ nat) → (α ⊗ β ⊗ γ−∘ α ⊗ β ⊗ γ)),

which is isomorphic to the type

∀β ∀γ. (β−∘ β) & (γ−∘ γ ⊗ nat) → (α ⊗ β ⊗ γ−∘ α ⊗ β ⊗ γ)

that we used to illustrate non-interference in the Introduction.

Note that the absence of Contraction in linear logic is not being used to account for the absence of Contraction in SCI. Indeed, the translations of SCI types always appear in the intuitionistic zone in the translation of a judgement. It is the use of different type variables that corresponds to the absence of Contraction in SCI: Different occurrences of the same SCI type θ, say x_{1} : θ, x_{2} : θ, get sent to different types, x_{1} : θ^{∘}α_{1}, x_{2} : θ^{∘}α_{2}. Generally, parametric polymorphism is used to model both local state and non-interference, whereas linearity (combined with polymorphism) ensures that there is no snapback.

We give several examples of term translations. First, if x_{1} and x_{2} are different identifiers of type comm, then the translation of x_{1} ∥ x_{2} is

x_{1} : α_{1}−∘ α_{1}, x_{2} : α_{2}−∘ α_{2};
⊢ \underline{λ} s : α_{1} ⊗ α_{2}. let [s_{1}, s_{2}] be s in [x_{1}s_{1}, x_{2}s_{2}] : α_{1} ⊗ α_{2}−∘ α_{1} ⊗ α_{2}.

From this we can see how the disjointness property of SCI is very explicit: It is obvious that x and y act on disjoint portions of the store, so we can run them in parallel.

Consider next the sequential composition x; y of two command identifiers. This is translated as

x_{1} : α_{1}−∘ α_{1}, x_{2} : α_{2}−∘ α_{2};
⊢ \underline{λ} s : α_{1} ⊗ α_{2}. x′_{2}(x′_{1}(s)) : α_{1} ⊗ α_{2}−∘ α_{1} ⊗ α_{2},

where

x′_{1} = λs : α_{1} ⊗ α_{2}. let [s_{1}, s_{2}] be s in [x_{1}s_{1}, s_{2}]
x′_{2} = λs : α_{1} ⊗ α_{2}. let [s_{1}, s_{2}] be s in [s_{1}, y_{2}s_{2}].

Although the translation uses x′_{2}(x′_{1}(s)), which indicates that x_{1} is evaluated first, it reduces to let [s_{1}, s_{2}] be s in [x_{1}s_{1}, x_{2}s_{2}] using typical reductions of linear λcalculus. Thus, it is clear that x_{1}; x_{2} and x_{1} ∥ x_{2} are equivalent.

Finally, consider our two addition operations leftadd and rightadd. The translations of leftadd(x_{1})(x_{2}) and rightadd(x_{1})(x_{2}) are both

x_{1} : α_{1}−∘ α_{1} ⊗ nat, x_{2} : α_{2}−∘ α_{2} ⊗ nat;
⊢ \underline{λ} s : α_{1} ⊗ α_{2}. let [s_{1}, s_{2}] be s in
let[[s′_{1}, n], [s′_{2}, m]] be [x_{1}s_{1}, x_{2}s_{2}] in [[s′_{1}, s′_{2}], m + n]
: α_{1} ⊗ α_{2}−∘ α_{1} ⊗ α_{2} ⊗ nat.

We regard the two arguments as being evaluated in parallel, possibly altering different portions of the store, before their results are added together. (The translations do not literally result in this term, but in ones that are, by an easy analysis using the semantic model of Section 6, seen to be equivalent to it.)

5. TRANSLATIONS OF TERMS

The detailed translations of terms follow ideas from functor-category semantics [Oles 1982].

5.1 Idealized Algol

We begin by translating assignment. An assignment statement M := N is executed by first evaluating N, obtaining a changed state and value, and then supplying this value and state to M. Thus, assignment is simply a composition of the form

[figure: α; α ⊗ nat; α.; N^{⋆}α; M^{⋆}α]

More explicitly, we may define

(M := N)^{⋆}α = \underline{λ}s : α. let [s′, m] = (N^{⋆}α s) in (M^{⋆}α [s′, m]).

To translate new_{comm} we follow the pattern of the newcounter example in the Introduction:

(new_{comm} P)^{⋆}α = \underline{λ}s : α. let [s′, n] be (P^{⋆}α)[nat] (v[α]) [s, 0] in

let ∗ be (discard n) in s′.

In this equation the expanded state [s, 0] and a local variable v[α] (defined below) are passed as arguments to the procedure P, and the final value n of the local variable is discarded on termination of P. The translation P^{⋆}α of P has type ∀β. var^{⋆}(α ⊗ β) → comm^{⋆}(α ⊗ β), and polymorphic instantiation is used to set the β-component to nat.

The local variable v is given by the term Λα. ⟨assign[α], lookup[α]⟩ of type ∀α. (acc × exp)^{⋆}(α ⊗ nat), where

assign = Λα. \underline{λ}s : (α ⊗ nat)⊗ nat. let [[a, n], m] be s in let ∗ be (discard n) in [a, m]

lookup = Λα. \underline{λ} s : α ⊗ nat. let [a, n] be s in let [n′, n′′] be (copy n) in [[a, n′], n′′].

The essence of these two operations is the use of discard in assign and copy in lookup. Similar assignment and lookup operations are therefore available if we replace nat by any type that has appropriate versions of copy and discard maps. Since all types of the form !A have copy and discard maps, if we were to consider an impredicative polymorphic calculus we could write lookup and assign maps for “storing” elements of any such type. An interesting question is whether such operations make (imperative) operational sense.

The translation of new_{exp} is similar:

(new_{exp} P)^{⋆}α = \underline{λ}s : α. let [[s′, n], m] be (P^{⋆}α)[nat] (v[α]) [s, 0] in

let ∗ be (discard n) in [s′, m].

If we had interpreted comm as α−∘ α ⊗ I then the two new constructs could have been treated uniformly, by the same defining equation. The translation of new_{acc} P is obtained by viewing it as sugar for byvalue (λy : exp. new_{comm} z. P z := y).

To translate an application (M N)^{⋆}, where M : θ → θ′ and N : θ, we must use translations of M and N with the following types:

M^{⋆}α : ∀β. θ^{⋆}(α ⊗ β) → θ^{′⋆}(α ⊗ β)
N^{⋆}α : θ^{⋆}α.

In order to apply M^{⋆} to N^{⋆}, we apply M^{⋆}α to the unit I of ⊗, and then use a canonical isomorphism α⊗I ≅ α to make the types of the procedure and argument match up. That is,

(MN)^{⋆}α = h((M^{⋆}α)[I](i(N^{⋆}α))),

where h : θ^{′⋆}(α ⊗ I)−∘ θ^{′⋆}α and i : θ^{⋆}α−∘ θ^{⋆}(α ⊗ I) are terms coding canonical isomorphisms.

We will not give the explicit definitions of h and i, but simply say that they are defined in a standard way by induction on types. If T (α) is a type of the polymorphic calculus with a free type variable α, and f : α−∘ β and g : β−∘ α are terms (β ^{∉} fv(T)), then there is an induced term T [f, g] : T (α)−∘ T (β) obtained by applying f for positive occurrences of α and g for negative occurrences. Further, T [f, g] is an isomorphism (say, in the model of the following section) whenever f and g denote inverse isomorphisms.

This use of canonical isomorphisms is unpleasant, and is treated much more smoothly in a semantics based explicitly on a functor category.

The next case we consider is λ-abstraction. We need to define

(λx : θ. M)^{⋆}α : ∀β. θ^{⋆}(α ⊗ β) → θ^{′⋆}(α ⊗ β)

in terms of

M^{⋆}α : θ′α, assuming x : θ^{⋆}α.

The type mismatch between θ^{⋆}α and θ^{⋆}(α ⊗ β) is dealt with now by using “expansion” mappings expand_{θ} : ∀αβ. θ^{⋆}α−∘ θ^{⋆}(α ⊗ β). Expansions show how a piece of code defined outside the scope of a local-variable declaration can be used within the scope of the declaration. For instance, a command identifier c : comm^{∗}α gets sent to \underline{λ}[s, s′] : α ⊗ β. [c(s), s′].

A detailed description of expand is postponed until later in this section, but the way expansions are used to treat λ-abstraction can be set out now. Suppose we are given

x_{1} : θ_{1}^{⋆} : α, …, x_{n} : θ_{n}^{⋆}α, x : θ^{⋆}α; ⊢ M^{⋆}α : θ′α.

Then we also have

x_{1} : θ_{1}^{⋆}(α ⊗ β), …, x_{n} : θ_{n}^{⋆}(α ⊗ β),x : θ^{⋆}(α ⊗ β) ;
⊢ M^{⋆}(α ⊗ β) : θ′(α ⊗ β),

and using a typical substitution lemma for the linear calculus we can infer

x_{1} : θ_{1}^{⋆} : α, …, x_{n} : θ_{n}^{⋆}α,x : θ^{⋆}(α ⊗ β) ;
⊢ (M^{⋆}(α ⊗ β))[expand_{θ_{i}}[α][β]x_{i}/x_{i}] : θ′(α ⊗ β),

where (M^{⋆}(α ⊗ β))[expand_{θ_{i}}[α][β]x_{i}/x_{i}] denotes the term obtained by substituting expand_{θ_{i}}[α][β]x_{i} for each x_{i}. Notice that x is not replaced. Given this judgement we can first λ-abstract x and then Λ-abstract β, leading to the definition

(λx : θ. M)^{⋆}α = Λβ λx : θ^{⋆}(α ⊗ β). (M^{⋆}(α ⊗ β))[expand_{θ_{i}}[α][β]x_{i}/x_{i}].

Note that the use of expansions makes the translation M^{⋆} dependent on the types of free identifiers; e.g. λx : comm. y(z) gets translated differently, depending on the types of y and z. So to be precise the translation in fact defines terms M_{Γ}^{⋆}α, indexed by Idealized Algol type assignments Γ.

The remaining clauses are straightforward by comparison. A canonical isomorphism h : θ^{⋆}(α ⊗ I)−∘ θ^{⋆}(α) is used to deal with the function application in the translation of the fixed-point combinator.

x^{⋆}α = x
(π_{i}M)^{⋆}α = π_{i}(M^{⋆}α)
⟨M, N⟩^{⋆}α = ⟨M^{⋆}α, N^{⋆}α⟩
0^{⋆}α = \underline{λ}s : α. [s, 0]
(if N_{1} = 0 then N_{2} = \underline{λ}s : α. let [s′, y] be N_{1}^{⋆} s in
else N_{3})^{⋆}α  if y = 0 then N_{2}^{⋆}α s′ else N_{3}^{⋆}α s′
(succ M)^{⋆}α = \underline{λ}s : α. let [s′, y] be M^{⋆}α s in [s′, (succ y)]
(pred M)^{⋆}α = \underline{λ}s : α. let [s′, y] be M^{⋆}α s in [s′, (pred y)]
(Y_{θ} M)^{⋆}α = h(Y_{θ^{⋆}(α⊗I)}M^{⋆}α[I])
(byvalue M)^{⋆}α = \underline{λ}[s, n] : α ⊗ nat.

let [s′, x] = (M^{⋆}α[I](\underline{λ}a : α ⊗ I. [a, n])[s, ∗]) in

let ∗ be x in s′
(M; N)^{⋆}α = \underline{λ}s : α. N^{⋆}α (M^{⋆}α s)
skip^{⋆}α = \underline{λ}s : α. s

The clause for M; N is for the cases when N : exp or N : comm. The case of M; N when N : acc is treated by the translation as sugar for the expression (byvalue λx : exp. M; (N := x)). Similarly, the clause for if is when N_{2}, N_{3} : comm or N_{2}, N_{3} : exp , and the acceptor case is sugar for the expression (byvalue λx : exp. if N_{1} = 0 then N_{1} := x else N_{2} := x).

5.2 Expansions

We define functions

expand_{θ} : ∀α∀β. θ^{⋆}α−∘ θ^{⋆}(α ⊗ β),

where α and β are different type variables. These functions will be given by closed terms. In the present setup, the Expansion Parametricity Lemma of [O’Hearn and Tennent 1995] is then a consequence of the definability of these expansions and the Logical Relations Lemma. The definition goes by induction on θ:

expand_{comm} = Λαβ. \underline{λ}c : α−∘ α. \underline{λ}[a, b] : α ⊗ β. [c a, b]
expand_{acc} = Λαβ. \underline{λ}c : α ⊗ nat−∘ α. \underline{λ}[[a, b], n] : (α ⊗ β) ⊗ nat. [c[a, n], b]
expand_{exp} = Λαβ. \underline{λ}e : α−∘ α ⊗ nat. \underline{λ}[a, b] : α ⊗ β. let [a′, n] = e a
in [[a′, b], n]
expand_{θ×θ′} = Λαβ. (expand_{θ}[α, β])&(expand_{θ′}[α, β])
expand_{θ→θ′} = Λαβ. \underline{λ}p. Λγ. i1 ∘ p[β ⊗ γ] ∘ i2

Here we have used the shorthand of composition ∘ (in functional order) and the functorial action of &. The terms i1 and i2 are for associativity isomorphisms:

i1 : θ′((α ⊗ β) ⊗ γ)−∘ θ′(α ⊗ (β ⊗ γ))
i2 : θ((α ⊗ β) ⊗ γ)−∘ θ(α ⊗ (β ⊗ γ)).

Thus, expansions for function types are defined according to the following diagram:

[figure: θ^{⋆}((α ⊗ β) ⊗ γ); θ^{⋆}(α ⊗ (β ⊗ γ)); θ^{′⋆}((α ⊗ β) ⊗ γ); θ^{′⋆}(α ⊗ (β ⊗ γ)); i2; p[β ⊗ γ]; expand_{θ→θ′}[α][β]p[γ]; i1]

5.3 Basic SCI

In the translation for Basic SCI we will gloss over isomorphisms for permuting and associating ⊗. The translation is similar in many ways to the one for Idealized Algol: We concentrate on the main differences.

First, to translate identifiers, given

x_{1} : θ_{1}, …, x_{m} : θ_{m} ⊢ x_{i} : θ_{i}

in SCI we must define

x_{1} : θ_{1}^{∘}α_{1}, …, x_{m} : θ_{m}^{∘}α_{m}; ⊢ x_{i}^{∘}(α_{1}, …, α_{m}) : θ_{i}^{∘}(α_{1} ⊗ ⋯ ⊗ α_{m}).

We define x_{i}^{∘}(α_{1}, …, α_{m}) = e(x_{i}), where e : θ_{i}^{∘}α_{i}−∘ θ_{i}^{∘}(α_{1} ⊗ ⋯ ⊗ α_{m}) is obtained by composing an expansion with appropriate symmetry isomorphisms.

For λ-abstraction, given

x_{1} : θ_{1}^{∘}α_{1}, …, x_{m} : θ_{m}^{∘}α_{m}, y : θ^{∘}β;
⊢ M^{∘}(α_{1}, …, α_{m}, β) : θ^{′∘}(α_{1} ⊗ ⋯ ⊗ α_{m} ⊗ β)

we can form the judgement

x_{1} : θ_{1}^{∘}α_{1}, …, x_{m} : θ_{m}^{∘}α_{m};
⊢ Λβ. λy : θ^{∘}β. M^{∘}(α_{1}, …, α_{m}, β). : ∀β. θβ → θ′(α_{1} ⊗ ⋯ ⊗ α_{m} ⊗ β).

We take this as the interpretation of λ-abstraction in SCI; it is remarkably simple compared to the translation for Idealized Algol.

The SCI rule for application is of the form

\begin{matrix}x_{1} : θ_{1}, …, x_{n} : θ_{n} ⊢ M : θ → θ′ & x_{n+1} : θ_{1}, …, x_{m} : θ_{m} ⊢ N : θ \\ x_{1} : θ_{1}, …, x_{m} : θ_{m} ⊢ MN : θ′ \end{matrix} ,

and we define (MN)^{∘}(α_{1}, …, α_{m}) to be

(M^{∘}(α_{1}, …, α_{n})[α_{n+1} ⊗ ⋯ ⊗ α_{m}])(N^{∘}(α_{n+1}, …, α_{m})).

In this definition the β-component of

M^{∘}(α_{1}, …, α_{n}) : ∀β. θ^{∘}β → θ^{′∘}(α_{1} ⊗ ⋯ ⊗ α_{n} ⊗ β)

is instantiated to the type α_{n+1} ⊗ ⋯ ⊗ α_{m} of the state for N.

For parallel composition, given

x_{1} : θ_{1}, …, x_{n} : θ_{n} ⊢ M : comm x_{n+1} : θ_{1}, …, x_{m} : θ_{m} ⊢ N : comm
x_{1} : θ_{1}, …, x_{m} : θ_{m} ⊢ M ∥ N : comm

,

we translate as follows:

(M ∥ N)^{∘}(α_{1}, …, α_{m}) = λs : α let [z_{1}, …, z_{m}] be s in
[M^{∘}(α_{1}, …, α_{n})[z_{1}, …, z_{n}],
N^{∘}(α_{n+1}, …, α_{m})[z_{n+1}, …, z_{m}]].

This interpretation splits the state into components z_{1}, …, z_{n} and z_{n+1}, …, z_{m} that are acted upon independently by M and N.

The equations for new_{comm} and new_{exp} are as in Idealized Algol, except that the variable v[α] is replaced by v : (acc × exp)^{∘}(nat), given by ⟨assign, lookup⟩, where

assign = \underline{λ}[n, m] : nat ⊗ nat. let ∗ be (discard n) in m
lookup = \underline{λ} n : nat. copy n.

There is no longer a need for the α component of v because procedures and arguments don’t interfere in Basic SCI.

Finally, expansions for procedure types are defined as follows:

expand_{θ→θ′} = Λαβ. \underline{λ}p. Λγ. i ∘ expand_{θ′}[α ⊗ γ][β] ∘ p[γ],

where i is an isomorphism as indicated in the following diagram

[figure: θ^{∘}(γ); θ^{′∘}(α ⊗ γ); θ^{′∘}((α ⊗ β) ⊗ γ); θ^{′∘}((α ⊗ γ) ⊗ β)); p[γ]; expand_{θ′}[α ⊗ γ][β]; expand_{θ→θ′}[α][β]p[γ]; i]

Expansions for the primitive types are the same as in Idealized Algol.

There is another candidate definition for expansions at procedure types, based on the following diagram.

[figure: θ^{∘}(γ); θ^{∘}(β ⊗ γ); θ^{′∘}((α ⊗ β) ⊗ γ); θ^{′∘}(α ⊗ (β ⊗ γ)); expand_{θ}[γ][β]; p[β ⊗ γ]; expand_{θ→θ′}[α][β]p[γ]; i]

The equivalence of these two definitions depends on a naturality property for p, which we will be able to verify later (Theorem 11) using a semantic model of the linear calculus.

6. THE STRICT PARAMETRICITY MODEL

Having defined the translations we now want to analyze them in more detail. The approach we take is to look at a simple semantic model of the target language, and push it as far as possible. This will allow us (in Section 7) to very quickly go beyond previous functor models [Oles 1982; O’Hearn and Tennent 1995]. Another possibility for analysis would have been to directly relate contextual equivalence relations for the source and target languages: A syntactic study along these lines would be interesting, but is outside the scope of the present paper. Additionally, the semantic model contains useful information beyond contextual equivalence, which can be viewed as providing relational reasoning principles, and which leads to representation results.

The model is based on strict continuous functions and relational parametricity; we call it simply the strict parametricity model. It actually supports Contraction, though it does not support Weakening. Such a simple model is useful for our purpose, it seems, because problematic examples like snapback in imperative languages typically use both Weakening and Contraction. Removing just one of Weakening or Contraction banishes many of these examples.

6.1 Semantics of Types

In the strict parametricity model, types are interpreted as cpo’s, i.e., directedcomplete partial orders possessing a least element [Plotkin 1983; Abramsky and Jung 1994]. Level 1 types will always denote countable, flat cpo’s, where there is a discretely-ordered set of elements arranged just above a least element ⊥.

More specifically, a type A determines a function [[A]] from type environments to cpo’s, where a type environment D maps type variables to countable, flat cpo’s. Most type constructors are interpreted directly by their cpo counterparts:

\begin{aligned}[[α]]_{D} & = & Dα \\ [[I]]_{D} & = & I \\ [[nat]]_{D} & = & N_{⊥} \\ [[σ ⊗ σ′]]_{D} & = & [[σ]]_{D} ⊗ [[σ′]]_{D} \\ [[A &B]]_{D} & = & [[A]]_{D} &[[A]]_{D} \\ [[A → B]]_{D} & = & [[A]]_{D} → [[B]]_{D} \\ [[A−∘ B]]_{D} & = & [[A]]_{D}−∘ [[B]]_{D} \\ [[!A]]_{D} & = & ([[A]]_{D})_{⊥}. \end{aligned}

On the right-hand side I is the two-point cpo, (·)_{⊥} is lifting, ⊗ is smash product, & is cartesian product, −∘ is strict continuous function space (pointwise ordered), and → is continuous function space.

To define ∀ we make use of an auxiliary relational semantics [Reynolds 1983]. Suppose R (a relation environment) is a function mapping each type variable into a pointed (i.e., ⟨⊥, ⊥⟩-containing) binary relation between flat cpo’s, such that

R(α) : Dα ↔ D′α, all α

for type environments D, D′. Then we define a complete relation

[[A]]_{R} : [[A]]_{D} ↔ [[A]]_{D′}

as follows. (Completeness means that the relation is closed under lubs of directed sets in [[A]]_{D} ↔ [[A]]_{D′}. This condition is needed for recursion to be compatible with the Logical Relations Lemma, below.)

\begin{aligned}[[α]]_{R} & = & Rα \\ [[I]]_{R} & = & \{⟨a, a⟩ | a ^{∈} I\} \\ [[nat]]_{R} & = & \{⟨n, n⟩ | n ^{∈} N_{⊥}\} \\ [[σ ⊗ σ′]]_{R} & = & \{⟨[d, d′], [e, e′]⟩ | ⟨d, e⟩ ^{∈} [[σ]]_{R} ∧ ⟨d′, e′⟩ ^{∈} [[σ′]]_{R}\} \\ [[A &B]]_{R} & = & \{⟨⟨d, d′⟩, ⟨e, e′⟩⟩ | ⟨d, e⟩ ^{∈} [[A]]_{R} ∧ ⟨d′, e′⟩ ^{∈} [[B]]_{R}\} \\ [[A → B]]_{R} & = & \{⟨f, f′⟩ | ∀⟨d, d′⟩ ^{∈} [[A]]_{R}. ⟨fd, f′d′⟩ ^{∈} [[B]]_{R}\} \\ [[A−∘ B]]_{R} & = & \{⟨f, f′⟩ | ∀⟨d, d′⟩ ^{∈} [[A]]_{R}. ⟨fd, f′d′⟩ ^{∈} [[B]]_{R}\} \\ [[!A]]_{R} & = & \{⟨d, e⟩ | ⟨d, e⟩ ^{∈} [[A]]_{R} ∨ d = e = ⊥\}. \end{aligned}

The relational actions of → and −∘ use the same clauses, the difference being that the clause for −∘ assumes that both f and f′ are strict. In the definition of ⊗, [x, y] is the least element ⟨⊥, ⊥⟩ if x or y is ⊥ and is the pair ⟨x, y⟩ otherwise. We often refer to the relational action of type constructors directly, for example by writing R ⊗ S instead of [[α ⊗ β]](α ↦ R, β ↦ S).

The relational action of ⊗ deserves comment. A basic justification for the definition is the following two properties that it satisfies:

—If ⟨f, g⟩ ^{∈} R−∘ S and ⟨f′, g′⟩ ^{∈} R′−∘ S′ then ⟨f ⊗ f′, g ⊗ g′⟩ ^{∈} R ⊗ R′−∘ S ⊗ S′, —R ⊗ S−∘ T ≅ R−∘ (S−∘ T).

The first property connects the functorial and relational actions of ⊗, and is needed for the interpretation of the elimination rule for ⊗ to satisfy relevant parametricity properties (needed for the Logical Relations Lemma below). The second is a relationship we expect between ⊗ and −∘.

Next, note that we do not have the property that

⟨a, b⟩(R ⊗ S)⟨c, d⟩ implies aRc and bSd.

For instance if ⊥Rc and bSd then ⟨⊥, ⊥⟩(R ⊗ S)⟨c, d⟩ even when we do not have ⊥Sd. The property fails because of the use of [·, ·] in the definition of R ⊗ S.

Finally, a particular subtlety is that the formula for R⊗S does not always produce a complete relation, for complete relations R and S on arbitrary cpo’s. For example, consider relations R : N_{⊥} ↔ I and S : N_{⊥} ↔ V nat where R = {⟨⊥, ⊥⟩, ⟨⊥, ∗⟩} and S = {⟨⊥, 0⟩, ⟨1, 2⟩, ⟨2, 3⟩, ...}, and V nat is the vertical natural numbers. Then R⊗S contains a chain of all tuples ⟨⟨⊥, ⊥⟩, ⟨∗, n⟩⟩, for n > 1, but it does not contain the lub ⟨⟨⊥, ⊥⟩, ⟨∗, ∞⟩⟩. Nevertheless, R ⊗ S is strict and trivially complete whenever R and S are strict relations on flat (or finite height) cpo’s. In the semantics of our polymorphic language ⊗ is only ever applied to flat cpo’s, so the definition of the relational action is suitable for this language.

Returning to the definition of the model, we can now define the cpo and relational semantics for ∀. For this, let Level1 stand for the collection of countable, flat cpo’s. A polymorphic function will be an element of an indexed product, indexed by cpo’s in Level1, subject to a relational parametricity condition:

[[∀α.A]]_{D} = {p ^{∈} ∏_{d^{∈}Level1}[[A]]_{D|α↦d} |

∀d, d′ ^{∈} Level1 , ∀r : d ↔ d′. ⟨p[d], p[d′]⟩ ^{∈} [[A]]_{I_{D}|α↦r}

}, ordered pointwise

⟨p, p′⟩ ^{∈} [[∀α.A]]_{R} ⇔ ∀d, d′ ^{∈} Level1 , ∀r : d ↔ d′. ⟨p[d], p′[d′]⟩ ^{∈} [[A]]_{R|α↦d}.

Here I_{D} maps each α to the identity relation Δ_{Dα} on Dα. The notation r : d ↔ d′ indicates that r is a relation between (flat) cpo’s d and d′ that relates their least elements. For the well-definedness of this definition it is crucial that Level1 is essentially small – there are only set-many countable, flat cpo’s (at least up to isomorphic copies).

With these definitions one may verify that each [[A]]_{D} is a cpo and each [[A]]_{R} is a complete relation on cpo’s. This ensures that the least fixed-point operator exists in the model.

By “parametric model” we mean a model satisfying the Identity Extension Lemma:

[[A]]_{I_{D}} = {⟨a, a⟩ | a ^{∈} [[A]]_{D}}.

This is usually taken as the defining characteristic of relational parametricity [Reynolds 1983], and the definition of ∀ is arranged precisely to ensure the identity property (which is included here as part of the Isomorphism Lemma).

Lemma 1. (Isomorphism Functoriality Lemma) For any type A, the relational action of [[A]] is functorial on isomorphisms. That is, (i) if Rα is the graph of an isomorphism between flat cpo’s for each α free in A then [[A]]_{R} is the graph of an isomorphism, and (ii) [[A]] preserves identities and composites of isomorphisms.

6.2 Semantics of Terms

A typing judgement

x_{1} : A_{1}, …, x_{n} : A_{n}; y_{1} : B_{1}, …, y_{m} : B_{m} ⊢ t : C

is interpreted by a D-indexed family of strict continuous functions

[[t]]_{D} : ([[A_{1}]]_{D})_{⊥} ⊗ ⋯ ⊗ ([[A_{n}]]_{D})_{⊥} ⊗ [[B_{1}]]_{D} ⊗ ⋯ ⊗ [[B_{m}]]_{D} ⟶ [[C]]_{D}.

We omit the detailed definition, which is standard, but we do describe the uniformity property of this family. For this, we extend relational actions from types to typing contexts using the actions for ⊗ and !:

\begin{aligned}& [[x_{1} : A_{1}, …, x_{n} : A_{n}; y_{1} : B_{1}, …, y_{m} : B_{m}]]_{R} \\ = & [[!A_{1}]]_{R} ⊗ ⋯ ⊗ [[!A_{n}]]_{R} ⊗ [[B_{1}]]_{R} ⊗ ⋯ ⊗ [[B_{m}]]_{R}. \end{aligned}

Lemma 2. (Logical Relations Lemma) If

Γ; Δ ⊢ t : A

Rα : Dα ↔ D′α, for all α ⟨η, η′⟩ ^{∈} [[Γ; Δ]]_{R},

then

⟨ [[t]]_{D}η , [[t]]_{D′}η′ ⟩ ^{∈} [[A]]_{R}.

Since logical relations are used to constrain ∀ types, the lemma and the welldefinedness of the maps [[t]]_{D} are proven simultaneously by induction on t.

7. WORKING WITH THE MODEL

Our aim in this section is to illustrate how strict, relational parametricity can be used to reason about types and terms in the source languages. All of the examples go beyond those that can be treated properly in either the basic functor category model of Oles [1982] or the parametric functor models of O’Hearn and Tennent [1995], and Sieber [1996]. (The ability to relate ⊥ to non-⊥ states is responsible for the improvement over [O’Hearn and Tennent 1995].)

From now on we will often mix notation for polymorphic types and cpo’s. For instance, we write

∀β. (S ⊗ β−∘ S ⊗ β) → (S ⊗ β−∘ S ⊗ β)

instead of the more cumbersome

[[∀β. (α ⊗ β−∘ α ⊗ β) → (α ⊗ β−∘ α ⊗ β)]]_{(α↦S)}.

Similarly, we write M^{⋆}S and M^{∘}S to indicate functions, and θ^{⋆}S and θ^{∘}S to indicate cpo’s, obtained by composing the translations with the semantics of the linear langauge.

7.1 Snapback

Example 1. We consider a snapback operator of type

∀α. (α−∘ α ⊗ nat) → (α−∘ α ⊗ nat).

Were it to exist in the model, this operator would satisfy the property

snap[S]e s = \{ \begin{matrix}⟨s, n⟩ & if e(s) = ⟨s′, n⟩ \\ ⊥ & if e(s) = ⊥ \end{matrix}

for countable flat cpo’s S and s ^{∈} S. We show that snap is not parametric.

Consider any p ^{∈} [[∀α. (α−∘ α ⊗ nat) → (α−∘ α ⊗ nat)]]. We show the following property (where 2 = {0, 1}):

If e : 2_{⊥}−∘ 2_{⊥} ⊗ N_{⊥} is such that e(s) = ⟨1, 1⟩ when s ≠ ⊥,
and p[2_{⊥}]e0 = ⟨0, 1⟩
then p[2_{⊥}]⊥0 = ⟨0, 1⟩.

This property says that if you use e at all, the final state can no longer be 0: Using e causes an irreversible state change.

To prove the property, suppose the two assumptions hold for p and e, and consider the relation R : 2_{⊥} ↔ 2_{⊥} consisting of tuples ⟨0, 0⟩, ⟨⊥, ⊥⟩, ⟨1, ⊥⟩. Then ⟨e, ⊥⟩ ^{∈} [R−∘ R ⊗ Δ_{N_{⊥}}] and by parametricity ⟨p[2_{⊥}]e0, p[2_{⊥}]⊥0⟩ ^{∈} R ⊗ Δ_{N_{⊥}}. Since ⟨0, 1⟩ is only R ⊗ Δ_{N_{⊥}}-related to itself the property follows.

In contrast, the property is not satisfied by snap because snap[2_{⊥}]⊥0 = ⊥, even though we will have snap[2_{⊥}]e0 = ⟨0, 1⟩ for any e satisfying the first assumption in the property. Thus, snap does not exist in the model.

The argument for the non-parametricity of snapback is, in fact, a transcription of the failure of Weakening in the category of cpo’s and strict functions. Specifically, for any cpo D there is a candidate Weakening map w_{D} : D−∘ I that takes ⊥ to ⊥ and all other elements of D to the non-⊥ element of I. Though this map exists for all D, it is not natural, in that

[figure: D; E; I; f; w_{D}; w_{E}]

does not commute when f takes a non-⊥ element to ⊥. Re-expressing this in relational form, using the graph of such an f, shows that the family w_{D} of maps, indexed by countable, flat cpo’s D ^{∈} Level1, is not in [[∀α. α−∘ I]].

The failure of the naturality of this Weakening map is reminiscent of our contention that it is general, or polymorphic, snapback that does not exist in Algol, whereas specific state changes can often be reversed.

Example 2. The reasoning in Example 1 can be used more positively, to verify the snaptester equivalence from the Introduction:

new x. x := 0; p(x := x + 1); if (x > 0) then diverge ≡ p(diverge).

To show the equivalence we argue that the translations

(2) \underline{λ}s : α. let [s′, n′] be p[nat](id_{α} ⊗ \underline{λ}n. n + 1)[s, 0]

in let [s′′, n′′] be (if n′ > 0 then Ω s′ else s′)

in (let ∗ be (discard n′′) in s′′) : α−∘ α

and

(3) \underline{λ}s : α. let [s′, n] be p[I](Ω_{(α⊗I)−∘ (α⊗I)}) [s, ∗] in let ∗ be (discard n) in s′

are equivalent, where

p : ∀β. (α ⊗ β−∘ α ⊗ β) → (α ⊗ β−∘ α ⊗ β).

Let S be a countable, flat cpo (the denotation of α) and consider the relation R : N_{⊥} ↔ I consisting of the tuples ⟨⊥, ⊥⟩, ⟨0, ∗⟩, and ⟨i, ⊥⟩ for i > 0. Let c : S ⊗ N_{⊥}−∘ S ⊗ N_{⊥} be id_{S} ⊗ succ, where succ is the strict extension of successor. Then

⟨c, ⊥⟩ ^{∈} Δ_{S} ⊗ R−∘ Δ_{S} ⊗ R.

As a result, for arbitrary p we can use the parametricity property to get

⟨p[N_{⊥}]c[s, 0] , p[I]⊥[s, ∗]⟩ ^{∈} Δ_{S} ⊗ R.

Next, for any s ^{∈} S suppose that p[N_{⊥}]c[s, 0] = [s′, n] and p[I]⊥[s, ∗] = [s′′, x]. Using ⟨[s′, n], [s′′, x]⟩ ^{∈} Δ_{S} ⊗ R we can argue that (2)=(3) by cases as follows:

—If [s′, n] = ⊥ then [s′′, x] = ⊥ by the definition of R and ⊗, and so (2)s=(3)s. —If p[N_{⊥}]c[s, 0] = [s′, n] ≠ ⊥ then there are two subcases.

—If n = 0 then, by the definition of R, we must have that [s′′, x] = [s′, ∗] and

obviously (2)s=(3)s, since both will, when beginning in state s, return s′. —If n > 0 then we know that (2) applied to s returns ⊥. But since n > 0 we

know, from the definition of R and parametricity, that [s′′, x] = ⊥, and so both (2) and (3) return ⊥ when started in state s.

Many other equivalences can be treated using this form of reasoning. Typically, one finds a relation between pieces of local state and implementations of different objects. For example, to show the equivalence of two counter classes

λp. new λ x. x := 0;  ≡  λp. new λ x. x := 0;
p(x := x + 1, x) p(x := x + 2, x/2)

for p : comm × exp → comm, we simply use a relation on their local states R : N_{⊥} ↔ N_{⊥} consisting of ⟨⊥, ⊥⟩ and all pairs ⟨i, 2i⟩. This example (taken from [O’Hearn and Tennent 1995]) indicates that the strict-function model provides an extension of the reasoning methods presented there.

Example 3. Since the cpo model of PCF contains functions such as “parallel or,” [Plotkin 1977] one might expect similar functions to arise in the model here. But, in the presence of side effects, if we are to evaluate two arguments in parallel then indeterminacy typically results, unless we use snapback. For example, a “parallel or” function of type (exp → exp → exp)^{∘}I in SCI would be determined by a function of type

∀αβ. (α−∘ α ⊗ nat)&(β−∘ β ⊗ nat) → (α ⊗ β−∘ α ⊗ β ⊗ nat)

with the following defining property:

por[S_{1}][S_{2}]⟨e_{1}, e_{2}⟩ [s_{1}, s_{2}] = \{ \begin{matrix}⟨s_{1}, s_{2}, 0⟩ & if ∃s′_{1}. e_{1}(s_{1}) = ⟨s′_{1}, 0⟩ \\ & ∨ ∃s′_{2}. e_{2}(s_{2}) = ⟨s′_{2}, 0⟩ \\ ⊥ & otherwise \end{matrix}

This function is not parametric, because por[I][–]⟨⊥, –⟩ would essentially be the unary snapback which, as we saw in Example 1, is not parametric. Note here that the condition ∃s′_{1}. e_{1}(s_{1}) = ⟨s′_{1}, 0⟩ is testing whether running e_{1} results in termination with result 0, and possibly some state change; it, and the other disjunct, are false in the case of non-termination and also in the case of producing a result other than 0.

A more subtle form of parallelism and snapback, which is not correctly treated by the model, will be considered at the end of this section.

7.2 Sample Type Analyses

Example 4. The polymorphic type (comm → comm)^{⋆}I corresponds to closed terms of type comm → comm in Idealized Algol. We can calculate its structure as follows:

(comm → comm)^{⋆}I
= ∀β. ((I ⊗ β)−∘ (I ⊗ β)) → ((I ⊗ β)−∘ (I ⊗ β))
≅ ∀β. (β−∘ β) → (β−∘ β)
≅ N_{⊥},

where the last isomorphism uses a parametricity argument in the strict-function model. On the level of Idealized Algol, we obtain a correspondence

n ↦ λc : comm. c^{n}
⊥ ↦ λc : comm . diverge,

where c^{0} = skip and c^{i+1} = c; c^{i}. This representation of comm → comm should be compared to that of O’Hearn and Tennent [1995], where (comm → comm)I is N_{⊥} ⊗ V nat^{op}, with V nat^{op} the vertical natural numbers flipped upside-down. The V nat component was concerned exclusively with a form of snapback.

It is instructive to examine the parametricity argument giving the final isomorphism with N_{⊥}. (It is in fact the usual parametricity argument for Church numerals [Plotkin 1980; Reynolds 1983], extended to take appropriate care of the presence of ⊥.) Let p ^{∈} [[∀β. (β−∘ β) → (β−∘ β)]] and consider any flat cpo D, d ^{∈} D, and c : D−∘ D. Let R : N_{⊥} ↔ D be the relation consisting of pairs ⟨⊥, ⊥⟩ and ⟨m, c^{m}(d)⟩. Then ⟨succ, c⟩ ^{∈} R−∘ R and, by parametricity, (p[N_{⊥}] succ 0) R (p[D] c d). Next, if (p[N_{⊥}] succ 0) = ⊥ then the definition of R ensures that (p[D] c d) = ⊥, and so p = ⊥. And if (p[N_{⊥}] succ 0) = n ≠ ⊥ then the definition of R ensures that (p[D] c d) = c^{n}d, and so p is the n’th Church numeral. We may conclude that [[∀β. (β−∘ β) → (β−∘ β)]] is isomorphic to N_{⊥}.

In this argument note that R is strict and single-valued. Note also that n is related to ⊥ when c^{n}d = ⊥. In [O’Hearn and Tennent 1995], relations that relate ⊥ to non-⊥ elements were not considered, which is why this argument could not go through.

Example 5. The SCI interpretation (comm → comm)^{∘}I turns out to be the same as (comm → comm)^{⋆}I. However, when we replace I by a non-trivial flat cpo S a difference appears. We calculate

(comm → comm)^{∘}S
= ∀β. (β−∘ β) → ((S ⊗ β)−∘ (S ⊗ β))
≅ S−∘ (S ⊗ N_{⊥}),

where the last isomorphism is again a straightforward parametricity argument. In the cpo S−∘ (S ⊗ N_{⊥}), the N_{⊥} part corresponds to use of the β-component, the number of times the command argument is executed (so this part is essentially a Church numeral). This cpo illustrates how the computation on the S and β components can be carried out independently: The input state can affect the number of times the command argument is used, but not what happens on each use. Equally, none of the uses of the command argument affects the S-component, which is why there is a single transformation from input state to output that is independent of β. This independence is reflected in certain equivalences between terms, such as between procedures λc. c; x := 1 and λc. x := 1; c of type comm → comm.

The same type in Idealized Algol translates as follows:

(comm → comm)^{⋆}S
= ∀β. (S ⊗ β−∘ S ⊗ β) → ((S ⊗ β)−∘ (S ⊗ β)).

The representation in terms of S−∘ (S ⊗ N_{⊥}) no longer works due to the possibility of interference between procedure and argument in Idealized Algol. For instance, the terms λc. c; x := 1 and λc. x := 1; c can be now distinguished by being applied to an argument that interferes with x.

An explicit description of the cpo for (comm → comm)^{⋆}S can be given in terms of resumptions. This will be presented as a special case of a representation result in Section 10.1.

Example 6. Next we consider a type for functions with two arguments:

(comm × comm → comm)^{⋆}I
≅ ∀β. (β−∘ β)&(β−∘ β) → (β−∘ β)
≅ (list{1, 2})_{⊥}.

A list ℓ of 1’s and 2’s corresponds to λc : comm × comm . c^{ℓ}, where c^{ϵ} = skip and c^{i,ℓ} = (π_{i}c); c^{ℓ}, for i = 1, 2 and i, ℓ is the cons of i onto ℓ. The parametricity argument showing the last isomorphism is essentially the same as in Example 4. With this representation we can see which argument an element of this type evaluates first: i, ℓ evaluates the i’th argument.

Example 7. Two-argument curried functions in SCI are less rigidly sequential, in that it is not necessary for one argument to be evaluated first:

(comm → comm → comm)^{∘}S
≅ ∀βγ. (β−∘ β)&(γ−∘ γ) → (S ⊗ β ⊗ γ−∘ S ⊗ β ⊗ γ)
≅ S−∘ (S ⊗ N_{⊥} ⊗ N_{⊥}).

In this case computation in the β, γ, and S components can all be carried out independently, being again Church numerals in β and γ. If we consider the case where S = I, then we obtain a correspondence between N_{⊥} ⊗ N_{⊥} and closed SCI terms of type comm → comm → comm:

\begin{matrix}⟨n, m⟩ & ↦ & λc_{1}. λc_{2}. c^{n} ∥ c^{m} \\ ⊥ & ↦ & λc_{1}. λc_{2} . diverge. \end{matrix}

In contrast to Example 6, the evaluations of the two command arguments can proceed completely independently, in parallel.

7.3 A Limitation of Binary, Strict Parametricity

Independence from evaluation order in SCI gives rise to examples that require stronger principles than binary relational parametricity to treat correctly.

Example 8. We define a function rotate in the denotation of the type

∀α_{1}α_{2}α_{3}. (α_{1}−∘ α_{1} ⊗ nat)&(α_{2}−∘ α_{2} ⊗ nat)&(α_{3}−∘ α_{3} ⊗ nat)
⟶ (α_{1} ⊗ α_{2} ⊗ α_{3}−∘ α_{1} ⊗ α_{2} ⊗ α_{3} ⊗ nat)

This type is isomorphic to (exp → exp → exp → exp)^{∘}I. The definition is

rotate[S_{1}, S_{2}, S_{3}]⟨c_{1}, c_{2}, c_{3}⟩[s_{1}, s_{2}, s_{3}]

= \{ \begin{matrix}[s′_{1}, s′_{2}, s_{3}, 0] & if c_{1}s_{1} = [s′_{1}, 0] ≠ ⊥ ∧ c_{2}s_{2} = [s′_{2}, 0] ≠ ⊥ \\ [s_{1}, s′_{2}, s′_{3}, 1] & if c_{2}s_{2} = [s′_{2}, 1] ≠ ⊥ ∧ c_{3}s_{3} = [s′_{3}, 1] ≠ ⊥ \\ [s′_{1}, s_{2}, s′_{3}, 2] & if c_{1}s_{1} = [s′_{1}, 2] ≠ ⊥ ∧ c_{3}s_{3} = [s′_{3}, 2] ≠ ⊥ \\ ⊥ & otherwise \end{matrix}

Informally, to evaluate rotate we begin by evaluating its three arguments in parallel. Of the three possible rightmost conditions above only one can apply. If it is the first, then we return the altered states s′_{1} and s′_{2}, while leaving s_{3} unchanged. Similarly we leave s_{1} unchanged in the second case and s_{2} in the third. Intuitively, this involves a form of snapback in each argument. Nevertheless, rotate does exist in the model. (We leave the verification of parametricity conditions as an exercise.)

This example shows a limitation of the strict-function model of the polymorphic calculus, and of the corresponding model of Basic SCI. In particular, because of the example we would not expect a result to the effect that the syntactic type (exp → exp → exp → exp)^{∘}I is, in the model, characterized by SCI-definable elements: It seems reasonably clear that rotate is not definable in the linear language (though a rigorous proof would be very involved).

Although this points to a limitation in the strict parametricity model, it does not indicate a problem in our syntactic translation. We believe that the elements of the cpo (exp → exp → exp → exp)^{∘}I that are definable by source and target language terms are the same. Furthermore, it appears that these definable elements (and their lubs) form a cpo that is isomorphic to the cpo N^{∗} × N^{∗} × N^{∗} →_{s} N_{⊥} of Kahn-Plotkin sequential functions, where N^{∗} is a stream cpo.

The rotate function is a variation on Berry’s [1978] example of a stable function that is not sequential. It came to our attention in the context of SCI because of Reddy’s coherence space model, where a version of it is also present. This indicates that neither model fully accounts for sequentiality, or for the absence of snapback. Reddy has suggested that one might hope that the approach to sequentiality using games [Abramsky et al. ; Hyland and Ong 1994] might help to resolve this issue. Another possibility would be to use a stronger form of parametricity based, perhaps, on Kripke relations, which have also proven useful in approaching sequentiality [O’Hearn and Riecke 1995; Riecke and Sandholm 1997].

8. RELATION TO FUNCTOR MODELS

While we have said that our translations are based on functor-category models, the precise relationship to them may not be obvious. In particular, the translation for Idealized Algol relies on special properties of the functor-category model defined by Oles [1982, 1997], and does not use standard structure found in all functor categories. Furthermore, the translation for Basic SCI is unusual, in that each identifier is associated with a separate store shape. In this section we describe the ingredients allowing connections between the polymorphic and functor-category forms of semantics to be drawn.

For Idealized Algol we define a logical relation between our model and the functorcategory model of Oles (allowing for side effects in expressions). The logical relation establishes that our model agrees with Oles’s on the meanings of closed terms of primitive type. A corollary of this is a computational adequacy result, connecting the model to an operational semantics for Idealized Algol. Interestingly, parametricity is not needed for this connection to be made, and it goes through for a model in which ∀ is simply an indexed product. For Basic SCI we relate the style of interpretation where each identifier is associated with a separate store shape to a notion of multi-map between functors.

It would be helpful to have some familiarity with functor-category models here. In the next section we return to an analysis of the translations in their own right.

8.1 Idealized Algol

We recall the category Σ of store shapes [Oles 1982; Oles 1987].

—The objects are countable sets. —The morphisms from W to X are pairs of set-theoretic functions

φ : X → W, ρ : W × X → X such that

(1) ∀x ^{∈} X. ρ⟨φ(x), x⟩ = x;

(2) ∀x ^{∈} X. ∀w ^{∈} W. φ(ρ⟨w, x⟩) = w;

(3) ∀x ^{∈} X. ∀w, w′ ^{∈} W. ρ⟨w, ρ⟨w′, x⟩⟩ = ρ⟨w, x⟩.

The propotypical example is the “expansion” morphism (φ, ρ): W → W × Y where W × Y is the set-product, φ is the first projection and ρ⟨w′, ⟨w, y⟩⟩ = ⟨w′, y⟩. The composite of morphisms (φ, ρ): W → X and (φ′, ρ′): X → Y is (φ′′, ρ′′): W → Y such that φ′′ = φ′; φ and ρ′′⟨w, y⟩ = ρ′⟨ρ⟨w, φ′(y)⟩, y⟩. The identity morphism on W is (φ, ρ) such that φ(w) = w and ρ(w, w′) = w. (φ, ρ) is an isomorphism iff φ is a bijection.

Let Predom denote the category of predomains (possibly bottomless cpo’s) and continuous functions. The functor category Predom^{Σ} is Cartesian closed. In fact, Predom^{C} is Cartesian closed, for any small category C: The internal hom can be given in a standard way using the definition

(F ⇒ G)X = Predom^{C}[C[X, –] × F, G]. (Standard Definition)

(Note that this formula is covariant in X, which gives the action on morphisms.) However, in the case that C = Σ a factorization of morphisms shown by Oles allows the internal hom to be calculated in a special way.

Lemma 3. (Expansion Factorization Lemma) Any morphism (φ, ρ) : X → Y in Σ factors as an expansion followed by an isomorphism X →^{e} X × Z →^{i} Y.

Lemma 4. (Exponent Representation Lemma) The internal hom ⇒ in Predom^{Σ} is such that

(F ⇒ G)X ≅ Predom^{Σ}[F (X × –), G(X × –)], ordered pointwise

for any functors F, G : Σ → Predom and any countable set X. (We are using X ×– to denote the evident endofunctor on Σ; but note that × is not the categorical product in Σ.)

Proof: The proof of the Factorization Lemma is in [Oles 1982]; we sketch why the Representation Lemma follows from it. Any p ^{∈} (F ⇒ G)X accepts a store shape Y and a pair ((φ, ρ) : X → Y, a ^{∈} F Y) as arguments, and produces a result in GY. Using Oles’s lemma, we can factor (φ, ρ) into a composite X →^{e} X × Z →^{i} Y. By functoriality F (i^{−1}) and Gi are both isomorphisms, where i^{−1} is the isomorphism inverse to i. By naturality for the isomorphisms, p[Y]((φ, ρ), a) must be equal to Gi(p[X × Z](e, (F i^{−1})a). Thus, we can see that p is completely determined by its action on expansions, and this leads in a straightforward fashion to the representation result.

Notice that the formula for the internal hom in the Representation Lemma is formally similar to the translation of function types in Idealized Algol. With this it is possible to establish a connection with the translation (·)^{⋆}, which we now outline.

First, given the Representation Lemma, we might as well define the internal hom as

(F ⇒ G)X = Predom^{Σ}[F (X × –), G(X × –)]. (Alternate Definition)

If e : X → X × Y is an expansion then the required functorial action of F ⇒ G is given (suppressing associativity isomorphisms) by

((F ⇒ G)e p)[W] = p[Y × W] : F (X × Y × W) → G(X × Y × W).

If i : X → Y is an isomorphism then

((F ⇒ G)i p)[W] = F (i × W)^{−1}; p[W]; G(i × W),

and the functorial action for arbitrary Σ-morphisms is then obtained from the Expansion Factorization Lemma.

In order to interpret recursion we need to work in the full subcategory whose objects are functors F where [Oles 1982]: (i) F X has a least element, for each store shape X, and (ii) F (φ, ρ) preserves least elements, for each Σ-morphism (φ, ρ). All of the objects we mention will in fact lie in this subcategory.

We can now define a functor O[[θ]] for each Idealized Algol type θ. (The product F × G of functors is defined pointwise as usual.)

O[[comm]]W = W_{⊥}−∘ W_{⊥}

O[[comm]](φ, ρ)cs = \{ \begin{matrix}⊥ & if s = ⊥ or c(φs) = ⊥ \\ ρ⟨c(φ(s)), s⟩ & otherwise \end{matrix}

O[[acc]]W = W_{⊥} ⊗ N_{⊥}−∘ W_{⊥}

O[[acc]](φ, ρ)c⟨s, n⟩ = \{ \begin{matrix}⊥ & if s = ⊥ or c[(φs), n] = ⊥ \\ ρ⟨c[φ(s), n], s⟩ & otherwise \end{matrix}

O[[exp]]W = W_{⊥}−∘ W_{⊥} ⊗ N_{⊥}

O[[exp]](φ, ρ)es = \{ \begin{matrix}⊥ & if s = ⊥ or e(φs) = ⊥ \\ ρ⟨ρ(s, s′), n⟩ & when ⟨s′, n⟩ = e(φs) \end{matrix}

O[[θ → θ′]] = O[[θ]] ⇒ O[[θ′]]

O[[θ × θ′]] = O[[θ]] × O[[θ′]] The morphism part of O[[comm]] appears, at first sight, to be nonlinear in the store, where s is copied. Apart from the fact that the two occurrences of s are in different arms of a pairing for a categorical product ⟨·, ·⟩, this is not a problem because when (φ, ρ) is an expansion the “otherwise” clause of the definition is equivalent to ρ⟨cx, y⟩, and this is what we use in the translation to linear λ-calculus.

Now we set up a logical relation between (·)^{⋆} and O[[·]], the former understood in terms of the strict parametricity model. For each type θ and countable set X, we define a relation

R_{θ}^{X} ⊆ θ^{⋆}X_{⊥} × O[[θ]]X.

For θ = comm, acc or exp, R_{θ}^{W} is an identity relation, and product types use the obvious pointwise definition. For procedures,

⟨p, q⟩ ^{∈} R_{θ→θ′}^{X} ⟺ ∀W. ⟨a, b⟩ ^{∈} R_{θ}^{X×W} ⇒ ⟨p[W_{⊥}]a, q[W]b⟩ ^{∈} R_{θ′}^{X×W} .

We define R_{Γ}^{X} by viewing a type assignment Γ as a product as usual.

Lemma 5. Each R_{θ}^{X} is a pointed, complete relation.

Lemma 6. (Expansion Relatedness Lemma) If ⟨a, b⟩ ^{∈} R_{θ}^{X} then

⟨(expand_{θ}[X_{⊥}][Y_{⊥}]a), (O[[θ]](e)b)⟩ ^{∈} R_{θ}^{X×Y} ,

where e : X → X × Y is the expansion in Σ.

The proof of the Expansion Relatedness Lemma is straightforward, as the definition of expand_{θ} merely copies the definition of O[[θ]]e in the functor category.

Each judgement Γ ⊢ M : θ in Idealized Algol is interpreted as a natural transformation

O[[M]] : O[[Γ]] →^{.} O[[θ]].

The interpretations are essentially as in the translations (·)^{⋆}, except that we use environment manipulations in place of substitution. Representing environments u ^{∈} O[[Γ]]X as functions from identifiers to appropriately-typed values, representative equations are:

O[[M; M′]]W us = O[[M′]]W u(O[[M]]W us)
O[[λx : θ. M]]W u[X]d = O[[M]](W × X) ((O[[Γ]]fu) | x ↦ d)
O[[M(M′)]]W u = h(O[[M]]W u[I](iO[[M′]]W u))
O[[new_{comm} M]]W uw = \{ \begin{matrix}w′ & if O[[M]]W u[N]v[w, 0] = [w′, n] \\ ⊥ & if O[[M]]W u[N]v[w, 0] = ⊥. \end{matrix}

In these definitions, i and h are suitable isomorphisms, f : W → W × X is the expansion morphism, N is the set of natural numbers. The standard local variable v is ⟨a, e⟩, where e : (X ×N)_{⊥}−∘ ((X ×N)×N)_{⊥} and a : ((X ×N)×N)_{⊥}−∘ (X ×N)_{⊥} are the unique strict functions such that

e⟨x, n⟩ = ⟨⟨x, n⟩, n⟩, and
a⟨⟨x, n⟩, m⟩ = ⟨x, m⟩.

(Notice that a and e are obtained by lifting ρ and φ from the expansion map (φ, ρ) : X → X × N in the category Σ.)

Lemma 7. Suppose Γ ⊢ M : θ in Idealized Algol, and that ⟨u, u′⟩ ^{∈} R_{Γ}^{X}. Then ⟨(M^{⋆}X_{⊥} u), (O[[M]]X u′)⟩ ^{∈} R_{θ}^{X}.

Proof: By induction on M. We indicate the key cases of new and λ-abstraction.

For new_{φ}(M), by induction we know that ⟨p, q⟩ ^{∈} R_{var→φ}^{X}, where p is the denotation of M in the strict parametricity model and q in the Oles model. new_{φ}(M) is defined in the models by supplying local variables v and v′ to p and q, and deallocating on termination. Clearly, by the definition of R for procedure types, this case will hold if we can show that the two standard variables are in relation R_{var}^{X×N}, and this is easy to check from their definitions above and in Section 5.

For the case Γ ⊢ λx : θ. M : θ → θ′, suppose ⟨d, d′⟩ ^{∈} R_{θ}^{X×Y}. We need to show that ⟨m, m′⟩ ^{∈} R_{θ′}^{X×Y}, where

m = ((M^{⋆}(α ⊗ β))[expand_{θ_{i}}[α][β]x_{i}/x_{i}])(α ↦ X_{⊥}, β ↦ Y_{⊥})(u | x ↦ d),
m′ = O[[M]](X × Y)(O[[Γ]]eu′|x ↦ d′).

Here, e : X → X × Y is the expansion, m is the translation of a λ-abstraction, applied in the strict parametricity model to an appropriate world Y_{⊥} and argument d′, and m′ is obtained from the meaning of λ-abstraction in the functor category. Using a substitution lemma for the parametricity model of the linear lambda-calculus we can infer

m = (M^{⋆}(X_{⊥} ⊗ Y_{⊥})(x_{i} ↦ (expand_{θ_{i}}^{⋆}[X_{⊥}][Y_{⊥}](ux_{i})) , x ↦ d).

Further, (O[[Γ]](e)u′|x ↦ d′) is of the form (x_{i} ↦ O[[θ_{i}]]e(u′x_{i}), x ↦ d), so we know that the environments (x_{i} ↦ (expand_{θ_{i}}^{⋆}[X_{⊥}][Y_{⊥}](ux_{i})) , x ↦ d) and ([[Γ]](e)u′|x ↦ d′) are R_{Γ,x:θ′}^{X×Y}-related, using the Expansion Relatedness Lemma and the assumptions that u and u′, and d and d′, are related. We can then use the induction hypothesis to conclude that m and m′ are related.

At primitive types this lemma reduces to the following.

Proposition 8. (Adequacy with Oles’s Model) If ⊢ M : φ in Idealized Algol then M^{⋆}X_{⊥} = O[[M]]X.

Furthermore, Lent [1993] has verified that Oles’s model satisfies an adequacy correspondence with a suitable operational semantics, to the effect that a closed term of command type converges operationally iff it does not denote ⊥ (and the proof carries through equally in the presence of expressions with side effects). Thus, adequacy with respect to Oles’s model establishes also adequacy with respect to a standard operational semantics. Note that parametricity has not been used thus far in this section, and the adequacy result would go through for the unconstrained model of polymorphism, where ∀ is simply indexed product over countable, flat cpo’s.

The logical relation, however, contains more information than required for adequacy, which will be put to use in some technical lemmas at the end of the next section.

8.2 Basic SCI

It is not difficult to interpret SCI in Predom^{Σ}, by mimicking (·)^{∘}, and to verify an adequacy correspondence as was done for Idealized Algol. Rather than do this, we want to relate the somewhat unusual form of interpretation, where each identifier gets a separate piece of the store, to structure found in the functor category; see also [O’Hearn et al. 1999].

First, recall the translation of the SCI function type:

(θ → θ′)^{∘}α = ∀β. θ^{∘}β → θ′^{∘}(α ⊗ β).

We can rewrite this in functorial form as follows: If G, F : Σ ⟶ Predom are functors, then the functor G^{F} is defined by the equation

(G^{F})X = Predom^{Σ}[F (–), G(X × –)], ordered pointwise.

This formula is covariant in X, which gives the action on morphisms.

What is the sense in which G^{F} is a function type? One way to explain this would be to find a tensor product of functors satisfying the usual adjunction property

Predom^{Σ}[E ⊗ F, G] ≅ Predom^{Σ}[E, G^{F}].

In fact, G^{F} is precisely the exponent of functors described by Day [1970], who also gives a recipe for obtaining the required tensor products.

Another, for our purposes more direct, way is to proceed is to look explicitly at maps of multiple arity.

Definition 9. Suppose F_{1}, …, F_{n} and G are functors in Predom^{Σ}. A multimap

η : F_{1}, …, F_{n} ⟶ G

is a family of continuous functions

η[X_{1}, …, X_{n}] : F_{1}X_{1} × ⋯ × F_{n}X_{n} ⟶ G(X_{1} × ⋯ × X_{n})

natural in store shapes X_{1}, …, X_{n}. (In case n = 0 a multi-map is a function from a one-point cpo to G(1), for 1 a one-point set.)

The connection between multi-maps and G^{F} is immediate from the definitions.

Proposition 10. Given functors F_{1}, …, F_{n}, F and G, multi-maps

η : F_{1}, …, F_{n}, F ⟶ G

are in bijective correspondence with multi-maps

η : F_{1}, …, F_{n} ⟶ G^{F}.

Proposition 10 could be restated in more abstract terms by saying that functors in Predom^{Σ}, together with multi-maps, comprise a closed multi-category [Lambek 1989]. We regard this as a kind of categorical justification for, or commentary on, the form of the translation of SCI.

At this point the reader may be wondering why we arranged the (·)^{∘} translation in this multi-map form: It would be more standard to follow the structure of a monoidal closed category, where we would interpret a term using a map out of a tensor product. There are two reasons. First, explicitly associating a different piece of local state with each identifier is very appealing, as it directly models the idea that distinct identifiers don’t interfere. Second, it is not clear to us how to describe Day’s tensor product of functors in polymorphic linear λ-calculus. As a result, if we were to add types θ ⊗ θ′ of noninterfering pairs to SCI, it would not be evident how to interpret them in the linear calculus.

9. ON NATURALITY AND PARAMETRICITY

We have seen a close relationship between our translations and semantic equations in a functor-category model. The main difference is that functor models require meanings to be natural with respect to expansions, where in the strict parametricity model we use binary relational parametricity. In this section we explore circumstances under which the former is implied by the latter. We begin by considering SCI, where the situation is simpler.

9.1 Basic SCI

In SCI, parametricity implies naturality at all types.

Theorem 11. (Naturality Theorem for SCI) Any p ^{∈} (θ_{1} → θ_{2})^{∘}S is natural with respect to expansions: for all flat cpo’s S_{1} and S_{2},

[figure: θ_{1}^{∘}(S_{1}); θ_{1}^{∘}(S_{1} ⊗ S′_{1}); θ_{2}^{∘}(S ⊗ S_{1}); θ_{2}^{∘}(S ⊗ S_{1} ⊗ S′_{1}); expand_{θ_{1}}[S_{1}][S′_{1}]; p[S_{1}]; p[S_{1} ⊗ S′_{1}]; expand_{θ_{2}}[S ⊗ S_{1}][S′_{1}]]

(where we have elided canonical isomorphisms (S ⊗ S_{1}) ⊗ S_{2} ↔ S ⊗ (S_{1} ⊗ S_{2})).

Proof: First, it is easy to see that the result holds for θ_{1} → (θ_{2} × θ_{3}) iff it holds for θ_{1} → θ_{2} and θ_{1} → θ_{3}. By an inductive argument we obtain that it suffices to prove the result for types of the form

θ_{1} → (θ_{2} → ⋯ (θ_{n} → φ) ⋯).

We prove it for φ = comm; the cases of acc and exp are similar. Also, to keep things simple, we give the proof for the case n = 2. This case shows the key role of disjointness between arguments in the proof, and is easily extended to other n.

We are required to show that (a)=(b), where

(a) = p[S_{1} ⊗ S′_{1}](expand_{θ_{1}}[S_{1}][S′_{1}]a_{1})[S_{2}]a_{2} [s, s_{1}, s′_{1}, s_{2}]

(b) = (expand_{θ_{2}→comm}[S ⊗ S_{1}][S′_{1}](p[S_{1}]a_{1}))[S_{2}]a_{2} [s, s_{1}, s′_{1}, s_{2}]

for all S_{2}, [s, s_{1}, s′_{1}, s_{2}] ^{∈} S ⊗ S_{1} ⊗ S′_{1} ⊗ S_{2}, a_{1} ^{∈} θ_{1}^{∘}S_{1} and a_{2} ^{∈} θ_{2}^{∘}S_{2}. It is crucial here that a_{2} lives in store shape S_{2}, which is separate from the S′_{1} component; this allows us to use a relation that fixes S′_{1} below.

By the definition of expand for procedure types, (b) is equal to

(c) = [q, q_{1}, s′_{1}, q_{2}], where p[S_{1}]a_{1}[S_{2}]a_{2}[s, s_{1}, s_{2}] = [q, q_{1}, q_{2}].

Let R : S_{1} ⊗ S′_{1} ↔ S_{1} be the relation that fixes s′_{1}, i.e. it contains ⟨⊥, ⊥⟩ and all pairs ⟨[x, s′_{1}], x⟩ where x ≠ ⊥. By the Identity Extension property (a special case of the Isomorphism Functoriality Lemma) we know that

(d) ⟨a_{1}, a_{1}⟩ ^{∈} θ_{1}^{∘}Δ_{S_{1}} and ⟨a_{2}, a_{2}⟩ ^{∈} θ_{2}^{∘}Δ_{S_{2}}.

Further, we claim that

(e) ⟨(expand_{θ_{1}}[S_{1}][S′_{1}]a_{1}), a_{1}⟩ ^{∈} θ_{1}^{∘}R.

Postponing the proof of (e) for a moment, (d), (e), and parametricity of p imply that (a) and [q, q_{1}, q_{2}] are Δ_{S} ⊗ R ⊗ Δ_{S_{2}}-related, and hence by the definition of R that (a)=(c). Since (b)=(c) we obtain the desired result (a)=(b).

Property (e) follows from parametricity of expand_{θ_{1}} : ∀β∀γ. θ_{1}^{∘}β−∘ θ_{1}^{∘}(β ⊗ γ). Specifically, we noted ⟨a_{1}, a_{1}⟩ ^{∈} θ_{1}^{∘}Δ_{S_{1}} in (d), and taking R′ : S′_{1} ↔ I as the relation containing ⟨⊥, ⊥⟩ and ⟨s′_{1}, ⊥⟩, we obtain

(f) ⟨(expand_{θ_{1}}[S_{1}][S′_{1}]a_{1}), (expand_{θ_{1}}[S_{1}][I]a_{1})⟩ ^{∈} θ_{1}^{∘}(Δ_{S_{1}} ⊗ R′).

Now, R is equal to the composition of Δ_{1} ⊗ R′ : S_{1} ⊗ S′_{1} ↔ S_{1} ⊗ I with the canonical isomorphism S_{1} ⊗ I ↔ S_{1}. We can then use Isomorphism Functoriality and parametricity of expand_{θ_{1}} once more (with respect to this canonical isomorphism) to obtain (e) from (f).

Similarly, we can show that the interpretation

x_{1} : θ_{1}^{∘}α_{1}, …, x_{m} : θ_{m}^{∘}α_{m} ⊢ M^{∘}(α_{1}, …, α_{n}) : θ^{∘}(α_{1} ⊗ ⋯ ⊗ α_{m}).

of a judgement satisfies a naturality property corresponding to Definition 9.

9.2 Idealized Algol

The proof of the Naturality Theorem for SCI relies on the simpler interpretation of function types, where the state for procedures and arguments is separate. In Idealized Algol, we have only been able to verify the corresponding result for types of a specific form.

Theorem 12. (Naturality Theorem for Idealized Algol) If φ is a primitive type then any p ^{∈} (θ_{1} → φ)^{⋆}S is natural with respect to expansions:

[figure: θ_{1}^{⋆}(S ⊗ S_{1}); θ_{1}^{⋆}(S ⊗ S_{1} ⊗ S′_{1}); φ^{⋆}(S ⊗ S_{1}); φ^{⋆}(S ⊗ S_{1} ⊗ S′_{1}); expand_{θ_{1}}[S ⊗ S_{1}][S′_{1}]; p[S_{1}]; p[S_{1} ⊗ S′_{1}]; expand_{φ}[S ⊗ S_{1}][S′_{1}]]

(where we have elided canonical isomorphisms (S ⊗ S_{1}) ⊗ S′_{1} ↔ S ⊗ (S_{1} ⊗ S′_{1})).

The proof can follow the proof of Naturality Theorem in [O’Hearn and Tennent 1995], and is essentially similar to the case of θ → φ in the proof of Naturality for SCI. The reason that the SCI proof does not generalize can be seen in the case θ_{1} → θ_{2} → comm. In Idealized Algol the application p[S_{1} ⊗ S′_{1}](expand[S_{1}][S_{2}]a_{1})[S_{2}]a_{2} uses an element a_{2} ^{∈} θ_{2}^{⋆}(S ⊗ S_{1} ⊗ S′_{1} ⊗ S_{2}) that can change members of S′_{1}, thus preventing the use of a relation that fixes the S′_{1} component in the proof.

In [O’Hearn and Tennent 1995], Section 9, there was a counterexample to “parametricity implies naturality,” which showed that this result failed to hold with φ replaced by arbitrary θ. But the counterexample there used Weakening and Contraction and does not exist in the strict parametricity model. As a result, using the representation in the Resumption Theorem in Section 10.1, we have been able to slightly extend Theorem 12 to cases where φ is replaced by a first-order type φ_{1} × ⋯ × φ_{n} → φ. The question of whether it holds for all types remains open.

Naturality is important, e.g., for proving the isomorphism θ_{1} × θ_{2} → θ_{3} ≅ θ_{1} → θ_{2} → θ_{3} that is characteristic of Cartesian closed categories. So, even though we have the adequacy result above, we have not verified the indicated CCC isomorphism at higher types in Idealized Algol.

Interesting though the open question may be, it does not pose a fundamental problem for our semantics, as it can be dealt with in at least two ways. First, every Idealized Algol type can be converted to a “canonical form” of a product of types of the form θ → φ, and we could simply use an uncurried presentation of the semantics of types (as in [O’Hearn and Tennent 1995], Section 2). The second option is to add naturality as an explicit additional requirement (as in [O’Hearn and Tennent 1995], Section 7). In either case, we get an interpretation of Idealized Algol using CCC structure, and satisfying all the laws of the typed λ-calculus. Since these two alternatives are thoroughly examined in [O’Hearn and Tennent 1995], the details do not bear repeating here. Instead, we choose to carry working on with the translation (·)^{⋆} as defined (which we have seen satisfies an adequacy property), and simply note that the naturality properties that we can verify are sufficient to support the technical results that we shall prove about low-order types. To this end, we finish this section with some technical lemmas that will be needed later, in Section 10.3.

9.3 Technical Lemmas

We now prove some technical lemmas that will be used to help produce a distinguishing context during the proof of full abstraction in the next section; the reader may wish to move on and refer back to these lemmas as necessary.

The first lemma reduces the domain approximation p ⊑ q between certain polymorphic functions to the ordering p[N_{⊥}] ⊑ q[N_{⊥}] of their instantiations to N_{⊥}. This is one of the steps which enables us to use a single local variable, which lives in store shape N_{⊥}, to produce a distinguishing context.

The use of I in the lemma corresponds, semantically, to meanings for closed terms of the indicated type.

Lemma 13. If p, q ^{∈} θ^{⋆}I, where θ = (φ_{1} × ⋯ × φ_{n} → φ) → φ′, then p ⊑ q iff p[N_{⊥}] ⊑ q[N_{⊥}].

Proof: The only if part is immediate. For the if part, consider any countable, flat cpo S, and suppose p[N_{⊥}] ⊑ q[N_{⊥}]. We must show p[S] ⊑ q[S] for arbitrary S. If S is {⊥} then the result is trivial. Otherwise, first note that N_{⊥} and S ⊗ N_{⊥} are isomorphic, since both are countably infinite and flat. Using the Isomorphism Functoriality Lemma and parametricity we infer p[S ⊗ N_{⊥}] ⊑ q[S ⊗ N_{⊥}]. We know that p and q are natural with respect to expansions by Theorem 12, and so we can then show that p[S] ⊑ q[S] using naturality with respect to the expansion S−∘ S ⊗ N_{⊥} and the easy fact that expansion maps expand_{φ′}[S_{1}][S_{2}] reflect order for primitive types φ′.

The next lemma refers to the logical relation R between (·)^{⋆} and O[[·]] defined in Section 8.1.

Lemma 14. If θ = (φ_{1} × ⋯ × φ_{n} → φ) → φ′ then the opposite of relation R_{θ}^{X} is single-valued: if pR_{θ}^{X}m and p′R_{θ}^{X}m then p = p′.

The point of this result is that, at first order types, the relationship between the two models can be described by a partial function; an element in the Oles model can correspond to at most one element in the parametricity model (which is more constrained).

Proof: Assume the antecedent. By Theorem 12 we have an injection

i : ((φ_{1} × ⋯ × φ_{n}) → φ)^{⋆}(X × W)_{⊥} ↪ O[[(φ_{1} × ⋯ × φ_{n}) → φ]](X × W),

and it is clear that if q ^{∈} ((φ_{1} ×⋯×φ_{n}) → φ)^{⋆}(X ×W)_{⊥} then qR_{φ_{1}×···×φ_{n}→φ}^{X×W}(iq). By the logical relation property for p and p′ this means that

(p[W]q)R_{φ′}^{X×W} (m[W](iq)) and (p′[W]q)R_{φ′}^{X×W} (m[W](iq)).

But the logical relation R_{φ′}^{X×W} at primitive type is an equality relation. Thus, we have shown that p[W]q = p′[W]q for arbitrary W and q, so p = p′.

Lemma 15. If ⊢ M : θ, where θ = (φ_{1} × ⋯ × φ_{n} → φ) → φ′, then M is natural:

[figure: I; I; θ^{⋆}S; θ^{⋆}(S ⊗ S′); id; M^{⋆}S; M^{⋆}(S ⊗ S′); expand_{θ}[S][S′]]

Proof: Let S = X_{⊥} and S′ = X′_{⊥}. From Lemma 7 we know that

(M^{⋆}X_{⊥}∗)R_{θ}^{X}(O[[M]]X∗) and (M^{⋆}(X × X′)_{⊥}∗)R_{θ}^{X×X′}(O[[M]](X × X′)∗).

By Expansion Relatedness (Lemma 6),

(expand_{θ}[S][S′](M^{⋆}X_{⊥}∗))R_{θ}^{X×X′}(O[[θ]] e (O[[M]]X∗)),

where e : X → X × X′ is the expansion. Further, by naturality of O[[M]] we know

O[[θ]] e (O[[M]]X∗) = O[[M]](X × X′) ∗ .

Naturality follows from these facts together with Lemma 14 and the standard isomorphism (X × X′)_{⊥} ≅ S ⊗ S′.

The order ⊑ on p and q in Lemma 13 is determined pointwise. Likewise, any derivable judgement Γ ⊢ M : θ in Idealized Algol determines a family of maps M^{⋆}(–) : Γ^{⋆}(–)−∘ θ^{⋆}(–) in the strict parametricity model, which we also order pointwise.

Lemma 16. If ⊢ M, N : θ, where θ = (φ_{1} × ⋯ × φ_{n} → φ) → φ′, then

M^{⋆} ⊑ N^{⋆} iff M^{⋆}I ⊑ N^{⋆}I.

Proof: The only if part is immediate from the pointwise order for ⊑. For the if part, if M^{⋆}I ⊑ N^{⋆}I we get M^{⋆}(I ⊗ S) ⊑ N^{⋆}(I ⊗ S) from naturality (Lemma 15), and then M^{⋆}S ⊑ N^{⋆}S using the Isomorphism Functoriality Lemma (Section 6) with the isomorphism S ↔ I ⊗ S.

10. RESUMPTIONS AND IDEALIZED ALGOL

In this section we show that the meanings of first-order types in our model of Idealized Algol may be characterized using domain equations for resumptions. The proof of this result goes by a parametricity argument which characterises the elements of these types exactly. Using this characterization, we derive a full abstraction result for closed terms of second-order type.

We have already seen in Section 7.3 that such representation results do not go through in our model of SCI.

10.1 A Representation Theorem

The domain equation we give will need to deal with a number of different capabilities for the primitive types, and it will help to look at some instances of it before giving the general equation.

To begin, (comm → comm)^{⋆}S is an initial solution of the familiar domain equation for deterministic resumptions [Plotkin 1983]:

D ≅ S−∘ (S ⊕ (S ⊗ D)),

where S is a flat cpo and ⊕ is coalesced sum. Using this domain equation we understand a procedure of type comm → comm as follows. A procedure with a command argument begins by possibly changing the state. It then either terminates or resumes. Resuming causes the argument to be evaluated once, with the state resulting from this evaluation fed through as an argument to the resumed procedure.

For expressions we augment deterministic resumptions with input and output capabilities. The equation for exp → exp is

D ≅ S−∘ ((S ⊗ N_{⊥}) ⊕ (S ⊗ (N_{⊥}−∘ D))).

This equation allows for an output value in the component S ⊗ N_{⊥} for the final value of execution of the resumption, and an input value in N_{⊥}−∘ D that is obtained from evaluating the input expression once.

For acceptors to the left of → consider a procedure p : acc → comm. A procedure call p(a) is a command which may assign a number of values to a during its evaluation. The appropriate domain equation is the one for comm → comm, augmented with natural number values to be supplied to the input acceptor on resumption:

D ≅ S−∘ (S ⊕ (S ⊗ D ⊗ N_{⊥})).

For acceptors to the right of → consider a procedure p : acc → acc. A procedure call p(a) is an acceptor, so that it accepts a natural number value and then behaves like a command, during evaluation of which a can be used a number of times. Accordingly, (acc → acc)^{⋆}S is isomorphic to N_{⊥}−∘ D, where D is the domain just given for acc → comm.

This treatment of acceptors can in fact be regarded as being derived from a view of acc as an infinite product of comm; semantically, acc^{⋆}S is isomorphic to an infinite product (comm^{⋆}S)^{N}. For acceptors to the right of →, the domain N_{⊥}−∘ D is isomorphic to the infinite product D^{N}. To the left of → the term S ⊗ D ⊗ N_{⊥} in the domain equation can be isomorphically rewritten to Σ_{i^{∈}N}S ⊗ D, for Σ the coalesced sum: Below we will use summation in this way to account for explicit product types to the left of →.

To formulate the general equation, for each primitive type φ we define functors φ^{in}, φ^{arg} and and φ^{res} (for input, argument, and result) on the category of cpo’s and strict continuous functions:

exp^{in} = (–)  exp^{arg} = N_{⊥}−∘ (–) exp^{res} = (–) ⊗ N_{⊥}
acc^{in} = N_{⊥}−∘ (–) acc^{arg} = (–) ⊗ N_{⊥} acc^{res} = (–)
comm^{in} = (–).  comm^{arg} = (–)  comm^{res} = (–)

Now we add the capability to choose among multiple arguments to the domain equations above.

Theorem 17. (Resumption Theorem) If φ_{1}, ..., φ_{n}, φ are primitive Idealized Algol types and S a countable flat cpo, then

(φ_{1} × ⋯ × φ_{n} → φ)^{⋆}S

is isomorphic to φ^{in}(D), where D is an initial solution of the domain equation

D ≅ S−∘ (φ^{res}(S) ⊕ (S ⊗ (Σ_{i=1}^{n}φ_{i}^{arg}(D)))),

where ⊕ and Σ are coalesced sum.

The summation over i ^{∈} 1, ..., n here corresponds to a strong form of sequentiality where a resumption must choose a specific i, which causes the i’th argument to be evaluated before resuming. This is analogous to strategies for picking sequentiality indices in sequential algorithms [Berry and Curien 1982]: In contrast, Kahn-Plotkin sequential functions require mere existence of a sequentiality index, and as a result are less distinguishing than the stronger form of sequentiality found in Idealized Algol. The weaker sequential-function form of sequentiality is closer to functions in SCI, where non-interference leads to less dependence on evaluation order than in Idealized Algol. (So the parallelism in SCI is reminiscent of independence from evaluation order in PCF, and appears to be actually sequential in this weaker sense of sequentiality.)

The proof of the Resumption Theorem is lengthy, and we give it separately in the following subsection. In describing the proof we have attempted to isolate the more conceptual part, the parametricity argument, from the technical development needed to apply the argument to verify the theorem.

10.2 Proof of the Theorem

To keep the notation simple we give the proof for the type exp×exp → exp. This requires us to address the most important issues raised by the domain equation, including multiple arguments and possibly non-trivial input and output values. The proof for more or fewer than two arguments involving comm or exp is a straight notational reworking of what follows, and acc requires only minor modifications (recall the remarks about acc as a infinite product of comm above).

The relevant cpo in the strict parametricity model is

Z = ∀β. (S ⊗ β−∘ S ⊗ β ⊗ nat)&(S ⊗ β−∘ S ⊗ β ⊗ nat)
→ (S ⊗ β−∘ S ⊗ β ⊗ nat).

Let D be an initial solution of the equation D ≅ T D, where T is the following functor on the category of cpo’s and strict continuous functions:

T (–) = S−∘ S ⊗ (N_{⊥} ⊕ (N_{⊥}−∘ (–)) ⊕ (N_{⊥}−∘ (–))).

(The functor S−∘ ((S⊗N_{⊥})⊕(S⊗Σ_{i=1}^{2}(N_{⊥}−∘ (–)))) is explicitly given by the statement of the theorem, but it is isomorphic to T, which is obtained by distributing ⊕ over ⊗.)

Our aim is to show that Z and D are isomorphic. To do this, we proceed in four steps. First, we describe the structure of D. This is straightforward, and follows from standard material on recursive domain equations [Plotkin 1983; Abramsky and Jung 1994]. Second, we give the parametricity argument, which relates uses of polymorphic functions to the structure described in the first step. Steps three and four consist of technical results, which use the information from the first two steps to verify that D and Z are isomorphic.

Step 1: Structure of D.

From the solution of domain equations by the inverse limit construction [Plotkin 1983; Abramsky and Jung 1994], we know that D is a bounded complete, algebraic cpo. As a result, any element is the lub of the finite elements beneath it. The first step needed for relating D to Z is to describe this structure explicitly. We do this using step functions. If E is a flat cpo, F is bounded complete and algebraic, e ^{∈} E is not ⊥, and f ^{∈} F is finite, then the step function e ↘ f : E−∘ F is such that

(e ↘ f)e′ = \{ \begin{matrix}f & if e = e′ \\ ⊥ & otherwise. \end{matrix}

The domain D can be described using special finite elements, the atoms. Recall that an atom a in a cpo is an element just above ⊥, i.e. a ≠ ⊥ and ∀b. b ⊑ a ⟹ b = a ∨ b = ⊥. The atoms a ^{∈} D can be generated using step functions as follows:

a ::= s ↘ [s′, e] (⊥ ≠ s, s′ ^{∈} S)
e ::= n | 1 : n ↘ a | 2 : n ↘ a (n ^{∈} N)

Here, we use n, 1 : n ↘ a and 2 : n ↘ a to indicate elements in respective components of the coproduct N_{⊥} ⊕ N_{⊥}−∘ D ⊕ N_{⊥}−∘ D. We will follow the usual practice of suppressing isomorphisms between D and T D. For instance, s ↘ [s′, n] is, strictly speaking, an element of T D, which we could coerce to D using an isomorphism.

It is not difficult to verify that each element a generated by this grammar is indeed an atom, and also that this exhausts the atoms of D. The role of the atoms in D is summed up by the following lemma.

Lemma 18. D is isomorphic to {A ⊆ D | A is a pairwise-consistent set of atoms}, ordered by subset inclusion. (That is, D is a coherence space.)

Here, two elements are said to be consistent when they have an upper bound. The lemma can be shown using a routine calculation with the inverse limit construction.

Step 2: The Parametricity Argument.

The essential part of the proof is the following use of parametricity. Suppose p ^{∈} Z, E is a flat cpo, c_{1}, c_{2} : S ⊗ E−∘ S ⊗ E ⊗ N_{⊥} and p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] = [s′_{0}, e′_{0}, n′] ≠ ⊥. We identify an element of D that tracks the calls of c_{1} and c_{2}.

Let L be the flat cpo whose non-⊥ elements are lists of elements drawn from the set coproduct S′ + N + N, where S′ is the set of non-⊥ elements of S. We use s, 1 : n, and 2 : n, with subscripts or superscripts, to range over components of the coproduct. Define R : L ↔ E to be the smallest strict relation such that

(s_{0})Re_{0} c_{i}[s, e] = [s′, e′, n] ≠ ⊥ and ℓRe ⟹ (ℓ, s, s′, i : n)Re′.

The initial and final values of the state on a use of c_{i}[s, e], together with component i (which is 1 or 2) and produced value n, are recorded in (ℓ, s, s′, i : n). (We are using a comma for appending an element to a list.) R is single-valued and determines a function f_{R} : L−∘ E, where f_{R}ℓ = e if ℓRe, and f_{R}ℓ = ⊥ if there is no e such that ℓRe. For i equal to 1 or 2, define c_{i}^{∗} : S ⊗ L−∘ S ⊗ L ⊗ N_{⊥} to be the function where

c_{i}^{∗}[s, ℓ] = let [s′, e, n] be c_{i}[s, f_{R}ℓ] in [s′, (ℓ, s, s′, i : n), n].

This definition is such that

⟨(s_{0}), e_{0}⟩ ^{∈} R ∧ ⟨c_{i}^{∗}, c_{i}⟩ ^{∈} Δ_{S} ⊗ R−∘ Δ_{S} ⊗ R ⊗ Δ_{N_{⊥}}.

Parametricity of p then implies that

⟨ p[L]⟨c_{1}^{∗}, c_{2}^{∗}⟩[s_{0}, (s_{0})] , p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}]⟩ ^{∈} Δ_{S} ⊗ R ⊗ Δ_{N_{⊥}}.

By the definition of R, this means p[L]⟨c_{1}^{∗}, c_{2}^{∗}⟩[s_{0}, (s_{0})] ≠ ⊥. Further, the use of Δ_{S} ⊗ R ⊗ Δ_{N_{⊥}} implies that p[L]⟨c_{1}^{∗}, c_{2}^{∗}⟩[s_{0}, (s_{0})] ^{∈} S ⊗ L ⊗ N_{⊥} is of the form

[s′_{0}, (s_{0}, s_{1}, s′_{1}, i_{1} : n_{1}, ..., s_{k}, s′_{k}, i_{k} : n_{k}), n′]

for some, possibly empty, list s_{1}, s′_{1}, i_{1} : n_{1}..., s_{k}, s′_{k}, i_{k} : n_{k} (here s′_{0} and n′ are the final values in p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] = [s′_{0}, e′_{0}, n′]). From this we can read off the behaviour of p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] as a sequence of calls to c_{1} and c_{2}, together with initial and final states and values produced when each call was made.

This determines an atom

s_{0} ↘ [s_{1}, i_{1} : (n_{1} ↘ (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ (s′_{k} ↘ [s′_{0}, n′]))] ⋯))]

in D, which we denote by a(E, p, c_{1}, c_{2}, s_{0}, e_{0}). The logical relation argument we have just given is a recipe for obtaining a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) from appropriately typed E, p, c_{1}, c_{2}, s_{0}, e_{0}, as long as p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] ≠ ⊥.

This completes the most important part of the proof. The remainder of the section consists of technical lemmas, showing how this way of generating atoms in D from elements of Z can be used to establish an isomorphism between D and Z.

Step 3: From D to Z.

We obtain a map from D to Z using the fact that there is an initial T -algebra T D →^{h_{D}} D, the structure map h_{D} of which is an isomorphism [Abramsky and Jung 1994]. Initiality implies that there is a (unique) strict continuous function ψ : D → Z making

[figure: T D; D; T Z; Z; h_{D}; T ψ; ψ; h_{Z}]

commute, where the T -algebra structure map T Z →^{h_{Z}} Z is as follows:

h_{Z} = λp ^{∈} T Z Λβ λ⟨c_{1}, c_{2}⟩ : (S ⊗ β−∘ S ⊗ β ⊗ nat)&(S ⊗ β−∘ S ⊗ β ⊗ nat)

\underline{λ}[s, b] : S ⊗ β
let [s′, x] be p s in
case x of
n ↦ [s′, b, n]
1 : f ↦ (let [s′′, b′, n] be c_{1}[s′, b] in (f n)[β]⟨c_{1}, c_{2}⟩[s′′, b′])
2 : g ↦ (let [s′′, b′, n] be c_{2}[s′, b] in (g n)[β]⟨c_{1}, c_{2}⟩[s′′, b′]).

We are using polymorphic λ-calculus notation as a convenient way of defining elements of Z in a way that makes the satisfaction of parametricity conditions obvious. The case construct is used to branch on coproduct components, where n, (1 : f), and (2 : g) range over components of N_{⊥} ⊕ (N_{⊥}−∘ E) ⊕ (N_{⊥}−∘ E). Note that the use of case is not a problem for parametricity because we are not branching on anything we are required to be parametric in.

The map ψ can be obtained from general considerations ([Abramsky and Jung 1994], Lemma 5.3.1) as a least fixed-point:

ψ = μg. (h_{D}^{−1}; T (g); h_{Z}).

For concreteness, it will be useful to spell out the action of ψ on atoms. Consider an atom

a = s_{0} ↘ [s_{1}, i_{1} : (n_{1} ↘ (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ s′_{k} ↘ [s′_{0}, n′])] ⋯))]

in D. Then we define the polymorphic function ψ(a) ^{∈} Z by induction on the size of a. The base case is for atoms of the form s_{0} ↘ [s′_{0}, n′], and ψ(a) is then the function

Λβ. λ⟨c_{1}, c_{2}⟩. \underline{λ}[s, b]. if (s = s_{0}) then [s′_{0}, b, n′] else ⊥.

For the induction case, suppose that we know the polymorphic function ψ(a′) corresponding to the atom

a′ = (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ s′_{k} ↘ [s′_{0}, n′])] ⋯).

Then ψ(a) is

Λβ. λ⟨c_{1}, c_{2}⟩. \underline{λ}[s, b].
if (s = s_{0}) then
(let [s′, b′, n] = c_{i_{1}}[s_{1}, b] in
if n = n_{1} then ψ(a′)[β]⟨c_{1}, c_{2}⟩[s′, b′] else ⊥)
else ⊥.

It is not difficult to see that this description is consistent with the abstract definition of ψ as a least fixed-point.

From Lemma 18 we know that D is determined by its atoms, and consistency between them. A key point is that ψ respects this consistency structure.

Lemma 19. (1) If ψd and ψd′ are consistent in Z then d and d′ are consistent in D.

(2) ψ reflects order: ψd ⊑ ψd′ ⟹ d ⊑ d′.

Proof: For part (1) of the lemma, by Lemma 18 it suffices to prove the result for atoms only. From the description of atoms in D it is clear that, if d and d′ are inconsistent, then we must have a situation in which

\begin{aligned}d & = & s_{0} ↘ [s_{1}, i_{1} : (n_{1} ↘ (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ s′_{k} ↘ [q, e])] ⋯))] \\ d′ & = & s_{0} ↘ [s_{1}, i_{1} : (n_{1} ↘ (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ s′_{k} ↘ [q′, e′])] ⋯))] \end{aligned}

where one of three cases must be true:

(1) e = m and e′ = n are in the first component, and m ≠ n,

(2) q ≠ q′, or

(3) e and e′ are in different components.

For each case it is straightforward to find arguments E, c_{1}, c_{2} and e_{0} such that (ψ d)[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] and (ψ d′)[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] are unequal and non-⊥. For instance, in the first case we can choose E = N_{⊥}, e_{0} = 0, and for y equal to 1 or 2 define c_{y} to be the least function such that c_{y}[s_{j}, j − 1] = [s′_{j}, j, n_{j}], for 1 < j < k. A routine calculation with the definition of ψ shows that (ψ d)[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] and (ψ d′)[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] are inconsistent. The other two cases are similar.

Part (2) of the lemma can also be shown straightforwardly by proving the contrapositive, constructing arguments that show ψd ⋢ ψd′ when d ⋢ d′.

From part (2) of this result it follows that ψ is an an injection that preserves and reflects order, so that D “sits inside” Z. The next result sets the stage for the proof that ψ is bijective; it shows that the behaviour of any polymorphic function p ^{∈} Z is completely determined by elements of the form ψ(a) lying below it, for a an atom of D.

Lemma 20. (1) ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[E]c[s_{0}, e_{0}] = p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}]

(2) ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0})) ⊑ p.

Proof: (1) follows straightforwardly from the relational parametricity property for ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0})), with the relation R used to define a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) above. For (2) we need more work because we must consider cpo’s other than E. That is, we must show the following for every flat cpo B:

(a) If ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[B]⟨h_{1}, h_{2}⟩[q_{0}, b_{0}] = [q′_{0}, b′_{0}] ≠ ⊥ then p[B]⟨h_{1}, h_{2}⟩[q_{0}, b_{0}] = [q′_{0}, b′_{0}].

Fix B and assume the antecedent of (a). Note that we must have s_{0} = q_{0}, or else we would have ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[B]⟨h_{1}, h_{2}⟩[q_{0}, b_{0}] = ⊥.

Let L and R : L ↔ E be as in the parametricity argument that defined the atom a(E, p, c_{1}, c_{2}, s_{0}, e_{0}), and define Q : L ↔ B as the least strict relation such that

(s_{0})Qb_{0} h_{i}[q, e] = [q′, b′, n] ≠ ⊥ ∧ ℓQb ⇒ (ℓ, q, q′, i : n)Qb′.

46 · P.W. O’Hearn and J.C. Reynolds

We define f_{Q} and h_{i}^{∗} similarly to f_{R} and c_{i}^{∗}. Again we have

⟨(s_{0}), b_{0}⟩ ^{∈} Q ∧ ⟨h_{i}^{∗}, h_{i}⟩ ^{∈} Δ_{S} ⊗ Q−∘ Δ_{S} ⊗ Q ⊗ Δ_{N_{⊥}}, so, by parametricity (remembering s_{0} = q_{0}) we obtain

(b) ⟨ p[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})] , p[B]⟨h_{1}, h_{2}⟩[s_{0}, b_{0}]⟩ ^{∈} Δ_{S} ⊗ Q ⊗ Δ_{N_{⊥}}, and

(c) ⟨ ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})],

ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[B]⟨h_{1}, h_{2}⟩[s_{0}, b_{0}]⟩ ^{∈} Δ_{S} ⊗ Q ⊗ Δ_{N_{⊥}}. Then (b) and (c) imply, since Q is single-valued, that to prove (a) it suffices to show

(d) ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})] = p[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})].

Now, the atom a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) must be of the form

s_{0} ↘ [s_{1}, i_{1} : (n_{1} ↘ (s′_{1} ↘ ⋯ [s_{k}, i_{k} : (n_{k} ↘ s′_{k} ↘ [s′_{0}, n′])] ⋯))].

Fixing k, for each 0 ≤ j ≤ k define

ℓ_{j} = (s_{0}, s_{1}, s′_{1}, i_{1} : n_{1}..., s_{j}, s′_{j}, i_{j} : n_{j}),

and, for i equal to 1 or 2, define c_{i}^{min} to be the function where

c_{i}^{min}[s_{j}, ℓ_{j−1}] = [s′_{j}, ℓ_{j}, n_{j}], for 1 ≤ j ≤ k, and c_{i}^{min}[s, ℓ] = ⊥ in all other cases. Define U : L ↔ L to be the relation containing ⟨⊥, ⊥⟩, all pairs ⟨ℓ_{j}, ℓ_{j}⟩ for 0 ≤ j ≤ k, and ⟨⊥, ℓ⟩ for all ℓ’s whose length is greater than 3k + 1 (which is the length of ℓ_{k}).

Intuitively, c_{i}^{min} is like c_{i}^{∗}, except that it is just defined enough to enable the polymorphic application p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] to be non-⊥.

More formally, it is easy to see that

⟨c_{i}^{min}, c_{i}^{∗}⟩ ^{∈} Δ_{S} ⊗ U−∘ Δ_{S} ⊗ U ⊗ Δ_{N_{⊥}}, and parametricity then implies

⟨ p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] , p[L]⟨c_{1}^{∗}, c_{2}^{∗}⟩[s_{0}, (s_{0})]⟩ ^{∈} Δ_{S} ⊗ U ⊗ Δ_{N_{⊥}}. We know from the parametricity argument that defined a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) that

p[L]⟨c_{1}^{∗}, c_{2}^{∗}⟩[s_{0}, (s_{0})] = [s′_{0}, ℓ_{k}, n′]. Further, the definition of U implies that

if ⟨ℓ, ℓ_{k}⟩ ^{∈} U then ℓ = ℓ_{k}, so we may conclude that

p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] = [s′_{0}, ℓ_{k}, n′]. In particular, it is not ⊥.

Next, we claim

(e) ⟨c_{i}^{min}, h_{i}^{∗}⟩ ^{∈} Δ_{S} ⊗ U−∘ Δ_{S} ⊗ U ⊗ Δ_{N_{⊥}}.

To see why (e) must hold, consider how c_{i}^{min} is defined in terms of the atom. If (e) did not hold then we would have

ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})] = ⊥,

and that cannot be the case because, by (c) and the definition of Q, it would contradict the assumed antecedent of (a).

From (e) and parametricity of p we obtain

⟨ p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] , p[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})]⟩ ^{∈} Δ_{S} ⊗ U ⊗ Δ_{N_{⊥}}.

By the definition of U and the fact, shown above, that p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] ≠ ⊥, this implies

(f) p[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] = p[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})].

By a similar (but easier) argument, parametricity of ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0})) with respect to U implies

(g) ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[L]⟨c_{1}^{min}, c_{2}^{min}⟩[s_{0}, (s_{0})] = ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0}))[L]⟨h_{1}^{∗}, h_{2}^{∗}⟩[s_{0}, (s_{0})].

The desired result (d) follows directly from (f) and (g).

Step 4: From Z to D.

Finally, we define the inverse map κ : Z → D:

κ p = ⨆{a ^{∈} D | ψa ⊑ p and a is an atom}.

Lemma 21. κ is well-defined.

Proof: If ψd, ψd′ ⊑ p then d and d′ are consistent by Lemma 19(1). Thus, the set {a ^{∈} D | ψa ⊑ p and a is an atom} is pairwise consistent, and by Lemma 18 its lub exists.

This shows that κ is a function but we do not, as yet, claim that it is continuous.

Lemma 22. κψd = d.

Proof:

κψd = ⨆{a ^{∈} D | ψa ⊑ ψd and a is an atom}  (definition)
= ⨆{a ^{∈} D | a ⊑ d and a is an atom} (Lemma 19(2))
= d  (Lemma 18)

Lemma 23. ψκp = p.

Proof: Certainly we have ψκp ⊑ p by the definition of κ. Conversely, suppose that p[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] = [s′_{0}, e′_{0}] and consider a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) ^{∈} D. We know from Lemma 20(1) that ψ(a(E, p, c_{1}, c_{2}, s_{0}, e_{0})) ⊑ p, and since, by definition, a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) is an atom in D, the inequality a(E, p, c_{1}, c_{2}, s_{0}, e_{0}) ⊑ ψκp follows from the definition of κ. This and Lemma 20(2) imply the desired equality (ψκp)[E]⟨c_{1}, c_{2}⟩[s_{0}, e_{0}] = [s′_{0}, e′_{0}], and we are done.

To prove the Resumption Theorem, note that in the specific category of cpo’s and strict continuous functions any order-reflecting bijection is an isomorphism. Lemmas 22 and 23 show that ψ is a bijection, so by Lemma 19 we conclude that it is an isomorphism (and we can finally infer that κ is continuous).

This Concludes the Proof of the Resumption Theorem

After all this work it is reasonable to ask if Theorem 17 could be seen as an instance of a more general result about relational parametricity in linear type theory. In suitably parametric models of (intuitionistic) polymorphic λ-calculus types of the form ∀α. (T α → α) → α denote initial T -algebras, and this paves the way for a characterization of all second-order types in prenex form. Plotkin [1993] in lectures has indicated that the corresponding property in linear polymorphic type theory is that ∀α. (T α−∘ α) → α denotes an initial T -algebra, for covariant functors T on a “linear” category where morphisms correspond to terms of −∘ type. It is not immediately obvious that this implies our result because our translations of first-order Idealized Algol types have quite a different form. Further, in contrast to intuitionistic type theory the mixing of intuitionistic and linear facilities blocks an evident reduction of these and other low order types to the form ∀α. (T α−∘ α) → α. Finally, note that the map κ in the proof, which essentially gives (weak) initiality, was defined using details about the structure of solutions of domain equations in the category of cpo’s and strict continuous functions.

10.3 A Full Abstraction Result

We know from the Resumption Theorem that the first-order types have algebraic cpo structure. We show that the finite elements are definable in a suitable sense. (This is related, but not identical, to the argument in [O’Hearn and Reddy 1999], Proposition 5.2.)

Let v_{N_{⊥}} ^{∈} var^{⋆}N_{⊥} be the evident variable that directly updates and reads from N_{⊥}. It can be obtained from the standard variable v[I] ^{∈} var^{⋆}(I ⊗ N_{⊥}) using the canonical isomorphism I ⊗ N_{⊥} ↔ N_{⊥}.

Lemma 24. (Definability Lemma) If φ_{1}, ..., φ_{n}, φ are primitive Algol types then every finite element d of (φ_{1} × ⋯ φ_{n} → φ)^{⋆}N_{⊥} is definable by an Idealized Algol term

x : var ⊢ M_{d} : φ_{1} × ⋯ φ_{n} → φ,

in the sense that

(M_{d}^{⋆}N_{⊥}) v_{N_{⊥}} = d

in the strict parametricity model.

In this result (M_{d}^{⋆}N_{⊥}) is a map of type var^{⋆}N_{⊥}−∘ (φ_{1} × ⋯ φ_{n} → φ)^{⋆}N_{⊥}. The standard variable v_{N_{⊥}} for updating N_{⊥} is given as the only component in the environment, and is denoted by x in (M_{d}^{⋆}N_{⊥}) v_{N_{⊥}}.

Proof: Again we concentrate on exp × exp → exp. It is standard that the finite elements d in the resumption domain can be generated as follows.

d ::= (s_{1} ↘ [s′_{1}, e_{1}]) ⊔ ⋯ ⊔ (s_{k} ↘ [s′_{k}, e_{k}])

(where s_{i}, s′_{i} ^{∈} N, s_{1}, ..., s_{k} are all distinct)

e ::= n | i : (n_{1} ↘ d_{1}) ⊔ ⋯ ⊔ (n_{m} ↘ d_{m})

(where all n_{j} ^{∈} N are distinct, and i = 1 or 2)

We define terms N_{d}, F_{e} by induction on d and e, where

x : var, c_{1} : exp, c_{2} : exp ⊢ N_{d} : exp
x : var, c_{1} : exp, c_{2} : exp ⊢ F_{e} : exp.

N_{d} is defined by

N_{(s_{1}↘[s′_{1},e_{1}])⊔···⊔(s_{k}↘[s′_{k},e_{k}])} = if x = s_{1} then x := s′_{1}; F_{e_{1}}

⋮

else if x = s_{k} then x := s′_{k}; F_{e_{k}} else Ω.

F_{e} is defined according to the component of e:

F_{n} = n
F_{i:(n_{1}↘d_{1})⊔···⊔(n_{m}↘d_{m})}
= new_{exp} y. y := c_{i}; if y = n_{1} then N_{d_{1}}
⋮

else if y = n_{m} then N_{d_{m}} else Ω.

Then we set M_{d} = λ⟨c_{1}, c_{2}⟩. N_{d}, and it is straightforward to verify that M_{d} defines d in the sense of the statement of the Lemma.

To formulate the full abstraction result, we will take convergence of closed terms of type comm as the observable. (We could also observe integers generated by terms of type exp, but this would lead to the same contextual equivalence relation.) To define this precisely, first note that if M is a closed term of type comm in Idealized Algol, the family of maps M^{⋆}(–) : I−∘ comm^{⋆}(–) is completely determined by the component M^{⋆}I : I−∘ φ^{⋆}I at I. (This follows from the Logical Relations Lemma, using relations of the form I ↔ S that fix a state in S.) The resulting function M^{⋆}I∗ : I−∘ I takes as an argument the state ∗ ^{∈} I and produces as a result either ∗ or ⊥. We take as observable this final value M^{⋆}I ∗ ∗, and we look at approximation in all comm-typed contexts.

Theorem 25. (Full Abstraction to 2nd order) Suppose ⊢ M : θ and ⊢ N : θ in Idealized Algol where θ = (φ_{1} × ⋯ φ_{n} → φ) → φ′. Then

M^{⋆} ⊑ N^{⋆} ⟺ ∀C[·]. C[M]^{⋆}I ∗ ∗ ⊑ C[N]^{⋆}I ∗ ∗

(where C[·] is understood to be a context such that C[M] and C[N] are closed terms of type comm).

Proof: The ⟹ direction is immediate from compositionality. For ⟸, suppose that [[M^{⋆}α]] ⋢ [[N^{⋆}α]]. We require a distinguishing context where C[M]^{⋆} ⋢ C[N]^{⋆}.

First suppose that φ′ is comm or exp. By Lemmas 13 and 16, and continuity, there is a finite element d and n ^{∈} N such that

(M^{⋆}I)[N_{⊥}]d[∗, n] ⋢ (N^{⋆}I)[N_{⊥}]d[∗, n].

By the Definability Lemma (using also an isomorphism N_{⊥} ↔ I ⊗ N_{⊥}) there is a term M_{d} that defines d in an environment where x denotes the standard variable v[I] for local variables.

If φ′ is comm then (M^{⋆}I)[N_{⊥}]d[∗, n] = [∗, m] for some m, and a distinguishing context is

C[·] = new_{φ′} x. x := n; ([·]M_{d}); if x = m then skip else diverge.

If φ′ is exp then (M^{⋆}I)[N_{⊥}]d[∗, n] = [∗, m, m′] for some m and m′, and a distinguishing context is

C[·] = new_{φ′} x. x := n; if ([·]M_{d}) = m′ then

if x = m then skip else diverge else diverge.

The proof when φ′ is acc is similar, if we observe that assignment to an acceptor is needed when using continuity and definability to generate a distinguishing context.

We have formulated the full abstraction result for second-order types of a specific form, but it is not difficult (observing remarks on naturality in Section 9.2) to extend the argument to all second-order types. We do not know if the result extends to higher types.

11. RELATED WORK

There are two ways to read the contribution of this paper. One has to do with semantic models of imperative languages, and the other with translating from an imperative language to a (linear) purely functional language. From the first point of view the semantics is being used to analyze the imperative source languages, while from the second the translation may be regarded just as much as telling us something about the functional target language. In discussing related work we consider these points of view in turn.

This paper builds on prior work on functor category semantics [Reynolds 1981a; Oles 1982; Oles 1997; O’Hearn and Tennent 1995; Sieber 1996], the main technical improvement being the elimination of snapback operators. The semantics may in fact be regarded as a refinement of the parametric-functor model of O’Hearn and Tennent [1995], obtained by moving from standard to linear polymorphism. Another difference with these works is our use of a polymorphic target language in place of a functor category (an aspect left implicit in the description of the parametric-functor model). This makes the store shape typing information implicit in a functor category more explicit, and statically checkable; we do not yet fully appreciate the significance of this point.

Pitts [1996] has carried out a study of contextual equivalence in Algol-like languages using operational techniques. His work is a good example of useful interplay between denotational and operational semantics. He proves a “possible worlds” version of the context lemma [Milner 1977], the formulation of which mimicks the structure of a functor category; it characterizes equivalence of functions in terms of applications to arguments at accessible worlds or store shapes. He uses an operational formulation of the relational principles considered here (and in [O’Hearn and Tennent 1995]) to prove his main result. A key point in Pitts’s work is that he separates the use of logical relations as reasoning principles from their use in constructing a model. This does not lead to representation results, and it de-emphasizes the connection with linear polymorphic typing, but it does provide a pleasantly simple mathematical expression of the relational principles, and interesting technical results.

A completely different view of imperative computation is given by implicit-state models, which interpret imperative programs using histories of events. The basic conception of this approach is similar to ideas in work on processes (e.g. [Milner 1989]), but novel models of Algol-like languages have now been defined using denotational tools. The first of these is due to Reddy [1996], who defined a model for syntactic control of interference using coherence spaces; more recently, Abramsky and McCusker [1997] gave a game model of Idealized Algol.

Reddy’s semantics is similar in spirit to domain-theoretic models of functional languages, and is based on a concrete description of domain-theoretic structure associated with SCI types. It accounts especially well for independence between arguments to functions. The model of Abramsky and McCusker is an extension the game semantics of PCF developed by Hyland and Ong [1994], obtained by dropping the “innocence” condition; this results in a clear distinction between functional and imperative behaviours in the model. They show that all finite elements in their model are definable by terms in essentially the same version of Idealized Algol considered here; this leads, after quotienting, to a fully abstract model. Previously, full abstraction had only been obtained up to second-order types [O’Hearn and Reddy 1999], which is where our analysis here (which was carried out around the same time) ends as well.

The difference between our semantics and implicit-state models is striking. For us the primitive concepts are sets of states, and the linearly polymorphic way that states are used. In the implicit models the primitive concepts are events or observations, and interaction of a program with its environment. The conceptual distance between the two approaches is thus very great. It is not obvious how to formulate a precise linkage between them, but to do so would be valuable.

We now turn to related work on linear functional programming. The informal connection between imperative-like state transformations and linear functions was emphasized from the beginning in linear logic. It formed part of the motivation for a number of linear functional languages [Mackie 1994; Lafont 1988; Holmström 1988; Chirimar et al. 1994], where linearity could be used to restrict the number of pointers to functional values and, in some cases, guarantee the safety of destructive array update.

This connection was illustrated particularly clearly by Wadler [1990], by translating an imperative langauge, without procedures, into a linear functional language. We argued in the Introduction that a language without procedures does not itself provide a stringent test for the imperative expressiveness of a linear language, but we do want to emphasize our debt to the work of Wadler, and to other early works on linear logic, for making the connection between imperative-like state transformations and linear functions. To these works we would add the point that moving from simple to polymorphic linear types allows for a treatment of procedures and local state, and as a result it becomes possible to cover a much wider range of imperative programming. We would also add that polymorphism can be used to capture that a non-linear state be used linearly.

Prior to the appearance of linear logic, Schmidt [1985] had already studied the relationship between syntactic restrictions on λ-terms and the imperative nature of state transformations. His aim was to detect, in a standard denotational definition, when a parameter was “single threaded.” The idea was that this would enable a compiler generator to detect when the parameter could be implemented in a storelike manner, by overwriting. His aim, and form of analysis, was thus different from ours; in particular, he works with simple types, where polymorphism plays a central role here. Some of his basic ideas are reflected in our translations, but one that is not is passivity [Reynolds 1978], where multiple copies of a store parameter are allowed in contexts that ensure that they are used in a read-only fashion.

12. DISCUSSION

In the course of the paper we have presented syntactic translations from two Algollike languages into a polymorphic, linear lambda-calculus, given a semantic model of the linear language, and used it characterize the cpo structure of a number of low-order types. We hope particularly to have convinced the reader that the translations and semantic model provide simple and effective principles that can be utilized in a variety of circumstances. This is highlighted by our work in Section 7, and also by Pitts’s work referenced above.

The semantic analysis provided by the strict parametricity model is, however, incomplete in come respects. We were in fact surprised to find that we could push the model as far as we could. To clarify this incompleteness we discuss a number of unanswered questions.

The first question arises from the work in Section 9.2: Does parametricity imply naturality with respect to expansions at all types for the Idealized Algol translation? If the answer is no then the translation of Idealized Algol, as it stands, would not verify the isomorphisms of cartesian closed categories at higher types. We indicated in Section 9.2 that this is not a fundamental problem, as we know a number of ways to overcome it. Furthermore, in Section 8 we verified an adequacy result to the effect that the translation gets convergence at primitive types right, so the translation can be used to soundly reason about Idealized Algol programs. But the question is irksome, because one might expect that parametricity should imply naturality [Plotkin and Abadi 1993].

Our analysis of equivalence only went as far as second-order types. We have not found a counterexample to full abstraction at higher types in Idealized Algol, but we did find an explicit limitation in the model for SCI in Section 7.3. One could consider a more focused study of contextual equivalence, either by using different models or by a syntactic analysis of the translations. Independently of any specific model we could ask if the translations are fully abstract, i.e., whether they preserve and reflect appropriate notions of contextual equivalence for source and target languages.

It may have seemed odd that we did use the strict function model, since it is actually a model of relevant lambda-calculus (it models Contraction). We observed that snapback requires both Contraction and Weakening, so that eliminating one has the effect of banishing snapback operators. But there may be a more comprehensive explanation than this. For primitive types in the translations there is always a unique occurrence of any type variable to the left or right of −∘: Intuitively, if you perform a Contraction, copying a value of one of these types, it must be followed by a Weakening to preserve the uniqueness property (and conversely if a Weakening is performed first). This leads to the question (which we leave imprecisely stated) of whether the translations are the same if we take relevant, linear, or affine lambda-calculus as the target language. When one moves outside the ranges of our translations, beyond Algol-like types, we expect that linearity would play a more crucial role; we would benefit from a more precise understanding of these points.

With this discussion of technical properties, it is well to remember that the original motivation for semantics based on store shapes was much more basic: It was to build a model that made the stack discipline obvious [Reynolds 1981a]. In particular, it is clear from the semantics of types that the shape of the store in the final state obtained by evaluating a command must be the same as the shape in the initial state. While the translation for Idealized Algol follows previous functorcategory models closely, in SCI store shapes play a further role, making clear that different identifiers work with different pieces of the state. So, more generally, we may say that semantics based on store shapes aims to communicate a spatial intuition: Programs working with different store shapes act on separate parts of the store, and consequently don’t interfere.

Our work here gives an implementation of store shape semantics by translation into a linear polymorphic functional language. We have, for the most part, concentrated on what the resulting semantics says about the source languages, but if we switch focus to the target language then the translations can just as well be regarded as telling us about it. In particular, since we already understand Algol as an imperative language, the translations (and representation results) give us a precise imperative way of reading certain linear types. This does not, however, help us to understand types that lie beyond the ranges of our translations, because there we do not have a prior understanding of an imperative language to fall back on.

A final note on the source languages, and limitations. While we concentrate on call-by-name, the adaptation of our semantic methods to a call-by-value setting does not appear to raise insuperable difficulties. Much more difficult is the inclusion of storable procedures or commands. Idealized Algol and SCI allow only stateless entities, such as integers, to be stored, and we do not know how well our methods might extend to deal with stateful values in the store.

We wonder whether this apparent limitation could be turned into a feature. That is, both Idealized Algol and Basic SCI are higher-order imperative languages that obey a stack discipline for variable declarations. While the stack discipline is made evident by the translations of types, there are other polymorphic types, lying outside the ranges of the translations, that display the same stack-like character. This raises the question of whether the stack-like sublanguage could be demarcated, perhaps leading to an imperative language that is more general and flexible than Algol, while maintaining efficient storage utilization.

Acknowledgements. This work first came to light at a workshop on Syntactic Control of Interference and Linear Logic in Glasgow in August of 1995, where the authors presented independently discovered translations into a linear polymorphic target language. The translations were essentially the same, except that O’Hearn used Idealized Algol as the source language where Reynolds used SCI. We are grateful to the workshop participants, especially the host Phil Wadler, for contributing to a remarkably congenial research atmosphere. Special thanks go to Uday Reddy for discussions on how the strict function model could eliminate snapback, to Gordon Plotkin for emphasizing the suitability of linear typing in the presence of recursion, and to Bob Tennent for numerous discussions, especially in relation to the material in Section 8. Thanks also to Jeff Polakow and Chris Stone for comments on the presentation in the paper, and the referees for helpful suggestions. O’Hearn was supported by NSF grant CCR-92110829 in the initial stages of this work. Reynolds was supported by NSF grant CCR-9409997. Support during extended visits was given to both authors from the Isaac Newton Programme on Semantics of Computation, held in Cambridge in 1995; to O’Hearn from the Electrotechnical Laboratory, Tsukuba, Japan; and to Reynolds from Bell Laboratories, Lucent Technologies, New Jersey.

REFERENCES

Abramsky, S. 1993. Computational interpretations of linear logic. Theoretical Computer

Science 111, 1–2 (April 12), 3–57. Abramsky, S., Jagadeesan, R., and Malacaria, P. Full abstraction for PCF. To appear in

Information and Computation. Abramsky, S. and Jung, A. 1994. Domain theory. In S. Abramsky, D. M. Gabbay, and

T. S. E. Maibaum Eds., Handbook of Logic in Computer Science, Volume 3, pp. 1–168. Clarendon Press.

Abramsky, S. and McCusker, G. 1997. Linearity, sharing and state. In P. W. O’Hearn and R. D. Tennent Eds., Algol-like Languages, Volume 2, pp. 297–330. Boston: Birkhauser. Extended abstract to appear in Proceedings of Linear Logic 1996, Electronic Notes in Theoretical Computer Science, volume 3, Elsevier Science, 1996.

Barber, A. and Plotkin, G. 1997. Dual intuitionistic linear logic. Submitted. Benton, N., Bierman, G., de Paiva, V., and Hyland, M. 1993. A term calculus for

intuitionistic linear logic. In M. Bezen and J. F. Groote Eds., Typed Lambda Calculi and Applications, Volume 664 of Lecture Notes in Computer Science (Utrecht, The Netherlands, March 1993), pp. 75–90. Springer-Verlag, Berlin.

Berry, G. 1978. Stable models of typed lambda-calculi. Automata, Languages and Pro-

gramming, Fifth Colloquium, Udine, 72–89. Lecture Notes in Computer Science 62. Berry, G. and Curien, P.-L. 1982. Sequential algorithms on concrete data structures.

Theoretical Computer Science 20, 265–321. Bezen, M. and Groote, J. F. Eds. 1993. Typed Lambda Calculi and Applications, Vol-

ume 664 of Lecture Notes in Computer Science (Utrecht, The Netherlands, March 1993). Springer-Verlag, Berlin.

Brookes, S., Main, M., Melton, A., and Mislove, M. Eds. 1995. Mathematical Foundations of Programming Semantics, Eleventh Annual Conference, Volume 1 of Electronic Notes in Theoretical Computer Science (Tulane University, New Orleans, Louisiana, March 29–April 1 1995). Elsevier Science.

Chirimar, J., Gunter, C. A., and Riecke, J. 1994. Reference counting as a computational interpretation of linear logic. Journal of Functional Programming 2, 6, 194–244.

Day, B. J. 1970. On closed categories of functors. In S. Mac Lane Ed., Reports of the Midwest Category Seminar, Volume 137 of Lecture Notes in Mathematics, pp. 1–38. Springer-Verlag, Berlin-New York.

Girard, J.-Y. 1972. Interprétation Fonctionnelle et Elimination des Coupures de l’Arith-

métique d’Ordre Supérieur. Ph. D. thesis, Université Paris VII. Girard, J.-Y. 1987. Linear logic. Theoretical Computer Science 46, 1–102. Holmström, S. 1988. Linear functional programming. Proceedings of the Workshop on

Implementation of Lazy Functional Languages, Chalmers University. Hyland, J. M. E. and Ong, C.-H. L. 1994. On full abstraction for PCF: I, II and III.

Submitted for publication. Lafont, Y. 1988. The linear abstract machine. Theoretical Computer Science 59, 157–180. Lambek, J. 1989. Multicategories revisited. In J. W. Gray and A. Scedrov Eds., Cat-

egories in Computer Science and Logic, Volume 92 of Contemporary Mathematics, pp. 217–240. American Mathematical Society.

Lent, A. F. 1993. The category of functors from state shapes to bottomless CPOs is adequate for block structure. In ACM SIGPLAN Workshop on State in Programming Languages (Copenhagen, Denmark, June 12, 1993), pp. 101–119. Technical report RR-968, Department of Computer Science, Yale University.

Mackie, I. 1994. Lilac : A functional programming language based on linear logic. Journal

of Functional Programming 4, 4 (Oct.), 395–433. Milner, R. 1977. Fully abstract models of typed λ-calculi. Theoretical Computer Science 4,

1–22. Milner, R. 1989. Communication and Concurrency. Prentice Hall, New York. O’Hearn, P. W., Power, A. J., Takeyama, M., and Tennent, R. D. 1999. Syntactic

control of interference revisited. Theoretical Computer Science ??, ???–??? To appear. Preliminary version in [Brookes et al. 1995] and in [O’Hearn and Tennent 1997b].

O’Hearn, P. W. and Reddy, U. S. 1999. Objects, interference and the Yoneda embedding. Theoretical Computer Science ??, ???–??? To appear. Preliminary version in [Brookes et al. 1995].

O’Hearn, P. W. and Riecke, J. G. 1995. Kripke logical relations and PCF. Information

and Computation 120(1), 107–116. O’Hearn, P. W. and Tennent, R. D. 1995. Parametricity and local variables. J.

ACM 42(3), 658–709. Also in [O’Hearn and Tennent 1997b], pages 109–164. O’Hearn, P. W. and Tennent, R. D. Eds. 1997a. Algol-like Languages, Volume 1.

Birkhauser, Boston. O’Hearn, P. W. and Tennent, R. D. Eds. 1997b. Algol-like Languages, Volume 2.

Birkhauser, Boston. Oles, F. J. 1982. A Category-Theoretic Approach to the Semantics of Programming Lan-

guages. Ph. D. thesis, Syracuse University, Syracuse, N.Y. Oles, F. J. 1987. Lambda calculi with implicit type conversions. Technical Report

RC 13245, IBM Research, T. J. Watson Research Center, Yorktown Heights, N.Y. Oles, F. J. 1997. Functor categories and store shapes. In P. W. O’Hearn and R. D.

Tennent Eds., Algol-like Languages, Volume 2, pp. 3–12. Boston: Birkhauser. Pitts, A. 1996. Reasoning about local variables with operationally-based logical relations.

In Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science (New Jersey, USA, 1996), pp. 152–163. IEEE Computer Society Press, Los Alamitos, California. Also in [O’Hearn and Tennent 1997b], pages 165–186.

Plotkin, G. 1983. Domains. 1992 TeXed edition of course notes prepared by Yugo Kashi-

wagi and Hidetaka Kondoh from notes by Tatsuya Hagino. Plotkin, G. and Abadi, M. 1993. A logic for parametric polymorphism. In M. Bezen and

J. F. Groote Eds., Typed Lambda Calculi and Applications, Volume 664 of Lecture Notes in Computer Science (Utrecht, The Netherlands, March 1993), pp. 361–375. Springer-Verlag, Berlin.

Plotkin, G. D. 1977. lcf considered as a programming language. Theoretical Computer

Science 5, 223–255. Plotkin, G. D. 1980. Lambda-definability in the full type hierarchy. In J. P. Seldin and

J. R. Hindley Eds., To H. B. Curry: Essays in Combinatory Logic, Lambda Calculus and Formalism, pp. 363–373. Academic Press.

Plotkin, G. D. 1993. Type theory and recursion (extended abstract). In Proceedings, Eighth Annual IEEE Symposium on Logic in Computer Science (Montreal, Canada, 19–23 June 1993), pp. 374. IEEE Computer Society Press.

Reddy, U. S. 1996. Global states considered unnecessary: introduction to object-based semantics. Lisp and Symbolic Computation. Special issue on State in Programming Languages. Also in [O’Hearn and Tennent 1997b], pages 227–296.

Reynolds, J. C. 1974. Towards a theory of type structure. In Proc. Colloque sur la Programmation, Volume 19 of Lecture Notes in Computer Science (Berlin, 1974), pp. 408–425. Springer-Verlag.

Reynolds, J. C. 1978. Syntactic control of interference. In Conference Record of the Fifth Annual ACM Symposium on Principles of Programming Languages (Tucson, Arizona, January 1978), pp. 39–46. ACM, New York. Also in [O’Hearn and Tennent 1997a], pages 273–286.

Reynolds, J. C. 1981a. The Craft of Programming. Prentice-Hall International, London. Reynolds, J. C. 1981b. The essence of Algol. In J. W. de Bakker and J. C. van Vliet

Eds., Algorithmic Languages (Amsterdam, October 1981), pp. 345–372. North-Holland, Amsterdam. Also in [O’Hearn and Tennent 1997a], pages 67-88.

Reynolds, J. C. 1983. Types, abstraction and parametric polymorphism. In R. E. A.

Mason Ed., Information Processing 83 , pp. 513–523. Amsterdam: North Holland. Riecke, J. G. and Sandholm, A. 1997. A relational account of call-by-value sequentiality.

In Proceedings, Twelth Annual IEEE Symposium on Logic in Computer Science (Warsaw, Poland, 29 June–2 July 1997), pp. 258–267. IEEE Computer Society Press.

Schmidt, D. A. 1985. Detecting global variables in denotational specifications. ACM Trans.

on Programming Languages and Systems 7, 3 (April), 299–310. Scott, D. S. 1972. Mathematical concepts in programming language semantics. In Proc.

1972 Spring Joint Computer Conference (1972), pp. 225–34. AFIPS Press, Montvale, N.J. Scott, D. S. and Strachey, C. 1971. Toward a mathematical semantics for computer

languages. In J. Fox Ed., Proceedings of the Symposium on Computers and Automata, Volume 21 of Microwave Research Institute Symposia Series (1971), pp. 19–46. Polytechnic Institute of Brooklyn Press, New York. Also Technical Monograph PRG-6, Oxford University Computing Laboratory, Programming Research Group, Oxford.

Sieber, K. 1996. Full abstraction for the second order subset of an Algol-like language.

Theoretical Computer Science 168, 1 (10 Nov.), 155–212. Strachey, C. 1972. The varieties of programming language. In Proceedings of the Interna-

tional Computing Symposium (Venice, April 1972), pp. 222–233. Cini Foundation, Venice. Also in [O’Hearn and Tennent 1997a], pages 51–64.

Tennent, R. D. 1991. Semantics of Programming Languages. International Series in Com-

puter Science. Prentice-Hall International. Wadler, P. 1990. Linear types can change the world! In M. Broy and C. Jones Eds.,

IFIP TC-2 Working Conference on Programming Concepts and Methods (Sea of Galilee, Israel, April 1990), pp. 347–359. North Holland, Amsterdam.

Wadler, P. 1991. Is there a use for linear logic? In ACM/IFIP Symposium on Partial Evaluation and Semantics-Based Program Manipulation (1991). Proceedings of the 1991 Conference.