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

グラフ書換え言語におけるグラフ操作の静的型検査
山本 直輝

上田 和紀

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面を併せ持つ言語である．また，関数的アトムというデザイ
ンパターンを用いて，型の変換を伴う演算をも記述できる．一方で，グラフ書換え言語ではリストや二分木よりも複雑な構造を扱えるため，静的な型体系の定式化は自明でない．グラフ書換えの前後においてグラフの構造が保たれることを検査する静的型体系の先行研究として，Structured Gamma が存在する．そこで本研究では，Structured
Gamma を基に，LMNtal に静的型を導入することを考える．本論文では，Structured Gamma の型検査手法を用いて，関数的アトムの入力と出力の型が整合していることを検査する手法を提案する．

A graph rewriting language LMNtal has aspects of both a programming language which expresses calculation by graph rewriting and a modeling language which can handle complicated graph structures. Also, we
can use a design pattern called functional atoms in order to describe calculations with type transformation.
On the other hand, since graph rewriting languages can handle a broader class of graph structures thanlists or trees, formulation of static type system for those languages is not obvious. Structured Gamma is
known as a static type system which veriﬁes that graph structures will not be destroyed by graph rewriting.
Therefore we shall introduce a static type system based on Structured Gamma for LMNtal. This paper proposes a type checking method for calculations with type transformation, using the type checking algorithm
in Structured Gamma.

現することが出来るが，依然としてダングリングポイ

1 はじめにンタなどの不正なポインタが発生する危険性がある．

ネットワークという構造は，インターネットをはじそこで，グラフを第一級オブジェクトとしてもち，めとして，情報網や交通網，あるいは人間関係など，

それを書き換えることによって計算を表現する，グラ

様々な分野でみられる．これを抽象化・モデル化した

フ書換え言語というパラダイムが提案されている．こ

データ構造がグラフである．一般のグラフは，代数的のパラダイムに属する言語の例としては，GROOVE

データ型（リストや木構造）よりも複雑な構造をも[3] や GP [5]，REGREL+ [11] などが挙げられる．

ち，それ故に既存のプログラミング言語では扱うこと

中でも，LMNtal [9] は，グラフ書換え言語の一つが難しい．例えば，C 言語のようなポインタを扱えるであり，アトム（ノード）やルール（書換え規則）と言語であれば，ポインタの接続構造としてグラフを表いった最小限の言語要素からなる言語モデルである．

∗ Static Type Checking of Graph Operations in Graph

Rewriting Languages.
This is an unrefereed paper. Copyrights belong to
the Author(s).
Naoki Yamamoto, Kazunori Ueda, 早稲田大学基幹理工学研究科情報理工・情報通信専攻, Dept. of Computer
Science and Communications Engineering, Graduate School of Fundamental Science and Engineering,
Waseda University.

しかしながら，LMNtal は十分な表現力・計算能力をも持ち合わせている．実際，LMNtal はチューリ
ング完全であり，ラムダ計算などの他の言語体系を

LMNtal プログラムにエンコードする手法が存在している．

LMNtal グラフは well-formed であるかぎり，不正なポインタを含まない．この意味で，LMNtal は言語

仕様のレベルに於いて不正なポインタを排除している自身によって型検査を行うという取り組みが研究テー（すなわち，ポインタ安全である）といえる．しかし

マとして非常に興味深いだけでなく，LMNtal の柔軟依然として，LMNtal には静的型の概念がないため，な表現力をそのまま型体系に活かすことができるの

書換えの結果がプログラマの意図しないものとなるは大きな強みである．

ことがある．

本論文では LMNtal においてよく用いられるデザ

例えば，静的型付きの関数型言語である OCaml でインパターンである関数的アトムに着目し，LMNtal

はリストの結合を行う append 関数を次のように定義

ShapeType を応用することによって静的に型安全性できる．

を検査する手法について述べる．

let rec append a b =match a with

2 関連研究| [] -> b

本節では，グラフを対象とする既存の型体系を紹介| h::t -> h::(append t b);;する．

この append 関数は引数に 2 つのリストが与えられる

Graph types [4] は正規表現を基にしたグラフの型体ことを期待し，それらを結合したリストを返却する．

系である．また，Structured Gamma [2] は文脈自由文

そのため，append 4 [1;2;3];; のようにリスト以法を基にした，生成規則によって型を定義する型体系

外のものを引数に与えると型エラーとなり，処理系がである．Shape Types [1] はこの Structured Gamma

その旨をプログラマに通知する．

のサブセットであり，型検査の完全性が満たされる

同様に，LMNtal においても次のように append ア
トムを定義できる †1 ．

ように型定義の範囲を制限したものである．そして，[8] ではこの Shape Types を基にして LMNtal グラ

Ret = append([],B) :- Ret = B.

フおよびルールの型検査を行う型体系として LMNtal

Ret = append([H|T],B)

ShapeType が提案されている．

:- Ret = [H|append(T,B)].

これらの型体系では，「グラフの書換え操作を 1 ス

しかし，list = append(4,[1,2,3]). のような不正テップ進めても，構造が破壊されない」ことの検査・なプログラムを処理系に与えたとしても，コンパイル保証を行うことに重点を置いていた．すなわち，「リス

時・実行時ともにエラーとはならず，ただ単に実行がトに対して挿入操作を行ったあとも必ずリストになっ

進まなくなってしまうだけである．

ている」や「二分木に対して要素の削除操作を行った

こうした問題点を解決するため，これまでにも LM-

Ntal を対象とする幾つかの静的型体系が提案されてあとも必ず二分木になっている」といった性質は，上述の型体系によって保証できる．

いる．例えば，文献 [6] の型体系ではノード間の局所

しかしながら，「整数のリストに対して，要素の総的な繋がりに着目し，入出力の方向性を解析し，それ和をとる操作を行うと，整数が返ってくる」のようにを極性として表現することで型を付ける．

操作の前後で型が変化する場合や，前述の append の一方，本研究で扱う LMNtal ShapeType [8] は，Shape types [1] を基とした型体系である．この型体ように複数の構造を入力にとる場合について対応していなかった．

系では，LMNtal のルールを生成規則として，生成文

また，このような型から型への変換を伴う計算には

法により型の定義を行う．そのため，LMNtal 自身に複数ステップを要することも多い．例えば，append

よって LMNtal の型検査を行えるという利点がある．

の場合は一方のリストの要素数の分だけ計算ステップ

ある言語の型体系をその言語自身で記述し，その言語を要する．従来の型体系では small-step での性質を†1 ここで用いた角括弧によるリスト記法は単なる構文糖
衣であり，実際には特別な名前 ‘.’ を持った 3 価アト
ムの鎖に展開される．

保証しているために，こうした big-step の性質についてはあまり注目されていなかった．





c

F

プロセス

a

b
d

P ::= G,R
グラフ
図2

（空）

G ::= 0| p (X1 , . . . ,Xm ) （アトム, m ≥ 0）
| G,G

p/m のように書き，「m 価の p アトム」のように読む．

（分子）

LMNtal におけるアトム・リンクは，それぞれグラフ

ルールセット理論における節点（ノード）・辺（エッジ）と対応し（空）

R ::= 0| [ RuleName @@ ] G :- G



LMNtal グラフの例

| R,R

ている．

（ルール）

LMNtal においては，アトムの多重集合によって無（分子）

向多重グラフを表現する（つまり，多重辺や自己ループの出現を許す）．例えば，

図1

LMNtal の構文

a(A,F), b(A,C,L1,L2), c(C,D,S,S), d(D,L1,L2)というアトムの多重集合は，図 2 に示すような無向グラフを意味する．ただし，図中において矢印は第 13 グラフ書換え言語 LMNtal

引数の場所を指しており，そこから矢印の向きに従っ

本節では，グラフ書換え言語 LMNtal について簡て引数に順序がついていることを示す． グラフ中に単に説明する．なお，本来 LMNtal には膜による階同じリンクは高々2 回出現する．グラフ中に 2 回出現

層や，ルールの発火に関する制約条件を記述するたするリンクは両端がアトムと繋がっている局所リンめのガード及びプロセス文脈といった機能が備わってクであり，1 回のみ出現するリンクは一端が無接続でいるが，本論文では簡単のためこれらを除外したサある（または，外部と接続している）自由リンクであブセット言語を扱う．また，LMNtal の拡張言語である．自由リンクのないグラフは閉じているという．2

る HyperLMNtal [7] において導入された拡張機能でつのグラフをカンマで結合する際は，局所リンク名がある，超辺を表すハイパーリンクについても扱わな

衝突しないように α 変換されたものとみなす．

い．しかしながら，これらの高度な言語機能をもたな

ルールは，部分グラフから部分グラフへの書換え

い LMNtal もまたチューリング完全であり，プログを表す書換え規則である．例えば，a(X) :- b(X) はラミング言語としてもモデリング言語としても十分

1 価の a アトムを，1 価の b アトムに書き換えるルー強力である．

ルである．便宜上，ルールの名前として RuleN ame
をルールの前に付すこともある．また可読性のため

3. 1 構文に，ルールはカンマで区切るかわりに，ピリオドで終LMNtal の構文を図 1 に示す． LMNtal プログ

わる形で書かれることもある．なお，書換えの前後にラムは，グラフ（アトムの多重集合）とルールセッ

おいて自由リンクの本数が増減することはあり得な

ト（ルールの多重集合）の組として表現され，これいので，ルール中に同じリンクはちょうど 2 回だけをプロセスと呼ぶ．p という名前で， m 本のリンク

出現する．

X1 , . . . , Xm をもつアトムを p (X1 , . . . ,Xm ) と書
く．これらのリンクをアトムの引数といい，順序がつ

3. 2 意味論

いている．英字の大文字から始まる名前はリンク名，LMNtal の意味論は，構造合同と遷移規則からな

そうでないものはアトム名として解釈される．アト
ム名と引数の本数（価数）の組をファンクタといい，る．これらについて順に説明する．





(E1)

0,P ≡ P

(E2)

P ,Q ≡ Q,P(E3)

P ,(Q,R) ≡ (P ,Q), R

G1 −−−−−−→ G′1
T :- U
G1 ,G2 −−−−−−→ G′1 ,G2(R1)P ≡ P [Y /X](E4)


T :- U(R3)

G2 ≡ G1

P ≡ P ′ ⇒ P ,Q ≡ P ′ ,Q

(E7)

X=X ≡ 0(E8)

X=Y ≡ Y =X

G′1 ≡ G′2

T :- UG2 −−−−−−→ G′2（X は P の局所リンク）(E5)

T :- U

G1 −−−−−−→ G′1

T :- UT −−−−−−→ U

(R6)



図4



LMNtal グラフ上の遷移関係

X=Y ,P ≡ P [Y /X](E9)(R6) である．これは，「ルールと，その左辺にパター（P はアトム，X は P の自由リンク）ンマッチするプロセスが存在したら，その左辺を右辺
図3

LMNtal グラフ上の構造合同関係に書換えてよい」ということを言っている．
また，この定義を自然にルールセットへと拡張する

3. 2. 1 構造合同

ことができる．すなわち，∃r ∈ R. G −−→ G′ が成り

グラフ理論における “同型” にあたるものとして，立つとき「ルールセット R によって，グラフ G が（1LMNtal にはグラフ間の構造合同関係 “≡” が存在すステップで）G′ に遷移する」といい，単に G −−→ G′

る．この関係は，図 3 の規則を満たす最小の同値関係

とかく．

r

R

として定義される．構造合同な LMNtal プロセスは

なお，通常の LMNtal においては，アトムとルー

互いに 0 ステップで変換可能である．なお，P [Y /X]

ルの多重集合であるプロセスが，遷移関係に基づいはグラフ P に出現するリンク X をリンク Y に置きておのずから書き換わっていく．そのため，「ルール

換えることを意味する．ただし，(E6), (E10) は膜にによる作用を受けてグラフが書き換わる」とは考え関する規則であるので省略した． (E1)–(E3), (E5) はない．しかしながら，書換えに関する性質を静的に保プロセス計算にもみられる一般的な規則であり，(E4)

証する型体系について定義および議論をするにあたっ

は局所リンク名の α 変換である．(E7) から (E9) まては，書換えの主体たるルールと客体たるグラフとでは特別な 2 価のアトムであるコネクタに関する規則

は明確に分離されていたほうが都合が良い．よって，である．=(X, Y ) は二つのリンク X, Y を接続すると

本論文では LMNtal の構文・意味論を簡明な形に等いう意味を持ち，中置記法で X = Y とも書く．(E7)

価変換して扱っている．

は一つのリンクの両端が繋がって輪になっているもの
は空とみなして良いこと，(E8) はリンクが対称であ3. 3 略記法

る（つまり無向である）こと，(E9) は直接接続され便宜上，次の二つの略記法が認められている．

ている二つのリンクが一つのリンクに縮約できるこ

1. アトムの引数にアトムを書いた場合は，そのアトとを表している．

ムの最終引数に繋がっているものと解釈される．つ3. 2. 2 遷移規則

まり，p(X1 , . . . ,q(Y1 , . . . ,Yn ), . . . ,Xm ) は，

LMNtal における本質的な計算ステップを表す，グp(X1 , . . . ,L, . . . ,Xm ), q(Y1 , . . . ,Yn ,L) とラフ間の二項関係として，ルール T :- U によるグ解釈される．ただし，L は使用されていない

T :- U

ラフの遷移関係 “−−−−−→” が存在する．これは，図適当なリンク名とする．例えば，a(b(c),d) は4 に示す遷移規則をみたす最小の二項関係として定義

a(B,D),b(C,B),c(C),d(D) を意味する．

される．ただし，(R2), (R4), (R5) は膜に関する規2. 引数リストを省略した場合は引数が 0 個である

則であるので省略した． 最も本質的で重要な規則はと解釈される．つまり，p は p() の意味である．

が含まれていない場合も，暗黙に含むものと考える．

4 LMNtal ShapeType

以上のように定義された型を，開始記号 S = t/m

本節では， [8] で提案された LMNtal を対象とするのアトム名 t と，適当なリンク名 L1 , . . . , Lm を用

静的な型体系である LMNtal ShapeType を紹介すいて t(L1 , . . . ,Lm ) 型などと呼ぶことにする．通常る．まず，形式的な定義を先に示しておく．なお，以の代数的データ型（二分木やリスト等）ではデータ

下で “記号” と言うときは，LMNtal のファンクタの構造の根は一つであるが，LMNtal ShapeType が扱ことを指す．

うデータ構造の根は一つとは限らない．そのため，

定義 1. LMNtal ShapeType における型（以下，こShapeType として定義される型の根と，型付け対象

れを単に “ShapeType” という）は，3 つ組 (S, P, N )のグラフの根（自由リンク）とが，どのように対応関である．ここで，係を持つのかを明示するために，根にそれぞれリンク• S = t/m は，開始記号と呼ばれるファンクタ

名を持たせている．

• P は，生成規則と呼ばれるルールの有限集合

ただし，リンク名が重要でないときは開始記号の• N は，非終端記号と呼ばれるファンクタの有限ファンクタを用いて t/m 型（あるいは m 価の t 型）

集合と呼び，誤解のおそれがないときは価数も省略して単

⋄

とする．

に t 型と呼ぶ．

4. 1 構文4. 2 意味論

ShapeType の構文を図 5 に示す．生成規則は，LM-

型付け関係 “:” を定義するにあたって，補助的な型

Ntal のルールとして well-formed である必要がある．

付け関係 “◁” を先に定義する．以下では，L1 , . . . , Lm

生成規則の左辺は 1 つ以上の（コネクタでない）非だけを自由リンクに持つグラフを G[L1 , . . . , Lm ] と終端アトムのみからなる．また，LMNtal と同様の略書く．また，グラフ G 中で使用されているファンク

記法（3. 3 節）を認める． 可読性の理由から，S とタ全体の集合を，Funct(G) と表す．
定義 2. 型 (t/m, P, N ) について，

ShapeType::=であるとき，かつそのときに限り，G[L1 , . . . , Lm ]defshape S { P } [ nonterminal{ N } ]は t(L1 , . . . ,Lm ) 型 に よって生 成 さ れ ると い い ，

開始記号

S

::=

G[L1 , . . . , Lm ] ◁ t(L1 , . . . ,Lm ) と書く．

p(X1 , . . . ,Xm )::=よって 0 ステップ以上遷移した先のグラフだけが t 型

0 | [ RuleN ame @@ ] A :- A | P ,Pによって生成されることを表す．

非終端記号の有限集合

N::=

次に，型付け関係 “:” を定義する．

A

アトムの有限集合



A

::=

⋄

これは直観的には，t 型の開始記号から生成規則に

生成規則の有限集合

P

P

t(L1 , . . . ,Lm ) −→* G[L1 , . . . , Lm ]0 | p(X1 , . . . ,Xm ) | A,A

定義 3. 型 (t/m, P, N ) について，



G[L1 , . . . , Lm ] ◁ t(L1 , . . . ,Lm )かつ

図5

ShapeType の構文

Funct(G[L1 , . . . , Lm ]) ∩ N = ∅であるとき，かつそのときに限り，G[L1 , . . . , Lm ]N の中でファンクタをアトムの形で記述しているが，は t(L1 , . . . ,Lm ) 型をもつといい，G[L1 , . . . , Lm ] :引数のリンク名に意味はなく，価数が同じであれば名t(L1 , . . . ,Lm ) と書く．

⋄

前は何でもよい．また，N の定義は省略することがこれは直観的には，t 型によって生成されるグラフ

でき，その場合は N = {S} とみなす．N の定義に Sのうち，非終端記号を含まないグラフのみが，t 型を

アトムは関数型言語における append 関数のように，もつことを表す．
これらの定義において，グラフの自由リンクをわざわざ明示しているのは，前節で述べた通り自由リンク

リストの結合を行う．

a1@@ R=append(c(L1),L2)の名前と順序が重要であるためである．例えば，:- R=c(append(L1,L2)).

defshape t(X,Y) { t(X,Y) :- a(X,Y) },a2@@ R=append(n,L) :- R=L.

という型があった時に，a(X,Y) ◁ t(X,Y) であるが，a(Y,X) ◁ t(X,Y) ではない．

これらのルールは図 6 に示すように可視化できる．
関数的アトムは，関数と同様に引数に対し入力されたデータに基づいて，適切に出力を返すことが期待さ

4. 3 型検査

れる．例えば，append/3 アトムは第 1 引数と第 2 引

LMNtal ShapeType には，2 つの基本的な型検査

数に入力として 2 本のリストが入ってくることを期手法がある．一つは，グラフの型検査である．これ待し，それらのリストをルールによって扱い，結合しは，与えられたグラフが，与えられた型に属している

たリストを出力として第 3 引数に向かって返却するかを検査するものである．もう一つは，ルールの型検（図 7）．

査である．これは，ルールと型が与えられたときに，通常の関数型言語における関数とは異なり，関数的ルールの実行によって型の構造が破壊されないことをアトムが返す型のルートは，一つとは限らない．その検査するものである．

ような型を返す関数的アトムの例として，次の t2l/3

ルールの型検査について，もう少し形式的に解説する．まず，型 t に関する LMNtal ルール r の型保存性を定義する．

t1@@ t2l(n(N,L,R),T,P):- t2l(L,c(N,t2l(R,T)),P).

定義 4. ルール r と型 t/m およびリンク列 L1 , . . . , Lm′

t2@@ t2l(l,T,P) :- T=P.
これらのルールは図 8 に示すように可視化できる．こについて，全ての G : t(L1 , . . . ,Lm ) が，
r（tree-to-list）がある．

′

G −−→ G ⇒ G : t(L1 , . . . ,Lm )

れは，二分木を受け取って，中間順に走査し，差分リを満たすとき，かつそのときに限り，r は t 型を保存

ストに変換する関数的アトムである（図 9）．

⋄以上のように関数的アトムとは，入力を受け取って自然言語で表現すると，「t 型をもつ全てのグラフ出力を返す関数のように振る舞うアトムのことを指G は，ルール r を（可能なら）適用した後も，t 型をす．一方で，通常の関数型言語においては関数が演算持っている」という性質である．このルールの型保存の主体であり，データ構造が演算の客体であるのに対するという．

性の検査のことを，単にルールの型検査という．

し，LMNtal においては演算の主体たるプロセスやLMNtal ShapeType においては，生成規則が LM-

メッセージと，客体たるデータを区別することなく，

Ntal 自身のルールとして記述されていることから，

それら全てをアトムという唯一の言語要素によって統LMNtal を対象言語とするモデル検査器 SLIM [10] を一的に表現する．そのため，「関数的アトム」という用い，生成規則の逆実行により実際にグラフの型検ものが，他のアトム（データアトム）とア・プリオリ

査・ルールの型検査を行うことが出来る．具体的な検に類別されているわけではない．

査手法については，文献 [8] を参照されたい．

また，LMNtal における演算の主体は，アトムではなくむしろルールであるので，アトムが自身の振る

5 関数的アトム

舞いについて責任を負っているわけではない．アトム

LMNtal プログラムを書く上で，よく用いられるデの振る舞いを規定するのは，ルールである．そして，

ザインパターンとして，関数的アトムというものがルールが発火するか否かはアトムそのものに依存しある．これは，関数型言語における関数のように振るているというよりは，各アトムのもつファンクタとそ舞うアトムである．例えば，以下のような append/3

れらの間の接続構造に依存している．

a

c

a

c

:-

図6

a

c

c

n

c

n

c

n

c

n

図7

t2l

H
N

T

H

:-

n

L

3

T

t2l

L

N

R

4

n
l

1
l

l

n
l

l

T

H

t2l

H

n

4

9

n
l

t2l

c

n

n
l

n

c

c

n

c

n

t2l

T

:-

H

c

c

c

c

c

c

4

1

1

3

5

9

H

T

l

T

3
5

a

t2l/3 アトムに関する関数的ルール

n

n

c

append/3 アトムによる計算過程

1
1

:-

c

c

図8

t2l

c

t2l

R

H

n

append/3 アトムに関する関数的ルール

a

c

a

1
l

...
5
l

n
l

l

n
9

T

n
l

l

l

図9

t2l/3 アトムによる計算過程

以上の事実を踏まえると，“関数的” という性質を関数的ルールセットという．また，F をもつアトムの定義する際には，個々のアトムではなくむしろルー

ことを単に関数的アトムという．誤解の恐れがないとルやファンクタに注目すべきである．よって，“関数

きは，R を略す．

的” という性質を以下のように定義する．

⋄

直観的に言えば，関数的アトム F に入力として定義 5. 型 t1 , . . . , tn , T と，f /m アトム一つからな

t1 , . . . , tn 型のグラフを与えて，計算が終了すると Tるグラフ F および 左辺に f /m アトムをちょうど型のグラフが得られるということを示している．た1 つもつルールからなるルールセット R について，

だし，ここではグラフ中に関数的アトムが残っていな

t1 , . . . , tn 型をそれぞれもつグラフ Gt1 , . . . , Gti にいこと（すなわち計算の正常終了）を仮定しているの対し，で，計算が行き詰まらないことを保証するわけではR

F ,Gt1 , . . . ,Gtn −→* Gを満たし，かつ F と同じファンクタのアトムを含まないような G について，G : T を（Gt1 , . . . , Gtn のとり方によらず）満たすとき，F は関数的であるという．また，これを t1 , . . . , tn ⊢R F : T とかく．

t1 , . . . , tn を入力型，T を出力型，R を F に関するない．
この記法を用いて，append アトムと t2l アトムの性質を図 10 のように記述できる．

list(L1),list(L2) ⊢{a1,a2} append(L1,L2,R) : list(R)tree(T) ⊢{t1,t2} t2l(T,X,Y) : dlist(X,Y)
図 10

append アトムと t2l アトムの性質（ここでは，二分木の型を tree，差分リストの型を dlist と表記している）

このとき G′ は，6 関数的アトムの型検査

1. 関数的アトムが 1 個以上残っている与えられたファンクタが関数的であるか否かを，LMNtal ShapeType におけるルールの型検査を用い（計算の途中である）

2. 関数的アトムが残っておらず，出力型をもつグて検証することを考える．関数的という性質は上述

ラフになっている（計算が終了している）のように大ステップ的に定義されるが，ルールの型検のいずれかであるが，この 2 つの性質は上記の議論

査によって検査可能であるのは「1 ステップのルール

により，「計算途中グラフが出力型をもつと仮定する

適用」のみである．そこで，以下では図 7 や図 9 にと，G′ は出力型をもつ」という性質によって統一的示したような関数的アトムによる計算過程を小ステッに表すことが出来る．

プ的に解釈していく．

「計算途中グラフが出力型をもつと仮定する」とい

以下では，「関数的アトムに入力型のグラフが繋がっ

うのは，具体的には出力型の開始記号から計算途中グたもの」を計算途中グラフと呼ぶ．例えば，図 7 の最ラフを生成するような生成規則を追加することで実左のグラフは関数的アトム append に入力型 list の現できる．すなわち，append の場合であればグラフが 2 つ繋がった形をしているので，計算途中グ

list(R) :- append(L1,L2,R),list(L1),list(L2)ラフそのものといえる．これに 1 ステップルールを適という生成規則を list 型の定義に，t2l の場合であ用したグラフ（図 7 の左から 2 つ目）は c アトムのれば先に計算途中グラフが繋がった形をしている．続いてdlist(X,Y) :- t2l(T,X,Y),tree(T)

図 7 の左から 3 つ目のグラフは，c アトムが 2 つ繋という生成規則を dlist 型の定義にそれぞれ加える

がった先に計算途中グラフが繋がった形をしている．

ことを指す．

同様に，図 9 の最左のグラフは全体が計算途中グ

また，この仮定の上で考えると，計算の開始時のグラフになっており，次のグラフは c アトムの前後に計ラフ（図 7 および図 9 の最左）は全体が計算途中グ

算途中グラフが繋がった形をしている．

ラフとなっていることから，これも出力型のグラフに

これらのグラフは，いずれも計算途中グラフが最なっているといえる．つまり，関数的ルールセット R

終的に出力型のグラフになると仮定すると，全体とが，生成規則の追加によって拡張された出力型を保存

して出力型のグラフになっている．つまり，図 7 の c

するならば，F は関数的であると言える．

アトムが 0 個以上繋がった先に計算途中グラフが繋以上の議論を定理の形にまとめると次のようにながった形は，計算途中グラフを list 型の任意のグラる．ただし，St , Pt , Nt は型 t の開始記号と生成規則

フで置き換えてやると，全体として list 型のグラフの集合と非終端記号の集合をそれぞれ表すとする．

となる．また，図 9 の左から 2 つ目のグラフは c ア

定 理 1. 生 成 規 則 の 集 合 P = PT ∪ Pt1 ∪ · · · ∪トムの前後に計算途中グラフが繋がった形をしている

Ptn ∪ {T :- F ,t1 , . . . ,tn } と 非 終 端 記 号 の 集 合

ので，計算途中グラフを差分リストで置き換えてやる

N = NT ∪ Nt1 ∪ · · · ∪ Ntn に つ い て ，す べ て のと，全体として差分リストになる．

ルール r ∈ R が，型 (ST , P, N ) を保存するとき，

関数的ファンクタ F をもつアトムを（0 個以上）含むグラフ G に対し，F に関する関数的ルールセット′

R を 1 ステップ適用すると，グラフ G を得たとする．

t1 , . . . , tn ⊢R F : T が成り立つ．

⋄

ただし，それぞれの型の非終端記号には重複がない
ように予め α 変換を施しておくものとする．

7 まとめと今後の課題
本論文では，関数的アトムというデザインパターンに着目し，複数ステップを要し，また型の変換を伴うようなグラフ操作について型検査を行う手法について述べた．
今後の課題としては，入力や出力のグラフが実質的に無限である場合に対応することが挙げられる．今回扱ったグラフはいずれも有限であることを暗黙に仮定しているが，6 節の議論は，グラフが実質的に無限である場合にも適用可能である．例えば，無限リス
ト（ストリーム）を出力するような関数的アトムや，
無限のメッセージ列を受け取るサーバのような関数的アトムといったものが考えられる．実際のところ，

LMNtal はプロセス計算を基に設計されていることから，こうした無限の性質をもったモデルを容易に記述出来る．そのため，無限グラフに対応した型体系を用意しておくことは重要である．
謝 辞 本 研 究 の 一 部 は ，科 学 研 究 費 基 盤 研 究 (B)

18H03223 の助成を受けて実施した．
参 考 文 献[ 1 ] Fradet, P. and Métayer, D. L.: Shape types,
Proc. POPL’97, ACM, 1997, pp. 27–39.

[ 2 ] Fradet, P. and Métayer, D. L.:
Structured Gamma, Science of Computer Programming,Vol. 31, No. 2(1998), pp. 263–289.
[ 3 ] 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.
[ 4 ] Klarlund, N. and Schwartzbach, M. I.: Graph
Types, Proc. POPL’93, 1993, pp. 196–205.
[ 5 ] 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.
[ 6 ] Ueda, K.: Towards a Substrate Frameworkof Computation, Concurrent Objects and Beyond,Agha, G. et al.(eds.), LNCS, Vol. 8665, Springer,
2014, pp. 341–366.
[ 7 ] 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.
[ 8 ] 吉元佑介, 上田和紀: グラフ書換え系における静的
グラフ型検査, 日本ソフトウェア科学会第 32 回大会(2015 年度) 講演論文集, 2015.
[ 9 ] 上田和紀, 加藤紀夫: 言語モデル LMNtal, コンピュー
タ ソフトウェア, Vol. 21, No. 2(2004), pp. 126–142.
[10] 石川力, 堀泰祐, 村山敬, 岡部亮, 上田和紀: 軽量なLMNtal 実行時処理系 SLIM の設計と実装, 情報処理学会第 70 回全国大会講演論文集, (2008), pp. 153–154.
[11] 東達軌, 武田正之: 動的な階層構造に基づくグラ
フ書き換え言語 REGREL+, 第 10 回情報科学技術フォーラム (FIT2011) 講演論文集（第 1 分冊）, 2011,
pp. 159–166.