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

パターン定義によるマッチングを導入したグラフ書換
え言語とその実装
奈良 耕太

上田 和紀

グラフ書換え系とは，与えられた書換え規則に従ってグラフを簡約することで計算が進行する系である．書換え規則の簡約基には通常，グラフの部分グラフを具体的に指定する．したがって，たとえば所定の性質を満たす任意のグラフを簡約基とするような書換え規則を記述することはできない．本研究では，グラフの集合を表現するための再帰的な生成文法を設計し，具体的なグラフでなくグラフの持つべきパターンによって簡約基を指定することのできるグラ
フ書換え言語を実装した．また実装にあたって，パターンマッチングのメモ化が多くの例題で計算量を改善することを確認した．このパターン記述言語の表現能力を確認する例題として，第一級の継続を持ったプログラミング言語の意味論をグラフ書換え系として記述し，実行することに成功した．

モデル検査器 SLIM の対象とするグラフ書換え言

1 はじめに語である LMNtal [3] は，“プロセス文脈” と呼ばれるグラフ書換え系とはグラフと簡約規則の集まりで機能によって，不特定多数のグラフを簡約基とする簡あって，グラフを規則に従って別のグラフに書換え

約規則を一部認めている．プロセス文脈は簡約規則てゆくことによって計算が進行するような系である．

に，そのプロセス文脈の持つべき性質に関する制約をグラフ書換え系はモデル記述の手段として広範なシ伴って出現し，その制約を満たす任意の部分グラフを

ステムを記述できる表現力を持ち，実際に SLIM [1],代表する．制約は処理系にあらかじめ組み込まれた

GROOVE [2] などグラフ書換え系を対象にしたモデいくつかの条件 (型) から選択して記述することがで

ル検査器も開発されている．

きる．

グラフ書換え系において簡約規則は通常，書換えのプロセス文脈はグラフ書換え系の表現力を部分的対象となる具体的なグラフ (の部分) と書換え後のグに改善するが，条件を組み込みの型から選択すること

ラフとのペアによって表現される．しかしこの表現方しかできないという点で，データの性質に対する記述法では，たとえば “ノード a に任意のリスト (と解釈力が高いとは言えない．本研究の目標は，簡約基の持できるグラフ) が接続されているとき，これを空リス

つべき性質を，組込みのものだけでなくプログラマがトに書き換える” などの書換えを，考えられるあらゆ

定義したものからも選択できるようなグラフ書換え

るリストを具体的に列挙することなしに記述するこ

言語の設計と，その実用的な実装である．これに向けとができない．

て，グラフの集合を記述するための再帰的な生成文法を設計し，記述されたグラフの集合をプロセス文脈の

A Graph Rewriting System and Its Implementation
with Matching via Pattern Definitions
Kota Nara, 早稲田大学理工学研究科 情報理工情報通信専
攻, Dept. of Computer Science and Communications
Engineering, Waseda University.
Kazunori Ueda, 早 稲 田 大 学 理 工 学 術 院 情 報 理 工 学科, Dept. of Computer Science and Engineering,
Waseda University.

型として選ぶことができるよう拡張した LMNtal のプロトタイプ処理系を実装した．また，この処理系の実行効率を改善するための手法として，パターンマッ
チングのメモ化について検討した．
本論文では，設計した生成文法およびグラフ書換え
系について紹介する．また生成文法の表現力を示す例





X

::=

⟨LinkName⟩p::=⟨AtomName⟩

P

::=

ϵ

a(X), b(X,Y), c(Y)

この例ではリンクを表す名前に X, Y を用いたが，別の名前を用いて a(A), b(A,B), c(B) としても同じプロセスを表すことにする．一方，アトムの引数の順(空)|p(X1 , . . . , Xn )(n ≥ 0)

|

P, P

(分子)

|

P :- P(ルール)

序を入れ替えたプロセス a(A), b(B,A), c(B) は元

(アトム)



のプロセスから区別する．
あるプロセスの中で２回出現するリンク名をそのプロセスの局所リンクといい，１回だけ出現するリンク名をそのプロセスの自由リンクという．たと
図1

LMNtal の構文として，一般的なプログラミング言語の苦手とする差えば a(X), b(X, Y), c(Y) の部分プロセス a(X),b(X,Y) において X は局所リンク，Y は自由リンクである．

分リスト [9] のようなデータ型，あるいは簡約規則のLMNtal で唯一予約されているアトム名は ’=’ で適用に関する条件などがこの文法で記述できることある．このアトムはリンクの相互接続を表すために用を紹介する．またメモ化を行うパターンマッチングのいられ，次の性質を持つ：

アルゴリズムと，これによって期待される性能の向上について触れる．

2 構文と意味論
2. 1 FlatLMNtal
提 案 言 語 は 既 存 の 言 語 LMNtal (の サ ブ セット

FlatLMNtal: 以下たんに LMNtal と書く) の後方互換な拡張として設計したため，まず LMNtal の構
文および意味論について解説する．なお本節の内容は
文献 [3] をもとに再構成したものである．

LMNtal の対象とする，グラフおよび書換えルールの多重集合をプロセスという．プロセスの構文を

X=X

≡

ϵ

X1 = X2 , P≡

P [X1 ← X2 ](X1 はアトム P の自由リンク)
たとえばプロセス a(X,Y), X = Y や a(Y,Y), X =X はどちらも a(Y,Y) と同じプロセスを表す．
リンク条件によって，局所リンクを持つプロセス P1と，その局所リンクと同じリンク名を１つ以上持つプロセス P2 に対してプロセス P1 , P2 や P2 , P1 は定義されない．便宜のために，本論文ではこのようなプロセスの組に対してもプロセス P1 , P2 および P2 , P1
を次のように定義する：P1 に出現する局所リンクをP2 に出現しない適当なリンク名で置き換えて得られ図 1 に示す．LinkName は大文字アルファベットかるプロセス P1′ を一つ決めて，P1 , P2 = P1′ , P2 またら始まる識別子，AtomName はそれ以外の英数字でP2 , P1 = P2 , P1′ ．

始まる識別子あるいは ‘’’ で囲まれた任意の文字列である．分子を構成する ‘,’ はルールを構成する ‘:-’よりも強い結合力を持つ．可読性のために，アトム’=’(X1 , X2 ) を X1 =X2 と略記する．
直感的には，アトムはグラフ理論で扱うグラフの

def

def

ルールは，‘:-’ の左側 (LHS: Left-Hand Side) に書かれたプロセスを右側 (RHS: Right-Hand Side)に書かれたプロセスに書き換える規則である．たとえばプロセス p(A,A), (p(X,Y) :- q(X,Y)) は次のよ
うに書き換わる．

ノードに相当する概念であり，リンクは同様にエッジに相当する概念である．同じリンク名の対によってエッジの接続を表す．したがって，あるプロセスに同じリンク名はたかだか２回しか出現しない (リンク条件)．たとえばアトム a と b ，b と c をそれぞれリンクで接続したグラフを次のように表現できる：

p(A,A). p(X,Y) :- q(X,Y)→

q(A,A).

p(X,Y) :- q(X,Y)

LHS または RHS に自由リンクが出現するとき，他方にも同じ自由リンクが出現しなければならない．一方，局所リンクは書換えの過程で消費することも，生成することもできる．
上の構文に加え，可読性のために次の別記法を用いることがある．

1. ‘:-’ よりも結合力の弱い ‘,’ として ‘.’ を用いる

2. 引数のないアトム a() をたんに a と表記する

図3

3. アトム a(X,Y) の最終引数を外に出して Y =a(X) と表記する

typedef dlist(T,H) {4. ’=’ アトムを含むプロセス a(X,Y), Y = b を

H = T.

たんに a(X,b) と表記する
たとえば，次の４つの表記はすべて等価である．

差分リストの例

H = c(A,B) :- atom(A), dlist(T,B).
}• a(X,Y), b(X), c(Z,Y)

この宣言は，直感的には次の主張を表す：２つの• a(X,Y), X = b, Y = c(Z)

リンク H, T (だけ) を自由リンクとするプロセス• a(b,c(Z))

P が型 dlist を持つとは，P が H = T であるか，• c(Z) = a(b)atom(A) の元 P1 と dlist(T,B) の元 P2 があって
H = c(A,B), P1 , P2 ということである．ただし atom

2. 2 グラフ集合のテキスト表現

は単一のアトムを表す組込みの型である．たとえば次以下では便宜のために，X1 , . . . , Xn のような自由のプロセスは dlist(T,H) の元である．

リンク名の列を単一の飾り文字で X などと表現することがある．
グラフ集合 (型) を宣言するための構文 Decl を図 2

H = c(1,c(2,c(3,c(4,c(5,T)))))
グラフ集合 t(X ) の定義に含まれる TypeRule は次の制約を満たさなければならない．

のように定義する．ただし TypeName は AtomName

1. LHS あるいは RHS に現れる自由リンクは，同として認められるような型名である．可読性のため，

じ自由リンクが他方あるいは X のいずれかに出TypeRule の RHS が空のとき ‘:-’ は省略することが現するある．また TypeRule が１つしかない Decl の波括
弧も省略することがある．

2. LHS のあらゆる空でない部分プロセスは少なくとも一つの自由リンクを持たなければならない

簡単な型宣言の例には次のようなものがある．

この制約の帰結として，プロセス文脈型は次の性質

typedef abc(X) { a(X). b(X). c(X). }を満たす：プロセス P がある型を持つならば，P のこの宣言は，直感的には次の主張を表す：グラフ集合

含むあらゆるアトムに P の少なくとも１つの自由リ

abc(X) は，３つのプロセス a(X); b(X); c(X) から

ンクから到達できる．たとえばプロセス a(X), b はなる３要素の集合である．あるいは次のようにも表現

自由リンク X からアトム b に到達できないから，こできる：リンク X (だけ) を自由リンクとするプロセのプロセスはいかなる型も持ってはならない．一方，

ス P が型 abc を持つとは，P が a(X); b(X); c(X)プロセス a(X), b(Y) は連結ではないが，部分プロのいずれかであるということを表す．

セス a(X); b(Y) および a(X), b(Y) はいずれも自由

また，要素を列挙することなしにグラフの無限集合

リンクを持つ．したがってこのプロセスは，どのアトを表現するために，‘:-’ を用いて集合を (相互) 再帰

ムにも X, Y の少なくとも一方から到達できる．組込的に定義することができる．これを用いて差分リスト

みのプロセス文脈型もすべてこの性質を満たす．このを表現すると，たとえば次のようになる．差分リスト

性質によって，ある自由リンクの列 X を引数とするとは図 3 のように，空リストで終端されていない線

ようなプロセス文脈の表すグラフはたかだか１つし形リストである．

か存在しない．




t

::=

⟨TypeName⟩

Decl

::=

typedef t(X ) {TypeRule1 . . . TypeRulen }TypeRule::=

P :- t1 (X1 ), . . . , tn (Xn ).

(n ≥ 0)(n ≥ 0)
図2型宣言の構文

形式的には，TypeRule とグラフ集合との対応付け

S を次のように定義できる．

7→Sと上のルールとを並べておくと，次のように簡約されていく (ルールは省略した)．

P :- t1 (X1 ), . . . , tn (Xn )--> dlist?(X,X), dlist?(a,a), yes{P, P1 , . . . , Pn | Pk ∈ tk (Xk )}--> yes, dlist?(a,a), yes

この S のもとで，宣言

typedef t(X ){TypeRule1 . . . TypeRulen }は，集合 t(X ) を

S(TypeRule1 ) ∪ · · · ∪ S(TypeRulen )と定義するものと決める．S と t(X ) の定義が相互再帰的であるが，それぞれ集合の包含関係にかんして最小の解を取るものとする．

a(H), a(T) は dlist(T,H) の元ではないから，これ以上は簡約されない．
形式的には，上の拡張されたルールは通常のルール
を無限個並べた次のプロセス

dlist?(T,T) :- yes.
dlist?(c(a,T),T) :- yes.
dlist?(c(b,T),T) :- yes.
...

2. 3 グラフ集合を用いたルール
定義されたグラフ集合を用いて簡約規則を記述する
ために，ルールの構文を図 4 のように拡張する．この構文では，アトム p(X ) と同様にプロセス文脈 $p[X ]をルール中に記述できる．また，プロセス文脈の満たすべき性質を記述するガードがルールの ‘:-’ の直後に存在する．ガードが空の場合，‘|’ は省略することがある．
拡張されたルールの例には次のようなものがある．

dlist?(H,T), $x[T,H] :- dlist($x) | yes.
あるいはアトムの略記法をプロセス文脈に援用して，次のように書いてもよい．

dlist?(c(a,c(a,T)),T) :- yes.
...と等価であると考えられる．同様に，任意の拡張されたルールから，それと等価な拡張されたルールを含まないプロセスを次のように構成することができる：

1. ガ ー ド が 空 の ル ー ル P1 :- | P2 は ル ー ル
P1 :- P2 と等価
2. ルール T1 :- t($p), . . . | T2 はルールの集合 T ⟨$p[X ] ← P ⟩ :- . . .
1
P ∈ t(X ) | T2 ⟨$p[Y] ← P, X =Y⟩の元をすべて , で結合したものと等価．ただし，

P1 ⟨P2 ← P3 ⟩ は，P1 の部分プロセス P2 に P3

dlist?($x[T], T) :- dlist($x) | yes.

を，必要に応じて局所リンクを改名して代入しこのルールは直感的には次のような書換えを表す：たもの．また X =Y は X の k 番目のリンクと Ydlist? アトムに２本のリンクで接続された部分プロの k 番目のリンク (k = 1, 2, . . . ) をそれぞれ’=’

セスが型 dlist を持つならば，それら全体を単一のアトムで接続したプロセス．

yes アトムに書き換える．
たとえば次のプロセス

dlist?(X,X), dlist?(a,a),dlist?(c(1,c(2,Y)),Y)

例として，次の型定義を考える．

typedef ab(X) { a(X). b(X). }typedef cd(X) { c(X). c(X). }この型定義のもとで，ルール




P

T

::=

ϵ

(空)

|

p(X )

(アトム)

|

P, P

|

T :- t1 ($p1 ), . . . , tn ($pn ) | T

::=

ϵ

|

p(X )

|

T, T

|

$p[X ]|

T :- t1 ($p1 ), . . . , tn ($pn ) | T(分子)(n ≥ 0)(拡張されたルール)(プロセス文脈)(n ≥ 0)
図4

ルールの構文の拡張




x

::=

⟨Variable⟩v::=⟨IntegerConstant⟩ | λx.e | succe::=ee|x|v

typedef v(L) {:- int(L).
L = X -> E :- x(X), m(E).
L = succ.


図5

typedef x(L) :- atom(L).

ラムダ式の構文}
typedef e(L) {L = E1 @ E2 :- e(E1), e(E2).

foo($x,$y) :- ab($x), cd($y) | .

:- x(L).

は２つの拡張されたルールからなるプロセス:- v(L).

foo(a,$y) :- cd($y) | .

}foo(b,$y) :- cd($y) | .

ただし int は名前が整数であるようなアトムを表すと等価であり，またこれはプロセス文脈を含まない４組込みの型である．たとえば次のプロセスは e(X) のつのルールからなるプロセス

元である：

foo(a,c) :- . foo(a,d) :- .

X = (x -> (succ @ x)) @ 1

foo(b,c) :- . foo(b,d) :- .と等価である．

3. 2 評価文脈の表現
プロセス文脈の型は，評価文脈の条件を記述するた

3 応用例
3. 1 データの性質の表現めに用いることもできる．
評価文脈とは，プログラミング言語の操作的意味

プロセス文脈の型は一般的な言語のデータ型と同論において，評価順序を表現するために Felleisen と様に，データの性質を記述するために用いることがで

Hieb によって提案された概念である [4] ．直感的にきる．

は，ある簡約において式全体から簡約基を取り除いた

例として，図 5 のラムダ式 e を考える．プロセス

部分，すなわち式のうちその簡約によって変化しないのうち特に上のラムダ式として解釈できる木だけを部分が評価文脈である．評価文脈の取ることのできる集めた集合を，次のように表現することができる．

形を制限することによって，簡約規則の適用順序を間うになる．
typedef c(Hole,X) {X = Hole.
X = C @ E :- c(Hole,C), e(E).
X = V @ C :- v(V),c(Hole,C).
}
Hole のような特殊な終端記号を用意することなく，
リンクによって自然に構文木の欠けを表現できている点は注目に値する．たとえば構文木 (x -> x) @(succ @ 1) において評価文脈は図 6 の四角で囲ま
図6

構文木で見た評価文脈

接的に表現することができる．
たとえば，上のラムダ式を left-to-right に (関数と引数をこの順で評価してから関数適用をする，という順に) 評価するための評価文脈を次のように定義できる．

れた部分に相当するが，これはたんに２つの自由リンクを持つ部分プロセスとして表現できる．この “評価文脈型” を用いて，簡約順序に制約のある簡約規則を
次のように記述することができる．
eval($c[(X -> E) @ $v]):- c($c), v($v)| eval($c[subst(E,X,$v)]).

C ::= [ ] | C e | v C[ ] は Hole と呼ばれる特別な終端記号である．この文法の生成する項には，次のようなものがある．

[][ ] (succ 1)eval($c[succ @ $v]):- c($c), int($v)| eval($c[$v + 1]).
代入を表すアトム subst のためのルール群は論文の本旨から外れるのでここでは省略する．

succ [ ]一方で，次のような項を生成しない．

3. 3 第一級の文脈((λx.x) succ) [ ]プロセス文脈それ自体も書換えの対象とすること

Hole を “次に評価する場所の候補” と考えると，こができる．これを用いて，たとえば上のラムダ計算のれは “関数の評価が終わるまで引数を評価しない” こ

モデルに第一級の継続を導入することができる．

との表現になっている．またこの評価文脈はラムダ抽

ある式の継続とは，その式の計算結果を使ってこれ象の内部に Hole を作らないから，冠頭標準形になっからするべき計算の全体である．Scheme などのプロていないラムダ式だけを評価するすることもわかる．

グラミング言語には，継続を第一級オブジェクトとし

この評価文脈 C を用いて，評価順序を反映した操作て扱うための組込み関数 call/cc がある．この関数的意味論を次のように記述することができる．

は，別の関数を引数に取り，受け取った関数をその時

C[(λx.e) v] → C[e⟨x ← v⟩]
C[succ v] → C[v ′ ](⌈v ′ ⌉ = ⌈v⌉ + 1)

ただし ⌈v⌉ は定数項 v の表す値を，C[e] は評価文脈

C の Hole を式 e で置換して得られる式をそれぞれ表す．⟨x ← v⟩ は x への v の Capture-Avoiding な
代入である．
プロセス文脈の型で評価文脈を記述すると，次のよ

点での継続を引数として呼び出す．呼び出された関数の受け取った継続は，１引数関数のように扱うことができる．継続 c が引数 v で呼び出されると，継続呼出し自体の継続を c で置き換え v を返す．
評価文脈 C の定義を思い出すと，評価文脈がまさに簡約基の継続そのものになっていることがわかる．
したがって，評価文脈に相当する部分プロセスを第一級に扱うことができれば，継続の捕捉や呼出しを行う簡約規則を記述することができる．たとえば我々のラムダ計算のモデルに第一級の継続を導入するには，

3. 1 節の v 型の定義に call cc と継続を加え，２つの簡約規則を追加すればよい．

typedef v(L) {:- int(L).
L = X -> E :- x(X), e(E).
L = succ.
L = call_cc.
L = cc(Hole,X) :- c(Hole,X).
}eval($c[call_cc @ $v]):- c($c), v($v)



fun typeCheck(Type, Links):
G ← Links から到達できるアトムを集めたグラフ;
foreach T ypeRule in Type {foreach g in
T ypeRule.LHS と同型な G の部分グラフ {foreach t(X ) in T ypeRule.RHS {X ′ ← g で X に対応するリンク列;
unless (typeCheck(t, X ′ ))next g;}return true;}}
return false;| eval($c[$v @ cc(H,$c[H])]).


図7

素朴な型検査の手順

eval($c1[cc(H,$c2[H]) @ $v]):- c($c1), c($c2), v($v)| eval = $c2[$v].

4 型検査のメモ化
4. 1 型検査へのメモ化の導入

次のプロセス

プロセス文脈型の型検査にかかる計算量は，型の定

eval(succ

義によっては指数的に増大しうる．極端な例にはたと@ (call_cc@ (cc -> succ @ (cc @ 1)))).
と上のルール，型定義とを並べておくと，次のようにえば次のようなものがある．

typedef tree0(X) {簡約されていく (ルールは省略した)．

X = a.

--> eval(succ

X = n(L,R) :- tree0(L), tree0(R).

@ ((cc -> succ @ (cc @ 1))@ cc(succ @ Hole,Hole)))}typedef tree1(X) {--> eval(succ

X = b.

@ (succ

X = n(L,R) :- tree1(L), tree0(R).

@ (cc(succ @ Hole,Hole)@ 1)))--> eval(succ @ 1).

X = n(L,R) :- tree0(L), tree1(R).
}typedef tree2(X) {--> eval(2).

X = n(L,R) :- tree2(L), tree0(R).
X = n(L,R) :- tree1(L), tree1(R).

3. 4 その他の例
ラムダ計算の評価戦略や第一級の継続のほかに，一X = n(L,R) :- tree0(L), tree2(R).
}

般的な言語の苦手とする循環リストなどのデータ型

型 tree0 は葉がすべて a，内部ノードがすべて n でや，括弧の対応の検査などの複雑なパターンマッチン

あるような二分木である．型 tree1 は tree0 に似グをプロセス文脈型として表現し，実行することに成ているが，葉のうちちょうど１つだけが b で，かつ功した．

残りがすべて a あるような二分木である．同様に型

tree2 は葉のうちちょうど２つだけが b であるような二分木である．図 7 のような素朴な手順で tree2

上の型を定義することはない．また２価以上の型の多くで，自由リンクのいくつかを固定した再帰的定

fun typeCheck(Type, Links):
if ((Type, Links) に対してメモ v が残っている)
return v;
G ← Links から到達できるアトムを集めたグラフ;
foreach T ypeRule in Type {foreach g in
T ypeRule.LHS と同型な G の部分グラフ {foreach t(X ) in T ypeRule.RHS {X ′ ← g で X に対応するリンク列;
unless (typeCheck(t, X ′ ))next g;}(Type, Links) に対してメモ true を残す;
return true;}}(Type, Links) に対してメモ false を残す;
return false;

義が行われる．たとえば 4. 2 節の c 型の定義を見ると，再帰的定義の中で c の自由リンクの一つは常にHole である．このとき，実際に検査の対象となる自由リンクの組み合わせはリンク数に線形である．

4. 2 メモの保持と更新
型検査のメモ化によって最悪の計算量を多項式で抑えられることがわかったが，型検査にはそれでもなお無視できないコストがかかる．また簡約の順序を指定する目的で書かれる型制約は，型検査をしても失敗することが少なくないため，一度の簡約のために何度も型検査が行われることも多い．そこで，型検査の過程で作られたメモを捨てずに保持し続けることで，
図8

メモ化型検査の手順

型検査の回数自体を削減することを考える．プロセス
文脈の型定義は再帰的に行われるため，１回の型検査

型の検査をすると，ノード数に対して計算時間が指数の中でその部分構造に対してもかなりの量の情報を的に増大する．

残すことができる．これを適切に管理することで，そ計算時間が増大する原因の一つに，同じ自由リンク

れ以降の型検査の回数を削減することが期待できる．

の列に対して同じ型を何度も検査してしまうというたとえば次の差分リスト (dlist 型のグラフ) を考問題がある．このような計算量の増大を防ぐために，える．

型検査のメモ化が有効である．たとえば上の例では，

H = c(1,c(2,c(3,T)))

型は３種類しか定義されていないのだから，リンク

一度この構造に対して型検査を行うと，この差分リスと型の組み合わせは高々リンク数に対して線形 (したトの要素を先頭から順々に除いて得られる差分リスト

がってアトム数に対して線形) である．したがって，に対してもメモが残る．

同じリンクと型の組み合わせを何度も型検査するとH = c(1,c(2,c(3,T)))∈dlist(T,H)

いうことがなければ，計算時間が指数的に増大するこH = c(2,c(3,T))∈

dlist(T,H)とはない．メモ化を行う型検査のアルゴリズムは図 8

H = c(3,T)∈

dlist(T,H)のように書ける．型検査に失敗しても，失敗したとい

H = T

∈

dlist(T,H)

う事実をメモすることに注意する．
メモ化によって，一般に自由リンクの組み合わせに対して線形な計算時間が期待できる．特に検査する

したがって，この差分リストのデータを先頭から消費していくルールがあったとき，メモが保持されていれ
ば型検査は１回で十分である．

型が１価の (自由リンクを１つしか持たない) 場合に

X = sum(c($h,$t[T]),T)

は，リンク数に対して線形な計算時間が期待できる．

:- int($h), dlist($t)

リンク数はアトム数の定数倍で抑えられるから，ある| X = $h + sum($t[T],T).

いはアトム数に対して線形な計算時間が期待できるメモの保持の一つの問題は，型の定義の仕方とデーとも言える．一方で，価数の高い型の検査には最悪でタの使い方とが異なる場合に，メモを活用できない

リンク数の価数乗だけの時間がかかる可能性がある．

ことである．たとえば差分リスト (dlist 型のプロセ

しかし経験的に，ほとんどの実際的な問題で３価以ス) のデータを末尾から消費していくルールに対して，保持されているメモは役に立たない．

X = rsum($i[c($l,T)],T):- int($l), dlist($i)| X = rsum($i[T],T) + $l.
しかし多くの問題で，型の定義を使い方に対して最適になるよう書き直すことができる．たとえば差分リストの定義を，末尾から消費する場合に最適になるよう書き直すと次のようになる．

typedef rdlist(T,H) {H = T.
A = c(B,T) :- rdlist(A,H), atom(B).
}同様に，ラムダ式の評価文脈 c も 節の定義は簡約操
作に対して最適でないが，次のように書きなおすことができる：

typedef c(Hole,X) {Y = Hole.
Y = Hole @ E :- c(Y,X), e(E).
Y = V @ Hole :- v(V), c(Y,X).
}
ただし，一般のプロセス文脈型に対してこのような変換ができるかどうかは明らかでない．また自動的な最適化も今後の課題である．
メモの保持の別の問題は，メモが計算の進行によって古くなることである．たとえば次のプロセスに対し

fun typeCheck(Parent, Type, Links, Update):if ((Type, Links) に対してメモ m が残っている)
unless (Update)return m.v;
else {(Type, Links) に対して新しいメモ m を作る;m ← {p:Parent, t:Type, l:Links, v:false};}
G ← Links から到達できるアトムを集めたグラフ;
foreach T ypeRule in Type {foreach g in
T ypeRule.LHS と同型な G の部分グラフ {foreach t(X ) in T ypeRule.RHS {X ′ ← g で X に対応するリンク列;
unless (typeCheck(m, t, X ′ , false))
next g;}if(¬m.v) {m.v ← true;
typeCheck(m.p.p, m.p.t, m.p.l, true);}
return true;}}if(m.v) {m.v ← false;
typeCheck(m.p.p, m.p.t, m.p.l, true);}
return false;




図9

依存関係を含むメモ化の手順て e (ラムダ式) 型の検査を行ったとする．
に，ある構造が書換えられたときには，その構造に対X = x -> (y -> (z -> y))
この型検査は成功し，その過程で以下のメモを得る．

して残っていたメモのそれぞれについて，書換え後の構造が性質を保存しているかを検査する必要がある．

X = x -> (y -> (z -> y))

∈

e(X)

X = x

∈

x(X)

X = y -> (z -> y)

∈

e(X)

X = y

∈

x(X)

X = z -> y

∈

e(X)

X = z

∈

x(X)

X = y

∈

e(X)

ここで，たとえばある簡約規則によってアトム z(X)がプロセス a(b,X) に書き換わると，これを部分プロ
セスに含むメモは古くなってしまう．すなわち，これらメモが残り続けていると，本来 e 型でないプロセ
スを e 型と判定してしまう可能性がある．このようラムダ式の例では，アトム z(X) が a(b,X) に書き換わったとき，a(b,X) が “x 型である” という性質を保存しているかを検査する必要がある．x 型でないことがわかれば，これを部分プロセスに持つ３つのプロ
セスが “e である” ことのメモは “e でない” ことのメモに更新しなければならない．

X = x -> (y -> (a(b) -> y))

∈
/

e(X)

X = y -> (a(b) -> y)

∈
/

e(X)

X = a(b) -> y

∈
/

e(X)

メモの効率の良い更新のためには，メモに自体に加えてメモ間の依存関係をも保持しておけばよい．たとえばあるプロセス P に対する型検査の中でその部分

プロセス P ′ に対して型検査が行われたとすると，P
′ラムダ式全体は次のように書き換わる．

に対する検査の結果は P に対する検査の結果に依存

X = succ @ ((x -> x) @ 1)

している．いま P ′ が書き換えられ，これに対するメ

メモを見てみると，簡約基 X = (x -> x) @ succ にモが更新されたとする．このとき，依存関係が保持さ

対して型 v を持たないことが期待されているのだっ

れていればこの変更を効率よく P のメモに伝播するた．そこで，簡約器の書換え後である X = succ にことができる．

対して，その性質を保存していることを検査する．X

図 9 は，メモに加えてメモの間の依存関係も保持するよう変更した型検査の手続きである．引数 Update= succ は v 型を持つから，この検査は失敗し，メモは更新される．

X = succ ∈ v(X)には通常 false を与える．このとき，メモを用いた型検査の省略を行う．書換えによってある構造が破壊されたとき，その構造に対してメモが残っていたならば，書換え後の新しい構造に対して Update を true

この更新は，このメモに依存している別のメモ

X = ((x -> x) @ succ) @ Hole ∈/ c(X,Hole)に伝播し，このメモも更新される．

として型検査を行う．このとき，メモが残っていてもX = succ @ Hole ∈ c(X,Hole)

型検査を行い，メモと実態とが異なっていればメモを

次の簡約基は X = (x -> x) @ 1 であるから，その更新する．メモの更新は親にも伝播する．

文脈 X = succ @ Hole は c(X,Hole) 型を持つこと

メモの更新は誤ったメモを残し続けないためのしくみであると同時に，古くなったメモをも有効に活用しが期待される．更新されたメモを見ると，確かにその事実が反映されていることがわかる．

て型検査を省略するために役立つ．例として，次のラ

5 プロトタイプ処理系

ムダ式

eval(((x -> x) @ succ) @ ((x -> x) @ 1))

拡張された LMNtal のプロトタイプ処理系を，文を 4. 2 節のルールに基づいて評価することを考える．

left-to-right の評価戦略を取っていたから，X = (x献 [8] を参考に実装した．実装した処理系は 1700 行
程度の Gauche†1 プログラムであり，ソースコードと-> x) @ 1 を先に簡約することはできない．実際，こチュートリアルが現在以下のページで公開されていの式の文脈 X = ((x -> x) @ succ) @ Hole に (本る：http://www.ueda.info.waseda.ac.jp/~nara/

節で最適化された) 型 c を検査すると，型検査は失csflatlmn/．

敗し次のメモが残る．

X = ((x -> x) @ succ) @ Hole∈/c(X,Hole)

X = (x -> x) @ succ

∈
/

v(X)

X = Hole∈c(X,Hole)

一方 X = (x -> x) @ succ は簡約することができる．実際，文脈 X = Hole @ ((x -> x) @ 1) に対する型 c の検査は成功し，これまでのメモと合わせ6 関連研究グラフ書換えに基づくプログラミング言語は存在するが，簡約規則の簡約基を生成文法によって指定できるものは著者の知る限りでは存在しない．グラフ書
換え系以外の言語でも，XML や文字列に対しては正規表現などによるマッチングが提供されることがある
が，一般のデータ構造に対しては単純なパターンマッ

るとこの時点で次のメモが残る．

チングしか提供されない．我々が提案する枠組は，パ

X = ((x -> x) @ succ) @ Hole∈/c(X,Hole)

X = (x -> x) @ succ

∈
/

v(X)

X = Hole∈c(X,Hole)

X = Hole @ ((x -> x) @ 1)∈c(X,Hole)

X = (x -> x) @ 1

∈

e(X)

いま， X = (x -> x) @ succ が簡約されると，元のターンを生成文法によって記述することができる点，パターンが列や木だけでなくグラフの集合を表現できる点で一般的である．また，自由リンクを２つ以上持つようなデータを記述できる点は他の言語にない†1 http://practical-scheme.net/gauche/

強力な特徴である．
文脈概念はメタ記法としては研究されているが，言語の第一級の構成要素としては確立していない．特にラムダ計算において，文脈の研究は主に代入やスコープの観点から行われてきた．文脈を第一級に扱うことのできる言語に PLT Redex [7] があるが，これは評価文脈を用いた操作的意味論のモデリングを行うための DSL (ドメイン固有言語) として開発されており，
提案言語とは目標が異なる．

7 まとめと今後の課題
本論文では，グラフの集合を表現するための再帰的な生成文法と，具体的なグラフでなくグラフの持つべきパターンによって簡約基を指定することのできるグ
ラフ書換え言語を提案した．また生成文法に基づいた
グラフのパターンマッチングについて，メモ化の手法がマッチングの効率を改善することを紹介した．
今後の課題としては，プロトタイプ処理系へのメモ化の実装と性能の評価，またデータの使われ方に応じた型定義の最適化がある．
謝辞 本研究の対象である LMNtal の研究開発に携わってきた早稲田大学上田研究室の皆様に感謝します．本研究の一部は科学研究費補助金（基盤研究(B)26280024）の助成を受けて行った．

参 考 文 献[1] 綾野貴之, 堀泰祐, 岩澤宏希, 小川誠司, 上田和紀: 統
合開発環境による LMNtal モデル検査. コンピュータ
ソフトウェア Vol.27, No.4, pp.197–214, 2010.
[2] Arend Rensink: The GROOVE Simulator: A
Tool for State Space Generation. In Proc. Applications of Graph Transformations with Industrial Relevance, LNCS 3062, Springer-Verlag, pp.479–485,
2004.
[3] 乾敦行, 工藤晋太郎, 原耕司, 水野謙, 加藤紀夫, 上田和紀: 階層グラフ書換えモデルに基づく統合プログラミ
ング言語 LMNtal. コンピュータソフトウェア, Vol.25,
No.1, pp.124–150, 2008.
[4] Matthias Felleisen, Robert Hieb: The Revised Report on the Syntactic Theories of Sequential Control
and State. Theoretical Computer Science, Vol.103,
No.2, pp.235–271, 1992.
[5] Bryan Ford: Packrat Parsing: A Practical LinearTime Algorithm with Backtracking. Master’s thesis,
Massachusetts Institute of Technology, 2002.
[6] Casey Klein, Jay McCarthy, Steven Jaconette,
Robert Bruce Findler: A Semantics for ContextSensitive Reduction Semantics. In Proc. 9th Asian
conference on Programming Languages and Systems, LNCS 7078, Springer-Verlag, pp.369–383,
2011.
[7] Matthias Felleisen, Robert Bruce Findler, Matthew
Flatt: Semantics Engineering with PLT Redex. The
MIT Press, 2009.
[8] 村山 敬, 工藤 晋太郎, 櫻井 健, 水野 謙, 加藤 紀夫, 上田 和紀: 階層グラフ書換え言語 LMNtal の処理系. コン
ピュータソフトウェア, Vol.25, No.2, pp.47–77, 2008.
[9] Keith Clark, Sten-Åke Tärnlund: A First Order Theory of Data and Programs. In Information
Processing ’77 (B. Gilchrist, ed.), North Holland,
pp.939–933, 1977.