|
37
|
1 -title: 非決定性オートマトン
|
|
|
2
|
|
|
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
|
|
|
4
|
|
|
5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
|
|
|
6
|
|
|
7 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。部分集合を使っても良いが、ここではリストを使おう。
|
|
|
8
|
|
|
9 record NAutomaton ( Q : Set ) ( Σ : Set )
|
|
|
10 : Set where
|
|
|
11 field
|
|
|
12 nδ : Q → Σ → List Q
|
|
|
13 sid : Q → ℕ
|
|
|
14 nstart : Q
|
|
|
15 nend : Q → Bool
|
|
|
16
|
|
|
17 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、nを付けた。
|
|
|
18
|
|
|
19 次の状態は状態の集合(List)になる。次の次の状態は、可能な状態の次の状態の集合を合わせた(union)ものになる。
|
|
|
20
|
|
|
21 少し複雑がだが、insert と merge を定義して、
|
|
|
22
|
|
|
23 <a href="../agda/nfa-list.agda"> nfa-list.agda </a>
|
|
|
24
|
|
|
25 insert : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → Q → List Q
|
|
|
26 insert M [] q = q ∷ []
|
|
|
27 insert M ( q ∷ T ) q' with (sid M q ) ≟ (sid M q')
|
|
|
28 ... | yes _ = insert M T q'
|
|
|
29 ... | no _ = q ∷ (insert M T q' )
|
|
|
30
|
|
|
31 merge : { Q : Set } { Σ : Set } → ( NAutomaton Q Σ ) → List Q → List Q → List Q
|
|
|
32 merge M L1 [] = L1
|
|
|
33 merge M L1 ( H ∷ L ) = insert M (merge M L1 L ) H
|
|
|
34
|
|
|
35 Nmoves : { Q : Set } { Σ : Set }
|
|
|
36 → NAutomaton Q Σ
|
|
|
37 → List Q → List Σ → List Q
|
|
|
38 Nmoves {Q} { Σ} M q L = Nmoves1 q L []
|
|
|
39 where
|
|
|
40 Nmoves1 : (q : List Q ) ( L : List Σ ) → List Q → List Q
|
|
|
41 Nmoves1 q [] _ = q
|
|
|
42 Nmoves1 [] (_ ∷ L) LQ = Nmoves1 LQ L []
|
|
|
43 Nmoves1 (q ∷ T ) (H ∷ L) LQ = Nmoves1 T (H ∷ L) ( merge M ( nδ M q H ) LQ )
|
|
|
44
|
|
|
45 Naccept : { Q : Set } { Σ : Set }
|
|
|
46 → NAutomaton Q Σ
|
|
|
47 → List Σ → Bool
|
|
|
48 Naccept {Q} { Σ} M L =
|
|
|
49 checkAccept ( Nmoves M ((nstart M) ∷ [] ) L )
|
|
|
50 where
|
|
|
51 checkAccept : (q : List Q ) → Bool
|
|
|
52 checkAccept [] = false
|
|
|
53 checkAccept ( H ∷ L ) with (nend M) H
|
|
|
54 ... | true = true
|
|
|
55 ... | false = checkAccept L
|
|
|
56
|
|
|
57 とする。
|
|
|
58
|
|
|
59 --部分集合を使うと簡単になる
|
|
|
60
|
|
|
61 <a href="../agda/nfa-list.agda"> nfa-list.agda </a>
|
|
|
62
|
|
|
63
|
|
|
64 record NAutomaton ( Q : Set ) ( Σ : Set )
|
|
|
65 : Set where
|
|
|
66 field
|
|
|
67 Nδ : Q → Σ → Q → Bool
|
|
|
68 Nstart : Q → Bool
|
|
|
69 Nend : Q → Bool
|
|
|
70
|
|
|
71
|
|
|
72 Nmoves : { Q : Set } { Σ : Set }
|
|
|
73 → NAutomaton Q Σ
|
|
|
74 → {n : ℕ } → FiniteSet Q {n}
|
|
|
75 → ( Q → Bool ) → Σ → Q → Bool
|
|
|
76 Nmoves {Q} { Σ} M fin Qs s q =
|
|
|
77 exists fin ( λ qn → (Qs qn ∧ ( Nδ M qn s q ) ))
|
|
|
78
|
|
|
79
|
|
|
80 Naccept : { Q : Set } { Σ : Set }
|
|
|
81 → NAutomaton Q Σ
|
|
|
82 → {n : ℕ } → FiniteSet Q {n}
|
|
|
83 → List Σ → Bool
|
|
|
84 Naccept {Q} {Σ} M fin input = Naccept1 M ( Nstart M ) input
|
|
|
85 where
|
|
|
86 Naccept1 : NAutomaton Q Σ → ( Q → Bool ) → List Σ → Bool
|
|
|
87 Naccept1 M sb [] = exists fin ( λ q → sb q ∧ Nend M q )
|
|
|
88 Naccept1 M sb (i ∷ t ) = Naccept1 M ( Nmoves M fin sb i ) t
|
|
|
89
|
|
|
90 --例題
|
|
|
91
|
|
|
92 transition3 : States1 → In2 → States1 → Bool
|
|
|
93 transition3 sr i0 sr = true
|
|
|
94 transition3 sr i1 ss = true
|
|
|
95 transition3 sr i1 sr = true
|
|
|
96 transition3 ss i0 sr = true
|
|
|
97 transition3 ss i1 st = true
|
|
|
98 transition3 st i0 sr = true
|
|
|
99 transition3 st i1 st = true
|
|
|
100 transition3 _ _ _ = false
|
|
|
101
|
|
|
102 fin1 : States1 → Bool
|
|
|
103 fin1 st = true
|
|
|
104 fin1 ss = false
|
|
|
105 fin1 sr = false
|
|
|
106
|
|
|
107 start1 : States1 → Bool
|
|
|
108 start1 sr = true
|
|
|
109 start1 _ = false
|
|
|
110
|
|
|
111 am2 : NAutomaton States1 In2
|
|
|
112 am2 = record { Nδ = transition3 ; Nstart = start1 ; Nend = fin1}
|
|
|
113
|
|
|
114 example2-1 = Naccept am2 finState1 ( i0 ∷ i1 ∷ i0 ∷ [] )
|
|
|
115 example2-2 = Naccept am2 finState1 ( i1 ∷ i1 ∷ i1 ∷ [] )
|
|
|
116
|
|
|
117
|
