Coqで、クイックソート
(* 注意:今回はCoq 8.1以上を使用。 *)
今回は、らくがきえんじんで、昔 言及されていた、クイックソートに挑戦してみる。
Coqで、再帰する関数を書く場合は、Definitionコマンドではなく、Fixpointコマンドを使う。
しかし、Fixpointによる関数定義では、明らかに停止する構造を持つ必要がある。
Coqでは、必ず停止する関数のみが定義できる、という制限のため、このように再帰する関数を定義するのは難しいが、Coqで作った関数は、必ず停止して結果を返す、という性質を保っている。
しかし、Fixpointによる定義では、簡単に定義できない再帰関数もある。
例えば、次のように、クイックソートの関数を素直にかいてみると、以下のようなエラーになる。
(* クイックソートの定義 失敗例 *) Fixpoint qsort (l : list A) : list A := match l with | nil => nil | x :: xs => qsort (filter (A_gtb compare x) xs) ++ (x :: qsort (filter (A_leb compare x) xs)) end. (* (::) はcons, (++) はappend *)
↓
Recursive definition of qsort is ill-formed.
In environment
qsort : list A -> list A
l : list A
x : A
xs : list A
Recursive call to qsort has principal argument equal to
"filter (A_gtb compare x) xs"
instead of xs
このqsort関数は、関数の定義内で、自分自身qsortを呼び出す、再帰関数であるが、その再帰呼び出しで、(filterごにょごにょ)が、与えられており、この関数が停止するかどうか、構造的には、明らかでない形になっている。
このため、Coqからは、qsortの再帰定義が正しくない形だよ。と言われてエラーになってしまう。
この場合は、 Listのfilter関数の結果は、必ず、長さが大きくならないので、停止するはずである。
このような関数を簡単に定義する方法が、Coqの8.1から導入された。それはFunctionコマンドとmeasureキーワードである。
このコマンドによって、停止するかどうかが、簡単にはわからない再帰関数を手軽に書き表すことができ、そのあと、停止性をtacticsを使って証明することができる。
先ほどのコードにおける、Fixpoint を Function にして、measureキーワードをつけたせば、エラーにならずに、停止性の証明モードに推移する。ここでは、measureとして、listの長さを測るlength関数を指定する。
(* クイックソートの定義 成功例 *) Function qsort (l : list A) {measure length l} : list A := match l with | nil => nil | x :: xs => qsort (filter (A_gtb compare x) xs) ++ (x :: qsort (filter (A_leb compare x) xs)) end.
↓
Coq < 2 subgoals A : Set compare : A -> A -> comparison ============================ forall (l : list A) (x : A) (xs : list A), l = x :: xs -> length (filter (A_leb compare x) xs) < length (x :: xs) subgoal 2 is: forall (l : list A) (x : A) (xs : list A), l = x :: xs -> length (filter (A_gtb compare x) xs) < length (x :: xs) qsort_tcc <
ここで、このゴールを証明すれば、停止性が保証され、関数定義が完了するといった具合だ。
証明が終了すると、次のような応答がかえってくるはずである。
Proof completed. qsort_tcc < Qed. qsort_ind is defined qsort_rec is defined qsort_rect is defined R_qsort_correct is defined R_qsort_complete is defined qsort is defined qsort_equation is defined qsort_terminate is defined qsort_tcc is defined
ぱっと見た感じ、qsort以外に、いろんなものが定義されている。これらは、qsortの性質を示すために便利な項達である。
今後、停止性以外の性質を証明しようと思ったら、ふつうのlistの構造に関する帰納法ではうまく行かないことが多い。
しかし、qsort_indを使うと、qsortの定義に従った帰納法によって、証明することができる。
ここでは、qsortしても、入力と出力の要素数が変わらないことと、順番は変わるけど、要素の内容は変わらないことを証明した。
以下が、ソースコードの全体である。
続きを読む