NGK2014B で SPIN について話してきました
名古屋工業大学で行われた LT 大会 NGK2014B で発表しました。
内容はタイトルそのままで、モデル検査ツール SPIN とその記述言語である Promela の特徴を概観する、というものです。
当日の動画は Youtube から見ることができます。
ちなみに、発表順は乱数で決められているはずなのですが、なぜか去年の NGK と全く同じ 3 番目でした。
リソース共有問題の Promela モデル
LT の冒頭に登場するリソース共有時のデッドロックについて、Promela で記述したモデルが Gist においてあります。
この Promela モデルは、次のようなシステムを想定したものです。
- クライアント
- スキャナもしくはプリンタのどちらかをロックし、その後もう片方をロック
- スキャナもしくはプリンタのどちらかをアンロックし、その後もう片方をアンロック
- リソース (スキャナ、プリンタ)
- ロックするメッセージを待ち、相手のプロセス ID を記憶
- アンロックするメッセージを待ち、相手のプロセス ID とロックしたプロセスを照合
- ロックとアンロックが同じプロセスからのものならば最初に戻る
すぐわかる通り (LT 内でも述べていますが) このシステムには欠陥があり、デッドロックが発生します。スキャナとプリンタにロックを掛ける順番が指定されていない (そして Promela がそういう非決定的な記述を許す) というところがポイントです。
いずれこのモデルを題材にして Promela/SPIN の入門記事でも書くつもりではありますが、それはまた別の話。
Coq で Quine
Coq で自己出力プログラム、いわゆる Quine を作成してみました。全体の流れとしては情報処理学会の連載「自分自身を出力するプログラム」の Haskell 版を参考にしてあります。今回のコードは短いので記事の最後に全体を載せてありますが、一応いつものごとく Gist 上 https://gist.github.com/4700318 にも同じものを置いておきました。
Coq の特性あれこれ
Quine なるものを初めて聞いた人は wikipedia:クワイン_(プログラミング) あたりを見てみましょう。「自分自身のソースコードを標準出力する。ただし空ファイルでなく、入力は受け付けない」というのが一般的な Quine のお作法ですが、Coq で書くにはいくつか考えねばならない点があります。
標準出力……。
最大の問題として、Coq 単体では出力ができません。純粋すぎる相手というのは得てして扱いにくいものです。悩んでどうにかなる問題でもないので、コードの最後を Eval compute in として、ここが評価されたときにコード全体と同じ文字列になることを目指しました。
文字列の扱い
大部分の言語と違い、Coq は文字列を扱うのにいちいちライブラリを読み込む必要があります。使うライブラリは Ascii と String。
ascii 型の方はコンストラクタの引数に bool を 8 個取って、8 ビット ASCII コードとして読むものです。
Inductive ascii : Set :=
Ascii : bool ->
bool -> bool -> bool -> bool -> bool -> bool -> bool -> asciiちなみに実験してみるとわかりますが、引数の順番は下位ビットが先です。
Eval compute in Ascii true false false false
false false true false.
= "A"%char
: asciiまた、string 型の方はリストと同じ構造を持っています。
Inductive string : Set :=
EmptyString : string | String : ascii -> string -> stringEmptyString が nil、String が cons 相当のコンストラクタですね。string_scope を開いておくと文字列の結合 append が + でシュガーされるので、見やすくするためにこれを使いました。
クォーテーションの扱い
文字列のデリミタは " です。Quine を書く上で、文字列の中に " が出現するためエスケープを考える訳ですが、ここで若干問題が。どうも Coq では (少なくとも CoqIDE の表示上は) 記号 " を単体で表示させることができないようです。実際、ASCII コード 34 を評価すると
Eval compute in ascii_of_nat 34.
= """"%char
: asciiとなり、"" で一文字分 (つまり "" が " のエスケープ表現) となっていることがわかります。ここは若干不本意ですが、「表示文字列中の " と "" との差には目をつぶる」として逃げることにしましょう。
Quine の実装
以上のことを踏まえて具体的なコードを作っていきましょうか。
まず大まかな構造として、次のような形を考えます。
Definition Q : string := [空欄 A]. Eval compute in [空欄 A'].
この Eval compute in [空欄 A']. でコード自身が表示されればよいわけです。
ステップその 1
Definition と Eval の二つの文がある以上、[空欄 A'] はこの二つの文をつなげた文字列が入るはずです。そこで、次のような形になることがわかります。
Definition Q : string := [空欄 A]. Eval compute in [空欄 B] ++ "." ++ [空欄 C].
非形式的な言い方をすれば、[空欄 B] が「Q にしかるべき文字列を代入せよ」、[空欄 C] が「「このコードを表示せよ」を表示せよ」を表す部分です。
ステップその 2
次に、[空欄 C] について考えます。意味するところが「〜を表示せよ」なので Eval compute in を入れたいところですが、そうすると堂々巡りになってしまいそうですね。回避策として、前半で定義している Q を参照します。
Definition Q : string := [空欄 A]. Eval compute in [空欄 B] ++ "." ++ Q.
そうすると、Q は「〜を表示せよ」でなくてはならないため、Eval compute in で始まることがわかりました。
Definition Q : string := "Eval compute in [空欄 D]". Eval compute in [空欄 B] ++ "." ++ Q.
ステップその 3
次に埋めるべきは [空欄 B] です。ここには前半部に対応する「Q に 「Q の中身」を定義せよ」を意味するコード文字列が入るはずですね。「Q の中身」を文字列として表すのに、冒頭に挙げた参照文献では Q に対して Haskell の show を使っています。Coq に show はないので、手動でデリミタ " を付けましょう。文字列「Q の中身」は """" ++ Q ++ """" です。
Definition Q : string := "Eval compute in [空欄 D]". Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
ステップその 4
これでほとんど完成しました。後は [空欄 D] として、実際に Eval compute in の引数になっている「"Definition Q : string := " ++ """" ++ Q + """" ++ "." ++ Q.」をそのまま持ってきてエスケープすればオッケー。
Definition Q : string := "Eval compute in ""Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.". Eval compute in "Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
完成！
ライブラリの読み込みなどを追加し、また見やすくなるように適宜改行を入れたりした完成品が以下になります。はてなブログのベタ打ちだと若干見づらいですが、Gist の方を見てもらうと地の文と文字列との境目が分かりやすいかと。
Require Import Ascii String. Open Scope string_scope. Definition Q : string := " Eval compute in "" Require Import Ascii String. Open Scope string_scope. Definition Q : string := "" ++ """" ++ Q ++ """" ++ ""."" ++ Q.". Eval compute in " Require Import Ascii String. Open Scope string_scope. Definition Q : string := " ++ """" ++ Q ++ """" ++ "." ++ Q.
その他補足
ここで書いた Quine は当然ですが最短ではありません。改行が無駄ですし、型宣言も省略できます。あるいは、今回は構成手順に重きを置いたためこの形になりましたが、もしかしたらもっと本質的にいい書き方があるかもしれません。しかしまあ、そもそも Coq は短く書くことに向いた言語ではありませんし、無理に追求はしないことにしましょう。なお、どうしても短い Quine が書きたい人は wikipedia:HQ9+ あるいは PHP の利用をおすすめします。
ちなみに今回は深入りはしませんが、「自分自身のコード」に言及する上でキモになっているのが [空欄 C] の中身「「このコードを表示せよ」を表示せよ」という部分です。こういう表現の背後には Kleene の再帰定理があり、またかの有名な不完全性定理の証明と関係があったりして面白い部分ではあるのですが、それはまた別の話。
Coq でクイックソート (3)
Coq でクイックソートの検証、三回目です。今回は最後に残った部分をちょろっとだけ埋めましょう。コードは前回、前々回に追記する形で、https://gist.github.com/4526374 に置いてありますのでよかったらご参照を。
今回の目標
今回は、最後に残った qsort の二つ目の仕様
- 出力が入力の置換 (並び替え) になっていること
を証明します。モジュール Sorting.Permutation を使いましょう。前回の Sorted に比べ、Permutation はリスト操作とそれなりに相性がよく、証明済みの定理も使えそうなヤツが揃っています。
述語 Permutation の中身
Permutation の定義は以下です。
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''特に複雑なところはないですね。要するに、空リストから始めて「同じ要素を先頭にくっつける」「先頭から二つを入れ替える」を有限回繰り返して得られるリストは互いに置換である、というわけです。
いざ、最後の証明
示したい定理を改めて掲げておきます。
Theorem qsort_Permutation : forall l : list nat,
Permutation (qsort l) l.証明に使うのは前回と同じく functional induction タクティク。さらに上手いことに、ライブラリを覗いてみるとこんなのがありました。
Permutation_cons_app
: forall (A : Type) (l l1 l2 : list A) (a : A),
Permutation l (l1 ++ l2) -> Permutation (a :: l) (l1 ++ a :: l2)qsort の定義が
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 の結果と antifilter の結果を append したものは、もとのリストの置換」という補題 filter_Permutation ですが、これにしたって単純な場合分けだけですぐに証明できてしまいます。
その他補足
さて、全三回に渡ってお送りしてきましたが、以上によりクイックソート qsort の仕様が証明されました。これで明日から安心してクイックソートが使えますね。めでたしめでたし。ちなみにこのナイーブな実装では遅すぎて実用性が皆無ですが、まあご愛嬌ということで。
今回の「置換であること」の定式化や証明には、この他にも方法が考えられるはずです。すぐに思いつくのは、「任意の要素に関して、二つのリストに含まれる個数が等しければ置換」というものでしょうか。形式的に書けば
Theorem Permutation_count : forall l1 l2 : list nat,
Permutation l1 l2 <->
(forall n : nat, count_occ eq_nat_dec l1 n =
count_occ eq_nat_dec l2 n).という感じでしょうかね。ただ、置換であることと述語 In とはあまり相性がよくありません。前回の補足でも述べた通り、In は重複した要素を区別することができないからです。リストが重複要素を含まないときのみ、In を使って Permutation を特徴づける補題 NoDup_Permutation も用意されていますが、使いどころは難しい気がします。
なお、ここに挙げた定理 Permutation_count はそう苦労せずに証明することができるのですが、それはまた別の話。
Coq でクイックソート (2)
Coq でクイックソートの検証、二回目です。コードは前回のものに追記する形で https://gist.github.com/4526374 に置いてあります。
今回の目標
さて、前回の最後にも触れた通り、前回定義したクイックソート qsort について、
- 出力が昇順になっていること
を保証することが第一の目標です。ここでは、標準ライブラリ Sorting モジュール内にある述語 Sorted を使うことにしました。Sorting.Sorted の中には、「リストが (ある関係 R に対して) 昇順である」ことを意味する述語が三種類用意されています (LocallySorted、Sorted、StronglySorted) が、これらはすべて同値です。
述語 Sorted の中身
Sorted の定義を見ると、次のようになっています。
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)ちなみに、ここで補助的に使われている HdRel の定義は以下です。
Inductive HdRel (A : Type) (R : A -> A -> Prop) (a : A) : list A -> Prop :=
HdRel_nil : HdRel R a nil
| HdRel_cons : forall (b : A) (l : list A), R a b -> HdRel R a (b :: l)自然言語で読み下せば、HdRel R a l は「a とリスト l の先頭要素との間に関係 R が成立」を意味しています。Head Relation の略でしょうね。これを考えると、Sorted は直感的には「既にソートされたリストに対して、現在の先頭要素以下のものを先頭に付け足してもソートされている」と定義されていることがわかります。
さて、ここまで来てちょっと困りました。というのも、qsort は再帰的に定義されていて、最終的な出力の先頭要素がどこから来ているのかわからないからです。こういうときに使えるのが functional induction タクティクです。
Functional Induction による証明
さて改めて確認しておくと、qsort の定義は以下でした。
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.もし人間が紙の上で「qsort の出力が昇順」を示したいとしたら、自然なのは「qsort lts とqsort ges が昇順だと仮定すると〜」というものでしょう。Coq に対してこれを伝えるタクティクが functional induction で、関数の再帰呼び出しに対して帰納法を適用することができます。実際に今回示したい定理
Theorem qsort_Sorted : forall l : list nat, Sorted le (qsort l).
に対して functional induction (qsort l) を打ち込んでみると、l = n :: l' の場合に使える仮定として「Sorted le (qsort (antifilter (leb n) l'))」および「Sorted le (qsort (filter (leb n) l'))」が追加されるはずです。
これができれば、それ以外はたいした問題はないはず。もちろん、二つの昇順リストを連結したときに結果が再び昇順になるためには、左側に小さい要素、右側に大きい要素が集まっている必要があるので、それさえ示しておけば大丈夫。定式化の方法はいろいろあると思いますが、ここでは次のような補題を使ってあります。
Lemma Sorted_app : forall (l1 l2 : list nat),
Sorted le l1 -> Sorted le l2 ->
(forall n1 n2 : nat,
In n1 l1 -> In n2 l2 -> n1 <= n2) ->
Sorted le (l1 ++ l2).
その他補足
さて、これで半分終わりました。次回は残りのもうひとつ、qsort の出力が入力の置換であることを証明する予定です。
ちなみに「置換である」という部分だけ見ると、今回補題として用いた
Lemma qsort_in : forall (l : list nat) (n : nat),
In n l <-> In n (qsort l).がそのまま使えそうな気がします。がしかし、この補題は置換であることを保証しません。というのも、述語 In は「リストの中に一個以上存在する」ことしか保証せず、ダブりを考慮できないからです。置換であるためには個数まで含めて一致する必要がありますからね。
とはいえ、ライブラリを見てもらえればわかる通り、Sorting.Permutation は今回の Sorting.Sorted よりも使えそうな補題が豊富です。次回はこいつらを活用する方針で行きたいと思いますが、それはまた別の話。
Coq でクイックソート (1)
以前の記事「Coq で filter 関数」の最後にちょっと触れた通り、Coq でクイックソートを扱ってみます。ひとつの記事にすると長くなりそうなので、全 3 回に分割してみました。
ちなみに、今回の分のコードは 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 が威力を発揮するのですが、それはまた別の話。
Coq で位相空間
前々回の記事「Coq でモジュラー束」で「群 G の部分群を述語 G -> Prop で表す」という方針を採用したところ、割と上手くいくということがわかりました。今回は他の題材として、「連結集合の連続写像による像は連結」であることを、同じ方針により証明してみます。大学の学部で習う定番問題ですね。証明付きの完全なコードは https://gist.github.com/4466805 です。
とりあえず概念を準備しよう
位相空間
「X の部分集合」の型をいちいち X -> Prop の形で書くと冗長になるため、シノニムを付けておきます。
Definition Subset (X : Set) : Type := X -> Prop.
また、開集合系の公理を記述するために必要な、X 自身、空集合、共通部分、和集合をそれぞれ定義しておきましょう。ここで、(X の) 空集合として
Definition empty (X : Set) : Subset X := fun (x : X) => x <> x.
としました。任意の x : X に対して ~ x <> x が成立することは、等号の反射性 eq_refl を用いて容易に示すことができます。また、開集合系の公理として「任意個の開集合の和集合」を表現する必要があるため、任意の添字付けに対する共通部分 bigcap と和集合 bigcup を先に定義しておき、2 個の場合 intsec と union はその特殊な場合として表しています。bigcap は今回は使い途がありませんでしたが。
以上を踏まえて、X が 位相 Open を備えた位相空間であることを、次のように表しました。
Class TopSpace (X : Set) (Open : Subset X -> Prop) := {
TS_whole :
Open (whole X);
TS_empty :
Open (empty X);
TS_intsec :
forall U1 U2 : Subset X,
Open U1 -> Open U2 ->
Open (intsec U1 U2);
TS_union :
forall (I : Set) (index : I -> Subset X),
(forall i : I, Open (index i)) ->
Open (bigcup I index)
}.
連続写像
逆像 preimage を用いて連続写像の定義を書きます。「任意の開集合の逆像が開なら連続」というやつですね。特に問題はなく、至って教科書通り。
Definition preimage {X Y : Set}
(f : X -> Y) (V : Subset Y) : Subset X :=
fun (x : X) => V (f x).
Class Continuous (X : Set) (XOpen : Subset X -> Prop)
(Y : Set) (YOpen : Subset Y -> Prop)
(f : X -> Y) := {
Conti_TopSpace_l :>
TopSpace X XOpen;
Conti_TopSpace_r :>
TopSpace Y YOpen;
Conti_preim :
forall V : Subset Y,
YOpen V -> XOpen (preimage f V)
}.
連結集合
さて、今回の主題である連結集合の定義です。
Class Connected (X : Set) (Open : Subset X -> Prop)
(S : Subset X) := {
Conn_TopSpace :>
TopSpace X Open;
Conn_insep :
forall U1 U2 : Subset X,
Open U1 -> Open U2 -> incl S (union U1 U2) ->
(exists x1 : X, (intsec S U1) x1) ->
(exists x2 : X, (intsec S U2) x2) ->
exists x : X, intsec S (intsec U1 U2) x
}.定義を書く上で、部分集合への所属を Prop で表現している関係上、否定 ~ の出現は避けたいところです。通常、連結空間の定義としては「S がふたつの (S の) 開集合の非交和として表せない」という言い回しが採用されることが多いですが、これを「S がふたつの開集合 U1 と U2 の和として表されればそれは非交和ではない」と表現することにして、さらに「共通部分が空でない」ことを「実際に元が存在する」として否定表現を回避してあります。
それから証明しよう
さて、本題の証明に入りましょう。(X, XOpen) と (Y, YOpen) を位相空間、f : X -> Y を連続写像とし、X の連結部分集合 U の像 f(U) の連結性を示します。
Variables X Y : Set. Variable XOpen : Subset X -> Prop. Variable YOpen : Subset Y -> Prop. Hypothesis X_TopSpace : TopSpace X XOpen. Hypothesis Y_TopSpace : TopSpace Y YOpen. Variable f : X -> Y. Hypothesis f_Continuous : Continuous X XOpen Y YOpen f. Variable U : Subset X. Hypothesis U_Connected : Connected X XOpen U. Instance image_Connected : Connected Y YOpen (image f U).
ちなみに証明の中身は、次のような感じ。なんと言うか、特にひねったところもないスタンダードな証明です。
- V1 と V2 を、f(U) を覆う Y の開集合とする。
- U の連結性から、U と f^{-1} (V1) と f^{-1} (V2) の共通部分は空でなく、ここから元 x が取れる。実際、
- f の連続性より f^{-1} (V1) と f^{-1} (V2) は開。
- f(U) が V1 と V2 の和集合に含まれることから、U は f^{-1} (V1) と f^{-1} (V2) の和集合に含まれる。
- f(U) と V1、V2 それぞれとの共通部分が空でないため、 U と f^{-1} (V1)、f^{-1} (V2) それぞれの共通部分も空でない。
- f(x) は f(U) と V1 と V2 の共通部分に属する。よってこの共通部分は空でない。
その他補足
今回の題材、本当は「コンパクト集合の連続写像による像はコンパクト」を証明しようかと思ったのですが、残念ながら上記の定式化では有限交叉性が上手く表現できません。FSet モジュール辺りが有望でしょうか。いずれこちらのネタもやってみたいものですが、それはまた別の話。
Coq で filter 関数
リストの要素の内、条件に合致するものだけを抜き出す関数 filter の仕様を Coq で証明してみました。元ネタは『ソフトウェアの基礎』の練習問題。完全なコードは https://gist.github.com/4401408 に置いてあります。
とりあえず定義の確認
List モジュールにある filter の定義を確認してみると、次のようになっています。
filter =
fun (A : Type) (f : A -> bool) =>
fix filter (l : list A) : list A :=
match l with
| nil => nil
| x :: l0 => if f x then x :: filter l0 else filter l0
end.要するにリストの要素を先頭から見ていって、条件 f が成り立つときだけ戻り値に反映させているわけです。実際、NPeano モジュールにある even : nat -> bool で試してみると、
Eval compute in filter even (2 :: 7 :: 3 :: 6 :: 1 :: nil). = 2 :: 6 :: nil : list nat
となり、確かに期待通りの動作をしていることがわかります。
さて、この filter 関数の仕様として、『ソフトウェアの基礎』では次の二種類が挙げられています。
集合 X と関数 test: X -> bool、リスト l とその型 list X を想定する。 さらに、l が二つのリスト l1 と l2 が順序を維持したままマージされたもので、 リスト l1 の要素はすべて test を満たし、 l2 の要素はすべて満たさないとすると、filter test l = l1 が成り立つ。
test の結果が true なる要素だけでできた、リスト l の すべての部分リストの中で、filter test l が最も長いリストである。
この二つを形式的に記述し、証明することを今回の目標としましょう。
なお、毎回 X と test を引数として書くのは面倒なので、これらは Variable であらかじめ宣言しておきます。
仕様の記述と filter 関数の検証
仕様その 1
一つ目の定式化から行きましょう。まず「l が二つのリスト l1 と l2 を順序を維持したままマージしたものである」ことの定義を帰納的に記述します。
Inductive merger : list X -> list X -> list X -> Prop :=
| Merger_nil_l : forall l : list X,
merger l nil l
| Merger_nil_r : forall l : list X,
merger l l nil
| Merger_cons_l : forall (x : X) (l l1 l2 : list X),
merger l l1 l2 ->
merger (x :: l) (x :: l1) l2
| Merger_cons_r : forall (x : X) (l l1 l2 : list X),
merger l l1 l2 ->
merger (x :: l) l1 (x :: l2).これですべてのパターンを網羅していることになるはず。さらにこれを用いて filter が満たすべき条件を記述します。
Theorem filter_challenge : forall l l1 l2 : list X,
let T := fun x => test x = true in
let F := fun x => test x = false in
merger l l1 l2 -> all T l1 -> all F l2 ->
filter test l = l1.all P l は「リスト l のすべての要素が P : Prop を満たす」を意味する述語です。この部分はbool 型のまま forallb を用いて扱う手もあったのですが、もう書いてしまったのでよしとしましょう。
証明そのものは特に難しいところはないです。上に挙げた証明は似たような部分が多いので、もしかすると順番を工夫すればもっと完結にまとまるかもしれませんね。
仕様その 2
さて、二つ目。いくつか補題を用意する関係上、こちらの方が分量としては長くなりました。まず「l1 は l2 の部分リストである」ことを定義しておきます。
Inductive sublist : list X -> list X -> Prop :=
| Sublist_nil : forall l : list X,
sublist nil l
| Sublist_cons1 : forall (x : X) (l1 l2 : list X),
sublist l1 l2 ->
sublist l1 (x :: l2)
| Sublist_cons2 : forall (x : X) (l1 l2 : list X),
sublist l1 l2 ->
sublist (x :: l1) (x :: l2).ちなみに書き終わった後で気がつきましたが、実はこの述語は前章で subseq として登場済みでした。今更です。そしてこれを用いた filter の仕様は以下。
Theorem filter_challenge_2 : forall l : list X,
let T := fun x => test x = true in
all T (filter test l) /\
sublist (filter test l) l /\
(forall l0 : list X,
all T l0 -> sublist l0 l ->
(l0 = filter test l \/
length l0 < length (filter test l))).問題文を見てみると「filter test l が最も長い」という言い回しになっていますが、これはちょっと解釈が微妙。つまり、「長さが最大値を取る」ことだけなら length l0 <= length (filter test l) でよい (つまり、同じ長さの l0 が他にあってもよい) のですが、直感的には「すべての要素が test に対して true を返す最長の部分リスト」がただ一つしかないのは明らかです。今回は後者を採用しています。
リストの長さを直接扱うと証明が複雑になりすぎるので、「部分リストである」という関係を基本にして、次の補題を使うことで長さに関する結論を得ています。
Lemma sublist_length : forall l1 l2 : list X,
sublist l1 l2 ->
(l1 = l2 \/ length l1 < length l2).
仕様の検証
おそらく想定された解答はここまでだと思うのですが、今回はもう少し先まで進んでみましょうか。
ここまでの議論では、filter が仕様を満たすことは検証されていますが、その仕様が filter の挙動をすべて表現している保証がありません。このことは例えば、「戻り値のリストの長さが引数のリスト以下」のような性質を考えてみればわかります。filter は当然この性質を満たしますが、これを満たす関数はそれこそいくらでも構成できますね？ そこでさらに追加として、「ここで記述された仕様を満たすものは filter に限る」ことを示してみます。
仕様その 1
邪魔にならないように Section を改め、仕様その 1 を満たすような関数 f1 を宣言しておきます。
Variable f1 : list X -> list X.
Hypothesis f1_challenge : forall l l1 l2 : list X,
let T := fun x => test x = true in
let F := fun x => test x = false in
merger l l1 l2 -> all T l1 -> all F l2 ->
f1 l = l1.この条件だけで f1 が filter と等しいことが言えればよいわけです。
Theorem spec1_valid : forall l : list X, f1 l = filter test l.
多少トリッキーなのは、filter と逆の抽出を行う関数 antifilter を定義していること。f1 の性質について結論部分に登場するのは l1 だけなので、l から l2 に当たる部分を抽出する関数を準備しておかないと証明が進まなくなってしまいます。
Fixpoint antifilter (f : X -> bool) (l : list X) : list X :=
match l with
| nil => nil
| x :: l' => if test x
then antifilter f l'
else x :: antifilter f l'
end.ちなみに当初の方針では、test x が false のとき true になるような antitest : X -> bool を定義していたのですが、この方法だと bool 値を反転させる関数 negb が必要になるせいで取り回しに難があるようです。
仕様その 2
f2 l と filter test l が長さについて両向きの不等号が成立することを用いて等号を示します。最大値の一意性を証明する際の常套手段ですね。これ以外にも、両向きに sublist 関係が成り立つから、という議論もできるはず。
Variable f2 : list X -> list X.
Hypothesis f2_challenge : forall l : list X,
let T := fun x => test x = true in
all T (f2 l) /\ sublist (f2 l) l /\
(forall l0 : list X,
all T l0 -> sublist l0 l ->
(l0 = f2 l \/
length l0 < length (f2 l))).
Theorem spec2_valid : forall l : list X, f2 l = filter test l.
その他補足
今回「filter と f1 や f2 が同じ関数であること」を、同じ戻り値を返すこと、いわゆる外延性によって定義しましたが、これはちょっと微妙に感じるかもしれません。実際、この意味ではすべてのソートは区別できないことになってしまい、あまりにも雑すぎるというもの。しかしまあ深入りすると危険な気がするので、プログラムの同値性についての話はこれ以上立ち入らないことにしておきましょう。
ちなみに以上の filter の検証、今後これを用いてクイックソートの検証をしようという予定があったりなかったりするのですが、それはまた別の話。
