%% Time-stamp: <modified on 27 Sep 2004 at 14:21 by Pierre Lescanne>
%% /MIM-1/REECRITURE/intro_reec.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

%\renewenvironment{slide}[1]{#1} 
%\def\printlandscape{}  % pour sortir en portrait
%\slidesmag{1} 
%\usepackage{fullpage}

%\def\printlandscape{\special{landscape}}     % pour sortir en landscape
%\rotateheaderstrue       % si tu combines slide et slide*

\slidesmag{5}


\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
\usepackage{amsmath}
\usepackage[all]{xy}
\usepackage{qsymbols}
\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}

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

\author{Introduction}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\renewcommand{\phi}{\varphi}
\newcommand{\ali}{\newline\hspace*{20pt}}
\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{\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{\xb}{\overline{x}}
    \newcommand{\xbb}{\overline{\overline{x}}} 

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                environnements
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}

\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{\ar@3{-}[r] &}}
\newqsymbol{"<<->>"}{\xymatrix {\ar@{<<->>}[r] &}}
\newqsymbol{"==>"}{\xymatrix @C 15pt {\ar@{=>}[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{\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]&||&}}

%%%%%%%%%%%%%%%%%% Headings %%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}
\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}
\heading{Qu'est-ce que la récriture}
La récriture\footnote{Certains disent et écrivent la
  «réécriture».} est la théorie de la simplification qui sert
\begin{itemize}
\item en \emph{calcul symbolique},
\item en \emph{sémantique}, la valeur d'une expression est son
  résultat par évaluation, (il y a des liens avec la lambda calcul),
\item en \emph{démonstration automatique}, (il faut «simplifier» à
  tour de bras!)
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le groupes}
%
Considérons les trois équations de l'axiomatique faible des groupes,
on note \bleu{*} le produit, \bleu{e} l'élément neutre et \bleu{\xb}
l'inverse de \bleu{x}.
\begin{eqnarraybleu}
  x * e &=& x \\
x * \xb &=& e \\
(x*y)*z &=& x*(y*z)
\end{eqnarraybleu}
On veut prouver que \brunir{$x=e*x$}, c'est-à-dire qu'«un élément neutre
à droite est aussi un élément neutre à gauche !».
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Pour s'y retrouver on utilise les des «flèches», pour orienter les
équations.
\begin{eqnarraybleu}
  x * e &\ra& x \\
x * \xb &\ra& e \\
(x*y)*z &\ra& x*(y*z)
\end{eqnarraybleu}

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Pour s'y retrouver on utilise les des «flèches», pour orienter les
équations.
\begin{eqnarraybleu}
  x * e &\ra& x \\
x * \xb &\ra& e \\
(x*y)*z &\ra& x*(y*z)
\end{eqnarraybleu}

%
\vfill %
\emph{$`(:-)$} Peut-être même que la flèche symbolise une
\emph{«simplification»!}%
    \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Preuve de $x=e*x$}

  \begin{tiny}
\hspace*{-30pt}\xymatrix @R 12pt @C 0pt {
      &&& &&& e * (x * (\xb * \xbb)) \ar[dr]\ar[dl]&\\
      & (x*\xb)*\xbb \ar[dr]\ar[dl]&& (e*e)*\xbb \ar[dr]\ar[dl]&& e*((x*\xb)*\xbb) \ar[dl]&& e*(x*e)\ar[d]\\
      x*(\xb*\xbb)\ar[d]&& e*\xbb && e*(e*\xbb)&&&e*x\\
x*e\ar[d]\\
x
    }
  \end{tiny}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La grande question de la récriture}%
Comment peut-on automatiser ce processus de démonstration?
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Encore des questions}
%
\begin{itemize}
\item \bleu{e*(x*(\xb*\xbb))}
\item ou \bleu{(e*e)*\xbb}
\item ou \bleu{(x*\xb)*\xbb}
\end{itemize}
se récrivent de plusieurs manières, ils posent un problème pour un
simplifieur.
%
\vfill
Est-on sûr que \bleu{e*(x*(\xb*\xbb))\ra e*((x*\xb)*\xbb)} simplifie
quelque chose ?

\verdir{Exercice:} prouver \bleu{e=\xb*x}.  On pourra regarder
\emph{All that} p. 5.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Encore des questions}
%
Des termes comme comme
\begin{itemize}
\item Y a-t-il une seule forme simplifiée?
\item Comment orienter les équations ?
\item Les processus de simplification se termine-t-il?
\item Comment le démontre-t-on?
\item Sait-on résoudre les équations dans les termes?
\item Peut-on calculer un système pour la simplification dans les
  groupes? Quitte à ajouter de nouvelles règles?
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un système de «simplification» pour les groupes}
  \begin{scriptsize}
    \begin{eqnarraybleu}
      x*e &\ra& x\\
      e*x &\ra& x\\
      x*\xb &\ra& e\\
      \xb*x &\ra& e\\
      \overline{e} &\ra& e\\
      \xbb &\ra& x\\
      \overline{x*y} &\ra& \overline{y}*\xb\\
      (x*y)*z &\ra& x*(y*z)\\
      x*(\xb*y) &\ra& y\\
      \xb*(x*b)&\ra&y
    \end{eqnarraybleu}
  \end{scriptsize}
    %
    \vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Associativité et endomorphisme}
Considérons les deux identités:

\begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &=& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x*y) &=& f(x)*f(y) &\emph{\mathsf{(E)}}
    \end{array}
}
\end{center}
% 
    \vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{première} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x*y) &\ra& f(x)*f(y) &\emph{\mathsf{(E)}}
    \end{array}
}
\end{center}
   \vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}
    \end{array}
}
\end{center}
   \vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}
    \end{array}
}
\end{center}

\vspace*{15pt}

\bleu{f(x*y)} est plus lourd que \bleu{f(x)},\\
donc \bleu{f(x*y)*z} penche plus à gauche que \bleu{f(x)*(f(y)*z)}.
   \vfill
C'est une bonne idée pour orienter l'associativité!
    \addtocounter{slide}{-1}
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}\\
f^2(x*y)*z &\ra& f^2(x)*(f^2(y)*z)  &\emph{\mathsf{(EEA)}}
    \end{array}
}
\end{center}
   \vfill  \addtocounter{slide}{-1}
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}\\
f^2(x*y)*z &\ra& f^2(x)*(f^2(y)*z)  &\emph{\mathsf{(2EA)}}\\
f^3(x*y)*z &\ra& f^3(x)*(f^3(y)*z)  &\emph{\mathsf{(3EA)}}
    \end{array}
}
\end{center}
   \vfill  \addtocounter{slide}{-1}
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}\\
f^2(x*y)*z &\ra& f^2(x)*(f^2(y)*z)  &\emph{\mathsf{(2EA)}}\\
f^3(x*y)*z &\ra& f^3(x)*(f^3(y)*z)  &\emph{\mathsf{(3EA)}}\\
&\vdots&\\
f^n(x*y)*z &\ra& f^n(x)*(f^n(y)*z)  &\emph{\mathsf{(nEA)}}\\
&\vdots&\\
    \end{array}
}
\end{center}
   \vfill  \addtocounter{slide}{-1}
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{deuxième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x*y)*z &\ra& f(x)*(f(y)*z)  &\emph{\mathsf{(EA)}}\\
f^2(x*y)*z &\ra& f^2(x)*(f^2(y)*z)  &\emph{\mathsf{(2EA)}}\\
f^3(x*y)*z &\ra& f^3(x)*(f^3(y)*z)  &\emph{\mathsf{(3EA)}}\\
&\vdots&\\
f^n(x*y)*z &\ra& f^n(x)*(f^n(y)*z)  &\emph{\mathsf{(nEA)}}\\
&\vdots&\\
    \end{array}
}
\end{center}
   \vfill  
\emph{\Large HUM!}
\addtocounter{slide}{-1}
  \end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{troisième} façon de simplifier:

 \begin{center}
\bleu{
    \begin{array}[c]{rcll}
(x*y)*z &\ra& x*(y*z)& \emph{\mathsf{(A)}}\\
f(x)*f(y) &\ra& f(x*y) &\emph{\mathsf{(E)}}\\
f(x)*(f(y)*z) &\ra&  f(x*y)*z &\emph{\mathsf{(EA)}}
    \end{array}
}
\end{center}
   \vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}

{\LARGE Il va falloir comprendre tout ça!}

  \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le plan du cours}
%
  \begin{itemize}
  \item Les réductions abstraites,
  \item Termes et systèmes de récriture,
  \item La terminaision des systèmes de récriture,
  \item La résolution des équations dans les termes ou unification.
  \item La complétion,
  \item La résolution et/ou les bases de Gröbner.
  \end{itemize}
%
\vfill
  \end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bibliographie}

 
  \brunir{Franz Baader et Tobias Nipkow}, \verdir{Term Rewriting and
    All that},\ali{Cambridge University Press}, (1998)


  \brunir{Chistoph Hankin}, \verdir{Lambda calculi: a Guide for the
    Computer Scientist}\footnote{pour ceux qui n'ont pas fait de
    lambda-calcul, à lire avant d'aborder le chapitre sur l'unification,}, \ali{Oxford University Press}, (1994)
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Plus de bibliographie}

  \brunir{Enno Ohlebusch}, \verdir{Advanced Topics in Term Rewriting},
  \ali {Springer-Verlag}, (2002).

  \brunir{Terese}, \verdir{Term Rewriting Systems}, \ali{Cambridge
    University Press}, (2003)
%
\vfill
\end{slide}
%------------------------------------------------------
%\begin{slide}
%\heading{}

%\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  joignable infixée ssi semi-confluence semi-confluente Church m-n
% LocalWords:  Church-Rosser d'ambiguïté Goodstein noethérien plongeable Newman
% LocalWords:  multiensemble irréflexive s'imaginer multiensembles II canopée
% LocalWords:  irréflexivité arborescence l'arborescence N.B All that Sait-on

%%% Local Variables: 
%%% mode: latex
%%% TeX-master: t
%%% End: 
% LocalWords:  simplifieur termine-t-il démontre-t-on Peut-on
