2006/05/12

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!

No comments :