Mercurial > hg > Members > kono > Proof > automaton

annotate agda/sbconst1.agda @ 84:29d81bcff049

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
found done
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Sat, 09 Nov 2019 07:47:32 +0900
parents aa15eff1aeb3
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module sbconst1 where
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 )
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
4 open import Data.Nat hiding ( _≟_ )
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
5 open import Data.Fin
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6 open import Data.List
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7 open import Data.Maybe
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
8 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
9 open import Relation.Binary.PropositionalEquality hiding ( [_] )
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10 open import Relation.Nullary using (¬_; Dec; yes; no)
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
11 open import Data.Product
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
12 open import finiteSet
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open import automaton
34
a904b6bc76af add regular language
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
15 open import nfa-list
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 open Automaton
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17 open NAutomaton
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 open FiniteSet
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
21 list2sbst : {Q : Set} { n : ℕ } → FiniteSet Q {n} → List Q → Q → Bool
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 list2sbst N [] _ = false
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
23 list2sbst N ( h ∷ t ) q with F←Q N q ≟ F←Q N h
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24 ... | yes _ = true
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 ... | no _ = list2sbst N t q
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
28 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → List Q ) → (Q → Bool) → Σ → (Q → Bool)
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
29 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r ∧ list2sbst N (nδ r i) q )
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
30
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 34
diff changeset
31 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
32 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
33 subset-construction {Q} { Σ} {n} N NFA = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
34 δ = λ q x → δconv N ( nδ NFA ) q x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
35 ; astart = astart1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
36 ; aend = aend1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
37 } where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
38 astart1 : Q → Bool
15
54382de19264 sbconst1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
39 astart1 = list2sbst N [ nstart NFA ]
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
40 aend1 : (Q → Bool) → Bool
15
54382de19264 sbconst1 done
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 14
diff changeset
41 aend1 f = exists N f
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
42