Mercurial > hg > Members > kono > Proof > automaton

changeset 0:e5aa1cf746cb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
automaton lecture
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 13 Aug 2018 22:38:05 +0900
parents
children 3c6de7cf2a95
files agda/automaton.agda agda/regex.agda index.ind
diffstat 3 files changed, 239 insertions(+), 0 deletions(-) [+]
line wrap: on
line diff
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/automaton.agda	Mon Aug 13 22:38:05 2018 +0900
@@ -0,0 +1,133 @@
+module automaton where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Fin
+open import Data.List 
+open import Data.Bool using ( Bool ; true ; false )
+open import  Relation.Binary.PropositionalEquality
+
+record Automaton ( Q : Set ) ( Σ : Set  ) 
+          ( δ : Q → Σ → Q ) ( q0 : Q ) ( F : Q → Bool )
+       : Set  where
+
+data  States1   : Set  where
+   r : States1
+   s : States1
+   t : States1
+
+data  In2   : Set  where
+   i0 : In2
+   i1 : In2
+
+moves : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
+    → Automaton Q  Σ  δ  q0  F
+    → Q → List  Σ → Q
+moves {Q} { Σ} { δ } { q0 } { F } _ q L = move q L
+   where
+      move : (q : Q ) ( L : List  Σ ) → Q
+      move q [] = q
+      move q ( H  ∷ T ) = move (  δ q H ) T
+
+accept : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
+    → Automaton Q  Σ  δ  q0  F
+    → List  Σ → Bool
+accept {Q} { Σ} { δ } { q0 } { F } _ L = move q0 L
+   where
+      move : (q : Q ) ( L : List  Σ ) → Bool
+      move q [] = F q
+      move q ( H  ∷ T ) = move (  δ q H ) T
+
+transition1 : States1  → In2  → States1 
+transition1 r i0  = r
+transition1 r i1  = s
+transition1 s i0  = r
+transition1 s i1  = t
+transition1 t i0  = r
+transition1 t i1  = t
+
+fin1 :  States1  → Bool 
+fin1 t = true
+fin1 _ = false
+
+am1  :  Automaton  States1 In2 transition1 r fin1
+am1  =  record {}
+
+
+example1-1 = accept am1 ( i0  ∷ i1  ∷ i0  ∷ [] )
+example1-2 = accept am1 ( i1  ∷ i1  ∷ i1  ∷ [] )
+
+reachable : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
+    → (M : Automaton Q  Σ  δ  q0  F )
+    → (q : Q )
+    → (L : List  Σ ) → Set 
+reachable {_} {_} {_} {q0} {_} M q L = moves M q0 L ≡ q
+
+example1-3 = reachable am1 t ( i1  ∷ i1  ∷ i1  ∷ [] )
+
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+state≟ : (s s' : States1 ) → Dec  ( s ≡ s' )
+state≟ r r = yes refl
+state≟ s s = yes refl
+state≟ t t = yes refl
+state≟ r t = no  λ()
+state≟ r s = no  λ()
+state≟ s t = no  λ()
+state≟ s r = no  λ()
+state≟ t s = no  λ()
+state≟ t r = no  λ()
+
+record NAutomaton ( Q : Set ) ( Σ : Set  ) 
+          ( δ : Q → Σ → List Q ) ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) ) ( q0 : Q ) ( F : Q → Bool )
+       : Set  where
+
+insert : { Q : Set } →  ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) )  → List Q  → Q  → List Q  
+insert  _≟_  [] q =  q ∷ []
+insert  _≟_  ( q  ∷ T ) q' with  q ≟ q'
+... | yes _ = insert  _≟_  T q'
+... | no _ = q  ∷ (insert  _≟_  T q' )
+
+merge : { Q : Set } →  ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) )  → List Q  → List Q  → List Q  
+merge  _≟_ L1 [] = L1
+merge  _≟_ L1 ( H  ∷ L  ) =  insert _≟_ (merge _≟_ L1 L ) H 
+
+Nmoves : { Q : Set } { Σ : Set  } { δ : Q → Σ → List Q }  { _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) } { q0 : Q } { F : Q → Bool }
+    → NAutomaton Q  Σ  δ  _≟_  q0  F
+    → List Q → List  Σ → List Q
+Nmoves {Q} { Σ} { δ } {_≟_} { q0 } { F } _ 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 _≟_  ( δ q H ) LQ )
+
+
+Naccept : { Q : Set } { Σ : Set  } { δ : Q → Σ → List Q }  { _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) } { q0 : Q } { F : Q → Bool }
+    → NAutomaton Q  Σ  δ  _≟_  q0  F
+    →  List  Σ → Bool
+Naccept {Q} { Σ} { δ } {_≟_} { q0 } { F } M L =
+       checkAccept ( Nmoves M (q0  ∷ [] )  [] )
+   where
+      checkAccept : (q : List Q ) → Bool
+      checkAccept [] = false
+      checkAccept ( H ∷ L ) with F H
+      ... | true = true
+      ... | false = checkAccept L
+
+
+transition2 : States1  → In2  → List States1 
+transition2 r i0  = (r ∷ [])
+transition2 r i1  = (s ∷ r ∷ [] )
+transition2 s i0  = (r  ∷ [])
+transition2 s i1  = (t  ∷ [])
+transition2 t i0  = (r  ∷ [])
+transition2 t i1  = (t  ∷ [])
+
+am2  :  NAutomaton  States1 In2 transition2 state≟ r fin1
+am2  =  record {}
+
+
+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/regex.agda	Mon Aug 13 22:38:05 2018 +0900
@@ -0,0 +1,22 @@
+module regex where
+
+open import Level renaming ( suc to succ ; zero to Zero )
+open import Data.Fin
+open import Data.List 
+open import Data.Bool using ( Bool ; true ; false )
+open import  Relation.Binary.PropositionalEquality
+
+data Regex   ( Σ : Set  ) : Set  where
+   _*    : Regex  Σ → Regex  Σ
+   _&_   : Regex  Σ → Regex  Σ → Regex Σ
+   <_>  : List   Σ → Regex  Σ
+
+
+-- data  In2   : Set  where
+--    a : In2
+--    b : In2
+
+open import automaton
+
+regex2nfa :  Regex In2 → NAutomaton ? In2 ? ? ? ?
+regex2nfa = ?
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/index.ind	Mon Aug 13 22:38:05 2018 +0900
@@ -0,0 +1,84 @@
+-title: オートマトン
+
+この授業では、Agda を使って、計算機科学の基礎であるオートマトンとチューリングマシンについえ学びます。
+
+
+-- 参考書
+
+<a href="http://www.sampou.org/haskell/tutorial-j/index.html">
+「やさしい 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> 
+</ol>
+
+電子メールおよび ura.ie.classes.software のニュースグループを使用する。
+
+--古い授業　
+
+<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>
+