科目番号
教室
登録人数
履修登録方法
対面/遠隔
知能225
[水4]工1－321
65
抽選対象
対面授業
開講年度
期間
曜日時限
開講学部等
2020
後学期
水4
工学部工学科
講義コード
科目名[英文名]
単位数
617019002
言語理論とオートマトン
2
担当教員[ローマ字表記]
河野 真治
授業の形態
講義
アクティブラーニング
学生が文献や資料を調べる
授業内容と方法
この授業では、
計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。
オートマトンはCPUなどの状態を持つハードウェアを数学的に定義したもの。
正規表現を実際に使う場合の問題点に付いて調べる。
可能な状態遷移を一度に調べる非決定性オートマトン、 非決定性Turing Machine、
それらに基づく計算量のクラスであるNPを調べる。
Turing Machineの停止性を判定できないことを証明する。
無限の入力に対するオートマトンの性質の時相論理により記述する方法を学ぶ。
URGCC学習教育目標
情報リテラシー、問題解決力、専門性
達成目標
証明支援系であるAgda を使って、automaton を形式的に定義し性質を証明できるようになる。
オートマトンには
文字列の検索に使うキーワードの組合せや繰り返しを表す正規表現と同等の能力が
あることを理解する。
インタラクティブシステムの検証方法に付いて理解し、検証ツールを使えるようになる。
評価基準と評価方法
レポートにより判定する。
履修条件
授業計画
(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)」
ISBN
備考
http://www.sampou.org/haskell/tutorial-j/index.html
著者名
出版社
出版年
NCID
教科書
書名
Introduction to the Theory of Computation
ISBN
0-534-95097-3
備考
https://en.wikipedia.org/wiki/Introduction_to_the_Theory_of_Computation
著者名
Michael Sipser
出版社
出版年
NCID
教科書全体備考
参考書にかかわる情報
参考書全体備考
使用言語
日本語
メッセージ
オフィスアワー
メールアドレス
この項目は教務情報システムにログイン後、表示されます。
URL
http://www.ie.u-ryukyu.ac.jp/%7Ekono/automaton/
ページの先頭へ