169 Myhill-Nerode theorem, where regular expressions fared much better |
169 Myhill-Nerode theorem, where regular expressions fared much better |
170 than automata \cite{WuZhangUrban11}. However, with Turing machines |
170 than automata \cite{WuZhangUrban11}. However, with Turing machines |
171 there seems to be no alternative if one wants to formalise the great |
171 there seems to be no alternative if one wants to formalise the great |
172 many proofs from the literature that use them. We will analyse one |
172 many proofs from the literature that use them. We will analyse one |
173 example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The |
173 example---undecidability of Wang's tiling problem---in Section~\ref{Wang}. The |
174 standard proof of this property uses the notion of \emph{universal |
174 standard proof of this property uses the notion of universal |
175 Turing machines}. |
175 Turing machines. |
176 |
176 |
177 We are not the first who formalised Turing machines in a theorem |
177 We are not the first who formalised Turing machines in a theorem |
178 prover: we are aware of the preliminary work by Asperti and Ricciotti |
178 prover: we are aware of the preliminary work by Asperti and Ricciotti |
179 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
179 \cite{AspertiRicciotti12}. They describe a complete formalisation of |
180 Turing machines in the Matita theorem prover, including a universal |
180 Turing machines in the Matita theorem prover, including a universal |
218 the reasoning more uniform. In addition some proofs \emph{about} Turing |
218 the reasoning more uniform. In addition some proofs \emph{about} Turing |
219 machines are simpler. The reason is that one often needs to encode |
219 machines are simpler. The reason is that one often needs to encode |
220 Turing machines---consequently if the Turing machines are simpler, then the coding |
220 Turing machines---consequently if the Turing machines are simpler, then the coding |
221 functions are simpler too. Unfortunately, the restrictiveness also makes |
221 functions are simpler too. Unfortunately, the restrictiveness also makes |
222 it harder to design programs for these Turing machines. In order |
222 it harder to design programs for these Turing machines. In order |
223 to construct a \emph{universal Turing machine} we therefore do not follow |
223 to construct a universal Turing machine we therefore do not follow |
224 \cite{AspertiRicciotti12}, instead follow the proof in |
224 \cite{AspertiRicciotti12}, instead follow the proof in |
225 \cite{Boolos87} by relating abacus machines to Turing machines and in |
225 \cite{Boolos87} by relating abacus machines to Turing machines and in |
226 turn recursive functions to abacus machines. The universal Turing |
226 turn recursive functions to abacus machines. The universal Turing |
227 machine can then be constructed as a recursive function. |
227 machine can then be constructed as a recursive function. |
228 |
228 |
229 \smallskip |
229 \smallskip |
230 \noindent |
230 \noindent |
231 {\bf Contributions:} |
231 {\bf Contributions:} We formalised in Isabelle/HOL Turing machines following the |
232 |
232 description of Boolos et al \cite{Boolos87} where tapes only have blank or |
|
233 occupied cells. We mechanise the undecidability of the halting problem and |
|
234 prove the correctness of concrete Turing machines that are needed |
|
235 in this proof; such correctness proofs are left out in the informal literature. |
|
236 We construct the universal Turing machine from \cite{Boolos87} by |
|
237 relating recursive functions to abacus machines and abacus machines to |
|
238 Turing machines. Since we have set up in Isabelle/HOL a very general computability |
|
239 model and undecidability result, we are able to formalise the |
|
240 undecidability of Wang's tiling problem. We are not aware of any other |
|
241 formalisation of a substantial undecidability problem. |
233 *} |
242 *} |
234 |
243 |
235 section {* Turing Machines *} |
244 section {* Turing Machines *} |
236 |
245 |
237 text {* \noindent |
246 text {* \noindent |