Mercurial > hg > Members > kono > Proof > automaton

annotate agda/automaton.agda @ 24:9406c2571fe7

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
naccept1
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Mon, 05 Nov 2018 07:53:48 +0900
parents 02b4ecc9972c
children ab265470c2d0
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 module automaton where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
24
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
3 -- open import Level renaming ( suc to succ ; zero to Zero )
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 1
diff changeset
4 open import Data.Nat
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
5 open import Data.List
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
6 open import Data.Maybe
24
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
7 open import Data.Bool using ( Bool ; true ; false ; _∧_ )
3
3ac6311293ec εAutomaton
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 2
diff changeset
8 open import Relation.Binary.PropositionalEquality hiding ( [_] )
9
e7bb980408fb separate epsiron
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 8
diff changeset
9 open import Relation.Nullary using (¬_; Dec; yes; no)
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
10
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
11 record Automaton ( Q : Set ) ( Σ : Set )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 : Set where
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
13 field
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
14 δ : Q → Σ → Q
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
15 astart : Q
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
16 aend : Q → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
17
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
18 open Automaton
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 data States1 : Set where
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
21 sr : States1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
22 ss : States1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
23 st : States1
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25 data In2 : Set where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26 i0 : In2
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 i1 : In2
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
29 moves : { Q : Set } { Σ : Set }
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
30 → Automaton Q Σ
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 → Q → List Σ → Q
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
32 moves {Q} { Σ} M q L = move q L
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33 where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34 move : (q : Q ) ( L : List Σ ) → Q
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 move q [] = q
24
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
36 move q ( H ∷ T ) = move ( δ M q H) T
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
38 accept : { Q : Set } { Σ : Set }
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
39 → Automaton Q Σ
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
40 → List Σ → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
41 accept {Q} { Σ} M L = move (astart M) L
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
42 where
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
43 move : (q : Q ) ( L : List Σ ) → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
44 move q [] = aend M q
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
45 move q ( H ∷ T ) = move ( (δ M) q H ) T
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
46
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
47 transition1 : States1 → In2 → States1
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
48 transition1 sr i0 = sr
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
49 transition1 sr i1 = ss
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
50 transition1 ss i0 = sr
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
51 transition1 ss i1 = st
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
52 transition1 st i0 = sr
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
53 transition1 st i1 = st
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
54
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
55 fin1 : States1 → Bool
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
56 fin1 st = true
24
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
57 fin1 ss = false
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
58 fin1 sr = false
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
59
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
60 am1 : Automaton States1 In2
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
61 am1 = record { δ = transition1 ; astart = sr ; aend = fin1 }
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
62
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
63
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
64 example1-1 = accept am1 ( i0 ∷ i1 ∷ i0 ∷ [] )
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
65 example1-2 = accept am1 ( i1 ∷ i1 ∷ i1 ∷ [] )
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
66
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
67 reachable : { Q : Set } { Σ : Set }
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
68 → (M : Automaton Q Σ )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
69 → (q : Q )
13
02b4ecc9972c start exp version of subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 9
diff changeset
70 → (L : List Σ ) → Set
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
71 reachable M q L = moves M (astart M) L ≡ q
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
72
1
3c6de7cf2a95 nfa worked
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 0
diff changeset
73 example1-3 = reachable am1 st ( i1 ∷ i1 ∷ i1 ∷ [] )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
74
24
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
75 ieq : (i i' : In2 ) → Dec ( i ≡ i' )
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
76 ieq i0 i0 = yes refl
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
77 ieq i1 i1 = yes refl
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
78 ieq i0 i1 = no ( λ () )
9406c2571fe7 naccept1
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 13
diff changeset
79 ieq i1 i0 = no ( λ () )
0
e5aa1cf746cb automaton lecture
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
80