sumiiの日記 - callccによる排中律の証明
http://d.hatena.ne.jp/sumii/20060507/1147006438

さらに劣化コピー。Schemeのcall/ccで悪魔の契約書を作ってみる。型についてはまったく無知なので、排中律の証明とは関係ありません。
（昨日は会社でhisashimさんに適当な説明をした気がする。ごめんなさい。）

追記：最初のは間違ってたので差し替えました。

(define able-to-pay? #f)
(define remind-contract #f)

(define (devils-contract init-choice)
  (let ((ability able-to-pay?))  
    ((lambda (choice)
      (cond ((equal? 'first-answer choice)
             (display ""))
            ((and (equal? 'B choice) ability)
             (display "Say any wish!"))
            (else
             (display "Devil gives you one billion dollars"))))
     (call/cc
      (lambda (continuation)
        (cond ((equal? 'A init-choice)
               (display "Devil chooses A"))
              ((equal? 'B init-choice)
               (display "Devil chooses B")))
        (set! remind-contract continuation)
        (continuation 'first-answer))))))

この挿話は、悪魔にとって選択肢が(A)と(B)しかありえないことがポイントなんだと思う。つまり、(B)じゃなければ(A)。(B)でもないし(A)でもないってことはありえないドライな世界。上のコードだと、最初のcondが契約書に相当するつもり。
で、悪魔は自分が「発話した内容」なんて覚えちゃいない。上のコードでいうと、call/ccの中のcondは覚えちゃいない。あくまでも契約書オンリーなので、後から1億ドル払っても、(B)じゃなかったんだから(A)を履行するってことなんだと思う。

くだんのシナリオは、こんな感じ。

gosh> (devils-contract 'B)
Devil chooses B
gosh> (set! able-to-pay? #t)
#t
gosh> (remind-contract 'B)
Devil gives you one billion dollars

最初の(devils-contract 'B)で悪魔自身は「(B)を選びます」と言っているけど、人間が1億ドル払わなかった時点で実は(A)の契約が成立している。あとから1億円用意(set! able-to-pay? #t)してもだめ（悪魔の契約履行が10年後だったのがひっかけっぽいかも）。

1億円支払い可能な状態で契約し、悪魔が(B)を選択すれば、望みがかなえられるんでしょう。そんな人に悪魔が契約を持ち込むとは思えませんが……

gosh> (set! able-to-pay? #t)
#t
gosh> (devils-contract 'B)
Devil chooses B
gosh> (remind-contract 'B)
Say any wish!