Hatena::ブログ(Diary)

chiguriの生態(嘘や誇張アリ)

2012-03-22

述語のdestruct

| 19:00

これ見る人いるのかな・・・


昨日の話と全然連続しないが、昨日のシリーズの続き。

Propに属する帰納型(以下、述語と記述)の展開の話。

Coqマニュアルだとここの4.5.4のAllowed elimination sortsのあたり。

実際のところ、使用者からして気になる部分はそう多くなくて、大体がこの部分。

しかし、非常に読みにくい。

というわけで簡単な説明をする。


destructといいながら、Curry-Howard対応から実際にはパターンマッチなのでこちらを使う。

内容は、パターンマッチで述語を場合分けすると、ある特定の場合にできない場合がある、というもの。

ちなみにSetやTypeに属する帰納型ではどんなものでも返せる。


さて、特定の場合、と言っているがどんな場合かと言うと、返す値が述語じゃないときである。

逆に言うと述語ならOK。SetとかTypeとか(述語でない)型自体とか全部ダメ。

この理由は、proof irrelevanceという考え方から来ている。

まあ、問題を見るにはextractionを考えればいい。


Proof irrelevanceは、簡単に言うと「証明なんてプログラムと関係ないんだから、プログラムとしては無視して問題ないよね?」ということ。

顕著な例がextraction。Coqから別の言語のコードに変換すること。

証明はきれいさっぱり消えるし、依存型も述語部分が消える。

いやはや、なかなか良くできている。


だが、消えるのだから困ることもある。

こんなプログラムが書けたらどうなるだろう?

fun x : or P Q =>
 match x with
 | or_intror _ => true
 | or_introl _ => false
 end

trueやfalseはbool型、boolはSet。orはProp。

さて、extractionするとどうなる?

  1. 関数引数xは消える。or P Qが述語だから。
  2. trueやfalseは消えない。boolはSetだから。

で、何が出る?関数じゃないことはわかるが、true?false?

つまりはこれがまずい、ということである。*1 *2 *3


だが、この問題、実は例外があって・・・

と言っても長くなるのでまた今度。

実は例外がないとそれはそれで困るのだ。*4

*1:もう少し体系に踏み込めば、これは「気にしない」はずの証明を「プログラムから気にしている」わけで、その意味でおかしい。

*2:実際、先週のPROでこの問題に引っかかった人がいたようだ。

*3:最初はPropがimpredicative sortだからか、とも思っていたが、昨日のオプションを試してもSetからTypeへのパターンマッチが可能なのでそういうわけでもなさそうだ。

*4:逆にこの例外のおかげで自分の研究では少し困ったんだが。

リンク元