オートマトンの概要
Menuオートマトンは自動的に動く人形という意味だが、ここでは文字列に対して自動的にできることを理論的に解析する。入力は有限の種類の文字が有限個並んだ文字列である。それを機械が読み込み、答えを返す。つまり、計算機そのものである。機械が文字列を返す場合もあるし、受け入れたかどうかを真偽で返す場合もある。機械はメモリと、メモリと入力によって次のメモリの状態が決まるとする。つまり、状態遷移機械(state transition)である。
この機械の様々な形の実装を調べて、それを比較する。また、受けれる文字列の集合を使って特徴づける。さらに、計算にかかるメモリと時間に付いて考察する。
証明と関数言語
証明は、命題の集まりと、それを結ぶ推論からなるネットワーク構造であることを学ぶ。関数言語は、集合である型と、それを結ぶ関数からなるネットワーク構造である。証明と関数言語が対応することを学び、証明を関数型言語(型つきλ計算)で表す。(カーリーハワード対応)
オートマトンの様々な概念をカーリーハワード対応に基づく証明支援系であるAgdaで記述しいていく。
いくつかの例題を通して、Agdaに慣れる。
実装方法による区別
決定性有限オートマトン
メモリが有限で、一文字読む毎に状態が進む
非決定性有限オートマトン
進む状態が複数ある
ε有限オートマトン
文字を読み込まないでも状態遷移することができるオートマトン
push down オートマトン
無限長のスタックを一つ持つオートマトン
Turing Machin
無限長のスタックを二つ(あるいはテープを一つ)持つオートマトン
文字列集合による区別
正規集合
文字の選択、文字の結合、そして、その繰り返しによって作られる文字列の集合
正規表現からオートマトンへの変換
正規表現の効率的な実装
決定性オートマトンと非決定性オートマトンの関係
Turing Machin の性質
万能 Turing Machin
Turing Machin の停止性
計算量
非決定性Turing MachineP と NP
時相論理とモデル検査
プログラムのInteractiveな仕様記述方法である時相論理を学び、そのモデルとして無限長の入力を扱うωオートマトンを使用する。オートマトンが時相論理式を満たしているかどうかを調べるモデル検査に付いて学ぶ。
SMVなどのモデル検査系を使えるようにする。