8 abbreviation |
8 abbreviation |
9 "update p a == new_tape a p" |
9 "update p a == new_tape a p" |
10 |
10 |
11 |
11 |
12 lemma fetch_def2: |
12 lemma fetch_def2: |
13 shows "fetch p 0 b = (Nop, 0)" |
13 shows "fetch p 0 b == (Nop, 0)" |
14 and "fetch p (Suc s) Bk = |
14 and "fetch p (Suc s) Bk == |
15 (case nth_of p (2 * s) of |
15 (case nth_of p (2 * s) of |
16 Some i \<Rightarrow> i |
16 Some i \<Rightarrow> i |
17 | None \<Rightarrow> (Nop, 0))" |
17 | None \<Rightarrow> (Nop, 0))" |
18 and "fetch p (Suc s) Oc = |
18 and "fetch p (Suc s) Oc == |
19 (case nth_of p ((2 * s) + 1) of |
19 (case nth_of p ((2 * s) + 1) of |
20 Some i \<Rightarrow> i |
20 Some i \<Rightarrow> i |
21 | None \<Rightarrow> (Nop, 0))" |
21 | None \<Rightarrow> (Nop, 0))" |
|
22 apply - |
|
23 apply(rule_tac [!] eq_reflection) |
22 by (auto split: block.splits simp add: fetch.simps) |
24 by (auto split: block.splits simp add: fetch.simps) |
23 |
25 |
24 lemma new_tape_def2: |
26 lemma new_tape_def2: |
25 shows "new_tape W0 (l, r) == (l, Bk#(tl r))" |
27 shows "new_tape W0 (l, r) == (l, Bk#(tl r))" |
26 and "new_tape W1 (l, r) == (l, Oc#(tl r))" |
28 and "new_tape W1 (l, r) == (l, Oc#(tl r))" |
256 \end{center} |
258 \end{center} |
257 |
259 |
258 \noindent |
260 \noindent |
259 The first two clauses replace the head of the right-list |
261 The first two clauses replace the head of the right-list |
260 with new a @{term Bk} or @{term Oc}, repsectively. To see that |
262 with new a @{term Bk} or @{term Oc}, repsectively. To see that |
261 these clauses make sense in case where @{text r} is the empty |
263 these tow clauses make sense in case where @{text r} is the empty |
262 list, one has to know that the tail function, @{term tl}, is defined |
264 list, one has to know that the tail function, @{term tl}, is defined |
263 such that @{term "tl [] == []"} holds. The third clause |
265 such that @{term "tl [] == []"} holds. The third clause |
264 implements the move of the read-write unit to the left: we need |
266 implements the move of the read-write unit one step to the left: we need |
265 to test if the left-list is empty; if yes, then we just add a |
267 to test if the left-list @{term l} is empty; if yes, then we just prepend a |
266 blank cell to the right-list; otherwise we have to remove the |
268 blank cell to the right-list; otherwise we have to remove the |
267 head from the left-list and add it to the right-list. Similarly |
269 head from the left-list and prepend it to the right-list. Similarly |
268 in the clause for the right move. The @{term Nop} operation |
270 in the clause for a right move action. The @{term Nop} operation |
269 leaves the the tape unchanged. |
271 leaves the the tape unchanged. |
270 |
272 |
271 Note that our treatment of the tape is rather ``unsymmetric''---we |
273 Note that our treatment of the tape is rather ``unsymmetric''---we |
272 have the convention that the head of the right-list is where |
274 have the convention that the head of the right-list is where the |
273 the read-write unit is currently possitioned. Asperti and |
275 read-write unit is currently positioned. Asperti and Ricciotti |
274 Ricciotti \cite{AspertiRicciotti12} also consider such a |
276 \cite{AspertiRicciotti12} also consider such a representation, but |
275 representation, but dismiss it as it complicates their |
277 dismiss it as it complicates their definition for \emph{tape |
276 definition for \emph{tape equality}. The reason is that |
278 equality}. The reason is that moving the read-write unit one step to |
277 moving the read-write unit to the left and then back |
279 the left and then back to the right might change the tape (in case |
278 to the right can change the tape (in case of going |
280 of going over the ``edge''). Therefore they distinguish four types |
279 over the ``edge''). Therefore they distinguish four |
281 of tapes: one where the tape is empty; another where the read-write |
280 cases where the tape is empty as well as the read-write unit |
282 unit is on the left edge, respectively right edge, and in the middle |
281 on the left edge, respectively right edge, or in the |
283 of the tape. The reading, writing and moving of the tape is then |
282 middle. The reading and moving of the tape is then |
284 defined in terms of these four cases. In this way they can keep the |
283 defined in terms of these four cases. Since we are not |
285 tape in a ``normalised'' form, and thus making a left-move followed |
284 going to use the notion of tape equality, we can |
286 by a right-move being the identity on tapes. Since we are not using |
285 get away with the definition above and be done with |
287 the notion of tape equality, we can get away with the unsymmetric |
286 all corner cases. |
288 definition above and by using the @{term update} function |
|
289 cover uniformely all cases including the corner cases. |
287 |
290 |
288 Next we need to define the \emph{states} of a Turing machine. Given |
291 Next we need to define the \emph{states} of a Turing machine. Given |
289 how little is usually said about how to represent states in informal |
292 how little is usually said about how to represent them in informal |
290 presentaions, it might be surprising that in a theorem prover we have |
293 presentaions, it might be surprising that in a theorem prover we have |
291 to select carfully a representation. If we use the naive representation |
294 to select carfully a representation. If we use the naive representation |
292 as a Turing machine consiting of a finite set of states, then we |
295 where a Turing machine consists of a finite set of states, then we |
293 will have difficulties composing two Turing machines. We would need |
296 will have difficulties composing two Turing machines. In this case we |
294 to somehow combine the two finite sets of states, possibly renaming |
297 would need to combine two finite sets of states, possibly requiring |
295 states apart if both machines share states. This renaming can be |
298 renaming states apart whenever both machines share states. This |
296 quite cumbersome to reason about. Therefore we made the choice |
299 renaming can be quite cumbersome to reason about. Therefore we made |
297 of representing a state by a natural number and the states of a |
300 the choice of representing a state by a natural number and the states |
298 Turing machine will always consist of the initial segment |
301 of a Turing machine will always consist of the initial segment |
299 of natural numbers starting from @{text 0} up to number of states |
302 of natural numbers starting from @{text 0} up to number of states |
300 of the machine minus @{text 1}. In doing so we can compose |
303 of the machine minus @{text 1}. In doing so we can compose |
301 two Turing machine by ``shifting'' the states of one by an appropriate |
304 two Turing machine by ``shifting'' the states of one by an appropriate |
302 amount to a higher segment. |
305 amount to a higher segment. |
303 |
306 |
304 An \emph{instruction} of a Turing machine is a pair consisting of a |
307 An \emph{instruction} of a Turing machine is a pair consisting of a |
305 natural number (the next state) and an action. A \emph{program} of a Turing |
308 natural number (the next state) and an action. A \emph{program} of a Turing |
306 machine is then a list of such pairs. Given a program @{term p}, a state |
309 machine is then a list of such pairs. Given a program @{term p}, a state |
307 and a cell being read by the read-write unnit, we need to fetch |
310 and the cell being read by the read-write unit, we need to fetch |
308 the corresponding instruction in the program. For this we define |
311 the corresponding instruction from the program. For this we define |
309 the function @{term fetch} |
312 the function @{term fetch} |
310 |
313 |
311 \begin{center} |
314 \begin{center} |
312 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
315 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
313 @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\<equiv>"} & @{thm (rhs) fetch_def2(1)}\\ |
316 \multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\ |
314 @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\ |
317 @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\ |
315 \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\ |
318 \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\ |
|
319 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\ |
|
320 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}}\\ |
316 @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\ |
321 @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\ |
317 \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\ |
322 \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\ |
|
323 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) |"}}\\ |
|
324 \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \<Rightarrow> i"}} |
318 \end{tabular} |
325 \end{tabular} |
319 \end{center} |
326 \end{center} |
320 |
327 |
|
328 start state |
|
329 |
|
330 What is tinres? What is it used for? |
|
331 |
|
332 \begin{center} |
|
333 @{thm dither_def} |
|
334 \end{center} |
|
335 |
|
336 |
|
337 A \emph{configuration} @{term c} of a Turing machine is a state together with |
|
338 a tape. If we have a configuration and a program, we can calculate |
|
339 what the next configuration is by fetching the appropriate next state |
|
340 and action from the program. Such a single step of execution can be defined as |
|
341 |
|
342 \begin{center} |
|
343 @{thm tstep_def2(1)}\\ |
|
344 @{thm tstep_def2(2)}\\ |
|
345 \end{center} |
321 |
346 |
322 For showing the undecidability of the halting problem, we need to consider |
347 For showing the undecidability of the halting problem, we need to consider |
323 two specific Turing machines. |
348 two specific Turing machines. |
324 |
349 |
325 |
350 |