理工学研究科Graduate School of Science and Engineering
COT500X3（計算基盤 / Computing technologies 500）プログラム意味論特論Programming Language Semantics
藤田 憲悦Kenetsu FUJITA
授業コードなどClass code etc
| 学部・研究科Faculty/Graduate school | 理工学研究科Graduate School of Science and Engineering |
| 添付ファイル名Attached documents | |
| 年度Year | 2023 |
| 授業コードClass code | YB028 |
| 旧授業コードPrevious Class code | |
| 旧科目名Previous Class title | |
| 開講時期Term | 春学期授業/Spring |
| 曜日・時限Day/Period | 月4/Mon.4 |
| 科目種別Class Type | |
| キャンパスCampus | 小金井 |
| 教室名称Classroom name | 各学部・研究科等の時間割等で確認 |
| 配当年次Grade | |
| 単位数Credit(s) | |
| 備考（履修条件等）Notes | |
| 実務経験のある教員による授業科目Class taught by instructors with practical experience | |
| カテゴリーCategory | 応用情報工学専攻 |
すべて開くShow all
すべて閉じるHide All
Outline (in English)
The aim of this course is to give an introduction to the formal semantics of programming languages. The goals of this course are to understand the principles of programming languages and the practical foundations. Students will be expected to have the relevant chapters from the text including the course notes. Your study time will be more than one hour for a class. Grading will be decided based on reports (50%) and/or term-end examination (50%).
授業で使用する言語Default language used in class
日本語 / Japanese
授業の概要と目的（何を学ぶか）Outline and objectives
最初に、述語論理の意味論と証明論の基礎を学ぶ。これは、プログラム意味論とその応用の一つであるプログラム検証にとって不可欠である。次にこれに基づいて、公理的意味論、表示的意味論、プログラムの不動点定理などを習得して、プログラミング言語の理論を理解する。
到達目標Goal
つぎの項目の習得をゴールとする
(1) 一階述語論理の意味論
(2) 一階述語論理の証明論
(3) 形式的体系NKの健全性と完全性（Gödelの完全性定理）
(4) 帰納法の原理、様々な帰納法、帰納法の証明と再帰的プログラム
(5) 公理的意味論
(6) 表示的意味論
(7) CPOとCPO上の連続関数
(8) プログラムの不動点意味論（最小不動点定理）
この授業を履修することで学部等のディプロマポリシーに示されたどの能力を習得することができるか（該当授業科目と学位授与方針に明示された学習成果との関連）Which item of the diploma policy will be obtained by taking this class?
ディプロマポリシーのうち、「DP1」「DP2」「DP3」に関連
授業で使用する言語Default language used in class
日本語 / Japanese
授業の進め方と方法Method(s)（学期の途中で変更になる場合には、別途提示します。 /If the Method(s) is changed, we will announce the details of any changes. ）
講義形式であり、テキストとスライドの両方を利用する。定理証明などに関するプログラミングの課題を活用することもある。対面での開講に変更される可能性がある。この場合の授業方法・授業計画、成績評価方法の変更などについては、課題等の提出・フィードバック等の仕方も含め学習支援システムまたは授業中に別途指示する。授業中に小問を質問することがあるので授業中に必ず解答のこと。
アクティブラーニング（グループディスカッション、ディベート等）の実施Active learning in class (Group discussion, Debate.etc.)
なし / No
フィールドワーク（学外での実習等）の実施Fieldwork in class
なし / No
授業計画Schedule
授業形態/methods of teaching：オンライン/online
※各回の授業形態は予定です。教員の指示に従ってください。
第1回[オンライン/online]：プログラム意味論：プログラミング言語の理論
プログラミング言語の役割、意味論的手法と証明論的手法、数理論理学：意味論と証明論、プログラミング言語の意味論、プログラムの意味関数とコンピュータの状態
第2回[オンライン/online]：述語論理への準備
命題論理の復習：意味論と証明論
第3回[オンライン/online]：形式的体系NK
NKの健全性と完全性：ブール代数、真理値表と排中律、ワンのアルゴリズム
第4回[オンライン/online]：帰納法の原理
最小数の原理，数学的帰納法、累積帰納法、整礎な関係とネーター帰納法、構造帰納法、計算帰納法，不動点帰納法
第5回[オンライン/online]：述語論理の意味論
構造と解釈
第6回[オンライン/online]：述語論理の証明論
NKの推論規則と証明図
第7回[オンライン/online]：NKの健全性と完全性
Shutteの分解法とGödelの完全性定理
第8回[オンライン/online]：公理的意味論
Naur-Floydの帰納的表明法、Hoare論理、プログラム検証：部分正当性と停止性
第9回[オンライン/online]：表示的意味論
手続き型プログラムから関数型プログラムへの変換
第10回[オンライン/online]：連続関数の不動点定理
半順序構造と近似の概念、CPOとCPO上の連続関数
第11回[オンライン/online]：複合データ領域
直積と関数空間
第12回[オンライン/online]：プログラムの不動点意味論
再帰プログラムの不動点意味論
第13回[オンライン/online]：プログラミング言語の理論再考
証明論と定理証明、意味論とモデル検査
第14回[オンライン/online]：総まとめと課題
プログラム検証技術
授業時間外の学習（準備学習・復習・宿題等）Work to be done outside of class (preparation, etc.)
【本授業の準備・復習時間は、各４時間を標準とします。】
スライドや課題の復習、テキストの予習に取り組む
テキスト（教科書）Textbooks
「数理パズルで楽しく学べる論理学」(藤田)コロナ社 (2022) ２章：命題論理の意味論、形式的体系、健全性と完全性，及び３章：述語論理の言語、形式的体系、意味論。
https://www.coronasha.co.jp/np/isbn/9784339029239/
参考書References
小野寛晰：情報科学における論理、日本評論社(1994)
Dirk van Dalen：Logic and Structure、Fifth Edition、Springer(2004)
J.-Y.Girard, P.Taylor, Y.Lafont：Proofs and Types、Cambridge University Press(1989)
田辺、中島、長谷川：コンピュータサイエンス入門（論理とプログラム意味論）、岩波書店(1999)
中島玲二：数理情報学入門（スコット・プログラム理論）、朝倉書店(1982)
横内寛文：プログラム意味論、共立出版(1994)
成績評価の方法と基準Grading criteria
【評価方法】
レポート(50%)と定期試験(50%)による。
【評価基準】
本科目において設定した達成目標を60%以上達成している学生を合格とする。 対面での開講となった場合、成績評価の方法と基準も(レポート100%などに)変更する場合がある。その場合の具体的な方法と基準は、学習支援システムまたは授業中に提示する。
学生の意見等からの気づきChanges following student comments
特になし
学生が準備すべき機器他Equipment student needs to prepare
授業にはノートPCを持参すること
その他の重要事項Others
対面授業への移行などは学習支援システムを通じて連絡する。学習支援システムを通じた連絡がないかどうか確認を怠らないこと。