\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\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\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{-6em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large the Mizar type system}

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

\red{TPHOLs 2007} \\
University of Kaiserslautern
\smallskip

{2007\hspace{3pt}09\hspace{3pt}12, 10\hspace{.7pt}:\hspace{1pt}00}
\end{slide}

\begin{slide}
\slidetitle{this talk}
\begin{itemize}
\item[$\bullet$]
\blue{Mizar}
\medskip
\adviwait

\item[$\bullet$]
\blue{Mizar types}
\medskip
%\adviwait

\item[$\bullet$]
\blue{the paper}
\medskip

\begin{itemize}
\item
the Mizar type system in the form of \red{typing rules}
\smallskip

\item
\red{correctness} with respect to first order predicate logic

\end{itemize}

%\medskip
%{proving a type system correct}

\end{itemize}
\adviwait

\vbox to 0pt{
\hfill\includegraphics[width=7em]{/home/freek/talks/miztype/andrzej.eps}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{Mizar versus the HOLs}
\begin{center}
\begin{tabular}{rcl}
\advirecord{a3}{\textbf{Mizar}}\adviplay{a3} &$\hspace{2em}$& \textbf{HOL} \\
%\noalign{\vspace{-\smallskipamount}}
&& \green{\advirecord{a1}{\textbf{Isabelle}}}\adviplay{a1} \\
%\noalign{\vspace{-\smallskipamount}}
&& \textbf{PVS} \\
%\noalign{\vspace{-\smallskipamount}}
&& \textbf{Coq} \\
%\noalign{\vspace{-\smallskipamount}}
%&& \textbf{Matita} \\
%\noalign{\vspace{-\smallskipamount}}
%&& \textbf{NuPRL} \\
%\noalign{\vspace{-\smallskipamount}}
&& \hspace{.7em}\vdots \\
\noalign{\bigskip}
\adviwait
batch checking && interactive \\
\adviwait
first order logic && higher order logic \\
\adviwait
\green{\advirecord{a2}{readable proofs}}\adviplay{a2} && tactic scripts \\
\adviwait
\adviplay[slidegreen]{a1}
\adviplay[slidegreen]{a2}
\adviplay[slidegreen]{a3}
\adviwait
untyped set theory && typed foundations \\
\adviwait
\red{very nice type system} && $\hspace{10em}$
\adviplay[slidered]{a3}
\end{tabular}
\end{center}

\vfill
\end{slide}

%\begin{slide}
%\slidetitle{Mizar}
%\strut\vspace{5em}
%\centerline{\Large demo}
%\strut\vspace{2em}
%\centerline{\green{\texttt{lmod\_5.miz}}}
%
%\vfill
%\end{slide}

\begin{slide}
\sectiontitle{Mizar types}
\slidetitle{features}
\begin{itemize}
\adviwait
\item[\advirecord{b10}{$\bullet$}\adviplay{b10}]
\red{\advirecord{b2}{dependent types}}\adviplay{b2}
\adviwait

\item[\advirecord{b9}{$\bullet$}\adviplay{b9}]
\advirecord{b7}{
\textbf{no} types built from types
}

\green{\advirecord{b8}{\textbf{no} function types $A\to B$ for types $A$ and $B$}} \\
\adviplay{b7}\adviplay[slidegreen]{b8}
\adviwait
\green{\advirecord{b13}{(`$\mbox{\tt\small Ordinal} \to \mbox{\tt\small Ordinal}$'?)}}
\adviplay[slidegreen]{b13}
\adviwait

\item[\advirecord{b11}{$\bullet$}\adviplay{b11}]
\red{\advirecord{b3}{subtyping}}\adviplay{b3}
\adviwait

\item[\advirecord{b12}{$\bullet$}\adviplay{b12}]
\red{\advirecord{b4}{`attributes'}}\adviplay{b4}
\adviwait

\item[\advirecord{b5}{$\bullet$}\adviplay{b5}]
\gray{\advirecord{b1}{structure types (records)}}\adviplay{b1}
\adviwait
\adviplay[slidegray]{b1}
\adviplay[slidegray]{b5}
\adviwait
\blue{\advirecord{b6}{\hfill\rlap{Alternative Aggregates in Mizar}\phantom{Gilbert Lee and Piotr Rudnicki}}} \\
\advirecord{b14}{\hfill Gilbert Lee and Piotr Rudnicki} \\
\advirecord{b15}{\hfill\rlap{{\small MKM 2007}, {\small LNAI 4573}}\phantom{Gilbert Lee and Piotr Rudnicki}}%
\adviplay[slideblue]{b6}%
\adviplay{b14}%
\adviplay{b15}%
\adviwait
\adviplay[slidered]{b2}%
\adviplay[slidered]{b3}%
\adviplay[slidered]{b4}%
\adviplay[slidegray]{b6}%
\adviplay[slidegray]{b7}%
\adviplay[slidegray]{b8}%
\adviplay[slidegray]{b9}%
%\adviplay[slidered]{b10}%
%\adviplay[slidered]{b11}%
%\adviplay[slidered]{b12}%
\adviplay[slidegray]{b13}%
\adviplay[slidegray]{b14}%
\adviplay[slidegray]{b15}%

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{attributes}
\begin{center}
\lightgray{\advirecord{c1}{\tt \framebox{\tt \framebox{\black{\tt \advirecord{c2}{non} \red{\advirecord{c7}{empty}}\strut}} \framebox{\black{\tt \red{\advirecord{c3}{finite}}\strut}}} \framebox{\black{\tt {\tt \green{\advirecord{c4}{Subset}} \advirecord{c5}{of}} \advirecord{c6}{NAT}\strut}}}}
\end{center}
\adviplay{c2}
\adviplay{c7}
\adviplay{c3}
\adviplay{c4}
\adviplay{c5}
\adviplay{c6}
\adviwait
\adviplay[slidelightgray]{c1}
\vspace{-\smallskipamount}
\strut\hspace{12em}\hbox to 0pt{\hss{$\uparrow$}\hss}\hspace{9em}\hbox to 0pt{\hss{$\uparrow$}\hss} \vspace{-\smallskipamount}\\
\strut\hspace{12em}\hbox to 0pt{\hss adjectives\hss}\hspace{9em}\hbox to 0pt{\hss radix type\hss}\\\adviwait
\adviplay[slidered]{c7}%
\adviplay[slidered]{c3}%
\adviplay[slidegreen]{c4}%
\adviplay[slidegreen]{c5}%
\strut\hspace{12em}\hbox to 0pt{\hss\red{attributes}\hss}\hspace{9em}\hbox to 0pt{\hss\green{mode}\hss}
\bigskip
\adviwait

\blue{overloading}

{meaning of an attribute depends on the radix type:}
\smallskip
\begin{itemize}
\item[--]
\texttt{\red{connected} Relation}

\item[--]
\texttt{\red{connected} Graph}

\item[--]
\texttt{\red{connected} TopSpace}

\end{itemize}

\vfill
\end{slide}

\let\leftbrace=\{
\let\rightbrace=\}
\def\{{\char`\{}
\def\}{\char`\}}
\def\_{\char`\_}

\begin{slide}
\slidetitle{example}
\vspace{-1.5\bigskipamount}
\def\boxed#1#2{\advirecord{#1}{\fbox{\strut \advirecord{#1boxed}{#2}}}\adviplay{#1boxed}}
\begin{alltt}\small
definition let d be \gray{\boxed{d1}{\black{non zero Element of NAT}}};
 func cyclotomic_poly d -> \gray{\boxed{d2}{\black{Polynomial of F_Complex}}} means
   \red{\advirecord{d5}{ex s being \gray{\boxed{d3}{\red{\advirecord{d6}{non empty finite Subset of F_Complex}}}}
    st s = \{ y where y is \gray{\boxed{d4}{\red{\advirecord{d7}{Element of MultGroup F_Complex}}}} : ord y = d \} &\toolong
       it = poly_with_roots((s,1)-bag);}}\phantom{\fbox{\strut}}
end;\phantom{\fbox{\strut}}
\end{alltt}
\adviplay{d5}
\adviplay{d6}
\adviplay{d7}
\adviwait
\adviplay[slidered]{d5}
\adviplay[slidered]{d6}
\adviplay[slidered]{d7}
\adviwait
\adviplay[slidegray]{d1}
\adviplay[slidegray]{d2}
\adviplay[slidegray]{d3}
\adviplay[slidegray]{d4}
\adviwait
\vbox to 0pt{
\begin{tabular}{rl}
\texttt{{UNIROOTS}} & \green{Primitive Roots of Unity and Cyclotomic Polynomials}\toolong\\
& Broderick Arneson and Piotr Rudnicki \\
& 3293 lines, 135K \adviwait\\
\noalign{\medskip}
{full Mizar library} & 985 `articles', 1.97 million lines, 68.9M
\end{tabular}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{typings also are formulas}
\begin{center}
\begin{tabular}{c}
%\small
\texttt{for i \advirecord{e1}{being}\adviplay{e1} Integer holds i >= 0 iff \red{\advirecord{e6}{i \advirecord{e2}{is}\adviplay{e2} Nat}}\adviplay{e6}}\adviwait\\
$\forall\,i \advirecord{e3}{:}\adviplay{e3} \mathbb{Z}\,.\,\; i \ge 0 \,\Leftrightarrow\, (\,\red{\advirecord{e5}{i\advirecord{e4}{:}\adviplay{e4}\mathbb{N}}}\adviplay{e5}\;)$
\end{tabular}
\end{center}
\adviwait
\adviplay[slidered]{e5}
\adviplay[slidered]{e6}
\adviwait
\medskip
\begin{flushright}
\lightgray{\small
$\left(\hfill
\black{
\begin{tabular}{rcl}
\texttt{{i \green{is} {Nat}}} & $\ne$ & \texttt{{i \green{in} {NAT}}} \\
\noalign{\vspace{-\medskipamount}}
\hbox to 0pt{\hss\gray{$\uparrow$}\hss}$\hspace{.8em}$ && $\hspace{3.3em}$\hbox to 0pt{\hss\gray{$\uparrow$}\hss} \\
\noalign{\vspace{-\medskipamount}}
\hbox to 0pt{\hss\gray{type}\hss}$\hspace{.8em}$ && $\hspace{3.3em}$\hbox to 0pt{\hss\gray{term}\hss} \\
\green{`has {type}'} && \green{`is element of'} \\
\noalign{\vspace{-\smallskipamount}}
the type system && the set theory
\end{tabular}%
}%
\hfill\right)$
}
\end{flushright}
\bigskip
\adviwait

\blue{`coerce' a term to a more informative type by giving a proof}

\def\xdots{{\rm\dots}}
\begin{alltt}\small
\gray{\xdots
then n' - n >= 0 by XREAL_1:50;
then \blue{{reconsider} d = n' - n as Nat} by INT_1:16;
\xdots}
\end{alltt}

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

\begin{slide}
\slidetitle{subtyping}
\def\xdots{{\rm\dots}}%
\begin{alltt}\small
definition let C be Category;
  mode \green{Subcategory of C} -> \green{Category} means
\gray{:: CAT_2:def 4}
    \xdots
end;
\end{alltt}
\medskip
\adviwait

\begin{center}
\red{\texttt{set}} \\
$\uparrow$ \\
\green{\texttt{Category}} \\
$\uparrow$ \\
\green{\texttt{Subcategory of C}}
\end{center}
\bigskip
\adviwait

%{every Mizar term always also has type \red{\texttt{set}}}
%\medskip

\blue{supertype may depend on the types of the arguments of the type}

\vfill
\end{slide}

\begin{slide}
\slidetitle{clusters}
\begin{center}
\texttt{for X being {set} holds X is \green{empty} implies X is \green{finite}}
\adviwait

$\downarrow$

\texttt{\blue{cluster} \green{empty} -> \green{finite} {set}}
\end{center}
\bigskip
\bigskip

\begin{center}
any term with attribute \green{\texttt{empty}} \red{automatically} also gets attribute \green{\texttt{finite}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{typed or untyped logic?}
\slidetitle{what does it all mean?}
{foundations of Mizar:}
\smallskip
\begin{center}
\green{Tarski-Grothendieck set theory} \\
$=$ \\
\strut\green{ZFC} $+$ `there are arbitrarily large inaccessible cardinals'
\end{center}
%\adviwait
\bigskip

set of axioms on top of \red{untyped} first order predicate logic

\vfill
\end{slide}

\def\Iff{\,\Leftrightarrow\,}%
\def\Implies{\,\Rightarrow\,}%

\begin{slide}
\slidetitle{the axioms of Mizar}
\vbox to 0pt{
\vspace{-1.5\bigskipamount}
\begin{center}
\footnotesize
\begin{tabular}{lcc}
\texttt{TARSKI:def 3} && $\red{X \subseteq Y} \Iff (\forall x.\; x \in X \Implies x \in Y)$ \\
\texttt{TARSKI:def 5} && $\red{\langle x,y\rangle} = {\leftbrace}{\leftbrace}x,y{\rightbrace},{\leftbrace}x{\rightbrace}{\rightbrace}$ \\
\texttt{TARSKI:def 6} && $\red{X \sim Y} \Iff \exists Z.\, (\forall x.\, x \in X. \!\Implies\! \exists y.\, y \in Y \land \langle x,y\rangle \in Z) \land {}$ \\
&& $\phantom{X \sim Y \Iff \exists Z.\,} (\forall y.\, y \in Y. \!\Implies\! \exists x.\, x \in X \land \langle x,y\rangle \in Z) \land {}$ \\
&& $(\forall x \forall y \forall z \forall u.\, \langle x,y\rangle \in Z \land \langle z,u\rangle \in Z \Implies (x = z \Iff y = u))$ \\
\noalign{\vspace{-.1em}\color{slideblue}\rule{\linewidth}{0.04em}\vspace{.2em}}%
\texttt{TARSKI:def 1} && $x \in \red{{\leftbrace}y{\rightbrace}} \Iff x = y$ \\
\texttt{TARSKI:def 2} && $x \in \red{{\leftbrace}y,z{\rightbrace}} \Iff x = y \,\lor\, x = z$ \\
\texttt{TARSKI:def 4} && $x \in \red{\bigcup X} \Iff \exists Y.\; x \in Y \,\land\, Y \in X$ \\
\noalign{\medskip}
\texttt{TARSKI:2} && $(\forall x.\; x\in X \!\Iff\! x\in Y) \Implies X = Y$ \\
\texttt{TARSKI:7} && $x \in X \Implies \exists Y.\; Y \in X \land \neg\exists x.\; x \in X \land x \in Y$ \\
\green{\texttt{TARSKI:sch 1}} && \green{$(\forall x\,\forall y\,\forall z.\, P[x,y] \land P[x,z] \!\Implies\! y = z) \rlap{${} \Implies {}$}$} \\
&& \green{$(\exists X.\; \forall x.\; x \in X \Iff \exists y.\; y \in A \,\land\, P[y,x])$} \\
\texttt{TARSKI:9} && $\exists M.\, N\in M \land (\forall X\forall Y.\, X \in M \land Y \subseteq X \!\Implies\! Y \in M) \land {}$ \\
&& $(\forall X.\, X \in M \!\Implies\! \exists Z.\, Z \in M \land \forall Y.\, Y \subseteq X \!\Implies\! Y \in Z) \land {}$ \\
&& $(\forall X.\, X \subseteq M \!\Implies\! X \sim M \lor X \in M)$
\end{tabular}
\end{center}
\vss
}

\vfill
\end{slide}

\begin{slide}
\slidetitle{translation to untyped logic}
\begin{center}
\texttt{for \green{i being Integer} holds i >= 0 iff \green{i is Nat}} \adviwait

$\forall\,\green{i : {\tt Integer}}\,.\,\; i \ge 0 \,\Leftrightarrow\, (\,\green{i:{\tt Nat}}\,)$
\adviwait

\medskip
$\downarrow$
\medskip

$\forall\,i\,.\; \green{\mathop{\tt Integer\,}(i)} \Rightarrow \big[\,i \ge 0 \,\Leftrightarrow\, \green{\mathop{\tt Nat\,}(i)}\,\big]$
\end{center}
\bigskip
\medskip
%\adviwait

types are just \red{predicates} that the system manages automatically
\bigskip
\adviwait

\blue{dependent} types with $n$ arguments are predicates with $n + 1$ arguments

\vfill
\end{slide}

\begin{slide}
\sectiontitle{the type system as typing rules}
\slidetitle{symbolic notation}

\def\cases{::=}
\def\alt{\;|\;}
\def\wf{\mathord{\cdot}}
\def\negvspace{\vspace{-\smallskipamount}}

\vspace{-1\bigskipamount}
\vbox to 0pt{
\enskip\begin{tabular}{ccll}
\green{$x$} &&& term variables\negvspace\\
\green{$f$} &&& function symbols\negvspace\\
\green{$M\!$} &&& mode symbols\negvspace\\
\green{$\alpha$} &&& attribute symbols\adviwait\\
$t$ &$\cases$& $x \alt f(\vec{t})$ & terms\negvspace\\
$R$ &$\cases$& $\blue{\star} \alt M(\vec{t})$ & radix types\negvspace\\
$a$ &$\cases$& $\alpha \alt \bar{\alpha}$ & adjectives\negvspace\\
$T$ &$\cases$& $\vec{a}\,R$ & types\adviwait\\
$J$ &$\cases$& $\wf \alt t : T \alt T \le T \alt \exists\, T \alt \alpha / T\qquad$ & judgment elements\negvspace\\
$D$ &$\cases$& $x : T$ & declarations\negvspace\\
$\Delta$ &$\cases$& $\vec{D}$\negvspace\\
$\Gamma$ &$\cases$& $\overrightarrow{[\Delta](J)}$\negvspace\\
&& \red{$\Gamma; \Delta \vdash J$} & judgments
\end{tabular}
\vss}

\vfill
\end{slide}

\begin{slide}
\slidetitle{rules}
\textbf{twenty-two typing rules}

\def\wf{\mathord{\cdot}}

\blue{three examples:}
$$
{
\over
\strut
\,;\, \vdash \wf
}
$$
\adviwait
$$
{
\strut
\Gamma;\, \vec{x} : \vec{T} \vdash \exists\, T'
\over
\strut
\Gamma,\, [\vec{x} : \vec{T}](M(\vec{x}) \le T'),\,
  [\vec{x} : \vec{T}](\exists\, M(\vec{x}));\, \vdash \wf
}
\rlap{$\; M \not\in \Gamma$}
\leqno{
\strut\rlap{\green{\textsl{mode definition:}}}
}
$$
\adviwait
$$
{
\strut
\Gamma; \Delta \vdash \vec{a}\,T' \le T'
\quad
\Gamma; \Delta \vdash \vec{a}'\,T' \le T'
\over
\strut
\Gamma,\, [\Delta](\vec{a}\,T' \le \vec{a}'\,T');\, \vdash \wf
}
\leqno{
\strut\rlap{\green{\textsl{conditional cluster:}}}
}
$$

\vfill
\end{slide}

\def\key#1{\mbox{\sf #1}}

\begin{slide}
\sectiontitle{correctness}
\slidetitle{translating judgments}
\begin{eqnarray*}
\mbox{type judgment} &\rightarrow& \mbox{first order sequent} \adviwait\\
\noalign{\bigskip}
\green{\strut\rlap{\small $\hspace{-8.35em}
\key{int} \le \star,\;
\exists\,\key{int},\;
\key{pos}/\key{int},\;
\exists\,\key{pos}\;\key{int}
\,;\;
x : \key{pos}\;\key{int}
\;\vdash\;
x : \star
$}\hspace{5em}\strut}
\\
\noalign{\vspace{-\smallskipamount}}
&\green{\rightarrow}& \\
\noalign{\vspace{-\smallskipamount}}
&& \green{\hspace{10em}\llap{\footnotesize $
\left(\forall x.\, \key{int}(x)\Rightarrow\top\right),\;
\left(\exists x.\, \key{int}(x)\right),\;
\top,\;
\left(\exists x.\, \key{pos}(x) \land \key{int}(x)\right),\;
\left(\key{pos}(x) \land \key{int}(x)\right)
\;\vdash\;
\top
$\hspace{-6.9em}
}} \adviwait\\
\noalign{\bigskip\textbf{main theorem}}
\noalign{\vspace{-.7\medskipamount}\red{`the type system is correct'}\bigskip}
\mbox{\red{derivable judgment}} &\red{\rightarrow}& \mbox{\red{provable sequent}}
\end{eqnarray*}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{outlook}
\slidetitle{system in the paper is an idealization}
\begin{alltt}\small
definition let n be Nat;
  redefine mode \red{\advirecord{f1}{Element}}\adviplay{f1} of n -> \red{\advirecord{f2}{Element}}\adviplay{f2} of n + 1;
end;
\end{alltt}
\bigskip
\adviwait

according to the rules from the paper we have

\green{
\texttt{\small Element of n} $\to$
\texttt{\small Element of n + 1} $\to$
\texttt{\small Element of n + 2} $\to$
\dots
}
\bigskip
\adviwait

in the actual Mizar system we just have

\green{
\texttt{\small Element of n} $\to$
\texttt{\small Element of n + 1}
}
\adviwait
\adviplay[slidered]{f1}
\adviplay[slidered]{f2}

\vfill
\end{slide}

\begin{slide}
\slidetitle{why not have something like the Mizar type system yourself?}
\begin{itemize}
\item[$\bullet$]
the Mizar proof language is well-known to be \green{nice}
\medskip

\item[$\bullet$]
the \red{Mizar type system} is less known, but \green{very nice} too
\medskip

\item[$\bullet$]
every system can have the Mizar type system \red{as a layer on top}

\end{itemize}
\vspace{3.5em}
\vbox to 0pt{
\hfill\includegraphics[width=7em]{/home/freek/talks/miztype/bialystok.eps}
\vss
}

\vfill
\end{slide}

\end{document}