# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1374583942 -7200
# Node ID fa021a0c698437d8c336e6bc6c4cee27beb27acc
# Parent  42f2c28d1ce6a78dafeb687ef83eeae105031b36
new slides

diff -r 42f2c28d1ce6 -r fa021a0c6984 Slides/Slides2.thy
--- a/Slides/Slides2.thy	Tue Jul 23 09:06:34 2013 +0200
+++ b/Slides/Slides2.thy	Tue Jul 23 14:52:22 2013 +0200
@@ -9,6 +9,39 @@
 abbreviation
   "update2 p a \<equiv> update a p"
 
+notation (Rule output)
+  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+syntax (Rule output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:\mbox{}\inferrule{>_\<^raw:}>\<^raw:{\mbox{>_\<^raw:}}>")
+
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" 
+  ("\<^raw:\mbox{>_\<^raw:}\\>/ _")
+
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (Axiom output)
+  "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
+
+notation (IfThen output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThen output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}> /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
+
+notation (IfThenNoBox output)
+  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+syntax (IfThenNoBox output)
+  "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
+  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "_asms" :: "prop \<Rightarrow> asms \<Rightarrow> asms" ("_ /\<^raw:{\normalsize \,>and\<^raw:\,}>/ _")
+  "_asm" :: "prop \<Rightarrow> asms" ("_")
+
+context uncomputable
+begin
 
 notation (latex output)
   Cons ("_::_" [48,47] 68) and
@@ -25,8 +58,16 @@
   inv_loop1 ("J\<^isub>1") and
   inv_loop0 ("J\<^isub>0") and
   inv_end1 ("K\<^isub>1") and
-  inv_end0 ("K\<^isub>0")
-
+  inv_end0 ("K\<^isub>0") and
+  recf.id ("Id\<^raw:\makebox[0mm]{\,\,\,\,>\<^isup>_\<^raw:}>\<^isub>_") and
+  Pr ("Pr\<^isup>_") and
+  Cn ("Cn\<^isup>_") and
+  Mn ("Mn\<^isup>_") and
+  tcopy ("copy") and 
+  tcontra ("contra") and
+  tape_of ("\<langle>_\<rangle>") and 
+  code_tcontra ("code contra") and
+  tm_comp ("_ ; _") 
 
  
 lemma inv_begin_print:
@@ -141,21 +182,26 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Some Previous Work}%
+  \frametitle{Some Previous Works}%
 
   \begin{itemize}
   \item Norrish formalised computability theory in HOL starting
-  from the lambda-calculus 
+  from the lambda-calculus\smallskip 
   \begin{itemize}
   \item \textcolor{gray}{for technical reasons we could not follow him}
   \item \textcolor{gray}{some proofs use TMs (Wang tilings)}
   \end{itemize}
- 
-
-
   \bigskip
 
-  \item Asperti and Ricciotti formalised TMs in Matita
+  \item Asperti and Ricciotti formalised TMs in Matita\smallskip
+  \begin{itemize}
+  \item \textcolor{gray}{no undecidability $\Rightarrow$ interest in complexity}
+  \item \textcolor{gray}{their UTM operates on a different alphabet than the TMs it simulates.}
+  \begin{quote}
+  \textcolor{gray}{"In particular, the fact that the universal machine operates with a different 
+  alphabet with respect to the machines it simulates is annoying." [Asperti and Ricciotti]}
+  \end{quote}
+  \end{itemize}
   \end{itemize}
 
   \end{frame}}
@@ -163,6 +209,64 @@
 *}
 
 text_raw {*
+  \tikzstyle{every node}=[node distance=25mm,text height=1.5ex, text depth=.25ex]
+  \tikzstyle{node1}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=black!50, top color=white, bottom color=black!20]
+  \tikzstyle{node2}=[rectangle, minimum size=12mm, rounded corners=3mm, very thick, 
+                     draw=red!70, top color=white, bottom color=red!50!black!20]
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{The Big Picture}%
+
+  \begin{center}
+  \begin{tikzpicture}
+  \matrix[ampersand replacement=\&,column sep=13mm, row sep=5mm]
+  { \node (def1)   [node1] {\large\hspace{1mm}TMs\hspace{1mm}\mbox{}}; \&
+    \node (proof1) [node1] {\begin{tabular}{c}Register\\Machines\end{tabular}}; \&
+    \node (alg1)   [node1] {\begin{tabular}{c}Recursive\\ Functions\end{tabular}}; \\    
+  };
+
+  \draw[->,black!50,line width=2mm] (proof1) -- (def1);
+  \draw[<-,black!50,line width=2mm] (proof1) -- (alg1);
+  
+  \end{tikzpicture}
+  \end{center}
+
+  \only<2->{
+  \begin{textblock}{3}(8.3,4.0)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
+  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}
+
+  \begin{textblock}{3}(3.1,4.0)
+  \begin{tikzpicture}
+  \node at (0,0) [single arrow, shape border rotate=270, fill=black!50,text=white]{};
+  \draw (0,1) node {\begin{tabular}{l}verified\\[-1mm] translator\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \only<3->{
+  \begin{textblock}{4}(10.9,9.4)
+  \begin{tikzpicture}
+  \draw (0,0) node {\begin{tabular}{l}UF\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}
+
+  \begin{textblock}{3}(1,10.0)
+  \begin{tikzpicture}
+  \draw (0,0) node {\small\begin{tabular}{l}undecidabilty\\of the halting\\ problem\end{tabular}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
@@ -183,6 +287,8 @@
   \draw[very thick] ( 1.25,0)   -- ( 1.25,0.5);
   \draw[very thick] (-1.75,0)   -- (-1.75,0.5);
   \draw[very thick] ( 1.75,0)   -- ( 1.75,0.5);
+  \draw[very thick] ( 3.0,0)   -- ( 3.0,0.5);
+  \draw[very thick] (-3.0,0)   -- (-3.0,0.5);
   \draw[rounded corners=1mm] (-0.35,-0.1) rectangle (0.35,0.6);
   \draw[fill]     (1.35,0.1) rectangle (1.65,0.4);
   \draw[fill]     (0.85,0.1) rectangle (1.15,0.4);
@@ -196,7 +302,7 @@
   \node [anchor=base] at (-2.2,0.2) {\ldots};
   \node [anchor=base] at ( 2.3,0.2) {\ldots};
   \end{tikzpicture}
-  \end{center}
+  \end{center}\pause
 
   \item @{text steps} function:
 
@@ -204,7 +310,7 @@
   What does the TM claclulate after it has executed @{text n} steps?
   \end{quote}\pause
 
-  \item designate the @{text 0}-state as \"halting state\" and remain there 
+  \item designate the @{text 0}-state as "halting state" and remain there 
   forever, i.e.~have a @{text Nop}-action
   \end{itemize}
 
@@ -213,25 +319,69 @@
 *}
 
 text_raw {*
+  
+
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Register Machines}%
+
+  \begin{itemize}
+  \item programs are lists of instructions
+
+  \begin{center}
+  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
+  @{text "I"} & $::=$  & @{term "Goto L\<iota>"}
+  & \textcolor{black!60}{jump to instruction @{text L}}\\[1mm]
+  & $\mid$ & @{term "Inc R\<iota>"} & \textcolor{black!60}{increment register @{text "R"} by one}\\[1mm]
+  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & \textcolor{black!60}{if content of @{text R} is non-zero,}\\
+  & & & \textcolor{black!60}{then decrement it by one}\\
+  & & & \textcolor{black!60}{otherwise jump to instruction @{text L}}
+  \end{tabular}
+  \end{center}
+  \end{itemize}
+
+  \only<2->{
+  \begin{textblock}{4}(0.3,4.2)
+  \begin{tikzpicture}
+  \node[ellipse callout, fill=red] at (0, 0){\textcolor{yellow}{Spaghetti Code!}};
+  \end{tikzpicture}
+  \end{textblock}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Register Machines}%
+  \frametitle{Recursive Functions}%
 
   \begin{itemize}
-  \item instructions
-
+  \item[] 
   \begin{center}
-  \begin{tabular}{rcl@ {\hspace{10mm}}l}
-  @{text "I"} & $::=$  & @{term "Inc R\<iota>"} & increment register @{text "R"} by one\\
-  & $\mid$ & @{term "Dec R\<iota> L\<iota>"} & if content of @{text R} is non-zero,\\
-  & & & then decrement it by one\\
-  & & & otherwise jump to instruction @{text L}\\
-  & $\mid$ & @{term "Goto L\<iota>"} & jump to instruction @{text L}
+  \begin{tabular}{@ {}rcl@ {\hspace{8mm}}l}
+  @{text "rec"} & $::=$  & @{term "Z"} & \textcolor{black!60}{zero-function}\\[1mm]
+  & $\mid$ & @{term "S"} & \textcolor{black!60}{successor-function}\\[1mm]
+  & $\mid$ & @{term "id n m"} & \textcolor{black!60}{projection}\\[1mm]
+  & $\mid$ & @{term "Cn n f gs"} & \textcolor{black!60}{composition}\\[1mm]
+  & $\mid$ & @{term "Pr n f g"} & \textcolor{black!60}{primitive recursion}\\[1mm]
+  & $\mid$ & @{term "Mn n f"} & \textcolor{black!60}{minimisation}
   \end{tabular}
-  \end{center}
+  \end{center}\bigskip
+
+  \item @{text "eval :: rec \<Rightarrow> nat list \<Rightarrow> nat"}\\ 
+  can be defined by simple recursion\\ (HOL has @{term "Least"})
+  
+  \item \small you define
+  \begin{itemize}
+  \item addition, multiplication, logical operations, quantifiers\ldots
+  \item coding of numbers (Cantor encoding), UTM
+  \end{itemize}
 
   \end{itemize}
+  
 
   \end{frame}}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
@@ -241,14 +391,14 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
-  \frametitle{Copy Turing Machines}%
+  \frametitle{Copy Turing Machine}%
 
   \begin{itemize}
-  \item TM that copies a number on the input tape
+  \item TM that copies a number on the input tape\smallskip
 
 
   \begin{center}
-\begin{tikzpicture}[scale=0.7]
+  \begin{tikzpicture}[scale=0.7]
   \node [anchor=base] at (2.2,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (5.6,0.1) {\small$\Rightarrow$};
   \node [anchor=base] at (10.5,0.1) {\small$\Rightarrow$};
@@ -331,6 +481,7 @@
   \footnotesize
   \begin{center}
   \begin{tabular}{@ {\hspace{-8mm}}c@ {\hspace{2mm}}c@ {\hspace{2mm}}c}
+  \multicolumn{3}{@ {\hspace{-8mm}}l}{\small@{text "copy \<equiv> cbegin ; cloop ; cend"}}\\[4mm]
   \begin{tabular}[t]{@ {}l@ {}}
   @{text cbegin} @{text "\<equiv>"}\\
   \hspace{2mm}@{text "["}@{text "(W\<^bsub>0\<^esub>, 0), (R, 2), (R, 3),"}\\
@@ -371,7 +522,7 @@
   \frametitle{Hoare Logic for TMs}%
 
   \begin{itemize}
-  \item Hoare-triples and Hoare-pairs:
+  \item Hoare-triples\onslide<2>{ and Hoare-pairs:}
 
   \small
   \begin{center}
@@ -384,12 +535,14 @@
   \hspace{7mm}@{text "is_final (steps (1, tp) p n)"} \hspace{1mm}@{text "\<and>"}\\
   \hspace{7mm}@{text "Q holds_for (steps (1, tp) p n)"}
   \end{tabular} &
+
+  \onslide<2>{
   \begin{tabular}[t]{@ {}l@ {}}
   \colorbox{mygrey}{@{thm (lhs) Hoare_unhalt_def}} @{text "\<equiv>"}\\[1mm]
   \hspace{5mm}@{text "\<forall>"}@{term "tp"}.\\ 
   \hspace{7mm}if @{term "P tp"} holds then\\
   \hspace{7mm}@{text "\<forall>"}@{term n}. @{text "\<not> is_final (steps (1, tp) p n)"}
-  \end{tabular}
+  \end{tabular}}
   \end{tabular}
   \end{center}
 
@@ -399,6 +552,108 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
 *}
 
+(*<*)
+lemmas HR1 = 
+  Hoare_plus_halt[where ?S.0="R\<iota>" and ?A="p\<^isub>1" and B="p\<^isub>2"]
+
+lemmas HR2 =
+  Hoare_plus_unhalt[where ?A="p\<^isub>1" and B="p\<^isub>2"]
+(*>*)
+
+text_raw {*
+  \definecolor{mygrey}{rgb}{.80,.80,.80}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
+  \frametitle{Some Derived Rules}%
+  \large
+  
+  \begin{center}
+  @{thm[mode=Rule] Hoare_consequence}\bigskip\bigskip\\
+  
+  \begin{tabular}{@ {\hspace{-5mm}}c@ {\hspace{4mm}}c@ {}}
+  $\inferrule*
+  {@{thm (prem 1) HR1} \\ @{thm (prem 2) HR1}}
+  {@{thm (concl) HR1}}
+  $ &
+  $
+  \inferrule*
+  {@{thm (prem 1) HR2} \\ @{thm (prem 2) HR2}}
+  {@{thm (concl) HR2}}
+  $
+  \end{tabular}
+  \end{center}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[t]
+  \frametitle{Undecidability}%
+
+  \begin{center}
+  @{thm tcontra_def}
+  \end{center}
+  
+  \only<2>{
+  \begin{itemize}
+  \item Suppose @{text H} decides @{text contra} called with code 
+  of @{text contra} halts, then\smallskip
+
+  \begin{center}\small
+  \begin{tabular}{@ {}l@ {}}
+  \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
+  @{term "P\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "P\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "P\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <0::nat>)"}
+  \end{tabular}\bigskip\bigskip
+  \\
+  \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
+  $\inferrule*{
+    \inferrule*{@{term "{P\<^isub>1} tcopy {P\<^isub>2}"} \\ @{term "{P\<^isub>2} H {P\<^isub>3}"}}
+    {@{term "{P\<^isub>1} (tcopy |+| H) {P\<^isub>3}"}}
+    \\ @{term "{P\<^isub>3} dither \<up>"}
+   }
+   {@{term "{P\<^isub>1} tcontra \<up>"}}
+  $
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+  \end{itemize}}
+  \only<3>{
+  \begin{itemize}
+  \item Suppose @{text H} decides @{text contra} called with code 
+  of @{text contra} does \emph{not} halt, then\smallskip
+
+  \begin{center}\small
+  \begin{tabular}{@ {}l@ {}}
+  \begin{tabular}[t]{@ {\hspace{-5mm}}l@ {}}
+  @{term "Q\<^isub>1 \<equiv> \<lambda>tp. tp = ([]::cell list, <code_tcontra>)"}\\
+  @{term "Q\<^isub>2 \<equiv> \<lambda>tp. tp = ([Bk], <(code_tcontra, code_tcontra)>)"}\\
+  @{term "Q\<^isub>3 \<equiv> \<lambda>tp. \<exists>k. tp = (Bk \<up> k, <1::nat>)"}
+  \end{tabular}\bigskip\bigskip
+  \\
+  \begin{tabular}[b]{@ {\hspace{20mm}}l@ {}}
+  $\inferrule*{
+    \inferrule*{@{term "{Q\<^isub>1} tcopy {Q\<^isub>2}"} \\ @{term "{Q\<^isub>2} H {Q\<^isub>3}"}}
+    {@{term "{Q\<^isub>1} (tcopy |+| H) {Q\<^isub>3}"}}
+    \\ @{term "{Q\<^isub>3} dither {Q\<^isub>3}"}
+   }
+   {@{term "{Q\<^isub>1} tcontra {Q\<^isub>3}"}}
+  $
+  \end{tabular}
+  \end{tabular}
+  \end{center}
+  \end{itemize}}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
 text_raw {*
   \definecolor{mygrey}{rgb}{.80,.80,.80}
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -445,6 +700,24 @@
   %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
   \mode<presentation>{
   \begin{frame}[c]
+  \frametitle{Midway Conclusion}%
+
+  \begin{itemize}
+  \item feels awfully like reasoning about machine code
+  \item compositional constructions / reasoning
+  \item sizes
+  
+  \end{itemize}
+
+  \end{frame}}
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%     
+*}
+
+
+text_raw {*
+  %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+  \mode<presentation>{
+  \begin{frame}[c]
   \frametitle{Recursive Functions}%
 
   \begin{itemize}
@@ -503,4 +776,5 @@
 
 (*<*)
 end
+end
 (*>*)
\ No newline at end of file
diff -r 42f2c28d1ce6 -r fa021a0c6984 slides2.pdf
Binary file slides2.pdf has changed