Mercurial > hg > Members > kono > Proof > automaton1
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) = {!!}