Mercurial > hg > Members > kono > Proof > automaton1

changeset 9:8a6660c5b1da

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
FindQ
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Nov 2020 13:09:22 +0900
parents 894feefc3084
children ef43350ea0e2
files nfa-lib.agda nfa.agda
diffstat 2 files changed, 46 insertions(+), 13 deletions(-) [+]
line wrap: on
line diff
--- a/nfa-lib.agda	Sun Nov 15 11:30:49 2020 +0900
+++ b/nfa-lib.agda	Sun Nov 15 13:09:22 2020 +0900
@@ -10,6 +10,9 @@
 open import nfa
 open NAutomaton
 
+Q3List : List Q3
+Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
+
 decs136 : (q : Q3) → Dec (start136 q)
 decs136 q₁ = yes refl
 decs136 q₂ = no (λ ())
@@ -71,6 +74,10 @@
 nfa136trace x a = ntrace exists-in-Q3 nfa136 start136 x a decs136 next136 Q3List
 
 postulate
+   nfa13rs0 : example136-0 
    nfa13rs1 : example136-1 
+   nfa13rs2 : example136-2 
+
+nfa13rt0 = nfa136trace ( s0 ∷ []  ) nfa13rs0
 nfa13rt1 = nfa136trace ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) nfa13rs1
-
+nfa13rt2 = nfa136trace ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] ) nfa13rs2
--- a/nfa.agda	Sun Nov 15 11:30:49 2020 +0900
+++ b/nfa.agda	Sun Nov 15 13:09:22 2020 +0900
@@ -17,9 +17,9 @@
 open NAutomaton
 
 naccept : {n  : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set)  → Set) → NAutomaton Q Σ → (Q → Set) → List Σ → Set 
-naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ q → qs q ∧ NF nfa q )
+naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ p → qs p ∧ NF nfa p )
 naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = 
-    naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' ))  input
+    naccept Nexists nfa (λ p' → Nexists (λ p → qs p ∧ Nδ nfa p x p' ))  input
 
 qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q))  → List Q → List Q
 qlist P dec [] = []
@@ -42,6 +42,27 @@
     qe2 :  P q₂ → exists-in-Q3 P
     qe3 :  P q₃ → exists-in-Q3 P
 
+record FindQ {n : Level} (Q : Set n) (Nexists : (Q → Set)  → Set) : Set (Suc n) where
+    field
+       create : (P : Q → Set) (q : Q ) → P q  → Nexists (λ q → P q) 
+       found  : (P : Q → Set) → Nexists (λ q → P q) → Q
+       exists : (P : Q → Set) → (n : Nexists (λ q → P q)) → P (found P n)
+
+FindQ3 : FindQ Q3 exists-in-Q3
+FindQ3 = record { create = create ;  found = found ; exists = exists } where
+    create :  (P : Q3 → Set) (q : Q3) → P q → exists-in-Q3 P
+    create P q₁ p = qe1 p
+    create P q₂ p = qe2 p
+    create P q₃ p = qe3 p
+    found : (P : Q3 → Set) → exists-in-Q3 P → Q3
+    found P (qe1 x) = q₁
+    found P (qe2 x) = q₂
+    found P (qe3 x) = q₃
+    exists : (P : Q3 → Set) (n : exists-in-Q3 P) → P (found P n)
+    exists P (qe1 x) = x
+    exists P (qe2 x) = x
+    exists P (qe3 x) = x
+
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
     d1 : transition136 q₁ s0 q₁ 
@@ -62,9 +83,6 @@
 
 example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1  ∷ s0  ∷ s1 ∷ s0 ∷ s1 ∷ [] )
 
-Q3List : List Q3
-Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
-
 subset-construction : {n : Level} { Q : Set n } { Σ : Set  }   → (Nexists : (Q → Set)  → Set) → 
     (NAutomaton Q  Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ 
 subset-construction {n} {Q} { Σ} Nexists  nfa = record {
@@ -76,7 +94,7 @@
 dfa136 = subset-construction  exists-in-Q3 nfa136
 
 t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set )
-t136 = trace dfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) 
+t136 = trace  dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) 
 
 open _∧_
 
@@ -124,11 +142,12 @@
    this : (a : states A)  → state-is A a
 
 closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
-   (PA : (states A  → Set)  → Set) 
-   (PB : (states B  → Set)  → Set) 
+   (PA : (states A  → Set)  → Set) (FA : FindQ (states A) PA)
+   (PB : (states B  → Set)  → Set) (FB : FindQ (states B) PB)
    → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
-closed-in-concat {n} {Σ} A B x PA PB =  [ closed-in-concat→ x , closed-in-concat← x ] where
+closed-in-concat {n} {Σ} A B x PA FA PB FB =  [ closed-in-concat→ x , closed-in-concat← x ] where
+    open FindQ 
     fa : RegularLanguage  Σ
     fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A (astart A)
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
@@ -136,14 +155,21 @@
     closed-in-concat→ [] c = cc1 c where
         cc1 : contain A [] ∧ contain B [] → 
                 PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
-        cc1 ctab = case1 {!!}
+        cc1 ctab = case1 (create FA _ (astart A) [ this (astart A) , [ proj1 ctab , proj2 ctab ] ] )
     closed-in-concat→ (x ∷ t) = {!!}
     closed-in-concat← : (x : List Σ) → contain fa x → Concat {n} {Σ} (contain A) (contain B) x
     closed-in-concat← [] cn = cc2 cn where
         cc2 : PA (λ q → astart fa (case1 q) ∧ NF (Concat-NFA A B) (case1 q)) ∨ PB (λ q → astart fa (case2 q) ∧ NF (Concat-NFA A B) (case2 q))
             →   contain A [] ∧ contain B [] 
-        cc2 (case1 ca) = {!!}
-        cc2 (case2 cb) = {!!}
+        -- ca : PA (λ q → state-is A (astart A) ∧ F (automaton A) q ∧ F (automaton B) (astart B))
+        cc2 (case1 ca) = [ cc4 , proj2 (proj2 (exists FA _ ca)) ] where
+           cc5 : found FA _ ca ≡ astart A
+           cc5 = {!!}
+           cc4 : accept (automaton A) (astart A) []
+           cc4 = {!!}
+           cc3 : accept (automaton A) (found FA _ ca ) []
+           cc3 = proj1 (proj2 (exists FA _ ca)) 
+        cc2 (case2 cb) = [ {!!} , {!!} ]
     closed-in-concat← (x ∷ t) = {!!}