I-categories and duality
Michael B. Smyth · Cambridge University Press eBooks · 1992
Introduction In recent joint work with A. Edalat[ES91] we developed a general approach to the solution of domain equations, based on information system ideas. The basis of the work was an axiomatization of the notion of a category of information systems, yielding what we may call an “information category”, or I-category for short. We begin this paper with an exposition of the I-category work. In the remainder of the paper we consider duality in I-categories, as the setting for studying initial algebra/final algebra coincidence. We then look at induction and coinduction principles in the light of these ideas. To amplify the preceding a little, we note that the existing treatments of information systems, following [Sco82] and [LW84], make use of a global ordering of the objects of the category (the information systems) in order to “solve” domain equations by the ordinary cpo fixed point theorem. In the I-category approach, an initial algebra characterization of the solutions is obtained, by making use of a global ordering ⊆ of morphisms in addition to the ordering ⊴ of objects. (In the usual cases, where morphisms are “approximable relations” between tokens, the global ordering is essentially set inclusion; more precisely, we have that ( f : A → B) ⊆ (f′ : A′ → B′) if A ⊴ A′, B ⊴ B′ and f ⊆ f′.) Moreover the axiomatic formulation enables us to handle many examples besides the usual categories of domains, in a unified manner: for example, “domain equations” over Stone spaces, via Boolean algebras as information systems. In the present exposition, we attempt to clarify the relation between the I-category approach and an established method of domain equation solution, namely the O-category method,usingthe Basic Lemma of [SP82] as a key.