Think Stitch
PRINCIPIA  最近の更新


循環に対応した equal?

Scheme の equal? の話です。R6RS および R7RS ではデータ構造が循環している場合でも計算が停止することを要求されています。この場合の同値性は,循環部分を展開して無限の木として見たときに等しいかどうかで判断すると書いてあります。

この判定を効率よく実行する方法については Efficient Nondestructive Equality Checking for Trees and Graphs という論文に書いてあります。ここでは,効率は悪いけれどももっとかんたんなプログラムについて,正当性を証明してみたいと思います。ここでの主な関心は2つあります。1つは循環がある場合の同値性の定義,もう1つはループ不変条件は何かということです。

循環がある場合を含む同値性の定義 その1

個人的には,枝に順序がつけられた無限に大きな木が同じかどうかという基準は,とても自明なことには思えません。枝の数が有限なので少しはましだとは思いますけど。せめて比較対象を無限集合くらいにしてもらえると分かりやすいと思います。

そこで,枝にラベルをつけて,たどることのできる経路をラベルのリストで表すことにします。ペアの場合は car と cdr という2つのラベルがあります。ベクタの場合はインデックスの数字をラベルにすればいいでしょう。

空リストは葉だと考えます。ここで困るのはシンボルや数値などのアトムです。これらについては,その値そのものがラベルとしてついた唯一の枝を持つノードで表すことにします。接続先は枝のない葉だと考えます。

こうすると2つの木が同じかどうかという問題を,たどることのできる経路の集合が同じかどうかという問題に変換できます。有限列の無限集合と,無限列を含む集合とで基準が同じになるのかどうかちょっと怪しいところもありますが,見逃してください。

循環がある場合を含む同値性の定義 その2

これはラベル付き遷移システムでいうところのトレース集合と同じです。以前にトレース集合の同値性と双模倣の存在が同値であるという話をしました。したがってさらに双模倣を使った定義に置き換えることができます。

双模倣性の定義を復習します。まずラベル付き遷移システム(Labelled-Transition System, LTS)が遷移関係 M で与えられているとします.

\[ M \subseteq S \times E \times S \]

ここで S はノードの集合,E はラベルの集合です。

ノード間の関係 R

\[ R \subseteq S \times S \]

が双模倣(bisimulation)であるとは次の条件が成り立つことです。

\begin{align} & \forall p, q, e. (p, q) \in R \Rightarrow \\ &\qquad (\forall p'. (p, e, p') \in M \Rightarrow (\exists q'. (q, e, q') \in M \land (p', q') : R)) \land \\ &\qquad (\forall q'. (q, e, q') \in M \Rightarrow (\exists p'. (p, e, p') \in M \land (p', q') : R)) \end{align}

平たくいえば,2つの循環グラフのノードに対応関係をつけることができるということです。むしろ最初からこのように定義してくれる方がわかりやすいと個人的には思います。計算機の中ではどうせ有限のノードしか扱わないわけだし,その場合は双模倣も有限になるので,無限と関わらなくてもよいからです。

先に上げた論文でも,双模倣という言葉こそ出てきませんが基本的には同じアプローチをとっています。実際にはさらに考えを進めて,対応するノードの同値類を考えることで,より効率的な判定を行うようにしているようです(たぶん)。

ここでは単純に対応するノードを集めて,実際に双模倣を作るという戦略でプログラムを書いてみます。

equal? アルゴリズム

先にコードを示します。

lemma "VARS x y p s r b
  {x = X & y = Y}
  b := True;
  r := {};
  s := {(x, y)};
  WHILE s ~= {} & b
  INV {INVARIANT}
  DO
    p := (SOME x. x : s);
    s := s - {p};
    x := fst p;
    y := snd p;
    IF (x, y) : r THEN
      SKIP
    ELSE
      IF {a. EX x'. (x, a, x') : M} = {a. EX y'. (y, a, y') : M} THEN
        r := r Un {(x, y)};
        s := s Un {(x', y'). EX a. (x, a, x') : M & (y, a, y') : M}
      ELSE
        b := False
      FI
    FI
  OD
  {b --> bisim r & (X, Y) : R}"

大文字で表された仕様変数 X と Y が比較する2つのノードを表しています。変数 r は作っている途中の双模倣で,ノードのペアの集合です。s はいわゆる探索のフロントで,まだ調べていないノードのペアの集合を保持しています。このアルゴリズムでは再帰を避けてループにしているので,s はスタックの代わりも兼ねています。

アルゴリズムは単純です。まず未処理のペア (x, y) を s から1つ任意に取り出します。これは (SOME x. x : s) で表されています。(SOME x. P x) は条件 P x を満たす x を表します。Hilbert の ε-operator というのだそうです。もしこのペアがすでに r に入っている場合は何もしません。そうでない場合は,x と y それぞれから出ている枝のラベルが完全に一致するかどうかを調べます。ここでは集合演算ができると考えて,一気に判定しています。もし一致しない場合は明らかに equal? ではないので,フラグ b を False にセットしてループを抜けます。一致する場合にはペアを r に移し,代わりに x, y それぞれから出ている対応する枝の行き先のペアをすべて s に追加します。典型的なグラフの探索です。

事後条件

事後条件はちょっと手抜きをして,ループを抜けてきたときに b が True だったら,いいかえると s が空集合になったら r が双模倣になっているとしました。

ループ不変条件

さて問題はループ不変条件です。なぜ問題かというと,s = {} のときに事後条件を含意するためには,r が双模倣の一部を形成するという形にしなければなりませんが,ちょっと思いつきません。s = {} ということから典型的なパターンが想像されるのですが...

双模倣の和集合は双模倣になるので,r を拡大した関係が双模倣になるという条件を考えて見たのですがうまくいきませんでした。そこで探索の基本に立ち返ってみました。探索とは何かを探しているというよりはむしろ,ある性質が成り立つ範囲を拡大する作業であるという考え方です。そこでピンときました。双模倣の条件を満たすことがはっきりした部分は r に移されていて,そこからはみ出した部分は s に入って処理を待っているわけです。わかった後に言葉で書くとあたりまえなんですけどね。

そこで次のような述語を用意します。

definition bisim ::
   "(state * state)set => (state * state)set => bool"
where
  "bisim r s =
    (ALL p q a. (p, q) : r -->
      (ALL p'. (p, a, p') : M -->
        (EX q'. (q, a, q'): M & ((p', q') : r | (p', q') : s))) &
      (ALL q'. (q, a, q') : M -->
        (EX p'. (p, a, p'): M & ((p', q') : r | (p', q') : s))))"

双模倣の定義と異なるのは,枝の先が r の代わりに s に入っていてもよいとしたところです。初期状態では r は空集合ですから明らかに成り立ちます。ループのステップでは,お互いに対応するラベルの枝があるものだけを r に移して,その枝の先を s に入れるので,やはり成り立ちそうです。最後は s が空集合になるので,双模倣の定義そのものになります。

これを使うとループ不変条件は次のようになります。事後条件も合わせて修正しました。

lemma "VARS x y p s r b
  {x = X & y = Y}
  b := True;
  r := {};
  s := {(x, y)};
  WHILE s ~= {} & b
  INV {b --> bisim r s & (X, Y) : r Un s}
  DO
    p := (SOME x. x : s);
    s := s - {p};
    x := fst p;
    y := snd p;
    IF (x, y) : r THEN
      SKIP
    ELSE
      IF {a. EX x'. (x, a, x') : M} = {a. EX y'. (y, a, y') : M} THEN
        r := r Un {(x, y)};
        s := s Un {(x', y'). EX a. (x, a, x') : M & (y, a, y') : M}
      ELSE
        b := False
      FI
    FI
  OD
  {b --> bisim r {} & (X, Y) : r}"

証明

説明なしで全体を示します。

theory Equal imports  "~~/src/HOL/Hoare/Hoare_Logic" begin

typedecl state
typedecl label
consts M :: "(state * label * state)set"

definition bisim :: "(state * state)set => (state * state)set => bool"
where
  "bisim r s = (ALL p q a. (p, q) : r -->
                 (ALL p'. (p, a, p') : M -->
                   (EX q'. (q, a, q'): M & ((p', q') : r | (p', q') : s))) &
                 (ALL q'. (q, a, q') : M -->
                   (EX p'. (p, a, p'): M & ((p', q') : r | (p', q') : s))))"

lemma x0:
  "[| s ~= {}; (SOME x. x : s) : r; bisim r s |]
       ==> bisim r (s - {SOME x. x : s})"
apply(unfold bisim_def)
apply(auto)
apply metis
apply metis
done

lemma x1 [rule_format]:
  "{a. EX x'. (x, a, x') : M} = {a. EX y'. (y, a, y') : M}
  ==>
  ALL a. (x, a, x') : M --> (EX y'. (y, a, y') : M)"
apply(auto)
done

lemma x2 [rule_format]:
  "{a. EX x'. (x, a, x') : M} = {a. EX y'. (y, a, y') : M}
  ==>
  ALL a. (y, a, y') : M --> (EX x'. (x, a, x') : M)"
apply(auto)
done

lemma x3:
  "[| s ~= {};
          (SOME x. x : s) ~: r; bisim r s;
          {a. EX x'. (fst (SOME x. x : s), a, x') : M} =
          {a. EX y'. (snd (SOME x. x : s), a, y') : M} |]
       ==> bisim (insert (SOME x. x : s) r)
            (s - {SOME x. x : s} Un
             {(x', y').
              EX a. (fst (SOME x. x : s), a, x') : M &
                    (snd (SOME x. x : s), a, y') : M})"
apply(unfold bisim_def)
apply(auto)
apply (metis (mono_tags) fst_eqD snd_eqD x1)
apply(drule_tac x="fst (SOME x. x : s)" and y="snd (SOME x. x : s)" and a="a" and y'="q'" in x2)
apply (metis snd_conv)
apply(clarsimp)
apply (metis fst_conv snd_conv)
apply metis
by metis

lemma "VARS x y p s r b
  {x = X & y = Y}
  b := True;
  r := {};
  s := {(x, y)};
  WHILE s ~= {} & b
  INV {b --> bisim r s & (X, Y) : r Un s}
  DO
    p := (SOME x. x : s);
    s := s - {p};
    x := fst p;
    y := snd p;
    IF (x, y) : r THEN
      SKIP
    ELSE
      IF {a. EX x'. (x, a, x') : M} = {a. EX y'. (y, a, y') : M} THEN
        r := r Un {(x, y)};
        s := s Un {(x', y'). EX a. (x, a, x') : M & (y, a, y') : M}
      ELSE
        b := False
      FI
    FI
  OD
  {b --> bisim r {} & (X, Y) : r}"
apply(vcg)
apply(clarsimp)
apply(subst bisim_def)
apply(clarsimp)
defer
apply(clarsimp)
(**)
apply(rule conjI)
apply(clarsimp)
apply(rule conjI)
apply(rule x0)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
(**)
apply(clarsimp)
apply(rule conjI)
apply(rule x3)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
apply(clarsimp)
done

補足

Scheme の場合は1つのラベルにかならず1つの枝がありますけど,このプログラムでは複数の枝があってもかまわないようになっています。

双模倣はとても大きくなる場合があります。たとえば,すべての car 部が同じアトムを指している長さ N の循環リストと N + 1 の循環リストを比較する場合,双模倣は N(N + 1) 個のペアを持つことになります。これを避けるには,Union-Find を使って同値類に分ける必要があります。詳しくは先の論文を見てください(たぶん)。

「アトム」なんて言葉は久しぶりに(Winston & Horn 初版以来?)使いました。なんとなくちょっと懐かしいようなはずかしいような感じがしました。(^^;)

2014/01/25
© 2013,2014,2015 PRINCIPIA Limited