%% Time-stamp: <modified on 14 Dec 2004 at 09:08 by Pierre Lescanne>
%% types.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{color}
\usepackage{epsfig}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}

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


\slidesmag{5}
\articlemag{1}


\title{\color{red}{\textit{Systèmes de types}}}

\author{}

\date{}

\newcommand{\logoLIP}{\includegraphics*[height=0.04\textwidth]{lipllipl.eps}}
\newcommand{\logoENS}{\includegraphics*[height=0.04\textwidth]{liplensl.eps}}
\newcommand{\logos}{\hspace*{12pt}Cours de sémantique --- automne 2002\hfill\logoENS }


\newpagestyle{AvecLogos}%
  {\hfil \thepage \rightmark}
{\logos}


\pagestyle{AvecLogos}

%\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                couleurs
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\input{mes_couleurs}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                symobles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{"->"}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\x}{\ensuremath{\textbf{x}}}
\newcommand{\y}{\ensuremath{\textbf{y}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\sD}{\textbf{D}}
\newcommand{\sF}{\textbf{F}}
\newcommand{\A}{\ensuremath{{\cal A}}}
\newcommand{\B}{\ensuremath{{\cal B}}}
\newcommand{\T}{\ensuremath{{\cal T}}}
\newcommand{\N}{\ensuremath{{\cal N}}}
\newcommand{\SN}{\ensuremath{{\cal SN}}}
\newcommand{\X}{\ensuremath{{\cal X}}}
\newcommand{\Y}{\ensuremath{{\cal Y}}}
\newcommand{\I}{\ensuremath{{\cal I}}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.58em}\lambda}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\interp}[3]{#3\,\llbracket#1\rrbracket_{#2}}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                new qsymobls
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newqsymbol{`ù}{\upharpoonright}
\newqsymbol{"'|`"}{\uparrow}
\newqsymbol{"=^="}{\triangleq}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        les symboles pour les substitutions explicites
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\newcommand{\Lift}{\Uparrow\!\!}
\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}

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

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

%%%%%%%%%%%%%%%%%%% -- B --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\raB}{\rasub{B}}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                environnements
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\newenvironment{mathbleu}[1]{$\color{blue}#1}{$}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                headings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

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

 \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\,:\,
   \ifnum\timemm<10 0\fi\number\timemm}}

\begin{document}

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

\vfill 

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

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Huge \bf \color{vertfonce}{\textit{Types avec intersection}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les types avec intersection} On part du $`l$-calcul avec types simples et on
  l'\emph{enrichit} par un opérateur intersection \bleu{`^},
\begin{itemize}
\item pour servir de support à des modèles, (comme nous l'avons vu),
\item pour caractériser les termes fortement normalisables.
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les types avec intersection} On part du $`l$-calcul avec types simples et on
  l'\emph{enrichit} par un opérateur intersection \bleu{`^},
\begin{itemize}
\item pour servir de support à des modèles, (comme nous l'avons vu),
\item pour caractériser les termes fortement normalisables.
\end{itemize}

\vspace*{15pt}

Nous allons essentiellement nous intéresser à la \emph{normalisation forte}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les types avec intersection : système \sD}
\begin{small}
    \begin{center}
      \begin{mathbleu}
        \prooftree
        \justifies `G, x:`s "|-" x: `s 
        \using \emph{(Var)} \endprooftree
    \end{mathbleu}
    \qquad \qquad
    \begin{mathbleu}
      \prooftree `G, x:`s "|-" M : `t %
      \justifies `G "|-" `l x . M : `s "->" `t.  %
      \using \emph{(Abs)} \endprooftree
    \end{mathbleu}
    \end{center}
    
    \vspace*{2.5pt}

\begin{center}
  \begin{mathbleu}
    \prooftree %
    `G "|-" M : `s"->"`t \qquad `G "|-" N:`s %
    \justifies `G "|-" M\ N : `t  %
    \using \emph{(App)} \endprooftree
  \end{mathbleu}
\end{center}
\end{small}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les types avec intersection : système \sD}
\begin{small}
    \begin{center}
      \begin{mathbleu}
        \prooftree
        \justifies `G, x: `s  "|-" x: `s 
        \using \emph{(Var)} \endprooftree
    \end{mathbleu}
    \qquad \qquad
    \begin{mathbleu}
      \prooftree `G, x : `s "|-" M : `t %
      \justifies `G "|-" `l x . M : `s "->" `t.  %
      \using \emph{(Abs)} \endprooftree
    \end{mathbleu}
    \end{center}
    
    \vspace*{2.5pt}

\begin{center}
  \begin{mathbleu}
    \prooftree %
    `G "|-" M : `s"->"`t \qquad `G "|-" N:`s %
    \justifies `G "|-" M\ N : `t  %
    \using \emph{(App)} \endprooftree
  \end{mathbleu}
\end{center}

\vspace*{1.2pt}
{\color{brunfonce} \begin{center} \rule{4cm}{1.5pt}\end{center}}
\vspace*{1.2pt}

\begin{center}
  \begin{mathbleu}
    \prooftree %
    `G "|-" M : `s \qquad `G "|-" M:`t %
    \justifies `G "|-" M : `s `^ `t  %
    \using \emph{(`^~I)} \endprooftree
  \end{mathbleu}
\end{center}
    
    \vspace*{2.5pt}

\begin{center}
      \begin{mathbleu}
      \prooftree %
      `G "|-" M : `s `^ `t
      \justifies `G "|-" M : `s  %
      \using \emph{(`^~E_g)} \endprooftree
    \end{mathbleu}
    \qquad \qquad
    \begin{mathbleu}
      \prooftree %
      `G "|-" M : `s `^ `t
      \justifies `G "|-" M : `t  %
      \using \emph{(`^~E_d)} \endprooftree
    \end{mathbleu}

    \end{center}
%
  \end{small}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{On n'a plus de correspondance de Curry-Howard}
Le système \sD{} ne satisfait plus la correspondance de Curry-Howard.

\bigskip

Les règles $\emph{(`^~E_g)}$, $\emph{(`^~E_g)}$ et $\emph{(`^~I)}$ 
\ali ne «parlent» que du même terme.

\medskip

On perd la connexion terme et preuve.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Contraction et affaiblissement}
\emph{Lemme:} Si \bleu{`G "|-" M:`s} et si \bleu{x} n'apparaît pas
dans  \bleu{`G} %
\ali alors \bleu{`G, x:`t "|-" M:`s}.

\emph{Lemme:} Si \bleu{`G, x:`t "|-" M:`s} et si \bleu{x\notin FV(M)}
alors \bleu{`G "|-" M:`s}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Types de quelques termes}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}

\bigskip

  \begin{footnotesize}
    \begin{math}
      \hspace*{-30pt} \prooftree %
      \prooftree % 1
      \prooftree % 1.1
      x: `s \wedge (`s"->" `t) "|-" x: `s \wedge (`s"->" `t)
      \justifies x: `s \wedge (`s"->" `t) "|-" x: `s"->" `t \using
      \emph{(\wedge I_g)}%
      \endprooftree % 1.1
      \qquad %
      \prooftree % 1.2
      x: `s \wedge (`s"->" `t) "|-" x: `s \wedge (`s"->" `t)
      \justifies x: `s \wedge (`s"->" `t) "|-" x: `s %
      \using \emph{(\wedge I_d)} %
      \endprooftree % 1.2
      \justifies x: `s \wedge (`s"->" `t) "|-" x~x: `t %
      \using
      \emph{(Abs)} \endprooftree % 1
      \justifies "|-" `l x . x~x: (`s \wedge (`s"->" `t)) "->" `t
      \using \emph{(App)} %
      \endprooftree
    \end{math} %
  \end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\bigskip

  \begin{footnotesize}
    \begin{math}
      \hspace*{-30pt} \prooftree %
      \prooftree % 1
      \prooftree % 1.1
      x: `s \wedge (`s"->" `t) "|-" x: `s \wedge (`s"->" `t)
      \justifies x: `s \wedge (`s"->" `t) "|-" x: `s"->" `t \using
      \emph{(\wedge I_g)}%
      \endprooftree % 1.1
      \qquad %
      \prooftree % 1.2
      x: `s \wedge (`s"->" `t) "|-" x: `s \wedge (`s"->" `t)
      \justifies x: `s \wedge (`s"->" `t) "|-" x: `s %
      \using \emph{(\wedge I_d)} %
      \endprooftree % 1.2
      \justifies x: `s \wedge (`s"->" `t) "|-" x~x: `t %
      \using
      \emph{(Abs)} \endprooftree % 1
      \justifies "|-" `l x . x~x: (`s \wedge (`s"->" `t)) "->" `t
      \using \emph{(App)} %
      \endprooftree
    \end{math} %
  \end{footnotesize}

\bigskip

On n'arrivera pas à typer \bleu{(`l x . x~x)~(`l x . x~x)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\bigskip

  \begin{footnotesize}
    \begin{math}
      \hspace*{-10pt} %
      \prooftree %
      \prooftree % 1
      y: `a "|-" y: `a%
      \justifies "|-" `l y . y: `a "->" `a
      \using \emph{(Abs)} %
      \endprooftree % 1
      \qquad %
      \prooftree % 1
      y: `a "->" `a` "|-" y: `a "->" `a %
      \justifies "|-" `l y . y: (`a
      "->" `a)"->"(`a "->" `a) %
      \using\emph{(Abs)} %
      \endprooftree % 1
      \justifies "|-" `l y . y: (`a "->" `a) \wedge ((`a "->" `a)"->"(`a "->" `a))%
      \using \emph{(\wedge I)} %
      \endprooftree
    \end{math} %
  \end{footnotesize}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\bigskip

  \begin{footnotesize}
    \begin{math}
      \hspace*{-10pt} %
      \prooftree %
      \prooftree % 1
      y: `a "|-" y: `a%
      \justifies "|-" `l y . y: `a "->" `a
      \using \emph{(Abs)} %
      \endprooftree % 1
      \qquad %
      \prooftree % 1
      y: `a "->" `a` "|-" y: `a "->" `a %
      \justifies "|-" `l y . y: (`a
      "->" `a)"->"(`a "->" `a) %
      \using\emph{(Abs)} %
      \endprooftree % 1
      \justifies "|-" `l y . y: (`a "->" `a) \wedge ((`a "->" `a)"->"(`a "->" `a))%
      \using \emph{(\wedge I)} %
      \endprooftree
    \end{math} %
  \end{footnotesize}

\bigskip

donc

\medskip

\["|-"(`l x . x~x)~(`l y . y): `a "->" `a\]

en posant $`s :=  `a "->" `a$ et  $`t :=  `a "->" `a$.

\bigskip

Donc d'après le théorème que l'on va montrer tous ces termes sont
fortement normalisables.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Les typables sont
          fortement normalisables}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques définitions}
%
Soit \bleu{\N} une partie de \bleu{`L}.


\vspace*{2.5pt}

\emph{Définition:} Un partie \bleu{\X}  de \bleu{`L} est \bleu{\N}-\emph{saturée} si
\ali pour tous \bleu{M, P_1, ..., P_n `: `L} et tout  \bleu{N`:\N}
\begin{displaymathbleu}
  M[x:=N]~P_1 ... P_n `: \X \quad \Longrightarrow \quad (`l x . M)~N~P_1 ... P_n `: \X
\end{displaymathbleu}

\vspace*{2.5pt}

\emph{Définition:} \bleu{\X "`->" \Y \quad "=^=" \quad \{M `: `L ~|~ (`A N`: \X)\quad M~N `: \Y\}}.

\vspace*{2.5pt}

\emph{Remarque:} \bleu{\X ``(= \X'} et  \bleu{\Y ``(= \Y'} impliquent  \bleu{\X'"`->" \Y ``(= \X "`->" \Y'}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{8cm}{\emph{Proposition:}  Si \bleu{\Y} est \N-saturé, alors \bleu{\X "`->" \Y}
    est \N-saturé.
}}

\vspace*{20pt}

\framebox{\parbox{5.3cm}{\emph{Proposition:}  Si \bleu{\X} et \bleu{\Y}
    sont \N-saturés, \ali alors \bleu{\X \cap \Y}
    est \N-saturé.
}}
\vspace*{20pt}

\framebox{\parbox{7.5cm}{\emph{Proposition:}  Plus généralement, si les
    \bleu{\X_i} 
    sont \N-saturés, \ali alors \bleu{\bigcap_i \X_i}
    est \N-saturé.
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\N-interprétation} 
%
\emph{Définition:} Une \emph{\N-interprétation} est par définition une application,\\ % 
qui, à chaque type de base \bleu{o}, associe une partie \N-saturée de \bleu{`L}, %
\ali notée \bleu{\interp{o}{}{\I}}. %(ou \bleu{\interp{`a}{}{}} s'il n'y a pas d'ambiguïté).

\vspace*{2.5pt}

On étend les interprétations aux types.
\begin{itemize}
\item \bleu{\interp{`s "->" `t}{}{\I} = \interp{`s}{}{\I} "`->" \interp{`t}{}{\I}}.
\item  \bleu{\interp{`s `^ `t}{}{\I} = \interp{`s}{}{\I} \cap \interp{`t}{}{\I}}.
\end{itemize}
%
\vfill
Pour tout type \bleu{`s}, \bleu{\interp{`s}{}{\I}} est \N-saturé.

\begin{footnotesize}
   \hspace*{30pt} Par induction sur la structure des types.
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
%
  \framebox{\parbox{9.5cm}{\emph{Lemme d'adéquation:} Soit \bleu{\I} une interprétation telle que
      pour tout type \bleu{`s} du système \bleu{\sD}, on ait
    \bleu{\interp{`s}{}{\I} ``(= \N}.%
\ali Si \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD M:`s} et \bleu{P_1`:\interp{`s_1}{}{\I}},... ,  \bleu{P_k`:\interp{`s_k}{}{\I}},
\ali \emph{alors} \bleu{M [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}}.
  }}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\emph{Commentaire:} Pour les termes clos le théorème dit que \ali si \bleu{"|-"_\sD M:`s} alors \bleu{M
  `:\interp{`s}{}{\I}}.

Si on prouve que \bleu{M} est de type \bleu{`s} alors on montre que \bleu{M}  appartient au modèle de
\bleu{`s}.


\emph{Terminologie:} La terminologie \emph{adéquation} est celle de Krivine.  

Certains appellent ce lemme, \emph{lemme de correction} comme en logique.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
La démonstration est par induction sur la preuve du typage de \bleu{M}.

On examine la dernière règle utilisée.

\begin{itemize}
\item[\emph{$\bullet$}] La dernière règle utilisée est \emph{(Var)}. \\
  Alors \bleu{M} est l'une des variables \bleu{x_i}.  \\
  Donc on a \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD x_i:`s_i}\\
  et par hypothèse
    \begin{eqnarraybleu}
      M [x_1:=P_1]...[x_k:=P_k] &`=& x_i [x_1:=P_1]...[x_k:=P_k] \\
      &`=& P_i `: \interp{`s_i}{}{\I}
    \end{eqnarraybleu}
  \end{itemize}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
 \begin{itemize}
 \item [\emph{$\bullet$}] La dernière règle est \emph{(Abs)}, donc 
   \begin{itemize}
   \item \bleu{M `= `l x . M'} 
   \item et \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD `l x . M' :`s "->" `t}.
  \end{itemize}
    Par conséquent, \bleu{x_1:`s_1, ..., x_k:`s_k, x:`s "|-"_\sD M':`t}.   \\[2.97pt]
    \verdir{Soit un} \bleu{N} \verdir{quelconque} tel que \bleu{N `: \interp{`s}{}{\I}}.\\
    Par induction, \bleu{M'[x_1:=P_1]...[x_k:=P_k] [x:=N]`:\interp{`t}{}{\I}}.\\
    Puisque \bleu{\interp{`t}{}{\I}} est \N-saturé et que \bleu{\interp{`s}{}{\I} ``(= \N} donc que \bleu{N`:\N},\\
    on peut appliquer la définition de \N-saturation et l'on obtient \bleu{(`l x
      . M')[x_1:=P_1]...[x_k:=P_k] ~N`:\interp{`t}{}{\I}}.\\
    Comme \bleu{N} est quelconque, cela signifie que \bleu{(`l x
      . M')[x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I} "`->" \interp{`t}{}{\I}}.\\
    Or \bleu{\interp{`s}{}{\I} "`->" \interp{`t}{}{\I} = \interp{`s"->"`t}{}{\I}}.\\[3pt]
    Donc \bleu{(`l x . M')[x_1:=P_1]...[x_k:=P_k]`: \interp{`s"->"`t}{}{\I}}.
    
\end{itemize}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
 \begin{itemize}
 \item [\emph{$\bullet$}] La dernière règle est \emph{(App)}, donc 
   \begin{itemize}
   \item \bleu{M`= M_1~M_2},
   \item \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD M_1 :`t "->" `s},
   \item et \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD  M_2 :`t}.  
   \end{itemize}
   Par induction \bleu{M_1 [x_1:=P_1]...[x_k:=P_k]`:\interp{`t "->" `s}{}{\I}} %
   et \bleu{M_2 [x_1:=P_1]...[x_k:=P_k]`:\interp{`t}{}{\I}}.\\
   Puisque \bleu{\interp{`s}{}{\I} "`->" \interp{`t}{}{\I} = \interp{`s"->"`t}{}{\I}},
   on a \\\bleu{M_1 [x_1:=P_1]\ldots[x_k:=P_k]~M_2 [x_1:=P_1]\ldots[x_k:=P_k]}\ali \bleu{`:\interp{`s}{}{\I}}.\\[3pt]
   C'est-à-dire \bleu{M_1~M_2 [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}}.
 \end{itemize}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
 \begin{itemize}
 \item [\emph{$\bullet$}] La dernière règle est \emph{$(`^I)$}, donc \bleu{x_1:`s_1, ..., x_k:`s_k
     "|-"_\sD M :`s} et \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD  M :`t}.\\
   Par induction 
   \begin{itemize}
   \item \bleu{M [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}} 
   \item et \bleu{M
       [x_1:=P_1]...[x_k:=P_k]`:\interp{`t}{}{\I}}.
   \end{itemize}
   donc \bleu{M [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}\cap \interp{`t}{}{\I}`=\interp{`s`^`t}{}{\I}}.
 \item [\emph{$\bullet$}] La dernière règle est \emph{$(`^E_g)$}, donc \bleu{x_1:`s_1, ..., x_k:`s_k
     "|-"_\sD M :`s`^`t} et par induction  \bleu{M [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}\cap
     \interp{`t}{}{\I}}, \\donc \bleu{M [x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{}{\I}}.
 \end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Faire en sorte que les interprétation soit dans \N}
  On donne maintenant une truc pour obtenir un ensemble \bleu{\N} tel que pour toute
  \N-interprétation, on ait \bleu{\interp{`s}{}{\I} ``(= \N} pour tout type \bleu{`s} du système
  \bleu{\sD}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Couple adapté} 
\emph{Définition:}  Un couple \bleu{(\N_0, \N)}  de parties de \bleu{`L} est dit \emph{adapté} si 
\begin{enumerate}
\item \bleu{\N} est \N-saturé,
\item \bleu{\N_0 ``(= \N \qquad \N_0 ``(= (\N "`->" \N_0) \qquad (\N_0 "`->" \N) ``(= \N}.
\end{enumerate}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{9cm}{\emph{Lemme d'adaptation:}  Soit
    \begin{itemize}
    \item \bleu{(\N_0, \N)} un couple adapté,
    \item \bleu{\I} une \N-interprétation
    \end{itemize}
telle que pour tout type de base \bleu{o}, \bleu{\interp{o}{}{\I}} soit une partie \N-saturée
  de \bleu{\N} contenant \bleu{\N_0},%
  \ali alors pour tout type \bleu{`s}, %
  \ali \bleu{\interp{`s}{}{\I}} est une partie \N-saturée
  de \bleu{\N} contenant \bleu{\N_0}.%
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\bleu{\SN} = l'ensemble des termes \emph{fortement normalisables},

\bleu{\N_0} = l'ensemble des termes \bleu{x~M_1..M_n} tels que
\bleu{M_i`:\SN}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{4cm}{\emph{Proposition:}  \bleu{\SN} est \SN-saturé.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{4cm}{\emph{Proposition:}  \bleu{\SN} est \SN-saturé.}}

On veut montrer que pour tous \bleu{M, P_1, ..., P_n `: `L} et tout  \bleu{N`:\SN}
\begin{displaymathbleu}
  M[x:=N]~P_1 ... P_n `: \SN \quad \Longrightarrow \quad (`l x . M)~N~P_1 ... P_n `: \SN
\end{displaymathbleu}


On raisonne par induction sur \bleu{red(N) + red(M[x:=N]~~P_1 ... P_n)}.  
\ali où \bleu{red(Q)} est la somme des longueurs de toutes
les réductions \ali qui commencent en \bleu{Q}.

On considère tous les termes obtenus en contractant un redex de \bleu{(`l x . M)~N~P_1 ... P_n}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

 \begin{itemize}
 \item [\emph{$\bullet$}] On contracte le redex \bleu{(`l x . M)~N}. On obtient le terme
   \bleu{M[x:=N]~P_1 ... P_n} qui est dans \bleu{\SN} par hypothèse.
 \item  [\emph{$\bullet$}] On contracte un redex dans \bleu{M}, on obtient \bleu{M'}, on a
   \bleu{M[x:=N]~P_1 ... P_n \rabeta M'[x:=N]~P_1 ... P_n}, donc 

   \begin{center}
   \begin{Bleu}
     $red(N) + red(M[x:=N]~~P_1 ... P_n)$
       
     $``>$
       
     $red(N) + red(M'[x:=N]~~P_1 ... P_n),$
   \end{Bleu}
 \end{center}

   et l'on peut
   appliquer l'hypothèse d'induction.

   On obtient \bleu{(`l x . M')~N~P_1 ... P_n `: \SN}.
 \item  [\emph{$\bullet$}] On contracte un redex dans \bleu{P_i}, même démonstration.
   \end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

 \begin{itemize}
 \item [\emph{$\bullet$}] On contracte un redex dans \bleu{N}. On obtient le terme \bleu{N'}.  On
   voit que 
   \begin{center}
   \begin{Bleu}
     $red(N) + red(M[x:=N]~~P_1 ... P_n)$
       
     $``>$
       
     $red(N') + red(M[x:=N']~~P_1 ... P_n),$
   \end{Bleu}
 \end{center}

on peut appliquer l'hypothèse de récurrence.

On obtient \bleu{(`l x . M)~N'~P_1 ... P_n `: \SN}.

 \end{itemize}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{4.5cm}{\emph{Proposition:}  \bleu{(\N_0, \SN)} est adapté.% 
  }}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{4.5cm}{\emph{Proposition:}  \bleu{(\N_0, \SN)} est adapté.% 
  }}

La condition 1. est satisfaite par le proposition précédente.

\bleu{\N_0``(=\SN} car les termes de \bleu{\N_0} sont visiblement fortement normalisables.%

\bleu{\N_0``(=\SN "`->"\N_0} fait partie de la définition de \bleu{\N_0}.%


Pour montrer \bleu{\N_0 "`->"\SN ``(=\SN}, \\
supposons \bleu{M`:\N_0 "`->"\SN } qui ne soit pas fortement normalisable.  En revanche, quand on lui
applique un élément de \bleu{\N_0}, par exemple une variable \bleu{x}, on obtient \bleu{M~x} qui est fortement
normalisable.  \verdir{Contradiction}.


%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{8.7cm}{\emph{Théorème de normalisation forte:}  Tout
    terme typable du système \bleu{\sD} est fortement normalisable.
  }}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{8.7cm}{\emph{Théorème de normalisation forte:}  Tout
    terme typable du système \bleu{\sD} est fortement normalisable.
  }}

On définit la \SN-interprétation qui associe à un type de base \bleu{o}, l'ensemble  \bleu{\SN},
i. e. \bleu{\interp{o}{}{\I} = \SN}.

Soit \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sD M:`s}.

Par définition de \bleu{\N_0}, on a \bleu{x_i`:\N_0}, donc \bleu{x_i`:\interp{`s_i}{}{\I}}.

D'après le lemme d'adéquation, \bleu{M = M [x_1:=x_1]...[x_k:=x_k]`:\interp{`s}{}{\I}}.

Or d'après le lemme d'adaptation, \bleu{\interp{`s}{}{\I}``(=\SN}.

Donc \bleu{M`:\SN}.
%
\vfil
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Les fortement
          normalisables sont typables}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les formes normales sont typables}
%
On note \bleu{`G ```[ `D} un environnement tel que:
\begin{eqnarraybleu}
  `G ```[ `D &"=^="& \{x: `s `^ `t ~|~ x: `s `: `G \ \&\  x: `t `: `D\} \cup (`G \setminus `D) \cup (`D \setminus `G).
\end{eqnarraybleu}

\emph{Lemme:} Si \bleu{`G_1 "|-" M:`s} et \bleu{`G_2 "|-" M:`s} 
alors \bleu{`G_1 ```[ `G_2 "|-" M:`s}. %

\vspace*{20pt}

Un terme en forme normale est de la forme \bleu{`l x_1 ... x_n . x ~M_1 ... M_k}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{6.3cm}{\emph{Proposition:} Les formes normales sont typables.
  }}

On raisonne par induction sur la structure des formes normales. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
  Si \bleu{M `= `l y . M'} est une abstraction. 
  
  Alors par induction \bleu{`G, y: `s "|-" M: `t} et donc \bleu{`G"|-" `l y . M: `s"->"`t}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

Supposons que \bleu{M `= x ~M_1 ... M_k} n'est pas une abstraction.

Alors par induction \bleu{`G_1"|-" M_1:`s_1}, ..., \bleu{`G_k"|-" M_k:`s_k}.

Si \fbox{\bleu{x`: `G_1 \cup ... \cup `G_k}} donc \bleu{x`: `G_1 ```[ ... ```[ `G_k} où \bleu{x} a un
  type \bleu{`s}. 

\medskip

Posons \bleu{`G "=^=" \{x: `s `^ (`s_1 "->" ... "->" `s_k "->" o)\} \cup (`G_1 ```[
    ... ```[ `G_k) \setminus \{x: `s\}}.

\medskip

On voit  que 
\begin{itemize}
\item \bleu{`G"|-" x:`s_1 "->" ... "->" `s_k "->" o}, 
\item \bleu{`G"|-" M_1:`s_1}
\item  et \bleu{`G"|-" M_k:`s_k}.
\end{itemize}
Donc on peut prouver que \bleu{`G"|-" x ~M_1 ... M_k:`t}.
\vfill
%
\end{slide}
%------------------------------------------------------
\begin{slide}

Soit \bleu{o} est un type de base.

\medskip

Si \fbox{\bleu{x`; `G_1 \cup ... \cup `G_k}} Posons \bleu{`G "=^=" \{x: `s_1 "->" ... "->" `s_k "->"
  o\} \cup (`G_1 ```[ ... ```[ `G_k)}.\\
On voit que
\begin{itemize}
\item \bleu{`G"|-" x:`s_1 "->" ... "->" `s_k "->" o}, 
\item \bleu{`G"|-" M_1:`s_1}
\item  et \bleu{`G"|-" M_k:`s_k}.
\end{itemize}
Donc on peut prouver que \bleu{`G"|-" x ~M_1 ... M_k:o}.
\vfill
%
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les stratégies perpétuelles}
%
Une \emph{stratégie perpétuelle} est une façon de trouver le redex à contracter pour réduire un
terme sans détruire la \emph{non forte normalisation}.
\begin{displaymathbleu}
  C[(`l x . M)~N] "-{_{perp}}>" C[M[x:=N]].
\end{displaymathbleu}
Si \bleu{C[(`l x . M)~N]} n'est pas fortement normalisable,  \ali alors
\bleu{C[M[x:=N]]} ne l'est pas non plus.

Ou encore si \bleu{C[M[x:=N]]} est fortement normalisable, \ali alors
\bleu{C[(`l x . M)~N]} est fortement normalisable.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les stratégies perpétuelles}
%
Une stratégie perpétuelle préserve la forte normalisation par expansion.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exemple~1}
%
Parmi ces réductions,
\begin{small}
\begin{eqnarraybleu}
  (`l x y . y)~((`l z . z z z)~(`l u . u u )) &\rabeta& `l y . y \\
  &\rabeta& (`l x y . y)~((`l u . u u)~(`l u . u u )~(`l u . u u ))
\end{eqnarraybleu}
\end{small}
la deuxième est perpétuelle, tandis que la première ne l'est pas.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exemple~2}
%
\begin{footnotesize}
Parmi ces réductions,
\begin{eqnarraybleu}
  (`l x . x ~(`l y . y y))~(`l z . \K z ( z z)) &\rabeta& (`l z . \K z
  (z z))~(`l y . y y)   \\
  &\rabeta& \K (`l y . y y)~((`l y . y y) (`l y . y y)) \\
  &\rabeta& \K (`l y . y y)~((`l y . y y) (`l y . y y)) \quad \rabeta
  \quad \ldots \\[1pt]
  &{\color{brunfonce} \rule{1cm}{1.5pt}}&\\[1pt]
  (`l x . x ~(`l y . y y))~(`l z . \K z ( z z)) &\rabeta& (`l x . x ~(`l y . y y))~(`l z . z) \\
  &\rabeta& (`l z . z) ~(`l y . y y) \\
  &\rabeta& `l y . y y.
\end{eqnarraybleu}
C'est la  première qui est perpétuelle.
\end{footnotesize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exemple~2 (continué)}
%
\begin{footnotesize}
On aurait pu continuer
\begin{eqnarraybleu}
   \K (`l y . y y)~((`l y . y y) (`l y . y y)) &\rabeta& (`l y . y y)
\end{eqnarraybleu}
Mais là encore on n'aurait pas appliqué une stratégie perpétuelle.
\end{footnotesize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Redex perpétuel}
%
On écrit \bleu{NF} l'ensemble des formes normales.

On peut définir un \emph{redex perpétuel} \bleu{perp(M)} dans un terme \bleu{M} qui n'est pas en forme
normale de la façon suivante:
\begin{small}
\begin{eqnarraybleu}
  perp(`l x . M) &=& perp(M)\\
  perp((`l x . P)~N) &=& (`l x . P)~N \textrm{\color{black}~si~} x`:FV(P) \textrm{\color{black}~ou~}
  (P`:NF \textrm{\color{black}~et~}  N`:NF)\\
  \textrm{\emph{sinon}}&&\\
  perp(M~N) &=& perp(N)  \quad \textrm{\color{black}~si~} N`;NF\\
  perp(M~N) &=& perp(M) \quad \textrm{\color{black}~autrement}.
\end{eqnarraybleu}
\end{small}
Une \emph{stratégie perpétuelle} est une réduction qui réduit à chaque étape un redex perpétuel.
%
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Stratégie perpétuelle et typage}
%
Si \bleu{\SN} est l'ensemble des termes fortement normalisables.

 \bleu{\SN} est plus petit point fixe de l'équation.
\begin{displaymathbleu}
  \SN = NF \cup \{M `: `L~|~ M "-{_{perp}}>" N \ \&\ N`:\SN\}
\end{displaymathbleu}
\emph{Remarque:} les typables sont obtenus \verdir{en itérant des expansions
perpétuelles à partir des formes normales.}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{7cm}{\emph{Lemme:} Si \bleu{x`:FV(M)} et
      \bleu{`G "|-" M[x:=N]:`t}, alors il existe un environnement \bleu{`G'} et un type
      \bleu{`s} tel que
      \begin{itemize}
      \item 
        \bleu{`G' "|-" N:`s} 
      \item et \bleu{`G', x: `s "|-" M:`t} 
    \end{itemize}
  }}

La démonstration est par induction sur la structure de \bleu{M}.

Si \bleu{M} est une \emph{variable}, alors cette variable est \bleu{x}
\ali puisque \bleu{x`:FV(M)}.\\ %
Donc \bleu{M`= x} alors \bleu{M[x:=N] `= N}.  On prend \bleu{`s = `t}
et \bleu{`G=`G'}.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Si \bleu{M} est une \emph{abstraction} \bleu{`l y. M'} alors \bleu{M[x:=N] `=
  `l y. (M'[x:=N])} et \bleu{`t} est de la forme \bleu{`t_1"->"`t_2} avec \bleu{`G "|-" `l
  y. (M'[x:=N]):`t_1"->"`t_2}.  \\ %
Puisque \bleu{`G, y:`t_1 "|-" M'[x:=N]:`t_2}, \\% 
par induction, il existe
un environnement \bleu{`G'} tel que \bleu{`G',y: `t_1 "|-" N:`s} et
\bleu{`G', y: `t_1, x: `s "|-" M':`t_2}. \\ %
Par la convention de Barendregt \bleu{y`; FV(N)}.  \\ %
Donc \bleu{`G'"|-" N:`s} et \bleu{`G',x: `s "|-" `l y .M':`t_1"->"`t_2}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Si \bleu{M} est une \emph{application} \bleu{M_1~M_2} alors \bleu{M[x:=N] `=
  (M_1[x:=N])~(M_2[x:=N])}. \\ %
Donc il existe 
\begin{itemize}
\item \bleu{`G "|-" M_1[x:=N]:`t'"->"`t} 
\item et \bleu{`G "|-" M_2[x:=N]:`t'}.
\end{itemize}
                                % 

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Si \bleu{x`;M_1} et \bleu{x`:M_2}, alors 
\begin{itemize}
\item \bleu{M_1[x:=N] `= M_1}
\item \bleu{`G "|-" M_1:`t'"->"`t}
\end{itemize}
et il
existe un environnement \bleu{`G'} tel que 
\begin{itemize}
\item \bleu{`G' "|-" N:`s} 
\item et \bleu{`G', x: `s "|-" M_2:`t'}.
\end{itemize}
Donc \bleu{(`G```[ `G'), x: `s "|-" M_1:`t'"->"`t} %
\ali et \bleu{(`G```[ `G'), x: `s "|-" M_2:`t'}. 

Ainsi \bleu{(`G```[ `G'), x: `s "|-" M_1~M_2:`t}.

Si \bleu{x`:M_1} et \bleu{x`;M_2}, la démonstration est similaire.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
  Si \bleu{x`:M_1} et \bleu{x`:M_2}, et il existe des environnements
  \bleu{`G'_1} et \bleu{`G'_2} tels que 
  \begin{itemize}
  \item \bleu{`G'_1 "|-" N:`s_1} et \bleu{`G'_1, x: `s_1 "|-" M_1:`t'"->"`t},
  \item \bleu{`G'_2 "|-" N:`s_2} et \bleu{`G'_2, x: `s_2 "|-" M_2:`t'}.
\end{itemize}
Donc 
\begin{itemize}
\item \bleu{`G'_1 ```[ `G'_2 "|-" N:`s_1`^ `s_2}, 
\item \bleu{`G'_1```[ `G'_2 , x: `s_1 `^ `s_2"|-" M_1:`t'"->"`t}, %
  \footnote{A prouver, mais vous me l'acheter!}
\item \bleu{`G'_1```[ `G'_2 , x: `s_1 `^ `s_2"|-" M_2:`t'}, $^\mathsf{a}$
\end{itemize}
puis \bleu{`G'_1```[ `G'_2 , x: `s_1 `^ `s_2"|-" M_1~M_2:`t}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{6.3cm}{\emph{Proposition:} Si \bleu{P} est typable
    et si \bleu{Q "-{_{perp}}>" P}% 
\ali alors \bleu{Q} est typable.
  }}

La démonstration est par induction sur la structure de \bleu{P}.

Si \bleu{P} est une \emph{abstraction}, donc \bleu{P`=`l x . P'}, alors
\bleu{Q' "-{_{perp}}>" P'} avec \bleu{Q`=`l x . Q'}.\\ %
Puisque \bleu{P} est typable, \bleu{P'} est typable.  \\ %
Par induction \bleu{Q'} est typable et clairement \bleu{Q} est
typable.

\bigskip

Si \bleu{P} est une \emph{application} \bleu{M~N}, telle que le redex
perpétuel se situe dans \bleu{M} ou \bleu{N}, le résultat vient
clairement par induction.


%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Supposons donc que \bleu{P} est le redex perpétuel.
\begin{itemize}
\item[\emph{$\bullet$}] Si \bleu{P `= (`l x . M')~N} avec \bleu{M'`:NF} et \bleu{N`:NF}, \ali le résultat
  se démontre facilement.
  
\item[\emph{$\bullet$}] Si \bleu{P `= (`l x . M')~N} avec \bleu{x`:FV(M')} et \bleu{Q`=M'[x:=N]}.
  
  En appliquant le lemme, on démontre qu'il existe 
  \begin{itemize}
  \item \bleu{`G' "|-" N:`s} 
  \item et \bleu{`G', x:`s "|-" M':`t}.
\end{itemize}
  
  On en déduit que \bleu{`G'"|-" `l x. M':`s"->"`t}.
  
  Par conséquent, \bleu{`G'"|-" (`l x. M')~N:`t}.
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{5.7cm}{\emph{Théorème:} Si \bleu{M} est fortement normalisable \ali alors  \bleu{M} est
    typable dans \sD.
  }}
%

Grâce à la proposition précédente et à la remarque.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Caractérisation des fortement normalisables}
%
\vspace*{20pt}
  \begin{center}
    \framebox{\parbox{5cm}{
    \begin{center}
      Un terme est fortement normalisable
      
      si et seulement si
      
      il est typable dans \sD
  \end{center}
}}
\end{center}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Huge \bf \color{vertfonce}{\textit{Le système \sF}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}
Le système de type admet maintenant des quantifications.

Par exemple, on veut pouvoir écrire %
\bleu{"|-" `l x . x: `A `a . (`a "->" `a)}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}
\begin{small}
    \begin{center}
      \begin{mathbleu}
        \prooftree
        \justifies `G, x: `s "|-" x: `s 
        \using \emph{(Var)} \endprooftree
    \end{mathbleu}
    \qquad \qquad
    \begin{mathbleu}
      \prooftree `G, x "|-" M : `t %
      \justifies `G "|-" `l x . M : `s "->" `t.  %
      \using \emph{(Abs)} \endprooftree
    \end{mathbleu}
    \end{center}
    
    \vspace*{2.5pt}

\begin{center}
  \begin{mathbleu}
    \prooftree %
    `G "|-" M : `s"->"`t \qquad `G "|-" N:`s %
    \justifies `G "|-" M\ N : `t  %
    \using \emph{(App)} \endprooftree
  \end{mathbleu}
\end{center}

\vfill

\begin{center}
  \begin{mathbleu}
    \prooftree %
    `G "|-" M : `s
    \justifies `G "|-" M : `A `a .`s %
    \using \emph{(`A~I)}  \qquad \textrm{\color{black} si~} `a
    \textrm{\color{black} ~n'est libre dans aucun des types de~} `G  %
\endprooftree
  \end{mathbleu}
\end{center}

\vspace*{2.5pt}

\begin{center}
      \begin{mathbleu}
      \prooftree %
      `G "|-" M : `A `a . `s 
      \justifies `G "|-" M : `s [`a:=`t]  %
      \using \emph{(`A~E)} \endprooftree
    \end{mathbleu}
    \end{center}
%
  \end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}
\vfill
\begin{center}
      \begin{mathbleu}
      \prooftree %
      \prooftree %%
      x : `a "|-" x : `a %
      \justifies "|-" `l x . x : `a "->" `a %
      \using \emph{(Abs)} 
      \endprooftree %%
      \justifies  "|-" `l x . x : `A `a . (`a "->" `a) %
      \using \emph{(`A~I)} 
      \endprooftree %
    \end{mathbleu}
    \end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}
\vfill
\begin{scriptsize}
\begin{center}
      \begin{mathbleu}
      \prooftree %
      \prooftree %%
       \prooftree %%%
      \vdots %
      \justifies "|-" `l x . x : `A `a . (`a "->" `a) %
      \using \emph{(`A I)}
      \endprooftree %%%
      \justifies "|-" `l x . x : `A `a . (`a "->" `a)  "->" `A `a . (`a "->" `a) %
      \using \emph{(`A E)}
      \endprooftree %%
      \qquad
      \prooftree %%
      \vdots %
      \justifies "|-" `l y . y : `A `a . (`a "->" `a) %
      \using \emph{(`A I)}
      \endprooftree %%
      \justifies  "|-" (`l x . x) ~(`l y . y) : `A `a . (`a "->" `a) %
      \using \emph{(App)}
      \endprooftree %
    \end{mathbleu}
    \end{center}
  \end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}

\begin{center}
      \begin{mathbleu}
      \prooftree %
      \prooftree %%
      \prooftree %%% 1
      x :`A `a . `a "|-" x :`A `a . `a  %
      \justifies x :`A `a . `a "|-" x : `a "->" `b %
       \using \emph{(`A~E)} 
     \endprooftree %%% 1
      \qquad
      \prooftree %%% 2
        x :`A `a . `a "|-" x :`A `a . `a %
        \justifies x :`A `a . `a   "|-" x : `a %
       \using \emph{(`A~E)} 
     \endprooftree %%% 2
        \justifies x : `A `a . `a "|-" x x : `b  %
      \using \emph{(App)} 
      \endprooftree %%
      \justifies  "|-" `l x . x x : (`A `a . `a) "->" `b  %
       \using \emph{(Abs)} 
     \endprooftree %
    \end{mathbleu}
    \end{center}
\vfill
\emph{Remarque:} Le type \bleu{(`A `a . `a)} n'est habité par aucun terme clos.  

On l'utilise pour noter la contradiction.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}

\begin{tiny}
  \begin{center} \hspace*{-25pt}
    \begin{mathbleu}
         \prooftree %
      \prooftree %%
      \prooftree %%% 1
      x :`A `a .  (`a "->" `a) "|-" x : `A `a .  (`a "->" `a) 
      \justifies x :`A `a .  (`a "->" `a) "|-" x : `A `a. (`a"->"`a) "->" `A `a. (`a"->"`a)
       \using \emph{(`A~E)} 
     \endprooftree %%% 1
     % 
      x :`A `a . (`a "->" `a)   "|-" x :`A `a .  ( `a "->" `a)%
      \justifies x : `A `a .  (`a "->" `a) "|-" x x :   `A `a .  (`a "->" `a) %
      \using \emph{(App)} 
      \endprooftree %%
      \justifies  "|-" `l x . x x : `A `a. (`a"->"`a) "->" `A `a. (`a"->"`a)
       \using \emph{(Abs)} 
     \endprooftree %
       \end{mathbleu}
 \end{center}
\end{tiny}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le système \sF}

\bleu{(`l x . x x)~(`l x . x x)}  n'est pas typable dans le système
\sF.

\bigskip

En revanche, \bleu{(`l x . x x)~(`l x . x)} est typable dans le
système \sF.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Réduction du sujet dans \sF}

\framebox{\parbox{7.5cm}{Si \bleu{\Gamma \vdash_\sF M:\sigma} et si
    \bleu{M\rabeta N} alors \bleu{\Gamma \vdash_\sF N:\sigma}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Les typables du système \sF{} \\ sont
          fortement normalisables}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La difficulté de la preuve de forte normalisation} 
%
  En général, quand on définit l'interprétation des types \ali on la
  définit par \verdir{des interprétations sur des types plus simples}.

L'interprétation \bleu{\interp{`A `a . `s}{`r}{\I}} ressemble à une
intersection et on veut la définir par
\begin{displaymathbleu}
  \interp{`A `a . `s}{`r}{\I} = \bigcap_{`t~\textrm{\color{black}\scriptsize types}} \interp{`s}{\modval{`r}{`a}{ \interp{`t}{`r}{\I}}}{\I}
\end{displaymathbleu}
Mais cette définition conduit à un cercle vicieux.

Car \bleu{`t} peut être \bleu{`A `a . `s} lui-même.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La difficulté de la preuve de forte normalisation} 
%
Une telle théorie est dite \emph{imprédicative}.

Pour résoudre ce problème, Jean-Yves Girard a défini les
\emph{candidats de réductibilité}.  %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Là aussi on considère la paire adaptée:

\bleu{\SN} = l'ensemble des termes \emph{fortement normalisables},

\bleu{\N_0} = l'ensemble des termes \bleu{x~M_1..M_n} tels que
\bleu{M_i`:\SN}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétations}
%
Soit \bleu{\I} une interprétation 
\begin{eqnarraybleu}
  `r: &Var& "->" \textrm{\color{black} parties \SN-saturées de \SN qui
    contiennent $\N_0$}\\
  &`a& "|->" `r(`a) 
\end{eqnarraybleu}
On a donc \bleu{\N_0``(=`r(`a)``(=\SN}.%

On modifie une valuation comme d'habitude
\begin{displaymathbleu}
  \modval{`r}{`a}{\A} =\left\{
    \begin{array}[c]{l@{\quad}l}
      `r(`b) & \textrm{if~} `b \not`= `a \\ %
      \A & \textrm{if~} `b `= `a
    \end{array}
  \right.
\end{displaymathbleu}
\bleu{\A} est une partie de \bleu{`L} qui est \SN-saturée et qui contient $\N_0$.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétations}
%
On définit l'interprétation d'un type comme suit:
  \bl{\begin{center}
  \begin{math}
    \begin{array}[c]{l@{\qquad\quad}l}
\hline
`s  &  \interp{`s}{}{`r}\\
\hline
`a  &  `r(`a)\\
`s_1 "->" `s_2  &  \interp{`s_1}{`r}{\I} "`->" \interp{`s_2}{`r}{\I} \\
`A `a  . `s & \bigcap_\A \interp{`s}{\modval{`r}{`a}{\A}}{\I}
    \end{array}
  \end{math}
\end{center}
} L'intersection est prise sur toutes les parties \bleu{\A} qui sont 
\SN-saturées et qui contiennent $\N_0$.  %

\begin{footnotesize}
\emph{Remarque:} Dans la suite \bleu{\bigcap_\A} signifiera que l'intersection est prise sur toutes les parties \bleu{\A} qui sont 
\SN-saturées et qui contiennent $\N_0$.    
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{5cm}{\emph{Proposition 1:} Pour tout \bleu{`s}, 
\begin{itemize}
\item \bleu{\interp{`s}{`r}{\I}} est \SN-saturé 
\item et \bleu{\N_0 ``(= \interp{`s}{`r}{\I} ``(= \SN}% 
\end{itemize}}}

Si \rouge{$`s `= `a$} est une variable, \bleu{\interp{`s}{`r}{\I} = `r(`a)} et
ça vient par définition des valuations.

Si \rouge{$`s `=`s_1 "->" `s_2$}, par induction \bleu{\N_0 ``(=
  \interp{`s_1}{`r}{\I} ``(= \SN} et \bleu{\N_0 ``(=
  \interp{`s_2}{`r}{\I} ``(= \SN} donc 
\begin{displaymathbleu}
  \N_0x ``(= \SN "`->" \N_0 ``(=  \interp{`s_1}{`r}{\I} "`->"
  \interp{`s_2}{`r}{\I} ``(= \N_0 "`->" \SN ``(= \SN.
\end{displaymathbleu}
\bleu{\interp{`s}{`r}{\I} = \interp{`s_1}{`r}{\I} "`->"
  \interp{`s_2}{`r}{\I}} est \verdir{\SN-saturé}  provient
\begin{itemize}
\item d'un des premiers lemmes sur la saturation
\item et du fait que par induction \bleu{\interp{`s_2}{`r}{\I}} est
  \SN-saturé.
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Si \rouge{$`s `= `A `a . `t$} alors
\begin{displaymathbleu}
  \interp{`s}{`r}{\I} = \bigcap_{\A} \interp{`t}{\modval{`r}{`a}{\A}}{\I}.
\end{displaymathbleu}
Par induction, chaque \bleu{\interp{`t}{\modval{`r}{`a}{\A}}{\I}} est \SN-saturé
\ali et \bleu{\N_0 ``(= \interp{`t}{\modval{`r}{`a}{\A}}{\I} ``(=\SN}. 

Clairement 
\begin{mathbleu}
  \N_0 ``(=  \bigcap_\A \interp{`t}{\modval{`r}{`a}{\A}}{\I} ``(=  \SN
\end{mathbleu}.

\begin{mathbleu}
\bigcap_\A \interp{`t}{\modval{`r}{`a}{\A}}{\I}
\end{mathbleu} est \SN-saturé, comme intersection de \SN-saturés.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7.2cm}{\emph{Proposition 2:}
    \bleu{\interp{`s[`a:=`t]}{`r}{\I} =
      \interp{`s}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}}.
}}

La démonstration est classique.

Si \rouge{$`s `= `a$} est une variable, facile!

Si \rouge{$`s `=`s_1 "->" `s_2$} 
\begin{eqnarraybleu}
  \interp{(`s_1"->"`s_2)[`a:=`t]}{`r}{\I} &=& \interp{`s_1[`a:=`t]"->"`s_2[`a:=`t]}{`r}{\I} \\
  &=&\interp{`s_1[`a:=`t]}{`r}{\I} "`->" \interp{`s_2[`a:=`t]}{`r}{\I} \\
  &=& \interp{`s_1}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}  "`->" \interp{`s_2}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}\\
  &=& \interp{`s_1"->"`s_2}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}
\end{eqnarraybleu}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Si \rouge{$`s `= `A `b . `s'$} alors
\begin{eqnarraybleu}
  \interp{(`A `b . `s')[`a:=`t]}{`r}{\I} &=& \interp{`A `b . (`s'[`a:=`t])}{`r}{\I}\\
  &=& \bigcap_\A \interp{`s'[`a:=`t]}{\modval{`r}{`b}{\A}}{\I} \\
  &=& \bigcap_\A \interp{`s'}{\modval{\modval{`r}{`b}{\A}}{`a}{\interp{`t}{\modval{`r}{`b}{\A}}{\I}}}{\I}\\
  &=& \bigcap_\A \interp{`s'}{\modval{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{`b}{\A}}{\I}\\
  &=& \interp{`A `b . `s'}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}
\end{eqnarraybleu}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
  \framebox{\parbox{9.5cm}{\emph{Lemme d'adéquation:} Soit \bleu{\I}
      une interprétation et \bleu{`r} une valuation
\ali Si \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sF M:`s} %
\ali et \bleu{P_1`:\interp{`s_1}{`r}{\I}},... , \bleu{P_k`:\interp{`s_k}{`r}{\I}}, %
\ali \emph{alors} \bleu{M[x_1:=P_1]...[x_k:=P_k]`:\interp{`s}{`r}{\I}}.  }}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Par induction sur la preuve de \bleu{x_1:`s_1, ..., x_k:`s_k "|-"_\sF M:`s}.

Pour les règles \emph{(Var)}, \emph{(Abs)} et \emph{(App)}, la démonstration est la même que pour le
lemme d'adéquation du système \sD.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
 \begin{itemize}
 \item [\emph{$\bullet$}] La dernière règle est \emph{$(`A~I)$}.   Posons \bleu{`s`=`A `a . `s'}.\\
   Par hypothèse d'induction, \bleu{M[x_1:=P_1]...[x_k:=P_k]`:\interp{`s'}{`r}{\I}}.
   
   Mais comme \bleu{`a} n'est libre dans aucun des \bleu{`s_i}, \\
   pour tout \bleu{\A}, \SN-saturé, tel que \bleu{\N_0``(=\A``(=\SN}, \\
   on a \bleu{\interp{`s_i}{`r}{\I} =
     \interp{`s_i}{\modval{`r}{`a}{\A}}{\I}}. \\
   Donc pour tout \bleu{\A} \SN-saturé, tel que \bleu{\N_0``(=\A``(=\SN},\ali
   \bleu{\small P_1`:\interp{`s_1}{`r}{\I}},... , \bleu{P_k`:\interp{`s_k}{`r}{\I}} implique \ali
   \bleu{\small M[x_1:=P_1]...[x_k:=P_k]`: \interp{`s'}{\modval{`r}{`a}{\A}}{\I}}. 

    Donc \ali
   \bleu{\small P_1`:\interp{`s_1}{`r}{\I}},... , \bleu{P_k`:\interp{`s_k}{`r}{\I}} implique \ali
   \bleu{\small M[x_1:=P_1]...[x_k:=P_k]`: \bigcap_\A \interp{`s'}{\modval{`r}{`a}{\A}}{\I}}
   \hspace*{125pt} \bleu{"=^="\ \interp{`A `a . `s'}{`r}{\I}}

 %  &=& \interp{`A `a . `s'}{`r}{\I}.
 \end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
 \begin{itemize}
 \item [\emph{$\bullet$}] La dernière règle est \emph{$(`A~E)$}.  Posons \bleu{`s`=`s'[`a:=`t]}.\\
   Par hypothèse d'induction,
   \begin{eqnarraybleu}
     M[x_1:=P_1]...[x_k:=P_k]&`:&\interp{`A `a . `s'}{`r}{\I}\\& =& \bigcap_\A \interp{`s'}{\modval{`r}{`a}{\A}}{\I}
\end{eqnarraybleu}
   C'est-à-dire que pour tout \bleu{\A}, \SN-saturé, tel que \bleu{\N_0``(=\A``(=\SN},\\
   on a \bleu{M[x_1:=P_1]...[x_k:=P_k]`:\interp{`s'}{\modval{`r}{`a}{\A}}{\I}}.\\
   Donc a fortiori,
\begin{eqnarraybleu}
  M[x_1:=P_1]...[x_k:=P_k]&`:&\interp{`s'}{\modval{`r}{`a}{\interp{`t}{`r}{\I}}}{\I}\\ 
    &=& \interp{`s'[`a:=`t]}{}{\I}.
\end{eqnarraybleu}
La dernière égalité provient de la proposition~2.

 \end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{8.7cm}{\emph{Théorème de normalisation forte:}  Tout
    terme typable du système \bleu{\sF} est fortement normalisable.
  }}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\framebox{\parbox{8.7cm}{\emph{Théorème de normalisation forte:}  Tout
    terme typable du système \bleu{\sF} est fortement normalisable.
  }}
%

On considère la valuation \bleu{`r_\SN} qui associe l'ensemble
\bleu{\SN} à chaque variable de type \bleu{`a}.

\bleu{x_i`:\interp{`s_i}{`r_\SN}{\I}} car d'après la proposition 2,
\bleu{\N_0``(= \interp{`s_i}{`r_\SN}{\I}}%

Donc d'après le lemme d'adéquation, on a \bleu{M
  [x_1:=x_1]...[x_k:=x_k]`= M `:\interp{`s}{`r_\SN}{\I}}.

Mais \bleu{\interp{`s}{`r_\SN}{\I}``(= \SN}.

Donc \bleu{M`:\SN}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Types de données}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Parties saturées}
%
Une partie de \bleu{`L} est \emph{saturée} si
\ali pour tous \bleu{M, P_1, ..., P_n, N `: `L}
\begin{displaymathbleu}
  M[x:=N]~P_1 ... P_n `: \X \quad \Longrightarrow \quad (`l x . M)~N~P_1 ... P_n `: \X
\end{displaymathbleu}
%
On définit les interprétations comme précédemment,%
\ali sauf qu'on remplace «\N-saturé» par «saturé».

Il y a un lemme d'adéquation avec le même énoncé et la même démonstration que précédemment.

Si \bleu{`s} est un type clos, \bleu{\interp{`s}{`r}{\I}} ne dépend pas de \bleu{`s}. %
\ali Donc on le note \bleu{\interp{`s}{}{\I}}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Types de données}
%
Un type clos est un \emph{type de données} si 
\begin{itemize}
\item \bleu{\interp{`s}{}{\I}``/= \emptyset},
\item tout terme de  \bleu{\interp{`s}{}{\I}} est $`b$-convertible à un terme clos.
\end{itemize}

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Types de données}
%
\begin{itemize}
\item \bleu{Id "=^=" `A `a . (`a "->" `a)} est le type de l'identité,%
  \ali  
  \begin{footnotesize}\bleu{M`: \interp{Id}{}{\I} \quad "<=>" \quad M \conv{`b} `l x . x}.
  \end{footnotesize}
\item \bleu{Bool "=^=" `A `a . (`a "->" `a "->" `a)} est le type des booléens, %
  \ali 
  \begin{footnotesize}
    \bleu{M`: \interp{Bool}{}{\I} \ "<=>" \ M \conv{`b} `l x y. x} ou \bleu{M \conv{`b} `l x
      y. y}. %
  \end{footnotesize}
\item \bleu{Nat "=^=" `A `a . ((`a "->" `a) "->" (`a "->" `a))} est le type des entiers, %
  \ali 
  \begin{footnotesize}
    \bleu{M`: \interp{Nat}{}{\I} \ "<=>"} il existe un entier \bleu{n} tel que \ali \qquad \bleu{M \conv{`b} `l
      f x . f (...{\color{black} \scriptstyle n \textrm{\tiny ~fois}}.. (f x)...)} ou \bleu{M \conv{`b} `l f . f}. %
\end{footnotesize}
\end{itemize}
%
\vfill
\end{slide}
\end{document}

% LocalWords:  cardinalité approxime sup bottom Fix Ap réflexif Retracts FV Var
% LocalWords:  retract valuation réflexivité s'évalue pt d'Engeler Scott
% LocalWords:  typable
