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

グラフ書換え言語における数値制約を伴う型の静的型
検査
山本 直輝

上田 和紀

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．そして，LMNtal の処理系は通常のプログラム実行とモデル検査の双方に対応した，強力な機能を提供している．グラフ書換え言語では，関数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，静的な型検査の定式化は自明でない．そこで，書換え
規則の型検査の手法として，グラフを対象とする静的型検査手法である Structured Gamma を基にした，LMNtal
ShapeType が提案されている．本論文では，LMNtal ShapeType に対し，LMNtal の拡張機能である型付きプロセス文脈を援用することにより，添字付きの非終端記号を表現し，赤黒木などの数値制約を伴うグラフ型を対象とした書換え規則の型検査を行う手法について述べる．

A graph rewriting language LMNtal has aspects of both a programming language that expresses computation
by graph rewriting and a modeling language that can handle complicated graph structures. Furthermore,
its implementation integrates both regular program execution and model checking. In graph rewriting languages, we can handle a broader class of graph structures than algebraic data structures that can be handled
by functional languages. As a type checking method for rewrite rules, LMNtal ShapeType was proposed
based on Structured Gamma, a static type checking method for graphs. This paper proposes a type checking method for rewrite rules targeting graph types with numeric constraints (e.g., red-black trees) by using
typed process context, which is an extension of LMNtal, as the index of nonterminal symbols.

一般のグラフは，代数的データ型（リストや木構

1 はじめに造）よりも複雑な構造をもち，それ故に既存のプログ

ネットワーク構造は，インターネットをはじめとしラミング言語では扱うことが難しい．例えば，C 言語て，情報網や交通網，あるいは人間関係など，様々なのようなポインタを扱える言語であれば，ポインタ

分野でみられる．あるいは，ミクロな視点で見ると，の接続構造としてグラフを表現することができるが，例えばコンピュータは各部品が接続関係にあるネット

依然としてダングリングポインタなどの不正なポイワークであり，それらの部品を構成する電子回路は素ンタが発生する危険性がある．

子が相互に接続されたネットワークである．こうしたそこで，グラフを第一級オブジェクトとしてもち，

ネットワークの構造を抽象化・モデル化したデータ構

それを書き換えることによって計算を表現する，グラ造がグラフである．

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

∗ Static Type Checking for Types with Numeric Con-straints 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 [16] は，グラフ書換え言語の一つであり，
アトム（ノード）やルール（書換え規則）といった最小限の言語要素からなる言語モデルである．しかしな
がら，LMNtal は十分な表現力・計算能力をも持ち合わせている．実際，LMNtal はチューリング完全であり，ラムダ計算などの他の言語体系を LMNtal プロ
グラムにエンコードする手法が存在している [9] [10]．

また，LMNtal はプログラミング言語としての側面

Ntal を対象とする幾つかの静的型検査手法が提案さの他に，モデリング言語としての側面を持ち合わせれている．例えば， [10] の手法ではノード間の局所的ている．実際，LMNtal の実行時処理系である SLIM

な繋がりに着目し，入出力の方向性を解析し，それを[17] [15] には，これらの 2 つの側面とそれぞれ対応す−1 から 1 までの実数値（極性）として表現することる 2 種類の実行モードがある．すなわち，LMNtal をで型を付ける．

プログラミング言語とみなす場合には SLIM は実行

一方，本研究で扱う LMNtal ShapeType [13] は，

時処理系となり，モデリング言語とみなす場合にはStructured Gamma [3] およびそのサブセットである

SLIM はモデル検査器となる．特にモデル検査器としShape types [2] を基とした型検査手法である．このての SLIM にはグラフの書換えによって遷移しうる手法では，LMNtal のルールを生成規則として，生全状態を出力する機能があるほか，LTL モデル検査

成文法により型の定義を行う．そのため，SLIM のモなどの機能も充実している．

デル検査機能を用いることによって，LMNtal 自身でLMNtal グラフは well-formed であるかぎり，不正LMNtal の型検査を行えるという利点がある．ある言なポインタを含まない．この意味で，LMNtal は言語語の型をその言語自身で記述し，その言語自身によっ仕様のレベルにおいて不正なポインタを排除しているて型検査を行うという取り組みが統一性の観点から（すなわち，ポインタ安全である）といえる．一方で，興味深いだけでなく，LMNtal の柔軟な表現力をそのLMNtal には静的型の概念がないため，書換えの結果

まま型の定義に活かすことができるのは大きな強みがプログラマの意図しないものとなることがある．

である．

例えば，スキップリスト [6] は線形リストに対して

本論文では，LMNtal ShapeType に対し，ベース

途中の幾つかのノードを通過するようなエッジを追

言語 LMNtal の拡張機能である型付きプロセス文脈

加した，図 1 (a) に示すようなデータ構造である．こを援用することにより，添字付きの非終端記号を表現

れは LMNtal グラフとして図 1 (b) のように表現でし，高さ n の完全二分木や（平衡している）赤黒木，

きる．

あるいは長さ n のリストなどの数値制約を伴うグラ

ここで，スキップリストの n2 ノードが 2 つ並んだフ型を対象とした書換え規則の型検査を行う手法に

ところがあったら，右側を n1 に書き換える，というついて述べる．また，ルールの型検査を既存手法より書換え規則を考え，次の 2 通りを書いたとする．

容易に実装するための手法についても述べ，その正当





性を示す．

n2(X,A,B,C,D), n2(Y,E,F,B,A):- n2(X,A,E,C,D), n1(Y,F,A).







n2(X,A,B,C,D), n2(Y,E,F,B,A):- n2(X,A,F,C,D), n1(Y,E,A).



2 関連研究
本節では，まずグラフを対象とする既存の型検査手法を紹介する．Graph types [5] は正規表現を基にしたグラフの型検査手法である．また，Structured

このように，特にテキスト表現においては，どちらが正しい書換え規則であるかをひと目で判断することは難しい．なお，これらを図に直すと，前者は図 2(a)，後者は図 2 (b) にそれぞれ示す通りの書換え規則になっている．後者は右側のエッジの繋がり方が変わってしまっているので，このルールを適用するとス
キップリストの形状が破壊されてしまうことになる．
こうした問題点を解決するため，これまでにも LM-

Gamma [3] は文脈自由文法を基にした，生成規則によって型を定義する型検査手法である．Shape Types[2] はこの Structured Gamma のサブセットであり，型検査の完全性が満たされるように型定義の範囲を制限したものである．LMNtal ShapeType [13] は ShapeTypes の技法を LMNtal に対して応用し，書換え規則の型検査を行う手法である．以上の手法では，「グラ
フの書換え操作を 1 ステップ進めても，構造が破壊されない」ことの検査・保証を行うことができる．しか

(a)

2

7

13

11

17

19

23

3

5

n2

n1

n1

n2

n1

n2

n1

n1

n2

2

3

5

7

11

13

17

19

23

Nil

List2
List1

nil

(b)

(a)

図1

スキップリスト： (a) グラフによる表現 および (b) LMNtal グラフによる表現

n2

n2

:-

n2

n1

3 グラフ書換え言語 LMNtal
本節では，グラフ書換え言語 LMNtal について簡単に説明する．なお，本来 LMNtal には膜による階

(b)

n2

n2

:-

n2

n1

層や，ルールの発火に関する制約条件を記述するためのガード及びプロセス文脈といった機能が備わっているが，本論文では簡単のためこれらを除外したサブ

図2

スキップリストの書換え規則： (a) 正しいもの および (b) 誤ったもの

セット言語を扱う．また，LMNtal の拡張言語である

HyperLMNtal [11] において導入された拡張機能である，超辺を表すハイパーリンクについても扱わない．

し，その対象となる型の表現力には後述する文脈自由

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

性による制限があり，完全二分木や赤黒木などの数値もまたチューリング完全であり，プログラミング言語

制約の入った型を表現することはできていなかった．

としてもモデリング言語としても十分強力である．

また，「二分木を入力するとリストが出力される」のように操作の前後で型が変化する場合や，「リストを 2

3. 1 構文

本入力すると 1 本のリストが出力される」のように

LMNtal の構文を図 3 に示す． LMNtal プログ

複数の構造を入力にとる場合について対応していな

ラムは，グラフ（アトムの多重集合）とルールセッ

かった．そこで [14] では，LMNtal でよく用いられるト（ルールの多重集合）の組として表現され，これデザインパターンの「関数的アトム」に着目して，以をプロセスと呼ぶ．p という名前で， m 本のリンク

上のような複数ステップを要し，かつ型の変化を伴う

X1 , . . . , Xm をもつアトムを p (X1 , . . . ,Xm ) と書ようなグラフ操作について型検査を行う手法についく．これらのリンクをアトムの引数といい，順序がつて述べた．

いている．英字の大文字から始まる名前はリンク名，

一方で，関数型言語をベースとした型体系では，型

そうでないものはアトム名として解釈される．アトに対して述語による数値制約を掛ける手法として篩型

ム名と引数の本数（価数）の組をファンクタといい，（reﬁnement types [12]）が知られている．また，このp/m のように書き，「m 価の p アトム」のように読む．

篩型を述語抽象化によって自動的に推論する手法とし

LMNtal におけるアトム・リンクは，それぞれグラフて Liquid Types [7] が存在する．他のアプローチとし理論における節点（ノード）・辺（エッジ）と対応して，赤黒木の型を高階型などの機能を用いて表現するている．

研究 [4] もある．

LMNtal においては，アトムの多重集合によって無向多重グラフを表現する（つまり，多重辺や自己ルー




プロセス

P ::= G,R
グラフ

ルールセット（空）| [ RuleName @@ ] G :- G



(E2)

P ,Q ≡ Q,P(E3)

P ,(Q,R) ≡ (P ,Q), R（分子）

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

(E7)

X=X ≡ 0(E8)

X=Y ≡ Y =X
X=Y ,P ≡ P [Y /X]

(E9)

（ルール）

| R,R

P ≡ P [Y /X]

(E5)

（分子）

R ::= 00,P ≡ P

（X は P の局所リンク）| p (X1 , . . . ,Xm ) （アトム, m ≥ 0）
| G,G

(E1)

(E4)

（空）

G ::= 0

（P はアトム，X は P の自由リンク）





図5

図3

LMNtal グラフ上の構造合同関係

LMNtal の構文

1 価の a アトムを，1 価の b アトムに書き換えるルールである．便宜上，ルールの名前として RuleN ame

c

F

a

をルールの前に付すこともある．また可読性のため

bに，ルールはカンマで区切るかわりに，ピリオドで終d
図4

わる形で書かれることもある．なお，書換えの前後において自由リンクの本数が増減することはあり得な

LMNtal グラフの例

いので，ルール中に同じリンクはちょうど 2 回だけ出現する．

プの出現を許す）．例えば，a(A,F), b(A,C,L1,L2), c(C,D,S,S), d(D,L1,L2)というアトムの多重集合は，図 4 に示すような無向3. 2 意味論

グラフを意味する．図中において矢印は第 1 引数のLMNtal の意味論は，構造合同と遷移規則からな場所を指しており，そこから矢印の向きに従って引数る．これらについて順に説明する．

に順序がついていることを示す．
グラフはいずれも次のリンク条件を満たす：



グラフ中に同名のリンクは高々 2 回出現する．



3. 2. 1 構造合同



グラフ理論における “同型” にあたるものとして，

LMNtal にはグラフ間の構造合同関係 “≡” が存在す

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

グラフ中に 2 回出現するリンクは両端がアトムと繋として定義される．構造合同な LMNtal プロセスはがっている局所リンクであり，1 回のみ出現するリン互いに 0 ステップで変換可能である．なお，P [Y /X]

クは一端が無接続である（または，外部と接続していはグラフ P に出現するリンク X をリンク Y に置きる）自由リンクである．自由リンクのないグラフは閉換えることを意味する．ただし，(E6), (E10) は膜にじているという．2 つのグラフをカンマで結合する際関する規則であるので省略した． (E1)–(E3), (E5) はは，局所リンク名が衝突しないように α 変換されたプロセス計算にもみられる一般的な規則であり，(E4)

ものとみなす．

は局所リンク名の α 変換である．(E7) から (E9) ま

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

では特別な 2 価のアトムであるコネクタに関する規則

を表す書換え規則である．例えば，a(X) :- b(X) はである．=(X, Y ) は二つのリンク X, Y を接続するという意味を持ち，中置記法で X = Y とも書く．(E7) 3. 3 略記法



より簡潔な記述を可能にするため，次の二つの略記

T :- U

G1 −−−−−−→ G′1

(R1)

(R3)

法が認められている．

T :- U

G1 ,G2 −−−−−−→ G′1 ,G2
G2 ≡ G1

T :- U

G1 −−−−−−→ G′1

1. アトムの引数にアトムを書いた場合は，そのアトG′1 ≡ G′2

ムの最終引数に繋がっているものと解釈される．つT :- UG2 −−−−−−→ G′2

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

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

(R6)



図6



p(X1 , . . . ,L, . . . ,Xm ), q(Y1 , . . . ,Yn ,L) と解釈される．ただし，L は使用されていない
適当なリンク名とする．例えば，a(b(c),d) はLMNtal グラフ上の遷移関係

a(B,D),b(C,B),c(C),d(D) を意味する．
は一つのリンクの両端が繋がって輪になっているもの

2. 引数リストを省略した場合は引数が 0 個であるは空とみなして良いこと，(E8) はリンクが対称であと解釈される．つまり，p は p() の意味である．

る（つまり無向である）こと，(E9) は直接接続されている二つのリンクが一つのリンクに縮約できるこ

4 LMNtal ShapeTypeとを表している．

本節では，LMNtal を対象とする静的な型検査手法

3. 2. 2 遷移規則

である LMNtal ShapeType を紹介する．まず，形式

LMNtal における本質的な計算ステップを表す，グ的な定義を先に示しておく．なお，以下で “記号” とラフ間の二項関係として，ルール T :- U によるグ言うときは，LMNtal のファンクタのことを指す．

T :- U

ラフの遷移関係 “−−−−−→” が存在する．これは，図定義 1. LMNtal ShapeType における型（以下，こ6 に示す遷移規則をみたす最小の二項関係として定義

れを単に “ShapeType” という）は，3 つ組 (S, P, N )される．ただし，(R2), (R4), (R5) は膜に関する規である．ここで，則であるので省略した． 最も本質的で重要な規則は• S = t/m は，開始記号と呼ばれるファンクタ(R6) である．これは，「ルールと，その左辺にパター• P は，生成規則と呼ばれるルールの有限集合

ンマッチするプロセスが存在したら，その左辺を右辺• N は，非終端記号と呼ばれるファンクタの有限に書き換えてよい」ということを言っている．
また，この定義を自然にルールセットへと拡張する
r集合とする．ただし，S ∈ N とする．

⋄′

ことができる．すなわち，∃r ∈ R. G −−→ G が成り立つとき「ルールセット R によって，グラフ G が（14. 1 構文ステップで）G′ に遷移する」といい，単に G −−→ G′

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

R

と書く．

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

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

生成規則の左辺は 1 つ以上の（コネクタでない）非ルの多重集合であるプロセスが，遷移関係に基づい

終端アトムのみからなる．また，LMNtal と同様の略ておのずから書き換わっていく．そのため，「ルール

記法（3. 3 節）を認める．

による作用を受けてグラフが書き換わる」とは考えな

nonterminal{N } は S 以外の非終端記号の宣言でい．しかしながら，書換えに関する静的な性質についあり，無ければ省略して良い．S や N の要素はファて定義および議論をするにあたっては，書換えの主体ンクタであってアトムではないので，本来であればたるルールと客体たるグラフとは明確に分離されていf /n の形式で記述するべきである．しかし，以下の 2

たほうが都合が良い．よって，本論文では LMNtal のつの理由から非終端記号はファンクタの形式ではなく構文・意味論を簡明な形に等価変換して扱っている．

自由リンク名を明示したアトムの形式で記述するほうが表記上自然である：



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

ShapeType::=defshape S { P } [ nonterminal{ N } ]のアトム名 t と，適当なリンク名 L1 , . . . , Lm を用いて t(L1 , . . . ,Lm ) 型などと呼ぶことにする．ただし，

開始記号

S

::=

p(X1 , . . . ,Xm )リンク名が重要でないときは開始記号のファンクタ

生成規則の有限集合

P::=を用いて t/m 型（あるいは m 価の t 型）と呼び，誤0 | [ RuleN ame @@ ] A :- A | P ,P

解のおそれがないときは価数も省略して単に t 型と非終端記号の有限集合

N

::=

呼ぶ．

A

アトムの有限集合



A

::=

0 | p(X1 , . . . ,Xm ) | A,A

図7

4. 2 意味論

 型付け関係 “ : ” を定義するにあたって，補助的な型
付け関係 “◁” を先に定義する．以下では，L1 , . . . , Lm

ShapeType の構文だけを自由リンクに持つグラフを G[L1 , . . . , Lm ] と1. s(L1 , . . . , Ln ) という非終端記号（開始記号を書く．また，グラフ G 中で使用されているファンク含む）は，そこから生成されるグラフの全体，すタ全体の集合を，Funct(G) と表す．

なわち

定義 2. 型 (t/m, P, N ) について，
P ∗{G | s(L1 , . . . , Ln ) −→ G}P
t(L1 , . . . ,Lm ) −→* G[L1 , . . . , Lm ]を代表しており，L1 , . . . , Ln はそのように生成であるとき，かつそのときに限り，G[L1 , . . . , Lm ]されるグラフ G の自由リンクの名前としても用は t(L1 , . . . ,Lm ) 型 に よって生 成 さ れ ると い い ，いられるG[L1 , . . . , Lm ] ◁ t(L1 , . . . ,Lm ) と書く．

⋄

2. 代数的データ型（二分木やリスト等）ではデー

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

タ構造の根が一つであるのに対して，LMNtal

よって 0 ステップ以上遷移した先のグラフだけが t 型

ShapeType が対象とするグラフ構造の根（自由によって生成されることを表す．

リンク）は一つとは限らず，かつそれらの自由リ
ンクにはそれぞれ異なる役割がある（非可換で次に，型付け関係 “ : ” を定義する．
定義 3. 型 (t/m, P, N ) について，

G[L1 , . . . , Lm ] ◁ t(L1 , . . . ,Lm )ある）
例えば，1 節で紹介したスキップリストの場合，次のように型定義できる．



defshape skiplist(List2,List1){
p0@@ skiplist(L2,L1) :- nil(L2,L1).
p1@@ skiplist(L2,L1):- n1(X1,L1), skiplist(L2,X1).
p2@@ skiplist(L2,L1):- n2(X1,X2,L2,L1), skiplist(X2,X1).
}



かつ



Funct(G[L1 , . . . , Lm ]) ∩ N = ∅であるとき，かつそのときに限り，G[L1 , . . . , Lm ]は t(L1 , . . . ,Lm ) 型をもつといい，G[L1 , . . . , Lm ] :t(L1 , . . . ,Lm ) と書く．

⋄

これは直観的には，t 型によって生成されるグラフのうち，非終端記号を含まないグラフのみが，t 型を

もつことを表す．

なお，図 1 (b) で示したスキップリストの各ノードには整数型の要素が繋がっているが，以降の本論文中ではグラフの形状を重視するために，こうしたデータ

また，前節で述べた通り，開始記号および（型付けの対象である）グラフの自由リンクの名前と順序の対応関係は重要である．例えば，構造に含まれるデータは省略して考える．例えば，上defshape t(X,Y) { t(X,Y) :- a(X,Y) },記の型をもつグラフは図 8 に示すような形状をしてという型があったときに，a(X,Y) ◁ t(X,Y) であるが，a(Y,X) ◁ t(X,Y) ではない．

List2
List1

n2

n1

n1

図8

n2

n2

n2

n1

n1

n2

nil

要素を無視したスキップリスト型グラフの例

グラフの型検査は，開始記号に生成規則を 0 回以

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

上適用して検査対象グラフ G に遷移できるかを検査手法がある．一つは，グラフの型検査である．これすればよい．そのため，逆に検査対象グラフ G からは，与えられたグラフが，与えられた型に属している

出発し，生成規則の反転を 0 回以上適用して開始記かを検査するものである．もう一つは，ルールの型検号に遷移できるか否かを調べればよい．これは一見す査である．これは，ルールと型が与えられたときに，ると同じことのようであるが，生成規則の適用によりルールの適用によって型の構造が破壊されないことを生成される状態空間は（その型をもつグラフの個数が検査するものである．

有限でない限り）一般に無限であるので，後者のほう

ルールの型検査について，もう少し形式的に解説する．まず，型 t に関する LMNtal ルール r の型保存が検証しやすいと言える．
一方で，ルールの型検査はより複雑である．本論文

性を定義する．

では，文献 [13] や Structured Gamma [3] の手法とは定義 4. ルール r と型 t/m およびリンク列 L1 , . . . , Lm

異なる，実装が容易な検査手法を紹介する．この検査について，全ての G : t(L1 , . . . ,Lm ) が，手法では，検査対象のルールそれ自体を書き換えてい

r

′

′

G −−→ G ⇒ G : t(L1 , . . . ,Lm )き，LMNtal ルールを状態とみなして状態空間を生を満たすとき，かつそのときに限り，r は t 型を保存成する．この考え方は，前提と結論のペアを一つのま⋄とまりとして捉えるという点で，シーケント計算の考するという．

自然言語で表現すると，「t 型をもつ全てのグラフ

え方と近い．

G は，ルール r を（可能なら）適用した後も，t 型をまず，各生成規則 α :- β について，β ≡ β1 ,β2 か持っている」という性質である．このルールの型保存

つ β1 が空でないようなグラフ β1 , β2 をとる．ここで，性の検査のことを，単にルールの型検査という．

状態 L : −R に対し，L ≡ β1 ,L′ であるならば，この状態を α,L′ :- β2 ,R へと書き換えるような書換え規

4. 4 具体的な検査手法

則を作成する．以上のようにして得られる全ての書換

LMNtal ShapeType においては，生成規則が LM-

え規則をルールセットとし，検査対象ルールを初期状

Ntal 自身のルールとして記述されていることから，態として状態空間を生成する．こうしてできた状態

LMNtal を対象言語とするモデル検査器 SLIM [17] を空間において，初期状態から出発して，左辺が開始記用い，生成規則の逆実行により実際にグラフの型検号であるような状態へと到達するような任意の経路

査・ルールの型検査を行うことができる．

上に，必ず reducible（左辺から右辺へと生成規則を定義 5. LMNtal ルール r = T :- U の反転 r

r

inv

inv

を，

≜ U :- T で定める．同様に，LMNtal ルール

検証すれば，型保存性を検査できる．

| r ∈ R} で型検査の正当性に関連する詳細な定義と証明は⋄付録にあるが，概略は次の通りである．まず，以上

つまり，反転とはルールの左辺と右辺を入れ替えたの手順で生成される状態空間を Kripke 構造の形でセット R の反転 R

inv

を，R

inv

≜ {r

0 回以上適用して遷移可能）な状態が存在することを

inv

定める．
r

′

′

r inv

ものである．ここで，G −→ G と G −−−→ G が同値

S = (W, T , L) と定義する．ただし，W は LMNtal

であることが LMNtal の遷移規則および構造合同規ルール全体の集合であり，L : W → 2{s,r} は状態へ則から容易に示せる．

のラベル付け関数である．ここで原子命題 s は “startsymbol” の頭文字であり，左辺が開始記号であること

reducibility の検査を行い，それ以上は遡らない．こを指す．r は前述の “reducible” を意味する．その上れにより完全性が幾分損なわれるが，もとよりルー

で，以下の定理を示す．ただし，T は検査対象の型，

ルの型検査は決定不可能問題であることが [3] においr は検査対象の書換え規則を表す．

て示されており，かつ [3] においても同様に探索の打定理 1. S, r |= ¬s W r ならば，r は T 型を保存する．

ち切りを行っていることから，型検査の能力を損なっ

ここで，W は “weak until” を意味する時相論理ていることにはならない．

演算子であり，P W Q は「Q が成り立つまでずっと

また，ルール自体を書き換える書換え規則や，左辺P が成り立つ，またはいつでも P が成り立つ（つまが同じ状態を同一とみなしての状態空間構築などは，り，(P U Q) ∨ G P ）」を意味する．よって，ここでのLMNtal メタインタプリタ [8] の機能を利用すれば実S, r |= ¬s W r は，
「r から出発して Kripke 構造 S に現できる．

従って遷移できる全ての経路上において，reducibleな状態にたどり着くまでは左辺が開始記号となるこ

4. 5 生成規則及び型の文脈自由性とはない．ただし，左辺が開始記号となる状態が存在

LMNtal ShapeType および 2 節で紹介したグラフ

しない経路では，reducible な状態が存在しなくてもを対象とする既存手法では，生成規則の形に次のよう良い」ことを表している．

な制限を加えることでルールの型検査の停止性を担

文献 [13] や Structured Gamma [3] における手法で保していた．

は，(i) 検査対象ルールの左辺を基にそれとマッチし定義 6. 生成規則 p = α :- β について，α がただ一うるグラフのパターンを導出するために，必要なグラ

つのアトムからなり，β がコネクタ以外のアトムを一フを補うことを許して生成規則により逆向きに遷移しつ以上含むとき，p は文脈自由な生成規則であるといて状態空間を構築し，(ii) 開始記号に到達するようなう．また，生成規則が全て文脈自由である型を文脈自全ての経路を列挙して，(iii) その経路上で左辺に補っ由な型という．

⋄

たグラフと同じものを右辺にも補い，開始記号から右

文脈自由な型についてのルールの型検査における状

辺に遷移できることを確かめる，という手順を踏ん

態空間が必ず有限となることは既に分かっているが，でいた．この場合，左辺に補ったグラフを状態空間のこれより広い型のクラスについては自明でない．

エッジ上に記録しておく必要があり，かつ左辺の自由リンクと補ったグラフの自由リンクとの接続関係を，

5 数値制約のある型

右辺に補う際に適切に再現することが実装上困難でここまでに述べた手法により，二分木や線形リスト

あった．実際，文献 [13] でも，実装のためには SLIMといった代数的データ型についてはもちろん，根（自に何らかの改造を施す必要がある，とされていた．

由リンク）が複数あるスキップリストや差分リスト，

一方で，本論文の手法では左辺を基にした逆向き

あるいはルートが一つもないリング構造のように，代の遷移と，右辺へのグラフの補完とを同時に行ってお数的データ型では表現ができないグラフの型も表現

り，かつそれらの手続きは全て LMNtal の上で完結することができる．

しているので，実装が容易である．

しかし，高さ n の完全二分木や（平衡している）赤なお，本論文の手法で生成される状態空間はその黒木，あるいは長さ n のリストといったような数値ままでは一般に有限とならない．そのため，実際の実制約の付いた型は表現することが難しい．もちろん，装においては左辺が同じ状態は同一とみなして状態

文脈自由でない型を許せばこうした型を表現するこ空間を構築する．ただし，このように左辺の構造合同とはできるが，その場合は型検査の停止性が自明でな関係で商を取った状態空間で，初期状態から左辺が開くなる．

始記号であるような状態へ至る経路上に閉路が出現

一方で，数値制約が定数であるもの，例えばちょうする場合，その閉路に進入した最初の状態においてど高さが 3 の赤黒木は次のように文脈自由な型で表すことができる．



defshape rbtree3(R){init@@ rbtree3(R) :- btree3(R).
bb3@@ btree3(R) :- b(tree2,tree2,R).
bb2@@ btree2(R) :- b(tree1,tree1,R).
bb1@@ btree1(R) :- b(tree0,tree0,R).
bl@@ btree0(R) :- leaf(R).
tb2@@ tree2(R) :- b(tree1,tree1,R).
tb1@@ tree1(R) :- b(tree0,tree0,R).
tr2@@ tree2(R) :- r(btree2,btree2,R).
tr1@@ tree1(R) :- r(btree1,btree1,R).
tr0@@ tree0(R) :- r(btree0,btree0,R).
tl@@ tree0(R) :- leaf(R).
} nonterminal {rbtree3(R), btree3(R), btree2(R),btree1(R), btree0(R),tree2(R), tree1(R), tree0(R)}はガード部（ :- と | に挟まれた部分）で指定される制約を満たす任意のグラフにマッチする機構である．しかし，ここでは全ての型付きプロセス文脈は自然数 †1 にのみマッチするものとする．この拡張では，生成規則の左辺に非終端記号 1 つの他に，任意個の自然数や型付きプロセス文脈の出現を許す．これにより「生成規則の左辺はただ一つのアトムのみからなる」という文脈自由性の前提を崩しているが，この自然数は元々非終端記号の添字の役割を担っており，非終端記号の付属物であるとみなすことができるので，本質的には文脈自由である．なおこうした添字付きの
非終端記号という着想は，形式言語理論におけるイン
デックス文法（indexed grammar [1]）から得たもの

である．

これらのプロセス文脈は任意の自然数値をとる変ここで登場した非終端記号のうち，btreeN は高さ N

数のようなものである．よって，無限通りの値をとる

かつ根が黒である赤黒木，treeN は黒高さ N の赤黒ことが考えられ，状態空間が爆発する危険がある．そ木（根は赤でも黒でもよい）を表し，終端記号の r は
赤ノード，b は黒ノード，leaf は葉ノードを表す．なお，黒高さとは根から葉に至るまでの経路上に出現する黒ノードの数である．赤黒木の性質上，黒高さは葉

この定義において，bb3 から bb1，tb2 から tb1，
あり，非終端記号の添字が変わっているにすぎない．
よって，次のように簡略化することができると考えら

defshape rbtree(R){init@@ rbtree(R) :- btree($n,R).
bb@@ btree($n,R):- $m = $n-1 | b(tree($m),tree($m),R).
bl@@ btree(0,R) :- leaf(R).
tb@@ tree($n,R):- $m = $n-1 | b(tree($m),tree($m),R).
tr@@ tree($n,R):- r(btree($n),btree($n),R).
tl@@ tree(0,R) :- leaf(R).
} nonterminal {rbtree(R), btree($n,R), tree($n,R)}

れにより，見かけ上は添字を導入する前と同一の状態

が，前述のちょうど高さが 3 の赤黒木の例のように文
脈自由な型の範囲で表現された型の場合と比べると，

tr2 から tr0 はそれぞれほとんど同一の生成規則でけの違いは無視し，同一状態とみなすこととする．こ空間が生成されるため，型検査の停止性が保証されるによらず一定であることが要求される．

れる．

のため，状態空間構築においては非終端記号の添字だ

複数の状態が一つの状態に抽象されるため，4. 4 節で述べたのと同様に，型検査の完全性を少し損なうこととなる．しかしながら，添字を導入することは型定義

の記述の簡潔性からも重要であり，かつ添字を導入せずに任意の高さの赤黒木を表現することは不可能であるから，全体としては型の表現力は向上している．

5. 1 型検査の手順
ここでは，例として以下のルールの型検査を行う．

b(S,leaf,R) :- b(S,r(leaf,leaf),R)

これは赤黒木へのノードの挿入のうち最も単純な（木の回転を必要としない）例である．まず，生成規則



ここで新たに $n といった記法を導入した．これは型付きプロセス文脈 [18] と呼ばれる LMNtal の拡張機能に由来するものである．本来の型付きプロセス文脈

tl を逆向きに使って，左辺の leaf を tree に戻す．
†1 LMNtal における数は，その数をアトム名に持つ 1
価のアトムとして表現される．





様に，初期状態から生成規則 tb を使った場合以下を

b(S,tree(0),R) :- b(S,r(leaf,leaf),R)

得るが，これも生成規則 tb により reducible である．



続いて，自由リンク S の先に tree(0) を補いつつ，
生成規則 tb を逆向きに使って，左辺全体を tree に戻す．

tree(1,R) :- b(tree(0),r(leaf,leaf),R)

tree(n + 1,R) :- b(tree(n),tree(n),R)

以上によりルールの型保存性が検証できた．



以上のような，具体値が必ずしも定まっていないが制約条件が存在するような数を含むグラフに対する

このルールは reducible である．実際，次の手順で左

操作は，一見すると自然なように思われる．しかし，こうした不定数を記号的に扱う機能は現在の LMNtal

辺から右辺へと遷移できる．

の組み込み機能には存在しない．そのため実装にあtree(1,R)tb

たっては，現在の型検査実装に用いている LMNtaltr

メタインタプリタを拡張して，数値に関する記号制約

blを扱えるようにするなどの工夫が必要である．

−−→ b(tree(0),tree(0),R)−−→ b(tree(0),r(btree(0),btree(0)),R)−−→ b(tree(0),r(leaf,btree(0)),R)bl−−→ b(tree(0),r(leaf,leaf),R)

6 まとめと今後の課題

また，生成規則 tb の代わりに bb を逆向きに使うと，
次を得る．



btree(1,R) :- b(tree(0),r(leaf,leaf),R)

象とした書換え規則について型検査を行う手法につ

いて述べた．また，ルールの型検査の実装をより容易

これもまた reducible である．実際の遷移経路は，先ほどのものとほとんど同一であるので割愛する．こが，その先は行き詰まり状態であって左辺が開始記号となることはないので，この経路は考えなくて良い．
以上により，ルールの型保存性が示された．

b(A,B,R) :- b(B,A,R)にルールの型検査のプロトタイプは実装済みであり，

4. 3 節で述べた手法により初期グラフの生成を除く全述べた型付きプロセス文脈による拡張には未対応であは，その添字に任意性があるため上記のように単純でたプロトタイプの実装および応用が挙げられる．既部分を LMNtal で実装した．しかし，これは 5 節で補うグラフに添字付き非終端記号が含まれる場合

にする手法についても述べ，その正当性を示した．
今後の課題としては，型付きプロセス文脈に対応しれ以外に初期状態から bl を使って戻ることもできるはない．例えば，次のルールを考える．

本論文では，型付きプロセス文脈により添字付きの非終端記号を表現することで，数値制約付きの型を対る．この実装ができれば， [14] で述べた関数的アトム

の型検査と組み合わせることにより，赤黒木への挿入
操作のように，数値制約を伴う型を対象とした，複数ステップを要し，あるいは型の変化を伴うようなグラ

これは単に黒ノードの左右の部分木を入れ替えるルー

フ操作についても型検査が可能になると考えられる．

ルである．あまり実用的でなくかつ型保存性が直感的

謝 辞 本 研 究 の 一 部 は ，科 学 研 究 費 基 盤 研 究 (B)には明らかであるが，この型検査にあたっては添字の18H03223 の助成を受けて実施した．

取扱いが難しい．まず自由リンク A と B の先に黒高
さ n の tree を補いつつ，生成規則 bb を逆向きに使い，次を得る．



参 考 文 献 [ 1 ] Aho, A. V.: Indexed grammars – An extensionof context free grammars, 8th Annual Symposium
on Switching and Automata Theory (SWAT 1967),
 1967, pp. 21–31.
[ 2 ] Fradet, P. and Métayer, D. L.: Shape types,
このルールは生成規則 bb により reducible である．同
Proc. POPL’97, ACM, 1997, pp. 27–39.

btree(n + 1,R) :- b(tree(n),tree(n),R)[ 3 ] Fradet, P. and Métayer, D. L.:
Structured Gamma, Science of Computer Programming,Vol. 31, No. 2(1998), pp. 263–289.
[ 4 ] KAHRS, S.: Red-black trees with types, Journalof Functional Programming, Vol. 11, No. 4(2001),
pp. 425–432.
[ 5 ] Klarlund, N. and Schwartzbach, M. I.: Graph
Types, Proc. POPL’93, 1993, pp. 196–205.
[ 6 ] Pugh, W.: Skip lists: A probabilistic alternative to balanced trees, Commun. ACM, Vol. 33,
No. 6(1990), pp. 668–676.
[ 7 ] Rondon, P. M., Kawaguci, M., and Jhala,R.: Liquid Types, Proc. PLDI 2008, ACM, 2008,
pp. 159–169.
[ 8 ] Tsunekawa, Y., Tomioka, T., and Ueda, K.:
Implementation of LMNtal Model Checkers: A
Metaprogramming Approach, Journal of Object
Technology, Vol. 17, No. 1(2018).
[ 9 ] Ueda, K.: Encoding the Pure Lambda Calculus
into Hierarchical Graph Rewriting, Proc. RTA2008,
Voronkov, A.(ed.), LNCS, Vol. 5117, Springer, 2008,
pp. 392–408.
[10] Ueda, K.: Towards a Substrate Frameworkof Computation, Concurrent Objects and Beyond,Agha, G. et al.(eds.), LNCS, Vol. 8665, Springer,
2014, pp. 341–366.
[11] 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.
[12] Vazou, N., Seidel, E., Jhala, R., Vytiniotis,
D., and Peyton Jones, S.: Reﬁnement Types For
Haskell, ACM SIGPLAN Notices, Vol. 49(2014).
[13] 吉元佑介, 上田和紀: グラフ書換え系における静的
グラフ型検査, 日本ソフトウェア科学会第 32 回大会(2015 年度) 講演論文集, 2015.
[14] 山本直輝, 上田和紀: グラフ書換え言語におけるグラフ操作の静的型検査, 日本ソフトウェア科学会第 36
回大会 (2019 年度) 講演論文集, 2019.
[15] 後町将人, 堀泰祐, 上田和紀: LMNtal 実行時処理系の並列モデル検査器への発展, コンピュータ ソフトウェ
ア, Vol. 28, No. 4(2011), pp. 4 137–4 157.
[16] 上田和紀, 加藤紀夫: 言語モデル LMNtal, コンピュー
タ ソフトウェア, Vol. 21, No. 2(2004), pp. 126–142.
[17] 石川力, 堀泰祐, 村山敬, 岡部亮, 上田和紀: 軽量なLMNtal 実行時処理系 SLIM の設計と実装, 情報処理学会第 70 回全国大会講演論文集, (2008), pp. 153–154.
[18] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal, コンピュータ ソフトウェア, Vol. 25,
No. 1(2008), pp. 124–150.

A ルールの型検査の正当性証明
LMNtal ルール α1 :- β1 と α2 :- β2 との間の遷移

関係 T を，T

α1 :- β1 −−→ α2 :- β2iﬀ∃αp :- βp ∈ P. ∃γ, γ ′ .
αp :- βpα2 −−−−−−→ α1 ,γ ∧ β2 ≡ β1 ,γ∧ βp ≡ γ,γ ′ ∧ γ ′ ̸≡ 0で定める．また，W を LMNtal ルール全体の集合とし，ラベル付け関数 L : W → 2{s,r} を次で定める．なお，原子命題 s は “start symbol”，r は “reducible”を意味する．ただし，ここでの ≡ は自由リンク名の違いを無視する．

s ∈ L(α :- β)

iﬀ

α≡T

r ∈ L(α :- β)iﬀ

α −→∗ βP

このとき，Kripke 構造 S = (W, T , L) を考える．
この Kripke 構造の意味する状態空間は，4. 3 節で述べた手法により構築される状態空間と同一である．以下，S, r |= ¬s W r が型保存性の十分条件であること
を示す．
T

−
→ α′ :- β ′補題 1. α :- β が reducible で，α :- β −なら，α′ :- β ′ も reducible．

Proof. 仮定より α −→∗ β である．また，T の定P

義から ∃γ. α′ −→ α,γβ ′ ≡ β,γ である．よって，
Pα′ −→ α,γ −→∗ β,γ ≡ β ′ ，すなわち α′ −→∗ β ′ で
P

P

P

ある．
補題 2. P ,Q ≡ R,S のとき，P ≡ A1 ,A2 , Q ≡A3 ,A4 , R ≡ A1 ,A3 , S ≡ A2 ,A4 を 満 た す
A1 , A2 , A3 , A4 が存在する．
Proof. 構造合同規則より明らか．
α :- β補題 3. P −−−−→ Q のとき，P ≡ C,α, Q ≡ C,βを満たす C が存在する．

Proof. 構造合同規則と遷移規則から明らか．
p

補題 4. X −→ Y ≡ α,C (p = αp :- βp ∈ P ) のとき，以下のいずれかが成り立つ．
T• ∀β. ∃α′ , β ′ , C1 , C2 . α :- β −−→ α′ :- β ′∧ C ≡ C1 ,C2 ∧ X ≡ α′ ,C2 ∧ β ′ ≡ β,C1p

• ∃C ′ . X ≡ α,C ′ ∧ C ′ −→ Cp

Proof. X −→ Y と補題 3 より，X ≡ αp ,Cp , Y ≡βp ,Cp なる Cp が存在する．Y ≡ βp ,Cp ≡ α,C な

α,C, G′ ≡ β,C なる C ∈ G(N ∪ Σ) が存在する．
次に，i = 0, . . . , n − 1 について，Xi ≡ αi ,Ci ならば以下を満たす αi+1 , βi+1 , Ci+1 が存在することを示す．
Tαi :- βi −−→∗ αi+1 :- βi+1

ので，補題 2 より C ≡ C1 ,C2 , α ≡ C3 ,C4 , βp ≡∧ Xi+1 ≡ αi+1 ,Ci+1

C1 ,C3 , Cp ≡ C2 ,C4 なる C1 , C2 , C3 , C4 が存在する．
C3 ̸≡ 0 の場合∧ βi+1 ,Ci+1 −→∗ βi ,CiPp

ここで α′ = αp ,C4 , β ′ = β,C1 とおく．α′ ≡pαp ,C4 −→ βp ,C4 ≡ C1 ,C3 ,C4 ≡ α,C1 なので ，C1 を T の 定 義 に お け る γ ，C3 を γ ′ とi
Xi+1 −−→
Xi と補題 4 より，以下のいずれかが成り立つ．

1. ∃αi+1 , βi+1 , Ci′ , Ci+1 .
T

αi :- βi −−→ αi+1 :- βi+1 ∧ Ci ≡ Ci′ ,Ci+1

T

見做すと，α :- β −−→ α′ :- β ′ である．また，X ≡ αp ,Cp ≡ αp ,C2 ,C4 ≡ α′ ,C2 である．
C3 ≡ 0 の場合
C1 ≡ βp なので，C ≡ βp ,C2 である．よって，p

αp ,C2 −→ C となる．ここで C ′ ≡ αp ,C2 とp

おくと，C ′ −→ C である．一方，α ≡ C4 なので，Cp ≡ C2 ,α である．よって，X ≡ αp ,Cp ≡αp ,C2 ,α ≡ α,C ′ である．

∧ Xi+1 ≡ αi+1 ,Ci+1 ∧ βi+1 ≡ βi ,Ci′pi
2. ∃Ci+1 . Xi+1 ≡ αi ,Ci+1 ∧ Ci+1 −−→Ci

1. の場合，βi+1 ,Ci+1 ≡ βi ,Ci′ ,Ci+1 ≡ βi ,Ci となることから明らか．一方，2. の場合は αi+1 = αi , βi+1 =βi とおけば明らか．
T−→∗ αn :- βn かつ T ≡ αn ,Cn
以上から，α :- β −かつ βn ,Cn −→∗ β,C なる αn , βn , Cn が存在する．
P

ここで，T は開始記号の（自己ループを含まない）ア定理 2. S, r |= ¬s W r ならば，r は T 型を保存する．

トム一つからなるので，Cn ≡ 0 であり，T ≡ αn でProof. G◁T および G −→ G′ ならびに S, r |= ¬s W r

ある．よって，s ∈ L(αn :- βn ) である．

rを仮定して G′ ◁ T を示す．

G ◁ T のとき，非負整数 n とグラフ X0 , . . . , Xn
(X0 = G, Xn = T ) および p0 , . . . , pn−1 ∈ P があっpiて，∀i < n. Xi+1 −−→ Xi である．

G −→ G′ なので，r = α :- β とすると，G ≡
r

T

r−
−
→∗ αn :- βn と S, r |= ¬s W r および補題 1 より，r ∈ L(αn :- βn ) でもある．つまり αn −→∗ βnP

P ∗である．よって，T ≡ αn −→ βn −→ β,C ≡ G′
なので，G′ ◁ T となる．

P ∗