tm: comparison Paper.thy

equal deleted inserted replaced

-:284468a61346
+:22e5804b135c
 apply -
 apply(rule_tac [!] eq_reflection)
 by (auto split: if_splits prod.split list.split simp add: tstep.simps)
 abbreviation
-"halt p inp out == \<exists>n. steps (1, inp) p n = (0, out)"
+"run p inp out == \<exists>n. steps (1, inp) p n = (0, out)"
 lemma haltP_def2:
 "haltP p n = (\<exists>k l m.
-halt p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
+run p ([], exponent Oc n) (exponent Bk k, exponent Oc l @ exponent Bk m))"
 unfolding haltP_def
 apply(auto)
 done
+lemma tape_of_nat_list_def2:
+shows "tape_of_nat_list [] = []"
+and "tape_of_nat_list [n] = exponent Oc (n+1)"
+and "ns\<noteq> [] ==> tape_of_nat_list (n#ns) = (exponent Oc (n+1)) @ [Bk] @ (tape_of_nat_list ns)"
+apply(auto simp add: tape_of_nat_list.simps)
+apply(case_tac ns)
+apply(auto simp add: tape_of_nat_list.simps)
+done
+lemma tshift_def2:
+fixes p::"tprog"
+shows "tshift p n == (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"
+apply(rule eq_reflection)
+apply(auto simp add: tshift.simps)
+done
 consts DUMMY::'a
 notation (latex output)
 Cons ("_::_" [78,77] 73) and
 tstep ("step") and
 steps ("nsteps") and
 abc_lm_v ("lookup") and
 abc_lm_s ("set") and
 haltP ("stdhalt") and
+change-termi-state ("adjust") and
+tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
 DUMMY  ("\<^raw:\mbox{$\_$}>")
 declare [[show_question_marks = false]]
 (*>*)
 data-structures at hand are ``structurally'' defined, like lists,
 natural numbers, regular expressions, etc. Such data-structures come
 with convenient reasoning infrastructures (for example induction
 principles, recursion combinators and so on).  But this is \emph{not}
 the case with Turing machines (and also not with register machines):
-underlying their definition is a set of states together with a
+underlying their definitions are sets of states together with
-transition function, both of which are not structurally defined.  This
+transition functions, all of which are not structurally defined.  This
 means we have to implement our own reasoning infrastructure in order
 to prove properties about them. This leads to annoyingly fiddly
 formalisations.  We noticed first the difference between both,
 structural and non-structural, ``worlds'' when formalising the
 Myhill-Nerode theorem, where regular expressions fared much better
 We are not the first who formalised Turing machines in a theorem
 prover: we are aware of the preliminary work by Asperti and Ricciotti
 \cite{AspertiRicciotti12}. They describe a complete formalisation of
 Turing machines in the Matita theorem prover, including a universal
 Turing machine. They report that the informal proofs from which they
-started are not ``sufficiently accurate to be directly useable as a
+started are \emph{not} ``sufficiently accurate to be directly useable as a
 guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
 our formalisation we followed mainly the proofs from the textbook
 \cite{Boolos87} and found that the description there is quite
 detailed. Some details are left out however: for example, it is only
 shown how the universal Turing machine is constructed for Turing
 (represented by @{term Bk} and @{term Oc}, respectively, in our
 formalisation). Traditionally the content of a cell can be any
 character from a finite alphabet. Although computationally equivalent,
 the more restrictive notion of Turing machines in \cite{Boolos87} makes
 the reasoning more uniform. In addition some proofs \emph{about} Turing
-machines will be simpler.  The reason is that one often needs to encode
+machines are simpler.  The reason is that one often needs to encode
 Turing machines---consequently if the Turing machines are simpler, then the coding
 functions are simpler too. Unfortunately, the restrictiveness also makes
-it harder to design programs for these Turing machines. Therefore in order
+it harder to design programs for these Turing machines. In order
-to construct a \emph{universal Turing machine} we follow the proof in
+to construct a \emph{universal Turing machine} we therefore do not follow
+\cite{AspertiRicciotti12}, instead follow the proof in
 \cite{Boolos87} by relating abacus machines to Turing machines and in
 turn recursive functions to abacus machines. The universal Turing
 machine can then be constructed as a recursive function.
 \smallskip
 \end{tikzpicture}
 \end{center}
 \noindent
 Note that by using lists each side of the tape is only finite. The
-potential infinity is achieved by adding an appropriate blank cell
+potential infinity is achieved by adding an appropriate blank or occupied cell
-whenever the read-write unit goes over the ``edge'' of the tape. To
+whenever the head goes over the ``edge'' of the tape. To
 make this formal we define five possible \emph{actions}
 the Turing machine can perform:
 \begin{center}
 \begin{tabular}{rcll}
 \end{center}
 \noindent
 We slightly deviate
 from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
-will become important when we formalise universal Turing
+will become important when we formalise halting computations and also universal Turing
-machines later. Given a tape and an action, we can define the
+machines. Given a tape and an action, we can define the
 following tape updating function:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\
 such that @{term "tl [] == []"} holds. The third clause
 implements the move of the head 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 prepend it to the right-list. Similarly
-in the clause for a right move action. The @{term Nop} operation
+in the fourth clause for a right move action. The @{term Nop} operation
-leaves the the tape unchanged.
+leaves the the tape unchanged (last clause).
 Note that our treatment of the tape is rather ``unsymmetric''---we
 have the convention that the head of the right-list is where the
 head is currently positioned. Asperti and Ricciotti
 \cite{AspertiRicciotti12} also considered such a representation, but
 definition above, and by using the @{term update} function
 cover uniformely all cases including corner cases.
 Next we need to define the \emph{states} of a Turing machine.  Given
 how little is usually said about how to represent them in informal
-presentations, it might be surprising that in a theorem prover we have
+presentations, it might be surprising that in a theorem prover we
-to select carfully a representation. If we use the naive representation
+have to select carfully a representation. If we use the naive
-where a Turing machine consists of a finite set of states, then we
+representation where a Turing machine consists of a finite set of
-will have difficulties composing two Turing machines: we
+states, then we will have difficulties composing two Turing
-would need to combine two finite sets of states, possibly
+machines: we would need to combine two finite sets of states,
-renaming states apart whenever both machines share
+possibly renaming states apart whenever both machines share
-states.\footnote{The usual disjoint union operation does not preserve types, unfortunately.} This
+states.\footnote{The usual disjoint union operation in Isabelle/HOL
-renaming can be quite cumbersome to reason about. Therefore we made
+cannot be used as it does not preserve types.} This renaming can be
-the choice of representing a state by a natural number and the states
+quite cumbersome to reason about. Therefore we made the choice of
-of a Turing machine will always consist of the initial segment
+representing a state by a natural number and the states of a Turing
-of natural numbers starting from @{text 0} up to the number of states
+machine will always consist of the initial segment of natural
-of the machine. In doing so we can compose
+numbers starting from @{text 0} up to the number of states of the
-two Turing machine by ``shifting'' the states of one by an appropriate
+machine. In doing so we can compose two Turing machine by
-amount to a higher segment and adjust some ``next states'' in the other.
+shifting the states of one by an appropriate amount to a higher
+segment and adjusting some ``next states'' in the other.
 An \emph{instruction} @{term i} of a Turing machine is a pair consisting of
 an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
-machine is then a list of such pairs. Using the following Turing machine
+machine is then a list of such pairs. Using as an example the following Turing machine
-program (consisting of four instructions) as an example
+program, which consists of four instructions
-\begin{center}
+\begin{equation}
 \begin{tikzpicture}
 \node [anchor=base] at (0,0) {@{thm dither_def}};
 \node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
 \node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
 \node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
 \node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
 \end{tikzpicture}
-\end{center}
+\label{dither}
+\end{equation}
-\noindent
-the reader can see we have organised our Turing machine programs so
+\noindent
-that segments of two belong to a state. The first component
+the reader can see we have organised our Turing machine programs so
-of the segment determines what action should be taken and which next
+that segments of two belong to a state. The first component of the
-state should be transitioned to in case the head reads a @{term Bk};
+segment determines what action should be taken and which next state
+should be transitioned to in case the head reads a @{term Bk};
 similarly the second component determines what should be done in
-case of reading @{term Oc}. We have the convention that the
+case of reading @{term Oc}. We have the convention that the first
-first state is always the \emph{starting state} of the Turing machine.
+state is always the \emph{starting state} of the Turing machine.
-The 0-state is special in that it will be used as the \emph{halting state}.
+The zeroth state is special in that it will be used as the
-There are no instructions for the 0-state, but it will always
+``halting state''.  There are no instructions for the @{text
-perform a @{term Nop}-operation and remain in the 0-state.
+0}-state, but it will always perform a @{term Nop}-operation and
+remain in the @{text 0}-state.  Unlike Asperti and Riccioti
+\cite{AspertiRicciotti12}, we have chosen a very concrete
+representation for programs, because when constructing a universal
+Turing machine, we need to define a coding function for programs.
+This can be easily done for our programs-as-lists, but is more
+difficult for the functions used by Asperti and Ricciotti.
 Given a program @{term p}, a state
 and the cell being read by the head, we need to fetch
 the corresponding instruction from the program. For this we define
 the function @{term fetch}
 \end{tabular}
 \end{center}
 \noindent
 In this definition the function @{term nth_of} returns the @{text n}th element
-from a list, if it exists (@{term Some}-case), or if it does not, it
+from a list, provided it exists (@{term Some}-case), or if it does not, it
-returns the default action @{term Nop} and the default state 0
+returns the default action @{term Nop} and the default state @{text 0}
 (@{term None}-case). In doing so we slightly deviate from the description
 in \cite{Boolos87}: if their Turing machines transition to a non-existing
 state, then the computation is halted. We will transition in such cases
-to the 0th state with the @{term Nop}-action. However, with introducing the
+to the @{text 0}-state. However, with introducing the
-notion of \emph{well-formed} Turing machine programs we will exclude such
+notion of \emph{well-formed} Turing machine programs we will later exclude such
-cases. A program @{term p} is said to be well-formed if it satisfies
+cases and make the  @{text 0}-state the only ``halting state''. A program
-the following three properties
+@{term p} is said to be well-formed if it satisfies
+the following three properties:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
 & @{text "\<and>"} & @{term "iseven (length p)"}\\
 \noindent
 The first says that @{text p} must have at least an instruction for the starting
 state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
 state, and the third that every next-state is one of the states mentioned in
-the program or being the 0-state.
+the program or being the @{text 0}-state.
 A \emph{configuration} @{term c} of a Turing machine is a state together with
 a tape. This is written as @{text "(s, (l, r))"}. If we have a
 configuration and a program, we can calculate
-what the next configuration is by fetching the appropriate next state
+what the next configuration is by fetching the appropriate action and next state
-and action from the program, and updating the state and tape accordingly.
+from the program, and by updating the state and tape accordingly.
-This single step of execution is defined as the function @{term tstep}:
+This single step of execution is defined as the function @{term tstep}
 \begin{center}
 \begin{tabular}{l}
 @{text "step (s, (l, r)) p"} @{text "\<equiv>"}\\
 \hspace{10mm}@{text "let (a, s) = fetch p s (read r)"}\\
 \hspace{10mm}@{text "in (s', update (l, r) a)"}
 \end{tabular}
 \end{center}
 \noindent
-It is impossible in Isabelle/HOL to lift this function realising
+where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
+empty it returns @{term Bk}.
+It is impossible in Isabelle/HOL to lift the @{term step}-function realising
 a general evaluation function for Turing machines. The reason is that functions in HOL-based
 provers need to be terminating, and clearly there are Turing machine
-programs which are not. We can however define an evaluation
+programs that are not. We can however define an evaluation
 function so that it performs exactly @{text n} steps:
 \begin{center}
 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
 @{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
 \end{tabular}
 \end{center}
 \noindent
 Recall our definition of @{term fetch} with the default value for
-the 0th state. In case a Turing program takes in \cite{Boolos87} less
+the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less
-then @{text n} steps before it halts, then in our setting the evaluation
+then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
-does not halt, but rather transitions to the 0th state and remain there
+does not actually halt, but rather transitions to the @{text 0}-state and
-performing @{text Nop}-actions.
+remains there performing @{text Nop}-actions until @{text n} is reached.
 Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
-@{term p} halts generating an output tape @{text "(l\<^isub>o,r\<^isub>o)"}:
+@{term p} generates a specific  output tape @{text "(l\<^isub>o,r\<^isub>o)"}
 \begin{center}
 \begin{tabular}{l}
-@{term "halt p (l\<^isub>i,r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
+@{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
 \hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
 \end{tabular}
 \end{center}
 \noindent
-where 1 stands for the starting state and 0 for the halting state, or
+where @{text 1} stands for the starting state and @{text 0} for our final state.
-in our settin it should better be called the final state.
+A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
+\begin{center}
+@{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
+\<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
+\end{center}
+\noindent
 Later on we need to consider specific Turing machines that
 start with a tape in standard form and halt the computation
-in standard form. By this we mean
+in standard form. To define a tape in standard form, it is
+useful to have an operation @{term "tape_of_nat_list DUMMY"} that
+translates
+lists of natural numbers into tapes.
+\begin{center}
+\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
+@{thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(1)}\\
+@{thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(2)}\\
+@{thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @{thm (rhs) tape_of_nat_list_def2(3)}\\
+\end{tabular}
+\end{center}
+By this we mean
 \begin{center}
 @{thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
 \end{center}
 tape corresponding to a value @{term n} and producing
 a new tape corresponding to the value @{term l} (the number of @{term Oc}s
 clustered on the output tape).
 Before we can prove the undecidability of the halting problem for Turing machines,
-we have to define how to compose them. Given our setup, this is relatively straightforward,
+we have to define how to compose Turing machines. Given our setup, this is relatively
-if slightly fiddly.
+straightforward, if slightly fiddly.
+\begin{center}
+@{thm tshift_def2}
+\end{center}
+(* HERE *)
 shift and change of a p
 composition of two ps

changeset 34	22e5804b135c
parent 33	284468a61346
child 35	839e37b75d9a