Mercurial > hg > Members > kono > Proof > automaton

annotate agda/sbconst2.agda @ 76:7b357b295272

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, 08 Nov 2019 13:40:25 +0900
parents 702ce92c45ab
children b3f05cd08d24
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
44
aa15eff1aeb3 seprate finite
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 32
diff changeset
13 open import finiteSet
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14 open FiniteSet
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
15 open import Relation.Binary.PropositionalEquality hiding ( [_] )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
16
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
17
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
18 open Bool
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
20 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool)
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
21 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
22
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
23 open FiniteSet
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
32
cd311109d63b suset construction for subset function nfa
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 17
diff changeset
25 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} →
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
26 (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
27 subset-construction {Q} { Σ} {n} fin NFA astart = record {
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
28 δ = λ q x → δconv fin ( Nδ NFA ) q x
70
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
29 ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q )
702ce92c45ab add concat
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 69
diff changeset
30 }
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
31
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
32 am2start = λ q1 → equal? finState1 ss q1
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
33
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
34 test4 = subset-construction finState1 am2 ss
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
35
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
36 test5 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i0 ∷ i1 ∷ i0 ∷ [] )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
37 test6 = accept test4 ( λ q1 → equal? finState1 ss q1) ( i1 ∷ i1 ∷ i1 ∷ [] )
14
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
38
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
39 subset-construction-lemma→ : { Q : Set } { Σ : Set } { n : ℕ } → (fin : FiniteSet Q {n} ) →
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
40 (NFA : NAutomaton Q Σ ) → (astart : Q )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
41 → (x : List Σ)
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
42 → Naccept NFA fin ( λ q1 → equal? fin astart q1) x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
43 → accept ( subset-construction fin NFA astart ) ( λ q1 → equal? fin astart q1) x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
44 subset-construction-lemma→ {Q} {Σ} {n} fin NFA astart x naccept = lemma1 x ( λ q1 → equal? fin astart q1) naccept where
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
45 lemma1 : (x : List Σ) → ( states : Q → Bool )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
46 → Naccept NFA fin states x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
47 → accept ( subset-construction fin NFA astart ) states x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
48 lemma1 [] states naccept = naccept
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
49 lemma1 (h ∷ t ) states naccept = lemma1 t (δconv fin (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
50
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
51 subset-construction-lemma← : { Q : Set } { Σ : Set } { n : ℕ } → (fin : FiniteSet Q {n} ) →
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
52 (NFA : NAutomaton Q Σ ) → (astart : Q )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
53 → (x : List Σ)
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
54 → accept ( subset-construction fin NFA astart ) ( λ q1 → equal? fin astart q1) x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
55 → Naccept NFA fin ( λ q1 → equal? fin astart q1) x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
56 subset-construction-lemma← {Q} {Σ} {n} fin NFA astart x saccept = lemma2 x ( λ q1 → equal? fin astart q1) saccept where
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
57 lemma2 : (x : List Σ) → ( states : Q → Bool )
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
58 → accept ( subset-construction fin NFA astart ) states x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
59 → Naccept NFA fin states x ≡ true
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
60 lemma2 [] states saccept = saccept
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 44
diff changeset
61 lemma2 (h ∷ t ) states saccept = lemma2 t (δconv fin (Nδ NFA) states h) saccept