Coq でクイックソート (1) - チェシャ猫の消滅定理

以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。

アルゴリズムの定義 (この記事)
仕様の検証その 1
仕様の検証その 2

ちなみに、今回の分のコードは https://gist.github.com/4526374 に置いてあります。使い古されたネタではありますが、もしよろしければしばしお付き合いを。

おなじみのアルゴリズム

今更ですが、アルゴリズムの復習から始めましょう。深く考えずにクイックソートを書き下すと次のようになります。

Fixpoint qsort (l : list nat) : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

前も使いましたが、antifilter は、filter と逆の (つまり false になる要素の) 抽出を行う関数として定義してあります。ここで言えば、ピボット n に対して、lts として n より小さい要素、ges として n 以上の要素が抽出されるわけです。

しかしこのコードを読み込むと、

Error:
Recursive definition of qsort is ill-formed.

と怒られてしまいます。Coq には qsort の再帰呼び出しが有限回で停止することが理解できないからです。

そこで、リストの長さが短くなっていることを明示的に教えてやりましょう。Recdef モジュールをインポートしておいて、Function コマンドで定義します。

Function qsort (l : list nat) {measure length} : list nat :=
    match l with
    | nil     => nil
    | n :: l' => let lts := antifilter (leb n) l' in
                 let ges := filter (leb n) l' in
                 (qsort lts) ++ n :: (qsort ges)
    end.

これで怒られることはなくなりましたが、その代わりリストの長さが短くなることの証明が必要です。filter 関数の検証の際に使った補題が役に立ちそうですね。

Lemma filter_sublist : forall (f : A -> bool) (l : list A),
                       sublist (filter f l) l.

Lemma antifilter_sublist : forall (f : A -> bool) (l : list A),
                           sublist (antifilter f l) l.

Lemma sublist_length : forall l1 l2 : list A,
                       sublist l1 l2 ->
                       (l1 = l2 \/ length l1 < length l2).

ソートがソートであるために

上で定義した qsort に対して、仕様の検証を行うのが今回のネタの最終目的です。 wikipedia:ソートにも書いてある通り、ソート関数の仕様として次の性質を要求します。

出力は昇順になっている。
出力は入力の置換になっている。

準備がよいことに、これらの性質は標準ライブラリ Sorting モジュールに既に準備されています。こいつを使ってやりましょう。

Inductive Sorted (A : Type) (R : A -> A -> Prop) : list A -> Prop :=
    Sorted_nil : Sorted R nil
  | Sorted_cons : forall (a : A) (l : list A),
                  Sorted R l -> HdRel R a l -> Sorted R (a :: l)

Inductive Permutation (A : Type) : list A -> list A -> Prop :=
    perm_nil : Permutation nil nil
  | perm_skip : forall (x : A) (l l' : list A),
                Permutation l l' -> Permutation (x :: l) (x :: l')
  | perm_swap : forall (x y : A) (l : list A),
                Permutation (y :: x :: l) (x :: y :: l)
  | perm_trans : forall l l' l'' : list A,
                 Permutation l l' -> Permutation l' l'' -> Permutation l l''

ちなみに有名チュートリアルプログラミング Coq では整列性の定義として、Sorted ではなく LocallySorted の方を採用しています。補題 Sorted_LocallySorted_iff によってこれら二つの性質は同値なので問題は無いはずです。

その他補足

今回は nat 型のリストに対してしか定義していないのであまり関係がありませんが、ここで定義した qsort は安定ソートになっています。「Coq で filter 関数」でも「順序を維持したままマージしたもの」という表現が出てきましたね。その代わりと言ってはなんですが、常に左端の値をピボットとして取るため、入力が整列済みの場合に計算量は最悪 O(n^2) になります。

次回はまず仕様その 1 として qsort の出力が整列していることを証明する予定です。この証明では functional induction が威力を発揮するのですが、それはまた別の話。