ajout d'intro et de conclusion

[hdrcouchot.git] / annexePreuveMixage.tex

diff --git a/annexePreuveMixage.tex b/annexePreuveMixage.tex
index 4757b0b68d5c5c0073db472a783b7fdda715ad5c..8132c680f019bab3fc16df7cc88a2f0e14e7ece2 100644 (file)
--- a/annexePreuveMixage.tex
+++ b/annexePreuveMixage.tex
@@ -1,104 +1,104 @@
-
-Let  us introduce an  ordering $\preceq$  between classes.   Formally, \class{p}
-$\preceq$   \class{q}   if   there    exists   a   path   of   length   $\alpha$
-($0<\alpha<|\mathcal{K}|$)  from  an  element  of  \class{p} to  an  element  of
-\class{q}.  One can  remark that if \class{p}$\preceq$\class{q}, then  it is not
-possible to also have \class{q}$\preceq$\class{p}.
-
-% \begin{lemma}
-%   The relation $ \preceq$ is a partial order
-%   \begin{Proof}
-%     Reflexivity is established  since for any $p_0 \in [p]$  there exists a path
-%     of length  0 from  $p_0$ to $p_0$.
-%     For antisymmetry, suppose  there exists two classes $[p]$ and 
-%     $[q]$ such that $[p] \preceq [q]$ and $[q] \preceq [p]$.
-%     There exists then $p_0,p'_0 \in [p]$, $q_0, q'_0 \in [q]$ with paths 
-%     from $p_0$ to $q_0$ and from $q'_0$  to $p_0$.
-%     Thus, elements $p_0$, $p'_0$, $q_0$ and $q'_0$ belong to the same 
-%     strongly connected component and then
-%     $[p]$ = $[q]$.  Transitivity is obviously established.
-%   \end{Proof}
-% \end{lemma}
+Introduisons tout d'abord une relation d'ordre 
+$\preceq$  entre les  classes d'équivalences.   
+Formellement, \class{p}
+$\preceq$   \class{q}   
+s'il existe un chemin de longueur   $\alpha$
+($0\le\alpha<|\mathcal{K}|$)  entre un élément le la classe
+\class{p} vers un élément  de
+\class{q}. 

 
 \begin{lemma}
 
 \begin{lemma}

-  There exists a renaming process  method that assigns new identifier numbers to
-  processes  $i\in$ \class{p}  and $j  \in$ \class{q}  s.t. $i  \le  j$ provided
+  Il existe un processus de renommage qui effecte un nouvel identifiant aux
+  élément  $i\in$ \class{p}  et $j  \in$ \class{q}  tel que 
+  $i  \le  j$ si et seulement si

   \class{p} $\preceq$ \class{q}.
   \class{p} $\preceq$ \class{q}.

-  \begin{Proof}
-    % We first  define a renaming process  method and later show  that it fulfills
-    % the requirements.
+  \begin{proof}

     
     

-    First  of   all,  let  \class{p_1},   \ldots,  \class{p_l}  be   classes  of
-    $n_1$,\ldots,  $n_l$  elements respectively  that  do  not  depend on  other
-    classes.   Elements of  \class{p_1} are  renamed by  $1$, \ldots,  $n_1$ and
-    elements   of  \class{p_i},   $2  \le   i  \le   l$  are   renamed   by  $1+
-    \Sigma_{k=1}^{i-1}  n_k$, \ldots, $\Sigma_{k=1}^{i}  n_k$.  We  now consider
-    the  classes \class{p_1},  \ldots, \class{p_{l'}}  whose elements  have been
-    renamed and let $m$ be the maximum index of elements of \class{p_1}, \ldots,
-    \class{p_{l'}}.  Given  another class \class{p} that  exclusively depends on
-    some \class{p_i}, $1 \le i \le l'$ and that contains $k$ elements.  Elements
-    of \class{p} are then renamed by $m+1$, \ldots, $m+k$.
-% In the end for remaining classes, i.e. those which do not depend on anything,
-% elements are arbitrarily numbered. 
-    This renaming  process method has then  been applied on  $l'+1$ classes.  It
-    ends since it  decreases the number of elements to  assign a number.  Notice
-    that this process is not determinist.
+    Tout d'abord,  soit  \class{p_1},   \ldots,  \class{p_l}  des   classes 
+    contenant respectivement les éléments $n_1$,\ldots,  $n_l$
+    qui ne dépendent d'aucune autre classe.  
+    Les éléments de  \class{p_1} sont renommés par $1$, \ldots,  $n_1$,
+    les elements  de \class{p_i},   $2  \le   i  \le   l$  sont renommés par 
+    $1+
+    \Sigma_{k=1}^{i-1}  n_k$, \ldots, $\Sigma_{k=1}^{i}  n_k$. 
+    On considère maintenant les classes \class{p_1},  \ldots, \class{p_{l'}} 
+    dont les éléments ont été renommés et soit 
+    $m$ le plus grand indice des elements de \class{p_1}, \ldots,
+    \class{p_{l'}}.
+    Soit une autre classe \class{p} qui dépend exclusivement d'une classe 
+    \class{p_i}, $1 \le i \le l'$ et qui contient $k$ elements. 
+    Les éléments de \class{p} sont renommés par  $m+1$, \ldots, $m+k$.
+    Ce processus a été appliqué sur  $l'+1$ classes. Il se termine 
+    puisqu'il diminue le nombre d'elements auquel il reste 
+    à affecter un numéro. 

 
 

-    We  are then  ready to  prove that  this renaming  method  verifies property
-    expressed in the lemma.  The proof is done by induction on the length $l$ of
-    the longest dependency path between classes.
+    Il reste à montrer que cette méthode de renommage vérifie la propriété 
+    énoncée dans le lemme.
+    Cette preuve se fait par induction sur la taille  $l$
+    du plus grand chemin de dépendance entre les classes.

 
 

-    First, if \class{p} $\preceq$ \class{q} and \class{q} immediately depends on
-    \class{p},  \textit{i.e.} the  longest path  from elements  of  \class{p} to
-    elements of \class{q} has length 1.  Due to the renaming method, all element
-    numbers of \class{q}  are greater than the ones of  \class{p} and the result
-    is established.   Let \class{p} and  \class{q} s.t.  the  longest dependency
-    path from \class{p}  to \class{q} has length $l+1$.   Then there exists some
-    \class{q'} s.t.  \class{q} immediately depends on \class{q'} and the longest
-    dependency path from \class{p} and  \class{q'} has length $l$.  We have then
-    \class{q'}  $\preceq$ \class{q}  and  then for  all  $k$, $j$  s.t. $k  \in$
-    \class{q'}  and $j  \in$  \class{q},  $k \le  j$.   By induction  hypothesis
-    \class{p}  $\preceq$ \class{q'}  and  then for  all  $i$, $k$  s.t. $i  \in$
-    \class{p} and $k \in$ \class{q'}, $i \le k$ and the result is established.
-  \end{Proof}
+    Tout d'abord, si \class{p} $\preceq$ \class{q} et \class{q} 
+    dépend immédiatement de 
+    \class{p},  \textit{i.e.} 
+    le chemin le plus long entre les éléments de   \class{p} et les 
+    elements de \class{q} est de longueur 1.  
+    En raison de la méthode renommage, chaque numéro d'élément
+    \class{q}  est plus grand que tous ceux de  \class{p} et la preuve est 
+    établie.
+    Soit \class{p} et  \class{q} tels que le plus long chemin de dépendance 
+    entre \class{p} et  \class{q} a une longueur de $l+1$.   
+    Il existe alors une classe 
+    \class{q'} telle que \class{q} 
+    dépend immédiatement de  \class{q'} et le chemin de dépendance le
+    plus long entre \class{p} et  \class{q'} a pour longueur $l$. 
+    On a ainsi
+    \class{q'}  $\preceq$ \class{q}  
+    et pour tout  $k$, $j$  tels que $k  \in$
+    \class{q'} et $j  \in$  \class{q},  $k \le  j$.
+    Par hypothèse d'induction, 
+    \class{p}  $\preceq$ \class{q'}  et pour chaque  $i$, $k$  tels que $i  \in$
+    \class{p} et  $k \in$ \class{q'}, $i \le k$
+    et le résultat est établi.
+  \end{proof}

 \end{lemma}
 
 \end{lemma}
 

-It can  be noticed that  the renaming process  is inspired from  \emph{graphs by
-  layer} of Golès and Salinas~\cite{GS08}. It ensures that identifier numbers of
-a layer are greater than all the identifier numbers of any lower layers.
-
-\begin{xpl}
-  We  have \class{1}  $=\{1,2\}$, \class{3}  $=\{3\}$ and  \class{4} $=\{4,5\}$.
-  Processes numbers are already compliant with the order $\preceq$.
-\end{xpl}
+On peut remarquer que ce processus de renommage est inspiré des \emph{graphes 
+  par couches } de Golès et Salinas~\cite{GS08}.

 
 

-\begin{Proof}[of Theorem~\ref{th:cvg}]
+% \begin{xpl}
+%   We  have \class{1}  $=\{1,2\}$, \class{3}  $=\{3\}$ and  \class{4} $=\{4,5\}$.
+%   Processes numbers are already compliant with the order $\preceq$.
+% \end{xpl}

 
 

-  % Since $\preceq$ is a partial order,  [[JFC citer un theoreme qui dit cela ou
-  % le prouver]]  there exists  a renaming process  that assigns  new identifier
-  % number to processes $i\in [p]$ and $j  \in [q]$ s.t. $i \le j$ provided $[p]
-  % \preceq [q]$.
-  % % $i \in [p]$ and $j \in [q]$.
+\begin{proof}[du théorème~\ref{th:cvg}]

 
 

-  The  rest of  the proof  is done  by  induction on  the class  index.  Let  us
-  consider  the first class  \class{b_1} with  $n_1$ elements  \textit{i.e.} the
-  class with the smallest identifiers.
+  Le reste de la preuve est fait par induction sur le numéro de classe. 
+  Considérons la première  classe \class{b_1} de $n_1$ éléments 
+  \textit{i.e.} la classe avec le plus petit identifiant.

 
 

-  By theorem hypotheses, %following the strategy $(S^t)$,
-  synchronous  iterations converge  to the  fixed point  in a  finite  number of
-  iterations. %pseudo periods. % [[JFC : borner m1/n1]].
-  So, all  \emph{source classes}  (independant from any  other class)  will also
-  converge in mixed mode.  Let us suppose now that mixed iterations with uniform
-  delays converge for classes \class{b_1},  \ldots, \class{b_k} in a time $t_k$.
-  By  construction, \class{b_{k+1}}  only depends  on some  \class{b_1}, \ldots,
-  \class{b_k} and \class{b_{k+1}}.  There  exists then a sufficiently large time
-  $t_0$  s.t.  $D^{t_0}_{p_{k+1}p_j}$  is  greater  or equal  to  $t_k$ for  any
-  $p_{k+1} \in$ \class{b_{k+1}} and $p_j \in$ \class{b_j}, $1 \le j \le k$.
+  D'après les hypothèses du  théorème, %following the strategy $(S^t)$,
+  les itérations synchrones convergent vers un point fixe en un nombre 
+  fini d'itérations. %pseudo periods. % [[JFC : borner m1/n1]].
+  Ainsi toutes les  \emph{classes sources} 
+  (indépendantes de toutes les  autres classes) vont aussi converger 
+  dans le mode mixe. 
+  On peut ainsi  supposer que le  mode d'itération mixe avec délais 
+  uniformes fait converger les classes \class{b_1},  \ldots, \class{b_k}
+  en  un temps $t_k$.
+  Par construction, la classe \class{b_{k+1}}  dépend uniquement 
+  de certaines classes de  \class{b_1}, \ldots,
+  \class{b_k} et éventuellement d'elle-même.
+  Il existe un nombre d'iteration suffisamment grand 
+  $t_0$  tel que  $D^{t_0}_{p_{k+1}p_j}$  est suppérieur ou égal à   $t_k$ 
+  pour chaque 
+  $p_{k+1} \in$ \class{b_{k+1}} et $p_j \in$ \class{b_j}, $1 \le j \le k$.

 
 

-  We are  then left with  synchronous iterations of elements  of \class{b_{k+1}}
-  starting with configurations  where all the elements of  \class{b_j}, $1 \le j
-  \le k$, have constant values.  By theorem hypotheses, it converges.
-\end{Proof}
+  Il ne reste donc que des itérations synchrones entre les 
+  elements  of \class{b_{k+1}} en démarant dans des configurations
+  où tous les éléments de  \class{b_j}, $1 \le j
+  \le k$, ont  des valeurs constantes.  
+  D'après les hypothèses du théorème, cela converge.
+\end{proof}