Mercurial > hg > Members > kono > Proof > automaton

changeset 9:e7bb980408fb

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
separate epsiron
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 22 Aug 2018 21:59:24 +0900
parents cdf75ae6f0c1
children 32fea87e21b8
files agda/automaton.agda agda/epautomaton.agda agda/regex.agda agda/sbconst.agda
diffstat 4 files changed, 189 insertions(+), 173 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Aug 15 17:38:48 2018 +0900
+++ b/agda/automaton.agda	Wed Aug 22 21:59:24 2018 +0900
@@ -6,6 +6,7 @@
 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)
 
 record Automaton ( Q : Set ) ( Σ : Set  ) 
        : Set  where
@@ -25,7 +26,6 @@
    i0 : In2
    i1 : In2
 
-open import Relation.Nullary using (¬_; Dec; yes; no)
 
 ieq : (i i' : In2 ) → Dec ( i ≡ i' )  
 ieq i0 i0 = yes refl
@@ -142,108 +142,3 @@
 example2-1 = Naccept am2 ( i0  ∷ i1  ∷ i0  ∷ [] )
 example2-2 = Naccept am2 ( i1  ∷ i1  ∷ i1  ∷ [] )
 
-nth : {S : Set } →  ℕ → List S → Maybe S
-nth _ [] = nothing
-nth 0 ( x  ∷ _ ) = just x
-nth (suc n) ( _  ∷ t ) = nth n t
-
-member :  ℕ → List ℕ → Bool
-member _ [] = false
-member n ( x  ∷ t ) with n ≟ x
-... | yes _ = true
-... | no _ =  member n t
-
-
-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
-insertT {E} n e empty = leaf n e
-insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1 
-... | yes _ |  _ = leaf n e
-... | no _ | yes _  = node n e ( leaf n1 e1 ) empty
-... | no _ | no _  = node n e empty (  leaf n1 e1 )
-insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1
-... | yes _ |  _ = node n e left right
-... | no _ | yes _  = node n1 e1 ( insertT n e left ) right
-... | no _ | no _   = node n1 e1 left ( insertT n e right ) 
-
-memberT :  {E : Set } → ℕ → Tree E → Maybe E
-memberT _ empty = nothing
-memberT n (leaf n1 e) with n ≟ n1
-... | yes _ = just e
-... | no _ = nothing
-memberT n (node n1 e1 left right) with n ≟ n1 | n ≤? n1
-... | yes _ | _ = just e1
-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
-          εend  : Q → Bool 
-
-open εAutomaton
-
---
---  find ε connected state by following ε transition
---    keep track state list in C
---    if already tracked, skip it
-εclosure : { Q : Set } { Σ : Set  }
-    → ( allState :  Tree Q )
-    → ( εδ : Q → Maybe Σ → Tree Q )
-    → Tree ( Tree  Q )
-εclosure {Q} { Σ} allState εδ  = closure (  allState   )
-    where
-         closure2 :  Tree Q →  Tree Q →  Tree Q 
-         closure2 empty C = C
-         closure2 ( leaf n1 q ) C with memberT n1 C
-         ... | just _  =  C
-         ... | nothing =  insertT n1 q C 
-         closure2 ( node n1 q left right ) C with memberT n1 C
-         ... | just _  =  closure2 left ( closure2 right C )
-         ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
-         closure1 : ℕ →  Tree  Q 
-         closure1 n with memberT n (allState  ) 
-         ... | nothing = empty
-         ... | 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)  )
-         closure (node n e left right) =
-              node n (closure1 n) ( closure left ) ( closure right ) 
-
-ε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 (allState M ) (  εδ 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
-
-
-
-
-
-
-
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/agda/epautomaton.agda	Wed Aug 22 21:59:24 2018 +0900
@@ -0,0 +1,121 @@
+module epautomaton 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)
+
+open import automaton
+
+
+nth : {S : Set } →  ℕ → List S → Maybe S
+nth _ [] = nothing
+nth 0 ( x  ∷ _ ) = just x
+nth (suc n) ( _  ∷ t ) = nth n t
+
+member :  ℕ → List ℕ → Bool
+member _ [] = false
+member n ( x  ∷ t ) with n ≟ x
+... | yes _ = true
+... | no _ =  member n t
+
+
+data STree (S E : Set ) : Set where
+   empty :  STree S E
+   leaf :  S → E → STree S E
+   node :  S → E → STree S E  → STree S E → STree S E
+
+Tree : Set → Set
+Tree E = STree ℕ E
+
+insertT :  {E : Set} → ℕ → E → Tree E → Tree E
+insertT {E} n e empty = leaf n e
+insertT {E} n e (leaf n1 e1 ) with  n ≟ n1  |  n ≤? n1 
+... | yes _ |  _ = leaf n e
+... | no _ | yes _  = node n e ( leaf n1 e1 ) empty
+... | no _ | no _  = node n e empty (  leaf n1 e1 )
+insertT {E} n e (node n1 e1 left right ) with n ≟ n1 | n ≤? n1
+... | yes _ |  _ = node n e left right
+... | no _ | yes _  = node n1 e1 ( insertT n e left ) right
+... | no _ | no _   = node n1 e1 left ( insertT n e right ) 
+
+memberT :  {E : Set } → ℕ → Tree E → Maybe E
+memberT _ empty = nothing
+memberT n (leaf n1 e) with n ≟ n1
+... | yes _ = just e
+... | no _ = nothing
+memberT n (node n1 e1 left right) with n ≟ n1 | n ≤? n1
+... | yes _ | _ = just e1
+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
+          εend  : Q → Bool 
+
+open εAutomaton
+
+--
+--  find ε connected state by following ε transition
+--    keep track state list in C
+--    if already tracked, skip it
+εclosure : { Q : Set } { Σ : Set  }
+    → ( allState :  Tree Q )
+    → ( εδ : Q → Maybe Σ → Tree Q )
+    → Tree ( Tree  Q )
+εclosure {Q} { Σ} allState εδ  = closure (  allState   )
+    where
+         closure2 :  Tree Q →  Tree Q →  Tree Q 
+         closure2 empty C = C
+         closure2 ( leaf n1 q ) C with memberT n1 C
+         ... | just _  =  C
+         ... | nothing =  insertT n1 q C 
+         closure2 ( node n1 q left right ) C with memberT n1 C
+         ... | just _  =  closure2 left ( closure2 right C )
+         ... | nothing =  insertT n1 q (closure2 left ( closure2 right C ))
+         closure1 : ℕ →  Tree  Q 
+         closure1 n with memberT n (allState  ) 
+         ... | nothing = empty
+         ... | 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)  )
+         closure (node n e left right) =
+              node n (closure1 n) ( closure left ) ( closure right ) 
+
+ε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 (allState M ) (  εδ 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
+
+
+
+
+
+
+
--- a/agda/regex.agda	Wed Aug 15 17:38:48 2018 +0900
+++ b/agda/regex.agda	Wed Aug 22 21:59:24 2018 +0900
@@ -23,6 +23,7 @@
 --    b : In2
 
 open import automaton
+open import epautomaton
 
 
 record RST ( Σ : Set )
--- a/agda/sbconst.agda	Wed Aug 15 17:38:48 2018 +0900
+++ b/agda/sbconst.agda	Wed Aug 22 21:59:24 2018 +0900
@@ -10,6 +10,7 @@
 open import Relation.Nullary using (¬_; Dec; yes; no)
 
 open import automaton
+open import epautomaton
 
 flatten : { Q : Set} → Tree Q  → List ℕ 
 flatten empty = []
@@ -38,79 +39,77 @@
 lengthT : { Q : Set} →  Tree  Q  →  ℕ
 lengthT t = length ( flatten t )
 
+findT : { Q : Set} →  Tree Q  → Tree ( Tree  Q ) → Maybe ( Tree Q )
+findT t empty  = nothing
+findT t (leaf x x₁) =  just x₁
+findT t (node x x₁ x₂ x₃) with t == x₁
+... | true =  just x₁
+... | false with findT t x₂
+...    | (just y) = just y
+...    | nothing  = findT t x₃
+
 open εAutomaton
 
-nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton Q Σ
+
+sbconst13 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Maybe Σ × Tree Q ) → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
+sbconst13 NFA empty t n = (n , empty , t )
+sbconst13 NFA (leaf x (p , q)) t n with memberTT q t
+... | true = ( n , empty , t )
+... | false = ( n + 1 , leaf x q , insertT x q t )
+sbconst13 NFA (node x (_ , q) left right) t n with memberTT q t
+sbconst13 NFA (node x (_ , q) left right) t n | true = ( n , empty , t )
+sbconst13 NFA (node x (_ , q) left right) t n | false = p2
+  where
+    p1 = sbconst13 NFA left  t n
+    p2 = sbconst13 NFA right (insertT (n + 1 ) q (  proj₁  ( proj₂ p1 ) ) ) ( n + 1 )
+sbconst12 :  { Σ Q : Set } →  εAutomaton Q Σ → Tree  Q  → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
+sbconst12 NFA empty t n = ( n , empty , t )
+sbconst12 NFA (leaf x q) t n = sbconst13 NFA ( all-εδ NFA q) t n
+sbconst12 NFA (node x q left right) t n = p2
+  where
+    p1 = sbconst12 NFA left  t n
+    p2 = sbconst12 NFA right ( proj₁  ( proj₂ ( sbconst13 NFA ( all-εδ NFA q) t n))) (  proj₁ p1 )
+sbconst11 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  → (  ℕ × Tree ( Tree Q )  × Tree ( Tree  Q ) )
+sbconst11 NFA empty t n = (n , empty , t)
+sbconst11 NFA (leaf x q) t n = sbconst12 NFA q t n
+sbconst11 NFA (node x q left right ) t n = p2
+  where
+    p1 = sbconst11 NFA left  t n
+    p2 = sbconst11 NFA right ( proj₁  ( proj₂ ( sbconst12 NFA q t n))) (  proj₁ p1 )
+       
+{-# TERMINATING #-}
+sbconst0 :  { Σ Q : Set } →   εAutomaton Q Σ → Tree ( Tree  Q ) → Tree ( Tree  Q )  →  ℕ  →  ( ℕ  ×  Tree ( Tree  Q ) )
+sbconst0 NFA t t1 n0 with sbconst11 NFA t t1 (lengthT t)
+... | n , empty , t2 =  (n , t2 )
+... | n , leaf x y , t2 = sbconst0 NFA (  proj₁  ( proj₂ p1 ))    (leaf x y) (proj₁ p1) 
+       where
+         p1 = sbconst11 NFA (leaf x y) t1 n0
+... | n , node x y left right , t2 = p3
+       where
+         p1 = sbconst0 NFA left t2 n
+         p2 = sbconst11 NFA (leaf x y) ( proj₂ p1 ) (  proj₁  p1 ) 
+         p3 = sbconst0 NFA right ( proj₁  ( proj₂ p2))  n
+
+nfa2dfa : { Σ Q : Set } →  εAutomaton Q Σ →  Automaton (Tree 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
+      MTree :  { Σ Q : Set } →  (x : εAutomaton Q Σ) →  Tree ( Tree  Q )
+      MTree {Σ} {Q} NFA = εclosure (allState NFA ) (  εδ NFA )
+      sbconst :  { Σ Q : Set } →  εAutomaton Q Σ → Tree ( Tree  Q )
+      sbconst NFA =  proj₂ (sbconst0 NFA ( MTree NFA ) (MTree NFA) zero)
+      δ' : Tree Q → Σ → Tree Q
+      δ' t x with findT t ( MTree NFA )
+      ... | nothing = leaf zero ( εstart NFA )   -- can't happen
+      ... | just q  = {!!}
+      astart' : Tree Q
+      astart' =  leaf zero ( εstart NFA )
+      aend' : Tree Q → Bool
+      aend' empty = false
+      aend' (leaf _ x)  = εend NFA x
+      aend' (node _ x left right ) =
+          aend' left ∨ εend NFA x ∨ aend' right 
 
--- 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
-
-
-
-
-
-
-