%% Time-stamp: <modified on  4 Nov 2004 at 09:32 by Pierre Lescanne>
%% /MIM-1/REECRITURE/UNIFICATION/unif.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,amssymb,stmaryrd}
\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}

\rotateheaderstrue       % si tu combines slide et slide*

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

\author{Unification}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\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{\Nat}{\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{\U}{{\cal U}}
\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{\eq}{\stackrel{?}{=}}

\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]{\emph{#1}\ali #2 \Mapsto #3}

\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{\ar@{>}[r] &}}
\newcommand{\ranorm}{\xymatrix{\ar@{>>|}[r] &}}
\newcommand{\rara}{\xymatrix{\ar@{>>}[r] &}}
\newcommand{\longequiv}{\xymatrix{\ar@3{-}[r] &}}

%%%%%%%%%%%%%%%%%%%% iteration of arrows  %%%%%%%%%%%%%%%%%%%%
\newcommand{\rastar}{\rasup{*}}
\newcommand{\raplus}{\rasup{+}}

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

\newcommand{\rasub}[1]{\xymatrix{\ar@{>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix{\ar@{<-}[r]_{#1} &}}
\newcommand{\ranormsub}[1]{\xymatrix{\ar@{>>|}[r]_{#1} &}}
\newcommand{\rarasub}[1]{\xymatrix{\ar@{>>}[r]_{#1} &}}
\newcommand{\rasup}[1]{\xymatrix{\ar@{>}[r]^{#1} &}}
\newcommand{\supar}[1]{\xymatrix{\ar@{<-}[r]^{#1} &}}
\newcommand{\rarasup}[1]{\xymatrix{\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix{\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\rarasupsub}[2]{\xymatrix{\ar@{>>}[r]^{#1}_{#2} &}}
\newcommand{\cv}[1]{\xymatrix{\ar@{<->}[r]_{#1} &}}
\newcommand{\conv}[1]{\xymatrix{\ar@{<->}[r]_{#1}^{*} &}}
\newcommand{\convplus}[1]{\xymatrix{\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{&\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]{%      % 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}
\vspace*{.8cm}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{La problème de l'unification}}}
\end{center}
\bigskip
%
%%%%%%%%%%%%%%
\begin{center}
\includegraphics[width=2.5cm]{Herbrand.eps} %\hfill
\end{center}
%%%%%%%%%%%%%%
%
\centerline{Jacques Herbrand}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Équation}

Le but de l'unification est de résoudre des équations.

Un \emph{problème équationnel} est un ensemble fini de
paires~\footnote{Attention il s'agit bien de \emph{paires} et pas de
  \emph{couples} !} de termes:

\begin{bdp}
P = \{s_1\eq t_1, ..., s_n\eq t_n\}
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Équation}

Le but de l'unification est de résoudre des équations.

Un \emph{problème équationnel} est un ensemble fini de
paires~\footnote{Attention il s'agit bien de \emph{paires} et pas de
  \emph{couples} !} de termes:

\begin{bdp}
P = \{s_1\eq t_1, ..., s_n\eq t_n\}
\end{bdp}

\bleu{s_i\eq t_i} est une \emph{équation}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Convention} 

Si \bleu{t_i} dans \bleu{s_i\eq t_i} est une variable \bleu{x_i},\ali
on écrira plutôt \bleu{x_i\eq s_i} que \bleu{s_i\eq x_i}~!

La variable isolée, si elle existe est toujours à gauche.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Solution} 
  
  Une \emph{solution} de \bleu{P} ou un \emph{unificateur} de \bleu{P}
  est une substitution \bleu{\sigma} telle que

  \begin{center}
    \bleu{
\begin{array}{c}
\sigma(s_1) = \sigma(t_1)\\
\vdots\\
\sigma(s_n)= \sigma(t_n)
\end{array}
}
  \end{center}

  
  L'\emph{ensemble des unificateurs} de \bleu{P} est noté
  \bleu{\U(P)}.

Si \bleu{\U(P)\not=\emptyset} on dit que \bleu{P} est \emph{unifiable}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\normalsize Exemple 1}
Soit le problème :
\begin{bdp}
\xymatrix{
& {*}\ar@{-}[ld]\ar@{-}[rd] &&&& {*}\ar@{-}[ld]\ar@{-}[rd]  &&\\
i\ar@{-}[d] && x & \eq & y && {*}\ar@{-}[ld]\ar@{-}[rd]  \\
x &&&&& z && u
}
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\normalsize Exemple 1}
Soit le problème :
\begin{bdp}
\xymatrix{
& {*}\ar@{-}[ld]\ar@{-}[rd] &&&& {*}\ar@{-}[ld]\ar@{-}[rd]  &&\\
i\ar@{-}[d] && x & \eq & y && {*}\ar@{-}[ld]\ar@{-}[rd]  \\
x &&&&& z && u
}
\end{bdp}
Les substitutions %
\ali\bleu{\{x\mapsto i(u) * u,\quad y\mapsto i(i(u)*u),\quad z \mapsto
  i(u)\}} %
\ali \bleu{\{x\mapsto z * u,\quad y\mapsto i(z * u)\}}\hfill
  sont chacune des solutions.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\normalsize Exemple 2}
Le problème :
\begin{bdp}
\xymatrix{
& {*}\ar@{-}[ld]\ar@{-}[rd] &&&& {*}\ar@{-}[ld]\ar@{-}[rd]  &&\\
i\ar@{-}[d] && x & \eq & y && y\\
x
}
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\normalsize Exemple 2}
Le problème :
\begin{bdp}
\xymatrix{
& {*}\ar@{-}[ld]\ar@{-}[rd] &&&& {*}\ar@{-}[ld]\ar@{-}[rd]  &&\\
i\ar@{-}[d] && x & \eq & y && y\\
x
}
\end{bdp}
n'a pas de solution, car il faudrait que \bleu{\sigma(x) =
  i(\sigma(x))}.

Ce qui est impossible.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ordre sur les substitutions}
L'ensemble \bleu{Sub(T(\Sigma,V))} est muni d'un ordre \bleu{\lesssim}
défini par

\begin{center}
  \bleu{\sigma\lesssim\tau} si et seulement si \bleu{(\exists \rho\in
    Sub(T(\Sigma,V)) \quad \tau = \rho\sigma}.
\end{center}

\bleu{\sigma} est dite \emph{plus générale} que \bleu{\tau}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{MGU}
L'\emph{unificateur le plus général }de \bleu{P} (ou \emph{mgu}) est
une substitution \bleu{\sigma} telle que
\begin{enumerate}
\item \bleu{\sigma} est un unificateur de \bleu{P}, c-à-d
  \bleu{\sigma\in \U(P)}.
\item Si \bleu{\theta\in\U(P)} alors \bleu{\sigma\lesssim\theta}.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Forme résolue}
Soit  \bleu{P} un problème contenant \bleu{x\eq t}.

\bleu{x\eq t} est en \emph{forme résolue} dans \bleu{P} si \bleu{x}
n'apparaît nulle part ailleurs dans \bleu{P}.  %
\ali En particulier,
\begin{itemize}
\item \bleu{x\notin Var(t)} 
\item et il n'y a pas d'autre équation de la forme
  \bleu{x\eq s}.
\end{itemize}

\bleu{x} est alors dite \emph{résolue}.

\emph{Un problème est résolu} si toutes ses équations sont en forme
résolue.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8cm}{Si \bleu{P = \{x_1\eq t_1,...,x_n\eq t_n\}}
      est résolu, \ali alors \bleu{\sigma= \{x_1\mapsto
        t_1,...,x_n\mapsto t_n\}} est un mgu de \bleu{P}.}}

\vspace*{20pt}

On note \bleu{\sigma_P} \ali au lieu de \bleu{\{x_1\mapsto
  t_1,...,x_n\mapsto t_n\}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8cm}{Si \bleu{P = \{x_1\eq t_1,...,x_n\eq t_n\}}
      est résolu, \ali alors \bleu{`s= \{x_1\mapsto
        t_1,...,x_n\mapsto t_n\}} est un mgu de \bleu{P}.}}

\brunir{Démonstration :} 

\bleu{\sigma} \textcolor{vertfonce}{est un unificateur de} \bleu{P}.

Pour \bleu{1\le i\le n}, \bleu{Var(t_i) \cap
  \{x_1,...,x_n\}=\emptyset}, car \bleu{P} est résolu.

Il s'en suit que \bleu{`s(t_i) = t_i}, car en plus pour \bleu{y\notin
  \{x_1,...,x_n\}} \ali on a \bleu{`s(y)=y}.

Donc nous déduisons \bleu{`s(x_i) = t_i= `s(t_i)}, ce qui prouve que
\bleu{\sigma} est un unificateur de \bleu{P}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
\bleu{`s} \textcolor{vertfonce}{est minimal.}

Soit \bleu{`t} un unificateur.

On a \bleu{`t(x_i) = `t(t_i)} pour \bleu{1\le i\le n}.

Donc aussi \bleu{`t(x_i) = `t(`s(x_i))}.

Si \bleu{y\not\in\{x_1,...,x_n\}}, alors \bleu{\sigma(y)=y}
et \bleu{`t(y) = `t(\sigma(y))}.
  
Donc \bleu{`t = `t \sigma}, ce qui prouve que \bleu{\sigma} est un
unificateur minimal \ali (c'est-à-dire un mgu).

\bigskip

On notera qu'on aussi montré que \bleu{`s} est le seul mgu, puisqu'en
fait, tout unificateur est comparable à \bleu{`s} et plus «grand» que lui.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{Unification par transformation}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Transformations}

Chaque transformation est écrite comme une règle d'inférence

\bleu{\inferLabel{R}{P_{\mbox{avant}}}{P_{\mbox{après}}}}




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

\bleu{
\inferLabel{Supprime}{\{u\eq u\}\cup P}{P}}

\bleu{\inferLabel{Decompose}{\{f(u_1,...,u_n) \eq f(v_1,...,v_n)\}\cup
  P}{\{u_1 \eq v_1,...,u_n\eq v_n\}\cup P}}~ \brunir{$f\in \Sigma_n$}

\bleu{\inferLabel{Elimine}{\{x\eq v\}\cup P}{\{x\eq v\}\cup \sigma(P)}}
\ali où \bleu{x\eq v} n'est \verdir{pas en forme résolue} dans \bleu{\{x\eq
  v\}\cup P} %
\ali et \bleu{x\notin Var(v)} et \bleu{\sigma = \{x\mapsto v\}}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Succès et échec}

Si \bleu{P} est résolu, aucune règle ne s'applique \brunir{(succès)}.

Ça n'est pas le seul cas d'arrêt. Les autres cas sont des
\brunir{échecs}.
\begin{itemize}
\item S'il existe une équation de la forme \bleu{f(u_1,...,u_m) \eq
    g(v_1,...,v_n)} avec \bleu{f\not= g}, on dit qu'il y a \brunir{clash}.
\item S'il existe une équation de la forme \bleu{x \eq v} avec
  \bleu{v`:Var(`s)} \\ on dit qu'il y a un \brunir{cycle}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Résoudre par transformation}

Si \bleu{P'} est obtenu à partir de \bleu{P} par application de l'une
des règles, \\on écrit
\begin{bdp}
P\Mapsto P'
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Résoudre par transformation}
Si \bleu{P'} est obtenu à partir de \bleu{P} par application de l'une
des règles, \\on écrit
\begin{bdp}
P\Mapsto P'
\end{bdp}

Cette méthode à des liens avec l'élimination de Gauss.  

On simplifie par \emph{Supprime} et \emph{Decompose} et on élimine par
\emph{Elimine}.

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

Appliquer les règles à:
\begin{bdp}
\xymatrix{
& {*}\ar@{-}[ld]\ar@{-}[rd] &&&& {*}\ar@{-}[ld]\ar@{-}[rd]  &&\\
i\ar@{-}[d] && x & \eq & y && {*}\ar@{-}[ld]\ar@{-}[rd]  \\
x &&&&& z && u
}
\end{bdp}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{.95\textwidth}{\emph{Préservation des unificateurs}: Si \bleu{P\Mapsto P'} alors \bleu{\U(P)= \U(P')}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{.95\textwidth}{\emph{Préservation des unificateurs}: Si
      \bleu{P\Mapsto P'} alors \bleu{\U(P)= \U(P')}.}}


La seule difficulté est \emph{Elimine}.  

Posons \bleu{P = \{s_1\eq t_1, ..., s_n\eq t_n\}}.

Supposons
\bleu{{x\eq v\cup P}\Mapsto{x\eq v\cup \sigma(P)}}
\ali où \bleu{x\eq v} n'est pas en forme résolue et \bleu{x\notin Var(v)} 
\ali et \bleu{\sigma = \{x\mapsto v\}}.

Soit \bleu{`t} telle que  \bleu{Dom(`t) \cap Range(`t) =
  \emptyset}, alors \bleu{`t`t=`t}, %
\ali on dit que \bleu{`t} est \brunir{idempotente}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On voit que si les unificateurs idempotents sont préservés, %
\ali alors tous les unificateurs sont préservés~\footnote{En effet, un
  unificateur non idempotent est obtenu par renommage de variables à
  partir d'un unificateur idempotent.}.

Soit \bleu{`t} idempotente telle que \bleu{`t(x)=  `t(v)},
\begin{itemize}
\item alors \bleu{`t  = `t \sigma}, 
\item et dans le problème \bleu{P}, pour chaque \bleu{i} on a
  \bleu{`t(s_i) = `t \sigma(s_i) = `t \sigma(t_i) =
    `t(t_i)}.
\end{itemize}
Donc  \bleu{`t\in \U(x\eq v\cup P)} si et seulement si \bleu{`t\in \U(x\eq v\cup \sigma(P))}.

Par conséquent \bleu{\U(x\eq v\cup P) = \U(x\eq v\cup \sigma(P))}.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{9cm}{\emph{Correction :} Si \bleu{P\stackrel{*}{\Mapsto} P'} et
      \bleu{P'} est résolu alors \bleu{mgu(P) = \sigma_{P'}}.}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{9cm}{\emph{Correction :} Si \bleu{P\stackrel{*}{\Mapsto} P'} et
      \bleu{P'} est résolu alors \bleu{mgu(P) = \sigma_{P'}}.}}

On combine les deux lemmes précédents.

\bleu{\U(P) = \U(P')} donc \bleu{mgu(P) = mgu(P')}.

Or \bleu{mgu(P') = \sigma_{P'}}. \hfill \emph{c.q.f.d.}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8cm}{\emph{Complétude :} Si \bleu{P} est
      unifiable alors il existe \bleu{P'} tel que
      \begin{itemize}
      \item \bleu{P\stackrel{*}{\Mapsto} P'},
      \item \bleu{P'} est résolu.
      \end{itemize}
}}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{6cm}{\begin{footnotesize}\emph{Complétude :} Si
        \bleu{P} est unifiable alors il existe \bleu{P'} tel que
      \begin{itemize}
      \item \bleu{P\stackrel{*}{\Mapsto} P'},
      \item \bleu{P'} est résolu.
      \end{itemize}
    \end{footnotesize}
}}

\begin{small}
Soit \bleu{(P_i)} une suite telle que \bleu{P_0=P} et \bleu{P_i\Mapsto 
  P_{i+1}}.   
  
  On veut montrer qu'il existe \bleu{n} tel que \bleu{P_n} est résolu.
  
  Si \bleu{P_i} n'est pas résolu, alors
\begin{itemize}
\item si \bleu{P_i} ne contient pas de variable \bleu{x} non
  résolue, il contient une équation \bleu{s=t} décomposable, alors
  \emph{Decompose} s'applique.
\item si \bleu{P_i} contient une équation triviale \bleu{x\eq x} alors
  \emph{Supprime} s'applique.
\item si \bleu{P_i} contient une équation non résolue \bleu{x\eq t}
  avec \bleu{x\notin Var(t)}, alors \emph{Elimine} s'applique.
\end{itemize}
\vfill
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{6cm}{\begin{footnotesize}\emph{Complétude :} Si
        \bleu{P} est unifiable alors il existe \bleu{P'} tel que
      \begin{itemize}
      \item \bleu{P\stackrel{*}{\Mapsto} P'},
      \item \bleu{P'} est résolu.
      \end{itemize}
    \end{footnotesize}
}}

\begin{small}
Soit \bleu{(P_i)} une suite telle que \bleu{P_0=P} et \bleu{P_i\Mapsto 
  P_{i+1}}.   
  
  On veut montrer qu'il existe \bleu{n} tel que \bleu{P_n} est résolu.
  
  Si \bleu{P_i} n'est pas résolu, alors
\begin{itemize}
\item si \bleu{P_i} ne contient pas d'équation \bleu{x\eq v} non
  résolue, il contient une équation \bleu{s=t} décomposable, alors
  \emph{Decompose} s'applique.
\item si \bleu{P_i} contient une équation triviale \bleu{x\eq x} alors
  \emph{Supprime} s'applique.
\item si \bleu{P_i} contient une équation non résolue \bleu{x\eq t}
  avec \bleu{x\notin Var(t)}, alors \emph{Elimine} s'applique.
\end{itemize}
\vfill
Si \bleu{P_i} n'est pas résolu et est unifiable alors \emph{le
  processus peut continuer}.
\end{small}
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{footnotesize}
  \framebox{\parbox{6cm}{\emph{Complétude :} Si \bleu{P} est
      unifiable alors il existe \bleu{P'} tel que
      \begin{itemize}
      \item \bleu{P\stackrel{*}{\Mapsto} P'},
      \item \bleu{P'} est résolu.
      \end{itemize}
}}
\end{footnotesize}

Le processus s'arrête.

En effet, si l'on attache à chaque \bleu{P_i} le triplet
\bleu{(n_v,n_f,n_e)}  où
\begin{itemize}
\item \bleu{n_v} est le nombre de \emph{variables non résolues}, 
\item \bleu{n_f} est le nombre de \emph{symboles fonctionnels},
\item et \bleu{n_e} est le nombre d'\emph{équations}.
\end{itemize}
Chaque règle \emph{diminue} cette quantité suivant l'ordre
lexicographique.  

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
En effet, 

La règle \emph{Supprime} 

\begin{itemize}
\item diminue le nombre de variables non résolues \bleu{n_v} (cas où la
suppression de \bleu{x\eq x} rend la variable \bleu{x} résolue), 

\item ou si elle ne diminue pas le nombre de variables non résolues, \\ elle
diminue le nombre \bleu{n_f} de symboles fonctionnels (cas où
\bleu{u} contient au moins un symbole fonctionnel), 

\item sinon elle diminue le nombre d'équations \bleu{n_e}. 
\end{itemize}

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

La règle \emph{Decompose} 

\begin{itemize}
\item diminue le nombre de variables non résolues \bleu{n_v} (cas où l'un
des \bleu{u_i\eq v_i} est de la forme \bleu{x\eq t} et où \bleu{x} est résolue),

\item ou si elle ne diminue pas le nombre de variables non résolues, elle
diminue le nombre \bleu{n_f} de symboles fonctionnels.
\end{itemize}

\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
La règle \emph{Elimine} \begin{itemize}
\item diminue le nombre \bleu{n_v} de variables non
résolues.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \framebox{\parbox{8.5cm}{L'unification peut être exponentielle en la
      taille du problème originel.}}

\vfill
\newcommand{\F}{{*}\ar@{-}[dl]\ar@{-}[dr]}
\newcommand{\FF}{{*}\ar@{-}[dl]\ar@{.}[ddrr]}

\begin{scriptsize}
\xymatrix @C=3pt @R=8pt {
& \F &&&&&  &&&&&& {*}\ar@{-}[dll]\ar@{-}[drr] &&&&\\
x_1 && \F &&&&\eq&&&& \F&&&& \FF\\
& x_2 && {*}\ar@{-}[dl]\ar@{.}[ddrr] &&&&&& x_2 && x_2 &&\F &&\\
&&x_3&&&&&&&&&& x_3 && x_3 && \F\\
&&&&&\F&&&&&&&&&&\F&&a\\
&&&& {x_{n-1}} && x_n&&&&&&&& x_n && x_n}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  
  Par un succession de \emph{Decompose} on obtient la (\brunir{forme
    triangulaire})
\begin{scriptsize}
\bl{\begin{eqnarray*}
  x_1 & = & x_2 * x_2\\
&\vdots&\\
x_{n-1} & = & x_n * x_n\\
x_n & = & a
\end{eqnarray*}}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Puis par une succession de \emph{Elimine} 

\begin{scriptsize}
\bl{\begin{eqnarray*}
  x_1 & = & (...((a*a)*(a*a))... * ((a*a)*(a*a))...)\\
&\vdots&\\
x_{n-2} & = & (a*a) * (a*a)\\
x_{n-1} & = & (a*a)\\
x_n & = & a
\end{eqnarray*}}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Moralité}
Pour une bonne efficacité, il faut utiliser la règle \emph{Elimine} de
façon paresseuse.

Il faut préférer
\begin{itemize}
\item une forme triangulaire\\
  \begin{scriptsize}
    \bleu{
    \begin{array}[c]{rcl@{\qquad}l}
      x_1 &=& t(x_2,...,x_n) &\\
      & \vdots&\\
      x_{n-1} &=& t(x_n)&\\
      x_n &=& t_n&Var(t_n) = \emptyset
    \end{array}
  }
\end{scriptsize}
\item ou une représentation par pointeurs%
\ali qui ne sont que des manières «indirectes» \ali de
représenter les fonctions.
\end{itemize}
\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  MGU mgu Dom green Decompose Elimine Var dr ddrr pt dll drr rd ld
% LocalWords:  rd c.q.f.d unifiable
