%% Time-stamp: <modified on 22 Nov 2004 at 14:29 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}

%% 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 dans des théories}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\input{mes_couleurs}
\renewcommand{\verdir}[1]{{\color{vertfonce} #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{\calC}{\ensuremath{\cal C}}
\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{displaymathbleu}[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 @C 15pt {\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 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{\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]{%
{\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{cyan}{\shadowbox{#1}}%
%  \end{center}
%  \markright{#1}
%  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vertfonce}{\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{Compléments sur l'unification}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Ensemble complet d'unificateurs}
Il existe des théories pour lesquels les problèmes n'ont pas \emph{un}
unificateur plus général, mais \emph{plusieurs} (ou pas du tout!).

Un ensemble \bleu{S} de substitutions est un \emph{ensemble complet
d'unificateurs} d'un problème \bleu{P} si
\begin{enumerate}
\item \bleu{S\subseteq \U(P)},
\item \bleu{(\forall \tau \in \U(P))\ (\exists \sigma\in S)\
    (\exists\rho\in Sub(T(\Sigma,V))\ \tau = \rho\ \sigma}.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Combinaison d'algorithmes d'unification}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Hétérogénéité}
Soit \bleu{F = F_0 \uplus F_1}.

On suppose que l'on a deux théories 
\begin{itemize}
\item \bleu{E_0} sur \bleu{T(F_0,X)} 
\item et \bleu{E_1} sur \bleu{T(F_1,X)}.
\end{itemize}

Un terme \bleu{t\in T(F,X)} est \emph{pur} si \bleu{t\in T(F_0,X)\cup
  T(F_1,X)}.

Si \bleu{t} \verdir{n'est pas pur}, il est \emph{hétérogène}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Hétérogénéité (suite)}
Un sous-terme pur \bleu{t_{|p}} est \emph{maximal} \ali si
\bleu{(\forall q\in Pos(t))} \bleu{q \pref p} \quad
\emph{$\Rightarrow$} \quad «\bleu{t_{|q}} est hétérogène».

Une équation \bleu{s \eq t} est \emph{pure} 
\begin{itemize}
\item si \bleu{\{s,t\}\subseteq T(F_0,X)} 
\item ou \bleu{\{s,t\}\subseteq T(F_1,X)}
\end{itemize}
Une équation \bleu{s \eq t} est \emph{propre} si ni \bleu{s},  ni
\bleu{t} ne sont des variables.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriété des théories}
Une théorie est \emph{sans collapsus} si elle ne contient aucune
identité de la forme \bleu{x = t}.

Une théorie est \emph{régulière} si dans chaque identité \bleu{s = t}
chaque variable qui apparaît dans \bleu{s} apparaît dans \bleu{t} et
vice-versa.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Organisation d'un problème hétérogène}
Un problème d'unification hétérogène s'écrit 
\bl{\[P = P_0 \cup P_1 \cup P_V \cup P_H\]}
où  \bleu{P_0}  est formé des équations propres et pures dans \bleu{T(F_0,X)},

\bleu{P_1}  est formé des équations propres et pures dans \bleu{T(F_1,X)},

\bleu{P_V}  est formé des équations de la forme \bleu{x \eq y},

\bleu{P_H}  est formé des équations hétérogènes.

\vfill
Dans ce qui suit on travaille sur des problèmes \emph{en forme
  triangulaire}.

Donc on n'appelle pas \emph{Elimine}.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification dans des théories hétérogènes}
\begin{small}
\begin{math}
\begin{array}{llcl}
\emph{\mathbf{\mathsf{Abstract}}} & P \cup \{s\eq t\} & \Mapsto&
P\cup\{s[x]_{p} \eq t, x\eq s_{|p}\} \\ 
&&& \verdir{s_{|p} \mbox{est un sous-terme maximal pur de~} s.}\\
&&&\verdir{p\not= `e \textrm{~et~} x~\textrm{est une variable fraiche}}\\
\emph{\mathbf{\mathsf{Solve_0}}} & P \cup P_0 & \Mapsto&P \cup P_0' \\
&&& \verdir{P_0' \mbox{~est une forme résolue pure de~} P_0} \\
&&& \verdir{\mbox{~dans~} E_0.}\\
\emph{\mathbf{\mathsf{Solve_1}}} & P \cup P_1 & \Mapsto&P \cup P_1' \\
&&& \verdir{P_1' \mbox{~est une forme résolue pure de~} P_1} \\
&&& \verdir{\mbox{~dans~} E_1.}
\end{array}
\end{math}                                
\end{small}     
\vfill                           
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification dans des théories hétérogènes (suite)}
\begin{small}
\begin{math}
\begin{array}{llcl}
\emph{\mathbf{\mathsf{Coalesce}}} & P \cup \{x\eq y\} & \Mapsto&P\{x\mapsto y\}\cup\{x\eq y\}\\
&&& \verdir{ x\not= y}\\
\emph{\mathbf{\mathsf{Merge}}} & P \cup \{x\eq f(\vec{s}), x\eq g(\vec{t})\} & \Mapsto&P\{x\eq f(\vec{s}), f(\vec{s})\eq g(\vec{t})\}\\
&&& \verdir{ }\\\end{array}
\end{math}
\end{small}

\vfill                           
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Quelques explications}
Dans \emph{Abstract}, la variable \bleu{x} introduite est une variable
d'interface entre des sous termes qui appartiennent à deux théories
différentes.

\emph{Coalesce} «prend acte» que la frontière ou l'interface a
disparu.

\emph{Merge} est une forme de la règle \emph{Elimine}.

\emph{Solve$_0$} et \emph{Solve$_1$} font appel à la résolution dans
les théories \bleu{E_0} et \bleu{E_1} respectivement. %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Présolutions et solutions}
Une \emph{présolution} est un problème dont toutes les équations sont de la
forme \bleu{x\eq t}.

Une présolution est une \emph{solution} \ali si elle n'admet pas de cycle
de la forme \bl{\[x_1\eq s_1[x_2] \ldots x_{i}\eq s_i[x_{i+1}]\ldots
  x_{2n}\eq s_i[x_{1}]\]} où les symboles à la racine d'au moins deux
\bleu{s_i} et \bleu{s_j} sont dans des théories différentes.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Du problème aux solutions}
La relation \bleu{\Mapsto} est clairement indéterministe.

En particulier, elle a un branchement multiple pour \emph{$Solve_i$} qui
peut fournir plus qu'une solution ou pas du tout.

On suppose que \emph{$Solve_i$} fournit un ensemble complet
d'unificateurs.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{\emph{$Solve_i$}}
\emph{$Solve_i$} %
\begin{itemize}
\item[$\bullet$] transforme \bleu{P} en \bleu{Q} (soit \bleu{P\Mapsto Q})%
\item[$\bullet$] et prend une équation dans \bleu{P_i} et retourne (de façon
  indéterministe mais complète)
\begin{itemize}
\item des équations de la forme \bleu{x_j\eq s_j} dans \bleu{P_i}
\item et des équations de la forme \bleu{y_k\eq y_l} \ali que l'on va
  mettre dans \bleu{P_V},
\item une transition existe pour chaque unificateur de l'ensemble
  complet, 
\end{itemize}
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les échecs}
L'algorithme échoue dans trois cas, c'est-à-dire  qu'on est en présence
d'un problème équationnel pour lequel aucune transition n'existe et
pourtant le problème n'est pas lui-même une solution.
\begin{small}
\begin{enumerate}
\item Seule une transition \emph{$Solve_i$} est applicable,
  mais elle ne retourne aucun unificateur,
\item Aucune transition n'est applicable, mais il reste une équation
  de la forme \bleu{s\eq t} avec ni \bleu{s}, ni \bleu{t} qui ne soit
  une variable.  Cela signifie que \bleu{s} et \bleu{t} sont des
  termes purs dans deux théories différentes.
\item Le problème est une présolution qui n'est pas une solution
  (présence d'un cycle).
\end{enumerate}
\end{small}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Du problème aux solutions}

\fbox{\parbox{8cm}{
Si \bleu{E_0} et \bleu{E_1} sont des théories \emph{régulières} et
\emph{sans collapsus}
\ali alors l'ensemble \bleu{\{Q \mbox{~\emph{solution}}~|~ P\stackrel{*}{\Mapsto} Q\}}
\ali forme un ensemble complet d'unificateurs pour \bleu{P}.
}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{L'unification associative et
          commutative restreinte}}}
\end{center}
\end{slide}
<%------------------------------------------------------
\begin{slide}
\heading{L'unification associative et commutative générale}
Dans le cas de l'unification \emph{associative et commutative générale}, seuls
certains opérateurs sont \emph{AC} (c'est-à-dire associatifs et
commutatifs\footnote{et pas \emph{automate cellulaire} comme le croient
certains.}).

Il faudra donc \verdir{combiner} des algorithmes d'unification où seul un
opérateur est AC. 

Si \bleu{+} est un opérateur associatif et commutatif, la
résolution d'équations dans la théorie \bleu{T(\{+\},X)} s'appelle
\emph{l'unification AC restreinte}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La représentation des termes}
A priori un terme associatif et commutatif dans la théorie
\bleu{T(\{+\},X)} est un arbre  dont les
noeuds internes sont des \bleu{+} et les feuilles des variables.

\emph{Par exemple} \bleu{(x_1 + x_2) + (x_3 + (x_3 + x_1))}, se
représente mieux par \bleu{x_1 + x_1 + x_2 + x_3 + x_3} ou par l'arbre
\begin{center}
\bl{
\xymatrix{
&& +\ar@{-}[drr]\ar@{-}[dr]\ar@{-}[dl]\ar@{-}[dll]\ar@{-}[d]&&\\
x_1 & x_1 & x_2 & x_3  & x_3
}}
\end{center}

ou par le terme \bleu{2x_1 + x_2 + 2x_3}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La représentation des termes et des équations}
Plus généralement un \emph{terme} \bleu{s} non réduit à une varibale
est représenté par %
\bl{\[s = \sum_{i=1}^n s_i x_i\]}%
avec 
\bl{\[\sum_{i=1}^n s_i \ge 2\]}%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La représentation des termes et des équations}
\begin{itemize}
\item Un terme réduit à une variable correspond au cas où
  \bl{\[\sum_{i=1}^n s_i =1 \]}%


\item Le cas \bl{\[\sum_{i=1}^n s_i = 0 \]}%
  ne correspond à aucun terme AC.\\
  Il doit éliminer absolument.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La représentation des termes et des équations}
Une \emph{équation} est représentée par
\bl{\[\sum_{i=1}^n s_i x_i \eq \sum_{i=1}^n t_i x_i \quad \quad (eq)\]}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La représentation des substitutions}
Clairement une substitution \bleu{\sigma} idempotente applique à chaque
variable \bleu{x_i} un terme AC \bleu{a_i} tel que \bleu{\{x_1,\ldots,
  x_n\} \cap Var(a_i)= \emptyset} donc
%
\bl{\[\sigma(x_i) = \sum_{j=1}^q a_{ij} y_j\]}
%
où \bleu{a_{ij}\in\Nat}, \bleu{x_i\notin \{y_1,\ldots,y_q\}} et la
condition (que l'on appelle \calC) est satisfaite : \bl{\[\sum_{j=1}^q
  a_{ij} \ge 1\qquad \qquad (\calC)\]}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (1/4)}
%
\bleu{\{..., x_i "|->" \sum_{j=1}^q a_{ij} y_j,...\}} est un
unificateur idempotent de \bleu{s\eq t} dans le problème \bleu{P} si %
\bl{\[\sum_{i=1}^n s_i \sum_{j=1}^q a_{ij} y_j = \sum_{i=1}^n t_i
  \sum_{j=1}^q a_{ij} y_j\]}

où \bleu{\{y_1,\ldots, y_q\} \cap Var(P)= \emptyset} 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (1/4)}
%
\bleu{\{..., x_i "|->" \sum_{j=1}^q a_{ij} y_j,...\}} est un
unificateur idempotent de \bleu{s\eq t} dans le problème \bleu{P} si %
\bl{\[\sum_{i=1}^n s_i \sum_{j=1}^q a_{ij} y_j = \sum_{i=1}^n t_i
  \sum_{j=1}^q a_{ij} y_j\]}
où \bleu{\{y_1,\ldots, y_q\} \cap Var(P)= \emptyset} 

Soit encore 
\bl{\[\sum_{j=1}^q y_j \sum_{i=1}^n s_i  a_{ij} = \sum_{j=1}^q y_j
  \sum_{i=1}^n t_i  a_{ij} \]}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (2/4)}
Clairement \bleu{\{..., x_i "|->" a_{ij}, ...\}} est une solution de
$(eq)$, car 
\bl{\[\sum_{i=1}^n s_i  a_{ij} = \sum_{i=1}^n t_i  a_{ij}.
  \]} %
Elle engendre l'ensemble des solutions  de $(eq)$.

\bigskip

\bleu{\{..., x_i "|->" a_{ij}, ...\}} est un unificateur si
\bl{\[\sum_{j=1}^q a_{ij} \ge 1 \]}%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (2/4)}
Donc si \bleu{(a_{1j} \ldots, a_{ij}, \ldots, a_{nj})} (pour un
\bleu{j} fixé) est  une solution génératrice de l'\emph{équation
diophantienne}
\begin{itemize}
\item \emph{linéaire} (tous les monômes de degré 1),
\item \emph{homogène} (pas de termes constants),
\end{itemize}
\bl{\[\sum_{i=1}^n s_i x_{i} \eq \sum_{i=1}^n t_i x_{i} \]}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (2/4)}
Donc si \bleu{(a_{1j} \ldots, a_{ij}, \ldots, a_{nj})} (pour un
\bleu{j} fixé) est  une solution génératrice de l'\emph{équation
diophantienne}
\begin{itemize}
\item \emph{linéaire} (tous les monômes de degré 1),
\item \emph{homogène} (pas de termes constants),
\end{itemize}
\bl{\[\sum_{i=1}^n s_i x_{i} \eq \sum_{i=1}^n t_i x_{i} \]}.  

La solution générale est une combinaison $\Nat$-linéaire des ces solutions.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'unification AC restreinte (3/4)}
  \fbox{\parbox{9cm}{Étant donné un problème d'unification \bleu{P},
      l'ensemble des solutions du système d'équations diophantiennes
      associé qui satisfont la condition \calC{} est l'ensemble des
      unificateurs de \bleu{P}.  }}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'unification AC restreinte (3/4)}
    \fbox{\parbox{9cm}{Étant donné un problème d'unification \bleu{P},
      l'ensemble des solutions du système d'équations diophantiennes
      associé qui satisfont la condition \calC{} est l'ensemble des
      unificateurs de \bleu{P}.  }}

\vfill

Reste à trouver un ensemble fini de générateurs de l'ensemble des
solutions qui satisfont \calC \ali pour avoir un \emph{ensemble complet
et fini d'unificateurs} de \bleu{P}.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'unification AC restreinte
    (4/4)} 
Pour cela on cherche d'abord un ensemble de générateurs
  des solutions du système dans \bleu{\Nat}.
 
 Ensuite on s'en sert pour engendrer un générateur des solutions qui
 satisfont \calC.

\vfill
 \end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{L'unification en lambda calcul\\
ou\\
unification d'ordre supérieur}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Objectif}
On peut vouloir résoudre des équations comme
\bl{\[\lambda x. sin (cos (x)) \eq \lambda x. sin (F (x)) \]}
qui a pour solution \bleu{\lambda y . cos (y)}. 

Alors que
\bl{\[\lambda x. F  \eq \lambda x. sin (cos (x)) \]}
n'a pas de solution.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemple} 
Plus généralement, on va résoudre des équations du type

\bl{\[\lambda x. F (\lambda y. x y a) \eq \lambda z . z (z a a) \]}

où \bleu{a: \tau} \qquad et \qquad  \bleu{\vdash \lambda z . z (z a a) :
  \emph{\LARGE ?}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Exemple} 
Plus généralement, on va résoudre des équations du type

\bl{\[\lambda x. F (\lambda y. x y a) \eq \lambda z . z (z a a) \]}

où \bleu{a: \tau} \qquad et  \qquad \bleu{\vdash \lambda z . z (z a a) : (\tau \rightarrow \tau \rightarrow \tau)
  \rightarrow \tau \rightarrow \tau.}

\bleu{F} est une \emph{inconnue à instancier}.

Quel est son type?

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le problème}
  Les termes que l'on cherche à unifier
  \begin{itemize}
  \item sont \emph{simplement typés}, 
  \item ils ne contiennent que des \emph{variables liées} que nous appellerons
    \verdir{variables} notées \bleu{x, x', x_1, x_2, ..., y, y', y_1,
      ..., z, ...}
  \item ils contiennent des \emph{inconnues} que nous cherchons à
    «résoudre» et que nous noterons
    \bleu{F, G, H} (l'ensemble de inconnues de \bleu{t} est noté
    \bleu{INC(t)}),
  \item ils peuvent contenir des \emph{constantes} notées \bleu{g, h,
      k, c ...}
  \item  et l'on travaille \emph{modulo} \bleu{\beta} \emph{et}
    \bleu{\eta}.  
\end{itemize}
On considère donc la forme $\beta$-normale de chaque terme.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le problème}
Les constituants atomiques d'un terme sont 
\begin{itemize}
\item soit des constantes,
\item soit des variables (liées),
\item soit des inconnues. 
\end{itemize}

  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le problème}
On va présenter une algorithme d'unification dû à Huet revisité par
Snyder pour une présentation en règles.

\begin{itemize}
\item Gérard Huet. \emph{A unification algorithm for typed $`l$-calculus}.
  Theoretical Computer Science, Vol.1, pp 27--57, 1975.
  
\item Wayne Snyder, \emph{A proof theory for general unification},
  Birkh\"auser, (1991), Vol. 11, Progress in computer science and
  applied logic,

\item Christian Prehofer,  \emph{Solving Higher-Order Equations: From
    Logic to Programming}, Birkhäuser PTCS Series, 1997.   
\end{itemize}
                                %
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $`b$-normale}
Une forme $`b$-normale est un terme de la forme
\begin{displaymathbleu}
  `l x_1 ... x_n . v M_1 ..M_p
\end{displaymathbleu}
\begin{itemize}
\item où \bleu{v} est soit l'une des variables $x_i$, soit une
  constante, soit une inconnue,
\item où chacun des \bleu{M_j} est une forme normale.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $`b$-normale}

  En effet tous les sous-termes d'une forme normale sont en forme
  normale.
  
  Les membres gauches d'une application ne peuvent pas être des
  abstractions donc ce sont
  
  \qquad soit des applications,
  
  \qquad soit des variables ou des constantes ou des inconnuees.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Rigidité et flexibilité} %
Si un terme est de forme  \bleu{\lambda \overrightarrow{x_k} .
    v(\overrightarrow{t_m'})} \ali où \bleu{v} est soit une variable ou une
  constante, \\le terme est dit \emph{rigide}.

\vspace*{20pt} 

Si un terme est de forme \bleu{\lambda \overrightarrow{x_k} .
  v(\overrightarrow{t_m'})} \ali où \bleu{v} est une inconnue
\\le terme est dit \emph{flexible}.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $\beta\eta$ longue}
D'autre part, on veut que si~\bl{\(\vdash M:\sigma_1 \rightarrow \ldots
  \rightarrow \sigma_n \rightarrow \tau\)} %
\ali alors le terme étudié soit
de la forme \bl{\[\lambda x_1\ldots x_n. N\]}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $\beta\eta$ longue} 
Si toutes les variables ne sont pas présentes il faut faire une ou
plusieurs \bleu{\eta}-expansions.

\verdir{En résumé} pour obtenir la \emph{forme $\beta\eta$ longue} d'un
terme \bl{\[\vdash M:\sigma_1 \rightarrow \ldots \rightarrow \sigma_n
  \rightarrow \tau\]} On calcule la forme $\beta$-normale
\bleu{\lambda x_1\ldots x_k. N}.

Clairement, \bleu{k\le n} et la forme $\beta\eta$ longue est 

\bl{\[\lambda x_1\ldots x_k x_{k+1}\ldots x_n. N x_{k+1}\ldots x_n\]}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $\beta\eta$ longue} 
La forme $\beta\eta$-longue du terme 
\bl{\[\lambda x. F (\lambda y. x y a) \eq \lambda z . z (z a a) \]}

est

\begin{center}
  {\Large \bl{?}}
\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme $\beta\eta$ longue} 
La forme $\beta\eta$-longue du terme 
\bl{\[\lambda x. F (\lambda y. x y a) \eq \lambda z . z (z a a) \]}

est
\bl{\[\lambda x_1 x_2. F (\lambda y. x_1 y a) x_2 \eq \lambda x_1 x_2 . x_1 (x_1 a a) x_2\]}


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Notations} 
On écrit \bleu{v(\vec{t_n})} pour \bleu{v~t_1 \ldots t_n} 

où \bleu{v = F}, \bleu{v = x} ou \bleu{v = f}, c'est-à-dire \bleu{v}
une inconnue ou une variable liée ou une constante.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Trois règles de transformation de problèmes de base}
\end{slide} 
%------------------------------------------------------
\begin{slide}
\bl{
\begin{footnotesize}
\begin{math}
\begin{array}{lcl}
\emph{Supprime} \\ {\{u\eq u\}\;\verdir{\cup}\; P} & \Mapsto & {P}\\[6pt]%
%-----------------------------
\emph{Decompose} \\ \{\lambda \overrightarrow{x_k}. v(\overrightarrow{t_m})
\eq \lambda \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P &
%
\Mapsto & 
%
%\bigcup_{i=1}^m%
\raisebox{-5pt}{\mbox{$\stackrel{\scriptsize m}{\stackrel{\bigcup}{\scriptsize i=1}}$}}%
\{\lambda \overrightarrow{x_k}. t_i)
\eq \lambda \overrightarrow{x_k}. t_i'\} \;\;\verdir{\cup}\;\; P\\[6pt]%
% ----------------------------
\emph{Elimine} \\ \{F \eq t\} \;\verdir{\cup}\; P & 
%
\Mapsto &
%
\theta P \qquad \mbox{\verdir{si~}} \theta = \{F \mapsto t\} \mbox{\verdir{~et~}} F\notin INC(t)
\end{array}
\end{math}
\end{footnotesize}}

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \subheading{Les règles d'imitation et de projection}
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide}} 
    Si l'équation est de la forme \bleu{\lambda \overrightarrow{x_k} .
    F(\overrightarrow{t_n}) \eq \lambda \overrightarrow{x_k} .
    v(\overrightarrow{t_m'})} \ali où \bleu{v} n'est pas une inconnue,

on appelle cela un cas \emph{flexible-rigide}.

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide}: projection} 
    Si l'équation est de la forme \bleu{\lambda \overrightarrow{x_k} .
    F(\overrightarrow{t_n}) \eq \lambda \overrightarrow{x_k} .
    v(\overrightarrow{t_m'})} \ali où \bleu{v} n'est pas une inconnue.
  
  On peut faire l'hypothèse que \bleu{v} est le \emph{symbole de tête
    de l'un des} \bleu{t_i} et que l'affectation que l'on fait à
  \bleu{F} vise à «atteindre» ce terme, pour créer une meilleure
  ressemblance.

\vfill
On appelle cette règle \emph{projection}.
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide}: projection} 
\begin{footnotesize}
Alors posons \emph{$`q := F \mapsto `l \overrightarrow{y_n} .
  y_i (\overrightarrow{H_q(\overrightarrow{y_n})})$}.
\bl{
\[\{`l \overrightarrow{x_k} .
  F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k} .
  v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P\]
\[\xymatrix{\ar@{|=>}[r]&}\]
\[\{`l
  \overrightarrow{x_k} .  `q(F(\overrightarrow{t_n})) \eq `l
  \overrightarrow{x_k} .  `q(v(\overrightarrow{t_m'}))\} \;\verdir{\cup}\;
  `q P\]}
Puisque \emph{$`q(F(\overrightarrow{t_n})) \rabeta `q (t_i(\overrightarrow{H_q(\overrightarrow{t_n})}))
  `=(`q t_i)(\overrightarrow{H_q(\overrightarrow{`q t_n})})$}
\bl{
\[\{`l \overrightarrow{x_k} .  F(\overrightarrow{t_n}) \eq
  `l \overrightarrow{x_k} .  v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P\]
\[\xymatrix{\ar@{|=>}[r]&}\]
\[\{`l \overrightarrow{x_k} .  `q t_i
  (\overrightarrow{H_q(\overrightarrow{`q t_n})}) \eq `l
  \overrightarrow{x_k} .  v(\overrightarrow{`q t_m'})\} \;\verdir{\cup}\;
  `q P\]}
\end{footnotesize}
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : projection, exercice 1 } 
Soit l'équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}
\vfill
\end{slide} 
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : projection, exercice 1 } 
Soit l'équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}

On a \bleu{g : \iota \rightarrow \iota \rightarrow \iota} et
\bleu{F : \iota \rightarrow \iota} où \bleu{\iota} est un type de base.

\bleu{k=2}, \bleu{n=1}, \bleu{i=1}, \bleu{m=2}, \bleu{q=0}

\emph{$F\mapsto `l y_1. y_1$}.

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : projection, exercice 1 } 
Soit l'équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}

\bleu{k=2}, \bleu{n=1},  \bleu{i=1}, \bleu{m=2}, \bleu{q=0} 

plus précisément \quad \bleu{`l x_1
  x_2. v(x_1~x_2)=`l x_1 x_2. g~x_1~x_2}

et \qquad \qquad\qquad \qquad \bleu{t_1= g~x_1~x_2}

\emph{$F\mapsto `l y_1. y_1$}.

\vfill
\centerline{\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Projette}&}}}

\centerline{\bleu{`l x_1 x_2 . g~x_1~x_2 \eq
    `l x_1 x_2 . g~x_1~x_2}}
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation (1/3)} 
  Si l'équation est de la forme \bleu{`l \overrightarrow{x_k} .
    F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k} .
    v(\overrightarrow{t_m'})} \ali où \bleu{v} n'est pas une inconnue.
  
  On peut faire l'hypothèse que \bleu{v} est précisément le symbole par
  lequel on souhaite que \bleu{F} commence. 
  
  Dans ce cas, \bleu{v} n'est pas une variable liée.

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation (2/3)} 
Alors posons \emph{$\theta := F \mapsto `l \overrightarrow{y_n} .
  v (\overrightarrow{H_q(\overrightarrow{y_n})})$}.

\bl{\[`l \overrightarrow{x_k} .
  F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k}
  v(\overrightarrow{t_m'}) \;\verdir{\cup}\; P\] %
\[\xymatrix{\ar@{|=>}[r]&}\]
\[\{`l \overrightarrow{x_k} .
  \theta(F(\overrightarrow{t_n})) \eq `l \overrightarrow{x_k}
  \theta (v(\overrightarrow{t_m'}))
  \} \;\verdir{\cup}\; \theta P\]}


\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation, exercice 2 } 
Soit la même équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1 x_2}

\emph{$F\mapsto `l y_1 .g (H_1~y_1) (H_2~y_1)$}.

\centerline{\bleu{`l x_1 x_2 . F(g~x_1 x_2) \eq `l x_1 x_2 . g~x_1~x_2}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Imite}&}}}

\centerline{\bleu{`l x_1 x_2 . g~(H_1~(g~x_1~x_2)) (H_2~(g~x_1~x_2))\eq
    `l x_1 x_2 . g~x_1~x_2}}
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation, exercice 2 } 
Soit la même équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}

\emph{$F\mapsto `l y_1 y_2 .g (H_1~y_1) (H_2~y_1)$}.

\centerline{\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 . g~x_1~x_2}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Imite}&}}}

\centerline{\bleu{`l x_1 x_2 . g~(H_1~(g~x_1~x_2)) (H_2~(g~x_1~x_2))\eq
    `l x_1 x_2 . g~x_1~x_2}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Decompose}&}}}


\centerline{\bleu{\{`l x_1 x_2 . H_1~(g~x_1~x_2)\eq `l x_1 x_2 .
    x_1, `l x_1 x_2 . H_2~(g~x_1~x_2)\eq `l x_1 x_2 . x_2\}}}

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation, exercice 2 } 
On ne peut pas appliquer \emph{Projette} sur 
  \begin{displaymathbleu}
    `l x_1 x_2 . H_1~(g~x_1~x_2) \eq `l x_1 x_2.  x_1
\end{displaymathbleu}
mais par \emph{Imite}, elle donne \emph{$H_1"|->" `l z_1 z_2 . x_1$}
\begin{displaymathbleu}
  `l x_1 x_2 . x_1 \eq `l x_1 x_2.  x_1
\end{displaymathbleu}
Par symétrie on voit que cette branche conduit à la solution
\emph{$F\mapsto `l y_1 y_2 .g (H_1~y_1) (H_2~y_1), \ali H_1"|->"
  `l z_1 z_2 . x_1, \quad H_2"|->" `l z_1 z_2 . x_2$.}

Donc \emph{$F\mapsto `l y_1 y_2 .g x_1 x_2$}.

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
\heading{Pour résumer}
  L'équation 
  \begin{displaymathbleu}
    `l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 .  g~x_1~x_2
  \end{displaymathbleu}
a donc deux solutions %

  \begin{center}
    \emph{$F\mapsto `l y_1. y_1$}
\end{center}
et 

\begin{center}
  \emph{$F\mapsto `l y_1 y_2 .g x_1 x_2$}.
\end{center}
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation, exercice 3 } 
Soit l'équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 .
  g~(g~x_1~x_2)~(g~x_1~x_2)}

\emph{$F\mapsto `l y_1 y_2 .g (H_1~y_1) (H_2~y_1)$}.

\centerline{\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 .
  g~(g~x_1~x_2)~(g(~x_1~x_2)}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Imite}&}}}

\centerline{\bleu{`l x_1 x_2 . g~(H_1~(g~x_1~x_2)) (H_2~(g~x_1~x_2))\eq
    `l x_1 x_2 . g~(g~x_1~x_2)~(g(~x_1~x_2)}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Decompose}&}}}


\centerline{\bleu{\{`l x_1 x_2 . H_1~(g~x_1~x_2)\eq `l x_1
    x_2 .  g~x_1~x_2, `l x_1 x_2 . H_2~(g~x_1~x_2)\eq `l x_1
    x_2 . g~x_1~x_2\}}}

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation, exercice 3 } 
Soit donc 

\centerline{\bleu{\{`l x_1 x_2 . H_1~(g~x_1~x_2)\eq `l x_1
    x_2 .  g~x_1~x_2, `l x_1 x_2 . H_2~(g~x_1~x_2)\eq `l x_1
    x_2 . g~x_1~x_2\}}}
  
  Par projection, sur le modèle de l'exercice précédent, en prenant
  \emph{$H_1\mapsto`l y.y$} et \emph{$H_2\mapsto`l y.y$}, on
  trouve


\centerline{\bleu{\{`l x_1 x_2 . H_1~(g~x_1~x_2)\eq `l x_1
    x_2 .  g~x_1~x_2, `l x_1 x_2 . H_2~(g~x_1~x_2)\eq `l x_1
    x_2 . g~x_1~x_2\}}}

\centerline{\bleu{\xymatrix @C 40pt {\ar@{|=>}[r]^{2, Projette}&}}}

\centerline{\bleu{\{`l x_1 x_2 . (g~x_1~x_2)\eq `l x_1
    x_2 .  g~x_1~x_2, `l x_1 x_2 . (g~x_1~x_2)\eq `l x_1
    x_2 . g~x_1~x_2\}}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \subheading{Le système \emph{PT0} de transformation de problèmes}
\end{slide} 
%------------------------------------------------------
\begin{slide}
\bl{
\begin{footnotesize}
\begin{math}
\begin{array}{lcl}
\emph{Supprime} \\ {\{u\eq u\}\;\verdir{\cup}\; P} & \Mapsto & {P}\\%
%-----------------------------
\emph{Decompose} \\ \{`l \overrightarrow{x_k}. v(\overrightarrow{t_m})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P &
%
\Mapsto & 
%
\bigcup_{i=1}^m\{`l \overrightarrow{x_k}. \overrightarrow{t_i})
\eq `l \overrightarrow{x_k}. \overrightarrow{t_i'}\} \;\verdir{\cup}\; P\\%
% ----------------------------
\emph{Elimine} \\ \{F \eq t\} \;\verdir{\cup}\; P & 
%
\Mapsto &
%
\theta P \qquad \mbox{\verdir{si~}} \theta = \{F \mapsto t\} \mbox{\verdir{~et~}} F\notin INC(t)\\
% ----------------------------
\emph{Projette} \\  \{`l \overrightarrow{x_k}. F(\overrightarrow{t_n})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P &
%
\Mapsto &
%
\{`l \overrightarrow{x_k}. \theta (F(\overrightarrow{t_n}))
\eq `l \overrightarrow{x_k}. \theta (v(\overrightarrow{t_m'}))\}  \;\verdir{\cup}\; \theta P
\\
&&\mbox{\verdir{où~}} \theta = \{F \mapsto `l \overrightarrow{y_n} .
  y_i (\overrightarrow{H_q(\overrightarrow{y_n})})\} \\
% ---------------------------
\emph{Imite} \\  \{`l \overrightarrow{x_k}. F(\overrightarrow{t_n})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P & 
%
\Mapsto &
%
\{`l \overrightarrow{x_k}. \theta (F(\overrightarrow{t_n}))
\eq `l \overrightarrow{x_k}. \theta (v(\overrightarrow{t_m'}))\}
 \;\verdir{\cup}\; \theta P \\
&& \mbox{\verdir{où~}} \theta := \{F \mapsto `l \overrightarrow{y_n} .
  v (\overrightarrow{H_m(\overrightarrow{y_n})})\}
\end{array}
\end{math}
\end{footnotesize}
}

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \subheading{Le système \emph{PT1} de transformation de problèmes}
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-rigide} : imitation (3/3)} 
\begin{footnotesize}
Soit \emph{$\theta := F \mapsto `l \overrightarrow{y_n} .
  v (\overrightarrow{H_m(\overrightarrow{y_n})})$}.

\centerline{\bleu{`l \overrightarrow{x_k} .
  F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k}
  v(\overrightarrow{t_m'}) \;\verdir{\cup}\; P}} %

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Imite-PT0}&}}}

\centerline{\bleu{
`l \overrightarrow{x_k} .
  \theta(F(\overrightarrow{t_n})) \eq `l \overrightarrow{x_k}
  \theta (v(\overrightarrow{t_m'}))
  \} \;\verdir{\cup}\; \theta P
}}

\centerline{\bleu{\xymatrix{\ar@{|=>}[r]^{Decompose}&}}}

\begin{center}
\bleu{
\{`l \overrightarrow{x_k} .
  H_1(\overrightarrow{\theta t_n}) \eq `l
  \overrightarrow{x_k} .  \overrightarrow{\theta t_1'}, %
   \ldots, %  
`l \overrightarrow{x_k} .
  {H_m(\overrightarrow{\theta t_n})} \eq `l
  \overrightarrow{x_k} .  \overrightarrow{\theta t_m'}\} \;\verdir{\cup}\; \theta
  P}
\end{center}
donc \bl{
\[`l \overrightarrow{x_k} .
  F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k}
  v(\overrightarrow{t_m'}) \;\verdir{\cup}\; P\] %
\[\xymatrix{\ar@{|=>}[r]^{Imite-PT1}&}\]
\[\{`l \overrightarrow{x_k} .
  H_1(\overrightarrow{\theta t_n}) \eq `l
  \overrightarrow{x_k} .  \overrightarrow{\theta t_1'}, %
   \ldots, %  
`l \overrightarrow{x_k} .
  {H_m(\overrightarrow{\theta t_n})} \eq `l
  \overrightarrow{x_k} .  \overrightarrow{\theta t_m'}\} \;\verdir{\cup}\; \theta
  P\]}
\vfill
\end{footnotesize}
\end{slide} 
%------------------------------------------------------
\begin{slide}
\bl{
\begin{footnotesize}
\begin{math}
\begin{array}{lcl}
\emph{Supprime} \\ {\{u\eq u\}\;\verdir{\cup}\; P} & \Mapsto & {P}\\%
%-----------------------------
\emph{Decompose} \\ \{`l \overrightarrow{x_k}. v(\overrightarrow{t_m})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P &
%
\Mapsto & 
%
\bigcup_{i=1}^m\{`l \overrightarrow{x_k}. \overrightarrow{t_i})
\eq `l \overrightarrow{x_k}. \overrightarrow{t_i'}\} \;\verdir{\cup}\; P\\%
% ----------------------------
\emph{Elimine} \\ \{F \eq t\} \;\verdir{\cup}\; P & 
%
\Mapsto &
%
\theta P \qquad \mbox{\verdir{si~}} \theta = \{F \mapsto t\} \mbox{\verdir{~et~}} F\notin INC(t)\\
% ----------------------------
\emph{Projette} \\  \{`l \overrightarrow{x_k}. F(\overrightarrow{t_n})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P &
%
\Mapsto &
%
\{`l
  \overrightarrow{x_k} .  \theta t_i
  (\overrightarrow{H_q(\overrightarrow{\theta t_n})}) \eq `l
  \overrightarrow{x_k} .  v(\overrightarrow{\theta t_m'})\} \;\verdir{\cup}\; \theta P
\\
&&\mbox{\verdir{où~}} \theta = \{F \mapsto `l \overrightarrow{y_n} .
  y_i (\overrightarrow{H_q(\overrightarrow{y_n})})\} \\
% ---------------------------
\emph{Imite} \\  \{`l \overrightarrow{x_k}. F(\overrightarrow{t_n})
\eq `l \overrightarrow{x_k}. v(\overrightarrow{t_m'})\} \;\verdir{\cup}\; P & 
%
\Mapsto &
%
\bigcup_{i=1}^m \{`l \overrightarrow{x_k} .
  H_i(\overrightarrow{\theta t_n}) \eq `l
  \overrightarrow{x_k} .  \overrightarrow{\theta t_i'}\} \;\verdir{\cup}\; \theta
  P \\
&& \mbox{\verdir{où~}} \theta := \{F \mapsto `l \overrightarrow{y_n} .
  v (\overrightarrow{H_m(\overrightarrow{y_n})})\}
\end{array}
\end{math}
\end{footnotesize}
}

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-flexible}} 
Les équations de la forme \bleu{`l \overrightarrow{x_k} .
    F(\overrightarrow{t_n}) \eq `l \overrightarrow{x_k} .
    G(\overrightarrow{t_m'})} sont dites \emph{flexibles-flexibles}.

On montre
\begin{enumerate}
  
\item qu'elles ont toujours au moins une solution,
\item qu'elles ont une infinité de solutions sans pourtant posséder un
  ensemble complet fini d'unificateurs.
\end{enumerate}

\emph{PT1} est une procédure de \emph{préunification}.

\bleu{\sigma} est un \emph{préunificateur} de \bleu{P} si \bleu{\sigma
  P} produit par \emph{Supprime}, \emph{Decompose}, \emph{Elimine}
un ensemble d'équations flexibles-flexibles.
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Forme \textit{flexible-flexible: exercice 4}} 
Soit l'équation:

\bleu{`l x_1 x_2 . F(g~x_1~x_2) \eq `l x_1 x_2 .
  g~(G~x_1~x_2)~(G~x_2~x_1)}

Montrer que l'on aboutit à des équations flexibles-flexibles et qu'une
solution possible est \bleu{F\mapsto `l y. y} et \bleu{G\mapsto
  `l y_1 y_2. y_1}.

Trouver une autre solution pour \bleu{G}.

\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
\heading{Cohérence}
Si \bleu{P \Mapsto P'} et si \bleu{\theta} est un préunificateur de
  \bleu{P'} alors \bleu{\theta} est un préunificateur de
  \bleu{P}.
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
\heading{Complétude}
Si \bleu{P} a une solution \bleu{`q}
 alors il existe un \bleu{P'} tel que 
 \begin{itemize}
 \item \bleu{P \Mapsto P'} en accumulant la substitution \bleu{`s} au
   cours de \emph{Elimine},
 \item \bleu{P'} est un ensemble d'équations  flexibles-flexibles
   ayant entre autres comme solution~\bleu{`r} 
 \item et \bleu{`q = `r `s}.
\end{itemize}
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Indécidabilité}%
\emph{Golfarb (1981):}

  \fbox{\parbox{7.8cm}{Le problème de l'unification du second ordre est
      indécidable. }} %

\vspace*{12pt}

La preuve se fait par réduction au 10$^\textrm{ème}$ problème de Hilbert.
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Les motifs ou patterns} Un terme simplement typé en
  $\beta\eta$-forme normale longue est un \emph{motif} ou un
  \emph{pattern} 
  \begin{enumerate}
  \item \emph{si toutes les occurrences de ses inconnues ont
      seulement des variables liées en paramètre}
  \item \emph{si toutes ces variables liées sont différentes les unes
      des autres.}
\end{enumerate}
\vspace*{30pt}

\bleu{`l x y . f(F(y,x))} et \bleu{`l x y . g(F(y,x), G(y))}
sont des motifs.

\bleu{`l x y . F(f(y), x)} et \bleu{`l x y . f(F(x, x)} ne
sont pas des motifs.  
\vfill
\end{slide} 
%------------------------------------------------------
\begin{slide}
  \heading{Unification des motifs ou patterns} Si un \bleu{P = s\eq t}
  est un problème d'unification où \bleu{s} et \bleu{t} sont deux
  motifs et si \bleu{P} a une solution \ali alors cette solution
  est \emph{unique} \ali et peut être \emph{trouvée en temps linéaire}.

\vfill
\end{slide} 
\end{document}

% LocalWords:  diophantiennes d'unificateurs idempotente Var ij idempotent nj
% LocalWords:  instancier flexible-rigide flexible-flexible flexibles-flexibles
% LocalWords:  PT préunification préunificateur Decompose Elimine patterns
% LocalWords:  pattern
