|
授業科目： 計算論理 （２単位） Computational Logic |
対象： ３・４学年 | |
|---|---|---|
| 第３学期 | 曜・時： 木２・３ | 担当教官: 亀山幸義 |
週別授業計画
教材：
講義のホームページ(下記)を通じて 講義ノートを公開する．
概要：
多くの現代的プログラム言語は，強力な型システムを持つことにより データ構造や制御構造の抽象化を果たし，プログラムの誤りを減らしたり， 可読性を高めることに役に立っている． 本講義では，型システムの理論的背景を知るため 「型つきラムダ計算 (typed lambda calculus)」の体系に基づいた プログラム言語の基礎理論を学ぶ． プログラム言語の構文と意味の厳密な定義方法， 型システム，計算規則などについて学ぶ． また，型つきラムダ計算に対応する直観主義論理の体系を取り上げ， これら２つの体系が本質的に等価であること，すなわち， 証明とプログラムが同一視できることを学ぶ． これらを通じて形式的体系とは何かを理解し， 形式的対象の操作が計算機で実行可能なことを学ぶ． 授業の中でソフトウェアを用いた演習を行う．
学習・教育目標：
授業計画：
| 週 | 講義内容 |
|---|---|
| 第1週 | 導入: ラムダ計算，命題論理，構文論と意味論，形式化 |
| 第2-4週 | 計算の論理： 命題の構成，導出， 直観主義論理と構成的解釈，導出の計算， ソフトウェアを使った演習 |
| 第5-7週 | 型付きラムダ計算: 項と型，導出，計算，性質， ソフトウェアを使った演習 |
| 第8-9週 | 計算と論理： カリーハワードの同型対応 |
| 第10週 | 型システムの応用・発展 |
参考書等：
プログラムの基礎理論（佐藤雅彦・桜井貴文共著，岩波書店）
ソフトウェア科学のための論理学（萩谷昌己著，岩波書店）
S. Thompson, "Type Theory and Functional Programming", Addison-Wesley,
1991.
Benjamine C. Pierce, "Types and Programming Languages", MIT Press, 2002.
予備知識・前提条件：
命題論理の基礎的事項
オフィスアワー：
金11:00〜12:30, 総合研究棟B棟1008
成績評価：
出席，授業中に実施する演習，学期末試験を総合して評価する．
講義のホームページ：
http://logic.cs.tsukuba.ac.jp/~kam/complogic/
教官メールアドレス：
亀山: kamの後にアットマーク，その後に ｃｓ．ｔｓｕｋｕｂａ．ａｃ．ｊｐ