Curry-Howard Isomorphism
「命題⇔型」や「証明⇔プログラム」という対応のお話。何だかすごいなあ。ところで「ゲーデルの不完全性定理」とか「チューリングマシンの停止問題」なども、プログラミング的に「証明」できたりするのでしょうか。
追記：読者さんから以下のページを教えていただきました。感謝！ Chaitinの例を書き直したものらしいですね。なるほど。
追記：k.inabaさんが、上記のコメントを受けてエントリを書いてくださいました。「証明」できるみたいですね。へええ。
「命題⇔型」や「証明⇔プログラム」という対応のお話。何だかすごいなあ。ところで「ゲーデルの不完全性定理」とか「チューリングマシンの停止問題」なども、プログラミング的に「証明」できたりするのでしょうか。
追記：読者さんから以下のページを教えていただきました。感謝！ Chaitinの例を書き直したものらしいですね。なるほど。
追記：k.inabaさんが、上記のコメントを受けてエントリを書いてくださいました。「証明」できるみたいですね。へええ。