Mercurial > hg > Members > kono > Proof > automaton
annotate a04/lecture.ind @ 104:fba1cd54581d
use exists in cond, nfa example
author | Shinji KONO <kono@ie.u-ryukyu.ac.jp> |
---|---|
date | Thu, 14 Nov 2019 05:13:49 +0900 (2019-11-13) |
parents | f124fceba460 |
children | b3f05cd08d24 |
rev | line source |
---|---|
37 | 1 -title: 非決定性オートマトン |
2 | |
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。 | |
4 | |
5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。 | |
6 | |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
7 この拡張は容易で、状態遷移関数が状態の代わりに状態のリストを返せば良い。しかし、リストを使うとかなり煩雑になる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
8 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
9 Regular Language は Concatについて閉じている。これは オートマトン A と B があった時に、z を前半 x ++ y |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
10 にわけて x を A が受理し、y を B で受理するものを、単一ののオートマトンで実現できると言う意味である。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
11 しかい、 これを決定性オートマトンで示すのは難しい。A ++ B の 境目がどこかを前もって予測することができないからである。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
12 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
13 --Agda での非決定性オートマトン |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
14 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
15 ここでは、部分集合を写像を使って表す。集合 Q から Bool (true または false) への写像を使う。true になる要素が |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
16 部分集合になる。すると、遷移関数は入力Σと状態から Bool への写像となる。終了条件は変わらない。 |
37 | 17 |
18 record NAutomaton ( Q : Set ) ( Σ : Set ) | |
19 : Set where | |
20 field | |
69 | 21 Nδ : Q → Σ → Q → Bool |
22 Nend : Q → Bool | |
37 | 23 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
24 これを非決定性オートマトンという。Agda では同じ名前を使いまわしすることはできない(monomorpphism)ので、Nを付けた。 |
37 | 25 |
69 | 26 <a href="../agda/nfa.agda"> nfa.agda </a> |
37 | 27 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
28 --NAutomatonの受理と遷移 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
29 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
30 非決定性オートマトンでは、一つの入力に対して、複数の状態が行き先になる。複数の状態を経由した経路のどれかが |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
31 入力を読み終わった後に、終了状態になれば受理されることになる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
32 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
33 このためには、状態の集合Qから条件 P : Q → Bool で true になるものを見つけ出す必要がある。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
34 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
35 true になるものは複数あるので、やはり部分集合で表される。つまり、 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
36 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
37 exists : ( P : Q → Bool ) → Q → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
38 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
39 このような関数を実現する必要がある。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
40 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
41 もし、Q が有限集合なら、P を順々に調べていけばよい。やはり List で良いのだが、ここでは Agda の Data.Fin を使ってみよう。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
42 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
43 --finiteSet |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
44 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
45 Data.Fin だけを使って記述することもできるが、数字だけというのも味気ない。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
46 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
47 record FiniteSet ( Q : Set ) { n : ℕ } : Set where |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
48 field |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
49 Q←F : Fin n → Q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
50 F←Q : Q → Fin n |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
51 finiso→ : (q : Q) → Q←F ( F←Q q ) ≡ q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
52 finiso← : (f : Fin n ) → F←Q ( Q←F f ) ≡ f |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
53 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
54 という感じで、Data.Fin と 状態を対応させる。そうすると、 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
55 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
56 lt0 : (n : ℕ) → n Data.Nat.≤ n |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
57 lt0 zero = z≤n |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
58 lt0 (suc n) = s≤s (lt0 n) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
59 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
60 exists1 : (m : ℕ ) → m Data.Nat.≤ n → (Q → Bool) → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
61 exists1 zero _ _ = false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
62 exists1 ( suc m ) m<n p = p (Q←F (fromℕ≤ {m} {n} m<n)) \/ exists1 m (lt2 m<n) p |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
63 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
64 exists : ( Q → Bool ) → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
65 exists p = exists1 n (lt0 n) p |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
66 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
67 という形で、 exists を記述することができる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
68 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
69 <a href="../agda/finiteSet.agda"> finiteSet.agda </a> |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
70 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
71 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
72 --NAutomatonの受理と遷移 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
73 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
74 状態の受理と遷移は exists を使って以下のようになる。 |
37 | 75 |
76 Nmoves : { Q : Set } { Σ : Set } | |
77 → NAutomaton Q Σ | |
78 → {n : ℕ } → FiniteSet Q {n} | |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
79 → ( Qs : Q → Bool ) → (s : Σ ) → Q → Bool |
37 | 80 Nmoves {Q} { Σ} M fin Qs s q = |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
81 exists fin ( λ qn → (Qs qn /\ ( Nδ M qn s q ) )) |
37 | 82 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
83 Qs は Q → Bool の型を持っているので、Qs qn は true または false である。今の状態集合 Qs に含まれていて、 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
84 Nδ M qn s q つまり、非決定オートマトン M の遷移関数 Nδ : Q → Σ → Q → Bool で true を返すものが存在すれば |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
85 遷移可能になる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
86 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
87 Naccept : { Q : Set } { Σ : Set } |
37 | 88 → NAutomaton Q Σ |
89 → {n : ℕ } → FiniteSet Q {n} | |
69 | 90 → (Nstart : Q → Bool) → List Σ → Bool |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
91 Naccept M fin sb [] = exists fin ( λ q → sb q /\ Nend M q ) |
69 | 92 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t |
93 | |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
94 Naccept では終了条件を調べる。状態の集合 sb で Nend を満たすものがあることを exists を使って調べればよい。 |
69 | 95 |
37 | 96 |
97 --例題 | |
98 | |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
99 例題1.36 を考えよう。状態遷移関数は以下のようになる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
100 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
101 transition136 : StatesQ → A2 → StatesQ → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
102 transition136 q1 b0 q2 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
103 transition136 q1 a0 q1 = true -- q1 → ep → q3 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
104 transition136 q2 a0 q2 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
105 transition136 q2 a0 q3 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
106 transition136 q2 b0 q3 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
107 transition136 q3 a0 q1 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
108 transition136 _ _ _ = false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
109 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
110 教科書にはε遷移(入力がなくても遷移できる)があるが、ここでは、ε遷移先の矢印を全部手元に持ってきてしまうという |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
111 ことしてしまう。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
112 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
113 end136 : StatesQ → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
114 end136 q1 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
115 end136 _ = false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
116 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
117 start136 : StatesQ → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
118 start136 q1 = true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
119 start136 _ = false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
120 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
121 nfa136 : NAutomaton StatesQ A2 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
122 nfa136 = record { Nδ = transition136; Nend = end136 } |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
123 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
124 <a href=" ../agda/nfa136.agda"> 1.36 の例題 </a> |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
125 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
126 example136-1 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ [] ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
127 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
128 最初の状態 q1 から a0 ∷ b0 ∷ a0 ∷ [] の入力を受けとる場合を考える。 |
37 | 129 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
130 a0 を受けとると、q1 にしか行けない。q1 で b0 を受けとると、q2 に移動する。q2 で a0 を受けとると、q3 か、または、 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
131 q2 に行ける。どちらも終了状態ではないので、不受理となる。ここで、もう一つ a0 が来れば q3 から q1 に行ける。q2 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
132 から行けないが、どれかの経路が成功すれば良いので受理となる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
133 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
134 example136-2 = Naccept nfa136 finStateQ start136( a0 ∷ b0 ∷ a0 ∷ a0 ∷ [] ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
135 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
136 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
137 --問題 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
138 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
139 ... 作成中... |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
140 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
141 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
142 --非決定性オートマトンと決定性オートマトン |
37 | 143 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
144 record Automaton ( Q : Set ) ( Σ : Set ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
145 : Set where |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
146 field |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
147 δ : Q → Σ → Q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
148 aend : Q → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
149 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
150 の Q に Q → Bool を入れてみる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
151 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
152 δ : (Q → Bool ) → Σ → Q → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
153 aend : (Q → Bool ) → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
154 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
155 これを、 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
156 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
157 record NAutomaton ( Q : Set ) ( Σ : Set ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
158 : Set where |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
159 field |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
160 Nδ : Q → Σ → Q → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
161 Nend : Q → Bool |
37 | 162 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
163 これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
164 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
165 NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
166 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
167 遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
168 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
169 Nδ : Q → Σ → Q → Bool |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
170 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
171 だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
172 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
173 f q /\ Nδ NFA q i nq |
69 | 174 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
175 これが true になるものを exists を使って探し出す。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
176 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
177 δconv : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → ( nδ : Q → Σ → Q → Bool ) → (f : Q → Bool) → (i : Σ) → (Q → Bool) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
178 δconv {Q} { Σ} { n} N nδ f i q = exists N ( λ r → f r /\ nδ r i q ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
179 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
180 ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
181 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
182 終了条件は |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
183 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
184 f q /\ Nend NFA q ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
185 ' |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
186 で良い。 これが true になるものを exists を使って探し出す。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
187 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
188 Q が FiniteSet Q {n} であれば |
37 | 189 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
190 subset-construction : { Q : Set } { Σ : Set } { n : ℕ } → FiniteSet Q {n} → |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
191 (NAutomaton Q Σ ) → (astart : Q ) → (Automaton (Q → Bool) Σ ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
192 subset-construction {Q} { Σ} {n} fin NFA astart = record { |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
193 δ = λ f i → δconv fin ( Nδ NFA ) f i |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
194 ; aend = λ f → exists fin ( λ q → f q /\ Nend NFA q ) |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
195 } |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
196 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
197 という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
198 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
199 λ f i → δconv fin ( Nδ NFA ) f i |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
200 は |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
201 λ f i q → δconv fin ( Nδ NFA ) f i q |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
202 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
203 であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
204 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
205 <a href=" ../agda/sbconst2.agda"> subset construction </a> |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
206 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
207 --subset constructionの状態数 |
37 | 208 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
209 実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
210 自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、 |
37 | 211 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
212 q1 q2 q3 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
213 false false false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
214 false false true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
215 false true false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
216 false true true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
217 true false false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
218 true false true |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
219 true true false |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
220 true true true |
69 | 221 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
222 という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。 |
69 | 223 |
104
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
224 アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
225 前もって、可能な状態を Automaton として探し出そうとすると、 指数関数的な爆発になってしまう。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
226 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
227 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。 |
fba1cd54581d
use exists in cond, nfa example
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
69
diff
changeset
|
228 |