2020年度学院等開講科目情報理工学院数理・計算科学系数理・計算科学コース

論理と計算

開講元: 数理・計算科学コース
担当教員: 鹿島亮 / 西崎真也
授業形態: 講義 (ZOOM)
メディア利用科目: -
曜日・時限 (講義室): 火1-2 (W833) / 金1-2 (W833)
クラス: -
科目コード: MCS.T416
単位数: 200
開講時期: 2020年度
開講クォーター: 1Q
シラバス更新日: 2025年7月10日
使用言語: 英語

シラバス

授業の目的（ねらい）、概要

ソフトウエアの基礎理論と数理論理学には概念や手法に共通部分が多い。たとえば「プログラム」と「証明」とは本質的に同じものである，という見方ができる（カリー・ハワード同型対応）。本講義のねらいはそのようなソフトウエア基礎理論と数理論理学の共通部分を明らかにすることである。
具体的には古典論理と直観主義論理の自然演繹，シークエント計算，そしてラムダ計算の基本的な性質を学ぶ。

到達目標

ソフトウエアの基礎理論における数理論理学的な概念や手法を身に付ける。

キーワード

カリー・ハワード同型対応，ラムダ計算，古典論理，直観主義論理，自然演繹，シークエント計算

学生が身につける力

専門力
教養力
コミュニケーション力
展開力 (探究力又は設定力)
展開力 (実践力又は解決力)

授業の進め方

講義による。
３回程度の宿題を課す。

授業計画・課題

	授業計画	課題
第1回	論理学の導入。論理式。	授業時に指示する。
第2回	論理式の真理値。	授業時に指示する。
第3回	自然演繹。	授業時に指示する。
第4回	シークエント計算。	授業時に指示する。
第5回	古典論理の完全性。	授業時に指示する。
第6回	直観主義論理の完全性。	授業時に指示する。
第7回	直観主義論理の性質。	授業時に指示する。
第8回	ラムダ計算の導入。	授業時に指示する。
第9回	ラムダ計算の能力。	授業時に指示する。
第10回	チャーチロッサー性。	授業時に指示する。
第11回	コンビネータ論理の導入。	授業時に指示する。
第12回	コンビネータ論理の性質。	授業時に指示する。
第13回	カリー・ハワード同型対応。	授業時に指示する。
第14回	型体系の性質。	授業時に指示する。

準備学修(事前学修・復習)等についての指示

学修効果を上げるため，教科書や配布資料等の該当箇所を参照し，「毎授業」授業内容に関する予習と復習（課題含む）をそれぞれ概ね100分を目安に行うこと。

教科書

Dirk van Dalen: Logic and Structure, Fourth Edition (Corrected 2nd printing 2008).
Henk Barendregt, Erik Barendsen: Introduction to Lambda Calculus (Revised edition December 1998, March 2000).
(Both are downloadable from the internet.)

参考書、講義資料等

授業時に指示する。

成績評価の方法及び基準

宿題による。

履修の条件・注意事項

MCS.T404「計算論理学」を履修済の学生は履修不可。