Mercurial > hg > Members > kono > Proof > automaton
annotate automaton-in-agda/src/sbconst2.agda @ 406:a60132983557
...
| author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
|---|---|
| date | Wed, 08 Nov 2023 21:35:54 +0900 |
| parents | af8f630b7e60 |
| children | 207e6c4e155c |
| 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 | |
| 23 δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool) | |
| 141 | 24 δ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
|
25 |
| 141 | 26 subset-construction : { Q : Set } { Σ : Set } → |
| 27 ( ( Q → Bool ) → Bool ) → | |
| 28 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) | |
| 29 subset-construction {Q} { Σ} exists NFA = record { | |
| 30 δ = λ q x → δconv exists ( Nδ NFA ) q x | |
| 31 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) | |
| 70 | 32 } |
| 69 | 33 |
| 398 | 34 subset-construction' : { Q : Set } { Σ : Set } → |
| 35 ( ( Q → Bool ) → Bool ) → | |
| 36 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ ) | |
| 37 subset-construction' {Q} { Σ} exists NFA = record { | |
| 38 δ = λ f i q → exists ( λ r → f r /\ Nδ NFA r i q ) | |
| 39 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q ) | |
| 40 } | |
| 41 | |
| 141 | 42 test4 = subset-construction existsS1 am2 |
| 69 | 43 |
| 141 | 44 test51 = accept test4 start1 ( i0 ∷ i1 ∷ i0 ∷ [] ) |
| 45 test61 = accept test4 start1 ( i1 ∷ i1 ∷ i1 ∷ [] ) | |
| 14 | 46 |
| 268 | 47 subset-construction-lemma→ : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 48 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 49 → (x : List Σ) |
| 141 | 50 → Naccept NFA exists astart x ≡ true |
| 51 → accept ( subset-construction exists NFA ) astart x ≡ true | |
| 268 | 52 subset-construction-lemma→ {Q} {Σ} exists NFA astart x naccept = lemma1 x astart naccept where |
| 69 | 53 lemma1 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 54 → Naccept NFA exists states x ≡ true |
| 55 → accept ( subset-construction exists NFA ) states x ≡ true | |
| 69 | 56 lemma1 [] states naccept = naccept |
| 141 | 57 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
|
58 |
| 268 | 59 subset-construction-lemma← : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool ) → |
| 141 | 60 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool ) |
| 69 | 61 → (x : List Σ) |
| 141 | 62 → accept ( subset-construction exists NFA ) astart x ≡ true |
| 63 → Naccept NFA exists astart x ≡ true | |
| 268 | 64 subset-construction-lemma← {Q} {Σ} exists NFA astart x saccept = lemma2 x astart saccept where |
| 69 | 65 lemma2 : (x : List Σ) → ( states : Q → Bool ) |
| 141 | 66 → accept ( subset-construction exists NFA ) states x ≡ true |
| 67 → Naccept NFA exists states x ≡ true | |
| 69 | 68 lemma2 [] states saccept = saccept |
| 141 | 69 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept |
| 332 | 70 |
| 71 | |
| 72 |