% Time-stamp: <modified on 23 Nov 2004 at 09:51 by Pierre Lescanne>
%% objets.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[all]{xy}
\usepackage{qsymbols}
\usepackage{prooftree}
                                            % avec dvips


\slidesmag{5}
\articlemag{1}


\title{\color{red}{\textit{Les langages à objets}}}

\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}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                symboles
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\newcommand{\ratwo}{\stackrel{\scriptscriptstyle 2}{\longrightarrow}}
\newcommand{\imp}{\rightarrow}
\newcommand{\rra}{\rouge{"->"}}
\newcommand{\rrastar}{\rouge{\rastar}}
\newcommand{\rratwo}{\rouge{\ratwo}}
\newcommand{\ali}{\newline\hspace*{20pt}}
\newcommand{\vdach}{\mathrel{\bl{\vdash}}}
\newcommand{\substit}[3]{#1[#2\leftarrow #3]}
\newcommand{\osubst}[3]{#1\{\!\!\{#2\leftarrow #3\}\!\!\}}
\newcommand{\jdgv}[3]{\bleu{#1\vdash\verdir{#2}, #3}}
\newcommand{\jdge}[3]{\bleu{#1, \verdir{#2} \vdash #3}}
\newcommand{\jdg}[2]{\bleu{#1\vdash #2}}
\newcommand{\Jdgv}[3]{#1\vdash\verdir{#2}, #3}
\newcommand{\Jdge}[3]{#1, \verdir{#2} \vdash #3}
\newcommand{\Jdg}[2]{#1\vdash #2}
\newcommand{\und}[1]{\underline{#1}}
\newcommand{\x}{\ensuremath{\textbf{x}}}
\newcommand{\y}{\ensuremath{\textbf{y}}}
\newcommand{\lx}{\ensuremath{`l \texttt{x}}}
\newcommand{\lxgc}{\ensuremath{`l \texttt{x}_{gc}}}
\newcommand{\F}{\ensuremath{{\cal F}}}
\newcommand{\T}{\ensuremath{{\cal T}}}
\newcommand{\I}{\mathbf{I}}
\newcommand{\K}{\mathbf{K}}
\renewcommand{\S}{\mathbf{S}}
\newcommand{\llbda}{\mathbf{\lambda\hspace{-.58em}\lambda}}
\newcommand{\Nat}{\mathbb{N}}
\newcommand{\interp}[3]{\llbracket#1\rrbracket^{#2}_{#3}}
\newcommand{\modval}[3]{#1\rouge{(}#2\rouge{:=}#3\rouge{)}}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%                new qsymobls
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newqsymbol{`ù}{\upharpoonright}
\newqsymbol{"'|`"}{\uparrow}
\newqsymbol{`8}{\infty}
\newqsymbol{"=^="}{\triangleq}
\newqsymbol{`£}{\varsigma}
\newqsymbol{"`="}{\leftharpoonup\!\!\!\!\!\!\!\!\raisebox{-.5ex}{$\leftharpoondown$}~}
\newqsymbol{`«}{\langle\hspace{-1.8pt}\langle}
\newqsymbol{`»}{\rangle\hspace{-1.8pt}\rangle}

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%        les symboles pour les substitutions explicites
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%% <...> are angle brackets.
\mathcode`\<=\string"4268 \mathcode`\>=\string"5269 %

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

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

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

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

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


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

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

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

\newenvironment{mathbleu}[1]{$\color{blue}#1}{$}

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

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

\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

\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}
  \heading{Les primitives du \(`£\)-calcul}
%

Le \emph{\(`£\)-calcul} est un calcul d'objets à la manière du
$`l$-calcul comme calcul de fonctions.

Le \(`£\)-calcul est un calcul minimaliste au même sens que le $`l$-calcul.

Un objet est composé de \emph{méthodes} et de \emph{champs}.

On \verdir{accède}  à un  \emph{champs} ou on le \verdir{modifie} 

On \verdir{accède}  à une  \emph{méthode} ou on la \verdir{modifie} 

\end{slide}
%------------------------------------------------------
\begin{slide}
  \heading{Les primitives du \(`£\)-calcul}
%
  
  En première approximation on peut considérer les champs comme des
  méthodes particulières.
  
  Un objet sera donc une collection de méthodes avec deux opérations
\begin{itemize}
\item \emph{invocation},
\item \emph{modification},
\end{itemize}

\emph{self} est une entité qui apparaît dans une méthode et représente
l'objet auquel la méthode appartient.

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les primitives du \(`£\)-calcul}

\begin{footnotesize}
\begin{mathbleu}
  \begin{array}{l@{\quad}l}
    `£(x) b & \noir{méthode avec comme paramètre} x \noir{et comme
    corps} b \\\\ %
  {[}l_1=`£(x_1)b_1,...,l_n=`£(x_n)b_n{]} & \noir{objet
    contenant} n \noir{méthodes} l_1,..., l_n\\\\ %
  o.l & \noir{invocation de la méthode } l \noir{de l'objet} o\\\\
  o.l "`=" `£(x) b & \noir{modification de la méthode} l \noir{de
    l'objet} o \\ %
  &\noir{avec remplacement par la méthode} `£(x) b
  \end{array}
\end{mathbleu}
\end{footnotesize}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les primitives du \(`£\)-calcul}

Un objet est donc composé de \bleu{n} composants
\bleu{l_i=`£(x_i)b_i}.

Les \emph{étiquettes} \bleu{l_i} sont tous distinctes.

L'ordre des composants n'a pas d'importance.

L'invocation d'un méthode s'écrit \bleu{o.l} où \bleu{l} est une étiquette
de \bleu{o}.  

Le but est d'exécuter la méthode nommée \bleu{l} de \bleu{o} auquel on
attache le paramètre \bl{\textit{self}} et de retourner le résultat de
cette exécution.


\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Les primitives du \(`£\)-calcul}
Une modification de méthode est écrite \bleu{o.l "`=" `£(x) b}. \ali On
produit une copie de \bleu{o} \ali où la méthode \bleu{l} est remplacée
  par \bleu{`£(x) b}.

Il s'agit d'une modification sans mutation, dite aussi
\emph{fonctionnelle}.

L'objet \bleu{o} est recopié avant qu'on lui change sa méthode \bleu{l}.

Les objets sont \emph{immuables}. 

Il n'y a donc pas de «modification en place» des objets. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un exemple}
\begin{displaymathbleu}
  [l_1 = `£(x_1)[~], l_2 = `£(x_2)x_2.l_1]
\end{displaymathbleu}
est un objet qui contient deux méthodes.

La première méthode, nommée \bleu{l_1} retourne un objet vide
\bleu{[~]}.

La seconde méthode \bleu{l_2} invoque la première méthode à travers le
paramètre \bleu{x_2}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La sémantique primitive}
%
On représente les objets par \bleu{o`=[l_i=`£(x_i) b_i~^{i`:1..n}]}.

\emph{Réduction d'une invocation}
\begin{eqnarraybleu}
  o.l &">->"& \osubst{b_i}{x_i}{o}
\end{eqnarraybleu}
\emph{Réduction d'une modification}
\begin{eqnarraybleu}
  o.l_j"`=" `£(y)b  &">->"&  [l_j=`£(y) b, l_i=`£(x_i) b_i~ ^{i`:1..n-\{j\}}]
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Un exemple}
%
Soit l'objet
\begin{displaymathbleu}
  o_1 "=^=" [l = `£(x)[\ ]]
\end{displaymathbleu}
alors
\begin{displaymathbleu}
  o_1.l ">->" \osubst{[~]}{x}{o_1} `= [~]
\end{displaymathbleu}
\begin{displaymathbleu}
  o_1.l"`=" `£(y)o_1 ">->" [l=`£(y)o_1]
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On peut facilement écrire des programmes qui ne terminent pas sans
utiliser explicitement la récursion.

Soit 
\begin{displaymathbleu}
  o_2"=^=" [l = `£(x)x.l]
\end{displaymathbleu}
alors
\begin{displaymathbleu}
  o_2.l ">->" \osubst{x.l}{x}{o_2} `= o_2.l ">->" ...
\end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  La substitution de «self» permet à une méthode de retourner ou de
  modifier «self» \ali c'est-à-dire de modifier ou de retourner
  l'\emph{objet lui-même}.

Soit
\begin{displaymathbleu}
  o_3"=^=" [l = `£(x)x]
\end{displaymathbleu}
alors
\begin{displaymathbleu}
  o_3.l ">->" \osubst{x}{x}{o_3} `= o_3
\end{displaymathbleu}
Soit
\begin{displaymathbleu}
  o_4"=^=" [l = `£(y)(y.l"`="`£(x)x)]
\end{displaymathbleu}
alors
\begin{displaymathbleu}
  o_4.l ">->" (o_4.l"`="`£(x)x) ">->" o_3
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Cette faculté de l'objet de se modifier lui-même est une
caractéristique des \emph{langages à prototype}.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{La syntaxe}
\begin{eqnarraybleu}
  a, b &::=& x ~|~ [l_i=`£(x_i) b_i~^{i`:1..n}] ~|~ a.l ~|~ a.l"`="`£(x)b
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Notations}
Si dans une méthode \bleu{`£(x) b}, \bleu{b}  ne contient pas
\bleu{x}, on peut considérer qu'il s'agit d'un champ. 

Si \bleu{x`;FV(b)}, on écrit \bleu{o.l := b} à la place de
\bleu{o.l"`="`£(x)b}.

Dans les objets, on écrira 
\begin{displaymathbleu}
  [...,l=o,...]
\end{displaymathbleu}
au lieu de 
\begin{displaymathbleu}
  [...,l=`£(s)o,...].
\end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Variables libres}
\begin{eqnarraybleu}
  FV(`£(y)b) &"=^="& FV(b) - \{y\}\\
  FV(x) &"=^="&\{x\}\\
  FV([l_i=`£(x_i) b_i~ ^{i`:1..n}]) &"=^="&
  \bigcup_{i`:1..n}FV(`£(x_i)b_i)\\
  FV(a.l) &"=^="& FV(a) \\
  FV(a.l"`="`£(y)b) &"=^="& FV(a) \cup FV(`£(y)b)
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Substitution dans les objets}
On applique la convention de Barendregt.
\begin{eqnarraybleu}
  \osubst{(`£(y)b)}{x}{c} &"=^="& `£(y)(\osubst{b}{x}{c}) \\ 
  \osubst{x}{x}{c} &"=^="& c \\
 \osubst{y}{x}{c} &"=^="& y \\
 \osubst{[l_i=`£(x_i) b_i~ ^{i`:1..n}]}{x}{c} &"=^="&
 [l_i=\osubst{`£(x_i) b_i}{x}{c}~^{i`:1..n}]\\
 \osubst{(a.l)}{x}{c} &"=^="& (\osubst{a}{x}{c}).l\\
 \osubst{(a.l"`="`£(y)b)}{x}{c} &"=^="& (\osubst{a}{x}{c}).l"`="(\osubst{(`£(y)b)}{x}{c})
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Huge \bf \color{vertfonce}{\textit{Exemples}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Traduction du $`l$-calcul}
%
Le $`£$-calcul est au moins aussi puissant que le $`l$-calcul!

On pose
\begin{eqnarraybleu}
  p `(!) q & "=^=" & (p.arg :=q).val 
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
alors
\begin{eqnarraybleu}
  \emph{`l-\textrm{termes}} && \emph{\textrm{objets pures}} \\\\
  `«x`» & "=^=" & x \\
  `«b(a)`» & "=^=" &  `«b`» `(!) `«a`» \\
  `«`l x . b`» & "=^=" & [arg = `£(x) x. arg,\quad val = `£(x) \osubst{`«b`»}{x}{x.arg}]
\end{eqnarraybleu}
\vfill
L'idée est que l'application \bleu{ `«b(a)`»} stocke l'argument dans une
place connue (le champ \bleu{arg}).

Puis elle invoque une méthode de \bleu{ `«b`»} qui peut accéder  à
l'argument à travers self.
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Par exemple,
\begin{eqnarraybleu}
  `«(`l x. x) y`»  & `= & ([arg = `£(x) x. arg,\quad val = `£(x) x.arg].arg := y).val \\
  &=& y
\end{eqnarraybleu}

La valeur initiale de l'argument \bleu{arg} n'a pas d'importance. 

Ici on prend une valeur qui conduit à une boucle si on tente de
l'«évaluer».  Ce qui correspond à une valeur non initialisée.
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
Soit
\begin{eqnarraybleu}
  o &`=& [arg=`«a`»,\quad val=`£(x) \osubst{`«b`»}{x}{x.arg}]
\end{eqnarraybleu}
alors
\begin{eqnarraybleu}
  `«(`l x. b)~a`» &`=&  ([arg = `£(x) x. arg,\\
  &&\quad val = `£(x) \osubst{`«b`»}{x}{x.arg}].arg :=`«a`»).val\\
  &=& o.val\\
  &=&\osubst{(\osubst{`«b`»}{x}{x.arg})}{x}{o}\\
  &=& \osubst{`«b`»}{x}{o.arg}\\
  &=& \osubst{`«b`»}{x}{`«a`»}
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
%
La $`h$-conversion n'est pas préservée, parce qu'il y a des objets qui
ne représentent pas des $`l$-termes. 
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Point fixe}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Point fixe}
%
Comme on peut coder le $`l$-calcul on peut obtenir une version objet
de tout ce que l'on peut coder dans le $`l$-calcul.

On peut cependant obtenir de meilleure version en les encodant
directement dans le $`£$-calcul.

C'est le cas du point fixe.
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Point fixe}
%
\begin{eqnarraybleu}
  \textrm{fix} & "=^=" & [arg = `£(x) x. arg, \quad val = `£(x) ((x.arg).arg := x.val).val]
\end{eqnarraybleu}
Vérifions.

D'abord posons
\begin{eqnarraybleu}
  \textrm{fix}_f  & "=^=" &  \textrm{fix}.arg:=f\\
  &=& [arg = f, \quad val = `£(x) ((x.arg).arg := x.val).val]
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
alors
\begin{eqnarraybleu}
  \textrm{fix} `(!) f &`=& \textrm{fix}_f.val\\
  &=& ((\textrm{fix}_f.arg).arg:=\textrm{fix}_f.val).val\\
  &=& (f.arg := \textrm{fix}`(!) f).val\\
  &`=& f `(!) (\textrm{fix} `(!) f)
\end{eqnarraybleu}
\emph{La traduction de} \bleu{`l x. x x} est
\begin{eqnarraybleu}
  `«`l x. x x`» &`=& [arg = `£(x) x. arg, \\
  &&\quad val = `£(x) ((x.arg).arg := x.arg).val]
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Le point fixe de Fisher, Honsell et Mitchell}
%
Fisher, Honsell et Mitchell ont proposé 
\begin{eqnarraybleu}
  \textrm{fix}' & "=^=" & `l f [rec = `£(s) f (s.rec)].rec.
\end{eqnarraybleu}
On peut le traduire de façon proche mais pas identique:
\begin{footnotesize}
\begin{eqnarraybleu}
  `«\textrm{fix}'`» &=& [arg = `£(x) x. arg, \\
  &&\quad val = `£(f) \osubst{[rec = `£(s) f `(!) (s.rec)].rec}{f}{f.arg}]\\
  &=& [arg = `£(x) x. arg, \\
  &&\quad val = `£(f) \osubst{[rec = `£(s) (f.arg:= s. rec).val].rec}{f}{f.arg}]\\
  &=& [arg = `£(x) x. arg, \\
  &&\quad val = `£(f)[rec = `£(s)((f.arg).arg:=s.rec).val].rec]
\end{eqnarraybleu}
\end{footnotesize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Le point géométrique}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{L'objet point}
%
Un grand classique de la théorie des langages à objets est le point géométrique qui contient un
méthode \emph{move} qui déplace le point c'est-à-dire qui modifie les coordonnées du point.
\begin{eqnarraybleu}
  origine_1  & "=^=" & [x=0, mv\_x = `£(s)`l\,dx (s.x := s.x + dx)]
\end{eqnarraybleu}
\begin{eqnarraybleu}
  origine_2  & "=^=" & [x=0, y=0,\\
  && \quad  mv\_x = `£(s)`l\,dx (s.x := s.x + dx),\\
  && \quad  mv\_y = `£(s)`l\,dy (s.y := s.y + dy)]
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On peut définir 
\begin{displaymathbleu}
  unit_2 "=^=" origin_2.mv\_x(1).mv\_y(1)
\end{displaymathbleu}
On peut montrer que l'abcisse de \bleu{unit_2} est \bleu{1}, autrement dit que 
\begin{eqnarraybleu}
  unit_2.x &=& 1.
\end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Méthodes archivantes}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Auto-archive}
%
\emph{Une illustration simple de la technique qui permet à un objet de se stocker soi-même.}

Un objet peut garder des copies de lui-même.

Cet objet a
\begin{itemize}
\item[\emph{$`(!)$}] une méthode d'archivage \emph{backup},
\item[\emph{$`(!)$}] et une méthode de restauration  \emph{retrieve} qui retourne la dernière
  archive.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{eqnarraybleu}
  o &"=^="& [retrieve = `£(s_1)s_1,\\
  && backup = `£(s_2) s_2.retrieve "`=" `£(s_1)s_2,\\
  && \noir{et plein d'autres choses}].
\end{eqnarraybleu}
On a donc
\begin{eqnarraybleu}
  o' &"=^="& o.backup \\
  &=& [retrieve = `s(s_1) o, ....]
\end{eqnarraybleu}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Plus tard après avoir modifier des attributs de \bleu{o'} on peut restaurer l'objet qui a été
archivé et l'on retrouve l'objet qui était l'objet courant au moment de l''archivage. 
\begin{eqnarraybleu}
  o'.retrieve &=& o
\end{eqnarraybleu}
On peut itérer des invocations de la  méthode \emph{retrieve} pour retrouver des objets de plus en plus
anciennement archivés, jusqu'à converger finalement vers l'objet initial.
  \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Cellules}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{eqnarraybleu}
    myCell &"=^="& [contents = 0,\\
    &&\quad get=`£(s) s.contents,\\
    &&\quad set = `£(s)`l~n~(s.contents := n)]
  \end{eqnarraybleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Une \emph{cellule à restauration}
\begin{itemize}
\item[\emph{$`.$}] une méthode \emph{backup} 
\item[\emph{$`.$}] et une méthode \emph{restore} pour restaurer l'objet en copiant l'archive dans le
  contenu.
\end{itemize}
\begin{footnotesize}
  \begin{eqnarraybleu}
    myReCell &"=^="& [contents = 0,\\
    &&\quad get=`£(s) s.contents,\\
    &&\quad set = `£(s)`l~n~(s.backup:=s.contents).contents := n,\\
    && \quad bakcup = 0,\\
    &&\quad restore = `£(s) s. contents : =s.backup]
  \end{eqnarraybleu}
\end{footnotesize}
%
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
On peut définir une cellule avec restauration sans champ backup, en s'appuyant sur la modification
de méthode. 

C'est la méthode \emph{set} qui est en charge de mettre à jour la méthode \emph{restore}.

Chaque fois que \emph{set} est invoquée elle modifie \emph{restore} en \bleu{`£(z) z.contents:=m}
où \bleu{m} est le contenue de la cellule avant l'invocation. 

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\begin{scriptsize}
\begin{mathbleu}
  myOtherReCell \quad "=^=" \\
  \hspace*{30pt}[contents = 0,\\
  \hspace*{30pt}\quad get=`£(s) s.contents,\\
  \hspace*{30pt}\mbox{$\quad set = `£(s)`l~n~(s.restore"`="`£(z)(z.contents:=s.contents).contents := n),$}\\
  \hspace*{30pt}\quad restore = `£(s) s. contents : =0]
\end{mathbleu}
\end{scriptsize}

Ceci montre qu'\verdir{il est primordial que les self soient des paramètres nommés}.

Fournir un mot-clé \textbf{self} comme cela est fait dans beaucoup de langages de programmation par
objet n'est pas suffisant.  \vfill
\end{slide}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Huge \bf \color{vertfonce}{\textit{Un système de types}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Typage des objets}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{displaymathbleu}
    \prooftree %
    `G "|-"B_i \qquad `A i`:1..n
    \justifies `G "|-" [l_i:B_i~^{i`:1..n}]%
    \using  \quad \noir{les} l_i \noir{sont distincts} \quad \emph{Type~Objet}
     \endprooftree %
   \end{displaymathbleu}

 \begin{displaymathbleu}
   \prooftree %
   `G, x_i:A "|-" b_i:B_i \qquad `A i`:1..n
   \justifies `G "|-" [l_i= `£(x_i:A) b_i~^{i`:1..n}]:A%
   \using  \quad \noir{où} A`= [l_i:B_i~^{i`:1..n}] \quad \emph{Val~Objet}
   \endprooftree %
   \end{displaymathbleu}

\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\fbox{Pour \bleu{j`:1..n},}
\begin{displaymathbleu}
   \prooftree %
   `G "|-" a: [l_i:B_i~^{i`:1..n}]
   \justifies `G "|-" a.l_j:B_j
   \using  \quad \emph{Val Select} 
   \endprooftree %
  \end{displaymathbleu}

  \begin{displaymathbleu}
    \prooftree %
    `G "|-" a:A \qquad `G, x:A "|-" b:B_j
    \justifies `G "|-" a.l_j "`=" `£(x:A) b :A
    \using \quad \noir{où} {A`= [l_i:B_i~^{i`:1..n}]} \quad \emph{Type Objet}
     \endprooftree %
   \end{displaymathbleu}
 \vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
  \begin{center}
    {\Large \bf \color{brunfonce}{\textit{Bonne formation des types}}}
\end{center}
\end{slide}
%------------------------------------------------------
\begin{slide}
  \bleu{`G "|-" \diamond} doit se lire \emph{«le contexte \bleu{`G}
    est cohérent»}.

\begin{displaymathbleu}
   \prooftree %
   \justifies   \emptyset "|-" \diamond
   \using  \quad \emph{Env~ \emptyset}
   \endprooftree %
  \end{displaymathbleu}

\begin{displaymathbleu}
   \prooftree %
   `G "|-" A \quad x`; dom(`G)
   \justifies `G, x:A "|-" \diamond
   \using  \quad \emph{Env~x}
   \endprooftree %
  \end{displaymathbleu}

\begin{displaymathbleu}
   \prooftree %
   `G', x:A, `G'' "|-" \diamond
   \justifies `G', x:A, `G'' "|-" x:A
   \using  \quad \emph{Env~x}
   \endprooftree %
  \end{displaymathbleu}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
Tout cela se lit:
\begin{itemize}
\item[\emph{$`.$}] le contexte vide est cohérent,
\item[\emph{$`.$}] si \bleu{A} est un type bien formé dans \bleu{`G},
  alors le contexte  \bleu{`G, x:A} est cohérent,
\item[\emph{$`.$}] si le contexte  \bleu{`G', x:A, `G''} est
  cohérent, alors \bleu{x} est de type \bleu{A} dans ce contexte.
\end{itemize}
\vfill
\end{slide}
%------------------------------------------------------
\begin{slide}
\heading{Unicité du type}
\emph{Proposition:} Si \bleu{`G"|-" a:A} et  \bleu{`G"|-" a:A'}  sont
dérivables \ali alors  \bleu{A `= A'}. 

\vspace*{20pt}

Ce système de type \emph{ne garantit pas la forte normalisation.}

Il garantit seulement la correction.


\vspace*{20pt}

On démontre aussi une propriété de \emph{réduction du sujet}.
\vfill
\end{slide}

\end{document}
