ñòð. 7 |

!

and I(f )[x] = [fx].

FL{2 If (f1 ; : : : ; fm ) and (g1; : : : ; gk ) are paths in a diagram in , both going

from a node labeled a to a node labeled b, and [x] 2 I(a), then

(If1 Â± If2 Â± : : : Â± Ifm )[x] = (Ig1 Â± Ig2 Â± : : : Â± Igk )[x]

in I(b).

Â¡

! is a diagram, ([x1 ]; : : : ; [xn ]) is a compatible family of ele-

FL{3 If D :

ments of I Â± D and p : q Â¡ D is a cone over D in , then [C(x1 ; : : : ; xn )]

!

is an element of I(q).

FL{4 If p : q Â¡ D and ([x1]; : : : ; [xn ]) are as in FL{ES 3, and x01 ; : : : ; x0n is a

!

compatible family of elements of I Â± D for which [xi ] = [x0i ] for i = 1; : : : ; n,

then

[C(x1 ; : : : ; xn )] = [C(x01 ; : : : ; x0n )]

FL{5 If p : q Â¡ D and ([x1]; : : : ; [xn ]) are as in FL{ES 3, then for i = 1; : : : ; n

!

[pi C(x1 ; : : : ; xn )] = [xi ]

FL{6 If p : q Â¡ D is a cone over D in

! and x 2 I(q), then

[x] = [C(p1x; : : : ; pn x)]

18 More about sketches

Compatibility implies that for any arrow u : i Â¡ j of

! ,

I(D(u))([xi ]) = [xj ]

As in 7.6.5, it follows that

I(pi )([C(x1 ; : : : ; xn )]) = [xi ]

for each i.

2.2.2 Binary trees We describe an FL sketch whose initial term algebra is the

set of binary trees of integers. We gave an FD sketch for binary trees in ES 1.3.11;

the sketch given here illustrates a diÂ®erent approach to the problem that opera-

tions such as taking the datum at the root or producing the left or right subtrees

are not deÂ¯ned on the empty tree.

We have the following basic nodes in the sketch: 1; t; t+ ; b; n. These should be

thought of as representing the types of binary trees, nonempty binary trees, the

Boolean algebra 2 and the natural numbers, respectively. We have the following

operations:

incl : t+ Â¡ t

empty : 1 Â¡ t

! empty? : t Â¡ b

! !

+ + +

val : t Â¡ n

! left : t Â¡ t

! right : t Â¡ t

!

zero : 1 Â¡ n

! succ : n Â¡ n

! true : 1 Â¡ b

!

and : b Â£ b Â¡ b

! not : b Â¡ b

!

The intended meaning of these operations is as follows: the constant emptyhi

is the empty tree; empty? is the test for whether a tree is the empty tree; incl

is the inclusion of the set of nonempty trees in the set of trees; val(T ) is the

datum stored at the root of the nonempty tree T ; left(T ) and right(T ) are the

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

The remaining operations are the standard operations appropriate to the natural

numbers and the Boolean algebra 2.

We require that

t+

Â¡ @

left Â¡ @ right

val

Â¡ @

Â¡

Âª ? R

@

t n t

2.3 The theory of an FL sketch 19

and

t+

Â¡ @

Â¡ @ incl

Â¡ @

Âª

Â¡ R

@

(2.1)

1 t

@ Â¡

not Â± true@ Â¡ empty?

@ Â¡

@

R Â¡

Âª

b

be cones and that

empty-

1 t

@

true@ empty?

@

R

@ ?

b

be a diagram.

In the cone (ES 2.1), there should be an arrow from the vertex to the node

b. It will appear in a model as either of the two (necessarily equal) composites.

Since its value is forced, it is customary to omit it from the cone; however, there

actually does have to be such an arrow there to complete the cone (and the

sketch). In omitting it, we have conformed to the standard convention of showing

explicitly only what it is necessary to show.

As in ES 1.3.11, the existence of the Â¯rst cone says that every nonempty tree

can be represented uniquely as a triplet

(left(T ); val(T ); right(T ))

The fact that (ES 2.1) is a cone requires that in a model M , M (t+ ) be exactly

the subset of M (t) of those elements which evaluate to false under M (empty?).

2.2.3 Exercise

1. In the sketch for binary trees, show that for any model M , M (incl) is an

injective function. (Hint: use Diagram (ES 2.1).)

2.3 The theory of an FL sketch

Just as in the case of linear and FP sketches, every FL sketch generates a category

with Â¯nite limits in which it has a universal model.

20 More about sketches

2.3.1 Theorem Given any FL sketch , there is a category ThFL( ) with

Â¡ ThFL ( ) such that for any model M :

!

Â¯nite limits and a model M0 :

Â¡

! into a category with Â¯nite limits, there is a functor F : ThFL( ) Â¡

! that

preserves Â¯nite limits for which

(i) F Â± M0 = M , and

(ii) if F 0 : ThFL ( ) Â¡

! is another functor that preserves Â¯nite limits for

which F 0 Â± M0 = M , then F and F 0 are naturally isomorphic.

ThFL ( ) is deÂ¯ned up to equivalence by the following properties:

FLT{1 has all Â¯nite limits.

FLT{2 M0 takes every diagram of to a commutative diagram in .

FLT{3 M0 takes every cone of to a limit cone of .

ñòð. 7 |