2016年12月02日

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は普通に使う分には問題なく便利なので、ご心配なく。
posted by chiguri at 00:00| Comment(0) | Coq

2013年12月14日

Coq/Agdaのどちらを使う?

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

さて、登録した時点では「Agdaが多いなあCoqかなあ」などと暢気に言っていて、また一日目のnotogawaさんは「みんなCoqのことを書くに決まってる」っぽいことをAAで言っていたわけですが、箱を開けてみたら

Σ(●△●)<Isabelleの人が一人で大半埋めてるじゃねえか!?

というわけでここではCoqとAgdaのことを書きましょう。そうしましょう。

え、CoqとAgdaのことはnotogawaさんが書いてただろって?
細けえこたぁいいんだよ!

・CoqとAgda、どちらを使うべき?


好きな方を選べば良いと思うのですが、個人的な考えを挙げます。

1:性質+証明を書くならCoqがいいです。記号処理や数学の定式化などですね。この辺りはtacticを使うという戦略がかなり効きます。ただ、これに関してはAgdaもたくさん使われていますので、それこそ好みでいいでしょう(個人的にはCoqがいいと思いますが)。
2:プログラム記述+検証についてはCoqの方がいいです。こちらは型や関数の記述自体は割と単純であることを想定しています。tacticもいいですし、SSReflectも便利(らしい)です。
3:型を複雑にして、いろいろな性質を型に持たせたプログラミングをしたいならAgdaの方がいいです。Coqだとプログラムを証明と一緒に(tacticで)書く勇気が必要になります(そうじゃないとやっていられません)。慣れればそれなりにできますが、いちいちイライラします。
4:型の階層を意識したいなら断然Agdaです。なにせCoqはSet/Prop/Typeの区別しかしませんし(内部でTypeのヒエラルキーは計算していますが、表に見えづらいです)。

1は比較的どちらでも良いですし、4は迷いようがありません。
したがって、おそらく悩むことが多いのは2/3の問題でしょう。
選択の一助になれば幸いです。

ちなみに、OCamlとHaskellの一方を使っているから、はほとんど理由になりません。
どうせ大した差ではありません。
スタートアップで一日差がつくかつかないかくらいです。

・inversion大好き


inversion tacticは便利です。(すでに何回主張したか忘れた)
簡単に説明すると、inversion tacticは「この帰納的述語が成り立つためにはどういうことが成り立っている必要がある?」というのを定義から見つけてくる優れものです。
このとき、成り立たないパターン(帰納的述語のコンストラクタのパラメータに一致しない)があるときは勝手にそれらに関して矛盾を作って証明してくれます。
(よって「起こりうるパターンが一つもない」、つまり矛盾していれば証明完了するわけですが、それはあくまで結果論)
inversionなかったらCoqの証明を勧めるとかありえませんね。
(ただしinversionの生成する項ははっきり言って読めない)
Agdaで同じこと?・・・reflection使えば、できたりするのかな・・・?

・で、証明しないの?


最近AgdaでD-Case書きまくってるので勘弁してください。
次があったら例題使って、最初の4分類が何を言いたいのか書いてもいいのですが・・・
タグ:Coq Agda
posted by chiguri at 00:14| Comment(330) | Coq

2012年12月06日

LL/ML Advent Calendar 6日目: gaLLinaで証明する

この記事はLL/ML Advent Calendarの6日目の記事である。

今年はなかなかに なごやこわい なアドベントカレンダーが出てきたなあ、とかつぶやいたら気づいたら犠牲参加者になっていた。

やっぱり なごやこわい 。

LL名古屋に似たようなのがあるようだが?

あの有名なmzpさんが似たような題で発表をしたらしい。

が、録画されたUstreamの動画を見たところ、ぜんぜんGallinaの話をしてない。

そりゃないぜとっつぁんmzpさん。

というわけで、今回は実際にGallinaを使って(証明して)みよう、という話。

Coqの中の言語

Coqはいくつもの言語を持っている。

いやほんと。Coqはシステム全体の総称。

CoqではVernacularとGallinaとLtacが主に使われて、あとはRussel(Programコマンドのシステム名)とかが入っている。

ほかは知らない。あるかもしれないし、ないかもしれない。

Vernacular

基本的にあなたがトップレベルで書いているのはVernacular。

私が書くのもVernacular。

このVernacularはコマンド記述言語。

DefinitionとかTheoremとかInductiveとかFixpointとかClassとかRecordとかGoalとかSearchとかSearchAboutとかPrintとかCheckとか全部Vernacular。

NotationとかCoInductiveとかLocateとか(以下略

Ltac

証明といえばLtac。

applyとか(e)autoとかintro(s)とかinductionとかrewriteとかinversionとかomegaとかgeneralizeとか全部Ltac。

revertとかelimとかcongruenceとか(ry

Gallina

Coqの項記述言語

fun x => tとかmatch a with ... endとかforall P : Prop, ...とか全部Gallina。*1

fix f p ... {struct p} : T := ...とかcofix f ... := ...とk


ここで記事は途切れて・・・ない。

Gallinaで証明?

が、あくまで項記述言語

当然Ltacなんて使えない。

で、Vernacularはできる限り避けるわけだけど・・・


帰納型の宣言ができない。


関数の宣言は無理やりできなくもないが、帰納型ばかりは対処のしようがない*2

しかし、帰納型を入れないと完全にCC*3になってしまうので、そこだけは我慢する。

また、型チェックができないといけないので、Checkコマンドだけは使うことにする。

残念ながらつまらない例

つまらない例しか出さない(出せない)。

Goal forall n : nat, n + 0 = n.
Proof.
intro n; induction n.
 reflexivity.
 simpl; rewrite IHn; reflexivity.
Qed.

これをGallinaでやろう。

とりあえず問題の整理。

  • 証明にLtac使ってる
  • +ってなに?

まあ、実際のところLtac使ってる、なんてPrintコマンドで項を出してしまえばいいんだけど・・・

四苦八苦しながらとりあえずLtacを使わずに書いたものは以下のとおり*4

Check
(nat_ind (fun n : nat => n + 0 = n)
          (eq_refl 0)
          (fun (n0 : nat) (IHn : n0 + 0 = n0) =>
            eq_ind (n0 + 0)
                   (fun n1 : nat => S (n0 + 0) = S n1)
                   (eq_refl (S (n0 + 0)))
                   n0
                   IHn) : forall n : nat, n + 0 = n).

ちなみに最後の型注釈は表示される型を強制するため。

あとは+が気に食わないので、+を展開してみる。

Check
 ((fun plus : nat -> nat -> nat =>
    nat_ind (fun n : nat => plus n 0 = n)
            (eq_refl 0)
            (fun (n0 : nat) (IHn : plus n0 0 = n0) =>
              eq_ind (plus n0 0)
                     (fun n1 : nat => S (plus n0 0) = S n1)
                     (eq_refl (S (plus n0 0)))
                     n0
                     IHn) : forall n : nat, plus n 0 = n)
  (fix plus (n m : nat) :=
    match n with
    | O => m
    | S n' => S (plus n' m)
    end))
> Error: In environment
> plus : nat -> nat -> nat
> The term "eq_refl 0" has type "0 = 0" while it is expected to have type
>  "(fun n : nat => plus n 0 = n) 0".

はて、どうやらplus 0 0が0だと信じられないらしい。

ああそうか、代入してくれないからか。

じゃあletでOKだな*5

Check
 (let plus : nat -> nat -> nat :=
       fix plus (n m : nat) :=
        match n with
        | O => m
        | S n' => S (plus n' m)
        end in
    nat_ind (fun n : nat => plus n 0 = n)
            (eq_refl 0)
            (fun (n0 : nat) (IHn : plus n0 0 = n0) =>
              eq_ind (plus n0 0)
                     (fun n1 : nat => S (plus n0 0) = S n1)
                     (eq_refl (S (plus n0 0)))
                     n0
                     IHn) : forall n : nat, plus n 0 = n).

通った通った。

欲を言えばnat_indとかeq_indとかも消したい。

そこまでやったら死にそうだから今回はやめておく。

まとめ

できる限りGallinaで証明を書くとこうなる、というのを見せた。

関数はlet束縛、rewriteはeq_indを使えばできる。

なんて非現実的。VernacularとLtac万歳。

ちなみに、まじめに上のコードは手で書いているので、しばらくeq_indの使い方のわからなさとエラーメッセージの意味不明さに泣きそうになった。

最後に

vernacuLar×gaLLina×Ltacとか、ダメ、絶対。

*1:matchはLtacにもある。

*2:Gallinaの範囲に帰納型の宣言はない。この宣言、CICの項ではあるのだが・・・

*3:Calculus of Construction、人によってはCoCと略す。

*4:ちなみに実際に元のスクリプトを使うと、eq_indではなくeq_ind_rを使った証明になる。rewrite <- IHnならeq_indとf_equalを使った証明。eq_indでいいじゃん・・・

*5:letとfunは型付け規則が違う。funは中身を展開しないが、letは展開した結果で行う。

posted by chiguri at 13:52| Comment(0) | TrackBack(0) | Coq

2012年03月23日

補足:Falseのパターンマッチのextraction

パターンマッチができるってことは、extractionできるということである。

singleton definitionのパターンマッチの場合、実は非常に簡単で、そのパターンマッチ自体が消えて、結果だけが残る。

一方、empty definitionはそうも行かない。そもそもCoqのterm上は分岐がないのだ。

しかもFalse自体は述語なので消える運命にある。

ではどうなるのか?


結果はこれまた簡単、assert(やそれに類するもの)を使って異常状態であることを知らせる。

なぜなら、検証した結果としてはそこに来ることを想定していないわけだから。

というわけで、これでextractionも可能となり、すべてが丸く収まったわけである。


これで終わり?まだもうひとつある。でもそれはいつ書くか不明。

posted by chiguri at 00:10| Comment(0) | TrackBack(0) | Coq

述語のdestructの例外

これが誰かの何かの役に立てば幸いなのだけれども。


さて、述語に対するパターンマッチは述語以外を返してはいけない、といった。

しかし例外がある。

それは、展開する述語がsingletonまたはempty definitionとして定義されている場合。

この場合はSetやTypeやnatやOやSを返すことが許される。

・・・いや、なにそのなんとかdefinitionって、と言いたくなるだろうがまずは説明を聞いてくれ。


そもそもパターンマッチが述語以外を返してはいけないのは、述語関係のものをすべて消したときに結果が一意にならないからだ。

昨日の問題も、要するにtrueかfalseに決まらないから問題なのだ。

よって、述語の状態が結果に影響を与えなければいい。

究極的には、分岐しなければいい。

つまりそういうことだ。


empty definitionとはコンストラクタを持たない述語のことであり、またsingleton definitionとはパラメータとして述語関係の値以外持たないようなコンストラクタを一つしか持たない述語のことである。

後者はずいぶんややこしいが、つまりはコンストラクタがひとつで、コンストラクタの中にnatだとかSetだとかが入っていなければいい、というもの。

これらはパターンマッチでの展開が結果に影響を与えないので、特別に述語以外を返す展開が許される。


さて、これはどういう場合に役に立つのだろうか?

こんな場面を想定してほしい。

「述語や値の混じった関数を作らなければならない状態で、ある述語が明らかにおかしな値をとった。しかしinversionが使えない。さてどうするか。」

昨日の補足で挙げたinversionができないケースをより細かくしただけだが。

この答えは、Falseを経由する、である。

Falseはboolのfalseではなく、Propに属する矛盾を意味する述語であり、定義は以下のとおり。

Inductive False : Prop := .

典型的なempty definitionである。

したがって、Falseのパターンマッチは許されている。


実際の流れは以下のとおり。

  1. 述語の矛盾が確定した時点でexfalsoやelimtype FalseなどのtacticでFalseの作成に移る。
  2. Falseの証明に述語のinversionを使う。*1

inversionを使って場合わけをしたいときは、データのdestructの後に上の流れを使ってありえない場合を排除するとうまくいく。*2


このように、例外があることで「述語の存在上ありえない状態」を排除することができる。

そんなにこの状態にはまることはないと思うが、もしあったら参考にしてほしい。

*1:Falseは述語なので、ここでのinversionの使用は許される。

*2:実は、inversionの内部でやっているのはまさしくこれ。Trueを使う部分もあるが、手動では明らかに無駄。

posted by chiguri at 00:04| Comment(0) | TrackBack(0) | Coq