Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/sbconst2.agda @ 411:207e6c4e155c
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 29 Nov 2023 17:40:55 +0900 |
| parents | a60132983557 |
| children |
| rev | line source |
|---|---|
| 406 | 1 {-# OPTIONS --cubical-compatible --safe #-} |
| 405 | 2 |
|
32
cd311109d63b
suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
3 module sbconst2 where |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
4 |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
5 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
|
6 open import Data.Nat |
| 69 | 7 open import Data.Fin |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
8 open import Data.List |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
9 |
|
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
10 open import automaton |
|
32
cd311109d63b
suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
11 open import nfa |
| 69 | 12 open import logic |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
13 open NAutomaton |
|
32
cd311109d63b
suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
17
diff
changeset
|
14 open Automaton |
| 69 | 15 open import Relation.Binary.PropositionalEquality hiding ( [_] ) |
| 16 | |
| 17 open Bool | |
|
13
02b4ecc9972c
start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff
changeset
|
18 |
| 332 | 19 -- exits : check subset of Q ( Q → Bool) is not empty |
| 20 --- ( Q → Σ → Q → Bool ) transition of NFA | |
| 21 --- (Q → Bool) → Σ → (Q → Bool) generate transition of Automaton | |
| 22 | |
| 411 | 23 δconv : { Q : Set } { Σ : Set } → (exists :( Q → Bool ) → Bool ) → (nδ : Q → Σ → Q → Bool ) |
| 24 → (Q → Bool) → Σ → (Q → Bool) | |
| 141 | 25 δ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
|
26 |
| 141 | 27 subset-construction : { Q : Set } { Σ : Set } → |
| 28 ( ( Q → Bool ) → Bool ) → | |
| 29 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) | |
| 30 subset-construction {Q} { Σ} exists NFA = record { | |
| 31 δ = λ q x → δconv exists ( Nδ NFA ) q x | |
| 32 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) | |
| 70 | 33 } |
| 69 | 34 |
| 398 | 35 subset-construction' : { Q : Set } { Σ : Set } → |
| 36 ( ( Q → Bool ) → Bool ) → | |
| 37 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) | |
| 38 subset-construction' {Q} { Σ} exists NFA = record { | |
| 39 δ = λ f i q → exists ( λ r → f r /\ Nδ NFA r i q ) | |
| 40 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) | |
| 41 } | |
| 42 | |
| 141 | 43 test4 = subset-construction existsS1 am2 |
| 69 | 44 |
| 141 | 45 test51 = accept test4 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 46 test61 = accept test4 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 14 | 47 |
| 268 | 48 subset-construction-lemma→ : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 49 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 50 → (x : List Σ) |
| 141 | 51 → Naccept NFA exists astart x ≡ true |
| 52 → accept ( subset-construction exists NFA ) astart x ≡ true | |
| 268 | 53 subset-construction-lemma→ {Q} {Σ} exists NFA astart x naccept = lemma1 x astart naccept where |
| 69 | 54 lemma1 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 55 → Naccept NFA exists states x ≡ true |
| 56 → accept ( subset-construction exists NFA ) states x ≡ true | |
| 69 | 57 lemma1 [] states naccept = naccept |
| 141 | 58 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
|
59 |
| 268 | 60 subset-construction-lemma← : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 61 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 62 → (x : List Σ) |
| 141 | 63 → accept ( subset-construction exists NFA ) astart x ≡ true |
| 64 → Naccept NFA exists astart x ≡ true | |
| 268 | 65 subset-construction-lemma← {Q} {Σ} exists NFA astart x saccept = lemma2 x astart saccept where |
| 69 | 66 lemma2 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 67 → accept ( subset-construction exists NFA ) states x ≡ true |
| 68 → Naccept NFA exists states x ≡ true | |
| 69 | 69 lemma2 [] states saccept = saccept |
| 141 | 70 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept |
| 332 | 71 |
| 72 | |
| 73 |