Mercurial Mercurial > hg > tm / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a comment about deeply embedding of recursive functions
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Wed, 06 Mar 2013 00:59:18 +0000
changeset 214 763ed488fa79
parent 213 30d81499766b
child 215 12f278bd67aa
added a comment about deeply embedding of recursive functions
Paper/Paper.thy file | annotate | diff | comparison | revisions
paper.pdf file | annotate | diff | comparison | revisions 
--- a/Paper/Paper.thy	Tue Mar 05 15:23:10 2013 +0000
+++ b/Paper/Paper.thy	Wed Mar 06 00:59:18 2013 +0000
@@ -1394,7 +1394,9 @@
   function for Church numbers, and also from Asperti and Ricciotti 
   \cite{AspertiRicciotti12} who construct a universal Turing machine
   directly, but for simulating Turing machines with a more restricted alphabet.
-  \emph{Recursive functions} are defined as the datatype
+  Unlike Norrish \cite{Norrish11}, we need to represent recursive functions
+  ``deeply'' because we want to translate them to abacus programs.
+  Thus \emph{recursive functions} are defined as the datatype
 
   \begin{center}
   \begin{tabular}{c@ {\hspace{4mm}}c}
Binary file paper.pdf has changed
tm