%% Time-stamp: <modifié par Pierre Lescanne le  2 Jan 2003 à 20h07>
%% denotationnelle.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{color}
\input{mes_couleurs}
\usepackage{epsfig}
\usepackage{stmaryrd,amssymb}
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}

\slidesmag{5}
\articlemag{1}


\title{\color{red}{\textit{Communication et mobilité}}}

\author{}

\date{}

\newcommand{\logoLIP}{\includegraphics*[height=0.04\textwidth]{lipllipl.eps}}
\newcommand{\logoENS}{\includegraphics*[height=0.04\textwidth]{liplensl.eps}}
\newcommand{\logos}{\hspace*{12pt}Cours de sémantique --- automne 2002\hfill\logoENS }


\newpagestyle{AvecLogos}%
  {\hfil \thepage \rightmark}
{\logos}


\pagestyle{AvecLogos}

%\pagestyle{empty}

\slidestyle{empty}

\slideframe{}


%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                symobles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{"->"}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\x}{\ensuremath{\textbf{x}}}
\newcommand{\y}{\ensuremath{\textbf{y}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.58em}\lambda}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\T}{\ensuremath{\mathbb{T}}}
\newcommand{\ifthenelse}[3]{\textbf{if~}#1\textbf{~then~}#2\textbf{~else~}#3}
\newcommand{\while}[2]{\textbf{while~}#1\textbf{~do~}#2}
\newcommand{\interp}[3]{\llbracket#1\rrbracket^{#2}_{#3}}
\newcommand{\Ainterp}[1]{\mathcal{A}\llbracket#1\rrbracket}
\newcommand{\Avinterp}[1]{\mathcal{A}v\llbracket#1\rrbracket}
\newcommand{\Binterp}[1]{\mathcal{B}\llbracket#1\rrbracket}
\newcommand{\Cinterp}[1]{\mathcal{C}\llbracket#1\rrbracket}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}
\newcommand{\prepost}[3]{\rouge{\{ #1\}}~#2~\rouge{\{#3\}}}
\renewcommand{\wp}[2]{wp^{`r}\llbracket#1, #2\rrbracket}
\newcommand{\sep}{~\rouge{|}~~}
\newcommand{\ba}[1]{\overline{#1}}
\newcommand{\new}{\rouge{\textsf{new}}~}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        les symboles pour les substitutions explicites
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

\newcommand{\Lift}{\Uparrow\!\!}
\newcommand{\rabeta}{\rasub{\beta}}
\newcommand{\rarabeta}{\rarasub{\beta}}

%%%%%%%%%%%%%%%%%%%% fleches avec souscrit et superscrit %%%%%%%%%%%%%
% par exemple -- B, p --> s'ecrit \rasub{B,p}

\newcommand{\rasub}[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{\rarasup}[1]{\xymatrix @C 15pt {\ar@{>>}[r]^{#1} &}}
\newcommand{\rasupsub}[2]{\xymatrix @C 15pt {\ar@{>}[r]^{#1}_{#2} &}}
\newcommand{\conv}[1]{\xymatrix @C 25pt {\ar@{<<->>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]_{#1} &}}

%%%%%%%%%%%%%%%%%%% -- B --> %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\raB}{\rasub{B}}


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

\newenvironment{displaymathbleu}%
  {\begin{displaymath}\color{blue}}
  {\end{displaymath}}

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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                headings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vertfonce}{\bf\Ovalbox{#1}}
  \end{center}}

 \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\,:\,
   \ifnum\timemm<10 0\fi\number\timemm}}

\begin{document}

%------------------------------------------------------
\begin{slide}
  \maketitle \addtocounter{slide}{-1} \slidepagestyle{empty}
  
  \vfill
  
  \hfill\textit{\footnotesize version du \timestamp}

\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Présentation du problème}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Quoi ?}  Les formalismes actuels savent parler
  \emph{seulement} de
\begin{itemize}
\item de modification et d'allocation de la mémoire (machine à
  registre, etc.)
\item d'appel de fonctions (lambda-calcul)
\end{itemize}
Un des problèmes clés aujourd'hui est celui de la \emph{communication}
et de la \emph{mobilité}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Communication} Il faut décrire les communications.


%                   d
%             b    , \
%            / \ ,    \
%           /  ,\      \
%          / ,   \      \
%         a       c      e


  
  \centerline{ \xymatrix @R 8pt @C 12pt{
      &&&& *++[o][F-]{d} \ar@{-}[ddddllll] \ar@{-}[ddddrrr] \\
      && *++[o][F-]{b} \ar@{-}[dddr]\ar@{-}[dddll] \\
      \\
      \\
      *++[o][F-]{a} &&& *++[o][F-]{c} &&&& *++[o][F-]{e} }}
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Évolution des communications} On peut supprimer des
  communications

%                   d
%             b    , \
%           .  . ,    \
%          .   ,.      \
%         .  ,   .      \
%         a       c      e
  
  \centerline{\xymatrix @R 8pt @C 12pt{
      &&&& *++[o][F-]{d} \ar@{-}[ddddllll] \ar@{-}[ddddrrr] \\
      && *++[o][F--]{b} \ar@{.}[dddr]\ar@{.}[dddll] \\
      \\
      \\
      *++[o][F-]{a} &&& *++[o][F-]{c} &&&& *++[o][F-]{e} }} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Évolution des communications} Des n{\oe}ds peuvent se
  dupliquer

%
%                   d1----d2
%             b    ,      |
%            / \ ,        |
%           /  ,\         |
%          / ,   \        |
%         a       c       e
  \centerline{ \xymatrix @R 8pt @C 12pt{
      &&&& *++[o][F-]{d_1} \ar@{-}[ddddllll] \ar@{-}[rr] &&  *++[o][F-]{d_2}\ar@{-}[ddddr] \\
      && *++[o][F-]{b} \ar@{-}[dddr]\ar@{-}[dddll] \\
      \\
      \\
      *++[o][F-]{a} &&& *++[o][F-]{c} &&&& *++[o][F-]{e} }}
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Systèmes de transition
          étiquetées et bissimulation}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Systèmes de transition étiquetées}%
  \emph{\textbf{Définition :}} Un \emph{système de transitions
    étiquetées} {\color{mauve} labelled transition system}
  (\emph{LTS}) sur \bleu{Act} est une paire \bleu{(\mathcal{Q},
    \mathcal{T})} consistant
\begin{itemize}
\item d'un ensemble \bleu{{\cal Q}} d'états,
\item d'une relation ternaire \bleu{\mathcal{T} ``(= \mathcal{Q} `*
    Act `* \mathcal{Q}}, les \emph{transitions}.
\end{itemize}

\vspace*{5pt}

Si \bleu{(q,`a,q') `: \mathcal{T}} on écrit \bleu{q \rasup{`a} q'} et
on dit que \bleu{q} est la \emph{source} et \bleu{q'} la \emph{cible}.

Si \bleu{q \rasup{`a_1} q_1 \rasup{`a_2} \ldots \rasup{`a_n} q_n}, on
dit que \bleu{q_n} est dérivé de \bleu{q} par \bleu{`a_1`a_2...`a_n}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation} Partant de la source ces deux systèmes ont
  les mêmes transitions, mais ils sont fondamentalement différents.
  \vfill
%  le dessin ci-dessus est grosso modo celui-ci
%
%           p2           q1-->q2
%          /            /
%         /            /
%  p0-->p1           q0
%        \            \
%         \            \
%          p3           q1'-->q3
  \xymatrix{
    &&*++[o][F-]{p_2}&&& *++[o][F-]{q_1}\ar^b[r] &*++[o][F-]{q_2}\\
    *++[o][F-]{p_0}\ar^b[r] &*++[o][F-]{p_1}\ar^b[ur]\ar^c[dr] &&& *++[o][F-]{q_0}\ar^a[ur]\ar^a[dr]\\
    &&*++[o][F-]{p_3}&&& *++[o][F-]{q_1'}\ar^c[r] &*++[o][F-]{q_3} }
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Simulation forte} \emph{\textbf{Définition :}} Si
  \bleu{\mathcal{S}} est une relation binaire sur \bleu{\mathcal{Q}}
  on dit que \bleu{\mathcal{S}} est une \emph{simulation forte}
sur \bleu{(\mathcal{Q}, \mathcal{T})} si %
\ali chaque fois que l'on a \bleu{p\mathcal{S}q} et \bleu{p\rasup{`a}p'} %
\ali alors il existe \bleu{q`:\mathcal{Q}} tel que
\bleu{q\rasup{`a}q'} et \bleu{p\mathcal{S}q'}.  \vfill
% p    S   q
% | a
% v
% p'
%
% ==>
%
%          q
%          |a
%          v
% p'  S    q'
%
\centerline{ \xymatrix @R 10pt @ C 5pt{
    p \ar[dd]^{`a}& \mathcal{S} & q &&&&&&&& q \ar[dd]^{`a}\\
    &&&& \Longrightarrow &\\
    p' &&&&&&&& p' &\mathcal{S} & q' } }
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Bissimulation forte}%
\emph{Définition : } {\color{mauve} bissimulation forte} Une relation
binaire sur \bleu{\mathcal{S}} sur \bleu{\mathcal{Q}} est une
\emph{bissimulation forte} sur \bleu{(\mathcal{Q}, \mathcal{T})} \ali
\bleu{\mathcal{S}} est sa converse sont des simulations fortes.

\vspace*{15pt}

\bleu{p} et \bleu{p} sont \emph{fortement bissimilaire}, ce qu'on
écrit \bleu{p \sim q} s'il existe une bissimulation forte
\bleu{\mathcal{S}} telle que \bleu{p~\mathcal{S}~q}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation, un exemple}
% Le schéma représente le LTS:
% p0 -a-> p1
% p0 -a-> p2
% p1 -a-> p2
% p1 -b-> p0
% p2 -b-> p0
% p2 -a-> p2
%
% q0 -a-> q1
% q1 -a-> q1
% q2 -a-> q1
% q1 -b-> q2
  \centerline{ \xymatrix{
&&*++[o][F-]{p_1}\ar@/_/[ld]_{b}\ar@/^/[dd]^{a} %
&&&& *++[o][F-]{q_0}\ar@/^/[rd]^{a}\\
&*++[o][F-]{p_0}\ar@/_/[ur]_{a}\ar@/^/[dr]^{a} %
&&&&&& *++[o][F-]{q_1}\ar@(ur,dr)[]^{a}\ar@/_/[ld]_{b}\\
&& *++[o][F-]{p_2}\ar@/^/[ul]^{b}\ar@(ur,dr)[]^{a}%
&&&& *++[o][F-]{q_2}\ar@/_/[ru]_{a} }} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation, un exemple} On a \bleu{p_0 \sim q_0}.
  
  Pour le prouver, on exhibe
\begin{displaymathbleu}
  \mathcal{S} = \{(p_0,q_0), (p_0,q_2), (p_1,q_1), (p_2,q_1))\}
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation, un exemple} \vfill
  
  \centerline{ \xymatrix{
&*++[o][F-]{p_1}\ar@/_/[ld]_{b}\ar@/^/[dd]^{a} %
    &&&& *++[o][F-]{q_0}\ar@/^/[rd]^{a}%
    \ar@{.}@/_/[llllld]\\
*++[o][F-]{p_0}\ar@/_/[ur]_{a}\ar@/^/[dr]^{a} %
    &&&&&& *++[o][F-]{q_1}\ar@(ur,dr)[]^{a}\ar@/_/[ld]_{b}%
    \ar@{.}@/_2pc/[llllld]\ar@{.}@/_5pc/[lllllu]\\
& *++[o][F-]{p_2}\ar@/^/[ul]^{b}\ar@(ur,dr)[]^{a}%
    &&&& *++[o][F-]{q_2}\ar@/_/[ru]_{a}%
    \ar@{.}@/^1pc/[lllllu] }}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation} \bleu{\sim} est une relation d'équivalence.
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation} Attention !
  
  Il n'y a pas bissimulation dans \centerline{ \xymatrix{
      &*++[o][F-]{~} \\
*++[o][F-]{p} \ar[ur]^a \ar[dr]^a %
&&&& *++[o][F-]{q} \ar[r]^a & *++[o][F-]{~} \ar[r]^b & *++[o][F-]{~}\\
& *++[o][F-]{~} \ar[r]^b & *++[o][F-]{~} }} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Bissimulation} Attention !
  
  \bleu{p} simule fortement \bleu{q} et \bleu{q} simule fortement
  \bleu{p} .
  
  Autrement dit, il existe \bleu{\mathcal{S}} et \bleu{\mathcal{S}'}
  telles que
\begin{itemize}
\item \bleu{\mathcal{S}} et \bleu{\mathcal{S}'} sont des simulations
  fortes
\item et \bleu{p~\mathcal{S}~q}
\item et \bleu{q~\mathcal{S}'~p},
\item mais \bleu{\mathcal{S}'} n'est pas la converse de
  \bleu{\mathcal{S}}.
\end{itemize}

Il n'y a donc \emph{pas de bissimulation}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{La mobilité}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{quotation}
    La \emph{plasticité} ... désigne la capacité générale du neurone
    et de ses synapses à changer de propriétés en fonction de leur
    état d'activité.  Cette propriété fondamentale va à l'encontre de
    l'impression naïve selon laquelle le cerveau serait une sorte
    d'\emph{automate rigide} constitué exclusivement de «roues et
    engrenages».
  \end{quotation}
  \rightline{{\color{mauve} Jean-Pierre Changeux}, \emph{L'Homme de
      vérité}, Odile Jacob, (2002). p.43}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{quotation}
    Je le répète parce que c'est un point important, le réseau
    cérébral ne s'assemble pas comme on construit un ordinateur avec
    des pièces détachées suivant un plan prédéterminé qui définirait
    exactement la nature et la disposition de chaque circuit et de
    chaque commutateur.
    
    Si tel était le cas, une erreur de détail, même minime dans la
    réalisation de ce programme pourrait avoir des conséquences
    catastrophiques.
  \end{quotation}
  \rightline{{\color{mauve} Jean-Pierre Changeux}, \emph{L'Homme de
      vérité}, Odile Jacob. (2002), p. 284}
\end{slide}
%------------------------------------------------------
\begin{slide}
  Il s'agit d'une vision «\emph{datée}» des ordinateurs.
  
  A l'heure d'Internet, la \emph{reconfiguration} des architectures
  des systèmes informatiques est \emph{continuelle}.
  
  C'est ce que nous allons étudier.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Qu'est-ce que la mobilité ?}  On cherche à abstraire les
  concepts clés de la mobilité,
  
  quand les processus, les programmes, les matériels, les agents
  migrent établissent et reconfigurent des liens.
  
  Trois sortes de vues de la mobilité:
\begin{enumerate}
\item \emph{Les processus se déplacent} dans un espace physique de
  \emph{sites de calcul}.
\item \emph{Les processus se déplacent} dans un espace virtuel de
  \emph{processus liés}.
\item \emph{Les liens se déplacent} dans un espace virtuel de
  \emph{processus liés}.
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Qu'est-ce que la mobilité ?}  Nous allons étudier la
  troisième vue.
\begin{quotation}
  \emph{Les liens se déplacent} dans un espace virtuel de
  \emph{processus liés}.
\end{quotation}

Dans le \bleu{`p-calcul}, il n'y a plus que de liens.

Malgré tout c'est extrêmement puissant.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{vertfonce}{\textit{Un exemple: les téléphones
          mobiles}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les téléphones mobiles} \vfill \centerline{ \xymatrix @ C
    10pt @ R 15pt{
      \bigodot \ar@{~}[rd]&& \bigodot \ar@{~}[rd]&& \bigotimes \ar@{~}[ld]&& \bigodot\ar@{~}[ld]\\
      & *++[o][F-]{T} \ar@{-}[rd]&& *++[o][F-]{T} \ar@{-}[ld]&&*++[o][F-]{T}\ar@{-}[llld]&&&\\
      \ar@{.}[r]&\ar@{-}[r]&*++[o][F-,]{CONTROL}
      \ar@{-}[r]&\ar@{.}[r]& }}
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les téléphones mobiles} \vfill \centerline{ \xymatrix @ C
    10pt @ R 15pt{
      \bigodot \ar@{~}[rd]&& \bigodot \ar@{~}[rd]&& \bigotimes \ar@{~}[rd]&& \bigodot\ar@{~}[ld]\\
      & *++[o][F-]{T} \ar@{-}[rd]&& *++[o][F-]{T} \ar@{-}[ld]&&*++[o][F-]{T}\ar@{-}[llld]&&&\\
      \ar@{.}[r]&\ar@{-}[r]&*++[o][F-,]{CONTROL}
      \ar@{-}[r]&\ar@{.}[r]& }}
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} \vfill
% Car --- talk1 --- Trans
% Car --- switch1 --- Trans
%
% Tans --- lose1 --- Contro
% Trans --- gain1 --- Control
%
% Tans --- lose1 --- Control
% Trans --- gain1 --- Control
%
% Itrans --- lose2 --- Control
% Itrans --- gain2 --- Control
%
%
  \centerline{ \xymatrix @ C 10pt @ R 15pt{
      &*++[F=]{{\scriptsize Car}} \ar@{-}@<1ex>[ld]^{talk_1}\ar@{-}@<-1ex>[ld]_{switch_1}\\
      *++[o][F-]{\rouge{Trans}}
\ar@{-}@<1ex>[rrd]^{gain_1}\ar@{-}@<-1ex>[rrd]_{lose_1}%
&&&& *++[o][F-]{Itrans}\ar@{-}@<1ex>[lld]^{gain_2}\ar@{-}@<-1ex>[lld]_{lose_2}\\
&&*++[F-,]{{\scriptsize CONTROL}} }} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} \vfill \centerline{
    \xymatrix @ C 10pt @ R 15pt{
      &*++[F=]{{\scriptsize Car}} \ar@{-}@<1ex>[rrrd]^{talk_2}\ar@{-}@<-1ex>[rrrd]_{switch_2}\\
      *++[o][F-]{Itrans}
\ar@{-}@<1ex>[rrd]^{gain_1}\ar@{-}@<-1ex>[rrd]_{lose_1}%
&&&& *++[o][F-]{\rouge{Trans}}\ar@{-}@<1ex>[lld]^{gain_2}\ar@{-}@<-1ex>[lld]_{lose_2}\\
&&*++[F-,]{{\scriptsize CONTROL}} }} \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} Faisons l'hypothèse
  qu'il n'y a que deux transmetteurs
\begin{itemize}
\item un \emph{transmetteur actif }
\item et un \emph{transmetteur inactif}
\end{itemize}


Le transmetteur actif a la forme
\begin{displaymathbleu}
  Trans<talk_1, switch_1,gain_1,lose_1>
\end{displaymathbleu}
dont les liens courants sont les paramètres de transmission.  \vfill
Les processus sont notés par des identificateurs commençant par une
majuscule.

Les canaux sont notés par des identificateurs commençant par une
minuscule.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} La voiture
  \emph{parle} au transmetteur sur le canal \bleu{talk_1}.
  
  Mais la \emph{centrale de contrôle} peut demander à tout instant à
  la voiture par l'intermédiaire du transmetteur de \emph{commuter
    vers un autre transmetteur}, dont elle lui transmet les
coordonnées: %
\ali c'est-à-dire les liens pour communiquer avec lui.

Pour cela,la centrale de contrôle communique avec la transmetteur par
le canal \bleu{lose_1}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} On a donc deux
  équations:

\begin{scriptsize}
\begin{eqnarraybleu}
  Trans(talk, switch, gain, lose) &"={^{def}}"& talk . Trans<talk,  switch, gain,  lose>\\
  && + lose(t,s) . \overline{switch}<t,s> . Itrans<gain, lose>\\
  Itrans(gain,lose) &"={^{def}}"& gain(t,s) . Trans<t, s, gain, lose>
  .
\end{eqnarraybleu}
\end{scriptsize}

Les interactions \emph{transmettent} des \emph{noms de canaux} dans
leurs messages.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} Une action
  \emph{positive} comme \bleu{lose(s,t)} reçoit des noms.
  
  Une action \emph{négative} comme \bleu{\overline{switch}<t,s>}
  envoie des noms.
  
  \bleu{lose(s,t)} est un \emph{lieur}, il introduit des noms locaux
  comme \bleu{s} et \bleu{t}.
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} Une action
  \emph{positive} comme \bleu{lose(s,t)} reçoit des noms.
  
  Une action \emph{négative} comme \bleu{\overline{switch}<t,s>}
  envoie des noms.
  
  \bleu{lose(s,t)} est un \emph{lieur}, il introduit des noms locaux
  comme \bleu{s} et \bleu{t}.
  
  \vspace*{10pt}
  
  Les \emph{parenthèses} \bleu{(...)} servent à lier des variables de
  noms de canaux reçus.
  
  Les \emph{chevrons} \bleu{<...>} servent à dénoter des tuples de
  noms de canaux que l'on envoie.

  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} %
  \bleu{Control} qui dit à \bleu{Trans} de lâcher (lose) une voiture
  doit lui transmettre les nouveaux canaux pour émettre.
  
  Il doit transmettre les mêmes canaux au transmetteur inactif pour
  lui permettre d'entrer en contact avec la voiture.
\begin{scriptsize}
\begin{eqnarraybleu}
  Control_1 &"={^{def}}"& \overline{lose_1}<talk_2,swicth_2>
  . \overline{gain_2}<talk_2,switch_2>. Control_2\\
  Control_2 &"={^{def}}"& \overline{lose_2}<talk_1,swicth_1> .
  \overline{gain_1}<talk_1,switch_1>. Control_1
\end{eqnarraybleu}
\end{scriptsize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} La \emph{voiture}
  (\emph{car}) peut
\begin{itemize}
\item ou bien \emph{parler} (\emph{talk})
\item ou bien \emph{échanger} (\emph{switch}) une nouvelle paire de
  canaux.
  \begin{scriptsize}
 \begin{eqnarraybleu}
   Car(talk, switch) &"={^{def}}"& \overline{talk}. Car<talk, switch>
   + switch(t,s) . Car<t,s>.
  \end{eqnarraybleu}
\end{scriptsize}
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} Comment faire de tout
  cela un processus?
\begin{scriptsize}
\begin{eqnarraybleu}
  System_1 &"={^{def}}"&\new talk_1, switch_1, gain_1,
  lose_1, talk_2, switch_2, gain_2, lose_2 \\
  && \quad (Car<talk_1, switch_1> ~|~ Trans_1 ~|~ Itrans_2 ~|~
  Control_1)
\end{eqnarraybleu}
\end{scriptsize}
avec les fonctions auxiliaires
\begin{scriptsize}
\begin{eqnarraybleu}
  Trans_i &"={^{def}}"& Trans<talk_i, switch_i, gain_i, loase_i>\\
  Itrans_i &"={^{def}}"& Itrans<gain_i, lose_i>
\end{eqnarraybleu}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le téléphone mobile à un seul mobile} %
  À l'aide du \emph{$`p$-calcul}, on mettra en évidence que ce
  protocole est correct.
  
  C'est-à-dire que les passage de «relais» et les attributions des
  canaux de communication se font bien.
  
Autrement dit que l'on a bien:
\begin{scriptsize}
\begin{eqnarraybleu}
  System_1 &\rasup{*}& System_2
\end{eqnarraybleu}
\end{scriptsize}
où \bleu{System_2} est juste \bleu{System_1} avec les indices
permutés:
\begin{scriptsize}
\begin{eqnarraybleu}
  System_2 &"={^{def}}"&\new talk_2, switch_2, gain_2,
  lose_2, talk_1, switch_1, gain_1, lose_1 \\
  && \quad (Car<talk_2, switch_2> ~|~ Trans_2 ~|~ Itrans_1 ~|~
  Control_2).
\end{eqnarraybleu}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{mauve}{\textit{Le $`p$-calcul}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les actions} %
  \begin{eqnarraybleu}
    `p &::=& x(y) \qquad \verdir{\textrm{reçoit \bleu{y} sur
        \bleu{x}}}\\
    && \ba{x}<y> \qquad \verdir{\textrm{envoie \bleu{y} sur
        \bleu{x}}}\\
    && `t \qquad \verdir{\textrm{action inobservable}}
  \end{eqnarraybleu}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le $`p$-calcul} %
  \begin{eqnarraybleu}
    P &::=& \sum_{i`:I} `p_i.P_i \sep P_1 | P_2 \sep \new a P \sep !P
  \end{eqnarraybleu}
  \bleu{\sum_{i`:I} `p_i.P_i } est une \emph{somme} \ali dans laquelle
  les \bleu{P_i} sont \emph{gardés} par les \bleu{`p_i}.
  
  \bleu{0} est la somme vide qui représente l'action vide.
  
  Nous l'omettons après une action.
  
  On écrit \bleu{\ba{x}<y>} au lieu de \bleu{\ba{x}<y> . 0}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La réplication} %
  \bleu{|} s'appelle la \emph{composition concurrente}.
  
  \bleu{!P} s'appelle la \emph{réplication} ou le \emph{bang}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple} %
  \begin{eqnarraybleu}
    P & = &\new z ((\ba{x}<y> + z(w).\ba{w}<y>) ~|~ x(u).\ba{u}<v> ~|~
    \ba{x}<z>).
  \end{eqnarraybleu}
  \bleu{x}, \bleu{y} et \bleu{v} sont les seuls noms libres dans
  \bleu{P}.
  
  Des paires positives et négatives qui utilisent le même canal sont
  dites être des \emph{paires complémentaires}.
  
  \bleu{\ba{x}<y>} et \bleu{ x(u)} sont complémentaires.
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Redex et déclenchement} %
  Si une paire complémentaire est formée de deux actions situées
  \verdir{dans des sommes différentes} et si elles sont \verdir{non
    gardées} alors elles forment un \emph{redex}.
  
  Le \emph{déclenchement} de ce redex constitue une \emph{réaction}
  \bleu{P "->" P'} qui met en {\oe}uvre une substitution ici
  \bleu{\{y/u\}}.
  
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Redex et déclenchement} %
  Si une paire complémentaire est formée de deux actions situées
  \verdir{dans des sommes différentes} et si elles sont \verdir{non
    gardées} alors elles forment un \emph{redex}.
  
  Le \emph{déclenchement} de ce redex constitue une \emph{réaction}
  \bleu{P "->" P'} qui met en {\oe}uvre une substitution ici
  \bleu{\{y/u\}}.
  
  \vfill La règle principale est

\begin{displaymathbleu}
  (x(y).Q + M) ~|~ (\ba{x}<z> .R + N) "->" \{z/y\}Q ~|~ R
\end{displaymathbleu}
Les autres règles sont contextuelles.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple} %
  \bleu{P} a deux redex
\begin{itemize}
\item la paire \bleu{\ba{x}<y>}, \bleu{ x(u)}
\item la paire \bleu{ x(u)}, \bleu{\ba{x}<z>}
\end{itemize}

Deux réactions possibles
\begin{itemize}
\item \bleu{P "->" P_1}
\item \bleu{P "->" P_2}
\end{itemize}
avec
\begin{eqnarraybleu}
  P_1 &=& \new z (0 ~|~ \ba{y}<v> ~|~ \ba{x}<z>)\\
  P_2 &=& \new z ((\ba{x}<y> + z(w).\ba{w}<y>) ~|~ \ba{z}<v> ~|~ 0).
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Un exemple} %
  Il n'y a plus de redex dans \bleu{P_1}.
  
  Et il y a la paire \bleu{z(w)} et \bleu{\ba{z}<v>} dans \bleu{P_2}.
  
  Nous avons \bleu{P_2"->" P_3} où
\begin{eqnarraybleu}
  P_3 &=& \new z (\ba{v}<y> ~|~ 0 ~|~ 0).
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Congruence de processus} %
  \bleu{\approxeq} est une relation d'équivalence telle que
\begin{displaymathbleu}
  \prooftree
  P \approxeq Q \\
  \justifies `p . P + M \approxeq `p . Q + M \endprooftree \qquad
  \qquad \prooftree
  P \approxeq Q \\
  \justifies \new x. P \approxeq \new x Q \endprooftree
\end{displaymathbleu}

\begin{displaymathbleu}
  \prooftree
  P \approxeq Q \\
  \justifies P ~|~ R \approxeq Q ~|~ R \endprooftree \qquad \qquad
  \prooftree
  P \approxeq Q \\
  \justifies R ~|~ P \approxeq R ~|~ Q \endprooftree \qquad \qquad
  \prooftree
  P \approxeq Q \\
  \justifies ! P \approxeq ! Q\endprooftree
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Congruence structurelle} %
  La congruence structurelle \bleu{`=} est définie comme la plus petit
  congruence qui contient:
\begin{itemize}
\item l'alpha-conversion,
\item l'associativité et la commutativité dans les sommes,
\item pour \bleu{|}, l'associativité, la commutativité, la neutralité
  de \bleu{0}, \\% \bleu{P ~|~ (Q ~|~ R) `= (P ~|~ Q) ~|~ R}
  \quad\bleu{P ~|~ Q `= Q ~|~ P} \quad\bleu{P ~|~ 0 `= P},
\item \bleu{\new x (P ~|~ Q) `= P ~|~ \new x Q} \qquad if \bleu{x\notin fn(P)},\\
  \bleu{\new 0 `= 0}, \qquad \bleu{\new x ~ y ~ P`= \new y~x~P},
\item \bleu{!P `= P ~|~ !P},
\end{itemize} 

\bleu{fn(P)} est l'ensemble de \emph{noms libres} de \bleu{P}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Congruence structurelle} %
  \bl{ \centerline{$\new z ((\ba{x}<y> + z(w).\ba{w}<y>) ~|~
      x(u).\ba{u}<v> ~|~ \ba{x}<z>)$} \centerline{$`=$}
    \centerline{$x(u).\ba{u}<v> ~|~ \new z (( z(w).\ba{w}<y> +
      \ba{x}<y>) ~|~\ba{x}<z>)$} }
\begin{eqnarraybleu}
  \new z (\ba{v}<y> ~|~ 0 ~|~ 0) &`=& \ba{v}<y>.
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Forme standard} %
  Un processus
\begin{displaymathbleu}
  \new \vec{a} (M_1 ~|~ ...~|~M_m ~|~ !Q_1 ~|~ ...  !Q_n)
\end{displaymathbleu}
est en \emph{forme standard}
\begin{itemize}
\item si aucun des \bleu{M_i} n'est une somme nulle
\item et si chaque \bleu{Q_j} est lui-même une forme standard.
\end{itemize}
\vfill Chaque processus est équivalent à une forme standard.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Relation de réaction} %
  \begin{displaymathbleu}
    \prooftree \justifies `t . P + M "->" P \using {\color{brunfonce}
      TAU} \endprooftree
  \end{displaymathbleu}
  \begin{displaymathbleu}
    \prooftree \justifies (x(y).P + M) ~|~ (\ba{x}<z> .Q + N) "->"
    \{z/y\}P ~|~ Q \using {\color{brunfonce} REACT} \endprooftree
  \end{displaymathbleu}
  \begin{displaymathbleu}
    \prooftree P "->" P' \justifies P ~|~ Q "->" P' ~|~ Q \using
    {\color{brunfonce} PAR} \endprooftree \qquad \prooftree P "->" P'
    \justifies \new x P "->" \new x P' \using {\color{brunfonce} RES}
    \endprooftree
   \end{displaymathbleu}
  \begin{displaymathbleu}
    \prooftree
    P "->" P' %
    \justifies Q "->" Q' %
    \using {\color{brunfonce} STRUCT} \qquad \textrm{\color{black}
      si~} P`=P \textrm{\color{black} ~et~} Q`=Q.  \endprooftree
  \end{displaymathbleu}
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La récursivité} %
  Le $`p$-calcul ne contient pas de définitions récursives.
  
  Mais on peut facilement les simuler.
  
  Supposons que l'on ait la définition~\footnote{Je prends une
    fonction à un seul paramètre, mais ça se généralise.}
\begin{eqnarraybleu}
  A(x) &=& Q_A \quad \textrm{\color{black} où} \quad Q_A = ... A<u>
  ... A<v> ...
\end{eqnarraybleu}
qui apparaît dans
\begin{eqnarraybleu}
  P &=& ... A<y> ... A<z> ...
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La récursivité} %
  On transforme la définition en utilisant les réplications.
\begin{enumerate}
\item On utilise un nouveau nom, disons \bleu{a}, pour \bleu{A}.
\item On remplace chaque invocation du processus \bleu{R} %
  \ali par  l'invocation du processus \bleu{\widehat{R}} %
  \\ obtenu en remplaçant chaque occurrence de \bleu{A<w>} par
  \bleu{\ba{a}<w>}.
\item On remplace \bleu{P} par
  \begin{eqnarraybleu}
    \widehat{\widehat{P}} &=& \new a ~(\widehat{P} ~|~ !a(x) .
    \widehat{Q_A})
  \end{eqnarraybleu}
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La récursivité} %
  Par exemple,
\begin{small}
\begin{eqnarraybleu}
  Car(talk, switch) &"={^{def}}"& \overline{talk}. Car<talk, switch> +
  switch(t,s) . Car<t,s>.
  \end{eqnarraybleu}
\end{small}
et
\begin{scriptsize}
\begin{eqnarraybleu}
  System_1 &"={^{def}}"&\new talk_1, switch_1, gain_1,
  lose_1, talk_2, switch_2, gain_2, lose_2 \\
  && \quad (Car<talk_1, switch_1> ~|~ Trans_1 ~|~ Itrans_2 ~|~
  Control_1)
\end{eqnarraybleu}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  se transforme en\footnote{J'utilise des canaux à plusieurs
    paramètres.}
\begin{scriptsize}
\begin{eqnarraybleu}
  System_1 &"={^{def}}"& \new car ~ \\
  && \new talk_1, switch_1, gain_1,
  lose_1, talk_2, switch_2, gain_2, lose_2 \\
  && \quad (\ba{car}<talk_1, switch_1> ~|~ Trans_1 ~|~ Itrans_2 ~|~
  Control_1\\
  &&~|~ ! car(lose,swicth) .  (\overline{talk}. \ba{car}<talk, switch>
  + switch(t,s) . \ba{car}<t,s>)).
\end{eqnarraybleu}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Tampons ou Buffers}%
Un buffer qui conserve une valeur peut se représenter par les
équations:
\begin{eqnarraybleu}
  B(l,r) &"={^{def}}"& l(x) . C<x,l,r>\\
  C(x,l,r) &"={^{def}}"& \ba{r}<x> . B<l,r>
\end{eqnarraybleu}
Tant que la valeur n'est pas réclamée sur le canal \bleu{r} la valeur
transmise sur la canal \bleu{l} (notée intérieurement \bleu{x}) est
conservée.

Une fois cette valeur transmise, le buffer est prêt pour un autre
stockage.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Tampons ou Buffers}%
Supposons que le processus appelant soit:
\begin{displaymathbleu}
  ... B<i,o> ... C<x,i,o> ...
\end{displaymathbleu}

Il se code en $`p$-calcul sous la forme:
\begin{eqnarraybleu}
  &\new b, c~ &... (\ba{b}<l,r> ... \ba{c}<x,l,r> ... \\
  && ~|~ !b(i,o).i(x).\ba{c}<x,i,o> ~|~ !c(y,e,s). \ba{e}<y> .
  \ba{b}<e,s>) .
\end{eqnarraybleu}
7 variables sont liées dans cette formule: \bleu{b, c, i, o, y, e, s}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Enchaînement de buffers}%
Pour allonger la capacité d'un buffer, on peut en «lier» plusieurs
\begin{displaymathbleu}
  B_1\frown B_2 \ldots \frown B_n
\end{displaymathbleu}

L'opération \bleu{\frown} se définit sur des processus, par exemple si
\bleu{F} et \bleu{G} sont d'arité 2 (notés \bleu{F:2} et \bleu{G:2}).
\begin{eqnarraybleu}
  (F\frown G)<l,r> & "={^{def}}" & \new m~(F<l,m> ~|~ G<m,r>).
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Enchaînement de buffers}%
Avec \bleu{B:2} et \bleu{C:3} on peut écrire \bleu{C<x>:2} et aussi:
\begin{eqnarraybleu}
  J &=& C<x_1> \frown B\frown C<x_2>.
\end{eqnarraybleu}
où
\begin{eqnarraybleu}
  J<l,r> &=& \new b~m_1~m_2~ (\ba{c}<x_1,l,m_1> \quad|\quad
  \ba{b}<m_1,m_2> |
  \ba{c}<x_1,m_2,r> \\
  &~|~& !b(i,o).i(x).\ba{c}<x,i,o> \quad|\quad !c(y,e,s). \ba{e}<y> .
  \ba{b}<e,s>)
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{vertfonce}{\textit{Systèmes simples}} }
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Systèmes simples}%
Un système en forme standard
\begin{eqnarraybleu}
  P &`=& \new \vec{z} (M_1 ~|~...~|~M_m ~|~ !N_1 ~|~...~|~ !N_n)
\end{eqnarraybleu}
est \emph{simple} si
\begin{description}
\item[S1] \bl{P} est structurellement équivalent à un système dans
  lequel toutes les réplications sont des sommes.
\item[S2] Aucun \bleu{M_i}, ni aucun \bleu{N_j} ne contient de
  réplication.
\item[S3] Aucun \bleu{M_i}, ni aucun \bleu{N_j} ne contient de
  composition concurrente.
\end{description}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Systèmes simples}%
La simplicité est stable par réaction.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Systèmes simples}%
Les buffers sont simples.

On voit que
\begin{eqnarraybleu}
  \new b~m_1~m_2&& (\ba{c}<x_1,l,m_1> ~|~ \ba{b}<l,r> ~|~
  \ba{c}<x_1,m_2,r> \\
  &&~|~ !b(i,o).i(x).\ba{c}<x,i,o> ~|~ !c(y,e,s). \ba{e}<y> .
  \ba{b}<e,s>)
\end{eqnarraybleu}
est simple.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriétés de systèmes}%
On veut prouver des propriétés sur les systèmes.

Ainsi dans le système des téléphones mobiles on veut pouvoir s'assurer
que la centrale de contrôle n'a pas attribué le même canal de
communication à plus d'un mobile\footnote{Ça m'est arrivé sur un
  téléphone fixe, c'est désagréable !}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Propriétés de systèmes}%
Dans un système complexe ça peut être vraiment compliqué.

On veut pourvoir mettre cela en évidence à travers des propriétés
syntaxiques.

Et on veut pouvoir prouver des théorèmes à propos des systèmes.

L'exigence de \emph{simplicité} est un cadre qui peut permettre de
prouver sans trop de contorsion des théorèmes suffisamment riches.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Prise}%
\bleu{P} \emph{a une prise sur} \bleu{x} si \bleu{P} a une occurrence
libre de \bleu{x} dans une action de la forme \bleu{\ba{x}<\ldots>} ou
\bleu{\ba{v}<\ldots x\ldots>}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Prise unique}%

\emph{Définition :} \verdir{prise unique}

Si \bleu{P} est un système simple en forme standard,%
\ali on dit que \bleu{P} a une prise unique sur \bleu{x}
\begin{itemize}
\item si au plus un seul \bleu{M_i} a une prise sur \bleu{x}
\item et aucun \bleu{N_j} n'a une prise sur \bleu{x}.
\end{itemize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Abandon de x}%

\emph{Définition :} \verdir{abandon de \bleu{x}}

Un terme \bleu{P} \emph{abandonne} \bleu{x} si dans chaque terme de la
forme
\bleu{a<\vec{u} x \vec{v}>. Q}%
\begin{itemize}
\item ni \bleu{\vec{u}}, ni \bleu{\vec{v}} ne contiennent \bleu{x},
\item \bleu{Q} n'a pas prise sur \bleu{x},
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Préservation de la prise unique}%

Soit \bleu{P} un système simple qui satisfait les conditions suivantes
pour un certain \bleu{x}
\begin{enumerate}
\item \bleu{P} a une prise unique sur \bleu{x},
\item \bleu{P} abandonne \bleu{x},
\item pour chaque sous-terme de la forme \bleu{z(\vec{y}).Q}, %
  \ali\bleu{Q} abandonne chacun des \bleu{y\in\vec{y}}
\end{enumerate}

\vspace*{10pt}

Si \bleu{P "->" P'}, alors \bleu{P'} est simple et satisfait 1., 2. et
3.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Démonstration du théorème}%
On la fait dans la cas monadique.

On suppose
\begin{eqnarraybleu}
  P &`=& \new \vec{z} (M_1 ~|~...~|~M_m ~|~ !N_1 ~|~...~|~ !N_n)
\end{eqnarraybleu}
Sans nuire à la généralité on peut supposer que l'interaction se fait
entre \bleu{M_1} et \bleu{M_2}.

Par exemple, on peut «décomposer» \bleu{!N_j} en \bleu{N_j~|~!N_j} et
prétendre que \bleu{N_j} est \bleu{M_1} ou \bleu{M_2}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Démonstration du théorème}%
Donc
\begin{eqnarraybleu}
  M_1 &`=& ...+\ba{u}<v> \new \vec{z_1} M'_1\\
  M_2 &`=& ...+ u(w).  \new \vec{z_2} M'_2
\end{eqnarraybleu}
et
\begin{eqnarraybleu}
  P' &`=& \new \vec{z_1}~\vec{z_2}(M'_1 ~|~ \{v/w\} M'_2 ~|~ ...~|~M_m
  ~|~ !N_1 ~|~...~|~ !N_n)
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Démonstration du théorème}%
\verdir{\bleu{P'} a une prise unique}

On va montrer qu'il y a moins de prises sur \bleu{x} dans \bleu{M'_1
  ~|~ \{v/w\} M'_2} %
\ali qu'il y en a dans \bleu{M_1 ~|~M_2}.

\begin{itemize}
\item \bleu{M'_1} a moins de prises sur \bleu{x} que \bleu{M_1},

\item \bleu{\{v/w\} M'_2} ne crée pas plus de prises sur  \bleu{x}.
 \begin{itemize}
 \item Si \bleu{v\neq x} alors \bleu{\{v/w\} M'_2} et \bleu{M_2} ont
   les mêmes prises sur \bleu{x},
 \item Si \bleu{v=x} alors l'unique prise de \bleu{x} dans \bleu{P}
   est \bleu{\ba{u}<v>. \new \vec{z_1} M'_1}, mais d'après la
   propriété d'abandon, \bleu{M_1'} n'a pas de prise sur \bleu{x}.\\
 %  Et d'après la simplicité \bleu{u(w).  \new \vec{z_2} M'_2} n'est
%   qu'une suite d'actions élémentaires. \\
 Donc  \bleu{\{v/w\}
     M'_2} (alias \bleu{\{x/w\} M'_2}) peut avoir  prise sur
   \bleu{x} en préservant l'unicité de la prise.
  \end{itemize}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Démonstration du théorème}%
\verdir{\bleu{P'} abandonne \bleu{x}}

L'abandon est une propriété sur des sous-termes qui ne peut changer
que si les dits sous-termes changent.

Donc, clairement, seul \bleu{\{v/w\} M'_2} et encore dans le cas où
\bleu{v=x} pourrait ne pas abandonner \bleu{x}.

Supposons donc que \bleu{\{x/w\} M'_2} n'abandonne pas \bleu{x}.

Cela veut dire que \bleu{M'_2} n'abandonne pas \bleu{w},

autrement dit que \bleu{u(w). \new \vec{z_2} M'_2} contredit la
condition (3).

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Démonstration du théorème}%
\verdir{Condition (3)}

La condition (3) ne peut être violée dans \bleu{P'} que dans
\bleu{\{v/w\} M'_2}.

Supposons que ce soit dans \bleu{z'(y) . \{v/w\} Q} (\bleu{z'} peut
être \bleu{w} ou non).

Alors elle est violée dans \bleu{z(y) . Q} (\bleu{z} est \bleu{v} si
\bleu{z'} est \bleu{w} et est \bleu{z'} sinon).

Ce qui contredit le fait que \bleu{P} satisfait (3).


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

  
  Et voilà démontré un théorème dans le $`p$-calcul !

\end{slide}
%======================================================
\end{document}
% LocalWords:  labelled system LTS Act Changeux Jacob reconfiguration d'abandon
% LocalWords:  réplication réplications n'abandonne pt ddddllll ddddrrr dddr ds
% LocalWords:  dddll rr ddddr ur dr dd bissimilaire ld rd ul ru llllld pc llld
% LocalWords:  lllllu L'Homme p-calcul vertfonce CONTROL talk Trans switch Tans
% LocalWords:  lose Contro Control Itrans rrd lld rrrd tuples i.P l'omettons fn
% LocalWords:  l'alpha-conversion Buffers buffer buffers
