6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
1 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
2 |
theory Paper
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
3 |
imports "../thys/uncomputable" "~~/src/HOL/Library/LaTeXsugar"
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
4 |
begin
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
5 |
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
6 |
(*
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
7 |
hide_const (open) s
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
8 |
*)
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
9 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
10 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
11 |
hide_const (open) Divides.adjust
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
12 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
13 |
abbreviation
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
14 |
"update2 p a \<equiv> update a p"
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
15 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
16 |
consts DUMMY::'a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
17 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
18 |
notation (latex output)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
19 |
Cons ("_::_" [78,77] 73) and
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
20 |
set ("") and
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
21 |
W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
22 |
W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
23 |
update2 ("update") and
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
24 |
tm_wf0 ("wf") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
25 |
(* abc_lm_v ("lookup") and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
26 |
abc_lm_s ("set") and*)
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
27 |
haltP ("stdhalt") and
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
28 |
tcopy ("copy") and
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
29 |
tape_of_nat_list ("\<ulcorner>_\<urcorner>") and
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
30 |
tm_comp ("_ \<oplus> _") and
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
31 |
DUMMY ("\<^raw:\mbox{$\_$}>")
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
32 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
33 |
declare [[show_question_marks = false]]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
34 |
(*>*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
35 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
36 |
section {* Introduction *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
37 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
38 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
39 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
40 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
41 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
42 |
%\noindent
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
43 |
%We formalised in earlier work the correctness proofs for two
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
44 |
%algorithms in Isabelle/HOL---one about type-checking in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
45 |
%LF~\cite{UrbanCheneyBerghofer11} and another about deciding requests
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
46 |
%in access control~\cite{WuZhangUrban12}. The formalisations
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
47 |
%uncovered a gap in the informal correctness proof of the former and
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
48 |
%made us realise that important details were left out in the informal
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
49 |
%model for the latter. However, in both cases we were unable to
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
50 |
%formalise in Isabelle/HOL computability arguments about the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
51 |
%algorithms.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
52 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
53 |
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
54 |
\noindent
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
55 |
Suppose you want to mechanise a proof about whether a predicate @{term P}, say, is
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
56 |
decidable or not. Decidability of @{text P} usually amounts to showing
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
57 |
whether \mbox{@{term "P \<or> \<not>P"}} holds. But this does \emph{not} work
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
58 |
in Isabelle/HOL and other HOL theorem provers, since they are based on classical logic
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
59 |
where the law of excluded middle ensures that \mbox{@{term "P \<or> \<not>P"}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
60 |
is always provable no matter whether @{text P} is constructed by
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
61 |
computable means.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
62 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
63 |
%The same problem would arise if we had formulated
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
64 |
%the algorithms as recursive functions, because internally in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
65 |
%Isabelle/HOL, like in all HOL-based theorem provers, functions are
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
66 |
%represented as inductively defined predicates too.
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
67 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
68 |
The only satisfying way out of this problem in a theorem prover based
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
69 |
on classical logic is to formalise a theory of computability. Norrish
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
70 |
provided such a formalisation for the HOL. He choose
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
71 |
the $\lambda$-calculus as the starting point for his formalisation of
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
72 |
computability theory, because of its ``simplicity'' \cite[Page
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
73 |
297]{Norrish11}. Part of his formalisation is a clever infrastructure
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
74 |
for reducing $\lambda$-terms. He also established the computational
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
75 |
equivalence between the $\lambda$-calculus and recursive functions.
|
52
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
76 |
Nevertheless he concluded that it would be appealing
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
77 |
to have formalisations for more operational models of
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
78 |
computations, such as Turing machines or register machines. One
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
79 |
reason is that many proofs in the literature use them. He noted
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
80 |
however that \cite[Page 310]{Norrish11}:
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
81 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
82 |
\begin{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
83 |
\it``If register machines are unappealing because of their
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
84 |
general fiddliness,\\ Turing machines are an even more
|
8
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
85 |
daunting prospect.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
86 |
\end{quote}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
87 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
88 |
\noindent
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
89 |
In this paper we take on this daunting prospect and provide a
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
90 |
formalisation of Turing machines, as well as abacus machines (a kind
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
91 |
of register machines) and recursive functions. To see the difficulties
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
92 |
involved with this work, one has to understand that Turing machine
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
93 |
programs can be completely \emph{unstructured}, behaving
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
94 |
similar to Basic programs involving the infamous goto \cite{Dijkstra68}. This precludes in the
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
95 |
general case a compositional Hoare-style reasoning about Turing
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
96 |
programs. We provide such Hoare-rules for when it \emph{is} possible to
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
97 |
reason in a compositional manner (which is fortunately quite often), but also tackle
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
98 |
the more complicated case when we translate abacus programs into
|
61
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
99 |
Turing programs. These difficulties when reasoning about computability theory
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
100 |
are usually completely left out in the informal literature, e.g.~\cite{Boolos87}.
|
12
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
101 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
102 |
%To see the difficulties
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
103 |
%involved with this work, one has to understand that interactive
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
104 |
%theorem provers, like Isabelle/HOL, are at their best when the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
105 |
%data-structures at hand are ``structurally'' defined, like lists,
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
106 |
%natural numbers, regular expressions, etc. Such data-structures come
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
107 |
%with convenient reasoning infrastructures (for example induction
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
108 |
%principles, recursion combinators and so on). But this is \emph{not}
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
109 |
%the case with Turing machines (and also not with register machines):
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
110 |
%underlying their definitions are sets of states together with
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
111 |
%transition functions, all of which are not structurally defined. This
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
112 |
%means we have to implement our own reasoning infrastructure in order
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
113 |
%to prove properties about them. This leads to annoyingly fiddly
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
114 |
%formalisations. We noticed first the difference between both,
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
115 |
%structural and non-structural, ``worlds'' when formalising the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
116 |
%Myhill-Nerode theorem, where regular expressions fared much better
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
117 |
%than automata \cite{WuZhangUrban11}. However, with Turing machines
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
118 |
%there seems to be no alternative if one wants to formalise the great
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
119 |
%many proofs from the literature that use them. We will analyse one
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
120 |
%example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
121 |
%standard proof of this property uses the notion of universal
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
122 |
%Turing machines.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
123 |
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
124 |
We are not the first who formalised Turing machines: we are aware
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
125 |
of the preliminary work by Asperti and Ricciotti
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
126 |
\cite{AspertiRicciotti12}. They describe a complete formalisation of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
127 |
Turing machines in the Matita theorem prover, including a universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
128 |
Turing machine. They report that the informal proofs from which they
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
129 |
started are \emph{not} ``sufficiently accurate to be directly usable as a
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
130 |
guideline for formalization'' \cite[Page 2]{AspertiRicciotti12}. For
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
131 |
our formalisation we followed mainly the proofs from the textbook
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
132 |
\cite{Boolos87} and found that the description there is quite
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
133 |
detailed. Some details are left out however: for example, it is only
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
134 |
shown how the universal Turing machine is constructed for Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
135 |
machines computing unary functions. We had to figure out a way to
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
136 |
generalise this result to $n$-ary functions. Similarly, when compiling
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
137 |
recursive functions to abacus machines, the textbook again only shows
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
138 |
how it can be done for 2- and 3-ary functions, but in the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
139 |
formalisation we need arbitrary functions. But the general ideas for
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
140 |
how to do this are clear enough in \cite{Boolos87}.
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
141 |
%However, one
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
142 |
%aspect that is completely left out from the informal description in
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
143 |
%\cite{Boolos87}, and similar ones we are aware of, is arguments why certain Turing
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
144 |
%machines are correct. We will introduce Hoare-style proof rules
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
145 |
%which help us with such correctness arguments of Turing machines.
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
146 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
147 |
The main difference between our formalisation and the one by Asperti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
148 |
and Ricciotti is that their universal Turing machine uses a different
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
149 |
alphabet than the machines it simulates. They write \cite[Page
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
150 |
23]{AspertiRicciotti12}:
|
10
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
151 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
152 |
\begin{quote}\it
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
153 |
``In particular, the fact that the universal machine operates with a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
154 |
different alphabet with respect to the machines it simulates is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
155 |
annoying.''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
156 |
\end{quote}
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
157 |
|
15
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
158 |
\noindent
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
159 |
In this paper we follow the approach by Boolos et al \cite{Boolos87},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
160 |
which goes back to Post \cite{Post36}, where all Turing machines
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
161 |
operate on tapes that contain only \emph{blank} or \emph{occupied} cells.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
162 |
Traditionally the content of a cell can be any
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
163 |
character from a finite alphabet. Although computationally equivalent,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
164 |
the more restrictive notion of Turing machines in \cite{Boolos87} makes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
165 |
the reasoning more uniform. In addition some proofs \emph{about} Turing
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
166 |
machines are simpler. The reason is that one often needs to encode
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
167 |
Turing machines---consequently if the Turing machines are simpler, then the coding
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
168 |
functions are simpler too. Unfortunately, the restrictiveness also makes
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
169 |
it harder to design programs for these Turing machines. In order
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
170 |
to construct a universal Turing machine we therefore do not follow
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
171 |
\cite{AspertiRicciotti12}, instead follow the proof in
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
172 |
\cite{Boolos87} by relating abacus machines to Turing machines and in
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
173 |
turn recursive functions to abacus machines. The universal Turing
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
174 |
machine can then be constructed as a recursive function.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
175 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
176 |
\smallskip
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
177 |
\noindent
|
38
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
178 |
{\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
179 |
description of Boolos et al \cite{Boolos87} where tapes only have blank or
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
180 |
occupied cells. We mechanise the undecidability of the halting problem and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
181 |
prove the correctness of concrete Turing machines that are needed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
182 |
in this proof; such correctness proofs are left out in the informal literature.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
183 |
We construct the universal Turing machine from \cite{Boolos87} by
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
184 |
relating recursive functions to abacus machines and abacus machines to
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
185 |
Turing machines. Since we have set up in Isabelle/HOL a very general computability
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
186 |
model and undecidability result, we are able to formalise the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
187 |
undecidability of Wang's tiling problem. We are not aware of any other
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
188 |
formalisation of a substantial undecidability problem.
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
189 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
190 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
191 |
section {* Turing Machines *}
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
192 |
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
193 |
text {* \noindent
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
194 |
Turing machines can be thought of as having a \emph{head},
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
195 |
``gliding'' over a potentially infinite tape. Boolos et
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
196 |
al~\cite{Boolos87} only consider tapes with cells being either blank
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
197 |
or occupied, which we represent by a datatype having two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
198 |
constructors, namely @{text Bk} and @{text Oc}. One way to
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
199 |
represent such tapes is to use a pair of lists, written @{term "(l,
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
200 |
r)"}, where @{term l} stands for the tape on the left-hand side of the
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
201 |
head and @{term r} for the tape on the right-hand side. We have the
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
202 |
convention that the head, abbreviated @{term hd}, of the right-list is
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
203 |
the cell on which the head of the Turing machine currently operates. This can
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
204 |
be pictured as follows:
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
205 |
%
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
206 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
207 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
208 |
\draw[very thick] (-3.0,0) -- ( 3.0,0);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
209 |
\draw[very thick] (-3.0,0.5) -- ( 3.0,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
210 |
\draw[very thick] (-0.25,0) -- (-0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
211 |
\draw[very thick] ( 0.25,0) -- ( 0.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
212 |
\draw[very thick] (-0.75,0) -- (-0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
213 |
\draw[very thick] ( 0.75,0) -- ( 0.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
214 |
\draw[very thick] (-1.25,0) -- (-1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
215 |
\draw[very thick] ( 1.25,0) -- ( 1.25,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
216 |
\draw[very thick] (-1.75,0) -- (-1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
217 |
\draw[very thick] ( 1.75,0) -- ( 1.75,0.5);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
218 |
\draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
219 |
\draw[fill] (1.35,0.1) rectangle (1.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
220 |
\draw[fill] (0.85,0.1) rectangle (1.15,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
221 |
\draw[fill] (-0.35,0.1) rectangle (-0.65,0.4);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
222 |
\draw (-0.25,0.8) -- (-0.25,-0.8);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
223 |
\draw[<->] (-1.25,-0.7) -- (0.75,-0.7);
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
224 |
\node [anchor=base] at (-0.8,-0.5) {\small left list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
225 |
\node [anchor=base] at (0.35,-0.5) {\small right list};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
226 |
\node [anchor=base] at (0.1,0.7) {\small head};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
227 |
\node [anchor=base] at (-2.2,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
228 |
\node [anchor=base] at ( 2.3,0.2) {\ldots};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
229 |
\end{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
230 |
\end{center}
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
231 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
232 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
233 |
Note that by using lists each side of the tape is only finite. The
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
234 |
potential infinity is achieved by adding an appropriate blank or occupied cell
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
235 |
whenever the head goes over the ``edge'' of the tape. To
|
52
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
236 |
make this formal we define five possible \emph{actions}, @{text a}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
237 |
the Turing machine can perform:
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
238 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
239 |
\begin{center}
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
240 |
\begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
241 |
@{text "a"} & $::=$ & @{term "W0"} & (write blank, @{term Bk})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
242 |
& $\mid$ & @{term "W1"} & (write occupied, @{term Oc})\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
243 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
244 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
245 |
& $\mid$ & @{term L} & (move left)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
246 |
& $\mid$ & @{term R} & (move right)\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
247 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
248 |
\begin{tabular}[t]{rcl@ {\hspace{2mm}}l@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
249 |
& $\mid$ & @{term Nop} & (do-nothing operation)\\
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
250 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
251 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
252 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
253 |
\noindent
|
20
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
254 |
We slightly deviate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
255 |
from the presentation in \cite{Boolos87} by using the @{term Nop} operation; however its use
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
256 |
will become important when we formalise halting computations and also universal Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
257 |
machines. Given a tape and an action, we can define the
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
258 |
following tape updating function:
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
259 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
260 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
261 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
262 |
@{thm (lhs) update.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
263 |
@{thm (lhs) update.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(2)}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
264 |
@{thm (lhs) update.simps(3)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(3)}\\
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
265 |
@{thm (lhs) update.simps(4)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(4)}\\
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
266 |
@{thm (lhs) update.simps(5)} & @{text "\<equiv>"} & @{thm (rhs) update.simps(5)}\\
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
267 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
268 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
269 |
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
270 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
271 |
The first two clauses replace the head of the right-list
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
272 |
with a new @{term Bk} or @{term Oc}, respectively. To see that
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
273 |
these two clauses make sense in case where @{text r} is the empty
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
274 |
list, one has to know that the tail function, @{term tl}, is defined
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
275 |
such that @{term "tl [] == []"} holds. The third clause
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
276 |
implements the move of the head one step to the left: we need
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
277 |
to test if the left-list @{term l} is empty; if yes, then we just prepend a
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
278 |
blank cell to the right-list; otherwise we have to remove the
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
279 |
head from the left-list and prepend it to the right-list. Similarly
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
280 |
in the fourth clause for a right move action. The @{term Nop} operation
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
281 |
leaves the the tape unchanged.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
282 |
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
283 |
%Note that our treatment of the tape is rather ``unsymmetric''---we
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
284 |
%have the convention that the head of the right-list is where the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
285 |
%head is currently positioned. Asperti and Ricciotti
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
286 |
%\cite{AspertiRicciotti12} also considered such a representation, but
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
287 |
%dismiss it as it complicates their definition for \emph{tape
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
288 |
%equality}. The reason is that moving the head one step to
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
289 |
%the left and then back to the right might change the tape (in case
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
290 |
%of going over the ``edge''). Therefore they distinguish four types
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
291 |
%of tapes: one where the tape is empty; another where the head
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
292 |
%is on the left edge, respectively right edge, and in the middle
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
293 |
%of the tape. The reading, writing and moving of the tape is then
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
294 |
%defined in terms of these four cases. In this way they can keep the
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
295 |
%tape in a ``normalised'' form, and thus making a left-move followed
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
296 |
%by a right-move being the identity on tapes. Since we are not using
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
297 |
%the notion of tape equality, we can get away with the unsymmetric
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
298 |
%definition above, and by using the @{term update} function
|
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
299 |
%cover uniformly all cases including corner cases.
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
300 |
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
301 |
Next we need to define the \emph{states} of a Turing machine.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
302 |
%Given
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
303 |
%how little is usually said about how to represent them in informal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
304 |
%presentations, it might be surprising that in a theorem prover we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
305 |
%have to select carefully a representation. If we use the naive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
306 |
%representation where a Turing machine consists of a finite set of
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
307 |
%states, then we will have difficulties composing two Turing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
308 |
%machines: we would need to combine two finite sets of states,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
309 |
%possibly renaming states apart whenever both machines share
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
310 |
%states.\footnote{The usual disjoint union operation in Isabelle/HOL
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
311 |
%cannot be used as it does not preserve types.} This renaming can be
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
312 |
%quite cumbersome to reason about.
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
313 |
We followed the choice made in \cite{AspertiRicciotti12}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
314 |
representing a state by a natural number and the states of a Turing
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
315 |
machine by the initial segment of natural numbers starting from @{text 0}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
316 |
In doing so we can compose two Turing machine by
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
317 |
shifting the states of one by an appropriate amount to a higher
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
318 |
segment and adjusting some ``next states'' in the other. {\it composition here?}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
319 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
320 |
An \emph{instruction} of a Turing machine is a pair consisting of
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
321 |
an action and a natural number (the next state). A \emph{program} @{term p} of a Turing
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
322 |
machine is then a list of such pairs. Using as an example the following Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
323 |
program, which consists of four instructions
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
324 |
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
325 |
\begin{equation}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
326 |
\begin{tikzpicture}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
327 |
\node [anchor=base] at (0,0) {@{thm dither_def}};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
328 |
\node [anchor=west] at (-1.5,-0.42) {$\underbrace{\hspace{21mm}}_{\text{1st state}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
329 |
\node [anchor=west] at ( 1.1,-0.42) {$\underbrace{\hspace{17mm}}_{\text{2nd state}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
330 |
\node [anchor=west] at (-1.5,0.65) {$\overbrace{\hspace{10mm}}^{\text{@{term Bk}-case}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
331 |
\node [anchor=west] at (-0.1,0.65) {$\overbrace{\hspace{6mm}}^{\text{@{term Oc}-case}}$};
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
332 |
\end{tikzpicture}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
333 |
\label{dither}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
334 |
\end{equation}
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
335 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
336 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
337 |
the reader can see we have organised our Turing machine programs so
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
338 |
that segments of two belong to a state. The first component of the
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
339 |
segment determines what action should be taken and which next state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
340 |
should be transitioned to in case the head reads a @{term Bk};
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
341 |
similarly the second component determines what should be done in
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
342 |
case of reading @{term Oc}. We have the convention that the first
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
343 |
state is always the \emph{starting state} of the Turing machine.
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
344 |
The @{text 0}-state is special in that it will be used as the
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
345 |
``halting state''. There are no instructions for the @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
346 |
0}-state, but it will always perform a @{term Nop}-operation and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
347 |
remain in the @{text 0}-state. Unlike Asperti and Riccioti
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
348 |
\cite{AspertiRicciotti12}, we have chosen a very concrete
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
349 |
representation for programs, because when constructing a universal
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
350 |
Turing machine, we need to define a coding function for programs.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
351 |
This can be easily done for our programs-as-lists, but is more
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
352 |
difficult for the functions used by Asperti and Ricciotti.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
353 |
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
354 |
Given a program @{term p}, a state
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
355 |
and the cell being read by the head, we need to fetch
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
356 |
the corresponding instruction from the program. For this we define
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
357 |
the function @{term fetch}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
358 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
359 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
360 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
361 |
\multicolumn{3}{l}{@{thm fetch.simps(1)[where b=DUMMY]}}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
362 |
@{thm (lhs) fetch.simps(2)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s) of"}\\
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
363 |
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}\\
|
49
b388dceee892
shortening a bit the paper and updating various things
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
364 |
@{thm (lhs) fetch.simps(3)} & @{text "\<equiv>"} & @{text "case nth_of p (2 * s + 1) of"}\\
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
365 |
\multicolumn{3}{@ {\hspace{4cm}}l}{@{text "None \<Rightarrow> (Nop, 0) | Some i \<Rightarrow> i"}}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
366 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
367 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
368 |
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
369 |
\noindent
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
370 |
In this definition the function @{term nth_of} returns the @{text n}th element
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
371 |
from a list, provided it exists (@{term Some}-case), or if it does not, it
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
372 |
returns the default action @{term Nop} and the default state @{text 0}
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
373 |
(@{term None}-case). In doing so we slightly deviate from the description
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
374 |
in \cite{Boolos87}: if their Turing machines transition to a non-existing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
375 |
state, then the computation is halted. We will transition in such cases
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
376 |
to the @{text 0}-state.\footnote{\it However, with introducing the
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
377 |
notion of \emph{well-formed} Turing machine programs we will later exclude such
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
378 |
cases and make the @{text 0}-state the only ``halting state''. A program
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
379 |
@{term p} is said to be well-formed if it satisfies
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
380 |
the following three properties:
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
381 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
382 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
383 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
384 |
@{term "t_correct p"} & @{text "\<equiv>"} & @{term "2 <= length p"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
385 |
& @{text "\<and>"} & @{term "iseven (length p)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
386 |
& @{text "\<and>"} & @{term "\<forall> (a, s) \<in> set p. s <= length p div 2"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
387 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
388 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
389 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
390 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
391 |
The first says that @{text p} must have at least an instruction for the starting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
392 |
state; the second that @{text p} has a @{term Bk} and @{term Oc} instruction for every
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
393 |
state, and the third that every next-state is one of the states mentioned in
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
394 |
the program or being the @{text 0}-state.
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
395 |
}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
396 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
397 |
A \emph{configuration} @{term c} of a Turing machine is a state together with
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
398 |
a tape. This is written as @{text "(s, (l, r))"}. If we have a
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
399 |
configuration and a program, we can calculate
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
400 |
what the next configuration is by fetching the appropriate action and next state
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
401 |
from the program, and by updating the state and tape accordingly.
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
402 |
This single step of execution is defined as the function @{term step}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
403 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
404 |
\begin{center}
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
405 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
406 |
@{text "step (s, (l, r)) p"} & @{text "\<equiv>"} & @{text "let (a, s') = fetch p s (read r)"}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
407 |
& & @{text "in (s', update (l, r) a)"}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
408 |
\end{tabular}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
409 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
410 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
411 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
412 |
where @{term "read r"} returns the head of the list @{text r}, or if @{text r} is
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
413 |
empty it returns @{term Bk}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
414 |
It is impossible in Isabelle/HOL to lift the @{term step}-function realising
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
415 |
a general evaluation function for Turing machines. The reason is that functions in HOL-based
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
416 |
provers need to be terminating, and clearly there are Turing machine
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
417 |
programs that are not. We can however define an evaluation
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
418 |
function so that it performs exactly @{text n} steps:
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
419 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
420 |
\begin{center}
|
30
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
421 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
422 |
@{thm (lhs) steps.simps(1)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
423 |
@{thm (lhs) steps.simps(2)} & @{text "\<equiv>"} & @{thm (rhs) steps.simps(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
424 |
\end{tabular}
|
22
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
425 |
\end{center}
|
18
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
426 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
427 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
428 |
Recall our definition of @{term fetch} with the default value for
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
429 |
the @{text 0}-state. In case a Turing program takes in \cite{Boolos87} less
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
430 |
then @{text n} steps before it halts, then in our setting the @{term steps}-evaluation
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
431 |
does not actually halt, but rather transitions to the @{text 0}-state and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
432 |
remains there performing @{text Nop}-actions until @{text n} is reached.
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
433 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
434 |
Given some input tape @{text "(l\<^isub>i,r\<^isub>i)"}, we can define when a program
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
435 |
@{term p} generates a specific output tape @{text "(l\<^isub>o,r\<^isub>o)"}
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
436 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
437 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
438 |
\begin{tabular}{l}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
439 |
@{term "runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"} @{text "\<equiv>"}\\
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
440 |
\hspace{6mm}@{text "\<exists>n. nsteps (1, (l\<^isub>i,r\<^isub>i)) p n = (0, (l\<^isub>o,r\<^isub>o))"}
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
441 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
442 |
\end{center}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
443 |
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
444 |
\noindent
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
445 |
where @{text 1} stands for the starting state and @{text 0} for our final state.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
446 |
A program @{text p} with input tape @{term "(l\<^isub>i, r\<^isub>i)"} \emph{halts} iff
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
447 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
448 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
449 |
@{term "halts p (l\<^isub>i, r\<^isub>i) \<equiv>
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
450 |
\<exists>l\<^isub>o r\<^isub>o. runs p (l\<^isub>i, r\<^isub>i) (l\<^isub>o,r\<^isub>o)"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
451 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
452 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
453 |
\noindent
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
454 |
Later on we need to consider specific Turing machines that
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
455 |
start with a tape in standard form and halt the computation
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
456 |
in standard form. To define a tape in standard form, it is
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
457 |
useful to have an operation %@{ term "tape_of_nat_list DUMMY"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
458 |
that translates lists of natural numbers into tapes.
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
459 |
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
460 |
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
461 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
462 |
\begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
463 |
%@ { thm (lhs) tape_of_nat_list_def2(1)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(1)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
464 |
%@ { thm (lhs) tape_of_nat_list_def2(2)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(2)}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
465 |
%@ { thm (lhs) tape_of_nat_list_def2(3)} & @{text "\<equiv>"} & @ { thm (rhs) tape_of_nat_list_def2(3)}\\
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
466 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
467 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
468 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
469 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
470 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
471 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
472 |
By this we mean
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
473 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
474 |
\begin{center}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
475 |
%@ {thm haltP_def2[where p="p" and n="n", THEN eq_reflection]}
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
476 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
477 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
478 |
\noindent
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
479 |
This means the Turing machine starts with a tape containg @{text n} @{term Oc}s
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
480 |
and the head pointing to the first one; the Turing machine
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
481 |
halts with a tape consisting of some @{term Bk}s, followed by a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
482 |
``cluster'' of @{term Oc}s and after that by some @{term Bk}s.
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
483 |
The head in the output is pointing again at the first @{term Oc}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
484 |
The intuitive meaning of this definition is to start the Turing machine with a
|
32
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
485 |
tape corresponding to a value @{term n} and producing
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
486 |
a new tape corresponding to the value @{term l} (the number of @{term Oc}s
|
33
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
487 |
clustered on the output tape).
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
488 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
489 |
Before we can prove the undecidability of the halting problem for Turing machines,
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
490 |
we have to define how to compose two Turing machines. Given our setup, this is
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
491 |
relatively straightforward, if slightly fiddly. We use the following two
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
492 |
auxiliary functions:
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
493 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
494 |
\begin{center}
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
495 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}l@ {}}
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
496 |
@{thm (lhs) shift.simps} @{text "\<equiv>"} @{thm (rhs) shift.simps}\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
497 |
@{thm (lhs) adjust.simps} @{text "\<equiv>"} @{thm (rhs) adjust.simps}\\
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
498 |
\end{tabular}
|
34
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
499 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
500 |
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
501 |
\noindent
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
502 |
The first adds @{text n} to all states, exept the @{text 0}-state,
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
503 |
thus moving all ``regular'' states to the segment starting at @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
504 |
n}; the second adds @{term "length p div 2 + 1"} to the @{text
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
505 |
0}-state, thus ridirecting all references to the ``halting state''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
506 |
to the first state after the program @{text p}. With these two
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
507 |
functions in place, we can define the \emph{sequential composition}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
508 |
of two Turing machine programs @{text "p\<^isub>1"} and @{text "p\<^isub>2"}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
509 |
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
510 |
\begin{center}
|
50
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
511 |
@{thm tm_comp.simps[where ?p1.0="p\<^isub>1" and ?p2.0="p\<^isub>2", THEN eq_reflection]}
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
512 |
\end{center}
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
513 |
|
37
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
514 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
515 |
This means @{text "p\<^isub>1"} is executed first. Whenever it originally
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
516 |
transitioned to the @{text 0}-state, it will in the composed program transition to the starting
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
517 |
state of @{text "p\<^isub>2"} instead. All the states of @{text "p\<^isub>2"}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
518 |
have been shifted in order to make sure that the states of the composed
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
519 |
program @{text "p\<^isub>1 \<oplus> p\<^isub>2"} still only ``occupy''
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
520 |
an initial segment of the natural numbers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
521 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
522 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
523 |
\begin{tabular}{@ {}l@ {\hspace{1mm}}c@ {\hspace{1mm}}p{6.9cm}@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
524 |
@{thm (lhs) tcopy_def} & @{text "\<equiv>"} & @{thm (rhs) tcopy_def}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
525 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
526 |
\end{center}
|
36
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
527 |
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
528 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
529 |
assertion holds for all tapes
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
530 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
531 |
Hoare rule for composition
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
532 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
533 |
For showing the undecidability of the halting problem, we need to consider
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
534 |
two specific Turing machines. copying TM and dithering TM
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
535 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
536 |
correctness of the copying TM
|
19
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
537 |
|
24
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
538 |
measure for the copying TM, which we however omit.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
539 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
540 |
halting problem
|
9
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
541 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
542 |
|
63
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
543 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
544 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
545 |
\begin{tabular}{@ {}p{3cm}p{3cm}@ {}}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
546 |
@{thm[mode=Rule]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
547 |
Hoare_plus_halt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?Q2.0="Q\<^isub>2" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
548 |
&
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
549 |
@{thm[mode=Rule]
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
550 |
Hoare_plus_unhalt[where ?P1.0="P\<^isub>1" and ?P2.0="P\<^isub>2" and ?Q1.0="Q\<^isub>1" and ?A="p\<^isub>1" and B="p\<^isub>2"]}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
551 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
552 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
553 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
554 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
555 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
556 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
557 |
section {* Abacus Machines *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
558 |
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
559 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
560 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
561 |
Boolos et al \cite{Boolos87} use abacus machines as a
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
562 |
stepping stone for making it less laborious to write
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
563 |
programs for Turing machines. Abacus machines operate
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
564 |
over an unlimited number of registers $R_0$, $R_1$, \ldots
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
565 |
each being able to hold an arbitrary large natural number.
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
566 |
We use natural numbers to refer to registers, but also
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
567 |
to refer to \emph{opcodes} of abacus
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
568 |
machines. Obcodes are given by the datatype
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
569 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
570 |
\begin{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
571 |
\begin{tabular}{rcll}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
572 |
@{text "o"} & $::=$ & @{term "Inc R\<iota>"} & increment register $R$ by one\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
573 |
& $\mid$ & @{term "Dec R\<iota> o\<iota>"} & if content of $R$ is non-zero,\\
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
574 |
& & & then decrement it by one\\
|
26
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
575 |
& & & otherwise jump to opcode $o$\\
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
576 |
& $\mid$ & @{term "Goto o\<iota>"} & jump to opcode $o$
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
577 |
\end{tabular}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
578 |
\end{center}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
579 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
580 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
581 |
A \emph{program} of an abacus machine is a list of such
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
582 |
obcodes. For example the program clearing the register
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
583 |
$R$ (setting it to 0) can be defined as follows:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
584 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
585 |
\begin{center}
|
48
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
586 |
%@ {thm clear.simps[where n="R\<iota>" and e="o\<iota>", THEN eq_reflection]}
|
27
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
587 |
\end{center}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
588 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
589 |
\noindent
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
590 |
The second opcode @{term "Goto 0"} in this programm means we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
591 |
jump back to the first opcode, namely @{text "Dec R o"}.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
592 |
The \emph{memory} $m$ of an abacus machine holding the values
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
593 |
of the registers is represented as a list of natural numbers.
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
594 |
We have a lookup function for this memory, written @{term "abc_lm_v m R\<iota>"},
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
595 |
which looks up the content of register $R$; if $R$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
596 |
is not in this list, then we return 0. Similarly we
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
597 |
have a setting function, written @{term "abc_lm_s m R\<iota> n"}, which
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
598 |
sets the value of $R$ to $n$, and if $R$ was not yet in $m$
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
599 |
it pads it approriately with 0s.
|
29
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
600 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
601 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
602 |
Abacus machine halts when it jumps out of range.
|
25
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
603 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
604 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
605 |
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
606 |
section {* Recursive Functions *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
607 |
|
13
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
608 |
section {* Wang Tiles\label{Wang} *}
|
7
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
609 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
610 |
text {*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
611 |
Used in texture mapings - graphics
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
612 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
613 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
614 |
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
615 |
section {* Related Work *}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
616 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
617 |
text {*
|
17
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
618 |
The most closely related work is by Norrish \cite{Norrish11}, and Asperti and
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
diff
changeset
|
619 |
Ricciotti \cite{AspertiRicciotti12}. Norrish bases his approach on
|
6
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
620 |
lambda-terms. For this he introduced a clever rewriting technology
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
621 |
based on combinators and de-Bruijn indices for
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
622 |
rewriting modulo $\beta$-equivalence (to keep it manageable)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
623 |
*}
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
624 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
625 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
626 |
(*
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
627 |
Questions:
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
628 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
629 |
Can this be done: Ackerman function is not primitive
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
630 |
recursive (Nora Szasz)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
631 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
632 |
Tape is represented as two lists (finite - usually infinite tape)?
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
633 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
634 |
*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
635 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
636 |
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
637 |
(*<*)
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
638 |
end
|
Christian Urban <christian dot urban at kcl dot ac dot uk>
parents:
diff
changeset
|
639 |
(*>*) |