1670 Norrish mentions |
1670 Norrish mentions |
1671 that formalising Turing machines would be a ``\emph{daunting prospect}'' |
1671 that formalising Turing machines would be a ``\emph{daunting prospect}'' |
1672 \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to |
1672 \cite[Page 310]{Norrish11}. While $\lambda$-terms indeed lead to |
1673 some slick mechanised proofs, our experience is that Turing machines |
1673 some slick mechanised proofs, our experience is that Turing machines |
1674 are not too daunting if one is only concerned with formalising the |
1674 are not too daunting if one is only concerned with formalising the |
1675 undecidability of the halting problem for Turing machines. This |
1675 undecidability of the halting problem for Turing machines. As a point of |
|
1676 comparison, the halting problem |
1676 took us around 1500 loc of Isar-proofs, which is just one-and-a-half |
1677 took us around 1500 loc of Isar-proofs, which is just one-and-a-half |
1677 times of a mechanised proof pearl about the Myhill-Nerode |
1678 times of a mechanised proof pearl about the Myhill-Nerode |
1678 theorem. So our conclusion is that this part is not as daunting |
1679 theorem. So our conclusion is that this part is not as daunting |
1679 as we estimated when reading the paper by Norrish \cite{Norrish11}. The work |
1680 as we estimated when reading the paper by Norrish \cite{Norrish11}. The work |
1680 involved with constructing a universal Turing machine via recursive |
1681 involved with constructing a universal Turing machine via recursive |
1703 presentations leave out any arguments why these Turing machines |
1704 presentations leave out any arguments why these Turing machines |
1704 should be correct. This means the reader is left |
1705 should be correct. This means the reader is left |
1705 with the task of finding appropriate invariants and measures for |
1706 with the task of finding appropriate invariants and measures for |
1706 showing the correctness and termination of these Turing machines. |
1707 showing the correctness and termination of these Turing machines. |
1707 Whenever we can use Hoare-style reasoning, the invariants are |
1708 Whenever we can use Hoare-style reasoning, the invariants are |
1708 relatively straightforward and as a point of comparison much smaller than for example the |
1709 relatively straightforward and again as a point of comparison much smaller than for example the |
1709 invariants used by Myreen in a correctness proof of a garbage collector |
1710 invariants used by Myreen in a correctness proof of a garbage collector |
1710 written in machine code \cite[Page 76]{Myreen09}. However, the invariant |
1711 written in machine code \cite[Page 76]{Myreen09}. However, the invariant |
1711 needed for the abacus proof, where Hoare-style reasoning does not work, is |
1712 needed for the abacus proof, where Hoare-style reasoning does not work, is |
1712 similar in size as the one by Myreen and finding a sufficiently |
1713 similar in size as the one by Myreen and finding a sufficiently |
1713 strong one took us, like Myreen, something on the magnitude of |
1714 strong one took us, like Myreen, something on the magnitude of |