推移律はいらない? ─比較ソートの正当性に必要な比較関数の性質─
この記事は Theorem Prover Advent Calendar 2013 最終日 (25日目)*1の記事です．
元々このネタは，
後学期の3年生向けの実験でCoqを教える際に提示した
「挿入ソートの正当性を示す」という最終課題の模範解答を作成する際に気づいたことです．
このため，ここで紹介するプログラムや証明は，
タクティクの種類やライブラリの利用が必要最低限に絞られているので，
もしかしたら Coq 初心者の方にも参考になるかもしれません
(各タクティクの作用を明確に理解してもらうため，敢えて auto も使いませんでした)．
Coq 上級者には冗長な証明が気になるかもしれませんが，その点は予めご了承ください．
はじめに
比較関数を利用して整列するアルゴリズムは比較ソートと呼ばれ，
クイックソートやマージソートをはじめとする多くの整列アルゴリズムがこれに属します
(逆に比較ソートでない整列アルゴリズムとしては，基数ソートやバケツソートなどがあります)．
比較関数は「2つの要素を引数を取り，真偽値 (true または false) を返す関数」として与えたり，
「2つの要素を引数を取り，比較値 (LessThan, EqualTo, GreaterThan) を返す関数」として与えたりしますが，
この記事では簡単のため前者を扱うことにします．
具体的には，ここでの比較関数は第1要素が第2要素より真に大きければ真，
第1要素が第2要素と等しいか小さければ偽を返すものとし，
比較ソートは入力を昇順に整列したものを出力することを想定しています．
比較ソートは，比較関数を入れ替えることで様々な指標で整列させることができるという反面，
与える比較関数が正しくないとそのアルゴリズムは意味を成しません．
例えば，どんな2つの要素を受け取っても必ず真を返すという関数を比較関数とすると，
どんな比較ソートでも正しく整列してくれません．
整列アルゴリズムは，整列する要素の順序関係が強全順序を成すことを前提としています((弱全順序を前提としてもかまいませんが，弱全順序を考えると反対称律を考慮する必要があり，要素の等価性の扱いなどの議論が面倒になるので，ここでは強全順序を仮定しています． 弱全順序を考える場合に同様の議論をすると，「反射律は不要であるが，「完全性 (cmp a b = true または cmp b a = true)」が必要になることになります．))．
つまり，比較関数 cmp が
- (1) [決定可能性] 全ての要素
a,bに対して，(cmp a b = true) ∨ (cmp a b = false) - (2) [非反射律] 全ての要素
aに対して，cmp a a = false - (3) [推移律] 全ての要素
a,b,cに対して，(cmp a b = true) ∧ (cmp b c = true)ならばcmp a c = true
- (4) [非対称律] 全ての要素
a,bに対して，cmp a b = trueならばcmp b a = false
Coqによる定式化
まずは簡単な準備から．
(* List ライブラリをインポート． 使うライブラリはこれだけ． *) Require Import List. (* 要素の型を A に固定． *) Parameter A : Set. (* 比較関数 cmp を宣言． 2つの要素を引数に取って真偽値を返すので，A -> A -> bool 型 ． *) Parameter cmp : A -> A -> bool.
Coq では，この cmp に関する宣言だけで (1) の決定可能性を仮定したことになります．
これは bool 型が帰納的に定義されているためで，実際に (1) を証明することも可能です．
(* cmp の決定可能性 *) Lemma cmp_dec : forall (x y:A), cmp x y = true \/ cmp x y = false. Proof. intros x y. destruct (cmp x y); [left|right]; reflexivity. Qed.
さらに，(4) に相当する cmp に関する非対称律を仮定します．
(* 非対称律を仮定 *) Parameter cmp_asym : forall (x y:A), cmp x y = true -> cmp y x = false.
(1) と (4) だけで正当性を証明すると言う目的のため，(2) と (3) は仮定しません．
さて，挿入ソートを定義しましょう．
まず，既に整列されているリストに要素を1つ挿入する関数 insert を定義してから，
挿入ソートを行う主たる関数 insertion_sort を実装します．
幸いにしてどちらもリスト上の単純な再帰関数で定義できるので，
整礎性の問題に苦しむこと無く簡単に定義することができます
(これは講義でこの問題を採用した大きな理由の一つです)．
cmp x y を x > y と読み替えて，
昇順に列べる整列をイメージすれば読みやすいと思います．
(* 1つの要素を挿入する関数 *) Fixpoint insert (x:A) (xs:list A) := match xs with | nil => x :: nil | y :: ys => if cmp x y then y :: insert x ys else x :: y :: ys end. (* 挿入ソート関数 *) Fixpoint insertion_sort (xs:list A) : list A := match xs with | nil => nil | y :: ys => insert y (insertion_sort ys) end.
さらに，整列アルゴリズムが正しいことを示す性質を定義しておきましょう．
まず，順序よく列んでいることを表す述語 Sorted を定義します．
(* Sorted xs := リスト xs が昇順に整列されている *) Inductive Sorted : list A -> Prop := | Sorted_nil : Sorted nil | Sorted_singleton : forall x:A, Sorted (x :: nil) | Sorted_conscons : forall (x y:A) (xs:list A), cmp x y = false -> Sorted (y :: xs) -> Sorted (x :: y :: xs).
ここでも，cmp x y を x > y と読み替える，すなわち
cmp x y=false を x ≦ y と読み替えれば理解しやすいでしょう．
整列アルゴリズムが正しいことを示すためには，Sorted だけでは不十分です．
たとえば，どんなリストが入力されても空リストを返す関数を考えると，
この関数は常に整列されたリストを返しますが，正しく整列したとは言えません．
出力されたリストが入力されたリストの並べ替えであるということを示す必要があります．
そこで，2つのリストが互いに並べ替えであることを表す述語 Permutation を定義します
(同等のものが Coq の Sorting ライブラリにもあります)．
(* Permutation xs1 xs2 := 2つのリスト xs1 と xs2 が互いに並べ替えの関係である *) Inductive Permutation : list A -> list A -> Prop := | Perm_nil : Permutation nil nil | Perm_skip : forall (x:A) (xs ys:list A), Permutation xs ys -> Permutation (x :: xs) (x :: ys) | Perm_swap : forall (x y:A) (xs:list A), Permutation (x :: y :: xs) (y :: x :: xs) | Perm_trans : forall (xs ys zs:list A), Permutation xs ys -> Permutation ys zs -> Permutation xs zs.
これで準備が完了です．
挿入ソートの正当性の証明
ここからが証明のお話です． まず，証明したい定理を先に見ておきましょう．
(* insertion_sort の正当性 *) Theorem insertion_sort_correctness : forall xs:list A, Sorted (insertion_sort xs) /\ Permutation xs (insertion_sort xs).
任意のリストに対して，insertion_sort は Sorted なリストを返し，
元のリストと Permutation の関係になっていることを表しています．
まず，補助関数である insert について，
Sorted に関わる性質を証明します．
(* 整列されているリストであればどんな要素を挿入しても整列される *) Lemma insert_sorted : forall (x:A) (xs:list A), Sorted xs -> Sorted (insert x xs). Proof. intros x xs Hxs. induction Hxs. (* Sorted_nil *) constructor. (* Sorted_singleton *) simpl. destruct (cmp_dec x x0) as [Hcmp1|Hcmp1]; rewrite Hcmp1. (* cmp x x0 = true *) apply cmp_asym in Hcmp1. constructor; [assumption|constructor]. (* cmp x x0 = false *) constructor; [assumption|constructor]. (* Sorted_conscons *) simpl in *. destruct (cmp_dec x x0) as [Hcmp1|Hcmp1]; rewrite Hcmp1. (* cmp x x0 = true *) apply cmp_asym in Hcmp1. destruct (cmp_dec x y) as [Hcmp2|Hcmp2]; rewrite Hcmp2 in *. (* cmp x y = true *) constructor; assumption. (* cmp x y = false *) constructor; [|constructor]; assumption. (* cmp x x0 = false *) constructor; [|constructor]; assumption. Qed.
また，Permutation に関わる性質を証明します．
(* 先頭に要素を追加したものと insert関数により要素を挿入したものは並べ替えの関係になっている *) Lemma insert_perm : forall (x:A) (xs:list A), Permutation (x :: xs) (insert x xs). Proof. intros x xs; induction xs; simpl. (* nil *) constructor; constructor. (* cons *) destruct (cmp_dec x a) as [Hcmp1|Hcmp1]; rewrite Hcmp1 in *. (* cmp x a = true *) apply Perm_trans with (a :: x :: xs); [constructor|constructor;assumption]. (* cmp x a = false *) clear. constructor; constructor. induction xs. (* nil *) constructor. (* cons *) constructor; assumption. Qed.
これらの insert 関数の性質を使えば，
insertion_sort も簡単な帰納法で証明することができます．
(* 挿入ソートの正当性 *) Theorem insertion_sort_correctness : forall xs:list A, Sorted (insertion_sort xs) /\ Permutation xs (insertion_sort xs). Proof. induction xs. (* nil *) simpl; split; constructor. (* cons *) simpl; split; destruct IHxs. (* Sorted *) apply insert_sorted, H. (* Permutation *) apply Perm_trans with (a :: insertion_sort xs). constructor; assumption. apply insert_perm. Qed.
これで証明が終わりです． 着目してほしいのは， 「挿入ソートの正当性を示すこの証明に使われている仮定は (1) と (4) だけで， (2) と (3) は仮定していない」という点です． このことから，比較関数に必要な性質として (3) の推移律はいらないのではないかという疑いが生じます． しかし，推移律が成り立たないじゃんけんのような3者関係があれば整列できないことは明らかです． それでは，比較関数が推移律を満たすことを仮定せずに挿入ソートの正当性が証明できてしまったことは何を意味しているのでしょうか．
種明かし
ここで，種明かしです．
「比較関数は推移律を満たさなくてもよい」と結論付けるには2つの問題があります．
1つめの問題は，隣り合った要素が順序通り列んでいればよいという Soreted の定義に関連します．
「(2) と (3) は一切使っていない」というのは真実ですが，これは Sorted の定義に強く依存します．
ここで使った定義は Coq の Sorting ライブラリにおける LocallySorted に相当していて，
隣り合った要素だけを見て整列しているかどうかを判定していますが，
「整列されている」という述語の定義は他にも考えられます．
たとえば，リストのどの2つの要素も順序通り列んでいるという定義
(Sorting ライブラリの StronglySorted に相当するもの)
を考えてみましょう．
(* CmpAll x ys := リスト ys のどの要素 y に対しても cmp x y = false (x≦y) が成り立つ． *) Inductive CmpAll : A -> list A -> Prop := | CmpAll_nil : forall x:A, CmpAll x nil | CmpAll_cons : forall (x y:A) (ys:list A), cmp x y = false -> CmpAll x ys -> CmpAll x (y::ys). (* StronglySorted xs := リスト xs のどの2つの要素についても x が y より前に現れるなら cmp x y = false が成り立つ． *) Inductive StronglySorted : list A -> Prop := | StronglySorted_nil : StronglySorted nil | StronglySorted_cons : forall (x:A) (xs:list A), CmpAll x xs -> StronglySorted xs -> StronglySorted (x :: xs).
どんなリスト xs に対しても，明らかに StronglySorted xs ならば Sorted xs が導けますが，
逆は成り立ちません．
逆を示すためには，(3) に似た否定推移律 (3)' が必要になります*2．
- (3)' [否定推移律] 全ての要素
a,b,cに対して，(cmp a b = false) ∧ (cmp b c = false)ならばcmp a c = false
StronglySorted を選んでしまうと，
挿入ソートの正当性を示すためには (3)' が必要になってしまいます．
つまり，「隣り合った要素の順序しか確認しなくてよい」という定義をした時点で，推移律の仮定を使っているわけです．2つめの問題も Sorted の定義に関連することですが，
「比較関数が推移律を満たすことを確認しなくてよい」と結論づけてはいけないことを示すより根本的な問題です．
比較関数 cmp そのものを Sorted の定義の一部に使ってしまっては，
比較関数の正しさに関して何も論じられないのです．
たとえば，S, T, U の
3種類しかないデータを要素とするリストの整列を考えてみましょう．
比較関数 cmp の定義を
Definition cmp (x y:A) := match (x, y) with | (S, T) => true | (T, U) => true | (_, _) => false end.とすると，この定義は (4) を満たしますが，(3) や (3)' は満たしません． この比較関数を基準に整列すると，
S::U::T::nil は U::T::S::nil や T::S::U::nil や S::U::T::nil になり得ますが，
S::T::nil は T::S::nil にしかなりません．
つまり，U があるかないかで順序が変わってしまうような妙な結果が得られます．
非対称律が成り立っていても，推移律が成り立っていなければ整列として意味をなさないのです．おわりに
結果的には「比較関数は推移律を満たさなくてもよい」というのは正しくありませんでしたが，
整列するアルゴリズムの正当性を示すには比較関数の推移律を必要としないというのは面白い結果ではないでしょうか．
実際，クイックソートやマージソートなどの別の比較ソートのアルゴリズムの場合も (4) だけで正当性が証明できます．
今回は，挿入ソート・クイックソート・マージソートについてしか確認していませんが，
上述のような Sorted の定義を考えている限り，推移律は必要にはならないような気がします．
では，比較関数の推移律を仮定しないと正当性が示せないような比較ソートアルゴリズムが存在しないことは証明できるでしょうか．
これは，あまり簡単ではないかもしれませんね．
