Mercurial > hg > Members > kono > Proof > automaton

changeset 8:cdf75ae6f0c1

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
add subset construction
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 15 Aug 2018 17:38:48 +0900
parents f1fbe6603066
children e7bb980408fb
files agda/automaton.agda agda/regex.agda agda/sbconst.agda
diffstat 3 files changed, 143 insertions(+), 10 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Aug 15 14:37:11 2018 +0900
+++ b/agda/automaton.agda	Wed Aug 15 17:38:48 2018 +0900
@@ -180,11 +180,13 @@
 memberT n (node n1 e1 left right) | no ¬p | (yes p) = memberT n left
 memberT n (node n1 e1 left right) | no ¬p | (no ¬p₁) = memberT n right
 
+open import Data.Product
 
 record εAutomaton ( Q : Set ) ( Σ : Set  ) 
        : Set  where
     field
           εδ : Q → Maybe Σ → Tree Q
+          all-εδ : Q → Tree ( Maybe Σ × Tree Q )
           εid : Q  →  ℕ
           allState : Tree Q
           εstart : Q
@@ -197,9 +199,10 @@
 --    keep track state list in C
 --    if already tracked, skip it
 εclosure : { Q : Set } { Σ : Set  }
-    → εAutomaton Q  Σ
+    → ( allState :  Tree Q )
+    → ( εδ : Q → Maybe Σ → Tree Q )
     → Tree ( Tree  Q )
-εclosure {Q} { Σ} M  = closure (  allState  M )
+εclosure {Q} { Σ} allState εδ  = closure (  allState   )
     where
          closure2 :  Tree Q →  Tree Q →  Tree Q 
          closure2 empty C = C
@@ -210,9 +213,9 @@
          ... | just _  =  closure2 left ( closure2 right C )
          ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
          closure1 : ℕ →  Tree  Q 
-         closure1 n with memberT n (allState  M) 
+         closure1 n with memberT n (allState  ) 
          ... | nothing = empty
-         ... | just q = closure2 (εδ M q nothing) ( leaf n q )
+         ... | just q = closure2 (εδ  q nothing) ( leaf n q )
          closure :  Tree Q  → Tree ( Tree  Q )
          closure empty = empty
          closure (leaf n e) = (leaf n (closure1 n)  )
@@ -228,7 +231,7 @@
      nend =  εend M
   } where
      MTree :  Tree ( Tree  Q )
-     MTree = εclosure M
+     MTree = εclosure (allState M ) (  εδ M )
      nδ1 : Tree Q → Σ → List Q
      nδ1 empty i = []
      nδ1 (leaf n q) i = [ q ]
--- a/agda/regex.agda	Wed Aug 15 14:37:11 2018 +0900
+++ b/agda/regex.agda	Wed Aug 15 17:38:48 2018 +0900
@@ -3,6 +3,7 @@
 open import Level renaming ( suc to succ ; zero to Zero )
 -- open import Data.Fin
 open import Data.Nat
+open import Data.Product
 -- open import Data.List 
 open import Data.Maybe 
 open import Data.Bool using ( Bool ; true ; false )
@@ -30,6 +31,7 @@
    field
       state :  ℕ
       move  :  Maybe Σ → Tree (RST Σ)
+      cond  :  Maybe Σ 
       RSTend : Bool
 
 open RST
@@ -53,7 +55,7 @@
 
 infixr 5 _++_ 
 
-_++_ : { Σ : Set} → Tree (RST Σ ) → Tree (RST Σ ) → Tree (RST Σ )
+_++_ : { Q : Set} → Tree Q → Tree Q → Tree Q 
 empty ++ t = t
 leaf n e ++ t = insertT n e t
 node n e left right ++ t =
@@ -61,13 +63,13 @@
 
 generateRNFA :  { Σ : Set  } → ( Regex  Σ ) → (_≟_ : ( q q' : Σ ) → Dec ( q ≡ q' ) ) →  RNFA  Σ
 generateRNFA  {Σ} regex _≟_ = generate regex (
-      record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; RSTend = true } ;
-                                Rend = record { state = 0 ; move = λ q → [] ; RSTend = true }  ; Rnum = 1 } )
+      record { Rstates = [] ; Rstart = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true } ;
+                                Rend = record { state = 0 ; move = λ q → [] ; cond = nothing ; RSTend = true }  ; Rnum = 1 } )
  where
   literal :  Maybe Σ →  Σ → ℕ → Tree (RST  Σ)
   literal nothing  q' n = []
   literal (just q)  q' n with q ≟  q'
-  ... | yes _ = [ record { state = n ; move = λ i → empty ; RSTend = true  } ]
+  ... | yes _ = [ record { state = n ; move = λ i → empty ; cond = nothing ; RSTend = true  } ]
   ... | no _ = []
   generate : ( Regex  Σ ) →  RNFA Σ → RNFA Σ 
   generate (x *) R = record R' { Rstart =  record (Rstart R') { move = move0  }   ;
@@ -94,7 +96,7 @@
        R1 :  RNFA  Σ 
        R1 = generate x (  record R { Rnum = Rnum R + 1 } )
        S1 : RST Σ
-       S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] }
+       S1 = record { state = Rnum R ; RSTend = RSTend (Rend R) ; move  = λ q → [] ; cond = nothing }
        R2 :  RNFA  Σ
        R2 = generate y ( record R1 { Rstart = S1 ; Rend = S1  } )
        move0 : Maybe Σ → Tree (RST  Σ)
@@ -108,6 +110,7 @@
        Rstart = record {
                state  = Rnum R
              ; move = λ q → literal q x ( state (Rstart R) )
+             ; cond = just x
              ; RSTend = false
             } ;
        Rstates =  [ Rstart R ] ++ Rstates R 
@@ -116,6 +119,7 @@
 regex2nfa :  (regex : Regex In2 ) → εAutomaton (RST In2) In2 
 regex2nfa regex = record {
       εδ =  move 
+    ; all-εδ =  cond1
     ; εid = λ s → state s
     ; allState = Rstates G
     ; εstart =   Rstart G
@@ -123,4 +127,14 @@
       where
           G : RNFA In2
           G =  generateRNFA regex ieq
+          GTree :  Tree ( Tree (RST In2) ) 
+          GTree = εclosure (Rstates G) move 
+          cond2 : Maybe (Tree (RST In2) )  → Tree (Maybe In2 × Tree (RST In2))
+          cond2 nothing =  empty
+          cond2 (just empty) = empty
+          cond2 (just (leaf n r)) = leaf n (  cond r , move r ( cond r ) )
+          cond2 (just (node n r left  right )) = cond2 (just left ) ++ leaf n (  cond r , move r ( cond r ) ) ++  cond2 (just right )
+          cond1 : RST In2 → Tree (Maybe In2 × Tree (RST In2))
+          cond1 s = cond2 ( memberT ( state s ) GTree ) 
 
+
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/sbconst.agda	Wed Aug 15 17:38:48 2018 +0900
@@ -0,0 +1,116 @@
+module sbconst 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.Product 
+open import Data.Bool using ( Bool ; true ; false ; _∨_ )
+open import  Relation.Binary.PropositionalEquality hiding ( [_] )
+open import Relation.Nullary using (¬_; Dec; yes; no)
+
+open import automaton
+
+flatten : { Q : Set} → Tree Q  → List ℕ 
+flatten empty = []
+flatten (leaf x x₁) = [ x ]
+flatten (node x x₁ x₂ x₃) = flatten x₂ ++ [ x ] ++ flatten  x₃
+
+listEq :  List ℕ  → List ℕ  → Bool
+listEq [] [] = true
+listEq [] ( _ ∷  _ )  = false
+listEq ( _ ∷  _ ) [] = false
+listEq ( h1 ∷ t1 ) ( h2 ∷ t2 ) with h1 ≟ h2
+... | yes _ =  listEq t1 t2
+... | no _ = false
+
+infixr 7 _==_
+_==_ : { Q : Set} → Tree Q  → Tree Q → Bool
+x == y = listEq ( flatten x ) ( flatten y )
+
+memberTT : { Q : Set} →  Tree  Q  → Tree ( Tree  Q ) → Bool
+memberTT t empty  = false
+memberTT t (leaf x x₁) = t == x₁
+memberTT t (node x x₁ x₂ x₃) with t == x₁
+... | true = true
+... | false = memberTT t x₂ ∨ memberTT t  x₃
+
+lengthT : { Q : Set} →  Tree  Q  →  ℕ
+lengthT t = length ( flatten t )
+
+open εAutomaton
+
+nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton Q Σ
+nfa2dfa {Σ} {Q} NFA = record {
+        δ  = δ'  
+     ;  astart =  astart' 
+     ;  aend = aend'
+  }
+    where
+      MTree :  Tree ( Tree  Q )
+      MTree = εclosure NFA
+      sbconst2 : Tree ( Maybe Σ × Tree Q ) → Tree ( Tree  Q )  →  ℕ  → Tree ( Tree  Q )
+      sbconst2 s t n with memberTT {!!} t
+      ... | true = t
+      ... | false = {!!}
+      sbconst1 : Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → Tree ( Tree  Q )
+      sbconst1 empty t n = t
+      sbconst1 (leaf x q) t n = sbconst2 ( all-εδ NFA {!!} ) t n
+      sbconst1 (node x q left right ) t n = {!!} 
+      sbconst : Tree ( Tree  Q )  → Tree ( Tree  Q )
+      sbconst t = sbconst1 {!!} t (lengthT t)
+      δ' : Q → Σ → Q
+      δ' = {!!}
+      astart' : Q
+      astart' = {!!}
+      aend' : Q → Bool
+      aend' = {!!}
+
+
+-- data Tree (E : Set ) : Set where
+--    empty :  Tree E
+--    leaf :  ℕ → E → Tree E
+--    node :  ℕ → E → Tree E  → Tree E → Tree E
+
+-- insertT :  {E : Set} → ℕ → E → Tree E → Tree E
+-- memberT :  {E : Set } → ℕ → Tree E → Maybe E
+
+-- record εAutomaton ( Q : Set ) ( Σ : Set  ) 
+--        : Set  where
+--     field
+--           εδ : Q → Maybe Σ → Tree Q
+--           εid : Q  →  ℕ
+--           allState : Tree Q
+--           εstart : Q
+--           εend  : Q → Bool 
+
+
+-- εclosure : { Q : Set } { Σ : Set  }
+--     → εAutomaton Q  Σ
+--     → Tree ( Tree  Q )
+
+-- εAutomaton2U : { Q : Set } { Σ : Set  }
+--     → εAutomaton Q  Σ → NAutomaton Q  Σ
+-- εAutomaton2U {Q} { Σ} M = record {
+--      nδ = nδ' ;
+--      sid = εid M ;
+--      nstart = εstart M  ;
+--      nend =  εend M
+--   } where
+--      MTree :  Tree ( Tree  Q )
+--      MTree = εclosure M
+--      nδ1 : Tree Q → Σ → List Q
+--      nδ1 empty i = []
+--      nδ1 (leaf n q) i = [ q ]
+--      nδ1 (node n q left right) i = nδ1 left i ++ [ q ] ++ nδ1 right i
+--      nδ' : Q → Σ → List Q
+--      nδ' q i with memberT ( εid M q ) MTree
+--      ... | nothing = []
+--      ... | just x = nδ1 x i
+
+
+
+
+
+
+