Mercurial > hg > Members > kono > Proof > automaton

annotate automaton-in-agda/src/sbconst2.agda @ 205:e97cf4fb67fa

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Fri, 18 Jun 2021 21:09:50 +0900
parents 3fa72793620b
children 8006cbd87b20
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
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
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
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
13 open import Relation.Binary.PropositionalEquality hiding ( [_] )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
14
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
15 open Bool
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
17 δconv : { Q : Set } { Σ : Set } → ( ( Q → Bool ) → Bool ) → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
18 δ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
19
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
20 subset-construction : { Q : Set } { Σ : Set } →
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
21 ( ( Q → Bool ) → Bool ) →
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
22 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
23 subset-construction {Q} { Σ} exists NFA = record {
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
24 δ = λ q x → δconv exists ( Nδ NFA ) q x
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
25 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q )
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
26 }
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
27
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
28 test4 = subset-construction existsS1 am2
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
29
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
30 test51 = accept test4 start1 ( i0 ∷ i1 ∷ i0 ∷ [] )
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
31 test61 = accept test4 start1 ( i1 ∷ i1 ∷ i1 ∷ [] )
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
32
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
33 subset-construction-lemma→ : { Q : Set } { Σ : Set } { n : ℕ } → (exists : ( Q → Bool ) → Bool ) →
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
34 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool )
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
35 → (x : List Σ)
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
36 → Naccept NFA exists astart x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
37 → accept ( subset-construction exists NFA ) astart x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
38 subset-construction-lemma→ {Q} {Σ} {n} exists NFA astart x naccept = lemma1 x astart naccept where
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
39 lemma1 : (x : List Σ) → ( states : Q → Bool )
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
40 → Naccept NFA exists states x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
41 → accept ( subset-construction exists NFA ) states x ≡ true
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
42 lemma1 [] states naccept = naccept
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
43 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
44
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
45 subset-construction-lemma← : { Q : Set } { Σ : Set } { n : ℕ } → (exists : ( Q → Bool ) → Bool ) →
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
46 (NFA : NAutomaton Q Σ ) → (astart : Q → Bool )
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
47 → (x : List Σ)
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
48 → accept ( subset-construction exists NFA ) astart x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
49 → Naccept NFA exists astart x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
50 subset-construction-lemma← {Q} {Σ} {n} exists NFA astart x saccept = lemma2 x astart saccept where
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
51 lemma2 : (x : List Σ) → ( states : Q → Bool )
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
52 → accept ( subset-construction exists NFA ) states x ≡ true
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
53 → Naccept NFA exists states x ≡ true
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
54 lemma2 [] states saccept = saccept
141
b3f05cd08d24 clean up
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 70
diff changeset
55 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv exists (Nδ NFA) states h) saccept