Think Stitch
PRINCIPIA  最近の更新


Isabelle によるグラフの探索アルゴリズムの部分正当性証明

Theorem Prover Advent Calendar 2013の参加エントリです.

定理証明支援系 Isabelle を使って,グラフの探索アルゴリズムの部分正当性証明をやってみたいと思います. 正確には単なる到達可能なノードの列挙ですけど,かんたんに探索へと改造できますので,よかったら遊んでください. 最近は Coq や Agda の話をよく見かけます.私はどちらも知らないので比較はできませんけど,Isabelle に興味を持つきっかけになれば幸いです.

Isabelle について

Isabelle は Larry Paulson, Tobias Nipkow, Makarius Wenzel らによって開発されている定理証明支援系です. HOL 一族の1つで,Standard ML で記述されています. 公式サイトはこちらになります:

Hoare 論理ライブラリ

Isabelle には Hoare 論理を扱うためのライブラリがついています. これを使うと命令型のプログラム(いわゆる WHILE プログラムと呼ばれているクラス)の部分正当性の証明を行うことができます. ライブラリは Isabelle をインストールしたディレクトリ以下の src/HOL/Hoare にあります.

Hoare 論理ライブラリを使うには,理論ファイルの先頭で次のように記述します.

theory 理論名 imports "~~/src/HOL/Hoare/Hoare_Logic" begin

詳しくは Hoare ディレクトリにある README.html と Examples.thy を見てください.

文法

プログラムの正当性証明は次のように記述します.

theorem "[| 前提1; 前提2; ... |] ==>
VARS 変数1 変数2 ...
{事前条件}
プログラム
{事後条件}"
証明コマンド ...

プログラムの構成要素は次のとおりです.

空文SKIP
代入文変数 := 式
文の連接文; 文
IF 文IF 条件式 THEN 文 ELSE 文 FI
WHILE 文WHILE 条件式 INV {ループ不変条件} DO 文 OD

グラフの探索問題(到達可能なノードの集合を求める問題)

ノードの集合 V と接続関係 R ⊆ V×V および初期ノード p が与えられているとします.V も R も有限であるとします. ここでの問題は初期ノード p から到達可能なノードをすべて求めることとします. 求めるノードの集合 s は反射的推移的閉包 R*を使って次のように表すことができます.

\[ s = R^*(\{p\}) \]

ここで R(A) は関係 R による集合 A の像を表すものとします.きちんと書くと次のようになります.

\[ R(A) = \{y \ |\ \exists x. (x, y) \in R \land x \in A\} \]

Isabelle ではこれを R `` A と書きます.

アルゴリズム

ここでは少し抽象度の高いコードを書いてみたいと思います.

theorem
  "VARS s f
  {True}
  s := {};
  f := {p};
  WHILE f ~= {}
  INV {ループ不変条件}
  DO
    s := s Un f;
    f := R `` f - s
  OD
  {s = R^* `` {p}}"

変数は s と f の2つを用意します.s は求めるノードの集合です. 変数 f はいわゆるフロントで,探索の前線です.計算の断面において,すでに調べ終わった(訪れた)ノードの集合が s で,f にはつぎに調べるノードが入っているとします. 初期状態では s は空集合,フロント f には初期ノード p だけを入れておきます. 事後条件はすでに書いたように s = R^* `` {p} です. R^* は Isabelle での反射的推移的閉包の記号です.

このプログラムではフロント f もノードの集合としています.これをリストにして,要素を先頭から順に取り出し,そこから到達可能なノードをフロントの前に加えたり後ろに加えたりすると,深さ優先になったり幅優先になったりすることはご存知でしょう. ここではその順序を抽象化してしまって,次のフロント計算を一気に行います.

f に含まれるノードから1ステップで到達できるノードの集合は R(f) ですけど,これにはすでに訪れたものや,フロントに入っているものが含まれている可能性があります.そこで,まず現在のフロントを訪問済みとし(s := s Un f),次のフロントは R(f) から s に含まれているものを除いたものとします.つまり,フロント f にははじめて訪れるノードだけが含まれるようにします.Un は和集合です.

この操作を繰り返し,f が空になったら,すべてのノードが手に入ったことになります.

ループ不変条件

一般に,ループ不変条件は事後条件から発見することができます. 事後条件は

\[ s = R^*(\{p\}) \]

で,右辺は定数です.これはエネルギー保存型ループ不変条件のパターンです. 実際,s は初期状態では空集合で,計算が進むにつれて要素が増えていきます. では,一方の減る方は何でしょうか.ここで少しジャンプが必要ですが,答えは R*(f) です. 計算の断面において,初期ノード p から到達できるノードは,すでに訪れたもの s か,あるいは調べ終わっていないフロントから到達できるもののどちらかだからです.したがってループ不変条件は次のようになります.

\[ s \cup R^*(f) = R^*(\{p\}) \]

初期状態では s = {} かつ f = {p} ですから,明らかに成り立ちます.ループが終了した時点では f = {} ですから事後条件そのものになることがわかります.

最初のトライ

ループ不変条件を入れたプログラムは次のようになります.

theorem
  "VARS s f
  {True}
  s := {};
  f := {p};
  WHILE f ~= {}
  INV {s Un R^* `` f = R^* `` {p}}
  DO
    s := s Un f;
    f := R `` f - s
  OD
  {s = R^* `` {p}}"

apply(vcg) というコマンドを発行すると,Isabelle はプログラムを証明すべき論理式に変換してくれます.

proof (prove): step 1

goal (3 subgoals):
 1. !!s f. True ==> {} Un R^* `` {p} = R^* `` {p}
 2. !!s f.
       s Un R^* `` f = R^* `` {p} & f ~= {}
       ==> s Un f Un R^* `` (R `` f - (s Un f)) = R^* `` {p}
 3. !!s f.
       s Un R^* `` f = R^* `` {p} & ~ f ~= {}
       ==> s = R^* `` {p}

!! と ==> はそれぞれメタレベルでの全称限量と含意です.詳細は省略します. 条件が3つになるのは,事前条件,ループ不変条件,事後条件のそれぞれについて証明すべきことがあるからです.

ここでは auto コマンドを使って,できるだけ Isabelle にがんばってもらうことにします.

apply(vcg)
apply(auto intro: transitive_closure_trans)
apply(erule contrapos_np)

"intro: transitive_closure_trans" というのは推移的閉包に関する推移律を使ってくださいという指示です. erule contrapos_np は結果を見やすくするためにつけただけで,意味はありません. ここまでで次のようになります.

proof (prove): step 3

goal (1 subgoal):
 1. !!s f x xa.
       [| s Un R^* `` f = R^* `` {p}; x : f; (p, xa) : R^*;
          xa ~: f; xa ~: s |]
       ==> xa : R^* `` (R `` f - (s Un f))

これはどこから出てきたかというと,ループ不変条件が不変であることの証明課題の残りです. 事前,事後に関する式は自動で証明されました. ループ不変条件が不変であるとは,ループ本体の2つの文を実行した後でも同じ条件が成り立つということです. すると,各文を実行する前では次のような条件が成り立たなければならないことになります.(texttt が出ない...見にくくてごめんなさい)

\[ \begin{split} &&[\textrm{s := s Un f}\,][\textrm{f := R `` f $-$ s}\,] s \cup R^*(f) = R^*(\{p\}) \\ &=&[\textrm{s := s Un f}\,] s \cup R^*(R(f) - s) = R^*(\{p\}) \\ &=& s \cup f \cup R^*(R(f) - (s \cup f)) = R^*(\{p\}) \end{split} \]

これがループ不変条件

\[ s \cup R^*(f) = R^*(\{p\}) \]

から言えればいいわけです(あと f ~= {}). 定石にしたがって考えると,左辺に属する場合はほぼ自明です. しかし右辺に属する場合 x ∈ R*({p}) は残った条件を示すことができません. ちょっと荒っぽい議論ですけど,理由は次のとおりです. まずループ不変条件の仮定から,s に属する場合は自明なので,残りは

\[ x \in R^*(f) \]

となります.したがって

\[ y \in f \land (y, x) \in R^* \]

となる y が存在します.x が s や f に含まれている場合は自明なので除くとすると,y は x とは異なることになります. したがってさらに

\[ y \in f \land (y, z) \in R \land (z, x) \in R^* \]

となる z があるはずです.

この z はフロント f に属するノード y から1ステップで到達できるノードです.これには3つの可能性があります. s に属する場合,f に属する場合,そしてどちらにも含まれない場合です. 最後の場合は新しいノードということで,条件に当てはまります. f に属する場合は,再び次のノードがあるはずで,R が有限ならばかならずいつかは s か 新規にたどり着きます. しかし問題は s に属する場合です.s に属するノードについては何も条件がないので,これ以上何もいうことができません. これはループ不変条件が弱いことが原因で,よく起こることです.このような場合には条件を強化する必要があります.

強化したループ不変条件

結論だけをいうと,強化したループ不変条件は次のようになります. すでに訪れたノードから1ステップで到達できるノードは,かならず s か f に含まれているという条件を追加してあります. このおかげで,s に戻ってしまうようなルートに対処できるようになります.

\[ \begin{split} & s \cup R^*(f) = R^*(\{p\}) \land \\ & R(s) \subseteq s \cup f \land \\ & p \in s \cup f \end{split} \]

補助定理

先ほどの議論でみたように,フロントから1ステップ進んだ先のノードが再び s やフロント f に戻ってしまう場合があります. この部分の証明には数学的帰納法が必要になります.ここでもちょっとジャンプしますけれども,必要になる補助定理をあらかじめ用意しておくことにします.

lemma x0: "[| (p, x) : R^*;
  R `` s <= s Un f
  |]
  ==>
  (p : s | p : f) -->
  x : s Un f Un R^* `` (R `` f - (s Un f))"
apply(erule converse_rtrancl_induct)
apply(auto)
done

通常,Isabelle で数学的帰納法の証明を行う場合には,induct_tac というコマンドを使うのですが,反射的推移的閉包の場合には,専用の定理がいくつか用意されています.converse_rtrancl_induct はそのうちの1つで,つぎのように定義されています.

[| (?a, ?b) : ?r^*; ?P ?b;
   !!y z. [| (y, z) : ?r; (z, ?b) : ?r^*; ?P z |] ==> ?P y |]
==> ?P ?a

閉包でたどり着けるすべてのノードについて,述語 ?P が成り立つことを証明するためのものです. 詳細は省略します.これを使うと,上のように auto で証明が完了します.

正当性証明

強化したループ不変条件に置き換え,補助定理を使うと,次のように証明が完成します.

theorem
  "VARS s f
  {True}
  s := {};
  f := {p};
  WHILE f ~= {}
  INV {
    s Un R^* `` f = R^* `` {p} &
    R `` s <= s Un f &
    p : s Un f
  }
  DO
    s := s Un f;
    f := R `` f - s
  OD
  {s = R^* `` {p}}"

apply(vcg)
apply(auto intro: transitive_closure_trans)
apply(drule x0)
apply(auto)
apply(drule x0)
apply(auto)
done

停止性の証明

ここでは部分正当性だけ証明しました.つまり,プログラムがもし終了したとしたら事後条件が成り立つけど,終了するかどうかについては保証していません.こちらは停止性の証明として別に行う必要があります.

停止性の証明はちょっと面倒です.まず R が有限だという条件を入れておく必要があります. それから,ループ本体を実行するたびに減少する関数で,かつ下限を持つものを見つけなければなりません. この例では,次のような関数を考えると証明することができます.

\[ \textrm{card} (R^* (\{p\}) - s) \]

ここで card(S) は集合 S の要素の数です. 計算が進むにつれて s の要素が増えるので,関数の値が減少することを示すことができます. しかし集合の要素の数ですから 0 が下限です.したがって永遠にループがまわり続けることはできません.したがってループが終了することがわかります.ただし,ループ不変条件をもうちょっと強化しなければならないかもしれません :P

補足

条件を指定して,それを満たすノードが発見された時点でループを終了するように改造するのはかんたんです. フロント f をリストにして,深さ優先や幅優先のように,より詳細なプログラムにすると,証明はかなり面倒になります.それでも大局的な論理構造はかわらないと思います.

2013/12/04
© 2013,2014,2015 PRINCIPIA Limited