1 Introduction
Designing graph transformation languages is difficult in general, because graph structured data may have cy- cles and shared nodes.  There are three major difficul- ties:  consistency, finiteness-preservation, and  termina- tion of evaluation.  The consistency indicates the same treatment of 'equivalent' graphs, where equivalence is usually specified by either bisimilarity or isomorphism. Graphs up to bisimilarity are equivalent to infinite trees, whereas graphs up to isomorphism are "graphs as they look". In this paper, we focus on graphs up to bisimilarity for the application to querying tree databases with cyclic references such as XML with IDREF. Ensuring consis- tency requires that every graph transformation is bisimu- lation generic : i.e., the transformation results of bisimilar graphs are bisimilar. For finiteness-preservation, it means that every term maps finite graphs (graphs with finite number of nodes) to finite graphs; this and the termination properties are important for graph query languages.  Full recursion, which is a typical way of constructing powerful trans- formations, is not desirable, since the termination and finiteness-preservation do not hold.  Structural recursion (fold) for inductive datatypes such as lists and finite trees naturally has both properties; however for graphs, be- cause of the non-well-founded nature, it is difficult to find such a structural recursion. Functions defined by core- cursion (unfold) terminate, but do not necessarily return finite graphs. One prominent step to solve these problems was given in the work of UnCAL [6].  Their structural recursion for graphs is suitably restricted from that for infinite trees so that the termination and finiteness-preservation hold. The expressive power is less than that of fold for finite trees, but it is still powerful enough to translate an SQL-style graph query language—called UnQL— into UnCAL.  Moreover, they gave bulk semantics for the structural recursion, which is "divide-and-aggregate" style semantics and enables parallel evaluation. The key to defining the structural recursion of UnCAL is use of ε- edges, which work as shortcut like the ε -transitions of automata.  Then the bulk semantics makes it easier to prove the finiteness-preservation and termination prop- erties.  UnCAL is used also as a basis for bidirectional graph transformation [15] and for model driven software engineering [27]. However, there is a big restriction on UnCAL:  graph models of UnCAL are just unordered graphs, i.e., graphs whose branches have no sibling order; while in real applications, there are many graph models such as or- dered graphs, weighted graphs, probability graphs, etc. Though, when we generalize the graph model of UnCAL, we come across a subtle problem: how can we generally define the notion of bisimilarity for each graph model that has the notion of ε-edge? Additionally, we should point out that UnCAL has an- other weak point. The structural recursion of UnCAL is a higher order function like the fold for trees, but the bisim- ulation genericity of the structural recursion in UnCAL has been proved only on the first order part, and UnCAL is formulated as just first order calculus, which blurs how to extend UnCAL to richer type systems. In the previous work [14], the authors studied how to modify the graph model of UnCAL so that we can treat ordered graphs in a similar way to UnCAL.  There it is found that ε -edges of ordered graphs may produce a subtle problem of infinite width on branches; this prob- lem does not occur in the case of unordered graphs.  It was resolved by proposing a new calculus for finite or- dered graphs, giving a new definition of bisimilarity for ordered graphs having ε -edges, and giving the semantics of the calculus for ordered graphs.  The calculus is ex- tended with higher order functions and formulated as an extension of simply typed lambda calculus. Along that line, in this paper we further generalize the graph models, and propose a family of calculi λ FG , which is parametrized by monads T ; each λ F G can treat graphs whose branches are represented by a monad T . For example, when T is the finite powerset monad, λ FG becomes UnCAL, precisely, UnCAL extended as a sim- ply typed lambda calculus. To introduce λ F G , we gen- eralize all the features of UnCAL with monads: i.e., its graph models, its graph constructors, and the structural recursion. In Section 2, we generalize the graph models from un- ordered graphs to T -graphs, by using a monad T (with some reasonable assumption) to represent various branch styles. When T is the list monad, the finite multiset monad, and the finite probability distribution monad, then T -graphs are ordered graphs, weighted graphs, and probability graphs, respectively. We also give a general definition of bisimilarity for T -graphs, with taking ac- count of ε-edges. In Section 3, we introduce the syntax and the seman- tics of the lambda calculi λ F G .  We give the definition of graph constructors, and show that all finite T -graphs can be represented by those graph constructors.  Then, we give a simple definition of the bulk semantics of the structural recursion for λ FG , and we prove all transfor- mations of λ F G is bisimulation generic. As well as gen- eralizing with monads, λ F C is extended from UnCAL with higher order functions, which is not for free but due to that our main theorem—bisimulation genericity of the bulk semantics—is stronger than the corresponding theo- rem for UnCAL [6]. In Section 4 we discuss related work, which includes more detail comparison between λ F G and the calculus in [14]. Our contributions are summarized as follows: ● We generalize the graph model of UnCAL with monads by applying coalgebra theory; also we present a general definition of semantic equivalence for graphs having ε-edges, which is given by combi- nation of ordinary bisimilarity and ε-elimination. ● We generally define graph constructors and struc- tural recursion for T -graphs, with identifying suit- able assumptions on the finiteness of T for the sake of practical use, which is discussed in Sec- tions 2.2. l and 3.2.4. ● We show that any finite T -graph can be constructed using graph constructors; also we find and utilize several equational properties for graph constructors. ● We extend semantic equivalence for graphs to higher order functions and show the bisimulation generic- ity of structural recursion as a higher order function, which enables us to reformulate UnCAL to more powerful and familiar style of calculus, i.e., the sim- ply typed lambda calculus λ FG The reformulation makes it clear that we can fur- ther extend λ F G  with familiar features such as co- product, algebraic datatype, polymorphic type, de- pendent type, and so on. In fact, although the cur- rent formulation of λ F ς (and also UnCAL) does not include transformations for manipulating the sibling direction—e.g., reversing the order of branches of an ordered graph—, we can add such transformations, using the above flexibility of extending λ FG . (See [2] for the details of such an extension for sibling transformations.)
2
Graph Model and Bisimilarity of λ FG
First, we explain what kind of graphs the λ F G -terms can transform.  After that, we give the semantic equiva- lence of the graphs: i.e., bisimilarity with ε-elimination.
2.1 Graph Model of XFG
The graphs in λ F G are rooted, directed, and edge- labeled graphs. Furthermore, the graph model of λ F G has two notable features: ε -edges and markers.  An ε -edge represents a shortcut between the two nodes; the shortcut works like the ε -transition in an automaton. Nodes may be marked with input and output markers ; these are used as interfaces to connect a graph to another graph by ε- edges. (This is done by @ and cycle as the dotted edges in Figure 4, and by srec as in Figure 5.) Let us introduce the notion of a T -graph, which has "T -kind of branches", for a monad T . First, though, let us recall the notion of a monad (in the Kleisli triple style): a monad on Set is a triple T = ( T , return , lift ) of func- tions T : |Set| → |Set| returns: S → T(S)   (S ∈ |Set|) lift s,s,: (S → T(S')) → (T(S) → T(S')) ( S, S' E |Set|) such that these satisfy certain axioms (see [23][4] for the axioms). Example 1 (List Monad).  The list functor List forms a monad with the following monad structures: return(x) ll [x] lift f xs = concat (map f xs) where concat is to flatten a list of lists to a list. ● Now, let us define the graph model. We use L to denote a set of labels and L c to denote the disjoint union LU{ ε} . Let X and Y be finite sets of markers ; we add the prefix & for meta-variables of markers like & x . Then, a T -graph (or just graph) G is defined as a triple (V, B, I) where ● V is a set of nodes , ● B: V → T ( L c × V + Y ) is a branch function , where an element x in L c × V + Y (called a branch ) is either an edge Edge (l,v) or an output marker Outm (&y), and
Example of Ordered Graph bra B of the endofunctor T(Lc ×(-)+Y) equipped with I : X → V , which can be regarded as a generalized ele- ment (state) of V . Example 2 (Unordered Graph, Ordered Graph, Weighted Graph, Probability Graph). For the finite powerset monad P fin, P fin-graphs are unordered graphs , which are (equivalent to) the graph model of UnCAL. List-graphs are ordered graphs [14], where the branches are ordered.  An example of an ordered graph is shown in Figure 1. The finite multiset monad (bag monad) is defined as Mfin: Man(S) ≡ {φ: S→N | φ-1(N − {0}): finite}. Branches of Mfn-graphs have the bag semantics (rather than set semantics of P fin ), i.e., multiplicity (called weight) of an identical branch is not ignored. The finite probability distribution monad Dfin is de- fined as Dfin (S)新{φ: $→[0,1] | φ− 1 ((0,1]): finite, Σ sφ(s)=1}. The monad structure is defined as below:  for s ∈ S , return(s) is the Dirac delta function δ s : S → [0, 1]: δ。(x) ≡ 0 (x ≠ s) δ s (s) = 1 and for f : S
The set 1 of graphs—with X and Y as sets of input and output markers, respectively—is denoted by T-G¥ ; here, T may be omitted as G X if it is clear from the con- text. We call a T -graph a finite T -graph when V is a finite set, and write T-G f X  for the set of finite T -graphs (in [6], Pfin-GfX is written as DB¥ ). We allow a graph to have multiple roots: a multi-rooted graph is to a forest as a single-rooted graph is to a tree. For single-rooted graphs, we often use a default marker & to indicate the root and use Gy  to denote G{ 4 } Note that a node can have several output markers—if a monad T is non-deterministic as the above examples— and an output marker can be put on several nodes; while, a node can be pointed by several input markers, but an input marker points just one node.
2.2   Graph Equivalence in λ F G : Bisimilarity with
ε-elimination
In the remaining part of this section, we give a se- mantic equivalence of graphs of λ ξ G .  As discussed in the introduction, we regard the graphs in λ F G as an ex- tended tree data structure, i.e., as infinite trees, so we shall use bisimilarity semantics rather than equality or isomorphism semantics. The main difficulty with our definition of bisimilarity is the treatment of ε -edges. We first explain strong bisim- ilarity , in which we regard the label ε as a usual label such as those in L. Then, we define bisimilarity , which "skips" ε-edges. Note that our notion of bisimilarity for the invisible la- bel ε is different from weak bisimilarity for the invisible label τ in the context of process algebra [21]. One pur- pose of our use of ε -edges is to postpone the calculations of the graph constructors, structural recursion, and so on, but weak bisimilarity is unsuitable for expected proper- ties of such graph transformations: e.g., weak bisimilar- ity can not ensure the associativity of the graph construc- tor ∪ (defined in the next section). Now, let us recall the notion of a bisimulation rela- tion for any endofunctor F on Set.  First, we define relational lifting F of F . For a relation R ⊂ V × V ′ , i.e., for an inclusion {r,r'}: R {} VxV', we obtain {F(r), F(r')} : F(R) → F(V)×F(V'); then the rela- tion F(R) ⊆ F(V)×F(V') can be defined as the im- age ⟨F(r), F(r')⟩(F(R)). Next, for 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 3 (Strong Bisimilarity). Let T be a monad, and G = (V, B, I) and G' = (V', B', I') be T-graphs in T-G ξ . Then G and G ′ are strongly bisimilar if there is a bisimulation relation R with respect to the endo- functor T ( L ε×(-)+Y ) between B and B ′ such that for any &x E X, I(&x) R I'(&x); in this case, we write G ～ G ′ . ● We assume that all monads T in the paper preserved weak-pullbacks, which is a mild assumption often used in coalgebra theory [26][30]. In particular, then T preserves injections and finite intersections. Using this assumption, it is easily checked that the strong bisimilarity relation is an equivalence relation on T-G X Let us unfold the above abstract definition of strong bisimilarity, when T = P fin : R : a bisimulation relation for P fin(L ε×(-)+Y) ←⇒∀( v, v' )∈R. (B(v), B' ( v' )) ∈ (Pfin(Le×r+Y), Pfin(Le×r'+Y))(Pfin(Le×R+Y)) ⇐⇒∀(v, v')∈R. ∃S ⊂fin Le×R+Y. B(v)=(Le×r+Y)(S) ∧ B'(v')=(Le×r'+Y)(S) ⇐⇒∀( v, v ' ) ∈ R. ∃{(l1, (u1, u'1)), ..., (ln, (un, u'n)), &y1, ..., &ym} Sfin Le×R+Y. B(v)={(l1,u1),...,(ln,un),&y1,...,&ym} ^ B'(v')={(l 1 , v'1), ..., (l n , v'n ), &y1, ..., &ym} ←⇒∀( v, v ' ) ∈ R. (∀(l,u)∈B(v).∃u'.(l,u')∈B'(v')∧(u,u')∈R)∧ (∀&y∈B(v). &y∈B' (v')) ∧ (∀(l,u')∈B'(v'). ∃u. (l,u)∈B(v)∧(u,u')∈R) ∧ (V&yEB'(v'). &yEB(v)) The last formula can be expressed as in the following pictures. Now, let us define our bisimilarity, whose instantiation to the case when T = P fin should agree with the bisim- ilarity of UnCAL [6]. The bisimilarity of UnCAL is de- fined by replacing the first and the third pictures above with the following two pictures (and similarly for the sec- ond and the fourth pictures). With this bisimulation, we "skip" zero or more occur- rences of ε -edges before a non- ε edge or an output marker.  Categorically, this kind of iteration is captured by the notion of an iteration operator , which is the dual notion of a fixed-point operator [29][17]. From now we define ε -elimination —which is almost the same as that for an ε -automaton—in terms of an iteration operator in the Kleisli category of a monad T , and then give a defi- nition of bisimilarity for T -graphs. For a monad T on Set, the Kleisli category Set T of T is defined as below: objects in Set T are sets, and mor- phisms S → S ′ are functions S → T ( S ′ ). The identity morphism id on S is id = return: S → T(S), and the composition g ⊙ f of f : S → T ( S ′ ) and g : S ′ → T( S ′′ ) is defined as g으f ≡ lift(g) ○ f : S → T(S"). A Kleisli category has coproducts:  the coproduct of S 1 and S 2 is just S 1 + S 2 , and the injections are in 1 = return 0 in 1 : S 1 → T (S 1 +S 2 ) in r = return o in r : S2 → T(S1+S2). Copairing of a pair of functions f 1 : S 1 → T ( S ′ ) and f 2 : S 2 → T ( S ′ ) is the same as the copairing in Set, i.e., [f1, f2]: S1+S2 → T(S'). We write ∇ : S+S → T(S) and + for the codiagonal and the coproduct on morphisms in Set T , respectively. Next we recall the notion of an iteration operator [10] [17]. Though we can define an iteration operator for any category with finite coproducts, here, we define it directly on the Kleisli category Set T of a monad T on Set, and say that a monad T has an iteration operator if Set T has it. An iteration operator iter on Set T is an operator on functions f : S → T (S + A) iter(f): S → T(A) such that the operator satisfies the following axioms: ● (naturality:) for f : S → T(S+A) and g : A → T(A'), g □ iter(f) = iter((ids+g) □ f): S → T(A'), ● (dinaturality:) for f : S → T(S ′ + A) and g : S ′ → T(S+A), [iter([f, inr]こg), idい]こf = iter([g, in,]으f ): S → T(A), ● (unfolding:) for f : S → T(S+A), iterf = [iterf, ida]こf : S → T(A), ● (codiagonal:) for f : S → T(S+S+A), iter(iterf) = iter(( ∇ +id λ )こf ): S → T(A). Further, for a class M of morphisms of Setr, iter is called uniform on M if for any function f : S → T ( S ′ ) in M , and any functions g : S ′ → T ( S ′ + A ) and h : S → T(S+A), iter(g)こf = iter(h): S → T(A) whenever gof = (f+id A )oh: S → T(S'+A). The axiom of uniformity is used for logical relation on an iteration operator [12]. We use uniformity to show later that strong bisimilarity implies bisimilarity, and also in the proof of Lemma 16. Example 4 (Monads with Iteration Operators).  For the countable powerset monad Pcnt and a morphism f : S → Pcnt (S'+S') in Set Pcnt , iter(f)(s) c= {s'ES' | 3kEN. 3s1, ..., skES. s1 Ef(s) ∧ … ∧ sk Ef(sk-1) ∧ s' Ef(sk)}. Also, the countable multiset monad  Mcnt : Mcnt (S)参{φ: S → NU{∞} | φ= 1 (N − {0}) is countable} has an iteration operator, which is given with the same formula as that for P cnt . Extending the list monad— List(S) ≡ countable list monad CList is defined as CList(S) ≡ L L EL S L , where N is generalized to L, the set of countable linear ordered sets up to order isomorphism † 2 . Set CList also has an iteration operator (see [14][2] for the details). For probability graphs, countable subprobability dis- tribution monad SubD cnt has an iteration operator: SubDcnt(S) = {φ: 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 for the probability of the nonter- mination of the iteration operator.  The definition of the iteration operator for SubDcnt is also similar to those for Pcnt and Mcnt , see [16] for the details. ● Now, let us define ε -elimination. The following char- acterization of ε -elimination as an iteration operator is due to [13][16]. Definition 5 ( ε -elimination).  Let T be a monad and iter be an iteration operator in Set T . For a T -graph G = (V, B, I) ∈ T-G¥ , its ε-elimination ε-elim(G) ∈ T-G¥ is (V, B', I) where B' ≡ embed 0 iter(iso 0 B), T(L×V+Y) embed is the embedding T( L c × V + Y ), and iso is the composition of T(Le×V+Y) ~ T((L+1)×V+Y) = T(V+(C×V+Y)). Conversely, ε -elimination induces an iteration opera- tor; let us consider a T -graph ( V, B, I ) in the case that L = 0. Then B : V  → T({ε}×V+Y), and if we ap- ply ε-elimination to this, the resulting branch function is B': V  → T(0×V+Y). That is, we get an opera- tor that maps a function V → T(V+Y) to a function V → T(Y). This operator is the same as the structure of an iteration operator in the Kleisli category (if we allow Y to be arbitrary sets); and then we find that it is natural to adopt the axioms of iteration operators as axioms of the ε-elimination. Now, let us define our bisimilarity for graphs having ε-edges. Definition 6 (Bisimilarity).  Let T be a monad having an iteration operator iter in the Kleisli category Set T , and G = (V, B, I) and G' = (V', B', I') be T-graphs in T-G¥. Then, G and G ′ are bisimilar if ε -elim( G ) and ε-elim( G ′ ) are strongly bisimilar; in this case, we write G ～ G ′ . ● It immediately follows that strong bisimilarity implies bisimilarity, if the iteration operator of T is uniform on the class of functions (rather than not necessarily on all morphisms in Set T ). We use this property in some of the proofs of this papers. When T = Pcnt, by unfolding the above definition, we get the original definition of bisimilarity in UnCAL. The above definition implies that the notion of an ε- edge a la ε -elimination is independent of bisimilarity se- mantics, and it can be accommodated in any equivalence relation, such as equality and graph isomorphism, by sim- ilarly taking inverse images.
2.2.1
Generalization of Bisimilarity with Monad
Extension
Although we could define bisimilarity as above, when T is one of the monads in Example 4, the T -graphs might have countably infinite width of branches. In a real database system, a graph (is often very large but) has fi- nite size, i.e., finite number of nodes and a finite width. In other words, real data graphs do not have ε -edges, which cause graphs to have infinite widths. Our use of ε -edge is just in an implementation of λ F G for efficiency and for defining structural recursion; so we shall suppose that what users of λ F G can observe is just finite-width graphs, and graphs whose ε -elimination have infinite widths are regarded as errors. (For any finite List-graph G , it is de- cidable whether the ε -elimination of G keeps finite width or not; see [14][2].) Therefore, the finite powerset monad and the other monads in Example 2 are more suitable for practical purposes; however, they do not have iteration operators. Hence, we do not require that T itself has an iteration operator in the Kleisli category, and instead we use the following assumption:  we say that T has an extension T ′ for ε -elimination if we have a monad T ′ , an injective monad morphism ι : T ↔ T ′ , and an iteration operator in the Kleisli category of T ′ that satisfies the uniformity Term e | if e then e else e { conditional } { T -algebraic graph constructors ( s ∈ Σ) } op, { common graph constructors } │ cycle(e) { structural recursion application } | srec(e)(e) { label ( α ∈ L ) and label equality } | a | e = e Type σ ::=  Bool | Label | G ¥ { boolean, labels, graphs } { product types and function types } │ σ×σ │ σ→ σ Fig. 2    Syntax of λ FG on the class of functions. Here, monad morphism is a nat- ural transformation that is compatible with return 's and with lift's (see [4] for the details). Definition 7 (Bisimilarity Generalized on Size).  Let T be a monad which has an extension T ′ for ε -elimination. Then there is an embedding ι-G¥ : T-G¥  →  T'-G¥ which maps (V, B, I) to (V, ι ( Lε ×V+Y) ◦ B, I ). For G and G' in T-G¥ , G and G' are bisimilar if ι-G¥ ( G ) and ι-G ξ (G ′ ) are bisimilar in the sense of Definition 6. From the assumption that ι has injective components and T preserves weak pullbacks, ι-G χ reflects strong bisimilarity [30]; hence, strong bisimilarity and the above bisimilarity are equivalent for T -graphs having no ε- edges. In the next section, we assume that a monad T is fini- tary and see the usefulness; after that, in Section 3.2.4 we will come back to more detail discussion why and how we need an extension of a monad for ε -elimination.
Syntax and Semantics of λ FG
3
Here, we give the syntax of λ ξ ς and its semantics. The semantics of λ F G has two steps.  The first step is an interpretation to just in the (V, B, I) form, without considering bisimilarity.  This is equality-based seman- tics rather than bisimilarity-based one. The next step is to give an interpretation up to the bisimilarity; to do so, we need to show bisimulation genericity of terms, i.e., well-definedness in terms of bisimilarity.  Since struc- tural recursion is a higher order function, before showing bisimulation genericity, we will extend the equivalence relation of bisimilarity to function types.

3.1  Syntax of λ FG
3.2  Graph Constructors
tors in λ FG - The original UnCAL and λ ρ fin have the nine graph constructors in Figure 4, by which all finite graphs can be represented.  (In the original UnCAL, the graph con- structors { a : -} and {&y} are written as { a : -} and &y, respectively.) Note that these constructors should be writ- ten as {} y, G 1 U x,y G 2 , and so on with type (marker- sets) annotation; however, we will omit the subscript X and Y to avoid clutter. We separate the nine graph constructors into common graph constructors and T-algebraic graph constructors. When T = Pfin, {} and ∪ are T -algebraic graph con- structors, and the other seven graph constructors are com- mon graph constructors. Common graph constructors are defined independently of the difference of monads, while the definition of T -algebraic graph constructors depends on algebraic operations of T 3.2.1  Common Graph Constructors Definition 8 (Common Graph Constructors).  Let T be a monad. ●   For G = (V, B, I) ∈ Gy, (Just unfamiliar rules are listed. We use l and q as meta variables for variables of types Label and G ¥ , respec- tively.) (a : G)当(V ∪ {v 0 : fresh}, B ′ , {& → v 0 }) रह where B'( v ) B(v) and return (Edge (a, I (&))). ●   For &y E Y, (&y) ≡ ({&},  {& → return(Outm (&y))},  id{&}) Typing Rules of λ F ( For G = (V, B, I) ∈ Gy, (&x := G)当(V, B, {&x → I(&)}) ∈ G, ●  ()蛍(∅, "the unique function from ∅",  id∅) ∈ G f For G = (V, B, I) ∈ G ¥ and G ′ = (V ′ , B ′ , I ′ ) such that X ∩ X ′ = ∅, GY G ⊕ G′ ≡ (V+V′, B″, I+I′) ∈ G where B"  el [T(Le ×(in1)+Y) ◦ B, T(Le ×(in1)+Y) ◦ B']: V +V' → T(L c ×(V +V')+Y). For G = (V, B, I) ∈ G ¥ and G ′ = (V ′ , B ′ , I ′ ) ∈ GY G @ G' ≡ (V+V', B", in1 o I) ∈ GZ where B" ( in i ( v )) " T ( f )( B ( v )) ′ f: Lc×V+Y → Lc×(V+V′)+Z Edge (l,v) → Edge (l,in1(v)) Outm (&y) → Edge (ε, in, (I' (&y))) B"(in,(v'))当(T(Lc×(in,)+Z))(B'(v')) For a graph G = (V, B, I) E GX, Y such that Fig. 4  Nine Graph Constructors of The syntax of λ F G is given in Figure 2, and the typ- ing rule is given in Figure 3. The syntax of λ F G in fact depends on not only a monad T but also its signature Σ , which will be explained in the next subsection. However, the expressive power of λξς is independent of a choice of the signatures Σ. Here, we give an interpretation of the graph construc-
We give a notice on Figure 4.  Recall that, for one graph G in G ¥ and one marker &y ∈ Y , there may be more than one or zero &y-occurrences in G , while for one marker &x  ∈  X , there must be just one &x-input node in G . Hence, for each &y i in G @ G ′ in the figure, although the number of ε -edges from a node with &y i - output marker seems just one, in fact we add the same number of ε -edges as the number of &y t -output marker occurrences in G . This is the same for cycle( G ); but, on G ∪ G ′ , the number of added ε -edges are just 2m. 3.2.2  T -algebraic Graph Constructors Here, we will define the T -algebraic graph construc- tors. The definition depends on algebraic operations of a monad T , and the syntax for T -algebraic graph construc- tors depends on a signature Σ generating the monad T . For example, a finite powerset P fin ( X ) is a free semilat- tice, which has two algebraic operators, i.e., bottom and join. In the syntax of λ ρ fin , when we choose the signature Σ of (the function symbols of) bottom and join, then op s (s ∈ Σ) have the same interpretation as the two graph constructors {} and ∪ in the original UnCAL. Below, we first define the interpretation of T -algebraic graph con- structors without considering signatures, and after that we consider signatures for syntax of λ FG. Later, we assume T to be finitary in order to prove Proposition 11. A finitary monad on Set is a monad T on Set such that the functor T preserves all directed colimits in Set; in other words, for any set S and any x ∈ T(S), there is a finite subset S ′ ⊆ S such that x ∈ T( S ′ ). The monads P fin , List , M fin , and D fin 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] E List({4, 1, 6}). Here, though we define graphs in ( V , B , I ) form, when we consider the property of graph operations, we con- sider them up to bisimilarity.  Hence, we assume that T has an extension for ε -elimination. First, we explain that defining T -algebraic graph con- structors for multi-rooted graphs is reduced to that for single-rooted graphs.  Note that the multi-rootedness is semantically the same as the power of sets of graphs: i.e.,
For an n -ary operator o : S n → S on a set S , there is the obvious n-ary operator o(x) on the X-th power of S: i.e., the composition of ( S × ) n  → ( S n ) ×  − →  S × ; we call this power algebra . Then, when T = Pfin, i.e., for UnCAL, it can be shown that ∪ : ( Gr ¥ ) 2 → Gr ¥ is noth- ing but the X-th power algebra of ∪: ( Gry ) 2 → Gry- Hence, we will define T -algebraic graph constructors with the type (GfY)" → GfY Now, for a finitary monad T , let us define a func- tion T G as T G (X) H T-G f X for a finite set X. As we will soon show, T G itself can be extended to a fini- Then, for constructing operators of the tary monad. type (Gry)" → Gry, i.e., T G (Y)" → T G (Y) we can use the result [24] that an element s in T(n) bi- jectively corresponds to a family o ( s ) of n -ary opera- tors (o(s)v: T(Y)n  → T(Y))y: set that is natural on Y ∈ Set T . In this context, s is called a generic effect , and o ( s ) is called an algebraic operation . For s ∈ T ( n ), o(s) is defined as
and for (oy : T(Y)n  → T(Y))y : Set T , the correspond- ing s is defined as o n ( return , ).  For example, when T = Pfin, {0,1} ∈ Pfin(2) (2 = {0,1}) corresponds to ∪: Pfin(Y) 2  →  Pfin(Y).  From now, we apply this correspondence to the case of T G as T .  Then we will show that, for a given finitary monad T , there is an em- bedding of T into T G , so that we can define T -algebraic graph constructors by algebraic operations of T . Now, let us define the monad T G . Here, we consider only finite sets, since it is enough here (and also since finitary monads are determined by definitions for finite sets by the left Kan-extension as in [18]).  The monad structures of T G are defined as follows:  return T G :  X → Gf χ maps &x to {&x}, and lift T c : (X → Gf y) → (Gi x → Gi y) maps f to (-) @ oplus(f). Thus, a graph in Gr ξ ( ≥ ( Gr Y ) × ) can be regarded as a "function" from X to Y (precisely, a morphism in the Kleisli category of T S ); then the composition is given by @ operator. For later use, for f : X → Y , we define its marker renaming graph [f] ≡ oplus(returny ° f) ∈ GiX Then, [ id χ ] becomes the identity for the composition @. Next, we define a monad morphism γ: T → T 9 ; यु ॥ for a finite set X and s  ∈  T(X), γ(s) ({*}, B, {& → *}) E Gr x where B(*)을T(inr)(s) E T(L ε ×{ &}+X). For example, for T = P fin and 2 = {&0,&1} ∈ Pfin(2), γ(2) ∈ T 9 (2) ＝ Gf 2 is a single node graph where the node has two output markers &O and &1 and no edges. Now, as promised above, let us consider T G as an in- stance of T for the function (1). For n = {&0, ..., &n=1} and G ∈ T S (n) = G r n , its algebraic operation is
agrees with ∪: ( Gry )² → Gry in UnCAL. As explained above, ∪ for G t -   in Figure 4 is just the X -th power alge- bra of ∪ for Giy . Observe that, corresponding to @ and ⊕ occurring in (2), in Figure 4, the graph constructor U has similar parts to @ and ⊕ . Let us sum up the above. Definition 9 ( T -Algebraic Graph Constructor). Let T be a finitary monad.  For a generic effect s ∈ T (n) (n = {&0, ..., &n=1}), the T-algebraic graph construc-
Signatures of Monads In general, there are infinitely many generic effects s ∈ T(n)(n = 1,2,...). For defining syntax of λ FG , we have to choose a set Σ of generic effects such that Σ is "presentable in computer" and generates all generic effects. For a finitary monad, there is a subset Σ of Π n ∈ N T ( n ) such that, for every set S , any generic effect in T( S ) is a finitely many times iterated composition of some generic effects in Σ; here, for generic effects s  ∈  T(n)(n={0,...,n=1}) and ti  ∈  T(S)(i  = 0, …, n –1), their composition means the Kleisli compo- sition lift T (i → t i )(s) ∈ T ( S ). We call such Σ a signature and call an element s in Σ ∩ T (n) a function symbol of arity n . The whole set L n ∈ N T ( n ) itself is one (maximum) signature, but usually there is a much smaller signature—finite, or presentable in a meta language for implementation—as the following examples. Example 10. When T = Pfin , we can take a signature {{}(E Pfin(0)), {0, 1}(E Pfin(2))}. Then, opfi and OP{0,1} are the same as the graph constructors {} and U in UnCAL, respectively. The cases of List and Mfin- which correspond to monoid and commutative monoid, respectively—are quite similar. For the finite probability monad Dfin , let us see that the following Σ becomes a signature: Σ(2) ≡ { s,: 2 → [0, 1] | r ∈ [0, 1]} C Dfin(2) Σ(n) ≡ 0 (for other n ) where s, is defined as s, (0)当r and s, (1)当1 − r, For φ 1 , φ 2 : S → [0, 1] in D fin (S), o(sr)(φ 0 , φ 1 ): S → [0, 1] in Dfin ( S ) is as below: o(sr)(φο,φι)(s) = r ·φο(s) + (1−r) ·φι(s). Now recall that "singletons" in Dfin(S) , i.e., elements in return( S ) are given as the Dirac delta functions δ s as in Example 2. Then it is easy to see that the above Σ in fact becomes a signature: for example, φ: N → [0, 1] in Dfin (N) such that can be represented by algebraic operations from the
As this example, though a signature may be infinite, still may be presentable in a meta-language for implementa- tion. ● A signature is enough to represent all T -algebraic For generic effects s graph    constructors:気T(n)(n={0, ...,n=1}) and t i ∈ T(m)(i = 0, ...,n=1), the T -algebraic graph constructor of the Kleisli composi- tion lift T (i → t i )(s) ∈ T (m) agrees with the composi- tion of the corresponding T -algebraic graph constructors op¸ : (Gr¥)²  → Gr¥ and op¸ : (Gr¥)m  → Gr¥, i.e., op¸ o ⟨ op¸ ⟩ i ∈ n : ( Gr ¥ ) m → Gr ¥ . Hence, by the definition of signatures, any T -algebraic graph construc- tor can be represented as a finitely many times iterated composition of T -algebraic graph constructors of some function symbols in a signature. Thus, though syntax of λ F G depends on the choice of signatures of T , the expressive power of T -algebraic graph constructors is the same regardless of the choice. As an important remark, the above definition of T- algebraic graph constructors gives us equational theories for T -algebraic graph constructors for free. T -algebraic graph constructors are defined through the monad mor- phism γ: T → T 9 , so the T -algebraic graph construc- tors obey the same axioms as those of the algebra of T . For example, finite powersets are free algebras of upper semilattices; hence, the graph constructors {} and ∪ sat- isfy all axioms of upper semilattices:  i.e., associativity, unitality, commutativity, and idempotency.  Moreover, since γ is monic, the converse, a kind of completeness, also holds. 3.2.3  Full Representability of Finite Graphs The next proposition is the most important property of graph constructors. Proposition 11 (Full Representability of Finite Graphs). Let T be a finitary monad on Set which has an extension for ε-elimination. Any finite T-graph can be represented up to bisimilarity as finitely many times applications of the graph constructors. Here we give a simple proof of the above proposition using the notion of markers; this proof is a generalization with monads of an idea explained with example in [6]. However, the use of markers is not essential; for naive and less simple proof, see [2]. Before the proof, we define 1-step unfolding function uf : Gfy  → T(Lc×Gfy+Y). First, for a graph G = (V, B, I) E Gr X , and a node ν ∈ V , we define G|v普(V, B, {& → v}) E Gf v (3) thus, we have a function G ( .) : V  → G f y .  Then for G = (V, B, I) ∈ Gry, uf(G) ≡ T(L c ×(G(c))+Y)(B(I(&))). The function uf  is strong bisimulation generic; taking the quotient G f y / ~ , the function uf /~~: Giy /~~ → T(Le×(Giy /~~)+Y) induced from uf is nothing but the coalgebra structure of final locally finite coalgebra [1][20]. Using [1] and [20], we can show that for any finitary monad T , uf / ~ α is iso- morphic. Let us define the inverse-up-to-strong-bisimilarity of uf : uf 1 : T(Le×Gry+Y) → Gry, i.e., uf-1 is also strong bisimulation generic and the in- duced function uf -1 /~, becomes the inverse of uf /~, This can be constructed just by our graph constructors: uf-1 = t ◦ T ([s, s']) where
and
Note that since T is finitary, for any element x ∈ T( G ε Y ), there exist s ∈ T ( n ) and n -number of graphs G i − i.e., G (.) : n → G t y − such that x = T ( G (.) ( s ) . Then,
Hence t ( x ) is defined with the T -algebraic graph con- structors. For example, when T = List , t = foldr(++,[]): List(Gfy) → Gfy . On the above s, precisely, s(ε, G) = {ε : G} is not a rep- resentation by graph constructors, because an expression {a : e} is not allowed in λ F G when a = ε . For the case, in the above definition, replace such {ε : ε} with e , which is bisimilar to {ε : e}. Now let us give the proof of Proposition 11. Proof.  Let G = (V, B, I) be a finite graph in G f X . First we prepare a marker &v for each node v , then we write & V  for the set of the markers, and define f : V → & V as f ( v ) = &v . Then for each v , Gv ∂≡ uf -1 (T(Lc×((-) o f)+Y)(B(v)) ) ∈ G k v +Y can be represented by graph constructors. Then | f ◦ I | @ cycle | ⊕  &v := G v ) is bisimilar to the original graph G. For example, for the graph G in Example 1,
then G is bisimilar to 〈&l〉 @ cycle ( ⊕i=1,…,4 (&i := G i )). 3.2.4 The Need of Monad Extensions for ε- elimination So far, we have seen the importance of the finitarity of a monad T for finite-graph transformation calculus λ F G .  Here, we explain why we need to care with the phenomenon of occurring infinite width in this paper and why we did not need to take such special care in the case of the original UnCAL for Pfin-graphs. When T is finitary and has an extension T ′ for ε- elimination, if we want to define ε -elimination only for finite T -graphs, without loss of generality, we can replace the extension T ′ with its finitary part T ′ | fin: (See Appendix A for the details.) For unordered graphs, ( Pcnt) | fin is equal to Pfin ; thus, we do not need Pcnt and ε -elimination does not produce infinite width. This is the reason why we did not need to consider infinite width for UnCAL. For ordered graphs, ( CList ) | fin ( S ) consists of such countable lists l that the number of elements of S that occur in l are finite.  Hence, still we can not avoid the notion of a countable linear order, i.e., infinite width, for even finite ordered graphs having ε -edges.  (For the de- tails on ordered graphs, see [14][2].) Also on the other two examples Man and Dfin, T ′ | fin does not become the original T : i.e., ( Mcnt ) | fin ( S ) = {φ: S → NU{∞} | φ − 1 (N − {0}) is finite} ( SubDcnt )|fin( S ) = {φ: S → [0, 1] | φ − 1 ((0, 1]) is finite, Σ xφ(x) ≤ 1}. However, in these cases, the both T ′ | fin are easily rep- resentable on computers differently from the case of infinite-width ordered graphs.
3.3 Structural Recursion
Now, let us define structural recursion for T -graphs, which plays a leading role in transformations of λ F G . We again show the typing rule for structural recursion:
When  T Pfin, the structural recursion f = srec(λ(l, g).e) is characterized by the equations below, where we ignore output markers and consider the case in which X  is a singleton for simplicity.
The above equations serve as a definition of f to be a function which inputs finite graphs and outputs infinite graphs, in a recursive way. However, the outputs of f are in fact (bisimilar to) finite graphs, and this is proved by using the following bulk semantics of f . Now, we give a definition of the bulk semantics, ex- plaining with Figure 5. In Figure 5, in each step, gray parts show parts unchanged from the previous step.  A marker above a node is an input marker and markers be- low a node mean output markers.  Each box with bold frame is itself a graph, while each dotted box—a part of a graph—has no meaning, just hints that it was a graph before. Briefly explaining, with bulk semantics, we first cal- culate the application of a given input function e to each pair of an edge and its following subgraph, as the graph (b) in Figure 5; though the example of e in the figure does not use the second argument for simplicity of expla- nation. After that, we connect the results in keeping with the shape of the original graph by using ε-edges, which results in the graph (f) in Figure 5. Definition 12 (Bulk Semantics of Structural Recursion). Let T be a finitary monad on Set.  For a function → Ge Z , a structural recursion function e: L×Gfy srec(e): Gr ¥  → Gr Z × ¥  is defined through the follow- ing steps. Before that, we extend e to ē: L ε×G t y  → G t ž which maps additionally (ε, _) to the "identity graph" [ id z ] ∈ Gr Z (see the upper leftmost picture in Figure 5). In the following, the steps from (a) to (f) correspond to those in Figure 5. (a)  [Input of srec(e)]. Let us take G = (V, B, I) ∈ Gi Y (b) [Relabeling by e]. Let us define ē: L c × V → G i Z as ē ○ ( id L ε ×G | ( - ) , where G | ( - ) : V  → G ε γ is de- fined as Equation (3).  Then, we construct a new branching function B 1 whose labels are graphs in G t Z : B 1 is defined as the composition of V → T( L ε × V + Y )  T( l ε , π 2 ) + idy )  T( G ε ≥ × V + Y ). (c) [Storing target nodes in output markers and du- plicating original output markers]. Let B 2 be the composition of the following functions V  => T(GfZ×V+Y) T([p,q]) T(GfZ×V+Z× where p and q are the obvious functions: (g,v) ≡ g @ [&z → in1((&z,v)) q(&y) ≡ [&z ) → inr((&z,&y))]. (d) [Connecting horizontally by T -algebraic graph constructors]. Now G f Y has the algebraic structure ty defined in Equation (4) after Proposition 11, and we can regard input marker sets as power through oplus: (Gry) X  => Gr X , so we have the obvious power algebra structure t(x) on G f X , i.e., the com- position of T(GfX) → T(GfY)× (ty)× Then, let B 3 be the composition of t(z) V ~ T(GfZxv+zxy) (e)  [Disjoint union by ⊕].  Using the bijective corre- spondence oplus : (V →GfZ×V+Z×Y) → GfZ×V+Z×Y we obtain a graph G' ≡ oplus(B 3 ) ∈ G i Z × V + Z × V (f) [Connecting vertically by cycle and input marker renaming]. Finally, we define srec(e)(G) 参[id z × I] @ cycle(G')   (E  Gr Z × ¥ ).   ロWe remark that the finitarity of a monad T is used at the step (d) for the algebra ty . The above definition works if we replace all G f with G ; for such definition for infinite graphs, T does not need to be finitary. We give an example of queries using the structural re- cursion, for more examples, see [6][15]. Example 13.  Consider an ordered graph representation of books. Since "sections" are ordered and there are some reference links in books, we can see books as ordered graphs.  The following structural recursion toc , which is adapted from [25], computes the table of contents of books in which sections can be arbitrarily nested: toc(db) = srec( λ(l,g).if l=section then {section : {get_title(g) ++ {&})} else (&) (db) where the function get_title results in the title of the sec- tion. get_title(g) = srec( λ(l 1 , g 1 ). if  l 1 = title then 〈title : srec〉 λ(l2,g2) 〈 l2 : [] 〉 〉 〈 g1 〉 〈 else [] ) (g)

3.4  Bisimilarity for Higher Order Functions
So far we have given the semantics with ( V, B, I ) form at the equality level. In the rest of this section, we con- sider semantics at the bisimilarity level. In Section 2, we gave the semantic equivalence for graph types G ξ , i.e., the bisimilarity. Since λ ξ G has higher order functions, and srec is a higher order func- tion, we have to extend the semantic equivalence for base types to function types. It is well known that if we lift an equivalence relation to function types we need to switch from the notion of an equivalence relation to that of a par- tial equivalence relation , i.e., an equivalence relation on some subset of the original set. This is because, now, not all functions on G r ξ  are bisimulation generic, so we have to cut out the subset consisting of bisimulation generic functions. Let us give the formal definition.  For the types σ of λ FG , we define binary logical relations ～ 。 on [σ]. When σ = G ξ , ~ c χ is the bisimilarity on G t ξ ; for the other base types σ , ～ σ are just the equality relations. When σ = σ 1 × σ 2 , we define a binary relation ～ σ on [σ] ≡ [σ₁] × [σ₂] as (x1,x2) ～σ (x'1,x'2)参考(x1 ~σ1 x'1) ∧ (x2 ~σ2 x'2). When σ = σ 1  → σ 2 , we define a binary relation ～ σ on [σ] dcf [σ1] → [σ2] as ∀ x, x' ∈ [σ₁]. (x ~σ₁ x' ⇒ f(x) ~σ₂ f'(x')). Then for any type σ , ～ σ becomes a partial equivalence relation on [σ], i.e., an equivalence relation on the subset |~o| ≡ {x ∈ [σ] | x ~o x}. We call a function f : [σ₁] → [σ₂] (higher order) bisim- ulation generic if f is in |~σ₁→σ₂|. (Note that this kind of lifting of semantic equivalence to function types is pos- sible for any equivalence relation such as strong bisimi- larity, graph isomorphism etc.) Then from the Basic Lemma of logical relation, inter- pretations of all the terms are bisimulation generic if in- terpretations of all the constants are bisimulation generic; as a result of the consequent of this implication, we ob- tain a model of λ F G in the cartesian closed category Set. (See the textbook [22] for the technique of logical rela- tion.)  In the rest of this paper, we prove that the inter- pretations of all the constants of λ F G are bisimulation generic.
3.5  Bisimulation Genericity of Terms of λ F G
First we show the bisimulation genericity of the graph constructors. Proposition 14 (Bisimulation Genericity of Graph Con- structors).  Let T be a finitary monad having an extension for ε-elimination. All the graph constructors are bisimu- lation generic. Proof.  First, for  a  constructor prove f, that ε-elim(f(G1, ...,Gn)) bisimilar is strongly to ε-elim( f (ε-elim( G 1 ), ...,ε-elim( G n ))).   By  this,  the bisimulation genericity of the statement is reduced to strong-bisimulation genericity, which is obvious. ● Next, let us consider structural recursion.  The result below is stronger than what is proved in [6], even when T = Pfin, because here bisimulation genericity is proved also on the first argument e , while in [6], it is proved only on the second argument G . This is the key point of our extension from UnCAL to the higher order calculus λ P fin Theorem 15.  Let T be a finitary monad having an ex- tension for ε-elimination T ′ .  Structural recursion srec is bisimulation generic, i.e., if e 1 ～ e 2 : L×T-GfY → T-G f Z , and G 1 ～ G 2 in T-G f X , then srec(e 1 )(G 1 ) ～ srec(e 2 )(G 2 ) in T-G f Z × X Proof.  Basically we want to prove in a similar way to the proof of Proposition 14, but there is a bit subtle problem. Though the following might be expected to hold, ε-elim(srec(e)(G)) ~ ε ε-elim(srec(ε-elim 0 e)(ε-elim(G))) in fact, there is a type error: i.e., now ε -elim o e is a function of the type L×T-Gfy → T'-GfZ so we can not apply srec with respect to either T nor T ′ . This can be solved as follows. First, it is easily shown that the structural recursion is defined “uniformly” on monads: Let r = t-Gf ∑ : T-Gf ∑ → T ′ Gf ∑ where ι-G f X  is defined as just the restriction of ι-G ξ . For e: L×T-Gfy → T-GfZ e' : L×T'-Gfy  → T'-Gfz G ∈ T -G f y if e' o (L×i) = i o e then srec T ′ (e′)(i(G)) = i(srec T (e)(G)). Here the equality = means the exact equality rather than strong bisimilarity or bisimilarity. This reduces the setting of the theorem to the case in which T is not necessarily finitary and ι : T → T ′ is the identity—i.e., T (= T r ) is an arbitrary monad whose Kleisli category has an iteration operator—, so that ε -elim is closed in T -G f . This is because, for any e1 ～ e2: L×T-Gfy → T-GfZ there are e'1 ～ e'2: L×T'-Gfy → T'-GfZ such that e' i 0 (L×i) = i 0 e i . We can take such e' i by using some bisimulation generic retraction i* of i. Such i* can be defined in an ad hoc way † 3 : Let G 0 be an ar- bitrary fixed graph in T-Gfy.  For G'  ∈ T'-Gfy, if G' is in T-G f Y , then i*(G ′ )当G ′ , else if G ′ is bisimilar to some graph G in T-Gfy, then i*(G')参与G (G should be chosen), else i* (G') ≡ G 0 Now, in this reduced setting, we will prove the goal in a similar way to Proposition 14. First, we can prove the commutativity of srec with ε-elim: ε-elim(srec(e)(G)) ~s ε-elim(srec(ε-elim o e)(ε-elim(G))). Then, for concluding the proof, it is enough to show the strong-bisimulation genericity of srec (Lemma 16). ● Lemma 16. The structural recursion srec is strong- bisimulation generic: i.e., for e1 ～s e2: L×Gry → GrZ and for G 1 ~ s  G 2  E  G ε χ , the following holds: srec(e1)(G1) ~ srec(e2)(G2) (E GrZxY We will use the following notions and notations in the proof of the above lemma. We write R : A 1 →→ a relation R ⊆ A 1 × A 2 ; e.g.,  the diagram on the left below means that, if α 1 R α 2 , then f 1 (α 1 ) S f 2 (α 2 ) For S : X1 : for G , E fine the relation ～ G 1 ～s T  G 2 if there exists a relation R : V 1 that the right diagram above commutes (i.e., each of the two squares holds). We write simply X for the diagonal relation between X and X , then note that ～ s x : Gry Gf X  is the same as ～ s Proof. Let G i be (V i , B i , I i ). From G i ~s G 2 , there exists R : V 1 → V 2 such that the following diagram commutes.
Next, from the assumption that e 1 ～ s  e 2 , the following diagram commutes.
of V i by oplus yields i.e.,
After that, we can show
and from the left square of the diagram (5) | id z × I 1 | @ cycle( G n | id z × I 2 | @cycle( G ′ 2 ) i.e.,
We give a remark on Equation (7).  As seen above, T c (Y) = G c y (and also G y ) becomes a monad; then cycle becomes an iteration operator in the Kleisli cate- gory.  Furthermore, the iteration operator is uniform on morphisms that come from the Kleisli category Set T via γ , if the iteration operator for T is uniform. The above derivation of Equation (7) from Equation (6) is just the uniformity principle on relations [12].  (Since we need the uniformity of cycle only on functions, so we need the uniformity of iter T only on functions as well.)
Concluding Remark
4
We presented a parameterized calculus λ F G that is an extension of the lambda calculus with finite graph types, the graph constructors, and the structural recursion, for generalizing and extending UnCAL [6].  We presented the semantics of λ F G that has a suitable bisimilarity accommodating ε -edges as well as the termination and finiteness preserving properties.  A further extension of λ FG  is presented in [2]. This paper is based on our previous work [14]. As ex- plained in the introduction, in the previous paper a new calculus—named as λ FG in the previous paper—for or- dered graphs was introduced. The calculus λ FG is not the same as λ FG in the current paper; here, we give the comparison of the current and the previous papers.  In λ FG , the structural recursion is extended from that in the current λ FG ', so that it can transform sibling direction of graphs; hence the expressive power of λ FG is higher than λ FG .  Therefore to extend current work with such sibling transformations is important future work.  Also, in the previous work we focused on ordered graphs, and gave some decidability results on ordered graphs. More- over, in the current paper the existence of a monad and an iteration operator is used as an assumption; while, in the previous paper to define the countable list monad and the iteration operator for the monad was a main contribution. The database community has undertaken a lot of work on graph transformation languages, but most of it has been on graphs up to isomorphism (or equality); there has been little work on graphs up to bisimilarity with consid- ering bisimulation genericity.  However, new semantics for the structural recursion of UnCAL was given in [3]. There has been a lot of work on structural recursion for specific kinds of graphs, such as graphs represented by trees with specific pointers [11][8], and graphs repre- sented by trees with embedded functions [9][7]. How- ever, these attempts seem not so easy to be applied in practice, due to the lack of a natural description of graph transformations where pointers need to be treated spe- cially; also, the notion of bisimilarity is not considered in the above work. In coalgebra theory, i.e., the study of infinitary/cyclic structures, some studies have focused on the finite- ness of graphs.  In [5][28], for every Kripke polyno- mial endofunctor or quantitative functor F , a system- atic way of giving a syntax fully representing all finite F -coalgebras and a sound and complete equational the- ory for bisimilarity were given. The differences between that study and ours are as follows:  (i) The two classes of endofunctors—quantitative functor and ours with ar- bitrary finitary monads—are not comparable; especially, our leading example List( L c ×(-)+Y ) is not a quantita- tive functor. (ii) Our equational theory is restrictive while the equational theory given in that study captures com- pletely the bisimilarity.  (iii) Their study does not treat e-edges, and is not a study for transformations.  (iv) The approaches to syntax are different: The both can express arbitrary finite coalgebras, but there seems no composi- tional translations between their and our graph represen- tation systems, and comparison of expressive power of open terms is not obvious.  Also, their approach is in a guarded style, by which the unique fixed point operator can be used; while ours does not require guardedness, and require an iteration operator instead. In [1][20], the authors studied categorical properties of the set of finite coalgebras, and characterized it as a final locally finite coalgebra .  The class of endofunctors for coalgebras in that study is wider than ours; some of the results are applied and inspire our work.  In that study, there is no consideration for finiteness-preserving struc- tural recursion. The finality among locally finite coalge- bras is a kind of corecursion and has a similar problem to that of corecursion; i.e., to assure finiteness-preservation, we have to check finiteness of infinite graphs locally, the automation of which seems difficult. The general treatment for ε -edges with iteration oper- ators in the current paper was hinted at in [16]. Although there was no consideration of ε -edges itself in that study, the author showed that the trace semantics for some kinds of coalgebra induces iteration operators by forgetting the length of trace paths; the resulting iteration operators can be regarded as ε -elimination.  The countable list monad is not treated in that paper; it does not satisfy the assump- tion of the theorem in that paper. In [19], the authors studied ε -elimination for wighted automata.  The kinds of automata treated in their paper are parametrized by certain semirings, and do not include our ordered case ( List-graphs). Also, their approach to spec- ifying weighted automata is different from ours.  They define first some class of weighted ε -automata, and then they restrict it to "valid" ones with some procedure; while our graphs are "valid" from first.  As a main contribu- tion, they give an algorithm for removing ε -transitions. It seems interesting future work to compare their and our general automaton/graph models and merge each advan- tages. [ 1 ] Adámek, J., Milius, S., and Velebil, J.: Iterative algebras [ 9 ]  Fegaras, L. and Sheard, T.: Revisiting Catamorphisms over Datatypes with Embedded Functions (or, Programs from Outer Space), POPL, ACM Press, 1996, pp.  284–294. [10] Haghverdi, E.: A Categorical Approach to Linear Logic, Geometry of Proofs and Full Completeness , PhD Thesis, University of Ottawa, 2000. [ 11 ] Hamana, M.: Initial Algebra Semantics for Cyclic Shar- ing Structures, TLCA , LNCS 5608, 2009, pp.  127–141. [12] Hasegawa, M.: The Uniformity Principle on Traced Monoidal Categories, Electr. Notes Theor. Comput. Sci., Vol. 69(2002), pp. 137–155. [13] Hasuo, I.: 2011. personal communication. [14] Hidaka, S., Asada, K., Hu, Z., Kato, H., and Nakano, K.: Structural Recursion for Querying Ordered Graphs, ICFP 2013, to appear , March 2013. [15] Hidaka, S., Hu, Z., Inaba, K., Kato, H., Matsuda, K., and Nakano, K.: Bidirectionalizing Graph Transformations, ICFP 2010, ACM Press, 2010, pp.  205–216. [16] Jacobs, B.: From Coalgebraic to Monoidal Traces, Electr. Notes Theor. Comput. Sci. , Vol. 264, No. 2(2010), pp. 125–140. [17] Kakutani, Y.: Duality between Call-by-Name Recur- sion and Call-by-Value Iteration, CSL , LNCS, Vol. 2471, Springer, 2002, pp. 506–521. [18] Kelly, G. M.: Structures defined by finite limits in the enriched context, I, Cahiers Topologie Géom. Différentielle , Vol. 23, No. 1(1982), pp. 3–42. [19] Lombardy, S. and Sakarovitch, J.: The Removal of Weighted ε -Transitions, Implementation and Application of Automata , LNCS, Vol. 7381, Springer Berlin Heidelberg, 2012, pp. 345–352. [20]  Milius, S.:  A Sound and Complete Calculus for Fi- nite Stream Circuits, LICS , IEEE Computer Society, 2010, pp. 421-430. [21]   Milner, R.: Communicating and Mobile Systems: the π- calculus , Cambridge University Press, 1999. [22]  Mitchell, J. C.:  Foundations for programming lan- guages , Foundation of computing series, MIT Press, 1996. [23] Moggi, E.: Computational Lambda-Calculus and Mon- ads, LICS , IEEE Computer Society, 1989, pp.  14–23. [24] Plotkin, G. and Power, J.:  Algebraic Operations and Generic Effects, Applied Categorical Structures , Vol. 11(2003), pp. 69–94. [25] Robertson, E. L., Saxton, L. V., Gucht, D. V., and Van- summeren, S.: Structural Recursion as a Query Language on Lists and Ordered Trees, Theory of Computing Systems , Vol. 44, No. 4(2009), pp. 590–619.
and Nakano, K.: Toward Bidirectionalization of ATL with GRoundTram, ICMT , LNCS, Vol. 6707, Springer, 2011, pp. 138–151. [28] Silva, A., Bonchi, F., Bonsangue, M. M., and Rutten, J. J. M. M.: Quantitative Kleene coalgebras, Inf. Comput. , Vol. 209, No. 5(2011), pp. 822–849. [29] Simpson, A. K. and Plotkin, G. D.: Complete Axioms for Categorical Fixed-Point Operators, LICS , 2000, pp. 30– 41. [30] Sokolova, A.: Coalgebraic Analysis of Probabilistic Systems , PhD Thesis, TU Eindhoven, 2005.
Let T be a monad and iter be an uniform iteration op- erator in Set T . We define ε -elimination for finite T | fin- graphs so that the result graph is equal to one obeying Definition 5. Let G = (V, B, I) be a finite T | fin-graph in T-G ξ . Since V is finite and T | fin is finitary by definition, there exists a finite subset L ′ ⊂ L ε and a function B ′ such that the following diagram commutes.
V+(L'×V+Y) is a hence, Now finite set; T|fin(V+(L'×V+Y)) = T(V+(L'×V+Y)). We can therefore apply the iteration operator iter to B ′ . Let us define B ′′ as the composition of
and 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 eas- ily checked that the above ε -elim( G ) is exactly equal to ε-elim( G ) in Definition 5. When a finitary monad T with an extension for ε- elimination T ′ is given, T ′ plays the role of T above. The condition that T is finitary can be used to show that ι : T → T ′ can be decomposed into the inclusion T ′ | fin ⊆ T ′ and some (necessarily injective and unique) monad morphism T → T ′ | fin