|
127
|
1 -title: Turing Machine
|
|
|
2
|
|
|
3 Turing Machine は無限長のテープを持つAutomatonである。これは、stack を二つ持つ Automaton として構成できる。
|
|
|
4
|
|
|
5 <a href="../agda/turing.agda"> turing.agda </a>
|
|
|
6
|
|
|
7 テープへの操作は、書き込みと移動である。
|
|
|
8
|
|
|
9 data Write ( Σ : Set ) : Set where
|
|
|
10 write : Σ → Write Σ
|
|
|
11 wnone : Write Σ
|
|
|
12
|
|
|
13 data Move : Set where
|
|
|
14 left : Move
|
|
|
15 right : Move
|
|
|
16 mnone : Move
|
|
|
17
|
|
|
18 Turing machineは状態と入力で、このコマンド二つを選択する。
|
|
|
19
|
|
|
20 record Turing ( Q : Set ) ( Σ : Set )
|
|
|
21 : Set where
|
|
|
22 field
|
|
|
23 tδ : Q → Σ → Q × ( Write Σ ) × Move
|
|
|
24 tstart : Q
|
|
|
25 tend : Q → Bool
|
|
|
26 tnone : Σ
|
|
|
27
|
|
|
28 書き込みと移動を二つのstack( List Σ)に対する関数として定義する。
|
|
|
29
|
|
|
30 {-# TERMINATING #-}
|
|
|
31 move : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
32 move q L [] = move q L ( tnone ∷ [] )
|
|
|
33 move q [] R = move q ( tnone ∷ [] ) R
|
|
|
34 move q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
|
|
|
35 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT )
|
|
|
36 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) )
|
|
|
37 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) )
|
|
|
38 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT )
|
|
|
39 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) )
|
|
|
40 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) )
|
|
|
41 {-# TERMINATING #-}
|
|
|
42 move-loop : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
43 move-loop q L R with tend q
|
|
|
44 ... | true = ( q , L , R )
|
|
|
45 ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) )
|
|
|
46 where
|
|
|
47 next = move q L R
|
|
|
48 {-# TERMINATING #-}
|
|
|
49 move0 : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
50 move0 q L R with tend q
|
|
|
51 ... | true = ( q , L , R )
|
|
|
52 move0 q L [] | false = move0 q L ( tnone ∷ [] )
|
|
|
53 move0 q [] R | false = move0 q ( tnone ∷ [] ) R
|
|
|
54 move0 q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH
|
|
|
55 ... | nq , write x , left = move0 nq ( RH ∷ x ∷ LT ) RT
|
|
|
56 ... | nq , write x , right = move0 nq LT ( x ∷ RH ∷ RT )
|
|
|
57 ... | nq , write x , mnone = move0 nq ( x ∷ LT ) ( RH ∷ RT )
|
|
|
58 ... | nq , wnone , left = move0 nq ( RH ∷ LH ∷ LT ) RT
|
|
|
59 ... | nq , wnone , right = move0 nq LT ( LH ∷ RH ∷ RT )
|
|
|
60 ... | nq , wnone , mnone = move0 nq ( LH ∷ LT ) ( RH ∷ RT )
|
|
|
61 {-# TERMINATING #-}
|
|
|
62 taccept : List Σ → ( Q × List Σ × List Σ )
|
|
|
63 taccept L = move0 tstart L []
|
|
|
64
|
|
|
65 --Turing Machine の例題
|
|
|
66
|
|
|
67 data CopyStates : Set where
|
|
|
68 s1 : CopyStates
|
|
|
69 s2 : CopyStates
|
|
|
70 s3 : CopyStates
|
|
|
71 s4 : CopyStates
|
|
|
72 s5 : CopyStates
|
|
|
73 H : CopyStates
|
|
|
74
|
|
|
75
|
|
|
76 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
|
|
|
77 Copyδ s1 0 = (H , wnone , mnone )
|
|
|
78 Copyδ s1 1 = (s2 , write 0 , right )
|
|
|
79 Copyδ s2 0 = (s3 , write 0 , right )
|
|
|
80 Copyδ s2 1 = (s2 , write 1 , right )
|
|
|
81 Copyδ s3 0 = (s4 , write 1 , left )
|
|
|
82 Copyδ s3 1 = (s3 , write 1 , right )
|
|
|
83 Copyδ s4 0 = (s5 , write 0 , left )
|
|
|
84 Copyδ s4 1 = (s4 , write 1 , left )
|
|
|
85 Copyδ s5 0 = (s1 , write 1 , right )
|
|
|
86 Copyδ s5 1 = (s5 , write 1 , left )
|
|
|
87 Copyδ H _ = (H , wnone , mnone )
|
|
|
88 Copyδ _ (suc (suc _)) = (H , wnone , mnone )
|
|
|
89
|
|
|
90 copyMachine : Turing CopyStates ℕ
|
|
|
91 copyMachine = record {
|
|
|
92 tδ = Copyδ
|
|
|
93 ; tstart = s1
|
|
|
94 ; tend = tend
|
|
|
95 ; tnone = 0
|
|
|
96 } where
|
|
|
97 tend : CopyStates → Bool
|
|
|
98 tend H = true
|
|
|
99 tend _ = false
|
|
|
100
|
|
|
101 test1 : CopyStates × ( List ℕ ) × ( List ℕ )
|
|
|
102 test1 = Turing.taccept copyMachine ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] )
|
|
|
103
|
|
|
104 test2 : ℕ → CopyStates × ( List ℕ ) × ( List ℕ )
|
|
|
105 test2 n = loop n (Turing.tstart copyMachine) ( 1 ∷ 1 ∷ 0 ∷ 0 ∷ 0 ∷ [] ) []
|
|
|
106
|
|
|
107
|
|
|
108 -- Turing machine の停止問題
|
|
|
109
|
|
|
110 ---Universal Turing Machine
|
|
|
111
|
|
|
112 文字列 x を判定する Turinging machine tm(x) があるとする。
|
|
|
113
|
|
|
114 tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine
|
|
|
115
|
|
|
116 utm(tm , x)
|
|
|
117
|
|
|
118 を構成することができる。utm(tm,x) は引数を二つ持つが、tm+x と結合した単一の文字列だと思えば単一引数になる。
|
|
|
119
|
|
|
120 utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。
|
|
|
121
|
|
|
122 utm(tm,x) = 0 受け入れない
|
|
|
123 1 受け入れる
|
|
|
124 ⊥ 止まらない
|
|
|
125
|
|
|
126 utm の構成の詳細には立ち入らない。実際に utm を構成するのは良い演習になる。
|
|
|
127
|
|
|
128 tm に対応する文字列を tm とすると、tm 自体を tm の入力とすることができる。utm は、そのためだけに導入したので、もう使わない。
|
|
|
129
|
|
|
130 --Turinng Machine の停止性の判定
|
|
|
131
|
|
|
132 halt(tm,x) は、以下のように定義される。これはまだ、Turing machine であるとは限らない。
|
|
|
133
|
|
|
134 halt(tm,x) = 0 tm(x) が止まらない (halt が停止しない) (1)
|
|
|
135 halt(tm,x) = 1 tm(x) が止まる (2)
|
|
|
136
|
|
|
137 halt(tm+x) 自体は ⊥ 、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?
|
|
|
138
|
|
|
139 --halt が tm ではあり得ないこの証明
|
|
|
140
|
|
|
141 halt の否定を考えよう。
|
|
|
142
|
|
|
143 neg(tm) = 1 halt(tm,tm) が0 (3)
|
|
|
144 neg(tm) = ⊥ halt(tm,tm) が1 (4)
|
|
|
145
|
|
|
146 つまり、halt(tm,tm) が1 の時、つまり、tm(tm) が停止する時には、neg(tm) は停止しない。neg 自体は halt があればtmとして簡単に作れる。
|
|
|
147
|
|
|
148 neg(neg) = 1
|
|
|
149
|
|
|
150 かどうか調べよう。ここで 引数の neg は Turing machine neg を表す文字列である。
|
|
|
151
|
|
|
152 まず、neg(neg) =1 と仮定する。(3) から、
|
|
|
153
|
|
|
154 halt(neg,neg) が 0
|
|
|
155
|
|
|
156 なことがわかる。つまり、neg(neg) は停止しない。neg(neg) = ⊥ 。これは最初の仮定 neg(neg)=1に矛盾する。
|
|
|
157
|
|
|
158 逆に、
|
|
|
159
|
|
|
160 neg(neg) = ⊥
|
|
|
161
|
|
|
162 とすると、(4) から、
|
|
|
163
|
|
|
164 halt(neg,neg) = 1
|
|
|
165
|
|
|
166 つまり、neg(neg) は止まる。つまり、neg(neg)=1。これも矛盾。
|
|
|
167
|
|
|
168 つまり、halt(tm,x) が⊥にならないようなものは存在しない。
|
|
|
169
|
|
|
170 つまり、Turinng machine が停止するかどうかを、必ず判定できる停止する Turing machine は存在しない。
|
|
|
171
|
|
|
172 --証明の考察
|
|
|
173
|
|
|
174 ここで用いているのは、Turing machine の詳細ではなく、
|
|
|
175
|
|
|
176 Turing machine に対応する文字列 tm がある
|
|
|
177 tm を入力として用いることができる
|
|
|
178
|
|
|
179 ということと、
|
|
|
180
|
|
|
181 tm が停止する、停止しない
|
|
|
182 tm が停止して、1から0
|
|
|
183
|
|
|
184 を返すという性質である。
|
|
|
185
|
|
|
186 neg(neg)
|
|
|
187
|
|
|
188 は自分自身を参照しているので、自己参照と呼ばれる。
|
|
|
189
|
|
|
190 halt は、neg が Turing machine になるためには、Turing machine である必要がある。
|
|
|
191
|
|
|
192 tm(x) は停止するかしないかどちらかだから、halt(tm,x) という述語自体はある。
|
|
|
193
|
|
|
194 しかし、halt(neg,neg) は 0 か 1 かを決めることはできない。
|
|
|
195
|
|
|
196 これは述語を定義しても、それが0か1かを決めることができない場合があるということである。
|
|
|
197
|
|
|
198 これは、述語論理の不完全性定理に対応する。
|
|
|
199
|
|
|
200 この証明は自己参照を用いて矛盾を導く方法である。
|
|
|
201
|
|
|
202 --対角線論法
|
|
|
203
|
|
|
204 0,1 からなる無限長の文字列を考えよう。これを順に拾っていく。どんな順序で拾っても、自然数の範囲では拾い切れないことをしまそう。
|
|
|
205
|
|
|
206 拾った順に、文字列を並べる。
|
|
|
207
|
|
|
208 00000000000000000000000000100000....
|
|
|
209 01000000000000000000000000001000....
|
|
|
210 01100000000000000000000000000100....
|
|
|
211 01110000000000000000000000000010....
|
|
|
212 01111000000000000000000000000000....
|
|
|
213 01111100000000000000000000000000....
|
|
|
214 01011100000000000000000000000000....
|
|
|
215 ...
|
|
|
216 ...
|
|
|
217 ...
|
|
|
218
|
|
|
219 行y列xの文字を v(x,y) とする。これは 0 か 1 である。上の文字列の対角線の要素は v(x,x) となる。以下の . が対角線要素になる。
|
|
|
220
|
|
|
221 .0000000000000000000000000100000....
|
|
|
222 0.000000000000000000000000001000....
|
|
|
223 01.00000000000000000000000000100....
|
|
|
224 011.0000000000000000000000000010....
|
|
|
225 0111.000000000000000000000000000....
|
|
|
226 01111.00000000000000000000000000....
|
|
|
227 010111.0000000000000000000000000....
|
|
|
228 ...
|
|
|
229 ...
|
|
|
230 ...
|
|
|
231
|
|
|
232 1-v(x,x) を考えると、
|
|
|
233
|
|
|
234 1000001 ...
|
|
|
235
|
|
|
236 となる。この文字列は、最初に拾った文字列のどれとも、v(x,x)のところで異なる。つまり拾った文字列とは異なる文字列が必ず存在する。
|
|
|
237
|
|
|
238 これは、順に取ってくるという方法では、無限長の文字列は尽くせないということを意味する。可算回と呼ぶ。
|
|
|
239
|
|
|
240 --2^N
|
|
|
241
|
|
|
242 この無限長の文字列は、自然数Nから{0,1} の写像と考えられる。あるいは、自然数Nの部分集合に1、それ以外に0を割り振ったものである。これを 2^N と書く。
|
|
|
243
|
|
|
244 自然数の部分集合全体
|
|
|
245 自然数から{0,1}への写像の全体
|
|
|
246
|
|
|
247 である。自然数に1対1対応する集合を可算集合という。これらの集合は可算集合ではないことが対角線論法からわかる。
|
|
|
248
|
|
|
249 この文字列の先頭に 0. を付けると、0から1 の実数を表す。実数の集合は可算集合でないことがわかる。
|
|
|
250
|
|
|
251 また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。
|
|
|
252
|
|
|
253 --対角線論法と Turing machine の対応
|
|
|
254
|
|
|
255 halt(tm,x) は、文字列 tm+x から、{0,1 } への写像を与える。文字列は、bit pattern と考えると、巨大な自然数となる。 tm であれば、文字列表現を持つ。
|
|
|
256
|
|
|
257 つまり、halt は 入力 x に対して Turing machine を、その表現の自然数順に並べた時に、止まるものを1、そうでないものを0とする文字列を与える。
|
|
|
258
|
|
|
259 入力 x も文字列なので、halt(tm,x) は二次元の0,1のパターンになる。横軸が tm で、縦軸が x として、
|
|
|
260
|
|
|
261 00000000000000000000000000100000....
|
|
|
262 01000000000000000000000000001000....
|
|
|
263 01100000000000000000000000000100....
|
|
|
264 01110000000000000000000000000010....
|
|
|
265 01111000000000000000000000000000....
|
|
|
266 01111100000000000000000000000000....
|
|
|
267 01011100000000000000000000000000....
|
|
|
268 ...
|
|
|
269 ...
|
|
|
270 ...
|
|
|
271
|
|
|
272 この文字列の表が halt(tm,x) を決めている。特性関数などと呼ばれる。
|
|
|
273
|
|
|
274 halt(x,x) は対角線要素になる。その否定を考えよう。
|
|
|
275
|
|
|
276 not(tm) = 1 halt(tm,tm) が0 (5)
|
|
|
277 not(tm) = 0 halt(tm,tm) が1 (6)
|
|
|
278
|
|
|
279 not(x) は、haltを入力順にした表の対角線要素を反転したものになる。(前の neg とは少し異なる)
|
|
|
280 この文字列は、x 番目の入力文字列に対するnot(x)の値を示している。
|
|
|
281
|
|
|
282 対角線論法から、not(x) の文字列は、haltを特徴付ける可算個のパターンに含まれてない。
|
|
|
283
|
|
|
284 もし、halt(tm,x) の x に not(x) が含まれていれば、同じパターンが出てくるはずである。
|
|
|
285 つまり、not(x) は、halt(tm,x) が判定できる範囲に含まれてないことがわかる。
|
|
|
286
|
|
|
287 --対角線論法に対する考察
|
|
|
288
|
|
|
289 tm(x) を実行して停止すれば、それは判定できる。しかし、停止しないかどうかはわからない。実際に、わからない tm を構成することはできて、それが not(x) である。
|
|
|
290
|
|
|
291 neg(neg) の議論は ⊥ を使っていたが、not(x) では、halt(tm,x) の特徴関数の入力に not(x) が含まれるかどうかに変わっている。
|
|
|
292
|
|
|
293 Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。
|
|
|
294
|
|
|
295 --さまざまな決定不能問題
|
|
|
296
|
|
|
297 多くの問題は Turing machine の停止性に帰着できる。
|
|
|
298
|
|
|
299 ディオファントス方程式
|
|
|
300 文脈依存文法
|
|
|
301 Automaton を含む方程式
|
|
|
302
|
