ISSN 1884-0760

GRACE TECHNICAL REPORTS

Parameterized Graph Transformation Languages
with Monads
Kazuyuki Asada Soichiro Hidaka Hiroyuki Kato
Zhenjiang Hu Keisuke Nakano

GRACE-TR-2012-07

October 2012

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 oﬀered their works here electronically. It is understood that all persons copying thisinformation 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.

Parameterized Graph Transformation Languages with Monads
Kazuyuki Asada
Hiroyuki Kato

Soichiro Hidaka
Zhenjiang Hu

Keisuke Nakano
University of Electro-Communications, Japan
ksk@cs.uec.ac.jp

National Institute of Informatics, Japan{asada,hidaka,kato,hu}@nii.ac.jp

Abstract

G2

UnCAL was introduced as a graph transformation language for unordered finite graphs, and has a powerful transformation method
for finite graphs: structural recursion. Although UnCAL is powerful and recently applied to model driven software engineering,
there are two major limitations. One is that its graph model is only
unordered graph in which branches of nodes are unordered. The
other is its limited expressive power: structural recursion functionstransform depth-direction well, but not well on sibling-direction.
We solve these problems by generalizing the graph model and extending the expressive power of UnCAL. We generalize the typeof branches of nodes from powerset to general monad, so that we
introduce graph transformation languages λTFG which are parameterized by (finitary) monads T . The special case where T is thefinite powerset monad becomes an extension of UnCAL. Our crucial instance is the case of list monad for treating ordered graph,
where we solve how to define bisimilarity between ordered graphs
having edges labeled by an invisible label ε. Also we extend the expressive power of λTFG from that of UnCAL: higher order functions
and transformations for sibling dimension. We demonstrate that we
can modularize designing graph transformation languages, by ourgeneralization with monads and by monad transformers.

1.

G1

0
0

0

a

∼

1

7→

hd

a
2

a

tl 2

hd
1

tl 2

1

1

0

G′1

∼
/

3

G′2

tl 5

hd
4

a
3
6

Figure 1. An Example of Unsound Encoding

graphs: bulk semantics. With bulk semantics, 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 (like ε transition in automata)to graphs, providing a smart way of treating shared nodes andcycles in graphs. In addition, UnCAL is designed carefully suchthat (i) every transformation is bisimulation generic in the sensethat it returns bisimilar results for bisimilar inputs, and (ii) everytransformation necessarily terminates and transforms finite graphs
to finite graphs.
Despite its beauty in theory and usefulness in graph querying,
there are two limitations in UnCAL that prevent it from being usedwidely. One is that UnCAL can treat only unordered graphs, being
weak in other graph models, such as ordered graphs where edges
from a node are ordered, which is widely used in many applications: e.g., in Ecore, MOF, and KM3 [Jouault and Bézivin 2006].
The other limitation is lack of expressive power of transformations
on sibling dimension. For example, when a graph labeled with natural number, we can not write in UnCAL a transformation which
extracts all such edges of some node that are labeled with the average number among all the siblings.
At the first sight, it seems that the first limitation could be easily
solved by encoding ordered graphs by unordered ones with suitableedge labels, say using hd and tl to represent the first branch and therest of the branches respectively. However, there is a fatal problem
with this encoding. The above encoding is unsound in the context
of UnCAL where ϵ-edges must be taken into account for graphconstruction and structural recursion. As shown in Figure 1, theordered graphs G1 and G2 , where we use dotted arrows to represent
ε-edges, are naturally bisimilar, but their corresponding encodedgraphs G′1 and G′2 are not at all.
In fact, it has been an open problem for more than ten years
whether structural recursion in UnCAL can be extended from unordered graphs to ordered ones or not, since it was first raised in the
conclusion of the paper [Buneman et al. 2000]:

Introduction

Structural recursion, such as fold on lists or catamorphism [Meijer et al. 1991] on algebraic data structures including trees, plays
an important role in functional programming, providing a systematic way for construction and manipulation of functional programs [Bird and de Moor 1996; Gill et al. 1993; Hu et al. 2006].
It is, however, a challenge to define structural recursions for graphdata structures, the most ubiquitous data in computing. This is because unlike lists and trees, graphs are essentially not inductive
and cannot be formalized as an initial algebra in general [Gibbons
1995].
It is certainly possible to use full recursion operator (fixed point
operator) to manipulate infinite data structures such as stream andgraph, but there are many cases targeting only finite graphs especially in database application. Therefore, it is very much desirable
that we could represent graphs in finite form, while guaranteeing
transformations (or queries) for graphs always terminate.
UnCAL [Buneman et al. 2000] was introduced in the databasecommunity to provide such a powerful querying method by structural recursion for finite graphs. The graph model of UnCAL isunordered (directed) graph, where outgoing edges are not ordered.
In UnCAL we can treat graphs semantically as regular trees [Ginali
1979], based on a suitable definition of bisimulation, up to which
finite graphs and regular trees are equivalent.
The benefit from this bisimulation is that structural recursion
on regular trees can be used for graphs, and moreover, it gives
an interesting and important semantics of structural recursion on

1

... we have shown how the principles of UnQL will workon an ordered tree. However, it is not clear how they canbe extended to an ordered graph model. ... we still lack acomplete picture of this topic ...

is proved as first order functions. This higher order bisimulation genericity enables us to introduce higher order functions to UnCAL and reformulation as a lambda calculus.
• We define our graph transformation languages λT
FG as ex-tensions of the simply typed lambda calculus, which is in
sharp contrast to UnCAL (first order calculus). This reformulation does not only provides us higher order functions,but also a clear vision of how to extend λTFG further, withother primitive functions or other type systems such as coproduct types, inductive data types, monad types, and polymorphic types.

In this paper, we provide a novel solution to this open problem,by defining a subtle notion of bisimilarity for ordered graph having
ε-edges so that structural recursion can be extended from that for
unordered graphs to that for ordered graphs. Moreover, we propose
λTFG , powerful higher order graph transformation languages, which
extends the lambda calculus with graph operations generalized withmonads and also extended with sibling transformation.
The main technical contributions of this paper can be summarized as follows.
There are mainly two independent contributions; (i) one is thedefinition of bisimilarity for ordered graphs, which has a subtle
problem of infinite width, which can not be seen in other graphmodels; (ii) the other one is the generalization with monads T and
extension of expressive power of graph transformations: introduction of higher order function and sibling transformation. Further
detail of these contributions are the following:• We show how to overcome the second limitation of UnCAL,

i.e., expressive power on sibling dimension, by introducing
two sibling transformation l-sbl and u-sbl upon the above
flexibility of extensions. For instance, when T = List, we
can manipulate branches of nodes as we transform lists: wecan, for example, reverse the order of branches of a node inan ordered graph with reverse function of list.
• Summarizing the above, we formulate parametrized graphtransformation languages λTFG with monads T .

(i). We give the first definition of the bisimilarity between orderedgraphs having ε-edges, which forms the semantic foundation
for λList
FG . Specifically, we identify that the branch order of evenfinite graphs is not necessarily finite but countable linear order,and clarify that combination of ε-edges and cycles will inducesuch countable linear order on branching, which would produce
new issues not occurring for the unordered case. We show thatthe judgment of emptiness of ordered graphs is decidable, andthat it is decidable whether we can eliminate all ε-edges—withkeeping finite width of graph—for a finite ordered graph having
ε-edges.

(iii). Then we have the following discussion for further extension.
• We extend the structural recursion to unify the above sib-ling transformations with the extended structural recursion,
so that we can transform graphs in depth-direction and in
sibling-direction at the same time.
• Finally we discuss how we can systematically compose

graph transformation languages to increase language power,by using monad transformer. For instance, although λList
FG
can treat ordered graphs but not unordered graphs, by thisPfin ×List
modular method, we can systematically obtain λFG,
which can treat both unordered and ordered graphs.

(ii). UnCAL consists of the following three technical points:• graph models and bisimilarity,

Organization of the Paper We shall start by an overview of λTFG ,focusing on the case when T = List, in Section 2. Then in Section 3, we see the first key technical contribution of this paper, i.e.,the definition of bisimilarity for ordered graphs having ε-edges.
Then we give a general definition of bisimilarity for graphs in λTFG .
In Section 4, we give interpretations of terms of λTFG , which includes graph constructors, structural recursion, and sibling transformations; then we show their bisimulation genericity. In Section 5,
we extend structural recursion with sibling transformation. In Section 6, we discuss how we can extend the languages with monadtransformers. We discuss the related work in Section 7 and conclude the paper in Section 8.

• syntactic graph representation (called graph constructors),and• structural recursion.

We generalize all the three points with monads T and extend
further:• We generalize the graph model in such a way that collec-

tion of outgoing edges of a node has the structure of themonad T . With this, unordered graph and ordered graphcorrespond to finite powerset monad and list monad, respectively. We can see its usefulness from other examples ofmultiset monad and distribution monad which correspondto weighted graph and probability graph, respectively.
Then we give a definition of bisimilarity for such graphmodels generally with T . The above (i), i.e., the definitionof bisimilarity for ordered graph is independent contribution
from this general definition; since for the general definition
we assume existence of iteration operators, which is newly
given in this paper for ordered graph, while those for othergraph models are already known.

2. Overview of λTFG
We start with an overview of our general graph transformation
language λTFG , especially when T = List. In fact, λList
FG , which
treats ordered graphs, is the most important case to understandessence of λTFG . In the following, after giving general definitionof graphs, we will move to the case of List, and see how orderedgraphs are constructed and how structural recursion can be easily
used to transform ordered graphs. In Section 4.4, we will see how
to design the syntax of general λTFG .

• Then according to the generalization of graph model, we

also give generalized definition of graph constructors andstructural recursion with monads. Specifically, we generalize bulk semantics of the structural recursion, and show thatstructural recursion is bisimulation generic. The bisimulation genericity is a stronger result than that in [Buneman
et al. 2000] even for the case of unordered graph, since here
we prove bisimulation genericity of structural recursion asa higher order function, while in [Buneman et al. 2000] it

2.1 Graph Model of λTFG
Graph in λTFG is rooted, directed, and edge-labeled graph. Additionally, graph in λTFG has two prominent features, ε-edges andmarkers. An ε-edge represents a shortcut between the two nodes,
working like the ε-transition in an automaton. Nodes may bemarked with input and output markers, which are used as an interface to connect them to other graphs by ε-edges.

2

We occasionally use record notation (-).V, (-).B, and (-).I forcomponents of a graph: i.e., G = (G.V, G.B, G.I).
We allow a graph to have multiple roots: multi-rooted graph is toforest what single-rooted graph is to tree. For single-rooted graphs,
we often use default marker & to indicate the root, and use DB Y to{& }denote DB Y .
An output marker is a place holder through which the input
node of another graph can be connected with an ε-edge. (This isdone with @, cycle (see Figure 3), and srec (see Figure 7) to be
explained later.)

1

d

2

d d
d b
3

4

&y
(a) A Simple Graph: G(b) An EquivalentGraph: G′(c) Result of
a2d xc on (a)Figure 2. Examples of Graphs

Example 3 (Unordered Graph, Weighted Graph, Probability
Graph). For the finite powerset monad Pfin , Pfin -graph is unordered graph, which is (equivalent to) the graph model of UnCAL.
Let us consider the finite multiset monad (bag monad) Mfin :We introduce the notion of graph with “T -kind of branch” for amonad T . First let us recall the notion of monad (in the Kleisli triple
style): T = (T, return, lift) is a monad on Set if T : Set → Set
is a functor,
return : S → T (S)andlift : (S → T (S ′ )) → (T (S) → T (S ′ ))are natural transformations, and they satisfy certain axioms called
monad laws, see [Benton et al. 2000; Moggi 1989] for the axioms.

Mfin (S) = {ϕ: S→N | ϕ−1 (N−{0}) is a finite set}.
def

Then branch of Mfin -graph has a 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:
Dfin (S) = {ϕ: S→[0, 1] | ϕ−1 ((0, 1]) is a finite set, Σs ϕ(s)=1}.
def

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

Example 1 (List Monad). List is a monad defined as follows.
return(s) = [s] (s ∈ S)
lift f = concat ◦ List(f ) (f : S → List(S ′ ))s 7→ 1

where(other than s) 7→ 0

concat : List(List(S ′ )) → List(S ′ )is flattening a list of lists to a list.

and for f : S → Dfin (S ′ ),lift(f ): Dfin (S) → Dfin (S ′ )()
lift(f )(ϕ): S ′ → [0, 1](ϕ: S → [0, 1]) 7→
s′ 7→ Σs∈S (ϕ(s) · f (s)(s′ ))Now we 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

Dfin -graph has probabilistic branch.

• V is a set of nodes,

2.2 Overview of λListFG• B : V → T (Lϵ ×V +Y ) is a branch function, where an element

From now we see an overview of λTFG when T = List.

x in Lϵ ×V +Y (called a branch) is either an edge Edge (l, v)
or an output marker Outm (&y), and2.2.1• I : X → V is a function, which determines input nodes (roots)

For ordered graphs, we consider bisimilarity as their graph equivalence, which is called value-equivalence in [Buneman et al. 2000],
since we observe only “values” l and &y pointed by a “pointer” v.
For instance, the graphs G and G′ , in Figure 2(a) and 2(b), respectively, are considered as being equivalent. In G′ , nodes 3 and 3′
are bisimilar because both of them only have one outgoing edge labeled d to the node 2. Also in G′ , from node 1 to node 3, there is anε-edge (denoted by the dotted line), which can be eliminated withkeeping its bisimilarity by adding outgoing edge labeled d fromnode 1 to node 2. Unreachable parts from roots are disregarded.
The definition of bisimulation on ordered graphs with ε-edges is
one of the important results in this paper, and this will be addressed
formally in Section 3.
A graph function f is called bisimulation generic if f (G) andf (G′ ) are bisimilar whenever G and G′ are bisimilar. λTFG is
designed to make the interpretation of every term bisimulation
generic.

of the graph.
Note that in the terminology of coalgebra theory, a T -graph is acoalgebra B of the endofunctor T (Lϵ ×(-)+Y ) equipped with |X|number of initial states I.
Example 2 (Ordered Graph). We call List-graphs ordered graphs,
where the branches are ordered. The graph in Figure 2(a) is represented as (V, B, I) where
V
B(1)
B(2)
B(3)
B(4)
I(&)

=
=
=
=
=
=

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

The set of graphs—with X and Y as sets of input and output
markers, respectively—is denoted by T DB X
Y , where T may beomitted if it is clear from context. We call a T -graph a finite T graph when V is a finite set, and write T DB f X
Y for the set offinite T -graphs. (“DB” is from [Buneman et al. 2000] and means“DataBase”.)

2.2.2

Graph Constructors

Figure 3 summarizes the nine graph constructors used in λList
FG , and
their typing rules are shown in Figure 5. They are similar withgraph constructors for unordered graphs in UnCAL [Buneman et al.
2000]. Note that these constructors should be written as e.g. []Y3

σ ::= σ + σ | σ × σ | σ → σ| Bool | Label | DBX
Y| α | Y | List(σ)&x1 ... &xm

a
G1
[]

G
〈a : G〉G2

G1 ++ G2&x&yG&x := G〈&y〉()&x1 ... &xk&x1 ... &xk&x’1 ... &x’m

G1

G2

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

G1
&y1 ... &ym
εε&y1 ... &ym
G2&z1 ... &zn
G1@G2

ε

Γ ⊢ [] : DB∅ε&x1 ... &xmΓ ⊢ e1 : LabelΓ ⊢ e2 : DBYΓ ⊢ ⟨e1 : e2 ⟩ : DBYΓ ⊢ e: DBY{&x}Γ ⊢ &x := e: DBY12
Γ ⊢ e1 : DBXΓ ⊢ e2 : DBXYY(X1 ∩ X2 = ∅)cycle (G)1 ∪X2
Γ ⊢ e1 ⊕ e2 : DBXYΓ ⊢ e: DBX(X ∩ Y = ∅)X∪YΓ ⊢ cycle(e): DBXYe ::= x | λx.e | ee | case e of inl (x) → e or inr (y) → e| inl e | inr e | (e, e) | π l e | π r e { terms of lambda calculus }| if e then e else e{ conditional }| a | &y | e = e{ label (a ∈ L), marker, and their equality }| [] | e ++ e
{ algebraic graph constructors }| ⟨e : e⟩ | ⟨&y⟩ | &x := e | () | e ⊕ e | e @ e | cycle(e)Γ ⊢ (): DB∅Y

Γ ⊢ e1 : DBXYΓ ⊢ e2 : DBYZ
Γ ⊢ e1 @ e2 : DBXZΓ ⊢ e: DBXYΓ ⊢ isEmpty(e): BoolΓ, l: Label, g: DBY ⊢ e1 : DBZΓ ⊢ e2 : DBXZYΓ ⊢ srec(λ(l, g).e1 )(e2 ): DBZ×X
Z×Y
Γ, x: List(Label×DBY +Y ) ⊢ e1 : List(Label×DBY +Y )
Γ ⊢ e2 : DBYΓ ⊢ l-sbl(λx.e1 )(e2 ): DBY{ common graph constructors }| isEmpty(e){ graph emptiness checking }| srec(e)(e){ structural recursion application }| nil | cons(e, e) | foldr(e, e, e) | ...
{ list operators }| l-sbl(e)(e) | u-sbl(e)(e){ sibling transformations }Γ, x: List(Label×α+Y ) ⊢ e1 : List(Label×α+Y )Γ ⊢ e2 : DBXYΓ ⊢ &y : YΓ ⊢ u-sbl(λx.e1 )(e2 ): DBX
Y(Just unfamiliar rules are listed. We use l and g as meta variables
for variables of types Label and DBX
Y , respectively.)

Figure 4. λList
FG Language

Figure 5. Types and Typing Rules of UnCALList

and G1 ++X,Y G2 ; however we will omit the subscript X and Y toavoid clutter.
Let us see each constructor; also see how type discipline on input and output markers works for each constructor. First, [] constructs a root-only graph with the default input marker and no
output markers. For two graphs G1 and G2 having identical input markers and output markers, G1 ++ G2 adds two branching εedges from each new root to the corresponding old roots of G1 andG2 . Next, ⟨a : G⟩ extends G with one a-labeled edge pointing theold root from a new fresh root node; and the constructor ⟨&y⟩ constructs a graph with a single node marked with an output marker &y(in [Buneman et al. 2000], ⟨a : G⟩ and ⟨&y⟩ are denoted as {a : G}and &y, respectively). Marker renaming &x := G associates an input
marker &x to the root node of G; () constructs a trivial graph thathas neither a node nor an edge; and G1 ⊕ G2 constructs a disjoint
union of G1 and G2 , where their branching functions B1 and B2
work independently. Then, G1 @ G2 composes two graphs sequentially by connecting the output nodes of G1 with the corresponding
input nodes of G2 by ε-edges, and cycle(G) connects the output
nodes with the input nodes of G to form cycles. It is worth notingthat this set of constructors are powerful enough to describe any
finite ordered graphs.

The graph constructors here are described separately, divided
into algebraic graph operators and common graph constructors.
Algebraic graph operators depend on T , while the seven common
graph constructors are fixed independently from T . In fact, algebraic graph operators further depend on signatures of T , as seen in
Section 6; but independently from choice of such signatures, theirexpressive power remains the same not just on closed terms but
also on open terms. The boolean expression isEmpty(e) resultsin true when the graph of the result of e has no non-ε edge in theaccessible part.
Structural Recursion Now we explain structural recursion,
which is a powerful mechanism borrowed from UnCAL [Buneman et al. 2000] to describe graph transformations. The structural
recursion f = srec(λ(l, g).e) is such a function that f satisfies thefollowing equations, where we ignore output markers and consider
the case when X is singleton, for simplicity:f ([])
f (⟨l : g⟩)f (g1 ++ g2 )

=
=
=

[]
e(l, g) @ f (g)f (g1 ) ++ f (g2 )The above equations give a definition of f as a function which
inputs finite graphs and outputs infinite graphs, in recursive way.
However the outputs of f are in fact (bisimilar to) finite graphs, and
it is made clear by the bulk semantics of f , which will be given in
Section 4.2. Intuitively, in the bulk semantics, structural recursion
f transforms a graph in a bulk way by keeping structure of thegraph—as map functions for list or tree—, transforming each edge
labeled l to new graph parts e(l, g). Here e can refer not only thelabel l but also its successor graph g in the input graph of f .

Syntax of λList
FG

Our graph transformation language λListFGΓ ⊢ e1 : DBXYΓ ⊢ e2 : DBXYΓ ⊢ e1 ++ e2 : DBX
Y(&y ∈ Y )Γ ⊢ ⟨&y⟩: DBY

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

Figure 3. Graph Constructors

2.2.3{ variant, product, function types }{ base types }{ types for sibling transformation }(and in general λTFG )is an extension of the simply typed lambda calculus with graphconstructors and graph operations. The syntax of λList
FG is depicted
in Figure 4, and the types and typing rules are in Figure 5.
X
The type DBX
Y is interpreted to DB f Y : the set of finite graphs,
and α are type variables, which are used just for u-sbl and explained later. We omit the standard explanations for lambda terms,
conditional, label, and equality for labels.

4

Example 4. The following structural recursion a2d xc replaces alllabels a with d and contracts edges labeled c.

00

Gs

a

0

a2d xc = srec(rc)

∼

a

where
rc = λ(l, g). if l = a then ⟨d : ⟨&⟩⟩

11

else if l = c then ⟨&⟩

a
1

...
01 11

...

∼

10

00

01 20

a

a

∼

... 11 ... ... 21 ...

a
...

11

...

a

a
...

...

01

21

Figure 6. Graphs with Stream Branching and with Dense Branching

toc(db) = srec( λ(l, g). if l = section

give a general definition of bisimilarity for T -graphs. Finally, we
extend the bisimilarity equivalence from graph types to higher
order function types.
We here remark that our bisimilarity for the invisible label εis different from weak bisimilarity for the invisible label τ in thecontext of process algebra [Milner 1999]. Our bisimilarity is characterized by the ε-elimination (Proposition 8.2) which is familiar
in automata theory. One purpose of our use of ε-edge is to postpone calculation of graph constructors, structural recursion and soon, but weak bisimilarity is unsuitable with respect to properties ofsuch graph transformations: e.g. associativity of ++ fails with weakbisimilarity.

then ⟨section : (get title(g) ++ ⟨&⟩)⟩
else ⟨&⟩ ) (db)where the function get title results in the title of the section.
get title(g) = srec( λ(l1 , g1 ). if l1 = title
then ⟨title : srec( λ(l2 , g2 ).⟨l2 : []⟩ ) (g1 )⟩else [] ) (g)Sibling Transformation Structural recursion functions are powerful transformations which terminate at evaluation and preserve
finiteness of graphs, but we need more expressive power: transformations on sibling dimension.
Let us consider an ordered graph and its unfolded (maybe infinite) tree. The branches under the root are then a list of the subtrees.
Then if one wants to, e.g., reverse the order of the branches under
the root, we can not do so with the structural recursion.
To resolve this problem, we introduce local sibling transformations l-sbl and uniform sibling transformations u-sbl, which enable such transformations. The former l-sbl transforms branches
only of the root node of a single-rooted graph; and by combination
with the structural recursion, l-sbl can transform branches of any
one node which the structural recursion function can reach. The
latter u-sbl transforms branches uniformly of all nodes in a graph.
Let us return to the Figure 4. List operators in the syntax areusual ones; we can add anything that is convenient such as car,cdr, filter, and reverse etc. These list operators are used forthe two sibling transformations; l-sbl(λx.e) and u-sbl(λx.e)transform sibling as λx.e transforms lists. In the typing rule foru-sbl, we use type variables α to prepare a parametric polymorphic function λx.e on List(Label×α+Y ) so that λx.e andhence u-sbl(λx.e) become “uniform” on α. The parametricity
guarantees bisimulation genericity of u-sbl. For the detail see
Section 4.3.

3.

∼

a
0

Example 5. 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 [Robertson et al. 2009],
computes the table of contents of books in which sections can bearbitrarily nested:

aa

00

Gb

Applying the function a2d xc to the graph in Fig. 2(a) yields thegraph in Fig. 2(c).

10

a

1

else ⟨l : ⟨&⟩⟩

00

01

3.1 Bisimilarity for Ordered Graph
Now we see the bisimilarity between ordered graphs: its intuition
and formal definition.
Intuition of the Bisimilarity
First let us see some examples of ordered graphs in order to havesome feeling of the bisimilarity to be defined. Consider the graphs
in Figure 6. For the graph Gs , first, in order to make our problem
easily understandable, let us unfold the graph to an infinite tree, i.e.,
the graph in the middle. Then intuitive “ε-elimination” of the tree
is the graph on the right, where the branching is as a stream. Notethat for ordered graph there is no idempotency which unorderedgraph has. The way of branching of graphs having ε-edges arethus possibly infinite essentially. However, it is not necessarily justa stream type, as in the next example Gb . Unfolding of graphGb yields the tree in the middle, and then its “ε-elimination” isthe graph on the right. This graph has a branch like the orderedset {n/2m ∈Q | n, m ∈ N, 0<n<2m }, which is a dense countablelinear ordered set. (In this paper, the term countable includes thecase of finite.)
In fact, for any countable linear ordered set, there is someordered graph having ε-edges such that the branches of the root
after eliminating ε-edges are exactly as the given ordered set. (Forthe detail, see Appendix A.)

Bisimilarity for ε-edge and Ordered Graph

Section 2.1 gives a general definition of T -graph, for a monad T .
To this end, we shall give the semantic equivalence for the graphmodel of λTFG : bisimilarity between T -graphs.
The main point is a treatment of ε-edge. The case of orderedgraph (List-graph) involves a big problem which does not occur
for unordered graph (Pfin -graph): i.e., ε-elimination might induce
infinite width. In the following, we shall see the problem andhow to define bisimilarity between ordered graphs. Also we givesome effective procedure to avoid such infinite width. Then we

Formal Definition of the Bisimilarity
Now let us define bisimilarity between ordered graphs. As seen
above, the ε-elimination of an ordered graph might induce countable width. So we shall first define a generalized notion of “orderedgraph with countable width”, and define bisimilarity for such generalized graphs. This asks us to extend the list monaddef

List(S) = Σn∈N S n

5Proposition 8. 1. For all CList-graphs G ∈ CList DB X
Y ,ε-elim(G) has no ε-edge, and G and ε-elim(G) are bisimilar.
′
2. For CList-graphs G, G′ ∈ CList DB X
Y , G and G are bisimi′
lar if and only if ε-elim(G) and ε-elim(G ) are bisimilar.

to the countable list monad CList which can be defined as thefollowing:def

CList(S) = ΣL∈L S L
where N is generalized to L, the set of countable linear orderedsets up to order isomorphism (with chosen representatives L). (SeeAppendix B for the precise definition of CList.) Thus we extend
ordered graphs to CList-graphs.
For B(v) ∈ ΣL∈L (Lϵ ×V +Y )L , let |B(v)| denote the countable linear ordered set L of B(v). Then, we call i ∈ |B(v)| abranch index of a node v, and write B(v).i ∈ Lϵ ×V +Y for thei-th branch.
Next we prepare the notion of “transitive closure” of ε-edges.
Let G = (V, B, I) ∈ CList DB X
Y and v ∈ V . Let us consider apair of an ε-path from v and a branch index in of the last node inthe ε-path:εHere we first gave the definition of bisimilarity for graphs having ε-edges and then gave that of ε-elimination and the above
proposition. However, we can define the bisimilarity for graphs
having ε-edges by the equivalence stated in Proposition 8.2 with the
ε-elimination and with the bisimilarity for graphs having no ε-edge;
the latter can be easily derived from general coalgebraic definitionof bisimilarity [Rutten 2000]. Then we see that such definition is
not just equivalent to but almost the same as that in Definition 6.
Thus we find that the key here is the definition of ε-elimination.
In the following we give a general definition of bisimilarity for T graphs by ε-elimination.

εv (= v0 ) →i0 v1 ... →in−1 vn →in (n ∈ N)

3.2 Decidability for Finite Width Graphs

where vn →in means just that in ∈ |B(vn )|. We call this proper
branch of v if the in -th branch B(vn ).in is not an ε-edge, i.e., it
is either a non-ε edge or an output marker. The set of all proper
branches of v in G is denoted by Pb(G, v). It is easily shown that
Pb(G, v) is a countable set.
Then there is a natural linear order ≤Pb on Pb(G, v): for two
different proper branchesεBefore going to the general setting with monads T , we give one
important decidability result for CList-graphs.
Let FG/ε be the set of finite List-graphs which are bisimilar tosome finite List-graphs having no ε-edge. There is a procedure
which answers, for a finite List-graph G, if G is in FG/ε or not.
If G is in FG/ε, we can effectively eliminate ε-edges; otherwise, it
is impossible to eliminate ε-edges, keeping finite width. This procedure is as the following. First note that for each node accessible
from a root, we can check if there is an ε-cycle—a cyclic path consisting only of ε-edges—on the node. Then if, for every accessible
node with ε-cycle, there is no proper branch, then the input graphis in FG/ε; otherwise, not in FG/ε.
This is enough for run-time use of the query language λList
FG ,because, though we need ε-edge for implementation—for structural
recursion and for efficiency of graph calculation—practical graphs
in the real world has no ε-edge. If a user of the language writes
such a practical query, then the result should return a graph in FG/ε;
if it is an incorrect query not intended by the user, and then if theresult has inevitable ε-edges, the procedure above can check it andcan warn the user.
Note that, in the class FG/ε, since we can eliminate ε-edges, we
can obtain familiar effective procedures for bisimilarity-checking
and for obtaining the minimum graphs in a similar way to unordered graph. Also note that if G is not in FG/ε, then G is not
empty, hence isEmpty is decidable.

εp = (v →i0 v1 ... →in−1 vn →in ),p′ = (v →i′0 v1′ ... →i′ ′
ε

ε

n −1

vn′ ′ →i′ ′ ),ndef

we obtain their branch indices sequences: p̃ = (i0 , ..., in−1 , in )def
and p̃′ = (i′0 , ..., i′n′ −1 , i′n′ ). With the starting node v, we canrecover p and p′ from these indices sequences. Then, between p̃
and p̃′ , we can consider lexicographical order ≤l , then we definedefp ≤Pb p′ ⇐⇒ p̃ ≤l p̃′ .
Now we define the bisimilarity.
Definition 6 (Bisimilarity). For CList-graphs G = (V, B, I), G′ =′(V ′ , B ′ , I ′ ) ∈ CList DB X
Y , a relation R between V and V is′called a bisimulation relation if for any vRv , there is an order isomorphism f : (Pb(G, v), ≤Pb ) → (Pb(G′ , v ′ ), ≤Pb ) satisfying
the following property. For any proper branchεp = (v →i0 ... vn →in ) ∈ Pb(G, v)
withf (p) = (v ′ →i′0 ... vn′ ′ →i′ ′ ) ∈ Pb(G′ , v ′ ),ε3.3 Generic Definition of Bisimilarityn

Now we define the notion of bisimilarity in general for T -graphs.
We define this bisimilarity for any monad T whose Kleisli category
SetT has a uniform iteration operator.
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 ′are functions S → T (S ′ ). The identity morphism id on S is

• if B(vn ).in = Edge (l, u) for some l ∈ L, u ∈ V , then there

exists u′ ∈ V ′ such that B ′ (vn′ ′ ).i′n′ = Edge (l, u′ ) and uRu′ ,′′• if B(vn ).in = Outm (&y) for some &y ∈ Y , then B ′ (vn′ ).in′ =Outm (&y).
Two graphs G and G′ are bisimilar (denoted by G ∼ G′ ) if there isa bisimulation relation R such that for every input marker &x ∈ X,
I(&x ) R I ′ (&x ).

def

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

Note that the bisimulation relation is an equivalence relation on
CList DB X
Y . Next, let us define ε-elimination.

g ◦ f = lift(g) ◦ f : S → T (S ′′ ).
defDefinition 7 (ε-elimination). For a CList-graphs G = (V, B, I) ∈CList DB X
Y , ε-elimination ε-elim(G) of G is a CList-graphdef′(V, B ′ , I) ∈ CList DB X
Y where |B (v)| = Pb(G, v) and forεdef
p = (v →i0 ... vn →in ) in |B ′ (v)|, B ′ (v).p = B(vn ).in .

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

in l = return ◦ in l : S1 → T (S1 +S2 )def

in r = return ◦ in r : S2 → T (S1 +S2 ).

Note that the ε-elimination does not change sets of nodes.

6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.,

Before that, let us recall the notion of bisimulation relation forgeneral endofunctor F on Set. First we recall F -lift of relations:for (the inclusion function of) a relation r: R ,→ V ×V ′ , let
def
def
r1 = pr l ◦ R: R → V and r2 = pr r ◦ R: R → V ′ ; so

[f1 , f2 ]: S1 +S2 → T (S ′ ).
We write ∇: S+S → T (S) and + for the codiagonal and thecoproduct on morphisms in SetT , respectively.
Next we recall the notion of iteration operator [Haghverdi 2000;
Kakutani 2002], which is the dual notion of fixed point operator [Simpson and Plotkin 2000]; also, iteration operator is to while
operator as coproduct type is to the boolean type. Though iteration
operator can be defined for any category with finite coproducts, wehere define directly on the Kleisli category SetT of a monad T on
Set. An iteration operator iter on SetT is a function which maps
a function
f : S → T (S+A)
toiter (f ): S → T (A)such that the mapping satisfies the following axioms:⟨F (r1 ), F (r2 )⟩ : F (R) → F (V )×F (V ′ ).
Then F̃ (R) is defined as the image⟨F (r1 ), F (r2 )⟩ (F (R)) ⊆ F (V )×F (V ′ ).
For a functor F on Set, and two coalgebras of F , i.e., two functions 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) ⊆ F̃ (R).
Definition 10 (Strong Bisimilarity and Bisimilarity). Let T bea monad, and G = (V, B, I) and G′ = (V ′ , B ′ , I ′ ) be T ′graphs in T DB X
Y . Then G and G are strong bisimilar if there
is a bisimulation relation R w.r.t. the endofunctor T (Lϵ ×(-)+Y )between B and B ′ such that for any &x ∈ X, I(&x ) R I ′ (&x ).
Now let iter be a uniform iteration operator in SetT . Then
G and G′ are bisimilar (written as G ∼ G′ ) if ε-elim(G) and
ε-elim(G′ ) are strong bisimilar.

• (naturality:) for f : S → T (S+A) and g: A → T (A′ ),g ◦ iter (f ) = iter ((id S +g) ◦ f ): S → T (A′ ),• (dinaturality:) for f : S → T (S ′ +A) and g: S ′ → T (S+A),

Note that the notions of ε-elimination and bisimilarity depend
on a given iteration operator, but in this paper we do not refer the
dependency in the terminology.
We assume that all monads T in the paper preserve weakpullbacks, which is just a mild assumption often used in coalgebra
theory [Rutten 2000; Sokolova 2005]. Especially, then T preserves
injections and finite intersections. Using this assumption, it is easily checked that the strong bisimilarity relation is an equivalence
relation on T DB X
Y .
It is immediately shown that strong bisimilarity implies bisimilarity from the uniformity of an iteration operator. We use thisproperty in some proofs in the papers. (In fact we can weaken theassumption of uniformity to that of uniformity with respect to morphisms in Set [Simpson and Plotkin 2000, Definition 2.7].)
Thus we gave the definition of bisimilarity, but it is not necessary that every monad has an iteration operator in the Kleisli category. However, as the case of List with CList, there is the casethat a monad T is presentable in programming languages, does nothave iteration operator, and has an extension T ′ which might not bepresentable in languages but has a uniform iteration operator. We
say that T has an extension T ′ for ε-elimination if there is a monadT ′ , an injective monad morphism ι : T ,→ T ′ , and a uniform iteration operator in the Kleisli category of T ′ . Here monad morphism
is a natural transformation which is compatible with return’s, andwith lift’s (see [Benton et al. 2000], for the detail).
By this, we generalize the definition of bisimilarity:[iter ([f, in r ] ◦ g), id A ] ◦ f = iter ([g, in r ] ◦ f ): S → T (A)• (unfolding:) for f : S → T (S+A),

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

iter (iter f ) = iter ((∇+id A ) ◦ f ): S → T (A).
Further, iter is called uniform if for functions f : S → T (S ′ ),g: S ′ → T (S ′ +A) and h: S → T (S+A),
iter (g) ◦ f = iter (h): S → T (A)wheneverg ◦ f = (f +id A ) ◦ h: S → T (S ′ +A).
The axiom of uniformity is used for logical relation for iteration
operator [Hasegawa 2002]. We use uniformity to show that strong
bisimilarity implies bisimilarity.
The following characterization of ε-elimination as iteration operator is due to [Hasuo 2011; Jacobs 2010a].
Definition 9 (ε-elimination). Let T be a monad and iter be an iteration operator in SetT . For an T -graph G = (V, B, I) ∈ T DB X
Y ,′its ε-elimination ε-elim(G) ∈ T DB X
Y is (V, B , I) wheredef
B ′ = embed ◦ iter (iso ◦ B); here embed is the embedding
T (L×V +Y ) → T (Lϵ ×V +Y ), and iso is the composition ofT (Lϵ ×V +Y ) ∼= T ((L+1)×V +Y ) ∼= T (V +(L×V +Y )).

Definition 11 (Bisimilarity Generalized on Size). Let T be amonad which has an extension T ′ for ε-elimination. Then thereX
X
is the embedding ι-DB X,→ T ′ DB Y which maps
Y : T DB Y′
(V, B, I) to (V, ι(Lϵ ×V +Y ) ◦B, I). For G and G in T DB X
Y , G
X
′
and G′ are bisimilar if ι-DB X
Y (G) and ι-DB Y (G ) are bisimilarin the sense of Definition 10.

Conversely, ε-elimination induces an iteration operator; let
us consider a T -graph (V, B, I) in the case when L = 0. Then
B : V → T ({ε}×V +Y ), and if we apply ε-elimination, the resulting branch function is B ′ : V → T (0×V +Y ). That is, we getan operator which maps a function V → T (V +Y ) to a function
V → T (Y ). This is just the same as the structure of an iteration
operator in the Kleisli category (if we allow Y to be arbitrarysets); and we find that it is natural to adopt the axioms of iteration
operator also as axioms of ε-elimination.
Now we give a general definition of bisimilarity for T -graphs,
using the above ε-elimination.

By the assumption that ι has injective components andT preserves weak pullback, ι-DB X
Y reflects strong bisimilarity [Sokolova 2005, Theorem 4.3.6], and hence for T -graphs having no ε-edges, strong bisimilarity and the above bisimilarity areequivalent.
Example 12. It is easy to see that the original bisimilarity for
unordered graphs is equivalent to the general definition of bisimilarity with T = Pfin and T ′ = Pcnt : countable powerset. For

7f : S → Pcnt (S+S ′ ),model of λTFG in the cartesian closed category Set, see the textbook [Mitchell 1996] for the detail. Note that the above lifting tofunction types is possible for any equivalence relations such as
strong bisimilarity.
In the next section we show the bisimulation genericity for all
constants.

∪
defiter (f )(s) =(f2 ◦ (f1 )n )(s)),
n∈N

where
def

f1 = [id S , const {} ] ◦ f : S → Pcnt (S)f2 = [const {} , id S ′ ] ◦ f : S → Pcnt (S ′ )def

4. UnCAL Generalized with Monadand the n-times composition (f1 )n is that in SetPcnt .
Similarly, finite multiset monad Mfin has an extension for εelimination, i.e., countable multiset monad Mcnt :In this section we give interpretations of terms of λTFG and show
their bisimulation genericity. As explained in the last of the previous section, it is enough to consider only constants; we will see
graph constructors, structural recursion, and sibling transformations. In the last place, we see how to define syntax of λTFG .

Mcnt (S) = {ϕ: S → N∪{∞} | ϕ−1 (N−{0}) is countable}.
def

The iteration operator for Mcnt is given with the same formula asthat for Pcnt .
Also finite probability distribution monad Dfin has an extension
for ε-elimination, i.e., countable subprobability distribution monaddef
SubD cnt : SubD cnt (S) =4.1 Graph Constructors
UnCAL and λList
FG respectively have nine graph constructors, as in
Section 2.2.2, by which we can represent all finite graphs. Here
we define such graph constructors for T -graphs by which we canrepresent all finite T -graphs.
Among the nine graph constructors of λList+ are inFG , [] and +herent in the list monad List, and the other seven constructors arecommon for all monads. List(S) is free monoid (generated by a set
S), which has nullary and binary operations: unit and multiplication. The nullary graph constructor [] and binary graph constructor++ correspond to the unit and the multiplication, respectively.
First we define the seven common graph constructors for T graphs.

{ϕ: 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 forthat of the abort of the iteration operator. The definition of the iteration operator for SubD cnt is also similar to those for Pcnt andMcnt , see [Jacobs 2010b] for the detail.
For List with CList, conversely rather we can give the iteration
operator in SetCList with the ε-elimination in Definition 7 in theway described after Definition 9.

Definition 13 (Common Graph Constructors).
3.4

Bisimilarity for Higher Order Functions• For G = (V, B, I) ∈ DB Y ,So far we have given the semantics for base types, i.e., bisimilarity
for graph types DBX
Y , and give just equality relations for the otherbase types. Here we extend such equivalence relations for basetypes to higher order function types.
It is well known that if we want to lift equivalence relation tofunction types then we need to switch from the notion of equivalence relation to that of partial equivalence relation, i.e., an equivalence relation on some subset of an original set. This is because,
now not all functions on DB f X
Y are bisimulation generic, so wehave to cut out the subset consisting of bisimulation generic functions.
Now let us see the formal definition. Let σ be a type of λTFG .
We define binary logical relation ∼σ from the above equivalence
relations on the base types. Let us recall the logical relation ∼σ
only on the essential case, i.e., function type: σ = σ1 → σ2 . By
induction hypothesis, we already defined a binary relation ∼σi ondef[[σi ]]. Then we define a binary relation ∼σ on [[σ]] = [[σ1 ]] → [[σ2 ]]as⟨l : G⟩ = (V ∪ {v0 : fresh}, B ′ , {& 7→ v0 }) ∈ DB Y()
def
B ′ = B ∪ {v0 7→ return Edge (l, I(&)) }.
def• For G = (V, B, I) ∈ DB Y ,
{&x}

def

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

• For &y ∈ Y ,def⟨&y⟩ = ({&}, {& 7→ return(Outm (&y))}, id {&} ) ∈ DB Y .
• () = (∅, ∅, id ∅ ) ∈ DB ∅Y .
def

′
′
′
′
X
• For G = (V, B, I) ∈ DB X
Y and G = (V , B , I ) ∈ DB Y′′

such that X ∩ X = ∅,G ⊕ G′ = (V +V ′ , B ′′ , I+I ′ ) ∈ DB X∪X
Y
def

′

B ′′ = [T (Lϵ ×(in l )+Y ) ◦ B, T (Lϵ ×(in r )+Y ) ◦ B ′ ]deff ∼σ f ′ ⇐⇒ ∀x, x′ ∈ [[σ1 ]]. (x ∼σ1 x′ ⇒ f (x) ∼σ2 f ′ (x′ ))def: V +V ′ → T (Lϵ ×(V +V ′ )+Y ).

⇐⇒ ∀x ∈ |∼σ1 |. f (x) ∼σ2 f ′ (x).

′
′
′
′
Y
• For G = (V, B, I) ∈ DB X
Y and G = (V , B , I ) ∈ DB Z ,Then for any type σ, ∼σ becomes a partial equivalence relationon [[σ]], i.e., an equivalence relation on the subset

G @ G′ = (V +V ′ , B ′′ , in l ◦ I) ∈ DB X
Z where
def

def

′′
B
 (in l (v)) = lift(f )(B(v))
f : Lϵ ×V +Y → T (Lϵ ×(V +V ′ )+Z)
 Edge (l, v) 7→ return(Edge (l, in l (v)))
Outm (&y) 7→ (T (Lϵ ×(in r )+Z))(B ′ (I ′ (&y)))def|∼σ | = {x ∈ [[σ]] | x ∼σ x}.
We call a function f : [[σ1 ]] → [[σ2 ]] (higher order) bisimulation
generic if f is in |∼σ1 →σ2 |, i.e.,∀x, x′ ∈ [[σ1 ]]. (x ∼σ1 x′ ⇒ f (x) ∼σ2 f (x′ )).

B ′′ (in r (v ′ )) = (T (Lϵ ×(in r )+Z))(B ′ (v ′ )).
• For a graph G = (V, B, I) ∈ DB X
X∪Y where X ∩ Y = ∅,defcycle(G) = (V, B ′ , I) ∈ DB X
where
Y
def

Then by the Basic Lemma of logical relation, interpretationsof all the terms are bisimulation generic if interpretations of
all the constants are bisimulation generic; and then we obtain a8′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))
def

and in this case, we call such Σ a family of signature sets of T and
we call elements in Σ(n) signatures.
Example 14. The three monads Pfin , Mfin , and List correspondto (upper) semilattice, commutative monoid, and monoid, respectively; then their zero ary operations and binary operations correspond to signatures as below.
For Pfin ,Outm (&y) 7→ Outm (&y)
In the definition of B ′′ (in l (v)) in the definition of @, by replacing lift(f )(B(v)) with T (f ′ )(B(v)) wheredef⊆ Pfin (0)def⊆ Pfin (2)Σ(2) = {{0, 1}}

f ′ : Lϵ ×V +Y → Lϵ ×(V +V ′ )+Zdef

Σ(n) = ∅Edge (l, v) 7→ Edge (l, in l (v))()
Outm (&y) 7→ Edge ε, I ′ (&y)(for other n).

For {} ∈ Σ(0), c{} = {} ∈ Pfin (S), and as seen above,\{0,1} = ∪: Pfin (S)2 → Pfin (S).

we obtain @′ operator, which is bisimilar to @ operator. With @operator, we find that we do not need ε-edge for graph constructors
except for cycle, but @′ is useful to postpone extra calculation of@, which is in effect equivalent to one step of ε-elimination.
We note that the multi-rootedness is semantically the same as
X∼
power of sets of graphs (or tuple of graphs): DB f X
Y = (DB f Y ) .
X
The function DB f Y → (X → DB f Y ) is G 7→ (&x 7→ ⟨&x ⟩ @ G),
and the inverse isThen any element in Pfin (S) can be represented as a compositionof these operators and singletons, i.e., elements in return(S): e.g.
{a, b, c} = ({a} ∪ {b}) ∪ {c}.
For Mfin , similarly,
Σ(0) = {{}}def

⊆ Mfin (0)def⊆ Mfin (2)Σ(2) = {{0, 1}}

f 7→ (&x1 := f (&x1 )) ⊕ ... ⊕ (&xn := f (&xn ))def

Σ(n) = ∅when X = {&x1 , ..., &xn }. Still multi-rootedness is useful for
efficient implementation, i.e., to share bisimilar nodes and to savethe size of graphs as small as possible.
Now we define the other graph constructors which depend oneach monad T . For Proposition 19 and so on, we finally assume
that a monad T is finitary; though we can postpone the definitionof finitary monad till Proposition 19, we first explain finitary monadso that the reader has more concrete intuition in the following
definitions and propositions.
A finitary monad on Set is a monad T on Set such thatthe functor T preserves all directed colimits in Set. We use thisproperty only in the following form (and an equivalent condition
explained soon): for any set S, and any x ∈ T (S), there is a
finite subset S ′ ⊆ S such that 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 have a finite subset {4, 1, 6} ⊆ N
and [4, 1, 6, 4, 6, 4] ∈ List({4, 1, 6}).
Next we recall one equivalent condition of finitary monad T :shortly speaking, T is generated by finite arity algebraic operations.
For a monad T on Set, an element f ∈ T (A) can be seen
as an |A|-ary algebraic operation on T (S) for any S ∈ Set: forg ∈ T (S)A ,(for other n).

Here {} and {0, 1} are regarded as multisets.
For List, similarly again,
Σ(0) = {[]}def

⊆ List(0)def⊆ List(2)Σ(2) = {[0, 1]}def

Σ(n) = ∅(for other n).

For Dfin ,defΣ(2) = {sig r : 2 → [0, 1] | r ∈ [0, 1]}def

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

def

def

where sig r is defined as sig r (0) = r and sig r (1) = 1−r. Thendr (ϕ0 , ϕ1 ) ∈ Dfin (S) is
for ϕ1 , ϕ2 : S → [0, 1] in Dfin (S), sigdsig r (ϕ0 , ϕ1 ): S → [0, 1] such thatdr (ϕ0 , ϕ1 )(s) = r · ϕ0 (s) + (1−r) · ϕ1 (s).
sig
Now recall that “singletons” in Dfin (S), i.e., elements in return(S)are given as the Dirac delta functions δs as in Example 3. Then it
is easy to see that the above family becomes a family of signaturesets; for example, ϕ: N → [0, 1] in Dfin (N) such thatdef
fb(g) = lift(g)(f ) ∈ T (S).
For example, when T = Pfin , for f = {0, 1} ∈ Pfin ({0, 1}) and
g0 , g1 ∈ Pfin (S),111
, ϕ(1) = , ϕ(2) = ,2
63
ϕ(n) = 0 (for other n),ϕ(0) =

fb(g0 , g1 ) = lift(0 7→ g0 , 1 7→ g1 )({0, 1}) = g0 ∪ g1 ,can be represented by signatures and “singletons” as
1
1
1
ϕ = δ0 + δ1 + δ2
2
6
3
1
1 1
2
= δ0 + ( δ1 + δ2 )2
2 3
3
d1 (δ0 , sig
d1 (δ1 , δ2 )).
= sig\i.e., {0,1} = ∪.
For a monad T , let us take a family of sets Σ(n) ⊆ T (n)(n ∈ N), where we regard n as the set {0, ..., n−1}. Let us define(i)TΣ (S) ⊆ T (S) (S ∈ Set) by induction on i ∈ N as below:(0)Σ(0) = {{}}defTΣ (S) = return(S) ⊆ T (S)

2

def
(i+1)
(i)
TΣ (S) = {fb(g) ∈ T (S) | m ∈ N, g ∈ (TΣ (S))m f ∈ Σ(m)}.

3

The above family of signature sets of Dfin has infinitely manysignatures. Still, when implementing λTFG in a programming language, one can represent it as the image of a function. For example, first let us interpret Dfin (S) as FinSet(S×Float) (or with finite multiset instead of finite set). Here a distribution f ∈ Dfin (S)Then a monad T is finitary if and only if there is a Σ such that
∪ (i)T (S) =TΣ (S),i∈N

9

In the former there are extra A-copy of X, i.e., Σi∈A (X) than thelatter; but with @ (rather than @′ ) in Definition 15, the nodes inΣi∈A (X) in the former are not reachable from the roots in theformer graph, so can be ignored.
The second and third points are immediate from the first pointby the definition of a family of signature sets of a finitary monad.

is regarded as a relation rather than a function, then a probability
f (s) ∈ [0, 1] can be regarded as the sum of the multi values off (s). Then the family of signature sets Σ for Dfin is presented as
sig: Float → Dfin (Nat) defined as below:
let sig r = {(0,r), (1,1-r)}
Now we define a graph constructor for T -graphs for each algebraic operator of T , i.e., for each element in T (A). Before this, notethat in the definitions of graph and common graph constructors, we
can easily extend set of marker from finite to arbitrary set A, and ⊕
=
A×X
A ∼
from binary operator to A-ary operator: ⊕: (DB X.
Y ) → DB Y
These are used in the following definition, but the reader who isinterested only in finite A’s—which are enough for implementablelanguage—may apply the following simply to the case A = n ={0, ..., n−1}.

This proposition also implies that T -algebraic graph constructors obey the same axioms as those of algebra of T . For example, finite powersets are free algebras of upper semilattice, hence
the graph constructors {} and (-) ∪ (-) satisfy all axioms of upper
semilattice: i.e., associativity, unitality, commutativity, and idempotency.
Proposition 18 (Bisimulation Genericity of Graph Constructors).
All the graph constructors (including @′ ) are strong-bisimulation
generic and also are bisimulation generic.

Definition 15 (T -Algebraic Graph Constructors). Let T be amonad on Set. For f ∈ T (A) (A ∈ Set), and a finite set X, let
defXGXf = (X, B, id ) ∈ DB A×X where

Proof. It is obvious that they are strong-bisimulation generic. Then,for a graph constructor f , prove that ε-elim(f (G1 , ..., Gn )) is
bisimilar to ε-elim(f (ε-elim(G1 ), ..., ε-elim(Gn ))). (For the caseof cycle, use unfolding axiom of iteration operator.) This implies
that strong-bisimulation genericity implies bisimulation genericity.

def

B(&x) = T (g)(f ) ∈ T (Lϵ ×X+A×X),
g: A → Lϵ ×X+(A×X)&a 7→ Outm ((&a, &x)) .
A
Then we define a T -algebraic graph constructor f : (DB X
Y ) →
def
X
X A
X
DB Y . For (Gi )i∈A ∈ (DB Y ) , f ((Gi )i ) = Gf @ (⊕((Gi )i )).

The next proposition is the most important property of the graphconstructors, for which we require T to be finitary.

We call T -algebraic graph constructors and the common graphconstructors graph constructors.

Proposition 19 (Full-Representability). Let T be a finitary monadon Set which has an extension for ε-elimination. Any finite T graphs can be constructed by the graph constructors.

Example 16. When T = List, let us consider f = [0, 1] ∈ Σ(2)in Example 14. Let us see the picture of G1 ++ G2 in Figure 3. Thisis the @′ version of [0, 1](G1 , G2 ). The top m-roots are G[0,1] andthe ε-edges are those by @′ ; and one can find that the juxtapositionof two graphs G1 and G2 in G1 ++ G2 are the same as that in
G1 ⊕ G2 in the same figure.

Proof. The proof is basically the same as that for UnCAL [Buneman et al. 2000]. See Appendix D for the detail.

Proposition 17. Let T be a monad on Set with an extension for
ε-elimination. For f ∈ T (A) (A ∈ Set), and fi ∈ T (Ai ) (i ∈A, Ai ∈ Set), let⨿⨿⨿
fi : A(∼1) → T (
Ai )
=
i∈A

i∈A

4.1.1

We give an important remark on “representability” of monads inlanguages, which explains why we need care to infinite width for
List-graphs, and why we do not need such special care for Pfin graph.
For T with an extension for ε-elimination T ′ , we defined εelimination for any T -graphs, but in fact it is enough to define
ε-elimination for finite T -graphs, since our languages target only
finite graphs. If T is finitary, in order to define ε-elimination only
for finite T -graphs, without loss of generality we can replace theextension T ′ with its finitary part T ′ |fin :def ∪T ′ |fin (S) = S ′ ∈Pfin (S) T ′ (S ′ ).

i∈Abe the coproduct of the morphisms fi : 1 → T (Ai ) in the Kleisli
category SetT . Then∏Aif ((fi (-))i∈A ): i∈A (DB X→ DB XY )Y
is bisimilar to

⨿
lift(

i∈A

⨿

fi )(f ): (DB X
Y )i∈A Ai→ DB XY ,via the isomorphism∏⨿
X Ai ∼i∈A Ai .
= (DB XY )i∈A (DB Y )(See Appendix C for the detail why generality is not lost.)
Then, (Pcnt )|fin is equal to Pfin , hence we do not need Pcnt
Pfin
for λFGanymore. On the other hand, CList|fin (S) consists ofcountable lists l such that the number of elements in S which occur
in one l are finite. For example, [0, 1, 0, 1, ...] ∈ CList|fin (N),but [0, 1, 2, 3, ...] ∈/ CList|fin (N), Thus CList|fin is far different
from List; we can not avoid the use of the notion of countablelinear ordered set. (However the authors do not know if for arbitrary
countable linear ordered set L there is an finite List-graph G whose
ε-elimination involves L; though we found such G as infinite Listgraphs as in Appendix A. As in Figure 6, it is certain that a densecountable linear ordered set (and more countable linear ordered setsconcatenated further) occur.)
For the other two examples,

Hence, if T is further a finitary monad with a family of signaturesets Σ, the graph constructor f of any f ∈ T (A) is a compositionof the graph constructors of a finite number of some signatures inΣ.
At the same time, when we add graph constructors of all the signatures in one family of signature sets to a calculus, then expressive
power on graph constructors are the same independently from thechoice of families of signature sets.
Proof. For Gii′ = (Vii′ , Bii′ , Iii′ ) (i ∈ A, i′ ∈ Ai ),f ((fi ((Gii′ )i′ ))i ).V = X+Σi∈A (X+Σi′ ∈Ai Vii′ )
and

⨿
lift(

i∈A

Remark on Representability of Monads(Mcnt )|fin (S) = {ϕ: S→N∪{∞} | ϕ−1 (N−{0}) is finite},fi )(f )((Gii′ )(i,i′ ) ).V = X+Σ(i,i′ )∈⨿i∈A Ai Vii′ .
10and (SubD cnt )|fin is the finite subprobability distribution monad
SubD fin :

&z1

&z2

0

1

a d
e(a, ) :SubD fin (S) = {ϕ: S→[0, 1] | ϕ−1 ((0, 1]) is finite, Σx ϕ(x) ≤ 1}.
def

&z1

4.2

&z2

0

1

b
e(b, ) :

c

2

3

&z1

&z2

2

Here (Mcnt )|fin and (SubD cnt )|fin are representable in a language
for implementing λTFG in a similar way to that after Example 14,
while it seems difficult to represent whole of CList|fin , because of
the notion of countable linear ordered set.
Note the difference between being finitary and being “representable”, and also note the difference between being “representable” of T and that of T ′ . (On the other hand, recall that as
above if T is finitary then T ′ can be finitary.) As above, it is notclear that being finitary of a monad implies that the monad is“representable” in a language; and being finitary of T is used toprove the property that every term in λTFG preserves finiteness (ofnodes) of graphs, while “representability” of T is needed for syntax of graph constructors and implementation of the graph model
B : V → T (Lϵ ×V +Y ). On the other hand, “representability” ofT ′ is needed for representation of graphs without ε-edges, which
is important if, in an application, graphs observable from users of
λTFG should be ε-edge free; in order to resolve this problem, wegave the effective procedure in Section 3.2 for the case of List with
CList.

&z1

&z2

&

0

b

2

a

(&z1,&) (&z2,&)srec(e)7−→

1 &y&z1,0 &z2,0

...

...

&x (input marker)&x&z1,2 &z2,2b,0b,1 (&z1,&y) (&z2,&y) a,0

c

a d

b,2

b,3

a,2

b

a,1

(output marker)&z1,1 &z2,1

Figure 7. Bulk Semantics of Structural Recursion

g: Z×(Lϵ ×V +Y ) →()
Lϵ × (Z×V ) + (Σ(l,v′ ) e(l, G|v′ ).V) + (Z×Y )



(
)

 (&z, Edge l, v ′ ) 7→


(


′ )


(if
l
=
ε
)
Edge
ε,
Hub(&z,
v
)


)
(


(if l ̸= ε ) Edge ε, Bulk(l,v′ )((e(l, G|v′ ).I)(&z)) (&z, Outm (&y)) 7→ (Outm ((&z, &y)) )Bulk(l,v′ ) (u) 7→ T (h) (e(l, G|v′ ).B)(u) h: L ×(e(l, G| ′ ).V)+Z →
ϵ
v
)
(

Lϵ × (Z×V ) + (Σ(l,v′ ) e(l, G|v′ ).V) + (Z×Y )

( ′ ′)()
 Edge l , u
7→ Edge l′ , Bulk(l,v′ ) (u′ )()
Outm (&z)
7→ Edge ε, Hub(&z, v ′ )• I ′ : Z×X → (Z×V ) + (Σ(l,v′ ) e(l, G|v′ ).V)(&z , &x ) 7→ Hub(&z , I(&x ))Structural Recursion

Now we give a general definition of the structural recursion, whichis the most important transformation method of λTFG . In [Buneman
et al. 2000], there are two semantics for the structural recursion:
bulk semantics and memoized recursive semantics. Here we generalize the bulk semantics.
A picture of the bulk semantics for ordered graphs is given
in Figure 7. As seen in the picture, with bulk semantics first we
calculate the application of a given input function f to a pair ofeach edge and its following subgraph of an input graph. Then weconnect the results in keeping with the shape of the original graph,using ε-edges.
Recall the record notation G = (G.V, G.B, G.I), which is usedin the following.

Next we see how structural recursion preserves finiteness ofgraphs.

Definition 20 (Bulk Semantics of Structural Recursion). Let T bea monad on Set. For a function e: L×DB Y → DB Z
Z , a structural
Z×X
recursion function srec(e): DB X
Y → DB Z×Y is defined as thefollowing.
def
′
′
′
For G = (V, B, I) ∈ DB X
Y , srec(e)(G) = (V , B , I ) ∈Z×X
DB Z×Y where

Proposition 21. Let T be a finitary monad. Structural recursion
function maps finite graphs to finite graphs; more precisely, fore: L×DB f Y → DB f Z
Z and a finite T -graph G, the accessible partof srec(e)(G) is finite.
Proof. Since T is finitary, for each element v ∈ V , there is a finite
subset Ev ⊆ Lϵ ×V such that B(v) ∈ T (Ev +Y ). Let
def ∪E = ( v∈V Ev ) ∩ (L×V ) ⊆ L×V,

• V ′ = (Z×V ) + (Σ(l,v′ )∈L×V e(l, G|v′ ).V)
def

(Here, an element (&z , v) in the left set Z×V —Z-copy ofnodes of G—is a “hub” of the new graph, for this case weuse the label Hub(&z , v) below. While, on the right of “+”and further in the case of (l, v ′ ) of the direct sum “Σ”, a nodeu in e(l, G|v′ ).V is “a piece of bulk”; each l-labeled edge tov ′ in G is replaced with this subgraph e(l, G|v′ ).V, which isrepresented by a dotted box in Figure 7. For this case, we use
the label Bulk(l,v′ ) (u). )• B ′ : (Z×V ) + (Σ(l,v′ ) e(l, G|v′ ).V) →()()
T Lϵ × (Z×V ) + (Σ(l,v′ ) e(l, G|v′ ).V) + (Z×Y )()
Hub(&z, v) 7→ T (g) lift(λx.(&z , x))(B(v))

then since V is finite, so is E, and B is decomposed throughT (E+Y ) ⊆ T (Lϵ ×V +Y ). Then the accessible part of srec(e)(G)is included in the finite set
V ′′ = (Z×V ) + (Σ(l,v′ )∈E e(l, G|v′ ).V) ⊆ V ′ ,defi.e., I ′ (Z×X) ⊆ V ′′ and B ′ (V ′′ ) ⊆ V ′′ .
Now recall the notion of bisimilarity for higher order functions.
The following is stronger result than that proved in [Buneman et al.
2000] even when T = Pfin , because here bisimulation genericity isproved also on the first argument e, while in [Buneman et al. 2000]11

it is proved only on the second argument G. This is the key why wePfin
can extend from UnCAL to the higher order calculus λFG.

&

Theorem 22. Let T be a finitary monad having an extension for εelimination T ′ . Structural recursion srec is bisimulation generic,i.e., ifa1 a2 … anba a … an

… 1 2[(a1, 1 ), (a2, 2 ), …, (an,a1 a2 … an&
1 2 … n

7→
&

b

2

]

)

]

7→

)

1 2 … nswap-hd-tl

Proof. Basically the proof is similar to that of Proposition 18 but a
bit subtle, because ε-elim embed T DB f into T ′ DB , while higher
order function types make inclusion relations between types opposite. So, first we show that the structural recursion is defined “uniform” on size of graphs: i.e., let[(a n ,

ba1 a2 … an&
1 2 … n&&), (a2,

2), …, (a1,

1

7→

uf -1

′
X
i = (ι-DB X
Y )|T DB f X : T DB f Y → T DB Y ,
X

def







uf -1 )7→

Z×X.
srec(e1 )(G1 ) ∼ srec(e2 )(G2 ) ∈ T DB f Z×Y

a1 a2 … an

(

&

then



1

uf

T DB f X
Y ,

∼

2 … n

1

e1 ∼ e2 : L×T DB f Y → T DB f Z
Z , andG1 ∼ G2 ∈







b

&

&

Y

then foran a2 … a1

e: L×T DB f Y → T DB f Z
Z,be′ : L×T ′ DB Y → T ′ DB Z ,Z

a1 a2 …an
1 2 … nG ∈ T DB f X
Y ,′if e ◦ (L×i) = i ◦ e then…
2

1

Figure 8. l-sbl(swap-hd-tl) (= uf -1 ◦ swap-hd-tl ◦ uf )′srecT (e′ )(i(G)) = i(srecT (e)(G)).

The two functions l-sbl(f ) and u-sbl(f ) can be applied only
to graphs without ε-edge. Hence we take ε-elimination of G before
evaluating l-sbl(f )(G) or u-sbl(f )(G). For T such that its extension T ′ is not presentable in a programming language (such as
List with CList), we check if the ε-elimination of a given graphresults in a T -graph—by the procedure in Section 3.2 for orderedgraphs—and if it is impossible, put an error. If T ′ is presentable ina language such as multiset, then we consider the T ′ as an instanceof T in the following. Thus below we consider a finitary monad
T and T -graphs without ε-edges. (In Example 23, we see why weavoid ε-edges.)

This reduces the setting of the theorem to the case when ι: T →T ′ is the identity and also the case of infinite graph (T DB rather
than T DB f ), because for any
e1 ∼ e2 : L×T DB f Y → T DB f Z
Z,
there aree′1 ∼ e′2 : L×T ′ DB Y′
such that ei ◦ (L×i) = i ◦ ei .

→ T ′ DB Z
Z

Now, in this reduced setting, we can prove commutativity ofsrec with ε-elim:

4.3.1

ε-elimZ×V (ε-elimΣ(l,v′ ) e(l,G|v′ ).V (srec(e)(G)))∼ssrec(ε-elim ◦ e)(ε-elim(G)).
εε

Local Sibling Transformation

Local sibling transformationl-sbl(f ): DB f Y → DB f Y

aHere, while ε-elim eliminates ε-edges in v0 → v1 ... → vn → ua
and adds v0 → u, ε-elimW does so only if v0 , ..., vn are in W .
Then it is sufficient in order to conclude the proof to prove thatif
e1 ∼s e2 : L×T DB Y → T DB Z
Z , andforf : T (L×DB f Y +Y ) → T (L×DB f Y +Y )manipulates branches of the root node of an input graph in sibling
direction. Before apply l-sbl, we take 1-step unfolding of the input
graph, which we now define, so we do not have to mind cycles
which the root might belong to.
We define the 1-step unfolding

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

uf : DB f Y → T (L×DB f Y +Y ),We can define a needed bisimulation relation just as we defined theset of nodes of srec(e)(G) in the bulk semantics.

where note that L has no ε since we consider graph having no εedges. First, for a graph G = (V, B, I) ∈ DB X
Y , and a node v ∈ V ,we define

4.3

G|v = (V, B, {& 7→ v}) ∈ DB Y .
Now for G = (V, B, I) ∈ DB f Y ,Sibling Transformationdef

So far we generalized all of UnCAL, parameterizing with monads.
However, when we take a monad other than powerset monad, say,the list monad for ordered graph, we need more expressive power
than what we got so far: i.e., graph transformations on sibling
dimension.
Here we introduce two term constructors for sibling transformation: first local sibling transformation l-sbl(f ) and then uniform
sibling transformation u-sbl(f ).

def

uf (G) = T (L×f +Y )(B(I(&)))
def

where f = G|(-) : V → DB f Y . A picture of uf can be seen in
Figure 8.
This coalgebra uf is called final locally finite coalgebra, and by
the results [Adámek et al. 2006, Theorem 3.3] with [Milius 2010,12

Corollary III.15], we can show that for any finitary monad T , thisuf is isomorphic up to bisimilarity and bisimulation generic. For
example, when T = List,
uf

-1

&

&
h

a b c d= foldr(++, []) ◦ List([⟨- : -⟩, ⟨-⟩]).

See Appendix D for the detail of uf -1 .
Then l-sbl is defined as below: for

e f g

h
հ

d b c af g e

f : T (L×DB f Y +Y ) → T (L×DB f Y +Y )and G ∈ DB f Y ,Figure 9. u-sbl(swap-hd-tl)
def-1

l-sbl(f )(G) = (uf ) (f (uf (G))).
The naturality of ϕ implies that u-sbl(ϕ) is bisimulation generic.
In the language λTFG , the naturality is realized by parametricity.
The term

A picture of an example of local sibling transformation is given
in Figure 8, where swap-hd-tl is the list function which swaps thehead and tail and maps nil to nil.
Since we take ε-elimination of G before applying l-sbl(f ) toG, and since uf is bisimulation generic, it is obvious that l-sbl
is (higher order) bisimulation generic. On the other hand, if we
apply l-sbl(f ) to G having ε-edges, bisimulation genericity does
not necessarily hold:

λx.e: T (Label×α+Y ) → T (Label×α+Y )in u-sbl(λx.e) should be written as a parametric term. Then theinterpretation of λx.e becomes a natural transformation, by the freetheorem.
Functions u-sbl(ϕ) are used for transforming (a list of)branches for each node. For example, using the list reverse function
reverse, the transformation u-sbl(reverse) reverses the ordersof branches for all nodes in an input graph.
The introduction of u-sbl also enhances the expressive powerof structural recursion. The structural recursion law

def

Example 23. Let us consider car defined as car([]) = [] andcar(a :: as) = [a]. Then if we apply l-sbl(car) to the twobisimilar graphs below left, then the results below right are notbisimilar.
06
1



66a
6

2

0
∼

a

l-sbl(car)
7→

2

0



1

0
∼
/

f (G ++ G′ ) = f (G) ++ f (G′ )awith f = srec(e) is too restrictive in the sense that the function
f cannot change the order of branches of any nodes. Under thisrestriction, we cannot write a transformation f which satisfies

2

We remark that, when taking ε-elimination of G before theapplication l-sbl(f )(G), it is enough to eliminate only ε-edges
from the root node of G—by which all branches of the root node
become non-ε edges or output markers—rather than the full εelimination.

f (G ++ G′ ) = f (G′ ) ++ f (G).
To circumvent the restriction, we can use the u-sbl construct
to rearrange the order of branches during structural recursion; for example, we can write the transformation above bysrec(e)(u-sbl(reverse)(G)).
The counterexample in Example 23 is also a counterexample
for the fact that if we apply u-sbl(ϕ) to graphs having ε-edges
then u-sbl(ϕ) is not necessarily bisimulation generic.
If ϕ: T (-) → T (-) is not just a natural transformation but alsoa monad morphism such that the lifted endofunctor Fϕ

Example 24. One can also transform branches of any nodes in an
input graph, by the combination of l-sbl with traversing the input
graph by the structural recursion, or by multiple use of l-sbl. For
example, the following apply transformation e to branches of allnodes pointed by a-labeled edges.
apply lct a(e)(db) = srec( λ(l, g). if l = a

Fϕ : SetT → SetT

then ⟨l : l-sbl(e)(g)⟩ @ () else ⟨l : ⟨&⟩⟩)(db)(f : S → T (S ′ )) 7→ (ϕS ′ ◦ f : S → T (S ′ ))The following applies a transformation l-sbl(e) to branches of thefirst branch of the root.

preserves a given iteration operator, then we do not need to calculate ε-elimination before application of u-sbl. For example, thereverse operator reverse is such ϕ. We can add such non εeliminating uniform sibling transformation u-sbl′ (ϕ) for ϕ satisfying the above condition, whose proof are subject to users. Or an
implementer can add u-sbl′ (ϕ) as primitive functions, after proving the condition for ϕ.

apply lct first branch(e)(db) = l-sbl( λbs.cons(
case car(bs) of Edge(l, g)→ Edge(l, l-sbl(e)(g))
or y
→ y,
cdr(bs)) )(db)

4.4 Syntax of λTFG
4.3.2

Finally let us see how to define the syntax of λTFG for general T ,modifying that of λList
FG , i.e., Figures 4 and 5 in Section 2.2.3.
First we choose a convenient family of signature sets Σ =(Σ(n))n∈N of T , and we replace algebraic graph constructors []and e ++ e with constants ops (s ∈ Σ), then we give the following
typing rules.

Uniform Sibling Transformation

While l-sbl(f ) transforms branches only of one node (root node),
u-sbl(f ) transform branches uniformly of all nodes in a given
graph, as in Figure 9.
Let us see the definition. Let
ϕ: T (L×(-)+Y ) → T (L×(-)+Y )Γ ⊢ ei : DBX(i ∈ n)Y(s ∈ Σ(n))Γ ⊢ ops (e1 , ..., en ): DBX
Y

be a natural transformation. For a T -graph G = (V, B, I) ∈DB f XY ,Also we replace the type constructor List with that of the current monad T . Then we replace list operators with any convenientdef

u-sbl(ϕ)(G) = (V, ϕV ◦B, I).
13

(e)

1

(a)

a

d
d

2

b

3

c
(b)

1

srec(rc, foldr(++,[]))

d

d

4
&y

2

d

3

d

5

b

d
(c)

1

(d)

1

4
&y

1

&

2

[1,2],1[1,4],1[1,2],1[1,4],1

d

d

d

d

[1,2],2[1,4],2[1,2],2[1,4],2

&

&

(1,&)

(2,&)

[3,2],1[3,2],1dd[3,2],2

3[4,3],1

b

&

4
&y

2

[3,2],2

&

3

4

(1,&)
[4,3],1[2,3],2

&

(1,&)

d
[1,4],2

2

d

3

4

[3,2],2[2,3],1[2,3],2d[1,2],2[3,2],1[4,3],2[2,3],1[1,4],1[1,2],1b(2,&y)[4,3],1&y[2,3],1b[4,3],2(1,&)[4,3],2[2,3],2Figure 10. Bulk Semantics of Structural Recursion: An Example of srec(rc, foldr(++, []))
operators on the monad T ; according to adding operators on T ,l-sbl and u-sbl become more powerful.

5.

operator to list operator; for a binary operator (with unit) we canconstruct a list operator by foldr (or foldl), where we do not need torequire them to be a monoid. We explain production-consumption
compatibility after giving bulk semantics of this srec.
Before giving the formal definition of bulk semantics ofsrec(e, d), we illustrate the bulk computation behavior usingdef
a2d xc = srec(rc, foldr(++, [])) (see Example 4 for rc). It consists of two steps of bulk computations followed by a grouping
step, starting with the input graph (a) in Figure 10.

Structural Recursion with Sibling
Transformation

In Section 4.3, we gave two kinds of sibling transformations. Here
we show one attempt to extend the structural recursion so that by
it we can transform graphs both in depth-direction and in siblingdirection at the same time. In this section we concentrate on thecase when T = List.
First we show our idea briefly. The original structural recursion
function f = srec(e) is characterized with the following equations:

1. Applying Map Computation on Edges with e
Apply function rc (which renames edges labeled a to thoselabeled d and contracts edges labeled c) to every edge labeledl and the graph g following to the edge, and yields a graph in
DB Z
Z . We call these graphs computed by e(= rc) e-graphs;
graph (b) shows e-graphs.

f (⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩)= e(l1 , g1 ) @ f (g1 ) ++ ... ++ e(ln , gn ) @ f (gn )2. Applying Map Computation on Nodes with d
For every node of the original graph, use binary operator ++ tocombine all branching e-graphs. We call these graphs computedby d(= foldr(++, [])) d-graphs; graph (c) shows the result.
The nodes 1 and 4 have more than one branches which need tobe merged using ++.
Before applying d = foldr(++, []) on a node of the originalgraph, for each ith branch of the node, we add the index i tothe output markers of the ith e-graph, which will be used in thenext “grouping” step.

We generalize above ++ with arbitrary operators ⊙ satisfying
certain axioms, i.e., as the following
f (⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩)= e(l1 , g1 ) @ f (g1 ) ⊙ ... ⊙ e(ln , gn ) @ f (gn )so that we can transform graphs in sibling direction with ⊙.
Now let us see the typing rule for the extended structural recursion function:Γ ⊢ e1 : Label×DBY → DBZ
ZZΓ ⊢ e2 : List(DBZα ) → DBαe1 and e2 are production-consumption compatible

3. Grouping Subgraphs with ε-Edges
Group all d-graphs computed in Step 2: for each d-graph, its
output marker produced by e with an index i is connected via anε-edge to the root of the d-graph on the node which the original
ith edge points to. We do not need anymore the original nodes,
and also delete indices i of the remaining output markers (e.g.,
2 of (2, &y) in the graph (c)). The root of new graph is the rootZ×X
Γ ⊢ srec(e1 , e2 ): DBX
Y → DBZ×Y

In the typing rule, e2 is a parametric polymorphic term on
the sets of output markers. We generalize ⊙ above from binary14• Gi = ⊕&z∈Z &z := ⟨(&z , &y)⟩ for some &y ∈ Y , Zi = Zi′ =of the d-graph on the original root node. With these, we can get
Graph (d) from Graph (c).
Graph (e) is the graph obtained by ε-elimination for Graph (d).
(We can further minimize Graph (e) if necessary; then nodes
2, 3, 5 are identified, since they are bisimilar.) We remark adifference between the two bulk semantics: the result graph (e)defof a2d xc = srec(rc, foldr(++, [])) is not isomorphic to thedefresult graph (c) in Figure 2 of a2d xc = srec(rc); but on theother hand, in general srec(e) and srec(e, foldr(++, [])) arebisimilar.

Z×Y , and G′i = ⌊id ⌋.

Then the following must be satisfiedd((G1 @ G′1 @ ⌊in 1 ⌋), ..., (Gn @ G′n @ ⌊in n ⌋))= d(G1 @ ⌊in 1 ⌋, ..., Gn @ ⌊in n ⌋) @ (G′1 +...+G′n )()∈ DB Z′Z1′ +...+Zn
Z1 +Z2where G′1 +G′2 = (G′1 @ ⌊in 1 ⌋) ⊕ (G′2 @ ⌊in 2 ⌋) ∈ DB Z
′
′.
1 +Z2
This condition means that d “consumes” only the informationof the graphs “produced” by e.
By this assumption, we can show that the bulk semantics agrees
with the recursive semantics: i.e., the structural recursion function
f = srec(e, d) in Definition 25 satisfies (and is characterized by)
the following equationdef

Now let us give a formal definition of bulk semantics of thestructural recursion. For a function f : X → Y , we define markerdef
renaming graph ⌊f ⌋ = ⊕&x∈X &x := ⟨f (&x )⟩ ∈ DB XY .
ZDefinition 25. For e: L × DB Y → DB Z
Z , d: List(DB α ) →
X
DB Z
,
and
G
=
(V,
B,
I)
∈
DB
,
α
Y

f (⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩)= d(e(l1 , g1 ) @ f (g1 ), ..., e(ln , gn ) @ f (gn )).

srec(e, d)(G) = (V ′ , B ′ , I ′ ) ∈ DB Z×X
Z×Y
def

is defined as below.
We assume G has no ε-edges since we can take ε-elimination;if ε-elim(G) has infinite width, we put an error.
We first extend e to the following dependent type function

If d = foldr(⊙, ι⊙ ) for some ⊙ and ι⊙ , then the following
characterizing equations are also availablef ([])
f (⟨l1 : g1 ⟩ ++ g)ē: L×V + Y → DB Z
Zx
x = Edge (l, v) 7→ e(l, G|v ) (Zx = Z)
x = Outm (&y) 7→ ⊕&z∈Z &z := ⟨(&z, &y)⟩ (Zx = Z×Y ),l = (li )i∈n 7→ (ē(li ) @ ⌊in i ⌋)i∈n (Wl =f ([])
f (⟨l : g⟩)f (g1 ++ g2 )⨿i∈n Zli ).

Next, for each v ∈ V , we define d-graph on v asι⊙e(l, g) @ f (g)f (g1 ) ⊙ f (g2 ).

Z×X
srec(e, d): DB X
Y → DB Z×Y(if B(v).i is an edge)(if B(v).i is an output marker).

is bisimilar to the singleton case to the Xth power

Then,

X
srec(e, d)X : (DB Y )X → (DB Z
Z×Y )

def ⨿
• V ′ = v∈V dv .V• B′ :===

Above we considered the case when X is a singleton and omitted the case when a branch might be an output marker &y; for thegeneral case, first note thatdef⨿ndv = d(eList (B(v))) ∈ DB Z,
i=1 Ziwhere n = |B(v)| and
{
Z
Zi =
Z×Y

ι⊙
(e(l1 , g1 ) @ f (g1 )) ⊙ f (g).

Further, if (⊙, ι⊙ ) is a monoid, then we obtain also the following
simpler characterizing equations

and then to the following dependent type function
eList : List(L×V + Y ) → List(DB Z
Wl )

=
=

with the isomorphisms)(⨿
v dv .V → List L×( v dv .V) + Z×Y⨿

X⊕: (DB Y )X ∼= DB Y ,(v, u) 7→ List(g)( (dv .B)(u) )()⨿(dv .B)(u) ∈ List L×(dv .V) + n
i=1 Zi⨿⨿ g: L×(dv .V) + n
i=1 Zi → L×( v dv .V) + Z×Y


(
)
(
)
′
′


Edge l, u
7→ Edge l, (v, u )( ′) 



Outm
((i,
&z))
→
7
let
B(v).i
=
Edge
l,
v
in

( ( ′
)) 


Edge ε, v , (dv′ .I)(&z) Outm ((i, (&z, &y))) 7→ Outm ((&z, &y))⨿
• I ′ : Z×X → v dv .V()(&z , &x ) 7→ I(&x ), (dI(&x) .I)(&z )Z×XX ∼⊕: (DB Z= DB Z×Y ,Z×Y )hence the case of general X is reduced to the case when X is asingleton. On the matter that a branch might be an output marker,
we replacee(l, g) @ f (g)for ⟨l : g⟩⊕&z∈Z &z := ⟨(&z, &y)⟩for ⟨&y⟩.

with

For example, the above second characterizing equations when d =foldr(⊙, ι⊙ ) becomes

Now we explain the assumption in the above typing rule. Terms
e1 and e2 are called production-consumption compatible if theinterpretations e = [[e1 ]] and d = [[e2 ]] satisfy the following. Let
Zi′
Gi ∈ DB Z
Zi , Gi ∈ DB Z ′ (i = 1, ..., n) be graphs such that forieach i, eitherf ([])
f (⟨l1 : g1 ⟩ ++ g)f (⟨&y⟩ ++ g)

=
=
=

ι⊙
(e(l1 , g1 ) @ f (g1 )) ⊙ f (g)⊕&z∈Z &z := ⟨(&z , &y)⟩ ⊙ f (g).

Example 26. The following left a path cut down the left sideof the leftmost path consisting only of a-labeled edges, as in Fig-

• Gi is an application of e and so Zi = Z, or

15

&

(
= if l1 = a(then (⟨&⟩ @ e(l1 , g1 ) @ ⌊in 1 ⌋)++&bc a b ad a bbհ(⟨&z⟩ @ e(l2 , g2 ) @ ⌊in 2 ⌋)

a b a

)

(
(⟨&z⟩ @ e(l1 , g1 ) @ ⌊in 1 ⌋)++

⊕ &z:=)(⟨&z⟩ @ e(l2 , g2 ) @ ⌊in 2 ⌋)()
else ⟨&⟩ @ e(l2 , g2 ) @ ⌊in 2 ⌋ ⊕ &z:=((⟨&z⟩ @ e(l1 , g1 ) @ ⌊in 1 ⌋)++)(⟨&z⟩ @ e(l2 , g2 ) @ ⌊in 2 ⌋))@ (g1′ + g2′ )a bcFigure 11. left a path= (∗).
The &z -root graph of f (g) is the original graph g; in fact, by therecursive semantics, we can check that ⟨&z ⟩ @ f (g) @ ⌊pr r ⌋ = g
as below:⟨&z⟩ @ f ([]) = ⟨&z⟩ @ i = [],ure 11. We explain the detail after the definition.
left a path : DBY → DBY
left a path(g) = ⟨&⟩ @ f (g) @ ⌊pr r ⌋ (pr r : {&, &z }×Y → Y )where{&,&z}
f : DBY → DB{&,&z}×Y
f = srec(e, foldr(o, i)){&,&z}
e: Label×DBY → DB{&,&z}e(l, g) = ⟨l : ⟨&⟩⟩ ⊕ &z := ⟨l : ⟨&z ⟩⟩is a under root of : DBY → Boolis a under root of (g) = not(isEmpty(
srec(λ(l, g). if l = a then ⟨a : []⟩ else [])(g) )){&,&z}{&,&z}{&,&z}
o: DBα×DBα→ DBαo(g1 , g2 ) = if is a under root of (⟨&z ⟩ @ g1 )then ((⟨&⟩ @ g1 ) ++ (⟨&z ⟩ @ g2 )) ⊕&z := ((⟨&z ⟩ @ g1 ) ++ (⟨&z ⟩ @ g2 ))else (⟨&⟩ @ g2 ) ⊕ &z := ((⟨&z ⟩ @ g1 ) ++ (⟨&z ⟩ @ g2 )){&,&z}
i: DBαi = [] ⊕ &z := []⟨&z⟩ @ f (⟨l1 : g1 ⟩ ++ g)= ⟨&z⟩ @ o(e(l1 , g1 ) @ f (g1 ), f (g))= if is a under root of (⟨&z⟩ @ e(l1 , g1 ) @ f (g1 ))then ⟨&z⟩ @ e(l1 , g1 ) @ f (g1 ) ++ (⟨&z⟩ @ f (g))
else ⟨&z⟩ @ e(l1 , g1 ) @ f (g1 ) ++ (⟨&z⟩ @ f (g))= ⟨&z⟩ @ e(l1 , g1 ) @ f (g1 ) ++ (⟨&z⟩ @ f (g))= ⟨l1 : (⟨&z⟩ @ f (g1 ))⟩ ++ (⟨&z⟩ @ f (g)).
(The above is paramorphism of structural recursion by tupling,
regarding multi-rootedness as tuple.)
Then let us see left a path(g), i.e., the &-root graph of f (g):⟨&⟩ @ f ([]) = ⟨&⟩ @ i = [],⟨&⟩ @ f (⟨l1 : g1 ⟩ ++ g)= ⟨&⟩ @ o(e(l1 , g1 ) @ f (g1 ), f (g))= if is a under root of (⟨&z⟩ @ e(l1 , g1 ) @ f (g1 ))First, it is easily checked that the above e and foldr(o, i) areproduction-consumption compatible. In fact,

then (⟨&⟩ @ e(l1 , g1 ) @ f (g1 )) ++ (⟨&z⟩ @ f (g))
else (⟨&⟩ @ f (g))

o(e(l1 , g1 ) @ g1′ @ ⌊in 1 ⌋, e(l2 , g2 ) @ g2′ @ ⌊in 2 ⌋)= if is a under root of (⟨l1 : (⟨&z⟩ @ f (g1 ))⟩)

= if is a under root of (⟨&z⟩ @ e(l1 , g1 ) @ g1′ @ ⌊in 1 ⌋)then ⟨l1 : (⟨&⟩ @ f (g1 ))⟩ ++ (⟨&z⟩ @ f (g))

then ... else ...

else (⟨&⟩ @ f (g))= if is a under root of (⟨l1 : (⟨&z⟩ @ g1′ @ ⌊in 1 ⌋)⟩)

= if is a under root of (⟨l1 : g1 ⟩)then ... else ...

then ⟨l1 : (⟨&⟩ @ f (g1 ))⟩ ++ g









)

′

(⟨&z⟩ @ e(l2 , g2 ) @ g2 @ ⌊in 2 ⌋)⊕ &z:= 



(

′

(⟨&z⟩ @ e(l1 , g1 ) @ g1 @ ⌊in 1 ⌋)++
)
(∗)
′

(⟨&z⟩ @ e(l2 , g2 ) @ g2 @ ⌊in 2 ⌋)


(
)



else ⟨&⟩ @ e(l2 , g2 ) @ g2′ @ ⌊in 2 ⌋ ⊕ &z:=


(


′

(⟨&z⟩ @ e(l1 , g1 ) @ g1 @ ⌊in 1 ⌋)++



)

′
(⟨&z⟩ @ e(l2 , g2 ) @ g2 @ ⌊in 2 ⌋)= if l1 = a(then (⟨&⟩ @ e(l1 , g1 ) @ g1′ @ ⌊in 1 ⌋)++

else (⟨&⟩ @ f (g)).
Now it is clear that the function left a path(= ⟨&⟩ @ f (-))
works as in Figure 11.
By the bulk semantics, it is clear that the above structural recursion function preserves finiteness of graphs. Also, similarly to
Theorem 22, we can show that the above structural recursion isbisimulation generic.
Comparison of Sibling Transformations
The structural recursion extended above is similar to the combination of u-sbl and the original structural recursion in Section 4.2. indeffact, when e: L×DB Y → DB {&} is “identity” i(l, g) = ⟨l : g⟩,srec(i, d) is similar to u-sbl(f ), though here d and f have a bit
different types. The main difference between the extended structural recursion and the combination of u-sbl and the original structural recursion is the following. In general, srec(e, d) transforms

and on the other hand,o(e(l1 , g1 ) @ ⌊in 1 ⌋, e(l2 , g2 ) @ ⌊in 2 ⌋) @ (g1′ + g2′ )
= ...

16

graphs in sibling direction by traversing graphs produced by e. Thissibling transformation can not be simulated by u-sbl(f ) used after
the original srec; in the latter f traverses just one step of children,
while in the former d can traverse more deep descendants as longas production-consumption compatibility holds.
The extended structural recursion includes also the feature of
l-sbl in the following sense. Let

In the following, as a demonstration of our modular approach,
we take up one simple binary monad transformer—the productT ×T ′
T ×T ′ of monads—, and see the language λFG.
6.1 Product of Monads
For a pair of monads T1 and T2 on Set, we define their productT1 ×T2 just as

f : List(Label×DB0 +0) → List(Label×DB0 +0)

def(T1 ×T2 )(X) = T1 (X)×T2 (X)be a function such that there isfor a set X andf ′ : List(DB{α&,&z} ) → DBαdef(T1 ×T2 )(f ) = T1 (f )×T2 (f )satisfying

for a function f . Then⟩def ⟨return T1 ×T2 = return T1 , return T2 : X → (T1 ×T2 )(X),f ′ ◦ List(pair ) = uf -1 ◦ f()= foldr(++, []) ◦ List([⟨- : -⟩, ⟨-⟩]) ◦ f

and for f : X → T1 (Y )×T2 (Y ),where{&,&z}

pair : Label×DB0 → DB0

lift T1 ×T2 (f ) = lift T1 (pr l ◦ f ) × lift T2 (pr r ◦ f ).
def

def

pair (l, g) = ⟨l : []⟩ ⊕ &z := g.
Then l-sbl(f ) can be represented by srec as the following:

From now we check that taking the product of monads preserves
the above three assumptions.
It is easy to check that if two monads T1 and T2 have uniform
iteration operators in their Kleisli categories, so does the productT1 ×T2 : for f : X → T1 (X+Y )×T2 (X+Y ),l-sbl(f ) = ⟨&⟩ @ srec(e, d)where{&,&z}

e: Label×DB0 → DB{&,&z}iter T1 ×T2 (f ) =⟨⟩iter T1 (pr l ◦ f ), iter T2 (pr r ◦ f ) : X → T1 (Y )×T2 (Y ).
def

def

e(l, g) = ⟨l : []⟩ ⊕ &z := (g @ ⌊!⌋) (!: 0 → {&, &z})
d: List(DB{α&,&z} ) → DB{α&,&z}= d(pair (l1 , g1 ), ..., pair (ln , gn ))If monads T1 and T2 preserve weak pullbacks, so does T1 ×T2 ,since the product functor × preserve them.
Also it is clear on finitarity since the product functor is finitary,
but let us see concretely what family of signature sets for the product monad T1 ×T2 we can get from families of signature sets for T1
and T2 since it is needed to define syntax and for implementation.
Let Σ1 and Σ2 be families of signature sets for T1 and T2 ,respectively. Then (Σ1 ⊗Σ2 )(n) is defined as the following:

hence,{(f1 , f2 ) ∈ T1 (n)×T2 (n) | m1 , m2 ∈ N, n= max(m1 , m2 ),d(l) = f ′ (l) ⊕ &z := [] .
def(Here again we used tupling technique for srec:) This is because,srec(e, d)(⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩)= d(e(l1 , g1 ) @ srec(e, d)(g1 ), ..., e(ln , gn ) @ srec(e, d)(gn ))f1 ∈ Σ1 (m1 )(⊆ T1 (m1 ) ⊆ T1 (n)),⟨&⟩ @ srec(e, d)(⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩)f2 ∈ Σ2 (m2 )(⊆ T2 (m2 ) ⊆ T2 (n)) }= f ′ (pair (l1 , g1 ), ..., pair (ln , gn ))+ {(f1 , return(n−1)) ∈ T1 (n)×T2 (n) |= (f ′ ◦ List(pair ))((l1 , g1 ), ..., (ln , gn ))n > 0, f1 ∈ Σ1 (n−1)(⊆ T1 (n−1))}= (uf -1 ◦ f )(uf (⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩))+ {(return(n−1), f2 ) ∈ T1 (n)×T2 (n) |= l-sbl(f )(⟨l1 : g1 ⟩ ++ ... ++ ⟨ln : gn ⟩).

6.

n > 0, f2 ∈ Σ2 (n−1)(⊆ T2 (n−1))}+ {(0, 1) ∈ T1 (n)×T2 (n) | n = 2 }Modularized Extension of UnCAL

where recall that we regard a natural number n as the set{0, ..., n−1}. Then one can check that this Σ1 ⊗Σ2 becomes afamily of signature sets for T1 ×T2 by induction.

In Section 4, we saw how we can generalize (and extend) UnCAL
to obtain λTFG with monads T which satisfy certain assumptions:
i.e.,

Example 27. Let us consider the case when T1 = Pfin andT2 = List.
Now we have two signatures {} and {0, 1}—which correspond to the syntax {} and ∪, respectively—for Pfin , and also
two signatures [] and [0, 1]—which correspond to the syntax[] and ++, respectively—for List, hence we should have nine(= 2×2+2+2+1) signatures for Pfin ×List. However some ofthem can be represented as compositions of the other ones andcommon graph constructors, then after all signatures we needfor Pfin ×List are: ({}, []) (nullary), ({0, 1}, [0, 1]) (binary),({}, return(0)) (unary), and (return(0), []) (unary).
Let the syntax corresponding to these four signatures be• T has an extension for ε-elimination,• T preserves weak-pullbacks, and• T is a finitary monad.

Also we saw four examples of such monads: Pfin , List, Mfin , andDfin . Here we see how we can compose monads T to obtain λTFG .
Since monad was introduced for the notion of computational
effects [Moggi 1989], there has been much study about how tocompose monads from smaller monads: i.e., monad transformers.
In [Benton et al. 2000] many examples of unary monad transformers are listed. In [Hyland et al. 2006], the authors studied binary
monad transformers and show also how they can be used to produce unary monad transformers such as those in the former paper.

({}, []) | e(∪, ++)e | del-unorder(e) | del-order(e)17and replace the part {algebraic graph operators} of syntax of λList
FGin Figure 4 with these four. Also replace all the occurrences of type
List(...) with Set(...)×List(...) both in the BNF type definitionof λList
FG and in the typing rules. The resulting syntax is the core
Pfin ×List
syntax of λFG.
The nullary operator ({}, []) produces single node graph withno branches. The binary operator (∪, ++) takes union of unorderedbranches of the roots of the two argument graphs, and at the sametime, takes append of ordered branches of the roots of the twoargument graphs. The unary operator del-unorder(e) deletes allunordered branches only of the roots of an argument graph, soe.g. unordered branches of ordered branches of the root remain.
Similarly, the unary operator del-unorder(e) deletes all orderedbranches only of the roots of an argument graph.
As we can add any list operator such as foldr or filter, we canfin ×List
add any operator for Pfin ×List to the core syntax of λP.
FGFor example, we can add the function l2s which maps lists tofinite sets by forgetting the orders of lists, then we can define thetermgraphs [Erwig 2001], but that inductive view is indirect in that thegraph view is dynamically maintained.
In coalgebra theory, which studies infinitary/cyclic structure,some work focused also on finiteness of graphs, as in the current
paper.
In the work [Bonsangue et al. 2009], for every Kripke polynomial endofunctor F , a systematic way for giving a syntax fully representing all finite F -coalgebras and a sound and complete equational theory for bisimilarity was given. The differences between
this work and our work are (i) the two classes of endofunctors—
Kripke polynomial ones and ours with monads—are incomparable,(ii) the work does not treat ε-edge, and is not a study for transformation (iii) in our work the equational theory is restrictive, and (iv)the approaches to give each syntax are different.
In the work [Adámek et al. 2006; Milius 2010], the authors studied categorical properties of the set of finite coalgebras, and characterized it as the final locally finite coalgebra. The class of endofunctors for coalgebra in this work is wider than ours; some of theresults are applied or influence to our work. In this work, there isno consideration for finiteness-preserving structural recursion. The
finality among locally finite coalgebras is a kind of corecursion,and has the similar problem to that of corecursion; i.e., to assure
finiteness-preservation, we have to check locally finiteness of infinite graphs, automation of which seems difficult.
A study of general framework for bisimilarity involving ε-edge
was implicitly started in the paper [Jacobs 2010a]. They gave somesufficient condition for a monad to have an iteration operator in
the Kleisli category. However, the theory can not be applied to thecase of CList, which does not satisfy the sufficient condition. So
the current paper gave a new example of iteration operator in a
Kleisli category and of such “ε-elimination as iteration operator”
perspective.

x: Set(b)×List(b) ⊢ (π l (x) ∪ l2s(π r (x)), []): Set(b)×List(b)and apply u-sbl to this to get a function which transform allordered branches to unordered ones.

7.

Related Work

Structural recursion for graphs, which we generalized, is much
related to research on algebras of programming [Bird and de Moor
1996; Gibbons 2002; Hu et al. 2006; Meijer et al. 1991], where
structural recursion such as folds and catamorphisms are used tostructure programs and to systematically manipulate programs. In
particular, our approach is influenced by many attempts of defining
structural recursion for various kinds of specific graphs, such as
directed acyclic graphs [Gibbons 1995], graphs represented bytrees with specific pointers [Dal Zilio et al. 2004; Hamana 2009],
and graphs represented by trees with embedded functions [Fegarasand Sheard 1996]. However, all these attempts are not easy to be
applied in practice, due to lack of expressive power or difficulty inguaranteeing finite representation of well-formed graphs with nodangling pointers.
As described in the introduction, it is the structural recursion in
UnCAL [Buneman et al. 2000] that is more practical for manipulating unordered graphs. This forms the basis of our work. Our λTFG
Pfin
is parameterized with monad T , and the case T = Pfin , i.e., λFG
is comparable with UnCAL. The following is the comparison bePfin
tween UnCAL and λFG. The two graph models are equivalent up
to each bisimilarity, which for UnCAL is called value equivalencein [Buneman et al. 2000]. Also the graph constructors and structural
recursion are the same. Then we extended expressive power in two
points. One is the extension on sibling transformations: i.e., l-sbl
and u-sbl. The other is the extension of type system; UnCAL isfinfirst order calculus, while λP
FG is a simply typed lambda calculus(extended with graph types). This extension of type system is not
for free, as we noted before Theorem 22.
A lot of work has been devoted to efficient implementation ofgraph algorithms in lazy functional languages [Burton and Yang
1990; Erwig 1997; Johnsson 1998; King and Launchbury 1995].
The emphasis there is placed on the importance of achieving efficient implementation of general graph algorithms through themonadic model for including actions on the state in the non-strict
context. In contrast, we focus on inductive traversals of orderedgraphs and aim to provide an efficient way to deal with a specificclass of important graph algorithms – graph querying. Erwig showsthat active patterns can be used to implement an inductive view of

8. Conclusions and Future WorkIn this paper, we present the first solution to the open problem
of how to modify the graph model and structural recursion fromunordered graphs to ordered ones, based on which we define a
new graph transformation language λList
FG . The key technical contributions here is the definition of bisimulation relation on orderedgraphs having ε-edges. We also extend expressive power on sibling
dimension with two new operators: local sibling transformation anduniform sibling transformation.
Furthermore, we generalize these results for ordered graphswith monads with suitable assumptions, and propose a more general graph languages λTFG which are parameterized by monads T .
This abstraction by monad T enables us to compose a language targeting bigger graph model from smaller graph models by monadtransformers. We demonstrate it with the product monad transformer.
There are many interesting and important future extensions.
First, we have discussed little about analysis of structural recursion.
One interesting analysis is when a structural recursion function is
productive. A graph function is said to be productive, if it produces
a finite ordered graph without ε-edges for any input ordered graphwithout ε-edge. Second, following our previous work of bidirectionalizing UnCAL [Hidaka et al. 2010], we are very interested ina systematic way to bidirectionalize λTFG , which is indeed the first
motivation of this work.
Acknowledgments Thanks are due to Ichiro Hasuo and Naohiko
Hoshino for helpful discussions.

References
J. Adámek, S. Milius, and J. Velebil. Iterative algebras at work. Mathematical. Structures in Comp. Sci., 16(6):1085–1131, Dec. 2006.

18

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.
R. Bird and O. de Moor. Algebras of Programming. Prentice Hall, 1996.
M. Bonsangue, J. Rutten, and A. Silva. Algebras for kripke polynomial
coalgebras. In LICS, IEEE, Computer Science Press, pages 49–58, 2009.
P. Buneman, M. F. Fernandez, and D. Suciu. UnQL: a query language andalgebra for semistructured data based on structural recursion. VLDB
Journal: Very Large Data Bases, 9(1):76–110, 2000.
F. W. Burton and H.-K. Yang. Manipulating multilinked data structuresin a pure functional language. Softw. Pract. Exper., 20:1167–1185,
November 1990.
S. Dal Zilio, D. Lugiez, and C. Meyssonnier. A logic you can counton. In Proceedings of the 31st ACM SIGPLAN-SIGACT symposium on
Principles of programming languages, POPL’04, pages 135–146, New
York, NY, USA, 2004. ACM.
M. Erwig. Functional programming with graphs. In Proceedings of the second ACM SIGPLAN international conference on Functional programming, ICFP ’97, pages 52–65, New York, NY, USA, 1997. ACM.
M. Erwig. Inductive graphs and functional graph algorithms. J. Funct.
Program., 11:467–492, September 2001. ISSN 0956-7968.
L. Fegaras and T. Sheard. Revisiting catamorphisms over datatypes withembedded functions. In Proc. ACM symposium on principles of programming languages, St. Petersburg Beach, Florida, Jan. 1996.
J. Gibbons. An initial-algebra approach to directed acyclic graphs. In Mathematics of Program Construction, MPC ’95, pages 282–303, London,
UK, 1995. Springer-Verlag.
J. Gibbons. Calculating functional programs, pages 149–201. SpringerVerlag New York, Inc., New York, NY, USA, 2002.
A. Gill, J. Launchbury, and S. P. Jones. A short cut to deforestation. In
Proc. Conference on Functional Programming Languages and Computer Architecture, pages 223–232, Copenhagen, June 1993.
S. Ginali. Regular trees and the free iterative theory. J. Comput. Syst. Sci.,
18(3):228–242, 1979.
E. Haghverdi. A Categorical Approach to Linear Logic, Geometry of Proofs
and Full Completeness. PhD thesis, University of Ottawa, 2000.
M. Hamana. Initial algebra semantics for cyclic sharing structures. In Proceedings of the 9th International Conference on Typed Lambda Calculi
and Applications, TLCA ’09, pages 127–141, Berlin, Heidelberg, 2009.
Springer-Verlag.
M. Hasegawa. The uniformity principle on traced monoidal categories.
Electr. Notes Theor. Comput. Sci., 69:137–155, 2002.
I. Hasuo, 2011. personal communication.
S. Hidaka, Z. Hu, K. Inaba, H. Kato, K. Matsuda, and K. Nakano. Bidirectionalizing graph transformations. In ACM SIGPLAN International
Conference on Functional Programming, pages 205–216. ACM, 2010.
Z. Hu, T. Yokoyama, and M. Takeichi. Program optimizations and transformations in calculational form. In Summer School on Generative andTransformational Techniques in Software Engineering, pages 139–164,
Braga, Portugal, 2006. Springer, LNCS 4043.
M. Hyland, G. Plotkin, and J. Power. Combining effects: sum and tensor.
Theor. Comput. Sci., 357(1):70–99, July 2006. ISSN 0304-3975.
B. Jacobs. From coalgebraic to monoidal traces. Electronic Notes in
Theoretical Computer Science, 264(2):125 – 140, 2010a. Proceedingsof the Tenth Workshop on Coalgebraic Methods in Computer Science(CMCS 2010).
B. Jacobs. From coalgebraic to monoidal traces. Electron. Notes Theor.
Comput. Sci., 264:125–140, August 2010b. ISSN 1571-0661.
T. Johnsson. Efficient graph algorithms using lazy monolithic arrays. J.
Funct. Program., 8:323–333, July 1998.
F. Jouault and J. Bézivin. KM3: A DSL for metamodel specification.
In Formal Methods for Open Object-Based Distributed Systems, pages
171–185. LNCS 4037, Springer, 2006.
Y. Kakutani. Duality between call-by-name recursion and call-by-value
iteration. In J. C. Bradfield, editor, CSL, volume 2471 of Lecture Notes in

Computer Science, pages 506–521. Springer, 2002. ISBN 3-540-442405.
D. J. King and J. Launchbury. Structuring depth-first search algorithms inhaskell. In Proceedings of the 22nd ACM SIGPLAN-SIGACT symposiumon Principles of programming languages, POPL ’95, pages 344–354,
New York, NY, USA, 1995. ACM.
E. Meijer, M. Fokkinga, and R. Paterson. Functional programming withbananas, lenses, envelopes and barbed wire. In Proc. Conference on
Functional Programming Languages and Computer Architecture (LNCS
523), pages 124–144, Cambridge, Massachuetts, Aug. 1991.
S. Milius. A sound and complete calculus for finite stream circuits. Logicin Computer Science, Symposium on, 0:421–430, 2010.
R. Milner. Communicating and Mobile Systems: the π-calculus. Cambridge
University Press, 1999.
J. C. Mitchell. Foundations for programming languages. Foundation ofcomputing series. MIT Press, 1996.
E. Moggi. Computational lambda-calculus and monads. In LICS, pages
14–23. IEEE Computer Society, 1989.
E. L. Robertson, L. V. Saxton, D. V. Gucht, and S. Vansummeren. Structural
recursion as a query language on lists and ordered trees. Theory ofComputing Systems, 44(4):590–619, 2009.
J. Rutten. Universal coalgebra: a theory of systems. Theoretical Computer
Science, 249(1):3 – 80, 2000.
A. K. Simpson and G. D. Plotkin. Complete axioms for categorical fixedpoint operators. In LICS, pages 30–41, 2000.
A. Sokolova. Coalgebraic Analysis of Probabilistic Systems. PhD thesis,
TU Eindhoven, 2005.

19

a

0

02 01 03

a
2 1 3

a
12 11 13that l′ ◦ f = l. The above correspondence is given as the following:for (L, l) ∈ CList(S),

0

0

Gt

a
02 01 03a-1
L
(R(L), [l ◦ ηL]∼= ),= ) ∈ ΣL∈L (S /∼...

12 11 13and for (L, [l]) ∈ ΣL∈L (S L /∼= ),a

R(L, l) ∈ CList(S),22 21 23

which is well-defined, i.e., if (L, l) and (L, l′ ) are isomorphic, thenR(L, l) and R(L, l′ ) are equal by the uniqueness in the definitionof R. It is easily checked that this correspondence is bijective.
In the body text, we omit the taking quotient in the right handside of the above isomorphism for simplicity.

Figure 12. Branch with Any Countable Linear Order

A.

Ordered Graphs for Any Countable Linear
Ordered Sets

We see here that, for any countable linear ordered set, there is an
infinite ordered graph having ε-edges such that the branches of theroot after eliminating ε-edges are exactly as the given ordered set.
Now let L be an infinite countable linear ordered set, so there∼=
exist a bijective function f : N → L. Then we construct a graph“representing L” as below. Let us consider the kind of ternary tree
Gt as the left tree in Figure 12. We call a leaf in a tree ε-leaf if
the path from the root to the leaf consists of just ε-edges. First,
corresponding to f (0) ∈ L, we take a fresh Gt . Next, we again
take a fresh Gt , and if f (1) < f (0), then we put together the rootof the new Gt and the left ε-leaf of the former graph, as the middle
graph in Figure 12. Otherwise if f (0) < f (1), we put similarly
to the right ε-leaf (03 in the example). Next, now there are three εleaves (12, 13, 03 in the example) with the obvious linear order, i.e.,
12 < 13 < 03. Then according to the three possible positions off (2) in the linear ordered set {f (0), f (1), f (2)}, we again put new
fresh Gt to the corresponding position of ε-leaf. The right graph in
Figure 12 is the example of the case when f (1) < f (2) < f (0).
Iterating as this, we have an infinite tree with finite (in fact justthree) width. Then it is obvious that the countable linear ordered
set occurring in the result graph of ε-elimination applied to thistree is order isomorphic to L.

B.

C. Finitary Monad Extension for ε-elimination
Let T be a monad and iter be an uniform iteration operator in
SetT . We define ε-elimination for finite T |fin -graphs, as the resultgraph is equal to one defined by Definition 9.
Let G = (V, B, I) be a finite T |fin -graphs in T DB X
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
commute.

/ T |fin (Lϵ ×V +Y )V XXXXXX
X
B∼=/ T |fin (V +(L×V +Y ))
O
XXXXX
XXXXX
XXXXX
XXXXX
B′
,
?

T |fin (V +(L′ ×V +Y ))Now V +(L′ ×V +Y ) is a finite set, hence T |fin (V +(L′ ×V +Y )) =T (V +(L′ ×V +Y )). We therefore can apply the iteration operator
iter to B ′ . We define B ′′ as the composition of the below
Viter (B ′ )−→ T |fin (L′ ×V +Y ) ,→ T |fin (Lϵ ×V +Y )and then define ε-elim(G) = (V, B ′′ , I).
For a finite T |fin -graph G, by the inclusion T |fin ,→ T , we
can regard G also as a T -graph. Then it can be easily checkedthat the above ε-elim(G) is exactly equal to ε-elim(G) defined in
Definition 9 for the T -graph G.
def

Countable List

Here we give a detail explanation about the countable list monad
CList.
First we give a formal (and abstract) definition: CList(S) is theobject-set of the skeleton category of the comma category (U ↓ S)
where U : CLO → Set is the forgetful functor from the category
CLO of countable linear ordered sets and monotone functions.
Now let us unfold this definition. An object of the comma
category (U ↓ S) is a pair (L, l) of a countable linear ordered set
L and a function l: L → S. A morphism f from (L, l) to (L′ , l′ ) isa monotone function f : L → L′ such that l′ ◦ f = l. Then we cantake the object-set CList(S) of a skeleton category of (U ↓ S),
i.e., we have a subset CList(S) of the object-set of (U ↓ S) suchthat for any object (L, l) in (U ↓ S), there is the unique R(L, l) ∈CList(S) such that (L, l) and R(L, l) are isomorphic in (U ↓ S),
and then also there is a chosen isomorphism η(L,l) : (L, l) →R(L, l).
There is another equivalent form to CList(S). Let L be theobject-set of a skeleton category of CLO, i.e., we have a subset
L of the object-set of CLO such that for any object L in CLO,
there is the unique R(L) ∈ L such that L and R(L) are isomorphic
in CLO, and then also there is a chosen isomorphism ηL : L →R(L).
Then, we give the following isomorphism

D. Proof of Full Representability by the Graph
Constructors
Here we give two proofs of Proposition 19: full representability offinite graphs by the graph constructors. The first one is simpler andhighly depends on the notion of marker, while the second one is ina naive way, which less depends on the notion of markers. The second proof shows that the notion of marker is—very convenient as in
the first proof but—not essential for the fact of full representability.
First let us see the notion of 1-step unfolding uf ε , which isalmost the same as that of uf defined in Section 4.3.1. Here we
consider graphs having ε-edges, while in Section 4.3.1 we consider
graphs having no ε-edge. However the two are essentially the same
notion since here we first consider strong bisimilarity for properties
of uf ε itself, and then we move to the level of bisimilarity by thefact that strong bisimilarity implies bisimilarity.
Now we define the 1-step unfolding
uf ε : DB f Y → T (Lϵ ×DB f Y +Y ).
First, for a graph G = (V, B, I) ∈ DB X
Y , and a node v ∈ V , wedefineL
CList(S) ∼= ΣL∈L (S /∼=)def

G|v = (V, B, {& 7→ v}) ∈ DB Y .
Then for G = (V, B, I) ∈ DB f Y ,where the ∼= in the right hand side, is the restriction of the isomorphism equivalence on |(U ↓ S)| to its subset S L ; i.e., forl, l′ : L → S, l ∼= l′ if there is an isomorphism f : L → L suchdef

uf ε (G) = T (Lϵ ×f +Y )(B(I(&)))
20

def

where f = G|(-) : V → DB f Y .
By the results [Adámek et al. 2006, Theorem 3.3] with [Milius
2010, Corollary III.15], we can show that for any finitary monad T ,this uf ε is isomorphic up to strong bisimilarity.
Furthermore, uf ε -1 is constructed just by graph constructors:

If the root I(&) is cyclic, we define a graphG′ = (V ∪{v0 }, B ′ , I) ∈ DB f Y ∪{&y0 }defwhere v0 and &y 0 are fresh ones, and B ′ is defined as below.
()
B ′ : V ∪{v0 } → T Lϵ ×(V ∪{v0 })+(Y ∪{&y 0 })uf ε -1 = t ◦ T ([s, s′ ])v0 7→ return(Outm (&y 0 ))

where



t: T (DB f Y ) → DB f Y
is defined with the T -algebraic graph constructors using the finitar∪(i)
ity T (S) = i∈N TΣ (S), andv 7→ T (g)(B(v))
g: Lϵ ×V +Y → Lϵ ×(V ∪{v0 })+(Y ∪{&y 0 }) Edge (l, I(&)) 7→ Edge (l, v0 )the other case : embeddingdefs = ⟨(-):(-)⟩: Lϵ ×DB f Y → DB f Y





Then
G = ⟨&y 0 ⟩ @ cycle(&y 0 := G′ ), and′ defs = ⟨-⟩: Y → DB f Y .

|G′ | < |G|,
since, while G′ has just one extra node, at least the root becomes
non-cyclic.
When the root I(&) is not cyclic, consider uf ε (G); then as seen
above, G is (strong bisimilar, hence) bisimilar to uf ε -1 (uf ε (G)),
where recall that uf ε -1 is a composition of graph constructors. On
the other hand, let us consider graphs G′ occurring in

For example, when T = List,
t = foldr(++, []): List(DB f Y ) → DB f Y .
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 see the first proof.

uf ε (G) ∈ T (Lϵ ×DB f Y +Y ),Proof. Let G = (V, B, I) be a finite graph in DB f X
Y . First we
prepare a marker &v for each node v, then we write &V for theset of the markers, and define f : V → &V as f (v) = &v . Then foreach v,
( (
)(
))
def
Gv = uf ε -1 T Lϵ ×(⟨-⟩ ◦ f )+Y B(v) ∈ DB &V +Y′

i.e., a graph G in the minimum—then finite since T is finitary—set
P ⊆ DB f Y such thatuf ε (G) ∈ T (Lϵ ×P +Y ).
′Each G in P is a subgraph of G, and the root of G′ is a node inPI(&) of G. Since I(&) is not cyclic, the accessible part of G′ does
not include I(&), hence |G′ | < |G|.

can be represented by graph constructors. Then⌊f ◦ I⌋ @ cycle(⊕v∈V &v := Gv ) ∈ DB X
Y
is bisimilar to the original graph G.
For example, for the graph G in Example 2,
G1 = ⟨d : ⟨&2 ⟩⟩ ++ ⟨a : ⟨&4 ⟩⟩G2 = ⟨c : ⟨&3 ⟩⟩G3 = ⟨d : ⟨&2 ⟩⟩G4 = ⟨b : ⟨&3 ⟩⟩ ++ ⟨&y⟩,then G is bisimilar to()⟨&1⟩ @ cycle (&1 := G1 ) ⊕ (&2 := G2 ) ⊕ (&3 := G3 ) ⊕ (&4 := G4 ) .

Now we see the second proof. First we define “node in cycle”.
For a finite graph (V, B, I) and v ∈ V we define Pv as theminimum subset P ⊆ V such that B(v) ∈ T (Lϵ ×P +Y ); thisis the set of all the nodes which are targets of edges from v. Then
def
def ∪
we define Pv0 = {v} and Pvn+1 = v′ ∈P n Pv′ by induction on
v
def ∪
def ∪
n. Now we define Pv∗ = n∈N Pvn and Pv+ = n>0 Pvn ; Pv∗ isthe set of the nodes which are accessible from v, and Pv+ is theset of the nodes which are accessible from v through at least one
transition. We call a node v such that v ∈ Pv+ a cyclic node.
Now let us see the second proof.
Proof. Let G = (V, B, I) be a finite graph in DB f X
Y . We canassume that X = 1(= {&}), recovering other cases by the graphconstructors () and ⊕. Now we show the statement by induction on
the natural number
def|G| = |V |+2×|V cycle |where V cycle is the set of cyclic nodes.

21