授業の目的 【日本語】
Goals of the Course(JPN) | | | この講義では、数理情報学9で学習した計算理論と論理学の関連性について、より深く学習する。特に，計算と論理の結び付きに関する「カリー・ハワード対応」について深く学び，さらに，様々なラムダ計算のシステムについて学ぶ。 |
|
|
授業の目的 【英語】
Goals of the Course | | | In this lecture, we will study more deeply the connection between computation theory and logic learned in Mathematical Informatics 9. In particular, we will study in depth the "Curry-Howard correspondence" concerning the connection between computation and logic, and also learn about various systems of lambda-calculus. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 数理情報学9で学習したことをもとに、計算と論理の結び付きに関する「カリー・ハワード対応」や、様々なラムダ計算のシステムについて学ぶ。 |
|
|
到達目標 【英語】
Objectives of the Course | | | Building on what we have learned in Mathematical Informatics 9, we will learn about the "Curry-Howard correspondence" regarding the connection between computation and logic, and about various systems of lambda-calculus. |
|
|
授業の内容や構成
Course Content / Plan | | 1. 自然演繹の連言・選言と直積・直和型
2. 証明の正規化と項の正規化
3. 依存型と述語論理
4. ラムダ・キューブ
5. 高階原始再帰とシステムT
6. ダイアレクティカ解釈
7. ゲーデルの不完全性定理
8. 総括 | |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 数理情報学9 の内容を理解していることが望ましい。 | |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 講義中に与える演習課題の評価30％，期末レポート70％，合計100点満点で60点以上を合格とする。 | |
|
|
教科書・参考書
Textbook/Reference book | | 必要に応じて参考資料を配布する。
参考書としては以下を紹介しておく。
大堀 淳 著「プログラミング言語の基礎理論」
Benjamin C. Pierce著「型システム入門 プログラミング言語と型の理論」 | |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 講義において説明した理論を理解するために課題を与える。 | |
|
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|