Compatibility of update propagation with update composition (the infamous 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 ndings. It is known that PutPut trivially holds for the sequential composition of two inserts or two deletes (what Johnson 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 examples. We will also analyze di erent 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.
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 [
We will rst consider di erent ways of update composition, and see that in whatever way an algebraic operation of delta composition is de ned, the real composition appearing in practice could be di erent, and, in general, a user input is required to correct an automatically produced delta. Thus, we have a 2-delta between the 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 su ciently large class of practically interesting and important cases of update propagation.
Thus, di erent deltas, their compositions and relationships between them form the very core of update propagation 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 de ned 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 x the terminology, basic concepts, and issues to be discussed. Speci cally, 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 rst 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
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
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 de nition. Suppose, for example, that N
consists of a class Person with the only attribute name of type String, and the view de nition 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 de nitions via mappings can be found in, e.g., [
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 identi ers (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 gure. Although B has semantically the same objects as A, their OIDs are di erent | 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 di erent computer, and thus OIDs may be di erent when the same get is applied to the same A at di erent 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-de ned single-valued function (we say \get is de ned up to isomorphism"), and we can write
q1: Person name=John q2: Person name=Mary
q1": Person name=John q2": Person name=Mary
q1': Person name=John →2q→1q→ ⋈’BB ><’BB q2→ q1→ ”q2 ”q1 ’”BB [ ⊆ ] ’”BB ”q2 ”q1 Model A p1: Person name1=John name2=Henry p2: Person name1=Mary name2=Ann A A ’ ⋈ A ’”A ”2p
AA ⋈
p p →2→1→ p 1 ” Model A” = A ⋈ p1": Person name1=John name2=Henry p2’’: Person name1 = Mary name2 = ?
p1': Person name1=John name2=Henry 3:put
:get
Corr RAB p1 ← q1 name1← name p2 ← q2 name1← name
Model A <> p1 <>: Person name1=John name2=Henry p2 <>: Person name1=Mary name2=Ann
AA <> Delta <> p1<>← p1” p2<>← p2” 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 de nitions everything would work smoothly.
In the gure, 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 de nition), in the asymmetric lens framework, the correspondence is implicit and o cially does not occur into the output of get{ hence our dashdotted notation for it.
Deltas Consider the following scenario further referred to as Example 1a. In the rst step, model B is updated to model B0. 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 speci ed by a delta BB0 (note the respective block-arrow in the gure), which consists of a single link (q1; q10) (in fact, an ordered pair) showing that the object q1 is preserved in B0. Placing into the delta a targetless arrow from q2 is just a syntactic sugar to show that set of links BB0 does not contain any link from q2, which means that object q2 is deleted in B0. Thus, formally, BB0 is a singleton f(q1; q10)g. 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 B0 is copied to another computer, having a di erent 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 B0 is to be included into the delta. Linking slots in B and B0 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 di erent if Person q1 changed his name from John in B to, say, Jo in B0. In this paper we do not consider attribute modi cations, 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 B0, besides the delta shown in the gure, there is an empty delta that speci es object q10 as a new object di erent from q1, which just happens to have the same name. In this sense, the notation BB0 could be misleading as pairs of models do not actually index deltas, but within our xed scenario, this notation is convenient.
Update propagation As updates are speci ed 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 B0 and BB0 , 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 gure. Note that these computed model and delta are blank (and blue with a colour display) to distinguish them from given (speci ed 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 BB0 (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; BB0 ) rather than (RAB; BB0 ) (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
Suppose that after update BB0 was propagated, model B0 is again updated by adding a new object q200, which is speci ed by delta B0B00 (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 A0A00 . 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 BB0 and B0B00 into a \jump" update BB00 = B;B0 ; B0;B00 (where ; denotes the operation of update composition), and propagate the result to the source side into delta A;A ; from model A to some model A ; : whether A ; = A00 and A;A ; = AA0 ; A0A00 , 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 B0B00 in Fig. 1. The rst delta has a link q1 `-0 q10 targeted at q10, and the second one has a link q10 BB0 and `0-0 q100 started from q10; we will call such links joinable. By composing these links, we obtain a link q1 `0./ -`00 q100 from the source of `0 to the target of `00 (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 BB0 ./ source of the rst 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 have two pairs of joinable links between the same source and target, say, q `-01 q10 `-010 q00 and q `-02 q20 `-020 q00, the composed delta BB0 ./ B0B00 would have two di erent links, q `01./ -`010 q00 and q `02./ -`020 q00 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 B0, and then deleted in model B00. 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;
BB0 ) ./ put(A0;
B0B00 ) = put(A; 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 BB0 and B0B00 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 B00, while the mediating model B0 is entirely ignored. In a sense, this way of composition is opposite to relational, and we denote it by an \opposite" symbol <>: BB0 <> B0B00 d=ef B<>B00 , where B<>B00 denotes the delta produced by matching. theTmhuast,chw-hbialeseidn tdheeltarelatB<io>Bn00alhlyascoamnpaodsedditidoenltaal lin.B/kB0(0q=2; q2B00B)0t.h/at Bm0Ba0k0 e,sobojbejcetctq2q0020i0s tahneeswalmyeinMseratreyd eMaralrieyr, existing in model B, and models B and B00 are thus equal (up to iso). Hence, delta B<>B00 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 nd 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 (Wr-ecohmavpeosciotinosnid),eraenddtwoB<>pBo00ss=ibilitBieBs0 o<f>upBda0Bte00 cfoomrpmoastitciho-nb:ased.B/Bm00-c=ompBoBsi0t.i/on.B0HB0o0wfeovrerre,lawtihoinchal ocfo mthpeosesittiwono variants is right, i.e., correctly models the reality? We instantly nd 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 B<>B00 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 di erent 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 speci ed by model B0 but came back at the moment of model B00.1Then delta .B/B00 is wrong.
Moreover, for models containing multiple classes, there are many formal ways of composing deltas, which di er 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, 1Think, 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 B0 and was hired again at the time of B00. Or, even simpler, the user who was editing model B, deleted Mary and saved the result as B0, but later recognized that it was an error, and so in model B00 the same object Mary is to be restored with all its attributes.
: Note that mapping c<>, which xes 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, BB00 = .B/B00 , then strict Putput stating the equality of two deltas holds | see eq. (1). If the real composed delta is match-based, BB00 = B<>B00 , 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; BB0 ) ./ put(A0; B0B00 ) ./ put2(A; ) put(A; BB00 ) 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. 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 awlewcaayns bendseamfaonrtmicaalllcyo mcoprorescittioans weB#Bha00v(e#ju2stfd./is;c<u>ss;e.d/.<T>h;a::t:gi)s,efqouraal tpoartthiecucloarrrepcatirdoelftadeltBasB00 ,BbBu0t, chBan0Bce00s, that it works for all pairs are not signi cant. For instance, in Example 1, we can have BB00 = B<>B00 , but
B0B000 = B0B00 ./ B00B000 for a consecutive series of updates from B0 to B00 to B000. We need to nd a way of managing this diversity.
As we have di erent 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 speci ed in the equations below: 2.3
Relational vs. match-based composition vd<e>l d=ef p2, and vi.n/s d=ef p00.
2 First, we need to make the notion of (structural) delta more accurate via the notion of span. That is, an update udel u of model X to model Y is modelled by a diagram X Hu ui-ns 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 BB0 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 i uins is the identity of Y (up to iso), and u is a pure insertion i 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: v0 : B 9 B0, v00 : B0 9 B00, and let v./ : B 9 B00 and v<> : B 9 B00 denote their r- and m-compositions resp. The r-composition is given by the pullback (PB) of mappings vi0ns and vd00el as shown in the diagram Fig. 2 (note the label [pb1]), which precisely describes the operation of joinable link composition that we considered above. Thus, Hv./ d=ef H1, vd./el d=ef p01; vd0el, and vi.n/s d=ef p00; vi0n0s. The m-composition is speci ed by another PB: a key set of attributes is modeled by a set of 1 functions from the object set of a model to some domain of values (note arrows key and key00, which actually are tuples of functions), to which we apply PB (note the label [pb2]) and obtain span (H2; p2; p020). Now Hv<> d=ef H2, (2) (3) (4)
If the diamond H1BValB00 is commuttaive (we will discuss it shortly), i.e., (tpphin01e;gnp01!b0)yasatnhsdehou(wpn2ni;vpein02r0s)a,tlhiateryedoijafogi[nrptablm2y],.mwoNenoihtceav(atehsaaptruoandlitquhucoeeudlgyhbdyeboPntBhed),spmsapanapsn-, ! p01 vin0s- H = (p01 ; vd0el; p010 ; vi0n0s) is not necessarily monic, and hence mapping ! H2 H1 [pb1] is not necessary injective (and indeed, matching does not care about p100 by how many ways an object in B can be linked to its match in B00 - v00del iavsniaqduabitmeeceondmoiaremtsinaagl s(oeebt.gjie.n,cctinluinosiuBorn"E)w.xhaBemunptwliefe1scp)o,anntshiHednerimshjaeopainpdtisnlygofm!siopsnaiinncs,jewuctphiivcteho, p200 Hv00 vin-0s0- ke0y0 iso { this is the inclusion in Fig. 1.
Commutativity (5) is essential for the existence of mapping !. This B00 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 B0 and will keep it in B00, then semantically composition true link q1q100 2 Hv./ will be lost in Hv<> . On the other hand, if there was some Jo in model B, who is deleted from B0 and B00, matching B and B00 would mistakenly link two di erent 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 di erent objects at a model state have the same name. Thus, the match-based composition is semantically awed 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 v0 : B 9 B0, v00 : B0 9 B00 and their r-composition v./ = v0./ v00 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. v0del k e y Av ) v ( utA p = u --" c 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 = putAv0 and u00 = putA0 v00, where we use a bit more compact notation, in which delta put(A; v) is denoted by putAv. We assume that Putput holds for r-composition, and thus u./ d=ef 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 B00, 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 di erent, and deltas u = putAv and u./ are also di erent and even non-parallel. However, as model A./ has nulls where model Av has certain values, there is a uniquely de ned (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 v0 is insertion, while v00 is the respective deletion. 3
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 gure.
Now suppose that an updated view B0 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 speci ed with delta v00 : A0 9 A00 and is lost for update v00. On the other hand, relational composition v./ = v0./ v00 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 di erence 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 de ned mediating delta m./ : A./ 8 A00 (consisting of a set of horizontal links in Fig. 4), which map
2A rather complicated theory of uncertain models and completions can be found in [
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 B0. 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 su ciently general mechanism of violating strict Putput,
but keeping a lax Putput|we discuss this in the next section.
In simple cases, a view de nition 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 rst augment M with derived elements de ned by queries (in fact, such
elements are query de nitions), and then cut out a required part in the augmented M , i.e., a view de nition is a
Kleisli mapping w: Q(M ) N wrt. the monad specifying the query language. Then computing the w-view of
model A 2 M , getw(A), amounts to, rst, 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 nally retyping the result to metamodel N .
Details of how this works can be found in [
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 di erent 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 B00 = 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 \ ghting" constraints and are of equal power (like budgetary and performance requirements 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 red 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 nally the piece ZR (workstation w2) generated by \unidirectional" contraints R is deleted. Composing just speci ed 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 underlying 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 de nition cases, and their interaction between themselves and update propagation were speci ed 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). Diagram in Fig. 3 speci es 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 modi ed 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./ = v0./ v00. The real update delta v supersets v./ which is shown by a 2-arrow .
Deltas v0 and v00 are propagated to u0 and u00 resp, and u000 = u0./ u00 (note the second commutativity declaration). However, the backward propagation of v./ , putAv./ , is not equal to u000 as relational Putput can fail if v0 is an insertion and v00 is a deletion. Thus, putAv./ is a di erent 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 di erence between these two triangles is that c is a partial completion mapping that does nothing besides lling some null slots with values (recall our Example 1). In contrast, while delta m./ also includes a signi cant 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
We will outline a formal framework, in which our preceding discussion can be speci ed. This work is in progress, some constructs behave well and settled, but there are also several ad hoc de nitions, whose clean categorical elaboration is still to be found. 4.1
As discussed in [
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 B3, 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. 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 i2I, (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 rst we need some preliminaries. In more detail, an arrow u1: A ! 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 u1; u ) u2 COb1L(jAeect;tsA),o2faTnCdA0 cbaarenea1bn-eaorcbroojnewvcste.rftrTeodhmeinAste,oti.aoef.c,aaOltleb1gj-oTarrAyroT=wAsCfir1no( Amth; eA)f.oislAldoweTniAno-gtaerdwraobywy. A1 u - A?2? from 1-arrow u1: A ! A1 to 1-arrow u2: A ! A2 is a pair 4 = (u; ) as shown in the inset gure 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 de ne composition of triangles by their tiling: given 4 = (u; ) : u1 ) u2 and 40 = (u0; 0) : u2 ) u3, composition 4; 40 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, TA is a category.
There are two special subcategories in TA, which have all objects that TA has, but fewer arrows. The rst 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 nA).
Any arrow f : A A0 gives rise to a reindexing functor f : TA ! TA0 in an obvious way by precomposition. , and triangle u1 u;- u2 is mapped is mapped to f (u1) d=ef f ; u1: A0 ! to triangle (f ; u1) u;f-; (f ; u2) with the same base u but a di erent (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 3in 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 1arrow 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 A2C 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 2 C 0. Backward propagation is modelled by two families of mappings inverse to get, both indexed by models A from M . The rst family, putA(: T M A T N)B, manages backward propagation of 2-deltas. The second, putA4: 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 putA4 are pyramids | constructs slightly more general than triangles.) Below we describe these two families in detail. 4.2.2
Suppose for a view B = get(A), we have two parallel updates from B, v1; v2: B ! B0, one subsetting the other
via : v1 ) v2 (see Fig. 6). It means that v1 creates more new objects in B0 (more accurately, more objects in B0
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 de ned partial
completion update c : A01 ! A02 and uniquely de ned 2-arrow " : u1; c ) u2. In its current state, the theory
of partial completions [
Arity of (-propagation Given a 2-functor get: M ! N called a view, we de ne an operation of backward (-propagation put( as the following three family of operations/mappings.
a) A family of mappings putA(0 : M 1(A; )
N 1(B; ) indexed by M -objects ( as before, B = get(A)). 4
b) A family of mappings putA(1 , which assign to each 2-delta : v1 ) v2 between parallel view updates v1: B ! B0, v2: B ! B0, a mediating update c = putA(1 ( ): A02
A01 as shown in Fig. 6, where ui = putA(0 vi, i = 1; 2; 12.
c) A family of mappings putA(2 , which assign to each 2-delta as above, a mediating 2-delta " = putA(2 ( ) : u2 ( (u1; c ) { see Fig. 6 again. Thus, the result of backward propagation is a triangle u1 (c ;"-) u2, and it is easy to see that the three mappings above de ne a correct graph morphism putA(: TA T (B. In fact, we can specify the construction above by saying that we have a family of graph morphisms.
De nition 1 (well-behaved put(). Given a 2-functor get: M ! N (a view), a backward (-propagation operation is a family of graph moprhisms putA(: 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 satis es the following PutGet law for any model A 2 M and any 2-delta : v1 ) v2 considered as a triangle in T N)B: (PutGet)A(
(putA( ):get = .
4Index 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 )
A03 ? A01 u1 :get B0
0 ) ) ? ? ? v3
In detail, the equality above means (PutGet)A(0 (PutGet)A(1 (PutGet)A(2 (putA(0 v):get = v for any v 2 N 1(B; ); (putA(1 ):get = idB0 (where B0 = v1 = v2 ); (putA(2 ):get = .
Functoriality of putA( Our examples show that in practice putA( has nice functorial properties shown in Fig. 6 (this is, in fact, transitivity of subsetting). Hence, we can require putA( to be a functor without being too restrictive for practical applications. Moreover, this functor is normally compatible with reindexing.
De nition 2. Operation put( is called very well-behaved (vwb), if it satis es the following Stability (identity preservation) and PutPut (2-composition preservation) laws speci ed below.
For any model A and update v: B ! , we require (Id)A(1
putA(1 (idv) = idu , where u = putA(0 v and u is its target model. (Id)A(2 putA(2 (idv) = idu, where u = putA(0 v.
Below we will encode these two equations as the Stability law for put(: for all A2M 0, (Id)A( putA((idv) = idu, where u = putA(0 v.
We also require, for any model A 2 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 putA(1 ( ; 0) = putA(1 ; putA(1 0 (PutPut)A(2 putA(2 ( ; 0) = (putA(2 ; putA(1 0) ; putA(2 0
Below we will encode these two equations as the PutPut law for put(: for all A2M 0, (PutPut)A(
putA(( ; 0) = putA( ; putA( 0 Finally, for any A and update B v- B0, we require the following diagram to commute: u
TA
6 TA0 putA( putA(0
T )B 6 v T )B0 (8)
The data above can be compactly speci ed 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 de ned above, which satis es the (PutGet) law.
Operation put( provides us with propagation of 1-deltas (updates) and 2-deltas, but does not give us anything for xing 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 AA00A./ in Fig. 5).
! N , we de ne a backward propagation operation put4 as the following three family Arity of 4-propagation Given a 2-functor get: M of mappings.
a) A family of mappings putA40 : M 1(A; )
N 1(B; ); where B stands for get(A) indexed by M -objects, and satisfying the (PutGet) law. (We may assume that this family is borrowed from putA( above, or de ne it here independently and later require that operations putA40 and putA(0 coincide for all A.) b) A family of mappings putA41 , which assign to each pair of composable view updates v1: B ! B1, v2: B1 ! B2 a mediating update m12 = putA41 (v1; v2): A12
A2 as shown in Fig. 7(b), where ui = putAvi, i = 1; 2; 12.
c) A family of mappings putA42 , which assign to each pair of composable view updates v1: B ! B1, v2: B1 ! B2, a mediating 2-delta
"12 = putA42 (v1; v2) : u12 ( (u1; u2); m12 { 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 AA1A12.
A ............................u....1..2......................-.........."......1..2u..1.;..u...2..................................................................?u1 A12 ...... ......... A2 ....... ......... A1 m12 u2 (a)
As Fig. 7(b) shows, con guration of arrows produced by putA4 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 TA: the rst 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 .
De nition 3 (pyramid categories). Let C be a 2-category, A2C 0 and u; u0 2 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 X2C 0 called the rst 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 = (b010; b020; "00) : u ) u00 with b010 = b1; b2; b01, b020 = b02, and "00 = "; b01; b02; "0. For any u 2 C 1(A; ), the identity pyramid u )u is the triple (idu ; idu ; idu).5
5We have de ned composition by taking X00 = X0, but there are two other natural ways with X00 = X or X00 = 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 2 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 putA4i , i = 0; 1; 2 above make a correct graph morphism putA4: P M A T N= B (below we will omit the model spaces subindexes and write putA4: PA T =B). In fact, we can specify the construction of these mappings by saying that we have a family of graph morphisms.
De nition 4 (well-behaved put4). Given a view 2-functor get: M ! N , a backward 4-propagation is a family of graph morphisms putA4: PA 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 satis es the following PutGet law for any model A 2 M and any commutative triangle v1 ; v2 = v12 in T =B denoted by 412: (PutGet)A4 (putA4412):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)A40 (PutGet)A41 (PutGet)A42 (putA40 v):get = v for any v 2 N 1(B; ); (putA41 412):get = idB2 (where B2 = v2 ); (putA42 412):get = idv12 (where v12 = v1; v2).
Note that equations (PutGet)A(0 and (PutGet)A40 coincide: they both state the PutGet law for updates (i.e., objects in the triangle categories).
Functoriality of put4
Summary
It is clear that operation put4 maps identity triangles (v2 = idB1 ) to identity, but its compatibility with
composition is much more intricate than for put(. Some details and discussion could be found in [
We can de ne 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 speci ed above. The two families are required to be mutually compatible in that mappings putA40 and putA(0 , which propagate view updates to the source side, are equal for all A2M 0. Other components of the two put families are di erent and play di erent 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
Overall, the present paper continues Johnson and Rosebrugh's program (stated very early in several talks,
lectures and recently in [
More speci cally, Putput problems were noticed as early as in the rst classical lens papers [