Think Stitch
PRINCIPIA  最近の更新


並び替えの条件を表す2つの方法

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

比較と交換によるソートのアルゴリズムを検証する際には,すでにある値の交換だけを行っていて,勝手な値を書き込んでいないことを確認する必要があります.これを確かめるための条件について書いてみたいと思います.

並び替えの条件

簡単のために1つの配列上で処理を行うソートアルゴリズムを考えます.ソートのアルゴリズムがすでにある配列中の値を交換する操作だけでできているならば,ソートを行う前の段階で配列に含まれていた値の種類と数は,ソートした後でも変わらないはずです.同じ値が2個以上含まれている場合も考えに入れることにすると,同じ値が何個あるかというそれぞれの数も考える必要があります.

いいかえれば,ソート後の配列はソート前の配列の順列(permutation)の1つになっているということです.そこで,配列 ys が配列 xs の要素を並べ替えたものであるという述語を perm xs ys と書くことにすれば,ソートの仕様を次のように書くことができます.

theorem
  "VARS v その他の変数 ...
   {v = C}
   プログラム
   {perm v C &
    (ALL i j. i < j & j < length v --> v ! i <= v ! j)}"

文字 C はソート前の配列を表す変数です.様々な配列を代表するという意味では変数ですけれども,検証としては定数で,さらにプログラムの中から参照することはできません.このような変数のことを仕様変数といいます.ユニットテストを書いている人は,この仕様変数に対応する変数をプログラムの中でも用意して,実行前後の変化を確認するのに使っていると思います.

プログラムの実行後の配列はもちろん v です.この内容がプログラム実行前と比較したときに,値の種類と数において変わっていないという条件は perm v C と表すことができます.そこでこれを事後条件に入れておけば,勝手な値を書き込んでいないという証明になります.ループを使う場合には(使わないことはないでしょうけど)ループ不変条件にも同じ条件を入れておきます.そうすれば,ループの毎回のステップでも,ループから脱出した後も,条件が成り立つことが確認できます.

前回の選択ソートを例に,この条件を入れて検証してみます.

theorem
  "ALL (v::int list) i j. i < j & j <= length v -->
     i <= (selmin v i j) & (selmin v i j) < j &
     (ALL k. i <= k & k < j --> v ! (selmin v i j) <= v ! k)
  ==>
  VARS (v::int list) i j k
  {v = C}
  i := 0;
  WHILE i < length v
  INV {
    perm v C &
    i <= length v &
    (ALL p q. p < q & q < i --> v ! p <= v ! q) &
    (ALL p q. p < i & i <= q & q < length v --> v ! p <= v ! q)
  }
  DO
    k := selmin v i (length v);
    v := v[i := v ! k, k := v ! i];
    i := i + 1
  OD
  {perm v C &
   (ALL p q. p < q & q < length v --> v ! p <= v ! q)}"
apply(vcg)
apply(auto simp add: nth_list_update)

すると次のような証明課題が出てきます.長いので一部だけお見せします.

proof (prove): step 2

goal (6 subgoals):
 1. ALL v i j.
       i < j & j <= length v -->
       i <= selmin v i j &
       selmin v i j < j &
       (ALL k. i <= k & k < j --> v ! selmin v i j <= v ! k)
    ==> perm C C
 2. !!v i.
       [| ALL v i j.
             i < j & j <= length v -->
             i <= selmin v i j &
             selmin v i j < j &
             (ALL k. i <= k & k < j --> v ! selmin v i j <= v ! k);
          perm v C; ALL p q. p < q & q < i --> v ! p <= v ! q;
          ALL p q.
             p < i & i <= q & q < length v --> v ! p <= v ! q;
          i < length v |]
       ==> perm
            (v[i := v ! selmin v i (length v),
               selmin v i (length v) := v ! i])
            C

ポイントを抜き出すと,次の2つの条件を証明しなさいといっています.

1. perm C C
2. perm v C ==> perm (v[i := v ! m, m := v ! i]) C

前者は述語 perm が反射律を満たすことを示せといっています.これは事前条件からループ不変条件を導く過程で出てきます.後者はループのステップから出てくる条件です.2つのスロットの値を交換してもよい(同じスロットの場合もある)ということです.この2つの条件を定理として用意しておけば,ソートのより完全な証明を作ることができるわけです.

そこで,まず perm の定義を作って,それからこの2つの条件を証明することにします.ここでは異なる2つのアプローチによる2つの定義を調べてみようと思います.定理の証明も,ただ上の2つの条件を示すだけでなく,他でも使えるように数学的にスタンダードな性質を証明して使うことにします.

互換の関係と反射的推移的閉包を使う方法

1つ目は互換の関係と反射的推移的閉包を使う方法です.まず,任意の配列と,その値のうちの1組を入れ替えたものとをペアにした集合を考えます.つまり2つの要素を交換した配列のペアをすべて含む関係(数学でいう関係)を考えます.これを swap_rel と呼ぶことにします.Isabelle では次のように定義することができます.

definition swap_rel :: "('a list * 'a list) set" where
  "swap_rel = {(xs, ys).
                 EX i j. i < length ys & j < length ys &
                         xs = ys[i := ys ! j, j := ys ! i]}"

この関係の反射的推移的閉包を考えると,互換だけを繰り返してできるすべての配列のペアが含まれているはずです.これは望んでいるものそのものです.そこで,述語 perm を次のように定義することができます.(この定義は友達に教えてもらいました)

definition perm :: "'a list => 'a list => bool" where
  "perm xs ys == (xs, ys) : swap_rel^*"

この定義を使って,上の条件を証明します.まず反射律です.反射的閉包ですから自動でできます.

lemma perm_refl: "perm xs xs"
apply(unfold perm_def)
apply(auto)
done

次に推移律を証明します.推移的閉包ですから,これも自明です.

lemma perm_trans:
  "[| perm xs ys; perm ys zs |] ==> perm xs zs"
apply(unfold perm_def)
apply(auto)
done

つぎに互換に関する次の定理を証明します.これも自動でできます.

lemma perm_swap:
  "[| i < length v; j < length v |]
    ==> perm (v[i := v ! j, j := v ! i]) v"
apply(unfold perm_def swap_rel_def)
apply(auto)
done

以上を組み合わせると,正当性証明で必要な次の条件が証明できます.

lemma perm_inv:
  "[| perm v C; i < length v; j < length v |] 
  ==> perm (v[i := v ! j, j := v ! i]) C"
apply(erule perm_trans[rotated])
apply(erule perm_swap)
apply(auto)
done

多重集合を使う方法

2つ目は多重集合(multiset, bag)を使う方法です.言葉通り,値の種類と数を調べて比較しようというわけです.

Isabelle には多重集合という型はありませんが,関数を使うと簡単に定義できます.値に対して自然数(個数)を返す関数を多重集合だと見なせばよいのです.そこで,次のように型の名前を用意します.これは関数の型に別名をつけているだけです.

type_synonym 'a bag = "'a => nat"

例えば空の多重集合は,次のように常に 0 を返す関数として表すことができます.

definition the_empty_bag :: "'a bag" where
  "the_empty_bag x == 0"

ここでは配列(実際は Isabelle のリスト)を扱うので,配列を多重集合に変換する関数を用意します.(Isabelle では lambda を % で表します)

fun bag :: "'a list => 'a bag" where
  "bag [] = the_empty_bag" |
  "bag (x#xs) = insert_bag x (bag xs)"

fun insert_bag :: "'a => 'a bag => 'a bag" where
  "insert_bag elem bag =
      (%x. if x=elem then (bag x) + 1 else (bag x))"

すると,順列の述語 perm を次のように定義することができます.

fun perm :: "'a list => 'a list => bool" where
  "perm xs ys = (bag xs = bag ys)"

この perm は等号を使って定義されているので,反射律と推移律は自明です.

lemma perm_refl: "perm xs xs"
apply(auto)
done
lemma perm_trans:
  "[| perm xs ys; perm ys zs |] ==> perm xs zs"
apply(auto)
done

問題は互換の性質です.長いので結果だけ示します.

lemma bag_elem_0 [rule_format]:
  "ALL i. i < length v --> (bag v)(v ! i) > 0"
apply(induct_tac v)
apply(auto)
apply(case_tac i)
apply(auto)
done

lemma bag_elem_upd [rule_format]:
  "ALL x y i. i < length v -->
    bag (v[i := x]) y =
        (if x = y then (if v ! i = y then bag v y else bag v y + 1)
                  else (if v ! i = y then bag v y - 1 else bag v y))"
apply(induct_tac v)
apply(auto)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
apply(subgoal_tac "bag list (list ! nat) > 0")
apply(auto)
apply(rule bag_elem_0)
apply(simp)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
apply(case_tac i)
apply(auto)
done

lemma bag_swap_aux [rule_format]:
  "ALL i j. i < length v & j < length v
       --> bag (v[i := v ! j, j := v ! i]) = bag v"
apply(induct_tac v)
apply(auto)
apply(rule ext)
apply(case_tac i)
apply(auto)
apply(case_tac j)
apply(auto)
apply(auto simp add: bag_elem_upd)
apply(case_tac j)
apply(auto)
apply(auto simp add: bag_elem_upd)
apply(auto simp add: bag_elem_0)
apply(case_tac j)
apply(auto)
apply(auto simp add: bag_elem_upd)
apply(case_tac j)
apply(auto)
apply(auto simp add: bag_elem_upd)
apply(auto simp add: bag_elem_0)
done

lemma bag_swap:
  "[| i < length v; j < length v |]
   ==> bag (v[i := v ! j, j := v ! i]) = bag v"
apply(subst bag_swap_aux)
apply(auto)
done
lemma "[| i < length v; j < length v |]
  ==> perm (v[i := v ! j, j := v ! i]) v"
apply(clarsimp)
apply(erule bag_swap)
apply(auto)
done

まとめと補足

このように順列を使えば値を交換しているだけであることを確認できます.

どちらの定義が好みだったでしょうか.どちらの定義もちょっと飛び道具を使っている感じがあるので,もっとギャップを埋めるべきだと感じた方もいるかもしれません.

例えば次のようにもっと直接的な定義を書くこともできます.この定義は存在限量を外せばそのまま Prolog のプログラムとしても動くでしょう.ただ,これに基づいて証明をするのはかなりたいへんです.:P

fun perm :: "'a list => 'a list => bool" where
  "perm [] ys = (ys = [])" |
  "perm (x#xs) ys = (EX us vs. perm xs (us @ vs) &
                               ys=(us @ (x # vs)))"

もう1つ.この3つの定義は等価なのかということが気になるでしょう.興味がある方は証明に挑戦してみてはいかがでしょうか.

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