%% Time-stamp: <modified on  9 Nov 2004 at 18:02 by Pierre Lescanne>
%% operationnelle.tex
\documentclass[%
  slidesonly,%  Pour sortir les transparents seuls
%  semrot,%      Permettre des rotations eventuelles
  semhelv,%    Helvetica
  a4%           A4 paper
  ]{seminar}

\usepackage{fancybox}
\usepackage[francais]{babel}
\usepackage[latin1]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{color}
\usepackage{epsfig}
%\usepackage{stmaryrd,amssymb}
%\usepackage[dvips]{graphicx}
%\usepackage{amsmath}            % nice mathematics
\usepackage[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}


%\input{macros}

%\def\printlandscape{\special{landscape}}    % pour sortir en landscape
                                            % avec dvips

%\rotateheaderstrue       % si tu combines slide et slide*

\slidesmag{5}
\articlemag{1}



\title{\color{red}{\textit{Sémantiques opérationnelles du lambda-calcul}}}

\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 2004\hfill\logoENS }


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


\pagestyle{AvecLogos}

%\pagestyle{empty}

\slidestyle{empty}

\slideframe{}   

%--- couleurs ----
\input{mes_couleurs}
\definecolor{cyanp}{cmyk}{.7,.6,0,0}

\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{\envdot}{\bullet}
\newcommand{\cm}[2]{\langle #1 \parallel #2\rangle}
\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{\perluette}{&}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\xx}{\ensuremath{\texttt{x}}}
\newcommand{\xgc}{\ensuremath{\texttt{x}_{gc}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\T}{\ensuremath{{\cal T}}}
\newcommand{\Fof}[1]{\F\llbracket#1\rrbracket}
\newcommand{\Fv}{\ensuremath{\F_v}}
\newcommand{\Fvof}[1]{\Fv\llbracket#1\rrbracket}
\newcommand{\nom}{\downarrow_n}
\newcommand{\valeur}{\downarrow_v}
\newcommand{\sep}{~\rouge{,}~~}
\newcommand{\Ia}{\ensuremath{I_{`a}}}
\newcommand{\Ja}{\ensuremath{J_{`a}}}
\newcommand{\interp}[3]{\llbracket#1\rrbracket^{#2}_{#3}}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                les symboles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> 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 15pt {\ar@{<<->>}[r]_{#1} &}}
\newcommand{\subar}[1]{\xymatrix @C 15pt {\ar@{<-}[r]_{#1} &}}

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

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

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


\newcommand{\heading}[1]{%
{\color{cyanp}\bf\large #1}{\color{yellow}\\\rule{\textwidth}{2pt}}
}
%\newcommand{\heading}[1]{%      % ca c'est des commandes a moi
%  \begin{center}                % mais ca peut t'interesser
%    \large\bf
%    \color{cyanp}{\shadowbox{#1}}%
%  \end{center}
%  \markright{#1}
%  \vspace{1ex minus 1ex}}

\newcommand{\subheading}[1]{%
  \begin{center}
    \color{vert}{\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

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

\newenvironment{eqnarraybleu}%
  {\begin{color}{blue}\begin{eqnarray*}}
  {\end{eqnarray*}\end{color}}
\newenvironment{displaymathbleu}[1]{\begin{displaymath}\color{blue}#1}{\end{displaymath}}
\newenvironment{mathbleu}[1]{$\color{blue}#1}{$}


\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{brunfonce}{\textit{\Huge Les substitutions explicites}}}
\end{center}
\end{slide}
%%----------------------------------------------------------------------
\begin{slide}

\begin{it}
\begin{quotation}
The synthetic theory of combinators
``gives the \brunir{ultimate analysis} of substitutions in terms of a system of
\brunir{extreme simplicity}. 

The theory of lambda-conversion is intermediate in character between
synthetic theories and ordinary logic ... and it has the advantage of
\brunir{departing less radically from our intuition}.''
\end{quotation}
\end{it}

\textcolor{magenta}{
\begin{footnotesize}
\rightline{\parbox{5cm}{Curry and Feys,\\
in the introduction of\\
{\sl Combinatory Logic}, (1958) p.~6}}
\end{footnotesize}
}
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Qu'est-ce que la contraction $\beta$?}

La définition habituelle de la  contraction $\beta$ en $`l $-calcul est


\[C[\![\bl{(`l x . M)\ P}]\!] "->" C[\![\bl{M[P/x]}]\!].\]

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

\heading{Qu'est-ce qu'une substitution?}

La substitution \rouge{$[\_ / \_ ]$} est une  opération atomique
\ali qui consiste à \brunir{remplacer} une variable par un terme.

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

\heading{Qu'est-ce qu'une substitution?}

La substitution \rouge{$[\_ / \_ ]$} est une  opération atomique
\ali qui consiste à \brunir{remplacer} une variable par un terme.

La substitution est une opération \brunir{complexe}
\begin{itemize}
\item dans son \verdir{calcul} \ali la même notation peut évoquer une
  opération coûteuse \ali ou une opération bon marché, \\ ça n'est pas
  réaliste,
  
\item et dans son \verdir{implantation}, \ali les \brunir{captures} sont difficiles à
  prendre en compte.
\end{itemize}

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

\heading{Qu'est-ce qu'une substitution?}

Traditionnellement, la \brunir{substitution} n'est pas définie dans la
\brunir{théorie}, \ali mais dans l'\brunir{épithéorie}.  

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

\heading{Qu'est-ce qu'une substitution?}

Traditionnellement, la \brunir{substitution} n'est pas définie dans la
\brunir{théorie}, \ali mais dans l'\brunir{épithéorie}.  

\vfill
\verdir{Pourquoi ne pas en faire un citoyen de première classe ?}
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Qu'est-ce qu'une substitution?}

Traditionnellement, la \brunir{substitution} n'est pas définie dans la
\brunir{théorie}, \ali mais dans l'\brunir{épithéorie}.  

\vfill
\verdir{Pourquoi ne pas ne faire un citoyen de première classe ?}

\verdir{Pourquoi ne pas l'internaliser?}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    \textbf{\LARGE {\color{vertfonce}Le calcul \lxgc}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  On fait un usage intensif de la \brunir{convention de Barendregt sur
    les variables.}

  \vspace*{20pt} 
  
  \fbox{\parbox{9cm}{Dans un même contexte, une même variable n'est
      jamais \ali \verdir{à la fois} \brunir{libre} et \brunir{liée}.}}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La syntaxe de \lxgc}
La syntaxe
\begin{center}
\begin{math}
\begin{array}{rcl}  
M,N \: &::=& \: x\: |\: `l  x.M\:|\: M\:N\:|\:M<x=N>
\end{array}
\end{math}
\end{center}

\vspace*{10pt}

Un terme de la forme \bleu{M<x=N>} s'appelle une \brunir{clôture}.

Dans \bleu{M<x=N>} la variable \bleu{x} est liée dans un \bleu{M}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La disponibilité} %
La notion de variable libre doit être généralisée avec précaution.

On parle de \brunir{«variable disponible»}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La disponibilité} %
La notion de variable libre doit être généralisée avec précaution.

On parle de \brunir{«variable disponible»}.

\vspace*{1cm}

Une variable est \brunir{non disponible} si elle apparaît dans une
clôture destinée à disparaître.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{La disponibilité} %
  Si dans \bleu{M<x=N>} 
  \begin{itemize}
  \item la variable \bleu{y} «apparaît» dans \bleu{N} 
  \item mais si \bleu{x} n'«apparaît» pas dans \bleu{M}
\end{itemize}
alors \bleu{y} n'est pas disponible dans \bleu{M<x=N>}.  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La disponibilité }
Plus formellement 
\begin{footnotesize}
\[
  \left\{
    \begin{array}{lll@{\hspace*{12pt}}l}
      AV(x)           & = &   \{x\} \\
      AV(`l x.M)     & = &   AV(M)\backslash \{x\} \\
      AV(M\:N)        & = &   AV(M)\cup AV(N) \\
      AV(M<x=N>)      & = &   (AV(M)\backslash \{x\})\cup AV(N)     & \mbox{if $x\in AV(M)$}\\
      AV(M<x=N>)      & = &   AV(M)                               & \mbox{if $x\not\in AV(M)$}
    \end{array}
  \right.
  \]
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Les règles de \lxgc} 
\begin{center}
\begin{math}
\begin{array}{lrcl}   %{rclcl}
\emph{(B)} & \quad (`l x .  M) \,P       & \quad "->" \quad   & M<x=P> \\
[2pt]
\emph{(App)} & \quad (M N)<x=A> & \quad "->" \quad   & M <x=A> \, N <x=A> \\
\emph{(Abs)} & \quad (`l y . M)<x=A>& \quad "->" \quad   & `l y . (M<x=A>)\\
\emph{(VarI)} & \quad x<x=A>    & \quad "->" \quad   & A      \\
\emph{(VarK)} & \quad y<x=A>    & \quad "->" \quad   & y        \\
\emph{(gc)}   & \quad M<x=A>    & \quad "->" \quad   & M  \hspace{20pt}\mbox{if~} x\not\in AV(M) 
\end{array}
\end{math}
\end{center}
                                \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{Les règles de \lxgc} 
\begin{center}
\begin{math}
\begin{array}{lrcl}   %{rclcl}
\emph{(B)} & \quad (`l x . M) \,P       & \quad "->" \quad   & M<x=P> \\
[2pt]
\emph{(App)} & \quad (M N)<x=A> & \quad "->" \quad   & M <x=A> \, N <x=A> \\
\emph{(Abs)} & \quad (`l y . M)<x=A>& \quad "->" \quad   & `l y . (M<x=A>)\\
\emph{(VarI)} & \quad x<x=A>    & \quad "->" \quad   & A      \\
\emph{(VarK)} & \quad y<x=A>    & \quad "->" \quad   & y        \\
\emph{(gc)}   & \quad M<x=A>     & \quad "->" \quad   & M  \qquad \mbox{if~} x\not\in AV(M) 
\end{array}
\end{math}
\end{center}
                                \vfill
Noter l'importance de la convention de Barendregt dans
la règle $\emph{(Abs)}$.
\end{slide}
%------------------------------------------------------
\begin{slide}
 \heading{La règle \emph{(gc)}} %
La règle \bleu{\emph{(VarK)}} est un cas particulier de la règle \bleu{\emph{(gc)}}. 

$\emph{(gc)}$ a un effet global sur un terme qui rappelle le glanage de cellule
(garbarge collection) dans les langages de programmation (notamment les
langages de programmation fonctionnelle).

\vfill
\end{slide}
%%------------------------------------------------------
%\begin{slide}
% \heading{Les ensembles} 

%\begin{eqnarray*}
%\xx & = & \{\emph{(App)}, \emph{(Abs)}, \emph{(VarI)}, \emph{(VarK)}\}\\
%\lx & = & \xx \cup \{\emph{(B)}\}\\
%\xgc& = & \{\emph{(App)}, \emph{(Abs)}, \emph{(VarI)}, \emph{(gc)}\}\\
%\lxgc & = & \xgc \cup \{\emph{(B)}\}
%\end{eqnarray*}
%\vfill
%\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{center}
    \textbf{\LARGE {\color{vertfonce}Les indices de de Bruijn}}
\end{center}
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Notations Standard}
%\vspace{5pt}

\epsfig{file=bourbaki.eps,height=4.5cm}

\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Notations de Bourbaki}
%\vspace{5pt}

\epsfig{file=bourbaki2.eps,height=4.5cm}

\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Les indices de de Bruijn}

\epsfig{file=bourbaki3.eps,height=4.5cm}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les indices de de Bruijn}

Dans chaque terme, chaque variable est remplacée par sa
profondeur de lien (son \textcolor{vertfonce}{indice de de~ Bruijn}).

\vfill 

En d'autres mots.

\newcommand{\donne}{\xymatrix{\ar@{~>}[r] &}}

\begin{math}
\begin{array}{lcl}
I \quad \rouge{`=} \quad  `l x . x & \donne & `l 
(\und{0})\\ 
%
K \quad \rouge{`=} \quad  `l c . `l x . c \quad
\rouge{`=} \quad `l c x 
. c &\donne&  `l (`l (\und{1}))\\  
%
two \quad \rouge{`=} \quad  `l f . `l x . f (f x)
\quad \rouge{`=} \quad `l f x . f (f x) &\donne &  `l (`l (\und{1}\, (\und{1}\,\und{0})))
\end{array}
\end{math}

\end{slide}
%------------------------------------------------------
\begin{slide}
\vspace*{50pt}
  \begin{center}
    {\bf \color{vertfonce}{\textit{\LARGE Présentation de $`l `y $}}}
\end{center}

\vfill
{\footnotesize Un peu d'anglais ne fait pas de mal.}

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

\heading{Règle Beta}

\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(B)} & (`l M) \; P & "->" & M\rouge{[}P\rouge{/}\rouge{]}
\end{array}
\end{math}
\end{center}

 \bl{(B)} introduit deux nouveaux opérateurs.

La syntaxe est étendue.
\begin{eqnarray*}
\rouge{/} &\bl{:}& {\color{cyanp}`L`y "->" Substitution}\\
\rouge{\_[\_]} &\bl{:}& {\color{cyanp} `L`y  \times  Substitution
"->"  `L`y}
\end{eqnarray*}
$\rouge{/}$ et \rouge{\_[\_]} introduisent une nouvelle sorte
\({\color{cyanp}Substitution}\).  \vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Clôtures}

\rouge{\_[\_]} doit être défini par deux règles nouvelles, à savoir., 

\begin{itemize}

\item une distribution à travers les applications les  abstractions,

\item une distribution sur les  variables (indices de de~Bruijn).

\end{itemize}

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

\heading{Clôtures}

\rouge{\_[\_]} doit être défini par deux règles nouvelles, à savoir., 

\begin{itemize}

\item une distribution à travers les applications les  abstractions,

\item une distribution sur les  variables (indices de de~Bruijn).

\end{itemize}

\bigskip

Les termes de la forme \rouge{\(M[s]\)} sont appelés des
\brunir{clôtures}.

Ils forment véritablement le \brunir{calcul de substitution explicites}.

\vfill
Les termes sans clôtures sont appelés des \brunir{termes purs}.
\end{slide}
%----------------------------------------------------------------------
\begin{slide}

\heading{Distribution des substitutions}

\subheading{À travers les applications}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(App)} & (M \; P) [s] & "->" & M[s]\ P[s]
\end{array}
\end{math}
\end{center}

\vfill

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

\heading{Distribution des substitutions}
\subheading{À travers les applications}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(App)} & (M \; P) [s] & "->" & M[s]\ P[s]
\end{array}
\end{math}
\end{center}

\vfill

\subheading{À travers les abstractions}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(Lambda)} & (`l M)[s] & "->" & `l (M[\rouge{\Uparrow}(s)])
\end{array}
\end{math}
\end{center}

(Lambda) introduit un nouvel opérateur
\[\rouge{\Uparrow}(s) : {\color{cyanp}Substitution "->" Substitution}.\]
\end{slide}
%----------------------------------------------------------------------

\begin{slide}
\heading{Définir \rouge{/} et \(\rouge{\Uparrow}\)}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(FVar)} & \und{0}[M/] & "->" & M \\
\emph{(RVar)} & \und{n+1} [M/] & "->" & \und{n} 
\end{array}
\end{math}
\end{center}
\vfill
\end{slide}
%----------------------------------------------------------------------

\begin{slide}
\heading{Définir \rouge{/} et \(\rouge{\Uparrow}\)}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(FVar)} & \und{0}[M/] & "->" & M \\
\emph{(RVar)} & \und{n+1} [M/] & "->" &
\und{n} \\[10pt] 
\emph{(FVarLift)} & \und{0} [\Uparrow(s)] & "->" & \und{0} \\
\emph{(RVarLift)} & \und{n + 1}[\Uparrow(s)] 
                                 & "->" & \und{n}[s][\rouge{\uparrow}] \\[5pt]
\end{array}
\end{math}
\end{center}
\vspace*{1cm}
{(RVarLift)} introduit  une nouvelle constante
\(\rouge{\uparrow} : {\color{cyanp}Substitution}\)
\vfill  \addtocounter{slide}{-1}
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Définir \(\rouge{\uparrow}\)}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(VarShift)} & \und{n}[\uparrow] & "->" & \und{n+1}
\end{array}
\end{math}
\end{center}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{\(\rouge{`l `y }\)}
\begin{center}
\begin{math}
\begin{array}{lrcl}
\emph{(B)} & (`l M) \; P & "->" &
M{[}P{/}{]} \\[1pt]
\emph{(App)} & (M \; P) [s] & "->" & M[s]\
P[s]\\\emph{(Lambda)} & (`l M)[s] & "->" &
`l (M[{\Uparrow}(s)])\\[1pt] 
\emph{(FVar)} & \und{0}[M/] & "->" & M \\
\emph{(RVar)} & \und{n+1} [M/] & "->" & \und{n} \\[1pt]

\emph{(FVarLift)} & \und{0} [\Uparrow(s)] &
"->" & \und{0} \\ 
\emph{(RVarLift)} & \und{n + 1}[\Uparrow(s)] %
                               & "->" &
                                 \und{n}[s][{\uparrow}]
                                 \\[1pt]
\emph{(VarShift)} & \und{n}[\uparrow] & "->"%
                               & \und{n+1} 
\end{array}
\end{math}
\end{center}
\vfill
\end{slide}
%----------------------------------------------------------------------

%----------------------------------------------------------------------------
%                 quelques calculs en lambda-upsilon
%----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}
\end{eqnarray*}
\vfill
\end{slide}
%----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}\\
& \rouge{"->"} & `l (\bl{(\und{1}\,(\und{1}\,\und{0}))
                   [\Lift(`l \und{0}/)]})
\end{eqnarray*}
\vfill \addtocounter{slide}{-1}
\end{slide}
%----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}\\
& \rouge{"->"} & `l (\bl{(\und{1}\,(\und{1}\,\und{0}))
                   [\Lift(`l \und{0}/)]})\\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)] \,\bl{(\und{1}\,\und{0})
                   [\Lift(`l \und{0}/)]}) \\
\end{eqnarray*}
\vfill \addtocounter{slide}{-1}
\end{slide}
 %----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}\\
& \rouge{"->"} & `l (\bl{(\und{1}\,(\und{1}\,\und{0}))
                   [\Lift(`l \und{0}/)]})\\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)] \,\bl{(\und{1}\,\und{0})
                   [\Lift(`l \und{0}/)]}) \\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)]\,
                 (\und{1} [\Lift(`l \und{0}/)]\,
                 \bl{\und{0}[\Lift(`l \und{0}/)]}))
\end{eqnarray*}
\vfill \addtocounter{slide}{-1}
\end{slide}
%----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}\\
& \rouge{"->"} & `l (\bl{(\und{1}\,(\und{1}\,\und{0}))
                   [\Lift(`l \und{0}/)]})\\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)] \,\bl{(\und{1}\,\und{0})
                   [\Lift(`l \und{0}/)]}) \\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)]\,
                 (\und{1} [\Lift(`l \und{0}/)]\,
                 \bl{\und{0}[\Lift(`l \und{0}/)]})) \\
& \rouge{"->"} & `l (\bl{\und{1}[\Lift(`l \und{0}/)]}\,
                 (\verdir{\und{1} [\Lift(`l \und{0}/)]}\,
                 \und{0}))
\end{eqnarray*}
\vfill \addtocounter{slide}{-1}
\end{slide}
%----------------------------------------------------------------------------
\begin{slide}
\heading{Calculs dans $`l `y $}
\begin{eqnarray*}
two\ I & \rouge{`=} & \bl{(`l `l \und{1}\,
   ( \und{1}\,\und{0})) \ (`l \und{0})}\\
& \rouge{"->"} & \bl{(`l \und{1}\, (\und{1}\,\und{0}))
    [`l \und{0}/]}\\
& \rouge{"->"} & `l (\bl{(\und{1}\,(\und{1}\,\und{0}))
                   [\Lift(`l \und{0}/)]})\\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)] \,\bl{(\und{1}\,\und{0})
                   [\Lift(`l \und{0}/)]}) \\
& \rouge{"->"} & `l (\und{1}[\Lift(`l \und{0}/)]\,
                 (\und{1} [\Lift(`l \und{0}/)]\,
                 \bl{\und{0}[\Lift(`l \und{0}/)]})) \\
& \rouge{"->"} & `l (\bl{\und{1}[\Lift(`l \und{0}/)]}\,
                 (\verdir{\und{1} [\Lift(`l \und{0}/)]}\,
                 \und{0}))\\
& \rouge{"->" `. "->"} & `l (\bl{\und{0}[`l \und{0}/]} [\uparrow]\,
                 (\verdir{\und{0} [`l \und{0}/]}[\uparrow]\,
                 \und{0}))\\\end{eqnarray*}
\vfill \addtocounter{slide}{-1}
\end{slide}
% ------------------------------------------------------------
\begin{slide}
\begin{eqnarray*}
& \rouge{"->" `. "->"} & `l (\bl{(`l \und{0}) [\uparrow]}\,
                 (\verdir{(`l \und{0})[\uparrow]}\, \und{0})) \\
& \rouge{"->" `. "->"} & `l (`l (\bl{\und{0} [\Lift(\uparrow)]})\,
                 (`l (\verdir{\und{0}[\Lift(\uparrow)]})\, \und{0})) \\
& \rouge{"->" `. "->"} & `l (`l \und{0}\,
                 ((`l \und{0}) \und{0})) \\
& \rouge{\vdots} & \\
& \rouge{"->>"} & `l \und{0}
\end{eqnarray*}

\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un calcul qui ne termine pas}%
\verdir{Exercice}: Montrer que \bleu{(`l \und{0} \und{0}) \: (`l \und{0}
  \und{0})\rarasub{`l `y} (`l \und{0} \und{0}) \: (`l \und{0} \und{0})}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\bf \color{vertfonce}{\textit{\LARGE Propriétés de $`l `y $}}}
\end{center}
\end{slide}
----------------------------------------------------------------------
\begin{slide}
\heading{Faits}

\begin{itemize}

\item $`l `y  = (B) \oplus `y $.

\item $`y $ est \brunir{orthogonal} \ali i.e., linéaire à gauche et
  sans paires critiques. 

\item $`y $  \brunir{termine} \ali i.e., \brunir{fortement
    normalisable}. 

\end{itemize}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Questions}

\begin{description}
\item[\brunir{Est-ce que ce  calcul représente}] \brunir{\bf le
    $`l $-calcul  classique?} 

\end{description}

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

\begin{description}
\item[\brunir{Est-ce que ce  calcul représente}] \brunir{\bf le
    $`l $-calcul  classique?} 

\verdir{Oui} %
\ali \bleu{M \rabeta P} est \bleu{M \raB N} et \bleu{N \rarasub{`y }
  `y(N)}.
\ali où \bleu{`y(N)} représente la forme normale par \bleu{`y} de
\bleu{N},%
\ali qu'on note aussi \bleu{N \ranormsub{`y} P} où \bleu{P`= `y(N)} .

\end{description}

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

\begin{description}

\item[\brunir{Est-ce que la spécification est complète?}]  
\end{description}

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

\begin{description}
\item[\brunir{Est-ce que la spécification est complète?}]~
  
  Que penser d'une règle \bl{\[M[s][t] "->" M[\dots s \dots t \dots]\]} où
  \bleu{[\dots s \dots t \dots]} est \bleu{[s `o t]} par exemple?

\end{description}

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

\begin{description}
\item[\brunir{Est-ce que la spécification est complète?}]~
  
  Que penser d'une règle \bl{\[M[s][t] "->" M[s `o t\]} par exemple?

\vfill

En fait, \verdir{on n'en a a pas besoin,} \ali puisque que chaque
clôture disparaît dans les \brunir{termes clos}.
\end{description}

\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le lemme de substitution}

\bleu{`l `y } admet une \brunir{paire critique}
\bl{\[\brunir{\langle} M[\Lift(s)][P[s]/] \brunir{~,~} M[P/][s]\brunir{\rangle}\]}


\vfill

\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le lemme de substitution}

\bleu{`l `y } admet une \brunir{paire critique}
\bl{\[\brunir{<} M[\Lift(s)][P[s]/] \brunir{~,~} M[P/][s]\brunir{>}\]}

\vfill

En général, l'identité

\bl{\[M[\Lift(s)][P[s]/] =  M[P/][s]\]}

est appelée le \brunir{lemme de substitution}. \addtocounter{slide}{-1}

\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le lemme de substitution}

\begin{center}
\begin{scriptsize}
  
  \xymatrix{
    &\ar[dl]_{\color{blue}\mathrm{App}}((`l \, M) \ P) [s] \ar[dr]^{\color{blue}\mathrm{B}} &\\
    \ar[d]_{\color{blue}\mathrm{Lambda}}(`l \, M)[s]\ P[s] & & M[P/][s]\\
    \ar[d]_{\color{blue}\mathrm{B}}`l (M[\Lift(s)])\ P[s]\\
    M[\Lift(s)][P[s]/] }
\end{scriptsize}
\end{center}
\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Le lemme de substitution}

\vspace*{40pt}

Le lemme de substitution est un  théorème inductive dans
\(`l `y \).

\vfill
\end{slide}

%----------------------------------------------------------------------
\begin{slide}
\heading{le Lemme de  projection}

Si \bleu{M\ \raB\ P} alors \bleu{`y (M)\rarabeta`y (P)}.

\hspace*{30pt}\xymatrix{
\bl{M} \ar[r]_{\color{blue}B} \ar@{.>|}[d]_{\color{blue}`y } & \bl{P}\ar@{.>|}[d]^{\color{blue}`y }\\
\bl{`y (M)} \ar@{.>>}[r]_{\color{blue}\beta} & \bl{`y (P)}
}

Le \brunir{lemme de projection} est une conséquence \ali du \brunir{lemme de substitution}.

\vfill
\end{slide}
%----------------------------------------------------------------------
\begin{slide}
\heading{Confluence de $`l `y $}
$`l `y $ est confluent sur les termes clos.

La \brunir{confluence} est conséquence du \brunir{lemme de
  projection}.

\begin{scriptsize}
\begin{center}
\mbox{
  \xymatrix{ & \ar@{>>}[dl]_{\color{blue}`l `y } M
    \ar@{.>|}[d]^{\color{blue}`y }
    \ar@{>>}[dr]^{\color{blue}`l `y }& &\\
    N\ar@{.>|}[d]_{\color{blue}`y } & M'
    \ar@{.>>}[dl]_{\color{blue}\beta}\ar@{.>>}[dr]^{\color{blue}\beta}
    &
    P \ar@{.>|}[d]^{\color{blue}`y } &\\
    N' \ar@{.>>}[dr]^{\color{blue}\beta} & & P'\ar@{.>>}[dl]_{\color{blue}\beta}\\
    & Q & }}
\end{center}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

\heading{\(`l `y \) préserve la  normalisation forte }

Si un terme \bleu{M} est  \brunir{fortement $\beta$ normalisable}, %
\ali alors \bleu{M} est \brunir{fortement  \(`l `y \) normalisable}.

La preuve est par contradiction, fondée sur l'existence d'un plus
petit contre-exemple.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\vspace*{50pt}
  \begin{center}
    {\bf \color{vertfonce}{\textit{\LARGE Présentation de $`l`s$ faible}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}

Le but est d'implanter la normalisation faible de tête:
\begin{itemize}
\item on ne réduit que le redex de tête,
\item on ne réduit pas sous les $`l$.
\end{itemize}

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

\heading{Les opérateurs}%

\bl{
\begin{center}
\begin{math}
\begin{array}{rclr}  
U, V \: &::=&  U\:V\:|\:M[s] 
    & \brunir{\textit{(Environnement d'évaluation)}}\\
M, N \: &::=& \: \und{n}\: |\: `l M\:|\: M\:N & \brunir{\textit{(Code)}}\\
s, t \: &::=& \:  id \: |\: U `. s & \brunir{\textit{(Substitutions)}}
\end{array}
\end{math}
\end{center}
}

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

\heading{Les règles}%
\bl{\begin{center}
\begin{math}
\begin{array}{lrcl}  
\emph{(B_{`s})} & (`l M)[s]\: U & "->" & M[U `. s]\\[2pt]
\emph{(App_{`s})} & (M\:N)[s] & "->" & M[s]\:N[s]\\
\emph{(Fvar_{`s})} & \und{0}[U `. s] & "->" & U\\
\emph{(RVar_{`s})} &  \und{n+1}[U `. s] & "->" &  \und{n}[s]
\end{array}
\end{math}
\end{center}}

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

\heading{Les règles}%
\bl{\begin{center}
\begin{math}
\begin{array}{lrcl}  
\emph{(B_{`s})} & (`l M)[s]\: U & "->" & M[U `. s]\\[2pt]
\emph{(App_{`s})} & (M\:N)[s] & "->" & M[s]\:N[s]\\
\emph{(Fvar_{`s})} & \und{0}[U `. s] & "->" & U\\
\emph{(RVar_{`s})} &  \und{n+1}[U `. s] & "->" &  \und{n}[s]
\end{array}
\end{math}
\end{center}}

\vfill
Le \brunir{formes normales} sont \bleu{(`l M)[s]}, on les appelle aussi
les \brunir{valeurs}.
\end{slide}
%------------------------------------------------------
\begin{slide}

\heading{Comment coder $`l`s_w$ dans $`l`y$ ?}%
On voit que tout environnement d'évaluation de \bleu{`l`s_w} s'écrit
\begin{itemize}
\item soit \bleu{M[U_1 `. \ldots `.  U_p `. id]}, \ali où \bleu{M} est un
  terme pur
  
\item soit c'est combinaison par applications de tels environnements
  d'évaluation.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}

Définissons \bleu{\T: `l`s_w "|->" `L`y} par  \bleu{\T(U) =
  \T'(U, 0)} où %
\begin{itemize}
\item \bleu{\T'(U\:V, n) = \T'(U, n)\:\T'(V, n)}
\item \bleu{\T' (M[id],n) = M },
\item \bleu{\T'(M[U `. s],n) = \T'(M[s], n+1)[\Lift^n(\T(U))/]}
\end{itemize}

Autrement dit: %
\ali \bleu{\T(M[U_0 `. \ldots `.  U_p `. id]) = M[\Lift^p(\T(U_p))/]
  \ldots [\T(U_0)/]}.

\bleu{M} est un terme pur donc il est laissé intact par \bleu{T}. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  Montrons que si \bleu {U \rasub{B_{`s}} V} alors \bleu{\T(U)
    \rarasub{Lambda_{`y}} \cdot \rasub{B_{`y}}\T(V)}.

On peut supposer que cette réduction a lieu à la racine.

On a \bleu{U `= (`l M) [U_1 `. \ldots `.  U_p `. id]\: U_0}\\ et \bleu{V
  `= M[U_0 `. U_1 `. \ldots `.  U_p `. id]}.

On a donc 
\bl{\begin{eqnarray*}
\T(U) & = & (`l M)  [\Lift^{p-1}(\T(U_p/))] \ldots [\T(U_1/)]\: \T(U_O)\\
& \rarasub{Lambda_{`y}} & (`l M  [\Lift^p(\T(U_p)/))] \ldots
[\Lift(\T(U_1)/)])\:\T(U_0)\\ 
&\rasub{B_{`y}}& M [\Lift^p(\T(U_p)/)] \ldots [\Lift(\T(U_1)/)][\T(U_0)/]\\
&=& \T(V)
\end{eqnarray*}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{\Huge Les machines abstraites}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE La machine de Krivine}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les états}%
Une machine abstraite comporte des \brunir{états} et des \brunir{transitions}.

L'état \bleu{c \sep e \sep s} de la machine de Krivine comporte trois
composantes :
\begin{itemize}
\item le \brunir{code} \bleu{c},
\item l'\brunir{environnement} \bleu{e},
\item la \brunir{pile} \bleu{s}.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les états}%
Une machine abstraite comporte des \brunir{états} et des \brunir{transitions}.

L'état \bleu{c \sep e \sep s} de la machine de Krivine comporte trois
composantes :
\begin{itemize}
\item le \brunir{code} \bleu{c},
\item l'\brunir{environnement} \bleu{e},
\item la \brunir{pile} \bleu{s}.
\end{itemize}

\vspace*{12pt}

\bleu{\begin{array}{rclll}
M,N &::=& `l M ~|~ M\:N ~|~ \und{n} && \brunir{\textit{(Code)}}\\
e &::=& <M, e> `. e ~|~ \mathsf{nil} &&\brunir{\textit{(Environnement)}}\\
s &::=&  <M, e> :: s ~|~ [~] &&\brunir{\textit{(Pile)}}
  \end{array}
  }

\vfill \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les transitions}%
On peut voir la machine de Krivine comme un moyen de décrire la
réduction la plus à gauche et la plus externe dans le système \bleu{`l`s_w}.

On a quatre transitions qui correspondent aux quatre instructions de~\bleu{`l`s_w}.
\bl{\begin{eqnarray*}
`l M \sep  e \sep  <N, f> :: s & "->" & M \sep  <N,f> `. e \sep  s\\
M\: N \sep  e \sep  s & "->" & M  \sep  e \sep  <N, e> :: s\\
0 \sep  <N,f> `. e \sep  s  & "->" & N \sep  f \sep  s \\
n+1 \sep  <N,f> `. e \sep  s  & "->"& n \sep  e \sep  s
\end{eqnarray*}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un exemple}%

\bl{
\begin{eqnarray*}
(`l \und{0})\:(`l \und{0}) \sep  \mathsf{nil} \sep  [~] & "->" & (`l \und{0}) \sep 
    \mathsf{nil} \sep   [<`l \und{0}, \mathsf{nil}>] \\
 & "->" & \und{0} \sep  <`l \und{0},\mathsf{nil}> \cdot \mathsf{nil} \sep  [~]\\
 & "->" & `l \und{0} \sep  \mathsf{nil}  \sep  [~]
\end{eqnarray*}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La sémantique}%
La machine  de Krivine implante l'\brunir{appel par nom}.

La partie du corps de la fonction est évaluée avant les arguments.

L'\brunir{état de départ} est %
    \bleu{M  \sep  \mathsf{nil} \sep  [~]}.

Les \brunir{états irréductibles} sont
\begin{itemize}
\item \bleu{`l M ~\rouge{,}~ e   ~\rouge{,}~ [~]} \quad {\small le code est
  une abstraction, mais il n'y a rien sur la pile,}
\item \bleu{\und{n} ~\rouge{,}~ \textsf{nil} ~\rouge{,}~ s} \quad
  {\small le code est une variable mais l'environnement est vide.}
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Lien avec $`l`s_w$}%
\verdir{Exercice}: Montrer la correspondance entre les réductions de la
machine de Krivine et les réductions les plus à gauche et les plus
externes dans le système \bleu{`l`s_w}.  
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE Une machine pour l'appel par nécessité}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Comment cela fonctionne}%

On utilise des places en mémoire repérées par des adresses pour
stocker des clôtures.

On ajoute donc un état mémoire le \brunir{tas} («heap» en anglais)
\bleu{h} qui fait correspondre à chaque adresse une clôture.

Lorsqu'on réduit une clôture, il faut l'isoler dans son contexte. 


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les états}%
Les états sont de la forme \bleu{M \sep e \sep s \sep u \sep h}.

\bleu{\begin{array}{rclll}
M,N &::=& `l M ~|~ M\:N ~|~ \und{n} && \brunir{\textit{(Code)}}\\
e &::=& a `. e ~|~ \mathsf{nil} &&\brunir{\textit{(Env)}}\\
s &::=& a :: s ~|~ [~] &&\brunir{\textit{(Pile)}}\\
u &::=& (s,a) :: u ~|~ [~] && \brunir{\textit{(Pile de mise à jour)}}\\
h &::=& \{~\} ~|~ h\{a "|->" <M,e>\} && \brunir{\textit{(Tas)}}\\
a && \brunir{\textit{les adresses de clôtures.}}
  \end{array}
  }
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les transitions}%
\begin{footnotesize}
\bleu{\begin{array}{rclll}%
M \: N \sep e\sep s \sep u \sep h &"->"& M \sep e \sep a `. s \sep u
    \sep h \{a "|->"<N,e>\} && 
    \brunir{\textit{(App)}}\\
    && \quad a \textrm{~fraîche} \\
`l M \sep e\sep a `. s \sep u \sep h &"->"& M \sep a `. e\sep s \sep u
    \sep h && \brunir{\textit{(Lam)}}\\
\und{n+1} \sep a `. e\sep s \sep u \sep h &"->"& \und{n} \sep e\sep s \sep u
    \sep h && \brunir{\textit{(Skip)}}\\
\und{0} \sep a `. e\sep s \sep u \sep h &"->"& N \sep e'\sep [~] \sep
    (s, a) :: u \sep h && \brunir{\textit{(Access)}}\\
    &&  \quad \textrm{où~} h~a = <N,e'> \\
`l M \sep e\sep [~] \sep (s,a) :: u \sep h &"->"& `l M \sep e\sep s
\sep u \sep h\{a "|->" <`l M, e>\} && \brunir{\textit{(Update)}}
\end{array}
  }
\end{footnotesize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Cette machine réduit les termes clos jusqu'à leur forme normale de tête.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{\Huge Sémantiques \\à grandes étapes}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La sémantique à grandes étapes}%
Un système de réécriture donne typiquement \brunir{une sémantique par
  petites étapes} de calcul \textit{small steps}.  %
\ali C'est-à-dire qu'on décrit les étapes élémentaires du calcul.

Une sémantique qui décrit une relation \brunir{donnée--résultat} est
dite \brunir{sémantique à grandes étapes} \textit{(big steps)}.
\ali La notation habituelle est \bleu{M \downarrow N}.

On parle aussi de \brunir{sémantique opérationnelle structurée} %
\ali (en abrégé et en anglais comme en français: SOS) %
\ali(due à Plotkin)

ou de \brunir{sémantique naturelle} (due à Kahn).  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par nom en sémantique à grandes étapes}%
On se fonde sur le calcul de substitution explicite \bleu{`l`s_w}.

On verra que dans les applications %
\ali on réduit d'abord le corps (partie gauche) %
\ali avant le paramètre (partie droite).
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par nom en sémantique à grandes étapes}%
\begin{center}
\begin{math}
\prooftree%
M[U `. s] \nom V
\justifies%
(`l M)[s] \: U \nom V
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
\prooftree%
 M_1[s] \nom  V \qquad V \: M_2[s] \nom W 
\justifies%
(M_1 \: M_2)[s] \nom W
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
\prooftree%
U\nom U'
\justifies%
\und{0}[U `. s] \nom U'
\endprooftree%
\qquad%
\prooftree%
\und{n}[s] \nom U'
\justifies%
\und{n+1}[U `. s] \nom U'
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
(`l M)[s] \nom (`l M)[s]
\end{math}
\end{center}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par nom en sémantique à grandes étapes}%

\begin{scriptsize}
\begin{displaymath}
  \prooftree
(`l `l 1)[id] \nom (`l `l 1)[id]
 \qquad %
 \prooftree %-2.1
 (`l 1)[((`l 0 0)~(`l 0 0))[id]`.id] \nom (`l 1)[((`l 0 0)~(`l 0 0))[id]`.id] \justifies (`l
 `l 1)[id]~((`l 0 0)~(`l 0 0))[id] \nom (`l 1)[((`l 0 0)~(`l 0 0))[id]`.id]
 \endprooftree %-2.1
 \justifies (`l `l 1)~((`l 0 0)~(`l 0 0))[id] \nom (`l 1)[(`l 0 0)~(`l 0 0)[id]`.id] %
 \endprooftree
\end{displaymath}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par valeur en sémantique à grandes étapes}%
Dans la suite une \brunir{valeur} est une clôture contenant une abstraction dans
sa partie terme,%
\ali c'est-à-dire de la forme \bleu{(`l x. M)[s]}.

On réduit d'abord le paramètre (partie droite),%
\ali avant le corps (partie gauche).  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par valeur en sémantique à grandes étapes}%
\begin{center}
\begin{math}
\prooftree%
M[U `. s] \valeur V
\justifies%
(`l M)[s] \: U \valeur V
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
\prooftree%
 M_2[s] \valeur V \qquad M_1[s] \: V \valeur W \qquad M_2[s]
 \mbox{\brunir{~n'est pas une valeur}}
\justifies%
(M_1 \: M_2)[s] \valeur W
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
\prooftree%
M_1[s] \valeur V \qquad V \:  M_2[s] \valeur W \qquad %
    M_2[s]  \mbox{\brunir{~est une valeur}}
\justifies%
(M_1 \: M_2)[s] \valeur W
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
\prooftree%
U\valeur U'
\justifies%
\und{0}[U `. s] \valeur U'
\endprooftree%
\qquad%
\prooftree%
\und{n}[s] \valeur U'
\justifies%
\und{n+1}[U `. s] \valeur U'
\endprooftree%
\end{math}
\end{center}

\begin{center}
\begin{math}
(`l M)[s] \valeur (`l M)[s]
\end{math}
\end{center}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par valeur en sémantique à grandes étapes}%
\begin{scriptsize}
\begin{displaymath}
  \prooftree
 \prooftree %-2
 \prooftree %-3
 (`l 0 0)[id] \valeur (`l 0 0)[id] %
 \justifies 0[(`l 0 0)[id] . id] \valeur (`l 0 0)[id]
 \endprooftree %-3
 \justifies ((`l 0)~(`l 0 0))[id] \valeur (`l 0 0)[id]
 \endprooftree %-2
 \qquad %
 \prooftree %-2.1
(`l 1)[(`l 0 0)[id]`.id] \valeur (`l 1)[(`l 0 0)[id]`.id]
 \justifies (`l `l 1)[id]~(`l 0 0)[id] \valeur (`l 1)[(`l 0 0)[id]`.id]
 \endprooftree %-2.1
 \justifies (`l `l 1)~((`l 0)~(`l 0 0))[id] \valeur (`l 1)[(`l 0 0)[id]`.id] \endprooftree
\end{displaymath}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'appel par valeur en sémantique à grandes étapes}%
\verdir{Exercice} :
\begin{enumerate}
\item Dans quel ordre réduit-on les arguments dans cette définition de
  l'appel par valeur ?
\item Comment changer les règles pour obtenir un autre ordre
  d'évaluation des arguments ?
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{\Huge La sémantique par continuation}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\Large Les origines et les motivations}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les origines}%
La méthode des continuations a été introduite par Strachey et
Wadsworth comme un outil pour formaliser la notion de \brunir{flot de contrôle}
dans les langages de programmation.

Dans cette méthode un terme est évalué dans un contexte qui représente
le \brunir{«reste du calcul»}.

Les termes, sont à proprement parler évalués de gauche à droite,
mais surtout en manipulant ce contexte.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les origines}%
  Il s'agit d'une technique fondée sur les fonctions d'ordre
  supérieur, qui peut-être utilisée
\begin{itemize}
\item directement par le programmeur,
\item dans la transformation de programme,
\item ou dans l'optimisation de compilateur.
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les origines}%
Si le terme implique l'évaluation d'un sous-terme, %
\begin{itemize}
\item[]  \textbf{alors} ce sous-terme
est évalué dans un nouveau contexte qui évalue le reste du terme %
\item[] \textbf{et alors} il prend en compte l'ancien contexte.
\end{itemize}


Si le terme peut être évalué immédiatement alors sa valeur est passée
au contexte. 

Un tel \brunir{contexte} est appelé une \brunir{continuation}. 
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un exemple}%
Soit la fonction OCAML

\begin{scriptsize}
    \begin{tt}
      let f(x,y) = y +. 3. *. x +. (2. +. 1./.x)/.(1. +. 2./.x)
    \end{tt}
\end{scriptsize}

On peut considérer le calcul qui se fait après la division
\texttt{1./.x} \\et qui est donné par

\begin{scriptsize}
    \begin{tt}
      let continue quotient = \ali avant +. (2. +. quotient)/.(1. +. 2./.x)
    \end{tt}
\end{scriptsize}

ou \texttt{avant} est donné par
\begin{scriptsize}
  \begin{quotation}
    \begin{tt}
      let avant = y +. 3. *. x
    \end{tt}
  \end{quotation}
\end{scriptsize}
et où \texttt{quotient} est le résultat  d'une division qui peut conduire à une erreur.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un exemple}%
On souhaite «naturellement» que dans le cas où \texttt{x} est égal à
zéro, la fonction \texttt{f(x,y)} rende le résultat \texttt{y
  +. 3. *. x +. 0.5}:

\begin{scriptsize}
  \begin{verbatim}
let f(x,y) = 
  let divide(numerateur, denominateur, continuation, autre_valeur) =
    if denominateur > 0.00001
    then continuation(numerateur /. denominateur)
    else autre_valeur
  in let avant = y +. 3. *. x
  in let continue quotient = 
             avant +. (2. +. quotient) /. (1. +. 2. /. x)
  in divide(1., x, continue, y +. 3. *. x +. 0.5)
  \end{verbatim}
\end{scriptsize}

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{IMP revisité}%
Si on reprend la sémantique de IMP avec continuation, il faut ajouter
une structure de données \bleu{\textbf{Réponses}}.
\newcommand{\Cinterp}[1]{\mathcal{C'}\llbracket#1\rrbracket}

\bleu{\Cinterp{c}: (`S "^->" \textbf{Réponses}) "^->" `S"^->"
  \textbf{Réponses}} 

On a une nouvelle définition de \bleu{\Cinterp{~}} sur la composition
séquentielle. 
\begin{eqnarraybleu}
  \Cinterp{c_0; c_1} & = & \Cinterp{c_0} `o \Cinterp{c_1}
\end{eqnarraybleu}
%
\bleu{\Cinterp{c_1}} transforme la continuation, puis c'est au
tour de \bleu{\Cinterp{c_0}}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les continuations et la sémantique}%
La \brunir{sémantique par continuation} explique des phénomènes que la \brunir{sémantique
directe} ne peut pas expliquer, \ali comme les sauts dans les langages
impératifs.

Elle rend compte et permet de définir des \brunir{implantations efficaces et
souples}.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les continuations et la sémantique}%
La sémantique par continuation est aussi appelée \verdir{style de
  passage de continuations}, en anglais \verdir{continuation passing
  style}, ou pour faire court \verdir{CPS}.

\vspace*{20pt}
En \brunir{lambda-calcul}

Elle fait une \brunir{traduction} du lambda-calcul vers lui-même.

C'est même une \brunir{véritable compilation} du lambda-calcul dans le
lambda-calcul.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\Large Un résultat d'équivalence}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Objectifs}%
\verdir{Dans ce qui suit}
\begin{itemize}
\item on va définir la sémantique par continuations,
\item on va montrer l'équivalence de la \verdir{sémantique par
    continuation} avec la \verdir{sémantique directe}.
%  \hfill \brunir{\includegraphics[width=.4cm]{attention.eps} un peu
%    costaud!}
\end{itemize}                                
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La source d'inspiration}%

  Notre inspiration vient d'un article d'Albert Meyer et Mitchell
  Wand, intitulé, \brunir{\textit{Continuation Semantics in Typed
      Lambda-Calculi}} \ali in Logic of Programs, LNCS 193, Springer
  (1985), pp:219-224.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\Large La transformation}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le langage}%
Le lambda calcul est simplement typé.  

Les types sont alors 
\begin{itemize}
\item des types de base \bleu{`s_1, `s_2,...}
\item ou des types fonctionnels \bleu{`a "->"`b}.
\end{itemize}
Il y a un type particulier \bleu{o} (pas nécessairement de base) %
\ali qui est le type des \brunir{réponses}.

Ce sont les seuls types.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des types}%
La sémantique par continuation manipule des représentations d'objets
qui apparaissent dans la sémantique directe.

On assigne à chaque type  \bleu{`a} un type \bleu{`a'} des
représentations des objets de type  \bleu{`a}. 

Les types de base sont représentés par eux mêmes. 
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation des types}%
A une fonction de type \bleu{`a "->"`b}, nous faisons correspondre
dans la sémantique par continuation une fonction qui prend deux
arguments:
\begin{itemize}
\item une \brunir{représentation} de  \bleu{`a},
\item et une \brunir{continuation} qui attend une représentation de  \bleu{`b}.
\end{itemize}

Munie de cette information la fonction calcule une réponse.

Ainsi nous avons:
\bl{
  \begin{eqnarray*}
    `s'  & \triangleq & `s \\
(`a "->" `b)' & \triangleq & `a' "->" (`b'"->"o) "->" o
  \end{eqnarray*}
}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%
Pour chaque terme \bleu{M} de type \bleu{`a}, nous construisons un
terme \bleu{\overline{M}} de type \bleu{(`a'"->"o)"->"o} comme suit:
\bl{
  \begin{eqnarray*}
    \overline{x}  & \triangleq & `l`k.`k x \\
\overline{`l x. M} & \triangleq & `l`k.`k (`l x \overline{M})\\
\overline{M\,N} & \triangleq & `l`k.\overline{M}(`l m . \overline{N} (`l n. m n `k))
  \end{eqnarray*}
}
%
\vfill
\verdir{Exercice} :
J'ai enlevé les annotations de types pour la clarté.  Rétablissez les.
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%
Montrons que si \bleu{M : `a}  alors \bleu{\overline{M} : (`a'"->"o)"->"o} %
\ali c'est-à-dire:
\bl{
  \begin{eqnarray*}
    x : `a & \brunir{"=>"} & \overline{x} : (`a'"->"o)"->"o \\
`l x. M : `a "->" `b & \brunir{"=>"} & \overline{`l x. M} : ((`a "->" `b)' "->"o)"->"o \\
M\,N : `b \textrm{\color {black} \quad avec~} M: `a "->" `b \textrm{\color {black} ~et~} N: `a
&\brunir{"=>"} & \overline{M\,N} : (`b'"->"o)"->"o 
  \end{eqnarray*}
}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%
En bref, 
\begin{itemize}
\item   Si on a une \brunir{variable}, on envoie le résultat à la
  continuation \bleu{`k}.\\
  \bleu{`k}:\verdir{$`a'"->"o$} et \bleu{`l`k.`k x}:\verdir{$(`a'"->"o)"->"o$} 
  
\item 
  Si on a une \brunir{abstraction}, on fournit à la continuation une
  fonction appropriée.
  \begin{itemize}
  \item \bleu{`l x.M}: \verdir{$`a"->"`b$},
  \item \bleu{M}: \verdir{$`b$},
  \item \bleu{`l x.\overline{M}}: \verdir{$`a'"->"(`b'"->"o)"->"o `=
      (`a"->"`b)'$},
  \item \bleu{`k}: \verdir{$(`a"->"`b)'"->"o$},
  \item \bleu{`k(`l x.\overline{M})}: \verdir{$o$},
  \item \bleu{`l`k.`k(`l x.\overline{M})}: \verdir{$((`a"->"`b)'"->"o)"->"o$},
  \end{itemize}

\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{itemize}
\item 
  Si on a une \brunir{application}, on évalue l'opérateur dans une continuation qui consiste à évaluer
  l'opérande dans une continuation qui elle-même consiste à appliquer la valeur de l'opérateur à la
  valeur de l'opérande et à la continuation courante.  %
  \ali cela s'accorde joliment avec la définition de \bleu{(\_)'}: Si \bleu{M} est de type
  \bleu{`a"->"`b}, alors 
  \begin{itemize}
  \item[$\star$] \bleu{m} doit être de type \bleu{(`a"->"`b)'\triangleq `a'"->"(`b'"->"o)"->"o},
  \item[$\star$] \bleu{n} doit être de type \bleu{`a'},
  \item[$\star$] \bleu{`k} doit être de type \bleu{`b'"->"o}.
\end{itemize}
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{itemize}
  \item \bleu{M} : \verdir{$`a"->"`b$},
  \item \bleu{N} : \verdir{$`a$},
  \item \bleu{\overline{M}}: \verdir{$((`a"->"`b)'"->"o)"->"o \\%
      \hspace*{50pt}`= ((`a'"->"(`b'"->"o)"->"o)"->"o)"->"o $}
  \item \bleu{\overline{N}}: \verdir{$(`a'"->"o)"->"o $},
  \item \bleu{m~n~`k}: \verdir{$o$},
  \item \bleu{`l n . m~n~`k}: \verdir{$`a'"->"o$},
  \item \bleu{\overline{N}(`l n . m~n~`k)}: \verdir{$o$},
  \item \bleu{`l m . \overline{N}(`l n . m~n~`k)}: \verdir{$(`a"->"`b)'"->"o \\%
      \hspace*{50pt} `= (`a'"->"(`b'"->"o)"->"o)"->"o$}
  \item \bleu{\overline{M}(`l m . \overline{N}(`l n . m~n~`k))}:
    \verdir{$o$},
  \item \bleu{`l `k. \overline{M}(`l m . \overline{N}(`l n . m~n~`k))}:
    \verdir{$(`b'"->"o)"->"o$}
  \end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%
Une propriété intéressante de \bleu{\overline{M}} est qu'elle est \brunir{récursive terminale}
(\verdir{tail-recursive}).

Les sous-termes de la forme \bleu{\overline{M}} qui apparaissent dans un
terme \bleu{P~Q} apparaissent toujours dans \bleu{P}.

Cette propriété se préserve par $`b$-réduction.

Il y a au plus un redex sous chaque lambda.

Ainsi (sur \bleu{\overline{M}}) la réduction par appel par valeur
  coïncide avec la réduction par appel par nom.

Les implantations sur les machines standards sont plus faciles.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%

\verdir{Exercice} :

Montrer que \bleu{\overline{`l x. M} = \overline{[x] M}} où \bleu{[x]
  M} est l'«abstraction-crochet» définie sur les combinateurs (voir mon cours de
logique sur la logique combinatoire).  
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La transformation}%
L'évaluation d'un terme se fait en l'appliquant à la \brunir{continuation
identité}.

C'est-à-dire en l'appliquant à la continuation qui rend comme
réponse la valeur qu'on lui a donnée.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\Large La correction}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Question}%
Comment définir la transformation inverse ?

\begin{displaymathbleu}
  \overline{M} \quad "->" \quad M
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Rétraction}%

On dit que \bleu{`a} est un \brunir{retract} de \bleu{`b} et on écrit
\bleu{`a\triangleleft `b} %
\ali s'il existe des applications lambda-définissables
\ali \qquad \bleu{i:`a"->"`b} et \bleu{j:`b"->"`a} %
\ali telles que \bleu{j`o i} soit l'identité sur \bleu{`a}.

\bigskip

Le couple \bleu{(i,j)} forme la \brunir{rétraction}.

%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Si \bleu{`s \triangleleft o} pour chaque type de base \bleu{`s}, alors \bleu{`a \triangleleft (`a
"->" o) "->" o}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Si \bleu{`s \triangleleft o} pour chaque type de base \bleu{`s}, alors \bleu{`a \triangleleft (`a
"->" o) "->" o}.

%\vspace*{1.5mm}

\begin{small}
\brunir{Démonstration}

Définissons \bleu{\Ia : `a "->" (`a "->" o) "->" o} par \bleu{\Ia \triangleq `l x`k.`kx}.  

Pour définir l'application inverse, observons que \bleu{`a} doit être de la forme \bleu{`a_1 "->"
  `a_2 "->"..."->"`g} où \bleu{`g} est un type de base. 

Soit \bleu{r:`g"->"o} l'injection de la rétraction de \bleu{`g} vers \bleu{o} avec comme inverse à
gauche \bleu{l}.  

Alors nous définissons 
\begin{displaymathbleu}
  \Ja \triangleq `l u:(`a "->" o) "->" o . `l x_1:`a_1...`l x_n:`a_n. l(u(`l a:
  `a.r(ax_1...x_n))).
\end{displaymathbleu}
\end{small}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On voit que \bleu{\Ja \circ \Ia = id_{`a}}.

En effet
\begin{eqnarraybleu}
  \Ja(\Ia(a')) &"->"& `l x_1...`l x_n. l(\Ia(a')(`l a.r(ax_1...x_n)))\\
  &=& `l x_1...`l x_n. l(( `l x`k.`kx)(a')(`l a.r(ax_1...x_n)))\\
  &"->"&`l x_1...`l x_n. l(( `l`k.`ka')(`l a.r(ax_1...x_n)))\\
  &"->"&`l x_1...`l x_n. l((`l a.r(ax_1...x_n))\,a')\\ 
  &"->"&`l x_1...`l x_n. l(r(a'x_1...x_n))\\
  &=&`l x_1...`l x_n. a'x_1...x_n\\
  &"-{_{`h}}>"& a'
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Pseudo-application}%
Notons que \bleu{\Ia} n'est pas le combinateur habituel \bleu{`l
  x:`a.x}.

\bigskip

Notons aussi qu'on peut «appliquer» 
\begin{itemize}
\item un élément \bleu{m} de type \bleu{(`a"->"`b)'} 
\item à un élément \bleu{n} de type \bleu{`a'} 
\item et obtenir un élément de type \bleu{`b'} 
\item en écrivant \bleu{J_{`b'}(m~n)}.
\end{itemize}


\vspace*{3mm}

Nous utiliserons la notation \bleu{m \bullet n} pour \bleu{J_{`b'}(m~n)} %
\ali et nous parlerons de \brunir{pseudo-application}.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Pour tout type  \bleu{`a}, \bleu{`a \triangleleft `a'}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Pour tout type  \bleu{`a}, \bleu{`a \triangleleft `a'}.

\vspace*{2mm}
\brunir{Démonstration}

Pour les types de base la rétraction est l'identité, \ali c'est-à-dire  \bleu{i_{`s}
  \triangleq id_{`s}} et \bleu{j_{`s} \triangleq id_{`s}}.

Pour les types fonctionnels, on définit

\bl{
  \begin{eqnarray*}
 i_{`a"->"`b} & \triangleq &  `l f: `a"->"`b . I_{`b'} `o i_{`b}  `o f `o j_{`a}\\
 j_{`a"->"`b} & \triangleq &  `l f': (`a"->"`b)' . j_{`b} `o J_{`b'}  `o f' `o i_{`a}.
  \end{eqnarray*}
}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On a bien

\bl{
  \begin{eqnarray*}
 i_{`a"->"`b} & : & (`a"->"`b)"->"(`a"->"`b)'\\
 j_{`a"->"`b} & : & (`a"->"`b)'"->"(`a"->"`b)
  \end{eqnarray*}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème principal}%
Soit \bleu{M} un terme clos de type  \bleu{`a}.

Alors \bleu{M = j_{`a} (J_{`a'} \overline{M})}.

\vfill
\end{slide}
%%------------------------------------------------------
\begin{slide}
\heading{Théorème principal}%
Soit \bleu{M} un terme clos de type  \bleu{`a}.

Alors \bleu{M = j_{`a} (J_{`a'} \overline{M})}.

\vfill
Sa preuve nécessite d'introduire quelques concepts.
\end{slide}
%%------------------------------------------------------
\begin{slide}
Vérifions cependant que les types fonctionnent.

\bigskip

\begin{eqnarraybleu}
  M&:&`a\\
  \overline{M} &:& `a' "->" o  "->" o \\
  J_{`a'}  &:& (`a' "->" o  "->" o) "->" `a'\\
  J_{`a'} \overline{M} &:& `a'\\
  j_{`a} &:&  `a' "->" `a \\
  j_{`a} (J_{`a'} \overline{M}) &:& `a
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\Large Preuve du théorème principal}}}
\end{center}
\end{slide}
------------------------------------------------------
\begin{slide}
\heading{Interprétation d'un terme dans une valuation}%
%
Pour démontrer le théorème on a besoin de considérer aussi les termes
avec des variables libres.

Si on dit comment instancier les variables, on sait interpréter les
termes ouverts par des termes clos

On a besoin de «valuations».

Dans la suite, \bleu{`r} est une \brunir{valuation}  
\begin{itemize}
\item[] c'est-à-dire une fonction qui associe des termes clos à des
  variables.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Interprétation d'un terme dans une valuation}%

On suppose que les termes ont été traduits sous forme de combinateurs
en utilisant l'abstraction-crochet.

\bl{\begin{center}
  \begin{math}
    \begin{array}[c]{l@{\qquad\quad}l}
M  &  \interp{M}{}{`r}\\
\hline
x  &  `r(x)\\
K & K\\
S & S\\
P\ Q  &  \interp{P}{}{`r}\bullet  \interp{Q}{}{`r}
%`l x . P  &  M  "|->" \interp{P}{}{\modval{`r}{x}{M}}
    \end{array}
  \end{math}
\end{center}
}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Invariants concrets et prédicats acceptables}%
Pour pouvoir  démontrer le théorème on a besoin de caractériser quels éléments de \bleu{`a'} sont des
représentants «légaux» d'éléments de \bleu{`a.}.

C'est-à-dire qu'on doit trouver un invariant concret (i. e.,
expressible) approprié pour ce schéma de représentation.  %
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Prédicats acceptables}%
\bleu{P} est un prédicat \brunir{acceptable} si

\vspace*{8pt}


\begin{enumerate}
\item Pour tous types \bleu{`a} et \bleu{`b}, ainsi que pour tout
  \bleu{x:`a}
\begin{itemize}
\item \bleu{P_{`a}(i_{`a} x)},
\item \bleu{P_{`a"->"(`b"->"`a)}(J_{\scriptscriptstyle (`a"->"(`b"->"`a))'}\overline{K})},
\item
  \bleu{P_{(`a"->"`b"->"`g)"->"(`b"->"`g)"->"(`a"->"`g)}(J_{\scriptscriptstyle ((`a"->"`b"->"`g)"->"(`b"->"`g)"->"(`a"->"`g))'}\overline{S})}.
\end{itemize}

\vspace*{8pt}


\item Si \bleu{P_{`a"->"`b}(m)} et \bleu{P_{`a}(n)} , alors
\begin{itemize}
\item \bleu{P_{`b}(m `(!) n)},
\item \bleu{(j_{`a"->"`b} \;m)(j_{`a} \; n) = j_{`b} (m `(!) n)},
\item \bleu{m n = I_{`b'}(m `(!) n)}.
\end{itemize}
\end{enumerate}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Prédicats acceptables}%
\brunir{La propriété 1.} dit que les représentations canoniques et les images de
combinateurs sont «légales».

\brunir{La propriété 2.} dit 
\begin{itemize}
\item   le prédicat est clos par pseudo-application,
\item les applications conventionnelles sont des images homomorphes de
  pseudo-applications,

\item l'application de représentation se comporte bien, elle envoie une
  valeur à sa continuation.
\end{itemize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Soit \bleu{P} un prédicat acceptable. 

Pour tout  \bleu{M} et toute valuation  \bleu{`r} tel que pour
tout  \bleu{x},  \bleu{P(`r(x))}, \ali on a
\begin{displaymathbleu}
  \interp{M}{}{j `o `r} \quad = \quad j(J(\interp{\overline{M}}{}{`r}))
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Soit \bleu{P} un prédicat acceptable. 

Pour tout  \bleu{M} et toute valuation \bleu{`r} tel que pour
tout  \bleu{x},  \bleu{P(`r(x))}, \ali on a
\begin{displaymathbleu}
  \interp{M}{}{j `o `r} \quad = \quad j(J(\interp{\overline{M}}{}{`r}))
\end{displaymathbleu}
\brunir{Démonstration}

D'après l'exercice ci-dessus, on peut supposer que le terme est une
composition des combinateurs \bleu{S} et \bleu{K}.

Et alors, il suffit d'utiliser la définition et une hypothèse
d'induction. 

A faire complètement comme exercice.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Commentaires sur le théorème}%
%
\brunir{Que dit le théorème?}

Il dit que si \bleu{M} est un terme clos,
\begin{itemize}
\item[] \begin{mathbleu}
  \interp{M}{}{j `o `r} \quad = \quad j(J(\interp{\overline{M}}{}{`r}))
\end{mathbleu}

\item[] or dans ce cas \bleu{\interp{M}{}{j `o `r} = M} et
  \bleu{\interp{\overline{M}}{}{`r} = \overline{M}}
\end{itemize}

\vspace*{8pt}

\brunir{L'énoncé du théorème repose sur l'existence d'un prédicat acceptable.}

Existe-t-il un prédicat acceptable?
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Il existe un prédicat acceptable.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Théorème}%
Il existe un prédicat acceptable.
%
\vfill
\brunir{Esquisse de la démonstration}\\
Le prédicat \bleu{R}
\begin{itemize}
\item qui contient \bleu{i~x} pour tout \bleu{x} 
\item qui contient
  \bleu{J\overline{S}} et \bleu{J\overline{K}} 
\item et qui est clos par
  \bleu{`(!)}
\end{itemize}
est acceptable.
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{brunfonce}{\textit{\Huge Les réseaux de Lamping}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE L'optimalité de la réduction}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le problème de l'optimalité}%
On revient au problème de la normalisation forte dans le lambda-calcul.


Comment réduire un terme à sa forme normale en effectuant le moins
possible de réductions?

En effet, si une contraction duplique un redex, \\
il faut d'abord réduire ce redex avant que la contraction ne le
duplique.

Si une réduction fait disparaître le résidu de la contaction d'un
redex \\
il n'aurait pas fallu contracter ce redex.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le problème de l'optimalité}%

Considérons le terme \bleu{(`l y . (yy))\:(Iz)} où \bleu{I \equiv `l x .x}.

\bleu{
\begin{array}{ccccccc}
\rouge{(`l y . (yy))\:(Iz)} &"->"& \rouge{(Iz)} \: (Iz) &"->"& z \: \rouge{(Iz)} &"->"& z\: z \\
\rouge{(`l y . (yy))\:(Iz)} &"->"& (Iz) \: \rouge{(Iz)} &"->"& \rouge{(Iz) \: z} &"->"& z\: z \\
(`l y . (yy))\:\rouge{(Iz)} &"->"& \rouge{(`l y . (yy))\:z} &"->"& z\: z 
\end{array}
}

On peut faire du partage.

\xymatrix{
\rouge{(`l y . (yy))\:(Iz)} \ar[r]& `(!) \ar@/_/[d] `(!) \ar@/^/[d] \ar[r]& `(!) \ar@/_/[d]  `(!)\ar@/^/[d] \\
                              &   \rouge{(Iz)} &     z &
}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le problème de l'optimalité}%
Réduire les redex internes n'est pas la solution.

Mais le partage associé à une réduction du redex le plus à gauche ne
suffit pas.

Considérons \bleu{N `= N_1 \: N_2} avec %
\ali \bleu{N_1 `= `l x . (xw \: (x z))} %
\ali \bleu{N_2 `= `l y . (I y)}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le problème de l'optimalité}%

\xymatrix @C 10pt {
N \ar[r]& (`(!) \ar@/_/[d] w)(`(!) \ar@/^/[d] z) %
   \ar[r]& (I w)(`(!) \ar@/^/[d] z) %
    \ar[r]& w (`(!) \ar[d] z) \ar[r]& w (I z) \ar[r]& w z\\
& `l y . (I y) & `l y . (I y) & `l y . y
}

\vspace*{20pt}


\xymatrix @C 10pt {
N \ar[r]& (`(!) \ar@/_/[d] w)(`(!) \ar@/^/[d] z) %
   \ar[r]& (`(!) \ar@/_/[d] w)(`(!) \ar@/^/[d] z) %
    \ar[r]& w (`(!) \ar[d] z) \ar[r]& w z\\
& `l y . (I y) & `l y . y & `l y . y
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE Les réseaux d'interaction}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 
  
Les réseaux d'interaction sont des manières graphiques de représenter
les termes.

Sur les entiers

%\entrymodifiers={++[o][F-]}
\begin{scriptsize}
\xymatrix{
& \ar@{-}[d]& &&&&&\\
& *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr] && *++[o][F-]{Succ}\ar[u]\ar@{-}[d]&&*++[o][F-]{Zero}\ar[u]\\
&&&&&&
}
\end{scriptsize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 

Un \brunir{réseau} est un graphe (cyclique) non orienté dont les noeuds sont
étiquetés.

Un ensemble fini et fixé de \brunir{ports} est attribué à chaque étiquette. 

L'un des ports est appelé \brunir{port principal}.

Les noeuds sont connectés les uns aux  autres par leurs ports.

Chaque port est connecté à un et un seul autre port.

\vspace*{2pt}

Si deux noeuds sont connectés par leur port principal, ils forment une
\brunir{paire active} \xymatrix @C 8pt {*++[o][F-]{~}\ar[r]&&*++[o][F-]{~}\ar[l]}.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 
\begin{scriptsize}
\xymatrix @R 10pt @C 8pt {
&& a &&&& a\\
&& *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr]\ar@{-}[u] &\ar[r] &&& *++[o][F-]{Succ}\ar[u]\ar@{-}[d] \\
&*\txt{}&& c &&& *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr]\ar@{-}[u]  \\
*++[o][F-]{Succ}\ar[ur]\ar@{-}[d] &&&&& b && c\\
b
}
 \vfill
\end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 
\begin{scriptsize}
\xymatrix @R 10pt @C 8pt {
&& a &&&& a\ar@{-}[ddd]\\
&& *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr]\ar@{-}[u] &\ar[r] & \\
&*\txt{}&& b &&&  \\
*++[o][F-]{Zero}\ar[ur] &&&&&& b
}
 \vfill
\end{scriptsize}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 

Une \brunir{règle d'interaction} est un couple de paires actives qui satisfont
les conditions 1, 2 et 3.
  
\verdir{Propriété 1,} \brunir{Linéarité :} Dans chaque règle, chaque
variable (associée à un port) a exactement deux occurrences: l'un dans
le membre gauche et l'autre dans le membre droit.

\verdir{Propriété 2,} \brunir{Non ambiguïté :} Il y a au plus une règle pour
chaque paire active.

\verdir{Propriété 3,} \brunir{Optimisation :}  Les membres droits ne
contiennent pas de paires actives.

 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 

Due à la localité des interactions et à leur non interférence avec une
quelconque autre interaction, on voit que:

\begin{center}
  \brunir{les réductions sont confluentes.}
\end{center}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les réseaux d'interaction}% 
\verdir{Exercice :} Réduire le  réseau.

\begin{tiny}
  \begin{center}
    \xymatrix @R 6pt @C 4pt {
      &&& a \\
      &&& *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr]\ar@{-}[u] \\
      && *++[o][F-]{Plus}\ar[dl]\ar@{-}[dr] && *\txt{}\\
      &*\txt{}&&*\txt{}&& *++[o][F-]{Zero}\ar[ul]\\
      *++[o][F-]{Succ}\ar[ur] &&&& *++[o][F-]{Succ}\ar[ul]\\
      \\
      *++[o][F-]{Zero}\ar[uu] &&&& *++[o][F-]{Zero}\ar[uu]}
\end{center}
\end{tiny}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les interblocages}% 
  Il faut éviter les situations d'\brunir{interblocage}.

\bigskip

\centerline{
\xymatrix@R 18pt @C 12pt{
    &&&&\\
    & *++[o][F-]{~~~} \ar[r]\ar@{-}[u]\ar@{-}[l]& *\txt{} \ar@{-}[r] &
    *++[o][F-]{~~~} \ar[d]\ar@{-}[u]\ar@{-}[r]&\\ %1
    &*\txt{} \ar@{-}[u] && *\txt{} \ar@{-}[d] &\\ %2
    & *++[o][F-]{~~~} \ar[u]\ar@{-}[l]\ar@{-}[d]&*\txt{} \ar@{-}[l]&
    *++[o][F-]{~~~}\ar@{-}[d] \ar[l] \ar@{-}[r]&\\ %3
    &&&& %4
  } }
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE Le réseau d'interaction\\
          universel}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Universalité des réseaux d'interaction}% 
On peut coder par des réseaux d'interaction:
\begin{itemize}
\item les machines de Turing,
\item les automates cellulaires,
\item et, nous allons le voir, le $`l$-calcul.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Universalité des réseaux d'interaction}% 
On peut coder par des réseaux d'interaction:
\begin{itemize}
\item les machines de Turing,
\item les automates cellulaires,
\item et, nous allons le voir, le $`l$-calcul.
\end{itemize}
\vfill
Nous allons maintenant définir un \brunir{réseau universel}.%
\vfill \addtocounter{slide}{-1}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les noeuds}% 
\centerline{
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] \\
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl]\\ %2
&*\txt{}\ar[d]\\ %3
&}
%
\qquad \qquad %
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] \\
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`d}[d]&*\txt{}\ar@{-}[dl]\\ %2
&*\txt{}\ar[d]\\ %3
&}
%
\qquad\qquad 
\xymatrix @R 12pt @C 8pt{
 \\
*++[o][F-]{\varepsilon}\ar[u]
}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 10pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] && &&&&  &&&&\\ %1
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl]&&
&&&&*\txt{}\ar@{-}[u]&&&&*\txt{}\ar@{-}[u] \\ %2
&*\txt{}\ar@{-}[dd]&& &&&&*\txt{}\ar@{-}@/_/[dddd]
*\txt{}\ar@{-}[rr]\ar@{-}[ur]&\ar@{}|{`d}[u]&*\txt{}\ar@{-}[ul]
\ar@(d,u)@{-}[ddddrr]&&
*\txt{}\ar@{-}[rr]\ar@{-}[ur]\ar@(d,u)@{-}[ddddll]&\ar@{}|{`d}[u]&*\txt{}\ar@{-}[ul]*\txt{}\ar@{-}@/^/[dddd]\\% 3
\\%4
&*\txt{}&&\ar^{`g`d}[rr]&&&& &&& &&&
\\ % niveau de la flêche %5
\\%6
&*\txt{}\ar@{-}[uu]  \ar@{-}[dr]&&&& && *\txt{}\ar@{-}[rr]
*\txt{}\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl] &&*\txt{}\ar@{-}[rr]*\txt{}\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl]&\\ %7
*\txt{}\ar@{-}[rr]\ar@{-}[ur]& \ar@{}|{`d}[u]&*\txt{}\ar@{-}[ul]
&&&& && *\txt{} &&&& *\txt{}\ar@{-}[ul]\\ %8
\ar@{-}[u] && \ar@{-}[u] &&&&&& \ar@{-}[u] &&&& \ar@{-}[u] \\
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] &&&&& &&\\
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl] \\ %2
&*\txt{}\ar@{-}[d] &&&&&& *++[o][F-]{\varepsilon}\ar@{-}[uu] &&*++[o][F-]{\varepsilon}\ar@{-}[uu] \\ %3
&*\txt{}\ar@{-}[d] &&\ar^{`g\varepsilon}[rr]&&\\
&*++[o][F-]{\varepsilon}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] &&&&& &&\\
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`d}[d]&*\txt{}\ar@{-}[dl] \\ %2
&*\txt{}\ar@{-}[d] &&&&&& *++[o][F-]{\varepsilon}\ar@{-}[uu] &&*++[o][F-]{\varepsilon}\ar@{-}[uu] \\ %3
&*\txt{}\ar@{-}[d] &&\ar^{`d\varepsilon}[rr]&&\\
&*++[o][F-]{\varepsilon}}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] &&&& \ar@{-}[dddddd]&& \ar@{-}[dddddd]\\ %1
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`g}[d]&*\txt{}\ar@{-}[dl]\\ %2
&*\txt{}\ar@{-}[d]\\ %3
&*\txt{}&&\ar^{`g`g}[rr]&&\\ % niveau de la flêche %4
&*\txt{}\ar@{-}[u]  \ar@{-}[dr]\\ %5
*\txt{}\ar@{-}[rr]\ar@{-}[ur]& \ar@{}|{`g}[u]&*\txt{}\ar@{-}[ul]\\
\ar@{-}[u] && \ar@{-}[u] &&&& &&\\
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] &&&& \ar@{-}[d]&& \ar@{-}[d]\\ %1
*\txt{}\ar@{-}[rr]\ar@{-}[dr]&\ar@{}|{`d}[d]&*\txt{}\ar@{-}[dl]&&&&*\txt{}\ar@(d,u)@{-}[ddddrr]&&*\txt{}\ar@(d,u)@{-}[ddddll]\\ %2
&*\txt{}\ar@{-}[d] \\ %3
&*\txt{}&&\ar^{`d`d}[rr]&&\\ % niveau de la flêche %4
&*\txt{}\ar@{-}[u]  \ar@{-}[dr] &&&&& *\txt{}&& *\txt{}\\ %5
*\txt{}\ar@{-}[rr]\ar@{-}[ur]& \ar@{}|{`d}[u]&*\txt{}\ar@{-}[ul]&&&&*\txt{}&&*\txt{}\\
\ar@{-}[u] && \ar@{-}[u] &&&& \ar@{-}[u]&&\ar@{-}[u]\\
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les règles}% 
\xymatrix @R 12pt @C 8pt{
*++[o][F-]{\varepsilon}\ar@{-}[dd]\\
&& \ar^{\varepsilon\varepsilon}[rr]&&\\
*++[o][F-]{\varepsilon}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le résultat}%
  Yves Lafont a montré que ce réseau (très simple!) est universel, \\
  en ce sens que l'on peut y coder n'importe quel autre réseau.
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{\LARGE Le réseau d'interaction\\
          pour le lambda calcul}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les noeuds}% 

  \begin{tabular}{l@{\hspace*{100pt}}l}
\xymatrix@R 12pt @C 8pt{&&\\&@ \ar[dl]\ar@{-}[dr]\ar@{-}[u]\\&&}
&
\xymatrix@R 12pt @C 8pt{&&\\&`l \ar[u]\ar@{-}[dr]\ar@{-}[dl]\\&&}
\\\\
\xymatrix@R 12pt @C 8pt{&\\ *++[o][F-]{~~}\ar[u]}
&
\xymatrix@R 12pt @C 8pt{
\ar@{-}[d] && \ar@{-}[d] \\
`*\ar@{=}[rr]\ar@{=}[dr]&\ar@{}|{s}[d]&`(!)\ar@{=}[dl]\\
&*\txt{}\ar[d]&\\
&}
\end{tabular}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{L'élimination de $`b$-redex}% 
\xymatrix{
&& a \ar@{-}[d] &&&& a \ar@{-}[ddd]\\
&& \txt{@}\ar@{-}[ld]|@{>}|@{<}\ar@{-}[rd] &&\\
&`l x \ar@{-}[ld]\ar@{-}[rd] && d &&&& d\\
b && c &&& b \ar@/^1pc/@{-}[urr] & c
}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{@ contre fans}% 
\begin{center}
\xymatrix @R 10pt @C 8pt{
   % 1
  && a \ar@{-}[d] &&&&&& a \ar@{<-}[d] 
  \\
   % 2
  && *\txt{@}\ar@{-}[dl]|@{>}|@{<}\ar@{-}[dr] &&&&&& *\txt{} \ar@{=}[dr]\ar@{=}[dl]\ar@{}|{s}[d]
  \\
   % 3
  &*\txt{} \ar@{=}[dl]\ar@{=}[dr]\ar@{}|{s}[d] && d & \ar[rr] &&& `*\ar@{=}[rr] \ar@{-}[d] && `(!)\ar@{-}[d]
   \\
   % 4
`*\ar@{=}[rr]\ar@{-}[d]&&`(!)\ar@{-}[d] &&&&& *\txt{@} \ar[dl]\ar@{-}[drrr]&&*\txt{@}\ar[dl]\ar@{-}[drrr]&
   \\
   % 5
   b&&c &&&& b && c && `*\ar@{=}[rr]\ar@{=}[dr]  &\ar@{}|{s}[d] & `(!)\ar@{=}[dl] 
   \\
   % 6
   &&&&&&&&&&& *\txt{} \ar[d]\\
   % 7
   &&&&&&&&&&& d
}
\end{center}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{$`l$ contre fans}% 

\vspace*{12pt}

\begin{center}
    \xymatrix @R 12pt @C 8pt{
   % 1
      a \ar@{-}[d]&& b\ar@{-}[d]&&&&& a \ar@{<-}[d]&&& b \ar@{<-}[d] \\
   % 2
      `*\ar@{=}[rr]\ar@{=}[dr] & \ar@{}|{s}[d] &
      `(!)\ar@{=}[dl] &
      && &&`lx \ar@{-}[dl]\ar@{-}[drr]&&& `lx\ar@{-}[dll]\ar@{-}[dr] \\
   % 3
      & *\txt{}\ar@{-}[d] |@{>}|@{<}&& \ar[rr] &&& `*\ar@{=}[rr]\ar@{=}[dr] &
      \ar@{}|{s}[d] & `(!)\ar@{=}[dl] &
      `*\ar@{=}[rr]\ar@{=}[dr]
      & \ar@{}|{s}[d] & `(!)\ar@{=}[dl]  \\
   % 4
      & `lx\ar@{-}[dl]\ar@{-}[dr] &&&&&& *\txt{}\ar[d] &&&
      *\txt{}\ar[d] \\
   % 5
      c && d &&&&& c &&& d }
\end{center}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Fans contre fans (même noms)}% 
Les fans de même nom s'annihilent.

     \qquad  \qquad \qquad   
  \xymatrix @R 12pt @C 8pt{
   % 1
      a \ar@{-}[d]&& b\ar@{-}[d]&&&& a \ar@{-}[ddddd] && b\ar@{-}[ddddd]\\
   % 2
      `*\ar@{=}[rr]\ar@{=}[dr] & \ar@{}|{s}[d] & `(!)\ar@{=}[dl] \\
   % 3
      & *\txt{}\ar@{-}[d]|@{>}|@{<}  && \ar[rr] &&\\
   % 4
      & *\txt{} \\
   % 5
      `* \ar@{-}[d] \ar@{=}[ur]&\ar@{}|{s}[u] & `(!)\ar@{=}[ul]\ar@{=}[ll]\ar@{-}[d]\\
   % 6
      c && d &&&& c && d &&& }

 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Fans contre fans (noms différents)}% 
Les fans de noms différents se dupliquent.
 \begin{center}
\xymatrix @R 10pt @C 8pt{
   % 1
   a \ar@{-}[d]&& b\ar@{-}[d]&&&&& a  \ar@{<-}[d]&&&& b \ar@{<-}[d]\\
   % 2
   `*\ar@{=}[rr]\ar@{=}[dr] & \ar@{}|{s}[d] & `(!)\ar@{=}[dl] &&&&%
   & \txt{} \ar@{=}[dl] \ar@{=}[dr] \ar@{}|{t}[d]&&& &\txt{} \ar@{=}[dl] \ar@{=}[dr] \ar@{}|{t}[d]
   \\
   % 3
   & *\txt{}\ar@{-}[d]|@{>}|@{<}  && \ar[rr] &&& %
   `*\ar@{=}[rr]\ar@{-}[d]&& `(!)\ar@{-}[drr] && %
   `*\ar@{=}[rr]\ar@{-}[dll]&& `(!)\ar@{-}[d] 
   \\
   % 4
   & *\txt{} &&&&& %
   `*\ar@{=}[dr]\ar@{=}[rr]&&`(!)\ar@{=}[dl] %
   &&`*\ar@{=}[dr]\ar@{=}[rr]&&`(!)\ar@{=}[dl] %
   \\
   % 5
   `* \ar@{-}[d] \ar@{=}[ur]&\ar@{}|{t}[u] &
   `(!)\ar@{=}[ul]\ar@{=}[ll]\ar@{-}[d]  &&&& %
    &*\txt{} \ar[d]  \ar@{}|{s}[u] &&&&*\txt{} \ar[d] \ar@{}|{s}[u] &
   \\
   % 6
   c && d &&&&& c &&&& d &&&
}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les noms des fans}% 
Préserver correctement les noms des fans est un problème difficile qui
n'est pas abordé dans ce cours.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Effaceur contre @}% 

\vspace*{12pt}

\qquad  \qquad \qquad    \xymatrix @R 10pt @C 8pt{
      &a&&&a && *++[o][F-]{~} \ar@{-}[dd]|@{>}\\
      &@ \ar@{-}[dl]|@{>}\ar@{-}[dr]\ar@{-}[u]
      &\ar[r]&&\\
      *++[o][F-]{~} \ar@{-}[ur]|@{>}&& b&&*++[o][F-]{~} \ar@{-}[uu]|@{>} && b
    }
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Effaceur contre $`l$}% 

 \vspace*{12pt}

   \qquad  \qquad \qquad      \xymatrix @R 10pt @C 8pt{
      &*++[o][F-]{~} \ar@{-}[dd]|@{>}&&&&&*++[o][F-]{~} \ar@{-}[ddd]|@{>} &&*++[o][F-]{~} \ar@{-}[ddd]|@{>}\\
      &&&\ar[rr]&&\\
      &`l \ar@{-}[uu]|@{>}\ar@{-}[dl]\ar@{-}[dr]\\
      a&&b&&&&a\ar@{-}[uuu]&&b\ar@{-}[uuu] }

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Effaceur contre fan}% 
  
 \vspace*{12pt}

   \qquad  \qquad \qquad        \xymatrix @R 12pt @C 8pt{
   % 1
      a \ar@{-}[d]&& b\ar@{-}[d]&&&& a && b  \\
   % 2
      `*\ar@{=}[rr]\ar@{=}[dr] & \ar@{}|{s}[d] &
      `(!)\ar@{=}[dl] &
      && && \\
   % 3
      & *\txt{}\ar@{-}[d] |@{>}|@{<}&& \ar[rr] &&&
      \\
   % 4
     &&    \\
   % 5
       & *++[o][F-]{~} \ar@{-}[uu]&&&&& *++[o][F-]{~} \ar@{-}[uuuu]|@{>}&& *++[o][F-]{~} \ar@{-}[uuuu]|@{>}
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Effaceur contre effaceur}% 

\vspace*{12pt}


    \qquad  \qquad \qquad    \xymatrix{
*++[o][F-]{~} \ar@{-}[dd]|@{>}\\
&\ar[rr]&&\\
*++[o][F-]{~} \ar@{-}[uu]|@{>}}

  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\large \bf \color{vertfonce}{\textit{Un exemple}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Le terme $`l z . (`l x . x\:x)\:(`l y . z)$} 
\hspace*{40pt}  \xymatrix @R 6pt @C 4pt{
  & \\
  &    `l z \ar[u]
            \ar@{-}[drrr] \\
  &&&&  @   \ar@{-}[drr]|@{<}
            \ar@{-}[dll] |@{>}|@{<} \\
  &&   `l x \ar@{-}[dr]
  &&&& `l y \ar@{-}[dl]
            \ar@{-}@(dr,r)[dddddlll] \\
  &&&  @    \ar@{-}[dr]
            \ar@{-}[dl]
  &&   *++[o][F-]{~} \ar@{-}[ur]|@{>}&&&\\
  &&   `*   \ar@{=}[rr]
            \ar@{=}[dr]
  &         \ar@{}|{s}[d]
  &    `(!) \ar@{=}[dl]&\\
  &&&  *\txt{} \ar@(d,dl)@{-}[uuul]|@{>} &&&&\\
  &&&&\\
  &&&  *\txt{} \ar@{-}@(l,dl)[lluuuuuuu]\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%  \heading{Le terme $`l z . (`l x . x\:x)\:(`l y . z)$}% 
\qquad\qquad \qquad\qquad  \xymatrix @R 6pt @C 4pt{
 &&  \\
 &&     `l z \ar[u]  \\\\
 &&&   @    \ar@{-}[dr]
            \ar@{-}[dl]
     \ar@{-}[uul]|@{>}&&&\\
     && `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&&\ar@{-}[dd]|@{>}\\
&&&\\
&&&`l y\ar@{-}[dl]\ar@{-}@(dr,r)[ddl]\ar@{-}[uu]|@{>}\\
&&  *++[o][F-]{~} \ar@{-}[ur]|@{>}\\
&&  *\txt{} \ar@{-}@(l,dl)[uuuuuuuu]|@{>}\\%point relais pour la flèche entre `lz et `ly
}
 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}\label{page:bifurcation}
\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
 &&&  \\
 &&&     `l z \ar[u]  \\\\
 &&&&   @    \ar@{-}[dr]
            \ar@{-}[dl]|@{>}
     \ar@{-}[uul]|@{>}&&&\\
 &&& `l y \ar@{-}[ur]|@{>}\ar@{-}[dll]\ar@{-}[dr]&& `l y\ar@{-}[dll]\ar@{-}[dr]\\
     & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl] 
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&\ar@{-}[dd]|@{>}& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&  *++[o][F-]{~} \ar@{-}[uu]|@{>}\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\qquad\qquad \qquad\qquad  
  \xymatrix @R 6pt @C 4pt{
 &&&  \\
 &&&     `l z \ar[u]  \\\\
 &&&&   @    \ar@{-}[dr]
            \ar@{-}[dl]|@{>}
     \ar@{-}[uul]|@{>}&&&\\
 &&& `l y \ar@{-}[ur]|@{>}\ar@{-}[dl]|@{<}\ar@{-}[dr]&& `l y\ar@{-}[dll]|@{<}\ar@{-}[dr]\\
     && *++[o][F-]{~}  &*++[o][F-]{~} 
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}\label{page:retour}
\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
&&&  \\
 &&&     `l z \ar[u] \ar@{-}[ddddr] \\
 &&&&&*++[o][F-]{~} \ar@{-}[dd]|@{>}\\
 &&&&&&&\\
 &&&&&  `l y\ar@{-}[dlll]|@{<}\ar@{-}[dr]\ar@{-}[uu]|@{>}\\
     &&  *++[o][F-]{~} &
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
&&&  \\
 &&&     `l z \ar[u] \ar@{-}[ddddr] \\
 &&&&&\\
 &&&&&& *++[o][F-]{~} \ar@{-}[dd]|@{>} &&&*++[o][F-]{~} \ar@{-}[dd]|@{>} \\
 &&&&& \\
     &&&
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]
&&& *++[o][F-]{~} \ar@{-}[uu]|@{>} \\
&&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
&&&  \\
 &&&     `l z \ar[u] \ar@{-}[ddddr] \\
 &&&&&\\
 &&&&&& *++[o][F-]{~} \ar@{-}[dd]|@{>} \\
 &&&&& \\
     &&&
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Ce qui est une des représentations possibles de \bleu{`l z . z}.

Le \bleu{z} n'est partagé avec rien.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{small}
    Notons qu'à partir du réseau de la page~\ref{page:bifurcation}
  \end{small}

  \qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
 &&&  \\
 &&&     `l z \ar[u]  \\\\
 &&&&   @    \ar@{-}[dr]
            \ar@{-}[dl]|@{>}
     \ar@{-}[uul]|@{>}&&&\\
 &&& `l y \ar@{-}[ur]|@{>}\ar@{-}[dll]\ar@{-}[dr]&& `l y\ar@{-}[dll]\ar@{-}[dr]\\
     & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl] 
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&\ar@{-}[dd]|@{>}& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&  *++[o][F-]{~} \ar@{-}[uu]|@{>}\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{small}
on obtient aussi le réseau
\end{small}

\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
 &&&  \\
 &&&     `l z \ar[u]  \ar@{-}[ddddr]\\\\
 &&&&   \\
 &&& && `l y\ar@{-}[dll]\ar@{-}[dr]\ar@{-}@(u,u)[lllld]\\
     & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl] 
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&\ar@{-}[dd]|@{>}& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&  *++[o][F-]{~} \ar@{-}[uu]|@{>}\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{small}
et on retrouve par contraction de la paire active le réseau de la
page~\ref{page:retour}. 
\end{small}

\qquad\qquad \qquad\qquad  
 \xymatrix @R 6pt @C 4pt{
&&&  \\
 &&&     `l z \ar[u] \ar@{-}[ddddr] \\
 &&&&&*++[o][F-]{~} \ar@{-}[dd]|@{>}\\
 &&&&&&&\\
 &&&&&  `l y\ar@{-}[dlll]|@{<}\ar@{-}[dr]\ar@{-}[uu]|@{>}\\
     &&  *++[o][F-]{~} &
           & `*   \ar@{=}[rr]
            \ar@{=}[dr]
           &\ar@{}|{s}[d]
           & `(!) \ar@{=}[dl]\\
&&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
&&\\
&&\\
  *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\%point relais pour la flèche entre `lz et `ly
}
\vfill
\brunir{Mettant en évidence la confluence!}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La philosophie}
Les réseaux d'interaction font du partage de \brunir{code} et du
partage des \brunir{paramètres}.

Partage le code suppose de savoir «départager» quand on fait des
calculs. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La philosophie}
Dans un cadre théorique qui sait identifier les «clones» de fans,
on peut montrer que les réseaux implantent une \brunir{réduction optimale du
lambda calcul}, c'est-à-dire,
\begin{itemize}
\item qu'ils minimisent le nombre de réductions de $`b$-redex,
  \begin{displaymath}
       \xymatrix @C 1pt @ R 3pt{
         && a \ar@{-}[d] \\
         && \txt{@}\ar@{-}[ld]|@{>}|@{<}\ar@{-}[rd]\\
         &`l x \ar@{-}[ld]\ar@{-}[rd] && d \\
         b && c
       }
  \end{displaymath}
\item mais en revanche ils augmentent considérablement la
  \brunir{bureaucratie}.  C'est-à-dire les réductions qui concernent les fans.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La décompilation}
A la fin du processus, il faut \brunir{décompiler} le réseau en un
terme du lambda-calcul.


On s'aperçoit que plusieurs réseaux peuvent correspondre à un
même terme.

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

\qquad\qquad \qquad\qquad  
  \xymatrix @R 3.8pt @C 2.3pt{
    &&&  \\\\
    &&&     `l z \ar[uu] \ar@{-}[ddddr] \\
    &&&&&\\
    &&&&&& *++[o][F-]{~} \ar@{-}[dd]|@{>} \\
    &&&&& \\
    &&& & `* \ar@{=}[rr] \ar@{=}[dr] &\ar@{}|{s}[d]
    & `(!) \ar@{=}[dl]\\
    &&& && \ar@(d,r)@{-}[dddlllll]|@{>} \\
    &&\\
    &&\\
    *\txt{} \ar@{-}@(l,dl)[uuuuuuuurrr]|@{>}&&\\ %point relais pour
                                %la flèche entre `lz et `ly 
  }
et \qquad\qquad    \xymatrix @R 12pt @C 8pt{
&`l \ar@(dr,dl)@{-}[]|@{>}\\
&&
}
\vfill
correspondent au même terme \bleu{`l z. z}.

\end{slide}
%------------------------------------------------------
\end{document}
% LocalWords:  épithéorie garbarge d'optimisations n'apparaissent Strachey IMP
% LocalWords:  d'indifférence Wadsworth tail-recursive OCAML CPS Meyer Mitchell
% LocalWords:  Wand Semantics Typed Lambda-Calculi Logic of Programs LNCS
% LocalWords:  Springe Krivine
