CPS変換と二重否定のカリーハワード対応の話
@syaminoが以下の2つのページを読んだところからスタート。ただしCalculus of constructionsの方は全然理解できていない。
『CPS(継続渡し方式)変換をJavaScriptで説明してみるべ、ナーニ、たいしたことねーべよ - 檜山正幸のキマイラ飼育記』
http://d.hatena.ne.jp/m-hiyama/20080116/1200468797
続きを読む
k
@mathink
@syamino 横槍失礼します。Tコンビネータの型とA->¬¬Aの対応ですが、後者は二重否定除去ではなく二重否定付加なので、直観主義的にも問題なく構成できる型ですから、自然な対応なのではないでしょうか。
2012-02-06 13:52:38
Takashi Miyamoto
@tmiya_
@syamino http://t.co/Ng8P3ldJ こことか読むといいかも。CPS変換は(A->B)をCPSすると((B->X)->(A->X))と思うし、A->¬¬Aは二重否定の除去じゃなくて二重否定導入ですね。
2012-02-06 13:54:42
シャミノ
@syamino
@tmiya_ A->Bを(B->X)->(A->X)にすることと,Aを(A->X)->Xにすることは,区別が必要なのでしょうか? https://t.co/3sZf1fKf
2012-02-06 13:58:02
シャミノ
@syamino
@mathink Tコンビネータに問題が無いことは把握しています。私が気になっているのは少し別のことです https://t.co/T9BbDrwf
2012-02-06 14:09:21
f127z
@f127z
@syamino 横からすいません。∀A Z.((A -> Z) -> Z)という型の関数に継続としてidを渡すことはできないと思います。idの型は∀A.(A -> A)です。∀A B.(A -> B)という型の関数なら渡せます。
2012-02-06 14:26:31
k
@mathink
@syamino すいません、言葉が足りませんでした。自然な対応があるので、むしろ"CPSから元に戻せる"と"任意の~"の対応にずれがあるのではないかと思います、
2012-02-06 14:40:22
シャミノ
@syamino
「任意の値aにTコンビネータを適用した後,idを適用するとaを取り出せる」というのは型をちゃんと見てないから出てきた愚かな発想なんやな
2012-02-06 14:51:59
f127z
@f127z
@syamino 先ほどの論理式なんですが、¬(A)が∀Z((A) -> Z)になるので¬(¬(A))は正確には∀Z ((∀Z ((A) -> Z)) -> Z)になりそうですね。つまりrank-2多相の関数。
2012-02-06 19:53:13