BRICS RS-99-10 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-99-10 ISSN 0909-0878 March 1999 Copyright \begin{matrix}c \\ ◯ \end{matrix} 1999, Jon G. Riecke & Anders B. Sandholm.

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/99/10/

A Relational Account of Call-by-Value Sequentiality^{∗}

Jon G. Riecke Bell Laboratories Lucent Technologies 700 Mountain Avenue Murray Hill, NJ 07974, USA

Anders Sandholm BRICS^{†}, Department of Computer Science University of Aarhus Ny Munkegade, Bldg. 540 DK-8000 Aarhus C, Denmark

March, 1999

Abstract We construct a model for FPC, a purely functional, sequential, callby-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 (1977), who pointed out that certain elements in Scott models are not definable. In Plotkin’s example, the function

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 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. Of course, there are other elements in the Scott model of PCF that cannot be programmed: the domains have uncountably many elements. Nevertheless, the por function causes problems for reasoning about programs: it causes two terms in the language PCF to be distinct denotationally even though the terms cannot be distinguished by any program.

∗A preliminary version of this paper appeared in Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, pages 258–267. IEEE Computer Society Press, 1997.

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

The problem of modelling sequentiality 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 por 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.

When examples like por do not exist, the denotational model is said to be fully abstract. More precisely, full abstraction requires an operational definition of equivalence (interchangeability in all programs) to match operational equivalence. Shortly after Plotkin’s paper, Milner proved that there was exactly one fully abstract model of PCF meeting certain conditions (Milner, 1977). Until recently, all descriptions of this fully abstract model have used operational semantics (see, for instance, (Mulmuley, 1987; Stoughton, 1988)). New constructions using logical relations (O’Hearn and Riecke, 1995; Sieber, 1992) have yielded a more abstract understanding of Milner’s model. Game semantics (Abramsky et al., 1994; Hyland and Ong, 1995; Nickau, 1994) has also been used to give other semantic constructions of fully abstract models of PCF, even though it is still open whether these models are isomorphic to Milner’s model.

This paper adapts and extends the logical-relations model for PCF to a call-by-value setting. More precisely, 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. First, FPC can be regarded as the purely functional, non-polymorphic sublanguage of Standard ML (Milner et al., 1997): 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. Second, FPC can serve as an expressive metalanguage for denotational semantics (Gunter, 1992; Plotkin, 1985). 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 (Riecke, 1993) from a language into FPC, the model of FPC yields a fully abstract model of the language.

There is another, purely technical reason to be interested in FPC: since it contains only one trivial base type, we can learn more about the structure of Sieber’s logical relations by studying FPC. Sieber’s model of PCF, and the fully abstract model of PCF using Kripke relations (O’Hearn and Riecke, 1995), begin from a set of n-ary relations (for all n) at a flat base type—i.e., where the convergent elements of the domain are unordered. PCF thus builds in a limited form of sum type, available only at the base type. When we decompose that base type into a sum of the primitive base type, we may learn more about the nature of sequential computation.

As a preview to seeing how our relations decompose Sieber’s, it is helpful to recall Sieber’s definition. 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}. Sieber’s sequentiality relations have an elegant semantic definition: nothing in the definition refers to the terms or operations of PCF. The relations can be used in simple proofs of the non-definability of elements, since all PCF terms preserve the sequentiality relations. For instance, it is easy to show that por does not preserve the sequentiality relation S_{{1,2},{1,2,3}}^{3}, and hence it must not be definable. The relations also seem to say something about sequential computation: if certain elements of a tuple must converge, then other elements must converge.

On a technical level, Sieber’s definition of “sequentiality relation” seems limited to flat base types. It is difficult to see how, for instance, to extend the definition to complex sums such as int⊕(int ⇒ int), since it does not make sense to check for equality at functional type. 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, 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 syntax and operational semantics of FPC. 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 (O’Hearn and Riecke, 1995) and lift the relations to Kripke relations of varying arity (Jung and Tiuryn, 1993). We then define a category, in which the objects have partial-order as well as relational structure, and in which the morphisms preserve the partial-order and relational structure of objects. A model of FPC lives inside this category. The Kripke relations are then used to establish the full abstraction of the model.

2 The Language FPC

FPC is a call-by-value, purely functional language with single base type unit, sums, products, functions, and recursive types (Gunter, 1992; Plotkin, 1985).

Our version of FPC has types given by the grammar

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

where α ranges over a collection of type variables. This version of FPC has one more base type, namely void, than the standard version of FPC. The type void stands for the type with no convergent elements, and can be represented by the type (rec α. α), but having an explicit name makes some of the notation simpler. Types are identified up to renaming of type variables bound by rec. We assume that all types appearing in terms and the typing rules are closed unless otherwise noted.

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 ofinj_{1}(x).N orinj_{2}(x).P) |

                       (intro_{rec α. s} M) | (elim_{rec α. s} M)

Ω denotes a divergent term, and only appears in our version of FPC in order to make the proofs simpler. 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.

Evaluation rules, written in natural style, 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. We write M ⇓ if there is a term V such that M ⇓ V, and M ⇑ if there is no such V. The operational approximation relation can then be defined as follows:

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

FPC is a sparse language, but it still has enough computing power for many applications. For instance, Plotkin (1985) and Gunter (1992) show how to build recursion operators using recursive types. One can encode a sequencing operation in FPC: (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 (Girard, 1971; Reynolds, 1974)), which precludes a good representation of abstract data types.

3 Category of Meanings

This section defines a category suitable for interpreting FPC, and gives various constructions for defining the meaning of types and terms. Objects in the Table 1: Type Rules for FPC.

Γ, x : t ⊢ x : t

Γ ⊢ Ω : s
Γ ⊢ ⟨⟩ : 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 ofinj_{1}(x).N_{1} orinj_{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 ofinj_{1}(x).N_{1} orinj_{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}

category will have both partial-order structure and relational structure. More precisely, the objects are composed of dcpo’s, i.e., directed-complete posets not necessarily possessing a least element, and relations on those dcpo’s. The morphisms of the category preserve the dcpo structure (i.e., are partial, continuous functions), and preserve the relational structure (a property we call uniformity). The formal definitions of dcpo and continuity may be found elsewhere (Gunter and Scott, 1990; Plotkin, 1985).

The construction consists of five main parts:

1. Definition of the relational structures (Sections 3.2-3.3).

2. Definition of the category, and the verification that it is a dcpo-enriched category (Section 3.4).

3. Definitions of meanings for void, unit as objects in the category, and of tensor product ⊗, coproduct ⊕, and function space ⇒ as functors, and verification that they satisfy certain conditions (Sections 3.5-3.6).

4. Verification that the category is “partial cartesian closed” (defined below), and hence a model of FPC without recursive types (Section 3.7).

5. Construction of colimits, and verification that the colimits produce objects in the category (Section 3.8).

Most of the proofs are straightforward and follow well-established patterns from category theory.

3.1 Preliminaries

Given two sets X, Y, the set (X ⊕ Y) is the disjoint union, (X × Y) is the cartesian product, [X →_{t} Y] is the set of total functions from X to Y, and [X →_{p} Y] is the set of partial functions from X to Y. The identity function on a set X is denoted id_{X}, and (h; f) denotes the diagrammatic composition of two functions h and f. The functions inj_{i} : X_{i} → (X_{1} ⊕ X_{2}) are the injection functions into the disjoint sum, and proj_{i} : (X_{1} × X_{2}) → X_{i} are the projection functions from the cartesian product. For products, we abuse notation and use ⟨x, y⟩ for elements of X × Y and ⟨f, g⟩ for functions W → (X × Y) when f : W → X and g : W → Y.

Partial functions require some special notation. We write f(d) ↓ when a partial function f is defined on argument d, and f(d)↑ when f(d) is undefined. Kleene equality takes definedness between mathematical expressions into account: we write exp_{1} ≃ exp_{2} if, whenever one side is defined, both sides are defined and equal. Similarly, we extend an ordering relation ⊑ to \begin{matrix}⊏ \\ ∼ \end{matrix} as follows: exp_{1} \begin{matrix}⊏ \\ ∼ \end{matrix} exp_{2} if, when exp_{1} is defined and equal to e_{1}, then exp_{2} is defined and equal to some e_{2} and e_{1} ⊑ e_{2}.

Following Jung and Tiuryn, we often represent the elements of relations as finite, total functions from indices to values instead of tuples of values; this simplifies some of the definitions and proofs (Jung and Tiuryn, 1993; O’Hearn and Riecke, 1995).

3.2 Termination and path theories

There are two kinds of relations in the model, termination relations and computational relations.

The first kind of relation uses subsets of indices generated from simple implicational theories. If w is a finite set of indices, then a w-termination theory is a set of implications of the form (w′ ⊢ d) where d ∈ w and w′ is a subset of w. Intuitively, each implication states a property similar to the Sieber’s sequentiality relations: if a function halts on the indices in the premise, it must halt on the index in the conclusion. Indeed, the termination part of Sieber’s relations S_{A,B}^{n} can be encoded using implications:

if A ⊆ B ⊆ w = {1, …, n} and B \ A = {d_{1}, …, d_{k}},
then S_{A,B}^{w} corresponds to the implications (A ⊢ d_{1}), …, (A ⊢ d_{k}).

The subsets of w that validate the implications in the theory are the building blocks of termination relations. Suppose w′ ⊆ w; then we say that w′ validates (w′′ ⊢ d), written w′ ⊧ (w′′ ⊢ d), if w′′ ⊆ w′ implies d ∈ w′. If T is a wtermination theory, 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. Suppose w is a finite set and X ⊆ 𝒫(w). Then X is a closure system if w ∈ X and X is closed under intersection. A closure system determines a w-termination theory:

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

Proof: (⇐) Suppose T is a w-theory. Then obviously w is a T -model. To see closure under intersection, suppose w_{1}, w_{2} are T -models. Suppose (w′ ⊢ d) ∈ T, and w′ ⊆ w_{1} ∩ w_{2}. Then d ∈ w_{1} and d ∈ w_{2}, hence d ∈ w_{1} ∩ w_{2}. Thus, w_{1} ∩ w_{2} is also a T -model.

(⇒) Suppose X is a closure system. Define the theory T by

(w′′ ⊢ d) ∈ T iff for all w′ ∈ X, w′ ⊧ (w′′ ⊢ 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 validates 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′. Now consider the formula (w′ ⊢ d). Note that (w′ ⊢ d) ∈ T, and w′ |̸= (w′ ⊢ d). Thus, w′ ∉ Y, completing the proof.

(See (Wechler, 1992), page 22 for the same 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 (Sieber, 1992).

The second kind of relation is built from sets of sets of T -models. If T is a wtermination theory, define a path set to be a set {w_{1}, …, w_{n}} of nonempty, disjoint T -models. (The reason for the name “path set” will become clear shortly.) By convention, when we write a path set we assume there are no duplicates. For example, when we write the path set {w_{1}, …, w_{n}}, each w_{i} differs from the others. A T -path theory S is a set of path sets that satisfies the following conditions:

• {} ∈ S (using the alternative notation for the empty set);

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

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

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

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

This definition appears to be related to the notion of a Grothendieck topology (Fiore and Simpson, 1999).

3.3 Relations

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

such that the following properties hold:

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

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

There is a subtle point in the definition of the ⊑ relation: only elements of R that have the same domain can be related. One might imagine a different definition, with “tuples” in the relations being partial functions whose domains are T -models. Under this alternative definition, two tuples might be related by ⊑ even if they had different domains. The definition of ⊗ on relations does not produce a directed complete relation, however, using this alternative definition.

The second form of relations, computational relations, is built from path theories. These relations lift a termination relation to a partial function on indices. Suppose S is a T -path theory and R is a T -termination relation on D. The computational relation R_{S} is defined 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 \}

In this case, the order relation on elements of R_{S} is defined in the usual way:

f ⊑ g if whenever f(d)↓, then g(d)↓ and f(d) ⊑ g(d).

The computational relations are reminiscent of Moggi’s analysis of call-by-value via monads (Moggi, 1991), and they will play a similar role in the semantics below.

These definitions have a common intuition of “tests” that one can apply to a function, with the tests designed so that only sequential functions will pass all tests. In this case, a test consists of a number of simultaneous applications of the function to arguments, where the arguments must also pass the test. Termination theories are used to test the termination behavior of functions; path theories are used to test the consistency of the branching structure of functions.

For example, let bool denote the FPC type (unit ⊕ unit) and true,false denote the terms (inj_{1}⟨⟩), (inj_{2}⟨⟩), and consider the term

              f = (λx : bool. if x thenfalseelsetrue).

Suppose we pick the termination theory {1, 2 ⊢ 3}. For the function f to pass a test determined by this termination theory, we must apply it to three arguments themselves satisfy the test. Such a test of three arguments might be, for instance, the tuple true, true, true. When the function is applied to three arguments, the result is false, false, false. All three answers terminate, so this test of the function succeeds. The test true, true, Ω does not yield a successful test: the function returns false, false, and diverges respectively. Fortunately, however, the arguments themselves do not pass the test themselves, so the function need not satisfy this test.

Tests of the branching behavior of functions using the path theories are similar. 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. For example, suppose the termination theory is as above, and that the path theory contains the set {{1}, {2}, {3}}. Then the function need not return consistent results given three arguments, but the function must halt on all three arguments.

We can now see from where the four conditions on path theories come. The first condition says that the empty set is a valid test; the second says that a potential path set that does no branching is a valid path set; the third says path sets can be combined; the fourth 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.4 Definition of the category

One could build a category from termination and path theories, but the result would probably not contain a fully abstract model of FPC (see the discussion in Section 7). Instead, we extend the relations to Kripke relations of varying arity (Jung and Tiuryn, 1993). 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). Suppose 𝒞 is an index category. A 𝒞termination theory T is an Ob(𝒞)-indexed family of w-termination theories T^{w} such that, for any φ : v ⟶^{𝒞} w, if w′ is a T^{w}-model, then φ^{−1}(w′) is a T^{v}-model, where φ^{−1}(w′) = {d ∈ v | φ(d) ∈ w′}. A Kripke relation is a set of termination relations that must fit together. Let 𝒞 be an index category, T be a 𝒞-termination theory, and D be a dcpo. A family R is a 𝒞, T -termination relation on D if R is an Ob(𝒞)-indexed family of T^{w}-termination relations R^{w} on D satisfying the

Kripke monotonicity condition: For any f ∈ R^{w} with domain w′ and

φ : v ⟶^{𝒞} w, then (\underline{λ}d ∈ v′. f(φ(d))) ∈ R^{v}, where v′ = φ^{−1}(w′).

Path theories also extend straightforwardly to the Kripke case. Let 𝒞 be an index category and T be a 𝒞-termination theory. Then S is a 𝒞, T -path theory if S is a family, indexed by objects w of 𝒞, of T^{w}-path theories. If S is a 𝒞, T - path theory and R is a 𝒞, T -termination relation on D, we let R_{S}^{w} denote the computational relation built from R^{w} and S^{w}.

We now have enough machinery to build the category ℛ𝒞𝒫𝒪 (for dcpo’s with relational structure).

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

Concreteness Condition: For any a ∈ |A|, (\underline{λ}d ∈ w. a) ∈ A(T, S)^{w}.

• Morphisms. A morphism f : A → B is a partial continuous function f : |A| →_{p} |B| satisfying the

Uniformity Condition: For all 𝒞, 𝒞-termination theories T, 𝒞, T - path theories S, and h ∈ A(T, S)^{w}, (h; f) ∈ B(T, S)_{S}^{w}.

The definitions of composition and identities are the same as on partial continuous functions. It is straightforward to check that ℛ𝒞𝒫𝒪 is indeed a category; the only non-obvious step is checking that composition produces uniform functions, which follows from

Lemma 3.2 If f ∈ A(T, S)_{S}^{w} and g : A → B, then (f; g) ∈ B(T, S)_{S}^{w}.

Proof: By definition, there exists a path set {w_{1}, …, w_{n}} such that f(d) ↓ iff d ∈ w_{i} for some i and (\underline{λ}d ∈ w_{i}. f(d)) ∈ A(T, S)^{w} for all i. By the uniformity of g, for all i, h_{i} = ((\underline{λ}d ∈ w_{i}. f(d)); g) ∈ B(T, S)_{S}^{w}. Thus, for all i, there exists a path set {w_{i,1}, …, w_{i,k_{i}}} such that

• h_{i}(d)↓ iff d ∈ w_{i,j} for some j; and

• (\underline{λ}d ∈ w_{i,j}. h_{i}(d)) ∈ B(T, S)^{w} for all j.

Note that each w_{i,j} ⊆ w_{i}, since the domain of h_{i} is a subset of w_{i}. Thus, by the properties of path sets, {w_{1,1}, …, w_{n,k_{n}}} is a path set. Note also that g(f(d))↓ iff d ∈ w_{i,j} for some i, j, and (\underline{λ}d ∈ w_{i,j}. g(f(d))) ∈ B(T, S)^{w} for all i, j. Thus, (f; g) ∈ B(T, S)_{S}^{w}.

Moreover, the category is dcpo-enriched, i.e., under the usual pointwise ordering of morphisms with f ⊑ g iff for any a ∈ |A|, f(a) \begin{matrix}⊏ \\ ∼ \end{matrix} g(a), the set of morphisms from A to B Hom_{ℛ𝒞𝒫𝒪} (A, B) is a dcpo. The proof of this fact, stated precisely as Proposition 3.5 below, requires two lemmas:

Lemma 3.3 Suppose f ∈ A(T, S)_{S}^{w} with path set W = {w_{1}, …, w_{k}}. Suppse W′ = {w′_{1}, …, w′_{l}} ∈ S, and ⋃ W = ⋃ W′. Then W ⊓ W′ = W′′ = {w′′_{1}, …, w′′_{m}} is also a path set for f. That is, d ∈ w′′_{i} iff f(d) ↓ and for all i, (\underline{λ}d ∈ w′′_{i}. f(d)) ∈ A(T, S)^{w}.

Proof: It is easy to see that ⋃ W′′ = ⋃ W, and hence it follows that d ∈ w′′_{i} ∈ W′′ iff f(d)↓.

Lemma 3.4 If A(T, S) is a 𝒞, T -relation on A, then A(T, S)_{S}^{w} is directed complete.

Proof: Suppose X = {f_{i} | i ∈ I} is directed in A(T, S)_{S}^{w}, and f = (⨆ X). Then for all i, there exists a path set σ_{i} = {w_{i,1}, …, w_{i,k_{i}}} such that f_{i}(d) ↓ iff d ∈ w_{i,j} for some j, and (\underline{λ}d ∈ w_{i,j}. f_{i}(d)) ∈ A(T, S)^{w} for all j. Note that if f_{i}, f_{j} ∈ X, then there is an f_{l} such that f_{i}, f_{j} ⊑ f_{l} (by directedness), and hence ⋃ σ_{i}, ⋃ σ_{j} ⊆ ⋃ σ_{l}. Since each ⋃ σ_{i} is a subset of the finite set w, there is a k such that for all f_{i} ⊒ f_{k}, ⋃ σ_{i} = ⋃ σ_{k}.

Let w′ = ⋃ σ_{k}. It is easy to see that d ∈ w′ iff f(d) ↓. What we need to show is that w′ can be subdivided into a set of disjoint sets that forms a path set, and that this path set “witnesses” the membership of f in A(T, S)_{S}^{w}. There are only finitely many distinct path sets W_{1}, …, W_{k} for the f_{i}’s above f_{k} such that for all i, ⋃ W_{i} = w′. Define

W = W_{1} ⊓ W_{2} ⊓ … ⊓ W_{k}.

By Lemma 3.3, W is a path set for f. Now, note that

f = ⋃\{⨆\{(\underline{λ}d ∈ w_{j}. f_{i}(d)) | f_{i} ⊒ f_{k}\} | w_{j} ∈ W \}

By the directed completeness of A(T, S)^{w}, for any w_{j} ∈ W,

⨆\{(\underline{λ}d ∈ w_{j}. f_{i}(d)) | f_{i} ⊒ f_{k}\} ∈ A(T, S)^{w}.

Thus, f ∈ A(T, S)_{S}^{w}.

Proposition 3.5 Hom_{ℛ𝒞𝒫𝒪} (A, B) is a dcpo.

Proof: Suppose X = {f_{i} | i ∈ I} ⊆ Hom_{ℛ𝒞𝒫𝒪} (A, B) is directed. We need to show that (⨆ X) is uniform; it is routine to show that it is continuous. Suppose h ∈ A(T, S)^{w}. By the uniformity of each f_{i}, (h; f_{i}) ∈ B(T, S)_{S}^{w}. It is easy to see that { (h; f_{i}) | i ∈ I } is directed. Thus, by Lemma 3.4, (h; (⨆ X)) ∈ B(T, S)_{S}^{w}.

3.5 Tensor products and coproducts

The category admits certain standard constructions. For instance, it is easy to show that void and unit, defined by

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

are objects in the category. The relational component of unit captures much of the intuition embedded in termination relations: elements in the termination relation are functions which terminate precisely on elements in a T^{w}-model.

The category has a notion of tensor product. Suppose A, B are objects, and f : A → B and g : C → D are morphisms. Define

|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 the same domain}
(f ⊗ g)⟨x, y⟩ = ⟨f(x), g(y)⟩

Proposition 3.6 (– ⊗ –) is a bifunctor on ℛ𝒞𝒫𝒪, covariant in both arguments.

Proof: The only non-obvious part is checking that the relations generated by ⊗ is directed complete. Suppose X = {f_{i} | i ∈ I} ⊆ (A ⊗ B)(T, S)^{w} is directed. Then all of the elements of X have the same domain, say w′ (which is a T^{w}- model). Note that there exist g_{i} ∈ A(T, S)^{w} and h_{i} ∈ B(T, S)^{w} such that f_{i} = ⟨g_{i}, h_{i}⟩. Therefore, it must be the case that the sets

X_{1} = {g_{i} | i ∈ I} X_{2} = {h_{i} | i ∈ I}

are directed. By hypothesis, ⨆ X_{1} ∈ A(T, S)^{w} and ⨆ X_{2} ∈ B(T, S)^{w}. Since (⨆ X) = ⟨⨆ X_{1}, ⨆ X_{2}⟩, (⨆ X) ∈ (A ⊗ B)(T, S)^{w}.

The proof of Proposition 3.6 requires that directed sets in (A ⊗ B)(T, S)^{w} have the same domain, which explains the definition earlier of the order on elements of termination relations.

The category also has coproducts in the usual sense. Suppose A, B are objects, and f : A → B and g : C → D are morphisms. Define

|A ⊕ B| = |A| ⊕ |B| (disjoint union)
(A ⊕ B)(T, S)^{w} = { (g; inj_{1}) | g ∈ A(T, S)^{w} } ∪ { (g; inj_{2}) | g ∈ B(T, S)^{w} }
(f ⊕ g)(x : A ⊕ C) = \{ \begin{matrix}f(y) & if x = inj_{1}(y) \\ g(y) & if x = inj_{2}(y) \end{matrix}

This definition yields the coproduct in the category, as the following proposition shows.

Proposition 3.7 ℛ𝒞𝒫𝒪 has coproducts.

Proof: It is not hard to prove that ⊕ is a bifunctor on ℛ𝒞𝒫𝒪. To finish the proof that ⊕ yields the coproduct in the category, suppose f : A → C and g : B → C are morphisms. Define

[f, g](d) = \{ \begin{matrix}f(a) & if d = inj_{1}(a) and f(a)↓ \\ g(b) & if d = inj_{2}(b) and g(b)↓ \\ undefined & otherwise \end{matrix}

We need to show that inj_{1} : A → (A ⊕ B), inj_{2} : B → (A ⊕ B), and [f, g] : (A ⊕ B) → C are morphisms in the category, and that [f, g] is the unique morphism making the diagram

\xymatrix{A \ar[r]^{^{inj^{1}}} \ar[dr]_{f} & (A ⊕ B) \ar[d]^{[f,g]} & B \ar[l]_{^{inj^{2}}} \ar[dl]^{g} \\  & C}

commute.

To see that the injections are morphisms, consider the case of inj_{1}. It is obvious that inj_{1} is a partial continuous function, so we only need to verify that inj_{1} satisfies the uniformity condition. Suppose h ∈ A(T, S)^{w} with domain w′ ⊆ w. We need to show (h; inj_{1}) ∈ (A ⊕ B)(T, S)_{S}^{w}. Since w′ is a T^{w}- model, {w′} is itself a path set. It is then easy to see that (h; inj_{1})(d) ↓ iff d ∈ w′, and (\underline{λ}d ∈ w′. (h; inj_{1})(d)) = (h; inj_{1}) ∈ (A ⊕ B)(T, S)^{w} (by definition of (A ⊕ B)(T, S)^{w}). Thus (h; inj_{1}) ∈ (A ⊕ B)(T, S)_{S}^{w}.

To see that [f, g] is a morphism, it is easy to check that [f, g] is a partial continuous function. We need only verify the uniformity condition. Suppose h ∈ (A ⊕ B)(T, S)^{w}; we want to show that (h; [f, g]) ∈ C(T, S)_{S}^{w}. By definition, either h = (h_{1}; inj_{1}) for h_{1} ∈ A(T, S)^{w} or h = (h_{2}; inj_{2}) for h_{2} ∈ B(T, S)^{w}. Consider the first case (the second case is analogous). Then (h; [f, g]) = (h_{1}; f). By uniformity, (h_{1}; f) ∈ C(T, S)_{S}^{w}. Thus, (h; [f, g]) ∈ C(T, S)_{S}^{w}.

What remains to be shown is that [f, g] makes the diagram commute, and that [f, g] is the unique such morphism. We consider the left triangle (the right triangle is analogous). So suppose a ∈ |A|. Observe that f(a) ↓ iff (inj_{1}; [f, g])(a)↓, so if f(a)↓, then

(inj_{1}; [f, g])(a) = f(a)

and hence the triangle commutes. To see the uniqueness of [f, g], suppose that h : (A ⊕ B) → C is such that the diagram commutes, i.e., f = (inj_{1}; h) and g = (inj_{2}; h). Since the injection functions are total functions, the domain of h must be

{d ∈ |A ⊕ B| | (d = inj_{1}(a) and f(a)↓) or (d = inj_{2}(b) and f(b)↓)}.

Thus [f, g] and h have the same domain.

Now suppose h(d) ↓. Suppose d = inj_{1}(a) (the other case is analogous). Then

h(d) = (inj_{1}; h)(a) = f(a) = [f, g](d).

That is, h = [f, g].

3.6 Function space

The category also has an operation associated with a space of functions. Suppose A, B are objects, and f : A → B and g : C → D are morphisms. Define

|A ⇒ B| = Hom_{ℛ𝒞𝒫𝒪} (A, B)
(A ⇒ B)(T, S)^{w} = \{ f | {∀φ : v ⟶^{𝒞} w, g ∈ A(T, S)^{v}. \atop (\underline{λ}d ∈ v. (f(φ(d)) (g(d)))) ∈ B(T, S)_{S}^{v}\}}
(f ⇒ g)(h : B → C) = (f; h; g) : A → D

The definition of function space on relations is the same as the one for Kripke relations (Jung and Tiuryn, 1993; O’Hearn and Riecke, 1995), except that the result of applying related arguments to related results must be in the computational relation, not the termination relation. Again, this is reminiscent of the monad style of semantics (Moggi, 1991).

We must verify that ⇒ is a bifunctor, contravariant in the first argument and covariant in the second. The proof is divided into two parts:

Proposition 3.8 (A ⇒ B) is an object.

Proof: By Proposition 3.5, we know that |A ⇒ B| is directed complete. Suppose 𝒞 is an index category, T is a 𝒞-termination theory, and S is a 𝒞, T -path theory. We need to show that (A ⇒ B)(T, S) is a 𝒞, T -termination relation and the concreteness condition holds.

First, we must show that (A ⇒ B)(T, S) is a 𝒞, T -termination relation. To see directed completeness, suppose X = {f_{i} | i ∈ I} ⊆ (A ⇒ B)(T, S)^{w} is directed. Then all of the elements of X have the same domain, say w′ (which is a T^{w}-model). To see (⨆ X) ∈ (A ⇒ B)(T, S)^{w}, suppose φ : v ⟶^{𝒞} w and h ∈ A(T, S)^{v}. Then for all i ∈ I, g_{i} = (\underline{λ}j ∈ v. f_{i} (φ(j)) (h(j))) ∈ B(T, S)_{S}^{v}. Since {g_{i} | i ∈ I} is directed, by Lemma 3.4 ⨆ g_{i} ∈ B(T, S)_{S}^{v}. Thus,

(\underline{λ}j ∈ v. (⨆ X) (φ(j)) (h(j))) ∈ B(T, S)_{S}^{v}

as needed.

The difficulty lies in showing downward closure and Kripke monotonicity. Suppose f ∈ (A ⇒ B)(T, S)^{w} with domain w′, and suppose w′′ is a T^{w}-model with w′′ ⊆ w′. Let f′ = (\underline{λ}d ∈ w′′. f(d)). To see that f′ ∈ (A ⇒ B)(T, S)^{w}, suppose φ : v ⟶^{𝒞} w and g ∈ A(T, S)^{v}. Then we know that

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

Thus, there is some path set {v_{1}, …, v_{n}} such that h(d)↓ iff d ∈ v_{i} for some i, and for all i,

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

Let h′ = (\underline{λ}d ∈ v. f′ (φ(d)) (g(d))). We need to show that h′ ∈ B(T, S)_{S}^{v}. First, we need to build up the right path set. Notice that v′′ = φ^{−1}(w′′) is a T^{v}- model by the definition of 𝒞-termination theories. Since X = {v_{1}, …, v_{n}} and X′′ = {v′′} are path sets, X ⊓ X′′ = {v′_{1}, …, v′_{k}} is a path set (recall that X ⊓ X′′ is the set of all (v ∩ v′′), with v ∈ X and v′′ ∈ X′′, that are non-empty). It is clear that h′(d) ↓ iff d ∈ v′_{i} for some i. Also, since each v′_{i} ⊆ v_{j} for some j, it follows by downward closure that (\underline{λ}d ∈ v′_{i}. f (φ(d)) (g(d))) ∈ B(T, S)^{v} for any i. Because (\underline{λ}d ∈ v′_{i}. f (φ(d)) (g(d))) = (\underline{λ}d ∈ v′_{i}. f′ (φ(d)) (g(d))), it follows that

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

Thus, h′ ∈ B(T, S)_{S}^{v} as desired.

To see Kripke monotonicity, suppose φ : v ⟶^{𝒞} w and f ∈ (A ⇒ B)(T, S)^{w} with domain w′. Let v′ = φ^{−1}(w′); we know that v′ is a T^{v}-model since T is a 𝒞-termination theory. We want

(\underline{λ}d ∈ v′. f(φ(d))) ∈ (A ⇒ B)(T, S)^{v}.

So suppose ψ : u ⟶^{𝒞} v and g ∈ A(T, S)^{u}. Then

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

by the fact that (ψ; φ) : u ⟶^{𝒞} w. Thus, (\underline{λ}d ∈ v′. f(φ(d))) ∈ (A ⇒ B)(T, S)^{v}.

Finally, to show concreteness, suppose f ∈ |A ⇒ B|; we need to show that (\underline{λ}i ∈ w. f) ∈ (A ⇒ B)(T, S)^{w}. From the definition, we must show that, for

φ : v ⟶^{𝒞} w and h ∈ A(T, S)^{v}, (\underline{λ}j ∈ v. ((\underline{λ}i ∈ w. f) (φ(j))) (h(j))) ∈ B(T, S)_{S}^{v}.

But this reduces to (\underline{λ}j ∈ v. f (h(j))) ∈ B(T, S)_{S}^{v}, which is the uniformity condition on ℛ𝒞𝒫𝒪-morphisms.

Proposition 3.9 (– ⇒ –) is a bifunctor on ℛ𝒞𝒫𝒪 that is contravariant in the first argument and covariant in the second.

Proof: By Proposition 3.8, if A, B are objects, then |A ⇒ B| is too. To check the functor part, suppose f : A′ → A and g : B → B′ in ℛ𝒞𝒫𝒪. The uniformity condition is preserved by composition (see Lemma 3.2), as is relevant domaintheoretic structure, so we may conclude that for any h, (f; h; g) ∈ |A′ ⇒ B′|. To see that (f ⇒ g) as a function satisfies the uniformity condition, consider m ∈ (A ⇒ B)(T, S)^{w}: we need to show that

(\underline{λ}d ∈ w. f; m(d); g) ∈ (A′ ⇒ B′)(T, S)_{S}^{w}.

If we can show that h′ = (\underline{λ}d ∈ w′. \underline{λ}a. g(m d f(a))) ∈ (A′ ⇒ B′)(T, S)^{w}, where w′ is the domain of m, then we will be done—the required path set will be {w′}. So suppose φ : v ⟶^{𝒞} w and h ∈ A′(T, S)^{v} and let

h′′ = (\underline{λ}d ∈ v. h′(φ(d))(h(d)))
= (\underline{λ}d ∈ v. g(m(φ(d))(f(h(d))))).

We then need to show that h′′ ∈ B′(T, S)_{S}^{v}. By the uniformity of f, we get (h; f) ∈ A(T, S)_{S}^{v}. Thus, there exists a path set {v_{1}, …, v_{n}} such that f(h(d))↓ iff d ∈ v_{i} for some i, and f_{i} = (\underline{λ}d ∈ v_{i}. f(h(d))) ∈ A(T, S)^{v} for all i. Thus, for each f_{i},

h_{i} = (\underline{λ}d ∈ v_{i}. m (φ(d)) (f_{i}(d))) ∈ B(T, S)_{S}^{v}

Therefore, for each i, there exists a path set {v_{i,1}, …, v_{i,k_{i}}} such that

• h_{i}(d)↓ iff d ∈ v_{i,j} for some j; and

• h_{i,j} = (\underline{λ}d ∈ v_{i,j}. m (φ(d)) (f_{i}(d))) ∈ B(T, S)^{v} for all j.

Note as well that each v_{i,j} ⊆ v_{i}. By the uniformity of g, (h_{i,j}; g) ∈ B′(T, S)_{S}^{v}. Thus, for each i, j, there exists a path set {v_{i,j,1}, …, v_{i,j,l_{i,j}}} such that

• h_{i,j}(d)↓ iff d ∈ v_{i,j,k} for some k; and

• h_{i,j,k} = (\underline{λ}d ∈ v_{i,j,k}. g(m (φ(d)) (f_{i}(d)))) ∈ B′(T, S)^{v} for all k.

Again, all of the v_{i,j,k} ⊆ v_{i,j}. Thus {v_{1,1,1}, …, v_{n,k_{n},l_{n,kn}} } is a path set and

• h′′(d)↓ iff d ∈ v_{i,j,k} for some i, j and k; and

• (\underline{λ}d ∈ v_{i,j,k}. h′′(d)) = h_{i,j,k} ∈ B′(T, S)^{v} for all i, j and k.

It follows that h′′ ∈ B′(T, S)_{S}^{v} and thus h′ ∈ (A′ ⇒ B′)(T, S)^{w} as desired.

3.7 Partial CCC

ℛ𝒞𝒫𝒪 is a partial cartesian closed category (Curien and Obtułowicz, 1989). Since there are a number of conditions to check, we break the proof up into three parts: ℛ𝒞𝒫𝒪 is a category of partial morphisms, it is partial cartesian, and it is partial cartesian closed.

A category of partial morphisms is a category with a notion of “total” morphisms and a “restriction relation” ⩽ on morphisms. Moreover, the identities must be total, and composition must preserve totality and be monotonic with respect to ⩽. In ℛ𝒞𝒫𝒪, the total morphisms are simply the total functions. If f and f′ are morphisms from A to B, then f ⩽ f′ iff

f(a)↓ implies f(a) = f′(a), for all a ∈ |A|.

It is thus easy to see that

Proposition 3.10 ℛ𝒞𝒫𝒪 is a category of partial morphisms.

A category of partial morphisms is cartesian if it has an object U—called a domain classifier—with a map ◯_{A} : A → U for any object A. There must also be a morphism f ∩ g : A → U for every f, g : A → U, and the following properties must hold:

• If f : A → U, then f ⩽ ◯_{A}.

• The total arrows are exactly those arrows f : A → B such that f; ◯_{B} = ◯_{A}.

• If f, f′, g : A → B are such that f, f′ ⩽ g and f; ◯_{B} ⩽ f′; ◯_{B}, then f ⩽ f′.

• If g : B → U and h, h′ : A → B are such that h ⩽ h′, then (h; g) = (h′; g) ∩ (h; ◯_{B}).

Furthermore, for a category of partial morphisms to be cartesian it must have, for any pair of objects A, B, a partial product given by an object A ⊗ B, projection arrows proj_{1} : A ⊗ B → A and proj_{2} : A ⊗ B → B, and a pairing operation, associating ⟨f, g⟩ : A → B ⊗ C with f : A → B, g : A → C such that the following properties hold:

• proj_{1} and proj_{2} are total.

• Pairing is monotonic with respect to ⩽ in both arguments.

• For any h : A → (B ⊗ C), ⟨h; proj_{1}, h; proj_{2}⟩ = h

• If f : A → B and g : A → C, then (⟨f, g⟩; proj_{1}) ⩽ f and (⟨f, g⟩; proj_{2}) ⩽ g.

• If f : A → B and g : A → C, then for all h : D → A we have (h; ⟨f, g⟩) = ⟨(h; f), (h; g)⟩.

• If f : A → B and g : A → C, then (⟨f, g⟩; ◯_{B⊗C}) = (f; ◯_{B}) ∩ (g; ◯_{C}).

Proposition 3.11 ℛ𝒞𝒫𝒪 is a partial cartesian category.

Proof: The domain classifier is the object unit; for every object A, we pick the morphism ◯_{A} : A → unit to be the unique morphism mapping all elements of A to ⊤. Also, define

(f ∩ f′)(a) = \{ \begin{matrix}⊤ & if f(a)↓ and f′(a)↓ \\ undefined & otherwise. \end{matrix}

The partial product is the tensor product defined previously, and the projection arrows and pairing operation the obvious ones. It is easy to see that these maps exist, and that the above properties hold.

Let (A →_{T} B) denote the set of total morphisms between objects A, B in ℛ𝒞𝒫𝒪. A partial cartesian category is a partial cartesian closed category if there exists a binary operation ⇒ of partial exponentiation on objects such that for any objects A, B, C there exist natural transformations curry(–) from (A ⊗ B) → C onto A →_{T} (B ⇒ C), and uncurry(–) from A →_{T} (B ⇒ C) onto (A ⊗ B) → C, uncurry(curry(f)) = f and curry(uncurry(g)) = g, and for any f′ : D → A,

(f′; curry(f)) ⩽ curry(⟨proj_{1}; f′, proj_{2}⟩; f).

Proposition 3.12 ℛ𝒞𝒫𝒪 is a partial cartesian closed category.

Proof: The partial exponentiation is the function space ⇒ defined previously. For f : (A ⊗ B) → C and g : A →_{T} (B ⇒ C), define

curry(f) = (\underline{λ}a ∈ |A|. \underline{λ}b ∈ |B|. f ⟨a, b⟩)
uncurry(g) = (\underline{λ}⟨a, b⟩ ∈ |A ⊗ B|. g(a)(b)).

We first need to show that the maps are well-defined, and that they satisfy the uniformity conditions. To see that curry(f) is a well-defined total function from |A| to |B ⇒ C|, suppose a ∈ |A| and h ∈ B(T, S)^{w}; we need to show (h; curry(f)(a)) ∈ C(T, S)_{S}^{w}.

By the concreteness condition h′ = (\underline{λ}d ∈ w′. a) ∈ A(T, S)^{w}, where w′ is the domain of h. Then ⟨h′, h⟩ ∈ (A ⊗ B)(T, S)^{w} and by uniformity of f we get (⟨h′, h⟩; f) ∈ C(T, S)_{S}^{w}. Since (⟨h′, h⟩; f) = (h; curry(f)(a)), we are done.

To see the uniformity of curry(f), suppose h_{A} ∈ A(T, S)^{w}; we need to show (h_{A}; curry(f)) ∈ (B ⇒ C)(T, S)_{S}^{w}. Let w′ be the domain of h_{A}. Since (\underline{λ}d ∈ w′. curry(f)(h_{A}(d))) = (h_{A}; curry(f)) and \{w′\} is a path set, it suffices to prove (h_{A}; curry(f)) ∈ (B ⇒ C)(T, S)^{w}. Now, given φ : v → w and h_{B} ∈ B(T, S)^{v} we must prove (\underline{λ}d ∈ v. (h_{A}; curry(f))(φ(d))(h_{B}(d))) ∈ C(T, S)_{S}^{v}. By Kripke Monotonicity of A(T, S)^{w}, h′_{A} = (φ; h_{A}) ∈ A(T, S)^{v}. Let v_{1} be the domain of h′_{A} and v_{2} be the domain of h_{B}, and v′ = (v_{1} ∩ v_{2}). By downward closure,

h′′_{A} = (\underline{λ}d ∈ v′. h′_{A}(d)) ∈ A(T, S)^{v}
h′′_{B} = (\underline{λ}d ∈ v′. h_{B}(d)) ∈ B(T, S)^{v}

Therefore ⟨h′′_{A}, h′′_{B}⟩ ∈ (A ⊗ B)(T, S)^{v}. By the uniformity of f,

(\underline{λ}d ∈ v. (h_{A}; curry(f))(φ(d))(h_{B}(d))) = (\underline{λ}d ∈ v. curry(f)(h′′_{A}(d))(h′′_{B}(d)))
= (\underline{λ}d ∈ v. (⟨h′′_{A}, h′′_{B}⟩; f)(d))
∈ C(T, S)_{S}^{v}

as desired.

Similarly, we need to show that uncurry(g) is a well-defined partial function from |A ⊗ B| to |C| and that it satisfies the uniformity condition. Welldefinedness follows immediately from definition. Now for uniformity, suppose h ∈ (A ⊗ B)(T, S)^{w}; we need to show (h; uncurry(g)) ∈ C(T, S)_{S}^{w}. Notice that h has the form h = ⟨h_{A}, h_{B}⟩, where h_{A} ∈ A(T, S)^{w} and h_{B} ∈ B(T, S)^{w}. By uniformity of g, (h_{A}; g) ∈ (B ⇒ C)(T, S)_{S}^{w}. This means that there exists a path set {w_{1}, …, w_{n}} such that

• (h_{A}; g)(d)↓ iff d ∈ w_{i} for some i; and

• (\underline{λ}d ∈ w_{i}. (h_{A}; g)(d)) ∈ (B ⇒ C)(T, S)^{w} for all i.

Now, since h_{B} ∈ B(T, S)^{w} and id_{w} (the identity) is a morphism in 𝒞, we have

g_{i} = (\underline{λ}d ∈ w. (\underline{λ}e ∈ w_{i}. (h_{A}; g)(e))(d)(h_{B}(d))) ∈ C(T, S)_{S}^{w}.

Thus there exist path sets {w_{i,1}, …, w_{i,k_{i}}} such that

• g_{i}(d)↓ iff d ∈ w_{i,j} for some i, j; and

• (\underline{λ}d ∈ w_{i,j}. g_{i}(d)) ∈ C(T, S)^{w} for all i, j.

¿From the observation that w_{i} ⊇ w_{i,j}, it follows that {w_{1,1}, …, w_{n,k_{n}}} is a path set. Furthermore, for

g′ = (\underline{λ}d ∈ w. g(h_{A}(d))(h_{B}(d))),

we have that

• g′(d)↓ iff d ∈ w_{i,j} for some i, j; and

• (\underline{λ}d ∈ w_{i,j}. g′(d)) ∈ C(T, S)^{w} for all i, j.

Since g′ = (h; uncurry(g)), we are done.

It is not hard to prove that curry(–) and uncurry(–) are natural transformations, and that they form an isomorphism pair. Thus, suppose f′ : D → A; we need to show that

(f′; curry(f)) ⩽ curry(⟨proj_{1}; f′, proj_{2}⟩; f).

Given d ∈ |D|, if f′(d)↑ then (f′; curry(f))(d) is not defined either and there is nothing to show. So suppose f′(d)↓. Then it suffices to show

(f′; curry(f))(d) = curry(⟨proj_{1}; f′, proj_{2}⟩; f)(d).

Now, if f⟨f′(d), b⟩↑, then both the left and right hand side functions above are undefined at b as well. If on the other hand f⟨f′(d), b⟩↓ then both of the above functions will equal that value on b.

3.8 Colimits

Coproducts and the partial cartesian closed structure give most of the structure necessary to interpret FPC types. The only part left is the interpretation of recursive types. To this end, we rework the standard colimit construction from domain theory (Abramsky and Jung, 1994; Gunter, 1992; Plotkin, 1985).

The basis of the colimit construction is embedding-projection pairs. Given objects A, B, then 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}. We abuse notation and write f : A → B when f is an ep-pair from A to B, and id : A → A for the ep-pair ⟨id, id⟩. The composition of ep-pairs is pointwise: if f : A → B and g : B → C, then (f; g) = ⟨f^{e}; g^{e}, g^{p}; f^{p}⟩ : A → C.

Colimits are formed from chains of objects connected by ep-pairs. Formally, an expanding sequence is a tuple

({D_{n} | n ≥ 0}, {f_{n} | f_{n} : D_{n} → D_{n+1} is an ep-pair}).

When n ≤ m, we write f_{mn} : D_{n} → D_{m} for the ep-pair defined by induction as follows:

f_{nn} = id
f_{(m+1)n} = f_{mn}; f_{m}.

Given an expanding sequence, define D by

|D| = {g ∈ [N →_{p} ⋃ D_{i}] | g(i)↓ implies g(i) ∈ D_{i}, and for all n ≤ m, g(n) ≃ f_{mn}^{p}(g(m))}
D(T, S)^{w} = \{h ∈ [w′ →_{t} D] | w′ is a T^{w}-model, and for all φ : v ⟶^{𝒞} w and n ∈ N, (\underline{λ}d ∈ v. h (φ(d)) (n)) ∈ D_{n}(T, S)_{S}^{v}\}

where ordering on |D| is pointwise ordering on the functions. The ep-pairs ⟨μ_{m}^{e} : D_{m} → D, μ_{m}^{p} : D → D_{m}⟩, defined by

μ_{m}^{p}(x) ≃ x(m)
μ_{m}^{e}(x)(l) ≃ ⨆_{k≥m,l}(f_{kl}^{p}(f_{km}^{e}(x)))

make D into a colimit of the expanding sequence, as the next two lemmas show.

Lemma 3.13 D is an object in ℛ𝒞𝒫𝒪.

Proof: It is easy to show that |D| is directed complete. To see that D(T, S)^{w} is a w-termination relation, we check directed completeness and leave the straightforward checks of downward closure, Kripke monotonicity, and concreteness to the reader. Suppose that {h_{i} | i ∈ I} ⊆ D(T, S)^{w} is directed, where each h_{i} has domain w′. Let h be the least upper bound of the h_{i}’s; we need to show that h ∈ D(T, S)^{w}. To show this, consider any φ : v → w and n ∈ N. Then

(\underline{λ}d ∈ v. h (φ(d)) (n)) = ⨆_{i∈I}(\underline{λ}d ∈ v. h_{i} (φ(d)) (n)) ∈ D_{n}(T, S)_{S}^{w}

by the directed completeness of the D_{n}(T, S)_{S}^{w}’s. Thus,

(\underline{λ}d ∈ v. h (φ(d)) (n)) ∈ D_{n}(T, S)_{S}^{w}

as required.

Lemma 3.14 For all m, μ_{m}^{e} : D_{m} → D and μ_{m}^{p} : D → D_{m} are morphisms. Moreover, (μ_{m}^{p}; μ_{m}^{e}) ⊑ id_{D}, (μ_{m}^{e}; μ_{m}^{p}) = id_{D_{m}}, and

⨆_{m≥0} μ_{m}^{p}; μ_{m}^{e} = id_{D}

Proof: The only difficult part of the proof lies in showing that μ_{m}^{e} and μ_{m}^{p} satisfy the uniformity property. To see that μ_{m}^{p} is uniform, suppose h ∈ D(T, S)^{w}. Then (h; μ_{m}^{p}) = (\underline{λ}d ∈ w. h (d) (m)) ∈ D_{m}(T, S)_{S}^{w}, which is what we needed to show.

The proof of the uniformity of μ_{m}^{e} is more involved. Suppose h ∈ D_{m}(T, S)^{w}, and consider g = (h; μ_{m}^{e}). We show that g ∈ D(T, S)^{w}, which will show that g ∈ D(T, S)_{S}^{w}. Note that g has the same domain as h, so consider any given φ : v ⟶^{𝒞} w and n ∈ N. Note that

(\underline{λ}d ∈ v. g (φ(d)) (n)) = (\underline{λ}d ∈ v. μ_{m}^{e} (h (φ(d))) n) = ⨆_{k≥m,n}(φ; h; f_{km}^{e}; f_{kn}^{p})

By the uniformity of f_{kn}^{p} and f_{km}^{e}, we know that (φ; h; f_{kn}^{e}; f_{km}^{p}) ∈ D_{n}(T, S)_{S}^{v}. Thus, by the directed completeness of D_{n}(T, S)_{S}^{w},

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

as required.

4 Interpretation of FPC

The constructions in the category ℛ𝒞𝒫𝒪 in Section 3 can now be used to build a model of FPC (Gunter, 1992; Riecke and Subrahmanyam, 1997). A model has both a meaning for types and for terms. Types denote objects in the category, and terms denote morphisms.

The meaning of a closed type is clear except for the meanings of recursive types, which necessitates describing the meaning of an open type expression. For this reason, the meaning of a type is a functor from its free type variables to the category ℛ𝒞𝒫𝒪. In making this precise, most of the difficulty lies in finding the right category of free type variables. To this end, define a pre-ep-pair to be a pair f = ⟨f^{e}, f^{p}⟩ of morphisms f^{e} : D → E and f^{p} : E → D in ℛ𝒞𝒫𝒪; we write f : D ↪ E as shorthand for saying that f is such a pre-ep-pair. Note that a pre-ep-pair is just like an ep-pair, but without the requirements that (f^{e}; f^{p}) = id and (f^{p}; f^{e}) ⊑ id. The use of pre-ep-pairs instead of ep-pairs makes certain theorems (particularly those in Appendix B) easier to prove.

A type environment η is a function from type variables to objects of ℛ𝒞𝒫𝒪, and a type environment map π : η → η′ is a function from type variables to pre-ep-pairs such that π(α) : η(α) ↪ η′(α) for all α. The category ℰ has type environments as objects, and type environment maps as morphisms. It is simple to check that ℰ is a category.

The meaning of a type s, then, is a functor [[s]] : ℰ → ℛ𝒞𝒫𝒪. The definition on objects of ℰ—except in the case of recursive types—is

[[α]]η = η(α)
[[unit]]η = unit
[[s ⊕ t]]η = ([[s]]η ⊕ [[t]]η)
[[s ⊗ t]]η = ([[s]]η ⊗ [[t]]η)
[[s ⇒ t]]η = ([[s]]η ⇒ [[t]]η)

The operation on morphisms of [[s]]π—except for recursive types—is

[[α]]π = π(α)
[[unit]]π = ⟨id_{unit}, id_{unit}⟩
[[s ⊕ t]]π = ([[s]]π ⊕ [[t]]π)
[[s ⊗ t]]π = ([[s]]π ⊗ [[t]]π)
[[s ⇒ t]]π = ([[s]]π ⇒ [[t]]π)

where, abusing notation, ⊕, ⊗, and ⇒ work on pre-ep-pairs as follows:

([[s]]π ⊕ [[t]]π) = ⟨([[s]]π)^{e} ⊕ ([[t]]π)^{e}, ([[s]]π)^{p} ⊕ ([[t]]π)^{p}⟩
([[s]]π ⊗ [[t]]π) = ⟨([[s]]π)^{e} ⊗ ([[t]]π)^{e}, ([[s]]π)^{p} ⊗ ([[t]]π)^{p}⟩
([[s]]π ⇒ [[t]]π) = ⟨([[s]]π)^{p} ⇒ ([[t]]π)^{e}, ([[s]]π)^{e} ⇒ ([[t]]π)^{p}⟩

(Recall the actions of ⊕, ⊗, and ⇒ on morphisms from Section 3.)

The case of recursive types requires more work. Suppose s = (rec α. t). Let ⟨T_{s,η}^{i}, f_{s,η}^{i} | i ≥ 0⟩ be the expanding sequence given by

\begin{aligned}T_{s,η}^{0} & = & void & f_{s,η}^{0} & = & !_{T_{s,η}^{1}} \\ T_{s,η}^{n+1} & = & [[t]](η[α ↦ T_{s,η}^{n}]) & f_{s,η}^{n+1} & = & [[t]](id[α ↦ f_{s,η}^{n}]) \end{aligned}

\xymatrix{T_{s,η_{1}}^{0} \ar[d]_{p_{s,π}^{0}} \ar[r]^{f_{s,η_{1}}^{0}} & T_{s,η_{1}}^{1} \ar[d]_{p_{s,π}^{1}} \ar[r]^{f_{s,η_{1}}^{1}} & T_{s,η_{1}}^{2} \ar[d]_{p_{s,π}^{2}} \ar[r]^{f_{s,η_{1}}^{2}} & ⋯ & [[s]]η_{1} \ar[d]^{[[s]]π} \\ T_{s,η_{2}}^{0} \ar[r]^{f_{s,η_{2}}^{0}} & T_{s,η_{2}}^{1} \ar[r]^{f_{s,η_{2}}^{1}} & T_{s,η_{2}}^{2} \ar[r]^{f_{s,η_{2}}^{2}} & ⋯ & [[s]]η_{2}}

Figure 1: Colimits and definition of [[s]](π), where s = (rec α. t).

where !_{D} is the unique ep-pair (not just pre-ep-pair) from void to D. This is an expanding sequence because the maps f_{s,η}^{n}’s are ep-pairs (by a simple induction on the definition). If D is the colimit of the expanding sequence, then define [[s]]η = D. Moreover, define the morphisms intro_{s,η} : [[t[s/α]]]η → [[s]]η and elim_{s,η} : [[t[s/α]]]η → [[s]]η and

intro_{s,η} = ⨆_{n≥0} [[t]]id[α ↦ μ_{s,η}^{n}]^{p}; μ_{s,η}^{n+1,e}
elim_{s,η} = ⨆_{n≥0} μ_{s,η}^{n+1,p}; [[t]]id[α ↦ μ_{s,η}^{n}]^{e}

These maps will be used to give meaning to intro and elim.

For the morphism part of the functor in the case of recursive types, consider the diagram in Figure 1. Given π : η_{1} → η_{2}, consider the expanding sequences ⟨T_{s,η_{1}}^{i}, f_{s,η_{1}}^{i} | i ≥ 0⟩, and ⟨T_{s,η_{2}}^{i}, f_{s,η_{2}}^{i} | i ≥ 0⟩, with colimiting cocones ⟨[[s]]η_{1}, μ_{s,η_{1}}^{i} | i ≥ 0⟩ and ⟨[[s]]η_{2}, μ_{s,η_{2}}^{i} | i ≥ 0⟩, respectively. Define the family of pre-ep-pairs p_{s,π}^{n}, where p_{s,π}^{n} is a pre-ep-pair from T_{s,η_{1}}^{n} to T_{s,η_{2}}^{n} by

p_{s,π}^{0} = !_{void}
p_{s,π}^{k+1} = [[t]](π[α ↦ p_{s,π}^{k}])

A simple induction argument shows that the diagram in Figure 1 commutes (assuming that [[·]] is a functor, which holds by construction). From this fact, it is clear that

⟨[[s]]η_{2}, μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n} | n ≥ 0⟩

is a cocone for the expanding sequence ⟨T_{s,η_{1}}^{i}, f_{s,η_{1}}^{i} | i ≥ 0⟩. Define [[s]]π to be the unique mediating map from [[s]]η_{1} to [[s]]η_{2}, which must exist by the colimiting properties.

The meaning of terms can now be given using the combinators of the category. If Γ = x_{1} : t_{1}, ..., x_{n} : t_{n}, define [[Γ]] = [[t_{1}]] ⊗ … ⊗ [[t_{n}]]. (If Γ is empty, [[Γ]] is the object unit). Elements of |[[Γ]]| are called environments. For an environment ρ ∈ |[[Γ]]|, we write ρ(x) for projection to the component corresponding to variable x. The meaning of a judgement Γ ⊢ M : t is an ℛ𝒞𝒫𝒪-morphism [[Γ ⊢ M : t]] : [[Γ]] → [[t]]. The definition is by induction on the structure of terms:

[[Γ, x : t ⊢ x : t]]ρ = ρ(x) [[Γ ⊢ ⟨⟩ : unit]]ρ = ⊤

[[Γ ⊢ (λx : s. M) : (s ⇒ t)]]ρ = f, where f(d) ≃ [[Γ, x : s ⊢ M : t]]ρ[x ↦ d]

[[Γ ⊢ (M N) : t]]ρ ≃ ([[Γ ⊢ M : (s ⇒ t)]]ρ) ([[Γ ⊢ N : s]]ρ)

[[Γ ⊢ (intro_{rec α. s} M) : (rec α. s)]]ρ ≃ intro([[Γ ⊢ M : s[rec α. s/α]]]ρ)

[[Γ ⊢ (elim_{rec α. s} M) : s[rec α. s/α]]]ρ ≃ elim([[Γ ⊢ M : (rec α. s)]]ρ)

[[Γ ⊢ ⟨M, N⟩ : (t_{1} ⊗ t_{2})]]ρ ≃ ⟨[[Γ ⊢ M : t_{1}]]ρ, [[Γ ⊢ N : t_{2}]]ρ⟩
[[Γ ⊢ (proj_{i} M) : t_{i}]]ρ ≃ proj_{i}([[Γ ⊢ M : (t_{1} ⊗ t_{2})]]ρ)
[[Γ ⊢ (inj_{i} M) : (t_{1} ⊕ t_{2})]]ρ ≃ inj_{i}([[Γ ⊢ M : t_{i}]]ρ)

[[Γ ⊢ (case M ofinj_{1}(x).N_{1} orinj_{2}(x).N_{2}) : t]]ρ ≃

\{ \begin{matrix}[[Γ, x : s_{i} ⊢ N_{i} : t]]ρ[x ↦ d] & if [[Γ ⊢ M : (s_{1} ⊕ s_{2})]]ρ = inj_{i}(d) \\ undefined & otherwise \end{matrix}

Here, the notation ρ[x ↦ d] denotes the environment in which the x component is extended (or overwritten) to d. For notational convenience, if ∅ ⊢ M : s, we write [[M]] for the corresponding element [[∅ ⊢ M : s]]⊤ ∈ [[s]].

The model is adequate:

Theorem 4.1 (Adequacy) Suppose M is a closed FPC term of type s. Then M ⇓ V iff [[M]]↓.

The proof appears in the Appendix.

Corollary 4.2 For closed terms M and N of type s,

if [[M]] \begin{matrix}⊏ \\ ∼ \end{matrix} [[N]], then M ⊑_{F P C} N.

Proof: Suppose [[M]] \begin{matrix}⊏ \\ ∼ \end{matrix} [[N]]. To show M ⊑_{F P C} N, suppose C[·] is a context such that C[M] ⇓. By the Adequacy Theorem 4.1, [[C[M]]]↓. By the hypothesis, it follows that [[C[N]]]↓ and thus C[N] ⇓.

5 Examples

Even though the semantic category ℛ𝒞𝒫𝒪 is arguably complicated, it does support simple reasoning about definability of FPC terms. This section gives two examples of non-definability proofs, with non-sequential functions drawn from the literature.

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

The function 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 that por is not definable (also due to Plotkin, see (Astesiano and Costa, 1980)). In this case, we need to exhibit an index category 𝒞, a choice of 𝒞-termination theory T, and a 𝒞, T -path theory S. Pick 𝒞 to be the category with just one index set w = {1, 2, 3} and the identity map, T^{w} to be the theory with just one implication (1, 2 ⊢ 3), and S^{w} to be the set { { }, {w′} | w′ is a T^{w}-model }. Let h : unit → unit be the identity function, 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, we must show that h_{1} = (h, h′, h′) and h_{2} = (h′, h, h′) are both in (unit ⇒ unit)(T, S)^{w}; this will show that (g_{1}, g_{2}, g_{3}) = ⟨h_{1}, h_{2}⟩ is in ((unit ⇒ unit) ⊗ (unit ⇒ unit))(T, S)^{w}.

We show the claim for the case of h_{1} and leave the analogous case of h_{2} to the reader. Pick any u ∈ unit(T, S)^{w}, and let u′ = (\underline{λ}d ∈ w. h_{1}(d)(u(d))). We must show u′ ∈ unit(T, S)_{S}^{w}. By choice of T^{w}, the domain of u is either ∅, {1}, {2}, {3}, {1, 3}, {2, 3}, or {1, 2, 3}. We verify the fact for the cases {} and {1, 2, 3}. The remaining cases are very similar and omitted here. First, consider the case of ∅. By definition, the domain of u′ is ∅ as well and the existence of the path set {} justifies u′ ∈ unit(T, S)_{S}^{w}. For the case of dom(u) = {1, 2, 3} we get dom(u′) = {1} since h_{1} = (h, h′, h′). Thus, via the path set {{1}}, we conclude that u′ ∈ unit(T, S)_{S}^{w}.

However, since f(g_{1}) = ⊤, f(g_{2}) = ⊤, and f(g_{3}) is undefined,

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

5.2 Sieber’s example is not definable

The second example is also due to Sieber (1992), a modified example due to Curien (1986). 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 satisfying

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. Pick 𝒞 to be the trivial index category 𝒞 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

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

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

It is not hard to prove that this is a 𝒞, T -path 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 conditions on the path sets. Thus, there is no such definable f.

6 Full Abstraction

We prove full abstraction for FPC in two steps. Let Finite FPC be the sublanguage of FPC with no recursive types. First, we reduce the full abstraction problem to the problem of showing that all elements in Finite FPC types are definable. The reduction uses techniques from (Riecke and Subrahmanyam, 1997), and we give the basic outline of the proof. Second, we prove that all elements in Finite FPC types are definable by terms. The proof follows the structure of the proof of full abstraction for PCF (O’Hearn and Riecke, 1995).

6.1 Reduction to definability for Finite FPC

Define the unwinding of all type recursions to depth n by

α^{n} = α  (s ⊕ t)^{n} = (s^{n} ⊕ t^{n})
void^{n} = void  (s ⊗ t)^{n} = (s^{n} ⊗ t^{n})
unit^{n} = unit  (s → t)^{n} = (s^{n} → t^{n})

(rec α. t)^{n} = \underbrace{t^{n}[t^{n}[… [t^{n}}_{n}[void/α]/α] …]/α]/α

In Appendix B, we construct terms clm_{s,n}^{p} : s → s^{n} and clm_{s,n}^{e} : s^{n} → s that, intuitively, denote a sequence of “colimiting” maps. The terms satisfy the following property:

Lemma 6.1 ⨆_{n≥0}([[clm_{s,n}^{p}]]; [[clm_{s,n}^{e}]]) = id_{[[s]]}.

The construction uses the techniques in (Riecke and Subrahmanyam, 1997), although we repeat the salient details in the Appendix for completeness. These terms allow us to reduce the problem to definability for Finite FPC.

Theorem 6.2 Suppose for all Finite FPC types s, all elements of [[s]] are definable by closed terms. Let M, N be closed FPC terms of type s. If [[M]] ⊏̸ ∼ [[N]], then M ⋢_{F P C} N.

Proof: We claim that it is enough to prove the theorem for all Finite FPC types s. To see this, suppose s is a general FPC type. We know by Lemma 6.1 that [[clm_{s,n}^{p} M]] ⊏̸ ∼ [[clm_{s,n}^{p} N]] for some n. Both of the terms M′ = (clm_{s,n}^{p} M) and N′ = (clm_{s,n}^{p} N) have a Finite FPC type s. Thus, if we can find a context C[·] distinguishing M′ from N′, then the context C[clm_{s,n}^{p} [·]] distinguishes M and N.

We now prove the theorem for all Finite FPC types s by induction on s, giving two of the five cases and leaving the others to the reader. In the first case, suppose s = (t ⊕ t′). There are three subcases:

• [[M]]↓ and [[N]]↑. Then, by Adequacy, the context [·] distinguishes M and N.

• [[M]] = inj_{i}(d) and [[N]] = inj_{j}(e), where i ≠ j. By Adequacy, we get that M ⇓ (inj_{i} V) and N ⇓ (inj_{j} V′). Suppose i = 1 (the other case is analogous); then the context (case [·] ofinj_{1}(x).x orinj_{2}(x).Ω) distinguishes M and N.

• [[M]] = inj_{i}(d) and [[N]] = inj_{i}(e). By Adequacy, M ⇓ (inj_{i} V) and N ⇓ (inj_{i} V′). Note that V ⋢_{F P C} V′. Suppose i = 1 (the other case is analogous), and the context distinguishing V, V′ is C[·]. Then the context (case [·] ofinj_{1}(x).C[x] orinj_{2}(x).Ω) distinguishes M and N.

In the second case, suppose s = (t → t′). If [[M]] ↓ and [[N]] ↑, then the context [·] distinguishes M and N. If both are defined, on the other hand, by Adequacy, M ⇓ (λx : t. M′) and N ⇓ (λx : t. N′). Since [[M]] ⋢ [[N]], there must be an argument d ∈ [[t]] such that [[M]](d) ⊏̸ ∼ [[N]](d). By hypothesis, there is a closed Finite FPC term P such that d = [[P]]. Thus, [[M P]] ⊏̸ ∼ [[N P]]. By induction, there is a context C[·] distinguishing (M P) and (N P). Thus, the context C[[·] P] distinguishes M and N.

6.2 Definability of elements of Finite FPC types

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

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

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

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

The path sets in S^{w} are defined as follows. {w_{1}, …, w_{k}} is a path set if:

• w_{1}, …, w_{k} ∈ X^{w}; and

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

In the following, we use if-then-else and other notation in terms when working with the types n̄; these are just shorthand for Finite FPC terms.

Using the alternative characterization of T -models given by Proposition 3.1, it is not hard to establish the following

Lemma 6.3 The set X = { X^{w} | w ∈ Obj(𝒞) } defines a 𝒞-termination theory T by taking X^{w} to be a set of models.

Proof: Let φ : v ⟶^{𝒞} w and

\begin{aligned}w & = & [s_{1}, …, s_{n}] & s & = & (s_{1} ⊗ … ⊗ s_{n}) \\ v & = & [s_{1}, …, s_{n}, …, s_{n+k}] & s′ & = & (s_{1} ⊗ … ⊗ s_{n} ⊗ … ⊗ s_{n+k}) \end{aligned}

First, we establish that each X^{w} ∈ X is a closure system; by Proposition 3.1, it will then be clear that each T^{w} is a w-theory. Note that w ∈ X^{w} (the requisite term is (λx : s. ⟨⟩) of type (s ⇒ unit)). So suppose w_{1}, w_{2} ∈ X^{w}. Then there exist M_{1}, M_{2} with [[M_{i}]](d)↓ iff d ∈ w_{i}. Consider the term

M = (λx : s. (M_{1} x); (M_{2} x)).

Then it is clear that [[M]](d)↓ iff d ∈ w_{1} ∩ w_{2}. Thus, (w_{1} ∩ w_{2}) ∈ X^{w}.

Second, suppose w′ is a T^{w}-model. Then by definition, there is a term N : (s ⇒ unit) such that [[N]](d)↓ iff d ∈ w′. Let v′ = φ^{−1}(w′), and

M = (λx : s′. N ⟨x_{1}, …, x_{n}⟩)

where x_{i} is shorthand for the i^{th} projection of the term x. Then [[M]](d) ↓ iff d ∈ v′, so v′ is a T^{v}-model as required. We conclude that T is indeed a 𝒞-termination theory.

Lemma 6.4 S is a 𝒞, T -path theory.

Proof: We need to show S^{w} satisfies four properties. Suppose w′ is a T^{w}-model and X = {w_{1}, …, w_{k}} and X′ = {w′_{1}, …, w′_{l}} are path sets in S^{w}. Then there exists a term M defining w′, and terms N and P defining these path sets.

• The term (λx : s. Ω) defines the path set {}.

• The term (λx : s. (M x); 1) defines the path set {w′}.

• If X ⊓ X′ = {w_{i_{1}} ∩ w_{j_{1}}, …, w_{i_{n}} ∩ w_{j_{n}}}, then the term

(λx : s. if ((N x) = i_{1}) ∧ ((P x) = j_{1}) then 1 else … if ((N x) = i_{n}) ∧ ((P x) = j_{n}) then (i_{n} ∗ j_{n}) else Ω)

defines the path set X ⊓ X′.

• Suppose there is a j such that for all i, w′_{i} ⊆ w_{j}. Then the term

(λx : s. if (N x) < j then (N x) else if (N x) > j then(N x) + l − 1 else (P x) + j − 1)

defines the path set {w_{1}, …, w_{j−1}, w′_{1}, …, w′_{l}, w_{j+1}, …, w_{k}}.

This completes the proof.

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

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

Proof: By induction on t.

• t = void. If g ∈ [[t]](T, S)_{S}^{w}, then the term M = (λx : s. Ω) defines g. The converse is also trivial.

• t = unit. For (⇐), suppose M : (s ⇒ unit). By definition, M defines a T^{w}-model w′ via

[[M]](d)↓ iff d ∈ w′.

Thus, [[M]] ∈ [[unit]](T, S)_{S}^{w}. For (⇒), suppose g ∈ [[unit]](T, S)_{S}^{w}. Thus, there exists a path set {w_{1}, …, w_{k}} such that

– g(d)↓ iff d ∈ w_{i} for some i; and

– (\underline{λ}d ∈ w_{i}. g(d)) ∈ [[unit]](T, S)^{w}.

(Of course, in this particular case of unit, the second clause is redundant.) By the definition of path sets, there is a P : (s ⇒ k̄) such that [[P]](d) = i iff d ∈ w_{i}, and undefined otherwise. Let

M = (λx : s. (P x); ⟨⟩).

It is not hard to see that [[M]] = g as needed.

• t = (t_{1} ⊕t_{2}). For (⇐), suppose M : (s ⇒ (t_{1} ⊕t_{2})). Consider the following two terms:

N_{1} = (λx : s. case (M x) ofinj_{1}(y).y orinj_{2}(y).Ω) : (s ⇒ t_{1})
N_{2} = (λx : s. case (M x) ofinj_{1}(y).Ω orinj_{2}(y).y) : (s ⇒ t_{2})

By induction (⇐), [[N_{i}]] ∈ [[t_{i}]](T, S)_{S}^{w}. Thus, we have for some path sets X = {w_{1}, …, w_{k}} and X′ = {w′_{1}, …, w′_{l}},

– [[N_{1}]](d)↓ iff d ∈ w_{i} for some i;

– (\underline{λ}d ∈ w_{i}. [[N_{1}]](d)) ∈ [[t_{1}]](T, S)^{w} for all i;

– [[N_{2}]](d)↓ iff d ∈ w′_{i} for some i; and

– (\underline{λ}d ∈ w′_{i}. [[N_{2}]](d)) ∈ [[t_{2}]](T, S)^{w} for all i.

Note that for any i, j, w_{i} and w′_{j} are disjoint: if d ∈ w_{i}, then [[N_{1}]](d) ↓, so [[M]](d) = inj_{1}(a), so [[N_{2}]](d) ↑, so d ∉ w′_{j}. Note also that the set {w_{1}, …, w_{k}, w′_{1}, …, w′_{l}} is a legal path set via the term

(λx : s. case (M x) ofinj_{1}(y).(P_{1} x) orinj_{2}(y).(P_{2} x) + k)

if P_{1} is the term for X and P_{2} is the term for X′. Finally, note that

– [[M]](d)↓ iff d ∈ w_{i} or w′_{i} for some i; and – For the first set of T^{w}-models,

(\underline{λ}d ∈ w_{i}. [[M]](d)) = ((\underline{λ}d ∈ w_{i}. [[N_{1}]](d)); inj_{1}) ∈ [[t_{1} ⊕ t_{2}]](T, S)^{w}

and for the second set,

(\underline{λ}d ∈ w′_{i}. [[M]](d)) = ((\underline{λ}d ∈ w′_{i}. [[N_{2}]](d)); inj_{2}) ∈ [[t_{1} ⊕ t_{2}]](T, S)^{w}.

Therefore, [[M]] ∈ [[t]](T, S)_{S}^{w}. For (⇒), suppose g ∈ [[t_{1} ⊕ t_{2}]](T, S)_{S}^{w}. By definition, there exists a path set {w_{1}, …, w_{k}} such that

– g(d)↓ iff d ∈ w_{i} for some i; and

– g_{i} = (\underline{λ}d ∈ w_{i}. g(d)) ∈ [[t_{1} ⊕ t_{2}]](T, S)^{w} for all i.

Then by definition, g_{i} = (h_{i}; inj_{j_{i}}) for some h_{i} ∈ [[t_{j_{i}}]](T, S)^{w}. Since {w_{i}} itself is a path set we get that h_{i} ∈ [[t_{j_{i}}]](T, S)_{S}^{w}, and thus by induction (⇒), there exists an N_{i} : (s ⇒ t_{j_{i}}) such that

d ∈ w_{i} iff [[N_{i}]](d)↓, and h_{i} = (\underline{λ}d ∈ w_{i}. [[N_{i}]](d)).

Since {w_{1}, …, w_{k}} is a path set, there is a term P : s ⇒ k̄ defining that path set. Let M_{i} = (λx : s. inj_{j_{i}} (N_{i} x)) and

M = (λx : s. if (P x) = 1 then (M_{1} x) else … if (P x) = k then (M_{k} x) else Ω).

Then [[M]] = g.

• t = (t_{1} ⊗t_{2}). For (⇐), suppose M : (s ⇒ (t_{1} ⊗t_{2})). Consider the following two terms:

N_{i} = (λx : s. proj_{i} (M x)) : (s ⇒ t_{i}).

By induction (⇐), [[N_{i}]] ∈ [[t_{i}]](T, S)_{S}^{w}. That is, there exists some path sets X = {w_{1}, …, w_{k}} and X′ = {w′_{1}, …, w′_{l}}, such that

– [[N_{1}]](d)↓ iff d ∈ w_{i} for some i;

– (\underline{λ}d ∈ w_{i}. [[N_{1}]](d)) ∈ [[t_{1}]](T, S)^{w} for all i;

– [[N_{2}]](d)↓ iff d ∈ w′_{i} for some i; and

– (\underline{λ}d ∈ w′_{i}. [[N_{2}]](d)) ∈ [[t_{2}]](T, S)^{w} for all i.

Note that X ⊓ X′ = {w′′_{1}, …, w′′_{m}} is a path set, and note that

[[M]](d)↓ iff d ∈ w′′_{i} for some i; and

\begin{aligned}(\underline{λ}d ∈ w′′_{i}. [[M]](d)) & = ⟨(\underline{λ}d ∈ w′′_{i}. [[N_{1}]](d)), (\underline{λ}d ∈ w′′_{i}. [[N_{2}]](d))⟩ \\ & ∈ [[t_{1} ⊗ t_{2}]](T, S)^{w}. \end{aligned}

Therefore, [[M]] ∈ [[t]](T, S)_{S}^{w}. For the converse, suppose g ∈ [[t_{1} ⊗ t_{2}]](T, S)_{S}^{w}. Then there exists a path set {w_{1}, …, w_{k}} such that – g(d)↓ iff d ∈ w_{i} for some i; and

– g_{i} = (\underline{λ}d ∈ w_{i}. g(d)) ∈ [[t_{1} ⊗ t_{2}]](T, S)^{w}.

By definition, g_{i} = ⟨h_{i,1}, h_{i,2}⟩ for some h_{i,j} ∈ [[t_{j}]](T, S)^{w}. By induction (⇒), there exist N_{i,j} : (s ⇒ t_{j}) such that

d ∈ w_{i} iff [[N_{i,j}]](d)↓, and h_{i,j} = (\underline{λ}d ∈ w_{i}. [[N_{i,j}]](d)).

Since we have a path set, there is a term P : s ⇒ k̄ defining that path set. Let M_{i} = (λx : s. ⟨N_{i,1} x, N_{i,2} x⟩) and

M = (λx : s. if (P x) = 1 then (M_{1} x) else … if (P x) = k then (M_{k} x) else Ω).

Then [[M]] = g.

• t = (t_{1} ⇒ t_{2}). For (⇐), suppose M : (s ⇒ (t_{1} ⇒ t_{2})). There are two cases: either [[M]] is undefined on every argument, or [[M]] is defined on at least one argument. In the first case, since {} is a path set in S^{w}, it is not hard to see that [[M]] ∈ [[t_{1} ⇒ t_{2}]](T, S)_{S}^{w}. In the second case, let

M′ = (λx : s. (M x); 1).

By the definition of S^{w}, M′ defines a path set consisting of one element; call it {w′}. We use this as our path set.

1. Obviously, [[M]](d)↓ iff d ∈ w′.

2. To see (\underline{λ}d ∈ w′. [[M]](d)) ∈ [[t_{1} ⇒ t_{2}]](T, S)^{w}, suppose φ : v ⟶^{𝒞} w and g ∈ [[t_{1}]](T, S)^{v}, where v = [s_{1}, …, s_{n+k}]. Furthermore, we let s′ = (s_{1} ⊗ … ⊗ s_{n+k}). Then, by induction (⇒), there is a closed N : (s′ ⇒ t_{1}) such that

d ∈ v′ iff [[N]](d)↓, and g = (\underline{λ}d ∈ v′. [[N]](d))

where v′ is the domain of g. Consider the term

P = (λx : s′. (M ⟨x_{1}, …, x_{n}⟩) (N x)) : (s′ ⇒ t_{2})

By induction (⇐), [[P]] ∈ [[t_{2}]](T, S)_{S}^{v}. But note that

[[P]](d) ≃ (\underline{λ}d ∈ w′. [[M]](d)) (φ(d)) (g(d)).

Thus,

(\underline{λ}d ∈ v. (\underline{λ}d ∈ w′. [[M]](d)) (φ(d)) (g(d))) ∈ [[t_{2}]](T, S)_{S}^{v}

as required.

For the converse, suppose g ∈ [[t_{1} ⇒ t_{2}]](T, S)_{S}^{w}. Then there exists a path set {w_{1}, …, w_{k}} such that – g(d)↓ iff d ∈ w_{i} for some i; and

– g_{i} = (\underline{λ}d ∈ w_{i}. g(d)) ∈ [[t_{1} ⇒ t_{2}]](T, S)^{w}.

Let v = [s_{1}, …, s_{n}, t_{1}], φ : v → w, and s′ = (s_{1} ⊗ … ⊗ s_{n} ⊗ t_{1}), and N = (λx : s′. x_{n+1}). By induction (⇐), [[N]] ∈ [[t_{1}]](T, S)_{S}^{v}. But note that the T^{v}-model that makes [[N]] converge is all of v. Thus, there is a path set {v_{1}, …, v_{l}} ∈ S^{v} with (v_{1} ∪ … ∪ v_{l}) = v and

h_{j} = (\underline{λ}d ∈ v_{j}. [[N]](d)) ∈ [[t_{1}]](T, S)^{v}

for all j ∈ {1, …, l}. Therefore,

h_{i,j} = (\underline{λ}d ∈ v. g_{i} (φ(d)) (h_{j}(d))) ∈ [[t_{2}]](T, S)_{S}^{v}.

By induction (⇒), there exist terms P_{i,j} : (s′ ⇒ t_{2}) such that h_{i,j} = [[P_{i,j}]]. But note that

[[P_{i,j}]]⟨d_{1}, …, d_{n}, d⟩ ≃ (g_{i} ⟨d_{1}, …, d_{n}⟩ d).

Let Q be the term that defines the path set {w_{1}, …, w_{k}} and Q_{j} be the term that defines each v_{j}. Define

Q′_{i} = (λx : s. λy : t_{1}. if Q_{1} ⟨x, y⟩ then P_{i,1} ⟨x, y⟩ else … if Q_{l} ⟨x, y⟩ then P_{i,l} ⟨x, y⟩ else Ω)

and let

M = (λx : s. if (Q x) = 1 then (Q′_{1} x) else … if (Q x) = k then (Q′_{k} x) else Ω)

Then it is not hard to see that [[M]] = g.

This completes the induction and hence the proof.

Corollary 6.6 All elements of closed Finite FPC types are definable.

Proof: Suppose s is a closed Finite FPC type, and g ∈ [[s]]. By concreteness,

h = (\underline{λ}d ∈ [ ]. g) ∈ [[s]](T, S)_{S}^{[ ]}.

By Lemma 6.5, h = [[N]] for some closed term N of type (unit → s). Then g = [[N ⟨⟩]].

6.3 Putting it together

We may now prove the main theorem of the paper.

Theorem 6.7 (Full Abstraction) Suppose M, N are closed terms of type s.

Then [[M]] \begin{matrix}⊏ \\ ∼ \end{matrix} [[N]] iff M ⊑_{F P C} N.

Proof: (⇐) is immediate from Theorem 6.2 and Corollary 6.6, and (⇒) is immediate from Corollary 4.2.

7 Discussion

We have shown in this paper how to construct a fully abstract model for call-by-value FPC using logical relations, generalizing the approach taken for PCF (O’Hearn and Riecke, 1995; Sieber, 1992). The model supports a simple form of reasoning for showing that certain values are not definable.

There are other ways to build fully abstract models for FPC. For instance, Riecke and Viswanathan give a dcpo-based model for call-by-value FPC (Riecke and Viswanathan, 1993; Riecke and Viswanathan, 1995), using the syntactic methods of Milner (1977). 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 for FPC by McCusker, who builds a model of call-by-name FPC (McCusker, 1996; McCusker, 1997). 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). Game semantics has been recently adapted to the callby-value setting (Abramsky and McCusker, 1997; Honda and Yoshida, 1997). These papers devise models by loosening the restrictions of the original games semantics (Abramsky et al., 1994; Hyland and Ong, 1995; Nickau, 1994) 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.

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 (Sieber, 1992). 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 by Jung and Stoughton (1993); see (Jung et al., 1996; O’Hearn and Riecke, 1995) for a further discussion. Loader shows that the decision problem for PCF over the single boolean base type is undecidable (Loader, 1997). We expect that the proof will carry over to Finite FPC.

The model presented here has some ad hoc features that should be examined more closely. The construction of path sets, for instance, might be better expressed in terms of Grothendieck topologies; recent work by Fiore and Simpson (1999) may be useful. Other recent work by Marz has defined a more general category of “sequential domains” that is suitable for call-by-name (Marz, 1998). Call-by-value can be simulated in Marz’s framework through a lifting operation. Marz’s conditions on path sets are perhaps easier to understand than our definitions, and also do not rely on the intermediate step of termination theories.

Such a simplification here would make the model easier to construct. It would be useful, among all of these definitions, to settle on a single, well-motivated definition.

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 (O’Hearn and Reynolds, 1997; O’Hearn and Tennent, 1995) 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 “path theories” 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. The extension of FPC with a notion of local state, as in Idealized Algol (Reynolds, 1981) or Standard ML (Milner et al., 1997), 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 Glynn Winskel, the organizer of the 1995 Full Abstraction Workshop, and 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 thank Samson Abramsky, Thomas Hildebrandt, Kohei Honda, Leonid Libkin, Rona Machlin, Peter O’Hearn, Riccardo Pucella, Thomas Streicher, and the anonymous referees of LICS 1997 for comments and encouragement. We also thank the tireless efforts of the referees in improving the exposition and in correcting the definitions with colimits.

References

Abadi, M. and Fiore, M. P. (1996). Syntactic considerations on recursive types. In Proceedings, Eleventh Annual IEEE Symposium on Logic in Computer Science, pages 242–252.

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

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

Abramsky, S. and McCusker, G. (1997). Call-by-value games. In Computer Science Logic. Submitted for publication.

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

Curien, P.-L. (1986). Categorical Combinators, Sequential Algorithms and Functional Programming. John Wiley & Sons.

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

Fiore, M. and Simpson, A. (1999). Lambda definability with sums via Grothendieck logical relations. In Typed Lambda Calculi and Applications, Lect. Notes in Computer Sci.. Springer-Verlag. To appear.

Girard, J.-Y. (1971). 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 Fenstad, J. E., editor, Proceedings of the Second Scandinavian Logic Symposium, volume 63 of Studies in Logic and the Foundations of Mathematics, pages 63–92. North-Holland.

Gunter, C. A. (1992). Semantics of Programming Languages: Structures and Techniques. MIT Press.

Gunter, C. A. and Scott, D. S. (1990). Semantic domains. In van Leeuwen, J., editor, Handbook of Theoretical Computer Science, volume B, pages 633–674. Elsevier.

Honda, K. and Yoshida, N. (1997). Game theoretic analysis of call-by-value computation. In Degano, P., Gorrieri, R., and Marchetti-Spaccamela, A., editors, Automata, Languages and Programming: 24^{th} International Colloquium, volume 1256 of Lect. Notes in Computer Sci. Springer-Verlag.

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

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

Jung, A. and Stoughton, A. (1993). 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.

Jung, A. and Tiuryn, J. (1993). 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.

Loader, R. (1997). Finitary PCF is not decidable. Unpublished manuscript

available from http://www.dcs.ed.ac.uk/~loader.

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

McCusker, G. (1997). Games and definability for FPC. Bulletin of Symbolic Logic, 3(3):347–362.

Marz, M. (1998) A fully abstract model for sequential computation. Technical Report CSR-98-06, Department of Computer Science, University of Birmingham, 1998.

Meyer, A. R. (1988). Semantical paradigms: Notes for an invited lecture, with two appendices by Stavros S. Cosmadakis. In Proceedings, Third Annual Symposium on Logic in Computer Science, pages 236–255. IEEE.

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

Milner, R., Tofte, M., Harper, R., and MacQueen, D. (1997). The Definition of Standard ML (Revised). MIT Press.

Moggi, E. (1991). Notions of computation and monads. Information and Control, 93:55–92.

Mulmuley, K. (1987). Full Abstraction and Semantic Equivalence. ACM Doctoral Dissertation Award 1986. MIT Press.

Nickau, H. (1994). Hereditarily sequential functionals. In Nerode, A. and Matiyasevich, Y., editors, Proceedings of the Symposium on Logical Foundations of Computer Science: Logic at St. Petersburg, volume 813 of Lect. Notes in Computer Sci. Springer-Verlag.

O’Hearn, P. W. and Reynolds, J. C. (1997). From Algol to polymorphic linear lambda calculus. Unpublished manuscript available from

http://www.dcs.qmw.ac.uk/~ohearn.

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:658–709.

Pitts, A. M. (1996). Relational properties of domains. Information and Computation, 127:66–90.

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

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

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

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

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

Riecke, J. G. and Subrahmanyam, R. (1997). Semantic orthogonality of type disciplines. Unpublished manuscript available from

http://www.cs.bell-labs.com/who/riecke/.

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

Riecke, J. G. and Viswanathan, R. (1995). 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.

Sieber, K. (1992). 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.

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

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

A Proof of Adequacy

To establish the adequacy of the model, we follow the proof techniques of (Meyer, 1988; Plotkin, 1985; Riecke and Subrahmanyam, 1997). There are two main steps. First, we define a notion of an “adequacy relation” between elements of the model and terms, and show that the meanings of terms and the terms themselves are related by any adequacy relation. Second, we construct a particular adequacy relation. The properties of the adequacy relation allow us to conclude that the model is adequate. Since the proof is not novel, we omit many of the details that are easy to check.

A.1 Adequacy relations

Definition A.1 An adequacy relation is a family of relations ≤_{s}, indexed by closed types, between elements of [[s]] and closed terms of type s. The following conditions must also hold.

1. d ≤_{void} M holds vacuously (since there is no d ∈ void).

2. ⊤ ≤_{unit} M iff M ⇓ ⟨⟩.

3. (inj_{i} e) ≤_{s_{1}⊕s_{2}} M iff M ⇓ (inj_{i} V) and (e ≤_{s_{i}} V).

4. ⟨e_{1}, e_{2}⟩ ≤_{s_{1}⊗s_{2}} M iff M ⇓ ⟨V_{1}, V_{2}⟩ and (e_{i} ≤_{s_{i}} V_{i}).

5. f ≤_{s_{1}⇒s_{2}} M iff M ⇓ (λx : s_{1}. N), and e ≤_{s_{1}} P implies f(e) ≲_{s_{2}} (M P).

6. e ≤_{rec α. s} M iff M ⇓ (intro V) and elim(e) ≤_{s[rec α. s/α]} V.

In the clause for function types, exp ≲_{s} M means either exp is undefined, or it is defined and exp ≤_{s} M.

Lemma A.2 Suppose ≤ is an adequacy relation, d ≤_{s} M, M ⇓ V, and N ⇓ V. Then d ≤_{s} N.

Proof: By a simple case analysis on s.

Lemma A.3 Suppose ≤ is an adequacy relation, e_{i} ≤_{s_{i}} M_{i}, ρ = ⟨e_{1}, …, e_{n}⟩, Γ = (x_{1} : s_{1}, …, x_{n} : s_{n}), and Γ ⊢ M : s. Then

[[Γ ⊢ M : s]]ρ ≲_{s} M[M_{1}, …, M_{n}/x_{1}, …, x_{n}].

Proof: By induction on the derivation of Γ ⊢ M : s. We give a few of the cases and leave the others to the reader.

1. Γ ⊢ x_{i} : s_{i}. Then [[Γ ⊢ x_{i} : s_{i}]]ρ = ρ(x_{i}) ≤_{s_{i}} M_{i} by the hypothesis.

2. Γ ⊢ (N P) : t where Γ ⊢ N : (s → t) and P : s. Follows easily from the induction hypothesis.

3. Γ ⊢ (λx : s. N) : (s → t) where Γ, x : s ⊢ N : t. Suppose e ≤_{s} P, and let

M′ = ((λx : s. N) P)[M_{1}, …, M_{n}/x_{1}, …, x_{n}]

By the induction hypothesis,

d′ = [[Γ, x : s ⊢ N : t]]ρ[x ↦ e] ≲_{t} N[M_{1}, …, M_{n}, P/x_{1}, …, x_{n}, x] = N′.

Thus, either d′ is not defined, or it is defined and d′ ≤_{t} N′. In the first case, d′ ≲_{t} M′. In the second case, N′ ⇓ V for some V. Note then that M′ ⇓ V. By Lemma A.2, d′ ≤_{t} M′. Thus, by the property of adequacy relations,

[[Γ ⊢ (λx : s. N) : (s → t)]]ρ ≲_{s→t} (λx : s. N)[M_{1}, …, M_{n}/x_{1}, …, x_{n}].

as desired.

4. Γ ⊢ (elim N) : t[rec α. t/α], where Γ ⊢ N : (rec α. t). Follows directly from the induction hypothesis and the definition of adequacy relations.

5. Γ ⊢ (intro N) : (rec α. t), where Γ ⊢ N : t[rec α. t/α]. By the induction hypothesis,

[[Γ ⊢ N : t[rec α. t/α]]]ρ ≲_{t[rec α. t/α]} N[M_{1}, …, M_{n}/x_{1}, …, x_{n}].

Suppose the left side is defined (the other case holds easily). Then

N[M_{1}, …, M_{n}/x_{1}, …, x_{n}] ⇓ V for some V,

and hence

(intro N)[M_{1}, …, M_{n}/x_{1}, …, x_{n}] ⇓ (intro V).

Recall that elim ∘ intro = id. Thus, since N[M_{1}, …, M_{n}/x_{1}, …, x_{n}] ⇓ V and (elim (intro V)) ⇓ V, it follows by Lemma A.2 that

elim([[Γ ⊢ (intro N) : rec α. t]]ρ) ≤_{t[rec α. t/α]} V.

Therefore, by definition of adequacy relations,

[[Γ ⊢ (intro N) : rec α. t]]ρ ≲_{rec α. t} (intro N)[M_{1}, …, M_{n}/x_{1}, …, x_{n}].

as desired.

This completes the induction and hence the proof.

Definition A.4 Suppose s is a closed type. A relation R between elements of [[s]] and closed terms of type s is directed complete if for any directed set {d_{i} | i ∈ I} such that for all i ∈ I, d_{i} R M, then (⊔d_{i}) R M.

Definition A.5 Suppose θ is a substitution from type variables to closed types, and R is a map from type variables to directed-complete relations. We say that R is compatible with θ if for all α, R(α) is a binary relation between [[θ(α)]] and closed terms of type θ(α).

Definition A.6 For all open types s, define the family

(≤_{s,R}| R compatible with θ),

where ≤_{s,R} is a relation between elements of [[θ(s)]] and closed terms of type θ(s), as follows:

1. d ≤_{α,R} M iff d R(α) M.

2. d ≤_{void,R} M holds vacuously.

3. ⊤ ≤_{unit,R} M iff M ⇓ ⟨⟩.

4. (inj_{i} e) ≤_{s_{1}⊕s_{2},R} M iff M ⇓ (inj_{i} V) and (e ≤_{s_{i},R} V).

5. ⟨e_{1}, e_{2}⟩ ≤_{s_{1}⊗s_{2},R} M iff M ⇓ ⟨V_{1}, V_{2}⟩ and (e_{i} ≤_{s_{i},R} V_{i}).

6. f ≤_{s_{1}⇒s_{2},R} M iff M ⇓ (λx : s_{1}. N), and e ≤_{s_{1},R} P implies f(e) ≲_{s_{2},R} (M P).

7. If s = (rec α. t), then e ≤_{s,R} M iff for all n ≥ 0, (μ_{θ(s)}^{n,p} e) ≲_{n,R}^{s} M, where ≤_{n,R}^{s} are the relations defined by

e ≤_{0,R}^{s} N ⟺ true
e ≤_{n+1,R}^{s} N ⟺ N ⇓ (intro V′) and e ≤_{t,R[α↦≤_{n,R}^{s}]} V′.

(Recall that μ_{θ(s)}^{n} are the maps in the colimiting cocone from Section 3.8.)

Lemma A.7 Suppose R is compatible with θ. Then for any type s, ≤_{s,R} is a directed-complete relation between elements of [[θ(s)]] and closed terms of type θ(s).

Lemma A.8 ≤_{t,R[α↦≤_{s,R}]}=≤_{t[s/α],R}

Proof: By induction on t. The only difficult case is t = (rec β. u). Let R′ = R[α ↦≤_{s,R}] and t′ = t[s/α]. Note that ≤_{0,R}^{t′}=≤_{0,R′}^{t}, and ≤_{n,R}^{t′}=≤_{n,R′}^{t} implies that ≤_{n+1,R}^{t′}=≤_{n+1,R′}^{t} using the induction hypothesis. Thus, for all n, ≤_{n,R}^{t′}=≤_{n,R′}^{t}, and hence

d ≤_{t,R′} M ⟺ d ≤_{t′,R} M

as desired.

Definition A.9 If s is a closed type and R is a relation between elements of [[s]] and closed terms of type s, we write exp R̃ M if either the expression exp is undefined, or it is defined and exp R M.

Lemma A.10 Suppose π : η → η′ is a ep-pair environment (i.e., mapping type variables to ep-pairs, not just pre-ep-pairs) and for all α,

d R(α) M implies π(α)^{e}(d) R′(α) M
d R′(α) M implies π(α)^{p}(d) { \atop R(α)} M

Then

1. If d ≤_{s,R} M, then ([[s]]π)^{e}(d) ≤_{s,R′} M.

2. If d ≤_{s,R′} M, then ([[s]]π)^{p}(d) ≲_{s,R} M.

Proof: By induction on s, proving both claims simultaneously. Most of the cases are straightforward; the only case that is not is when s = (rec α. t). For this case, we first prove a claim. Let ≤_{n,R}^{s} and ≤_{n,R′}^{s} be the relations defined above. We claim that for all n,

• If e ≤_{n,R}^{s} N, then p_{s,π}^{n,e}(e) ≤_{n,R′}^{s} N.

• If e ≤_{n,R′}^{s} N, then p_{s,π}^{n,p}(e) ≲_{n,R}^{s} N.

We prove the claim by induction on n. The basis is easy, so consider the induction case. Let

π′ = π[α ↦ p_{s,π}^{n}] : η[α ↦ T_{s,η}^{n}] → η′[α ↦ T_{s,η′}^{n}]

Since p_{s,π}^{n} is an ep-pair (by a simple induction on the definition of p_{s,π}^{n}), π′ is an ep-pair environment. To see the second part of the claim, suppose e ≤_{n+1,R′}^{s} N. Then N ⇓ (intro V) and e ≤_{t,R′[α↦≤_{n,R′}^{s}]} V. By the induction hypothesis,

p_{s,π}^{n+1,p}(e) = ([[t]]π′)^{p}(e) ≲_{t,R[α↦≤_{n,R}^{s}]} V

and hence p_{s,π}^{n+1,p}(e) ≲_{n+1,R}^{s} N. The first part holds analogously, completing the proof of the claim.

Using the claim, we can now prove the lemma. We prove only the second part and leave the other to the reader. Suppose d ≤_{s,R′} M. Then for all n, μ_{s,η′}^{n,p}(d) ≲_{n,R′}^{s} M. By the claim, p_{s,π}^{n,p}(μ_{s,η′}^{n,p}(d)) ≲_{n,R}^{s} M. By general facts about the colimit, p_{s,π}^{n,p} ∘ μ_{s,η′}^{n,p} = μ_{s,η}^{n,p} ∘ ([[s]]π)^{p}, so for all n,

μ_{s,η}^{n,p} (([[s]]π)^{p} (d)) ≲_{n,R}^{s} M.

Thus, ([[s]]π)^{p} (d) ≲_{s,R} M as desired.

Lemma A.11 Suppose s = (rec α. t) and ≤_{n,R}^{s} are the relations defined above. If d ≤_{k,R}^{s} M, then μ_{s,η}^{k,e}(d) ≤_{s,R} M.

Proof: First, we claim that the following two statements hold:

• If d ≤_{n,R}^{s} M, then f_{s,η}^{n,e}(d) ≤_{n+1,R}^{s} M.

• If d ≤_{n+1,R}^{s} M, then f_{s,η}^{n,p}(d) ≲_{n,R}^{s} M.

We prove the claim by induction on n. The base case is straightforward. For the induction case, we prove the first statement and leave the second to the reader. Now, assume that d ≤_{n,R}^{s} M implies f_{s,η}^{n,e}(d) ≤_{n+1,R} M. Recall that f_{s,η}^{n+1,e} = ([[t]](id[α ↦ f_{s,η}^{n}]))^{e}. Therefore, for any β,

d R[α ↦≤_{n,R}^{s}](β) M implies (id[α ↦ f_{s,η}^{n}](β))^{e}(d) R[α ↦≤_{n+1,R}^{s}](β) M.

So suppose d ≤_{n+1,R}^{s} M; then M ⇓ (intro V) and d ≤_{t,R[α↦≤_{n,R}]} V. By Lemma A.10 (1),

([[t]](id[α ↦ f_{s,η}^{n}]))^{e}(d) ≤_{t,R[α↦≤_{n+1,R}]} V

and so f_{s,η}^{n+1,e}(d) ≤_{n+2,R}^{s} M.

We can now prove the lemma. Suppose d ≤_{k,R}^{s} M. We show that for all n ≥ 0, μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d)) ≲_{n,R}^{s} M. There are two cases:

• If n < k, then

μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d)) = f_{s,η}^{n,p} (f_{s,η}^{n+1,p} (… f_{s,η}^{k,p} (d) …)).

By repeated uses of the second part of the claim,

f_{s,η}^{n,p} (f_{s,η}^{n+1,p} (… f_{s,η}^{k,p} (d) …)) ≲_{n,R}^{s} M.

• If n ≥ k, we proceed by induction on n. In the basis, n = k, and μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d)) = d ≤_{n,R}^{s} M by hypothesis. For the induction case, note that

μ_{s,η}^{n+1,p} (μ_{s,η}^{k,e} (d)) = f_{s,η}^{n,e} (μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d))).

By the induction hypothesis, μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d)) ≤_{n,R}^{s} M. By the first part of the claim,

f_{s,η}^{n,e} (μ_{s,η}^{n,p} (μ_{s,η}^{k,e} (d))) ≤_{n+1,R}^{s} M

as desired.

This completes the proof.

Lemma A.12 Let R be compatible with θ. Then the family of relations ≤_{s,R} for all closed types s forms an adequacy relation.

Proof: The only tricky part then is to verify condition (6) of the definition of adequacy relations. Suppose s = (rec α. t) is a closed type, and pick any η. To see one direction of (6), suppose d ≤_{s,R} M. Then for all n,

d_{n} = μ_{s,η}^{n,p} (d) ≲_{n,R}^{s} M.

In particular, M ⇓ (intro V) and for all n,

d_{n+1} ≲_{t,R[α↦≤_{n,R}^{s}]} V.

By Lemmas A.10 and A.11,

([[t]](id[α ↦ μ_{s,η}^{n}]))^{e}(d_{n+1}) ≲_{t,R[α↦≤_{s,R}]} V.

But note that ([[t]](id[α ↦ μ_{s,η}^{n}]))^{e} = elim ∘ μ_{s,η}^{n+1,e}. Thus, for all n,

elim(μ_{s,η}^{n+1,e}(d_{n+1})) ≲_{t,R[α↦≤_{s,R}]} V

and hence by Lemma A.7,

⨆_{n≥0} elim(μ_{s,η}^{n+1,e}(d_{n+1})) = elim(d) ≲_{t,R[α↦≤_{s,R}]} V

as desired. The converse holds by a similar argument.

The Adequacy Theorem 4.1 now follows directly from Lemmas A.3 and A.12.

B Proof of Lemma 6.1

The proof of Lemma 6.1 uses techniques from (Riecke and Subrahmanyam, 1997). In outline, we show how to construct, from the syntax of the language, pre-ep-pairs which mimic the semantic pre-ep-pairs in the construction of the model. We use these to construct the desired terms clm_{s,n}^{e} and clm_{s,n}^{p}.

Given type expressions s and s′, a pair of closed terms

M : s ⇒ s′ and M′ : s′ ⇒ s

is called a syntactic pre-ep-pair from s to s′ (written ⟨M, M′⟩ : s ↪ s′). Some notation on syntactic pre-ep-pairs will be helpful. If P is a syntactic preep-pair, P^{e} and P^{p} represent its first and second components respectively, and P^{−1} denotes the pair ⟨P^{p}, P^{e}⟩. There are also several constructions for building complex syntactic pre-ep-pairs from simple ones. Let M : s ↪ t, N : t ↪ u and P : s′ ↪ t′. Define

id_{s} : s ↪ s = ⟨λx : s. x, λx : s. x⟩ !_{t} : void ↪ t = ⟨Ω, Ω⟩

      iso_{rec α. t} : t[rec α. t/α] ↪ rec α. t = ⟨intro_{rec α. t}, elim_{rec α. t}⟩

iso_{rec α. t}^{−1} : (rec α. t) ↪ t[rec α. t/α] = ⟨elim_{rec α. t}, intro_{rec α. t}⟩
(N ∘ M) : s ↪ u = ⟨N^{e} ∘ M^{e}, M^{p} ∘ N^{p}⟩

(M ⊕ P) : (s ⊕ s′) ↪ (t ⊕ t′) = ⟨λx : s ⊕ s′. case x ofinj_{1}(y).(M^{e} y) orinj_{2}(y).(P^{e} y), λx : t ⊕ t′. case x ofinj_{1}(y).(M^{p} y) orinj_{2}(y).(P^{p} y)⟩

(M ⊗ P) : (s ⊗ s′) ↪ (t ⊗ t′) = ⟨λx : s ⊗ s′. ⟨M^{e} (proj_{1} x), P^{e} (proj_{2} x)⟩,
λx : t ⊗ t′. ⟨M^{p} (proj_{1} x), P^{p} (proj_{2} x)⟩⟩

(M ⇒ P) : (s ⇒ s′) ↪ (t ⇒ t′) = ⟨λx : s ⇒ s′. P^{e} ∘ x ∘ M^{p}, λx : t ⇒ t′. P^{p} ∘ x ∘ M^{e}⟩

where, abusing notation, (Q ∘ Q′) stands for the term (λx. Q (Q′ x)).

We use these constructions in defining terms ⟨F_{s}^{e}, F_{s}^{p}⟩ that syntactically represent the action, on syntactic pre-ep-pairs, of the functor [[s]] on semantic pre-ep-pairs. The terms are defined by induction on the structure of s. As with the functors, the syntactic terms take in a map, usually denoted pi, from type variables to syntactic pre-ep-pairs. These maps go between type substitutions θ, i.e., maps from type variables to closed types. More precisely, we write pi : θ ↪ θ′ if θ, θ′ are type substitutions such that for all α, pi(α) : θ(α) ↪ θ′(α). We write \overline{id} : θ ↪ θ to denote the map where for all type variables α, \overline{id}(α) = id_{θ(α)}.

To define the syntactic representation of the functor, let s be a type, and pi : θ ↪ θ′. Let θ(τ) denote the type produced from applying the type substitution θ to τ. The term F_{s}(pi) : θ(s) ↪ θ′(s) is a syntactic pre-ep-pair defined by induction on s:

F_{α}(pi) = pi(α)

      F_{unit}(pi) = id_{unit}

F_{s⇒t}(pi) = F_{s}(pi) ⇒ F_{t}(pi)
F_{rec α. t}(pi) = fix (λf. iso_{θ′(rec α. t)} ∘ F_{t}(pi[α ↦ f]) ∘ iso_{θ(rec α. t)}^{−1})

A similar definition appears elsewhere (Abadi and Fiore, 1996). In the definition, the term fix in the last line is shorthand for the term λg. Δ (intro Δ), where

Δ = λx. ⟨λy. (proj_{1} (g ((elim x) x))) y, λz. (proj_{2} (g ((elim x) x))) z⟩.

The term fix is a simple modification of the call-by-value recursion combinator (see (Gunter, 1992)); it defines a pair ⟨F_{rec α. t}^{e}(pi), F_{rec α. t}^{p}(pi)⟩ by mutual recursion.

We will show that the semantic functor [[s]] coincides with the syntactic functor F_{s}. In order to do this, we must have a way to connect semantic preep-environments π with syntactic pre-ep-environments pi. Suppose π is a morphism in ℰ (see previous subsection) and η is a type environment. Then π matches pi : θ ↪ θ′ if for all type variables α, [[pi(α)]] = π(α).

Suppose pi : θ ↪ θ′ and s = (rec α. t). For any g : θ(s) ↪ θ′(s), define J_{s}(pi, g) : θ(s) ↪ θ′(s) by

J_{s}(pi, g) = iso_{θ′(s)} ∘ F_{t}(pi[α ↦ g]) ∘ iso_{θ(s)}^{−1}.

Define

J_{s}^{0}(pi, g) = g
J_{s}^{n+1}(pi, g) = J_{s}(pi, J_{s}^{n}(pi, g))

Lemma B.1 [[F_{s}(pi)]] = ⨆_{n≥0}[[J_{s}^{n}(pi, Ω)]].

Theorem B.2 (Correspondence) Suppose π matches pi : θ_{1} ↪ θ_{2}. Then [[s]]π = [[F_{s}(pi)]].

Proof: By induction on the structure of s. We consider four of the cases here.

1. s = α. Then [[F_{α}(pi)]] = [[pi(α)]] = π(α) = [[α]](π) by the hypothesis that π matches pi.

2. s = unit, void. Then [[F_{s}(pi)]] = id_{s} = [[s]]π.

3. s = (s_{1} ⇒ s_{2}). Then

[[F_{s}(pi)]] = [[(F_{s_{1}}(pi) ⇒ F_{s_{2}}(pi))]]
= ([[F_{s_{1}}(pi)]] ⇒ [[F_{s_{2}}(pi)]])
= [[s_{1}]]π ⇒ [[s_{2}]]π
= [[s]]π

4. s = (rec α. t). Define type environments η_{1} and η_{2} by η_{1}(α) = [[θ_{1}(α)]] and η_{2}(α) = [[θ_{2}(α)]]. We claim that [[F_{s}(pi)]] is the unique mediating map from [[s]]η_{1} = T_{s,η_{1}} to [[s]]η_{2} = T_{s,η_{2}}. The proof of the claim is quite similar to the proof of the existence of Freyd’s minimal invariants from (Abramsky and Jung, 1994; Pitts, 1996), but we present the argument in detail because of the slight difference in setting with type environments.

Recall the definitions of μ_{s,η}^{n} and p_{s,π}^{n} and the definition of J_{s}^{n} above. To prove the claim, we note three facts:

• For any type environment η, μ_{s,η}^{n+1} = [[iso]] ∘ [[t]](id[α ↦ μ_{s,η}^{n}]).

• [[J_{s}^{n}(pi, Ω)]] is a pair of partial functions.

• [[J_{s}^{n}(pi, Ω)]] ∘ μ_{s,η_{1}}^{n} = μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n}.

The first fact holds from general principles about the colimit. The second may be proved by induction on n, using the induction hypothesis of the theorem. The proof of the third proceeds by induction on n. The base case, when n = 0, is easy. For the induction step,

[[J_{s}^{n+1}(pi, Ω) ∘ μ_{s,η_{1}}^{n+1}]]
= [[iso]] ∘ [[F_{t}(pi[α ↦ J_{s}^{n}(pi, Ω)])]] ∘ [[iso^{−1}]] ∘ μ_{s,η_{1}}^{n+1}
= [[iso]] ∘ [[t]](π[α ↦ [[J_{s}^{n}(pi, Ω)]]]) ∘ [[t]](id[α ↦ μ_{s,η_{1}}^{n}])
= [[iso]] ∘ [[t]](π[α ↦ [[J_{s}^{n}(pi, Ω)]] ∘ μ_{s,η_{1}}^{n}])
= [[iso]] ∘ [[t]](π[α ↦ μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n}])
= [[iso]] ∘ [[t]](id[α ↦ μ_{s,η_{2}}^{n}]) ∘ [[t]](π[α ↦ p_{s,π}^{n}])
= μ_{s,η_{2}}^{n+1} ∘ p_{s,π}^{n+1}

as desired, where the second line follows by the induction hypothesis of the theorem (the fact that the semantic functor [[s]] coincides with F_{s}) , and the fourth line follows by the induction hypothesis.

These facts can be used to prove the claim. Any mediating map must be unique, since ⟨[[s]]η_{1}, μ_{s,η_{1}}^{n} | n ≥ 0⟩ is a colimiting cocone for the chain ⟨T_{s,η_{1}}^{i}, f_{s,η_{1}}^{i} | i ≥ 0⟩ and ⟨[[s]]η_{2}, μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n} | n ≥ 0⟩ is a cocone for the same chain. Thus, all we need to do is to show that F_{s}(pi) is a mediating map, i.e., for all n ≥ 0,

[[F_{s}(pi)]] ∘ μ_{s,η_{1}}^{n} = μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n}.

To see this, for any type s and type environment η, define f_{s,η}^{n⇒m} to be the composition of the maps from T_{s,η}^{n} to T_{s,η}^{m}; then for any n ≤ m,

[[J_{s}^{m}(pi, Ω)]] ∘ μ_{s,η_{1}}^{n} = [[J_{s}^{m}(pi, Ω)]] ∘ μ_{s,η_{1}}^{m} ∘ f_{s,η_{1}}^{n⇒m}
= μ_{s,η_{2}}^{m} ∘ p_{s,π}^{m} ∘ f_{s,η_{1}}^{n⇒m}
= μ_{s,η_{2}}^{m} ∘ f_{s,η_{2}}^{n⇒m} ∘ p_{s,π}^{n}
= μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n}

and hence

[[F_{s}(pi)]] ∘ μ_{s,η_{1}}^{n} = ( ⨆_{m≥0}[[J_{s}^{m}(pi, Ω)]]) ∘ μ_{s,η_{1}}^{n}
= ⨆_{m≥0} μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n} = μ_{s,η_{2}}^{n} ∘ p_{s,π}^{n}

as desired. This completes the induction and hence the proof.

Define two families of syntactic pre-ep-pairs

unwnd_{s,i} : s^{i} ↪ s^{i+1} and clm_{s,i} : s^{i} ↪ s

by induction on s. Most of the definition is straightforward—the main difficulty lies when s is a recursive type.

1. For type variables, unwnd_{α,n} = id_{α} and clm_{α,n} = id_{α}.

2. For the base types s = void, unit, let unwnd_{s,n} = id_{s} and clm_{s,n} = id_{s}.

3. For sum, product, and function types, let

unwnd_{s_{1}⇒s_{2},n} = unwnd_{s_{1},n} ⇒ unwnd_{s_{2},n}
clm_{s_{1}⇒s_{2},n} = clm_{s_{1},n} ⇒ clm_{s_{2},n}

and similarly for sums and products.

4. For recursive types, suppose s = (rec α. t). Define the family of types

T_{s,k}^{n}, for n, k ≥ 0, by

T_{s,k}^{0} = void
T_{s,k}^{n+1} = t_{k}[T_{s,k}^{n}/α].

Notice that, for any n, T_{s,n}^{n} is the same as s_{n} defined above. Define two families of syntactic pre-ep-pairs

f_{s,k}^{n} : T_{s,k}^{n} ↪ T_{s,k+1}^{n} and g_{s,k}^{n} : T_{s,k}^{n} ↪ T_{s,k}^{n+1}

by

f_{s,k}^{0} = !_{void}      f_{s,k}^{n+1} = F_{t_{k+1}}(\overline{id}[α ↦ f_{s,k}^{n}]) ∘ unwnd_{t,k}[T_{s,k}^{n}/α]
g_{s,k}^{0} = !_{T_{s,k}^{1}}  g_{s,k}^{n+1} = F_{t_{k}}(\overline{id}[α ↦ g_{s,k}^{n}])

A diagram clarifies these types and functions:

[figure: ⋮; ⋮; ⋮; T_{s,0}^{2}; _{g{0 \atop s,2}}; _{f{2 \atop s,0}}; T_{s,1}^{2}; _{g{1 \atop s,2}}; _{f{2 \atop s,1}}; T_{s,2}^{2}; _{g{2 \atop s,2}}; _{f{2 \atop s,2}}; ⋯; T_{s,0}^{1}; _{g{0 \atop s,1}}; _{f{1 \atop s,0}}; T_{s,1}^{1}; _{g{1 \atop s,1}}; _{f{1 \atop s,1}}; T_{s,2}^{1}; _{g{2 \atop s,1}}; _{f{1 \atop s,2}}; ⋯; void; _{g{0 \atop s,0}}; _{f{0 \atop s,0}}; void; _{g{1 \atop s,0}}; _{f{0 \atop s,1}}; void; _{g{2 \atop s,0}}; _{f{0 \atop s,2}}; ⋯]

Then define the maps unwnd_{s,n} along the main diagonal:

unwnd_{s,n} = f_{s,n}^{n+1} ∘ g_{s,n}^{n}

For the colimiting maps, define clm_{s,k}^{n} : T_{s,k}^{n} ↪ s by

clm_{s,k}^{0} = !_{s}
clm_{s,k}^{n+1} = iso_{s} ∘ F_{t}(\overline{id}[α ↦ clm_{s,k}^{n}]) ∘ clm_{t,k}[T_{s,k}^{n}/α]

and set clm_{s,n} = clm_{s,n}^{n}. In order to prove Lemma 6.1, we need to break up the definition of the

colimiting maps on recursive types into two pieces. Suppose s = (rec α. t). Define the syntactic pre-ep-pairs h_{s,k}^{n} : T_{s,k}^{n} ↪ T_{s}^{n} and mu_{s}^{n} : T_{s}^{n} ↪ s, where

T_{s}^{0} = void  T_{s}^{n+1} = t[T_{s}^{n}/α]
h_{s,k}^{0} = id_{void}       h_{s,k}^{n+1} = F_{t}(\overline{id}[α ↦ h_{s,k}^{n}]) ∘ clm_{t,k}[T_{s,k}^{n}/α]
mu_{s}^{0} = !_{s}  mu_{s}^{n+1} = iso_{s} ∘ F_{t}(\overline{id}[α ↦ mu_{s}^{n}])

Lemma B.3 [[θ(mu_{s}^{n})]] = μ_{θ(s)}^{n}. The proof follows from the Correspondence Theorem and the properties of colimits. Lemma B.4 [[θ(clm_{s,k}^{n})]] = [[mu_{s}^{n} ∘ h_{s,k}^{n}]].

Proof: By induction on n; to simplify notation, we omit meaning brackets below. The base case is trivial; the induction step is as follows:

θ(mu_{s}^{n+1} ∘ h_{s,k}^{n+1})
= θ(iso_{s} ∘ F_{t}(\overline{id}[α ↦ mu_{s}^{n}]) ∘ F_{t}(\overline{id}[α ↦ h_{s,k}^{n}]) ∘ clm_{t,k}[T_{s,k}^{n}/α])
= θ(iso_{s} ∘ F_{t}(\overline{id}[α ↦ mu_{s}^{n} ∘ h_{s,k}^{n}]) ∘ clm_{t,k}[T_{s,k}^{n}/α])
= θ(iso_{s} ∘ F_{t}(\overline{id}[α ↦ clm_{s,k}^{n}]) ∘ clm_{t,k}[T_{s,k}^{n}/α])
= θ(clm_{s,k}^{n+1})

where the first equality follows from the definition of mu_{s}^{n+1}, h_{s,k}^{n+1}, the second from syntactic functoriality, the third from the induction hypothesis, and the forth from the definition of clm_{s,k}^{n+1}. This completes the induction step and hence the proof.

Lemma B.5 For any s and θ, ⨆_{n≥0}[[θ(clm_{s,n}^{e} ∘ clm_{s,n}^{p})]] = id_{[[θ(s)]]}.

Proof: We proceed by induction on s, omitting meaning brackets to simplify the notation. We give only the case of s = (rec α. t) and leave the others to the reader. We claim

⨆_{k≥0} θ(h_{s,k}^{n,e} ∘ h_{s,k}^{n,p}) = id.

We prove the claim by induction on n. The basis, n = 0, is easy, so for the induction step,

⨆_{k≥0} θ(h_{s,k}^{n+1,e} ∘ h_{s,k}^{n+1,p})

= ⨆_{k≥0} θ(F_{t}^{e}(\overline{id}[α ↦ h_{s,k}^{n,e}]) ∘ clm_{t,k}^{e}[T_{s,k}^{n}/α] ∘ clm_{t,k}^{p}[T_{s,k}^{n}/α] ∘ F_{t}^{p}(\overline{id}[α ↦ h_{s,k}^{n,e}]))

= ⨆_{k,m≥0} θ(F_{t}^{e}(\overline{id}[α ↦ h_{s,k}^{n,e}]) ∘ clm_{t,m}^{e}[T_{s,k}^{n}/α] ∘ clm_{t,m}^{p}[T_{s,k}^{n}/α] ∘ F_{t}^{p}(\overline{id}[α ↦ h_{s,k}^{n,e}]))

= ⨆_{k,m≥0} θ(F_{t}^{e}(\overline{id}[α ↦ h_{s,k}^{n,e}]) ∘ (clm_{t,m}^{e} ∘ clm_{t,m}^{p})[T_{s,k}^{n}/α] ∘ F_{t}^{p}(\overline{id}[α ↦ h_{s,k}^{n,e}]))

= ⨆_{k≥0} θ(F_{t}^{e}(\overline{id}[α ↦ h_{s,k}^{n,e}]) ∘ ( ⨆_{m≥0} clm_{t,m}^{e} ∘ clm_{t,m}^{p})[T_{s,k}^{n}/α] ∘ F_{t}^{p}(\overline{id}[α ↦ h_{s,k}^{n,e}]))

= ⨆_{k≥0} θ(F_{t}^{e}(\overline{id}[α ↦ h_{s,k}^{n,e}]) ∘ F_{t}^{p}(\overline{id}[α ↦ h_{s,k}^{n,e}]))

= id

where the second line follows from Bekič’s Lemma, the fifth from the global induction hypothesis, and the last by a simple induction on t, using the local induction hypothesis. Taking advantage of this fact,

⨆_{n≥0} θ(clm_{s,n}^{e} ∘ clm_{s,n}^{p}) = ⨆_{n≥0} θ(clm_{s,n}^{n,e} ∘ clm_{s,n}^{n,p})
= ⨆_{k,n≥0} θ(clm_{s,k}^{n,e} ∘ clm_{s,k}^{n,p})
= ⨆_{k,n≥0} θ(mu_{s}^{n,e} ∘ h_{s,k}^{n,e} ∘ h_{s,k}^{n,p} ∘ mu_{s}^{n,p})
= ⨆_{n≥0} θ(mu_{s}^{n,e} ∘ ( ⨆_{k≥0} h_{s,k}^{n,e} ∘ h_{s,k}^{n,p}) ∘ mu_{s}^{n,p})
= ⨆_{n≥0} θ(mu_{s}^{n,e} ∘ mu_{s}^{n,p})
= id_{θ(s)}

where the third line follows from Lemma B.4, the fifth from the claim, and the last by Lemma B.3 and the properties of colimits. This completes the induction and hence the proof.

Lemma 6.1 now follows directly from Lemma B.5.

Recent BRICS Report Series Publications

RS-99-10 Jon G. Riecke and Anders B. Sandholm. A Relational Account of Call-by-Value Sequentiality. March 1999. 51 pp. To appear in Information and Computation, LICS ’97 Special Issue. Extended version of an article appearing in Twelfth Annual IEEE Symposium on Logic in Computer Science, LICS ’97 Proceedings, 1997, pages 258–267. This report supersedes the earlier report BRICS RS-97-41.

RS-99-9 Claus Brabrand, Anders Møller, Anders B. Sandholm, and Michael I. Schwartzbach. A Runtime System for Interactive Web Services. March 1999. 21 pp. Appears in Mendelzon, editor, Eighth International World Wide Web Conference, WWW8 Proceedings, 1999, pages 313–323 and Computer Networks, 31:1391–1401, 1999.

RS-99-8 Klaus Havelund, Kim G. Larsen, and Arne Skou. Formal Verification of a Power Controller Using the Real-Time Model Checker Uppaal. March 1999. 23 pp. To appear in Katoen, editor, 5th International AMAST Workshop on Real-Time and Probabilistic Systems, ARTS ’99 Proceedings, LNCS, 1999.

RS-99-7 Glynn Winskel. Event Structures as Presheaves—Two Representation Theorems. March 1999. 16 pp.

RS-99-6 Rune B. Lyngsø, Christian N. S. Pedersen, and Henrik Nielsen. Measures on Hidden Markov Models. February 1999. 27 pp. To appear in Seventh International Conference on Intelligent Systems for Molecular Biology, ISMB ’99 Proceedings, 1999.

RS-99-5 Julian C. Bradfield and Perdita Stevens. Observational Mu-Calculus. February 1999. 18 pp.

RS-99-4 Sibylle B. Fröschle and Thomas Troels Hildebrandt. On Plain and Hereditary History-Preserving Bisimulation. February 1999. 21 pp.

RS-99-3 Peter Bro Miltersen. Two Notes on the Computational Complexity of One-Dimensional Sandpiles. February 1999. 8 pp.

RS-99-2 Ivan B. Damgård. An Error in the Mixed Adversary Protocol by Fitzi, Hirt and Maurer. February 1999. 4 pp.

RS-99-1 Marcin Jurdziński and Mogens Nielsen. Hereditary History Preserving Simulation is Undecidable. January 1999. 15 pp.