Home

SKETCHES AND SPECIFICATIONS USER'S GUIDE First part: Wefts

1. C c 2 D 2 U S wa wD wu NT A realization of S towards is an arrow from S towards A which satisfies every constraint of S Then as usual we write w S A though S and A belong to two distinct categories is a point of A whereas S is a point of Weft A Although the category A can be identified to the subcategory Weft 4 of Weft A a realization of S towards A is not an arrow in Weft A except when S has level 0 It is easy to check the compatibility of realizations at various levels and to define the set Real 1 S of realizations of any level of S towards A Let S S be an A weft homomorphism Then we define Real 0 A Real S A Real 1 S A as the map which assigns to each realization w of S towards A the realization woo of S towards A In this way we get a contravariant functor Real 1 A Weft A Set Let S be a weft of ambigraphs The elements of Real 4n S Set i e the realizations of S towards Set are called the set valued realizations of S If S is an A weft A a point of A and w a realization of S towards A then we say that S specifies w with respect to A and A Actually such a good notion of realizations is half what is needed for a specification tool The second half is a good formalization of programs It will be seen in guide3 that indeed A wefts can be used to describe functional programming Example 8 Let S be a weft of ambigraphs w
2. CES CDU it can be represented as follows coa 2 D 2 U x Y This drawing represents both the potential c2D 5u in Weft A and the body CSS in A which are related through the A weft homomorphism C gt C in Weft A When the potential has level 0 then C C and the whole diagram is in the category A In this case it is possible to simplify the drawing as was done in 2 2 c s More generally for any level of the potential this drawing can be used recursively to get a diagram which is entirely in the category A see example 6 The word weft derives from these 6 D U diagrams Of course it is easy to generalize these drawings to several constraints 2 WEFTS 13 Example 5 By adding the constraint U I of level 0 to the ambigraph Gs resp Gsp in example 1 we get a weft of ambigraphs of level 1 Ambi WEFT Ss Ambi WEFT Ss p support Gs support Gsp terminal point U terminal point U S Sap Both these examples correspond to the following diagram in Ambi YT Dr or Cr ceo Gs or Gs p Ur Example 6 Let us consider once more the weft of ambigraphs S from example 5 it allows us to characterize in a way that will be made precise below by the definition of realizations the sets which are endowed with an element and a unary operation However it is far from enough to characterize the set of natural numbers we must add the information that it is freely ge
3. lt pos idn U N 3 5 About wefts and sketches Projective sketches are a special kind of wefts Comp wefts with limit constraints and the models of a projective sketch are its set valued realizations However projective sketches will play a very specific role among wefts since they will sketch wefts More precisely we will consider A wefts for categories A which are projectively sketchable i e such that A Mod E for some projective sketch E This is the reason why we have introduced for dealing with wefts a terminology which is different from the usual one for sketches The table below sums up these SKETCHES WEFTS A is a category and A is a point of A projective sketch A weft E S differences model of E realization of S towards A 1 E Set w S A the category the set Mod E Real S 4 BLOWING UP PROJECTIVE SKETCHES 27 4 Blowing up projective sketches According to 2 the A wefts for any category A can be used for specifying Quite often A is the category Ambi of ambigraphs According to 3 the category Ambi is projectively sketchable it is equivalent to the category Mod E Ambi of models of the projective sketch E Anvi In guide2 we will consider A wefts for other categories A which will also be projectively sketchable i e equivalent to Mod F for some projective sketch F We will focus on the special case where there is a homomorphism p F gt E wi The simplest among th
4. E u E is replaced by its sagittal diagram Definition 11 The blow up of E by u is the following compositive graph El y e its points are the E x where E is a point of E and z n E e its arrows resp its identity arrows are the e x E E x where e E E is an arrow resp an identity arrow of E x E and 1 pu e x u E e a pair of consecutive arrows e1 11 e2 2 is composable in El y if and only if the pair of arrows e1 2 is composable in E and then ez 2 o e1 11 e2 o e1 z1 In the notation e1 21 e2 2 for a pair of consecutive arrows x2 is redundant since z2 p e1 x1 This is why we denote e1 2 11 ler x1 e2 tal Let x Cp B E be a B projective cone of E For all element x of u x C where C is the vertex of Cp B let us consider the B projective cone x x of El y defined as follows e the image of the vertex C of C is the point y C x of El y e the image of a point B of B is the point x B x pg x of EA y e the image of an arrow b B B of B is the arrow x b x p8 x of El y e and the image of a projection arrow pg C B of C is the arrow x pg x of El y Definition 12 The blow up of E by p is the projective sketch El y with support the compos itive graph E u and with distinguished projective cones the x x where x is a distinguished projective cone of E and x u x C
5. grammes 18 pp CL1 CL47 1987 Lair 93 Christian Lair El ments de th orie des patchworks Diagrammes 29 pp CL1 CL29 1993 Lellahi 89 S K Lellahi Categorical abstract data types Diagrammes 21 pp SKL1 SKL23 1989 Also S K Lellahi Types abstraits cat goriques Une extension des types abstraits alg briques Rapport de recherche 063 Universit de Paris Sud Orsay Laboratoire ISEM 1987 Mac Lane 71 Saunders Mac Lane Categories for the working mathematician Graduate Texts in Mathematics 5 Springer Verlag 1971 Wells amp Barr 88 Charles Wells and Michael Barr The formal description of data types using sketches In M Main et al editor Mathematical Foundation of Programming Language Semantics pp 490 527 Springer Verlag 1988 Lecture Notes in Computer Science 298 Wirsing 90 Martin Wirsing Algebraic specifications In J van Leeuwen editor Handbook of Theoretical Computer Science chapter 13 pp 675 788 Elsevier 1990 CONTENTS Contents 1 2 Introduction Wefts 2 1 2 2 2 3 2 4 2 5 2 6 Ambipraphs Let LAS al san is kA GS RS ange eee ee An example of a constraint Constraints aies es A a a Ra eel MEN ae ee Wefts and weft homomorphisms Re alizations Of a weit uses sn ego de SO pee lie hs Ag gui Eunctorialit y Of Wefts ps een eS ARE SN A A Se iet Projective sketches 3 1 3 2 3 3 3 4 3 9 A com
6. For all integer n gt 1 assume that we know the category Weft _ A of A wefts of level lt n 1 as well as the functor Supp y Weft A gt A An A weft S of level lt n is made up of a point Supp S of A called the support of S and a set of constraints over Supp S in the category Weft _ A called the constraints of S An 2 WEFTS 12 A weft homomorphism a S S of level lt n is an arrow Supp 0 from Supp S to Supp S in A such that for all constraint Supp C Supp S cpu of S the body Supp 0 o x Supp 1 C Supp S together with the same potential cpu is a constraint of S In this way we get the category Weft A of A wefts of level lt n with the support functor Supp Weft A A It is easy to check that Weft A is a subcategory of Weft A hence A is a subcategory of Weft A The union or more exactly the inductive limit as defined in A 6 of the categories Weft A for n N is the category of A wefts Weft A Since the support functors Supp are compatible they define a functor Supp Weft A A Another notation is used for supports for an A weft S we write S for Supp S and for an A weft homomorphism o we write a or just o for Supp c Since S is a point of A it is also an A weft of level 0 The fact of adding constraints to S in order to get the A weft S is an A weft homomorphism DS When S has exactly one constraint
7. and that it is the only one up to isomorphism Hence Ss ini specifies precisely the natural numbers Example 10 Let S be a weft of ambigraphs with a sum constraint x Cg gt S example 4 Let w be a set valued realization of S It follows from the definition above that up to isomorphism e the set w x C is the disjoint union of w x C1 and w x C2 and the maps w x c1 and w x c2 are the inclusions So a set valued realization w of the weft of ambigraphs Se from example 7 is characterized up to isomorphism by a non empty set w H with a special element e image of the one element set w H by the map w h Then the image of the set w H by the map w h is the complement of e in w H In other words if LU denotes the disjoint union w H is equal to w H U e AS Ieee Sa wae et In general given an A weft S and a point A of A it is possible to define many notions of homomorphisms between the realizations of S towards A among which none is more canonical than the others see Lair 93 However in some special and important cases there is a natural definition for such homomorphisms we will see in 3 that this is the case when S is a projective sketch this remains true when S is any sketch 2 6 Functoriality of wefts The definition of A wefts is such that any functor on the category A gives rise to a functor on the category Weft A of A wefts For example as soon as a functor is defined on ambigraphs we
8. map f X X such that f x1 x4 f x2 23 x The sagittal diagram of f is the directed graph made up of points E x for from 1 to 3 points E x for i from 1 to 4 and arrows e x E xi E f xi for from 1 to 3 Now let us consider the following directed graph G map Then f defines a model Tf of G Map Tp x ew and the blow up Gmap Zf of G map by this model is precisely the sagittal diagram of f Similarly the blow up of Emo by an ambigraph G counts each point Pt Ar etc of E mo as many times as the number of elements in the set G Pt G Ar etc For instance the blow up of E Amb by the ambigraph 9 replaces the point Pt of E Amb by three points Pt Eo Pt Es and Pt Ez Finally a fundamental theorem allows us to characterize the models of a projective sketch which is defined as a blow up To sum up in this paper we define and study two levels of specification 1 INTRODUCTION 4 1 the first level is made of wefts which specify their realizations 2 the second level is made of projective sketches which sketch their models The link between both levels is that we focus on A wefts for a category A which is equivalent to the category of models of a projective sketch E In the simplest cases corresponding to functional programming E is E qnp so that A Ambi is the category of ambigraphs Other projective sketches among which blow ups of E Ambi will be use
9. yr and r YT or Cr Dr Gs An ambifunctor w Gs Set satisfies I r if and only if with we w o x Cr Set Ur e for all ambifunctor wp from Dr to Set such that wp o yr we there exists a unique ambifunctor wy from Ur to Set such that wy or wp Cr a Dr i Ur A yr a Set Henceforth w satisfies Py if and only if w U is a terminal set i e a one element set as required VX wp D wu D assou w U we C wp C wu C In the following we define A wefts and their realizations in such a way that if we add to Gs this constraint Ty we get an Ambi weft S example 5 whose set valued realizations are the ambifunctors w from G to Set such that w U is a one element set As a consequence the ambifunctor M from Gs to Set is a set valued realization of S 2 3 Constraints Let us consider a category W and a functor Supp W A For example W can be the category A itself and Supp the identity Later W will be a category of A wefts and Supp will be the support functor Definition 2 Let W be a category Supp W Aa functor and Ap a point of A A constraint T over Ag relative to Supp W A is made up of e three points C D and U of W 2 WEFTS 11 e a pair of consecutive arrows CDU of W e and an arrow Supp C gt Ao of A The arrow y is the body of the constraint and the pair of consecutive arrows y 9 is its potential In such a constraint x y 6 the b
10. 48 extension 6 34 45 factorisation 49 51 fibration 30 functor 45 homomorphism 12 21 35 44 45 identity arrow 45 indexation 27 34 induction 51 inductive cone 51 inductive factorisation 51 inductive limit 52 ingredient 22 initial point 52 isomorphism 45 left exact 41 limit inductive cone 51 limit projective cone 20 49 loose homomorphism 35 map 6 model 21 monomorphism 51 morphism 45 nature 22 natural isomorphism 47 natural transformation 46 objects 45 pair of composable arrows 45 pair of consecutive arrows 44 point 21 44 potential 11 product 50 projection 48 projective cone 20 48 projective factorisation 49 projective limit 49 projective sketch 21 pullback 50 pushout 53 rank 44 realization 14 satisfaction 15 selection of identities 45 set valued realization 15 set valued span 40 sketch 21 22 sum 52 support 11 21 terminal point 49 triangle 27 typical base 48 51 typical inductive cone 51 typical projective cone 20 48 vertex 44 48 51 weft 11 Yoneda counter model 38 Yoneda functor 38 57
11. French trames and to show how they can be used for specification issues in computer science Moreover in guide2 and guide3 wefts will be extended to mosaics in order to deal with implicit features of computer languages including the notion of state Here and in guide2 we focus on the realizations of the wefts and mosaics which give them their meaning Programs are considered in guide3 wefts provide a good frame for functional programming while mosaics extends it to imperative programming This paper is part of a general study of some applications of Ehresmann s sketch theory to computer science along with the reference manual ref No prerequisite is assumed to read it 1 INTRODUCTION 1 1 Introduction Specifications are used in industry in order to design software The client s requirements are used in order to build a specification which in turn is used for making and testing the imple mentation Hence the aim of a specification is twofold it must help to clarify the requirements and to check that the software does meet them Among the range of specifications are algebraic specifications Goguen et al 78 Wirsing 90 Astesiano et al 99 With each algebraic specification are associated on one side its models and on the other side its terms Models are used to check that the problem is well posed and terms are used to describe programs and evaluation processes at least in functional or applicative languages lik
12. The fibration E u E u E is the homomorphism of projective sketches defined as e E x1 gt E for all point E of E and all x u E e le x gt e for all arrow e of E and all x u dom e note that the domain of an arrow e of E is often denoted dom e rather than E dom e Consequently the fibration satisfies 4 BLOWING UP PROJECTIVE SKETCHES 31 e e e2 11 gt e1 e2 for all pair of consecutive arrows e1 e2 z1 of E and all x dom e1 For example if E x1 v2 v3 and u E x1 75 and ue is such that 21 gt 2 2 gt 13 and 23 gt 23 then Ey Ey Let h u y be a homomorphism of models of E The homomorphism of projective sketches E h EA y El y is defined by E h e x e h x It is easy to check that in this way we get a functor E Mod E Psk Example 15 The blow up of a projective sketch generalizes the usual sagittal diagram of a map Indeed for all map f X X the blow up EmapYZf Of Exp by Tf see example 12 is precisely the sagittal diagram of f PROJECTIVE SKETCH Ep Zf points E x for all x X E 11 for all x X arrows e x E x E f x for all x X Example 16 Here is the blow up of Epir by Pir see example 13 PROJECTIVE SKETCH Epir Zpart points Pt I Ar part Ar tot arrows dom part codom part Ar part Pt I dom tot codo
13. Ya e the homomorphism Z dom Z Pt Z Ar is defined by Pt Y gt Pt Ya e the homomorphism Z codom Z Pt Z Ar is defined by Pt Y gt Pt YQ More generally the table below draws the ambigraph Y E and the projective sketch Z E for all point E of E Ambi For all arrow e E E of E Ambi it is then easy to determine the ambifunctor Y e Y E Y E and the homomorphism Z e Z E gt Z E Actually in this table only the directed graph sublying Z E is drawn however constraints are suggested in the following way monomorphisms are drawn as gt gt and the projections from both distinguished cones P compp and gg are drawn as gt and cees gt respectively With these conventions the directed graph sublying E ww is the following one IdA ConsP lt lt CompP yS Y O pe fe A A Po 3 ho RankP lt Eq Here is the table of the interpretation of the points of E Ambi by Y Ve amai Eambi t Ambi and by Z Emo Psk 4 BLOWING UP PROJECTIVE SKETCHES 40 3 It is easy to check that Y is a counter model of E Ambi and that Z is not a counter model of E Anvi for example the homomorphism Z jraar Z Ar Z IdAr is not an epimorphism Theorem 1 states that the categories Mod Z Ar and Mod E moi Y Ar are equivalent We now check directly that the set of models of Z Ar is in one to one correspondence with the set of indexations of ambigraphs b
14. a Dpart indexation where Di is the following directed graph DIRECTED GRAPH T point I arrows part I 1 tot 1 I 0 T part part o The Z part indexation of the directed graph sublying to Func is the following HOMOMORPHISM Abus Func T points X gt I for all set X arrows f gt tot for all total function f ft part for all partial function f art Let us now consider the directed graph Ge and its T indexation hga DIRECTED GRAPH G2 points U WN arrows z U N s N gt N p N N HOMOMORPHISM hf Go gt Thon points U Nel arrows z gt tot s tot pr part 4 BLOWING UP PROJECTIVE SKETCHES 29 Let k be any homomorphism of directed graphs from Ge towards the category Func then the interpretation of the arrows z s and p by k are arbitrary functions Now more precisely let k bea T triangle from ne towards Dats then the interpretation of the arrows z and s by k are total functions whereas the interpretation of p is a partial function art k Gee Func SS oe Tai Example 14 Let us try to go further by adding equations to the example above For this purpose the directed graph Z can be extended by the following ambigraph Lpart par AMBIGRAPH Zyart extends Dari identity arrow tot idr composed arrows tot o tot tot part o part part o tot tot o part part equations tot tot part part The identity arrow of Zpart means that
15. cone A homomorphism of models of E is a natural transformation see A 4 between the sublying functors The definition of a homomorphism A 1 u2 of models of E does not involve the dis tinguished projective cones of E it is a family of maps h E E pa E for all point E of E such that po e o h E1 h E2 o pue for all arrow e Ey Es of E However such a homomorphism behaves well with respect to distinguished projective cones of E indeed the property of projective limits ensures that given a distinguished projective cone x C B E of E the restriction of h to the image of B determines h upon the image of the whole C B The models of E are the points and the homomorphisms between these models are the arrows Of the category Mod E 3 PROJECTIVE SKETCHES 22 Let p E E be a homomorphism of projective sketches Then Mod p Mod E Mod E denotes the functor associated with p It maps each model u El Set to the model p o p E Set In this way we get a contravariant functor Mod Psk Cat A model u of E is denoted pw E Set In a similar way a weft S of models of E i e a Mod E weft is denoted S E gt Set Definition 8 Let E be a point of E Let u E Set be a model of E An ingredient of y of nature E is an element of the set u E Let S E gt Set be a Mod E weft An ingredient of S of nature E is an ingredient of nature E of its sup
16. get a functor on wefts of ambigraphs Indeed the construction of A wefts is functorial in A This property will be used in guide2 in order to define the crown product for wefts from the crown product for their supports Precisely Let 9 A A be a functor between two categories A and A Then determines a functor Weft Weft A Weft A which respects the level of the wefts This functor Weft is defined recursively on the level 2 WEFTS 17 At level 0 Weft is just Let n gt 1 and assume that Weft is defined on the category of A wefts of level lt n 1 For all constraint T x y 0 of level lt n 1 over a point Ag of A let Weft B T denote the constraint of level lt n 1 on A with body P x and potential Weft y Weft d Then the image by Weft of an A weft S of level lt n is the A weft with support S and constraints the Weft T for all the constraints F of S 3 PROJECTIVE SKETCHES 18 3 Projective sketches A wefts were defined in 2 for any category A as well as the realizations which they specify In our examples the category A is the category Ambi of ambigraphs However we will see in guide2 and guide3 that other categories may prove useful Let us consider once more the category Ambi According to its definition an ambigraph G is made up of sets G Pt G Ar etc and maps G dom G Ar G Pt G codom G Ar G Pt etc which satisfy some p
17. pred gt part and predosucc gt tot but part o tot part tot so that this cannot define an ambifunctor A similar problem arises when we try to extend the indexation ae to the following ambigraph Gsp AMBIGRAPH Gs p 0 extends Gsp equation pos idy in Let hsp Gsp Lpart be an ambifunctor extending ho Since RE p N I we must have hsp idn id tot And since h pls tot and h p P part we must have hsp p o s part o tot part So it is impossible to define hsp po s idy in a way compatible with the projections of both members of the equation In other words it is impossible to extend he into an ambifunctor hsp Gsp gt Tpart 4 BLOWING UP PROJECTIVE SKETCHES 30 Both these problems come from the fact that by composing a total function and a partial function we generally get a partial function but not always This last point is not expressed by the composition part o tot part in Zpart and the composition part o tot tot would still be worse We will see in guide2 how it is possible to overcome this difficulty 4 2 Blow ups We now come to the definition of the projective sketch El y blow up of E by p For this purpose we first define the compositive graph Ely where each point E of E is counted as many times as there are ingredients of nature E in y for all point E of E all ingredient x of y of nature E gives rise to a point E x and for all arrow e E E of E the map ple
18. 47 e for all arrow g G1 Ga of G we have t G2 o 441 g ua g ot G1 in V t G1 Hi G1 H2 G1 9 Jato 11 Ga en 12 Ga It is also denoted G pi 2 y The functors from G to V are the points and the natural transformations are the arrows of a category Func G V In this category Func G V e the identity arrows are defined from the identity arrows of V for all functor u G V the arrow id is the natural transformation id u u defined by id G id a for all point G of G e the composition of arrows is defined from the composition of arrows in V let ti y po and t2 u2 u3 be two natural transformations between functors from G to V then the composed natural transformation tg o ty y u3 is defined by t2 ot1 G te G o t1 G for all point G of G From its definition an isomorphism of the category Func G V is a natural transformation ty 1 u2 such that there exists a natural transformation to y2 u which satisfies ta o t id and t ot2 1d ie which satisfies for all point G of G the equalities t2 G ot1 G idn G and t1 G o t2 G id a In other words t is an isomorphism of Func G V if and only if for all point G of G the arrow t G is invertible in V Then ti is called a natural isomorphism Let V be a category We have defined in A 3 the contravariant functor Homcomp V Comp gt Set From above for all compositive graph G the set Ho
19. L C Ilse n B or L C B x x Bn when B B Bn The property of the product can be stated as follows e for all point V of V and all set of arrows vg V gt n B for B B there is a unique arrow v V gt II n B BEB such that L pp o v vg for all Be B When Y is the category of sets it means that seg n B is up to bijection the cartesian product of the sets 7 B and the maps L pp are the canonical projections Pullback When the typical base B is made up of two arrows with the same codomain say b B Bo and bz B2 Bo and maybe some identity arrows the projective cone Cp B has three projections pp C B1 pg C B2 and pg C Bo such that b1 o pp pB and b2 o pp pB so that pg is determined by pp pp and B and can be forgotten BB Then L is called the pullback of n or sometimes the pullback of 7 B1 and n B2 above Bo If we denote L C n B1 x 85 n B2 the property of the pullback can be stated as follows e for all pair of arrows v V By and va V n B2 such that n b1 o v n b3 o va there is a unique arrow v V gt Bi Xn Bo B2 such that L pp o v v and L pp ov vz When Y is the category of sets it means that 7 B1 x p n B2 is up to bijection the set v of pairs x1 2 N B1 x n B2 such that v 11 v2 x2 in n Bo and the maps L pg and L pB are the canonical projections Monomorphism Th
20. N 2 WEFTS 9 The ambifunctor Msp Gsp Set can be replaced by the following functor FUNCTOR M p G n Set points N N U gt U arrows s succ z gt 0 p gt pred One of the reasons for choosing ambigraphs rather than compositive graphs is well known and plays a crucial part in Duval amp Reynaud 94a Duval amp Reynaud 94b where the symbol is used instead of in the compositive graph Gip we cannot describe a computation process which replaces pos by idy since both are already equal A second reason for choosing ambigraphs rather than compositive graphs will become clear in guide2 and guide3 where we will have to interpret the equations as a relation weaker than equality 2 2 An example of a constraint Let w be an ambifunctor from G to Set How is it possible to ensure that the set w U has exactly one element This property gr e w U is a one element set is satisfied by some ambifunctors from Gs to Set like N but not by all of them Actually the property gr can be associated with something called a constraint and denoted I r in such a way that the ambifunctors from Gs to Set which satisfy the property gr are exactly those which satisfy the constraint Tr Constraints are defined in 2 3 and satisfaction in 2 5 Now let us look more closely at the constraint Ip First let us give an abstract version of the property or The one element sets are exactly the terminal sets in the fol
21. N 7 YT u of models of E by the following maps u VT E u T E u E for all point E of E e the set 1 T E is the disjoint union of the sets T E x for x E UV T E Uren T E 2 27 E 1 e and the map w T E W T E u E is defined piecewise u r E y x for all y T E z 4 BLOWING UP PROJECTIVE SKETCHES 33 The end of the proof is easy to check Let h and hz be two indexations by u in Mod E and let k hy ha be a p triangle It is easy to check that for all point E of E the map k E E 12 assigns to each element of u h1 E z an element of u h2 E xl indeed let y v E be such that hi E y1 2 then ho E k E y1 h1 E y x Let UA e E x denote this restriction of the map k E it defines a homomorphism of models of EA yu HAK Ah gt A ha and a functor uN Mod E p Mod EA y On the other hand let HAP Ah gt vo EN u denote the homomorphism of models of EA y defined by the inclusion 4 h E x v E for all point E x of E u Then u h dom u h Ji i ees Set LAN le 21 1 ae u h E2 22 1 UNB ezn GAME ea Pal i LAR Es 2 nq J v e v E1 v E2 Example 17 Let us consider the indexation Hie of Func by Toi as in example 13 The model Doart Moart Of Epir Zpart interprets the points Pt 7 Ar part and Ar tot respectively as sets partial functions
22. Paco Laboratoire d Arithm tique de Calcul formel et d Optimisation ESA CNRS 6090 SKETCHES AND SPECIFICATIONS USER S GUIDE First part Wefts for Explicit Specifications Dominique Duval amp Christian Lair Rapport de recherche n 2000 03 Universit de Limoges 123 avenue Albert Thomas 87060 Limoges Cedex T l 05 55 45 73 23 Fax 05 55 45 73 22 laco unilim fr http Awww unilim fr laco SKETCHES AND SPECIFICATIONS USER S GUIDE First part Wefts for Explicit Specification Dominique DUVAL Universit de Limoges Laboratoire d Arithm tique Calcul formel et Optimisation 123 avenue Albert Thomas 87060 Limoges Cedex France dominique duval unilim fr and Christian LAIR Universit Denis Diderot Paris 7 U F R de Math matiques Equipe Cat gories et Structures 2 place Jussieu 75251 Paris Cedex 05 France lairchrist aol com February 17 2000 http www unilim fr laco rapports SKETCHES AND SPECIFICATIONS USER S GUIDE SKETCHES AND SPECIFICATIONS is a common denomination for several papers which deal with applications of Ehresmann s sketch theory to computer science These papers can be considered as the first steps towards a unified theory for software engineering However their aim is not to advocate a unification of computer languages they are designed to build a frame for the study of notions which arise from several areas in computer science These papers are arrang
23. Y Ar describes the shape of the arrows of G etc Moreover when E E ww and u Set the second part of theorem 2 states that Set Hom 4nbi Y Set This result is easy to check directly Indeed it is clear except for the problems related to the size of the sets which are addressed in ref1 that e the models of Y Pt are the sets e the models of Y Ar are the maps e and so on 5 CONCLUSION 43 5 Conclusion In this paper we have given the main definitions and fundamental results needed for looking at specification problems in computer science from the point of view of sketch theory and its generalizations Our specification tools are the A wefts for some category A which is generally projectively sketchable Wefts of ambigraphs i e Ambi wefts where Ambi is the category of ambigraphs are well suited for dealing with purely functional problems However for dealing with the implicit features of computer languages we will see in guide2 and guide3 that we need a new specification tool This is given by mosaics which construction requires A wefts for other categories A A APPENDIX ABOUT CATEGORIES 44 A Appendix About categories Here is a short survey about compositive graphs categories functors and natural transfor mations as well as projective limits and inductive limits in a category These notions are well known However the way limits are introduced here from typical cones comes from the theory
24. an indexation H of S by p is an indexation H of S by y extended to all the constraints of S for all constraint T C X S C 7 p gt U of S an extension of H toT is made up of three indexations Hc Hp and Hy of respectively C D and U by y such that Hox Hc Hp y Hc Huo Hp The composition H oo of an indexation by a homomorphism of wefts a S S of level lt n is made up of the indexation H o g H oa of S by y extended to all the constraints of S in the following way let IY CSS CD gt U be a constraint of S then from the definition of a homo morphism of wefts C 4S C D 2 gt U is a constraint of S Now let H o o c He Hoo p Hp and H o o y Hu 6 y D 6 U HS Hp U NZ la ES Un 4 BLOWING UP PROJECTIVE SKETCHES 39 Then we may define the category of indexations by y in Weft Mod E Weft Mod E n Its points are the indexations by y of Mod E wefts and an arrow from H S y to Ho S2 u is a homomorphism of Mod E wefts K S S such that H o K H S z S2 NA u Now it is easy to check the equivalence Proposition 4 Weft Mod E u Weft Mod E p From the equivalence in theorem 1 follows the equivalence of the categories of wefts Weft Mod E u Weft Mod EA y whence by proposition 4 the equivalence Weft Mod E u Weft Mod EA y which is denoted H uNH Let S be a Mod E weft and H S u a pr
25. and total functions It interprets the arrows dom part and codom part resp dom tot and codom tot as the domain and codomain maps restricted to partial resp total functions Similarly the indexation ae Sop 7 Tart of the directed graph Go by Fe from exam ple 13 determines the following model Dave ARS p of En Zo pat Z sS aie ee U N Y The homomorphism of models of Epj Z purt Te Ap Teele g e Cope o Epir To 4 BLOWING UP PROJECTIVE SKETCHES 34 is defined by the inclusions UN 2 8 p 4 3 Indexations of wefts The definition of a y indexation can be generalized to the wefts of models of E in such a way that the category of Mod E u wefts can be identified to the category of Mod E wefts together with a u indexation An indexation H of a Mod E weft S by u as defined below is denoted A S u though S and u do not belong to the same category u is a point of Mod E whereas S is a point of Weft Mod E The definition of an indexation by u of a weft S of models of E is made recursively on the level of S together with the definition of the composition H o of an indexation H S u by a homomorphism of wefts o S Definition 13 If S has level 0 an indexation H of S by u is an indexation H of S by u The composition H oo of an indexation by a homomorphism of wefts S S of level 0 is the composition H o g as homomorphisms of models of E If S has level n gt 1
26. ariant homomorphism of directed graphs y G G is made up of two maps y Pt G Pt G Pt w ar G Ar G Ar such that for all arrow g Gj Go of G y Ar g p Pt G2 gt p Pt G1 in Y The maps Pt and y Ar are often both denoted y A APPENDIX ABOUT CATEGORIES 45 A 2 Compositive graphs Definition 17 A compositive graph G is a directed graph with e aset of identity arrows G IdAr C G Ar such that G dom g G codom g when there is only one identity arrow of rank G G it is often denoted ida e a set of pairs of composable arrows G CompP G ConsP and a map G comp from G CompP towards G Ar which maps each pair of composable arrows g1 Gi Go ga Ga G3 to its composed arrow G comp g1 92 G1 Gs which is denoted ga o g1 Definition 18 Let G and G be two compositive graphs A functor p G G is a homomorphism of directed graphs such that e for all identity arrow g of G the arrow p g is an identity arrow of g e for all composable pair g1 g2 of G the pair y g1 p g2 is a composable pair of G and plga o 91 p g2 91 A contravariant functor p G G is a contravariant homomorphism of directed graphs such that e for all identity arrow g of G the arrow w g is an identity arrow of g e for all composable pair g1 g2 of G the pair y g2 w g1 is a composable pair of G and plga o 91 9 91 o p g2 A functor o
27. d in guide2 and guide3 in order to define the mosaics and to study their applications to implicit features of programming languages No prerequisite is required to read this paper However it can prove helpful to be familiar with either algebraic specifications as introduced in Goguen et al 78 or Astesiano et al 99 for example or with categories part of Mac Lane 71 or sketches as in Coppey amp Lair 84 in Lellahi 89 or in the first pages of Duval amp Reynaud 94a This paper is intended to be an introductory paper We motivate our choices from detailed examples but definitions and results are usually not given in their most general setting proofs are just sketched and technical issues like the size of sets are left out On the other hand the reference manual ref gives general definitions and results comprehensive proofs and addresses size issues 2 WEFTS 5 2 Wefts The definition of wefts is given in this section Examples of wefts for the specification of natural numbers are considered in some detail The set of natural numbers can be defined as the set which is freely generated by an element 0 and an operation succ for successor In order to get a weft for the specification of natural numbers we proceed in the following way e First we consider the directed graph which underlies this definition for this purpose we introduce a one element set U x so that the natural number 0 can be seen as th
28. d the sets and its arrows the maps Clearly each category V with equations v v for all the arrows v in V becomes an ambi graph It follows that an ambifunctor from an ambigraph G towards a category Y maps each equation of G to an equality between arrows of V Example 1 We now build from the natural numbers two ambigraphs Gs and Gsp and two ambifunctors from Gs and Gs p respectively towards the category Set The ambigraph G has no identity arrow no composable pair of arrows and no equation AMBIGRAPH Us points U N arrows z U N s N gt N Gs Let us consider the set N of natural numbers with the element 0 and the map successor succ n n 1 Let U x be a one element set the constant map x 0 U N is also denoted 0 The ambifunctor M from Gs to Set is defined as follows AMBIFUNCTOR WN Gs Set points N N U gt U arrows succ z gt Q U SUCC 2 WEFTS T The ambigraph Gs p extends Gs AMBIGRAPH Gs p extends Gs arrows p N N idy N gt N pos N N identity arrow idy N gt N composable pair s p composed arrow pos N gt N equation pos idy Gsp The map predecessor pred N N is defined as pred n n 1l if n 0 and pred 0 0 The ambifonctor N sp from Gsp to Set is defined as follows AMBIFUNCTOR Nop Gsp Set extends Na arrow pt pred U x po N DS pred ___It is an ambifunctor since it maps the equation pos idy on the equality b
29. e constant map gt 0 from U to N The directed graph is made up of two points U and N which represent respectively the sets U and N and two arrows s N gt N and z U gt N which represent respectively the maps succ and 0 This directed graph is the support of the weft e Then we add two constraints to this support One says that the point U represents a one element set the other says that we are interested in the set which is freely generated by 0 and succ In a more general setting a A weft for some category A is made up of e a support which is a point in A e and constraints which are defined from points and arrows in A In the example above A is the category Dir of directed graphs Often A is the category Ambi of ambigraphs which is more expressive than Dir The wefts of ambigraphs or Ambi wefts can be seen as generalizations of the usual algebraic specifications Goguen et al 78 Wirsing 90 Most examples of wefts in this paper are either wefts of ambigraphs or wefts of compositive graphs However in guide2 we will focus on A wefts for other categories A For this reason in this section A is any category In 2 1 we define the category Ambi of ambigraphs an ambigraph is just a compositive graph see A 2 plus equations Constraints with respect to any category are defined in 2 3 and a recursive definition of A wefts follows in 2 4 The comprehensive definition of wefts will be given in the reference manual he
30. e Lisp and ML The use of algebraic specifications for imperative languages like Pascal or C is less straight forward because of the implicit features of these languages These implicit features include the notion of state and the side effects as well as overloading and coercions or error handling In this paper we introduce a new way to describe and handle specifications which can be considered as an extension of the theory of algebraic specifications Then using this new notion of specification the problems involved with implicit features will be dealt with in guide2 and guide3 It is known Lellahi 89 Wells amp Barr 88 that Ehresmann s sketches theory Ehresmann 66 Ehresmann 67a Ehresmann 67b Ehresmann 68 gives rise to notions which are quite similar to algebraic specifications Wefts and patchworks theory as introduced by Lair in Lair 87 and Lair 93 extends sketches theory It is somewhat related to notions introduced by Freyd in Freyd 73 see Freyd amp Scedrov 90 also In this paper a specification is defined as a weft Wefts generalize algebraic specifications and the realizations of a weft generalize the models of an algebraic specification Moreover wefts can be used to define mosaics as will be seen in guide2 leading to a clear management of states state and more generally of many implicit features of computer languages This paper is made up of three sections together with an appendix giving som
31. e Paris 264 pp 273 276 1967 Ehresmann 67b Charles Ehresmann Sur les structures alg briques Comptes Rendus de l Acad mie des Sciences de Paris 264 pp 840 843 1967 REFERENCES 59 Ehresmann 68 Charles Ehresmann Esquisses et types de structures alg briques Bulletin de l Institut Polytechnique Iasi 14 pp 1 32 1968 Freyd 73 Peter J Freyd Properties invariant within equivalence types of categories In Filen berg Festschrift Academic Press 1973 Freyd amp Scedrov 90 Peter J Freyd and A Scedrov Categories Allegories Mathematics Library 39 North Holland 1990 Guitart amp Lair 82 Ren Guitart and Christian Lair Limites et colimites pour repr senter les formules Diagrammes 7 pp GL1 GL24 1982 Goguen et al 78 Joseph A Goguen J W Thatcher and Eric G Wagner An initial algebra approach to the specification correctness and implementation of abstract data types In R T Yeh editor Current Trends in Programming Methodology Volume IV Data Structuring chapter 5 pp 80 149 Prentice Hall 1978 Lair 71 Christian Lair Foncteurs d omission de structures alg briques Cahiers de Topologie et G om trie Diff rentielle 12 pp 147 186 1971 Lair 77 Christian Lair Esquissabilit des structures alg briques Th se de doctorat es sciences math matiques Universit de Picardie Amiens 1977 Lair 87 Christian Lair Trames et s mantiques cat goriques des syst mes de trames Dia
32. e basic notions in category theory The aim of section 2 is to define the wefts more precisely the A wefts with respect to an arbitrary category A the definition of a category is given in A 3 We also define the category Ambi of ambigraphs since the Ambi wefts or wefts of ambigraphs are quite similar to the algebraic specifications A weft has realizations and the more precise a weft is the less realizations it has Here are some examples of specifications which are presented in an informal way from the point of view of wefts These specifications are more and more precise e A directed graph see A 1 for this well known notion made up of points and arrows is a specification though a very simple one A set valued realization of a directed graph is made up of a set for all point of the graph and a map for all arrow For instance let us consider the directed graph Gint Ey X E lt lt E 1 INTRODUCTION 2 and three realizations among others of Gint They are called respectively w1 w2 and w3 and they are defined from the set Z of integers with the operations succ and pred for successor and predecessor the addition Z Z and the constant map 0 from the one element set x to Z succ succ succ w x 0 Z 72 w9 yl z w3 fx 0 Z 72 pred pred sueo By composition of arrows from Gint we get terms or programs which may be interpreted by these realizations For example the program p z compo
33. ective sketch E Ambi So each ambigraph can be identified with a model of E Ambi Since an ambigraph has points arrows and equations the sketch E qm has points called Pt Ar Eq The ambigraph G for example can be identified with a model of E Ambi which interprets the point Pt as the set Ep E1 E2 the point Ar as the set 2 5 p a and the point Eq as the set p s x 2 s p x x We will only need projective sketches i e sketches with constraints for projective limits From the point of view of their logical power projective sketches essentially correspond to positive conditional i e Horn universal specifications while sketches correspond to first order specifications Guitart amp Lair 82 With wefts as with patchworks we can reach second order specifications So from our point of view an A weft for any category A is a specification In particular A can be the category Ambi of ambigraphs which is sketched by Emp We will consider other categories A which can also be sketched Therefore we need a method for building new sketches together with a way to recover their categories of models Such a method is presented in section 4 It is called the blow up of a projective sketch and it is similar to a well known construction over categories called the discrete fibration The blow up generalizes the usual sagittal diagram of a map For example let us consider the two sets X x1 12 13 and X x 1 4 and the
34. ed in two complementary families REFERENCE MANUAL and USER S GUIDE The reference manual provides general definitions and results with comprehensive proofs On the other hand the user s guide places emphasis on motivations and gives a detailed description of several examples These two families though complementary can be read independently No prerequisite is assumed however it can prove helpful to be familiar either with specification techniques in computer science or with category theory in mathematics These papers are under development they are or will be available at http www unilim fr laco rapports REFERENCE MANUAL First Part Compositive Graphs Second Part Projective Sketches Third Part Models USER S GUIDE First Part Wefts for Explicit Specification Second Part Mosaics for Implicit Specification Third Part Functional and Imperative Programs In addition further papers about APPLICATIONS are in progress with several co authors They deal with various topics including the notion of state in computer science state over loading coercions and subsorts These articles owe a great deal to the working group sketches and computer algebra we would like to thank its participants specially Catherine Oriat and Jean Claude Reynaud as well as the CNRS These papers have been processed with ATEX and Xy pic First Part Wefts for Explicit Specification The aim of this paper is to define wefts for the
35. efts and sketches 3 1 A compositive graph for ambigraphs Ambigraphs are defined in 2 1 from compositive graphs which themselves are defined in A 2 from directed graphs which are defined in A 1 Hence we now build three projective sketches each one extending the previous one first Ep for directed graphs then Ecomp for compositive graphs and finally E Ambi for ambigraphs Their supports which are compositive graphs are described in this section these descriptions are abbreviated as in 2 1 Their constraints will be described in section 3 4 To begin with for directed graphs let Ey be the following simple compositive graph COMPOSITIVE GRAPH Epp points Pt Ar arrows dom Ar Pt codom Ar Pt Epir Each directed graph G determines a functor from Ep towards Set points Pt gt G Pt Ar gt G Ar arrows dom G dom codom gt G codom 3 PROJECTIVE SKETCHES 19 For compositive graphs let Ecomp be the following compositive graph COMPOSITIVE GRAPH Ecomp extends points arrows composition Ep IdAr ConsP CompP comp CompP Ar p ConsP Ar p2 ConsP Ar jraar IdAr Ar jcompp CompP ConsP dom O jraar codom O jrqar dom o po codom o pj dom o comp dom o pj jcompp codom o comp codom o p2 jcompp ConsP lt CompP pi j CompP eR AAA comp Ecomp Pt o ME codom composition Similarly each compositive graph G dete
36. egory of sets More precisely the first one can be stated as a pullback and the second one as a monomorphism This is why we add to E three distinguished projective cones 3 PROJECTIVE SKETCHES 24 e the point ConsP is the vertex of the distinguished projective cone I consp Deonsp Hence with d p c for distinguished projective cones PROJECTIVE SKETCH Ecomp support Ecomp d p c Tconsp Dcompr gt Draar This is an abbreviated notation indeed the identity arrows idcompp and idqqar which occur in the distinguished projective cones compp and lraar should be added to the support of Ecomp Moreover it should be noted since it is not clear from our notations that a point in a projective sketch can be the vertex of several distinguished projective cones Proposition 2 The category of models of the projective sketch Ecomp is equivalent to the cate gory Comp of compositive graphs Mod Ecomp Comp 3 PROJECTIVE SKETCHES 25 About the proof A functor Pcomp Comp Mod Ecomp is easily defined using the functor Ppir Dir Mod Epjr from the proof of proposition 1 Then it is easy to check that comp is an equivalence The functor Pp is an isomorphism however the functor Peomp is only an equivalence This comes from the fact that Ecomp unlike Epir has distinguished projective cones The interpretation of such a cone by a model of Ecomp is any limit projective cone However we will ide
37. el 1 will be used guide2 in order to study error handling It includes a terminal point constraint and a binary sum constraint as described in examples 3 and 4 Ambi WEFT Se points H H H arrows h H H h H H terminal point H sum pt de pre Se H gt H ape eo 2 5 Realizations of a weft It is now with the definition of the realizations of an A weft S that we explicitly give the property which is associated with the potential of a constraint A realization of S is defined as an arrow in A with domain the support of S which satisfies the constraints of S satisfaction is defined recursively on the level of the weft the realizations of a weft are called its models in Lair 87 Definition 4 Let S be an A weft and A a point of A If S has level 0 a realization of S towards is an arrow w S A in Let n be an integer gt 1 Assume that e S has level lt n e for all A weft S of level lt n 1 we know the set Real 1 n1 8S A of realizations of S towards A 2 WEFTS 15 e and Realy 1 S A is a subset of the set Homa S A of arrows from S to A in the category A Let r C5s CDU be a constraint of S Then an arrow w S A of A satisfies the constraint I if e woy C A is a realization wc of C towards A e and for all realization wp of D towards A such that wp o y we there exists a unique realization wy of U towards A such that wy o uwp
38. ese projective sketches are the blow ups Env Z of Emo by an ambigraph Z with the homomorphism called fibration E 4mbi Z E4mbi Z Emi More over the blow up Emo Z sketches the category of T indexations where an Z indexation is an ambifunctor with codomain Z The blow up of a projective sketch by one of its models is studied by Lair in Lair 71 Lair 77 this notion is similar for sketches to the well known notion of discrete fibration associated to a functor from a category towards Set or to the compositive graph of hypermorphisms introduced by Ehresmann in Ehresmann 65 The aim of this section is to define and study the blow ups of any projective sketch Let E be a projective sketch and u a model of E In 4 1 we define the category Mod E p of indexations of models of E Then in 4 2 we define the projective sketch Ely blow up of E by y and we prove its main property both categories Mod E p and Mod El y are equivalent In 4 3 we generalize this result to pu indexations of Mod E wefts and we introduce the loose homomorphisms of wefts In 4 4 we consider an example the blow up of E gnp by each model Ve E given by its Yoneda counter model VB ny EAmbi gt Mod E Anvi 4 1 Indexations Definition 10 An indexation by u or p indexation of a model v of E is a homomorphism h v u of models of E Let h 1 u and ha v y be two p indexations A u triangle from h towards hs is a homomorphism k v v2 o
39. etween maps pred o succ dy i e the equality Yn EN pred succ n n In the description of the ambigraph Gs p for the equation po s idy to make sense it is necessary that Gs contains the identity arrow idy the composable pair s p and its composed arrow pos This is why we are allowed to use the following abbreviated description AMBIGRAPH Gs p 2 WEFTS 8 extends Ges arrow p NON equation pos idy From now on such abbreviated descriptions will be used for ambigraphs Let pp Gs Gs be the extension functor Then clearly N N5p Op Pp Gs Gsp Set It is worth noticing that the image of the point U by an ambifunctor from Gs or Gs p to Set can be any set not just a one element set We are not yet able to lay down such a property however it will become possible later thanks to realizations of wefts see example 5 In order to justify the use of equations i e the use of ambigraphs rather than compositive graphs let us come back to example 1 Example 2 In example 1 the equation pos id y can be avoided by replacing the ambigraph Gs p by the following compositive graph COMPOSITIVE GRAPH G y points U N arrows z U gt N s N gt N p N gt N idy N gt N identity arrow idy N gt N composable pair s p composed arrow pos idy N gt N or with the abbreviated description COMPOSITIVE GRAPH points U N arrows z U gt N s N gt N p N gt N pos idy N gt
40. f compositive graphs is called an extension if it is an inclusion on the sets of points and on the sets of arrows Then it is also an inclusion on the set of identity arrows and on the set of composable pairs This notion of extension is borrowed from the theory of algebraic specifications it should not be mistaken for the notion of extension in category theory A 3 Categories Definition 19 A category A is a compositive graph where e the map a gt A dom a defines a bijection of A IdAr on A Pt the inverse map A gt id a from A Pt to A IdAr is denoted A selid and called the selection of identities e the sets A CompP and A ConsP are equal such that e unitarity ao ida a and id oa a for all arrow a Ay Ao e associativity a3 o az o ai a3 0 az o a1 for all triple of arrows a1 az az such that the pairs a1 a2 and az a3 are consecutive The points of a category are also called objects and its arrows are also called morphisms or homomorphisms An isomorphism from A to Ag in A is an arrow a A Az such that there exists an arrow az Ag Aj inverse of ay i e such that as o ai id 4 and aj o a2 id4 Then and A are isomorphic and we write A SA A APPENDIX ABOUT CATEGORIES 46 Since a category is a compositive graph we may consider the functors resp the con travariant functors from a compositive graph towards a category or from a category towards a category The functors from a comp
41. f models of E such that ha ok hy k Vo u Mod E u V1 It is easy to define the category Its points are the y indexations in Mod E and its arrows are the y triangles Let h v y be an indexation of v by y in the category Mod E Let x and y be two ingredients of y and y respectively both with the same nature E If h E y a we say that x is the index of y Example 12 Let us consider 4 BLOWING UP PROJECTIVE SKETCHES 28 PROJECTIVE SKETCH E map points E E arrow e E gt P Each map f X X determines a model Z of Ep and vice versa MODEL Tf Emap Set points E X BE X arrow er f An indexation by Tf of a model Z of E Map where g Y Y is some map is a homomor phism h I Ty ie a pair of maps h Y X h Y gt X such that foh h og yx Ny ff Y z gt xX Example 13 Let us consider the following category Func its points are sets and its arrows are functions where a function unlike a map can be partial In this example we consider the homomorphisms from a directed graph G towards the category Func Moreover we wish to say for all arrow g of G whether the interpretation of g should be total or partial here partial means strictly partial i e not total For this purpose we map each arrow of G to the symbol tot if we wish its interpretation to be total or to the symbol part if we wish it to be partial More precisely we build
42. for specifications with implicit state Rapport de recherche du LACO 2000 http www unilim fr laco rapports Also D Duval idem Submitted for publication Ageron 91 Pierre Ageron Structure des logiques et logique des structures Th se de doctorat de math matiques Universit de Caen 1991 Astesiano et al 99 E Astesiano H J Kreowski and B Krieg Brckner Algebraic Foundations of Systems Specification Springer 1999 Coppey amp Lair 84 Laurent Coppey and Christian Lair Le ons de th orie des esquisses I Diagrammes 12 1984 Coppey amp Lair 88 Laurent Coppey and Christian Lair Le ons de th orie des esquisses II Diagrammes 19 1988 Duval amp Reynaud 94a Dominique Duval and Jean Claude Reynaud Sketches and computa tion part I Basic definitions and static evaluation Mathematical Structures in Com puter Science 4 pp 185 238 1994 Duval amp Reynaud 94b Dominique Duval and Jean Claude Reynaud Sketches and computa tion part II Dynamic evaluation and applications Mathematical Structures in Com puter Science 4 pp 239 271 1994 Ehresmann 65 Charles Ehresmann Cat gories et Structures Dunod 1965 Ehresmann 66 Charles Ehresmann Introduction to the theory of structured categories Tech nical Report 10 University of Kansas at Lawrence 1966 Ehresmann 67a Charles Ehresmann Probl mes universels relatifs aux cat gories n aires Comptes Rendus de l Acad mie des Sciences d
43. identity functions are total The composed arrows of Zpart mean that given two functions f and g the composed function go f is total when f and g are total and otherwise g o f is generally partial The equations of Tu mean that for two functions to be equal they must be either both total or both partial It should be noticed that here composition and equations play fairly different roles unlike in previous examples the role of the equation pos id y in the ambigraph Gs p from example 1 is similar to the role of the composition po s idy in the compositive graph Gip from example 2 indeed both are interpreted as equalities in categories On the contrary the ambigraph Zpart is not used as the domain of an ambifunctor towards a category it indexes other ambigraphs G and each of its ingredients gives some information about the required interpretation of some ingredients of G We will see in guide2 and guide3 more sophisticated examples where equations will be used to express more subtle notions of equality Here it is impossible to extend the indexation of directed graphs hour Func gt Than an indexation of ambigraphs Apart Func Tpart Indeed when at least one function in a pair of consecutive functions is partial the composed function is generally partial however it may sometimes be total for example succ N N is total pred N N is partial however predosucc N N is total Hence we should have succ gt tot
44. indexation of S The homomorphism of models of EA y uN HL yA E gt So E u has been defined in 4 2 from the inclusions u H E x C S E for all point E x of EX y It can easily be extended recursively on the level of S into UN A u H gt So EN u which however is not a homomorphism of Mod E u wefts It is a loose homomorphism as defined below Eu E Y A NE E E Cal Set Definition 14 Let A be a category and S and S two A wefts A loose homomorphism S gt S of A wefts is made up of an arrow amp S S of A and for all constraint of S PSC 48 02 U of a constraint of S P C x s c Y D o U E 4 BLOWING UP PROJECTIVE SKETCHES 36 and three loose homomorphisms 6c C C 0p D D 5u U U such that with the natural definition of composition ao dad oGp Gy 06 x oe oct Cc gt 5 U S x Gr Z ln This definition can be compared with the definition of the homomorphisms of A wefts given in 2 4 It follows that a homomorphism of A wefts is a loose homomorphism such that for all constraint I we have I T and the three loose homomorphisms c p and y are the identities The homomorphisms of A wefts behave well with respect to the realizations let o S S be a homomorphism of A wefts if an arrow w S A satisfies the constraints of S then the arrow w o g S A satisfies the constraints of S Con
45. is is a special kind of pullback With the same typical base 6 as above let us assume that 7 B n B2 and n b1 n b2 Let Vi 7 B1 Vo Bo and m m b1 Vi Vo Let us consider the projective cone L with base 7 and vertex L C Vi A APPENDIX ABOUT CATEGORIES 51 and projections L pg L pp idy and L pp m Then it is easy to check that L is the pullback of 7 if and only if m is a monomorphism which means e for all pair of arrows v and va V Vi mov M O Vo gt gt U 09 When V is the category of sets it means that m is an injective map A 6 Inductive limits Formally this section is obtained from the previous one by duality i e by changing the direction of the arrows inside the compositive graphs However the interpretation of this duality in the category of sets is not straightforward Definition 25 Let B be a compositive graph The typical inductive cone of typical base B also called the typical B inductive cone is the compositive graph C 6 made up of B a point C an arrow ig B C for all point B of B and an equation iprob i8 for all arrow b B B of B The point C is the vertex of the cone C B and the arrow ig is its induction towards B Definition 26 Let B and G be two compositive graphs An inductive cone of typical base B also called a B inductive cone in G is a functor x C B G The functor n x 0 8g B G is the base of the inductive cone
46. ith a terminal point constraint y Cr S see the example 3 Let w be a realization of S towards a category V From the definition above e for all point V of V there exists a unique arrow f V w x C in V 2 WEFTS 16 This means that w y C is a terminal point of V When V is the category of sets it means that w x C is a one element set For instance the ambifunctor M Gs Set example 1 defines a set valued realization of S example 5 since N lt U x In the same way the ambifunctor Msp Gsp Set example 1 defines a set valued realization of Ssp example 5 Note that S and Ssp have many other set valued realizations Example 9 The weft of ambigraphs Ss ini in example 6 is made up of S and the constraint Tz It follows that the realizations of Ss ini are the realizations of S which satisfy the constraint Tz Let w Ss Set be a set valued realization of Sy it is characterized by a set w N with an element w z w N and an operation w s w N w N Then w defines a set valued realization of Sx init if and only if e woyxy C Set is a set valued realization of Cz it means that w U is terminal which is already true since w satisfies the constraint U 1 of S e and for all set X with an element ro X and a map f X X there exists a unique map u W N gt X such that uow z x0 and fou uou s It is easy to check that M Gs Set defines a set valued realization of Ss init
47. l is the following theorem 2 proven in our reference manual It is similar to the classical result on Yoneda functor The composition of the contravariant functors Yp E gt Mod E and Hom 4a E 4 Mod E Set gives rise to a functor Home Ye 1 E Set In addition since VE is a counter model of E and Hom ya 1 is left exact which means that it maps each limit inductive cone of Mod E to a limit projective cone the composed functor Hom var Ve 4 is a model of E Hom mam JE 1 E Set VE eo E Mod E Hom moa Ve 4 as Hom Woa e 4 TS Set Theorem 2 Yoneda lemma for projective sketches Let y be a model of E Then Eu y u IndLim E u E 45 Mod E and Le Hom Mod E VE 1 In the first part of this theorem only the sublying contravariant functor of the counter model Ye o EN y of El y is used to build the inductive limit Example 21 The description of Y VE 4 in example 20 gives the following interpretation of Yoneda lemma when E E Ambi e the first part of theorem 2 states that each ambigraph G can be built by taking each one of its ingredients points arrows etc and gluing them together in the right way 4 BLOWING UP PROJECTIVE SKETCHES 42 e the second part states that for all point E of E 4 the ambigraph Y E describes the shape of the ingredients of G of nature E the ambigraph Y Pt describes the shape of the points of G the ambigraph
48. lowing sense a set U is terminal if for all set X there exists a unique map from X to U VX au U Hence the property gr can be stated as e w U is a terminal set It follows that the constraint r r must be such that an ambifunctor w Gs Set satisfies ly if and only if the set w U which we denote U is terminal e First we must pick out the point U in G since it is the point on which the constraint acts For this purpose we introduce the ambigraph Cr made up of a single point and the ambifunctor x Cr Gs such that y C U The ambifunctor we w o y Cr Set is characterized by we C U Now in order to express the terminality property we must be able to pick out pairs of sets U X for any set X For this purpose we introduce the ambigraph Dr made up of two points C and D and the extension ambifunctor yr Cr Dr Then the pairs of sets U X are the pairs wp C wp D where wp Dr Set are the ambifunctors which extend we in the sense that wp oyr we 2 WEFTS 10 e Lastly we introduce the ambigraph Ur made up of two points C and D and one arrow u D C and the extension ambifunctor r Dr Ur Let wp be as above and let X wp D The maps f X U are the maps wy u wy D wy C where wy Up Set are the ambifunctors which extend wp in the sense that wy odp wop Cr Dr D Ur D C C C The constraint I r is made up of the ambigraphs Cr Dr and Ur and the ambifunctors x
49. m tot Ar tot Pt J Epir Zpart Ar tot Po P Pt 7 dom part codom part Ar part Epir Z part l dom A TT ES Epir Pt A A Ar codom 4 BLOWING UP PROJECTIVE SKETCHES 32 We now come to the fundamental property of the blow up Theorem 1 Fundamental property of the blow up The category of indexations by y is equivalent to the category of models of the blow up of E by pu Mod E u Mod EA y First let us introduce some notations On the points of both categories the equivalence is denoted Mod E u Mod E y h BAS Nh p r Eva Ta Moreover similarly to the notation Ely dom E u we denote p 7 dom N 7 in such a way that HVT UVT gt H The theorem states that for all 7 model of EA y HAVT ST and that for all h v y indexation by y UV uh ER so that looking at the domains of both homomorphisms p uA h v About the proof For all point of Mod E p i e all homomorphism v u of models of E we define the model yA h of EA y as follows e the interpretation of a point E x of EA y is a subset of v E it is made up of the elements of v E which are mapped to x by h E HAR E x y ev E TR E y x lt SvV E e and the interpretation of an arrow e x of E is the restriction of the map v e LAN le x y v e y for all y LAME a In the opposite direction for all model 7 of EA y we define the homomorphism
50. mcomp 9 V is the set of points of the category Func G V Moreover it is easy to check that for all functor of compositive graphs yp G G the map Homcomp V Homeomp G V Homeomp G V is sublying to a functor Func p V Func G V Func G V which is defined by e Func y V y p o for all functor y from G to V e and Func p V t to p for all natural transformation t u wh where op pop gt u o is the natural transformation defined by t o y G 1 p G for all point G of G A APPENDIX ABOUT CATEGORIES 48 All this defines a contravariant functor Func V Comp Set On the other hand the equivalence of two categories which is weaker than the isomorphism can be useful Definition 21 An equivalence between two categories A and A is a pair of functors A A A A and a pair of natural isomorphisms o id and Do idy It is denoted AZ A Example 23 A simple example of equivalence which is not an isomorphism is the following one Let A be the category made up of two points A and Ag their identities id4 and idA two arrows a Ay A and ag Ag Aj with the composition defined by ag o as 1id 4 and ayoa2 ida Let A be the category made up of one point A and its identity idy A A Then A and A are equivalent let A A be the unique functor from A to A and let A A be
51. n L is called the sum of the n B for B B in V Its vertex is denoted L C peg n B or L C B Bn when B B B The property of the sum can be stated as follows A APPENDIX ABOUT CATEGORIES 53 e for all point V of V and all set of arrows vg n B V for B B there is a unique arrow v JI n B V BEB such that vo L ig vp for all Be B When V is the category of sets it means that peg n B is up to bijection the disjoint union of the sets 7 B and the maps L ig are the canonical injections Pushout When the typical base B is made up of two arrows with the same domain say bi Bo B and ba Bo B and maybe some identity arrows the inductive cone C 6 has three inductions ig B C ig By gt C and ig Bo C such that ip o b1 iB and ip 0 b2 ip so that ip is determined by p ig and B and can be forgotten BB _ Then L is called the pushout of 7 or sometimes the pushout of 7 B1 and Bz above n Bo If we denote L C n B1 n 8p 7 B2 the property of the pushout can be stated as follows e for all pair of arrows v n B1 V and v2 n B2 V such that v o n b1 v2 o n b2 there is a unique arrow v Bi n B 1 B2 gt V such that vo L ig v and vo L ig v2 When V is the category of sets it means that 7 B1 n 8 n B2 is obtained up to bijec tion by identifying in the disjoint union 7 B1 Be the element
52. nerated by 0 and succ This amounts to saying that it satisfies the following initiality property e for all set X endowed with an element xy X and a map f X X there exists a unique map u N gt X such that u 0 xp and flu n u s n for all n N Let us build a weft of ambigraphs Ss ini by adding to S an initiality constraint Ty The potential of this constraint is the following dyouy u1 oco dioui u10c and its body is defined as AMBIFUNCTOR yz Cy gt Gs points CoU Ci N arrows Coz Q res 2 WEFTS 14 The wefts of ambigraphs Cyr Dz and Uy have level 1 because they have constraints of level 0 Henceforth the weft of ambigraphs Ss ini has level 2 This example corresponds to the following diagram in Ambi where each line e e e represents Cp 2 Dr re J o 0 o o 0 0 ee ee BE e Xr or A va s init Wefts of ambigraphs generalize algebraic specifications However example 6 shows that the initiality constraint over natural numbers can be handled by the wefts in the same way as the terminality constraint over the point U This point of view on constraints is highly powerful and plays a fundamental role It is borrowed from Lair 87 and Lair 93 see also the notion of canvas in Ageron 91 On the contrary algebraic specifications use fairly different techniques in order to handle these two constraints see Wirsing 90 Example 7 The following weft of ambigraphs of lev
53. ntify each compositive graph with the corresponding model of Ecomp Now let us add to the compositive graph E 4 4 some constraints corresponding to the fol lowing properties of each ambigraph 4 e G ConsP resp G RankP is the set of all consecutive pairs resp pairs with the same rank of G e the maps G jraar G jcompp and G jzq are injections These properties can be stated as projective limits in the category of sets So that we now add to E 4 five distinguished projective cones e the point ConsP is the vertex of the distinguished projective cone Pconsp as above e the point RankP is the vertex of the distinguished projective cone l ranxp Drankp e the point IdAr resp CompP is the vertex of the distinguished projective cone l raar resp comp as above e the point Eq is the vertex of the distinguished projective cone Pg Hence PROJECTIVE SKETCH E Ambi support E Ambis d p c PconsP Drankp l raar L compP Irq 3 PROJECTIVE SKETCHES 26 Proposition 3 The category of models of the projective sketch E mp is equivalent to the cate gory Ambi of ambigraphs Mod E Ambi Ambi About the proof Similar to the proof of proposition 2 Example 11 The ambigraph G in example 1 corresponds to a model of E Ambi 0 2 8 0 D In the same way the ambigraph Gs p in example 1 corresponds to a model of E Ambi idn tz 5 gt s p UNI z s p idy po s EAN a s p
54. o the domain of ga e the pairs with the same rank are all the pairs g gr such that the rank of gr is equal to the rank of gy e the maps G jraar G jcompp and G jzq are injections 3 2 Projective cones and projective sketches The constraints which we will add to Ecomp and E gnp have a special shape they are called distinguished projective cones and they lay down properties of projective limits Definitions of a typical projective cone a projective cone and a limit projective cone can be found in A 5 Definition 5 Let B be a compositive graph A B distinguished projective cone is a constraint which has level 0 and the following potential e the compositive graph C is the typical B projective cone Cp B e the compositive graph D D B extends Cp 8 by a second typical B projective cone i e by a point D an arrow qp D B for all point B of 6 and composition bo qg qp for all arrow b B B of B e the compositive graph U U B extends D B by an arrow u D C and composi tion pg ou qg for all point B of B e the functors yg Cp B D B and g Dp B U B are the extensions 3 PROJECTIVE SKETCHES 21 Let G be a compositive graph For any given compositive graph B a distinguished B projective cone in G is characterized by its body x C B G Often it is this body which is called the distinguished B projective cone rather than the complete constraint A distingui
55. ody x is used to pick out in Ap the image of Supp C by x The potential y 6 is used to lay down some property of the image of x Supp C by an arrow w Ag A where A is a point of A this property is made precise in 2 5 through the notion of satisfaction Example 3 Let both A and W be the category of ambigraphs and let Supp be the identity Then Ag is an ambigraph called G In the same way C D and U are ambigraphs called C D and U and y y and 6 are ambifunctors For instance a terminal point constraint has potential 5 Cr Dr Ur as described in 2 2 Let G x C be the image of the point C of Cr in G This is usually denoted G 1T Example 4 Here also let A W Ambi and let Supp be the identity A binary sum constraint over an ambigraph G has potential Cs C1 al Ys C ee Ca Let Gy 462 42 C CL C2 be the image of Cs in G Usually when g and gz are clear from the context this is denoted G G1 G 2 2 4 Wefts and weft homomorphisms Each A weft has a level which is a non negative integer and a support which is a point of A An A weft of level 0 is just made up of its support it is a point of A An A weft of level lt n for some integer n gt 1 is made up of a support and constraints which themselves are made up of A wefts and A weft homomorphisms of level lt n 1 Definition 3 The category Weft A of A wefts of level 0 is equal to A The functor Suppo Wefty A A is the identity
56. of sketches and wefts Various examples of all these notions can be found in the previous sections of this paper A 1 Directed graphs Definition 15 A directed graph G is made up of e aset of points G Pt e aset of arrows G Ar e and two maps G dom and G codom from G Ar to G Pt which assign to each arrow respectively its domain and its codomain Let g be an arrow of domain G and codomain Ga it is denoted g Gi Ga and we say that Gi Ga is the rank of g A pair of arrows g1 g2 is consecutive if the codomain of g is equal to the domain of g The set of pairs of consecutive arrows is denoted G ConsP and the set of pairs of arrows with the same rank is denoted G RankP The points of a directed graph are often called vertices and its arrows edges Proposition 1 in 3 4 justifies the use of notations like G Pt etc rather than Pt G etc for example Often G G means G G Pt Also dom g and codom g denote the domain and the codomain of an arrow g of G rather than G dom g and G codom g respectively A homomorphism of directed graphs preserves the direction of arrows whereas a contravari ant homomorphism reverses it Definition 16 Let G and G be two directed graphs A homomorphism of directed graphs p G G is made up of two maps y Pt G Pt G Pt y Ar G Ar G Ar such that for all arrow g Gj Go of G p ar g p Pt G1 p Pt G2 in Y A contrav
57. oint of Ep VS art Trart Peart Epi ee Set see example 17 By definition these realizations are the homomorphisms of Ep Zpart models from Zare AA p towards Tari har Which satisfy the constraint Toy AD T It means that such a realization w is made up of e two sets w U and w N e two total functions w z w U w N and w s w N w N and one partial function w p W N gt w N e and in addition the set w U is such that for all set X there is a unique total function f X w U it means that w U is a one element set 4 4 Yoneda counter model The Yoneda functor is considered here in the framework of projective sketches see Lair 71 and the reference manual Let E be a projective sketch For all point E of E let Ye E be the model of E freely generated by an ingredient of nature E it can be proven that such a model does exist Then to each arrow e E E of E is canonically associated a homomorphism of E models Yp e Ve E YE E This defines a contravariant functor Vg from E to Mod E In addition this contravariant functor maps each distinguished projective cone of E to a limit inductive cone of Mod E for this reason it is called a counter model It is the Yoneda counter model of E Ve E gt Mod E Example 19 Let E E Map as in example 12 Then e the model Yg E of E Map is made up of two sets Ye E E zx and VB E E a and of the map Yp E e x 2 e
58. ositive graph towards a category are sometimes called diagrams Let A be a category For all point A of A there is a contravariant functor Homax A A Set which assigns to each point A of A the set Hom 4 Aj A of arrows from A to A in A and to each arrow a A Aj the map Hom 4 a1 A Hom4 A1 A gt Homa 4 A defined as Hom a1 A a a0a A A for all arrow a A A of A A Example 22 In fact we have already met three categories see ref1 for size issues Dir Comp Cat Indeed the directed graphs with the homomorphisms of directed graphs make up a category Dir e the identity arrow idg G G of a directed graph G is defined by the two identity maps idg pt and idg ar i e the composed arrow y o of a pair of consecutive arrows y y is defined by the two composed maps y o p Pt p Pt o p Pt and y oy Ar y Ar o p Ar Similarly e the compositive graphs with the functors make up a category Comp e the categories with the functors make up a category Cat A 4 Natural transformations The functors from a compositive graph towards a category can themselves in a natural way be seen as the points of a category Definition 20 Let G be a compositive graph V a category and 1 u2 two functors from G to V a natural transformation t y u2 is made up of e for all point G of G an arrow t G y G gt pa G of V such that A APPENDIX ABOUT CATEGORIES
59. port S Some categories can be described as the category of models of a projective sketch Definition 9 Let A be a category It is projectively sketchable if it is equivalent to the category of models of some projective sketch E i e if A Mod E Then we say that E sketches A 3 4 A projective sketch for ambigraphs Let us now add to the compositive graph E 4 some distinguished projective cones in order to get a projective sketch E Amb which sketches ambigraphs i e such that the category of models of E mov is equivalent to Ambi As in 3 1 let us first look at directed graphs and compositive graphs The compositive graph Ep is the support of a projective sketch without any distinguished projective cone PROJECTIVE SKETCH Ep support Epy Proposition 1 The category of models of the projective sketch En is isomorphic to the category Dir of directed graphs Mod Epi Dir About the proof We have already noticed that each directed graph Y determines a functor p G from Ep towards Set such that e Pnr G E G E for all point E of Epi i e H Pt or Ar 3 PROJECTIVE SKETCHES 23 e Por G e G e for all arrow e of Ep i e e dom or codom Similarly each homomorphism of directed graphs y G g determines a family of maps Sn U E V E G E gt G 8 for all point E of Ex Let us check that these maps build up a homomorphism p Y pi G Ppir G of models of Epir i e tha
60. positive graph for ambigraphs Projective cones and projective sketches Models of a projective sketch A projective sketch for ambigraphs About wefts and sketches Blowing up projective sketches 4 1 4 2 4 3 4 4 INA XALIONSE AUS EII Be ha OR fo esos OMS Sup an BlOWS UPS en Asie eos eis AS ai BON eae oe eee ii ly A ee Indexations of welts 2 222 de dou Shs a AO part a ia A Bu le as Yoneda counter model Conclusion Appendix About categories A l A 2 A3 AA A5 A 6 Direct ed eraphs moco Less us a a a ee do MATE 4 R Compositive graphs Categories 2 6 4 4 945 honte ee AS AA a ee BEd ee Ee Rae Bee Natural transformations Projective limits ardian en D AR et a nu a oe Ve les Inductive mits ss su Et LA DL ane ttn Ml EO D LRU oe 56 18 18 20 21 22 26 27 27 30 34 38 43 Index ambigraph 5 ambifunctor 6 arrows 21 44 base 48 51 blow up 30 body 11 category 45 codomain 44 composed arrow 45 compositive graph 45 cone 20 48 51 constraint 10 11 contravariant functor 45 contravariant homomorphism 44 counter model 38 diagram 46 directed graph 44 distinguished projective cone 20 domain 44 duality 51 edge 44 epimorphism 53 equation 6 equivalence
61. re endowed with strong functoriality properties once something is well defined in a precise meaning over ambigraphs its definition extends automatically to wefts of ambigraphs It means that the extension of such a definition to the constraints however powerful they are does not require any effort Section 3 is devoted to projective sketches Sketch theory has been known since Ehresmann s pioneering work in the 60 s Sketches can be considered as wefts of compositive graphs com positive graphs which are defined in A 2 are directed graphs with some composition of arrows with constraints only for limits projective or inductive limits see A 5 and A 6 The set valued realizations of a sketch are called its models The restriction on the shape of the constraints results in an easy definition of homomorphisms between models of a given sketch E which gives the category Mod E of models of E Actually sketches will be used here in order to sketch or specify specifications Indeed wefts of ambigraphs make up a relevant notion for specification in a purely functional setting Moreover in order to take into account implicit features of pro gramming languages we will use in guide2 wefts with respect to various categories A Each category A which we will consider is sketched by a sketch E which means that it is equivalent to the category of models of E 1 INTRODUCTION 3 For instance the category of ambigraphs can be sketched by a proj
62. re we restrict our definition to rather simple constraints Actually it is the definition of the realizations of a A weft as given in 2 5 which enlightens the meaning of the constraints Beforehand one constraint is studied in some detail in 2 2 2 1 Ambigraphs Ambigraphs are compositive graphs the definition of compositive graphs is given in A 2 with equations which are just pairs of arrows with the same rank Ambifunctors between ambigraphs are functors between the sublying compositive graphs which preserve equations It follows that ambifunctors from an ambigraph to a category map each equation to an equality Definition 1 An ambigraph G is a compositive graph together with 2 WEFTS 6 e a set of equations G Eq C G RankP whose elements are denoted g gr rather than 91 9r Let G and G be ambigraphs An ambifunctor y G G is a functor between the sublying compositive graphs such that e for all equation g gr of G the pair of arrows with the same rank p g1 p g is an equation p g1 91 of G An ambifunctor 4 G G is called an extension if it is an inclusion both on points and on arrows Then it is also an inclusion on identity arrows on composable pairs and on equations We say that G extends G Ambigraphs with ambifunctors are the points and arrows of a category Ambi Moreover let us consider a category of sets Set restricted to small sets see ref1 Its points are calle
63. rmines a functor from Ec towards Set Compo sition in Ez corresponds to the following properties of G e g G G for all identity arrow g of G e the codomain of g is equal to the domain of ga for all consecutive pair g1 g2 of G e the domain of ga o g is the domain of g1 and its codomain is the codomain of ga for all composable pair g1 g2 of G However there is nothing in Ecomp which corresponds to the following properties e the consecutive pairs are all the pairs g1 g2 such that the codomain of g is equal to the domain of ga e the maps G jraar G IdAr G Ar and G jcompp G CompP G ConsP are injections We will see in 3 4 how constraints can be added to E in order to lay down these properties Finally for ambigraphs let E be the following compositive graph COMPOSITIVE GRAPH E y extends points arrows composition Ecomp RankP Eq pi RankP Ar pr RankP Ar jeq Eq RankP dom o pp dom o pr codom o p codom o pr 3 PROJECTIVE SKETCHES 20 E api IdAr ConsP lt CompP er 7 IdAr A 2 Le hr _ codom Pr Pl RankP lt Eq JEq composition In a similar way each ambigraph G determines a functor from E y towards Set We will see in 3 4 how constraints can be added to E yy in order to lay down the following properties of G e the consecutive pairs are all the pairs g1 g2 such that the codomain of g is equal t
64. roperties Actually as is suggested by our notation G can be identified with a set valued realization of a weft Em It is a Comp weft i e a weft of compositive graphs the definition of the category Comp is given in A 3 The support of E Ambi is made up of points Pt Ar etc and arrows dom Ar Pt codom Ar Pt etc In addition the weft of compositive graphs E mp is a projective sketch because all its constraints are constraints of projective limits see A 5 Sketches were introduced by Ehresmann Ehresmann 66 Ehresmann 67a Ehresmann 67b Ehresmann 68 In Coppey amp Lair 84 Coppey amp Lair 88 they are presented in an elementary way Here we focus on projective sketches The set valued realizations of a projective sketch E are called the models of E We will see that it is easy to define the category Mod E of models of E The category Mod E Ambi is equivalent to the category Ambi of ambigraphs We say that the projective sketch E Ambi sketches the category Ambi A category A is projectively sketchable if it is equivalent to the category of models of some projective sketch Since we will be interested in A wefts for projectively sketchable categories A we now study projective sketches and their categories of models In 3 1 and 3 4 we build the projective sketch E wi In 3 2 projective sketches are defined Their models with the corresponding homomorphisms are defined in 3 3 A table in 3 5 sums up our terminology about w
65. rrow projfact p or fact p from P C to L C in V such that L pp o projfact p P pp for all point B of B This arrow is the projective factorisation or sometimes simply the factorisation of P with respect to L Let n B V It is easy to check that two limit projective cones L and L in V with the same base y are isomorphic Often one of these limit projective cones is chosen it is called the limit projective cone with base y in Y and denoted ProjLim n or ProjLim B gt V or sometimes omitting the arrows ProjLimpe g n B The vertex L C of the limit projective cone L is often called the projective limit of y Let us now look at special cases of limit projective cones which correspond to special typical bases Notations are the same as above Terminal point When the typical base B is empty the projective cone Cp 8 is made up of the vertex C alone OHT Then the vertex I L C of L is called a terminal point of V Its property can be stated as follows e for all point V of V there is a unique arrow projfacty y or projfacty or facts or facty V I When Y is the category of sets it means that Il is a one element set A APPENDIX ABOUT CATEGORIES 50 Product When the typical base B is discrete i e without any arrow except maybe some identity arrows the projective cone Cp B has no non trivial equation Then L is called the product of the n B for B B in V Its vertex is denoted
66. s L ig n bi x and L ig n b2 x which come from the same element x of 7 Bo and the maps L ip and L ip are the canonical injections Epimorphism This is a special kind of pushout With the same typical base B as above let us assume that 7 B n B2 and n b1 n b2 Let Vi 7 B1 Vo Bo and e m b1 Vo V1 Let us consider the inductive cone L with base n of vertex L C V and inductions L ip L is idy and L ig e Then it is easy to check that L is the pushout of y if and only if e is an epimorphism which means e for all pair of arrows v and va Vi V V10e V920 V V2 When V is the category of sets it means that e is a surjective map REFERENCES 54 References ref Christian Lair and Dominique Duval Sketches and specifications reference manual Rapport de recherche du LACO 2000 http www unilim fr laco rapports ref1 First part Compositive graphs ref2 Second part Projective sketches ref3 Third part Models guide Dominique Duval and Christian Lair Sketches and specifications User s guide Rapport de recherche du LACO 2000 http www unilim fr laco rapports Also D Duval idem Submitted for publication guidel First part Wefts for explicit specification This paper guide2 Second part Mosaics for implicit specification guide3 Third part Functional and imperative programs Work in progress state Dominique Duval and Christian Lair Mosaics
67. sed of the two arrows z Ey gt Ej and p Ej Es is interpreted in w as the integer pred 0 1 in wa as the map pred o succ Z Z i e as the identity map of Z and in w3 as the integer succ 0 1 e Adding equations we get an ambigraph which is a more precise kind of specification For instance let us add to Gin two equations p s x x and s p 1 x we get an ambigraph Gi n Ina realization of G the maps which interpret the arrows s and p are the inverse of each other Hence w1 and wy are realizations of G but w3 is not On the other hand thanks to equations we can evaluate programs for example we can replace the program p s s z by s 2 e Now adding constraints we get a weft of ambigraphs which is a still more precise kind of specification Like an equation a constraint both restricts the number of realizations and enriches the programming language For instance a constraint let us call it T allows us to say that whenever E is interpreted as Z then E gt must be interpreted as Z Let Sint denote the specification made up of the ambigraph G together with the constraint T then w is a realization of Sin but w2 is not On the other hand this constraint allows us to consider pairs like s z p z hence programs like a s z p z The pair s z p z is interpreted by w1 as the pair of integers 1 1 and a s z p z as the integer 1 1 0 As a consequence of their definition wefts a
68. shed B projective cone x Cp B G is outlined as follows Definition 6 A projective sketch E is a compositive graph E called the support of E together with a set of distinguished projective cones The points arrows of a projective sketch are the points arrows of its support A homomorphism of projective sketches p E E is a functor of compositive graphs p E E such that for all distinguished projective cone x C E of E the composed arrow pox C gt E is a distinguished projective cone of F Equivalently projective sketches are the wefts of compositive graphs with level lt 1 and constraints which are distinguished projective cones And homomorphisms of projective sketches are homomorphisms of Comp wefts between projective sketches This defines the category of projective sketches for size questions see ref1 and ref2 Psk 3 3 Models of a projective sketch Let E be a projective sketch The definition of models of E is given below they are the realizations of the Comp weft E But here in addition we are able to define in a simple way homomorphisms between these models Since we will only need set valued models we do not consider models of E towards other compositive graphs though it would not be any more difficult Definition 7 A model of E is a functor from the compositive graph E towards Set such that the image of each distinguished projective cone of E is a limit projective
69. t for all arrow e Ej Es of Epir PDir 1 E2 o pir G Ppir Pe o Opin th Er Por 9 Er gt Poy 9 Er In Dir In Mod Erir In Set G 9 a VO GE Jw ewe ewe g 9 INE gt ONE Indeed from the definition of Pp it means that for all arrow e Ej Es of Epir Ez o G e G e o p Er G E1 gt 9 Es Since Ep has only two arrows dom and codom both with rank Ar Pt the required property is the following one w Pt o G dom G dom o Ar and Y Pt o G codom G codom o Ar It means that for all arrow g Gi Ga of G the arrow w Ar g of G has domain Pt G and codomain 7 Pt G2 which is indeed true since is a homomorphism of directed graphs In this way we get a functor pir Dir gt Mod Ep Now it is easy to check that Pop is an isomorphism Thanks to this result we may identify directed graphs and models of Ep For all directed graph G we use G for p G In the same way for all homomorphism of directed graphs d G G we use y for Poy 1 Now let us add to the compositive graph Ecomp some constraints in order to lay down the following properties of each compositive graph G e the consecutive pairs are all the pairs g1 g2 of arrows of G such that the codomain of g is equal to the domain of ga e the maps G jraar and G jcompp are injections These properties can be stated as projective limits in the cat
70. the functor such that A gt A Then of course o D id y and 009 4 id it remains to prove that P o amp id 4 For this purpose let t A id4 A1 Az and t A2 a2 Ag Aj It is easy to check that this defines a natural transformation t id 0 0 and that t is a natural isomorphism Hence we get the required result Az A In Func A A ida p o In A Aj di e anf Ja ida Pida A2 t A2 a2 Ay A 5 Projective limits Definition 22 Let B be a compositive graph The typical projective cone of typical base B also called the typical B projective cone is the compositive graph C B made up of B a point C an arrow pp C B for all point B of B and an equation bo pg pp for all arrow b B B of B The point C is the vertex of the cone Cp B and the arrow pg is its projection towards B Definition 23 Let B and G be two compositive graphs A projective cone of typical base B also called a B projective cone in G is a functor x Cp B G The functor n xo Pg B G is the base of the projective cone x The point x C is its verter and the arrows x pp are its projections B EE 078 A APPENDIX ABOUT CATEGORIES 49 Definition 24 Let B be a compositive graph V a category and L C B Va B projective cone in V Then L is a limit projective cone if for all projective cone P C B V with the same base 7 as L i e such that 7 Po Pg Lo 8g there is a unique a
71. the model Yp L of E Map is made up of two sets VE E E 0 and Yp L E y and of the unique map Yp L e of to y e the homomorphism Yp e Ve E Ye E is made up of the unique maps Yp e F 0 x and Yp e E yy gt x In Mod E Map In Set Ya 0 23 Yr E 0 a L ty r Example 20 Let us consider the projective sketch E 4 5 described in 3 4 and let Y VE ayy Proposition 3 proves that Mod E ww is equivalent to Ambi hence V VE vu EAmbi gt Ambi The counter model Y interprets each point E of E Amb as an ambigraph Y E and each arrow e E gt E of E mo as an ambifunctor Y e Y E Y E For instance 4 BLOWING UP PROJECTIVE SKETCHES 39 e the ambigraph Y Pt is made of a single point denoted Y e the ambigraph Ar is made of two points Yq and Y and one arrow y Ya Ye e the ambifunctor Y dom Y Pt Y Ar is defined by Y Yq e the ambifunctor Y codom Y Pt Y Ar is defined by Y Y For all point E of Embi the following projective sketch can be obtained by a blow up Z E Esm V E Each Z E is a projective sketch as Eno and Z defines a contravariant functor Z Emi Psk For instance e the projective sketch Z Pt is made of a single point Pt Y e the projective sketch Z Ar is made of three points Pt Y Pt Y and Ar y and of two arrows dom y Ar y Pt Ya and codom y Ar y Pt
72. valence of proposition 4 to the point H oh of the category Weft Dir Ts The indexation HQ of S by Tp gives rise to the Mod Epir Zpart welt Dart NH Its support is T9 it AR see example 17 In order to describe its unique constraint let us first consider the models Zp h of En Loa where means C D or U see example 18 They are quite simple Zo AA E 2 0 except for Tart NA OPE 1 10 Y Ear NAS Pt 1 C D Tari Ahu Pt T 1C D and Zn Ny lar tot u The unique constraint of the Mod EDir Zlare weft Tai NH2 is denoted Tha ATT Its body is Tin Ax Tari ARE Toart hes defined by Zoare x Pt 1 CHU Its potential is T in NIT De Aor T part ARE Dart ARD Tari NhU where Zoi Nor and Zar N r are defined by the inclusions for all point E x of Epir Thon Zart Ahe LE part RD IE 2 Zart Ahu LE xl The loose homomorphism of Mod EpiZ0ayi wefts TN Thart NHS _ sc 2 Epir Z art extends the homomorphism Toii Al described in example 17 It is only a loose homomor phism of Mod Epjr Zparz wefts because on one hand Zpare hy Ur part 0 while on the other hand Sp Epir Zpart Ar part Sy Ar u hence both constraints are different Finally let us consider the realizations of this Mod Epir Tpart welt art A Set ipa VAE Ep Z 4 BLOWING UP PROJECTIVE SKETCHES 38 towards the p
73. versely the loose homomorphisms of A wefts do not behave well with respect to the realizations However this is not always a drawback For instance in guide2 this is the kind of property which we will be interested in Example 18 Let us consider the projective sketch Ep and the directed graph Toart from example 13 Proposition 4 states that Weft Dir T part Weft Dir Lo We now look at this isomorphism by an example Let us consider the following weft of directed graphs S example 13 and with the unique constraint U I Dir WEFT S support Ge terminal point U with support S G9 see 8 p s p Let us consider the indexation hf Ge gt Tari from example 13 as well as the indexations e h Cr gt Do rt such that Cr I e h Dr gt Dart such that C I De I e ht Ur Fr gt I DH I u tot To 4 BLOWING UP PROJECTIVE SKETCHES 37 Then AS extended by A h h makes up an indexation H9 of Sp by Da Hence H is a point of the category Weft Dir Zpart Now let us look at Ress h hh et A as four T rt indexations The homomorphisms of directed graphs x Cr G p yr Cr Dr and r Dr Ur give rise to Tari triangles x h9 gt ee YT he h and r hh gt h In this way we get a weft of Tf ayi indexations with support hlp and with constraint h 5R hQ 719 5h2 this is a point of the category Weft Dir Doo It corresponds by the equi
74. x The point x C is its vertex and the arrows x pg are its inductions B Ci B Definition 27 Let B be a compositive graph V a category and L C B Va B inductive cone in V Then L is a limit inductive cone if for all inductive cone I C B V with the same base 7 as L there is a unique arrow indfactr p from L C to I C such that indfact p o L ig oI ig for all point B of B This arrow is the inductive factorisation of I with respect to L A APPENDIX ABOUT CATEGORIES 52 Let n B V It is easy to check that two limit inductive cones L and L in Y with the same base 7 are isomorphic Often one of these limit inductive cones is chosen it is called the limit inductive cone with base 7 in V and denoted IndLim n or IndLim B V or sometimes omitting the arrows IndLimpeg n B The vertex L C of the limit inductive cone L is often called the inductive limit of n Let us now look at special cases of limit inductive cones Initial point When the typical base B is empty the inductive cone C B is made up of the vertex C alone C C Then the vertex O L C of L is called an initial point of V Its property can be stated as follows e for all point V of V there is a unique arrow indfactg y or indfacty O gt V When Y is the category of sets it means that O is the empty set Sum When the typical base B is discrete the inductive cone C B has no non trivial equation The
75. y Y Ar On one hand the models of Z Ar are the pairs of maps with the same domain they are called the set valued spans On the other hand the indexations of ambigraphs by Y Ar are the ambifunctors h G Y Ar Such an indexation h is characterized by the three sets Xy h Pt Ya X h Pt Y and X h Ar y which satisfy G Pt X4 U Xe and G Ar X and the two maps G dom G codom X Xa O X such that G dom X Xq and G codom X Xe Consequently h is characterized by the set valued span CEA es where fq and fe re spectively denote the restrictions of G dom and G codom Xa Xe G Pt ae lt a Xa R Xe V Ar dom rss A h Ar ar Ar y la x G ar J Ar Pt Ya Ye The ambigraph G from example 1 cannot be indexed by Y Ar since the point N is both a domain for s and a codomain for z and s 4 BLOWING UP PROJECTIVE SKETCHES 41 But the ambigraph Go Go can be indexed in two ways by Ar indeed all arrows of Go must be indexed by y and the points G1 G2 and G3 resp G4 and G5 must be indexed by Yq resp Y since they are domains resp codomains But Gg which is neither a domain nor a codomain can be indexed either by Yq or by Y These indexations h and hg correspond respectively to the set valued spans G1 G2 G3 G6 G1 G2 G3 j Se ee 91 92 93 ga 91 92 93 ga AR GaGa Y Ga Gs Go The fundamental result on the Yoneda counter mode

SKETCHES AND SPECIFICATIONS USER'S GUIDE First part: Wefts

Contents

Download Pdf Manuals

Related Search

Related Contents