ñòð. 23 |

!

then it is the coequalizer of its kernel pair.

5. Give an example in Set of a function with a kernel pair which is not the

coequalizer of its kernel pair.

e

6. Show that in the category of sets, S can be taken to be S [ fÂ¤g, where Â¤ is an

element not in S.

e

7. Show that in a topos, the subobject classiÂ¯er is 1, the object that represents

partial arrows into 1.

64 Toposes

5.3 Is a two-element poset complete?

This discussion requires familiarity with the concept of recursive set (there is an

algorithm that always halts that tells whether an element is in the set or not) and

recursively enumerable set (there is an algorithm that generates all the elements

of the set and no others).

We consider a 2 element chain we denote by 2. The word `complete' in the

question in the heading means that it has sups of all subsets. The question seems

absurd at Â¯rst, but it improves with age. In fact, we will show that both in a

topos and in realistic models of computation, the answer is `no'. Moreover the

answer is no in both cases for the same reason.

The claim we want to make, and for which this discussion is evidence, is

that topos semantics is an appropriate model for computation, or at least a more

appropriate one than set theory. This will not mean that topos theory will tell you

how to compute something that you could not compute without it. What happens

is that in many toposes certain computationally meaningless constructions cannot

be made at all, although they are all possible in Set.

5.3.1 Computation models Of course, in a most naive sense, 2 is certainly

complete as a poset, but we want to look at this in a more sophisticated way.

What we really want to be true if we say that a poset P is complete is that for

any other object A, the poset [A Â¡ P ], with the pointwise order, is complete.

!

In the case of 2, this means that [A Â¡ 2] is complete. To see why we want this

!

to be true, recall that an element of a set is essentially the same thing as a

function from a one-element set to that set. However, in categories thought of

as workspaces, it is more useful to think of any arrow with codomain S as an

element of S { a variable element of S. (A variable elements whose domain is a

terminal object is then a constant element or global element (2.7.19)). Categories

rich enough to be workspaces for a type of mathematics typically come with an

internal language; statements in that internal language can often be perceived

as statements about elements, but their truth is dependent on `elements' being

interpreted as variable elements.

In the case of ordinary set theory, it is still true that 2 is complete in this

internal sense. For computational semantics, the situation is diÂ®erent. Consider

the case A = N, although any inÂ¯nite set would do as well. A function N Â¡ 2 is

!

determined by and determines a subset of N. However, a computable function N

Â¡ 2 is determined by and determines a recursive subset of N. And it is well known

!

that the set of recursive subsets of N is not complete. It is not even countably

complete; in fact, the recursively enumerable subsets are characterized as the

countable unions of recursive subsets. Of course, arbitrary unions of recursive

subsets will be even worse.

5.3 Is a two-element poset complete? 65

5.3.2 Topos models The situation in an arbitrary topos is similar. A topos

has an object - with the property that for any object A, Hom(A; -) is the set

of subobjects of A. A topos also always has an object 2 = 1 + 1, and an arrow

A Â¡ 2 does not represent an arbitrary subobject, but rather a complemented

!

subobject (see 8.6.2). Such an arrow A Â¡ 2 gives a decomposition of A as a sum

!

A0 + A1 where A0 and A1 are the pullbacks shown below, where true; false : 1

Â¡ 2 are the two injections:

!

-A -A

A0 A1

? ? ? ?

- -2

1 2 1 true

false

The fact that a topos has universal sums implies that from 2 = 1 + 1 we can

conclude that A = A0 + A1 . On the other hand, if A = A0 + A1 , there is a unique

arrow A Â¡ 2 whose restriction to A0 is false Â± hi and to A1 is true Â± hi. Thus 2

!

is internally complete in a topos if and only if the supremum of complemented

sets are complemented. It is not hard to show that this is not true in general.

In fact, there is a topos in which the arrows from N to 2 are just the total

recursive two-valued functions (and in fact, the arrows from N to itself are also

the total recursive functions). In that topos a complemented subset of N is exactly

a recursive subset (one which, with its complement, has a recursive characteristic

function) and the fact that a union of recursive subsets is not recursive Â¯nishes

the argument.

In 6.6.4 we constructed a semantics for an If loop by constructing a supre-

mum in [A Â¡ D? ], where D? is a Â°at CPO (of which 2 is an example). However,

!

the last paragraph shows that in general this semantics does not make compu-

tational sense. The reason is that, although you can write down the sup as a

formal thing, it will not be guaranteed to give a terminating program. The sup of

partial functions exists, but the domain of such a partial function is not generally

computable.

In a topos model of computational semantics, in which all arrows N Â¡ N are

!

given by recursive functions, a subobject of N is determined by an arrow into -.

The maps into - cannot usually be computed. The one special case in which they

can is that of an arrow that factors through the subobject htrue; falsei : 2 Â¡ -.

!

This corresponds to the traditional distinction between recursively enumerable

and recursive subsets. In classical set theory, all subsets are classiÂ¯ed by arrows

into 2, but here only recursive subsets are.

66 Toposes

5.4 Presheaves

be a category. A functor E : op Â¡ Set is called a

!

5.4.1 DeÂ¯nition Let

presheaf on . Thus a presheaf on is a contravariant functor. The presheaves

on with natural transformations as arrows forms a category denoted Psh( ).

We considered presheaves as actions in Section 3.2. They occur in other guises

in the categorical and computer science literature, too. For example, a functor

F : A Â¡ Set, where A is a set treated as a discrete category, is a `bag' of elements

!

of A. If a 2 A, the set F (a) denotes the multiplicity to which a occurs in A. See

[Taylor, 1989] for an application in computing science.

The category of presheaves on a category form a topos.

5.4.2 Proposition

The proof may be found in [Barr and Wells, 1985] Section 2.1, Theorem 4.

That proof uses a diÂ®erent, but equivalent, deÂ¯nition of topos.

Â¡

!

5.4.3 Example Consider the category we will denote by 0 Â¡ 1. It has two

!

objects and four arrows, two being the identities. A contravariant set-valued func-

tor on this category is a pair of objects G0 and G1 and a pair of arrows we will

call source; target : G1 Â¡ G0 . The two identities are sent to identities. Thus the

!

category of presheaves on this category is the category of graphs, which is thereby

a topos. This category is the theory of the sketch for graphs given in 4.6.7.

We described the exponential object for graphs in 6.1.12. It is instructive to

see what the subobject classiÂ¯er is. We have to Â¯nd a graph - and an arrow

true : 1 Â¡ - such that for any graph and subgraph 0 Âµ , there is a unique

!

graph homomorphism Ã‚ : Â¡ - such that the diagram

!

- -

0

Ã‚

? ?

--

1 true

commutes.

We deÂ¯ne the graph - as follows. It has Â¯ve arrows we will call `all', `source',

`target', `both' and `neither'. The reason for these names should become clear

ñòð. 23 |