44 shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))" |
43 shows "tstep (s, l, r) p == (let (a, s') = fetch p s (read r) in (s', new_tape a (l, r)))" |
45 apply - |
44 apply - |
46 apply(rule_tac [!] eq_reflection) |
45 apply(rule_tac [!] eq_reflection) |
47 by (auto split: if_splits prod.split list.split simp add: tstep.simps) |
46 by (auto split: if_splits prod.split list.split simp add: tstep.simps) |
48 |
47 |
|
48 abbreviation |
|
49 "halt p inp out == \<exists>n. steps (1, inp) p n = (0, out)" |
|
50 |
|
51 lemma haltP_def2: |
|
52 "haltP p n = (\<exists>k l m. |
|
53 halt p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))" |
|
54 unfolding haltP_def |
|
55 apply(auto) |
|
56 done |
|
57 |
49 consts DUMMY::'a |
58 consts DUMMY::'a |
50 |
59 |
51 notation (latex output) |
60 notation (latex output) |
52 Cons ("_::_" [78,77] 73) and |
61 Cons ("_::_" [78,77] 73) and |
|
62 set ("") and |
53 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
63 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
54 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
64 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
|
65 t_correct ("twf") and |
55 tstep ("step") and |
66 tstep ("step") and |
56 steps ("nsteps") and |
67 steps ("nsteps") and |
57 abc_lm_v ("lookup") and |
68 abc_lm_v ("lookup") and |
58 abc_lm_s ("set") and |
69 abc_lm_s ("set") and |
|
70 haltP ("stdhalt") and |
59 DUMMY ("\<^raw:\mbox{$\_$}>") |
71 DUMMY ("\<^raw:\mbox{$\_$}>") |
60 |
72 |
61 declare [[show_question_marks = false]] |
73 declare [[show_question_marks = false]] |
62 (*>*) |
74 (*>*) |
63 |
75 |
269 |
281 |
270 \noindent |
282 \noindent |
271 The first two clauses replace the head of the right-list |
283 The first two clauses replace the head of the right-list |
272 with a new @{term Bk} or @{term Oc}, repsectively. To see that |
284 with a new @{term Bk} or @{term Oc}, repsectively. To see that |
273 these two clauses make sense in case where @{text r} is the empty |
285 these two clauses make sense in case where @{text r} is the empty |
274 list, one has to know that the tail function, @{term tl}, is in |
286 list, one has to know that the tail function, @{term tl}, is defined in |
275 Isabelle/HOL defined |
287 Isabelle/HOL |
276 such that @{term "tl [] == []"} holds. The third clause |
288 such that @{term "tl [] == []"} holds. The third clause |
277 implements the move of the head one step to the left: we need |
289 implements the move of the head one step to the left: we need |
278 to test if the left-list @{term l} is empty; if yes, then we just prepend a |
290 to test if the left-list @{term l} is empty; if yes, then we just prepend a |
279 blank cell to the right-list; otherwise we have to remove the |
291 blank cell to the right-list; otherwise we have to remove the |
280 head from the left-list and prepend it to the right-list. Similarly |
292 head from the left-list and prepend it to the right-list. Similarly |
302 Next we need to define the \emph{states} of a Turing machine. Given |
314 Next we need to define the \emph{states} of a Turing machine. Given |
303 how little is usually said about how to represent them in informal |
315 how little is usually said about how to represent them in informal |
304 presentations, it might be surprising that in a theorem prover we have |
316 presentations, it might be surprising that in a theorem prover we have |
305 to select carfully a representation. If we use the naive representation |
317 to select carfully a representation. If we use the naive representation |
306 where a Turing machine consists of a finite set of states, then we |
318 where a Turing machine consists of a finite set of states, then we |
307 will have difficulties composing two Turing machines. In this case we |
319 will have difficulties composing two Turing machines: we |
308 would need to combine two finite sets of states, possibly requiring |
320 would need to combine two finite sets of states, possibly |
309 renaming states apart whenever both machines share states. This |
321 renaming states apart whenever both machines share |
|
322 states.\footnote{The usual disjoint union operation does not preserve types, unfortunately.} This |
310 renaming can be quite cumbersome to reason about. Therefore we made |
323 renaming can be quite cumbersome to reason about. Therefore we made |
311 the choice of representing a state by a natural number and the states |
324 the choice of representing a state by a natural number and the states |
312 of a Turing machine will always consist of the initial segment |
325 of a Turing machine will always consist of the initial segment |
313 of natural numbers starting from @{text 0} up to number of states |
326 of natural numbers starting from @{text 0} up to number of states |
314 of the machine minus @{text 1}. In doing so we can compose |
327 of the machine. In doing so we can compose |
315 two Turing machine by ``shifting'' the states of one by an appropriate |
328 two Turing machine by ``shifting'' the states of one by an appropriate |
316 amount to a higher segment and adjust some ``next states''. |
329 amount to a higher segment and adjust some ``next states''. |
317 |
330 |
318 An \emph{instruction} @{term i} of a Turing machine is a pair consisting of |
331 An \emph{instruction} @{term i} of a Turing machine is a pair consisting of |
319 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
332 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing |
332 |
345 |
333 \noindent |
346 \noindent |
334 the reader can see we have organised our Turing machine programs so |
347 the reader can see we have organised our Turing machine programs so |
335 that segments of two belong to a state. The first component |
348 that segments of two belong to a state. The first component |
336 of the segment determines what action should be taken and which next |
349 of the segment determines what action should be taken and which next |
337 state should be transitioned to in case the head read a @{term Bk}; |
350 state should be transitioned to in case the head reads a @{term Bk}; |
338 similarly the second component determines what should be done in |
351 similarly the second component determines what should be done in |
339 case of reading @{term Oc}. We have the convention that the |
352 case of reading @{term Oc}. We have the convention that the |
340 first state is always the \emph{starting state} of the Turing machine. |
353 first state is always the \emph{starting state} of the Turing machine. |
341 The 0-state is special in that it will be used as \emph{halting state}. |
354 The 0-state is special in that it will be used as the \emph{halting state}. |
342 There are no instructions for the 0-state, but it will always |
355 There are no instructions for the 0-state, but it will always |
343 perform a @{term Nop}-operation and remain in the 0-state. |
356 perform a @{term Nop}-operation and remain in the 0-state. |
344 |
357 A \emph{well-formed} Turing machine program @{term p} is one that satisfies |
|
358 the following three properties |
|
359 |
|
360 \begin{center} |
|
361 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
362 @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\ |
|
363 & @{text "\<and>"} & @{term "iseven (length p)"}\\ |
|
364 & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"} |
|
365 \end{tabular} |
|
366 \end{center} |
|
367 |
|
368 \noindent |
|
369 The first says that @{text p} must have at least an instruction for the starting |
|
370 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every |
|
371 state, and the third that every next-state is one of the states mentioned in |
|
372 the program or being the 0-state. |
|
373 |
345 Given a program @{term p}, a state |
374 Given a program @{term p}, a state |
346 and the cell being read by the head, we need to fetch |
375 and the cell being read by the head, we need to fetch |
347 the corresponding instruction from the program. For this we define |
376 the corresponding instruction from the program. For this we define |
348 the function @{term fetch} |
377 the function @{term fetch} |
349 |
378 |
360 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}} |
389 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}} |
361 \end{tabular} |
390 \end{tabular} |
362 \end{center} |
391 \end{center} |
363 |
392 |
364 \noindent |
393 \noindent |
365 |
394 In this definition the function @{term nth_of} returns the @{text n}th element |
|
395 from a list, if it exists (@{term Some}-case), or if it does not, it |
|
396 returns the default action @{term Nop} and the default state 0 |
|
397 (@{term None}-case). In doing so we slightly deviate from the description |
|
398 in \cite{Boolos87}: if their Turing machines transition to a non-existing |
|
399 state, then the computation is halted. We will transition in such cases |
|
400 to the 0th state with the @{term Nop}-action. |
366 |
401 |
367 A \emph{configuration} @{term c} of a Turing machine is a state together with |
402 A \emph{configuration} @{term c} of a Turing machine is a state together with |
368 a tape. This is written as the triple @{term "(s, l, r)"}. If we have a |
403 a tape. This is written as @{text "(s, (l, r))"}. If we have a |
369 configuration and a program, we can calculate |
404 configuration and a program, we can calculate |
370 what the next configuration is by fetching the appropriate next state |
405 what the next configuration is by fetching the appropriate next state |
371 and action from the program. Such a single step of execution can be defined as |
406 and action from the program, and updating the state and tape accordingly. |
|
407 This single step of execution is defined as the function @{term tstep}: |
372 |
408 |
373 \begin{center} |
409 \begin{center} |
374 \begin{tabular}{l} |
410 \begin{tabular}{l} |
375 @{thm (lhs) tstep_def2(1)} @{text "\<equiv>"}\\ |
411 @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\ |
376 \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\ |
412 \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\ |
377 \hspace{10mm}@{text "in (s', update (l, r) a)"} |
413 \hspace{10mm}@{text "in (s', update (l, r) a)"} |
378 \end{tabular} |
414 \end{tabular} |
379 \end{center} |
415 \end{center} |
380 |
416 |
381 No evaluator in HOL, because of totality. |
417 \noindent |
|
418 It is impossible in Isabelle/HOL to lift this function in order to realise |
|
419 a general evaluation function for Turing machines. The reason is that functions in HOL-based |
|
420 provers need to be terminating, and clearly there are Turing machine |
|
421 programs for which this does not hold. We can however define an evaluation |
|
422 function so that it performs exactly @{text n}: |
382 |
423 |
383 \begin{center} |
424 \begin{center} |
384 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
425 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
385 @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\ |
426 @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\ |
386 @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\ |
427 @{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\ |
387 \end{tabular} |
428 \end{tabular} |
388 \end{center} |
429 \end{center} |
389 |
430 |
390 \emph{well-formedness} of a Turing program |
431 \noindent |
391 |
432 Recall our definition of @{term fetch} with the default value for |
392 programs halts |
433 the 0th state. In case a Turing program takes in \cite{Boolos87} less |
|
434 then @{text n} steps before it halts, then in our setting the evaluation |
|
435 does not halt, but rather transitions to the 0th state and remain there |
|
436 performing @{text Nop}-actions. |
|
437 |
|
438 Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program |
|
439 @{term p} halts generating an output tape @{text "(l\<^isub>o,r\<^isub>o)"}: |
|
440 |
|
441 \begin{center} |
|
442 \begin{tabular}{l} |
|
443 @{term "halt p (l\<^isub>i,r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\ |
|
444 \hspace{6mm}@{text "\<exists> n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n= (0, (l\<^isub>o,r\<^isub>o))"} |
|
445 \end{tabular} |
|
446 \end{center} |
|
447 |
|
448 \noindent |
|
449 Later on we need to consider specific Turing machines that |
|
450 start with a tape in standard form and halt the computation |
|
451 in standard form. By this we mean |
|
452 |
|
453 \begin{center} |
|
454 @{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]} |
|
455 \end{center} |
|
456 |
|
457 \noindent |
|
458 the Turing machine starts with a tape containg @{text n} @{term Oc}s |
|
459 and the head pointing to the first one; the Turing machine |
|
460 halts with a tape consisting of some @{term Bk}s, followed by a |
|
461 ``cluster'' of @{term Oc}s and after that by some @{term Bk}s. |
|
462 The head in the output is at the first @{term Oc}. |
|
463 The intuitive meaning of this definition is to start Turing machine with a |
|
464 tape corresponding to a value @{term n} and producing |
|
465 a new tape corresponding to the value @{term l} (the number of @{term Oc}s |
|
466 clustered on the tape). |
393 |
467 |
394 shift and change of a p |
468 shift and change of a p |
395 |
469 |
396 composition of two ps |
470 composition of two ps |
397 |
471 |