Mercurial > hg > Members > kono > Proof > automaton

changeset 1:3c6de7cf2a95

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
nfa worked
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Tue, 14 Aug 2018 21:44:12 +0900
parents e5aa1cf746cb
children e4d298d26820
files agda/automaton.agda agda/regex.agda
diffstat 2 files changed, 103 insertions(+), 55 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Mon Aug 13 22:38:05 2018 +0900
+++ b/agda/automaton.agda	Tue Aug 14 21:44:12 2018 +0900
@@ -7,79 +7,90 @@
 open import  Relation.Binary.PropositionalEquality
 
 record Automaton ( Q : Set ) ( Σ : Set  ) 
-          ( δ : Q → Σ → Q ) ( q0 : Q ) ( F : Q → Bool )
        : Set  where
+    field
+        δ : Q → Σ → Q
+        astart : Q
+        aend : Q → Bool 
+
+open Automaton
 
 data  States1   : Set  where
-   r : States1
-   s : States1
-   t : States1
+   sr : States1
+   ss : States1
+   st : States1
 
 data  In2   : Set  where
    i0 : In2
    i1 : In2
 
-moves : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
-    → Automaton Q  Σ  δ  q0  F
+moves : { Q : Set } { Σ : Set  }  
+    → Automaton Q  Σ  
     → Q → List  Σ → Q
-moves {Q} { Σ} { δ } { q0 } { F } _ q L = move q L
+moves {Q} { Σ} M q L = move q L
    where
       move : (q : Q ) ( L : List  Σ ) → Q
       move q [] = q
-      move q ( H  ∷ T ) = move (  δ q H ) T
+      move q ( H  ∷ T ) = move (  (δ M) q H ) T
 
-accept : { Q : Set } { Σ : Set  } { δ : Q → Σ → Q } { q0 : Q } { F : Q → Bool }
-    → Automaton Q  Σ  δ  q0  F
+accept : { Q : Set } { Σ : Set  } 
+    → Automaton Q  Σ  
     → List  Σ → Bool
-accept {Q} { Σ} { δ } { q0 } { F } _ L = move q0 L
+accept {Q} { Σ} M L = move (astart M) L
    where
       move : (q : Q ) ( L : List  Σ ) → Bool
-      move q [] = F q
-      move q ( H  ∷ T ) = move (  δ q H ) T
+      move q [] = aend M q
+      move q ( H  ∷ T ) = move (  (δ M) 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
+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 t = true
+fin1 st = true
 fin1 _ = false
 
-am1  :  Automaton  States1 In2 transition1 r fin1
-am1  =  record {}
+am1  :  Automaton  States1 In2 
+am1  =  record {  δ = transition1 ; astart = sr ; aend = fin1   }
 
 
 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 )
+reachable : { Q : Set } { Σ : Set  } 
+    → (M : Automaton Q  Σ  )
     → (q : Q )
     → (L : List  Σ ) → Set 
-reachable {_} {_} {_} {q0} {_} M q L = moves M q0 L ≡ q
+reachable M q L = moves M (astart M)  L ≡ q
 
-example1-3 = reachable am1 t ( i1  ∷ i1  ∷ i1  ∷ [] )
+example1-3 = reachable am1 st ( 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  λ()
+state≟ sr sr = yes refl
+state≟ ss ss = yes refl
+state≟ st st = yes refl
+state≟ sr st = no  λ()
+state≟ sr ss = no  λ()
+state≟ ss st = no  λ()
+state≟ ss sr = no  λ()
+state≟ st ss = no  λ()
+state≟ st sr = no  λ()
 
 record NAutomaton ( Q : Set ) ( Σ : Set  ) 
-          ( δ : Q → Σ → List Q ) ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) ) ( q0 : Q ) ( F : Q → Bool )
        : Set  where
+    field
+          nδ : Q → Σ → List Q
+          n≟ : (q q' : Q ) → Dec ( q ≡ q' )
+          nstart : Q
+          nend  : Q → Bool 
+
+open NAutomaton
 
 insert : { Q : Set } →  ( _≟_ : (q q' : Q ) → Dec ( q ≡ q' ) )  → List Q  → Q  → List Q  
 insert  _≟_  [] q =  q ∷ []
@@ -91,40 +102,40 @@
 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
+Nmoves : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ  
     → List Q → List  Σ → List Q
-Nmoves {Q} { Σ} { δ } {_≟_} { q0 } { F } _ q L = Nmoves1 q L []
+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 _≟_  ( δ q H ) LQ )
+      Nmoves1 (q  ∷ T ) (H  ∷ L) LQ = Nmoves1 T  (H  ∷ L) ( merge (n≟ M)  ( nδ M 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
+Naccept : { Q : Set } { Σ : Set  } 
+    → NAutomaton Q  Σ  
     →  List  Σ → Bool
-Naccept {Q} { Σ} { δ } {_≟_} { q0 } { F } M L =
-       checkAccept ( Nmoves M (q0  ∷ [] )  [] )
+Naccept {Q} { Σ} M L =
+       checkAccept ( Nmoves M ((nstart M)  ∷ [] )  L )
    where
       checkAccept : (q : List Q ) → Bool
       checkAccept [] = false
-      checkAccept ( H ∷ L ) with F H
+      checkAccept ( H ∷ L ) with (nend M) 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  ∷ [])
+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 transition2 state≟ r fin1
-am2  =  record {}
+am2  :  NAutomaton  States1 In2
+am2  =  record { nδ = transition2 ; n≟ = state≟ ; nstart = sr ; nend = fin1}
 
 
 example2-1 = Naccept am2 ( i0  ∷ i1  ∷ i0  ∷ [] )
--- a/agda/regex.agda	Mon Aug 13 22:38:05 2018 +0900
+++ b/agda/regex.agda	Tue Aug 14 21:44:12 2018 +0900
@@ -2,13 +2,17 @@
 
 open import Level renaming ( suc to succ ; zero to Zero )
 open import Data.Fin
+open import Data.Nat
 open import Data.List 
 open import Data.Bool using ( Bool ; true ; false )
 open import  Relation.Binary.PropositionalEquality
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
 
 data Regex   ( Σ : Set  ) : Set  where
    _*    : Regex  Σ → Regex  Σ
    _&_   : Regex  Σ → Regex  Σ → Regex Σ
+   _||_   : Regex  Σ → Regex  Σ → Regex Σ
    <_>  : List   Σ → Regex  Σ
 
 
@@ -18,5 +22,38 @@
 
 open import automaton
 
-regex2nfa :  Regex In2 → NAutomaton ? In2 ? ? ? ?
-regex2nfa = ?
+
+record RST ( Σ : Set )
+     : Set where
+   inductive
+   field
+      state :  ℕ
+      move  :  Σ → List (RST Σ)
+      RSTend : Bool
+
+open RST
+
+record RNFA ( Σ : Set )
+     : Set where
+   field
+      eqRST? :  (q q' : RST Σ) → Dec (q ≡ q')
+      start :  RST Σ
+      end   :  RST Σ → Bool
+
+open RNFA
+
+generateRNFA :  { Σ : Set  } →  ( Regex  Σ ) →  RNFA  Σ
+generateRNFA  {Σ} regex = record {
+          eqRST? = eqRST
+       ;  start = {!!}
+       ;  end = λ s → RSTend s
+    } where
+       eqRST :  (q q' : RST Σ) → Dec (q ≡ q')
+       eqRST q q' with  (state q)  ≟  (state q')
+       ... | yes eq = {!!}
+       ... | no neq = {!!}
+
+
+regex2nfa :  (regex : Regex In2 ) → NAutomaton (RST In2) In2 
+regex2nfa regex = record {  nδ = λ s i → move s i ; n≟ = {!!} ; nstart = {!!} ;  nend = {!!} }
+