\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}{.6,.6,.6}
\definecolor{slidelightblue}{rgb}{.8,.8,1}
\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\lightblue#1{\textcolor{slidelightblue}{#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}{\large\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{-5em}$}

\def\tto{\to\hspace{-5pt}\!\!\to}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large polymorphism and impredicativity}

\red{logical verification} \\
week 10 \\
2004 11 17

\end{slide}

\begin{slide}
\sectiontitle{polymorphism}
\slidetitle{the course}
\vspace{0pt}

\begin{center}
$\hspace{-1em}$\begin{tabular}{rcl}
propositional logic &$\leftrightarrow$& \textbf{simple} type theory \\
&& {$\qquad\lambda{\to}$} \\
\noalign{\medskip}
predicate logic &{$\leftrightarrow$}& {type theory with \textbf{dependent types}} \\
&& {$\qquad\lambda P$} \\
\noalign{\medskip}
\gray{2nd order propositional logic} &\gray{$\leftrightarrow$}& \red{\textbf{polymorphic} type theory} \\
&& \red{$\qquad\lambda 2$}
\end{tabular}$\hspace{-1em}$
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the lambda cube}

$$
\xymatrix@!{
 & \lambda\omega \ar@{-}[rr]\ar@{-}'[d][dd]
   & & \green{\lambda C} \ar@{-}[dd]
\\
 \red{\lambda2} \ar@{-}[ur]\ar@{-}[rr]\ar@{<-}[dd]|-{\mbox{\small\red{polymorphism}}}
 & & \lambda P2 \ar@{-}[ur]\ar@{-}[dd]
\\
 & \lambda\underline\omega \ar@{-}'[r][rr]
 & & \lambda P\underline\omega
\\
 \red{\lambda{\to}} \ar@{->}[rr]|-{\mbox{\small{$\,$dependence$\,$}}}
   \ar@{-}[ur]
 & & {\lambda P} \ar@{-}[ur]
}
\vspace{-8pt}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{polymorphism}
we had {functions \& quantification} over the \textbf{elements} of a type
$$\begin{array}{c}\lambda n : \green{\mbox{nat}}\,.\; {\cdots}\\
\forall n : \green{\mbox{nat}}\,.\; {\cdots}\end{array}$$

\begin{center}
\texttt{\ \ \ fun n :\ \green{nat} => }{\dots}\texttt{\ \ \ \ \ } \\
\texttt{forall n :\ \green{nat}, }{\dots}\texttt{\ \ \ \ \ \ \ }
\end{center}
\medskip
\adviwait

we now add {functions \& quantification} over the \textbf{types} themselves
$$\begin{array}{c}\lambda A : \red{*}\,.\; {\cdots}\quad\enskip\\
\forall A : \red{*}\,.\; {\cdots}\quad\enskip\end{array}$$

\begin{center}
\texttt{\ \ \ fun A :\ \red{Set} => }{\dots}\texttt{\ \ \ \ \ } \\
\texttt{forall A :\ \red{Set}, }{\dots}\texttt{\ \ \ \ \ \ \ }
\end{center}
\vspace{-2pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{dependent types versus polymorphism}
\begin{itemize}
\item[$\bullet$]
\textbf{dependent types}
\medskip

\begin{center}
\red{types} can take \red{terms} as an argument
\end{center}
\bigskip

\item[$\bullet$]
\textbf{polymorphism}
\medskip

\begin{center}
\red{terms} can take \red{types} as an argument
\end{center}

\end{itemize}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the polymorphic identity}
\slidetitle{\texttt{natid}}
\red{identity function on the natural numbers}
$$\green{\lambda n : {\mbox{nat}}\,.\; n}\bigskip\adviwait$$

\begin{alltt}
Definition \red{natid} : \green{nat -> nat} :=
  \green{fun n : nat => n}.
\end{alltt}
\bigskip

\begin{alltt}
Check \blue{(natid 0)}.
Eval compute in \blue{(natid 0)}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{boolid}}
\red{identity function on the booleans}
$$\green{\lambda b : {\mbox{bool}}\,.\; b}\bigskip\adviwait$$

\begin{alltt}
Definition \red{boolid} : \green{bool -> bool} :=
  \green{fun b : bool => b}.
\end{alltt}
\bigskip

\begin{alltt}
Check \blue{(boolid true)}.
Eval compute in \blue{(boolid true)}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{polyid}}
\red{\textbf{polymorphic} identity function}
$$\green{\advirecord{x1}{\green{\lambda A : *.}}\, \lambda x : A.\, x} \advirecord{x2}{\quad:\quad \green{\Pi A : *.\, A \to A}}\bigskip\adviwait\adviplay{x1}\adviwait\adviplay{x2}\adviwait$$

\begin{alltt}
Definition \red{polyid} : \green{forall A : Set, A -> A} :=
  \green{fun A : Set => fun x : A => x}.
\end{alltt}
\bigskip

\begin{alltt}
Check \blue{(polyid nat 0)}.
Check \blue{(polyid bool true)}.\medskip
Eval compute in \blue{(polyid nat 0)}.
Eval compute in \blue{(polyid bool true)}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Notation}}
\begin{alltt}
Check \blue{(polyid nat 0)}.
Check \blue{(polyid _ 0)}.\adviwait
\end{alltt}
\bigskip

\begin{alltt}
Notation \red{id} := \green{(polyid _)}.
\end{alltt}
\bigskip

\begin{alltt}
Check \blue{(id 0)}.
Check \blue{(id true)}.\medskip
Eval compute in \blue{(id 0)}.
Eval compute in \blue{(id true)}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{lists}
\slidetitle{\texttt{natlist}}

\begin{alltt}
Inductive \red{natlist} : \green{Set} :=
  \green{natnil} : natlist
| \green{natcons} : nat -> natlist -> natlist.
\end{alltt}
\bigskip

$$\blue{3, 1, 4, 1, 5, 9, 2, 6}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{natlist\char`\_dep}}
\red{generalizing \texttt{natlist} to a \textbf{dependent} type}
\bigskip

\begin{alltt}
Inductive \red{natlist_dep} : \green{(nat -> Set)} :=
  \green{natnil_dep} : (natlist_dep O)
| \green{natcons_dep} : forall n : nat,
    nat -> (natlist_dep n) -> (natlist_dep (S n)).
\end{alltt}
%\bigskip
%
%$$\blue{3, 1, 4, 1, 5, 9, 2, 6}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{boollist}}

\begin{alltt}
Inductive \red{boollist} : \green{Set} :=
  \green{boolnil} : boollist
| \green{boolcons} : bool -> boollist -> boollist.
\end{alltt}
\bigskip

$$\blue{F, T, F, F, F, T, T, F}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{polylist}}
\red{generalizing \texttt{natlist} to a \textbf{polymorphic} type}
\bigskip

\begin{alltt}
Inductive \red{polylist} \blue{(A : Set)} : \green{Set} :=
  \green{polynil} : (polylist A)
| \green{polycons} : A -> (polylist A) -> (polylist A).
\end{alltt}
\bigskip
\adviwait

\begin{alltt}
\red{polylist} : \blue{forall A : Set,} Set \adviwait
\red{polylist} : \blue{Set ->} Set \medskip\adviwait
\green{polynil}  : \blue{forall A : Set,} (polylist A)
\green{polycons} : \blue{forall A : Set,} A -> (polylist A) -> (polylist A)\toolong
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{examples of polymorphic lists}

$$\red{3, 1}$$
\begin{alltt}
polycons \green{nat} \red{3} (polycons \green{nat} \red{1} (polynil \green{nat}))
\end{alltt}

$$\red{F, T}$$
\begin{alltt}
polycons \green{bool} \red{false} (polycons \green{bool} \red{true} (polynil \green{bool}))
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\dots and now in stereo!}

\begin{alltt}
Inductive \red{poly}list\green{_dep} \red{(A : Set)} : \green{nat ->} Set :=
  \red{poly}nil\green{_dep} : (\red{poly}list\green{_dep} \red{A} \green{O})
| \red{poly}cons\green{_dep} : \green{forall n : nat,}
    \red{A} -> (\red{poly}list\green{_dep} \red{A} \green{n}) -> (\red{poly}list\green{_dep} \red{A} \green{(S n)}).
\end{alltt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{Notation}}

\begin{alltt}
Notation \red{ni} := \green{(polynil _)}.
Notation \red{co} := \green{(polycons _)}.
\end{alltt}
\bigskip

\begin{alltt}
Check \blue{(co 3 (co 1 ni))}.
Check \blue{(co false (co true ni))}.\medskip
Check \blue{(co 3 (co true ni))}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} and even more polymorphic}

\begin{alltt}
Inductive polylist' : \blue{Type} :=
  polynil' : polylist'
| polycons' : \green{forall A : Set,} A -> polylist' -> polylist'.
\end{alltt}
\bigskip
\adviwait

\begin{alltt}
polycons' \green{nat} \red{3} (polycons' \green{bool} \red{true} polynil')
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{length of a list}
\slidetitle{\texttt{natlength}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint \red{natlength} (l : natlist) \{struct l\} : nat :=
  match l with
    \green{natnil} => O
  | \green{natcons h t} => S (natlength t)
  end.
\end{alltt}
\endgroup
\bigskip

\begin{alltt}
\red{natlength} : natlist -> nat
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{polylength}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint \red{polylength}
    (A : Set) (l : polylist A) \{struct l\} : nat :=
  match l with
    \green{polynil}   => O
  | \green{polycons   h t} => S (polylength A t)
  end.
\end{alltt}
\endgroup
\bigskip

\begin{alltt}
\red{polylength} : forall A : Set, polylist A -> nat
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{polylength}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint \red{polylength'} (l : polylist') \{struct l\} : nat :=
  match l with
    \green{polynil'} => O
  | \green{polycons' A h t} => S (polylength' t)
  end.
\end{alltt}
\endgroup
\bigskip

\begin{alltt}
\red{polylength'} : polylist' -> nat
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{applying a function to each element of a list}
\slidetitle{\texttt{natmap}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint \red{natmap}
    (f : nat -> nat) (l : natlist) \{struct l\} : natlist :=
  match l with 
    \green{natnil} => natnil
  | \green{natcons h t} => natcons (f h) (natmap f t)
  end.
\end{alltt}
\endgroup
\medskip

\begin{alltt}
\red{natmap} : (nat -> nat) -> natlist -> natlist
\end{alltt}
\bigskip

$\red{\mbox{\texttt{natmap}}} \;(\lambda n.\, n + 10)\, \blue{(3,1,4,1,5,9,2,6)} = \blue{(13,11,14,11,15,19,12,16)}$

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

\begin{slide}
\slidetitle{\texttt{polymap}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint polymap \red{(A : Set)}
    (f : \green{A} -> \green{A}) (l : polylist \red{A}) \{struct l\} : polylist \red{A} :=\toolong
  match l with 
    polynil => polynil \red{A}
  | polycons h t => polycons \red{A} (f h) (polymap \red{A} f t)
  end.
\end{alltt}
\bigskip
\endgroup

\begin{alltt}
polymap :
  \red{forall A : Set,} (\green{A} -> \green{A}) -> polylist \red{A} -> polylist \red{A}\toolong
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{{\dots} and even more polymorphic}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint polymap' \red{(A B : Set)}
    (f : \green{A} -> \green{B}) (l : polylist \red{A}) \{struct l\} : polylist \red{B} :=\toolong
  match l with 
    polynil => polynil \red{B}
  | polycons h t => polycons \red{B} (f h) (polymap' \red{A} \red{B} f t)
  end.
\end{alltt}
\bigskip
\endgroup

\begin{alltt}
polymap' :
  \red{forall A B : Set,} (\green{A} -> \green{B}) -> polylist \red{A} -> polylist \red{B}\toolong
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{iterating an operation over a list}
\slidetitle{\texttt{natfold}}

\begingroup
\def\{{\char`\{}
\def\}{\char`\}}
\begin{alltt}
Fixpoint \red{natfold} (f : nat -> nat -> nat) (z : nat)
    (l : natlist) \{struct l\} : nat :=
  match l with
    \green{natnil} => z
  | \green{natcons h t} => f h (natfold f z t)
  end.
\end{alltt}
\endgroup
\medskip

\begin{alltt}
\red{natfold} : (nat -> nat -> nat) -> nat -> natlist -> nat
\end{alltt}

$$\begin{array}{l}\red{\mbox{natfold}}\;f\,z\;\blue{(3,1,4,1)} = f\,\blue{3}\,(f\,\blue{1}\,(f\,\blue{4}\,(f\,\blue{1}\,z)))\\
\red{\mbox{natfold}}\;\mbox{\rlap{$\ast$}\phantom{$f$}}\,z\;\blue{(3,1,4,1)} = \blue{3} \ast \blue{1} \ast \blue{4} \ast \blue{1} \ast z
\end{array}$$

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

\begin{slide}
\slidetitle{\texttt{sum}}

\begin{alltt}
Definition sum := natfold \red{plus} \green{O}.
\end{alltt}

\begin{alltt}
sum : natlist -> nat
\end{alltt}
\bigskip

\begin{alltt}
Eval compute in
  sum \blue{(natcons 3 (natcons 1 (natcons 4 (natcons 1 natnil))))}.\toolong
\end{alltt}

$$\mbox{natfold}\;\red{\mbox{$(+)$}}\;\green{0}\;\blue{(3,1,4,1)} = 3 \mathbin{\red{+}} 1 \mathbin{\red{+}} 4 \mathbin{\red{+}} 1 \mathbin{\red{+}} \green{0} = 9$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{polyfold}}

\begin{alltt}
Fixpoint \red{polyfold} (A B : Set) (f : A -> B -> B) (z : B)
    (l : polylist A) {struct l} : B :=
  match l with
    \green{polynil} => z
  | \green{polycons h t} => f h (polyfold A B f z t)
  end.
\end{alltt}
\bigskip

\begin{alltt}
\red{polyfold} :
  forall A B : Set, (A -> B -> B) -> B -> polylist A -> B
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{\texttt{sum} defined with \texttt{polyfold}}

\begin{alltt}
Definition \red{sum'} := \green{polyfold nat nat plus O}.
\end{alltt}

\begin{alltt}
Definition \red{sum'} := \green{polyfold _ _ plus O}.
\end{alltt}
\bigskip

\begin{alltt}
\red{sum'} : \green{polylist nat -> nat}
\end{alltt}
\bigskip

\begin{alltt}
Eval compute in \red{sum'} \blue{(co 3 (co 1 (co 4 (co 1 ni))))}.
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{impredicativity}
\slidetitle{Russell's paradox}
Cantor: \green{power set} is bigger than the set itself
\bigskip

\textbf{naive set theory}
$$\green{{\cal P}(\mbox{Set})} \subseteq \mbox{Set}$$

$$\begin{array}{c}
\red{\{x \mathrel{|} x \not\in x\}} \mathrel{\red{\in}} \red{\{x \mathrel{|} x \not\in x\}} \\
\Updownarrow \\
\red{\{x \mathrel{|} x \not\in x\}} \mathrel{\red{\not\in}} \red{\{x \mathrel{|} x \not\in x\}}
\end{array}
$$
\textbf{inconsistent}

\vfill
\end{slide}

\begin{slide}
\slidetitle{impredicativity}
$\lambda 2$ is \red{impredicative}
$$\mbox{bool} : * \;\vdash\; \green{* \to \mbox{bool}} \,:\, \red{*}\medskip$$
$$\green{{\cal P}(\mbox{Set})} \in \mbox{Set}\bigskip\medskip\adviwait$$
$$\;\vdash\; \blue{(\Pi A : *.\, A)} \,:\, \red{*}\adviwait$$

\textbf{Coq} \\
\texttt{Prop} is \red{impredicative}, \texttt{Set} is \red{predicative}

\begin{center}
\texttt{\blue{(forall A : Prop, A)} : \red{Prop}} \\
\texttt{\blue{(forall A : Set , A)} : \red{Type}}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{$\lambda 2$ is inconsistent with classical mathematics}

$$\mbox{bool} : * \;\vdash\; \green{\Pi A : *.\, (A \to \mbox{bool})} \,:\, *\medskip\adviwait$$

\begin{center}
{`set of functions that map \textbf{each} set into a subset of that set'}
\end{center}

$$\textstyle \advirecord{y}{\red{U :=}\;} \green{\prod_{A \in {\sf Set}} {\cal P}(A)} \in \mbox{Set}\adviwait\adviplay{y}\adviwait$$

$$\red{U} = {\cal P}(\red{U}) \times \dots$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{the paradox}
$$\textstyle {\red{U} :=\;} {\prod_{A \in {\sf Set}} {\cal P}(A)} \in \mbox{Set}\adviwait\bigskip$$

if $u \in U$ then for each $A \in \mbox{Set}$ holds that $u(A) \in {\cal P}(A)$
\adviwait

in particular $u(U) \in {\cal P}(U)$
\adviwait

$$\red{X} := \{ u \in U \mathrel{|} u \not\in u(U) \} \adviwait\in {\cal P}(U)\bigskip\adviwait$$

take some $\red{x} \in U$ such that $x(U) = X$\adviwait

$$\blue{x \in x(U) \;\Leftrightarrow\; x \in X \;\Leftrightarrow\; x \not\in x(U)}$$

\vfill
\end{slide}

\end{document}