\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{\nf}{\textsf{nf}}
\newcommand{\Nat}{\mathbb{N}}

%\pagestyle{empty}


\title{Magistère d'Informatique et Modélisation}
\author{Corrigé du 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}

\section*{Exercice 1}
\begin{enumerate}
\item Aucun membre gauche de règle de $R_1\cup R_2$ ne filtre
  $s^k(0)$.
  
  Pour montrer que chaque terme admet une forme normale qui est l'un
  des $s^k(0)$, il faut montrer que tout terme qui n'est pas de cette
  forme est réductible et comme il n'y a qu'un nombre fini de
  réductions possibles partant d'un terme donné, cette forme $s^k(0)$
  est forcément atteinte.
  
  Soit un terme $t$ qui n'est pas de la forme $s^k(0)$ ; $t$ contient
  un symbole qui est soit $\oplus$, soit $d$, soit $c$.  Considérons,
  le symbole $\oplus$, $d$, $c$ qui est le plus bas dans $t$ ;c-à-d
  que ce symbole est à une position $p$ telle que pour tout $r$, $t(p
  r)$ est soit $s$ , soit $0$.  Par conséquent $t_{|p}$ filtre l'un des
  membres gauches d'une règle de $R_1\cup R_2$.

\item On admet que $\nf(s^p(0) \oplus s^q(0)) = s^{p+q}(0)$.  On voit que
  $\nf(d(s^n(0)))= s^{2n}(0)$.  En effet, par induction $\nf(d(0)) = 0 =
  s^0(0)$ et
\[\nf(d(s^{n+1}(0))) = \nf(d(s(s^n(0)))) = s(s(\nf(d(s^n(0))))) =
s(s(s^{2n}(0))) = s^{2(n+1)}(0).\]

Montrons que $\nf(c(s^n(0))) = s^{n^2}(0)$.  Clairement $\nf(c(0)) = 0$
et  
\begin{eqnarray*}
\nf(c(s^{n+1}(0))) &=& \nf(c(s(s^n(0))))\\
 &=& s(\nf(d(s^n(0))) \oplus \nf(c(s^n(0))))\\
 &=& s(s^{2n}(0) \oplus s^{n^2}(0)) \\
 &=& s^{1+2n+n^2}(0) = s^{(n+1)^2}(0).
\end{eqnarray*}

\item Il suffit de démontrer un certain nombre d'inégalités.

  \begin{eqnarray*}
    \pi(s(m) \oplus n) &=& 2\pi(m) + 2 + \pi(n) \\
    &>& 2\pi(m) +\pi(n) + 1 \\
    &=& \pi(s(m \oplus n))
  \end{eqnarray*}
 \begin{eqnarray*}
    \pi(0 \oplus n) &=& 4 + \pi(n) \\
    &>& \pi(n)
  \end{eqnarray*}
 \begin{eqnarray*}
    \pi(d(s(n))) &=& 3\pi(n) + 3\\
    &>& 3\pi(n)+2\\
    &=& \pi(s(s(d(n))))
  \end{eqnarray*}
  Si l'on sait prouver que $6>2$ on doit pouvoir prouver que
  $\pi(d(0)) > \pi(0)$.

\item On prend comme interprétation $\cro c\crf(p) = p^3$ et on voit
  que 
  \begin{eqnarray*}
    \pi(c(s(n))) & = & (\pi(n) + 1)^3 \\
    &=& \pi(n)^3 + 3\pi(n)^2 + 3 \pi(n) + 1\\
    &>& 1 + 2(3\pi(n)) + \pi(n)^3 \\
    &=& \pi(s(d(n) \oplus c(n))).
  \end{eqnarray*}
  On remarque, en effet, que $\pi(n)^2>\pi(n)$, puisque $\pi(n)>2$.\\
   $\pi(c(0)) > \pi(0)$ vient de $2^3 = 8 > 2$.
\item La forme normale de $t(s^n(0))$ est $s^{2^{2^n}}(0)$.  Tout
  d'abord remarquons que $(2^{2^n})^2 = 2^{2^{n+1}}$.
  \begin{eqnarray*}
    \nf(t(s^{n+1}(0))) &=& \nf(c(t(s^n(0))))\\
    &=& \nf(s^{(2^{2^n})^2}(0))\\
    &=& s^{2^{2^{n+1}}}(0).
  \end{eqnarray*}
  La forme normale de $t^p(0)$ est donc une tour de la forme
$2^{2^{.^{.^2}}}$ et la longueur de la plus longue chaîne de
dérivation est plus que doublement exponentielle.  Donc on ne peut pas 
faire la preuve de terminaison en utilisant les ordres polynômiaux.

Un autre argument peu s'appuyer sur la fonction $\theta(n)$ où
$s(^{\theta(n)}(0))$ est la forme normale de $t(s^n(0))$.  $\theta(n)$
est la fonction ``calculée'' par le système de réécriture. Comme cette
fonction n'est pas à croissance polynomiale la terminaison de ce
système n'est pas prouvé par un ordre polynômial.

Une troisième méthode plus délicate consiste à montrer que les
inégalités que l'on peut déduite des interprétations des règles, ne
peuvent être satisfaite par aucun polynôme.

\item Il n'y a pas de paires critiques, donc le système est localement
  confluent.  Et comme il termine, il est confluent.  Donc il y a
  unicité de la forme normale.
\end{enumerate}
\newpage

\section*{Exercice 2}
\begin{enumerate}
\item
  \begin{eqnarray*}
 Muleq(a, b) &=& Muleq (x, f(c,c)) \cup Muleq (f(x,c), f(x,y))\\
 &=& (\{x\}, \aco f(c,c)\acf) \cup Muleq(x,x) \cup Muleq(c,y)\\
 &=& \{(\{x\}, \aco f(c,c)\acf), (\{x\},\aco~\acf), (\{y\},\aco c\acf)\}.
\end{eqnarray*} 
\begin{eqnarray*}
Com(a,b) &=& f(Com(x,f(c,c)), Com(f(x,c), f(x,y)))\\
&=& f(x, f(Com(x,x), Com(c,y)))\\
&=& f(x, f(x,y))
\end{eqnarray*}

\item L'équation se met sous la forme 

\[(\Sigma,\Pi) = \{(\{\xi\}, \aco f(f(x,f(x,c)), f(f(c,c), f(x,y)))\textbf{,} f(z,z)\acf)\}.\]

On a donc 
\begin{center}
    $(\Sigma,\Pi)$

$\Mapsto$

 $(\{\xi\}, \aco f(z,z)\acf)$
  
  $(\{z\}, \aco f(x,f(x,c))\acf)$

 $(\{z\}, \aco f(f(c,c), f(x,y))\acf)$

  $\Mapsto$

 $(\{\xi\}, \aco f(z,z)\acf)$
  
  $(\{z\}, \aco f(x,f(x,c)), f(f(c,c),  f(x,y))\acf)$

$\Mapsto$

 $ (\{\xi\}, \aco f(z,z)\acf)$

  $(\{z\}, \aco f(x,f(x,y))\acf)$

$(\{x\}, \aco f(c,c)\acf)$ 

$(\{x\},\aco~\acf)$ 

$(\{y\},\aco c\acf)$

  $\Mapsto$

 $ (\{\xi\}, \aco f(z,z)\acf)$

  $(\{z\}, \aco f(x,f(x,y))\acf)$

$(\{x\}, \aco f(c,c)\acf)$ 

$(\{y\},\aco c\acf)$

\end{center}
La première étape est $Dec$, la deuxième $Fus$, la troisième $Dec$, la
quatrième $Net$.

\item Une première forme d'échec pour l'algorithme est un échec d'un
  $Dec$ à travers un échec de $Muleq$ quand un appel récursif à
  $Muleq$ se fait sur deux termes qui ont des racines différentes
  (dans notre cas $+$ et $c$).
  
  Une deuxième forme d'échec pour l'algorithme est la détection d'un
  cycle parmi les variables (relation $\lessdot_E$).

\item Une forme résolue est une multi-équation  dans laquelle, 
  \begin{itemize}
  \item chaque variable apparaît une seule fois en partie gauche, 
  \item chaque membre droit est réduit à un terme ou à aucun terme
    dans le cas où le membre gauche contient plus d'une variable,
  \item la relation $\lessdot_E$ est sans cycle.
\end{itemize}
Après un tri topologique des variables, suivant $\lessdot_E$, qui
donne $x_1 \ll x_2 \ll ...\ll x_n$, une substitution $\sigma_E$ est
obtenue comme la dernière substitution d'une suite de substitutions
\begin{itemize}
\item $\sigma_{0} = id$
\item si $x_i$ apparaît dans un couple $(\{...,x_i,...\}, \aco t \acf)$, 
  $\sigma_{i+1} = \{x_i\mapsto \sigma_{i}(t)\} \cup \sigma_{i}$,
\item si $x_i$ apparaît dans un couple $(\{...,x_i,...\}, \aco \acf)$,
  où toutes les autres variables $y$ sont telles que $y\ll x_i$
  alors $\sigma_{i+1} = \sigma_{i}$,
\item si $x_i$ apparaît dans un couple $(\{...,x_i,...\}, \aco \acf)$,
  où il existe une autre variable $y$ telle que $x_i\ll y$,
  alors $\sigma_{i+1} = \{x_i\mapsto y\} \cup \sigma_{i}$.
\end{itemize}

\item La relation $\lessdot_E$ est $\xi\lessdot_E z\lessdot_E x$ et
  $z\lessdot_E y$.

\item Si $Fus$ n'est pas applicable, alors chaque variable apparaît
  une seule fois en partie gauche.  Si $Dec$ n'est pas applicable,
  chaque membre droit est réduit à un terme. Si $Net$ n'est pas
  applicable, les membres gauches contiennent au moins deux variables
  ou le membre droit contient au moins un terme.   Avec l'absence de
  cycle, cela caractérise effectivement les formes résolues.
\item On définit sur $E$ deux nombres.
  \begin{itemize}
  \item $n_v(E)$ est le nombre total d'occurrences des variables dans les 
    membres gauches des couples $(X,M)$.  Si une variable apparaît deux
    fois , elle est comptée deux fois.

  \item $n_f(E)$ est le nombre total d'opérateurs fonctionnels.
  \end{itemize}
On dit que $E \ggg F$ si et seulement si $n_v(E) > n_v(F)$ ou  $n_v(E)
= n_v(F)$ et  $n_f(E) > n_f(F)$.   L'ordre $\ggg$ termine clairement
et on voit que $Fus$ et $Net$ réduisent $n_v$   et $Dec$ ne change pas
$n_v$ et réduit $n_f$. 

\item Une solution d'un problème multi-équationnel est une
  substitution $\sigma$ telle que pour chaque $(\{x_1,...,x_p\},\aco
  t_1,..., t_q\acf)$ on a $\sigma(x_1) =...=\sigma(x_p) = \sigma(t_1)
  ...= \sigma(t_q)$.

 Puisqu'il y a une variable $x$ commune dans $X\cap X'$ on voit que 
 $\sigma(x_1) =...=\sigma(x_p) = \sigma(t_1) ...=
  \sigma(t_q) = \sigma(x) = \sigma(x_1') =...=\sigma(x_{p'}') = \sigma(t_1')= ...=
  \sigma(t_{q'}')$ et donc $Fus$ préserve les solutions. 

$Net$ préserve clairement les solutions.

$Dec$ préserve aussi les solutions. En effet (en gros), si
$\sigma(s)=\sigma(t)=\sigma(u)$ pour chaque $u\in M$, alors
$\sigma(Com(s,t))=\sigma(u)$. D'autre part, pour chaque $p\in Pos(s)$
tel que $s_{|p}=x$, on a $\sigma(x)=\sigma(t_{|p})$ ; donc la
multi-équation $(\{x\}, \aco t_{|p}\acf)$ apparaît dans $Muleq(s,t)$
et vice-versa si elle apparaît alors il y a une position dans $s$ où
il y a une variable. $(\{x\}, \aco t_{|p}\acf)$ est donc satisfaite
avant et après $Dec$.  On a le résultat pour $t$ par symétrie.
\end{enumerate}

\end{document}
