diff nfa.agda @ 8:894feefc3084

subset construction lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Nov 2020 11:30:49 +0900 (2020-11-15)
parents 8f1828ec8d1b
children 8a6660c5b1da
line wrap: on
line diff
--- a/nfa.agda	Sat Nov 14 19:10:03 2020 +0900
+++ b/nfa.agda	Sun Nov 15 11:30:49 2020 +0900
@@ -1,3 +1,4 @@
+{-# OPTIONS --allow-unsolved-metas #-} 
 module nfa where
 open import Level renaming ( suc to Suc ; zero to Zero )
 
@@ -64,75 +65,11 @@
 Q3List : List Q3
 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ []
 
-decs136 : (q : Q3) → Dec (start136 q)
-decs136 q₁ = yes refl
-decs136 q₂ = no (λ ())
-decs136 q₃ = no (λ ())
-
-dect136 : (x : Σ2)  → (nq q : Q3)  →  Dec (Nδ nfa136 nq x q) 
-dect136 s0 q₁ q₁ = yes d1
-dect136 s0 q₁ q₂ = no (λ ())
-dect136 s0 q₁ q₃ =  no (λ ())
-dect136 s0 q₂ q₁ =  no (λ ())
-dect136 s0 q₂ q₂ =  yes d2
-dect136 s0 q₂ q₃ =  yes d3
-dect136 s0 q₃ q₁ =  yes d5
-dect136 s0 q₃ q₂ =  no (λ ())
-dect136 s0 q₃ q₃ =  no (λ ())
-dect136 s1 q₁ q₁ =  no (λ ())
-dect136 s1 q₁ q₂ =  yes d0
-dect136 s1 q₁ q₃ =  no (λ ())
-dect136 s1 q₂ q₁ =  no (λ ())
-dect136 s1 q₂ q₂ =  no (λ ())
-dect136 s1 q₂ q₃ =  yes d4
-dect136 s1 q₃ q₁ =  no (λ ())
-dect136 s1 q₃ q₂ =  no (λ ())
-dect136 s1 q₃ q₃ =  no (λ ())
-
-open import Data.Empty
-open import Relation.Nullary
-open _∧_
-
-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 = ne0 where
-   ne1 : (q : Q3) → (x : Σ2) → Dec (qs q₁) → Dec (Nδ nfa136 q₁ x q) → Dec (qs q₁ ∧ Nδ nfa136 q₁ x q)
-   ne1 q x (no n) _ = no (λ not → n (proj1 not))
-   ne1 q x _ (no n) = no (λ not → n (proj2 not))
-   ne1 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
-   ne2 : (q : Q3) → (x : Σ2) → Dec (qs q₂) → Dec (Nδ nfa136 q₂ x q) → Dec (qs q₂ ∧ Nδ nfa136 q₂ x q)
-   ne2 q x (no n) _ = no (λ not → n (proj1 not))
-   ne2 q x _ (no n) = no (λ not → n (proj2 not))
-   ne2 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
-   ne3 : (q : Q3) → (x : Σ2) → Dec (qs q₃) → Dec (Nδ nfa136 q₃ x q) → Dec (qs q₃ ∧ Nδ nfa136 q₃ x q)
-   ne3 q x (no n) _ = no (λ not → n (proj1 not))
-   ne3 q x _ (no n) = no (λ not → n (proj2 not))
-   ne3 q x (yes y0) (yes y1) = yes [ y0 , y1 ]
-   ne0 : Dec (exists-in-Q3 (λ nq → qs nq ∧ Nδ nfa136 nq x q))
-   ne0 with ne1 q x (dec q₁) (dect136 x q₁ q)
-   ... | yes y = yes ( qe1 y)
-   ... | no n with ne2 q x (dec q₂) (dect136 x q₂ q)
-   ... | yes y2 = yes (qe2 y2)
-   ... | no n2 with ne3 q x (dec q₃) (dect136 x q₃ q)
-   ... | yes y3 = yes (qe3 y3)
-   ... | no n3 = no ne4 where
-      ne4 : ¬ exists-in-Q3 (λ nq → qs nq ∧ transition136 nq x q)
-      ne4 (qe1 x) = n x
-      ne4 (qe2 x) = n2 x
-      ne4 (qe3 x) = n3 x
-
-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
-
-postulate
-   nfa13rs1 : example136-1 
-nfa13rt1 = nfa136trace ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) nfa13rs1
-
 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 {
         δ = λ qs x q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )
-     ;  F = λ qs → Nexists ( λ q → NF nfa q )
+     ;  F = λ qs → Nexists ( λ q → qs q ∧ NF nfa q )
    } 
 
 dfa136 : Automaton (Q3 → Set) Σ2
@@ -141,13 +78,17 @@
 t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set )
 t136 = trace dfa136 start136 ( s0  ∷ s1  ∷ s0 ∷ s0 ∷ [] ) 
 
+open _∧_
+
 subset-construction-lemma→ : { Q : Set } { Σ : Set  }   →   
     (Nexists : (Q → Set)  → Set) →
     (NFA : NAutomaton Q  Σ ) → (astart : Q → Set )
     → (x : List Σ)
     → naccept Nexists NFA ( λ q1 → astart q1) x 
     → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
-subset-construction-lemma→ = {!!}
+subset-construction-lemma→ {Q} {Σ} Nexists nfa qs [] na = na
+subset-construction-lemma→ {Q} {Σ} Nexists nfa qs (x ∷ t) na = 
+   subset-construction-lemma→ Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t na 
 
 subset-construction-lemma← : { Q : Set } { Σ : Set  }   → 
     (Nexists : (Q → Set)  → Set) →
@@ -155,7 +96,9 @@
     → (x : List Σ)
     → accept (  subset-construction Nexists NFA ) ( λ q1 → astart q1) x 
     → naccept Nexists NFA ( λ q1 →  astart q1) x 
-subset-construction-lemma← = {!!}
+subset-construction-lemma← {Q} {Σ} Nexists nfa qs [] a = a 
+subset-construction-lemma← {Q} {Σ} Nexists nfa qs (x ∷ t) a = 
+   subset-construction-lemma← Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a 
 
 open import regular-language 
 
@@ -185,7 +128,23 @@
    (PB : (states B  → Set)  → Set) 
    → 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 {Σ} A B x = {!!}
+closed-in-concat {n} {Σ} A B x PA PB =  [ closed-in-concat→ x , closed-in-concat← x ] where
+    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 )}
+    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 {!!}
+    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) = {!!}
+    closed-in-concat← (x ∷ t) = {!!}