授業の目的 【日本語】
Goals of the Course(JPN) | | プログラム検証などプログラムの性質を議論する上では，対象のプログラミング言語の意味を定義し，その性質を扱うための理論的バックグランドを知ることが必要である。
本講義では，プログラムに関する議論に欠くことの出来ない計算モデルの基礎を学ぶ。 |
|
|
授業の目的 【英語】
Goals of the Course | | | It is necessary to define the semantics of objective languages and to understand their theoretical backround in order to discuss properties of programs such as program verification. In this lecture, we will learn the basis of computation models, which is indispensable for discussion on programs. |
|
|
到達目標 【日本語】
Objectives of the Course(JPN) | | | 計算モデルの基礎概念を理解し，ネータ帰納法や辞書式順序などの理論的道具を活用できる。 |
|
|
到達目標 【英語】
Objectives of the Course | | | Goal of this class is to understand basic notions of computation models, and to utilize theoretical tools such as Noetherian induction and the lexicographic ordering. |
|
|
授業の内容や構成
Course Content / Plan | | 具体的な計算モデルとして項書換え系に注目し，その基礎をなす等式推論系，ならびに，停止性や合流性などの書換え系の諸性質を理解する。
課題として与えられた証明問題などを解くことを通じて理論的な問題解決能力を涵養する。
〔計画〕
1. 抽象書換え系
2. 語問題
3. ネータ帰納法と停止性
4. 合流性
5. 完備化 | Focusing on term rewriting systems as a specific computation model, we will study their underlying equational theory, and propeties of rewriting systems such as the termination and/or confluence.
We will also train theoretical problem solving ability through exercises.
1. Abstract reduction systems
2. Word problems
3. Noetherian induction and termination
4. Confluence
5. Completion |
|
|
履修条件・関連する科目
Course Prerequisites and Related Courses | | | 離散数学、および、数理論理学の知識を有することが望ましい。 | |
|
|
成績評価の方法と基準
Course Evaluation Method and Criteria | | | 課外学習のレポート４０％，期末試験６０％で評価する。２回以上のレポート未提出者，もしくは，期末試験欠席者は「W（欠席）」とする。 | |
|
|
教科書・参考書
Textbook/Reference book | | | 授業で用いるスライドのハンドアウトをWEB上に用意する。 | |
|
|
課外学習等（授業時間外学習の指示）
Study Load(Self-directed Learning Outside Course Hours) | | | 講義において説明した理論を理解し，活用できるようにするために課題を与える。 | | Excercises are given for better understanding. |
|
|
授業開講形態等
Lecture format, etc. | | | 原則対面にて実施する。詳細はTACTの講義ページを通じて通知する。 |
|
|
遠隔授業（オンデマンド型）で行う場合の追加措置
Additional measures for remote class (on-demand class) | | |
|