Solving Recursive Domain Equations with Enriched Categories

Kim Ritter Wagner

July 1994

CMU-CS-94-159

School of Computer Science Carnegie Mellon University Pittsburgh, PA 15213-3890

Submitted in partial fulfillment of the requirements for the degree of Doctor of Philosophy

Thesis committee: Dana S. Scott (chair)

Stephen Brookes John C. Reynolds Giuseppe Rosolini

This research has been partially supported by Carnegie Mellon University, RISC Linz, Johannes Kepler Universität Linz, The Medlar Project, and Forskerakademiet.

Keywords: semantics of programming languages, recursive domain equations, enriched categories, metric spaces, quantales.

Abstract

Both pre-orders and metric spaces have been used at various times as a foundation for the solution of recursive domain equations in the area of denotational semantics. In both cases the central theorem states that a ‘converging’ sequence of ‘complete’ domains/spaces with ‘continuous’ retraction pairs between them has a limit in the category of complete domains/spaces with retraction pairs as morphisms. The pre-order version was discovered first by Scott in 1969, and is referred to as Scott’s inverse limit theorem. The metric version was mainly developed by de Bakker and Zucker and refined and generalized by America and Rutten. The theorem in both its versions provides the main tool for solving recursive domain equations. The proofs of the two versions of the theorem look astonishingly similar, but until now the preconditions for the pre-order and the metric versions have seemed to be fundamentally different. In this thesis we establish a more general theory of domains based on the notions of enriched categories, and prove Scott’s inverse limit theorem in this theory. The metric and pre-order versions are special cases, obtained just by using different logics as parameter to the general theory.

We establish a general framework for the most basic parts of domain theory, thereby unifying the partial order and the metric approach to solving recursive domain equations. More generally we provide a recipe for going from a logic of approximations to a category of domains reflecting this logic, and suitable for the solution of recursive domain equations. The categories of chain complete pre-orders with continuous maps and generalized complete metric spaces with continuous maps are only two examples of the categories obtainable this way. The main unifying tool is our notion of limsup convergence in enriched categories, which unifies least upper bounds of chains in pre-orders with metric limits of Cauchy sequences.

We show that there is a straightforward logical connection from a choice of a particular notion of approximation in semantic domains to a category of domains that firstly supports that notion of approximation and secondly supports the solution of recursive domain equations. Furthermore, in most cases it is just a matter of placing yourself in the right universe, and what is externally the above mentioned category of domains is internally the category of chain complete pre-ordered sets and continuous maps.

Contents

1 Introduction 3

2 Domains for Denotational Semantics 9 2.1 Pre-orders for semantics - The Scott approach . . . . . . . . . . . . . . . . . 9 2.2 Metric spaces for semantics . . . . . . . . . . . . . . . . . . . . . . . . . . . 13

2.2.1 Metric prerequisites . . . . . . . . . . . . . . . . . . . . . . . . . . . . 14 2.2.2 Denotational semantics for processes . . . . . . . . . . . . . . . . . . 18 2.2.3 Solving general domain equations with metric spaces . . . . . . . . . 22

2.3 Metric spaces as pre-orders . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29

3 Enriched Category Theory 31 3.1 Basics of enriched category theory . . . . . . . . . . . . . . . . . . . . . . . . 31 3.2 Cauchy completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 38 3.3 The enriched Dedekind-MacNeille completion . . . . . . . . . . . . . . . . . 42 3.4 Limsup completeness . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 47 3.5 Banach’s fixed-point theorem . . . . . . . . . . . . . . . . . . . . . . . . . . 52

4 Internalization 55 4.1 Preliminaries . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 56 4.2 Pre-sheaves and sheaves . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 62 4.3 Cauchy completion and sheafification . . . . . . . . . . . . . . . . . . . . . . 68 4.4 Internal logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 69 4.5 Quantale logic . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 70 4.6 Internal enriched categories: APOs . . . . . . . . . . . . . . . . . . . . . . . 70 4.7 Limsup complete APOs . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 72

5 A General Inverse Limit Theorem 79 5.1 The inverse limit construction . . . . . . . . . . . . . . . . . . . . . . . . . . 79 5.2 Fixed-points of functors . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 85

6 Powers of APOs 87

7 Conclusion 91 2

Chapter 1

Introduction

Both pre-orders and metric spaces have been used at various times as a foundation for the solution of recursive domain equations in the area of denotational semantics. In both cases a crucial theorem holds, stating that a ‘converging’ sequence of ‘complete’ objects with ‘continuous’ retraction pairs between them has a limit in the category of complete objects with retraction pairs as morphisms. The pre-order version was discovered first ([Scott 69] and [Scott 72]), and is referred to as Scott’s inverse limit theorem. The metric version was mainly developed in [de Bakker & Zucker 82], [de Bakker & Zucker 82b], and [America & Rutten 87]. The theorems occupy a central place in both the pre-order and the metric approach to solving recursive domain equations. The proofs look astonishingly similar, but until now the preconditions for the pre-order and the metric versions have seemed to be fundamentally different. In this thesis we indicate how to use one and the same proof for both cases, just varying the logic to move from one setting to the other.

We aim at establishing a general framework for the most basic parts of domain theory, thereby unifying the partial order and the metric approach to solving recursive domain equations. More generally we provide a recipe for going from a logic of approximations to a category of domains reflecting this logic, and suitable for the solution of recursive domain equations. The categories of chain complete pre-orders with continuous maps and generalized complete metric spaces with continuous maps are only two examples of the categories obtainable this way.

Our intention is to show that there is a straightforward logical connection from a choice of a particular notion of approximation in semantic domains to a category of domains that firstly supports that notion of approximation and secondly supports the solution of recursive domain equations. Furthermore, in most cases it is just a matter of placing yourself in the right universe, and what is externally the above mentioned category of domains is internally the category CPreOrd, the category of chain complete pre-ordered sets and continuous maps.

The whole branch of denotational semantics of programming languages grew out of Scott and Strachey’s work on giving a mathematical interpretation to standard programming languages using the λ-calculus as a meta-language. Scott’s worries about Russelian paradoxes caused by the type-free form of self-application in the λ-calculus were only settled when he gave a consistent model himself ([Scott 69]). The paradigm in this model, and in numerous subsequent denotational models for programming languages is to model data types by partial orders. The objects of the partial orders should not be seen as data themselves, but as pieces of information about data. One can have more or less information about a piece of data (the output of some function, for example), which amounts to one element in the partial order being less than another. Having no information at all is modeled by the always existent unique least element, ⊥, pronounced ‘bottom’. In the partial order one element is in general less than another if you can obtain the second from the first by gaining more information. We say that the first element approximates the second. It is worth emphasizing that this notion of approximation is a binary one. Either one element approximates another or it does not. There is no gradation.

The use of metric spaces for semantics was initiated by Nivat (see for instance [Nivat 79] and [Arnold & Nivat 80]), followed by de Bakker and Zucker ([de Bakker & Zucker 82] and [de Bakker & Zucker 82b]). Initially de Bakker and Zucker’s aim was to model concurrency in a way that was thought to be more straightforward than the pre-order (partial order) approach, which would model the non-determinism typically occurring in the context of concurrent languages with one of the power-domain constructions in use, the Smyth, Plotkin or Hoare power domain (see e.g. [Plotkin 76], [Smyth 78], and [Apt & Plotkin 81]). It was easy to introduce a distance between two sequences, following the paradigm that the longer you had to watch them to detect a difference, the closer they were. This is also at the root of the metric concept of approximation: an element approximates another to the extent of their mutual distance. Thus approximation is no longer a binary concept, but classified in (some subset of) the real numbers.

Metrics extend via the Hausdorff distance to distances between subsets, and it was possible for de Bakker and Zucker to give a denotational semantics to a wide range of language constructs in the realm of concurrent languages such as CSP. Later America and Rutten ([America & Rutten 87]) generalized the metric techniques to cover all the usual constructs in traditional programming language semantics, viz. products, sums (disjoint union), powerset, and function space, with constants such as the one element data type, the Booleans and the natural numbers. Their approach allows to a certain extent for a solution of all the traditional kinds of domain equations involving the constructs we just mentioned, but with an interesting proviso. It is often necessary to shrink the right-hand side occurrences of the left-hand side variable. Thus, an equation like D = D → ℕ + ℕ would have to be modified to D = \frac{1}{2}D → ℕ + ℕ, in order to have a solution in metric spaces. Here \frac{1}{2}D is the metric space that has the same points as D, but with all distances half those in D . We will return to a discussion about what this means for the metric approach as a semantics, and we also offer an analysis that shows that one might at least want to restrict oneself to categories of ultra-metric spaces, in order to obtain Cartesian closed categories.

As the unifying concept of pre-orders and metric spaces we follow Lawvere and use enriched categories. Enriched categories were introduced by Eilenberg and Kelly in 1966 ([Eilenberg & Kelly 66]) and popularized in the best sense of the word by Lawvere in 1973 ([Lawvere 73]). In this latter paper Lawvere showed how to use essentially categorical techniques on for instance pre-orders and metric spaces by softening the requirements on what constitutes a category, such that the resulting concept, an enriched category includes preorders, (generalized) metric spaces, and traditional categories, together with a whole range of other structures. The relaxation compared to traditional categories is to allow the hom functor to map into other categories than SET. In traditional categories the hom functor always maps a pair of objects into a set (i.e. an object of the category SET), viz. the set of morphisms from the first object to the second. In enriched categories we replace the base category SET by another category, such as for instance the two point lattice, 2, seen as a category with two objects and a morphism from one to the other object.

Categories enriched over 2 are precisely the pre-orders, and similarly we can obtain a category of generalized metric spaces starting with the interval [0, ∞] as the base category. Seen in this way the only thing that distinguishes a pre-order from a (generalized) metric space is that in a pre-order the connection between any two points a and b is classified by the set 2 = {⊤, ⊥} – either a ≤ b or not – whereas in a metric space the connection between two points is their distance. Allowing infinite distances the classifier of connections is then the extended interval [0, ∞]. Rules for composition of connections amount to transitivity of pre-orders and to the triangular inequality for metric spaces respectively. This approach to unification also suggests by itself ([Lawvere 73] p. 142) a suitable logic in which to reason about such structures, viz. intuitionistic logic in which the space of truth values is the classifier of the connections. So we should treat pre-orders in a two-valued logic and (generalized) metric spaces in a [0, ∞]-valued logic. In the cases where the classifier is a complete Heyting algebra this leads straightforwardly to the theory of the topos of sheaves over the classifier.

That the pre-order and the metric approaches to domain theory get unified this way is not surprising. What we do in effect is to reason about metric spaces (or other structures) in a universe where they are pre-orders, viz. in sheaves over [0, ∞] (or other Ω). Fortunately (!) Scott’s inverse limit construction is sufficiently general to survive the transport.

In the presented framework we have defined the concept of forward Cauchy sequence and directed net, which in case of pre-orders specialize to eventual chain and directed subset and in the case of metric spaces to Cauchy net (or equivalently Cauchy sequence). Further we have formulated a general form of convergence, generalizing least upper bound and metric limit, and thus we have unified the concepts of chain or directed completeness for preorders with Cauchy completeness for metric spaces, as well as the two forms of continuity. Following the same pattern the Egli-Milner ordering and the Hausdorff distance is unified, and a constructive metric notion of compactness is carried over to pre-orders. With these concepts, as they are expressed internally, we have proven a general version of Scott’s inverse limit theorem, and formulated a general sufficient condition for when functors of abstract pre-orders have fixed-points.

In Chapter 2 we give a brief summary of the basics of solving recursive domain equations in the partial order and the metric setting. It will be a quite basic resume, where we will aim at the simplest possible formulation. We will not go into any discussion of interesting subcategories or related categories, such as those consisting of ω-algebraic, consistently complete cpos, or of continuous lattices. Our treatment of the metric approaches will be a little longer than the partial order one, because we assume that the reader in general would be less familiar with it.

Next, in Chapter 3 we introduce one of the main tools used for the unification, viz. the theory of enriched categories. Our emphasis will be on the cases where the base category is a pre-order, as in the two examples just given, but it is very likely that a similar development would go through even in the full generality of categories enriched over a monoidal closed category. One would have to work with limits and colimits in the monoidal category instead of meets and joins in the lattice, and the generalization may by no means be trivial. We consider this an obvious subject for further study.

The elements of enriched category theory that we have used are just the very basic ones. There might be something gained by using categories enriched over bicategories (so-called Bcategories, à la Walters ([Walters 81] and [Walters 82])), as suggested to us by Pino Rosolini. For an introduction to bicategories in general, see [Bénabou 67] and more directly relevant to our work, [Carboni & Walters 85]. However, we have shied away from this complication, also for pedagogical reasons, and because simple enriched categories have been enough for our purposes. It is our hope however, that subsequent work will take advantage of the increased expressive power of bicategories, about which we offer a small discussion in Section 4.3.

Apart from the most basic elements of enriched category theory we describe the notions of Cauchy and MacNeille completion for enriched categories in some detail, and introduce a notion of convergence which we call limsup convergence, and which unifies least upper bounds of chains or directed sets in a pre-order with metric limits of Cauchy sequences in metric spaces. Naturally this step is crucial in our efforts to unify the pre-order and the metric approaches to semantics, and it has to our knowledge not been noticed before. We have after our own discovery found that Rowlands-Hughes in his thesis ([Rowlands-Hughes 87]) notices that there is a common formulation for being eventually chain in a pre-order and being a Cauchy sequence in a metric space, but he does not follow this up by defining the associated notion of completeness and using the resulting (limsup) complete spaces as domains.

We relate our notions of convergence and completeness with the Cauchy and MacNeille completeness, and give a formulation in terms of indexed limits in enriched categories. Finally we look at a generalized version of Banach’s fixed-point theorem to enriched categories, and formulate a (not very interesting) sufficient condition for when an endo-morphism on a limsup complete enriched category has a fixed-point.

In Chapter 4 we discuss aspects of internalization of the notions of limsup convergence and completeness that we have just defined. The aim here is to show that the general structures we have defined, limsup complete enriched categories, in suitable universes, are nothing but ordinary chain (directed) complete pre-orders. Inside such a universe, which for suitable base categories is the topos of sheaves over the category, we can reason as if we were dealing with pre-orders, and thus we just have to make the proofs we want to generalize from a pre-order setting to our general setting constructive. This also allows us to simplify the notion of limsup completeness internally. However, we can carry through the most crucial steps, viz. Scott’s inverse limit theorem in a wider class of enriched categories than those that allow for a topos of sheaves over a complete Heyting algebra as universe. We allow for a general commutative unital quantale as base category, and still get this theorem. This part of our development can also be internalized, but only to a first order logic based on a quantale of truth-values, which however, is enough for our purposes. In Chapter 4 we first give the preliminaries about Ω-sets, presheaves and sheaves, and the associated logic, subsequently we discuss the internal formulation of our completeness and convergence concepts.

Finally, in Chapter 5 we present a generalized version of Scott’s inverse limit theorem and give sufficient conditions for when a functor has fixed-points. These conditions generalize those of Scott (the original reference is [Scott 69], for a categorical exposition see [Smyth & Plotkin 82]) and America and Rutten ([America & Rutten 87]). Finally, we also discuss power-set constructions, notions of compactness of elements and of domains. We relate to the Plotkin, Smyth, and Hoare power-domains, and discuss the relation between the Egli-Milner ordering and the Hausdorff distance, something Smyth has already done in a less general setting.

Concerning the prerequisites necessary for reading this thesis, I have tried to minimize them, and to make the thesis self-contained, except when it comes to category theory. There are plenty of books on category theory available, most notably [Mac Lane 71] which explains the concepts much more elegant than I could hope to do. Therefore there are no introductions or expositions of the basics of standard category theory in this thesis.

It is our hope that the method outlined in this thesis can be extended straightforwardly to cover categories enriched not just over pre-orders, but over proper categories as well. This would allow for iterating the process such that for instance we would go from the two point lattice to chain complete pre-orders with continuous maps and on to complete cpo-enriched categories (see [Fiore 93] and [Smyth & Plotkin 82]).

Acknowledgements.

First thanks to my parents and the rest of my family for their love and support. I have never been able to explain to them quite what I’m doing, but I guess they have been convinced that I was having a good time, especially in times when I traveled a lot.

My unscientific thanks also to the greatest office mates one can ever wish to have, Jim Stichnoth, Todd and Mary Wilson, Karel Stokkermans, Shang-Hua and Suzie Teng. All have become my close friends, and their hospitality seem unrelenting and unabated by my abuse. Also many thanks to all the other friends Lorenzo and Irene (and now Maria) Alvisi, Viorica Sofronie, Victor Pollara, Yashushige Watase, Carl van Geem, Josef Schicho, Wolfgang Gehrke, Drew Dean, Peter Sestoft, Peter Krogh, Roger Christensen, Helle Knudsen, Anne Haxthausen, and all the others, too many to mention, whom I met at Carnegie Mellon and RISC Linz, and those from my time at DIKU, DDC and CRI in Denmark.

First scientific thanks to Dana Scott, my advisor through almost 5 years at Carnegie Mellon. His patiently throwing out pieces of wisdom that I could try to chew on eventually seems to have gotten me within reach of a Ph.D. thesis. I remain frustrated that alone in the wisdom I was allowed to share there would be material enough for many many more theses. If I could only remember all he had said! Please, Dana, make sure to subject many others to your ‘transient thoughts’! And not only scientific thanks to Dana, but especially thanks to him and his wife Irene for lots of support and help during some unsettled times in Austria.

Secondly, thanks to all the people from the scientific community who shared their knowledge with me in the most altruistic way. Special thanks go to Pino Rosolini for inviting me to Parma for a week, and for all his comments to my work. Without his help my sheaves would have been even more crooked than they are now. Thanks also to Steve Brookes who read the whole thesis with his usual thoroughness, and caught many flaws. Thanks to Roy Crole, Mike Smyth, Steve Vickers, and Samson Abramsky from Imperial College for inviting me for visits twice, and for the long, pleasant and inspiring conversations I had with them all. Thanks to Dines Bjørner, Søren Prehn and Zhou Chao Chen from UNU/IIST in Macao for hosting me there. Many thanks to Jiří Adámek, Aleš Pultr and the TEMPUS project for inviting me to Prague on many occasions, for our numerous interesting conversations, and for the very fruitful collaboration that we were able to establish, also with the TEMPUS students. Thanks to Glynn Winskel for inviting me to visit Aarhus University, to Anders Kock for a very interesting conversation there, to Jaco de Bakker and Jan Rutten for inviting me to CWI and for many hours of interesting conversations there. Also thanks to Gordon Plotkin from Edinburgh for inviting me there, and to him, Marcelo Fiore, and John Power for interesting conversations. Especially John Power’s comments as to the structure and emphasis in my thesis have been most helpful. Thanks to Andy Pitts for inviting me to Cambridge, for our interesting conversations, and for offering me a post-doc position (!) Thanks also to Barry Jay who together with Pino Rosolini referred me to Lawvere’s wonderful article about generalized logic and metric spaces, [Lawvere 73], John Reynolds, Mike Beeson, Andrzej Tarlecki, Andre Joyal, Fer-Jan de Vries, Todd Wilson, Frédéric van der Plancke, and many whom I’ve forgotten at the moment for their fruitful comments.

Also my deepest appreciation and thanks to Dines Bjørner to whom I went sometime back in 1988 when I was working at his company DDC. I told him that I’d like to quit sometime, to become a Ph.D. student in Denmark. He told me that I should go abroad, ‘You should go to Carnegie Mellon, Cambridge, Oxford, Edinburgh, Stanford, … ’ he said. Without his continued encouragement and help at that stage, I would never have gone to Carnegie Mellon, and this thesis would certainly never have happened.

Economical and logistical thanks to Carnegie Mellon University, Forskerakademiet, Johannes Kepler Universität Linz, and RISC Linz, where the remodelled castle ‘Schloß Hagenberg’ provided an excellent and most scenic environment for the last almost two years of my studies. Special thanks to the leader of RISC, Bruno Buchberger and to Jochen Pfalzgraf and the Medlar project whose support in the period 1992-1994 has been invaluable. Also many thanks to Jiří Adámek and the TEMPUS project for their support in connection with all my trips to Prague and to the summer school in Brno.

And then, finally, a couple of untraditional thanks. First to the staff at Carnegie Mellon, mostly, as will be obvious for all who have been to CMU, to assistant dean Sharon Burks. Somehow she manages to know all the administrative and bureaucratic snares of grad school, and helps the 100+ students through all that as if it were nothing at all. Also many thanks to Cathy Copetas, Karen Olack, Rebecca Clark and all the other professionals, and to the fabulous Carnegie Mellon CS operators. Wherever I go people only hesitatingly believe me (or claim to believe me out of politeness) when I tell them that you can call any time 24 hrs a day, 365 days a year (non-leap years) and get a friendly and competent voice at the other end saying ‘CS operator, … speaking, how may I help you’. I considered giving away the extension of you guys, just to prove that I’m right, but I guess you’d then get lots of calls Christmas night or some time like that, from people all over the world, who’d just go: ‘Oh wow, you’re really there’.

I have used John Reynold’s macro package for diagrams and various other mathematical notation throughout this thesis.

Domains for Denotational Semantics

This is not going to be a primer on denotational semantics or the associated theory of domains, but just an outline of some of the main motivations of the latter. In addition we will list some useful references. After all, our purpose is to propose a new, general way of thinking about domains for semantics that aim at unifying two previous approaches, and thus we just want to remind the reader what we are unifying. We will go a little more into details with the metric approaches to semantics, since these are less well known than the partial order based ones.

2.1 Pre-orders for semantics - The Scott approach

It has been customary since [Scott 70a] and [Scott & Strachey 71] to model the domain of possible outcomes of a function computed by some algorithm, with a pre-order (or more precisely with a partial order). Consider for example a function f which is supposed to output a Boolean. If we have called f , but not yet gotten an answer we are in a state of having no information about f’s output - perhaps f will not even terminate before we lose patience and turn off the computer. We denote this state of information ⊥ (‘bottom’), and ⊥ is the unique least element in the pre-order modeling Booleans. We do not normally distinguish between the kinds of data that we allow functions to take as arguments and the kind of data that is allowed as output, and thus every data type we model will reasonably be equipped with its own bottom element. Returning to the function f , the only other states of information we can reasonably be in are ones where we have observed that f has returned ‘true’ or ‘false’, and therefore the model pre-order (semantic domain) for Booleans look like this:

[figure: true; false; ⊥]

The pre-order is interpreted as ‘less information’.

Naturally we now proceed to consider functions that may return structured data (pairs, triples, pairs of pairs etc.) and so we need products of domains. In this connection we have to decide whether we will consider it possible that a function returns with only partial information about its output. This would certainly be reasonable when dealing with concurrent programs where two processes may each produce one element of a pair, say. The choice in this matter decides whether we should identify elements like (⊥, 3) with (⊥, ⊥) . If we want a categorical product we need to maintain the distinction. In this case, we now get ‘taller’ pre-orders: (⊥, ⊥) < (⊥, 3) < (1, 3) , say.

Similarly we will often need to take sums of domains, as e.g. in Stmt = Cmd+Exp+…. If we, as it is normal, but not mandatory for all purposes, insist on every domain having a unique least element, we have the choice between coalesced and separated sum. The coalesced sum of two pre-orders is the set theoretic union between the underlying sets with the two bottom elements identified (and other elements from different summands unrelated, of course). The separated sum does not identify the two bottoms, but adds a new one below the two existing ones. In a categorical framework we would like to see the sum as a coproduct. Consider the category PreOrd_{⊥} of pre-orders with a least element unique up to isomorphism and monotone maps. This category does not have a categorical coproduct. If we restrict the morphisms to be the strict ones, that is, those monotone maps that preserve bottom, then we do have a coproduct, viz. the coalesced sum. If we just consider pre-orders and monotone maps, without any requirement about strictness of functions or existence of unique least elements, then the coproduct is just set theoretical union. Always when we consider pre-orders we should notice that the notion of equality between morphisms is only up to equivalence. Two morphisms are equal if and only if, for every argument they give equivalent results. This is necessary in order to obtain the standard universal properties of for instance product and coproduct.

If we now consider functions as values that can be used as arguments to other functions, we have to consider function spaces between domains as domains themselves. The issue that arose in the work of Scott and Strachey on the λ-calculus is then if it is possible to model an untyped notion of function where any function can take any other function as argument. Russelian paradoxes seem to be lurking, something that worried Scott (see the now finally published paper [Scott 93]) until he found a suitable model himself ([Scott 69]). One of the crucial steps in the construction is to restrict the allowable functions in the domains to be not the monotone functions, but only the continuous ones. Monotonicity is obvious, the more information about the input to a function we have the more information we can expect about the output. Continuity means that we additionally require that if a chain (an increasing sequence) of elements (a_{n})_{n^{∈}ℕ} in a pre-order A combine to a piece of information, a (the least upper bound of the chain), then a continuous function f from A will respect this relationship between the chain and its least upper bound in the sense that the sequence (f(a_{n}))_{n^{∈}ℕ} will be a chain and have f(a) as least upper bound. We say that f is continuous if it preserves least upper bounds. Further, in any categorical analysis, we want to equate functions that for equivalent arguments give equivalent results. It is actually enough to require that they give equivalent results for equal arguments. Then monotonicity implies that they also give equivalent results for equivalent arguments. Here, naturally, two elements a and a′ are equivalent if a ≤ a′ and a′ ≤ a. The consequence of introducing this equivalence on functions is that we can use the usual categorical universal constructions that involves unique existence of morphisms. Without the equivalence we would often have unique existence only up to equivalence, and thus not fulfill the categorical conditions for universality.

One requirement on the domains themselves that we will almost always impose is that they support recursive definitions. This means for instance that given a domain A defined by the equation A = ℕ + A × ℕ we want to be able to define an element a of A by the equation a = (1, a) and think of a countably infinite structure a = (1, (1, …)) as the object being defined. We can find this object as a least upper bound of the chain ⊥ ≤ (1, ⊥) ≤ (1, (1, ⊥)) ≤ (1, (1, (1, ⊥))) ≤ ⋯, and we therefore require our domains to be chain complete, or more generally directed complete. The notion of directedness is introduced to cover larger domains than countable chains can. A subset of a pre-order is called directed if it contains upper bounds for all its finite subsets, and a pre-order is directed complete if every directed set has a least upper bound. We see that directed sets generalize chains and directed completeness chain completeness. Thus, it seems that the relevant category of domains is the category of chain (or directed) complete pre-orders with continuous morphisms. Further analysis will show that many more elaborate categories derived from these can be very fruitful. To obtain unique fixed-points we might want to impose a partial order not just a pre-order, and also a unique least element. Further considerations concerning computability may prompt us to consider ω-algebraic cpos or continuous lattices, and consistently complete ones to obtain a Cartesian closed category again. A good first source for such considerations is [Gunter 92].

Let us summarize the categories so far:

Definition 2.1 We denote by PreOrd the category of pre-ordered sets with equivalence classes of monotone maps, by CPreOrd the full sub-category thereof, consisting of the chain complete pre-orders, DPreOrd, the directed complete ones, and we use subscript ⊥ as in PreOrd_{⊥} to indicate that we require a unique least element (up to isomorphism). In all cases the equivalence relation is the one induced by the pre-order: two maps f and g are equivalent if f(a) ≤ g(a) and g(a) ≤ f(a) for all arguments a. □

Concerning the definition of domains we may want to use recursive definitions here for two reasons. First, as was the case for Scott and Strachey, the language may have a semantic domain that is inherently self-referential. For example, untyped λ-calculus has only one type, and thus just one semantic domain, D say, which has to contain D → D, and languages such as LAMBDA ([Scott 76]) that are based on λ-calculus, but have products and some basic types added, then have to have a type, L say, which contains both L × L and L → L besides more mundane types such as those representing Booleans and natural numbers. The self referencing nature of the language need not be as obvious as this. It suffices for instance that the language contains statements that may contain commands, and commands that may contain statements. A second reason for recursively defined semantic domains might be the possibility in the programming language to specify data types recursively. This facility we see for instance in Standard ML.

Whatever the reason for the recursive domains, for their definition we use a technique similar to the iteration we saw for values. Take for example the domain equation.

L = ℕ + ℕ × L ,

which is meant to specify lists of natural numbers in form of layered pairs. The associated functor is the one that maps the left-hand side of the equation into the right-hand side, that is,

F (L) = ℕ + ℕ × L .

The functor F works on a morphism f : L → M in the natural way,

F (f)(n) = f(n) ,
F (f)(n, l) = (f(n), F (f)(l)) .

We find a fixed-point for F by iterating F on the terminal object, 1l = {⊥} of our category, obtaining, with D_{n} = F^{n}1l .

D_{0} = {⊥}
D_{1} = ℕ + ℕ × {⊥}
D_{2} = ℕ + ℕ × (ℕ + ℕ × {⊥})
⋮

Since we are in a category of chain complete pre-orders the desired limit object, D say, of this sequence consists of all finite and infinite ‘sequences’ of natural numbers. For an analysis leading to sufficient properties for a functor to have a fixed-point it turns out to be useful to split the considerations in two as follows.

(i) When does a sequence D_{0}→^{ϕ_{0}} ; ←_{ψ_{0}}D_{1}→^{ϕ_{1}} ; ←_{ψ_{1}}D_{2}→^{ϕ_{2}} ; ←_{ψ_{2}} ⋯ have a limit (in a suitable sense, to be made

precise soon)?

(ii) Which functors generate chains that fulfill (i), and when is the ‘limit’ of the chain a fixed-point up to isomorphism of the functor?

As to (i) we have Scott’s inverse limit theorem.

Theorem 2.1 When the diagram D_{0}→^{ϕ_{0}} ; ←_{ψ_{0}}D_{1}→^{ϕ_{1}} ; ←_{ψ_{1}}D_{2}→^{ϕ_{2}} ; ←_{ψ_{2}} ⋯ in the category of chain complete pre-

orders with continuous maps fulfills

(i) ψ_{n} ∘ ϕ_{n} = id_{D_{n}} (that is, (ϕ_{n}, ψ_{n}) is a retract),

(ii) ϕ_{n} ∘ ψ_{n} ≤ id_{D_{n+1}} ,

for all n ^{∈} ℕ , then there exists D and (Φ_{n}, Ψ_{n})_{n^{∈}ℕ} such that (D, (Φ_{n})_{n^{∈}ℕ}) is a colimit for

D_{0} →^{ϕ_{0}} D_{1} →^{ϕ_{1}} D_{2} … and (D, (Ψ_{n})_{n^{∈}ℕ}) is a limit for D_{0} ←_{ψ_{0}}D_{1} ←_{ψ_{1}}D_{2} …. Further Ψ_{n} ∘ Φ_{n} =

id_{D_{n}} and Φ_{n} ∘ Ψ_{n} ≤ id_{D} for all n ^{∈} ℕ . □

The D above is defined D = { (x_{i})_{i^{∈}ω} | ∀i ^{∈} ω. [x_{i} ^{∈} D_{i} ∧ x_{i} = ψ_{i}(x_{i+1})] } with the pointwise ordering \overline{x} ≤ \overline{y} if and only if x_{i} ≤ y_{i} , for all i ^{∈} ω , where, of course, x_{i} (y_{i}) is the i’th element of \overline{x} (\overline{y}). Define further τ_{ij} : D_{i} → D_{j}, Φ_{i} : D_{i} → D, and Ψ_{i} : D → D_{i} as follows.

τ_{ij}(m_{i}) = \{ \begin{matrix}ψ_{j} ∘ ψ_{j−1} ∘ … ∘ ψ_{i−1}(m_{i}) & if & i > j \\ m_{i} & if & i = j \\ ϕ_{j−i} ∘ ϕ_{j−2} ∘ … ∘ ϕ_{i}(m_{i}) & if & i < j, \end{matrix}
Φ_{i}(m_{i}) = (τ_{ij}(m_{i}))_{j^{∈}ω},
Ψ_{i}(\overline{x}) = x_{i}.

Then ((D, ≤), (Φ_{i}, Ψ_{i})_{i^{∈}ω}) is the limit/colimit promised in Theorem 2.1. There are plenty of expositions on this theorem, for instance [Smyth & Plotkin 82] and [Lambek & Scott 86].

As to (ii) we follow Plotkin ([Plotkin 83]) and introduce the notion of a (locally) continuous functor as one that preserves chains and their limits as in (i). In this case, given ϕ_{0} : D_{0} → F D_{0} , that is, an element in F D_{0} , it can be seen that F generates a satisfactory chain if and only if ϕ(⊥) is the unique least element of F D_{0} up to isomorphism. In this case, and only then, do we have ϕ_{0} ∘ ψ_{0} ≤ id_{D_{1}} . The limit/colimit of the chain, according to (i) is a fixed-point up to isomorphism of F. The morphisms Ψ : D → F D and Φ : F D → D are obtained by the universal property of D being a limit and a colimit at the same time.

Notice, that the requirement that F D_{0} has a unique least element together with the obvious wish to use sums, often makes it desirable to move to the category CPreOrd_{⊥} of complete pre-orders with ⊥ . In order to obtain a categorical coproduct we can then restrict the morphisms to the strict ones (those preserving ⊥) and use coalesced sum.

Actually, considering the functors that usually come up in semantics we face the problem that the functor that maps a domain A into A → B for some domain B is contravariant. In general, functors may be covariant in some of their arguments and contravariant in others. We may either do like Smyth and Plotkin ([Smyth & Plotkin 82]) and move to a category where the morphisms are retracts, that is, pairs (ϕ, ψ) as above, fulfilling ψ ∘ϕ = id, whereby all functors become covariant, or we may do like Freyd ([Freyd 91] and [Freyd 92]) and split the positive and negative occurrences of a variable and obtain covariancy that way. For a further development in this direction see ([Pitts 93]). Paul Taylor remarks in his thesis ([Taylor 86], 2.2.12, p. 43) that in order to obtain the limit/colimit coincidence, it is really enough to require that ϕ_{n} is left adjoint to ψ_{n} for all n ^{∈} ℕ , that is, to require ψ_{n} ∘ϕ_{n} ≥ id_{D_{n}} instead of 2.1.(i).

2.2 Metric spaces for semantics

Metric spaces have been used in many ways to provide models for semantics. Most attention has been given to the use of metric spaces in the semantics of concurrent processes, an approach initiated by Nivat ([Nivat 79]), de Bakker and Zucker ([de Bakker & Zucker 82]), and probably inspired by the use of metric spaces in automata theory. The basic idea is that the distance between two sequences of events is 2^{−n} where the two sequences differ for the first time at the n’th element. One goes on to define a metric on for instance sets of event sequences by using the Hausdorff distance based on the distance between two single sequences.

America and Rutten showed in ([America & Rutten 87]) de Bakker and Zucker’s approach can be extended to traditional domain equations using operators such as Cartesian product, disjoint sum, function space, and power set. One essential feature in this approach is the concept of shrinking. It is easy to see that with the function space construction that America and Rutten use, viz. conservative maps (also called ‘non-distance increasing’: those that do not increase distance), there can be no solution to an equivalence as e.g. D ≡ (D → D) + (D × D) + ℕ. However, if we allow the copies of D → D and D × D to occur shrunk, say with all distances halved, America and Rutten show that solutions exist in general. The equivalence from before would be written D ≡ \frac{1}{2}(D → D) + \frac{1}{2}(D × D) + ℕ.

The same notion of shrinking plays a more intuitive role in metric models of fractals ([Barnsley 88]). One obtains a fractal from an initial (basically arbitrary) figure in ℝ^{2} by iterating a function from the set of subsets of ℝ^{2} to itself, that is contracting and therefore has a fixed-point – the fractal. For some of the usual fractals the function is a pasting together of several shrunk copies of the original figure. This is witnessed by the recursive look of most fractals.

A final application of metric spaces in semantics that deserves to be mentioned is the use of metric spaces as models of polymorphic types in [MacQueen et al. 84]. The use of metric spaces was motivated by the need to show that a certain functor had a fixed-point. In a partial order setting it was not monotone, but in the metric setting it became contracting. It turned out however, that a partial order approach would have worked, if one incorporated both positive and negative information ([Cartwright 85]).

We will start by giving the preliminary definitions for metric spaces, and will, due to their special role in semantics, spend some time on ultra-metric spaces as well. Then we give a taste of how metric spaces have been used by de Bakker and Zucker to give semantics to concurrency, and lastly we describe America and Rutten’s generalization to standard type equations, and end by giving their equivalent of Scott’s inverse limit theorem, this time using metric spaces instead of pre-orders. For the metric preliminaries we recommend [Dugundji 66], [Willard 70] and [Bourbaki 89], and for the specific ultra-metric material [Schikhof 84].

2.2.1 Metric prerequisites

We give some basic definitions and theorems that will lay the foundation for the subsequent development.

Definition 2.2 A metric space is a pair (M, d) where M is a set and d : M × M → [0, ∞) fulfills

(i) d(a, b) = 0 if and only if a = b (separating and reflexive),

(ii) d(a, b) = d(b, a) (symmetric),

(iii) d(a, b) + d(b, c) ≥ d(a, c) (triangle inequality).

A function f : A → B between metric spaces is called conservative if it does not increase the distance between its arguments, that is, if d_{B}(f(a), f(a′)) ≤ d_{A}(a, a′) for all a, a′ ^{∈} A. America and Rutten call such functions ‘non-distance-increasing’. Mappings that preserve the distance are called isometries. □

Actually, as we shall see in Chapter 3 we can relax the above axioms considerably and still get a category useful for semantics, while retaining its metric ‘character’. We will straightaway relax the above axioms to allow infinite distances. This makes it possible to measure distance between functions with common domain and codomain as the supremum of the distance between their values over their domain. An alternative would be to restrict ourselves to consider bounded metric spaces.

Definition 2.3 We denote by δ^{∘}(x, ϵ) the open disk with radius ϵ > 0 and center x in M , that is, the set { y ^{∈} M | d(x, y) < ϵ } . The corresponding closed disk δ(x, ϵ) is the set { y ^{∈} M | d(x, y) ≤ ϵ } . We allow radius 0 for closed disks. In general, a subset A ⊆ M is open if for every a ^{∈} A there exists an open disk completely within A with a a center. A subset is closed if it is the complement of an open subset. By the diameter of a subset we understand the supremum of the set of distances between points in the subset. □

Definition 2.4 A sequence (a_{n})_{n^{∈}ℕ} of elements of a metric space is Cauchy if

∀ϵ > 0. ∃N ^{∈} ℕ. ∀m, n ≥ N. d(a_{n}, a_{m}) ≤ ϵ .  □

Definition 2.5 A sequence α = (a_{n})_{n^{∈}ℕ} converges to a if

∀ϵ > 0. ∃N ^{∈} ℕ. ∀n ≥ N. d(a_{n}, a) ≤ ϵ .

In this case we write a = lim_{n^{∈}ℕ} α , and call a the limit of α . □

To adhere with categorical terminology we should really call the metric limit a colimit. When it seems more suggestive we will write ‘α_{n} → a as n → ∞’ to denote a = lim_{n^{∈}ℕ} α .

Proposition 2.1 A sequence (a_{n})_{n^{∈}ℕ} converges to a if d(a_{n}, x) → d(a, x) as n → ∞ for all x ^{∈} M . □

Definition 2.6 A metric space is complete if every Cauchy sequence has a limit. □

Definition 2.7 A subspace N ⊆ M of a metric space (M, d) is dense in M if every element in M is a limit of a Cauchy sequence from N. □

We give without proof the following crucial proposition about metric spaces and the notion of completeness that we have just described.

Proposition 2.2 Every metric space (M, d) can be embedded isometrically and dense in a complete metric space, which we will denote (\overline{M}, \overline{d}), and every continuous function from M can be uniquely extended to a continuous function from \overline{M}. The completion thus described is unique up to isometry. □

Definition 2.8 A function between metric spaces is continuous if it preserves Cauchy sequences and their limits. □

Proposition 2.3 A function f : A → B is continuous if

∀ϵ > 0. ∀x, y ^{∈} A. ∃δ > 0. d(x, y) ≤ δ → d(f(x), f(y)) ≤ ϵ .  □

Definition 2.9 A metric space (M, d) is an ultra-metric space if it fulfills the strong triangular inequality d(x, y) ≤ max{d(x, z), d(z, y)} for all x, y, z ^{∈} M. □

Notice that the strong triangular inequality says that every triangle in an ultra-metric space is isosceles with two long legs and one short leg (or all three legs can be of the same length). The strong triangular inequality seems on the face of it a quite strong requirement, but it turns out that there are many very interesting ultra-metric spaces. The prime application of ultra-metric spaces is in the field of p-adic analysis ([Schikhof 84]), but we will give an example closer to semantic applications.

Example 2.1 Let Σ be a set (the alphabet) and consider Σ^{ω} the set of countably infinite lists (words) of elements of Σ . Define [x, y] for two words x and y to be the first index where they differ, ∞ if they are equal. Then we can define

d(x, y) = 2^{−[x,y]} .

Here we take 2^{−∞} = 0 . Then it is easy to see that d(x, y) = 0 if and only if x = y , and that d is symmetric. To see that the strong triangular inequality holds, let x, y, and z be given. To show max{d(x, y), d(y, z)} ≥ d(x, z) is the same as showing min{[x, y], [y, z]} ≤ [x, z], but this is obvious: if x and y agree up to some index, and y and z agree up to some index, then x and z must agree at least up to the minimum of the two indices. □

Definition 2.10 We denote by Met the category of metric spaces with possibly infinite distances and conservative maps. CMet denotes the full sub-category thereof, consisting of the complete spaces. Ult denotes the full subcategory of Met consisting of the ultra-metric spaces, and CUlt the finally the complete ultra-metric spaces, the ‘intersection’ of CMet and Ult . □

Definition 2.11 A ultra-metric space (M, d) is distance discrete if for any two sequences (x_{n})_{n^{∈}ω}, (y_{n})_{n^{∈}ω}, if d(x_{1}, y_{1}) > d(x_{2}, y_{2}) > …, then lim_{n→∞} d(x_{n}, y_{n}) = 0. □

The above notion is called ‘discrete’ by Schikhof in ([Schikhof 84]), but to avoid ambiguity we use ‘distance discrete’ instead. We see that distance discreteness is a requirement on the set of realized distances (i.e. the set of ϵ such that there exists points that are precisely ϵ apart) viz. that any sharply decreasing sequence of realized distances converges to 0 .

We recall some standard properties of closed and open subsets without proof. For an exposition, see any textbook on topology, for instance [Bourbaki 89] or [Dugundji 66].

Proposition 2.4 A subset of a metric space is open if every Cauchy sequence that converges to a point within the subset, also shares an element with the subset. □

It is immediate that a convergent Cauchy sequence that from some point on lies entirely within a closed subset, also has its limit point in the closed subset. It is also evident that any union of open subsets is open, dually, that any intersection of closed subsets is closed. Further, any finite intersection of open subsets is open, and any finite union of closed subsets is closed.

Definition 2.12 We write cl(N) for the closure of the subset N of a metric space M, which is the intersection of all closed subsets of M that contain N . □

From [Schikhof 84] we take the following proposition.

Proposition 2.5 In an ultra-metric space

(i) every two disks are either disjoint or one is a subset of the other, and

(ii) every disk is both open and closed.

Proof : For (i), let S_{1} = {y ^{∈} X | d(x_{1}, y) < ϵ_{1}} and S_{2} = {y ^{∈} X | d(x_{2}, y) < ϵ_{2}} be two disks. If z ^{∈} S_{1} ∩ S_{2} we have d(x_{1}, z) < ϵ_{1} and d(x_{2}, z) < ϵ_{2}. Assume without loss of generality that ϵ_{1} ≤ ϵ_{2}. By ultra-metricity d(x_{1}, x_{2}) < max{ϵ_{1}, ϵ_{2}} = ϵ_{2}. Let v ^{∈} S_{1}. Then d(v, x_{2}) ≤ max{d(v, x_{1}), d(x_{1}, x_{2})} ≤ max{ϵ_{1}, ϵ_{2}} = ϵ_{2}, so v ^{∈} S_{2}.

For (ii), let ϵ > 0 and x_{0} ^{∈} X be given. We will prove that S = {y ^{∈} X | d(x_{0}, y) < ϵ} is closed. Let (x_{n})_{n^{∈}ω} be a sequence in S with limit x. Assume without loss of generality that (ϵ_{n})_{n^{∈}ω} = (d(x_{n}, x))_{n^{∈}ω} is strictly decreasing or constantly 0 from some point on. Let S_{n} = {y ^{∈} X | d(x, y) < ϵ_{n}} for all n ^{∈} ω. Then x_{n+1} ^{∈} S_{n}, and consequently S_{n} ∩ S ≠ ∅ for all n ^{∈} ω. From (i) we get that S_{n} ⊆ S for every n ^{∈} ω, so since x ^{∈} S_{n}, we have x ^{∈} S. □

Observation 2.1 Theorem 2.5.(i) implies that the set of disks of an ultra-metric space is a partial order with a tree structure.

Definition 2.13 An ultra-metric space is spherically complete if each nested sequence of disks has a non-empty intersection. □

It is easy to see that a complete, distance discrete ultra-metric space is spherically complete: Let (B_{n})_{n^{∈}ω} be a nested sequence of disks in (M, d). Without loss of generality assume they are all different. This implies that their diameters form a strictly decreasing sequence (that is, diam B_{n} > diam B_{n+1} for all n ^{∈} ℕ). As a consequence of distance discreteness lim_{n→∞} diam(B_{n}) = 0. By completeness, the intersection is not empty.

In an ultra-metric space convergence is easier than in a general metric space in the following sense.

Definition 2.14 A sequence (x_{n})_{n^{∈}ω} is called narrowing if lim_{n→∞} d(x_{n}, x_{n+1}) = 0. □

Proposition 2.6 In an ultra-metric space a sequence is Cauchy if and only if it is narrowing.

Proof : It is obvious that a Cauchy sequence is narrowing. To see that a narrowing sequence is Cauchy, let (x_{n})_{n^{∈}ω} be narrowing in an ultra-metric space. For n ≤ m we have d(x_{n}, x_{m}) ≤ max{d(x_{n}, x_{n+1}), d(x_{n+1}, x_{n+2}), …, d(x_{m−1}, x_{m})}. Given ϵ > 0 we can find N ^{∈} ℕ such that d(x_{n}, x_{n+1}) ≤ ϵ for all n ≥ N , and consequently d(x_{n}, x_{m}) ≤ ϵ . □ Notice, that in a general metric space this is not a theorem. Take e.g. x_{n} = ∑_{i=1}^{n} \frac{1}{n} in the Euclidian space.

We can define product and function space on Met as follows.

Definition 2.15 The product A×B of two metric spaces A and B is the set-theoretic product of their set components equipped with the max-distance, that is d_{A×B}((a, b), (a′, b′)) = max{d(a, a′), d(b, b′)} . The function space A → B is the set of conservative maps from A to B equipped with the sup-distance, that is d(f, g) = sup_{a^{∈}A} d(f(a), g(a)) .

It is easy to see that the product we have defined above is already a categorical product in Met . The function space is not an exponent in Met , however. Theorem 2.2 makes the situation clear. The following theorem is folklore (at least I did not manage to find it in any reference, which of course does not mean that it has not been written down somewhere).

Theorem 2.2 The largest Cartesian closed full subcategory of Met is Ult.

Proof : It is easy to prove that Ult is Cartesian closed. Notice, that we have to allow infinite distance in order for the distance always to be defined on two functions with the same domain and codomain.

To see (with a highly non-constructive proof) that the restriction to ultra-metric spaces is necessary, consider a category in which an object B is not an ultra-metric space. This means that we have points b, b′, b′′ ^{∈} B such that d_{B}(b, b′′) > max{d_{B}(b, b′), d_{B}(b′, b′′)}. Assume without loss of generality that d_{B}(b, b′) ≥ d_{B}(b′, b′′), and define f : B → B by f(b) = b′ and f(b′) = f(b′′) = b′′. Clearly f is conservative, but we can use f and id_{B} to show that ev_{B,B} is not! Here ev_{B,B} stands for the evaluation mapping that takes a pair consisting of a function from B to B and an element of B into the value of the function evaluated at the element. For ev_{B,B} to be conservative it has (for instance) to hold that d_{B}(id_{B}(b), f(b′)) ≤ max{d_{B^{B}}(id_{B}, f), d_{B}(b, b′)}, that is, d_{B}(b, f(b′)) = d_{B}(b, b′′) ≤ max{sup_{x^{∈}B} d_{B}(x, f(x)), d_{B}(b, b′)}, but the latter is d_{B}(b, b′), and so we violate our assumption. □ The theorem also holds if we replace the above categories with the sub-categories of complete metric and ultra-metric spaces.

As remarked earlier, every metric space can be embedded isometrically and densely in a complete metric space, its completion. We have an adjunction where the completion functor is left adjoint to the forgetful functor. Writing \overline{M} for the metric completion of a metric space M we have an isomorphism between conservative maps f : M → C and \overline{f} : \overline{M} → C with C complete. We already knew this: a continuous function can be uniquely extended to the completion of its domain. It is not surprising that if the original function is an conservative map then so is the extension.

2.2.2 Denotational semantics for processes

We will briefly introduce how metric spaces have been used to provide models for processes. For this purpose we will base ourselves on the work of de Bakker and Zucker ([de Bakker & Zucker 82] and [de Bakker & Zucker 82b]).

Deterministic, applicative processes

As a first example, consider deterministic processes that can only perform events from the alphabet A. Thus a process is just a list of events, taken from A, possibly ending with a special symbol (√, say) which is not an element of A and which marks termination. The corresponding type equation is

P = {√} + A × P .

Thus, these simplified processes are basically lists.

As a semantic domain for the solution to the equation above, de Bakker and Zucker use a metric space. The idea behind de Bakker and Zucker’s metric on lists is that since the lists are processes, there is a chronology on the elements. Two lists are close if you have to watch them for a long time to detect any difference. So if n is the first index where (x_{1}, x_{2}, …) and (y_{1}, y_{2}, …) differ, then we define their distance to be 2^{−n+1}. If they never differ, then of course their distance is 0 (see also Example 2.1). If one sequence stops before the other, they we say that they differ (at least) at the index at which only one of the lists have an element.

We can obtain a solution to the above mentioned type equation by the following iteration:

\begin{aligned}P_{0} & = & ∅ , \\ P_{n+1} & = & \{√\} ∪ A × P_{n}, for n > 0 , \\ P & = & ⋃_{n^{∈}ω} P_{n} , \end{aligned}

with the metric

d((x_{1}, x_{2}, …), (y_{1}, y_{2}, …)) = \{ \begin{matrix}0 & if & \overline{x} = \overline{y} , \\ 2^{−n+1} & if & n = min\{k ^{∈} ω|x_{k} ≠ y_{k}\}. \end{matrix}

With a little rewriting we have that

P = ⋃_{n^{∈}ω}{A_{1} × … × A_{n} × {√}|A_{1} = … = A_{n} = A}

with the metric indicated above. However, if we want a solution in CMet, the category of complete metric spaces with conservative maps, then we need to complete P:

P = \overline{⋃_{n^{∈}ω} P_{n}} ,

Then we are able to define processes (i.e. lists) recursively, as in p = a :: p for the process that outputs an infinite stream of a’s. The p thus specified is the limit of the Cauchy sequence

√, a√, aa√, aaa√, …

The distance between the n’th process and the n+1’st is 2^{−n+1}, which converges to 0. Due to the fact that we are now working with equivalence classes of Cauchy sequences, P is now only a solution to our type equation up to isomorphism.

Non-deterministic, imperative processes

Having solved the first equation does not bring us not very far towards giving a denotational semantics to a language à la CSP or CCS for concurrent processes. As de Bakker and Zucker discuss, we have to take care of non-determinism and state dependency (imperativeness).

To explain non-determinism we need something like the following equation.

P = {√} + ℘(A × P) ,

where ℘ is a power set operator yielding some subset of the set of subsets of its argument. The intuition about the equation is that a process either stops or has a choice among a set of possible continuations. Each continuation consists of performing an action from A and behaving like some process again. We know from set theory that if we allow ℘(X) to denote the set of all subsets of X, then we have no hope of a solution to the above equation. We shall see later, which subset of the set of subsets of X it is adequate to let ℘(X) denote in order to have a solution.

To explain state dependency and non-determinism combined we need something like the following equation.

P = {√} + Σ → ℘(A × Σ × P) .

The intuition is that a process either stops or yields a choice among a set of triples consisting of an action, a new state, and a new process. The choice depends on the state.

By now we see that for such equations we need a language of types containing basic types like A for the alphabet, possibly 2 , ℕ, and {√}, and type operators for +, ×, →, and ℘ . The basic types should be complete metric spaces, and the type operators should be functions mapping one or two complete metric spaces into a complete metric space.

It is possible to use as motivation for the choices of type operators the idea of distance between two elements x and y being inversely proportional to the time needed to distinguish them by some non-deterministic algorithm that follows the structure of the elements (or equivalently by the size of the proof needed to prove that they are different). It should be pointed out, that this is ours and not de Bakker and Zucker’s motivation (so historically it is more a rationalization than a motivation). It should also, as a minor point, be noticed that actually, for convenience and in order to follow de Bakker and Zucker accurately, the distance is inversely proportional with 2 to the effort to distinguish two elements.

Booleans and natural numbers are defined as basic types. A singleton type, 1l, is also defined. We will assume that the distance between any different x and y in any basic type is ∞. Such metric spaces—where distances are either 0 or ∞—are called discrete metric spaces.

Definition 2.16 The metric space 1l is the singleton set {√} with the trivial metric. The metric space 2 is the two-element set {⊤, ⊥} with the discrete metric. The metric space ℕ is the countably infinite set {0, 1, 2, …} with the discrete metric. □

Definition 2.17 Disjoint sum is defined such that elements from different components are as far away from each other as possible. Elements from the same component inherit their distance from the component.

(M_{0}, d_{0}) + (M_{1}, d_{1}) = ({0} × M_{1} ∪ {1} × M_{2}, d), where
d((i, x), (j, y)) = \{ \begin{matrix}d_{k}(x, y) & if i = j = k ^{∈} \{0, 1\} , \\ ∞ & otherwise. \end{matrix}
□

Definition 2.18 Asymmetric product is defined such that the distance between two elements is the distance between their first coordinates, if they differ, else half the distance of their second coordinates.

(M_{0}, d_{0}) × (M_{1}, d_{1}) = (M_{0} × M_{1}, d), where
d((x_{0}, x_{1}), (y_{0}, y_{1})) = \{ \begin{matrix}d_{0}(x_{0}, y_{0}) & if & x_{0} ≠ y_{0}, \\ \frac{1}{2}d_{1}(x_{1}, y_{1}) & if & x_{0} = y_{0}. \end{matrix}
□

The asymmetric product can be used in modeling the chronology of events in a process. The longer you have to watch two processes to detect a difference, the less they differ. So a (deterministic) process can be an element of a layered product where the left element comes before the right ones. Later we shall see that the asymmetric product is unnecessary, and we will follow America and Rutten and introduce a symmetric product.

Definition 2.19 The function space from one metric space to another is defined as the set of conservative functions. The metric on the function space is the supremum-norm.

(M_{0}, d_{0}) → (M_{1}, d_{1}) = (M_{0} →_{c} M_{1}, d), where
M_{0} →_{c} M_{1} = {f ^{∈} M_{0} → M_{1}|∀x_{0}, y_{0} ^{∈} M_{0}. d_{1}(f(x_{0}), f(y_{0})) ≤ d_{0}(x_{0}, y_{0})}, and
d(f, g) = sup_{a^{∈}A} d_{B}(f(a), g(a)).
□

The function arrow occurring on the right-hand side of the definition above is of course the usual set theoretic function constructor, yielding all functions. In the sequel we will omit the subscript ‘c’ on the function arrow, and always assume that a function is conservative.

It should be noticed that every conservative map is continuous. The reason for not choosing simply continuous functions (or uniformly continuous functions) as the morphisms of our category seems subtle at this point. However, when we consider enriched categories as a foundation for a unification in Chapter 3, the conservative maps come out as the canonical choice for morphisms. For now, let it suffice with an example.

Example 2.2 Consider the P defined by the first of our equations:

P = {√} + A × P .

What are the conservative maps from P to P? Before answering this question we introduce the function L that takes two lists as arguments and yields the length of their longest common prefix.

f ^{∈} P → P iff ∀x, y ^{∈} P. d_{P} (f(x), f(y)) ≤ d_{P} (x, y)
iff ∀x, y ^{∈} P. [f(x) = f(y) ∨ L(f(x), f(y)) ≥ L(x, y)] .

So we see that conservative maps map elements into images that are either equal or have a common prefix of at least the same length as the longest common prefix of the elements they came from. Saying it briefly, we could say that the conservative maps respect prefix agreements. □

Concerning the power-set operator, we again have to define a set and a distance component. To determine the distance component we need to extend a metric on a set to a metric on (a subset of) the subsets of a set. To determine the set component we need to decide on a suitable subset of the subsets of a metric space.

It turns out that we can use the well-known Hausdorff metric between sets, and by doing that, de Bakker and Zucker obtain an intuitively appealing measure of distance between processes that might be non-deterministic. De Bakker and Zucker have chosen the set component to be the closed subsets, and we have the following definition.

Definition 2.20 The power-set of a metric space is the set of closed subsets of the space, equipped with the Hausdorff metric.

℘(A, d_{A}) = ({X ⊆ A|X closed }, d), where
d(X, Y) = max{sup_{x^{∈}X} inf_{y^{∈}Y} d_{A}(x, y), sup_{y^{∈}Y} inf_{x^{∈}X} d_{A}(x, y)}.
□

Note, that we do not have any problems with empty sets. In fact

d(X, ∅) = \{ \begin{matrix}0 if X = ∅ \\ ∞ otherwise. \end{matrix}

De Bakker and Zucker showed that with the above definitions it is possible to solve all three kinds of equations we have shown. An important property of the type operators is that they preserve completeness. This makes it possible to conceive recursively defined values of any of the types obtained as solutions to recursive type equations. Thus processes can be defined recursively and a solution to their defining equation found in the denotation of the types of our universe as outlined above.

We have not yet described the limitations of this approach—what kind of domain equations can be solved within the given framework. In the next section we will answer that question for a slightly generalized setting.

2.2.3 Solving general domain equations with metric spaces

We will here describe how the technique of de Bakker and Zucker was generalized by America and Rutten ([America & Rutten 87]), plus notice a few comments and corrections of our own in this connection. America and Rutten’s category has as objects complete metric spaces with diameter at most 1, and as morphisms conservative maps. We can instead work with the category CMet, since there is a straightforward isomorphism between the two categories.

The approach outlined above very naturally lead to the question of the limitations of this metric space approach to solving recursive domain equations. Pierre America and Jan Rutten presented in [America & Rutten 87] a generalization of de Bakker and Zucker’s approach that facilitates the solution of equations like

P = (P → P) + A ,

with the proviso that some shrinking has to occur. We will return to this point later. The above equation is more difficult than the above equations because of the left P on the righthand side of the equation. We will give a brief description of America and Rutten’s general method of solving domain equations involving the type operators +, ×, →, ℘, and id_{ϵ}. Of these operators +, →, and ℘ work like already described. Below we define the new × and id_{ϵ}.

This time × is symmetric, corresponding to the idea that we check (x_{0}, x_{1}) ≠ (y_{0}, y_{1}) by checking in parallel x_{0} ≠ x_{1} and y_{0} ≠ y_{1}.

Definition 2.21 The Cartesian product is the set-theoretic product with the max-norm.

(M_{0}, d_{0}) × (M_{1}, d_{1}) = (M_{0} × M_{1}, d), where
d((x_{0}, x_{1}), (y_{0}, y_{1})) = max{d_{0}(x_{0}, y_{0}), d_{1}(x_{1}, y_{1})}.

□

Concerning id_{ϵ}, actually this is a family of type operators, indexed by ϵ which can be any real number in the half-open interval (0, 1]. The function id_{ϵ} multiplies every distance of its argument by ϵ, but leaves otherwise the points unchanged. Under one hat we call these operators down-scalers.

Definition 2.22 The family of down-scalers is id_{ϵ}(M, d) = (M, ϵ · d), indexed by ϵ ^{∈} (0, 1]. □

We can see that we can obtain the same effect as the asymmetrical product with a combination of the new product and the id_{ϵ}-operator. What solved the equation P = 1l + A × P before, now solves P = 1l + A × id_{\frac{1}{2}} P .

Actually the generality of id_{ϵ} is an overkill. We only need id_{\frac{1}{2}} . With our connection between effort to distinguish elements and distance we can read id_{\frac{1}{2}} as signaling a structural depth of the argument, making it twice as difficult to access it. With this reading it would make better sense to demand every occurrence of the left-hand type name on the right-hand side to be subjected to id_{\frac{1}{2}} . In fact this approach works, but we will be faithful to America and Rutten and retain the general id_{ϵ}.

In the following we will show how one can isolate a nice, large class of type equations that have solutions. The method of solution is extremely similar to the so-called inverse limit approach of Scott ([Scott 72]) which we just sketched in Section 2.1.

Definition 2.23 A retraction pair is a pair (ϕ, ψ) of weak contractions, ϕ : A → B and ψ : B → A such that ψ ∘ ϕ = id_{A}. We call ψ the projection, ϕ the embedding, and A the retract of B. Sometimes we write the retraction pair like ϕ : A ↔ B : ψ for brevity. □

Proposition 2.7 All embeddings are isometries.

Proof : To see this, let a_{1}, a_{2} ^{∈} A. We will show that d_{A}(a_{1}, a_{2}) = d_{B}(ϕ(a_{1}), ϕ(a_{2})). Let b_{1} = ϕ(a_{1}) and b_{2} = ϕ(a_{2}). Since ψ ∘ ϕ = id_{A}, we know that ψ(b_{1}) = a_{1} and ψ(b_{2}) = a_{2}. Using the fact that both ψ and ϕ are conservative we get

d_{B}(b_{1}, b_{2}) = d_{B}(ϕ(a_{1}), ϕ(a_{2})) ≤ d_{A}(a_{1}, a_{2}) = d_{A}(ψ(b_{1}), ψ(b_{2})) ≤ d_{B}(b_{1}, b_{2}).

□

It follows that B from definition 2.23 contains an isometric copy, ϕ(A), of its retract A.

Notice, that functors preserve retraction pairs, that is, if (ϕ, ψ) is a retraction pair and F a functor, then (F (ϕ), F (ψ)) is a retraction pair.

Definition 2.24 The noise δ(ϕ, ψ) of a retraction pair ϕ : A ↔ B : ψ is defined as

sup_{b^{∈}B} d(b, ϕ ∘ ψ(b)).  □

Thus the noise measures the maximum ‘inaccuracy’ you can experience by going from B to A and back, that is, how well A approximates B. From our definition of function spaces we see that δ(ϕ, ψ) = d(id, ϕ ∘ ψ). Another, not completely equivalent measure of the same thing, would be d(ϕ(A), B), d being the Hausdorff distance generated by d_{B}.

Proposition 2.8 In an ultra-metric space we have for a retraction pair (ϕ, ψ) from A to B that d_{B→B}(ϕ ∘ ψ, id_{B}) = d_{℘B}(ϕ(A), B).

Proof : First notice that

d_{B→B}(ϕ ∘ ψ, id_{B}) = sup_{b^{∈}B} d_{B}(ϕ ∘ ψ(b), b)
≥ sup_{b^{∈}B} inf_{a^{∈}A} d_{B}(ϕ(a), b)
= d_{℘B}(ϕ(A), B).

We have the last equality because ϕ(A) ⊆ B. To go the other way, first observe that d_{℘B}(B, ϕ(A)) = d_{℘B}(B, \overline{ϕ(A)}) = d_{℘B}(B, ϕ(\overline{A})). Then let b ^{∈} B and choose a′ ^{∈} A such that inf_{a^{∈}A} d_{B}(ϕ(a), b) = d_{B}(ϕ(a′), b). We thus have to show that d_{B}(ϕ ∘ ψ(b), b) ≤ d_{B}(ϕ(a′), b). But d_{B}(ϕ ∘ ψ(b), b) ≤ max{d_{B}(ϕ ∘ ψ(b), ϕ(a′)), d_{B}(ϕ(a′), b)}, and we have

d_{B}(ϕ ∘ ψ(b), ϕ(a′)) = d_{A}(ψ(b), a′)
= d_{A}(ψ(b), ψ(ϕ(a′)))
≤ d_{B}(b, ϕ(a′)).
□

Definition 2.25 A functor F is contracting if there exists a constant ϵ < 1 such that F reduces the noise of every retraction pair with at least the factor ϵ , that is, for every retraction pair ϕ : A ↔ B : ψ , it holds that δ(F (ϕ), F (ψ)) ≤ ϵ · δ(ϕ, ψ) . We say that F is weakly contracting when ϵ is allowed to be 1 . □

Definition 2.26 A chain of metric spaces is a sequence (M_{i})_{i^{∈}ω} of metric spaces with connecting retraction pairs (ϕ_{i}, ψ_{i})_{i^{∈}ω}, such that ϕ_{i} : M_{i} ↔ M_{i+1} : ψ_{i} for all i ^{∈} ω. □

[figure: M_{0}; M_{1}; M_{2}; ⋯; ϕ_{0}; ψ_{0}; ϕ_{1}; ψ_{1}; ϕ_{2}; ψ_{2}]

For any such chain we give special names for the compositions of sequences of embeddings and projections. The functions τ_{nm} : M_{n} → M_{m} are defined as follows.

τ_{ij}(m_{i}) = \{ \begin{matrix}ψ_{j} ∘ ψ_{j−1} ∘ … ∘ ψ_{i−1}(m_{i}) & if & i > j \\ m_{i} & if & i = j \\ ϕ_{j−i} ∘ ϕ_{j−2} ∘ … ∘ ϕ_{i}(m_{i}) & if & i < j, \end{matrix}

One way to generate a chain of metric spaces is to use a functor repeatedly. Let F be a functor and M = {m} a one-point metric space. Assume F (M) ≠ {}. Choose an element n ^{∈} F (M). Then we can define a retraction pair ϕ : M ↔ F (M) : ψ by defining ϕ(m) = n and ψ(x) = m for every x ^{∈} F (M). F is a functor, so it preserves retraction pairs. Therefore

[figure: M; F (M); F (F (M)); ⋯; ϕ; ψ; F (ϕ); F (ψ); F (F (ϕ)); F (F (ψ))]

is a chain of metric spaces.

Following America and Rutten’s terminology we introduce so-called weak limits.

Definition 2.27 A weak limit of a chain of metric spaces (M_{i}, (ϕ_{i}, ψ_{i}))_{i^{∈}ω} is a pair (D, (Φ_{i}, Ψ_{i})_{i^{∈}ω}), such that for all i ^{∈} ω

(i) (D, (Φ_{n})_{n^{∈}ℕ}) is a cone over the embedding part of the chain, and (D, (Ψ_{n})_{n^{∈}ℕ})) is a cocone over the projection part of the chain, that is,

[figure: D; M_{i}; M_{i+1}; Φ_{i}; Φ_{i+1}; ϕ_{i}; and; D; M_{i}; M_{i+1}; Ψ_{i}; Ψ_{i+1}; ψ_{i}; commute.]

(ii) Φ_{i} : M_{i} ↔ D : Ψ_{i} is a retraction pair.

(iii) For any (D′, (Φ′, Ψ′)) with the properties (i) and (ii) there exists a retraction pair α : D ↔ D′ : β.

□

Definition 2.28 A limit is a weak limit where the retraction pair in 2.27.(iii) is always unique. This is then a categorical limit in the category of metric spaces with retraction pairs as morphisms (in the direction of the projections). □

The limit is, when it exists, unique up to isometry. From America and Rutten we distill the following theorem.

Theorem 2.3 When the diagram D_{0}→^{ϕ_{0}} ; ←_{ψ_{0}}D_{1}→^{ϕ_{1}} ; ←_{ψ_{1}}D_{2}→^{ϕ_{2}} ; ←_{ψ_{2}} ⋯ in the category of complete metric

spaces with conservative maps fulfills (i) ψ_{n} ∘ ϕ_{n} = id_{D_{n}} ,

(ii) ∀ϵ > 0. ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. d(τ_{nm} ∘ τ_{mn}, id_{D_{m}}) ≤ ϵ ,

then there exists D and (Φ_{n}, Ψ_{n})_{n^{∈}ℕ} such that (D, (Φ_{n})_{n^{∈}ℕ}) is a colimit for D_{0} →^{ϕ_{0}} D_{1} →^{ϕ_{1}} D_{2} …

and (D, (Ψ_{n})_{n^{∈}ℕ}) is a limit for D_{0} ←_{ψ_{0}}D_{1} ←_{ψ_{1}}D_{2} …. Further Ψ_{n}∘Φ_{n} = id_{D_{n}} and Φ_{n}∘Ψ_{n} ≤ id_{D}

for all n ^{∈} ℕ . □

Please compare with Theorem 2.1! Only condition (ii) is modified, but the modification looks quite severe. The condition for pre-orders is of a local character, just concerning each individual retraction pair, whereas the metric version concerns the whole sequence of retraction pairs. As we shall see, however, the two conditions can be unified.

Further, America and Rutten showed the following theorem ([America & Rutten 87]). Those familiar with the D_{∞} construction will recognize the precise structure of that construction given in the proof.

Theorem 2.4 If F is a contracting functor, all chains generated by it have limits. The limits are fixed-points of the functor.

Outline of Proof : The fixed-point can be constructed in the following way. Let ϕ : M ↔ F (M) : ψ be a retraction pair and (M_{i}, (ϕ_{i}, ψ_{i}))_{i^{∈}ω} the generated chain, where M = M_{0}, ϕ = ϕ_{0}, and ψ = ψ_{0}. Define

D = {(x_{i})_{i^{∈}ω}|∀i ^{∈} ω. [x_{i} ^{∈} M_{i} ∧ x_{i} = ψ_{i}(x_{i+1})]}

and a metric d on D by

d(\overline{x}, \overline{y}) = sup_{i^{∈}ω} d_{i}(x_{i}, y_{i}) ,

where, of course, d_{i} is the metric on M_{i} and x_{i} (y_{i}) is the i’th element of \overline{x} (\overline{y}). Define further Φ_{i} : M_{i} → D, and Ψ_{i} : D → M_{i} as follows.

\begin{aligned}Φ_{i}(m_{i}) & = & (τ_{ij}(m_{i}))_{j^{∈}ω}, \\ Ψ_{i}(\overline{x}) & = & x_{i}. \end{aligned}

Then it is easy to check that ((D, d), (Φ_{i}, Ψ_{i})_{i^{∈}ω}) is a limit of (M_{i}, (ϕ_{i}, ψ_{i}))_{i^{∈}ω} and (D, d) is a fixed-point (up to isometry) of F. □

Notice, that we have silently assumed a number of lemmas, such that d defined above is in fact a metric. All the details can be found in [America & Rutten 87].

We now have all the tools ready to solve domain equations. All we have to do is to translate the domain equations we want to solve, into fixed-point equations for contracting functors. Each type operator will correspond to a functor. Since we have already defined the metric space component of the functors corresponding to the type operators, we just have to define how the type operators work on weak contractions. This is done below.

Assume in the following that f : (M_{0}, d_{0}) → (M_{1}, d_{1}) and g : (M_{2}, d_{2}) → (M_{3}, d_{3}).

(f + g)((i, x)) = \{ \begin{matrix}(0, f(x)) & if & i = 0 & (so x ^{∈} M_{0}), \\ (1, g(x)) & if & i = 1 & (so x ^{∈} M_{2}), \end{matrix}
(f × g)(m_{0}, m_{2}) = (f(m_{0}), g(m_{2})),
(f → g)(h)  = λm_{0} : M_{0}. g ∘ h ∘ f(m_{0}),
℘f(m)  = cl(f(m)),
id_{ϵ}f  = f,

As noted in [America & Rutten 87], the operators +, ×, →, and ℘ are all conservative, while the nullary functors 1l, 2, ℕ, and id_{ϵ} are contractions. Obviously, a composition of a conservative map with a contraction is a contraction. Thus the set of recursive type equations of the form

D = F (D)

solvable in America and Rutten’s framework contain those equations where F is build up using the above defined type operators, where every occurrence of D sits inside an application of id_{ϵ}.

We have already seen in Theorem 2.2 that America and Rutten’s category is not Cartesian closed, and that with the choice of morphisms it is necessary to restrict to ultra-metric spaces.

To see a specific counter-example, consider the following example.

Example 2.3 What we will show is that for some choices of A and B the evaluation function is not a morphism in the category. To see this, consider the following.

Let A = \{0, \frac{1}{2}\} with Euclidian distance (i.e. d_{A}(0, \frac{1}{2}) = \frac{1}{2}). Let B = \{0, \frac{1}{2}, 1\}, also with Euclidian distance. A and B are finite, thus complete. Their diameter is \frac{1}{2} and 1 respectively, so they are objects of the category CMet. Let f, g : A → B be defined thus: f(a) = a for a ^{∈} A, and g(a) = a + \frac{1}{2}. Clearly f and g are morphisms in the category. Let a_{1} = 0 and a_{2} = \frac{1}{2}. Then

d_{B}(ev_{A,B}(f, a_{1}), ev_{A,B}(g, a_{2})) = d_{B}(f(a_{1}), g(a_{2})) = 1,

but

d_{B^{A}×A}((f, a_{1}), (g, a_{2})) = max\{d_{B^{A}}(f, g), d_{A}(a_{1}, a_{2})\} = max\{\frac{1}{2}, \frac{1}{2}\} = \frac{1}{2},

so

d_{B}(ev_{A,B}(f, a_{1}), ev_{A,B}(g, a_{2})) > d_{B^{A}×A}((f, a_{1}), (g, a_{2})),

implying that ev_{A,B} isn’t a weak contraction.

What goes wrong is that in B^{A} × A we can change both function and argument, thereby making the difference in result values exceed both the difference in functions and the difference in arguments. □

If we only deal with ultra-metric spaces we can obtain some simplifications, however. As easy consequences of proposition 2.6 we get the following.

Corollary 2.1 Every chain of ultra-metric spaces where the noise of the mediating retraction pairs converge to zero has a limit.

Proof : Construct D_{∞} as above and observe that the metric space of conservative maps Φ_{n} ∘ Ψ_{n} from D_{∞} via the D_{n}’s back to D_{∞} is an ultra-metric space, and that (Φ_{n} ∘ Ψ_{n})_{n^{∈}ω} is a narrowing sequence, since the pairwise distance between two successive elements is the noise of the retraction pairs between the corresponding D_{n}’s. □

As a consequence of this then, we can relax the requirements imposed on functors to ensure that they have unique fixed-points.

Conjecture 2.1 An endo-functor F : CUlt → CUlt for which F 1l ≠ ∅ and where d(F^{n}f, F^{n}g) converges towards 0 for n → ∞ for any pair of morphisms f and g has a unique fixed-point.

Proof : The chain generated by applying F repeatedly to 1l and choosing an arbitrary point in F 1l fulfills the condition in corollary 2.1. If we verify that F preserves converging chains and their limits, we can mimic the proof of theorem 3.14 in [America & Rutten 87]. □ In other words, for functors on ultra-metric spaces we do not need the uniform ϵ convergence.

Completeness and ultra-metricity are both preserved by the inverse limit construction.

Theorem 2.5 The limit construction preserves completeness.

Proof : Let (\overline{x}^{i})_{i^{∈}ω} be a Cauchy sequence in D = \{(x_{i})_{i^{∈}ω}|∀i ^{∈} ω. [x_{i} ^{∈} M_{i} ∧ x_{i} = ψ_{i}(x_{i+1})]\}. For any ϵ > 0 there exists N ^{∈} ω such that for all m, n ≥ N, we have d(\overline{x}^{m}, \overline{x}^{n}) < ϵ. But the latter means

∀m, n ≥ N. ∀i ^{∈} ω. d_{i}(\overline{x}_{i}^{m}, \overline{x}_{i}^{n}) < ϵ.

Thus especially

∀ϵ > 0. ∀i ^{∈} ω. ∃N ^{∈} ω. ∀m, n ≥ N. d_{i}(\overline{x}_{i}^{m}, \overline{x}_{i}^{n}) < ϵ,

so (\overline{x}_{i}^{n})_{n^{∈}ω} is a Cauchy sequence in (M_{i}, d_{i}) for every i ^{∈} ω, and since (M_{i}, d_{i}) is complete, it is permissible to define

x_{i} = lim_{n→∞} \overline{x}_{i}^{n}.

It is then easy to see that (x_{i})_{i^{∈}ω} is a limit for (\overline{x}^{i})_{i^{∈}ω}. □

Theorem 2.6 The limit construction preserves ultra-metricity.

Proof : Assume all M_{i}’s from the construction of D are ultra-metric spaces.

d(\overline{x}, \overline{z}) = sup_{i^{∈}ω} d_{i}(\overline{x}_{i}, \overline{z}_{i})
≤ sup_{i^{∈}ω} max\{d_{i}(\overline{x}_{i}, \overline{y}_{i}), d_{i}(\overline{y}_{i}, \overline{z}_{i})\}
≤ max\{sup_{i^{∈}ω} d_{i}(\overline{x}_{i}, \overline{y}_{i}), sup_{i^{∈}ω} d_{i}(\overline{y}_{i}, \overline{z}_{i})\}
= max\{d(\overline{x}, \overline{y}), d(\overline{y}, \overline{z})\}.
□

We have now seen that one can use metric spaces to solve recursive domain equations, and that one needs ultra-metric spaces to obtain a Cartesian closed category. However, it is necessary, in order to obtain non-trivial solutions, to shrink the right-hand side occurrences of the left-hand side variable. On the one hand we seem to be able to modeling interesting structures like fractals and processes, where it seems to make sense that the right-hand side is shrunk, due to either the geometrical intuition for fractals or the intuition about processes connecting the effort needed to distinguish two processes with their distance. Certainly we must admit that the need for shrinking makes the metric models fundamentally different from the partial order (pre-order) ones, where you can have a model of the λ-calculus in the categorical sense that has become standard. This by no means however, implies that the metric models are uninteresting, rather that they introduce a new aspect in semantics. For one application of metric spaces to semantics or processes using real time see [Reed & Roscoe 88]. Here some conceptual and technical advantage seem to be gained by considering time explicitly via a metric instead of implicitly via discrete event sequences. One advantage that Reed and Roscoe mention is that hiding of events usually causes problems with recursion and continuity. Using explicit time means that even if one hides some events of a process, it does not make the process faster, and thus one obtains less equivalences than with the models that use implicit time. It is to the author an open question whether pre-orders could have been used to the same effect.

2.3 Metric spaces as pre-orders

Concluding our resumé of the pre-order and the metric treatment of recursive domain equations and as a prelude to our development we will give an introduction to the line of thought that makes a unification of pre-orders and metric spaces for semantics possible. As to the motivation for such a unification, the main aim is to lay bare more clearly the pre-requisites for solving recursive domain equations. Obviously, as the two approaches have shown, it is not an essential feature to be either in some category of pre-orders or in some category of metric spaces. This indicates that more general structures are available.

By adopting the viewpoints of particular constructive logics one can achieve that what expressed internally looks like ordinary pre-orders have a more delicate structure when observed from the outside. This happens when the truth values have a more delicate structure than the usual two point lattice. We will try to elaborate on this idea before we establish all the formal machinery in Chapter 3 and 4.

Notice first, that a pre-order on a set A can be defined as a function ≤: A × A → Ω (which will be written in infix notation), where Ω is the lattice {⊤, ⊥} of truth values, and where ‘≤’ fulfils two laws, viz. (a ≤ a) = ⊤ (reflexivity) and (a ≤ b) ∧ (b ≤ c) → (a ≤ c) = ⊤ (transitivity) with the usual meaning attached to the logical connectives ‘∧’ and ‘→’.

Consider then what happens if we change our viewpoint from this normal universe based on a two valued logic to a logic based on, say, the extended half open interval [0, ∞] with an interpretation of the logical connectives where a ∧ b = max{a, b} and a → b = (0 if a ≥_{ℝ} b else b).

The intuition behind that logic is that we want to use it for not only telling whether two elements are equal, but to indicate to what extent they differ; in other words, to tell the distance between two elements: a logic of metric spaces if you wish. Perfect equality implies distance 0, and so 0 = ⊤ in the lattice [0, ∞] of truth values. This lattice is denoted by [0, ∞]_{max}.

With the indicated interpretation of the connectives, consider what the axioms for reflexivity and transitivity of pre-orders mean now, if we look at them from outside our new universe (from the inside of course, they just express pre-order-ness). Reading now the ‘preorder’ as distance, the first law expresses that, d(a, a) = ⊤ = 0 , and the second one says, also translated into metric terms, that max{d(a, b), d(b, c)} ≥_{ℝ} d(a, c), that is, it expresses the strong triangular inequality that characterizes ultra-metric spaces. If the interpretation of ‘∧’ changed to ‘+’ the result would be the normal triangular inequality for metric spaces.

What we have observed then is, that in the logic of [0, ∞]_{max}, what internally is a preorder, is externally a (generalized) ultra-metric space. (And that we in a similar fashion can obtain the generalized metric spaces.)

In a more complicated example we now use the lattice structure of Ω. Both (2, ∧) and ([0, ∞], sup) are complete lattices. We will use A(a, a′) as a generic term for a ≤ a′ and d(a, a′) in the rest of this section. Let (a_{n})_{n^{∈}ℕ} be a sequence of elements of a pre-order (or a metric space), and consider the formula

⊤_{Ω} ≤ ⋁_{N^{∈}ℕ} ⋀_{m≥n≥N} A(a_{n}, a_{m}) .  (∗)

For pre-orders, where Ω is 2 this means that there exists a natural number N, such that ∀m ≥ n ≥ N. a_{n} ≤ a_{m}, that is, (a_{n})_{n^{∈}ℕ} is eventually increasing. For metric spaces, where Ω is [0, ∞], we have that ⋀ is sup and ⋁ is inf, and thus (∗) reads

0 ≥ inf_{N^{∈}ℕ} sup_{m≥n≥N} d(a_{n}, a_{m}) ,

which is equivalent to that for every ϵ > 0 there exists N ^{∈} ℕ such that sup_{m≥n≥N} d(a_{n}, a_{m}) ≤ ϵ, that is, the sequence is Cauchy.

We should now have an idea that it is possible not only to unify the notions of pre-order and metric space, but also the convergence and completeness properties of the two notions. The main part of the rest of this thesis will be devoted to this unification, aiming at providing a proper logical framework, plus showing how Scott’s inverse limit theorem can be stated and proved in such a framework. First however, we will go through the very basics of the well-known theory of Ω_{⊗}-categories in some detail, since it provides the foundation for our unification.

Enriched Category Theory

We have in the previous chapter seen as an example how pre-orders and metric spaces can be generalized to sets on which there is a reflexive and transitive relation yielding values in some lattice Ω . In [Lawvere 73] Lawvere described enriched categories as a unifying concept for categories, pre-orders and metric spaces, among other structures. We will first give a small motivation and introduction to the basic concepts of enriched category theory as seen entirely from our perspective. For an excellent basic and general exposition see [Lawvere 73], and for comprehensive references see [Eilenberg & Kelly 66] and [Kelly 82]. Then we will introduce Cauchy and MacNeille completeness for enriched categories, and finally a notion of completeness that we will call limsup completeness, and which generalizes metric Cauchy completeness and chain (or directed) completeness for pre-orders.

3.1 Basics of enriched category theory

Attempting to use categorical methods on pre-orders and metric spaces we try to see any given pre-order as a kind of category, and also any given metric space as a kind of category. Both will be particular enriched categories. In a genuine category (an object of the category CAT of small categories and functors (see e.g. [Mac Lane 71])) the hom functor maps two objects into SET, the category of sets. With the terminology of enriched categories, a genuine category is then a SET-enriched category, or just a SET-category. In a metric space we can look at the metric as a hom-functor (suitably generalized). It maps any two points of the metric space into [0, ∞]_{+}, the extended non-negative reals. So if we take the points of the metric space as the objects, then we can see a metric space as an [0, ∞]_{+}-category. The same way we can see a pre-order as a 2-category. The pre-ordering ‘≤’ maps a pair (a, b) into ⊤ if a ≤ b and into ⊥ if a ≰ b. It will turn out that the way in which PreOrd builds on 2 is just the same as the way in which GMet builds on [0, ∞]_{+} and CAT builds on SET. The process of going from the base structures (2, [0, ∞]_{+}, and SET) to the structures that build on them is called enrichment, and the resulting structures (PreOrd, GMet, and CAT) thus enriched categories.

We notice that we can consider both [0, ∞]_{+} and 2 as categories, the base categories. The objects of the base category are called homs. Naturally the intuitive reading of ‘hom’ varies with the applications we have in mind, but for pre-orders and metric spaces it seems one natural choice to read hom(a, b) as an indication of how well a approximates b. In order to obtain a feasible theory of enriched categories we need several additional requirements for the base category.

These requirements come for instance from the fact that we want to be able to relate hom(a, b) , hom(b, c) and hom(a, c) . The way we do this in CAT is via the notion of composition of morphisms. Given a category, C say, objects a, b, c ^{∈} C_{0} , and morphisms f ^{∈} C(a, b) and g ^{∈} C(b, c) we can form g ∘ f ^{∈} C(a, c) . In other words, for each a, b, c ^{∈} C_{0} we have a morphism (in the base category SET) from C(a, b) × C(b, c) to C(a, c) , viz. composition of morphisms from those particular homsets. For pre-orders we have the axiom (a ≤ b) ∧ (b ≤ c) ≤_{2} (a ≤ c) . In metric spaces we have d(a, b) + d(b, c) ≥_{[0,∞]_{+}} d(a, c) . Here we have used C , ≤ , and d as hom functors, and we see that in all three cases we have an operation (×, ∧, and + respectively), ⊗ say, (a bifunctor, actually) that takes two objects from the base category into a third. We will call this bifunctor ‘tensor’ in general, and require it to be commutative and associative up to isomorphism, plus have a unit, 1_{⊗} , such that 1l ⊗ a ≅ a ⊗ 1l ≅ a for all a . In our examples the unit is the singleton set, ⊤ , and 0 . Further we have the requirement that there be a morphism from hom(a, b) ⊗ hom(b, c) to hom(a, c) , when we remember that 2 is a category with a morphism from ⊥ to ⊤ (in addition to the identities), and that [0, ∞]_{+} is a category with a morphism from x to y if and only if x ≥ y .

If we choose to interpret homs as a measure of how well the first argument approximates the second, then the above rule for pre-orders reads simply: ‘if a approximates b and b approximates c, then a approximates c.’ The rule for metric spaces reads ‘if a approximates b to within ϵ_{1} and b approximates c to within ϵ_{2}, then a approximates c to within ϵ_{1} + ϵ_{2}. In the case of CAT the approximation interpretation becomes a little artificial and it might be better to think of C(A, B) for a category C as the set of paths from A to B. In addition to the transitivity requirement we require that there is a morphism from 1l to C(A, A). We call this requirement reflexivity. In the pre-order case it is simply the usual rule of reflexivity, and in the metric case it says that 0 ≥ d(a, a) for all a.

An additional requirement stems from the desire to see the base category as a category enriched over itself. If the tensor preserves colimits in each variable (and the base category satisfies what is known as the solution set condition (see e.g. [Mac Lane 71] p. 117, Theorem 2), something that is always satisfied when the base category is a pre-order, which it will be in our cases in the sequel) then a ⊗ has a right adjoint a−• say. This amounts to the requirement that the base category be closed. The above adjunction appears in the category of sets between A × and A → where × is Cartesian product and → is exponentiation. In 2 (or any other Heyting algebra) the adjunction is between a ∧ and a → and in [0, ∞]_{+} the adjunction is between a + and −^{.}a where −^{.} is truncated minus.

We can use −• as the internal hom for the base category. To see that reflexivity holds, we need to see that there is a morphism from 1l to a−• a, but by adjointness this is the same as requiring a morphism from a to a, and we have id_{a} always. To see transitivity we need to see that there is a morphism from (a−• b) ⊗ (b−• c) to a−• c, but by adjointness that is the same as finding a morphism from a ⊗ (a−• b) ⊗ (b−• c) to c. In general there is a morphism from a ⊗ (a−• b) to b by adjointness and the existence of id_{a−• b} (in fact, it is the counit of the adjunction), and by applying this fact twice we get the desired morphism.

The last requirements to the base category come from the desire to have sufficiently many limits and colimits available, for instance, in our case to use it as a foundation for a logical interpretation. Thus we require that it be cocomplete (and that colimits behave well wrt. pullbacks, a requirement that trivializes in our cases, where the base category is a pre-order). All these requirements are just the ones specified by Lawvere in [Lawvere 73]. In summary they are that the base category be cocomplete and that it has a symmetric, monoidal closed structure, the tensor, ⊗, that is used to compose homs, and with 1l as unit.

Concerning the monoidal closedness, actually we have further a number of coherence conditions, but they trivialize in our cases, so we will just refer the reader to [Eilenberg & Kelly 66] for a reference.

The requirements to the base category specialize to it being a unital, commutative quantale as defined below when its objects are indexed by a set (which for one thing implies that it is a pre-order).

Definition 3.1 A quantale is a complete lattice with a binary, associative operation ⊗, called tensor, such that for every element a, both a ⊗ and ⊗ a have right adjoints. A quantale is called commutative whenever its tensor is, and it is called unital if there is an element 1_{⊗}, the unit, such that 1_{⊗} ⊗ a = a = a ⊗ 1_{⊗} for all a. For commutative quantales we denote the right adjoint to a ⊗ (and to ⊗ a) by a−• . □

Our prime example of a unital commutative quantale is [0, ∞]_{+}, where ⊗ is +. The logic that we get from such a quantale is a particular linear logic. See [Ambler 92] for a detailed exposition. In that thesis it is also exposed how we do not have a very nice higher order logic on this basis. We remark that by being a left adjoint a + preserves all colimits (infima) for all a , and as it is, most limits. The only limit that a + does not preserve is the empty one: a = a + sup_{ℝ} ∅ ≠ sup_{ℝ} ∅ = 0 , for a ≠ 0 .

We note a number of useful facts about unital, commutative quantales.

a−• b = ⋁{ c | a ⊗ c ≤ b }  (3.1)
a = 1_{⊗}−• a  (3.2)
a ⊗ (a−• b) ≤ b  (3.3)
a ≤ (a−• b)−• b  (3.4)
(a−• b) ⊗ (b−• c) ≤ a−• c  (3.5)
(a−• b) ⊗ (c−• d) ≤ a−• (c−• (b ⊗ d))  (3.6)
a ⊗ ⋁ B = ⋁{ a ⊗ b | b ^{∈} B }  (3.7)
a−• ⋀ B = ⋀{ a−• b | b ^{∈} B }  (3.8)
a−• ⋁ B ≥ ⋁{ a−• b | b ^{∈} B }  (3.9)
(⋁ B) −• a = ⋀{ b−• a | b ^{∈} B }  (3.10)
(⋀ B) −• a ≥ ⋁{ b−• a | b ^{∈} B }  (3.11)

(1-8) follow easily from adjointness of ⊗ and −• . To see (9) notice that it is equivalent to a−• ⋁ B ≥ a−• b for all b , which follows from the fact that −• is covariant in the second

Name  Set  ∧ ⋁ ⊗ −• 1_{⊗} ⊤ ⊥
2  {⊤, ⊥} ∧ ∨ ∧ → ⊤ ⊤ ⊥
[0, ∞]_{+}  [0, ∞] max inf + −^{.}^{(i)} 0  0 ∞
[0, ∞]_{max}  [0, ∞] max inf max −•^{(ii)} 0  0 ∞
[−∞, ∞]_{+} [−∞, ∞] max inf + −^{(iii)} 0 −∞ ∞
[0, ∞]_{•}  [0, ∞] max inf · /^{(iv)} 1  0 ∞

Table 3.1: A selection of quantales

argument (8). Again, adjointness gives (10) and (11) is equivalent to (⋀ B)−• a ≥ b−• a for all b, which follows from the contravariancy of −• in the first argument (10).

Table 3.1 summarizes a number of quantales based on the two valued set or the reals. The numbers annotating −• refer to the following comments.

(i) −^{.} is truncated minus, a−^{.}b = \{ \begin{matrix}b − a & if a ≥_{ℝ} b , \\ 0 & otherwise, and when a = b = ∞. \end{matrix}

(ii) a−• b = \{ \begin{matrix}b & if a ≥_{ℝ} b , \\ 0 & otherwise. \end{matrix}

(iii) The extension of plus and minus to infinite values is determined by the requirement that a + is left-adjoint to − a , that is a + b ≥ c if and only if a ≥ c − b . We see that c − ∞ = −∞ for all c , that −∞ + ∞ = ∞ , and that −∞ − −∞ = −∞ . Not very nice algebraic properties, but the nicest we can get.

(iv) Also here the adjointness determines division extended to being total by incorporating infinity. We have that a/0 = ∞/a = ∞ for all a .

We are ready for the basic definitions. Let Ω_{⊗} be a unital commutative quantale with unit 1_{⊗}.

Definition 3.2 An Ω_{⊗}-category is a pair (A_{0}, A) where A_{0} is a set and where A is a mapping, A : A_{0} × A_{0} → Ω_{⊗} satisfying 1_{⊗} ≤ A(a, a) (reflexivity) and A(a, b) ⊗ A(b, c) ≤ A(a, c) (transitivity) for all a, b, c ^{∈} A_{0}. As morphisms between Ω_{⊗}-categories (A_{0}, A) and (B_{0}, B) we take equivalence classes of functions f on the underlying sets that respect the relation, i.e. where A(a, a′) ≤ B(f(a), f(a′)) for all a, a′ ^{∈} A_{0}. Two morphisms f, g : (A_{0}, A) → (B_{0}, B) are equivalent if and only if 1_{⊗} ≤ B(f(a), g(a)) ∧ B(g(a), f(a)) for all a ^{∈} A_{0}. We denote by Ω_{⊗}-CAT the category of Ω_{⊗}-categories with morphisms as above. □

When we wish to disambiguate an Ω_{⊗}-category from its second component we will refer to the second component using placeholders thus: A( , ). We note, that we could equivalently have formulated the equivalence between functions as A(a, a′) ≤ B(f(a), g(a′)) ∧ B(g(a), f(a′)) for all a, a′ ^{∈} A_{0}.

Instead of functions it will be fruitful to introduce relations (‘bimodules’), as we shall see. To be able to introduce these concepts more elegantly we internalize some of the notions.

Observation 3.1 Observe that (Ω_{⊗}, −•) is an Ω_{⊗}-category in its own right. To see that (Ω_{⊗}, −•) is an Ω_{⊗}-category we have to check reflexivity and transitivity of −•. Reflexivity is trivial and transitivity is just (a−• b) ⊗ (b−• c) ≤ a−• c, which by adjointness is equivalent to a ⊗ (a−• b) ⊗ (b−• c) ≤ c, which is true by two applications of rule (3) above.

We define what will turn out to be the initial object in a category of Ω_{⊗}-categories.

Definition 3.3 With 1l we denote the Ω_{⊗}-category with one element (and the only possible relation part.) □

We can define two kinds of products on Ω_{⊗}-categories in the following way.

Definition 3.4 Given Ω_{⊗}-categories A and B we define products A × B and A ⊗ B corresponding to ∧ and ⊗ respectively. The set part of a product is the Cartesian product of the set parts of the components, and the relation parts are as follows.

(A × B)((a, b), (a′, b′)) = A(a, a′) ∧ B(b, b′),
(A ⊗ B)((a, b), (a′, b′)) = A(a, a′) ⊗ B(b, b′).
□

We have the following propositions.

Proposition 3.1 When A and B are Ω_{⊗}-categories, so are A × B and A ⊗ B .

Proof : Reflexivity is in both cases obvious. To show transitivity of A × B we calculate as follows.

(A × B)((a, b), (a′, b′)) ⊗ (A × B)((a′, b′), (a′′, b′′)) =
(A(a, a′) ∧ B(b, b′)) ⊗ (A(a′, a′′) ∧ B(b′, b′′)) ≤
(A(a, a′) ⊗ A(a′, a′′)) ∧ (B(b, b′) ⊗ B(b′, b′′)) ≤
A(a, a′′) ∧ B(b, b′′) =
(A × B)((a, b), (a′′, b′′)) .

To show that A ⊗ B is transitive we calculate thus.

(A ⊗ B)((a, b), (a′, b′)) ⊗ (A ⊗ B)((a′, b′), (a′′, b′′)) =
A(a, a′) ⊗ B(b, b′) ⊗ A(a′, a′′) ⊗ B(b′, b′′) ≤
A(a, a′′) ⊗ B(b, b′′) =
(A ⊗ B)((a, b), (a′′, b′′)) .
□

We define the function space between Ω_{⊗}-categories as follows.

Definition 3.5 Given Ω_{⊗}-categories A and B the set part of the function space is the set of morphisms from A to B and the relations are given by

(A−• B)(f, g) = ⋀_{a^{∈}A_{0}} B(f(a), g(a)) .  □

Proposition 3.2 (A−• B) is an Ω_{⊗}-category whenever A and B are.

Proof : To show that (A−• B) is transitive we calculate as follows.

(A−• B)(f, g) ⊗ (A−• B)(g, h) = ( ⋀_{a^{∈}A_{0}} B(f(a), g(a))) ⊗ ( ⋀_{a^{∈}A_{0}} B(g(a), h(a)))
≤ ⋀_{a^{∈}A_{0}} ⋀_{a′^{∈}A_{0}} (B(f(a), g(a)) ⊗ B(g(a′), h(a′)))
≤ ⋀_{a^{∈}A_{0}}(B(f(a), g(a)) ⊗ B(g(a), h(a)))
≤ ⋀_{a^{∈}A_{0}} B(f(a), h(a))
= (A−• B)(f, h) .
□

Proposition 3.3 For any Ω_{⊗}-category A we have (A ⊗ ) ⊣ (A−• ).

Proof : Let f : A⊗B−• C. Thus (*) A(a, a′)⊗B(b, b′) ≤ C(f(a, b), f(a′, b′)). Let the function g : A−• (B−• C) be defined as g(a)(b) = f(a, b) and show A(a, a′) ≤ (B−• C)(g(a), g(a′)). Now, (*) above gives us that A(a, a′) ≤ B(b, b′)−• C(f(a, b), f(a′, b′)), so in particular

A(a, a′) ≤ ⋀_{b^{∈}B_{0}}(B(b, b)−• C(f(a, b), f(a′, b)))
= ⋀_{b^{∈}B_{0}}(B(b, b)−• C(g(a)(b), g(a′)(b)))
≤ (B−• C)(g(a), g(a′)) .
□

Observation 3.2 We have now established that Ω_{⊗}-CAT is a monoidal closed category. □

Naturally we also have the following easy theorem. Theorem 3.1 Ω_{⊗}-CAT is Cartesian if and only if ⊗ is ∧. □ Definition 3.6 With A^{op} we denote the opposite of an Ω_{⊗}-category A, that is, A^{op}(a, a′) = A(a′, a). □

We can now build the notion of functional relations (called bimodules) on our primitive notion of morphism. Definition 3.7 A bimodule f : A ⇒ B between Ω_{⊗}-categories A and B is a morphism f : (A^{op} ⊗ B) −• (Ω_{⊗}, −•). □

This means that A(a′, a) ⊗ B(b, b′) ≤ f(a, b)−• f(a′, b′), which for instance implies

A(a′, a) ⊗ f(a, b) ≤ f(a′, b) and B(b, b′) ⊗ f(a, b) ≤ f(a, b′) .

We notice, that many authors list the arguments of a bimodule in the opposite order of ours. However, a bimodule from A to B is always contravariant in A and covariant in B, regardless of whether one writes f(a, b) or f(b, a) for applications of such a bimodule.

It is easy to make the set of bimodules from A to B into an Ω_{⊗}-category by the following definition.

Definition 3.8 For bimodules f, g : A ⇒ B we define

(A ⇒ B) (f, g) = ((A^{op} ⊗ B) −• (Ω_{⊗}, −•)) (f, g) .  □

So the relation is just the underlying relation on the underlying morphisms. To see that (A ⇒ B) really is a transitive relation we calculate as follows.

(A ⇒ B)(f, g) ⊗ (A ⇒ B)(g, h)
= (A^{op} ⊗ B−• (Ω_{⊗}, −•)) (f, g) ⊗ (A^{op} ⊗ B−• (Ω_{⊗}, −•)) (g, h)
= ( ⋀_{a^{∈}A_{0},b^{∈}B_{0}}(f(a, b)−• g(a, b))) ⊗ ( ⋀_{a^{∈}A_{0},b^{∈}B_{0}}(g(a, b)−• h(a, b)))
≤ ⋀_{a^{∈}A_{0},b^{∈}B_{0}}(f(a, b)−• g(a, b)) ⊗ (g(a, b)−• h(a, b))
≤ ⋀_{a^{∈}A_{0},b^{∈}B_{0}}(f(a, b)−• h(a, b))
= (A ⇒ B)(f, h) .

Two bimodules are equivalent if they are equivalent as functions. Spelled out this means that f, g : A−• B are equivalent if and only if 1_{⊗} ≤ (f(a, b)−• g(a, b)) ∧ (g(a, b)−• f(a, b)) for all a ^{∈} A_{0} and all b ^{∈} B_{0}, that is, if and only if 1_{⊗} ≤ (A−• B)(f, g) ∧ (A−• B)(g, f). Thus we could just define (A ⇒ B) = (A^{op} ⊗ B−• (Ω_{⊗}, −•)) as a definition of one Ω_{⊗}-category in terms of another.

Bimodules are composed as follows.

Definition 3.9 Let f : A ⇒ B and g : B ⇒ C be bimodules. Their composition, g ∘ f : A ⇒ C is defined as g ∘f(a, c) = ⋁_{b^{∈}B_{0}} g(b, c)⊗f(a, b) . We denote by Ω_{⊗}-CAT_{⇒} the category

of Ω_{⊗}-categories with bimodules as morphisms. □

Observation 3.3 For an Ω_{⊗}-category A, we have that A( , ) : (A^{op} ⊗ A) −• (Ω_{⊗}, −•) and therefore A( , ) is itself a bimodule from A to A . (This, by the way, is why we chose to let bimodules from A to B take their A argument first. Otherwise A( , ) would have been a bimodule from A^{op} to A^{op} .) Furthermore, in Ω_{⊗}-CAT_{⇒} it is the identity morphism on A . To see this we just have to convince ourselves that for any bimodules f : A ⇒ B and g : B ⇒ A we have f ∘ A( , ) = f and A( , ) ∘ g = g . But

(f ∘ A)(a, b) = ⋁_{a′^{∈}A_{0}} f(a′, b) ⊗ A(a, a′) = f(a, b) ,

and

(A ∘ g)(b, a) = ⋁_{a′^{∈}A_{0}} A(a′, a) ⊗ g(b, a′) = g(b, a) .

□

To a bimodule f : A ⇒ B between Ω_{⊗}-categories there is an obvious corresponding bimodule f^{op} : B ⇒ A defined as f^{op}(b, a) = f(a, b).

Definition 3.10 We say that one bimodule f : A ⇒ B is left-adjoint to another, g : B ⇒ A , if f ∘ g ≤ B and A ≤ g ∘ f . □

Here we have used the pointwise ordering that makes any function space into Ω_{⊗} into a (traditional) pre-order. Thus, spelled out the adjointness conditions mean that

f∘g(b, b′) = ⋁_{a^{∈}A_{0}} f(a, b′)⊗g(b, a) ≤ B(b, b′) and A(a, a′) ≤ ⋁_{b^{∈}B_{0}} g(b, a′)⊗f(a, b) = g∘f(a, a′)

for all a, a′ ^{∈} A_{0} and all b, b′ ^{∈} B_{0} .

Morphisms can generate bimodules.

Definition 3.11 If A and B are Ω_{⊗}-categories and f : A → B is a morphism, we define f_{∗} : B ⇒ A as f_{∗}(b, a) = B(b, f(a)) and f^{∗} : A ⇒ B as f^{∗}(a, b) = B(f(a), b) . We say that f generates f_{∗} and f^{∗} . □

It is easy to see that f_{∗} is left adjoint to f^{∗} .

3.2 Cauchy completeness

We have the following completeness concept, introduced by Lawvere in [Lawvere 73]. Proposition 3.6 provides the best reason for the name of the concept.

Definition 3.12 An Ω_{⊗}-category is Cauchy complete if every adjoint pair of bimodules with the left-adjoint going into it is generated by a morphism in Ω_{⊗}-CAT. □

We hope that the following exposition will illuminate the concept to some extent, but the author acknowledges that the intuition behind the above definition is still rather mystical to him.

Concerning Cauchy completeness we will first show that it is enough to consider adjunctions from 1l (see [Borceux & Dejean 86]). First we need a lemma of general interest.

Given an Ω_{⊗}-category A, for every a ^{∈} A_{0} we have A(a, ) : A → Ω_{⊗} and A( , a) : A^{op} → Ω_{⊗} . We can identify A(a, ) with a function from 1l ⊗ A → Ω_{⊗} by composing A(a, ) with the isomorphism from 1l ⊗ A to A . We will also use the name A(a, ) for this morphism, and we will pretend that it takes elements of A as arguments. The use of this identification is that we can see A(a, ) as a bimodule from 1l to A (since 1l = 1l^{op}). Likewise we can see A( , a) as a bimodule from A to 1l . We then have Lemma 3.1 As bimodules, A(a, ) ⊣ A( , a) for every a ^{∈} A_{0} .

Proof : The two adjointness conditions for bimodules reduce to

A(a, a′′) ⊗ A(a′, a) ≤ A(a′, a′′) and 1_{⊗} ≤ ⋁_{a′^{∈}A_{0}} A(a′, a) ⊗ A(a, a′) ,

for all a′, a′′ ^{∈} A_{0}. The first condition is just transitivity of A and the second is seen by taking a′ = a . □

Let us spell out what means that we have a pair of adjoint bimodules ϕ : 1l ⇒ B and ψ : B ⇒ 1l with ϕ ⊣ ψ . First, looking at the bimodules as morphisms we have ϕ : 1l ⊗ B → Ω_{⊗} and ψ : B^{op} ⊗ 1l → Ω_{⊗} . We will write applications of ϕ and ψ both in the long form as ϕ(∗, b) and ψ(b, ∗) and in the abbreviated form ϕ(b) and ψ(b) . The adjointness requirement is ϕ ∘ ψ ≤ B and 1l ≤ ψ ∘ ϕ . Unfolding the definition of composition we get that the adjointness requirements amount to

⋁_{∗} ϕ(∗, b′) ⊗ ψ(b, ∗) ≤ B(b, b′) and 1l(∗, ∗) ≤ ⋁_{b^{∈}B} ψ(b, ∗) ⊗ ϕ(∗, b) ,

that is,

ϕ ∘ ψ(b, b′) = ϕ(b′) ⊗ ψ(b) ≤ B(b, b′) and 1_{⊗} ≤ ⋁_{b^{∈}B} ψ(b) ⊗ ϕ(b) = ψ ∘ ϕ(∗, ∗)

for all b, b′ ^{∈} B_{0} .

Proposition 3.4 Assuming the axiom of choice, given any Ω_{⊗}-category B , every pair of adjoint bimodules ϕ : A ⇒ B and ψ : B ⇒ A with ϕ ⊣ ψ is generated by a function f : A → B if and only if every pair of adjoint bimodules ϕ : 1l ⇒ B and ψ : B ⇒ 1l with ϕ ⊣ ψ is generated by a function (an element) f : 1l → B .

Proof : Assume every pair of adjoint bimodules with the left-adjoint out of 1l and into B is generated by a function as above, and let the pair ϕ : A ⇒ B and ψ : B ⇒ A of adjoint bimodules with ϕ ⊣ ψ be given. In other words, ϕ : A^{op} ⊗ B → Ω_{⊗} and ψ : B^{op} ⊗ A → Ω_{⊗}. That ϕ is left-adjoint to ψ means that

ϕ(a, b′) ⊗ ψ(b, a) ≤ B(b, b′) and A(a, a′) ≤ ⋁_{b^{∈}B} ψ(b, a′) ⊗ ϕ(a, b)

for all a, a′ ^{∈} A_{0} and all b, b′ ^{∈} B_{0}. We will construct a function f : A → B such that f^{∗} = ϕ and f_{∗} = ψ, that is, such that ϕ(a, b) = B(f(a), b) and ψ(b, a) = B(b, f(a)).

According to Lemma 3.1, given a ^{∈} A_{0} we have an adjunction A(a, ) ⊣ A( , a) from 1l to A , and thus by composition ϕ∘A(a, ) ⊣ A( , a)∘ψ from 1l to B . By assumption this pair of adjoint bimodules is generated by a function (an element), b_{a} : 1l → B say. We will identify b_{a}(∗) with b_{a} as an element of B_{0} . We remember that b_{a}^{∗}(∗, b) = B(b_{a}, b) and b_{a}_{∗}(b, ∗) = B(b, b_{a}), and that our assumption says that ϕ ∘ A(a, ) = b_{a}^{∗} and A( , a) ∘ ψ = b_{a}_{∗} , that is,

ϕ ∘ A(a, )(b) = B(b_{a}, b) and A( , a) ∘ ψ(b) = B(b, b_{a}) .

We use the axiom of choice to choose a particular b_{a} for each a, and we claim that the mapping that takes a into b_{a} is the desired morphism from A to B. We will first check that it is a morphism at all. We have

ϕ ∘ A(a, )(b) = ⋁_{a′^{∈}A_{0}} ϕ(a′, b) ⊗ A(a, a′)
= ϕ(a, b) ,

where we have the last equality by ϕ being a bimodule (suffices for ‘≤’) and from taking a′ = a . In the same way we get that A( , a) ∘ ψ(b) = ψ(b, a) . Then we have

B(b_{a}, b_{a′}) ≥ ⋁_{b^{∈}B_{0}} B(b, b_{a′}) ⊗ B(b_{a}, b)
= ⋁_{b^{∈}B_{0}} ψ(b, a′) ⊗ ϕ(a, b)
≥ A(a, a′) ,

where we have the first inequality by transitivity of B, and the latter inequality by adjointness of ϕ and ψ.

We note, that in proving that a ↦ b_{a} was a morphism we also showed that ϕ(a, b) = B(b_{a}, b) and ψ(b, a) = B(b, b_{a}) , which means that we are done. □

We will see what Cauchy completion means for pre-orders.

Proposition 3.5 Assuming the axiom of choice, every pre-order is Cauchy complete (as a category enriched over 2 .)

Proof : Let A be a pre-order and ϕ : 1l ⇒ A and ψ : A ⇒ 1l be adjoint bimodules with ϕ ⊣ ψ . We have ϕ : A → Ω, and we will identify ϕ with the up-closed subset of A (more precisely sub-enriched category) that is mapped into ⊤ by (the underlying function corresponding to) ϕ . Similarly we will see ψ as an down-closed subset of A, and we will use set notation for ϕ and ψ . Then the adjointness of ϕ and ψ amounts to

a′ ^{∈} ϕ ∧ a ^{∈} ψ → a ≤ a′ and ϕ ∩ ψ ≠ ∅ .

If ϕ and ψ overlap at a and a′ then by the first adjointness condition a ≤ a′ and a′ ≤ a, so the intersection is a singleton up to isomorphism. Now, choose one element a from the intersection. Then given a′, the first adjointness condition gives us that a ^{∈} ϕ ∧ a′ ^{∈} ψ → a′ ≤ a , so a′ ^{∈} ψ → a′ ≤ a , but also, since ψ is down-closed and contains a we see that a′ ≤ a → a′ ^{∈} ψ . Similarly we see that a′ ^{∈} ϕ ↔ a ≤ a′ . Therefore ϕ and ψ are generated by a (they are the principal filter and principal ideal generated by a ). □

Observe however, that we have used the axiom of choice to pick a, and in fact it is shown in [Carboni & Street 86] (Corollary 4) that the axiom of choice is equivalent to every pre-order being Cauchy complete.

In the special case of symmetric (generalized) metric spaces, that is, symmetric categories enriched over [0, ∞]_{+} we have the following theorem from [Lawvere 73].

Proposition 3.6 A symmetric generalized metric space is metrically complete if and only if it is Cauchy complete as an [0, ∞]_{+}-category. □

Proof : The adjointness conditions for bimodules from 1l to a metric space A specialize to the following.

ϕ(a′) + ψ(a) ≥ d(a, a′) and 0 = inf_{a^{∈}A_{0}}(ϕ(a) + ψ(a)) .

Assume that every such pair is generated by a function, that is, that there exists an element e ^{∈} A_{0} such that ϕ(a) = ψ(a) = d(a, e) for all a ^{∈} A_{0} . Then, let (a_{n})_{n^{∈}ℕ} be a Cauchy sequence in (A_{0}, d) and define ϕ(a) = ψ(a) = lim_{N→∞} sup_{n≥N}d(a, a_{n}) . By metric completeness of ℝ the second adjointness condition is fulfilled, and the first follows from symmetry of d and the triangular inequality. Then by assumption there exists e ^{∈} A_{0} such that lim_{N→∞} sup_{n≥N}d(a, a_{n}) = ϕ(a) = ψ(a) = d(a, e) , which means that e is the metric limit of (a_{n})_{n^{∈}ℕ} .

The other way, assume that (A_{0}, d) is metrically complete, and let ϕ and ψ be adjoint as above. Then the second adjointness condition allows us to construct a sequence (a_{n})_{n^{∈}ℕ} with ψ(a_{n})+ϕ(a_{n}) ≤ \frac{1}{n} say. But then the first adjointness condition and the triangular inequality give us that

\frac{1}{n} + \frac{1}{m} ≥ ψ(a_{n}) + ϕ(a_{m}) ≥ d(a_{n}, a_{m})

for all m, n ^{∈} ℕ, so the sequence (a_{n})_{n^{∈}ℕ} is Cauchy and by metrical completeness it converges, say to e . By the triangular inequality then it is easy to see that ϕ(a) = ψ(a) = d(a, e) for every a ^{∈} A_{0} . □ We note that we never in the proof used that ϕ and ψ were (potentially) different functions– in fact they turned out to be identical. This fact seems to indicate that the symmetric metric case only illuminates quite a limited aspect of the notion of Cauchy completeness. As we have seen, every pre-order is Cauchy complete, so the situation is even worse there.

Definition 3.13 The Cauchy completion of an Ω_{⊗}-category A is the full sub-category of 1l ⇒ A whose objects have right adjoints. □

We have the expected universal property of the Cauchy completion \overline{A} of an Ω_{⊗}-category A viz. that it is Cauchy complete and that every morphism from A to a Cauchy complete Ω_{⊗}-category can be uniquely extended to a morphism from \overline{A}. For this and many more details we refer the reader to the overview article [Borceux & Dejean 86] and to [Kelly 82].

We wish to draw the attention of the reader to a connection to the Karoubi envelope which Todd Wilson and the author realized during conversations. We refer the reader to [Borceux & Dejean 86], [Kelly 82], and [Lambek & Scott 86] for details. As it is, neither of the references mention explicitly the connection, but this must be just a case of different terminology. The development here applies to ordinary categories, that is, to categories enriched over SET, the category of sets. Remember that pre-orders are also categories.

Definition 3.14 A morphism e : A → A is idempotent if e = e ∘ e . □

Observation 3.4 For a retract B ↪^{ϕ} ; ←_{ψ} A the composite ϕ ∘ ψ is idempotent because ψ ∘ ϕ =

id_{B} . □

Definition 3.15 We say that an idempotent e : A → A splits if there exists a retract B ↪^{ϕ} ; ←_{ψ} A

with ϕ ∘ ψ = e . □

From [Borceux & Dejean 86] we have

Proposition 3.7 A category is Cauchy complete if and only if all its idempotents split. □

From [Lambek & Scott 86] we take the following definition and proposition without proof.

Definition 3.16 For a category A the Karoubi envelope K(A) has as objects all the idempotents of A, and as morphisms between f : A → A and g : B → B the triples (f, ϕ, g) where ϕ : A → B satisfies ϕ ∘ f = ϕ = g ∘ ϕ . □

Proposition 3.8 The Karoubi envelope of any category is Cauchy complete. □

Thus it would seem that Cauchy completion and Karoubi envelope are just two names for the same thing, when it comes to ordinary categories, although this of course has to be proven. In any case, the Cauchy completeness formulation with bimodules generalizes more straightforwardly to the enriched setting.

3.3 The enriched Dedekind-MacNeille completion

We will discuss an enriched version of the Dedekind-MacNeille completion. This construction is presumably well-known, but the author has not seen it written out in detail elsewhere. We remind ourselves about the construction in the pre-order case (see e.g. [Johnstone 82] p.109).

Definition 3.17 Given a pre-order A the MacNeille completion of A is the set M(A) of pairs (L, U) of subsets of A, such that L = lb(U) and U = ub(L) , where lb(U) is the set of lower bounds of U and ub(L) is the set of upper bounds of L . The pre-order on M(A) is (L_{1}, U_{1}) ≤ (L_{2}, U_{2}) if and only if L_{1} ⊆ L_{2} . □

Notice that any L from an element of M(A) is down-closed and any U up-closed. The notable properties of the Dedekind-MacNeille completion of a pre-order are that it is a complete lattice (with everything up to isomorphism wrt. the pre-order, of course), and that the process of completion preserves all existing joins and meets.

The embedding m : A → M(A) is defined m(a) = (↓ a, ↑ a) , and it preserves all meets and joins (that already exist). Here we use the notation ↓ a for the set { x ^{∈} A | x ≤ a } and similarly for ↑ a .

To put this into an enriched framework we first consider just how to formulate the above properly when considering pre-orders as categories enriched over the two point lattice. We could venture the definition that a subset of a 2-category A is just any 2-functor from A into 2, where the latter 2 denotes 2 considered as a 2-category itself, that is, as (2, →). This definition means however, that subsets of pre-orders are all up-closed, since the requirement of S being a 2-functor means that A(a, a′) ≤ S(a) → S(a′), that is, that a ≤ a′ implies that S(a) ≤ S(a′). In the Dedekind-MacNeille completion we have to work with both up-closed and down-closed subsets (but those are enough), and thus we define as follows.

Definition 3.18 An up-subset of A is any Ω_{⊗}-morphism U : A−• Ω_{⊗}, and a down-subset is any up-subset of A^{op}. An up-down-subset of A is any pair (L, U) of a down and an up-subset of A. □

We can think of the bimodule L ⊗ U : (A^{op} ⊗ A) −• Ω_{⊗} as the intersection of L and U. Then, for a ^{∈} A_{0}, we would say that a belongs to L ⊗ U to the extent L(a) ⊗ U(a).

Concerning upper and lower bounds, to take the upper bound of a set is not interesting when the set is an up-set, and conversely, lower bounds are not interesting for down-sets. However, in pre-orders, any set obtainable as the upper bounds of some set, S say, is obtainable as the upper bounds of a down-set, viz. the down-closure of S, and the dual result holds for lower bounds. This justifies the following definition where we in the pre-order case only take upper-bounds of down-sets and lower bounds of up-sets.

Definition 3.19 For a down-subset L of A we define the up-subset ub(L) of upper bounds of L as ub(L)(a) = [A^{op}−• Ω_{⊗}](L, A( , a)). Conversely, for an up-subset U we define the down-subset of lower bounds of U as lb(U)(a) = [A−• Ω_{⊗}](U, A(a, )). □

Notice, that an up-subset of A is the same as a bimodule from 1l into A , and that a down-subset is just a bimodule from A into 1l . Naturally we have Ω_{⊗}-morphisms lb( ) : [A−• Ω_{⊗}]−• [A^{op}−• Ω_{⊗}] and ub( ) : [A^{op}−• Ω_{⊗}]−• [A−• Ω_{⊗}] for every A. Now we can define cuts à la Dedekind and MacNeille, essentially generalizing the presentation from [Johnstone 82] from pre-orders (partial orders, actually) to enriched categories.

Definition 3.20 A cut in a Ω_{⊗}-category A is an up-down-subset (L, U) of A such that L = lb(U) and U = ub(L). □

Definition 3.21 The MacNeille completion of a Ω_{⊗}-category A is the Ω_{⊗}-category M(A) where M(A)_{0} is the set of cuts in A, and M(A)((L_{1}, U_{1}), (L_{2}, U_{2})) = [A^{op}−• Ω_{⊗}](L_{1}, L_{2})^{1}. The embedding m of A into M(A) is defined as m(a) = (A( , a), A(a, )). □

To justify this definition we have the following proposition and observation. First we will show that m(a) is really a cut for every a ^{∈} A_{0}.

Proposition 3.9 The pair (A( , a), A(a, )) is a cut in A for every a ^{∈} A_{0}.

1but see Theorem 3.2

Proof : Given a′ ^{∈} A_{0} we have to show that (i) A( , a′) = lb(A(a, )) and (ii) A(a′, ) = ub(A( , a′)). To see (i) we calculate as follows.

lb(A(a′, ))(a) = [A−• Ω_{⊗}](A(a′, ), A(a, ))
= A(a, a′),

where we get the last equality by Yoneda (thanks to Marcelo Fiore for pointing this out to the author), which in general says that [A−• Ω_{⊗}](A(a′, ), F) = F a′ for every a′ ^{∈} A_{0} .

To see (ii) we calculate as follows.

ub(A( , a′))(a) = [A^{op}−• Ω_{⊗}](A( , a′), A( , a))
= A(a′, a),

where we get the last equality from Yoneda again. □ We also have the following

Theorem 3.2 [A^{op}−• Ω_{⊗}](L_{1}, L_{2}) = [A−• Ω_{⊗}](U_{2}, U_{1}) for any cuts (L_{1}, U_{1}) and (L_{2}, U_{2}) in A.

Proof : We calculate

[A^{op}−• Ω_{⊗}](L_{1}, L_{2}) = [A^{op}−• Ω_{⊗}](lb(U_{1}), lb(U_{2}))
= ⋀_{a^{∈}A_{0}}(lb(U_{1})(a)−• lb(U_{2})(a))
= ⋀_{a^{∈}A_{0}}([A−• Ω_{⊗}](U_{1}, A(a, ))−• [A−• Ω_{⊗}](U_{2}, A(a, )))
≥ [A−• Ω_{⊗}](U_{2}, U_{1}) ,

where the last inequality comes from adjointness and the transitivity of [A−• Ω_{⊗}] . To see the inequality the other way we calculate as follows.

[A−• Ω_{⊗}](U_{2}, U_{1}) = [A−• Ω_{⊗}](ub(L_{2}), ub(L_{1}))
= ⋀_{a^{∈}A_{0}}(ub(L_{2})(a)−• ub(L_{1})(a))
= ⋀_{a^{∈}A_{0}}([A^{op}−• Ω_{⊗}](L_{2}, A( , a))−• [A^{op}−• Ω_{⊗}](L_{1}, A( , a)))
≥ [A^{op}−• Ω_{⊗}](L_{1}, L_{2}) .

For 2-categories the enriched Dedekind-MacNeille completion is precisely the well-known Dedekind-MacNeille completion, a trivial fact since all the definitions specialize straightforwardly to Johnstone’s, observing as we did, that it is enough to take upper bounds of down-sets and vice versa. For symmetric metric spaces up and down closed mean the same thing. L : A^{op} → Ω_{⊗} is just any ‘subset’, where the elements can be ‘fuzzy’ in the sense that L(a) need not be either ∞ or 0 . For any cut (L, U) we have

L(a) = [A−• Ω_{⊗}](U, A(a, ))
= sup_{a′^{∈}A} |U(a′) − d(a, a′)|
≥ U(a),

and

U(a) = [A−• Ω_{⊗}](L, A( , a))
= sup_{a′^{∈}A} |L(a′) − d(a′, a)|
≥ L(a),

so L = U , and the condition for being a cut reduces to L = lb(L) , which means that for all a ^{∈} A we have L(a) = sup_{a′^{∈}A} |L(a′) − d(a, a′)| which is always the case, since L is a morphism. This means that the MacNeille completion of a metric space is just the presheaf category (see Def. 4.11), and the embedding of a metric space into its MacNeille completion is the Yoneda embedding A ↦ Ω_{⊗}^{A^{op}} (see also [Lawvere 73], p. 154).

We will show the following lemma, again generalized from [Johnstone 82].

Lemma 3.2 Given any family (L_{i}, U_{i})_{i^{∈}I} of cuts in A, the pair (⋀_{i^{∈}I}L_{i}, ub(⋀_{i^{∈}I} L_{i})) is a cut in

A.

Proof : We will show that lb(ub(⋀_{i^{∈}I} L_{i})) is equivalent to ⋀_{i^{∈}I} L_{i} . First, ⋀_{i^{∈}I} L_{i} ≤ L_{i} for every i, and therefore ub(⋀_{i^{∈}I} L_{i}) ≥ ub(L_{i}) = U_{i}, and again lb(ub(⋀_{i^{∈}I} L_{i})) ≤ lb(U_{i}) = L_{i} for all i, and we have one of the desired inequalities:

lb(ub(⋀_{i^{∈}I} L_{i})) ≤ ⋀_{i^{∈}I} L_{i}.

To see the inequality the other way we rewrite as follows.

lb(ub(⋀_{i^{∈}I} L_{i})) = [A−• Ω_{⊗}](ub(⋀_{i^{∈}I} L_{i}), A(a, ))
= ⋀_{a′^{∈}A_{0}}(ub(⋀_{i^{∈}I} L_{i})(a′)−• A(a, a′))
= ⋀_{a′^{∈}A_{0}}([A^{op}−• Ω_{⊗}](⋀_{i^{∈}I} L_{i}, A( , a′))−• A(a, a′))
= ⋀_{a′^{∈}A_{0}}( ⋀_{a′′^{∈}A_{0}}(⋀_{i^{∈}I} L_{i}(a′′)−• A(a′′, a′))−• A(a, a′)),

and see that we need to show

⋀_{i^{∈}I} L_{i}(a) ≤ ⋀_{a′^{∈}A_{0}}( ⋀_{a′′^{∈}A_{0}}(⋀_{i^{∈}I} L_{i}(a′′)−• A(a′′, a′))−• A(a, a′))

for all a ^{∈} A_{0}, but this is by adjointness equivalent to

(⋀_{i^{∈}I} L_{i}(a)) ⊗ ⋀_{a′′^{∈}A_{0}}(⋀_{i^{∈}I} L_{i}(a′′)−• A(a′′, a′)) ≤ A(a, a′),

which follows when we choose a′′ = a on the left-hand side. □ In fact, were we to introduce the general notions of completeness and limits in enriched categories, we would be able to state that the construction just described yields the colimit of the family, and that the MacNeille completion is complete and cocomplete, just like in the pre-order case.

Theorem 3.3 Every adjoint pair of bimodules L : A ⇒ 1l and U : 1l ⇒ A with U ⊣ L is a cut in A.

Proof : First we point the attention of the reader to the unfortunate fact that the rightadjoint is L and that it is written to the left in the pair (L, U) . Then we spell out what the two conditions say. U ⊣ L means U ∘ L ≤ A and 11l ≤ L ∘ U, that is,

1.i. U(a′) ⊗ L(a) ≤ A(a, a′) for all a, a′ ^{∈} A_{0} ,

1.ii. 1_{⊗} ≤ ⋁_{a^{∈}A_{0}} U(a) ⊗ L(a) .

The condition of (L, U) being a cut, that is, L = lb(U) and U = ub(L) means

\begin{matrix}2.i. L(a) = [A−• Ω_{⊗}](U, A(a, )) , \\ 2.ii. U(a) = [A^{op}−• Ω_{⊗}](L, A( , a)) . \end{matrix}

Then we show that condition 1 implies condition 2, so assume that L and U are bimodules fulfilling condition 1. To see 2.i we calculate

[A−• Ω_{⊗}](U, A(a, )) ≤ ( ⋁_{a′^{∈}A_{0}} U(a′) ⊗ L(a′)) ⊗ [A−• Ω_{⊗}](U, A(a, ))

= ( ⋁_{a′^{∈}A_{0}} U(a′) ⊗ L(a′)) ⊗ ⋀_{a′′^{∈}A_{0}}(U(a′′)−• A(a, a′′))

= ⋁_{a′^{∈}A_{0}} (U(a′) ⊗ ( ⋀_{a′′^{∈}A_{0}}(U(a′′)−• A(a, a′′))) ⊗ L(a′))
≤ ⋁_{a′^{∈}A_{0}} (U(a′) ⊗ (U(a′)−• A(a, a′)) ⊗ L(a′))
≤ ⋁_{a′^{∈}A_{0}}(A(a, a′) ⊗ L(a′))
≤ L(a),

where we get the last inequality from the fact that L : A^{op}−• Ω_{⊗}. On the other hand we know L(a) ≤ (U(a′)−• A(a, a′)) for all a′ by 1.i, and thus L(a) ≤ [A−• Ω_{⊗}](U, A(a, )), and we have 2.i.

2.ii is seen is a similar way. □ For an example of an Ω_{⊗}-category that is Cauchy complete but not MacNeille complete

we can take any pre-order that is not a complete lattice. For a specific example, consider the three element pre-order as follows.

[figure: ·; ·; ·]

The adjoint bimodules are all the pairs of principal filters and ideals generated by the same points of the pre-order, that is, three pairs in all, ordered by set inclusion of the principal ideals (the down-closed sets). This means that we end up with what we started with, as we should. The pairs of cuts are all of the above, plus the cut whose lower set is the lower set the whole set, and whose upper set is the empty set.

Ordered in the same way as the adjoint pairs of bimodules we get a complete lattice, by ‘adding’ a top element to the pre-order we started out with.

3.4 Limsup completeness

It is by now clear that we can use neither Cauchy complete nor MacNeille complete enriched categories as a generalization of cpo’s and complete metric spaces. In order to provide this unification we define as follows.

Definition 3.22 For a sequence α and N ^{∈} ℕ we let α_{≥N} stand for the sequence such that α_{≥N}(n) = α(n + N), that is, we have dropped the first N elements of α. □

Definition 3.23 For a sequence α ^{∈} [ℕ−• A] we define Cauchy(α) = ⋀_{m≥n^{∈}ℕ}A(α_{n}, α_{m}) as a

measure of how ‘well-behaved’ α is. □

Definition 3.24 We say that a sequence α ^{∈} [ℕ−• A] of elements of an Ω_{⊗}-category A is (forward) Cauchy if

1_{⊗} ≤ ⋁_{N^{∈}ℕ}Cauchy(α_{≥N}) .  □

For pre-orders it is clear that a sequence is forward Cauchy if and only if it is a chain from some index onward. Naturally we have an analogous definition of backward Cauchy based on the following predicate.

Cauchy^{op}(α) = ⋀_{m≥n^{∈}ℕ}A(a_{m}, a_{n}) .

This generalizes eventually decreasing sequences with Cauchy sequences. A forward Cauchy sequence is a backward Cauchy sequence in the opposite enriched category.

For a symmetric metric space the forward Cauchy condition means

inf_{N^{∈}ℕ} sup_{m≥n≥N} d(a_{n}, a_{m}) = 0 ,

which is equivalent to

∀ϵ > 0. ∃N ^{∈} ℕ. sup_{m≥n≥N} d(a_{n}, a_{m}) ≤ ϵ ,

which again is equivalent to

∀ϵ > 0. ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. d(a_{n}, a_{m}) ≤ ϵ .

This is just the usual Cauchy condition for sequences of points in metric spaces, when we notice that we do not need the ordering between m and n, because d is symmetric.

Various rewrites might help illustrate the definition. We have that

Cauchy(α) = ⋀_{m,n^{∈}ℕ}(n ≤ m)−• A(a_{n}, a_{m}) ,

where n ≤ m = \{ \begin{matrix}1_{⊗} & if n ≤ m \\ ⊥_{Ω_{⊗}} & otherwise \end{matrix} .

Definition 3.25 Given a reflexive and transitive bimodule B : A^{op} ⊗ A−• Ω_{⊗} we call B a strengthening of A and obtain a new Ω_{⊗}-category A † B = (A_{0}, B). □

We could have tried to pursue a presheaf terminology and used ‘restriction’ instead of ‘strengthening’. Notice, that A( , ) is the initial strengthening of A = (A_{0}, A( , )) and the identity bimodule from A to itself.

Definition 3.26 Given a morphism f : A−• C and a strengthening B of A, we say that f respects B if the underlying mapping f : A−• C is a morphism from A † B to C. □

This means that B(a, a′) ≤ C(f(a), f(a′)) or equivalently 1_{⊗} ≤ B(a, a′)−• C(f(a), f(a′)) for all a, a′ ^{∈} A_{0}. To cover our definition of Cauchy sequence we introduce the following definition.

Definition 3.27 For an ℕ-indexed family B = (B_{n})_{n^{∈}ℕ} , where B_{n} : (A^{op} ⊗ A) −• Ω_{⊗} of reflexive transitive bimodules we say that f : A−• C eventually respects B if

1_{⊗} ≤ ⋁_{n^{∈}ℕ} ⋀_{a,a′^{∈}A_{0}}(B_{n}(a, a′)−• C(f(a), f(a′)) .  □

Specifically we now define the family (≤_{N})_{N^{∈}ℕ} by letting

n ≤_{N} m = \{ \begin{matrix}1_{⊗} & if n = m or N ≤ n ≤ m, \\ ⊥_{Ω_{⊗}} & otherwise. \end{matrix}

With these definitions the following proposition is immediate.

Proposition 3.10 A sequence α : [ℕ−• A] is forward Cauchy if and only if it eventually respects ≤_{N}. □

We can straightforwardly generalize to directed sets thus.

Definition 3.28 Let D be a directed set and (a_{i})_{i^{∈}D} a D-indexed family of elements of the Ω_{⊗}-category A. We say that (a_{i})_{i^{∈}D} is a directed net if

1_{⊗} ≤ ⋁_{i_{0}^{∈}D} ⋀_{j≥i≥i_{0}} A(a_{i}, a_{j}) .  □

We will define a notion of convergence that fits with our notion of forward Cauchy sequences. As we know from metric convergence, any given prefix of a convergent sequence does not contribute to the metric limit of the sequence. Likewise, in the pre-order case, since we accept a ‘wild’ prefix, we would like that not to contribute to the limit either. Thus, our notion of limit is much more like a (co)limsup, and definitely we are not looking for the categorical notion of limit (or colimit). We define as follows.

Definition 3.29

Colim(a, α) = ⋀_{x^{∈}A_{0}} (A(a, x) •−• ⋀_{n^{∈}ℕ}A(a_{n}, x)) ,

which can be read as the extent to which α ‘converges’ to a. □

We have here use the notation x •−• y to stand for x−• y ∧ y−• x. As we shall see later, the above formula expresses precisely the extent to which a is a colimit for α .

Definition 3.30 Let a be an element of an Ω_{⊗}-category and let α = (a_{n})_{n^{∈}ℕ} be a forward Cauchy sequence in A. We say that α converges to a if

1_{⊗} ≤ ⋁_{N^{∈}ℕ}(Cauchy(α_{≥N}) ∧ Colim(a, α_{≥N})) .

In this case we call a the limsup of α and write this a = lim sup α. □

A completely analogous definition defines limsups of directed nets. We recognize the above definition from the usual formulation of least upper bound for partial orders (with α = (a_{n})_{n^{∈}ℕ}):

a = ⊔α in (A, ≤) iff ∀x ^{∈} A. [a ≤ x ↔ ∀n ^{∈} ℕ. a_{n} ≤ x] .

As for the metric case the limsup condition says

inf_{N^{∈}ℕ}max { sup_{m≥n≥N} d(a_{n}, a_{m}), sup_{x^{∈}A_{0}} |d(a, x) − sup_{n≥N} d(a_{n}, x)|} = 0 ,

that is,

∀ϵ > 0. ∃N ^{∈} ℕ. [ sup_{m≥n≥N} d(a_{n}, a_{m}) ≤ ϵ ∧ sup_{x^{∈}A_{0}} |d(a, x) − sup_{n≥N} d(a_{n}, x)| ≤ ϵ] ,

where in the symmetric case we can ignore the first term which just states that the sequence is Cauchy. The second term is equivalent to stating that a_{n} converges to a, that is, that d(a_{n}, a) converges to 0 – just take x to a.

We could also have replaced the ∧ in the formula for limsup with ⊗ while retaining the interpretation for the two special cases pre-orders and metric spaces. The author has not succeeded in finding an example that highlights the difference in the two definitions.

We relate our notion of limsup to the notion of indexed (co)limits in enriched categories. From [Street 76] we take the following definition specialized to Ω_{⊗}-categories from general V-categories.

Definition 3.31 Let J : [D−• Ω_{⊗}] and S : [D−• A] where D and A are Ω_{⊗}-categories. A J-weighted limit for S is an object lim_{J} S ^{∈} A_{0} together with an Ω_{⊗}-natural isomorphism (which in our case reduces to just an equality)

A(x, lim_{J}S) = [D−• Ω_{⊗}](J, A(x, S( )))

for all x ^{∈} A_{0} . The idea is that J provides an index of convergence of S. Example 3.1 and 3.2 below provide two illustrations of this. We define

Lim_{J}(S, a) = ⋀_{x^{∈}A_{0}}(A(x, a) •−• [D−• Ω_{⊗}](J, A(x, S( ))) ,

the degree to which a is a J-weighted limit of S . Dually a J-weighted colimit is an object colim_{J} S ^{∈} A_{0} together with an Ω_{⊗}-natural isomorphism

A(colim_{J}S, x) = [D−• Ω_{⊗}](J, A(S( ), x)) .

Also

Colim_{J}(S, a) = ⋀_{x^{∈}A_{0}}(A(a, x) •−• [D−• Ω_{⊗}](J, A(S( ), x))) .  □

We have used A(S( ), x) to denote the Ω_{⊗}-functor that takes n ^{∈} D_{0} into A(S(n), x) . Notice further with respect to the colimit which arrows get turned around compared to the limit, and which don’t. As usual J-weighted limits and colimits are unique up to isomorphism (see e.g. [Kelly 82]).

Example 3.1 Let Ω_{⊗} = 2 and D = (ℕ, =) , the discrete natural numbers. Then

Lim_{J}(S, a) = ∀x ^{∈} A_{0}. x ≤ a iff ∀n ^{∈} ℕ. J(n) → x ≤ S(n) .

Thus, Lim(S, a) is true if and only if a is the greatest lower bound of the set { S(n) | J(n), n ^{∈} ℕ } . Similarly the colimit object is the least upper bound of the same set. If we had used D = (ℕ, ≤) instead then J would have had to identify some (possibly empty) suffix of the S . □

Example 3.2 Let Ω_{⊗} = [0, ∞]_{+} and D = (ℕ, =) . Now the isomorphism reads

d(x, lim_{J} S) = sup_{n^{∈}ℕ}(d(x, S(n))−^{.}J(n)) .

Assuming that the limit exists, take x = lim_{J} S and we get that d(lim_{J} S, S(n)) ≤_{ℝ} J(n) for all n ^{∈} ℕ . Thus, J is an index of convergence and the sequence is converging in the standard metric sense if J(n) → 0 for n → ∞ . For symmetric metric spaces, naturally limits and colimits coincide. □

We can now define a convergence concept very close to ours. First a small auxiliary definition.

Definition 3.32 We define S_{≥N}(n) = S(n + N) for n, N ^{∈} ℕ . □

Definition 3.33 For an Ω_{⊗}-category A we say that a ^{∈} A_{0} is the limsup of S : [ℕ−• A] if

(i) There exists J : [(ℕ, ≤)−• Ω_{⊗}] such that it covers 1_{⊗}, that is, 1_{⊗} ≤ ⋁_{n^{∈}ℕ} J(n) ,

(ii) 1_{⊗} ≤ ⋁_{N^{∈}ℕ}[Cauchy(S_{≥N}) ∧ Colim_{J}(S_{≥N}, a)] . □

If we require J only to take the values 1_{⊗} and ⊥ we get the same notion as our limsup convergence.

Naturally we now define as follows.

Definition 3.34 An Ω_{⊗}-category is limsup complete if every (forward) Cauchy sequence has a limsup. It is directed (limsup) complete if every directed net has a limsup. □

The above analysis also answers (in the negative) the question whether we could have used filtered colimits in enriched categories directly, instead of inventing a new concept (well, limsup is hardly new). Filtered colimits are just colimits where the indexing category (J) is a filtered category, and that is not enough to obtain our dependency on the index N.

Notice that if a pre-order has limsups of all forward Cauchy sequences, then it has least upper bounds of all chains (in the traditional meaning of the word, a countable sequence (a_{n})_{n^{∈}ℕ} with a_{n} ≤ a_{n+1} for all n ^{∈} ℕ), since every chain is a forward Cauchy sequence with index 0 – it is well-behaved from the start – and the limsup of the sequence is its least upper bound. Moreover, if a pre-order is a cpo, that is, every chain has a least upper bound (no bottom required), then every forward Cauchy sequence has a limsup. Given a forward Cauchy sequence, it is a chain from some index on, and the least upper bound of this chain is the limsup of the sequence. Thus we have the following.

Proposition 3.11 The limsup complete pre-orders are precisely the cpos. □

We have the following observation.

Observation 3.5 Limsup completeness and Cauchy completeness are independent.

Proof : Examples of pre-orders that (all) are Cauchy complete but not limsup complete abound. Thus it suffices to find an Ω_{⊗}-category which is limsup complete but not Cauchy complete. Take Ω_{⊗} = 2 × 2 with elements named as follows.

[figure: u; ⊥; ⊤; v]

The tensor is normal conjunction. Let A be the discrete two element Ω_{⊗}-category with elements p and q. This means that A(p, q) = A(q, p) = ⊥ , and A(p, p) = A(q, q) = ⊤ . To see that A is limsup complete it suffices to observe that every sequence (a_{n})_{n^{∈}ℕ} with ⋁_{N^{∈}ℕ} ⋀_{m≥n≥N} A(a_{n}, a_{m}) ≥ ⊤ must have A(a_{n}, a_{m}) = ⊤ from some point N onward, which means that from that point it is constant. Its value after that point is then its limsup, naturally.

To see that A is not Cauchy complete as an Ω_{⊗}-category let ϕ be a bimodule defined as follows.

ϕ(p) = u and ϕ(q) = v .

Then ϕ ⊣ ϕ since (i) ϕ(a′) ⊗ ϕ(a) ≤ A(a, a′) and (ii) ⋁_{a^{∈}A_{0}} ϕ(a) ⊗ ϕ(a) ≥ ⊤ , but there is clearly no a ^{∈} A_{0} with ϕ(x) = A(a, x) for all x ^{∈} A_{0} . □

3.5 Banach’s fixed-point theorem

Consider Banach’s fixed-point theorem for metric spaces.

Theorem 3.4 ([Dugundji 66] p. 305) A contractive endo-map f : A → A on a non-empty complete metric space A has a unique fixed-point.

The proof starts by choosing an arbitrary a ^{∈} A_{0} and iterating f on a to obtain a sequence (f^{n}(a))_{n^{∈}ℕ} . One sees that

d(f^{i}(a), f^{i+1}(a)) ≤ ∑_{i=n}^{m−1} d(f^{i}(a), f^{i+1}(a))
≤ ∑_{i=n}^{m−1} ϵ^{i} · d(a, f(a))
= d(a, f(a)) · ∑_{i=n}^{m−1} ϵ^{i}
= d(a, f(a)) · ϵ^{n} \frac{1 − ϵ^{m−n}}{1 − ϵ} ,

where ϵ is a contraction coefficient for f . Then, since ϵ < 1 we see that (f^{n}(a))_{n^{∈}ℕ} is a Cauchy sequence, because for m ≥ n ,

ϵ^{n} \frac{1 − ϵ^{m−n}}{1 − ϵ} < \frac{ϵ^{n}}{1 − ϵ} ,

which converges to 0 for n → ∞ .

How can we generalize the notion of contraction to Ω_{⊗}-categories? We can to each endo-morphism f : A → A in Ω_{⊗}-CAT associate ϵ_{f} : Ω_{⊗} → Ω_{⊗} defined as ϵ_{f}(q) = ⋀{ A(f(a), f(a′)) | a, a′ ^{∈} A_{0}, q ≤ A(a, a′) } .

For a metric contraction f with contraction coefficient ϵ we see that ϵ_{f}(q) ≤_{ℝ} ϵ · q . Naturally we always have p ≤ ϵ_{f}(p) . With our definition we have

A(f^{n}(a), f^{m}(a)) ≥ ⨂_{i=n}^{m−1} A(f^{i}(a), f^{i+1}(a))
≥ ⨂_{i=n}^{m−1} ϵ_{f}^{i}(A(a, f(a))) .

Therefore (1) 1_{⊗} ≤ ⋁_{n^{∈}ℕ} ⋀_{m≥n} ⨂_{i=n}^{m−1} ϵ_{f}^{i}(A(a, f(a))) is a sufficient condition for a continuous f to have a fixed-point. We see immediately that (f^{n}(a))_{n^{∈}ℕ} is forward Cauchy, say with limsup x . Then f(x) = f(lim sup_{n} f^{n}(a)) = lim sup_{n} f(f^{n}(a)) = x . Notice that as usual, the limsup is only determined up to isomorphism, so x is also just a fixed-point up to isomorphism.

What does this mean when Ω_{⊗} = 2 ? Given any f we only have two possibilities for ϵ_{f} : 2 → 2 , viz. either constant ⊤ or the identity. In the first case (1) means that f is constant up to isomorphism and thus has a unique fixed-point. In the other case (1) reduces to ⊤ = ⋁_{n^{∈}ℕ} ⋀_{m≥n} A(a, f(a)) , that is, we just need an a ^{∈} A_{0} such that a ≤ f(a) . Of course, if A has a unique least element then we have a canonical choice for a , and the fixed-point based on a will be the least fixed-point, as is easily seen.

How about uniqueness of fixed-points? In the metric case this is achieved if we have all distances < ∞ because ϵ^{n} · d(a, a′) → 0 for n → ∞ if ϵ < 1 . For pre-orders of course, if a ≰ a′ then it is not reasonable to guarantee the existence of some n ^{∈} ℕ such that f^{n}(a) ≤ f^{n}(a′) . In fact, if this were the case for all a, a′ ^{∈} A_{0} then there would be n′ ^{∈} ℕ such that f^{n′}(a′) ≤ f^{n′}(a′) , so at m = max{n, n′} we would have f^{m}(a) equivalent to f^{m}(a′) . If this is fulfilled, then f does have a unique fixed-point up to equivalence.

54

Internalization

We have seen how we can express central concepts such as forward Cauchy sequence and limsup completeness in a language that uses the lattice theoretic operations on the underlying Ω_{⊗} together with inequality between elements of Ω_{⊗} . Insofar as we can interpret Ω_{⊗} as a space of truth-values and the lattice operations as logical operations, we can give a logical interpretation to our formulas. The advantage of this approach is mainly conceptual. A logical interpretation would facilitate the viewpoint that once Ω_{⊗} has been fixed we can imagine ourselves situated in a universe that uses the values of Ω_{⊗} as truth-values. Expressed in the internal language of our universe the properties of being forward Cauchy, being a limsup or being limsup complete become quite mundane, and logical manipulations replace lattice theoretical ones. Perhaps the largest single advantage is that Ω_{⊗}-categories become simply plain pre-orders. It should be easier in general to think about pre-orders than about enriched categories. Naturally, it is a matter of taste which formalism one prefers, but I also think that reasoning about quantifiers is easier for most people than reasoning with meets and joins. Another more specific aspect of internalization is that of local witnesses for existence. As we shall see in the section on power-sets, Chapter 6, an internal view can substantially simplify certain arguments.

At this place it is also in order to point out that the busy reader may skip this chapter. With an intuition that one can read ⋁ as ∃ and ⋀ as ∀ etc., the reader should be able to grasp the main points of the internal formulations that will follow.

Considering which universe we achieve with which Ω_{⊗} , we find that there are first and second class Ω_{⊗}’s. When Ω_{⊗} is a complete Heyting algebra and ⊗ = ∧ , the universe that naturally bases itself on Ω_{⊗} is that of sheaves on Ω_{⊗}. This is a universe of constructive higher-order logic. That means that we have a complete constructive set theory, in technical terms what is known as a topos. We are not so lucky when Ω_{⊗} is ‘just’ a quantale. In this case we only get a first-order logic with a linear ‘bend’ to it. Such logics, their differences based on different requirements to Ω_{⊗}, have been studied extensively recently. Some important sources are [Borceux & van den Bossche 91], [Ambler 92], [Rosenthal 90], and [van der Plancke 93] (the latter of which my missing skills in French prevents me from fully appreciating). We will not enter into any details here, merely notice that the logic based on commutative, unital quantales is strong enough to prove Scott’s inverse limit theorem. Specific investigations of the logic concerned with the special case where Ω_{⊗} is [0, ∞]_{+} or [0, ∞]_{max} should be at the core of ‘fuzzy logic’, and for a thorough exposition we refer the reader to [Wyler 91].

4.1 Preliminaries

We will give a brief introduction to the necessary concepts, viz. Ω-sets, quantale sets, presheaves, sheaves, topoi, and the logic in topoi. However, the exposition should serve more as a reminder and a statement about notation than a first introduction to the concepts just listed. For that a much longer text is needed, and we refer the reader to the following list of core references. [Fourman & Scott 77], [Mac Lane & Moerdijk 92], [Johnstone 77], [Troelstra & van Dalen 88], [Wyler 91], [Fourman 74], and also [Fourman 77], [Rosolini 80], [Ambler 92], and [Nawaz 85].

The intention behind the notion of an Ω-set is to model sets in a constructive universe with truth-values in Ω. Thus operations like equality (between members of sets) and set membership that usually yield values in 2 should now yield values in Ω . The standard theory of Ω-sets ([Fourman & Scott 77]) is based on Ω having stronger properties than those of a quantale.

Definition 4.1 A complete Heyting algebra (cHa) is a complete lattice in which the operation a ∧ has a right adjoint for every element a . We call this adjoint a → , and the operation → , implication. □

This means that a ∧ b ≤ c if and only if a ≤ b → c . We see that a cHa is just a unital commutative quantale where the tensor is ∧ . Prime examples are here 2 with the usual ∧ and [0, ∞]_{max} with ∧ = max . We could have defined cHa’s in another equivalent way, as the following proposition shows.

Proposition 4.1 A complete lattice (A, ≤) is a complete Heyting algebra if and only if

a ∧ ⋁ B = ⋁_{b^{∈}B}(a ∧ b)

for every a ^{∈} A and every B ⊆ A, □

Concerning implication we have the following.

Proposition 4.2 In a cHa (A, ≤) we have b → c = ⋁{ a ^{∈} A | a ∧ b ≤ c } . □

Complete Heyting algebras allow us to build a higher order intuitionistic logic with the usual interpretation of the quantifiers. This is the logic in the topos of sheaves over a cHa. One presentation of this theory ([Fourman & Scott 77]) uses so-called Ω-sets which are sets with an Ω-valued equality defined on them. We require that the equality be symmetric and transitive, but not that it be reflexive. Why not reflexive? The idea is that elements can be more or less defined, and only the totally defined (or global) elements are equal to themselves to the extent of ⊤_{Ω} .

Definition 4.2 An Ω-set is a pair A = (A_{0}, A( , )), where A_{0} is a set and A : A_{0} × A_{0} → Ω is a function such that for all a, b, c ^{∈} A, (i) A(a, b) = A(b, a), (reflexivity) and

(ii) A(a, b) ∧ A(b, c) ≤ A(a, c) (transitivity).

The function A is called an Ω-valued equality on A. We equip every Ω-set with a function, extent, E, defined as follows.

(iii) Ea = A(a, a),

Elements which have extent ⊤_{Ω} are called global or total. An Ω-set is global if all its elements are. As morphisms between Ω-sets (A_{0}, A) and (B_{0}, B) we take functions f on the underlying sets that respect the relation, i.e. where

(iv) A(a, a′) ≤ B(f(a), f(a′)) for all a, a′ ^{∈} A_{0}.

We denote by SET_{f}(Ω) the category of Ω-sets with morphisms as above. □

Example 4.1 This example is due to D. Scott. Consider a topological space T with opens OT , and define R_{0} = { x : U → ℝ | U ^{∈} OT } . We write dom x for the domain U of x above. We can define an equality R on R_{0} by taking R(x, y) = int{ t ^{∈} T | x(t) = y(t) } . Here we have used int(S) for the interior of a subset S of a topological space S, that is, int(S) is the union of all open sets contained in S. Clearly (R_{0}, R) is a OT -set. The extent of a function is its domain – a good example why we do not want reflexivity of equality. □

Example 4.2 Consider an ultra-metric space (M, d) where we allow distances to be infinite (alternatively we could restrict all distances to at most 1 – both amendments to the usual definition of (ultra) metric spaces allow us to take the distance between two functions to be the supremum of the distance between their values taken over their argument domain). We see that (M, d) is a global [0, ∞]_{max}-set. The strong triangular inequality of ultra-metric spaces is precisely the transitive law for equality. The morphisms are the mappings that do not increase distance. □

Observation 4.1 It is easy to see that (Ω, ↔) is itself a global Ω_{⊗}-set, and that (Ω, ∧) is a (not always global) Ω-set. □

Here, naturally, we mean a → b ∧ b → a when we write a ↔ b.

The article [Fourman & Scott 77] pioneered the use of so-called singletons as a useful conceptual tool to connect Ω-sets with sheaves, and with which to express completeness properties. Remember from Ω_{⊗}-categories how we defined subsets to be morphisms into Ω_{⊗} . With this in mind the following definition should be natural.

Definition 4.3 A singleton of an Ω-set A is a morphism s : A → (Ω, ↔) in SET_{f}(Ω) such that s(a) ∧ s(a′) ≤ A(a, a′) for all a, a′ ^{∈} A_{0} . □

It is intuitively helpful to read s(a) as a ^{∈} s. Notice, that the second requirement Fourman and Scott impose on singletons, viz. that they respect equality, is automatic when one requires them to be morphisms in SET_{f}(Ω) . To see this, observe that the morphism requirement is that A(a, a′) ≤ s(a) ↔ s(a′), which by adjointness implies A(a, a′) ∧ s(a) ≤ s(a′), which is the requirement about equality.

Definition 4.4 Given an element a in an Ω-set A, the function ã = A(a, ) : A_{0} → Ω denotes the map that takes a′ ^{∈} A_{0} to A(a, a′). It is easy to see that ã is a singleton for every a ^{∈} A_{0}. Given a singleton s : A_{0} → Ω and an element a ^{∈} A_{0} we say that s determines a if ã = s. □

Definition 4.5 An Ω-set is complete if every singleton determines a unique element and separated if a = a′ whenever Ea ∨ Ea′ ≤ A(a, a′). □

Notice, that for global Ω-sets, separatedness implies that a = a′ whenever A(a, a′) = ⊤.

Concerning completeness, a first observation is that for a global Ω-set to be complete the singleton which is constant ⊥ must determine a unique element, wherefore the Ω-set must be empty. We will return to the notion of completeness later, when we do not require globality.

We will continue our examples 4.1 and 4.2. Concerning Scott’s example, Example 4.1, with functions we see that as an Ω-set it is not global (with any but the trivial topology on T), since we can have functions that are not defined on the whole space. Separatedness means that if the union of the domains of two functions is a subset of the part of the intersection of their domains where they agree, then they are equal. Since this is the case, every such Ω-set is separated. Recall that the equality on the functions is R(f, g) = int{ x ^{∈} dom (f) ∩ dom (g) | f(x) = g(x) }. With respect to completeness we see that a singleton is a mapping s : { f : U → ℝ | U ^{∈} OT } → OT where (1) s(f) ∩ s(g) ⊆ R(f, g) and (2) s(f) ∩ R(f, g) ⊆ s(g) . From (1) we see that s(f) ⊆ dom (f) for all f, and we see that every singleton s determines a function f_{s} which has as domain ⋃_{f:U→ℝ} s(f) and on a ^{∈} dom (f_{s}) takes the value of any f(a) where a ^{∈} s(f). That there is such one is by definition of the domain of f_{s}, and to see that they all agree, let f, g be such that a ^{∈} s(f) and a ^{∈} s(g). Then, by (1) we know that a ^{∈} R(f, g), and thus that f(a) = g(a). Thus Scott’s Ω-sets of functions are complete. Notice, that even if we had required the functions to be continuous we would still have had a complete Ω-set. The f constructed as above would be continuous.

Concerning Example 4.2 we can introduce partial elements in form of closed disks, where we define equality as

d(A, B) = sup_{a^{∈}A_{0}} sup_{b^{∈}B_{0}} d(a, b) ,

which one can read as a worst case distance – choose a random element from A and a random element from B – how far do we risk that they are apart. Naturally, d is not a metric since d(A, A) is not 0 for any A except singletons. However, d is symmetric and transitive, so the set of disks (or for that matter all subsets) of A equipped with d as equality, is an [0, ∞]_{max}-set. Since diameter and radius is the same for ultra-metric spaces, and every point in a disk is a center point, the extent of a disk is its diameter. The global elements are the original points, seen as disks with diameter 0 . The most undefined element is the whole space. Which such spaces are separated? Given two disks A and B , assume the minimum of their diameter is greater than or equal to d(A, B) . Observe that for ultra-metric spaces, two given disks are either disjoint of one is inside the other. Thus, if A and B are inside each other the condition is only fulfilled if A = B . If they are disjoint the condition cannot be fulfilled, and therefore every such space is separated.

We can generate another space of the disks by taking the distance to be the normal Hausdorff distance, and in this case of course, we get a global space.

When it comes to morphisms between Ω-sets it turns out that the category SET_{f}(Ω) for many purposes has too few. To allow the morphisms to adequately reflect the possibility for elements to be partial it is best to work with functional relations. As was the case for enriched categories some amount of internalization will make our formulations more streamlined.

Products are defined analogously to tensor products for Ω_{⊗}-categories.

Definition 4.6 Given two Ω-sets A and B their product A × B is (A_{0} × B_{0}, (A × B)) , where (A × B)((a, b), (a′, b′)) = A(a, a′) ∧ B(b, b′) . □

As for Ω_{⊗}-categories we have the following easily proven proposition.

Proposition 4.3 When A and B are Ω-sets, so is A × B. □

We define the function space by letting the set part be the set of morphisms, and the relations be as follows.

(A → B)(f, g) = ⋀_{a^{∈}A_{0}}(Ea → B(f(a), g(a))).  (4.1)

Proposition 4.4 (A → B) is an Ω-set whenever A and B are.

Proof : To show that (A → B) is transitive we have to prove

(A → B)(f, g) ∧ (A → B)(g, h) ≤ (A → B)(f, h) ,

that is, since (A → B)(f, h) = ⋀_{a^{∈}A_{0}}(A(a, a) → B(f(a), h(a))) ,

(A → B)(f, g) ∧ (A → B)(g, h) ≤ A(a, a) → B(f(a), h(a))

for every a, but by adjunction (and unfolding definitions) this is equivalent to

\begin{matrix}A(a, a) ∧ ( ⋀_{a^{∈}A_{0}}(A(a, a) → B(f(a), g(a))) ∧ ⋀_{a^{∈}A_{0}}(A(a, a) → B(g(a), h(a)))) ≤ \\ B(f(a), h(a)) , \end{matrix}

which results from distributivity of ∧ over ∧ and transitivity of B. □ In fact we have the following.

Proposition 4.5 SET_{f}(Ω) is a Cartesian closed category.

Proof : As the terminal element we have the one element Ω-set with global extent – that the extent is global is necessary for there being a morphism from every other Ω-set. Evaluation in SET_{f}(Ω) is also a morphism as is easily seen, and there is an adjunction (A × ) ⊣ (A → ) in SET_{f}(Ω), as the following calculation shows (using symmetry of A).

A ∧ (A → B)((a, f), (a′, g)) = A(a, a′) ∧ ⋀_{a′′^{∈}A_{0}}(A(a′′, a′′) → B((a′′), g(a′′)))
≤ A(a, a′) ∧ (A(a′, a′) → B(f(a′), g(a′)))
≤ A(a, a′) ∧ A(a′, a′) ∧ (A(a′, a′) → B(f(a′), g(a′)))
≤ A(a, a′) ∧ B(f(a′), g(a′))
≤ B(f(a), f(a′)) ∧ B(f(a′), g(a′))
≤ B(f(a), g(a′)) .

□

However, to deal better with partiality we define as follows, mainly following [Wyler 91] and [Fourman & Scott 77].

Definition 4.7 A relation from an Ω-set A to an Ω-set B is a morphism in SET_{f}(Ω) from A × B to (Ω, ↔). We denote by REL(Ω) the category of Ω-sets with relations as morphisms.

□

We see that a relation f from A to B is a mapping f_{0} : A_{0} × B_{0} → Ω on the underlying sets that is extensional: A(a, a′) ∧ B(b, b′) ≤ f_{0}(a, b) ↔ f_{0}(a′, b′). In the sequel we will omit the subscript that distinguishes a morphism from its underlying function.

Definition 4.8 A functional relation between Ω-sets A and B is a relation f from A to B which fulfills

(i) f(a, b) ∧ f(a, b′) ≤ B(b, b′) (single-valuedness), and

(ii) ⋁_{b^{∈}B_{0}} f(a, b) = A(a, a) (totality).

We denote by SET(Ω) the sub-category of REL(Ω) with functional relations as morphisms. □

As we shall see in a moment, conditions (i) and (ii) can be stated as a simple adjointness condition.

We can make the relations and the functional relations between two Ω-sets into an Ω-set analogously to how we made bimodules between Ω_{⊗}-categories into an Ω_{⊗}-category, and we define composition in the same way as for bimodules between Ω_{⊗}-categories.

Observation 4.2 For an Ω-set A, the relation A( , ) is itself a relation from A to A . □

To a relation f : A ⇒ B between Ω-sets there is an obvious corresponding relation f^{op} : B ⇒ A defined as f^{op}(b, a) = f(a, b) .

Definition 4.9 We say that one relation f : A ⇒ B is left-adjoint to another, g : B ⇒ A, in REL(Ω) if f ∘ g ≤ B and A ≤ g ∘ f . □

Spelled out this means that

⋁_{a^{∈}A_{0}} f(a, b′) ⊗ g(b, a) ≤ B(b, b′) and A(a, a′) ≤ ⋁_{b^{∈}B_{0}} g(b, a′) ⊗ f(a, b)

for all a, a′ ^{∈} A_{0} and all b, b′ ^{∈} B_{0}.

We thus see that conditions (i) and (ii) from definition 4.8 reduce to requiring f ⊣ f^{op} in REL(Ω) (see also [Ambler 92]), and we have the following proposition.

Proposition 4.6 A relation f from A to B in REL(Ω) is functional if and only if f ⊣ f^{op}. □

Remark 4.1 Note, that we can see a singleton s : A → Ω as a relation s : 1l ⇒ A , and the requirement s(a)∧s(a′) ≤ A(a, a′) amounts to single-valuedness according to Def. 4.8(i), and a singleton is total (has extent ⊤) if and only if it as a relation fulfils the requirement of totality from Def. 4.8(ii). □

The categorical structure of SET(Ω) is as nice as one can want it, viz a (-n elementary) topos. For completeness we state the definition of an elementary topos, but refer the reader to some of the many sources ([Mac Lane & Moerdijk 92], [Wyler 91], [Fourman 74], [Fourman & Scott 77]). There are many equivalent definitions. The following one comes from [Mac Lane & Moerdijk 92].

The central concept to introduce is that of a sub-object classifier. Consider in SET the role of the two point set, {⊤, ⊥} say. Given any set A and a subset A′ thereof, we have a characteristic function for A′ which takes every a ^{∈} A into ⊤ if a ^{∈} A′ and into ⊥ otherwise. With this motivation the following definition should seem reasonable.

Definition 4.10 In a category with finite limits a sub-object classifier is an object O together with a monomorphism, ⊤ : 1l → O such that for every monomorphism m : A′ → A there is a unique morphism chm : A → O such that the following diagram is a pullback square.

[figure: A; A′; O; 1l; m; ⊤; ·; chm]

A topos is a category with finite limits, exponentials and a sub-object classifier. □

To see that SET(Ω) is a topos we first have to determine the terminal object and the sub-object classifier. The terminal object 1l is (Ω, ∧) . Intuitively an element a from an Ω-set A is mapped into Ea from (Ω, ∧) . Expressed in terms of functional relations then, the value of the unique map into 1l from A of (a, p) with a ^{∈} A_{0} and p ^{∈} Ω is Ea∧p . We will thus denote the unique map into 1l as E . The sub-object classifier plays the role as the internal truth-values. It is the set { (p, q) ^{∈} Ω × Ω | p ≤ q } with the equality ((p, q) = (p′, q′)) = (p ↔ p′) ∧ q ∧ q′ , denoted (Ω, ↔) , together with the morphism ⊤ : 1l → (Ω, ↔) . See also [Fourman & Scott 77].

Proposition 4.7 SET(Ω) is a topos for every cHa Ω .

Proof : See loc. cit. □ Ungrateful as we are, having just introduced relations to cater for partiality we admit

that we would prefer to work with functions. Luckily, in the case of Ω-sets, by restricting the set of objects we can achieve that every functional relation is generated by precisely one function, a fact which then of course has the desired effect. To account for which restriction to do we have to develop a few more concepts. The development follows essentially loc. cit.

4.2 Pre-sheaves and sheaves

Where Ω-sets generalize the notions of equality and extent in an intuitionistic framework, presheaves generalize the notions of extent and restriction, also in an intuitionistic framework. In the setting of presheaves, equality can be defined, and it turns out that every presheaf corresponds to an Ω-set. Not every Ω-set is a presheaf: Some restrictions may be missing. However, one can always add them, possibly also introducing certain equivalences, though.

Definition 4.11 A presheaf over a cHa Ω is a triple (A_{0}, E, †) where A_{0} is a set, and extent, E : A_{0} → Ω, and restriction, † : A_{0} × Ω → A_{0} fulfil

(i) a † Ea = a ,

(ii) (a † p) † q = a † (p ∧ q) ,

(iii) E(a † p) = Ea ∧ p ,

for all a ^{∈} A_{0} and all p, q ^{∈} Ω. On any presheaf we define equality thus:

(iv) [[a = b]] = ⋁{ p ≤ Ea ∧ Eb | a † p = b † p } . □

As a matter of fact, there is an equivalent and much shorter definition of the notion of a presheaf over Ω . It is simply a functor from Ω^{op} to SET , where we obviously regard Ω as a category in the way we always regard pre-orders as (standard) categories, viz. by having an arrow from q to p if and only if q ≤ p . Let us see how the two definitions correspond to each other.

First, let F : Ω^{op} → SET be a functor. We take as A_{0} the disjoint union of F (p) for all p ^{∈} Ω , that is, { (s, p) | p ^{∈} Ω and s ^{∈} F (p) } . Then we define E(s, p) = p and (s, p) † q = (s, p ∧ q) .

To see that (A_{0}, E, †) defined in this way fulfil 4.11, (i)-(iii) we calculate.

(i) (s, p) † E(s, p) = (s, P ∧ p) = (s, p) ,

(ii) (s, p) † q † r = (s, p ∧ q ∧ r) = (s, p) † (q ∧ r) ,

(iii) E((s, p) † q) = p ∧ q = E(s, p) ∧ q .

Second, let the presheaf (A_{0}, E, †) be given. Define F (p) = { a ^{∈} A_{0} | Ea = p } , and F (p ≥ q) to be the mapping from F (p) to F (q) that takes a into a † q . It is easy to see that the correspondence we have defined is an isomorphism.

As morphisms among presheaves in Ω^{op} → SET we take simply the natural transformations. To illustrate what they amount to in our alternative view of presheaves, consider two presheaves F, G : Ω^{op} → SET and a natural transformation α : F →^{·} G . This means that for every p ^{∈} Ω we have a morphism in SET, viz. α_{p} : F (p) → G(p) . Further, for p ≥ q we have a commuting diagram

[figure: F (p); F (q); G(p); G(q); F (p ≥ q); α_{p}; α_{q}; G(p ≥ q)]

which means that for every t ^{∈} F (p) we have α_{p}(t) † q = α_{q}(t † q) . We have here and will in the sequel use the notation a † q for F (Ea ≥ q)(a) when F is clear from the context. Thus, if we view F and G as sets with extent and restriction, (F_{0}, E, †) and (G_{0}, E, †) say, then the above rules mean that we can express the set of morphisms between F and G as those mappings α : F_{0} → G_{0} on the underlying sets which fulfil

(i) Eα(a) = Ea (preserves extent),

(ii) α(t) † p = α(t † p) (commute with restrictions).

In other words, we have lumped the natural transformation together along Ω .

Definition 4.12 By SET^{Ω^{op}} we denote the category of presheaves over Ω with natural transformations as morphisms. □

Consider the two examples of Ω-sets from above. To see those Ω-sets as presheaves we can maintain the same sets of elements, and define the extent of a function f : U → ℝ as U and restriction as restriction in the traditional sense. For ultra-metric spaces extent is diameter and to restrict a disk means to blow it up to a larger diameter.

We can in general see every presheaf as an Ω-set because the defined equality on presheaves is symmetric and transitive. As previously mentioned, it is not always possible to do the converse – some restrictions may be missing.

A further requirement on how overlapping restrictions fit together leads us from presheaves to sheaves. One motivation for using sheaves has to do with descriptions. When we interpret a language in (pre)sheaves we might want to give the iota function a meaning, such that

[figure: (t_{x}, t_{y}, t_{z}); \begin{matrix}t_{x} † x ∧ x & t_{x} † x ∧ y & t_{x} † x ∧ z \\ t_{y} † y ∧ x & t_{y} † y ∧ y & t_{y} † y ∧ z \\ t_{z} † z ∧ x & t_{z} † z ∧ y & t_{z} † z ∧ z \end{matrix}; \begin{matrix}t_{x} † x ∧ x & t_{y} † x ∧ y & t_{z} † x ∧ z \\ t_{x} † y ∧ x & t_{y} † y ∧ y & t_{z} † y ∧ z \\ t_{x} † z ∧ x & t_{y} † z ∧ y & t_{z} † z ∧ z \end{matrix}; α; β]

Figure 4.1: Restricting along first or second coordinate

ιx.ϕ(x) denotes the ‘largest’ (i.e. with largest extent) x with the property ϕ. The interpretation of such a formula will be a singleton, and in a sheaf every singleton determines a unique element.

In terms of pre-sheaves over a cHa we can formulate a definition of sheaves as follows, following [Mac Lane & Moerdijk 92].

Definition 4.13 For X ⊆ Ω and p ^{∈} Ω we say that X covers p if ⋁ X = p. We write C(p) for the set of covers of p. □

Remark 4.2 In the two point cHa, 2, to cover ⊤, a set has to contain ⊤, but in [0, ∞] with 0 = ⊤, to cover 0, we can make do with, say, (0, 1]. This is the difference between the ‘true for all’ arguments in pre-orders and the ‘for all ϵ greater than zero’ arguments for metric spaces. We will see how far this carries in general arguments for metric spaces and pre-orders.

Definition 4.14 A presheaf F : Ω^{op} → SET is called a sheaf if for each p ^{∈} Ω and each cover Q ⊆ Ω of p we have an equalizer diagram

[figure: F (p); ∏_{q^{∈}Q} F (q); ∏_{r,s^{∈}Q} F (r ∧ s); e; α; β]

where for t ^{∈} F (p) we define e(t) = { t † p ∧ q | q ^{∈} Q } and where for (t_{q})_{q^{∈}Q} ^{∈} ∏_{q^{∈}Q} F (q) we define α((t_{q})_{q^{∈}Q}) = (t_{r} † r ∧ s)_{r,s^{∈}Q} and β((t_{q})_{q^{∈}Q}) = (t_{s} † r ∧ s)_{r,s^{∈}Q} . □

We illustrate how α and β work with Figure 4.1. Here we assume that x, y, and z combine to cover p . The figure shows how α and β map a generic element of ∏_{q^{∈}Q} F (q) into ∏_{r,s^{∈}Q} F (r∧ s) . That we have a morphism e that makes the diagram commute means that there exist (t_{q})_{q^{∈}Q} such that t_{r} †r ∧s = t_{s} †r ∧s for all r, s ^{∈} Q , that is, the order of restriction does not matter. That e has domain F (p) and is defined as it is means that there is a ‘global’ (relative to p) element t_{p} such that for any r, s ^{∈} Q we have t_{p} † r † r ∧ s = t_{p} † s † r ∧ s , again – the order of restriction doesn’t matter. That e is an equalizer means that t_{p} is unique.

As morphisms between sheaves we just inherit them from presheaves.

Definition 4.15 With Sh(Ω) we denote the category of sheaves over Ω with natural transformations as morphisms. □

We can define the notion of sheaf in several other ways. To give one alternative, we will introduce a notion of separatedness for presheaves (see [Fourman & Scott 77] p. 342).

Definition 4.16 Given a presheaf (A_{0}, E, †) we define a pre-order ≤: A_{0} ×A_{0} → 2 by a ≤ a′ if and only if a = a′ † Ea . A subset B ⊆ A_{0} is called compatible if b † Eb′ = b′ † Eb for every b, b′ ^{∈} B . When we talk about joins or upper bounds of subsets of A_{0} we mean joins and upper bounds in the pre-order (A_{0}, ≤) . We call a presheaf separated if every subset of A_{0} has at most one minimal upper bound. □

Proposition 4.8 A presheaf is a sheaf if and only if every compatible subset of its underlying set has a join. □

We could in fact have defined sheaves in a third way, viz. as complete Ω-sets. It is proven in [Fourman & Scott 77] that a sheaf and a complete Ω-set come to the same thing. We will just give the correspondence, also from loc. cit. Given a sheaf, view it as a triple (A_{0}, E, †) , and associate with it the Ω-set (A_{0}, A) , where A is the defined equality on the presheaf. The other way, given a complete Ω-set (A_{0}, A) we can define extent as usual, and to see that we have all the restrictions we need, let a ^{∈} A_{0} and p ^{∈} Ω be given. Then notice, that the mapping A(a, ) ∧ p is a singleton. By completeness it determines a unique element which we will call a † p . It turns out that restrictions defined in this way work as they should.

One important question is now how the sheaf morphisms look, when we look at sheaves as complete Ω-sets.

Given (A_{0}, A) and (B_{0}, b) , two complete Ω-sets and a functional relation f : A ⇒ B , we can define f′(a) = ⋁{ b † f(a, b) | b ^{∈} B } = ⋁ B_{a} . It is not hard to see that B_{a} is compatible (see [Fourman & Scott 77]). This means that the morphisms from A to B as sheaves (ie. in Sh(Ω)) are the same as the morphisms from A to B as complete Ω-sets (ie. in SET(Ω)). Thus, if we define CSET(Ω) as the full subcategory of SET(Ω) consisting of all the complete Ω-sets, we have an isomorphism between categories, Sh(Ω) ≅ CSET(Ω) . This was all we came for – we wanted a constructive universe where we could work with functions in place of functional relations, and we got the universe Sh(Ω) . The price is that we can only work with sheaves.

An important notion yet to cover here is that of sheafification, which is the process of completing in a certain sense to be made precise below Ω-sets or presheaves to make them sheaves. It turns out that every Ω-set and every presheaf can be ‘sheafified’ in a universal way.

Definition 4.17 The sheafification Â of an Ω-set A is the Ω-set defined by (i) Â_{0} = { s : A_{0} → Ω | s is a singleton } ,

(ii) Â(s, t) = ⋁_{a^{∈}A_{0}}(s(a) ∧ t(a)), for all s, t ^{∈} |Â| . □

Paying justice to the name of the process the following proposition holds.

Proposition 4.9 The sheafification of any Ω-set is complete. □

The following theorem originates with Higgs and independently with Fourman and Scott. Here we quote from [Fourman & Scott 77].

Theorem 4.1 The categories Sh(Ω) and SET(Ω) are equivalent.

Proof : (sketch) The mapping A ↦ Â can be made into a functor in the following way. Let f : A → B be a morphism in SET(Ω), i.e. a functional relation. We define f̂(s)(b) = ⋁_{a^{∈}A_{0}} s(b) ∧ f(a, b) for a ^{∈} A_{0}, b ^{∈} B_{0}, and s : A_{0} → Ω a singleton. This sheafification functor is an equivalence of categories. The actual proof of this statement is somewhat elaborate and can be found in [Fourman & Scott 77] □

Letting CSET_{f}(Ω) stand for the category of complete Ω-sets with functions we can illustrate some of the connections between the many categories outlined above with the following diagram.

[figure: Sh(Ω); CSET(Ω); SET^{Ω^{op}}; CSET_{f}(Ω); SET(Ω); SET_{f}(Ω); REL(Ω); s; full; s; full; full; full; full]

Diagram 4.1: Categories of Ω-sets, presheaves and sheaves.

The arrows marked ‘full’ are full embeddings, and the two connections without arrow heads are isomorphisms of categories. ‘s’ stands for sheafification in two instances. In both these cases sheafification is left adjoint to the embedding.

Observation 4.3 By Theorem 4.1 sheafification preserves all limits and colimits. □

Example 4.3 We have already seen that an ultra-metric space and a global [0, ∞]_{max}-set come to the same thing, also when it comes to the natural morphisms in the two categories. As a simple special case of Walters’ theorem ([Walters 82]) we will show that in this case metric completion and sheafification coincide.

So let A = (A_{0}, d) be an ultra-metric space. Identify A with the global, separated Ω-set (A_{0}, d) . Then the sheafification Â of A consists of the singletons s : A_{0} → [0, ∞]_{max} with

d(s, t) = ⋁_{a^{∈}A_{0}}(s(a) ∧ t(a)) = inf_{a^{∈}A_{0}} max{s(a), t(a)}.

We have that s : A_{0} → [0, ∞]_{max} is a singleton if and only if for all a, b ^{∈} A_{0},

s(a) ∧ d(a, b) ≤ s(b) & s(a) ∧ s(b) ≤ d(a, b)  iff
max{s(a), d(a, b)} ≥ s(b) & max{s(a), s(b)} ≥ d(a, b) iff
s(a) = s(b) ≥ d(a, b) or d(a, b) = max{s(a), s(b)}.

By the definition of equality on (pre)sheaves we get that a singleton s is global if and only if d(s, s) = ⊤, i.e. if and only if inf_{a^{∈}A_{0}} s(a) = 0.

Given a metric space (A_{0}, d) and a singleton s : A → [0, ∞]_{max}, it is clear how to conceive s as a ‘phantom’ point a_{s} in A_{0}. Like any ‘normal’ point of A_{0} we can see a singleton as mapping any pair of points a and b into a triangle given by its three sides, s(a), s(b), and d(a, b). The above characterization of singletons assures that this triangle is isosceles. To make a singleton s into a new point a_{s} in A_{0} we simply define d(a, a_{s}) = s(a) for any (other) point a in A. We see that if s is global and a_{s} does not already exist, a_{s} will become an accumulation point, and that if (A_{0}, d) is complete it will already exist. Sheafification can thus be seen as a way of adding points to a metric space. We shall make this more precise in the following.

Let ΓS denote the set of global elements of the sheaf S.

Lemma 4.1 For any complete ultra-metric space A, we see that A_{0} is as a set isomorphic to the set of global elements of the sheafification of the Ω-set that corresponds to A. That is

A_{0} ≅ ΓÂ.

Proof : Given a global singleton s : A_{0} → [0, ∞]_{max} we find the unique corresponding a_{s} ^{∈} A as follows. Since inf_{a^{∈}A_{0}} s(a) = 0 the set \{ a ^{∈} A_{0} | s(a) < \frac{1}{n} \} is non-empty for every natural number n. We can therefore choose a sequence (a_{n})_{n^{∈}ω} such that s(a_{n}) < \frac{1}{n} for every n. By the properties of singletons, d(a_{n}, a_{m}) ≤ max{s(a_{n}), s(a_{m})}, so (a_{n})_{n^{∈}ω} is a Cauchy sequence, and by completeness of A, convergent to some a_{s} ^{∈} A_{0}. We must show that s(a_{s}) = 0. But by properties of singletons, s(a_{s}) ≤ max{s(a_{n}), d(a_{n}, a_{s})} for all n ^{∈} ω, and we have the result.

On the other hand, given an a ^{∈} A_{0}, the corresponding global singleton is λb ^{∈} A.d(a, b). This mapping is clearly injective and the inverse of the above. □

In fact, we do not need complete spaces to start with. The sheafification gives us the same completion as we would get metrically. This is the contents of the following theorem.

Theorem 4.2 For any ultra-metric space A, the metric completion \overline{A} of A is as a set isomorphic to the set of global elements of the sheafification of the Ω-set that corresponds to A. That is

\overline{A} ≅ ΓÂ.

Proof : We now want to show that any global singleton corresponds to a Cauchy sequence, and that different global singletons correspond to non-equivalent Cauchy sequences.

We have already shown the first part in the proof of lemma 4.1. To see the latter, consider how we go from a Cauchy sequence to a global singleton. Given (a_{n})_{n^{∈}ω} we take the corresponding global singleton to be λa ^{∈} A_{0}. lim_{n→∞} d(a_{n}, a).

Given a global singleton s we should now verify that when (a_{n})_{n^{∈}ω} is chosen such that s(a_{n}) < \frac{1}{n} for every natural number n, then λa ^{∈} A. lim_{n→∞} d(a_{n}, a) = s, that is s(a) = lim_{n→∞} d(a_{n}, a) for every a ^{∈} A_{0}. By properties of singletons we have for all n ^{∈} ω:

(i) s(a) ≤ max{d(a_{n}, a), s(a_{n})},

(ii) d(a_{n}, a) ≤ max{s(a), s(a_{n})}.

(Notice, how this indicates to which extent s can be seen as a point in an ultra-metric space—read s(a) as d(a, s).) By the choice of (a_{n})_{n^{∈}ω} we have s(a_{n}) → 0 for n → ∞, and the desired equality is immediate. □

4.3 Cauchy completion and sheafification

For a general connection between Cauchy completeness and sheafification, see [Walters 81] and in a more general setting [Walters 82]. We will, out of the general interest of the setting Walters presents give a brief resume of the main points.

Walters uses bicategories instead of categories as base structures for enriched categories. We will give the basic definitions for bicategories and bicategory-enriched categories. A bicategory is like an enriched category in that it consists of a set S_{0} of objects connected with a hom that connects any two elements of S_{0}. However, where we in an enriched category have a single base category the objects of which is the codomain of the hom, then in a bicategory we require that the hom between any two elements is a category. It could then look as if a bicategory is a CAT-enriched category (which is the same as a 2-category – not to be confused with a 2-category, which is a category enriched over the two-point lattice), but the coherence conditions are weakened.

Walters considers a particular kind of bicategory B, viz. one which is locally posettal, which means that B(a, b) is a poset for every a, b in B_{0}. (So we have something that is very similar to a poset enriched category here - as the base category?) Sometime it is further required that B(a, b) is a cL and that composition, ∘, in B preserves colimits (sups). (So A ∘ has a right adjoint, A−• , say).

We can use the extra structure of a bicategory compared to that of a normal category in that we can now vary the category in which the hom between two objects (in the enriched category) lie.

Consider a metric space as an enriched category. It is reasonable that all distances (homs) between points (objects) lie in the same category, the pre-order [0, ∞]. However, if we were to introduce partial elements (disks) and use a ‘worst case’ distance between them, then obviously, if a disk has radius r then its distance to any other ‘point’ will be at least r. Thus the natural codomain category for homs starting from such a disk is [r, ∞]. In general, for two disks with radius r and t respectively their hom should be in [max{r, t}, ∞].

We thus have one component of a B-enriched category S being a mapping e from the set of elements S_{0} to B_{0}, and another component being the generalization of our hom from standard enriched categories, viz a mapping S : S_{0} × S_{0} → B_{1} where S(a, b) : B(e(a), e(b)), that is, S(a, b) is a morphism from e(a) to e(b). Since B(x, y) is a poset we can recognize our simple enriched categories - let B_{0} be a singleton set and B_{1} for instance 2 or [0, ∞]_{+}. We require further that 1_{e(x)} ≤ S(x, x) and S(x_{1}, x_{2}) ∘ S(x_{2}, x_{3}) ≤ S(x_{1}, x_{3}) (where we perhaps should write composition the other way around). Think of e as extent.

Concerning B-functors we have to take care that we can at all compare the hom between the arguments with the hom between the results. We thus require of a functor f : S → T that e(f(x)) = e(x), and then the standard S(x, y) ≤ T (f(x), f(y)).

Example 4.4 (from Walters):

Let (H, ≤) be a Ha and construct a bicategory H^{∗} thus:

H_{0}^{∗} = H, H(a, b) = ({ c | c ≤ a ∧ b }, ≤), composition in H is intersection. Let (F, [ = ]) be an H-set. We form a H^{∗}-enriched category F^{∗} thus:

F_{0}^{∗} = F, e(a) = Ea, F^{∗}(a, b) = [a = b]. The bicategory now is used to express the fact that [a = b] cannot exceed Ea (or Eb), but takes values in H(a, b) = { c | c ≤ Ea ∧ Eb }. □

Walters now shows ([Walters 81]) that if H is a cHa then Sh(H) is equivalent to the category of skeletal symmetric Cauchy complete H^{∗}-categories, where a B-category is skeletal if whenever (taken from [Walters 82], not from [Walters 81]) e(x) = e(x′) = u and 1_{u} ≤ B(x, x′) ∧ B(x′, x) then x = x′. This corresponds to the notion of skeletal categories from standard category theory, where a category is skeletal if the only isomorphisms between objects are the identities.

So perhaps we should look at B-categories instead of Ω_{⊗}-categories. The proper B for classical pre-orders and metric spaces are just the one object B’s, corresponding to 2 and [0, ∞]_{+}, but if we want to look at them in a better logic, perhaps it is enough to be able to vary the object along 2 (or [0, ∞]_{+}) like above. One issue here is how to express the Cauchy condition with B-categories. The reason why we have not pursued this line is twofold. First, we found that the simpler approach works, and as a first step it seems to be adequate. Also for pedagogical reasons it seems to be reasonable to stay simple at the outset.

4.4 Internal logic

In this section we will discuss how to interpret formulas in higher order logic in sheaves over a cHa. This means that we can choose in the sequel whether we want to formulate properties of apos and their elements externally, only using the global sections and the lattice operations on Ω or internally, using logical connectives instead.

We use the logic of forcing over Ω, that is, the logic in Sh(Ω). For a good reference to forcing over a cHa, see [Troelstra & van Dalen 88] volume II, and also in general for internal logic in a topos, for instance [Mac Lane & Moerdijk 92], [Johnstone 77], or [Fourman 74].

Definition 4.18 For an atomic formula ϕ with value [[ϕ]] = p ^{∈} Ω we define q ⊢⊢ ϕ if q ≤ p. For composite formulae we define forcing as follows (taken from [Troelstra & van Dalen 88] p. 720 with minor typographical changes). By A(q) we denote the set of sections of the sheaf A over q.

q ⊢⊢ ϕ ∧ ψ  if q ⊢⊢ ϕ and q ⊢⊢ ψ,
q ⊢⊢ ϕ → ψ  if ∀q′ ≤ q. [q′ ⊢⊢ ϕ implies q′ ⊢⊢ ψ] ,
q ⊢⊢ ϕ ∨ ψ  if ∃E ^{∈} C(q). ∀q′ ^{∈} E. [q′ ⊢⊢ ϕ or q′ ⊢⊢ ψ] ,
q ⊢⊢ ∀x ^{∈} A. ϕ(x) if ∀q′ ≤ q. ∀a ^{∈} A(q′). q′ ⊢⊢ ϕ(a),
q ⊢⊢ ∃x ^{∈} A. ϕ(x) if ∃E ^{∈} C(q). ∀q′ ^{∈} E. ∃a ^{∈} A(q′). q′ ⊢⊢ ϕ(a).

We write ⊢⊢ ϕ for ⊤ ⊢⊢ ϕ. □

4.5 Quantale logic

In the cases where ⊗ is not ∧ we do not have the topos of sheaves over Ω_{⊗} as our universe. Many attempts have been made to extend parts of the theory of sheaves over cHa’s to sheaves over some restricted class of quantales. In Nawaz’ thesis ([Nawaz 85]) it is required that the quantales be idempotent, something which is not fulfilled by e.g. [0, ∞]_{+}, where a + a = a only for a = 0 or a = ∞.

Later works, e.g. [Borceux & van den Bossche 91], [van der Plancke 93], and [Ambler 92] does not have this requirement, and also the work on ∗-autonomous categories ([Barr 80] and e.g. [Girard 87], [Blute 93], and [Rosenthal 92]) points towards a clarification of quantales as a foundation for linear logic.

However, instead of pursuing a formal internalization here in terms of (probably the multiplicative fragment of linear logic) we have taken the simple-minded path and reasoned externally with the quantale structure of Ω_{⊗} in the theory leading up to Scott’s inverse limit theorem. This means that we really ought to have two versions of the forthcoming development, an internal and an external. However, it turns out that the correspondence between the internal and the external formulations is so straightforward that such a parallel approach would be tediously repetitive. The only aspect in this connection one has to be alert to in what follows is the occasional temptation to use a = a ⊗ a in connection with a (non-) rule like a⊗(a−• b)⊗(b−• c) ⊢ b⊗c. It turns out that the complete internal development can be done in a style that remains valid in the linear case. Naturally then, we only use first order reasoning. We have thus adopted an internal formulation that is immediately valid in sheaves over a cHa, but where the corresponding external formulation is valid over any commutative unital quantale Ω_{⊗}.

4.6 Internal enriched categories: APOs

In order to be able to reason about our enriched categories in an Ω-valued logic we define the analogue of an enriched category internally in sheaves over a cHa. We will use the term abstract pre-order for this concept. Thus, an abstract pre-order is a morphism in Sh(Ω), say A : A_{0} × A_{0} → Ω, where Ω is the subobject classifier, and where we require that A fulfils the usual axioms of reflexivity and transitivity for pre-orders, expressed internally, which motivates the following definition.

Definition 4.19 We write APO(Ω) for the category of abstract pre-orders (apos) over Ω. The objects are pairs (A_{0}, A), where A_{0} is a sheaf over Ω and where, A : A_{0} × A_{0} → Ω is reflexive and transitive, that is, where ⊢⊢ (a = b) → A(a, b) and ⊢⊢ A(a, b)∧A(b, c) → A(a, c), for all a, b, c ^{∈} A. The morphisms are equivalence classes of monotone functions, that is, morphisms f : A_{0} → B_{0} in Sh(Ω), that fulfil ⊢⊢ A(a, a′) → B(f(a), f(a′)). Two such morphisms, f, g : (A_{0}, A) → (B_{0}, B) are equivalent if and only if ⊢⊢ (A → B)(f, g) ∧ (B → A)(g, f). □

Here, the equality in the formula for reflexivity is the defined sheaf equality. Notice, that reflexivity as expressed in Definition 4.19 implies ⊢⊢ Ea → A(a, a), and that we already know, by properties of sheaves, that ⊢⊢ A(a, a) → Ea, so that we always have ⊢⊢ A(a, a) ↔ Ea.

We see that the global sections of an apo over Ω is an Ω-category. Thus, what we have done is to replace the set components of Ω-categories with sheaves and adjust the formulation of pre-orders accordingly. Further, we see that internally the enriched categories are nothing more than usual pre-orders in an ‘alternative’ universe. Therefore, in order to make Scott’s inverse limit theorem go through for apos all we have to do is to make his proof constructive!

We could have expressed Def. 4.19 more categorically, following [Mac Lane & Moerdijk 92], p. 199-200, where they define what an internal partial order is in a topos. We have already remarked that there is a one-to-one correspondence between morphisms from an object A of a topos into the sub-object classifier and sub-objects of A . Therefore we can identify our pre-order relation A from Def. 4.19 with a sub-object of A_{0} × A_{0} , say the monomorphism A : α → A_{0} × A_{0} . Reflexivity of A can then be expressed by requiring that the diagonal Δ_{A_{0}} : A_{0} → A_{0} × A_{0} which maps a to (a, a) factors through A as in the following diagram.

[figure: A_{0}; α; A_{0} × A_{0}; Δ_{A_{0}}; A]

To see how to express transitivity with a diagram, consider T obtained by the following pullback diagram.

[figure: α; A_{0} × A_{0}; A_{0}; T; α; A_{0} × A_{0}; v; u; A; π_{2}; A; π_{1}]

You can think of the elements of T as pairs, (((x, y), A(x, y)), ((y, z), A(y, z))), where commutativity of the above diagram causes the identification of the y’s across the pairs. Thus, transitivity can be expressed by requiring that ⟨π_{1} ∘ A ∘ v, π_{2} ∘ A ∘ u⟩ : T → A_{0} × A_{0} factors through A as in the following diagram.

[figure: T; α; A_{0} × A_{0}; ⟨π_{1} ∘ A ∘ v, π_{2} ∘ A ∘ u⟩; A]

Which presentation one prefers is naturally a matter of taste, although at the first glance, the diagram way of saying things seem rather complicated. However, diagrams have proven their value in terms of facilitating proofs on many occasions. For a good example of lots of nice proofs using categorical diagrams, see [Fourman 77].

We define products and function spaces for apos as expected.

Definition 4.20 Given apos A and B the sheaf part of the product A × B is the product (in Sh(Ω)) of the sheaf parts of the components, and the relation part A × B is defined as A × B((a, b), (a′, b′)) = A(a, a′) ∧ B(b, b′). □

Definition 4.21 Given apos A and B the sheaf part of the exponent [A → B] is the exponent (in Sh(Ω)) of the sheaf parts of the components, and the relation part [A → B] is defined as [A → B](f, g) = ∀a ^{∈} A_{0}. f(a) = g(a). □

We have used the internal logic of Sh(Ω) in our definitions in order to obtain a presentation just like the one from Ω_{⊗}-categories.

We can obtain an Ω_{⊗}-set from an Ω_{⊗}-category (when Ω_{⊗} is a cHa with ⊗ = ∧) by taking as the equality the ordering reflection (A^{∗}(a, a′) = A(a, a′) ∧ A(a′, a)), but this does not give us a sheaf. We then obtain a sheaf by sheafification. We carry the pre-order from the Ω_{⊗}-category over as a morphism on sheaves in the obvious way, since it has an internal representation in Ω_{⊗}-sets. Since the sheafification functor for Ω-sets is an equivalence of categories it preserves all small limits and colimits.

We can now carry over our previous definitions concerning forward Cauchy sequences and limsup convergence to be expressed internally in sheaves over Ω, that is, concerning the category APO(Ω). Since an apo is just a sheaf with a pre-ordering and sheaves are just intuitionistic sets we can see this as a natural generalization of domain theory from working on pre-ordered (or partially ordered sets) to an intuitionistic setting where we work with sheaves.

4.7 Limsup complete APOs

We now internalize and develop the concepts of convergence and completeness described in Section 3.4. One natural question to ask at the outset is why we cannot just take the usual definition of chain, chain completeness, and directed completeness, since we are just working with pre-orders anyway (internally in a topos). However, there are many ways to specify chain completeness and directed completeness, which are equivalent classically, but differ widely intuitionistically. Thus one definition of chain completeness amounts to Cauchy completeness when seen externally for a topos over [0, ∞]_{max} , and others do not. The fact that there is a definition that makes chain completeness and Cauchy completeness coincide just says that the theories concerning the two notions are not contradictory.

Whenever we have an observation or theorem etc. in the following, and we have formulated it internally, unless otherwise specified, it also holds in its external version, using just commutative, unital quantales.

Definition 4.22 We denote by ℕ the natural numbers sheaf. It is the sheafification of the presheaf that is constant with value {0, 1, …}. Such a sheaf is called a simple sheaf ([Troelstra & van Dalen 88] vol.II p.782). □

We also use ℕ for the associated apo with its ordering taken as the sheaf equality. We notice that ℕ is a discrete apo, in that ⊢⊢ ℕ(n, m) → n = m. A little confusing, but unavoidable we also use the usual ordering (written m ≤ n) on the natural numbers, which is of course different from this discrete apo ordering. The reason for not building the ordering on natural numbers into the apo structure of ℕ is that the requirement of monotonicity on functions would exclude too many functions. For instance, we would not be able to define (truncated) subtraction on natural numbers. For sequences α ^{∈} [ℕ → A] for a presheaf A, we will use the notation α_{n} for α(n).

Definition 4.23 A sequence α ^{∈} [ℕ → A] of elements of an apo A is forward Cauchy if

⊢⊢ ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. A(α_{n}, α_{m}) .

In this case we call N the Cauchy witness for α. □

In PreOrd the interpretation of the above is that there exists a natural number, the Cauchy witness N, such that the sequence starting from N is monotonically increasing. In GUlt we see that a sequence is forward Cauchy if for every ϵ > 0 there exists an N such that whenever m, n ≥ N then d(α_{n}, α_{m}) ≤ ϵ, that is, the sequence is Cauchy in the traditional metric sense. Notice that in this case the Cauchy witness N is local to ϵ. We remark, that for ultra-metric spaces ∀n ≥ N. A(α_{n}, α_{n+1}) implies ∀m ≥ n ≥ N. A(α_{n}, α_{m}) by the strong triangular inequality.

Definition 4.24 A sequence α ^{∈} [ℕ → A] in A converges to a ^{∈} A if

⊢⊢ ∃N ^{∈} ℕ. (∀m ≥ n ≥ N. A(α_{n}, α_{m})) ∧ (∀x ^{∈} A. [A(a, x) ↔ ∀n ≥ N. A(α_{n}, x)]) .

In this case we call a the (ω-)limsup of α, and write a = lim sup α. A morphism is (ω-limsup) continuous if it preserves forward Cauchy sequences and their (ω-)limsups. □

In PreOrd this translates to that a is the least upper bound for the sequence (α_{n})_{n≥N}, and in GUlt it means that the sequence is converging with limit a. As before, we have introduced the dependence on the Cauchy witness to avoid influence of the potentially ‘wild’ initial segment of the sequence.

Definition 4.25 An apo A is (ω-)limsup complete if every Cauchy sequence has a limsup. We write CAPO^{ω}(Ω) for the category of ω-limsup complete apos over Ω with (ω-limsup) continuous morphisms. □

We see that this is a common definition for being chain complete and metrically complete.

As before we generalize the notion of chain to that of a directed set, in order to be able to describe more notions of convergence.

Definition 4.26 We will call a non-empty apo D over Ω with a function ≤: D_{0} × D_{0} → Ω that fulfils ∀i, j ^{∈} D_{0}. ∃k ^{∈} D_{0}. i ≤ k ∧ j ≤ k a directed apo.

We borrow the following definitions almost verbatim from [Gierz et al. 80], p. 2. Only the definition of a directed net is substantially changed.

Definition 4.27 A net in an apo A over Ω is a morphism f ^{∈} [D → A] for some directed apo D. We will often write just D for the net, and leave the morphism as understood. When the net is understood, we will write a_{i} for f(i). If P (a) is a predicate on A then we say that P (a_{j}) holds eventually if ⊢⊢ ∃i_{0} ^{∈} D. ∀j ≥ i_{0}. P (a_{j}). A net is called directed if i ≤ j → A(a_{i}, a_{j}) holds eventually, and in this case i_{0} is called the witness for the directed net. □

Unconvoluting the last definition we see that a net is directed if ⊢⊢ ∃i_{0} ^{∈} D. ∀j ≥ i ≥ i_{0}. A(a_{i}, a_{j}).

It is now clear why we cannot let the ordering be built in. If we built it in then any mapping from a directed set would be monotone from the start, and a directed net would be a trivial concept.

Definition 4.28 A (directed) net D on A converges to a ^{∈} A if

⊢⊢ ∃i_{0} ^{∈} D. (∀j ≥ i ≥ i_{0}. A(a_{i}, a_{j})) ∧ (∀x ^{∈} A. [A(a, x) ↔ ∀j ≥ i_{0}. A(α_{j}, x)]) .

In this case we call a the limsup of α, and write a = lim sup α. □

Definition 4.29 An apo A is limsup complete if every directed net has a limsup. We write CAPO(Ω) for the category of limsup complete apos over Ω with (limsup) continuous morphisms. □

Notice, that we have a corresponding definition for Ω_{⊗}-categories. We have the following theorem.

Theorem 4.3 Every symmetric apo is directed complete. □

Proof : Let α = (a_{i})_{i^{∈}D} be a directed net in a symmetric apo (A_{0}, A). This means that ⊢⊢ ∃i_{0} ^{∈} D. ∀j ≥ i ≥ i_{0}. A(a_{i}, a_{j}) . We want to construct a limsup for α . We will look at the sheaf part A_{0} of A as a complete Ω-set (|A_{0}|, [ = ]) and sketch an internal proof. Define s : |A_{0}| → Ω as s(a) = ∃i_{0} ^{∈} D. ∀i ≥ i_{0}. A(a_{i}, a). It is easy to see that s is a singleton, so by completeness of A_{0} we can find a ^{∈} |A_{0}| such that [a = ] = s. With this definition it is not hard to show that a = lim sup α. □ Of course, this should not be surprising to us, since a symmetric pre-order is essentially discrete (Rosolini).

This gives us the following corollary.

Corollary 4.1 (Ω, ↔) is a directed complete apo over itself. □

The following theorem is obtained by easy applications of the logic in sheaves.

Theorem 4.4 For apos A and B, if B is (limsup/directed) complete, so is [A → B]. □

Proof : Given a forward Cauchy sequence F in [A → B] and an a ^{∈} A we write F (a) for the function that maps n ^{∈} ℕ into F_{n}(a).

It is immediate by the definition of [A → B] that the sequence F (a) is forward Cauchy for any a. Every such sequence has a limsup because B is complete. Define f to be the function that takes a ^{∈} A into lim sup F (a).

To see that f is monotone, we have to show ⊢⊢ A(a, a′) → B(f(a), f(a′)). By the definition of f we know that for any a ^{∈} A,

⊢⊢ ∃N ^{∈} ℕ. ∀b ^{∈} B. [B(f(a), b) ↔ ∀n ≥ N. B(F_{n}(a), b)] ,  (4.2)

and we have in general

⊢⊢ A(a, a′) → Ea ∧ Ea′ ∧ B(g(a), g(a′)),  (4.3)

for all g ^{∈} [A → B]. Using (4.2) with a = a′ and b = f(a′) we get

⊢⊢ ∃N ^{∈} ℕ. B(f(a′), f(a′)) ↔ ∀n ≥ N. B(F_{n}(a′), f(a′)).  (4.4)

Using (4.3) with g = f and g = F_{n} we then get

⊢⊢ A(a, a′) → ∃N ^{∈} ℕ. ∀n ≥ N. [B(F_{n}(a), F_{n}(a′)) ∧ B(F_{n}(a′), f(a′))] ,  (4.5)

that is, by transitivity and (4.2)

⊢⊢ A(a, a′) → B(f(a), f(a′)),  (4.6)

as desired. □

Definition 4.30 A function f : A → B is limsup continuous if it preserves limsups of directed nets. □

Remark 4.3 By monotonicity all morphisms of apos preserve forward Cauchy sequences and directed nets.

As an exercise we prove the following proposition, which will turn out to be useful later. It also illustrates an internal and an external proof.

Proposition 4.10 Any left-adjoint is limsup continuous.

Proof : Let f : D → E be left-adjoint to g : E → D. By being a left-adjoint we know that f preserves colimits, and as we indicated above we can characterize a limsup as a filtered colimit, thus avoiding the following technical details. For the sake of illustration, however, we stick to the details.

We will first reason internally, assuming that we are working in a category enriched over a cHa. Let α : J → D be a directed net with lim sup α = a. We will show that ϕ ∘ α is a directed net with lim sup f ∘α = f(a). We know that it is a directed net, say with index i_{0}, by Observation 4.3, so we have left to prove that ∀y ^{∈} E_{0}. [E(f(a), y) ↔ ∀i ≥ i_{0}. E(f(a_{i}), y)]. So let y ^{∈} E_{0} be given. The implication ‘→’ is easy. To see ‘←’ we assume ∀i ≥ i_{0}. E(f(a_{i}), y). Since g is a morphism that implies ∀i ≥ i_{0}. D(g ∘ f(a_{i}), g(y)), and since by adjointness D(d, g ∘ f(d)) for all d ^{∈} D_{0}, we have by transitivity ∀i ≥ i_{0}. D(a_{i}, g(y)). Since a = lim sup α we know that ∀i ≥ i_{0}. D(a_{i}, g(y)) implies D(a, g(y)), and thus, since f is a morphism, E(f(a), f ∘ g(y)). By adjointness we know E(f ∘ g(y), y), and so by transitivity E(f(a), y) as desired.

To see that the theorem also holds for general enriched categories over commutative unital quantales we have the following external proof. Of course, this proof suffices to prove the whole theorem. We want to show that ⋀_{i≥i_{0}} E(f(a_{i}), y)−• E(f(a), y) ≥ 1_{⊗}, that is, E(f(a), y) ≥ ⋀_{i≥i_{0}} E(f(a_{i}), y). We calculate

⋀_{i≥i_{0}} E(f(a_{i}), y) ≤ ⋀_{i≥i_{0}} D(g ∘ f(a_{i}), g(y))
≤ ⋀_{i≥i_{0}} D(a_{i}, g ∘ f(a_{i})) ⊗ D(g ∘ f(a_{i}), g(y))
≤ ⋀_{i≥i_{0}} D(a_{i}, g(y))
≤ E(f ∘ g(y), y),

where we get the second inequality by adjointness (D(a_{i}, g∘f(a_{i})) ≥ 1_{⊗}) and the last because a = lim sup α. □

Theorem 4.5 Composition on the right is continuous in APO(Ω).

Proof : Let (g_{n})_{n^{∈}ℕ} be a sequence in [B → C] with limsup g and let f ^{∈} [A → B]. We will show (lim sup_{n^{∈}ℕ} g_{n}) ∘ f = lim sup_{n^{∈}ℕ}(g_{n} ∘ f). That g_{n} converges to g means

⊢⊢ ∃N ^{∈} ℕ. ∀g′ ^{∈} [B → C]. [[B → C](g, g′) ↔ ∀n ≥ N. [B → C](g_{n}, g′)] ,  (4.7)

and we want to show

⊢⊢ ∃N ^{∈} ℕ. ∀h ^{∈} [A → C]. [[A → C](g ∘ f, h) ↔ ∀n ≥ N. [A → C](g_{n} ∘ f, h)] .  (4.8)

By definition of [A → C] this amounts to showing

⊢⊢ ∃N ^{∈} ℕ. ∀h ^{∈} [A → C]. [∀a ^{∈} A. [C(g(f(a)), h(a))] ↔ ∀n ≥ N. ∀a ^{∈} A. [C(g_{n}(f(a)), h(a))]] .

(4.9)

From (4.7), with g′ = g we have ⊢⊢ ∃N ^{∈} ℕ. ∀n ≥ N. [B → C](g_{n}, g), which expands to ⊢⊢ ∃N ^{∈} ℕ. ∀n ≥ N. ∀b ^{∈} B. C(g_{n}(b), g(b)). With b = f(a) this implies ⊢⊢ ∃N ^{∈} ℕ. ∀n ≥ N. ∀a ^{∈} A. [C(g_{n}(f(a)), g ∘ f(a))]. So if ⊢⊢ [A → C](g ∘ f, h), then by transitivity ⊢⊢ ∃N ^{∈} ℕ. ∀n ≥ N. ∀a ^{∈} A. [C(g_{n}(f(a)), h(a))].

The other way we want to show that ⊢⊢ ∀n ≥ N. ∀a ^{∈} A. [C(g_{n}(f(a)), h(a))] implies ⊢⊢ [A → C](g ∘ f, h). By expanding the latter expression and swapping the two universal quantifiers in the former, we see that it is enough to show that

⊢⊢ ∀n ≥ N. C(g_{n}(f(a)), h(a))  (4.10)

implies ⊢⊢ C(g(f(a)), h(a)) for all a ^{∈} A. Let g′ : B → C be the constant function with value h(a). Then (4.9) and (4.10) give that ⊢⊢ ∀b ^{∈} B. C(g(b), g′(b)), that is, ⊢⊢ ∀b ^{∈} B. C(g(b), h(a)), and with b = f(a) we have the desired result. □

Proposition 4.11 Composition to the left with a continuous function is continuous.

Proof : For g ^{∈} [B → C] continuous and (f_{n})_{n^{∈}ℕ} a convergent sequence in [A → B] with limsup f we have to prove that g ∘ lim sup_{n^{∈}ℕ} f_{n} = lim sup_{n^{∈}ℕ}(g ∘ f_{n}). This is trivial by the continuity of g. □

78

A General Inverse Limit Theorem

In this chapter we present a generalization of Scott’s inverse limit theorem, and sufficient conditions for when functors have fixed-points. In order for apos to be usable as models for recursive domain equations, the category APO(Ω) or suitable subcategories thereof must have feasible closure properties. The development follows essentially the pattern from [Scott 72] and [Smyth & Plotkin 82]. With our definitions of completeness etc. we will see that the old (patterns of) proofs still work.

Remark 5.1 It is also worth noticing that the development works for Ω_{⊗}-categories instead of apos if the internal statements are replaced with the obvious corresponding external statements. □

Definition 5.1 We will write [A ↪^{ϕ} ; ←_{ψ} B] for a retraction pair, that is, a pair of morphisms,

ϕ : [A → B] and ψ : [B → A], such that ψ ∘ ϕ = id_{A}. Here ϕ is called the embedding and ψ the projection. □

Definition 5.2 We denote by CAPO_{⇄}(Ω) the category of complete APOs with continuous retraction pairs between them. The morphisms go in the direction of the embedding. □

5.1 The inverse limit construction

We will now look at sequences of abstract pre-orders with mediating retraction pairs between

them. Let [D_{n} ↪^{ϕ_{n}} ; ←_{ψ_{n}} D_{n+1}]_{n^{∈}ℕ} be a sequence of apos and define τ_{nm} : [D_{n} → D_{m}] as follows.

τ_{nm}(a_{n}) = \{ \begin{matrix}ψ_{m} ∘ ψ_{m−1} ∘ … ∘ ψ_{n−1}(a_{n}) & if & n > m , \\ a_{n} & if & n = m , \\ ϕ_{m−1} ∘ ϕ_{m−2} ∘ … ∘ ϕ_{n}(a_{n}) & if & n < m . \end{matrix}

The following definition provides the unification of the conditions for when chains of complete pre-orders and chains of complete metric spaces have limits (in the suitable category). One essential obstacle that it overcomes is the apparent discrepancy between the locality of the pre-order condition and the globality of the metric condition.

Definition 5.3 The sequence [D_{n} ↪^{ϕ_{n}} ; ←_{ψ_{n}} D_{n+1}]_{n^{∈}ℕ} is forward Cauchy if

⊢⊢ ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. [D_{m} → D_{m}](τ_{nm} ∘ τ_{mn}, id_{D_{m}}) .  □

In PreOrd this means that from some N onward, ϕ_{n} ∘ ψ_{n} ≤ id_{D_{n+1}}, which is a local condition on each retraction pair, and in GUlt it means that d(ϕ_{n} ∘ ψ_{n}, id_{D_{n+1}}) converges to 0, a global condition on the chain.

Note that we can express the forward Cauchy condition equivalently as an associative law (or triangle inequality if you wish) as follows.

⊢⊢ ∃N ^{∈} ℕ. ∀m, n, k ≥ N. [D_{m} → D_{n}](τ_{kn} ∘ τ_{mk}, τ_{mn}) .

Here the tensor is composition. A nice reading of the above is that beyond N, approximation is transitive: if τ_{mk} is a witness that D_{m} approximates D_{k} and if τ_{kn} is a witness that D_{k} approximates D_{n}, then τ_{kn} ∘ τ_{mk} is a witness that D_{m} approximates D_{n}. Of course, approximation is reflexive, so since the space of retracts between two domains form a Cartesian closed category it should be possible to streamline the formulation.

The name ‘forward Cauchy’ is not chosen arbitrarily. Consider the Ω_{⊗}-category with the set part being the set of domains in the chain, i.e. D_{n} for n ^{∈} ℕ, and the hom from the object D_{n} to D_{m} as [D_{m} → D_{m}](τ_{nm} ∘ τ_{mn}, id_{D_{m}}). Then the predicate forward Cauchy takes its usual meaning, except that we cannot see the index set, ℕ, as an object of the category.

Within the framework of apos that we have built, we have proven the following general version of Scott’s inverse limit theorem; its specializations to pre-ordered sets and metric spaces are already well known (see for instance [Scott 72], [Smyth & Plotkin 82] and [America & Rutten 87]).

Theorem 5.1 Any forward Cauchy sequence of capos with continuous retraction pairs has a limit in CAPO_{⇄}(Ω).

For the proof we start out by constructing an inverse limit of the projection part of the sequence. Of course, this inverse limit is in the category CAPO(Ω) and not in CAPO_{⇄}(Ω). The construction follows the path known from the special cases.

Define the abstract pre-order D with functions Φ_{n} : D_{n} → D and Ψ_{n} : D → D_{n} as follows. D is the inverse limit sheaf of the projection part of the sequence. It is section wise the set of sequences (a_{n})_{n^{∈}ℕ} where a_{n} ^{∈} D_{n} and a_{n} = ψ_{n}(a_{n+1}) for all n ^{∈} ℕ. The pre-ordering D(\overline{a}, \overline{b}) is ∀n ^{∈} ℕ. D_{n}(Ψ_{n}(\overline{a}), Ψ_{n}(\overline{b})), where we define Ψ_{n}(\overline{a}) = a_{n}.

We could be worried that also chains of domains might be ‘wild’ in the start, and thus conjecture that it would make better sense to define D(\overline{a}, \overline{b}) as ∃N ^{∈} ℕ. ∀n ≥ N. D_{n}(Ψ_{n}(\overline{a}), Ψ_{n}(\overline{b})), but it makes no difference due to the following observation.

Observation 5.1 The sequence (D_{n}(x_{n}, y_{n}))_{n^{∈}ℕ} is decreasing in Ω.

Proof : Since x_{n} = ψ_{n}(x_{n+1}) and likewise for \overline{y}, and ψ_{n} is a morphism for every n we have D_{n+1}(x_{n+1}, y_{n+1}) ≤ D_{n}(x_{n}, y_{n}). □ Therefore we get the following corollary.

Corollary 5.1 For \overline{x}, \overline{y} ^{∈} D , if 1_{⊗} ≤ ⋁_{n^{∈}ℕ} ⋀_{m≥n} D_{m}(x_{m}, y_{m}) then 1_{⊗} ≤ ⋀_{n^{∈}ℕ} D_{n}(x_{n}, y_{n}) .

□

The proof that D is the object part of the limit we were looking for is mostly a simpleminded generalization of the special cases, containing no surprises. We will alternate freely between external and internal reasoning. Lemma 5.1 D is an apo.

Proof : We must show D(\overline{a}, \overline{b}) ⊗ D(\overline{b}, \overline{c}) ≤ D(\overline{a}, \overline{c}).We calculate

D(\overline{a}, \overline{b}) ⊗ D(\overline{b}, \overline{c}) = ⋀_{n^{∈}ℕ}D_{n}(Ψ_{n}(\overline{a}), Ψ_{n}(\overline{b})) ⊗ ⋀_{n^{∈}ℕ}D_{n}(Ψ_{n}(\overline{b}), Ψ_{n}(\overline{c}))
≤ ⋀_{n^{∈}ℕ}(D_{n}(Ψ_{n}(\overline{a}), Ψ_{n}(\overline{b})) ⊗ D_{n}(Ψ_{n}(\overline{b}), Ψ_{n}(\overline{c})))
≤ ⋀_{n^{∈}ℕ}D_{n}(Ψ_{n}(\overline{a}), Ψ_{n}(\overline{c}))
= D(\overline{a}, \overline{c}) ,
□

Lemma 5.2 Ψ_{n} is monotone for every n.

Proof : This is immediate from the definition of D(\overline{a}, \overline{b}). □ Lemma 5.3 D is complete.

Proof : Let (\overline{x}^{i})_{i^{∈}I} be a directed net in D with witness i_{0}. This means that ⊢⊢ ∃i_{0} ^{∈} I. ∀j ≥ i ≥ i_{0}. D(\overline{x}^{i}, \overline{x}^{j}), in particular

⊢⊢ ∀k ^{∈} ℕ. ∃i_{0} ^{∈} I. ∀j ≥ i ≥ i_{0}. D_{i}(\overline{x}_{k}^{i}, \overline{x}_{k}^{j}) ,

so (\overline{x}_{k}^{i})_{i^{∈}I} is a directed net in D_{k}. By completeness of D_{k} there is a limsup x_{k} = lim sup_{i^{∈}I} \overline{x}_{k}^{i}. We have that x_{k} = ψ_{k}(x_{k+1}), that is, lim sup_{i^{∈}I} \overline{x}_{k}^{i} = ψ_{k}(lim sup_{i^{∈}I} \overline{x}_{k+1}^{i}). This follows from continuity of ψ_{k} because ψ_{k}(lim sup_{i^{∈}I} \overline{x}_{k+1}^{i}) = lim sup_{i^{∈}I} ψ_{k}(\overline{x}_{k+1}^{i}) = lim sup_{i^{∈}I} \overline{x}_{k}^{i} = x_{k}. □ Lemma 5.4 Ψ_{n} is continuous.

Proof : Easy. □ Lemma 5.5 For every other cone (D′, (Ψ_{n})_{n^{∈}ℕ}) in CAPO(Ω) over the diagram (D_{n}, ψ_{n})_{n^{∈}ℕ} there exists a unique morphism Ψ : D′ → D such that the following diagram commutes for every n ^{∈} ℕ, that is, (D, (Ψ_{n})_{n^{∈}ℕ}) is a limit for (D_{n}, ψ_{n})_{n^{∈}ℕ} .

[figure: D′; D; D_{n}; Ψ′_{n}; Ψ_{n}; Ψ]

Proof : Define Ψ(a) = ⟨Ψ′_{0}(a), Ψ′_{1}(a), …⟩. Now the definition of D and the fact that every Ψ′_{n} is monotone together imply that D′(a, b) ≤ D(⟨Ψ′_{0}(a), Ψ′_{1}(a), …⟩ , ⟨Ψ′_{0}(b), Ψ′_{1}(b), …⟩). The uniqueness of Ψ is by the definition of Ψ_{n} as the n’th element. □

After having dealt with the projections we include the embeddings. We use the initiality of (D, (Ψ_{n})_{n^{∈}ℕ}), on the following diagram for any n ^{∈} ℕ.

[figure: D_{0}; D_{1}; D_{2}; ⋯; D_{n}; ψ_{0}; ψ_{1}; τ_{n0}; τ_{n1}; τ_{n2}]  (5.1)

Thereby we get unique existence of Φ_{n} : D_{n} → D such that the following diagram commutes for all n ^{∈} ℕ.

[figure: D_{n}; D_{m}; D; τ_{nm}; Φ_{n}; Ψ_{m}]  (5.2)

Lemma 5.6 For all n ^{∈} ℕ, the pair (Φ_{n}, Ψ_{n}) is a retraction pair.

Proof : By diagram 5.2, Ψ_{n} ∘ Φ_{m} = τ_{nm}, and thus we get the result when n = m. □

Lemma 5.7 For all n ^{∈} ℕ the following three diagrams commute.

[figure: (1); D_{n}; D; D_{n+1}; Φ_{n}; Ψ_{n+1}; ϕ_{n}; (2); D_{n}; D; D_{n+1}; Ψ_{n}; Φ_{n+1}; ψ_{n}; (3); D_{n}; D; D_{n+1}; Φ_{n}; Φ_{n+1}; ϕ_{n}]

Proof : (1) Let m = n + 1 in diagram 5.2. (2) Let n = n + 1 and m = n in diagram 5.2.

(3) By uniqueness of a function Φ′_{n} : D_{n} → D such that diagram 5.2 commutes for m = n+1 we get Ψ_{n+1} ∘ Φ_{n+1} ∘ ϕ_{n} = ϕ_{n} = Ψ_{n+1} ∘ Φ_{n}. □

Lemma 5.8 Φ_{n} is continuous.

Proof : Let α be forward Cauchy with index N in D_{n} with limsup a . Assume without loss of generality that n ≤ N (otherwise take N′ = max{n, N} and continue with N′ instead of N ). Since τ_{nN} is continuous τ_{nN} ∘α is forward Cauchy with limsup τ_{nN}(a) . By Lemma 5.7 (3) we have Φ_{n}(a) = Φ_{N}(τ_{nN}(a)) . We know that Φ_{n} preserves forward Cauchy sequences, as any morphism does, and thus that Φ_{n} ∘ α is forward Cauchy, say with limsup x. It is easy to see that ⊢⊢ D(x, Φ_{n}(a)) since ⊢⊢ ∀m ^{∈} ℕ. D_{n}(α_{m}, a) . We will show that ⊢⊢ D(Φ_{n}(a), x) .

By continuity of Ψ_{N} we have lim sup_{n}(Ψ_{N} ∘ Φ_{n} ∘ α) = Ψ_{N}(x) . However, Ψ_{N} ∘ Φ_{n} ∘ α = τ_{nN} ∘α , so Ψ_{N}(x) = lim sup_{n} Ψ_{N} ∘Φ_{n} ∘α = lim sup_{n} τ_{nN} ∘α = τ_{nN}(a) . Thus, Φ_{N} ∘Ψ_{N}(x) = Φ_{N} ∘ τ_{nN}(a) = Φ_{n}(a) , but we know ⊢⊢ D(Φ_{N} ∘ Ψ_{N}(x), x), so ⊢⊢ D(Φ_{n}(a), x) as desired. □

We have now established the existence of the following commuting diagram in CAPO_{⇄}(Ω), where h_{n} = (ϕ_{n}, ψ_{n}) and H_{n} = (Φ_{n}, Ψ_{n}).

[figure: D_{0}; D_{1}; D_{2}; ⋯; D; h_{0}; h_{1}; H_{0}; H_{1}; H_{2}]

We will show that (D, (H_{n})_{n^{∈}ℕ}) is a limit of the sequence of D_{n}’s with the mediating retraction pairs.

Lemma 5.9 Given r : D → D , if (1) ⊢⊢ ∀n ^{∈} ℕ. [D → D](Φ_{n} ∘ Ψ_{n}, r) then (2) ⊢⊢ [D → D](id_{D}, r) .

Proof : To show (2) amounts to showing for any m ^{∈} ℕ that ⊢⊢ [D → D_{m}](Ψ_{m}, Ψ_{m} ∘ r) . By specialization of (1) with n = m we have ⊢⊢ [D → D](Φ_{m} ∘ Ψ_{m}, r) and thus ⊢⊢ [D → D_{m}](Ψ_{m} ∘ Φ_{n} ∘ Ψ_{m}, Ψ_{m} ∘ r) which is ⊢⊢ [D → D_{m}](Ψ_{m}, Ψ_{m} ∘ r) as desired. □

Corollary 5.2 Given r : D → D and N ^{∈} ℕ , if ⊢⊢ ∀n ≥ N. [D → D](Φ_{n} ∘ Ψ_{n}, r) then ⊢⊢ [D → D](id_{D}, r) .

Proof : By Lemma 5.9 and Corollary 5.1. □

Lemma 5.10 For f, g ^{∈} [D → D] we have

[D → D](f, g) = ⋀_{n^{∈}ℕ}[D → D_{n}](Ψ_{n} ∘ f, Ψ_{n} ∘ g) .

Proof :

[D → D](f, g) = ⋀_{\overline{x}^{∈}D} ⋀_{n^{∈}ℕ}D_{n}(f(\overline{x})_{n}, g(\overline{x})_{n})
= ⋀_{n^{∈}ℕ} ⋀_{\overline{x}^{∈}D} D_{n}(f(\overline{x})_{n}, g(\overline{x})_{n})
= ⋀_{n^{∈}ℕ}[D → D_{n}](Ψ_{n} ∘ f, Ψ_{n} ∘ g)
□

Lemma 5.11 Given r : D → D , if (1) ⊢⊢ [D → D](id_{D}, r) then (2) ⊢⊢ ∀n ^{∈} ℕ. [D → D](Φ_{n} ∘ Ψ_{n}, r).

Proof :

[D → D](Φ_{n} ∘ Ψ_{n}, id_{D}) = ⋀_{m^{∈}ℕ}[D → D_{m}](Ψ_{m} ∘ Φ_{n} ∘ Ψ_{n}, Ψ_{m})
= ⋀_{m^{∈}ℕ}[D → D_{m}](τ_{nm} ∘ Ψ_{n}, Ψ_{m})
= ⋀_{m^{∈}ℕ}[D → D_{m}](τ_{nm} ∘ τ_{mn} ∘ Ψ_{m}, Ψ_{m})
≥ ⋀_{m^{∈}ℕ}[D_{m} → D_{m}](τ_{nm} ∘ τ_{mn}, id_{D_{m}})

Here the first equality is by Lemma 5.10. □

Corollary 5.3 id_{D} = lim sup Φ_{n} ∘ Ψ_{n} .

Proof : By Corollary 5.2 and Lemma 5.11. □ Lemma 5.12 For any other cone (D′, (H′_{n})_{n^{∈}ℕ}) over (D_{n}, h_{n})_{n^{∈}ℕ} with H′_{n} = (Φ′_{n}, Ψ′_{n}) the sequence (Φ′_{n} ∘ Ψ_{n})_{n^{∈}ℕ} is Cauchy.

Proof : We know ⊢⊢ ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. [D_{m} → D_{m}](τ_{nm} ∘τ_{mn}, id_{D_{m}}), but we also have

[D_{m} → D_{m}](τ_{nm} ∘ τ_{mn}, id_{D_{m}}) ≤ [D → D_{m}](τ_{nm} ∘ τ_{mn} ∘ Ψ_{m}, Ψ_{m})
= [D → D_{m}](τ_{nm} ∘ Ψ_{n}, Ψ_{m})
≤ [D → D′](Φ′_{m} ∘ τ_{nm} ∘ Ψ_{n}, Φ′_{m} ∘ Ψ_{m})
= [D → D′](Φ′_{n} ∘ Ψ_{n}, Φ′_{m} ∘ Ψ_{m}).

□

[D → D′] is complete because D′ is, and we define Φ = lim sup_{n^{∈}ℕ} Φ′_{n} ∘ Ψ_{n}. It is not too hard to see that Φ is limsup continuous itself. Thanks to Jan Rutten for pointing out the necessity of this (5.14). Lemma 5.13 Ψ ∘ Φ = id_{D}.

Proof : Ψ ∘ Φ = Ψ ∘ lim sup_{n^{∈}ℕ}(Φ′_{n} ∘ Ψ_{n}) = lim sup_{n^{∈}ℕ}(Ψ ∘ Φ′_{n} ∘ Ψ_{n}). Therefore we have for all m ^{∈} ℕ and all a ^{∈} D that

Ψ_{m} ∘ Ψ ∘ Φ = Ψ_{m} ∘ lim sup_{n^{∈}ℕ}(Ψ ∘ Φ′_{n} ∘ Ψ_{n})
= lim sup_{n^{∈}ℕ}(Ψ_{m} ∘ Ψ ∘ Φ′_{n} ∘ Ψ_{n})
= lim sup_{n^{∈}ℕ}(Ψ′_{m} ∘ Φ′_{n} ∘ Ψ_{n})
= lim sup_{n^{∈}ℕ}(τ_{nm} ∘ Ψ′_{n} ∘ Φ′_{n} ∘ Ψ_{n})
= lim sup_{n^{∈}ℕ}(τ_{nm} ∘ Ψ_{n})
= lim sup_{n^{∈}ℕ}Ψ_{m}
= Ψ_{m}.
□

Lemma 5.14 Φ is unique such that Φ ∘ Φ_{n} = Φ′_{n} for all n ^{∈} ℕ

Proof : From Corollary 5.3 we know that Φ = Φ ∘ lim sup_{n^{∈}ℕ}(Φ_{n} ∘ Ψ_{n}), and by continuity of composition we get Φ = lim sup_{n^{∈}ℕ}(Φ ∘ Φ_{n} ∘ Ψ_{n}) = lim sup_{n^{∈}ℕ}(Φ′_{n} ∘ Ψ_{n}). □

We have now proven theorem 5.1.

5.2 Fixed-points of functors

Concerning fixed-points of functors we note that the category CAPO_{⇄}(Ω) does not in general have an initial object. This means that there is not always a canonical way to let a functor start off generating a chain of domains with mediating retraction pairs. We also know from the metric setting that we sometimes get fixed-points, but not unique or canonical fixedpoints. We will see how much we can achieve in the general setting.

Definition 5.4 An endo-functor on CAPO_{⇄}(Ω) is continuous if it preserves Cauchy chains and their limits. □

Proposition 5.1 Both [ → ] and [ × ] are continuous in both their arguments.

Proof : Standard. □ It is also standard to extend this definition to functors that take several arguments and

to define (local) continuity analogously for functors of the type CAPO(Ω)^{n} → CAPO(Ω) that are covariant in some and contravariant in other arguments. Further one can show that such functors, when viewed as endo-functors on CAPO_{⇄}(Ω), are continuous. For all of this one can mimic e.g. [Plotkin 83].

The general fixed-point theorem looks like this.

Theorem 5.2 Given a continuous endo-functor F on CAPO(Ω), consider the corresponding endo-functor (which we will also call F) on CAPO_{⇄}(Ω) and a global section ϕ of F 1l. If the

chain C = [F^{n}1l ↪^{F^{n}ϕ} ; ←_{F^{n}E} F^{n+1}1l]_{n^{∈}ℕ} is Cauchy, then its limit is a fixed-point of F.

Proof : First remember that a global section of F 1l is just a mapping ϕ from 1l to F 1l, so

that we are able to start the chain with [1l ↪^{ϕ} ; \overleftarrow{E} F 1l]. We denote the unique morphism into 1l by

E because of its similarity to the extent operation. Let [F^{n}1l ↪^{Φ_{n}} ; ←_{Ψ_{n}} D]_{n^{∈}ℕ} be the limiting cone

for C. Since F preserves (retracts and) Cauchy chains and their limits, [F^{n+1}1l ↪^{F Φ_{n}} ; ←_{F Ψ_{n}} F D]_{n^{∈}ℕ}

is a limiting cone as well. Its limit object is isomorphic to D, since the chain is the same, except that we have excluded the first element. □

We will briefly go through what this theorem translates to in our example categories. In PreOrd, if we just have ϕ : [1l → F 1l] with ϕ ∘ E ≤ id_{F1l} and F is continuous, then we fulfil the criteria for Thm. 5.2. To see this, notice first that E∘ϕ = id1l by necessity, so we do have

a retraction [1l ↪^{ϕ} ; \overleftarrow{E} F 1l]. Then remember that the Cauchy condition for pre-orders reduces to

F^{n}ϕ∘F^{n}E ≤ id_{F^{n+1}1l} for all n ^{∈} ℕ, and that this condition is fulfilled for n = 0 and preserved by F. We see here a glimpse of the role of the unique bottom element in CPOs. It makes the choice of ϕ unique, by the requirement ϕ ∘ E ≤ id_{F1l}. On the other hand, this requirement implies the existence of a unique least element of F 1l up to isomorphism.

In GMet the (corresponding external) criterion is met if we have a contracting functor, i.e. one for which there exists ϵ < 1 such that ϵ · d(ϕ, ψ) ≥_{ℝ} d(F ϕ, F ψ) for every pair of morphisms ϕ and ψ with the same domain and codomain. We can then just choose any global section of F 1l, and we get a Cauchy sequence as desired.

In GUlt the above requirement can be relaxed because of the strong triangular inequality. It turns out to be enough that F is such that d(F^{n}ϕ, F^{n}ψ) converges to 0 for n → ∞ for all ψ and ψ.

We also notice that a very trivial but important way to fulfill the requirement is that there be an isomorphism between F^{n}1l and F^{n+1}1l for some n ^{∈} ℕ. This is for instance the case in GMet or GUlt if we have F (X) = X × ℕ with n = 1. We all know bijective codings of ℕ × ℕ into ℕ. To establish the Cauchy sequence we just need that ℕ be a discrete metric space, and we need to choose ϕ_{0}(∗) from 1l × ℕ. The solution (the fixed-point up to isomorphism of F) is then all finite sequences of natural numbers, coded into the first element of the list. This is also a good example of the importance of the mediating morphisms. If we had just chosen them to be the naive projections/embeddings into a product, then the sequence of domains that we obtain is not Cauchy. It does, however, have a limit/colimit, the set of countably infinite lists of natural numbers, and this limit is a fixed-point up to isomorphism of F!

Powers of APOs

As the power-set PA of an enriched category A we follow [Lawvere 73] and take it to be the function space [A−• (Ω_{⊗}, −•)]. Given p : A−• B between Ω_{⊗}-categories we have a corresponding ϕ_{p} : B−• (Ω_{⊗}, −•) defined as ϕ_{p}(b) = ⋁_{a^{∈}A_{0}} B(p(a), b). We notice, that since ϕ_{p} is a morphism (which is easy to see), we have B(b, b′) ≤ ϕ(b)−• ϕ(b′) and thus by adjointness B(b, b′) ⊗ ϕ(b) ≤ ϕ(b′), the (asymmetric) extensionality property we would want of a subset.

Consider further the following diagram.

[figure: B; A; (Ω_{⊗}, −•); 1l; p; ϕ_{p}; ⊤]

For which monos p is the above diagram a pullback? If 1_{⊗} = ⊤ the diagram commutes, since 1_{⊗} ≤ B(p(a), p(a)) for all a ^{∈} A_{0}. Assume the situation

[figure: B; A; (Ω_{⊗}, −•); 1l; p; ϕ_{p}; ⊤; A′; p′; ?]

and let a′ ^{∈} A_{0}. Since ϕ_{p}(p′(a)) = 1_{⊗} we know 1_{⊗} = ⋁_{a^{∈}A_{0}} B(p(a), p′(a′)), so if p(A) is closed in the sense that 1_{⊗} = ⋁_{b^{∈}p(A)} B(b, b′) implies b′ ^{∈} p(A), we have the desired pullback. Thus (Ω_{⊗}, −•) classifies the closed subsets if 1_{⊗} = ⊤.

We will spend a little time investigating notions of ‘set membership’ based on the preorder instead of the sheaf equality. Naturally even the symmetric closure of such a membership predicate will be weaker than the sheaf notion, since elements can be equivalent under the pre-order without being identical.

Based on the pre-order we can define non-symmetric notions of ‘membership’ as follows.

Definition 6.1 For an APO A we define the relations ^{∈}^{l},^{∈}^{r}: A × PA → Ω as follows.

(i) ⊢⊢ a ^{∈}^{l} X ↔ ∃x ^{∈} X. A(a, x),

(ii) ⊢⊢ a ^{∈}^{r} X ↔ ∃x ^{∈} X. A(x, a). □

We will write A(a, X) for a ^{∈}^{l} X and A(X, a) for a ^{∈}^{r} X. We can introduce a symmetric membership in two ways, one of which is based on the previous definitions (6.1).

Definition 6.2 For an APO A we define the relations ^{∈}_{1},^{∈}_{2}: A × PA → Ω as follows.

(i) ⊢⊢ a ^{∈}_{1} X ↔ ∃x ^{∈} X. A(x, a) ∧ A(a, x),

(ii) ⊢⊢ a ^{∈}_{2} X ↔ A(a, X) ∧ A(X, a). □

We will use the notation A^{∗}(a, X) for a ^{∈}_{2} X. It is easy to see that of the two symmetric notions of membership the first one is the stronger one, and that they are equivalent for convex X, where we define convex as follows.

Definition 6.3 A subset X ^{∈} PA is convex if

⊢⊢ ∀a ^{∈} A. ∀x, x′ ^{∈} X. [A(x′, a) ∧ A(a, x) → a ^{∈} X]

Here we have used the ‘real’ set membership in the definition. Notice, that X is convex if and only if ⊢⊢ ∀a ^{∈} A. [A^{∗}(a, X) → a ^{∈} X]. Could we introduce a notion of ⊗-convexity?

Lemma 6.1 For any subset X of an APO A, the function from A to (Ω, ↔) that maps a into A(a, X) ∧ A(X, a), is monotone.

Proof : Holds in general for any sup or inf of an extensional predicate. (D. Scott) □ It is a common conception (e.g. [Edalat & Smyth 92], [Adámek 93]) that the class of

compact subsets is the interesting one from a computational viewpoint when one considers power-sets. The best way to formulate compactness constructively is to say that a compact subset is one that is totally bounded and complete ([Bishop & Bridges 85], p. 95). We have already defined completeness. Total boundedness is naturally formulated as follows.

Definition 6.4 A subset X of A is totally bounded if

⊢⊢ ∃N ^{∈} ℕ. ∃a_{1}, …, a_{N} ^{∈} A. ∀x ^{∈} X. ∃n ≤ N. A(x, a_{n}) .  □

It is trivial to formalize the ‘…’s. In PreOrd total boundedness means that the pre-order has a finite set of elements containing as a subset all the maximal elements, and in GMet and GUlt it means that for any ϵ > 0 we can find a finite set of points such that the ϵ-disks around those points cover the whole space. The requirement to find a particular finite set of points is what sets this notion apart from the (classically equivalent) notion of boundedness, where we only require that there exists an upper bound to the distance between any two points.

Naturally we can dualize the notion of total boundedness using A(a_{n}, x) instead of A(x, a_{n}), and then a pre-order is totally bounded if it has a finite number of minimal elements.

Definition 6.5 An apo is compact if it is totally bounded and complete. We write P_{c}A for the set of compact subsets of A. □

It is clear how to define the pre-order on P_{c}A, since Hausdorff distance and Egli-Milner ordering coincide in our framework. See also the remarks of Smyth in [Smyth 89] on a generalized power domain. The definition also corresponds precisely to the equality in power sheaves in the sense that the pre-ordering between power apos depends on the pre-order on the initial set in the same manner as equality between power sheaves depends on equality on the initial set.

Definition 6.6 For an apo A and X, Y ^{∈} P_{c}A we define ⊢⊢ [P_{c}A](X, Y) ↔ ∀x ^{∈} X. A(x, Y)∧ ∀y ^{∈} Y. A(X, y). □

We can in fact use the same definition (with PA instead of P_{c}A) to give PA an APO structure.

As a first step towards showing that P_{c}A is complete (if this is true), we show the following theorem.

Theorem 6.1 Let (D_{n})_{n^{∈}ℕ} be a Cauchy sequence in P_{c}A, with a limit D in PA. Then D is totally bounded.

Proof : We know

⊢⊢ ∃N ^{∈} ℕ. ∀m ≥ n ≥ N. [P_{c}A](D_{n}, D_{m}),  (6.1)
⊢⊢ ∃N ^{∈} ℕ. ∀X ^{∈} P_{c}A. [[P_{c}A](D, X) ↔ ∀n ≥ N. [P_{c}A](D_{n}, X)] ,  (6.2)
⊢⊢ ∃N ^{∈} ℕ, a_{1}, …, a_{n} ^{∈} A. ∀x ^{∈} D_{m}. ∃n ≤ N. A(x, a_{n}) for all m,  (6.3)

and we will show

⊢⊢ ∃N′ ^{∈} ℕ, a′_{1}, …, a′_{N′} ^{∈} A. ∀x ^{∈} D. ∃n ≤ N′. A(x, a′_{n}).  (6.4)

Use (6.1) to get N_{1} that witnesses (6.1) (locally). Use (6.2) to get N_{2}, and (6.1) gives us

⊢⊢ ∃N_{3} ^{∈} ℕ. ∀m ≥ max{N_{1}, N_{2}, N_{3}} ≥ N_{3}. [P_{c}A](D_{max{N_{1},N_{2},N_{3}}}, D_{m}).  (6.5)

Let K = max{N_{1}, N_{2}, N_{3}}. Now, D_{K} is totally bounded, so we get N and a_{1}, …, a_{N} ^{∈} A such that

⊢⊢ ∀x ^{∈} D_{K}. ∃n ≤ N. A(x, a_{n}).  (6.6)

Take X as D_{K} in (6.2). Since by (6.5) ⊢⊢ ∀n ≥ K. [P_{c}A](D_{k}, D_{n}), we get ⊢⊢ [P_{c}A](D, D_{K}), implying by definition

⊢⊢ ∀x ^{∈} D. ∃a ^{∈} D_{K}. A(x, a).  (6.7)

But by transitivity, using the a from (6.7) as x in (6.6) we get

⊢⊢ ∀x ^{∈} D. ∃n ≤ N. A(x, a_{n}).  (6.8)

as desired. □

It is interesting to compare this proof to the one that comes natural in the special case of metric spaces. Here one would use an \frac{ϵ}{2}–argument, finding an index N above which the sets are within \frac{ϵ}{2} of each other, and in D_{N} then K_{N} points such that disks with diameter \frac{ϵ}{2} with these points as centers cover D_{N}. Then ϵ–disks around the same points will cover the limit. In the sheaf argument the splitting of ϵ that seemed crucial in the metric case has apparently disappeared.

We should also show that the traditional notion of limit of subsets ([Hahn 32]), viz. that (D_{n})_{n^{∈}ℕ} is convergent with limit D if and only if

⋃_{n^{∈}ℕ} ⋂_{m≥n} \overline{D_{m}} = ⋂_{n^{∈}ℕ} ⋃_{m≥n} \overline{D_{m}} = D

coincides with our general notion of limit of a Cauchy sequence. Here the notion of Cauchy sequence is clear, given the Egli-Milner/Hausdorff ordering, and the closure, \overline{X} of an APO X ⊆ A is naturally expressed (D. Scott) as \overline{X} = \{x ^{∈} A|A(x, D)\}. Due to the lack of symmetry we have a ‘dual’ closure, where we use A(D, x) instead. In PreOrd we get up or down closure, and in GMet and GUlt we get the metric closure.

It is also possible to connect to the categorical notion of finiteness (compactness) as can be seen by the following definition and proposition.

Definition 6.7 An element e of an apo A is finite if for every directed net α : D → A with A(e, lim α) we have ⊢⊢ ∃i ^{∈} D. A(e, α(i)). □

Proposition 6.1 An element e of an apo A is finite if and only if the representable A(e, ) is continuous.

Proof : That A(e, ) is continuous means that for every directed net α : D → A the morphism A(e, ) ∘ α is a directed net in Ω and that A(e, lim α) = lim_{i^{∈}D} A(e, α(i)). But internally lim_{i^{∈}D} A(e, α(i)) is ∃i ^{∈} D. A(e, α(i)), so all we have to show is that for every directed α : D → A and finite e it holds that

(∃i ^{∈} D. A(e, α(i))) → A(e, lim α) ,

but this follows straightforwardly from the definitions of limit and directed net. □

Remark 6.1 This means that we can introduce algebraicity as for complete partial orders by saying that an apo is algebraic if every representable is the limit of a directed net of continuous representables. We can then go on an define continuous apos as the retracts of the algebraic ones etc.

We have not yet explored what these notions imply for generalized ultra-metric spaces, or their external versions for generalized metric spaces. Following a comment from Kock, it should be possible to connect the notion of compactness of apos just given with this categorical notion of finiteness.

Conclusion

We have achieved a unification of pre-orders and metric spaces as models for recursive domain equations, but it is our hope that this thesis will be seen more as showing a natural link from a choice of logic (the logic of approximations) to a category for domain equations. More specifically we have given a recipe for how to go from an Ω_{⊗}, a commutative unital quantale, to a suitable category for domains over the logic of Ω_{⊗}, namely the category of colimsup complete Ω_{⊗}-categories with colimsup continuous morphisms. In this category Scott’s inverse limit theorem holds, and we have given sufficient conditions for when functors have fixed-points in this setting. The conditions generalize those already known from partial order semantics and metric semantics.

Concerning connections to other work than what we have referred to extensively in the body of this thesis we wish to mention the following.

Smyth ([Smyth 87], [Smyth 88], and [Smyth 92]) has found a common ground for preorder and metric semantics by combining the order properties and the distance properties in quasi-metric spaces. These spaces are precisely the [0, ∞]_{+}-categories with the extra requirement of symmetric separatedness, i.e. ⊢⊢_{Sh([0,∞]_{max})} d(x, y) ∧ d(y, x) → (x = y). His nice results are in this light not surprising. The generalization to quasi-uniformities that he develops would be an interesting candidate for a generalization along the lines of enriched categories, and an analysis of his work using the suitable logic, viz. the logic of [0, ∞]_{+} should also be interesting.

Flagg and Kopperman have also worked towards a unification of metric spaces and domains for semantics (see for instance [Flagg & Kopperman 93], [Flagg & Kopperman 93b], and [Flagg & Kopperman 94]). They have, independently from the theory of enriched categories, developed a closely related concept. Their continuity spaces are categories enriched over what they call value quantales. A value quantale is almost like a commutative unital quantale, but with an additional property that makes an analogue to contraction in metric spaces easy to formulate. They pursue a topological rather than categorical line. A combination should be fruitful, and especially their concept of actions on a quantale might be developed in a logical direction, to better characterize when functors have fixed-points.

In his thesis, [Lehmann 78], Lehmann shows how ordinary categories fulfilling some simple conditions (such as a categorical version of chain completeness, being skeletal, and being large) can be subjected to the same constructions as in Scott’s inverse limit theorem. The fact that this approach is possible seems promising to the desire to generalize the approach in this thesis to general enriched categories.

In his forthcoming thesis, Fiore ([Fiore 93]) considers CPO-enriched categories, and even the o-category approach from [Smyth & Plotkin 82] considers structures ‘enriched’ over poset structures. This seems to be a second layer, where the apos form a first layer. In other words, one should be able to consider also GMet and GUlt, and in general APO(Ω_{⊗}) or rather CAPO(Ω_{⊗}) enriched categories. The process of iterating the enrichment operation (functor) is described for instance in [Casley et al. 93]. One possible path towards ‘repeating’ the process of ‘enrichment’ (which is more than enrichment, since we restrict the objects to the colimsup complete ones, and the morphisms to the colimsup continuous ones), in case it does not generalize to all enriched categories, might be found in the theory of quantaloids ([Rosenthal 92]). A quantaloid is a category enriched over the category of sup-lattices, that is, a locally small category such that the hom set between any two objects is a complete lattice, and such that composition of the morphisms preserve suprema in both variables. The structure of quantales lifts nicely to quantaloids, and for instance the category of bimodules over a quantaloid is again a quantaloid.

Ultra-metric spaces play a central role in p-adic analysis (see e.g. [Schikhof 84]), and by observing that they are just (separated) sheaves over a particular cHa, one should think that a nice logical angle to constructive p-adic analysis has been opened. If one wants it computable, then of course, one can work within the realizability topos.

Barnsley ([Barnsley 88]) showed how recursive equations over metric spaces naturally model fractals. He thereby provided one of the most convincing arguments that metric spaces can do something useful that partial orders cannot, when it comes to semantics. (For another example see the work by Reed and Roscoe on the modelling of real time concurrency in [Reed 90] and [Reed & Roscoe 88].) By indicating how the metric (and the ultra-metric) approaches fit in the same scheme as the partial order approach, and by indicating the possibilities for a whole range of structures in between (Smyth’s quasi-metric spaces being just one example), perhaps other interesting applications can arise.

Concerning future work in direct continuation of this thesis, a first comment must be that there certainly seems to be enough. During the course of writing the thesis we have repeatedly had to be very conservative when deciding whether to pursue an interesting digression from the main line of thought, just in order to stay within reasonable space and time bounds. Among the most tempting avenues of further exploration, one could think of redoing in the enriched setting many of the domain constructions from traditional domain theory, such as for instance consistently complete algebraic cpos, continuous lattices, bidomains, stable functions and so on. Also the notion of powerdomain seems to be generalizable, and perhaps the general notion of compactness suggested in this thesis can be used in that connection. There are also numerous connections to topology to investigate, and Smyth’s work could be an obvious guideline, for instance to various notions of completions. As mentioned before, the generalization from metric spaces to uniformities should have an enriched version, which would then provide a new logical angle to uniformities.

Along another line it would be interesting to study spaces over radically different quantales than 2 and [0, ∞]_{+}, that is, not just over for instance their product (where we would get a notion of convergence and completeness pointwise in each coordinate). Examples are hard to come by, but [Rosenthal 90] seems to be a good source. Connections to linear logic should be helpful here, and perhaps a study of semantics over particular Ω_{⊗} can also help pin down interesting classes of Ω_{⊗} for linear logic (where of course the Girard quantales (see e.g. [Rosenthal 90]) are already one class. Much work lies ahead in carrying out an internalization for apos over general commutative unital quantales as it has already been done in this thesis for apos over complete Heyting algebras. More generally one should study the connection between the algebraic properties of Ω_{⊗} and the logical properties of APO(Ω_{⊗}).

Finally, a generalization to bicategories as we have already mentioned would incorporate sheaves directly into the same framework as pre-orders and metric spaces. Walters has already studied Cauchy completeness for sheaves, but colimsup completeness could perhaps also be interesting.

94

Bibliography

[Adámek 93] Adámek, J., Private communication, talk in Prague, April 15, 1993.

[Ambler 92] Ambler, S.J., First order linear logic in symmetric monoidal closed categories, D. Phil thesis, Edinburgh University, CST-87-92 and ECS-LFCS-92-194, 1992.

[America & Rutten 87] America, P., J.J.M.M. Rutten, Solving reflexive domain equations in a category of complete metric spaces, Centrum voor Wiskunde en Informatica, Centre for Mathematics and Computer Science, Report CS-R8709, February 1987. Also appeared in Journal of Computer and System Sciences, 39(3):343-375, 1989.

[Apt & Plotkin 81] Apt, K.R., G.D. Plotkin, A cooks tour of countable nondeterminism, Proceedings of the 8’th ICALP, pp. 479-494, eds.: Even & Kariv, Lecture Notes in Computer Science, vol. 115, Springer Verlag 1981.

[Arnold & Nivat 80] Arnold, A., M. Nivat, The metric space of infinite trees. Algebraic and topological properties, Fundamenta Informaticae III, 4 (1980), pp. 445-476.

[de Bakker & Zucker 82] de Bakker, J.W., J.I. Zucker, Processes and the denotational semantics of concurrency, in Information and Control 54, 70-120, 1982.

[de Bakker & Zucker 82b] de Bakker, J.W., J.I. Zucker, Denotational semantics of concurrency, in proceedings of the 14’th ACM Symposium: Theory of Computing, 1982.

[Barnsley 88] Barnsley, M., Fractals Everywhere, Academic Press, 1988.

[Barr 80] Barr, M., ∗-autonomous categories, Springer Lecture Notes in Mathematics vol. 752, 1980.

[Bénabou 67] Bénabou, J., Introduction to bicategories, Reports of the Midwest Category Seminar, I, vol. 47, Springer Lecture Notes in Mathematics, 1967.

[Bishop & Bridges 85] Bishop, E., D. Bridges, Constructive Analysis, Grundlehren der mathematischen Wissenschaften, vol. 279, Springer-Verlag, 1985.

[Blute 93] Blute, R.F., Linear topology, Hopf algebras and ∗-autonomous categories, Preprint obtained via anonymous ftp from triples.math.mcgill.ca, McGill University, May 21, 1993.

[Borceux & Dejean 86] Borceux, F., D. Dejean, Cauchy completion in category theory, Cahiers de Topologie et Géométrie Différentielle Catégoriques, vol. XXVII-2 (1986).

[Borceux & van den Bossche 91] Borceux, F., G. van den Bossche, A generic sheaf representation for rings, Proceedings of Category Theory, Como 1990, pp. 30-42, eds.: Carboni, Pedicchio, Rosolini, Springer-Verlag, 1991.

[Bourbaki 89] Bourbaki, N., Elements of Mathematics, General Topology, Springer Verlag 1989.

[Carboni & Street 86] Carboni, A., R. Street, Order ideals in categories, Pacific Journal of Mathematics, vol. 124, No. 2, pp. 275-288, 1986.

[Carboni & Walters 85] Carboni, A., R.F.C. Walters, Cartesian bicategories I, Journal of Pure and Applied Algebra 49 (1987), pp. 11-32.

[Cartwright 85] Cartwright, R., Types as intervals, Conference Record of the 12’th Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, January 1985.

[Casley 91] Casley, R.T., On the specification of concurrent systems, Ph.D. Thesis, Department of Computer Science, Stanford University, 1991.

[Casley et al. 93] Casley, R., R.F. Crew, J. Meseguer, V. Pratt, Temporal structures, Revision of article in Mathematical Structures in Computer Science, 1(2):179 – 213, July 1991. Available by anonymous ftp from boole@cs.stanford.edu.

[Davey & Priestley 90] Davey, B.A., H.A. Priestley, Introduction to Lattices and Order, Cambridge University Press, 1990.

[Dugundji 66] Dugundji, J., Topology, Wm.C. Brown Publishers, 1989. (Also Allyn & Bacon 1966.)

[Edalat & Smyth 92] Edalat, A., M.B. Smyth, Compact metric information systems (extended abstract), Imperial College, 1992.

[Eilenberg & Kelly 66] Eilenberg, S., G.M. Kelly, Closed categories, Proceedings of La Jolla Conference on Categorical Algebra, Springer Verlag 1966.

[Fiore 93] Fiore, M.P., private communication (draft thesis), 1993.

[Flagg & Kopperman 93] Flagg, B., R. Kopperman, The asymmetric topology of computer science, Proceedings of MFPS-IX (sorry, no more information available now).

[Flagg & Kopperman 93b] Flagg, B., R. Kopperman, Tychonoff poset structures and auxiliary relations. Topology SumConf 9 (SRU, 6/93) (as above).

[Flagg & Kopperman 94] Flagg, B., R. Kopperman, Continuity spaces: reconciling domains and metric spaces, Copies of slides for MFPS-X, 1994.

[Fourman 74] Fourman, M., Connections between category theory and logic, D.Phil Thesis, Linacre College, Oxford University, 1974.

[Fourman 77] Fourman, M., The logic of topoi, in Handbook of Mathematical Logic (ed. Barwise), pp. 1053-1090, North-Holland, 1977.

[Fourman & Scott 77] Fourman, M., D.S. Scott, Sheaves and logic, in proceedings Durham 1977, Applications of Sheaves, Lecture Notes in Mathematics, vol. 753, eds.: Fourman, Mulvey, Scott. Springer Verlag, 1979.

[Freyd 91] Freyd, P., Algebraically complete categories, in Category Theory, Proceedings of Category Theory, Como 1990, pp. 95-104, eds.: Carboni, Pedicchio, Rosolini, Springer-Verlag, 1991.

[Freyd 92] Freyd, P., Remarks on algebraically compact categories, in Applications of Categories in Computer Science, pp. 95-106, eds.: Fourman, Johnstone, Pitts, LMS Lecture Note Series 177, Cambridge University Press 1992.

[Gierz et al. 80] Gierz, G., K.H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, D.S. Scott, A Compendium of Continuous Lattices, Springer-Verlag, 1980.

[Girard 87] Girard, J.Y., Linear logic, Theoretical Computer Science, 50:1-102 (1987).

[Gunter 92] Gunter, C.A., Semantics of Programming Languages, The MIT Press, 1992.

[Hahn 32] Hahn, H., Reelle Funktionen, erster Teil, Punktfunktionen, Akademische Verlagsgeschellschaft MBH., Leipzig, 1932 (republished by Chelsea Publ. Company, New York, 1948).

[Johnstone 77] Johnstone, P.T., Topos Theory, L.M.S. Monographs, vol. 10, Academic Press, 1977.

[Johnstone 82] Johnstone, P.T., Stone Spaces, Cambridge Studies in Advanced Mathematics, vol. 3, Cambridge University Press, 1982.

[Kelly 82] Kelly, F.A.A., Basic Concepts of Enriched Category Theory, London Mathematical Society Lecture Notes Series, vol. 64, Cambridge University Press, 1982.

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

[Lawvere 73] Lawvere, F.W., Metric spaces, generalized logic, and closed categories, Rend. Semi. Mat. Fis. Milano, vol. 43, pp. 135-166, 1974.

[Lehmann 78] Lehmann, D.J., Categories for fixpoint semantics, D.Phil. Thesis, Department of Computer Science, University of Warwick, 1978.

[Mac Lane 71] Mac Lane, S., Categories for the Working Mathematician, Springer-Verlag, 1971.

[Mac Lane & Moerdijk 92] Mac Lane, S., I. Moerdijk, Sheaves in Geometry and Logic, Springer-Verlag, 1992.

[MacQueen et al. 84] MacQueen, D., G. Plotkin, R. Sethi, An ideal model for recursive polymorphic types, Conference Record of the 11’th Annual ACM Symposium on Principles of Programming Languages, Salt Lake City, Utah, January 1984. (extended version)

[Nawaz 85] Nawaz, M., Quantales: Quantal Sets, D. Phil thesis, Unniversity of Sussex, September 1985.

[Nivat 79] Nivat, M., Infinite words, infinite trees, infiite computations, Foundations of Computer Science III, 2, pp. 3-52, eds.: de Bakker & Van Leeuwen, Mathematical Centre Tracts 109, 1979.

[Pitts 93] ,Pitts, A.M., Relational properties of recursively defined domains, Cambridge 1993.

[van der Plancke 93] van der Plancke, Frédéric, Deux remarques sur les ensembles à valeurs dans un quantale non nécessairement bilatère, Master thesis, Université Catholique de Louvain, Institut de Mathématique Pure et Appliquée, August 1993.

[Plotkin 76] Plotkin, G., A powerdomain construction, SIAM J. Computing 5, 1976.

[Plotkin 83] Plotkin, G., Domains, Department of Computer Science, University of Edinburgh, 1983.

[Reed 90] Reed, G.M., A hierarchy of domains for real-time distributed computing, Proceedings of the 5’th International Conference on the Mathematical Foundations of Programming Semantics, Tulane, March/April 1989, Lecture Notes in Computer Science, Vol. 442, Springer Verlag, 1990.

[Reed & Roscoe 88] Reed, G.M., A.W. Roscoe, Metric spaces as models for real-time concurrency, Proceedings of the 3’rd Workshop on the Mathematical Foundations of Programming Language Semantics, Tulane, April 1987, Lecture Notes in Computer Science, Vol. 298, Springer Verlag, 1988.

[Rosenthal 90] Rosenthal, K.I., Quantales and Their Applications, Pitman Research Notes in Mathematics Series, Vol. 234, Longman Scientific & Technical, 1990.

[Rosenthal 92] Rosenthal, K.I., Girard quantaloids, Mathematical Structures in Computer Science (1992), vol. 2, pp. 93-108.

[Rosolini 80] Rosolini, G., Internal properties of structures in toposes, Master Thesis, Merton College, Oxford University, Sept. 1980.

[Rowlands-Hughes 87] Rowlands-Hughes, D.M., Domains versus metric spaces, M.Sc. Thesis, Imperial College of Science and Technology, Spetember 1987.

[Schikhof 84] Schikhof, W., Ultrametric Calculus : an introduction to p-adic analysis, Cambridge studies in advanced mathematics series; 4, Cambridge University Press, 1984.

[Scott 69] Scott, D.S., Models for The Lambda Calculus, Manuscript, 1969, (unpublished).

[Scott 70a] Scott, D.S., Outline of a mathematical theory of computation, Oxford University Technical Monograph PRG-2, November 1970.

[Scott & Strachey 71] Scott, D.S., C. Strachey, Toward a mathematical semantics for computer languages, Oxford University Technical Monograph PRG-6, August 1971.

[Scott 72] Scott, D.S., Continuous lattices, in Lawvere: Toposes, Algebraic Geometry and Logic, Lecture Notes in Mathematics 274, Springer-Verlag, Berlin 1972.

[Scott 76] Scott, D.S., Data types as lattices, SIAM Journal on Computing, Vol. 5, 1976, pp. 522-587.

[Scott 77] Scott, D.S., Identity and existence in intuitionistic logic, in proccedings, Durham 1977, Applications of Sheaves, Lecture Notes in Mathematics, vol. 753, eds.: Fourman, Mulvey, Scott. Springer Verlag 1977.

[Scott 93] Scott, D.S., A type-theoretical alternative to ISWIM, CUCH, OWHY, Theoretical Computer Science, vol. 121 (1993), pp. 411-440 (originating from 1969).

[Smyth 78] Smyth, M.B., Power domains, Journal of Computer and System Sciences, vol. 16, pp. 23-36, 1978.

[Smyth 87] Smyth, M.B., Completeness of quasi-uniform spaces in terms of filters, To appear (slightly revised) in Journal of London Mathematical Society.

[Smyth 88] Smyth, M.B., Quasi-uniformities: reconciling domains with metric spaces, Proceedings of the 3’rd Workshop on the Mathematical Foundations of Programming Language Semantics, Tulane, April 1987, Lecture Notes in Computer Science, Vol. 298, Springer Verlag, 1988.

[Smyth 89] Smyth, M.B., Totally bounded spaces and compact ordered spaces as domains of computation, in Proceedings of the Oxford Symposium in Topology and its Applications, June 1989.

[Smyth 92] Smyth, M.B., Completeness of quasi-uniformities and syntopological spaces, Journal of London Mathematical Society, 1992, to appear.

[Smyth & Plotkin 82] Smyth, M.B., G.D. Plotkin, The category theoretic solution of recursive domain equations, SIAM Journal of Computing, Vol. 11, No. 4, Nov. 1992.

[Street 76] Street, R., Limits indexed by category-valued 2-functors, Journal of Pure and Applied Algebra 8 (1976), pp. 149-181.

[Taylor 86] Taylor, P., Recursive domains, indexed category theory and polymorphism, D.Phil. thesis, University of Cambridge, 1986.

[Troelstra & van Dalen 88] Troelstra, A.S., D. van Dalen, Constructivism in Mathematics - An Introduction, vol. I, II, Studies in Logic and the Foundations of Mathematics, vol. 121, North Holland 1988.

[Walters 81] Walters, R.F.C., Sheaves and Cauchy-complete categories, Cahiers de Topologie et Geometrie Differentielle 22-3 (1981).

[Walters 82] Walters, R.F.C., Sheaves on sites as Cauchy-complete categories, Journal of Pure and Applied Algebra 24 (1982) 95-102.

[Willard 70] Willard, S., General Topology, Addison Wesley 1970.

[Wyler 91] Wyler, O., Lecture Notes on Topoi and Quasitopoi, World Scientific 1991.