|
0
|
1 -title: オートマトン
|
|
|
2
|
|
24
|
3 この授業では、
|
|
|
4 計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。
|
|
|
5 オートマトンはCPUなどの状態を持つハードウェアを数学的に定義したもの。
|
|
|
6 正規表現を実際に使う場合の問題点に付いて調べる。
|
|
|
7 可能な状態遷移を一度に調べる非決定性オートマトン、 非決定性Turing Machine、
|
|
|
8 それらに基づく計算量のクラスであるNPを調べる。
|
|
|
9 Turing Machineの停止性を判定できないことを証明する。
|
|
|
10 無限の入力に対するオートマトンの性質の時相論理により記述する方法を学ぶ。
|
|
|
11
|
|
|
12 -- 達成目標
|
|
0
|
13
|
|
24
|
14 証明支援系であるAgda を使って、automaton を形式的に定義し性質を証明できるようになる。
|
|
|
15 オートマトンには
|
|
|
16 文字列の検索に使うキーワードの組合せや繰り返しを表す正規表現と同等の能力が
|
|
|
17 あることを理解する。
|
|
|
18 インタラクティブシステムの検証方法に付いて理解し、検証ツールを使えるようになる。
|
|
|
19
|
|
|
20 -- 教科書
|
|
|
21
|
|
|
22 Introduction to the Theory of Computation
|
|
|
23 ISBN 0-534-95097-3
|
|
|
24 https://en.wikipedia.org/wiki/Introduction_to_the_Theory_of_Computation
|
|
0
|
25
|
|
|
26 -- 参考書
|
|
|
27
|
|
|
28 <a href="http://www.sampou.org/haskell/tutorial-j/index.html">
|
|
|
29 「やさしい Haskell 入門 (バージョン98)」
|
|
|
30 </a>
|
|
|
31
|
|
65
|
32 --Agdaのinstall 方法
|
|
|
33
|
|
|
34 <a href="a02/agda-install.html"> ここを参照 </a>
|
|
|
35
|
|
141
|
36 --Agdaの記述
|
|
|
37
|
|
|
38 <a href="agda/index.html"> 2020 </a><br>
|
|
|
39 <a href="agda-2.6.2/index.html"> 2019 </a>
|
|
0
|
40
|
|
|
41 -- 評価方法
|
|
24
|
42
|
|
|
43 レポートにより判定する。
|
|
0
|
44
|
|
|
45 --授業計画
|
|
|
46
|
|
|
47 <ol>
|
|
24
|
48 <li><a href="a01/lecture.html"> オートマトンの概要</a>
|
|
|
49 <li><a href="a02/lecture.html"> Agdaによる数学的構造の定義と証明</a>
|
|
|
50 <li><a href="a03/lecture.html"> 決定性オートマトン</a>
|
|
|
51 <li><a href="a04/lecture.html"> 非決定性オートマトン </a>
|
|
|
52 <li><a href="a05/lecture.html"> 正規表現</a>
|
|
|
53 <li><a href="a06/lecture.html"> 正規表現とオートマトン </a>
|
|
|
54 <li><a href="a07/lecture.html"> 非決定性オートマトンから決定性オートマトンへの変換</a>
|
|
|
55 <li><a href="a08/lecture.html"> push donwオートマトンと文法クラス</a>
|
|
|
56 <li><a href="a09/lecture.html"> Turing Machine</a>
|
|
|
57 <li><a href="a10/lecture.html"> Turing Machine と計算量の理論</a>
|
|
|
58 <li><a href="a11/lecture.html"> ω オートマトン</a>
|
|
|
59 <li><a href="a12/lecture.html"> 時相論理とCTL</a>
|
|
|
60 <li><a href="a13/lecture.html"> モデル検査とSAT</a>
|
|
0
|
61 </ol>
|
|
|
62
|
|
24
|
63 電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。
|
|
0
|
64
|
|
55
|
65 問題に関しては、問題ごとに別なメールで、以下のタイトルで
|
|
|
66 Subject: Automaton Lecture Exercise 1.1
|
|
|
67 kono@ie.u-ryukyu.ac.jp まで送ること。
|
|
|
68
|
