Mercurial > hg > Members > kono > Proof > automaton

annotate 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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
1 module sbconst2 where
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 open import Level renaming ( suc to succ ; zero to Zero )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4 open import Data.Nat
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 open import Data.List
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
6 open import Data.Bool using ( Bool ; true ; false ; _∧_ )
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8 open import automaton
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
9 open import nfa
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open NAutomaton
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
11 open Automaton
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 open FiniteSet
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
14 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
15 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → nδ r i q )
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
17 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
18 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
19 subset-construction {Q} { Σ} {n} N NFA = record {
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
20 δ = λ q x → δconv N ( Nδ NFA ) q x
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
21 ; astart = astart1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
22 ; aend = aend1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
23 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
24 astart1 : Q → Bool
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25 astart1 = Nstart NFA
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
26 aend1 : (Q → Bool) → Bool
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
27 aend1 f = exists N ( λ q → f q ∧ Nend NFA q )
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
28
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
29 test4 = subset-construction finState1 am2
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
30
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
31 test5 = accept test4 ( i0 ∷ i1 ∷ i0 ∷ [] )
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
32 test6 = accept test4 ( i1 ∷ i1 ∷ i1 ∷ [] )