Mysaa/stage-2022
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Ajout des notes du Lundi.

Browse Source
This commit is contained in:
Mysaa 2022-06-21 11:52:06 +02:00
parent 735f2d52b6
commit 5ffd08c62d
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 118 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

119
NotesStage.tex
View File

@ -18,6 +18,7 @@
\usepackage{mdframed}
\usepackage{proof}
\usepackage[lighttt]{lmodern}
\usetikzlibrary{shapes.geometric}
\newcommand{\pgrph}{\P}
\newcommand{\hsep}{\vspace{.2cm}\centerline{\rule{0.8\linewidth}{.05pt}}\vspace{.4cm}}
@ -36,8 +37,11 @@
\newcommand\newtag[2]{#1\def\@currentlabel{#1}\label{#2}}
\makeatother
\DeclareMathOperator{\varnull}{varnull}
\DeclareMathOperator{\nextop}{next}
\DeclareMathOperator{\new}{\text{\textbf{new}}}
\DeclareMathOperator{\CT}{CT}
\DeclareRobustCommand{\leftsarrow}{\text{\reflectbox{$\;\rightarrow^*$}}}
\let\rbar\bar
\let\bar\overline
\newcommand\subclass{<:}
@ -804,8 +808,121 @@
$$CT_1 \prec_{TS} CT_2 \iff \forall \left[\fj{Class : D meth(}\overline{\fj{E}}\fj{)}\right] \in TI \quad CT_1 \methprec{Class.meth} CT_2$$
\end{theorem}
\subsection{Lemme des arguments finis}
Pour un ensemble $\overline{CT}$, on note $\bigwedge \overline{CT}$ l'ensemble des valeurs qui sont valides dans chaque \textit{class table} de $\overline{CT}$.
Soient $CT_i$ des class tables.
Soient $\overline{d}$ des expressions typables dans chaque $CT_i$ telles que pour toute sous-expression $\varepsilon$ de $d_i$, $\forall i,j \; (CT_i,\varepsilon)\Downarrow v \iff (CT_j,\varepsilon)\Downarrow v$
Alors il existe une famille d'ensembles de variables $\overline{V}$ indexée par les $\overline{d}$, dont les variables sont dans $\bigwedge CT_i$ telle que
$$\left[\overline{d}/\overline{x}\right]e \rightarrow^* V \iff \forall v_i \in V_i\quad \left[\overline{v}/\overline{x}\right]e \rightarrow^* V$$
$\overline{V}$ dépend donc de $\bigwedge CT_i$ et de $d$.
\subsubsection{Preuve de la confluence de la réduction en Featherweight Java}
Nous allons dans cette section essayer de démontrer que la relation $\rightarrow$ de réduction de Featherweight Java est \textit{confluente}, c'est à dire que
$$\forall e,e_1,e_2\quad e_1 \leftsarrow e \rightarrow^* e_2 \implies (\exists e'\quad e_1 \rightarrow^* e' \leftsarrow e_2)$$
La relation dénote ici la réduction sous une class table quelconque fixée.
On peut se contenter de montrer la semi-confluence, c'est à dire
$$\forall e,e_1,e_2\quad e_1 \leftarrow e \rightarrow^* e_2 \implies (\exists e'\quad e_1 \rightarrow^* e' \leftsarrow e_2)$$
Si $e \rightarrow e_1$, c'est qu'il y a un nœud qui s'est fait réduire de la forme \fj{e.f}, \fj{e.meth(...)} ou \fj{(C) e} où \fj{e} est de la forme \fj{new D(...)}. On va procéder à un \textit{marquage} de ce nœud afin de pouvoir l'observer dans $e_2$. Le marquage perdurera le long de la réduction $e \rightarrow^* e_2$. Notez que le marquage se démultiplie si un argument il est dans un argument d'une méthode qui se fait déplier et qu'il est utilisé plusieurs fois, et qu'il est détruit si la réduction s'effectue sur ce nœud.
Ensuite, pour chaque expression du chemin $e \rightarrow^* e_2$, on remplace chaque nœud marqué par sa version réduite par application de la même règle que pour $e \rightarrow e_1$. On obtient un chemin $e_1 \rightarrow^* e'$ car une réduction ne modifie que le nœud qu'elle réduit plus éventuellement un nœud \fj{new} associé, or, une expression sous la forme \fj{new C(...)} ne pourra être réduite que en une expression de la même forme.
Enfin, nous avons $e_2 \rightarrow e'$ car il suffit de réduire séquentiellement chaque nœud marqué dans $e_2$ par la même opération que pour $e \rightarrow e_1$, et nous obtenons par définition e'.
\subsubsection{Obtention des ensembles de valeurs $V$}
Pour créer l'ensemble de valeurs, nous allons nous restreindre à une seule \textit{class table} (la relation de réduction est donc simplement notée $\rightarrow$) et une seule expression $e \in \overline{d}$.
Nous allons déjà définir une application appelée $\varnull$ qui transforme une expression en valeur en transformant les nœuds selon le tableau suivant:
\begin{tabular}{c|cl}
Remplacer & Par & \\\hline
\fj{e.f} & \fj{null(D)} & si $(\fj{D},\fj{f}) \in \operatorname{fields}(\fj{C})$ et $\vdash \fj{e} : \fj{C}$ \\
\fj{e.m(...)} & \fj{null(D)} & si $\operatorname{mtype}(\fj{C},\fj{m}) = \overline{\fj{E}}\rightarrow\fj{D}$ et $\vdash \fj{e} : \fj{C}$ \\
\fj{(D)e} & \fj{null(D)} &
\end{tabular}
Cette transformation peut se faire dans n'importe quelle ordre, tant qu'il ne reste plus de nœuds à remplacer à la fin. Il est tout de même préférable de commencer par le nœud le plus proche de la racine afin de procéder au nombre minimal de remplacements.
Nous allons distinguer trois différents cas.
\paragraph{Premier cas} $e \rightarrow^* v$ et $v$ est une valeur.
Alors on note simplement $V = \{v\}$ (c'était le cas le plus simple).
\paragraph{Second cas} $e$ ne se réduit pas en une valeur, et toute suite de réduction partant de $e$ est finie.
Alors, puisque le nombre d'expressions $e'$ telles que $e\rightarrow e'$ est fini pour tout $e$ et $e'$, on peut assurer qu'il y a un nombre fini d'expressions $e'$ telles que $e \rightarrow^* e'$. En appliquant la confluence de la réduction autant de fois qu'il y aie de $e'$ (moins $1$), on peut assurer qu'il existe une expression notée $e_v$ telle que $\forall e'\quad e \rightarrow^* e' \implies e' \rightarrow^* e_v$.
On note enfin notre ensemble $V = \{\varnull(e_v)\}$.
\paragraph{Troisième cas} $e$ ne se réduit pas en une valeur, et il existe au moins une suite de réductions infinie.
Alors, notons $\mathcal{E}_k$ l'ensemble des expressions qui sont atteintes depuis $e$ avec $k$ réductions ou moins:
$$\mathcal{E}_0 = \{e\}\qquad \mathcal{E}_{k+1}= \mathcal{E}_k \cup \rightarrow\!\!(\mathcal{E}_k)$$
Par le même argument qu'au paragraphe précédent, les $\mathcal{E}_k$ sont tous finis.
En appliquant $\#\mathcal{E}_k - 1$ fois la propriété de confluence, on détermine une expression $e_k$ (avec $e_0 = e$) telle que
$$\forall e' \quad e' \in \mathcal{E}_k \implies e' \rightarrow^* e_k$$
\begin{center}
\begin{tikzpicture}
\node[ellipse,draw,fill opacity=.1,minimum width=6cm,minimum height=1.4cm, fill=red] (7) at (0,0) {};
\node (0) at (0, 2) {$e$};
\node (1) at (-2, 0) {$e^x_1$};
\node (2) at (-1, 0) {$e^x_2$};
\node (3) at (1, 0) {$e^x_{n-1}$};
\node (4) at (2, 0) {$e^x_n$};
\node (5) at (0, -2) {$e_k$};
\node (6) at (0,0) {$\cdots$};
\draw [->] (0) -- (1) node[left, above,pos=1]{$*$};
\draw [->] (0) -- (2) node[left, above,pos=1]{$*$};
\draw [->] (0) -- (3) node[left, above,pos=1]{$*$};
\draw [->] (0) -- (4) node[left, above,pos=1]{$*$};
\draw [->] (1) -- (5) node[left,pos=1]{$*$};
\draw [->] (2) -- (5) node[right, above,pos=1]{$*$};
\draw [->] (3) -- (5) node[right, above,pos=1]{$*$};
\draw [->] (4) -- (5) node[right,pos=1]{$*$};
\node (8) at (3.2,0) {$\mathcal{E}_k$};
\end{tikzpicture}
\end{center}
On note ensuite $\nextop(k) = \min\{i \in \mathbb{N},e_k \in \mathcal{E}_i, i > k\}$
On peut enfin noter la considérer la chaine infinie (où la puissance dénote la composition).
$$e_{\nextop^0(0)} \rightarrow^* e_{\nextop^1(0)} \rightarrow^* e_{\nextop^2(0)} \rightarrow^* \cdots$$
Cette chaine a la propriété intéressante que l'on puisse y relier n'importe quelle expression $e'$ issue de $e$.
$$\forall e'\quad e\rightarrow^* e' \implies (\exists i\quad e' \rightarrow^* e_{\nextop^i(0)})$$
En effet, si on note $i$ le nombre d'étape de $e \rightarrow^* e'$, alors $e' \in \mathcal{E}_i$ donc $e' \in \mathcal{E}_{\nextop^i(0)}$ car $\nextop$ est strictement croissant et $\mathcal{E}$ aussi. Donc $e' \rightarrow^* e_{\nextop^i(0)}$ par définition de $e_{\nextop^i(0)}$.
Enfin, notre ensemble de valeurs est $V = \{\varnull(e_{\nextop^i(0)})\}_{i\in\mathbb{N}}$.
\subsubsection{Preuve du lemme}
\newpage
\bibliography{NotesStage}
\bibliographystyle{ieeetr}