# HG changeset patch # User Christian Urban # Date 1357806462 0 # Node ID cb8754a0568a556d219071d4c48cd87a11b0f5a7 # Parent c5e3007fed2a3f060b161b714676acec80164436 update diff -r c5e3007fed2a -r cb8754a0568a Paper.thy --- a/Paper.thy Thu Jan 10 07:34:08 2013 +0000 +++ b/Paper.thy Thu Jan 10 08:27:42 2013 +0000 @@ -10,15 +10,17 @@ lemma fetch_def2: - shows "fetch p 0 b = (Nop, 0)" - and "fetch p (Suc s) Bk = + shows "fetch p 0 b == (Nop, 0)" + and "fetch p (Suc s) Bk == (case nth_of p (2 * s) of Some i \ i | None \ (Nop, 0))" - and "fetch p (Suc s) Oc = + and "fetch p (Suc s) Oc == (case nth_of p ((2 * s) + 1) of Some i \ i | None \ (Nop, 0))" +apply - +apply(rule_tac [!] eq_reflection) by (auto split: block.splits simp add: fetch.simps) lemma new_tape_def2: @@ -258,44 +260,45 @@ \noindent The first two clauses replace the head of the right-list with new a @{term Bk} or @{term Oc}, repsectively. To see that - these clauses make sense in case where @{text r} is the empty + these tow clauses make sense in case where @{text r} is the empty list, one has to know that the tail function, @{term tl}, is defined such that @{term "tl [] == []"} holds. The third clause - implements the move of the read-write unit to the left: we need - to test if the left-list is empty; if yes, then we just add a + implements the move of the read-write unit one step to the left: we need + to test if the left-list @{term l} is empty; if yes, then we just prepend a blank cell to the right-list; otherwise we have to remove the - head from the left-list and add it to the right-list. Similarly - in the clause for the right move. The @{term Nop} operation + head from the left-list and prepend it to the right-list. Similarly + in the clause for a right move action. The @{term Nop} operation leaves the the tape unchanged. Note that our treatment of the tape is rather ``unsymmetric''---we - have the convention that the head of the right-list is where - the read-write unit is currently possitioned. Asperti and - Ricciotti \cite{AspertiRicciotti12} also consider such a - representation, but dismiss it as it complicates their - definition for \emph{tape equality}. The reason is that - moving the read-write unit to the left and then back - to the right can change the tape (in case of going - over the ``edge''). Therefore they distinguish four - cases where the tape is empty as well as the read-write unit - on the left edge, respectively right edge, or in the - middle. The reading and moving of the tape is then - defined in terms of these four cases. Since we are not - going to use the notion of tape equality, we can - get away with the definition above and be done with - all corner cases. + have the convention that the head of the right-list is where the + read-write unit is currently positioned. Asperti and Ricciotti + \cite{AspertiRicciotti12} also consider such a representation, but + dismiss it as it complicates their definition for \emph{tape + equality}. The reason is that moving the read-write unit one step to + the left and then back to the right might change the tape (in case + of going over the ``edge''). Therefore they distinguish four types + of tapes: one where the tape is empty; another where the read-write + unit is on the left edge, respectively right edge, and in the middle + of the tape. The reading, writing and moving of the tape is then + defined in terms of these four cases. In this way they can keep the + tape in a ``normalised'' form, and thus making a left-move followed + by a right-move being the identity on tapes. Since we are not using + the notion of tape equality, we can get away with the unsymmetric + definition above and by using the @{term update} function + cover uniformely all cases including the corner cases. Next we need to define the \emph{states} of a Turing machine. Given - how little is usually said about how to represent states in informal + how little is usually said about how to represent them in informal presentaions, it might be surprising that in a theorem prover we have to select carfully a representation. If we use the naive representation - as a Turing machine consiting of a finite set of states, then we - will have difficulties composing two Turing machines. We would need - to somehow combine the two finite sets of states, possibly renaming - states apart if both machines share states. This renaming can be - quite cumbersome to reason about. Therefore we made the choice - of representing a state by a natural number and the states of a - Turing machine will always consist of the initial segment + where a Turing machine consists of a finite set of states, then we + will have difficulties composing two Turing machines. In this case we + would need to combine two finite sets of states, possibly requiring + renaming states apart whenever both machines share states. This + renaming can be quite cumbersome to reason about. Therefore we made + the choice of representing a state by a natural number and the states + of a Turing machine will always consist of the initial segment of natural numbers starting from @{text 0} up to number of states of the machine minus @{text 1}. In doing so we can compose two Turing machine by ``shifting'' the states of one by an appropriate @@ -304,20 +307,42 @@ An \emph{instruction} of a Turing machine is a pair consisting of a natural number (the next state) and an action. A \emph{program} of a Turing machine is then a list of such pairs. Given a program @{term p}, a state - and a cell being read by the read-write unnit, we need to fetch - the corresponding instruction in the program. For this we define + and the cell being read by the read-write unit, we need to fetch + the corresponding instruction from the program. For this we define the function @{term fetch} \begin{center} \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} - @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\"} & @{thm (rhs) fetch_def2(1)}\\ + \multicolumn{3}{l}{@{thm fetch_def2(1)[where b=DUMMY]}}\\ @{thm (lhs) fetch_def2(2)} & @{text "\"} & \\ - \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\ + \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s) of"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \ (Nop, 0) |"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \ i"}}\\ @{thm (lhs) fetch_def2(3)} & @{text "\"} & \\ - \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\ + \multicolumn{3}{@ {\hspace{1cm}}l}{@{text "case nth_of p (2 * s + 1) of"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "None \ (Nop, 0) |"}}\\ + \multicolumn{3}{@ {\hspace{1.4cm}}l}{@{text "Some i \ i"}} \end{tabular} \end{center} + start state + + What is tinres? What is it used for? + + \begin{center} + @{thm dither_def} + \end{center} + + + A \emph{configuration} @{term c} of a Turing machine is a state together with + a tape. If we have a configuration and a program, we can calculate + what the next configuration is by fetching the appropriate next state + and action from the program. Such a single step of execution can be defined as + + \begin{center} + @{thm tstep_def2(1)}\\ + @{thm tstep_def2(2)}\\ + \end{center} For showing the undecidability of the halting problem, we need to consider two specific Turing machines. diff -r c5e3007fed2a -r cb8754a0568a paper.pdf Binary file paper.pdf has changed