2024年度 学院等開講科目 情報理工学院 数理・計算科学系 数理・計算科学コース
代数学特論
- 開講元
- 数理・計算科学コース
- 担当教員
- 土岡 俊介
- 授業形態
- 講義 (対面型)
- メディア利用科目
- -
- 曜日・時限
(講義室) - 月7-8 (W8E-306(W832)) / 木7-8 (W8E-306(W832))
- クラス
- -
- 科目コード
- MCS.T417
- 単位数
- 200
- 開講時期
- 2024年度
- 開講クォーター
- 4Q
- シラバス更新日
- 2025年3月14日
- 使用言語
- 日本語
シラバス
授業の目的（ねらい）、概要
依存型と形式証明を、検証器の実装を通じて学ぶ
到達目標
Cやpythonといったありふれた言語で、教科書「Type Theory and Formal Proof: An Introduction (R. NederpeltとH. Geuvers著)」に基づく検証器を実装し、簡単な命題の証明の形式証明を各自の検証器で行えるようになる。実装に主眼を置くため、理論的な背景は解説しない。
キーワード
ラムダ・キューブ、形式証明、依存型
学生が身につける力
- 専門力
- 教養力
- コミュニケーション力
- 展開力 (探究力又は設定力)
- 展開力 (実践力又は解決力)
授業の進め方
月曜日は教科書を解説し、木曜日は演習風の実装の時間とする
授業計画・課題
| 授業計画 | 課題 | |
|---|---|---|
| 第1回 | イントロダクション | 授業の内容を理解する |
| 第2回 | 実装（アルファ合同） | 授業の内容を理解する |
| 第3回 | ラムダ・キューブ | 授業の内容を理解する |
| 第4回 | 実装（ベータ変換） | 授業の内容を理解する |
| 第5回 | 表示的定義（別名） | 授業の内容を理解する |
| 第6回 | 実装（デルタ展開） | 授業の内容を理解する |
| 第7回 | 原始的定義（公理） | 授業の内容を理解する |
| 第8回 | 実装（型推論） | 授業の内容を理解する |
| 第9回 | 実装（複雑さ） | 授業の内容を理解する |
| 第10回 | ド・ブラウン・インデックス | 授業の内容を理解する |
| 第11回 | 実装（最適化） | 授業の内容を理解する |
| 第12回 | 命題・型（証明・項）対応（PAT） | 授業の内容を理解する |
| 第13回 | 証明支援系（Lean） | 授業の内容を理解する |
| 第14回 | A future of mathematics?（私見） | 授業の内容を理解する |
準備学修(事前学修・復習)等についての指示
学修効果を上げるため，教科書や配布資料等の該当箇所を参照し，「毎授業」授業内容に関する予習と復習（課題含む）をそれぞれ概ね100分を目安に行うこと。
教科書
「Type Theory and Formal Proof: An Introduction (R. NederpeltとH. Geuvers著)」, Cambridge University Press（学内から閲覧可能）
参考書、講義資料等
講義のホームページを作成し、補助資料を配置する
成績評価の方法及び基準
実装（ソースコード）と理解度チェックに基づく
関連する科目
- MTH.A301 ： 代数学第一
- MTH.A302 ： 代数学第二
- MTH.A331 ： 代数学続論
履修の条件・注意事項
(1) 1つ以上のプログラミング言語で簡単なコードが書けること（必須）
(2) C++のコンパイラがあれば、参考に講師の実装をバイナリで渡すことができる（必須ではない）
(3) 大学数学の知識は必要としない