# HG changeset patch # User Shinji KONO # Date 1605407449 -32400 # Node ID 894feefc3084ef47a147b5ff2984b98e0f33d5c3 # Parent 8f1828ec8d1bdb21ea8c7957c5f17bd0251e9bf8 subset construction lemma diff -r 8f1828ec8d1b -r 894feefc3084 logic.agda --- 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 ) diff -r 8f1828ec8d1b -r 894feefc3084 nfa-lib.agda --- /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 + diff -r 8f1828ec8d1b -r 894feefc3084 nfa.agda --- 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) = {!!} diff -r 8f1828ec8d1b -r 894feefc3084 regular-language.agda --- 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 {!!}