MSetsの愚痴、あるいはTheorem Prover Advent Calendar 2日目

これはTheorem Prover Advent Calendar 2日目の記事です。

この記事は、Coqの標準ライブラリに含まれるMSetsについてです。
今回は利用側の視点ではなく、ライブラリ作成側の視点なので、まあ非常にニッチだと思います。

名前からピンとくるかもしれませんが、MSetsは集合のライブラリです。
集合に入っているかを判定する述語、要素の追加や削除、和集合や共通集合、フィルターをかけるなど、一通りのことができます。
ただし、単純な集合ではなく、別途利用者が定義した同値関係を与えることで、「同値な要素」が入っているかを判定するようになっています。
（同値関係にLogicに定義されているeqを使えばよくある集合になります）

MSetsでは、新しい実装を実現する方法として、直接インターフェースを満たすように定義する以外に、RawSetsと呼ばれる「それ自体は集合らしくないこともありうるが、条件を付けると性質が成り立つ」ように記述するインターフェースが提供されています。
（実際はWSetsに対してWRawSets、Setsに対してRawSetsがあります。前者が要素に順序関係を必要としない、後者が要素に順序関係を必要とするものです。以下の説明は正しくはWRawSetsのものです。）
ちょっと分かりにくい日本語だと思うので、例としてリストを使った実装を考えます。
集合を実現するためにリストを用いることは不自然ではありませんが、リストでは要素の重複があったりします。
MSetsでは集合の要素全てをリストにして取り出すelementsという関数が定義されており、そのリストに重複はないことが要求されているので、重複を認めるとちょっと面倒です（ちょっとだけですけどね）。
そのため、「重複のないリストである」場合にそれを集合とする、と考えることで、リストを使ってRawSetsを構築できます。
インターフェース上の性質は全て「重複のないリストであるとする」という条件を課すことになり、それによって初めて証明が可能になったり、また簡単になったりします。

「全て」と書いた直後に何ですが、これが本来のRawSetsの考え方のハズなのです。
では実際のCoqのRawSetsの記述を見てみるとどうでしょう。
ほとんどのものはOkという述語を満たすように集合が扱われています。
しかし、「全て」ではありません。


サボったな貴様

これは予想なのですが、おそらくMSetsの実装者は、いくつかの集合の実装をした際に、「この性質は条件付けなくても簡単に成り立つからいいや」と抜かしたのです。
（実装中に必要になったものだけ追加したのでしょう。）
なぜそのような予想を言うかというと、抜けているものがWRawSetsのfilterやpartition、elements、chooseなど、割と実装からならストレートに示せそうな性質ばかりだからです。
（RawSetsのmin_elt_spec1から3は2だけある割にどのくらいの影響があるかすぐには説明できませんが）

なぜ全部に付けない。


こんなことを調べた理由ですが、MSetsでは毎回要素との等価判定をする（または大小関係の比較をする）ので、等価判定が遅い場合、あまり全体のパフォーマンスが上がらないことになります。
（もっとも、WSetsはともかくSetsでは大小関係を付けて大体が木探索を行うので要素数の対数のオーダーでしか比較を行わず、あまり影響がない気もします）
そこで、等価判定や比較を行う際に「代表的な値」を取ってそれ同士で比較できれば、その「代表的な値」同士で、より高速に比較できるのではないか、と考えたのです。
例えば、剰余が等しいかで同値関係を定義した場合、剰余の結果を取ればそれが「代表的な値」になるでしょう。
集合にある要素を全て剰余にしてしまえば、集合側の要素は毎回剰余を計算しなくてよくなりますから、まあ速くなるのではないでしょうか。


これを実装するには、既存の実装を用いて「代表的な値」による集合を構築して、適切にその集合とのやりとりを定義すればよいでしょう。
というわけで実装しようとしたのですが、上の問題で証明できなくなりました。
集合に入っている要素は全て「代表的な値」であるはずなのですが、簡単にそうでないものが入ります。
filterを始める際に、「代表的な値」以外が入っていると（そして条件がなければ簡単に入り得ます）、filter後の条件を容易には示せません。
結果的に、このままではそんな実装はできないわけです。
どう考えてもできるはずなのに！！

ちなみに、もう一つ問題があり、MSets中ではfilterやpartitionはある性質を持ったフィルター用関数についてしか言及しません。
その結果、目標とするものではfilter後の集合が条件を満たすこと（filter_ok）を示せなくなります。
なぜなら、この性質ではfilterに渡す関数に何の仮定も置かれていないからです。
裏側で動いている「代表的な値」の集合は、filterがある特定の性質を満たす場合に限りうまく動きます。
それじゃ渡しても何も言えません。
インターフェースに何もないのですから。


最初、この二つの点を直したMSetsでPull Requestを送ろうと思ったのですが、いかんせん古いライブラリ（FSets）との互換性を保つための部分に問題が起こり、もう知るかと投げ出しました。
（前者は問題ないのですが、後者がインターフェースに性質を追加するので互換性がなくなります）
現状、ほとんどMSetsと同じそれをXSetsという名前で公開しています。
Opam使ったライブラリに登録をしたいところですが、あまりにMSetsと同じコードなのでなんとも気が引ける部分ではあります。
なお、XSetsの使い方はほぼMSetsと同じです。表面的にはインターフェース上に性質が三つ増えているだけなので。

上の問題、MSetsを普通に使っている分には何の問題もないのですが、どうも嫌なところをついてしまったようです。
上で述べた「代表的な値」による実装（XSetRepresentative）を作っては見たのですが、なんだかんだと実装に時間がかかった割に多分あまり速度上がりそうもありません。（実はまだ試してません）
本当はそれを作ってドヤ顔したかったのですが。


最後に、もう一度言いますが、MSetsは普通に使う分には問題なく便利なので、ご心配なく。