Specifications in mathematics and computer science are most commonly ex-pressed using a formal language with rules spelling out the semantics. How-ever, there are other objects in mathematics intended as specifications that are not based on a formal language. Many of these are tuple-based; for ex-ample the signature of an algebraic structure or the tuple specifying a finite state machine.
A sketch is another kind of formal abstract specification of a mathemat-ical structure; it is based on a graph rather than on a formal language or tuple. The semantics is often a functor; in other contexts it is a structure generalizing Goguen’s initial algebra semantics.
Each sketch generates a (categorical) theory; this theory is a category that in a strong sense contains all the syntax implied by the sketch.
4.6.1 Linear sketches We construct a hierarchy of types of sketches here and in Chapters 7, 8 and 10. Each new type uses additional categorical constructions to provide more expressive power than the preceding types.
What we can do now is describe a very simple type of structure using
‘linear’ sketches. It can describe multisorted algebraic structures with only
unary operations. If you are not familiar with multisorted algebraic struc-tures, it will not matter.
4.6.2 Definition Alinear sketchS is a pair (G,D) whereG is a graph andD is a collection of diagrams inG. Because of the motivating example of algebraic structures, the arrows of the graph of a sketch (not just a linear sketch) are often calledoperationsof the sketch.
4.6.3 Definition A model of a linear sketchS in a category C is a model (graph homomorphism)M :G −→C such that wheneverD:I −→G is a diagram inD, thenM ◦Dis acommutativediagram inC. The diagrams represent the equations which have to be true in all models.
We write M :S −→C for such a model. This use of the same symbol to denote both the sketch homomorphism and the graph homomorphism is a bit of notational overloading that in practice is always disambiguated by context. The collection of all models ofS inC is denotedMod(S,C).
A model of a sketchS inSetis (among other things) a set indexed by the nodes of the graph ofS as discussed in 2.6.11. IfM is a model andcis a node of the graph, an element ofM(c) is an element indexed by c, or an element of typec.
4.6.4 Definition A homomorphism of models of a linear sketch S, both models in the same categoryC, is a natural transformation between the models. For givenS andC, the models therefore form a category with natural transformations as arrows; this category is a full subcategory of the category of all graph homomorphisms fromG toC (which in general do not take the diagrams inD to commutative diagrams).
4.6.5 Example Any categoryE can be made into a linear sketch called theunderlying linear sketchof E, denotedU(E) (concerning this nota-tion, see 4.6.10 below), by taking for the diagrams the collection of all com-mutative diagrams in the category. A model of the underlying linear sketch E in some categoryC is the same as a functor on the original category: on the one hand, any functor takes any commutative diagram to a commuta-tive diagram and so is a model. On the other hand a modelM :S −→C of the underlying linear sketchS ofE preserves in particular all commutative diagrams of the form
A f -B
C
g◦f@@R ¡ª¡g (4.35)
4.6 Linear sketches 129 and so preserves composition as well as every commutative diagram consist-ing of a sconsist-ingle node and no arrows, and so preserves identities (see 4.1.6).
4.6.6 Example The linear sketch for u-structures has the graph with one node and one arrow as its graph, and no diagrams.
4.6.7 Example The construction in 4.2.7 gives thesketch for graphs.
Its graph is
a s
−−→−−→
t n (4.36)
and it has no diagrams.
4.6.8 Example We now consider an example of a linear sketch which has diagrams. Suppose we wanted to consider sets with permutations as struc-tures. This would be a u-structure (S, u) withua bijection. We can force u to go to a bijection inSet-models by requiring that it have an inverse. Thus the sketchP of sets with permutations has as graph the graphG with one nodeeand two arrowsuandv, together with this diagramD:
e u
−−→←−−v e (4.37)
based on the shape graph
i x
−−→←−−y j (4.38)
A modelM of this sketch in Set must have M(e) a set, M(u) and M(v) functions from M(e) to itself (since D(i) =D(j) =e), and because Dia-gram (4.37) must go to a commutative diaDia-gram, it must have
M(u)◦M(v) =M(v)◦M(u) = idM(e)
This says thatM(u) and M(v) are inverses to each other, so that they are permutations. Note that a model in any category is an object of that category together with an isomorphism of the object with itself and the inverse of that isomorphism.
If we had used as the only diagram the diagram with one node e and both arrows uandv, the result would have been a sketch in which any model M had the property thatM(u) andM(v) are the identity.
4.6.9 Example Suppose we wanted to have a linear sketch for graphs which have at least one loop at every node. We could try the following con-struction, which contains a mild surprise. The sketch has the graph (4.19), page 102 as its graph, with arrowss:N −→Aand idN :N −→Nadded. The an arrow. The commutativity of Diagram (4.39) forcesM(idN) to be idM(N) (see 4.1.6), and the commutativity of the diagrams (4.40) forces the source and target ofM(s)(n) to ben, so thatM(s)(n) is a loop onn.
The surprise is that a homomorphism α:M −→M0 of models of this sketch must take the particular loopM(s)(n) to M0(s)(αN(n)). Of course, any homomorphism of graphs will take the loop M(s)(n) tosome loop on αN(n), but our homomorphisms are stricter than that. So what we really have are graphs with adistinguished loop at every node and homomorph-isms which take distinguished loops to distinguished loops. These are called reflexivegraphs. A node in a reflexive graph may have other loops but they are not part of the given structure.
If you want a sketch for graphs which have a loop on every node, but not a distinguished loop (so that a homomorphism takes the loop onn to some loop onαN(n), but it does not matter which one), you will have to wait until we can study regular sketches in Section 10.4.
4.6.10 Homomorphisms of linear sketches Ahomomorphism of lin-ear sketchesfromS = (G,D) toS0= (G0,D0) is a graph homomorphism φ:G −→G0 with the property that if D:I−→G is a diagram inD, then φ◦D :I−→G0 is a diagram in D0. It is easy to check that this definition makes linear sketches and their homomorphisms into a category.
Note that here we are defining homomorphisms between possibly different sketches, whereas in Definition 4.6.4 we defined homomorphisms between two models of a sketch.
If F : C −→C0 is a functor between categories, the underlying linear sketch homomorphism U(F) : U(C)−→U(C0) is F regarded as a
homo-4.6 Linear sketches 131 morphism of graphs. Since it takes any commutative diagram in C to a commutative diagram inC0, it is a homomorphism of linear sketches.
We have already used the symbolU(E) to denote the underlying graph of a category E in 3.1.10. Here, we use it to denote the underlying linear sketch. In this text, we disambiguate such notation by using phrases such as ‘the underlying graphU(E)’. In a situation where one needed frequently to refer to several different underlying functors from the same category, one could introduce heavy notation such asUGrfCat.
4.6.11 The theory of a linear sketch You can reverse 4.6.5: given a linear sketchS, there is a category Th(S), thetheory of S, which has a universal model M0 of S in this sense: M0 : S −→U(Th(S)) is a model, and for any other modelM :S −→U(C), there is a unique functor F :Th(S)−→ C such that U F ◦M0 =M. Since U F is a model of the underlying sketch of the categoryTh(S) (see 4.6.5),M0induces a bijection between models of S and models of its theory (functors from Th(S) to Set). This bijection is in fact part of an equivalence of categories between Mod(S,Set) and the functor category Func(Th(S),Set).
Th(S) satisfies the following requirements:
LT–1 Every arrow ofTh(S) is a composite of arrows of the formM0(a) for arrowsaofS.
LT–2 M0 takes every diagram ofS to a commutative diagram inTh(S).
4.6.12 Construction of the theory of a linear sketch Let S be a linear sketch. The idea behind the construction ofTh(S) is: ‘Freely compose the arrows of G and impose the diagrams as equations.’ Formally, begin with the free categoryF(G) generated by G and construct Th(S) and a functorQ:F(G)−→Th(S) which make all the diagrams inD commute as described in 4.1.13. The universal modelM0:G −→U(Th(S)) isU Q◦ηG (see 3.1.14); it takes each node to itself and each arrow to its congruence class inTh(S).
That M0 has the property claimed in 4.6.11 follows by considering this diagram for a given modelM :G −→UC:
For a givenM, it follows by Proposition 3.1.15 that there is a unique func-torMcfor which the left triangle commutes. Then by Proposition 3.5.4 (see
also 4.1.13) there is a unique functorF0: Th(S)−→C making the right hand triangle commute. ApplyU to the right hand triangle, put them to-gether and letM0=U Q◦ηG. Then we have a commutative triangle:
G M0 -UTh(S)
UC M
@@
@@R
U F0
¡¡
¡ª¡
(4.42)
This shows the existence and we leave the uniqueness to the reader.
The construction of a semantics functor for a functional programming language illustrated in 3.5.9 is a special case of the construction just given.
4.6.13 Examples The theory which is generated by the underlying linear sketch of a category is isomorphic to the category itself (Exercise 3). The sketch for u-structures (see 4.2.5 and 4.6.6) generates a category with one node u0, its identity arrow, and arrows e, e◦ e, e ◦ e◦ e, and so on, all different because there are no equations to make them the same. In other words, it has one arrowen for each natural numbern.
The theory for the sketch for graphs (its graph is 1.3.9 and it has no diagrams) has only two arrows besides those in the graph 1.3.9, namely the identity arrows inaandn. That is because the two arrows of the graph do not compose with each other.
The sketch for permutations in 4.6.8 is more complicated. It has one node eand arrows un for all positive andnegative integers n. This is essentially becausevmust be u−1in the theory; see 4.7.13 for more details.
The reader may wonder why the term ‘linear sketch’ is appropriate. One way of thinking of linear sketches is that they are exactly the sketches for which the following are true:
(i) IfM1 andM2are models in the category of sets, then there is a model M1+M2defined by setting (M1+M2)(a) =M1(a)+M2(a),a∈G0(S).
(S+T is the disjoint union of setsS andT.)
(ii) IfM is a model and X is a set, there is a model X×M defined by setting (X×M)(a) =X×M(a),a∈G0.
The linear sketches with constants that we will consider in Section 4.7 below lack these ‘linearity’ properties. They should perhaps be called affine sketches.
For the reader familiar with equational theories we observe that linear sketches have only unary operations while linear sketches with constants have, in addi-tion, nullary operations.