Continuous information categories

Abbas Edalat

Department of Computing Imperial College of Science, Technology and Medicine 180 Queen’s Gate London SW7 2BZ England

November 7, 1991

1 Introduction

The abstract notion of category of information systems, whose initial idea was proposed in [Smy89], was formulated in [Eda89] and was later developed in [ES91a]. The original aim in [Eda89] was to generalize Larsen and Winskel’s category of Scott information systems in [LW84] into an abstract category of “information systems” with a distinguished class of morphisms, called inclusion morphisms. These morphisms induce a partial order on objects and one on morphisms and it is assumed that the set of morphisms, as well as objects, form an ω-algebraic poset. This abstract category then provided a common framework for effectively presenting a wide range of categories, including categories of sets, domains and Boolean algebras. The main result was to obtain an initial algebra (least fixed point) theorem which makes solving a domain equation F (X) ≅ X for an endofunctor F on a category of information systems particularly simple. Provided that the function induced by F on the cpo of morphisms is continuous, we can readily obtain a canonical solution (initial algebra) to the domain equation. Moreover the whole construction can be done effectively.

These ideas were further refined in [ES91a], where the notions of a pre-I-category, an I-category, a complete I-category and an ω-algebraic algebraic I-category were introduced. An ω-algebraic I-category is what was previously called a category of information systems; whereas pre-I- categories, I-categories and directed complete I-categories stand to ω-algebraic I-categories as pre-orders, posets and dcpo’s stand to ω-algebraic posets. Furthermore, the notion of concrete I-categories or information categories was formalized. In these categories, objects are structured sets and morphisms are functions or relations preserving the structure. The unique inclusion morphism from an object A to an object B exists iff A is a substructure of B. Many concrete categories have in fact such a structure and, in the work cited above, more basic examples of complete and ω-algebraic information categories, including categories of information systems for a number of cartesian closed categories of domains, were presented.

In view of the wide range of categories which can be presented as complete or ω-algebraic information categories (and there are other examples including metric spaces which will be treated in future papers), we make the following observation: Many basic categories are equivalent to complete or algebraic information categories.

The relation between I-categories and partial orders merits more discussion. It was shown in [ES91a] that an ω-algebraic I-category can be obtained by a certain completion, called I-completion, of a countable I-category, analogous to the way an ω-algebraic poset is obtained from the ideal completion of a countable poset. This analogy goes much further. In fact, one can regard a pre-I-category, an I-category, a complete I-category and an ω-algebraic I-category as generalizations of a pre-order, a poset, a cpo and an ω-algebraic poset respectively. In a pre-I-category, inclusion morphisms correspond to the trivial morphisms in a pre-order, but here we also have general morphisms in hom-sets which make the category non-trivial. It is well known that we can view a category as a generalized pre-order, a skeleton category as a generalized poset, a category with filtered colimits as a generalized dcpo and a locally finitely presentable category as a generalized algebraic poset. However, I-categories, while categorically non-trivial, have more structure and more common features with partial orders, and therefore can be viewed as taking an intermediate position between the simple ordered structures (cpo’s etc.) and their well known categorical generalizations (categories with filtered colimits etc.). This intermediate position is also reflected in solving domain equations in a complete I-category, where finding the initial algebra of an endofuctor is more involved that finding the least fixed point of a continuous function on a cpo but much easier than the usual categorical methods for solving a domain equation.

Our discussion above is further substantiated by the results in this paper. We will here introduce the notion of continuous I-category which generalizes the notion of algebraic I-category in the same spirit that continuous posets generalize algebraic posets. Any continuous poset regarded as a category is an example of a continuous I-category. It turns out that like the ideal completion construction, the notions of way below relation, retraction, projection, and basically all the standard theorems on cpo’s, algebraic and continuous posets have their counterparts in I-categories. In the other direction, we can compare continuous I-categories with continuous categories of Johnstone and Joyal in [JJ82]. They define a category E to be continuous if it has (small) filtered colimits and if the functor lim_{→} : Ind-(E) → E, where Ind-(E) is the ind-completion of E, has a left adjoint. (See Section 3.3.) In fact our definition of a continuous I-category is consistent with theirs once we rephrase their definition in our own framework and use I-category notions of I-completion and I-adjunction instead of ind-completion and adjunction respectively. Furthermore, whereas the analogue of the way below relation in a continuous category is quite involved, it is relatively simple and tangible in a continuous I-category. These simple features arise because completion and continuity in I-categories can be defined w.r.t. the subclass of inclusion morphisms rather than the whole class of morphisms. The analogies with the theory of continuous posets on the one hand and the theory of continuous categories ala Johnstone and Joyal on the other present a satisfactory basis for I-categories and give us the following table:

pre-order  pre-I-category  category
poset  I-category  skeleton category
dcpo  directed complete I-category category with filtered colimits
continuous poset continuous I-category  continuous category
algebraic poset algebraic I-category  locally finitely presentable category

We are therefore justified to make our second observation: Complete, continuous, and algebraic (pre) I-categories are generalizations of complete, continuous and algebraic partial (pre) orders. Another related and important result established here is that the axioms of a complete I-category and those of an ω-algebraic I-category as formulated in [ES91a] are by no means ad hoc. They are in fact consequences of and are therefore justified by universal constructions: See Proposition 3.3 for a universal definition of a directed complete I-category and Theorem 3.10 for a universal definition of a continuous I-category. Such universal characterization is particularly welcome in view of the fact that algebraic I-categories give us a most suitable framework to effectively present many basic categories, including cartesian closed categories of domains, and to solve domain equations in a simple way.

The plan of the paper is as follows. We first introduce continuous I-categories and establish their basic properties and their relations with algebraic I-categories in detail. This is followed by studying a number of functors on I-categories and proving various results for I-categories whose analogous versions hold for posets on the one hand and for general categories on the other. We then give an improved version of the initial algebra theorem by only assuming the continuity of the endofunctor on the dcpo of objects (the earlier version in [ES91a] had the stronger assumption that the endofunctor is continuous on the cpo of morphisms). We also formulate an effective theory for ω-continuous posets which is different from that in [Smy77] and [Tan74] and in fact generalises the corresponding theory for ω-algebraic posets as given in [Plo81]. We use this formulation to give an effective presentation of an ω-continuous I-category and also an effective version of the initial algebra theorem for ω-continuous posets. Finally in the last section, we show that any locally compact space gives rise to a non-trivial continuous I-category by taking its open sets as objects and the continuous maps between them as morphisms.

2 Basic definitions

In this section we give the definition of a continuous I-category. Our notations are as in [ES91a]. For a category K, we denote its set of objects by Obj_{K} and its set of morphisms by Mor_{K}, and we often delete the subscript K. The mappings dom and cod: Mor → Obj denote the domain and the codomain mappings associated with K, and Id:Obj → Mor denotes the mapping which takes an object to the identity morphism of that object. Composition of two morphisms f and g is denoted by f; g. Given a functor F : K_{1} → K_{2} between two categories K_{1} and K_{2} we write F_{o} : Obj_{K_{1}} → Obj_{K_{2}} and F_{m} : Mor_{K_{1}} → Mor_{K_{2}} for the induced mappings on objects and morphisms respectively. In this paper, unless otherwise stated, the carrier of a partial order is a class, i.e. a set or a proper class. A dcpo D is a partial order with bottom such that every directed subset A ⊆ D has a least upper bound (lub). By writing x = ⋁^{↑} A we imply that A is a directed set with lub x. Given two elements x and y of a dcpo D, we say that y is way below x, denoted by y ≪ x, if whenever for a directed subset A ⊆ D we have x ⊑ ⋁^{↑} A, there is an element a ∈ A with y ⊑ a. We say x ∈ D is compact if x ≪ x. A continuous dcpo is a dcpo D such that for every x ∈ D the class of elements way below x is a directed set with lub x. By writing x = ⋁↑ ↑ A we imply that A is a directed set of elements way below x with lub x. If D is a continuous dcpo then a subclass B ⊆ D is a basis of D if for every element x ∈ D the class of elements of B way below x is a directed set with lub x; note that D is a basis of itself. An ω-continuous poset is a continuous dcpo with a countable basis. An (ω−)algebraic dcpo is a continuous dcpo with a (countable) basis of compact elements.

2.1 I-categories

For the sake of completeness we recall the definition of an I-category from [ES91a], and we then slightly gereralize the definitions of a complete I-category and an ω-algebraic I-category to obtain a directed complete I-category and an algebraic I-category respectively.

Definition 2.1 An I-category is a four tuple (P, Inc, ⊑, Δ) where:

• P is a category,

• Inc ⊆ Mor is the subclass of inclusion morphisms of P such that in every hom-set, hom(A, B), there is at most one inclusion morphism, denoted by in(A, B) or A ↣ B,

• ⊑^{A,B} is a partial order on hom(A, B), for all A, B ∈ Obj,

• Δ ∈ Obj is a distinguished object;

which satisfy the following two axioms:

Axiom 1 (i) The subcategory P^{i} of all objects and inclusion morphisms of P forms a partially ordered class represented as a category.

(ii) in(Δ, A) exists, for all A ∈ Obj and in(Δ, A) ⊑ f for all morphisms f ∈ hom(Δ, A).

(iii) f; in(A, B) ⊑ g; in(A, B) ⇒ f ⊑ g, for all f, g ∈ Mor, in(A, B) ∈ Inc, such that the compositions are defined.

Axiom 2

f_{1} ⊑ f_{2} & g_{1} ⊑ g_{2} ⇒ f_{1}; g_{1} ⊑ f_{2}; g_{2}.

We denote the partial order induced by inclusion morphisms on Obj by ⊴, i.e. we write A ⊴ B if the unique inclusion morphism from A to B, denoted by in(A, B), exists in Inc. Observe that in(A, B) = Id(A). The partial order ⊴^{m} on Mor is defined by f ⊴^{m} g if dom(f) ⊴ dom(g), cod(f) ⊴ cod(g), and the following diagram weakly commutes:

dom(g) \overline{g} \overline{}cod(g) ∧  ∧
∧  ⊒  ∧
dom(f) \overline{f} \overline{}cod(f)

i.e. f; in(cod(f), cod(g)) ⊑ in(dom(f), dom(g)); g. Note that we can also define a pre-I-category by requiring in Axiom(i) that (P, Inc) is just a pre-order. It is also possible to dispense with the object Δ and drop Axiom 1(ii) to get an I-category without a least object. All the results in this paper with no reference to Δ remain valid for I-categories without a least object.

A directed complete I-category (P, Inc, ⊑, Δ) is an I-category which satisfies the following three axioms:

Axiom 3 (Mor, ⊴^{m}) is a dcpo.

Axiom 4 (Inc, ⊴^{m}) is a sub-dcpo of (Mor, ⊴^{m}).

Axiom 5 Composition of morphisms is a continuous operation with respect to ⊴^{m}, i.e. ⋁_{i}^{↑}(f_{i}; g_{i}) = (⋁_{i}^{↑} f_{i}); (⋁_{i}^{↑} g_{i}) whenever {f_{i}|i ∈ I} and {g_{i}|i ∈ I} are directed sets in (Mor, ⊴^{m}) with cod(f_{i}) = dom(f_{i}), for all i ∈ I.

The above three axioms are equivalent to a categorical property of completion of I-categories, which we will present in Proposition 3.3. The proof of the following proposition is a only a slight modification of the corresponding result for complete I-categories.

Proposition 2.2 In a directed complete I-category, (Obj, ⊴) is a dcpo and the mappings Id : (Obj, ⊴) → (Mor, ⊴^{m}), and dom, cod : (Mor, ⊴^{m}) → (Obj, ⊴) are continuous.

Finally, an (ω-)algebraic I-category is a directed complete I-category which satisfies the following two axioms:

Axiom 6 The dcpo (Mor, ⊴^{m}) is (ω-)algebraic.

Axiom 7 (i) f ∈ (Mor, ⊴^{m}) is compact ⇒ cod(f) ∈ (Obj, ⊴) is compact.

(ii) A, B ∈ (Obj, ⊴) are compact with A ⊴ B ⇒ in(A, B) ∈ (Mor, ⊴^{m}) is compact.

(iii) Composition of compact morphisms is compact.

The following proposition is again a refinement of the corresponding result for ω-algebraic I-categories.

Proposition 2.3 In an algebraic I-category, (Obj, ⊴) is an algebraic dcpo and compact morphisms have compact domains.

2.2 Continuous I-categories

Let P be a directed complete I-category. We will now generalise Axioms 6 and 7 to obtain a continuous I-category. It is obvious how Axiom 6 should be generalised; in order to generalise Axiom 7, however, we need to use the way below relations in (Obj, ⊴) and (Mor, ⊴^{m}), which we denote by ≪^{o} and ≪^{m} respectively. Using these relations and remembering that in a dcpo an element is compact iff it is way below itself, we can rewrite Axiom 7 as follows:

Axiom 7 (i) f ≪^{m} f ⇒ cod(f) ≪^{o} cod(f).

(ii) (A ≪^{o} A , B ≪^{o} B , A ⊴ B) ⇒ in(A, B) ≪^{m} in(A, B).

(iii) (f ≪^{m} f , g ≪^{m} g , cod(f) = dom(g)) ⇒ f; g ≪^{m} f; g.

It is now not difficult to see how Axiom 7 should be generalised:

Definition 2.4 An (ω-)continuous I-category is a directed complete I-category which satisfies the following axioms:

Axiom 6* (Mor, ⊴^{m}) is an (ω-)continuous dcpo.

Axiom 7* (i) f ≪^{m} g ⇒ cod(f) ≪^{o} cod(g).

(ii) A ≪^{o} A′ & B ≪^{o} B′ & A ⊴ B & A′ ⊴ B′ ⇒ in(A, B) ≪^{m} in(A′, B′).

(iii) f ≪^{m} f′ & g ≪^{m} g′ & cod(f) = dom(g) & cod(f′) = dom(g′) ⇒ f; g ≪^{m} f′; g′.

In summary the three clauses of Axiom 7* simply say that the (total or partial) maps:

Cod : Mor → Obj
in(−, −) : Obj × Obj → Mor
−; − : Mor × Mor → Mor

preserve the way below relations in the corresponding dcpo’s. Recall that in a dcpo the relation “a is way below b” can be interpreted as “a is a finite approximation to b” (see for example [GHK^{+}80, page xii]). Therefore Axiom 7* together with Proposition 2.7 state that in a continuous I-category the mappings dom, cod, in(−, −) and −; − preserve the notion of finite approximation. We will discuss this further in Section 2.3 below. However, before examining the basic properties of continuous I-categories, we look at the most basic example of such categories.

Example 2.5 Continuous dcpo’s. Let D be a continuous dcpo. Then, considered as a category, (D, Inc, =, ⊥) with Inc=Mor is easily seen to be a directed complete I-category (see [ES91a, page 14]). We will now show that this is in fact a continuous I-category.

Proposition 2.6 (D, Inc, =, ⊥) is a continuous I-category.

Proof We first prove that given two morphisms f = in(a, b) and f′ = in(a′, b′), we have f′ ≪^{m} f iff a′ ≪^{o} a and b′ ≪^{o} b. Suppose f′ ≪^{m} f and let a = ⋁_{i∈I}^{↑} a_{i}. Put f_{i} = in(a_{i}, a); f, for each i ∈ I. Then f′ ≪^{m} f = ⋁_{i} f_{i} and, hence, there exists i ∈ I with f′ ⊴^{m} f_{i} which implies a_{i} ⊴ a′, i.e. a′ ≪^{o} a. To show that b′ ≪^{o} b, assume

b = ⋁_{i∈I}^{↑} and let a = ⋁↑ ↑_{j∈J} a_{j}. Then for each j ∈ J, there exists j′ ∈ I with a_{j} ⊴ b_{j′}. Putting f_{j} = in(a_{j}, b_{j′}), we have f′ ≪^{m} f = ⋁_{j}^{↑} f_{j}. It follows that for some j ∈ J we have f′ ⊴^{m} f_{j}, i.e. b′ ⊴ b′_{j} which implies that b′ ≪^{o} b. To prove the converse, assume a′ ≪^{o} a and b′ ≪^{o} b and suppose f ⊴^{m} ⋁_{i∈I}^{↑} f_{i}, with f_{i} : a_{i} → b_{i}. Then a ⊴ ⋁_{i∈I}^{↑} a_{i} and b ⊴ ⋁_{i∈I}^{↑} b_{i}, and, hence there exist i_{1}, i_{2} ∈ I with a′ ⊴ a_{i_{1}} and b′ ⊴ b_{i_{2}}. Let i ∈ I be such that f_{i} is above f_{i_{1}} and f_{i_{2}}, then f′ ⊴^{m} f_{i} and therefore f′ ≪^{m} f. This proves our claim. The three clauses of Axiom 7* now follow immediately and it is easy to show that (Mor, ⊴^{m}) is continuous. □

To demonstrate that we do indeed have a generalisation of the notion of an algebraic I-category we start by proving the following proposition, which is the analogue of Proposition 2.10 in [ES91a] for algebraic I-categories.

Proposition 2.7 In a continuous I-category we have:

(i) The dcpo (Obj, ⊴) is continuous.

(ii) f ≪^{m} g ⇒ dom(f) ≪^{o} dom(g).

Proof (i) The map Id ∘ dom : (Mor, ⊴^{m}) → (Mor, ⊴^{m}) is a retraction and therefore its image is a continuous dcpo (see, for example, [Jun88, page 24]). But this image is isomorphic with (Obj, ⊴).

(ii) Let (f : A → B) ≪^{m} (g : C → D) and let C = ⋁_{i∈I}^{↑} E_{i}. We must find i ∈ I with A ⊴ E_{i}. For each i ∈ I, let t_{i} = in(E_{i}, C); g. Then {t_{i}|i ∈ I} is directed and f ≪^{m} g = ⋁_{i∈I}^{↑} t_{i} which implies that there exists i ∈ I with f ⊴^{m} t_{i} i.e. A ⊴ E_{i}.

Given a continuous I-category P, we say that a subcategory Q of P is a basis of P if (Mor_{Q}, ⊴^{m}) is a basis of (Mor_{P} , ⊴^{m}). The following observation is now immediate.

Proposition 2.8 A continuous I-category with a basis of compact morphisms is algebraic.

We now justify our claim that a continuous I-category is a generalisation of an algebraic I-category by the following proposition.

Proposition 2.9 An algebraic I-category is continuous.

Proof Let P be an algebraic I-category. Then (Mor, ⊴^{m}) is an algebraic and, hence, a continuous dcpo. We will show that P satisfies the three clauses of Axiom 7*. We will repeatedly use the fact that in an algebraic dcpo we have a ≪ b iff ∃c.a ⊑ c ≪ c ⊑ b i.e. iff the two elements can be interpolated by a compact element.

(i) Suppose f ≪^{m} g. Then there exists a compact morphism h with f ⊴^{m} h ⊴^{m} g. Since Cod(h) is compact, by Proposition 2.3, and Cod(f) ⊴ Cod(h) ⊴ Cod(g), we get Cod(f) ≪^{o} Cod(g).

(ii) Suppose A ≪^{o} A′, B ≪^{o} B′, A ⊴ B and A′ ⊴ B′. Then there exists objects A′′ and B′′ with A ⊴ A′′ ≪^{o} A′′ ⊴ A′ and B ≪^{o} B′′ ≪ B′′ ⊴ B′. Furthermore, since the compact elements below B′ are directed, we can assume A′′ ⊴ B′′. By Axiom 7(ii) in(A′′, B′′) is compact and in(A, B) ⊴^{m} in(A′′, B′′) ≪^{m} in(A′′, B′′) ⊴^{m} in(A′, B′).

(iii) Suppose f ≪^{m} f′, g ≪^{m} g′, cod(f) = dom(g), and cod(f′) = dom(g′). There exists a compact morphism k : A → B with f ≪^{m} k ≪^{m} f′. We can now find a compact morphism g′′ : C → D with g ⊴^{m} g′′ ⊴^{m} g′ and B ⊴ C. Put f′′ = k; in(B, C). f′′ is the composition of compact morphisms and is therefore compact. It can also be easily shown that f ⊴^{m} f′′ ⊴^{m} f′. We now have f; g ⊴^{m} f′′; g′′ ≪^{m} f′′; g′′ ⊴^{m} f′; g′. □

2.3 Way-below preserving maps

We saw in Section 2.2 that in a continuous I-category the mappings dom, cod, in(−, −) and −; − preserve the way below relation and, therefore, the notion of finite approximation. In this section, we will give some equivalent characterization of way below preserving maps.

Let (D, ⊑) be a dcpo, where D is now assumed to be a set. Recall that the open sets of the Scott topology, ΩD, are the upward closed subsets A ⊆ D which are inaccesible by directed joins, i.e. ↑A = A and ⋁^{↑} B ∈ A ⇒ A ∩ B ≠ ∅. We say a map f : D → E between two dcpo’s is open if A ∈ ΩD ⇒ ↑f(A) ∈ ΩE. We now obtain the following topological characterisation of the way below preserving maps.

Proposition 2.10 For a map f : D → E between two continuous dcpo’s the following are equivalent:

(i) f preserves the way below relation.

(ii) f is open.

Proof (i)⇒(ii) Let A be an open set in D. We must show that ↑f(A) is inaccesible by directed lubs in E. Suppose, for some x ∈ A, f(x) = ⋁^{↑} B ∈ ↑f(A). Since D is continuous, x is the directed lub of elements of D way below it and since A is open one of these elements y, say, is in A. Now y ≪ x implies f(y) ≪ f(x). Hence, there exists b ∈ B with f(y) ⊑ b, and as f(y) ∈ f(A) we conclude that b ∈ ↑f(A).

(ii)⇒(i) Let y ≪ x and f(x) ⊑ ⋁^{↑} B. The set A = {z|y ≪ z} is open (see [Joh82, page 290]), and x ∈ A. Therefore ↑f(A) is open and contains f(x) and, hence, also ⋁^{↑} B. So there exists some b ∈ B ∩ ↑f(A). But, f(y) ⊑ a for all elements a ∈ ↑f(A). It follows that f(y) ⊑ b. □

Since open sets can be regarded as properties, the above proposition means that way below preserving maps, i.e. maps preserving the notion of finite approximation of points, and property preserving maps are basically the same. We also give the following categorical characterisation of way below preserving maps.

Proposition 2.11 Let D and E be dcpo’s and f : D → E a continuous map. Then the following are equivalent.

(i) f is an open map.

(ii) The frame map Ωf : ΩE → ΩD preserves meets.

(iii) The frame map Ωf : ΩE → ΩD, considered as a functor between two categories, has a left adjoint.

Proof (i)⇒(ii) First note that given a family of open sets A_{i} ∈ ΩX, i ∈ I, of a topological space X, we have ⋀_{i∈I} A_{i} = Int(⋂_{i} A_{i}). Now assume A_{i} ∈ ΩE, for i ∈ I. Since f is continuous, we have

Ωf(Int(⋂_{i} A_{i})) ⊆ Int(Ωf(⋂_{i} A_{i})).

Suppose a ∈ Int(Ωf(⋂_{i} A_{i})), then there exists an open set A ∈ ΩE containing a with A ⊆ Ωf(⋂_{i} A_{i}) which implies f(A) ⊆ ⋂_{i} A_{i}. Since ⋂_{i} A_{i} is upperclosed, we get ↑(f(A)) ⊆ ⋂_{i} A_{i}, and since f is open ↑f(A) ⊆ Int(⋂_{i} A_{i}). We now obtain A ⊆ Ωf(Int(⋂_{i} A_{i})), i.e. a ∈ Ωf(Int(⋂_{i} A_{i})).

(ii)⇒(i) First we show that for any upperclosed set B of a dcpo X we have

B = ⋂{C|C ∈ ΩX, B ⊆ C}.

Clearly B ⊆ ⋂{C|C ∈ ΩX, B ⊆ C}. On the other hand if x ∉ B, then the open set X \ ↓x is a superset of B which does not contain x. Therefore, x ∉ ⋂{C|C ∈ ΩX, B ⊆ C}. Now let A ∈ ΩE be an open set and put B = ↑f(A). We claim that B = Int(⋂{C|C ∈ ΩX, B ⊆ C}). For convenience we denote the right hand side by {C_{i}|i ∈ I} where I is an indexing set. By what we have just shown, we have Int(⋂_{i} C_{i}) ⊆ B. We therefore have to show that B ⊆ Int(⋂_{i} C_{i}). Since Ωf preserves meets, we get

Int(⋂_{i} Ωf(C_{i})) = Ωf(⋂_{i} Int(C_{i}))

and, hence,

f(Int(⋂_{i} Ωf(C_{i})) ⊆ ⋂_{i} Int(C_{i}).

But ↑f(A) = B ⊆ C_{i}, for all i ∈ I, implies A ⊆ Int(⋂_{i} Ωf(C_{i})), i.e.

f(A) ⊆ f(Int(⋂_{i} Ωf(C_{i}))) ⊆ ⋂_{i} Int(C_{i}).

(ii) ⟺ (iii) This is a well known exercise; see for example [LS86, page 15]. □

3 Some functors on I-categories

In this section, we generalise the notions of Galois connections, retractions and projections, and we will show that the basic retractive and projective properties of dcpo’s have their counterparts for directed complete I-categories. We will also show some universal properties of I-completion. Recall that a standard functor between two I-categories is one which preserves inclusion morphisms and a continuous functor between two directed complete dcpo’s is one for which the induced mapping on morphisms is continuous.

3.1 I-adjunctions

Recall that given pre-orders (A, ≤) and (B, ≤) a pair of order preserving maps f : A → B and g : B → A is said to be a Galois connection if Id_{A} ≤ g ∘ f and f ∘ g ≤ Id_{B}. Furthermore the Galois connections between A and B are precisely the adjunctions between A and B considered as categories. We will now show that these notions can be extended to pre-I-categories. For convenience, we will drop the subscripts on the maps F_{o} and F_{m} induced by a functor F.

Definition 3.1 Let P and Q be pre-I-categories. A pair of standard functors F : P → Q and G : Q → P forms a Galois I-connection if G ∘ F ⊴^{m} 1_{P} and F ∘ G ⊴^{m} 1_{Q}.

We will show in the following proposition that a Galois I-connection is a lax adjunction, in which the natural transformations are lax i.e. give rise to weakly commutatative square diagrams.

Proposition 3.2 An I-connection between a pair of pre-I-categories is a lax adjunction.

Proof Let F : P → Q and G : Q → P be a Galois I-connection. Define η : 1_{P} → G ∘ F by η_{A} = in(A, G ∘ F (A)) and ϵ : F ∘ G → 1_{Q} by ϵ_{B} = in(F ∘ G(B), B). The statement that ϵ and η are lax natural transformations is precisely the statement that 1_{P} ⊴^{m} G ∘ F and F ∘ G ⊴^{m} 1_{Q} respectively. Furthermore, we have

((Gϵ) ∘ (ηG))_{B} = G(ϵ_{B}) ∘ η_{G(B)} = in(GF G(B), G(B)) ∘ in(G(B), GF G(B)) = Id_{G(B)}

i.e. Gϵ ∘ ηG = 1_{G} and similarly ϵF ∘ F η = 1_{F}. This shows the triangular equalities and completes the proof. □

In view of the above proposition, we call a Galois I-connection (F, G) an I-adjunction, F a left I-adjoint and G a right I-adjoint.

3.2 I-completion

We need to recall the definition of the I-completion of an I-category from [ES91a], which we will slightly refine here as I-categories can be large in the present paper; we will also show the universal property of I-completion. Given a partial order (L, ⊑), where L is a class, its ideal completion, denoted by (\overline{L}, ⊆), is the class of directed and downward closed subsets of L ordered by inclusion.

Now let P = (P, Inc, ⊑, Δ) be an I-category, its I-completion, \overline{P} = (\overline{P} , \overline{Inc}, ⊆, \overline{Δ}) is given by:

• Obj\overline{P} = \overline{Obj_{P}};

• Mor\overline{P} = \overline{Mor_{P}} ,

dom(F) = {dom(f)|f ∈ F} , cod(F) = ↓{cod(f)|f ∈ F},

Id(A) = ↓{Id(A)|A ∈ A} ,

F; G = ↓{f; g|f ∈ F, g ∈ G}(assuming cod(F) = dom(G))

(where ↓S is the downward closure of S);

• in(A, B) exists iff A ⊆ B, and when it exists we have:

in(A, B) = ↓{in(A, B)|A ∈ A, B ∈ B, A ⊴ B};

• the inclusion ⊆ as the partial order on hom-sets;

• \overline{Δ} = \{Δ\}.

It was proved in [ES91a] that if P is a countable I-category, \overline{P} is an ω-algebraic I-category. One can easily extend the proof to show that if P is any I-category, then \overline{P} is an algebraic I-category. It should be clear that I-completion is a generalisation of ideal completion. In fact if P is a poset, the ideal completion of P is an algebraic dcpo which regarded as a category is the same as the I-completion of P regarded as an I-category.

On the other hand, I-completion can be regarded as a restricted form of Ind-completion of a category, i.e. an Ind-completion which is restricted to the inclusion morphisms. To make this more precise we need to recall the definition of an Ind-object of a category, say from [JJ82]. Let P be a locally small category. An Ind-object in P is defined to be a small filtered diagram in P, i.e. a functor J → P where J is a small filtered category. For any object A of P, there is the constant Ind-object y(A) : 1 → P which picks A. Morphisms between Ind-objects are also defined but we will not go into them here. We then obtain a category Ind-P, the Ind-completion of P, which has filtered colimits and in which P can be embedded by y : P → Ind-P. We can now compare this with I-completion. If P is an I-category an object of its I-completion \overline{P} is, in effect, an Ind-object F : J → P^{i}, where P^{i} is the subcategory of inclusion morphisms. It also turns out that morphisms of \overline{P} are in effect morphisms between such Ind-objects.

A poset P is a dcpo iff the embedding ↓(−) : P → \overline{P} has a left adjoint (the left adjoint necessarily sends an ideal to its directed lub in P); and a locally small category P has small filtered colimits iff the embedding y : P → Ind-P has a left adjoint. A similar result holds for I-categories:

Proposition 3.3 An I-category P is directed complete iff the functor ↓(−) : P → \overline{P} has a left I-adjoint.

Proof If P is directed complete, the functor ⋁^{↑}(−) : \overline{P} → P which sends any ideal of objects and any ideal of morphisms to their directed lub is left I-adjoint to ↓(−). To prove the converse, suppose that F : \overline{P} → P is left I-adjoint to ↓(−), then F_{m} : Mor\overline{P} → Mor_{P} is left adjoint to ↓(−)_{m} : Mor_{P} → Mor\overline{P} and, hence, by the remark just before this proposition, we have F = ⋁^{↑}(−) and Mor_{P} is a dcpo. Axioms 4 and 5 follow from the functorial properties of ⋁^{↑}(−). In fact, suppose in(A, B) is an inclusion morphism in \overline{P}. Since ⋁^{↑}(−) is standard by assumption, we have ⋁^{↑} in(A, B) = in(⋁^{↑} A, ⋁^{↑} B), i.e. Axiom 4 holds. Axiom 5 is shown in a similar way. □

The above proposition therefore provides us with an alternative definition for a directed complete I-category: An I-category P is directed complete if the functor ↓(−) : P → \overline{P} has a left I-adjoint.

Furthermore I-completion can be regarded as a functor. Let I-Cat be the category of I-categories with standard functors and AlgI-Cat the category of algebraic I-categories with standard and continuous functors. It is now clear that I-completion extends to a functor C : I-Cat → AlgI-Cat, where for an I-category P, we have C(P) = \overline{P} and for a standard functor F : P → Q, we have C(F) = F : \overline{P} → \overline{Q} with F defined on the basis \overline{P}^{b} of \overline{P} by F_{o}(↓A) = ↓F_{o}(A), and F_{m}(↓f) = ↓F_{m}(f), and extended by continuity to \overline{P}. We now have the following universal property:

Proposition 3.4 C is left adjoint to the forgetfull functor from AlgI-Cat to I-Cat.

Proof Let P be an I-category and let η(P) : P → \overline{P} be the functor which sends each object A and each morphism f to the principal ideals ↓A and ↓f respectively. Given an algebraic I-category Q and a standard functor F : P → Q, we obtain a unique functor F̂ such that F̂ ∘ η(P) = F by putting F̂_{o} and F̂_{m} to be the unique maps such that F̂_{o} ∘ η(P)_{o} = F_{o} and F̂_{m} ∘ η(P)_{m} = F_{m} hold; the existence and uniqueness of F̂_{o} and F̂_{m} follow of course from the universal property of ideal completion of partial orders. This completes the proof. □

3.3 I-retractions and I-projections

Recall that a continuous function f : D → D on a dcpo D is called a retraction if r ∘ r = r. It is called a projection if we also have r ⊑ Id_{D}. Continuous functions r : D → E and e : E → D between dcpo’s D and E are said to form a retraction-embedding pair, if r ∘ e = Id_{E}. The pair (r, e) is a projection-embedding pair if e ∘ r is a projection on D and r ∘ e = Id_{E}. If there is a retraction (projection)-embedding pair between D and E, we say that E is a retractive (projective) image of D.

We now need the following propositions.

Proposition 3.5 Let r : D → D be a retraction. Then im(r) is a dcpo and the supremum of a directed subset of im(r) formed in im(r) coincides with the supremum formed in D.

Proof See [Jun88, page 24]. □

Proposition 3.6 Let D be an continuous dcpo, E a dcpo and p : D → E and e : E → D a projection embedding pair. Then

(i) E is continuous.

(ii) If D is ω-continuous, so is E.

(iii) x ≪_{E} y ⟺ e(x) ≪_{D} e(y).

Proof (i) See [Jun88, page 24].

(ii) This follows from the fact that if {a_{i}|i ∈ I} is a basis for D, then {r(a_{i})|i ∈ I} is a basis for E.

(iii) Suppose x ≪_{E} y. Let e(y) = ⋁_{i∈I}^{↑} z_{i}. Then y = p ∘ e(y) = ⋁_{i∈I}^{↑} p(z_{i}), and, therefore, there exists i ∈ I with x ⊑ p(z_{i}). Hence, e(x) ⊑ e ∘ p(z_{i}) ⊑ z_{i}, which implies that e(x) ≪_{D} e(y). Suppose on the other hand that e(x) ≪_{D} e(y) and y = ⋁_{i∈I}^{↑} z_{i}. Then e(y) = ⋁_{i∈I}^{↑} e(z_{i}), and so there exists i ∈ I with e(x) ⊑ e(z_{i}). Therefore x = p ∘ e(x) ⊑ p ∘ e(z_{i}) = z_{i} which implies that x ≪_{E} y. □

We will now define the notions of retraction and projection for I-categories.

Definition 3.7 Let P and Q be directed complete I-categories. A standard continuous endofunctor R : P → P is called an I-retraction (I-projection) if the induced map on morphisms R_{m} : Mor → Mor is a retraction (projection). Two standard and continuous functors R : P → Q and E : Q → P are said to form an I-retraction (projection) embedding pair if R_{m} : Mor_{P} → Mor_{Q} and E_{m} : Mor_{Q} → Mor_{P} form a retraction (projection) embedding pair.

It can be easily seen from the equality R_{o} = dom ∘ R_{m} ∘ Id that if R is an I-retraction (projection), then R_{o} : Obj → Obj is a retraction (projection). Same thing holds for I-retraction (projection) embedding pairs. Note that an I-projection embedding is a Galois I-connection and, hence, a lax adjunction.

Proposition 3.8 (i) The image of an I-retraction is a directed complete I-category.

(ii) The image of an I-projection on a continuous I-category is a continuous I-category.

Proof (i) Let R : P → P be an I-retraction. Then R(P) is an I-category with distinguished object R(Δ), where Δ is the distinguished object of P. Furthermore, by the definition of an I-retraction and by Proposition 3.3, Mor_{R(P)} is a dcpo and Inc_{R(P)} is a subdcpo. The other axioms are trivial to check.

(ii) Let R : P → Q and E : Q → P be an I-projection embedding pair and Q continuous. Then, by definition, Mor_{P} is a continuous dcpo. The three clauses of Axiom 7* can be proved by repeated use of Proposition 3.6(iii). We will show Axiom 7*(i) here. We have:

f ≪_{P}^{m} g  ⇒
R_{m}(f) ≪_{Q}^{m} R_{m}(g)  ⇒ (Proposition 3.6(iii))
Cod(R_{m}(f)) ≪_{Q}^{o} Cod(R_{m}(g)) ⇒ (Axiom 7*(i) for Q)
R_{o}(Cod(f)) ≪_{Q}^{o} R_{o}(Cod(g)) ⇒ (R is a functor)
Cod(f) ≪_{P}^{o} Cod(g)  (Proposition 3.6(iii)).
□

Next, we will show the analogue of the most basic property of continuous dcpo’s.

Proposition 3.9 Any (ω)-continuous I-category is the projective image of an (ω)-algebraic I-category.

Proof Let P be a continuous I-category and let the subcategory Q be a basis of P (since P is a basis of itself there is always a basis). The I-completion \overline{Q} of Q is an algebraic I-category. with basis \overline{Q}^{b}, where

Mor\overline{Q}_{b} = \{↓f|f ∈ Mor_{Q}\} Obj\overline{Q}_{b} = \{↓A|A ∈ Obj_{Q}\}.

We define a pair of functors F : P → \overline{Q} and G : \overline{Q} → P as follows. For f ∈ Mor_{P} and A ∈ Obj_{P}, we put

F_{m}(f) = Mor∩↓ ↓f = {g ∈ Mor_{Q}|g ≪^{m} f}, F_{o}(f) = Obj∩↓ ↓A = {B ∈ Obj_{Q}|B ≪^{o} A};

and for F ∈ Mor\overline{Q} and A ∈ Obj\overline{Q}, we put G_{m}(\overline{A}) = ⋁^{↑} F and G_{o}(\overline{A}) = ⋁^{↑} A. We have G ∘ F (f) = G(Mor_{Q} ∩ ↓ ↓f) = f, and therefore G ∘ F = 1_{P}. For f ∈ Mor_{Q}, i.e. ↓f ∈ Mor\overline{Q}_{b}, we have F ∘ G(↓f) = ↓ ↓f ⊆ ↓f and, hence, by continuiuty, F ∘ G ⊴^{m} 1\overline{Q}. Therefore (F, G) is an I-projection embedding pair as required. If P is ω-continuous, we choose Q to be a countable basis, which implies that \overline{Q} is ω-algebraic. □

Theorem 3.10 Let P be a directed complete I-category. Then P is continuous iff the functor ⋁^{↑}(−) : \overline{P} → P has a left I-adjoint.

Proof The “only if” part follows immediately from Proposition 3.9. Suppose then that the functor F : P → \overline{P} is such that (F, ⋁^{↑}(−)) is a Galois I-connection. Since the induced maps on morphisms and on objects form Galois connections, it follows by Lemma 2.1 in [JJ82] that F = ↓ ↓(−) and that Mor_{P} and Obj_{P} are continuous dcpo’s. The three clauses of axiom 7* follow from the functorial properties of ↓ ↓(−) as we will now verify. Suppose f ≪^{m} g. Since ⋁^{↑}(−) is a functor, we have ↓ ↓cod(g) = cod(↓ ↓g) = ↓{cod(h)|h ∈ ↓ ↓g}. Hence, cod(f) ∈ ↓ ↓cod(g). Suppose A ≪^{o} A′, B ≪^{o} B′, A ⊴ B and A′ ⊴ B′. Then Since ⋁^{↑}(−) is standard by assumption, we have in(↓ ↓A′, ↓ ↓B′) = ↓{in(A, B)|A ≪^{o} A′, B ≪^{o} B′, A ⊴ B}. Hence, in(A, B) ∈ ↓ ↓in(A′, B′) Suppose f ≪^{m} f′ and g ≪^{m} g′ with cod(f) = dom(g) and cod(f′) = dom(g′). Then ↓ ↓(f′; g′) = (↓ ↓f′); (↓ ↓g′) = ↓{f; g|f ∈ ↓ ↓f′, g ∈ ↓ ↓g′, cod(f′) = dom(g′)} and therefore f; g ∈ ↓ ↓(f′; g′). This completes the proof that P is continuous.

Theorem 3.10 provides us with an alternative definition of a continuous I-category: A directed complete I-category P is continuous if the functor ⋁^{↑}(−) : \overline{P} → P has a left I-adjoint. As pointed out in the introduction, this makes the definition of a continuous I-category universal and shows also that our definition is consistent with the way Johnstone and Joyal define a continuous category.

It is well known that a retract of a continuous dcpo is a continuous dcpo. A similar result holds for I-categories. The proof of the following result, in effect, uses the anologue of the “adjoint lifting” lemma [Joh81] for I-categories.

Proposition 3.11 Let P be a continuous I-category and P′ a directed complete I-category. Suppose R : P → P′ and E : P′ → P form an I-retraction embedding pair. Then P′ is continuous.

Proof Let F = ↓ ↓(−)_{P} : P → \overline{P}, G = ⋁_{P}^{↑} : \overline{P} → P and G′ = ⋁_{P′}^{↑} : \overline{P′} → P′. Since P is continuous (F, G) forms an I-projection embedding by Proposition 3.9. Put F′ = \overline{R} ∘ G ∘ E : P′ → \overline{P′}. We will show that F′ is left I-adjoint to G′ which establishes the proof by Theorem 3.10. Since R and E are continuous, we get E ∘ G′ = G ∘ \overline{E} and G′ ∘ \overline{R} = R ∘ G. We now calculate

F′ ∘ G′ = \overline{R} ∘ F ∘ E ∘ G′ = \overline{R} ∘ F ∘ G ∘ \overline{E} ⊴^{m} \overline{R} ∘ \overline{E} = 1\overline{P′}

and

G′ ∘ F′ = G′ ∘ \overline{R} ∘ F ∘ E = R ∘ G ∘ F ∘ E = R ∘ E = 1_{P′}.
□

4 Effectiveness

In [ES91a], an effective theory for ω-algebraic I-categories was developed and an effective version of the initial algebra theorem was presented. In this section, we will generalise these to ω-continuous I-categories. To do this, we need to formulate a suitable notion of effectively given ω-continuous dcpo’s, as the existing formulations in [Smy77] and [Tan74] do not fit into our context.

4.1 Effectively given ω-continuous dcpo’s

We define the notion of effectively given ω-continuous cpo by putting a suitable recursive structure on a basis of it. Our treatment resembles that of Plokin in [Plo81] for ω-algebraic cpo’s, but it is more involved. We will use the standard notions from classical recursion theory as, for example, in [Cut80]. In particular, ϕ_{n}, is the n^{th} partial recursive function in the standard enumeration and ⟨m_{1}, ⋯, m_{n}⟩ is the n-tupling function from ℕ^{n} to ℕ.

Let E be an ω-continuous cpo with a countable basis B and let e : ℕ → B be an onto map i.e. an enumeration of the basis elements of E. We say E is effectively given w.r.t. e with index < a, s, t, u > if

(i) e_{a} = ⊥.

(ii) The predicate e_{m}↑e_{n} (i.e. e_{m} and e_{n} are bounded above) is recursive in m and n with index s.

(iii) e_{m} ⊑ e_{n} is recursive in m and n with index t.

(iv) e_{m} ≪ e_{n} is recursive in m and n with index u.

An effective chain w.r.t. B of E with index l w.r.t. e is an increasing chain < e_{ϕ_{l}(n)} >_{n≥0} with e_{ϕ_{l}(n)} ≪ ⨆_{i} e_{ϕ_{l}(i)} for all n ≥ 0. An element d ∈ E is computable w.r.t. B and e if there exists an effective chain with lub d. The index of d w.r.t. e is defined to be the index of this effective chain. We now want to enumerate the computable elements of E and for this we need the following.

Proposition 4.1 Every non-negative integer, i.e. every index, gives rise to an effective chain.

Proof We can assume that every index l gives rise to an increasing total chain of elements of B (see [Plo81] for how this is done). We will now show that every index further gives rise to an increasing chain such that every element of the chain is way below the lub of that chain. Suppose then that the index l gives rise to the increasing chain < e_{n_{i}} >_{i≥0}. We effectively construct an array < e_{m_{ij}} >_{i,j≥0} such that

(i) ⨆_{j} e_{m_{ij}} = e_{n_{i}}, for all i ≥ 0.

(ii) e_{m_{ij}} ≪ e_{n_{i}}, for all i, j ≥ 0.

(iii) e_{m_{ij}} ⊑ e_{m_{i+1 j}} for all i, j ≥ 0.

Then it will follow that ⨆_{i} e_{m_{ii}} = ⨆_{i} e_{n_{i}} and furthermore e_{m_{ii}} ≪ e_{n_{i}} ⊑ ⨆_{k} e_{n_{k}}, for all i ≥ 0, and therefore the increasing chain < e_{m_{ii}} >_{n≥0} will satisfy our requirement. The array < e_{m_{ij}} >_{i,j≥0} is constructed inductively as follows.

• Construction of < e_{m_{0j}} >_{j≥0}: If e_{n_{0}} ≪ e_{n_{0}}, put m_{0j} = n_{0} for all j ≥ 0. Otherwise, let m_{00} be the least integer with e_{m_{00}} ≪ e_{n_{0}}. Suppose m_{0j} has been chosen such that e_{m_{0 j−1}} ⊑ e_{n_{0j}} ≪ e_{n_{0}}. Let m_{0 j+1} be the least integer with m_{0j} < m_{0 j+1} ≪ e_{n_{0}}.

• Construction of < e_{m_{i+1 j}} >_{j≥0}: Assume < e_{m_{ij}} >_{j≥0} has been constructed. If e_{m_{i+1}} ≪ e_{m_{i+1}} put m_{i+1 j} = n_{i+1} for all j ≥ 0. Otherwise let m_{i+1 0} be the least integer with e_{m_{i0}} ⊑ e_{m_{i+1 0}} ≪ e_{m_{i+1}}. Assuming m_{i+1 j} has been determined with e_{m_{i+1 j−1}} ⊑ e_{m_{i+1 j}} ≪ e_{m_{i+1}} and e_{m_{ij}} ⊑ e_{m_{i+1 j}}, let m_{i+1 j+1} be the least integer with

– m_{i+1 j} < m_{i+1 j+1}.

– e_{m_{i j+1}} ⊑ e_{m_{i+1 j+1}}.

– e_{m_{i+1 j}} ⊑ e_{m_{i+1 j+1}}.

– e_{m_{i+1 j+1}} ≪ e_{n_{i+1}}.

This completes the proof. □

Denoting the poset of the computable elements of E by C_{E}, we can then obtain an enumeration e′ : ℕ → C_{E} of C_{E} with respect to e. Given two ω-algebraic cpo’s E_{1} and E_{2} with e_{1}, e′_{1} and e_{2}, e′_{2} as enumeration of their compact and computable elements respectively, we say that a continuous function f : E_{1} → E_{2} is computable if there exists a recursive function l : ℕ → ℕ such that the diagram:

ℕ  \overline{l} \overline{}ℕ
[figure: e′_{1}; e′_{2}]
E_{1}  \overline{f} \overline{}E_{2}

commutes. Any index for l is, then, said to be an index for f. Note that the composition of computable functions is computable, since the composition of recursive functions is recursive.

Lemma 4.2 The lub of an increasing effective chain of computable elements is computable and an index for it can be effectively obtained from an index for the effective chain.

Proof Let a = ⨆_{n} a_{n} be the lub of a chain of computable elements with a_{n} = ⨆_{i} e_{m_{ni}}. For each n ≥ 0, we will construct an effective chain < e_{l_{ni}} >_{i≥0} with a_{n} = ⨆_{i} e_{l_{ni}} such that e_{l_{ni}} ⊑ e_{l_{n+1 i}} for all i ≥ 0. For n = 0, we put l_{0i} = m_{0i} for all i ≥ 0. Suppose < e_{l_{ni}} >_{i≥0} has been constructed. We have

e_{l_{ni}} ≪ a_{n} ⊑ a_{n+1} = ⨆_{i} e_{m_{n+1 i}},

for each i ≥ 0. Let i′ be the least integer with i′ ≥ i and e_{l_{ni}} ⊑ e_{m_{n+1 i′}} and put l_{n+1 i} = m_{n+1 i′}. Then e_{m_{n+1 i}} ⊑ e_{l_{n+1 i}} ≪ a_{n+1} and hence < e_{l_{n+1 i}} >_{i≥0} is an effective chain with a_{n+1} = ⨆_{i} e_{l_{n+1 i}}. It now follows that the chain < e_{l_{nn}} >_{n≥0} is effective with lub a as required. □

Corollary 4.3 The least fixed point of a computable function on an ω-algebraic cpo is computable and an index for it is effectively obtainable from an index for the function.

4.2 Effectively given continuous I-categories

We are now ready to define the notion of effectively given ω-continuous I-category.

Definition 4.4 Let P be an ω-continuous I-category. An enumeration (A, f) of a basis, Q, of P is given by an enumeration A : ℕ → Obj_{Q} and an enumeration f : ℕ → Mor_{Q} of objects and morphisms of Q respectively. P is said to be effectively given with respect to (A, f) by index ⟨a, r, s, t, u, v, w⟩ if the following five conditions hold:

R1 (Mor_{P} , ⊴^{m}) is effectively given with respect to f with index ⟨a, r, s⟩;

R2 dom(f_{n}) = A_{l} is recursive in n and l with index t;

R3 cod(f_{n}) = A_{l} is recursive in n and l with index u;

R4 f_{n} = in(A_{l}, A_{p}) is recursive in n, l and p with index v;

R5 f_{n}; f_{l} = f_{p} is recursive in n, l and p with index w.

We now have the following properties which are the analogue of the corresponding results for effectively given ω-algebraic I-categories.

Proposition 4.5 Let P be an ω-continuous I-category effectively given with respect to (A, f).

(i) (Obj_{P} , ⊴) is effectively given with respect to A with an index which can be effectively obtained from an index for P with respect to (A, f).

(ii) The mappings dom, cod : (Mor, ⊴^{m}) → (Obj, ⊴) and the mapping Id : (Obj, ⊴) → (Mor, , ⊴^{m}) are computable and an index for each can be effectively obtained from an index for P with respect to (A, f).

(iii) If B, C ∈ Obj_{P} are computable with indices i, j respectively and B ⊴ C, then in(B, C) is computable and an index for it can be effectively obtained from i, j.

(iv) If g, h ∈ Mor_{P} are computable with cod(g) = dom(h), then g; h is also computable and an index for it can be effectively obtained from one for g and one for h.

Proof (i)-(ii) The proof is as in Proposition 4.4 in [ES91a].

(iii) We have B = ⨆_{n} A_{ϕ_{i}(n)} and C = ⨆_{n} A_{ϕ_{j}(n)}. For each integer n ≥ 0, let n′ be the least integer with n′ ≥ n and A_{ϕ_{i}(n)} ⊴ A_{ϕ_{j}(n′)}. Such n′ exists since A_{ϕ_{i}(n)} ≪ B ⊑ C, for all n ≥ 0. Now let l(n) be the least integer with f_{l(n)} = in(A_{ϕ_{i}(n)}, A_{ϕ_{j}(n′)}). Then l is recursive with an index which can be effectively obtained from i, j. We also have in(B, C) = ⨆_{n} f_{l(n)} and, by Axiom 7*(ii), in(A_{ϕ_{i}(n)}, A_{ϕ_{j}(n′)}) ≪^{m} in(A, B).

(iv) Let g, h have indices i, j respectively, i.e. g = ⨆_{n} f_{ϕ_{i}(n)} and h = ⨆_{n} f_{ϕ_{j}(n)}. For each n ≥ 0, let n′ be the least integer with n′ ≥ n and cod(f_{ϕ_{i}(n)}) ⊴ dom(f_{ϕ_{j}(n′)}) and let l(n) be the least integer with

f_{l(n)} = f_{ϕ_{i}(n)}; in(cod(f_{ϕ_{i}(n)}), dom(f_{ϕ_{j}(n′)})); f_{ϕ_{j}(n′)}.

Since f_{ϕ_{i}(n)} ≪ g, in(cod(f_{ϕ_{i}(n)}), dom(f_{ϕ_{j}(n′)})) ≪ Id(cod(g)) and f_{ϕ_{j}(n′)} ≪ h, we get, by Axiom 7*(iii), f_{l(n)} ≪ g; h. We also have g; h = ⨆_{n} f_{l(n)}, and moreover, by applying R2-R5, we find that l is recursive with an index which is effectively computable from i and j. □

This completes our treatment of effectively given ω-continuous I-categories. Without any further work, however, we can obtain an effective version of the initial algebra theorem for ω-continuous I-categories. Recall the following definition.

Definition 4.6 (i) A continuous endofunctor F on an effectively given ω-continuous I-category is computable if the induced cpo function F_{m} : (Mor_{P} , ⊴^{m}) → (Mor_{P} , ⊴^{m}) is computable.

(ii) An F -algebra (E, k) is computable if k ∈ (Mor_{P} , ⊴^{m}) is computable.

The following results now hold exactly as in the case of ω-algebraic I-categories.

Proposition 4.7 If F is a computable endofunctor on an effectively given ω-continuous I-category P, then the induced function F_{o} : Obj_{P} → Obj_{P} is computable.

Proposition 4.8 Let F be a computable endofunctor on an effectively given ω-continuous I-category P. Then P has a computable initial algebra (D, Id(D)), an index for which is effectively obtainable from one for F. Moreover if (E, k) is a computable F -algebra, the unique morphism h satisfying h = F (h); k is computable and an index for h can be effectively obtained from one for F and one for (E, k).

5 Locally compact topological spaces

Clearly, all the ω-algebraic I-categories presented in [ES91a], including BC-ISys (Scott information systems with approximable mappings), SFP-ISys (SFP information systems with approximable mappings) and dI-ISys (dI-infformation systems with stable mappings), are examples of ω-continuous I-categories. There are however continuous I-categories which are not algebraic, a situation similar to the case of posets. The simplest non-algebraic continuous I-category is of course a continuous poset regarded as a category, which we have already discussed in Example 2.5. We will now give a non-trivial example of a continuous (non-algebraic) I-category.

Recall that a topological space (not necessarily Hausdorff) is said to be locally compact if every point has a basis of compact neighborhoods, i.e. given a point and an open set containing it, there is a compact set contained in the open set whose interior contains that point. (Note that some authors use the term “quasicompact” rather than “compact” when the space is non-Hausdorff, but we will continue to use “compact” in the non-Hausdorff setting as well). Consider a locally compact space X. It is well known that the lattice of open sets of X is a continuous lattice and given two open sets A and B, we have A ≪ B iff A is relatively compact w.r.t. B (i.e. every open covering of B has a finite subcovering of A) iff there exists a compact C ⊆ X with A ⊆ C ⊆ B [GHK^{+}80, Page 42]. We will now show that X gives rise to a non-trivial continuous I-category. Let K be the category whose objects are the open sets of X and whose morphisms are the continuous functions between these open sets. Then we claim that (K, Inc, =, ∅), where Inc is the set of set inclusions, is a continuous I-category. Note that here we have the simple relation f ⊴^{m} g ⇒ f = g↾_{dom(f)}. We first need the following lemma.

Lemma 5.1 Let f : A → C and g : B → D be morphisms of C. Then we have

f ≪^{m} g ⟺ f ⊴^{m} g & A ≪^{o} B & C ≪^{o} D.

Proof ⇒: Clearly f ⊴^{m} g. Since ΩX is a continuous lattice, B and D are the

directed sup of open sets way below them, i.e. B = ⋁↑ ↑_{i∈I} B_{i} and D = ⋁↑ ↑_{j∈J} D_{j}. For each i ∈ I, let g_{i} : B_{i} → D be given by g_{i} = g↾_{B_{i}}. Then ⟨g_{i}⟩_{i∈I} is directed and g = ⋁_{i}^{↑} g_{i}. Therefore, f ⊴^{m} g_{i} for some i ∈ I and hence A ⊴ B_{i} ≪^{o} B. To prove that C ≪^{o} D, let E_{j} = Ωf(D_{j}) for each j ∈ J and define h_{j} : E_{j} → D_{j} by h_{j} = g↾_{E_{j}}. Then B = ⋁_{j}^{↑} E_{j} and g = ⋁_{j}^{↑} h_{j} and therefore f ⊴^{m} h_{j} for some j ∈ J. This gives C ⊴ E_{j} ≪^{o} D, as required.

⇐: Suppose f ⊴^{m} g, A ≪^{o} B and C ≪^{o} D. Let g_{i} : B_{i} → D_{i} satisfy g ⊴^{m} ⋁_{i}^{↑} g_{i}. Then B ⊴ ⋁_{i}^{↑} B_{i} and D ⊴ ⋁_{i}^{↑} D_{i}, and hence there exists i ∈ I with A ⊴ B_{i} and C ⊴ D_{i}. Since g_{i} = (⋁_{i}^{↑} g_{i})↾_{B_{i}}, g = (⋁_{i}^{↑} g_{i})↾_{B} and f = (⋁_{i}^{↑} g_{i})↾_{A}, we get f = g_{i}↾_{A}, i.e. f ⊴^{m} g_{i} which gives f ≪^{m} g. □

Now we can establish our claim.

Proposition 5.2 (K, Inc, =, ∅) is a continuous I-category.

Proof Axioms 1-5 are easy to verify and are left to the reader. Axiom 7* follows from Lemma 5.1. To verify that (Mor, ≪^{m}) is a continuous dcpo, note first that the set of morphisms way below a given morphism g : A → B is directed: Given f : C → D and h : E → F with f ≪^{m} g and h ≪^{m} g, the mapping k : C ∪ E → D ∪ F given by k = g↾_{C∪E} is above f and h and way below g. It remains to show that g is the directed sup of morphisms way below it. First we write A and B as the directed

sup of open sets way below them: A = ⋁↑ ↑_{i∈I} A_{i} and B = ⋁↑ ↑_{i∈I} B_{i}. (Note that we are

justified to use the same indexing sets for if A = ⋁↑ ↑_{i∈I} A_{i} and B = ⋁↑ ↑_{j∈J} B_{j}, then we

have A = ⋁↑ ↑{A_{ij}|(i, j) ∈ I × J} and B = ⋁↑ ↑{B_{ij}|(i, j) ∈ I × J}, where A_{ij} = A_{i} and B_{ij} = B_{j}.) For each i ∈ I, let C_{i} be a compact subset with A_{i} ⊆ C_{i} ⊆ A. Since

g is continuous g(C_{i}) is also compact and we have g(C_{i}) ⊆ B = ⋁↑ ↑_{i∈I} B_{i}. Hence there exists i′ ∈ I with g(C_{i}) ⊆ B_{i′} and we can assume that i′ ≥ i. We now let

g_{i} : A_{i} → B_{i′} be the restriction of g to A_{i}. Then we have g ≪^{m} g_{i} and B = ⋁↑ ↑_{i∈I} B_{i′}

which imply g = ⋁↑ ↑_{i∈I} g_{i} as required. □

Example 5.3 ℝ^{n} Let X = ℝ^{n} with the usual Huasdorff topology. Then X is locally compact and the category K constructed above is a continuous I-category. Since ℝ^{n} is second countable, Obj_{K} is in fact an ω-continuous cpo and if we restrict the morphisms to a countable set, e.g. all linear transformations represented by n × n matrices with rational entries, we obtain an ω-continuous I-category.

Example 5.4 Continuous posets. Let (X, ⊑) be a continuous poset. Then X with the Scott topology ΩX is locally compact. (Given an open set A ∈ ΩX and a point

x ∈ A, we have x = ⋁↑ ↑{y | y ≪ x} and, therefore, there exists y ∈ A with y ≪ x. Then the set ↑y is compact and its interior ↑ ↑y contains x.) It follows that the category (K, Inc, =, ∅), constructed in the previous subsection, is a continuous I-category. We now ask the following question. If the hom-sets are ordered in the usual way (i.e. for f, g : A → B, we define f ⊑ g iff f(a) ⊑ g(a) for all a ∈ A), is (K, Inc, ⊑, ∅) also a continuous I-category? The answer is that it is still a directed complete I-category but it is not, in general, continuous. First note that given a directed set of morphisms ⟨f_{i} : A_{i} → B_{i}⟩_{i∈I}, the directed sup f = ⋁_{i}^{↑} f_{i} : ⋁_{i}^{↑} A_{i} → ⋁_{i}^{↑} B_{i} is defined by f(a) = ⋁_{i≥j}^{↑} f_{i}(a), where j is such that a ∈ A_{j} and the continuity of f is easy to check. Furthermore, given a directed set of inclusions ⟨in(A_{i}, B_{i})⟩_{i∈I}, its directed sup is clearly in(⋃_{i} A_{i}, ⋃_{i} B_{i}). This establishes that (K, Inc, ⊑, ∅) is a directed complete I-category. To show that it is, in general, not a continuous I-category, let X = [0, 1] with the Scott topology. Then we have (1/2, 1] ≪^{o} (0, 1], but Id((1/2, 1]) is not way below Id((0, 1]) as required by Axiom 7*(ii): Defining f_{n} : (1/n, 1] → (1/n − 1/n^{2}, 1] by f_{n}(x) = (1 − 1/n)x (n ≥ 2), we have Id((0, 1]) = ⋁_{n≥1}^{↑} f_{n}, but there is clearly no n ≥ 2 with Id((1/2, 1]) ⊴^{m} f_{n}.

Example 5.5 Category of locally compact spaces and continuous maps. The above result can be generalised to LocCom, the category of locally compact spaces and continuous maps between them. If A and B are locally compact spaces, we put A ⊴ B if A is a subspace of B and the inclusion is an open map. We also use the discrete order on homsets as before. Then (LocCom, Inc, =, ∅) is an I-category, which is easily seen to be complete. In fact if ⟨(A_{i}, ΩA_{i})⟩_{i∈I} is a directed set of locally compact spaces, then the space (⋃_{i∈I} A_{i}, ⋃_{i∈I} ΩA_{i} is locally compact. Furthermore, the lub of a directed set of morphisms is also obtained in the usual way. Now we observe that if f : A → B and g : B → D are morphisms of LocCom, then, as in Lemma 5.1, we have f ≪^{m} g iff f ⊴^{m} g & A ≪^{o} B & C ≪^{o} D. Therefore, as in Proposition 5.2, we can deduce that (LocCom, Inc, =, ∅) is a continuous I-category.

6 Categories of continuous posets

In this section we will show, as an example, that the category of bounded complete continuous posets with strict, Scott continuous and open maps is equivalent to a continuous information category whose inclusion morphisms correspond to rigid embeddings.

Consider CS-ISys, the category of continuous Scott information systems with approximable mappings which is equivalent to CS-Dom, the category of bounded complete (or Scott) continuous posets. See [ES91a]. It is convenient for us to work with a full equivalent subcategory of CS-ISys denoted by CS-ISys_{0}, which is obtained by adding an additional axiom for the objects of the category. In more detail, an object of CS-ISys_{0} is of the form A = (|A|, ≤, ∧, Δ, <) satisfying the following axiom:

O(i) (|A|, ≤) is a partial order.
O(ii) ∀a. a ≤ Δ.
O(iii) c ≤ a ∧ b ⟺ c ≤ a & c ≤ b.
O(iv) Δ < Δ.
O(v) a ≤ b, b < c, c ≤ d ⇒ a < d.
O(vi) a < b, a < c ⇒ a < b ∧ c.
O(vii) a < b, b < c ⇒ a < c.
O(viii) a < c ⇒ ∃b. a < b < c.
O(ix) a < b ⇒ a ≤ b.
O(x) ∀a ∃b. b < a.

The first nine axioms are the same as those in [ES91a, page 47] for CS-ISys; the first three say that I = (|A|, ≤, ∧, Δ) is a Scott (bounded complete) information system, (iv)-(vi) say that < is an approximable mapping and (vii)-(ix) say that <: I → I is a projection, i.e. an approximable mapping satisfying <; < = < and < ⊆ ≤, as ≤ is the identity morphism on I. The last axiom is added here in order to make the representation simple; it eliminates the redundant tokens representing the empty set, which, as we will see shortly, play no part in making the points of the space. We also assume that tokens of the carrier sets of objects come from a pool, and for a ∈ |A| we write ↑ ↑a = {a′ | a < a′}. Note that < is not necessarily the same as ⪇. A morphism R : (I, <) → (I′, <′) of CS-ISys_{0} is an approximable mapping R : I → I′ satisfying <; R; <′ = R, i.e. we have:

M(i) ΔRΔ.
M(ii) a ≤ bRb′ ≤ a′ ⇒ aRa′.
M(iii) aRb & aRc ⇒ aR(b ∧ c).
M(iv) <; R; <′ = R

When A ⊴ B as models, the inclusion morphism from A to B is defined by in(A, B) =<_{A}; <_{B}⊆ |A| × |B|, and projection morphism pr(B, A) : B → A is given by pr(B, A) =<_{B}; <_{A} and they satisfy:

in(A, B); pr(B, A) = <_{A} = Id(A), pr(B, A); in(A, B) ⊆ <_{B} = Id(B).

It was shown in [ES91a, Section 5.6] that (CS-ISys, ≤, ∧, <, Inc, ⊆) is an ω-complete information category. Since the extra axiom we have added here for the objects of the category is of universal-existential (u.e.) type, (CS-ISys_{0}, ≤, ∧, <, Inc, ⊆) is a directed complete information category: the lub of a directed set of objects ⟨A_{i}, ≤_{i}, ∧_{i}, Δ, <_{i}⟩_{i∈I} is simply their union (⋃ A_{i}, ⋃ ≤_{i}, ⋃ ∧_{i}, Δ, ⋃ <_{i}), and the lub of a directed set of morphisms is simply the union of the relations representing these morphisms.

We construct a pair of functors

CS-Dom <G ; _{F >} CS-ISys_{0}

which induce an equivalence of the two categories. For an object D of CS-Dom with associated relations and operations ⊑, ≪, ⊔ and ⊥, we put F (D) = (Q, ≤, ∧, ⊥, <), where Q is any base of D closed under existing binary joins and with no maximal element w.r.t. ≪, the pre-order ≤ is the inverse of ⊑, the operation ∧ is given by a ∧ b = a ⊔ b, and finally < is defined by a < b iff b ≪ a. For a Scott continuous map f : D → E, we define the approximable mapping R_{f} : F (D) → F (E) by aR_{f}b iff b ≪ f(a). In the other direction, for an object A = (|A|, ≤, ∧, Δ, <) of CS-ISys_{0}, we let G(A) = (Fil(A), ⊆) where Fil(A) is the set of filters of (|A|, <), i.e. upperclosed and co-directed subsets of |A|, ordered by inclusion. Note that if t is a filter and a ∈ t, then, by the definition of a filter, there exists a′ ∈ t with a′ < a; this means that we get the same set of filters, i.e. the same points, with or without axiom (x) above. For a morphism R : A → B of CS-ISys_{0}, we define G(R) = f_{R} : Fil(A) → Fil(B) by f_{R}(x) = {b | ∃a ∈ x. aRb}.

Proposition 6.1 (i) F and G are functors inducing an equivalence between CS-Dom and CS-ISys_{0}.

(ii) For x, y ∈ G(A), we have x ≪ y iff ∃a ∈ y. x ⊆ ↑ ↑a,

(iii) When A ⊴ B in CS-ISys_{0}, the pair of morphisms in(A, B) and pr(B, A) represent an embedding-projection pair in CS-Dom.

However (CS-ISys_{0}, ≤, ∧, <, Inc, ⊆) is not a continuous information category. We can see this by taking a simple object of this information category and show that there are not enough objects way below it in the category, i.e. the object cannot be approximated by objects way below it. The set, Q_{0} of rational numbers in (0, 1], with the usual strict ordering < and the extra proviso that 1 < 1, is clearly an object A_{0} = (Q_{0}, ≤, ∧, Δ, <) of this category, where x ∧ y is simply the smaller number between x and y and Δ = 1. If we identify x ∈ Q_{0} with the Scott open set ↑ ↑(1 − x) of the unit interval, it becomes clear that A_{0} in fact represents a countable basis of the unit interval with 1 representing the whole interval [0, 1]. We will prove that the carrier set of any object B way below A_{0} has at most two elements, one of which must of course be Δ = 1. For suppose |B| has elements p and q with, say, p < q < 1 and q ≠ 1. Then, since < is interpolative, there is a strictly decreasing sequence of elements r_{i} ∈ |J|, i ≥ 1 with p < r_{i} < q. This sequence, then, has a limit r ∈ ℝ (p ≤ r) with respect to the usual metric on the the real line. Let Q_{i} be the set of rational numbers in (0, 1] \ (r, r_{i}], and consider the objects A_{i} = (Q_{i}, ≤_{i}, ∧_{i}, Δ, <_{i}), i ≥ 1, where ≤_{i}, ∧_{i} and <_{i} are simply the restrictions of ≤, ∧ and < to Q_{i} respectively. We now have A_{0} = ⋃_{i} A_{i}, however there is no i ≥ 1 with B ⊴ A_{i} since r_{i} ∈ |B| and r_{i} ∉ |A_{i}|. This implies that B is not way below A and, therefore, proves our claim that CS-ISys_{0} is not a continuous I-category.

We will now show that a subcategory of CS-ISys_{0} gives rise to a continuous information category. This subcategory, denoted by CS-ISys_{1}, is equivalent to the category of continuous Scott domains with strict, continuous and open maps which, as a subcategory of CS-Dom, we denote by CS-Dom_{1}. In terms of solving domain equations effectively, confining ourselves to strict morphisms is not really a restriction, since the initial algebra theorem only holds in the subcategory of strict morphisms anyway. On the other hand, restricting to open maps, i.e. those preserving properties, is an essential requirement to obtain a (non-algebraic) continuous information category. CS-ISys_{1} is defined by adding the following to the axioms for morphisms of CS-ISys_{0}:

\begin{matrix}M(v) & ΔRb ⇒ b = Δ. \\ M(vi) & ∀a, a′∃b′∀b. [a′ < a ⇒ a′Rb′ & (aRb ⇒ b′ < b)]. \end{matrix}

Proposition 6.2 CS-ISys_{1} is equivalent to CS-Dom_{1}.

Proof Let R : A → B be a morphism of CS-ISys_{0} and let G(R) = f_{R} : D → E be its image in CS-Dom_{1} under the functor G. Since ⊥ = {Δ}, we have f_{R}({Δ}) = {Δ} iff M(v) holds, i.e. f_{R} is strict iff R satisfies M(v). Next suppose f_{R} is open and let a′ < a. By Proposition 2.10, f_{R} preserves the way below relation. Since < is interpolative, it is easy to see by Proposition 6.1(ii) that ↑ ↑a ≪ ↑ ↑a′ and hence f_{R}(↑ ↑a) ≪ f_{R}(↑ ↑a′). By definition of f_{R}, we therefore have:

{b | ∃a_{1}. a < a_{1} & a_{1}Rb} ≪ {b | ∃a_{1}. a′ < a_{1} & a_{1}Rb}.

Applying Proposition 6.1(ii) again, we conclude that there exists b′ ∈ f_{R}(↑ ↑a′) with f_{R}(↑ ↑a) ⊆ ↑ ↑b′, i.e. a′Rb′ & (aRb ⇒ b′ < b) as required. Assume now that M(vi) holds for R. We will prove that f_{R} preserves the way below relation and is therefore open by Proposition 2.10. Suppose then that x and y are in D with x ≪ y. By Proposition 6.1(ii), there exists a ∈ y such that x ⊆ ↑ ↑a. Since y is a filter, there exists a′ ∈ y with a′ < a. By M(vi), there is b′ with a′Rb′ (i.e. b′ ∈ f_{R}(y)) satisfying aRb ⇒ b′ < b. Now for any b ∈ f_{R}(x) there is a_{1} ∈ x with a_{1}Rb. Since a < a_{1}, we get aRb by M(iv) and hence b′ < b. Therefore f_{R}(x) ⊆ ↑ ↑b′ which implies f_{R}(x) ≪ f_{R}(y) as required. □

We can make CS-ISys_{1} into a continuous information category if we define inclusion morphisms such that they correspond to rigid embeddings. This can be done by stipulating that in a substructure relation between objects the principal filters w.r.t. < are also preserved. We therefore write the objects of CS-ISys_{1} as A = (|A|, ≤, ∧, Δ, <, ↑ ↑(−)), with

\begin{aligned}↑ ↑(−) : & |A| & ⟶ & P(|A|) \\ & a & ⟼ & \{a′ | a < a′\}, \end{aligned}

where P(S) is the powerset of the set S. Note that in the information categories formulated in [ES91b] all predicates and functions in an object are defined on the carrier set or its finite subsets. The finiteness was required there in order to obtain (ω-)algebraic information categories. Here on the other hand ↑ ↑(a) is in general an infinite subset of |A|. This is to be expected as we are dealing with a category of continuous posets which we want to represent simply as a continuous information category. In order to axiomatize the function ↑ ↑(−), we need the following axiom:

\begin{matrix}O(xi) & a < a′ ⇒ a′ ∈ ↑ ↑a. \\ O(xii) & a′ ∈ ↑ ↑a ⇒ a < a′. \end{matrix}

We will now show by a number of steps that C = (CS-ISys_{1}, ≤, ∧, ↑ ↑(−), Inc, =) is a continuous information category. Note that, since the homsets are discretely ordered, we have:

(R : A → B) ⊴^{m} (S : C → D) ⟺ A ⊴ C & B ⊴ D & ∀a ∈ |A|. R(a) = S(a);

where R(a) = {b | aRb}.

Proposition 6.3 (i) C is a directed complete information category.

(ii) (Obj_{C}, ≪^{o}) is a continuous poset.

(iii) Given morphisms R : A → B and S : C → D of C, we have R ≪^{m} S iff A ≪^{o} C & B ≪^{o} D.

(iv) (Mor, ≪^{m}) is a continuous poset.

Proof (i) Axioms O(i)-O(xii) and M(v) are of u.e. type and are therefore preserved in the union of any directed set of objects or morphisms. It is easy to see that M(vi) is also preserved: Let ⋃ R_{i} : ⋃ A_{i} → ⋃ B_{i} be the union of the directed set of morphisms ⟨R_{i} : A_{i} → B_{i}⟩_{i∈I} satisfying M(vi). Given a, a′ ∈ ⋃ A_{i}, there is i ∈ I with a, a′ ∈ A_{i}. Since R_{i} : A_{i} → B_{i} satisfies M(vi), there is b′ ∈ B_{i} with a′R_{i}b′ & (aR_{i}b ⇒ b′ < b). By the remark before the proposition, we have a(⋃ R_{i})b ⇒ aR_{i}b. We conclude that a′(⋃ R_{i})b′ & (a(⋃ R_{i})b ⇒ b′ < b) as required. (In fact since R(a) is preserved in a substructure relation, M(vi) can be rewritten in the u.e. form: ∀a, a′∃b′. [a′ < a ⇒ a′Rb′ & b′ < R(a)], where by b′ < R(a) we simply mean b′ < b for all b ∈ R(a).) This shows that we have a directed complete information category.

(ii) Let A = (|A|, ≤_{A}, ∧_{A}, Δ, <_{A}, ↑ ↑(−)_{A}) be an object of C. Consider the poset of the substructures of A ordered by ⊴. If A_{i}, i ∈ I, is a non-empty collection of substructures of A, then

⋀_{i} A_{i} = (| ⋀_{i} A_{i}| ≤, ∧, Δ, <, ↑ ↑(−))

where | ⋀_{i} A_{i}| = {a ∈ ⋂_{i} A_{i} | ∃a′ ∈ ⋂_{i} A_{i}. a′ <_{A} a} and ≤, ∧ ,< and ↑ ↑(−) are respectively the restrictions of ≤_{A}, ∧_{A}, <_{A} and ↑ ↑(−)_{A}) to | ⋀_{i} A_{i}. It is easy to see that ⋀_{i} A_{i} satisfies O(i)-(xii). As an example we will verify O(x). Given a ∈ | ⋀_{i} A_{i}| we know that a ∈ ⋂_{i} A_{i} and there is a′ ∈ ⋂_{i} A_{i} with a′ <_{A} a. Since <_{A} is interpolative (by O(viii)) there is b ∈ |A| with a′ <_{A} b <_{A} a. But then b ∈ ↑ ↑_{A}a′ = ↑ ↑_{A_{i}}a′ for each i ∈ I. Hence b ∈ | ⋀_{i} A_{i}| as required. Clearly ⋀_{i} A_{i} is the meet of A_{i}’s. Therefore the poset of the substructures of A is in fact a complete lattice. In particular it follows that if A_{i}, i ∈ I is a finite collection of structures way below A, then ⋁_{i} A_{i} is also way below A i.e. the set of objects way below A is directed. Now for any a ∈ |A| there is b ∈ |A| with b < a and the object with carrier set ↑ ↑b is way below A. It follows that A = ⋃{B | B ≪^{o} A}.

(iii) Suppose R ≪^{m} S. Then A ≪^{o} C, for if C = ⋁^{↑} C_{i} then putting S_{i} = in(C_{i}, C); S we get ⋁^{↑} S_{i} = S and hence R ⊴^{m} S_{i} for some i, i.e. A ⊴ C_{i}. Suppose now that D = ⋁^{↑} D_{i}. Let C_{i} = S^{−1}(D_{i}) = {x ∈ C | S(x) ⊆ D_{i}}. Then S^{−1}(D_{i}) ⊴ C and we claim that ⋁^{↑} C_{i} = C. For assume that x ∈ S^{−1}(D_{i}). Then there is y ∈ C with y ∈ C. By M(vi), there is z ∈ D, say z ∈ D_{i}, such that xSw implies z < w. Then x ∈ C_{i} which proves the claim. Now let S_{i} : C_{i} → D_{i} be defined by S_{i} = S ∩ (C_{i} × D_{i}). Then ⋃ S_{i} = S and hence there exists S_{i} with R ⊴^{m} S_{i}, i.e. B ⊴ D.

Suppose now that A ≪^{o} C, B ≪^{o} D and R ⊴^{m} S. Assume S ⊴^{m} ⋁^{↑}(S_{i} : C_{i} → D_{i}). Then C ⊴ bigvee^{↑}C_{i} and D ⋁^{↑} D_{i}. Take i with A ⊴ C_{i} and B ⊴ D_{i}. We have, R(x) = ⋁^{↑} S_{i}(x) = S_{i}(x), for all x ∈ A. Hence R ⊴^{m} S_{i}.

(iv) Similar to (i).

References

[Cut80] N. J. Cutland. Computability: An Introduction to Recursive function theory. Cambridge University Press, 1980.

[Eda89] A. Edalat. Categories of information systems. Master’s thesis, Imperial College, University of London, 1989.

[ES91a] A. Edalat and M. B. Smyth. Categories of information systems. In D. H. Pitt, P. L. Curien, S. Abramsky, A. M. Pitts, A. Poigne, and D. E. Rydeheard, editors, Category theory in computer science, pages 37–52. Springer-Verlag, 1991.

[ES91b] A. Edalat and M. B. Smyth. Categories of Information Systems. Technical Report Doc-91-21, Imperial College, London, 1991. submitted to Theoretical computing science.

[GHK^{+}80] G. Gierz, K. H. Hofmann, K. Keimel, J. D. Lawson, M. Mislove, and D. S. Scott. A Compendium of Continuous Lattices. Springer Verlag, Berlin, 1980.

[JJ82] P. T. Johnstone and A. Joyal. Continuous categories and exponentiable toposes. J. Pure Appl. Algebra, 25:255–296, 1982.

[Joh81] P. T. Johnstone. Injective toposes. In Continuous lattices, pages 284–297. Springer, Berlin, 1981. Lecture Notes in Math. No. 871.

[Joh82] P. T. Johnstone. Stone Spaces, volume 3 of Cambridge Studies in Advanced Mathematics. Cambridge University Press, Cambridge, 1982.

[Jun88] A. Jung. Cartesian Closed Categories of Domains. PhD thesis, Technische Hochschule Darmstadt, 1988.

[LS86] J. Lambek and P. J. Scott. Introduction to Higher Order Categorical Logic. Cambridge Studies in Advanced Mathematics Vol. 7. Cambridge University Press, 1986.

[LW84] K. G. Larsen and G. Winskel. Using information systems to solve recursive domain equations effectively. In D. B. MacQueen G. Kahn and G. Plotkin, editors, Semantics of Data Types, pages 109–130, Berlin, 1984. Springer-Verlag. Lecture Notes in Computer Science Vol. 173.

[Plo81] G. D. Plotkin. Post-graduate lecture notes in advanced domain theory (incorporating the “Pisa Notes”). Dept. of Computer Science, Univ. of Edinburgh, 1981.

[Smy77] M. B. Smyth. Effectively given domains. Theoretical Computer Science, 5:257–274, 1977.

[Smy89] M. M. Smyth. Private Communication, 1989.

[Tan74] A. Tang. Recursion theory and descriptive set theory in effectively given T_{0} spaces. PhD thesis, University of Princeton, 1974.