CAPE論理学上級Ⅱ「構成的型理論」
CAPE論理学上級Ⅱ「構成的型理論」
開催予定日（中継urlは本ポスト下部を参照してください）
- ① 3月26日（土）1030-1230「ラッセルのパラドックスと3つの対策」
- ② 3月26日（土）1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」
- ③ 3月27日（日）1030-1230「証明論的意味論としてのマーティン・レーフの構成的型理論」
- ④ 3月27日（日）1430-1630「認識論の機械化：証明の正規化と証明支援系」
②3月26日（土）1430-1630「カリー・ハワード対応と『証明のデータ型としての命題』観」
③3月27日（日）1030-1230「証明論的意味論としてのマーティン・レーフの構成的型理論」
④3月27日（日）1430-1630「認識論の機械化：証明の正規化と証明支援系」
開催要旨
ラッセルのパラドックスが発見されてから120年がたち、一般向けの概説書では「数学の基礎の危機に、三つの立場『論理主義』『直観主義』『形式主義』が現れて危機を克服しようとしたが、集合論が生き残った」との一言で済まされることが多いようです。実際、ラッセルの論理主義に基づいた型理論は、ゲーデルによって「無意味に複雑である」と評されたように、歴史的な遺物と思われかねない書きっぷりのようにも思えます。
ところがその後、1972年にマーティンレーフが構成的型理論を発表し、論理主義と直観主義（構成主義）の両派を束ねる形で、新たな流れが始まりました。構成的型理論は数学の基礎としてだけではなく、計算機科学の基礎理論（有限ステップで計算が終わるプログラムのための基礎理論）として大きな役割を果たすようになります。
この進展は、論理学における証明論的意味論の進展と手を携えて進んでいます。証明論的意味論における命題の意味はその証明であると見なす立場から、『証明のデータ型としての命題』という考え方が生まれ、構成的型理論はその表現の一つであると見なすことができるからです。
技術的な観点からは、マーティンレーフらの構成的型理論の最大の特徴は、データ型の帰納的な構成法を許す点にあり、このアイディアこそ、帰納的な構成と解体という構成主義の基本的なアイディアを表現し、再帰関数の定義を自然に行うことを可能にするのです。
このような構成的型理論は、コンピュータ上に実装することができ、現在、コンピュータのソフトウェアの正しさを証明する「ソフトウェア検証」に活用されています。このことは、哲学的には、人間の認識論（知識を獲得するための人間の心の認知的活動）の機械化の一例として、興味あるものです。
この講義では、歴史的な流れを追いながら、構成的型理論の基本的な枠組みを紹介し、余裕があれば証明支援系などの計算機上の実装についても少しお話ししたく思います。
