\documentclass[12pt]{article}

\usepackage{a4}
\usepackage[latin1]{inputenc}
\usepackage[francais]{babel}
\usepackage[all]{xy}
\usepackage{amsfonts,amsmath,amsthm,amssymb,stmaryrd}

\renewcommand{\phi}{\varphi}

\renewcommand{\S}{\textbf{S}}
\newcommand{\bl}[1]{#1}
\newcommand{\bleu}[1]{$#1$}
\newcommand{\Un}{\textsf{\textbf{1}}}
\newcommand{\Y}{\mathbf{Y}}
\newcommand{\K}{\mathbf{K}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\T}{\mathbf{T}}
\newcommand{\F}{\mathbf{F}}
\newcommand{\jnt}{\uparrow}
\newcommand{\ou}{\ensuremath{\mathbf{ou}\ }}
\newcommand{\non}{\ensuremath{\mathbf{non}}}
\newcommand{\Ra}{\Rightarrow}
\newcommand{\eq}{\stackrel{?}{=}}
\newcommand{\cro}{[\!\![}
\newcommand{\crf}{]\!\!]}
\newcommand{\aco}{\{\!\!\{}
\newcommand{\acf}{\}\!\!\}}
\newcommand{\ra}{\xymatrix{\ar@{>}[r] &}}
\newcommand{\Nat}{\mathbb{N}}

%\pagestyle{empty}


\title{Magistère d'Informatique et Modélisation}
\author{Partiel de réécriture}

\date{\emph{26 Mars 2001}}

\newcommand{\infer}[2]{
 \begin{array}{c}
   #1\\
   \hline \noalign{\vskip 1pt}#2
  \end{array}}

 \newcommand{\inferTwo}[3]{
 \begin{array}{c}
   #1 \hspace{2em} #2\\
   \hline \noalign{\vskip 1pt}#3
  \end{array}}

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

 \newcommand{\inferSideLabel}[4]{
 {#1} \;\; 
  \begin{array}{c}
  #2 \\
  \hline \noalign{\vskip 1pt}#3
  \end{array}
  \quad {\textrm{#4}}}

\begin{document}
\maketitle 
\thispagestyle{empty}

\centerline{\textit{Documents autorisés.}}

\section*{Exercice 1}

Soient les systèmes de réécriture:

\begin{center}
\begin{math}
  R_1\left\{
\begin{array}{lcl}
  s(m) \oplus n & \ra & s(m \oplus n) \\
  0 \oplus n & \ra & n\\[4pt]
  d(s(n)) & \ra & s(s(d(n)))\\
  d(0) & \ra & 0
\end{array}
\right.
\quad
R_2\left\{
\begin{array}{lcl}
  c(s(n)) & \ra & s(d(n) \oplus c(n))\\
  c(0) & \ra & 0
\end{array}
\right.
\end{math}
\end{center}

\begin{enumerate}
\item Montrez que les termes $s^k(0)$ pour $k\in \Nat$ sont des formes
  normales pour $R_1\cup R_2$.  En admettant la terminaison de
  $R_1\cup R_2$, montrez que chaque terme clos $t\in T(\Sigma)$
  possède pour $R_1\cup R_2$ une forme normale qui est $s^k(0)$ pour
  un $k\in \Nat$.
  
\item Admettant que la forme normale est unique, calculez $k$ en
  fonction de $p$ pour la forme normale de $c(s^p(0))$.

\item Montrez la terminaison du système $R_1$ par l'ordre polynômial
  défini sur $A=\{n\in\Nat ~|~ n\ge 2\}$ par les interprétations
  \begin{eqnarray*}
    \cro 0 \crf &=& 2\\
    \cro s \crf(p) & = & p+1\\
   \cro \oplus \crf(p,q) & = & 2p+q\\
      \cro d \crf(p) & = & 3p
  \end{eqnarray*}
\item Montrez la terminaison du système  $R_1 \cup R_2$, par un ordre
  polynômial. 
\item Soit
\begin{center}
\begin{math}
  R_3\left\{
\begin{array}{lcl}
  t(s(n)) & \ra & c(t(n))\\
  t(0) & \ra & s(s(0))
\end{array}
\right.
\end{math}
\end{center}
Peut-on montrer la terminaison de $R_1\cup R_2 \cup R_3$ par un ordre polynômial?

\item Montrez que la forme normale dans $R_1\cup R_2$ de tout terme
  est unique.
\end{enumerate}

\section*{Exercice 2}

Dans cet exercice, qui est une variation sur l'\emph{algorithme
  d'unification de Martelli-Montanari}, on suppose que la signature
n'est constituée que d'une constante $c$ et d'un symbole dyadique $f$,
c-à-d d'arité $2$.  

Dans la suite, un multiensemble comme $a \mapsto 1, b \mapsto 2$ et $c
\mapsto 0$ pour tout autre elément $c$ est noté $\aco a, b, b \acf$.
L'ensemble vide est noté $\emptyset$ et le multiensemble vide est noté
$\aco~\acf$.  Une \emph{multi-équation} est un couple $(X,M)$ où $X$
est un ensemble de variables et $M$ est un multiensemble de termes qui
ne sont pas des variables.  Un \emph{problème multi-équationnel} est
un ensemble de multi-équations.  Si $(s,t)$ est une paire de termes
qui ne sont pas des variables et que l'on veut unifier, on lui associe
le problème multi-équationnel $\{(\Xi, \Pi)\}$ où $\Xi=\{\xi\}$, où
$\Pi=\aco s, t\acf$ et où $\xi$ est une variable qui n'apparaît ni
dans $s$ ni dans $t$ (introduite d'ailleurs uniquement par commodité).
Par exemple, si on doit unifier $x+y=x+(z+z)$, on considérera le
problème multi-équationnel $\{(\{\xi\}, \aco x+y, x+(z+z)\acf)\}$.

On définit trois règles:

$\inferLabel{Net}{(\{x\}, \aco~\acf)\cup E}{E}$

$\inferSideLabel{Fus}{(X, M) \cup (X', M') \cup
  E}{(X\cup X', M\cup M') \cup E}{si $X\cap X' \not= \emptyset$}$

$\inferSideLabel{Dec}{(X, M \cup \aco s, t\acf)\cup E}{(X, M \cup\aco
  Com(s,t)\acf) \cup Muleq(s,t) \cup E}{si $Muleq(s,t)$ est défini}$.

Si $s$ et $t$ sont deux termes, $Muleq(s,t)$ est l'ensemble des
multi-équations issues de $s$ et $t$ et $Com(s,t)$ est la partie
commune de $s$ et $t$.  Ils sont définis comme suit. Dans les
définitions, $tt$ est un terme qui n'est pas une variable et $x$ et $y$
sont des variables.

\begin{eqnarray*}
  Muleq(f(s_1, s_2), f(t_1, t_2)) &=& Muleq(s_1,t_1) \cup Muleq(s_2, t_2)\\
  Muleq(c, c) &=& \emptyset\\
  Muleq(x, tt) &=& (\{x\}, \aco tt\acf)\\
  Muleq(tt, x) &=& (\{x\}, \aco tt\acf)\\
  Muleq(x,y) &=& (\{x\}\cup\{y\}, \aco~\acf)
\end{eqnarray*}
Si $Muleq(s,t)$ n'apparaît dans aucun des cas ci-dessus,
$Muleq(s,t)$ n'est pas défini.

\begin{eqnarray*}
  Com(f(s_1, s_2), f(t_1, t_2)) &=& f(Com(s_1,t_1),Com(s_2, t_2))\\
  Com(c, c) &=& c\\
  Com(x, tt) &=& x\\
  Com(tt, x) &=& x\\
  Com(x,y) &=& x
\end{eqnarray*}
Si $Com(s,t)$ n'apparaît dans aucun des cas ci-dessus,
$Com(s,t)$ n'est pas défini.

\begin{enumerate}
  
\item On définit deux termes $a=f(x,f(x,c))$ et $b=f(f(c,c), f(x,y))$.
  Calculez $Muleq(a, b)$ et $Com(a,b)$.
\item «Unifiez» par cette méthode $f(f(x,f(x,c)), f(f(c,c), f(x,y))) =
  f(z,z)$.  En d'autres termes, mettez l'équation sous la forme
  $(\Xi,\Pi)$ ci-dessus et appliquez les règles de transformation,
  jusqu'à ce que plus aucune ne s'applique.
\item Donnez et discutez les cas d'arrêt par échec de l'algorithme.
\item Étant donné un problème multi-équationnel $E$, on définit sur
  les variables une relation $x\lessdot_E y$ s'il existe une
  multi-équation $(X,M)\in E$ et un terme $t\in M$ tels que $x\in X$
  et $y\in Var(t)$.  Définissez les formes résolues.  Quelle est la
  substitution que vous associeriez à chacune de ces formes résolues.

\item Décrivez $\lessdot_E$ pour le  problème multi-équationnel
  $E$  résultat de la question~2.
\item Montrez que s'il n'y a pas de règle applicable, s'il n'y pas
  d'échec et si la relation $\lessdot_E$ n'a pas de cycle, alors le
  système $E$ est en forme résolue.

\item Donnez un ordre qui termine et tel que les règles diminuent cet
  ordre. 
\item Définissez l'ensemble des solutions d'un problème
  multi-équationnel.  Montrez que les règles préservent cet ensemble
  de solutions.
\end{enumerate}

\end{document}

