科目 : 情報論理学

科目詳細

2017
前期
半期
20DIFa01
情報論理学
情報学
2
専門領域
情報基礎科学
プログラミング言語や仕様記述に関して重要である型理論について、その初歩を、数学的に厳密に説明する。
(1)
型理論の初歩を数学的に厳密に理解すること。
(2)
型理論を実際のプログラミングの問題に応用できるようになること。
担当教員:龍田 真
開講日:火曜4限(14:45-16:15)

授業計画:
(1)
型理論の基礎となる最も簡単な型理論である単純型理論λ→をいろいろな角度から説明する。λ→の定義を与える。型理論に対して一般に定義できる性質としてサブジェクトリダクション性、強正規化性、主型の存在についてλ→を例に用いて説明する。λ→に対するこれらの性質を証明する。
(2)
プログラミング言語 ML の型理論について説明し、型推論のアルゴリズムを説明し、その正しさを証明する。
(3)
型理論 F を説明し、その強正規化性を証明する。
(4)
構成的自然演繹命題論理 NJ と、構成的自然演繹二階命題論理 NJ2 を説明する。その証明の正規化を定義する。カリーハワードの同型対応が型理論と論理体系の自然な対応を与えることを、λ→とNJ, F とNJ2 を例として説明する。
日本語または英語
授業の達成目標の(1)(2)が習得できたかどうかをレポートおよび授業中の質問により判定する。
1,2,3,4,5 学年
国立情報学研究所(NII):講義室1(12階1212号室)
教科書:なし
参考書:
[1]
龍田 真, 型理論 (近代科学社, 1992.11).
[2]
S. Abramsky, Dov M. Gabbay and T. S. E. Maibaum, "Handbook of logic in computer science" (Oxford University Press, 1992), Page 117--309.
ラムダ計算の知識をもっていることが望ましい
専攻

科目情報
履修年度
2017 / 前期
研究科・専攻
情報学
科目番号
20DIFa01
科目名称
情報論理学
単位
2
授業形態
設定なし
科目の概要
プログラミング言語や仕様記述に関して重要である型理論について、その初歩を、数学的に厳密に説明する。
聴講・参加資格
専攻
参加状態
参加できません
開催講義
参加可能講義なし