equal
deleted
inserted
replaced
1256 the abacus programs. One last problem to overcome is that an abacus |
1256 the abacus programs. One last problem to overcome is that an abacus |
1257 program is assumed to calculate a value stored in the last |
1257 program is assumed to calculate a value stored in the last |
1258 register (the one with the highest register). That means we have to append a Turing machine that |
1258 register (the one with the highest register). That means we have to append a Turing machine that |
1259 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1259 ``mops up'' the tape (cleaning all @{text Oc}s) except for the |
1260 @{term Oc}s of the last register represented on the tape. This needs |
1260 @{term Oc}s of the last register represented on the tape. This needs |
1261 a Turing machine program with @{text "2 * R + 12"} states, assuming @{text R} |
1261 a Turing machine program with @{text "2 * R + 6"} states, assuming @{text R} |
1262 is the number of registers to be ``cleaned''. |
1262 is the number of registers to be ``cleaned''. |
1263 |
1263 |
1264 While generating the Turing machine program for an abacus program is |
1264 While generating the Turing machine program for an abacus program is |
1265 not too difficult to formalise, the problem is that it contains |
1265 not too difficult to formalise, the problem is that it contains |
1266 @{text Goto}s all over the place. The unfortunate result is that we |
1266 @{text Goto}s all over the place. The unfortunate result is that we |
1561 theorem. So our conclusion is that this part is not as daunting |
1561 theorem. So our conclusion is that this part is not as daunting |
1562 as we estimated when reading the paper by Norrish \cite{Norrish11}. The work |
1562 as we estimated when reading the paper by Norrish \cite{Norrish11}. The work |
1563 involved with constructing a universal Turing machine via recursive |
1563 involved with constructing a universal Turing machine via recursive |
1564 functions and abacus machines, we agree, is not a project |
1564 functions and abacus machines, we agree, is not a project |
1565 one wants to undertake too many times (our formalisation of abacus |
1565 one wants to undertake too many times (our formalisation of abacus |
1566 machines and their correct translation is approximately 4300 loc; |
1566 machines and their correct translation is approximately 4600 loc; |
1567 recursive functions 5000 loc and the universal Turing machine 10000 loc). |
1567 recursive functions 5000 loc and the universal Turing machine 10000 loc). |
1568 |
1568 |
1569 Our work is also very much inspired by the formalisation of Turing |
1569 Our work is also very much inspired by the formalisation of Turing |
1570 machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the |
1570 machines by Asperti and Ricciotti \cite{AspertiRicciotti12} in the |
1571 Matita theorem prover. It turns out that their notion of |
1571 Matita theorem prover. It turns out that their notion of |