Math. Struct. in Comp. Science (1993), vol. 11, pp. 1–000 Copyright \begin{matrix}c \\ ◯ \end{matrix} Cambridge University Press

Order-Enrichment for Categories of Partial Maps

Marcelo P. Fiore^{†}

Department of Computer Science,

Laboratory for Foundations of Computer Science,

University of Edinburgh, The King’s Buildings,

Edinburgh EH9 3JZ, Scotland.

<mf@dcs.ed.ac.uk>

Received October 6, 1994

Synopsis

Motivated by the desire of treating non-termination directly in the semantics of computation, the notion of approximation between programs is studied in the context of categories of partial maps. In particular, contextual approximation and specialisation are considered and shown to coincide. Moreover, after exhibiting the approximation between total maps as a primitive notion, from an arbitrary (or axiomatic) approximation order on total maps a computationally natural approximation order on partial maps is derived. The main technical contribution is a characterisation of when this approximation order between partial maps is domain-theoretic (in the sense that the category of partial maps Cpo-enriches) provided that so is the approximation order between total maps.

1. Introduction

In (Plotkin 1985) a revitalised approach to domain theory was initiated. Roughly, the idea was to eliminate the bottom from the domains and to keep the functions partially defined. Thus replacing Cppo (the category of small cppos —posets with a least element and closed under lubs of ω-chains— and continuous functions) with pCpo (the category of small cpos —posets closed under lubs of ω-chains— and partial continuous functions — see Subsection 3.1). One important point in the reformulation is the recognition of pCpo

† Research partially supported by Fundación Antorchas and The British Council grant ARG 2281/14/6, and SERC grant RR30735.

as a category of partial maps as, for example, such presentation fits better with standard formulations of recursion theory and it allows a categorical description of data types (via partial cartesian closed categories (Longo and Moggi 1984) with finite coproducts) in the presence of fixed-point operators.

Following the main motivation of the reformulation (i.e. to provide a direct treatment of non-termination in the semantics of computation) we postulate categories of partial maps as the primitive universe in which to interpret possibly non-terminating programs. Thus we study the interaction between partiality and approximation, which constitutes the starting point of our programme, initiated in (Fiore 1994; Fiore and Plotkin 1994), towards an axiomatic theory of domains.

In Section 2 the basic notions of order-enriched category theory used throughout are reviewed. In Section 3, categorical structures suitable for describing partial maps, viz. domain structures (K, D), are introduced and their induced categories of partial maps p(K, D) are defined. Examples are included. (For a thorough survey on categories of partial maps consult (Robinson and Rosolini 1988)). In Section 4 we observe that the consideration of partiality provides notions of approximation between partial maps. In particular, contextual approximation and specialisation are defined and seen to coincide. In these cases, the approximation relation between partial maps can be characterised in terms of the approximation relation between total maps and testing for totality. This exhibits the notion of approximation for partial maps as derived and, in Section 5, is used to derive a computationally natural approximation order for partial maps ( ⊏ ∼ ) from an arbitrary approximation order between total maps (⊑). Sections 6 and 7 are devoted to the problem of when ⊏ ∼ is domain-theoretic provided that so is ⊑. In particular, our main technical result (Theorem 7.1) answers by characterising those categories of partial maps p(D, K) which are Cpo-enriched with respect to ⊏ ∼ provided that the category of total maps K is Cpo-enriched with respect to ⊑ and that the domain structure (D, K) is uniform. Intuitively, the uniformity axiom makes least upper bounds of ω-chains of admissible subobjects (i.e. domains of definition of partial maps) behave like unions. The conceptual import of the characterisation, see (Fiore 1994, Chapter 10, Section 4), is the insight that provides to identify families (of admissible monos) which, when K and p(D, K) are Cpo-enriched with respect to ⊑ and ⊏ ∼ respectively and (D, K) is uniform, generate a subcanonical Grothendieck topology on K. Thus providing embeddings of small categories of domains in sheaf toposes.

2. Basic Order-Enriched Category Theory

We introduce the basic concepts of order-enrich category theory that will be needed in the sequel. (For a thorough treatment of enriched category theory consult (Kelly 1982).)

Let Preo/Poset (Cpo) be the category of small preorders/posets (cpos) and monotone (continuous) functions.

A Preo-category/Poset-category (Cpo-category) is a category whose hom-sets come equipped with a preorder/partial order (complete partial order) with respect to which composition of morphisms is a monotone (continuous) operation.

Let V denote either Poset or Cpo.

The immediate examples of Poset-categories are Poset and Cpo where each hom-set is ordered pointwise; even more, Cpo is a Cpo-category. More examples are obtained from the observation that every category K freely induces a V-category K_{V} by discretely ordering each hom-set.

For V-categories K and L, a V-functor F : K → L is a functorial mapping such that for every A, B ∈ | K | the assignment F_{A,B} : K(A, B) → L(F A, F B) is a morphism in V. Convention. To ease the notation we generally contravene some conventions of the enriched-category theorist. Particularly, we write K both for a V-category as well as for its underlying category K_{0} where the order structure has been forgotten. (This is in the vein of the usual convention of using the same notation for a poset or cpo as well as for its underlying set.) A similar convention is adopted for V-functors.

A V-adjunction χ : F ⊣ U : K → L is given by V-categories K and L, V-functors F : L → K and U : K → L, and a natural isomorphism

χ : K(F , ) ≅ L( , U ) : L^{op} × K → V.

For a category G and a V-category K, a diagram Γ in K of type G is a V-functor G_{V} → K. We have a “constant diagram” V-functor K : K → [G_{V}, K] defined as the composite K ≅ [1, K] ⟶^{[U,Id]} [G_{V}, K] where U is the unique V-functor G_{V} → 1.

A V-colimit of a diagram Γ is given by an object C of K and a natural transformation γ : Γ \underrightarrow{.} KC : G_{V} → K such that for every A ∈ | K |,

[G_{V}, K](γ, id) ∘ K_{C,A} : K(C, A) → [G_{V}, K](Γ, KA)

is an isomorphism in V. Remark. The treatment of V-colimits offered above is far from been complete and just concerns a restricted class of conical colimits (Kelly 1982). Proposition 2.1. Let G be a category, K be a Cpo-category, and Γ be a diagram in K of type G. Then, the following are equivalent: 1 (C, γ) is a Cpo-colimit of Γ. 2 (C, γ) is a Poset-colimit of Γ. 3 (C, γ) is a colimit of Γ and for every f, g : C → A, if f ∘ γ ≤ g ∘ γ then f ≤ g. □

3. Categories of Partial Maps

3.1. Categorical Setting

To motivate the definition of a partial map, observe that a partial function u : A ⇀ B is determined by its domain of definition dom(u) ⊆ A and the total function dom(u) → B induced by the mapping a ↦ u(a). Thus, every partial function A ⇀ B can be described by a pair consisting of an injection D ↣ A and a total function D → B with the same source. These descriptions are not unique, for (m, f) and (n, g) describe the same partial function if and only if

for some isomorphism i, m = n ∘ i and f = g ∘ i.  (1)

Following the above reformulation, given a category whose morphisms are to be thought of as total maps, a pair (m : D ↣ A, f : D → B) will be a description of a partial map [m, f] : A ⇀ B; and conversely, every partial map A ⇀ B will be described by some pair (D ↣ A, D → B). Formally, the descriptions (m, f) and (n, g) are regarded as equivalent whenever (1) holds; and a partial map is defined to be an equivalence class of descriptions.

When working with partial maps it is usual just to deal with their descriptions and observe that the arguments or constructions involved are independent of the chosen descriptions. For example, in a category with enough pullbacks, the composition of the partial map v = [n, g] : B ⇀ C with the partial map u = [m, f] : A ⇀ B is defined to be the partial map v ∘ u = [m ∘ f^{−1}(n), g ∘ (n^{∗}f)] : A ⇀ C where

n f n^{∗}f f^{−1}(n)  (2)

is a pullback.

The suspicious reader should check that the above definition is independent of any choice of descriptions for the partial maps, as well as for the required pullback. It is also easy to see that composition is associative, and that the partial map [id, id] is a unit for it.

Before defining categories of partial maps it will be necessary to refine the notion of partial map as the following examples show. Let pPoset be the category whose objects are posets and whose morphisms u : P ⇀ Q are partial monotone functions, in the sense that, for every x, x′ ∈ P,

if x ⊑ x′ then u(x) ⊏ ∼ u(x′)  (3)

where, for two mathematical expressions e and e′, we write e ⊏ ∼ e′ to mean that if e denotes some y ∈ Q then e′ denotes some y′ ∈ Q and y ⊑ y′. We write e ≃ e′ whenever both e ⊏ ∼ e′ and e′ ⊏ ∼ e. Further let pCpo (Plotkin 1985) be the subcategory of pPoset whose objects are cpos and whose morphisms u : P ⇀ Q are partial continuous functions, in the sense that, for every ω-chain ⟨x_{k}⟩ in P,

⨆ u(x_{k}) ≃ u( ⨆_{k∈| ω |} x_{k})  (4)

where the expression on the left is intended to be undefined if every u(x_{k}) is; or, otherwise, denote ⨆_{k_{0}≤k∈| ω |} u(x_{k}) where k_{0} is any index for which u(x_{k_{0}}) is defined. In these two categories, the domain of definition of a morphism P ⇀ Q cannot be any subobject of P: in pPoset, by (3), the only possible domains of definitions are the upper-closed subsets of P (i.e. those D ⊆ P such that for every x ∈ D and y ∈ P, x ≤ y implies y ∈ D), whilst in pCpo, by (4), they are the Scott-open subsets of P (i.e. those D ⊆ P which are upper-closed and inaccessible by lubs of ω-chains, in the sense that for every ω-chain ⟨x_{k}⟩ in P, ⨆ x_{k} ∈ D implies x_{k_{0}} ∈ D for some k_{0}).

To include such a possibility, descriptions of partial maps are to be pairs (m, f) where m is confined to a class of admissible monos. Such a class together with the category of total maps constitute a domain structure.

Definition 3.1. (Rosolini 1986; Moggi 1986) A domain structure is a pair (K, D) consisting of a well-powered category D and a category K, such that D is a full-on-objects subcategory of K all of whose morphisms are monos in K, with the following closure property: every diagram ⟶^{f}↢^{n} with f ∈ K and n ∈ D has a pullback in K and whenever

f^{−1}(n)  f  n

then f^{−1}(n) ∈ D. □

Convention. K is called the category of total maps and D is called the category of admissible monos. For every A ∈ | D |, D(A) will denote the skeleton of the slice category D/A. As D is well-powered, | D(A) | is a small set and hence D(A) is a small poset.

Categories of admissible monos are closed under isomorphisms, for every isomorphism i appears in the pullback

id idi i  .

For monos m and n, we write [m] ⊆_{i} [n] (resp. m ⊆_{i} n) and say that i realises the inequality [m] ⊆ [n] (resp. m ⊆ n) whenever m = n ∘ i. Realisers of inequalities between admissible subobjects are admissible, for consider the equivalence:

n i id  m ⟺ [m] ⊆_{i} [n]  .

Definition 3.2. The category of partial maps p(K, D) induced by a domain structure (K, D) has the same objects as K, a morphism is an equivalence class of descriptions in D × K, and composition and identities are given as detailed above. □ Convention. Whenever we write p(K, D) it is assumed that (K, D) is a domain structure; when D is clear from the context we simply write pK.

To distinguish total maps (i.e. morphisms in K) from partial maps (i.e. morphisms in pK) we denote the former with → and the latter with ⇀.

The category of total maps can be viewed as a full-on-objects subcategory of the category of partial maps by identifying K with its image under the faithful inclusion functor J : K → pK which acts as the identity on objects and sends a total map f to the partial map [id, f]. It should then be clear what is meant by a total partial map and by the composition of a total map with a partial map. To indicate that a partial map u is total we write u ↓. Totality and composition interact in the desirable way: for partial maps u and v, (v ∘ u) ↓ ⇒ u ↓. Definition 3.3. When the category of total maps has a terminal object 1, we say that totality is extensional if for all u : A ⇀ B, u ↓ ⟺ ∀ x : 1 → A. (u ∘ x) ↓. □

Every admissible mono m : D ↣ A induces a partial identity on A, viz. the partial map [m, m] : A ⇀ A. There is a partial inclusion functor ( )^{R} : D^{op} → pK which acts as the identity on objects and sends m : D ↣ A in D to m^{R} = [m, id] : A ⇀ D. Partial inclusions have nice equational properties, in particular

m^{R} = n^{R} ⟺ [m] = [n],
m^{R} ∘ m = id,  (5)
[m, f] = f ∘ m^{R}.  (6)

While (5) justifies the terminology, (6) shows that every partial map can be factored as a partial inclusion followed by a total map. In fact, as observed by John Power, this determines a factorisation system (Freyd and Kelly 1972). Partial inclusions also provide a simple equational characterisation for the pullbacks we are interested in, as

⟺ n m  g  n^{R} ∘ f = g ∘ m^{R}. f

The adopted description of partial maps allows the definition of the inverse image, u^{−1}[n], of an admissible subobject [n] ∈ D(B) along a partial map u = [m, f] : A ⇀ B, simply as the admissible subobject [m ∘ f^{−1}(n)] ∈ D(A). In fact, we have an inverse image functor D( ) : p(K, D)^{op} → Poset sending A ∈ | pK | to D(A) and u : A ⇀ B to u^{−1}( ) : D(B) → D(A). Its restriction to total maps, K^{op} → Poset, is the composite D( ) ∘ J^{op} : K^{op} → Poset. As a convention, for u : A ⇀ B and [m : D ↣ B] ∈ D we write u^{−1}(m) : u^{−1}(D) → A for any representative of u^{−1}[m] ∈ D(A). Notice that, for f : A → B, the convention agrees with the already adopted notation, f^{−1}(m), for any mono obtained by pulling back m along f. Also, extending the n^{∗}f notation of diagram (2) to partial maps, so that n^{∗}[m, f] = n^{∗}f, we have: Proposition 3.1. The commuting square

D Bm u A u^{−1}(m) u^{−1}(D) m^{∗}u

is a pullback for total maps. That is, for every A ⟵^{f} C ⟶^{g} D satisfying u ∘ f = m ∘ g there exists a unique h : C → u^{−1}(D) such that f = u^{−1}(m) ∘ h and g = (m^{∗}u) ∘ h. □

From the inverse image of a partial map we can obtain its domain of definition by setting, for every A, B ∈ | pK |,

dom_{A,B}( ) = ( )^{−1}[id_{A}] : pK(A, B) → D(A).

It follows then that a partial map is total if and only if its domain of definition is the maximal subobject.

3.2. Examples

Every well-powered category K appears in two domain structures: a minimal one, (K, Isos_{K}) where Isos_{K} is the category of all isomorphisms in K; and a maximal one, (K, Monos_{K}) where Monos_{K} is the category of all monomorphisms in K.

To obtain further examples, we show how to construct new domain structures from old ones. Let (K, D) be a domain structure. 1 Convention. For a category C and a set O ⊆ | C |, the full subcategory of C with set

of objects O is denoted as C ↾ O.

Let L be a full subcategory of K whose objects are closed under taking the source of admissible monos (i.e. for every A ∈ | L | and D ∈ | D |, if D ↣ A in D then D ∈ | L |). Then (L, D ↾ | L |) is a domain structure.

2 Convention. For a category C and a small category W, we write [W, C] for the category of functors W → C and natural transformations. Let W be a small category. Then, ([W, K], D-Nat_{[W,K]}) where D-Nat_{[W,K]} is the subcategory of [W, K] of all the pointwise-admissible natural transformations, and ([W, K], D-Cart_{[W,K]}) where D-Cart_{[W,K]} is the subcategory of [W, K] of all the pointwise-admissible cartesian natural transformations are domain structures. A more tangible example of domain structure is (Top, Open) where Top is the cat-

egory of topological spaces and continuous functions, and Open is its subcategory of all those monos m : (X, OX) ↣ (Y, OY) such that (m(X), P(mX) ∩ OY) is a topological space isomorphic to (X, OX). The construction (1) above applied to K = Top, D = Open, and L = Poset (resp. Cpo), viewed as the full subcategory of Top whose objects are posets (resp. cpos) with the Alexandrov (resp. Scott) topology, yields the domain structure (Poset,Open) (resp. (Cpo,Open), usually denoted (Cpo,Σ)).

Another domain structure on Top is (Top, Close) where Close consists of all those monos m : (D, OD) ↣ (A, OA) such that m(D) is closed in A and for every U ⊆ D, U is open in D if and only if m(U) is open in A. Applying the construction (1) as before we obtain the domain structures (Poset, Close) and (Cpo, Close).

Outside the scope of topological spaces we may consider the domain structure (Cpo_{∧}, Σ_{∧}) where Cpo_{∧} is the category of small cpos (posets) with bounded meets and stable functions (viz. continuous functions preserving bounded meets) and Σ_{∧} is its subcategory of all those order-reflecting monos m : D ↣ A such that m(D) is Scott-open and closed under bounded meets in A.

The categories of partial maps induced by some of our examples of domain structures are: p(K, Isos_{K}) ≅ K; p(Set, Monos) ≅ Pfn (the category of sets and partial functions); p(Poset, Open) ≅ pPoset; p(Cpo, Σ) ≅ pCpo; p(Cpo_{∧}, Σ_{∧}) ≅ pCpo_{∧} (the category of small cpos with bounded meets and partial functions defined on a Scott-open closed under bounded meets and such that their restriction to the domain of definition is stable); finally, p([W, K], D-Cart_{[W,K]}) ≅ [W, p(K, D)] ↾ | [W, K] | (see (Fiore 1994, Proposition 5.3.5)).

4. Testing and Observing Partial Maps

The capability of observing that an input/output program terminates serves as the basis for discriminating between programs. For example, in the contextual approach, a program e is said to approximate a program e′ (written e ⊏ ∼^{c} e′) if, in every program in which e occurs, e can be safely replaced by e′ in the sense that new non-terminating behaviour will not happen.

The distinction between partial and total maps induces an approximation relation between maps, in which contexts are used to discriminate between maps based on their terminating behaviour. Following the informal description of a context as a “program with a hole”; in a category of partial maps, a context is described as a “partial map with a hole”. Formally, contexts are incomplete composites w ∘ ∘ t where t and w are partial maps. The contextual approximation relation for partial maps is defined as follows, Definition 4.1. (Plotkin) For every u, v : A ⇀ B,

u ⊏ ∼^{c} v if and only if for every context C[ ], C[u] ↓ ⇒ C[v] ↓. □

Remark. Observe that because of the adopted description of partial maps it is enough to consider contexts of the form m^{R} ∘ ∘f for m an admissible mono and f a total map. But the definition is independent of the description of the category of partial maps, and thus, makes sense in any axiomatisation of such categories (e.g. the p-categories of (Robinson and Rosolini 1988)).

The restriction of ⊏ ∼^{c} to total maps gives a contextual approximation relation on total maps which we denote ⊑^{c}. Both ⊑^{c} and ⊏ ∼^{c} are preorders and, in general, they are not partial orders.

Justifying our computational intuition, in the examples of interest the contextual approximation relation turns out to be a partial order which, further, coincides with the usual notion of approximation. In Poset and Cpo, ⊑^{c} is the pointwise order ⊑; whilst in pPoset and pCpo, ⊏ ∼^{c} is the appropriate generalisation of the pointwise order, namely for u, v : P ⇀ Q,

u ⊏ ∼ v if and only if for every x ∈ P, u(x) ↓ ⇒ (v(x) ↓ ∧ u(x) ⊑ v(x)).  (7)

Instead of checking these facts, which follow from general considerations (see the remark after Proposition 4.2), we exemplify the use of contexts to discriminate maps. Let f, g : P → Q in Poset be such that there exists t ∈ P for which ft ⊏ gt, and let C[ ] be the context in pPoset, W^{R} ∘ ∘t, where t : 1 → P : ∗ ↦ t and W = Q\{y ∈ Q | y ⊑ ft}. Then, with respect to termination, C[ ] distinguishes f and g, as C[f] ↑ and C[g] ↓.

In pPoset (pCpo), (7) reduces the order on partial monotone (continuous) functions to the test for definedness and the order on elements. As the next proposition shows this is a general phenomenon and sustains a claim that testing for totality and the approximation of total maps are primitive concepts, whilst the approximation of partial maps is a derived one. Proposition 4.1. For every u, v : A ⇀ B,

u ⊏ ∼^{c} v if and only if for every x : X → A, u ∘ x ↓ ⇒ (v ∘ x ↓ ∧ u ∘ x ⊑^{c} v ∘ x). Moreover, when the category of total maps has terminal object 1 and totality is extensional (Definition 3.3) the above can be strengthened to

u ⊏ ∼^{c} v if and only if for every x : 1 → A, u ∘ x ↓ ⇒ (v ∘ x ↓ ∧ u ∘ x ⊑^{c} v ∘ x). □ Remark. In the proposition, it would make no difference to allow x to range over partial maps, as u ∘ x ↓ ⇒ x ↓. Moreover, this property is central to the (omitted) proof.

Further evidence for the suitability of contextual approximation is that it interacts well with composition (see Proposition 4.2 and 8.1).

The description of partial maps based on domain structures provides another computationally natural notion of approximation. For this purpose, admissible monos are regarded as predicates describing observable properties (c.f. (Smyth 1992)).

A program e is said to specialise a program e′ (written e ⊏ ∼^{s} e′) if the observable properties of the outputs of e are also satisfied by the outputs of e′. Put it in another way, for any observable property U, the weakest precondition ensuring that every execution of e satisfies U is a precondition ensuring that every execution of e′ satisfies U. Thus, an observer content with the input/output behaviour of e should also be content with the input/output behaviour of e′. The specialisation relation for partial maps is defined as follows: Definition 4.2. u ⊏ ∼^{s} v : A ⇀ B in pK if and only if u^{−1}( ) ⊆ v^{−1}( ) : D(B) → D(A) in Poset. □

The specialisation relation generalises the one from topology (see (Smyth 1992)). Recall that for a T_{0}-space (X, O(X)), its specialisation order ≤ ⊆ X × X is defined as

x ≤ y if and only if for every U ∈ O(X), x ∈ U ⇒ y ∈ U.

Then, by identifying elements with functions out of the singleton, the above definition can be put in a form resembling Definition 4.2:

x ≤ y if and only if for every U ∈ O(X), x^{−1}(U) ⊆ y^{−1}(U).

Pleasantly enough, the notions of approximation obtained by testing and by observing partial maps coincide.

Lemma 4.1. For f ∈ K(X, A), u ∈ pK(A, B) and m ∈ D(D, B),

m^{R} ∘ u ∘ f ↓ ⟺ f factors through u^{−1}(m).

Proof. (⇒) For every n ∈ D(E, Y) and g ∈ K(X, Y), n^{R} ∘ g ↓ ⇒ g = n ∘ n^{R} ∘ g. Thus, assuming m^{R} ∘ u ∘ f ↓ we have that u ∘ f = m ∘ (m^{R} ∘ u ∘ f), and since A ↢^{u^{−1}(m)} u^{−1}(D) ⟶^{m^{∗}u} D is a pullback of A ⇀^{u} B ↢^{m} D for total maps (see Proposition 3.1) we are done. (⇐) Assume f = u^{−1}(m) ∘ g. Then, g is total and so is

(m^{∗}u) ∘ g = m^{R} ∘ m ∘ (m^{∗}u) ∘ g = m^{R} ∘ u ∘ u^{−1}(m) ∘ g = m^{R} ∘ u ∘ f. □

Proposition 4.2. ⊏ ∼^{c} equals ⊏ ∼^{s} .

Proof. ( ⊏ ∼^{c} ⊆ ⊏ ∼^{s} ) Let u ⊏ ∼^{c} v : A ⇀ B. Then,

u ⊏ ∼^{c} v ⇒ ∀ [m] ∈ D(B).
(m^{R} ∘ u ∘ u^{−1}(m) ↓ ⇒ m^{R} ∘ v ∘ u^{−1}(m) ↓)
⟺ ∀ [m] ∈ D(B). m^{R} ∘ v ∘ u^{−1}(m) ↓

, as m^{R} ∘ u ∘ u^{−1}(m) = m^{∗}u ↓

⟺ ∀ [m] ∈ D(B). u^{−1}(m) factors through v^{−1}(m)

, by Lemma 4.1

⟺ u ⊏ ∼^{s} v.

( ⊏ ∼^{s} ⊆ ⊏ ∼^{c} ) Let u ⊏ ∼^{s} v : A ⇀ B. Then,

u ⊏ ∼^{s} v ⟺ ∀ [m] ∈ D(B). u^{−1}(m) ⊆ v^{−1}(m)
⟺ ∀ [m] ∈ D(B). u^{−1}(m) factors through v^{−1}(m)
⇒ ∀ f ∈ K(X, A). ∀ [m] ∈ D(B).
(f factors through u^{−1}(m) ⇒ f factors through v^{−1}(m))
⇒ ∀ f ∈ K(X, A). ∀ [m] ∈ D(B).
(m^{R} ∘ u ∘ f ↓ ⇒ m^{R} ∘ v ∘ f ↓)  , by Lemma 4.1
⟺ u ⊏ ∼^{c} v.

Remark. In Poset (resp. Cpo), the contextual approximation relation, the specialisation relation, and the pointwise order are equal, by Proposition 4.2 and the well-known fact that, for f, g : P → Q, f ⊑ g if and only if for every upper-closed (resp. Scott-open) U ⊆ Q, f^{−1}(U) ⊆ g^{−1}(U). Moreover, the equality extends to pPoset and pCpo, by Propositions 4.1 and 4.2.

The following table describes the specialisation preorder for various domain structures:

Domain Structure f ⊑^{s} g : P → Q
(K, Isos_{K})  for every f and g
(Set,Monos)  iff f = g (i.e. discrete)
(Poset,Close)  iff ∀ x ∈ P. f(x) ⊒ g(x)

(Cpo,Close)

Quite disapointingly the specialisation order induced by (Cpo_{∧}, Σ_{∧}) is not the stable order ⊑_{st} (where f ⊑_{st} g : P → Q if and only if ∀x, y ∈ P. x ⊑ y ⇒ f(x) = f(y)∧g(x)) which is the one making Cpo_{∧} into a Cpo-cartesian-closed-category. In fact, as the following proposition shows, in order to observe stability a more subtle way of comparing weakest preconditions (see (Zhang 1991, Theorem 8.2)) is needed: Proposition 4.3. The specialisation order induced by any domain structure (Cpo_{∧}, D) is not the stable order.

Proof. Let 2 = {⊥ ⊑ ⊤} be the Sierpinski space and write, respectively, K_{⊥} and K_{⊤} for the constantly ⊥ and ⊤ stable functions 2 → 2. Recall that the stable order on 2 → 2 is: id_{2} _{st}⊒ K_{⊥} ⊑_{st} K_{⊤}. If id_{2} ⋢^{s} K_{⊤} then there exists D ↣ 2 in D such that D = id_{2}^{−1}(D) ⊈ K_{⊤}^{−1}(D), so D = {⊥} and hence {⊥} ↣ 2 is in D. But then we have that K_{⊥} ⋢^{s} id_{2} because 2 = K_{⊥}^{−1}{⊥} ⊃ id_{2}^{−1}{⊥} = {⊥}. Hence, the result follows.

In general, specialisation is a preorder and not a partial order (e.g. consider the domain structures (K, Isos_{K}) and (Top,Open)), but in every domain structure it is possible to identify a sub-domain-structure in which the specialisation preorder is antisymmetric. To this end we introduce a T_{0}-axiom: Definition 4.3. Let (K, D) be a domain structure. We say that A ∈ | K | is a T_{0}-object if for all f, g : X → A, (∀ [m] ∈ D(A). f^{−1}[m] = g^{−1}[m]) ⇒ f = g. □

Admissible subobjects of T_{0}-objects are T_{0}: Proposition 4.4. Let (K, D) be a domain structure. If A′ ∈ | K | is T_{0} and n : A ↣ A′ is in D then A is T_{0}.

Proof. Let f, g : X → A and assume f^{−1}[m] = g^{−1}[m] for all [m] ∈ D(A). Then, for all [m′] ∈ D(A′),

(n ∘ f)^{−1}[m′] = f^{−1}[n ∩ m′] = g^{−1}[n ∩ m′] = (n ∘ g)^{−1}[m′]

and, as A′ is T_{0}, n ∘ f = n ∘ g; but then, as n is mono, f = g.

For a domain structure (K, D) let K_{0} be the full subcategory of K of all T_{0}-objects. Then, (K_{0}, D ↾ | K_{0} |) is a domain structure in which the specialisation preorder is a partial order that coincides with that of (K, D).

5. Ordering Partial Maps

Motivated by the discussion in Section 4, the approximation order between total maps is adopted as primitive and is used to derive a notion of approximation between partial maps.

From now on and till Section 8, we will consider an arbitrary approximation order, ⊑, on total maps (instead of just restricting attention to the specialisation preorder ⊑^{s}), and define and study an induced approximation order ⊏ ∼ on partial maps. This generality is mandatory if, for example, a stable order on pCpo_{∧} is to be analysed. Convention. For V = Poset or Cpo, a domain structure with a V-category of total maps is called a V-domain-structure and the order on total maps is denoted ⊑.

A Poset-domain-structure induces an order on partial maps whose definition is motivated by Proposition 4.1: Definition 5.1. Given a Poset-domain-structure, for every u, v : A ⇀ B,

u ⊏ ∼ v if and only if for every x : X → A, u ∘ x ↓ ⇒ (v ∘ x ↓ ∧ u ∘ x ⊑ v ∘ x). □ Remark. ⊏ ∼ is clearly reflexive and transitive. That it is antisymmetric follows from Proposition 5.1 below.

As an example consider the Poset-domain-structure (Cpo_{∧},Σ_{∧}) with the stable order ⊑_{st}, then u ⊏ ∼_{st} v : P ⇀ Q in pCpo_{∧} if and only if

∀ x ∈ P. u(x) ↓ ⇒ (v(x) ↓ ∧ ∀ y ∈ P. x ⊑ y ⇒ u(x) = u(y) ∧ v(x)).

The intuition behind Definition 5.1 is that a possibly non-terminating input/output program e approximates another one e′ provided that under all possible inputs, the outputs of e approximate the outputs of e′. Thus, in particular, whenever e outputs, so does e′. In symbols, dom(e) ⊆ dom(e′) ∧ e ↾ dom(e) ⊑ e′ ↾ dom(e). This intuition is technically correct:

Proposition 5.1. Given a Poset-domain-structure, for every [m, f], [n, g] : A ⇀ B,

[m, f] ⊏ ∼ [n, g] ⟺ m ⊆_{i} n ∧ f ⊑ g ∘ i for some (unique) i.

(In diagram form:

A  B n  g D E f m  ⊒ i  .)

Proof. (⇒) Assume [m, f] ⊏ ∼ [n, g]. Since [m, f]∘m = f is total then so is [n, g]∘m and therefore there exists a unique i for which

i id  n m  and f = [m, f] ∘ m ⊑ [n, g] ∘ m = g ∘ i.

(⇐) Let m ⊆_{i} n and f ⊑ g ∘ i for some i. For x : X → A, if [m, f] ∘ x ↓ then

[id] = dom([m, f] ∘ x) = x^{−1}[m] ⊆ x^{−1}[n] = dom([n, g] ∘ x)

and therefore [n, g] ∘ x ↓. Moreover, we have

m^{∗}x id  n n^{∗}x  ⊒ f id  i g x

and hence, [m, f] ∘ x = f ∘ (m^{∗}x) ⊑ g ∘ i ∘ (m^{∗}x) = [n, g] ∘ x. Convention. We introduce the notation [m, f] ⊏ ∼_{i} [n, g] to indicate that i realises the inequality between the representatives (i.e. m ⊆_{i} n and f ⊑ g∘i). Clearly, if [m, f] ⊏ ∼ [n, g] and m ⊆_{i} n then [m, f] ⊏ ∼_{i} [n, g].

An example of the order induced by a Poset-domain-structure is a generalisation of the graph inclusion order; denoted ⊆, and defined to be the order induced by (K_{Poset}, D) where (K, D) is a domain structure and K_{Poset} is the Poset-category obtained from K by discretely ordering each hom-set. Explicitly,

[m, f] ⊆_{i} [n, g] if and only if m ⊆_{i} n and f = g ∘ i.

Justifying the terminology, when (K, D) = (Set, Monos),

u ⊆ v if and only if graph(u) ⊆ graph(v).

The characterisation of ⊏ ∼ , provided by Proposition 5.1, is more convenient to work with than its definition; for example, using the characterisation the following is straightforward: Proposition 5.2. Let (K, D) be a Poset-domain-structure. Then, for A, B ∈ | K |, 1 (pK(A, B), ⊏ ∼ ) is a poset. 2 J_{A,B} : (K(A, B), ⊑) ↪ (pK(A, B), ⊏ ∼ ) is a full functor. 3 K(A, B) is upper-closed in (pK(A, B), ⊏ ∼ ), i.e. for every f : A → B and u : A ⇀ B,

if f ⊏ ∼ u then u ↓. 4 J_{A,B} preserves lubs. 5 dom_{A,B} : (pK(A, B), ⊏ ∼ ) → (D(A), ⊆) is monotone. □ Remark. From (2) and (3) above, it follows that J_{A,B} is a full and upper-closed morphism in Poset, in the sense that for every f : A → B and u : A ⇀ B, if Jf ⊏ ∼ u then there exists a unique g : A → B such that f ⊑ g and Jg = u. This property together with monotonicity imply (4).

Full and upper-closed morphisms play a central role in the next section.

6. Poset-Categories of Partial Maps

Now our main goal is to understand when ⊏ ∼ is domain theoretic, in the technical sense that the category of partial maps Cpo-enriches with respect to it. For simplicity we undertake this study in two steps: in this section, we characterise Poset-categories of partial maps induced by domain structures with a Poset-category of total maps; in Section 7, we restrict our attention to uniform domain structures (Definition 7.2) with a Cpo-category of total maps, and provide necessary and sufficient conditions so that the induced category of partial maps Cpo-enriches. As an example, in Section 8, these characterisations are used when the approximation order is specialisation.

We have seen that the category of partial maps induced by a Poset-domain-structure has hom-posets with respect to the induced order (Proposition 5.2 (1)). Thus, it would be Poset-enriched if composition (or equivalently, composition on the right and composition on the left) was monotone.

Checking for monotonicity, and also continuity (as will be seen in the next section), of composition on the right is easier than for composition on the left due to the asymmetry in the diagram

⊒  (8)

expressing the inequality between two partial maps. But when the order on partial maps is the graph inclusion order, the situation in (8) is symmetric (as both triangles commute) and potentially more manageable.

Monotonicity of composition on the right is immediate:

Lemma 6.1. For a Poset-domain-structure, pK( , A) is a functor pK^{op} → Poset for every A ∈ | pK |.

Proof. Let [m, f] : X ⇀ Y. Assume [n′, g′] ⊏ ∼_{i} [n, g] : Y ⇀ A, then the diagram

g i f m  n n′  g′ ⊒ j

states that j realises the inequality [n′, g′] ∘ [m, f] ⊏ ∼ [n, g] ∘ [m, f].

Aiming at characterising monotonicity of composition on the left, some domain theoretic concepts in the context of Poset-categories, due to Barry Jay, are introduced. Definition 6.1. (Jay) In a Poset-category C, a morphism m : A → B is said to be 1 full if for every C ∈ | C |, the monotone map m ∘ : C(C, A) → C(C, B) is full as a

functor (i.e. m ∘ x ≤ m ∘ y ⇒ x ≤ y). 2 upper-closed if for every x : C → A and y : C → B, whenever m ∘ x ≤ y there exists

a z : C → A such that m ∘ z = y. □ In Poset (Cpo), a morphism m : P → Q is full if and only if establishes an iso-

morphism between P and m(P) ordered as in Q. Further, if f : P → Q is upper-closed then f(P) is an upper-closed subset of Q. The converse need not hold, but whenever m : P → Q is full and such that m(P) is an upper-closed subset of Q then m is an upper-closed morphism. Therefore, the full and upper-closed subobjects of a poset (cpo) are exactly its upper-closed subsets with the induced order.

Full and upper-closed morphisms can be characterised along the lines of the remark after Proposition 5.2: Proposition 6.1. In a Poset-category, a morphism m : A → B is full and upper-closed if and only if it is a mono and for every x : C → A and y : C → B, if m ∘ x ≤ y then there exists a (necessarily) unique z : C → A such that x ≤ z and m ∘ z = y. □

In pPoset every admissible mono is full and upper-closed. This is not accidental: Theorem 6.1. Given a Poset-domain-structure (K, D), the following are equivalent 1 p(K, D) Poset-enriches with respect to ⊏ ∼ . 2 for every A ∈ | pK |, pK(A, ) is a functor pK → Poset. 3 For every A ∈ | K | and m : D ↣ B in D, the map m^{R} ∘ : K(A, B) → pK(A, D) is

monotone. 4 Every admissible mono is full and upper-closed.

Proof.

(1) ⇒ (2) Vacuously.

(2) ⇒ (1) By Lemma 6.1.

(2) ⇒ (3) Obvious.

(3) ⇒ (4) Let m ∈ D, and assume that m ∘ x ⊑ y. Then, x = m^{R} ∘ m ∘ x ⊏ ∼ m^{R} ∘ y. In diagram form,

y  m i m^{∗}y x id  ⊒ y^{−1}(m)

for some i. Therefore, x ⊑ (m^{∗}y) ∘ i and m ∘ (m^{∗}y) ∘ i = y.

(4) ⇒ (2) Let [n, g] : X ⇀ Y. Assume [m′, f′] ⊏ ∼_{i} [m, f] : A ⇀ X, then

n ∘ (n^{∗}f′) = f′ ∘ f^{′−1}(n) ⊑ f ∘ i ∘ f^{′−1}(n).

Since n is full and upper-closed, it follows that there exists a unique z such that

z  n^{∗}f′ n f if^{′−1}(n)  ⊒  .

Then, by the universal property of pullbacks, there exists a unique j such that

n f if^{′−1}(n)  z j n^{∗}f f^{−1}(n)  .

And finally, it follows that j realises the inequality [n, g] ∘ [m′, f′] ⊏ ∼ [n, g] ∘ [m, f]. Corollary 6.1. For every domain structure (K, D), p(K_{Poset}, D) Poset-enriches with respect to ⊆. □

As a consequence of the theorem we have that the categories of partial maps induced by (Poset,Open) and (Cpo,Σ) with the pointwise order, ⊑, Poset-enrich with respect to ⊏ ∼ . Also, the category of partial maps induced by (Cpo_{∧},Σ_{∧}) with the stable order, ⊑_{st}, Poset-enriches with respect to ⊏ ∼_{st} . Clearly, the category of partial maps induced by (Poset,Close) and (Cpo,Close) with the pointwise order do not Poset-enrich.

7. Cpo-Categories of Partial Maps

Convention. Whenever we say that a category of partial maps is Cpo-enriched we assume that so is the domain structure that induces it and that the order is ⊏ ∼ .

We start the investigation on Cpo-categories of partial maps focusing on the properties enforced by the enrichment. In this respect, two important points are: the fact that the class of admissible subobjects of a Cpo-domain-structure inducing a Cpo-category of partial maps ought to be locally a cpo (i.e. the skeleton of every slice is a cpo), and a trick which reduces lubs of arbitrary partial maps to lubs of graph included partial maps (Subsection 7.1). Afterwards, with the purpose of obtaining lubs of admissible subobjects and lubs of partial maps in a canonical way, uniform domain structures are introduced and their properties studied (Subsection 7.2). This, together with the characterisation of Poset-categories of partial maps, will provide a characterisation of Cpo-categories of partial maps induced by uniform Cpo-domain-structures. Finally, as an application, a recipe for computing lubs of ω-chains of partial maps in these categories is given (Subsection 7.4).

7.1. Properties of Cpo-Categories of Partial Maps

Convention. We regard lubs (of subobjects and partial maps) as colimits. Thus we sometimes write ⨆ ⟨[m_{k}] ⊆ [m_{k+1}]⟩ = ⟨[m_{k}] ⊆ [m]⟩ to mean that ⟨[m_{k}] ⊆ [m_{k+1}]⟩ is an ω-chain with lub [m]. (An analogous notation is used for partial maps.)

Proposition 7.1. For a Poset-domain-structure (K, D), if p(K, D) has hom-cpos with respect to ⊏ ∼ then D is locally a cpo.

Proof. If ⟨[m_{k}] ⊆ [m_{k+1}]⟩ is an ω-chain in D(A) then ⟨[m_{k}, m_{k}] ⊆ [m_{k+1}, m_{k+1}]⟩ is an ω-chain in pK(A, A). And, if ⨆ [m_{k}, m_{k}] = [m, f], it follows that ⨆ [m_{k}] = [m].

The local completeness of the class of admissible subobjects has interesting consequences:

Proposition 7.2. In a domain structure (K, D), if D is locally a cpo then 1 If ⟨[m_{k}] ⊆_{i_{k}} [m_{k+1}]⟩ is an ω-chain in D(A) with lub ⟨[m_{k}] ⊆_{μ_{k}} [m : D ↣ A]⟩ then

⟨[μ_{k}] ⊆_{i_{k}} [μ_{k+1}]⟩ is an ω-chain in D(D) with lub [id_{D}]. 2 For every n : D ↣ A in D, the mapping [n ∘ ] : D(D) → D(A) is continuous. 3 dom preserves lubs of ω-chains.

Proof.

(1) Clearly ⟨[μ_{k}] ⊆_{i_{k}} [μ_{k+1}]⟩ is an ω-chain in D(D), and ⨆ [μ_{k}] = [id_{D}] because for every [n] ∈ D(D),

∀ k ∈ | ω |. μ_{k} ⊆ n ⟺ ∀ k ∈ | ω |. m_{k} = m ∘ μ_{k} ⊆ m ∘ n
⟺ m ⊆ m ∘ n
⟺ [n] = [id_{D}].

(2) First, observe that for every [m] ∈ D(D) and [n′] ∈ D(A),

n ∘ m ⊆ n′ ⟺ m ⊆ n^{−1}(n′).  (9)

Now, let ⟨[m_{k}] ⊆ [m_{k+1}]⟩ be an ω-chain in D(D) with lub [m]. Then, for every [n′] ∈ D(A),

∀ k ∈ | ω |. n ∘ m_{k} ⊆ n′ ⟺ ∀ k ∈ | ω |. m_{k} ⊆ n^{−1}(n′) , by (9)
⟺ m ⊆ n^{−1}(n′)
⟺ n ∘ m ⊆ n′  , by (9).

(3) Let ⟨[m_{k}, f_{k}] ⊏ ∼ [m_{k+1}, f_{k+1}]⟩ be an ω-chain. If ⨆ [m_{k}, f_{k}] = ⟨[m_{k}, f_{k}] ⊏ ∼ _{μ′_{k}}[m′, f]⟩ and ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ then we are required to prove that [m] = [m′]. [m′] is an upper bound of the ω-chain ⟨[m_{k}] ⊆ [m_{k+1}]⟩ and then [m] ⊆_{i} [m′]. For every k ∈ | ω |, since [m_{k}] ⊆_{μ_{k}} [m] ⊆_{i} [m′] and [m_{k}] ⊆_{μ′_{k}} [m′], it follows that μ′_{k} = i ∘ μ_{k}. Therefore [m, f ∘ i] is an upper bound of the ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼ [m_{k+1}, f_{k+1}]⟩, and then, [m′] ⊆ [m].

Convention. Let ⟨i_{k} : D_{k} → D_{k+1}⟩ be an ω-chain, then 1 we write ⟨m_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.} A to indicate that ⟨m_{k} : D_{k} → A⟩ is a cone for ⟨i_{k}⟩ (i.e. for

all k ∈ | ω |, m_{k} = m_{k+1} ∘ i_{k}); 2 we write ⟨f_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.}_{≤}B to indicate that ⟨f_{k} : D_{k} → B⟩ is a lax cone for ⟨i_{k}⟩ (i.e.

for all k ∈ | ω |, f_{k} ⊑ f_{k+1} ∘ i_{k}); and, 3 for cones ⟨μ_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.} D and ⟨m_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.} A, we write m : ⟨μ_{k}⟩ → ⟨m_{k}⟩ to indicate

that m : D → A is a morphism of cones (i.e. for all k ∈ | ω |, m ∘ μ_{k} = m_{k}).

We now analyse ω-chains of partial maps and their lubs. Let ⟨[m_{k}, f_{k}] ⊏ ∼_{i_{k}} [m_{k+1}, f_{k+1}]⟩ be an ω-chain in pK(A, B). Then we have that ⟨i_{k}⟩ is an ω-chain in D, ⟨m_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.} A, and ⟨f_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.}_{≤}B. In diagram form,

D_{k} D_{k+1} i_{k}  f_{k+1} B ⊑  (k ∈ | ω |) f_{k} A  D_{k} D_{k+1} m_{k} m_{k+1}  i_{k}  (k ∈ | ω |) .

The Cpo-enrichment of K allows us to replace lax cones by cones. Definition 7.1. Let ⟨i_{k} : D_{k} → D_{k+1}⟩ be an ω-chain. Given a lax cone ⟨f_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.}_{≤}B, for k ∈ | ω | we define f_{k}^{#} : D_{k} → B as ⨆_{l≥k} f_{l} ∘ i_{k,l} where we write i_{k,l} for the composite i_{l−1} ∘ … ∘ i_{k}. □ Proposition 7.3. Let ⟨i_{k}⟩ be an ω-chain. Every lax cone ⟨f_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.}_{≤} B induces a cone ⟨f_{k}^{#}⟩ : ⟨i_{k}⟩ \underrightarrow{.} B.

Proof. For k ∈ | ω |,

\begin{aligned}f_{k}^{#} & = & ⨆_{l≥k+1} f_{l} ∘ i_{k,l} & = & ⨆_{l≥k+1}(f_{l} ∘ i_{k+1,l} ∘ i_{k}) \\ & = & (⨆_{l≥k+1} f_{l} ∘ i_{k+1,l}) ∘ i_{k} & = & f_{k+1}^{#} ∘ i_{k}. \end{aligned}

Intuitively, f_{k}^{#} improves f_{k} by taking into account the information of the f_{l}’s, for l ≥ k, restricted to D_{k}. But, technically, f_{k}^{#} may not be f restricted to D_{k}, as f_{k}^{#} ⊑ f ∘ μ_{k} (see Proposition 7.4 (1)) but the equality need not hold (see Subsection 7.2, where this oddity is removed by imposing a uniformity condition on the domain structure).

We have thus seen that every ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼_{i_{k}} [m_{k+1}, f_{k+1}]⟩ induces the graph included ω-chain ⟨[m_{k}, f_{k}^{#}] ⊆_{i_{k}} [m_{k+1}, f_{k+1}^{#}]⟩. As we show below, both chains have the same lub and hence the calculation of lubs of arbitrary chains of partial maps can be reduced to the calculation of lubs of chains of graph included partial maps. Proposition 7.4. 1 ⨆ [m_{k}, f_{k}] exists if and only if so does ⨆ [m_{k}, f_{k}^{#}] and they are equal.

2 For [n, g] : X ⇀ A, ⨆ ([m_{k}, f_{k}]∘[n, g]) exists if and only if so does ⨆ ([m_{k}, f_{k}^{#}]∘[n, g]) and they are equal. Proof.

(1) Observe that for every k ∈ | ω |,

[m_{l}, f_{l}] ⊏ ∼_{μ_{l}} [m, f] for every l ≥ k ⇒ [m_{k}, f_{k}^{#}] ⊏ ∼_{μ_{k}} [m, f]  (10)

because assuming the antecedent, f_{l} ⊑ f ∘ μ_{l} and then, f_{l} ∘ i_{k,l} ⊑ f ∘ μ_{l} ∘ i_{k,l} = f ∘ μ_{k} for l ≥ k, yielding f_{k}^{#} ⊑ f ∘ μ_{k}. Then, by (10) and the fact that for every k ∈ | ω |, [m_{k}, f_{k}] ⊏ ∼_{id} [m_{k}, f_{k}^{#}] it follows that

[m_{k}, f_{k}] ⊏ ∼_{μ_{k}} [m, f] for all k ∈ | ω | ⟺ [m_{k}, f_{k}^{#}] ⊏ ∼_{μ_{k}} [m, f] for all k ∈ | ω |

and we are done.

(2) By Proposition 7.4 (1), ⨆ ([m_{k}, f_{k}] ∘ [n, g]) = ⨆ [n ∘ g^{−1}(m_{k}), f_{k} ∘ (m_{k}^{∗}g)] exists if and only if so does ⨆ [n ∘ g^{−1}(m_{k}), (f_{k} ∘ (m_{k}^{∗}g))^{#}] and they are equal. Thus, to conclude the proof it is enough to show that (f_{k} ∘ (m_{k}^{∗}g))^{#} = f_{k}^{#} ∘ (m_{k}^{∗}g) because then [n ∘ g^{−1}(m_{k}), (f_{k} ∘ (m_{k}^{∗}g))^{#}] = [n ∘ g^{−1}(m_{k}), f_{k}^{#} ∘ (m_{k}^{∗}g)] = [n, g] ∘ [m_{k}, f_{k}^{#}]. Let [n ∘ g^{−1}(m_{k}), f_{k} ∘ (m_{k}^{∗}g)] ⊏ ∼_{j_{k}} [n ∘ g^{−1}(m_{k+1}), f_{k+1} ∘ (m_{k+1}^{∗}g)] as indicated in the following diagram

n  j_{k} g  f_{k+1} m_{k+1} m_{k+1}^{∗}g  f_{k} m_{k}^{∗}g ⊒ i_{k} m_{k}  .  (11)

From (11), by induction, it follows that (m_{l}^{∗}g) ∘ j_{k,l} = i_{k,l} ∘ (m_{k}^{∗}g) for every l ≥ k and hence (f_{k} ∘(m_{k}^{∗}g))^{#} = ⨆_{l≥k} f_{l} ∘(m_{l}^{∗}g)∘j_{k,l} = ⨆_{l≥k} f_{l} ∘i_{k,l} ∘(m_{k}^{∗}g) = f_{k}^{#} ∘(m_{k}^{∗}g).

As mentioned at the beginning of Section 6, checking for continuity of composition on the left is more difficult than checking for continuity of composition on the right. This is reflected in the fact that the technique used to prove Proposition 7.4 does not extend to prove that ⨆ ([n, g] ∘ [m_{k}, f_{k}]) = ⨆ ([n, g] ∘ [m_{k}, f_{k}^{#}]) for every [n, g] : B ⇀ Y. For instance, a straight reduction of this equality to Proposition 7.4 (1) —as done for proving Proposition 7.4 (2)— is not possible because, for a start, there is no reason for which dom([n, g] ∘ [m_{k}, f_{k}]) = [m_{k} ∘ f_{k}^{−1}(n)] equals dom([n, g] ∘ [m_{k}, f_{k}^{#}]) = [m_{k} ∘ f_{k}^{#}^{−1}(n)].

7.2. Uniform Domain Structures

There are Cpo-categories of partial maps in which lubs do not behave as expected, the worst case being that the lub of an ω-chain of partial identities need not be a partial identity (i.e. for every A ∈ | K |, the partial identity mapping [ , ] : D(A) → pK(A, A) need not be continuous). For an example, consider the Cpo-category K pictured as

0  ⋯ k 1  1 0  ⋯  k ω⊥ ⋯  ⋯  (k ∈ | ω |)

where ⊥ ⊏ ω, and hence forced to be idempotent. Then Monos_{K} = K \ {⊥} and p(K, Monos) Cpo-enriches. The only infinite chain is ⟨[k, k] ⊆ [k + 1, k + 1]⟩ in pK(ω, ω) and, contradicting all expectations, ⨆ [k, k] = [ω, ⊥] ⊏ [ω, ω].

The problem is that for an ω-chain ⟨[m_{k}] ⊆_{i_{k}:D_{k}↣D_{k+1}} [m_{k+1}]⟩ in D(A) with lub ⟨[m_{k}] ⊆_{μ_{k}:D_{k}↣D} [m]⟩ the universal property of lubs is not enough to capture the intuition that D = ⋃ D_{k}. Pursuing this intuition, given an | ω |-indexed family ⟨f_{k} : D_{k} → B⟩ such that f_{k+1} extends f_{k} (i.e. f_{k} = f_{k+1} ↾ D_{k}) there ought to be a unique uniform extension f : D → B of the f_{k}’s (i.e. f_{k} = f ↾ D_{k}).

In categorical terms, we are asking for the following property to hold If ⨆ ⟨[m_{k}] ⊆_{i_{k}} [m_{k+1}]⟩ = ⟨[m_{k}] ⊆_{μ_{k}:D_{k}↣D} [m]⟩ then ⟨μ_{k}⟩ : ⟨i_{k}⟩ \underrightarrow{.} D is colimiting in K.

(12)

A colimit as in (12) can be used to obtain lubs of ω-chains of admissible subobjects:

Lemma 7.1. Let ⟨[m_{k}] ⊆_{i_{k}} [m_{k+1}]⟩ be an ω-chain in D(A), and let ⟨μ_{k}⟩ be a colimit in K for ⟨i_{k}⟩. If the unique mediating morphism m : ⟨μ_{k}⟩ → ⟨m_{k}⟩ is admissible, then ⨆ [m_{k}] = [m].

Proof. ⟨μ_{k}⟩ : ⟨m_{k}, i_{k}⟩ \underrightarrow{.} m is colimiting in D/A because the forgetful functor U_{A} : D/A → K reflects colimits.

When (12) holds for all ω-chains of admissible subobjects, the domain structure is said to be uniform.

Definition 7.2. A domain structure (K, D) is said to be uniform if the forgetful functor U : Σ_{A∈| D |}D/A → K preserves colimits of ω-chains. □

The following should help in understanding uniformity:

Lemma 7.2. The domain structure (K, D) is uniform and D is locally a cpo if and only if p(K_{Poset}, D) has hom-cpos.

Proof. (⇒) ⨆ ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩ = [m, f] where ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ and f : ⟨μ_{k}⟩ → ⟨F_{k}⟩. (⇐) By Proposition 7.1, D is locally a cpo. Let ⟨[m_{k}] ⊆ [m_{k+1}]⟩ be an ω-chain in D(A) with lub ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩, and let ⟨F_{k}⟩ : ⟨μ_{k}⟩ \underrightarrow{.} B in K. Then the ω-chain ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩ in pK(A, B) has lub ⟨[m_{k}, F_{k}] ⊆_{μ_{k}} [m, f]⟩ for some f (because if ⨆ [m_{k}, F_{k}] = [n, g] then [m] = ⨆ [m_{k}] = [n]). Clearly f : ⟨μ_{k}⟩ → ⟨F_{k}⟩. To see that it is the unique such, let g : ⟨μ_{k}⟩ → ⟨F_{k}⟩ then for every k ∈ | ω |, [m_{k}, F_{k}] ⊆ [m, g] and therefore [m, f] ⊆ [m, g]. Thus, f = g.

It follows from the lemma that (Set, Monos), (Poset, Open), (Cpo, Σ), and (Cpo_{∧}, Σ_{∧}) are uniform. A non-example was given at the beginning of the subsection.

The next proposition exhibits the appropriateness of uniformity by showing that, for uniform domain structures, the partial identity mapping is continuous. Various other consequences are also presented. Proposition 7.5. Let (K, D) be a uniform Poset-domain-structure. If pK has hom-cpos w.r.t. ⊏ ∼ , then for every A ∈ | K |, the partial identity mapping [ , ] : D(A) → pK(A, A) is continuous.

Proof. Monotonicity is clear. For preservation of lubs, let ⟨[m_{k}] ⊆ [m_{k+1}]⟩ be an ω-chain in D(A). Assume that ⨆ [m_{k}, m_{k}] = ⟨[m_{k}, m_{k}] ⊏ ∼ _{μ_{k}}[m, f]⟩. Then, by Proposition 7.1, ⨆ [m_{k}] = [m] and therefore we just need to check that f = m. Since, [m, m] is an upper bound of the ω-chain ⟨[m_{k}, m_{k}] ⊆ [m_{k+1}, m_{k+1}]⟩ it follows that [m, f] ⊏ ∼ [m, m] and therefore f ⊑ m. Thus, f ∘μ_{k} ⊑ m∘μ_{k} and since m∘μ_{k} = m_{k} ⊑ f ∘μ_{k}, invoking uniformity the proof is finished. Proposition 7.6. Let (K, D) be a uniform Cpo-domain-structure. If pK Cpo-enriches, then 1 D( ) is a Cpo-functor K^{op} → Cpo. 2 If ⟨[m_{k}] ⊆ [m_{k+1}]⟩ is an ω-chain in D(A) with lub [m], then for every f, g : A → B,

f ∘ m_{k} ⊑ g ∘ m_{k} for every k ∈ | ω | if and only if f ∘ m ⊑ g ∘ m.

3 ⊆ is a subcpo of ⊏ ∼ .

Proof.

(1) By Proposition 7.1, D is locally a cpo. And D( )( ) is a composition of continuous maps, namely, dom([ , ] ∘ ).

(2) (⇒) For every k ∈ | ω |, f ∘ m_{k} ⊑ g ∘ m_{k} implies f ∘ [m_{k}, m_{k}] ⊏ ∼ g ∘ [m_{k}, m_{k}]. Then f ∘[m, m] = ⨆ f ∘[m_{k}, m_{k}] ⊏ ∼ ⨆ g ∘[m_{k}, m_{k}] = g ∘[m, m] and therefore f ∘m ⊑ g ∘m.

(⇐) For every k ∈ | ω |, let [m_{k}] ⊆_{μ_{k}} [m]. Then,

f ∘ m_{k} = f ∘ m ∘ μ_{k} ⊑ g ∘ m ∘ μ_{k} = g ∘ m_{k}.

(3) For every A, B ∈ | pK |, by Propositions 7.1 and 7.2, (pK(A, B), ⊆) is a cpo. As ⊆ is a subposet of ⊏ ∼ , we only need to show that for every ω-chain ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩ with lub ⟨[m_{k}, F_{k}] ⊆_{μ_{k}} [m, f]⟩ in (pK(A, B), ⊆)

[m_{k}, F_{k}] ⊏ ∼ _{ν_{k}}[n, g] for every k ∈ | ω | ⇒ [m, f] ⊏ ∼ [n, g].

Assuming the antecedent, for every k ∈ | ω |, [m_{k}] ⊆_{ν_{k}} [n] and, because ⨆ [m_{k}] = [m], we have that [m] ⊆_{i} [n]. Finally, to show that f ⊑ g ∘ i observe that [m_{k}] ⊆_{ν_{k}} [n] and [m_{k}] ⊆_{μ_{k}} [m] ⊆_{i} [n] imply ν_{k} = i ∘ μ_{k}. Then, f ∘ μ_{k} = F_{k} ⊑ g ∘ ν_{k} = g ∘ i ∘ μ_{k} and since, by Proposition 7.2 (1), ⨆ [μ_{k}] = [id], using Proposition 7.6 (2) we are done.

7.3. Characterisation of Cpo-Categories of Partial Maps induced by Uniform Domain Structures

Theorem 7.1. Let (K, D) be a uniform Cpo-domain-structure. Then,

p(K, D) Cpo-enriches with respect to ⊏ ∼ if and only if

1 p(K, D) Poset-enriches with respect to ⊏ ∼ (see Theorem 6.1),

2 D( ) is a Cpo-functor K^{op} → Cpo, and

3 the colimits of ω-chains preserved by the forgetful functor U : Σ_{A∈| D |}D/A → K

are Poset-colimits. □ That the three conditions above are necessary follows from Propositions 7.6 (1), 7.6 (2),

7.2 (1) and 2.1. We show that they are sufficient in a series of steps.

Remark. The idea behind the proof is simple though one has to go through a series of long calculations.

(i) For showing that every hom-poset is a cpo, by Proposition 7.4 (1), we reduce the general case to finding lubs of chains of graph inclusions. Intuitively, the lub of a chain of graph inclusions is the partial map with domain of definition the union of the domains of definition of the partial maps in the chain, and with total component the unique uniform extension of the total components of the partial maps in the chain. (Recall that such extensions exist by the uniformity of the domain structure.)

(ii) For showing that composition on the right is continuous, by Proposition 7.4 (2), the general case is reduced to the graph inclusion case which, in turn, is proved by calculating the relevant lub with the above recipe.

(iii) For showing that composition on the left is continuous the problem is broken down in more subcases. We show that composition on the left with total maps is continuous, and that composition on the left with partial inclusions is continuous for total maps. This allows us to reduce the general case to the graph inclusion case. Then, after proving that composition on the left is continuos for chains of graph inclusions the general case is proved.

Until the end of this subsection, let (K, D) be a uniform domain structure.

Hom-posets are cpos

Lemma 7.3. (The graph inclusion case) Let D be locally a cpo, and let K be Posetenriched. Assume that U maps colimits of ω-chains to Poset-colimits. For an ω-chain ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩,

⨆ [m_{k}, F_{k}] = ⟨[m_{k}, F_{k}] ⊏ ∼_{μ_{k}} [m, f]⟩ ⟺ ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ and f : ⟨μ_{k}⟩ → ⟨F_{k}⟩.

Proof. (⇒) ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ because dom preserves lubs of ω-chains —see Proposition 7.2 (3). Since U preserves colimits of ω-chains, it follows that ⟨μ_{k}⟩ is a colimiting cone. Let g : ⟨μ_{k}⟩ → ⟨F_{k}⟩, then [m, g] is an upper bound of the ω-chain ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩ and therefore f ⊑ g. Thus, f ∘ μ_{k} ⊑ g ∘ μ_{k} = F_{k}, and since F_{k} ⊑ f ∘ μ_{k}, it follows that f : ⟨μ_{k}⟩ → ⟨F_{k}⟩. (⇐) By construction, [m, f] is an upper-bound of ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩. It is also the least, for assuming that [m_{k}, F_{k}] ⊏ ∼_{ν_{k}} [n, g], it follows that [m_{k}] ⊆_{ν_{k}} [n], and therefore [m] ⊆_{i} [n]. Thus, ν_{k} = i ∘ μ_{k} and then for every k ∈ | ω |, f ∘ μ_{k} ⊑ g ∘ i ∘ μ_{k}. Finally, since ⟨μ_{k}⟩ is a Poset-colimit, we conclude that f ⊑ g ∘ i.

Proposition 7.7. (Hom-posets are cpos) Let D be locally a cpo, and let K be Cpoenriched. If U maps colimits of ω-chains to Poset-colimits, then every hom-poset in pK is a cpo.

Proof. Follows from Lemma 7.3 and Proposition 7.4 (1).

Composition on the right is continuous

Proposition 7.8. Let K be Cpo-enriched. Assume that U maps colimits of ω-chains to Poset-colimits, and that D( ) is a functor K^{op} → Cpo. Then, 1 (Composition on the right is continuous for ω-chains of graph inclusions)

for every ω-chain ⟨[m_{k}, F_{k}] ⊆ [m_{k+1}, F_{k+1}]⟩ in pK(B, C), and every [n, g] : A ⇀ B,

(⨆ [m_{k}, F_{k}]) ∘ [n, g] = ⨆ ([m_{k}, F_{k}] ∘ [n, g]).

2 (Composition on the right is continuous) for every A ∈ | pK |, pK( , A) is a functor pK^{op} → Cpo. Proof.

(1) Let ⨆ [m_{k}, F_{k}] = ⟨[m_{k}, F_{k}] ⊏ ∼_{μ_{k}} [m, f]⟩. By Lemma 7.3, ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ and f : ⟨μ_{k}⟩ → ⟨F_{k}⟩. By Corollary 6.1, ⟨[m_{k}, F_{k}] ∘ [n, g] ⊆ [m_{k+1}, F_{k+1}] ∘ [n, g]⟩ is an ω-chain. To prove

⨆ [n ∘ g^{−1}(m_{k}), F_{k} ∘ (m_{k}^{∗}g)] = [n ∘ g^{−1}(m), f ∘ (m^{∗}g)]

we will, again, use Lemma 7.3. First, ⨆ [n ∘ g^{−1}(m_{k})] = [n ∘ g^{−1}(m)] by Proposition 7.2 (2) and the continuity of D(g). Second, assume that n ∘ g^{−1}(m_{k}) ⊆_{ν_{k}} n ∘ g^{−1}(m). Since f : ⟨μ_{k}⟩ → ⟨F_{k}⟩, it follows that

m_{k}^{∗}g ν_{k}  μ_{k} f m^{∗}g  F_{k}

and therefore f ∘ (m^{∗}g) : ⟨ν_{k}⟩ → ⟨F_{k} ∘ (m_{k}^{∗}g)⟩.

(2) For every ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼ [m_{k+1}, f_{k+1}]⟩ in pK(C, A) and [n, g] : B ⇀ C, by Lemma 6.1, ⟨[m_{k}, f_{k}] ∘ [n, g] ⊏ ∼ [m_{k+1}, f_{k+1}] ∘ [n, g]⟩ is an ω-chain in pK(B, A). And, we have

(⨆ [m_{k}, f_{k}]) ∘ [n, g] = (⨆ [m_{k}, f_{k}^{#}]) ∘ [n, g] , by Proposition 7.4 (1)
= ⨆ ([m_{k}, f_{k}^{#}] ∘ [n, g]) , by Proposition 7.8 (1)
= ⨆ ([m_{k}, f_{k}] ∘ [n, g]) , by Proposition 7.4 (2).

7.3.1. Composition on the left is continuous

Proposition 7.9. Let D be locally a cpo, let K be Cpo-enriched, and let pK be Poset-enriched. Assume that U maps colimits of ω-chains to Poset-colimits. Then,

1 (Composition on the left with total maps is continuous) for every A ∈ | pK |, pK(A, ) is a functor K → Cpo.

2 (Composition on the left with partial inclusions is continuous for total maps) For A ∈ | K | and m ∈ D(D, B), if the mapping D( )[m] : K(A, B) → D(A) is continuous, then so is the mapping m^{R} ∘ : K(A, B) → pK(A, D).

3 (Reduction to the graph inclusion case) If D( ) is a Cpo-functor K^{op} → Cpo, then for every ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼_{i_{k}} [m_{k+1}, f_{k+1}]⟩ in pK(A, B) and [n, g] : B ⇀ C,

⨆ ([n, g] ∘ [m_{k}, f_{k}]) = ⨆ ([n, g] ∘ [m_{k}, f_{k}^{#}]).

Proof.

(1) Let ⟨[m_{k}, f_{k}] ⊏ ∼_{i_{k}} [m_{k+1}, f_{k+1}]⟩ be an ω-chain in pK(A, B). By Proposition 7.4 (1) and Lemma 7.3, we have that ⨆ [m_{k}, f_{k}] = [m, f] where ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ and f : ⟨μ_{k}⟩ → ⟨f_{k}^{#}⟩. Then, g ∘ f : ⟨μ_{k}⟩ → ⟨g ∘ f_{k}^{#}⟩ and since g ∘ f_{k}^{#} = (g ∘ f_{k})^{#}, by Proposition 7.4 (1) and Lemma 7.3, ⨆ [m_{k}, g ∘ f_{k}] = [m, g ∘ f].

(2) m^{R} ∘ is monotone because pK is Poset-enriched. For the preservation of lubs, if ⟨f_{k}⟩ is an ω-chain in K(A, B), writing f for ⨆ f_{k}, we must prove ⨆ [f_{k}^{−1}(m), m^{∗}f_{k}] = [f^{−1}(m), m^{∗}f]. The ω-chain ⟨[f_{k}^{−1}(m), m^{∗}f_{k}] ⊏ ∼ [f_{k+1}^{−1}(m), m^{∗}f_{k+1}]⟩ in pK(A, D) has [f^{−1}(m), m^{∗}f] as an upper bound because the composition of partial maps is monotone. To see that it is the least assume [f_{k}^{−1}(m), m^{∗}f_{k}] ⊏ ∼_{μ_{k}} [f^{−1}(m), m^{∗}f] and [f_{k}^{−1}(m), m^{∗}f_{k}] ⊏ ∼_{ν_{k}} [n, g]. First, [f_{k}^{−1}(m)] ⊆_{ν_{k}} [n] and therefore [f^{−1}(m)] ⊆_{i} [n], by the continuity of D( )[m]. Second, we will show that m^{∗}f ⊑ g ∘ i. The inequalities [f_{k}^{−1}(m)] ⊆_{μ_{k}} [f^{−1}(m)] ⊆_{i} [n] and [f_{k}^{−1}(m)] ⊆_{ν_{k}} [n], imply ν_{k} = i ∘ μ_{k}. So we have

f_{k}  m μ_{k}  g n  i ⊑  .

Thus, for every k ∈ | ω |, f_{k} ∘ n ∘ i ∘ μ_{k} ⊑ m ∘ g ∘ i ∘ μ_{k} and since ⟨μ_{k}⟩ is a Poset-colimit, we conclude that m ∘ g ∘ i is an upper bound of the ω-chain ⟨f_{k} ∘ n ∘ i⟩. On the other hand, ⨆ (f_{k} ∘ n ∘ i) = f ∘ n ∘ i = f ∘ f^{−1}(m) = m ∘ (m^{∗}f). Then, m ∘ (m^{∗}f) ⊑ m ∘ g ∘ i, and since m is full we are done.

(3) We proceed via two calculations: First,

⨆_{k≥0}(n^{R} ∘ [m_{k}, f_{k}^{#}]) = ⨆_{k≥0}(n^{R} ∘ (⨆_{l≥k} f_{l} ∘ i_{k,l}) ∘ m_{k}^{R})
= ⨆_{k≥0} ((⨆_{l≥k} n^{R} ∘ f_{l} ∘ i_{k,l}) ∘ m_{k}^{R}) , by Proposition 7.9 (2)
= ⨆_{k≥0} ⨆_{l≥k}(n^{R} ∘ f_{l} ∘ i_{k,l} ∘ m_{k}^{R})  , by Proposition 7.8 (2)
= ⨆_{k≥0}(n^{R} ∘ f_{k} ∘ m_{k}^{R})
= ⨆_{k≥0}(n^{R} ∘ [m_{k}, f_{k}]).

Second,

⨆ ([n, g] ∘ [m_{k}, f_{k}]) = ⨆ (g ∘ n^{R} ∘ [m_{k}, f_{k}])
= g ∘ ⨆ (n^{R} ∘ [m_{k}, f_{k}]) , by Proposition 7.9 (1)
= g ∘ ⨆ (n^{R} ∘ [m_{k}, f_{k}^{#}]) , by the previous calculation
= ⨆ (g ∘ n^{R} ∘ [m_{k}, f_{k}^{#}]) , by Proposition 7.9 (1)
= ⨆ ([n, g] ∘ [m_{k}, f_{k}^{#}]).

Proposition 7.10. (Composition on the left is continuous for ω-chains of graph inclusions) Let K be Cpo-enriched. Assume that U maps colimits of ω-chains to Poset-colimits, and that D( ) is a functor K^{op} → Cpo. Then, for every ω-chain ⟨[m_{k}, F_{k}] ⊆_{i_{k}} [m_{k+1}, F_{k+1}]⟩ in pK(A, B) and [n, g] : B ⇀ C,

⨆ ([n, g] ∘ [m_{k}, F_{k}]) = [n, g] ∘ ⨆ [m_{k}, F_{k}].

Proof. Let ⨆ [m_{k}, F_{k}] = ⟨[m_{k}, F_{k}] ⊏ ∼_{μ_{k}} [m, f]⟩. By Corollary 6.1, ⟨[n, g] ∘ [m_{k}, F_{k}] ⊆ [n, g] ∘ [m_{k+1}, F_{k+1}]⟩ is an ω-chain. To prove

⨆ [m_{k} ∘ F_{k}^{−1}(n), g ∘ (n^{∗}F_{k})] = [m ∘ f^{−1}(n), g ∘ (n^{∗}f)]

we will use Lemma 7.3. If [m_{k} ∘ F_{k}^{−1}(n)] ⊆_{j_{k}} [m_{k+1} ∘ F_{k+1}^{−1}(n)] then to show ⨆ [m_{k} ∘ F_{k}^{−1}(n)] = [m ∘ f^{−1}(n)], by Lemma 7.1, it is enough to find a colimiting cone for ⟨j_{k}⟩, say ⟨ν_{k}⟩, such that m ∘ f^{−1}(n) : ⟨ν_{k}⟩ → ⟨m_{k} ∘ F_{k}^{−1}(n)⟩. We have

j_{k}i_{k}  F_{k} m_{k+1} m_{k}  n n^{∗}F_{k+1} F_{k+1} n^{∗}F_{k} F_{k}^{−1}(n)  F_{k+1}^{−1}(n)

and so

F_{k+1}^{−1}(n) i_{k} j_{k}  . F_{k}^{−1}(n)

Moreover, by Lemma 7.3, f : ⟨μ_{k}⟩ → ⟨F_{k}⟩, and therefore for every k ∈ | ω | we have

f^{−1}(n) μ_{k} ν_{k}  f  n n^{∗}f n^{∗}F_{k} F_{k} F_{k}^{−1}(n)  (13)

for some unique ν_{k}. The complete picture is as follows

j_{k}i_{k} m_{k+1} F_{k+1}^{−1}(n) m f^{−1}(n) μ_{k} ν_{k}  μ_{k+1} ν_{k+1}  m_{k}  . F_{k}^{−1}(n)

Thus, ⟨ν_{k}⟩ is a cone for ⟨j_{k}⟩ and m ∘ f^{−1}(n) : ⟨ν_{k}⟩ → ⟨m_{k} ∘ F_{k}^{−1}(n)⟩. Finally, recall that by Lemma 7.3, ⨆ [m_{k}] = ⟨[m_{k}] ⊆_{μ_{k}} [m]⟩ and so, by Proposition 7.2 (1), ⨆ [μ_{k}] = [id]. Since, by construction, ν_{k} is obtained by pulling back μ_{k} along f^{−1}(n), and D(f^{−1}(n)) is continuous, it follows that ⨆ [ν_{k}] = [id]. Hence, since U preserves colimits of ω-chains, ⟨ν_{k}⟩ is a colimit for ⟨j_{k}⟩. To complete the proof, by Lemma 7.3, we need only check whether g ∘ (n^{∗}f) : ⟨ν_{k}⟩ → ⟨g ∘ (n^{∗}F_{k})⟩. This follows because (n^{∗}f) ∘ ν_{k} = n^{∗}F_{k} —see diagram (13). Proposition 7.11. (Composition on the left is continuous) Let K be Cpo-enriched and let pK be Poset-enriched. Assume that U maps colimits of ω-chains to Posetcolimits and that D( ) is a Cpo-functor K^{op} → Cpo. Then, for every A ∈ | pK |, pK(A, ) is a functor pK → Cpo.

Proof. Because for every ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼ [m_{k+1}, f_{k+1}]⟩ in pK(A, B), and every [n, g] : B ⇀ C, we have

[n, g] ∘ ⨆ [m_{k}, f_{k}] = [n, g] ∘ ⨆ [m_{k}, f_{k}^{#}] , by Proposition 7.4 (1)
= ⨆ ([n, g] ∘ [m_{k}, f_{k}^{#}]) , by Proposition 7.10
= ⨆ ([n, g] ∘ [m_{k}, f_{k}]) , by Proposition 7.9 (3).

7.4. Computing Lubs of ω-Chains of Partial Maps

A by-product of the characterisation provided by Theorem 7.1 is a recipe for computing lubs of ω-chains of partial maps in Cpo-categories of partial maps: Proposition 7.12. Let (K, D) be a uniform Cpo-domain-structure such that pK Cpo-enriches. For every ω-chain ⟨[m_{k}, f_{k}] ⊏ ∼_{i_{k}} [m_{k+1}, f_{k+1}]⟩,

⨆ [m_{k}, f_{k}] = ⟨[m_{k}, f_{k}] ⊏ ∼_{μ_{k}:D_{k}↣D} [m, f]⟩ if and only if

⟨μ_{k}⟩ : ⟨D_{k}, i_{k}⟩ \underrightarrow{.} D is colimiting in K, m : ⟨μ_{k}⟩ → ⟨m_{k}⟩ and f : ⟨μ_{k}⟩ → ⟨f_{k}^{#}⟩.

Proof. Follows from Proposition 7.4 (1) and Lemma 7.3.

8. Enrichment with respect to Specialisation

In this section the characterisation theorems of order-enriched categories of partial maps (Theorems 6.1 and 7.1) are applied when the order is specialisation. As will be seen, Poset-enrichment is immediate, whilst Cpo-enrichment requires that the operation of pulling back admissible monos along arbitrary maps be continuous. Proposition 8.1. Let (K, D) be a domain structure. Then, K and pK Preo-enrich with respect ⊑^{s} and ⊏ ∼^{s} respectively. Thus, if every object in K is T_{0} (Definition 4.3) then K and pK Poset-enrich with respect ⊑^{s} and ⊏ ∼^{s} respectively.

Proof. It is enough to see that pK Preo-enriches with respect to ⊏ ∼^{s} . This follows because ⊏ ∼^{s} is a preorder and, for t : X ⇀ A, u ⊏ ∼^{s} v : A ⇀ B and w : B ⇀ Y, we have that

u ⊏ ∼^{s} v ⟺ D(u) ⊆ D(v)
⇒ D(w ∘ u ∘ t) = D(t) ∘ D(u) ∘ D(w) ⊆ D(t) ∘ D(v) ∘ D(w)
⟺ w ∘ u ∘ t ⊏ ∼^{s} w ∘ v ∘ t.

Proposition 8.2. Let (K, D) be a uniform domain structure. If D is locally a cpo, K has hom-cpos with respect to ⊑^{s}, and for every A, B ∈ | K |, the mapping D( )( ) : K(A, B) × D(B) → D(A) is continuous, then K and pK Cpo-enrich with respect to ⊑^{s} and ⊏ ∼^{s} respectively.

Proof. By Proposition 8.1, K Poset-enriches. By hypothesis every hom in K is a cpo. Moreover, using the fact that D( ) : K(A, B) → Cpo(D(B), D(A)) is injective, we have that

— since for every m : D ↣ B in D, the mapping D( )[m] : K(A, B) → D(A) is continuous, then so is composition on the left in K; and,

— since, in addition, for every f : A → B, the mapping D(f) : D(B) → D(A) is continuous, it follows that so is composition on the right in K.

Therefore, K Cpo-enriches. By Proposition 8.1, pK Poset-enriches. Finally, for every ω-chain ⟨[m_{k}] ⊆ [m_{k+1}]⟩ for which [m_{k}] ⊆_{μ_{k}:D_{k}→D} ⨆ [m_{k}] we show that for f, f′ : D → B,

f ∘ μ_{k} ⊑^{s} f′ ∘ μ_{k} for every k ∈ | ω | ⇒ f ⊑^{s} f′.  (14)

Order-Enrichment for Categories of Partial Maps 33

This will establish item (3) of Theorem 7.1 and, by invoking this theorem, conclude the proof of the proposition. For [m] ∈ D(B), let D(f)[m] = [n] and let D(f′)[m] = [n′]. Assuming the antecedent of (14), it follows that D(μ_{k})[n] = D(f ∘ μ_{k})[m] ⊆ D(f′ ∘ μ_{k})[m] = D(μ_{k})[n′] and therefore [n ∘ n^{−1}(μ_{k})] = [μ_{k} ∘ μ_{k}^{−1}(n)] ⊆ [μ_{k} ∘ μ_{k}^{−1}(n′)] = [n′ ∘ n^{′−1}(μ_{k})]. Then,

D(f)[m] = ⨆ [n ∘ n^{−1}(μ_{k})] , because [n ∘ ] and D(n) are continuous,
⨆ [μ_{k}] = [id] and n^{−1}[id] = [id]
⊆ ⨆ [n′ ∘ n^{′−1}(μ_{k})]
= D(f′)[m].

Acknowledgements

This work was done under the supervision of Gordon Plotkin and Barry Jay. I would like to thank them both for their general guidance and specific ideas. I would also like to thank John Power and Eugenio Moggi for intense discussions. Finally, thanks to the referees for comments and suggestions.

References

Fiore, M.P. (1994) Axiomatic Domain Theory in Categories of Partial Maps. PhD thesis, Uni-

versity of Edinburgh. Fiore, M.P. and Plotkin, G.D. (1994) An Axiomatisation of Computationally Adequate Domain

Theoretic Models of FPC. In 9^{th} LICS Conf., pages 92–102. IEEE, Computer Society Press. Freyd, P.J. and Kelly, G.M. (1972) Categories of continuous functors, I. Journal of Pure and

Applied Algebra, 2:169–191. Kelly, G.M. (1982) Basic Concepts of Enriched Category Theory. Cambridge University Press. Longo, G. and Moggi, E. (1984) Cartesian Closed Categories of Enumerations for effective Type-

Structures. In G. Kahn, D. MacQueen, and G. Plotkin, editors, Symposium on Semantics of Data Types, volume 173 of Lecture Notes in Computer Science. Springer-Verlag.

Moggi, E. (1986) Categories of Partial Morphisms and the partial lambda-calculus. In Proceedings Workshop on Category Theory and Computer Programming, Guildford 1985 , volume 240 of Lecture Notes in Computer Science, pages 242–251. Springer-Verlag.

Plotkin, G.D. (1985) Denotational Semantics with Partial Functions. Lecture at C.S.L.I. Summer

School. Robinson, E. and Rosolini, G. (1988) Categories of Partial Maps. Information and Computation,

79:95–130. Rosolini, G. (1986) Continuity and Effectiveness in Topoi. PhD thesis, University of Oxford. Smyth, M.B. (1992) Topology. In S. Abramsky, D.M. Gabbay, and T.S.E. Maibaum, editors,

Handbook of Logic in Computer Science, volume 1, pages 641–761. Oxford University Press.

Marcelo P. Fiore 34

Zhang, G.-Q. (1991) Logic of Domains. Birkhäuser.