equal
deleted
inserted
replaced
1392 easily construct a universal Turing machine via a universal |
1392 easily construct a universal Turing machine via a universal |
1393 function. This is different from Norrish \cite{Norrish11} who gives a universal |
1393 function. This is different from Norrish \cite{Norrish11} who gives a universal |
1394 function for Church numbers, and also from Asperti and Ricciotti |
1394 function for Church numbers, and also from Asperti and Ricciotti |
1395 \cite{AspertiRicciotti12} who construct a universal Turing machine |
1395 \cite{AspertiRicciotti12} who construct a universal Turing machine |
1396 directly, but for simulating Turing machines with a more restricted alphabet. |
1396 directly, but for simulating Turing machines with a more restricted alphabet. |
1397 \emph{Recursive functions} are defined as the datatype |
1397 Unlike Norrish \cite{Norrish11}, we need to represent recursive functions |
|
1398 ``deeply'' because we want to translate them to abacus programs. |
|
1399 Thus \emph{recursive functions} are defined as the datatype |
1398 |
1400 |
1399 \begin{center} |
1401 \begin{center} |
1400 \begin{tabular}{c@ {\hspace{4mm}}c} |
1402 \begin{tabular}{c@ {\hspace{4mm}}c} |
1401 \begin{tabular}{rcl@ {\hspace{4mm}}l} |
1403 \begin{tabular}{rcl@ {\hspace{4mm}}l} |
1402 @{term r} & @{text "::="} & @{term z} & (zero-function)\\ |
1404 @{term r} & @{text "::="} & @{term z} & (zero-function)\\ |