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

データ構造としてのグラフを対象とした型の表現力
拡張
山本 直輝

上田 和紀

グラフ書換え言語 LMNtal は，グラフの書換えによって計算を表現するプログラミング言語としての側面と，一般の複雑なグラフ構造を扱えるモデリング言語としての側面とを兼ね備えた言語である．グラフ書換え言語では，関
数型言語で扱える代数的データ構造よりも広範な構造を扱えるため，計算対象となるグラフの型の定式化が課題となっている．そこで我々は，グラフの型に関する枠組みとして，形式文法に基づいた LMNtal ShapeType を提案
し，文脈自由を超えた広範な型に対応した型検査手法を定式化してきた．しかし，ラムダ式のグラフによる表現やグ
リッドグラフなど，ルートの本数が一定でない型については，型の定義や検査手法が他の型に比べても自明でない．
そこで本論文では，LMNtal ShapeType の定義および検査手法に対して拡張を施すことで，以上のようなグラフ型を対象とする型検査手法の定式化を目指す．

ンタが発生する危険性がある．

1 はじめにそこで，グラフを第一級オブジェクトとしてもち，

ネットワーク構造は，インターネットをはじめとしそれを書き換えることによって計算を表現する，グラて，情報網や交通網，あるいは人間関係など，様々なフ書換え言語というパラダイムが提案されている．

分野でみられる．あるいは，ミクロな視点で見ると，

LMNtal [20] は，グラフ書換え言語の一つであり，

例えばコンピュータは各部品が接続関係にあるネット

アトム（ノード）やルール（書換え規則）といった最ワークであり，それらの部品を構成する電子回路は素小限の言語要素からなる言語モデルである．しかしな子が相互に接続されたネットワークである．こうしたがら，LMNtal は十分な表現力・計算能力をも持ち合ネットワークの構造を抽象化・モデル化したデータ構わせている．実際，LMNtal はチューリング完全であ造がグラフである．

り，ラムダ計算などの他の言語体系を LMNtal プロ

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

グラムにエンコードする手法が存在している [11] [12]．

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

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

ラミング言語では扱うことが難しい．例えば，C 言語の他に，モデリング言語としての側面を持ち合わせのようなポインタを扱える言語であれば，ポインタている．実際，LMNtal の実行時処理系である SLIMの接続構造としてグラフを表現することができるが，[21] [19] には，これらの 2 つの側面とそれぞれ対応す依然としてダングリングポインタなどの不正なポイ

る 2 種類の実行モードがある．すなわち，LMNtal を∗

Extending the Expression Power of Types forGraphs as a Data Structure.
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.

プログラミング言語とみなす場合には SLIM は実行
時処理系となり，モデリング言語とみなす場合にはSLIM はモデル検査器となる．特にモデル検査器としての SLIM にはグラフの書換えによって遷移しうる
全状態を出力する機能があるほか，LTL モデル検査などの機能も充実している．

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

う利点がある．ある言語の型をその言語自身で記述仕様のレベルにおいて不正なポインタを排除している

し，その言語自身によって型検査を行うという取り組（すなわち，ポインタ安全である）といえる．一方で，みが統一性の観点から興味深いだけでなく，LMNtal

LMNtal には静的型の概念がないため，書換えの結果の柔軟な表現力をそのまま型の定義に活かすことががプログラマの意図しないものとなることがある．

できるのは大きな強みである．

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

我々はこれまでの研究 [18] [15] において，LMNtal

途中の幾つかのノードを通過するようなエッジを追ShapeType の表現力拡張を模索し，文脈自由を超え加した，図 1 (a) に示すようなデータ構造である．こた広範な型に対応した型検査手法を定式化してきた．

れは LMNtal グラフとして図 1 (b) のように表現でしかし，ラムダ式のグラフによる表現やグリッドグ

きる．

ラフなど，ルートの本数が一定でない型については，

ここで，スキップリストの n2 ノードが 2 つ並んだ型の定義や検査手法が他の型に比べても自明でない．

ところがあったら，右側を n1 に書き換える，という

そこで本論文では，LMNtal ShapeType の定義およ

書換え規則を考え，次の 2 通りを書いたとする．

び検査手法に対して更なる拡張を施すことで，以上の

ようなグラフ型の定義を可能にし，型検査手法の定式

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



化を目指す．

 2 グラフ書換え言語 LMNtal

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



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

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

層や，ルールの発火に関する制約条件を記述するためのガード及びプロセス文脈といった機能が備わっているが，本論文における型付けの対象言語としては，
簡単のためこれらを除外したサブセット言語を扱う．
しかしながら，これらの言語機能をもたない LMNtal
もまたチューリング完全であり，プログラミング言語
としてもモデリング言語としても十分強力である．

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

Ntal を対象とする幾つかの静的型検査手法が提案されている．例えば， [12] の手法ではノード間の局所的な繋がりに着目し，入出力の方向性を解析し，それを−1 から 1 までの実数値（極性）として表現することで型を付ける．
一方，本研究で扱う LMNtal ShapeType [17] は，Structured Gamma [5] およびそのサブセットである
Shape types [4] を基にしてグラフの型を定義・検査する手法である．この手法では，LMNtal のルールを生成規則として，生成文法により型の定義を行う．そ
のため，SLIM のモデル検査機能を用いることによって，LMNtal 自身で LMNtal の型検査を行えるとい2. 1 構文
LMNtal の構文を図 3 に示す． LMNtal プログラ
ムは，グラフ（アトムの多重集合）とルールセット（ルールの多重集合）の組として表現され，これをプロセスと呼ぶ．

LMNtal におけるアトム・リンクは，それぞれグラ
フ理論における節点（ノード）・辺（エッジ）と対応している．p という名前で， m 本のリンク X1 , . . . , Xmをもつアトムを p (X1 , . . . ,Xm ) と書く．これらのリンクをアトムの引数といい，順序がついている．英字の大文字から始まる名前はリンク名，そうでないものはアトム名として解釈される．アトム名と引数の本数（価数）の組をファンクタといい，p/m のように

(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

c

F

n1

a

b
d

n2

(b)

n2

:-

n2

図4

n1

LMNtal グラフの例

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

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

グラフはいずれも次のリンク条件を満たす：

び (b) 誤ったもの



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






プロセス

P ::= G,R



グラフ中に 2 回出現するリンクは両端がアトムと繋グラフ

がっている局所リンクであり，1 回のみ出現するリン（空）

クは一端が無接続である（または，外部と接続してい| p (X1 , . . . ,Xm ) （アトム, m ≥ 0）る）自由リンクである．自由リンクのないグラフは閉| G,Gじているという．2 つのグラフをカンマで結合する際

G ::= 0（分子）

ルールセットは，局所リンク名が衝突しないように α 変換された（空）

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

に順序がついていることを示す．

| R,R

図3

ものとみなす．

（ルール）
（分子）

ルールは，部分グラフから部分グラフへの書換えを表す書換え規則である †1 ．例えば，a(X) :- b(X) は

1 価の a アトムを，1 価の b アトムに書き換えるルー
LMNtal の構文ルである．便宜上，ルールの名前として RuleN ame
をルールの前に付すこともある．また可読性のため

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

に，ルールはカンマで区切るかわりに，ピリオドで終LMNtal においては，アトムの多重集合によって無わる形で書かれることもある．なお，書換えの前後に

向多重グラフを表現する（つまり，多重辺や自己ルー

おいて自由リンクの本数が増減することはあり得なプの出現を許す）．例えば，

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

a(A,F), b(A,C,L1,L2), c(C,D,S,S), d(D,L1,L2)

出現する．

というアトムの多重集合は，図 4 に示すような無向グラフを意味する．図中において矢印は第 1 引数の†1 本論文では簡単のため，コネクタはルールの左辺・右辺のいずれにも出現しないものとする．





(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)



図6



LMNtal グラフ上の遷移関係

X=Y ,P ≡ P [Y /X](E9)

される．ただし，(R2), (R4), (R5) は膜に関する規（P はアトム，X は P の自由リンク）則であるので省略した． 最も本質的で重要な規則は
図5

LMNtal グラフ上の構造合同関係(R6) である．これは，「ルールと，その左辺にパターンマッチするプロセスが存在したら，その左辺を右辺

2. 2 意味論に書き換えてよい」ということを言っている．

LMNtal の意味論は，構造合同と遷移規則からなる．これらについて順に説明する．

また，この定義を自然にルールセットへと拡張することができる．すなわち，∃r ∈ R. G −−→ G′ が成りr

2. 2. 1 構造合同

立つとき「ルールセット R によって，グラフ G が（1まず，グラフ間の構造合同関係 “≡” を，図 5 の規

ステップで）G′ に遷移する」といい，単に G −−→ G′

則を満たす最小の同値関係として定義する．これは，

R

と書く．

グラフ理論におけるグラフ同型にあたる同値関係で

なお，通常の LMNtal においては，アトムとルーあり，構造合同な項は同じグラフを意味する．なお，

ルの多重集合であるプロセスが，遷移関係に基づい

P [Y /X] はグラフ P に出現するリンク X をリンク Yておのずから書き換わっていく．そのため，「ルールに置き換えることを意味する．ただし，(E6), (E10)による作用を受けてグラフが書き換わる」とは考えなは膜に関する規則であるので省略した．

い．しかしながら，書換えに関する静的な性質につい(E1)–(E3), (E5) はプロセス計算にもみられる一般て定義および議論をするにあたっては，書換えの主体的な規則であり，(E4) は局所リンク名の α 変換であたるルールと客体たるグラフとは明確に分離されている．(E7) から (E9) までは特別な 2 価のアトムであたほうが都合が良い．よって，本論文では LMNtal のるコネクタに関する規則である．=(X,Y ) は二つの構文・意味論を簡明な形に等価変換して扱っている．

リンク X, Y を接続するという意味を持ち，中置記法
で X = Y とも書く．(E7) は一つのリンクの両端が繋

2. 3 略記法

がって輪になっているものは空とみなして良いこと，

より簡潔な記述を可能にするため，次の二つの略記(E8) はリンクが対称である（つまり無向である）こと，(E9) は直接接続されている二つのリンクが一つのリンクに縮約できることを表している．

法を認める．

1. アトムの引数にアトムを書いた場合は，そのアト
ムの最終引数に繋がっているものと解釈される．つ2. 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) は6 に示す遷移規則をみたす最小の二項関係として定義

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

2. 引数リストを省略した場合は引数が 0 個であると解釈される．つまり，p は p() の意味である．

3 LMNtal ShapeType
本節では，LMNtal を対象とする静的な型検査手法
である LMNtal ShapeType を紹介する．まず，形式的な定義を先に示しておく．なお，以下で “記号” と定義 3.1. LMNtal ShapeType における型（以下，これを単に “ShapeType” という）は，3 つ組 (S, P, N )defshape skiplist/2 {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).
}は整数型の要素が繋がっているが，以降の本論文中ではグラフの形状を重視するために，こうしたデータ構造に含まれるデータは省略して考える．例えば，上である．ここで，記の型をもつグラフは図 8 に示すような形状をして• S = t/m は，開始記号と呼ばれるファンクタ

いる．

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

以上のように定義された型を，開始記号 S = t/m• N は，非終端記号と呼ばれるファンクタの有限を用いて t/m 型（あるいは m 価の t 型）と呼び，誤集合

解のおそれがないときは価数を省略して単に t 型と⋄呼ぶ．

3. 1 構文ShapeType の構文を図 7 に示す．生成規則は，LMNtal のルールとして well-formed である必要がある．
生成規則の左辺は 1 つ以上の（コネクタでない）非終端アトムのみからなる．また，LMNtal と同様の略記法（2. 3 節）を認める．nonterminal{N } は S 以外の非終端記号の宣言であり，無ければ省略して良い．



なお，図 1 (b) で示したスキップリストの各ノードに言うときは，LMNtal のファンクタのことを指す．

とする．ただし，S ∈ N とする．



3. 2 意味論
型 付 け 関 係 “ : ” を 定 義 す る に あ たって ，補 助
的な型付け関係 “◁” を先に定義する．以下では，⃗ = L1 , . . . , Lm だけを自由リンクに持つグラフをL⃗ ] と書く．また，グラフ G 中で使用されている
G[ L
ファンクタ全体の集合を，Funct(G) と表す．
P⃗ ) −→*
定 義 3.2. 型 (t/m, P, N ) に つ い て ，t( L⃗ ] であるとき，かつそのときに限り，G[ L
⃗]は
G[ L

ShapeType⃗ ) 型によって生成されるといい，G[ L⃗ ] ◁ t( L
⃗)
t( L

::=

と書く．

defshape S { P } [ nonterminal{ N } ]

開始記号

S

::=

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

p/m

生成規則の有限集合

P::=

によって生成されることを表す．

0 | [ RuleN ame @@ ] A :- A | P ,P

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

非終端記号の有限集合N::=⃗ ]◁t( L⃗ )か
定義 3.3. 型 (t/m, P, N ) について，G[ L

0 | p/m | N ,N⃗ ])∩N = ∅ であるとき，かつそのときに
つ Funct(G[ L

アトムの有限集合



A

::=

⋄

これは直観的には，t 型の開始記号から生成規則に0 | p(X1 , . . . ,Xm ) | A,A

図7⃗ ] は t( L⃗ ) 型をもつといい，G[ L⃗ ] : t( L⃗)
限り，G[ L

と書く．

ShapeType の構文⋄

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

例えば，1 節で紹介したスキップリストの場合，次のように型定義できる．

もつことを表す．
また，開始記号および（型付けの対象である）グラList2
List1

n2

n1

n1

図8

n2

n2

n2

n1

n1

n2

nil

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

フの自由リンクの名前と順序の対応関係には意味がを，rinv ≜ U :- T で定める．同様に，LMNtal ルーある．例えば，

ルセット R の反転 Rinv を，Rinv ≜ {rinv | r ∈ R} で

⋄

定める．

defshape t/2 { t(X,Y) :- a(X,Y) }という型があったときに，a(X,Y) ◁ t(X,Y) である

定理 3.1. 両辺ともにコネクタを持たない LMNtal

が，a(Y,X) ◁ t(X,Y) ではない．

ルール r = T :- U について，
r inv

G′ −
→ G ⇔ G −−−−→ G′r

3. 3 型検査

である．

⋄

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

この定理は，ルールの左辺と右辺を入れ替えた反転手法がある．一つは，グラフの型検査である．これ

ルールの適用によって，遷移関係を逆向きに辿ることは，与えられたグラフが，与えられた型に属しているができると主張している．

かを検査するものである．もう一つは，ルールの型検グラフの型検査の目標は，開始記号に生成規則を 0

査である．これは，ルールと型が与えられたときに，回以上適用して検査対象グラフ G に遷移できるかを

ルールの適用によって型の構造が破壊されないことを判定することである．そのため素朴には，定理 3.1 よ検査するものである．

り，逆に検査対象グラフ G から出発し，生成規則のルールの型検査について，もう少し形式的に解説する．まず，型 t に関する LMNtal ルール r の型保存性を定義する．

反転を 0 回以上適用して開始記号に遷移できるか否かを調べればよい．
次に，ルールの型検査の概略は以下の通りである．

⃗ =定義 3.4. ルール r と型 t/m およびリンク列 L

まず，各生成規則 α :- β について，β ≡ β1 ,β2 かつ⃗ ) が，
L1 , . . . , Lm について，全ての G : t( Lr⃗)
G −−→ G′ ⇒ G′ : t( L

β1 が空でないようなグラフ β1 , β2 をとる．ここで，を満たすとき，かつそのときに限り，r は t 型を保存

状態を α,L′ :- β2 ,R へと書き換えるような書換え規⋄則を作成する．以上のようにして得られる全ての書換

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

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

G は，ルール r を（可能なら）適用した後も，t 型を態として状態空間を生成する．こうしてできた状態

持っている」という性質である．このルールの型保存空間において，初期状態から出発して，左辺が開始記性の検査のことを，単にルールの型検査という．

号であるような状態へと到達するような任意の経路するという．

状態 L :- R に対し，L ≡ β1 ,L′ であるならば，この上に，必ず reducible（左辺から右辺へと生成規則を

3. 4 具体的な型検査手法の概略

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

以下では，2 つの検査手法について概略を述べる．

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

より詳細な型検査の手法およびその正当性証明につなお，以上の手順で生成される状態空間はそのま

いては文献 [15] [18] で詳しく述べているため，そちらまでは一般に有限とならない．そのため，実際の実装を参照されたい．

においては左辺が同じ状態は同一とみなして状態空まず，LMNtal ルールおよびその逆実行について，
以下の性質が成り立つ．
定義 3.5. LMNtal ルール r = T :- U の反転 r間を構築する．ただし，このように左辺の構造合同
関係で商を取った状態空間で，初期状態から左辺がinv

開始記号であるような状態へ至る経路上に閉路が出ることで型検査の停止性を担保している．

rule

L

b

X

定義 3.6. 生成規則 p = α :- β について，α がただcXa

一つのアトムからなり，β がコネクタ以外のアトムを一つ以上含むとき，p は文脈自由な生成規則であるという．また，生成規則が全て文脈自由である型を文脈自由な型という．

図9

第一級書換え規則によるルールの表現⋄

グラフの型検査に関しては，型検査が必ず停止し，
かつ false-negative とならないような，文脈自由より現する場合，その閉路に進入した最初の状態におい広い型のクラスが既に発見されている [15] が，ルールて reducible であるかの検査を行い，それ以上は遡らの型検査については，文脈自由より型定義のクラス

ない．

を広げると容易に状態空間のサイズが無限となり，停以上の手法ではルール自体をメタ的に書き換えて型止性を満たさなくなることがわかっている．これは，検査を進めているが，このような計算は LMNtal メ

直観的にはルールの型検査が「必要なグラフを仮定とタインタプリタ [10] における第一級書換え規則のアイして補った上で生成規則の逆適用を行う」ことに基づディアを応用することにより実現できる．

いているためである．

まず，第一級書換え規則とは，LMNtal において

文脈自由な型に関するルールの型検査が停止する

ルールを第一級に，すなわち書換えの対象として扱う

理由を簡単に述べる．文脈自由な型において，生成規ために考案された書換え規則の表現形式である．こ

則左辺は必ず 1 つのアトムのみからなるため，逆適の形式においては，ルールは左辺と右辺を表す 2 つの膜と，それらを束ねるアトムの形で表現される †2 ．

用前にアトムをいくつ補ったとしても，逆適用後は必

例えば，a(L),b(X,L) :- c(X) というルールを第一の数が増加することはない．すなわち，逆実行による級書換え規則として表現すると，状態空間は（左辺の構造合同関係で商をとると）有限rule({a(L),b(X,L)},{c(X)})

ずアトム 1 つとなる．よって，逆適用によってアトムとなる．

となり，これを図示したものが図 9 である．なお，テ型の表現力を向上するために単に文脈自由の前提

キスト表現では { . . . }，図中においては角丸四角形

を崩してしまうと，上記の状態空間の有限性に関するで表される膜とは，本論文における型付け対象言語

議論までも成り立たなくなってしまう．したがって，には含まれない LMNtal の言語要素で，アトムをグ

ルールの型検査をより広範な型へと応用するにあたっ

ループ化する機能を有する機構である．

ては，生成規則左辺がひとまとまりであるという前提

以上のように第一級書換え規則により検査対象ルーを崩さずに型定義を拡張することが重要となる．

ルをグラフとして表現することで，検査対象ルールを
直接書き換えてルールの型検査を行うことができる．

4 インデックス型
4. 1 背景

3. 5 生成規則及び型の文脈自由性

文脈自由な型により，二分木や線形リストといった7 節で後述するように，グラフを対象とする既存手

代数的データ型についてはもちろん，根（自由リン法の多くでは，生成規則の形に次のような制限を加えク）が複数あるスキップリストや差分リスト，あるいはルートが一つもないリング構造のように，代数的†2 本論文における第一級書換え規則の表現は，実装上の都合により [10] で導入されたものと若干異なる．特に，原典では自由リンクはハイパーリンク（超辺）によって表現されていたが，本論文では通常のリンクにより表現している．

データ型では表現ができないグラフの型も表現することができる．
しかし，高さ n の完全二分木や（平衡している）赤黒木，あるいは長さ n のリストといったような数値

 4. 2 インデックス型の形式的な定義


defshape rbtree3/1 {bb3@@ rbtree3(R) :- b(tree2,tree2,R).
bb2@@ rbtree2(R) :- b(tree1,tree1,R).
bb1@@ rbtree1(R) :- b(tree0,tree0,R).
bl@@ rbtree0(R) :- leaf(R).
tb2@@ tree2(R) :- b(tree1,tree1,R).
tb1@@ tree1(R) :- b(tree0,tree0,R).
tr2@@ tree2(R) :- r(rbtree2,rbtree2,R).
tr1@@ tree1(R) :- r(rbtree1,rbtree1,R).
tr0@@ tree0(R) :- r(rbtree0,rbtree0,R).
tl@@ tree0(R) :- leaf(R).
} nonterminal {rbtree3/1, rbtree2/1, rbtree1/1,
rbtree0/1, tree2/1, tree1/1, tree0/1
}



図 10

添字付きの非終端記号の出現を認めるインデックス型を定式化するにあたっては，まずアトムが添字を持つことができるように LMNtal グラフの定義を拡張する必要がある．
定義 4.1. 添字により拡張された LMNtal グラフの構文を以下の BNF で定める．
G ::= 0|

(添字付きアトム, n ≥ 0, m ≥ 0)
|

(分子)

G,G

ここで，

 • x1 , . . . , xn は変数を表すプロセス文脈 $p または

黒高さがちょうど 3 の赤黒木の型定義

制約の付いた型は表現することが難しい．もちろん，
文脈自由でない型を許せばこうした型を表現することはできるが，その場合は型検査における状態空間の有限性が自明でなくなる．
一方で，数値制約が定数であるもの，例えばちょうど黒高さが 3 の赤黒木は図 10 のように文脈自由な型で表すことができる． ここで登場した非終端記
号のうち，rbtreeN は高さ N かつ根が黒である赤黒木，treeN は黒高さ N の赤黒木（根は赤でも黒でもよい）を表し，終端記号の r は赤ノード，b は黒ノード，leaf は葉ノードを表す．なお，黒高さとは根から葉に至るまでの経路上に出現する黒ノードの数である．赤黒木の性質上，黒高さは葉によらず一定であることが要求される．この定義において，bb3 から

bb1，tb2 から tb1，tr2 から tr0 はそれぞれほとん
ど同一の生成規則であり，非終端記号の添字が変わっているにすぎない．
以上の観察結果から，添字付きの非終端記号の出現を認めることにより，赤黒木のような数値制約付きの型の定義を簡略化することができると考えられる．
本論文では，このような添字付きの非終端記号の出現を認める拡張をインデックス型と呼ぶ．なお，こうした添字付きの非終端記号という着想は，形式言語理論におけるインデックス文法（indexed grammar [1]）から得たものである．

(空)

p <x1 , . . . ,xn >(L1 , . . . ,Lm )非負整数定数からなる列であり，これらを（アトムの）添字という†3 ．

• p <x1 , . . . ,xn >(L1 , . . . ,Lm ) を 添 字 付 き ア ト
ムという．

• 添字付きアトムの名前と添字数と価数からなる三つ組を p/n/m のように書き，これを（添字付
きアトムの）ファンクタという．
なお，（従来記法との整合性のため）p <>(L1 , . . . ,Lm )のように添字が 0 個である場合は，添字リストの括
弧を省略して p(L1 , . . . ,Lm ) と書いても良い．同様に，ファンクタ p/0/m は p/m と書いても良い． ⋄次に，LMNtal ルールとそれによる遷移規則についても次のように拡張し，ルールが発火するための条件を記述できるようにする．
定義 4.2. ガード付きの LMNtal ルールの構文を以下で定める．

[RuleName @@] G :- [C|] G.
ここで，C はガードと呼ばれる 0 個以上の等式・不等式制約の列であり，省略されている場合は空列とみなす．なお，今回使用できる演算はプレスバーガ算術の範疇のみとする（加減算・定数倍）．

⋄

定義 4.3. 遷移規則 (R6) を以下の通り拡張する．
G :- C | G′Gθ −−−−−−−→ G′ θiﬀ

θ が C を充足する†3 ここで新たに導入した $p といった記法および「プロセス文脈」という名称は，型付きプロセス文脈 [22] という任意性のあるグラフにマッチするための LMNtalの拡張機能に由来するものであるが，ここでは単に変数を表す記法として使用している．



 4. 3 インデックス型の性質に関する議論
インデックス型の定義において，添字は任意の非負

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

整数値をとる可能性がある．よって，無限通りの値をとることが考えられ，状態空間が爆発する危険がある．そのため，状態空間構築においては非終端記号の添字だけの違いは無視し，同一状態とみなすこととする．
以上の仮定により，見かけ上は添字なしの文脈自由



図 11

な型と同一の状態空間が生成されるため，型検査の停止性が保証される．一方で，前述のちょうど高さがインデックス型を用いた赤黒木の型定義

3 の赤黒木の例のように文脈自由な型の範囲で表現さ

なお，θ はプロセス文脈に対する具体値（非負整数定れた型の場合と比べると，複数の状態が一つの状態に数）の代入であり，C に含まれる全ての制約が θ に縮約されるため，結果が false-negative となる可能性

より充足されるとき，θ は C を充足する代入であるが少し高まる．しかしながら，添字を導入することは⋄型定義の記述の簡潔性からも重要であり，かつ添字を以上の準備のもとで，LMNtal ShapeType の定義

導入せずに任意の高さの赤黒木を表現することは不という．

を拡張し，インデックス型を扱えるようにする．

可能であるから，全体としては型の表現力は向上して

定義 4.4. 以下の三つからなる組 (S, P, N ) を LMNtal

いるといえる．

ShapeType における型と呼ぶ．
• S = t/n/m： 開始記号と呼ばれる，ファンクタ• P ： 生成規則と呼ばれるルールの有限集合

4. 4 具体的な型検査の手順
ここでは，例として以下のルールの型検査を行う．

• N： 非終端記号と呼ばれるファンクタの有限集合

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

ただし，生成規則の左辺・右辺に登場するアトムの

ファンクタのうち N に含まれないもの（終端記号）

これは赤黒木へのノードの挿入のうち最も単純な（木⋄の回転を必要としない）例である．まず，生成規則 tl⃗ = L1 , . . . , Lm は自
以下，(t/n/m, P, N ) は型， L

を逆向きに使って，左辺の leaf を tree<0>に戻す．

は添字をもってはならない．

由リンクの列， ⃗c = c1 , . . . , cn は具体値（非負整数定b(S,tree<0>,R) :- b(S,r(leaf,leaf),R)数）の列であるとする．



定義 4.5.
∗P⃗ ) −−⃗]
t < ⃗c >( L→ G[ L⃗⃗ ) により生であるとき，グラフ G[ L ] は型 t < ⃗c >( L⃗ ] ◁ t < ⃗c >( L⃗ ) と書く．
成されるといい，G[ L⋄

定義 4.6.

⃗ ] : t < ⃗c >( L⃗ ) と書く．
いい，G[ L⋄

以上のように型の定義を拡張した上で，任意の高さの赤黒木の型は図 11 のように記述できる．




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

tree<1>(R) :- b(tree<0>,r(leaf,leaf),R)⃗ ] ◁ t < ⃗c >( L⃗ ) ∧ Funct(G[ L⃗ ]) ∩ N = ∅G[ L⃗ ] は型 t < ⃗c >( L⃗ ) をもつとであるとき，グラフ G[ L








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

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

ruletree<1>(R)tb−−→ b(tree<0>,tree<0>,R)tr−−→ b(tree<0>,r(rbtree<0>,rbtree<0>),R)b

bl−−→ b(tree<0>,r(leaf,rbtree<0>),R)

btree

bl

−−→ b(tree<0>,r(leaf,leaf),R)

tree

tree

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





1
+

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



eq



eq

これもまた reducible である．実際の遷移経路は，先
図 12ほどのものとほとんど同一であるので割愛する．こ拡張された第一級書換え規則による検査対象ルールと制約ストアの表現

れ以外に初期状態から bl を使って戻ることもできる
が，その先は行き詰まり状態であって左辺が開始記号となることはないので，この経路は考えなくて良い．

操作は，一見すると自然なように思われる．しかし，以上により，ルールの型保存性が示された．

こうした不定数を記号的に扱う機能は現在の LMNtal

補うグラフに添字付き非終端記号が含まれる場合の組み込み機能には存在しない．そのため実装にあは，その添字に任意性があるため上記のように単純でたっては，従来の型検査実装に用いていた第一級書はない．例えば，次のルールを考える．

換え規則 [10] を拡張し，数値に関する記号制約を持っb(A,B,R) :- b(B,A,R)

ておくことができるようにした．具体的には，ルールの左辺と右辺を表す膜に加えて，制約ストアを表す



これは単に黒ノードの左右の部分木を入れ替えるルールである．あまり実用的でなくかつ型保存性が直観的には明らかであるが，この型検査にあたっては添字のbtree<n + 1>(R) :- b(tree<n>,tree<n>,R)btree<n + 1>(R) :- b(tree<n>,tree<n>,R)という書換え規則は，実装上は図 12 のように表現される． 図中で下側にある角丸四角形が制約ストアを

表す膜である．その膜の中に入れ子になっている膜がこのルールは生成規則 bb により reducible である．同様に，初期状態から生成規則 tb を使った場合以下を得るが，これも生成規則 tb により reducible である．

tree<n + 1>(R) :- b(tree<n>,tree<n>,R)で接続し，それらの膜の間に，添字が満たすべき制約

例えば，前節の型検査の例において登場した

さ n の tree を補いつつ，生成規則 bb を逆向きに使

分はそれぞれ制約ストア膜内の対応する膜とリンク

条件を表すアトムを橋渡しする形で制約を表現した．

取扱いが難しい．まず自由リンク A と B の先に黒高
い，次を得る．

膜を追加した．左辺・右辺において添字が出現する部

3 つあり，それぞれが非終端記号の添字を表している．
便宜上，図中左から順に x, y, z と呼ぶことにすると，

右側にある eq/2 アトムは y = z という制約を表しており，左側にある eq/2, +/3, 1/1 アトムは x = y + 1

という制約を表している．

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

このように，制約をグラフとして管理することで，

LMNtal が元来持っている構造合同による状態空間圧
4. 5 インデックス型の実装

縮の恩恵に与ることができ，全く同一の制約をもつ全以上のような，具体値が必ずしも定まっていないがく同一のルールについては 2 度以上探索を繰り返さ制約条件が存在するような数を含むグラフに対するずに済むという利点がある．



defshape grid/0 {r1@@ grid :- bgn(L1,L1).
r2@@ bgn(X,Y) :- f(e,L,X), bgn(L,Y).
r3@@ bgn(X,Y) :- mid(Z,Z,X,Y,e).
r4@@ mid(Z,W,f(H,X),Y,R):- f(L1,L2,W), n(H,mid(Z,L1,X,Y),L2,R).
r5a@@ mid(Z,W,X,X,R):- e(R), mid(X,X,Z,W,e).
r5b@@ mid(Z,W,X,X,R):- e(R), end(Z,W).
r6@@ end(f(H,X),Y) :- e(H), end(X,Y).
r7@@ end(f(H,X),X) :- e(H).
} nonterminal {bgn/2, mid/5, end/4, f/3
}



図 13

deque（bgn/2 の第 1 引数と第 2 引数）によって管理する．

3. r3 により非終端記号が mid/5 に変化し，従前の deque はそのまま第 3 引数と第 4 引数に受け継いだ上で，同時に第 1 引数と第 2 引数にも空の deque をつくり，上の端を表す e/1 を 1 つ生成する．

4. r4 により 2 つ目の deque から（左側へとつながる）リンクを 1 つ取り出して，グリッドグラフのノード（n/4）を一つ生成して，新しい左側へのリンクを 1 つ目の deque の末尾へと返却する
手順を 1 回以上（縦の幅の分だけ）繰り返す．

 5. 2 つ目の deque が空になったら，以下のいずれ

グリッドグラフの文脈自由でない型定義

かを非決定的に選択し行う：(a) r5a により 1 つ目の deque を 2 つ目に移し替え，下の端を表す e/1 を生成して一列

5 インデックス型における添字の拡張
5. 1 背景： m × n グリッドグラフ

分の生成を終えるとともに，次の列の上の端を表す e/1 を生成し，手順 4 に戻る．

これまでの拡張により，非終端記号に添字として非(b) r5b により下の端を表す e/1 を生成する

負整数の情報を持たせられるようになり，赤黒木など

とともに，非終端記号が end/2 に変化し，従の数値制約を伴う型を扱えるようになった．しかし，前の 1 つ目の deque を引き継ぐ．手順 6 に

ラムダ式のグラフによる表現やグリッドグラフなどを進む．

型として表現するためには，これまでの拡張だけでは不十分である．
まず，大きさ m × n のグリッドグラフについて見6. r6 を 1 回以上（縦の幅の分だけ）適用すること
により，右の端を表す e/1 の列を生成し，dequeが空になったら r7 により生成を終わる．

ていく．m が一定であり n のみが動く場合は，一列この型において，f/3 からなる deque は単にリン分にあたる m 個のアトムを同時に生成するような規

クを束ねるためのものであるので，f/3 は独立した非則を書けば文脈自由の範囲で生成可能である．m と終端記号というよりは，bgn/2 や mid/5 のような他

n が逆の場合も同様である．一方で，m, n ともに動の非終端記号の付属物であるとみなすことができる．

く場合については，文脈自由な生成規則では素朴に記

このように考えると，前掲の grid/0 型の定義は形の述することが難しい．このような型は，文脈自由では

上では文脈自由な型と捉えることができる．

ない生成規則を許すと図 13 のように記述できる．
この型による生成は以下のように進む．また，生成過程の例を図 14 に示す．

5. 2 リンクを要素とする deque の導入
そこで，インデックス型における添字について，リ

1. ルール r1 により開始記号の grid/0 が自己ルーンクを要素とする deque（差分リスト）を取れるよ

プ（空の deque）を伴う非終端記号 bgn/2 に変う拡張することを考える．以下，4. 2 節において導入化する．

したプロセス文脈のうち，名前が $D から始まるもの

2. r2 を 1 回以上適用することにより終端記号 e/1

をリンクの deque として扱う．特に，$Demp は空のの列からなる左の端が生成される．この際，左のdeque を表す予約語とする．加えて，deque に関する

端につながるリンクは非終端記号 f/3 からなる

以下の制約をガードに記述してよいこととする．

e

grid

bgn

e

f

*

bgn

e

e

f

e

f

e

f

e

f

e

bgn

e

f

e

f

e
e

n

f

e

f

f

e

f

f

e

f

mid

mid

e
e

n

e

e

e

f

n

e

n

f

e

n

f

f

*
e

n

f

e

n

f

mid

e

n

f

e

n

f

e

e

e

e

n

n

n

f

e

n

n

n

f

*

mid

e

n

n

n

f

e

n

n

n

f

e

e

mid

e

e

e

e

n

n

n

f

e

n

n

n

f

e

n

n

n

f

e

n

n

n

f

e

e

e

end

e
e

e

e

e

n

n

n

e

e

n

n

n

f

e

n

n

n

f

e

n

n

n

f

e

e

e

end

*

e

e

e

e

n

n

n

e

e

n

n

n

e

n

n

e

n
e

図 14

e

e

e

e

n

n

n

e

e

e

n

n

n

e

n

e

e

n

n

n

e

n

n

f

e

n

n

n

e

e

e

e

e

e

end

グリッドグラフの生成過程の例

push(X,$D1,$D2)
deque $D1 の末尾に要素としてリンク X を追加

以上の拡張のもとで，グリッドグラフの型は図 15のように記述できる．

した結果得られる deque が $D2 である

shift(X,$D1,$D2)
deque $D1 の先頭要素のリンク X を削除した結果得られる deque が $D2 である

6 ハイパーグラフへの拡張
関数型プログラミング言語に対応する計算モデルであるラムダ計算においては，α 変換可能な名前によ

一般に deque に許される操作は他に pop, unshift

り変数の束縛を表現する方式が一般的に用いられてなどがあり，これらも上記と同様に導入できるが，本いる．一方で，より直截的な表現方法として，ラムダ

論文では割愛する．

式をグラフとして表現し，束縛を辺の接続により表

次に，構文上ルールに課せられる制約条件についてす手法が存在する [12] [16]．特に， [16] の方法では多述べる．まず，$Demp 以外の deque は両辺において対多接続を許す超辺により束縛を表現している．こちょうど 1 回ずつ出現する必要がある．ただしこのれは，1 対 1 接続の通常辺をベースとして補助的な頂際，ガードにおいて push や shift の第 2 引数に出点により分配を行う [12] などの他の手法と比べても，現する deque は右辺，第 3 引数に出現する deque はより直截的なラムダ式の表現であるといえる．この節左辺に出現しているものとみなす．

では， [16] の方法でグラフとして表現されたラムダ

defshape grid/0 {r1@@ grid :- bgn<$Demp>.
r2@@ bgn<$D1> :- push(X,$D1,$D2) | e(X), bgn<$D2>.
r3@@ bgn<$D1> :- mid<$Demp,$D1>(e).
r4@@ mid<$D1,$D2> :- push(X,$D1,$D3),shift(Y,$D2,$D4) | n(X,mid<$D3,$D4>,Y,R).
r5a@@ mid<$D,$Demp>(R) :- e(R), mid<$Demp,$D>(e).
r5b@@ mid<$D,$Demp>(R) :- e(R), end<$D>.
r6@@ end<$D1> :- shift(H,$D1,$D2) | e(H), end<$D2>.
r7@@ end<$D> :- shift(H,$D,$Demp) | e(H).
} nonterminal { grid/0, bgn/1/0, mid/2/1, end/1/0 }




図 15

拡張されたインデックス型を用いたグリッドグラフの型定義

式を型として表現することを目指す．
ハイパーリンクと呼ばれる超辺の出現を許す LMN-

lamtal の拡張を HyperLMNtal [13] という．言語仕様

lam等の詳細は [13] を参照されたい．
以下，アトムの引数にハイパーリンクの出現を許

!F

app

す．ハイパーリンクは，プログラム中では !X のよう
varに，!とそれに続く英大文字から始まる名前により表現されるものとする．例えば，lam(!F,lam(!X,
app(var(!F),app(var(!F),var(!X)))),R)

app
var

var

!X

は図 16 のようなグラフを意味する．
また，このグラフはラムダ式 λf x.f (f x) を表す．

lam/3 は λ 抽象を表し，第 1 引数はこの λ が束縛する変数を表すハイパーリンク，第 2 引数は抽象の本体である．app/3 は関数適用を表し，第 1 引数が関数，
第 2 引数が引数である．また，ここでは後ほどの型定義の都合上，（ラムダ計算における）変数の出現を表すハイパーリンクの直前に var/2 アトムを挟んでいる．

HyperLMNtal においては，型検査を行う上で重要となる，逆実行と反転ルールの関係を表した定理

3.1 が素朴には成り立たない．というより，そもそもHyperLMNtal のルールはハイパーリンクの生成及び破棄を行えるため，対称ではない．そのため，型検査の過程における反転ルール生成の際，ハイパーリンクを生成する生成規則については，生成された（右辺にのみ存在する）ハイパーリンクの要素数が，元のルールの右辺に出現する回数とちょうど一致することを検査する必要がある．例えば，

図 16ハイパーグラフの例

a(!X) :- b(!Y,!Y,!X).
の反転ルールは，b(!Y,!Y,!X) :- num(!Y)=:=2 | a(!X).
とする．ここで， num(!Y)=:=2 はグラフ全体におけるハイパーリンク !Y の出現数がちょうど 2 であることを表す HyperLMNtal のガード制約である．また，生成規則においてはハイパーリンクの破棄を許さないこととする．すなわち，左辺に出現するハイパーリ
ンクは必ず右辺においても出現しなくてはならない．
また，プロセス文脈のうち，名前が $HD から始まるものをハイパーリンクの deque として扱う．特に，$HDemp は空の deque を表す予約語とする．加えて，前節と同様の deque に関する制約をガードに記述してよいこととする．以上の拡張を認めた上で，ハイパーグラフとして表現されたラムダ式の型は図 17 のように表せる．なお，開始記号 term/1/1 の添字は自defshape term/1/1 {t1@@ term<$HD>(R) :- lam_<$HD>(!X,R).
l1@@ lam_<$HD1>(!X,R) :- push(!X,$HD1,$HD2) | lam_<$HD2>(!X,R).
l2@@ lam_<$HD>(!X,R) :- lam(!X,term<$HD>,R).
t2@@ term<$HD>(R) :- app_<$HDemp,$HDemp,$HD>(R).
a1@@ app_<$HD1,$HD2,$HD3>(R) :shift(!X,$HD3,$HD5), push(!X,$HD1,$HD4) | app_<$HD4,$HD2,$HD5>(R).
a2@@ app_<$HD1,$HD2,$HD3>(R) :shift(!X,$HD3,$HD5), push(!X,$HD2,$HD4) | app_<$HD1,$HD4,$HD5>(R).
a3@@ app_<$HD1,$HD2,$HDemp>(R) :- app(term<$HD1>,term<$HD2>,R).
t3@@ term<$HD>(R) :- shift(!X,$HD,$HDemp) | var(!X,R).
t4@@ term<$HD1>(R) :- shift(!X,$HD1,$HD2), push(!X,$HD2,$HD3) | term<$HD3>(R).
} nonterminal { term/1/1, lam_/1/2, app_/3/1 }




図 17

拡張されたインデックス型を用いたラムダ式のグラフ表現の型定義

由変数を表すハイパーリンクからなる deque である．

認めていないため，そのような生成規則は記述するこ

以下，この型による生成の流れを説明する．まず，とができない．そのため，前もって使用する回数分だ

以下のいずれかを非決定的に選択し行う：

けハイパーリンクをコピーしておくことにしている．

1. ル ー ル t1 に よ り，非 終 端 記 号 term/1/1 がこの方式では，生成過程において束縛変数を保存し

lam_/1/2 に変化し，その第 1 引数に新しい束た数と使用した数の辻褄が合わず，行き詰まりとなる

縛変数を表すハイパーリンク !X を生成する．以ケースが多発するため，一見すると効率的でないが，降，ルール l1 を繰り返し適用することにより，型検査を行う際の逆実行の効率だけを考えれば特に0 回以上 !X を deque に push した後，ルール l2問題とはならない．

により λ 抽象を表す lam/3 アトムを生成した上で抽象の本体に deque を引き渡す．

7 関連研究2. ル ー ル t2 に よ り，非 終 端 記 号 term/1/1 が

本節では，まずグラフを対象とする既存の型検査

app_/3/1 に変化する．以降，ルール a1, a2 に手法を紹介する．Graph types [7] は正規表現を基により deque の中身を非決定的に 2 つの deque にしたグラフの型検査手法である．また，Structured

分配し，分配が終わったらルール a3 により関数

Gamma [5] は文脈自由文法を基にした，生成規則に適用を表す app/3 アトムを生成した上で 2 つのよって型を定義する型検査手法である．Shape Typesdeque をそれぞれ関数側と引数側へと引き渡す．

[4] はこの Structured Gamma のサブセットであり，

3. ルール t3 により，deque がシングルトンであ型検査の完全性が満たされるように型定義の範囲

ることを確認した上で，変数を表す var/2 アトを制限したものである．本論文で扱っている LMN-

ムを生成する．

tal ShapeType は上記 Shape Types 及び Structured

4. ルール t4 により，deque から一つ要素を shift

Gamma の技法をベースとして，LMNtal の書換え規してそのまま push する．すなわち，単に deque則の型検査を行う手法である．以上の手法は，いずれを rotate する．

も「グラフの書換え操作を 1 ステップ進めても，構造

特に，ルール l1 の繰り返し適用によって先に束縛変が破壊されない」ことの検査・保証を目的としたもの

数の使用回数を決め打ってしまうのが重要なポイントである．しかし，その対象となる型の表現力には文脈である．束縛された変数を各々一つだけ deque に保

自由性による制限（定義 3.6 参照）があり，完全二分

存して生成を進める場合，最終的に使用しなかった変木や赤黒木などの数値制約の入った型を表現すること数を破棄する必要があるが，ハイパーリンクの破棄ははできていなかった．

本論文においては赤黒木のような数値制約を含む

ゴリズムの再定式化が挙げられる．特に，ラムダ式の型の表現にインデックス型を用いたが，関数型言語

グラフ表現において，β 簡約を表す書換え規則 [16] のをベースとした型体系では，型に対して述語による型検査を行うためには，検査対象ルールがガードをも

数値制約を掛ける手法として篩型（reﬁnement types

つことを許す必要がある．本論文ではインデックス型[14]）が知られている．また，この篩型を述語抽象化

を通して，ガードを持つ生成規則に関して議論してきによって自動的に推論する手法として Liquid Types

たが，検査対象ルール，すなわち型付けの対象言語が[9] が存在する．他のアプローチとして，赤黒木の型

ガードを持つ場合については依然定式化も議論も十を高階型などの機能を用いて表現する研究 [6] もある．
また，ハイパーグラフにおける超辺 †4 を文脈自由分でない．

文法により書き換えることでグラフの言語を定める(2022C-421, 2022C-435, 2022Q-006) の補助を得てHyperedge Replacement Grammar (HRG) [2] の分実施した．

謝辞 本研究の一部は，早稲田大学特定課題研究費野においては，文脈自由より広い文法を表現できるよ
うにする Contextual HRG という拡張が提案されて

参 考 文 献いる [3]．この拡張は，生成規則の左辺に，書換え対[ 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 ] Drewes, F., Kreowski, H.-J., and Habel, A.: Hyperedge Replacement Graph Grammars, World Scientiﬁc, 1997, pp. 95–162.
[ 3 ] Drewes, F., Hoﬀmann, B., and Minas, M.:
Contextual Hyperedge Replacement, Proc. AGTIVE’11, Springer, 2011, pp. 182–197.
[ 4 ] Fradet, P. and Métayer, D. L.: Shape types,
Proc. POPL’97, ACM, 1997, pp. 27–39.
[ 5 ] Fradet, P. and Métayer, D. L.:
Structured Gamma, Science of Computer Programming,Vol. 31, No. 2(1998), pp. 263–289.
[ 6 ] KAHRS, S.: Red-black trees with types, Journalof Functional Programming, Vol. 11, No. 4(2001),
pp. 425–432.
[ 7 ] Klarlund, N. and Schwartzbach, M. I.: Graph
Types, Proc. POPL’93, 1993, pp. 196–205.
[ 8 ] Pugh, W.: Skip lists: A probabilistic alternative to balanced trees, Commun. ACM, Vol. 33,
No. 6(1990), pp. 668–676.
[ 9 ] Rondon, P. M., Kawaguci, M., and Jhala,R.: Liquid Types, Proc. PLDI 2008, ACM, 2008,
pp. 159–169.
[10] Tsunekawa, Y., Tomioka, T., and Ueda, K.:
Implementation of LMNtal Model Checkers: A
Metaprogramming Approach, Journal of Object
Technology, Vol. 17, No. 1(2018).
[11] Ueda, K.: Encoding the Pure Lambda Calculus
into Hierarchical Graph Rewriting, Proc. RTA2008,
Voronkov, A.(ed.), LNCS, Vol. 5117, Springer, 2008,
pp. 392–408.
[12] Ueda, K.: Towards a Substrate Frameworkof Computation, Concurrent Objects and Beyond,Agha, G. et al.(eds.), LNCS, Vol. 8665, Springer,
2014, pp. 341–366.
[13] Ueda, K. and Ogawa, S.: HyperLMNtal: An Ex-

象となる超辺に加えて，その超辺に接続されていない頂点を記述できるようにすることで，任意のラベ
ルへとジャンプする goto 文を許したコントロールフ
ローグラフや，任意のハイパーグラフを生成する文法などを記述可能にしている．一方で，Contextual

HRG では生成規則左辺に出現する頂点に（頂点の名前以外の）制約をかけることが困難であるため，本論文において例題として示したラムダ式のように，階層的な構造をなすハイパーグラフを生成する文法は記述が難しいと考えられる．

8 まとめと今後の課題
本論文では，形式文法に基づいてグラフの型定義・検査を行う枠組みである LMNtal ShapeType に対して，添字として非負整数や，辺・超辺を要素とするリストを伴う非終端記号の出現を許す拡張を施すこと
で，赤黒木を始めとする数値制約付きのデータ構造
や，グリッドグラフ・ラムダ式のグラフ表現といった複雑なグラフ型を表現可能にした．
今後の課題としては，辺や超辺を要素とするリスト
が添字に出現する型に対応したルールの型検査アル†4 HRG では名前を持つ超辺が書換えの対象であり，HyperLMNtal では名前を持つアトム（頂点）が書換えの対象である．このことから，HRG における超辺は HyperLMNtal におけるアトムと，HRG における頂点は HyperLMNtal におけるハイパーリンクと，それぞれ対応づけられる．

tension of a Hierarchical Graph Rewriting Model,
KI - Künstliche Intelligenz, Vol. 26, No. 1(2012),
pp. 27–36.
[14] Vazou, N., Seidel, E., Jhala, R., Vytiniotis,
D., and Peyton Jones, S.: Reﬁnement Types For
Haskell, ACM SIGPLAN Notices, Vol. 49(2014).
[15] Yamamoto, N. and Ueda, K.: Engineering
Grammar-based Type Checking for Graph Rewriting Languages, Proc. Twelfth International Workshop on Graph Computation Models (GCM 2021),
June 2021, pp. 93–114.
[16] Yasen, A. and Ueda, K.: Revisiting Graph Types
in HyperLMNtal: A Modeling Language for Hypergraph Rewriting, IEEE Access, Vol. 9(2021),
pp. 133449–133460.
[17] 吉元佑介, 上田和紀: グラフ書換え系における静的
グラフ型検査, 日本ソフトウェア科学会第 32 回大会(2015 年度) 講演論文集, 2015.
[18] 山本直輝, 上田和紀: グラフ書換え言語における数
値制約を伴う型の静的型検査, 日本ソフトウェア科学会
第 37 回大会 (2020 年度) 講演論文集, 2020.
[19] 後町将人, 堀泰祐, 上田和紀: LMNtal 実行時処理系の並列モデル検査器への発展, コンピュータ ソフトウェ
ア, Vol. 28, No. 4(2011), pp. 4 137–4 157.
[20] 上田和紀, 加藤紀夫: 言語モデル LMNtal, コンピュー
タ ソフトウェア, Vol. 21, No. 2(2004), pp. 126–142.
[21] 石川力, 堀泰祐, 村山敬, 岡部亮, 上田和紀: 軽量なLMNtal 実行時処理系 SLIM の設計と実装, 情報処理学会第 70 回全国大会講演論文集, (2008), pp. 153–154.
[22] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal, コンピュータ ソフトウェア, Vol. 25,
No. 1(2008), pp. 124–150.