-title: オートマトン

この授業では、
計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。
オートマトンは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

-- 参考書

<a href="http://www.sampou.org/haskell/tutorial-j/index.html">
「やさしい Haskell 入門 (バージョン98)」
</a> 

--Agdaのinstall 方法

<a href="a02/agda-install.html"> ここを参照 </a>

--Agdaの記述

<a href="https://github.com/shinji-kono/automaton-in-agda"> github  </a><br>

-- 評価方法

レポートにより判定する。

--授業計画

<ol>
<li><a href="a01/lecture.html"> オートマトンの概要</a>
<li><a href="a02/lecture.html"> Agdaによる数学的構造の定義と証明</a>
<li><a href="a02/sumtype.html"> Sum type または data </a>
<li><a href="a03/lecture.html"> 決定性オートマトン</a> 
<li><a href="a04/lecture.html"> 非決定性オートマトン </a>
<li><a href="a05/lecture.html"> 正規表現</a> 
<li><a href="a06/lecture.html"> 正規表現とオートマトン  </a> 
<li><a href="a07/lecture.html"> 非決定性オートマトンから決定性オートマトンへの変換</a> 
<li><a href="a08/lecture.html"> push donwオートマトンと文法クラス</a> 
<li><a href="a09/lecture.html"> Turing Machine</a> 
<li><a href="a10/lecture.html"> Turing Machine と計算量の理論</a> 
<li><a href="a11/lecture.html"> ω オートマトン</a> 
<li><a href="a12/lecture.html"> 時相論理とCTL</a> 
<li><a href="a13/lecture.html"> モデル検査とSAT</a> 
</ol>

電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。

問題に関しては、問題ごとに別なメールで、以下のタイトルで
    Subject: Automaton Lecture Exercise 1.1
kono@ie.u-ryukyu.ac.jp まで送ること。

--Zotero

論文管理用のソフトウェア

https://www.zotero.org