%% Time-stamp: %% 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{$\lambda\mathsf{x}$ et la normalisation}}} \title{\color{red}{\textit{Sémantique opérationnelle 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 2003\hfill\logoENS } \newpagestyle{AvecLogos}% {\hfil \thepage \rightmark} {\logos} \pagestyle{AvecLogos} %\pagestyle{empty} \slidestyle{empty} \slideframe{} %--- couleurs ---- \input{mes_couleurs} \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{green}{\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 \rouge{ultimate analysis} of substitutions in terms of a system of \rouge{extreme simplicity}. The theory of lambda-conversion is intermediate in character between synthetic theories and ordinary logic ... and it has the advantage of \rouge{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 réduction $\beta$?} La définition habituelle de la réduction $\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 à \emph{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 à \emph{remplacer} une variable par un terme. La substitution est une opération \emph{complexe} \begin{itemize} \item dans son \verdir{calcul} -- la même notation peut évoquer une opération coûteuse ou une opération bon marché, ça n'est pas réaliste --, \item et dans son \verdir{implantation}, les \emph{captures} sont difficiles à prendre en compte. \end{itemize} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Qu'est-ce qu'une substitution?} Traditionnellement, la \rouge{substitution} n'est pas définie dans la \emph{théorie}, \ali mais dans l'\rouge{épithéorie}. \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Qu'est-ce qu'une substitution?} Traditionnellement, la \rouge{substitution} n'est pas définie dans la \emph{théorie}, \ali mais dans l'\rouge{é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 \rouge{substitution} n'est pas définie dans la \emph{théorie}, \ali mais dans l'\rouge{é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 \emph{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} \emph{libre} et \emph{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 \end{array} \end{math} \end{center} \vspace*{10pt} Un terme de la forme \bleu{M} s'appelle une \emph{clôture}. Dans \bleu{M} 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 \emph{«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 \emph{«variable disponible»}. \vspace*{1cm} Une variable est \emph{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} \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}. \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) & = & (AV(M)\backslash \{x\})\cup AV(N) & \mbox{if $x\in AV(M)$}\\ AV(M) & = & 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 \\ [2pt] \emph{(App)} & \quad (M N) & \quad "->" \quad & M \, N \\ \emph{(Abs)} & \quad (`l y . M)& \quad "->" \quad & `l y . (M)\\ \emph{(VarI)} & \quad x & \quad "->" \quad & A \\ \emph{(VarK)} & \quad y & \quad "->" \quad & y \\ \emph{(gc)} & \quad M & \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 \\ [2pt] \emph{(App)} & \quad (M N) & \quad "->" \quad & M \, N \\ \emph{(Abs)} & \quad (`l y . M)& \quad "->" \quad & `l y . (M)\\ \emph{(VarI)} & \quad x & \quad "->" \quad & A \\ \emph{(VarK)} & \quad y & \quad "->" \quad & y \\ \emph{(gc)} & \quad M & \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)}}. Elle 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{De Bruijn's indices} \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 Presentation of $`l `y $}}} \end{center} \vfill {\footnotesize Un peu d'anglais ne fait pas de mal.} \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Rule 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)} introduces two new operators. The syntax is extended. \begin{eqnarray*} \rouge{/} &\bl{:}& {\color{cyanp}`L`y "->" Substitution}\\ \rouge{\_[\_]} &\bl{:}& {\color{cyanp} `L`y \times Substitution "->" `L`y} \end{eqnarray*} $\rouge{/}$ and \rouge{\_[\_]} introduce a new sort \({\color{cyanp}Substitution}\). \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Closures} \rouge{\_[\_]} must be defined, by other rules, i.e., \begin{itemize} \item distributed through applications and abstractions, \item defined on variables (de~Bruijn's indices). \end{itemize} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Closures} \rouge{\_[\_]} must be defined, by other rules, i.e., \begin{itemize} \item distributed through applications and abstractions, \item defined on variables (de~Bruijn's indices). \end{itemize} \vspace*{1cm} Terms of the form \rouge{\(M[s]\)} are called \rouge{closures}. They are true terms in the \verdir{calculus of explicit substitution}. \vfill Teems without closure are called \emph{pure terms}. \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Distributing substitutions} \subheading{Through 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{Distributing substitutions} \subheading{Through 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{Through 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) introduces a new operator \[\rouge{\Uparrow}(s) : {\color{cyanp}Substitution "->" Substitution}.\] \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Defining \rouge{/} and \(\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{Defining \rouge{/} and \(\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)} introduces a new constant \(\rouge{\uparrow} : {\color{cyanp}Substitution}\) \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Defining \(\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{Computations in $`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{Computations in $`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 \end{slide} %---------------------------------------------------------------------------- \begin{slide} \heading{Computations in $`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 \end{slide} %---------------------------------------------------------------------------- \begin{slide} \heading{Computations in $`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 \end{slide} %---------------------------------------------------------------------------- \begin{slide} \heading{Computations in $`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 \end{slide} %---------------------------------------------------------------------------- \begin{slide} \heading{Computations in $`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 \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 Properties of $`l `y $}}} \end{center} \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Facts} \begin{itemize} \item $`l `y = (B) \oplus `y $. \item $`y $ is \rouge{orthogonal} \ali i.e., left-linear and without critical pair. \item $`y $ is \rouge{terminating} \ali i.e., \rouge{strongly normalizing}. \end{itemize} \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Questions} \begin{description} \item[\emph{Does this calculus represent}] \emph{\bf the classical $`l $-calculus?} \vspace*{1cm} \end{description} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Questions} \begin{description} \item[\emph{Does this calculus represent}] \emph{\bf the classical $`l $-calculus?} \verdir{Yes} % \ali \bleu{M \rabeta P} is \bleu{M \raB N} and \bleu{N \rarasub{`y } P}. \end{description} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Questions} \begin{description} \item[\emph{Is the specification complete?}] \end{description} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Questions} \begin{description} \item[\emph{Is the specification complete?}]~ How about a rule \bl{\[M[s][t] "->" M[\dots s \dots t \dots]\]} where \bleu{[\dots s \dots t \dots]} is \bleu{[s `o t]} for instance? \end{description} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Questions} \begin{description} \item[\emph{Is the specification complete?}]~ How about a rule \bl{\[M[s][t] "->" M[\dots s \dots t \dots]\]} where \bleu{[\dots s \dots t \dots]} is \bleu{[s `o t]} for instance? \vfill \verdir{No need,} since every closure can be removed in \rouge{ground terms}. \end{description} \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{The substitution lemma} \bleu{`l `y } admits a \emph{critical pair} \bl{\[\emph{\langle} M[\Lift(s)][P[s]/] \emph{~,~} M[P/][s]\emph{\rangle}\]} \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{The substitution lemma} \bleu{`l `y } admits a \emph{critical pair} \bl{\[\emph{<} M[\Lift(s)][P[s]/] \emph{~,~} M[P/][s]\emph{>}\]} \vfill Note that usually the identity \bl{\[M[\Lift(s)][P[s]/] = M[P/][s]\]} is called the \rouge{substitution lemma}. \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{The substitution lemma} \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{The substitution lemma} \vspace*{40pt} The substitution lemma is an inductive theorem in \(`l `y \). \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Projection Lemma} If \bleu{M\ \raB\ P} then \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)} } It is a consequence of substitution lemma. \vfill \end{slide} %---------------------------------------------------------------------- \begin{slide} \heading{Confluence of $`l `y $} $`l `y $ is confluent on ground terms. This is a consequence of \rouge{projection lemma}. \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 \) preserves strong normalisation} If a term \bleu{M} is \rouge{strongly $\beta$ normalising}, % \ali then \bleu{M} is \rouge{strongly \(`l `y \) normalising}. The proof is by contradiction, based on the existence of a smallest counter-example. \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] & \emph{\textit{(Environnement d'évaluation)}}\\ M, N \: &::=& \: \und{n}\: |\: `l M\:|\: M\:N & \emph{\textit{(Code)}}\\ s, t \: &::=& \: id \: |\: U `. s & \emph{\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 \emph{formes normales} sont \bleu{(`l M)[s]}, on les appelle aussi les \emph{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 \emph{états} et des \emph{transitions}. L'état \bleu{c \sep e \sep s} de la machine de Krivine comporte trois composantes : \begin{itemize} \item le \emph{code} \bleu{c}, \item l'\emph{environnement} \bleu{e}, \item la \emph{pile} \bleu{s}. \end{itemize} \vfill \end{slide} %------------------------------------------------------ \begin{slide} \heading{Les états}% Une machine abstraite comporte des \emph{états} et des \emph{transitions}. L'état \bleu{c \sep e \sep s} de la machine de Krivine comporte trois composantes : \begin{itemize} \item le \emph{code} \bleu{c}, \item l'\emph{environnement} \bleu{e}, \item la \emph{pile} \bleu{s}. \end{itemize} \vspace*{12pt} \bleu{\begin{array}{rclll} M,N &::=& `l M ~|~ M\:N ~|~ \und{n} && \emph{\textit{(Code)}}\\ e &::=& `. e ~|~ \mathsf{nil} &&\emph{\textit{(Environnement)}}\\ s &::=& :: s ~|~ [~] &&\emph{\textit{(Pile)}} \end{array} } \vfill \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*} M\: N \sep e \sep s & "->" & M \sep e \sep :: s\\ `l M \sep e \sep :: s & "->" & M \sep `. e \sep s\\ 0 \sep `. e \sep s & "->" & N \sep f \sep s \\ n+1 \sep `. 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'\emph{appel par nom}. La partie du corps de la fonction est évaluée avant les arguments. L'\emph{état de départ} est % \bleu{M \sep \mathsf{nil} \sep [~]}. Les \emph{é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 \emph{tas} («heap» en anglais) \bleu{h} qui fait correspondre à chaque adresse un 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} && \emph{\textit{(Code)}}\\ e &::=& a `. e ~|~ \mathsf{nil} &&\emph{\textit{(Env)}}\\ s &::=& a :: s ~|~ [~] &&\emph{\textit{(Pile)}}\\ u &::=& (s,a) :: u ~|~ [~] && \emph{\textit{(Pile de mise à jour)}}\\ h &::=& \{~\} ~|~ h\{a "|->" \} && \emph{\textit{(Tas)}}\\ a && \emph{\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 "|->"\} && \emph{\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 && \emph{\textit{(Lam)}}\\ \und{n+1} \sep a `. e\sep s \sep u \sep h &"->"& \und{n} \sep e\sep s \sep u \sep h && \emph{\textit{(Skip)}}\\ \und{0} \sep a `. e\sep s \sep u \sep h &"->"& N \sep e'\sep [~] \sep (s, a) :: u \sep h && \emph{\textit{(Access)}}\\ && \quad \textrm{où~} h~a = \\ `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>\} && \emph{\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 \emph{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 \emph{programme--résultat} est dite \emph{sémantique à grandes étapes} \textit{(big steps)}. \ali La notation habituelle est \bleu{M \downarrow N}. On parle aussi de \emph{sémantique opérationnelle structurée} (en anglais SOS) (due à Plotkin et 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{displaymathbleu} \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{displaymathbleu} \end{scriptsize} \vfill \end{slide} %------------------------------------------------------ \begin{slide} \heading{L'appel par valeur en sémantique à grandes étapes}% Dans la suite une \emph{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{\emph{~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{\emph{~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{displaymathbleu} \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{displaymathbleu} \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 \emph{flot de contrôle} dans les langages de programmation. Dans cette méthode un terme est évalué dans un contexte qui représente le \emph{«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}% 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 \emph{contexte} est appelé une \emph{continuation}. % \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 origines}% La \emph{sémantique par continuation} explique des phénomènes que la \emph{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 \emph{implantations efficaces et souples}. % \vfill \end{slide} %------------------------------------------------------ \begin{slide} \heading{Les origines}% La sémantique par continuation est aussi appelé \verdir{style de passage de continuations}, en anglais \verdir{continuation passing style}, ou pour faire court \verdir{CPS}. Elle fait une \emph{traduction} du lambda-calcul vers lui-même. C'est même une \emph{véritable compilation} du lambda-calcul dans le lambda-calcul. % \vfill \end{slide} %------------------------------------------------------ \begin{slide} \heading{Les origines}% \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 sémantique par continuation avec la sémantique directe \emph{\includegraphics[width=.4cm]{attention.eps} un peu costaud!} \end{itemize} % \vfill \end{slide} %------------------------------------------------------ \begin{slide} \heading{Les origines}% Notre inspiration vient d'un article d'Albert Meyer et Mitchell Wand, intitulé, \emph{\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} (qui pas nécessairement de base) qui est le type des \emph{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 \emph{représentation} de \bleu{`a}, \item et une \emph{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}% En bref, pour l'application, \begin{itemize} \item Si on a une \emph{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 \emph{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 \emph{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 \emph{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 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 \emph{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 \emph{retract} de \bleu{`b} et on écrit \bleu{`a\triangleleft `b} s'il existe des applications lambda-définissables \bleu{i:`a"->"`b} et \bleu{j:`b"->"`a} telles que \bleu{j`o i} soit l'identité sur \bleu{`a}. \vspace*{2mm} Le couple \bleu{(i,j)} forme la \emph{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} Notons que \bleu{\Ia} n'est pas le combinateur habituel \bleu{`l x:`a.x}. \vspace*{3mm} 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 \emph{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é. 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} \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} \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 \emph{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 \emph{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}% \emph{La propriété 1.} dit que les représentations canoniques et les images de combinateurs sont «légales». \emph{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 réduction fait des duplications, il faut d'abord réduire les redex avant qu'elle ne les duplique. Si une réduction fait disparaître le résidu d'un redex il n'aurait pas fallu le contracter. \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)} &"->"& \emph{(Iz)} \: (Iz) &"->"& z \: \emph{(Iz)} &"->"& z\: z \\ \rouge{(`l y . (yy))\:(Iz)} &"->"& (Iz) \: \emph{(Iz)} &"->"& z \: \emph{(Iz)} &"->"& z\: z \\ (`l y . (yy))\:\emph{(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 \emph{réseau} est un graphe (cyclique) non orienté dont les noeuds sont étiquetés. Un ensemble fini et fixé de \emph{ports} est attribué à chaque étiquette. L'un des ports est appelé \emph{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 \emph{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 \emph{règle d'interaction} est un couple de paires actives qui satisfont les conditions 1, 2 et 3. \verdir{Propriété 1,} \emph{Linéarité :} Dans chaque règle, chaque variable a exactement deux occurrences: l'un dans le membre gauche et l'autre dans le membre droit. \verdir{Propriété 2,} \emph{Non ambiguïté :} Il y a au plus une règle pour chaque paire active. \verdir{Propriété 3,} \emph{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} \emph{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} \begin{center} {\large \bf \color{vertfonce}{\textit{\LARGE Le réseaux 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} 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 \emph{Mettant en évidence la confluence!} \end{slide} %------------------------------------------------------ \begin{slide} \heading{La philosophie} Les réseaux d'interaction font du partage de \emph{code} et du partage des \emph{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 \emph{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 \emph{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 \emph{décompiler} le réseau en un terme du lambda-calcul. On s'aperçoit que plusieurs réseaux peuvent correspondre un à une 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 % LocalWords: d'indifférence Wadsworth tail-recursive