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
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -title: 非決定性オートマトン
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 決定性オートマトンは入力に対して次の状態が一意に決まる。一つの入力に対して可能な状態が複数ある場合を考える。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 例えば、ドアの鍵がテンキーだったら、次に何を入れるかには自由度がある。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 record NAutomaton ( Q : Set ) ( Σ : Set )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 field
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
21 Nδ : Q → Σ → Q → Bool
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
22 Nend : Q → Bool
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
26 <a href="../agda/nfa.agda"> nfa.agda </a>
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
75
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
76 Nmoves : { Q : Set } { Σ : Set }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
77 → NAutomaton Q Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
88 → NAutomaton Q Σ
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
89 → {n : ℕ } → FiniteSet Q {n}
69
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
92 Naccept M fin sb (i ∷ t ) = Naccept M fin ( Nmoves M fin sb i ) t
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
95
37
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
96
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
97 --例題
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
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
f124fceba460 subset construction
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 37
diff changeset
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