Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/sbconst2.agda @ 392:23db567b4098
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Thu, 27 Jul 2023 09:03:13 +0900 |
| parents | 6f3636fbc481 |
| children | d7ea37e49f35 |
| 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 |
| 69 | 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 |
|
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 |
| 69 | 10 open import logic |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
11 open NAutomaton |
|
32
cd311109d63b
suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
12 open Automaton |
| 69 | 13 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 14 | |
| 15 open Bool | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
16 |
| 332 | 17 -- exits : check subset of Q ( Q → Bool) is not empty |
| 18 --- ( Q → Σ → Q → Bool ) transition of NFA | |
| 19 --- (Q → Bool) → Σ → (Q → Bool) generate transition of Automaton | |
| 20 | |
| 21 δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) | |
| 141 | 22 δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q ) |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
23 |
| 141 | 24 subset-construction : { Q : Set } { Σ : Set } → |
| 25 ( ( Q → Bool ) → Bool ) → | |
| 26 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) | |
| 27 subset-construction {Q} { Σ} exists NFA = record { | |
| 28 δ = λ q x → δconv exists ( Nδ NFA ) q x | |
| 29 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) | |
| 70 | 30 } |
| 69 | 31 |
| 141 | 32 test4 = subset-construction existsS1 am2 |
| 69 | 33 |
| 141 | 34 test51 = accept test4 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 35 test61 = accept test4 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 14 | 36 |
| 268 | 37 subset-construction-lemma→ : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 38 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 39 → (x : List Σ) |
| 141 | 40 → Naccept NFA exists astart x ≡ true |
| 41 → accept ( subset-construction exists NFA ) astart x ≡ true | |
| 268 | 42 subset-construction-lemma→ {Q} {Σ} exists NFA astart x naccept = lemma1 x astart naccept where |
| 69 | 43 lemma1 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 44 → Naccept NFA exists states x ≡ true |
| 45 → accept ( subset-construction exists NFA ) states x ≡ true | |
| 69 | 46 lemma1 [] states naccept = naccept |
| 141 | 47 lemma1 (h ∷ t ) states naccept = lemma1 t (δconv exists (Nδ NFA) states h) naccept |
|
32
cd311109d63b
suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
48 |
| 268 | 49 subset-construction-lemma← : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 50 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 51 → (x : List Σ) |
| 141 | 52 → accept ( subset-construction exists NFA ) astart x ≡ true |
| 53 → Naccept NFA exists astart x ≡ true | |
| 268 | 54 subset-construction-lemma← {Q} {Σ} exists NFA astart x saccept = lemma2 x astart saccept where |
| 69 | 55 lemma2 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 56 → accept ( subset-construction exists NFA ) states x ≡ true |
| 57 → Naccept NFA exists states x ≡ true | |
| 69 | 58 lemma2 [] states saccept = saccept |
| 141 | 59 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept |
| 332 | 60 |
| 61 | |
| 62 |