CPS変換と二重否定のカリーハワード対応の話

@syaminoが以下の2つのページを読んだところからスタート。ただしCalculus of constructionsの方は全然理解できていない。 『CPS(継続渡し方式)変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ - 檜山正幸のキマイラ飼育記』 http://d.hatena.ne.jp/m-hiyama/20080116/1200468797 続きを読む
6
シャミノ @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:13:55
シャミノ @syamino

忘れてた #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
シャミノ @syamino

Tコンビネータ λa b. b a の型はC->(C->X)->Xなので,CPS変換の一種といえそうだなー

2012-02-04 19:42:42
シャミノ @syamino

CPS変換,直観主義論理,古典論理のあたりを調べている

2012-02-04 20:06:18
シャミノ @syamino

¬A を A->False として扱うことと ∀Z.A->Z として扱うことがあるの? / 『Calculus of constructions - Wikipedia, the free encyclopedia』 http://t.co/zMuK8My7

2012-02-05 09:53:10
シャミノ @syamino

@syamino ということは,AとTrue->Aの対応から類推して,∀Z.Z->Aというのも考えたら楽しいのかな?

2012-02-05 09:59:49
Takashi Miyamoto @tmiya_

@syamino 片方からもう片方を導けるので等価だと思います。http://t.co/HVT0VKxY

2012-02-05 10:42:00
シャミノ @syamino

@tmiya_ Coqの勉強をさぼって質問します。これは「矛盾からは何でも導ける」という話と関係がありますか?∀Z.False->Z は証明できるのですか?

2012-02-05 11:27:03
シャミノ @syamino

@tmiya_ さらに質問です。∀Z.A->(A->Z)->Z はTコンビネータであり,問題なく作れる。 ∀Z.((A->Z)->Z)->A はidを適用すれば取り出せる(継続渡しスタイルから戻す)。という認識なのですが,これらは証明できるのですか?

2012-02-05 11:36:14
シャミノ @syamino

継続渡しスタイルの関数にidを渡して値を取り出すことと,二重否定除去の関係がわからない

2012-02-05 11:38:20
Sosuke MORIGUCHI @chiguri

@syamino 横やりで申し訳ないと思いますが、1:∀Z:Prop.False->Zは証明できますし、それを使ってtmiya_さんは証明なさっています。2:Tコンビネータは作れますが、後ろの方は無理です。直観的には、ZとAの関連がないので直観主義的ではありません。

2012-02-05 12:44:42
シャミノ @syamino

@chiguri @tmiya_ なるほど。ありがとうございます

2012-02-05 12:49:55
シャミノ @syamino

「二重否定除去はできない」なら抵抗は無いけれど,「継続渡しスタイルから元の形に戻せない」だと抵抗が有る

2012-02-06 07:07:30
シャミノ @syamino

Propとかsmall typesとかよくわかってないけど,そのへんが関係あるのかなあ

2012-02-06 07:08:17
Takashi Miyamoto @tmiya_

@syamino 「継続渡しスタイルから元の形に戻せない」ではなく「call/ccが無い」ではないかなぁ。「二重否定の除去が出来ない」の対応物は。

2012-02-06 12:19:48
シャミノ @syamino

@tmiya_ では,「継続渡しスタイルから元に戻せる」もっと具体的に言うと「任意の値aにTコンビネータを適用した後,idを適用するとaを取り出せる」という現象は一体何なのでしょうか?

2012-02-06 12:32:30
シャミノ @syamino

継続渡し周辺のカリーハワード対応むずかしい

2012-02-06 12:34:38
Takashi Miyamoto @tmiya_

@syamino ごめんなさいTコンビネータを検索したけどみつかりませんでした。あと、現象はいったい何なのかというのはもしかして哲学的な話なんでしょうか?だとしたら全然判りません。(カリーハワード対応という現象はいったい何かと聞かれても私にはそういう対応があるとしか判りません。)

2012-02-06 12:53:23
シャミノ @syamino

@tmiya_ λa b. b a のことです / 『Combinator Birds』 http://t.co/EnB76Ges

2012-02-06 12:55:16
Takashi Miyamoto @tmiya_

@syamino 多分 syamino さんがちょっとだけ論理学を勉強するのが一番早道かも。小野先生の「現代数理論理学序説」とか多分読むと色々得られるところのある本だと思います。

2012-02-06 12:55:42
シャミノ @syamino

@tmiya_ Tコンビネータの型は A->(A->B)->B です。私にはこれがCPS変換に見えると同時に,A->¬¬A にも見えます

2012-02-06 12:58:32
Takashi Miyamoto @tmiya_

@syamino Tコンビネータの情報ありがとうございます。うーむ、単にそう計算するとそうなる、としかよく判りません。特に意味とか考えてないし。。。

2012-02-06 13:00:55
集会の自由 @oskimura

否定を入れるにはボトム_|_が必要なのでは?

2012-02-06 13:05:19
シャミノ @syamino

@oskimura こういう否定を想定しています / 『Calculus of constructions - Wikipedia, the free encyclopedia』 http://t.co/zMuK8My7

2012-02-06 13:08:14
シャミノ @syamino

@tmiya_ 単純に,二重否定除去に対応しているように見える型の項を作ることができるのを不思議に思っているだけです。おそらく私がどこかを勘違いしているのでしょうが,どこかわかりません

2012-02-06 13:32:55