CPS変換と二重否定のカリーハワード対応の話
A->Bを(B->X)->(A->X)にすることと,Cを(C->X)->Xにすることの対応。Cを1->Cとみなして,(C->X)->(1->X) 。1->XをXとみなして,(C->X)->X
2012-02-04 19:13:55忘れてた #1は終対象 RT @syamino: A->Bを(B->X)->(A->X)にすることと,Cを(C->X)->Xにすることの対応。Cを1->Cとみなして,(C->X)->(1->X) 。1->XをXとみなして,(C->X)->X
2012-02-04 19:14:27¬A を A->False として扱うことと ∀Z.A->Z として扱うことがあるの? / 『Calculus of constructions - Wikipedia, the free encyclopedia』 http://t.co/zMuK8My7
2012-02-05 09:53:10@tmiya_ Coqの勉強をさぼって質問します。これは「矛盾からは何でも導ける」という話と関係がありますか?∀Z.False->Z は証明できるのですか?
2012-02-05 11:27:03@tmiya_ さらに質問です。∀Z.A->(A->Z)->Z はTコンビネータであり,問題なく作れる。 ∀Z.((A->Z)->Z)->A はidを適用すれば取り出せる(継続渡しスタイルから戻す)。という認識なのですが,これらは証明できるのですか?
2012-02-05 11:36:14@syamino 横やりで申し訳ないと思いますが、1:∀Z:Prop.False->Zは証明できますし、それを使ってtmiya_さんは証明なさっています。2:Tコンビネータは作れますが、後ろの方は無理です。直観的には、ZとAの関連がないので直観主義的ではありません。
2012-02-05 12:44:42@syamino 「継続渡しスタイルから元の形に戻せない」ではなく「call/ccが無い」ではないかなぁ。「二重否定の除去が出来ない」の対応物は。
2012-02-06 12:19:48@tmiya_ では,「継続渡しスタイルから元に戻せる」もっと具体的に言うと「任意の値aにTコンビネータを適用した後,idを適用するとaを取り出せる」という現象は一体何なのでしょうか?
2012-02-06 12:32:30@syamino ごめんなさいTコンビネータを検索したけどみつかりませんでした。あと、現象はいったい何なのかというのはもしかして哲学的な話なんでしょうか?だとしたら全然判りません。(カリーハワード対応という現象はいったい何かと聞かれても私にはそういう対応があるとしか判りません。)
2012-02-06 12:53:23@syamino 多分 syamino さんがちょっとだけ論理学を勉強するのが一番早道かも。小野先生の「現代数理論理学序説」とか多分読むと色々得られるところのある本だと思います。
2012-02-06 12:55:42@tmiya_ Tコンビネータの型は A->(A->B)->B です。私にはこれがCPS変換に見えると同時に,A->¬¬A にも見えます
2012-02-06 12:58:32@syamino Tコンビネータの情報ありがとうございます。うーむ、単にそう計算するとそうなる、としかよく判りません。特に意味とか考えてないし。。。
2012-02-06 13:00:55@oskimura こういう否定を想定しています / 『Calculus of constructions - Wikipedia, the free encyclopedia』 http://t.co/zMuK8My7
2012-02-06 13:08:14@tmiya_ 単純に,二重否定除去に対応しているように見える型の項を作ることができるのを不思議に思っているだけです。おそらく私がどこかを勘違いしているのでしょうが,どこかわかりません
2012-02-06 13:32:55