|
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
|
|
326
|
20 record TM ( Q : Set ) ( Σ : Set )
|
|
127
|
21 : Set where
|
|
|
22 field
|
|
326
|
23 automaton : Automaton Q Σ
|
|
|
24 tδ : Q → Σ → Write Σ × Move
|
|
127
|
25 tnone : Σ
|
|
326
|
26 taccept : Q → List Σ → ( Q × List Σ × List Σ )
|
|
|
27 taccept q L = move1 (aend automaton) tnone (δ automaton) tδ q L []
|
|
127
|
28
|
|
|
29 書き込みと移動を二つのstack( List Σ)に対する関数として定義する。
|
|
|
30
|
|
|
31 {-# TERMINATING #-}
|
|
|
32 move : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
33 move q L [] = move q L ( tnone ∷ [] )
|
|
|
34 move q [] R = move q ( tnone ∷ [] ) R
|
|
|
35 move q ( LH ∷ LT ) ( RH ∷ RT ) with tδ q LH
|
|
|
36 ... | nq , write x , left = ( nq , ( RH ∷ x ∷ LT ) , RT )
|
|
|
37 ... | nq , write x , right = ( nq , LT , ( x ∷ RH ∷ RT ) )
|
|
|
38 ... | nq , write x , mnone = ( nq , ( x ∷ LT ) , ( RH ∷ RT ) )
|
|
|
39 ... | nq , wnone , left = ( nq , ( RH ∷ LH ∷ LT ) , RT )
|
|
|
40 ... | nq , wnone , right = ( nq , LT , ( LH ∷ RH ∷ RT ) )
|
|
|
41 ... | nq , wnone , mnone = ( nq , ( LH ∷ LT ) , ( RH ∷ RT ) )
|
|
|
42 {-# TERMINATING #-}
|
|
|
43 move-loop : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
44 move-loop q L R with tend q
|
|
|
45 ... | true = ( q , L , R )
|
|
|
46 ... | flase = move-loop ( proj₁ next ) ( proj₁ ( proj₂ next ) ) ( proj₂ ( proj₂ next ) )
|
|
|
47 where
|
|
|
48 next = move q L R
|
|
|
49 {-# TERMINATING #-}
|
|
|
50 move0 : (q : Q ) ( L : List Σ ) ( L : List Σ ) → ( Q × List Σ × List Σ )
|
|
|
51 move0 q L R with tend q
|
|
|
52 ... | true = ( q , L , R )
|
|
|
53 move0 q L [] | false = move0 q L ( tnone ∷ [] )
|
|
|
54 move0 q [] R | false = move0 q ( tnone ∷ [] ) R
|
|
|
55 move0 q ( LH ∷ LT ) ( RH ∷ RT ) | false with tδ q LH
|
|
|
56 ... | nq , write x , left = move0 nq ( RH ∷ x ∷ LT ) RT
|
|
|
57 ... | nq , write x , right = move0 nq LT ( x ∷ RH ∷ RT )
|
|
|
58 ... | nq , write x , mnone = move0 nq ( x ∷ LT ) ( RH ∷ RT )
|
|
|
59 ... | nq , wnone , left = move0 nq ( RH ∷ LH ∷ LT ) RT
|
|
|
60 ... | nq , wnone , right = move0 nq LT ( LH ∷ RH ∷ RT )
|
|
|
61 ... | nq , wnone , mnone = move0 nq ( LH ∷ LT ) ( RH ∷ RT )
|
|
|
62 {-# TERMINATING #-}
|
|
|
63 taccept : List Σ → ( Q × List Σ × List Σ )
|
|
|
64 taccept L = move0 tstart L []
|
|
|
65
|
|
|
66 --Turing Machine の例題
|
|
|
67
|
|
|
68 data CopyStates : Set where
|
|
|
69 s1 : CopyStates
|
|
|
70 s2 : CopyStates
|
|
|
71 s3 : CopyStates
|
|
|
72 s4 : CopyStates
|
|
|
73 s5 : CopyStates
|
|
|
74 H : CopyStates
|
|
|
75
|
|
|
76
|
|
|
77 Copyδ : CopyStates → ℕ → CopyStates × ( Write ℕ ) × Move
|
|
|
78 Copyδ s1 0 = (H , wnone , mnone )
|
|
|
79 Copyδ s1 1 = (s2 , write 0 , right )
|
|
|
80 Copyδ s2 0 = (s3 , write 0 , right )
|
|
|
81 Copyδ s2 1 = (s2 , write 1 , right )
|
|
|
82 Copyδ s3 0 = (s4 , write 1 , left )
|
|
|
83 Copyδ s3 1 = (s3 , write 1 , right )
|
|
|
84 Copyδ s4 0 = (s5 , write 0 , left )
|
|
|
85 Copyδ s4 1 = (s4 , write 1 , left )
|
|
|
86 Copyδ s5 0 = (s1 , write 1 , right )
|
|
|
87 Copyδ s5 1 = (s5 , write 1 , left )
|
|
|
88 Copyδ H _ = (H , wnone , mnone )
|
|
|
89 Copyδ _ (suc (suc _)) = (H , wnone , mnone )
|
|
|
90
|
|
326
|
91 copyTM : TM CopyStates ℕ
|
|
|
92 copyTM = record {
|
|
|
93 automaton = record { δ = λ q i → proj₁ (Copyδ q i) ; aend = tend }
|
|
|
94 ; tδ = λ q i → proj₂ (Copyδ q i )
|
|
127
|
95 ; tnone = 0
|
|
|
96 } where
|
|
|
97 tend : CopyStates → Bool
|
|
|
98 tend H = true
|
|
|
99 tend _ = false
|
|
|
100
|
|
326
|
101 Automaton と違って入力文字列はテープ(stack)上に置かれている。
|
|
127
|
102
|
|
326
|
103 終了状態に遷移すると計算は終了する。
|
|
|
104
|
|
|
105 つまり入力と同時に計算が終了するとは限らない。
|
|
127
|
106
|
|
|
107
|
|
|
108 -- Turing machine の停止問題
|
|
|
109
|
|
|
110 ---Universal Turing Machine
|
|
|
111
|
|
|
112 文字列 x を判定する Turinging machine tm(x) があるとする。
|
|
|
113
|
|
326
|
114 record TM : Set where
|
|
|
115 field
|
|
|
116 tm : List Bool → Maybe Bool
|
|
|
117
|
|
127
|
118 tm はプログラムなので、文字列である。tm をその文字列とする。tm が Turing machine として x を受け入れるかどうかを判定するTuring machine
|
|
|
119
|
|
326
|
120 record UTM : Set where
|
|
|
121 field
|
|
|
122 utm : TM
|
|
|
123 encode : TM → List Bool
|
|
|
124 is-tm : (t : TM) → (x : List Bool) → tm utm (encode t ++ x ) ≡ tm t x
|
|
127
|
125
|
|
326
|
126
|
|
|
127 を構成することができる。utm は引数をtとxの二つ持つが、encode t ++ x と結合した単一の文字列だと思えば単一引数になる。
|
|
|
128
|
|
127
|
129
|
|
|
130 utm は interpreter だと思えば良い。tm, utm は、停止してT/Fを返すか、停止しないかである。
|
|
|
131
|
|
326
|
132 just true 受け入れない
|
|
|
133 ust false 受け入れる
|
|
|
134 nothing 止まらない
|
|
127
|
135
|
|
326
|
136 実際に utm を構成した例がある。
|
|
127
|
137
|
|
326
|
138 <a href="../agda/utm.agda"> utm.agda </a>
|
|
|
139
|
|
|
140 これには足りないものが結構ある。実際に utm は正しく動くのか? ( record UTM を構成できるのか?)
|
|
127
|
141
|
|
|
142 --Turinng Machine の停止性の判定
|
|
|
143
|
|
|
144 halt(tm,x) は、以下のように定義される。これはまだ、Turing machine であるとは限らない。
|
|
|
145
|
|
326
|
146 record Halt : Set where
|
|
|
147 field
|
|
|
148 halt : (t : TM ) → (x : List Bool ) → Bool
|
|
|
149 is-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ true ) ⇔ ( (just true ≡ tm t x ) ∨ (just false ≡ tm t x ) )
|
|
|
150 is-not-halt : (t : TM ) → (x : List Bool ) → (halt t x ≡ false ) ⇔ ( nothing ≡ tm t x )
|
|
|
151
|
|
|
152 つまり、
|
|
|
153
|
|
127
|
154 halt(tm,x) = 0 tm(x) が止まらない (halt が停止しない) (1)
|
|
|
155 halt(tm,x) = 1 tm(x) が止まる (2)
|
|
|
156
|
|
326
|
157 halt(tm+x) 自体は Bool 、つまり停止しないことはないとする。こういう Turing machine があったらどうなるだろうか?
|
|
127
|
158
|
|
|
159 --対角線論法
|
|
|
160
|
|
|
161 0,1 からなる無限長の文字列を考えよう。これを順に拾っていく。どんな順序で拾っても、自然数の範囲では拾い切れないことをしまそう。
|
|
|
162
|
|
|
163 拾った順に、文字列を並べる。
|
|
|
164
|
|
|
165 00000000000000000000000000100000....
|
|
|
166 01000000000000000000000000001000....
|
|
|
167 01100000000000000000000000000100....
|
|
|
168 01110000000000000000000000000010....
|
|
|
169 01111000000000000000000000000000....
|
|
|
170 01111100000000000000000000000000....
|
|
|
171 01011100000000000000000000000000....
|
|
|
172 ...
|
|
|
173 ...
|
|
|
174 ...
|
|
|
175
|
|
|
176 行y列xの文字を v(x,y) とする。これは 0 か 1 である。上の文字列の対角線の要素は v(x,x) となる。以下の . が対角線要素になる。
|
|
|
177
|
|
|
178 .0000000000000000000000000100000....
|
|
|
179 0.000000000000000000000000001000....
|
|
|
180 01.00000000000000000000000000100....
|
|
|
181 011.0000000000000000000000000010....
|
|
|
182 0111.000000000000000000000000000....
|
|
|
183 01111.00000000000000000000000000....
|
|
|
184 010111.0000000000000000000000000....
|
|
|
185 ...
|
|
|
186 ...
|
|
|
187 ...
|
|
|
188
|
|
|
189 1-v(x,x) を考えると、
|
|
|
190
|
|
|
191 1000001 ...
|
|
|
192
|
|
|
193 となる。この文字列は、最初に拾った文字列のどれとも、v(x,x)のところで異なる。つまり拾った文字列とは異なる文字列が必ず存在する。
|
|
|
194
|
|
|
195 これは、順に取ってくるという方法では、無限長の文字列は尽くせないということを意味する。可算回と呼ぶ。
|
|
|
196
|
|
326
|
197
|
|
|
198
|
|
127
|
199 --2^N
|
|
|
200
|
|
|
201 この無限長の文字列は、自然数Nから{0,1} の写像と考えられる。あるいは、自然数Nの部分集合に1、それ以外に0を割り振ったものである。これを 2^N と書く。
|
|
|
202
|
|
|
203 自然数の部分集合全体
|
|
|
204 自然数から{0,1}への写像の全体
|
|
|
205
|
|
|
206 である。自然数に1対1対応する集合を可算集合という。これらの集合は可算集合ではないことが対角線論法からわかる。
|
|
|
207
|
|
|
208 この文字列の先頭に 0. を付けると、0から1 の実数を表す。実数の集合は可算集合でないことがわかる。
|
|
|
209
|
|
|
210 また、可算集合でなくても順序は持つこともわかる。実数などは非可算集合と呼ぶ。
|
|
|
211
|
|
326
|
212 -- Agda による対角線論法
|
|
127
|
213
|
|
326
|
214 record HBijection {n m : Level} (R : Set n) (S : Set m) : Set (n Level.⊔ m) where
|
|
|
215 field
|
|
|
216 fun← : S → R
|
|
|
217 fun→ : R → S
|
|
|
218 fiso← : (x : R) → fun← ( fun→ x ) ≡ x
|
|
|
219
|
|
|
220 fiso→ : (x : S ) → fun→ ( fun← x ) ≡ x もあるのだが、ここでは使わない。
|
|
|
221
|
|
|
222 diag : {S : Set } (b : HBijection ( S → Bool ) S) → S → Bool
|
|
|
223 diag b n = not (fun← b n n)
|
|
|
224
|
|
|
225 これで対角線部分の否定を采関数を定義する。
|
|
127
|
226
|
|
326
|
227 diagonal : { S : Set } → ¬ HBijection ( S → Bool ) S
|
|
|
228 diagonal {S} b = diagn1 (fun→ b (diag b) ) refl where
|
|
|
229 diagn1 : (n : S ) → ¬ (fun→ b (diag b) ≡ n )
|
|
|
230 diagn1 n dn = ¬t=f (diag b n ) ( begin
|
|
|
231 not (diag b n)
|
|
|
232 ≡⟨⟩
|
|
|
233 not (not fun← b n n)
|
|
|
234 ≡⟨ cong (λ k → not (k n) ) (sym (fiso← b _)) ⟩
|
|
|
235 not (fun← b (fun→ b (diag b)) n)
|
|
|
236 ≡⟨ cong (λ k → not (fun← b k n) ) dn ⟩
|
|
|
237 not (fun← b n n)
|
|
|
238 ≡⟨⟩
|
|
|
239 diag b n
|
|
|
240 ∎ ) where open ≡-Reasoning
|
|
127
|
241
|
|
326
|
242 それに対して、HBijection ( S → Bool ) S があるとすると、
|
|
|
243
|
|
|
244 not (diag b n) ≡ diag b n
|
|
127
|
245
|
|
326
|
246 となっている。証明の各段階を追ってみよ。
|
|
|
247
|
|
|
248
|
|
|
249 --halt が tm ではあり得ないこの証明
|
|
|
250
|
|
|
251 halt の否定を考えよう。
|
|
|
252
|
|
|
253 neg(tm) = 1 halt(tm,tm) が0 (3)
|
|
|
254 neg(tm) = ⊥ halt(tm,tm) が1 (4)
|
|
|
255
|
|
|
256 つまり、halt(tm,tm) が1 の時、つまり、tm(tm) が停止する時には、neg(tm) は停止しない。neg 自体は halt があればtmとして簡単に作れる。
|
|
|
257
|
|
|
258 neg(neg) = 1
|
|
|
259
|
|
|
260 かどうか調べよう。ここで 引数の neg は Turing machine neg を表す文字列である。
|
|
|
261
|
|
|
262 まず、neg(neg) =1 と仮定する。(3) から、
|
|
|
263
|
|
|
264 halt(neg,neg) が 0
|
|
|
265
|
|
|
266 なことがわかる。つまり、neg(neg) は停止しない。neg(neg) = ⊥ 。これは最初の仮定 neg(neg)=1に矛盾する。
|
|
|
267
|
|
|
268 逆に、
|
|
|
269
|
|
|
270 neg(neg) = ⊥
|
|
|
271
|
|
|
272 とすると、(4) から、
|
|
|
273
|
|
|
274 halt(neg,neg) = 1
|
|
|
275
|
|
|
276 つまり、neg(neg) は止まる。つまり、neg(neg)=1。これも矛盾。
|
|
|
277
|
|
|
278 つまり、halt(tm,x) が⊥にならないようなものは存在しない。
|
|
|
279
|
|
|
280 つまり、Turinng machine が停止するかどうかを、必ず判定できる停止する Turing machine は存在しない。
|
|
127
|
281
|
|
326
|
282 -- Agda での構成
|
|
|
283
|
|
|
284 Halt は languageなので、存在すれば UTM で simulation できることに注意しよう。
|
|
|
285
|
|
|
286 Halt と UTM から HBijection (List Bool → Bool) (List Bool) を示す。
|
|
127
|
287
|
|
326
|
288 TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
|
|
|
289
|
|
|
290 すると、
|
|
|
291
|
|
|
292 TNL1 : UTM → ¬ Halt
|
|
|
293 TNL1 utm halt = diagonal ( TNL halt utm )
|
|
127
|
294
|
|
326
|
295 となる。TNL は以下のように構成する。
|
|
|
296
|
|
|
297 λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
|
|
|
298
|
|
|
299 は (List Bool → Bool) → List Bool になっている。
|
|
127
|
300
|
|
326
|
301 h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
|
|
|
302 h1 h x with h x
|
|
|
303 ... | true = just true
|
|
|
304 ... | false = nothing
|
|
|
305 λ h → encode utm record { tm = h1 h }
|
|
|
306
|
|
|
307 は、List Bool → (List Bool → Bool である。
|
|
|
308
|
|
|
309 これから、fiso← を導けば良い。
|
|
127
|
310
|
|
326
|
311 TNL : (halt : Halt ) → (utm : UTM) → HBijection (List Bool → Bool) (List Bool)
|
|
|
312 TNL halt utm = record {
|
|
|
313 fun← = λ tm x → Halt.halt halt (UTM.utm utm) (tm ++ x)
|
|
|
314 ; fun→ = λ h → encode utm record { tm = h1 h }
|
|
|
315 ; fiso← = λ h → f-extensionality (λ y → TN1 h y )
|
|
|
316 } where
|
|
|
317 open ≡-Reasoning
|
|
|
318 h1 : (h : List Bool → Bool) → (x : List Bool ) → Maybe Bool
|
|
|
319 h1 h x with h x
|
|
|
320 ... | true = just true
|
|
|
321 ... | false = nothing
|
|
|
322 tenc : (h : List Bool → Bool) → (y : List Bool) → List Bool
|
|
|
323 tenc h y = encode utm (record { tm = λ x → h1 h x }) ++ y
|
|
|
324 h-nothing : (h : List Bool → Bool) → (y : List Bool) → h y ≡ false → h1 h y ≡ nothing
|
|
|
325 h-nothing h y eq with h y
|
|
|
326 h-nothing h y refl | false = refl
|
|
|
327 h-just : (h : List Bool → Bool) → (y : List Bool) → h y ≡ true → h1 h y ≡ just true
|
|
|
328 h-just h y eq with h y
|
|
|
329 h-just h y refl | true = refl
|
|
|
330 TN1 : (h : List Bool → Bool) → (y : List Bool ) → Halt.halt halt (UTM.utm utm) (tenc h y) ≡ h y
|
|
|
331 TN1 h y with h y | inspect h y
|
|
|
332 ... | true | record { eq = eq1 } = begin
|
|
|
333 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-halt halt (UTM.utm utm) (tenc h y) ) (case1 (sym tm-tenc)) ⟩
|
|
|
334 true ∎ where
|
|
|
335 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ just true
|
|
|
336 tm-tenc = begin
|
|
|
337 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩
|
|
|
338 h1 h y ≡⟨ h-just h y eq1 ⟩
|
|
|
339 just true ∎
|
|
|
340 ... | false | record { eq = eq1 } = begin
|
|
|
341 Halt.halt halt (UTM.utm utm) (tenc h y) ≡⟨ proj2 (is-not-halt halt (UTM.utm utm) (tenc h y) ) (sym tm-tenc) ⟩
|
|
|
342 false ∎ where
|
|
|
343 tm-tenc : tm (UTM.utm utm) (tenc h y) ≡ nothing
|
|
|
344 tm-tenc = begin
|
|
|
345 tm (UTM.utm utm) (tenc h y) ≡⟨ is-tm utm _ y ⟩
|
|
|
346 h1 h y ≡⟨ h-nothing h y eq1 ⟩
|
|
|
347 nothing ∎
|
|
|
348 -- the rest of bijection means encoding is unique
|
|
|
349 -- fiso→ : (y : List Bool ) → encode utm record { tm = λ x → h1 (λ tm → Halt.halt halt (UTM.utm utm) tm ) x } ≡ y
|
|
127
|
350
|
|
326
|
351 f-extensionality は関数の入出力がすべて一致すれば関数自体が等しいという仮定である。これは Agda では証明できない。
|
|
127
|
352
|
|
|
353 Turing machine が停止するかどうかではなく、論理の真か偽か限定しても同じ問題がある。ただし、入力に自分自身を記述できる能力がある論理の場合である。自然数を使って論理自体を記述することができるので、自然数論を論理が含んでいるかどうかが、決定不能問題を含んでいるかどうかの鍵となる。
|
|
|
354
|
|
326
|
355 HBijection を使わずに diag1 を直接つかって証明することもできる。この場合は halt が UTM で simulation できること
|
|
|
356 から矛盾がでる。
|
|
|
357
|
|
127
|
358 --さまざまな決定不能問題
|
|
|
359
|
|
|
360 多くの問題は Turing machine の停止性に帰着できる。
|
|
|
361
|
|
|
362 ディオファントス方程式
|
|
326
|
363 文脈依存文法の判定
|
|
127
|
364 Automaton を含む方程式
|
|
|
365
|
