A Parameterized Graph Transformation Calculus for Finite
Graphs with Monadic Branches
Kazuyuki Asada

Soichiro Hidaka

Hiroyuki KatoThe University of Tokyo

National Institute ofInformatics

National Institute ofInformatics

Zhenjiang Hu

Keisuke Nakano

National Institute ofInformatics

The University ofElectro-Communications

ABSTRACT1.

We introduce a lambda calculus λTFG for transformations of finite
graphs by generalizing and extending an existing calculus UnCAL.
Whereas UnCAL can treat only unordered graphs, λTFG can treat
a variety of graph models: directed edge-labeled graphs whosebranch styles are represented by monads T . For example, λTFG
can treat unordered graphs, ordered graphs, weighted graphs, probability graphs, and so on, by using the powerset monad, list monad,
multiset monad, probability monad, respectively. In λTFG , graphs
are considered as extension of tree data structures, i.e. as infinite(regular) trees, so the semantics is given with bisimilarity.
A remarkable feature of UnCAL and λTFG is structural recursion
for graphs, which gives a systematic programming basis like thatfor trees. Despite the non-well-foundedness of graphs, by suitably
restricting the structural recursion, UnCAL and λTFG ensures that
there is a termination property and that all transformations preserve
the finiteness of the graphs. The structural recursion is defined in a"divide-and-aggregate" way; "aggregation" is done by connecting
graphs with ε-edges, which are similar to the ε-transitions of automata. We give a suitable general definition of bisimilarity, taking
account of ε-edges; then we show that the structural recursion iswell defined with respect to the bisimilarity.

Designing graph transformation languages is difficult in general, because graph structured data may have cycles and shared
nodes. There are three major difficulties: consistency, finitenesspreservation, and termination of evaluation. The consistency indicates the same treatment of ‘equivalent’ graphs, where equivalence
is usually specified by either bisimilarity or isomorphism. Graphs
up to bisimilarity are equivalent to infinite trees, whereas graphs
up to isomorphism are “graphs as they look”. In this paper, we focus on graphs up to bisimilarity for the application to querying tree
databases with cyclic references such as XML with IDREF. Ensuring consistency requires that every graph transformation is bisimulation generic: i.e., the transformation results of bisimilar graphs
are bisimilar.
For finiteness-preservation, it means that every term maps finite
graphs (graphs with finite number of nodes) to finite graphs; thisand the termination properties are important for graph query languages. Full recursion, which is a typical way of constructing powerful transformations, is not desirable, since the termination andfiniteness-preservation do not hold. Structural recursion (fold) for
inductive datatypes such as lists and finite trees naturally has bothproperties; however for graphs, because of the non-well-foundednature, it is difficult to find such a structural recursion. Functions
defined by corecursion (unfold) terminate, but do not necessarily
return finite graphs.
One prominent step to solve these problems was given in thework of UnCAL [6]. Their structural recursion for graphs is suitably restricted from that for infinite trees so that the terminationand finiteness-preservation hold. The expressive power is less thanthat of fold for finite trees, but it is still powerful enough to translate
an SQL-style graph query language—called UnQL—into UnCAL.
Moreover, they gave bulk semantics for the structural recursion,
which is “divide-and-aggregate” style semantics and enables parallel evaluation. The key to defining the structural recursion of
UnCAL is use of ε-edges, which work as shortcut like the εtransitions of automata. Then the bulk semantics makes it easierto prove the finiteness-preservation and termination properties.
UnCAL is used also as a basis for bidirectional graph transformation [15] and for model driven software engineering [27].
However, there is a big restriction on UnCAL: graph modelsof UnCAL are just unordered graphs, i.e., graphs whose branches
have no sibling order; while in real applications, there are manygraph models such as ordered graphs, weighted graphs, probability graphs, etc. Though, when we generalize the graph model of
UnCAL, we come across a subtle problem: how can we generally
define the notion of bisimilarity for each graph model that has theCategories and Subject Descriptors
D.3.2 [Programming Languages]: Language Classifications—
Specialized application languages; E.1 [Data Structures]: Graphs
and networks

General Terms
Language, Theory

Keywords
graph transformation, bisimilarity, structural recursion, graph algebra, monad, epsilon edge

This is a full version of the paper to apper in Proc. of the 15th International Symposiumon Principles and Practice of Declarative Programming (PPDP ’13). ACM holds the
copyright of the definite version.

1

INTRODUCTION

notion of ε-edge?
Additionally, we should point out that UnCAL has another weak
point. The structural recursion of UnCAL is a higher order function
like the fold for trees, but the bisimulation genericity of the structural recursion in UnCAL has been proved only on the first orderpart, and UnCAL is formulated as just first order calculus, whichblurs how to extend UnCAL to richer type systems.
In previous work [14], the authors studied how to modify thegraph model of UnCAL so that we can treat ordered graphs in asimilar way to UnCAL. There it is found that ε-edges of orderedgraphs may produce a subtle problem of infinite width on branches;
this problem does not occur in the case of unordered graphs. It
was resolved by proposing a new calculus for finite ordered graphs,
giving a new definition of bisimilarity for ordered graphs having εedges, and giving the semantics of the calculus for ordered graphs.
The calculus is extended with higher order functions and formulated as an extension of simply typed lambda calculus.
Along that line, in this paper we further generalize the graphmodels, and propose a family of calculi λTFG , which is parametrizedby monads T ; each λTFG can treat graphs whose branches are represented by a monad T . For example, when T is the finite powerset
monad, λTFG becomes UnCAL, precisely, UnCAL extended as asimply typed lambda calculus. To introduce λTFG , we generalize
all the features of UnCAL with monads: i.e., its graph models, itsgraph constructors, and the structural recursion.
In Section 2, we generalize the graph models from unorderedgraphs to T -graphs, by using a monad T (with some reasonableassumption) to represent various branch styles. When T is the list
monad, the finite multiset monad, and the finite probability distribution monad, then T -graphs are ordered graphs, weighted graphs,
and probability graphs, respectively. We also give a general definition of bisimilarity for T -graphs, taking ε-edges into account.
In Section 3, we introduce the syntax and the semantics of thelambda calculi λTFG . We give the definition of graph constructors,
and show that all finite T -graphs can be represented by those graphconstructors. Then, we give a simple definition of the bulk semantics of the structural recursion for λTFG , and we prove that all transformations of λTFG are bisimulation generic. As well as generalizing with monads, λTFG is extended from UnCAL with higher orderfunctions, which is not for free but due to that our main theorem—
bisimulation genericity of the bulk semantics—is stronger than thecorresponding theorem for UnCAL [6].
In Section 4 we discuss related work, which includes more detailcomparison between λTFG and the calculus in [14].
Our contributions are summarized as follows:

formulate UnCAL to more powerful and familiar style of calculus, i.e., the simply typed lambda calculus λTFG .
• The reformulation makes it clear that we can further extend λTFG with familiar features such as coproduct, algebraic
datatypes, polymorphic types, dependent types, and so on.
In fact, although the current formulation of λTFG (and also
UnCAL) does not include transformations for manipulating
the sibling direction—e.g., reversing the order of branchesof an ordered graph—we can add such transformations, using the above flexibility of extending λTFG . (See [2] for thedetails of such an extension for sibling transformations.)

2.

GRAPH MODEL AND BISIMILARITY

First, we explain what kind of graphs the λTFG -terms can transform. After that, we give the semantic equivalence of the graphs:
i.e., bisimilarity with ε-elimination.

2.1

Graph Model of λTFG

The graphs in λTFG are rooted, directed, and edge-labeled graphs.
Furthermore, the graph model of λTFG has two notable features: εedges and markers. An ε-edge represents a shortcut between thetwo nodes; the shortcut works like the ε-transition in an automaton.
Nodes may be marked with input and output markers; these areused as interfaces to connect a graph to another graph by ε-edges.
(This is done by @ and cycle as the dotted edges in Figure 4, andby srec as in Figure 5.)
Let us introduce the notion of a T -graph, which has “T -kind of
branches”, for a monad T . First, though, let us recall the notionof a monad (in the Kleisli triple style): a monad on Set is a triple
T = (T, return, lift) of functions
T : |Set| → |Set|
return S : S → T (S)(S ∈ |Set|)′

lift S,S ′ : (S → T (S )) → (T (S) → T (S ′ )) (S, S ′ ∈ |Set|)such that these satisfy certain axioms (see [23, 4] for the axioms).
Example 1 (List Monad). The list functor List forms a monadwith the following monad structures:
return(x)lift f xs= [x]= concat (map f xs)

where concat is to flatten a list of lists to a list.

• We generalize the graph model of UnCAL with monads byapplying coalgebra theory; also we present a general definition of semantic equivalence for graphs having ε-edges,
which is given by combination of ordinary bisimilarity andε-elimination.

2

Now, let us define the graph model. We use L to denote a set oflabels and Lϵ to denote the disjoint union L ∪ {ε}. Let X and Y
be finite sets of markers; we add the prefix & for meta-variables ofmarkers like &x . Then, a T -graph (or just graph) G is defined as a
triple (V, B, I) where• We generally define graph constructors and structural recursion for T -graphs, with identifying suitable assumptions on
the finiteness of T for the sake of practical use, which is discussed in Sections 2.2.1 and 3.2.4.

• V is a set of nodes,• B : V → T (Lϵ ×V +Y ) is a branch function, where an element x in Lϵ ×V +Y (called a branch) is either an edge
Edge (l, v) or an output marker Outm (&y), and• We show that any finite T -graph can be constructed usinggraph constructors; also we find and utilize several equational properties for graph constructors.

• I : X → V is a function, which determines input nodes(roots) of the graph.

• We extend semantic equivalence for graphs to higher orderfunctions and show the bisimulation genericity of structural
recursion as a higher order function, which enables us to re-

In terms of coalgebra theory, a T -graph is a coalgebra B of theendofunctor T (Lϵ ×(-)+Y ) equipped with I : X → V , which canbe regarded as a generalized element (state) of V .
2

V
B(1)
B(2)
B(3)
B(4)
I(&)

=
=
=
=
=
=

{1, 2, 3, 4}[Edge (d, 2) , Edge (a, 4) ][Edge (c, 3) ][Edge (d, 2) ][Edge (b, 3) , Outm (&y) ]1

The main difficulty with our definition of bisimilarity is the treatment of ε-edges. We first explain strong bisimilarity, in which weregard the label ε as a usual label such as those in L. Then, we
define bisimilarity, which “skips” ε-edges.
Note that our notion of bisimilarity for the invisible label ε is different from weak bisimilarity for the invisible label τ in the context
of process algebra [21]. One purpose of our use of ε-edges is topostpone the calculations of the graph constructors, structural recursion, and so on, but weak bisimilarity is unsuitable for expected
properties of such graph transformations: e.g., weak bisimilarity
can not ensure the associativity of the graph constructor ∪ (definedin the next section).
Now, let us recall the notion of a bisimulation relation for any
endofunctor F on Set. First, we define relational lifting Fe of F .
For a relation R ⊆ V ×V ′ , i.e., for an inclusion ⟨r, r′ ⟩: R ,→V ×V ′ , we obtain ⟨F (r), F (r′ )⟩ : F (R) → F (V )×F (V ′ ); thenthe relation Fe(R) ⊆ F (V )×F (V ′ ) can be defined as the image⟨F (r), F (r′ )⟩(F (R)). Next, for two coalgebras of F , i.e., twofunctions B : V → F (V ) and B ′ : V ′ → F (V ′ ), a bisimulation
relation R between B and B ′ is a relation R ⊆ V ×V ′ such that
(B×B ′ )(R) ⊆ Fe(R).

Figure 1: Example of Ordered Graph
Example 2 (Unordered/Ordered/Weighted/Probability Graphs).
For the finite powerset monad Pfin , Pfin -graphs are unorderedgraphs, which are (equivalent to) the graph model of UnCAL.
List-graphs are ordered graphs [14], where the branches are ordered. An example of an ordered graph is shown in Figure 1.
The finite multiset monad (bag monad) is defined as Mfin :Mfin (S) = {ϕ: S→N | ϕ−1 (N−{0}): finite}.
defBranches of Mfin -graphs have the bag semantics (rather than set
semantics of Pfin ), i.e., multiplicity (called weight) of an identicalbranch is not ignored.
The finite probability distribution monad Dfin is defined as−1

def

Dfin (S) = {ϕ: S→[0, 1] | ϕDefinition 3 (Strong Bisimilarity). Let T be a monad, and G =(V, B, I) and G′ = (V ′ , B ′ , I ′ ) be T -graphs in T G X
Y . Then G
and G′ are strongly bisimilar if there is a bisimulation relation R
with respect to the endofunctor T (Lϵ ×(-)+Y ) between B and B ′such that for any &x ∈ X, I(&x ) R I ′ (&x ); in this case, we writeG ∼s G ′ .
2((0, 1]): finite, Σs ϕ(s)=1}.

The monad structure is defined as below: for s ∈ S, return(s) is
the Dirac delta function δs : S → [0, 1]:defδs (s) = 1defδs (x) = 0 (x ̸= s)

We assume that all monads T in the paper preserve weakpullbacks, which is a mild assumption often used in coalgebra
theory [26, 30]. In particular, then T preserves injections and finite
intersections. Using this assumption, it is easily checked that thestrong bisimilarity relation is an equivalence relation on T G X
Y .
Let us unfold the above abstract definition of strong bisimilarity,
when T = Pfin :and for f : S → Dfin (S ′ ),lift(f ): Dfin (S) → Dfin (S ′ )lift(f )(ϕ): S ′ → [0, 1]∑()(ϕ: S → [0, 1]) 7→ s′ 7→
ϕ(s) · f (s)(s′ )  .
s∈S

Dfin -graphs have probabilistic branches.

R: a bisimulation relation for Pfin (Lϵ ×(-)+Y )2⇐⇒∀(v, v ′ )∈R. (B(v), B ′ (v ′ )) ∈The set1 of graphs—with X and Y as sets of input and output
markers, respectively—is denoted by T G X
Y ; here, T may be omitted as GYX if it is clear from the context. We call a T -graph a finite
T -graph when V is a finite set, and write T Gf X
Y for the set of finiteXT -graphs (in [6], Pfin Gf X
Y is written as DB Y ).
We allow a graph to have multiple roots: a multi-rooted graph is
to a forest as a single-rooted graph is to a tree. For single-rooted
graphs, we often use a default marker & to indicate the root and use{& }GY to denote GY .
Note that a node can have several output markers—if a monad T
is non-deterministic as the above examples—and an output marker
can be put on several nodes; while, a node can be pointed by several
input markers, but an input marker points just one node.

⟨Pfin (Lϵ ×r+Y ), Pfin (Lϵ ×r′ +Y )⟩(Pfin (Lϵ ×R+Y ))⇐⇒∀(v, v ′ )∈R. ∃S ⊆fin Lϵ ×R+Y.
B(v)=(Lϵ ×r+Y )(S) ∧ B ′ (v ′ )=(Lϵ ×r′ +Y )(S)⇐⇒∀(v, v ′ )∈R. ∃{(l1 ,(u1 ,u′1 )), ..., (ln ,(un ,u′n )), &y1 , ..., &ym }⊆fin Lϵ ×R+Y.
B(v)={(l1 , u1 ), ..., (ln , un ), &y1 , ..., &ym } ∧B ′ (v ′ )={(l1 , u′1 ), ..., (ln , u′n ), &y1 , ..., &ym }⇐⇒∀(v, v ′ )∈R.
()∀(l, u)∈B(v). ∃u′ . (l, u′ )∈B ′ (v ′ ) ∧ (u, u′ )∈R ∧()∀&y∈B(v). &y∈B ′ (v ′ ) ∧()∀(l, u′ )∈B ′ (v ′ ). ∃u. (l, u)∈B(v)∧(u, u′ )∈R ∧()∀&y∈B ′ (v ′ ). &y∈B(v)

2.2 Graph Equivalence in λTFG : Bisimilarity
with ε-elimination
In the remaining part of this section, we give a semantic equivalence of graphs of λTFG . As discussed in the introduction, we regard
the graphs in λTFG as an extended tree data structure, i.e., as infinite
trees, so we shall use bisimilarity semantics rather than equality or
isomorphism semantics.

The last formula can be expressed as in the following pictures.
∀

v

∀

/ u

l ∀

R
R
∀ ′ l ∃ ′v

1

Precisely, this is not a set but a proper class, but this matter isresolved in usual way in coalgebra theory, if T is ranked. In thispaper, we consider only ranked monads.

/ u

/ u

l ∃

∀

R
R∀
∀ ′ l ∀ ′

R
∀ ′

∀

v
v

/ u

v om∀ &yv om &y∀v om &yR∀ ′v om∀ &y

Now, let us define our bisimilarity, whose instantiation to
the case when T = Pfin should agree with the bisimilarity of3

Further, for a class M of morphisms of SetT , iter is called uniform on M if for any function f : S → T (S ′ ) in M, and any
functions g: S ′ → T (S ′ +A) and h: S → T (S+A),

UnCAL [6]. The bisimilarity of UnCAL is defined by replacing
the first and the third pictures above with the following two pictures(and similarly for the second and the fourth pictures).
v∀/ v1 ε /... ε ∀/ vk l ∀/ uε ∀R∀ ′ ε ∃ ′ εvv1//... ε ∃/ vk′ ′

R
l ∃ ′

/ u

∀

v

/ v1 ε /... ε ∀/ vkε ∀R∀ ′ ε ∃ ′ εvv1//... ε ∃/ vk′ ′

∀
om
om

iter (g) ◦ f = iter (h): S → T (A)&ywhenever&yg ◦ f = (f +id A ) ◦ h: S → T (S ′ +A).

With this bisimulation, we “skip” zero or more occurrences of εedges before a non-ε edge or an output marker. Categorically, thiskind of iteration is captured by the notion of an iteration operator,
which is the dual notion of a fixed-point operator [29, 17]. From
now we define ε-elimination—which is almost the same as that foran ε-automaton—in terms of an iteration operator in the Kleisli
category of a monad T , and then give a definition of bisimilarity
for T -graphs.
For a monad T on Set, the Kleisli category SetT of T is defined
as below: objects in SetT are sets, and morphisms S → S ′ arefunctions S → T (S ′ ). The identity morphism id on S is

The axiom of uniformity is used for logical relation on an iteration operator [12]. We use uniformity to show later that strong
bisimilarity implies bisimilarity, and also in the proof of Lemma 16.
Example 4 (Monads with Iteration Operators). For the countable powerset monad Pcnt and a morphism f : S → Pcnt (S+S ′ )in SetPcnt ,iter (f )(s) = {s′ ∈S ′ | ∃k∈N. ∃s1 , ..., sk ∈S.
def

s1 ∈f (s) ∧ ... ∧ sk ∈f (sk−1 ) ∧ s′ ∈f (sk )}.

def

id = return : S → T (S),Also, the countable multiset monad Mcnt :Mcnt (S) = {ϕ: S → N∪{∞} | ϕ−1 (N−{0}) is countable}
def

and the composition g ◦ f of f : S → T (S ′ ) and g: S ′ → T (S ′′ )is defined as

has an iteration operator, which is given with the same formula asthat for Pcnt .
defExtending the list monad—List(S) = n∈N S n —, a countable
list monad CList is defined asg ◦ f = lift(g) ◦ f : S → T (S ′′ ).
def∏

A Kleisli category has coproducts: the coproduct of S1 and S2 isjust S1 +S2 , and the injections aredef

CList(S) =defin l = return ◦ in l : S1 → T (S1 +S2 )

L∈L S

∏

∀

L

,

where N is generalized to L, the set of countable linear ordered sets
up to order isomorphism2 . SetCList also has an iteration operator(see [14, 2] for the details).
For probability graphs, countable subprobability distribution
monad SubD cnt has an iteration operator:def

in r = return ◦ in r : S2 → T (S1 +S2 ).
Copairing of a pair of functions f1 : S1 → T (S ′ ) and f2 : S2 →T (S ′ ) is the same as the copairing in Set, i.e.,[f1 , f2 ]: S1 +S2 → T (S ′ ).

def

SubD cnt (S) =We write ∇: S+S → T (S) and + for the codiagonal and thecoproduct on morphisms in SetT , respectively.
Next we recall the notion of an iteration operator [10, 17].
Though we can define an iteration operator for any category withfinite coproducts, here, we define it directly on the Kleisli category
SetT of a monad T on Set, and say that a monad T has an iteration operator if SetT has it. An iteration operator iter on SetT
is an operator on functions{ϕ: S → [0, 1] | ϕ−1 ((0, 1]) is countable, Σx ϕ(x) ≤ 1}.
Note that here the summation of probabilities Σx ϕ(x) is not necessarily 1; this is because the probability 1−Σx ϕ(x) is reserved forthe probability of the nontermination of the iteration operator. The
definition of the iteration operator for SubD cnt is also similar to
those for Pcnt and Mcnt , see [16] for the details.
2
Now, let us define ε-elimination. The following characterizationof ε-elimination as an iteration operator is due to [13, 16].

f : S → T (S+A)
iter (f ): S → T (A)Definition 5 (ε-elimination). Let T be a monad and iter be an
iteration operator in SetT . For a T -graph G = (V, B, I) ∈ T G X
Y ,′its ε-elimination ε-elim(G) ∈ T G X
Y is (V, B , I) wheresuch that the operator satisfies the following axioms:• (naturality:) for f : S → T (S+A) and g: A → T (A′ ),B ′ = embed ◦ iter (iso ◦ B),defg ◦ iter (f ) = iter ((id S +g) ◦ f ): S → T (A′ ),• (dinaturality:) for f : S → T (S ′ +A) and g: S ′ → T (S+A),

embed is the embedding T (L×V +Y ) → T (Lϵ ×V +Y ), and iso
is the composition of[iter ([f, in r ] ◦ g), id A ] ◦ f = iter ([g, in r ] ◦ f ): S → T (A),T (Lϵ ×V +Y ) ∼= T ((L+1)×V +Y ) ∼= T (V +(L×V +Y )).
Conversely, ε-elimination induces an iteration operator; let us
consider a T -graph (V, B, I) in the case that L = 0. Then B : V →T ({ε}×V +Y ), and if we apply ε-elimination to this, the resulting• (unfolding:) for f : S → T (S+A),
iter f = [iter f, id A ] ◦ f : S → T (A),2More precisely, CList(S) is the set of objects of the skeleton of
the comma category (U ↓ S) where U : CLO → Set is the forgetful functor from the category CLO of countable linear orderedsets and monotone functions.

• (codiagonal:) for f : S → T (S+S+A),
iter (iter f ) = iter ((∇+id A ) ◦ f ): S → T (A).

4

Term e ::= x | λx.e | ee | (e, e) | π l e | π r e{ lambda terms }| if e then e else e{ conditional }| ops{ T -algebraic graph constructors (s ∈ Σ) }| ⟨e : e⟩ | ⟨&y⟩ | &x := e | () | e ⊕ e | e @ e || cycle(e){ common graph constructors }| srec(e)(e){ structural recursion application }| a|e=e{ label (a ∈ L) and label equality }{ boolean, label, graph types }Type σ ::= Bool | Label | GX
Y|σ × σ | σ → σ{ product types and function types }branch function is B ′ : V → T (0×V +Y ). That is, we get an
operator that maps a function V → T (V +Y ) to a function V →T (Y ). This operator is the same as the structure of an iteration
operator in the Kleisli category (if we allow Y to be arbitrary sets);and then we find that it is natural to adopt the axioms of iteration
operators as axioms of the ε-elimination.
Now, let us define our bisimilarity for graphs having ε-edges.
Definition 6 (Bisimilarity). Let T be a monad having an iteration
operator iter in the Kleisli category SetT , and G = (V, B, I) and′G′ = (V ′ , B ′ , I ′ ) be T -graphs in T G X
Y . Then, G and G are′
bisimilar if ε-elim(G) and ε-elim(G ) are strongly bisimilar; inthis case, we write G ∼ G′ .
2

Figure 2: Syntax of λTFG

It immediately follows that strong bisimilarity implies bisimilarity, if the iteration operator of T is uniform on the class of functions(rather than not necessarily on all morphisms in SetT ). We use thisproperty in some of the proofs in this paper.
When T = Pcnt , by unfolding the above definition, we get theoriginal definition of bisimilarity in UnCAL.
The above definition implies that the notion of an ε-edge a laε-elimination is independent of bisimilarity semantics, and it canbe accommodated in any equivalence relation, such as equality andgraph isomorphism, by similarly taking inverse images.

(s ∈ Σ, s: n-arity)nΓ ⊢ ops : GX
→ GX
YY(&y ∈ Y )Γ ⊢ ⟨&y⟩: GY

Γ ⊢ e: GY{&x}Γ ⊢ &x := e: GY12
Γ ⊢ e1 : GXΓ ⊢ e2 : GXYY
(X1 ∩ X2 = ∅)1 ∪X2
Γ ⊢ e1 ⊕ e2 : GX
Y

2.2.1 Generalization of Bisimilarity with Monad ExtensionΓ ⊢ e1 : LabelΓ ⊢ e2 : GY
Γ ⊢ ⟨e1 : e2 ⟩ : GYΓ ⊢ (): G∅YΓ ⊢ e 1 : GXYΓ ⊢ e2 : GYZΓ ⊢ e1 @ e2 : GXZ

Γ ⊢ e: GX(X ∩ Y = ∅)X∪YΓ ⊢ cycle(e): GX
Y

Although we could define bisimilarity as above, when T is oneof the monads in Example 4, the T -graphs might have countably
infinite width of branches. In a real database system, a graph (isoften very large but) has finite size, i.e., finite number of nodes
and a finite width. In other words, real data graphs do not have
ε-edges, which cause graphs to have infinite widths. Our use of
ε-edge is just in an implementation of λTFG for efficiency and for
defining structural recursion; so we shall suppose that what users
of λTFG can observe is just finite-width graphs, and graphs whose
ε-elimination have infinite widths are regarded as errors. (For any
finite List-graph G, it is decidable whether the ε-elimination of G
keeps finite width or not; see [14, 2].)
Therefore, the finite powerset monad and the other monads in
Example 2 are more suitable for practical purposes; however, they
do not have iteration operators. Hence, we do not require that T itself has an iteration operator in the Kleisli category, and instead we
use the following assumption: we say that T has an extension T ′for ε-elimination if we have a monad T ′ , an injective monad morphism ι : T ,→ T ′ , and an iteration operator in the Kleisli categoryof T ′ that satisfies the uniformity on the class of functions. Here,monad morphism is a natural transformation that is compatible withreturn’s and with lift’s (see [4] for the details).

Γ, l: Label, g: GY ⊢ e1 : GZΓ ⊢ e 2 : GXZYΓ ⊢ srec(λ(l, g).e1 )(e2 ): GZ×X
Z×Y
(Just unfamiliar rules are listed. We use l and g as meta variables
for variables of types Label and GX
Y , respectively.)
Figure 3: Typing Rules of λTFG

3.

SYNTAX AND SEMANTICS OF λTFG

Here, we give the syntax of λTFG and its semantics. The semantics of λTFG has two steps. The first step is an interpretation tojust in the (V, B, I) form, without considering bisimilarity. Thisis equality-based semantics rather than bisimilarity-based one. The
next step is to give an interpretation up to the bisimilarity; to doso, we need to show bisimulation genericity of terms, i.e., welldefinedness in terms of bisimilarity. Since structural recursion isa higher order function, before showing bisimulation genericity,
we will extend the equivalence relation of bisimilarity to function
types.

Definition 7 (Bisimilarity Generalized on Size). Let T be a monad
which has an extension T ′ for ε-elimination. Then there is anX
X
embedding ι G X,→ T ′ G Y which maps (V, B, I) to
Y : T GY′
(V, ι(Lϵ ×V +Y ) ◦B, I). For G and G′ in T G X
Y , G and G are
X
X′bisimilar if ι G Y (G) and ι G Y (G ) are bisimilar in the sense of
2
Definition 6.

3.1

Syntax of λTFG

The syntax of λTFG is given in Figure 2, and the typing rule isgiven in Figure 3. The syntax of λTFG in fact depends on not onlya monad T but also its signature Σ, which will be explained in thenext subsection. However, the expressive power of λTFG is independent of a choice of the signatures Σ.

From the assumption that ι has injective components and T preserves weak pullbacks, ι G X
Y reflects strong bisimilarity [30, Theorem 4.3.6]; hence, strong bisimilarity and the above bisimilarity
are equivalent for T -graphs having no ε-edges.
In the next section, we assume that a monad T is finitary andsee the usefulness; after that, in Section 3.2.4 we will come backto more detail discussion why and how we need an extension of amonad for ε-elimination.

3.2

Graph Constructors

Here, we give an interpretation of the graph constructors in λTFG .
Pfin
The original UnCAL and λFG
have the nine graph constructors
in Figure 4, by which all finite graphs can be represented. (In theoriginal UnCAL, the graph constructors ⟨a : -⟩ and ⟨&y⟩ are written
as {a : -} and &y, respectively.) Note that these constructors should5&x1...&xm

&

G

G

ሼሽ

def

a

&

G'

G ‫ ׫‬G'

B ′′ (in l (v)) = T (f )(B(v))
f : Lϵ ×V +Y → Lϵ ×(V +V ′ )+Z Edge (l, v) 7→ Edge (l, in (v))

l


(
)
Outm (&y) 7→ Edge ε, in r (I ′ (&y))

&x

&
&y

䚾a G䚿

G

䚾&y䚿

&x

()

G

B ′′ (in r (v ′ )) = (T (Lϵ ×(in r )+Z))(B ′ (v ′ ))def

&x1...&xm &x'1...&x'm'&x1...&xkG&y1...&ymGG'&y1...&ym&y1...&yn&y1...&yn&z1...&zn

G ْ G'G'

X
such that X ∩ Y = ∅,• For a graph G = (V, B, I) ∈ GX∪Y

&x1...&xm

cycle(G) = (V, B ′ , I) ∈ GYX
def

G&x1...&xm &y1...&yn

G ̷ G'

where B ′ (v) = T (f )(B(v)).
f : Lϵ ×V +(X ∪ Y ) → Lϵ ×V +YEdge (l, v) 7→ Edge (l, v)





Outm (&x) 7→ Edge (ε, I(&x))
defcycle(G)P

fin
Figure 4: Nine Graph Constructors of λFG

Outm (&y) 7→ Outm (&y)

be written as {}Y , G1 ∪X,Y G2 , and so on with type (marker-sets)
annotation; however, we will omit the subscript X and Y to avoid
clutter.
We separate the nine graph constructors into common graph constructors and T -algebraic graph constructors. When T = Pfin , {}and ∪ are T -algebraic graph constructors, and the other seven graphconstructors are common graph constructors. Common graph constructors are defined independently of the difference of monads,
while the definition of T -algebraic graph constructors depends on
algebraic operations of T .

Remark for Figure 4: Recall that, for one graph G in GYX andone marker &y ∈ Y , there may be more than one or zero &yoccurrences in G, while for one marker &x ∈ X, there must be justone &x -input node in G. Hence, for each &y i in G @ G′ in the figure, although the number of ε-edges from a node with &y i -output
marker seems just one, in fact we add the same number of ε-edges
as the number of &y i -output marker occurrences in G. This is thesame for cycle(G); but, on G ∪ G′ , the number of added ε-edges
are just 2m.

3.2.2

T -Algebraic Graph Constructors
Here, we will define the T -algebraic graph constructors. The
definition depends on algebraic operations of a monad T , and thesyntax for T -algebraic graph constructors depends on a signatureΣ generating the monad T . For example, a finite powerset Pfin (X)is a free semilattice, which has two algebraic operators, i.e., bottom
Pfin
and join. In the syntax of λFG, when we choose the signature Σof (the function symbols of) bottom and join, then ops (s ∈ Σ)have the same interpretation as the two graph constructors {} and∪ in the original UnCAL. Below, we first define the interpretationof T -algebraic graph constructors without considering signatures,
and after that we consider signatures for syntax of λTFG .
Later, we assume T to be finitary in order to prove Proposition 11. A finitary monad on Set is a monad T on Set such that thefunctor T preserves all directed colimits in Set; in other words, forany set S and any x ∈ T (S), there is a finite subset S ′ ⊆ S suchthat x ∈ T (S ′ ). The monads Pfin , List, Mfin , and Dfin are all finitary monads; for example, for [4, 1, 6, 4, 6, 4] ∈ List(N), we havea finite subset {4, 1, 6} ⊆ N and [4, 1, 6, 4, 6, 4] ∈ List({4, 1, 6}).
Here, though we define graphs in (V, B, I) form, when we consider the property of graph operations, we consider them up tobisimilarity. Hence, we assume that T has an extension for εelimination.
First, we explain that defining T -algebraic graph constructors
for multi-rooted graphs is reduced to that for single-rooted graphs.
Note that the multi-rootedness is semantically the same as thepower of sets of graphs: i.e., there is the following bijection.

3.2.1 Common Graph Constructors
We first give a definition of common graph constructors.
Definition 8 (Common Graph Constructors). Let T be a monad.
• For G = (V, B, I) ∈ GY ,⟨a : G⟩ = (V ∪ {v0 : fresh}, B ′ , {& 7→ v0 }) ∈ GY
def

(
)
def
def
where B ′ (v) = B(v) and B ′ (v0 ) = return Edge (a, I(&)) .
• For &y ∈ Y ,def⟨&y⟩ = ({&}, {& 7→ return(Outm (&y))}, id {&} ) ∈ GY .
• For G = (V, B, I) ∈ GY ,
def

{&x}

(&x := G) = (V, B, {&x 7→ I(&)}) ∈ GY.

• () = (∅, “the unique function from ∅”, id ∅ ) ∈ GY∅ .
def• For G = (V, B, I) ∈ GYX and G′ = (V ′ , B ′ , I ′ ) ∈ GYX
such that X ∩ X ′ = ∅,G ⊕ G′ = (V +V ′ , B ′′ , I+I ′ ) ∈ GYX∪X
def

2

′

′

where B ′′ = [T (Lϵ ×(in l )+Y ) ◦ B, T (Lϵ ×(in r )+Y ) ◦B ′ ]: V +V ′ → T (Lϵ ×(V +V ′ )+Y ).
def

∼
=

oplus : (Gf Y )X → Gf X
Y
f 7→ ⊕ &x := f (&x)

Y
• For G = (V, B, I) ∈ GYX and G′ = (V ′ , B ′ , I ′ ) ∈ GZ,

&x∈X(&x 7→ ⟨&x⟩ @ G) ←[ G

G @ G′ = (V +V ′ , B ′′ , in l ◦ I) ∈ GZX
def

For an n-ary operator o: S n → S on a set S, there is the obvious n-ary operator o(X) on the X-th power of S: i.e., the com-

where
6

∼
=

oX

position of (S X )n −→ (S n )X −−→ S X ; we call this power algebra. Then, when T = Pfin , i.e., for UnCAL, it can be shown
2
X
that ∪: (Gf X
Y ) → Gf Y is nothing but the X-th power algebra of2∪: (Gf Y ) → Gf Y . Hence, we will define T -algebraic graph constructors with the type (Gf Y )n → Gf Y .
Now, for a finitary monad T , let us define a function T G as
def
G
T (X) = T Gf X for a finite set X. As we will soon show, T G itself can be extended to a finitary monad. Then, for constructing operators of the type (Gf Y )n → Gf Y , i.e., T G (Y )n → T G (Y ) we canuse the result [24] that an element s in T (n) bijectively corresponds
to a family o(s) of n-ary operators (o(s)Y : T (Y )n → T (Y ))Y : setthat is natural on Y ∈ SetT . In this context, s is called a genericeffect, and o(s) is called an algebraic operation. For s ∈ T (n),o(s) is defined aso(s)Y : T (Y )n (= n→T (Y )) → T (Y )Definition 9 (T -Algebraic Graph Constructor). Let T be a finitary monad. For a generic effect s ∈ T (n) (n = {&0, ..., &n 1}),
the T -algebraic graph constructor ops of s is defined as below.
For graphs G0 , ..., Gn 1 ∈ Gf X
Y ,
(
)
n 1
def
ops (G0 , ..., Gn 1 ) = (γ(s)·X) @ ⊕ (⌊iso i ⌋ @ Gi ) ∈ Gf X
Y
i=0

where
def

&x∈X
def

in &x = {&i 7→ (&i, &x)}: n → n×X
def

iso i = πr : {&i}×X → X.

In general, there are infinitely many generic effects s ∈ T (n)(n =1, 2, ...). For defining syntax of λTFG , we have to choose a set Σof generic effects such that Σ is “representable in computer” andgenerates all generic effects.
For a finitary monad, there is a subset Σ of n∈N T (n) suchthat, for every set S, any generic effect in T (S) is a finitely
many times iterated composition of some generic effects in Σ;
here, for generic effects s ∈ T (n)(n={0, ..., n 1}) and ti ∈T (S)(i = 0, ..., n 1), their composition means the Kleisli composition lift T (i 7→ ti )(s) ∈ T (S). We call such Σ a signatureand call an element s in Σ ∩ T (n) a function symbol of arity n.
The whole set n∈N T (n) itself is one (maximum) signature, but
usually there is a much smaller signature—finite, or presentable ina meta language for implementation—as the following examples.

f 7→ lift (f )(s)and for (oY : T (Y )n → T (Y ))Y : SetT , the corresponding s is defined as on (return Tn ). For example, when T = Pfin , {0, 1} ∈Pfin (2) (2 = {0, 1}) corresponds to ∪: Pfin (Y )2 → Pfin (Y ).
From now, we apply this correspondence to the case of T G as T .
Then we will show that, for a given finitary monad T , there is anembedding of T into T G , so that we can define T -algebraic graphconstructors by algebraic operations of T .
Now, let us define the monad T G . Here, we consider only finite sets, since it is enough here (and also since finitary monads are
determined by definitions for finite sets by the left Kan-extension
as in [18, Proposition 7.6]). The monad structures of T G are deG
fined as follows: return T : X → Gf X maps &x to ⟨&x ⟩, andG
lift T : (X → Gf Y ) → (Gf X → Gf Y ) maps f to (-) @ oplus(f ).
X∼
Thus, a graph in Gf X
Y (= (Gf Y ) ) can be regarded as a “function”
from X to Y (precisely, a morphism in the Kleisli category of T G );then the composition is given by @ operator. For later use, forf : X → Y , we define its marker renaming graph∏∏

Example 10. When T = Pfin , we can take a signature {{}(∈
Pfin (0)), {0, 1}(∈ Pfin (2))}. Then, op{} and op{0,1} are thesame as the graph constructors {} and ∪ in UnCAL, respectively.
The cases of List and Mfin —which correspond to monoid andcommutative monoid, respectively—are quite similar.
For the finite probability monad Dfin , let us see that the following
Σ becomes a signature:G⌊f ⌋ = oplus(return TY ◦ f ) ∈ Gf X
Y .
Then, ⌊id X ⌋ becomes the identity for the composition @.
Next, we define a monad morphism γ : T → T G ; for a finite
def
set X and s ∈ T (X), γ(s) = ({∗}, B, {& 7→ ∗}) ∈ Gf X wheredefB(∗) = T (in r )(s) ∈ T (Lϵ ×{&}+X). For example, for T =Pfin and 2 = {&0, &1} ∈ Pfin (2), γ(2) ∈ T G (2) = Gf 2 is a single
node graph where the node has two output markers &0 and &1 andno edges.
Now, as promised above, let us consider T G as an instance of T
for the function (1). For n = {&0, ..., &n 1} and G ∈ T G (n) =Gf n , its algebraic operation isdefΣ(2) = {sr : 2 → [0, 1] | r ∈ [0, 1]}def

Σ(n) = ∅⊆ Dfin (2)(for other n)

def

def

where sr is defined as sr (0) = r and sr (1) = 1−r. For
ϕ1 , ϕ2 : S → [0, 1] in Dfin (S), o(sr )(ϕ0 , ϕ1 ): S → [0, 1] inDfin (S) is as below:o(sr )(ϕ0 , ϕ1 )(s) = r · ϕ0 (s) + (1−r) · ϕ1 (s).
Now recall that “singletons” in Dfin (S), i.e., elements in return(S)are given as the Dirac delta functions δs as in Example 2. Then
it is easy to see that the above Σ in fact becomes a signature: forexample, ϕ: N → [0, 1] in Dfin (N) such thato(G)Y : (Gf Y )n → Gf Y
f 7→ G @ oplus(f ).

111, ϕ(1) = , ϕ(2) = , ϕ(n) = 0 (for other n)2
63
can be represented by algebraic operations from the above Σ as

For example, for T = Pfin and 2 = {&0, &1} ∈ Pfin (2), the binary
operatorϕ(0) =o(γ(2))Y : (Gf Y )2 → Gf Y
(G0 , G1 ) 7→ γ(2) @ (&0 := G0 ⊕ &1 := G1 )2

Signatures of Monads

(1)

T

def

⊕ (&x := (γ(s) @ ⌊in &x ⌋)) ∈ Gf X
n×X

γ(s)·X =

1
1
1
1
1 1
2
δ0 + δ1 + δ2 = δ0 + ( δ1 + δ2 )
2
6
3
2
2 3
3
= o(s 1 )(δ0 , o(s 1 )(δ1 , δ2 ))

ϕ=

(2)

agrees with ∪: (Gf Y )2 → Gf Y in UnCAL. As explained above, ∪for Gf X
Y in Figure 4 is just the X-th power algebra of ∪ for Gf Y .
Observe that, corresponding to @ and ⊕ occurring in (2), in Figure 4, the graph constructor ∪ has similar parts to @ and ⊕.
Let us sum up the above.

2

3(or, = o(s 1 )(δ1 , o(s 3 )(δ0 , δ2 )) etc.).
6

5

As this example, though a signature may be infinite, still may bepresentable in a meta-language for implementation.
2
7

A signature is enough to represent all T -algebraic graph constructors: For generic effects s ∈ T (n)(n={0, ..., n 1}) andti ∈ T (m)(i = 0, ..., n 1), the T -algebraic graph constructorof the Kleisli composition lift T (i 7→ ti )(s) ∈ T (m) agrees
with the composition of the corresponding T -algebraic graph connX
X mstructors ops : (Gf X→ Gf X
Y ) → Gf Y and opti : (Gf Y )Y , i.e.,⟨⟩X m
X
ops ◦ opti i∈n : (Gf Y ) → Gf Y . Hence, by the definition of
signatures, any T -algebraic graph constructor can be represented
as a finitely many times iterated composition of T -algebraic graphconstructors of some function symbols in a signature.
Thus, though syntax of λTFG depends on the choice of signaturesof T , the expressive power of T -algebraic graph constructors is thesame regardless of the choice.
As an important remark, the above definition of T -algebraic
graph constructors gives us equational theories for T -algebraic
graph constructors for free. T -algebraic graph constructors aredefined through the monad morphism γ : T → T G , so the T algebraic graph constructors obey the same axioms as those of thealgebra of T . For example, finite powersets are free algebras ofupper semilattices; hence, the graph constructors {} and ∪ satisfy all axioms of upper semilattices: i.e., associativity, unitality,commutativity, and idempotency. Moreover, since γ is monic, theconverse, a kind of completeness, also holds.

where
def

s = ⟨(-):(-)⟩: Lϵ ×Gf Y → Gf Y ,s′ = ⟨-⟩: Y → Gf Y ,
def

and
def

G

t = µTY ◦ γGf Y : T (Gf Y ) → Gf Y

(4)

G def
G
(µTY = lift T (id T G (Y ) )).

Note that since T is finitary, for any element x ∈ T (Gf Y ), there exist s ∈ T (n) and n-number of graphs Gi —i.e., G(-) : n → Gf Y —such that x = T (G(-) )(s). Then,Gt(x) = (µTY ◦ γGf Y ◦ T (G(-) ))(s)G= (µTY ◦ T G (G(-) ) ◦ γn )(s)G

= (lift T (G(-) ) ◦ γn )(s)= γn (s) @ oplus(G(-) )= ops (G0 , ..., Gn 1 ).

(naturality of γ)(by monad axioms)
G(def. of lift T )(def. of op)

Hence t(x) is defined with the T -algebraic graph constructors. For
example, when T = List,
t = foldr(++, []): List(Gf Y ) → Gf Y .

3.2.3 Full Representability of Finite Graphs

On the above s, precisely, s(ε, G) = ⟨ε : G⟩ is not a representation
by graph constructors, because an expression ⟨a : e⟩ is not allowedin λTFG when a = ε. For the case, in the above definition, replacesuch ⟨ε : e⟩ with e, which is bisimilar to ⟨ε : e⟩.
Now let us give the proof of Proposition 11.
P ROOF. Let G = (V, B, I) be a finite graph in Gf X
Y . First we
prepare a marker &v for each node v, then we write &V for the setof the markers, and define f : V → &V as f (v) = &v . Then foreach v,
( (
)(
))
def
Gv = uf -1 T Lϵ ×(⟨-⟩ ◦ f )+Y B(v) ∈ G&V +Y

The next proposition is the most important property of graphconstructors.
Proposition 11 (Full Representability of Finite Graphs). Let
T be a finitary monad on Set which has an extension for εelimination. Any finite T -graph can be represented up to bisimilarity as finitely many applications of the graph constructors. 2
Here we give a simple proof of the above proposition using thenotion of markers; this proof is a generalization with monads ofan idea explained by example in [6]. However, the use of markers is not essential; for a naive and less simple proof, see [2, Appendix D].
Before the proof, we define 1-step unfolding function

can be represented by graph constructors. Then()⌊f ◦ I⌋ @ cycle ⊕ &v := Gv ∈ GYX

uf : Gf Y → T (Lϵ ×Gf Y +Y ).

v∈VFirst, for a graph G = (V, B, I) ∈ Gf X
Y , and a node v ∈ V , weis bisimilar to the original graph G.

define2

For example, for the graph G in Example 1,

def

G|v = (V, B, {& 7→ v}) ∈ Gf Y

(3)thus, we have a function G|(-) : V → Gf Y .
(V, B, I) ∈ Gf Y ,Then for G =G1 = ⟨d : ⟨&2 ⟩⟩ ++ ⟨a : ⟨&4 ⟩⟩G2 = ⟨c : ⟨&3 ⟩⟩G3 = ⟨d : ⟨&2 ⟩⟩G4 = ⟨b : ⟨&3 ⟩⟩ ++ ⟨&y⟩,def

uf (G) = T (Lϵ ×(G|(-) )+Y )(B(I(&))).

then G is bisimilar to()⟨&1⟩ @ cycle (&1 := G1 ) ⊕ (&2 := G2 ) ⊕ (&3 := G3 ) ⊕ (&4 := G4 ) .

The function uf is strong bisimulation generic; taking the quotient Gf Y /∼s , the function
uf /∼s : Gf Y /∼s → T (Lϵ ×(Gf Y /∼s )+Y )3.2.4

The Need of Monad Extensions for ε-elimination
So far, we have seen the importance of the finitarity of a monad
T for finite-graph transformation calculus λTFG . Here, we explain
why we need to care with the phenomenon of occurring infinite
width in this paper and why we did not need to take such special
care in the case of the original UnCAL for Pfin -graphs.
When T is finitary and has an extension T ′ for ε-elimination, if
we want to define ε-elimination only for finite T -graphs, without
loss of generality, we can replace the extension T ′ with its finitary
part T ′ |fin :∪def
T ′ |fin (S) =T ′ (S ′ ).

induced from uf is nothing but the coalgebra structure of final
locally finite coalgebra [1, 20]. Using [1, Theorem 3.3] and [20,Corollary III.15], we can show that for any finitary monad T ,uf /∼s is isomorphic.
Let us define the inverse-up-to-strong-bisimilarity of uf :uf -1 : T (Lϵ ×Gf Y +Y ) → Gf Y ,i.e., uf -1 is also strong bisimulation generic and the induced function uf -1 /∼s becomes the inverse of uf /∼s . This can be constructed just by our graph constructors:
uf -1 = t ◦ T ([s, s′ ])S ′ ⊆S, S ′ : finite

8

(b) [Relabeling by e]. Let us define ẽ: Lϵ ×V → Gf Z
Z as ē ◦(id Lϵ ×G|(-) ), where G|(-) : V → Gf Y is defined as Equation (3). Then, we construct a new branching function B1
whose labels are graphs in Gf Z
Z : B1 is defined as the composition of(See Appendix A for details.)
For unordered graphs, (Pcnt )|fin is equal to Pfin ; thus, we do notneed Pcnt and ε-elimination does not produce infinite width. Thisis the reason why we did not need to consider infinite width for
UnCAL.
For ordered graphs, (CList)|fin (S) consists of such countablelists l that the number of elements of S that occur in l are finite.
Hence, still we can not avoid the notion of a countable linear order,i.e., infinite width, for even finite ordered graphs having ε-edges.
(For the details on ordered graphs, see [14, 2].)
Also on the other two examples Mfin and Dfin , T ′ |fin does not
become the original T : i.e.,(Mcnt )|fin (S) = {ϕ: S → N∪{∞} | ϕ−1(c) [Storing target nodes in output markers and duplicating
original output markers]. Let B2 be the composition of thefollowing functions
T ([p,q])

B

1
Z
V −−→
T (Gf Z
Z ×V +Y ) −−−→ T (Gf Z×V +Z×Y )(N−{0}) is finite}where p and q are the obvious functions:(SubD cnt )|fin (S) =defp(g, v) = g @ ⌊&z 7→ in l ((&z, v))⌋

{ϕ: S → [0, 1] | ϕ−1 ((0, 1]) is finite, Σx ϕ(x) ≤ 1}.

def

q(&y) = ⌊&z 7→ in r ((&z, &y))⌋.

However, in these cases, T ′ |fin are easily representable on computers differently from the case of infinite-width ordered graphs.

(d) [Connecting horizontally by T -algebraic graph constructors]. Now Gf Y has the algebraic structure tY defined in
Equation (4) after Proposition 11, and we can regard input∼=
marker sets as power through oplus : (Gf Y )X −→ Gf XY , so(X)
we have the obvious power algebra structure tY on Gf X
Y ,i.e., the composition of

3.3 Structural Recursion
Now, let us define structural recursion for T -graphs, which plays
a leading role in transformations of λTFG . We again show the typing
rule for structural recursion:
Γ, l: Label, g: GY ⊢ e: GZZ

T (⟨ẽ,π2 ⟩+id Y )BV −→ T (Lϵ ×V +Y ) −−−−−−−−−→ T (Gf Z
Z ×V +Y ).

Γ ⊢ e′ : GX
Y

′

Z×X
Γ ⊢ srec(λ(l, g).e)(e ): GZ×Y(t

)X

T (Gf X
→ T (Gf Y )X −−Y−−→ Gf X
Y ) −
Y .

When T = Pfin , the structural recursion f = srec(λ(l, g).e)satisfies the following characteristic equations, where we consider
single-rooted case for simplicity.

Then, let B3 be the composition of(Z)

tZ×V +Z×Y

B

2
T (Gf Z−−−−−−−→ Gf Z
V −−→
Z×V +Z×Y ) −Z×V +Z×Y .

f ({})= {}f (g1 ∪ g2 ) = f (g1 ) ∪ f (g2 )f (⟨l : g⟩)= e(l, g) @ f (g)f (⟨&y⟩)= ⌊&z →
7 (&z , &y)⌋.

(e) [Disjoint union by ⊕]. Using the bijective correspondence∼=→ Gf Z×V
oplus : (V →Gf Z
Z×V +Z×Y ) −Z×V +Z×Y ,we obtain a graph G′ = oplus(B3 ) ∈ Gf Z×V
Z×V +Z×Y .
def

By regarding the above equations as an recursive definition for infinite trees, the above equations serve as a definition of f to bea function which inputs finite graphs and outputs infinite graphs.
However, the outputs of f are in fact (bisimilar to) finite graphs,
and this is proved by using the following bulk semantics of f .
Now, we give a definition of the bulk semantics, explaining with
Figure 5. In Figure 5, in each step, gray parts show parts unchanged
from the previous step. A marker above a node is an input marker
and markers below a node mean output markers. Each box withbold frame is itself a graph, while each dotted box—a part of agraph—has no meaning, just hints that it was a graph before.
Briefly explaining, with bulk semantics, we first calculate the application of a given input function e to each pair of an edge and its
following subgraph, as the graph (b) in Figure 5; though the example of e in the figure does not use the second argument for simplicity of explanation. After that, we connect the results in keepingwith the shape of the original graph by using ε-edges, which resultsin the graph (f) in Figure 5.

(f) [Connecting vertically by cycle and input marker renaming]. Finally, we definesrec(e)(G) = ⌊id Z ×I⌋@ cycle(G′ ) (∈ Gf Z×X
Z×Y ).
def2

We remark that the finitarity of a monad T is used at the step (d)for the algebra tY . The above definition works if we replace all Gf
with G; then, T does not need to be finitary.
The above semantics can be implemented in an obvious way (ahint for implementation can be found in [14]). Our implementation
for unordered graphs and ordered graphs in OCaml can be found at
http://www.biglab.org/src/lambdaFG/.
For generic implementation parameterizing monads, in a meta
language we define a class of monads-with-signatures with threemethods: a signature g: Σ→T (N), an arity function a: Σ→N, and∏fold: ∀S.( s∈Σ (S a(s) →S))→(T (S)→S). In, e.g., Haskell, the∏dependent type s∈Σ (S a(s) →S) can be replaced with a larger
type Σ→(S N →S), since there is a right inverse of the projection
S N →S a(s) , i.e., id S a(s) ×⊥: S a(s) ×1 → S a(s) ×S N ∼= SN.
Finally, we give an example of queries using the structural recursion; for more examples, see [6, 15].

Definition 12 (Bulk Semantics of Structural Recursion). Let T
be a finitary monad on Set. For a function e: L×Gf Y → Gf ZZ,
Z×X
a structural recursion function srec(e): Gf X
Y → Gf Z×Y is defined through the following steps. Before that, we extend e toē: Lϵ ×Gf Y → Gf Z
Z which maps additionally (ε, _) to the “identity
graph” ⌊id Z ⌋ ∈ Gf Z
Z (see the upper leftmost picture in Figure 5).
In the following, the steps from (a) to (f) correspond to those in
Figure 5.

Example 13. Consider an ordered graph representation of books.
Since “sections” are ordered and there are some reference links inbooks, we can see books as ordered graphs. The following structural recursion toc, which is adapted from [25], computes the table(a) [Input of srec(e)]. Let us take G = (V, B, I) ∈ Gf X
Y .
9

(a)

&z1 &z2

(b)

a’

1

e(a,_):= 0 1&z1 &z2

1&z1 &z20a0 1
e(b,_):=
2 b’&z1&z1 &z2_e(ε,_):= 0 1&z1 &z2&z1 &z2&z1 &z2a’

0 1&z1 &z2

a

b

&
0

0 1
&z1 &z2&&z1 &z22&y(c)&z1 &z2a’
01(&z1,2)(&z2,2)
0 1
2 b’(&z1,1)

(e)
(0,0)

(1,0)

(&z1,&) (&z2,&)(&z1,0) (&z2,0)(&z1,1) (&z2,1)
(0,1)

a’

(0’,0)(2,2)(1’,0)(1,1)(&z1,2)
(0,2)

a’

(1,2)
b’

(d)

(&z1,1)(&z2,1) (0,0) (1,0)(&z1,1) (&z2,1) (&z1,1)(&z2,1)

(0,2)
(2,2)
(&z1,1)(1,2)
b’&z1 &z2a’
01(&z1,2)(&z2,2)B2 (0)(0’,2) (1’,2)(&z1,&y)(&z2,&y)B2 (2)&z2
01(&z1,&y)(&z2,&y)&z1

B3 (1)&z1 &z2&z1 &z2a’
01(&z1,2)(&z2,2)

0 1
2 b’
(&z1,1)&z1 &z2&z1 &z2

0 1(&z1,1)(&z2,1)B3 (0)&z1&z1(&z1,2) (&z2,2)(&z1,2) (&z2,2)(&z2,2)(0’,2)(1’,2)(&z1,&y) (&z2,&y)(&z1,0) (&z2,0)(&z1,0) (&z2,0)a’(0’,0) (1’,0)(&z1,2) (&z2,2)a’(0,1) (1,1)(&z1,2) (&z2,2)

0 1(&z1,1)(&z2,1)&z1 &z22&ysrec(e)(f)&z1 &z2&z1 &z2a’
0 1&z1 &z2

0 1
2 b’
&z1

B2 (1)a’
0’ 1’(&z1,2)(&z2,2)&z2&z2

B3 (2)

0’1’(&z1,&y)(&z2,&y)Figure 5: Bulk Semantics of Structural Recursion: Example with Ordered Graphs
def

When σ = σ1 → σ2 , we define a binary relation ∼σ on [[σ]] =[[σ1 ]] → [[σ2 ]] asof contents of books in which sections can be arbitrarily nested:toc(db) = srec( λ(l, g). if l = section
then ⟨section : (get_title(g) ++ ⟨&⟩)⟩f ∼σ f ′ ⇐⇒ ∀x, x′ ∈ [[σ1 ]]. (x ∼σ1 x′ ⇒ f (x) ∼σ2 f ′ (x′ )).

else ⟨&⟩ ) (db)

Then for any type σ, ∼σ becomes a partial equivalence relation on[[σ]], i.e., an equivalence relation on the subset

def

where the function get_title results in the title of the section:
get_title(g) = srec( λ(l1 , g1 ). if l1 = title

def|∼σ | = {x ∈ [[σ]] | x ∼σ x}.

then ⟨title : srec( λ(l2 , g2 ).⟨l2 : []⟩ ) (g1 )⟩else [] ) (g)2

We call a function f : [[σ1 ]] → [[σ2 ]] (higher order) bisimulation
generic if f is in |∼σ1 →σ2 |. (Note that this kind of lifting of semantic equivalence to function types is possible for any equivalence
relation such as strong bisimilarity, graph isomorphism etc.)
Then from the Basic Lemma of logical relation, interpretationsof all the terms are bisimulation generic if interpretations of all theconstants are bisimulation generic; as a result of the consequent of
this implication, we obtain a model of λTFG in the cartesian closed
category Set. (See the textbook [22] for the technique of logicalrelation.) In the rest of this paper, we prove that the interpretationsof all the constants of λTFG are bisimulation generic.

3.4 Bisimilarity for Higher Order Functions
So far we have given the semantics with (V, B, I) form at theequality level. In the rest of this section, we consider semantics atthe bisimilarity level.
In Section 2, we gave the semantic equivalence for graph types
T
GX
Y , i.e., the bisimilarity. Since λFG has higher order functions,and srec is a higher order function, we have to extend the semantic equivalence for base types to function types. It is well known
that if we lift an equivalence relation to function types we need toswitch from the notion of an equivalence relation to that of a partial
equivalence relation, i.e., an equivalence relation on some subset ofthe original set. This is because, now, not all functions on Gf X
Y arebisimulation generic, so we have to cut out the subset consisting ofbisimulation generic functions.
Let us give the formal definition. For the types σ of λTFG , wedefine binary logical relations ∼σ on [[σ]]. When σ = GX
Y , ∼GX

3.5

Bisimulation Genericity of Terms of λTFGFirst we show the bisimulation genericity of the graph constructors.
Proposition 14 (Bisimulation Genericity of Graph Constructors).
Let T be a finitary monad having an extension for ε-elimination.
All the graph constructors are bisimulation generic.
2
P ROOF. For a constructor f , prove that ε-elim(f (G1 , ..., Gn ))is strongly bisimilar to ε-elim(f (ε-elim(G1 ), ..., ε-elim(Gn ))).
This reduces the bisimulation genericity in the statement to strongbisimulation genericity, which is obvious.
2

Y

is the bisimilarity on Gf X
Y ; for the other base types σ, ∼σ are justthe equality relations. When σ = σ1 × σ2 , we define a binary
def
relation ∼σ on [[σ]] = [[σ1 ]] × [[σ2 ]] as

Next, let us consider structural recursion. The result below isstronger than what is proved in [6], even when T = Pfin , because(x1 , x2 ) ∼σ (x′1 , x′2 ) ⇐⇒ (x1 ∼σ1 x′1 ) ∧ (x2 ∼σ2 x′2 ).
def

10Lemma 16. The structural recursion srec is strong-bisimulation
generic: i.e., for e1 ∼s e2 : L×Gf Y → Gf Z
Z and for G1 ∼s G2 ∈Gf X
Y , the following holds:

here bisimulation genericity is proved also on the first argumente, while in [6], it is proved only on the second argument G. Thisis the key point of our extension from UnCAL to the higher orderPfin
calculus λFG.

srec(e1 )(G1 ) ∼s srec(e2 )(G2 ) (∈ Gf Z×X
Z×Y ).

Theorem 15 (Bisimulation Genericity of Structural Recursion).
Let T be a finitary monad having an extension for ε-elimination
T ′ . Structural recursion srec is bisimulation generic, i.e., if
e1 ∼ e2 : L×T Gf Y → T Gf ZZ,

P ROOF. Basically, this is proved straightforwardly according to
the steps in Definition 12. At the step (f) in Definition 12, we used
cycle; accordingly in this proof, we use the uniformity of the iteration operator. For details, see Appendix B.
2

and G1 ∼ G2 ∈ T Gf X
Y ,

then
Z×X
srec(e1 )(G1 ) ∼ srec(e2 )(G2 ) ∈ T Gf Z×Y.

4.

ε-elim(srec(e)(G)) ∼s ε-elim(srec(ε-elim ◦ e)(ε-elim(G)))
in fact, there is a type error: i.e., now ε-elim ◦ e is a function of theZtype L×T Gf Y → T ′ Gf Z so we can not apply srec with respect′
to either T nor T . This can be solved as follows.
First, it is easily shown that the structural recursion is defined“uniformly” on monads: LetX′i = ι Gf X
Y : T Gf Y → T Gf Y ,X

def

CONCLUDING REMARK

We presented a parameterized calculus λTFG that is an extensionof the lambda calculus with finite graph types, the graph constructors, and the structural recursion, for generalizing and extending
UnCAL [6]. We presented the semantics of λTFG that has a suitablebisimilarity accommodating ε-edges as well as the termination andfiniteness preserving properties. A further extension of λTFG is presented in [2].
This paper is based on our previous work [14]. As explainedin the introduction, in the previous paper a new calculus—named
as λFG in the previous paper—for ordered graphs was introduced.
The calculus λFG is not the same as λList
FG in the current paper; here,
we give the comparison of the current and the previous papers. In
λFG , the structural recursion is extended from that in the current
λList
FG , so that it can transform sibling direction of graphs; hence theexpressive power of λFG is higher than λList
FG . Therefore to extend
current work with such sibling transformations is important future
work. Also, in the previous work we focused on ordered graphs,
and gave some decidability results on ordered graphs. Moreover, inthe current paper the existence of a monad and an iteration operator
is used as an assumption; while, in the previous paper to define thecountable list monad and the iteration operator for the monad wasa main contribution.
The database community has undertaken a lot of work on graphtransformation languages, but most of it has been on graphs up toisomorphism (or equality); there has been little work on graphs
up to bisimilarity with considering bisimulation genericity. In [3],however, new semantics for the structural recursion of UnCAL wasgiven.
There has been a lot of work on structural recursion for specifickinds of graphs, such as graphs represented by trees with specificpointers [11, 8], and graphs represented by trees with embedded
functions [9, 7]. However, they do not ensure all of the bisimulation
genericity, terminating property, and finiteness preserving property,
which are our original goals as explained in the introduction.
In coalgebra theory, i.e., the study of infinitary/cyclic structures,some studies have focused on the finiteness of graphs. In [5, 28],
for every Kripke polynomial endofunctor or quantitative functor F ,a systematic way of giving a syntax fully representing all finite F coalgebras and a sound and complete equational theory for bisimilarity were given. The differences between that study and ours are
as follows: (i) The two classes of endofunctors—quantitative functor and ours with arbitrary finitary monads—are not comparable;
especially, our leading example List(Lϵ ×(-)+Y ) is not a quantitative functor. (ii) Our equational theory is restrictive while theequational theory given in that study captures completely the bisimilarity. (iii) Their study does not treat ε-edges, and is not a study
for transformations. (iv) The approaches to syntax are different:
The both can express arbitrary finite coalgebras, but there seems nocompositional translations between their and our graph representation systems, and comparison of expressive power of open terms is
not obvious. Also, their approach is in a guarded style, by which

P ROOF. Basically we want to prove in a similar way to the proofof Proposition 14, but there is a bit subtle problem. Though thefollowing might be expected to hold,X
where ι Gf X
Y is defined as just the restriction of ι G Y . For

e: L×T Gf Y → T Gf Z
Z,e′ : L×T ′ Gf Y → T ′ Gf Z ,Z

G ∈ T Gf X
Y ,if e′ ◦ (L×i) = i ◦ e then′srecT (e′ )(i(G)) = i(srecT (e)(G)).
Here the equality = means the exact equality rather than strong
bisimilarity or bisimilarity.
This reduces the setting of the theorem to the case in which T is
not necessarily finitary and ι: T → T ′ is the identity—i.e., T (=T ′ ) is an arbitrary monad whose Kleisli category has an iteration
operator—, so that ε-elim is closed in T Gf X
Y . This is because, forany
e1 ∼ e2 : L×T Gf Y → T Gf Z
Z,
there aree′1 ∼ e′2 : L×T ′ Gf Y → T ′ Gf Z
Z

such that e′i ◦ (L×i) = i ◦ ei . We can take such e′i by using somebisimulation generic retraction i∗ of i. Such i∗ can be defined in
an ad hoc way3 : Let G0 be an arbitrary fixed graph in T Gf Y . Fordef
G′ ∈ T ′ Gf Y , if G′ is in T Gf Y , then i∗ (G′ ) = G′ , else if G′ isdefbisimilar to some graph G in T Gf Y , then i∗ (G′ ) = G (G should∗′ def
be chosen), else i (G ) = G0 .
Now, in this reduced setting, we will prove the goal in a similar
way to Proposition 14. First, we can prove the commutativity ofsrec with ε-elim:
ε-elim(srec(e)(G)) ∼s ε-elim(srec(ε-elim ◦ e)(ε-elim(G))).
Then, for concluding the proof, it is enough to show the strong2
bisimulation genericity of srec (Lemma 16).
3

For one who wants non-ad-hoc way, if we assume that the givenfunction ei is the interpretation of some term ti in λTFG , then we′
can get the desired e′i as the interpretation of ti in λTFG .
11the unique fixed point operator can be used; while ours does not
require guardedness, and require an iteration operator instead.
In [1, 20], the authors studied categorical properties of the set offinite coalgebras, and characterized it as a final locally finite coalgebra. The class of endofunctors for coalgebras in that study is wider
than ours; some of the results are applied and inspire our work. In
that study, there is no consideration for finiteness-preserving structural recursion. The finality among locally finite coalgebras is akind of corecursion and has a similar problem to that of corecursion; i.e., to assure finiteness-preservation, we have to check localfiniteness of infinite graphs, automation of which seems difficult.
The general treatment for ε-edges with iteration operators in thecurrent paper was hinted at in [16]. Although there was no consideration of ε-edges itself in that study, the author showed thatthe trace semantics for some kinds of coalgebra induces iteration
operators by forgetting the length of trace paths; the resulting iteration operators can be regarded as ε-elimination. The countable list
monad is not treated in that paper; it does not satisfy the assumptionof the theorem in that paper.
In [19], the authors studied ε-elimination for weighted automata.
The kinds of automata treated in their paper are parametrized bycertain semirings, and do not include our ordered case (Listgraphs). Also, their approach to specifying weighted automata
is different from ours. They define first some class of weighted
ε-automata, and then they restrict it to “valid” ones with some procedure; while our graphs are “valid” from the beginning. As a main
contribution, they give an algorithm for removing ε-transitions. It
seems interesting future work to compare their and our generalautomaton/graph models and merge each advantages.

[8] S. Dal Zilio, D. Lugiez, and C. Meyssonnier. A logic you cancount on. In POPL’04, pages 135–146. ACM Press, 2004.
[9] L. Fegaras and T. Sheard. Revisiting catamorphisms overdatatypes with embedded functions (or, programs from outerspace). In POPL, pages 284–294. ACM Press, 1996.
[10] E. Haghverdi. A Categorical Approach to Linear Logic,
Geometry of Proofs and Full Completeness. PhD thesis,
University of Ottawa, 2000.
[11] M. Hamana. Initial algebra semantics for cyclic sharing
structures. In TLCA, LNCS 5608, pages 127–141, 2009.
[12] M. Hasegawa. The uniformity principle on traced monoidal
categories. Electr. Notes Theor. Comput. Sci., 69:137–155,
2002.
[13] I. Hasuo, 2011. personal communication.
[14] S. Hidaka, K. Asada, Z. Hu, H. Kato, and K. Nakano.
Structural recursion for querying ordered graphs. In ICFP
2013, to appear, Mar. 2013.
[15] S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and
K. Nakano. Bidirectionalizing graph transformations. In
ICFP 2010, pages 205–216. ACM Press, 2010.
[16] B. Jacobs. From coalgebraic to monoidal traces. Electr.
Notes Theor. Comput. Sci., 264(2):125–140, 2010.
[17] Y. Kakutani. Duality between call-by-name recursion andcall-by-value iteration. In CSL, volume 2471 of LNCS, pages
506–521. Springer, 2002.
[18] G. M. Kelly. Structures defined by finite limits in theenriched context, I. Cahiers Topologie Géom. Différentielle,23(1):3–42, 1982.
[19] S. Lombardy and J. Sakarovitch. The removal of weighted
ϵ-transitions. In Implementation and Application ofAutomata, volume 7381 of LNCS, pages 345–352. Springer,
2012.
[20] S. Milius. A sound and complete calculus for finite stream
circuits. In LICS, pages 421–430. IEEE Computer Society,2010.
[21] R. Milner. Communicating and Mobile Systems: theπ-calculus. Cambridge University Press, 1999.
[22] J. C. Mitchell. Foundations for programming languages.
Foundation of computing series. MIT Press, 1996.
[23] E. Moggi. Computational lambda-calculus and monads. In
LICS, pages 14–23. IEEE Computer Society, 1989.
[24] G. Plotkin and J. Power. Algebraic operations and genericeffects. Applied Categorical Structures, 11:69–94, 2003.
[25] E. L. Robertson, L. V. Saxton, D. V. Gucht, andS. Vansummeren. Structural recursion as a query language
on lists and ordered trees. Theory of Computing Systems,
44(4):590–619, 2009.
[26] J. Rutten. Universal coalgebra: a theory of systems.
Theoretical Computer Science, 249(1):3 – 80, 2000.
[27] I. Sasano, Z. Hu, S. Hidaka, K. Inaba, H. Kato, and
K. Nakano. Toward bidirectionalization of ATL with
GRoundTram. In ICMT, volume 6707 of LNCS, pages
138–151. Springer, 2011.
[28] A. Silva, F. Bonchi, M. M. Bonsangue, and J. J. M. M.
Rutten. Quantitative Kleene coalgebras. Inf. Comput.,
209(5):822–849, 2011.
[29] A. K. Simpson and G. D. Plotkin. Complete axioms for
categorical fixed-point operators. In LICS, pages 30–41.
IEEE Computer Society, 2000.
[30] A. Sokolova. Coalgebraic Analysis of Probabilistic Systems.
PhD thesis, TU Eindhoven, 2005.

5. ACKNOWLEDGMENTS
We thank Ichiro Hasuo and Kazutaka Matsuda for useful comments. The research was supported in part by the Grand-Challenging
Project on the “Linguistic Foundation for Bidirectional Model
Transformation” of the National Institute of Informatics and KAKENHI No. 23700047, 22300012, 25240009, and 23220001.

6. REFERENCES[1] J. Adámek, S. Milius, and J. Velebil. Iterative algebras atwork. Mathematical. Structures in Comp. Sci.,
16(6):1085–1131, Dec. 2006.
[2] K. Asada, S. Hidaka, H. Kato, Z. Hu, and K. Nakano.
Parameterized graph transformation languages with monads.
Technical Report GRACE-TR-2012-07, GRACE Center,
National Institute of Informatics, 2012.
[3] A. A. Benczúr and B. Kósa. Static analysis of structural
recursion in semistructured databases and its consequences.
In ADBIS, volume 3255 of LNCS, pages 189–203. Springer,
2004.
[4] N. Benton, J. Hughes, and E. Moggi. Monads and effects. In
In International Summer School on Applied Semantics,
APPSEM 2000, pages 42–122. Springer-Verlag, 2000.
[5] M. Bonsangue, J. Rutten, and A. Silva. Algebras for Kripke
polynomial coalgebras. In LICS, IEEE, Computer Science
Press, pages 49–58, 2009.
[6] P. Buneman, M. F. Fernandez, and D. Suciu. UnQL: a querylanguage and algebra for semistructured data based on
structural recursion. The VLDB Journal, 9(1):76–110, 2000.
[7] B. C. d. S. Oliveira and W. R. Cook. Functional
programming with structured graphs. In ICFP, pages 77–88.
ACM Press, 2012.
12

P ROOF. Let Gi be (Vi , Bi , Ii ). From G1 ∼s G2 , there exists
R : V1 p V2 such that the following diagram commutes.

APPENDIX
A. FINITARY MONAD EXTENSION FOR
ε-ELIMINATION′X′

For a monad T with an iteration operator iter in SetT ′ , T |fin
may not have an iteration operator (as Pcnt |fin = Pfin ). Still, we
can define ε-elimination for finite T ′ |fin -graphs so that the resultgraph is equal to one obeying Definition 5.
X
Let G = (V, B, I) be a finite T ′ |fin -graph in T ′ |fin Gf Y . Since′
V is finite and T |fin is finitary by definition, there exists a finite
subset L′ ⊆ L and a function B ′ such that the following diagram
commutes.

X

1

iter (B ′ )1−→ T ′ (L′ ×V +Y ) = T ′ |fin (L′ ×V +Y )since L′ ×V +Y is a finite set. Let us define B ′′ as the composition
of

T (⟨f
e1 ,πr ⟩+id Y )t◦T ([p,q])T (⟨fe2 ,πr ⟩+id Y )t◦T ([p,q])

2

G′1

G′2

/

1
/ Gf Z×V
Z×V1 +Z×Y
Z×R_ ∼s Z×R+Z×Y′
i.e., G′1 ∼s Z×R
Z×R+Z×Y G2 . (6)2
Gf Z×VZ×V2 +Z×Y′
cycle(G′1 ) ∼s Z×R
Z×Y cycle(G2 ),−→ T ′ |fin (L′ ×V +Y ) ,→ T ′ |fin (Lϵ ×V +Y )(7)

iter (B )′′def

and from the left square of the diagram (5) we get′⌊id Z ×I1 ⌋ @ cycle(G′1 ) ∼s Z×X
Z×Y ⌊id Z ×I2 ⌋ @ cycle(G2 )′X, I) in T |fin Gf Y .

and define ε-elimfin (G) = (V, B
Then, for a finite T ′ |fin -graph G, by the inclusion T ′ |fin ,→ T ′ ,we can regard G also as a T ′ -graph. It can be easily checkedthat ε-elim(G) in Definition 5 is exactly equal to the above
ε-elimfin (G) regarded as a T ′ -graph.
For a finitary monad T with an extension for ε-elimination T ′ ,the condition that T is finitary can be used to show that ι: T → T ′can be decomposed into the inclusion T ′ |fin ⊆ T ′ and some (necessarily injective and unique) monad morphism ιfin : T → T ′ |fin .
Then (T, T ′ |fin , ιfin , ε-elimfin ) becomes a “finitary monad extension for ε-elimination” which is almost a monad extension for
ε-elimination except for that ε-elimfin can perform ε-elimination
only for finite graphs.

i.e., srec(e1 )(G1 ) ∼s srec(e2 )(G2 ).

We give a proof of Lemma 16—the strong-bisimulation genericity of the structural recursion.
We will use the following notions and notations in the proof ofthe lemma. We write R : A1 p A2 for a relation R ⊆ A1 ×A2 ;e.g., the diagram on the left below means that, if a1 R a2 , thenf1 (a1 ) S f2 (a2 ).
f1

_

f2

/ B1
_S
/ B2

X1
S

I1

_

X2

I2

/ V1
R_
/ V2

B1

B2

2

We give a remark on Equation (7). As seen above, T G (Y ) =Gf Y (and also GY ) becomes a monad; then, cycle becomes an iteration operator in the Kleisli category. Furthermore, the iteration
operator is uniform on morphisms that come from the Kleisli category SetT via γ, if the iteration operator for T is uniform. The
above derivation of Equation (7) from Equation (6) is just the uniformity principle on relations [12]. (Since we need the uniformityof cycle only on functions, so we need the uniformity of iter T
only on functions as well.)B. STRONG-BISIMULATION GENERICITY OF STRUCTURAL RECURSION

A2

(5)

/ T (Lϵ ×V2 +Y )After that, we can show—see the remark below—that

′

R

B2

/ T (Lϵ ×V1 +Y )_ T (Lϵ ×R+Y )Then, for the composition of the above, the transposition of Vi by
oplus yields

Now V +(L′ ×V +Y ) is a finite set; hence, T ′ |fin (V +(L′ ×V +Y ))= T ′ (V +(L′ ×V +Y )). We can therefore apply the iteration operator iter to B ′ ; the result is

A1

B1

B2

T ′ |fin (V +(L′ ×V +Y ))V

B1/ Gf Z/ T (Lϵ ×V1 +Y ) / T (Gf Z
Z ×V1 +Y )Z×V1 +Z×Y__∼s Z
T (∼s Z
R _ T (Lϵ ×R+Y ) _Z×R+Z×Y
Z ×R+Y )
Z
Z
/
/
/
V2
T (Lϵ ×V2 +Y )
T (Gf Z ×V2 +Y )Gf Z×V +Z×Y
V1∼=
/ T ′ |fin (V +(L×V +Y ))ZZZZZZZOZZZZZZZ
ZZZ?
B′

V

I2

/ V1
R_
/ V2

Next, from the assumption that e1 ∼s e2 , the following diagram
commutes.

V ZZZZZ/ZTZ′Z|fin (Lϵ ×V +Y )B

I1

/ T (Lϵ ×V1 +Y1 )_ T (Lϵ ×R+T )/ T (Lϵ ×V2 +Y2 )For S : X1 p X2 and T : Y1 p Y2 , let us define the relation
Xi
X1
S
2
p Gf X∼s S
T : Gf Y1
Y2 : for Gi ∈ Gf Yi , G1 ∼s T G2 if there exists a
relation R : V1 p V2 such that the right diagram above commutes(i.e., each of the two squares holds). We write simply X for theXpdiagonal relation between X and X, then note that ∼s X
Y : Gf YX
Gf Y is the same as ∼s .
13