\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{-3em}$}

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

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large simply typed $\lambda$-calculus}

\red{logical verification} \\
week 2 \\
2004 09 15

\end{slide}

\begin{slide}
\sectiontitle{newsflash}
\slidetitle{prime number theorem formalized}
write $\pi(n)$ for the number of primes below $n$, then

$$\red{\lim_{n\to\infty} {\pi(n)\over n/\ln(n)} = 1}
\medskip$$

\green{\url{http://www.andrew.cmu.edu/user/avigad/isabelle/}} %\\
%{Isabelle/HOL}
\begin{itemize}
\item[$\bullet$]
Jeremy Avigad
\item[$\bullet$]
Kevin Donelly
\item[$\bullet$]
David Gray
%\medskip
\end{itemize}

\vfill
\end{slide}

\newcommand\opensquare[1]{%
{\begin{picture}(#1,#1)
\put(0,0){\line(1,0){#1}}
\put(#1,0){\line(0,1){#1}}
\put(#1,#1){\line(-1,0){#1}}
\put(0,#1){\line(0,-1){#1}}
\end{picture}}}

\newcommand\filledsquare[3]{\advirecord{#1}{\lightblue{\rule{#3pt}{#3pt}}}%
  \llap{\advirecord{#2}{\opensquare{#3}}}}

\begin{slide}
\sectiontitle{overview}
\slidetitle{last week}

\begin{center}
\begin{tabular}{rccc}
&& logic & $\,$type theory$\,$ \\
\noalign{\vspace{-\smallskipamount}}
&& \red{proofs} & \hbox to 0pt{\hss\red{$\lambda$-terms}\hss} \\
\noalign{\bigskip}
\raise1.3em\hbox{on paper} && \filledsquare{a1a}{a1b}{30} & \opensquare{30} \\
\noalign{\bigskip\smallskip}
\raise1.3em\hbox{\green{in Coq}} && \filledsquare{a2a}{a2b}{30} & \opensquare{30}
\end{tabular}
$\hspace{3em}$
\end{center}
\adviplay{a1a}
\adviplay{a1b}
\adviplay{a2a}
\adviplay{a2b}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{why typed $\lambda$-calculus?}
\slidetitle{C program}
\begingroup%
\renewcommand{\\}{\char`\\}%
\renewcommand{\{}{\char`\{}%
\renewcommand{\}}{\char`\}}%
\begin{alltt}
#include <math.h>
\end{alltt}
\begin{alltt}
\red{double findzero(\green{\underline{\red{double (*f)(double)}}}, double z)} \{
  double x, y;
  while (x = z, y = (*f)(x), z = x - y/((*f)(x + y) - y)*y,\toolong
    fabs(z/x - 1) >= 1e-15) ;
  return z;
\}
\end{alltt}
\begin{alltt}
\green{double sqrminus2(double x)} \{ return x*x - 2; \}
\end{alltt}
\begin{alltt}
{main()} \{
  printf("%.15g{\\}n", \red{findzero}(&\green{sqrminus2}, 1));
\}
\end{alltt}
\endgroup
\vspace{-10pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{programming styles}
\begin{itemize}
\item[$\bullet$]
imperative programming
\begin{itemize}
\item[]
C
\end{itemize}
\item[$\bullet$]
object-oriented programming
\begin{itemize}
\item[]
C++
\item[]
java
\end{itemize}
\item[$\bullet$]
logic programming
\begin{itemize}
\item[]
prolog
\end{itemize}
\item[$\bullet$]
{functional programming}
\begin{itemize}
\item[]
lisp
\item[]
\red{\rlap{ML}} \green{\qquad\qquad\quad `typed'}
\item[]
\red{\rlap{haskell}} \green{\qquad\qquad\quad `lazy' \qquad
calculations with infinite data structures}
\end{itemize}
\end{itemize}

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

\begin{slide}
\slidetitle{functional programming}

functional values become \green{first class objects}
\medskip

no need to name functions anymore
\medskip

\begin{center}
\verb|findzero( &sqrminus2 ,| \dots\verb|)| \\
\smallskip
$\downarrow$ \\
\smallskip
%\verb|findzero( |\red{$\lambda \texttt{x} : \texttt{double} \,.\;\, \texttt{x*x - 2}$}\verb| ,| \dots\verb|)|
\verb|findzero( |\red{$\lambda \texttt{x} \,.\;\, \texttt{x*x - 2}$}\verb| ,| \dots\verb|)|
\bigskip
\end{center}

functions also can \textbf{return} functional values \\
\green{`higher order' functions}

\vfill
\end{slide}

\begin{slide}
\slidetitle{currying}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}

$$\red{f : A \times B \to C}$$

\green{partial evaluation}
$$\green{f(a,\cdot)} : B \to C
%\adviwait
\bigskip$$

curried version of the function:
$$f : A \to (B \to C)
%\adviwait
%\medskip
$$
$$\red{f : A \to B \to C}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{the type of \texttt{findzero}}
\vspace{-\bigskipamount}
\vspace{-\medskipamount}

$$(\texttt{double} \to \texttt{double}) \times \texttt{double} \to \texttt{double}$$
%\adviwait

curried:
$$\red{(\texttt{double} \to \texttt{double}) \to \texttt{double} \to \texttt{double}}$$
\vspace{-1.8\bigskipamount}
\adviwait
$$
\green{
\hspace{-6.2em}
\begin{array}{c}\uparrow\\\noalign{\vspace{-\smallskipamount}}\mbox{atomic type}\end{array}
\hspace{1.1em}
\begin{array}{c}\uparrow\\\noalign{\vspace{-\smallskipamount}}\mbox{function type}\end{array}
}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{simply typed $\lambda$-calculus}
\slidetitle{types}
\begin{itemize}
\item[$\bullet$]
\textbf{atomic types}

\quad \red{$A$ $B$ $C$ \dots}
\item[$\bullet$]
\textbf{function types}

\quad \red{$A \to B$}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{terms}
\begin{itemize}
\item[$\bullet$]
\textbf{variables}

\quad \red{$x$ $y$ $z$ \dots}
\item[$\bullet$]
\textbf{lambda abstraction}

\quad $\red{\lambda x : A.\, t}$

\quad the function that maps the variable $x$ of type $A$ to $t$
\item[$\bullet$]
\textbf{function application}

\quad $\red{t\,u}$

\quad the result of applying the function $t$ to the argument $u$
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{parentheses}
\begin{itemize}
\item[$\bullet$]
function types associate to the right
\item[$\bullet$]
application associates to the left
\medskip
\end{itemize}

\green{these conventions are natural for curried functions}:
\medskip
$$
\red{
\begin{array}{l}
f : A \to (B \to C) \\
(f\,a)\,b \\
\noalign{\smallskip\smallskip}
\qquad\quad\green{\downarrow} \\
\noalign{\medskip}
f : A \to B \to C \\
f\,a\,b
\end{array}
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{simplest example}
\green{identity function on $A$}
\medskip

\begin{tabular}{rl}
term & \red{$\lambda x : A.\, x$} \\
type & \red{$A \to A$}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example in the real numbers}
\vspace{-\medskipamount}

\begin{tabular}{rl}
term & \red{$\lambda x : {\mathbb R}.\; x^2 - 2$} \\
type & \red{${\mathbb R} \to {\mathbb R}$}
\end{tabular}
\bigskip

$
\begin{array}{rcccl}
(\lambda x : {\mathbb R}.\; x^2 - 2)\; 1 &=& 1^2 - 2 &=& -1 \\
(\lambda x : {\mathbb R}.\; x^2 - 2)\; 2 &=& 2^2 - 2 &=& 2 \\
\noalign{\vspace{-\smallskipamount}}
& \green{\uparrow} \\
\noalign{\vspace{-\medskipamount}}
& \hbox to 0pt{\hss \green{$\beta$-step} \hss}
\end{array}
$

\vfill
\end{slide}

\begin{slide}
\slidetitle{bigger example}
\vspace{-\medskipamount}

\begin{tabular}{rl}
term & \red{$\lambda x : (A \to B) \to C \to D.\, \lambda y : C.\, \lambda z : B.\, x \, (\lambda w : A.\, z)\, y$} \\
type & \red{$((A \to B) \to (C \to D)) \to C \to B \to D$}
\end{tabular}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{type derivations}
\slidetitle{judgments}

$$\red{\gray{\underbrace{\red{\strut x_1 : A_1,\; x_2 : A_2,\; \dots,\; x_n : A_n}}_{
\green{\begin{array}{c}\mbox{\large $\Gamma$}\\
\noalign{\vspace{-1.5\smallskipamount}}
\mbox{context}\\
\mbox{\black{list of variable declarations}}\end{array}}}} \,\vdash\, t : A}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{the three typing rules}
$$
%\red
{
%\over
\Gamma,\, x : A,\, \Gamma' \,\vdash\, \red{x} : A
}
\leqno{\mbox{\rlap{\textbf{variable rule}}}}
%\medskip
$$

\rightline{\green{$x$ does not occur in $\Gamma'$}}

$$
%\red
{
\strut
\Gamma,\, x : A \,\vdash\, t : B
\over
\strut
\Gamma \,\vdash\, (\red{\lambda x : A.\, t}) : (A \to B)
}
\leqno{\mbox{\rlap{\textbf{abstraction rule}}}}
$$

$$
%\red
{
\strut
\Gamma \,\vdash\, t : A \to B
\qquad
\Gamma \,\vdash\, u : A
\over
\strut
\Gamma \,\vdash\, \red{t\,u} : B
}
\leqno{\mbox{\rlap{\textbf{application rule}}}}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{type derivation for the example}
\vspace{0pt}

$\vdash \red{\lambda x : (A \to B) \to C \to D.\, \lambda y : C.\, \lambda z : B.\, x \, (\lambda w : A.\, z)\, y} :$ \\
\rightline{$\red{((A \to B) \to (C \to D)) \to C \to B \to D}$}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the Curry-Howard-de Bruijn isomorphism}
\slidetitle{recap minimal logic}
\begin{itemize}
\item[$\bullet$]
\textbf{formulas}

propositional variables \\
implication $A \to B$
\item[$\bullet$]
\textbf{rules}

implication introduction \\
implication elimination
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{recap example natural deduction}

$$((A \to B) \to (C \to D)) \to C \to B \to D$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{implication introduction \& the abstraction rule}

$$
\hspace{2em}
{
\begin{array}{c}
[\green{A}^x] \\
\vdots \\
\green{B}
\end{array}
\over
\strut
\red{A \to B}
}
\enskip
{I[\blue{x}]{\to}}
\hspace{4em}
{
\strut
\Gamma,\, \blue{x} : \green{A} \,\vdash\, {t} : \green{B}
\over
\strut
\Gamma \,\vdash\, {(\lambda x : A.\, t)} : (\red{A \to B})
}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{implication elimination \& the application rule}

$$
\hspace{2em}
{
\begin{array}{c}
\vdots \\
\green{A \to B}
\end{array}
\qquad
\begin{array}{c}
\vdots \\
\green{A}
\end{array}
\over
\strut
\red{B}
}
\enskip
{E{\to}}
\hspace{4em}
{
\strut
\Gamma \,\vdash\, {t} : \green{A \to B}
\qquad
\Gamma \,\vdash\, {u} : \green{A}
\over
\strut
\Gamma \,\vdash\, {t\,u} : \red{B}
}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{isomorphism}
\begin{center}
\begin{tabular}{rcl}
propositional variable  &$\red{\sim}$&  type variable \\
the connective $\to$  &$\red{\sim}$&  the type constructor $\to$ \\
formula  &$\red{\sim}$&  type \\
\noalign{\bigskip}
assumption  &$\red{\sim}$&  variable \\
implication introduction  &$\red{\sim}$&  lambda abstraction \\
implication elimination  &$\red{\sim}$&  function application \\
proof  &$\red{\sim}$&  term \\
\noalign{\bigskip}
provability  &$\red{\sim}$&  `inhabitation' \\
proof checking  &$\red{\sim}$&  type checking
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{BHK-interpretation}
\red{Brouwer, Heyting, Kolmogorov} \\
\green{intuitionistic logic}
\medskip

\begin{center}
\begin{tabular}{lcl}
proof of $A \to B$    &$\red{\sim}$&  function that maps proofs of $A$ to proofs $B$ \\
proof of $\bot$       &&              does not exist \\
proof of $A \land B$  &$\red{\sim}$&  pair of a proof of $A$ and a proof of $B$ \\
proof of $A \lor B$   &$\red{\sim}$&  either a proof of $A$ or a proof of $B$
\end{tabular}
\end{center}

\vfill
\end{slide}

\begin{slide}
\slidetitle{propositions as types}

$$\red{\lambda x : A.\, x} \,:\, \green{A \to A}
\medskip$$

the function type  $\green{A \to A}$  represents a proposition \\
the term  $\red{\lambda x : A.\, x}$  represents a proof of that proposition
\bigskip

$\lambda$-terms are \textbf{proof objects}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Coq}
\slidetitle{term syntax}
\begin{itemize}
\item[$\bullet$]
\texttt{x}
\item[$\bullet$]
\verb|fun x : A => t|
\item[$\bullet$]
\texttt{t u}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{commands}
\begin{itemize}
\item[$\bullet$]
\verb|Check|

\green{prints a term with its type}

\item[$\bullet$]
\verb|Print|

\green{print the term for a symbol with its type}

\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}

\begin{center}
\verb|fun x : A => x : A |\red{\texttt{->}}\verb| A|
\end{center}
\bigskip

\green{Coq as proof checker} \\
`\red{\texttt{->}}'\enskip represents implication
\medskip

\green{Coq as functional programming language} \\
`\red{\texttt{->}}'\enskip represents function type

\vfill
\end{slide}

\begin{slide}
\slidetitle{proof objects}

\begin{alltt}
Lemma {I : A -> A}.
\green{\dots}
Qed.
\end{alltt}
\begin{alltt}
{Print I.}
\end{alltt}

\vfill
\end{slide}

\begin{slide}
\slidetitle{example}

$$\red{\texttt{((A -> B) -> (C -> D)) -> C -> B -> D}}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{summary}
\slidetitle{this week}

\begin{center}
\begin{tabular}{rccc}
&& logic & $\,$type theory$\,$ \\
\noalign{\vspace{-\smallskipamount}}
&& \red{proofs} & \hbox to 0pt{\hss\red{terms}\hss} \\
\noalign{\bigskip}
\raise1.3em\hbox{on paper} && \filledsquare{b1a}{b1b}{30} & \filledsquare{b3a}{b3b}{30} \\
\noalign{\bigskip\smallskip}
\raise1.3em\hbox{\green{in Coq}} && \filledsquare{b2a}{b2b}{30} & \filledsquare{b4a}{b4b}{30}
\end{tabular}
$\hspace{3em}$
\end{center}
\adviplay{b1a}
\adviplay{b1b}
\adviplay{b2a}
\adviplay{b2b}
\adviplay{b3b}
\adviplay{b4b}
%\adviwait
\adviplay{b3a}
\adviplay{b3b}
\adviplay{b4a}
\adviplay{b4b}

\vfill
\end{slide}

\end{document}