70 the $\lambda$-calculus as the starting point for his formalisation of

    70 the $\lambda$-calculus as the starting point for his formalisation of

    71 computability theory, because of its ``simplicity'' \cite[Page

    71 computability theory, because of its ``simplicity'' \cite[Page

    72 297]{Norrish11}.  Part of his formalisation is a clever infrastructure

    72 297]{Norrish11}.  Part of his formalisation is a clever infrastructure

    73 for reducing $\lambda$-terms. He also established the computational

    73 for reducing $\lambda$-terms. He also established the computational

    74 equivalence between the $\lambda$-calculus and recursive functions.

    74 equivalence between the $\lambda$-calculus and recursive functions.

    76  to have formalisations for more operational models of

    76  to have formalisations for more operational models of

    77 computations, such as Turing machines or register machines.  One

    77 computations, such as Turing machines or register machines.  One

    78 reason is that many proofs in the literature use them.  He noted

    78 reason is that many proofs in the literature use them.  He noted

    79 however that \cite[Page 310]{Norrish11}:

    79 however that \cite[Page 310]{Norrish11}:

    80 

    80 

   230   

   230   

   231   \noindent

   231   \noindent

   232   Note that by using lists each side of the tape is only finite. The

   232   Note that by using lists each side of the tape is only finite. The

   233   potential infinity is achieved by adding an appropriate blank or occupied cell 

   233   potential infinity is achieved by adding an appropriate blank or occupied cell 

   234   whenever the head goes over the ``edge'' of the tape. To 

   234   whenever the head goes over the ``edge'' of the tape. To 

   236   the Turing machine can perform:

   236   the Turing machine can perform:

   237 

   237 

   238   \begin{center}

   238   \begin{center}

   239   \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}

   239   \begin{tabular}[t]{@ {}rcl@ {\hspace{2mm}}l}

   240   @{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\

   240   @{text "a"} & $::=$  & @{term "W0"} & (write blank, @{term Bk})\\