Mercurial > hg > Members > kono > Proof > automaton

changeset 38:ab265470c2d0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
push down automaton example
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 12 Dec 2018 17:50:42 +0900
parents a7f09c9a2c7a
children 3f099f353f1c
files agda/automaton.agda agda/nfa.agda agda/pushdown.agda agda/regex1.agda
diffstat 4 files changed, 96 insertions(+), 33 deletions(-) [+]
line wrap: on
line diff
--- a/agda/automaton.agda	Wed Dec 05 16:17:28 2018 +0900
+++ b/agda/automaton.agda	Wed Dec 12 17:50:42 2018 +0900
@@ -78,3 +78,12 @@
 ieq i0 i1 = no ( λ () )
 ieq i1 i0 = no ( λ () )
 
+inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ 
+inputnn {zero} {_} _ _ s = s
+inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )
+
+lemmaNN :  Q : Set } { Σ : Set  } → (M : Automaton Q  Σ) →  ¬ accept M ( inputnn {n} x y [] )
+lemmaNN = ?
+
+
+
--- a/agda/nfa.agda	Wed Dec 05 16:17:28 2018 +0900
+++ b/agda/nfa.agda	Wed Dec 12 17:50:42 2018 +0900
@@ -145,3 +145,15 @@
 -- test4 zero = {!!}
 -- test4 (suc zero) = {!!}
 -- test4 (suc (suc ()))
+
+--  0011
+--  00000111111
+inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
+inputnn {zero} {_} _ _ s = s
+inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )                                                                                                         
+-- lemmaNN :  { Q : Set } { Σ : Set  } → ( x y : Σ ) → (M : NAutomaton Q  Σ)
+--     → ( n :  ℕ )  → (fin :  FiniteSet Q  {n} ) 
+--     →  Naccept M fin ( inputnn {n} x y [] )  ≡ true  
+--     →  Naccept M fin ( inputnn {suc n} x y [] )  ≡ false  
+-- lemmaNN {Q} {Σ} x y M n fin nac = {!!}
+
--- a/agda/pushdown.agda	Wed Dec 05 16:17:28 2018 +0900
+++ b/agda/pushdown.agda	Wed Dec 12 17:50:42 2018 +0900
@@ -21,27 +21,55 @@
     field
         pδ : Q → Σ →  Γ → Q × ( PushDown  Γ )
         pstart : Q
-        pz0 :  Γ
-    pmoves :  Q → List  Σ → ( Q × List  Γ )
-    pmoves q L = move q L [ pz0 ]
+        pok : Q → Bool
+        pempty : Γ
+    pmoves :  Q → List  Γ  → Σ → ( Q × List  Γ )
+    pmoves q [] i with pδ q i pempty
+    pmoves q [] i | qn , pop = ( qn , [] )
+    pmoves q [] i | qn , push x = ( qn , ( x ∷  [] ) )
+    pmoves q (  H  ∷ T  ) i with pδ q i H
+    pmoves q (H ∷ T) i | qn , pop =  ( qn , T )
+    pmoves q (H ∷ T) i | qn , push x = ( qn , ( x ∷ H ∷ T) )
+
+    paccept : List  Σ → Bool
+    paccept L = move pstart L []
            where
-              move : Q → ( List  Σ ) → ( List  Γ ) → ( Q × List  Γ )
-              move q _ [] = ( q , [] )
-              move q [] S = ( q , S )
-              move q ( H  ∷ T ) ( SH ∷ ST ) with  pδ q H SH 
-              ... | (nq , pop )     = move nq T ST
-              ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
-    paccept : List  Σ → Bool
-    paccept L = move pstart L [ pz0 ]
-           where
-              move : (q : Q ) ( L : List  Σ ) ( L : List   Γ ) → Bool
-              move q [] [] = true
-              move q _ [] = false
+              move : (q : Q ) ( In : List  Σ ) ( sp : List   Γ ) → Bool
+              move q [] [] = pok q
+              move q ( H  ∷ T) [] with pδ q H pempty
+              move q (H ∷ T) [] | qn , pop = move qn T []
+              move q (H ∷ T) [] | qn , push x = move qn T (x  ∷ [] )
               move q [] (_ ∷ _ ) = false
               move q ( H  ∷ T ) ( SH  ∷ ST ) with pδ q H SH
               ... | (nq , pop )     = move nq T ST
               ... | (nq , push ns ) = move nq T ( ns  ∷  SH ∷ ST )
 
 
+--  0011
+--  00000111111
+inputnn : { n :  ℕ }  →  { Σ : Set  } → ( x y : Σ )  → List  Σ → List  Σ
+inputnn {zero} {_} _ _ s = s
+inputnn {suc n} x y s = x  ∷ ( inputnn {n} x y ( y  ∷ s ) )       
 
+data  States0   : Set  where
+   sr : States0
 
+data  In2   : Set  where
+   i0 : In2
+   i1 : In2
+ 
+pnn : PushDownAutomaton States0 In2 States0
+pnn = record {
+         pδ  = pδ
+      ;  pstart = sr
+      ;  pempty = sr
+      ;  pok = λ q → true
+   } where
+        pδ  : States0 → In2 → States0 → States0 × PushDown States0
+        pδ sr i0 _ = (sr , push sr) 
+        pδ sr i1 _ = (sr , pop ) 
+
+test1 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i1 ∷ [] )
+test2 = PushDownAutomaton.paccept pnn ( i0 ∷ i0 ∷ i1 ∷ i0 ∷ [] )
+test3 = PushDownAutomaton.pmoves pnn sr [] i0 
+
--- a/agda/regex1.agda	Wed Dec 05 16:17:28 2018 +0900
+++ b/agda/regex1.agda	Wed Dec 12 17:50:42 2018 +0900
@@ -112,37 +112,35 @@
 
 open import Data.Product
 
-regex2nfa' : {Σ : Set} → Regex Σ → {n m : ℕ } (fin : FiniteSet Σ {n}) → ( NAutomaton (Regex Σ) Σ  ×   FiniteSet (Regex Σ) {m} )
-regex2nfa' = {!!}
 
-regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ
-regex2nfa {Σ} (r *) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
-          nr0 = regex2nfa r fin
+regex2nfa : {Σ : Set} → Regex Σ → {n : ℕ } (fin : FiniteSet Σ {n}) → NAutomaton (Regex Σ) Σ × ( List (Regex Σ) ) 
+regex2nfa {Σ} (r *) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!}  where
+          nr0 =  proj₁ (regex2nfa r fin)
           Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
           Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nδ nr0 s0 i s1)
           Nstart : (Regex Σ) → Bool
           Nstart s0 = NAutomaton.Nstart nr0 s0
           Nend : (Regex Σ) → Bool
           Nend s0 =  NAutomaton.Nend nr0 s0
-regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
-          nr0 = regex2nfa r0 fin
-          nr1 = regex2nfa r1 fin
+regex2nfa {Σ} (r0 & r1) fin =  record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
+          nr0 =  proj₁ (regex2nfa r0 fin)
+          nr1 =  proj₁ (regex2nfa r1 fin)
           Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
           Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ ( NAutomaton.Nend nr0 s0 ∧  NAutomaton.Nδ nr1 s0 i s1 )
           Nstart : (Regex Σ) → Bool
           Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ ( NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nstart nr1 s0 )
           Nend : (Regex Σ) → Bool
           Nend s0 = NAutomaton.Nend nr0 s0  ∨ (  NAutomaton.Nend nr0 s0 ∧ NAutomaton.Nend nr1 s0 )
-regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
-          nr0 = regex2nfa r0 fin 
-          nr1 = regex2nfa r1 fin
+regex2nfa {Σ} (r0 || r1) fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
+          nr0 =  proj₁ (regex2nfa r0 fin)
+          nr1 =  proj₁ (regex2nfa r1 fin)
           Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
           Nδ s0 i s1 = NAutomaton.Nδ nr0 s0 i s1 ∨ NAutomaton.Nδ nr1 s0 i s1
           Nstart : (Regex Σ) → Bool
           Nstart s0 = NAutomaton.Nstart nr0 s0  ∨ NAutomaton.Nstart nr1 s0 
           Nend : (Regex Σ) → Bool
           Nend s0 = NAutomaton.Nend nr0 s0  ∨ NAutomaton.Nend nr1 s0 
-regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } where
+regex2nfa {Σ} < x > fin = record { Nδ = Nδ ;  Nstart = Nstart ;  Nend = Nend } , {!!} where
           Nδ : (Regex Σ) → Σ → (Regex Σ) → Bool
           Nδ r1 s r2 with cmpi fin s x
           Nδ r1 s r2 | yes _ = true
@@ -159,15 +157,31 @@
 
 -- testr5 = Naccept test-r4 {!!} ( i0  ∷ i1  ∷ [] )
 
+rfin : {Σ : Set} → (s : List ( Regex Σ)) → FiniteSet (Regex Σ ) {length s } 
+rfin {Σ} s = record {
+        Q←F = Q←F'
+      ; F←Q  = F←Q'
+      ; finiso→ = finiso→'
+      ; finiso← = finiso←'
+  } where
+        Q←F' : Fin (length s) → Regex Σ
+        Q←F' = {!!}
+        F←Q'  : Regex Σ → Fin (length s)
+        F←Q'  = {!!}
+        finiso→' : (q : Regex Σ) → Q←F' (F←Q' q) ≡ q
+        finiso→' = {!!}
+        finiso←' : (f : Fin (length s)) → F←Q' (Q←F' f) ≡ f
+        finiso←' = {!!}
+
 reglang⇔n=regex2nfa : {Σ : Set} → {n m : ℕ } (fin : FiniteSet Σ {n}) 
      → ( regex : Regex Σ )
-     → ( rfin : FiniteSet (Regex Σ) {m} )
      → ( In : List Σ )
-     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} ( regex2nfa {Σ} regex  fin  ) rfin In
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) rfin In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) rfin In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) rfin In = {!!}
-reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > rfin In = {!!}
+     → regular-language regex fin  In  ≡ Naccept {Regex Σ} {_} (  proj₁ ( regex2nfa {Σ} regex  fin  ))
+         (rfin (proj₂  ( regex2nfa {Σ} regex  fin  ) )) In
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex *) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex & regex₁) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin (regex || regex₁) In = {!!}
+reglang⇔n=regex2nfa {Σ} {n} {m} fin < x > In = {!!}