changeset 8:894feefc3084

subset construction lemma
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sun, 15 Nov 2020 11:30:49 +0900
parents 8f1828ec8d1b
children 8a6660c5b1da
files logic.agda nfa-lib.agda nfa.agda regular-language.agda
diffstat 4 files changed, 117 insertions(+), 77 deletions(-) [+]
line wrap: on
line diff
--- a/logic.agda	Sat Nov 14 19:10:03 2020 +0900
+++ b/logic.agda	Sun Nov 15 11:30:49 2020 +0900
@@ -26,6 +26,9 @@
 _⇔_ : {n m : Level } → ( A : Set n ) ( B : Set m )  → Set (n ⊔ m)
 _⇔_ A B =  ( A → B ) ∧ ( B → A )
 
+id : {n : Level} {A : Set n} → A → A
+id x = x
+
 contra-position : {n m : Level } {A : Set n} {B : Set m} → (A → B) → ¬ B → ¬ A
 contra-position {n} {m} {A} {B}  f ¬b a = ¬b ( f a )
 
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/nfa-lib.agda	Sun Nov 15 11:30:49 2020 +0900
@@ -0,0 +1,76 @@
+module nfa-lib where
+open import Level renaming ( suc to Suc ; zero to Zero )
+
+open import Relation.Binary.PropositionalEquality 
+open import Data.List
+open import Relation.Nullary
+open import automaton
+open import logic
+
+open import nfa
+open NAutomaton
+
+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
+
--- 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) = {!!}
 
 
 
--- a/regular-language.agda	Sat Nov 14 19:10:03 2020 +0900
+++ b/regular-language.agda	Sun Nov 15 11:30:49 2020 +0900
@@ -2,7 +2,7 @@
 module regular-language where
 
 open import Level renaming ( suc to Suc ; zero to Zero )
-open import Data.List 
+open import Data.List  hiding ([_])
 -- open import Data.Nat hiding ( _≟_ )
 -- open import Data.Bool 
 -- open import Data.Fin hiding ( _+_ )
@@ -60,8 +60,8 @@
 test-AB→split {_} {A} {B} = refl
 
 open RegularLanguage 
-isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set (Suc Zero)
-isRegular A x r = A x ≡ contain r x 
+isRegular : {n : Level} {Σ : Set} → (A : language {Σ} ) → ( x : List Σ ) → (r : RegularLanguage {n} Σ ) → Set 
+isRegular A x r = A x ⇔ contain r x 
 
 M-Union : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → RegularLanguage Σ
 M-Union {n} {Σ} A B = record {
@@ -73,16 +73,18 @@
         }
    }  
 
+open _∧_
+
 closed-in-union :  {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) → isRegular (Union (contain A) (contain B)) x ( M-Union A B )
 closed-in-union A B [] = lemma where
-   lemma : F (automaton A) (astart A) ∨ F (automaton B) (astart B) ≡
-           F (automaton A) (astart A) ∨ F (automaton B) (astart B)
-   lemma = refl
+   lemma : (F (automaton A) (astart A) ∨ F (automaton B) (astart B)) ⇔
+           (F (automaton A) (astart A) ∨ F (automaton B) (astart B))
+   lemma = [ id , id ]
 closed-in-union {n} {Σ} A B ( h ∷ t ) = lemma4 t ((δ (automaton A) (astart A) h)) ((δ (automaton B) (astart B) h)) where
    lemma4 : (t : List Σ) → (qa : states A ) → (qb : states B ) → 
-     accept (automaton A) qa t ∨ accept (automaton B) qb  t
-       ≡ accept (automaton (M-Union A B)) (qa , qb) t
-   lemma4 [] qa qb = refl
+     (accept (automaton A) qa t ∨ accept (automaton B) qb  t)
+       ⇔ accept (automaton (M-Union A B)) (qa , qb) t
+   lemma4 [] qa qb = [ id , id ]
    lemma4 (h ∷ t ) qa qb = lemma4 t ((δ (automaton A) qa h)) ((δ (automaton B) qb h))
 
 -- closed-in-concat :  {Σ : Set} → (A B : RegularLanguage Σ ) → ( x : List Σ ) → isRegular (Concat (contain A) (contain B)) x {!!}