Mercurial > hg > Members > kono > Proof > automaton1

changeset 6:c42493f74570

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 14 Nov 2020 18:05:41 +0900
parents 06cc23ff53d7
children 8f1828ec8d1b
files automaton.agda nfa.agda
diffstat 2 files changed, 45 insertions(+), 23 deletions(-) [+]
line wrap: on
line diff
--- a/automaton.agda	Sat Nov 14 11:05:25 2020 +0900
+++ b/automaton.agda	Sat Nov 14 18:05:41 2020 +0900
@@ -51,11 +51,6 @@
 data a16end : Q3 → Set where
    a16q2 : a16end q₂
 
-data exists-in-Q3 (P : Q3 → Set) :  Set where
-  qe1 :  P q₁ → exists-in-Q3 P
-  qe2 :  P q₂ → exists-in-Q3 P
-  qe3 :  P q₃ → exists-in-Q3 P
-
 a16 : Automaton Q3 Σ2
 a16 = record { δ = δ16 ; F = λ q → a16end q }
 
--- a/nfa.agda	Sat Nov 14 11:05:25 2020 +0900
+++ b/nfa.agda	Sat Nov 14 18:05:41 2020 +0900
@@ -28,15 +28,18 @@
 
 ntrace : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ )
      → naccept Nexists nfa qs input
-     → ((qs : Q → Set) (a : Nexists (λ q → qs q ∧ NF nfa q)) (q : Q)  → Dec (qs q ∧ NF nfa q))
-     → ((qs : Q → Set) (x : Σ) (t : List Σ) (a : naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q')) t)
-          (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t))
+     → ((q : Q) → Dec (qs q))
+     → (next-dec : (qs : Q → Set) → ((q : Q) → Dec (qs q)) → (x : Σ) → (q : Q ) → Dec (Nexists (λ nq → qs nq ∧ Nδ nfa nq x q)))
      → List Q
      → List (List Q)
-ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs a) L ∷ []
-ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a decNF decNδ L = 
-      qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t a ) L
-      ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a decNF decNδ L )
+ntrace {n} {Q} {Σ} Nexists nfa qs [] a dec next-dec L = qlist qs dec L ∷ []
+ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a dec next-dec L = 
+      qlist qs dec L ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a (next-dec qs dec x) next-dec L ) 
+
+data exists-in-Q3 (P : Q3 → Set) :  Set where
+    qe1 :  P q₁ → exists-in-Q3 P
+    qe2 :  P q₂ → exists-in-Q3 P
+    qe3 :  P q₃ → exists-in-Q3 P
 
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
@@ -61,19 +64,43 @@
 Q3List : List Q3
 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
 
-decFN136 : (qs' : Q3 → Set)  → (q : Q3) →  exists-in-Q3 (λ q' → qs' q' ∧ (q' ≡ q₁)) → Dec (qs' q ∧ NF nfa136 q)
-decFN136 qs' q₁ (qe1 x) = yes x
-decFN136 qs' q₂ _ = no (λ ())
-decFN136 qs' q₃ _ = no (λ ())
+decs136 : (q : Q3) → Dec (start136 q)
+decs136 q₁ = yes refl
+decs136 q₂ = no (λ ())
+decs136 q₃ = no (λ ())
+
+open import Data.Empty
+open import Relation.Nullary
+open _∧_
+
+p136→ : (qs : Q3 → Set) → exists-in-Q3 (λ nq → qs nq ) →   qs q₁  ∨  qs q₂  ∨   qs q₃  
+p136→ qs (qe1 a) = case1 a 
+p136→ qs (qe2 a) = case2 (case1 a)
+p136→ qs (qe3 a) = case2 (case2 a)
+
+p136← : (qs : Q3 → Set) → qs q₁  ∨  qs q₂  ∨   qs q₃ → exists-in-Q3 (λ nq → qs nq ) 
+p136← qs (case1 a) = qe1 a
+p136← qs (case2 (case1 a)) = qe2 a
+p136← qs (case2 (case2 a)) = qe3 a
 
-decF̨δ136 :  (qs' : Q3 → Set) (s : Σ2) (t : List Σ2) 
-    → (a : naccept exists-in-Q3 nfa136 (λ q' → exists-in-Q3 (λ q₄ → qs' q₄ ∧ transition136 q₄ s q')) t)
-    → (q : Q3) → Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q s q') t)
-decF̨δ136 qs' s [] a q = {!!}
-decF̨δ136 qs' s (x ∷ t) a q = {!!}
+next136 : (qs : Q3 → Set) → ((q : Q3) → Dec (qs q)) → (x : Σ2) (q : Q3) →
+    Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
+next136 qs dec x q = {!!} where
+   ne1 : (q : Q3) → (x : Σ2) → Dec (qs q₁) → Dec (qs q₁ ∧ Nδ nfa136 q₁ x q)
+   ne1 q x ( no n)  = no ( λ not → n (proj1 not))
+   ne1 q₁ s0 (yes y) = yes [ y , d1 ]
+   ne1 q₁ s1 (yes y) = no (λ not → ne11 (proj2 not)) where
+     ne11 : ¬ Nδ nfa136 q₁ s1 q₁
+     ne11 ()
+   ne1 q₂ s0 (yes y) = no (λ not → ne12 (proj2 not)) where
+     ne12 : ¬ Nδ nfa136 q₁ s0 q₂
+     ne12 ()
+   ne1 q₂ s1 (yes y) = yes [ y , d0 ]
+   ne1 q₃ s0 (yes y) = {!!}
+   ne1 q₃ s1 (yes y) = {!!}
 
-nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3)
-nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' a' q → decFN136 qs' q a' ) (λ qs' s t a' q →  decF̨δ136 qs' s t a' q ) Q3List
+nfa136trace : (input : List Σ2 ) → naccept exists-in-Q3 nfa136 start136 input → List (List Q3)
+nfa136trace x a = ntrace exists-in-Q3 nfa136 start136 x a decs136 next136 Q3List
 
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ