Observations relating to the equivalences induced on model sets by bidirectional transformations Electronic Communications of the EASST Volume 49 (2012) Proceedings of the First International Workshop on Bidirectional Transformations (BX 2012) Observations relating to the equivalences induced on model sets by bidirectional transformations Perdita Stevens 16 pages Guest Editors: Frank Hermann, Janis Voigtländer Managing Editors: Tiziana Margaria, Julia Padberg, Gabriele Taentzer ECEASST Home Page: http://www.easst.org/eceasst/ ISSN 1863-2122 http://www.easst.org/eceasst/ ECEASST Observations relating to the equivalences induced on model sets by bidirectional transformations Perdita Stevens Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh Abstract: A bidirectional transformation on a pair of sets of models induces two principal equivalence relations on each set of models. Since a model can be uniquely identified by specifying its equivalence class in each of these relations, they function as a coordinate system for the model sets, with respect to the transformation. We prove some results relating to this observation. Using them we give the implication relationships between various properties of bidirectional transformations. In partic- ular, we characterise the bidirectional transformations that can be decomposed into a pair of lenses working “tail to tail”. Keywords: bidirectional transformation 1 Introduction The study of bidirectional transformations between model sets is, so far, hampered by lack of sufficiently deep understanding of the structures involved. This paper aims to be one step in the right direction. A recurring informal theme in work on bidirectional transformations is the idea of looking at different models “through glasses” which make them indistinguishable; for example, if we look at two correct implementations of the same abstract model through glasses which only care about what is relevant to the abstract model, they should not be distinguished. This idea is formalised using equivalence relations on the sets of models which are related by the transformation. This paper gives a collection of results concerning them, and goes on to exploit these to deduce (non-)implications between various “niceness” conditions on bidirectional transformations. We also give examples: an informal, MDD-realistic one, and some tiny, formal ones to illustrate points and serve as counter-examples to over-optimistic conjectures. The paper is structured as follows. In Section 2 we introduce notation and terminology, and give a our first couple of examples. Section 3 introduces the main focus of the paper, defining a pair of equivalence relations on each model set related by a bidirectional transformation, giving examples and basic properties. Section 4 exploits them to prove relationships between the various “niceness” conditions on bidirectional transformations, summarised in Figure 1. Especially, we show that a condition called simply matching, defined in terms of our equivalences, is achieved precisely when a bidirectional transformation can be re-expressed as a pair of lenses connected “tail to tail”. Section 5 discusses related work, and Section 6 concludes. 1 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations 2 Background Here we recapitulate definitions found for example in [Ste10]. For purposes of this paper a bidirectional transformation R : M ↔ N between non-empty sets M and N is given by specifying a consistency relation, also by slight abuse of notation called R ⊆ M×N, together a pair of functions −→ R : M×N → N ←− R : M×N → M whose task is to enforce consistency. We use the term “model” for the structures related by a bidirectional transformation because our motivation is from model-driven development, but this does not in fact entail any intention to restrict what the structures can be: throughout this paper, M and N can be any sets, finite or infinite, including uncountable. We will be concerned only with bidirectional transformations that only change a model when consistency requires it and, in that case, do enforce consistency: that is, those that are correct and hippocratic. Definition 1 R : M ↔ N is correct if ∀m ∈ M ∀n ∈ N R(m, −→ R (m, n)) ∀m ∈ M ∀n ∈ N R( ←− R (m, n), n) Definition 2 R : M ↔ N is hippocratic if for all m ∈ M and n ∈ N, we have R(m, n) ⇒ −→ R (m, n) = n R(m, n) ⇒ ←− R (m, n) = m From now on, all bidirectional transformations will be assumed to be correct and hippo- cratic. Please note also that many statements we shall make have exactly dual versions with dual proofs, replacing −→ R with ←− R etc. Generally we state both versions, but prove only one. Technically we need not include the consistency relation as part of the definition of a correct and hippocratic transformation, because we have immediately from the definitions Lemma 1 R(m, n) ⇔ −→ R (m, n) = n ⇔ ←− R (m, n) = m. However, the consistency relation is for software engineering purposes the primary part of the transformation definition, so it is convenient to include it. In order to help the reader’s intuition we will use the following, informal, running example. Proc. BX 2012 2 / 16 ECEASST Example 1 Let the elements of model set M be UML models. Let each element of model set N be a test suite, given as a set of test classes. Suppose the development team wishes to count a UML model m as being consistent with a test suite n iff the following two conditions hold: • for every class in model m, say with name Foo1, there is at least one test class in n, with the naming convention that each such test class is called TestFooX for some natural number X ; • for every string Name such that there is at least one test class in n with a name of the form TestNameX for an integer X (there could be several different values of X for the same Name), there is a class called Name in m.2 We write T (m, n) if this holds. Notice that each model typically contains a lot of information not included in the other. There is a choice of ways to restore consistency, but one possibility is: • −→ T (m, n) deletes any test classes from n whose names are of the form TestNameX but for which there is no class Name in m. For any class (say called Name) in m not having any corresponding test class in n, it adds one “skeleton” test class TestName0. • ←− T (m, n) deletes from m any class for which n contains no test class (along with any other model elements that must be deleted, such as associations to deleted classes). For any test class in n whose name is of the form TestNameX but for which there is no class Name in m, it adds a new class Name to m (in a suitable “default” state, e.g., not related to any other class, and having no attributes or operations). Appropriately implemented, this bidirectional transformation could (and should) be correct and hippocratic. A well-known problem is that these definitions alone are too weak to enforce “sensible” be- haviour. Unfortunately the most natural extra conditions to impose have the disadvantage that they seem to be too strong in practice. One well-known possibility, here using terminology coined in [Dis08], is: Definition 3 R : M ↔ N is history ignorant if for all m, m′ ∈ M and n, n′ ∈ N, we have −→ R (m, −→ R (m′, n)) = −→ R (m, n) ←− R ( ←− R (m, n′), n) = ←− R (m, n) The terminology for special properties of bidirectional transformations is mildly problematic, partly because different perspectives make different names seem natural. In earlier versions of this paper, what we now call history ignorance was termed strong undoability. This was natural to 1 For simplicity, in the example we assume that UML class names are strings containing only characters from [A-Za- z], and in particular that there is only one package! 2 Note that there could be other test classes in n whose names were not of this form, e.g. called BasicSetUpTest, Performance; these are deemed to be irrelevant for purposes of determining consistency with a given UML model. 3 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations us because the notion called undoability in [Ste10] demanded the same conditions as above, but only for m ∈ M and n ∈ N satisfying R(m, n). That notion makes the bidirectional transformation undoable in the following sense: suppose that (m, n) is a consistent pair of models, and suppose the developer of m modifies it to m′, propagates the modification by applying −→ R , and then wishes to undo the modification, returning to m. To say that the transformation is undoable is to say that now, applying −→ R will return the situation to exactly what it was in the beginning, the pair (m, n); mistakes can be undone – provided that the initial pair of models was consistent. History ignorance is a stronger form of undoability, in that it demands the same conditions for more model pairs. Indeed, the condition does capture a notion of undoability that is stronger, in the following sense. Suppose our indecisive developer starts from any pair of models (m, n), not necessarily consistent, and behaves as before. The final pair of models, (m, n′) say, may of course not be identical to the initial pair (m, n), since −→ R always ensures consistency and the original state may not have been consistent. Still, the developer’s mistaken modification to m has no effect in the final situation, in the sense that n′ is the very same model that would have been the result of −→ R (m, n); the mistake has been undone, even though the initial state of the pair of models might not have been consistent. An alternative perspective, though, is that a history ignorant bidirectional transformation al- lows the developer to be safely ignorant of the history of when modifications to their model have been propagated to the other side: for example, if a developer starts with m′ and modifies it to m, it does not matter whether −→ R was ever applied to m′; provided that it is applied to m at the end, the effect on the other side’s model will be the same regardless. We use the term history ignorance here for consistency with [Dis08, XSHT11]. Whatever our terminology, the special situation that we have when a bidirectional transforma- tion is history ignorant would clearly be hugely advantageous to the usability of a bidirectional- transformation enabled tool, because the tool could reasonably propagate changes as and when it was convenient to do so without needing the developer’s permission. It is unfortunate that realistic bidirectional transformations do not have this property. As we shall see in Section 4, the essential reason why they do not is that the information that is relevant to consistency is usually interdependent with the rest of the information in a model, whereas history ignorance requires the consistency-relevant information to be independent of the rest. History ignorance is also algebraically a more natural condition than undoability, as we shall see. That it is indeed stronger than undoability is illustrated by the following (minimal) example, this one given formally. Example 2 Let M = {a, b, c}×{false, true} and let N = {a, b, c}. For all x, y ∈{a, b, c}, φ ∈ {false, true}, let: R((x, φ ), y) hold iff x = y; −→ R ((x, φ ), y) = x; ←− R ((x, φ ), y) = (y,¬φ ) if (as sets) {x, y} = {a, c} = (y, φ ) otherwise. Then R is correct, hippocratic and undoable, but not history ignorant. A counterexample to his- tory ignorance is that ←− R ( ←− R ((a, true), c), b) = ←− R ((c, false), b) = (b, false) whereas ←− R ((a, true), b) = (b, true). However, it is easy to check that there is no counterexample to undoability. Proc. BX 2012 4 / 16 ECEASST Example 3 The example begun in Example 1 is not even undoable. Suppose we start with a UML model m containing class Foo and a test suite n which has a test class TestFoo1 containing some actual test code, and also consistent in every other way so that T (m, n). We modify m in a way which involves deleting Foo, giving m′, and apply −→ T . This results in test class TestFoo1 being deleted, and the code which it contained being lost. If we now edit m′ back to its original state m, and again apply −→ T , the resulting test suite will include a skeleton test class for Foo, called TestFoo0, but the lost test code is not restored. That is, −→ T (m, −→ T (m′, n)) 6= n. 3 Coordinate grid induced by a bidirectional transformation Suppose we are given a bidirectional transformation R which is correct and hippocratic (but not necessarily undoable). Recall the equivalences from [Ste08] (but presented here with slightly different symbols for better readability), defined in terms of R. Definition 4 The equivalence relations ∼MF and ∼ M B on M, and ∼ N F and ∼ N B on N, are defined as follows: • m ∼MF m ′ ⇔∀n ∈ N. −→ R (m, n) = −→ R (m′, n) • m ∼MB m ′ ⇔∀n ∈ N. ←− R (m, n) = ←− R (m′, n) and dually, • n ∼NF n ′ ⇔∀m ∈ M. −→ R (m, n) = −→ R (m, n′) • n ∼NB n ′ ⇔∀m ∈ M. ←− R (m, n) = ←− R (m, n′) Notice that it is immediate that these relations are indeed equivalence relations. Intuitively, m ∼MF m ′ says “m and m′ do not differ in any way that is visible on the N side”. The reader familiar with lenses will recognise that this generalises ∼g. On the other hand, m ∼MB m′ says that “the only differences between m and m′ are those visible on the N side, so that they become indistinguishable after any synchronisation with an element of N”. The reader familiar with [BFP+08] will recognise that this generalises ∼max, the coarsest equivalence with respect to which a lens is quasi-oblivious. In an even more specialised setting, that of constant complement view updates, it generalises the equivalence defined in Theorem 7.2 of [BS81]. We can import the latter into the symmetric setting and demonstrate the relationship as follows. Definition 5 The relation ≡ on M is defined as follows: m ≡ m′ ⇔∃n ∈ N. ←− R (m, n) = m′ In general, this is not an equivalence relation, even though for consistency with [BS81] we have used the ≡ symbol for it. For history ignorant bidirectional transformations R, however, we see that it is an equivalence relation because it coincides with ∼MB : 5 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations Proposition 1 Let R be a history ignorant bidirectional transformation. Then m ∼MB m ′ iff m ≡ m′. We postpone the proof until Section 4, by which point we will have introduced some conse- quences of our definitions which make it easier. We will generally suppress the superscripts and just write ∼F , ∼B. Example 4 Returning to the informal example of Examples 1, 3, we see that: • m ∼MF m ′ iff the set of names of classes in m is the same as the set of names of classes in m′; • m ∼MB m ′ iff m and m′ are identical apart from (perhaps) containing different classes in the default state, that is, if one can be edited into the other just by adding and/or deleting default state classes. • n ∼NF n ′ iff n and n′ are identical apart from (perhaps) differing in the set of Names for which they include a “skeleton” test class called TestName0. (In particular, if n con- tained a skeleton TestName0, n′ could be equivalent even if it did not contain any test class TestName0. However, if n’s TestName0 had been filled in with some test code, then in order to be equivalent, n′ would have to have a TestName0 with identical code.) • n ∼NB n ′ iff the set of class names derived by taking class name Name for every test class in n whose name is of the form TestNameX for some integer X (ignoring any test classes with names not of that form) is the same as the set of names derived from n′ using the same procedure. Very informally, the fact that ∼MB and ∼ N F are relatively fine – e.g. one feels that it would be unlikely for a randomly chosen m and m′ to happen to be such that m ∼MB m ′ – arises from the fact that both models can hold plenty of information not present in the other; it is not likely that m and m′ will have only differences which are visible on the N side, because most potential differences between them are invisible there. If we represent a bidirectional transformation R by giving a table for −→ R and a table for ←− R , each with a row for each element of M and a column for each element of N, the equivalences can be read off: m ∼F m′ if the rows for m and m′ in the −→ R table are identical, n ∼F n′ if the columns for n and n′ in the −→ R table are identical, and similarly for the ∼B equivalences using the ←− R table. Example 5 Let us represent Example 2 in this way. −→ R a b c (a, true) a a a (b, true) b b b (c, true) c c c (a, false) a a a (b, false) b b b (c, false) c c c ←− R a b c (a, true) (a, true) (b, true) (c, false) (b, true) (a, true) (b, true) (c, true) (c, true) (a, false) (b, true) (c, true) (a, false) (a, false) (b, false) (c, true) (b, false) (a, false) (b, false) (c, false) (c, false) (a, true) (b, false) (c, false) Proc. BX 2012 6 / 16 ECEASST We read off that (x, φ ) ∼F (x′, φ ′) iff x = x′, while m ∼B m′ only when m = m′. Looking at N, n ∼F n′ always, while n ∼B n′ only when n = n′. Remark 1 Clearly, that n ∼F n′ always is equivalent to saying that −→ R ignores its second argu- ment, that is, that the transformation is a lens in the sense of [FGM+07]. We shall use this as the definition. Definition 6 A bidirectional transformation R is a lens if it is correct and hippocratic and fur- thermore −→ R ignores its second argument, which we therefore omit for notational convenience. The relationship between lenses and bidirectional transformations is easy to see and was dis- cussed in Section 4.4 of [Ste10], although in the context of undoability rather than history igno- rance. We will not introduce lens notation and laws, but simply state for the benefit of readers familiar with lenses: Proposition 2 Let R be a (for once, not necessarily correct and hippocratic) bidirectional transformation in which −→ R ignores its second argument. Then 1. R is a well-behaved lens in the sense of [FGM+07] iff it is correct and hippocratic. 2. R is a very well-behaved lens in the sense of [FGM+07] iff it is correct, hippocratic and history ignorant. The following easy result was proved in [Ste08] and illustrated above. Proposition 3 If both m1 ∼F m2 and m1 ∼B m2 then m1 = m2. This results shows that a model is uniquely determined by specifying its ∼F and its ∼B equiv- alence class. Given a model m, we can think of its ∼F equivalence class as its x-coordinate and of its ∼B equivalence class as its y-coordinate. Specifying coordinates in this sense determines at most one model, but some pairs of coordinates specify no model; that is, if a given ∼F equiv- alence class and a given ∼B equivalence class intersect, they do so in a set of just one model, but it is in general possible that they do not intersect. We think of the elements of a model space laid out in a coordinate grid in this way; some squares on the grid are empty, but no square contains more than one model. Let MF be a transversal3 of ∼F and MB be a transversal of ∼B. We may identify M with a subset of MF ×MB: that is, henceforth we notate any element m∈M as (mF , mB) where mF is the unique element of MF satisfying mF ∼F m and mB is the unique element of MB satisfying mB ∼B m . The closure of M, M, is the whole of MF ×MB. Similarly for N, we let NF be a transversal of ∼F and NB be a transversal of ∼B. Remark 2 We are identifying a model by specifying its equivalence class in each of two equiv- alence relations. We have a notational choice to make here: do we represent a model m by giving 3 Recall that a transversal T for an equivalence relation on a set A is a set T ⊆ A comprising exactly one element of each equivalence class. 7 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations representatives of each equivalence class, (mF , mB) or do we use some notation for the equiv- alence classes themselves, ([m]∼F , [m]∼B )? Each choice has strengths and weaknesses. Since there is, in our setting, generally no canonical choice of representative of an equivalence class, the latter choice appeals; but it has the disadvantage that we must either define new symbols for a version of R lifted to equivalence classes, and juggle both versions in our work, or risk the confusion that might result from our abusing notation by not doing so. Instead we choose the former option, despite the disadvantage that it involves an arbitrary choice of transversal. What we gain is that when we write, for example, mF , it does not matter whether we think of mF as partial information concerning a model m = (mF , mB) or as a model in its own right: it is both. It is important to understand, however, that it is not generally possible to ensure that the elements of MF are all ∼B equivalent; see Lemma 3. This way of representing models is useful because it separates relevant from irrelevant infor- mation for purposes of applying the components of the bidirectional transformation. Lemma 2 1. Whenever m ∼F m′ and n ∼B n′ we have R(m, n) ⇔ R(m′, n′); that is, whether R((mF , mB), (nF , nB)) is determined from mF and nB alone: it is R(mF , nB). 2. Whenever m ∼F m′ and n ∼F n′ we have −→ R (m, n) = −→ R (m′, n′); that is, the value of −→ R ((mF , mB), (nF , nB)) is determined by mF and nF alone: it is −→ R (mF , nF ). 3. Whenever m ∼B m′ and n ∼B n′ we have ←− R (m, n) = ←− R (m′, n′); that is, the value of ←− R ((mF , mB), (nF , nB)) is determined by mB and nB alone: it is ←− R (mB, nB). Proof. If R(m, n) and m′ ∼F m then since n = −→ R (m, n) = −→ R (m′, n) we must have R(m′, n) by Remark 1. Similarly, ←− R (m, n) = m iff R(m, n) in which case if n′ ∼B n then also R(m, n′). In other words, whether R((mF , mB), (nF , nB)) is determined by the entries mF and nB alone. Since mF itself is an element of M, and nB itself is an element of N, we have R(m.n) = R(mF , nB). Similarly, if −→ R ((mF , mB), (nF , nB)) = (n′F , n ′ B) then by definition −→ R ((mF , m′′B), (nF , n ′′ B)) = (n′F , n ′ B) for any other m ′′ B, n ′′ B; in other words the result of −→ R ((mF , mB), (nF , nB)) is determined by the entries mF , nF alone. Dually, ←− R ((mF , mB), (nF , nB)) is determined by mB, nB alone. Remark 3 In terms of the symmetric lens formalism of [HPW11], MB ×NF forms a minimal complement. Example 6 In model set M of Example 2, let us pick MF = {(a, true), (b, true), (c, true)} (the second element of each pair being an arbitrary choice) and MB = M. With respect to these choices, the coordinate grid for M is: (a, true) (a, true) (b, true) (b, true) (c, true) (c, true) (a, false) (a, false) (b, false) (b, false) (c, false) (c, false) (a, true) (b, true) (c, true) Proc. BX 2012 8 / 16 ECEASST For NF we may take any of {a}, {b}, {c}; for NB we must take {a, b, c}. The coordinate grid for N is a single column, because the transformation is a lens with N its abstract side. In terms of the coordinate grid, whether m is consistent with n is determined by the column of m and the row of n. It is natural to ask whether one column can be consistent with more than one row. The answer is yes, but only provided that the rows do not overlap, in the following sense: Lemma 3 Suppose R(mF , nB) and R(mF , zB) where nB, zB ∈NB and nB 6= zB. Then there cannot exist any nF ∈ NF such that both (nF , nB) ∈ N and (nF , zB) ∈ N. Dually, suppose R(mF , nB) and R(wF , nB) and mF 6= wF . Then there cannot exist any mB ∈ MB such that both (mF , mB) ∈ M and (wF , mB) ∈ M. Proof. Suppose that such an nF did exist. Then −→ R (mF , (nF , nB)) = (nF , nB) by hippocraticness and similarly −→ R (mF , (nF , zB)) = (nF , zB). But (nF , nB) ∼F (nF , zB) so (nF , nB) = (nF , zB) which is a contradiction. 4 Applications of equivalences In this section we exploit the results of the previous section to investigate the relationships be- tween different special properties of bidirectional transformations. We know that given m1, m2 ∈ M there can be at most one m ∈ M such that m ∼F m1 and m∼B m2. An important special case is when there is exactly one: every square in our “coordinate grid” is occupied. Definition 7 M is full with respect to bidirectional transformation R if for any m1, m2 ∈ M there exists m ∈ M such that m ∼F m1 and m ∼B m2. Intuitively, when we specify a model m ∈ M by specifying its ∼F and ∼B equivalence classes, what we are doing is picking out the information in m which is relevant to the question of whether m is consistent with some model in N. As we have seen, this consistency is completely deter- mined by m’s ∼MF equivalence class (and dually, for a model n ∈ N its consistency is determined by its ∼NB class). In the simplest practical cases, this consistency-relevant information may actu- ally be identifiable in the model, as being, for example, the set of model elements of particular types contained in the model; however, our set-up also works generally. What it means for M to be full is that the consistency-relevant information is in in a certain sense independent of the rest of the information needed to specify a model fully; there is no redundancy in the representation. If M is full, and if m = (mF , mB) is changed by modifying one of the pieces of information (say mF is changed to m′F ), it will not be necessary for the other piece of information to be modified as a side-effect, because fullness tells us that (m′F , mB) will definitely exist as a model in M. This simplifies the situation in an important way. Contrast the more usual situation we see in Examples 1, 3; the information in m ∈ M on which consistency depends (the set of class names) is strongly interdependent with the rest of the information in the model. For example, suppose we take m1 to be a model containing only a class Foo in default 9 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations state (no attributes or other associated information), and m2 to be a model containing a class Bar which is not in default state (say it has an attribute, or a state machine, or whatever). It is clear that there can be no model m such that m ∼F m1 and m ∼B m2. In order for m ∼F m1 to hold, the set of names of classes in m must be the singleton {“Foo”}; in order for m ∼B m2 to hold, the non-default-state class Bar must be in m. More generally, we may informally consider that the more sparsely the coordinate grid is populated, the more dependency there is between the consistency-relevant information and the rest. Definition 8 Let R : M ↔ N be a bidirectional transformation inducing equivalences and a coordinate system as usual. We say that R is matching if there is a bijection f : MF → NB such that R(mF , f (mF )) for all mF ∈ MF . We say that R is simply matching if, in addition, R(mF , nB) holds only when nB = f (mF ). Lemma 4 If N is full, then given mF ∈ MF there exists a unique nB ∈ NB satisfying R(mF , nB). Dually if M is full, then given nB ∈ NB there exists a unique mF ∈ MF satisfying R(mF , nB). Therefore if both M and N are full, then R is simply matching. Proof. Follows directly from Lemma 3. Proposition 4 The following are equivalent: 1. R : M ↔ N is history ignorant. 2. M and N are full with respect to R. 3. For each m∈M and n∈N we have −→ R (m, n)∼F n and ←− R (m, n)∼B m: that is, −→ R stabilises the coordinate grid columns of N and ←− R stabilises the coordinate grid rows of M. Proof. 1 ⇔ 3 is immediate from the definitions. Next we show (1, 3) ⇒ 2. Let m1, m2 ∈ M. We must construct m∈M such that m∼F m1 and m∼B m2. Write m1 = (m1F , m1B), m2 = (m2F , m2B). Pick any (nF , nB) ∈ N. Then, using 3., for some wF ∈ MF , zB ∈ NB we have −→ R ((m1F , m1B), n) = (nF , zB) ←− R ((m2F , m2B), (nF , zB)) = (wF , m2B) and by correctness R(m1F , zB) and R(wF , zB). Using 1. and Lemma 4, m1F = wF so we have constructed (m1F , m2B) = m ∈ M as required. Dually for N. Finally we show 2⇒3. Consider −→ R (m, (nF , nB) = (n′F , n ′ B); we must show that nF = n ′ F . Since R is correct, R(m, (n′F , n ′ B)) which is equivalent to R(m, n ′ B). Since N is full, (nF , n ′ B) ∈ N, and since R(m, n′B), by hippocraticness −→ R (m, (nF , n′B)) = (nF , n ′ B). But since (nF , nB) ∼F (nF , n ′ B), (n′F , n ′ B) = −→ R (m, (nF , nB)) = −→ R (m, (nF , n′B)) = (nF , n ′ B) so nF = n ′ F as required. Corollary 1 If R is history ignorant, then R is simply matching. The following example shows that not every undoable transformation is simply matching. Proc. BX 2012 10 / 16 ECEASST Example 7 We slightly modify Example 2 so that undoability is retained but simple matching is lost. Let M = N = {a, b, c}×{false, true}. For all x, y ∈{a, b, c}, ψ, φ ∈{false, true}, let: R((x, φ ), (y, ψ)) iff x = y; −→ R ((x, φ ), (y, ψ)) = (x, ψ); ←− R ((x, φ ), (y, F)) = (y,¬φ ) if (as sets) {x, y} = {a, c} = (y, φ ) otherwise ←− R ((x, φ ), (y, T )) = (y, φ ) This transformation is still correct, hippocratic and undoable, but not history ignorant. To see that it is not simply matching, observe that {(a, F), (a, T )} is a ∼MF -equivalence class which is consistent with two ∼NB -classes, viz. {(a, F)} and {(a, T )}. Our “twist” has ensured that these two classes remain separate, because ←− R ((c, T ), (a, F)) = (a, F) 6= (a, T ) = ←− R ((c, T ), (a, T )). Now it is easy to prove Proposition 1 relating Bancilhon and Spyratos’ equivalence to our ∼MB . Proof. Suppose first that m ≡ m′, that is, ∃n ∈ N. ←− R (m, n) = m′. We need to show that m ∼B m′. Since R is history ignorant, by Proposition 4, m′ = ←− R (m, n) ∼B m as required. Conversely, suppose m ∼B m′; we must show that ∃n ∈ N. ←− R (m, n) = m′. By Corollary 1 there is a unique nB ∈ NB such that R(m′, nB). Then by correctness of R and by Lemma 2,←− R (m, nB)∼F m′. By Proposition 4, ←− R (m, nB)∼B m ∼B m′. Finally by Proposition 3, this implies that ←− R (m, nB) = m′ as required. (Notice that any n ∼NB nB would have done as well.) Once we have a simply matching bidirectional transformation R it is natural to relabel the ele- ments of MF and NB so that both are identified with a matching transversal P, so that R((p, mB), (nF , p′)) iff p = p′. This is reminiscent of constant complement bidirectional transfor- mations, but it is important to be aware (a) that M ⊆P×MB but equality does not hold in general; (b) that while −→ R ((p, mB), (nF , p′)) = (n′F , p), we do not necessarily have n ′ F = nF . In fact, by Lemma 2 n′F depends on p and nF . We will write −→ R ((p, mB), (nF , p′)) = ( f p(nF ), p). Dually,←− R ((p′, mB), (nF , p)) = (p, bp(mB)). The property of being simply matching is an interesting one, being strictly weaker than being history ignorant, satisfied by realistic examples such as Example 1, and yet not universally true. It turns out that there is an alternative characterisation of this class of bidirectional transformations: it comprises those that can be constructed by placing two lenses “tail to tail” in a certain way. Definition 9 Let R : M ↔ N be a simply matching bidirectional transformation with matching transversal P. Then we define lenses RM : M ↔ P and RN : N ↔ P as follows, exploiting the representation of elements of M as elements of P×MB: • RM(m, p) iff −→ RM(m) = p iff m = (p, mB) for some mB ∈ MB. • ←− RM((p′, mB), p) = (p, bp(mB)). • Dually, RN (n, p) iff −→ RN (n) = p iff n = (nF , p) for some nF ∈ NF , and 11 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations • ←− RN ((nF , p′), p) = ( f p(nF ), p). The following lemma is obvious: Lemma 5 RM and RN are indeed correct and hippocratic. The following construction of a bidirectional transformation from a pair of lenses has been recorded before, see for example Theorem 6 of [Dis08]; here we shall show that it produces exactly the simply matching bidirectional transformations. Definition 10 Let RM : M ↔ P and RN : N ↔ P be any lenses sharing a common view. Then the bidirectional transformation R = 〈RM, RN〉 : M ↔ N constructed from RM and RN is defined thus: • R(m, n) iff −→ RM(m) = −→ RN (n) • −→ R (m, n) = ←− RN (n, −→ RM(m)) • ←− R (m, n) = ←− RM(m, −→ RN (n)) Proposition 5 Given lenses RM : M ↔ P and RN : N ↔ P, 1. 〈RM, RN〉 is indeed correct and hippocratic. 2. 〈RM, RN〉 is simply matching with common transversal in bijection with P. Proof. Let R = 〈RM, RN〉. 1. Correctness: let n′ = −→ R (m, n) = ←− RN (n, −→ RM(m)). We have to show that R(m, n′), that is, that−→ RM(m) = −→ RN (n′). Now −→ RN (n′) = −→ RN ( ←− RN (n, −→ RM(m))) = −→ RM(m) as required. Hippocratic- ness: suppose R(m, n), that is, −→ RM(m) = −→ RN (n), and consider −→ R (m, n) = ←− RN (n, −→ RM(m)) =←− RN (n, −→ RN (n)) = n by hippocraticness of RN . 2. We show that the ∼MF equivalence classes are the sets ( −→ RM)−1({p}) for p ∈ P. Suppose m1 and m2 are in ( −→ RM)−1({p}). Then for any n∈N, −→ R (m1, n) = ←− RN (n, −→ RM(m1)) = ←− RN (n, p) =←− RN (n, −→ RM(m2)) = −→ R (m2, n), so m1 ∼F m2 as required. Conversely, suppose that m1 ∼F m2 and pick n1 such that −→ RN (n1) = −→ RM(m1) = p1. Then since −→ R (m1, n1) = −→ R (m2, n1) by hypothesis, we have n1 = ←− RN (n1, −→ RM(m1)) = ←− RN (n1, −→ RM(m2)) so by correctness of RN we must have RN (n1, −→ RM(m2)), that is, −→ RN (n1) = −→ RM(m2) = p1 as required. It follows from the definition of R that R is simply matching. We may summarise Lemma 5 and Proposition 5 in the following (informally-stated) theorem: Theorem 1 A bidirectional transformation R : M ↔ N is simply matching if and only if it can be decomposed into a pair of lenses working “tail to tail”. Any such decomposition gives rise to a choice of matching transversal for R, and vice versa. Proc. BX 2012 12 / 16 ECEASST Example 2 is simply matching; take f ((a,true)) = a etc. Example 1 is also simply matching, for each possible subset of the set of all legal class names determines and is determined by a transversal element (of both MF and NB) and T (mF , nB) holds iff the sets thus determined by mF and nB are identical. Notice that since we have already observed that neither of these examples is history ignorant, and that Example 1 is not even undoable, this shows that simply matching is a strictly weaker condition. The following tiny example, which is matching but not simply matching, illustrates some of the difficulty inherent in “less nice” bidirectional transformations. Example 8 Let M = N = {0, 1} and let R(m, n) hold iff mn = 0. −→ R and ←− R are determined by correctness and hippocraticness: R 0 1 0 T T 1 T F −→ R 0 1 0 0 1 1 0 0 ←− R 0 1 0 0 0 1 1 0 0 6∼F 1 because −→ R (0, 1) = 1 6= −→ R (1, 1); 0 6∼B 1 because ←− R (0, 1) = 0 6= ←− R (1, 1); thus each element of M forms an equivalence class under each equivalence, and dually for N. Therefore there is only one choice of transversal, and we identify the elements with the equivalence classes. Considered as a subset of MF ×MB, M is the diagonal subset {(0, 0), (1, 1)} where (0, 0) rep- resents 0 and (1, 1) represents 1. That is, the coordinate grids for M and N are both, identically: 1 1 0 0 0 1 We have here the simplest possible example in which there are two distinct elements of MF (0 and 1) compatible with one element of NB (0), and only one of those MF elements (0) is also compatible with a second, distinct element of NB (1). In other words, both columns of M’s coordinate grid are compatible with the 0 row of N’s, and the 0 column of M’s grid is also compatible with the 1 row of N’s. Note that neither the rows, nor the columns, of the coordinate grids overlap in the sense of Lemma 3. Clearly R is not undoable. For example, R(0, 1), but −→ R (0, −→ R (1, 1)) = −→ R (0, 0) = 0 6= 1. Example 9 Finally, lest the reader suspect that all bidirectional transformations be matching, we record an example which is not. Let M = {0, 1} and N = {a, b, c}. Let R, −→ R and ←− R be as follows: R a b c 0 T T F 1 F T T −→ R a b c 0 a b a 1 c b c ←− R a b c 0 0 0 1 1 0 1 1 We read off that the only non-trivial equivalence is that a ∼NF c. Taking a as the representative of their ∼NF equivalence class, the coordinate grids are 1 1 0 0 0 1 c c b b a a a b This is not undoable, since although R(0, b), we have ←− R ( ←− R (0, c), b) = ←− R (1, b) = 1. 13 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations Figure 1: Implications between properties of correct hippocratic bidirectional transformations. Labels p;q on arrows indicate that p is for the implication and q for absence of the reverse implication, “def” meaning direct from the definition.     very well­behaved lens lens history ignorant bx simply­matching bx matching bx undoable bx def; Ex 8 correct and hippocratic bx def; Ex 9 def;Ex 1 def;Ex 2 Cor 1;Ex 1 incomparable (Ex 1,Ex 7) def;Ex 1 Prop2;def To summarise, Figure 1 gives the implication relationships between different special cases of bidirectional transformations. 5 Related work Defining equivalence relations on model sets that are induced by bidirectional transformations goes back at least to [BS81] in the special case of constant complement view updates in databases and to [BFP+08] in the less special case of lenses. We have demonstrated the relation of our work to those papers. A major concern of the model-driven development community, as it has started to consider bidirectional transformations, has been the generalisation to the symmetric case, in which nei- ther model set comprises strict abstractions of the models in the other model set. An early work on properties of such bidirectional transformations was the present author’s MODELS’07 paper that led to [Ste10]; Diskin’s MODELS’08 paper [Dis08] explored further, including, as already remarked, defining history ignorance and discussing the construction of a bidirectional transfor- Proc. BX 2012 14 / 16 ECEASST mation from a pair of lenses. Neither of those papers, however, made use of equivalences on model sets comparable to those considered in the earlier database and lens work. These were first generalised to the symmetric case as part of the work in [Ste08], but only a few results relating to them (identified here) were given in that paper. Later work has included [XSHT11], focusing on the additional problems posed by concurrent updates, and a body of work exemplified by [DXC+11] on delta-based bidirectional transforma- tions. The latter defines several other properties of bidirectional transformations; there is more work to be done to fully elucidate the connections. 6 Conclusion We have laid out some results relating to the principal equivalence relations induced on model sets by a correct and hippocratic bidirectional transformation between them. By means of these results we have established implications and non-implications between many different conditions that can be placed on bidirectional transformations to ensure that they are “nice”. A topic of conversation among people interested in bidirectional transformations has long been the extent to which the symmetric case, in which we relate models neither of which is a strict abstraction of the other, raises essentially new problems from the asymmetric case studied earlier in the database field. In practice, it is often possible to conceptualise a symmetric bidirectional transformation as a pair of lenses placed “tail to tail”, that is, having a common view: the view captures the information which is common to both models, and the lenses manage the synchro- nisation. Actually writing the transformation this way would have the obvious drawback that it would involve a great deal of duplication between the two lenses. In this paper, we have char- acterised the bidirectional transformations that could, in principle, be written in this way; they are the simply matching ones. Although we have shown that not all bidirectional transforma- tions are simply matching, we have the impression that a large class of practical examples (such as our Example 1 etc.) are in fact simply matching. A bidirectional transformation language that gave good, usable facilities for expressing and working with simply matching transforma- tions might be practically useful even if it did not permit the expression of non-simply-matching transformations. We have also begun, but not reported here, an investigation into subspaces and subspace pairs of model sets, which capture the fact that teams of developers can agree to stay within certain subspaces of the model spaces, in which case it is desirable that applying a transformation will not move them outside their agreed zone. In future work we will build on this to investigate the implications of adding an information orderings to a model set, and relate this work to the study of monoids of edits acting on model spaces. Acknowledgements: The author thanks the referees, the participants in the Bx’12 workshop, and Zinovy Diskin, for very helpful comments, including some that we hope will lead to future work. 15 / 16 Volume 49 (2012) Equivalences induced on model sets by bidirectional transformations Bibliography [BFP+08] A. Bohannon, J. N. Foster, B. C. Pierce, A. Pilkiewicz, A. Schmitt. Boomerang: Re- sourceful Lenses for String Data. In ACM SIGPLAN–SIGACT Symposium on Prin- ciples of Programming Languages (POPL), San Francisco, California. Jan. 2008. [BS81] F. Bancilhon, N. Spyratos. Update Semantics of Relational Views. ACM Trans. Database Syst. 6(4):557–575, 1981. [Dis08] Z. Diskin. Algebraic Models for Bidirectional Model Synchronization. In Model Driven Engineering Languages and Systems, 11th International Conference, MOD- ELS 2008, Toulouse, France, September 28 - October 3, 2008. Proceedings. Lecture Notes in Computer Science 5301, pp. 21–36. Springer, 2008. [DXC+11] Z. Diskin, Y. Xiong, K. Czarnecki, H. Ehrig, F. Hermann, F. Orejas. From State- to Delta-Based Bidirectional Model Transformations: The Symmetric Case. In Model Driven Engineering Languages and Systems, 14th International Conference, MOD- ELS 2011, Wellington, New Zealand, October 16-21, 2011. Proceedings. Lecture Notes in Computer Science 6981, pp. 304–318. Springer, 2011. [FGM+07] J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, A. Schmitt. Combina- tors for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Transactions on Programming Languages and Systems 29(3):17, May 2007. [HPW11] M. Hofmann, B. C. Pierce, D. Wagner. Symmetric Lenses. In ACM SIGPLAN– SIGACT Symposium on Principles of Programming Languages (POPL), Austin, Texas. Jan. 2011. [Ste08] P. Stevens. Towards an algebraic theory of bidirectional transformations. In Proceed- ings of the International Conference on Graph Transformations, ICGT’08. Lecture Notes in Computer Science 5214, pp. 1–17. Springer, September 2008. [Ste10] P. Stevens. Bidirectional Model Transformations in QVT: Semantic Issues and Open Questions. Journal of Software and Systems Modeling (SoSyM) 9(1):7–20, 2010. [XSHT11] Y. Xiong, H. Song, Z. Hu, M. Takeichi. Synchronizing concurrent model updates based on bidirectional transformation. Journal of Software and Systems Modeling (SoSyM), 2011. Online first. Proc. BX 2012 16 / 16 Introduction Background Coordinate grid induced by a bidirectional transformation Applications of equivalences Related work Conclusion