日本ソフトウェア科学会第 39 回大会 (2022 年度) 講演論文集

A functional language with graphs asﬁrst-class data
Jin Sano, Kazunori Ueda
Graphs are a generalized concept that encompasses more complex data structures than trees, such as difference lists, doubly-linked lists, skip lists, and leaf-linked trees. Normally, these structures are handledwith destructive assignments to heaps, as opposed to a purely functional programming style. We proposeda new purely functional language, λGT , that handles graphs as immutable, ﬁrst-class data structures witha pattern matching mechanism based on Graph Transformation. Since graphs can be more complex thantrees and require non-trivial formalism, the implementation of the language is also more complicated thanordinary functional languages. λGT is even more advanced than the ordinary graph transformation systems. We implemented a reference interpreter, a reference implementation of the language. We believe thisis usable for further investigation, including in the design of real languages based on λGT . The interpreteris written in only 500 lines of OCaml code.

1 Introduction
λGT is a functional language to support graphs
as ﬁrst-class data. λGT enables us to construct andpattern match graphs as well as Algebraic Data
Types. The key features of λGT are the following.
Data structures more complex than trees. Algebraic Data Types (ADT) in purely functional languages can only represent tree structures. On theother hand, in λGT , not just lists and trees but also
diﬀerence lists, skip lists [20], doubly linked lists,
leaf linked trees, and threaded trees, etc, can behandled succinctly.
Graphs as ﬁrst-class data. Not pointers/references to a global heap but graphs are ﬁrst-class,i.e., values, in this language. That is, graphs canbe dynamically created, graphs can be bound tovariables, be input and output of functions, and be∗ グラフを第一級に扱う関数型言語

This is an unrefereed paper. Copyrights belong to
the Authors.
Jin Sano, Kazunori Ueda, 早稲田大学基幹理工学研究科
情報理工・情報通信専攻, Dept. of Computer Science
and Communications Engineering, Graduate Schoolof Fundamental Science and Engineering, Waseda
University.

dynamically discarded.
Powerful pattern matching mechanism. Whenmatching ADTs in functional languages, we canonly use the patterns that allow only the matchingof a ﬁxed region near the root of the structure. On
the other hand, we enabled more powerful matching based on Graph Transformation [6] [21].
Syntax-driven semantics. To establish the semantics of λGT , we incorporated that of HyperLMNtal [31] [25] to call-by-value λ calculus. Unlike
deﬁnitions common in conventional graph transformations, such as the triplet of a set of vertices, a
set of sets of vertices (hyperlinks), and a labeling
function, the graphs in HyperLMNtal can be constructed compositionally from sub-graphs. These
syntax and semantics follow the style of π-calculus[23] rather than traditional algebraic graph transformation formalism. This make it easier to incorporate graphs into λ-calculus.
Type System. The type system of λGT incorporates graph grammar and use inﬁnite decent. However, in this paper, we focus on the language anddo not mention much about the type system [26].
First-class functions. Functions are ﬁrst-classdata in λGT as well as in other functional languages.
Immutability. Graphs are immutable in this lan-

guage. We do not rely on destructive rewriting
but employ immutable composing and decomposing with pattern matching.
Contributions
λGT can handle graphs. Since graphs can be
more complex than trees, it requires non-trivial formalism. Thus its implementation is also more complicated than the ordinary functional languages.
λGT is even more advanced than the ordinary
graph transformation systems. Graph transformation systems rewrite one global graph with rewriting rules. On the other hand, in λGT , graphs are
local values that can be decomposed by patternmatching with possibly multiple wildcards, passed
as inputs of functions, and composed to constructlarger graphs from the subgraphs. Therefore, how
to trivial to implement the language is not trivial.
Thus, we implemented a reference interpreter,a reference implementation of the language. We
believe this is usable for further investigation, including in the design of real languages based on
λGT . The interpreter is written in only 500 lines ofOCaml [14] code, which is strikingly concise†1 .
Structure of the paper
The rest of this paper is organized as follows. Section 2 introduces λGT informally. Section 3 gives
the formal syntax and the operational semanticsof λGT . In Section 4, we give more detailed explanation about the examples we have introduced
informally in Section 2. Section 5 describes why
we need such an interpreter. Section 6 explains theimplementation. Section 7 discusses related work
and indicates our expected future work.

that points to the address of the last node (sentinelnode) of the list. Adding a new element to the list
can be done with the destructive assignment to thesentinel node with a new number and the address
to the newly created sentinel node. We also need
to update last ptr to point to the new sentinelnode. These low-level operations are tiresome andprone to errors, e.g. we can easily forget to updatelast ptr.
sentinelhead ptr
12
34
last ptr
In λGT , such data structure can be abstracted toa diﬀerence list ; a list with a link to the last node,as follows. Adding a new element to the list can beunderstood as concatenating a singleton list to the
list.
C

C

C

1

2

3

(1)

We can represent a program with a function thattakes two diﬀerence lists and returns the concatenated diﬀerence list as the following. Notice thatthe input and output of the function are not pointers to a global heap but graphs as local values. λGT
can handle graphs as ﬁrst-class data (i.e., values)
in such a manner.

λ

y

x

y

x

C

C

1

2

2 Informal introduction to λGT
In this section, we introduce λGT informally. We
will give the formal syntax and semantics of thelanguage later in Section 3.
Consider the case where we want to enableadding an element to the end of a list eﬃciently.
In imperative languages, we will prepare a pointer†1 Thesourcecode
isavailableathttps://github.com/sano-jin/lambda-gt-alpha.
We have also implemented a visualizing toolthat runs on a browser, which is available athttps://sano-jin.github.io/lambda-gt-online/.

−→val

y

λ

C
C
1

−→val

C

C

1

2

y

2

−→

nodes

r1

C
r2

Fig. 1

nodes

−→

nodes

ditional functional languages with Algebraic Data
Types. With Algebraic Data Types, normally, only
the root of a tree can be matched. Taking the lastelement of a list needs iterating from the head ofthe list. On the other hand, in λGT , we can pop
the last element in one step.

nat
x

case

Production rules for a diﬀerence listyAlthough we will not discuss in detail in this paper, we have also proposed a new type system forthe language in [26], which is extended from thetyping framework for graph transformation based
languages [8] [9] [32]. In this type system, the typesof graphs are deﬁned using graph grammar. For
example, the type of a diﬀerence list can be deﬁned
using the production rules in Figure 1.
Informally, we can say graph has a type if we
can obtain the graph from the type applying production rules zero or more times. The following
example shows that we can obtain a diﬀerence list
with two elements using the production rules.

of
C

→

Some (

→

None

y

,

z

|

otherwise

Here, we used an option type (Some and None)and a tuple to return both the popped list andthe element. λGT we will describe in the next section does not have option type and tuple explicitly.
However, they can be easily introduced directly tothe language or encoded without extension.
For example, Some x can be encoded as Some
x

nodes

⇝r2

C

and (

nodes

y

z

,

,

) as

⇝r1

C

.

y

nat

⇝r2

)

z

C

If we have bound (1) to

x

(

C

C

1

2

nodes

z

, then the ob).

tained result will be
nat

nat

C

C

nat

nat

Here, ⇝r is a HyperLMNtal reduction using therule r, where the formal semantics is described in[26] [25]. In [26], we have shown that the function
has a type that takes two diﬀerence lists and returns a diﬀerence list.
λGT can not only handle graphs as input/output of functions, but also able to pattern matchgraphs. This is more powerful than those of tra-,3

The values in λGT are undirected graphs. However, it will be suitable for the links in the graphs
to be directed when compiling to an impure functional language program using reference types. In
λGT , we can easily encode directed edges. The links
in the diﬀerence lists we have introduced can be regarded as directed edges from left to right or fromup to down.
C

C

C

1

2

3

(1 − b)

−→

nodes

−→

nodes

Nil

r1

r1

−→

nodes

C1

nodes

r2

C2

nodes

r3

Fig. 2

nat

r2

−→

nodes

F

−→

forks

forks

C

−→

nodes

r3

forks

−→

X

nodes

Production rules for 2-level skip list

However, if the list consists only of forward pointers, it will be diﬃcult to match backward eﬃciently
such as matching to the last node of the list. Therefore, we consider making it a doubly linked list as
the following. We can easily rewrite the program
to handle this.
C

C

C

1

2

3

forks

nodes

r4

Fig. 3

Production rules for an arbitrary-levelskip list

NN

λGT can handle not only diﬀerence lists but also
various data structures. Skip list is a list with extra
edges, as shown in Figure 4. The extra edges canbe used to make searching more eﬃcient. In λGT ,the skip list of level 2 can be expressed as shown in
Figure 5, using the production rules in Figure 2.
Suppose we want to represent a skip list of arbitrary level. A skip list using a list of links to thenodes to be skipped can be represented as in Figure 6. Figure 3 shows the production rules for such
lists. The rules exploit diﬀerence lists to link to askipped node after Forking. The list of skipping
links is terminated with the neXt atom.
For operations that cannot be performed by simply decomposing and composing graphs, we canprepare atoms to behave as markers and use themfor matching. For example, a map function thatapplies a function to the element of the leaves in aleaf-linked tree can be expressed as Table 7.
Here, if+1

is a function that returns the suc-cessor of a given number, and we have bound

N

L

N

1

L

L

2

3

L

L

4

5

to

t

, then eval-uating the program will result in
N

.

N
L
2

N
N

L

L

3

4

L

L

5

6

3 The syntax and semantics of λGT
Throughout the paper, we use the following syntactic conventions.
→−
For some syntactic entity E, E stands for a sequence E1 , . . . , En for some n (≥ 0). The length of→−→−
the sequence E is denoted as | E |.
For some syntactic entities E, p and q, a substitution E[q/p] stands for E with all the (free) occurrences of p replaced by q. An explicit deﬁnition

head

1
Fig. 42

3

4

5

2-level skip list with heaps and pointers

C2

C1

C2

C1

C2

1

2

3

4

5

Fig. 5Nil

2-level skip list in λGT

F
F
C
1

X

F
C

X

2

C
3

Fig. 6

X

C
4

X

C

X

5

n-level skip list (n = 3)

will be given if the substitution should be captureavoiding. For substitutions of hyperlinks, we use aslightly diﬀerent syntax Ehq/pi for clarity.
3. 1 Syntax of λGT
The λGT language is composed of the following
syntactic categories.
• X denotes a Link Name.
• C denotes a Constructor Name.
– Cons, Fork, etc.
• x denotes a Graph Context Name.
λGT is designed to be a small language focusing
on handling graphs. The syntax of λGT is given in
Figure 8.
Graph Template. 0 denotes an empty graph. A→−→−
graph context x[ X ], where X is a sequence of different links, is a wildcard in pattern matching corresponding to a variable in functional languages. It→−→−
matches any graph with free links X . v ( X ) is anatom. Intuitively, it is a node of a data structure→−with label v and links X . (T, T ) is a multiset union.
νX.T hides the link X. We call a link free link, if
it is not hidden. The set of the free links in T isdenoted as fn(T ). The links that do not occur free
are called local links.
→−
Atom name. C( X ) is a constructor atom. For

example, Nil(X), Cons(Y, Z, X), etc.
The λ→−→−
abstraction atoms have the form (λ x[ X ].e)( Y ).
Intuitively, the atom takes a graph with free links→−→−
X , binds it to the graph context x[ X ], and returns
the value obtained by evaluating the expression ewith the bound graph context. An atom X ▷◁ Y ,called a fusion, fuses the link X and the link Y intoa single link.
Expression. T is a graph template we have deﬁned so far. Notice that the corresponding concepts of variables and λ-expressions have alreadyincorporated as graph contexts and λ-abstraction
atoms in a graph template. (case e1 of T →e2 | otherwise → e3 ) evaluates e1 , checks whether
this matches the graph template T , and reduces to
e2 or e3 . (e1 e2 ) is an application.
Value. G stands for a value of the language λGT ,which is T not containing graph contexts. Henceforth, we may call both G and T a graph when the
distinction is not important.
Although we omitted in the ﬁgures in the previous section, graphs have free links and the links(edges) atoms (nodes) are ordered. This is diﬀerent
from ordinary graphs in graph theory. We believethat the graph in λGT is a structure that naturally
incorporates PL concepts and is easy to handle in

let

map

f

let rec

helper

case

=

x

=

x′

of

x′

z′

let
y

=

f

z

in

→

L
m

z

y

helper
L
z′

|

→

y

m

y

m
in
x

helper
m
in
map

+1

t

Fig. 7A map function for leaf linked trees

programming. Also, the graph is composed of subgraphs, in which we can naturally use structural
induction, which is advantageous in veriﬁcation.
The graphs in λGT is undirected. However, since
the edges of an atom are ordered, we can easily encode directed graphs by stipulating that the ﬁnal
argument of atoms is the head of the links. All theexamples in this paper can be interpreted as such.
3. 2 Structural Congruence
Structural congruence ≡ deﬁnes what graphs T

or G are essentially the same.
Deﬁnition 3.1 (Structural Congruence). We deﬁne the relation ≡ on graphs as the minimal equivalence relation satisfying the rules shown in Figure 9.
Here, GhY /Xi is a hyperlink substitution that replaces all free occurrences of X with Y . Notice if afree occurrence of X occurs in a location where Y
would not be free, α-conversion may be required.
Two graphs related by ≡ are essentially the sameand are convertible to each other in zero steps.
(E1), (E2) and (E3) are the characterization ofExpression

e

::=
|
|

T
case e of T → e | otherwise → e
(e e)

Graph
Case
Application

Graph Template

T

::=
|
|
|
|

0
→
−
x[ X ]→−v (X )(T, T )νX.T

NullGraph context
Atom
Molecule
Hyperlink creation

Atom Name

v

::=
|
|

C
▷◁
→
−
λ x[ X ].e

Constructor name
FusionAbstraction

Value

G

::=

→
−
0 | v ( X ) | (G, G) | νX.G

GraphFig. 8

Syntax of λGT

molecules as multisets. (E4) and (E5) are structural rules that make ≡ a congruence. (E6) and(E7) are concerned with fusions. (E7) says thata closed fusion is equivalent to 0. (E6) is an absorption law of ▷◁, which says that a fusion canbe absorbed by connecting hyperlinks. Because of
the symmetry of ▷◁, (E6) says that an atom canemit a fusion as well. (E8), (E9) and (E10) areconcerned with hyperlink creations. We give two
important theorems showing that the symmetry of▷◁ and α-conversion can be derived from the rulesof Figure 9.
Theorem 3.1 (Symmetry of ▷◁).
X ▷◁ Y ≡ Y ▷◁ X
Proof. See Chapter 3 of [24].
Thus, (E6) can be used also when we have a local
link on the right-hand side of ▷◁.
Theorem 3.2 (α-conversion of hyperlinks).
Bound link names are α-convertible, i.e.,
νX.G ≡ νY.GhY /Xi where Y ∈/ fn(G)
Proof. See Chapter 3 of [24].
Using structural congruence (syntax-directed approach) instead of graph isomorphism or bisimulation is not a common approach in graph transformation formalisms. However, we believe using
syntax-directed approach makes the semantics a loteasier than adopting the other approaches, since(E1)(0, G) ≡ G(E2)(G1 , G2 ) ≡ (G2 , G1 )(E3) (G1 , (G2 , G3 )) ≡ ((G1 , G2 ), G3 )(E4)
G1 ≡ G2 ⇒ (G1 , G3 ) ≡ (G2 , G3 )(E5)
G1 ≡ G2 ⇒ νX.G1 ≡ νX.G2(E6) νX.(X ▷◁ Y, G) ≡ νX.GhY /Xi
where X ∈ fn(G) ∨ Y ∈ fn(G)(E7) νX.νY.X ▷◁ Y ≡ 0(E8)
νX.0 ≡ 0(E9)
νX.νY.G ≡ νY.νX.G(E10) νX.(G1 , G2 ) ≡ (νX.G1 , G2 )where X ∈/ fn(G2 )Fig. 9Structural congruence on graphs

the λ-calculus and many other computational models derived from the λ-calculus are are deﬁned as
Structural Operational Semantics [19].
→−The pair of the name p and the arity n = | X | of→−a graph context x[ X ] is referred to as the functor †2of the context and is written as x/n.
Deﬁnition 3.2 (Free functors of an expression).
We deﬁne free functors of an expression e, ﬀ (e),in Figure 10. Free functors are not to be confusedwith free link names.
†2 Synonym of function symbol and function object;
not to be confused with functors in category theory.

ﬀ (case e1 of T → e2 | otherwise → e3 ) =ﬀ (e1 ) ∪ (ﬀ (e2 ) \ ﬀ (T )) ∪ ﬀ (e3 )ﬀ ((e1 e2 ))→−ﬀ (x[ X ])→−ﬀ (v( X ))→−→−ﬀ ((λ x[ X ].e)( Y ))ﬀ ((T1 , T2 ))ﬀ (νX.T )Fig. 10

=
=
=
=
=
=

ﬀ (e1 ) ∪ ﬀ (e2 )→−{x/| X |}∅→−ﬀ (e) \ {x/| X |}ﬀ (T1 ) ∪ ﬀ (T2 )ﬀ (T )

Free functors of an expression

3. 3 Operational semantics of λGT
3. 3. 1 Graph Substitution
We deﬁne graph substitution, which replaces agraph context whose functor occurs free by a given
subgraph. The substitution avoids clashes with any
bound functors by implicit α-conversion (captureavoiding substitution). Graph substitution is not
to be confused with hyperlink substitution. Intuitively, hyperlink substitution just reconnects hyperlinks. On the other hand, graph substitution performs deep copying at the semantics level(though it could or should be implemented withsharing whenever possible).
We deﬁne capture-avoiding substitution θ of a→−graph context x[ X ] with a template T in e, written→−e[T /x[ X ]], as in Figure 11. The deﬁnition is standard except that it handles the substitution of thefree links of graph contexts in the third rule.
3. 3. 2 Matching
We say that T matches a graph G if there exists agraph substitution θ such that G ≡ T θ. For example, Figure 12 shows the matching of a diﬀerence
list.
Note that the matching of λGT is not subgraphmatching (as is standard in graph rewriting systems) but the matching with the entire graph G(as is standard in pattern matching of functional
languages). For this reason, the free link names
appearing in a template T must exactly match thefree links in the graph G to be matched. This is tobe contrasted with free links of HyperLMNtal rulesthat are eﬀectively α-convertible since the rules canmatch subgraphs by supplementing fusion atoms ([25]).

(T1 , T2 )θ

=(T1 θ, T2 θ)(νX.T )θ= νX.T θ→−→−(x[ X ])[T /y[ Y ]] =→−→−− /Y →− i
if x/| X | = y/| Y | then T hX1 /Y1 i . . . hX|→
X|
|Y |
→
−
else x[ X ]→−→−(v( X ))θ= v( X )
−
→
→
−
→
−
((λ x[ X ].e)( Z ))[T /y[ Y ]] =
→
−
→
−
→
−
→
−
if x/| X | = y/| Y | then (λ x[ X ].e)( Z )
→
−
→
−
→ −
−
→
else if x/| X | ∈/ ﬀ (e) then (λ x[ X ].e[T /y[ Y ]])( Z )
→
−
→
−
→
−
→ −
−
→
else (λ z[ X ].e[z[ X ]/x[ X ]][T /y[ Y ]])( Z )→−where z/| X | ∈/ ﬀ (e).
(case e1 of T → e2 | otherwise → e3 )θ =case e1 θ of T → e2 θ | otherwise → e3 θ
(T1 T2 )θ

=(T1 θ T2 θ)

Fig. 11Graph Substitution

3. 3. 3 Reduction
The evaluation strategy of λGT is call-by-value.
In order to deﬁne the small-step reduction relation, we extend the syntax with evaluation contexts
deﬁned as follows: E ::= [] | (case E of T →e | otherwise → e) | (E e) | (G E) | T . As usual,
E[e] stands for E whose hole is ﬁlled with e.
We deﬁne the reduction relation in Figure 13.
Rd-Case1 and Rd-Case2 are for matching graphs
we have explained so far. Rd-β is the key relationthat applies a value to a function. The deﬁnition isstandard except that (i) we need to check the correspondence of free links and (ii) we use graph substitution but the normal substitution in λ-calculus.
The Rd-App1, Rd-App2, and Rd-Ctx are the sameas in the call-by-value λ-calculus..

4 Programs examples in detailThis section describes some of the programs wehave introduced informally in Section 2 in detailwith the formal semantics in order to discuss theimplementation algorithm in later sections.
We introduce some abbreviations before moving
on to the examples.
Deﬁnition 4.1 (Abbreviations). We introduce thefollowing abbreviation schemes:
1. A nullary atom v () can be simply written asv.
2. Term Notation:
νXn .(v1 (. . . , Xn , . . . ), v2 (X1 , . . . , Xn )) can be

X

C

C

Y

X

x

C

Y

[

Z

C

]

W/
Z

1

2

2

≡

G
νZ.(
νZ1 .(Cons(Z1 , Z, X), 1(Z1 )),νZ2 .(Cons(Z2 , Y, Z), 2(Z2 ))
)

x

W

1

T

θ

νZ.(
[
]
/
x[Z, X],
νZ1 .(Cons(Z1 , Z, W ), 1(Z1 )) x[Z, W ]νZ2 .(Cons(Z2 , Y, Z), 2(Z2 )))Fig. 12

Example of the graph matchingG ≡ Tθ
Rd-Case1(case G of T → e2 | otherwise → e3 ) −→val e2 θMatching succeeded¬∃θ.G ≡ T θ
Rd-Case2(case G of T → e2 | otherwise → e3 ) −→val e3

Matching failed→−
fn(G) = { X }→−→−→ Rd-β−((λ x[ X ].e)( Y ) G) −→val e[G/x[ X ]]Beta reduction

e1 −→val e′1
Rd-App1(e1 e2 ) −→val (e′1 e2 )e −→val e′
Rd-App2(G e) −→val (G e′ )Fig. 13e −→val e′
Rd-CtxE[e] −→val E[e′ ]Reduction relation of λGT

written as v1 (. . . , v2 (X1 , . . . , Xn−1 ), . . . ). For
example, a diﬀerence list with two elements,
νZ.(
νZ1 .(Cons(Z1 , Z, X), 1(Z1 )),,νZ2 .(Cons(Z2 , Y, Z), 2(Z2 )))can be abbreviated as Cons(1, Cons(2, Y ), X).
3. We abbreviate νX1 . . . . νXn .G to νX1 . . . Xn .G.
4. Application is left-associative.
5. Parentheses can be omitted if there is no ambiguity.
→−
6. let x[ X ] = e2 in e1 reduces in one step to→−e1 [e2 /x[ X ]].
Here, (1) and (2) also apply to graph contexts.
For the sake of explanation, the graph of evaluation results may be rewritten using the structuralcongruence rules.

let append [Z] =(λ x[Y, X].
(λ y[Y, X].
νZ.(x[Z, X], y[Y, Z]))(Z))(Z)in append [Z] Cons(1, Y, X) Cons(2, Y, X)
Fig. 14

Append operation on diﬀerence lists

Graphs as inputs and output of a function
For example, we can describe a program to append two singleton diﬀerence lists as in Figure 14.
We show the whole process of reduction of thisprogram in Figure 15, whose process is alreadyshown graphically in Section 2.
Firstly, the λ-abstraction atom is bound to
the graph context append [Z]†3 . The bound λ†3 It may appear that the Z of append [Z] does notabstraction atom is a function that takes two difference lists, both having X and Y as free links,
and returns their concatenation also having X andY as its free links.
Pattern matching graphs
Figure 16 shows the program, a slightly simpliﬁed version of the program introduced in Section 2,that matches the diﬀerence list and removes thelast node. If Cons(1, Cons(2, Y ), X) is bound tox[Y, X], this will result in Cons(1, Y, X).
Without the term-notation abbreviation, thegraph template used in the matching can be written
as νW.(y[W, X], Cons(Z, Y, W ), z[Z]). The matching in this template proceeds as the following,
which is mostly the same as we have explained in
Figure 12 in the previous section.
Cons(1, Cons(2, Y ), X)≡ νW Z.(y[W, X], Cons(Z, Y, W ), z[Z])[Cons(1, W, X)/y[W, X], 2(Z)/z[Z]]absorbed and does not appear explicitly in the return value. Consider the program in Figure 17 thatcycles the elements by taking the last node of thediﬀerence list and reconnecting it to the head. Fusion can be absorbed in the return value in thisprogram.
If Cons(1, Y, X) is bound to x[Y, X], this will
result in Cons(1, Y, X).
The pattern matching proceeds in the same way as in the previous program. Thus we will obtain the substitution [W ▷◁ X/y[W, X], 1(Z)/z[Z]]. Substituting
the graph template on the right-hand side of → will
result in Cons(1, Y, X) as follows.
νW Z.(Cons(Z, W, X), z[Z], y[Y, W ])[W ▷◁ X/y[W, X], 1(Z)/z[Z]]= νW Z.(W ▷◁ X, Cons(Z, Y, X), 1(Z))≡ Cons(1, Y, X)
The program using the map function for leaf-linked

trees in Figure 7 in Section 2 also uses the matchingwith supplying fusions.
Such fusion-complementary matching does not
In order to implement the language precisely, we
appear in ordinary ADT matching in functional
also need to consider the corner case; for example,
languages. Also, formalization using fusions is not
the matching which exploits fusion.
common in ordinary graph transformations, as well
Consider if a singleton list νZ.(Cons(Z, Y, X), 1(Z)) as the tools based on them. Thus, it is a challenge
is bound to x[Y, X]. We need a sub-graph that has
to deal with it.
free links W and X, the free links of the graph
5 Reference interpreter: Uses and Recontext y[W, X] in the graph template, which does
quirements
not exist in the list. Thus the matching would not
We implement a reference interpreter, a reference
proceed without supplying sub-graphs.
implementationof the language, which has several
This time, we need to ﬁrstly supply a fusion atom.
potentialuses
asfollows.
Then we can match y[W, X] to the supplied fusionFor
researchofthe design of real languages. λGT
atom. The matching proceeds as follows.
is a computational model with a new concept.
Cons(1, Y, X)
While the operational semantics are deﬁned, this≡ νW Z.(W ▷◁ X, Cons(Z, Y, X), 1(Z))
only deﬁnes the behavior as a computational model,= νW Z.(y[W, X], Cons(Z, Y, W ), z[Z])and does not deﬁne how we can implement data
[W ▷◁ X/y[W, X], 1(Z)/z[Z]]structures and perform eﬃcient pattern matching.
Therefore, the program will result in Y ▷◁ X.
It is ultimately up to the language designer to decide how to implement this.
Even if a bound fusion atom is used, it may be
If general hypergraphs are handled purely andno restrictions are placed on pattern matching toplay any role in this example. However, sucha link becomes necessary when the append isthem, an eﬃcient implementation will be diﬃcult.
made to appear in a data structure (e.g., as in
Therefore, in designing a real language, it is reνZ.(Cons(Z, Y, X), append [Z])). This is why λalistic to put in appropriate restrictions while usabstraction atoms are allowed to have argument
ing the type system as support. However, theselinks. Once such a function is accessed and βconstraints should not exclude practicality. Actual
reduction starts, the role of Z ends, while the freeprogramming using the reference interpreter is uselinks inside the abstraction atom start to play key
roles.
ful to determine whether or not it is practical tolet append [Z] = (λ x[Y, X]. (λ y[Y, X]. x[y[Y ], X])(Z))(Z)in append [Z] Cons(1, Y, X) Cons(2, Y, X)
−→val
−→val
=
−→val
=

Fig. 15(λ x[Y, X]. (λ y[Y, X]. x[y[Y ], X])(Z))(Z) Cons(1, Y, X) Cons(2, Y, X)(λ y[Y, X]. x[y[Y ], X])(Z)[Cons(1, Y, X)/x[Y, X]] Cons(2, Y, X)(λ y[Y, X]. Cons(1, y[Y ], X))(Z) Cons(2, Y, X)(Cons(1, y[Y ], X))(X)[Cons(2, Y, X)/y[Y, X]]
Cons(1, Cons(2, Y ), X)

An example of reduction: append operation on diﬀerence lists

let pop[Z] =(λ x[Y, X].
case x[Y, X] ofy[Cons(z, Y ), X] → y[Y, X]| otherwise → x[Y, X])(Z)
in pop[Z] x[Y, X]
Fig. 16

Pop operation on a diﬀerence list

let rotate[Z] =(λ x[Y, X].
case x[Y, X] ofy[Cons(z, Y ), X] → Cons(z, y[Y ], X)| otherwise → x[Y, X])(Z)
in rotate[Z] x[Y, X]
Fig. 17

Rotate operation on a diﬀerence list

include constraints.
For testing future implementations. We intend
to build a more eﬃcient implementation in the future. However, since we are dealing with complex
data structures, we need to do low-level programming making full use of pointers at the meta-level,
which is not easy. Therefore, it is assumed thatdevelopment will proceed with testing. To test theresults, it is useful to have an implementation that
outputs the correct results, even if the execution
eﬃciency is poor.
To develop applications using λGT . It is betterto have a runtime to ﬁnd and test programs thatcan be written concisely using λGT .
To develop tools. This study pioneers a method
for representing graphs in terms of terms, and gives
a semantics based on them. This is advantageous interms of semantics and veriﬁcation. However, it is
not clear whether it is easy for users to write. If weare dealing with graphs, it is considered more intuitive to be able to draw them graphically. Therefore, the editor of λGT may be GUI-based. It would
be advantageous to be able to actually run the tool
when developing tools．

6 Implementation
6. 1 Overview
The goal of this study is to implement as simple
as possible, without regard to eﬃciency. Our implementation consists of only 500 lines of OCaml code
as shown in Table 1. This is about half of the lines
of a reference interpreter of a graph transformationbased language GP 2 [1], which is about 1,000 linesof Haskell code [2]. This is striking considering that
our language does not only support graph transformation but we have incorporated it into a functional language without sacriﬁcing functional language features such as higher-order functions.
The interpreter is composed of pure functions
without destructive operations. We use lists to handle graphs.
6. 2 Parser
Our current implementation is not intended toprovide a complete language that can be used inreal-world programming. The ﬁnal design of theconcrete syntax is left to the designer of the actual
language. There is even a possibility of providing
a graphical UI and not allowing the language to be
written in texts. In this study, we gave a concrete
syntax that is easy to parse. The syntax is not sophisticated enough for programmers to write easily.
However, this still satisﬁes our purpose.

Table 1

LOC of the interpreter

File

LOC

eval/match ctxs.ml
parser/parser.mly
parser/lexer.mll
eval/syntax.ml
eval/eval.ml
eval/pushout.ml
eval/match atoms.ml
eval/preprocess.ml
parser/syntax.ml
eval/match.mlparser/parse.ml
bin/main.ml

79
70
51
47
43
42
36
36
16
11
4
3

SUM

438

Concrete syntax• Link name starts from a capital letter with anunderscore as a preﬁx.
• ν is written as nu.
→−→−• λ-abstraction atom (λ x[ X ].e)( Y ) is writtenwith < and > as follows.
<\ x[_X1, ..., _Xn]. e> (_Y1, ..., _Ym).
• The graph templates appears in expressions
should be surrounded with { and }.
6. 3 Preprocessing graphs
In our implementation, values, i.e., graphs, arerepresented with lists of atoms without link creations inside; i.e., prenex normal form. We callthem host graphs. Links are classiﬁed into free links
with string names and local links α-converted to
fresh integer ids. In this paper, we denote Li forthe local link with the id i and FX for the free linkwith the name X.
Fusion atoms with local link(s) are absorbed beforehand. Currently, we assign numbers startingfrom 1,000 to the local links in the template to
avoid conﬂict with the host graphs whose local links
are assigned numbers starting from 0†4 .
The interpreter transforms graph templates toa pair of the list of the atoms and the list of thegraph contexts. For example, the graph templatey[Cons(z, Y ), X], the pattern in the Figure 16, is†4 This may be too ad-hoc solution but is simple anddoes work in our examples.

transformed into the following.
h [Cons(L1001 , FY , L1000 )] ,(1)
[y [L1000 , FX ] , z [L1001 ]] i
Whereas the host graph Cons(1, Y, X) is transformed into the following.
[Cons(L0 , FY , FX ), 1(L0 )](2)This preprocessing occurs every time evaluating
the expression. This can be easily optimized to bememorized. However we focused more on the simplicity of the implementation.
6. 4 Matching graphs
The interpreter ﬁrstly tries to match all theatoms in the template to the host graph and thenmatch the graph contexts to the rest of the hostgraph. The interpreter backtracks if the consequent
matching failes.
6. 4. 1 Matching atoms
We take an atom from the head of the list of
atoms in the graph template and try to ﬁnd thecorresponding atom from the host graph. If thematching succeeds, the atom in the host graph isremoved.
To match an atom, we need to check that they
have the same name and the correspondence oflinks. Since the local link names are α-convertible,
it is not suﬃcient only to check that they have thesame link names. Therefore, we exploit a link environment, a mapping from the local link names inthe template to the link names in the host graph.
Using structural congruence rules such as (E6),
we can fuse local link names. Therefore, it seems
that diﬀerent link names can be mapped to thesame link name, and vice-versa. However, since wehave absorbed all the fusion atoms that have local
links in the graph template, the former situation
is impossible. Thus the link environment is functional, i.e., the same link names are mapped to thesame link name. Notice the latter is still possible
since we can supply fusion atoms to the host graphin the matching.
The matching of link names using the link environment proceeds as in Figure 18. Free links in thetemplate should match links with the same namesin the host graph (line 7–8). On the other hand, thematching of local links in the template (line 10–14)
is more ﬂexible, since we can α-convert them.
For example, the atom Cons(L1001 , FY , L1000 )in the template (1) can be matched to the atom

Cons(L0 , FY , FX ) in the host graph (1) with linkenvironment{L1000 7→ FX , L1001 7→ L0 }(3)
and we have[1(L0 )]
(4)
left in the host graph.
6. 4. 2 Supplying fusions
After all the atoms in the template have matched,
we substitute link names in the host graph with inverse of the obtained link environment. For example, the rest host graph (4) becomes the following.
[1(L1001 )](5)
We supply fusion atoms to the host graph using
the link environment obtained in the matchings ofatoms. If the mapping is not injective, then weshould supply fusion atoms to the host graph. For
example, if we obtain the link environment{L1000 7→ L0 , L1001 7→ L0 }then we should supply L1000 ▷◁ L1001 .
If a local link in the template is mapped to afree link in the host graph, then we also need tosupply a fusion since a local link does not matcha free link without such treatment. For example, in the link environment (3), we have a mapping {L1000 7→ FX }. Thus, we should supply
L1000 7→ FX and obtain[1(L1001 ), L1000 ▷◁ FX ](6)
as the rest sub-graph.
Since we have preprocessed the template tohave no fusion atoms with local links, this fusionsupplying task can be performed after all the atoms
have matched. However, since graph contexts canmatch with fusions, we need to perform the task before moving on to the matching of graph contexts.
6. 4. 3 Matching graph contexts
Limitation. We place the following two limitations on the graph contexts to make the implementation simple: (i) the graph that a graphcontext can match is connected and (ii) the local
links of a graph context are connected to atom(s).
The matching that does not satisfy these two constraints can be highly non-deterministic, which we
believe is not practical and thus not the main scopeof our language.
→−
The matching of a graph context x[ X ] with subgraph G, initially Null, proceeds as follows.
→−→−
1. Find all the atom(s) with link Y where { Y } ∩→−{ X } 6= ∅. Add the atoms to G.
→
−
→
−
→
−
2. Update X with { Y } \ { X } and iterate fromlet check linkσ(* Link environment *)3
X(* Link in the template *)4Y(* Link in the host graph *)5=
6match (X, Y ) with
7
(FX , FY ) →8
if X = Y then Some σ else None12

13

(FX , Li ) → None
(Li , Y ) →if Li 7→ Z ∈ σ thenif Y = Z then Some σelse None

14

else Some (σ ∪ {Li 7→ Y })

9
10
11
12

Fig. 18

Link name matching(1) again.
3. If we obtain no more newly added atom, thencheck the free links of G is the same as the links→−of the graph context x[ X ].
For example, y[L1000 , FX ] and z[L1001 ], the graphcontexts in (1), can match host graphs L1000 ▷◁ FX
and 1(L1001 ), the sub-graphs in (6), respectively.
After the matching, we obtain the following graphsubstitution.
[ L1000 ▷◁ FX /y [L1000 , FX ] ,(7)
1(L1001 )/z [L1001 ] ]6. 5 Graph substitution
Graph substitution can be done by adding thematched atom(s) G to the host graph, the listof atoms. However, we need to take care oflink names. As we have deﬁned in Figure 11 in
Section 3, we need to substitute the link namesof G with the link names of the graph context in an evaluating template. Therefore, if we→−have matched G with x[ X ] and the template has→−x[ Y ], we need to update G with substitution− /X →− i. We also need to reassign
hY1 /X1 i . . . hY|→Y||X |ids for the local links since composing graphs may
result in a conﬂict of ids.
With the obtained graph substitution (7), we caninstantiate the template on the right-hand side of→ in Figure 16, [y[FY , FX ]], which will result in[FY ▷◁ FX ](8)
Our implementation absorbs fusions as much as
possible after graph substitutions. The fusion atomin (8) cannot be absorbed since both its links arefree links. On the other hand, the example in Figure 17 will result in[ L1000 ▷◁ FX ,Cons(L1001 , FY , L1000 ),1(L1001 )]which will be normalized and reassigned ids to obtain the following.
[Cons(L0 , FY , FX ), 1(L0 )]6. 6 The Evaluator
The evaluator is implemented just as these forfunctional languages. It takes an environment, a
mapping from graph contexts to the matched subgraphs, and an expression to evaluate.

7 Related and Future work
7. 1 Related work
7. 1. 1 Functional languages with graphs
FUnCAL [17] is a functional language that supports graphs as a ﬁrst-class data structure. This
language is based on an existing graph rewriting
language, UnCAL [4]. In UnCAL (and FUnCAL),
graphs may include back edges and their equality
is deﬁned based on bisimulation. FUnCAL comeswith its type system but does not support patternmatching for user-deﬁned data types, which classic
functional languages support for ADTs.
Functional programming with structured graphs[18] can express recursive graphs using recursivefunctions, i.e., let rec statements. Since they employ ADTs as the basic structure, they can enjoy
type-based analysis based on the traditional typesystem. On the other hand, we can do further detailed type analysis by our language and type system.
Initial algebra semantics for cyclic sharing tree
structures [12] discusses how to express graphs by
λ-expressions. However, there is a large gap between λ-expressions and pointer structures. On theother hand, we deﬁned a graph based on nodes andhyperedges, which has a clear correspondence toa pointer structure. This style is rather suitablefor future implementation. In addition, they do
not support user-deﬁned graph types or veriﬁcation
based on them.
7. 1. 2 Implementations for Graph Trans-

formation Systems
There are several languages based on graphtransformations. For example, AGG [22], GAMMA[3], Structured Gamma [9], GP [16], GP 2 [1],GROOVE [10], GrGen.NET [13], (Hyper) LMNtal[29] [31] [25], PORGY [7], and PROGRES [27]. However, as far as we know, few published implementations have focused on simplicity.
HyperLMNtal, which is the language we have incorporated, has the compiler [15] and the runtime
SLIM [28] [11]. The compiler is written in Java inaround 12,000 lines and the runtime is written in
C++ in around 47,000 lines. SLIM is highly optimized and enables non-deterministic execution andmodel checking, which is out of the scope of ourlanguage and implementation. Thus, we cannot
say our implementation surpasses it. Even so, thecontrast with the 500 lines of OCaml code for ourinterpreter is conspicuous.
GP 2 has a reference interpreter [2]. This is written in around 1,000 lines of Haskell sources without sacriﬁcing performance signiﬁcantly. Though
we sacriﬁced performance, we have implemented
the language that exceeds graph transformation inabout half of the lines in OCaml.
7. 2 Future work
The implementation in this study is only a Proofof Concept: execution eﬃciency is not considered.
To improve execution performance to the same level
as the corresponding imperative code, it is necessary to develop static analysis. We are planningto extend the type system to check the direction(polarity) of links [30], and then perform ownershipchecking [5]. Then, we develop a method to a transpile to a lower-level code using reference types infunctional languages such as OCaml or an imperative code with pointers.
Acknowledgments Part of this research was
supported by Waseda University Research Grant(2022C-421, 2022Q-006).
References[ 1 ] Bak, C.: GP 2: eﬃcient implementation of agraph programming language, PhD Thesis, Department of Computer Science, The University of York,2015.
[ 2 ] Bak, C., Faulkner, G., Plump, D., and Runciman, C.: A Reference Interpreter for the Graph

Programming Language GP 2, Proceedings Graphs
as Models, GaM@ETAPS 2015, London, UK, 1112 April 2015, Rensink, A. and Zambon, E.(eds.),
EPTCS, Vol. 181, 2015, pp. 48–64.
[ 3 ] Banâtre, J.-P. and Le Métayer, D.: Programming by Multiset Transformation, Commun. ACM,
Vol. 36, No. 1(1993), pp. 98–111.
[ 4 ] Buneman, P., Fernandez, M., and Suciu,
D.: UnQL: A Query Language and Algebra for
Semistructured Data Based on Structural Recursion, The VLDB Journal, Vol. 9(2000).
[ 5 ] Dietl, W. and Müller, P.: Universes: Lightweight
Ownership for JML., Journal of Object Technology,
Vol. 4(2005), pp. 5–32.
[ 6 ] Ehrig, H., Ehrig, K., Prange, U., and Taentzer,
G.: Fundamentals of Algebraic Graph Transformation, Springer, 2006.
[ 7 ] Fernández, M., Kirchner, H., Mackie, I., andPinaud, B.: Visual Modelling of Complex Systems:
Towards an Abstract Machine for PORGY, Language, Life, Limits, Beckmann, A., Csuhaj-Varjú,E., and Meer, K.(eds.), Cham, Springer International Publishing, 2014, pp. 183–193.
[ 8 ] Fradet, P. and Métayer, D. L.: Shape types,
Proc. POPL’97, ACM, 1997, pp. 27–39.
[ 9 ] Fradet, P. and Métayer, D. L.:
Structured Gamma, Science of Computer Programming,Vol. 31, No. 2(1998), pp. 263–289.
[10] Ghamarian, A., de Mol, M., Rensink, A., Zambon, E., and Zimakova, M.: Modelling and analysis using GROOVE, STTT, Vol. 14, No. 1(2012),
pp. 15–40.
[11] Gocho, M., Hori, T., and Ueda, K.: Evolution of
the LMNtal Runtime to a Parallel Model Checker,
Computer Software, Vol. 28, No. 4(2011), pp. 4 137–
4 157.
[12] Hamana, M.: Initial Algebra Semantics for
Cyclic Sharing Tree Structures, Log. Methods Comput. Sci., Vol. 6, No. 3(2010).
[13] Jakumeit, E., Buchwald, S., and Kroll, M.:
GrGen.NET: The expressive, convenient and fast
graph rewrite system, International Journal on
Software Tools for Technology Transfer, Vol. 12,
No. 3(2010), pp. 263–271.
[14] Leroy, X., Doligez, D., Frisch, A., Garrigue, J.,Rémy, D., and Vouillon, J.: The OCaml system release 41̇4, INRIA, Vol. 3(2022).
[15] LMNtal:
https://github.com/lmntal/lmntalcompiler.
[16] Manning, G. and Plump, D.: The GP programming system, Proc. Graph Transformation
and Visual Modelling Techniques (GT-VMT 2008),
volume 10 of Electronic Communications of the
EASST, 2008.

[17] Matsuda, K. and Asada, K.: A Functional Reformulation of UnCAL Graph-Transformations: Or,
Graph Transformation as Graph Reduction, Proc.
POPL’97, ACM, 2017, pp. 71–82.
[18] Oliveira, B. C. and Cook, W. R.: Functional
Programming with Structured Graphs, SIGPLAN
Not., Vol. 47, No. 9(2012), pp. 77–88.
[19] Plotkin, G.: A Structural Approach to Operational Semantics, J. Log. Algebr. Program., Vol. 6061(2004), pp. 17–139.
[20] Pugh, W.: Skip lists: A probabilistic alternative to balanced trees, Commun. ACM, Vol. 33,
No. 6(1990), pp. 668–676.
[21] Rozenberg, G.: Handbook of Graph Grammars
and Computing by Graph Transformation, World
Scientiﬁc, 1997.
[22] Runge, O., Ermel, C., and Taentzer, G.: AGG
2.0 – New Features for Specifying and Analyzing Algebraic Graph Transformations, Applicationsof Graph Transformations with Industrial Relevance, Schürr, A., Varró, D., and Varró, G.(eds.),
Berlin, Heidelberg, Springer Berlin Heidelberg,
2012, pp. 81–88.
[23] Sangiorgi, D. and Walker, D.: The Pi-Calculus:
A Theory of Mobile Processes, Cambridge University Press, USA, 2001.
[24] Sano, J.: Implementing G-Machine in HyperLMNtal, Bachelor’s thesis, Waseda University,
2021. https://arxiv.org/abs/2103.14698.
[25] Sano, J. and Ueda, K.: Syntax-driven andcompositional syntax and semantics of HypergraphTransformation System, Proc. 32nd JSSST Annual
Conference (JSSST 2021), 2021.
[26] Sano, J., Yamamoto, N., and Ueda, K.: Typechecking data structures more complex than trees,
Presented at the 141th IPSJ Special Interest Groupon Programming, Yamaguchi, Japan, 2022.
[27] Schürr, A., Winter, A. J., and Zündorf, A.: The
PROGRES Approach: Language and Environment,
World Scientiﬁc, 1997, chapter 13, pp. 487–550.
[28] SLIM: https://github.com/lmntal/slim.
[29] Ueda, K.: LMNtal as a hierarchical logic programming language, Theoretical Computer Science,Vol. 410, No. 46(2009), pp. 4784–4800.
[30] Ueda, K.: Towards a Substrate Frameworkof Computation, Concurrent Objects and Beyond,
LNCS, Vol. 8665, Springer, 2014, pp. 341–366.
[31] Ueda, K. and Ogawa, S.: HyperLMNtal: An Extension of a Hierarchical Graph Rewriting Model,
KI - Künstliche Intelligenz, Vol. 26, No. 1(2012),
pp. 27–36.
[32] Yamamoto, N. and Ueda, K.: Engineering
Grammar-based Type Checking for Graph Rewriting Languages, Proc. 12th Int. Workshop on Graph
Computation Models (GCM 2021), 2021.