Think Stitch
PRINCIPIA  最近の更新


Isabelle によるグラフの循環検出アルゴリズムの部分正当性証明

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

グラフが初期ノード s0 と接続関係 R ⊆ V × V で与えられているとします.V はノードの集合です. 与えられたグラフの中に,初期ノードから到達可能な循環があるかどうかを調べるアルゴリズムを考えます. もしあれば,具体的にパスを求めるものとします.このアルゴリズムの部分正当性を証明してみたいと思います.

グラフ探索アルゴリズムのときと同じように,少し抽象度の高いレベルでプログラムを書きたいと思います.抽象度が高いというのは,データ構造全体を見渡したり,操作したりする手続きをプリミティブとして使うという意味です.そういう手続きを用意すれば実際に動かすことができます.手続きには並列に実行できる部分がかなりありそうなので,並列アルゴリズムの雰囲気もあると思います.

初期ノードから到達可能な循環が存在する条件

循環が存在するという条件は,推移的閉包を使って次のように表すことができます.

\[ \exists p. (p, p) \in R^+ \]

この循環が初期ノード s0 から到達可能である条件を加えると次のようになります.

\[ \exists p. (s0, p) \in R^* \land (p, p) \in R^+ \]

初期ノード s0 自体が循環に含まれている場合もあり得るので,こちらは反射的推移的閉包になります.

具体的な事後条件では,あと2点考慮が必要です.1つは見つからなかった場合の条件を表すことです.もう1つは,循環のパスを具体的に求めることが要求されているという点です.これらについてはプログラムの変数に依存するので,具体的なコードで見ていただくことにします.

アルゴリズム

パスの集合を表す変数 s を用意します.変数はこれだけです.初期状態では,初期ノードだけからなる長さ1のパスだけを含むようにします.パスはリストで表して,ノードを前に追加していくこととします.逆順になってしまいますけど,リストなので前に追加(cons)する方が都合がよいでしょう :P

戦略は次のとおりです.ループの1ステップで,集合 s に含まれているすべてのパスをグラフをたどって1つ延ばします.このとき,パスに追加したノードがすでにパスに含まれていた場合は循環があることになります.行き先のないノードに達したパスは取り除きます.これを繰り返すと,最終的には循環が発見されるか,あるいはすべてのパスが終端に達して集合 s が空になります.(もちろん R は有限だとします.)

集合 s に含まれるパスの中に,1つ伸ばしたら循環になるものがあるという条件は次のように書くことができます.

\[ \exists \textit{ps} \in s. \exists p. (\textrm{hd}\,\textit{ps}, p) \in R \land p \in \textit{ps} \]

hd ps はリスト ps の先頭の要素です.つまりパスの最後のノードということです.ここから接続をたどって行けるノード p の中で,すでにパスに出現しているノードがあれば循環しているということです.最後のところではリストと集合を同一視してます.

この判定を行う手続きがあると考えて,ループの条件として使います.ループはこの条件が成り立たない間実行するので,否定を使うことになります.

次にループのステップでは,同じように考えてパスを伸ばします.接続先は複数あり得るので,1つのパスから複数のパスが生成されることになります.そこで,与えられたパスを1つ伸ばしたパスの集合を求める関数 extend があるものとします.次のように定義することができます.

definition
  extend :: "('a * 'a)set =>'a list => 'a list set"
where
  "extend R ps = {qs. EX p. (hd ps, p) : R & qs = p#ps}"

もし接続先がなければ空集合になります.p#ps は cons を意味します.

以上の2つを使うと,次のようにプログラムを書くことができます.

theorem
  "VARS s
  {True}
  s := {[s0]};
  WHILE s ~= {} &
        (ALL ps:s. ALL p. (hd ps, p) : R --> p ~: set ps)
  INV {ループ不変条件}
  DO
    s := Union ((extend R) ` s)
  OD
  {s ~= {} -->
    (EX p ps. ps:s & ps ~= [] &
        (hd ps, p) : R &
        p : set ps &
        ps ! (length ps - 1) = s0 &
        (ALL i. i < length ps - 1
           --> (ps ! (i + 1), ps ! i) : R))}"

ループ本体で使っている Union は名前のとおり和集合です.関数 extend の結果は集合なので,それらをすべて合わせるということです.バックスラッシュは関数の像です.結局,次の意味になります.

\[ s\ :=\ \bigcup \{\textrm{extend}\,R\,\textit{ps}\,|\,\textit{ps} \in s \} \]

ループ条件では先ほどの条件の否定と,あと s ~= {} があります.これは循環がなかった場合の条件です.

事後条件はちょっと複雑ですが,1つ1つ見れば明らかだと思います.前半はループ条件の否定で,最後に追加したノードがすでにパスにあるという条件です.次はパスの先頭,つまりリストの末尾のノードが初期ノードであることをいっています.最後の全称限量は,パスに含まれている隣り合わせのノードはすべて接続されているという条件です.もし s が空集合でなければ,以上の条件を満たすパスが s に含まれているということです.これが求めるものでした.存在限量がついていますけど,ループ条件と同じように,条件を満たすパスは s から取り出せると考えておきます.

ループ不変条件

ループ不変条件は事後条件をにらんで求めます.ここでは素直に,事後条件からループ条件(の否定)を除いた残りをループ不変条件とすればうまくいきます.

ALL ps:s. ps ~= [] & ps ! (length ps - 1) = s0 &
  (ALL i. i < length ps - 1 --> (ps ! (i + 1), ps ! i) : R)

正当性証明

正当性を証明します.すべて自動というわけにはいきませんが,一本道です.

theorem
  "VARS s
  {True}
  s := {[s0]};
  WHILE s ~= {} &
        (ALL ps:s. ALL p. (hd ps, p) : R --> p ~: set ps)
  INV {
    (ALL ps:s. ps ~= [] & ps ! (length ps - 1) = s0 &
       (ALL i. i < length ps - 1
                --> (ps ! (i + 1), ps ! i) : R))
  }
  DO
    s := Union ((extend R) ` s)
  OD
  {s ~= {} -->
    (EX p ps. ps:s & ps ~= [] & (hd ps, p) : R &
            p : set ps &
            ps ! (length ps - 1) = s0 &
            (ALL i. i < length ps - 1
                 --> (ps ! (i + 1), ps ! i) : R))}"

apply(vcg)
(* precondition *)
apply(clarsimp)
(* postcondition *)
defer
apply(clarsimp)
apply(rule_tac x="p" in exI)
apply(rule_tac x="ps" in exI)
apply(clarsimp)
(* loop invariant *)
apply(clarsimp)
apply(unfold extend_def)
apply(clarsimp)
apply(rename_tac s ps p i)
apply(drule_tac x="ps" in bspec)
apply(clarsimp)
apply(clarsimp)
apply(case_tac i)
apply(clarsimp)
apply(case_tac ps)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
done

閉包を使った条件の導出

閉包を使った到達可能な循環が存在する条件を,事後条件から導けることを証明しておきます.事後条件で十分という方は飛ばしてください.

まず補題を2つ証明します.

1つ目は,パスの中で隣り合わせになっているノードが接続しているならば,パスの中の任意の2つは推移的閉包に含まれているという補題です.パスの長さに関する帰納法を使うと証明できます.

lemma x1 [rule_format]:
  "length xs >= 2 &
    (ALL k<length xs - 1. (xs!(k+1), xs!k):R)
    --> (ALL i j. i < j & j < length xs
                   --> (xs!j, xs!i) : R^+)"
apply(induct_tac xs)
apply(auto)
apply(erule contrapos_np)
apply(subgoal_tac "length list = 1")
apply(subgoal_tac "i = 0 & j = 1")
apply(drule_tac x="0" in spec)
apply(clarsimp)
apply(erule r_into_trancl)
apply(clarsimp)
apply(clarsimp)
apply(drule_tac x="k+1" in spec)
apply(clarsimp)
apply(drule_tac x="i" in spec)
apply(drule mp)
apply(clarsimp)
apply(case_tac "i = j - 1")
apply(clarsimp)
apply(erule r_into_trancl)
apply(drule_tac x="i" in spec)
apply(drule_tac x="j - 1" in spec)
apply(drule mp)
apply(arith)
by (metis One_nat_def trancl.trancl_into_trancl)

2番目は循環があった場合に使うもので,リストに含まれている要素には対応するインデックスがあるというあたりまえの事実を述べたものです.存在限量を外して,具体的なインデックスを求めるために使います.

lemma x2 [rule_format]:
  "x : set xs --> (EX k < length xs. x = xs ! k)"
apply(induct_tac xs)
apply(auto)
done

以上の2つの補題を使うと,事後条件から循環の条件を導出することができます.

theorem
  "EX p ps. ps ~= [] &
       (hd ps, p) : R & p : set ps &
       ps ! (length ps - 1) = s0 &
       (ALL i. i < length ps - 1
           --> (ps ! (i + 1), ps ! i) : R)
  ==>
  EX p. (s0, p) : R^* & (p, p) : R^+"
apply(auto)
apply(rule_tac x="p" in exI)
apply(auto)
apply(subgoal_tac "(ps ! (length ps - 1), hd ps) : R^*")
apply (metis One_nat_def rtrancl.simps)
apply(subgoal_tac "hd ps = ps ! 0")
apply(clarsimp)
apply(case_tac "length ps >= 2")
apply(rule trancl_into_rtrancl)
apply(rule x1)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(case_tac ps)
apply(clarsimp)
apply(clarsimp)

apply(subgoal_tac "EX k < length ps. p = ps ! k")
apply(clarify)
apply(subgoal_tac "(ps!k, ps!0) : R^*")
apply(subgoal_tac "hd ps = ps ! 0")
apply(clarsimp)
apply (metis rtrancl_into_trancl1)
apply(case_tac ps)
apply(clarsimp)
apply(clarsimp)
apply(case_tac "k=0")
apply(clarsimp)
apply(rule trancl_into_rtrancl)
apply(rule x1)
apply(clarsimp)
apply(clarsimp)
apply(erule x2)
done

補足

グラフ探索の場合はフロントをリストにすることで,より具体的なコードに簡単に変換することができました.しかし循環検出の場合は,extend の結果が集合になるので,ちょっと複雑になります.フロントからノードを1つ選んで調べるとき,接続先が複数あり得るので,それらが新しいフロントになります.そのため元のフロントの残りを保留にして記録しておくスタック(あるいは再帰)が必要になるでしょう.ループ不変条件はかなり複雑になり,検証も相当面倒なことになります.

フロントをリストにして1つずつ調べる場合,実際にパスを作るのは1度に1つだけで済みます.さらに循環に含まれていないとわかったノードを記録しておくと,より効率的に調べることができます.実は上のプログラムには問題があって,複数のパスが同じノードに達した場合でもすべて調べています. これを避けるように修正することはできますが,必ずしも効率がよくなるわけではないと思われます.グラフが木に近くて重複がほとんど起こらない場合もあるでしょうし,並列実行の場合は同一ノードの検出コストの方が高いかもしれません.もともと効率がどうこういうレベルではないですけど.

停止性については直観的にわかるといえるレベルではないように思いました.でも実質的にこのアルゴリズムはの関係 R の閉包 R^* の一部(初期ノードから到達可能な部分)を求めているわけですから,R が有限ならば止まるでしょう.R^* も有限だからです.ループの実行回数は,R の要素数の関数で上から押さえることができると思われます.

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