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しても、入力と出力の要素数が変わらないことと、順番は変わるけど、要素の内容は変わらないことを証明した。

以下が、ソースコードの全体である。

続きを読む