# HG changeset patch # User Shinji KONO # Date 1541372028 -32400 # Node ID 9406c2571fe7e46c6346633be1d50148596f2a91 # Parent 0c3054704de7dd9bbb9eb724dd675a15cbd1b847 naccept1 diff -r 0c3054704de7 -r 9406c2571fe7 agda/automaton.agda --- a/agda/automaton.agda Mon Sep 17 20:43:59 2018 +0900 +++ b/agda/automaton.agda Mon Nov 05 07:53:48 2018 +0900 @@ -1,10 +1,10 @@ module automaton where -open import Level renaming ( suc to succ ; zero to Zero ) +-- open import Level renaming ( suc to succ ; zero to Zero ) open import Data.Nat open import Data.List open import Data.Maybe -open import Data.Bool using ( Bool ; true ; false ) +open import Data.Bool using ( Bool ; true ; false ; _∧_ ) open import Relation.Binary.PropositionalEquality hiding ( [_] ) open import Relation.Nullary using (¬_; Dec; yes; no) @@ -26,13 +26,6 @@ i0 : In2 i1 : In2 - -ieq : (i i' : In2 ) → Dec ( i ≡ i' ) -ieq i0 i0 = yes refl -ieq i1 i1 = yes refl -ieq i0 i1 = no ( λ () ) -ieq i1 i0 = no ( λ () ) - moves : { Q : Set } { Σ : Set } → Automaton Q Σ → Q → List Σ → Q @@ -40,7 +33,7 @@ where move : (q : Q ) ( L : List Σ ) → Q move q [] = q - move q ( H ∷ T ) = move ( (δ M) q H ) T + move q ( H ∷ T ) = move ( δ M q H) T accept : { Q : Set } { Σ : Set } → Automaton Q Σ @@ -61,7 +54,8 @@ fin1 : States1 → Bool fin1 st = true -fin1 _ = false +fin1 ss = false +fin1 sr = false am1 : Automaton States1 In2 am1 = record { δ = transition1 ; astart = sr ; aend = fin1 } @@ -78,67 +72,9 @@ example1-3 = reachable am1 st ( i1 ∷ i1 ∷ i1 ∷ [] ) -s1id : States1 → ℕ -s1id sr = 0 -s1id ss = 1 -s1id st = 2 - -record NAutomaton ( Q : Set ) ( Σ : Set ) - : Set where - field - nδ : Q → Σ → List Q - sid : Q → ℕ - nstart : Q - nend : Q → Bool - -open NAutomaton - -insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q -insert M [] q = q ∷ [] -insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') -... | yes _ = insert M T q' -... | no _ = q ∷ (insert M T q' ) - -merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q -merge M L1 [] = L1 -merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H +ieq : (i i' : In2 ) → Dec ( i ≡ i' ) +ieq i0 i0 = yes refl +ieq i1 i1 = yes refl +ieq i0 i1 = no ( λ () ) +ieq i1 i0 = no ( λ () ) -Nmoves : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → List Q → List Σ → List Q -Nmoves {Q} { Σ} M q L = Nmoves1 q L [] - where - Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q - Nmoves1 q [] _ = q - Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] - Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) - - -Naccept : { Q : Set } { Σ : Set } - → NAutomaton Q Σ - → List Σ → Bool -Naccept {Q} { Σ} M L = - checkAccept ( Nmoves M ((nstart M) ∷ [] ) L ) - where - checkAccept : (q : List Q ) → Bool - checkAccept [] = false - checkAccept ( H ∷ L ) with (nend M) H - ... | true = true - ... | false = checkAccept L - - -transition2 : States1 → In2 → List States1 -transition2 sr i0 = (sr ∷ []) -transition2 sr i1 = (ss ∷ sr ∷ [] ) -transition2 ss i0 = (sr ∷ []) -transition2 ss i1 = (st ∷ []) -transition2 st i0 = (sr ∷ []) -transition2 st i1 = (st ∷ []) - -am2 : NAutomaton States1 In2 -am2 = record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1} - - -example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] ) -example2-2 = Naccept am2 ( i1 ∷ i1 ∷ i1 ∷ [] ) - diff -r 0c3054704de7 -r 9406c2571fe7 agda/nfa-list.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/nfa-list.agda Mon Nov 05 07:53:48 2018 +0900 @@ -0,0 +1,96 @@ +module nfa-list where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat +open import Data.List +open import Data.Maybe +open import Data.Bool using ( Bool ; true ; false ) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Nullary using (¬_; Dec; yes; no) + + +data States1 : Set where + sr : States1 + ss : States1 + st : States1 + +data In2 : Set where + i0 : In2 + i1 : In2 + +transition1 : States1 → In2 → States1 +transition1 sr i0 = sr +transition1 sr i1 = ss +transition1 ss i0 = sr +transition1 ss i1 = st +transition1 st i0 = sr +transition1 st i1 = st + +fin1 : States1 → Bool +fin1 st = true +fin1 _ = false + +s1id : States1 → ℕ +s1id sr = 0 +s1id ss = 1 +s1id st = 2 + +record NAutomaton ( Q : Set ) ( Σ : Set ) + : Set where + field + nδ : Q → Σ → List Q + sid : Q → ℕ + nstart : Q + nend : Q → Bool + +open NAutomaton + +insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q +insert M [] q = q ∷ [] +insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q') +... | yes _ = insert M T q' +... | no _ = q ∷ (insert M T q' ) + +merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q +merge M L1 [] = L1 +merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H + +Nmoves : { Q : Set } { Σ : Set } + → NAutomaton Q Σ + → List Q → List Σ → List Q +Nmoves {Q} { Σ} M q L = Nmoves1 q L [] + where + Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q + Nmoves1 q [] _ = q + Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L [] + Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ ) + + +Naccept : { Q : Set } { Σ : Set } + → NAutomaton Q Σ + → List Σ → Bool +Naccept {Q} { Σ} M L = + checkAccept ( Nmoves M ((nstart M) ∷ [] ) L ) + where + checkAccept : (q : List Q ) → Bool + checkAccept [] = false + checkAccept ( H ∷ L ) with (nend M) H + ... | true = true + ... | false = checkAccept L + + +transition2 : States1 → In2 → List States1 +transition2 sr i0 = (sr ∷ []) +transition2 sr i1 = (ss ∷ sr ∷ [] ) +transition2 ss i0 = (sr ∷ []) +transition2 ss i1 = (st ∷ []) +transition2 st i0 = (sr ∷ []) +transition2 st i1 = (st ∷ []) + +am2 : NAutomaton States1 In2 +am2 = record { nδ = transition2 ; sid = s1id ; nstart = sr ; nend = fin1} + + +example2-1 = Naccept am2 ( i0 ∷ i1 ∷ i0 ∷ [] ) +example2-2 = Naccept am2 ( i1 ∷ i1 ∷ i1 ∷ [] ) + diff -r 0c3054704de7 -r 9406c2571fe7 agda/omega-automaton.agda --- a/agda/omega-automaton.agda Mon Sep 17 20:43:59 2018 +0900 +++ b/agda/omega-automaton.agda Mon Nov 05 07:53:48 2018 +0900 @@ -118,12 +118,10 @@ next n | ts | false = 1 next n | ts* | true = 2 next n | ts* | false = 1 + infinite' : (n m : ℕ) → n ≥″ m → aend ωa2 (ω-run ωa2 (m + (next m)) flip-seq) ≡ true → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true + infinite' = {!!} infinite : (n : ℕ) → aend ωa2 (ω-run ωa2 (n + (next n)) flip-seq) ≡ true - infinite n with ω-run ωa2 n flip-seq | flip-seq n | - infinite n | ts | true = {!!} - infinite n | ts | false = {!!} - infinite n | ts* | true = {!!} - infinite n | ts* | false = {!!} + infinite = {!!} lemma3 : Buchi ωa1 false-seq → ⊥ lemma3 = {!!} diff -r 0c3054704de7 -r 9406c2571fe7 agda/regop.agda --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/regop.agda Mon Nov 05 07:53:48 2018 +0900 @@ -0,0 +1,34 @@ +module regop where + +open import automaton + +-- open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat +open import Data.List +open import Data.Maybe +open import Data.Product +open import Data.Bool using ( Bool ; true ; false ; _∧_ ) +open import Relation.Binary.PropositionalEquality hiding ( [_] ) +open import Relation.Nullary using (¬_; Dec; yes; no) + + +union : {Q1 Q2 Σ : Set } → ( M1 : Automaton Q1 Σ) ( M2 : Automaton Q2 Σ) → Automaton (Q1 × Q2) Σ +union {Q1} {Q2} {Σ} M1 M2 = record { + δ = δ + ; astart = astart + ; aend = aend + } where + δ : (Q1 × Q2) → Σ → (Q1 × Q2) + δ = {!!} + astart : (Q1 × Q2) + astart = {!!} + aend : (Q1 × Q2) → Bool + aend = {!!} + +data _∨_ (A B : Set) : Set where + p1 : A → A ∨ B + p2 : B → A ∨ B + +union← : {Q1 Q2 Σ : Set } → ( M1 : Automaton Q1 Σ) ( M2 : Automaton Q2 Σ) → + ∀ ( s : List Σ ) → accept ( union M1 M2 ) s ≡ true → ( ( accept M1 s ≡ true ) ∨ ( accept M2 s ≡ true) ) +union← {Q1} {Q2} {Σ} M1 M2 s eq = {!!} diff -r 0c3054704de7 -r 9406c2571fe7 index.ind --- a/index.ind Mon Sep 17 20:43:59 2018 +0900 +++ b/index.ind Mon Nov 05 07:53:48 2018 +0900 @@ -1,7 +1,27 @@ -title: オートマトン -この授業では、Agda を使って、計算機科学の基礎であるオートマトンとチューリングマシンについえ学びます。 +この授業では、 +計算機科学の基礎であるオートマトンとチューリングマシンについて学ぶ。 +オートマトンは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 -- 参考書 @@ -9,76 +29,28 @@ 「やさしい Haskell 入門 (バージョン98)」 - -すごい Haskell Miran Lipova - - - -達人プログラマー -アンドリュー ハント、デビッド トーマス (ピアソン・エデュケーション) - オブジェクト指向における再利用のためのデザインパターンエリッ - ク ガンマ (著), ラルフ ジョンソン (著), リチャード ヘルム ( - 著), ジョン ブリシディース (著), Erich Gamma (原著), Ralph Johnson - (原著), Richard Helm (原著), John Vlissides (原著), 本位田 - 真一 (翻訳), 吉田 和樹 (翻訳) - -プログラミング作法 - ブライアン カーニハン (著), ロブ パイク (著), Brian Kernighan (原著), Rob Pike (\ - 原著), 福崎 俊博 (翻訳) - -やさしいUML入門 Javaオブジェクト・モデリング - 浅海 智晴 (著) - -コードコンプリート —完全なプログラミングを目指してMicrosoft PRESS - スティーブ マコネル (著), Steve McConnell (原著), 石川 勝 (翻訳) - -Effective C++ 原著第3版 -- 評価方法 - 演習の結果を総合して判定する。 - + +レポートにより判定する。 --授業計画
    -
  1. ソフトウェア工学 -
  2. 集合、論理、関数 -
  3. 一階述語論理とシーケント代数 -
  4. Haskell 入門 -
  5. Haskell のFunctor -
  6. Curry Howard 対応 -
  7. Agda -
  8. Category と Natural Transformation -
  9. Monad -
  10. Monad の合成 -
  11. Design Pattern と Refactoring -
  12. Test と Debug +
  13. オートマトンの概要 +
  14. Agdaによる数学的構造の定義と証明 +
  15. 決定性オートマトン +
  16. 非決定性オートマトン +
  17. 正規表現 +
  18. 正規表現とオートマトン +
  19. 非決定性オートマトンから決定性オートマトンへの変換 +
  20. push donwオートマトンと文法クラス +
  21. Turing Machine +
  22. Turing Machine と計算量の理論 +
  23. ω オートマトン +
  24. 時相論理とCTL +
  25. モデル検査とSAT
-電子メールおよび ura.ie.classes.software のニュースグループを使用する。 - ---古い授業　 +電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。 -
    -
  1. EasyPackage -
  2. Perl と Perl module -
  3. Python -
  4. 5分でわかる Ruby -
  5. Ruby part 2 -
  6. Ruby UML Web framework -
  7. Haskell part 1 -
  8. Haskell part 2 -
  9. Haskell part 3 -
  10. Haskell part 4 -
  11. Emacs Lisp -
  12. Lisp part 2 -
  13. Coq -
  14. Prolog -
  15. Prolog part 2 -
  16. Object 指向 -
  17. AppleScript -
  18. Objective C -
  19. Server Programming -
  20. Eralang -
-