TYPES

AND STRUCTURES

An Introduction to Category Theory for the working computer scientist

Andrea Asperti

Giuseppe Longo

I

INTRODUCTION

The main methodological connection between programming language theory and category theory is

the fact that both theories are essentially ’theories of functions.“ A crucial point, though, is that the

categorical notion of morphism generalizes the set-theoretical description of function in a very broad

sense, which provides a unified understanding of various aspects of the theory of programs. This is

one of the reasons for the increasing role of category theory in the semantic investigation of programs

if compared, say, to the set-theoretic approach. However, the influence of this mathematical

discipline on computer science goes beyond the methodological issue, as the categorical approach to

mathematical formalization seems to be suitable for focusing concerns in many different areas of

computer science, such as software engineering and artificial intelligence, as well as automata theory

and other theoretical aspects of computation.

This book is mostly inspired by this specific methodological connection and its applications to the

theory of programming languages. More precisely, as expressed by the subtitle, it aims at a self-

contained introduction to general category theory (part I) and at a categorical understanding of the

mathematical structures that constituted, in the last twenty or so years, the theoretical background of

relevant areas of language design (part II). The impact on functional programming, for example, of

the mathematical tools described in part II, is well known, as it ranges from the early dialects of Lisp,

to Edinburgh ML, to the current work in polymorphisms and modularity. Recent applications, such

as CAML, which will be described, use categorical formalization for the purposes of implementation.

In addition to its direct relevance to theoretical knowledge and current applications, category theory

is often used as an (implicit) mathematical jargon rather than for its explicit notions and results.

Indeed, category theory may prove useful in construction of a sound, unifying mathematical

environment, one of the purposes of theoretical investigation. As we have all probably experienced, it

is good to know in which ’category“ one is working, i.e., which are the acceptable morphisms and

constructions, and the language of categories may provide a powerful standardization of methods and

language. In other words, many different formalisms and structures may be proposed for what is

essentially the same concept; the categorical language and approach may simplify through abstraction,

display the generality of concepts, and help to formulate uniform definitions. This has been the case,

for example, in the early applications of category theory to algebraic geometry.

The first part of this book should encourage even the reader with no specific interest in

programming language theory to acquire at least some familiarity with the categorical way of looking

at formal descriptions. The explicit use of deeper facts is a further step, which becomes easier with

access to this information. Part II and some chapters in part I are meant to take this further step, at

II

least in one of the possible directions, namely the mathematical semantics of data types and programs

as objects and morphisms of categories.

We were urged to write the general introduction contained in part I, since most available books in

category theory are written for the ’working mathematician“ and, as the subject is greatly indebted to

algebraic geometry and related disciplines, the examples and motivations can be understood only by

readers with some acquaintance with nontrivial facts in algebra or geometry. For most computer

scientists, it is not much help in the understanding of ’natural transformations“ to see an involved

example based on tensor products in categories of sheaves. Thus our examples will be based on

elementary mathematical notions, such as the definition of monoid, group, or topological space, say,

and on structures familiar for readers with some acquaintance with the tools in programming language

semantics. In particular, partial orders and the various categories of domains for denotational

semantics will often be mentioned or introduced, as well as basic results from computability theory.

For example, we will try to present the fundamental operation of ’currying“ for cartesian closed

categories with reference to the connection between the universal function and the g del- numbering

of the partial recursive functions. Partial morphisms will be presented as a generalization of a

common notion in theory of computation.

Category theory may be presented in a very abstract way: as a pure game of arrows and diagrams.

It is useful to reach the point where acquaintance with the formal (essentially, equational) approach is

so firm that it makes sense independently of any ’structural“ understanding. In this book, though, we

will stress the role of structures, and we will always try to give an independent meaning to abstract

notions and results. Each definition and fact will be exemplified, or even derived, from applications

or structures in some way indebted to computing. However, in order to stress the role of the purely

equational view, the last chapters of each part (essentially chapters 7 and 11) will be largely based on

a formal, computational approach. Indeed, even if mathematically very abstract, the equational

arguments turn out to be particularly relevant from a computer science perspective.

The early versions of this book grew out of two graduate courses taught by Longo in Pisa, in

1984/85, and at Carnegie Mellon University, in 1987/88. Then the book was entirely revised under

the influence of Asperti•s work for his Ph.D. dissertation. In particular, chapters 7 and 11, the

technically most difficult, are part of his dissertation.

We are indebted to several people. The joint work with Simone Martini and Eugenio Moggi in

several papers directly influenced many chapters. Moreover, Eugenio suggested, in handwritten notes

and electronic mail messages, the basic ideas for the categorical understanding of polymorphism via

internal categories and realizability toposes. Their mathematical insights and suggestions also

influenced other parts of the book.

We must acknowledge the influence on our approach of the ideas and work of Dana Scott and

Gordon Plotkin, who also encouraged us and made comments on early drafts. Pino Rosolini helped

III

us with comments and many suggestions. Jean Yves Girard and Yves Lafont brought to our attention

the tidy categorical meaning of linear logic and its applications to computing. Roberto Amadio and

many students helped us by detecting errors and incompleteness in the presentation. We are looking

forward to aknowledge the readers who will detect the remaining errors.

The first draft of this book was completed while the authors were visiting Carnegie Mellon

University, in 1987/88. Longo would like to thank the Computer Science Dept. of CMU for its very

generous hospitality while he was teaching there that academic year. The circulation of the draft, its

complete revision, and the writing of the final version of the book have been made possible by the

Joint Collaboration Contract ST2J-0374-C (EDB) of the European Economic Community and by the

Italian CNR "Stanford-grant" #89.00002.26. The authors would like to thank INRIA, Rocquencourt,

for a postdoc granted to Asperti while completing this work and l•Ecole Normale SupŽrieure, Paris,

for inviting Longo to teach a graduate course in 1989/90 based partly on this book.

IV

TABLE OF CONTENTS

PART I: Categories and Structures

CATEGORIES ......................................................................................1

1.1 Category: Definition and Examples..................................................1

1.2 Diagrams................................................................................3

1.3 Categories out of Categories .........................................................4

1.4 Monic, Epic, and Principal Morphisms ............................................5

1.5 Subobjects .............................................................................8

CONSTRUCTIONS.............................................................................. 10

2.1 Initial and Terminal Objects ........................................................ 10

2.2 Products and Coproducts........................................................... 12

2.3 Exponentials.......................................................................... 15

2.4 Examples of CCC•s ................................................................. 20

2.4.1 Scott Domains ............................................................ 20

2.4.2 Coherent Domains........................................................ 24

2.5 Equalizers and Pullbacks ........................................................... 27

2.6 Partial Morphisms and Complete Objects........................................ 31

2.7 Subobject Classifiers and Topoi ................................................... 35

FUNCTORS AND NATURAL TRANSFORMATIONS ................................... 40

3.1 Functors .............................................................................. 40

3.2 Natural Transformations............................................................ 45

3.3 Cartesian and Cartesian Closed Categories Revisited ........................... 51

3.4 More Examples of CCC•s .......................................................... 54

3.4.1 Partial Equivalence Relations ........................................... 54

3.4.2 Limit and Filter Spaces .................................................. 55

3.5 Yoneda's Lemma .................................................................... 58

3.6 Presheaves............................................................................ 60

CATEGORIES DERIVED FROM FUNCTORS AND

NATURAL TRANSFORMATIONS........................................................... 63

4.1 Algebras Derived from Functors................................................... 63

V

4.2 From monoids to monads .......................................................... 67

4.3 Monoidal and monoidal closed categories ........................................ 72

4.4 Monoidal Categories and Linear Logic............................................ 79

UNIVERSAL ARROWS AND ADJUNCTIONS ............................................ 88

5.1 Universal arrows .................................................................... 89

5.2 From Universal Arrows toward Adjunctions .................................... 93

5.3 Adjunctions........................................................................... 97

5.4 Adjunctions and Monads ..........................................................104

5.5 More on Linear Logic ..............................................................110

CONES AND LIMITS ..........................................................................120

6.1 Limits and Colimits.................................................................120

6.2 Some Constructions Revisited ....................................................123

6.3 Existence of limits ..................................................................125

6.4 Preservation and Creation of Limits..............................................127

6.5 w-limits ..............................................................................130

INDEXED AND INTERNAL CATEGORIES...............................................132

7.1 Indexed Categories .................................................................132

7.2 Internal Category Theory ..........................................................136

7.3 Internal Presheaves.................................................................143

7.4 Externalization ......................................................................150

7.5 Internalization .......................................................................156

Appendix .................................................................................158

PART II: Types as Objects

FORMULAE, TYPES, AND OBJECTS .....................................................166

8.1 l-Notation...........................................................................167

8.2 The Typed l-Calculus with Explicit Pairs (lbhpt) ............................168

8.3 The Intuitionistic Calculus of Sequents ..........................................171

8.4 The Cut-Elimination Theorem.....................................................176

8.5 Categorical Semantics of Derivations ............................................185

8.6 The Cut-Elimination Theorem Revisited .........................................187

8.7 Categorical Semantics of the Simply Typed Lambda Calculus................191

8.8 Fixpoint Operators and CCCs.....................................................197

VI

REFLEXIVE OBJECTS AND

THE TYPE-FREE LAMBDA CALCULUS..................................................204

9.1 Combinatory Logic.................................................................206

9.2 From Categories to Functionally Complete Applicative Structures ...........208

9.3 Categorical Semantics of the l-Calculus.........................................214

9.4 The Categorical Abstract Machine ................................................217

9.5 From Applicative Structures to Categories ......................................220

9.6 Typed and Applicative Structures: Applications and Examples ...............225

Part 1: Provable isomorphisms of types .....................................226

Part 2: Higher type objects as models of the type-free l-calculus .........234

RECURSIVE DOMAIN EQUATIONS.......................................................241

10.1 The Problem of Contravariant Functors........................................242

10.2 0-Categories .......................................................................245

SECOND ORDER LAMBDA CALCULUS..................................................251

11.1 Syntax ..............................................................................252

11.2 The External Model ...............................................................254

11.3 The External Interpretation.......................................................257

11.4 The Internal Model................................................................258

11.5 The Internal Interpretation........................................................261

11.6 Relating Models ...................................................................263

EXAMPLES OF INTERNAL MODELS .....................................................272

12.1 Provable Retractions..............................................................272

12.2 PER inside w -Set..................................................................275

12.3 PL-Categories Inside Their Groethendiek Completion .......................277

BIBLIOGRAPHY ...............................................................................283

VII

1. Categories

Chapter 1

CATEGORIES

Category Theory studies ’objects“ and ’morphisms“ between them. These concepts are both

primitive in Category Theory: objects are not collections of ’elements,“ and morphisms do not need

to be functions between sets (thus morphisms cannot be applied to ’elements“ but only composed

with other morphisms). Any immediate access to the internal structure of objects is prevented: all

properties of objects must be specified by properties of morphisms (existence of particular

morphisms, their unicity, validity of some equations among them, and so on). This is quite similar to

considering objects as ’abstract data types,“ that is, data specifications that are independent of any

particular implementation. The relevance of Category Theory for programming languages comes

from the previous consideration: it offers a highly formalized language especially suited for stating

abstract properties of structures. Thus, it relates to widely used programming methodologies and

provides as well a formal setting for the mathematical investigation of the semantics of programming

languages.

1.1 Category: Definition and Examples

As we have mentioned, Category Theory is a theory of functions, and the only basic operation is

composition. The concept of Category embodies some abstract properties of the composition

operator ’»“ for functions that ’reasonably“ must be guaranteed. In particular, if g: a®b and h:

b®c, then there exist h » g: a®c; moreover, composition must be associative and an identity must

exist for all objects.

This is the formal definition:

1.1.1 Definition A category C is

- a collection ObC of objects, denoted by a, b . . . A, B . . .

- a collection MorC of morphisms (arrows), denoted by f, g . . . ,

- two operations dom, cod assigning to each arrow f two objects respectively called domain

(source) and codomain (target) of f

- an operation id assigning to each object b a morphism idb (the identity of b) such that

dom(idb) = cod(idb) = b

- an operation ’ » “ (composition) assigning to each pair f, g of arrows with dom(f) = cod(g) an

arrow f » g such that dom( f » g ) = dom(g), cod( f » g ) = cod(f)

- identity and composition, moreover, must satisfy the following conditions:

1

1. Categories

identity law: for any arrows f, g such that cod(f) = b = dom(g)

idb » f = f

g » idb = g

associative law: for any arrows f, g, h such that dom(f) = cod(g) and dom(g) = cod(h)

(f»g)»h=f»(g»h)

We write f: a ® b to denote a morphism whose source and target are respectively a and b. Given

two objects a and b, the collection of all morphisms f such that f: a ® b is denoted by C[a,b]; the

writing fÎC[a,b] is thus a third way to express the fact that dom(f) = a, and cod(f) = b. For the

moment we shall use one notation or the other indifferently

The following table lists some common categories by specifying their objects and arrows, letting

the definition of their operators as an exercise for the reader:

Category Objects Morphisms

Set sets functions

Top topological spaces continuous functions

Vect vector spaces linear transformations

Grp groups group homomorphisms

PO partially ordered sets monotone functions

The intuition of the notion of ’category“ suggested by the previous examples is to consider the

objects as a collection of ’structured“ sets and the morphisms as the ’associated“ or ’acceptable“

functions with respect to the structure. This is too restrictive, though, since no requirement is made in

the definition which may force the morphisms to be ’single valued“ or to be functions in extenso: a

simple example is the category Rel with sets as objects and relations as morphisms.

The simplest category has only one object and one arrow (the identity for that object): this

category is usually called 1. Note that, by definition, if C is a category, then every object b of C

has an identity idb: b®b. The identity is unique, since if idb' is another identity for b, then for

the identity law, idb' = idb ° idb' = idb . A category is called discrete if every arrow is the identity

of some object: in this case a category is fully determined by the collection of its objects. 1 is a

discrete category.

A category is called a preorder if for every pair of objects a, b there is at most one morphism

f: a®b. The reason for the name is that a preorder category is fully determined by a preordering

relation among its objects. Indeed, in a preorder C, there is only one way that composition may be

defined; thus C is known when the collection of morphisms MorC and the operations dom and cod

are known. But every arrow f: a®b may be identified with the pair (a,b), since once the source and

2

1. Categories

target are known there is no choice about what the arrow is to be; thus, all the information about the

category C is given by the relation RC = {(a,b) / there is an arrow fÎC[a,b]}, that is, by a preorder

relation.(Exercise: prove that the relation RC is a preorder for every category C ).

Every discrete category is a preorder. The simplest nondiscrete category which is a preorder is

the category 2, which has two objects, let us call them 0 and 1, and three arrows: the two identities

id0 , id1 and an arrow (0,1): 0®1. In a similar way we can define for each natural number n a

preorder category n, from the usual ordering on the set {0,1, . . . n-1}. Preorder categories have a

common property: they may have plenty of objects, but given two objects, there exists at most one

morphism between them.

A dual situation is given by monoids, viewed as categories. A monoid is a set having an

associative binary operation and an identity element. A category with just one object yields a monoid,

where composition of morphisms is the binary operation. Conversely, any monoid (A, . ) is a

category with just one object. For example, the category with the set of natural numbers as unique

object and the recursive functions as morphisms yields the monoid of the recursive functions.

As well as preorders, another example where objects are not necessarily understood as

’structured sets“ is given by deductive systems as categories. In these categories propositions are

objects and each morphism f : a®b corresponds to (a suitable equivalence class of) a proof of a |-

b (a entails b). Observe that a category is obtained easily in the presence of the identical entailment

ia : a®a and the associative composition of proofs

f : a®b g : b®c

________________

g ° f : a®c

This approach to deduction is very relevant in the categorical understanding of logics of a

constructive nature, such as Intuitionistic Logic, where the intended interpretation of proofs is given

by (effective) operations. It will be the main paradigm for understanding the relation between types

and objects investigated in the second part of this book.

1.2 Diagrams

An important tool in the practice of Category Theory is the use of diagrams for representing

equations. In a diagram a morphism fÎC[a,b] is drawn as an arrow from a to b labeled f. A diagram

commutes if the composition of the morphism along any path between two fixed objects is equal.

For example, the associative and identity laws of the definition of ’category“ may be nicely visualized

by the following commuting diagrams:

3

1. Categories

Diagrams are a typical way, in Category Theory, to describe equational reasoning and turn out to

be particularly effective when dealing with several equations at a time. In particular, assertions such

as ’if diagram 1 and . . . diagram n commute, then diagram commutes“ express conditional

statements about equalities.

We hope that the reader, while using this book, will acquire some familiarity with diagrams and

will learn how to go back and forth from diagrams to equations. Our extended use of equations in

this book comes from our desire to stress the ’computational“ nature of most categorical reasoning.

1.3 Categories out of Categories

A main feature of Category Theory is the facility to define new, more structured categories out of

simpler ones. In this section we consider only a few simple constructions; a number of other

examples occur throughout the book.

1.3.1 Definition A category D is a subcategory of a category C, if

1. ObD Í ObC;

2. for all a, b in ObD, D[a,b] Í C[a,b];

3. composition and identities in D coincide with those of C.

A subcategory is full if for all a, b in ObD D[a,b] = C[a,b].

A full subcategory is fully determined by its collection of objects.

1.3.2 Definition The dual category C op of a category C has the same objects and the same

morphisms of C, idopb = idb, domop(f) = cod(f), codop(f) = dom(f), and f °op g = g ° f.

Note that Cop[b,a] = C[a,b] and (Cop)op = C.

Exercise Setop is a subcategory of Rel, but not of Set. Is it a full subcategory?

Duality is a very powerful technique of Category Theory. If P is a generic proposition expressed

in the language of Category Theory, the dual of P (Pop) is the statement obtained by replacing the

4

1. Categories

word ’dom“ by ’cod,“ ’cod“ by ’dom,“ ’g ° h“ by ’h ° g.“ If P is true in a category C, then Pop

is true in Cop; if P is true in every category, then also Pop is, since every category is the dual of its

dual.

Duality may be applied to diagrams as well: given a diagram in a category C, the dual diagram in

Cop is obtained by simply reverting the arrows; of course, a dual diagram commutes if and only if

the original one does.

1.3.3 Definition Given two Categories C and D, the product category C´ D has for objects

´

the pairs (a,b) where a and b are respectively objects of C and D, and for morphisms pairs (f,g):

(a,b)®(a',b') where f: a®a' and g: b®b' are respectively morphisms of C and D. Finally, id(a,b)

= (ida,idb) and (f,g) ° (f',g') = (f ° f', g ° g').

1.3.4 Definition Given a category C and an object a in ObC , the category C¯a of objects

over a is so defined: ObC¯a = {fÎMor C / cod(f) = a}; given two objects f: b®a, g: c®a, a

morphism with source f and target g is an arrow hÎC[b, c] such that g ° h = f. Identities and

composition in C¯a are inherited from C.

In case C is Set in the above definition, it is useful to think of an object g: B®A in Set¯A as an

A-indexed family of disjoint sets, namely, {g-1(a)}aÎA (these sets are the inverse images of

elements in A under g). Then h: B®B' is a morphism from g: B®A to g': B'®A if and only if

it is consistent with the ’decomposition“ of B and C induced by g and g', i.e., if and only if (iff)

"b bÎg-1(a) Þ h(b)Îg'-1(a).

Since the intended meaning behind the construction of a category C¯I is that to consider an

object g: A®I as a collection {{i}´g -1 (i)} iÎI , it is usual to call C¯I a slice category over I

(denoted C/I). An object g: A®I of the slice category is then called a generalized object of C at

stage I. A section of g: A®I is a function s: I®A such that g ° s = idI; the idea is that s gives,

for each index iÎI, an element s(i)Îg-1(i).

Exercise Define the dual notion, that is, the category C-a of objectsunder a, whose objects are

the arrows with source a.

1.4 Monic, Epic, and Principal Morphisms

A function f between two sets A and B is called ’injective“ when, for all a , a' Î A , if f(a) =

f(a') then a = a'. In particular, given any two functions g, h : C®A, if for all cÎC f(g(c)) =

f(h(c)), then for all cÎC g(c) = h(c) or, also, if f ° g = f ° h then g = h . Thus, every injective

function behaves like a left identity (it is left cancellable). The converse is also true: given f: A®B, if

5

1. Categories

for any pair of functions g, h : C®A , f ° g = f ° h implies g = h , then f is injective. For suppose

otherwise: then there are a and a' such that f(a) = f(a') but a ¹ a' ; define then g and h by g(c)

= a for all cÎ C , and h(c) = a' for all cÎ C; of course f ° g = f ° h but g ¹ h , that is, a

contradiction.

We have proved thus that a function f is injective if and only if f ° g = f ° h implies g = h . In a

similar way it is not difficult to prove that f is surjective if and only if g ° f = h ° f implies g = h.

These considerations motivate the following definitions.

1.4.1 Definition. Let C be a category and a, bÎOb C . Then

i. an arrow hÎC[a,b] is epic (is an epimorphism) iff

g»h=f»h Þ g=f;

ii. an arrow hÎC[a,b] is monic (is a monomorphism) iff

h»g=h»f Þ g=f;

iii. an arrow hÎC[a,b] is iso (is an isomorphism) iff there exists gÎC[b,a] such that

g » h = id and h » g = id .

Two objects a and b are isomorphic (a @ b) if there exists an isomorphism hÎC[a,b]. Clearly,

any isomorphism is monic and epic; the converse, though, does not need to be true (see the example

and the exercises below).

A monic (or epic) hÎC[a,b] (or h'ÎC[a,b]) is split if there exist gÎC[b,a] (or g'ÎC[b,a])

such that g » h = id (h' » g' = id).

Although the intuition of regarding mono- and epimorphisms as injective and surjective maps is

correct for many interesting categories, sometimes it can be misleading. Consider, say, the category

Mon of monoids and the inclusion inc from w, the positive integers, into z, the relative ones. Clearly

mono, inc is also epi, though. As a matter of fact, take g,hÎMon[z,a] for some monoid a, and write

\g(n) for g(-n). Then g » inc = h » inc implies g = h for g(-n) = \g(n) =\h(n) = h(-n) (that is, the

behavior of the monoids• homomorphism g or h on z is entirely determined by their behavior on

w). As a side consequence, we may also conclude that not every arrow that is both monic and epic is

an isomorphism: this is clearly in contrast to the set-theoretic intuition.

Exercises

1. Give an epi which is not surjective in Top.

2. Find a counterexample for the following assertion: let C be a category; if fÎC[a,b] and gÎC[b,a]

are mono, then a is isomorphic to b. (Note that the assertion is true in Set.)

3. Prove that a split monic is an iso.

1.4.2 Definition Let C be a category and a, bÎObC. Then

i. an arrow hÎC[a,b] is a principal morphism iff

6

1. Categories

"fÎC[a,b] $gÎC[a,a] f = h» g ;

ii. a pair of arrows fÎC[a,b] and gÎC[b,a] is a retraction pair iff g » f=id. Then, a is called a

retract of b (a<b) via the retraction pair (f,g).

By diagrams, h is principal iff for all f there is a g such that

Principal morphisms have been inspired by recursion theory; the idea they are based on essentially

corresponds to a classical notion of reducibility (see the category EN in section 2.2 below).

1.4.3 Proposition Let C be a category and a, bÎObC . Then

1. if a<b via (i,h), then h is epi and principal, i is mono;

2. if hÎC[a,b] is principal and there exists an epi kÎC[a,b,], then h is epi;

3. if a<b and fÎC[b,a] is principal, then there exists gÎC[a,b] such that a<b via (g,f).

Proof 1. g»h = f»h Þ g»h»i = f»h»i Þ g = f, for h»i = id.

The proof that h is principal is a simple diagram chase:

That is, "f $g f = h»g. Just take g = i»f; then h»g = h»i»f = f.

Finally, i»g = i»f Þ h»i»g = h»i»f Þ g = f.

2. g»h = f»h Þ g»k = g»h»g' = f»h»g' = f»k (for a suitable g') Þ g = f .

3. Let a<b via (j,i). Since f is principal, $sÎC[b,b] j = f°s. Then, for g = s°i, one has f°g = j°i =

ida. As a diagram,

¨

7

1. Categories

Exercises

1. Characterize retractions in terms of split monos and epis.

2. Show that, given a category C, one can define a category CRet whose objects are the same of C

and whose morphisms are retraction pairs in C, that is FÎCRet[a,b] iff F=(f,g) and a<b via (f,g) in

C.

If (f:a®b, g:b®a) is a retraction pair, then the function h = f ° g: b®b is idempotent, that is, h ° h

= h . Indeed, h ° h = (f ° g) ° (f ° g) = f ° (g ° f) ° g = f ° g = h . This property suggests the following

definition:

1.4.4 Definition Given a category C and an object bÎOb C , the category of idempotents on

b (Retb) is so defined:

ObRetb = { fÎC[b,b] / f ° f = f }

MorRetb = { (f, k, g) / f, gÎObRetb, kÎC[b,b], k = g ° k ° f }

dom( (f, k, g) ) = f, cod( (f, k, g) ) = g

idf = (f, f, f)

(f, k, g) ° (g', k', f) = (g', k ° k', g)

We leave as an exercise for the reader to check the identity and associative laws for the previous

category. Retb will be used in several places because of its relevance to this book.

1.5 Subobjects

The concept of subobject is the categorical version of the set-theoretical subset . The main idea is to

regard a subset A of a given object B as a monomorphism f: D®B (intuitively, a monomorphism

f such that ’f(D) = A“). Of course, many different monic arrows may define the same subset; thus,

it is necessary to introduce a reasonable equivalence relation, and define subobjects up to this

equivalence.

Let C be a category. If f: b®a and g: c®a are two monic arrows with common target a, then

we say f £ g if and only if there exists h: b®c such that g ° h = f. Note that in this case, the unique

h must be monic too, indeed h ° k = h ° k' Þ g ° h ° k = g ° h ° k' Þ f ° k = f ° k' Þ k = k'.

Exercise Prove that the preorder £ is the full subcategory of C¯a determined by monomorphisms

only.

8

1. Categories

When f £ g and g £ f we write f @ g. Then @ is an equivalence relation among the

monomorphisms with common target a (prove it as an exercise); the equivalence classes of this

equivalence relation are called subobjects of a.

1.5.1 Definition Let a be an object of a category C. A subobject [f] of a is an equivalence

class of a monomorphism f: b®a, with respect to the equivalence relation @ defined above.

Very often, we shall make no distinction between equivalence classes and their representatives, and

we shall denote a subobject with a single monomorphism.

It should be clear that the categorical approach to ’subsets“ carries more information than the set-

theoretic one. Monomorphisms, like all morphisms, preserve the structural information of the

category. For example, in the category Grp of groups subobjects are subgroups: (mono)morphisms

must take the identity to the identity and preserve the group operation. Similarly consider the category

of p.o.sets (partially ordered sets) with a bottom element. A subobject of one such p.o.set must be a

structured subset as well, and it must contain an element smaller than all the others.

References: Any book in Category Theory, such as MacLane (1971) Herrlich and Strecker

(1973), Arbib and Manes (1975), Barr and Wells (1985), Rydeheard and Burstall (1988). The

specific notions and categories introduced (such as retractions) will be used later in more structured

settings, with the appropriate references.

9

2. Constructions

Chapter 2

CONSTRUCTIONS

In this chapter we consider some fundamental categorical constructions, i. e., particular objects (and

morphisms) that satisfy a given set of axioms described in the language of Category Theory. Since in

this language there is no way to look at the internal membership structure of objects, all the concepts

must be defined by their relations with other objects, and these relations are established by the

existence and the equality of particular morphisms. This property of the categorical language, if

compared to the traditional set-theoretic jargon, may be well understood by an analogy with computer

science; namely, as we already mentioned, the categorical description corresponds to an abstract data

specification, while the traditional set-theoretic approach is more similar to a concrete implementation.

2.1 Initial and Terminal Objects

2.1.1 Definition Let C be a category. An object 0 is initial iff for any bÎObC there is a unique

fÎC[0,b].

The typical example of an initial object is the empty set Æ in Set; indeed the empty function (i.e., the

function whose graph is empty) is the unique arrow with Æ for source.

A more interesting example is the following. Let S be a signature. The class AlgS of S -algebras

with S-homomorphisms as arrows forms a category. AlgS has an initial object TS which is called S-

word-algebras, or also Herbrand Universe for S . The set TS,s (the carrier of TS of sort s) is just the

set of all well-formed expressions of sort s. If S is derived by a context free grammar (that is: sorts

are nonterminals and operator symbols are productions of the grammar), then TS ,s is the set of all

parse trees for derivations in the grammar from the nonterminal s. In general the initial S-algebra TS

corresponds to the syntax of a language of signature S. Any other S-algebras A in AlgS is a possible

semantic domain; the semantic function (interpretation) is the unique homomorphism from TS to A.

Initiality is the simplest universal notion in Category Theory, since it is given by the existence and

unicity of morphisms satisfying certain properties. This method is used everywhere in Category

Theory.

2.1.2 Proposition If 0 and 0' are two initial objects in a category C, then they are isomorphic.

10

2. Constructions

Proof. Let i: 0®0', j: 0'®0 the morphisms respectively given by the initiality of 0 and 0'. Then

j ° i: 0®0, but also id0: 0®0, and since by initiality of 0, there is exactly one morphism in C[0,0],

then j ° i = id0; in the same way, by initiality of 0' we have i ° j = id0'.¨

We will now show how duality can be used to define new concepts and to prove new assertions.

Let P(c) be the property ’for any bÎObC there is a unique f, such that dom(f) = c, cod(f) = b.“ By

definition c is initial iff P(c) holds; that is, P defines initiality. The dual statement of P is Pop(c) =

’for any bÎObC there is a unique f, such that cod(f) = c, dom(f) = b.“ Usually the dual Qop of a

property Q defines a concept named by prefixing ’co-“ to the name of the property Q. In our case, we

say that Pop defines coinitiality. An object c such that Pop(c) holds, is called co-initial. Anyway it

is common practice to assign to every coentity an independent name which better expresses its

properties; for example, a coinitial object is known as terminal object. Note that an initial object is

coterminal.

Terminal objects are usually represented with the number 1 or with the letter t. The unique

morphism from an object a to the terminal object t is usually written !a: a®t.

Any singleton set is terminal in Set. In the category 2 one object is initial and the other one is

terminal. If c is initial in C, then it is terminal in the dual category Cop.

Consider now the statement P1 = ’If 0 and 0' are two initial objects, then they are isomorphic.“

Its dual is: P1op = ’If 0 and 0' are two terminal objects, then they are isomorphic.“ (the property

to be an isomorphism is the dual of itself: prove it as an exercise.) By our discussion of duality in

chapter 1 and, since by proposition 2.1.2 P1 holds in every category, P1op also does. We conclude

the following:

2.1.3 Proposition If 0 and 0' are two terminal objects in a category C, then they are

isomorphic.

Proof By duality and by proposition 2.1.2.¨

An object c in a category C may be both initial and terminal. An example is the unit group in Grp;

in this case, it is called a zero object.

In Set, a morphism from the singleton {*} to a set A defines an element of A. For this reason an

arrow from a terminal object t to an object a in a generic category C is usually called an element

or a point of a. In this case, however, the set-theoretic intuition must be used very carefully, because

it is quite common to work in categories where the categorical notion does not reflect the behavior of

elements in Set. For example the set-theoretic intuition would suggest that every non-initial object

must have at least one element: but consider the partial order category 3 which has three object 0 £

1 £ 2; clearly 0 is initial and 2 is terminal, 1 is non-initial but has no elements. Similarly, in Set

two arrows are equal iff they coincide on all points, or, more formally, given functions f and g,

11

2. Constructions

one has f ¹ g iff there is an element x of their domain such that f ° x ¹ g ° x. However, in a

generic category C with terminal object t, this is not necessarily true.

2.1.4 Definition. Let C be a category. tÎOb C is a generator iff for all a,bÎOb C and all

f,gÎC[a,b], one has: f ¹ g Þ $hÎC[t,a] f°h ¹ g°h .

C has enough points (or is well pointed), if there exists a generator t that is terminal in the

given category.

In short, a category has enough points when the arrows from the terminal object allow to discriminate

between morphisms, similarly as for elements over Set. Of course, it is not a surprise that the set-

theoretic notions of ’element“ and of ’extensionality“ are somewhat awkward to deal with in the

language of Category Theory.

2.2 Products and Coproducts

The categorical product is merely a ’structural“ generalization of the notion of Cartesian product of

sets. Given two sets A and B, their cartesian product is:

A´B = {<x,y> / xÎA, yÎB}

Associated with this set there are two special maps pA: A´B®A , pB: A´B®B called projections,

such that for every <x,y> in A´B pA(<x,y>) = x, pB(<x,y>) = y. Note that for every c in A´B,

<pA(c), pB(c)> = c.

Let C be another set, and f: C®A, g: C®B. Define <f,g>: C®A´B by <f,g>(c) = <f(c),g(c)>

for every cÎC. Then, for every cÎC, pA( <f,g>(c) ) = pA( <f(c),g(c)> ) = f(c), that is, pA ° <f,g>

= f. In the same way, we obtain pB ° <f,g> = g. Conversely, let h: C®A´B. Then for every cÎC,

<pA ° h, pB ° h >(c) = <pA(h(c)), pB(h(c))> = h(c), that is, <pA ° h, pB ° h > = h.

The previous consideration suggests the following definition:

2.2.1 Definition Let C be a category, and a,bÎOb C . The categorical product of a and b is

an object a´b together with two morphisms pa: a´b®a, pb: a´b®b, and for every object c an

operation < , >c : C[c,a]´C[c,b]®C[c,a´b] such that for all morphisms f: c®a, g: c®b, h:

c®a´b, the following equations hold:

ia. pa ° <f,g>c = f ;

ib. pb ° <f,g>c = g ;

ii. <pa ° h, pb ° h >c = h .

It is common practice to omit the subscript c in < , >c when its meaning is clear from the context.

12

2. Constructions

The operation < , > : C[c,a]´C[c,b]®C[c,a´b] of a categorical product is a bijection: its inverse

is the operation that takes every arrow hÎC[c,a´b] to the pair (pa ° h, pb ° h )ÎC[c,a]´C[c,b].

The proof that these operations are inverse of each other is stated above in definition 2.2.1.

Conversely, given a bijective operation < , > : C[c,a]´C[c,b]®C[c,a´b] which satisfies (ia) and

(ib), then (ii) is necessarily true. Indeed, let hÎC[c,a´b]. Then, since < , > is bijective, there is a

pair (f,g)ÎC[c,a]´C[c,b] such that h = <f,g>; but f = pa ° <f,g> = pa ° h and analogously, g = pb °

<f,g> = pb ° h; thus, h = <pa ° h, pb ° h >.

The last consideration leads us to a more compact but equivalent definition of a categorical

product.

2.2.2 Definition Let C be a category, and a,bÎOb C . The categorical product of a and b is

an object a´b together with two morphisms pa: a´b®a , pb: a´b®b, such that, for any fÎC[c,a]

and gÎC[c,b], there exists exactly one hÎC[c,a´b] such that the following diagram commutes

2.2.3 Definition For fÎC[a,c] and gÎC[b,d], set f´g = <f»pa,g»pb> : a´b® c´d.

Exercise Prove that for all arrows h: e®a and k: e®b, f´g»<h,k> = <f»h,g»k>.

2.2.4 Proposition In a category, the product is unique (up to isomorphisms), if it exists.

Proof Let a„b be an alternative product with projections qa and qb.

Then <qa,qb> » <pa,pb> is the unique morphism such that the following diagram commutes:

13

2. Constructions

Since ida´b also does the same job, ida´b = <pa,pb>»<qa,qb>.

By symmetry, one also has <pa,pb> » <qa,qb> = ida’„b .¨

Exercise. Prove the following facts:

1. a @ a' and b @ b' imply a´b @ a'´b'.

2. a´b @ b´a.

2.2.5 Definition A category C is Cartesian (C is a CC) iff

i. it contains a terminal object t;

ii. every pair a,bÎObC has a categorical product (a´b, pa,b,1: a´b®a, pa,b,2: a´b®b)

Exercises

1. Generalize the definition of a product of two objects to arbitrary products.

2. Prove that a Cartesian category C always contains all finite products.

3. Let C be a CC and let t be its terminal object. Prove that for all b in ObC, b @ t´b @ b´t .

Examples The categories Set, Top, Grp are all Cartesian.

An interesting Cartesian category in Computability Theory is the category EN of numbered sets.

Objects in EN are pairs a = (a,ea), where a is a countable set and ea: w®a is an onto map (an

enumeration of a). fÎEN[a,b] iff for some total recursive f' the following diagram commutes:

We say that f' represents f. The product is easily obtained by using any effective pairing of w2,

[,]: w´w®w.

A typical numbered set which is worth studying is PR = (PR,f), the partial recursive functions

with a Goedel numbering f: w®PR. Then EN[PR,PR ] are exactly the type two recursive

functionals. Of course, this is also a countable set. It is not trivial, though, to construct an

’acceptable“ enumeration of it. This will be an important issue in the sequel.

Exercises

1. Let w = (w,id) in EN. Then fÎEN[w,PR] iff $f'ÎPR f'([x,y]) = f(x)(y). Moreover, gÎ

EN[w,PR] is principal iff g is an acceptable Goedel numbering of PR, in the sense of classical

recursion theory.

14

2. Constructions

2. Let C be a CC, and V be an object such that V´V<V. Then the category of retractions on V (see

definition 1.4.4 ) is a CC.

The dual of the notion of a product is the coproduct a+b with embeddings q1, q2.

2.2.6 Definition. Let C be a category, and a,bÎOb C . The coproduct of a and b is an object

a+b together with two morphisms qa: a®a+b, qb: b®a+b such that, for any fÎC[a,c] and

gÎC[b,c], there exists exactly one hÎC[a+b,c] such that the following diagram commutes

By duality, the coproduct is unique (up to isomorphisms).

Examples

1. In Set the coproduct is the disjoint union.

2. In a preorder P the product is the greatest lower bound, if it exists. The coproduct is the least

upper bound, if it exists.

3. Let CPO be the category of complete partial orders with continuous functions with respect to the

order or Scott topology. CPOS is the subcategory with only strict functions, i.e., morphisms always

take the least element ^ to the least element of the target space. It is easy to see that both categories

are Cartesian. The coproduct in CPOS is given by the coalesced sum, i.e., the disjoint union except

for the identification of the two least elements. On the other hand, there is no coproduct in CPO.

This may be seen by observing that in CPO one may have f( ^ ) ¹ g( ^ ), by which the coalesced

sum fails to give a coproduct; an extra common least element (disjoint sum) may give more than one

extension of the required <f,g>op.

2.3 Exponentials

In the connection we mentioned between Category Theory and Computation Theory, as ’theories of

functions,“ a fundamental aspect still has to be taken care of. In either case, we may be interested in

computing with procedures as arguments. That is, we may need to describe higher type functions.

So far we have only become familiar with Cartesian categories, where the object a´b, representing

the product, is defined. Thus, the notion of morphism taking morphisms as arguments doesn't yet

make sense. What we first need, then, is a further closure property, namely, the existence within the

15

2. Constructions

category of an object ba which suitably represents the set of morphisms from b to a. With an

informal reference to typing in programming, the key property of the objects, which represent the

sets of morphisms, provides an interpretation to a common construct in actual programming, namely,

the identification of types such as A´B®C and A®(B®C). This corresponds to the following

important uniformity property of programs of several arguments, which is directly inherited from

classical Recursion Theory.

Let {fi}iÎw = PR be an acceptable Gšdel numbering of the partial recursive functions and [,]:

w´w®w be an effective pairing. Define then, as usual, f: w´w®w is a binary partial recursive

function iff $f'ÎPR f(x,y) = f'([x,y]) (similarly, for n-ary functions, n ³ 2). By this and by the

s-m-n iteration theorem one immediately has f: w´w®w is partial recursive iff $sÎR fs(x)(y) =

f(x,y).

Thus, a two-(or more) argument function f is computable iff it is computable in each argument

and the function x |_ f(x,_) is also ’computable,“ i.e., $sÎR fs(x) = f(x,_). In other words, in

computability theory, f is in w´w®w iff x |_ f(x,_) is in w®(w®w). Similarly, the category-

theoretic closure property we need concerns the existence, for any f: c´a®b, of a morphism within

the category, which does the same job as s or x |_ f(x,_) in recursion theory. We will call it L(f).

Exercise For n ³ 2, not every n-ary function which is computable in each argument needs to be

computable. (Hint: take g total nonrecursive and set f(x,y) = g(min{x,y}) ).

2.3.1 Definition Let C be a Cartesian category, and a,bÎOb C . The exponent of a and b is

an object ba together with a morphism evala,b: ba´a®b (evaluation map), and for every object c an

operation Lc : C[c´a,b]®C[c,ba] such that for all morphisms f: c´a®b, h: c®ba, the following

equations hold:

b). evala,b ° (L(f)´ida) = f ;

h) . Lc(evala,b ° (h´ida)) = h .

(We may omit the indices when unambiguous, as usual.)

In Set the exponent set of A and B is BA = {f / f is a function from A to B}, thus BA =

Set[A,B]. The function eval: BA´A®B is given by the rule: eval(<f,x>) = f(x) .

L: Set[C´A,B]®Set[C,BA ] takes every function f: C´A®B to the function L(f): C®B A

defined by L(f)(c) = la.f(c,a), where la.f(c,a)ÎBA=Set[A,B] is the function which takes aÎA to

f(c,a)ÎB. The proof of (b) and (h) is almost immediate.

As in the case of the product, observe that in general the operation L: C[c´a,b]®C[c,ba] in

definition 2.3.1 is a bijection. Indeed, by (b) and (h), L -1 is the operation which takes every

hÎC[c,ba] to evala,b ° (h´ida)ÎC[c´a,b].

16

2. Constructions

Conversely, if L : C[c´a,b]®C[c,ba] is a bijection and (b) holds, then (h) is necessarily true.

Indeed, let hÎC[c,b a ] and take fÎC[c´a,b] such that h = L(f); then L(eval a,b ° (h´id a )) =

L(evala,b ° (L(f)´ida)) = L(f) = h .

The following is thus an equivalent definition of ’exponent“:

2.3.2 Definition Let C be a Cartesian category and a,bÎObC. The exponent of a and b is an

object ba together with a morphism evala,b: ba´a®b, such that for all morphisms f: c´a®b, there

exists one and only one h: c®ba such that the following diagram commutes:

Exercise By setting L(f) = h, give the details of the equivalence proof between the two definitions.

The previous diagram should suggest in which sense ba ’represents“ C[a,b]. The eval morphism

generalizes the set-theoretic evaluation function eval(f,x) = f(x). Moreover, take c = t, the terminal

object. Then C[t,ba] @ C[t´a,b] @ C[a,b] as sets. This is particularly significant if C has enough

points (why?).

2.3.3 Definition. C is a Cartesian closed category (CCC) iff

1. C is cartesian,

2. for every pair a,bÎObC, there is an exponent.

Set is a CCC: the previous definition of exponents in Set clearly holds for every pair of sets.

Another simple CCC is CPO, the category of complete partial orders and continuous maps. As well-

known, given c.p.o.•s a and b, CPO[a,b] is also a c.p.o., with respect to the pointwise ordering.

Moreover, both eval and L(f), defined as for Set by using continuous functions, are continuous

and satisfy the required conditions. Note that the proof uses the well-known fact that in CPO a

function is continuous iff it is so in each argument and the map x |_ ly.f(x,y) is continuous.

Actually, even L is continuous.

Among the various examples of categories mentioned in these notes, an important one does not

satisfy Cartesian closedness: the category EN in section.2.2. Consider, say, w = (w,id). Then

EN[w,w] (= R, the recursive functions) is surely countable. However, if a numbered set (ww,j) and

17

2. Constructions

a morphism eval with the above properties existed, then u(x,y) = eval(j(x),y) would be a universal

function for R.

Also, the w-algebraic c.p.o.•s, that is, the c.p.o.•s with a countable collection of compact elements

approximating all the others (see Scott domains below) and continuous maps as morphisms do not

form a CCC. They contain, though, some fundamental subCCC's for the purposes of denotational

semantics of programming languages and higher type Recursion Theory. They will be explored in the

examples below.

Given a CCC D, it may be interesting to consider specific "structures of types" in it. That is, for a

collection A of objects in D, let DA be the full sub CCC generated by A in D, i.e., the least full

sub category such that AÍDA and a,bÎDA Þ a´b,abÎDA.

Exercise Prove that in any CCC one has ab´c @ (ab)c.

In definition 1.4.2, we introduced the notion of ’retract“: in a category C, a<b via the retraction

(i,j) iff j » i = ida. In these assumptions, i turns out to be mono and j epic. Thus, a retract a of

b is a subobject of b in the sense of section 1.5. In the case of Set, nonempty subsets and retracts

happen to coincide, as surjections from a set to a subset are always possible. In more structured

categories this reinforcement of the idea of subset, given by retractions, turns out to be very

informative. In particular, we will discuss categories with nontrivial objects a such that aa<a. This

is clearly impossible in Set because, by Cantor•s theorem, the cardinality of the exponent aa , when

a is not a singleton, is strictly bigger than the cardinality of a. In short, we will put together retracts

and exponents, in a nontrivial way, in order to discuss one of the early relevant applications of

categorical notions to computer science, namely the invention of mathematical (categorical, to be

precise) models of type-free languages. In these languages, programs are viewed as data or,

semantically, exponents may be retracted into (source and target) objects. It is convenient to prove, in

general, some basic properties of exponents and retractions for their relevance and simplicity as well

as for some preliminary training on equational reasononing, which will turn out to be useful to the

reader in the sequel.

2.3.4 Proposition Let C be a CCC. If a<a' (via ina : a®a', outa : a'®a), and b<b' (via inb :

b®b', outb: b'®b), then ba<b'a', via L(inb°eval°(id´outa)): ba®b'a', L(outb°eval°(id´ina)):

b'a'®ba.

Proof. L(outb°eval°(id´ina)) ° L(inb°eval°(id´outa)) =

= L(outb°eval°(id´ina)°L(inb°eval°(id´outa))´id )

= L(outb°eval°L(inb°eval°(id´outa))´id°(id´ina) )

= L(outb°(inb°eval° id´outa )°(id´ina) )

= L(eval ° id´(outa°ina) )

18

2. Constructions

= L(eval ° id´id)

= id. ¨

2.3.5 Definition Let C be a CCC. An object V of C is reflexive iff VV <V.

Before we get to see some reflexive objects in relevant CCC's in the following sections, it is worth

proving two simple, but general, properties of reflexive objects (see chap.8 for applications).

2.3.6 Proposition Let C be a CCC, and V a reflexive object. Then t < V and V´V < V .

Proof. Let (in: VV®V, out: V®VV) the retraction pair between VV and V. In order to prove that

t<V we must only prove the existence of a morphism from t to V (why?). Let then p1: t´V®V be

the projection; L(p1): t®VV, and thus in ° L(p1): t®V.

The proof that V´V<V is much more complex; we prove that V´V<VV; then V´V<V follows by

composition.

Let app = eval°(out´idV ): V´V®V, and let a a,b,c be the isomorphism a a,b,c: (b´c)´a®

(a´b)´c. Then: app ° (app´id) ° aV,V,V : (V´V)´V®V

in1 = L( app ° (app´id) ° a ) : (V´V)®VV.

and

By proposition 2.3.4 one has (VV)V<VV via

in2 = L( in ° eval ° (id´id) ) : (VV)V®VV

out2 = L( out ° eval ° (id´id) ) : VV®(VV)V.

Let p2: t´V®V and pr1:V´V®V, pr2: V´V®V be the projections respectively associated with the

products t´V and V´V. Then, for i =1,2, L(pr i): V® V V and, thus, for L(L(pr i ) ° p 2 ) :

t®(VV)V, pi = in ° in2 ° L(L(pri ) ° p2) : t®V.

Define, then, out1 = < eval ° <id, p1 ° !VV> , eval ° <id, p2 ° !VV> > : VV®V´V.

We must prove that out1 ° in1 = idV´V , or equivalently that for i = 1,2, pri ° out1 ° in1 =

pri .

pri ° out1 ° in1 = eval ° <id, pi ° !VV> ° in1

= eval ° < L( app ° (app´id) ° a ), pi ° !V´V>

= app ° (app´id) ° a ° < idV´V, pi ° !V´V>

= app ° < app ° < pi ° !V´V, pr1> , pr2>

= app ° < eval°(out´idV) ° < in°in2°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>

= app ° < eval°<in2°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>

= app ° < eval°< L(in°eval°(id´id))°L( L(pri ) ° p2 ) ° !V´V, pr1>, pr2>

= app ° < eval°< L(in°eval°(L( L(pri ) ° p2 )´id))° !V´V, pr1>, pr2>

= app ° < eval°< L(in ° L(pri ) ° p2 )° !V´V, pr1>, pr2>

= app ° < in ° L(pri ) ° pr1, pr2>

= eval°(out´idV) ° (in ° L(pri ))´idV

19

2. Constructions

= eval° (L(pri )´idV)

= pri . ¨

Exercises For the following exercises, assume that C is a CCC.

1. Let V be a reflexive object of C. Prove that the collection RetV of all retracts of V in C is a CCC.

2. (Difficult, see section 8.8) Let b be an object of C. A fixpoint operator for b is a morphism

Fixb: bb®b such that Fixb = evalb,b° <id,Fixb>. Let VV<V via (in,out). Let also

F = eval ° <id, in> : VV®V ;

H = L( eval ° (id´(F°out)) ) : VV®VV.

Prove that F°H is a fixpoint operator for V. Define a fixpoint operator for all objects in RetV.

3. Let C be a CCC and suppose that for all a, b in ObC there exists the coproduct a+b (with

embedding ina: a®a+b , inb: b®a+b ). Prove that, for all c in ObC, (a´c)+(b´c) is isomorphic to

(a+b)´c, and define explicitly the isomorphism.

Result: (a´c)+(b´c) @ (a+b)´c via

i1 = (ina´idc)+(ina´idc): (a´c)+(b´c) ® (a+b)´c

i2 = L-1( L(ina´c)+L(inb´c) ): (a+b)´c ® (a´c)+(b´c)

Proving i2°i1=id is easy. For i1°i2 = id, note first that g°L-1(f) = L-1(L(g°eval)°f).

Then, in a few steps, one obtains

i1°i2 = L-1( L(ina´idc)+L(inb´idc) )

= L-1( L(id)°ina+L(id)°inb )

= L-1( L(id) )

= id

2.4 Examples of CCC•s

2.4.1 Scott Domains

In this section and in the following one we introduced two fundamental examples of CCC's, namely,

Scott domains and coherent domains. We define only the exponent object and the eval function and

check that they are respectively an object and an arrow of the category. We leave the problem of

defining the isomorphism L and checking (bcat) and (hcat) as an (easy) exercise for the reader.

2.4.1.1 Definition Let (X,£) be a partiallly ordered set (po-set).

D Í X is directed iff it is nonempty and, for any i,jÎD, there is kÎD such that i £ k, j £ k. A

p.o.set (X,£) is complete (is a CPO) iff every directed subset DÍX has a least upper bound ÈD

(the least element ^ is the least upper bound of the empty directed set).

20

2. Constructions

A point xÎX is compact (finite) if for every directed D such that x £ ÈD , there is an element

yÎD such that x £ y. Let X0 denote the collection of compact elements of X.

The c.p.o. (X, £) is algebraic if for every xÎX the set x¯ = {x 0 ÎX 0 | x0 £ x}is directed and

È(x¯) = x.

A c.p.o. (X,£) is bounded complete if every bounded subset of X has a least upper bound. A

Scott Domain is a bounded complete algebraic c.p.o..

Exercises

1. Check that {{y | x0 £ y} | x0ÎX0} is a basis for a T0 topology on a Scott Domain. This topology

is usually called Scott topology.

2. Prove that the least upper bound of a finite set of finite elements is always finite, if it exists.

3. (Nontrivial) Find counterexamples for the following assertions:

i. if x0 is compact then the set {y | y £ x0} is finite;

ii. if x0 is compact and y £ x0 then y is compact.

2.4.1.2 Definition Let (X,£X ), (Y, £Y ) be c.p.o.•s. A function f: X® Y is monotonic if it

is order preserving, i.e., i £X j implies f(i) £Y f(j) . (We will often omit the subscript X in £X.)

A function f: X®Y is continuous if for every directed DÍX, f(ÈD) = ÈdÎDf(d).

Exercise Let (X,£X), (Y, £Y) be Scott domains. Prove that a function f: X®Y is continuous

according to the previous definition iff it is continuos with respect to the Scott topology.

2.4.1.3 Definition The category D has Scott domains for objects and continuous functions for

morphisms. Let X, Y be objects of D. YX is just the collection of the continuous functions from

X to Y ordered pointwise.

Of course YX is a c.p.o.. We have to prove that it is bounded complete and algebraic.

In order to show that YX is bounded complete, assume that {fi} iÎI has an upper bound g.

Define then h by h(x) = È iÎI{fi(x)}. The function h is well defined since the set {fi(x)}iÎI is

bounded by g(x) and, thus, it has a least upper bound in Y. Moreover, h is continuous because for

every directed set D in X one has:

h(ÈD) = È iÎI{fi(ÈD)}

= È iÎI È xÎD {fi(x)} by the continuity of fi

= È xÎD È iÎI {fi(x)}

= È xÎD {h(x)}

It easy to check that h is a least upper bound for {fi}iÎI.

To show that YX is algebraic, we explicitly define the set (YX)0 of its compact elements.

21

2. Constructions

2.4.1.4 Definition A step funcion from X to Y is a function step-a,b where aÎX 0 , bÎY 0 ,

defined by: step-a,b (x) = if a £ x then b else ^ .

We claim that the compact element of YX are exactly the least upper bound of finite bounded sets of

step functions. In other words, for every f0Î(YX)0, (*) f0 = ÈiÎI{step-ai,bi} for some finite I.

Let us prove first that every function f = È iÎI {step-a i,b i} is compact, when I is finite and

È iÎI{step-ai,bi} exists, i.e., when for all subset J of I, aJ = È iÎJ{ai} exists Þ bJ = È iÎJ{bi}

exists (We then say that I is a compatible set of indices.)

Then, let {gh}hÎD be a directed family in YX such that f £ ÈhÎD{gh}. In particular, for every

J in I as above, f(aJ ) = bJ £ (È hÎD {g h })(a J ) = È hÎD {gh (a J )}. Clearly, for each J, bJ is

compact and {gh(aJ)}hÎD is directed. Let then bJ £ gh(J)(aJ) for some h(J)ÎD. Since I is finite

and {gh}hÎD is directed, let gk , for kÎD , be such that gk ³ gh(J) for all J in I. Clearly f £

gk and we are done.

Prove now for exercise that for every continuous function f: X®Y, one has

i. the set F = { ÈiÎI{step-ai,bi}| I finite, and bi £ f(ai) } is directed

ii. f = ÈF

Suppose then that f is compact. We need to prove that f = È iÎI {step-a i,bi} for some finite

compatible I. By the exercise, f = ÈF, for F directed; thus, there exists I such that È iÎI{step-

ai,bi}ÎF and È iÎI{step-ai,bi} ³ f = ÈF ³ È iÎI{step-ai,bi}. In conclusion f = È iÎI{step-ai,bi};

that is, every finite element in XY has the form (*) and, in particular, XY is a Scott domain.

The function evalX,Y: YX´X®Y is defined by evalX,Y(f,x) = f(x). The proof that eval is

continuous is straightforward.

Interesting examples of Scott Domains may be found everywhere in the literature of denotational

semantics. Indeed, the Cartesian closedness of the category allows you to construct plenty of them as

products and exponents over commonly used ground types. That is, consider your preferred types

of data (integers, booleans, strings,etc.). Organize them as flat p.o.sets, i.e., add a least element ^

and set x £ x' iff x = ^ or x = x'. These are clearly objects of D as well as their products and

exponents.

Other relevant examples are given, for example, by the p.o.sets P of the partial maps from w to

w, the natural numbers, and Pw, the powerset of w. The partial order, in these cases, is given by set

inclusion, which on P means graph inclusion of functions, i.e., f £ g iff "n (f(n)¯ Þ g(n) =

f(n)). As an exercise, the reader may check that both P and Pw live in D.

Interestingly enough, these two familar structures are also reflexive objects in D . We sketch the

proof of this for Pw , see section 9.6-2 for more on P.

22

2. Constructions

Let {en}nÎw be a canonical (bijective and effective) enumeration of the finite subsets of w and let

< , > : w´w®w be a canonical coding of pairs. Define then graph: D[Pw,Pw]®Pw by graph(f) =

{<n,m> | mÎf(en)} and fun: Pw®D[Pw,Pw] by fun(a)(b) = {m | $en Í b <n,m>Îa}. It is a

simple exercise to check that graph and fun are morphisms in D. Moreover, fun » graph = id and,

thus, PwPw<Pw.

This example, which played a relevant role in denotational semantics, has been directly inspired by

Recursion Theory (see the references). Indeed, the work carried on so far can be naturally

’effectivized.“

2.4.1.5 Definition A Scott domain X = (X,£) is effectively given if $e 0 : w®X 0 bijective

and 1. $zÎX e0(n), e0(m) £ z is decidable in n, m

2. $gÎR ($zÎX e0(n), e0(m) £ z Þ e0(g(n,m)) = sup{e0(n),e0(m)}).

Call ED the category of effectively given Scott domains and continuous functions. ED is a CCC. As

a matter of fact, the effectiveness properties are easily inherited at higher types.

Observe that, instead of taking the least upper bounds (l.u.b.•s) of all directed sets, as required in

the definition of ED, one may take only the computable l.u.b.'s, i.e. the l.u.b.'s of directed sets or

ideals in (X0,e0) that are indexed over recursively enumerable (r.e.) sets. (One may independently

choose directed sets or ideals and obtain the same collection of computable elements.)

These limits are computable in a very sound sense. For example, (Pw, {en}nÎw, Í) is in ED

and its computable elements are exactly the r.e. sets.

Exercise Prove a similar fact for the set P of partial maps from w to w .

Call constructive domain a domain whose elements are the computable elements in an

effectively given domain. Since ED is Cartesian closed, this may be done in any (higher) type. In

particular, given the constructive domains Xc, Yc obtained from X and Y , one may consider the

constructive domain YXc of the computable elements of YX . Define then the following

2.4.1.6 CD is the category of constructive domains and continuous and computable morphisms.

Exercise One clearly has to check that, for fÎYXc, "xÎXc f(x)ÎYc.

By the Cartesian closedness of ED, CD also is a CCC. Observe that each Xc is countable and that it

can be effectively enumerated by using an acceptable enumeration of the r.e. sets. Typical objects in

CD are RE, the recursively enumerable sets, and PR (= Pc), the partial recursive functions (see the

exercise above).

23

2. Constructions

Thus, in a rather indirect way, that is by topological and order properties, we obtained a CCC of

countable (and numbered) sets. The proof that CD is a full sub-CCC of EN requires an important

generalization, in higher types, of the classical Myhill-Shepherdson theorem for enumeration

operators. The main application of CD is the characterization of the partial (continuous) and

computable functionals as the sub-CCC of CD generated by PR, i.e., taking PR and constructing all

higher types within CD (see also section 8.4-I). Moreover, one can give a countable and effective

interpretation to the recursive definitions of programs and data types within CD (by a constructive

version of the ’limit constructions“ in chapter 10).

Exercise Prove that RE is reflexive in CD (use the full and faithful embedding of CD in EN).

2.4.2 Coherent Domains

2.4.2.1 Definition A coherent structure is a pair (|X|,-), where |X| is a set and - is a

binary, reflexive, symmetric relation on |X|. The elements of |X| are called points, and the relation

- is called coherence.

The coherent domain associated with (|X|,-) is the collection X of subsets of P(|X|) whose

points are pairwise coherent. The elements of X are ordered by set-inclusion.

Coherence is extended to X in the obvious way, that is: A - B iff AÈBÎX.

Exercise Prove, when X is a coherent domain, that

1. ÆÎX

2. X is closed under directed union

3. (AÎX and B Í A) Þ BÎX

2.4.2.2 Definition Let X, Y be two coherent domains. A function F: X ® Y is stable iff

i). F is continuous

ii."A, BÎX A - B Þ F(AÇB) = F(A)ÇF(B)

2.4.2.3 Definition The category Stab has coherent domains as objects and stable functions as

morphisms.

Given two coherent domains X and Y, their product X´Y is defined by:

i |X´Y| = {(0,z) / zÎ|X| } È {(1,z) / zÎ|Y| }

ii. (a,z)-(a',z') [mod X´Y] iff a = a' Þ z - z' [mod D(a)], where D(0) = X and D(1) = Y.

24

2. Constructions

Exercise Define the projections and check that they are stable, i.e., prove that Stab is Cartesian.

There is simple way to obtain stable functions over coherent domains.

2.4.2.4 Definition Let X,Y be coherent domains. Let also f be an injective function from |X|

to |Y| such that, for all x,x'Î|X|, one has {x, x'}ÎX Û {f(x), f(x')}ÎY. Define then f+ :X®Y

and f -: Y®X by

i. f+(a) = {f(z) / zÎa }

ii. f -(b) = {z / f(z)Îb }

It is a matter of a simple exercise to prove that both f+ and f- are stable functions.

We need to construct next an exponent object out of the set of stable maps over coherent domains.

2.4.2.5 Definition Let F: X®Y be a stable function. The Trace of F is Tr(F) = {(a,z) / aÎX,

a is finite, zÎ|Y|, zÎF(a), ("a'Í a , zÎF(a') Þ a = a')}.

F is completely determined by its trace by means of the following equation: F(A) = {zÎ|Y| / $a Í A

(a,z)ÎTr(F)}.

Exercise Prove that the correspondence between stable functions and their traces is bijective.

Notation The symbol -- is used to represent strict coherence, i.e., A--B iff A-B and A¹B.

2.4.2.6 Definition Let |YX | = {(a,z) / aÎX, a is finite, zÎ|Y| }. Moreover, let (a,z) - (a',z')

iff

i. a -- a' [mod X] Þ z -- z' [mod Y] and

ii. a - a' [mod X] Þ z - z' [mod Y].

Then YX is the arrow domain (exponent object).

Exercises

1. Prove that conditions (i) and (ii) may be stated equivalently as

(a,z) = (a',z') or z--z' or not a-a'.

2. Prove that every element of YX is a trace of some stable function from X to Y , and conversely

that if F: X®Y is stable then tr(F)ÎYX.

3. Let f,g : X ® Y be two stable functions.

Define f £B g (Berry's order) iff "x,yÎX x Í y Þ f(x) = f(y)Çg(x)

Prove that f £B g if and only if Tr(f) Í Tr(g). Let moreover £p be the pointwise order. Prove that:

25

2. Constructions

i. f £B g Þ f £p g

ii. f-g Þ (f £Bg Û f £p g)

4. Let X,Y be coherent domains. A stable function f: X®Y is linear iff :

i. a È bÎX Þ f(a È b) = f(a) È f(b)

ii. f(Æ) = Æ

Prove that f: X®Y is linear iff its trace is formed of pairs (a,z), where the component a is a

singleton. Observe that the maps f+ and f- in 2.4.2.4 are actually linear. Call Lin the category of

coherent domains and linear maps.

5. Let f: X®Y, g: X®Y be two linear functions. Prove that Tr(f) Í Tr(g) if and only if for all x

in X f(x) £ g(x). Deduce as a corollary that on linear functions between coherent domains the order

of Berry coincides with the pointwise order.

2.4.2.7 Definition The function eval X,Y : YX ´X®Y is defined by the following equation:

"AÎY X , "BÎX evalX,Y (A,B) = {y / $(b,y)ÎA, b Í B}.

We prove that evalX,Y is stable. Continuity is trivial. We must only check that if (A,B)-(A',B')

[mod YX] then evalX,Y( (A,B)Ç(A',B') ) = evalX,Y( (A,B) ) Ç evalX,Y( (A',B') ). The inclusion

Í is immediate by continuity.

Take then z in evalX,Y ( (A,B) ) Ç eval X,Y ( (A',B') ). This implies $(b,z)ÎA, b Í B and

$(b',z)Î A', b' Í B'. Note that B-B' by hypothesis and, thus, b-b'. Moreover, also by

hypothesis, A-A' and then, by definition of consistency mod YX , one has b = b'. This implies

(b,z)ÎAÇA',b Í BÇB' Û zÎevalX,Y( (AÇA'),(BÇB') ) Û zÎevalX,Y( (A,B) Ç (A',B') ).

In conclusion, the category Stab of coherent domains and stable functions is a CCC.

Exercise Let f+ and f- be defined as in 2.4.2.4, over coherent domains X and Y. Prove that f-