123   \renewcommand{\slidecaption}{ITP, 24 July 2013}

   123   \renewcommand{\slidecaption}{Imperial College, 24 November 2013}

   131   {\fontsize{20}{20}\selectfont{}Mechanising Turing Machines and}\\[-2mm] 

   131   {\fontsize{30}{30}\selectfont{}Turing Machines and}\\[-1mm]  

   132   {\fontsize{20}{20}\selectfont{}Computability Theory in Isabelle}\\[-3mm] 

   132   {\fontsize{30}{30}\selectfont{}Separation Logic}\\[0mm]

   133   {\fontsize{22}{22}\selectfont{}(Work in Progress)}\\[-3mm] 

   162   \item At the beginning, it was just a student project

   163   \item we wanted to formalise computability theory

   163   about computability.\smallskip

   164   \item at the beginning, it was just a student project\smallskip

   177   \end{frame}}

   178   \only<2->{

   178   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   179   \begin{textblock}{1}(0.7,4)

   179 *}

   180   \begin{tikzpicture}

   180 

   181   \draw (0,0) node[inner sep=2mm,fill=cream, ultra thick, draw=red, rounded corners=2mm] 

   181 text_raw {*

   182   {\normalsize

   182   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   183   \begin{minipage}{11cm}

   183   \mode<presentation>{

   184   \begin{quote}\rm

   184   \begin{frame}[c]

   185   \begin{itemize}

   185   \frametitle{Some Previous Works}%

   186   \item is a fantastic model of low-level code

   187   \item completely unstructured\makebox[0mm][10mm]{\mbox{}}\;\; 

   188   \only<2>{\textcolor{cream}{\fontspec{Chalkduster}Spaghetti Code}}%

   189   \only<3->{\textcolor{red}{\fontspec{Chalkduster}Spaghetti Code}}

   190   \bigskip

   191   \item good testbed for verification techniques

   192   \item Can we verify a program with 38 Mio instructions?

   193   \item we can delay implementing a concrete machine model (for OS/low-level code verification)

   194   \end{itemize}

   195   \end{quote}

   196   \end{minipage}};

   197   \end{tikzpicture}

   198   \end{textblock}}

   199 

   200   \end{frame}}

   201   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

   202 *}

   203 

   204 text_raw {*

   205   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

   206   \mode<presentation>{

   207   \begin{frame}[c]

   208   \frametitle{

   209   \begin{tabular}{c}Some Previous Works\\[-5mm]

   210   \hspace{3.5cm}\small (but not interested in low-level code)

   211   \end{tabular}}%

   202   alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}

   228   alphabet with respect to the machines it simulates is annoying." (Asperti and Ricciotti)}

   219   \begin{frame}[c]

   245   \begin{frame}[t]

   225   { \node (def1)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&

   252   { \node (tm)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&

   226     \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&

   253     \node (reg) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&

   227     \node (alg1)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    

   254     \node (rf)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    

   230   \draw[->,black!50,line width=2mm] (proof1) -- (def1);

   257   \only<2->{\draw[->,black!50,line width=2mm] (reg) -- (tm);}

   231   \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);

   258   \only<2->{\draw[<-,black!50,line width=2mm] (reg) -- (rf);}

   232   

   259 

   233   \end{tikzpicture}

   260   \only<4->{

   234   \end{center}

   261    \draw [<-, black!50,line width=2mm, rounded corners]

   262      %  start right of digit.east, that is, at the point that is the

   263      %  linear combination of digit.east and the vector (2mm,0pt). We

   264      %  use the ($ ... $) notation for computing linear combinations

   265      ($ (rf.south) + (0mm,0) $)

   266      %  Now go down

   267      -- ++(0,-2.5)

   268      %  And back to the left of digit.west

   269      -| ($ (tm.south) - (0mm,0) $);}

   270   

   271   \end{tikzpicture}

   272   \end{center}

   273 

   274   \only<1->{

   275   \begin{textblock}{3}(1,4.9)

   276   \begin{tikzpicture}

   277   \draw (0,0) node {\small\begin{tabular}{l}undecidability\\of the halting\\ problem\end{tabular}};

   278   \end{tikzpicture}

   279   \end{textblock}}

   237   \begin{textblock}{3}(8.3,4.0)

   282   \begin{textblock}{3}(8.3,8.4)

   239   \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

   284   \node at (0,0) [single arrow, shape border rotate=90, fill=black!50,text=white]{};

   240   \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   285   \draw (0,-1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   244   \begin{textblock}{3}(3.1,4.0)

   289   \begin{textblock}{3}(3.1,8.4)

   246   \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};

   291   \node at (0,0) [single arrow, shape border rotate=90, fill=black!50,text=white]{};

   247   \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   292   \draw (0,-1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};

   252   \begin{textblock}{4}(10.9,9.4)

   297   \begin{textblock}{4}(12.5,5.8)

   265   \begin{textblock}{4}(4.2,12.4)

   304   \begin{textblock}{4}(3.3,13.3)

   382   can be defined by simple recursion\\ (HOL has @{term "Least"})

   421   \hspace{3mm}can be defined by recursion (HOL has @{term "Least"})

   612   \item Suppose @{text H} decides @{text contra} called with the code 

   725   \item Suppose @{text H} decides whether @{text contra} called with the code 

   637   \item Suppose @{text H} decides @{text contra} called with the code 

   750   \item Suppose @{text H} decides wether @{text contra} called with the code 

   638   of @{text contra} does \emph{not} halt, then\\[-8mm]\mbox{}

   751   of @{text contra} does \alert{not} halt, then\\[-8mm]\mbox{}

   726   \end{center}\smallskip\pause

   839   \end{center}\smallskip

   727 

   840 

   728   \item an observation: our treatment of recursive functions is a mini-version

   729   of the work by\\ Myreen \& Owens about deeply embedding HOL

   780   assembly programs and macros\bigskip

   920   assembler programs and macros\bigskip

   781   

   921   

   782   \item assembly for TMs:\medskip

   922   \item assembler for TMs:\medskip

   832   \begin{frame}[c]

   972   \begin{frame}[t]

   833   \frametitle{{\large The Trouble With Hoare-Triples}}%

   973   \frametitle{An RM-API with TMs}%

   834 

   974 

   835   \begin{itemize}

   975   \begin{center}

   836   \item Whenever we wanted to prove 

   976   \begin{tikzpicture}

   837 

   977   \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]

   838   \begin{center}

   978   { \node (tm)   [node1, minimum size=44mm] {\mbox{}}; \&

   839   \large @{text "{P} p {Q}"}

   979     \node (rf)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    

   840   \end{center}\bigskip\medskip

   980   };

   841  

   981 

   842   \item[@{text "(1)"}] we had to find invariants for each state\\ \textcolor{gray}{(not easy)}

   982   \draw[->,black!50,line width=2mm] (rf) -- (tm);

   843 

   983   

   844   

   984   \node [above, rotate=90] at (tm.east) {\textcolor{gray}{Reg.Mach. API}};

   845   

   985   \node [below right] at (tm.north west) {\textcolor{gray}{Macros}};

   846   \item[@{text "(2)"}] we had to find a termination order proving that @{text p} terminates

   986   \node [node1] at (tm) {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; 

   847   \textcolor{gray}{(not easy either)}

   987   

   848   \end{itemize}\pause

   988 

   849   

   989   \end{tikzpicture}

   850   \begin{center}

   990   \end{center}

   851   \alert{very little opportunity for automation}

   991 

   992   \begin{itemize}

   993   \item Suppose the first four registers of an RM contain 1,2,0 and 3, then the encoding is

   994 

   995   \begin{center}

   996   \begin{tikzpicture}[scale=1]

   997 

   998   \draw[very thick] (-0.25,0)   -- ( 8.25,0);

   999   \draw[very thick] (-0.25,0.5) -- ( 8.25,0.5);

  1000 

  1001   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  1002   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  1003   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  1004   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  1005   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);  

  1006   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5); 

  1007   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);  

  1008   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5); 

  1009   \draw[very thick] ( 3.75,0)   -- ( 3.75,0.5); 

  1010   \draw[very thick] ( 4.25,0)   -- ( 4.25,0.5); 

  1011   \draw[very thick] ( 4.75,0)   -- ( 4.75,0.5); 

  1012   \draw[very thick] ( 5.25,0)   -- ( 5.25,0.5); 

  1013   \draw[very thick] ( 5.75,0)   -- ( 5.75,0.5); 

  1014   \draw[very thick] ( 6.25,0)   -- ( 6.25,0.5); 

  1015   \draw[very thick] ( 6.75,0)   -- ( 6.75,0.5); 

  1016 

  1017   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  1018   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

  1019   \draw[fill]     ( 1.35,0.1) rectangle (1.65,0.4);

  1020   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

  1021   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

  1022   \draw[fill]     ( 3.35,0.1) rectangle (3.65,0.4);

  1023   \draw[fill]     ( 4.35,0.1) rectangle (4.65,0.4);

  1024   \draw[fill]     ( 4.85,0.1) rectangle (5.15,0.4);

  1025   \draw[fill]     ( 5.35,0.1) rectangle (5.65,0.4);

  1026   \draw[fill]     ( 5.85,0.1) rectangle (6.15,0.4);

  1027   \end{tikzpicture}

  1028 

  1029   \end{center}

  1030   \end{itemize}

  1031 

  1032   \end{frame}}

  1033   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1034 *}

  1035 

  1036 text_raw {*

  1037   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1038   \mode<presentation>{

  1039   \begin{frame}[c]

  1040   \frametitle{Inc a}%

  1041 

  1042   \begin{center}

  1043   \begin{tabular}{@ {\hspace{-10mm}}l}

  1044   @{text "Inc a"} @{text "\<equiv>"} \\

  1045   \hspace{16mm} @{text "locate a"} @{text ";"}\\

  1046   \hspace{16mm} @{text "right_until_zero"} @{text ";"}\\

  1047   \hspace{16mm} @{text "move_right"} @{text ";"}\\

  1048   \hspace{16mm} @{text "shift_right"} @{text ";"}\\

  1049   \hspace{16mm} @{text "move_left"} @{text ";"}\\

  1050   \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\

  1051   \hspace{16mm} @{text "write_one"} @{text ";"}\\

  1052   \hspace{16mm} @{text "left_until_double_zero"} @{text ";"}\\

  1053   \hspace{16mm} @{text "move_right"} @{text ";"}\\

  1054   \hspace{16mm} @{text "move_right"}\\

  1055   \end{tabular}

   899   @{text "c"} can be\;\;\; @{text "i:[move_left_until_zero]:j"}

  1103   \begin{center}

   900   

  1104   @{text "\<lbrace> st i \<star> hd v \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\

  1105   @{text "i:[left_until_zero]:j"}\\

  1106   @{text "\<lbrace> st j \<star> hd u \<star> zero u \<star> ones (u + 1) v \<rbrace>"}\\

  1107   \end{center}

  1108 

  1109   \end{frame}}

  1110   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1111 *}

  1112 

  1113 text_raw {*

  1114   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1115   \mode<presentation>{

  1116   \begin{frame}[c]

  1117   \frametitle{Inductions over \textit{ones}}%

  1118 

  1119   \begin{itemize}

  1120   \item What most simplifies the work is that we can do inductions over

  1121   the ''input'' (inductively defined assertions)\pause\medskip

  1122 

  1123   \item Suppose @{text "right_until_zero"}:\bigskip

  1124 

  1125     \begin{center}

  1126   \begin{tikzpicture}[scale=1]

  1127 

  1128   \draw[very thick] (-0.25,0)   -- ( 8.25,0);

  1129   \draw[very thick] (-0.25,0.5) -- ( 8.25,0.5);

  1130 

  1131   \draw[very thick] (-0.25,0)   -- (-0.25,0.5);

  1132   \draw[very thick] ( 0.25,0)   -- ( 0.25,0.5);

  1133   \draw[very thick] ( 0.75,0)   -- ( 0.75,0.5);

  1134   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);

  1135   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);  

  1136   \draw[very thick] ( 2.25,0)   -- ( 2.25,0.5); 

  1137   \draw[very thick] ( 2.75,0)   -- ( 2.75,0.5);  

  1138   \draw[very thick] ( 3.25,0)   -- ( 3.25,0.5); 

  1139   \draw[very thick] ( 3.75,0)   -- ( 3.75,0.5); 

  1140   \draw[very thick] ( 4.25,0)   -- ( 4.25,0.5); 

  1141   \draw[very thick] ( 4.75,0)   -- ( 4.75,0.5); 

  1142   \draw[very thick] ( 5.25,0)   -- ( 5.25,0.5); 

  1143   \draw[very thick] ( 5.75,0)   -- ( 5.75,0.5); 

  1144   \draw[very thick] ( 6.25,0)   -- ( 6.25,0.5); 

  1145   \draw[very thick] ( 6.75,0)   -- ( 6.75,0.5); 

  1146   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);

  1147   \draw[fill]     (-0.15,0.1) rectangle (0.15,0.4);

  1148   \draw[fill]     ( 0.35,0.1) rectangle (0.65,0.4);

  1149   \draw[fill]     ( 0.85,0.1) rectangle (1.15,0.4);

  1150   \draw[fill]     ( 1.35,0.1) rectangle (1.65,0.4);

  1151   \draw[fill]     ( 1.85,0.1) rectangle (2.15,0.4);

  1152   \draw[fill]     ( 2.35,0.1) rectangle (2.65,0.4);

  1153   \draw[fill]     ( 3.35,0.1) rectangle (3.65,0.4);

  1154   \draw[fill]     ( 3.85,0.1) rectangle (4.15,0.4);

  1155   \draw[fill]     ( 4.35,0.1) rectangle (4.65,0.4);

  1156   \draw[fill]     ( 4.85,0.1) rectangle (5.15,0.4);

  1157   \draw[fill]     ( 5.35,0.1) rectangle (5.65,0.4);

  1158   \draw[fill]     ( 5.85,0.1) rectangle (6.15,0.4);

  1159 

  1160   \path (2.75,0) edge [decorate,decoration={brace,amplitude=14pt}, thick] node[below=8pt] 

  1161   {\small\textcolor{gray}{@{text "ones u v"}}} (-0.25,0);

  1162 

  1163   \end{tikzpicture}

  1164   \end{center}

  1165 

  1166   \begin{center}

  1167   @{text "\<lbrace> st i \<star> hd u \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\

  1168   @{text "i:[right_until_zero]:j"}\\

  1169   @{text "\<lbrace> st j \<star> hd (v + 1) \<star> zero (v + 1) \<star> ones u v \<rbrace>"}\\

  1170   \end{center}

  1171   \end{itemize}

  1172 

  1173   \begin{textblock}{3}(11,10)

  1174   \begin{tikzpicture}

  1175   \only<2>{\node at (0,0) [single arrow, shape border rotate=270, fill=red,text=white]{\mbox{\alert{a}}};}

  1176   \end{tikzpicture}

  1177   \end{textblock}

   920   of the input (e.g.~how many @{text "1"}s are on the tape)\pause

  1197   of the input (e.g.~how many @{text "0"}s/@{text "1"}s are on the tape)

   921   

  1198   

   922   \item these macros allow us to completely get rid of register machines

  1199   \item no termination measures are needed

   923   \end{itemize}

  1200 

   924   

  1201   \end{itemize}

   925 

  1202   

   926   \end{frame}}

  1203 

   927   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1204   \end{frame}}

   928 *}

  1205   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1206 *}

  1207 

  1208 text_raw {*

  1209   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

  1210   \mode<presentation>{

  1211   \begin{frame}[c]

  1212   \frametitle{Register Machines}%

  1213 

  1214   \begin{itemize}

  1215   \item We could also use Jensen's et al work to give

  1216   a more appropriate \alert{view}  on register machines

  1217 

  1218   \begin{center}

  1219   @{text "\<lbrace>p\<rbrace> i:[rm_c]:j \<lbrace>q\<rbrace>"}

  1220   \end{center}\bigskip

  1221   \end{itemize}

  1222   

  1223   \small

  1224   \begin{itemize}

  1225       \item Rule for @{text "Inc"}

  1226 

  1227              \begin{tabular}{rl}

  1228                @{text "RM."} & @{text "\<lbrace> pc i \<star> m a v \<rbrace>"} \\

  1229                & @{text "i:[ Inc a ]:j"} \\

  1230                & @{text "\<lbrace> pc j \<star> m a (Suc v)\<rbrace>"}

  1231              \end{tabular}

  1232      \item Rules for @{text "Dec"}

  1233      \begin{tabular}{c c}

  1234        \begin{tabular}{r l}

  1235             @{text "RM."} & @{text "\<lbrace>(pc i \<star> m a (Suc v))\<rbrace>"} \\

  1236           & @{text "i :[ Dec a e ]: j"} \\

  1237           & @{text "\<lbrace>pc j \<star> m a v\<rbrace>"}

  1238        \end{tabular} &

  1239        \begin{tabular}{r l}

  1240          @{text "RM."} & @{text "\<lbrace> pc i \<star> m a 0 \<rbrace>"} \\

  1241          & @{text "i:[ Dec a e ]:j"} \\

  1242          & @{text "\<lbrace> pc e \<star> m a 0 \<rbrace>"}

  1243        \end{tabular}

  1244      \end{tabular}

  1245     %\item Rule for @{text "Goto"}

  1246     %

  1247     %   \begin{tabular}{r l}

  1248     %     @{text "RM."} & @{text "\<lbrace> pc i \<rbrace>"} \\

  1249     %    &@{text "i:[ (Goto e) ]:j"} \\

  1250     %    &@{text "\<lbrace> pc e \<rbrace>"}

  1251     %   \end{tabular} 

  1252   \end{itemize}

  1253 

  1254 

  1255   \end{frame}}

  1256   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     

  1257 *}

  1258