changeset 10:ef43350ea0e2

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Nov 2020 14:36:25 +0900
parents 8a6660c5b1da
children 554fa6e5a09d
files nfa.agda
diffstat 1 files changed, 48 insertions(+), 31 deletions(-) [+]
line wrap: on
line diff
--- a/nfa.agda	Sun Nov 15 13:09:22 2020 +0900
+++ b/nfa.agda	Sun Nov 15 14:36:25 2020 +0900
@@ -44,24 +44,24 @@
 
 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)
+       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 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
+    create :  {P : Q3 → Set} (q : Q3) → P q → exists-in-Q3 P
+    create q₁ p = qe1 p
+    create q₂ p = qe2 p
+    create q₃ p = qe3 p
+    found : {P : Q3 → Set} → exists-in-Q3 P → Q3
+    found (qe1 x) = q₁
+    found (qe2 x) = q₂
+    found (qe3 x) = q₃
+    exists : {P : Q3 → Set} (n : exists-in-Q3 P) → P (found n)
+    exists (qe1 x) = x
+    exists (qe2 x) = x
+    exists (qe3 x) = x
 
 data transition136 : Q3  → Σ2  → Q3 → Set  where
     d0 : transition136 q₁ s1 q₂ 
@@ -138,39 +138,56 @@
        nend (case2 q) = F (automaton B) q
        nend (case1 q) = F (automaton A) q ∧ F (automaton B) (astart B) -- empty B case
 
-data state-is {n : Level} {Σ : Set }  (A : RegularLanguage {n} Σ ) : (a : states A ) → Set where
-   this : (a : states A)  → state-is A a
+data state-is {n : Level} {Σ : Set }  (A B : RegularLanguage {n} Σ ) : (q : states A ∨ states B ) → Set where
+   this : state-is A B (case1 (astart A))
+
+record Split {Σ : Set} (A : List Σ → Set ) ( B : List Σ → Set ) (x :  List Σ ) : Set where
+    field
+        sp0 : List Σ
+        sp1 : List Σ
+        sp-concat : sp0 ++ sp1 ≡ x
+        prop0 : A sp0 
+        prop1 : B sp1 
+
+open Split
+split→AB :  {Σ : Set} → (A B : List Σ → Set ) → ( x : List Σ ) → split A B x → Split A B x
+split→AB A B [] sp = record { sp0 = [] ; sp1 = [] ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp }
+split→AB A B (x ∷ t) (case1 sp) = record { sp0 = [] ; sp1 = x ∷ t ; sp-concat = refl ; prop0 = proj1 sp ; prop1 = proj2 sp } 
+split→AB A B (x ∷ t) (case2 sp) with split→AB  (λ t1 → A ( x ∷ t1 )) B t sp
+... | Sn = record { sp0 = x ∷ sp0 Sn ; sp1 = sp1 Sn ; sp-concat = cong (λ k → x ∷ k) (sp-concat Sn) ; prop0 = prop0 Sn ; prop1 = prop1 Sn } 
 
 closed-in-concat :  {n : Level} {Σ : Set } → (A B : RegularLanguage {n}  Σ ) → ( x : List Σ ) 
    (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)
+   → isRegular (Concat {n} (contain A) (contain B)) x record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
 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)
+    fa = record {states = states A ∨ states B → Set ; astart = λ q → state-is A B q
          ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )}
     closed-in-concat→ : (x : List Σ) → Concat {n} {Σ} (contain A) (contain B) x → contain fa x
     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 (create FA _ (astart A) [ this (astart A) , [ proj1 ctab , proj2 ctab ] ] )
-    closed-in-concat→ (x ∷ t) = {!!}
+        cc1 ctab = case1 (create FA (astart A) [ this , [ proj1 ctab , proj2 ctab ] ] )
+    -- fina : (F (automaton A) (astart A) ∧ accept (automaton B) (δ (automaton B) (astart B) x) t) 
+    closed-in-concat→ (x ∷ t) (case1 fina ) = {!!}
+    -- sp :  split (λ t1 → accept (automaton A) (δ (automaton A) (astart A) x) t1) (λ x₁ → accept (automaton B) (astart B) x₁) t
+    closed-in-concat→ (x ∷ t) (case2 sp ) = {!!}
     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 [] 
-        -- 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) = {!!}
+        -- ca : PA (λ q → state-is A B (case1 q) ∧ F (automaton A) q ∧ F (automaton B) (astart B))
+        cc2 (case1 ca) = [ subst (λ k → accept (automaton A) k [] ) (cc5 _ (proj1 (exists FA ca))) cc3 , proj2 (proj2 (exists FA ca)) ] where
+           cc5 : (q : states A) → state-is A B (case1 q) → q ≡ astart A
+           cc5 q this = refl
+           cc3 : accept (automaton A) (found FA ca ) []
+           cc3 = proj1 (proj2 (exists FA  ca)) 
+        cc2 (case2 cb) with proj1 (exists FB  cb)
+        ... | ()
+    closed-in-concat← (x ∷ t) cn = {!!}