%% Time-stamp: <modified on  4 Oct 2004 at 17:05 by Pierre Lescanne>
%% /MIM-1/REECRITURE/red_abst.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

%\renewenvironment{slide}[1]{#1} 
%\def\printlandscape{}  % pour sortir en portrait
%\slidesmag{1} 
%\usepackage{fullpage}

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\rotateheaderstrue       % si tu combines slide et slide*

\slidesmag{5}


\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage[dvips]{graphicx}
\input{mes_couleurs}

%% 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


\articlemag{1}

\title{\color{red}{\textit{Réécriture}}}

\author{Reductions abstraites}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\renewcommand{\phi}{\varphi}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\IN}{\ensuremath{\mathcal{IN}}}
\newcommand{\gtmult}{\ensuremath{>_{mult}}}
\newcommand{\dminus}{\mbox{\ensuremath{\stackrel{\raisebox{+.01ex}{.}}{-}}}}
\newcommand{\Nat}{\textsf{I}\hspace{-.7pt}\textsf{N}}
\newcommand{\M}{{\cal M}}
\newcommand{\Ra}{\ensuremath{\mathop{\Rightarrow}}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\set}[2]{\{#1~|~#2\}}
\newcommand{\da}{\downarrow}
\newcommand{\jgbl}{\mathop{\da}}
\newcommand{\inferTwoLabel}[4]{\bl{
 {#1} \quad 
 \begin{array}{c}
   #2 \hspace{2em} #3\\
   \hline \noalign{\vskip 1pt}#4
  \end{array}}}

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

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

\newenvironment{bdp}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}
    
%% ==============================================================
%%                   Reductions and other relations
%% ==============================================================

\newcommand{\ra}{\xymatrix @C 15pt {\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix @C 15pt {\ar@{>>}[r] &}}
\newcommand{\rara}{\xymatrix @C 15pt {\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}
\newqsymbol{"<<->>"}{\xymatrix {\ar@{<<->>}[r] &}}
\newqsymbol{"==>"}{\xymatrix @C 15pt {\ar@{=>}[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 @C 15pt {\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[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{\supar}[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{\rarasupsub}[2]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix @C 20pt {\ar@{<->}[r]_{#1}^{+} &}}

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

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raR}{\rasub{R}}
\newcommand{\Rar}{\subar{R}}
\newcommand{\rastarR}{\rasupsub{*}{R}}
\newcommand{\raraR}{\rarasub{R}}
\newcommand{\plusararR}{\xymatrix @C 15pt {&\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{vertfonce}{\shadowbox{#1}}%
  \end{center}
  \markright{#1}
  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{brunfonce}{\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{Quelques rappels} 
  
  Si \bleu{R} et \bleu{T} sont deux relations binaires sur \bleu{A}
  notées de façon infixée (c-à-d, \bleu{x~R~y}). On définit
\begin{itemize}
\item \bleu{x~R\,T~y} ssi il existe \bleu{z} tel que
\bleu{x~R~z} et \bleu{z~T~y}.  

\item \bleu{R^n} par \bleu{R^0=\{(x,x) ~|~ x\in A\}} et \bleu{R^{n+1}
    = R\,R^n} \\\hspace*{20pt}(donc \bleu{R^1=R}).   

\item \bleu{R \subseteq T} ssi \bleu{x~R~y} implique \bleu{x~T~y}.

\item \bleu{x~(R\bigcup T)~y} ssi \bleu{x~R~y} ou \bleu{x~T~y}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Quelques rappels} 
 Une relation est \rouge{transitive} si \bleu{x~R~y} et \bleu{y~R~z}
impliquent \bleu{x~R~z}.  

La \rouge{fermeture transitive} de \bleu{R}
est la plus petite relation transitive qui contient \bleu{R}.
Elle est notée \bleu{R^+}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Encore des notations}
Souvent la relation \bleu{R} est notée \bleu{\raR}.

\begin{itemize}
\item \bleu{R^{-1}} est la relation \rouge{converse} \bleu{\set{(y,x)\in A\times
      A}{(x,y)\in R}}, \\
\hspace*{30pt}aussi notée \bleu{\Rar}.

\item \bleu{\rasupsub{+}{R}} est la \rouge{clôture transitive} de
  \bleu{\raR},
\item \bleu{\rastarR} est la \rouge{clôture réflexive et
  transitive} de \bleu{\raR},
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Terminologie}

Si \bleu{a \raR b}, on dit que \bleu{a}  se \verdir{contracte} en \bleu{b} par \bleu{R}.

Si \bleu{a \rastarR b}, on dit que \bleu{a} se \verdir{réduit} en
\bleu{b} par \bleu{R}.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Encore des notations}

\begin{itemize}
\item \bleu{\cv{R}} est la \rouge{clôture symétrique}, \\\hspace*{20pt}c'est la relation
  \bleu{\raR\cup\Rar}.
\item \bleu{\conv{R}} est la \rouge{clôture réflexive, symétrique et
  transitive} de \bleu{\raR}.\\
C'est aussi la clôture réflexive et transitive de \bleu{\cv{R}}.\\

\item \bleu{\convplus{R}} est la \rouge{clôture symétrique et
    transitive} de \bleu{\raR}.\\
C'est aussi la clôture transitive de \bleu{\cv{R}}.\\
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Encore des notations}

\begin{itemize}
\item \bleu{\rasupsub{=}{R}} est la \rouge{clôture réflexive},
  \\\hspace*{20pt}c'est la relation \bleu{\raR\cup \rasupsub{0}{R}}
  \\\hspace*{20pt}sachant que \bleu{\rasupsub{0}{R}} est l'égalité
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Encore des notations}

En $\lambda$-calcul, 
\begin{itemize}
\item \bleu{\rastar} est noté \bleu{\rara},
\item \bleu{\conv{}} est noté \bleu{\xymatrix{\ar@{<<->>}[r] &}}.
\end{itemize}
C'est culturel!
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Confluence}
Une \quad relation \bleu{R} sur \bleu{A} est \rouge{confluente} si
\begin{center}
\bleu{(\forall M,N_1,N_2\in A)M \rastarR N_1 \et M \rastarR N_2}

\bleu{"==>"}

\bleu{(\exists P \in A) N_1\rastarR P \et N_2\rastarR P}
\end{center}

\vfill
\verdir{autrement dit}
\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}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Semi-confluence}
Une relation  \bleu{R} sur \bleu{A} est \rouge{semi-confluente} si

\begin{small}
\begin{center}
\bleu{(\forall M,N_1,N_2\in A)~~ M \raR N_1 \et M \rastarR N_2}

\bleu{"==>"}

\bleu{(\exists P \in A)\;\; N_1\rastarR P \et N_2\rastarR P}
\end{center}

\vfill \verdir{autrement dit} \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}
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Confluence locale}
Une relation  \bleu{R} sur \bleu{A} est \rouge{localement confluente} si

\begin{small}
\begin{center}
\bleu{(\forall M,N_1,N_2\in A)~~ M \raR N_1 \et M \raR N_2}

\bleu{"==>"}

\bleu{(\exists P \in A)\;\; N_1\rastarR P \et N_2\rastarR P}
\end{center}

\vfill
\verdir{autrement dit} 
\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}
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Paire joignable}
Une paire de terme \bleu{(N_1,N_2)} est \rouge{joignable}, notée
\bleu{N_1\jgbl N_2} si

\begin{center}
  \bleu{(\exists P \in A)\;\; N_1\rastarR P \et N_2\rastarR P}
\end{center}

d'où
\begin{itemize}
\item \verdir{confluence}: \bleu{M \rastarR N_1 \et M \rastarR N_2 \quad\rouge{"==>"}\quad
    N_1\jgbl N_2},
\item \verdir{semi-confluence}: \bleu{M \raR N_1 \et M \rastarR N_2 \quad\rouge{"==>"}\quad
    N_1\jgbl N_2}.
\item \verdir{confluence locale}: \bleu{M \raR N_1 \et M \raR N_2 \quad\rouge{"==>"}\quad
    N_1\jgbl N_2},
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Diagrammes} 
\begin{center}
\parbox{2.5cm}{\xymatrix{& \ar@{>}[dl]_{*}\ar@{>}[dr]^{*}\\ 
  \ar@{.>}[dr]^{*} && \ar@{.>}[dl]_{*}\\ &&}

\centerline{\verdir{confluence}}}
\parbox{2.5cm}{\xymatrix{& \ar@{>}[dl]\ar@{>}[dr]^{*}\\ 
  \ar@{.>}[dr]^{*} && \ar@{.>}[dl]_{*}\\ &&}

\centerline{\verdir{semi-confluence}}}
\parbox{2.5cm}{\xymatrix{& \ar@{>}[dl]\ar@{>}[dr]\\ 
  \ar@{.>}[dr]^{*} && \ar@{.>}[dl]_{*}\\ &&}

\centerline{\verdir{confluence locale}}}
\end{center}
\vfill
\bleu{\xymatrix{\ar@{.>}[r]^{*}&}} est un flèche existentielle.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Propriété de Church Rosser} 

\bleu{N_1 \conv{R} N_2 \quad\rouge{"==>"}\quad N_1\jgbl N_2}

\begin{center}
\parbox{2.5cm}{\xymatrix{\ar@{<->}[rr]^{*}
  \ar@{.>}[dr]^{*} && \ar@{.>}[dl]_{*}\\ &&}}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{center}
  \framebox{\parbox{5.5cm}{Les conditions suivantes sont équivalentes
      \begin{itemize}
      \item \bleu{R} est confluente,
      \item \bleu{R} est semi-confluente,
      \item \bleu{R}  a la propriété de Church-Rosser
      \end{itemize}
}}
  \end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  Church-Rosser $\quad\Ra\quad$ confluence $\quad \Ra\quad$
  semi-confluence \verdir{est facile}!

\vspace*{20pt}

\framebox{Semi-confluence  $\quad\Ra\quad$ Church-Rosser}

Par induction sur la longueur de \bleu{\conv{}}.


\vspace*{10pt}


\xymatrix{
a \ar@{<->}[rr]^{*} \ar@{.>}[rdd]^{*} && b
\ar@{<->}[rr]\ar@{.>}[ldd]_{*}  && c\\
& \mbox{{\scriptsize IND}} \\
&&&&
}
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&& c \ar[ldd]\\\\
a \ar@{<->}[rr]^{*} \ar@{.>}[rdd]^{*} && b
\ar@{.>}[ldd]_{*}  && \\
& \mbox{\scriptsize IND} \\
&&&&
}
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&& c \ar[ldd]\ar@{.>}@/^2pc/[lldddd]^{*}\\\\
a \ar@{<->}[rr]^{*} \ar@{.>}[rdd]^{*} && b
\ar@{.>}[ldd]_{*}  && \\
& \mbox{\scriptsize IND} \\
&&&&
}
\end{slide}
%------------------------------------------------------
\begin{slide}

\xymatrix{
a \ar@{<->}[rr]^{*} \ar@{.>}[rdd]^{*} && b
\ar@{.>}[ldd]_{*} \ar[rdd] && \\
& \mbox{\scriptsize IND} \\
&&& c
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\xymatrix{
a \ar@{<->}[rr]^{*} \ar@{.>}[rdd]^{*} && b
\ar@{.>}[ldd]_{*} \ar[rdd] && \\
& \mbox{\scriptsize IND} &  \\
&\ar@{.>}[rdd]^{*}& \mbox{\scriptsize SC} & c \ar@{.>}[ldd]_{*}\\\\
&& 
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Encore des concepts !}
A partir de maintenant on laisse tomber les \bleu{R} s'il n'y a pas
d'ambiguïté. 

\begin{itemize}
\item \bleu{x} est \rouge{réductible} ssi il existe un \bleu{y} tel que
  \bleu{x\ra y},
\item \bleu{x} est \rouge{irréductible} ssi \bleu{x} n'est pas
  réductible,
\item \bleu{y} est une \rouge{forme normale} de \bleu{x} ssi
  \bleu{x\rastar y} et \bleu{y} est irréductible.\\
Si la forme normale est déterminée de façon unique on la note \bleu{x\da}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\subheading{Terminaison}
Une relation\bleu{R} \rouge{termine} ou est \rouge{noethérienne}

ssi

il n'existe pas de suite infinie \bleu{x_0 \raR x_1 \raR \dots x_n\raR
  x_{n+1} \dots}
\subheading{Convergence}
Une relation est \rouge{convergente} si elle \verdir{termine} et est
\verdir{confluente}
\subheading{Normalisante}
Une relation est \rouge{normalisante} si toute élément a une fonorme normale.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques faits}
\begin{itemize}
\item Si \bleu{\ra} est confluente, chaque élément a au plus une forme
  normale.
\item Si \bleu{\ra} est confluente et normalisante, chaque élément a  une forme
  normale unique.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve de convertibilité par normalisation}
 \framebox{\parbox{6cm}{Si \bleu{\ra} est confluente et normalisante,
     alors 

\bleu{x\conv{} y} \quad\rouge{$\Leftrightarrow$}\quad \bleu{x\da=y\da}}}
\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve de convertibilité par normalisation}
 \framebox{\parbox{6cm}{Si \bleu{\ra} est confluente et normalisante,
     alors 

\bleu{x\conv{} y} \quad\rouge{$\Leftrightarrow$}\quad \bleu{x\da=y\da}}}
\vfill
Fort bien, mais y  a-t-il un moyen simple 
\begin{enumerate}
\item de calculer ces formes normales?
\item de savoir si une relation est normalisante?
\end{enumerate}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Induction noethérienne}
\begin{bdp}
\inferLabel{(\IN)}%
     {(\forall x\in A)\ \ ((\forall y \in A)\; x\ra y\ \Ra\ P(y))\ \ \Ra
       \ P(x)}%
     {(\forall a \in A) P(a)}
\end{bdp}

\vspace*{20pt}

\framebox{\parbox{8cm}{\rouge{\emph{(\IN)}} est satisfaite sur
    \bleu{A} si et seulement si \bleu{\ra} termine.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Encore des concepts !}

Une relation est  \rouge{à branchement fini} \\
\hspace*{30pt}ssi pour tout \bleu{x} il
n'y a qu'un nombre fini de \bleu{y} tels que \bleu{x\ra y}.

Une relation est \rouge{globalement finie} \\
\hspace*{30pt}ssi pour tout \bleu{x} il
n'y a qu'un nombre fini de \bleu{y} tels que \bleu{x\raplus y}.


Une relation est \rouge{acyclique} \\
\hspace*{30pt}ssi il n'y a pas d'élément \bleu{a} tel que
\bleu{a\raplus a}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{Une relation à branchement fini est globalement
    finie si elle termine}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{Une relation à branchement fini est globalement
    finie si elle termine}

\vspace*{20pt}

Nous devons prouver 

\centerline{\bl{branchement fini} \rouge{+} \bl{termine}}

\centerline{$\rouge{"==>"}$}

\centerline{\bl{globalement fini}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{{Une relation à branchement fini est globalement
    finie si elle termine}}

\verdir{Par induction noethérienne.} 

Soit \bleu{Contract(a) = \set{x\in A}{a\ra x}}.

Soit \bleu{Reduits(a) = \set{x\in A}{a\raplus x}}.

Nous devons prouver \bl{«$(\forall a\in A)\ Reduits(a)$ est fini»}.

Pour le faire par \verdir{induction noethérienne}, nous devons prouver que 

\begin{center}
  \bl{«Pour tout \bleu{b} tel \bleu{a\ra b} on a \bl{$Reduits(b)$ est
      fini»}}
\end{center} 

\begin{center}
  \rouge{implique}
\end{center}

\begin{center}
  \bl{«$Reduits(a)$ est fini»}.
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{{Une relation à branchement fini est globalement
    finie si elle termine}}

\vspace*{10pt}

Or
\begin{bdp}
Reduits(a) = Contract(a) \cup \bigcup_{b\in Contract(a)} Reduits(b)
\end{bdp}
Donc \bleu{Reduits(a)} qui est une réunion finie d'ensembles finis est finie.

En application de \rouge{(\IN)}, \bl{«}\bleu{(\forall a\in A)\ Reduits(a)} \bl{est fini»}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{Une relation acyclique termine si elle est
      globalement finie.}

\vspace*{20pt}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{Une relation acyclique termine si elle est
      globalement finie.}

\vspace*{20pt}

\vspace*{20pt}

Nous devons prouver 

\centerline{\bl{acyclique} \rouge{+} \bl{globalement fini}}

\centerline{$\rouge{"==>"}$}

\centerline{\bl{termine}}
\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{Une relation acyclique termine si elle est
      globalement finie.}
  
  \vspace*{20pt} 
  
  Soit \bleu{\ra} une relation acyclique. 
  
  Si elle ne termine pas, alors il existe une suite \bleu{x_0 \ra x_1
    \ra \dots x_n\ra x_{n+1} \dots}  
  
  Puisque la relation est acyclique, les éléments sont tous
  différents.  
  
  Donc \bleu{Reduits(x_0)} est infini et la relation n'est pas globalement
  finie.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de Koenig}

  \vspace*{20pt} 
    
  \begin{center}
    \framebox{\parbox{9.5cm}{Soient \bleu{(A, \ra)} une relation
        \verdir{acyclique} et
        \verdir{à branchement fini} et
        \bleu{a\in A}.\\[6pt]
        \bleu{Reduits(a)} est infini \\
        \centerline{\rouge{si et seulement si}}\\
        il existe un chemin infini \\
\begin{footnotesize}\bleu{a \ra a_1 \ra \ldots \ra a_n
          \ra a_{n+1} \ra \ldots}
      \end{footnotesize}\\
      qui part de \bleu{a}.}}
\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de Koenig (deuxième formulation)}

  \vspace*{20pt} 
    
  \begin{center}
    \framebox{\parbox{7.5cm}{Soient \bleu{\ra} une relation
        \verdir{acyclique} et
        \verdir{à branchement fini}.\\[6pt]
        \bleu{\ra} est \verdir{globalement finie} \\
        \centerline{\rouge{si et seulement si}}\\
        \bleu{\ra} \verdir{termine}.}}
\end{center}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de Koenig (démonstration)}
On s'appuie sur les deux lemmes précédents.

Dans un sens, on a montré que 

\centerline{\bl{acyclique} \rouge{+} \bl{globalement fini}}

\centerline{$\rouge{"==>"}$}

\centerline{\bl{termine}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de Koenig (démonstration)}
Dans l'autre sens, on a montré que 

\centerline{\bl{à branchement fini} \rouge{+} \bl{termine}}

\centerline{$\rouge{"==>"}$}

\centerline{\bl{globalement fini}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{green}{\textit{Prouver la terminaison}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les suites de Goodstein}
Considérons la décomposition en base \bleu{k} d'un nombre.

Ainsi la décomposition en base \bleu{3} de \bleu{111} est %
\bleu{3^{3+1} + 3^{3} + 3}.

Soit un nombre \bleu{n}. On définit une suite \bleu{n_2, n_3, \ldots}
dont le premier terme est \bleu{n_2=n}.

On passe de \bleu{n_k} à \bleu{n_{k+1}} de la façon suivante: on pose
\bleu{m_k= n_k -1}.  Dans la décomposition en base \bleu{k} de
\bleu{m_k} on remplace toutes les occurrences de \bleu{k} par
\bleu{k+1}, on obtient \bleu{n_{k+1}}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Ainsi si \bleu{n_2=15} alors \bleu{m_2=14=2^{2+1} + 2^{2} + 2}

\bleu{n_3=3^{3+1} + 3^{3} + 3=111}, 

\bleu{n_4=4^{4+1} + 4^4 + 2= 1282}, 

\bleu{n_5=5^{5+1} + 5^5 + 1 = 18751},

\bleu{n_6=6^{6+1} + 6^6 = 326592}, 

\bleu{n_7=7^{7+1} + ...},

\vdots

\bleu{n_{40000}=40000^{40000+1} + ...} 

\vdots

\rouge{Le processus termine}, il existe un entier $p$ tel que $n_p = 0$

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les fonctions croissantes}

Soit \bleu{(A, \ra)}

On connaît \bleu{(B, >)} est noethérien et
\bleu{\phi:A "->" B} telle que \bleu{x\ra y} implique
\bleu{\phi(x)>\phi(y)}. 

\vspace*{20pt}

Le plus souvent on prend \bleu{(\Nat, >)}. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{5cm}{Une relation à branchement fini termine \\
      si et seulement si\\
      elle est plongeable dans \bleu{\Nat}.}}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Composition lexicographique de deux ordres}
Soient deux ordres \bleu{(A_1,>_1)} et \bleu{(A_2,>_2)}.

On définit l'ordre \bleu{>_1\times_{lex} >_2} sur \bleu{A_1\times A_2}, par

\bleu{(a_1,a_2) \;\;>_1\times_{lex} >_2\;\; (b_1,b_2)} ssi
\begin{itemize}
\item \bleu{a_1 >_1 b_1}
\item ou \bleu{a_1 =_1 b_1} et \bleu{a_2 >_2 b_2}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{{Si \bleu{>_1} et \bleu{>_2} terminent
      alors \bleu{>_1\times_{lex} >_2} termine.}}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Composition lexicographique de $n$ ordres} 
  
  Soient \bleu{(A_n, >_n)}, ..., \bleu{(A_1, >_1)}, \bleu{(A_0, >_0)}
  des ordres.

Soit \bleu{\mathbf{A}_{n+1} = A_{n+1} \times \mathbf{A}_n}\\
et \bleu{\mathbf{A}_{0} = A_{0}}.

On définit l'ordre \bleu{>^{lex}_n} sur \bleu{\mathbf{A}_n} ainsi:
\begin{itemize}
\item \bleu{>^{lex}_0} est \bleu{>_0},
\item Si \bleu{(x,\mathbf{x}), (y,\mathbf{y})\in A_{n+1} \times
    \mathbf{A}_n}, alors \bleu{(x,\mathbf{x}) >^{lex}_{n+1}(y,\mathbf{y})}
  ssi 
  \begin{itemize}
  \item \bleu{x >_{n+1} y},
  \item ou \bleu{x = y} et \bleu{\mathbf{x} >^{lex}_{n}\mathbf{y}}.
  \end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7,5cm}{Si les ordres \bleu{(A_n, >_n)}, ...,
    \bleu{(A_1, >_1)}, \bleu{(A_0, >_0)} terminent\\
alors  \bleu{(\mathbf{A}_n, >^{lex}_n)} termine  }}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{7,5cm}{Si les ordres \bleu{(A_n, >_n)}, ...,
    \bleu{(A_1, >_1)}, \bleu{(A_0, >_0)} terminent\\
alors  \bleu{(\mathbf{A}_n, >^{lex}_n)} termine  }}
\vfill
\heading{Ordres stricts et lexicographie}

Un \rouge{ordre strict} est une relation \verdir{transitive} et
\verdir{irréflexive}.

\vspace*{20pt}

\framebox{\parbox{8cm}{Si les ordres \bleu{(A_n, >_n)}, ...,
    \bleu{(A_1, >_1)}, \bleu{(A_0, >_0)} sont stricts \\
    alors \bleu{(\mathbf{A}_n, >^{lex}_n)} est strict.  }}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Attention à la lexicographie !}

La composition lexicographique se fait sur des relations et peut
donner des résultats surprenants.

Sur \bleu{\Nat\times \Nat},


\bleu{\ge_{\Nat} \times_{lex} \ge_{\Nat} \;\;\equiv\;\; \ge_{\Nat} \times_{lex}
  \textbf{U}}\\ 
où \bleu{\textbf{U}} est la relation universelle
\bleu{\set{(x,y)}{x\in \Nat \ \et\ y\in\Nat}}.
  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Attention à la lexicographie !}

La composition lexicographique se fait sur des relations et peut
donner des résultats surprenants.

Sur \bleu{\Nat\times \Nat},


\bleu{\ge_{\Nat} \times_{lex} \ge_{\Nat} \;\;\equiv\;\; \ge_{\Nat}
  \times_{lex} \textbf{U}}\\ 
où \bleu{\textbf{U}} est la relation universelle
\bleu{\set{(x,y)}{x\in \Nat \ \et\ y\in\Nat}}.
  
\vspace*{20pt}

Pour tous \bleu{m}, \bleu{n}, \bleu{p}, on a donc  \bleu{(m,n)
  \ge_{\Nat} \times_{lex} \ge_{\Nat} (m,p)}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Produit lexicographique d'ordres}
Pour définir le produit lexicographique d'ordres on définit
\begin{enumerate}
\item le produit lexicographique de leur partie stricte\footnote{la
    partie stricte de \bleu{\ge} est l'ordre défini par \bleu{x>y} ssi 
    \bleu{x\ge y \et x\not=y}},
\item la clôture réflexive de ce produit,
\end{enumerate}
ou encore directement
\begin{bdp}
(x,y) \ge_{A\times B} (x',y') \qquad \mbox{ssi}\qquad(x >_A x') \vee
(x=x' \ \et\ y\ge_B y').
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Multiensemble}
Un \rouge{multiensemble} \bleu{M} sur \bleu{A} est une fonction
\bleu{M: A\rightarrow \Nat}.

\verdir{Intuitivement:} on peut s'imaginer qu'il s'agit d'«ensembles» où la
répétition d'éléments est autorisée, \bleu{M(x)} est le nombre de
répétitions de \bleu{x} dans \bleu{M}.

Un multiensemble est \rouge{fini} si \bleu{\set{x\in A}{M(x)\not=0}}
est fini.

\bleu{\M(A)} est l'ensemble des multiensembles finis sur \bleu{A}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Multiensemble} La notation standard est \bleu{\{a, a, b\}}
  \\ ou \bleu{\{\!\!\{a, a, b\}\!\!\}} si l'on veut bien préciser
  qu'il s'agit d'un multiensemble.%
  \ali pour \bleu{\{a\mapsto 2, b\mapsto 1, c \mapsto 0\}}.  %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Opérations sur les multiensembles}
\rouge{$x\in M$} ssi \bleu{M(X) > 0}

\rouge{$M\supseteq N$} ssi \bleu{(\forall x\in A) M(x) \ge N(x)}

\rouge{$(M\cup N)(x)$} = \bleu{M(x) + N(x)}

\rouge{$(M - N)(x)$} = \bleu{M(x)\dminus N(x)} où
\bleu{m\dminus n = max(m-n,0)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Ordre multiensemble} 

Soit \bleu{>} un ordre strict sur
  \bleu{A}.  

L'extension multiensemble \bleu{\gtmult} sur \bleu{\M(A)} est définie
par 

\vspace{20pt}

\bleu{M\gtmult N} ssi \hspace*{20pt}%
\parbox{4cm}{il existe \bleu{X} et \bleu{Y} tels que 
  \begin{itemize}
  \item \bleu{\emptyset\not=X\subseteq M} et
  \item \bleu{N = (M - X) \cup Y} et\ 
  \item \bleu{(\forall y \in Y) (\exists x\in X) x > y}
\end{itemize}
}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriété de l'ordre multiensemble I}
\framebox{{Si \bleu{>} est strict, alors \bleu{\gtmult}
    est strict.
}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriété de l'ordre multiensemble I}
\framebox{{Si \bleu{>} est strict, alors \bleu{\gtmult}
    est strict.
}}

\begin{enumerate}
\item \rouge{irréflexivité}
\item \rouge{transitivité}
\end{enumerate}
\vfill
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriété de l'ordre multiensemble II}
\framebox{{Si \bleu{\gtmult} termine, alors \bleu{>}
    termine.  }}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Propriété de l'ordre multiensemble II} \framebox{{Si
      \bleu{\gtmult} sur 
      \bleu{\M(A)} termine, alors
      \bleu{>} sur \bleu{A} termine.  }}

Puisque \bleu{A} est plongé dans \bleu{\M(A)} par \bleu{a\mapsto
  \{\!\!\{a\}\!\!\}}, clairement la terminaison sur \bleu{\M(A)} implique celle
sur \bleu{A}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriété de l'ordre multiensemble II}
\framebox{{Si \bleu{>} termine, alors \bleu{\gtmult}
    termine.  }}

Réciproquement, supposons que  \bleu{\gtmult} ne  termine pas sur
      \bleu{\M(A)}.  Alors il existe une suite infinie décroissante de
      multiensembles. 

\begin{bdp}
M_0 \gtmult M_1 \gtmult ... M_n\gtmult M_{n+1}
\end{bdp}

\vspace*{2pt}

On pose \bleu{M_{n+1} = (M_n - X_n) \cup Y_n}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  On veut construire une arborescence étiquetée qui \rouge{contredit
    le lemme de Koenig}, à savoir:
      \begin{itemize}
      \item infini, 
      \item à branchement fini,
      \item tous ses chemins sont finis.
      \end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  Plus précisément, on construit une relation 
      \begin{itemize}
      \item qui n'est pas globalement finie, 
      \item qui est à branchement fini,
      \item et qui ne termine pas.
      \end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  On construit l'arborescence par niveau.  On peut aussi dire que l'on a une
  canopée croissante qui tend vers l'infini \begin{scriptsize}(pour
    faire décroître l'effet de serre).
  \end{scriptsize}
  
  Au niveau \bleu{0}, on met les éléments de \bleu{M_0}.  
  
  Au niveau \bleu{n}, on trouve des noeuds étiquetés par les éléments
  de \bleu{M_n}. 

Les noeuds du niveau \bleu{n+1} sont 
\begin{itemize}
\item les noeuds étiquetés par les éléments de \bleu{M_n} inchangés,
\item moins ceux étiquetés par les éléments du \bleu{X_n} utilisés,
\item plus ceux étiquetés par les éléments du \bleu{Y_n} utilisé,
  c-à-d les nouveaux venus dans \bleu{M_{n+1}}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\vfill
Soit 
\begin{itemize}
\item \bleu{M_n = \{\!\!\{a, a, 5, 5, 3\}\!\!\}}
\item \bleu{M_{n+1} = \{\!\!\{a, b, b, c, 5, 4, 4, 3, 3, 2\}\!\!\}},
\item \bleu{X_n = \{\!\!\{a, 5, 3\}\!\!\}},
\item \bleu{Y_n = \{\!\!\{b, b, c, 4, 4, 3, 3, 2\}\!\!\}},
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}

\xymatrix{
*+[o][F-]{a} && *+[o][F-]{a}  && *+[o][F-]{5} & & *+[o][F-]{5} &
*+[o][F-]{3} \\
*+[o][F-]{b} & *+[o][F-]{b} & *+[o][F-]{c} & 
*+[o][F-]{4} & *+[o][F-]{4} & *+[o][F-]{3} & *+[o][F-]{3} &
*+[o][F-]{2} 
}

\vfill
\begin{itemize}
\item \bleu{M_n = \{\!\!\{a, a, 5, 5, 3\}\!\!\}}
\item \bleu{M_{n+1} = \{\!\!\{a, b, b, c, 5, 4, 4, 3, 3, 2\}\!\!\}},
\item \bleu{X_n = \{\!\!\{a, 5, 3\}\!\!\}},
\item \bleu{Y_n = \{\!\!\{b, b, c, 4, 4, 3, 3, 2\}\!\!\}},
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}

\xymatrix{
*+[o][F-]{a} && *+[o][F-]{a} \ar[lld] \ar[ld] \ar[d] && *+[o][F-]{5} & & *+[o][F-]{5} \ar[llld]\ar[lld]\ar[ld]\ar[d]&
*+[o][F-]{3} \ar[d]\\
*+[o][F-]{b} & *+[o][F-]{b} & *+[o][F-]{c} & 
*+[o][F-]{4} & *+[o][F-]{4} & *+[o][F-]{3} & *+[o][F-]{3} &
*+[o][F-]{2} 
}

\vfill
\begin{itemize}
\item \bleu{M_n = \{\!\!\{a, a, 5, 5, 3\}\!\!\}}
\item \bleu{M_{n+1} = \{\!\!\{a, b, b, c, 5, 4, 4, 3, 3, 2\}\!\!\}},
\item \bleu{X_n = \{\!\!\{a, 5, 3\}\!\!\}},
\item \bleu{Y_n = \{\!\!\{b, b, c, 4, 4, 3, 3, 2\}\!\!\}},
\end{itemize}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\newcommand{\va}{\verdir{a}}
\newcommand{\vc}{\verdir{5}}
\newcommand{\vt}{\verdir{3}}

\xymatrix{
*+[o][F-]{\va} && *+[o][F-]{\va} \ar[lld] \ar[ld] \ar[d] && *+[o][F-]{\vc} & & *+[o][F-]{\vc} \ar[llld]\ar[lld]\ar[ld]\ar[d]&
*+[o][F-]{\vt} \ar[d]\\
*+[o][F-]{b} & *+[o][F-]{b} & *+[o][F-]{c} & 
*+[o][F-]{4} & *+[o][F-]{4} & *+[o][F-]{3} & *+[o][F-]{3} &
*+[o][F-]{2} 
}

\vfill
\begin{itemize}
\item \verdir{$M_n = \{\!\!\{a, a, 5, 5, 3\}\!\!\}$}
\item \bleu{M_{n+1} = \{\!\!\{a, b, b, c, 5, 4, 4, 3, 3, 2\}\!\!\}},
\item \bleu{X_n = \{\!\!\{a, 5, 3\}\!\!\}},
\item \bleu{Y_n = \{\!\!\{b, b, c, 4, 4, 3, 3, 2\}\!\!\}},
\end{itemize}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \renewcommand{\emph}[1]{\rouge{#1}} \xymatrix{ *+[o][F-]{\emph{a}}
    && *+[o][F-]{a} \ar[lld] \ar[ld] \ar[d] && *+[o][F-]{\emph{5}} & &
    *+[o][F-]{5} \ar[llld]\ar[lld]\ar[ld]\ar[d]&
    *+[o][F-]{3} \ar[d]\\
    *+[o][F-]{\emph{b}} & *+[o][F-]{\emph{b}} & *+[o][F-]{\emph{c}} &
    *+[o][F-]{\emph{4}} & *+[o][F-]{\emph{4}} & *+[o][F-]{\emph{3}} &
    *+[o][F-]{\emph{3}} & *+[o][F-]{\emph{2}} }

\vfill
\begin{itemize}
\item \bleu{M_n = \{\!\!\{a, a, 5, 5, 3\}\!\!\}}
\item \rouge{$M_{n+1} = \{\!\!\{a, b, b, c, 5, 4, 4, 3, 3, 2\}\!\!\}$},
\item \bleu{X_n = \{\!\!\{a, 5, 3\}\!\!\}},
\item \bleu{Y_n = \{\!\!\{b, b, c, 4, 4, 3, 3, 2\}\!\!\}},
\end{itemize}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
  Le cas où \bleu{Y_n=\emptyset} ne peut pas arriver indéfiniment à
  partir d'un certain rang \bleu{n} car, les \bleu{M_n} étant finis,
  cela serait contradictoire avec le fait que la suite est infinie.
  
  Donc il y a une infinité d'étapes où l'on ajoute vraiment de
  nouveaux noeuds.  Donc \rouge{l'arbre est infini.}
  
  La construction montre que \rouge{l'arbre est à branchement fini.}
  
  Les étiquettes sur un chemin forme une suite décroissante d'éléments
  de \bleu{A}.  Comme \bleu{(A, >)} termine, \rouge{il n'y a pas
    chemins infinis.}

\vfill

N.B. Je n'ai pas utilisé \bleu{(A_\bot,>_\bot)} comme dans le
\emph{All that.}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{green}{\textit{Prouver la confluence}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de confluence locale}

\framebox{\parbox{7.1cm}{Si une relation est localement
    confluente, \\alors elle est  confluente.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de confluence locale}

\framebox{\parbox{7.1cm}{Si une relation est localement
    confluente, \\alors elle est  confluente.}}
\vfill
\verdir{Par induction sur $m$ et sur $n$?}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de confluence locale}

\centerline{
  \xymatrix{
    && \ar[dl] \ar[dr]\\
    &\ar[dl]_{n} \ar@{.>}[dr]^{*} &&\ar@{.>}[dl]_{*}\ar[dr]^{m}\\
    \ar@{.>}[dr]^{*}&&\ar@{.>}[dr]^{*}\ar@{.>}[dl]_{*}&&\ar@{.>}[dl]_{*}\\
    &\ar@{.>}[dr]^{*}&&\ar@{.>}[dl]_{*}\\
    &&& }}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lemme de confluence locale}

\centerline{
  \xymatrix{
    \ar@3{-}[ddddrrrr]&& \ar[dl] \ar[dr]&&\ar@3{-}[ddddllll]\\
    &\ar[dl]_{n} \ar@{.>}[dr]^{*} &&\ar@{.>}[dl]_{*}\ar[dr]^{m}\\
    \ar@{.>}[dr]^{*}&&\ar@{.>}[dr]^{*}\ar@{.>}[dl]_{*}&&\ar@{.>}[dl]_{*}\\
    &\ar@{.>}[dr]^{*}&&\ar@{.>}[dl]_{*}\\
    &&&& }}
\vfill
\centerline{\verdir{L'induction sur $m$ et $n$ ne fonctionne pas!}}
\addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\includegraphics[width=1cm]{attention.eps} 

\emph{\Large Il n'y a pas de
  lemme de confluence locale sans terminaison.}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le lemme de Newman}


\framebox{\parbox{7.1cm}{Si une relation \rouge{termine} et est localement
    confluente, \\alors elle est  confluente.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \rouge{La terminaison est importante.} 
\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
  \rouge{La terminaison est importante.} 

%\begin{scriptsize}
  Les deux relations suivantes sont localement confluentes, mais non
  confluentes.
%  \end{scriptsize}
  
\vspace*{10pt}

\subheading{Une relation globalement finie, localement confluente et non
  confluente}

\vspace*{10pt}

\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
  \rouge{La terminaison est importante.} 

%\begin{scriptsize}
  Les deux relations suivantes sont localement confluentes, mais non
  confluentes.
%  \end{scriptsize}
  
\vspace*{10pt}

\subheading{Une relation globalement finie, localement confluente et non
  confluente}

\vspace*{10pt}

\begin{center}
\xymatrix{a & b\ar[l]\ar@/^/[r]&c\ar@/^/[l]\ar[r]&d}
\end{center}

\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
  \rouge{La terminaison est importante.} 

\vspace*{10pt}

\subheading{Une relation acyclique, localement confluente et non
  confluente}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

Soit la relation sur \bleu{\Nat\cup \{a,b\}} définie par:

\bleu{n\ra n+1}

Si \bleu{n} est \rouge{pair}, \bleu{n\ra a}.

Si \bleu{n} est \rouge{impair}, \bleu{n\ra b}.

\begin{scriptsize}
\xymatrix{
&&&&& b\\
& 1 \ar[dr]\ar[urrrr] && 3\ar[dr]\ar[urr] &&\ar@{.}[r]&\\%\ar@{.>}[u]\\
0 \ar[ur]\ar[drrrrr]&&2 \ar[ur]\ar[drrr] & &4\ar[dr]\ar@{.>}[ur]&\ar@{.}[r]&\\
&&&&& a
}
\end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve du lemme de Newman}

\framebox{\parbox{7.1cm}{Si une relation termine et est localement
    confluente, \\alors elle est confluente.}}

\begin{bdp}
P(x) = (\forall y, z) y \supar{*} x \rastar z \ \Ra\ y \da z.
\end{bdp}

La confluence c'est \bleu{(\forall x) P(x)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve du lemme de Newman}

\framebox{\parbox{7.1cm}{Si une relation termine et est localement
    confluente, \\alors elle est confluente.}}

\begin{bdp}
P(x) = (\forall y, z) y \supar{*} x \rastar z \ \Ra\ y \da z.
\end{bdp}

La confluence c'est \bleu{(\forall x) P(x)}.

On peut supposer sans nuire à la généralité que \bleu{x\rastar y} et
\bleu{x\rastar z}, prennent chacun au moins une étape de réduction

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve du lemme de Newman}

  \xymatrix@R 15pt @C 15pt{x \ar[rr]\ar[dd] && z_1 \ar@{.>}[dd]^{*}\ar[rr]^{*} && z\ar@{.>}[dddd]^{*}\\
    & CL & \\
    y_1\ar@{.>}[rr]^{*}\ar[dd]^{*}&&  u \ar@{.>}[dd]^{*}& Ind\\
    &Ind\\
    y\ar@{.>}[rr]^{*} && v\ar@{.>}[rr]^{*} && w }

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forte confluence}
Une relation est \rouge{fortement confluente} ssi 
\begin{bdp}
y_1 \subar{} x \ra y_2 \qquad\Ra\qquad (\exists z) y_1 \rastar z\supar{=} y_2.
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forte confluence}
Une relation est \rouge{fortement confluente} ssi 
\begin{bdp}
y_1 \subar{} x \ra y_2 \qquad\Ra\qquad (\exists z) y_1 \rastar z\supar{=} y_2.
\end{bdp}

\vspace*{10pt}

\parbox{2.5cm}{\xymatrix{
& x \ar[dr] \ar[dl]& \\
y_1\ar@{.>}[dr]^{*} && y_2\ar@{.>}[dl]\\
& z 
}}
\hfill
\parbox{2.5cm}{\xymatrix{
& x \ar[dr] \ar[dl]& \\
y_1\ar@{.>}[rr]^{*} && y_2\\
& 
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forte confluence}
\framebox{{Une relation fortement confluence est confluente.}}

On prouve que si une relation est fortement confluence alors elle est
semi-confluente.

On fait une récurrence sur la longueur de la branche \bleu{\rastar}.

\xymatrix{
\ar[rr] \ar[dd]&& \ar[rr]^{*} \ar@{.>}[dd]^{=}&&\\
& \mbox{\scriptsize FC} \\
\ar@{.>}[rr]^{*}&&&&
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forte confluence}

Deux cas:

Cas \bleu{\rasup{=} = \ra}.

\xymatrix{
\ar[rr] \ar[dd]&& \ar[rr]^{*} \ar@{.>}[dd]&&\ar@{.>}[dd]^{*}\\
& \mbox{\scriptsize FC} && \mbox{\scriptsize IND} \\
\ar@{.>}[rr]^{*}&&\ar@{.>}[rr]^{*}&&
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forte confluence}

Cas \bleu{\rasup{=} = \rasup{0}}.

\xymatrix{
\ar[rr] \ar[dd]&& \ar[rr]^{*} &&\\
& \mbox{\scriptsize FC} && \\
\ar@{.>}[uurr]^{*}&&&&
}
\vfill
\end{slide}
%------------------------------------------------------
%\begin{slide}
%\heading{}

%\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  joignable infixée ssi semi-confluence semi-confluente Church m-n
% LocalWords:  Church-Rosser d'ambiguïté Goodstein noethérien plongeable Newman
% LocalWords:  multiensemble irréflexive s'imaginer multiensembles II canopée
% LocalWords:  irréflexivité arborescence l'arborescence N.B All that
