%% Time-stamp: <modified on 21 Oct 2004 at 19:31 by Pierre Lescanne>
%% /MIM-1/LOGIQUE/00-01/COURS+TRANSP/HILBERT/transp.tex
% \documentclass[%
%   slidesonly,%  Pour sortir les transparents seuls
%   semrot,%      Permettre des rotations eventuelles
%   semhelv,%    Helvetica
%   a4%           A4 paper
%   ]{seminar}


\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semrot,%      Permettre des rotations eventuelles
  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
\slidesmag{5}


\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage{color}
\usepackage{amsmath}
\usepackage{prooftree}
\usepackage{qsymbols}
\usepackage[all]{xy}

%% 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{Algèbres de termes}

\date{}

\pagestyle{}

\slidestyle{empty}

\slideframe{}   

\input{mes_couleurs}
\renewcommand{\emph}[1]{\rouge{#1}}

%--- symboles ---
\renewcommand{\phi}{\varphi}
\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{\Ra}{\ensuremath{\mathop{\Rightarrow}}}
\newcommand{\et}{\mathop{\&}}
\newcommand{\sh}{\mathop{|}}
\newcommand{\set}[2]{\{#1~|~#2\}}
\newcommand{\da}{\downarrow}
\newcommand{\jgbl}{\mathop{\da}}
\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]{
    \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]&||&}}

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

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

\newenvironment{displaymathbleu}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}

%%%%%%%%%%%%%%%%%% 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{green}{\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{L'ordre \bleu{\pref}}

L'ordre \bleu{\pref} est défini sur les mots de \bleu{A^*} par.

\begin{center}
  \bleu{\alpha\pref \beta} si et seulement \bleu{(\exists \gamma\in
  A^*)\; \alpha\,\gamma = \beta}.
\end{center}


\vfill
\end{slide}
%%------------------------------------------------------
\begin{slide}
\heading{Domaine d'un arbre enraciné étiqueté}

\bleu{\Natstar =\Nat-\{0\}}

Un \rouge{domaine d'arbre} est un sous-ensemble fini non vide \bleu{D} de
\bleu{\Natstar^*} tel que :
\begin{itemize}
\item \bleu{p\in D \quad\et\quad q \pref p
  \qquad\Ra\qquad q\in D}

\item \bleu{p i \in D \quad\et\quad j\in\Natstar
  \quad\et\quad j < i \qquad\Ra\qquad p j \in D}
\end{itemize}
\vskip 2 mm

{\sc Remarque :} \framebox{Tout domaine contient le mot vide.}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Arbre enraciné étiqueté}
Un \rouge{arbre étiqueté} par \bleu{A} est une application \bleu{T: D
  \rightarrow A} :
\begin{itemize}

\item \bleu{T(\epsilon)} est la \rouge{racine} de l'arbre.

\item \bleu{D} est le \rouge{domaine} (ou l'ensemble des \rouge{positions})
de \bleu{T} noté \bleu{Pos(T)}.

\item \bleu{T(p)} s'appelle l'\rouge{étiquette} à la position \bleu{p}.

\item Si \bleu{p\in Pos(T)} et \bleu{(\forall i\in\Natstar)p i\not\in
  Pos(T)}, alors \bleu{p} est une \rouge{feuille}
de \bleu{T}.
\end{itemize}

\vskip 2mm
Soit \bleu{TT} tel que \bleu{Pos(TT)= \{\epsilon, 1, 2, 21, 22, 221, 222\}}
et : 
\begin{footnotesize}
  \begin{eqnarray*}
    \epsilon \mapsto +\\
    1 \mapsto x\\
    2 \mapsto +\\
    21 \mapsto y\\
    22 \mapsto +\\
    221 \mapsto z\\
    222 \mapsto z
  \end{eqnarray*}
\end{footnotesize}

\xymatrix{
           &     &   +\ar@{-}[dl]\ar@{-}[dr]   &\\
 TT\quad = &  x  &      & + \ar@{-}[dl]\ar@{-}[dr] \\
           &     &   y  &    &  + \ar@{-}[dl]\ar@{-}[dr] \\
           &     &      & z  &     &   z
}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Sous-arbre}
\bleu{T_{|p}} est le \rouge{sous-arbre à la position} \bleu{p} défini par
  \bleu{T_{|p}(q) = T(pq)} \\\hspace*{20pt}où \bleu{Pos(T_{|p}) = \{ q \ | \ pq \in
  Pos(T)\}}.  
\vskip 2 mm
{\sc Exercice:} Décrivez \bleu{Pos(TT_{|22})} et \bleu{TT_{|22}}.
\vskip 2 mm
{\sc Fait:} \bleu{(T_{|p})_{|q} = T_{|pq}}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Remplacement}
\bleu{T[U]_p} est le \rouge{remplacement} du sous-arbre de \bleu{T} à la position
\bleu{p} par l'arbre~\bleu{U}, on le définit par 
\begin{bdp}Pos(T[U]_p) = \{q\in Pos(T) ~|~ \neg (p \pref q)\} \cup \{p p' ~|~ p'\in 
Pos(U)\}
\end{bdp}
et
\begin{bdp}
T[U]_p(q) = \left\{
\begin{array}{l}
T(q) \textrm{~si~} \neg(p\pref q)\\
U(p')  \textrm{~si~} q=pp' \textrm{~avec~} p'\in Pos(U)
\end{array}
\right.
\end{bdp}

\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
{\sc Exercice:} Soit \bleu{UU = TT[TT]_{21}}.
\begin{itemize}
\item Que vaut \bleu{UU(212)}?
\item Dessinez \bleu{UU}. 
\end{itemize}

\vskip 1cm

{\sc Résultats : }
\begin{itemize}
\item \bleu{T[U[V]_q]_p = T[U]_p[V]_{pq}}.
  
\item \bleu{T[U]_p[V]_q = T[V]_q[U]_p} si \bleu{p} et \bleu{q} sont
  étrangers\footnote{\bleu{p} et \bleu{q} sont dits \rouge{étrangers},
    si \bleu{p} n'est pas préfixe de \bleu{q} et si \bleu{q} n'est pas
    préfixe de \bleu{p}.}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Sous-arbre d'un remplacement}
\begin{itemize}
\item Si \bleu{p} et \bleu{q} sont étrangers, alors
  \bleu{(T[U]_p)_{|q} = T_{|q}}.
  
\item \bleu{(T[U]_p)_{|pp'} = U_{|p'}}.
\item \bleu{(T[U]_{pp'})_{|p} = (T_{|p})[U]_{p'}}.
\end{itemize}
\vfill

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Signature}
Une \rouge{signature} est une famille d'ensembles
\bleu{(\Sigma_n)_{n\in\Nat}}.

\begin{bdp}
\Sigma = \bigcup_{n\in\Nat} \Sigma_n
\end{bdp}

Si \bleu{f\in\Sigma_n}, \bleu{f} est dit d'\rouge{arité} \bleu{n}.

\bleu{\Sigma_0} est l'ensemble des \rouge{constantes}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Termes}
Soit \bleu{X} un ensemble dit ensemble des \rouge{variables}.
\vskip 2 mm
Quelques définitions : 
\begin{itemize}

\item[*] Un \rouge{$\Sigma$-terme} sur \bleu{X} est un arbre \bleu{t} étiqueté par
\bleu{\Sigma\cup X}, tel que
\begin{itemize}
\item Si \bleu{t(p)\in X} alors \bleu{p} est une feuille.
\item Si \bleu{t(p)\in \Sigma_n} alors 
  \begin{itemize}
  \item \bleu{p n\in Pos(t)} (donc \bleu{i\le n \quad\et\quad
      i\in\Natstar \Ra p i\in Pos(t)})
  \item et \bleu{p (n+1)\not\in Pos(t)}.
\end{itemize}
\end{itemize}

\item [*]\bleu{T(\Sigma,X)} est l'ensemble des \rouge{$\Sigma$-termes} sur
\bleu{X}.

\item [*] \bleu{Var(t) = \set{x\in X}{(\exists p\in Pos(t))\; t(p) = x}}

\end{itemize}
\vskip 2 mm

{\sc Fait:} Si \bleu{t(p)\in\Sigma_0} alors \bleu{p} est
une feuille.
\vfill 
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{$\Sigma$-algèbres}

Une \emph{$\Sigma$-algèbre} est un couple \bleu{{\cal A} = (A, \Sigma^{\A})} où

\bleu{A} est un ensemble dit \emph{support} de l'algèbre,
\begin{bdp}
{\Sigma^{\A}=\bigcup_{n\in\Nat} \Sigma^{\A}_n} 
\end{bdp}
et \bleu{f^{\A}\in\Sigma^{\A}_n: A^n\rightarrow A}.
\vfill 
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{$\Sigma$-algèbres libres}
\bleu{T(\Sigma,X)} munie des opérations d'\emph{enracinement} est
  une algèbre.   

Si \bleu{t_1} \ldots \bleu{t_n} sont $\Sigma$-termes sur \bleu{X} et
\bleu{f\in\Sigma_n} \ali on
définit le terme \bleu{f(t_1,\dots,t_n)} obtenu \ali en enracinant \bleu{f}
sur \bleu{t_1,...,t_n} par 
\begin{itemize}
\item \bleu{Pos(f(t_1,\dots,t_n)) = \{\varepsilon\} \cup
    \bigcup_{i=1}^n i Pos(t_i)}
\item \bleu{f(t_1,\dots,t_n)(\varepsilon) = f}
\item \bleu{f(t_1,\dots,t_n)(i p) = t_i(p).}
\end{itemize}
On dit que \bleu{T(\Sigma,X)} est l'\emph{algèbre libre} sur \bleu{X}.

\bleu{T(\Sigma)= T(\Sigma,\emptyset)} est l'\emph{algèbre initiale}.

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Algèbre initiale et induction structurelle} %
  Pour prouver une propriété \bleu{(`A t`:T(`S))\,P(t)} dans une
  algèbre initiale  \bleu{T(`S)} on utilise l'\brunir{induction structurelle}.  

  \begin{displaymathbleu}
    \prooftree%
    \parbox{8cm}{\bleu{(`A n`:\Nat)\,(`A f`:`S_n)(`A
      t_1`: T(`S))... (`A t_n`: T(`S))} \\
      \bleu{\hspace*{20pt}(\bigwedge_{i=1}^nP(t_i) "=>" P(f(t_1,...,t_n)))}}
    \justifies (`A t`:T(`S))\,P(t) \endprooftree
  \end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Algèbre initiale et induction structurelle} %

\brunir{Autrement dit:}

Pour vérifier une propriété sur toute l'algèbre initiale,\ali il faut
vérifier que pour chaque opérateur \bleu{f} d'arité \bleu{n}\ali la
propriété se transpose des termes \bleu{t_i} \ali vers le terme
\bleu{f(t_1,...,t_n)}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Algèbre initiale et induction structurelle} %
Par exemple, \ali si \bleu{`S_0=\{\textsf{nil}\}, `S_2=\{`.\}, `S_i=\emptyset} pour
\bleu{i=1} ou \bleu{i\ge 3}, l'induction structurelle est


  \begin{displaymathbleu}
    \prooftree%
    \parbox{8cm}{\bleu{P(\textsf{nil}) \ \wedge} \\  \hspace*{20pt}\bleu{(`A t_1,t_2`: T(\textsf{nil}\ ```+)\
        `. )) (P(t_1) \wedge P(t_2) "=>" P(t_1`.t_2))}}
    \justifies (`A t`:T(\textsf{nil} \ ```+)\ `. ))\,P(t)
    \endprooftree
  \end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Morphismes}
Un \emph{morphisme} \bleu{\phi: T(\Sigma, X)\rightarrow A} est une
application telle que
\begin{itemize}
\item \bleu{\phi(x_i) = a_i}
\item \bleu{\phi(f(t_1,...,t_n)) = f^{\A}(\phi(t_1),...,\phi(t_n))}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Substitutions, domaine, codomaine}

Soit \bleu{X} un ensemble dénombrable de variables.
\vskip 2 mm
\begin{itemize}
\item [*]
Une \rouge{substitution} est une application \bleu{\sigma :  X\rightarrow
  T(\Sigma, X)} qui est l'identité presque partout (c-à-d sauf sur un
ensemble fini).

\item [*]
On note :
  \bleu{Dom(\sigma) = \set{x\in X)}{x\not=\sigma(x)}}
\ali le \emph{domaine}.

\item [*] On note : \begin{displaymathbleu}
  Range(\sigma) = \bigcup_{\sigma(x)\not=x}Var(\sigma(x)) = \set{x\in Var(\sigma(x))}{x\not=\sigma(x)}
\end{displaymathbleu}
  \ali le \emph{codomaine}.

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Substitutions, domaine, codomaine}

On \rouge{étend} \bleu{\sigma} à \bleu{T(\Sigma,X)} en une application
\bleu{\shat} (souvent notée \bleu{\sigma}).


\begin{itemize}
\item \bleu{\shat(x) = \sigma(x)},
\item \bleu{\shat(f(t_1, ..., t_n)) = f(\shat(t_1),..., \shat(t_n))}.
\end{itemize}

\bleu{Sub(T(\Sigma,X))} est l'ensemble des substitutions.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Identités et réduction}

\begin{itemize}

\item [*]  Une \rouge{identité} \bleu{g \approx d}
  est un couple, c'est-à-dire un élément de \bleu{T(\Sigma,X)\times T(\Sigma,X)}.
  
\item [*]  Soit \bleu{E} un ensemble d'identités, la \rouge{contraction} \bleu{\raE} est
  définie par

\begin{center} 
\bleu{s \raE t}

ssi

\bleu{(\exists g\approx d\in E) (\exists \sigma\in
  Sub(T(\Sigma,X)))(\exists p\in Pos(s))}

et

\bleu{s_{|p} = \sigma(g) \quad\et\quad t=s[\sigma(d)]_p.}

\end{center}

\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Systèmes de réécriture}

D'autres définitions :
\begin{itemize}


\item Une \emph{règle de réécriture} est une identité \bleu{g\approx d} telle que
\bleu{Var(g)\supseteq Var(d)}.
\ali 
\begin{small}
  On écrit \bleu{g \rightarrow d}.
\end{small}

\item Un \emph{système de réécriture} est un ensemble de règles de
réécriture.

\item Un \emph{redex} de \bleu{s} est une instance (c'est-à-dire un
  sous-terme de \bleu{s} de la forme \bleu{\sigma(g)} pour
  \bleu{\sigma\in Sub(T(\Sigma,X))}) d'un membre gauche de règle de
  réécriture \bleu{g \rightarrow d}.

\item \emph{Contracter le redex} \bleu{s_{|p}} à la position \bleu{p}, \ali
c'est passer de \bleu{s = s[\sigma(g)]_p} à \bleu{t=s[\sigma(d)]_p}.

\end{itemize}
\vfill
\end{slide}
\end{document}
% LocalWords:  joignable infixée ssi semi-confluence semi-confluente Church Dom
% LocalWords:  Church-Rosser d'ambiguïté Goodstein noethérien plongeable Newman
% LocalWords:  multiensemble Sous-arbre sous-arbre d'identités




