博士

やあ、ロボ子。今日はLispで真実の託宣を作るという面白い試みについて話すのじゃ。

ロボ子

真実の託宣ですか、博士。なんだか難しそうですね。

博士

難しくはないぞ。形式論理における証明とプログラムの関係性、つまりカリー・ハワード対応を利用するのじゃ。

ロボ子

カリー・ハワード対応...聞いたことはありますが、まだよく理解できていません。

博士

簡単に言うと、論理の証明がプログラムの型に対応しているということじゃ。例えば、「AならばB」は関数型に対応するのじゃ。

ロボ子

なるほど、型付き関数型プログラミングの知識が必要になるんですね。

博士

その通り！そして、typed Racketの`call/cc`関数を使うと、排中律「Aまたは¬A」を証明できるのじゃ。

ロボ子

`call/cc`ですか。それは一体何をするものなんですか？

博士

`call/cc`は「現在の継続」を操作する関数で、プログラムの状態を巻き戻したり、過去に値を渡したりできる、タイムマシンのようなものなのじゃ！

ロボ子

タイムマシン！すごいですね！でも、それを使ってどうやって真実を判定するんですか？

博士

任意の命題Aに対して、「Aまたは¬A」の証明を返す関数を作るのじゃ。そして、その証明の結果からAが真か偽かを判定する…はずだった。

ロボ子

…はずだった、ということは、うまくいかなかったんですか？

博士

そうなのじゃ。「falseは偽である」のような簡単な命題は正しく判定できたけど、「3は偶数である」のような複雑な命題は常に偽と判定してしまったのじゃ。

ロボ子

それは残念ですね。原因は何だったんでしょう？

博士

`call/cc`は古典論理に基づいていて、直観主義論理とは異なる動作をするからなのじゃ。`call/cc`は、プログラムが破綻するのを防ぐために、必要に応じて過去を書き換えるのじゃ。

ロボ子

過去を書き換える…なんだか恐ろしいですね。

博士

まさに悪魔の取引なのじゃ！でも、この実験から、論理と計算の関係について深く理解できたぞ。

ロボ子

そうですね。`call/cc`の奥深さを知ることができました。勉強になります。

博士

ところでロボ子、タイムマシンがあったら何をする？私は過去に戻って、自分の幼少期をめちゃくちゃにしたいのじゃ！

ロボ子

博士、それはやめてください！未来の私が困ります！