annotate a07/lecture.ind @ 406:a60132983557

...
author Shinji KONO <kono@ie.u-ryukyu.ac.jp>
date Wed, 08 Nov 2023 21:35:54 +0900
parents 6f3636fbc481
children
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
rev   line source
127
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
1 -title: 非決定性オートマトンから決定性オートマトンへの変換
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
2
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
3 非決定性オートマトンは、ある状態から複数の可能な状態へ遷移する。そのうちのどれかが受理状態へ遷移すれば accept となる。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
4
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
5 状態は有限なので、複数の可能な状態は、状態の部分集合となる。状態Qの部分集合は、
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
6
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
7   Q → Bool
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
8
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
9 と表すことができる。つまり、その部分集合に含まれるかどうかを表す関数が部分集合そのものになる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
10
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
11 これを、Bool
127
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
12 <sup>Q</sup> と書くことがある。Bool は二つの要素がある。状態数4からBoolへの関数は、2
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
13 <sup>4</sup>個ある。集合のべき乗をこのようにして定義することができる。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
14
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
15 非決定性オートマトンを状態Qの部分集合を状態とする決定性オートマトンと考えることができる。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
16 NAutomaton Q Σ は状態の集合Qと入力文字の集合Σからなる非決定性オートマトンだった。これから、
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
17
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
18 Automaton (Q → Bool) Σ
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
19
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
20 を作れれば、非決定性オートマトンから決定性オートマトンへの変換ができることになる。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
21
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
22 状態Q入力文字Σの決定性オートマトンの状態遷移関数は Q → Σ → Q だったから、
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
23 この状態Qの部分集合を状態とするAutomatonの状態遷移関数は、
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
24
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
25  (Q → Bool) → Σ → (Q → Bool)
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
26
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
27 となる。右のかっこは省略可能である。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
28
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
29  (Q → Bool) → Σ → Q → Bool
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
30
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
31 つまり、状態遷移関数は三つの入力を持つ。f i q としよう。決定性オートマトンの状態遷移関数は、
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
32
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
33   Nδ : Q → Σ → Q → Bool
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
34
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
35 だった。f : Q → Bool が入力の状態で、i : Σ が決まっている。出力状態は Q → Bool なので q を入力に持つ。
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
36
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
37   λ q → f q ∧ Nδ q i
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
38
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
39
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
40 --状態の部分集合を使う
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
41
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
42 true になるものは複数あるので、やはり部分集合で表される。つまり、
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
43
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
44 exists : ( P : Q → Bool ) → Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
45
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
46 このような関数を実装する必要がある。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
47
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
48 --非決定性オートマトンと決定性オートマトン
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
49
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
50 record Automaton ( Q : Set ) ( Σ : Set )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
51 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
52 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
53 δ : Q → Σ → Q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
54 aend : Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
55
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
56 の Q に Q → Bool を入れてみる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
57
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
58 δ : (Q → Bool ) → Σ → Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
59 aend : (Q → Bool ) → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
60
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
61 これを、
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
62
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
63 record NAutomaton ( Q : Set ) ( Σ : Set )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
64 : Set where
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
65 field
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
66 Nδ : Q → Σ → Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
67 Nend : Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
68
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
69 これの Nδ と Nend から作れれば、NFA から DFA を作れることになる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
70
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
71 NFAの受理を考えると、状態の集合を持ち歩いて受理を判断している。つまり、状態の集合を状態とする Automaton を考えることになる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
72
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
73 遷移条件は、状態の集合を受けとって、条件を満たす状態の集合を返せば良い。条件は
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
74
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
75 Nδ : Q → Σ → Q → Bool
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
76
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
77 だった。つまり、入力の状態集合を選別する関数 f と、 Nδ との /\ を取ってやればよい。q は何かの状態、iは入力、nq は次の状態である。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
78
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
79 f q /\ Nδ NFA q i nq
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
80
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
81 これが true になるものを exists を使って探し出す。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
82
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
83 δconv : { Q : Set } { Σ : Set } → (exists : ( Q → Bool ) → Bool )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
84 → ( Q → Σ → Q → Bool ) → (Q → Bool) → Σ → (Q → Bool)
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
85 δconv {Q} { Σ} exists nδ f i q = exists ( λ r → f r /\ nδ r i q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
86
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
87 ここで、( nδ : Q → Σ → Q → Bool ) は NFAの状態遷移関数を受けとる部分である。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
88
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
89 終了条件は
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
90
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
91 f q /\ Nend NFA q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
92
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
93 で良い。 これが true になるものを exists を使って探し出す。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
94
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
95 Q が FiniteSet Q {n} であれば
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
96
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
97 subset-construction : { Q : Set } { Σ : Set } →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
98 ( ( Q → Bool ) → Bool ) →
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
99 (NAutomaton Q Σ ) → (Automaton (Q → Bool) Σ )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
100 subset-construction {Q} { Σ} exists NFA = record {
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
101 δ = λ q x → δconv exists ( Nδ NFA ) q x
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
102 ; aend = λ f → exists ( λ q → f q /\ Nend NFA q )
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
103 }
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
104
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
105 という形で書くことができる。状態の部分集合を作っていくので、subset construction と呼ばれる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
106
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
107 λ f i → δconv exists ( Nδ NFA ) f i
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
108
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
109 λ f i q → δconv exists ( Nδ NFA ) f i q
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
110
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
111 であることに注意しよう。これは、Curry 化の省略になっている。省略があるので、δ : (Q → Bool ) → Σ → Q → Bool という形に見える。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
112
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
113 これで実際に、NFAから DFA を作成することができた。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
114 ここで、状態の exists (有限性または部分集合の決定性)を使っていることに注意しよう。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
115
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
116 <a href=" ../agda/sbconst2.agda"> subset construction </a>
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
117
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
118
127
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
119 ---問題7.1 以下の非決定性オートマトンを決定性オートマトンへ変換せよ
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
120
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
121
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
122 <a href="../exercise/003.html"> 例題 </a> <!--- Exercise 7.1 --->
0e8a0e50ed26 add some files
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents:
diff changeset
123
332
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
124 --subset constructionの状態数
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
125
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
126 実際にこれを計算すると、状態数 n のNFAから、最大、2^n の状態を持つDFAが生成される。しかし、この論理式からそれを
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
127 自明に理解することは難しい。しかし、f は Q → Bool なので、例えば、3状態でも、
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
128
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
129 q1 q2 q3
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
130 false false false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
131 false false true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
132 false true false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
133 false true true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
134 true false false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
135 true false true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
136 true true false
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
137 true true true
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
138
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
139 という8個の状態を持つ。exists は、このすべての場合を尽くすように働いている。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
140
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
141 アルゴリズムとしてこのまま実装すると、 exists が必要な分だけ計算するようになっている。これは結構遅い。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
142 前もって、可能な状態を Automaton として探し出そうとすると、 指数関数的な爆発になってしまう。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
143
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
144 実際に、指数関数的な状態を作る NFA が存在するので、これを避けることはできない。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
145
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
146 --NFAの実行
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
147
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
148 subset construction した automaton はすべての状態を生成する前でも実行することができる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
149 ただし、毎回、nest した exists を実行することになる。
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
150
Shinji KONO <kono@ie.u-ryukyu.ac.jp>
parents: 127
diff changeset
151