sumiiの日記 このページをアンテナに追加 RSSフィード

2006-05-07

callccによる排中律の証明

Wadlerのパクリ。というか劣化コピー

悪魔:「あなたが私と契約してくれたら、(A)『私があなたに一億円をあげる』、(B)『あなたが私に一億円をくれたら、どんな願いでもかなえてあげる』のどちらかをして差し上げます。(A)と(B)のどちらにするかは、私が決めます。」

人間:「どちらにせよ害はなさそうなので、じゃあ契約します。」

悪魔:「はい、では私は(B)を選びます。」

人間:「やっぱりそう来るか。でも一億円なんて持ってないし、まあいいや。」

(十年後)

人間:「気になってしょうがないので、悪いことをして一億円を集めました。だから願いをかなえてください。」

悪魔:「そりゃどうも(と一億円を受け取る)。では私は(A)を選びます。はいどうぞ(と一億円を返す)。」

ICFP 2003の会場ではWadlerとShiversが壇上で寸劇をやりました(本当)。λ式で書くと

callcc(λk:¬(T∨¬T). InRight(λx:T. k(InLeft x)))

が型T∨¬Tを持つ。ただし¬T = T→Void。Voidは偽(False)を表す、属する値がない空の型で、たとえばOCamlでいうと

type void = Void of void

みたいなものです(前にも書きましたがC言語のvoidがvoidと名付けられているのは型理論的に間違い)。InLeftとInRightは、∨の証明を表現するための値構成子で、まあ

type ('a, 'b) sum = InLeft of 'a | InRight of 'b

と思って良いです。

ちなみに有名事実のようですが、一般にCPS変換は二重否定に対応するので、単純型つきλ計算+callcc(古典論理)で命題Tが証明できるなら、¬¬Tはcallccのない単純型つきλ計算直観主義論理)でも証明できるらしい。実際に¬¬(T∨¬T)は

λk:¬(T∨¬T). k(InRight(λx:T. k(InLeft x)))

と証明できる。

門外漢なので、嘘を言っていたらツッコんでください。>専門家

追記:酒井さんのエントリと完全にかぶってた…。まったく知らずに書いてしまいました。いや本当に。;_;

あと、このエントリではCurry-Howard同型の説明はサボりましたが、稲葉さんのわかりやすい解説が。ちなみに細かい話ですが「(a -> ⊥) -> ⊥ 型の値をうけとると a 型になっちゃうヤツ、それが call/cc」の「(a -> ⊥) -> ⊥」は「(a -> ⊥) -> a」です…よね? 例によって僕がボケていなければ…。東大ISでCurry-Howard同型を教えていないのは…昔は演習3で萩谷研へ行けばやりましたが、言われてみれば計算機言語論あたりでやっても良いのかも。僕が言ってもしょうがないですが。あと、僕も極座標表示は高校では習っていません。もちろんではやったけど。

酒井酒井 2006/05/08 00:08 直感主義じゃなくて直観主義ですよ(^^;
それと、古典命題論理でAが証明できるならば¬¬Aは直観主義命題論理で証明できるというのは、論理学では Glivenko’s Theorem として知られています。

sumiisumii 2006/05/08 07:09 ぐは。(^^; すごい変換ミス…

k.inabak.inaba 2006/05/08 22:29 はい。指摘いただいたとおりcall/ccは「(a -> ⊥) -> a」だと思います…。自分の日記に追記しましたが、正直、「(a -> ⊥) -> ⊥」の方が説明が楽だったので適当書きましたスミマセン(^^;;;

k.inabak.inaba 2006/05/09 00:01 …そして、しばらく考えてみると「(a -> ⊥) -> a」だと説明が面倒そうと感じたのは完全に自分の勘違いだったことに気づいたので、ざっくりと修正しています…(汗

j=1728j=1728 2006/05/10 01:18 契約は1回しかしてないのになぜ悪魔は2回選択できたんですか?

sumiisumii 2006/05/10 06:41 それがcallccの「特徴」でして、タイムマシンのごとく、同じ継続を何度も使えるという…

massmass 2006/05/11 00:09 あれ?IS で Curry-Howard 対応は普通にやった記憶がありますよ?……よねけんの内輪での話でしたっけ。。。うーん。授業でやったような気がするんですが。

j=1728j=1728 2006/05/11 00:51 うーーん、この寸劇を見ても callcc が理解しやすくなった気がしないんですが…。別にそういう目的ではなかったのかな。

sumiisumii 2006/05/11 07:43 タイトルにもあるように、目的はcallccの説明じゃなくて、「callccによる排中律の証明」(callcc(λk:¬(T∨¬T). InRight(λx:T. k(InLeft x))))の説明なので…

sumiisumii 2006/05/11 07:57 >massさん
どの授業でした? 毎年の授業内容は完全に担当教員にまかせられているので、やった人ないし年があってもおかしくないとは思います。

olegoleg 2006/05/11 20:02 スミマセン。排中律というは、Curry-Howard対応によって自動証明があります。
こちらに
[http://pobox.com/~oleg/ftp/Computation/Computation.html#typechecker-CH]、
型と式を相互に表現する関係です。式を入れて型を手に入れられます。逆に、
型では、式を手に入れようとします。例えば、型(A∨¬A)から変換
した型`(neg (neg `(,(neg ’a) + ,(neg (neg ’a)))))を入れると、374 ms後、
(lambda (_.0) (_.0 (inr (lambda (_.1) (_.0 (inl _.1))))))という式を見
ています。CPSから変換すると、(call/cc (lambda (k) (k (inr (lambda (x) (k (inl
x)))))))になりますよ。日本語が全然上手じゃありません、ごめんなさい。

sumiisumii 2006/05/11 22:07 コメント、どうもです。命題論理なので自動証明できるのは自然ですが、negが一つ多いような気もします。何か深い訳があるのでしょうか…? あと、なぜ+は二重にquoteする必要があるのでしょうか。リンク先を見ればわかるのかもしれませんが。

…とか日本語で書いても良かったでしょうか。:-)

j=1728j=1728 2006/05/12 01:34 くどくてすみませんが、この寸劇の楽しさを理解できるのは「callccによる排中律の証明」の近辺を理解しそうな人だろうということですか。

sumiisumii 2006/05/12 07:28 いや、もちろんそうですが…? そもそも少なくともCurry-Howard同型を知らないとわからないでしょうし。

olegoleg 2006/05/12 13:57 「+は二重にquoteする」ということは、typoがありました。2つquasiquoteじゃな
くて唯一のquasiquoteです。大切な詳細を忘れてしまいました。
そういうlogic.scmには、(define (neg x) `(,x -> . F))という定義なんです。
Fというのは、抽象型ですよ。
なので、(neg (neg `(,(neg ’a) + ,(neg (neg ’a)))))と同じ(Haskellの記法に)
(((Either (a->F) ((a->F)->F))->F)->F)という型です。
深い訳は、次のようなものかもしれません。
古典命題論理の(A + ¬A)を
直観主義命題論理にGlivenko theoremで変換すると、¬¬(A + ¬A)になります。それで、
¬¬(A + ¬A) == ¬( ¬(A + ¬A) ) =={DeMorganの律}
¬( ¬A * ¬¬A ) == {DeMorganの律ですよ、直観主義命題論理で}
¬¬( ¬¬A + ¬¬¬A ) == ¬¬(¬¬A + ¬A)
logic.scmには、DeMorganの律などの証明式があります。

sumiisumii 2006/05/12 14:12 単純に¬¬(A + ¬A)を表現した(neg (neg `(a + ,(neg ’a))))を入力しても駄目なんでしょうか?

olegoleg 2006/05/13 12:36 (neg (neg `(a + ,(neg ’a))))もうまくいきましたよ。143 ms間がかかって、結
果が全く同じです。難しい解答が好きですようなんです...
¬¬(A + ¬A)==¬¬(¬¬A + ¬A)そういう証明が正しかったようです。
logic.scmを改正しました。ありがとうございます。

投稿したコメントは管理者が承認するまで公開されません。

スパム対策のためのダミーです。もし見えても何も入力しないでください
ゲスト


画像認証

トラックバック - http://d.hatena.ne.jp/sumii/20060507/1147006438