07/12/29 00:24:27
>>167
数理論理学とコンピュータ・プログラムの間には深い関連性がある。
Ａ．近代論理学の開祖であるフレーゲの概念記法を出発点とするゲンツェンの自然演繹
Ｂ．チャーチの型付きラムダ計算
２つのモデルはカリー・ハワード対応によって同型として対応付けられる。
つまり、論理学の問題と言っているのは、実はコンピュータ・プログラムの問題と言っているのと同じなのだ。
QED.
07/12/29 00:24:27
>>167
数理論理学とコンピュータ・プログラムの間には深い関連性がある。
Ａ．近代論理学の開祖であるフレーゲの概念記法を出発点とするゲンツェンの自然演繹
Ｂ．チャーチの型付きラムダ計算
２つのモデルはカリー・ハワード対応によって同型として対応付けられる。
つまり、論理学の問題と言っているのは、実はコンピュータ・プログラムの問題と言っているのと同じなのだ。
QED.