Mercurial > hg > Members > kono > Proof > automaton

changeset 24:9406c2571fe7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
naccept1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 07:53:48 +0900
parents 0c3054704de7
children 256b7a6de863
files agda/automaton.agda agda/nfa-list.agda agda/omega-automaton.agda agda/regop.agda index.ind
diffstat 5 files changed, 180 insertions(+), 144 deletions(-) [+]
line wrap: on
line diff
--- 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  ∷ [] )
-
--- /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  ∷ [] )
+
--- 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 = {!!}
--- /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 = {!!}
--- 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)」
 </a> 
 
-<a href="http://www.amazon.co.jp/dp/4274068854">
-すごい Haskell   Miran Lipova
-</a>
-
-
-<a href="http://www.amazon.co.jp/exec/obidos/redirect?link_code=ur2&tag=shinjkonoshom-22&camp=247&creative=1211&path=external-search%3Fsearch-type=ss%26index=books-jp%26keyword=%25E9%2581%2594%25E4%25BA%25BA%25E3%2583%2597%25E3%2583%25AD%25E3%2582%25B0%25E3%2583%25A9%25E3%2583%259E%25E3%2583%25BC">達人プログラマー</a>
-アンドリュー ハント、デビッド トーマス (ピアソン・エデュケーション)
-    オブジェクト指向における再利用のためのデザインパターンエリッ
-    ク ガンマ (著), ラルフ ジョンソン (著), リチャード ヘルム (
-    著), ジョン ブリシディース (著), Erich Gamma (原著), Ralph Johnson
-    (原著), Richard Helm (原著), John Vlissides (原著), 本位田
-    真一 (翻訳), 吉田 和樹 (翻訳)
-
-<a href="http://www.amazon.co.jp/exec/obidos/redirect?link_code=ur2&tag=shinjkonoshom-22&camp=247&creative=1211&path=external-search%3Fsearch-type=ss%26index=books-jp%26keyword=%25E3%2583%2597%25E3%2583%25AD%25E3%2582%25B0%25E3%2583%25A9%25E3%2583%259F%25E3%2583%25B3%25E3%2582%25B0%25E4%25BD%259C%25E6%25B3%2595">プログラミング作法</a>
-    ブライアン カーニハン (著), ロブ パイク (著), Brian Kernighan (原著), Rob Pike (\
-    原著), 福崎 俊博 (翻訳)
-
-<a href="http://www.amazon.co.jp/exec/obidos/redirect?link_code=ur2&tag=shinjkonoshom-22&camp=247&creative=1211&path=external-search%3Fsearch-type=ss%26index=books-jp%26keyword=%25E3%2582%2584%25E3%2581%2595%25E3%2581%2597%25E3%2581%2584UML%25E5%2585%25A5%25E9%2596%2580">やさしいUML入門</a> Javaオブジェクト・モデリング
-    浅海 智晴 (著)
-
-<a href="http://www.amazon.co.jp/exec/obidos/redirect?link_code=ur2&tag=shinjkonoshom-22&camp=247&creative=1211&path=external-search%3Fsearch-type=ss%26index=books-jp%26keyword=%25E3%2582%25B3%25E3%2583%25BC%25E3%2583%2589%25E3%2582%25B3%25E3%2583%25B3%25E3%2583%2597%25E3%2583%25AA%25E3%2583%25BC%25E3%2583%2588">コードコンプリート</a> —完全なプログラミングを目指してMicrosoft PRESS
-    スティーブ マコネル (著), Steve McConnell (原著), 石川 勝 (翻訳)
-
-<a href="http://www.amazon.co.jp/exec/obidos/redirect?link_code=as2&path=ASIN/4894714515&tag=shinjkonoshom-22&camp=247&creative=1211">Effective C++ 原著第3版</a> 
 
 -- 評価方法
-    演習の結果を総合して判定する。
-    
+
+レポートにより判定する。
 
 --授業計画
 
 <ol>
-<li> ソフトウェア工学
-<li><a href="s01/lecture.html"> 集合、論理、関数</a>
-<li><a href="s02-logic/lecture.html"> 一階述語論理とシーケント代数</a>
-<li><a href="s02/lecture.html"> Haskell 入門</a>
-<li><a href="s02/lecture-functor.html"> Haskell のFunctor</a>
-<li><a href="s03/lecture.html"> Curry Howard 対応 </a> 
-<li><a href="s04/lecture.html"> Agda </a>
-<li><a href="s05/lecture.html"> Category と Natural Transformation </a> 
-<li><a href="s06/lecture.html"> Monad  </a> 
-<li><a href="s07/lecture.html"> Monad の合成  </a> 
-<li><a href="s08/lecture.html"> Design Pattern と Refactoring </a> 
-<li><a href="s09/lecture.html"> Test と Debug </a> 
+<li><a href="a01/lecture.html"> オートマトンの概要</a>
+<li><a href="a02/lecture.html"> Agdaによる数学的構造の定義と証明</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.software のニュースグループを使用する。
-
---古い授業　
+電子メールおよび ura.ie.classes.automaton のニュースグループを使用する。
 
-<ol>
-<li><a href="old/s02-perlmod/epkg.html">  EasyPackage </a>
-<li><a href="old/s02-perlmod/lecture.html">  Perl と Perl module </a>
-<li><a href="old/s03python/lecture.html"> Python</a>
-<li><a href="old/s03ruby/Rubyin5minutes.html"> 5分でわかる Ruby</a>
-<li><a href="old/s04haskell2/lecture-ruby.html"> Ruby part 2</a>
-<li><a href="old/s03ruby/lecture.html">  Ruby UML Web framework</a>
-<li><a href="old/s04haskell2/haskell.html"> Haskell part 1</a>
-<li><a href="old/s04haskell2/haskell2.html"> Haskell part 2</a>
-<li><a href="old/s04haskell2/haskell3.html"> Haskell part 3</a>
-<li><a href="old/s04haskell2/haskell4.html"> Haskell part 4</a>
-<li><a href="old/s05-emacslisp/lecture-lisp.html"> Emacs Lisp</a>
-<li><a href="old/s06-UML/lecture-lisp.html"> Lisp part 2</a>
-<li><a href="old/s05-logic/coq.html"> Coq</a>
-<li><a href="old/s11-prolog/lecture.html"> Prolog</a>
-<li><a href="old/s05-logic/prolog.html"> Prolog part 2</a>
-<li><a href="old/s06-UML/object.html"> Object 指向</a>
-<li><a href="old/s07-applescript/lecture.html"> AppleScript</a>
-<li><a href="old/s07-objective-C/lecture.html"> Objective C</a>
-<li><a href="old/s10-server/lecture.html"> Server Programming</a>
-<li><a href="old/s12-erlang/lecture-erlang.html"> Eralang</a>
-</ol>
-