授業の目的 【日本語】
Goals of the Course(JPN) | | | 本講義では、「計算理論」およびその論理学との結びつきについて学習する。計算理論は、1930年代にゲーデル、チャーチ、チューリング、ポストらによって計算可能性の定義が独立に定式化されたときに始まった。数理情報学9においてはこれらの計算モデルとその定式化の概要を学ぶことを第一の目的とする。特に、現代的な様々なプログラミング言語の基礎をなしている「ラムダ計算」を中心に、様々な計算モデル間の関係性について学び、さらに計算と論理の深い結び付きを与えるカリー・ハワード対応の基礎について学ぶ。 |
|
|
授業の目的 【英語】
Goals of the Course | | | In this lecture, we will learn about "computation theory" and its connection to logic. The theory of computation began in the 1930s when the definition of computability was independently formulated by Gödel, Church, Turing, and Post. In Mathematical Informatics 9, the primary objective is to learn these models of computation and an overview of their formulations. In particular, we will learn about the relationships among various computational models, with a focus on "lambda calculus" that forms the basis of various modern programming languages, and we will also learn about the basics of the Curry-Howard correspondence that provides a deep connection between computation and logic. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 計算可能性理論は，20世紀前半にゲーデルが不完全性定理の証明に用いた（自然数上の）再帰的関数の定式化に始まり，続けてチャーチ，チューリング，ポストらがそれと同等な計算モデルを様々に考案した結果，計算可能性の普遍性が確立された。この講義ではそれらの計算モデルとその定式化の概要を学ぶことを第一の目的とする。 |
|
|
到達目標 【英語】
Objectives of the Course | | | Computability theory began in the first half of the 20th century with Gödel's formulation of recursive functions (on natural numbers) used in the proof of the incompleteness theorem, and was followed by Church, Turing, and Post, who devised various equivalent computational models, thus establishing the universality of the notion of computability. The primary purpose of this lecture is to give an overview of these computational models and their formulations. |
|
|
授業の内容や構成
Course Content / Plan | | 数理情報学9においては計算可能性の定義を原始的なプログラム等（ラムダ計算やコンビネータ）を使って導入し，それと原始帰納的関数（再帰的関数）の関係を調べながら計算可能性理論の基礎を学習する。
1. チャーチ・チューリングの提唱
2. コンビネータ論理
3. 型なしラムダ計算と計算可能性
4. ラムダ表現可能性と再帰的関数
5. ライスの定理とクリーネの再帰定理
6. 単純型付きラムダ計算
7. カリー・ハワード対応
8. 総括 | |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | |
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 講義中に与える演習課題の評価30％，期末レポート70％，合計100点満点で60点以上を合格とする。 | |
|
|
教科書・参考書
Textbook/Reference book | | 必要に応じて参考資料を配布する。
参考書としては以下を紹介しておく。
大堀 淳 著「プログラミング言語の基礎理論」
Benjamin C. Pierce著「型システム入門 プログラミング言語と型の理論」 | |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 講義において説明した理論を理解するために課題を与える。 | |
|
|
授業開講形態等
Lecture format, etc. | | |
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|