%% /home/plescann/MIM-1/LOGIQUE/LAMBDA/transp.tex

%% Time-stamp: <version du Thu 23 Nov 2000 à 10h22 par Pierre Lescanne>

% \documentclass[%
%   slidesonly,%  Pour sortir les transparents seuls
%   semrot,%      Permettre des rotations eventuelles
%   semhelv,%    Helvetica
%   a4%           A4 paper
%   ]{seminar}
\documentclass{article}
\usepackage{fancybox}
\usepackage{fullpage}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}

% %% Time-stamping  
% %% compute the time in hours and minutes; 
%  \newcount\timehh\newcount\timemm \timehh=\time 
%  \divide\timehh by 60 \timemm=\time
%  \count255=\timehh\multiply\count255 by -60 \advance\timemm by \count255
%  \newcommand{\timestamp}
%  { {\protect\small\sl\today\ -- 
%  \ifnum\timehh<10 0\fi\number\timehh\,h\,
%    \ifnum\timemm<10 0\fi\number\timemm}}
%                                           % avec dvips

% \def\printlandscape{\special{landscape}}    % pour sortir en landscape
%                                             % avec dvips

% \slidesmag{5}
% \articlemag{1}

% \rotateheaderstrue       % si tu combines slide et slide*


\title{{\textit{Lambda-calcul simplement typé}}}

\author{}

\date{}


% \slidestyle{empty}

% \slideframe{}   

\newcommand{\rouge}[1]{{\color{red}#1}}
\newcommand{\VERT}[1]{{\color{green}#1}}
\newcommand{\bleu}[1]{\textcolor{blue}{$#1$}}
\newcommand{\rougeMa}[1]{\textcolor{red}{$#1$}}
\newcommand{\bl}[1]{\textcolor{blue}{#1}}
\newcommand{\Ra}{\ensuremath{\Rightarrow}}
\newcommand{\fleche}{\rightarrow}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\eqa}{\mathop{\equiv_\alpha}}
\newcommand{\Y}{\mathsf{Y}}


\newcommand{\inferTwoLabel}[4]{
{#1} \quad 
 \bl{\begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

\newcommand{\leafLabel}[2]{
 {#1} \quad
  \bl{\begin{array}{c}
  #2
  \end{array}}}

\newcommand{\inferLabel}[3]{
    {#1} \quad 
    \bl{\begin{array}{c}
      #2\\
      \hline \noalign{\vskip 1pt}#3
    \end{array}
  }}

 \newcommand{\inferTwo}[3]{\bl{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}}

 \newcommand{\infer}[2]{\bl{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<<->>}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%%% Les fleches %%%%%%%%%%%%%

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix{&\ar@{>>}[l]^{R}_+}}
\newcommand{\plusraraR}{\rarasupsub{+}{R}}
\newcommand{\rapar}{\xymatrix @ -1.5pc {\ar@{>}[rr]&||&}}
\newcommand{\rarapar}{\xymatrix @ -1.5pc {\ar@{>>}[rr]&||&}}

% %%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
% \newcommand{\heading}[1]{%      % ca c'est des commandes a moi
%   \begin{center}                % mais ca peut t'interesser
%     \large\bf
%     \color{cyan}{\shadowbox{#1}}%
%   \end{center}
%   \markright{#1}
%   \vspace{1ex minus 1ex}}

% \newcommand{\subheading}[1]{%
%   \begin{center}
%     \color{green}{\bf\Ovalbox{#1}}
%   \end{center}}

\begin{document}
\maketitle

% %------------------------------------------------------
% \section
%   \maketitle \addtocounter{slide}{-1} \slidepagestyle{empty}


%   

% \hfill\textit{\footnotesize version du \timestamp}

 
%------------------------------------------------------
\section{Introduction}

\subsection{Introduction au typage}
\bleu{\Omega} et \bleu{\Y}  contiennent des termes qui s'appliquent à
eux-mêmes.  

Le \rouge{paradoxe du barbier} est:

\begin{quotation}
\VERT{Le barbier rase tous ceux qui ne se rasent pas eux-mêmes. \emph{Qui rase le
barbier} ?}
\end{quotation}

Pour éviter les paradoxes, on cherche à éviter de tels termes.

On va donc \rouge{typer} les termes.

C'est aussi bien pour la programmation. 
 
%------------------------------------------------------
\subsection{Objectifs du typage}
Le typage a donc deux objectifs:
\begin{itemize}
\item préserver la correction, \VERT{rien de mauvais ne peut arriver},
\item préserver la terminaison, \VERT{toutes les réductions se terminent}. 
\end{itemize}
\vspace*{8pt}
En $\lambda$-calcul la \rouge{terminaison} s'appelle la \rouge{normalisation forte}.
 
%------------------------------------------------------
  \subsection{Notion d' environnement} 

Il faut typer les variables libres, il faut donc faire des hypothèses
sur les types de ces variables.

D'où la notion d'\rouge{environnement}.

Un environnement est un ensemble d'association de types à des variables.

\bl{
\begin{displaymath}
  \label{eq:env}
  \Gamma \equiv x_1:\sigma_1,...,x_n:\sigma_n
\end{displaymath}}
 
%------------------------------------------------------
  \subsection{Les types} 
Un \rouge{jugement} est l'affirmation du type \bleu{\sigma} d'un terme
\bleu{M} sous un certain environnement \bleu{\Gamma}:
\bl{
\begin{displaymath}
  \label{eq:jug}
  \Gamma \vdash M:\sigma
\end{displaymath}}
Les types sont
\begin{itemize}
\item soit des variables \bleu{\alpha},
\item soit des types applications \bleu{\sigma \fleche \tau}.
\end{itemize}
 
%------------------------------------------------------
  \subsection{Les règles} 
\[\leafLabel{\mbox{(Var)}}{\Gamma, x:\sigma \vdash x:\sigma}\]

\[\inferLabel{\mbox{(Abs)}}{\Gamma, x:\sigma \vdash
  M:\tau}{\Gamma\vdash \lambda x:\sigma . M:\sigma\fleche\tau}\]

\[\inferTwoLabel{\mbox{(App)}}{\Gamma\vdash
  M:\sigma\fleche\tau}{\Gamma\vdash N:\sigma}{\Gamma\vdash M N :
  \tau}\]

 
%------------------------------------------------------
\section{Exercices et théorèmes}
  \subsection{Exercices} 
Typez les termes 
\begin{itemize}

\item \bleu{B\equiv \lambda x y z. x (y z)}, 

\item \bleu{I \equiv \lambda x. x},

\item \bleu{C\equiv \lambda x y z. x z y}, 

\item \bleu{K \equiv \lambda x y . x}, 

\item \bleu{S \equiv \lambda x y z . x z (y z)}.

\item \bleu{I I \equiv (\lambda x. x)(\lambda x. x)}.

  
\item \bleu{\textbf{2}\textbf{2} \equiv (\lambda f x. f(f x))
    (\lambda f x. f(f x))}.
\end{itemize}

A-t-on le même type pour \bleu{I} (resp. \bleu{\textbf{2}}) dans 
  chaque cas?
\vskip 3 mm
\VERT{Conclusion :}  Le système de types simples n'est pas assez général.  Il
ne permet d'affecter un type unique à chaque terme.
 
 
%------------------------------------------------------
\subsection{Théorèmes}

 
 
%------------------------------------------------------
\framebox{\parbox{8.5cm}{Si \bleu{\Gamma, x:\sigma \vdash M:\tau} et
    \bleu{\Gamma\vdash N:\sigma} alors \bleu{\Gamma\vdash
      M[x:=N]:\tau}}}\\

{\bf Démonstration :}  Par induction sur \bleu{M}.


 
\section{Réduction du sujet} 
\vskip 2 mm
{\bf Lemme} \VERT{Réduction du sujet}

La $\beta$-réduction préserve le type.
\vskip 2 mm
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}
\vskip 2 mm
{\bf Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x:\tau.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x:\tau.M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.

\item \rouge{$M\equiv (\lambda x:\tau.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x:\tau.M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.

\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\end{itemize}
 
\vskip 2 mm
%------------------------------------------------------
\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash N:\sigma}.}}
\vskip 2 mm
{\bf Démonstration :}  Par induction sur la définition de
\bleu{M\rabeta N}.  
\begin{itemize}
\item \rouge{$M\equiv (\lambda x:\tau.M_1) M_2$} \\\bleu{\Gamma\vdash
    (\lambda x:\tau.M_1) M_2:\sigma} vient de \bleu{\Gamma, x:\tau
    \vdash M_1:\sigma} et de \bleu{\Gamma \vdash M_2:\tau}.\\
D'autre part \bleu{N\equiv M_1[x:=M_2]}\\ or d'après le lemme
\bleu{\Gamma\vdash M_1[x:=M_2]:\sigma}.
\item \rouge{$M\equiv M_1 M_2$} avec  \rouge{$N\equiv N_1 M_2$} et
  \rouge{$M_1\rabeta N_1$}.\\
\bleu{\Gamma\vdash M} vient de \bleu{\Gamma\vdash
  M_1:\tau\fleche\sigma} et \bleu{\Gamma\vdash M_2:\tau}, \\par
induction  \bleu{\Gamma\vdash
  N_1:\tau\fleche\sigma} et donc \bleu{\Gamma\vdash N_1 M_2:\sigma}.
\item \rouge{Les autres cas sont similaires.}
\end{itemize}
  
 
%------------------------------------------------------
\subsection{Commentaires}
\begin{itemize}
\item Si un terme est d'un certain type, \rouge{il n'en sortira pas} par
  $\beta$-réduction. 
\item Si un terme a une forme normale et s'il a un type, alors \rouge{sa
  forme normale a ce type}.
\end{itemize}
 
 
%------------------------------------------------------
  \section{L'isomorphisme de Curry-Howard} 
\begin{small}
\begin{math}
\begin{array}{c | c}
\leafLabel{\mbox{\VERT{(Var)}}}{\Gamma,\rouge{ x:}~\sigma \vdash \rouge{x:}~\sigma} & \bl{\Gamma, p \vdash p}\\

\inferLabel{\mbox{\VERT{(Abs)}}}{\Gamma, \rouge{x:}~\sigma \vdash
 \rouge{M:}~\tau}{\Gamma\vdash \rouge{\lambda x:\sigma . M:}~\sigma\fleche\tau} 
& \inferLabel{\VERT{\Ra I}}{\Gamma, p \vdash q}{\Gamma\vdash p\Ra q} \\

\inferTwoLabel{\mbox{\VERT{(App)}}}{\Gamma\vdash
 \rouge{M:}~\sigma\fleche\tau}{\Gamma\vdash \rouge{N:}~\sigma}{\Gamma\vdash \rouge{M N :}~
  \tau} & \inferTwoLabel{\VERT{\Ra E}}{\Gamma\vdash p\Ra q}{\Gamma\vdash
  p}{\Gamma\vdash q} \\
\end{array}
\end{math}
\end{small}
 
\vskip 3 mm
Dans \bleu{\Gamma\vdash \rouge{M:}~\sigma}, 
\begin{itemize}
\item  \rouge{M:} est une \rouge{annotation} qui est le \rouge{«terme de preuve»},

\item \bleu{\sigma} peut-être vu comme un \rouge{type} ou comme une \rouge{proposition}.
\end{itemize}

\vskip 3 mm

On obtient le tableau de correspondance:

\vspace*{5pt}


\begin{center}
\begin{tabular}{c | c}
\VERT{types} & \VERT{propositions}\\
\VERT{termes} & \VERT{preuves}\\
\VERT{réduction} & \VERT{simplification des preuves}
\end{tabular}
\end{center}
 
%------------------------------------------------------
\section{Normalisation forte}
{\bf Définition :}\\
Un terme \bleu{M} est \VERT{fortement normalisable} si
toute suite de réductions \bleu{M \rabeta M_1 \rabeta ...\rabeta M_n
  ...} est finie.

\vspace{10pt}

{\bf Théorème :}\\
Si \bleu{\Gamma \vdash \tau} alors \bleu{M} est
\VERT{fortement normalisable}.
 
 
%------------------------------------------------------
\end{document}