ñòð. 4 |

z of type b and c, respectively, and cones forcing b and c to be terminal. Now

there are two initial models, one in which s(x) = y and another in which s(x) = z.

Since there is a model in which s(x) 6y, there can be no equation that forces

=

s(x) = y and there is similarly no equation that forces s(x) = z. But one or the

other equation must hold in any model.

1.3.9 Example It is well known and proved in abstract algebra texts that the

initial Â¯elds are (a) the rational numbers and (b) the integers mod p for each

prime p. (The word for initial model in these texts is `prime Â¯eld'.) A Â¯eld is in

1.3 Term algebras for FD sketches 9

the component of the integers mod p if and only if 1 + 1 + : : : + 1 (sum of p 1's)

is zero. These Â¯elds have confusion. Otherwise the Â¯eld is in the component of

the rational numbers, which have no confusion (nor junk). Duval and Reynaud

[1994a, 1994b] show how to implement simultaneous computation in the initial

algebras for a Â¯nite discrete sketch for Â¯elds.

The real numbers and the complex numbers form Â¯elds with the usual oper-

ations. The irrational real numbers constitute junk.

1.3.10 Example The example in ES 1.1.2 has only one component and hence

a single initial model in which all sorts are empty except the singleton 1. If you

add constants to d, the initial model is just the set of lists of Â¯nite length of

elements of d. In the model discussed there which also has all inÂ¯nite sequences,

the inÂ¯nite sequences are junk.

1.3.11 Binary trees We now describe a sketch for ordered rooted binary trees

(called trees in this discussion). `Binary' means that each node has either no

children or two children, and `ordered' means that the children are designated

left and right. This is an example which uses cocones to treat exceptional cases,

in this case the empty tree.

Trees are parametrized by the type of data that are stored in them. We will say

nothing about this type of data, supposing only that it is a type for which there

is an initial model. The way in which the parametrized data type is Â¯lled in with

a real one is described, for example, in Section ES 3.2. We would like to thank

Adam D. Barr for helpful discussions on how binary trees operate (especially

their error states) on real machines.

The sketch will have sorts 1; t; s; d. Informally, t stands for tree, s for

nonempty tree and d for datum. We have the following operations:

empty : 1 Â¡ t

!

incl : s Â¡ t

!

val : s Â¡ d

!

left : s Â¡ t

!

right : s Â¡ t

!

The intended meaning of these operations is as follows.

Emptyhi is the empty tree; incl is the inclusion of the set of nonempty trees in

the set of trees; val(S) is the datum stored at the root of S; left(S) and right(S) are

the right and left branches (possibly empty) of the nonempty tree S, respectively.

We require that

10 Finite discrete sketches

s

Â¡ @

Â¡ @

@ right

left Â¡ val

Â¡ @

Âª

Â¡ ? R

@

t d t

be a cone and that

1 s

@ Â¡

Â¡ incl

empty@

@ Â¡

@

R Â¡

Âª

t

be a cocone.

There are no diagrams.

The cocone says that every tree is either empty or nonempty. This cocone

could be alternatively expressed t = s + femptyg. The cone says that every non-

empty tree can be represented uniquely as a triplet (left(S); val(S); right(S)) and

that every such triplet corresponds to a tree. Note that this implies that left, val

and right become coordinate projections in a model.

Using this, we can deÂ¯ne subsidiary operations on trees. For example, we can

deÂ¯ne an operation of left attachment, lat : t Â£ s Â¡ s by letting

!

lat(T; (left(S); val(S); right(S))) = (T; val(S); right(S))

This can be done without elements: lat is deÂ¯ned in any model as the unique

arrow making the following diagram commute (note that the horizontal arrows

are isomorphisms):

M (t) Â£ hleft; val; righti-

M (t) Â£ M (s) M (t) Â£ M (t) Â£ M (d) Â£ M (t)

hp1 ; p3 ; p4i

lat

? ?

- M (t) Â£ M (d) Â£ M (t)

M (s)

hleft; val; righti

In a similar way, we can deÂ¯ne right attachment as well as the insertion of a

datum at the root node as operations deÂ¯nable in any tree. These operations

are implicit in the sketch in the sense that they occur as arrows in the theory

generated by the sketch (see 4.6.11), and therefore are present in every model.

1.3.12 Proposition Supposing there is an initial algebra for the data type,

then the category of binary trees of that type has an initial algebra. If the data type

has (up to isomorphism) a unique initial algebra, then so does the corresponding

category of binary trees.

1.3 Term algebras for FD sketches 11

Proof. We construct the initial algebra recursively according to the rules:

(i) The empty set is a tree;

(ii) If Tl and Tr are trees and D is element of the initial term algebra for the

data type, then (Tl ; D; Tr ) is a nonempty tree;

(iii) Nothing else is a tree.

This is a model M0 deÂ¯ned by letting M0(s) be the set of nonempty trees,

M0 (t) = M0 (s) + f;g and M0 (d) be the initial model of the data type. Here `+'

denotes disjoint union. It is clear how to deÂ¯ne the operations of the sketch in

such a way that this becomes a model of the sketch.

Now let M be any model with the property that M (d) is a model for the data

type. Then there is a unique morphism f(d) : M0 (d) Â¡ M (d) that preserves

!

all the operations in the data type. We also deÂ¯ne f (t)f;g to be the value of

M (empty) : 1 Â¡ M (t). Finally, we deÂ¯ne

!

f(s)((Tl ; D; Tr )) = (f (t)(Tl ); f (d)(D); f (t)(Tr ))

where f (t) is deÂ¯ned recursively to agree with f (s) on nonempty trees. It is

immediately clear that this is a morphism of models and is unique. In particular,

if the data type has, up to isomorphism, only one initial model then M0 is also

unique up to isomorphism.

1.3.13 In Pascal textbooks a deÂ¯nition for a tree type typically looks like this:

type TreePtr = bTree;

Tree = record LeftTree, RightTree : TreePtr;

Datum : integer

end;

Note that from the point of view of the preceding sketch, this actually deÂ¯nes

nonempty trees. The empty tree is referred to by a null pointer. This takes ad-

vantage of the fact that in such languages deÂ¯ning a pointer to a type D actually

deÂ¯nes a pointer to what is in eÂ®ect a variant record (union structure) which is

either of type D or of `type' null.

1.3.14 Exercise

y is an FD sketch and f : M Â¡ N is a homomorphism

!

1. a. Show that if

between models in the category of sets, then the image of f is a submodel of N .

b. Show that every model in the category of sets of an FD sketch has a smallest

submodel.

2

ñòð. 4 |