# HG changeset patch # User Shinji KONO # Date 1605418585 -32400 # Node ID ef43350ea0e242ef4fcd7c839bb41ae385ede1fa # Parent 8a6660c5b1dafa2657c06710127e2b77aaf9b0a4 ... diff -r 8a6660c5b1da -r ef43350ea0e2 nfa.agda --- 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 = {!!}