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

%% Time-stamp: <modifié par Pierre Lescanne le  6 Nov 2002 à 15h38>

\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}
\usepackage{qsymbols}

%% 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{\color{red}{\textit{Confluence du lambda-calcul}}}

\author{}

\date{}

\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   

\definecolor{mauve}{rgb}{1,0,1}
\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{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\eqa}{\mathop{\equiv_\alpha}}
\newcommand{\Y}{\mathsf{Y}}
\newcommand{\ali}{\newline\hspace*{20pt}}


\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]{%
{\color{mauve}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

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

\begin{document}

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


\vfill 

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

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Propriété du losange} 

\vspace*{50pt}

\xymatrix{
& M \ar[dl]_{R}\ar[dr]^{R} && \bl{\Longrightarrow \exists P} & N_1 \ar[dr]^{R}&& N_2\ar[dl]_{R} \\
N_1 && N_2  &&&  P}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Confluence} 

\vspace*{50pt}

\xymatrix{
& M \ar@{>>}[dl]_{R}\ar@{>>}[dr]^{R} && \bl{\Longrightarrow \exists P} & N_1 \ar@{>>}[dr]^{R}&& N_2\ar@{>>}[dl]_{R} \\
N_1 && N_2  &&&  P}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Remarques} 
  \begin{enumerate}
  \item \bleu{\raR} est confluente si \bleu{\raraR} a la propriété du
    losange.

  \item Parfois on note la confluence :

    \begin{center}
\mbox{
      \xymatrix{& \ar@{>>}[dl]\ar@{>>}[dr]\\ \ar@{.>>}[dr] &&
        \ar@{.>>}[dl]\\ &&}
}
    \end{center}

où \bleu{\xymatrix{\ar@{.>>}[r]&}} est un flèche existentielle.
  \end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Confluence et convertibilité} 
\rouge{Théorème (Church-Rosser):}
\begin{center}
  \framebox{\parbox{8cm}{Si \bleu{R} est
      \VERT{confluente} alors\\
      \bleu{M\conv{R}N} \rouge{$\Longleftrightarrow$} \bleu{\exists P
        (M\raraR P \wedge N\raraR P)}.}}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{center}
  \framebox{\parbox{8cm}{Si \bleu{R} est
      \VERT{confluente} alors\\
      \bleu{M\conv{R}N} \rouge{$\Longleftrightarrow$} \bleu{\exists P
        (M\raraR P \wedge N\raraR P)}.}}
\end{center}

\rouge{Démonstration :}  $\Longleftarrow$ est évident car \bleu{\raraR 
  \subseteq \conv{R}} et \bleu{\conv{R}} est symétrique et
transitive. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{center}
  \framebox{\parbox{8cm}{Si \bleu{R} est
      \VERT{confluente} alors\\
      \bleu{M\conv{R}N} \rouge{$\Longleftrightarrow$} \bleu{\exists P
        (M\raraR P \wedge N\raraR P)}.}}
\end{center}

\rouge{Démonstration :}    
$\Longrightarrow$. Par induction sur le nombre de «pics» dans
 \bleu{M\conv{R}N}. Soit

\begin{scriptsize}
    \bleu{M\plusararR M_1 \plusraraR N_1...\plusararR M_i
     \plusraraR N_1 ...} \\
\hspace*{2pt}\hfill \bleu{... N_{n-1}\plusararR M_n \plusraraR
     N_n\xymatrix{&\ar@{>>}[l]^{R}}N}
 \end{scriptsize}
 
\begin{itemize}
\item si \bleu{n=0} alors \bleu{M\xymatrix{&\ar@{>>}[l]^{R}}N} ou
    \bleu{M\raraR N}.
  \end{itemize}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{center}
  \framebox{\parbox{8cm}{Si \bleu{R} est
      \VERT{confluente} alors\\
      \bleu{M\conv{R}N} \rouge{$\Longleftrightarrow$} \bleu{\exists P
        (M\raraR P \wedge N\raraR P)}.}}
\end{center}

\rouge{Démonstration :} $\Longrightarrow$. 

\begin{itemize}
\item si \bleu{n\not=0}, par confluence, dans 
\begin{tiny}
    \bleu{M\plusararR M_1 \plusraraR N_1...N_{n-1}\plusararR M_n \plusraraR
     N_n\xymatrix{&\ar@{>>}[l]^{R}}N}
 \end{tiny}
il existe \bleu{M_n'} tel que 
\bleu{  N_{n-1} \plusraraR M_n' \plusararR
     N_n\xymatrix{&\ar@{>>}[l]^{R}}N} 

et 

\begin{scriptsize}
\bleu{M\plusararR M_1 \plusraraR N_1...\plusararR M_i
     \plusraraR N_1 ...} \\
\hspace*{2pt}\hfill \bleu{... N_{n-1}\plusraraR M_n' \plusararR
     N_n\xymatrix{&\ar@{>>}[l]^{R}}N}
 \end{scriptsize}

a un pic de moins, donc on a le résultat par induction.
\end{itemize}
\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Confluence et convertibilité} 

\vspace*{20pt}

\rouge{Corollaire :} Si \bleu{R} est confluente
\begin{enumerate}
\item Si \bleu{N} est une forme normale de \bleu{M} alors 
\bleu{M \raraR N}.
\item Un terme a au plus une forme normale.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Confluence de $\rightarrow_\beta$} 
\rouge{Théorème :}

\begin{center}
  \framebox{\parbox{3cm}{\bleu{\rabeta} est confluent}}
\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\subheading{Remarques préliminaires}
\begin{itemize}
\item Si \bleu{\raR} a la propriété du losange, alors \bleu{\raraR} a
  la propriété du losange.
\item \bleu{\rabeta} n'a pas la propriété du losange. Pourquoi ?
\item Il faut donc trouver une relation \bleu{\rapar} telle que
  \begin{itemize}
  \item[\rouge{o}] \bleu{\rapar} a la propriété du losange,
  \item[\rouge{o}] \bleu{\rarapar = \rarabeta}, 
    \begin{itemize}
    \item[\VERT{+}] donc \bleu{\rarabeta} a la propriété du losange, 
    \item[\VERT{+}] ce qui signifie que \bleu{\rabeta} est confluente.
  \end{itemize}
  \end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Lemme de substitution} 
 \framebox{\parbox{7.5cm}{Si \bleu{x\not\in FV(L)} alors\\\
\bleu{M[x:=N][y:=L] \equiv M[y:=L][x:=N[y:=L]]}}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \framebox{\parbox{7.5cm}{Si \bleu{x\not\in FV(L)} alors\\\
\bleu{M[x:=N][y:=L] \equiv M[y:=L][x:=N[y:=L]]}}}
\rouge{Démonstration :} Par induction sur la structure de \bleu{M}.

\rouge{M est une variable}
\begin{itemize}
\item \VERT{$M\equiv x$}, les deux côtés valent \bleu{N[y:=L]},
\item \VERT{$M\equiv y$}, les deux côtés valent \bleu{L},
\item \VERT{$M\equiv z$}, les deux côtés valent \bleu{z},
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \framebox{\parbox{7.5cm}{Si \bleu{x\not\in FV(L)} alors\\\
\bleu{M[x:=N][y:=L] \equiv M[y:=L][x:=N[y:=L]]}}}
\rouge{Démonstration :} Par induction sur la structure de \bleu{M}.

\rouge{M est une abstraction} \bleu{M\equiv \lambda z.M_1}.
\begin{scriptsize}
\bl{
\begin{eqnarray*}
M[x:=N][y:=L] &\equiv & (\lambda z.M_1)[x:=N][y:=L]\\
              &\equiv & \lambda z.(M_1[x:=N][y:=L])\hspace*{5pt} \mbox{\VERT{(par
                définition)}}\\
              &\equiv & \lambda z.(M_1[y:=L][x:=N[y:=L]])\hspace*{5pt} \mbox{\VERT{(par
                induction)}}\\
              &\equiv & (\lambda z.M_1)[y:=L][x:=N[y:=L]]\hspace*{5pt} \mbox{\VERT{(par
                définition)}}
\end{eqnarray*}
}
\end{scriptsize}
\rouge{M est une application} facile.
                                
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Définition de la réduction parallèle} 
\begin{scriptsize}
\[\leafLabel{\mbox{(réflexivité)}}{M\rapar M}\]
\[\inferTwoLabel{\mbox{(APP-congruence)}}{M\rapar M'}{N\rapar N'}{M N
    \rapar M' N'}\]
\[\inferLabel{\mbox{(ABS-congruence)}}{M\rapar M'}{\lambda x.M\rapar
  \lambda x.M'}\]
\[\inferTwoLabel{\mbox{($\beta$-parallèle)}}{M\rapar M'}{N\rapar
  N'}{(\lambda x.M) N
    \rapar M'[x:=N']}\]
\end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Trois résultats} 
  \begin{enumerate}
  \item Si \bleu{M\rabeta M'} alors \bleu{M\rapar M'}\\
    \hfill c'est-à-dire\begin{scriptsize}{\bleu{\rabeta\subseteq\rapar}}
      \end{scriptsize}
    \item Si \bleu{M\rapar M'} alors \bleu{M\rarabeta M'}\\
    \hfill c'est-à-dire\begin{scriptsize}{\bleu{\rapar\subseteq\rarabeta}}
      \end{scriptsize}
      
  \item Si \bleu{M\rapar M'} et \bleu{N\rapar N'} alors
    \hspace*{10pt}\bleu{M[x:=N]\rapar M'[x:=N']}
  \end{enumerate}

\vspace{5pt}
\VERT{En exercice.}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Une propriété plus forte} On prouve une propriété
  \rouge{plus forte} (due à M.~Takahashi)
\\\hspace*{10pt}que la \VERT{propriété du losange}
  pour \bleu{\rapar} :

\vspace{10pt}

\hspace*{25pt}$\bl{M\rapar N} \Longrightarrow \bl{N\rapar M^*}$\hfill
\VERT{(*)} 

\vspace{10pt}

où  \bleu{M^*} est un terme déterminé par \bleu{M} mais \rouge{indépendant} de
\bleu{N}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Une propriété plus forte} On prouve une propriété
  \rouge{plus forte} \\\hspace*{10pt}que la \VERT{propriété du losange}
  pour \bleu{\rapar} :

\vspace{10pt}

\hspace*{25pt}$\bl{M\rapar N} \Longrightarrow \bl{N\rapar M^*}$\hfill
\VERT{(*)} 

\vspace{10pt}

où \bleu{M^*} est un terme déterminé par \bleu{M} mais
\rouge{indépendant} de \bleu{N}.

\VERT{Intuitivement} \bleu{M^*} est le terme obtenu à partir de \bleu{M} en
contractant tous ses redex simultanément.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le définition de $M^*$} 
  \begin{enumerate}
  \item \bleu{x^*\equiv x}
  \item \bleu{(\lambda x.M)^* \equiv \lambda x. M^*}
  \item \bleu{(M_1 M_2)^* \equiv M_1^* M_2^*} si \bleu{M_1M_2} n'est
    pas un redex.
  \item \bleu{((\lambda x. M_1) M_2)^*\equiv M_1^*[x:=M_2^*]}
  \end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercices} 
Calculer
\begin{enumerate}
\item \bleu{((`l x . x)~((`l yzu . y~(z~u))~ a b c))^*}
\item \bleu{((`l x . x~x)~ (`l y . y~y))^*}
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    \framebox{\parbox{5cm}{\bleu{M\rapar N} $\Longrightarrow$
        \bleu{N\rapar M^*}.}}
\end{center}

Les cas correspondant aux parties 1., 2. et 3. de la définition
\bleu{M^*} sont laissés en exercice.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    \framebox{\parbox{5cm}{\bleu{M\rapar N} $\Longrightarrow$
        \bleu{N\rapar M^*}.}}
\end{center}

Si \bleu{M\equiv ((\lambda x. M_1) M_2) \rapar N}, alors \rouge{deux cas}
pour \bleu{N},
\begin{itemize}
\item \bleu{N\equiv (\lambda x. N_1) N_2}
\item \bleu{N\equiv N_1[x:=N_2]}
\end{itemize}
dans les deux cas, il y a des \bleu{N_i} (i=1 ou i=2) tels que
\bleu{M_i\rapar N_i}.  

Par induction, \bleu{N_i\rapar M_i^*}.

Pour chaque cas :
\begin{itemize}
\item Si \bleu{N\equiv (\lambda x. N_1) N_2} alors \bleu{N\rapar
    M_1^*[x:=M_2^*]\equiv M^*}.
\item Si \bleu{N\equiv N_1[x:=N_2]},alors nous avons \bleu{N\rapar
    M_1^*[x:=M_2^*]\equiv M^*}, par le résultat 3.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Résumons}
De la propriété \VERT{(*)} pour \bleu{\rapar}

on déduit la propriété du losange pour \bleu{\rapar}

de laquelle on déduit la propriété du losange pour \bleu{\rarapar}

de laquelle on déduit la propriété du losange pour \bleu{\rarabeta} 
\ali parce que \bleu{\rarabeta = \rarapar},

qui est la confluence de \bleu{\rabeta}.

Donc \bleu{\rabeta} est confluent.

\rouge{C.q.f.d.}
\vfill
\end{slide}
%------------------------------------------------------
\end{document}
