| 授業の目的 【日本語】 | | | 本講義では，プログラムに関する議論に欠くことの出来ない計算モデルの基礎を学ぶ。 |
|
|
| 授業の目的 【英語】 | | | In this lecture, we will learn the basis of computation modes, which is indispensable for discussion on programs. |
|
|
| 到達目標 【日本語】 | | プログラム検証などプログラムの性質を議論する上では，対象のプログラミング言語の意味を定義し，
その性質を扱うための理論的バックグランドを知ることが必要である。
本講義では，プログラムに関する議論に欠くことの出来ない計算モデルの基礎を学ぶ。
それを通じて，ネータ帰納法や辞書式順序などの理論的道具を理解し利用できるようにする。 |
|
|
| 到達目標 【英語】 | | 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 modes, which is indispensable for discussion on programs.
We will also discuss and practice theoretical tools such as Noetherian induction and the lexicographic ordering. |
|
|
| 授業の内容や構成 | | 具体的な計算モデルとして項書換え系に注目し，その基礎をなす等式推論系，ならびに，停止性や合流性などの書換え系の諸性質を理解する。
課題として与えられた証明問題などを解くことを通じて理論的な問題解決能力を涵養する。
〔計画〕
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 |
|
|
| 履修条件・関連する科目 | | |
|
| 成績評価の方法と基準 | | | 講義中に与える演習課題の評価４０％，期末試験６０％，合計１００点満点で６０点以上を合格とする。 | | Exercises(40%), examination(60%) |
|
|
| 教科書・参考書 | | | 必要に応じて配布する。 | | Handouts are distributed as necessary. |
|
|
| 課外学習等（授業時間外学習の指示） | | | 講義において説明した理論を理解し，活用できるようにするために課題を与える。 | | Excercises are given for better understanding. |
|
|
| 授業開講形態等 | | |
|
| 遠隔授業（オンデマンド型）で行う場合の追加措置 | | |
|