BRICS RS-97-41 Riecke & Sandholm: A Relational Account of Call-by-Value Sequentiality BRICS

Basic Research in Computer Science

A Relational Account of Call-by-Value Sequentiality

Jon G. Riecke Anders B. Sandholm BRICS Report Series RS-97-41 ISSN 0909-0878 December 1997 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1997, BRICS, Department of Computer Science

University of Aarhus. All rights reserved.

Reproduction of all or part of this work is permitted for educational or research use on condition that this copyright notice is included in any copy.

See back inner page for a list of recent BRICS Report Series publications. Copies may be obtained by contacting:

BRICS Department of Computer Science University of Aarhus Ny Munkegade, building 540 DK–8000 Aarhus C Denmark

Telephone: +45 8942 3360
Telefax: +45 8942 3255
Internet: BRICS@brics.dk

BRICS publications are in general accessible through the World Wide Web and anonymous FTP through these URLs:

http://www.brics.dk
ftp://ftp.brics.dk

This document in subdirectory RS/97/41/

A Relational Account of Call-by-Value Sequentiality

Jon G. Riecke Bell Laboratories Lucent Technologies

            riecke@bell-labs.com

Anders Sandholm BRICS^{∗}, Department of Computer Science University of Aarhus, Denmark

              sandholm@brics.dk

Abstract

We construct a model for FPC, a purely functional, sequential, call-by-value language. The model is built from partial continuous functions, in the style of Plotkin, further constrained to be uniform with respect to a class of logical relations. We prove that the model is fully abstract.

1 Introduction

The problem of finding an abstract description of sequential functional computation has been one of the most enduring problems of semantics. The problem dates from a seminal paper of Plotkin [25], who pointed out that certain elements in Scott models are not definable. In Plotkin’s example, the function

∗ Basic Research in Computer Science, Centre of the Danish National Research Foundation.

por(x, y) = \{ \begin{matrix}true & if x or y = true \\ false & if x and y = false \\ ⊥ & otherwise \end{matrix}

where ⊥ denotes divergence, cannot be programmed in the language in the language PCF, a purely functional, sequential, call-by-name language with booleans and numbers as base types. The problem is called the “sequentiality problem” because, intuitively, the only way to program por involves evaluating boolean expressions in parallel.

There are, of course, plenty of elements in the Scott model of PCF that cannot be programmed: the domains have uncountably many elements. Nevertheless, the por function is worse: it causes two terms in the language PCF to be distinct denotationally even though the terms cannot be distinguished by any program. When similar examples do not exist— in other words, when denotational approximation coincides with operational approximation—the denotational model is said to be fully abstract. Shortly after Plotkin’s paper, Milner proved that there was exactly one fully abstract model of PCF meeting certain conditions [16]. Until recently, all descriptions of this fully abstract model have used operational semantics (see, for instance, [19, 34]). New constructions using games semantics [2, 10, 20] and logical relations [22, 33] have yielded a more abstract understanding of PCF.

The sequentiality problem is enduring because it is robust. For instance, changing the reduction strategy of PCF from call-by-name to call-by-value makes no difference: versions of the “parallel or” function reappear in the standard Scott model (albeit at higher type). Even for languages that lack an explicit base type, e.g., the polymorphic λ-calculus with recursion, the known Scott models contain parallel elements that cause a failure of full abstraction.

This paper extends the logical-relations approach to another setting. It constructs a model for a call-by-value, purely functional, sequential language called FPC. FPC includes a base type with one convergent value, strict products, strong (categorical) sums, functions, and recursive types. Full abstraction for FPC is interesting for at least two reasons:

1. FPC can be regarded as the purely functional, non-polymorphic sublanguage of Standard ML [17]: recursive types and sums are the basis of datatype declarations, and both Standard ML and FPC are call-by-value. By studying FPC, we learn more about programming languages like Standard ML.

2. FPC can serve as an expressive metalanguage for denotational semantics [8, 26]. FPC, for instance, has enough expressive power to encode a call-by-value version of PCF (the base type of numbers can be encoded via a recursive type). Given a fully abstract translation [29] from a language into FPC, the model of FPC yields a fully abstract model of the language.

The relations used in the construction of the model for FPC tease apart the structure of Sieber’s relations for PCF [33]. Sieber’s model of PCF, and the fully abstract model of PCF using Kripke relations [22], begin from a class of relations at any flat base type (e.g., the partial order of natural numbers with a divergent ⊥ element below every other element). Sieber’s definition of the relations is simple to state.

Definition 1 Suppose A ⊆ B ⊆ {1, …, n}, and let S_{A,B}^{n} be

{(d_{1}, …, d_{n}) | (∀i ∈ A. d_{i} ≠ ⊥) ⟹ (∀i, j ∈ B. d_{i} = d_{j})}.

Then R is an n-ary sequentiality relation if R is the intersection of relations of the form S_{A,B}^{n}.

These relations thus have an elegant semantic definition: nothing in the definition refers to the terms or operations of PCF. They also seem to say something about sequential computation: if certain elements of a tuple must converge, then other elements must converge. (It is helpful to think of the elements of a relation as potential results of a function.) One can easily show all PCF terms preserve the sequentiality relations, and that por does not preserve the sequentiality relation S_{{1,2},{1,2,3}}^{3}. It must therefore be the case that por is not definable.

Sieber’s definition of “sequentiality relation” seems to be limited to flat base types. It does not make sense to check for equality at functional type, and the relations say nothing about more complicated partial order structures. It is difficult to see how, for instance, to extend directly the definition to complex sums such as int ⊕ (int ⇒ int).

Instead of directly extending Sieber’s relations, our relations break down sequentiality relations into two components. The first captures the sequential behavior of termination: if certain elements in a tuple in the relation terminate (are non-bottom), then certain other elements in the tuple must terminate. The second captures the behavior of sums: if certain elements in a tuple lie in one side of a sum type, other components must lie in the same side of the sum type. This is much like Sieber’s definition in asking for equality of all B-indexed elements of a tuple in S_{A,B}^{n}. The interesting case comes when this second component of relations is lifted to types other than sums: when, for example, the tuple is a tuple of elements in a function type. In essence, the second component of relations encodes a form of “computation tree,” stating which subtuples of a tuple form consistent traces of the computation so far.

We begin by introducing the language FPC, the main language of study in this paper. We then describe the form of the relations, showing the decomposition into the two portions described above. We follow the O’Hearn-Riecke construction for PCF [22] and lift the relations to Kripke relations, using a definition found in [13]. It will be these relations that will be used to define a category in which a model of FPC can be constructed. The Kripke relations will be used to establish the full abstraction of the model.

2 The Language FPC

FPC as described in [8, 26] is a call-by-value, purely functional language with a single base type unit, sums, products, functions, and recursive types. More familiar base types, such as booleans or natural numbers, can be easily constructed in the language.

FPC has types given by the grammar

s, t ::= unit | (s ⊕ t) | (s ⊗ t) | (s ⇒ t) | α | (rec α. t)

where α ranges over a collection of type variables. Types are identified up to renaming of type variables bound by rec. The raw terms of FPC are given by the grammar

M, N, P ::= x | (λx : t. M) | (M N) |
⟨⟩ | ⟨M, N⟩ | (proj_{i} M) | (inj_{i} M) |
(case M of inj_{1}(x).N or inj_{2}(x).P) |
(intro_{rec α. s} M) | (elim_{rec α. s} M)

A typing judgement is a formula of the form Γ ⊢ M : t where M is a term, t a type, and Γ is a typing context, i.e., a finite function from variables to types. Rules for deriving typing judgements appear in Table 1. In the type rules, we assume that all types are closed.

Evaluation rules for FPC appear in Table 2. In the rules, we use the notation M[N/x] to denote capture-free substitution of N for x in M. Notice that function application in FPC is call-by-value: arguments to functions must be values before they are substituted into bodies of functions. The operational approximation relation can then be defined as follows:

Definition 2 M ⊑_{F P C} N if for any context C[·] such that C[M] and C[N] are closed, well-typed terms, C[M] ⇓ V implies C[N] ⇓ V′ for some V′.

Note that we observe termination at any type.

FPC is a very sparse language: there is no recursion nor even any obvious divergent computations. Nevertheless, it still has enough computing power for many applications. For instance, Plotkin [26] and Gunter [8] show how to build recursion operators using recursive types. For a slightly simpler example, one can encode a sequencing operation: (M; N) stands for the term ((λx : s. N) M), where x does not occur free in N. Indeed, the semantics of many programming languages—including non-functional languages—can be given by translation to FPC. FPC’s main deficiency as a metalanguage for denotational semantics is a lack of parametric polymorphism (as in the Girard–Reynolds calculus [7, 27]), which precludes a good representation of abstract data types.

3 Category of Meanings

In this section we construct a category suitable for interpreting FPC. Throughout the section, DCPO denotes the category of dcpos and partial continuous functions, where a dcpo is a directed-complete poset (not necessarily possessing a least element).

The category is built from objects that have both dcpo structure and relational structure. The relations are defined in two stages. First, we show how to define base relations suitable for modeling the language. Second, we lift the relations to Kripke relations of varying arity. The category of meanings will use Kripke relations; morphisms will be continuous functions that additionally preserve the Kripke relational structure.

Table 1: Type Rules for FPC. Γ, x : t ⊢ x : t

Γ ⊢ ⟨⟩ : unit

\frac{Γ, x : s ⊢ M : t}{Γ ⊢ (λx : s. M) : (s ⇒ t)}

\frac{Γ ⊢ M : (s ⇒ t) Γ ⊢ N : s}{Γ ⊢ (M N) : t}

\frac{Γ ⊢ M : s Γ ⊢ N : t}{Γ ⊢ ⟨M, N⟩ : (s ⊗ t)}

\frac{Γ ⊢ M : (s_{1} ⊗ s_{2})}{Γ ⊢ (proj_{i} M) : s_{i}}

\frac{Γ ⊢ M : s_{i}}{Γ ⊢ (inj_{i} M) : (s_{1} ⊕ s_{2})}

\frac{Γ ⊢ M : (s_{1} ⊕ s_{2}) Γ, x : s_{i} ⊢ N_{i} : t}{Γ ⊢ (case M of inj_{1}(x).N_{1} or inj_{2}(x).N_{2}) : t}

\frac{Γ ⊢ M : s[rec α. s/α]}{Γ ⊢ (intro_{rec α. s} M) : (rec α. s)}

\frac{Γ ⊢ M : (rec α. s)}{Γ ⊢ (elim_{rec α. s} M) : s[rec α. s/α]}

Table 2: Evaluation Rules for FPC.

⟨⟩ ⇓ ⟨⟩

(λx : s. M) ⇓ (λx : s. M)

\frac{M ⇓ (λx : s. M′) N ⇓ V′ M′[V′/x] ⇓ V}{(M N) ⇓ V}

\frac{M_{1} ⇓ V_{1} M_{2} ⇓ V_{2}}{⟨M_{1}, M_{2}⟩ ⇓ ⟨V_{1}, V_{2}⟩}

\frac{M ⇓ ⟨V_{1}, V_{2}⟩}{(proj_{i} M) ⇓ V_{i}}

\frac{M ⇓ V}{(inj_{i} M) ⇓ (inj_{i} V)}

\frac{M ⇓ (inj_{i} V) N_{i}[V/x] ⇓ R}{(case M of inj_{1}(x).N_{1} or inj_{2}(x).N_{2}) ⇓ R}

\frac{M ⇓ V}{(intro_{rec α. s} M) ⇓ (intro_{rec α. s} V)}

\frac{M ⇓ (intro_{rec α. s} V)}{(elim_{rec α. s} M) ⇓ V}

3.1 Base relations

The basic relations of the model come in two varieties: termination relations and computational relations. Both kinds of relations range over elements of a dcpo. Following [13, 22], it will be helpful to represent relations by finite, total functions from indices to values instead of as tuples of values. Of course, there is no real difference between the two presentations, but the functional version will be easier to extend to Kripke relations later on.

Termination relations are defined using simple implicational theories. Let w be a finite set of indices. Then a w-termination theory is a set of implications of the form (d_{1}, …, d_{n} ⊢ d) where d_{1}, …, d_{n}, d ∈ w and n ≥ 1. Intuitively, each implication states a property similar to the Sieber’s sequentiality relations: if a function halts on the indices in the argument, it must halt on the index in the result. Indeed, the termination part of Sieber’s relations S_{A,B}^{n} can be encoded: if A ⊆ B ⊆ w, A = {d_{1}, …, d_{k}}, and B = {d_{1}, …, d_{k}, d_{k+1}, …, d_{n}} then S_{A,B}^{w} corresponds to the implications (d_{1}, …, d_{k} ⊢ d_{k+1}), …, (d_{1}, …, d_{k} ⊢ d_{n}).

For w′ ⊆ w, we say that w′ ⊧ (d_{1}, …, d_{n} ⊢ d) if d_{1}, …, d_{n} ∈ w′ implies d ∈ w′. If T is a set of such implications, we say that w′ ⊆ w is a T -model if w′ ⊧ ψ for all ψ ∈ T. There is an alternative characterization of T -models that can be helpful in proving facts about termination relations (a closelyrelated characterization can be found in [35], page 22). Suppose w is a finite set and X ⊆ P(w). Then X is a closure system if w ∈ X, ∅ ∈ X, and X is closed under intersection.

Proposition 3 Suppose w is a finite set. Then X ⊆ P(w) is a closure system iff there is a w-termination theory T such that X is the set of T - models.

Proof: For the easy direction, suppose T is a w-theory. Then obviously w and ∅ are T -models. To see closure under intersection, suppose w_{1}, w_{2} are T -models. Suppose (d_{1}, …, d_{n} ⊢ d) ∈ T, and d_{i} ∈ w_{1} ∩ w_{2} for all i. Then d ∈ w_{1} and d ∈ w_{2}, hence d ∈ w_{1} ∩ w_{2}. Thus, w_{1} ∩ w_{2} is also a T -model.

For the other direction, suppose X is a closure system. Define the theory T by

(d_{1}, …, d_{n} ⊢ d) ∈ T iff for all w′ ∈ X, w′ ⊧ (d_{1}, …, d_{n} ⊢ d).

Let Y = {w′ | w′ is a T -model}; we want to show that X = Y.

It is obvious that X ⊆ Y: if w′ ∈ X, then by construction it satisfies all the formulas in T and hence is a T -model. Conversely, suppose w′ ∉ X. Let

w_{0} = ⋂{w_{1} ∈ X | w′ ⊆ w_{1}}.

Since X is closed under finite intersections, and the set above is finite because w is, w_{0} must be in X. But since w′ ∉ X and w′ ⊆ w_{0}, it must be the case that there is a d ∈ w_{0} such that d ∉ w′. Also, because w′ ∉ X, it cannot be the empty set. Now consider the formula (w′ ⊢ d). This is a legal formula because w′ has at least one element. Note that (w′ ⊢ d) ∈ T, and w′ |̸= (w′ ⊢ d). Thus, w′ ∉ Y, completing the proof.

The proof is similar to a part of Sieber’s proof that the sequentiality relations are precisely those that are closed under the operations of PCF (see [33]).

Termination theories are the building blocks of the first kind of relations, the termination relations. Let T be a w-termination theory, and D be a dcpo. A T -termination relation on D is a set of the form

R ⊆ ⋃_{w′ is a T -model} [w′ →_{t} D],

where [w′ →_{t} D] denotes the set of all total (set-theoretic) functions from w′ to D, such that the following properties hold:

1. Non-emptiness: R is non-empty.

2. Directed completeness: R is directed complete, where f ⊑ g iff f, g have the same domain w′ and for all d ∈ w′, f(d) ⊑ g(d) in D.

3. Downward closure: For any f ∈ R with domain w′ and T -model w′′ ⊆ w′, (\underline{λ}d ∈ w′′. f(d)) ∈ R.

Here, (\underline{λ}d ∈ w′′. f(d)) stands for the function with domain w′′, whose return value is f(d); thus, an element of a termination relation R is a function from a subset of indices to elements of the dcpo. To get some intuition, it is again helpful to think of indices as possible arguments to a function, and the elements as the return values of the function. An element of R then represents a “related” set of values returned by a function.

One subtlety in this definition is the ⊑ relation: we only compare elements of R that have the same domain. The definition of ⊗ on relations does not produce a directed complete relation if we regard the elements of R as partial functions and compare elements with different domains. A second subtlety arises from the first and third conditions. These two conditions imply that the empty function is always an element of R, which is necessary to prove that divergent terms always respect the relations.

Of course, functions represented by terms in FPC may have much more complex behavior: they may test some of their arguments and branch based on the results. At the ends of branches are “related” values returned by the function, but there need be no relationship between the values returned by different branches. To model this behavior, we use computational relations. We first need a preliminary definition. Let T be a w-termination theory. Then S is a T -computational theory if S is a set of finite sets of T - models, i.e., each element of S has the form {w_{1}, …, w_{k}}, and satisfies the following conditions:

• If w′ is a T -model, then {w′} ∈ S;

• If {w_{1}, …, w_{k}} and {w′_{1}, …, w′_{l}} are in S, and w_{i,j} = (w_{i} ∩ w′_{j}), then {w_{1,1}, …, w_{k,l}} ∈ S; and

• If {w_{1}, …, w_{k}} and {w′_{1}, …, w′_{l}} are in S, and for all i and some j, w′_{i} ⊆ w_{j}, then

{w_{1}, …, w_{j−1}, w′_{1}, …, w′_{l}, w_{j+1}, …, w_{k}} ∈ S.

The elements of S are called path sets for reasons that will become clear in a moment.

The path sets permit the definition of computational relations, which just lifts a termination relation to a partial function on indices. Suppose S is a T -computational theory and R is a T -termination relation on D. Define the computational relation R_{S} by

R_{S} = \{ f ∈ [w →_{p} D] | there exists \{w_{1}, …, w_{k}\} ∈ S such that f(d) ↓ iff d ∈ w_{i} for some i, and for all i, (\underline{λ}d ∈ w_{i}. f(d)) ∈ R \}

where [w →_{p} D] represents the set of partial set-theoretic functions from the set w to the set D. The computational relations are reminiscent of Moggi’s analysis of call-by-value via monads [18], and they will play a similar role in the semantics below.

It is useful to think of elements of R_{S} as the interpretation of a term given some environment. A computation branches based on its inputs and returns some final results at the end. Each set in {w_{1}, …, w_{n}} represents a path in that computational tree; the answers returned at the end of a path must be consistent, hence the restriction of the function to (\underline{λ}d ∈ w_{i}. f(d)) must be in R. We can now see from where the three conditions on computational theories come. The first condition says that a potential path set that does no branching is a valid path set; the second says path sets can be combined; the third says that an element of a path set may be replaced by finer-grain path set, which amounts to adding a set of branches to a non-branching part of the computation.

3.2 Extension to Kripke relations

We could build a category of meanings directly using termination and computational theories; we would probably not get a fully abstract model (see the discussion in Section 6). Instead, we extend the relations to Kripke relations of varying arity [13]. Kripke relations of this kind begin from an index category whose objects are finite sets and whose morphisms are total functions (not necessarily all of them).

Definition 4 Suppose C is an index category. A C-termination theory is a family

T = { T^{w} | w ∈ Ob(C), T^{w} is a w-termination theory },

such that, for any φ : v ⟶^{C} w, if w′ is a T^{w}-model, then { d ∈ v | φ(d) ∈ w′ } is a T^{v}-model.

A Kripke relation is a set of termination relations that must fit together.

Definition 5 Let C be an index category, T be a C-termination theory, and D be a dcpo. A C, T -termination relation on D is a family of sets

R = {R^{w} | w ∈ Ob(C), R^{w} is a T^{w}-termination relation on D}

satisfying the

Kripke monotonicity condition:

For any f ∈ R^{w} with domain w′ and φ : v ⟶^{C} w, then (\underline{λ}d ∈ v′. f(φ(d)) ∈ R^{v}, where v′ = \{ d ∈ v | φ(d) ∈ w′ \}.

Computational theories also extend straightforwardly to the Kripke case:

Definition 6 Let C be an index category and T be a C-termination theory. Then S is a C, T -computational theory if S is a set, indexed by objects w of C, of T^{w}-computational theories.

If S is a C, T -computational theory and R is a C, T -termination relation on D, we let R_{S}^{w} denote the computational relation built from R^{w} and S^{w}.

3.3 A category for interpreting FPC

We now have enough machinery to build the category SR (for sequentiality relations).

• Objects. An object A consists of a dcpo |A| and a C, T -termination relation A(T, S) on |A| for each C-termination theory T and C, T - computational theory S. Objects must also satisfy the

Concreteness Condition:

For any d ∈ D, (\underline{λ}i ∈ w. d) ∈ A(T, S)^{w}.

• Morphisms. A morphism f : A → B is a partial continuous function f : |A| ⇀ |B| satisfying the

Uniformity Condition:

For all C, C-termination theories T, C, T -computational theories S, and h ∈ A(T, S)^{w}, (h; f) ∈ B(T, S)_{S}^{w}, where (h; f) denotes diagrammatic composition of h and f.

Composition and identities are inherited from DCPO. It is straightforward to check that SR is indeed a category; the only slightly non-obvious step is checking that composition is uniform, for which one needs the closure properties of path sets. Moreover, the category is dcpo-enriched, meaning that for any objects A, B, the set of morphisms Hom_{SR}(A, B) is a dcpo; the morphisms are ordered

f ⊑ g iff
for any a ∈ |A|, f(a)↓ implies that g(a)↓ and f(a) ⊑ g(a) in |B|

where f(a)↓ means that f(a) is defined.

3.4 Interpretation of FPC

The basic constructions needed for interpreting FPC are the following:

Void object:

|void| = {}

void(T, S)^{w} = {∅}

Unit object:

|unit| = {⊤}

unit(T, S)^{w} = \{ (\underline{λ}d ∈ w′. ⊤) | w′ is a T^{w}-model \}

Products:

|A ⊗ B| = |A| × |B| (cartesian product)

(A ⊗ B)(T, S)^{w} = {⟨g, h⟩ | g ∈ A(T, S)^{w}, h ∈ B(T, S)^{w},

and g, h have same domain}

Coproducts:

|A ⊕ B| = |A| ⊕ |B| (disjoint union)

(A ⊕ B)(T, S)^{w} = { f | (∃g ∈ A(T, S)^{w}.f = (g; inj_{1})) ∨
(∃h ∈ B(T, S)^{w}.f = (h; inj_{2})) }

Exponentiation:

|A ⇒ B| = Hom_{SR}(A, B),

(A ⇒ B)(T, S)^{w} = { f | ∀φ : v ⟶^{C} w, g ∈ A(T, S)^{v}.

(\underline{λ}d ∈ v. (f(φ(d)) (g(d)))) ∈ B(T, S)_{S}^{v}\}

The definition of exponentiation on relations follows the one in [13, 22]. Note that the definition of the relational component of unit captures much of the intuition we set out for termination relations.

One may check that void, unit are objects and ⊗, ⊕, and ⇒ are bifunctors (where ⇒ is contravariant in the first argument as usual). To interpret FPC, a bit more structure is required. It is not hard to show that ⊕ is a coproduct, and the usual constructions on pairs (projections and pairing) also define morphisms. Also, the category is a partial cartesian closed category in the sense of [5]. This provides all the structure to interpret FPC types and terms except those involving recursive types.

The interpretation of recursive types requires adapting standard results from domain theory (see, for instance, [1, 8]) to SR. Recursive types are interpreted via a colimit construction. Given objects A, B, f is an embedding projection pair (ep-pair for short) if f = (f^{e} : A → B, f^{p} : B → A), (f^{e}; f^{p}) = id_{A}, and (f^{p}; f^{e}) ⊑ id_{B}. An expanding sequence is a tuple

({D_{n} | n ≥ 0}, {f_{mn} | f_{mn} : D_{n} → D_{m} is an ep-pair, n ≤ m}),

such that f_{nn} = id_{D_{n}} and for any n ≤ k ≤ m, f_{mn}^{e} = (f_{kn}^{e}; f_{mk}^{e}) and f_{mn}^{p} = (f_{mk}^{p}; f_{kn}^{p}). Given an expanding sequence as above, define the object D by

|D| = {⟨x_{0}, x_{1}, …⟩ | x_{i} ∈ D_{i} and ∀n ≤ m, x_{n} = f_{mn}^{p}(x_{m})}
D(T, S)^{w} = {h ∈ [w′ →_{t} D] | w′ is a T^{w}-model, and there exist h_{i} ∈ D_{i}(T, S)^{w} with domain w′, such that h = ⟨h_{0}, h_{1}, h_{2}, …⟩ and for all n ≤ m, h_{n} = (h_{m}; f_{mn}^{p})}.

This is indeed an object in SR. The embedding-projection pairs (μ_{m}^{e} : D_{m} → D, μ_{m}^{p} : D → D_{m}), defined by

\begin{matrix}μ_{m}^{p}(⟨x_{0}, x_{1}, …⟩) = x_{m} \\ μ_{m}^{e}(d) = ⟨⨆_{k≥m,0}(f_{k0}^{p}(f_{km}^{e}(d))), ⨆_{k≥m,1}(f_{k1}^{p}(f_{km}^{e}(d))), ..⟩ \end{matrix}

make the object D into a colimit of the expanding diagram. The only nonstandard part of the proof lies in showing that μ_{m}^{e} and μ_{m}^{p} satisfy the uniformity property.

Recursive types make the interpretation somewhat complex [8, 26]. The meaning of a possibly open type is a functor from its free variables to the category SR. The functor, though, may be covariant in some of its arguments and contravariant in others. For instance, the type expression (α ⇒ β) has α occurring contravariantly and β occurring covariantly. We follow recent tradition (see [6, 24]) and convert a type with n-variables into one with 2n variables: α⃗ occurring only negatively and β⃗ occurring only positively. For instance, the type (α ⇒ α) gets converted to the type (α ⇒ β).

The meaning of a type is a functor (SR^{op})^{n} × (SR)^{n} → SR. The definition on objects is

[[unit]](A⃗, B⃗) = unit
[[rec α. s]](A⃗, B⃗) = F IX([[s]](X :: A⃗, Y :: B⃗))
[[s ⊕ t]](A⃗, B⃗) = ([[s]](A⃗, B⃗) ⊕ [[t]](A⃗, B⃗))
[[s ⊗ t]](A⃗, B⃗) = ([[s]](A⃗, B⃗) ⊗ [[t]](A⃗, B⃗))
[[s ⇒ t]](A⃗, B⃗) = ([[s]](B⃗, A⃗) ⇒ [[t]](A⃗, B⃗))

where F IX is an operation on functors that generates a canonical colimit (it can be easily expressed as a colimit of an expanding sequence starting from the void object, using the functor to build the subsequent elements of the chain). We omit the full definition here, and the definition of [[s]] on morphisms. When acting on ep-pairs, the functor [[s]] is continuous in the sense described in [1]. The canonical maps

intro : F IX(G(X, Y)) → G(F IX(G(X, Y)), F IX(G(X, Y)))
elim : G(F IX(G(X, Y)), F IX(G(X, Y))) → F IX(G(X, Y))

which define an isomorphism, are used to give meaning to the intro and elim term constructors.

The meaning of terms can then be given using the combinators of the category. Suppose Γ ⊢ M : s. If

Γ = x_{1} : t_{1}, ..., x_{n} : t_{n},

define [[Γ]] = [[t_{1}]] ⊗ … ⊗ [[t_{n}]]. (If Γ is empty, [[Γ]] is the object unit). Then [[Γ ⊢ M : s]] is a morphism in SR. We omit the full definition here. For notational convenience, if ∅ ⊢ M : s, we write [[M]] for the corresponding element [[∅ ⊢ M : s]]⊤ ∈ [[s]].

4 Examples

Even though the semantic category SR is arguably complicated, it does support simple reasoning about definability of FPC terms.

4.1 Parallel convergence testing is not definable

Consider the partial continuous function

f : (unit ⇒ unit) ⊗ (unit ⇒ unit) → unit

defined

f⟨g, h⟩ = \{ \begin{matrix}⊤ & if g(⊤)↓ or h(⊤)↓ \\ undefined & otherwise. \end{matrix}

f appears to need to do its calculation “in parallel.” We would like to prove that f is not a morphism in the category, which will immediately imply that f is not definable.

The argument follows the proof of Sieber (also due to Plotkin, see [3]) that por is not definable. In this case, we need to exhibit an index category C, a choice of C-termination theory T, and a C, T -computational theory S. Pick C to be the category with just one index set w = {1, 2, 3}, T^{w} to be the theory with just one implication (1, 2 ⊢ 3), and S to be the set { (w′) | w′ is a T^{w}-model }. Let h : unit → unit be the function that returns ⊤ given ⊤, and h′ : unit → unit be the empty partial function. Also, let

g_{1} = ⟨h, h′⟩, g_{2} = ⟨h′, h⟩, g_{3} = ⟨h′, h′⟩.

Returning to standard tuple notation for relations, we claim

(g_{1}, g_{2}, g_{3}) ∈ ((unit ⇒ unit) ⊗ (unit ⇒ unit))(T, S)^{w}.

To prove the claim, one may show (h, h′, h′), (h′, h, h′) ∈ (unit ⇒ unit)(T, S)^{w} by a simple case analysis. But

(f(g_{1}), f(g_{2}), f(g_{3})) ∉ unit(T, S)_{S}^{w},

so f is not uniform. Thus, f cannot be a morphism, and hence it cannot be definable.

4.2 Sieber’s last example is not definable

The second example is essentially the last example in [33], an example modified from [4]. Let

• bool be the object (unit ⊕ unit), and

• A = (unit ⇒ bool) ⊗ (unit ⇒ bool).

Let true denote inj_{1}(⊤) ∈ bool and false denote inj_{2}(⊤) ∈ bool. Consider the morphisms g_{1}, g_{2}, g_{3}, g_{4} : A → unit defined by

g_{1}⟨h_{1}, h_{2}⟩ ≃ \{ \begin{matrix}⊤ & if h_{2}(⊤) = true \\ ⊤ & if h_{1}(⊤) = true and \\ & h_{2}(⊤) = false \\ undefined & otherwise \end{matrix}

g_{2}⟨h_{1}, h_{2}⟩ ≃ \{ \begin{matrix}⊤ & if h_{1}(⊤) = false \\ undefined & otherwise \end{matrix}
g_{3}⟨h_{1}, h_{2}⟩ ≃ \{ \begin{matrix}⊤ & if h_{2}(⊤) = false \\ undefined & otherwise \end{matrix}
g_{4}⟨h_{1}, h_{2}⟩ ≃ undefined

We claim that any f : (A ⇒ unit) → unit where

f(g_{1}) = ⊤, f(g_{2}) = ⊤, f(g_{3}) = ⊤, f(g_{4}) ↑

is not definable in FPC.

The proof of nondefinability requires a nontrivial use of path sets, and follows the ideas in [33]. Pick C to be the trivial index category C with object w = {1, 2, 3, 4}. Let T^{w} be the termination theory T^{w} with just one implication (1, 2, 3 ⊢ 4). Let S be the set of path sets {w_{1}, …, w_{n}} such that

1. Each w_{i} is a T^{w}-model;

2. If i ≠ j, then w_{i}, w_{j} are disjoint;

3. If 1 ∈ w_{i} and 2 ∈ w_{j}, then i = j; and

4. If 1 ∈ w_{i} and 3 ∈ w_{j}, then i = j.

It is not hard to prove that this is a C, T -computational theory, and that

(g_{1}, g_{2}, g_{3}, g_{4}) ∈ (A ⇒ unit)(T, S)^{w}.

However, it is evident that

(f(g_{1}), f(g_{2}), f(g_{3}), f(g_{4})) ∉ unit(T, S)_{S}^{w}

because of the last two conditions on the path sets. Thus, there is no such definable f.

5 Full Abstraction

We prove full abstraction for FPC by considering a different language called Finite FPC. A model of Finite FPC lives in the same category SR. We prove that all elements of the model of Finite FPC are definable by terms. Terms in Finite FPC have representatives in FPC, which will be used to establish full abstraction.

The proof of full abstraction follows the structure of the proof in [22].

5.1 Finite FPC

Finite FPC is a simplification of FPC. It has types given by the grammar

s, t ::= void | unit | (s ⊕ t) | (s ⊗ t) | (s ⇒ t)

Finite FPC thus differs from FPC in not having recursive types and in having void. The raw terms are given by the grammar

M, N, P ::= x | Ω | (λx : t. M) | (M N) | ⟨⟩ |
⟨M, N⟩ | (proj_{i} M) | (inj_{i} M) |
(case M of inj_{1}(x).N or inj_{2}(x).P)

Note that there is no recursion on terms in the language, only a divergent term Ω at all types. Rules for deriving typing judgements are as in Table 1 with three exceptions: the rules for elim and intro are omitted and the rule for divergence

Γ ⊢ Ω : s

is added. The language has the evident interpretation in the category SR using the objects and morphisms described in the previous section.

5.2 Construction of relation

To prove that all elements of the model of Finite FPC are representable by terms, we will consider a particular index category C, particular Ctermination theory T, and particular C, T -computational theory S. Define the index category to be the set of sets of the form

[s_{1}, …, s_{n}] = |[[s_{1}]] ⊗ … ⊗ [[s_{n}]]|.

Morphisms are the projections [s_{1}, …, s_{n+k}] → [s_{1}, …, s_{n}]. For any object w = [s_{1}, …, s_{n}] of C, let s = (s_{1} ⊗ … ⊗ s_{n}) and

X^{w} = { w′ ⊆ w | there is a closed M : (s ⇒ unit) such that [[M]](d)↓ iff d ∈ w′ }.

The path sets in S^{w} are defined by

{w_{1}, …, w_{k}} is a path set
if there is an M : (s ⇒ k̄) such that [[M]](d) = i iff d ∈ w_{i},

where

n̄ = \underbrace{(unit ⊕ … ⊕ unit)}_{n}

and 1 = inj_{1}(⊤), 2 = inj_{2}(inj_{1}(⊤)), and so on. It is then not hard to establish the following

Lemma 7 The set X = { X^{w} | w ∈ Obj(C) } defines a C-termination theory T by taking X^{w} to be a set of models. Moreover, S is a C, T - computational theory.

The proof uses the alternative characterization of T -models given by Proposition 3.

The next lemma is the main one needed for full abstraction. It proves that every element of the computational relations is represented by a term in Finite FPC.

Lemma 8 Suppose w = [s_{1}, …, s_{n}] and s = (s_{1} ⊗ … ⊗ s_{n}). Then g ∈ [[t]](T, S)_{S}^{w} iff there exists a closed M : (s ⇒ t) such that g = [[M]].

The proof proceeds by induction on the structure of t.

5.3 Main results

Theorem 9 (Adequacy) Suppose M is a closed FPC term of type s. Then

M ⇓ V iff [[M]]↓ .

Proof: (Sketch) A standard inclusive predicates argument; see [26] for the outline of the proof.

Theorem 10 (Full Abstraction) Suppose M, N are FPC terms. Then

[[M]] ⊑ [[N]] iff M ⊑_{F P C} N.

Proof: (Sketch) The difficult direction to prove is the (⇐) direction. Suppose M, N : s and [[M]] ⋢ [[N]]. Then there exist closed terms P_{n}^{s} : s → s^{n}, where s^{n} is a Finite FPC type, such that [[P M]] ⋢ [[P N]] (any void’s in the type s^{n} are replaced by (rec α. α)). The terms P_{n}^{s} are also used in [30]. By Lemma 8, there exists an f ∈ [[s^{n} ⇒ unit]] such that f([[P M]]) is defined and f([[P N]]) is not. We know by the concreteness condition that

g = (\underline{λ}d ∈ [ ]. f) ∈ [[s^{n} ⇒ unit]](T, S)^{[]}.

Thus, g is definable by a term Q : (unit ⇒ s^{n} ⇒ unit). Then the context C[·] = (Q ⟨⟩ (P [·])) distinguishes M and N, completing the proof.

6 Related Work

We have shown how to construct a fully abstract model for call-by-value FPC. It is the first model of a call-by-value language, or one with sums, or one with recursive types to use the logical-relations approach pioneered by Sieber. Our model also supports a simple form of reasoning for showing that certain values are not definable, and yields insight into the structure of sequential computation.

There are other ways to build fully abstract models for FPC. For instance, Riecke and Viswanathan [31, 32] give a dcpo-based model for call-by-value FPC. The construction uses Milner’s syntactic methods of [16]. This construction sheds little light into the structure of FPC, except that the model validates least fixpoint reasoning.

Games semantics has also been applied to full abstraction questions for FPC. In [15], McCusker builds a model of call-by-name FPC. The sums in this model are separated: applying the injection operations to the meaning of a divergent computation returns a convergent value (on which a case expression can branch).

Until recently, it was not known how to adopt games models to the call-by-value setting. Honda and Yoshida have bridged that gap, devising a model for call-by-value PCF using games semantics [9]. The model loosens the restrictions of the original games semantics [2, 10, 20] to include strategies that start with the opponent’s answer rather than a question. Intuitively, this means that the value supplied to a call-by-value function is immediately available without interrogation by the player. The basic definitions are quite different from our logical-relations-based model, and the games model sheds light on the process nature of sequentiality.

7 Discussion

Much of the complexity of our model of FPC lies in the use of Kripke relations. On the one hand, since all examples of reasoning in the model seem to require only the “base” relations, it would be interesting to determine when base relations were sufficient. This kind of result might be analogous to Sieber’s result that sequentiality relations suffice for proving facts about PCF up to third-order types [33]. On the other hand, recent results of Ralph Loader suggest that one must go beyond base relations to achieve full abstraction. We conjecture that the following problem is undecidable: given a type in Finite FPC, can one decide how many elements there are in the model of that type? If we remained only with the “base” relations, the problem would be decidable. The related decision problem for PCF was first pointed out in [12]; see [11, 22] for a further discussion. Loader shows that the decision problem for PCF over the single boolean base type is undecidable [14]. We expect that the proof will carry over to Finite FPC.

We have some hope that the relational account can be adapted to extensions of FPC with other kinds of effects other than simple functional branching, such as continuation-based control operations. We also believe that there is a relationship between “single-threading” of state [21, 23] and sequentiality; it would be interesting to see if our model can be adapted to model a single-threaded global state. One strength of the current model is its clean separation of values and computations. We conjecture that only the definition of “computational relations” must change to reflect the new settings.

Other extensions seem more difficult. For instance, we began by trying to find a similar relation-based model for a linear type system, but ran into technical difficulties. Extending FPC with a notion of local state, as in Idealized Algol [28] or Standard ML [17], also seems to be difficult. One interesting, though non-trivial, direction would be to extend the language with parametric polymorphism. A different kind of relations would be needed in this instance to model parametricity.

Acknowledgements: The first author thanks the organizers of the Semantics of Computation program at the Newton Institute for Mathematical Sciences, Cambridge, UK where this work was begun. The second author thanks Bell Laboratories for offering a very stimulating and pleasant environment during his visit in the summer of 1996. We also thank Thomas Hildebrandt, Leonid Libkin, Rona Machlin, Peter O’Hearn, Riccardo Pucella, and the anonymous referees for comments.

References

[1] S. Abramsky and A. Jung. Domain theory. In S. Abramsky, D. M. Gabbay, and T. S. E. Maibaum, editors, Handbook of Logic in Computer Science, volume 3, pages 1–168. Clarendon Press, 1994.

[2] S. Abramsky, P. Malacaria, and R. Jagadeesan. Full abstraction for PCF (extended abstract). In M. Hagiya and J. Mitchell, editors, Theoretical Aspects of Computer Software, number 789 in Lect. Notes in Computer Sci., pages 1–15. Springer-Verlag, 1994.

[3] E. Astesiano and G. Costa. Nondeterminism and fully abstract models. RAIRO, 14(4):323–347, 1980.

[4] P.-L. Curien. Categorical Combinators, Sequential Algorithms and Functional Programming. John Wiley & Sons, 1986.

[5] P.-L. Curien and A. Obtułowicz. Partiality, cartesian closedness, and toposes. Information and Computation, 80:50–95, 1989.

[6] P. J. Freyd. Algebraically compact categories. In A. Carboni, M. C. Pedicchio, and G. Rosolini, editors, Como Category Theory Conference, volume 1488 of Lect. Notes in Math., pages 95–104. Springer-Verlag, 1991.

[7] J.-Y. Girard. Une extension de l’interprétation de Gödel à l’analyse, et son application à l’élimination des coupures dans l’analyse et la théorie des types. In J. E. Fenstad, editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63–92. North-Holland, 1971.

[8] C. A. Gunter. Semantics of Programming Languages: Structures and Techniques. MIT Press, 1992.

[9] K. Honda and N. Yoshida. Game theoretic analysis of callby-value computation. Unpublished manuscript available from “http://hypatia.dcs.qmw.ac.uk”, 1997.

[10] J. M. E. Hyland and C.-H. L. Ong. Pi-calculus, dialogue games and PCF. In 7th Annual ACM Conference on Functional Programming Languages and Computer Architecture, La Jolla, California, 1995.

[11] A. Jung, M. Fiore, E. Moggi, P. W. O’Hearn, J. G. Riecke, G. Rosolini, and I. Stark. Domains and denotational semantics: History, accomplishments, and open problems. Bulletin of the European Association for Theoretical Computer Science, pages 227–256, June 1996.

[12] A. Jung and A. Stoughton. Studying the fully abstract model of PCF within its continuous function model. In Typed Lambda Calculi and Applications, volume 664 of Lect. Notes in Computer Sci., pages 230–244. Springer-Verlag, 1993.

[13] A. Jung and J. Tiuryn. A new characterization of lambda definability. In Typed Lambda Calculi and Applications, volume 664 of Lect. Notes in Computer Sci., pages 245–257. Springer-Verlag, 1993.

[14] R. Loader. Finitary PCF is not decidable. Unpublished manuscript available from “http://hypatia.dcs.qmw.ac.uk”, 1996.

[15] G. McCusker. Games and full abstraction for FPC. In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 174–183, 1996.

[16] R. Milner. Fully abstract models of the typed lambda calculus. Theoretical Computer Sci., 4:1–22, 1977.

[17] R. Milner, M. Tofte, and R. Harper. The Definition of Standard ML. MIT Press, 1990.

[18] E. Moggi. Notions of computation and monads. Information and Control, 93:55–92, 1991.

[19] K. Mulmuley. Full Abstraction and Semantic Equivalence. ACM Doctoral Dissertation Award 1986. MIT Press, 1987.

[20] H. Nickau. Hereditarily sequential functionals. In Proceedings of the Symposium on Logical Foundations of Computer Science: Logic at St. Petersburg, Lect. Notes in Computer Sci. Springer-Verlag, 1994.

[21] P. W. O’Hearn and J. C. Reynolds. From Algol to polymorphic linear lambda calculus. Lectures at Isaac Newton Institute for Mathematical Sciences, Cambridge, UK, 1995.

[22] P. W. O’Hearn and J. G. Riecke. Kripke logical relations and PCF. Information and Computation, 120(1):107–116, 1995.

[23] P. W. O’Hearn and R. D. Tennent. Parametricity and local variables. J. ACM, 42:658–709, 1995.

[24] A. M. Pitts. Relational properties of domains. Information and Computation, 127:66–90, 1996.

[25] G. D. Plotkin. LCF considered as a programming language. Theoretical Computer Sci., 5:223–257, 1977.

[26] G. D. Plotkin. (Towards a) logic for computable functions. Unpublished manuscript, CSLI Summer School Notes, 1985.

[27] J. C. Reynolds. Towards a theory of type structure. In Proceedings Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408–425, Berlin, 1974. Springer-Verlag.

[28] J. C. Reynolds. The essence of Algol. In J. W. de Bakker and J. C. van Vliet, editors, Algorithmic Languages, pages 345–372. North-Holland, Amsterdam, 1981.

[29] J. G. Riecke. Fully abstract translations between functional languages. Mathematical Structures in Computer Science, 3:387–415, 1993. Preliminary version appears in Conference Record of the Eighteenth Annual ACM Symposium on Principles of Programming Languages, pages 245–254, ACM, 1991.

[30] J. G. Riecke and R. Subrahmanyam. Extensions to type systems can preserve operational equivalences. In M. Hagiya and J. C. Mitchell, editors, Proceedings of 1994 International Symposium on Theoretical Aspects of Computer Software, volume 789 of Lect. Notes in Computer Sci., pages 76–95. Springer-Verlag, 1994.

[31] J. G. Riecke and R. Viswanathan. Full abstraction for call-by-value sequential languages. Unpublished manuscript, 1993.

[32] J. G. Riecke and R. Viswanathan. Isolating side effects in sequential languages. In Conference Record of the Twenty-Second Annual ACM Symposium on Principles of Programming Languages, pages 1–12. ACM, 1995.

[33] K. Sieber. Reasoning about sequential functions via logical relations. In Applications of Categories in Computer Science, volume 177 of London Mathematical Society Lecture Note Series. Cambridge University Press, 1992.

[34] A. Stoughton. Fully Abstract Models of Programming Languages. Research Notes in Theoretical Computer Science. Pitman/Wiley, 1988. Revision of Ph.D thesis, Dept. of Computer Science, Univ. Edinburgh, Report No. CST-40-86, 1986.

[35] W. Wechler. Universal Algebra for Computer Scientists. Number 25 in EATCS Monographs in Theoretical Computer Science. Springer-Verlag, 1992.

Recent BRICS Report Series Publications

RS-97-41 Jon G. Riecke and Anders B. Sandholm. A Relational Account of Call-by-Value Sequentiality. December 1997. 24 pp. Appears in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, pages 258–267.

RS-97-40 Harry Buhrman, Richard Cleve, and Wim van Dam. Quantum Entanglement and Communication Complexity. December 1997. 14 pp.

RS-97-39 Ian Stark. Names, Equations, Relations: Practical Ways to Reason about ‘new’. December 1997. ii+33 pp. This supersedes the earlier BRICS Report RS-96-31. It also expands on the paper presented in Groote and Hindley, editors, Typed Lambda Calculi and Applications: 3rd International Conference, TLCA ’97 Proceedings, LNCS 1210, 1997, pages 336–353.

RS-97-38 Micha� Hańćkowiak, Micha� Karoński, and Alessandro Panconesi. On the Distributed Complexity of Computing Maximal Matchings. December 1997. 16 pp. To appear in The Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’98.

RS-97-37 David A. Grable and Alessandro Panconesi. Fast Distributed Algorithms for Brooks-Vizing Colourings (Extended Abstract). December 1997. 20 pp. To appear in The Ninth Annual ACM-SIAM Symposium on Discrete Algorithms, SODA ’98.

RS-97-36 Thomas Troels Hildebrandt, Prakash Panangaden, and Glynn Winskel. Relational Semantics of Non-Deterministic Dataflow. December 1997. 21 pp.

RS-97-35 Gian Luca Cattani, Marcelo P. Fiore, and Glynn Winskel. A Theory of Recursive Domains with Applications to Concurrency. December 1997. ii+23 pp.

RS-97-34 Gian Luca Cattani, Ian Stark, and Glynn Winskel. Presheaf Models for the π-Calculus. December 1997. ii+27 pp. Appears in Moggi and Rosolini, editors, Category Theory and Computer Science: 7th International Conference, CTCS ’97 Proceedings, LNCS 1290, 1997, pages 106–126.

RS-97-33 Anders Kock and Gonzalo E. Reyes. A Note on Frame Distributions. December 1997. 15 pp.