読者です 読者をやめる 読者になる 読者になる

にわとり小屋でのプログラミング ブログ

名古屋のCoqエンジニアです。日記は勘で書いてるところがあるので細かいとこが違うことがあります。

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

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

続きを読む