Bidirectional Transformations

This is the proceedings of the 4th International Workshop on Bidirectional Transformations (Bx 2015). Bidi

rectional transformations (Bx) are a mechanism for maintaining the consistency of at least two related sources of information. Such sources can be relational databases, software models and code, or any other document following standard or ad-hoc formats. Bx are an emerging topic in a wide range of research areas, with prominent presence at top conferences in several di erent elds (namely databases, programming languages, software engineering, and graph transformation), but with results in one eld often getting limited exposure in the others. Bx 2015 was a dedicated venue for Bx in all relevant elds and part of a workshop series that was created in order to promote cross-disciplinary research and awareness in the area. As such, since its beginning in 2012, the workshop rotated between venues in di erent elds. In 2015, Bx was co-located with STAF for the rst time, and was previously held at the following locations: 1. Bx 2012: Tallinn, Estonia, co-located with ETAPS 2. Bx 2013: Rome, Italy, co-located with ETAPS 3. Bx 2014: Athens, Greece, co-located with EDBT/ICDT

The call for papers attracted 11 complete submissions (14 abstracts were initially submitted) from which the program committee, after a careful reviewing and discussion process, selected 7 papers for presentation at the workshop (6 regular papers and 1 tool paper):

Michael Johnson and Robert Rosebrugh: Spans of Delta Lenses Faris Abou-Saleh, James McKinna, and Jeremy Gibbons: Coalgebraic Aspects of Bidirectional Computation

Michael Johnson and Robert Rosebrugh: Distributing Commas, and the Monad of Anchored Spans

Zirun Zhu, Hsiang-Shang Ko, Pedro Martins, Jo~ao Saraiva, and Zhenjiang Hu: BiYacc: Roll Your Parser and Pretty-Printer into One (tool paper) Soichiro Hidaka, Martin Billes, Quang Minh Tran, and Kazutaka Matsuda: Trace-based Approach to Editability and Correspondence Analysis for Bidirectional Graph Transformations James Cheney, Jeremy Gibbons, James McKinna, and Perdita Stevens: Towards a Principle of Least Surprise for Bidirectional Transformations Anthony Anjorin, Erhan Leblebici, Roland Kluge, Andy Schurr, and Perdita Stevens: A Systematic Approach and Guidelines to Developing a Triple Graph Grammar

In addition to the presentation of these papers, the program of Bx 2015 consisted of two panel discussions. The rst one, focussing on \Benchmarks and reproducibility", addressed topics such as: the current status and evolution perspectives of the Bx Examples Repository; how to best support the reproduction of paper results; or how to replicate in this community successful benchmarking initiatives from other areas. The second panel, focussing on \Reaching out to end-users", tried to identify what would be necessary for Bx languages and tools to be more applied in practice, and addressed questions such as: should we just invest more time in making existing tools more stable, usable, and better documented? or do we still need to improve the underlying Bx techniques to provide stronger guarantees to end users, namely some sort of least change or \least surprise"? We hope these panels helped the Bx community take an interest in aspects of Bx that must be improved for its research to have a real impact in di erent application elds. These might also pave the way for interesting submissions to next year's Bx workshop, which will be held on April 8th, 2016, in Eindhoven, The Netherlands, again co-located with ETAPS.

We would like to thank the Program Committee and the external reviewers for their detailed reviews and careful discussions, and for the overall e ciency that enabled the tight schedule for reviewing. We would also like to thank all the authors and participants for helping us make Bx 2015 a success.

June 2015, Alcino Cunha (INESC TEC and Universidade do Minho) and Ekkart Kindler (Technical University of Denmark, DTU) PC chairs of Bx 2015

Program Committee

Anthony Anjorin, Chalmers j University of Technology

Anthony Cleve, University of Namur Alcino Cunha (co-chair), INESC TEC and Universidade do Minho Romina Eramo, University of L'Aquila Jeremy Gibbons, University of Oxford Holger Giese, Hasso Plattner Institute at the University of Potsdam Soichiro Hidaka, National Institute of Informatics Michael Johnson, Macquarie University Ekkart Kindler (co-chair), Technical University of Denmark (DTU) Peter McBrien, Imperial College London Hugo Pacheco, INESC TEC and Universidade do Minho Jorge Perez, Universidad de Chile Arend Rensink, University of Twente Perdita Stevens, University of Edinburgh James Terwilliger, Microsoft Corporation Meng Wang, University of Kent Jens Weber, University of Victoria

Yingfei Xiong, Peking University

External Reviewers

Dominique Blouin Johannes Dyck Nuno Macedo James McKinna

Uwe Wolter Spans of Delta Lenses

Michael Johnson Departments of Mathematics and Computing, Macquarie University

Robert Rosebrugh Department of Mathematics and Computer Science

Mount Allison University

Abstract

As part of an ongoing project to unify the treatment of symmetric lenses (of various kinds) as equivalence classes of spans of asymmetric lenses (of corresponding kinds) we relate the symmetric delta lenses of Diskin et al, with spans of asymmetric delta lenses. Because delta lenses are based on state spaces which are categories rather than sets there is further structure that needs to be accounted for and one of the main findings in this paper is that the required equivalence relation among spans is compatible with, but coarser than, the one expected. The main result is an isomorphism of categories between a category whose morphisms are equivalence classes of symmetric delta lenses (here called fb-lenses) and the category of spans of delta lenses modulo the new equivalence. 1

Introduction

In their 2011 POPL paper [ 4 ] Hoffmann, Pierce and Wagner defined and studied (set-based) symmetric lenses. Since then, with the study of variants of asymmetric lenses (set-based or otherwise), there has been a need for more definitions of corresponding symmetric variants. This paper is part of an ongoing project by the authors to develop a unified theory of symmetric and asymmetric lenses of various kinds. The goal is to make it straightforward to define the symmetric version of any, possibly new, asymmetric lens variant (and conversely). Once an asymmetric lens is defined the unified theory should provide the symmetric version (and vice-versa).

In [ 4 ] Hoffmann et al noted that there were two approaches that they could take to defining symmetric lenses. One involved studying various right and left (corresponding to what other authors call forwards and backwards) operations. The other would be based on spans of asymmetric lenses. In both cases an equivalence relation was needed to define composition of symmetric lenses, to ensure that that composition is associative, and to identify lenses which were equivalent in their updating actions although they might differ in “hidden” details such as their complements (see [ 4 ]) or the head (peak) of their spans. Hoffmann et al gave their definition of symmetric lens in terms of left and right update operations, noting that “in the span presentation there does not seem to be a natural and easy-to-use candidate for . . . equivalence”.

In [ 6 ] the present authors developed the foundations needed to work with spans of lenses of various kinds and proposed an equivalence for spans of well-behaved set-based asymmetric lenses (called here HPW-lenses) and also for several other set-based variants. Our goal was to find the finest equivalence among spans of HPW lenses that would satisfy the requirements of the preceding paragraph. Such an equivalence needed to include, and be coarser than, span equivalence (an isomorphism between the heads of the spans commuting with the Copyright c by the paper’s authors. Copying permitted for private and academic purposes. legs of the spans). Furthermore pre-composing the legs of a span of HPW lenses with a non-trivial HPW lens gives a new span which differs from the first only in the “hidden” details — the head would be different but the updating actions at the extremities would be the same — so such pairs of spans should also be equivalent. In [ 6 ] we were able to show that the equivalence generated by such non-trivial HPW lenses (commuting with the legs of the spans) worked well, and that result was very satisfying because it demonstrated, as so much work in the theory of lenses does, that lenses and bidirectional transformations more generally are valuable generalisations of isomorphisms.

Of course, the work so far, being entirely set-based, is still far from a unified theory, so in this paper we turn to the category-based delta-lenses of Diskin, Xiong and Czarnecki [ 1 ] and study the symmetric version derived from spans of such lenses and compare it with the symmetric (forwards and backwards style) version that Diskin et al propose in [ 2 ].

The paper is structured as follows. In Sections 2 and 3 we review and develop the basic mathematical properties of delta-lenses (based on [ 1 ] and referred to here as d-lenses) and symmetric delta lenses (based on [ 2 ], and called here fb-lenses after their basic operations called “forwards” and “backwards”, thus avoiding clashing with the general use of “symmetric” for equivalence reduced spans of lenses). As in the work of Hoffmann et al, both fb-lenses and spans of d-lenses need to be studied modulo an equivalence relation and the two equivalence relations we propose are introduced in Section 4. In Section 5 we show that using the two equivalences does indeed yield a category of (equivalence classes of) fb-lenses and a category of (equivalence classes of) spans of d-lenses respectively (and of course, we need to show that the equivalence relations we have introduced are congruences in order to construct the categories). Finally in Section 6 we explore the relationship between the two categories and show that there is an equivalence of categories, indeed in this case an isomorphism of categories, between them.

Because of the usefulness of category-based lenses (in particular delta-lenses) in applications, the work presented here lays important mathematical foundations. Furthermore the extra mathematical structure provided in the category-based variants has revealed a surprise — an equivalence generated by non-trivial lenses is not coarse enough to ensure that two spans of d-lenses with the same fb-behaviour are always identified. The difficulty that arises is illustrated in a short example and amounts to “twisting” the structures so that no single lens can commute with the lenses on the left side of the spans, and at the same time commute with the lenses on the right side of the spans. The solution, presented as one of the equivalences in Section 4, relaxes the requirement that the comparison be itself a lens, and asks that it properly respect the put operations on both sides (rather than having its own put operation commuting with both sides). 2

Asymmetric delta lenses

For any category C, we write |C| for the set (discrete category) of objects of C and C2 for the category whose objects are arrows of C. For a functor G : S / V, denote the “comma” category, whose objects are pairs consisting of an object S of S and an arrow α : GS / V , by (G, 1V) . We recall the definition of a delta lens (or d-lens) [ 1, 5 ]: Definition 1 A (very well-behaved) delta lens (d-lens) from S to V is a pair (G, P ) where G : S functor (the “Get”) and P : |(G, 1V)| / |S2| is a function (the “Put”) and the data satisfy: / V is a (i) d-PutInc: the domain of P (S, α : GS

/ V ) is S (ii) d-PutId: P (S, 1GS : GS

/ GS) = 1S (iii) d-PutGet: GP (S, α : GS

/ V ) = α (iv) d-PutPut: P (S, βα : GS of P (S, α : GS / V ) / V / V 0) = P (S0, β : GS0 / V 0)P (S, α : GS / V ) where S0 is the codomain

For examples of d-lenses, we refer the reader to [ 1 ]. Meanwhile, we offer a few sentences here to help orient the reader to the notations used. Both the categories S and V represent state spaces. Objects of S are states and an arrow S / S0 of S represents a specific transition from the state S which is its domain to the state S0 which is its codomain. Such specified transitions are often called “deltas”. Similarly for V. A functor G : S / V maps states of S to states of V — S is sent to GS. Furthermore, being a functor it maps deltas S / S0 in S to deltas GS / GS0 in V. The objects of (G, 1V) are important because, being a pair (S, α : GS / V ), they encapsulate both an object of S and a delta starting at GS. Such a pair is the basic input for a Put operation. The Put operation P itself, in the case of a d-lens, is just a function (not a functor) and it takes such an “anchored delta” (S, α : GS / V ) in V to a delta in S which, by d-PutInc, starts at S. The axioms d-PutId and d-PutPut ensure that the P operation respects composition, including identities. Finally, the axiom d-PutGet ensures that, as expected, the Put operation results in a delta in S which is carried by G to α, the given input delta.

In [ 5 ], we proved that d-lenses compose, that a c-lens as defined there is a special case of d-lens and that their composition is as for d-lenses, and finally that d-lenses are strictly more general than c-lenses. We also proved that d-lenses are certain algebras for a semi-monad.

Furthermore, in [ 6 ] we developed the technique to compose spans of lenses in general. For d-lenses, this specializes to Definition 3. We first need a small but important proposition, and we formally remind the reader about our notations for spans and cospans.

A span is a pair of morphisms, with common domain:

X u

S ????v?

Y Despite the symmetry, such a span is often described as a “span from X to Y ”, and is distinguished from the same two arrows viewed as a span from Y to X. The illustrated span above is often denoted for brevity’s sake u : X o S / Y : v and, when X, S and Y are understood or easily derived, we sometimes just refer to it as the span u, v. The object S is sometimes called the head or peak of the span and the arrows u and v are called the legs of the span. The objects X and Y are, naturally enough, called the feet of the span. Cospans are described and notated in the same way but the arrows u and v are reversed. Finally, if, as sometimes is necessary, a span is drawn upside down, the common domain is still called the head despite being drawn below the feet.

When working with spans it is often necessary to calculate pullbacks. For simplicity of presentation we will usually assume that the pullback has been chosen so that its objects and morphisms are pairs of objects from the categories from which it has been constructed (so, for example, in the diagram below, objects of T are pairs of objects (S, W ) from the categories S and W respectively, with the property that G(S) = H(W ), and similarly for morphisms of T).

Proposition 2 Let G : S / V o W : H be a cospan of functors. Suppose that P : |(G, 1V)| function which, with G, makes the pair (G, P ) a d-lens. Then, in the pullback square in cat: / |S2| is a the functor G0 together with P 0 : |(G0, 1W)| /|T2| defined by P 0((S, W ), β : G0(S, W ) (S, W ) / (S0, W 0) define a d-lens from T to W. /W 0) = (P (S, H(β)), β) : Proof. Note first that P 0 makes sense since H(β) is a morphism HG0(S, W ) / H(W 0) but HG0(S, W ) = GH0(S, W ) = GS so it is in fact a morphism GS / H(W 0). Furthermore we denote the codomain of P (S, H(β)) by S0 so that G(S0) = H(W 0) and thus (S0, W 0) is an object of T. The d-PutInc, d-PutId and d-PutGet conditions on (G0, P 0) are satisfied by construction. The d-PutPut condition follows immediately from d-PutPut for (G, P ).

This means we can talk about the “pullback” of a d-lens along an arbitrary functor, in particular along the Get of another d-lens. This is similar to the situations described in [ 6 ]. The inverted commas around “pullback” are deliberate because the constructed d-lens may not be an actual pullback in the category of d-lenses (the category whose objects are categories and whose arrows S / V are d-lenses from S to V).

S ysKHKsGKs0KsKsKsKs% VT KysKsKsKsGHKs0Ks% W

Definition 3 Suppose that in

GLssss X ysss

S ysKsHsssss T KKKKKKK% S0 K

GKKRKKKK% Y ysssFssLs

KKKFR

KKK% Z the functors GL, GR, FL, and FR are the Gets of d-lenses with corresponding Puts PL, PR, QL, and QR, and T is the pullback of GR and FL. For the “pullback” d-lenses with Gets H and K, denote the Puts by PH and PK .

Then the span composite of the span of d-lenses (GL, PL), (GR, PR) from X to Y with the span of d-lenses (FL, QL), (FR, QR) from Y to Z, denoted

((GL, PL), (GR, PR)) ◦ ((FL, QL), (FR, QR)) is the span of d-lenses from X to Z specified as follows. The Gets are GLH and FRK. The Puts are those for the composite d-lenses (GL, PL)(H, PH ) and (FR, QR)(K, PK ).

In a sense, the composite just defined corresponds to the ordinary composite of spans in a category with pullbacks. In the category of categories, the ordinary span composition of the span GL, GR and with the span FL, FR is the span GLH, FRK. As usual for such composites, the operation is not associative without introducing an equivalence relation and we do so later in this paper. 3

Symmetric delta lenses

A symmetric delta lens (called an “fb-lens” below) is between categories, say X and Y. It consists of a set of synchronizing “corrs”, so named because the make explicit intended correspondences between objects of X and objects of Y, together with “propagation” operations. In the forward direction, given objects X and Y synchronized by a corr r and an arrow x with domain X, the propagation returns an arrow y with domain Y and a corr synchronizing the codomains of x and y. This is made precise in the following definition and is based on definitions in [ 2 ] and [ 3 ]. We denote the domain and codomain of an arrow x by d0(x), d1(x). Definition 4 Let X and Y be categories. An fb-lens from X to Y is M = (δX, δY, f, b) : X ←→ Y specified as follows. The data δX, δY are a span of sets δX : |X| o

RXY / |Y| : δY An element r of RXY is called a corr. For r in RXY, if δX(r) = X, δY(r) = Y the corr is denoted r : X ↔ Y . The data f and b are operations called forward and backward propagation: f : Arr(X) ×|X| RXY

/ Arr(Y) ×|Y| RXY b : Arr(Y) ×|Y| RXY / Arr(X) ×|X| RXY where the pullbacks (also known as fibered products) mean that if f(x, r) = (y, r0), we have d0(x) = δX(r), d1(y) = δY(r0) and similarly for b. We also require that d0(y) = δY(r) and δX(r0) = d1(x), and the similar equations for b.

Furthermore, we require that both propagations respect both the identities and composition in X and Y, so that we have: r : X ↔ Y

implies f(idX , r) = (idY , r) and b(idY , r) = (idX , r) and and f(x, r) = (y, r0) and f(x0, r0) = (y0, r00) imply f(x0x, r) = (y0y, r00) b(y, r) = (x, r0) and b(y0, r0) = (x0, r00) imply b(y0y, r) = (x0x, r00)

For examples of fb-lenses we refer the reader to [ 2 ].

Definition 5 Let M = (δXR, δYR , fR, bR) and M 0 = (δYS, δZS, fS, bS) be two fb-lenses. We define the composite fb-lens M 0M = (δX, δZ, f, b) as follows. Let TXZ be the pullback of categories in Let δX = δXRδ1 : TXZ / X and δZ = δZSδ2. The operations for M 0M are defined as follows. Denote fR(x, r) = (y, rf ), fS(y, s) = (z, sf ) and bS(z, s0) = (y, sb), bR(y, r0) = (x, rb). Then

f(x, (r, s)) = (z, (rf , sf )) and b(z, (r0, s0)) = (x, (rb, sb)) If f(x, r) = (y, r0) and b(y0, r) = (x0, r00), we display instances of the propagation operations as: r f RXYδKYRKKKK%

TXZ |Y|

KKKδ2

KK% ss ysssδY

S

SYZ X o r s

/ Z shows that the arities are correct for f in the forward direction. That is, we have

It is easy to show that the f and b just defined respect composition and identities in X and Z and we record:

Proposition 6 The composite M 0M just defined is an fb-lens from X to Z.

We note that because it is defined using a pullback, this construction of the composite of a pair of fb-lenses is not associative, and when we later define a category of fb-lenses the arrows will be equivalence classes of fb-lenses.

Next we define two constructions relating spans of d-lenses with fb-lenses.

We first consider a span of d-lenses. Let L = (GL, PL) where GL : S / V and K = (GK , PK ) where GK : S / W be (a span of) d-lenses.

Construct the fb-lens ML,K = (δV, δW, f, b) as follows: – the corrs are RV,W = |S| with δVS = GLS and δWS = GK S; – forward propagation f for v : V / V 0 and S : V ↔W is defined by f(v, S) = (w, S0) where w = GK (PL(S, v)) and S0 is the codomain of PL(S, v); – backward propagation b is defined analogously.

Lemma 7 ML,K is an fb-lens.

Proof. Identity and compositionality for ML,K follow from functoriality of the Gets for L and K and the d-PutId and d-PutPut equations in Definition 1.

In the other direction, suppose that M = (δV, δW, f, b) is an fb-lens from V to W with δV : |V| o

R / |W| : δW

We now construct a span of d-lenses LM : V o S / W : KM from V to W. The first step is to define the head S of the span. The set of objects of S is the set R of corrs of M . The morphisms of S are defined as follows: For objects r and r0, S(r, r0) = {(v, w) | d0v = δV(r), d1v = δV(r0), d0w = δW(r), d1v = δW(r0)} (where we write, as usual, S(r, r0) for the set of arrows of S from r to r0). Thus an arrow may be thought of as a formal square:

V o v V 0 o r r0 / W

w / W 0

Composition is inherited from composition in V and W at boundaries, or more precisely, for (v, w) ∈ S(r, r0) and (v0, w0) ∈ S(r0, r00) we define:

(v0, w0)(v, w) = (v0v, w0w) in S(r, r00). The identities are pairs of identities. It is easy to see that S is a category.

Next we define the d-lens LM to be the pair (GL, PL) where we define GL : S / V on objects by δV, and on arrows by projection, that is GL(v, w) = v. The Put for LM , PL : |(GL, 1V)| / |S2|, is defined on objects (r, v : GL(r) / V 0) of the category (GL, 1V) by PL(r, v) = (v, π0f(v, r)) which is indeed an arrow of S from r to π1f(v, r). (As is usual practice, we write π0 and π1 for the projection from any pair onto its first and second factors respectively.) We define KM = (GK , PK ) similarly.

Lemma 8 LM = (GL, PL) and KM = (GK , PK ) is a span of d-lenses.

Proof. GL and GK are evidently functorial. We need to show that PL and PK satisfy (i)-(iv) of Definition 1. These follow immediately from the properties of of the fb-lens M .

The two constructions above are related. One composite of the constructions is actually the identity.

Proposition 9 For any fb-lens M , with the notation of the constructions above

M = MLM ,KM Proof. By inspection, the corrs and δ’s of MLM ,KM are those of M . Further, it is easy to see that, for example, the forward propagation of MLM ,KM is identical to that of M .

However, the other composite of the constructions above, namely the span of d-lenses LML.K , KML.K is not equal to the original span L, K (because the arrows of the original S have been replaced by the formal squares described above). We have yet to consider the appropriate equivalence for spans of d-lenses, and we do so now. We will see that LML.K , KML.K is indeed equivalent to L, K. 4

Two equivalence relations

Our first equivalence relation is on spans of d-lenses from X to Y.

Suppose that are such spans.

The functor Φ : S / S0 is said to satisfy conditions (E) if: (1) G0LΦ = GL and G0RΦ = GR

X o (GL,PL)

(GR,PR) S / Y and

X o (G0L,P L0)

(G0R,P R0) S0

/ Y (2) Φ is surjective on objects

To simplify describing ≡Sp we now prove some properties of functors satisfying conditions (E).

Lemma 11 A composite of d-lens span morphisms satisfying (E) also satisfies (E).

Proof. Suppose that we have spans of d-lenses (GL, PL), (GR, PR) and (G0L, P L0), (G0R, P R0) as above, and a third such span is:

X o (G0L0,P L00)

S00 (G0R0 ,P R00) / Y Suppose Φ : S /S0 and Φ0 : S0

/S00 satisfy (E). Properties (1) and (2) for Φ0Φ are immediate. We show the P L0 Φ0(Φ(S)) = S00, we have P L00(S00, G0L0 S00 α / X) = Φ0P L0(Φ(S), and G0LΦ(S) as required. part of property (3) for Φ0Φ. Suppose Φ0ΦS = S00 and consider P L00(S00, G0L0 S0 α / X). By (E) for Φ and Φ0, since α / X) = Φ0ΦPL(S, GLS α / X)

Suppose that Φ satisfies (E). When ΦS = S0 it follows that GLS = G0LΦS = G0LS0, which we will use below. Note that if Φ were the Get of a d-lens (although it need not be) then it would be surjective on arrows by the d-PutGet equation, but not necessarily surjective on hom sets.

Lemma 12 Suppose once again that (GL, PL), (GR, PR), (G0L, P L0), (G0R, P R0) and (G0L0 , P L00), (G0R0 , P R00) are spans of d-lenses as above. Let Φ : S / S0 o S00 : Φ0 be the functors in a cospan of span morphisms satisfying (E). Let

S yKssΨsssss T KKKKΨK0K% S00

KΦKKKKK% S0 yssssΦs0s be a pullback in cat. Then there is a span of d-lenses X o / Y defined by GTL = GLΨ and PLT ((S, S00), GTL(S, S00) α / X) = (S

P L00(S00,α)

/ W 00) (GTL,PLT ) PL(S,α)

T / W, S00 (GTR,PRT ) and similarly for (GTR, PRT ). Moreover, Ψ and Ψ0 satisfy (E).

PLT ((S, S00), GTL(S, S00)

P L00(S00,α)

Proof. The first point is that (GTL, PLT ) and (GTR, PRT ) actually are d-lenses. We need to know that PLT is

well-defined. Since (S, S00) is an object of the pullback T, we know that Φ(S) = Φ0(S00) = S0, say. We want PL(S,α) α / X) to be an arrow of T, so we need to show that Φ(S / W ) is equal to Φ0(S00 / W 00). However both are equal to P L0(S0, α) since both Φ and Φ0 satisfy (E). Thus furthermore, (W, W 00) is an object of T and using this for d-PutPut each of the required d-lens equations is easy to establish.

Next, we show that Ψ and Ψ0 satisfy (E). First of all, the Gets commute by definition. Moreover, both Ψ and Ψ0 are surjective on objects because Φ and Φ0 are so. It remains to check property (3) for Ψ and Ψ0. We need to show that whenever Ψ(S, S00) = S, we have PL(S, GLS α / U ) = Ψ(PLT ((S, S00), GTL(S, S00) α / U )) and this follows immediately from the definitions of Ψ and PLT . (Notice that for S = Ψ(S, S00) we have GLS = G0LΦS = G0LΦ0(S00) = G0L0 (S00) and thus P L00(S00, G0L0 S00 α / U ) is well-defined.) Similarly Ψ0 satisfies (3).

Corollary 13 Zig-zags of span morphisms satisfying (E) reduce to spans of span morphisms satisfying (E).

A zig-zag is any string of arrows (ignoring the direction of the indidual arrows so that neighbouring arrows might be connected head to head or tail to tail as well as tail to head). It follows that any proof that two spans of d-lenses are ≡Sp equivalent can be reduced to a single span Ψ, Ψ0 of span morphisms satisfying (E).

The second equivalence relation we introduce is on the set of fb-lenses from X to Y. Recall that Diskin et al [ 3 ] defined symmetric delta lenses (our fb-lenses), but they did not consider composing them. Like Hoffman et al [ 4 ] they would find that they need to consider equivalence classes of their symmetric delta lenses in order for the appropriate composition to be associative. Also like Hoffman et al, there is a need for an equivalence among their lenses to eliminate artificial differences. In fact, defining an equivalence to restore associativity is easy. Choosing the correct equivalence to eliminate the artificial differences is more delicate. And what do we mean by “atificial differences”? Symmetric lenses of various kinds include hidden data — the complements of Hoffmann et al and the corrs of Diskin et al are examples. The hidden data is important for checking and maintaining consistency, but different arrangements of hidden data with the same overall effect should not be counted as different symmetric lenses.

We now introduce such a relation on the set of fb-lenses from X to Y.

Definition 14 Let L = (δX, δY, f, b) and L0 = (δX0, δY0, f0, b0) be two fb-lenses (from X to Y) with corrs RXY, RX0Y. We say L ≡fb L0 iff there is a relation σ from RXY to RX0Y with the following properties: 1. σ is compatible with the δ’s, i.e. rσr0 implies δXr = δX0r0 and δYr = δY0r0 2. σ is total in both directions, i.e. for all r in RXY, there is r0 in RX0Y with rσr0 and conversely.

3. for all r, r0, x an arrow of X, if rσr0 and δXr is the domain of x then the first components of f(x, r) and

f0(x, r0) are equal and the second components are σ related, i.e. π0f(x, r) = π0f0(x, r0) and π1f(x, r)σπ1f0(x, r0)

4. the corresponding condition for b, i.e. for all r, r0, y an arrow of Y, if rσr0 and δXr is the domain of x then

π0b(y, r) = π0b0(y, r0) and π1b(y, r)σπ1b0(y, r0) Lemma 15 The relation ≡fb is an equivalence relation.

Proof. For reflexivity take σ to be the identity relation; for symmetry take the opposite relation for σ; for transitivity, the composite relation is easily seen to satisfy conditions 1. to 4.

Lemma 16 For L, L0 as in the definition above, consider a surjection ϕ : RXY and satisfying the following conditions: / RX0Y compatible with the δ’s • for corrs r, r0, and an arrow x of X, if ϕ(r) = r0 and δXr is the domain of x then the first components of f(x, r) and f0(x, r0) are equal and the second components are ϕ related, i.e. π0f(x, r) = π0f0(x, r0) and ϕ(π1f(x, r)) = π1f0(x, r0) • the corresponding condition for b, i.e. for all r, r0, y an arrow of Y, if ϕ(r) = r0 and δXr is the domain of x then π0b(y, r) = π0b0(y, r0) and ϕ(π1b(y, r)) = π1b0(y, r0) The collection of such surjections (viewed as relations) generates the equivalence relation ≡fb.

Proof. To see that ≡fb is generated by such surjections, consider the span tabulating the relation σ in ≡fb viz.

RXY o σ / RX0Y.

Notice that each leg is a surjection satisfying the conditions of the lemma. Conversely, any zig-zag of such surjections defines a relation which is easily seen to satisfy the conditions of Definition 14.

Remark 17 Although ≡fb is generated by zig-zags of certain surjections, we have just seen that any such zig-zag

can be reduced to a single span of such surjections between sets of corrs.

Proposition 18 Suppose that M ≡fb M 0 are fb-lenses from X to Y equivalent by a generator for ≡fb, i.e. a surjection ϕ : RXY / RX0Y. Then (LM , KM ) ≡Sp (LM0 , KM0 ) as spans of d-lenses from X to Y. Proof. We first define Φ : S / S0 on objects by ϕ. Notice that Φ is surjective on objects since ϕ is a surjection. To define Φ on arrows of S, consider an arrow of S. Its image under Φ is defined to be the arrow

X o x X0 o X o x X0 o r r0 ϕ(r) ϕ(r0) / Y / Y 0 / Y / Y 0 y y which is an arrow of S0 since ϕ is compatible with the δs. This Φ is evidently functorial and commutes with the Gets. It remains to show that Φ satisfies condition (3) of (E), that is, whenever Φ(r) = r0, P L0(r0, G0Lr0 x / X0) = ΦPL(r, GLr x / X0) (with the similar equation holding for P K0 ).

Now, when r0 = Φ(r), we have

P L0(r0, x) as required. Similarly for P K0 .

Proposition 19 Suppose that (L, K) ≡Sp (L0, K0) as spans of d-lenses from X to Y are made equivalent by a generator for ≡Sp, i.e. a functor Φ : S / S0 satisfying conditions (E). Then ML,K ≡fb ML0,K0 as fb-lenses from X to Y.

Proof. Let ϕ be the object function of Φ. Since Φ commutes with the Gets, ϕ is compatible with the δ’s.

We need to show that ϕ satisfies the conditions in Lemma 16. Suppose Φ(S) = S0 and GL(S) is the domain of x. Then π0f(x, S) and ϕπ1f(x, S) as required. Similarly for the equations involving b. 5

Two categories of lenses

The collections of lenses so far discussed do not form categories since their composition is not associative. We are going to use the equivalence relations of the previous section to resolve this, but first we show that the equivalence relations respect the composites defined above, that is they are “congruences”. Proposition 20 Suppose that M = (δX, δY, fR, bR), M 0 = (δX0, δY0, fR0 , bR0 ) and N = (δYS, δZ, fS , bS ) are fblenses (see the diagram below in which RXY, RX0Y and SYZ are the corresponding corrs). Further, suppose ϕ : RXY / RX0Y is a generator of ≡fb. Thus M ≡fb M 0. Then N M ≡fb N M 0.

Proof. The composite N M has as corrs the pullback TXZ as in Definition 5, and similarly N M 0 has corrs T X0Z .

|X|

δ1

RXY? o δX ?????δ?Y?

ϕ |Y| o _???? ? δX0 ??? δY0

RX0Y o δ0 1

TXZ? T X0Z ??? δ2 ? ? δYS ??  S?YZ    δ20 δZ / Z | |

In order to show that N M ≡fb N M 0, we construct ϕ0 : TXZ / T X0Z. This is straightforward using the

universal property of the pullback T X0Z, since δY0ϕδ1 = δYSδ2.

To finish, we need to check that ϕ0 satisfies the four requirements of Definition 14.

Compatibility with δs is easy when we note that ϕδ1 = δ10ϕ0 and δ20ϕ0 = δ2.

The function ϕ0 is a total relation in both directions since it is surjective. To see that ϕ0 is surjective, note that any element of T X0Z can be thought of as a pair (r0, s) compatible over Y, and since ϕ is surjective, there exists an r in RXY, necessarily compatible with s, such that ϕ0(r, s) = (ϕ(r), s) = (r0, s).

Let f be the forward propagation of the composite N M , as defined in Definition 5, and let f0 be the forward propagation of the composite N M 0. Suppose r0 = ϕ(r) and thus (r0, s) = ϕ0(r, s). We need to show that the first components of f(x, (r, s)) and f0(x, (r0, s)) are equal and that ϕ0 takes the second component of f(x, (r, s)) to the second component of f0(x, (r0, s)).

The first component of f(x, (r, s)) is π0fS (π0fR(x, r), s), while the first component of f0(x, (r0, s)) is π0fS (π0fR0 (x, r0), s), and these are equal since ϕ is a generator of ≡fb implies π0fR(x, r) = π0fR0 (x, ϕ(r)).

The second component of f(x, (r, s)) is (π1fR(x, r), π1fS (π0f R(x, r), s)), while the second component of f0(x, (r0, s)) is (π1fR0 (x, r0), π1fS (π0f R0 (x, r0), s)), and ϕ0 of the first equals the second since, as before, π0fR(x, r) = π0fR0 (x, ϕ(r)).

The same arguments work for b and b0.

Proposition 21 Suppose that M = (δX, δYR , fR, bR), N = (δY, δZ, fS , bS ) and N 0 = (δY0, δZ0, fS0 , bS0 ) are fblenses (see the diagram below in which RXY, SYZ and SY0Z are the corresponding corrs). Further, suppose ϕ : SYZ / SY0Z is a generator of ≡fb. Thus N ≡fb N 0. Then N M ≡fb N 0M . Proof. The composite N M has as corrs the pullback TXZ as in Definition 5, and similarly N 0M has corrs T X0Z .

|X| o δX

TXZ δ1 

  δYR / |Y| RXY_?δ?10? ???? _?? ?

T X0Z δ2 / SYZ? δY 

 

ϕ ?? δY0 ??? δ0 / SY0Z 2 ??? δZ ? ? ? ?

Z ? | |  δZ0

The proof follows the same argument as in the previous proposition.

Theorem 22 Equivalence classes for ≡fb are the arrows of a category, denoted fbDLens. Proof. We first note that Propositions 20 and 21 ensure that composition is well-defined independently of choice of representative. There is an identity fb-lens with obvious structure which acts as an identity for the composition. It remains only to note that associativity follows by standard re-bracketing of iterated pullbacks.

The re-bracketing function is the ϕ for an ≡fb equivalence.

Proposition 23 Suppose that (GL, PL), (GR, PR), (G0L, P L0), (G0R, P R0), (FL, QL), and (FR, QR) are d-lenses whose Gets are shown in the diagram below. Further, suppose Φ : S / S0 is a functor satisfying properties (E). Thus the span (GL, PL), (GR, PR) is ≡Sp to the span (G0L, P L0), (G0R, P R0). Then the two possible span composites are equivalent, that is

((GL, PL), (GR, PR)) ◦ ((FL, QL), (FR, QR)) ≡Sp ((G0L, P L0), (G0R, P R0)) ◦ ((FL, QL), (FR, QR)). Proof. The top composite span of d-lenses in the diagram below has head T, the pullback of GR and FL (see Definition 3), similarly T0 is the head of the bottom span composite.

X

GL   _??

??? G0L ???

H

S o  ?????GR

??? Φ ? Y o     G0R  S0 o

H0

T0 T ?????K???

FL ? R     K0 

FR / Z

In order to show the claimed equivalence, we construct a functor Φ0 : T / T0. Since G0RΦH = FLK, Φ0 is defined by applying the universal property of the pullback T0.

Since T and T0 are pullbacks of functors, their objects can be taken to be pairs of objects from S and R, respectively S0 and R. Similarly, their arrows can be taken to be pairs. Also H and K, respectively H0 and K0 can be taken to be projections. We can now explicitly describe the action of Φ0 on an arrow of T as Φ0(t0, t1) = (Φt0, t1).

As in Definition 3, we denote the Puts of the lenses whose Gets are H and K by PH and PK . Similarly for H0 and K0. Denote the composite lens (GL, PL)(H, PH ) by (G, P ) and similarly (G0, P 0) = (G0L, P L0)(H0, PH0 ).

We need to show that Φ0 satisfies the conditions (E). By its construction Φ0 commutes with the Gets, and is surjective on objects.

It remains to show that whenever Φ(S, R) = (S0, R0) (which implies that R = R0 and Φ(S) = S0) we have and

γ Q0((S0, R0), FRK0(S0, R0) / Z0) = Φ0Q((S, R), FRK(S, R) γ / Z0) We begin by proving the first equation immediately above.

P L0(S0, G0L(S0) α / X0) = ΦPL(S, GL(S) α / X0). We calculate We know that whenever Φ(S) = S0, The first step is merely that H0 is a projection; the second is the definition of P 0 as the Put of the composite lens whose Get is G0LH0; the third is the definition of PH0 (see Proposition 2); the fourth uses R0 = R and the hypothesis stated just before the equations; the fifth follows since Φ commutes with GR and G0R and the definition of Φ0; the sixth is the definition of PH (see Proposition 2); the last is the definition of P as the Put of the composite lens whose Get is GLH.

To establish the second equation, suppose Φ0(S, R) = (S0, R0), whence R = R0 and Φ(S) = S0, and so because Φ satisfies conditions (E), we have

β P R0(S0, G0R(S0) / Y 0) = ΦPR(S, GR(S) β / Y 0) and since GR(S) = G0RΦ(S) = G0R(S0), the right hand side can be written as ΦPR(S, G0R(S0) calculate / Y 0). We γ Q0((S0, R0), FRK0(S0, R0) / Z0) =

PK0 ((S0, R0), QR(R0, FR(R0) Before continuing the calculation, we simplify by defining β by (G0R(S0) / Y 0) = FLQR(R0, FR(R0) / Z0) = FLQR(R, FR(R) γ / Z0) after noting that G0R(S0) is the domain of FLQR(R0, FR(R0)γZ0) since the T 0 pullback square commutes. Now, continuing the calculation above: γ β γ

/ Z0)) = (P R0(S0, FLQR(R0, FR(R0)

/ Z0)), QR(R0, FR(R0) β β β = (P R0(S0, G0R(S0)

/ Y 0, QR(R0, FR(R0) = (ΦPR(S, GR(S)

/ Y 0, QR(R0, FR(R0) = (ΦPR(S, G0R(S0) / Y 0, QR(R, FR(R) γ γ γ γ / Z0))) / Z0))) / Z0))) Φ0(PR(S, FLQR(R, FR(R)

/ Z0), QR(R, FR(R) Φ0PK ((S, R), QR(R, FR(R)

γ Φ0Q((S, R), FRK(S, R) γ / Z0) / Z0), QR(R, FR(R) β γ / Z0))

γ γ γ / Z0))) / Z0)) The first step uses that K0 is a projection and the definition of Q0 as the Put of the composite lens whose Get is F R0K0 ; the second is the definition of PK0 (see Proposition 2); the third is the definition of β above; the fourth uses the hypothesis stated before the equations; the fifth uses R = R0 and the note just before the equations; the sixth uses the definitions of Φ0 and β; the seventh is the definition of PK (see Proposition 2); the last is the definition of Q as the Put of the composite lens whose Get is FRK.

Like Propositions 20 and 21, there is a reflected version of Proposition 23, showing that equivalent spans of d-lenses when composed on the left with another span of d-lenses are equivalent.

((GL, PL), (GR, PR)) ◦ ((FL, QL), (FR, QR)) ≡Sp ((GL, PL), (GR, PR)) ◦ ((F L0, Q0L), (F R0, Q0R)). Theorem 25 Equivalence classes for ≡Sp are the arrows of a category, denoted SpDLens. Proof. We first note that Proposition 23 and Proposition 24 ensure that composition is well-defined independently of choice of representative. There is a span of identity d-lenses which acts as the identity for the composition. Again, associativity follows by standard re-bracketing of iterated pullbacks of categories. The re-bracketing functor is the Φ for an ≡Sp equivalence. 6

An isomorphism of categories of lenses

Now that we have the categories fbDLens and SpDLens, we can extend the constructions of Section 3 to functors on them.

Definition 26 For the ≡fb equivalence class [M ] of an fb-lens M , let A([M ]) be the ≡Sp equivalence class of, in the notation of Lemma 8, the span LM , KM .

Proposition 27 A is the arrow function of a functor, also denoted A, from fbDLens to SpDLens.

Proof. We need to show that A preserves identities and composition.

For the former denote by MX the identity fb-lens on a category X. We begin by noticing that the category Xp at the head of the span of d-lenses constructed from MX has as its objects exactly those of X. Its arrows from X to X0 are arbitrary pairs of X arrows, both of which are from X to X0. Define the functor Φ from the head X of the identity span on X to Xp by sending an arrow x of X to the pair of arrows (x, x). This functor Φ satisfies conditions (E), and so A([MX]) = [X] as required.

Let M and M 0 be a composable pair of fb-lenses from X to Y and Y to Z respectively. The composite fb-lens M 0M has as corrs compatible pairs of corrs, one from M and one from M 0 (see Definition 5). The head S of the span of d-lenses constructed from M 0M has objects compatible pairs of corrs and as arrows from compatible corrs (r1, r2) to compatible corrs (r10, r20), pairs of arrows, one from X and one from Z as shown X o x X0 o X o x X0 o r1 r0 1 r1 r0 1 On the other hand, the span composite of the spans constructed from M and M 0 has as head a category T whose objects are pairs of compatible corrs from M and M 0 respectively. The arrows of T are triples of arrows (x, y, z) as shown Define the functor Φ from T to S by sending the triple of arrows (x, y, z) to the pair of arrows (x, z). This functor Φ satisfies conditions (E), and so A([M 0M ]) = A([M 0])A([M ]) as required.

Definition 28 For the ≡Sp equivalence class [L, K] of a span of d-lenses L, K, let S([L, K]) be the ≡fb equivalence class of, in the notation of Lemma 7, the fb-lens ML,K .

Proposition 29 S is the arrow function of a functor, also denoted S, from SpDLens to fbDLens. / Y o / Y 0 o / Z / Z0

z / Z

z / Z0

Proof. We need to show that S preserves identities and composition.

Unlike the previous proof, the preservation of identities and composition is “on the nose”. That is, the construction applied to the identity gives precisely the identity fb-lens. Moreover, with judicious choice of pullbacks, the construction applied to the composite of two composable spans of d-lenses is the composite of the fb-lenses constructed from each of the spans.

Thus S preserves the equivalence class of the identity span and S([L1, K1][L2, K2]) = S([L1, K1])S([L2, K2]). Theorem 30 The functors A and S are an isomorphism of categories SpDLens ∼= fbDLens.

Proof. We need to show that the composites AS and SA are identities. Recall first that both A and S have

identity functions as object functions. Considering the arrows, Proposition 9 shows that SA is the identity functor. We now consider AS.

For a span L, K of d-lenses between X and Y, using the notation of Lemmas 7 and 8, AS([L, K]) = [LML,K , KML,K ], so we consider the span LML,K , KML,K of d-lenses whose Gets and Puts we denote by FL, QL and FK , QK respectively. The head of the span is a category we denote SL,K whose objects are the same as the objects of S, the head of the span L, K. We define an identity on objects functor Φ : S / SL,K on arrows by Φ(s) = (GL(s), GK (s)) (recalling that arrows of SL,K are pairs of arrows from X and Y, respectively). We finish by showing that Φ satisfies conditions (E), and so witnesses AS([L, K]) = [L, K].

It remains to show that Φ satisfies conditions (E). Being identity on objects, Φ is certainly surjective on objects, and it commutes with the Gets by its construction. For condition (3), given an object S0 of SL,K , an object S of S such that ΦS = S0, and an arrow α : GL(S) = FL(S0) / X0 in X, we have PL(S, α) an arrow of S. We need to show that ΦPL(S, α) = QL(S0, α). Since ΦS = S0 we have S = S0. Now QL(S0, α) = QL(S, α) = (α, π0f(α, S)), for the forward propagation f of ML,K constructed as in Lemma 7. By that construction π0f(α, S) = GK (PL(S, α)). But ΦPL(S, α) = (GL(PL(S, α)), GK (PL(S, α))) = (α, π0f(α, S)) = QL(S0, α).

Thus, since AS([L, K]) = [L, K], AS is the identity. 7

Conclusions

Because asymmetric delta lenses and symmetric delta lenses are so useful in applications, it is important that we understand them well and provide a firm mathematical foundation. This paper provides such a foundation by formalizing fb-lenses and their composition, including determining the equivalence required on fb-lenses for the composition to be well-defined and associative. Furthermore the resultant category fbDLens of fb-lenses is equivalent, indeed isomorphic, to the category SpDLens of equivalence classes of spans of d-lenses.

This last result, the isomorphism between fbDLens and SpDLens, furthers the program to unify the treatment of symmetric lenses of type X as equivalence classes of spans of asymmetric lenses of type X, carrying that program for the first time into category-based lenses. (And that extension came with a surprise — see below.)

Naturally a unified treatment needs to be tested extensively on a wide range of lens types, and more work remains. The present paper is an important step in the program, and provides a reason to be hopeful that the unification is close at hand. Indeed, with this work the program encounters the important category-based lenses for the first time and that substantially widens the base of unified examples.

We end with a distilled example. It shows in a simplified way why the equivalence used here, based on conditions (E), needs to be coarser than an equivalence generated by lenses commuting with the spans though it remains compatible with the earlier work. Thus it is also a coarser equivalence relation than might have been expected based on [ 6 ].

The figure below presents two spans of d-lenses. The categories at the head and feet of the spans have been shown explicitly. In three cases the category has a single non-identify morphism called variously γ, δ and while in the fourth case the category has two distinct nonidentity morphisms denoted α and β. In all cases objects and identity morphisms have not been shown. In three cases there are just two objects, while in the fourth case there are three, with a single object serving as the domain of both α and β. γ vlllllll ↓ hRRRRRRRRRR ↓ Φ llllllllll6 ↓

The arrows displayed in both spans represent (the Gets of) d-lenses. In the lower span the d-lenses are simply identity d-lenses (the Gets are isomorphisms sending to γ in the left hand leg, and to δ in the right hand leg). Both of the Puts are then determined. The upper span is made up of two non-identity d-lenses. In both cases the Gets send both α and β to the one non-identity morphism (γ in the left hand leg and δ in the right hand leg). We specify the Puts for the upper span (eliding reference to objects in the Puts’ parameters since they can be easily deduced): PL(γ) = α and PR(δ) = β for the left and right Puts respectively.

Notice that Φ, the functor that sends both α and β to , satisfies conditions (E) showing, as expected, that the two spans are equivalent. After all, if one traces through the forward and backward behaviours across the two spans the results at the extremities are in all cases the same, though the intermediate results at the heads of the spans differ. However, Φ cannot be the Get of a lens which commutes with the other four d-lenses. Indeed, to commute with the left hand lenses would require PΦ( ) = α while to commute with the right hand lenses would require PΦ( ) = β, but α 6= β. 8

Acknowledgements

This paper has benefited from valuable suggestions by anonymous referees. The authors are grateful for the careful and insightful refereeing. In addition, the authors acknowledge with gratitude the support of NSERC Canada and the Australian Research Council. Coalgebraic Aspects of Bidirectional Computation Faris Abou-Saleh1

James McKinna2

Jeremy Gibbons1

Abstract

We have previously (Bx, 2014; MPC, 2015) shown that several statebased bx formalisms can be captured using monadic functional programming, using the state monad together with possibly other monadic effects, giving rise to structures we have called monadic bx (mbx). In this paper, we develop a coalgebraic theory of state-based bx, and relate the resulting coalgebraic structures (cbx) to mbx. We show that cbx support a notion of composition coherent with, but conceptually simpler than, our previous mbx definition. Coalgebraic bisimulation yields a natural notion of behavioural equivalence on cbx, which respects composition, and essentially includes symmetric lens equivalence as a special case. Finally, we speculate on the applications of this coalgebraic perspective to other bx constructions and formalisms. 1 Many scenarios in computer science involve multiple, partially overlapping, representations of the same data, such that whenever one representation is modified, the others must be updated in order to maintain consistency. Such scenarios arise for example in the context of model-driven software development, databases and string parsing [ 6 ]. Various formalisms, collectively known as bidirectional transformations (bx), have been developed to study them, including (a)symmetric lenses [ 8, 16 ], relational bx [30], and triple-graph grammars [27].

In recent years, there has been a drive to understand the similarities and differences between these formalisms [ 18 ]; and a few attempts have been made to give a unified treatment. In previous work [5, an extended abstract] and [1, to appear], we outlined a unified theory, with examples, of various accounts of bx in the literature, in terms of computations defined monadically using Haskell’s do-notation. The idea is to interpret a bx between two data sources A and B (subject to some consistency relation R ⊆ A × B ) relative to some monad M representing computational effects, in terms of operations, getL : MA and setL : A → M (), and similarly getR, setR for B , which allow lookups and updates on both A and B while maintaining R. We defined an effectful bx over a monad M in terms of these four operations, written as t : A ⇐⇒M B , subject to several equations in line with the Plotkin–Power equational theory of state [23]. The key difference is that in a bidirectional context, the sources A and B are interdependent, or entangled : updates to A (via setL) should in general affect B , and vice versa. Thus we must abandon some of the Plotkin–Power equations; for instance, one no longer expects setL to commute with setR. To distinguish our earlier effectful bx from the coalgebraic treatment to be developed in this paper, we will refer to them as monadic bx, or simply mbx, from now on.

We showed that several well-known bx formalisms may be described by monadic bx for the particular case of the state monad, MS X = S → (X × S ), called State S in Haskell. Moreover, we introduced a new class of bx: monadic bx with effects, expressed in terms of the monad transformer counterpart TSM to MS (called StateT S M in Haskell), where TSM X = S → M (X × S ) builds on some monad M , such as I/O. We defined Copyright c by the paper’s authors. Copying permitted for private and academic purposes.

In: A. Cunha, E. Kindler (eds.): Proceedings of the Fourth International Workshop on Bidirectional Transformations (Bx 2015), L’Aquila, Italy, July 24, 2015, published at http://ceur-ws.org • If m is CM , there is no choice: we must return CN to be correct. • If m = xm and n = (b, xn) are both drawn from the copies of R, we must return (b0, xm) for some b0 ∈ B.

If in fact xm = xn, hippocraticness tells us we must return exactly n. Otherwise, we could legally return a result which is on the other branch from n, that is, flip the boolean as well as changing the real number. It is easy to argue, though, that to do so violates any reasonable least change principle, since the boolean-flipping choice gives us a change in the model which is larger by our chosen metric, with no obvious prospect for any compensating advantage. Let us suppose we agree not to do so. • The interesting case is →−R(xm, CN ) for real xm. We must return either (>, xm) or (⊥, xm); neither correctness nor hippocraticness place any further restrictions, and when we look at one restoration scenario in isolation, our metric does not help us make the choice, either. We could, for example: 1. pick a boolean value and always use that, e.g. →−R(xm, CN ) = (>, xm) for all xm ∈ R; 2. return (>, xm) if xm ≥ 0, (⊥, xm) otherwise; or we could even go for bizarre behaviour such as 3. return (>, xm) if xm is rational, (⊥, xm) otherwise.

All of these options for →−R(xm, CN ) will turn R into a correct and hippocratic bx. It seems intuitive that these are in decreasing order of merit from a strong least surprise point of view. Imagine that the developers on the

M side were not quite sure whether they wanted to put one real number, or another very close to it. The danger

that their choice on this matter has determined which branch the N model ends up on, “merely because” the state of the N model at the moment they chose to synchronise “happened” to be CN , increases as we go down the list of options.

From the point of view of weak least surprise, however, there is no difference between the options, at least for

a sufficiently small notion of “small change”. For, if R(m, n) holds, and then m is changed to m0 by a change that has size greater than 0 but less than 1, it follows that neither m nor n can be the special points CM and CN : there are no other models close to CM , so m has to be one of the real number points, say xm ∈ R, m0 has to be a nearby real number xm0 , and from consistency it follows that n must be (b, xm) for some b. We have already agreed that the result of →−R(m0, n) should be (b, xm0 ).

The key point here is that only in the first option is →−R( , CN ) : M → N a continuous function in the usual sense of mathematics; in the middle option this function has a discontinuity, while in the final option it is discontinuous everywhere except CM . This motivates our considerations of continuity in Section 7. Note that not only is ({CM }, {CN }) a subspace pair on which any of these variants is continuous (trivially, any pair of consistent states always forms a subspace pair), so is (M \ {CM }, N \ {CN }). This illustrates the potential for a future bx tool to use subspace pairs to warn developers of discontinuous behaviour.

The next example is boring from the point of view of consistency restoration, as consistency is a bijective relation here so there is no choice about how to restore consistency, but it will allow us to demonstrate a technical point later.

Example 4.8 (continuousNotHolderContinuous) Our model spaces are subsets of real space with the stan

dard metric. Let M ⊆ R2 comprise the origin, which we label CM , together with the unit circle centred on the origin, parameterised by θ running over the half-open interval (0, 1]. Let N ⊆ R be {0} ∪ [1, +∞). We say that the origin CM is consistent only with 0, while the point on the unit circle at parameter θ is consistent only with 1/θ. 5

Ordering changes

If we wish to identify changes that are defensibly “least”, the most basic thing we can do is to identify the possible changes that could restore consistency, place a partial order on these changes, and insist that the chosen change be minimal. Of course this does not solve anything, and any solution to our problem can be cast in this setting.

Meertens [ 14 ] requires structure stronger than this, but weaker than a metric on the model sets. For any model m ∈ M he assumes given a reflexive and transitive relation on M , notated x vm y and read “x is at least as close to m as y is”, satisfying the property that m vm x for any m, x. If M is a metric space of course we derive this relation from the metric; most of Meertens’ examples do actually use a metric, typically size of symmetric difference of sets. He takes it as axiomatic that consistency restoration should give a closest consistent model (according to the preorder), and that it should do so deterministically; much of his paper is devoted to showing how to calculate systematically a biased selector that does this job. Example 4.6 illustrates. Using a similar structure, Macedo et al. [ 13 ] address the tricky question of when it is possible to compose bx that satisfy such a least change condition. As might be expected, they have to abandon determinacy (so that the composition can choose “the right path” through the middle model), and impose stringent additional conditions; fundamentally, there is no reason why we would expect bx that satisfy this kind of least change principle to compose.

Changes as sets of small changes A preorder on changes is a useful starting point in cases where changes are uncontroversially identified with sets of discrete elements to be added to/deleted from a structure; this is usually taken to be the case for databases. We can then generate a preorder on changes from the inclusion ordering on sets, and this gives a way to prefer changes that do not add or delete elements unnecessarily. Even there, a drawback is that if an element is modified, perhaps very slightly, and we must model this as a deletion of one thing and an addition of something very similar, this change appears bigger than it is. Indeed Example 4.5 is a cautionary tale on how such an approach can produce poor results, where models are structured collections of elements, not just sets.

A similar approach is used by TGGs when used in an incremental change scenario; [ 11 ] explains and compares several TGG tools from the point of view of various properties including “least change”. In the context of a set of triple graph grammar rules, we suppose given: a derivation of an integrated triple MS ← MC → MT ; that is, a pair of consistent models MS and MT together with a correspondence graph MC ; a change ΔS to MS . The task is to produce a corresponding change ΔT to MT , updating the auxiliary structures appropriately. What the deltas can be is not formally defined in [ 11 ] but their property (p7)

Least change (F4): An incremental update must choose a ΔT to restore consistency such that there is no subset of ΔT that would also restore consistency, i.e., the computed ΔT does not contain redundant modifications. makes the assumption clear. The issues of handling changes other than as additions plus deletions (mentioned above) and of avoiding creating new elements where old ones could instead of reused (cf Example 4.5 and Example 4.4), are mentioned. Two tools (MoTE and TGG Interpreter) are said to “provide a sufficient means to attain [least change] in practical scenarios” but we are aware of no formal guarantee. 6

Measuring changes

One very natural approach, particularly in the pure state-based setting, is to assume we are given a metric on each model space, and require that the distance between the old, and the chosen new, target models is minimal among all distances between the old target model and any new target model that restores consistency. That is, the effect on their model is as small as it can possibly be, given that consistency must be restored: if this is the case, one argues, it is pointless to insist on more. However, the approach has some limitations, such as failure to compose (essentially because not all triangles are degenerate).

An instance of this approach has been explored and implemented by Macedo and Cunha in [ 12 ], although they do not explicitly use the term “metric”. They take as given a pair of models and a QVT-R transformation; the QVT-R transformation is used only to specify consistency, the metric-based consistency restoration explored here being used as a drop-in replacement for the standard QVT-R consistency restoration. The models and consistency relation are translated into Alloy, and the tool searches for the nearest consistent model. Their metric is “graph edit distance”; they also briefly considered allowing the user to define their own notion of edits, which amounts to defining their own metric on the space of models.

This approach is very sensitive to the specific metric chosen, and, because it operates after a model has been translated, the graph edit distance used in [ 12 ] is not a particularly good match for any user’s intuitive idea of distance. There may not be a canonical choice, because different tools for editing models in the same modelling language provide different capabilities. We saw an example of this already in Example 4.2. If my tool provides a simple menu item to make a change that, in your tool, requires many manual steps, is that change small or large? Relative to a specific tool, one can imagine defining a metric by something like “minimal number of clicks and keystrokes to achieve the change”, but this is not satisfying when models are likely to be UML models or programs, with hundreds of different available editors. Still, it is reasonable to expect this approach to give more intuitive results than those of the standard QVT-R specification illustrated in Example 4.5.

One still needs a way to resolve non-determinism; it is unlikely that there will be a unique closest consistent model. In [ 12 ], the tool offered to the user all consistent models found at the same minimum distance from the current model. The implementation is very resource intensive and not practical for non-toy cases, and this is probably essential because of the need to consider all models at a given distance from the current one.

We are pessimistic about whether usably efficient algorithms that guarantee to find optimal solutions to the least change problem will ever be available, because Buneman, Khanna and Tan’s seminal paper [ 3 ] addressing the closely-related minimal update problem in databases showed a number of NP-hardness results even in very restricted settings. For example, where S is a database and Q(S) a view of it defined by a query (even a projectjoin query of constant size involving only two relations), they showed that it is NP-hard to decide, given a tuple t ∈ Q(S), whether there exists a set T ⊆ S of tuples such that Q(S \ T ) = Q(S) \ {t}.

Example 4.1 shows, we think, that the model that will be found by this approach will not always be what the user desires in any case. It is possible, though, that by applying exactly the same approach to the witness structure, rather than the model, we might get better behaviour. This would be interesting to investigate.

Formally, for relational bx we may define:

Definition A bx R : M ↔ N is metric-least, with respect to given metrics dM , dN on M and N , if for all m ∈ M and for all n, n0 ∈ N , we have

R(m, n0) ⇒ dN (n, n0) ≥ dN (n, →−R(m, n)) and dually.

Note that this is a property which a given bx may or may not satisfy: it does not generally give enough information to define deterministic consistency restoration behaviour, because of the possibility that there may be many models at equal distance.

The bx in Example 4.2 will be metric-least or not depending on the chosen metric on N . That in Example 4.3 will be metric-least, with respect to the usual metric on M and with any positive distance between + and − in N . Variant 1 of that example cannot be, however, for the reason given there. Variant 2 is metric-least, regardless of whether 0 is considered consistent with both of + and − or just one. All three variants of Example 4.7 are metric-least. 7

Continuity and other forms of structure preservation

We turn now to codifying reasonable, rather than optimal, behaviour; in a sense we now make the equation “least change = most preservation”. The senses in which transformations preserve things have of course been long studied in mathematics (and abstracted in category theory).

The most basic idea, and the most natural way to move on from the metrics-based approach considered in the previous section, is continuity, in the following metric-based formulation. (The other setting in which continuity appears in undergraduate mathematics, topology, we leave as future work.) Informally, a map is continuous (at a source point) if, however close you want to get to your target, you can ensure you get that close by starting within a certain distance of your source. Formally

Definition f : S → T is continuous at s iff

∀ > 0 . ∃δ > 0 . ∀s0 . dS (s, s0) < δ ⇒ dT (f (s), f (s0)) < We say just “f is continuous” if it is continuous at all s.

Standard results [ 17 ] apply: the identity function, and constant functions, are continuous (everywhere), the composition of continuous functions is continuous (at the appropriate points) etc.

To see how to adapt these notions to bx it will help to be more precise. In particular, metric-based continuity of a map is defined at a point: the idea that a map is continuous overall is a derived notion, defined by saying that it is continuous if it is continuous at every point. For us, the points are clearly going to be pairs of models. Supposing that we have metrics dM , dN on the model spaces M , N related by a relational bx R: Definition →−R is continuous at (m, n) iff

∀ > 0 . ∃δ > 0 . ∀m0 . dM (m, m0) < δ ⇒ dN (→−R(m, n), →−R(m0, n)) < This is nothing other than the standard metrics-based continuity of →−R( , n) : M continuous at (m, n) iff ←R−(m, ) : N → M is continuous at n.

Definition →−R is strongly continuous if it is continuous at all (m, n); that is, for every n, →−R( , n) is a continuous function. The definition for ←R− is dual. We say a bx R is strongly continuous if its restorers →−R, ←R− are so. → N at m. Dually, ←R− is

The terminology “strongly continuous” is justified with respect to our earlier discussion of strong versus weak least surprise, because of the insistence that →−R( , n) is continuous at all m, regardless of whether m and n are consistent.

Definition →−R is weakly continuous if it is continuous at all consistent (m, n); that is, for every n, →−R( , n) is continuous at all points m such that R(m, n) holds. The definition for ←R− is dual. We say a bx R is weakly continuous if its restorers →−R, ←R− are so.

Just as discussed in Section 3, one could consider further variants in which →−R( , n) is required to be continuous at points m where (m, n) is in some other subset of M × N .

Example 4.7 shows that weakly continuous really is weaker than strongly continuous. While all three of the options we considered for →−R(m, CN ) yield a weakly continuous →−R, only the first gives strong continuity. However, history ignorance – that is, the property that →−R(m, →−R(m0, n)) = →−R(m, n), and dually, for all values of m, m0, n, generalising PutPut for lenses – makes weak and strong continuity coincide.

Lemma 7.1 If R : M ↔ N is history ignorant as well as correct and hippocratic, then →−R is strongly continuous if and only if it is weakly continuous. Dually this holds for ←R− and hence for R.

Proof Suppose R is weakly continuous and consider (m, n) not necessarily consistent. We are given find δ > 0 such that and must ∀m0 . dM (m, m0) < δ ⇒ dN (→−R(m, n), →−R(m0, n)) < Using the same , we apply weak continuity at (m, →−R(m, n)) to find δ0 such that

∀m0 . dM (m, m0) < δ0 ⇒ dN (→−R(m, →−R(m, n)), →−R(m0, →−R(m, n))) < Applying history ignorance, this implies the condition we had to satisfy, so we take δ = δ0.

This approach has advantages over metric-leastness that we do not have space to explore, but it is worth giving one example. It is straightforward to prove: Theorem 7.2 Let R : M ↔ N and S : N ↔ P be strongly [rsp. weakly] continuous bx which, as usual, are correct and hippocratic. Suppose further that R is lens-like, i.e., →−R ignores its second argument; we write →−R(m). It follows that →−R(m) is the unique n ∈ N such that R(m, n). Define the composition R; S : M ↔ P as usual for lenses: (R; S)(m, p) holds iff there exists n ∈ N such that R(m, n) and S(n, p); R−−;→S(m, p) = →−S(→−R(m), p); R←−;−S(m, p) = ←R−(m, ←S−(→−R(m), p)). Then R; S is also correct, hippocratic and strongly [rsp. weakly] continuous.

Less positively, continuity is not useful in discrete model spaces, such as those that arise in (non-idealised) model-driven development, because: Lemma 7.3 Suppose m ∈ M is an isolated point, in the sense that for some real number Δ > 0 there is no m0 6= m ∈ M such that dM (m, m0) < Δ. Then with respect to dM , any →−R is continuous at (m, n), for every n ∈ N .

This holds just because for any one may pick δ < Δ and then the continuity condition holds vacuously.

As we would expect, metric-leastness is incomparable with continuity: they offer different kinds of guarantee. All three options in Example 4.7 are metric-least, so metric-leastness does not imply strong continuity. In fact it does not even imply weak continuity; Example 4.3 is metric-least, but not weakly continuous at (0, +). Conversely, Lemma 7.3 shows that even strong continuity does not imply metric-leastness; apply discrete metrics to M and N in Example 4.2, so that by Lemma 7.3 any variant of the bx discussed there is strongly continuous, and pick a variant that is not metric-least by the chosen metric. 7.1

Stronger variants of metric-based continuity Given that continuity is unsatisfactory because in many of the cases we wish to cover it holds vacuously, a reasonable next step is to consider the standard panoply of strengthened variants of continuity. (Standardly, these definitions do imply continuity.) Will any of them be better for our purposes? Let S and T be metric spaces as before.

Definition f : S → T is uniformly continuous iff

∀ > 0 . ∃δ > 0 . ∀s, s0 . dS (s, s0) < δ ⇒ dT (f (s), f (s0)) < That is, in contrast to the standard continuity definition, δ depends only on , not on s. This, adapted to bx, will obviously also be vacuous on discrete model spaces, so let us not pursue it.

Definition Given non-negative real constants C, α, we say f : S → T is H¨older continuous (with respect to

C, α) at s iff

∀s0 . dT (f (s), f (s0)) ≤ CdS (s, s0)α We say that f is H¨older continuous if it is so at all s. The special case where α = 1 is known as Lipschitz continuity.

Note that, to be congruent with our other definitions and for ease of adaptation, we have defined H¨older continuity first at a point, and then of a function. Since the definition is symmetric in s and s0, it is not often presented that way. Adapting to bx as before by considering the H¨older continuity of →−R( , n) : M → N at m, we get Definition →−R is H¨older continuous (with respect to C, α) at (m, n) iff

∀m0 . dN (→−R(m, n), →−R(m0, n)) ≤ CdM (m, m0)α Then as before, we may say that R is strongly (C, α)-H¨older continuous if it is so at all (m, n), weakly (C, α)H¨older continuous if it is so at consistent (m, n), and we may consider intermediate notions if we wish.

The fact that the adaptation to bx is symmetric in m and m0 raises the question of whether strong Ho¨lder continuity is actually stronger than weak H¨older continuity, however. In fact Example 4.7 was designed to demonstrate this: for example, variant 2 is easily seen to be weakly (1,1)-H¨older continuous, but is not strongly (1,1)-H¨older continuous because we can pick n = CN and m, m0 to be real numbers which are arbitrarily close but on opposite sides of 0.

We get again the analogue of Lemma 7.1, by the same argument.

Lemma 7.4 If R : M ↔ N is history ignorant as well as correct and hippocratic, then R is strongly (C, α)-H¨older continuous if and only if it is weakly (C, α)-H¨older continuous.

The next interesting question is whether H¨older continuity might avoid the problem we noted for continuity, viz. that it is trivially satisfied at isolated points. The answer is that it does, as Example 4.8 (which, recall, actually had no choice about how to restore consistency) shows: although →−R is continuous at every (m, n), it is not (C, α)-H¨older continuous at (CM , n) for any n ∈ N because, while the distance between CM and any other m0 is 1, the distance between →−R(CM , n) = 0 and →−R(m0, n) can be made arbitrarily large by judicious choice of m0.

Thus it is possible that H¨older continuity might turn out to be a useful least change principle, and we leave this as an open research question; we remark, though, that continuity is already a strong condition, Ho¨lder continuity much stronger, and it seems more likely that this will be a “nice if you can get it” property rather than one it is reasonable to insist on. Still, it might be interesting to consider, for example, subspace pairs on which it holds, and the possibility that a tool might indicate when a user leaves such a subspace pair.

Future work might consider e.g. locally Lipschitz functions, or in a sufficiently special space, continuously differentiable functions, etc. 8

Category theory

As previously discussed in Section 5, various authors have investigated least change in a partially (or even pre-) ordered setting. A natural generalisation of such work is to move from posets to categories. In particular, a number of people (notably Diskin et al. [ 5 ], Johnson, Rosebrugh et al. [10, 9, among others]) have considered generalisations of very well-behaved (a)symmetric lenses from the category of Sets to more general settings, notably Cat itself, the category of small categories.

The basic idea underlying these approaches is to go beyond the basic set-theoretic (state-based, whole-update) approach of lenses in order to incorporate additional information about the updates themselves, modelled as arrows. Rather than consider models, database states, as elements of an unstructured set (corresponding to a discrete category), they are taken as objects of a category S. Arrows γ : S −→ S0 correspond to updates, from old state S to new state S0. Arrows from a given S carry a natural preorder structure induced by post-composition, generalising the order induced by multiplication in a monoid: γ : S −→ S0 ≤ γ0 : S −→ S00 iff

∃δ : S0 −→ S00.γ0 = γ; δ

Johnson, Rosebrugh and Wood introduced the idea of a c-lens [ 10 ] as the appropriate categorical generalisation of very-well-behaved asymmetric lens: given by a functor G : S −→ V specifying a view of S, together with data defining the analogues of Put, satisfying appropriate analogues of the GetPut, PutGet and PutPut laws (we omit the details, which are spelt out very clearly, if compactly, in their subsequent paper [ 9 ]). They make explicit the connection with, and generalisation of, Hegner’s earlier work characterising least-change update strategies on databases [ 7 ]; in the categorical setting, database instances are models of a sketch defining an underlying database schema or entity-relationship model.

The crucial detail is that the ‘Put’ functor then operates not on pairs of states and views alone (that is, objects of S × V), but on updates from the image of some state S under G to a new view V , that is, on pairs consisting of an S-state S and a V-arrow α : GS −→ V , returning a new S-arrow γ : S −→ S0 such that Gγ = α. In other words, Put not only returns a new updated state S0 on the basis of a updated view V , but also an update from S to S0 that is correlated with the view update α. Notice that, because we have an update to a source S correlated with an update to a view GS which is consistent with the source, we are in the weak least surprise setting – but since very-well-behavedness in their framework is history-ignorance, the notions of weak and strong least surprise coincide.

They then show that the laws for Put establish that such an update γ is in fact least (indeed, unique) up to the ≤ ordering, namely as an op-cartesian lifting of α. Thus very-well-behaved asymmetric c-lenses do enjoy a Principle of Least Change. Extending this analysis, which applies to insert updates, with deletes being considered dually via a cartesian lifting condition on arrows α : V −→ GS, to the symmetric case is the object of ongoing study in terms of spans of c-lenses.

Johnson and Roseburgh further showed that Diskin et al.’s delta lenses [ 5 ] generalise the c-lens definition; in particular, every c-lens gives rise to an associated d-lens. However, such d-lenses do not enjoy the unique arrowlifting property, so there is some outstanding issue about the generality of the d-lens definition. In subsequent work [ 6 ], Diskin et al. have given a definition of symmetric d-lenses. It remains to be seen what least-change properties such structures might enjoy, on their own, or by reference to spans of c-lenses. 9

Conclusions and future work

The vision of bx in MDD is that developers should be able to work on essentially arbitrary models, which capture just what is relevant to them, supported by languages and tools which make it straightforward to define consistency and restore consistency between their model and others being used elsewhere. Clearly, if anything like this is to be achieved, there is vastly more work to be done on all fronts. Although there are some islands of impressive theoretical results (e.g. in category theory) and some pragmatically useful tools (e.g. based on TGGs), the theory currently works only in very idealised settings and the tools offer inadequate guarantees while still lacking flexibility. For software development, this situation limits productivity. For researchers it is an adventure playground.

We understand enough already to be sure that we will never achieve behaviour guarantees as strong as we would ideally like within the flexible tools we need. But the limits of what can be achieved are unknown. How far can we go, for example, by identifying “good” parts of the model spaces, where guarantees can be offered, and developing tools that warn their users when danger is near, so that they can spend their attention where it is most needed? If we need information from users to define domain-specific metrics, how can we elicit this information without unacceptably burdening users? Can we do better by focusing on reasonable behaviour than on optimal behaviour? It is noteworthy that, despite the name, HCI experts following the Principle of Least Surprise (or Astonishment) there are not really making an optimality claim so much as a reasonableness one: interface users might not know precisely what to expect, but when they see what happens, they should not be surprised. We think this is a good guide.

We have been pointing out, through the paper, areas we think need work (or play). Let us now mention some others that we have not touched on here. We have not mentioned topology, although we have touched on both metric spaces (a specialisation) and category theory (a generalisation). Perhaps the language of topology, or even algebraic topology, might help us to make progress. Even more speculatively, as type theory, especially dependent type theory, is a language we work in elsewhere, it is natural to wonder whether at some point spatial aspects of types such as for example homotopy type theory will have a role.

We have not attempted to analyse which properties any of the existing formalisms provide or could provide. Do any of the many existing bx formalisms that we have not mentioned, each thoughtfully designed in an attempt to “do the right thing”, satisfy any of the properties discussed here – and if not, why not? Under what circumstances do only global optima exist, so that guaranteeing reasonable behaviour would automatically guarantee optimal behaviour? Would identifying such circumstances help to resolve the tension between wanting optimality and wanting composition? Is there any mileage in applying the kind of guarantees of reasonable behaviour considered here to partial bx in the sense of [ 16 ], which do not necessarily restore consistency but, in an appropriate sense, at least improve it? Could someone make use of insights from Lagrangian and Hamiltonian mechanics? Or from simulated annealing?

Nailing our colours to the mast, we think: change to witness structures is important; pursuing reasonable behaviour will be more fruitful than pursuing optimal behaviour; identifying “good” subspace pairs will help tools in practice; and weak least surprise is not enough. But there is plenty of room for other opinions. We thank the anonymous reviewers, Faris Abou-Saleh, and the bx community for helpful comments and discussions. The work was funded by EPSRC (EP/K020218/1, EP/K020919/1). A Systematic Approach and Guidelines to Developing a Triple Graph Grammar

Anthony Anjorin Chalmers | University of Gothenburg [e-mail]

Erhan Leblebici, Roland Kluge, Andy Schu¨rr

Technische Universita¨t Darmstadt {firstname.lastname}@es.tu-darmstadt.de

Perdita Stevens University of Edinburgh [e-mail] Engineering processes are often inherently concurrent, involving multiple stakeholders working in parallel, each with their own tools and artefacts. Ensuring and restoring the consistency of such artefacts is a crucial task, which can be appropriately addressed with a bidirectional transformation (bx ) language. Although there exist numerous bx languages, often with corresponding tool support, it is still a substantial challenge to learn how to actually use such bx languages. Triple Graph Grammars (TGGs) are a fairly established bx language for which multiple and actively developed tools exist. Learning how to master TGGs is, however, currently a frustrating undertaking: a typical paper on TGGs dutifully explains the basic “rules of the game” in a few lines, then goes on to present the latest groundbreaking and advanced results. There do exist tutorials and handbooks for TGG tools but these are mainly focussed on how to use a particular tool (screenshots, tool workflow), often presenting exemplary TGGs but certainly not how to derive them systematically. Based on 20 years of experience working with and, more importantly, explaining how to work with TGGs, we present in this paper a systematic approach and guidelines to developing a TGG from a clear, but unformalised understanding of a bx. 1

Introduction and Motivation

Formalizing and maintaining the consistency of multiple artefacts is a fundamental task that is relevant in numerous domains [ 6 ]. Bidirectional transformation (bx ) languages address this challenge by supporting bidirectional change propagation with a clear and precise semantics, based on a central notion of consistency specified with the bx language. Although numerous bx approaches exist [ 19 ], often with corresponding tool support, mastering a bx language is still a daunting task. Even once the user has a clear, though unformalised, understanding of what the bx should do, embodying this understanding in a bx is non-trivial. Formal papers do not address this issue, and neither, usually, do tool-centric handbooks.

Copyright c by the paper’s authors. Copying permitted for private and academic purposes.

In: A. Cunha, E. Kindler (eds.): Proceedings of the Fourth International Workshop on Bidirectional Transformations (Bx 2015), L’Aquila, Italy, July 24, 2015, published at http://ceur-ws.org

Triple Graph Grammars (TGGs) [ 18 ] are a prominent example of a bx language for which this observation holds: a typical paper on TGGs dutifully explains how TGGs “work” in a few lines, then conjures up a complete and perfect TGG specification for the running example out of thin air. This is not how things work in practice; going from a clear, but unformalised understanding of consistency to a formal TGG specification is difficult, especially for developers who do not already have ample practice with rule-based, declarative, (graph) patternbased languages. Existing tutorials, handbooks, and introductory papers on TGGs do not alleviate this situation as they are either tool-specific, focusing on how to use a certain TGG tool, or present basic concepts without providing a systematic approach to how TGG rules can be iteratively engineered.

To the best of our knowledge, the only existing work in this direction is from Kindler and Wagner [ 13 ] and later, treated in some more detail in Wagner’s PhD thesis [22]. Similarly to [21] for model transformation, Kindler and Wagner propose an algorithm that “synthesizes” TGG rules from a set of consistent examples provided by the user. Although this can be very helpful in scenarios where rather simple but numerous TGG rules are required, we have observed that a typical TGG involves a careful design process with direct consequences for the resulting behaviour of derived model synchronizers. Indeed, Kindler and Wagner mention that synthesized TGGs probably have to be adjusted, extended and finalized manually, but do not provide adequate guidance of how this can be done systematically.

Based on 20 years’ experience working together with industrial partners and students, learning how to understand and use TGG specifications, our contribution in this paper is, therefore, to provide a systematic approach to creating and extending TGGs. Our aim with the resulting step-by-step process, is to substantially lower the initial hurdle of concretely working with TGGs, especially for other users and researchers in the bx community.

The rest of the paper is organized as follows: Sect. 2 reviews the preliminaries of TGGs and provides our running example that is available as Ecore2Html from the bx example repository [ 5 ], and as a plug-and-play virtual machine hosted on Share.1 Sect. 3 introduces an iterative approach and a set of guidelines for engineering a TGG, constituting our main contribution in this paper. Sect. 4 complements this by providing an intuitive understanding of TGG-based synchronization algorithms. Sect. 5 compares our work to other related contributions. Sect. 6 summarizes and gives a brief outlook on future tasks. 2

Running Example and Preliminaries

The running example used in the rest of this paper is a bidirectional transformation between class diagrams and a corresponding HTML documentation. Consider, for instance, a software development project for implementing a TGG-based tool. The project consists of two groups of developers: (i) core developers who are responsible for establishing and maintaining the main data structures and API provided by the tool, and (ii) other developers who mainly use the API and work with the tool (functioning as beta testers for the project). The latter group does not define the data structures involved, but is probably in a better position to document all packages, classes, and methods. It thus makes sense to maintain two types of artefacts for the two groups of stakeholders: (1) class diagrams, maintained by core developers, and (2) HTML documents, maintained by API users in, e.g., a wiki-like manner. The class diagram to the left of Fig. 1 depicts the main data structures of a TGG tool, with a corresponding folder structure containing HTML files to the right.

The outermost package TGGLanguage corresponds to the top-most folder TGGLanguage, and contains subpackages and classes, which correspond to subfolders and HTML files, respectively. TripleGraphGrammars consist of TGGRules, which are in essence graph patterns (referred to as StoryPatterns) consisting of variables that stand for objects (ObjectVariables) and links (LinkVariables) in a model. This general concept of a graph pattern is extended for TGGs by attaching a Domain to each concept. Each Domain references a Metamodel, a wrapper for the supported metamodelling standard.2 The classes StoryPattern, LinkVariable, ObjectVariable, and EPackage are imported from other class diagrams (greyed out) and are not part of the documentation of TGGLanguage. The corresponding documentation model is much simpler: it consists of a folder structure mirroring the package structure in the class diagram, and an HTML file for each class. Note that packages are also documented in corresponding files, which start with “ ” to distinguish them from class documentation files (e.g.,

TGGLanguage.html). Inheritance and references are irrelevant for the documentation model, but all methods of each class (excluding inherited methods) are to be documented as a table with two columns (name of the method and documentation) in the corresponding class documentation file.

1http://is.ieis.tue.nl/staff/pvgorp/share/?page=LookupImage&bNameSearch=eMoflon 2In this case EPackage for Ecore, the de facto standard of the Eclipse Modeling Framework (EMF). TripleGraphGrammar tripleGraphGrammar 1 1 tripleGraphGrammar metamodel outermostPackage 2..3 Metamodel 1 EPackage metamodel 1

eSubpackages 0..* eSuperPackage 0..1 source correspondence 1 target 1 1 domain 1 domain 3

Domain

TGGLinkVariable TGGObjectVariable domain 1 analysis csp precompiler tripleGraphGrammar

1 tggRule 0..* TGGRule refines 0..* linkVariable

0..* LinkVariable pattern 1 incomingLink 0..* outgoingLink 0..* StoryPattern pattern 1

The following points are noteworthy: (1) Information loss is incurred when transforming class diagrams to documentation models (e.g., inheritance relations and references) and when transforming documentation models to class diagrams (all entered documentation is lost!). This is the main reason why the change propagation strategy required for this example must take the old version of the respective output artefact into account. (2) Not all possible changes make sense: it is arguable whether API users should be able to rename elements in the documentation and propagate such changes to the corresponding class diagrams. Even more arguable are changes such as adding new elements in the documentation that do not yet exist in the class diagram. Such changes may be interpreted as feature requests, but are probably not primary use cases.

Models, Metamodels, Deltas, and Triple Graph Grammars: We assume a very basic understanding of TGGs and of Model-Driven Engineering (MDE) concepts, and refer readers having a hard time understanding the following to, e.g., the eMoflon handbook3 for a gentle, tutorial-like introduction. Readers more interested in a formal and detailed introduction to TGGs are referred to, e.g., [ 1 ].

In the following, we introduce core terms and notation as they are to be understood (informally) in this paper. Based on this understanding, we then propose a systematic, iterative TGG development process in Sect. 3, together with a set of guidelines or best practices. This process is then demonstrated by applying it to develop a TGG for our running example.

A model is an abstraction (a simplification) of something else, chosen to be suitable for a certain task. In an MDE context, metamodels, essentially simplified UML class diagrams, are used to define languages of models.

Given two languages of models and their respective metamodels, say a source and a target language, a consistency relation over source and target models is a set of pairs of a source and a target model, which are to be seen as being consistent with each other.

Given a consistent pair of source and target models, a change applied to the source model is referred to as a source delta, and a change to the target model is called a target delta. As models are graph-like structures consisting of attributed nodes and edges, we may decide that atomic deltas are one of: element (node/edge) creation, element deletion, and attribute changes. Atomic deltas can be composed to yield a composite delta. A composite delta that only involves element creation is called a creating delta. A source/target delta that does nothing is called an idle source/target delta, respectively.

Given a consistent pair of source and target models, and a source delta, the task of computing a corresponding target delta that restores consistency by changing the target model appropriately is referred to as forward model synchronization, or just model synchronization. This applies analogously to target deltas and computed source deltas, i.e., backward model synchronization. The more general task of restoring consistency given both a source and a target delta is referred to as model integration, which is outside the scope of this paper.

A Triple Graph Grammar (TGG) is a finite set of rules that each pair a creating source/target delta with either a corresponding creating target/source delta or with an idle target/source delta, respectively.

Each TGG rule states that applying the specified pair of deltas together will extend a given pair of source and target models consistently. To keep track of correspondences between consistent source and target models on an element-to-element basis, a third correspondence model can be maintained consisting of explicit correspondence elements connecting certain source and target elements with each other. These correspondence elements are typed with a correspondence metamodel, which can be chosen as required. In general, a TGG can thus be used to generate a language of triples, consisting of connected source, correspondence, and target models. A triple is denoted as GS ← GC → GT (G for graph). A TGG induces a consistency relation as follows: A pair of source and target models (GS , GT ) is consistent if there exists a triple GS ← GC → GT that can be generated by applying a sequence of deltas, as specified by the rules of the TGG.

A TGG tool is able to perform model synchronization using a given TGG as the specification of consistency. A TGG tool is correct if it only produces results that are consistent according to the given TGG used to govern the synchronization process [ 18 ]. As correctness does not in any way imply that information loss should be avoided, one TGG tool is said to be more incremental than another if it handles (avoids) information loss better [ 1 ]. A TGG tool is said to scale if the runtime for synchronization depends polynomially (and not exponentially) on model and delta size, and is efficient if the runtime for synchronization only depends on delta size (and no longer on model size) [ 1 ].

Example: To explain these basics further, Fig. 2 depicts the source and target metamodels chosen for the running example. The source metamodel (to the left) is Ecore, a well-known standard for simple class diagrams. Class diagrams basically consist of packages (EPackages) containing subpackages, and classes (EClasses) with methods (EOperations). The target metamodel (to the right) is MocaTree, a generic tree-like target metamodel providing concepts to represent a hierarchy of folders with files, where each file contains a tree consisting of Nodes. Objects of type Text but not of type Node are used to represent leaves in the tree that cannot have children. In this manner, it is possible to represent arbitrary (X)HTML trees. The correspondence metamodel consists of types connecting source and target elements as required for the rules and is omitted here. parentFolder 10..1 ENamedElement

TreeElement subFolder *

EPackage eSubpackages 0..*

1 eClassifiers 0..* eSuperPackage 0..1 eSuperTypes 0..*

EClassifier

EClass 1 eType eContainingClass eOperations 1 0..*

ETypedElement

EOperation Ecore

Folder folder 1 file * File file 1

Node rootNode 1 Text children parentNode 0..* 1

MocaTree

To introduce the notation and language features used in this paper to specify TGG rules, let us consider two TGG rules for handling (sub)packages and their corresponding documentation. The TGG rule for handling root packages is depicted to the left of Fig. 3. The source and target deltas paired by this rule are: (i) creating a new EPackage in the source model, and (ii) creating a Folder with a single HTML File. The basic structure of the HTML file, consisting of a header and a paragraph where a description of the package can be entered, is also created in the same target delta. The package and folder are connected with a correspondence node of type EPackageToFolder. In standard TGG visual notation, all elements created in a rule are depicted in green with an additional "++" markup for black and white printouts. Correspondence nodes are additionally depicted as hexagons to clearly differentiate them from source and target elements.

A set of attribute constraints specifies the relationship between attribute values of the elements in a TGG rule. All TGG tools provide an extra, typically simple textual language for expressing such attribute constraints. In this case, the eq constraint expresses that ePackage has the same name as docuFolder. To express that the name of the htmlFile should start with " ", end with ".html", and contain the name of ePackage, two attribute constraints addSuffix and addPrefix are used, where withSuffix is a temporary variable.

For cases where an attribute is simply assigned a constant, this can be “inlined” in the respective node, e.g., name := "html" in rootNode. If we consider Fig. 1 again, we can now compare the creating deltas in the TGG rule to the package TGGLanguage, the folder TGGLanguage and the HTML file TGGLanguage.html, and see that all attribute constraints are fulfilled.

It is often useful to extract parts of a rule into a basis rule, so that these parts can be reused in other subrules. Apart from possibly enabling reuse, readability can also be increased by decomposing a rule into modular fragments that each handle a well-defined concern. Many TGG tools support some form of rule refinement [ 3, 8, 14 ] as depicted to the right of Fig. 3: A new TGG rule HTMLFileAndHeader, creating the basic structure of an HTML file, has been extracted and is now refined (denoted by an arrow) by the subrule RootPackageToDocuFolder to yield the same rule as depicted to the left of Fig. 3. As we do not want to allow creating basic HTML files on their own, HTMLFileAndHeader is declared to be abstract (denoted by displaying the rule’s name in italics). This means that it is solely used for modularization and not for synchronization. The exact details of rule refinement are out-of-scope for this paper, but in most cases (as here), it is a merge of the basis with the refining rule, where elements in the refining rule override elements with the same name in the basis rule (this is the case for htmlFile and title). Such overriding elements are shaded light grey in subrules to improve readability. TGGs with rule refinements are flattened to normal TGGs. Abstract rules are used in the process, but are not included in the final TGG. Non-abstract rules are called concrete rules.

Fig. 4 depicts a further TGG rule SubPackageToDocuFolder for handling subpackages (EPackages with a super package). SubPackageToDocuFolder refines RootPackageToDocuFolder and additionally places the created package into a super package, and the corresponding subfolder into a parent folder (determined using the correspondence node superToFolder). Finally, the title is adjusted for subpackages by overriding it in SubPackageToDocuFolder. This rule shows how context can be demanded; the context elements superPackage, superToFolder, superFolder, and connecting source and target links are depicted in black and must be present (created by some other rule) before the rule can be applied. In this sense, the context elements form a precondition for the application of the rule.

Our current TGG consists of two concrete rules and one abstract rule, and can be used to generate consistent package hierarchies and corresponding folder structures with HTML files for documenting the packages.

In the following section, we shall take a look at how to systematically develop TGG rules in a step-by-step process, discussing various kinds of TGG rules and how design choices affect derived TGG-based synchronizers. 3

An Iterative Process and Guidelines for Developing a TGG

To introduce basic concepts we have already specified a TGG to handle package structures and their HTML documentation. This was done in a relatively ad-hoc fashion, choosing source and target metamodels, deciding to start with handling packages, and specifying the required TGG rules without consciously applying any systematic process. Although this might work fine for simple cases or for seasoned TGG experts, we propose the following process depicted in Fig. 5, which consists of four steps outlined in the following sections. In each step, we give guidelines that represent current best practice and provide guidance when making design decisions. 1 2 3 4 Choose and adjust your abstractions

Extend your testsuite of supported deltas

Extend your TGG to pass the new tests

Profile for hotspots and scalability

Choose and adjust your abstractions (metamodels) In practice, the final artefacts to be synchronized are typically fixed for a certain application scenario, e.g., XML files, a certain textual format, a tool’s API, or programs in some programming language. As TGG tools do not usually operate directly on these final artefacts, a parser/unparser component, referred to as an adapter in the following, is required to produce a graph-like abstraction of the artefacts. The choice of source/target metamodels thus becomes a degree of freedom with a direct impact on the complexity of the required adapter.

Guideline 1 (Adapter complexity vs. rule complexity). Choosing very high-level source and target metamodels

might lead to simple, elegant TGG rules but also requires complex adapters in form of (un)parsers or some other import/export code. As this shifts complexity away from the TGG, strive to keep such pre/post-processing adapter logic to a minimum. Decomposing the synchronization into multiple steps by introducing an intermediate metamodel and developing two TGGs instead of one can be a viable alternative.

Example: For our running example, the source artefacts are XMI files representing class diagrams, while target artefacts are XHTML files. As the class diagrams already conform to Ecore, choosing Ecore as the source metamodel means that the standard EMF XMI reader and writer can be used. To handle XHTML files, a simple and generic XML adapter is used that produces instances of a basic, tree-like metamodel MocaTree, as depicted in Fig. 2. Although these choices reduce the required adapter logic to a minimum (G1), our TGG rules are rather verbose, especially in the target domain (cf. Fig. 3). We addressed this with rule refinement (any form of modularity concept could be beneficial in this case if supported by the chosen TGG tool), but could also have chosen a richer target metamodel and shifted most of the complexity to a problem-specific XHTML parser and unparser instead. 3.2

Extend your test suite of supported deltas Although it is generally accepted best practice in software development to work iteratively and to apply regression testing, beginners still tend to specify multiple rules or even a complete TGG without testing. This is particularly problematic because the understanding of the consistency relation often grows and changes while specifying a TGG. The following guideline highlights that any non-trivial TGG should be supported by a test suite.

Guideline 2 (Take an iterative, test-driven approach). When specifying a TGG, take a test-driven approach to prevent regression as the rules are adjusted and extended. Run your test suite after every change to your TGG.

In this context, a source test case consists of: (i) a consistent triple (possibly empty), (ii) a source delta to be applied to the triple, and (iii) a new target model representing the expected result of forward synchronizing the source delta. Target test cases are defined analogously. Although all important deltas for an application scenario should eventually be tested, it makes sense to focus first on creating deltas as these can be almost directly translated into TGG rules.

Guideline 3 (Think in terms of creating source and target deltas). Think primarily in terms of consistent pairs of creating source and target deltas and derive corresponding test cases. This simplifies the transition to a TGG. The following two guidelines propose to handle “easy” cases first before going into details. Concerning creating deltas, “easy” translates to “not dependent on context”.

Guideline 4 (Start with context-free creating deltas). Start with context-free pairs of creating deltas as these are usually simpler. A context-free delta can always be propagated in the same way, independent of what the elements it creates will be later connected with.

Although graphs do not have a “top” or “bottom” in general, in many cases models do have an underlying containment tree. Top-down thus means container before contents. As containers typically do not depend on their contents, we get the following guideline as a corollary of Guideline 4:

Guideline 5 (Prefer top-down to bottom-up). If possible, start top-down with roots/containers of the source and target metamodels as containers typically do not depend on their contents.

Example: Applying these guidelines to our running example, we chose to handle package hierarchies in a first iteration (G2). We started thinking about creating a root package in the class diagram as a source delta, whose corresponding target delta is creating a folder containing a single HTML file named “ ” + ePackage.name, which is to contain the documentation for the root package (G3). This is always the case irrespective of what the root package/folder later contains and is thus a context-free pair of creating deltas (G4). We took a top-down approach (G5) handling root packages before subpackages (cf. Fig. 3 and Fig. 4). 3.3

Extend your TGG to pass the new tests After discussing with domain experts and collecting test cases addressing a certain aspect, e.g., (sub)packages and folders, the next step is to specify new, or adjust existing, TGG rules to pass these tests. To accomplish this, it is crucial to understand that there are only a few basic kinds of TGG rules as depicted schematically in Fig. 6. The names are chosen to give a geographical intuition, where green and black clouds/arrows denote created and context elements, respectively: Islands are context-free rules that do not demand any context. An island may either be idle, creating either source or target elements, or it may create both, source and target elements. After applying such a rule, an isolated “island” of elements is created.

Extensions require a context island and then extend it by creating and directly attaching new elements to it. Bridges connect two context islands by creating new elements to form a bridge between the islands. Bridges can of course be generalized to connect multiple islands, but remain fundamentally the same. Bridges connecting more than two islands are rare in practice, probably because they become increasingly complex to comprehend. Ignore rules (not depicted) are TGG rules that do not create any elements in either the source or target domain. Such rules state explicitly that applying a certain creating delta in one domain has no effect on the other domain. Based on these basic kinds of TGG rules, we propose the following guidelines.

Extension Rule

Guideline 6 (Prefer islands and bridges to extensions). When specifying an extension, always ask domain experts

if it is acceptable to split the extension into an island and a bridge, as this often improves derived synchronizers.

Extensions should only be used if an island would have to change once it is connected via a bridge.

An extension states that all created elements are dependent on the specified context. In many cases, this introduces unnecessary dependencies between islands. In general, TGG-based synchronization works better, the fewer context dependencies are specified in rules.

Guideline 7 (Formalize information loss via explicit ignore rules). Most TGG tools attempt to ignore irrelevant elements automatically, as specifying this explicitly with ignore rules can be tedious, especially in the first few iterations, when the TGG covers only a small subset of the source and target metamodels. Explicit ignore rules are nonetheless better than tool-specific heuristics and automatic ignore support, and should be preferred. Example: Applying these guidelines to our running example, we now discuss the current TGG (handling package/folder hierarchies) as well as new rules for handling classes and methods, together with their respective documentation. Reflecting on rules RootPackageToDocuFolder and SubPackageToDocuFolder (cf. Fig 3 and 4) now in the light of our guidelines, we can identify RootPackageToDocuFolder as an island, and SubPackageToDocuFolder as an extension thereof. Can we split the extension into an island and a bridge (G6)? Although subpackages are treated just like root packages, it must be clear from the corresponding documentation file that this is the documentation for a subpackage and not a root package. The heading in the file (title in RootPackageToDocuFolder) must, therefore, be adjusted appropriately. Interestingly, if a (sub)package p is deleted in the source model, all subpackages of p consequently become root packages and must now be (re)translated differently! This also applies to making a former root package a subpackage by connecting it to a super package. In this case, the root package is now a subpackage and must also be (re)translated appropriately. Creating and documenting subpackages in this manner is an example of creating deltas that cannot be handled as an island.

Creating a class c corresponds to creating an HTML file named <c.name> + “.html”, this time with a header “EClass” + <c.name>. In addition, an empty HTML table to contain all methods of the class should be created in the file. Adding a class c to a package p corresponds to simply placing the documentation file for c into the documentation folder for p. This time around, these consistency requirements can be transferred directly to an island and a bridge: Fig. 7 depicts the island EClassToHTMLFile for handling the creation of an EClass and its documentation file with internal HTML structure. EClassToHTMLFile once again refines HTMLFileAndHeader to reuse the basic structure of an HTML file. The body of the HTML file is extended, however, by a table node methodTable and an extra subheader for the table. Attribute constraints are used to ensure that the name and header of the file correspond appropriately to the created class. Specifying this as an island means that classes and their documentation are created in this manner, independent of what package the class is later placed in.

Fig. 7 also depicts the bridge EClassToFileBridge used to handle adding classes to packages and their documentation files to the corresponding documentation folder. In this case the “bridge” consists of an edge in each domain. In general, however, an arbitrary number of elements can be created to connect the context clouds as required. The primary advantage of using a bridge here instead of an extension (G6) is that unnecessary dependencies are avoided; a class can be moved to a different package without losing its documentation. Finally, Fig. 7 depicts an ignore rule IgnoreFileDocu (no elements are created in the source domain), which states explicitly that adding documentation to an HTML file does not affect the source domain (G7). Note that this handles documentation for both packages and classes as the basic structure of the HTML file is identical.

Fig. 8 depicts an island DocumentMethod, a bridge EOperationTableBridge, and an ignore rule IgnoreMethodDocu used to handle creating methods and their corresponding documentation. «Rule» RootPackageToDocuFolder

«Rule»

EClassToHTMLFile

Creating a method of a class corresponds to creating a row in an HTML table with two column entries: the first for the name of the method, and the second for its documentation (initially empty). Connecting a method to a class corresponds to adding this row to the method table of the class that was created by EClassToHTMLFile. A row in an HTML table is a tr element, while column entries are td elements. Indices are used in DocumentMethod to ensure that the column entries are always in the same order (name before documentation). EOperationTableBridge connects a method to a class, and adds its HTML row node to the method table of the class. Analogously to IgnoreFileDocu, the ignore rule IgnoreMethodDocu states that documenting a method does not affect the source domain. Note that the node documentation is constrained to be a column entry.

According to G7, we would actually need to specify ignore rules for all irrelevant concepts in the source domain (cf. Fig. 2) including inheritance relations, attributes, references, and datatypes. This guideline can be relaxed, however, for types that do not occur in any TGG rule. It is, for instance, easy to automatically ignore the reference eSuperTypes denoting inheritance, but difficult to automatically ignore Text documentation nodes (as in IgnoreMethodDocu), as the type Text does occur, e.g., as ref:Text in DocumentMethod.

Profile for hotspots and scalability Declarative languages such as TGGs certainly have their advantages, but one must reserve some time for profiling and testing for scalability. Depending on the TGG tool and the underlying modelling framework and transformation engine, certain patterns and constructs can be, especially for beginners, surprisingly inefficient.

Guideline 8 (Use a profiler to test regularly for hotspots). Regularly profiling the synchronization for medium

and large sized models is important to avoid bad design decisions early enough in the development process4. To support such a scalability analysis, some TGG tools [ 11, 23 ] provide support for generating models (of theoretically arbitrary size) using the TGG specification directly. This should be exploited if available.

Concrete optimization strategies for TGGs are discussed in detail in [ 15 ]. The most common user-related optimization is to provide more specific (and in some cases redundant) context elements and attribute constraints within the source and target domains of a rule. This helps the transformation engine eliminate inappropriate rule applications in an early phase, i.e., before checking all (costly) inter-model connections in a rule pattern. 4

TGG-Based Synchronization Algorithms

In this section we try to bring our TGG to life in the synchronization scenario depicted in Fig. 9. Our goal is to impart a high-level intuition for how TGG-based synchronization algorithms work in general. This provides not only a rationale for the guidelines already provided in the previous section, but also an understanding for how arbitrary deltas (and not only the explicitly specified creating deltas) are propagated. How this propagation works arguably depends on the chosen TGG tool, in our case eMoflon whose algorithm is described in [ 1 ], and we refer to [ 12, 16 ] for a detailed comparison of TGG tools. Nevertheless, the provided intuition is still helpful in understanding the TGG-related consequences of a delta, i.e., which TGG rule applications from former runs must be invalidated or preserved, and which TGG rules must be applied in a new run. In the following, the labels 1 – 6 are used to refer to certain parts of the synchronization scenario in Fig. 9. Batch Translation 1 , 2 : The scenario starts with the creation of a new class diagram 1 . To provide a consequent delta-based intuition, this initial step can also be seen as a large source delta consisting of adding all elements in the class diagram. To create this class diagram 1 , a root folder TGGLanguage containing two classes and two subfolders compiler and precompiler must be created. Each subfolder also contains a class, and compiler contains a subfolder as well. To propagate this source delta 2 , TGG-based algorithms compute a sequence of TGG rule applications that would create the resulting source model. A possible sequence in this case is: (1) RootPackageToDocuFolder to create TGGLanguage, (2) SubPackageToDocuFolder applied three times to create compiler, precompiler, and compilerfacade, (3) EClassToHTMLFile to create all classes, and (4) EClassFileBridge to connect all classes to their containing packages. As TGG rules are specified as triple rules, applying this sequence of rules yields not only the expected source model but also a correspondence and a target model. In addition, the resulting triple of source, correspondence, and target models is, by definition, in the specified TGG language and is, therefore, correct. The target model is thus the result of forward propagating 2 the source delta 1 . Although this search for a possible rule application sequence can be implemented na¨ıvely 4Although this ultimately depends on the specific metamodels and TGG rules, our current experience is that models of up to about 200 000 elements can be handled reasonably well by TGG-based synchronizers [ 15 ]. 2

3 as a straightforward trial and error procedure with backtracking, this would have exponential runtime and does not scale. All TGG tools we are aware of do not backtrack and instead restrict the class of possible TGGs.

A common restriction is demanding some variant of confluence, a well-known property of transition systems, which can be checked for statically using a so-called critical pair analysis. The interested reader is referred to, e.g., [ 2 ] for details. The na¨ıve understanding of just fitting TGG rules until the correct sequence of rule applications is determined is, however, sufficient for an intuitive understanding of how this works in theory. Ignoring Changes with Ignore Rules 3 , 4 : A target delta consisting of two changes is applied in 3 . As depicted in Fig. 9, the documentation files precompiler.html and RefinementPrecompiler.html for the package precompiler and the class RefinementPrecompiler, respectively, are edited. In terms of our HTML metamodel, this corresponds to adding a textual node to the corresponding paragraphs (p nodes) in the HTML files. A TGG-based synchronizer would propagate 4 this target delta by simply doing nothing, i.e., the source model is not changed at all. The same process is taken as with 2 , i.e., a sequence of TGG rules is determined that applies the given target delta. The sequence in this case is: IgnoreFileDocu applied twice to create the added text node in both HTML files. As both rules are specified as ignore rules, the correspondence and target models are not changed in the process.

Handling Deleted and Added Elements 5 , 6 : After discussing two simple cases, we now demonstrate how the choice between extensions and bridges affects the behaviour of a TGG-based synchronizer. Let us consider a more general source delta 5 , which “moves” the subpackage precompiler from TGGLanguage to compiler.

This is accomplished by (i) deleting the link between TGGLanguage and precompiler, and (ii) creating a new link between compiler and precompiler. Propagating this source delta 6 thus entails handling a deletion and an addition. The synchronization is, therefore, executed in three phases: a deletion phase, an addition phase, and a translation phase: for all deletions: revoke all dependent rule applications for all additions: revoke all dependent rule applications translate all revoked and newly added elements To revoke means to rollback a rule application, i.e., for forward synchronization, all correspondence and target elements created by the rule application to be revoked are deleted, while all created source elements are considered as revoked and to be (re)translated in the ensuing translation phase.

For every element that has been deleted, all rule applications that require the element as context and thus depend on the deleted element become invalid and must be revoked. Note that this must be done transitively.

In general, additions also have to be handled analogously to deletions, i.e., sometimes rule applications must be revoked as a consequence of newly added elements. For our running example, consider adding a new root package eMoflonLanguages that contains the current root package TGGLanguage. This must lead to revoking TGGLanguage and re-translating it as a subpackage of the new root package eMoflonLanguages!

To explain this further with our synchronization scenario, Fig. 10 depicts a relevant excerpt of the source and target models involved (top left). The deleted link is depicted bold and red with a “--” markup for emphasis. A TGG-based synchronizer typically keeps track of the translation by grouping links and objects into rule applications. This grouping is depicted visually in Fig. 10 for all rule applications required to create the current triple. For example, the rule application 3:SubPackageToDocuFolder comprises the deleted link between TGGLanguage and precompiler, the subpackage precompiler, as well as the corresponding target elements: the link between the root folder TGGLanguage and subfolder precompiler, the folder precompiler, and the HTML file precompiler.html. Note that the rule applications also comprise all relevant correspondence elements, which are abstracted from in Fig. 10 to simplify the explanation.

This grouping into rule applications, which can be reconstructed by simulating the creation of a consistent triple from scratch if necessary, is used to determine dependencies between the groups of elements. This is depicted visually in Fig. 10 (top right) as a dependency graph, showing that, for example, the rule application 5:EClassFileBridge depends on (shown as an arrow) 3:SubPackageToDocuFolder and 4:EClassToHTMLFile, as these two rule applications create objects that are required as context in 5:EClassFileBridge.

Given a source delta and calculated dependencies between rule applications, the deletion phase is carried out by revoking all rule application containing deleted elements, recursively revoking all rule applications that directly or transitively depend on revoked rule applications, and finally removing the deleted source elements from all data structures. This process is depicted in Fig. 10 (top right) showing (with a bold, red outline and “--” markup) that 3:SubPackageToDocuFolder is to be revoked as it contains the deleted source link between TGGLanguage and precompiler. In this case, the only dependent rule application is 5:EClassFileBridge, which must also be revoked (bottom right of Fig. 10).

In the translation phase, all revoked source elements are treated as if they were newly added, i.e., they are translated together with all added elements. This is depicted in Fig. 10 (bottom left) showing (bold, green outline and “++” markup) the revoked source elements precompiler and the link between precompiler and RefinementPrecompiler, as well as the newly added link between compiler and precompiler from the source delta. In this state, the same translation strategy as explained for 2 and 4 can be applied, however, only for all added and revoked source elements. Due to this process, the documentation added to RefinementPrecompiler.html in 3 is retained as its corresponding class is not revoked (Fig. 10, bottom left). As the subpackage precompiler is, however, revoked and re-translated, its documentation file precompiler.html is deleted, losing the changes made in 3 , and is re-created afresh.

This is a direct consequence of using an extension rule for handling subpackages, but a bridge to connect classes to their parent packages. Similarly, the decision to use a bridge to connect methods to their classes enables, e.g., a pull-up method refactoring in the class diagram without having to revoke the method and lose its documentation. One can certainly argue that this behaviour is not always optimal, but it is what can currently be expected from state-of-the-art TGG-based synchronizers, given the choices we made when designing our TGG. Further improving current TGG synchronization algorithms to handle extensions as bridges during change propagation and still guarantee correctness is ongoing research. -2: SubPackageToDocuFolder

__TGGLanguage.html 5: EClassFileBridge 4: EClassToHTMLFile RefinementPrecompiler

RefinementPrecompiler

Elements grouped into rule applications __compiler.html __precompiler.html __compiler.html Triple after handling deletions and additions 1: RootPackageToDocuFolder 4: EClassToHTMLFile 5: EClassFileBridge

-3: SubPackageToDocuFolder Dependency graph

2: SubPackageToDocuFolder 1: RootPackageToDocuFolder 4: EClassToHTMLFile

-- 2: SubPackageToDocuFolder 5: EClassFileBridge

Dependency graph 5

Related Work

We consider three different groups of related work in the following: (1) previous TGG publications with a focus similar to this work, (2) guidelines for bx approaches based on QVT-R which, similar to TGGs, address bx in an MDE context, and (3) other approaches to systematically developing model transformation rules in general. Other approaches to systematically developing a TGG: Kindler and Wagner [ 13, 22 ] propose to semiautomatically synthesize TGG rules from exemplary pairs of consistent source and target models. Viewing their iterative synthesizing procedure through our geographical intuition, an island is first constructed from a given pair of consistent models, and is then stepwise deconstructed to smaller islands, bridges, or extensions by removing parts already covered by rules synthesized from former runs. As the procedure largely depends on the complexity of the transformation as well as the representativeness and conciseness of the provided examples, the authors suggest finalizing the process with manual modifications, for which our guidelines can be used.

Engineering guidelines are presented in [ 15 ] based on experience with profiling and optimizing TGGs. In contrast to this paper, the topics handled in [ 15 ] are mostly scalability-oriented and address, in many cases, primarily TGG tool developers rather than end users.

Guidelines for bx with QVT-R: Similar to TGGs, QVT-Relations (QVT-R) addresses bx in an MDE context. The standard QVT-R reference [ 17 ] already supplies examples demonstrating the usage of different language constructs. The standardized textual concrete syntax facilitates the distribution of such best practices across different QVT-R tools, whereas TGG tools currently suffer from interoperability issues as different metamodels are used for representing graphs, rules, and correspondences. Considering the chronological order of formal and practical contributions for TGGs and QVT-R, one can observe that while we now strive to impart a practical intuition and guidelines to complement existing formal work on TGGs, recent papers on QVT-R [ 4, 9, 20 ] strive to formalize concepts for an existing intuition. Approaches to designing model transformation rules in general: Most of the work to facilitate transformation rule development focuses on semi-automatic usage of exemplary model pairs. While not necessarily focusing on bx, such approaches (e.g., [21, 24]) often require explicit mappings on the instance level, which closely resemble the correspondences in TGG rules. Further related contributions are those based on design patterns for model transformation [ 7, 10 ]. Although such design languages help to share solution strategies based on a common representation, our experience (especially with TGGs and QVT-R) is that the concrete choice of transformation language has a substantial impact on the proper way of thinking about a notion of consistency. In case of TGGs, for example, one must refrain from planning with control flow structures or (recursive) explicit rule invocations; features that are not necessarily excluded from other (bx ) languages or general design pattern languages. Finally, this paper was inspired by the work of Zambon and Rensink in [25], where they demonstrate best practices for the transformation tool GROOVE using the N-Queens problem.

Conclusion and Future Work

In this paper, we have presented not only a basic introduction to TGGs, but also a process and a set of guidelines to support the systematic development of a TGG from a clear, but unformalised understanding of a bx.

We have, however, only been able to handle the basics and leave guidelines for advanced language features and techniques to future work including: negative application conditions, multi-amalgamation, user-defined attribute manipulation, test generation, and how best to specify the correspondence metamodel.

Acknowledgements. The first author of this paper received partial funding from the European Union’s Seventh Framework Program (FP7/2007-2013) for CRYSTAL-Critical System Engineering Acceleration Joint Undertaking under grant agreement No 332830 and from Vinnova under DIARIENR 2012-04304. [ 1 ] Anthony Anjorin. Synchronization of Models on Different Abstraction Levels using Triple Graph Grammars.

Phd thesis, Technische Universit¨at Darmstadt, 2014. [ 2 ] Anthony Anjorin, Erhan Leblebici, Andy Schu¨rr, and Gabriele Taentzer. A Static Analysis of Non-Confluent Triple Graph Grammars for Efficient Model Transformation. In Holger Giese and Barbara K¨onig, editors, ICGT 2014, volume 8571 of LNCS, pages 130–145. Springer, 2014. [ 3 ] Anthony Anjorin, Karsten Saller, Malte Lochau, and Andy Schu¨rr. Modularizing Triple Graph Grammars Using Rule Refinement. In Stefania Gnesi and Arend Rensink, editors, FASE 2014, volume 8411 of LNCS, pages 340–354. Springer, 2014. [ 4 ] Julian C. Bradfield and Perdita Stevens. Recursive Checkonly QVT-R Transformations with General when and where Clauses via the Modal Mu Calculus. In Juan de Lara and Andrea Zisman, editors, FASE 2012, volume 7212 of LNCS, pages 194–208. Springer, 2012. [ 5 ] James Cheney, James McKinna, Perdita Stevens, and Jeremy Gibbons. Towards a Repository of Bx Examples. In K. Selccuk Candan, Sihem Amer-Yahia, Nicole Schweikardt, Vassilis Christophides, and Vincent Leroy, editors, BX 2014, volume 1133 of CEUR Workshop Proc., pages 87–91, 2014. [ 6 ] Krzysztof Czarnecki, John Nathan Foster, Zhenjiang Hu, Ralf L¨ammel, Andy Schu¨rr, and James Terwilliger.

Bidirectional Transformations: A Cross-Discipline Perspective. In Richard F. Paige, editor, ICMT 2009, volume 5563 of LNCS, pages 260–283. Springer, 2009. [ 7 ] Hu¨seyin Ergin and Eugene Syriani. Towards a Language for Graph-Based Model Transformation Design Patterns. In Davide Di Ruscio and D´aniel Varr´o, editors, ICMT 2014, volume 8568 of LNCS, pages 91–105.

Springer, 2014. [ 8 ] Joel Greenyer and Jan Rieke. Applying Advanced TGG Concepts for a Complex Transformation of Sequence Diagram Specifications to Timed Game Automata. In Andy Schu¨rr, D´aniel Varr´o, and Gergely Varro´, editors, AGTIVE 2011, volume 7233 of LNCS, pages 222–237. Springer, 2012. [ 9 ] Esther Guerra and Juan de Lara. An Algebraic Semantics for QVT-Relations Check-only Transformations.

Fundamentae Informatica, 114(1):73–101, 2012. [23] Martin Wieber, Anthony Anjorin, and Andy Schu¨rr. On the Usage of TGGs for Automated Model Transformation Testing. In Davide Di Ruscio and D´aniel Varr´o, editors, ICMT 2014, volume 8568 of LNCS, pages 1–16. Springer, 2014.

References

[1] Faris Abou-Saleh , James Cheney, Jeremy Gibbons, James McKinna , and Perdita Stevens . Notions of bidirectional computation and entangled state monads . In Proceedings of MPC, number 9129 in LNCS , 2015 . To appear.

[2] Julian C. Bradfield and Perdita Stevens . Recursive checkonly QVT-R transformations with general when and where clauses via the modal mu calculus . In Proceedings of FASE , volume 7212 of LNCS , pages 194 - 208 . Springer, 2012 .

[3] Peter Buneman , Sanjeev Khanna, and Wang Chiew Tan . On propagation of deletions and annotations through views . In Proceedings of PODS , pages 150 - 158 . ACM, 2002 .

[4] James Cheney , James McKinna , Perdita Stevens , and Jeremy Gibbons . Towards a repository of bx examples . In K. Selc¸uk Candan, Sihem Amer-Yahia , Nicole Schweikardt, Vassilis Christophides, and Vincent Leroy, editors, Proceedings of the Workshops of EDBT/ICDT , volume 1133 of CEUR Workshop Proceedings , pages 87 - 91 . CEUR-WS.org, 2014 .

[5] 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 .

[6] Zinovy Diskin , Yingfei Xiong, Krzysztof Czarnecki, Hartmut Ehrig, Frank Hermann, and Fernando Orejas . From state- to delta-based bidirectional model transformations: The symmetric case . In Proceedings of MODELS , pages 304 - 318 , 2011 .

[7] Stephen J. Hegner . An order-based theory of updates for closed database views . Ann. Math. Artif. Intell., 40 ( 1-2 ): 63 - 125 , 2004 .

[8] Stephen J. Hegner . Information-based distance measures and the canonical reflection of view updates . Ann. Math. Artif. Intell., 63 ( 3-4 ): 317 - 355 , 2011 .

[9] Michael Johnson and Robert D. Rosebrugh . Delta lenses and opfibrations . ECEASST , 57 , 2013 .

[10] Michael Johnson , Robert D. Rosebrugh , and Richard J. Wood . Lenses, fibrations and universal translations . Mathematical Structures in Computer Science , 22 : 25 - 42 , 2 2012 .

[11] Erhan Leblebici , Anthony Anjorin, Andy Schu¨rr, Stephan Hildebrandt, Jan Rieke, and Joel Greenyer . A comparison of incremental triple graph grammar tools . ECEASST , 67 , 2014 .

[12] Nuno Macedo and Alcino Cunha . Implementing QVT-R bidirectional model transformations using alloy . In Vittorio Cortellessa and D´aniel Varr´o, editors, Proceedings of FASE , volume 7793 of LNCS , pages 297 - 311 . Springer, 2013 .

[13] Nuno Macedo , Hugo Pacheco, Alcino Cunha, and Jos´e Nuno Oliveira. Composing least-change lenses . ECEASST , 57 , 2013 .

[14] Lambert Meertens . Designing constraint maintainers for user interaction . Unpublished manuscript , available from http://www.kestrel.edu/home/people/meertens/, June 1998 .

[15] Perdita Stevens . A simple game-theoretic approach to checkonly QVT Relations . Journal of Software and Systems Modeling (SoSyM) , 12 ( 1 ): 175 - 199 , 2013 . Published online, 16 March 2011 .

[16] Perdita Stevens . Bidirectionally tolerating inconsistency: Partial transformations . In Stefania Gnesi and Arend Rensink , editors, Proceedings of FASE , volume 8411 of LNCS , pages 32 - 46 . Springer, 2014 .

[17] W A Sutherland . Introduction to metric and topological spaces . Oxford University Press, 1975 .

[10] Esther Guerra , Juan de Lara, Dimitrios S. Kolovos, Richard F. Paige, and Osmar Marchi dos Santos. Engineering model transformations with transML . SoSym , 12 ( 3 ): 555 - 577 , 2013 .

[11] Stephan Hildebrandt , Leen Lambers, Holger Giese, Dominic Petrick, and Ingo Richter . Automatic Conformance Testing of Optimized Triple Graph Grammar Implementations . In Andy Schu¨rr, D´aniel Varr´o, and Gergely Varr´o, editors, AGTIVE 2011 , volume 7233 of LNCS , pages 238 - 253 . Springer, 2011 .

[12] Stephan Hildebrandt , Leen Lambers, Holger Giese, Jan Rieke, Joel Greenyer, Wilhelm Sch¨afer, Marius Lauder, Anthony Anjorin, and Andy Schu¨rr. A Survey of Triple Graph Grammar Tools . In Perdita Stevens and James Terwilliger, editors, BX 2013 , volume 57 of ECEASST. EASST , 2013 .

[14] Felix Klar , Alexander K¨onigs , and Andy Schu¨rr. Model Transformation in the Large . In Ivica Crnkovic and Antonia Bertolino, editors, ESEC-FSE 2007 , pages 285 - 294 . ACM, 2007 .

[15] Erhan Leblebici , Anthony Anjorin, and Andy Schu¨rr. A Catalogue of Optimization Techniques for Triple Graph Grammars . In Hans-Georg Fill , Dimitris Karagiannis, and Ulrich Reimer, editors, Modellierung 2014 , volume 225 of LNI , pages 225 - 240 . Gesellschaft fu¨r Informatik, 2014 .

[16] Erhan Leblebici , Anthony Anjorin, Andy Schu¨rr, Stephan Hildebrandt, Jan Rieke, and Joel Greenyer . A Comparison of Incremental Triple Graph Grammar Tools . In Frank Hermann and Stefan Sauer, editors, GT-VMT 2014 , volume 67 of ECEASST. EASST , 2014 .

[17] OMG. MOF2 . 0 query/view/transformation (QVT) version 1.2 . OMG document formal/2015-02-01, 2015 . Available from www. omg.org.

[18] Andy Schu ¨rr. Specification of Graph Translators with Triple Graph Grammars . In Ernst W. Mayr, Gunther Schmidt, and Gottfried Tinhofer, editors, WG 1994 , volume 903 of LNCS , pages 151 - 163 . Springer, 1994 .

[19] Perdita Stevens . A Landscape of Bidirectional Model Transformations . In Ralf L¨ammel, Joost Visser, and Joa˜o Saraiva, editors, GTTSE 2007 , volume 5235 of LNCS , pages 408 - 424 . Springer, 2008 .