ñòð. 5 |

This chapter develops the concept of sketch in several ways. The Â¯rst three sec-

tions describe a generalization of FP theories called FL theories which allow the

use of equalizers, pullbacks and other limits in the description of a structure.

These theories have expressive power which includes that of universal Horn the-

ories.

The last section gives further generalizations of the concept of sketch. These

generalizations are described without much detail since they do not appear to

have many applications (yet!) in computer science.

This chapter is needed only for Chapter ES 3, except that the sketch for

categories of Section ES 2.1.5 is required for Section ES 5.7.

2.1 Finite limit sketches

A cone is called Â¯nite if its shape graph is Â¯nite, meaning that it has only Â¯nitely

many nodes and arrows.

2.1.1 DeÂ¯nition A Â¯nite limit or FL sketch = ( ; ; ) is a Â¯nite graph

together with a Â¯nite set of diagrams and a Â¯nite set of Â¯nite cones. A model

of is a model of that takes all the diagrams in to commutative diagrams

and all the cones in to limit cones.

For historical reasons, FL sketches are also known as left exact sketches or

LE sketches.

In 7.2.8 we described the way the choice of products and terminal objects in a

model to represent the vertices of cones in a sketch were irrelevant but could result

in the technicality that, for example, the set representing the product might not

actually be a set of ordered pairs. The same sort of statement is true of models

of FL theories. In particular, in a model the equalizer of parallel arrows need not

be a subset of their common domain.

FL sketches allow the speciÂ¯cation of structures or data types with sorts

that include equationally speciÂ¯ed subsorts, by using equalizers. More generally,

you can specify an operation whose domain, in a model, will be an equationally

deÂ¯ned subobject of another sort. FL theories can express anything expressible

by universal Horn theories, but in general FL theories are more powerful (see

[Barr, 1989] and [AdÂ¶mek and RosiÂ·ky, 1994], pages 209-210). For example, small

a c

categories and functors form the category of models of an FL theory (which we

12

2.1 Finite limit sketches 13

give in ES 2.1.5 below) but not of a universal Horn theory. Categories of models

of FL sketches can be described axiomatically as locally Â¯nitely presentable

categories (see [Gabriel and Ulmer, 1971] and [AdÂ¶mek and RosiÂ·ky, 1994]).

a c

In practice it is generally suÂ±cient to restrict the types of cones to a few

simple types, products, pullbacks and equalizers. In principle, an FL sketch can

always be replaced by one which has an equivalent category of models and which

has only these three types of cones, but there might be some case in which this

is not the most eÂ±cient approach.

2.1.2 Other approaches In the introduction to Chapter 7, we mentioned

three approaches to formalization: logical theories, signatures and equations, and

sketches. Systems equivalent to FL sketches have been developed for both the

other approaches. Coste [1976], Cartmell [1986] and McLarty [1986] generalize

logical systems and Reichel [1987] generalize signatures. The book by Reichel has

many examples of applications to computer science.

2.1.3 Notation for FL sketches We extend the notational conventions in

Section 7.3 to cover products, pullbacks and equalizers.

First, the notation of N{2 in 7.3.1 using product projections is extended to

cover the arrows from the limit to any of the nodes in the diagram: that is they

are all denoted by an appropriate p; moreover, the notation of N{4 in 7.3.1 is

extended to arrows into the limit in terms of the composite with the projections.

See Example ES 2.1.5 below of the sketch of categories to see how this is used.

Of course, it is sometimes necessary to be more explicit than this.

We add the following to the notational conventions of Section 7.3.

N{8 If we have a node labeled a Â£c b this implies the existence of a cone

a Â£c b

Â¡ @

Â¡ @

Â¡ @

Â¡

Âª R

@

- cÂ¾

a b

Of course, this notation is not self-contained since it is necessary to specify

the arrows a Â¡ c Ãƒ b. In many cases, these arrows are clear, but it may be

!Â¡

necessary to specify them explicitly.

!

N{9 If we have an arrow labeled s : a )Â¡ b (recall from 2.8.2 that in a category this

notation means an arrow that is a monomorphism), then we are implicitly

including a cone

14 More about sketches

a

Â¡ @

id Â¡ @

s id

Â¡ @

Âª

Â¡ ? R

@

- bÂ¾

a a

s s

This notation makes sense because of Theorem 8.3.3.

We could go on and turn our notational conventions into a formal language, but have

chosen not to do so because we do not know what it would add to the theory. For

us, they remain a set of notational conventions; the real object of study is the whole

sketch or else the theory it generates.

2.1.4 The sketch for simple graphs Here is a simple example that shows

how the added power of FL sketches can be used to deÂ¯ne a familiar type of

structure. A simple graph is a graph with the property that for any pair (a; b)

of nodes there is no more than one arrow with source a and target b.

The sketch for graphs has the graph

source

a Â¡Â¡ Â¡ ! n

Â¡Â¡

Â¡Â¡ Â¡ !

Â¡Â¡

target

and no cones or diagrams. We can modify it to get a sketch for simple graphs

by adding an object n Â£ n and the necessary discrete cone to make it a formal

product, an arrow u : a )Â¡ n Â£ n (hence adding a formal pullback as in N{ES 9

!

making it formally monic) and also the diagram (not cone)

a

Â¡ @

source Â¡ u @ target

Â¡ @

Â¡

Âª ? @

R

Â¾ nÂ£n p - n

np

1 2

The eÂ®ect of this is to make the monic arrow u become hsource; targeti in a model,

so that no two arrows can have the same source-target pair.

2.1.5 The sketch for categories We give here an FL sketch whose models

in the category of sets are small categories and arrows between the models are

functors. Models in an arbitrary category with Â¯nite limits are called category

objects in . These are used in Section ES 5.7.

The sketch has nodes c0 ; c1 ; c2 and c3 which stand for the objects, the arrows,

the composable pairs and the composable triples of arrows respectively. The

arrows of the sketch are:

u : c0 Â¡ c1

!

s; t : c1 Â¡ c0

!

2.1 Finite limit sketches 15

p1 ; p2 ; c : c2 Â¡ c1

!

p1 ; p2 ; p3 : c3 Â¡ c1

!

hp1; p2 i; hp2 ; p3 i; hp1 ; ci; hc; p3 i : c3 Â¡ c2

!

ñòð. 5 |