=Paper=
{{Paper
|id=Vol-1571/paper_9
|storemode=property
|title=Incorporating Uncertainty into Bidirectional Model Transformations and their Delta-Lens Formalization
|pdfUrl=https://ceur-ws.org/Vol-1571/paper_9.pdf
|volume=Vol-1571
|dblpUrl=https://dblp.org/rec/conf/etaps/DiskinEPC16
}}
==Incorporating Uncertainty into Bidirectional Model Transformations and their Delta-Lens Formalization==
https://ceur-ws.org/Vol-1571/paper_9.pdf
Incorporating Uncertainty into Bidirectional Model
Transformations and their Delta-Lens Formalization
Zinovy Diskin1,2 Romina Eramo3 Alfonso Pierantonio3 Krzysztof Czarnecki2
1 2
NECSIS, Generative Software Development Lab,
McMaster University, Canada University of Waterloo, Canada
diskinz@mcmaster.ca {zdiskin|kczarnec}@gsd.uwaterloo.ca
3
Dipartimento di Ingegneria e Scienze dell’Informazione e Matematica,
Università degli Studi dell’Aquila, Italy
{name.surname}@univaq.it
Abstract
In Model-Driven Engineering, bidirectional transformations are key to
managing consistency and synchronization of related models. Delta-
lenses are a flexible algebraic framework designed for specifying delta-
based synchronization operations. Since model consistency is usually
not a one-to-one correspondence, the synchronization process is inher-
ently ambiguous, and consistency restoration can be achieved in many
different ways. This can be seen as an uncertainty reducing process:
the unknown uncertainty at design-time is translated into known un-
certainty at run-time by generating multiple choices. However, many
current tools only focus on a specific strategy (an update policy) to se-
lect 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 consis-
tency restoration. This multitude is managed in an intentional manner
via models with built-in uncertainty.
1 Introduction
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 specified 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
Copyright c by the paper’s authors. Copying permitted for private and academic purposes.
In: A. Anjorin, J. Gibbons (eds.): Proceedings of the Fifth International Workshop on Bidirectional Transformations (Bx 2016),
Eindhoven, The Netherlands, April 8, 2016, published at http://ceur-ws.org
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 multi-
valued transformations modeled by multi-valued operations. However, multi-valued operations essentially com-
plicate the algebraic framework, and are not easy to manage technically. Our idea is different, and allows us
to manage uncertainty within the usual algebra of single-valued operations. We extend model spaces with in-
complete (uncertain) models, each of which determines a set of its full completions, which are ordinary complete
(fully-specified, certain) models. This allows us to model a multi-valued underspecified transformation by a
single-valued one, which results in an incomplete/uncertain model encoding the required set of ordinary com-
plete 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 Background and Motivation
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 Managing budget cuts is easy...
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
officer 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 VIEW DEFINITION MMF
MAPPING
Engineer Project Project
name: String pid: String pid: String
salary: Integer /budget: Integer budget: Integer
* workforce 1
/budget = ∑ {e.salary: e in p.workforce}
Figure 1: Metamodels and the view definition mapping.
Figure 1 depicts two metamodels developed by Ian to model Helen’s and Fred’s views of the project. The
metamodel M MH (in the left half of the figure) allows specifying Project objects with their pid (project identifier).
Each project is associated with a number of Engineers (with theirs name and salary) via association workforce.
The metamodel M MF (in the right half of the figure) represents Fred’s view of the projects, in which only budgets
are of interest. The forward transformation (get-the-view ) is defined as follows: given a project p, its budget is
computed by taking the sum of salaries of the engineers: p.budget = Σ {e.salary : e ∈ p.workforce}, and this
derived attribute/budget is taken to be the attribute budget in M MF . The view definition mapping defining
this view consists of three links shown in Fig. 1 by curved lines, while the entire mapping is shown as a block
arrow encompassing the links.
One of the company’s most promising projects is Perpetuum Mobile Engine (PME) identified by pid=PME, and
Fred was able to allocate a decent budget of 200 units monthly for PME. For this budget, Helen organized the
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 defined 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
B 0 ). 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 delta-
lenses 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
definition 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 ∆BB 0 in Fig. 2 consists of
three links, which say that the project q2 with its attributes in model B 0 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 B 0 are
different, we conclude that the attribute budget is updated in B 0 .
As models A and B 0 are in- A B
consistent (budgets are different), p1: Project w2:workforce fig.2
the delta lens invokes operation pid= PME
↔←→ /budget= 200 Delta ΔAB q1: Project
of backward update propagation L0: p1:Project ← q1:Project
w1:workforce L01: p1.pid ← q1.pid pid= PME
called put-update-back or just put). L02: p1.budget ← q1.budget budget= 200
e1: Engineer e2: Engineer
This operation (shown in Fig. 2 by name= Ben name= Bill
salary= 100 salary= 100
a chevron put, takes two deltas,
∆AB and ∆BB , together with
0
Delta ΔAA' Delta ΔBB'
their source and target models, L0: p1:Project → p2:Project L0: q1:Project → q2:Project
L1: e1:Engineer → e3:Engineer L01: q1.pid → q2.pid
and produces an update (vertical L02: q1.budget →q2.budget
L2: e2:Engineer → e4:Engineer
:put
delta) ∆AA (only links between
0
A’ B’
OIDs are shown to save space, p2: Project
w4:workforce
the attribute links can be restored pid= PME
/budget= 150 q2: Project
from them) together with an up- w3:workforce Delta ΔA'B'
L0: p2:Project ← q2:Project pid= PME
dated correspondence. Given e3: Engineer e4: Engineer L01: p2.pid ← q2.pid budget= 150
models and deltas are shaded, L02: p2.budget ← q2.budget
name= Ben name= Bill
salary= 75 salary= 75
while the derived model and two
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 re-
store 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 flexible. 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 predefined 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 final completions,
i.e., models with fixed values for the attribute salary, e.g., 70 for Ben, and 80 for Bill. In-between, there are
many completions that are not-final, 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 difficult to manage.
Being very satisfied 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
/budget= 200
files, Helen found that as ↔←→both
w1:workforce
Ben and Bill are senior and ex- fig.3
e1: Engineer e2: Engineer
perienced engineers, reduction of
name= Ben name= Bill
their salary is not a good solu- salary= 100 salary= 100
tion at all. A Helen’s new idea
was to keep one of the engineers Delta ΔAA'1 Delta ΔAA'2
L0: p1:Project → p2:Project L0: p1:Project → p2:Project
with the same or even increased L1: e1:Engineer → e3:Engineer L1: e1:Engineer → e3:Engineer ?
salary, and hire a recent gradu- L2: e2:Engineer → e4:Engineer L2: e2:Engineer → e4:Engineer ?
|= L1 XOR L2
ate as his assistant for a smaller
salary. Again, to keep this ap- A’1 A’2
p2: Project p2: Project
proach flexible, salaries should not w4:workforce w4:workforce
pid= PME pid= PME
be be fixed but rather kept within /budget= 150 /budget= 150
some predefined ranges. When w3:workforce w3:workforce
Ian asked which of the engineers, e3: Engineer e3: Engineer
e4: Engineer e4: Engineer
Ben or Bill, Helen intends to keep, name= Ben name= Bill name= Ben + String name= Bill + String
she answered that she would de- salary= [65..85] salary= [65..85] salary= [100..110] salary= [100..110]
or [40..50] or [40..50]
cide this later.
C1: e3.salary + e4.salary <= 150
After some thinking, Ian im- C1: e3.salary + e4.salary <= 150
plemented a new lens satisfying
Helen’s new approach: this lens
Figure 3: The incomplete models A01 and A02
should produce an incomplete up-
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 specified in the logical
part of the delta labeled with |=, 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 specified but not shown in
the figure: 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 finished 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 Bx’s Underspecification via Delta-Lenses with Uncertainty
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 different: 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-specified models. This allows us to model a multi-valued underspecified
transformation by a single-valued operation, which results in an incomplete model encoding the required set of
1 In 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 configurations: {L1, L2}, {L1}, {L2},
and ∅. Then we simply mark optionality of each of the links without further constraints.
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-final completions of update ∆AA0 : A ← A0 : they are more
complete than it, but not all the choices are fixed.
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, 4AA0 A01 , 4AA01 A02 and 4AA02 A03 , whose tiling is
distorted in the lower part of the figure to fit 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.
Each of the triangles describes A B fig.4
p1: Project
a completion of its right-hand w2:workforce
pid= PME
side update to its left-hand side Delta ΔAB q1: Project
↔←→ /budget= 200
L0: p1:Project ← q1:Project
update, where an update is w1:workforce L01: p1.pid ← q1.pid pid= PME
L02: p1.budget ← q1.budget budget= 200
understood as a triple consist- e1: Engineer e2: Engineer
ing of the original model, the name= Ben name= Bill
salary= 100 salary= 100
updated model, and the delta
relating them. The right-most Delta ΔAA' Delta ΔBB'
L0: p1:Project → p2:Project L0: q1:Project → q2:Project
and the left-most triangles are L1: e1:Engineer → e3:Engineer ? L01: q1.pid → q2.pid
commutative: in each of them, L2: e2:Engineer → e4:Engineer ? L02: q1.budget →q2.budget
L1 OR L2 :put
the left delta is a composition
of the right delta with the base A’ B’
p2: Project
c-delta. The middle triangle is not w4:workforce
pid= PME
commutative: the composed link /budget= 150
Delta ΔA'B' q2: Project
w3:workforce
(e2→e4)∈∆AA0 ; (e4→e4)∈C∆A0 A0 L0: p2:Project ← q2:Project pid= PME
1 1 2 e3: Engineer ? e4: Engineer ? L01: p2.pid ← q2.pid budget= 150
is not included into ∆AA02 . We can L02: p2.budget ← q2.budget
name= Ben + String name= Bill + String
salary = [150] or salary = [150] or
understand this as first composing [100..110] or [100..110] or
two deltas ∆AA01 ; C∆A01 A02 , and [65..85] or [65..85] or
[40..50] [40..50]
then transforming the result by
the removal of the link specified
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 specifies a mapping
(relation), and a logical formula (marked with |=) 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
specification 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 specified by triangle AA0 A01 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
triangle fixes exact salaries and thus results in a (fully) complete update ∆AA03 : A ← A03 targeting at a (fully)
complete model A03 .
A
ΔAA’
[=] [=]
A’3 CΔA’2A’3 A’2 CΔA’1A’2 A’1 CΔA’A’1 A’
A
p1: Project w2:workforce
pid= PME
/budget= 200
Delta AA’2 w1:workforce AA’3
e1: Engineer e2: Engineer
Delta AA’1 name= Ben name= Bill
L0: p1:Project → p2:Project salary= 100 salary= 100
L1: e1:Engineer → e3:Engineer ?
L2: e2:Engineer → e4:Engineer ?
|= L1 XOR L2 Delta AA'
Delta AA’2
L0: p1:Project → p2:Project
L0: p1:Project → p2:Project
L1: e1:Engineer → e3:Engineer ? [=]
L1: e1:Engineer → e3: Engineer
[=] L2: e2:Engineer → e4:Engineer ?
|= L1 OR L2
A’1
w4:workforce
w3:workforce
p2: Project A’ p2: Project
pid= PME w3:workforce pid= PME w4:workforce
C-Delta A’A’1 /budget= 150
/budget= 150
L0: p2 <- p2
L1: e3 <- e3 |= e3 OR e4
e3: Engineer e4: Engineer L2: e4 <- e4
e3: Engineer ? e4: Engineer ?
name: Ben + String name: Bill + String
salary: [100..110] name= Ben + String name= Bill + String
salary: [100..110] salary = [150] or salary = [150] or
or [40..50] or [40..50] [100..110] or [100..110] or
[65..85] or [65..85] or
[40..50] [40..50]
C-Delta A’1A’2
L0: p2->p2
L1: e3->e3 Delta AA’3
L2: e4->e4 L0: p1:Project → p2:Project
L1: e1:Engineer → e3:Engineer
A’2 A’3
w1':workforce
w2':workforce
p2: Project p2: Project
w3:workforce
pid= PME pid= PME w4:workforce AA’3
AA’2 /budget=150
C-Delta A’2A’3 /budget= 150
L0: p2 -> p2
e3: Engineer e4: Engineer L1: e3 -> e3 C2
e3: Engineer e4: Engineer D
L2: e4 -> e4
name: Ben name: String name: Ben name: String
salary: [100..110] salary: [40..50] salary: 100 salary: 50
C1
D
Figure 5: A multi-valued model and its completions within the delta-lenses framework
4 Formal framework: Incorporating uncertainty into asymmetric delta-lenses
The first 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. Specifically, in a recent series of seminal papers [Lib14b, Lib14a, Lib15],
Leonid Libkin showed a major deficiency of a widely accepted common approach to uncertainty (the so called
certain answers), and proposed a simple elegant framework to fix the deficiency. 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 → ... → Aac ) with Ac0 = A and Aac being a fully certain model. Each model Ak in this chain
besides the last one (k = 0, 1, ...) can be a branching point of the completion process, which can go into another
0 0 0 0
direction (Ak = Ac0 → Ac1 → ... → Aac ) terminating at another fully certain model Aac , and so on. In general,
even small finite uncertain models can have an infinite number of completions exactly like small finite theories
can have an infinite 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 first 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 different 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 specification 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 sufficiently 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 find the most
economical presentation. Some unintended omisisons are, unfortunately, also possible: the formal section of the
paper was significantly 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 defintions 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 Categorical preliminaries and notation
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 S its class of objects, and for A, B∈C C •S
, C (A, B) is the
set of morphisms/arrows from A to B. Also, C (A, ∗) is B∈C C • C (A, B), and dually, C (∗, B) is A∈CC • C (A, B),
Let then C be the class of all arrows denoted by the same letter as the entire category (i.e., writing u∈C C 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
{u∈C C : u |= prop} 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 {B∈C C •: B ∼ 0
= A}. If C is a subcategory of C with the
0 0• • 0 0
same class of objects, i.e., C ⊂ C but C = C , we write C ⊆• C and say C is an object-full subcategory of C .
Given a functor (indexed category) f : C → Cat and an object A∈C C • , 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 object-
full subfunctor of f and write f 0 ⊆• f if f 0 A ⊆• f A for all A∈C C • and, for any u: A ← B in C , reindexing
f 0 u: f 0 A → f 0 B is the restriction of reindexing f u: f A → f B to f 0 A.
4.1.2 Families, spans and products. Given a set X, a family of its elements is denoted by expression
x = {{xi ∈X: i ∈ I}} with double brackets, while the set of elements participating in the family is denoted by
expression x# = {xi ∈X: i ∈ I} 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 {{xy ∈X: y ∈ Y }}
with xy = y for all y∈Y .
A span in a category C is a family of arrows u = {{ui : H → ∗ ∈ M : i ∈ Iu }} 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• = {{ui • : i∈Iu }} (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 {{uf j : j∈J}} denoted by
f ∗ u.
Given a family of C -objects A = {{Ai ∈C C • : i ∈ I}}, its (chosen) product is a span ΠA =
{{Πi A∈CC (• ΠA, Ai ): i ∈ I}}, whose head is denoted by • ΠA, and legs Πi A 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 isomor-
phic objects A = {{Ai ∈C C • : i ∈ I}} with Ai ∼= Aj for any two i, j ∈ I, all projections Πi A 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). Specifically, 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 = {{f (ui ): i∈Iu }}. Functor f is said to
preserve products (up to iso) if for any family of C -objects A={{Ai : i ∈ I}}, 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 A∈C C • , symbol T A denotes a triangle category, whose objects are arrows u: A → ∗, and arrows
•
are triples (u, u , b) with u, u0 ∈ C (A, ∗) and b: u• → u0 . Such a triple can be seen as a triangle with vertexes A
0
• 0• 0
(called the main vertex, u , u , sides u and u , 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 ) ∼
(T = C (u• , u0 ). Note that we cannot assume equality T A (u, u0 ) = C (u• , u0 ) because two
0 0
T A and (v, v , b)∈TT B, can share the same base b. To
triangles from different triangle categories, say, (u, u , b)∈T
make this explicit, we will sometimes write triangles as quadruples (A, u, u0 , b) with the first 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 A\C C.
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
def
mapped to f ∗ u = f ; u: B → ∗, and triangle τbA : u ⇒4 u0 is 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 C 0A ⊆• T CA =
T A whose triangle bases are taken from C 0 , i.e., T C 0A arrows are triples (u, v, b0 ) with u, v ∈ C (A, ∗) and
b0 ∈CC 0 (u• , v • ).2 As C 0 is a subcategory of C , triangle tiling and identities are inherited from T A. Reindexing
along f ∈C C (A, B) is obviously a functor f ∗ : T C 0A ← T C 0B, and we thus have an indexed category T C 0 : C → Catop
such that T C 0 ⊆• 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), A∈C C • defined in an obvious way. We will write fA T
for T fA to ease notation when T fA
is applied to an argument.
4.2 Model spaces with uncertainty, I: uncertain models and their completions
M , M 4 ) with M a category
Definition 1 (U-spaces) A space of uncertain models or just an u-space is a pair (M
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 ∈ M 4 (A, B).
2 Warning: a more accurate notation for T 0 would be T 0
C C ⊆• C as T C 0 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
C 0 -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 N , N 4 ) is a functor f : M → N that preserves 4-arrows: if
M , M 4 ) to u-space (N
M 4 , then f (c)∈N
c∈M N 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 difference (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 specifies 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 differ 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 4-
updates can do the following four types of changes: (i) narrow the possible value range for a null value (specifically,
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 isomor-
phic, 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 c∈M M iso and c0 ∈M
M 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.
Definition 2 (full completions) If the only 4-arrows leaving model A are isomorphisms, M 4 (A, ∗) =
M iso (A, ∗), we call A (fully) certain or complete. We denote the class of all complete models by M a• , where
symbol a is used to suggest the termination of the completion process at complete models. We write c : A →4 a
to say that c• ∈MM 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 specifies 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 specified 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.
A0 A B C D E
R a b R a b R a b R a b R a b R a b
q1? ⊥3 3? r1? ⊥1 3? ⇒4 q1 ⊥1 3 ⇒ 4 r1 ⊥1 3 ⇒4 q1 ⊥1 3 ⇒4 r 2 3
q2? ⊥1 ⊥2 ∼
= r2? ⊥2 ⊥3
% q2? ⊥2 3
& %
& r2 ? ⊥2 3 %
& q2? ⊥1 3 %
&
a ≤ 5, b ≤ 5 a ≤ 5, b ≤ 5 a ≤ 5, b ≤ 5 a ≤ 5, b ≤ 5
a + b ≤ 10 a + b ≤ 10 a + b ≤ 10
a+b≤5 a+b≤5
Figure 6: Model completions vs. model updates
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 figure for a
moment). However, the above understanding of the update silently assumes that object ri was updated to object
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 different completion arrows between the same models, and the provenance of objects and values in model B
is different for these deltas.
In the rest of the figure 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
positions).
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
different (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 specifies 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 different 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 specified 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 predefined 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.
(iso) M iso ⊆• M 4
Definition 4 (Pre-well-behaved u-spaces) An u-space (M M , M 4 ) is
(preord) c : A →4 B and c0: A <← B
called pre-well-behaved (pre-wb) if it satisfies the four laws on the right.
imply c∈MM iso and c0 ∈M
M iso
The last one says that any model can be fully completed, i.e., seen as
(epi) M 4 ⊆• M epi
knowledge, is a consistent theory.
(cons) for any A there is c : A →4 a
Given a model A, let FC•4 (A) = {{c• : c∈FC4 (A)}} be the respective family of complete models (we recall that
double figure brackets denote a family, i.e., a function from an indexing set ( FC4 (A) in our case) to the carrier
M • ). The corresponding member set (FC•4 A)# is denoted by FC•4# (A) = {c• : c∈FC4 (A)}. If A is complete
set (M
(fully certain), then FC•4 (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 = ⊂ FC•4 (A) for any A∈M M • and B∈FC•4# (A).
∼ B implies FC• (A) =
(ii) iso-ignorance: A = ∼ FC• (B) and FC• # (A) = FC• # (B).
4 4 4 4
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 definition. 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). t
u
Thus, 4-arrows indeed do not decrease certainty. However, even non-isomorphic completion can be non-
increasing either, e.g., recall the parallel delta from B to C in Ex. 3.
Definition 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 Logic for uncertainty
#
In the database literature, class FC•4 (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 FC•4 (A) are more important and actually necessary for an accurate formal semantics for updates (cf. the
discussion of deltas in [DXC11]). Libkin’s definition of the informational preorder, A A0 iff [[ A0 ]] ⊆ [[ A ]],
is subsumed by reindexing specified 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 satisfiability relation |=
between models and formulas both built over some given signature Σ of operation and predicate symbols. Oper-
ator Mod maps a set of formulas, or a theory, Φ, to its set of models ModΦ = {X∈ Mod(Σ): X |= φ for all φ∈Φ}.
Operator Th maps a class of models X to its theory ThX = {φ∈Φ(Σ): X |= φ for all X∈X }. 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 satisfiability between a model A and a fully certain model C can be defined via the existence of
4-arrow from A to C, i.e., C |= A iff 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 ⊂ FC4 X, there should be a uniquely defined 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 define Th C as Π• C. It
3 The 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].
Definition 6 (well-behaved u-spaces: products) A pre-wb u-space (M 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 • Π4 FC•4 (A)
(understood as ThModA) and denoted by A|= . Dually, for any family of certain models C = {{Ci : i∈IC }}, there
is a family FC•4 (• Π4 C) (understood as ModThC and) denoted by C . t
u
The following lemma (a straightforward consequence of the universality of products) shows that we indeed have
a version of the abstract model theory.
Lemma 2 (Galois correspondence for models)
|=-closure operator Law name -closure operator
•
for any A∈M M there is unique A! : A → A ≈ |=
(unit) for any C∈Fam(M M a• ) there is unique C! : C ,→ C
•
FC4 (Π4 FC4 (A)) = FC4 (A) • • ∼
(idemp) Π4 FC4 ( Π4 C) = Π4 C
c : A →4 B gives rise to c|= : A|= →4 B |= (monot) f : C → D gives rise to f : C → D
Definition 7 (closed and equivalent objects) Model A is closed if A! : A →≈ A|= is an isomorphism in M ,
|= |=
i.e., A and A|= are isomorphic via A!. Two models are semantically equivalent, A1 ≈ A2 , if A1 = A2 .
A family C is called closed if C! is a bijection, i.e., families C and C only differ 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 →≈ A|= is an iso-
morphism. (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 Model spaces with uncertainty, II: uncertain updates and their completions
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.
M , M 4 ), the triangle functor T M 4 generated by subcategory M 4 (Sect. 4.1.3) will be denoted
For an u-space (M
by T 4.
Definition 8 (uu-spaces) A model space with uncertain models and uncertain updates, or uu-space, is a triple
M = (M M , M 4 , T 6) such that the pair (M M , M 4 ) is an u-space, and T 6 is an object-full subfunctor of T 4 (i.e.,
T 6 ⊆• T 4 see Sect. 4.1) such that for any A∈M M • , the pair (T
T4A, T 6A) is an u-space too. Moreover, reindexing
T f : T 4A ← T 4B along any update f ∈M M (A, B) is an u-space morphism.
In detail, for any object A∈M M • , we have a category T 6A, whose objects are updates, T 6• A = M (A, ∗),
and morphisms are some of triangles based on 4-arrows (see Sect. 4.1.3), i.e., any T 6A morphism is a triangle
(A, u, u0 , b) whose base b is an M 4 -arrow (but, in general, not all such triangles are T 6A-arrows). We call T 6A
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, T 6A ⊆• T 4A ⊆• T A for all A∈M M •.
Note that all three functors share the same reindexing along M -arrows via precomposition. Requiring rein-
dexing 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
T 6A is mapped to arrow τcB : f ;u ⇒6 f ;u0 in T 6B.
Definition 9 (well-behaved uu-spaces) Uu-space is
(Comm) T [=] ∩ T 4 ⊂ T 6
M , M 4 ) and all u-spaces
called well-behaved (wb) if u-space (M •
(Id) if τcA : idA ⇒6 ∗ then (τcA ) = c
T4A, T 6A), A∈M
(T M • are wb, and, particularly, have products.
(Iso) T6A)iso = T iso A ∩ T [=] A
(T
We recall that products in category M 4 are denoted by Π4 ,
(CertCert) M `a ⊂ M .
and products in categories T 6A will be denoted by ΠA 6
(FC6 vs. 4) if u∈MM 4 then FC•6 (u) ⊂ M 4
with index A often omitted. In addition, all products Π6
(Π6 vs. 4) if U ⊂ T a• ∩M
M 4 then • Π6 U ∈ M 4 .
are required to be idempotent, and conditions in the inset
table on the right must hold. t
u
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.
•
M , completions of the identity update are nothing but completions of A (and all completion
(Id) Given model A∈M
triangles are commutative).
(Iso) To define 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 T 6A. It is easy to see that any commutative triangle (A, u, u; i, i)
∼ •
based on isomorphism i : u• →= u0 is an isomorphism in T 6A. 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 definition for updates as objects. If the only 6-triangles from update u: A → ∗ are
its isomorphisms, T 6A(u, ∗) = T 6iso A(u, ∗), then u is called (fully) certain or complete, and let T a• A denotes the
class of all such in the category T 6A.. We write τ : u ⇒6 a to say that τ • ∈ T a• A, and call τ a full completion of
u.
def
Let FCA 6 (u) or just FC6 (u) denote the class of all such, and FC•6 (u) = {τ • : τ ∈FC6 (u)} 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 iff FC•6 (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 . Law (CertCert) states that composition of two certain updates is
M a• , and M `a (A, ∗) = T a• (A, ∗) for A∈M
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 first 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. t
u
As categories T 6A have idempotent products, we can introduce semantics closure u|= 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
M •.
T4A, T6A), A∈M
constructions on page 12 for u-spaces (T
Lemma 4 (FC6 -properties) Any wb uu-space has the following properties:
∼
(i) iso-closure: u0= ⊂ FC•6 (u) for any u: A → ∗ and u0 ∈FC•6 (u).
(ii) iso-ignorance: u ∼
= v implies FC•6 (u) = FC•6 (v).
(iii) reindexing: Any τc : u ⇒6 u0 gives rise to injection τc∗ : FC6 (u) ←- FC6 (u0 )
M • ).
T4A, T 6A), A∈M
(iv) id-certainty: If model A is certain, then update idA is certain as well (in the u-space (T
Proof. (i) and (ii) are direct consequences of the definition. 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
Definition 10 (semantic equivalence for updates) A completion triangle τc : u ⇒6 v is a semantic equiva-
lence, if function τc∗ : FC6 (u) ←- FC6 (v) is bijective; then we write τc : u ⇒≈ v.
Lemma 5 (Galois correspondence for updates)
|=-closure operator Law name -closure operator
for any u∈MM there is unique u! : u ⇒≈ u|= (unit) U ⊂ U for any U ⊂ T a•
FC6 (• Π6 FC•6 (u)) = FC6 (u) (idemp) Π6 FC•6 (• Π6 U) ∼
= Π6 U
6 0 |= |= 6 0|=
τc : u ⇒ u gives rise to τc : u ⇒ u (monot) U ⊂ U 0 implies U ⊂ U 0
Definition 11 (closed and equivalent objects) Update u is called closed if u! : u ⇒≈ u|= is an isomorphism
|= |=
in T 6A, i.e., u and u|= are isomorphic via u!. Two update are semantically equivalent, u1 ≈ u2 , if u1 = u2 . A
class U of updates is closed if U! is a bijection. Two classes are logically equivalent, U1 ≈ U2 , if U1 = U2 .
Lemma 6 (certain objects and semantic closure) (i) If update u is certain, then u! : u →≈ u|= is an iso-
morphism. (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
Definition 12 (uu-space morphisms or views) Let M = (M M , M 4 , T 6) and N = (N
N , N 4 , U6) be two wb uu-
spaces (i.e., U6 is an object-full subfunctor of the triangle functor U4 generated by subcategory N 4 as 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 A∈M M • , the restriction of triangle functor getTA (see
Sect. 4.1.3) to T 6A is a functor getA 6 : T 6A → 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 A∈M M • ) preserve
6-products.
We define uu-space morphisms to be wb views, and denote them by arrows get: M → N . t
u
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 A∈M M • and update u∈FC A• ∼
6 (idA ), there is getu = idgetA
(iii) For any update u: A → ∗, equation getA (u|= ) ∼
= (getA u)|= holds.
4.5 Lenses over uu-spaces
First, we recall the notion of an ordinary (delta) lens.
Definition 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 = {{putA : A∈M M • }} a
family of functions putA : M (A, ∗) ← N (getA, ∗) indexed by M -objects. We will often write putA v for putA (v),
•
and put•A v for (putA v) .
(ii) A lens is called well-behaved (wb) if the following two conditions (laws) are satisfied for all A∈M M • (below
B stands for getA):
Identity preservation: putA (idB ) = idA .
PutGet law: get(putA v) = v for all updates v: B → ∗.
Note that the definition does not require putA to map a triangle of updates on the view side, v: B → B 0 ,
v 0 : B 0 → B 00 , and v 00 : B → B 00 , to a triangle on the source side, i.e., the case when put•A v 00 6= put•A0 v 0 with A0
standing for put•A v 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; v 0 ) = (putA v); (putA0 v 0 ) where A0 = put•A v. (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 definition above is equivalent to the delta lens definition in [DXC11] with a minor distinction that in
[DXC11], functoriality of get is attributed to the very wb rather than wb lenses. t
u
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 first 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.
Definition 14 (update policies) Let M = (M M , M 4 , T 6) and N = (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
•
{{PutA : 2T a A ← U a• B: A ∈ M • , B = getA}} indexed by M -objects (note that both the input and the out-
put deal with certain updates). We will often write PutA v for PutA (v), and Put•A v for {u• : u∈PutA v}.
(ii) A policy is called well-behaved (wb) if the following conditions are satisfied for all A∈M M • and v∈N
N (B, ∗)
(where B stands for getA. and update isomorphisms are considered in the respective triangle categories U6B
and T 6A):
∼
o) PutGet law (up to iso): getu ∼ = v for any u ∈ PutA v. In other words, PutA (v) ⊂ get−1 (v = ).
a) 4-preservation: if v∈N N 4 , then PutA v ⊂ M 4
∼
b1) Iso-closedness: if u∈PutA v, then u= ⊂ PutA v
b2) Iso-ignorance: If v ∼ = v 0 , then PutA v = PutA v 0 .
c) Identity: if v = idB , then PutA v = FC•6 (idA ) (Note that Lemma 7(ii) ensures that the specific policy c) for
identities satisfies 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 PutA v ⊇ Put0A v for all A and all v: getA → ∗. This gives us a posetal category Polget .
Definition 15 (uu-lenses) Let M = (M M , M 4 , T 6) and N = (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 defined 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 defined in Def. 12
(uu-put) Family put must satisfy the following set of conditions to hold for any A∈M M • and v: B → ∗ (B is getA):
|=
o) A version of Putget law called uu-Putget: get(putA v) = v for any v: B → ∗.
a) if v∈N N 4 then putA v∈M M 4 , i.e., model completions are preserved;
b1) for any completion triangle on the view side, (B, v, v 0 , c), its put-image (A, putA v, putA v 0 , putA0 c) (where
A0 = putA v • ) is a completion triangle on the source side.
In other words, we require an U6B-arrow τcB : v ⇒6 v 0 on the view side to be mapped to an T 6A-arrow
τputA0 c : putA v ⇒6 putA v 0 on the source side. This allows us to define a mapping putA6 : T 6A ← U6B, and we
A
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 : T 6A ← U6B must preserve composition of update completions (i.e., tiling).
|=
c) if v = idB , then putA v = idA , i.e., identities are preserved up to semantic equivalence.
As for a general update v, v is not isomorphic to v |= , we cannot say that uu-lens satisfying the laws above is
absolutely well-behaved. However, as v ∼ = v |= 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 |= do provide isomorphism get(putA v) ∼ =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 defined over the view get.
Definition 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 trans-
formations σA : putA ⇒ put0A (read tau-to-tau) indexed by A∈M M • . That is, for any A and update v: getA → ∗,
we have an update completion (i.e., a triangle) σA (v) : putA v ⇒6 put0 A v, and naturality means that for any
completion τ : v ⇒6 v 0 , we have a commutative square: σA (v) ; put0 A (τ ) = putA (τ ) ; σA (v 0 ).
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 pol get : 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 lens get : Polget → Lensget .
(iii) Functors above are adjoint: pol get a lens get .
|=
The unit of the adjunction is given by the family of update completions u!A,v : uA,v ⇒≈ uA,v = u∗∗ A,v , where
∗∗ ∗∗ ∗∗ pol get (put)) being the lens based on the policy implicit in
uA,v = putA v and uA,v = putA v with put = lens get (pol
` = (get, put) ∈ Lens•get . The counit of the adjunction is given by the family of inclusions iA,v : UA,v ∗∗
= UA,v ←-
UA,v where UA,v = PutA v and UA,v ∗∗
= Put∗∗
A,v with Put ∗∗
= pol get lens
(lens get (Put)) being the policy implicit in the
lens based on the policy Put∈Pol•get .
Thus, multi-valued update policies and single-valued lenses with uncertainty are basically equivalent up to
“semantic” closure x 7→ x|= on one side, and “syntactic closure” x 7→ x on the other side.
5 Related Work
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 specific 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 prac-
tical side, novel declarative approaches to bidirectionality have been recently proposed for dealing with non-
deterministic transformations. Among them, the Janus Transformation Language (JTL) [EMM+ 10, CDREP10]
is a constraint-based model transformation language specifically 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 per-
mits 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 effec-
tiveness 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. Different 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 Conclusion
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 underspecification 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 underspecification later. The
formal framework of delta-lenses with uncertainty opens several interesting directions for mathematical modeling
of uncertainty. Specifically, update completions make the lens framework essentially bicategorical. Employing
the bicategorical conceptual framework and machinery should make the naive (and somewhat bulky and diffuse)
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).
References
[BDA+ 13] Kacper Bak, Zinovy Diskin, Michal Antkiewicz, Krzysztof Czarnecki, and Andrzej Wasowski. Partial
instances via subclassing. In SLE13, pages 344–364, 2013.
[BHLW07] Simon M. Becker, Sebastian Herold, Sebastian Lohmann, and Bernhard Westfechtel. A graph-based
algorithm for consistency maintenance in incremental and interactive integration tools. Software
and System Modeling, 6(3):287–315, 2007.
[BS81] F. Bancilhon and N. Spyratos. Update semantics of relational views. ACM Trans. Database Syst.,
6(4):557–575, 1981.
[CDREP10] Antonio Cicchetti, Davide Di Ruscio, Romina Eramo, and Alfonso Pierantonio. JTL: a bidirectional
and change propagating transformation language. In SLE10, pages 183–202, 2010.
[Dis16] Zinovy Diskin. Asymmetric Delta-Lenses with Uncertainty: Towards a Formal Framework
for Flexible BX. Technical Report GSDLab-TR 2016-03-01, University of Waterloo, 2016.
http://gsd.uwaterloo.ca/node/660.
[DXC11] Zinovy Diskin, Yingfei Xiong, and Krzysztof Czarnecki. From State- to Delta-Based Bidirectional
Model Transformations: the Asymmetric Case. Journal of Object Technology, 10:6: 1–25, 2011.
[EMM+ 10] R. Eramo, I. Malavolta, H. Muccini, P. Pelliccione, and A. Pierantonio. A model-driven approach
to automate the propagation of changes among Architecture Description Languages. SOSYM,
1(25):1619–1366, 2010.
[FGM+ 07] J Nathan Foster, Michael B Greenwald, Jonathan T Moore, Benjamin C Pierce, and Alan Schmitt.
Combinators for bidirectional tree transformations: A linguistic approach to the view-update prob-
lem. ACM TOPLAS, 29(3):17, 2007.
[FSC12] Michalis Famelis, Rick Salay, and Marsha Chechik. Partial models: Towards modeling and reasoning
with uncertainty. In ICSE, pages 573–583, 2012.
[JR13] Michael Johnson and Robert D. Rosebrugh. Delta lenses and opfibrations. ECEASST, 57, 2013.
[JR16] Michael Johnson and Robert D. Rosebrugh. Unifying set-based, delta-based and edit-based lenses.
In Proceedings BX’16, 2016. To appear.
[Lib14a] 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.
[Lib14b] Leonid Libkin. Incomplete data: what went wrong, and how to fix it. In Richard Hull and Martin
Grohe, editors, Procs of PODS’14, pages 1–13. ACM, 2014.
[Lib15] Leonid Libkin. How to define certain answers. In Qiang Yang and Michael Wooldridge, editors,
Procs of IJCAI 2015, pages 4282–4288. AAAI Press, 2015.
[MC13] Nuno Macedo and Alcino Cunha. Implementing QVT-R Bidirectional Model Transformations Using
Alloy. In FASE, volume 7793, pages 297–311, 2013.
[RE15] Gianni Rosa Romina Eramo, Alfonso Pierantonio. Managing uncertainty in bidirectional model
transformations. In SLE 2015, 2015.
[SC15] Rick Salay and Marsha Chechik. A generalized formal framework for partial modeling. In FASE
2015, pages 133–148, 2015.
[SCHS13] Rick Salay, Marsha Chechik, Jennifer Horkoff, and Alessio Di Sandro. Managing requirements
uncertainty with partial models. Requir. Eng., 18(2):107–128, 2013.
[Ste09] Perdita Stevens. Bidirectional model transformations in QVT: semantic issues and open questions.
SOSYM, 8, 2009.
[ZPH14] Tao Zan, Hugo Pacheco, and Zhenjiang Hu. Writing bidirectional model transformations as inten-
tional updates. In ICSE Companion, pages 488–491, 2014.