--- a/Paper/Paper.thy Wed Jan 23 20:18:40 2013 +0100
+++ b/Paper/Paper.thy Thu Jan 24 00:20:26 2013 +0100
@@ -1,6 +1,6 @@
(*<*)
theory Paper
-imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
+imports "../thys/uncomputable"
begin
(*
@@ -22,6 +22,7 @@
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
update2 ("update") and
tm_wf0 ("wf") and
+ is_even ("iseven") and
(* abc_lm_v ("lookup") and
abc_lm_s ("set") and*)
haltP ("stdhalt") and
@@ -31,6 +32,41 @@
DUMMY ("\<^raw:\mbox{$\_$}>")
declare [[show_question_marks = false]]
+
+(* THEOREMS *)
+notation (Rule output)
+ "==>" ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms"
+ ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+ "Trueprop" ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+ "==>" ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+ "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+ ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+ "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+ "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+
+
(*>*)
section {* Introduction *}
@@ -52,13 +88,15 @@
\noindent
-Suppose you want to mechanise a proof about whether a predicate @{term P}, say, is
+Suppose you want to mechanise a proof for whether a predicate @{term P}, say, is
decidable or not. Decidability of @{text P} usually amounts to showing
whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic
where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
is always provable no matter whether @{text P} is constructed by
-computable means.
+computable means. We hit this limitation previously when we mechanised the correctness
+proofs of two algorithms \cite{UrbanCheneyBerghofer11,WuZhangUrban12},
+but were unable to formalise arguments about computability.
%The same problem would arise if we had formulated
%the algorithms as recursive functions, because internally in
@@ -183,9 +221,12 @@
We construct the universal Turing machine from \cite{Boolos87} by
relating recursive functions to abacus machines and abacus machines to
Turing machines. Since we have set up in Isabelle/HOL a very general computability
-model and undecidability result, we are able to formalise the
-undecidability of Wang's tiling problem. We are not aware of any other
-formalisation of a substantial undecidability problem.
+model and undecidability result, we are able to formalise other
+results: we describe a proof of the computational equivalence
+of single-sided Turing machines, which is not given in \cite{Boolos87},
+but needed for formalising the undecidability proof of Wang's tiling problem. {\it citation}
+%We are not aware of any other
+%formalisation of a substantial undecidability problem.
*}
section {* Turing Machines *}
@@ -311,11 +352,11 @@
%cannot be used as it does not preserve types.} This renaming can be
%quite cumbersome to reason about.
We followed the choice made in \cite{AspertiRicciotti12}
- representing a state by a natural number and the states of a Turing
- machine by the initial segment of natural numbers starting from @{text 0}.
- In doing so we can compose two Turing machine by
+ representing a state by a natural number and the states in a Turing
+ machine programme by the initial segment of natural numbers starting from @{text 0}.
+ In doing so we can compose two Turing machine programs by
shifting the states of one by an appropriate amount to a higher
- segment and adjusting some ``next states'' in the other. {\it composition here?}
+ segment and adjusting some ``next states'' in the other.
An \emph{instruction} 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
@@ -356,35 +397,26 @@
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}
+ \begin{equation}\label{fetch}
+ \mbox{\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
\multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\
@{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
@{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
- \end{tabular}
- \end{center}
+ \end{tabular}}
+ \end{equation}
\noindent
In this definition the function @{term nth_of} returns the @{text n}th element
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 @{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 @{text 0}-state.\footnote{\it However, with introducing the
- notion of \emph{well-formed} Turing machine programs we will later exclude such
- cases and make the @{text 0}-state the only ``halting state''. A program
- @{term p} is said to be well-formed if it satisfies
- the following three properties:
+ (@{term None}-case). We often need to restrict Turing machine programs
+ to be well-formed: a program @{term p} is \emph{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)"}\\
- & @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
- \end{tabular}
+ @{thm tm_wf.simps[where p="p" and off="0::nat", simplified, THEN eq_reflection]}
\end{center}
\noindent
@@ -392,7 +424,6 @@
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 @{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
@@ -425,69 +456,14 @@
\end{center}
\noindent
- Recall our definition of @{term fetch} with the default value for
+ Recall our definition of @{term fetch} (shown in \ref{fetch}) with the default value for
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 @{term steps}-evaluation
does not actually halt, but rather transitions to the @{text 0}-state and
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} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
-
- \begin{center}
- \begin{tabular}{l}
- @{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 @{text 1} stands for the starting state and @{text 0} for our 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. 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}
-
- \noindent
- This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
- and the head pointing to the first one; the Turing machine
- halts with a tape consisting of some @{term Bk}s, followed by a
- ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
- The head in the output is pointing again at the first @{term Oc}.
- The intuitive meaning of this definition is to start the Turing machine with a
- 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 two Turing machines. Given our setup, this is
+ we have to define how to compose two Turing machine programs. Given our setup, this is
relatively straightforward, if slightly fiddly. We use the following two
auxiliary functions:
@@ -501,8 +477,8 @@
\noindent
The first adds @{text n} to all states, exept the @{text 0}-state,
thus moving all ``regular'' states to the segment starting at @{text
- n}; the second adds @{term "length p div 2 + 1"} to the @{text
- 0}-state, thus ridirecting all references to the ``halting state''
+ n}; the second adds @{term "Suc(length p div 2)"} to the @{text
+ 0}-state, thus redirecting all references to the ``halting state''
to the first state after the program @{text p}. With these two
functions in place, we can define the \emph{sequential composition}
of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
@@ -512,12 +488,26 @@
\end{center}
\noindent
- This means @{text "p\<^isub>1"} is executed first. Whenever it originally
- transitioned to the @{text 0}-state, it will in the composed program transition to the starting
- state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
- have been shifted in order to make sure that the states of the composed
- program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
- an initial segment of the natural numbers.
+ %This means @{text "p\<^isub>1"} is executed first. Whenever it originally
+ %transitioned to the @{text 0}-state, it will in the composed program transition to the starting
+ %state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
+ %have been shifted in order to make sure that the states of the composed
+ %program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
+ %an initial segment of the natural numbers.
+
+ In the following we will consider the following Turing machine program
+ that makes a copies a value on the tape.
+
+ \begin{figure}
+ \begin{center}
+ \begin{tabular}{@ {}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {\hspace{4mm}}p{3.6cm}@ {}}
+ @{thm tcopy_init_def} &
+ @{thm tcopy_loop_def} &
+ @{thm tcopy_end_def}
+ \end{tabular}
+ \end{center}
+ \end{figure}
+
\begin{center}
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
@@ -620,6 +610,62 @@
lambda-terms. For this he introduced a clever rewriting technology
based on combinators and de-Bruijn indices for
rewriting modulo $\beta$-equivalence (to keep it manageable)
+
+
+
+ Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
+ @{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
+
+ \begin{center}
+ \begin{tabular}{l}
+ @{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 @{text 1} stands for the starting state and @{text 0} for our 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. 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}
+
+ \noindent
+ This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
+ and the head pointing to the first one; the Turing machine
+ halts with a tape consisting of some @{term Bk}s, followed by a
+ ``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
+ The head in the output is pointing again at the first @{term Oc}.
+ The intuitive meaning of this definition is to start the Turing machine with a
+ 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).
+
*}