Self duality in information categories

Abbas Edalat

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

November 5, 1991

Abstract

We define PI-categories by enriching the notion of I-category (information category) such that every inclusion morphism has a right adjoint or projection. As a result of having proper adjunctions, rather than simply projection-embeddings, PI-categories become closed under taking the Karoubi envelope. A strict PI-category, one whose morphisms are all strict, has the self dual property that its opposite is again a strict PI-category. This implies that these categories are, in Freyd’s terminology, algebraicly compact wrt standard and continuous endofunctors, in the sense that every such endofunctor has an invariant object which is simultaneously an initial algebra and a final co-algebra. We show that the continuity of the functor on the cpo of objects is sufficient for this result. A simple characterisation of minimal invariant objects of contravariant and mixed functors on PI-categories is given and we also obtain an effective version of the theory for ω-algebraic PI-categories. We present a number of examples and establish that categories of information systems for various domains (SFP, Scott domains, continuous Scott domains, etc.), are all PI-categories and we show in these categories how the substructure relation on objects can be weakened to obtain proper adjunctions between objects.

1 Introduction

I-categories, and their concrete instance Information categories, were introduced in [ES91a, ES91b] to generalise the work in [BC81, Sco81, LW84] on solving domain equations by constructing a cpo of information systems. The class of inclusion morphisms of an I-category induces a partial order ⊴ on objects and a partial order ⊴^{m} on morphisms of the category. In a complete I-category, these partial orders become cpo’s and it was shown that any ω−chain of inclusions has a colimit, and any endofunctor that is standard (i.e. preserves inclusion morphisms) and continuous on the cpo of morphisms of such a category has an initial algebra in the subcategory of strict (i.e. bottom preserving) morphisms.

A major class of examples captured by information categories consists of categories of information systems for various domains, and it is well known that in a category of domains an ω-chain of embedding-projections has a bilimit, i.e. an object which is at the same time a colimit wrt the chain of embeddings and a limit wrt the chain of projections. This so called coincidence of limits and colimits was first remarked in [Sco72] and was discussed in the general setting of O-categories in [SP82]. By the equivalence of categories of domains and information systems, we expect a similar property for categories of information systems. In fact, for information systems A and B the usual substructure relation A ⊴ B implies the existence of a projection morphism from B to A as well as an inclusion morphism from A to B. This leads us to the notion of a PI-category as an I-category with projections, and in the general theory it is in fact sufficient to require that an inclusion-projection pair forms an adjunction (a Galois connection). All categories of information systems for domains, constructed by us and other authors, e.g. in [ES91b, Hoo91, LW84, Zha89] will then be examples of a complete PI-category. This is also true of Abramsky’s category of SFP pre-locales in [Abr91].

We will show that the substructure relation, A ⊴ B, between objects in these categories can in fact be weakened to obtain proper adjunctions between the corresponding information systems. This is done by replacing the condition ⊢_{A} = ⊢_{B} ∩(|A| × |A|) by the weaker requirement ⊢_{A} ⊆ ⊢_{B}. In terms of logic, this means that the extension is not necessarily conservative any more. In terms of information, it means that positive information is still preserved but, in general, not negative information, i.e. a ⊬_{A} a′ ⇒ a ⊬_{B} a′ does not hold any more. All the basic constructors on information systems preserve this weaker notion of substructure relation and the solution of domain equations remain unchanged. The advantage of working with the weaker notion and hence with all adjunctions is that the Karoubi envelope of the category will be another PI-category and every standard and continuous endofunctor on the category will induce a standard and continuous endofunctor on the Karoubi envelope. This makes the task of solving domain equations over the categories of continuous domains which are retracts of algebraic ones particularly simple.

A strict PI-category, i.e. one whose morphisms are strict, has the self dual property that its opposite is also a strict PI-category. The inclusions (projections) in the opposite category are the projections (inclusions) of the original category considered as arrows in the opposite category. Furthermore, the cpo’s of objects and morphisms of the opposite category will be isomorphic to the corresponding cpo’s of the original category. This implies that any standard and continuous endofunctor on a strict PI-category gives rise to a standard and continuous endofunctor on the opposite category. A number of results follow from this self-duality.

The first immediate result is the coincidence of limits and colimits of ω-chains of inclusion-projection pairs as discussed above. Another result is the coincidence of the initial algebra and the final co-algebra for standard and continuous endofunctors. For locally continuous endofunctors on O-categories, this coincidence follows from the basic lemma and Theorem 2 in [SP82]. In his recent work on algebraicly complete and algebraicly compact categoies [Fre91a, Fre91b], Freyd defines an endofunctor on a category to be algebraiclly bounded if it has an initial algebra and a final co-algebra which are canonically isomorhic, and he proves a number of general results about them. Of course for PI-categories this coincidence follows directly from self duality and an effective version of the proofs can also be obtained in a simple way. In Freyd’s terminology, strict PI-categories become algebraicly compact wrt standard and continuous endofunctors. In this work, we will also show that the continuity of the functor on the cpo of objects of a complete I-category is all that is needed to obtain the initial algebra theorem, thereby improving the result in [ES91a] which assumes its continuity on the cpo of morphisms.

Another consequence of self duality is that, following Freyd in his above cited notes, we can define the minimal invariant object of a contravariant endofunctor F on a strict PI-category K. As explained in Section 3.2, we do this by considering an induced covariant functor F̂ on the strict PI-category K × K^{op}. The initial algebra/final co-algebra of F̂ then gives us the desired minimal invariant object D of F itself, with F (D) = D, which is characterised by the property that it has only one endomorphism k : D → D satisfying F (k) = k. Mixed endofunctors can be treated in a similar way; for example the minimal invariant object D of a bifunctor F : K^{op} × K → K satisfies F (D, D) = D and is characterised by the property that it has only one endomorphism k : D → D, with F (k, k) = k. The upshot of this for categories of information systems is that we can use the function space constructor, which is contravariant in the first argument and covariant in the second, in solving domain equations. Note that in [ES91b], we followed the work in [SP82] and dealt with the function space constructor by restricting it to the subcategory of inclusions to obtain a covariant functor. Self duality in strict PI-categories now allows us to obtain a minimal invariant object in the relevant sense for the function space constructor on the category as a whole. In particular, we obtain a characterisation of the solution of D ≅ (D → D)_{⊥} which gives us a model of the untyped λ−calculus.

2 Basics

2.1 I-categories

Recall from [ES91a] that an I-category is a four tuple (K, Inc, ⊑, Δ) where

• K is a category with ordered hom-sets,

• Inc ⊆ Mor is the subclass of inclusion morphisms of K such that in each hom-set, hom(A, B), there is at most one inclusion morphism which we denote by in(A, B) or A ↣ B,

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

• Δ ∈ Obj is a distinguished object,

which satisfy the following two axioms:

Ax 1 (i) The class of objects Obj and the inclusion morphisms Inc form a partial order represented as a category.

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

Ax 2 Composition of morphisms is monotone with respect to the partial order on hom-sets, i.e.

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

whenever the compositions are defined.

Note that we have dropped from the definition of I-category the axiom which makes inclusion morphisms monomorphisms, i.e. we no longer require 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. This axiom was not needed to obtain the general result, i.e. the initial algebra theorem, in [ES91a] and in fact there are categories in which inclusions are not monomorphisms. Therefore, we are justified in dropping it in the definition of I-category to obtain a more general theory.

The partial orders ⊴ on Obj and ⊴^{m} on Mor are defined as follows:

• A ⊴ B if in(A, B) exists;

• f ⊴^{m} g if the diagram

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

weakly commutes, i.e. if

(i) dom(f) ⊴ dom(g),

(ii) cod(f) ⊴ cod(g),

(iii) f; in(cod(f), cod(g)) ⊑ in(dom(f), dom(g)); g.

A complete I-category further satisfies:

Ax 3 (Mor, ⊴^{m}) is a cpo.

Ax 4 (Inc, ⊴^{m}) is a subcpo of (Mor, ⊴^{m}).

Ax 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≥0} and ⟨g_{i}⟩_{i≥0} are increasing chains in (Mor, ⊴^{m}) with cod(f_{i}) = dom(f_{i}), for all i ≥ 0.

Recall that if P is any category, the Karoubi envelope K(P) of P has as objects the pairs (A, r) where A is an object of P and r : A → A is a retraction (that is, r; r = r), while a morphism from (A, r) to (B, s) is a morphism f : A → B of P such that r; f = f; s = f. Suppose P is an I-category, then the hom-sets of K(P) are ordered by the order induced from P and we can define inclusion morphisms in K(P) by putting (A, r) ⊴ (B, s) iff A ⊴ B and r ⊴^{m} s, with in((A, r), (B, s)) = r; in(A, B); s. We furthermore take (Δ, Id(Δ)) as the distinguished object of K(P) and obtain the following result, which was stated in [ES91a] in the particular case when P is the category of bounded complete information systems.

Proposition 2.1 If P is a (complete) I-category, then so is K(P).

Proof It is routine to check that if P is an I-category, so is K(P). To verify that K(P) is complete if P is complete, we show that if f : (A, r) → (A′, r′) and g : (B, s) → (B′, s′), with r; f = f; r′ = f and s; g = g; s = g, are morphisms of K(P), and if (A, r) ⊴ (B, s) and (A′, r′) ⊴ (B′, s′), then f ⊴^{m} g iff f ⊴_{K}^{m} g, where ⊴_{K}^{m} denotes the global partial order in K(P). Putting e = in(A, B) and e′ = in(A′, B′), by assumption we have r; e ⊑ e; s and r′; e′ ⊑ e′; s′. Therefore

f ⊴^{m} g ⇒ f; e′ ⊑ e; g ⇒
f; r′; e′; s′ = r; f; e′; s′ ⊑ r; e; g; s′ ⊑ r; e; s; g ⇒ f ⊴_{K}^{m} g

and

f ⊴_{K}^{m} g ⇒ f; r′; e′; s′ ⊑ r; e; s; g ⇒

f; e′ = f; r′; r′; e′ ⊑ f; r′; e′; s′ ⊑ r; e; s; g ⊑ e; s; s; g = e; g ⇒ f ⊴^{m} g.

The proof now follows easily. □

Finally, an ω-algebraic I-category is defined by also requiring that:

Ax 6 (Mor, ⊴^{m}) is ω-algebraic.

Ax 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) The composition of compact morphisms is compact.

2.2 PI-categories

Let K be an I-category and suppose A and B are objects with A ⊴ B. We say that the inclusion morphism in(A, B) has a right adjoint or projection if there exists a morphism pr(B, A) : B → A such that

in(A, B); pr(B, A) ⊒ Id(A) pr(B, A); in(A, B) ⊑ Id(B).

It is easy to see that a projection morphism, if it exists, is uniquely determined by the inclusion. Furthermore, the inclusion and projection morphisms induce an adjunction (a Galois connecton) (e, p) between hom(A, A) and hom(B, B) where

e : f ⟼ pr(B, A); f; in(A, B)  p : g ⟼ in(A, B); g; pr(B, A).

If an inclusion-projection pair satisfies the stronger condition that in(A, B); pr(B, A) = Id(A), then it is easy to see that we get

f; in(A, B) ⊑ g; in(A, B) ⇒ f ⊑ g,
pr(B, A); f ⊑ pr(B, A); g ⇒ f ⊑ g;

in particular the inclusion becomes a monomorphism and the projection an epimorphism, and, in this case, we call the inclusion an embedding.

Definition 2.2 A PI-category is an I-category such that every inclusion has a right adjoint and Δ is a terminal object.

We denote a PI-category as P = (P, Inc, Pr, ⊑, Δ), where Pr is the class of projections. Clearly the subcategories (Obj,Inc) and (Obj,Pr) are dual to each other. Work in information systems, e.g. in [LW84, Zha89, Abr91], has so far been with embedding-projections rather than the bigger class of proper adjunctions. However, Gunter does deal with adunctions in the context of domains in his thesis [Gun85]. We will shortly see the advantage of working with adunctions when we consider the Karoubi envelope of a PI-category. But before that we look at an example.

2.3 ISys

Consider the category of (Scott) information systems ISys as in [LW84, Sco82]. Objects are of the form A = (|A|, ⊢, Con), where |A| is a set of tokens, Con ⊆ P_{fin} is the set of consistent tokens and ⊢⊆ P_{fin} × P_{fin} is an entailment relation and the following axioms hold:

X ⊆ Y & Y ∈ Con ⇒ X ∈ Con
a ∈ |A| ⇒ {a} ∈ Con
X ⊢ Y ⇒ X ∈ Con_{A} & Y ∈ Con_{B}
X ⊢ Y ⇒ X ∪ Y ∈ Con_{B}
X ∈ Con & Y ⊆ X ⇒ X ⊢ Y
X ⊢ Y & Y ⊢ Z ⇒ X ⊢ Z.

A morphism, called an approximable mapping, r : A → B between two objects is a relation r ⊆ Pf(|A|) × Pf(|B|) satisfying:

XrY ⇒ X ∈ Con_{A} & Y ∈ Con_{B}
∅r∅
XrY & XrY′ ⇒ Xr(Y ∪ Y′)
X′ ⊢_{A} X & XrY & Y ⊢_{B} Y′ ⇒ X′rY′

The identity morphism on A is the relation ⊢. An object A is said to be a substructure of object B, written A ⊴ B, if s(i) |A| ⊆ |B|.

s(ii) ⊢_{A}=⊢_{B} ∩(|A| × |A|).

s(iii) Con_{A} = Con_{B} ∩ P_{fin}(A).

This is in fact how the substructure relation is defined in [LW84]. If A ⊴ B, then we have an inclusion and a projection morphism given by

X(in(A, B))Y ⟺ X ⊢_{B} Y Y (pr(B, A))X ⟺ Y ⊢_{B} X,

and an easy calculation shows that in(A, B); pr(B, A) = Id(A) and pr(B, A); in(A, B) ⊑ Id(B). ISys is then a PI-category with embeddings and with distinguished object (∅, {(∅, ∅)}, {∅}).

2.4 ISys with weak substructure relations

We can also define a weaker form of the substructure relation in ISys to obtain proper adjunctions. In detail, we say A is a weak substructure of B if the conditions s(i) and s(iii) above hold and s(ii) is replaced by the weaker condition ⊢_{A}⊆⊢_{B}. Defining the inclusion and projection as before, we can show that they are in fact morphisms which satisfy: in(A, B); pr(B, A) ⊇ Id(A) and pr(B, A); in(A, B) ⊑ Id(B). We also note that any pair of adjunction between Scott domains can be captured in ISys in the above manner. To see this, let (D, ⊑) and (E, ⊑) be Scott domains and let the continuous maps e : D → E and p : E → D form an adjunction with e left adjoint to p. Then e preserves compact points, but it is not necessarily one to one. Let e_{0} : K_{D} → K_{E} denote the restriction of e to K_{D}. We represent D as usual by (K_{D}, ⊢_{D}, Con_{D}), where K_{D} is the set of compact points of D, the relation X ⊢_{D} Y holds iff the lub of elements of X is above that of Y, and Con_{D} is the set of finite consistent subsets of K_{D}. Next we consider K_{E} from which we define a new set of tokens K_{E}^{+} representing E. This is done by replacing every element a ∈ K_{E} which is in the image of e_{0} by all tokens in the set e_{0}^{−1}(a), i.e. K_{E}^{+} is the smallest set A satisfying:

e_{0}^{−1}(a) ⊆ A if a ∈ Im(e_{0})
a ∈ A  otherwise.

The set K_{E}^{+} gives us a representation (K_{E}^{+}, ⊢_{E}, Con_{E}) of E in which all tokens in e_{0}^{−1}(a) are equivalent for each a ∈ Im(e_{0}). Furthermore substructure relation as the notion of approximation of objects provides us with a bigger class of inclusion-projection pairs in ISys. See the last section for more examples.

2.5 Basic properties of PI-categories

Proposition 2.3 The Karoubi envelope K(P) of a PI-category P is a PI-category. Furthermore, if P has embedding-projections, then the full subcategory of K(P) consisting of projections has also embedding-projectios.

Proof Suppose P is a PI-category. If (A, r) ⊴ (B, s), i.e. A ⊴ B and r ⊴^{m} s, with e = in(A, B) and p = pr(B, A), then as before we define the corresponding inclusion and projection in K(P) by e_{K} = r; e; s and p_{K} = s; p; r respectively. We check this gives us an inclusion-projection pair:

e_{K}; p_{K} = r; e; s; s; p; r = r; e; s; p; r ⊑ r; r; e; p; r = r; e; p; r ⊑ r; r = r = Id((A, r));
p_{K}; e_{K} = s; p; r; r; e; s = s; p; r; e; s ⊑ s; p; e; s; s = s; p; e; s ⊑ s; s = s = Id((B, s)).

Furthermore if s is a projection, i.e. s ⊑ Id(B), and e; p = Id(A), we also get e_{K}; p_{K} = r; e; s; p; r ⊑ r; e; p; r = r = Id((A, r)), which together with the first equation above implies that e_{K} is an embedding. Finally, it is clear that (Δ, Id(Δ)) is a terminal object of K(P). □

Recall that a morphism f : A → B of an I-category is strict if the diagram

A

∧

∧ [figure: f]
Δ \underline{>}  \overline{>} B

commutes. We say that an I-category is strict if all its morphisms are strict. Clearly an I-category is strict iff Δ is an initial object. For an I-category K, we denote its strict subcategory, i.e. the subcategory of strict morphisms, by K^{s}.

Proposition 2.4 Projection morphisms are strict.

Proof Let A ⊴ B. We have

in(Δ, A) ⊑ in(Δ, A); in(A, B); pr(B, A) ⇒ in(Δ, A) ⊑ in(Δ, B); pr(B, A).

The reverse inequality of course holds by Ax1(ii). □

It therefore follows that if K is a PI-category, K^{s} is also a PI-category in which Δ is a zero object i.e. both initial and terminal. We say that a PI-category is complete if it is complete as an I-category.

Proposition 2.5 If K is a complete I-category, then (Pr, ⊴^{m}) is a subcpo of (Mor, ⊴^{m}).

Proof Let pr(B_{1}, A_{1}) ⊴^{m} pr(B_{2}, A_{2}) … be an increasing chain of projections. it can easily be checked that ⨆_{i} pr(B_{i}, A_{i}) = pr(⨆_{i} B_{i}, ⨆_{i} A_{i}) by showing that the right hand side satisfies the required equations with in(⨆_{i} A_{i}, ⨆_{i} B_{i}). For example we have (in(⨆_{i} A_{i}, ⨆_{i} B_{i})); (⨆_{i} pr(B_{i}, A_{i})) = (⨆_{i} in(A_{i}, B_{i})); (⨆_{i} pr(B_{i}, A_{i})) = ⨆_{i}((in(A_{i}, B_{i})); (pr(B_{i}, A_{i}))) ⊒ ⨆_{i} Id(A_{i}). The other equation follows in a similar way. □

A PI-category is said to be ω-algebraic if it is ω-algebraic as an I-category and also satisfies the following property (which corresponds to Ax7(ii)):

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

As with I-categories, we can complete a PI-category to obtain an algebraic PI-category as in the following definition. We denote the set of ideals of a poset L by \overline{L}.

Definition 2.6 For a countable PI-category P = (P, Inc, Pr, ⊑, Δ), its PI-completion, \overline{K} = (\overline{K}, \overline{Inc}, \overline{Pr}, ⊆, \overline{Δ}) is given by:

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

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

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 in the latter equation that cod(F) = dom(G), f, g are composable and denoting the downward closure of S by ↓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},
pr(B, A) = ↓{pr(B, A) | A ∈ A, B ∈ B, A ⊴ B};

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

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

Since K is an I-category, we know that \overline{K} is an ω-algebraic I-category, in which the compact objects and morphisms are precisely the principle ideals of (Obj, ⊴) and (Mor, ⊴^{m}) respectively [ES91b, page 14]. But we can say more:

Proposition 2.7 \overline{K} is an ω-algebraic PI-category.

Proof Let A ⊆ B. Then

pr(B, A); in(A, B) = ↓{pr(B, A); in(A, B)|A ∈ A, B ∈ B, A ⊴ B}
⊆ ↓{Id(B)|B ∈ B} = Id(B).

The other inequality holds in a similar way. Suppose now that F : A → {Δ}, then each f ∈ F is of the form (f : A → Δ) ⊑ pr(A, Δ) for some A ∈ A. Therefore F = pr(A, \overline{Δ}) and \overline{Δ} is terminal. Next suppose ↓A and ↓B, with A, B ∈ Obj_{K}, are compact elements of (Obj\overline{K}, \overline{⊴}) with ↓A ⊆ ↓B, then A ⊴ B and, by definition of projections in \overline{K}, pr(↓B, ↓A) = ↓pr(B, A) which is compact. □

As in the case of I-categories, we define the base of an ω-algebraic PI-category K to be the subcategory K^{b} of compact objects and morphisms of K. Then we have:

Proposition 2.8 If K is an ω-algebraic PI-category, then K is isomorphic to \overline{K^{b}}.

3 Self dual property of strict PI-categories.

We will now show the interesting result that the opposite of any strict PI-category is itself a strict PI-category. Let K = (K, Inc, Pr, ⊑, Δ) be a strict PI-category. We know that Δ is both an initial and a final object. By switching inclusions and projections, we can make K^{op} into a PI-category. First, we need a lemma.

Lemma 3.1 (f : A → B) ⊴^{m} (g : C → D) iff the diagram

C  \overline{g} \overline{}D |  |
| ; ∨ ∨  ⊑  | ; ∨ ∨
A  \overline{f} \overline{}B

weakly commutes, i.e. if

(i) A ⊴ C,

(ii) B ⊴ D,

(iii) pr(C, A); f ⊑ g; pr(D, B).

Proof Suppose f; in(B, D) ⊑ in(A, C); g. Composing both sides with pr(C, A) from the left and pr(D, B) from the right and then using the inequalities for inclusion-projections, we get pr(C, A); f ⊑ g; pr(D, B). Similarly if pr(C, A); f ⊑ g; pr(D, B)., we compose both sides with the corresponding inclusions to obtain f; in(B, D) ⊑ in(A, C); g. □

Now consider K^{op}. For clarity, we denote by f_{op} the arrow in K^{op} represented by the arrow f of K. Furthermore, the composition of arrows f ∈ hom_{K^{op}}(A, B) and g ∈ hom_{K^{op}}(B, C) will be written as f ∗ g. The hom-sets of K^{op} inherit the order from K, i.e. we put f_{op} ⊑ g_{op} if f ⊑ g. We also let Inc^{op}, the inclusion morphisms of K^{op}, be Pr, the projection morphisms of K considered as arrows in K^{op} and we denote the inclusion morphism from A to B in K^{op} by in_{op}(A, B), i.e. we define in_{op}(A, B) = (pr(B, A))_{op} whenever A ⊴ B in K; similarly we let Pr^{op} be Inc considered as arrows in K^{op}, i.e. pr_{op}(B, A) = (in(A, B))_{op} whenever A ⊴ B in K.

Proposition 3.2 K^{op} = (K^{op}, Inc^{op}, Pr^{op}, ⊑, Δ) is a strict PI-category. If the inclusions of K are embeddings, so are those of K^{op}.

Proof Since Δ is an initial object of K^{op}, Ax 1(ii) holds trivially and we only need to check the inclusion-projection equations. If A ⊴ B in K, then

in_{op}(A, B) ∗ pr_{op}(B, A) = (pr(B, A))_{op} ∗ (in(A, B))_{op} = (in(A, B); pr(B, A))_{op} ⊒ Id(A),

and if equality holds in K it holds in K^{op} as well. Similarly we have pr_{op}(B, A) ∗ in_{op}(A, B) ⊑ Id(B). □

Clearly, we have A ⊴ B in K iff A ⊴_{op} B in K^{op}. The same holds for the global partial order ⊴^{m} on morphisms:

Proposition 3.3 f ⊴^{m} g iff f_{op} ⊴_{op}^{m} g_{op}.

Proof Suppose f ∈ hom_{K}(A, B) and g ∈ hom_{K}(C, D), with A ⊴ C and B ⊴ D. Then

f; in(B, D) ⊑ in(A, C); g ⟺ pr(C, A); f ⊑ g; pr(D, B) (by the lemma) ⟺

f_{op} ∗ in_{op}(A, C) ⊑ in_{op}(B, D) ∗ g

from which the result follows. □

All this says that the contravariant functor from K to K^{op} which acts as identity on objects and sends f ∈ hom_{K}(A, B) to f_{op} ∈ hom_{K^{op}}(B, A) induces an isomorphism between the partial orders (Obj_{K}, ⊴_{K}) and (Obj_{K^{op}}, ⊴_{K^{op}}) and one between (Mor_{K}, ⊴_{K}^{m}) and (Mor_{K^{op}}, ⊴_{K^{op}}). We have also proved the following theorem.

Theorem 3.4 If K is a (complete, ω-algebraic) strict PI-category, so is K^{op}.

Therefore, for any categorical property true of strict PI-categories, the dual property also holds for them. As the first application of duality we have the following result on the coincidence of limits and colimits.

Theorem 3.5 The lub of any increasing chain of objects in a complete PI-category K is a bi-limit of the chain, i.e. it is the colimit of the chain of inclusions and also the limit of the corresponding chain of projections in K. It is also a bi-limit of the chain in K^{s}.

Proof We know from [ES91b] that the lub D = ⨆ D_{i} of the chain

D_{0} ↣ D_{1} ↣ D_{2} ↣ …

is the colimit of the chain of inclusions in K and also in K^{s}. The same is true in K^{op}, i.e. D is the colimit of the chain of inclusions

D_{0} ↣_{op} D_{1} ↣_{op}↣_{op} D_{2} ↣_{op} …

in K^{op} and in K^{op^{s}}, but this implies that D is the limit of the corresponding chain of projections

D_{0} ↞ D_{1} ↞ D_{2} ↞ …

in K and in K^{s}. □

3.1 Coincidence of initial algebras and final co-algebras

Another interesting consequence of self-duality is the coincidence of initial algebra and final coalgebra of endofunctors on strict PI-categories. Recall that a functor F : K → K′ between I-categories is standard if it preserves the order of hom-sets and the inclusion morphisms; when K and K′ are complete, F is said to be continuous on objects (respectively on morphisms) if the induced map on objects F_{o} : (Obj_{K}, ⊴) → (Obj_{K′}, ⊴) (respectively the induced map on morphisms F_{m} : (Mor_{K}, ⊴^{m}) → (Mor_{K′}, ⊴^{m})) is (Scott) continuous. Suppose now that K and K′ are PI-categories and F is standard. It then follows from the uniqueness property of projections that F preserves projections as well: If (i, p) is an inclusion-projection pair between objects A and B in K, then F (i) is an inclusion and from i; p ⊒ Id(A) and p; i ⊑ Id(B) we get F (i); F (p) ⊒ Id(F (A)) and F (p); F (i) ⊑ Id(F (B)), which imply that F (p) is the projection associated with F (i). Assume now that K is a complete and strict PI-category and F : K → K is a standard endofunctor. Then we have a standard endofunctor F^{op} : K^{op} → K^{op} defined by F^{op}(f_{op}) = (F (f))_{op}, and by Proposition 3.3 we immediately get the following:

Proposition 3.6 F is continuous on objects (morphisms) iff F^{op} is so.

Recall that given an endofunctor F : C → C on a category C, the category of F -algebras has as objects the pairs (A, f), with A ∈ Obj_{C} and f ∈ hom(F (A), A), and as morphisms, between objects (A, f) and (B, g), those h ∈ hom(A, B) for which the following diagram:

[figure: A; f; F (A); h; F (h); B; g; F (B)]

commutes. An initial algebra, of F is defined to be an initial object, if it exists, of the category of F -algebras; if (A, f) is an initial algebra, f will necessarily be an isomorphism and we say that F has an initial algebra in C. Dually, we have the notions of co-algebra and final co-algebra. If C is a poset and F : C → C a monotonic function, then the initial algebra of F will be its least fixed point and the final co-algebra its greatest fixed point. This is why an initial algebra is also called a least fixed point and a final co-algebra a greatest fixed point. If an endofunctor F has an initial algebra (A, f) and a final co-algebra (B, g) which are isomorphic, i.e. A ≅ B, then up to isomorphism F has a unique invariant object. The self-duality of strict PI-categories allows us to deduce an immediate result on this coincidence as follows.

Suppose that K is a complete PI-category and F : K → K is is standard and continuous on morphisms. We know from [ES91a, page 45] that F has an initial algebra (D, Id(D)) in K^{s}, which is in fact given by D = ⨆_{i≥0} F^{i}(D). By the above proposition (D, Id(D)) is also an initial algebra of F^{op} in K^{op^{s}}, but this means that (D, Id(D)) is a final co-algebra of F in K^{s}. We have therefore proved that a standard and morphism-continuous endofunctor F on a complete and strict PI-category has an invariant object D = F (D) such that (D, Id(D)) is both an initial algebra and a final co-algebra of F. In the terminology of Freyd in [Fre91a, Fre91b], we can say that standard and morphism-continuous endofunctors on such categories are totally bounded. This result can be strenghtened by only requiring the continuiuty of the functors on objects. In fact the initial algebra theorem can be stated and proved easily as follows.

Theorem 3.7 Let K be a complete I-category and F a standard and object-continuous endofunctor. Then F has an initial algebra in K^{s}.

Proof Recall that Δ is the initial object in K^{s}. Let T be the chain

Δ ↣ F (Δ) ↣ F^{2}(Δ) ↣ …

and put D = ⨆_{i} F^{i}(Δ). We know from [ES91a, Proposition ] that s : T → D, with s_{i} = in(F^{i}(Δ), D) is a colimiting cone, and so is F (s) : F (T) → F (D). Therefore the conditions of the basic lemma in [SP82, page 765] are satisfied and, hence, the initial F-algebra exists in K^{s} and is given by (D, α), where α : F (D) → D is the mediating morphism from F (T) to T. Clearly we have F (D) = D and α = Id(D). □

Since in a PI-category Δ is the terminal object, by duality we obtain the following.

Theorem 3.8 Let K be a PI-category and F a standard and object-continuous functor. Then F has an invariant object D = F (D), such that (D, Id(D) is an initial algebra in K^{s} and a final co-algebra in K.

3.2 Minimal objects of contravariant and mixed functors

We can use the method developed in [Fre91a] to obtain minimal objects of contravariant and mixed functors on complete and strict PI-categories. We start by noting that in a category with a zero object, any zero object is characterised by the property that it has only one endomorphism. In particular, given a (covariant) endofunctor F on a strict PI-category, the object D = ⨆ F^{i}(D) which is both an initial algebra and a final co-algebra is a zero object of the category of invariant objects of F and hence it is characterised by the property that it has only one invariant enomorphism. Now let F : K → K be a contravariant functor on a strict PI-category. Consider the covariant functor F̂ : K^{op} × K → K^{op} × K defined by F̂(A, B) = (F (B), F (A)) and F̂(f, g) = (F (g), F (f)). The functor F̂ has the invariant object (D, D), with D = ⨆_{i} F^{i}(Δ), such that ((D, D), (Id(D), Id(D))) is both an initial algebra and a final co-algebra. Hence, by the above remark, (D, D) has only one invariant endomorphism (k, l), i.e. only one such pair with F (k) = l and F (l) = k. Since the same thing can be said about (l, k), we have l = k. This means that D as an invariant object of F is charachterized by the property that it has only one invariant endomorphism, i.e. only one morphism k : D → D, namely Id(D), with F (k) = k. Mixed endofunctors can be treated in a similar way.

Suppose F : K^{op} × K → K is a bifunctor on a strict PI-category contravariant in its first argument and covariant in the second. By considering the covariant functor F̂ : K^{op} × K → K^{op} × K with F̂(A, B) = (F (B, A), F (A, B)), we obtain an invariant object D = ⨆ F̂^{i}(Δ, Δ), satisfying F (D, D) = D, and characterised among invariant objects of F by the property that it has only one invariant endomorphism, i.e. only one morphism k : D → D with F (k, k) = k.

4 Effectiveness

We can construct an effective theory for PI-categories similar to the case of I-categories by simply adding an extra recursive predicate for projections as follows. See [ES91a] for the background. Let K be an ω-algebraic PI-category. An enumeration (A, f) of the base of K is given by an enumeration A : ℕ → Obj_{K^{b}} and an enumeration f : ℕ → Mor_{K^{b}} of its compact objects and morphisms (i.e. objects and morphisms of K^{b}) respectively. K is said to be effectively given with respect to (A, f) by index ⟨a, r, s, t, u, v, x, w⟩ if the following six 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} = pr(A_{l}, A_{p}) is recursive in n, l and p with index x;

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

R5 is the extra condition we have added here. As in the case of inclusions we now have the following property for projections.

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

We then obtain the effective version of the co-final algebra theorem:

Theorem 4.2 Let F be a computable endofunctor on K with a co-final algebra D = F (D). If (E, k) is a computable F -algebra, the unique morphism h : E → D satisfying h = k; F (h) is computable and an index for h can be effectively obtained from one for F and one for (E, k).

5 Information categories with projections

The notion of information category, which was introduced in [ES91b] as a concrete instance of an I-category can be enriched to become a PI-category. Recall that in an information category, objects are weak second order stuctures and the partial ordrer on objects corresponds to the substructure relation between objects; morphisms are relations between elements or finite subsets of the carrier sets of objects and the identity morphism is necessarily a transitive and interpolative relation, and in most examples it is at least a pre-order. In order to obtain a PI-catgory, we need to introduce projections which must satisfy a couple of axioms. In the following definition the C clauses are those of an information category and the extra D clauses are the new projection axioms.

Definition 5.1 An information category with projections, (C, <, T^{i}, f^{j}, Inc, Pr, ⊆, Δ), (i ∈ I, j ∈ J, where I, J are indexing sets), is a category C with the following properties:

• Objects of C are weak second order structures of fixed signature of the form A = (|A|, <_{A}, T_{A}^{i}, f_{A}^{j}), where <_{A} is a transitive-interpolative order on |A| (or Pf(|A|)) and the elements of |A| are from a fixed alphabet.

• Morphisms of C are relations between elements (or finite sets) of the objects with the usual composition rule for relations, which satisfy the following:

C1 The relation <_{A} is the identity morphism on A for all A ∈ Obj.

• Hom-sets are partially ordered by subset inclusion ⊆.

• The subset of inclusion morphisms, Inc ⊆ Mor, satisfies:

C2 Whenever an object A is a substructure of an object B, the relation <_{A}; <_{B} ⊆ |A| × |B|, with a (<_{A}; <_{B}) b iff ∃a′ ∈ |A|. a <_{A} a′ & a′ <_{B} b, is a morphism, the unique inclusion morphism in hom(A, B).

C3 For all objects A, in(Δ, A) exists and in(Δ, A) ⊆ f for all f ∈ hom(Δ, A).

• The subset of projection morphisms, Pr ⊆ Mor, satisfies:

D1 Whenever an object A is a substructure of an object B, the relation <_{B}; <_{A} ⊆ |B| × |A|, with b (<_{B}; <_{A}) a iff ∃a′ ∈ |A|. b <_{B} a′ & a′ <_{A} a, is a morphism, the projection morphism in hom(A, B).

D2 Δ is a terminal object.

It is easy to see that an information category with projections is a PI-category with embeddings: In fact, if A ⊴ B we have <_{A}=<_{B} ∩(|A| × |A|) and therefore:

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

which establishes that we have an embedding-projection pair. We can also weaken the substructure relation A ⊴ B by only stipulating that <_{A}⊆<_{B} ∩(|A| × |A|), which will then give us proper adjunctions as in the case of ISys.

Recall that in an information category the global partial order on morphisms reduces to inclusions of relations, i.e.

(f : A → B) ⊴^{m} (g : C → D)  iff  A ⊴ C & B ⊴ D & f ⊆ g.

Recall also that an information category is complete if it is closed under taking the union of increasing chains of objects and the union of increasing chain of morphisms. an information category with projections is defined to be complete if it is complete as an information category. Since a complete information category is a complete I-category, it follows by definition that a complete information category with projections is a complete PI-category. Similarly, an ω-algebraic p-information categories is defined in the obvious way.

5.1 Examples

Par. Consider the category of sets and partial maps. The hom-sets are partially ordered in the usual way, i.e. we put f ⊑ g if whenever f is defined g is also defined and has the same value. When A ⊆ B, we take in(A, B) to be the inclusion map and pr(B, A) to be the partial map which acts as identity on elemnts of A and is undefined otherwise. This clearly gives us an embedding-projection pair. Furthermore, Δ = ∅ is the initial and the final object. This proves that (Par, Inc, Pr, ⊑, ∅) is a p-information category, which is easily seen to be complete. Any subcategory, whose objects have elements from a countable pool will be ω-algebraic.

Rel. More generally consider the category of sets and relations. The hom-sets are partially ordered by inclusion of relations. When A ⊆ B, we define in(A, B) ⊆ A × B and pr(B, A) ⊆ B × A to be the set {(a, a) | a ∈ A}. We again have a projection-embedding pair and the empty set is initial and terminal. Therefore Rel is a complete information category with projections, with ω-algebraic subcategories, as in Par.

Information systems for domains. We have already seen that ISys that is an information category with projections. Here we list some other examples. Recall that in [ES91b], the following complete information categories, equivalent to the corresponding categories of domains, were constructed:

1 The category BC-ISys equivalent to the category of Scott domains and continuous functions.

2 The category SFP-ISys equivalent to the category of SFP domains with continuous functions.

3 The category DI-ISys equivalent to the category of dI-domains with stable maps.

4 The category CS-ISys equivalent to the category of continuous Scott domains and continuous functions.

In each case, an inclusion morphism appears with its corresponding projection morphism as in the following table:

category  object  a(in(A, B))b  b(pr(B, A))a
BC-ISys  (A, ⊢, ∧)  a ⊢_{B} b  b ⊢_{B} a
SFP-ISys  (A, ⊢, Mlb, V)  a ⊢_{B} b  b ⊢_{B} a
DI-ISys  (A, ⊢, ∧, ∨, h)  a ≡_{A} b  b ≡_{A} a
CS-ISys  (A, ⊢, ∧, <)  a(<_{A}; <_{B})b  b(<_{B}; <_{A})a

where ≡_{A} is the equivalence relation induced by ⊢_{A}. It is easy to see that all these categories are in fact complete information categories with projectios. Moreover, it was shown in the above cited work that BC-ISys, SFP-ISys and DI-ISys have full and equivalent subcategories BC-ISys*, SFP-ISys* and DI-ISys* which are ω-algebraic information categories. These categories are therefore ω-algebraic.

We mention some other examples constructed by other authors:

5 Gunter’s category of pre-orders and approximable mappings PO in [Gun87], which is equivalent to the category of algebraic dcpo’s and continuous functions. Objects are of the form (A, ⊢) and if A ⊴ B then the inclusion and projection are given by in(A, B) = ⊢ ∩(A × B) and pr(B, A) = ⊢ ∩(B × A).

6 Gunter’s category of Plotkin orders and approximable mapping in the above cited work, which is equivalent to the category of bifinite domains and continuous functions. Objects can be considered as tuples (A, ⊢, B(−)), where (A, ⊢) is a pre-order and B : P_{fin}(A) → P_{fin}(A) is such that B(u) is normal in A for all u ∈ P_{fin}(A) (i.e. for all a ∈ A the set ↓a ∩ B(u) is directed). The inclusions and projections are defined as in the case of PO above.

7 Abramsky’s category of SFP pre-locales, DPL1, in [Abr91]. Objects are of the form (A, ≤_{A}, =_{A}, 0, ∨, 1, ∧, C_{A}, T_{A}). Given objects A and B with A ⊴ B, the inclusion and projection are defined by:

a(in(A, B))b ⟺ a ≤_{B} b b(pr(B, A))a ⟺ b ≤_{B} a.

8 Vicker’s category of continuous information systems with approximable maps Infosys in [Vic91], which is equivalent to the category of continuous posets and continuous maps. Objects are of the form (A, <), where < is a transitive-interpolative order. An approximable map f : A → B is a relation from A to B satisfying:

(i) if a′ > afb then a′fb

(ii) if a′fb then a′ > afb for some a

(iii) if afb′ > b then afb

(iv) if a′ > afb_{i} (1 ≤ i ≤ n), then there is some b ∈ B with a′fb and b > b_{i} for all i.

The identity morphism on A is given by >. Suppose now that (A, <_{A}) ⊴ (B, <_{B}), i.e. A ⊆ B and <_{A}=<_{B} ∩(A × A). Then it is easy to check that >_{A}; >_{B}: A → B and >_{B}; >_{A}: B → A are in fact morphisms, which we define to be the inclusion and the projection as they satisfy (>_{A}; >_{B}); (>_{B}; >_{A}) = >_{A} = Id(A) and (>_{B}; >_{A}); (>_{A}; >_{B}) ⊆ >_{B} = Id(B).

9 Zhang’s category of stable information systems with stable approximable maps SIS in [Zha89], which is equivalent to the category of dI-domains and stable maps. We will not present the details of his work in here and assume the interested reader is familiar with this work. Given stable information systems \underline{A} = (A, Con\underline{A}, ⊢\underline{A}) and \underline{B} = (B, Con\underline{B}, ⊢\underline{B}), recall that \underline{A} ⊴ \underline{B} if

1. A ⊆ B

2. X ∈ Con\underline{A} ⟺ X ⊆ A & X ∈ Con\underline{B}

3. X ⊢\underline{A} a ⟺ X ⊆ A & X ⊢\underline{B} a

We can now define the inclusion and projection maps by

X(in(A, B))b ⟺ X ⊣⊢\underline{A} \{b\} Y (pr(B, A))a ⟺ Y ⊣⊢\underline{A} \{a\}.

Note that we necessarily have b ∈ A and Y ∈ Con_{A} in the above definitions.It is easy to check that these are stable approximable mappings which satisfy in(A, B); pr(B, A) = Id(A) and pr(B, A); in(A, B) ⊆ Id(B). It can then be deuced that, SIS is a complete information category with projections.

10 Hoofman’s category of continuous information systems with continuous approximable maps cIS in [Hoo91], which is equivalent to the category of continuous Scott domains and continuous maps. An object of the category has the form (A, ⊢, Con), where con is as in the case of ISys the set of consistent tokens and ⊢ is an entailment relation which is transitive-interpolative but not necessarily reflexive. If A ⊴ B, then it can be checked that ⊢_{A}; ⊢_{B}: A → B and ⊢_{B}; ⊢_{A}: B → A are in fact morphisms, which define the inclusion and the projection.

11 Hoofman’s category of qualitative information systems and qualitative approximable mappings, qIS, also in [Hoo91], which is equivalent to the category of qualitative domains and continuous functions. Objects are of the form (A, Con), where Con ⊆ P_{fin}(A) is the set of consistent sets and a morphism f : A → B can be considered as a relation f ⊆ Con_{A} × Con_{B} satisfying: (X ⊆ X′ & XfY) ⇒ X′fY. If A ⊴ B, the inclusion and the projection are defined by

X(in(A, B))Y ⟺ Y ⊆ X Y (pr(B, A))X ⟺ X ⊆ Y.

As we did in the case of ISys, we can weaken the substructure relation in the above examples, except for the case of dI-domains, to obtain proper adjunctions rather than only embedding-projection pairs. When we do that, CS-ISys simply becomes the Karoubi envelope of BC-ISys.

References

[Abr91] S. Abramsky. Domain theory in logical form. Annals of Pure and Applied Logic, 1991.

[BC81] G. Berry and P.-L. Currien. Sequential algorithms on concrete data structures. Technical report, Report of Ecole Nationale Superieure des Mines de Paris, Centre de Mathematiques Appliquées, Sophia Antipolis, 1981.

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

[Fre91a] P. Freyd. Algebraically complete categories. Preprint, 1991.

[Fre91b] P. Freyd. Remarks on algebraically compact categories. Preprint, 1991.

[Gun85] C. Gunter. Profinite Solutions for Recursive Domain Equations. PhD thesis, University of Wisconsin, Madison, 1985.

[Gun87] C. Gunter. Universal profinite domains. Information and Computation, 72(1):1–30, 1987.

[Hoo91] R. Hoofman. Continuous information systems. Information and Computation, 1991. to appear.

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

[Sco72] D. S. Scott. Continuous lattices. In E. Lawvere, editor, Toposes, Algebraic Geometry and Logic, pages 97–136. Springer-Verlag, Berlin, 1972. Lecture Note in Mathematics 274.

[Sco81] D. S. Scott. Lectures on a mathematical theory of computation. Monograph PRG-19, Oxford University Computing Laboratory, Oxford, 1981.

[Sco82] D. S. Scott. Domains for denotational semantics. In M. Nielson and E. M. Schmidt, editors, Automata, Languages and Programming: Proceedings 1982. Springer-Verlag, Berlin, 1982. Lecture Notes in Computer Science 140.

[SP82] M. B. Smyth and G. D. Plotkin. The category-theoretic solution of recursive domain equations. SIAM J. Computing, 11:761–783, 1982.

[Vic91] S. Vickers. Continuous information systems. pre-print, 1991.

[Zha89] G. Q. Zhang. dI-domains as information systems. In G. Ausiello, M. Dezani-Ciancaglini, and S. Ronchi Della Rocca, editors, Automata, Languages and Programming, volume 372 of Lecture Notes in Computer Science, pages 773–788, Berlin, 1989. Springer Verlag.