Mercurial > hg > Members > kono > Proof > automaton

comparison agda/sbconst2.agda @ 32:cd311109d63b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 agda/sbconst1.agda@08b589172493
children aa15eff1aeb3
comparison
equal deleted inserted replaced
31:9b00dc130ede 32:cd311109d63b
1 module sbconst2 where
2
3 open import Level renaming ( suc to succ ; zero to Zero )
4 open import Data.Nat
5 open import Data.List
6 open import Data.Bool using ( Bool ; true ; false ; _∧_ )
7
8 open import automaton
9 open import nfa
10 open NAutomaton
11 open Automaton
12 open FiniteSet
13
14 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
15 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → nδ r i q )
16
17 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
18 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
19 subset-construction {Q} { Σ} {n} N NFA = record {
20 δ = λ q x → δconv N ( Nδ NFA ) q x
21 ; astart = astart1
22 ; aend = aend1
23 } where
24 astart1 : Q → Bool
25 astart1 = Nstart NFA
26 aend1 : (Q → Bool) → Bool
27 aend1 f = exists N ( λ q → f q ∧ Nend NFA q )
28
29 test4 = subset-construction finState1 am2
30
31 test5 = accept test4 ( i0 ∷ i1 ∷ i0 ∷ [] )
32 test6 = accept test4 ( i1 ∷ i1 ∷ i1 ∷ [] )