\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.0cm}}\vss}\strut}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-4em}$}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large the Poincar\'e principle \green{versus} reduction in the logic}

\red{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

\blue{Types 2006} \\
University of Nottingham \\
2006 04 19, 14:00
\adviembed{xvieww /home/freek/talks/poincare/witnesses.jpg}
\end{slide}

\begin{slide}
\sectiontitle{advertisement}
\slidetitle{Logic Colloquium 2006}
\red{Nijmegen, July 27$\,$--$\;$August 2}
\hfill \green{\url{http://www.cs.ru.nl/lc2006/}$\!$}
\smallskip
\adviwait

\begin{itemize}
\item[$\bullet$]
\textbf{tutorials}

\textsl{Rodney Downey}, {algorithmic randomness and computability} \\
\textsl{Ieke Moerdijk}, {introduction to algebraic set theory} \\
\textsl{Boban Velickovic}, {forcing axioms}
\adviwait

\item[$\bullet$]
\textbf{special sessions}

\blue{computability theory} / \blue{computer science logic} / \blue{model theory}\\
/ \blue{proof theory \& type theory} / \blue{set theory}

\item[$\bullet$]
\textbf{14 plenary talks} \& many \textbf{contributed talks}
\adviwait

\item[$\bullet$]
\textbf{plenary} `{100th birthday}' \textbf{discussion} on \red{G\"odel's legacy}

\end{itemize}

\vspace{-5pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{my discussion with Henk}
\slidetitle{the Poincar\'e principle}
\vspace{-\bigskipamount}
\vbox to 0pt{
\vspace{-.2cm}
\hbox to \hsize{\hfill\includegraphics[height=3.2cm]{/home/freek/talks/poincare/face.eps}\hspace{0cm}}
\vss
}
$$\adviwait\medskip\mbox{\large$\red{\vdash\, 2 + 2 = 4}$}\adviwait\hspace{3cm}$$

\begin{flushleft}\rightskip=3cm plus .5cm
Ce n'est pas une d\'emonstration proprement dite, c'est une v\'erification.$\;$ {\dots} La v\'erification diff\`ere pr\'ecis\'ement de la v\'eritable d\'emonstration, parce qu'elle est purement analytique.
\end{flushleft}
\begin{flushright}\rightskip=3.2cm
\green{
---Henri Poincar\'e, La Science et l'Hypoth\`ese
}
\end{flushright}
\adviwait
\medskip

\begin{flushleft}\rightskip=3cm plus .5cm
\gray{
This is not a demonstration properly so called; it
is a verification.$\;$ {\dots} Verification differs from proof precisely because it is analytical.
}
\end{flushleft}
\begin{flushright}\rightskip=3.2cm
\gray{
---Henri Poincar\'e, \rlap{Science and Hypothesis}\phantom{La Science et l'hypoth\`ese}
}
\end{flushright}

\vspace{-2.5em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{logics for formalized mathematics}
\vspace{-2.2\bigskipamount}
\ 
\vbox to 0pt{
\small
\vbox to .3\baselineskip{
\vspace{.3\baselineskip}
\rlap{\textsl{\hspace{4.1cm}\advirecord{b0}{\red{top 100}}%
\hspace{.6cm}\advirecord{d1}{reduction in the logic}%
\hspace{.45cm}\advirecord{d2}{{Poincar\'e}}}}
\vss
}
\vspace{-.2cm}
\begin{itemize}
\def\x{\hspace{3.9cm}}
\def\y{\hspace{6.3cm}}
\def\z{\hspace{8.95cm}}
\item[$\bullet$]
\textbf{type theory} \\
\advirecord{c1}{\rlap{Coq}}\advirecord{b1}{\rlap{\x\red{31}}}\advirecord{d3}{\rlap{\y$+$}\rlap{\z$+$}} \\
\advirecord{c2}{\rlap{NuPRL}}\advirecord{b2}{\rlap{\x\red{\hspace{.48em}8}}}\advirecord{d4}{\rlap{\y$+$}\rlap{\z$+$}} \\
\advirecord{c3}{\rlap{Agda}}\advirecord{d5}{\rlap{\y$+$}\rlap{\z$+$}} \\
\advirecord{c4}{\rlap{Plastic}}\advirecord{d6}{\rlap{\y$+$}\rlap{\z$+$}}

\item[$\bullet$]
\textbf{higher order logic} \\
\advirecord{c5}{\rlap{HOL Light}}\advirecord{b3}{\rlap{\x\red{{62}}}}\advirecord{d7}{\rlap{\y$-$}\rlap{\z$+$}} \\
\advirecord{c6}{\rlap{Isabelle/{\small HOL}}}\advirecord{b4}{\rlap{\x\red{{33}}}}\advirecord{d8}{\rlap{\y$-$}\rlap{\z$+$}} \\
\advirecord{c7}{\rlap{ProofPower}}\advirecord{b5}{\rlap{\x\red{{36}}}}\advirecord{d9}{\rlap{\y$-$}\rlap{\z$+$}} \\
\advirecord{c8}{\rlap{PVS}}\advirecord{d10}{\rlap{\y$-$}\rlap{\z$+$}}

\item[$\bullet$]
\textbf{set theory} \\
\advirecord{c9}{\rlap{Mizar}}\advirecord{b6}{\rlap{\x\red{30}}}\advirecord{d11}{\rlap{\y$-$}\rlap{\z$-$}} \\
\advirecord{c10}{\rlap{Isabelle/{\small ZF}}}\advirecord{d12}{\rlap{\y$-$}\rlap{\z$+$}} \\
\advirecord{c11}{\rlap{B method}}\advirecord{d13}{\rlap{\y$-$}\rlap{\z$-$}}
\adviwait
\adviplay{c1}
\adviplay{c2}
\adviplay{c3}
\adviplay{c4}
\adviwait
\adviplay{c5}
\adviplay{c6}
\adviplay{c7}
\adviplay{c8}
\adviwait
\adviplay{c9}
\adviplay{c10}
\adviplay{c11}
\adviwait

\item[\gray{$\bullet$}]
\gray{\textbf{{higher order set theory}} \\
\rlap{Isabelle/{\small HOLZF}}\advirecord{d14}{\rlap{\y$-$}\rlap{\z$+$}}}

\end{itemize}
\vss
}
\adviwait
\adviplay{d1}
\adviplay{d2}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviplay{d6}
\adviplay{d7}
\adviplay{d8}
\adviplay{d9}
\adviplay{d10}
\adviplay{d11}
\adviplay{d12}
\adviplay{d13}
\adviplay{d14}
\adviwait
\adviplay{b0}
\adviplay{b1}
\adviplay{b2}
\adviplay{b3}
\adviplay{b4}
\adviplay{b5}
\adviplay{b6}
\adviplay[slidegreen]{d2}
\vfill
\end{slide}

\begin{slide}
\slidetitle{type theory without reduction}
\red{$\lambda P$} = LF

$${\Gamma \vdash \red{a} : A \qquad \gray{\Gamma \vdash A' : s} \strut\over\strut \Gamma \vdash \red{a} : A'} \rlap{$\;\;\;\green{A =_{\beta} A'}$}\bigskip\adviwait$$

\red{$\lambda F$}

\green{\textbf{explicit} conversions}

$${\Gamma \vdash \red{a} : A \qquad \green{\Gamma \vdash \red{H} : A = A'} \strut\over\strut \Gamma \vdash \red{a^{\red{H}}} : A'}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{does the four color theorem need type theory?}
\red{Georges Gonthier, late 2004} \\
full {formalization} of the proof of the \red{four color theorem} in {Coq}
\adviwait
\medskip

the core of the proof is a large {functional program}
\medskip

\begin{center}
{\texttt{refl\char`\_equal true\ :\ (\green{check\char`\_reducible} \textsf{\textsl{cf}}) = true}}
\end{center}
\adviwait
\bigskip

\begin{tabular}{rl}
\textsl{Georges$\,$:} & the use of {type theory was \textbf{essential}} \\
\noalign{\vspace{-\smallskipamount}}
& (this only could have been done in Coq) \adviwait\\
\noalign{\vspace{-\smallskipamount}}
\textsl{Henk$\,$:} & \textsl{{\dots}\ because it needs {reduction inside the logic} {\dots}} \adviwait\\
\noalign{\vspace{-\smallskipamount}}
\textsl{Georges$\,$:} & no, the use of reduction in the logic is {\textbf{not} essential} \\
\noalign{\vspace{-\smallskipamount}}
& (it only makes things run a bit faster) \adviwait\\
\noalign{\vspace{-.7\smallskipamount}}
\textsl{me$\,$:} & \blue{{???}}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{programs for set theory}
\slidetitle{while programs for ZF}
\green{Tucker \& Zucker:} \\ `while programs' over an {arbitrary many-sorted algebra}
\adviwait
\bigskip

\blue{proposal: add new kind of definition to set theory} \\
\red{`{while programs}' over the set theoretic universe $V$}
\adviwait

-- old-fashioned imperative programs \\
-- all variables hold untyped ZF sets
\adviwait
\bigskip

\blue{possibility to actually execute program: not an issue} \\
\adviwait
but: \textbf{some} programs will be executable!

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}
\begin{quote}\small
\textbf{func} \green{leastfixedpoint}($f$) \\
\textbf{begin} \\
\strut\quad \textbf{var} $X$ := {emptyset}, $X'$; \\
\strut\quad \textbf{while} true \textbf{do} \\
\strut\quad \quad $X'$ := {apply}($f$,$X$); \\
\strut\quad \quad \textbf{if} \advirecord{a}{$X'$ == $X$}\adviplay{a} \textbf{then} \textbf{break} \textbf{fi}; \\
\strut\quad \quad $X$ := $X'$ \\
\strut\quad \textbf{od}; \\
\strut\quad \textbf{return} $X$ \\
\textbf{end};
\end{quote}
\adviwait
\adviplay[slidered]{a}

\vfill
\end{slide}

\begin{slide}
\slidetitle{transfinite loops}
\red{possibility to loop `beyond' omega}
\bigskip
\adviwait

value of the variable $x$ at iteration $\gamma$ we call $x_{\gamma}$

$$x_{\alpha} \;:=\; \bigcup_{\beta < \alpha}\; \bigcap_{\beta < \gamma < \alpha} x_{\gamma}\bigskip\adviwait$$

\gray{or, alternatively}
$$\gray{x_{\alpha} \;:=\; \bigcap_{\beta < \alpha}\; \bigcup_{\beta < \gamma < \alpha} x_{\gamma}}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{experimenting with HOL Light}
\slidetitle{evaluation by rewriting}
\begingroup
\def\\{\char`\\}%
\def\x{$\,$}%
\begin{alltt}\small
\gray{#} {\adviwait}let PLUS = \red{define}\hfill\green{(* \textsf{`\x}\red{Fixpoint}\textsf{\x'} *)}
  \blue{`(!m. plus 0 m = m) /\\
   (!n m. plus (SUC n) m = SUC (plus n m))`};;\smallskip\adviwait
\gray{val PLUS : thm =
  |- (!m. plus 0 m = m) /\\
     (!n m. plus (SUC n) m = SUC (plus n m))}\smallskip
\gray{#} \adviwait\blue{\red{REWRITE_CONV[PLUS]} `plus (SUC (SUC 0)) (SUC (SUC 0))`}
\hfill\green{(* \textsf{`\x}\red{Eval compute in}\textsf{\x'} *)}\rlap{;;}\adviwait
\gray{val it : thm =
  |- plus (SUC (SUC 0)) (SUC (SUC 0)) =
     \green{SUC (SUC (SUC (SUC 0)))}}\smallskip
\gray{#} 
\end{alltt}
\endgroup

\vfill
\end{slide}

\begin{slide}
\slidetitle{programs should not have to terminate!}
\begingroup
\def\\{\char`\\}
\begin{alltt}\small
let COLLATZ = new_definition
  `\blue{COLLATZ} = \red{Y} \\\green{COLLATZ} n.
     if n = 1 then 0 else
       let n' = if EVEN n then n DIV 2 else 3*n + 1 in
       \green{COLLATZ} n' + 1`;;
\end{alltt}
\adviwait

\begin{alltt}\small
let COLLATZ =
  `\blue{COLLATZ} =
     (DO \\x. x,0) SEQ
     (\red{WHILE} (\\(x,n). ~(x = 1))
       ((DO \\(x,n). x,(n + 1)) SEQ
        (\red{IF} (\\(x,n). EVEN x)
           (DO \\(x,n). (x DIV 2),n)
           (DO \\(x,n). (3*x + 1),n)))) SEQ
     (RETURN \\(x,n). n)`;;
\end{alltt}
\endgroup

\vspace{-5pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{evaluation by C compiler}
importing \green{external computations} through an \red{extra proof rule} \adviwait{\dots}\\
\strut\quad {\dots} that is \red{conservative} over the existing logic
\adviwait
\vbox to 0pt{
\vspace{.15cm}
\begin{center}
\thinlines
\begin{picture}(100,75)
\put(-15,80){\makebox(0,0)[l]{\textsl{\blue{reduction in the logic:}}}}\footnotesize
\put(0,0){\framebox(100,60){}}
\put(100,63){\makebox(0,0)[br]{kernel}}
\gray{
\put(5,5){\framebox(90,43){}}
\put(95,50){\makebox(0,0)[br]{logic}}
}
\green{\put(25,10){\framebox(50,15){\strut conversion}}}
\end{picture}
\hspace{2cm}
\begin{picture}(100,75)
\put(-15,80){\makebox(0,0)[l]{\textsl{\blue{evaluation by rewriting:}}}}\footnotesize
\put(0,20){\framebox(100,40){}}
\put(100,63){\makebox(0,0)[br]{kernel}}
\gray{
\put(5,25){\framebox(90,23){}}
\put(95,50){\makebox(0,0)[br]{logic}}
}
\green{\put(25,0){\framebox(50,15){\strut rewriting}}}
\end{picture}
\\
\vspace{.7cm}
\adviwait
\begin{picture}(100,75)
\put(-15,80){\makebox(0,0)[l]{\textsl{\blue{external evaluation:}}}}\footnotesize
\put(0,0){\framebox(100,60){}}
\put(100,63){\makebox(0,0)[br]{kernel}}
\gray{
\put(5,25){\framebox(90,23){}}
\put(95,50){\makebox(0,0)[br]{logic}}
}
\green{\put(25,5){\framebox(50,15){\strut external}}}
\end{picture}
\hspace{.2cm}\strut
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{conclusion}
\slidetitle{should reduction be built into the logic?}

logics with a natural notion of computation
\begin{itemize}
\item[$\bullet$]
beautiful\adviwait
\item[$\bullet$]
\green{complex}\adviwait
\begin{itemize}
\item[]
\gray{(`is ZF a hack?')}
\end{itemize}
\end{itemize}
\bigskip
\adviwait

can one afford \textbf{not} to have computation in the logic?\adviwait
\begin{itemize}
\item[]
\begin{itemize}
\item[]
slowdown by a \red{constant factor}
\item[]
\gray{(trading {speed} for {simplicity})}
\end{itemize}
\end{itemize}
my answer: \blue{yes!}

\vfill
\end{slide}

\end{document}