授業の形態
|
|
講義
|
| |
|
アクティブラーニング
|
|
学生が文献や資料を調べる
|
| |
|
授業内容と方法
|
この授業では、
計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。
オートマトンはCPUなどの状態を持つハードウェアを数学的に定義したもの。
正規表現を実際に使う場合の問題点に付いて調べる。
可能な状態遷移を一度に調べる非決定性オートマトン、 非決定性Turing Machine、
それらに基づく計算量のクラスであるNPを調べる。
Turing Machineの停止性を判定できないことを証明する。
無限の入力に対するオートマトンの性質の時相論理により記述する方法を学ぶ。
Zoom/MatterMost automaton 上でのonline授業
|
| |
|
URGCC学習教育目標
|
|
情報リテラシー、問題解決力、専門性
|
| |
|
達成目標
|
証明支援系であるAgda を使って、automaton を形式的に定義し性質を証明できるようになる。
オートマトンには
文字列の検索に使うキーワードの組合せや繰り返しを表す正規表現と同等の能力が
あることを理解する。
インタラクティブシステムの検証方法に付いて理解し、検証ツールを使えるようになる。
|
| |
|
評価基準と評価方法
|
課題について文献、資料を自ら調べたレポートにより判定する
Agdaでオートマトンの課題を記述できる
簡単な証明を型検査することができる
|
| |
|
履修条件
|
|
|
| |
|
授業計画
|
(1) オートマトンの概要
(2,3) Agdaによる数学的構造の定義と証明
(4)決定性オートマトン
(5)非決定性オートマトン
(6)正規表現
(7)正規表現とオートマトン
(8)非決定性オートマトンから決定性オートマトンへの変換
(9)push donwオートマトンと文法クラス
(10)Turing Machine
(11)Turing Machine と計算量の理論
(12)ω オートマトン
(13,14)時相論理とCTL
(15)モデル検査とSAT
|
| |
|
事前学習
|
特になし。
Webの資料を前もって公開する。
|
| |
|
事後学習
|
|
Web上に公開されたレポートについて解答する。
|
| |
|
教科書にかかわる情報
|
|
「やさしい Haskell 入門 (バージョン98)」
|
|
http://www.sampou.org/haskell/tutorial-j/index.html
|
|
|
|
|
|
|
|
|
0-534-95097-3
|
https://en.wikipedia.org/wiki/Introduction_to_the_Theory_of_Computation
|
|
Michael Sipser
|
|
|
|
|
|
|
| |
|
教科書全体備考
|
|
|
| |
|
参考書にかかわる情報
|
|
|
978-1970001242
|
ACM books, #9
|
|
Aaron Stump
|
|
Association for Computing Machinery : Morgan & Claypool Publishers
|
2016
|
|
|
|
| |
|
参考書全体備考
|
|
|
| |
|
使用言語
|
|
日本語
|
| |
|
メッセージ
|
|
|
| |
|
オフィスアワー
|
|
MatterMost で随時
|
| |
|
メールアドレス
|
|
この項目は教務情報システムにログイン後、表示されます。
|
| |
|
URL
|
|
http://www.ie.u-ryukyu.ac.jp/%7Ekono/automaton/
|
| |
|
|