In Model-Driven Engineering, bidirectional transformations are key to managing consistency and synchronization of related models. Deltalenses are a exible algebraic framework designed for specifying deltabased synchronization operations. Since model consistency is usually not a one-to-one correspondence, the synchronization process is inherently ambiguous, and consistency restoration can be achieved in many di erent ways. This can be seen as an uncertainty reducing process: the unknown uncertainty at design-time is translated into known uncertainty at run-time by generating multiple choices. However, many current tools only focus on a speci c strategy (an update policy) to select only one amongst many possible alternatives, providing developers with little control over how models are synchronized. In this paper, we propose to extend the delta-lenses framework to cover incomplete transformations producing a multitude of possible solutions to consistency restoration. This multitude is managed in an intentional manner via models with built-in uncertainty.
A basic assumption underlying the lens framework to bidirectional transformations (bx) is that an update policy ensuring the uniqueness of backward propagation is known to the transformation writer at design time. Each operation of forward propagation is supplied with a corresponding backward operation based on some update policy, which is a priori known to the transformation writer so that the transformation language becomes bidirectional. This idea was emphasized by the lens creators by calling the approach linguistic [FGM+07]. This implies that backward propagation can be modeled by a single-valued algebraic operation, and thus semantics of bx can be speci ed in ordinary algebraic terms as a pair of single-valued operations subject to a set of ordinary equations (laws). On this base, the entire algebraic machinery of lenses, including delta-lenses, is built.
However, this major assumption has the following major drawback. At the time of transformation writing, the policy is often not known or uncertain, but postponing the transformation design until the policy will be known is also not a good solution. To choose the policy, the user should normally have the possibility to observe possible variations, compare them, and discuss with the stakeholders involved, so that choosing a right policy is typically a process depending on many parameters and contexts. Requiring the transformation writer to select a single update policy at the design time could be a too strong imposition, and tools based on the current lens framework gives the user little (if at all) control over the inherent uncertainty of update propagation.
A straightforward approach to enriching lenses with an uncertainty mechanism would be to consider multivalued transformations modeled by multi-valued operations. However, multi-valued operations essentially complicate the algebraic framework, and are not easy to manage technically. Our idea is di erent, and allows us to manage uncertainty within the usual algebra of single-valued operations. We extend model spaces with incomplete (uncertain) models, each of which determines a set of its full completions, which are ordinary complete (fully-speci ed, certain) models. This allows us to model a multi-valued underspeci ed transformation by a single-valued one, which results in an incomplete/uncertain model encoding the required set of ordinary complete models. Thus, what is essentially changed is the notion of model spaces over which delta lenses operate rather than the very notion of a delta-lens (but, of course, the latter also needs a suitable adaptation).
Structure of the paper. The next section presents an example to motivate the importance of modeling uncertainty in bx. In Sect. 3, we discuss the example in terms of delta lenses and model completions. Section 4 presents a formal model along with its discussion. Related work is discussed in Sect. 5, and Sect. 6 draws conclusions and future plans. 2
A major problem that one needs to deal with in bx is that the consistency relation between model spaces is often of many-to-many or one-to-many types, so that restoring consistency is an inherently ambiguous process [Ste09, ZPH14]. Consistency violated by an update on one side, can be restored by updating the other side in multiple ways, which makes at least one direction of update propagation a multi-valued operation. For example, the budget of a complex project can be uniquely computed, but if the budget is changed, there are usually many ways to change the project to adjust it to the new budget. To make the update propagation a single-valued operation, the transformation designer should make certain assumptions (often referred to as an update propagation policy) ensuring uniqueness of consistency restoration in a reasonable way. Non-triviality of this problem is well known in the database literature for a long time under the name of the view update problem [BS81]. Indeed, the budget is a view of a project, and adjusting the project to a new budget is nothing but propagation of the view update back to the source. Below is a simple scenario illustrating the problem. 2.1
Helen is a manager of the Human Resources (HR) department. She tracks and analyses employee scheduling and performance, and negotiates employee contracts. The budgetary resources for projects are managed by Fred, an o cer of the Finance and Accounting (FA) department. HR and FA work together on the budgeting process and need an automated synchronizing system (a bx-engine), which was developed by an IT-department star Ian.
MMH
name: String pid: String salary: Integer /budget: Integer * workforce 1 /budget = ∑ {e.salary: e in p.workforce} VIEW DEFINITION
MAPPING
MMF
pid: String budget: Integer workforce of the project as shown by model A in the top left of Fig. 2: she hired two senior engineers, Ben and Bill, with equal salaries 100. Query /budget de ned in metamodel M MH , can be executed for model A and results in the /budget(A)=200.
Engineers Ben and Bill have been working hard but with a limited success, and when the company has undertaken administrative cost reductions, Fred is forced to cut the PME budget to 150 (as depicted in the model B0). To adapt the project to the reduced budget and restore consistency between the HR and the FA models, the system designed by Ian prescribed to cut salaries of Ben and Bill and make them each equal to 75.
Ian is a great fan of delta-lenses, and when he was tasked to implement a bx system, he implemented a deltalenses framework, in which propagation operations use deltas as input and output rather than compute them internally. Deltas consist of links between model elements. Horizontal links specify correspondences between the elements of models to be synchronized, e.g., horizontal delta AB in Fig. 2 consists of three links: L0 relating objects, and L01; L02 relating the respective attributes. Note, these links are instances of the respective view de nition links (i.e., associations) in Fig. 1. (Formally, instance links are just pairs of elements written with arrows.) The link L02 in AB maps attribute budget of model B to the derived attribute /budget in model A, and as values of the two attributes are equal, we consider models to be consistent. Vertical links specify traceability from the original to the updated model. For example, the vertical delta BB0 in Fig. 2 consists of three links, which say that the project q2 with its attributes in model B0 is the same project with the same semantics of attributes as in model B. However, as the values of the attribute budget in models B and B0 are di erent, we conclude that the attribute budget is updated in B0. conAsisstmenotd(eblsudAgetasnadreBd0i aerreenitn)-, A p1: Project w2:workforce B tcohafellbeaddcepkltuwata-urldepndsautpeidn-bavatocekkepsorroojp↔puasegt←raaptt→uiioot)nn. w1:weo1rk:fEorn/pcbgeiduin=degPeeMrt=E200 e2: Engineer LLLD000e:12ltp::a1ppΔ:11P..ApbrBoiudjde←gcett←q←1.qpq1id1:P.broujdegcett pbiudd=gqPe1tM=:PE2r0o0ject This operation (shown in Fig. 2 by name= Ben name= Bill a chevron put, takes two deltas, salary= 100 salary= 100 tadOhneIAeldDtiBrasp)rsaaoonrduedAurAccsee0hsoB(aawonBnnnd0l,yuttptoaldoirnaggskteeaesttvhe(bemvreestorpwdwtaieeciceltaesnhl,, A’LLLD210e:::lteepa211Δ:::EEPArnnAogg'jiiepnnc2eet:ee→Prrr→→opj2eee:cP43t::rEEojnneggciitnneeeerr :put LLLDB000e:21’lt::aq1qqΔ:11PB..Bbpro'iudjde→gcett→q→2.qpq2i2d:.Pbruodjegcett the attribute links can be restored pid= PME w4:workforce fdwmraohotmideledeltsthhceeoamrndr)deestrpoidvgoeeenldttdhaemesnrocadewr.eielthasnahGdnaditvuewepdno-, w3sn:waaeolma3rrke:yf=oE=rnBc7/bege5uinndegeert= 150nsaaelma4re:y=E=nB7gi5llineer LLLD000e:12ltp::a2ppΔ:22P..Apbr'Boiud'jde←gcett←q←2.qpq2id2:P.broujdegcett bpiudd=gqPe2tM=:PE1r5o0ject deltas are blank (and blue with a color display). Figure 2: An example of a single-valued delta len
As there are many ways to restore consistency, to make put single-valued (certain, deterministic), some update policy ensuring uniqueness is needed. Ian has based his lens design on a simple and reasonable policy: a budget cut is to be propagated to cuts in the salaries of all engineers proportionally to the values of salaries. Since Ben and Bill have equal salaries, the cut in 50 units results in 25 cut for each of them. 2.2
..but not as easy as it may seem.
Unfortunately, Helen was not happy with the automatic update provided by the delta lens. She told Ian she was not sure that cuts should be equal, rather, they should depend on some background information about the engineers and their contribution to the PME project, with which she still needed to familiarize herself. She also mentioned that she is disappointed with the result of synchronization via delta lenses that Ian so much praised.
After a few days of thinking, Ian found how to make the lens framework more exible. Now put would produce an incomplete (or uncertain) model A01, in which the attributes salary of the engineers are uncertain but must be within a prede ned range, e.g.[65..85], as shown in the left part of the Fig.3. Constraint C1 ensures that although the user can vary the salaries, their sum must be not greater than 150. (Moreover, Helen could even modify the lower and upper bounds of the ranges if needed.) Incomplete model A01 has multiple nal completions, i.e., models with xed values for the attribute salary, e.g., 70 for Ben, and 80 for Bill. In-between, there are many completions that are not- nal, e.g., [65..70] for Ben and [85..80] for Bill. Thus, the lens framework should include the notions of uncertain models and their completions, which seem to be not very di cult to manage.
Being very satis ed with the solution, Ian came to HR again, A but found another problem. Af- p1: Project w2:workforce ter studying the employee pro- pid= PME Bleens, aHndeleBnillfoaurnedsetnhiaotr aa↔snd←boe→txh- w1:workfor/cbeudget= 200 perienced engineers, reduction of e1: Engineer e2: Engineer their salary is not a good solu- snaalmarey==B1e0n0 nsaalmarey==B1i0ll0 tion at all. A Helen's new idea was to keep one of the engineers Delta ΔAA'1 Delta ΔAA'2 with the same or even increased LL10:: ep11::EPrnogjiencete→r →p2e:P3:rEojnegcitneer LL01:: pe11::PErnogjiencete→r →p2e:P3:rEojnegcitneer ? salary, and hire a recent gradu- L2: e2:Engineer → e4:Engineer L2: e2:Engineer → e4:Engineer ? ate as his assistant for a smaller |= L1 XOR L2 spbareloabarecyh. xeeAxdgibbaluient,,sraatlotahrekireesekpsehpotthuwilsditnhaopint- A’1 /pbidup=d2gP:eMPt=Ero1j5e0ct w4:workforce A’2 /pbidup=d2gP:eMPt=Ero1j5e0ct w4:workforce some prede ned ranges. When w3:workforce w3:workforce Ian asked which of the engineers, e3: Engineer e4: Engineer e3: Engineer e4: Engineer sBhene oarnBswilelr,edHetlhenatinstheendwsotuoldkedepe-, nsaalmarey== B[6e5n..85] nsaalmarey== B[6il5l..85] nsaalmarey== B[1e0n0+..1S1t0ri]ng nsaalmarey== B[1il0l0+..1S1t0ri]ng cide this later. or [40..50] or [40..50]
After some thinking, Ian im- C1: e3.salary + e4.salary <= 150 C1: e3.salary + e4.salary <= 150 plemented a new lens satisfying sHheoluenld'spnroedwucaepapnroianccho:mpthleitse luenps- Figure 3: The incomplete models A01 and A02 date AA02 resulting in an incomplete model A02 as shown in the right part of Fig.3 (where + denotes the disjoint union of a singleton set and the set of strings, and union of integer ranges is denoted by \or" to avoid confusion with addition of numbers). Delta AA02 is composed of three object links, two of which are optional. It means that engineer e3 could be Ben, if link L1 is present in the delta, or be a new engineer with unknown name, if link L1 is removed from the delta; similarly for the link L2. Moreover, the XOR constraint speci ed in the logical part of the delta labeled with j=, says that one and only one link must be present, i.e., one of the engineers e3,e4 must be a previous engineer and one must be a new hire. In addition, we mark each link with symbol ? showing its optional existence.1 Two other constraints on possible completions are assumed speci ed but not shown in the gure: if link L1 is present, then e3.salary is within the range [100..110], and if it is absent, then the salary range is [40..50]; similarly for link L2 and the salary range for e4.
However, at the moment Ian nished debugging his new bx system, Helen informed him that she talked to her boss Hilary, who said that the possibility of leaving in the project only one engineer is not excluded. Moreover, Hilary told Helen that the board of directors is thinking about cancelling the PME project, but is not certain yet, and needs to analyse some additional data to take a decision. At this point Ian became entirely convinced that incorporating uncertainty into the lens framework was an urgent task of vital importance for lenses. 3
A straightforward approach to enrich lenses with an uncertainty mechanism would be to consider multi-valued transformations modeled by multi-valued operations. However, multi-valued operations essentially complicate the algebraic framework, and are not easy to manage technically. Ian's (and our) idea is di erent: we extend model spaces with uncertain, or incomplete models (which can be seen as incomplete instances of the respective metamodel as described in [BDA+13, RE15]). Each such an incomplete model determines a set of its full completions, which are ordinary fully-speci ed models. This allows us to model a multi-valued underspeci ed transformation by a single-valued operation, which results in an incomplete model encoding the required set of 1In the presence of the XOR-formula above, ? labels are redundant yet suggestive. Moreover, they become very handy if we want to declare optional existence of both links without constraints so that there are four possible con gurations: fL1; L2g, fL1g, fL2g, and ;. Then we simply mark optionality of each of the links without further constraints. fig. ordinary complete models.
The example below illustrates the main ingredients of the approach. Figure 4 depicts Ian's system within the delta-lenses framework with built-in uncertainty, which we call delta-lenses with uncertainty. The incomplete update AA0 : A A0 represents a set of update policies discussed with Helen; in fact, it encodes two updates from Fig. 3, but canceling the entire PME project is not considered. That is, updates AA01 : A A01 and
AA01 : A A02 from Fig. 3 can be seen as non- nal completions of update AA0 : A A0: they are more complete than it, but not all the choices are xed.
In more detail, the process of update completion is described in Fig. 5. The schema of the process is described in the upper part above the dashed line. The part below the line presents an instantiation of the schema: nodes are models, vertical and inclined arrows are update deltas, and horizontal arrows are completion deltas (i.e., C-Delta). The scheme consists of three cojoined triangles, 4AA0A01, 4AA01A02 and 4AA02A03, whose tiling is distorted in the lower part of the gure to t in the page. Horizontal arrows (bases of the triangles) are model completions; more accurately, a completion is a triple consisting of a less certain model, more certain model, and the c-delta relating them. a Ecoamchploeftitohne torfia nitgslesridghestc-hriabneds A p1: Project w2:workforce B suuipndddeearutsept,odoadtwehateosreiatsatnlreifptlu-ehpa↔dncaod←tness→iisdties- w1:weo1rk:fEorn/pcbgeiduin=degPeeMrt=E200 e2: Engineer LLLD000e:12ltp::a1ppΔ:11P..ApbrBoiudjde←gcett←q←1.qpq1id1:P.broujdegcett pbiudd=gqPe1tM=:PE2r0o0ject ing of the original model, the name= Ben name= Bill updated model, and the delta salary= 100 salary= 100 rcaeonlmdatmintuhgteatthilveefemt:-m.ionsTtehatecrhiarnioggfhlett-smheaomrset, LLLD012e:::ltpeea112Δ:::PEEArnnAogg'jiiennceetee→rr→→p2ee:P34::rEEojnneggciitnneeeerr ?? LLLD000e:12lt::aq1qqΔ:11PB..Bpbro'iudjde→gcett→q→2.qpq2i2d:.Pbruodjegcett the left delta is a composition L1 OR L2 :put co-fdtehltea.riTghhet mdeidltdalewtritiahngthleeisbnaoset A’ pid=p2P:MPEroject w4:workforce B’ i(cuseon2nmd!oemtresui4ntta)ca2nltudivdAteeAh:d01is;itn(haetseo4 !croseAmt4Ac)p022oo.mCsWepdAoe01slcAii nna02nkg wsnaa3lm:awere3oy=r:=kEBf[o[1en1r/0cn5gb0e0ui+n.]d.1eoSg1eret0rrti]=n?og1r50snaalmaere4y=:=EB[[1in1l0l5g0+0in.].S1eot1erri0rn]g?or LLLD000e:12lt::pa2ppΔ:22P..Apbr'Boiud'jde←gcett←q←2.qp2qid:2P.broujdegctet pbiudd=gqPe2tM=:EP1r5o0ject two deltas AA01 ; C A01A02 , and [[6405....5805]] or [[6405....5805]] or then transforming the result by the removal of the link speci ed Figure 4: A round-trip scenario with uncertainty. above.
Models, in general, consist of two parts: a set of objects and links (called an object diagram in UML), and an uncertainty mechanism; the latter, in its turn, may have three components: (a) ranges of possible values for some attributes (e.g., salary in model A0), (b) optionality of some objects (e.g., in model A0, optionality of objects e3, e4 is shown by ? marks), and (c) logical formulas that constrain possible completions. E.g., formula e3 _ e4 says that a completion in which both engineers are removed is prohibited (although the existence of each of the engineers is optional). Update deltas, in general, also consist of two parts: a set of links that speci es a mapping (relation), and a logical formula (marked with j=) that constrains possible completions. For example, formula L1 _ L2 in AA0 says that the delta can be completed by keeping one or both links. In addition, the update speci cation includes logical formulas relating uncertainty of both the delta and the updated model. E.g., for incomplete update AA0 : A A0, if in a possible completion, link L1 is kept but both link L2 and object e4 are deleted, then the salary of object e3 in this completion must be 150, while if both links are kept, then salaries of e3 and e4 are to be within the range [65..85]. These inter-delta-model constraints again show that an update is a triple of objects rather than just its delta.
The completion speci ed by triangle AA0A01 is the following one. The updated model must contain two engineers (with commutativity of the triangle and removal of the salary value 150), but the option of keeping both previous engineers is now excluded due to the constraint L1 xor L2 in delta AA01 , which is stronger than constraint L1 _ L2. All this makes update AA01 more certain, or more complete, than update AA0 . However, it is not fully certain in that which of the engineers is to be kept is still not decided The next completion triangle decides to keep Ben and hire a recent graduate, but their exact salaries are still not certain. Finally, the third
Delta AA’2 Delta AA’2 LL10:: ep11::EPrnogjeincete→r →p2e:P3:roEjencgtineer
Delta AA’1 L0: p1:Project → p2:Project L1: e1:Engineer → e3:Engineer ? L2: e2:Engineer → e4:Engineer ? |= L1 XOR L2 A’1 rce o fr k o w : 3 w e3: Engineer name: Ben + String salary: [100..110] or [40..50]
p2: Project pid= PME /budget= 150
e4: Engineer name: Bill + String salary: [100..110]
or [40..50] CL-0D: eplt2a->Ap’21A’2 L1: e3->e3
L2: e4->e4 AA’2
A’2 'f:rrkco1oeww /pbidu=pd2gP:eMPt=Er1o5je0ct 'f:rrkcoo2eww e3: Engineer e4: Engineer name: Ben name: String salary: [100..110] salary: [40..50]
C-Delta A’2A’3 L0: p2 -> p2 L1: e3 -> e3
L2: e4 -> e4 [=] A’2 e c frr o k o w : 4 w
C-Delta A’A’1 L0: p2 <- p2 L1: e3 <- e3 L2: e4 <- e4
A triangle xes exact salaries and thus results in a (fully) complete update complete model A03. A’3 The rst issue in building incomplete bx is a suitable enrichment of the notion of a model space. However, building a formal model of incomplete models and their completions is challenging |as challenging as many other problems of dealing with uncertainty. These problems are a classical subject of database and AI research, whose foundations are still debated. Speci cally, in a recent series of seminal papers [Lib14b, Lib14a, Lib15], Leonid Libkin showed a major de ciency of a widely accepted common approach to uncertainty (the so called certain answers), and proposed a simple elegant framework to x the de ciency. In a nutshell, Libkin proposed to view incomplete models (databases) as both semantic objects (i.e., as models in the parlance of the classical model theory) and syntactic knowledge (i.e., theories) about the objects, and built a corresponding formal framework.
The two-fold view of uncertain models is smoothly integrated in our approach to uncertainty originated in [BDA+13]. In a nutshell, we formally model the process of models completion by arrows in a suitable category, so that progressing from an uncertain model A to its particular full completion can be seen as an arrow chain c = (Ac0 ! Ac1 ! Ac2 ! ::: ! Ac ) with Ac0 = A and Ac being a fully certain model. Each model Ak in this chain a a besides the last one (k = 0; 1; :::) can be a branching point of the completion process, which can go into another direction (Ak = Ac00 ! Ac10 ! ::: ! Aac0 ) terminating at another fully certain model Aac0 , and so on. In general, even small nite uncertain models can have an in nite number of completions exactly like small nite theories can have an in nite number of models. For any two-arrow fragment of a completion chain, An 1 ! An ! An+1, model An can be seen as both a semantic model for theory An 1 and a theory of model An+1. Fully certain models are thus theories of themselves. In this section, we develop the arrow view of completion into a formal framework of model spaces with uncertainty, and show how the notion of a delta lens could be adapted to work over such spaces and respect uncertainty.
Our plan is as follows. Section 4.1 presents our categorical notation, sometimes not quite standard. Special attention is paid to an elementary construction of arrow triangles, which is heavily used later. In Sect. 4.2, we formalize the completion process sketched above with the notion of u-space (`u' stands for uncertainty). A logic for u-spaces is introduced in Sect. 4.3. However important are uncertain models and their completions, our main objects of interest in BX are updates, and they can also be uncertain as we have seen in our running example. Hence, in Sect. 4.4 we introduce uu-spaces, which formalize both uncertain model and uncertain update completions (hence, `uu' in their name). Update completions are formalized as special arrow triangles, hence the attention to the construct in Sect. 4.1.3. Section 4.5 is the culmination. We introduce two constructs to relax the rigidity of ordinary single-valued update policies. The rst one, multi-valued update policies, do it in a direct semantic way with the notion of a multi-valued operation. The second one, uu-lenses, do it indirectly (and we may say syntactically) by encoding a multitude of models by a suitable uncertain model. Our main results specify a pair of adjoint functors between the categories of multi-valued policies and uu-lenses built over the same given view functor get, so that the two notions are, in a sense, equivalent. Thus, uu-lenses can be seen as a sound and complete representation of multi-valued update policies.
Several words about formalities as such. As is traditional for the lens framework, the mathematical structures are very general, and specify basic relationships and operations over models and updates without saying what models and updates really are. This abstraction allows one to instantiate lenses with rather di erent notions of a model, e.g., models can be attributed typed graphs, relational databases, semi-structured data/XML documents, or models of a FOL theory, enriched with an uncertainty speci cation mechanism. In stating the axioms (laws) our structures should satisfy, we were trying to respect the following requirements. First, we wanted to exclude what we feel are wrong examples, and allow for (what we feel are) the right ones. Checking the axioms for concrete instantiations is a work in progress, some results can be found in [Dis16]. Second, the laws should allow us to prove our results in a su ciently direct way. We did not strive to present an economical system of axioms|it is possible that some of them can be inferred from the others, nor we strived to nd the most economical presentation. Some unintended omisisons are, unfortunately, also possible: the formal section of the paper was signi cantly extended after submission, and so far the proofs were not peer reviewed. Overall, as both checking our formal requirements against major instantiations and completing the proofs are a work in progress, our formal de ntions are somewhat experimental and subject to change. We consdier the paper as a working paper for a working workshop. The accompanying technical report [Dis16] is intended to provide a maintained version of the formal framework for some time onwards. 4.1
To simplify technicalities and avoid size problems, we will assume all our categories to be small, and use terms set and class interchangeably. 4.1.1 Objects and arrows. If C is a category, C denotes its class of objects, and for A; B2C , C (A; B) is the set of morphisms/arrows from A to B. Also, C (A; ) is SB2C C (A; B), and dually, C ( ; B) is SA2C C (A; B), Let then C be the class of all arrows denoted by the same letter as the entire category (i.e., writing u2C means that u is an arrow, while objects are elements of C ). If u: A ! B, we write u for A and u for B. We write u: A ! and u: ! B for elements of C (A; ) and C ( ; B) resp. Sequential composition of u: A ! B, v: B ! C is denoted by u; v, and the identity of object A is idA. If prop is a property of C -arrows, the class fu2C : u j= propg is denoted by C prop, which gives us three subcategories C iso; C epi; C mono. Isomorphic objects are denoted by A = B, and let A= denote A's iso-closure fB2C : B = Ag. If C 0 is a subcategory of C with the same class of objects, i.e., C 0 C but C 0 = C , we write C 0 C and say C 0 is an object-full subcategory of C .
Given a functor (indexed category) f : C ! Cat and an object A2C , we write f A for (f A) . Thus, f A is a category while f A is its class of objects. For two parallel functors f 0; f : C ! Cat, we say f 0 is an objectfull subfunctor of f and write f 0 f if f 0A f A for all A2C and, for any u: A B in C , reindexing f 0u: f 0A ! f 0B is the restriction of reindexing f u: f A ! f B to f 0A. 4.1.2 Families, spans and products. Given a set X, a family of its elements is denoted by expression x = ffxi2X: i 2 Igg with double brackets, while the set of elements participating in the family is denoted by expression x# = fxi2X: i 2 Ig with single brackets; we will refer to this set as to the member set of the family. Even if the family at hand is injective, i.e., xi 6= xj for i 6= j, and hence x is a bijection x: I ! x#, we still denote the family with double brackets. Any subset Y X of the carrier set gives rise to a family ffxy2X: y 2 Y gg with xy = y for all y2Y .
A span in a category C is a family of arrows u = ffui: H ! 2 M : i 2 Iugg with a common source called the head of the span and denoted by u; the arrows are called legs, and their targets are feet of the spans. The family of feet is denoted by u = ffui : i2Iugg (note that it may be non-injective family if even the family of legs is injective). Given a set J and a function f : J ! Iu, reindexing of u along f is the span ffufj : j2J gg denoted by f u.
Given a family of C -objects A = ffAi2C : i 2 Igg, its (chosen) product is a span A = ff iA2C ( A; Ai): i 2 Igg, whose head is denoted by A, and legs iA are called projections (note that the product span uses the same indexing set I). We will follow a common practice and denote the head of the product span and the entire span by the same letter , but sometimes we will use for the head if we want to emphasize that we are talking about an object. Products are called idempotent, if for any family of isomorphic objects A = ffAi2C : i 2 Igg with Ai = Aj for any two i; j 2 I, all projections iA are isomorphisms. Given a span u, universality of products means a uniquely determined arrow u!: u ! (u ) commuting with projections (i.e., a span morphism). Speci cally, any function f : J ! Iu gives rise to a unique span morphism f !: u ! (f u).
A functor f : C ! D between categories maps any span u to a span f u = fff (ui): i2Iugg. Functor f is said to preserve products (up to iso) if for any family of C -objects A=ffAi: i 2 Igg, we have f ( A) = (f A) (or just f ( A) = (f A)). 4.1.3 Triangle functors. We will heavily use the following simple construction.
Given an object A2C , symbol T A denotes a triangle category, whose objects are arrows u: A ! , and arrows are triples (u; u0; b) with u; u0 2 C (A; ) and b: u ! u0 . Such a triple can be seen as a triangle with vertexes A (called the main vertex, u , u0 , sides u and u0, and the base b; we will call them triangles and denote by double arrows b: u ) u0 with the subscript referring to the base. Thus, T A (u; u0) = C (u; u0) where we write T A for (T A) , and T A (u; u0) = C (u ; u0 ). Note that we cannot assume equality T A (u; u0) = C (u ; u0 ) because two triangles from di erent triangle categories, say, (u; u0; b)2T A and (v; v0; b)2T B, can share the same base b. To make this explicit, we will sometimes write triangles as quadruples (A; u; u0; b) with the rst component being the main vertex, or via arrows as bA : u )4 u0. Triangle composition is given by tiling: for b: u ) u0 and b0 : u0 ) u00, we have b;b0 : u ) u00. The identity idu: u ) u is the triangle with base idu . The subcategory of commutative triangles is denoted by T [=]A, and it is nothing but the slice category AnC .
Any arrow f : A B gives rise to a reindexing functor f : T A ! T B in an obvious way: an arrow u: A ! is mapped to f u d=ef f ; u: B ! , and triangle bA : u )4 u0is mapped to triangle cB : f u )4 f u0 with the same base b. We will call this construction reindexing by precomposition. 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 explicit.
Given an object-full subcategory C 0 C , for each object A we have an arrow subcategory T C0A T CA = TA whose triangle bases are taken from C 0, i.e., T C0A arrows are triples (u; v; b0) with u; v 2 C (A; ) and b02C 0(u ; v ).2 As C 0 is a subcategory of C , triangle tiling and identities are inherited from T A. Reindexing along f 2C (A; B) is obviously a functor f : T C0A T C0B, and we thus have an indexed category T C0 : C ! Catop such that T C0 T .
Finally, any functor f : C ! D gives rise to a natural transformation T f : T C ) f ; T D with a family of functors T fA: T C (A) ! T D (f A), A2C de ned in an obvious way. We will write fAT for T fA to ease notation when T fA is applied to an argument. 4.2
De nition 1 (U-spaces) A space of uncertain models or just an u-space is a pair (M ; M 4) with M a category of (possibly uncertain) models and their updates (deltas), and M 4 M an object-full subcategory of M . Arrows of M 4 are called certainty non-decreasing updates, or (model) completions, or just 4-arrows, and we write c : A !4 B in order to say that c 2 M 4(A; B).
2Warning: a more accurate notation for T C0 would be T C0 C as T C0 could be understood as the triangle functor of category C 0 alone, whose triangles have all three sides taken from C 0, whereas we deal with the situation when only the triangle bases are C0-arrows. A similar concern appears later with reindexing, which is considered along any C -arrows, not just C 0-arrows. As we will never deal with the case of C 0 considered as an independent category knowing nothing about C , we can safely use the shorter notation.
A morphism from u-space (M ; M 4) to u-space (N ; N 4) is a functor f : M ! N that preserves 4-arrows: if c2M 4, then f (c)2N 4. Below are some motivational discussions and additional details.
Models and updates. A more accurate name for M 's arrows would be co-deltas, as we understand them as spans specifying the common part of the source and the target models rather than their di erence (for which the term delta typically used), but we will stick to the established bx terminology. We also call arrows updates as in our context the target model of an arrow is understood as an updated version of the source model, and the delta speci es the non-changed data common for both models.
Having isomorphism arrow i: A ! B in M means that models A and B are basically the same; in our main instantiation of the framework, isomorphic models are isomorphic attributed graphs that only di er in OIDs and null labels, and have the same values in all certain attribute slots.
Both models and updates are understood as possibly uncertain or incomplete as demonstrated by our examples above. More formally, objects can be optional (marked with question marks), and attribute values can be labeled nulls rather than actual values (in the database literature, actual values are often called constants). In addition, both models and updates include a set of logical formulas regulating possible completions of its uncertain elements. We will consider several examples below in Ex. 3 (see also [BDA+13]). Model completions. Subcategory M 4 encompasses very special updates. Intuitively, we assume that 4updates can do the following four types of changes: (i) narrow the possible value range for a null value (speci cally, make it a singleton, which means substituting a constant for the null); (ii) glue together two nulls into a null with a suitable value range; (iii) delete an optional OID; (iv) glue together two optional OIDs. Example 3 below shows these possibilities. Of course, updates that delete or glue together non-optional model elements are also possible, but such updates are not 4-arrows. Updates that add new elements to a model are not 4-arrows either. In this sense, our uncertainty semantics is of the CWA type (Closed World Assumption), while the OWA semantics (Open World Assumption) can be simulated by composing a 4-arrow with an insert update. Thus, assuming the CWA semantics means that 4-arrows are surjections, which we formalize by requiring them to be M -epimorphisms, i.e., we require M 4 M epi.
To formalize the intuition of 4-arrows as certainty non-decreasing , we impose two additional conditions. First, we require any isomorphism i: A ! B to be an 4-arrow: being isomorphic, both models should be equally (un)certain, hence, M iso M 4: Second, we require that having c : A !4 B and c0: A < B imply c2M iso and c02M iso (although mutual invertibility of c and c0 isn't required). Finally, we require that M = M 4 as any model can be the source or the target of a 4-arrow, e.g., the model's identity loop.
De nition 2 (full completions) If the only 4-arrows leaving model A are isomorphisms, M 4(A; ) = Msy misob(oAl;a)i,s wuesedcatllo Asug(gfuelslty)thceerttearimninoartcioonmopfletthee. cWome pdleetniootne ptrhoececslsasast ocfomalpllceotemmploedteelsm. oWdeelswbriyteMc :a A, w!h4erae to say that c 2M a , and call such an update c a (full) completion of A; let FC4(A) denotes the class of all such. We call model A consistent if FC4(A) 6= ?.
The following simple example illustrates the notions introduced above.
Example 3 Suppose given a metamodel that speci es a class R with two attributes a; b, whose values are positive integers. Suppose that for objects instantiating class R, both attributes are declared to be optional (in this sense R is a semi-structured relation, which can be instantiated with tuples having one or no components). Moreover, we assume that the metamodel can be instantiated with uncertain data, in which the existence of both objects and attribute slots can be optional, and attribute slots can hold nulls rather than actual values. We call such an instantiation an uncertain model, and Fig. 6 shows several simple examples.
Model A (the second left) consists of two objects r1; r2, both are assumed optional (note two ?-marks) and can be deleted in a legal completion. Attribute a of object r1 (we will write a@r1) is uncertain and represented by a labeled null ?1: in a legal completion, any value allowed by the metamodel (i.e., a positive integer in our case) can be substituted for ?1. (Thus, an attribute domain is the union Val [ Null where Val is the set of values for the attribute speci ed in the metamodel, and Null is a countable set of labeled nulls.) Attribute b@r1 is certain but optional: if it exists, its value is known and given, but the existence is not guaranteed. Object r2 is optional and has two mandatory but uncertain attributes. Model A0 (the leftmost) is an isomorphic copy of A: its OIDs and labeled nulls are in bijective correspondence with OIDs and nulls of model A, whereas the real value 3 is kept. In practice, models are normally considered up to their isomorphism, and below we will freely rename OIDs and nulls without mentioning.
R q1? q2? a + b ?1 ?2 5; b b 3 3 5 10
4 %& a ?1 5; b R q1 q2? a a + b a + b 5; b a + b a + b b 3
5 10 5
Models B can be seen as a completion of A, in which the existence of object r1 and its attribute b became certain, and null ?3@r2 was substituted by value 3 (ignore the empty bottom compartment of the moment). However, the above understanding of the update silently assumes that object ri was updated to object gure for a qi for i = 1; 2. This update delta is denoted by the two-parallel-arrows symbol with superscript 4. However, it is also possible to consider an update from A to B as updating r1 to q2 and r2 to q1 (which is denoted by the crossed-arrows symbol), which changes the meaning of the update: now object q2 is just r1 with optional value 3 promoted to really existing in B, whereas object q1 is certainly existing r2, in which, additionally, the null value at the b-slot is completed with value 3. Note also that while the logical part of model A is empty (any positive integer can be substituted for nulls), model B has constraints that lessens the set of possible completions. Hence, both deltas are 4-arrows indeed (but the superindex 4 near the crossed-arrows delta is omitted). Thus, we have two di erent completion arrows between the same models, and the provenance of objects and values in model B is di erent for these deltas. positions).
In the rest of the
gure we will continue to consider two deltas for the same pair of models: the parallel delta (which maps objects in parallel: upper to upper and lower to lower), and the crossed one (which swaps the object
The parallel delta from B to C does nothing with the structure, but there is a change in the logical part: formula a + b
10 was added to the model. Syntactically, this change is an update, moreover, a completion as we added a new restriction to possible completions. However, as the new constraint can be inferred from the previous constraints, nothing was changed semantically. That is, although models B and C are syntactically di erent (and the parallel update is not an isomorphisms), semantically they are same, i.e., they have the same set of completions. Later we will formally explain such cases.
Now consider the cross delta from B to C. It speci es a general update rather than completion, because it changes a mandatory object q1 to an optional one, thus increasing uncertainty of the model. On the other hand, the part of uncertainty related to object q2@B is decreased as this object became certain in C. Thus, the sets of full completions of B and C intersect via composing C-completions with the delta, but neither is a subset of the other. That is, B-completions in which object q2 is deleted are not achievable from C, and C-completions in which r2 is deleted are not achievable from B (later we will consider in detail how C-completions are mapped to B-completions via precomposition with deltas).
The parallel delta from C to D shows the only change in the structure: null ?2@r2 was replaced by null ?1@q2, but this change is not a trivial null renaming because null ?1 was already used in model C for attribute a@r1 and is kept in model D. In fact, having the same null in di erent slots is equivalent to declaring an equality constraint a@q1 = a@q2 for model D, which reduces the set of possible completions. The new constraint a+b 5 added to D also reduces the set of completions, and hence the parallel delta from C to D is a legal 4-arrow. Indeed, any completion of D can be transformed to a completion of C by precomposition with the delta, while model C evidently has more completions than D.
The meaning of the crossed delta from C to D is also clear, but it is again not a completion as it changed the status of object r1 from mandatory in C to optional in D, and thus increased uncertainty of the model. On the other hand, the cross delta decreases uncertainty by (a) resolving optionality of r2, and (b) equalizing two nulls. Hence, again, the sets of full completions of C and D \intersect" but neither is a subset of the other if the relation between C and D is speci ed by a cross delta.
Finally, model E is fully certain as the only allowed completions are renaming of the OID. The parallel delta can be seen as a full completion that substitutes value 2 for ?1@q1 and deletes q2. In contrast, the cross delta deletes non-optional object r1 (and hence is a general update rather than a completion), resolves optionality of q2 and substitutes 2 for ?1@q2. We can also consider yet another delta that glues objects q1 and q2 into one object r@E. This delta is a completion as it decreases uncertainty and any completion of E (only renaming of r are allowed) is mapped to a completion of D.
Examples above show that the comparative certainty of two models can only be considered a binary relation if there is a prede ned way to relate models and compute the delta between them based on some information contained in the models, e.g., using some unique keys. If we do not have such keys (which is quite possible in MDE practice), certainty increasing or decreasing or non-comparability is a property of deltas relating the two models rather than pairs of models, and this is exactly the idea of u-spaces|designating a subcategory of arrows considered as certainty non-decreasing.
De nition 4 (Pre-well-behaved u-spaces) An u-space (M ; M 4) is called pre-well-behaved (pre-wb) if it satis es the four laws on the right.
The last one says that any model can be fully completed, i.e., seen as knowledge, is a consistent theory. (iso) M iso M 4 (preord) c : A !4 B and c0: A < B
imply c2M iso and c02M iso (epi) M 4 M epi (cons) for any A there is c : A !4 a
Given a model A, let FC4(A) = ffc : c2FC4(A)gg be the respective family of complete models (we recall that double gure brackets denote a family, i.e., a function from an indexing set ( FC4(A) in our case) to the carrier set (M ). The corresponding member set (FC4A)# is denoted by FC4#(A) = fc : c2FC4(A)g. If A is complete (fully certain), then FC4(A) consists of all isomorphic copies of A (perhaps repeated in the family). Lemma 1 (FC-properties) Any pre-wb u-space has the following properties> (i) iso-closure: B= FC4#(A) for any A2M and B2FC4#(A). (ii) iso-ignorance: A = B implies FC4(A) = FC4(B) and FC4#(A) = FC4#(B). iii) reindexing: Any c : A !4 B gives rise to injection c : FC4(A) - FC4(B) Proof. (i) and (ii) are direct consequences of the de nition. For (iii), we use pre-composition (see Sect. 4.1) that lifts any 4-arrow c : A !4 A0 to a function c : FC4(A) FC4(A0). The latter is injection due to (epi). tu
Thus, 4-arrows indeed do not decrease certainty. However, even non-isomorphic completion can be nonincreasing either, e.g., recall the parallel delta from B to C in Ex. 3.
De nition 5 (semantic equivalence) A 4-arrow c : A !4 B is a semantic equivalence, if function c : FC4(A) - FC4(B) is bijective; then we write c : A ! B. 4.3
In the database literature, class FC4#(A) is usually called the semantics of incomplete model A and often denoted by [[ A ]]. As the example above shows, the class of completion arrows FC4(A) and the corresponding family FC4(A) are more important and actually necessary for an accurate formal semantics for updates (cf. the discussion of deltas in [DXC11]). Libkin's de nition of the informational preorder, A A0 i [[ A0 ]] [[ A ]], is subsumed by reindexing speci ed in Lemma 1(iii). In [Dis16], the relation between fair database domain (introduced by Libkin as the universe supporting naive query evaluation on incomplete databases) and u-spaces is discussed in more detail, and several results are proven.
The two major operations of the classical model theory are Mod and Th derived from satis ability relation j= between models and formulas both built over some given signature of operation and predicate symbols. Operator Mod maps a set of formulas, or a theory, , to its set of models Mod = fX2 Mod( ): X j= for all 2 g. Operator Th maps a class of models X to its theory ThX = f 2 ( ): X j= for all X2X g. Operator FC4 is a 4-arrow counterpart of Mod, but we also need a 4-arrow counterpart of Th. Uncertain models are themselves theories, and satis ability between a model A and a fully certain model C can be de ned via the existence of 4-arrow from A to C, i.e., C j= A i there is c : A !4 C. Then given a set of certain models C M a , its theory, i.e., model Th C, should be uncertain enough to encode all models in C and provide the inclusion C FC4(Th C).3 However, having in Th C enough uncertainty to encode C, we would not like to have it more than needed, and we require model ThC to be maximally certain amongst all models encoding C. In other words, for any model X with C FC4X, there should be a uniquely de ned completion arrow X! : X !4 Th C. Categorically, the last statement means that Th C is nothing but the product of class C, so that we can de ne Th C as C. It 3The exact equality rather than subsetting is desirable, but in general is not achievable as semantics is usually richer than logic, and we normally have C Mod Th C. Equality only holds for special classes of models called closed. is precisely the categorical reformulation of Libkin's consideration of theories as greatest lower bounds in the information pre-order [Lib15].
De nition 6 (well-behaved u-spaces: products) A pre-wb u-space (M ; M 4) is called well-behaved (wb) if category M 4 has products (denoted by 4). Products provide that for any model A, there is a model 4FC4(A) (understood as ThModA) and denoted by Aj=. Dually, for any family of certain models C = ffCi: i2ICgg, there is a family FC4( 4C) (understood as ModThC and) denoted by C . De nition 7 (closed and equivalent objects) Model A is closed if A! : A ! Aj= is an isomorphism in M , i.e., A and Aj= are isomorphic via A!. Two models are semantically equivalent, A1 A2, if Aj1= = Aj2=.
A family C is called closed if C! is a bijection, i.e., families C and C only di er in the choice of the indexing set but otherwise are the same.
Lemma 3 (certain objects and semantic closure) (i) If model A is certain, then A! : A ! Aj= is an isomorphism. (ii) If A1 A2 and both updates are certain, then A1=A2. (iii) If A1 A2 and A1 is certain, then A2 is certain as well. 4.4
Similarly to how model-based (a.k.a. state-based) updating can be ambiguous without deltas [DXC11], our examples above show that model completions are also ambiguous without deltas. But the latter can themselves be uncertain. (For example, if deltas are spans, their heads are ordinary models that can be uncertain.) Hence, our next goal is to extend the notion of u-space with uncertain updates.
For an u-space (M ; M 4), the triangle functor T M 4 generated by subcategory M 4 (Sect. 4.1.3) will be denoted by T4.
De nition 8 (uu-spaces) A model space with uncertain models and uncertain updates, or uu-space, is a triple M = (M ; M 4; T6) such that the pair (M ; M 4) is an u-space, and T6 is an object-full subfunctor of T4 (i.e., T6 T4 see Sect. 4.1) such that for any A2M , the pair (T4A; T6A) is an u-space too. Moreover, reindexing T f : T4A T4B along any update f 2M (A; B) is an u-space morphism.
In detail, for any object A2M , we have a category T6A, whose objects are updates, T6 A = M (A; ), and morphisms are some of triangles based on 4-arrows (see Sect. 4.1.3), i.e., any T6A morphism is a triangle (A; u; u0; b) whose base b is an M 4-arrow (but, in general, not all such triangles are T6A-arrows). We call T6A morphisms update completions, or certainty non-decreasing triangles, or just 6-arrows, and denote them by a double arrow cA : u )6 u0 with the base arrows denoted by c rather than b to recall that this arrow is a model completion (but the sides of the triangle are general updates, i.e., M -arrows). Normally, the superscript A will be omitted. Thus, T6A T4A T A for all A2M .
Note that all three functors share the same reindexing along M -arrows via precomposition. Requiring reindexing to be an u-space morphism means that for any update f : A B and update completion (A; u; u0; c), the triangle (B; f ; u; f ; u0; c) is an update completion as well. In other words, an arrow cA : u )6 u0 in category T6A is mapped to arrow cB : f ;u )6 f ;u0 in T6B.
called well-behaved (wb) if u-space (M ; M 4) and all u-spaces (T4A; T6A), A2M are wb, and, particularly, have products.
We recall that products in category M 4 are denoted by 4, and products in categories T6A will be denoted by A 6 with index A often omitted. In addition, all products 6 are required to be idempotent, and conditions in the inset table on the right must hold.
T [=] \ T4 T6 if cA : idA )6 (T6A)iso = T isoA \ T [=]A M `a M . if u2M 4 then FC6(u) if U T a \M 4 then then ( cA) = c
M 4 6U 2 M 4.
These conditions are explained below. (Comm) We require any commutative triangle based on a 4-arrow (i.e., a quadruple c = (A; u; u0; c) with c : u !4 u0 and u0 = u ; c) to be a 6-arrow c : u )6 u0. Indeed, commutativity means that update u0 is, essentially, u, but its target is a completion of u's target. However, although any commutative triangle is a completion, there can be non-commutative completion triangles as we have seen in Fig. 5. Hence, the formulation of the (Comm) law as above. (Id) Given model A2M , completions of the identity update are nothing but completions of A (and all completion triangles are commutative). (Iso) To de ne full update completions, i.e., to apply the general u-space Def. 2 to updates-as-objects, we need to discuss update isomorphisms in categories T6A. It is easy to see that any commutative triangle (A; u; u; i; i) based on isomorphism i : u != u0 is an isomorphism in T6A. We require the converse to be true as well, which provides the law (Iso) (in which T iso denotes T M iso ).
Now we repeat the general de nition for updates as objects. If the only 6-triangles from update u: A ! are ictlsasissoomf oarllpshuiscmhsi,nTt6hAe (cua;te)go=ryTT66isAoA..(uW; e)w,trhiteen u: uis )ca6lleadt(ofuslalyy)tchearttain2orTcaoAm,palentde,caanlld leat fTulalAcodmepnloetteiosnthoef u.
Let FCA 6(u) or just FC6(u) denote the class of all such, and FC6(u) d=ef f : 2FC6(u)g is the respective set of complete updates (note a distinction from FC4, which was a family rather than a set). Thus, update u is complete i FC6(u) contains all isomorphic copies of u and nothing else. It is easy to see that if u is complete, then u is a complete model (otherwise, composition u; c for a non-trivial completion c: A ! would be a non-trivial completion of u). However, our examples in section 3 show that there can be non-complete updates, whose target is a complete model. (CertCert) Let M `a M denote the class of all (fully) certain models and certain updates between them: M `a = M a , and M `a (A; ) = T a (A; ) for A2M `a . Law (CertCert) states that composition of two certain updates is certain, i.e., the universe of certain models and updates is a subcategory, M `a M . (6 vs. 4) Finally, there are two laws regulating interaction between 4- and 6-arrows. The rst says that update completions of a model completion are themselves model completions. The second says that the update encoding a set of model completions is itself a model completion. tu
As categories T6A have idempotent products, we can introduce semantics closure uj= of an update u: A ! , and syntactic closure U of a class U of certain updates of A. The following is a rewrite of general u-space constructions on page 12 for u-spaces (T4A; T6A), A2M .
Lemma 4 (FC6-properties) Any wb uu-space has the following properties: (i) iso-closure: u0= FC6(u) for any u: A ! and u02FC6(u). (ii) iso-ignorance: u = v implies FC6(u) = FC6(v). (iii) reindexing: Any c : u )6 u0 gives rise to injection c : FC6(u) - FC6(u0) (iv) id-certainty: If model A is certain, then update idA is certain as well (in the u-space (T4A; T6A), A2M ). Proof. (i) and (ii) are direct consequences of the de nition. For (iii), we use pre-composition (see Sect. 4.1) that lifts any 6-arrow c : A !4 A0 to a function c : FC6(A) FC6(A0). The latter is injection due to law (epi). tu De nition 10 (semantic equivalence for updates) A completion triangle c : u )6 v is a semantic equivalence, if function c : FC6(u) - FC6(v) is bijective; then we write c : u ) v.
j=-closure operator Law name for any u2M there is unique u! : u ) uj= (unit) FC6( 6FC6(u)) = FC6(u) (idemp) c : u )6 u0 gives rise to cj= : uj= )6 u0j= (monot) U
U
U 6FC6( -closure operator for any U
6U ) = U 0 implies U
T a 6U
U 0 De nition 11 (closed and equivalent objects) Update u is called closed if u! : u ) in T6A, i.e., u and uj= are isomorphic via u!. Two update are semantically equivalent, u1 class U of updates is closed if U ! is a bijection. Two classes are logically equivalent, U1 uj= is an isomorphism
u2, if uj1= = uj2=. A U2, if U1 = U2 .
Lemma 6 (certain objects and semantic closure) (i) If update u is certain, then u! : u ! uj= is an isomorphism. (ii) If u1 u2 and both updates are certain, then u1=u2. (iii) If u1 u2 and u1 is certain, then u2 is certain as well.
Morphisms of uu-spaces are nothing but view functors compatible with uu-structure De nition 12 (uu-space morphisms or views) Let M = (M ; M 4; T6) and N = (N ; N 4; U6) be two wb uuspaces (i.e., U6 is an object-full subfunctor of the triangle functor U4 generated by subcategory N 4as explained in Sect. 4.1.3). A well-behaved (wb) view M ! N is a surjective on objects and full functor get: M ! N compatible with the uu-structure in the following way.
a) Model completions are preserved, i.e., the restriction of get to M 4 is a functor get4: M 4 ! N 4. a') Moreover, we require get4 to be full.
b) Update completions are preserved, i.e., for any A2M , the restriction of triangle functor getTA (see Sect. 4.1.3) to T6A is a functor getA 6: T6A ! U6B (where B stands for getA).
b') Moreover, we require all functors getA 6 to be full.
c) Product preservation: Functor get preserves 4-products, and all functors getA 6 (for A2M ) preserve 6-products.
We de ne uu-space morphisms to be wb views, and denote them by arrows get: M ! N . tu In the lens framework, functor get is normally considered together with put, and the latter provides fullness conditions. However, views are themselves interesting (e.g., for databases), and we would like to state the next result independently of put.
Lemma 7 (wb view properties) (i) A wb view get: M ! N maps certain models and certain updates in space M to certain models and certain updates in N . Thus, there is a functor get `a : M `a ! N `a . (ii) For any model A2M and update u2FCA6 (idA), there is getu = idgetA (iii) For any update u: A ! , equation getA(uj=) = (getAu)j= holds. 4.5
First, we recall the notion of an ordinary (delta) lens.
De nition 13 (delta lenses) Let M , N be two categories considered as model spaces.
(i) A lens from M to N is a pair ` = (get; put) with get: M ! N a functor, and put = ffputA: A2M gg a family of functions putA: M (A; ) N (getA; ) indexed by M -objects. We will often write putAv for putA(v), and putAv for (putAv) .
(ii) A lens is called well-behaved (wb) if the following two conditions (laws) are satis ed for all A2M (below B stands for getA): Identity preservation: putA(idB) = idA.
PutGet law: get(putAv) = v for all updates v: B ! .
Note that the de nition does not require putA to map a triangle of updates on the view side, v: B ! B0, v0: B0 ! B00, and v00: B ! B00, to a triangle on the source side, i.e., the case when putAv00 6= putA0 v0 with A0 standing for putAv is not prohibited (and actually appears in practice, see [DXC11] for an example).
(iii) A wb lens is called very well-behaved (vwb) if the put-image of any commutative triangle of view updates is mapped to a commutative triangle on the source side.
PutPut law: putA(v; v0) = (putAv); (putA0 v0) where A0 = putAv. (Note that mapping of an arbitrary triangle to a triangle is still not required, but commutative triangles are mapped to triangles (which are also commutative).
The de nition above is equivalent to the delta lens de nition in [DXC11] with a minor distinction that in [DXC11], functoriality of get is attributed to the very wb rather than wb lenses.
The ordinary lenses are based on very strict update (propagation) policies: for a given view update v: getA ! , in the entire set get 1(v) M (A; ) of updates satisfying the Putget law, only one is chosen. The following two constructs relax this requirement. The rst one, update policies, do it in a direct semantic way with the notion of a multi-valued operation. The second one, uu-lenses, do it indirectly by encoding a multitude of models by a suitable uncertain model.
De nition 14 (update policies) Let M = (M ; M 4; T6) and N = (N ; N 4; U6) be two uu-spaces (i.e., spaces of uncertain models and uncertain updates with U the triangle functor for N ), and get: M ! N be a wb view as described in Def. 12.
(i) A (multi-valued) update policy for get is a family Put of set-valued functions ffPutA: 2T aA U a B: A 2 M ; B = getAgg indexed by M -objects (note that both the input and the output deal with certain updates). We will often write PutAv for PutA(v), and PutAv for fu : u2PutAvg.
(ii) A policy is called well-behaved (wb) if the following conditions are satis ed for all A2M and v2N (B; ) (where B stands for getA. and update isomorphisms are considered in the respective triangle categories U6B and T6A): o) PutGet law (up to iso): getu = v for any u 2 PutAv. In other words, PutA(v) get 1(v=). a) 4-preservation: if v2N 4, then PutAv M 4 b1) Iso-closedness: if u2PutAv, then u= PutAv b2) Iso-ignorance: If v = v0, then PutAv = PutAv0. c) Identity: if v = idB, then PutAv = FC6(idA) (Note that Lemma 7(ii) ensures that the speci c policy c) for identities satis es the general Putget law o).)
(iii) Given two policies for the same view get, Put and Put0, we say that Put is not more certain than Put0 and write Put v Put0, if PutAv Put0Av for all A and all v: getA ! . This gives us a posetal category Polget. De nition 15 (uu-lenses) Let M = (M ; M 4; T6) and N = (N ; N 4; U6) be two uu-spaces as above.
(i) An (asymmetric) uu-lens (read a lens with uncertainty) from M to N is a delta lens ` = (get; put) : M N between the carrier categories as de ned above in Def. 13(i).
(ii) An uu-lens is called (almost) well-behaved (wb) if it is compatible with the uu-structure as follows. (uu-get) Functor get is a wb view (uu-space morphism) as de ned in Def. 12 (uu-put) Family put must satisfy the following set of conditions to hold for any A2M and v: B ! (B is getA): o) A version of Putget law called uu-Putget: get(putAv) = vj= for any v: B ! . a) if v2N 4 then putAv2M 4, i.e., model completions are preserved; b1) for any completion triangle on the view side, (B; v; v0; c), its put-image (A; putAv; putAv0; putA0 c) (where A0 = putAv ) is a completion triangle on the source side.
In other words, we require an U6B-arrow cB : v )6 v0 on the view side to be mapped to an T6A-arrow pAutA0 c : putAv )6 putAv0 on the source side. This allows us to de ne a mapping putA6: T6A U6B, and we will often omit the subindex 6 (but note that we do not require from put to map general triangles based on U4-arrows on the N -side to triangles on the M-side).
b2) All mappings putA: T6A U6B must preserve composition of update completions (i.e., tiling). c) if v = idB, then putAv = idjA=, i.e., identities are preserved up to semantic equivalence.
As for a general update v, v is not isomorphic to vj=, we cannot say that uu-lens satisfying the laws above is absolutely well-behaved. However, as v = vj= for certain updates by Lemma 6(i), and idA is certain for a certain model A by Lemma 4(iv), uu-Putget and identity preservation up to j= do provide isomorphism get(putAv) = v for certain v and putA(idB) = idA for certain A. We thus may say that the lens satisfying the laws above is almost wb, and, as a rule, we will omit the adjective 'almost'.
We will denote an uu-lens by a double arrow ` : M
N , and say lens ` = (get; put) is de ned over the view get.
De nition 16 (arrows between uu-lenses) Let ` = (get; put) and `0 = (get; put0) be two wb uu-lenses over the same view get: M ! N . A completion arrow from ` to `0 is a family of product preserving natural transformations A: putA ) put0A (read tau-to-tau) indexed by A2M . That is, for any A and update v: getA ! , we have an update completion (i.e., a triangle) A(v) : putAv )6 put0Av, and naturality means that for any completion : v )6 v0, we have a commutative square: A(v) ; put0A( ) = putA( ) ; A(v0).
This gives us a category Lensget of all wb u-lenses and their completion arrows over a given view get: M ! N . Theorem 8 (from lenses to policies and back) Let get: M ! N be a wb view between wb uu-model spaces. Then
(i) Any wb uu-lens ` = (get; put) : M N over get gives rise to a wb update policy Put` for get. We will say that policy Put` is implicit in `. Moreover, this correspondence extends to a functor polget: Lensget ! Polget.
(ii) Any wb update policy Put for get gives rise to a wb uu-lens `Put = (get; put) over get. We will say that the lens `Put is based on Put. Moreover, this correspondence extends to a functor lensget: Polget ! Lensget.
(iii) Functors above are adjoint: polget a lensget.
The unit of the adjunction is given by the family of update completions u!A;v : uA;v ) ujA=;v = uA;v, where uA;v = putAv and uA;v = putA v with put = lensget(polget(put)) being the lens based on the policy implicit in ` = (get; put) 2 Lensget. The counit of the adjunction is given by the family of inclusions iA;v: UA;v = UA;v UA;v where UA;v = PutAv and UA;v = PutA;v with Put = polget(lensget(Put)) being the policy implicit in the lens based on the policy Put2Polget.
Thus, multi-valued update policies and single-valued lenses with uncertainty are basically equivalent up to \semantic" closure x 7! xj= on one side, and \syntactic closure" x 7! x on the other side. 5
Uncertainty is one of the main problems in software engineering, which typically occurs when the designer does not have the complete, consistent and accurate information required to make a decision during software development. Uncertainty management has been studied in many works, often with the intention to express and represent it in models. In [FSC12, SCHS13], the notion of partial model is introduced to let the designer specify uncertain information by suitable annotations of the model. The machinery (called MAVO) is essentially based on FOL and can be seen as a speci c instantiation of (some of the ) constructs developed in our paper. Some categorical elements were introduced into the MAVO modeling in [SC15], but the latter is still based on FOL syntactically and semantically. A comparison with Libkin's work on uncertainty modeling [Lib14b, Lib14a, Lib15] is discussed above in Sect. 4, see also [Dis16] for more details. Understanding incomplete objects as theories (metamodels), which encode objects' possible completions, was proposed in [BDA+13]. The leading role of the notion of models spaces for the lens framework was emphasized and discussed by Johnson and Rosebrugh in several of their papers and talks [JR16, JR13].
Uncertainty in bidirectional transformations has been often discussed as non-determinism. On the practical side, novel declarative approaches to bidirectionality have been recently proposed for dealing with nondeterministic transformations. Among them, the Janus Transformation Language (JTL) [EMM+10, CDREP10] is a constraint-based model transformation language speci cally tailored to support bidirectionality and change propagation. Its relational semantics is able to generate a multitude of models as a solution of a non-deterministic transformation. In [RE15], the JTL engine is revised to accommodate the new intensional semantics. This permits a transformation to natively generate a model with uncertainty instead of a myriad of models. In [BHLW07], the authors propose PROGRES, a bx solution based on TGG, which is able to recognize ambiguous mappings and resolve them by interacting with the user, who needs to be an experts in these techniques. An attempt in making bidirectional transformation deterministic by means of intentional updates is represented by the BiFluX language [ZPH14]; however, as a transformation cannot be tested for non-determinism at static-time, the e ectiveness of the approach is reduced. In [MC13] a bidirectional transformation approach is proposed, in which the QVT-R semantics is implemented by means of Alloy. Di erent generated alternatives are obtained from the execution of a model transformation and reduced by either adding extra OCL constraints or by limiting the upper-bound search criteria. 6
Most of the current bx tools and frameworks (including lenses) typically require the transformation writer to consider only one particular consistency restoration strategy among many possible alternatives. Hence, the developers have little or no control over the inherent uncertainty of update propagation. In this paper, we propose an approach to the problem by enriching the delta lens framework with an uncertainty mechanism, which allows managing underspeci cation and incompleteness within the usual algebra of single-valued operations. Our future plans include the possibility of representing uncertainty in a practically handy way, and assist the modeler with appropriate visualization and tools. For instance, the set of consistency-restoring updates may be encoded by a single feature model, which is convenient for the user to gradually resolve the underspeci cation later. The formal framework of delta-lenses with uncertainty opens several interesting directions for mathematical modeling of uncertainty. Speci cally, update completions make the lens framework essentially bicategorical. Employing the bicategorical conceptual framework and machinery should make the naive (and somewhat bulky and di use) formal framework presented in the paper better structured and clearer.
Acknowledgement. We are grateful to BX'16 reviewers for careful reviewing and numerous comments on improving the presentation. Thanks go to Harald Koenig for reading and commenting on some parts of the formal section. Special thanks are for the PC Chairs for their patience in softening several hard deadlines. Financial support for the Canadian part of the author team was provided by Automotive Partnership Canada via the Network on Engineering Complex Software Intensive Systems (NECSIS). [BDA+13] [FSC12] [JR13]
Michalis Famelis, Rick Salay, and Marsha Chechik. Partial models: Towards modeling and reasoning with uncertainty. In ICSE, pages 573{583, 2012.
Michael Johnson and Robert D. Rosebrugh. Delta lenses and op brations. ECEASST, 57, 2013. Michael Johnson and Robert D. Rosebrugh. Unifying set-based, delta-based and edit-based lenses. In Proceedings BX'16, 2016. To appear.
Leonid Libkin. Certain answers as objects and knowledge. In Chitta Baral, Giuseppe De Giacomo, and Thomas Eiter, editors, Procs of KR 2014. AAAI Press, 2014.
Leonid Libkin. Incomplete data: what went wrong, and how to x it. In Richard Hull and Martin Grohe, editors, Procs of PODS'14, pages 1{13. ACM, 2014.
Leonid Libkin. How to de ne certain answers. In Qiang Yang and Michael Wooldridge, editors, Procs of IJCAI 2015, pages 4282{4288. AAAI Press, 2015.
Nuno Macedo and Alcino Cunha. Implementing QVT-R Bidirectional Model Transformations Using Alloy. In FASE, volume 7793, pages 297{311, 2013.
Gianni Rosa Romina Eramo, Alfonso Pierantonio. Managing uncertainty in bidirectional model transformations. In SLE 2015, 2015.