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

%% Time-stamp: <version du Thu 23 Nov 2000 à 10h19 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{Confluence du lambda-calcul}}

\author{}

\date{}

% \pagestyle{}

% \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{\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{Définitions préliminaires}
  \subsection{Propriété du losange} 
  C'est une propriété vérifiée par une relation $R$.\\
  \vskip 2 mm
  \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}
  \vskip 2 mm
%------------------------------------------------------

  \subsection{Confluence} 
  \vskip 2 mm

  \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}

  \vskip 3 mm

%------------------------------------------------------

  \subsection{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 une flèche existentielle.
  \end{enumerate}
 
%------------------------------------------------------

  \section{Confluence et convertibilité} 

\subsection{Théorème de Church-Rosser}
{\bf 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}

{\bf Démonstration}
\begin{itemize}
\item  $\Longleftarrow$ est évident\\
 car \bleu{\raraR 
  \subseteq \conv{R}} et \bleu{\conv{R}} est symétrique et
transitive. 

\item $\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}
\end{itemize}
 
\begin{itemize}
\item si \bleu{n=0} alors \bleu{M\xymatrix{&\ar@{>>}[l]^{R}}N} ou
    \bleu{M\raraR N}.
\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}
 
 
 
%------------------------------------------------------
  \subsection{Confluence et convertibilité} 
{\bf 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}
 
%------------------------------------------------------
  \section{Confluence de $\rightarrow_\beta$} 
{\bf Théorème :}

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

 
 
%------------------------------------------------------

\subsection{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[{o}] \bleu{\rapar} a la propriété du losange,
  \item[{o}] \bleu{\rarapar = \rarabeta}, 
    \begin{itemize}
    \item[{+}] donc \bleu{\rarabeta} a la propriété du losange, 
    \item[{+}] ce qui signifie que \bleu{\rabeta} est confluente.
  \end{itemize}
  \end{itemize}
\end{itemize}
 
 
%------------------------------------------------------
\subsection{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]]}}}\\

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

\begin{itemize}
\item \rouge{si 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}

\item
\rouge{si 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}
\item \rouge{si M est une application} , c'est facile.
\end{itemize}                                
 
 
%------------------------------------------------------
  \subsection{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}
 
%------------------------------------------------------
  \subsection{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}

 
%------------------------------------------------------
  \subsection{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


\vspace{10pt}

où \bleu{M^*} est un terme déterminé par \bleu{M} mais
\rouge{indépendant} de \bleu{N}.
\vskip 3 mm
\VERT{Intuitivement} \bleu{M^*} est le terme obtenu à partir de \bleu{M} en
contractant tous ses redex simultanément.
 
 
%------------------------------------------------------
\section{$M^*$}
  \subsection{La 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} 

%------------------------------------------------------
\subsection{Un résultat sur $M^*$}
  \begin{center}
    \framebox{\parbox{5 cm}{\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. On montre ici le cas 4.
\vskip 3 mm

{\bf Démonstration}

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}

 
 
%------------------------------------------------------
\end{document}