\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 the pure type system called $\lambda P$}

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

\end{slide}

\begin{slide}
\sectiontitle{recap}
\slidetitle{where we are in the course}
\vspace{0pt}

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

\begin{slide}
\slidetitle{the main difference between $\lambda{\to}$ and $\lambda P$}
$${A \to B}$$

\green{`type of functions from $A$ to $B$'}

$$\red{\Pi x : A.\, B}$$

\vbox to 0pt{
\green{`type of functions from $A$ to $B$'}
\vss
}
\vspace{-1.2\medskipamount}
\rightline{\red{dependent \rlap{product}\phantom{function type}}}
\rightline{\red{dependent function type}}
\medskip

type of function value $B$ now can \green{depend} on function argument $x$ \\
arrow type becomes a special case
\vfill
\end{slide}

\begin{slide}
\sectiontitle{$\lambda P$}
\slidetitle{syntax}

\begin{itemize}
\item[$\bullet$]
\textbf{two sorts}

$\red{*}$, $\red{\Box}$
\item[$\bullet$]
\textbf{variables}

$x$, $y$, $z$, \dots
\item[$\bullet$]
\textbf{function application}

$M N$
\item[$\bullet$]
\textbf{function abstraction}

$\red{\lambda} x : A.\, M$
\item[$\bullet$]
\textbf{dependent product}

$\red{\Pi} x : A.\, M$
\end{itemize}
\vspace{-11pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{Coq syntax versus $\lambda P$ syntax}
\begin{center}
\begin{tabular}{rcl}
$\red{*}$ &$\green{\leftrightarrow}$& \texttt{\red{Set}} \\
$\red{*}$ &$\green{\leftrightarrow}$& \texttt{\red{Prop}} \\
$\red{\Box}$ &$\green{\leftrightarrow}$& \texttt{\red{Type}} \\
$x$ &$\green{\leftrightarrow}$& \texttt{x} \\
$M\,N$ &$\green{\leftrightarrow}$& \texttt{M N} \\
$\red{\lambda} x : A{.}\, M$ &$\green{\leftrightarrow}$& \texttt{\red{fun} x:A {=>} M} \\
$\red{\Pi} x : A{.}\, M$ &$\green{\leftrightarrow}$& \texttt{\red{forall} x:A{,} M}
\end{tabular}
\end{center}
\bigskip

\green{$\lambda P$ does not make the distinction between \texttt{Set} and \texttt{Prop}}
\vfill
\end{slide}

\begin{slide}
\slidetitle{pseudo-terms versus terms}
any expression according to the $\lambda P$ grammar is called a \red{pseudo-term}
$$\medskip
\green{\begin{array}{c}
(\Box\,*) \\
\lambda n : \mbox{nat}.\, \lambda x : n.\, x \\
(\lambda x : \mbox{nat}.\, x\,x)\,(\lambda x : \mbox{nat}.\, x\,x)
\end{array}}
$$

if also all types are okay, then the expression is called a \red{term}
$$\medskip
\green{\begin{array}{c}
\Box \\
\lambda n : \mbox{nat}.\, \mbox{nat} \\
(\lambda f : (\Pi m : \mbox{nat}.\, \mbox{nat}) .\, \lambda x : \mbox{nat}.\, f\,x)\,(\lambda n : \mbox{nat}.\, n) \\
(\lambda f : \mbox{nat}\to \mbox{nat} .\, \lambda x : \mbox{nat}.\, f\,x)\,(\lambda n : \mbox{nat}.\, n)
\end{array}}
\vspace{-5pt}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{contexts and judgments}

a \red{judgment} has the form
$\green{\Gamma \vdash M : N}$ \\
with $\Gamma$ a {context} and $M$ and $N$ terms
\medskip

a \red{context} $\Gamma$ is a {list of type {declarations}}
\medskip

a type \red{declaration} has the form
$\green{x : M}$ \\
with $x$ a variable name and $M$ a term
\adviwait
\bigskip
\begin{eqnarray*}
\green{A : *,\; P : (\Pi x : A.\, *),\; a : A} &\green{\vdash}& \green{(\Pi w : P\,a.\, *) : \Box} \\
\green{A : *,\; P : A \to *,\; a : A} &\green{\vdash}& \green{(P\,a) \to * : \Box}
\end{eqnarray*}
\vfill
\end{slide}

\begin{slide}
\slidetitle{the seven rules of $\lambda P$}
\begin{itemize}
\item[$\bullet$]
one rule for each kind of term
\begin{itemize}
\item
axiom rule (for the \red{sorts})
\item
\red{variable} rule
\item
\red{product} rule
\item
\red{abstraction} rule
\item
\red{application} rule
\end{itemize}
\item[$\bullet$]
two more rules
\begin{itemize}
\item
weakening rule (for the contexts)
\item
\green{conversion rule}
\end{itemize}
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rule 1: axiom}

$$
{
\over
\strut
\vdash
\red{*} : \Box
}
\bigskip
$$

gives the type of the \red{sort $*$}

\green{the only rule with no premises\exclspace!}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rules 2 and 3: variable and weakening}
\green{in these rules $s$ is either $*$ or $\Box$}

$$
{
\strut
\Gamma
\vdash
A : \green{s}
\over
\strut
\Gamma,\, x : A\,\vdash\, \red{x} : A
}
\medskip
$$

gives the type of the \red{variable $x$}
\adviwait
\bigskip

if the variable is not the last in the context we need the \red{weakening} rule

$$
{
\strut
\Gamma \,\vdash\, A : B
\qquad
\Gamma \,\vdash\, C : \green{s}
\over
\strut
\Gamma,\, \red{x : C} \,\vdash\, A : B
}
\bigskip
$$

%\green{the type of the type of a variable in a context is a sort}
%\vspace{-14pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rule 4: product}

$$
\gray
{
\strut
\Gamma \,\vdash\, A : *
\qquad
\Gamma \,\vdash\, B : s
\over
\strut
\Gamma
\vdash
{A \to B} : s
}
\bigskip
\adviwait
$$

$$
{
\strut
\Gamma \,\vdash\, A : *
\qquad
\Gamma,\, \green{x : A} \,\vdash\, B : {s}
\over
\strut
\Gamma \,\vdash\, \red{\Pi x : A.\, B} : {s}
}
\bigskip
$$

gives the type of a \red{dependent product}
%\adviwait

%\green{with this rule you cannot have functions that take \textbf{types} as argument\exclspace!}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rule 5: abstraction}

$$
\gray
{
\strut
\Gamma,\, x : A \,\vdash\, M : B
%\qquad
%\Gamma \,\vdash\, {A \to B} : {s}
\over
\strut
\Gamma \,\vdash\, {\lambda x : A.\, M} : {A \to B}
}
\bigskip
\adviwait
$$

$$
{
\strut
\Gamma,\, x : A \,\vdash\, M : B
\qquad
\Gamma \,\vdash\, \green{\Pi x : A.\, B} : {s}
\over
\strut
\Gamma \,\vdash\, \red{\lambda x : A.\, M} : \green{\Pi x : A.\, B}
}
\bigskip
$$

gives the type of a \red{function abstraction}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rule 6: application}

$$
\gray
{
\strut
\Gamma \,\vdash\, M : A \to B
\qquad
\Gamma \,\vdash\, N : A
\over
\strut
\Gamma \,\vdash\, {M N} : {B}
}
\bigskip
\adviwait
$$

$$
{
\strut
\Gamma \,\vdash\, M : \green{\Pi x : A.\, B}
\qquad
\Gamma \,\vdash\, N : A
\over
\strut
\Gamma \,\vdash\, \red{M N} : \green{B}\advirecord{a}{\rlap{$\green{[x := N]}$}}
}
\bigskip
$$

gives the type of a \red{function application}
\adviwait
\adviplay{a}
\vfill
\end{slide}

\begin{slide}
\slidetitle{rule 7: conversion}

$$
{
\strut
\Gamma \,\vdash\, A : \red{B}
\qquad
\Gamma \,\vdash\, B' : s
\over
\strut
\Gamma \,\vdash\, A : \red{B'}
}
\rlap{\qquad with $\red{B =_\beta B'}$}
\bigskip
$$

\green{is needed to make everything work}
\vfill
\end{slide}

\begin{slide}
\slidetitle{reduction and convertibility}

\begin{itemize}
\item[$\bullet$]
step
$$\dots ((\lambda x : A.\, M) N) \dots \; \red{\to_\beta} \; \dots (M[x := N]) \dots
\bigskip$$

\item[$\bullet$]
reduction
\quad
$\red{\tto_\beta}$

\green{zero or more steps}
\bigskip
\item[$\bullet$]
convertibility
\quad
$\red{=_\beta}$

\green{smallest equivalence relation}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\sectiontitle{cheat sheet}
\slidetitle{axiom, application, abstraction, product}
$$
{
\over
\strut
\vdash
\red{*} : \Box
}
$$

$$
{
\strut
\Gamma \,\vdash\, M : {\Pi x : A.\, B}
\qquad
\Gamma \,\vdash\, N : A
\over
\strut
\Gamma \,\vdash\, \red{M N} : {B}{\rlap{${[x := N]}$}}}
$$

$$
{
\strut
\Gamma,\, x : A \,\vdash\, M : B
\qquad
\Gamma \,\vdash\, {\Pi x : A.\, B} : {s}
\over
\strut
\Gamma \,\vdash\, \red{\lambda x : A.\, M} : {\Pi x : A.\, B}
}
$$

$$
{
\strut
\Gamma \,\vdash\, A : *
\qquad
\Gamma,\, {x : A} \,\vdash\, B : {s}
\over
\strut
\Gamma \,\vdash\, \red{\Pi x : A.\, B} : {s}
}
\vspace{-10pt}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{weakening, variable, conversion}
$$
{
\strut
\Gamma \,\vdash\, A : B
\qquad
\Gamma \,\vdash\, C : {s}
\over
\strut
\Gamma,\, \red{x : C} \,\vdash\, A : B
}
$$

$$
{
\strut
\Gamma
\vdash
A : {s}
\over
\strut
\Gamma,\, x : A\,\vdash\, \red{x} : A
}
$$
\vspace{0pt}

$$
{
\strut
\Gamma \,\vdash\, A : \red{B}
\qquad
\Gamma \,\vdash\, B' : s
\over
\strut
\Gamma \,\vdash\, A : \red{B'}
}
\rlap{\qquad with $\red{B =_\beta B'}$}
$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{examples}
\slidetitle{example 1}

$$\red{X : *,\, x : X \,\vdash\, x : X}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 2}

$$\red{X : * \,\vdash\, (X \to X) : *}$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{example 3}

$$\red{A : *,\; P : A \to *,\; a : A \,\vdash\, (P\,a) \to * : \Box}$$

\vfill
\end{slide}

\begin{slide}
\sectiontitle{Curry-Howard-de Bruijn for minimal predicate logic}
\slidetitle{introduction rules versus abstraction rule}
$$
{
\begin{array}{c}
[\green{A}^x] \\
\blue{\vdots} \\
\green{B}
\end{array}
\over
\strut
\red{A \to B}
}
\rlap{\enskip ${I[{x}]{\to}}$}
\hspace{6em}
{
\begin{array}{c}
\blue{\vdots} \\
\green{B}
\end{array}
\over
\strut
\red{\forall x.\, B}
}
\rlap{\enskip $I\forall$}
\bigskip
$$

$$
{
\strut
\Gamma,\, x : \green{A} \,\vdash\, \blue{M} : \green{B}
\qquad
\gray{\Gamma \,\vdash\, {\Pi x : A.\, B} : {s}}
\over
\strut
\Gamma \,\vdash\, \blue{\lambda x : A.\, M} : \red{\Pi x : A.\, B}
}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{elimination rules versus application rule}
$$
{
\begin{array}{c}
\blue{\vdots} \\
\green{A \to B}
\end{array}
\qquad
\begin{array}{c}
\blue{\vdots} \\
\green{A}
\end{array}
\over
\strut
\red{B}
}
\rlap{\enskip ${E{\to}}$}
\hspace{6em}
{
\begin{array}{c}
\vdots \\
\green{\forall x.\, B}
\end{array}
\over
\strut
\red{B[x:={N}]}
}
\rlap{\enskip $E\forall$}
\bigskip
$$

$$
{
\strut
\Gamma \,\vdash\, \blue{M} : \green{\Pi x : A.\, B}
\qquad
\Gamma \,\vdash\, \blue{N} : \green{A}
\over
\strut
\Gamma \,\vdash\, \blue{M N} : \red{{B}{\rlap{${[x := N]}$}}}
}
$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{examples}
\slidetitle{example 4}

$$\red{\forall x.\, (P(x) \to (\forall y.\, P(y) \to A) \to A)}$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{example 5}

$$\red{(\forall x.\, P(x) \to Q(x)) \to (\forall x.\, P(x)) \to \forall y.\, Q(y)}$$
\vfill
\end{slide}

\begin{slide}
\sectiontitle{logical framework}
\slidetitle{from automath to twelf}
\begin{itemize}
\item[$\bullet$]
\textbf{automath}

1968, de Bruijn \\
\green{start of proof checking of mathematics}

\item[$\bullet$]
\textbf{LF}

1987, Harper \& Honsell \& Plotkin \\
\green{framework for defining logics}

\red{the type of theory of LF is precisely $\lambda P$}

\item[$\bullet$]
\textbf{twelf}

1998, Pfenning \& Sch\"urmann \\
\green{current implementation of LF}
\end{itemize}

\vfill
\end{slide}

\begin{slide}
\slidetitle{logics in a logical framework}
\red{each logic has a $\lambda P$ context that contains syntax and rules of the logic}
\bigskip
\adviwait

\blue{\textbf{example:} minimal propositional logic as a $\lambda P$ context}

$$
\begin{array}{c}
\red{P} : *\adviwait\,,\\
\red{\mathord{\Rightarrow}} : P \to P \to P\adviwait\,,\\
\red{T} : P \to *\adviwait\,,\\
\red{I} : \Pi p : P.\, \Pi q : P.\, (T p \to T q) \to T (p \Rightarrow q)\,,\\
\red{E} : \Pi p : P.\, \Pi q : P.\, T (p \Rightarrow q) \to T p \to T q\adviwait\\
\green{\vdash} \\
\noalign{\vspace{-\medskipamount}}
\dots
\end{array}
$$

\vfill
\end{slide}

\begin{slide}
\slidetitle{logosphere}
Sch\"urmann, Pfenning, Kohlhase, Shankar, Owre
\medskip

\begin{center}
\red{making proof assistants talk to each other}
\bigskip
\medskip
\end{center}

\textbf{approach:}
\begin{itemize}
\item[$\bullet$]
define contexts for the logics of the various proof assistants in twelf
\item[$\bullet$]
import the libraries of the proof assistants in twelf
\end{itemize}
\bigskip

\textbf{see:}
\begin{center}
\green{\url{http://www.logosphere.org/}}
\end{center}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{the Barendregt cube}
\slidetitle{pure type systems}
Berardi \& Terlouw:
\medskip

\begin{center}
\green{framework for defining and studying typed $\lambda$-calculi}

\red{PTS = pure type system}
\bigskip
\end{center}

the PTS rules are exactly\gray{$^*$} the $\lambda P$ rules as presented here
\bigskip
\bigskip

\gray{($^*$ except for \textbf{one} symbol, in the product rule)}

\vfill
\end{slide}

\begin{slide}
\slidetitle{variations on the product rule}

$$
{
\strut
\Gamma \,\vdash\, A : \red{s_1}
\qquad
\Gamma,\, {x : A} \,\vdash\, B : \red{s_2}
\over
\strut
\Gamma \,\vdash\, {\Pi x : A.\, B} : \red{s_2}
}
\bigskip
$$

\begin{center}
\begin{tabular}{ll}
\green{$\lambda P$} & $\red{s_1} = *\,,\; \red{s_2} \in \{ *, \green{\Box} \}$ \adviwait\\
\noalign{\medskip}
& $(\red{s_1},\red{s_2}) \in \{ (*,*), \green{(*,\Box)} \}$ \adviwait\\
$\lambda{\to}$
& $(\red{s_1},\red{s_2}) \in \{ (*,*) \}$ \adviwait\\
$\lambda C$
& $(\red{s_1},\red{s_2}) \in \{ (*,*), \green{(*,\Box)}, (\Box,*), (\Box,\Box) \}$ \\
\end{tabular}
\end{center}
\vfill
\end{slide}

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

$$
\xymatrix@!{
 & \lambda\omega \ar@{->}[rr]\ar@{<-}'[d][dd]
   & & \red{\lambda C} \ar@{<-}[dd]
\\
 {\lambda2} \ar@{->}[ur]\ar@{->}[rr]\ar@{<-}[dd]|-{\mbox{{$\strut(\Box,*)$}}}
 & & \lambda P2 \ar@{->}[ur]\ar@{<-}[dd]
\\
 & \lambda\underline\omega \ar@{->}'[r][rr]
 & & \lambda P\underline\omega
\\
 {\lambda{\to}} \ar@{->}[rr]|-{\mbox{\green{$\,\strut(*,\Box)\,$}}}
   \ar@{->}[ur]|-(.54){\mbox{{$\strut(\Box,\Box)$}}}
 & & \green{\lambda P} \ar@{->}[ur]
}
\vspace{-8pt}
$$
\vfill
\end{slide}

\begin{slide}
\slidetitle{two schools of type theory}

$$
\hspace{-1em}
\xymatrix{
& *+<1em>\txt{\textbf{\red{automath}} \\\noalign{\smallskip} \green{Netherlands}}\ar[ddl]\ar[ddr] & \\ \\
*+\txt{\textbf{impredicative} \\ \textbf{type theory} \\ \noalign{\smallskip} \red{calculus of constructions} \\\noalign{\smallskip} \green{France}}
&&
*+\txt{\textbf{predicative} \\ \textbf{type theory} \\ \noalign{\smallskip} \red{Martin-L\"of's type theory} \\\noalign{\smallskip} \green{Sweden}}
}
\hspace{-1em}
$$
\vfill
\end{slide}

\end{document}