--- 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