|
学科(専攻)・科目の種別等
|
基盤理学 数学情報数理学コース ・・・・・・・・・・・・・・・ |
授業コード Class Code |
S21122001 | 科目コード Course Code |
S211220 |
| 授業の方法 Course Type |
単位数 Credits |
2 | |||
| 期別 Semester Offered |
前期 | 曜日・時限 Day & Period |
月３ | ||
| 授業科目 Course Title |
情報論理学I |
||||
| Mathematical Logic for Computer Sciences I | |||||
| 担当教員 Instructor |
桜井 貴文,山本 光晴,新井 敏康 | ||||
| 概要 Brief Description |
計算機プログラムのモデルでもあるラムダ計算はカリー・ハワードの対応などにより数理論理学との深い関係が知られている。ここでは単純型付ラムダ計算を取り上げ、その構文論と意味論についての基礎的な部分を論じる。 | ||||
| 目的・目標 Objectives and Goals |
ラムダ計算は計算機プログラムのモデルであるが、その中でも単純型付ラムダ計算は最も基本的なものである。この講義では、単純型付ラムダ計算の基本的な性質を理解し、その性質がプログラムの性質を考えるときにも重要であることを理解することを目標とする。 | ||||
| 授業計画・授業内容 Course Plans and Contents |
1. 単純型付ラムダ計算の定義 2. 単純型付ラムダ計算の表示的意味論 3. 単純型付ラムダ計算の公理的意味論 4. 公理的意味論の健全性と完全性 5. 単純型付ラムダ計算の操作的意味論 (評価文脈と自然意味論) 6. 型付ラムダ計算の拡張 |
||||
| 教科書・参考書 Textbooks/Reference Books |
教科書 大堀淳「プログラミング言語の基礎理論」共立出版 |
||||
| 評価方法・基準 Evaluation Procedures and Criteria |
試験またはレポート(発表)にによって成績の評価を行なう。 単純型付ラムダ計算の構文と意味の関係(特に健全性)、および操作的意味論の表現の仕方を理解できていることが合格の要件である。 |
||||
