■

授業第二十五回目、授業最終回ですが、本日はエクストラとして、カリー・ハワード対応の話です。最小論理の⇒断片について、命題は証明の集まりというアイディアをもとに、証明をλ項で表現し、⇒の導入規則がλ抽象化と、⇒の除去規則が関数適用と対応がつくことを紹介します。このことは、論理式を証明すると言うことと、λ項を使い計算を行うことが本質的には同じことを示唆しています。