オートマトン
Menuこの授業では、計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。オートマトンはCPUなどの状態を持つハードウェアを数学的に定義したもの。正規表現を実際に使う場合の問題点に付いて調べる。可能な状態遷移を一度に調べる非決定性オートマトン、 非決定性Turing Machine、それらに基づく計算量のクラスであるNPを調べる。Turing Machineの停止性を判定できないことを証明する。無限の入力に対するオートマトンの性質の時相論理により記述する方法を学ぶ。
達成目標
証明支援系であるAgda を使って、automaton を形式的に定義し性質を証明できるようになる。オートマトンには文字列の検索に使うキーワードの組合せや繰り返しを表す正規表現と同等の能力があることを理解する。インタラクティブシステムの検証方法に付いて理解し、検証ツールを使えるようになる。
教科書
Introduction to the Theory of Computation ISBN 0-534-95097-3 https://en.wikipedia.org/wiki/Introduction_to_the_Theory_of_Computation
参考書
「やさしい Haskell 入門 (バージョン98)」
Agdaのinstall 方法
ここを参照Agdaの記述
github評価方法
レポートにより判定する。
授業計画
- オートマトンの概要
- Agdaによる数学的構造の定義と証明
- Sum type または data
- 決定性オートマトン
- 非決定性オートマトン
- 正規表現
- 正規表現とオートマトン
- 非決定性オートマトンから決定性オートマトンへの変換
- push donwオートマトンと文法クラス
- Turing Machine
- Turing Machine と計算量の理論
- ω オートマトン
- 時相論理とCTL
- モデル検査とSAT
電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。
問題に関しては、問題ごとに別なメールで、以下のタイトルで
Subject: Automaton Lecture Exercise 1.1
kono@ie.u-ryukyu.ac.jp まで送ること。
Zotero
論文管理用のソフトウェアhttps://www.zotero.org