Mercurial > hg > Members > kono > Proof > automaton
changeset 32:cd311109d63b
suset construction for subset function nfa
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Mon, 05 Nov 2018 18:37:23 +0900 |
| parents | 9b00dc130ede |
| children | f163122da10c |
| files | agda/sbconst2.agda |
| diffstat | 1 files changed, 32 insertions(+), 0 deletions(-) [+] |
line wrap: on
line diff
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/agda/sbconst2.agda Mon Nov 05 18:37:23 2018 +0900 @@ -0,0 +1,32 @@ +module sbconst2 where + +open import Level renaming ( suc to succ ; zero to Zero ) +open import Data.Nat +open import Data.List +open import Data.Bool using ( Bool ; true ; false ; _∧_ ) + +open import automaton +open import nfa +open NAutomaton +open Automaton +open FiniteSet + +δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) +δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → nδ r i q ) + +subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → + (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) +subset-construction {Q} { Σ} {n} N NFA = record { + δ = λ q x → δconv N ( Nδ NFA ) q x + ; astart = astart1 + ; aend = aend1 + } where + astart1 : Q → Bool + astart1 = Nstart NFA + aend1 : (Q → Bool) → Bool + aend1 f = exists N ( λ q → f q ∧ Nend NFA q ) + +test4 = subset-construction finState1 am2 + +test5 = accept test4 ( i0 ∷ i1 ∷ i0 ∷ [] ) +test6 = accept test4 ( i1 ∷ i1 ∷ i1 ∷ [] )