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

シャミノ @syamino

@tmiya_ 近々『現代数理論理学序説』を読むつもりです

k @mathink

@syamino 横槍失礼します。Tコンビネータの型とA->¬¬Aの対応ですが、後者は二重否定除去ではなく二重否定付加なので、直観主義的にも問題なく構成できる型ですから、自然な対応なのではないでしょうか。

Takashi Miyamoto @tmiya_

@syamino http://t.co/Ng8P3ldJ こことか読むといいかも。CPS変換は(A->B)をCPSすると((B->X)->(A->X))と思うし、A->￢￢Aは二重否定の除去じゃなくて二重否定導入ですね。

シャミノ @syamino

@tmiya_ A->Bを(B->X)->(A->X)にすることと，Aを(A->X)->Xにすることは，区別が必要なのでしょうか？ https://t.co/3sZf1fKf

シャミノ @syamino

@mathink Tコンビネータに問題が無いことは把握しています。私が気になっているのは少し別のことです https://t.co/T9BbDrwf

集会の自由 @oskimura

Coqのような高階型だとCPS変換は型を保存するとは限らない

集会の自由 @oskimura

単純型付きラムダ計算やSystemFでは保存されるけど

シャミノ @syamino

こういう話を調べている RT @oskimura: Coqのような高階型だとCPS変換は型を保存するとは限らない

集会の自由 @oskimura

@syamino こちらをどうぞ http://t.co/XoRqGjXk

シャミノ @syamino

@oskimura ありがとうございます

f127z @f127z

@syamino 横からすいません。∀A Z.((A -> Z) -> Z)という型の関数に継続としてidを渡すことはできないと思います。idの型は∀A.(A -> A)です。∀A B.(A -> B)という型の関数なら渡せます。

f127z @f127z

@syamino しかしこれは戻り値が多相なので値を作れません。なので例外を投げたりできないといけません。

シャミノ @syamino

@f127z なるほど，だんだん私の勘違いがわかってきました

f127z @f127z

@syamino お役に立てたようでなによりです。

k @mathink

@syamino すいません、言葉が足りませんでした。自然な対応があるので、むしろ"CPSから元に戻せる"と"任意の~"の対応にずれがあるのではないかと思います、

シャミノ @syamino

「任意の値aにTコンビネータを適用した後，idを適用するとaを取り出せる」というのは型をちゃんと見てないから出てきた愚かな発想なんやな

シャミノ @syamino

自己適用は出てこないけど，これも型無しラムダ計算の闇の１つなのかな

f127z @f127z

あれ、∀のスコープがちょっと違うかな…？

f127z @f127z

@syamino 先ほどの論理式なんですが、￢(A)が∀Z((A) -> Z)になるので￢(￢(A))は正確には∀Z ((∀Z ((A) -> Z)) -> Z)になりそうですね。つまりrank-2多相の関数。

f127z @f127z

idは戻り値の型が多相ではないので渡せない、という結論は変わらないのですが。