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

グラフ書換え系における静的グラフ型検査
吉元 佑介

上田 和紀

グラフ書換え系とは、グラフ構造を、部分グラフの書換え規則によって書き換えることによって計算を行う系である。グラフを書き換えの対象とすることで、複雑なポインタ構造をもったデータ構造の操作を自然に表現できる。だが、データ構造の操作を書換え規則として表したとき、その規則による書き換えが、データ構造の持つ不変条件を崩さないことを示すのは容易ではない。そこで、本研究では、グラフ書換え系に静的型体系を導入し、書換え規則がデータ構造を保存することを検証する手法を提案する。この静的型によって、複数のルートを持つグラフ、循環や共有を表現するグラフ、数値制約を満たすグラフが表現できることを確認した。また、多くの型について、変換ルールがデータ構造を保存するか検査できることを確認した。

Graph rewriting systems are computation models that proceed by applying subgraph rewriting rules to graphs. Since they
rewrite graph structures directly, they enable us to express operations on data structures with complicated pointer linkings
naturally. However, when we express operations on data structures by graph rewriting rules, it is hard to verify that the rules
preserve invariants of the data structures. In this research, we introduced a static type system for graph rewriting systems andproposed a method to verify preservation of invariants for rewriting rules. We confirmed that the type system can express
graph structures with multiple roots, loops, data sharings and numerical constraints. Furthermore, we confirmed that theproposed method can verify the preservation of invariants for rules for a large class of types.

フ構造の持つ不変条件が、書換え規則による書換え

1 はじめにを行っても保存されることが検証できると便利であ

グラフ書換え系とは、グラフ構造を、部分グラフのる。そこで、グラフ書換え系に静的型体系を導入し、書換え規則によって書き換える計算モデルである。グ不変条件の保存をグラフの型の保存という形で表し、ラフの書換え規則は、「左辺のグラフを右辺のグラフそれを検証する手法を提案する。に書き換える」という形式で記述する。現在のグラフが、書換え規則の左辺を部分グラフを部分グラフとし2 言語モデル LMNtalて含む場合、書換え規則が適用され、マッチした部分

本論文では、グラフ書換え系のひとつである LMNtal

グラフが書き換え規則右辺のグラフに置換される。そ[10] に型体系を導入する。そのため、まずは LMNtalの応用例としては、オブジェクト指向言語の検証ツーの構文と意味論を定義する。なお、ここで定義するルである GROOVE [5] や、グラフ書換えの実行系およのは、LMNtal のサブセットである Flat LMNtal に、びモデル検査ツールである SLIM [9] [7] があげられる。

ルールの生成を許さないという制限を加えた体系でグラフ書換え系は、グラフを直接操作する計算モデある。本論文では断りのない限り、LMNtal はここでルであるため、入り組んだポインタ構造の操作を自定義する体系を指す。

然に記述できるという点で優れている。ここで、グラ
Static Graph Type Checking for Graph Rewriting Systems
Yusuke Yoshimoto, 早稲田大学基幹理工学研究科情報理工・情報通信専攻, Waseda University, Graduate School of Fundamental Science and Engineering, Department of Computer
Science and Communications Engineering.

2. 1 構文
LMNtal の構文は、グラフとルール（書換え規則）から構成される。まず、LMNtal グラフの構文を以下に示す。

::= 0( 空)| p(L1 , ..., Ln ) (アトム)| G, G(分子)
直観的には、空は、何もないことを表すグラフであG0, G ≡ G
G1 , G2 ≡ G2 , G1る。アトム p(L1 , ..., Ln ) は、 p という名前のノードに、L1 , ..., Ln という n 個の無向エッジ（LMNtal ではリンG1 , (G2 , G3 ) ≡ (G1 , G2 ), G3クと呼ぶ）が接続されたものを表す。なお、アトムの種類は、その名前 p と、接続すべきリンク数 n の組

G ≡ G[L/M]で表せる。この組をファンクタと呼び、 p/n と表記す

ただし、L は G の局所リンクで、M は新たなリンク名

同名のリンクが 2 回出現した場合、エッジの接続を

G1 ≡ G′1
G1 , G2 ≡ G′1 , G2表す。グラフに対し、1 回しか出現しないリンクを自=(L, L) ≡ 0る。分子は、二つのグラフを合わせたグラフである。

由リンク、ちょうど 2 回出現するリンクを局所リンクという。

=(L1 , L2 ) ≡ =(L2 , L1 )

G に含まれる自由リンクを明示したいとき
は 、L1 , ..., Ln が す べ て の 自 由 リ ン ク で あ る と き 、=(L, L′ ), p(L1 , ..., L, ..., Ln ) ≡ p(L1 , ..., L′ , ..., Ln )G[L1 , ..., Ln ] と表記する。

ただし，L は p(L1 , ..., L, ..., Ln ) の自由リンク

次に、LMNtal ルールの構文を以下に示す。

図1

LMNtal グラフの合同関係

R ::= G :- G
直観的には、 LHS :- RHS によって、グラフ LHS がG1 →R G′1
G1 , G2 →R G′1 , G2

RHS に書換え可能であるという規則を表す。

R ≡ R′ G →R′ G′
G →R G ′2. 2 意味論
構文上異なる LMNtal グラフが、意味的に同じグラ

LHS →R RHS

フを表すことがある。このことを表す、LMNtal グラフの同値関係を、図 1 を満たす最小の同値関係とし

図2

LMNtal グラフのルールによる遷移関係て定義する。

（R = LHS :- RHS ）特徴的な点は、局所リンクの名前は意味を持たないことと、二つのリンクを持つイコールアトムは、リン意味である。

クを接続するという意味を持った特別なアトムであるということである。

LMNtal グラフ G とルール R := LHS :- RHS が与えられたとき、G が G′ に書換え可能であるという関係を G →R G′ で表す。直観的には、G に LHS と合同な部分グラフが含まれるとき、その部分グラフを RHS に置換した構造に書き換え可能である。これは、図 2 を満たす最小の関係として定義される。 な

2. 3 略記法
グラフの表記を簡略化するための略記法を導入する。適当なリンク名 L1i を用いて、

p(L11 , ..., L1i , ..., L1n ), q(L21 , ..., L2m , L1i )と表されるグラフは、

p(L11 , ..., q(L21 , ..., L2m ), ..., L1n )と表記してよい。

お、二つのルール LHS :- RHS と LHS ′ :- RHS ′ が合また、ルールの表記を簡略化するための略記法を導同であるとは、これらをグラフ :- (LHS , RHS ) および入する。自由リンク L1 , ..., Ln をもつ任意の連結なグ:- (LHS ′ , RHS ′ ) として見たときに合同であるという

ラフを、適当な名前 p を用いて、$p(L1 , ..., Ln ) と表記

G[L1 , ..., Ln ] ◁ t(L1 , ..., Ln ) を 、「 G[L1 , ..., Ln ] はしてよい。これは構文としてはアトムに属し、この形のアトムを含むルールは、$p(L1 , ..., Ln ) が表す全てのt(L1 , ..., Ln ) によって生成される」と表現する。また、グラフに対するルールを意味する。

G[L1 , ..., Ln ]◁t(L1 , ..., Ln ) であり、かつ、2 を満たすこと
を、G[L1 , ..., Ln ] : t(L1 , ..., Ln ) と表記し、「 G[L1 , ..., Ln ]3 LMNtal グラフ型

は t(L1 , ..., Ln ) 型を持つ」と表現する。

LMNtal グラフに、Shape Type [2] をベースにした

また、LMNtal ルールのうち、型 t(L1 , ..., Ln ) の非終型体系を導入する。型に属すグラフの集合を、生成文端記号のみから構成されるものを、型 t(L1 , ..., Ln ) の法によって定義する。

変換ルールと呼ぶ。「変換ルールが型を保存する」という関係を、以下をもって定義する。
ルール R = LHS :- RHS が型 t(L1 , ..., Ln ) を保存す

3. 1 構文
LMNtal グラフ型の定義構文を以下に示す。

るとは、∀G ◁ t(L1 , ..., Ln ). G →R G′ ⇒ G′ ◁ t(L1 , ..., Ln )defshape t(L1 , L2 , ..., Ln ) {を満たすことである。

Rules} nonterminal {4 グラフ型の例

Functors}

複数のルートを持ち、循環を含むデータ構造とし

t は型名である。型は n 個の自由リンク（順序有り）て、スキップリスト [4] をグラフ型で表現する。レベをもち、リンク名 L1 〜 Ln で表す。 Rules は生成規則

ル 2 のスキップリストは、以下のグラフ型で表せる。の集合である。 Functors は非終端記号の集合である。

defshape skiplist(List1, List2) {なお、nonterminal 以降は省略可能で、省略した場合、(Prod0 ) skiplist(L1, L2) :- nil(L1, L2).

非終端記号は t/n のみとなる。

(Prod1 ) nil(L1, L2) :- node1(X1, L1),nil(X1, L2).

3. 2 意味論(Prod2 ) nil(L1, L2) :- node2(X1, X2, L1, L2),型 t(L1 , L2 , ..., Ln ) に属すグラフの集合は、直観的にnil(X1, X2).
}は、以下の条件をみたすものである。

1. 文法の開始記号 t(L1 , L2 , ..., Ln ) に、生成規則を 0回以上適用して生成されるグラフである

2. グラフに含まれる全てのアトムのファンクタは、これは、リンクリストの一部のノードに、途中のノードを飛ばすポインタを付与したものである。ソートされたデータをスキップリストを用いて実装すると、途中のノードを飛ばすポインタを利用した、効率非終端記号である
グラフ G[L1 , ..., Ln ] が 1 を満たすことを、G[L1 , ..., Ln ]◁的な探索が可能となる。なお、ここではスキップリスt(L1 , ..., Ln ) と表記する。これは、図 3 を満たす最小のトの構造だけに着目しているため、各ノードが持つ関係として定義される。

データは無視している。

ただし、 p は t(L1 , ..., Ln ) 型の推論規則に含まれるskiplist(List1, List2) 型をもつグラフの例を図 4 に示す。

任意のルールである。
なお、推論規則において、遷移関係の表記は冗長であるので、以降はG′ [L1 , ..., Ln ] ◁ t(L1 , ..., Ln )G[L1 , ..., Ln ] ◁ t(L1 , ..., Ln )と表記する。

List2
List1n1n2

n1n2n1n1

図4

スキップリストの例

(p)

n2nil

t(L1 , ..., Ln ) ◁ t(L1 , ..., Ln )G′ [L1 , ..., Ln ] ◁ t(L1 , ..., Ln ) G′ [L1 , ..., Ln ] → p G[L1 , ..., Ln ]G[L1 , ..., Ln ] ◁ t(L1 , ..., Ln )図3(p)グラフ型によるグラフの生成の定義

また、数値制約を含むデータ構造として、赤黒木Tree[1] をグラフ型で表現する。黒高さ 3 の赤黒木は、以b下のグラフ型で表せる。

defshape rbtree(Tree) {br(Prod0 ) rbtree(X) :- bnode(s(s(s(z))), X).
(Prod1 ) bnode(z, X) :- l(X).

lrbb(Prod2 ) bnode(s($m), X) :llllllb(node($m), node($m), X).
(Prod3 ) node(z, X) :- l(X).

図5

赤黒木の例

(Prod4 ) node(s($m), X) :- b(node($m), node($m), X).
(Prod5 ) node($m, X) :- r(bnode($m), bnode($m), X).
}できる。例えば、 skiplist(List1, List2) 型を持つグラフ

node1(X11, List1),
これは、以下の制約を満たすような二分木である。

node2(X12, X21, X11, List2),

1. 根と葉は黒に色づけられている

nil(X12, X21)

2. 赤に色づけられたノードの子は、黒に色づけられたノードである。の型検査は、図 6 に示す証明図を、下から上へ向かって構成することで行える。

3. 任意のノードについて、葉に至るまでの全ての経路上に、同数の黒に色づけられたノードがある

6 ルール型検査

3 の数値制約は、各ノード上に、そのノードから葉に文脈自由な型、すなわち、全ての生成規則の左辺至るまでの経路上の黒のノードの数を、0 と successorがひとつのアトムだけからなるような型については、で表した自然数で持たせておくことで実現している。

与えられた変換ルールの型保存性が検査できる。検査

なお、スキップリストと同様、各ノードが持つデータは以下の 2 ステップで構成される。

は無視している。

rbtree(Tree) 型をもつグラフの例を、図 5 に示す。

1. 検査対象ルール左辺を含む t 型のグラフを生成する、証明図のパターンを全て列挙する

2. 全ての証明図パターンに対し、検査対象ルール

5 グラフ型検査の左辺グラフを右辺グラフに置換したグラフが t

与 え ら れ た グ ラ フ G[L1 , ..., Ln ] に 関 し て 、型であることの証明が、パターンを元に構成でき

G[L1 , ..., Ln ] : t(L1 , ..., Ln ) で あ る か 検 査 す る 方 法 を示す。LMNtal グラフの定義から、グラフに含まれるアトムの数は有限なので、 G[L1 , ..., Ln ] が非終端記号るか調べる
以降では、リンクの集合を L というように太字で表記する。

を含まないことは、全てのアトムを見ることで判定できる。 G[L1 , ..., Ln ] ◁ t(L1 , ..., Ln ) であるかどうかは、生

6. 1 ステップ 1 : 証明図パターンの列挙

成規則を逆向きにしたルールを用いて、 G[L1 , ..., Ln ]ステップ 1 を実現するには、変換ルール左辺に、生が t(L1 , ..., Ln ) に遷移するかどうかを見ることで判定

成規則を逆向きにしたルールを適用し、開始記号まで

skiplist(List1, List2) ◁ skiplist(List1, List2)(Prod0 )nil(List1, List2) ◁ skiplist(List1, List2)(Prod1 )node1(X11, List1), nil(X11, List2) ◁ skiplist(List1, List2)
node1(X11, List1), node2(X12, X21, X11, List2), nil(X12, X21) ◁ skiplist(List1, List2)
図6(Prod2 )スキップリストのグラフ型検査

遷移させればよい。ただし、変換ルール左辺以外のグラフが未知であるので、逆向きルール中の一部（ひとつ以上）のアトムと反応することを許す。
つまり、ルール左辺 LHS [L1 ] に対し、証明図の最明図を得ることができる。
例えば、レベル 2 のスキップリストの変換ルール

node2(X1,Y1,X,Y), node2(X2,Y2,X1,Y1):- node1(X1,X), node2(X2,Y,X1,Y2)の場合、ステップ 1 によって、図 7 に示す証明図のみ

下部

Gn [L n ∪ L], LHS [L n] ◁ t(L)が得られる。変換ルールの左辺グラフ node1(X1,X),

node2(X2,Y,X1,Y2) を含むスキップリストは、全てこからスタートし、

G1 [L1 ∪ L], t(L1 ) ◁ t(L)に到達するまで、以下を繰り返す。

1. 外部グラフ Gi [Li ∪ L] のみを、生成規則によって 0 回以上還元するのパターンで生成することができる。

6. 2 ステップ 2 : 証明図パターンの変形
ステップ 1 で得られた証明図の、一番下に現れる外部グラフ Gn [L n ∪ L] は、そのパターンの証明図で2. 変換ルールの左辺グラフの一部である LHS i [Li ]生成される全ての外部グラフを代表している。従っの部分グラフ LHS i′ [L′i ] （空であってはならない）て、すべての証明図パターンの各々に対して、それをと、外部グラフの部分グラフ G′i−1 [L′i−1 ] （空でも元に、よい）からなる分子を、生成規則によって還元す

Gn [L n ∪ L], RHS [L n] ◁ t(L)る。ここで、 LHS i [Li ] の残りを LHS i′′ [L′′i ] 、還の証明図を構成できれば、任意の t(L) 型のグラフに元によってできるグラフ（これは一つのアトムのついて、ルール LHS :- RHS は型を保存する事が分みから生る）を G′′i−1 [L′i △ L′i−1 ] とする。

かる。

これらの操作によって、部分的な証明図

Gi−1 [Li ∪ L \ L′i−1 ], G′′i−1 [L′i △ L′i−1 ], LHS i′′ [L′′i ] ◁ t(L)Gi−1 [Li ∪ L \ L′i−1 ], G′i−1 [L′i−1 ], LHS i [Li ] ◁ t(L)Subproof
Gi [Li ∪ L], LHS i [Li ] ◁ t(L)を得る。なお、2 の還元において、複数通りの還元がここで、このことは型保存のための十分条件であるが、必要条件ではないことに注意する。たとえば、二つの証明図パターンが得られ、証明図最下部に現れる外部グラフが、それぞれ G, G′ だったとする。もし、G として考えられるグラフの集合と、 G′ として考えられるグラフの集合が一致するなら、二つのうち一つ可能であったり、還元が不可能である場合がある。まの証明図パターンに対して、書換え後のグラフが t 型た、還元の結果得られた明示的なグラフが、すでに得である証明が得られれば十分である。必ずしも、両方られた明示的なグラフと同型である場合、その還元はに対して証明が得られる必要はない。
では、左辺グラフを含むグラフの証明図パターンを考えない。
これを繰り返して証明図を構成した後、最後にt(L′ ) ◁ t(L)Subproof
G1 [L1 ∪ L], t(L1 ) ◁ t(L)を加えて、ルール左辺を含むグラフの生成に関する証元に、書き換え後のグラフの証明図を構成する方法を示す。まず、i ≥ 1 なる各々の i に対し、
Gi [Li+1 ∪ L \ L′i ], G′i [L′i ], LHS i+1 [Li+1 ] ◁ t(L)Subproofn
Gi+1 [Li+1 + L], LHS i+1 [Li+1 ] ◁ t(L)skiplist(List1, List2) ◁ skiplist(List1, List2)
Subproof 0
G1 [List1, List2, X, Y], skiplist(X, Y) ◁ skiplist(List1, List2)
G1 [List1, List2, X, Y], nil(X, Y) ◁ skiplist(List1, List2)(Prod0 )Subproof 1G2 [List1, List2, X, Y], nil(X, Y) ◁ skiplist(List1, List2)
G2 [List1, List2, X, Y], nil(X1, Y1), node2(X1, Y1, X, Y) ◁ skiplist(List1, List2)(Prod2 )Subproof 2G3 [List1, List2, X, Y], nil(X1, Y1), node2(X1, Y1, X, Y) ◁ skiplist(List1, List2)
G3 [List1, List2, X, Y], nil(X3, Y2), node2(X1, Y1, X, Y), node2(X3, Y2, X1, Y1) ◁ skiplist(List1, List2)(Prod2 )Subproof 3G4 [List1, List2, X, Y, X3, Y2], node2(X1, Y1, X, Y), node2(X3, Y2, X1, Y1) ◁ skiplist(List1, List2)
図7

スキップリスト変換ルールの左辺グラフの生成の形の部分的な証明図が得られているとする。
右辺グラフ RHS n [L n] と、グラフ G′1 [L′1 ], ..., G′n−1 [L′n−1 ]7 型検査の実装からなる分子を考える。ただし、自由リンクは適切にグラフやルールに対する型検査は、既存の LMNtal接続されているものとする。 この分子をグラフ型検処理系を用いた実装が可能である。グラフの型検査

査にかける。ただし、型の持つ自由リンクの接続方法を行うには、生成規則を逆向きにしたルールを、非決は問わない。

定的にグラフに適用すればよい。これはすでに実装

型検査に成功し、グラフがアトム t まで還元されると、グラフの自由リンクと型の自由リンクの対応関係がわかるので、それに従って、証明図中のグラフの自由リンク名を書き換える。
型検査に失敗した場合は、ルール型検査は失敗したとみなす。

ができている [8]。ルールに対する型検査を行うには、以下の操作が必要である。

1. 変換ルール左辺のグラフを、逆向きの生成規則との部分的なマッチにより書き換る。このとき、外部グラフを記録しておく。

2. 変換ルール右辺のグラフと記録した外部グラフ

スキップリストの例だと、右辺グラフ node1(X1, X),を、逆向きの生成規則によって書き換える。

node2(X2, Y, X1, Y2) に付加すべきグラフは、 nil(X2,1 の部分的なマッチは、逆向きの生成規則から、可能Y2) である。これらからなる分子を型検査にかけるな部分的マッチを表すルール群を生成して、それらをと、図 8 に示す証明図を得る。

非決定的に適用することによって実現できている [8]。

ここでできた右辺グラフの証明図と、左辺グラフ外部グラフの記録の際には、外部グラフと変換ルールの証明図の Subproof を適切に組み合わせることで、左辺のグラフとの自由リンクを適切に対応させる必Gn [L n ∪ L], RHS [L n] ◁ t(L) の証明図を構成できる。

要がある。これは今後実装を行う予定である。

スキップリストの例だと、図 9 に示す証明図を得ることができる。

8 関連研究したがって、グラフ G′1 [L′1 ], ..., G′n−1 [L′n−1 ] を、型の循環構造を含むようなグラフに対する型付けは、持つ自由リンクの接続方法を問わず型検査して、検査

Shape Type や Graph Type [3] といった先例がある。こが成功すれば、変換ルールは型を保存することが分れらの研究は、グラフ書換え系でない言語の静的検証かる。のためにグラフ型を用いており、本研究では、グラフ書換え系自体に型をつけているという違いがある。

skiplist(List1, List2) ◁ skiplist(List1, List2)(Prod0 )nil(List1, List2) ◁ skiplist(List1, List2)(Prod1 )node1(X1, List1), nil(X1, List2) ◁ skiplist(List1, List2)
node1(X1,List1), node2(X2, List2, X1, Y2), nil(X2, Y2) ◁ skiplist(List1, List2)
図8(Prod2 )スキップリストのルールの右辺グラフ型検査

skiplist(List1, List2) ◁ skiplist(List1, List2)
Subproof 0
G1 [List1, List2, X, Y], skiplist(X, Y) ◁ skiplist(List1, List2)
G1 [List1, List2, X, Y], nil(X, Y) ◁ skiplist(List1, List2)(Prod0 )Subproof 1G2 [List1, List2, X, Y], nil(X, Y) ◁ skiplist(List1, List2)
G2 [List1, List2, X, Y], node1(X1, X), nil(X1, Y) ◁ skiplist(List1, List2)(Prod1 )Subproof 2G2 [List1, List2, X, Y], node1(X1, X) nil(X1, Y) ◁ skiplist(List1, List2)
G2 [List1, List2, X, Y], node1(X1, X), node2(X2, Y2, X, Y), nil(X2, Y2) ◁ skiplist(List1, List2)(Prod2 )Subproof 3G3 [List1, List2, X, Y, X2, Y2], node1(X1, X), node2(X2, Y2, X1, Y) ◁ skiplist(List1, List2)
図9

スキップリスト変換ルールの右辺グラフの生成

また、数値制約を含むデータ構造への型付けは、得て行った。

Liquid Haskell [6] といった先例がある。これは関数型言語に対して数値制約を導入するものであり、一般的参考文献なグラフに対する制約を記述することはできない。

[ 1 ] Bayer, R.: Symmetric Binary B-Trees: Data Structure and Maintenance Algorithms, Acta Informatica, Vol. 1,No. 4, 1972, pp. 290–306.
[ 2 ] Fradet, P. and Métayer, D. L.: Shape Types, Proceedingsof the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1997, pp. 27–39.
[ 3 ] Klarlund, N. and Schwartzbach, M. I.: Graph Types,
Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, 1993,
pp. 196–205.
[ 4 ] Pugh, W.: Skip lists: a probabilistic alternative tobalanced trees, Communications of the ACM, Vol. 3,
No. 6(1990), pp. 668–676.
[ 5 ] Rensink, A.: The GROOVE simulator: A tool for state
space generation, Applications of Graph Transformations
with Industrial Relevance (AGTIVE), LNCS 3062, 2004,
pp. 479–485.
[ 6 ] Vazou, N., Seidel, E. L., and Jhala, R.: LiquidHaskell:
experience with refinement types in the real world, Proceedings of the 2014 ACM SIGPLAN symposium on Haskell,
2014, pp. 39–51.
[ 7 ] 綾野貴之, 堀泰祐, 岩澤宏希, 小川誠司, 上田和紀: 統
合開発環境による LMNtal モデル検査, コンピュータソフトウェア, Vol. 27, No. 4(2010), pp. 197–214.

9 まとめと今後の課題
本論文では、グラフ書換え系のひとつである LMN-tal に型体系を導入し、グラフの型検査と、変換ルールの型検査を行う方法を示した。
今後の課題として、検査可能なルールをより一般的なものにする、ということが挙げられる。本論文で示したルール型検査は、文脈自由な型に対してしか適用できない。しかし、グラフ型の例として示したように、文脈自由でない型を利用することで、制約の概念が表現できるようになる。このような型の変換ルールに対する型検査は重要である。
謝辞 LMNtal 処理系の開発に携わった早稲田大学上田研究室の先輩方、本発表に関する議論に快く応じてくれた現役生に感謝申し上げる。本研究の一部は、科学研究費補助金（基盤研究 (B) 26280024）の補助を

[ 8 ] 吉元佑介: グラフ書換え言語 LMNtal への Shape Typeの導入と実装, 早稲田大学卒業論文, 2014.
[ 9 ] 石川力, 堀泰祐, 岡部亮, 村山敬, 上田和紀: 軽量なLMNtal 実行時処理系 SLIM の設計と実装, 情報処理学会全国大会講演論文集 第 70 回, 2008, pp. 153–154.
[10] 上田和紀, 加藤紀夫: 言語モデル LMNtal, コンピュー
タ ソフトウェア, Vol. 21, No. 2(2004), pp. 126–142.