Mercurial > hg > Members > kono > Proof > automaton1
changeset 2:b4548639121e
ntrace
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Sat, 14 Nov 2020 09:27:57 +0900 (2020-11-14) |
parents | 7399aae907fc |
children | bf6d7843ba11 |
files | automaton.agda nfa.agda |
diffstat | 2 files changed, 64 insertions(+), 42 deletions(-) [+] |
line wrap: on
line diff
--- a/automaton.agda Fri Nov 13 13:03:56 2020 +0900 +++ b/automaton.agda Sat Nov 14 09:27:57 2020 +0900 @@ -15,8 +15,8 @@ open Automaton accept : {n : Level} {Q : Set n} {Σ : Set } → Automaton Q Σ → Q → List Σ → Set -accept {Q} {Σ} atm q [] = F atm q -accept {Q} {Σ} atm q (x ∷ input) = +accept {n} {Q} {Σ} atm q [] = F atm q +accept {n} {Q} {Σ} atm q (x ∷ input) = accept atm (δ atm q x ) input trace : {n : Level} {Q : Set n} {Σ : Set } → (A : Automaton Q Σ) → (start : Q) → (input : List Σ ) → accept A start input → List Q
--- a/nfa.agda Fri Nov 13 13:03:56 2020 +0900 +++ b/nfa.agda Sat Nov 14 09:27:57 2020 +0900 @@ -12,21 +12,30 @@ field Nδ : Q → Σ → Q → Set NF : Q → Set - Nexists : (Q → Set) → Set open NAutomaton +naccept : {n : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set) → Set) → NAutomaton Q Σ → (Q → Set) → List Σ → Set +naccept {n} {Q} {Σ} Nexists nfa qs [] = Nexists (λ q → qs q ∧ NF nfa q ) +naccept {n} {Q} {Σ} Nexists nfa qs (x ∷ input) = + naccept Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) input -naccept : {n : Level} {Q : Set n} {Σ : Set} → NAutomaton Q Σ → (Q → Set) → List Σ → Set -naccept {n} {Q} {Σ} nfa qs [] = Nexists nfa (λ q → qs q ∧ NF nfa q ) -naccept {n} {Q} {Σ} nfa qs (x ∷ input) = - Nexists nfa (λ q → qs q ∧ (naccept nfa (Nδ nfa q x) input )) +qlist : {n : Level} {Q : Set n} → (P : Q → Set ) → ((q : Q) → Dec ( P q)) → List Q → List Q +qlist P dec [] = [] +qlist P dec (q ∷ qs) with dec q +... | yes _ = q ∷ qlist P dec qs +... | no _ = qlist P dec qs -record DecStates {n : Level} ( Q : Set n ) : Set (Suc n) where - field - QList : List Q - QDec : (P : Q → Set) → (q : Q) → Dec (P q) - +ntrace : {n : Level} {Q : Set n} {Σ : Set } → (Nexists : (Q → Set) → Set) → (nfa : NAutomaton Q Σ) → (qs : Q → Set ) → (input : List Σ ) + → naccept Nexists nfa qs input + → ((qs : Q → Set) (q : Q) → Dec (qs q ∧ NF nfa q)) + → ((qs : Q → Set) (x : Σ) (t : List Σ) (q : Q) → Dec (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q') t)) + → List Q + → List (List Q) +ntrace {n} {Q} {Σ} Nexists nfa qs [] a decNF decNδ L = qlist (λ q → qs q ∧ NF nfa q) (decNF qs) L ∷ [] +ntrace {n} {Q} {Σ} Nexists nfa qs (x ∷ t) a decNF decNδ L = + qlist (λ q → (naccept Nexists nfa (λ q' → qs q ∧ Nδ nfa q x q' ) t )) (decNδ qs x t) L + ∷ ( ntrace Nexists nfa (λ q' → Nexists (λ q → qs q ∧ Nδ nfa q x q' )) t a decNF decNδ L ) data transition136 : Q3 → Σ2 → Q3 → Set where d0 : transition136 q₁ s1 q₂ @@ -40,53 +49,64 @@ start136 q = q ≡ q₁ nfa136 : NAutomaton Q3 Σ2 -nfa136 = record { Nδ = transition136 ; NF = λ q → q ≡ q₁ ; Nexists = exists-in-Q3 } +nfa136 = record { Nδ = transition136 ; NF = λ q → q ≡ q₁ } -example136-1 = naccept nfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) +example136-1 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) -example136-0 = naccept nfa136 start136 ( s0 ∷ [] ) +example136-0 = naccept exists-in-Q3 nfa136 start136 ( s0 ∷ [] ) -example136-2 = naccept nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] ) +example136-2 = naccept exists-in-Q3 nfa136 start136 ( s1 ∷ s0 ∷ s1 ∷ s0 ∷ s1 ∷ [] ) -nfa136-P : (q : Q3 → Set) → (input : List Σ2 ) → Dec (naccept nfa136 q input ) -nfa136-P q [] = {!!} -nfa136-P q (x ∷ t) = {!!} +nfa136-FN : (q : Q3 ) → Dec ( NF nfa136 q ) +nfa136-FN q₁ = yes refl +nfa136-FN q₂ = no (λ ()) +nfa136-FN q₃ = no (λ ()) Q3List : List Q3 Q3List = q₁ ∷ q₂ ∷ q₃ ∷ [] -nfa136trace : (q : Q3 → Set) → (input : List Σ2 ) → naccept nfa136 q input → List (List Q3) -nfa136trace q [] (qe1 [ proj1 , refl ]) = {!!} -nfa136trace q (x ∷ t) (qe1 [ proj1 , a ]) = {!!} -nfa136trace q (x ∷ t) (qe2 [ proj1 , a ]) = {!!} -nfa136trace q (x ∷ t) (qe3 [ proj1 , a ]) = {!!} +decFN136 : (qs qs' : Q3 → Set) → (x : List Σ2) → naccept exists-in-Q3 nfa136 qs x → (q : Q3) → Dec (qs' q ∧ NF nfa136 q) +decFN136 qs qs' (_ ∷ _) _ _ = {!!} +decFN136 qs qs' [] (qe1 x) q₁ = {!!} +decFN136 qs qs' [] _ q₂ = no (λ ()) +decFN136 qs qs' [] _ q₃ = no (λ ()) --- --- ((Q → Set) → Set) → ((Q → Set) → Set) → Set --- +decF̨δ136 : (qs qs' : Q3 → Set) (x : Σ2) (t : List Σ2) → naccept exists-in-Q3 nfa136 qs' t → (q : Q3) → + Dec (naccept exists-in-Q3 nfa136 (λ q' → qs' q ∧ Nδ nfa136 q x q') t) +decF̨δ136 qs qs' x t a q₁ = {!!} +decF̨δ136 qs qs' x t a q₂ = {!!} +decF̨δ136 qs qs' x t a q₃ = {!!} -data Nexists→exits {n : Level} { Q : Set n } {Σ : Set} ( NFA : NAutomaton Q Σ ) : ((Q → Set) → Set) → Set where - one-of : Nexists→exits NFA (Nexists NFA) +nfa136trace : (qs : Q3 → Set) → (input : List Σ2 ) → naccept exists-in-Q3 nfa136 qs input → List (List Q3) +nfa136trace qs x a = ntrace exists-in-Q3 nfa136 qs x a (λ qs' q → decFN136 qs qs' x a q ) (λ qs' x t q → decF̨δ136 qs qs' x {!!} a q) Q3List -subset-construction : {n : Level} { Q : Set n } { Σ : Set } → +subset-construction : {n : Level} { Q : Set n } { Σ : Set } → (Nexists : (Q → Set) → Set) → (NAutomaton Q Σ ) → Automaton {Suc Zero ⊔ n} (Q → Set) Σ -subset-construction {n} {Q} { Σ} NFA = record { - δ = λ qs x qs → Nexists NFA (λ q → Nδ NFA q x qs ) - ; F = λ qs → Nexists NFA ( λ q → NF NFA q ) +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 ) } +dfa136 : Automaton (Q3 → Set) Σ2 +dfa136 = subset-construction exists-in-Q3 nfa136 + +t136 : accept dfa136 start136 (s0 ∷ s1 ∷ s0 ∷ s0 ∷ []) → List ( Q3 → Set ) +t136 = trace dfa136 start136 ( s0 ∷ s1 ∷ s0 ∷ s0 ∷ [] ) + subset-construction-lemma→ : { Q : Set } { Σ : Set } → + (Nexists : (Q → Set) → Set) → (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) → (x : List Σ) - → naccept NFA ( λ q1 → astart q1) x - → accept ( subset-construction NFA ) ( λ q1 → astart q1) x + → naccept Nexists NFA ( λ q1 → astart q1) x + → accept ( subset-construction Nexists NFA ) ( λ q1 → astart q1) x subset-construction-lemma→ = {!!} subset-construction-lemma← : { Q : Set } { Σ : Set } → + (Nexists : (Q → Set) → Set) → (NFA : NAutomaton Q Σ ) → (astart : Q → Set ) → (x : List Σ) - → accept ( subset-construction NFA ) ( λ q1 → astart q1) x - → naccept NFA ( λ q1 → astart q1) x + → accept ( subset-construction Nexists NFA ) ( λ q1 → astart q1) x + → naccept Nexists NFA ( λ q1 → astart q1) x subset-construction-lemma← = {!!} open import regular-language @@ -95,11 +115,11 @@ open Automaton open import Data.Empty --- Concat-exists : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → (states A ∨ states B → Set) → Set --- Concat-exists {n} {Σ} A B P = exists (automaton A) (λ q → P (case1 q)) ∨ exists (automaton B) (λ q → P (case2 q)) +Union-Nexists : {n m : Level} → {A : Set n} → {B : Set m} → ( (A → Set) → Set )→ ( (B → Set) → Set ) → ( (A ∨ B → Set) → Set ) +Union-Nexists {n} {m} {A} {B} PA PB P = PA (λ q → P (case1 q)) ∨ PB (λ q → P (case2 q)) -Concat-NFA : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ -Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend ; Nexists = {!!} } +Concat-NFA : {n : Level} {Σ : Set} → (A B : RegularLanguage {n} Σ ) → NAutomaton (states A ∨ states B) Σ +Concat-NFA {n} {Σ} A B = record { Nδ = δnfa ; NF = nend } module Concat-NFA where data δnfa : states A ∨ states B → Σ → states A ∨ states B → Set where a-case : {q : states A} {i : Σ } → δnfa ( case1 q) i (case1 (δ (automaton A) q i)) @@ -113,8 +133,10 @@ this : (a : states A) → state-is A a closed-in-concat : {n : Level} {Σ : Set } → (A B : RegularLanguage {n} Σ ) → ( x : List Σ ) + (PA : (states A → Set) → Set) + (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 ( Concat-NFA A B )} + ; automaton = subset-construction (Union-Nexists PA PB) ( Concat-NFA A B )} closed-in-concat {Σ} A B x = {!!}