1 (*<*) |
1 (*<*) |
2 theory Paper |
2 theory Paper |
3 imports UTM |
3 imports UTM |
4 begin |
4 begin |
|
5 |
|
6 hide_const (open) s |
|
7 |
|
8 abbreviation |
|
9 "update p a == new_tape a p" |
|
10 |
|
11 |
|
12 lemma fetch_def2: |
|
13 shows "fetch p 0 b = (Nop, 0)" |
|
14 and "fetch p (Suc s) Bk = |
|
15 (case nth_of p (2 * s) of |
|
16 Some i \<Rightarrow> i |
|
17 | None \<Rightarrow> (Nop, 0))" |
|
18 and "fetch p (Suc s) Oc = |
|
19 (case nth_of p ((2 * s) + 1) of |
|
20 Some i \<Rightarrow> i |
|
21 | None \<Rightarrow> (Nop, 0))" |
|
22 by (auto split: block.splits simp add: fetch.simps) |
|
23 |
|
24 lemma new_tape_def2: |
|
25 shows "new_tape W0 (l, r) == (l, Bk#(tl r))" |
|
26 and "new_tape W1 (l, r) == (l, Oc#(tl r))" |
|
27 and "new_tape L (l, r) == |
|
28 (if l = [] then ([], Bk#r) else (tl l, (hd l) # r))" |
|
29 and "new_tape R (l, r) == |
|
30 (if r = [] then (Bk#l,[]) else ((hd r)#l, tl r))" |
|
31 and "new_tape Nop (l, r) == (l, r)" |
|
32 apply - |
|
33 apply(rule_tac [!] eq_reflection) |
|
34 apply(auto split: taction.splits simp add: new_tape.simps) |
|
35 done |
|
36 |
|
37 lemma tstep_def2: |
|
38 shows "tstep (s, l, []) p = (let (ac, ns) = fetch p s Bk in (ns, new_tape ac (l, [])))" |
|
39 and "tstep (s, l, x#xs) p = (let (ac, ns) = fetch p s x in (ns, new_tape ac (l, x#xs)))" |
|
40 by (auto split: prod.split list.split simp add: tstep.simps) |
|
41 |
|
42 consts DUMMY::'a |
|
43 |
|
44 notation (latex output) |
|
45 Cons ("_::_" [78,77] 73) and |
|
46 W0 ("W\<^bsub>\<^raw:\hspace{-2pt}>Bk\<^esub>") and |
|
47 W1 ("W\<^bsub>\<^raw:\hspace{-2pt}>Oc\<^esub>") and |
|
48 DUMMY ("\<^raw:\mbox{$\_$}>") |
5 |
49 |
6 declare [[show_question_marks = false]] |
50 declare [[show_question_marks = false]] |
7 (*>*) |
51 (*>*) |
8 |
52 |
9 section {* Introduction *} |
53 section {* Introduction *} |
111 \end{quote} |
155 \end{quote} |
112 |
156 |
113 \noindent |
157 \noindent |
114 In this paper we follow the approach by Boolos et al \cite{Boolos87}, |
158 In this paper we follow the approach by Boolos et al \cite{Boolos87}, |
115 which goes back to Post \cite{Post36}, where all Turing machines |
159 which goes back to Post \cite{Post36}, where all Turing machines |
116 operate on tapes that contain only blank or filled cells (represented |
160 operate on tapes that contain only \emph{blank} or \emph{filled} cells |
117 by @{term Bk} and @{term Oc}, respectively, in our |
161 (represented by @{term Bk} and @{term Oc}, respectively, in our |
118 formalisation). Traditionally the content of a cell can be any |
162 formalisation). Traditionally the content of a cell can be any |
119 character from a finite alphabet. Although computationally |
163 character from a finite alphabet. Although computationally equivalent, |
120 equivalennt, the more restrictive notion of Turing machines make |
164 the more restrictive notion of Turing machines in \cite{Boolos87} makes |
121 the reasoning more uniform. Unfortunately, it also makes it |
165 the reasoning more uniform. In addition some proofs \emph{about} Turing |
122 harder to design programs for Turing machines. Therefore |
166 machines will be simpler. The reason is that one often need to encode |
123 in order to construct a \emph{universal Turing machine} we follow |
167 Turing machines---if the Turing machines are simpler, then the coding |
124 the proof in \cite{Boolos87} by relating abacus machines to |
168 functions are simpler. Unfortunately, the restrictiveness also makes |
125 turing machines and in turn recursive functions to abacus machines. |
169 it harder to design programs for these Turing machines. Therefore in order |
126 |
170 to construct a \emph{universal Turing machine} we follow the proof in |
127 \medskip |
171 \cite{Boolos87} by relating abacus machines to Turing machines and in |
|
172 turn recursive functions to abacus machines. The universal Turing |
|
173 machine can then be constructed as recursive function. |
|
174 |
|
175 \smallskip |
128 \noindent |
176 \noindent |
129 {\bf Contributions:} |
177 {\bf Contributions:} |
130 |
178 |
131 *} |
179 *} |
132 |
180 |
133 section {* Turing Machines *} |
181 section {* Turing Machines *} |
134 |
182 |
135 text {* |
183 text {* |
136 |
184 \noindent |
137 Tapes |
185 Turing machines can be thought of as having read-write-unit |
138 |
186 ``gliding'' over a potentially infinite tape. Boolos et |
139 %\begin{center} |
187 al~\cite{Boolos87} only consider tapes with cells being either blank |
140 %\begin{tikzpicture} |
188 or occupied, which we represent with a datatype having two |
141 %% |
189 constructors, namely @{text Bk} and @{text Oc}. One easy way to |
142 %\end{tikzpicture} |
190 represent such tapes is to use a pair of lists, written @{term "(l, |
143 %\end{center} |
191 r)"}, where @{term l} stands for the tape on the left of the |
|
192 read-write-unit and @{term r} for the tape on the right. We have the |
|
193 convention that the head, written @{term hd}, of the right-list is |
|
194 the cell on which the read-write-unit currently operates. This can |
|
195 be pictured as follows: |
|
196 |
|
197 \begin{center} |
|
198 \begin{tikzpicture} |
|
199 \draw[very thick] (-3.0,0) -- ( 3.0,0); |
|
200 \draw[very thick] (-3.0,0.5) -- ( 3.0,0.5); |
|
201 \draw[very thick] (-0.25,0) -- (-0.25,0.5); |
|
202 \draw[very thick] ( 0.25,0) -- ( 0.25,0.5); |
|
203 \draw[very thick] (-0.75,0) -- (-0.75,0.5); |
|
204 \draw[very thick] ( 0.75,0) -- ( 0.75,0.5); |
|
205 \draw[very thick] (-1.25,0) -- (-1.25,0.5); |
|
206 \draw[very thick] ( 1.25,0) -- ( 1.25,0.5); |
|
207 \draw[very thick] (-1.75,0) -- (-1.75,0.5); |
|
208 \draw[very thick] ( 1.75,0) -- ( 1.75,0.5); |
|
209 \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6); |
|
210 \draw[fill] (1.35,0.1) rectangle (1.65,0.4); |
|
211 \draw[fill] (0.85,0.1) rectangle (1.15,0.4); |
|
212 \draw[fill] (-0.35,0.1) rectangle (-0.65,0.4); |
|
213 \draw (-0.25,0.8) -- (-0.25,-0.8); |
|
214 \draw[<->] (-1.25,-0.7) -- (0.75,-0.7); |
|
215 \node [anchor=base] at (-0.8,-0.5) {\small left list}; |
|
216 \node [anchor=base] at (0.35,-0.5) {\small right list}; |
|
217 \node [anchor=base] at (0.1,0.7) {\small head}; |
|
218 \node [anchor=base] at (-2.2,0.2) {\ldots}; |
|
219 \node [anchor=base] at ( 2.3,0.2) {\ldots}; |
|
220 \end{tikzpicture} |
|
221 \end{center} |
144 |
222 |
145 An action is defined as |
223 \noindent |
|
224 Note that by using lists each side of the tape is only finite. The |
|
225 potential infinity is achieved by adding an appropriate blank cell |
|
226 whenever the read-write unit goes over the ``edge'' of the tape. To |
|
227 make this formal we define five possible \emph{actions} |
|
228 the Turing machine can perform: |
146 |
229 |
147 \begin{center} |
230 \begin{center} |
148 \begin{tabular}{rcll} |
231 \begin{tabular}{rcll} |
149 @{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\ |
232 @{text "a"} & $::=$ & @{term "W0"} & write blank (@{term Bk})\\ |
150 & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\ |
233 & $\mid$ & @{term "W1"} & write occupied (@{term Oc})\\ |
151 & $\mid$ & @{term L} & move left\\ |
234 & $\mid$ & @{term L} & move left\\ |
152 & $\mid$ & @{term R} & move right\\ |
235 & $\mid$ & @{term R} & move right\\ |
153 & $\mid$ & @{term Nop} & do nothing\\ |
236 & $\mid$ & @{term Nop} & do-nothing operation\\ |
154 \end{tabular} |
237 \end{tabular} |
155 \end{center} |
238 \end{center} |
|
239 |
|
240 \noindent |
|
241 By using the @{term Nop} operation, we slightly deviate |
|
242 from the presentation in \cite{Boolos87}; however its use |
|
243 will become important when we formalise universal Turing |
|
244 machines. Given a tape and an action, we can define the |
|
245 following updating function: |
|
246 |
|
247 \begin{center} |
|
248 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
249 @{thm (lhs) new_tape_def2(1)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(1)}\\ |
|
250 @{thm (lhs) new_tape_def2(2)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(2)}\\ |
|
251 @{thm (lhs) new_tape_def2(3)} & @{text "\<equiv>"} & \\ |
|
252 \multicolumn{3}{p{3cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(3)}}\\ |
|
253 @{thm (lhs) new_tape_def2(4)} & @{text "\<equiv>"} & \\ |
|
254 \multicolumn{3}{p{2cm}}{\hspace{1cm}@{thm (rhs) new_tape_def2(4)}}\\ |
|
255 @{thm (lhs) new_tape_def2(5)} & @{text "\<equiv>"} & @{thm (rhs) new_tape_def2(5)}\\ |
|
256 \end{tabular} |
|
257 \end{center} |
|
258 |
|
259 \noindent |
|
260 The first two clauses replace the head of the right-list |
|
261 with new @{term Bk} or @{term Oc}, repsectively. To see that |
|
262 these clauses make sense in case where @{text r} is the empty |
|
263 list, one has to know that the tail function, @{term tl}, is defined |
|
264 such that @{term "tl [] == []"} holds. The third clause |
|
265 implements the move of the read-write unit to the left: we need |
|
266 to test if the left-list is empty; if yes, then we just add a |
|
267 blank cell to the right-list; otherwise we have to remove the |
|
268 head from the left-list and add it to the right-list. Similarly |
|
269 in the clause for the right move. The @{term Nop} operation |
|
270 leaves the the tape unchanged. |
|
271 |
|
272 Note that our treatment of the tape is rather ``unsymmetric''---we |
|
273 have the convention that the head of the right-list is where |
|
274 the read-write unit is currently possitioned. Asperti and |
|
275 Ricciotti \cite{AspertiRicciotti12} also consider such a |
|
276 representation, but dismiss it as it complicates their |
|
277 definition for \emph{tape equality}. The reason is that |
|
278 moving the read-write unit to the left and then back |
|
279 to the right can change the tape (in case of going |
|
280 over the ``edge''). Therefore they distinguish four |
|
281 cases where the tape is empty as well as the read-write unit |
|
282 on the left edge, respectively right edge, or in the |
|
283 middle. The reading and moving of the tape is then |
|
284 defined in terms of these four cases. Since we are not |
|
285 going to use the notion of tape equality, we can |
|
286 get away with the definition above and be done with |
|
287 all corner cases. |
|
288 |
|
289 Next we need to define the \emph{states} of a Turing machine. Given |
|
290 how little is usually said about how to represent states in informal |
|
291 presentaions, it might be surprising that in a theorem prover we have |
|
292 to select carfully a representation. If we use the naive representation |
|
293 as a Turing machine consiting of a finite set of states, then we |
|
294 will have difficulties composing two Turing machines. We would need |
|
295 to somehow combine the two finite sets of states, possibly renaming |
|
296 states apart if both machines share states. This renaming can be |
|
297 quite cumbersome to reason about. Therefore we made the choice |
|
298 of representing a state by a natural number and the states of a |
|
299 Turing machine will always consist of the initial segment |
|
300 of natural numbers starting from @{text 0} up to number of states |
|
301 of the machine minus @{text 1}. In doing so we can compose |
|
302 two Turing machine by ``shifting'' the states of one by an appropriate |
|
303 amount to a higher segment. |
|
304 |
|
305 An \emph{instruction} of a Turing machine is a pair consisting of a |
|
306 natural number (the next state) and an action. A \emph{program} of a Turing |
|
307 machine is then a list of such pairs. Given a program @{term p}, a state |
|
308 and a cell being read by the read-write unnit, we need to fetch |
|
309 the corresponding instruction in the program. For this we define |
|
310 the function @{term fetch} |
|
311 |
|
312 \begin{center} |
|
313 \begin{tabular}{l@ {\hspace{1mm}}c@ {\hspace{1mm}}l} |
|
314 @{thm (lhs) fetch_def2(1)[where b=DUMMY]} & @{text "\<equiv>"} & @{thm (rhs) fetch_def2(1)}\\ |
|
315 @{thm (lhs) fetch_def2(2)} & @{text "\<equiv>"} & \\ |
|
316 \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(2)}}\\ |
|
317 @{thm (lhs) fetch_def2(3)} & @{text "\<equiv>"} & \\ |
|
318 \multicolumn{3}{l}{\hspace{1cm}@{thm (rhs) fetch_def2(3)}}\\ |
|
319 \end{tabular} |
|
320 \end{center} |
|
321 |
156 |
322 |
157 For showing the undecidability of the halting problem, we need to consider |
323 For showing the undecidability of the halting problem, we need to consider |
158 two specific Turing machines. |
324 two specific Turing machines. |
159 |
325 |
160 *} |
326 *} |