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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.6,.6,.6}
\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}}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\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{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large convertibility proof terms}

Herman Geuvers \& \blue{Freek Wiedijk} \\
University of Nijmegen

%local seminar of the foundations group \\
%%University of Nijmegen \\
%2004 06 14, 14:00

% Fourth International
%\blue{workshop LFM'04} \\
LFM'04, IJCAR \\
Cork, Ireland \\
2004 07 05, 12:00
\end{slide}

\begin{slide}
\sectiontitle{the problem}
\slidetitle{a `proof' of the Riemann hypothesis}
\begin{quote}
\rightskip=0pt
\green{
\textbf{Theorem.} The non-trivial zeroes of Riemann's $\zeta(s)$ function
all lie on the complex line $\Re s = {1\over 2}$.
}
\adviwait

\rightskip=0pt
\green{
\textbf{Proof.} There exists a derivation of this statement with a length
less than \black{$10^{10^{100}}$} symbols (finding it is \green{left as an exercise
to the reader}).  Therefore the statement is true. \hfill $\Box$}%
\end{quote}
\adviwait
\medskip

suppose that a proof of the Riemann hypothesis will be found \\
then this is a correct proof too! \\
\red{but: is it an acceptable proof?}
\adviwait
\medskip

formalizing this proof as a Coq lambda-term is doable (using reflection)\\
\red{but: `left as an exercise to the reader' in a formal proof object?}
\vspace{-3em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{linear time proof checking?}
%proof checking \\
%\dashskip
\red{`following a proof with your finger'}
\adviwait
\bigskip

proof checking in type theory \\
{\dots}is decidable \\
{\dots}can be intractable
\adviwait
\medskip

\blue{deciding whether two terms are {convertible}} \\
\green{`convertible' $=$ equal up to beta-reductions and definitional expansions}
\adviwait
\smallskip

naive way:
fully normalize both terms and compare \\
not practical
%\adviwait
\smallskip

in practice:
\red{clever \textbf{search} for `convertibility proof'}
\vfill
\end{slide}

\begin{slide}
\slidetitle{slow checking of errors}
\begin{center}
\red{error in formalization: checking `freezes'}
\end{center}
\adviwait
\bigskip

\blue{Automath}

solution: limit on the number of reductions \\
\green{limit exceeded $\to$ probably incorrect}
\adviwait

%effectively: \green{correctness is only semi-decidable}
%\adviwait
\medskip

\blue{Coq}

solution: limit automatic definitional expansions \\
\green{definitions can be `transparent' and `opaque'}

%\green{in practice sometimes necessary} to make definitions opaque
\vfill
\end{slide}

\begin{slide}
\slidetitle{systems without convertibility checking}
\begin{center}
\begin{tabular}{lcl}
type theory &$\to$& conversion rule \\
%\adviwait
LF &$\to$& conversion rule \\
\adviwait
\red{HOL} &$\to$& no conversion rule \\
\advirecord{z1}{Isabelle/Pure} &\advirecord{z2}{$\to$}& \advirecord{z3}{no conversion rule}
\end{tabular}
\end{center}
\medskip

in \red{HOL} each beta reduction step takes an inference step \\
\green{beta rule is one of the proof rules}
\adviwait
\adviplay[slidered]{z1}
\adviplay{z2}
\adviplay{z3}
\adviwait
\medskip

\red{proof objects checkable in linear time}
$$
\left.
\begin{array}{l}
\mbox{comparing two terms} \\
\mbox{substituting a term in a term}
\end{array}
\right\}
\mbox{ unit time}
$$
\vfill
\end{slide}

\def\alt{\mathrel{|}}

\begin{slide}
\sectiontitle{the system}
\slidetitle{a logical framework with explicit conversions}
\begin{itemize}
\item[]
\textbf{judgments}
$$
\begin{array}{l}
\Gamma \vdash a : A \\
\advirecord{a3}{\Gamma \vdash \green{H} : A = B}
\end{array}
$$
\item[]
\textbf{terms}
$$
\begin{array}{lll}
T &::=& x \alt \Box \alt \mathord{*} \alt \advirecord{a5}{\Pi x{:}T}\adviplay{a5}. T \alt \advirecord{a6}{\lambda x{:}T}\adviplay{a6}. T \alt TT \adviwait \alt \green{T^H} \\
\noalign{\medskip}
\green{H} &::=& \advirecord{a4}{\beta(T)}\adviplay{a4} \alt \iota(T) \alt \\
&& \bar T \alt H^\dagger \alt H \cdot H \alt \\
&& \{H,\advirecord{a1}{[x{:}T]}\adviplay{a1}H\} \alt \langle H,\advirecord{a2}{[x{:}T]}\adviplay{a2}H\rangle \alt HH
\adviwait
\adviplay{a3}
\adviwait
\adviplay[slidered]{a4}
\adviwait
\adviplay[black]{a4}
\adviplay[slidered]{a1}
\adviplay[slidered]{a2}
\adviplay[slidered]{a5}
\adviplay[slidered]{a6}
\end{array}
$$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{derivation rules}
\begin{itemize}
\item[$\bullet$]
\blue{six} `pure type system' rules

(all the usual rules, minus the conversion rule)
\medskip
\adviwait
\item[$\bullet$]
\blue{nine} equality proof rules

(one for every equality proof term constructor,
plus \\ weakening for equality proofs)
\medskip
\adviwait
\item[$\bullet$]
our \red{conversion rule}

$${\Gamma \vdash \green{a} : A \quad \Gamma \vdash \green{H} : A = A' \over \Gamma \vdash \green{a^H} : A'}$$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{basic equality proofs}

\begin{itemize}
\item[]
\red{beta reduction} rule

$$\begin{array}{rcl}\red{\beta(}\green{(\lambda x{:}A.b)a}\red{)} &:& (\lambda x{:}A.b)a \,=\, b[x:=a]\end{array}$$
\medskip
\adviwait
\item[]
\red{John-Major} rule

$$\begin{array}{rcl}\red{\iota(}\green{a^H}\red{)} &:& a \,=\, a^H\end{array} \bigskip$$

we do not have equality for equality proofs \\
this rule allows us to interchange `equal' equality proofs

%irrelevance of proof for equality proofs
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{combining equality proofs}
\begin{itemize}
\item[]
\textbf{reflexitivity, symmetry, transitivity}
$$
\hspace{-2em}
\begin{array}{rcl}
H &:& a = b \\
H' &:& b = c
\end{array}
\quad\Rightarrow\quad
\begin{array}{rcl}
\red{\bar a} &:& a = a \\
\red{H^\dagger} &:& b = a \\
\red{H \cdot H'} &:& a = c
\end{array}
\adviwait
$$
\item[]
\textbf{equalities in contexts}
$$
\hspace{-2em}
\begin{array}{rcl}
\ \\
H &:& A = A' \\
H' &:& B = B' \\
\advirecord{b1}{H'' &:& B = B'[x':=x^H]\hspace{-2em}}
\end{array}
\;\;\Rightarrow\quad
\begin{array}{rcl}
\red{HH'} &:& AB = A'B' \\
\red{\{H,[x{:}A]\advirecord{b2}{\rlap{$H'\}$}}\advirecord{b3}{H''\red{\}}}} &:& \Pi x{:}A.B = \Pi x'{:}A'.B' \\
\red{\langle H,[x{:}A]\advirecord{b4}{\rlap{$H'\rangle$}}\advirecord{b5}{H''\red{\rangle}}} &:& \lambda x{:}A.B = \lambda x'{:}A'.B'
\adviplay[slidered]{b2}
\adviplay[slidered]{b4}
\adviwait
\adviplay[white]{b2}
\adviplay[white]{b4}
\adviplay[slidegreen]{b1}
\adviplay[slidegreen]{b3}
\adviplay[slidegreen]{b5}
\end{array}
\hss
$$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{type uniqueness}
$$\vdash a : \red{A}  \quad\&\quad \vdash a : \red{A'}  \quad\Rightarrow\quad  A \equiv A'$$

not just equal up to $\beta\delta$-equality \\
\red{identical terms} %\adviwait \green{(up to alpha renaming of bound variables)}
\medskip
\adviwait

\textbf{example}
$$
\begin{array}{rll}
F : \Pi x{:}A.B,\;\; a : A &\vdash& \!{\phantom{(}Fa\phantom{)}} : \;\rlap{$B[x:=a]$}\phantom{(\lambda x{:}A.B)a} \\
F : \Pi x{:}A.B,\;\; a : A &\not\vdash& \!{\phantom{(}Fa\phantom{)}} : \;(\lambda x{:}A.B)a \adviwait \\
%\noalign{\medskip}
F : \Pi x{:}A.B,\;\; a : A &\vdash& \!{(Fa)}^{\green{\beta((\lambda x{:}A.B)a)^\dagger}} : (\lambda x{:}A.B)a
\end{array}
$$
$$
\begin{array}{rcl}
\green{\beta((\lambda x{:}A.B)a)\phantom{{}^\dagger}} &:& (\lambda x{:}A.B)a = B[x:=a] \\
\green{\beta((\lambda x{:}A.B)a)^\dagger} &:& B[x:=a] = (\lambda x{:}A.B)a
\end{array}
$$
\vspace{-6pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Martin-L\"of type theory $\leftrightarrow$ our system}
$$
\begin{array}{rl}
\mbox{MLTT}\quad & \Gamma \vdash a = b : \green{A} \\
& \advirecord{c1}{\Gamma \vdash a = b :\green{B}} \\
\mbox{our system}\quad & \Gamma \vdash \red{H} : \advirecord{c2}{a} = \advirecord{c3}{b}
\adviplay{c2}
\adviplay{c3}
\end{array}
\medskip
\adviwait
\adviplay[slideblue]{c2}
\adviplay[slideblue]{c3}
$$
types of $\blue{a}$ and $\blue{b}$ need not be identical \\
\blue{John-Major equality}
\medskip

in our system the judgment really is something like
$$\Gamma \vdash \red{H} : (\blue{a}:\green{A}) = (\blue{b}:\green{B})$$
\adviwait
\adviplay{c1}
\vfill
\end{slide}

\begin{slide}
\slidetitle{subject reduction}
$$
\green{a \rightarrow\hspace{-.8em}\rightarrow_\beta b} \quad\&\quad \vdash a : A \quad\Rightarrow\quad \vdash b : A
%\adviwait
$$

our system \red{does not have reduction}
\medskip
\adviwait

`\blue{subject reduction}' for our system:
$$
\medskip
\vdash \green{a = b} \quad\&\quad \vdash a : A \quad\&\quad \vdash b : B \quad\Rightarrow\quad \vdash \green{A = B}
\vspace{-\medskipamount}
$$
\blue{`if two terms are convertible then their types are also convertible'}
\bigskip
\adviwait

{\black{$\;\;\vdash \green{A = B}\;\;$} means that some $\red{\,H\,}$ exists with \black{$\;\;\vdash \red{H} : \green{A = B}$}}

\vfill
\end{slide}

\begin{slide}
\slidetitle{two versions of our system}
\begin{center}
\strut\hspace{1em}\rlap{$\underbrace{\mbox{\strut\blue{\textbf{LF} = $\lambda$P} $\hspace{3em}$ \red{$\lambda$H}}}_{\hbox to 0pt{\hss\footnotesize convertibility path does not need to be type-correct\hss}}$}%
\phantom{\strut\textbf{LF} = $\lambda$P $\hspace{3em}$}
$\overbrace{\mbox{\strut\red{$\lambda$H} $\hspace{8em}$ \green{$\lambda$F}}}^{\hbox to 0pt{\hss\footnotesize explicit convertibility proof terms\hss}}$
\end{center}
\bigskip
\adviwait
$\beta((\lambda x{:}A.b)a) : (\lambda x{:}A.b)a = b[x:=a]$

$\quad$ \green{$\lambda$F:$\;\;\;$} \green{beta rule is only allowed when $\;\;\vdash a : A$} \\
$\strut\quad$ \red{$\!\lambda$H:$\;\;\;$} \red{beta rule is allowed even when the type of $a$ is `wrong'}
\bigskip
\adviwait

\green{\rlap{John-Major rule of $\lambda$F:}}\hspace{10.7em}$\green{\iota(a) : a = a^H}$ \\
\red{\rlap{John-Major rule of $\lambda$H:}}\hspace{10.7em}$\red{\iota(a) : |a| = a}$
\smallskip

\blue{$|a|\quad$ `erase all conversions from the term $a$'} \\
\adviwait
{\phantom{$|a|\quad$} is not generally a well-typed $\lambda$H-term!}
\vspace{-5pt}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the results}
\slidetitle{correspondence of our systems to LF}
\begin{itemize}
\item[$\bullet$]
\green{$\lambda$F} \quad \green{future work}
\adviwait
\item[$\bullet$]
\red{$\lambda$H}
\begin{eqnarray*}
\red{\Gamma \vdash_{\lambda{\sf H}} a : A} &\Rightarrow& \blue{|\Gamma| \vdash_{\lambda{\sf P}} |a| : |A|} \\
\noalign{\bigskip}
\adviwait
\blue{\Gamma' \vdash_{\lambda{\sf P}} a' : A'} &\Rightarrow&
\exists \Gamma\; a\; A. \;\,
\Gamma' \equiv |\Gamma| \;\land\; a' \equiv |a| \;\land\; A' \equiv |A| \;\land \\
\noalign{\vspace{-\smallskipamount}}
&&\phantom{\exists \Gamma\; a\; A. \;\,} \red{\Gamma \vdash_{\lambda{\sf H}} a : A} \\
%\noalign{\medskip}
\adviwait
\begin{array}{r}
\red{\Gamma \vdash_{\lambda{\sf H}} A : s} \;\;\land\, \\
\blue{|\Gamma| \vdash_{\lambda{\sf P}} a' : |A|}
\end{array} \!\!\!
&\Rightarrow&
\exists a.\;\, a' \equiv |a| \;\land\;\,
\red{\Gamma \vdash_{\lambda{\sf H}} a : A} \\
\end{eqnarray*}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{ephemeral proofs}

\begin{center}
\red{our systems: proof terms become much bigger}
\end{center}
\bigskip
\medskip
\adviwait

{Coq}:
`proof objects' are stored as terms in memory
\bigskip

{HOL}:
`proof objects' are \textbf{not} stored in memory
\smallskip

\green{ephemeral proof objects} \\
{computed \& checked \& garbage collected away on the fly}
\bigskip

%\begin{center}
\red{$\lambda$F/$\lambda$H implementation with ephemeral proof terms?}
%\end{center}
\vfill
\end{slide}

\end{document}