%% Time-stamp: <modified on 27 Oct 2004 at 13:32 by Pierre Lescanne>
%% /MIM-1/REECRITURE/TERMINAISON/terminaison.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\def\printlandscape{\special{landscape}}     % pour sortir en landscape
\slidesmag{5}

\usepackage{amsfonts,amsmath,amsthm,stmaryrd}
\usepackage{fancybox}
%\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
%\usepackage{amsmath}
\usepackage[all]{xy}

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

\rotateheaderstrue       % si tu combines slide et slide*

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

\author{Terminaison des systèmes de réécriture}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\renewcommand{\emph}[1]{\rouge{#1}}

%--- symboles ---
\renewcommand{\phi}{\varphi}
%\newcommand{\llbracket}{\ensuremath{|\![}}
%\newcommand{\rrbracket}{\ensuremath{]\!|}}
\newcommand{\Emb}{\bl{\ensuremath{\cal EMB}}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\shat}{\ensuremath{\hat{\sigma}}}
\newcommand{\pref}{\mathop{\textbf{\textsl{prefix}}}}
\newcommand{\IN}{\ensuremath{\mathcal{IN}}}
\newcommand{\gtmult}{\ensuremath{>_{mult}}}
\newcommand{\dminus}{\mbox{\ensuremath{\stackrel{\raisebox{+.01ex}{.}}{-}}}}
%\newcommand{\Natg}{\textsf{I}\hspace{-.7pt}\textsf{N}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\Natstar}{\Nat_\star}
\newcommand{\A}{\ensuremath{\bl{\cal A}}}
\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{\lpo}{<_{lpo}}
\newcommand{\lepo}{\le_{lpo}}

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

%%%%%%%%%%%%%%%%%%%% 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 15pt{\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix @C 15pt{\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix @C 15pt{\ar@{<->}[r]_{#1}^{+} &}}

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

\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}
\newcommand{\raE}{\rasub{E}}
\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]&||&}}
\newcommand{\remb}{\rasub{\Emb}}
\newcommand{\plgt}{\rasupsub{+}{\Emb}}
\newcommand{\plonge}{\xymatrix{\ar@{<-}[r]_{\Emb}^{*} &}}

%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{cyanp}\textbf{\large #1}}{\color{yellow}\\\rule{\textwidth}{2pt}
}}
%\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}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Indécidabilité de la terminaison}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Problème de correspondance de Post}
%
Un ensemble \bleu{(\alpha_1,\beta_1), ..., (\alpha_n,\beta_n)} \ali
o\`u \bleu{\alpha_i\in A^*} et \bleu{\beta_i\in A^*}  \\
est appelé un \rouge{problème de correspondance de Post}.

Une \rouge{holorime} est formée
\begin{itemize}
\item d'un mot \bleu{w\in A^+} 
\item et d'une suite \bleu{(i_1,...,i_p)\in[1..n]^+}
\end{itemize}
tels que
\begin{bdp}
w = \alpha_{i_1}...\alpha_{i_p} = \beta_{i_1}...\beta_{i_p}.
\end{bdp}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Problème de correspondance de Post}%
\begin{scriptsize}
\begin{enumerate}
\item (ala, tour)
\item (aman, dela) 
\item (dela, rène) 
\item (gal, galaman) 
\item (magnanime, anime)
\item (rène, ala) 
\item (tour, magn)
\end{enumerate}
\end{scriptsize}
\begin{footnotesize}
Une holorime est \rouge{galamandelarènealatourmagnanime}
avec la suite \bleu{\scriptstyle{(4, 2, 3, 6, 1, 7,5)}}.
\begin{quotation}
  Gal, amant de la reine, alla, tour magnanime, 

  Galamment de l'arène, à la tour Magne, à Nîmes.

\hspace*{100pt}\bl{Victor Hugo}
\end{quotation}
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
Mais là c'est super-facile.

\vspace*{20pt}
Une autre holorime est due à la poétesse Louise de Vilmorin:
\bigskip
\begin{quote}
  Étonnamment monotone et lasse 

  Est ton âme en mon automne, hélas!
\end{quote}
\end{slide}
%----------------------------------------
\begin{slide}
  \heading{Des exemples} Les problèmes de correspondance ci-dessus~:
\begin{center}
\begin{math}
\begin{array}{cccc}
\begin{array}{|c|r|r|}
\hline
i & \alpha_i & \beta_i\\
\hline
1 & 010 & 101\\
2 & 00 & 000\\
3 & 101 & 10\\
\hline
\end{array}
&&&
\begin{array}{|c|r|r|}
\hline
i & \alpha_i & \beta_i\\
\hline
1 & 101 & 10\\
2 & 11 & 011\\
3 & 011 & 101\\
\hline
\end{array}\\
\textbf{\large{\bl{1}}} &&& \textbf{\large{\bl{2}}} 
\end{array}
\end{math}
\end{center}
ont-ils une holorime~?
\vfill
\end{slide}

%----------------------------------------
\begin{slide}
  \heading{Des exemples (encore)} Et ceux là?
\begin{center}
\begin{math}
\begin{array}{cccc}
\begin{array}{|c|r|r|}
\hline
i & \alpha_i & \beta_i\\
\hline
1 & 011 & 1\\
2 & 1 & 0\\
3 & 0 & 011\\
4 & 10  & 001\\
\hline
\end{array}
&&&
\begin{array}{|c|r|r|}
\hline
i & \alpha_i & \beta_i\\
\hline
1 & 000 & 0\\
2 & 0   &  111\\
3 & 11 & 0\\
4 & 10 & 100\\
\hline
\end{array}\\
\textbf{\large{\bl{3}}} &&& \textbf{\large{\bl{4}}} 
\end{array}
\end{math}
\end{center}
ont-ils une holorime~?
\vfill
\end{slide}

%------------------------------------------------------
\begin{slide}
Le problème \emph{3} a pour solution
\[
\overbrace{0}^{3}\overbrace{1}^{2}\overbrace{1~~0}^{4}\overbrace{0}^{3}\overbrace{0}^{3}\overbrace{1}^{2}\overbrace{0~~1~~1~}^{1}
\overbrace{0~~1~~1~}^{1} \overbrace{0~~1~~1}^{1} \overbrace{1~~0}^{4} \overbrace{0~~1~~1}^{1} 
\]
et
\[
\underbrace{0~~1~~1~}_{3}\underbrace{0}_{2}\underbrace{0~~0~~1~}_{4}\underbrace{0~~1~~1~}_{3}\underbrace{0~~1~~1~}_{3}\underbrace{0}_{2}
\underbrace{1}_{1}\underbrace{1}_{1}\underbrace{1}_{1}\underbrace{0~~0~~1~}_{4}\underbrace{1}_{1}
\]
\end{slide}
%------------------------------------------------------
\begin{slide}
Le problème \emph{3} a pour solution
\newcommand{\la}{\rouge{\tiny{|}}}
\[
\overbrace{0}^{3}\overbrace{1}^{2}\overbrace{1~~0}^{4}\overbrace{0}^{3}\la\overbrace{0}^{3}\overbrace{1}^{2}\overbrace{0~~1~~1~}^{1}\la
\overbrace{0~~1~~1~}^{1} \overbrace{0~~1~\la~1}^{1} \overbrace{1~~0}^{4} \overbrace{0~~1~~1}^{1} 
\]
et
\[
\underbrace{0~~1~~1~}_{3}\underbrace{0}_{2}\underbrace{0~\la~0~~1~}_{4}\underbrace{0~~1~~1~}_{3}\la\underbrace{0~~1~~1~}_{3}\underbrace{0}_{2}
\underbrace{1}_{1}\la\underbrace{1}_{1}\underbrace{1}_{1}\underbrace{0~~0~~1~}_{4}\underbrace{1}_{1}
\]
\end{slide}
%------------------------------------------------------
\begin{slide}
  La plus petite solution du problème \emph{4} est de taille 204.

\vspace*{50pt}

A vous de la trouver!
\end{slide}
%------------------------------------------------------
\begin{slide}
  Le problème de correspondance de Post (ou PCP) est
  \rouge{indécidable},\ali à partir de deux éléments dans \bleu{A}.

Autrement dit, il n'y a pas d'algorithme avec
\begin{itemize}
\item\emph{entrée :} un PCP sur deux lettres 
\item \emph{sortie :} le problème a une holorime ou le problème n'a pas d'holorime .
\end{itemize}

\end{slide}
%------------------------------------------------------
%\begin{slide}
%\heading{Problème de correspondance de Post modifié}
%Dans le \rouge{problème de Post modifié}, la suite d'indice commence
%à \bleu{1}, c'est-à-dire
%\begin{bdp}
%w = \alpha_{1}\alpha_{i_2}...\alpha_{i_p} =
%\beta_{1}\beta_{i_2}...\beta_{i_p}. 
%\end{bdp}

%\vspace*{30pt}

%Le problème de Post modifié est \rouge{indécidable}, même si \bleu{A}
%a deux éléments.

%\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Réduction de la terminaison à PCP}
On considère la signature 
\begin{itemize}
\item \bleu{\Sigma_0 = \{\#\}},
\item \bleu{\Sigma_1 = A},
\item \bleu{\Sigma_2 = \emptyset},
\item \bleu{\Sigma_3 = \{f\}},
\item \bleu{\Sigma_n=\emptyset} pour \bleu{n\ge 4}.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
 A chaque mot \bleu{a_1 a_2... a_n} de \bleu{A^*} on peut associer un
terme \ali dit \emph{monadique}
\begin{bdp}{(a_1 (a_2(...(a_n(\#))...)))} \in T(\Sigma).
\end{bdp}
que l'on note \bleu{a_1 a_2... a_n}.

Dans la suite \bleu{a_1 a_2... a_n x} pour \bleu{x\in X} est 
\begin{bdp}
  {(a_1 (a_2(...(a_n(x))...)))} \in
  T(\Sigma, X).
\end{bdp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  Étant donné un problème de correspondance de Post sur
  \bleu{A \equiv \{a_1,...,a_m\}}.  

On considère le système de réécriture :
\begin{small} 
$\emph{R_1} = \left\{
\bl{\begin{array}{lcl}
  f(\alpha_1 x,\beta_1 y, z) &\emph{\ra}& f(x, y, z)\\
         & \emph{\vdots} & \\
  f(\alpha_n x, \beta_n y, z) &\emph{\ra}& f(x,y, z)
\end{array}}
 \right.$


$\verdir{R_2} = \left\{
\bl{\begin{array}{lcl}
  f(\#, \#, a_1(y)) & \verdir{\ra} & f(a_1(y),a_1(y), a_1(y))\\
       & \verdir{\vdots} & \\
  f(\#, \#, a_m(y)) & \verdir{\ra} & f(a_m(y),a_m(y), a_m(y))
 \end{array}}
 \right.$
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\bleu{\rasub{R_1\cup R_2}} \emph{ne termine pas} si et seulement
    si PCP a une holorime.}

Si PCP a une holorime \bleu{w}, alors 
\begin{bdp}
f(\#,\#,w) \verdir{\rasub{R_2}} f(w,w,w) \emph{\rasupsub{+}{R_1}} f(\#,\#,w).
\end{bdp}

Si \bleu{\rasub{R_1\cup R_2}} ne termine pas, alors elle passe une
infinité de fois par des règles \verdir{$\rasub{R_2}$}. Et cela implique
qu'il y a une holorime.

En effet, les règles \rouge{$\rasub{R_1}$} décroissent la taille des
termes et ne peuvent pas contribuer seules à la non terminaison.

\end{slide}
%------------------------------------------------------
\begin{slide}
  On a d'ailleurs montré plus fort : \bleu{\rasub{R_1\cup R_2}} est
  \emph{cyclique} si et seulement si PCP a une holorime.

Donc
\begin{itemize}
\item l'acyclicité,
\item et la terminaison 
\end{itemize}
sont \emph{indécidables}.
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Ordre de réduction}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
 Un \emph{ordre de réécriture} est  une ordre sur \bleu{T(\Sigma, V)}
 qui est
 \begin{itemize}
 \item \emph{compatible} c'est-à-dire si \bleu{s > u} %

   \bleu{f(t_1,...,t_{i-1},s,t_{i+1},..., t_n) >
     f(t_1,...,t_{i-1},u,t_{i+1},..., t_n)}
\item \emph{clos par substitution} c'est-à-dire si \bleu{s_1>s_2\quad\Ra\quad 
    (\forall \sigma\in Subst(T(\Sigma, V)))\quad
    \sigma(s_1)>\sigma(s_2)}.
 \end{itemize}
 Un \emph{ordre de réduction} est un ordre de réécriture noethérien
 (c'est-à-dire qui termine). 
\vfill
N.B. La taille du terme n'est pas un ordre de réduction.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{6cm}{
      {Un système de réécriture \bleu{R} termine \\
        si et seulement si\\
        il existe un ordre de réduction \bleu{>} \ali tel que \bleu{l>r}
        pour tout \bleu{l\ra r\in R}.}}}
\vspace*{10pt}


\emph{Si :} \bleu{>} est une relation noethérienne qui
contient \bleu{\raplus}.\ali
Donc \bleu{\raplus} elle-même est noethérienne.

\emph{Seulement si :} \bleu{\raplus} est une ordre de réduction qui
satisfait clairement la condition (d'ordonner les règles de
réécriture, il est clair que l'on a \bleu{l\raplus r}, on peut donc
prendre  \bleu{\raplus} comme ordre).
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Interprétations}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Algèbre ordonnée et ordre induit}
Une \emph{algèbre ordonnée} est la donnée d'une algèbre 
\A{} \ali et d'un ordre \bleu{>} sur \bleu{A}.

L'ordre \bleu{>_{\A}} sur \bleu{T(\Sigma, V)} \emph{induit} par cette algèbre
est défini par :
\begin{bdp}
 s>_{\A} t \quad\textrm{ssi}\quad \pi(s) >
\pi(t) \quad\mbox{pour tout morphisme~}\pi:  T(\Sigma, V) \rightarrow \A.
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Monotonie}
Une fonction \bleu{F:A^n\rightarrow A} est \emph{monotone} si 

\begin{small}
\bleu{ b > c \quad\emph{\Ra}\quad \\
  F(a_1,...,a_{i-1},b,a_{i+1},...,a_n)>F(a_1,...,a_{i-1},c,a_{i+1},...,a_n)
  }
\end{small}

\vspace{20pt}

\framebox{\parbox{8cm}{Si \A{} est une algèbre ordonnée, munie d'un
    ordre noethérien, \\ si toutes les interprétations \bleu{f^{\A}}
    sont monotones, \ali alors \bleu{>_{\A}} est un ordre de
    réduction.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Polynômes monotones}
\bleu{A = \Natstar}

Les \bleu{f^{\A}_n\in \Sigma^{\A}_n} sont des polynômes à \bleu{n}
indéterminées de \bleu{\Nat [X_1,...,X_n]}.

Un \emph{polynôme} est \emph{monotone}
\begin{itemize}
\item s'il dépend de toutes ses indéterminées,
\item c'est-à-dire que pour chaque \bleu{i} tel que \bleu{1\le i \le
    n}, \\il contient un monôme avec une occurrence de \bleu{X_i}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Interprétations polynomiales}
Une \emph{interprétation polynomiale monotone} est une interprétation dans
laquelle toutes les interprétations sont des polynômes monotones.

\bigskip

L'ordre induit est un ordre de réduction, appelé \emph{ordre
  polynômial}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Exercice}
Prouver par un ordre polynômial la terminaison des systèmes suivants.

\fbox{\parbox{8cm}{\begin{center}
\bleu{
  \begin{array}[c]{rclrr}
  (x * y) * z &\ra& x * (y * z) && \textrm{\rouge{(A)}}\\
  f(x * y)    &\ra& f(x) * f(y) && \textrm{\rouge{(E)}}
  \end{array}
}
\end{center}}}
\vfill
\fbox{\parbox{8cm}{\begin{center}
\bleu{
  \begin{array}[c]{rclrr}
  (x * y) * z &\ra& x * (y * z) && \textrm{\rouge{(A)}}\\
  f(x) * f(y)     &\ra& f(x * y) && \textrm{\rouge{(E)}}\\
  f(x) * (f(y) * z)     &\ra& f(x * y) * z && \textrm{\rouge{(EA)}}
  \end{array}
}
\end{center}}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les limites des ordres polynômiaux I}
%  
  Prouver la satisfaction d'un ensemble
  \bl{\[(F_i(X_1,...,X_n)>G_i(X_1,...,X_n))_{1\le i\le m}\]}
  \begin{itemize}
  \item où \bleu{F_i\in \Nat[X_1,...,X_n]} et \bleu{G_i\in
      \Nat[X_1,...,X_n]}
  \item et où les \bleu{X_i} parcourent \bleu{\Nat}
\end{itemize}
est \emph{indécidable}.

\vfill

Pour le prouver on se ramène au $10^{eme}$ problème de Hilbert.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{$10^{eme}$ problème de Hilbert}
  
  Dans son $10^{eme}$ problème (1900) Hilbert demandait un algorithme
  pour \emph{déterminer si les systèmes d'équations diophantiennes  
  ont une solution} ou non,
  
Un système d'équations diophantiennes est une suite \bleu{(P_1,...,
  P_m)} o\`u les \bleu{P_i\in \mathbb{Z}[
  X_1,...,X_n]} sont des polynômes à coefficients entiers
relatifs.
  
  Une solution est un $n$-uplet \bleu{(a_1,...a_n)\in \mathbb{Z}^n}
  tel que \ali pour chaque \bleu{1\le i\le m}, on a \bleu{P_i(a_1,..., a_n)=0}.
  
  \emph{Youri Matijasevi{\v{c}}} (1970) a démontré que ce problème est
  \emph{indécidable}.

  \begin{footnotesize}
    \hfill \textcolor{vertfonce}{Le dixième problème de Hilbert, son
      indécidabilité}, Éditions Masson.
  \end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Réduction de la positivité des polynômes au $10^{eme}$
    problème de Hilbert} %
  Comme souvent pour démontrer qu'un problème est indécidable \\%
  \emph{on réduit le problème} en question à un problème de référence
  connu pour être indécidable.

Dans notre cas, le problème de référence est le $10^{eme}$ problème
de Hilbert.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Une suite de réductions} 
Nous n'allons pas faire une réduction en une seule étape, mais en
trois que nous allons appeler:
\begin{itemize}
\item \verdir{solutions dans $\Nat^n$,}
\item \verdir{positivité dans $\Nat^n$,}
\item \verdir{comparaison de polynômes dans $\Nat^n$.}
\end{itemize}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Première réduction: solutions dans $\Nat^n$ (1/4)} 

  \fbox{\parbox{8cm}{ Dans cette réduction, on montre que l'existence
      de zéros dans \bleu{\mathbb{N}^n} pour les polynômes à coefficients
      dans \bleu{\mathbb{Z}} se réduit à l'existence de zéros dans
      \bleu{\mathbb{Z}^n} pour les polynômes à coefficients dans
      \bleu{\mathbb{Z}}.  }}

J'appelle hyperquadrant de $\mathbb{Z}^n$ un ensemble \bleu{\{X_i~|~
  X_i \%_i 0\}} %
\ali où \bleu{\%_i} est soit \bleu{>},  soit \bleu{<}.  

Il y a $2 ^n$ hyperquadrants.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \subheading{Première réduction: solutions dans $\Nat^n$ (2/4)} 
 On peut transformer le système \bleu{(P_1,..., P_m)} en $2 ^n$ systèmes
\bleu{(P_{1,k},..., P_{m,k})} pour \bleu{1\le k\le 2^n} associés à
chaque hyperquadrant.

Dans chaque polynôme \bleu{P(X_1,...,X_n)} on transforme 
\begin{itemize}
\item \bleu{X_j} en \bleu{X_j} si on est dans un hyperquadrant où
  \bleu{X_j > 0}, 
\item et \bleu{X_j}
  en \bleu{-X_j} si on est dans un hyperquadrant où
  \bleu{X_j < 0}.
\end{itemize}


\vfill 
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Première réduction: solutions dans $\Nat^n$ (3/4)}
%
\textcolor{vertfonce}{Exemple :} \bleu{\{(X_1,X_2,X_3,X_4)~|~X_1>0,
  X_2<0,X_3<0,X_4>0\}} est un hyperquadrant de \bleu{\mathbb{Z}^4}.

Dans ce quadrant on transforme le polynôme \bleu{P(X_1,X_2,X_3,X_4)} en
\bleu{P(X_1,-X_2,-X_3,X_4)}.

\vspace*{20pt}

On voit que pour chaque système \bleu{(P_{1,k},..., P_{m,k})}, on peut
chercher chercher les solutions dans \bleu{\mathbb{N}^n} pour trouver
les solutions du système \bleu{(P_1,..., P_m)} dans le
$k^{\textrm{ème}}$ hyperquadrant.

\vfill 
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Première réduction: solution dans $\Nat^n$ (4/4)}
%
Donc si on a un algorithme pour décider si un système de polynômes
\bleu{(P_1,..., P_m)} a une solution dans  \bleu{\mathbb{N}^n}, 

\emph{alors }on a un algorithme pour décider si un système de polynômes
\bleu{(P_1,..., P_m)} a une solution dans  \bleu{\mathbb{Z}^n},

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Première réduction: solution dans $\Nat^n$ (4/4)}
%
Donc si on a un algorithme pour décider si un système de polynômes
\bleu{(P_1,..., P_m)} a une solution dans  \bleu{\mathbb{N}^n}, 

\emph{alors }on a un algorithme pour décider si un système de polynômes
\bleu{(P_1,..., P_m)} a une solution dans  \bleu{\mathbb{Z}^n},

\bigskip

\emph{alors} on a un algorithme pour résoudre le $10^{eme}$
    problème de Hilbert.


\vfill   \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Deuxième réduction: positivité dans $\Nat^n$}
  \fbox{\parbox{8cm}{ Dans cette réduction, on montre que la
      positivité dans \bleu{\mathbb{N}^n} pour les polynômes à
      coefficients dans \bleu{\mathbb{Z}} se réduit à l'existence de
      zéros dans \bleu{\mathbb{N}^n} pour les polynômes à coefficients
      dans \bleu{\mathbb{Z}}.  }}

Le problème de la positivité des systèmes de polynômes est de savoir
  si un système de \bleu{(Q_1,..., Q_m)} o\`u les \bleu{Q_i\in
    \mathbb{Z}[X_1,...,X_n]} est \emph{strictement
    positif pour tout} \bleu{(a_1,..., a_n)\in \mathbb{N}^n}.
  
  Si l'on a un algorithme pour la positivité des systèmes de
  polynômes, alors pour chaque système de polynômes \bleu{(P_1,...,
    P_m)} où les \bleu{P_i\in \mathbb{Z}[
    X_1,...,X_n]}, on est capable de répondre si le système
  \bleu{(P_1^2,..., P_m^2)} est strictement positif ou non sur
  \bleu{\mathbb{N}^n}, donc de décider s'il a une solution ou non dans
  \bleu{\mathbb{N}^n}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Troisième réduction: comparaison de polynômes dans
    $\Nat^n$ (1/3)}
%
  \fbox{\parbox{8cm}{ Dans cette réduction, on montre que comparer des
      couples de polynômes à coefficients dans \bleu{\mathbb{N}} se
      réduit à la positivité dans \bleu{\mathbb{N}^n} pour les
      polynômes à coefficients dans \bleu{\mathbb{Z}}.  }}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Troisième réduction: comparaison de polynômes dans
    $\Nat^n$ (2/3)}
%
Si on a un algorithme pour prouver la satisfaction d'un ensemble
  \bl{\[(F_i(X_1,...,X_n)>G_i(X_1,...,X_n))_{1\le i\le m}\]}
  \begin{itemize}
  \item où \bleu{F_i\in \Nat[X_1,...,X_n]} et \bleu{G_i\in
      \Nat[X_1,...,X_n]}
  \item et où les \bleu{X_i} parcourent \bleu{\Nat}
  \end{itemize}
\emph{alors} on a un algorithme pour prouver la positivité des systèmes
de \bleu{(Q_1,...,
    Q_m)} où les \bleu{Q_i\in \mathbb{Z}[X_1,...,X_n]}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Troisième réduction: comparaison de polynômes dans
    $\Nat^n$ (3/3)}
%
\emph{En effet}, chaque \bleu{Q_i} peut être décomposé en \bleu{Q_i =
  F_i - G_i} où \bleu{F_i\in \Nat[X_1,...,X_n]} et \bleu{G_i\in
      \Nat[X_1,...,X_n]}.  
    
    \emph{Et alors} prouver la positivité de \bleu{Q_i} revient à
    prouver \bleu{(F_i(X_1,...,X_n)>G_i(X_1,...,X_n))_{1\le i\le m}}.
    \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Prouver la positivité par ordinateur} 
%  
  Puisque c'est indécidable on peut se ramener à la décidabilité sur
  les réels qui est décidable, mais inefficace (méthode
  d'\emph{élimination des quantificateurs de Tarski}).
  
  On peut utiliser des heuristiques.  De toute façon la terminaison
  est indécidable!
\vfill
En pratique on  cherche des interprétations dans un espace plus petit:
\begin{itemize}
\item en limitant le degré,
\item et en limitant la taille des coefficients.
\end{itemize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les limites des ordres polynômiaux II}
%
La \emph{longueur maximale} des réductions d'un système de réécriture dont la 
terminaison est prouvée par un ordre polynômial est doublement
exponentielle.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8cm}{Si \bleu{R} est un système de réécriture dont
      la preuve de terminaison est faite par une interprétation
      polynômial monotone, alors il existe \bleu{c} telle que la
      longueur de toute dérivation à partir de \bleu{t} soit majorée
      par \bleu{2^{2^{c\|t\|}}}}}.



\vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8cm}{\emph{Si} \bleu{R} est un système de réécriture dont
      la preuve de terminaison est faite par une interprétation
      polynomiale monotone, \ali \emph{alors} il existe \bleu{c} telle que la
      longueur de toute dérivation à partir de \bleu{t} soit majorée
      par \bleu{2^{2^{c\|t\|}}}}}.

On fait l'hypothèse que  \bleu{R} n'a qu'un nombre fini de règles (on
peut généraliser à un nombre infini de règles).

Soit \bleu{t} un terme et \bleu{a} un entier quelconque pour
interpréter les variables de \bleu{t}.  Soit \bleu{\pi_a} un morphisme
qui prend la valeur \bleu{a} sur chaque variable.

Soit \bleu{t \ra t_1 \cdots \ra t_m} une dérivation partant de \bleu{t} et
de longueur \bleu{m}.   On a \bleu{\pi_a(t) > \pi_a(t_1) > \cdots>
  \pi_a(t_m)} donc \bleu{\pi_a(t) \ge m}.
\hfill \verdir{Il suffit donc de majorer \bleu{\pi_a(t)}.}

\end{slide}
%------------------------------------------------------
\begin{slide}
Soit \bleu{c \ge \log_2(k) +\log_2(\log_2(d))} o\`u pour chaque opérateur \bleu{f}
apparaissant dans le système de réécriture
\begin{bdp}
P_f(a_1,...,a_n) \le d\prod_{1\le i \le n} a_i^k.
\end{bdp}

On procède par récurrence sur la structure de \bleu{t}.

Si \bleu{t} est une constante alors \bleu{\pi_a(t) \le d \le
  2^{2^c}}.

\vfill 

Si \bleu{t = f(t_1,...,t_n)} alors 
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{small}
    \bl{
\begin{eqnarray*}
\pi_a(f(t_1,...,t_n)) &=& P_f(\pi(t_1),...,\pi(t_n))\\
   &\verdir{\le}& d\cdot\prod_{1\le i \le n} \pi(t_i)^k\\
   &\le& d\cdot\prod_{1\le i \le n} 2^{k\cdot 2^{c\cdot\|t_i\|}} %
   = d\cdot 2^{k\cdot\Sigma_{1\le i \le n} 2^{c\cdot\|t_i\|}}\\ 
   &\rouge{\le}& d\cdot 2^{k\cdot 2^{c\cdot\Sigma_{1\le i\le n}\|t_i\|}} %
   = 2^{\log_2(d)}\cdot 2^{k\cdot 2^{c\cdot\Sigma_{1\le i \le
         n}\|t_i\|}} \\
   & = & 2^{2^{\log_2(\log_2(d))} + k\cdot 2^{c\cdot\Sigma_{1\le i \le
         n}\|t_i\|}} \\
   & = & 2^{2^{\log_2(\log_2(d))} + 2^{\log_2(k) + c\cdot\Sigma_{1\le i \le
         n}\|t_i\|}} \\
   & \rouge{\le} & 2^{2^{c\cdot( 1+ \Sigma_{1\le i \le n}\|t_i\|)}}\\
   & = & 2^{2^{c\|t\|}}
\end{eqnarray*}
}
\end{small}
\begin{footnotesize}
  $\verdir{\le}$ par définition de \bleu{d} et \bleu{k}, \bleu{\le}
  par récurrence, $\emph{\le}$ par convexité de $n\mapsto 2^n$.
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
 \framebox{\parbox{3cm}{La borne est atteinte}}

\emph{Exercice :} Trouver un système de réécriture tel que la
longueur de la plus longue chaîne de dérivation soit doublement
exponentielle. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \framebox{\parbox{3cm}{La borne est atteinte}}

\emph{Exercice :} Trouver un système de réécriture tel que la
longueur de la plus longue chaîne de dérivation soit doublement
exponentielle. 

\verdir{Indication :} Un système de réécriture 
\begin{itemize}
\item qui ``calcule'' quelque chose comme une exponentielle (une
  puissance fixe d'un entier par exemple, cube, carré, \ldots),
\item dont la preuve de terminaison est faite par une interprétation
  polynomiale,
\item dans lequel il y un terme court qui se normalise en temps
  doublement exponentiel.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Le système suivant calcule le \emph{carré} d'un nombre
\bl{
  \begin{eqnarray*}
 0 + m & \ra & m\\
s(n) + m &\ra & s(n +m) \\
double(0) &\ra&0\\
double(s(n)) &\ra& s(s(double(n)))\\
carre(0) &\ra & 0\\
carre(s(n)) &\ra& s(carre(n) + double(n))
  \end{eqnarray*}
}
est prouvé terminer par un ordre polynomial.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Le système suivant calcule le \emph{carré} d'un nombre
\bl{
  \begin{eqnarray*}
 0 + m & \ra & m\\
s(n) + m &\ra & s(n +m) \\
double(0) &\ra&0\\
double(s(n)) &\ra& s(s(double(n)))\\
carre(0) &\ra & 0\\
carre(s(n)) &\ra& s(carre(n) + double(n))
  \end{eqnarray*}
}
réduit le terme \bleu{carre^{n+1}(s(s(0)))} (de taille $n+4$) vers
\bleu{carre(s^{2^{2^n}}(0))} dont la réduction demande au moins
$2^{2^n}$ appels à la dernière règle du système.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les limites des ordres polynômiaux III}

  \framebox{\parbox{8cm}{ \emph{Si} un système de réécriture
      \emph{calcule une fonction entière} (avec les deux constructeurs
      \bleu{0} et \bleu{s}) et a une \emph{preuve de terminaison fondée sur
      un ordre polynomiale},
\ali \emph{alors} cette fonction est à
      croissance polynomiale.}}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\emph{Exercice :} Le système \bl{
  \begin{eqnarray*}
 0 + m & \ra & m\\
s(n) + m &\ra & s(n +m) \\
binom(n,0) &\ra & 1\\
binom(0, s(p)) & \ra & 0 \\
binom(s(n), s(p)) &\ra & binom(n, s(p))+ binom(n,p)
  \end{eqnarray*}
}
ne possède pas de preuve de terminaison fondée sur un ordre
polynômial. 

Comment faut-il faire, si on veut le faire par une algèbre ordonnée?

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Les beaux ordres}}}
\end{center}
 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les bons ordres}
Les \emph{bons ordres} sont les ordres noethériens totaux.

Les bons ordres sont aussi appelés des \emph{ordinaux}.

En réécriture, nous sommes intéressés par des \emph{ordres partiels}.
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ordre noethérien et incrémentalité}
%
Jusqu'à maintenant, on a montré qu'un ordre était noethérien parce
qu'il était contenu dans un ordre qui était noethérien.

Mais un informaticien veut construire les ordres noethériens
\emph{incrémentalement}, c'est-à-dire en ajoutant de nouvelles paires à un
ordre déjà connu.

C'est exactement ce qui se passe dans une procédure de
\emph{complétion}.  On ajoute des paires nouvelles à l'ordre
correspondant aux identités que l'on a ne sait pas orienter.

Il faut donc \emph{agrandir} l'ordre à la \emph{volée}.

 \end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{6cm}{\emph{Définition :} Un ordre est incrémental
      si :
\begin{itemize}
\item il est noethérien,
\item tout ordre qui le contient est noethérien.
\end{itemize}
}}

Un ordre incrémental doit être ``beau'' : \ali il ne doit être \verdir{ni trop
  grand, ni trop gros}.

 \end{slide}
%------------------------------------------------------
\begin{slide}
\emph{Ni trop grand :} noethérien,

\emph{Ni trop gros :} il n'y a pas d'\emph{antichaîne} infinie.

Une \emph{antichaîne} est un ensemble tel que \bleu{x \le y \quad
  \Ra\quad x=y}.  

C'est-à-dire que dans une antichaîne, tous les éléments sont tous deux à deux
incomparables.

\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
\subheading{Je rappelle}
%
\bleu{\le} est un préordre donné \ali (c'est-à-dire un relation réflexive et
transitive).

\bleu{x < y}\quad \rouge{$\Leftrightarrow$} \quad \bleu{x \le y} et \bleu{\neg(x\ge
  y)} \ali (irréflexive, antisymétrique et transitive).

\bleu{x\sim y}\quad \rouge{$\Leftrightarrow$} \quad \bleu{x \le y} et \quad \bleu{x
  \ge y} \ali (relation d'équivalence).

\bleu{x\# y}\quad  \rouge{$\Leftrightarrow$} \quad \bleu{\neg(x \le y)} et \quad
\bleu{\neg(x \ge y)}. 
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  Une suite \bleu{(x_i)_{i\in \Nat}} dans laquelle il existe \bleu{i}
  et \bleu{j} \ali tels que \bleu{i<j} et \bleu{x_i \le x_j} est dite
  \emph{bonne}.

Si une suite n'est pas \verdir{bonne}, elle est \emph{mauvaise}.

Une \emph{sous-suite} de \bleu{(x_i)_{i\in \Nat}} est donnée \ali par
une application \bleu{\phi:\Nat \rightarrow\Nat} croissante, \ali
autrement dit la sous-suite est celle des \bleu{(x_{\phi(i)})_{i\in
    \Nat}}
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{9cm}{Les définitions suivantes sont équivalentes :
    \begin{enumerate}
    \item l'ordre est incrémental
    \item l'ordre est noethérien et sans antichaîne infinie,
    \item toute suite est bonne, 
    \item de toute suite \bleu{(x_i)_{i\in \Nat}} on peut extraire une 
        sous-suite croissante. 
    \end{enumerate}
}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\framebox{\parbox{9cm}{Les définitions suivantes sont équivalentes :
    \begin{enumerate}
    \item l'ordre est incrémental
    \item l'ordre est noethérien et sans antichaîne infinie,
    \item toute suite est bonne,
    \item de toute suite \bleu{(x_i)_{i\in \Nat}} on peut extraire une 
        sous-suite croissante. 
    \end{enumerate}
}}

\vspace*{20pt}
\begin{center}
\begin{tabular}{c}
\verdir{(1) $\Longrightarrow$ (2)}\\
\verdir{(4) $\Longrightarrow$ (3)}\\
\verdir{(3) $\Longrightarrow$ (2)}
\end{tabular}\quad\quad
\begin{tabular}{c}
\rouge{(2) $\Longrightarrow$ (1)}\\
\rouge{(2) $\Longrightarrow$ (3)}\\
\rouge{(3) $\Longrightarrow$ (4)}
\end{tabular}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{(2) $\Longrightarrow$ (1)}

Supposons que l'ordre est noethérien sans antichaîne infinie.

Soit un ordre \bleu{\sqsupset} qui contient \bleu{>} et une suite infinie
\bleu{(x_i)_{i\in\Nat}} décroissante pour \bleu{\sqsupset}.

Dans cette suite il existe une sous-suite
\bleu{(x_{\phi(i)})_{i\in\Nat}} telle que 
\begin{center}
  \bleu{i>j \Ra x_{\phi(i)} \sqsupset x_{\phi(j)} \wedge
    \neg(x_{\phi(i)} > x_{\phi(j)})}.
\end{center}


Si on ne pouvait pas construire cette sous-suite, cela voudrait dire
qu'à tout moment chaque élément serait plus grand pour \bleu{>} que
ses suivants.
 \ali ce qui serait une contradiction avec le fait que
\bleu{>} est noethérien.

\bleu{(x_{\phi(i)})_{i\in\Nat}} est un antichaîne infinie pour
\bleu{>}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{(2) $\Longrightarrow$ (3)}

Supposons qu'il n'y ait pas de suite infinie strictement décroissante. 

Soit une suite mauvaise.

On considère la suite extraite \bleu{(x_{\phi(i)})_{i\in\Nat}} ainsi
\begin{itemize}
\item \bleu{x_{\phi(0)}} est tel que pour \bleu{j>\phi(0)} on a
  \bleu{x_{\phi(0)}\# x_j} .  C'est possible, car la suite est
  mauvaise et il n'y a pas de suite infinie strictement décroissante.
  
\item \bleu{x_{\phi(k+1)}} est tel que \bleu{\phi(k)<\phi(k+1)} et pour
  \bleu{j>\phi(k+1)} on a \bleu{x_{\phi(k+1)}\# x_j} .
\end{itemize}
Cette suite extraite \bleu{(x_{\phi(i)})_{i\in\Nat}} est une
antichaîne infinie.\hfill \verdir{Contradiction !}  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\rouge{(3) $\Longrightarrow$ (4)}

Soit une suite qui n'admet pas de sous-suite croissante.  

Les sous-ensembles \emph{maximaux} qui sont ordonnés par indices croissants \emph{et}
sont faiblement croissants pour \bleu{\le} sont tous finis.
\begin{itemize}
\item Ils sont en nombre \emph{infini}.
\item Ils ont tous un \emph{dernier élément}.  
\end{itemize}
La suite (infinie) \bleu{(x_{\phi(i)})_{i\in\Nat}} de ces derniers
éléments est bonne, donc il existe dans cette suite \bleu{i < j} avec
\bleu{x_{\phi(i)}\le x_{\phi(j)}}.  

En contradiction avec la supposition que \bleu{x_{\phi(i)}} est un
dernier élément~!
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Beaux ordres}
%
Les ordres qui satisfont les conditions du lemme précédent sont appelés
aussi des \emph{beaux ordres.}

\vfill

 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Beaux ordres}
%
Les ordres qui satisfont les conditions du lemme précédent sont appelés
aussi des \emph{beaux ordres.}

\vspace*{20pt}

Le \emph{produit} \verdir{(composante par composante)} de beaux ordres
est un bel ordre.

Le \emph{produit} d'ordre \bleu{(A_1,\le_1) \times \dots \times
  (A_n,\le_n)} est défini par 
\begin{bdp}
(a_1, ..., a_n) \le_1 \times ...\times\le_n (b_1, ..., b_n) \quad
\rouge{\Longleftrightarrow}\quad \bigwedge_{i=1}^n a_i\le_i b_i
\end{bdp}


\vfill

 \end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Le plongement}}}
\end{center}
 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le plongement}
Considérons le système de réécriture \Emb{} qui contient pour chaque
\bleu{f\in\Sigma_n} et chaque \bleu{1\le i\le n} une règle,
\bl{
  \begin{eqnarray*}
    f(x_1,...,x_n) \ra x_i
  \end{eqnarray*}
}

\bleu{\plgt} est sans cycle. 


La relation \bleu{\plgt} est un ordre strict noethérien qui s'appelle
le \emph{plongement}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le plongement}
%
Intuitivement, un terme \bleu{t} est plongé dans un terme \bleu{t'},
si \bleu{t'\plgt t}, c'est-à-dire si on passe de \bleu{t'} à \bleu{t} en effaçant
des n{\oe}uds et en recollant un terme fils du n{\oe}ud manquant à la
place laissée libre.
le \emph{plongement}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&&& f \ar@{-}[dll]\ar@{-}[drr] & \\
&&  f \ar@{-}[dl]\ar@{-}[dr] &&&&  g \ar@{-}[dl]\ar@{-}[dr]\\
& g \ar@{-}[dl]\ar@{-}[dr] && b && h\ar@{-}[d] && b &&\\
a && a &&& a 
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&&& f \ar@{-}[dll]\ar@{-}[drr] & \\
&&  \emph{f} \ar@{-}[dl]\ar@{-}[dr] &&&&  g \ar@{-}[dl]\ar@{-}[dr]\\
& \verdir{g} \ar@{-}[dl]\ar@{-}[dr] && b && h\ar@{-}[d] && b &&\\
a && a &&& a 
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&&& f \ar@{-}[dll]\ar@{-}[drr] & \\
&&  \verdir{g} \ar@{-}[dl]\ar@{-}[dr] &&&&  g \ar@{-}[dl]\ar@{-}[dr]\\
& a && a && h\ar@{-}[d] && b &&\\
 &&  &&& a 
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&&& f \ar@{-}[dll]\ar@{-}[drr] & \\
&&  g \ar@{-}[dl]\ar@{-}[dr] &&&&  g \ar@{-}[dl]\ar@{-}[dr]\\
& a && a && \emph{h}\ar@{-}[d] && b &&\\
 &&  &&& \verdir{a} 
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\xymatrix{
&&&& f \ar@{-}[dll]\ar@{-}[drr] & \\
&&  g \ar@{-}[dl]\ar@{-}[dr] &&&&  g \ar@{-}[dl]\ar@{-}[dr]\\
& a && a && \verdir{a} && b &&\\
 &&  &&& 
}
\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le plongement dans $A^*$}
%
Les termes de \bleu{A^*} sont les termes monadiques.

Le plongement est défini par
\begin{footnotesize}
\begin{itemize}
\item \bleu{(\forall \alpha\in A^+)\quad \alpha \plgt \varepsilon},
\item \bleu{(\forall \alpha\in A^*)(\forall \beta\in A^*)(\forall
    \verdir{a}\in{A})\; \alpha \plgt \beta \quad \emph{\Ra} \quad
    \verdir{a}\alpha \plgt \verdir{a}\beta}
\item \bleu{(\forall \alpha\in A^*)(\forall \beta\in A^*) (\forall
    \verdir{a}\in A)\; \alpha \rasupsub{*}{\Emb} \beta \quad \emph{\Ra} \quad \verdir{a}\alpha \plgt \beta}
\end{itemize}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Le Théorème de Higman}}}
\end{center}
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Théorème de Higman} 
  %
  \framebox{\parbox{7cm}{Si \bleu{A} est fini, le plongement est un bel ordre sur
      \bleu{A^*}.}}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème de Higman}
%
\framebox{\parbox{7cm}{Si \bleu{A} est fini, le plongement est un bel ordre sur
    \bleu{A^*}.}}

Supposons que  \bleu{A^*, \plgt} n'est pas un bel ordre.

Soit une suite \bleu{(\alpha_i)_{i\in\Nat}} \verdir{mauvaise et minimale}
définie de la façon suivante.

\begin{enumerate}
\item \bleu{\alpha_0} est un des plus petits éléments qui commence une 
  mauvaise suite.
\item \bleu{\alpha_i} est le plus petit élément en $i$ème position
  d'une mauvaise suite qui commence par \bleu{\alpha_0,...\alpha_{i-1}}.
\end{enumerate}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Cette suite ne contient aucun \bleu{\varepsilon}.  Donc tous les termes
sont de la forme \bleu{a_i\alpha_i'}.

On peut extraire une sous-suite \bleu{a\alpha_{\phi(i)}'}, pour le même
\bleu{a} (parce que \bleu{A} est fini).

La suite
\bleu{\alpha_0,...\alpha_{\phi(0)-1},\alpha_{\phi(0)}',...,\alpha_{\phi(j)}'...
} est \verdir{bonne}.

Donc 
\begin{enumerate}
\item soit  \bleu{\alpha_k\plonge \alpha_{\phi(j)}'} pour \bleu{0\le
    k<\phi(0)}  et \bleu{0\le j}, \ali donc \bleu{\alpha_k\plonge
    a\alpha_{\phi(j)}'}, contradiction!
\item soit \bleu{\alpha_{\phi(j)}'\plonge \alpha_{\phi(j')}'} pour
  \bleu{0\le j<j'}, \ali donc \bleu{a\alpha_{\phi(j)}'\plonge
    a\alpha_{\phi(j')}'}, contradiction!
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème de Higman généralisé}
On a besoin du théorème de Higman sur un alphabet infini dénombrable.

\emph{Comment le généraliser?}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème de Higman généralisé}
On a besoin du théorème de Higman sur un alphabet infini dénombrable.

\emph{Comment le généraliser?}

\begin{itemize}
\item Il faut ordonner \bleu{A} par un bel ordre,
\item Il faut généraliser l'énoncé.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Plongement avec restriction sur $A^*$} 
\begin{footnotesize}
\begin{itemize}
\item \bleu{(\forall \alpha\in A^+)\quad \alpha \plgt \varepsilon},
\item \bleu{(\forall \alpha\in A^*)(\forall \beta\in A^*)(\forall
    a\in{A})\ali \verdir{a} \ge \verdir{b} \;\emph{\et}\;\alpha \plgt
    \beta \quad \emph{\Ra} \quad \verdir{a}\alpha \plgt \verdir{b}\beta}
\item \bleu{(\forall \alpha\in A^*)(\forall \beta\in A^*) (\forall
    \verdir{a}\in A)\; \alpha \rasupsub{*}{\Emb} \beta \quad \emph{\Ra} \quad
    \verdir{a}\alpha \plgt \beta}
\end{itemize}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Théorème de Higman généralisé} 
  %
  \framebox{\parbox{6cm}{Si \bleu{\ge} est un bel ordre sur \bleu{A} \ali le
      plongement est un bel ordre sur \bleu{A^*}.}}
  
  Là où on a dit \ali ``On peut extraire une sous-suite
  \bleu{a\alpha_{\phi(i)}'}, pour le même
  \bleu{a}.'',
  
  on dit \ali``On peut extraire une sous-suite
  \bleu{a_{\phi(i)}\alpha_{\phi(i)}'} \ali telle que la suite
  \bleu{a_{\phi(i)}} soit croissante.''  

Le reste de la démonstration est identique.

\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Le théorème de Kruskal}}}
\end{center}
 \end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Théorème de Kruskal} 
  %
 \framebox{\parbox{8cm}{Si \bleu{\Sigma} est fini, le plongement est un bel
     ordre sur \bleu{T(\Sigma, X)}.}}  \vfill \vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Théorème de Kruskal} 
  %
 \framebox{\parbox{8cm}{Si \bleu{\Sigma} est fini, le plongement est un bel
     ordre sur \bleu{T(\Sigma, X)}.}}

Supposons que le plongement n'est pas un bel ordre.

Considérons une mauvaise suite minimale, construite comme dans le
théorème de Higman. (\verdir{Exercice :} refaire la construction.)

De cette suite on peut extraire une sous-suite de la forme
\bleu{(f(s_1^i, ...,s_n^i))_{i\ge 0}}. 

\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
Les \bleu{n} suites \bleu{(s_j^i)_{i\ge 0}} ainsi que leurs sous-suites
sont bonnes. 

De \bleu{(s_1^i)_{i\ge 0}} on peut extraire une sous-suite croissante
\bleu{(s_1^{\phi_1(i)})_{i\ge 0}}.

De \bleu{(s_2^{\phi_1(i)})_{i\ge 0}} on peut extraire une sous-suite
croissante \bleu{(s_2^{\phi_2\phi_1(i)})_{i\ge 0}}.

\centerline{$\vdots$}

De \bleu{(s_n^{\phi_{n-1}...\phi_1(i)})_{i\ge 0}} on peut extraire une sous-suite
croissante \bleu{(s_n^{\phi_n....\phi_1(i)})_{i\ge 0}}.

Clairement la suite 
\bleu{(f(s_1^{\phi_{n}...\phi_1(i)},...,s_n^{\phi_{n}...\phi_1(i)}))_{i\ge 
    0}} est croissante.  \emph{Contradiction !}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Plongement avec restriction sur $T(\Sigma, X)$} 
%
Un ordre sur \bleu{\Sigma} est appelé une \emph{précédence}.

On se donne
\begin{itemize}
\item une précédence \bleu{\ge}
\item et un système de réécriture appelé \emph{restriction} \ali tel
  que pour chaque \bleu{f} et chaque \bleu{g} avec \bleu{f\ge g} %
  \ali et chaque permutation \bleu{\pi: [1..n]\ra[1..n]}
\end{itemize}
\bl{
  \begin{eqnarray*}
    f(x_1,...,x_n) \ra g(x_{\pi(1)},...,x_{\pi(p)})
  \end{eqnarray*}
}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Plongement avec restriction sur $T(\Sigma, X)$} 
%
Le \emph{plongement avec restriction} est défini par les règles de
\bleu{\Emb} (\verdir{effacement}) et les règles de \emph{restriction}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Théorème de Kruskal} 
 \framebox{\parbox{8cm}{Si \bleu{(\Sigma,\le)} est un bel ordre, le
     plongement avec restriction est un bel ordre sur \bleu{T(\Sigma,
       X)}.}}  \vfill \vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Les ordres de simplification}}}
\end{center}
 \end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ordre de simplification}
%
Un \emph{ordre de simplification} est un ordre de réécriture \bleu{>}
qui satisfait la propriété de \emph{sous-terme}, c'est-à-dire :
\begin{bdp}
(\forall p \in Pos(t))\qquad t> t_{|p}
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ordre de simplification}
%
Un \emph{ordre de simplification} est un ordre de réécriture \bleu{>}
qui satisfait la propriété de \emph{sous-terme}, c'est-à-dire :
\begin{bdp}
(\forall p \in Pos(t))\qquad t> t_{|p}
\end{bdp}

\vspace*{10pt}

Combiné avec la comptabilité, les ordres de simplification contiennent le 
plongement.  Donc
\ali les ordres de simplification sont des beaux ordres,
\ali les ordres de simplification terminent,
\ali les ordres de simplification sont des ordres de réduction.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'ordre lexicographique sur les chemins} 
  %
  Supposons donné un préordre \bleu{\le} sur \bleu{\Sigma} appelé
  \emph{précédence}.  
  
  \hspace*{40pt}\bleu{s \lpo t}  \hspace*{40pt}\mbox{ssi}\\
  \emph{(A)} \quad \bleu{s} \mbox{~est une variable~} \bleu{x},
  \bleu{t} n'est pas une variable et \bleu{x\in Var(t)} \\
  \hspace*{20pt}\mbox{ou}\\
  \emph{(B1)} \quad \bleu{s\equiv f(s_1,...,s_m)} \mbox{~et~}
  \bleu{t \equiv   g(t_1,...,t_n) } \ali et \quad \bleu{\forall
    i\in[1..m]~s_i\lpo t} \\ 
  \emph{(B2)} \\
  \hspace*{30pt}\emph{(B21)} \bleu{f<g} \quad \verdir{ou}\\
  \hspace*{30pt}\emph{(B22)} \bleu{f\sim g} et
  \bleu{(s_1,...,s_m)\lpo^{lex}(t_1,...,t_n)} \quad \verdir{ou}\\
  \hspace*{30pt}\emph{(B23)} \bleu{\exists j\in[1..n] s \lepo t_j}
  \vfill \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'ordre lexicographique sur les chemins} 
%
\framebox{\parbox{2.5cm}{\bleu{\lpo} est un ordre.}}

Antisymétrique

Transitivité.

Simplification.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'ordre lexicographique sur les chemins} 
%
\framebox{\parbox{4.5cm}{\bleu{\lpo} est un ordre de simplification.}}


\bleu{\lpo} est \emph{compatible} et \emph{clos par
  substitution} et satisfait la \emph{propriété de sous-terme}.

Donc \bleu{\lpo} est un \emph{ordre de réduction}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice : Fonction d'Ackermann-Peter} 
Prouver la terminaison de la fonction d'Ackermann-Peter
\bl{
\begin{eqnarray*}
  A(0,n) & \ra & s(n)\\
  A(s(m), 0) & \ra & A(m, s(0))\\
  A(s(m), s(n)) &\ra& A(m, A(s(m),n))
\end{eqnarray*}
}\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice : (E) + (A)}
%
Premier cas :

\begin{center}
\bleu{
  \begin{array}[c]{rclrr}
  (x * y) * z &\ra& x * (y * z) && \textrm{\rouge{(A)}}\\
  f(x * y)    &\ra& f(x) * f(y) && \textrm{\rouge{(E)}}
  \end{array}
}
\end{center}

Deuxième cas :

\begin{center}
\bleu{
  \begin{array}[c]{rclrr}
  (x * y) * z &\ra& x * (y * z) && \textrm{\rouge{(A)}}\\
  f(x) * f(y)     &\ra& f(x * y) && \textrm{\rouge{(E)}}\\
  f(x * y) * z    &\ra& f(x) * (f(y) * z)  && \textrm{\rouge{(EA)}}\\
  \end{array}
}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice : (E) + (A)}
%
Troisième cas :

\begin{center}
\bleu{
  \begin{array}[c]{rclrr}
  (x * y) * z &\ra& x * (y * z) && \textrm{\rouge{(A)}}\\
  f(x) * f(y)     &\ra& f(x * y) && \textrm{\rouge{(E)}}\\
  f(x) * (f(y) * z)     &\ra& f(x * y) * z && \textrm{\rouge{(EA)}}
  \end{array}
}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice : les groupes}
%
%
\renewcommand{\bar}[1]{i(#1)}
\newcommand{\ix}{\ensuremath{\bar{x}}}
\newcommand{\iix}{\ensuremath{\bar{\bar{x}}}}
\begin{footnotesize}
\vspace*{-15pt}
\bl{\begin{eqnarray*}
x * e & \ra &  x \\
e * x & \ra &  x \\
x * \ix & \ra & e \\
\ix * x & \ra & e \\
\bar{e} & \ra & e \\
\iix & \ra & x \\
\bar{x * y} & \ra & \bar{y} * \ix \\
(x * y) * z & \ra & x * (y * z) \\
x * (\ix * y) & \ra & y \\
\ix * (x * y) & \ra & y
\end{eqnarray*}}
\end{footnotesize}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le statut des opérateurs}
%
On peut choisir de prendre l'ordre lexicographique %
\ali de \emph{gauche à droite}, %
\ali ou de \emph{droite à gauche}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice : les groupes (variante avec division)}

\vspace*{-18pt}

\begin{footnotesize}
\bl{\begin{eqnarray*}
i(e) & \ra & e \\
x / e & \ra &  x \\
e / x & \ra &  i(x) \\
x / x & \ra & e \\
i(x / y) & \ra & y / x \\
i(i(x)) & \ra & x \\
x / (y / z) & \ra & (x / i(z)) / y\\
(x / i(y)) / y & \ra & x\\
(x / y) / i(y) & \ra & x
\end{eqnarray*}}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice : les groupes (variante avec division)}

\vspace*{-8pt}

\begin{footnotesize}
\bleu{\begin{array}{ccc}
i(e) & \ra & e \\
x / e & \ra &  x \\
e / x & \ra &  i(x) \\
x / x & \ra & e \\
i(x / y) & \ra & y / x \\
i(i(x)) & \ra & x \\
x / (y / z) & \ra & (x / i(z)) / y\\
(x / i(y)) / y & \ra & x\\
(x / y) / i(y) & \ra & x
\end{array}}
\begin{math}
\rouge{\begin{array}{ccc}
x * y &\ra& x / i(y)
\end{array}}
\end{math}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Exercice d'école}
 \bl{\begin{eqnarray*}
f(f(x)) & \ra & f(g(f(x)))
   \end{eqnarray*}}
    \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice : une définition tarabiscotée de l'identité}  
\bl{\begin{eqnarray*}
i(s(x)) & \ra & s(i(p(s(x))))\\
i(0) & \ra & 0\\
p(s(0)) & \ra & 0\\
p(s(s(x)) & \ra & s(x)
   \end{eqnarray*}}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exercice : pgcd} 
\begin{scriptsize} 
  \bl{\begin{eqnarray*}
      if(s(m), s(n),p,q) & \rightarrow & if(m,n,p,q)\\
      if(s(m),0,p,q) & \rightarrow & p\\
      if(0,n,p,q) & \rightarrow & q\\[5pt]
      s(m)- s(n) & \rightarrow & m - n\\
      s(m)- 0 & \rightarrow & m\\
      0 - s(n) & \rightarrow & 0\\[5pt]
      \emph{pgcd}(m,0) &\rightarrow& m\\
      \emph{pgcd}(0,m) &\rightarrow& m\\
      \emph{pgcd}(s(m),s(n)) &\rightarrow &
          if(m,n,\emph{pgcd}(m-n,s(n)),\emph{pgcd}(s(m),n-m))
\end{eqnarray*}}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  Post l'acyclicité diophantiennes uplet Youri Matijasevi uds ud
% LocalWords:  positivité morphisme incrémentalement Kruskal sous-arbres Higman
% LocalWords:  sous-suites PCP sous-suite holorime hyperquadrant polynômiaux II
% LocalWords:  l'hyperquadrant polynômial d'holorime monadique Subst ssi Masson
