#はじめに
前回の記事で、全順序が仮定されているからこそうまくいくソートアルゴリズムを半順序で使用するとどうなるかを見ました。結果としてクイックソートなら半順序でもうまくソートできることを見ましたが、本記事では、これを定理証明支援系Coqを用いて、形式的に証明していきます。
定理証明支援系Coqに関して軽く説明しておくと、プログラムが正しく動くことを、数学的に検証できるツールとして使えるものです。
#クイックソートを定義
SSReflectのpathライブラリには、標準のソート関数sortが定義されていますが、このアルゴリズムはマージソートなので、前回の記事で検証したように半順序では使えません。
そこでCoqでクイックソートを定義します。
まず定義の前に、ソートを行う要素の集合Tと、半順序関係Rを宣言しておきます。実際にはTは型で、RはただのT上の二項関係T -> T -> boolとして定義しています。Rが半順序関係であることは証明する時に仮定します。
Section qsort.
Variable (T:Type).
Variable (R:Rel T).
クイックソートqsortを定義するためにFunctionコマンドを使います。
Function qsort (s:seq T) {measure size s} :=
if s is x :: s'
then qsort [seq y <- s' | R y x] ++ x :: qsort [seq y <- s' | ~~ R y x]
else [::].
Proof.
- move => _ x s _/=. apply /ltP. by rewrite ltnS size_filter count_size.
- move => _ x s _/=. apply /ltP. by rewrite ltnS size_filter count_size.
Defined.
ここで{measure size s}と記述するのは、qsortの停止性を保証するためです。
Coqでプログラムを定義するには、プログラムの停止性を保証しなくてはいけません。具体的には、メジャー関数と呼ばれる、以下のような性質を満たす関数を示してやる必要があります。
- プログラムの引数から自然数への関数であり、プログラムが再帰呼び出しされるたびに呼び出される関数の引数が狭義短調減少するもの。
今回、メジャーとして列の長さを返す関数sizeを与えています。Proof以降では、この関数の再帰呼び出しを行った際の引数がこのメジャーで狭義減少していることを証明しています。
##帰納原理
Functionコマンドで関数を定義すると、その関数の帰納原理など、定義した関数に関する基本的な定理も自動生成されます。しかし、今回定義したクイックソートの場合、自動生成される帰納原理qsort_indの使い勝手が悪いです。
qsort_ind
: forall P : seq T -> seq T -> Prop,
(forall (s : seq T) (x : T) (s' : seq T),
s = x :: s' ->
P [seq y <- s' | R y x] (qsort [seq y <- s' | R y x]) ->
P [seq y <- s' | ~~ R y x] (qsort [seq y <- s' | ~~ R y x]) ->
P (x :: s')
(qsort [seq y <- s' | R y x] ++ x :: qsort [seq y <- s' | ~~ R y x])) ->
(forall s _x : seq T,
s = _x ->
match _x with
| [::] => True
| _ :: _ => False
end -> P _x [::]) -> forall s : seq T, P s (qsort s)
本当は以下のようなシンプルなもので十分です。
Lemma my_qsort_ind (P:seq T -> Prop) :
P [::] ->
(forall x s, P [seq y <- s | R y x] ->
P [seq y <- s | ~~ R y x] ->
P (x :: s)) ->
forall s, P s.
この補題の証明は[こちらの記事]
(https://qiita.com/nekonibox/items/8147291e9fd483e3d579)を参照してください。
クイックソートにおいて、引数が[::]の場合とそうでない場合で場合分けをするので、この帰納原理にもそれぞれの場合に対応した2つの仮定があります。
なぜ、自動生成された帰納原理よりシンプルに記述できるかというと、my_qsort_indはqsortが再帰呼び出しをする引数のみに着目した補題であり、その計算には触れていないからです。その証拠に、自動生成されたqsort_indの定義にはqsortが表れていますが、my_qsort_ind内にqsortは表れません。
関数の停止性を示すときにも、内部の計算には触れず、再帰呼び出しする引数のみに着目しますが、同様に帰納原理も引数だけに着目したもので十分です。
実際にmy_qsort_indを使用した証明を見ていきます。
###クイックソートに関する補題
後の半順序でのソートに関する証明に使う補題を示しておきます。
Lemma all_qsort p s : all p (qsort s) = all p s.
Proof.
elim /my_qsort_ind : s =>[|x s]//=.
rewrite [qsort (_ :: _)]qsort_equation all_cat /==>->->.
case : (p x) =>/=; last exact : andbF. elim : s =>[|y s]//=.
case : ifP =>_/=<-; case : (p y)=>//=. exact : andbF.
Qed.
この補題はクイックソートしたリストqsort sの各要素でpが成り立つことと、元のリストsの各要素でpが成り立つことが同値であることを示しており、my_qsort_indを使った帰納法で示すことができます。
証明中にqsort_equationという補題が使われていますが、これはqsortを定義したときに自動生成される補題で、qsort sを定義式の右辺に書き換えるものになっています。
次に半順序におけるソートされている状態を定義します。
#半順序におけるソートされている状態とは
以下に定義するのが半順序に関するソートされている状態を表す述語になります。
Fixpoint mysorted (s:seq T) :=
if s is x :: s'
then all (fun y => ~~ R y x || R x y) s' && mysorted s'
else true.
~~ R y x || R x yはR y x ==> R x yの言い換えとなっており、前回の記事と同様の定義になっていることがわかります。
ここで名前がmysortedなのは、もともとpathライブラリに全順序におけるソートされた状態を表す述語sortedがあるからです。実際に、Rが全順序のときはmysortedとsortedは同値になります。
また、mysortedに関する補題を1つ示しておきます。
Lemma mysorted_cat s1 s2 :
mysorted s1 -> mysorted s2 ->
all (fun x => all (fun y => ~~ R y x || R x y) s2) s1 ->
mysorted (s1 ++ s2).
Proof.
elim : s1 =>[|x s1 IHs1]//=.
rewrite all_cat => /andP [->] Hs1 Hs2 /andP [->]/=. exact : IHs1.
Qed.
これは、リストs1、s2を結合したときにmysortedであることの十分条件を表しています。クイックソートでは再帰呼び出しを行った後に結合するので、この補題があると便利です。
#ソート可能であることの証明
ここからが本題です。まず半順序を仮定します。
Hypothesis (Htrans:transitive R).
あれ？と思うかも知れませんが、これでいいのです。
半順序は反射性、反対称性、推移性を満たす二項関係で定義されますが、ここでは推移性のみを仮定しています。
実はクイックソートでソート可能であることを示すには推移性だけしか使わないです。
実際の証明は以下の通りです。
Lemma qsort_sorted s : mysorted (qsort s).
Proof.
elim /my_qsort_ind : s =>[|x s IHs1 IHs2]//.
rewrite qsort_equation. apply : mysorted_cat =>//=.
- rewrite IHs2 andbT all_qsort.
by apply : (sub_all _ (filter_all _ _)) => y ->.
- rewrite all_qsort.
apply : (sub_all _ (filter_all _ _)) => y Hyx.
rewrite Hyx orbT all_qsort /=.
apply : (sub_all _ (filter_all _ _)) => z.
case Hzy : (R z y)=>//. by rewrite (Htrans Hzy Hyx).
Qed.
証明の流れとしては、まずmy_qsort_indを使い、qsortが再帰呼び出しする場合としない場合で場合分けをします。引数が[::]の場合は//ですぐ示せるので、引数がx :: sの場合だけを考えればいいです。
引数がx :: sの場合はmysorted (qsort [seq y <- s | R y x] ++ x :: qsort [seq y <- s | ~~ R y x])を示すわけですが、ここで先程示したmysorted_catを使います。
mysorted_catの1つ目と2つ目の仮定は帰納法の仮定からすぐわかるので、最後の仮定だけを示せばいいです。そこから先は流れで示せます。
#まとめ
クイックソートが半順序でもソートできることをCoq/SSReflectを使って形式的に証明しました。実は半順序を仮定しなくても、推移性を満たす任意の二項関係で成り立つことがわかりました。