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

LMNtal におけるグラフ書換え操作の Coq による形式化
信夫 裕貴

田辺 良則

上田 和紀

LMNtal は階層グラフ書換えに基づく言語モデルであり，書換えルールの適用によってグラフの接続・階層構造を書換えていくことで計算が進行する．LMNtal プログラムはコンパイラによって手続き的な中間命令列に変換され，解釈・実行される．これまで LMNtal コンパイラの形式的な検証は十分に行われてこなかったが，処理系が複雑化・高度化するにつれてコンパイルや最適化変換の正当性保証が重要性を高めている．そこで我々は，証明支援系 Coq を用いて LMNtal コンパイラを形式化し，正当性が検証された処理系を構築することを目指している．本研究ではその第一歩として，階層構造を持たないグラフの書換え操作の Coq による形式化およびその正当性検証について述べる．

ライブラリ (Dupra 2001) ではグラフに頂点と辺を再1 はじめに帰的に追加する形でグラフを定義しているが，通常のグラフ構造の表現と操作の形式化は，リストや木の再帰的データ構造と異なり，等価なグラフが一意的にような再帰的データ構造と違って自明ではない．グラ構成されるわけではない．また，各頂点の出力辺が順フの数学的定義になるべく忠実な形をとるのか，プロ序付けられた根つき有向グラフは余再帰的に定式化す

グラム中での表現に忠実な形をとるのか，などの選択ることも可能である (Picard and Matthes 2010) が，肢がある．

他のグラフや異なる同型性概念に対して同様の手法

さらにグラフは，ループや多重辺の有無，辺の向きを適用することは難しい．の有無などで多くのクラスに分けることができ，成コンパイラ検証の観点からは，手続き型言語と比べり立つ性質もそれぞれ異なってくるし，適切な定式て宣言型言語コンパイラの技術的蓄積は十分でない．

化の方法も異なってくる．このため，一般的なグラフ

また，宣言型言語は手続き型言語と比べてソース言語に対する証明支援系のライブラリは存在するもののとターゲット言語のセマンティックギャップが大きく，（例：Coq の GraphBasics），再利用性は高いとはいコンパイラの正当性検証の必要性はより高い．実際，えない．

LMNtal コンパイラの最適化機能には，対処が容易

グラフ構造は、再帰に基づく定式化が必ずしも不可能なわけではない．たとえば，Coq の GraphBasics
Formalization of the Graph Rewriting Operations ofLMNtal by Coq.
Yuuki Shinobu, 早稲田大学大学院基幹理工学 研究 科
情報理工学専攻, Graduate School of Fundamental
Science and Engineering, Waseda University.
Yoshinori Tanabe, 国立情報学研究所, National Institute of Informatics.
Kazunori Ueda, 早 稲 田 大 学 理 工 学 術 院 情 報 理 工 学科, Dept. of Information and Computer Science,
Waseda University.

でない問題点があることが指摘されていながら長期間未解決であった．

LMNtal は階層グラフ書換えに基づく並行言語モデルであり，グラフの部分構造をルールによって書換えていくことで計算を表現する．近年では，その表現力の高さからモデル検査器のためのモデル記述言語としての発展が著しく，LMNtal 実行時処理系は並列モデル検査器を備えている．このことからも，LMNtal 処理系自体の正当性の検証は重要な要請であると考えている．我々は，定理証明支援系 Coq を用いて LMNtal コンパイラと処理系の形式化を行うこαβγαβ
X=Yとで，信頼性の保証された LMNtal 処理系を進化的に構築していくことを目指している．

XaYbZ
cefγZdW

本論文では，LMNtal コンパイラ検証のための第一歩として，階層構造を持たないグラフとその書換え操

図1

書換えルールの例

作を Coq 上で形式化し，一部の性質について形式的証明を与えた．

先同士が接続される．

• 元々存在したアトム a，b，c が削除される．

2 言語モデル LMNtal とその処理系• 3 つの 1 価アトム d，e，f が新しく作られる．

2. 1 言語モデル LMNtal• d は c が接続していた箇所に接続される．

LMNtal は階層グラフ書換えに基づく並行言語モ• e と f が接続される．

デルである．LMNtal の階層グラフ構造をプロセスこの書換えを図で表現したものが図 1 である．ここ(process) と呼び，プロセスはアトム (atom)，リンで，α, β, γ はマッチした構造が接続する外部の構造

ク (link)，膜 (membrane) から構成される．リンの一部を表している．

クと膜はそれぞれプロセス間の接続構造，階層構造をプロセステンプレート a(X), b(Y) などは，アト表す．グラフ書換えの規則を表すルール (rule) を適

ム a，b が直接接続されているような構造にもマッチ用し動的にグラフを書換えていくことでプログラムする．の計算が進行する．
アトムは n(n ≥ 0) 個の順序付けられた引数を持ち，リンクは 2 つのアトムの引数の間を一対一に接続する無向辺である．引数の個数をそのアトムの価

2. 2 LMNtal 言語処理系
LMNtal 言語処理系は主に LMNtal コンパイラと実行時処理系からなる．

数 (arity) といい，n 個の引数を持つアトムを n 価

LMNtal プログラムは，LMNtal コンパイラによっのアトムという．アトムの名前と価数の組をファンクてルール毎に中間命令列に変換される．そして，中間タ (functor) と呼ぶ．

命令列が実行時処理系によって解釈・実行されること

書換えルールはによって，プログラムが実際に動作する．

Head :- Body

LMNtal の中間命令列はレジスタ変数を用いた SSAのように記述し，左辺をヘッド部，右辺をボディ部と形式であり，ヘッド部のマッチング処理とボディ部へ呼ぶ．ルール両辺は部分グラフによって表現し，これの書換え処理を手続き的に実現するものである．それをグラフテンプレート (graph template) と呼ぶ．

ぞれ，マッチングを処理する命令列をヘッド命令列，ルールは，ヘッド部に記述されたグラフテンプレート

マッチした構造に対する書換えを行う命令列をボディにマッチしたプロセスに対して適用され，ボディ部に命令列と呼ぶ．

記述した構造へと書換えられる．
次のようなルール

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

図 2，図 3 はそれぞれ前節のルールをコンパイルすることで生成される中間命令列のヘッド命令列とボ:-

X=Y,d(Z),e(W),f(W)

ディ命令列である．の適用を考える．このルールは，3 つの 1 価アトム a，b，c を持ち，それぞれの第 0 引数が任意の場所へ接3 中間命令の再設計続しているような部分構造にマッチする．マッチした

現状の LMNtal コンパイラを即座に検証すること構造に対して，以下のようにしてグラフが書換えらは困難．その理由の一つとして，リンク操作に関わるれる．

中間命令にポインタレベルのものが存在し，命令列• 右辺の X=Y によって左辺のリンク X，Y の接続の形式的な扱いが難しいという点が挙げられる．そspec
findatomfindatomfindatomjump[1, 4][1, 0, ’a’_1][2, 0, ’b’_1][3, 0, ’c’_1][L122, [0], [1, 2, 3], []]図2

ヘッド命令列newlink

unify
図4

spec
commitdequeueatom
dequeueatom
dequeueatom
removeatom
removeatom
removeatom
unify
newatomnewatomnewatom
relinknewlink
enqueueatom
enqueueatom
enqueueatom
freeatomfreeatomfreeatomproceed[4, 7]["_aXbY", 0]
[1]
[2]
[3]
[1, 0, ’a’_1][2, 0, ’b’_1][3, 0, ’c’_1][1, 0, 2, 0, 0][4, 0, ’d’_1][5, 0, ’e’_1][6, 0, ’f’_1][4, 0, 3, 0, 0][5, 0, 6, 0, 0]
[6]
[5]
[4]
[1]
[2]
[3]
[]

relinkリンク操作

トム atom2 の第 pos2 引数を接続する．

unify [atom1, pos1, atom2, pos2, mem]
膜 mem に存在するアトム a1 の第 p1 引数の接続先と，
アトム a2 の第 p2 引数の接続先を接続する．

relink [atom1, pos1, atom2, pos2, mem]
膜 mem に存在するアトム atom1 の第 pos1 引数と，ア
トム atom2 の第 pos2 引数の接続先を接続する．

getlink [-link, atom, pos]
アトム atom の第 pos 引数の接続先への参照を linkに格納する．

inheritlink [atom1, pos1, link2, mem]
アトム atom1 の第 pos1 引数と，リンク参照 link2

図3

ボディ命令列こで，検証を見据えた扱いやすい命令体系を再設計した．

によって参照される引数の接続先を接続する．

ここで，getlink 命令と inheritlink 命令はアトムの引数への参照を直接扱う命令であり，最適化処理で relink 命令を分解するために用意されている．し3. 1 既存の命令体系とその問題点

かし，これらの命令を使用した最適化変換は正しさ

既に動作している LMNtal 処理系では，リンクのが保証されておらず，実際に実行結果が不正なグラフ書換えを主に newlink, unify, relink の基本的なリ構造となる場合もあった．これは，処理系の正当性検ンク操作命令と，getlink, inheritlink といった最証を目指す背景であるが，まずは短絡リンクを考慮適化用命令の組み合わせによって実現している．これしたリンク書換えの実現とその安全性検証のために，らの命令の引数形式と動作は以下のようになってい命令体系の再設計とポインタレベル命令の回避につる．

いて考える必要性があった．

newlink [atom1, pos1, atom2, pos2, mem]
膜 mem に存在するアトム atom1 の第 pos1 引数と，アで行う．また，接続先が存在しない引数をリンク名の代わりに. で表すことにする．

R に対して以上の変換を行うとa(., W), c(Z), b(., X, Y):-a(Y, .), d(Z, ., W), c(X)となる．

(a)
図5(b)

(c)

swaplink 命令の動作

次に (1) の処理を行う．右辺に X=Y の形の接続が存在したら，対応する左辺のアトム引数に対する unify命令を生成する．その後，X=Y をルールから除外し，3. 2 互換によるリンク書換え
グラフ書換え操作を実現する命令体系およびコンパイル処理を，newatom，removeatom，unify，newlinkに接続先の交換を行う swaplink 命令を新たに加えた

5 命令を主要命令として再設計した．

左辺における X と Y は. に置き換える．

R の右辺には X=Y の形が存在しないため，ここでは何もしない．
次に (2) の処理を行う．まず，両辺に存在する同型なアトム同士の対応を考える．ここで，ファンクタが等しいアトムを同型とみなす．そして，対応が付けら

swaplink [atom1, pos1, atom2, pos2]

れない（他方の辺に同型なアトムが存在しない）アト

アトム atom1 の第 pos1 引数の接続先と，アトムムについて，対応が付けられるようにアトムを補う．

atom2 の第 pos2 引数の接続先を交換する．

ここで，補うアトムの引数はすべて. とする．

R において同型なアトムの対は a の対と c の対で
swaplink 命令は図 5 に示すように，非接続も含めたある．また，左辺に対して d，右辺に対して b を補う．

交換（図の (b)）を行う．ここでは，swaplink 命令

ここまでの変換を R に施すとを含めたコンパイル手法について説明する．
大まかに，コンパイル処理は次の各処理からなる．

a(., W), c(Z), b(., X, Y), d(., ., .):-a(Y, .), d(Z, ., W), c(X), b(., ., .)となる．

(1) ルール右辺に存在する X=Y に対して unify 命令を生成する．

(2) リンク列の置換を互換に分解し swaplink 命令を生成する．

(3) ルール右辺に存在する内部リンクに対してnewlink 命令を生成する．

ここで，右辺に対して補ったアトムはルール適用によって削除されるので，対応する左辺のアトムに対する removeatom 命令を生成する．一方，左辺に対して補ったアトムは適用によって生成されるので，対応する右辺のアトムに対する newatom 命令を生成する．
ここまでで，アトムの生成と削除に関する処理が完了する．

以下では，次のルール R:-

次に，アトムの並びの中で対応するものが同じ位置

a(I, W), c(Z), b(I, X, Y)になるように適当に並び替える．R の両辺のアトムa(Y, J), d(Z, J, W), c(X)の並びを対応を意識して並び替えるとのコンパイルを例に説明する．
まず，内部リンクに関して前処理を行う．ルール左a(., W), c(Z), b(., X, Y), d(., ., .):-a(Y, .), c(X), b(., ., .), d(Z, ., W)

辺に存在する内部リンクは破棄し，接続先が存在しなとなる．さらに，並び替え後のルール両辺のリンクのいとみなす．ルール右辺に存在する内部リンクは新しみを取り，ルールをリンク列からリンク列への置換とく接続されることを表しているため，newlink 命令みなす．の対象となる．ただし，実際の命令生成は処理の最後.WZ.XY... −→ Y.X...Z.W

この置換は 4 回の互換で実行できる．1 回の互換につことにする．この表現において，ある 2 つのポートがき互換の対象となったアトム引数に対する swaplink

接続されていることはこの 2 つのポートが互いに参命令を生成する．

照し合うことで表され，この場合に限りグラフ上で辺最後に (3) の処理で，最初に判明していた「右辺でが存在することとする．これは，この表現の範疇で不新しく接続されるリンク」に対する newlink 命令を正な構造を持つグラフが存在しうることを意味する．

生成する．
以上で，R に示したようなルールのコンパイルが実現できる．

まず，リンクを表現するために，C 言語や Java の参照に相当する概念であるポートの集合 Port を次のように定める．

Port:=(N × N) ∪ {null}

4 グラフ書換え操作の形式化

唯一の要素 null は，いかなる点も参照しないポート

本論文で行った LMNtal グラフ書換えの Coq 上でである．ポート null が指す点は未定義だが，任意のの形式化について述べる．

Coq 上での形式化は，主に以下の項目に分けて行った．

点に null を格納することは可能である．
次に，アトムの集合 Atom の各要素 a ∈ Atom について，以下を定める．a が n 価のアトムであるとき(a) 扱う対象となるデータ構造の定義(b) データ構造に対する処理（関数）の定義(c) 命題の定義(d) 補題，定理の証明(a) では，アトムやリンクの表現，それらからなるグラフ構造の表現を定めた．(b) では，実際の処理となるリンク書換え操作や，それを実現するための補助関数を実装した．本論文では newlink 命令と swaplink命令の実装を示す．(c) では，データ構造の間の関係や証明すべき性質を論理式で定義した．(d) では，補arity(a)=nとする．また，args(a){(p, k) ∈ Port × N | k < arity(a)}=とする．すなわち，n 価アトムは，n 個の順序付けられたポートを持つレコードである．
グラフの集合 Graph を，識別番号からアトムへの対応の集合として次のように表現する．

Graph:={F | F : N → Atom⊥ }ただし，Atom⊥:=Atom ∪ {⊥}助関数の性質などの小さな補題の証明，およびそれらとする．アトムを一つも含まないグラフは Gϕ (n) = ⊥を利用したより大きな定理の証明を行った．本論文でによって定義できる．定義より，グラフ Gϕ はリンク

は newlink に関して説明する．

をひとつも持たない．さらに，あるグラフ G 上で識別番号 k にアトム a を対応させた新しいグラフ G′ を

4. 1 書換え対象となる LMNtal グラフの形式化

返す関数 add を書換え対象となる（すなわち実行時における）LM-add(G, k, a)=

Ntal グラフの形式化について述べる．なお，本論文

G′ (n)=が対象とする LMNtal グラフは階層構造を持たず，アトムのみから構成されるものである．
一般に，グラフは頂点集合 V と辺集合 E の組による表現 G = (V, E) が普通だが，本論文では実際の処理系実装を意識した構造による表現を選択した．この表現ではグラフは辺の集合を明示的には持たず，代わりに頂点集合の各要素が相互参照しあうフィールドを持つレコードとなる．ここで，アトムの識別番号と引数番号で一意に区別される点をポート (port) と呼ぶ′G{a(n = k)G(n) (n ̸= k)と定義する．これはグラフへのアトムの追加を表している．逆に，識別番号 k に対応するアトムの削除はremove(G, k)=G′ (n)=′G{⊥(n = k)G(n)(n ̸= k)と定義できる．
以上を Coq 上で表現したものが図 6 である．

Inductive Port :=null | link : nat -> nat -> Port.
Record Atom := { args : list Port }.
Definition Graph := nat -> option Atom.
Definition empty : Graph :=fun _ => None.
Definition add (G : Graph) k a : Graph :=fun n => if eq_nat_dec n k then Some aelse G n.

図6Definition swaplink p1 p2 G :=match (deref G p1, deref G p2) with| (Some p1’, Some p2’) =>if eq_port p1’ p2 then Some Gelse
G1 <- setport G p1 p2’ ;G2 <- setport’ G1 p2’ p1 ;G3 <- setport G2 p2 p1’ ;setport’ G3 p1’ p2| _ => Noneend.

データ構造の定義
図9

Definition bind {A B} a (f : A -> option B) :=match a with| Some x => f x| None => Noneend.

swaplink の定義更新されたグラフを返す．ポートが存在しない点を指す場合や，null であった場合には代入操作が失敗し，2 つの代入操作のいずれかが失敗すれば全体も失敗しNone を返す．

Notation " v <- M ; F " :=(bind M (fun v => F))(at level 30, right associativity).

同様に，swaplink 命令の実装は以下のようになる．

ここで，setport’ 関数は代入先のポートが null の図7

結合子の関数と記法の定義

場合には何もしない（失敗しない）ように setport 関数を拡張したものである．これは，swaplink 命令がDefinition newlink p1 p2 G :=G’ <- setport G p1 p2 ;setport G’ p2 p1.

接続先が存在しないリンクも含めた互換を行うためである．

5 リンク書換え操作に関する定理の証明
図8

newlink の定義

Coq 上で実現した各処理についての補題，リンク書換え命令の仕様を述語として定義し，証明を行っ

4. 2 操作の形式化
前節の定義を用いて，実際にグラフを書換える操作を Coq 上で実現した．
例 と し て ，以 上 の 表 現 の 上 で newlink 命 令 とswaplink 命令の実装である newlink 関数，swaplink関数を定義する．
ここで，option 型の値に関する場合分けを要するので，これを簡略表記するための結合子を定義する．

newlink 関数はアトム引数への接続する 2 つのポートに対してそれぞれ他方への参照代入を行う．これを表現したものが次の定義である．

setport 関数はポートの指す引数へポートを代入するもので，代入操作が正しく行われた場合は状態がた．ここでは newlink 関数に関して述べる．
あるグラフに対してリンク操作命令を実行した結果のグラフが満たすべき基本的な性質として，• 命令で指定された箇所が正しく接続される• 他の箇所の接続関係を変更しないの 2 つが挙げられる．以下では，この性質の newlink関数に対する形式化について述べる．
主となる命題を記述するため，いくつか補助的な述語を定義する．
グラフ G 上で互いに異なるポート p と q が接続している（相互参照している）ことを表す述語 Linked，
ポート p の参照先が異なるグラフ間で同一であることを表す述語 RefEq をそれぞれ次のように定義する．

d. ポートに関する補題
setport deref : ∀ G G′ p q,

Linked G p q :=′p ̸= q ∧ Refers G p q ∧ Refers G q p.
RefEq G G′ p :=setport G p q = Some G′ ⇒ Refers G′ p q.
setport deref diﬀatom : ∀ G G′ a i p,∀q, Refers G p q ⇒ Refers G′ p q.

setport G (link a i) p = Some G′ ⇒これらの述語を用いると，newlink 関数が満たすべき∀ a′ i′ , a′ ̸= a ⇒接続の条件はderef G′ (link a′ i′ ) = deref G (link a′ i′ ).

newlink connect : ∀ G G′ p1 p2 ,setport deref diﬀpos : ∀ G G′ a i q,′p1 ̸= p2 ∧ newlink p1 p2 G = Some G ⇒setport G (link a i) q = Some G′ ⇒Linked G′ p1 p2 .

∀ a′ i′ , i ̸= i′ ⇒newlink preserve : ∀ G G′ p1 p2 ,deref G′ (link a′ i′ ) = deref G (link a′ i′ ).

p1 ̸= p2 ∧ newlink p1 p2 G = Some G′ ⇒(∀ p, p ̸= p1 ∧ p ̸= p2 ⇒ RefEq G G′ p).

setport deref diﬀport : ∀ G G′ p q,
setport G p q = Some G′ ⇒∀ p′ , p ̸= p′ ⇒ deref G′ p′ = deref G p′ .となる．
以下に，newlink 関数の性質証明のために必要と

setport diﬀ : ∀ G G′ p1 q1 p2 q2 ,Refers G p1 q1 ∧ p1 ̸= p2 ∧なった補題を挙げる．

setport G p2 q2 = Some G′ ⇒Refers G′ p1 q1 .

a. リストの要素置換に関する補題′

subst prop1 {X} : ∀ l l n (x : X),
subst l n x = Some l′ ⇒まず，命題 newlink connect の非形式的な証明′を記す．

get l n = Some x.
′

subst prop2 {X} : ∀ l l n (x : X),
subst l n x = Some l′ ⇒定理∀ i, i ̸= n ⇒ get l′ i = get l i.

ト p1 , p2 に対して，newlink p1 p2 G が成功して結果任意のグラフ G 上で互いに異なる任意のポーのグラフ G′ を返すならば，グラフ G′ 上で p1 , p2 は接続されている．

b. アトムの追加と取得に関する補題
addatom diﬀ : ∀ G a i j,i ̸= j ⇒ (addatom i a G) j = G j.

証明 まず，最初の代入 setport G p1 p2 の成否について場合分けをする．これが失敗した場合，newlinkc. アトム引数に関する補題は結果を返さないため，定理の前提と矛盾する．した′setarg subst : ∀ a a i p,がって，setport G p1 p2 は変更後のグラフ G1 を返′setarg a i p = Some a ⇒すと仮定して良い．また，この時点でグラフ G1 への′subst (args a) i p = Some (args a ).
setarg getarg prop : ∀ a a′ i p,′setarg a i p = Some a ⇒代入 setport G1 p2 p1 が成功し，最終的なグラフ G′を返すことも仮定される．
次に，補題 setport deref から，′getarg a i = Some p.

setport G p1 p2 = Some G1′setarg getarg diﬀ : ∀ a a i p,′setarg a i p = Some a ⇒′∀j, i ̸= j ⇒ getarg a j = getarg a j.

⇒Refers G1 p1 p2が成り立つ．さらに，p1 ̸= p2 であるから，補題

setport diﬀ よりRefers G1 p1 p2 ⇒ Refers G′ p1 p2

の 2 点を保証する補題を要した．

Lemma newlink_connect :forall G G’ p1 p2,
p1 <> p2 ->newlink p1 p2 G = Some G’ ->Linked G’ p1 p2.
Proof.
intros G G’ p1 p2 Hsep H1.
unfold newlink in H1.
remember (setport G p1 p2) as someG1.
rename HeqsomeG1 into H2.
symmetry in H2.
destruct someG1 as [G1|]; simpl in H1.

また，2 つの書換えが独立であるかという点は，破壊的代入を扱う上で重要な性質であった．

6 LMNtal コンパイラの正当性検証
前節までで，Coq 上で形式化したグラフ表現を用いて実行時のリンク書換え操作の性質証明を行った．
ここでは，本研究の目標である LMNtal コンパイラの正当性検証について述べる．
大まかに，以下のステップを進めることで目標とし(* setport succeeded *)unfold Linked.
apply setport_deref in H2.
eapply setport_diff in H2; try eassumption.
apply setport_deref in H1. tauto.ている検証を達成しようと考えている．

(1) LMNtal におけるグラフ書換えルール
Head :- Bodyの意味を定義する．これは，このルールを適用するこ(* setport failed *)inversion H1.
Qed.とでグラフ G1 が G2 に書換わるという命題[[ Head :- Body ]](G1 , G2 )を定義することで与えられる．同時に，あるグラフ

図 10

G がグラフテンプレート T にマッチするという命題

Coq における証明スクリプト

Match(T, G)である．また，2 つめの代入に関して

setport G1 p2 p1 = Some G⇒も合わせて定義する．
′(2) 書換えを実現する中間命令列の意味論を定義する．

′

グラフ Graph とは別に，実行時におけるレジスタ番Refers G p2 p1が成り立つ．以上より号とアトムの対応といったの環境を Env とおくと，

p1 ̸= p2 ∧ Refers G′ p1 p2 ∧ Refers G′ p2 p1⇔′[[ I ]] : Graph × Env → Graph × Env

Linked G p1 p2である．

各中間命令 I の意味論は，それぞれについて関数□

図 5 は，以上の証明を Coq 上で記述した証明スクリプトである．の定義を与えることによる．この定義から，中間命令のリストである中間命令列 C の意味論[[ C ]] : Graph × Env → Graph × Env
も自然に定義される．

5. 1 考察(3) 与えられた書換えルール R を中間命令列 C に変本論文時点で，スクリプトの規模はリストに関する換するアルゴリズム，すなわち基本的な関数と補題が 218 行，グラフ操作に関するC実装と証明が 873 行程度である．また，本論文に記=compile(R)なる compile を実装する．

載しなかったものも含めて 50 程度の補題・定理の証明を行った．
基本的なデータ構造からグラフ構造まで共通して，以上の形式化の下で，アルゴリズム compile の正当性を示す主定理は次のようになる．

ある一部を書換えて状態が更新された結果を返す関Match(Head , G1 ) ∧数が存在し，それぞれについて[[ compile(Head :- Body) ]](G1 , e1 ) = (G2 , e2 )1. 変更が期待通り行われていること
2. 他の部分は元の状態と同一であること⇒ [[ Head :- Body ]](G1 ) = G2
以上が LMNtal コンパイラ検証の全体像である．なお，本論文で扱ったグラフ書換え操作の性質検証は，また，中間命令体系の検証に向けた再設計では，数個々の中間命令の実装の正しさを保証することに繋学的な扱いの利点から置換と互換を利用した．ここがっている．

で，互換の積を逆順にしたものが元の置換の逆元になることを考えると，中間命令列を逆向きに実行するこ

7 まとめと今後の課題とでグラフ書換えの逆実行を実現できる可能性が見え

グラフ構造の書換え操作に関して，グラフ構造の表てくる．グラフ書換えの逆実行は，LMNtal プログラ

現，操作の定義，命題の定義と証明を Coq 上で行うムを使用したモデル検査で利点となると考えられる．

ことで形式化を行った．また，その過程で通常の数学

LMNtal モデル検査は，プログラムを非決定的に実行的なグラフ表現との差異や，不正構造を許容した表現し，グラフ書換えを状態遷移とみて状態を網羅的に探による形式化に関する知見を得ることができた．

索することによって実現されている．網羅的な探索のCoq での実装，証明に関して，今回は高度なタクためには全状態を保持しておく必要があるとされてティックや拡張ライブラリを利用しなかった．今後さきたが，グラフ書換えの逆実行が可能である場合，一らに扱う対象の規模が拡大していくことを考えると，部の状態については必要に応じて復元することが可

証明の自動化手法や記法の簡略化についても積極的能となる．したがって，グラフ書換えの逆実行の実現に習熟する必要があると考えられる．

によって状態保持のコストを削減することができる．

本論文で形式化を行ったのは処理系の一部分であり，コンパイラの正当性検証へ進むためには多くの課書換えルール逆実行とその正当性検証については，将来的な拡張として検討していく．

題が残されている．今回はグラフの書換えに注目した

謝辞 本論文作成にあたって，多くの貴重な意見を下が，一連のコンパイル処理と書換えルールの検証にはさった上田研言語班の皆様に感謝致します．本研究の第 6 節に示すようにルールやマッチングなど本論文

一部は，科学研究費補助金（基盤研究 (B)23300011）

で扱っていないものについての形式化を進める必要がの補助を得て行った．

ある．