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

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.55,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}{#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}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large partial functions \& domain conditions}

Freek Wiedijk \& Jan Zwanenburg \\
University of Nijmegen

TPHOLs 2003 \\
Rome

2003 09 11, 09:30
\end{slide}

\begin{slide}
\sectiontitle{the context}
\slidetitle{proof checking of mathematics}
\vspace{-\bigskipamount}
$$
\begin{array}{c}
\mbox{\advirecord{c1}{Metamath}\adviplay{c1}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{c2}{Agda}\adviplay{c2}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{a1}{Coq}\adviplay{a1}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{a2}{NuPRL}\adviplay{a2}}
\end{array}
$$
\vspace{-1.2em}
$$
\phantom{\left.\right\rbrace\begin{array}{l}\mbox{\textbf{no partial functions}}\end{array}}\left.%
\advirecord{b1}{\llap{{$\begin{array}{c}\mbox{serious}\vspace{-\medskipamount}\\\mbox{mathematical}\vspace{-\medskipamount}\\\mbox{libraries}\end{array}\to\qquad$}}}%
\begin{array}{c}
\mbox{\advirecord{a3}{Mizar}\adviplay{a3}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{a4}{Isabelle}\adviplay{a4}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{a5}{HOL}\adviplay{a5}}
\end{array}
\advirecord{b2}{\right\rbrace\begin{array}{l}\mbox{no empty types}\vspace{-\smallskipamount}\\\advirecord{b3}{\mbox{\textbf{no partial functions}}}\end{array}}
$$
\vspace{-1.2em}
$$
\begin{array}{c}
\mbox{\advirecord{a6}{PVS}\adviplay{a6}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{a7}{IMPS}\adviplay{a7}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{c3}{ACL2}\adviplay{c3}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{c4}{Theorema}\adviplay{c4}}\vspace{-\smallskipamount} \\
\mbox{\advirecord{c5}{Otter}\adviplay{c5}}
\end{array}
$$
\adviwait
\adviplay[slidegray]{c1}
\adviplay[slidegray]{c2}
\adviplay[slidegray]{c3}
\adviplay[slidegray]{c4}
\adviplay[slidegray]{c5}
\adviplay{b1}
\adviwait
\adviplay{a1}
\adviplay{a2}
\adviplay{a3}
\adviplay{a4}
\adviplay{a5}
\adviplay{a6}
\adviplay{a7}
\adviplay[white]{b1}
\adviplay[slidered]{a3}
\adviplay[slidered]{a4}
\adviplay[slidered]{a5}
\adviwait
\adviplay{b2}
\adviplay[slidered]{b3}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{some partial operations in mathematics}

\begin{tabular}{lccl}
& $x/y$ && \advirecord{d1}{$y\ne 0$} \\
& $\sqrt{x}$ && \advirecord{d2}{$x\ge 0$} \\
& $\tan{x}$ && \advirecord{d3}{$\exists n.\; n\pi - {\pi\over 2} < x < n\pi + {\pi\over 2}$} \\
& $\displaystyle\lim_{x\to a} f(x)$ && \advirecord{d4}{$f$ is continuous in $a$} \medskip\\
& $\displaystyle\int_a^b f(x)\,dx$ && \advirecord{d5}{$f$ is integrable on $[a,b]$} \bigskip
\adviwait
\adviplay{d1}
\adviplay{d2}
\adviplay{d3}
\adviplay{d4}
\adviplay{d5}
\adviwait \\
\rlap{\blue{function application in set theory}}\qquad \vspace{-\smallskipamount}\\
\rlap{(Mizar, Isabelle/ZF, Metamath, B method)}\qquad \smallskip\\
& $\advirecord{d7}{f}(\advirecord{d8}{x})$\adviplay[slidered]{d7}\adviplay[slidered]{d8}\adviwait
%\adviplay{d7}\adviplay{d8}
&& \red{$f$} is a function $\land$ \advirecord{d6}{\quad$\leftarrow$ set of pairs} \vspace{-\smallskipamount}\\
&&& $\red{x}\in \mathop{\mbox{dom}} \red{f}$ %\\
%\adviwait
%\adviplay[slidegreen]{d6}
%\adviwait
%& $\mathop{\mbox{dom}} f$ && $f$ is a relation
\end{tabular}
%\vspace{-1em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{partial functions \& proof assistants}
\slidetitle{\textbf{approach I:} making all functions total}
\green{give each partial function a convenient value
outside its domain}
\adviwait

approach used by ACL2 \hfill\hfill \red{1/0 = 0 \quad (car nil) = nil} \hfill\strut \\
\adviwait
approach possible in all systems %\\
%\adviwait
%\quadskip (but not constructively!)
\adviwait
\medskip

\blue{disadvantages:} \\
not faithful to actual mathematics \\
the need to remember `special cases'
\adviwait
\medskip

\textbf{example}
$$\advirecord{z}{\tan\pi = 0 = {1\over 1 - \advirecord{z1}{0}} - {1\over 1 + \advirecord{z2}{0}} = {1\over 1 - \advirecord{z3}{\tan{\pi\over 2}}} - {1\over 1 + \advirecord{z4}{\tan{\pi\over 2}}}}$$
\adviplay{z}
\adviplay[slidered]{z1}
\adviplay[slidered]{z2}
\adviplay[slidered]{z3}
\adviplay[slidered]{z4}
\adviwait
\adviplay[white]{z}
\adviplay[white]{z1}
\adviplay[white]{z2}
\adviplay[white]{z3}
\adviplay[white]{z4}
\vspace{-3.14\bigskipamount}
$$
\rlap{$\displaystyle \red{\tan{\textstyle{\pi\over 2}} = 0} \ne -{1\over 2} = \red{0} - {1\over 2} = \red{1\over 0} - {1\over 2} = {1\over 1 - \tan{\pi\over 4}} - {1\over 1 + \tan{\pi\over 4}}$}
\phantom{\tan\pi = 0 = {1\over 1 - 0} - {1\over 1 + 0} = {1\over 1 - \tan{\pi\over 2}} - {1\over 1 + \tan{\pi\over 2}}}
$$

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

\begin{slide}
\slidetitle{\textbf{approach II:} undefined behavior outside domain}
\green{give each partial function some arbitrary value outside its domain} \\
\red{`$1/0$ is some real number, but we can't prove which one'}
\adviwait

approach used by HOL, Isabelle, Mizar
\adviwait
\medskip

\blue{disadvantages:} \\
not faithful to actual mathematics \\
not possible to state that the meaning of an expression is `known'
\adviwait
\medskip

\textbf{example}
$$\tan 2\theta = {1\over 1 - \tan\theta} - {1\over 1 + \tan\theta}:\quad
\mbox{truth value is \red{unknown} for $\theta = {\pi\over 2}$}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{approach III:} using the type system \advirecord{e1}{\hfill $\leftarrow$ this talk}}
%\adviwait
\adviplay[slidegray]{e1}%
\adviwait
\green{encode the domain of the partial function in its type \\
make application outside that domain a type error}
\adviwait

approach used by Coq, PVS
\adviwait
\medskip

\blue{disadvantages:} \\
complicates logic \\
doing type-related proofs is extra work
\adviwait
\medskip

\textbf{example} \\
Coq: division and $\tan$ both get an extra `proof' argument
$$\tan_{\red{H_1}} 2\theta = 1/\!_{\red{H_4}}(1 - \tan_{\red{H_2}}\theta) - 1/\!_{\red{H_5}}(1 + \tan_{\red{H_3}}\theta)$$
\adviwait
PVS: proofs don't occur explicitly in the terms (\red{TCCs})

\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{approach IV:} having a true logic of partial terms}
approach used by LCF, IMPS
\adviwait
\medskip

\blue{disadvantages:} \\
complicates logic \\
\green{how to deal with equality of undefined terms}: $\displaystyle {1/0} \mathrel{{=}} {1/0}\,$? \\
%\adviwait
\quadskip different kinds of equality? \\
%\adviwait
\quadskip undefined truth values?
\adviwait
\medskip

\textbf{examples}
$$\tan\theta \,\mathord{\red{\downarrow}} \mathrel{\Leftrightarrow} \exists n.\; n\pi - {\pi\over 2} < \theta < n\pi + {\pi\over 2}$$
%\adviwait
$$\tan 2\theta \mathrel{\red{\sqsupseteq}} {1\over 1 - \tan\theta} - {1\over 1 + \tan\theta}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{the importance of first order logic}
two reasons to want a system based on \red{total first order predicate logic}
\adviwait
\begin{itemize}
\item[$\bullet$]
\textbf{best known}

easier for users of the system
\adviwait

\item[$\bullet$]
\textbf{prover technology}

\blue{Otter, Spass, Gandalf, Vampire, Bliksem, Waldmeister,\\{\small E-SETHEO}, {\small DCTP}, etc.}

\end{itemize}
\adviwait
\medskip

this talk: how to have \green{approach III} and \red{total FOL} at the same time \vspace{-.5\smallskipamount} \\
\green{
\strut\hspace{12em}\hbox to 0pt{\hss $\uparrow$\hss} \vspace{-2.6\smallskipamount} \\
\strut\hspace{12em}\hbox to 0pt{\hss $|$\hss} \vspace{-.8\smallskipamount} \\
\strut\hspace{12em}\hbox to 0pt{\small\hss \llap{`}applying a partial function\hss} \vspace{-1.5\smallskipamount} \\
\strut\hspace{12em}\hbox to 0pt{\small\hss outside its domain is a type error\rlap{'}\hss}
}

\vfill
\end{slide}

\def\DC{{\cal DC}}
\let\phi=\varphi

\begin{slide}
\slidetitle{the goal}
the user gives for each partial function $f$ a \green{\textbf{domain predicate}} $D_f$
\begin{eqnarray*}
%D_+(x,y) \quad\!\Leftrightarrow\!\quad D_-(x,y) &\Leftrightarrow& \green{\top} \\
D_/(x,y) &\Leftrightarrow& \green{y\ne 0} \\
D_{\tan}(\theta) &\Leftrightarrow& \green{\exists n.\; n\pi - {\pi\over 2} < \theta < n\pi + {\pi\over 2}}
\adviwait
\end{eqnarray*}
the system calculates for each formula \red{\textbf{domain conditions}} $\DC(\phi)$
$$
\begin{array}{c}
\DC\Big({\displaystyle\tan 2\theta = {1\over 1 - \tan\theta} - {1\over 1 + \tan\theta}}\Big) = \qquad\qquad \medskip\\
\displaystyle
\hspace{-1em} \Big\{ \vdash \red{\exists n.\; n\pi - {\pi\over 2} < 2\theta < n\pi + {\pi\over 2}}\,,\;
\vdash \red{\exists n'.\; n'\pi - {\pi\over 2} < \theta < n'\pi + {\pi\over 2}}\,,\; \hfill \\
\hfill \vdash \red{\tan\theta\ne 1}\,,\; \vdash \red{\tan\theta\ne -1} \,\Big\} \hspace{-1em}
\end{array}
\adviwait
$$

{the system uses \textbf{total FOL} to infer formulas and domain conditions} \\
(during steps in the proofs it may reason about $1/0$)

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

\def\IF{\textbf{if}\;}
\def\THEN{\;\textbf{then}\;}
\def\ELSE{\;\textbf{else}\;}

\begin{slide}
\sectiontitle{three logical systems}
\slidetitle{\textbf{system T:} the operational logic}
\green{the well-known classical first order logic with \blue{\textbf{T}}otal functions} \\
%\adviwait
\blue{24 derivation rules in the paper}
\adviwait
%\medskip
\begin{eqnarray*}
{\cal T} &::=& {x_i} \mathrel{|} \advirecord{f2}{c_i}\adviplay{f2} \mathrel{|} {f_i({\cal T},\ldots,{\cal T})} \mathrel{|} \advirecord{f1}{\IF {\cal F} \THEN {\cal T} \ELSE {\cal T}}\adviplay{f1} \\
{\cal F} &::=& {\bot} \mathrel{|} {P_i({\cal T},\dots,{\cal T})} \mathrel{|} {{\cal T} = {\cal T}} \mathrel{|} {{\cal F} \to {\cal F}} \mathrel{|} {\forall x_i.\, {\cal F}}
\end{eqnarray*}
\adviwait
\adviplay[slidered]{f1}%
\advirecord{f3}{if-then-else construction}\adviplay[slidered]{f3}
$$\IF x\ne 0 \THEN {1\over x} \ELSE 0$$
needed to make the proofs manageable
\adviwait
\smallskip

\adviplay{f1}%
\adviplay{f3}%
\adviplay[slidered]{f2}%
\red{constant symbols in the language} \\
our result doesn't hold when constants are nullary functions

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

\begin{slide}
\slidetitle{\textbf{system P:} the intended logic}
\green{logic with \blue{\textbf{P}}artial functions in type theoretical style} \\
\blue{24 derivation rules in the paper}

\adviwait
as close as possible to system T: untyped, classical, first order
\adviwait
\medskip

every function gets one extra argument:
\begin{eqnarray*}
f(x_1,\dots,x_a) &\leadsto&
\rlap{\hspace{9em}$\green{\red{\alpha} : D_f(x_1,\dots,x_a)}$}
\green{f(x_1,\dots,x_a,\red{\alpha})} \\
\noalign{\smallskip}
{\displaystyle x\over y} &\leadsto&
\rlap{\hspace{9em}$\green{\red{\alpha} : y\ne 0}$}
\green{\mbox{\rm div}(x,y,\red{\alpha})} \\
\noalign{
\adviwait
\smallskip
implications turn into a product and bind a proof variable:
\medskip
}
\forall x.\; \blue{x\ne 0} \to {1\over x}\ne 0
&\leadsto&
\green{\forall x.\; \Pi_{\red{H} : \blue{x\ne 0}}.\;\, \mbox{\rm div}(1,x,\red{H})\ne 0} \\
\noalign{\medskip}
\adviwait
\hspace{-2em}\IF x\ne 0 \THEN {\displaystyle 1\over x} \ELSE 0
&\leadsto&
\green{\IF x\ne 0 \THEN\!\!_{\,\red{H} : x\ne 0}\; \mbox{\rm div}(1,x,\red{H}) \ELSE\!\!_{\,\red{H'} : x = 0}\; 0}\hspace{-2em}
\end{eqnarray*}

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

\begin{slide}
\slidetitle{erasure of proof terms}
\green{$|\cdot|$} \quad maps system P to system T
\adviwait
\bigskip

\blue{inductively defined following the structure of the argument}
\begin{eqnarray*}
|f(t_1,\cdots,t_a,\red{\alpha})| &=& f(|t_1|,\dots,|t_a|) \\
|\Pi_{\red{H}:\phi}.\; \psi| &=& |\phi| \to |\psi| \\
|\IF \phi \THEN\!\!_{\,\red{H:\phi}}\; t \ELSE\!\!_{\,\red{H':\neg\phi}}\; u|
&=&
\IF |\phi| \THEN |t| \ELSE |u|
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\slidetitle{domain conditions}
\green{$\DC_\Gamma(\cdot)$} \quad maps a system T expression to a set of system T judgments
\adviwait
\bigskip

\blue{inductively defined following the structure of the argument}
\begin{eqnarray*}
\DC_\Gamma(f(t_1,\ldots,t_a)) &=&
\DC_\Gamma(t_1) \cup \ldots \cup \DC_\Gamma(t_a) \cup {} \\
\noalign{\vspace{-\smallskipamount}}
&& \qquad\qquad\left\{ \green{\Gamma \vdash D_f(t_1,\ldots,t_a)} \right\} \\
\noalign{
\adviwait
\medskip
}
\DC_\Gamma(\phi \to \psi) &=& \DC_\Gamma(\phi) \cup \DC_{\Gamma,\,\red{\phi}}(\psi) \\
\DC_\Gamma(\IF \phi \THEN t \ELSE u) &=&
\DC_\Gamma(\phi) \cup \DC_{\Gamma,\,\red{\phi}}(t) \cup \DC_{\Gamma,\,\red{\neg\phi}}(u)
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\slidetitle{main correspondence result}
\textbf{statement together with domain conditions provable in system T \\
\quadskip $\iff$ that statement provable in system P}
\adviwait
\bigskip

more precisely:

$\Gamma\vdash^{\sf P} \mbox{wf}$
\medskip
$$\green{\Gamma \vdash^{\sf P} \phi} \enskip\Rightarrow\enskip \red{|\Gamma| \vdash^{\sf T} |\phi|\mbox{\enskip\&\enskip}\DC_{|\Gamma|}(|\phi|)}$$
$$\red{|\Gamma| \vdash^{\sf T} \phi'\mbox{\enskip\&\enskip}\DC_{|\Gamma|}(\phi')} \enskip\Rightarrow\enskip \mbox{\large$\exists$}\,\phi\mbox{\small$\,$}.\enskip |\phi| = \phi'\mbox{\enskip\&\enskip}\green{\Gamma \vdash^{\sf P} \phi}$$

%\gray{(where $\green{\Gamma}$ is a correct system P context)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{how the proof works}
\blue{\textbf{system D}: a third system}

\green{term arguments have to stay inside the \blue{\textbf{D}}omain} \\
\red{`forbidden to reason about undefined objects'}

system T formulas \\
system P derivation rules
\adviwait
\bigskip

$\green{\,\cdot\,\mbox{\footnotesize\strut}^*}$ \quad \blue{lifting from system T to system D}

$
f(t_1,\ldots,t_a)^* \enskip\,=\,\enskip \IF D_f(t_1^*,\ldots,t_a^*) \THEN f(t_1^*,\ldots,t_a^*) \ELSE c_0
$
\adviwait
\medskip

\textbf{facts:}
%\vspace{-\medskipamount}
$$\red{\Gamma \vdash^{\sf T} \phi} \enskip\Rightarrow\enskip \green{\Gamma^* \vdash^{\sf D} \phi^*}
\adviwait
$$
$$\red{\Gamma \vdash^{\sf T} \phi} \mbox{\enskip\&\enskip} \DC(\Gamma) \mbox{\enskip\&\enskip} \DC_\Gamma(\phi) \enskip\Rightarrow\enskip \green{\Gamma\vdash^{\sf D} \phi}$$

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

\begin{slide}
\sectiontitle{conclusions}
\slidetitle{domain conditions don't respect logical equivalence!}
$$\DC(x\ne 0 \;\land\; \green{{1\over x} > 1}) \enskip\ne\enskip \DC(\green{{1\over x} > 1} \;\land\; x\ne 0)
%\adviwait
$$

\red{`left-to-right evaluation'}
%\adviwait

{$\phi \land \psi \equiv \neg(\phi \to \neg\psi)$}
%\adviwait

{$\DC_\Gamma(\phi \land \green{\psi}) = \DC_\Gamma(\phi) \cup \DC_{\Gamma,\,\red{\phi}}(\green{\psi})$}
\adviwait
\medskip
\smallskip

{strange in logic, but common in programming}:
\vspace{-\smallskipamount}
\begingroup
%\small
$$
\begin{array}{l}
\texttt{if (x != 0\ \char`\&\char`\&\ \green{1/x > 1})\ \char`\{} \vspace{-\medskipamount}\\
\texttt{\ \ }\ldots \vspace{-\medskipamount}\\
\texttt{\char`\}}
\end{array}
$$
\endgroup

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

\begin{slide}
\slidetitle{is it worth it?}
\green{proving domain conditions is extra work}

\quadskip popularity of PVS is encouraging \\
\adviwait
\quadskip \gray{it can't be worse than a total system} %\\
%\quadskip\quadskip \gray{just make all functions total\dots}
\adviwait
\bigskip

\textbf{theoretical questions}
\begin{itemize}
\item[$\bullet$]
same theory without if-then-else?
\adviwait

\item[$\bullet$]
equivalent theory for higher order logic?

%\adviwait

%\item[$\bullet$]
%equivalent theory for constructive logic?

\end{itemize}
\adviwait
\medskip

\textbf{implementation?}
\begin{center}
\red{\textbf{`partial Mizar'}}
\end{center}

\vfill
\end{slide}

\end{document}