ISSN 1884-0760

GRACE TECHNICAL REPORTS

Towards Bidirectional Transformations on Ordered
GraphsSoichiro Hidaka Kazuyuki Asada Hiroyuki Kato
Keisuke Nakano Zhenjiang Hu

GRACE-TR 2011–07

December 2011

CENTER FOR GLOBAL RESEARCH IN
ADVANCED SOFTWARE SCIENCE AND ENGINEERINGNATIONAL INSTITUTE OF INFORMATICS
2-1-2 HITOTSUBASHI, CHIYODA-KU, TOKYO, JAPANWWW page: http://grace-center.jp/

The GRACE technical reports are published as a means to ensure timely dissemination ofscholarly and technical work on a non-commercial basis. Copyright and all rights therein are
maintained by the authors or by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information
will adhere to the terms and constraints invoked by each author’s copyright. These works
may not be reposted without the explicit permission of the copyright holder.

1

Towards Bidirectional Transformations on Ordered Graphs∗
Soichiro Hidaka1 , Kazuyuki Asada1 , Hiroyuki Kato1 , Keisuke Nakano2 , andZhenjiang Hu1
National Institute of Informatics1
University of Electro-Communications2
Abstract: The linguistic (language-based) approach plays an important role in development of structured and well-behaved bidirectional transformations. It has beensuccessfully applied to solve the challenging problem of bidirectional transformation on graphs, where a clear bidirectional semantics is given based on a bulk semantics of the structural recursion. However, the graphs that can be dealt with are
limited to unordered ones, and it has not yet been known how to treat ordered graphs
such as XML graphs in which the child nodes of a node are ordered. In this paper,
we show that the bulk semantics of structural recursion can be extended to orderedgraphs, and that a clear bidirectional semantics of a new graph transformation language can be defined. The key technical point is a novel definition of bisimilarity
between ordered graphs with ε edges.
Keywords: Ordered Graphs, Graph Transformation, Bisimulation

1

Introduction

Bidirectional transformations [FGM+ 05, CFH+ 09] provide a novel mechanism for synchronizing and maintaining the consistency of information between input and output. They are pervasive and has many potential applications, including the synchronization of replicated data in
different formats [FGM+ 05], presentation-oriented structured document development [HMT08],
interactive user interface design [Mee98], coupled software transformation [Läm04], and thewell-known view updating mechanism which has been intensively studied in the database community [BS81, Heg90].
The linguistic (language-based) approach [FGM+ 05] gives a promising way for developmentof structured and well-behaved bidirectional transformation, in which every expression simultaneously specifies both a forward and the responding (correct) backward transformation, andevery composite of expressions defines a structured way of gluing smaller bidirectional transformations to a bigger one. Despite its usefulness for bidirectional transformations on lists andtrees [FGM+ 05, BFP+ 08, MHN+ 07, HMT08, Voi09, VHMW10, WGW11], it is a challenge todeal with bidirectional transformation on graphs. First, unlike lists and trees, there is no unique
way of representing, constructing, or decomposing a general graph, and this requires a more
precise definition of equivalence between two graphs. Second, graphs have shared nodes andcycles, which makes both forward and backward computation more complicated than that ontrees; naı̈ve computation would visit the same nodes many times and possibly infinitely.
∗This is a full version of the paper submitted to the First International Workshop on Bidirectional Transformations(2012). EASST style file is used to format this article.

2

2 UNCALO : A TRANSFORMATION LANGUAGE FOR ORDERED GRAPHS

In our previous work [HHI+ 10], we challenged the problem by showing that the linguistic
approach can be applied to bidirectional transformation on graphs, where a clear bidirectionalsemantics is given for UnCAL, a graph algebra for the known graph query language UnQL
[BFS00]. The key to this success is the bulk semantics of the structural recursion: a structural
recursion is evaluated by first processing in parallel on all edges of the input graph and then
combining the results. This bulk semantics relies on introduction of ε edges to graphs, providing
a smart way of treating shared nodes and cycles in graphs and of tracing back from the view tothe source.
However, the graphs that can be dealt with in this manner must be unordered. It has not yet
been known how to treat ordered graphs such as XML graphs in which the child nodes of a node
are ordered. One might consider encoding the ordered graphs in terms of unordered ones byintroducing specialized edge labels, but this would make it difficult to keep consistency of theselabels during transformation. In fact, it is an open problem, as pointed out in [BFS00], how
to structure transformations on ordered graphs. In particular, it is unclear how to define a bulk
semantics for transformations on ordered graphs.
In this paper, we show that the bulk semantics can be extended to ordered graphs, and thata clear bidirectional semantics of UnCALo , an ordered version of UnCAL, can be defined.
The main technical contributions are three folds. First, we design a new graph transformation
language UnCALo (Section 2), which is similar to the graph algebra UnCAL [BFS00] for unordered graphs. Next, we give a novel definition of bisimulation relation on ordered graphs withε edges, propose the bulk semantics of structural recursion, and prove bisimulation genericity(well-definedness on bisimilarity) of the constructors and the structural recursion (Section 3).
Finally, based on the above results, we show that the bidirectionalization method in [HHI+ 10]
can be adapted to define bidirectional semantics of UnCALo (Section 4).

2

UnCALo : A Transformation Language for Ordered Graphs

UnCALo is a graph transformation language, which is similar to UnCAL [BFS00], but can distinguish orders of outgoing edges. In UnCALo , we will use [] and ++ for ordering instead of{} and ∪ used in UnCAL. The purpose of this section is to give an intuition of UnCALo . The
formal definition of the semantics of UnCALo is shown in Section 3.

2.1

Graph ModelIn UnCALo , graphs are rooted, directed, and edge-labeled graphs with order on outgoing edges.
This graph data model has two prominent features, markers and ε -edges. Nodes may be marked
with input and output markers, which are used as an interface to connect them to other graphs.
An ε -edge represents a shortcut of two nodes, working like the ε -transition in an automaton. We
use L to denote the set of labels, Lε to denote L ∪ {ε }, X to denote the set of input markers,
and Y to denote the set of output markers.
An ordered graph G is represented as a triple (V, B, I), where V is a set of nodes, B : V →List(Lε ×V +Y ) is a function that maps a node to a list of elements, which is either a pair of alabel and a node, or an output marker, and I : X → V is a function that maps an input marker to a

2.1

Graph Model

3

1

0

a b c

1
2

3

4

c

a b

a a

61
5

2

3

c
62

da

a d

51

52

42
c

4
c c

d
6

(a) A Simple Graph

41(b) An Equivalent Graph(c) Result of a2d xc on (a)Figure 1: Graph Equivalence Based on Bisimulatione ::= [] | [l : e] | e ++ e | &x := e | &y | ()| e ⊕ e | e @ e | cycle(e){ constructor }| $g{ graph variable }| let $g = e in e
{ variable binding }| if l = l then e else e{ conditional }| rec(λ ($l, $g).e)(e) { structural recursion application }l ::= a | $l
{ label (a ∈ Lε ) and label variable }Figure 2: UnCALo Language

node, which is called input node. Unlike input markers, more than one node can be marked with
an identical output marker. They are called output nodes. Intuitively, input nodes are root nodesof the graph (we allow a graph to have multiple root nodes, and for singly rooted graphs, we often
use default marker & to indicate the root), while an output node can be seen as a “context-hole”
of graphs where an input node with the same marker will be plugged later.
Note that multiple-marker graphs are meant to be an internal data structure for graph composition. In fact, initial source graphs of our transformation have one input marker (singlerooted) and no output markers (no holes). For instance, the graph in Fig. 1(a) is denoted by(V, B, I) where V = {1, 2, 3, 4, 5, 6}, B(1) = [(a, 2), (b, 3), (c, 4)], B(2) = [(a, 5)], B(3) = [(a, 5)],
B(4) = [(c, 4)], B(5) = [(d, 6)], B(6) = [], and I(&) = 1.

Notion of Graph Equivalence While a formal definition of graph equivalence will be given
in Section 3, two graphs are value equivalent if they are bisimilar. For instance, the graph inFig. 1(b) is value equivalent to the graph in Fig. 1(a); the new graph has an additional ε -edge(denoted by the dotted line), duplicates the graph rooted at node 5, and unfolds and splits the cycle at node 4. Unreachable parts are also disregarded, i.e., two bisimilar graphs are still bisimilar
if one adds subgraphs unreachable from input nodes.

4

2.2

2 UNCALO : A TRANSFORMATION LANGUAGE FOR ORDERED GRAPHS

Graph Constructors

Figure 3 summarizes the nine graph constructors. To treat order of outgoing edges, we use [] and++ instead of {} and ∪ used in UnCAL. Here, [] constructs a root-only graph, [a : G] constructs
a graph by adding an edge with label a ∈ Lε pointing to the root of graph G, and G1 ++ G2 adds
two ε -edges from a new root to the roots of G1 and G2 , respectively. Also, &x := G associates
an input marker, &x, to the root node of G, &y constructs a graph with a single node marked
with an output marker &y, and () constructs an empty graph that has neither a node nor an edge.
Furthermore, G1 ⊕G2 constructs a graph by using a componentwise (V, B and I) union. ++ differsfrom ⊕ in that ++ unifies input nodes while ⊕ does not. ⊕ requires input markers of operands
to be disjoint, while ++ requires them to be identical. G1 @ G2 composes two graphs verticallyby connecting the output nodes of G1 with the corresponding input nodes of G2 with ε -edges,
and cycle(G) connects the output nodes with the input nodes of G to form cycles. The formal
definition of the semantics of these constructors can be found in Section 3. It is worth noting that
this set of constructors are powerful enough to describe any ordered graphs.

2.3

UnCALo Syntax

The syntax of UnCALo is depicted in Fig. 2. As will be seen in Section 3, UnCALo is bisimulation generic, i.e., for bisimilar inputs, each UnCALo expression results in bisimilar result.
It consists of the graph constructors, variables1 , variable bindings, conditionals, and structural
recursion. We have already described the graph constructors, while variables, variable bindings
and conditionals are self explanatory. Now we introduce structural recursion, which is a powerful mechanism in UnCALo to describe graph transformations. A structural recursion is a function
f , which satisfies the following equations.
f ([])= []f ([$l : $g])
= e @ f ($g)
f ($g1 ++ $g2 ) = f ($g1 ) ++ f ($g2 ),and f can be encoded by rec(λ ($l, $g).e). For [], f results in []. For a graph with an edge
labelled $l connected to a graph $g, f results in connecting vertically the result of e with theresult of recurring f to $g. For a graph with $g1 preceding $g2 , f results in concatenating two
graphs of f ($g1 ) and f ($g2 ).
Example 1 The following structural recursion a2d xc replaces all labels a with d and contractedges labeled c.
a2d xc($db) = rec(λ ($l, $g). if $l = a then[d : &]
else if $l = c then [&]else[$l : &]) ($db)

Applying the function a2d xc to the graph in Fig. 1(a) yields the graph in Fig. 1(c).
1 We prefix $ to represent variables.

5&x1 ... &xm

a

&z
G1

G
[a : G][]G2

G1 ++ G2G&z := G&z&z()

&x1 ... &xm&x1 ... &xm&x1’ ... &xm’

G1

G2

&y1 ... &yn &y1 ... &yn
G1G2

G1
&y1 ... &yn
εε&y1 ... &yn
G2&z1 ... &zp
G1@G2

ε

ε
&x1 ... &xm
G&x1 ... &xm &y1 ... &yn
cycle (G)Figure 3: Graph Constructors

Example 2 Consider an ordered graph representation of books. Since “sections” are ordered
and there are some references in books, we can see books as ordered graphs. The following
structural recursion toc, which is adapted from [RSGV09], computes the table of contents ofbooks in which sections can be arbitrarily nested:
toc($db) = rec(λ ($l, $g). if $l = section then [section : [gettitle($g), &]]else &) ($db)

where the function gettitle results in the title of the section.
gettitle($g) = rec(λ ($l1 , $g1 ). if $l1 = title then [title : rec(λ ($l2 , $g1 ).[$l2 : []]) ($g1 )]else []) ($g)

3Ordered Graph and Structural Recursion

In the previous section, we gave syntax of UnCALo , its intuitive meaning, and its usage. In
this section, we give semantics of UnCALo . In the next section, we extend the semantics here
for bidirectional transformation, where ε -edge and bulk semantics for structural recursion—
main contents in this section—are importantly used to keep source information during forward
transformation. Thus we heavily use ε -edge, so the bisimilarity for ordered graph with ε -edges
is important.
Here we first give definitions of ordered graph and its bisimilarity. These ordered graphs
up to bisimilarity form the domain of the semantics of UnCALo . Next we define graph constructors and structural recursion with bulk semantics. Then we show bisimulation genericity(well-definedness on bisimilarity) of the graph constructors and the structural recursion (Theorem 1).

3 ORDERED GRAPH AND STRUCTURAL RECURSION6

The reader who believe our proofs and naturality of definitions can skip this section except for
Section 3.1, Definitions 6 and 7.

3.1

Formal Definition of Ordered Graph

Definition 1 (Ordered Graph) Let L be a set of labels, and Lε be the disjoint union L ∪ {ε }.
Let X be a finite set of input markers and Y be a finite set of output markers.
An ordered graph, or just a graph G is a triple (V, B, I) where• V is a set of nodes,• B : V → n∈N (Lε × V + Y )n is a function, which maps a node to its ordered branches
consisting of labeled edges or output markers, and• I : X → V is a function, which determines roots (input nodes) of the graph.
∏

The set of all graphs (defined with X and Y ) is denoted by DBYX (meaning DataBase following [BFS00]). For a graph G, we refer each component of the triple by record notation withlabels V, B, I: i.e., G = (G.V, G.B, G.I).
Remark 1 In the paper [BFS00], unordered graph was defined additionally with the following
three requirements: an input function I is injective; there is no incoming edge to an input node;and there is no outgoing edge from an output node. While, the above definition of ordered graphis relaxed on such points. The both styles are in fact equivalent: i.e., for the above style of agraph, if we extend each input node with a fresh epsilon edge incoming from a fresh new input
node, and also replace each output marker occurrence on an output node by a fresh epsilon edge
outgoing to a fresh node having only the branch of the output marker, then the resulting graphsatisfies the above three requirements, and still is bisimilar (Definition 5) to the given graph. Thistransformation is possible for both unordered case and ordered case.
As meta-variables for markers, we use &x, &y, &z, etc. Since we often consider single-rooted
graphs, i.e., graphs whose sets of input markers are singleton, we choose a default marker de{&}noted by &, and DBY is denoted by DBY .
In the above definition, n∈N (Lε ×V +Y )n = List(Lε ×V +Y ). To represent ordered branch,“list in polynomial style” is more essential than “list as initial algebra”, since with polynomial
style, the more generalized notion of graph with countably wide ordered branch can be similarly
defined with B : V → L∈L (Lε ×V +Y )L where L is the set of countable linear ordered sets (upto order isomorphism).
For a list x, |x| denotes the length of x, and we regard |x| also as the set of component-indicesof x, i.e., |x| = {0, ..., |x|−1}. Then for i ∈ |x|, x.i denotes the i-th component of x. We often
represent a list as [xi ]i∈n , as well as an extensional style such as [x, y, z]. For a tuple x ∈ ∏i∈I Xi
and an index i ∈ I, we use x.i to denote the i-th component of x: e.g., for x ∈ A × B, x = (x.0, x.1).
For sets A and B, an element of the coproduct A + B is either inl (a) with a ∈ A exclusively orinr (b) with b ∈ B. For ternary coproduct, we use inl , inm , and inr .
For a graph G = (V, B, I), a node v ∈ V , and a branch index i ∈ |B(v)|, the list component B(v).i
∏

∏

def

def

is either an l-labeled edge E (l, v0 ) = inl (l, v0 ) from v to v0 , or an output marker O (&y) = inr (&y).
Do not confuse the notion of branch with the notion of edge; a branch might be an output marker

3.2 Bisimilarity

7

G0

G00

0

0

a

∼

a

G1

0

0

1

2

a

1
3

a
1

∼

a
2

G01

1

a
3

Figure 4: graphs with left-to-right-stream branching and with right-to-left-stream branchingas well as an edge. An output marker can be considered as a “future (collection of) branches”;
an output marker is a variable (or place holder) to which the all branches of a root of anothergraph can be “substituted” through an ε -edge by @ operator or cycle operator (see Figure 3 andDefinition 6).
For a graph G, we call G finite if G.V is finite. In this section, we also consider infinite graphs
because we need infinite graph (in fact infinite tree) to define bisimilarity even for finite graph.
In other sections, we treat only finite graphs and call them just (ordered) graphs.
For a graph G ∈ DBYX , and a node v ∈ G.V, G|v denotes the graph in DBY whose set of nodes
are restricted to the set of all nodes “accessible through consecutive branches” from v.
For a graph G ∈ DBYX , G is a tree if (i): G.I is injective, (ii): for every root node, there is no
incoming edge, (iii): for every non-root nodes, there is exactly one incoming edge, and (iv) any
node can be accessible from a root node in finite steps. (For finite graphs, the condition (iv) is
derived from the conditions (ii) and (iii).) The conditions (ii) and (iii) keep out cycle and sharing
from tree. Note that if t is a tree, so is t|v for any v ∈ t.V, and also that any multi-rooted treet ∈ DBYX is the disjoint union of the family (t|t.I(&x) ))&x∈X of the single-rooted trees.

3.2

Bisimilarity

Bisimilarity between ordered graph is—if the notion does not involve ε -edge—easily definedwith a general coalgebraic definition (e.g. [Rut00, SR11]) applied to the endofunctor V 7→
List(L ×V +Y ). However, for ordered graph with ε -edges, the definition of bisimilarity is not
obvious. In the unordered case, we can take the approach in the paper [BJ10], but for orderedcase, it is not available.
First let us see the bisimilarity for the case without ε -edge.
Definition 2 For ordered graphs G, G0 ∈ DBYX without ε -edges, G and G0 are bisimilar (anddenoted by G ∼L G0 ) if there is a relation R between G.V and G0 .V such that (i): for every
input marker &x ∈ X, (G.I(&x))R(G0 .I(&x)), and (ii): R is a bisimulation relation: i.e., for any
vRv0 , |G.B(v)| = |G0 .B(v0 )|, and then for any i ∈ |G.B(v)|, either if (G.B(v)).i = E (l, v1 ), thenthere is v01 ∈ G0 .V such that (G0 .B(v0 )).i = E (l, v01 ) and v1 Rv01 , or if (G.B(v)).i = O (&y), then
(G0 .B(v)).i = O (&y).
Now let us see some ordered graphs with ε -edges, to have some feeling of bisimilarity. Consider graphs in Figure 4. The graphs Gi should be intuitively bisimilar respectively to their
1-step-unfolding G0i , because unfolding generally maintains bisimilarity. Here, we should distinguish G0 from G1 . This is because, observing their further unfolding, it is found that G0 is a tree

3 ORDERED GRAPH AND STRUCTURAL RECURSION

8

with height one and with countable width of branch, and the order of the branching is like an
infinite stream from left to right; on the other hand, the graph G1 is similar one but the branch islike an infinite stream from right to left.
In the case without ε -edge, we just compare the list of branches under the condition “|G.B(v)| =|G0 .B(v)|” above; on this point for the case with ε -edge, we first extend the notion of list of
branches to that of linear ordered set of branches, and then compare them in terms of orderisomorphism. For the examples, G0 has no maximum (right side) but has minimum (left side),
while G1 has maximum and has no minimum, so they are not isomorphic, and hence not bisimilar. (Order isomorphism was implicit in the case without ε -edge, since for finite linear orderedsets, to be order isomorphic is determined just by their cardinalities.) In order to define sets ofall such branches and to define linear orders on them, we first unfold graphs to trees.
Thus we define bisimilarity for ordered graph with ε -edges in two steps: we first unfold graphs
to trees, which might be infinite even for finite graphs; and then determine “proper” branches bytaking transitive closure of ε -edges, and “bi-simulate” them with order isomorphisms.
The definition of unfolding of graph to tree is usual one, which keeps ε -edges, regarding ε asa normal label in L .
Definition 3 (Unfolding) Let G = (V, B, I) ∈ DBYX . We define a tree uf(G) ∈ DBYX as in thefollowing.
We will define only for the case that X is a singleton, say {&}, then for the other case, we candefine uf(G) as the disjoint union tree of family (uf(G|(G.I)(&x) ))&x∈X of single-rooted graphs.
First we define a family of disjoint sets (Vn )n∈N by induction on n ∈ N, as Vn will be theset of n-depth nodes v ∈ uf(G).V, and there v = (the depth n of v, the parent node of v, thecorresponding node in the original graph G, the branch index of v).
def• V0 = { (0, ⊥, I(&), ⊥) }, where the element will be the root, hence ⊥ in the two undefinable
components is just some dummy.
def• Vn+1 = { (n+1, x, v, i) | x ∈ Vn , i ∈ |B(x.2)|, B(x.2).i = inl (l, v) }def∪

Then uf(G) = (0n∈N Vn , B , {& 7→ (0, ⊥, I(&), ⊥)}) ∈ DBY where for x ∈ Vn ,[def
B0 (x) =]B(x.2).i = E (l, v) ⇒ E (l, (n+1, x, v, i))= O (&y) ⇒ O (&y)

i∈|B(x.2)|

For graphs G and G0 (possibly with ε -edges), we can define their bisimilarity observing ε(denoted by G ∼! G0 ) just as G ∼Lε G0 , where we regard ε as a normal label. Then it is easily
shown that G ∼! G0 if and only if uf(G) and uf(G0 ) are (uniquely) isomorphic. We use this notionof bisimilarity observing ε in the proof of bisimulation genericity (Theorem 1).
Now let us go to the second step; first we consider transitive closure of ε -edges.
For a tree T ∈ DBYX and a node v ∈ T.V, let v0 be a self-or-ancestor of v, i.e., there is a path
l

ln−1

def

lj

0
v0 →
i0 ...vn−1 → in−1 vn ( = v)(n ∈ N) where v j →i j v j+1 means G.B(v j ).i j = E (l j , v j+1 ). Notethat by the condition of tree, such path is unique. Then for a branch index i ∈ |T.B(v)| of v, thepair (v, i) is proper branch of v0 if (i): all l j are ε , and (ii): if T.B(v).i = E (l, v0 ) for some l andv0 , then l 6= ε . (Note that for the case that T.B(v).i = O (&y), the condition (ii) holds.) For a tree
T ∈ DBYX and a node v0 ∈ T.V, Pb(T, v0 ) denotes the set of all proper branches of v0 .

3.3 Graph Constructors and Bulk Semantics for Structural Recursion

9

Then there is a natural linear order ≤Pb on Pb(T, v0 ): for two different proper branches(v, i) and (v0 , i0 ), we compare the two branches of the lowest one—in terms of depth of tree—
ε

ε

def

among common self-or-ancestors of v and v0 . Formally, let v0 →i0 ...vn−1 →in−1 vn ( = v) and
def

ε

ε

v00 ( = v0 ) →i00 ...v0n0 −1 →i0 0

def

n −1

def

v0n0 ( = v0 ) be respectively the paths from v0 to v and v0 ; and also let

def

in = i and i0n0 = i0 . Then by conditions in the definition of proper branch, (vmin(n,n0 ) , imin(n,n0 ) ) 6=
(v0min(n,n0 ) , i0min(n,n0 ) ), hence we can take the least k such that (vk , ik ) 6= (v0k , i0k ) as k0 . Then we candefshow that vk0 = v0k0 , hence ik0 6= i0k0 . Now we define as (v, i) <Pb (v0 , i0 ) ⇐⇒ ik0 < i0k0 .
Now let us go to the second step for defining bisimilarity of ordered graph.
Definition 4 (Bisimilarity for Tree) For a pair of trees T, T 0 ∈ DBYX , T and T 0 are bisimilar if
there is a relation R between T.V and T 0 .V such that• for every input marker &x ∈ X, (T.I(&x))R(T 0 .I(&x)), and• R is a bisimulation relation: i.e., for any v0 Rv00 , there is an order isomorphism f :(Pb(T, v0 ), ≤Pb ) → (Pb(T 0 , v00 ), ≤Pb ) satisfying the following property. For any proper
branch (v, i) ∈ Pb(T, v0 ), let (v0 , i0 ) be f (v, i). Then,– for any l ∈ L , u ∈ T.V, if T.B(v).i = E (l, u), then there exist u0 such that T 0 .B(v0 ).i0 =E (l, u0 ) and uRu0 , and– for any &y ∈ Y , if T.B(v).i = O (&y), then T 0 .B(v0 ).i0 = O (&y).
It can be checked that the above bisimilarity relation is symmetric and an equivalence relation.
Definition 5 (Bisimilarity for Ordered Graph with ε -edges) For graphs G, G0 ∈ DBYX , G and
G0 are bisimilar (and denoted by G ∼ G0 ) if uf(G) and uf(G0 ) are bisimilar (in the sense of
Definition 4). (Bisimilarity is called value equivalence in [BFS00].)
For a tree T ∈ DBYX , T and uf(T ) are equal up to the unique isomorphism. Hence for any pairof trees, the two bisimilarity above are equivalent, and not ambiguous.
For a pair of graphs G, G0 ∈ DBYX , if G and G0 has no ε -edge, then G ∼ G0 ⇐⇒ G ∼! G0 ⇐⇒G ∼L G0 . Otherwise, if G ∼! G0 then G ∼ G0 , but the converse is not necessarily true.

3.3

Graph Constructors and Bulk Semantics for Structural Recursion

Now we define graph constructors and a structural recursion; we use the same function name as
the name of a function symbol in the syntax.
Definition 6(Graph Constructors)def• [] = ({&}, {& 7→ []}, id{&} ) ∈ DBY
def• For G ∈ DBY , [l : G] = (G.V∪{v0 : fresh}, G.B∪{v0 7→ [E (l, G.I(&))]}, {&7→ v0 }) ∈ DBY
def• For Gl ∈ DBYX and Gr ∈ DBYX , Gl ++ Gr = (Gl .V + X + Gr .V, B0 , inm ) ∈ DBYX where

3 ORDERED GRAPH AND STRUCTURAL RECURSION10[B0 (ink (v))
B0 (in

def

=

(
)
(
)]
Gk .B(v).i = E l, v0 ⇒ E l, ink (v0 )⇒ O (&y)= O (&y)(k=l or r)i∈|gk .B(v)|defm (&x)) = [E (ε , inl (Gl .I(&x))) , E (ε , inr (Gr .I(&x)))]
{&x}

def

• For G ∈ DBY , (&x := G) = (G.V, G.B, {&x 7→ G.I(&)}) ∈ DBY
def• For &y ∈ Y , &y = ({&}, {& 7→ [O (&y)]}, id{&} ) ∈ DBY
def• () = (0,/ 0,/ id0/ ) ∈ DBY0/
def• For Gl ∈ DBYXl and Gr ∈ DBYXr such that Xl ∩ Xr = 0,
/ Gl ⊕ Gr = (Gl .V + Gr .V, B0 , I 0 ) ∈Xl ∪Xr
DBY
where
[
(
)
(
)]
Gk .B(v).i = E l, v0 ⇒ E l, ink (v0 )def0B (ink (v)) =(k=l or r)= O (&y) ⇒ O (&y)
i∈|Gk .B(v)|def0I (&x) = inl (Gl .I(&x)) (if &x ∈ Xl ) or inr (Gr .I(&x)) (if &x ∈ Xr )def

• For Gl ∈ DBYX and Gr ∈ DBYZ , Gl @ Gr = (Gl .V + Gr .V, B0 , inl ◦ Gl .I) ∈ DBXZ where
(
)
(
)


Gk .B(v).i = E l, v0 ⇒ E l, ink (v0 )
{
def


B0 (ink (v)) = 
k = l ⇒ E (ε , inr (Gr .I(&w))) (k=l or r)= O (&w) ⇒= r ⇒ O (&w)

i∈|gk .B(v)|def• For G ∈ DBXX∪Y such that X ∩Y = 0,
/ cycle(G) = (G.V, B0 , G.I) ∈ DBYX where][( 0)
B(v).i
=
E
l,
v
or
O
(&y)
(&y
∈
Y
)
⇒
B(v).idef
B0 (v) == O (&x) (&x ∈ X)
⇒ E (ε , G.I(&x))
i∈|B(v)|Remark 2 The definition of cycle above is different from that in the paper [BFS00]: i.e., wejust added cycling epsilon edges, while in loc. cit. additionally each input node is extended
with a fresh epsilon edge incoming from a fresh new input node. This is just (a part of) thetransformation in Remark 1 and hence the both are equivalent.
Definition 7 (Bulk Semantics of Structural Recursion) For e : L × DBY → DBZZ , a structural
recursion function (for ordered graph) rec(e) : DBYX → DBZ×X
Z×Y is defined as the following.
Let G = (V, B, I) ∈ DBYX . We extend e to ē : Lε × DBY → DBZZ which maps (ε , ) to thedef“identity” graph (Z, {&z 7→ [O (&z)]}, idZ ). For a list x ∈ List(Lε ×V +Y ), let x|edge = {(i, l, v) ∈N × Lε ×V | i ∈ |x|, x.i = E (l, v)}.
def

Then rec(e)(G) = (V 0 , B0 , I 0 ) wheredef• V 0 = (Z ×V ) + (∏v∈V,(i,l,v0 )∈B(v)|edge ē(l, G|v0 ).V)v,i,l,v0 , in the following.)(n Lε × (Z ×V )+(∏ē(l, G|v0 ).V) →

(

∏

∏

v,i,l,v0∏• B0 : (Z ×V )+(v∈V,(i,l,v0 )∈B(v)|edge just as∏(We simplify the indices in

v,i,l,v0)n)ē(l, G|v0 ).V) +Z ×Y

3.3 Graph Constructors and Bulk Semantics for Structural Recursion[inl (&z, v) 7→

11

(
)
(
(
))]
B(v).i = E l, v0 ⇒ E ε , inr (v, i, l, v0 ), ē(l, G|v0 ).I(&z)= O (&y) ⇒ O ((&z, &y))i∈|B(v)|[( 0 0)(0())]
x.i = E l , u ⇒ E l , inr (v, i, l, v0 ), u00inr ((v, i, l, v ), u)
7→
)
(
def
= O (&z) ⇒ E ε , inl (&z, v0 )(x = (ē(l, G|v0 ).B)(u))
i∈|x|v,i,l,v0 ē(l, G|v0 ).V) : (&z, &x) 7→ inl (&z, I(&x))∏• I 0 : Z × X → (Z ×V ) + (It should be noticed that the above graph constructors are closed on finiteness, i.e., they map
finite graphs to a finite graph; and also if e is closed on finiteness, so is rec(e).
From now we show that the above functions on graphs are bisimulation generic.
Definition 8 (Bisimulation Genericities) Let f : DBYX11 × ... × DBYXnn → DBYX . Then f is bisimulation generic if for G1 ∼ G01 , ..., Gn ∼ G0n , f (G1 , ..., Gn ) ∼ f (G01 , ..., G0n ); and f is strongly
bisimulation generic if both f is bisimulation generic observing ε , i.e., for G1 ∼! G01 , ..., Gn ∼!
G0n , f (G1 , ..., Gn ) ∼! f (G01 , ..., G0n ), and f is bisimulation generic for trees, i.e., for trees T1 ∼T10 , ..., Tn ∼ Tn0 , f (T1 , ..., Tn ) ∼ f (T10 , ..., Tn0 ).
Since our bisimilarity was defined in two steps, proving bisimulation genericity is complicated, so we split the bisimulation genericity into the two simpler bisimulation genericities:
Lemma 1 Let f : DBYX11 × ... × DBYXnn → DBYX . If f is strongly bisimulation generic, then f isbisimulation generic.
0

Proof. Let f : DBYX → DBYX0 be a unary function to keep presentation simple, and assume theboth assumption in the statement and G ∼ G0 . Our goal is to prove that f (G) ∼ f (G0 ).
By the definition of the bisimilarity, G ∼ G0 implies uf(G) ∼ uf(G0 ). Now f is bisimulation
generic for trees uf(G) and uf(G0 ), so f (uf(G)) ∼ f (uf(G0 )). On the other hand, since f isbisimulation generic observing ε , and since G ∼! uf(G) and G0 ∼! uf(G0 ), it holds that f (G) ∼!
f (uf(G)) and f (G0 ) ∼! f (uf(G0 )). Since ∼! implies ∼, hence f (G) ∼ f (uf(G)) and f (G0 ) ∼f (uf(G0 )). Thus it is derived that f (G) ∼ f (G0 ).
We remark that the converse of this lemma is trivially false. Because, take such graphs G0 , G1 ,def
and G00 that G0 ∼ G1 , not G0 ∼! G1 , G0 ∼! G00 , and G0 6= G00 . Then we define f (G) = if G = G0
then G1 else G. Then, since f (G) ∼ G, f is bisimulation generic; but f is not bisimulation
generic observing ε , since G0 ∼! G00 and not f (G0 ) ∼! f (G00 ).
Theorem 1 The graph constructors and the structural recursion are strongly bisimulation
generic. The latter means that for e : L × DBY → DBZZ , if for any l ∈ L , e(l, -) is strongly
bisimulation generic, then so is rec(e) : DBYX → DBZ×X
Z×Y .
Proof. We omit similar parts to the proof of the similar theorem in the paper [BFS00], anddescribe other points proper to this ordered case. On the case of graph constructors, the proofs are
straightforward. For the structural recursion, first we can directly show that if e is bisimulation
generic observing ε , then so is rec(e). We can also directly show that for any graph g and12

4 BIDIRECTIONAL SEMANTICS OF ORDERED UNCALe, e0 : L × DBY → DBZZ , if e ∼! e0 (pointwisely), then rec(e)(G) ∼! rec(e0 )(G). Then using this,we can show that if e is bisimulation generic for trees, then so is rec(e).

4Bidirectional semantics of Ordered UnCALIn this section, we provide bidirectional semantics for UnCALo proposed in Section 2, enriching
the semantics given in Section 3. We adapt our previous work [HHI+ 10] on unordeded UnCAL.
Overall framework in the previous work—enriching forward semantics by trace information,and providing backward semantics for the forward transformation—remains unchanged. In particular, we decompose target graphs in the backward transformation based on operators having
produced the trace information, and produce updated variable binding environment as a resultof backward transformation. As in the forward semantics, order between branches are respectedin the backward transformation. Major difference between the bidirectional semantics of unordered UnCAL and that of UnCALo is that branches are represented as ordered lists instead ofsets. However, the fact that the union operator is no longer commutative does not essentiallychange the backward evaluation. For example, when we unify the result of binary operation, theorder between the operands are not reflected.

Bidirectional Properties Our goal in bidirectionalizing UnCALo is to have bidirectional properties inherited from the previous work [HHI+ 10]. Let F [[e]]ρ denote a forward evaluation (get)of expression e under environment ρ to produce a view, and B[[e]](ρ , G0 ) denote a backward
evaluation (put) of expression e under environment ρ to reflect a possibly modified view G0 to
the source by computing an updated environment. An environment ρ is a mapping with a formof {$x 7→ X, . . . } where X is a graph G or a label l. The following are two properties we aim at:
F [[e]]ρ = G(G ET P UT )B[[e]](ρ , G) = ρ

B[[e]](ρ , G0 ) = ρ 0 F [[e]]ρ 0 = G00(WP UT G ET )B[[e]](ρ , G00 ) = ρ 0

The (G ET P UT) property states that unchanged view G should give no change on the environment
ρ in the backward evaluation, while the (WP UT G ET) property states that the modified view G0
and the view obtained by backward evaluation followed by forward evaluation may differ, butboth views have the same effect on the original source if backward evaluation is applied. A pairof forward and backward evaluations is well-behaved if it satisfies (G ET P UT) and (WP UT G ET)
properties. In the rest of this paper, we will present forward and backward evaluations (bidirectional semantics) for UnCALo and prove the following theorem.
Theorem 2 (Well-behavedness) The proposed forward and backward evaluations are wellbehaved, provided their evaluations succeed.
In the rest of this section, we first provide forward semantics enriched with trace information,and then define backward semantics using the trace information.

4.1 Traceable Forward Evaluation

4.1

13

Traceable Forward Evaluation

As in our previous work [HHI+ 10], we augment node IDs of the view with trace information.
The trace information has a structure similar to the index structure of products and coproducts
in Definition 6 and 7, except that we add code position information for bidirectionalization. The
trace ID is defined byTraceID ::= SrcID | Code Pos Marker| RecN Pos TraceID Marker | RecE Pos TraceID TraceID Num,
where SrcID ranges over identifiers uniquely assigned to all nodes of the database, Pos ranges
over code positions in the UnCALo expression, Marker ranges over input/output markers, andNum stands for integers. This trace ID is different from that of the previous work in that in the
RecE part, TraceID and ordinal Num is used instead of edge. The Num part represents fromwhich branch of the input graph of rec the node is produced. In unordered setting, the positionin the set of branches are not important, so the edge, i.e, triple of source node, label and target
node was sufficient. In ordered setting, he have to keep track of the position. For example, if anode w is generated from the i-th branch (l, vt ) of node vs through the rec construct at the code
position p, then trace ID of the form RecE w vs i is produced.

4.2

Enriched Forward Semantics

We now formally define the enriched forward semantics for finite graphs by simple augmentation of trace IDs to the semantics in the previous section. We still use (V, B, I) representation,
but we use TraceID structure for nodes in V instead of products and coproducts. In addition,
we replace the composition of markers in X × Z by a monoid (·, &), with & as the identity, i.e.,&· &x = &x · & = &x. The type of rec will be (L × DBY → DBZZ ) → DBYX → DBZ·X
Z·Y , where Z · X is
defined by {&z · &x | &z ∈ Z, &x ∈ X}. In particular, {&} · Z = Z · {&} = Z for any Z. This treatment
is inherited from [BFS00], and easier to implement. It is not for the sake of bidirectionalization.
For example, rec(λ ($l, $t).e)(G) ∈ DBYX for e : (L × DBY → DB& ) and G ∈ DBYX , meaning thata rec with the body that consists only of the default marker does not change the type of their
input graphs through applications. So ++ in rec(λ ($l, $t).e)(G) ++ G is well defined (recall that
operands of ++ must have identical set of input markers). In order for the new rec to be welldefined, however, we should restrict the combination of Z and X so that Z · X is isomorphic to
Z × X. For example, if both Z and X include the default marker & and a non-default marker incommon, then I component in the result of rec is ill-defined, mapping identical input marker tomore than one nodes. In practice, Z either contains only the default marker, or contains only
non-default markers. In the following definitions, e p denotes an UnCALo subexpression e atcode position p, ρ ($x) denotes G when ($x 7→ G) ∈ ρ . ρ is naturally used as variable substitution in UnCALo expressions, e.g., eρ for an expression e. As in [HHI+ 10], we inductively define
the enriched forward semantics F [[e p ]]ρ for each UnCALo construct of e.
Graph Constructor Expressions. The semantics of graph constructor expressions is a straightforward extension of that in section 3. For instance, we havepF [[[]]]ρ = ({Code p}, {Code p 7→ []}, {& 7→ Code p}),

14

4 BIDIRECTIONAL SEMANTICS OF ORDERED UNCAL

Note that we have nonempty B despite there is no edge in the graph.
As another example, the semantics for the expression e1 ++ e2 is defined below.
F [[(e1 ++ e2 ) p ]]ρ = F [[e1 ]]ρ ++ p F [[e2 ]]ρ G1 ++ p G2 = (V ∪ G1 .V ∪ G2 .V, B ∪ G1 .B ∪ G2 .B, I)
where M = inMarker(G1 ) = inMarker(G2 )V = {Code p &m | &m ∈ M}
B = {Code p &m 7→ [E (ε , I1 (&m)) , E (ε , I2 (&m))] | &m ∈ M}
I = {&m 7→ Code p &m | &m ∈ M},
where ++ p is a union operator for two graphs concerning position p. We write inMarker(G) todenote the set of input markers and outMarker(G) to denote the set of output markers in a graphG.
e1 ⊕ e2 It performs a componentwise union like ++, except that no ε -edges are involved.
F [[(e1 ⊕ e2 ) p ]]ρ = F [[e1 ]]ρ ⊕ F [[e2 ]]ρ ,where ⊕ is a componentwise union operator for two graphs. A graph G1 ⊕ G2 is defined byG1 ⊕ G2 = (V1 ∪V2 , B1 ∪ B2 , I1 ∪ I2 )where (V1 , B1 , I1 ) = G1
(V2 , B2 , I2 ) = G2
inMarker(G1 ) ∩ inMarker(G2 ) = 0/
Nullary constructors &y and () These expressions construct constant graphs: &y constructs a
node with a default input marker & and an output marker &y, and () constructs the empty graph.
F [[&m p ]]ρ = ({Code p}, {Code p 7→ [O (&m)]}, {& 7→ Code p})
/ 0,
/ 0)
/
F [[() p ]]ρ = (0,[l : e]F [[[l : e] p ]]ρ =({Code p} ∪V, {Code p 7→ [(l ρ , I(&))]} ∪ B, {& 7→ Code p})
where (V, B, I) = F [[e]]ρ
Trace ID Code is generated for the newly constructed node.
e1 @ e2 It appends two graphs by connecting the output nodes of the left operand and corresponding input nodes of the right operand with ε -edges.
F [[(e1 @e2 ) p ]]ρ = F [[e1 ]]ρ @ p F [[e2 ]]ρ ,where @ p is an append operator for two graphs concerning position p. A graph G1 @ p G2 isdefined by0
G1 @ p G2 = (G{
1 .V ∪ G2 .V, B1 ∪ G2 .B, G1 .I)}][
x.i = (l, v) ⇒ (l, v)
0| (u 7→ x) ∈ G1 .B
where B1 = u 7→
= &m ⇒ (ε , G2 .I(&m)) i∈|x|4.2 Enriched Forward Semantics

15

Note that @ may introduce unreachable parts in the right operand due to unmatched input/output
nodes.
&m := e It distributes the marker on the left operand to each of the input markers of the graph in
the right operand, using the Skolem function “.” introduced at the beginning of this section.
F [[(&m := e) p ]]ρ = (&m := F [[e]]ρ ),where := is an operator for a marker distribution for a graph. A graph (&m := G) is defined by(&m := G) = (V, E, I 0 )where (V, E, I, O) = G
I 0 = {&m.&x 7→ v | (&x 7→ v) ∈ I}
cycle(e) It is defined as followspF [[(cycle(e)) p ]]ρ =cycle p (G) = (G.V, B0 , G.I)  cycle (F [[e]]ρ )G.B(u).i = E (l, v)⇒ E (l, v)= O (&m) ∧ &m ∈ dom(I) ⇒ E (ε , I(&m))
where B0 (u) = = O (&m) ∧ &m ∈/ dom(I) ⇒ O (&m)
i∈|G.B(u)|where cycle p is a cycle operator for a graph concerning position p.
Variable and Condition. They have the following obvious definitions.
F [[($v) p ]]ρ = ρ ($v)

F [[(if l1 = l2 then e1 else e2 ) p ]]ρ ={F [[e1 ]]ρ
F [[e2 ]]ρ

if l1 ρ = l2 ρotherwise.

rec(λ ($l, $g).eb )(ea ) The semantics of a structural recursion is given by bulk semantics as defined in Section 3. Following [HHI+ 10], we define the enriched forward semantics of structural
recursion by two auxiliary functions composerec and fwd eachedge:p
F [[(rec(λ ($l, $g).eb )(ea )) p ]]ρ = composerec(fwd eachedge(Ga , ρ , eb ), Ga , M)
where M = inMarker(eb ) ∪ outMarker(eb )Ga = F [[ea ]]ρ

The function fwd eachedge evaluates the body expression eb for each edge of the argument
graph Ga obtained by evaluating ea and the set of result graphs. The function composerec glues
all of those results together along the structure of Ga . These functions are defined by

4 BIDIRECTIONAL SEMANTICS OF ORDERED UNCAL

16

fwd eachedge(G, ρ , e) = {(v, i, vi , F [[ē]]ρv,i )| v ∈ G.V, x ∈ G.B(v), i ∈ |x|, E (li , vi ) = x.i, ρv,i = ρ ∪ {$l 7→ li , $g 7→ G|v }}pcomposerec(G , G, M) = (VRecE ∪VRecN , BRecE ∪ BRecN , IRecN )where VRecE = {RecEp w v i | (v,]{[ i, , Gv,i ) ∈ G , w ∈ Gv,i .V}
x. j = E (l j , w j ) ⇒ E (l j , RecE p w j v i)
BRecE = RecE p w v i 7→
= O (&m) ⇒ E (ε , RecN p vi &m) j∈|x|| (v, i, vi , Gv,i ) ∈ G , w ∈ Gv,i .V, x = Gv,i .B(w)}
VRecN = {RecN p v &m | v ∈ G.V, &m ∈ M}
BRecN = {RecN
p v &m 7→[]
x.i = E (li , vi ) ⇒ E (ε , RecE p Gv,i .I(&m) v i) where (v, i, , Gv,i ) ∈ G= O (&n) ⇒ O (&m · &n)i∈|x|| v ∈ G.V, x = G.B(v), &m ∈ M}
IRecN = {&n · &m 7→ RecN p v &m | G.I(&n) = v, &m ∈ M}

4.3

Backward Semantics

Thanks to the bulk semantics defined in Section 3 and trace information generated at enrichedforward evaluation, the similarity in shape between input and output graphs are retained. As in
the previous work [HHI+ 10], the graph constructors become invertible, and backward evaluationof rec(e) is reduced to that of its body e. We again divide backward evaluation algorithm by
updates supported: (1) edge-renaming, (2) edge-deletion, and (3) insertion of edges or a subgraphrooted at a node. In the following, we give the backward semantics for these updates.
4.3.1

Backward Semantics for Edge Renaming

Backward semantics is, similarly to the forward semantics, defined inductively, i.e., backward
evaluation of an UnCALo expression is computed by combining results of backward evaluationsof the operand expressions. We first define backward semantics of simple expressions, followedby that of structural recursion.
Graph Constructor Expressions. [], &y and () construct constant graphs in the forward computation. Therefore, for the backward computation, they accept no modification on the resultview.
B[[[] p ]](ρ , G0 ) = ρ
B[[&m p ]](ρ , G0 ) = ρ
B[[() p ]](ρ , G0 ) = ρ

if G0 = F [[[] p ]]ρ
if G0 = F [[&m p ]]ρ
if G0 = F [[() p ]]ρ

A label constant similarly accepts no modification.
B[[a]](ρ , a0 ) = ρ

if a0 = a[l : e] Backward computation detaches the (possibly modified) edge from the top of the modified

4.3 Backward Semantics

17

graph. Other modification on the graph is reflected to the other operand G2 (as G02 ).
B[[[l : e] p ]](ρ , G0 ) = B[[l]](ρ , a0 ) ]ρ B[[e]](ρ , G02 )where a= lρG2
= F [[e]]ρ
(a0 , G02 ) = decomp[a : p G2 ] (G0 )Here, the decomposition function is defined as follows:
decomp[a1 : p G2 ] (G0 ) =(a01 , (V 0 \ {r0 }, B0 \ {r0 7→ ζ 0 }, {& 7→ v}))
where (V2 , B2 , {& 7→ v}) = G2
(V 0 , B0 , {& 7→ r0 }) = G0
ζ 0 = the unique branch in B0 of the form ([E (a01 , v) ]).
The modified view G0 is decomposed into its unique root branch ζ 0 = [E (a01 , v) ] from the original root r0 and the rest of the graph rooted at v. If G0 has more than one branches from theroot node or the new root v does not match the root node of the original result G2 , the backward
evaluation fails.
e1 ++ e2 We have the following definition, given decompG1 ++G2 (G0 ) as the decomposition of thegraph G0 .
B[[(e1 ++ e2 ) p ]](ρ , G0 ) = B[[e1 ]](ρ , G01 ) ]ρ B[[e2 ]](ρ , G02 )where (G1 , G2 ) = (F [[e1 ]]ρ , F [[e2 ]]ρ )(G01 , G02 ) = decompG1 ++G2 (G0 )(ρ1 ]ρ ρ2 )($v) = mg(ρ ($v),
ρ1 ($v), ρ2 ($v))
 G1 if G2 = G ∨ G1 = G2
where mg(G, G1 , G2 ) = G2 if G1 = GFAIL otherwise
decomp is defined below. G1 \ G2 denotes (G1 .V \ G2 .V, G1 .B \ G2 .B, G1 .I \ G2 .I) where G1 .B \G2 .B and G1 .I \ G2 .I respectively denote removal of bindings in G2 .B and G2 .I from those in
G2 .B and G2 .I. Simple union of graphs G1 ∪ G2 is defined by (G1 .V ∪ G2 .V, G1 .B ∪ G2 .B, G1 .I ∪G2 .I).
decompG1 ++ p G2 (G0 ) = (xreachable(G01 , G1 ), xreachable(G02 , G2 ))where (V 0 , B0 , I 0 ) = G0
(Vi , Bi , Ii ) = GiG0i
= reachable((V 0 , B0 , Ii ))satisfying
M = inMarker(G1 ) = inMarker(G2 )∀&m ∈ M, E (ε , v0 ) ∈ B0 (I 0 (&m)) : (&m 7→ v0 ) ∈ I1 ∪ I2
unreachable(G) = G \ reachable(G)xreachable(G0 , G) = reachable(G0 ) ∪ unreachable(G)18

4 BIDIRECTIONAL SEMANTICS OF ORDERED UNCAL

e1 ⊕ e2 It is like ++, except that no ε -edge is involved.
B[[(e1 ⊕ e2 ) p ]](ρ , G0 ) = B[[e1 ]](ρ , G01 ) ]ρ B[[e2 ]](ρ , G02 )where Gi= F [[ei ]]ρ
00(G1 , G2 )= decompG1 ⊕G2 (G0 )0decompG1 ⊕G2 (G ) = decompG1 ∪G2 (G0 )without satisfying condition
e1 @ e2 Because of unmatched I/O nodes, it may introduce unreachable part in the second argument during forward computation. Backward computation carefully passes those parts backwards untouched to avoid unnecessary failure because of inconsistency because these parts arepart of ordinary computation (computation on reachable parts) before discarding by the @ operator.
B[[(e1 @e2 ) p ]](ρ , G0 ) = B[[e1 ]](ρ , G01 ) ]ρ B[[e2 ]](ρ , G02 )where (G01 , G02 ) = decompG1 @ p G2 (G0 )(G1 , G2 ) = (F [[e1 ]]ρ , F [[e2 ]]ρ )decompG1 @ p G2 (G0 )= (xreachable(G01 , G1 ), xreachable(G02 , G2 )) where(Vi , Bi , Ii ) = Gi
0 , I 0 ) = G0
(V 0 , B





x.i
=
E
(
ε
,
v)
∧
v
∈
V
∧
B
(u).i
=
O
(&m)


1
1
⇒ O (&m) 000
B = u 7→ ∧(&m 7→ v) ∈ I2
| (u 7→ x) ∈ Botherwise
⇒ x.i
i∈|x|
G0i = reachable((V 0 , B00 , Ii ))&m := e It “peels off” the marker on the left hand side from each of the input markers in G0 at
the front.
B[[&m := e]](ρ , G0 ) = B[[e]](ρ , G01 )where G01
= (V 0 , B0 , I10 )000(V , E , I ) = G0
I10
= {(&x 7→ v) | (&m.&x 7→ v) ∈ I 0 }cycle(e) It removes the ε -edges introduced in the forward evaluation and restores the original
output markers.
B[[cycle(e)]](ρ , G0 ) = B[[e]](ρ , G02 )where (V 0 , B0 , I 0 ) = G0
(V, B, I) ={F [[e]][ρ
}]x.i = E (ε , v) ∧ B(u).i = O (&m) ⇒ O (&m)
Bcycle = u 7→
| (u 7→ x) ∈ B0
otherwise
⇒ x.i
i∈|x|
G02 = (V, Bcycle , I)

4.3 Backward Semantics

19

Variable. A variable simply updates its binding as B[[$v]](ρ , G0 ) = ρ [$v ← G0 ]. Here, ρ [$v ←G0 ] is an abbreviation for (ρ \ {$v 7→ }) ∪ {$v 7→ G0 }.
Condition. The backward evaluation of a condition is defined by 0
if l1 ρ = l2 ρ ∧ l1 ρ10 = l2 ρ10 ρ1
ρ0
if l1 ρ 6= l2 ρ ∧ l1 ρ20 6= l2 ρ20
B[[if l1 = l2 then e1 else e2 ]](ρ , G0 ) = 2
FAIL otherwise
where (ρ10 , ρ20 ) = (B[[e1 ]](ρ , G0 ), B[[e2 ]](ρ , G0 ))which is reduced to the backward evaluation of e1 if l1 = l2 holds, and to the backward evaluationof e2 otherwise. To guarantee well-behavedness, we further ensure that l1 = l2 does not change
after backward evaluation. Because the result of l1 = l2 may be influenced indirectly by backward
evaluation of the bodies e1 and e2 , if they update variable bindings and the value of label variablesin the condition is produced from the updated bindings. We check this by returning the condition
l1 = l2 in addition to the variable bindings, and check that condition at the expression binding
the label variables. However, to simplify presentation, we omit this passing around of conditions
and checking in the following.
Backward Evaluation of Structural Recursion. Backward evaluation is defined by
B[[rec(λ ($l, $g). eb )(ea )]](ρ , G0 )= merge(ρ , ea , Ba , bwd eachedge(Ga , ρ , eb , decomprec (G0 , Ba )))where Ga = ( , Ba , ) = F [[ea ]]ρ ,pwhere decomprec performs the inverse operation of composerec(G , G, M) by decomposing
the entire updated view into the updated views of the body eb using bulk semantics. In
bwd eachedge, we carry out backward computation of eb on each edge to obtain the updated en0 . Finally, merge combines these environments to produce the updated environment
vironment ρv,i
0 ($g) for each binding of $l andρ 0 of the whole expression. merge first merge ρv,i ($l) and ρv,i
0
$g to compute Ga , which is the updated view of the argument expression
ea . Unlike unordered()
0 ($g).B or {v 7→ [E ρ ($l), ρ 0 ($g).I(&) ]} assemantics, we cannot just simply unify each ρv,iv,iv,isets, since there are overlapping originating nodes among them, in addition to possible overlap
0 ($g) in the presence of cycles. We let the backward
between the edge for ρv,i ($l) and graph ρv,i
0 ($g) with this check,evaluation fails if these overlapped parts are inconsistent. We first unify ρv,i()
0
and unify {v 7→ [E ρv,i ($l), ρv,i ($g).I(&) ]}, maintaining the order in the original branches in
Ba (the result is stored in B0 ). If the original label in Ba was ε , then we just restore the ε edge.
Output marker of the input is also recovered. If the edge is in the prior graph (graphs createdby merging ρ 0 ($g)), which means every edge from the originating node is in the prior graph,then they must coincide with the edge in the prior graph. If the edge is not in the prior graph,then we add all edges from the originating node together (elements of B0 ). Above unification
produces G0a . Then, we inductively carry out backward evaluation on ea to obtain another0 s (excluding binding of $l and $g) are merged to
updated environment ρa0 . This ρa0 and all ρv,i
produce the result of entire backward evaluation.

20

4 BIDIRECTIONAL SEMANTICS OF ORDERED UNCAL

0 0 0
decomprec ((V , B , I ), Ba ) =
Ba (v) = b, i ∈ |b|, E (l, vi ) = b.i, ζ = (v, i, vi ),






0 = {w | (RecE p w v i) ∈ V 0 },


V


ζ


[
]




s.
j
=
E
(l
,
RecE
p
w
v
i)
⇒
E
(l
,
w
)
j
j
j
j
0
0
0
0
(ζ , (Vζ , Bζ , Iζ )) Bζ (w) == E (ε , RecN p vi &m) ⇒ O (&m)
j∈|B0 (RecE p w v i)|






0 (RecE p w v i)


s
=
B





0
0
Iζ = {&m 7→ w | B (RecN p v &m) = s, j ∈ |s|, E (ε , RecE p w v i) = s. j} 0 ) = {(ζ , B[[e]](ρ , G0 ))bwd eachedge(G, ρ , e, Gv,iv,iv,i(ζ , G0v,i ) ∈ G 0 , (v, i, vi ) = ζ , E (a, vt ) =G.B(v).i,
ρv,i = ρ ∪ {$l 7→ a, $g 7→ G|vt } }
}
U{ 0
0 )∈R
ρv,i \ {$l 7→ }) \ {$g 7→ } ((v, i, vi ), ρv,imerge(ρ , ea , Ba , R)( = B[[ea ]](ρ , G0a ) ]ρ∪ 0
∪ 0
where G0a = V 0 ∪ ρv,i($g).V, B0 ∪ ρv,i($g).B, Ia
V0 = 
∪{{v} ∪ {w | E (l, w) ∈ s} | (v 7→ s) ∈ B0 }
Ba (v). j = E (ε , v j ) ⇒ E (ε , v j )= E (l, v j ) ⇒ E (ρv, j ($l), v j ) 
B0 (v) = = O (&m) ⇒ O (&m)
j∈|B (v)|a

4.4

Backward Semantics for Edge Deletion

Similarly to the treatment in the previous work, we reflect deletion of an edge in the view asdeletion of the corresponding edge in the source using trace IDs. In unordered graph, edge isidentified by the triple of origin node, label and destination node, but here we can identify witha pair of origin node and branch position.
corr defined below takes a pair of origin node ID and branch position that uniquely identify anedge in the view, and computes the corresponding edge as a pair of origin node ID and branch
position in the source.
corr((u, i)) = (u, i)if u ∈ SrcID
corr((RecE p u{v i, j))corr((u, j)) if corr((u, j)) 6= FAIL=
corr((v, i)) if corr((u, j)) = FAIL
corr(ζ )= FAILotherwise.
FAIL means failure on finding the corresponding edge.
Using this function, we compute the set of corresponding edges from set of deleted edges on
the updated view G0view . If one of the computation of corr fails, then the backward evaluation fails.
Otherwise, we compute the updated source G0src by removal of the set of corresponding edges(branches). Note that this removal should take place at a time, since if multiple branches of anode are to be deleted, one removal of branch will change the relative position of the following(sibling) branches.
Finally, we check if F [[e]]ρ [$db ← G0src ] is bisimilar to G0view , and returns ρ [$db ← G0src ] if thebisimulation test succeeds.
It is straightforward to show that the backward semantics for edge deletion is well behaved,
since the final check does (WP UT G ET) property.

4.5 Backward Semantics for Insertion

4.5

21

Backward Semantics for Insertion

The method used in the previous work for handling insertion can be adopted here. We briefly
discuss this adoption.
The insertion operation on the view is specified by a triple of a node v on the view and theposition i where a graph is inserted, and the inserted graph Gvins . Then we first compute thecorresponding source node u at which insertion of corresponding subgraph Gsins takes place, by
the following function tr.
= tr(v)tr(SrcID)= SrcID
tr(RecN v )tr(Code ) = FAIL
tr(RecE v ) = tr(v)We find a graph Gsins connected to u and the corresponding position j at which Gsins is connected, by inversion computation on G0view using the Universal Resolving Algorithm (URA)[AG02], where G0view is obtained by adding ε edge from v at position i to Gvins .
We conjecture that well-behavedness of the above insertion reflection can be directly derived
from the soundness of URA.

4.6

Well-behavedness

Now we turn to the well-behavedness of the bidirectional transformation defined above, andbriefly sketch the proof.
Proof. This statement can be proved by induction on the structure of e, in a way similar to thatin [HHI+ 10]. Note that we perform aggressive check for branch changing behavior of if for thiswell-behavedness.

5

Conclusion

In this paper, we report our ongoing work on extension of the previous method for bidirectionalizing graph transformations from unordered graphs to ordered ones, and demonstrate that
this is possible by defining a new graph transformation language UnCALo , a novel definitionof bisimulation relation on ordered graphs with ε , and a bulk and bidirectional semantics of thegraph language UnCALo . This paves a new way towards practically solving the open problem
of unidirectional and bidirectional transformation over ordered graphs.
In our definition of structured recursion, we implicitly assume that the order of children does
not change during transformation. This assumption, however, rules out transformations whichreorder the children. For instance, the current UnCALo cannot define a transformation thatreverses the children. In the future, we wish to relax this limitation introducing a new graphconstructor that is similar to the append constructor ++ but can swap the order of two operandgraphs. As another important future work, we will study how to efficiently implement the new
bidirectional semantics of UnCALo , and evaluate it with practical applications.

Bibliography[AG02]S. M. Abramov, R. Glück. Principles of Inverse Computation and the Universal Resolving
Algorithm. In The Essence of Computation. Pp. 269–295. 2002.

22[BFP+ 08]

[BFS00][BJ10][BS81]

BIBLIOGRAPHY
A. Bohannon, J. N. Foster, B. C. Pierce, A. Pilkiewicz, A. Schmitt. Boomerang: resourcefullenses for string data. In Necula and Wadler (eds.), POPL ’08: ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages. Pp. 407–419. ACM, 2008.
P. Buneman, M. F. Fernandez, D. Suciu. UnQL: a query language and algebra for semistructured data based on structural recursion. VLDB Journal: Very Large Data Bases 9(1):76–
110, 2000.
Bart, Jacobs. From Coalgebraic to Monoidal Traces. Electronic Notes in Theoretical Computer Science 264(2):125 – 140, 2010. Proceedings of the Tenth Workshop on Coalgebraic
Methods in Computer Science (CMCS 2010).
F. Bancilhon, N. Spyratos. Update semantics of relational views. ACM Transactions on
Database Systems 6(4):557–575, 1981.

[CFH+ 09]

K. Czarnecki, J. N. Foster, Z. Hu, R. Lämmel, A. Schürr, J. F. Terwilliger. Bidirectional
Transformations: A Cross-Discipline Perspective. In International Conference on Model
Transformation (ICMT 2009). Pp. 260–283. LNCS 5563, Springer, 2009.

[FGM+ 05]

J. N. Foster, M. B. Greenwald, J. T. Moore, B. C. Pierce, A. Schmitt. Combinators forbi-directional tree transformations: a linguistic approach to the view update problem. In
POPL ’05: ACM SIGPLAN–SIGACT Symposium on Principles of Programming Languages. Pp. 233–246. 2005.
S. J. Hegner. Foundations of Canonical Update Support for Closed Database Views. In ICDT
’90: Proceedings of the Third International Conference on Database Theory. Pp. 422–436.
Springer-Verlag, London, UK, 1990.

[Heg90][HHI+ 10]

S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, K. Nakano. Bidirectionalizing Graph
Transformations. In ACM SIGPLAN International Conference on Functional Programming.
Pp. 205–216. ACM, 2010.
[HMT08]
Z. Hu, S.-C. Mu, M. Takeichi. A Programmable Editor for Developing Structured Documents based on Bidirectional Transformations. Higher-Order and Symbolic Computation
21(1-2):89–118, 2008.
[Läm04]
R. Lämmel. Coupled Software Transformations (Extended Abstract). In First International
Workshop on Software Evolution Transformations. Nov. 2004.
[Mee98]L. Meertens. Designing Constraint Maintainers for User Interaction. June 1998. http://www.
cwi.nl/∼lambert.
+[MHN 07] K. Matsuda, Z. Hu, K. Nakano, M. Hamana, M. Takeichi. Bidirectionalization Transformation based on Automatic Derivation of View Complement Functions. In 12th ACM
SIGPLAN International Conference on Functional Programming (ICFP 2007). Pp. 47–58.
ACM Press, Oct. 2007.
[RSGV09] E. L. Robertson, L. V. Saxton, D. V. Gucht, S. Vansummeren. Structural Recursion as a
Query Language on Lists and Ordered Trees. Theory of Computing Systems 44(4):590–619,
2009.
[Rut00]J. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer Science 249(1):3– 80, 2000.
[SR11]
D. Sangiorgi, J. Rutten. Advanced Topics in Bisimulation and Coinduction. Cambridge
Tracts in Theoretical Computer Science. Cambridge University Press, 2011.
[VHMW10] J. Voigtländer, Z. Hu, K. Matsuda, M. Wang. Combining Syntactic and Semantic Bidirectionalization. In ACM SIGPLAN International Conference on Functional Programming.
Pp. 181–192. ACM, 2010.
[Voi09]
J. Voigtländer. Bidirectionalization for free! (Pearl). In POPL ’09: ACM SIGPLAN–SIGACT
Symposium on Principles of Programming Languages. Pp. 165–176. ACM, New York, NY,
USA, 2009.
[WGW11] M. Wang, J. Gibbons, N. Wu. Incremental updates for efficient bidirectional transformations. In Proceedings of the 16th ACM SIGPLAN international conference on Functional
programming. ICFP ’11, pp. 392–403. ACM, New York, NY, USA, 2011.