Home

SKETCHES AND SPECIFICATIONS USER'S GUIDE Second part

1. acc u mod This altogether is a simplified mosaic X The indexation in this example is a special case of a more general notion called a stratification property names apparent weft ex st acc mod ex S properties stratification ex static access modification ez s gt st r acc u gt mod 1 INTRODUCTION 4 Our claim is that the mosaic gives at least as much information as the weft S This will be proven by the construction of S from X using a ribbon product S Expl X We call Expl 2 the explicit weft associated with gt We will define the set Real 2 V of realizations of a mosaic 3 towards any ambigraph V directly from the components of X properties and stratification We will prove that these realizations are the same as the realizations of S by the fundamental theorem on the ribbon product Real X Y Real Expl 2 V In the above example this proves that the realizations of X yield the required meaning This result states that implicit features can be made explicit thanks to the weft Expl 2 which is often quite large and intricate This fact is well known from experience here it becomes a theorem which is similar to the fundamental result on tensor products in category theory Actually the mosaic X gives more information than the weft S For instance in our example it can be proven that with the mosaic the use of the point E x E can be forbidden guide3 In fact the
2. The inclusions r E i v E i u E now define a homomorphism r v pop of set valued realizations of F Thus the triple y v r determines a p stratification F E E M uH d Set j 5 5 Contravariant functor O W Set As in 2 5 let W denote the category of wefts of ambigraphs W Weft A where A Ambi and let O denote the left exact contravariant functor O Real4 Set W gt Set 5 6 Counter model F gt W As in 2 7 each comment K E i corresponds to a weft of ambigraphs amp E i in the sense that the interpretations which satisfy the comment K Ei can be identified with the set valued realizations of amp E i A WEFT k Pt Err k Pt A WEFT k Ar for 2 amp Ar A WEFT k Ar ok extends K Ar for arrow k H H equation k ohj hgok he s Ar ok Hi Hi H Ht He 1 E ja pe h Ha BH Ha 45 HS 1 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 41 A WEFT k Ar err extends K Ar for arrow k Hi gt HS equation k z h ok k Ar err H H H4 Ht A ecc gt Hi ciu qup cH WES Ww H 3 Hi Hy Hz H I Now it is easy to get a counter model F W of the projective sketch F towards the category W K IdAr ok For all i for ok err HOMOMORPHISM k dom amp Pt Err k Ar il lines K Pt Err gt k Pt Err HOMOMORPHISM k codon i
3. k Pt Err k Ar i lines amp Pt Err gt k Pt Err 2 For all i ok err HOMOMORPHISM k lidar gt for k Ar for k Ar i it is the extension A WEFT k RankP for for k RankP A WEFT K Eq eg amp Eq And so on In this way we get a counter model R Fi W 5 7 Ribbon product amp B r From the study above e the interpretation of an ingredient x of v of nature E i for all point F i of F should be an element of the set Real 1 E il Set In addition if x is in v E i for several values of 7 then these interpretations should be compatible Now this study can be carried on in two ways 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 42 1 By composition of the counter model x F gt W and the contravariant functor O W Set which is left exact we get a set valued realization of F O o k Real 1 k Set F Set which interprets each point E i of F as the set Real mo amp E 1 Set of set valued realizations of the weft of ambigraphs k E i From the study above the natural numbers with the predecessor map define a homomor phism from v to O ok i e an element of the set Hom woa r 7 Oo K Precisely as in 2 points U U ZU eu Ne NENG en arrows z gt 0 s succ p gt pred 2 With the second point of view we consider for all point U and N of y a copy of k Pt Err for all arrow z and
4. Let us check that the set valued realizations of S are irrelevant Each set valued realization of S interprets U N z and s respectively as U N 0 and succ because of the constraints It also interprets p as a map pred N N such that pred n 1 n for all n N because of the equation Hence the value of pred 0 is a natural number instead of an error Since the set Real Ambi S Set of set valued realizations of S is irrelevant we are going to build two other sets of realizations which are much more relevant 1 on one hand the set of realizations of S in an ambigraph different from Set Real 4mbi S 2 on the other hand the set of set valued realizations of a weft of ambigraphs different from S obtained from S by a crown product Real Ambil S Set As we will see both points of view lead to the same result but this result is not wholly satis factory It is only in 5 thanks to a more subtle approach that we will get a good answer to the question of dealing with natural numbers with a predecessor operation 2 CROWN PRODUCT AN EXAMPLE 8 2 2 Comments It follows from 2 1 that we do not look at the set valued realizations of S Instead we look at some interpretations in a sense which has to be defined of S which satisfy the following comments The interpretation of each point of S should satisfy the comment e K Pt the interpretation of a point G satisfies K Pt if it is made of a set X
5. image of Pt I U N image of Ar tot 2 5 id image of Ar func z s idN p pos image of lidar tot func the inclusion image of Eq funcz func pos idw etc STRATIFICATION Tsp Hsp gt Gs p Dfunc image of Pt I the identity of U N e image of Ar tot the inclusion z s idv 12 s idy p po s image of Ar func the identity of z s idv p po s image of Eq func z func the identity of po s idy etc p unc F func Ejsunc Ts p ee d Hs p Set Gs p 4 2 Ribbon product The definition of the ribbon product follows directly from the definitions of the crown product and the stratifications Thanks to the crown product we may define the interpretations of a weft which assign to each point a set with some given property the same property for all points to each arrow a map with some given property the same property for all arrows and so on If a stratification is used before the crown product it becomes possible to assign sets with distinct properties to distinct points maps with distinct properties to distinct arrows and so on see 5 for an example We consider a homomorphism of projective sketches p FE a cocomplete category Ww and a counter model of F towards W k F W Definition 6 Let u v r v po p be a p stratification The ribbon product of k by r over p is the point of W KG r kQOrv It follows immediately from
6. the symbol x to the right of J returns a value which is a natural number and does not need any argument on the other hand the symbol x to the left of needs an argument of natural number type and does not return any value Hence let us consider the following weft of ambigraphs S It has a point N and an arrow s N N to be interpreted as the set N 1 INTRODUCTION 3 and the map succ as well as a point U with the constraint U and two arrows r U N and u N U which are formal artefacts for translating respectively the symbols x and x Then the instruction J corresponds to the term p r o s o u of S pL AN GU With this point of view the weft is smaller the term is simpler and in addition it preserves the shape of the instruction But it does not seem to have any meaning indeed in any set valued realization w of S the interpretation of U is a one element set U and the interpretation of p is the unique map from U to U i e the identity of U This means that p does not change anything whereas of course the instruction does change something We might look at realizations of S towards another ambigraph V but the result would be similar the interpretation of U is a terminal point Vr of V hence the interpretation of p is the unique arrow with rank Vr Vr in V namely the identity arrow of Vr However we claim that e the term p can be interpreted in a generalized s
7. COMMENTS wee Rer Tuan Poe ata al RI U UE a Rogue eat 5 3 Homomorphism p F E A ied ete a etie s rrr Roh Noe C fee tg sape Rue tdt 5 5 Contravariant functor O Wi Set 5 6 Counter model k F gt Y les of Ribbon product RU A A RIA A A v E RS E gs 5 8 Terminal point constraint 5 9 Initiality constraint 5 10 Conclusion 2 2 e uel vom ege E RU Reps Dow Laine a le bue 5 11 Product constraint 4 19 a pO wey Boe ee OM a Rub n Re Y Dat ee eee quy sy 5 12 Other deduction rules 6 Conclusion 55 D 0000000 M Rth DQ Ot 18 18 20 21 23 23 30 31 35 35 36 37 39 40 40 41 43 45 45 45 49 52 Index apparent weft 32 cocomplete 18 crown product 18 20 crown product functor 19 explicit weft 32 homomorphism of stratifications 24 index 26 lax colimit 25 left exact 18 mosaic 31 realization 32 ribbon product 30 31 satisfaction 20 26 stratification 24 56
8. Og y Let amp Og S1 denote the weft of ambigraphs made of the support of k Og u the four con straints of k Ox p and the constraint k g T over the support of k Og u also The elements of the set O x Or 1 are the set valued realizations of amp Og S1 ie the set valued realizations of Og which satisfy the constraint x QE l It is easy to check that in this way as above the interpretation of U should be a one element set and not a two element set as required In this example neither of these two points of view meets our requirements However both are equivalent Indeed corollary 1 will prove the existence of a canonical bijection O amp Og 81 Real uga g 81 O 0 amp or equivalently Real Anvi amp OE mi 81 Set Real Amoi S1 Real abi K Set 2 9 Initiality constraint Now let us handle in the same two ways the initiality constraint of S which says that the interpretation of U NN is initial among the on xy where Xo is terminal It is easy to check that we get the following result the interpretation of N is up to isomorphism the same as the interpretation of U i e a one element set and the interpretation of z as the interpretation of s is the identity This means that natural numbers have disapppeared this is not at all what is required 2 CROWN PRODUCT AN EXAMPLE 16 2 10 Conclusion The previous study is related to the approach using monads Moggi 91 Wa
9. amp E where E x is a point of E which means that E is a point of E and x an element of u E This construction runs as for the example in 2 it amplifies each ingredient x of u of nature E into k E and merges these amplifications More precisely for all point E x of El u we consider a copy amp E x of the point amp E of W For all arrow e zi E1 zi E2 x9 where z9 u e z1 of E we consider a copy amp e 21 amp Eo 12 gt K E1 1 of the arrow k e K E2 gt k E of W Then in the category W these points amp E x are merged together 3 CROWN PRODUCT 19 according to the arrows amp e x this is the inductive limit IndLimq g y amp E which does exist because W is cocomplete Let h 1 u2 be a homomorphism of models of E We define the arrow of W k Or k Or 1 gt KOR pa from the identity arrows from amp E x1 towards k E h E x1 both are equal to amp E for all point E of E and all ingredient x of 4 of nature E In this way we get the crown product functor k Og Mod E W The fundamental property of the crown product below states that there is a canonical bijection between the set O amp Og and the set of homomorphisms of y towards O o amp as models of E Proposition 1 For all model y of E there is a canonical bijection O s Os 1 Hom mou 11 O 0 amp eet k E p EW Hu ge Set About the proof The proof of this resu
10. and pz of N on N are arrows of O o x since they are set valued realizations of k Ar We now prove that NP N 2 9 N is the interpretation of N N 2 N First in the category of sets since N N gt N is a cartesian product for all set Y and all pair of maps fi Y N f Y N the map f fact f f Y N is defined by FW 9 Gt Ey for all y Y If in addition Y has an error element and if fi and f propagate the error then f will also propagate the error It proves that N N 2 N is a product in Ook Y Y ey pu e ASN ex In this way up to isomorphism N m and 7 are interpreted as N p and po But this is not was we wish Indeed N NU ey is different from N N U eye it has elements like ey x2 with z2 n and z1 n with z ey which we want to avoid It follows that of these three constraints in 2 8 2 9 and 2 11 none is correctly handled by the crown product We will see in 5 that they can be handled correctly thanks to a ribbon product However in 3 we will use this section in order to illustrate the definition of the crown product 3 CROWN PRODUCT 18 3 Crown product This section is devoted to the study of the crown product Let e E be a projective sketch e W a cocomplete category i e a category such that for all base B W there is in W an inductive limit cone with base 7 e k E
11. hz 0 hy kj ho hao i har kha ho o hao hz o hap go hao hare haa igs haz c p d Io Ta and for 1 and 2 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 49 HOMOMORPHISM k pc ceq k RankP for for amp PEq ceq lines amp Pt Err 1 gt k Pt Err o k Pt Err a gt k Pt Err arrows kk kg koi kg kaio ka Kaa Now let vy PEq ceg uu PEq c1 ou d1 c2 0 u d2 In this way fact t1 t2 is defined as required given two terms t T N and tg T N of S the term t fact t1 t2 T N is defined once t and ta satisfy K Ar for However of course if fj f and f denote the interpretations of 1 t2 and t generally p o f is different from fj and p5 o f is different from f We only have as required the partial equalities p o f y fi y and ph o f y faly for all y def f def f1 N def fa 5 12 Other deduction rules Let us come back to the ribbon product k 9 R as in 5 8 From the information we have about the interpretations of p and s we may deduce that the interpretation of po s propagates the error nothing more On the other hand the interpretation of idw is an ok map Since the equation p o s id y is part of S clearly the interpretation of posis also an ok map We will see how it is possible to extend F and p in order to express the deduction rule e ifthe interpretation of the right hand si
12. 4 W a counter model of E e and O W gt Set a contravariant functor which is left exact i e which maps each inductive limit cone in W to a projective limit cone in Set Ress W a Set The crown product amp QE y of k by a model y of E is defined in 3 1 Proposition 1 general izes 2 7 amp Og u is a point of W which is mapped by O on the set of homomorphisms from y towards O o k Then in 3 2 we use the functoriality of amp Og y with respect to u in order to define the crown product amp Og S of amp by a weft S of models of E The fundamental result on the crown product is theorem 1 In 3 3 we assume that W Weft A In this important case we prove corollary 1 This result generalizes what could be seen in 2 8 amp Og S is a point of W and it is mapped by Real 1 A for all point A of A on the set of realizations of S towards Real A amp A These definitions and results can be illustrated by the example considered in 2 3 1 Support We may now define the crown product k Og u of k by a model y of E It is a point of W and its image by O is characterized by proposition 1 Definition 1 Let y be a model of E The crown product of k by u over E is the point of W k Og u IndLim E p E s4 wW In this definition though amp o EN y is a model of EA y towards W it is only the sublying functor which is used for the construction of the inductive limit We may also write k Ox u IndLimi z jy
13. Ehrig and Fernando Orejas Dynamic abstract data types An in formal proposal Bulletin of the European Association for Theoretical Computer Science 53 pp 162 169 1994 Ehrig amp Orejas 98 Hartmut Ehrig and Fernando Orejas Integration paradigm for data types and process specification techniques Bulletin of the European Association for Theoretical Computer Science 65 pp 90 97 1998 Filliatre 99 Jean Christophe Filli tre Proof of imperative programs in type theory In Pro ceedings of the TYPES 98 workshop Lecture Notes in Computer Science 1657 Springer Verlag 1998 Freyd 73 Peter J Freyd Properties invariant within equivalence types of categories In Eilen berg Festschrift Academic Press 1973 REFERENCES 54 Freyd amp Scedrov 90 Peter J Freyd and A Scedrov Categories Allegories Mathematics Library 39 North Holland 1990 Gaudel et al 99 Marie Claude Gaudel Carole Khoury and Alexandre Zamulin Dynamic systems with implicit state In ETAPS 99 Lecture Notes in Computer Science 1577 pp 114 128 Springer Verlag 1999 Goguen 78 Joseph A Goguen Abstract errors for abstract data types In E J Neuhold editor Formal Description of Programming Concepts pp 491 525 North Holland 1978 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
14. Our aim is to generalize this result to languages with implicit features like imperative lan guages For this purpose in this paper we define the mosaics their terms and their realizations As usual the realizations give the meaning while the terms determine the programs However the terms of a mosaic are the terms of some weft S called apparent whereas the realizations of X can be identified to the realizations of another weft S called explicit The construction of the explicit weft S from gt enlightens the relation between the implicit and the explicit points of view on specifications for example specifications with implicit state or with explicit state as in the example below It also proves that the implicit point of view contains more information than the explicit one The implicit point of view is also much better suited to the study of programs and computation this will be seen in guide3 Let us now consider a typical example of imperative programming including a notion of state and an assignment of a value to a variable in the computer science meaning Let I denote the instruction r rcl where x is a variable of type in the computer science meaning natural integer It is well known Dauchy amp Gaudel 94 that the instruction can be made into a functional program at the price of some serious drawbacks For this purpose let us consider the following weft of ambigraphs S and its set valued realization w
15. is defined by CCB wneENn2pNy The arrows c and c should satisfy K Ar ok since the projections p and p5 are ok maps On the other hand the arrows d and da should only satisfy K Ar for since their interpretations fi and fj are any maps which propagate the error Similarly the arrow u should only satisfy K Ar for since its interpretation f has no other property generally than the propagation of the error Now we introduce a new comment for the equations c ou d and co ou d of Hu First both equations c o u d and co o u do which have the same domain D are considered as a unique ingredient of 14 For this purpose we add to E this is a conservative extension e a composed arrow domeq domo pg o jeq domo pao jeq Eq Pt in order to get direct access to the common domain of both sides of an equation e point PEq e two arrows proj PEq Eq and proj PEq Eq e and the distinguished projective cone pgg which says that PEq should be interpreted as the set of pairs of equations with the same domain e in addition in order to be able to speak about the two pairs of arrows with the same rank which are part of each pair of equations with the same domain we also add to E the composed arrows PC jgq proj PEq RankP PCy jeq proj PEq RankP Then the pair c ou d1 c2 o u da belongs to the set wy PEq it is a pair of equations of Lu with
16. its set valued realizations are irrelevant In order to get more relevant realizations we can try 1 either to look at non set valued realizations of S 2 or to look at set valued realizations of another weft of ambigraphs which might be built from S using a crown product Both points of view are studied here first in 2 7 for the support of S then in 2 8 and 2 9 for its constraints Since the set valued realizations of S are irrelevant the first thing to do is to say precisely how each ingredient of S should be interpreted This is done in 2 1 and 2 2 2 1 Analysis Let us now give a precise statement for our example The predecessor of 0 is an error i e an element ey which is not a natural number Hence the predecessor is pred N N where N NU en with the symbol U denoting the disjoint union and pred 0 en Moreover in order to propagate the error when maps are composed the successor map succ N N is extended to a map succ N N such that succ en en In the same way pred N N is extended to pred N N such that pred ey en Now as in guidel let U x denote a one element set and 0 the constant map 0 U N The unique map facty N U such that n x for all n N can also be useful Hence it should propagate the error which means that it should be extended to facty N U where U UU ey eu in such a way that facty en eu Then the constant
17. level 0 then c a If S has level n 21 then S is made of the A weft S together with for all constraint I of S the constraint D over S defined as follows using the functoriality of Let us consider the body of I x 58 inw and its potential cpu in Weft W Then D is the constraint with body x C S in A and with potential o C 2 oy uy This is indeed a constraint over S because C koc Ifo S S has level n gt 1 then we chec which is denoted in Weft A S defines a homomorphism of A wefts a S S5 Then clearly S 2S and it is easy to check that Real4 A weg S Real4 S A for all point A of A The following result follows immediately from theorem 1 Corollary 1 Assume that W Weft A for some cocomplete category A For all point A of A and all Mod E weft S there is a canonical bijection Real 1 1 Or S A Real moa S Real 1 x A K EPA E pe k Og S Weft A W A ealA A BEC Ie as Set 4 MOSAICS AND RIBBON PRODUCT 23 4 Mosaics and ribbon product In this section is introduced the key notion of weft mosaics They form a new tool for specification which generalizes wefts hence algebraic specifications In 2 we used a ribbon product in order to amplify a weft of ambigraphs S according to a counter model amp of E55 This was not sufficient for our purpose because all arrows of S were amplified in the same w
18. map 0 U N should also be extended to 0 U gt N such that 0 ey en U U UL eu lt ev ar N N NU en lt en 6 pred SUCE succ pred 2 CROWN PRODUCT AN EXAMPLE 7 To sum up each set X gives rise to a set X X U ex disjoint union of X and of an element x called the error and each map f X Y resp f X Y gives rise to a map f X Y which extends f and which propagates the error which means that f ex ey Now let us look at the programs they should be written without mentioning any error This means that they should be written as if the predecessor map had all its values in N So that a program can be defined as a term of the following weft of ambigraphs S Ambi WEFT S points U N arrows z U gt N s N gt N p N gt N equation pos idy terminal point U initiality constraint the interpretation of U N N is initial among the BCE ES where Xo is terminal the support of S is Ua and its constraints are described in guidel section 2 4 The description of S is given here in its abbreviated form Because of the equation S also includes the identity arrow idy N N and the composed arrow pos N gt N In a program the arrows s and p can be composed at will indeed so po z is a term of S as well as po so z Independently the error handling should be such that s o p o z is recognized as erroneous whereas po so z is not
19. s a copy of k Ar ok and a copy of k Ar for for the arrow p a copy of k Ar for for the arrow poz a copy of k Ar err and a copy of k Ar for and so on Then we merge these wefts k E i together according to the homomorphisms k e j The weft of ambigraphs which we get is amp Or v By definition this is the ribbon product Kpr A WEFT amp 9 r lines K Pt Err u k Pt Err w arrows k Hy gt Hy k Hy gt Hy k Hi gt Hy ks Hn gt Hy ky Hy gt Hy k HS Hs k Hy Hy kp HA gt HRS ke Hi gt Hg equations k ohy hy o kz ko h hs o k k ohy hy 0ks ko hs 2 hy o ke k o hy hy o kg kl o k 2 hS o kz kpo k idp equations In this example the homomorphisms k idar ok for and k idar err for are extensions Consequently when we consider for instance for the arrow z a copy of 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 43 k Ar ok and a copy of k Ar for and when we merge them together according to k lidar ok for the result is just a copy of k Ar ok This is another way to say that if the interpretation of an arrow satisfies K Ar ok then it also satisfies K Ar for From the study above the natural numbers with the predecessor operation define a set valued realization of amp 9 r i e an element of the set O amp g r Precisely points Hy U Hy U Hf ev Hy oN Hy N Hi en arrows k
20. set Real 1 S A of realizations of S towards A The A weft S specifies each of its realizations These notions are now generalized Definition 8 An A mosaic is made up of e a homomorphism of projective sketches p F E 4 MOSAICS AND RIBBON PRODUCT 32 e a weft of p stratifications S T R T S o p e and a counter model amp F gt Weft A p S E Weft A W T S Set Then S is called the apparent weft of the A mosaic X and is also called an A mosaic of S Definition 9 Let N p F gt E R T gt Sop k F gt Weft A be an A mosaic and let A be a point of A A realization of E towards A is a realization of T towards Real x A Real 1 2 A Real uoa r T Real 1 x A If Y is an A mosaic a point of A and w a realization of 3 towards A then we say that Y specifies w with respect to A and A As in guidel section 2 5 this is only half of what is needed for mosaics to be a good specification tool The second half related to programs will be seen in guide3 indeed A mosaics will allow us to deal with imperative programming Now let us check that mosaics do generalize wefts Let S be an A weft and assume that A is projectively sketchable i e Mod E for some projective sketch E Since A is a subcategory of Weft A the Yoneda counter model of E guidel section 4 4 VE E 4 A determines a counter model also denoted Vg from E towards Weft A The Yoneda lemma for p
21. specification Goguen et al 78 Astesiano et al 99 e category is sketched by a sketch E if A is equivalent to the category of models of E A Mod E Set For example the category Ambi is sketched by the projective sketch E Ambi e Given a projective sketch E each model y of E determines another projective sketch the blow up Ely of E by y On the other hand a indexation is a homomorphism h v p of models of E it is a point of the category Mod E Set u of ji indexations The fundamental property of the blow up states that the category of models of El y is equivalent to the category of j indexations Mod E Set u Mod E y Set This paper is devoted to the definition of mosaics and their realizations and to the study of a construction called the ribbon product which assigns to each mosaic a weft with the same realizations large part of this paper deals with an example A comprehensive study of the ribbon product will be found in our reference manual Several papers in progress deal with applications of these ideas to various implicit features of computer languages The only prerequisite to read this paper is guidel Implicit features in computer languages include side effects error handling partiality over loading coercions They can be found in all computer languages at various degrees They are fundamental in mperative languages like Pascal or C while they are of minor importance in applicativ
22. the crown product the Yoneda lemma for projective sketches states that Ve QE 3 CROWN PRODUCT 20 It means that the Yoneda counter model is a unit for the crown product The definition of the crown product uses a blow up of the composition graph E in order to count the ingredients of E in a proper way However it does not use the fundamental result on the blow up as stated in guidel section 4 2 3 2 Constraints We now define the crown product k OgS of k by a Mod E weft S This is a W weft and its definition is quite simple thanks to the functoriality of the crown product amp Og y with respect to u Theorem 1 is easily deduced from proposition 1 It characterizes the image of amp OgS by a functor Oyyef which is defined from 6 As noted in guidel section 2 6 the functor k Og Mod E W can be extended to a functor Weft amp Og which is still denoted amp Og since this cannot lead to any mistake between the corresponding categories of wefts k Or Weft k QE Weft Mod E Weft W This functor amp Qg has been defined recursively according to the level of the wefts For all Mod E weft S the W weft k Og S has for support amp Og S and for constraints amp Og IT for all the constraints I of S Definition 2 Let S be a weft of models of E The crown product of k by S over E is the W weft KOES On the other hand for all point M of W the definition of the realizatio
23. 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 guide2 Second part Mosaics for implicit specification This paper guide3 Third part Functional and imperative programs Work in progress state Dominique Duval and Christian Lair Mosaics for specifications with implicit state Rapport de recherche du LACO 2000 http www unilim fr laco rapports Also D Duval idem Submitted for publication Astesiano et al 99 E Astesiano H J Kreowski and B Krieg Brckner Algebraic Foundations of Systems Specification Springer 1999 Astesiano amp Zucca 95 Egidio Astesiano and Elena Zucca D oids a model for dynamic data types Mathematical Structures in Computer Science 5 pp 257 282 1995 Dauchy amp Gaudel 94 Pierre Dauchy and Marie Claude Gaudel Algebraic specifications with implicit state Rapport de Recherche 887 Universit de Paris Sud Laboratoire de Recherche en Informatique 1994 Ehresmann 66 Charles Ehresmann Introduction to the theory of structured categories Tech nical Report 10 University of Kansas at Lawrence 1966 Ehresmann 68 Charles Ehresmann Esquisses et types de structures alg briques Bulletin de l Institut Polytechnique Iasi 14 pp 1 32 1968 Ehrig amp Orejas 94 Hartmut
24. ORPHISM E Ambi ME func E AnbiNL func E Ambi points Pt I Ar func Ar tot IdAr tot ConsP 71 2 and CompP i1 i2 for all i and i2 in func tot RankP ig i4 for all ig and ig in func tot Eq funcz func arrows dom func codom func Ar func Pt I dom tot codom tot Ar tot Pt I etc IdAr tot ConsP tot tot lt CompP tot tot Pt RankP func func Eg eq composition Our aim is to generalize example 1 in the following way The point Pt J will be interpreted as the set of sets and the points Ar tot and Ar func respectively as the set of total functions and the set of all functions In order to take into account the fact that each total function is a function E Anvi ML fune is extended by an arrow from Ar tot towards Ar func which will be interpreted as the inclusion of the set of total functions into the set of all functions In other words we are building a homomorphism of projective sketches Pfunc F func Ejsunc gt 4 MOSAICS AND RIBBON PRODUCT 29 which extends the fibration E Ambi Zfunc but which is no more a fibration There are only minor differences between E 4 5 and Eye in particular their models are the same ones On the contrary F fune is significantly different from E Ambi M func PPROJECTIVE SKETCH Ep extends E nbi identity arrow idar Ar Ar PROJECTI
25. Paco Laboratoire d Arithm tique de Calcul formel et d Optimisation ESA CNRS 6090 SKETCHES AND SPECIFICATIONS USER S GUIDE Second part Mosaics for Implicit Specification Dominique Duval amp Christian Lair Rapport de recherche n 2000 04 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 Second part Mosaics for Implicit Specification Dominique DUVAL Universit de Limoges Laboratoire d Arithm tique Calcul formel et Optimisation 123 avenue Albert Thomas 87060 Limoges Cedex France dominique duvalQunilim fr and Christian LAIR Universit Denis Diderot Paris 7 U F R de Math matiques quipe 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 arranged i
26. Set In addition it is easy to check that the interpretation of the identity arrow idy should be a set valued realization of k IdAr that the interpretation of the pair of compos able arrows s p should be a set valued realization of k CompP that the interpretation of the equation p o s id yy should be a set valued realization of amp Eq and so on To sum up e the interpretation of an ingredient of y of nature E for all point E of E should be an element of the set Real A amp E Set Now this study can be carried on in two ways 1 The composition of the counter model k E gt W and the contravariant functor O W Set which is left exact is a model of E O o k Real4 K Set E Set It interprets each point E of E as the set Real A amp E Set of set valued realizations of the weft of ambigraphs amp E E m Mi Ook H Q Set Since O o k is a model of E it is an ambigraph From the previous study the natural numbers with the predecessor operation define a homomorphism from p to Ook i e an element of the set Hom Mod E 4 Oo K E 2 CROWN PRODUCT AN EXAMPLE 13 Precisely points UHR U U eu N gt N N en arrows z 0 se succ p pred 2 Here is another point of view Since we would like to interpret the point U of y as a set valued realization of amp Pt we replace in yy the point U by a copy of amp Pt We do the same for the point N Then we replace each a
27. The weft of ambigraphs S has two points N and E which are interpreted respectively by w as the set N of natural numbers and the set E of the states of the machine Here the state is explicit because it is represented by a point E in the weft In addition S has three arrows s N N r E Ex N and u Ex N E where s is interpreted by w as the map succ r as the map read the value of x and u as the map update the value of x Then the instruction J corresponds to the term p uo idg x s or of S idgxs SS ExN ES ES INR The interpretation of p is a map which assigns to each input state ein in E an output state eout in E where the value of x is incremented However this point of view becomes rapidly untractable because of the size of S and the occurrence of E nearly everywhere see Dauchy Gaudel 94 In addition the programs cannot be identified with the terms indeed the term p is fairly different from the instruction Another drawback is that with this point of view it is difficult to forbid adding to the weft the point E x E interpreted as E though this is generally not wished Actually there is a second way to build a term corresponding to the instruction This point of view is most naive and does not seem to have any meaning Looking at the instruction in a formal way without any attempt to understand its meaning we get the following information
28. Trends in Programming Methodology Volume IV Data Structuring chapter 5 pp 80 149 Prentice Hall 1978 Gurevich 91 Yuri Gurevich Evolving algebras A tutorial introduction Bulletin of the Euro pean Association for Theoretical Computer Science 43 pp 264 284 1991 Gurevich 99 Yuri Gurevich The sequential ASM thesis Bulletin of the European Association for Theoretical Computer Science 67 pp 93 124 1999 Hopcroft amp Ullman 79 John E Hopcroft and Jeffrey D Ullman Introduction to automata theory languages and computation Addison Wesley 1979 Lafont 88 Yves Lafont The linear abstract machine Theoretical Computer Science 59 pp 157 180 1988 Lair 87 Christian Lair Trames et s mantiques cat goriques des syst mes de trames Dia grammes 18 pp CL1 CL47 1987 Lair 93 Christian Lair El ments de th orie des patchworks Diagrammes 29 pp CL1 CL29 1993 Lellahi amp Zamulin 99 Kazem Lellahi and Alexandre Zamulin Dynamic system based on up date sets Rapport de Recherche 99 03 Universit Paris Nord Institut Galil e LIPN 1999 Moggi 91 Eugenio Moggi Notions of computation and monads Information and computation 93 pp 55 92 1991 Wadler 85 Philip Wadler Monads for functional programming In J Jeuring and E Meijer editors Advanced Functional Programming Proceedings of the Bastad Spring School 1985 Lecture Notes in Computer Science 925 Springer Verlag 1985 Wadler 90 P
29. VE SKETCH F func and HOMOMORPHISM Pfunc F func Efunc extends E Ambi NLfunc and E Ami NL func arrow idar tot func Ar tot Ar func Although it is above the identity arrow idar the arrow id ar tot gt func is not an identity arrow The notation tot gt func refers to the property if a function satisfies tot then it will also satisfie func Let us consider the pfunc stratification Func H func func F func MODEL Hyunc image of Pt I all the sets image of Ar tot all the total functions image of Ar func all the functions image of idar tot func the inclusion of the set of total functions in the set of functions image of Eq func func the equalities f f for all function f etc STRATIFICATION T func Hfunc Func Dfunc image of Pt I the identity of the set of sets image of Ar tot the inclusion of the set of total functions in the set of functions image of Ar func the identity of the set of functions etc p unc F func Esunc Tfunc D UND H fune Set Func Now let us consider the ambigraph Gsp AMBIGRAPH Gs p extends S o equation pos idn In order to say that each arrow of Gsp should be interpreted as a function and that in addition the interpretations of the arrows z and s should be total functions we consider the following Pfunc Stratification Gs p Hs p Tsp F func MODEL Hsp 4 MOSAICS AND RIBBON PRODUCT 30
30. al with the treatment of errors It would be easy to analyse other examples involving error handling using the same properties but changing the apparent weft and the stratification Our first version in 2 using the crown product in a naive way is not powerful enough Our second version in 5 gives a much better result thanks to a mosaic and a ribbon product 2 CROWN PRODUCT AN EXAMPLE 6 2 Crown product an example Examples here and in section 5 address the issue of computing with natural numbers with a predecessor operation as described now The set N of natural numbers is freely generated by the element 0 and the successor map succ N N We wish to add a predecessor map such that pred succ n n for all n N and such that any attempt to compute the predecessor of O returns an error In addition in order to keep them simple the programs should be written without any mention of a potential error error handling should remain implicit This section is devoted to the study of a first way to deal with this example which as we will see is not wholly satisfactory However this method leads to the introduction of the crown product in 3 then the crown product is used in 4 to define the ribbon product finally thanks to the ribbon product a much better way to deal with this example is given in 5 In 2 1 an analysis of the example leads to a weft of ambigraphs S which does not mention the error it can be used to build programs but
31. alues of 21 and ig they are all interpreted by v as the same map When there is only one such arrow e j E1 i1 E2 i2 it is sometimes denoted Le i1 gt 19 Ey i1 E5 i5 This notation refers to the property corresponding to the arrow e 4 i2 if an ingredient x of y of nature E4 satisfies i4 then the ingredient xo u e x1 of 1 of nature Ez satisfies 12 Example 1 The example of partial functions where partial means strictly partial i e not total without any constraint has been considered in guidel section 4 1 We have described the directed graph Fi ari and the homomorphism of projective sketches P part F port gt Ep where E par is the blow up Ep 70 part ANd Ppart is the fibration Epir Ais Let Func denote the category with the sets for points and the functions which may be either total or partial for arrows The 72 indexation hay of Func guidel section 4 1 determines a Ppart Stratification Func Harts part Where Te part Ds A libus and m 12 A ae E part MODEL n Tort M iaet image of Pt I all the sets image of Ar tot all the total fonctions image of Ar part all the partial functions STRATIFICATION Tart D art ari Hari Func 9 Ppart image of Pt I it is the identity image of Ar tot it is the inclusion of the set of total functions in the set of functions image of Ar part it is the inclusion of the set of partial functi
32. ay This may lead us to first classify the ingredients of S before amplifying each of them according to its class Such a classification could be done by an indexation as defined in guidel however this is not sufficient for most applications Here we define stratifications which generalize indexations and we use them for classifying the ingredients of S Hence a mosaic is made of a weft S called its apparent weft together with a stratification which classifies the ingredients of S and a counter model amp which gives the shape of the amplifications In this way a mosaic is able to specify implicit features while preserving their implicit nature The realizations of a mosaic take into account all its components They are quite different from the realizations of its apparent weft S However it is possible thanks to a ribbon product to build a weft S called the explicit weft of X with the same realizations as gt It means that it is possible to explicit a mosaic First in 4 1 we define the stratifications Then in 4 2 using the crown product and the stratifications we define the ribbon product and we state its fundamental property The mosaics and their realizations are defined in 4 3 and the fact that it is possible to explicit any mosaic is obtained as an immediate consequence of the fundamental property of the ribbon product These definitions and results will be illustrated in 5 4 1 Stratifications First we recall the not
33. be a set valued realization of k Ar then the map w k H1 w H2 propagates the error Now it is easy to get a contravariant functor k from E towards the category W k IdAr k ConsP MG ie CompP Ong zd ye jcompp k dom Je a ARE Ta me k Ar K comp Se NW pi K RankP amp Eq k jgq HOMOMORPHISM k dom k Pt k Ar lines amp Pt amp Pt i HOMOMORPHISM k codom k Pt gt K Ar lines amp Pt K Pt o A WEFT k IdAr extends K Pt identity arrows idp H gt H idge H H equation idg o h hf o id ye k IdAr HOMOMORPHISM k j1dar amp Ar gt amp IdAr lines k Pt 1 gt K Pt K Pt o gt k Pt arrows k gt idp k idge A WEFT k ConsP lines K Pt 1 k Pt 2 k Pt 3 arrows ki Hi gt Hi k Hi H ko H5 H k H H equations ki o h h o k k o h h o k k ConsP fh Pie Ho HET We Je B nn ef LE pe Vs H Hi H Hg lt gt Hg 1 HOMOMORPHISM k p1 k Ar k ConsP lines k Pt 1 gt K Pt 1 amp Pt o gt K Pt o arrows ki oki k m k 2 CROWN PRODUCT AN EXAMPLE HOMOMORPHISM k pa k Ar k ConsP lines k Pt 1 gt k Pt 2 k Pt 2 gt k Pt 3 arrows k e kh k k A WEFT k CompP extends k ConsP arrows ki Hi gt H3 k Hi gt H composition k k o k k k 0 k equation ki oh zh amp ok k CompP Pa k Ln rn Ho Hii ns I
34. bon product as defined in 4 In 5 we will see that this does indeed solve point B and that in addition it solves point C Finally let us see what happens when dealing with a binary product constraint 2 11 Product constraint Let us consider the cartesian product N N x N and the addition N N Since any attempt to compute the predecessor of 0 should return an error the addition should return an error as soon as one of its arguments is an error Going on with the analysis made in 2 1 this means that we need a new error element ey the set N N U fey2 and the map N2 N which extends the addition and propagates the error Let us replace the weft S by the following one since the constraints of S do not behave well we forget about them Ambi WEFT S4 2 CROWN PRODUCT AN EXAMPLE 17 extends S point N arrows m N gt N m N gt N a NN equations ao fact z o facty idy idy ao fact s 07 72 2 soa product NN DN The support of S4 is T1 NE n p s US aofact zofact y id y id y aofact somi 72 soa We consider a realization of S towards O o amp which interprets U N z s and pas U N 0 suce and pred respectively and we look at the way it interprets N m and 7 Let ex en eu N and let X be the complement of ex in N Then N X LI ex is a point of Ook since it is a set valued realization of Pt Both projections pi
35. cations more powerful than wefts l hese new specifications are called mosaics They generalize wefts in order to be able to deal with implicit features of computer languages In addition each mosaic can be explicited by building a weft with the same meaning This construction is called the ribbon product it is related to the family of tensor products 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 The only prerequisite to read this article is guidel Here as well as in guidel we focus on the interpretations of our specifications The point of view of programs and computation will be studied in guide3 1 INTRODUCTION 1 1 Introduction In guidel we define wefts and some tools for handling them Wefts have been intro duced by Lair in Lair 87 They come from Ehresmann s theory of sketches Ehresmann 66 Ehresmann 68 and they are related to patchworks Lair 93 They are also somewhat related to notions introduced by Freyd in Freyd 73 Freyd amp Scedrov 90 Here is a short survey of guidel e An A weft for any category A is made of a support which is a point of A and constraints A realization w of an A weft S towards a point A of A is specified by S w Real 1 S When A is the category Ambi of ambigraphs and A is the ambigraph Set of sets this notion of specification is very similar to the notion of algebraic
36. components of X are all mixed together in S and can no longer be torn apart These components split the information into three parts e on one hand the apparent weft focuses on the computations involving one variable x of natural number type without worrying about the state e on the other hand the properties describe how an operation can interfere with the state e and both are related by the indexation which says how each operation in the apparent weft does interfere with the state Modularity i e building large specifications from small ones is a fundamental process of any specification paradigm Most usual specification constructors like enrichments extensions quotients and pushouts Goguen et al 78 Wirsing 90 are special cases of the inductive limit or colimit constructor from category theory The theorem which describes the realizations often called models of the new specification is the following one the realizations of the inductive limit of a family of specifications are the projective limits of the realizations of the given specifications The ribbon product is a new tool for modularity since it builds a large weft Expl from small pieces organized into a mosaic The fundamental theorem describes the realizations of xpl 321 they can be identified with the realizations of the mosaic but not with the realizations of the apparent weft S Actually in order to build a ribbon product we use a crown produ
37. ct which is a special kind of inductive limit So the fundamental theorem on the ribbon product is a consequence of the general theorem stated above about the realizations of an inductive limit of specifications Other methods have been brought forward for dealing with implicit features in computer languages at least for dealing with the notion of state in an implicit way Among them are monads linear logic and various methods involving a notion of instant algebra We now give some hints about a comparison with our point of view 1 INTRODUCTION 5 The method using monads Moggi 91 Wadler 85 makes use of an algebraic specification for dealing with the functional features of the language and monads for dealing with its implicit features A generalization of this method can be found in Filliatre 99 Monads are related to a special kind of mosaic as we will see in an example in 2 The linear logic approach Lafont 88 Wadler 90 is able to deal with the notion of state in such a way that the state cannot be duplicated this problem has been mentioned above This can also be obtained with a mosaic thanks to a suitable definition of imperative programs guide3 The notion of instant algebra is crucial for the state as algebra approaches like dynamic systems Gaudel et al 99 Lellahi amp Zamulin 99 D oids Astesiano amp Zucca 95 dynamic ab stract data types Ehrig amp Orejas 94 Ehrig amp Orejas 98 and abstract state machin
38. de of an equation is an ok map then the interpre tation of its left hand side is also an ok map This will give an example of the way a distinguished projective cone in F can express a conjunction of properties The hypothesis e the interpretation of the right hand side of an equation is an ok map is a new property which corresponds to a new point of F A priori if the interpretation of an equation satisfies K Eq eq then the interpretation of its right hand side satisfies K Ar for which is weaker than K Ar ok So we have to express the conjunction of the properties K Eq eq for an equation and K Ar ok for its right hand side in a way compatible with K Ar for for its right hand side First of all we add to E this is a conservative extension e the identity arrow ide e the composed arrows in order to access directly to both members of a equation qi pi jeq Eq Ar Or Pr jeq Eq gt Ar e and the distinguished projective cone 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 50 Then in order to express the hypothesis we add to F e above Eq a point Eq eqq e above idgg an arrow idgg eqq eq Eq egg Eq eq e above qq an arrow qy eq4 ok Eq eq4 Ar ok e above the distinguished projective cone just added to E the distinguished projective cone idea eq eg Eq eq l Ar ok qa eq dar ok for Ar for Finally in order to express t
39. dler 85 indeed the ambigraph o is related to the Kleisli category of the monad M X 1 X Note that a map f Xi X5 which propagates the error is characterized by its restriction f x Xi gt XoU ex This means that the set valued realizations of k Ar can be identified to the set valued realizations of the following weft of ambigraphs he H H H H lt Hf a he H gt Hi Hy H5 H I To sum up this first way to deal with the example of natural numbers with predecessor is not entirely satisfactory A the support of S behaves fairly well we have formalized the fact that in each set there is an error element and that each map propagates the error B however even on the support of S we have not been able to say that the interpretations of z and s should not create an error while the interpretation of po z should always return an error C and what is not satisfactory at all is that our formalism is not able to deal properly with the constraints of S Our approach relies on the idea of giving additional information on the required interpre tation of each ingredient of S for instance each map should propagate the error Point B above will be solved in 5 by giving more accurate information each map should propagate the error and in addition some maps should not create an error whereas some others should always return an error For this purpose we will build a stratification and a rib
40. e or functional languages like Lisp or ML Unlike what happens with natural lan guages the implicit features of computer languages should be made explicit before the program is run If this is not done correctly it may lead to surprising results Specification by wefts of ambigraphs together with their set valued realizations is sufficient for dealing with purely functional programming This will be seen in guide3 and can be deduced from the important work done in and around the theory of algebraic specifications a fundamental paper is Goguen et al 78 whereas Astesiano et al 99 is a recent survey This works in the following way A functional program can be defined as a term p of a weft of ambigraphs S A term of S is composed of arrows from the support of S and arrows which arise from the constraints of S The meaning of such a program is given by the interpretation of the 1 INTRODUCTION 2 term p by a set valued realization w of S For instance let S be the weft of ambigraphs made of two points N and U two arrows z U N and s N N and the constraint U T Let w be the set valued realization of S which interprets N U z and s respectively as N a one element set U x the constant map 0 identified with the natural number 0 and the successor map succ nt n 1 Then the term p sosoz U N is a functional program and its interpretation by w is the constant map x gt 2 identified with the natural number 2
41. e for the properties of the interpretation of the product constraint has the following consequence Given two terms t S N and tz S N of ST for any point S of S the term t fact t4 t3 S N is defined only when t and t satisfy K Ar ok However usually the term t is meaningful as soon as 1 and ta satisfy K Ar for Indeed let Y Y U ey be a set with an error element and let fj Y 2 Nand f Y N be two maps which propagate the error and which may create an error We define the map f Y 5 N y by f ey ene and for all y Y e f y ew if f y en or ay en e f y x1 22 if y x1 EN and f2 y 2x9 EN Then if p N 2 N and ph N N denote the two projections the equalities p o f fi and p5 o f fj are partially satisfied on Y Precisely if def f denotes the set of elements y of Y such that f y is not an error we see that the map f is characterized by def f def Fi N def f2 and Vy def f pro f y fi y and ps o Py faly This means if f p o f and f f for i 1 and 2 that def fj N def fip def fi O def Fio and for all y in this set fiy 1 41 and Fialu fiy We will see that it is possible to extend p in order to express this property of the product The potential of the constraint of product is pe 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 47 and its body
42. ed o succ N N In order to solve this problem first we weaken our requirements and then we use a stratifi cation Our requirements are weakened in the following way for all arrow g of a directed graph G it can still be said that the interpretation of g should be a total function but it cannot be said that it should be a partial function It means that the arrows of G can be indexed by two symbols tot for an interpretation as a total function and func otherwise Whereas the properties total and partial corresponding to the indices tot and part in example 1 are not compatible the properties total and any corresponding here to the indices tot and func are compatible indeed each total function is a function This last point cannot be expressed by an indexation but we will see that it can be expressed by a stratification However as in example 1 let us first consider an ambigraph Zune the blow up E Ami M func and the fibration E ww ML sine The ambigraph Zfunc is the same apart from the name of the arrow func as the ambigraph Zpar in guidel section 4 1 AMBIGRAPH Zfunc 4 MOSAICS AND RIBBON PRODUCT 28 point I arrows func 1 I tot I I identity arrow tot id composed arrows tot o tot tot func o func func o tot tot o func func equations func z func tot tot T func totofunc f I SD toi idr funczfunc PROJECTIVE SKETCH E Ambi M func and HOMOM
43. ense in order to recover the meaning of the instruction J e and it is possible to build the weft with explicit state S from S using a general con struction called the ribbon product Moreover we claim that a similar approach is valid for various implicit features of computer languages The generalized interpretation of p mentioned above as well as the ribbon product con struction depends on the kind of implicit feature which is considered in this example it is an implicit notion of state The information on this implicit feature can be given in various ways for instance by syntactic conventions like the use of the assignment symbol or by informal comments which are added to the program let us speak about comments in any case In our example comments deal with the state They say that the interpretation of u may modify the current state while the interpretation of r depends on the current state but is not allowed to modify it and the interpretation of s should neither use nor modify it We say that s is a static operation r is an access operation and u is a modification operation In addition we choose a name for each property for instance here the names st acc and mod respectively In this way the information can be split between e the apparent weft S e the description of the properties e the names of the properties st acc and mod e the indexation of the arrows of S by the property names s gt st r
44. es or evolv ing algebras Gurevich 99 Gurevich 91 Let us use the terminology of Ehrig amp Orejas 94 There are four specification levels and the first three levels correspond to an increasingly large part of our apparent weft The first level specifies the values types and the corresponding part of our apparent weft contains all the arrows indexed by st The second level specifies the in stant structures and it corresponds to adding the arrows indexed by acc The third level with dynamic operations corresponds to the whole apparent weft by adding the arrows indexed by mod Other points of view such as those which rely upon automata theory Hopcroft amp Ullman 79 are designed for dealing with states but it is difficult for them to deal with complex data types With our point of view we may consider the usual graphic representations of automata as wefts so that we may conjecture that our approach encompasses part of automata theory along with algebraic specifications theory The crown product is introduced in 3 while the stratifications the mosaics and the ribbon product are studied in 4 Sections 2 and 5 are devoted to a detailed study of two versions of an example The aim of this example is to specify the natural numbers with a predecessor operation in such a way that any attempt to evaluate the predecessor of zero results in an error In both versions the apparent weft takes care of the natural numbers while the properties de
45. ew we can see why it is important for the stratification in to be a loose homomorphism see 4 1 Indeed since loose homomorphisms behave badly with respect to the realizations we may expect that some realizations of the mosaic will be relevant although all the realizations of its apparent weft S are irrelevant In contrast to 2 here we succeed in formalizing in a correct way the natural numbers with a predecessor operation 5 2 Comments As in 2 2 rather than the set valued realizations of S we look at interpretations of S which satisfy some comments In 2 2 our comments said that the interpretation of each point of S should be a set with an error element and that the interpretation of each arrow of S should propagate the error Here our comments are more accurate the interpretation of some arrows is not allowed to create an error while on the contrary the interpretation of other arrows should always return an error Given an arrow g G1 G in S if X X U fex denotes the interpretation of G4 and X5 XU ex the interpretation of G2 then three distinct comments may be used for g e K Ar for like K Ar in 2 the interpretation of g is a map f X X which propagates the error which means that f 1 amp 2 for for forward e K Ar ok the interpretation of g is a map f Xi X which does not create any error which means that f 1 6 amp 2 and f x X for all x X4 e K A
46. for for denoted eq T f gt err composition equation The definition of the identity of Err corresponds to the fact that the identity map of a set with an error element is an ok map The definition of the composition in Z corresponds to the properties of composed maps For instance the equality err o for err means that if fi f2 is a pair of consecutive maps such that fi propagates the error and f is an error map then fo fi is also an error map Since Z like any ambigraph can be identified with a set valued realization of the projective sketch EAmbi we can build the projective sketch blow up of E Ambi by Z and the corresponding fibration E Ambi NL Emil E pos The projective sketch E 4npi Z includes 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 38 e above the point Pt only the point Pt Err e above the point Ar three points Ar ok Ar for and Ar err e above the arrow dom three arrows dom i Ar i Pt Err for ok for err e above the arrow codom three arrows codon i Ar i Pt Err for ok for err e above the point IdAr the point IdAr ok e above the arrow jraar the arrow jraar ok IdAr ok Ar ok e and so on E Ami M IdAr ok lr dom ok Ar ok a a dom for Pt Err Ar for codom for dom err codom err Ar err E ynbi Z E Anti The blow up E mp Z deals with the fac
47. graphs S is essentially the same as in 2 1 it has the arrows z s p the identity arrow idw and the composed arrow po s We add the composed arrow po z only in order to be able to speak about the properties of the interpretation of p o z Ambi WEFT S points U N arrows z U gt N s N gt N p N gt N idv N bNN pos N 5 N poz UN equation pos idy terminal point U initiality constraint the interpretation of UN 5N is initial among the eos CES where Xo is terminal The analysis is the same as in 2 1 it proves that the set of set valued realizations of S Real 4nbi S Set is irrelevant Moreover in 2 we could not find any solution among the sets of realizations of S in another ambigraph Real 4mbi S Indeed the set Real S Real mp K Set which appeared as a fairly good candidate when we looked only at the support of S failed to deal in a correct way with the constraints as seen in 2 8 and 2 9 Here we first build a mosaic 3 with apparent weft S Then we proceed as in 2 with the mosaic X instead of the weft S We build two new sets of realizations corresponding exactly to our requirements 1 on one hand the set of set valued realizations of X Real 4nbi 2 Set 2 and on the other hand the set of set valued realizations of the explicit weft of X built thanks to a ribbon product Real mpi Expl Set 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 36 With the former point of vi
48. he constraints a weft T of models of F Moreover T is related to S o p by a family of homomorphisms of models of F the r s in the support and the constraints These homomorphisms define a loose homomorphism of Mod F wefts It follows that a weft of p stratifications can be identified to a triple S T R or just R where e S is a weft of models of E e T is a weft of models of F e and R T Sopis a loose homomorphism of Mod F wefts p x 1j S Set The special case of the stratifications associated with an indexation suggests a method for the description of all the stratifications using inverse images which will be used in the examples To begin with any homomorphism of projective sketches p F E can be described by inverse images For this purpose all the ingredients of the projective sketch E are first described Then e for all point E of E we describe all the points F of F above E i e such that their image by pis E they can be denoted E i where i is in some suitable set e for all arrow e of E we describe all the arrows f of F above e i e such that their image by p is e they can be denoted e j where j is in some suitable set e for all distinguished projective cone c of E we describe all the distinguished projective cones d of F above c i e such that their image by p is c they can be denoted c k where k is in some suitable set e and so on In this way the homomorphism p is kn
49. he deduction rule we add to F e above qg an arrow qy eqq ok Eq egg Ar ok Now let us add to the counter model xk A WEFT k Eq eq4 extends K Eq eq arrow ka H gt Ho equation kho hi h20 ka K Eq eq4 HOMOMORPHISM K idea eqq gt eq K Eq eq amp Eq egal it is the extension HOMOMORPHISM k ga eqq ok amp Ar ok amp Eq eq4 lines amp Pt Err gt k Pt Err 1 K Pt Err o gt k Pt Err 2 arrows ke ka k kh ke ke HOMOMORPHISM amp qg eqq ok amp Ar ok amp Eq egal lines amp Pt Err gt k Pt Err 1 K Pt Err o gt k Pt Err 2 arrows keskgq k ek k ke Actually for k qy eg ok to be really a homomorphism we slightly extend amp Eq eq4 More precisely we add the equation k oh ha o kg This extension is conservative because this equation can be deduced from k o hy h2 o ka and ki kh 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 51 In this way if we know that pos id y satisfies K Eq eq and that id y satisfies K Ar ok we may deduce that pos satisfies K Ar ok 6 CONCLUSION 52 6 Conclusion In this paper using the basic notions introduced in guidel we have defined mosaics and the ribbon product and studied one of their applications Whereas simple specifications have been defined in guidel section 2 5 as wefts more com pl
50. hilip Wadler Linear types can change the world In M Broy and C B Jones editors Programming Concepts and Methods North Holland 1990 Wirsing 90 Martin Wirsing Algebraic specifications In J van Leeuwen editor Handbook of Theoretical Computer Science chapter 13 pp 675 188 Elsevier 1990 CONTENTS Contents 1 Introduction 2 Crown product an example 2 L Analysis x 0 ia a a A sr tr E RS 2 2 A A O A gh O O 2 3 Projective sketch E ss 2 4 Model 2 Set re A A a 2 5 Contravariant functor O Wi Set 2 6 Counter model k E gt Wo 2 Crown product E NU ker co 8 ok nes a E xU Ne RUP gos uu arg 2 8 Terminal point constraint 2 0 Initiality constraint 4 4 2i 44 4 ya A Xo hog e XI ERR GR dod s 2 10 Conclusion xxr Bet aden qoa c RC m ESAE eX UE EN 211 Product constraint mire a eek eA Re ER Gu ee e a x Ru 3 Crown product Sol SUPPORT A det tied EO E Vae NA ee Mee te rea E 3127 CONSTTIDES r a usu aues uw dr EC rgo e CS eut dr etc REB ort c Ue ce 3 3 Wetts Or wefts deed de Ae n o Shot n estan x Ded Ae dud esas 4 Mlosaics and ribbon product AS StratiiiGationsS ice A Rub euros svn IH AN MUN 4 2 Ribbon products ere a qr bete ede E ATTE e oe e icit 42 3 MOSAICS rtu mach he iS ter och Moye mos AV T termes e EU ati la pe cb e LZ e el 5 Mosaics and ribbon product an example Dilo Analysis a eue enean Rr a AA PO Ne QE Xe cempore 5 2
51. icated specifications are defined in 4 3 as mosaics Their interest lies in their ability to deal with the implicit features of computer languages The ribbon product is a new constructor for specifications The fundamental result regarding it states that each mosaic can be made explicit thanks to a ribbon product This result justifies the use of mosaics and allows us to avoid making them explicit In this paper we focus on the realizations of a mosaic From this point of view the apparent weft of a mosaic is rather uninteresting its realizations are irrelevant and the apparent weft must be corrected thanks to a stratification before yielding something meaningful On the contrary in guide3 we will focus on the major role of the apparent weft in the design of programs Thanks to the ribbon product we have been able to prove that the so called explicit and implicit points of view about specifications in computer science far from being opposed are strongly related In guide3 this will enable us to build a common framework for dealing with functional and imperative programs which preserves the specificities of both programming modes REFERENCES 53 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
52. inductive limit cone of W to a projective limit cone of Set 2 6 Counter model k E 2 W From 2 2 the interpretation of each point of y should satisfy the comment K Pt and the interpretation of each arrow of u should satisfy the comment K Ar In both cases ie for E Pt as for E Ar the comment K E corresponds to a weft of ambigraphs amp E the interpretations which satisfy the comment K E can be identified to the set valued realizations of amp E A WEFT k Pt points H H H arrows h H H h He H terminal point H sum HE E He K Pt H y 2H H lt HT Let us check that the comment K Pt corresponds to the weft of ambigraphs k Pt let w be a set valued realization of amp Pt and let X w H X w H and x be the unique element of w h wm H We then get X X U fex In the description of amp Ar and everywhere below referring to our drawings the line K Pt stands for a copy of k Pt with the names of all its ingredients indexed by the symbol n This means that the line k Pt is the weft of ambigraphs with support H s gi He and constraints HE 1l and H H H A WEFT k Ar lines k Pt 1 K Pt o arrows k Hi gt H k Ht H equation k ohg 2 h ok y up alo opt Sp Tu Eg 1 4 5 pups cou S boh he Ho H H j 1 2 CROWN PRODUCT AN EXAMPLE 10 The comment K Ar corresponds to the weft of ambigraphs amp Ar indeed let w
53. ions of indexation fibration and blow up as defined in guidel Let E be a projective sketch Then each model of E determines a projective sketch E called the blow up and a homomorphism of projective sketches EN called the fibration EWV EV E The definition of the fibration in guidel section 4 2 is such that e for all point E of E the inverse image of E by EV is made of the points E i where i is in the set E e for all arrow e E E of E the inverse image of e by EN is made of the arrows Le 21 E1 i1 Ez i2 where 11 is in the set E1 and i e 41 E2 e and so on Each v indexation i e each h u v in Mod E determines by the fundamental theorem on the blow up see guidel section 4 2 a model Ah of EV Ah EN Set such that for all point E of E and all i E CANE x E A E x i ME 4 MOSAICS AND RIBBON PRODUCT 24 and for all arrow e E1 E of E and all i 4 CAD le d CADIE d gt ARE e 41 is the restriction of e u E1 gt u E2 Moreover the inclusions v h E i u E define a homomorphism AA LAR gt wo EN E ug Nh m Nh Set Z More generally see guidel section 4 3 each v inderation H S v of a Mod E weft S determines a Mod E v weft A H NH El Set and a loose homomorphism A H AH gt S o EN EN ay NH Set As noted in guidel sectio
54. l 32 k 9 R which has the same set valued realizations Real s Expl 22 Set S Real my 2 Set 5 10 Conclusion This example in contrast to the one in 2 is totally satisfactory thanks to a mosaic and a ribbon product it has been possible to meet our requirements Now let us see what happens when dealing with a binary product constraint in 5 11 and new deduction rules in 5 12 5 11 Product constraint Let us replace the weft of ambigraphs S by S4 as in 2 11 First we consider the constraint of product and we say that the interpretation of the arrows 7 and 7 should satisfy K Ar ok as well as each arrow in each ambigraph of the constraint Of course points should satisfy K Pt Err and equations K Eq eq Then it is easy to see that in each realization of S towards O o x the interpretation of N is N N U eye as required 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 46 Then it follows from the equations that the interpretation of a is the addition In this way the mosaic is extended into a mosaic X such that natural numbers with a predecessor operation correspond to 1 a set valued realization of 2 or equivalently a set valued realization of rpl 31 This is wholly satisfactory from the point of view of realizations however we will see that it does not behave very well from the point of view of programs the notion of program will be studied in guide3 Indeed our choic
55. lt will be given in our reference manual It makes use of the Yoneda lemma for projective sketches from guidel section 4 4 Here we only give an idea of the proof First let us consider the lefthand side O amp Og u Since amp Og y is the inductive limit of the points amp E x and since O is left exact O x Og u is the projective limit of the sets O amp E x an element y of O k Og 1 is a compatible family of elements of O K E 1 It means that Y YE x e 2 With each yg O K E 2 and for all e E E with x p e x the following compatibility condition holds O x e 2 Yin a gt YE Now let us consider the righthand side Hom moa r 1 O o x The model y of E can be seen as the inductive limit of all its ingredients arranged according to their nature this is the Yoneda lemma for projective sketches Then a homomorphism h of models of E with domain u can be described as the compatible family of images of all the ingredients of u Let VE h x for all point E of E and all x E then h is characterized by the family Y WEaj tE By definition of a homomorphism the following compatibility condition holds O e 2 UE x VIE 01 Finally we have given the same description for both hand sides the theorem follows When W Mod E which is a cocomplete category we may consider the Yoneda counter model see guidel section 4 4 Ve E 2 Mod E Given the definition of
56. n 4 3 whereas the homomorphisms of Mod E wefts behave well with respect to the realizations the loose homomorphisms do not behave well And actually this is the kind of property we are looking for see the example in 2 and the discussion in 5 1 It happens that the indexations are not general enough for most applications This will be illustrated by example 2 and by the problem of natural numbers with a predecessor operation in 5 This is why we now define the stratifications Let us consider a homomorphism of projective sketches p F gt E Definition 5 A stratification along p or p stratification is a triple u v r or just r where e is a model of E e v is a model of F e and r v po pis a homomorphism of models of F F E E M ee n Set A homomorphism of p stratifications from u1 v4 r1 towards u2 vo r2 is a pair h k where e h iij ua is a homomorphism of models of E e and k v4 n is a homomorphism of models of F such that rok hop onri 4 MOSAICS AND RIBBON PRODUCT 25 In this way we get the category of p stratifications It can be proven that this category is projectively sketchable by a lax colimit of p see the reference manual It is easy to see that a weft of p stratifications determines on one hand looking only at the A ps in the support and the constraints a weft S of models of E and on the other hand looking ga only at the v s in the support and t
57. n 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 Second Part Mosaics for Implicit Specification The aim of this paper is to introduce new specifi
58. ndamental property of the crown product For all Mod E weft S there is a canonical bijection Owen K Or S Real 4 E S Oo K K eo E Oe S Weft W oyw A e ee Dad Set About the proof The proof proceeds recursively according to the level and uses proposition 1 see the reference manual 0 3 3 Wefts of wefts Now let us focus on the special case where W itself is a category of wefts W Weft A for some cocomplete category A so that W is cocomplete and where O Real1 A for some point A of A this is the case in our example in 2 with A Ambi and A Set Then k D S is a weft of A wefts We will assign to it a A weft x Og S in such a way that theorem 1 implies a characterisation of the image of k Og S by the functor Real 4 A For all category we will build a functor Weft Weft A Weft A 3 CROWN PRODUCT 22 such that for all Weft A weft S S 8 nA and for all point A of A there is a canonical bijection Owept S Real4 S A weg Real4 S A This property states that the generalized realizations from S towards A can be identified to the realizations of S towards A Weft Weft A gt Weft A keal 4 B rs o Bp CH ee The functor Weft W Weft A may now be defined recursively according to the level of the Weft W weft S Definition 4 If S has level 0 then S is its support S If c S S has
59. ns of a weft as given in guide1 section 2 5 gives rise to an extension of the contravariant functor Homy M W Set to a contravariant functor Realw M Weft W Set This is generalized by the definition given below of the extension OWweft Weft W Set of the contravariant functor O Indeed whenever O Homyy M we will get Homy M we Realy M Definition 3 For all W weft T the set Owe T will be a subset of O T and for all ho momorphism c T T of W wefts the map Oyefe 0 Ow T gt Oper T will be the restriction of O a If T is a W weft of level 0 then Owep is O Now let n be an integer gt 0 Assume that O yyef is defined on the W wefts of level lt n 1 Let T be a W weft of level n and let T C EST CD 2 U be a constraint of T Then an element x of O T satisfies the constraint T if e the element zc O x x of O C is in Owen C 3 CROWN PRODUCT 21 e and for all element xp of Owgj D such that O y 2p xc there is a unique element ry of Ow U such that O 0 zu xp C C 1 D U T O C Owen ones cm D Siaz U eco O T Then Oy T is the set of the elements of O T which satisfy all the constraints of T The fundamental property of the crown product of k by a weft below states that there is a canonical bijection between the set Os K Or S and the set of realizations of S towards Ook Theorem 1 Fu
60. ons in the set of functions pp F part TE Ep art i es Set mA part In similar way the Tri indexation ja of G guidel section 4 1 determines a Ppart stratification 69 H9 o pr T9 p Where Hos ZI E and az Ems 4 MOSAICS AND RIBBON PRODUCT 27 Fpart MODEL His T art Ah p image of Pt I U N image of Ar tot z U N s N N image of Ar part p N N STRATIFICATION r9 T5 4 ANAL p Hop 09 Dpart image of Pt I U N U N image of Ar tot z s 52 s p image of Ar part Az Ss p Ppart F part 5 Ep 219 5 Set Gp The homomorphisms of Ppari stratifications from on towards Pon express the fact that the interpretations of the arrows z and s of Ur should be total while the interpretation of the arrow p should be partial Example 2 Example 1 shows that partial functions can be handled thanks to an indexation at least as long as we do not try to compose the functions In order to take care of the composition of functions we should extend V NE by adding to it all the composed arrows including the arrow part o tot When we compose a total function and a partial function we generally get a partial function Henceforth it is natural to define part o tot part However as has been noted in guidel section 4 1 this does not fit because it may happen that the composition of a total function and a partial function is a total function see pr
61. own indeed p E i 2 E p e j e etc Of course whenever p is not a fibration there is no simple relation between the set of the j sin the description of the arrows e j above an arrow e E E and the set of the 7 s in the description of the points E1 i1 above the point j Now a p stratification u v r v po p can also be described by inverse images First the model y of E is described which means that a set u E is given for all point E of E and a map e for all arrow e of E Then e for all point E of E and all point E i of F above E we describe the set v E il e for all arrow e of E and all arrow e j of F above e we describe the map v e j e and for all point E of E and all point E i of F above E we describe the map r E i V E i gt E 4 MOSAICS AND RIBBON PRODUCT 26 Quite often in practice the maps r E i are inclusions and each application v e j is the suitable restriction of e Then this description becomes much simpler since the maps v e j and r E i are known In this case it is sufficient to describe e for all point E of E and all point E i of F above E the subset v E i of u E Whenever an ingredient x of u of nature E is in v E i we say that i is an index for x or that x satisfies i Moreover under these assumptions if there are several arrows e jk E1 11 Ez i2 above the same arrow e Ej E and with the same v
62. p T 1 Let us consider the set O amp Ri of set valued realizations of x R1 It is easy to check that as above the interpretation of U by each of these realizations should be a two element set as we wish These two points of view are equivalent by corollary 2 e O I Real voa F T1 Oo K gt 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 45 or equivalently Real 4nbi amp p Ri Set Real moa r T1 Real 4mbi K Set In addition this gives exactly for this example what was required Let 34 denote the mosaic p Ri k Its set valued realizations have been defined as Real 4nbi 21 Set Real voa r T1 Real mpi amp Set Then k R1 is the explicit weft Expl 31 of Xy The equivalence of both points of view means that 34 and rpl 341 have the same set valued realizations Real s pl 241 Set Real asy 21 Set 5 9 Initiality constraint Now let us handle in the same two ways the initiality constraint of S Let us decide that the interpretation of each arrow in each ambigraph in the constraint should satisfy the comment K Ar ok In this way we extend S1 T1 R1 to a weft of p stratifications S T R It is easy to check that we get the following result the interpretation of N should be N NU ey and the interpretation of z and s should be the maps 0 and succ as required We have built from the mosaic X p R K the weft xp
63. po sy etc For all arrow e E gt E of E and all x E take a copy amp e z K E x k E 2 where x u e x u E of the homomorphism k e k E gt k E for example a copy k dom z k Pt U gt k Ar z of k dom etc Then the wefts amp E x are merged together according to the homomorphisms k e x for example the line amp Pt of the weft amp Ar z is merged with Pt U thanks to k dom z In this way we amplify each ingredient x of y of nature E into amp E and we merge them all together in the most natural way i e in the same way as the ingredients x of y are merged together for building y Such a construction is an inductive limit in the category of wefts of ambigraphs a short survey about projective and inductive limits can be found in the appendix of guidel Although we have not yet taken into account the constraints of S it should be noted that there are four constraints in amp Og Li arising from the constraints of the wefts K Hi Hy He H 1 HV Hy H HS 1 2 8 Terminal point constraint Let us now consider the constraint U I of S which means that the interpretation of U should be a terminal point Let Si DE gt Set be the weft of ambigraphs of support u and constraint L where I which is denoted Ir in guidel section 2 2 is the constraint over u of level 0 with potential EUR UD D Au D C C C and body x uc y such tha
64. proposition 1 that Proposition 2 For all p stratification y v r there is a canonical bijection O amp 0 7 Hom wa Vv O o amp 4 MOSAICS AND RIBBON PRODUCT 31 ER ee dup N NT ic e Definition 7 Let S T R T So p be a weft of p stratifications The ribbon product of k by R above p is the W weft Set kQy R k OPT It follows immediately from theorem 1 that Theorem 2 Fundamental property of the ribbon product For all weft of p stratifica tions S T R there is a canonical bijection Oweg amp 9 R gt Real yag T Oo K K bya F idis w MNT LATE SN ey Set When W Weft A for some category A It follows immediately from corollary 1 that Corollary 2 Assume that W Weft A for some cocomplete category A For all point A of A and all weft of p stratifications S T R there is a canonical bijection Real 8j R 4 Real va E Real a K 4 amp Bp R Weft A d Ti a SEL Real 1 E 4 3 Mosaics The wefts are not powerful enough to deal with the implicit features of computer languages The mosaics are much better suited as will appear in 5 Here we define the mosaics we prove that they generalize the wefts and we see how the ribbon product can be used in order to associate with each mosaic a weft with the same meaning In this section A is any category Let S be an A weft and A a point of A We have defined in guidel section 2 5 the
65. r err the interpretation of g is a map f X X which always returns the error which means that f 1 6 amp 2 and f x e2 for all x Xi These comments are related if the interpretation of g satisfies K Ar ok or K Ar err then it will also satisfy K Ar for A map which does not create any error will be called an ok map and a map which always returns the error will be called an error map This is similar to the notations in Goguen 78 and indeed as in Goguen 78 we believe that significant improvements in the art of programming can be achieved by treating errors in a more systematic manner However we do not completely agree with this paper when it advocates to include all exceptional state behavior especially error messages directly in the specifications From our point of view these exceptional behaviors are not included in the apparent weft but only in the explicit weft which is not meant to be built as explained in 4 2 In order to have homogenous notations the unique comment for the interpretation of a point G of S is denoted e K Pt Err as K Pt in 2 the interpretation of a point G satisfies K Pt Err if it is made of a set X X U ex The unique comment for the interpretation of an equation g gr of S is denoted e K Eq eq the interpretation of an equation g gr satisfies K Eq eq if it is made of two maps f and f with the same rank X1 X5 such that f f With these nota
66. r0 k r succ k 0 kh gt suce ky gt pred kz gt Eu gt EN ES gt id ey gt ky gt id fen r ko EN Eu EN poz Proposition 2 proves that there is a canonical bijection between the two sets 00 r Hom voa F VY Oo K gt which means that Real Amii 4 r Set Hom moa F V Real 4nbi K Set 5 8 Terminal point constraint Let us now consider the constraint U I of S which means that the interpretation of U should be a terminal point Let Si DE E Set be the weft of ambigraphs of support y and constraint I as in 2 8 Let us decide that the ingredients of ue yp and py should satisfy e the interpretation of the points C in uc pp and wy and D in wp and py should satisfy K Pt Err e the interpretation of the arrow u in pu should satisfy K Ar ok hence also K Ar for Then proceeding as in 5 4 to build the p stratification y v r we may build three more p stratifications uc vc rc up vp rp and uu vu ru Their most significant part is the following one e vc Pt Err C and vc E i 0 for the others E i e vp Pt Err C D and vp E i 20 for the others E i e vu Me Err C D vy Ar ok vy Ar for 2 u and vy E i 20 for the others 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 44 The homomorphisms x y and determine homomorphisms of p stratifications hence we get a constraint over the p st
67. ratification r and a weft S1 T1 R4 of p stratifications p i Set E The Mod F weft T has only one constraint denoted l 1 Its potential is made of the extensions Ve vp vy and its body ve v is defined by C U As above there are two points of view 1 The first point of view considers the realizations of T towards O o k i e the elements of the set Real moa r T1 Oo K They are the ambifunctors from v to O o k which satisfy the constraint T1 It means that the interpretation of U by such a realization denoted X X U ex satisfies the following property for all set Y 2Y U ey there is a unique map f Y gt X such that Fley ex and f Y X Equivalently the interpretation of U should be among the sets with an error terminal with respect to the ok maps It is easy to check that X should be a two element set x i e X should be a one element set x This is exactly what we wish for the interpretation of U 2 Similarly to amp amp r above we may build the three wefts of ambigraphs KB re KQprp and amp B ru with the extensions KG re Kk rp e gt and the body amp x Supp k Dore gt Supp amp O r defined by Ho SHL U HE e Hy HQ HE In this way we get the constraint x I 1 over the ambigraph support of k 9 r By defi nition the weft of ambigraphs amp 9 R1 is made of x 9 r and of the constraint am
68. rojective sketches states that for all point A of A the set RealA Yg A HomaA Yg A can be identified with A Let gt denote the mosaic made of ide ESE ids S S o idg Vp E Weft Mod E It follows from the Yoneda lemma that the set of realizations of 3 can be identified with the set of realizations of S From now on we assume that A is a cocomplete category so that the category Weft A is also cocomplete Definition 10 Let p R K be an A mosaic The explicit weft of X is the A weft xpl 3 Kk R Corollary 2 states that for all mosaic X the explicit weft Espl has the same realizations as X It can be reformulated as Corollary 3 Fundamental property of mosaics Let A be a cocomplete category and A a point of A Let Y be an A mosaic and rxpl 31 its explicit weft Then there is a canonical bijection Reala A Real 1 Ezxpl 2 4 MOSAICS AND RIBBON PRODUCT 33 So from the point of view of realizations something as elaborated as a mosaic can be replaced by a weft which may look much simpler However the direct definition of the realizations of a mosaic definition 9 is often much easier to use Indeed the explicit weft Expl is quite large hence difficult to handle Moreover it is a mixture of all the components of the mosaic which cannot be retrieved from rxpl 32 however interesting they are on their own Consequently on one hand it is important
69. rrow z s and p of u by a copy of k Ar and so on for all the ingredients of u In this way we get a weft of ambigraphs which is called the crown product of k by y above E and is denoted KOEL A WEFT amp Og H lines K Pt u K Pt w arrows k Hy gt Hy k Hi Hy ki Hy gt Hy k HR Hi Hy gt Hy kp Hy Hy equations k o hf hs o k M o hy hy o k k o ho he o k kpo k idp kpo k5 idus Op Hy Hi Hy He Hg 1 NN hE Hy 2H Hy He He 1 kl UNS Ki ke CAN ke equations From the previous study the natural numbers with the predecessor operation define a set valued realization of k Og p i e an element of the set O amp Ox u Precisely points Hy U Hr U Hf eu Hy ON Hy eN Ay en arrows k 0 k gt suce kj gt pred k gt eu gt EN k gt td fen kp gt id fen Both these points of view are equivalent indeed proposition 1 will prove that there is a canonical bijection O amp Oz u Homyta e 1 O 0 amp 2 CROWN PRODUCT AN EXAMPLE 14 which means that Real 4nbi amp OB sng bs Set Hom Anvi p Real amos amp Set The construction of amp Og u can be described as follows For all point E of E and all x u E take a copy k E x of the weft k E for example two copies k Pt U and k Pt N of k Pt five copies k Ar x of amp Ar for x fz s p idy
70. s possible to complete this description in order to get a counter model kK func from F func towards Weft Ambi In this way we get a mosaic 3 func Pfunc F func td Ejsunc gt Tsp Hsp ue Gsp O Dfunc func F func te Weft Ambi A The set valued realizations of Y fun are such that the interpretations of the arrows z and s of Gs p are total functions while the interpretation of the arrow p is any function The explicit weft Expl junc contains 4 MOSAICS AND RIBBON PRODUCT Ambi WEFT Expl S func points Hy Hy Hoi arrows k Hy Hy ks Hn gt An kp Hj gt HN hp H gt An e constraints hp is a monomorphism and so on Exrpl func partial description 34 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 35 5 Mosaics and ribbon product an example This example is based as in 2 on the problem of natural numbers with a predecessor op eration In 2 we used a weft and a crown product which was not subtle enough Here we use a mosaic and the corresponding ribbon product leading to a much better solution More precisely instead of the weft of ambigraphs S of 2 here we use an Ambi mosaic X such that S is the apparent weft of gt This section runs like section 2 the support of S is studied in 5 7 then its constraints in 5 8 and 5 9 The required interpretation of each ingredient of S is expressed more precisely here than in 2 this is done in 5 1 and 5 2 5 1 Analysis The weft of ambi
71. s ps nm By Hg Hio HOMOMORPHISM k jcompp K ConsP k CompP this is the extension HOMOMORPHISM k comp k Ar k CompP lines k Pt 1 gt K Pt 1 amp Pt o gt k Pt 3 arrows k k k m k A WEFT k RankP lines K Pt i k Pt a arrows ky Hi gt Ha ki Hi HS ky Hi Ho kg Hi H3 equations k o h h o k kgo h h o kg e h e k RankP H Hf Hf 1 ul IE dl E h5 Hy 2H Ho Hg Hg 1 HOMOMORPHISM k pg amp Ar k RankP lines K Pt gt K Pt 1 amp Pt o gt K Pt o arrows k e kk ok HOMOMORPHISM kK pq k Ar k RankP lines k Pt 1 gt K Pt 1 amp Pt o gt K Pt o arrows k k ko k A WEFT K Eq 11 2 CROWN PRODUCT AN EXAMPLE 12 extends k RankP equations ky kg kg k he H H HS HOMOMORPHISM k jzq k RankP k Eg this is the extension In this way we get a contravariant functor E gt W Moreover this functor maps each of the five distinguished projective cones of E to an inductive limit cone so that it is a counter model k E W 2 7 Crown product s Og We have just said that the interpretations of the points U and N of u should be set valued realizations of amp Pt i e elements of the set Real 1 x Pt Set Similarly the interpretations of the arrows z s p of u should be set valued realizations of k Ar i e elements of the set Real 1 x Ar
72. t that distinct arrows of S may have interpretations which satisfy distinct comments But it does not deal with the fact that these comments are related The relations between the comments state that each ok map resp each error map does propagate the error In order to deal with these relations we extend E Amb Z and E Ambi M We also extend E Ambi though in an innocuous way without modifying its realizations such an extension is called conservative It can be helpful to use the point of view of logic already used in 4 1 for which each point of a projective sketch is a property name and each arrow is a deduction rule Then the composition of arrows corresponds to reasoning by deduction and each distinguished projective cone corresponds to a conjonction of properties For example in the projective sketch E 4 5 M the point Ar ok corresponds to the property e a map is an ok map and the arrow comp ok ok CompP ok ok Ar ok corresponds to the deduction rule e if both maps in a composable pair are ok maps then the composed map is also an ok map 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 39 Let us translate the deduction rule e if the interpretation of an arrow is an ok map resp an error map then it propagates the error For this purpose let E denote the projective sketch obtained by adding to E445 an identity arrow dar Ar Ar clearly this is a conservative extension Then in order to translate
73. t y C U Both points of view used in 2 7 for the support can be extended to the constraint 1 The first point of view considers the realizations of S towards O ok i e the elements of the set Real 4 e S1 Oo K They are the ambifunctors from y to O o k which satisfy the constraint This means that the interpretation of U by such a realization denoted X X U ex satisfies the following property for all set Y Y U ey there is a unique map f Y X such that f ey x Equivalently the interpretation of U is among the sets with an error terminal with respect to the maps which propagate the error It is easy to check that X is a one element set i e that X is empty But this does not meet our requirement according to 2 1 the interpretation of U should be the two element set U ey 2 CROWN PRODUCT AN EXAMPLE 15 2 Similarly to the construction of k Og y in 2 7 we may build the three wefts of ambigraphs K Ox pc RO pop and amp Og Ly with the extension homomorphisms k Or y and amp Og Denoting for Og and representing each line k Pt as the potential we get is the following KO nuc KO up e O y Let us denote amp Og x this notation will become clear in 3 2 the ambifunctor from Supp amp Og uc towards Supp amp Og u defined by he ht Ho SHES rey qu pP EHE In this way we get a constraint amp OgD over the ambigraph support of amp
74. the deduction rule let us extend E 445 NZ and E wnpi Z by adding e above idar two arrows id ar ok for Ar ok Ar for and idar err for Ar err Ar for Note that these arrows are not identities and that this extension of EA V T is not conservative In this way we get a projective sketch F and a homomorphism p F E which extends the fibration E 445 MZ E Amai Z E 4mbi F IdAr ok Ds T Ar ok T Pa idar ok for dom for Pt Err Ar for codom for oi er id ar err for codom err Ar err du In 5 12 we will deal with other deduction rules 5 4 Stratification y v r Let us build a p stratification i e a set valued realization y of E a set valued realization v of F and a homomorphism r v po p of set valued realizations of F As in 2 4 let p S E gt Set Then for all point E i of F let us define the set v E i as the following subset of u E v E i the set of the x u E such that x satisfies the comment K E i We get 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 40 points v Pt Err U N arrows v Ar for z s p idv pos poz equation v Eq eg poss idy etc For all arrow e j E1 i1 Ez i2 of F let us define the map v e j as the restriction of u e v e D 2 ne a for all z v Ex is It is easy to check that this is a map from v E1 41 towards v E i2
75. the same domain Now we introduce a new comment e K PEq ceq consider a pair of equations with the same domain s11 512 1 52 Let fj denote the interpretation of s and f the interpretation of sp for i 1 and 2 The interpretation of s11 81 2 51 572 satisfies the comment K PEq ceq if def fi def fr def fr N def 7 2 and for all y in this set fa zi and Laly fro 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 48 Then the equations s 52 and 8 1 5 2 generally do not satisfy the comment K Eq eq Clearly the property of the product can now be stated as follows the interpretation of the pair of equations of uj with the same domain ci ou d4 c9 o u d2 should satisfy the comment K PEq ceq This is why we extend F in a non conservative way and p by adding e above PEq a point PEq ceq e above pc for i 1 and 2 an arrow pc ceq PEq ceg RankP for for Finally in order to formalize the comment K PEq ceq we add to amp A WEFT K PEq ceq lines amp Pt Err o k Pt Err 1 k Pt Err 2 point H arrows koa Ho gt Hi koi Hg AY kyo Ho H5 kgo H As kar Ho gt Hi kgs Hg gt Hi kao Ho H5 kj Hi gt H3 hoo Hj hi Hi hga H gt H3 hao H Ho ha H gt Hy haa H gt H equations k 91 9 hj hio kg1 kg 29 hj h30kj2 ke 0 h M ok Ry OMG ho kia kj 9 ho oigo ha o hga ky 0 ho hy o
76. tions e the interpretation of the points U and N should satisfy K Pt Err e the interpretation of the arrows z and s should satisfy K Ar ok 5 MOSAICS AND RIBBON PRODUCT AN EXAMPLE 37 e the interpretation of the arrow p should satisfy K Ar for e the interpretation of the arrow p o z should satisfy K Ar err e the interpretation of the equation p o s id y should satisfy K Eq eq From which it follows immediately that e the interpretation of the arrow idy should satisfy K Ar ok e the interpretation of all the arrows should satisfy K Ar for Hence the interpretation of a unique arrow of S may satisfy several comments in a compatible way For instance the fact that z satisfies K Ar ok and K Ar for does not mean that the interpretation of z includes two maps one ok map and another map which propagates the error It means that the interpretation of z includes a unique map which is an ok map and which consequently propagates the error 5 3 Homomorphism p F E The name of the properties used in the comments i e Err for ok err and eq can be seen as the point the arrows and the equation of an ambigraph T AMBIGRAPH TZ point Err arrows for ok err Err Err identity arrow id prr ok Err Err composable pairs i1 i2 for all and 2 in ok for err composed arrows ok oi io ok 1 for all since ok idg err o i ioerr err for alli for o for for equation
77. to know how to build the explicit weft of a mosaic since this yields a consistent framework for dealing simultaneously with the functional point of view and the implicit features in the computer languages On the other hand in practice it is generally unwise to build the explicit weft it is much more advisable to deal directly with the mosaic Example 3 In example 1 we defined a homomorphism Pfunc Func Efunc of projective sketches and a homomorphism fs p Hsp Gsp Pfunc Of models of F func which is of course a loose homomorphism of Mod F func wefts without constraints We now describe some Ambi wefts and some homomorphisms between them A WEFT k Pt I point H amp IPt 11 a A WEFT k Ar tot points H Ho arrow k H Ho K Ar tot Hi Vk H A WEFT k Ar part points H H2 Hi arrows k Hi gt H h Hi Hi k Ar part Hi gt Hi constraint h is a monomorphism Ha HOMOMORPHISM k dom tot k Pt 1 k Ar tot points HH HOMOMORPHISM k dom part k Pt 1 k Ar part points HH HOMOMORPHISM amp codon tot k Pt I k Ar tot points H gt Ho HOMOMORPHISM amp codon part k Pt 1 k Ar part points Ht Ho The set valued realizations of k Pt 1 are the sets and the set valued realizations of k Ar tot resp of k Ar part are the total functions resp all the functions It i
78. which contains an error element denoted x Let X denote the complement of ex in X so that X X u ex The interpretation of each arrow of S should satisfy the comment e K Ar the interpretation of an arrow g G4 Ga satisfies K Ar knowing that the interpretation of the points G1 and G2 satisfies K Pt if it is made of a map f Xi gt X3 which propagates the error which means that f 1 amp 2 It can happen for these comments themselves to be expressed by means of wefts This will be seen in 2 6 but let us first introduce some notations 2 3 Projective sketch E Let B E ui denote the projective sketch of ambigraphs as in guidel section 3 4 with support E IdAr ConsP lt CompP aS mores p IdAr pA a zc Pr PI RankP lt Eq JEq composition 2 4 Model u E Set First let us look at the support of S Its constraints will be studied in 2 8 and in 2 9 respectively Let p S E gt Set This is an ambigraph identified with a model of the projective sketch E idn 2 5 J 8D Ad Z 8 p idy po s s p Ed Us Pp ip s idn 2 CROWN PRODUCT AN EXAMPLE 9 2 5 Contravariant functor O W Set Let W denote the category of wefts of ambigraphs guidel sections 2 1and 2 4 W Weft A where A Ambi and let O denote the contravariant functor O Real 1 Set W Set It is left exact which means that it maps each

SKETCHES AND SPECIFICATIONS USER'S GUIDE Second part

Contents

Download Pdf Manuals

Related Search

Related Contents