Compositionality of Update Propagation: Laxed PutPut Zinovy Diskin McMaster University, Hamilton, Canada diskinz@mcmaster.ca Abstract Compatibility of update propagation with update composition (the in- famous Putput law) is fundamental for the mathematical modelling of bx, but is not easy to ensure in practical scenarios. This severely restricts practical applicability of elegant algebraic models based on Putput, while leaving practical bx without solid algebraic support is also unsatisfactory. The paper aims to mitigate these problems, and presents the following findings. It is known that PutPut trivially holds for the sequential composition of two inserts or two deletes (what John- son and Rosebrugh called the monotonic Putput); it also holds for the relational (pullback based) composition of a delete followed by an insert (the mixed Putput). In the present paper, we will see that relational Putput can fail for the relational composition of an insert followed by a delete, which represents a wide class of practically interesting exam- ples. We will also analyze different ways of update composition, and discuss their interaction with update propagation. We will see that update propagation and Putput need a 2-categorical setting, formulate a notion of lax Putput, and show that it is much wider applicable to practical situations than the ordinary strict Putput. 1 Introduction Compatibility of update propagation with update composition (the infamous Putput) is fundamental for the mathematical modeling of bx, but is not easy to ensure in practical scenarios if we treat compatibility in a straightforward way. This severely restricts practical applicability of elegant algebraic models based on Putput, while leaving practical bx without solid algebraic support is also unsatisfactory (for, at least, some members of the bx community). Putput needs a careful analysis and investigation, but seems to be not a very popular research subject in bx. Problems with Putput were noticed since the very early work on lenses [9], and continued to be remarked later in, e.g., [8, 15], but the first (and seemingly the only so far) careful and mathematically solid analysis of Putput basics was undertaken by Johnson and Rosebrugh in [12]. They distinguished “easy” monotonic Putput, when two consecutive inserts or two consecutive deletes are to be propagated, from more problematic mixed Putput, when operation put must propagate an interleaving sequence of inserts and deletes. For the later case, they found an equivalent but more elementary and easier to verify condition for the mixed Putput to hold. The present paper continues Putput analysis and presents the following findings. We will first consider different ways of update composition, and see that in whatever way an algebraic operation of delta composition is defined, the real composition appearing in practice could be different, and, in general, a user input is required to correct an automatically produced delta. Thus, we have a 2-delta between the Copyright c by the paper’s authors. Copying permitted for private and academic purposes. In: R. Eramo, M. Johnson (eds.): Proceedings of the Sixth International Workshop on Bidirectional Transformations (Bx 2017), Uppsala, Sweden, April 29, 2017, published at http://ceur-ws.org automatically produced and the real delta. However, the former always subsets the latter, if deltas are composed as binary (multi)relations. This subsetting is in a sense preserved, when deltas are propagated backward to the source side, and gives rise to a lax compositionality of update propagation. Then we will consider a simple example of relational composition, in which an insert is followed by a delete, and see that Putput fails, but, again, some lax version of Putput still holds; we will also argue that this example is a representative of a sufficiently large class of practically interesting and important cases of update propagation. Thus, different deltas, their compositions and relationships between them form the very core of update propa- gation and Putput. This observation makes categorical models of bx essentially 2-categorical: deltas are 1-arrows, and relationships between them are 2-arrows. The 2-categorical setting allows us to distinguish the strict Putput, which requires equality of the two deltas (and hence their target models), from the lax Putput, in which the two deltas and their target models are not equal nor isomorphic, but comparable via a uniquely defined mediating 2-construct. We will see that in many interesting cases, including the insert-delete example mentioned above, while the strict Putput fails, the lax Putput holds. In a sense, problems of Putput mentioned in the literature can be seen as the problems of forcing an essentially 2-categorical lax phenomenon into a 1-categorical strict framework. Our plan for the paper is as follows. We will begin in Section 2 with a very simple Example 1 to fix the terminology, basic concepts, and issues to be discussed. Specifically, we consider relational, match-based and mixed update compositions (in this paper, updates are spans a.k.a structural deltas between models), and discuss how they coexist with Putput; the last subsection 2.3 builds a more abstract and general framework and presents our first schema/pattern of the lax Putput. In Section 3, we consider Example 2, in which relational Putput fails, discuss how general such type of examples could be, and build our second schema of the lax Putput; the last subsection 3.3 integrates the two schemas into a general lax Putput pattern. Section 4 outlines a formalization in terms of lax delta lenses. Remarks on related work and some historical sentiments can be found in Section 5, which also concludes the paper. 2 Putput and Update Composition (relational, match-based, and mixed) We will begin with a very simple example explaining the main notions and notations of the delta framework. Then we introduce three types of update composition: relational, match-based, and mixed, and consider how backward update propagation interacts with them. 2.1 Example 1: Basics of update propagation Models, metamodels, and views Metamodels are class diagrams with constraints. For example, suppose a metamodel M consisting of the only class Person with two attributes, name1 and name2, both of type String. A view of this metamodel is another metamodel N together with a mapping w: M ← N called the view definition. Suppose, for example, that N consists of a class Person with the only attribute name of type String, and the view definition maps Person in N to Person in M , and name in N to name1 in M . It means that in the w-view of M -models, attribute name2 is ignored while values of attribute name1 are called names. Thus, any model instantiating M is mapped to a model instantiating N , and we have a view execution function between the respective model spaces getw : M → N (note the reversal of the direction), whose name get abbreviates the command “get the view” (more interesting examples of view definitions via mappings can be found in, e.g., [10, 2]). In the lens framework for bx, the view mapping generating getw is forgotten, and the index w is omitted. A simple model A instantiating metamodel M is shown in Fig. 1 (at the left top corner of the grey-border rectangle labelled as Example 1a). It has two objects p1, p2 with attribute values as shown. As models are stored in computers, p1, p2 should be understood as object identifiers (OIDs), and name1, name2 as attribute slots that hold values, e.g., John and Henry. Function get applied to this model results in model B shown in the figure. Although B has semantically the same objects as A, their OIDs are different — think, for example, about model B stored in another computer. Moreover, mapping get is typically a non-deterministic function as the view execution engine may not control OIDs in the view model stored in a different computer, and thus OIDs may be different when the same get is applied to the same A at different time moments. If we do not want to consider a family of gets indexed by time moments, it makes sense to consider models up to their isomorphisms caused by isomorphic OID replacement; the more so that OIDs are invisible to the user, who sees isomorphic models as equal. Thus, pi, qi should be seen as representatives of the respective equivalence classes, which makes get a well-defined single-valued function (we say “get is defined up to isomorphism”), and we can write :get Example 1a Model A p1: Person Corr RAB Model B name1=John p1 ← q1 q1: Person name2=Henry name1← name name=John p2 ← q2 q2: Person p2: Person name1← name name1=Mary name=Mary name2=Ann <> AA 1:put ⋈ AA AA’ ⋈ A’A” BB’<> B’B” BB’ ⋈ B’B” q1 → q1” q2 → q2” p2 → p1→p1” Model A’ Model B’ 𝜹 q2 → q1→q1” → p2” p1': Person q1': Person [ ⊆] → q2” name1=John name=John name2=Henry 2:put 4:put <> Model A ⋈ <> p1 : Person <> Model A” = A name1=John Delta 𝒄 p1": Person 3:put Model B” <> name2=Henry p1 ← p1” name1=John q1": Person <> <> p2 : Person p2 ← p2” name=John name2=Henry name1=Mary p2’’: Person q2": Person name2=Ann name1 = Mary name=Mary 4:put name2 = ? Figure 1: Two examples of backward update propagation: 1a (framed) and 1b (the entire figure) B = get(A) or sometime A.get = B when this notation makes reading formulas easier. In this paper, we will not make “up-to-iso” considerations formally accurate (which is a rather laborious endeavour) and will work with a semi-formal understanding of equality of two models in the hope (supported by the previous experience of managing similar issues) that with a suitable formal definitions everything would work smoothly. In the figure, the grey arrow labeled :get denotes an application of function get to model A: its bulleted tail is attached to the argument/input object, and the arrow head points to the result – model B. The second arrow head (note the dashed-dotted branch) points to the second object produced by the view execution – a traceability/correspondence mapping RAB that maps elements of B to their origin in A. This mapping is essential for update propagation, but as it can be computed from A (for a given view definition), in the asymmetric lens framework, the correspondence is implicit and officially does not occur into the output of get– hence our dash- dotted notation for it. Deltas Consider the following scenario further referred to as Example 1a. In the first step, model B is updated to model B 0 . Imagine a user manually editing the model with a computer, who deletes object q2, and does nothing with object q1. Such an update can be specified by a delta ∆BB 0 (note the respective block-arrow in the figure), which consists of a single link (q1, q10 ) (in fact, an ordered pair) showing that the object q1 is preserved in B 0 . Placing into the delta a targetless arrow from q2 is just a syntactic sugar to show that set of links ∆BB 0 does not contain any link from q2, which means that object q2 is deleted in B 0 . Thus, formally, ∆BB 0 is a singleton {(q1, q10 )}. Of course, in the case of a user manually editing model B with a computer, OIDs q1 and q10 would be identical (which is not excluded by our notation). However, if model B 0 is copied to another computer, having a different OID would be a useful option for our update modelling (with all reservations about OIDs and up-to-iso applicable again). We assume that our view metamodel says that the multiplicity of attribute name is exactly 1, i.e., any Person object has one and only one name slot. Hence, if two objects are the same, their name slots are also the same, and we may safely omit links between such slots. However, for attributes with multiplicity more than one (e.g., think of an attribute phone of multiplicity 0..3), data about which phone-slot in model B corresponds to which phone-slot in model B 0 is to be included into the delta. Linking slots in B and B 0 declares them to be the same slot, but it does not prohibit changing the value held in the slot. E.g., despite that q1 and q10 are linked, which implies their name-slots are linked, the values held in these slots would be different if Person q1 changed his name from John in B to, say, Jo in B 0 . In this paper we do not consider attribute modifications, but some details can be found in [2, Section 3]. Importantly, for the same two models, there can generally be multiple deltas between them. E.g., for models B and B 0 , besides the delta shown in the figure, there is an empty delta that specifies object q10 as a new object different from q1, which just happens to have the same name. In this sense, the notation ∆BB 0 could be misleading as pairs of models do not actually index deltas, but within our fixed scenario, this notation is convenient. Update propagation As updates are specified by deltas, update propagation amounts to delta propagation. In general, there are many source models A0 and deltas ∆AA0 , whose get-views are equal to B 0 and ∆BB 0 , hence we need some update policy to ensure uniqueness. A reasonable update policy should propagate updates along the correspondence RAB , i.e., in our case, delete object p2 corresponding to q2, and keep object p1 untouched—the result is the model A0 and delta ∆AA0 as shown in the figure. Note that these computed model and delta are blank (and blue with a colour display) to distinguish them from given (specified by the user rather than computed) models and deltas, which are shaded (and black. The blue colour aims to refer to mechanical computation.) The propagation procedure is modelled as an application of operation put to model A and delta ∆BB 0 (note the group of arrows 1:put). The correspondence RAB is essentially employed in the propagation, but as it can be computed for a given model A, in the asymmetric lens framework the explicit input for put is a pair (A, ∆BB 0 ) rather than (RAB , ∆BB 0 ) (note the dashed input arrow from RAB to 1:put illustrating the trick). Now we are ready to approach the main issue of our analysis. 2.2 Example 1 continued: Update composition and Putput Suppose that after update ∆BB 0 was propagated, model B 0 is again updated by adding a new object q200 , which is specified by delta ∆B 0 B 00 (note the arrow without source). Applying put to this delta results in a model A00 with a new object p200 corresponding to q2”, and the respective delta ∆A0 A00 . Note that model A0 is uncertain, as the name2 value for the newly inserted object is not known, and the attribute slot contains a null value ?. Our main question is what happens if we compose updates ∆BB 0 and ∆B 0 B 00 into a “jump” update ∆BB 00 = ∆B,B 0 ; ∆B 0 ,B 00 (where ; denotes the operation of update composition), and propagate the result to the source ; ; side into delta ∆AA ; ; from model A to some model A : whether A ; = A00 and ∆AA ; = ∆AA0 ; ∆A0 A00 , or not? Two main actors determine the answer: (a) How operation put restores missing information on the source side; (b) How much of the information about the component updates is forgotten in the composed (jump) update. We will call this information mediating. In our simple example, restoration (a) is very simple – if a Person in the view is newly inserted, his/her name2 is set to a null. But update composition is non-trivial even in this simple example, and it is the subjects of our analysis below. We will consider two somewhat opposite ways of composing updates. One is relational composition, which strives to respect the mediating information; we will also say that relational composition is history respecting. The other is match-based composition, which entirely ignores the mediating information, and thus is history ignoring. Relational composition and Putput As deltas consist of links, it’s natural to compose deltas by composing links. Consider again deltas ∆BB 0 and `0 `00 ∆B 0 B 00 in Fig. 1. The first delta has a link q1 - q10 targeted at q10 , and the second one has a link q10 - q100 0 00 ` ./ ` started from q10 ; we will call such links joinable. By composing these links, we obtain a link q1 - q100 from 0 00 the source of ` to the target of ` (symbol ./ means to remind about the composition mechanism based on composing joinable links). If the component deltas would have more links, we repeat the procedure and create a jump link for each pair of joinable links. In this way, we obtain a delta ∆BB 0 ./ ∆B 0 B 00 : B → B 00 from the source of the first delta to the target of the second. Such composition is basically the well-known binary relation composition generalized for multirelations. (And indeed, symbol ./ is often used in the database literature to denote the operation of relational join.) We will call this way of composing deltas relational. Note that if even the component deltas are ordinary (not multi) relations (i.e., every possible pair of elements either occurs into the delta or not), their composition described above can result in a multirelation. Indeed, if we `01 `00 `02 `00 have two pairs of joinable links between the same source and target, say, q - q10 - 1 q 00 and q - q20 -2 q 00 , 0 00 0 00 ` ./ `1 ` ./ `2 the composed delta ∆BB 0 ./ ∆B 0 B 00 would have two different links, q 1 - q 00 and q 2 - q 00 between the same pair of OIDs; we will call such links parallel. Thus, relational composition treats mediating information rather accurately except the case when an object is inserted in model B 0 , and then deleted in model B 00 . We will consider such a case later in Sect. 3, but in our Example 1a, relational composition is accurate, restoration of the source information is not problematic, and hence it is not surprising that Putput holds: it is easy to verify that in Fig. 1, put(A, ∆BB 0 ) ./ put(A0 , ∆B 0 B 00 ) = put(A, ∆BB 0 ./ ∆B 0 B 00 ). (1) We will phrase this pleasant result by saying that relational Putput holds for Example 1a. Match-based composition and Putput Consider the case, when deltas between models are computed by matching based on a key attribute rather than independently set by the user as in the scenario above. Suppose that attribute name on the view side is a key to class (table) Person, i.e., for any two objects p1, p2 instantiating the class, equality p1.name = p2.name implies p1 = p2. For example, deltas ∆BB 0 and ∆B 0 B 00 can exactly be computed by matching objects by their name attributes. In this view of deltas and updating, the composition of two deltas would be the delta determined by matching the end models, B and B 00 , while the mediating model B 0 is entirely ignored. In a sense, this way of def composition is opposite to relational, and we denote it by an “opposite” symbol <>: ∆BB 0 <>∆B 0 B 00 = ∆<> BB 00 , <> where ∆BB 00 denotes the delta produced by matching. 00 Thus, while in the relationally composed delta ∆./ BB 00 = ∆BB 0 ./ ∆B 0 B 00 , object q2 is a newly inserted Mary, the match-based delta ∆BB 00 has an additional link (q2, q2 ) that makes object q200 the same Mary earlier <> 00 existing in model B, and models B and B 00 are thus equal (up to iso). Hence, delta ∆<> BB 00 is propagated to the isomorphism/identity delta ∆AA<> as shown in Fig. 1 by dashed elements outside the frame (green with a colour display), and Putput fails. However, despite Putput stating equality (we say strict Putput) fails, we can still find some discipline in the propagation results. To wit: note the horizontal green delta c<> from A00 to A<> , which simply completes model A00 by replacing the null for “new” Mary’s name2 by its value Ann for the previously existing Mary. This delta is uniquely determined by our update composition and propagation procedures. Moreover, the discipline also includes relationships between deltas discussed below. Mixed composition and Putput: 2-deltas We have considered two possibilities of update composition: ∆./ BB 00 = ∆BB 0 ./ ∆B 0 B 00 for relational composition (r-composition), and ∆<> BB 00 = ∆ BB 0 <>∆B 0 B 00 for match-based m-composition. However, which of these two variants is right, i.e., correctly models the reality? We instantly find than neither one does. It may happen that the “new Mary” is indeed a new person that just happens to have the same name as Mary from model B, and then delta ∆<> BB 00 is wrong. (That is, while attribute name is a good key for a given state of the model, it does not work across the states, i.e., states at different time moments. We will phrase this by saying that name is a valid static key, but invalid dynamic key.) Or it may happen that new Mary is the same Mary from model B, which left the domain at the moment specified by model B 0 but came back at the moment of model B 00 .1 Then delta ∆./ BB 00 is wrong. Moreover, for models containing multiple classes, there are many formal ways of composing deltas, which differ by for which classes composition is relational, and for which is match-based. For example, suppose that our models contain two classes, Person and Car, and for objects of class Person we use r-composition, while for Car, m-composition is used. Then, we would have four ways of computing composed deltas: entirely relational, 1 Think, for example, about class Person as a class of employees of some company, and of Mary as an employee who quit the company at the time of model B 0 and was hired again at the time of B 00 . Or, even simpler, the user who was editing model B, deleted Mary and saved the result as B 0 , but later recognized that it was an error, and so in model B 00 the same object Mary is to be restored with all its attributes. entirely match-based, and two mixed ways depending on which of the classes is managed relationally and which is match-based. Thus, there is a whole variety of formal automatic compositions, but often neither of them can always be semantically correct as we have just discussed. That is, for a particular pair of deltas ∆BB 0 , ∆B 0 B 00 , we can find a formal composition ∆# BB 00 (# ∈ {./ , <>, ./ <>, ...}) equal to the correct delta ∆BB 00 , but chances that it works for all pairs are not significant. For instance, in Example 1, we can have ∆BB 00 = ∆<> BB 00 , but ∆B 0 B 000 = ∆B 0 B 00 ./ ∆B 00 B 000 for a consecutive series of updates from B 0 to B 00 to B 000 . We need to find a way of managing this diversity. As we have different types of deltas between models, we need a way to compare them. The simplest one is to compare deltas as sets of links, which works well under condition that the source and the target models of deltas to be compared are the same (i.e., deltas are parallel). For such deltas, their sets of links can coincide, be disjoint, intersected, or one be included into the other. In the latter case, we call the inclusion mapping a 2-delta and denote it by a double arrow, or sometimes by the set-inclusion symbol ⊆. (Then deltas between models can be called 1-deltas.) For instance, in Fig. 1 we have two 2-delta declarations labelled by δ on the right, and ε on the left. The content of these declarations is specified in the equations below: δ: ∆BB 0 ./ ∆B 0 B 00 ⊆ ∆BB 0 <>∆B 0 B 00 (2) <> ε: (∆AA0 ./ ∆A0 A00 ) ./ c ⊆ ∆AA<> (3) Note that mapping c<> , which fixes the gap between models A00 and A<> , is a necessary ingredient in (3) as 2-delta subsetting can only be declared for parallel 1-deltas. Now we can summarize our analysis of Example 1 in the following way. If the real composed delta coincides with the relationally composed, ∆BB 00 = ∆./ BB 00 , then strict Putput stating the equality of two deltas holds — see eq. (1). If the real composed delta is match-based, ∆BB 00 = ∆<> BB 00 , and hence 2-delta δ gives us a comparison between the real and the relationally composed 1-deltas, then eq. (3) gives us the following lax form of Putput: put(A, ∆BB 0 ) ./ put(A0 , ∆B 0 B 00 ) ./ put2 (A, δ) ⊆ put(A, ∆BB 00 ) (4) where delta c<> from (3) is considered as the result of the 2-activity of operation put, or 2-projection of put, and is denoted by put2 (A, δ) (we have also used associativity of ./ ). Our next goal is to see how much the content of the story described above for Example 1 can be extended for more general cases of update propagation. 2.3 Generalizing Example 1 Relational vs. match-based composition First, we need to make the notion of (structural) delta more accurate via the notion of span. That is, an update udel uins u of model X to model Y is modelled by a diagram X  Hu - Y , in which Hu is the model consisiting of all sameness links declared in u, which is called the head of the span, and udel , uins are injective mappings that specify, resp., deletions and insertions caused by u. To wit: X’s elements beyond the range of udel are deleted, and Y ’s elements beyond the range of uins are inserted. For example, the head of span ∆BB 0 in Fig. 1 is a model consisting of one object q1q10 , whose attribute name has value John by default. If this update along with deletion of q2 would change the name of q1, say, to Jo, then the name-slot of q1q10 would hold a null, and mapping udel would map this null to John, while uins would map it to Jo (details and formalization can be found in [2, Sect.3]) Clearly, update u is a pure deletion iff uins is the identity of Y (up to iso), and u is a pure insertion iff udel is the identity of X (up-to-iso). Spans will be denoted by stroked arrows u : X 9 Y in text, or bulleted u arrows X •- Y in diagrams. Now suppose we have two consecutive updates on the view side: v 0 : B 9 B 0 , v 00 : B 0 9 B 00 , and let v ./ : B 9 B 00 and v <> : B 9 B 00 denote their r- and m-compositions resp. The r-composition is given by the 0 00 pullback (PB) of mappings vins and vdel as shown in the diagram Fig. 2 (note the label [pb1 ]), which precisely def def ./ describes the operation of joinable link composition that we considered above. Thus, Hv./ = H1 , vdel = p01 ; vdel 0 , def ./ and vins = p001 ; vins 00 . The m-composition is specified by another PB: a key set of attributes is modeled by a set of functions from the object set of a model to some domain of values (note arrows key and key00 , which actually are def tuples of functions), to which we apply PB (note the label [pb2 ]) and obtain span (H2 , p2 , p002 ). Now Hv<> = H2 , def def <> vdel ./ = p2 , and vins = p002 . If the diamond H1 BValB 00 is commuttaive (we will discuss it B - - shortly), i.e., p01 ; vdel 0 ; key = p001 ; vins 00 ; key00 (5) v0 l de key p2 H 0 then by the universality of [pb2 ], we have a uniquely defined map- v - v in 0 s- ping ! as shown in the diagram. Note that although both spans, (p01 , p001 ) and (p2 , p002 ), are jointly monic (as produced by PB), span - p0 1 ! H = (p01 ; vdel 0 , p001 ; vins 00 ) is not necessarily monic, and hence mapping ! H2  H1 [pb1 ] B 0 [pb2 ] Val v 00 - - is not necessary injective (and indeed, matching does not care about p1 00 by how many ways an object in B can be linked to its match in B 00 l de - via a mediating object in B”). But if span H is jointly monic, which key 00 is quite normal (e.g., in our Example 1), then mapping ! is injective, p200 Hv00 v in 00 s - and becomes a set inclusion when we consider heads of spans up to - iso – this is the inclusion δ in Fig. 1. Commutativity (5) is essential for the existence of mapping !. This B 00 condition requires that an object does not change its key attribute values. For instance, in the example in Fig. 1, if object q1 changes Figure 2: Relational vs. match-based its name to, say, Jo in B 0 and will keep it in B 00 , then semantically composition true link q1q100 ∈ Hv./ will be lost in Hv<> . On the other hand, if there was some Jo in model B, who is deleted from B 0 and B 00 , matching B and B 00 would mistakenly link two different objects (named Jo and John in B) as the same. Note that in both these cases of erroneous match, attribute name remains a valid static key, i.e., no two different objects at a model state have the same name. Thus, the match-based composition is semantically flawed and can do both: create invalid links and miss valid links. Relational composition behaves much better: although it can miss valid links (and treat returned Mary from model B as a new Mary), it cannot create an invalid link. It allows us to postulate a semantically valid inclusion δ : v ./ ,→ v for any consecutive pair of updates v 0 : B 9 B 0 , v 00 : B 0 9 B 00 and their r-composition v ./ = v 0 ./ v 00 as shown in the right part of diagram in Fig. 3 (note the label [=] declaring commutativity of the triangle). This observation is formalized in Sect. 4.1 via the notion of a model as a lax functor. Laxity is also fundamental for Putput as discussed next. :get A - B .. .. .. u0 .. .. v 0 .. .. • . .1:put .. .. • .. .. .. ) .. .. • tA (v .. - .. ..  .. δ •.. u./ A0 - B0 [=] v ./ •.. ⇒• v pu [=] .. .. u= .. .. .. .. .. • .. --εδ .. .. • 00 . .2:put v 00 .. . .. ..? u - ....? ?  δ c  :get Av  A = A00 ./ - B 00 Figure 3: Towards general Putput, I: Backward propagation of 2-deltas Lax Putput Consider the diagram in Fig. 3, in which all vertical and inclined arrows are spans (note bulleted bodies of those arrows) denoting deltas. Deltas on the view side are denoted by v with superscripts, their backward propagations on the source side are denoted by u with the respectrive superscripts, e.g., u0 = putA v 0 and u00 = putA0 v 00 , where we use a bit more compact notation, in which delta put(A, v) is denoted by putA v. We assume that Putput holds def for r-composition, and thus u./ = putA (v ./ ) equals to u0 ./ u00 (note the left label [=]). As discussed above, 2-arrow δ says that delta v contains additional sameness links, and thus there are objects in B 00 , which are new according to delta v ./ but came from B according to v. As backward propagation of newly created objects leads to source models with nulls, in general, model A./ has nulls where model Av has certain values. Thus, models Av and A./ are different, and deltas u = putA v and u./ are also different and even non-parallel. However, as model A./ has nulls where model Av has certain values, there is a uniquely defined (partial) completion delta cδ as shown in the diagram.2 Finally, it’s reasonable to assume that update propagation is monotonic wrt. inclusion of sets of links, and if delta v ./ has less links than v, then delta u./ ; cδ has less links than u, which is shown by 2-delta εδ . The schema looks plausible, but it assumes that relational Putput holds strictly. In the next section we consider a simple example showing that this assumption can fail if update v 0 is insertion, while v 00 is the respective deletion. 3 Problems of Relational Putput Model A Model B c1,c2:PhDC :get A - B f1 :PDF g1 :PDF .. w1 :WS .. .. v0 .. u 0 .. . .1:put ) • • • A (v ./ .. ..  .. - .. Model A0 Model B 0 ut •.. u000 [=] A0 - B0 [=] • v ./ =p ... :PhDC .. u ./ .. f1,f2:PDF g1,g2:PDF -ε./ .... - . .2:put u 00• • 00 .. w1,w2:WS v .. - .?   ./ ? m :get A./  A00 - B 00 Model A./ Model A00 Model B 00 c1,c2: PhDC c1",c2":PhDC f1 : PDF f1 :PDF g1 :PDF w1 : WS w1,w2 :WS Figure 4: Towards general Putput, II: Lax relational Putput 3.1 Example 2: Relational Putput can fail We consider yet another synchronization scenario. Suppose that the source models specify states of some research project consisting of two tasks. Each of them is to be performed by either a post-doctoral fellow (PDF), or by two PhD candidates (PhDC), but due to budgetary constraints, only one of these options is allowed. In addition, a PDF is to be provided with one work station (WS). For example, model A in the top right part of Fig. 4 shows some state of the project, in which the workforce consists of two PhDC and one PDF with his workstation. On the view side, only PDFs involved in the project are shown. This gives us the view B shown in the figure. Now suppose that an updated view B 0 shows a new PDF g2 added to PDF g1. Hence, due to budgetary constraints, two PhDC should be assigned to another project—see model A0 , whose dashed frame (blue with a color display) shows that this model is computed. In the next step of the scenario, the recent PDF g2 quits, and so two PhDC should be hired on the source side to ensure performance, while g2’s workstation may be kept to minimize the amount of changes — these changes result in model A00 . Whether PhDC c100 , c200 are fresh for the project, or the previous PhDCs got involved again, this information cannot be specified with delta v 00 : A0 9 A00 and is lost for update v 00 . On the other hand, relational composition v ./ = v 0 ./ v 00 is identity, which is propagated to identity on the source side. Thus, the state A./ is the same as A (up to iso), and delta u./ is identity. Note the essential difference between updates u000 = u0 ./ u00 and u./ : not only model A00 has an extra WS in comparison with A./ , but according to update u000 , model A00 has two newly hired PhDC, while two PhDC in model A./ are the same as in state A according to update u./ . Thus, relational Putput fails. However, the good news is that some lax discipline of update propagation still holds. Indeed, there is a uniquely defined mediating delta m./ : A./ 8 A00 (consisting of a set of horizontal links in Fig. 4), which map 2 A rather complicated theory of uncertain models and completions can be found in [5], but it is much more general than our needs in the present paper. (a) newly created objects in A00 to their counterparts in A./ , (b) objects in A00 that were preserved from A (via composition u000 ) to their counterparts in A./ ∼ = A, and, finally, (c) deletes extra objects in A00 . Of course, there are two bijections of set {c100 , c200 } to set {c1,c2}, but if roles of the two PhDCs are indistinguishable, then our up-to-iso approach to models equalizes these two bijections, while if the two PhDCs play different roles specified in the metamodel, then there is only one role-preserving bijection: we map c100 to that ci, which plays the same role. Now composing u000 with m./ results in a delta parallel to u./ , which does not have any extra links due to (c), but misses some of u./ ’s links due to broken links in B 0 . For instance, in Fig. 4, there are links c1 → c1 and c2 → c2 in u./ , but there are no links c1 → c100 , c2 → c200 in u000 . This explains the 2-delta ε./ : u000 ./ m./ ⇒ u./ . Despite the simplicity of the example, it illustrates a sufficiently general mechanism of violating strict Putput, but keeping a lax Putput—we discuss this in the next section. 3.2 Generalizing Example 2 In simple cases, a view definition mapping w: M ← N is just a projection that cuts out a piece of M (e.g., in our Examples 1 and 2). In complex cases, we first augment M with derived elements defined by queries (in fact, such elements are query definitions), and then cut out a required part in the augmented M , i.e., a view definition is a Kleisli mapping w: Q(M M ) ← N wrt. the monad specifying the query language. Then computing the w-view of model A ∈ M , getw (A), amounts to, first, executing the queries in the image of w, which results in an augmented model Q(A), then cutting out the respective piece in Q(A), and finally retyping the result to metamodel N . Details of how this works can be found in [7]. Now suppose that model B = getw (A) is updated by inserting a piece Y , which we informally encode by writing B 0 = B + Y . To restore consistency, a respective piece X should be added to Q(A), Q(A0 ) = Q(A) + X, and if the queries used in the view definition are monotonic (which is anyway a basic assumption underlying functoriality of get), then some piece Z should be added to A so that A0 = A + Z and Q(A0 ) = Q(A) + Q(Z). However, normally models are bound by constraints, and compliance with some constraints, say, R, may force to complement the addition of Z to A by adding to A another related piece, say, ZR (e.g., workstations for PDFs in our example). Moreover, other constraints (like budgetary requirements in our example), say Σ, may force to complement the addition of Z by deleting from A some piece ZΣ (removal of PhDC in our example). We encode this complex interplay of different constraints by writing A0 = A + Z + ZR − ZΣ = (A − ZΣ ) + Z + ZR (6) The next step of our scenario is deletion of Y so that B 00 = B + Y − Y = B. Consistency restoration leads to deleting X from Q(A0 ), which for many update policies would cause deleting Z from A0 . However, deletion of Z does not necessarily imply deletion of ZR like in our example with workstations, i.e., constraints R may work in only one direction. Also, the metamodel may have constraints Π dual to Σ in the sense that deletion of Z from A0 causes addition to A” of some piece ZΠ (performance requirements in our example forcing to have either two PhDC or one PDF for the task). Encoding this interplay in our “algebra” gives us equation A00 = (A − ZΣ ) + ZR + ZΠ (7) Importantly, if even “fighting” constraints Σ and Π are of equal power (like budgetary and performance require- ments in our example), and pieces ZΣ and ZΠ are isomorphic (like in our example, where the deleted piece ZΣ amounts to two PhDCs, and the added piece ZΠ amounts to two PhDC again), the total of (A − ZΣ ) + ZΠ is not A (i.e., update u000 is not an identity) as relational composition does not create links between the newly added piece ZΠ and its counterpart ZΣ (exactly like in our example, when two PhDCs are fired and then hired again). Now we notice that model A00 can be updated to model A./ ∼ = A in the following canonic way m./ : the piece (A − ZΣ ) is identically mapped to itself in A, the new piece ZΠ (two new PhDCs) is mapped to its counterpart ZΣ (two previous PhDCs), and finally the piece ZR (workstation w2) generated by “unidirectional” contraints R is deleted. Composing just specified delta with vertical composed delta from A to A00 via A0 (i.e., u000 ) still lacks links from ZΣ to ZΠ , which gives us 2-delta ε./ as shown in the diagram Fig. 4. The considerations above although quite informal still demonstrate the generality of the mechanism under- lying the example. A mandatory relationship R regulating additions of new source elements, and mutually opposite constraints Σ and Π (resources vs. performance) seem to be quite general notions appearing in many view definition cases, and their interaction between themselves and update propagation were specified in rather general terms. Obviously, if relational Putput fails in a simple example, it will fail in many other more or less similar and practically interesting cases. What is less clear is how stable the idea of having a lax discipline for relational Putput, i.e., having a unique 1-delta m./ and a unique 2-delta ε./ medaiting the two results of update propagation. Here an accurate formalization of the generalization above would be very helpful, and it hopefully could be done if we enrich the model spaces with some additive structure suggested by equations (6,7). 3.3 Lax Putput Diagram in Fig. 3 specifies a lax Putput schema in the assumption that relational Putput holds strictly. As we have just seen, relational Putput is also lax, and thus the schema should be modified as shown by diagram in Fig. 5. This diagram integrates the two previous diagrams, and we again slightly simplify notation to make the meaning of the diagram more transparent. The right-most triangle commutativity means that v ./ = v 0 ./ v 00 . The real update delta v supersets v ./ which is shown by a 2-arrow δ. :get A - B .. .. u0 .. 0 v .. • . .1:put .. • ) • tA (v ./ .. (v ) .. .. tA .. - pu :get -  δ •.. u000 A0 B0 [=] v ./ •⇒• v pu v = • [=] u .. = .. .. u ./ .. • -εδ - -ε./ - .. .. • 00 . .2:put v 00 .. u ..? - ? ?   cδ m./  :get Av  A./  A00 - B 00 Figure 5: Towards general Putput, III: diagrams in Fig. 3 and Fig. 4 are integrated Deltas v 0 and v 00 are propagated to u0 and u00 resp, and u000 = u0 ./ u00 (note the second commutativity declaration). However, the backward propagation of v ./ , putA v ./ , is not equal to u000 as relational Putput can fail if v 0 is an insertion and v 00 is a deletion. Thus, putA v ./ is a different delta u./ , and mediating delta m./ together with 2-delta ε./ provide a comparison between the two. In this way, the laxity of relational Putput is provided by the triangle around ε./ . Similarly, the leftmost triangle around εδ provides the mediating constructs for propagating back 2-delta δ. An important difference between these two triangles is that cδ is a partial completion mapping that does nothing besides filling some null slots with values (recall our Example 1). In contrast, while delta m./ also includes a significant completion part, it also can delete objects (recall our Example 2). However, neither cδ nor m./ insert objects in our examples. Now by standard arguments of 2-category theory, we conclude that tiling the two comparison triangles results in a comparison triangle with base m./ ./ cδ and comparison 2-arrow (ε./ ; cδ ); εδ , where ; denotes composition of a 2-arrow with 1-arrow (actually with the respective 2-identity) in the standard 2-categorical way. 4 Towards Formalization: Lax Lenses We will outline a formal framework, in which our preceding discussion can be specified. This work is in progress, some constructs behave well and settled, but there are also several ad hoc definitions, whose clean categorical elaboration is still to be found. 4.1 Models as (lax) trajectories As discussed in [6], model synchronization is a dynamic rather than static notion: what is to be synchronized is trajectories of models in their model spaces rather than discrete model states. For the asymmetric case, we may assume the same tree I of version numbers for both the source and the view models, which are interpreted as mappings A: I → M and B: I → N considered consistent if Ai .get = Bi for all i∈I (we write Ai , Bi for A(i), B(i) respectively). In the delta setting, we have a richer picture in which tree I is considered a graph, model spaces are also graphs, and A, B are graph morphisms considered consistent if uij .get = vij for all pairs i ≤ j in I with i being the parent of j if i < j, and uij = A(ij), vij = B(ij) being the respective updates (deltas). If the source update uij is the result of backward propagation of the view update vij , then the equality above is the PutGet law for delta lenses. As update composition is a key part of the picture, we consider model spaces as categories, and any tree I can be seen as a poset and hence a category as well. To fully employ the categorical machinery, we would like to make mappings A, B functors, i.e., graph morphisms preserving composition. However, as our discussion in Section 2 shows, it would exclude many practically important cases. Fortunately, relational composition always subsets semantically valid composition, and then declaring mappings A, B to be lax functors into respective model spaces considered as 2-categories, would not be practically restrictive. Thus, for any pair of composable arrows in I, i.e., for any triple i ≤ j ≤ k, we require existence of mediating 2-arrows: εijk : uij ./ ujk ⇒ uik for A and δijk : vij ./ vjk ⇒ vik for B 3 , which make A, B lax functors. Hence, the slogan: models are lax trajectories. Lax delta lenses are intended to be a gadget that synchronizes such lax trajectories by propagating updates back and forth. 4.2 Lax lenses The forward propagation half of the lens structure is easy. Model spaces are categories with a posetal 2-structure (i.e., categories enriched over posets), and get: M → N is a strict 2-functor. It is easy to see that 2-functoriality is just an extension of get’s monotonicity for 2-arrows. Two models (as trajectories) A: I → M , B: I → N are called consistent if A; get = B as 2-functors. This equality implies (o) state-based consistency Ai .get = Bi for any version number i∈I, (i) delta-based consistency uij .get = vij for any pair i ≤ j in I, and (ii) 2-delta consistency εijk .get = δijk for any triple i ≤ j ≤ k in I. The second half of the lens structure—backward propagation with operation put—is much more complicated because we need to describe two lax phenomena: (a) put’s action on 2-deltas, and (b) lax Putput as such. We will consider the former in Sect. 4.2.2 and the latter in Sect. 4.2.3, but first we need some preliminaries. 4.2.1 Preliminaries Triangle functors Let C be a small 2-category. We will write C i , i = 0, 1, 2 for, resp., its set of objects (0-cells), arrows (1-cells) and 2-arrows (2-cells). If u is an arrow A (1- or 2-cell), then • u denotes its source cell, and u• its target cell. For 1-arrows this notation is especially suggestive as bulleted symbols denote objects, and we will mainly use this notation for 1-arrows. u1 u ; u ⇒ δ u2 1 Let A ∈ C 0 be an object. The set of all 1-arrows from A is denoted by C 1 (A, ∗), and can be converted into a category T A in the following way.  u ?? A1 - A2 Objects of T A are 1-arrows from A, i.e., Obj T A = C 1 (A, ∗). A T A-arrow from 1-arrow u1: A → A1 to 1-arrow u2: A → A2 is a pair 4 = (u, δ) as shown in the inset figure with 1-arrow u: A1 → A2 called the base of 4 , and 2-arrow δ : u1; u ⇒ u2 called the delta of 4 . We will often write 4u,δ : u1 ⇒ u2. We define composition of triangles by their tiling: given 4 = (u, δ) : u1 ⇒ u2 and 4 0 = (u0 , δ 0 ) : u2 ⇒ u3 , composition 4; 4 0 is the pair (u; u0 , δ; u0 ; δ 0 ). It is easy to check that such composition is associative, and pair (idA2 , idu2 ) is the identity of u2 wrt. this composition. Thus, T A is a category. There are two special subcategories in T A, which have all objects that T A has, but fewer arrows. The first one, T ⇒A, has arrows with the base being identity. Then triangles degenerates into 2-arrows between 1-arrows from A, and non-parallel 1-arrows in T ⇒A are not connected. The second special category has arrows with the delta being 2-identity. It is easy to see that its triangle-arrows are nothing but commutative triangles with vertex A and we denote this category by T =A (that is, T =A is nothing but the slice category C \A). Any arrow f : A ← A0 gives rise to a reindexing functor f ∗ : T A → T A0 in an obvious way by precomposition. def u,δ In more detail, an arrow u1 : A → ∗ is mapped to f ∗ (u1 ) = f ; u1 : A0 → ∗, and triangle u1 - u2 is mapped u,f ;δ to triangle (f ; u1 ) - (f ; u2 ) with the same base u but a different (composed) delta. Thus, any category C is equipped with a triangle functor T : C → Catop . We will write T C when we need to make the carrier category 3 in more detail, we have mappings between the heads of the spans, which commutes with their legs explicit. It is easy to see that reindexing preserves the two special types of arrows so that we also have functors T ⇒: C → Catop and T =: C → Catop . Finally, suppose F : C → D is a 2-functor (and hence a 1-functor as well). As any 1-functor preserves 1- arrow parallelism and composition, a 2-functor F gives rise to a family of functors between triangle categories FA : T C A → T D B with B = F (A) indexed by objects A∈C C 0 . Below we will omit subindex A in FA . Lax lenses – a brief sketch Now we can describe a view mechanism as a 2-functor get: M → N from a 2-category (model space) M to a 2-category N . This functor gives rise to a family of functors getA : T MA ⇒ T NB with B = get(A) indexed by objects A ∈ C 0 . Backward propagation is modelled by two families of mappings inverse to get, both indexed ⇒ by models A from M . The first family, put⇐ A : T M A ← T N B, manages backward propagation of 2-deltas. The 4 = second, putA : T M A ← T N B, provides lax Putput. However, Putput laxity is special: the comparison is provided by a pair consisting of a 1-arrow and a 2-arrow, while an ordinary laxity only involves 2-arrows. (Actually we will see that the target categories of mappings put4A are pyramids — constructs slightly more general than triangles.) Below we describe these two families in detail. 4.2.2 Backward propagation of 2-deltas: Put and the 2-structure Suppose for a view B = get(A), we have two parallel updates from B, v1 , v2 : B → B 0 , one subsetting the other via δ : v1 ⇒ v2 (see Fig. 6). It means that v1 creates more new objects in B 0 (more accurately, more objects in B 0 are considered new according to delta v1 ). Hence, the backward propagation of v1 , update u1 : A → A01 , creates more new objects on the source side than u2 : A → A02 . Hence, in general, model A01 will contain more nulls (be less certain) than model A02 (see Fig. 1 for a simple example). Hence, there should be a uniquely defined partial completion update cδ : A01 → A02 and uniquely defined 2-arrow εδ : u1 ; cδ ⇒ u2 . In its current state, the theory of partial completions [3] is complex and under construction, and in the present paper we will work in a more abstract setting and consider cδ to be just an update. Arity of ⇐-propagation Given a 2-functor get: M → N called a view, we define an operation of backward ⇐-propagation put⇐ as the following three family of operations/mappings. a) A family of mappings put⇐ A : M 1 (A, ∗) ← N 1 (B, ∗) 0 indexed by M -objects ( as before, B = get(A)). 4 b) A family of mappings put⇐ A , which assign to each 2-delta δ : v1 ⇒ v2 between parallel view updates v1 : B → 1 0 0 B , v2 : B → B , a mediating update cδ = put⇐ 0 A (δ): A2 ← A1 1 0 as shown in Fig. 6, where ui = put⇐ A vi , i = 1, 2, 12. 0 c) A family of mappings put⇐ A 2 , which assign to each 2-delta δ as above, a mediating 2-delta εδ = put⇐ δ A (δ) : u2 ⇐ (u1 ; c ) 2 δ δ (c ,ε ) – see Fig. 6 again. Thus, the result of backward propagation is a triangle u1 - u2 , and it is easy to see ⇐ ⇐ that the three mappings above define a correct graph morphism putA : T A ← T B. In fact, we can specify the construction above by saying that we have a family of graph morphisms. Definition 1 (well-behaved put⇐ ). Given a 2-functor get: M → N (a view), a backward ⇐-propagation ⇒ operation is a family of graph moprhisms put⇐ A : T M A ← T N (A.get) indexed by models A from M . Below we write B for A.get. This family is called well-behaved (wb), if it satisfies the following PutGet law for any model A ∈ M and any 2-delta δ : v1 ⇒ v2 considered as a triangle in T N⇒ B: (PutGet)⇐ A (put⇐ A δ).get = δ. 4 Index 0 means to recall that the operands of the operation are objects/0-cells in the respective triangle categories (although 1-cells in the model space N ) :get A - B u3 u2 δ δ δ0 • δ 0 • -ε • u1 v1 •⇒•⇒• v3 -ε - - ? ? ? ? :get - A03   0 A2 0   A01 B0 cδ cδ Figure 6: Put and the 2-structure In detail, the equality above means (PutGet)⇐ A 0 (put⇐ A v).get = v for any v ∈ N 1 (B, ∗); 0 (PutGet)⇐ A 1 (put⇐1 0 • • A δ).get = idB 0 (where B = v1 = v2 ); (PutGet)⇐ A 2 (put⇐ A δ).get = δ. 2 Functoriality of put⇐ A Our examples show that in practice put⇐A has nice functorial properties shown in Fig. 6 (this is, in fact, transitivity of subsetting). Hence, we can require put⇐ A to be a functor without being too restrictive for practical applications. Moreover, this functor is normally compatible with reindexing. Definition 2. Operation put⇐ is called very well-behaved (vwb), if it satisfies the following Stability (identity preservation) and PutPut (2-composition preservation) laws specified below. For any model A and update v: B → ∗, we require (Id)⇐ A 1 put⇐ ⇐0 • A (idv ) = idu• , where u = putA v and u is its target model. 1 (Id)⇐ A 2 put⇐ ⇐0 A (idv ) = idu , where u = putA v. 2 Below we will encode these two equations as the Stability law for put⇐ : for all A∈M M 0, ⇐0 (Id)⇐ A put⇐ A (idv ) = idu , where u = putA v. We also require, for any model A ∈ M and two consecutive 2-deltas δ : v1 ⇒ v2 , δ 0 : v2 ⇒ v3 in T N⇒ B as shown in Fig. 6, the following two equations (PutPut)⇐ A 1 put⇐ 1 0 ⇐1 ⇐1 0 A (δ; δ ) = putA δ ; putA δ (PutPut)⇐ A 2 put⇐ 2 0 ⇐2 ⇐1 0 ⇐2 0 A (δ; δ ) = (putA δ ; putA δ ) ; putA δ Below we will encode these two equations as the PutPut law for put⇐ : for all A∈M M 0, (PutPut)⇐ A put⇐ 0 ⇐ ⇐ 0 A (δ; δ ) = putA δ ; putA δ v Finally, for any A and update B - B 0 , we require the following diagram to commute: put⇐ TA  A T ⇒B 6 6 u∗ v∗ (8) put⇐ A0 T A0  T ⇒B 0 The data above can be compactly specified as follows. Lemma 1. Given a view 2-functor get: M → N , a very well-behaved backward ⇐-propagation is a (strict) natural 2-transformation put⇐ : T M ← get; T N⇒ between triangle functors defined above, which satisfies the (PutGet) law. 4.2.3 Backward propagation of update composition: Toward Lax Putput laws Operation put⇐ provides us with propagation of 1-deltas (updates) and 2-deltas, but does not give us anything for fixing the problems of strict Putput. This is the goal of operation put4 , which provides any composable pair of view updates, i.e., a commutative triangle on the view side, with a complex (non-commutative) triangle including a comparison construct on the source side (see triangle AA00 A./ in Fig. 5). Arity of 4-propagation Given a 2-functor get: M → N , we define a backward propagation operation put4 as the following three family of mappings. a) A family of mappings put4 A : M 1 (A, ∗) ← N 1 (B, ∗), where B stands for get(A) 0 indexed by M -objects, and satisfying the (PutGet) law. (We may assume that this family is borrowed from put⇐ A ⇐0 above, or define it here independently and later require that operations put4A and putA coincide for all A.) 0 b) A family of mappings put4A , which assign to each pair of composable view updates v1 : B → B1 , v2 : B1 → B2 1 a mediating update m12 = put4 A (v1 , v2 ): A12 ← A2 1 as shown in Fig. 7(b), where ui = putA vi , i = 1, 2, 12. c) A family of mappings put4 A , which assign to each pair of composable view updates v1 : B → B1 , v2 : B1 → B2 , 2 a mediating 2-delta ε12 = put4 A (v1 , v2 ) : u12 ⇐ (u1 ; u2 ); m12 2 – see Fig. 7(b) again, where b12 = u2 ; m12 ; owing to associativity of arrow composition, 2-arrow ε12 can be interpreted as mediating delta ε12 : u12 ⇐ u1 ; b12 in the back-side triangle AA1 A12 . :get A A - B .. .. ....... .... ..... .. .. ...... ... ...... .... .... .. .. ..... u2 ... ..... .... .. .. u 1. •..... •1 v .. .. . -ε ......... u1 ; 2 ....... .. .. .. .. ...... - ε ....... .... 12 .. ..  .. .- ... ..... .. .. . :get - .... 1 - .... 12 ..... 12 •.. u1 •.. u1 ; u2 412 • v12 • ... A1 B1 ..•.. .... u ..... u .. .. .... .. .. ... .... .. .. .... .. . u • ....... .... 12 •... ..... .. b .... ...... .. .. • .... ... ..... .. .. v2 .... 2 .... ...... .. .. ..... .... .... -   .? .? ? .. ..  :get A12 ......•......... A2 .......•......... A1 A12 ......................  A2 - B2 m12 u2 m12 (a) (b) Figure 7: Comparison arrows for Putput As Fig. 7(b) shows, configuration of arrows produced by put4 A can be seen as a pyramid. Figure 7(a) presents a planar layout of the same diagram, which shows that a pyramid is just a pair of composable triangles in T A: the first is commutative with base u2 , and the second is non-commutative with base m12 and delta ε12 . The back side triangle of the pyramid (with base b12 ) is exactly the composition of the two front triangles. The construction makes sense for any 2-category C . Definition 3 (pyramid categories). Let C be a 2-category, A∈C C 0 and u, u0 ∈ C 1 (A, ∗) are two arrows with the same source. Like triangles, pyramids are special arrows between such arrows, to wit. A pyramid π : u ⇒ u0 is a • triple (b1 , b2 , ε) with b1 : u• → X, b2 : X → u0 for some object X∈C C 0 called the first and second base of π resp., and ε : u; b1 ; b2 ⇒ u0 called the delta of π. Given two composable pyramids, π = (b1 , b2 , ε) : u ⇒ u0 and π 0 = (b01 , b02 , ε0 ) : u0 ⇒ u00 , their composition is a pyramid π 00 = (b001 , b002 , ε00 ) : u ⇒ u00 with b001 = b1 ; b2 ; b01 , b002 = b02 , and ε00 = ε; b01 ; b02 ; ε0 . For any u ∈ C 1 (A, ∗), the identity pyramid u ⇒u is the triple (idu• , idu• , idu ).5 5 We have defined composition by taking X 00 = X 0 , but there are two other natural ways with X 00 = X or X 00 = u0 • . The one we have chosen works better for our further considerations. It is straightforward to check that composition is associative and identity pyramids are units. Hence, for any 2-category C and any object A ∈ C 0 , we have a category P C A of pyramids over A. A functorial arrangement of the construction can be done in parallel with that for triangle categories in Sect. 4.2.1 It’s easy to see that the three mappings put4 4 A , i = 0, 1, 2 above make a correct graph morphism putA : P M A ← i = 4 = T N B (below we will omit the model spaces subindexes and write putA : P A ← T B). In fact, we can specify the construction of these mappings by saying that we have a family of graph morphisms. Definition 4 (well-behaved put4 ). Given a view 2-functor get: M → N , a backward 4-propagation is a family = of graph morphisms put4 A : P A ← T B indexed by models A from M (as before, we write B for A.get). This family is called well-behaved (wb), if it satisfies the following PutGet law for any model A ∈ M and any commutative triangle v1 ; v2 = v12 in T = B denoted by 412 : (PutGet)4 A (put4 A 412 ).getA = 412 (where getA is the triangle functor generated by get—see Sect. 4.2.1). In detail, the equality above means (Fig. 7(b) illustrates the incidence conditions) (PutGet)4 A 0 (put4 A v).get = v for any v ∈ N 1 (B, ∗); 0 • (PutGet)4 A 1 (put4 A 412 ).get = idB2 (where B2 = v2 ); 1 (PutGet)4 A 2 (put4 A 412 ).get = idv12 (where v12 = v1 ; v2 ). 2 Note that equations (PutGet)⇐ 40 A and (PutGet)A coincide: they both state the PutGet law for updates (i.e., 0 objects in the triangle categories). Functoriality of put4 It is clear that operation put4 maps identity triangles (v2 = idB1 ) to identity, but its compatibility with compo- sition is much more intricate than for put⇐ . Some details and discussion could be found in [4] but are omitted here due to space limitations. Briefly, functoriality of put4 turns out closely related to associativity, and provides a sort of associator on the source side, when updates are propagated. Summary We can define a well-behaved lax (asymmetric delta) lens from a 2-category M to 2-category N as a triple (get, put4 , put⇐ ), in which get: M → N is a 2-functor, and put4 , put⇐ are families of mappings inverse to get in the sense specified above. The two families are required to be mutually compatible in that mappings put4 A 0 ⇐0 M and putA , which propagate view updates to the source side, are equal for all A∈M 0 . Other components of the two put families are different and play different roles: put41 and put42 provide mediation arrows to ensure lax Putput, while put⇐1 and put⇐2 ensure accurate propagation of 2-deltas also subject to a lax discipline. In a proper categorical framework, the two operations can hopefully be integrated into one 2-categorical construct still to be found. We call a lax lens very well-behaved if both put4 and put⇐ enjoy functoriality wrt. triangle and pyramid categories involved, which is necessary for coherent working of the 2-category machinery. A clean categorical elaboration of put4 ’s functoriality is also an important future work. 5 Related work and historical remarks: instead of conclusion Overall, the present paper continues Johnson and Rosebrugh’s program (stated very early in several talks, lectures and recently in [13]) of building bx foundations by progressing from poor to richer categories employed for modelling model spaces. In the sequence of Sets (state-based lenses), Posets (Hegner’s framework [11]), Cats (delta-lenses), 2-Cats appear as a very natural next step. More specifically, Putput problems were noticed as early as in the first classical lens papers [9, 14], and continued to be remarked later, e.g., in [15]. In [8], the relational update composition was proposed as a means to mitigate Putput problems, but it was also noticed that it does not solve all problems. The first investigation of Putput based on solid mathematical foundations was undertaken in [12], where (as mentioned in the introduction) Johnson and Rosebrugh found sufficient and necessary conditions for the relational (they say mixed) Putput to hold. Their analysis seems to be the maximum of what could be done for Putput in the strict (i.e., equality- based) setting. That paper can be seen as the first chapter in the long Putput story (with the previous results classified as prehistorical). The present paper owns to paper [12] the categorical approach to Putput, attention to details, and the very genre of a Putput story. Hopefully, it begins its second – lax – chapter. Acknowledgement. Thanks go to anonymous referees for careful reading the first submitted version of the paper despite numerous typos (for which the author is really sorry), suggestions, and encouragement. I am also grateful to Michael Johnson and Robert Rosebrugh for many stimulating discussions of delta lenses in general, and Putput in particular. References [1] A. Anjorin and J. Gibbons, editors. Proceedings of the 5th International Workshop on Bidirectional Trans- formations, Bx 2016, co-located with The European Joint Conferences on Theory and Practice of Software, ETAPS 2016, Eindhoven, The Netherlands, April 8, 2016, volume 1571 of CEUR Workshop Proceedings. CEUR-WS.org, 2016. [2] Z. Diskin. Model Synchronization: Mappings, Tiles, and Categories. In J. M. Fernandes, R. Lämmel, J. Visser, and J. Saraiva, editors, GTTSE, volume 6491 of Lecture Notes in Computer Science, pages 92– 165. Springer, 2009. [3] Z. Diskin. Asymmetric Delta-Lenses with Uncertainty: Towards a Formal Framework for Flexible BX. Technical Report GSDLab-TR 2016-03-01, University of Waterloo, 2016. http://gsd.uwaterloo.ca/node/660. [4] Z. Diskin. Compositionality of update propagation: Lax Putput. Technical Report GSDLab-TR 2017-02-28, McMaster University, 2017. http://gsd.uwaterloo.ca/node/691. [5] Z. Diskin, R. Eramo, A. Pierantonio, and K. Czarnecki. Incorporating uncertainty into bidirectional model transformations and their delta-lens formalization. In Anjorin and Gibbons [1], pages 15–31. [6] Z. Diskin, H. Gholizadeh, A. Wider, and K. Czarnecki. A three-dimensional taxonomy for bidirectional model synchronization. Journal of System and Software, 2015. In Press. Online at doi:10.1016/j.jss.2015.06.003. [7] Z. Diskin, T. Maibaum, and K. Czarnecki. Intermodeling, queries, and kleisli categories. In Fundamental Approaches to Software Engineering, pages 163–177. Springer, 2012. [8] Z. Diskin, Y. Xiong, and K. Czarnecki. From State- to Delta-Based Bidirectional Model Transformations: the Asymmetric Case. Journal of Object Technology, 10:6: 1–25, 2011. [9] J. Foster, M. Greenwald, J. Moore, B. Pierce, and A. Schmitt. Combinators for bi-directional tree transfor- mations: a linguistic approach to the view update problem. In POPL, pages 233–246, 2005. [10] H. Gholizadeh, Z. Diskin, S. Kokaly, and T. Maibaum. Analysis of source-to-target model transformations in quest. In J. Dingel, S. Kokaly, L. Lucio, R. Salay, and H. Vangheluwe, editors, Proceedings of the 4th Workshop on the Analysis of Model Transformations co-located with the 18th International Conference on Model Driven Engineering Languages and Systems (MODELS 2015), Ottawa, Canada, September 28, 2015., volume 1500 of CEUR Workshop Proceedings, pages 46–55. CEUR-WS.org, 2015. [11] S. J. Hegner. An order-based theory of updates for closed database views. Ann. Math. Artif. Intell., 40(1-2):63–125, 2004. [12] M. Johnson and R. D. Rosebrugh. Lens put-put laws: monotonic and mixed. ECEASST, 49, 2012. [13] M. Johnson and R. D. Rosebrugh. Unifying set-based, delta-based and edit-based lenses. In 5th Int. Workshop on Bidirectional Transformations, Bx 2016, volume 1571 of CEUR Workshop Proceedings, 2016. [14] P. Stevens. Bidirectional model transformations in qvt: semantic issues and open questions. Software & Systems Modeling, 9(1):7–20, 2010. [15] Y. Xiong, H. Song, Z. Hu, and M. Takeichi. Synchronizing concurrent model updates based on bidirectional transformation. Software and System Modeling, 12(1):89–104, 2013.