callccによる排中律の証明
悪魔：「あなたが私と契約してくれたら、(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同型を教えていないのは…昔は演習３で萩谷研へ行けばやりましたが、言われてみれば計算機言語論あたりでやっても良いのかも。僕が言ってもしょうがないですが。あと、僕も極座標表示は高校では習っていません。もちろん塾ではやったけど。
