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

Prise en compte des commentaires sur mes commentaires sur les commentaires de Clément.

Browse Source
This commit is contained in:
Mysaa 2022-08-09 09:10:25 +02:00
parent e31a43228a
commit bb2c062cc8
Signed by: Mysaa
GPG Key ID: 7054D5D6A90F084F
1 changed files with 36 additions and 32 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

68
RapportStage.tex
View File

@ -73,7 +73,9 @@
On note $\vdash$ la relation de typage. On notera par exemple $\mathcal{A},\Gamma \vdash e : \fj{C}$ pour indiquer que l'expression $e$ avec l'environnement de typage $\Gamma$ (une ensemble d'entrées de type $e : \fj{C}$) est typée par la classe \fj{C} sous la \eng{class table} $\mathcal{A}$.
La relation de réduction dépend de la \eng{class table} $\mathcal{A}$ utilisée. On la notera $\rightarrow_\mathcal{A}$ ou simplement $\rightarrow$ si il n'y a pas d’ambigüité. On notera aussi $\rightarrow^*_\mathcal{A}$ ou $\rightarrow^*$ la cloture transitive et réflexive de la relation. On notera enfin $e\Downarrow v$ lorsque $e \rightarrow^* v$ et $v$ est une valeur. On pourra même écrire $e \Downarrow$ pour dire $\exists v \quad e \Downarrow v$.
Notez qu'une \eng{class table} n'est pas nécessairement typée. En effet, toutes les classes sont définies individuellement, et c'est le typage de la \eng{class table} complète qui les lie et qui leur donne leur cohérence. Cette propriété nous permet de considérer des \eng{class tables} partielles, qui seront ensuite accolées à d'autres pour être bien typées. FJ définit la notation $\mathcal{A}\;\texttt{OK}$ pour indiquer que la \eng{class table} $\mathcal{A}$ est bien typée. On notera aussi souvent la concaténation de deux \eng{class tables} qui définissent des noms de classe \emph{distincts} $\mathcal{A} \oplus \mathcal{B}$.
La relation de réduction dépend de la \eng{class table} $\mathcal{A}$ utilisée. On la notera $\rightarrow_\mathcal{A}$ ou simplement $\rightarrow$ si il n'y a pas d’ambigüité. On notera aussi $\rightarrow^*_\mathcal{A}$ ou $\rightarrow^*$ la clôture transitive et réflexive de la relation. On notera enfin $e\Downarrow v$ lorsque $e \rightarrow^* v$ et $v$ est une valeur. On pourra même écrire $e \Downarrow$ pour dire $\exists v \quad e \Downarrow v$.
Cette relation est définie avec deux types de règles \cite[Fig.3]{fjdef}, les règles de type \textsc{R} qui indiquent :
\begin{itemize}
@ -133,6 +135,8 @@
\section{Étude d'équivalences simples}
\label{sec:eqsimpl}
Dans cette section, je vais présenter les équivalences les plus simples et présenter les problèmes que je leur ai trouvé. Cette section n'a pas pour objectif de construire des théorèmes, ni même d'être rigoureuse, mais elle vise à donner au lecteur l'intuition sur les propriétés souhaitables pour un préordre sur les programmes FJ.
\subsection{Explication de l'utilité d'un contexte}
Les équivalences entre les programmes sont habituellement définies en utilisant des \enquote{contextes}. Deux programmes sont dits équivalents lorsqu'ils donnent les mêmes résultats sous tout contexte. Pour un contexte $C$, on va noter $C\bracket{P}$ l'interprétation d'un programme $P$ dans le contexte. Alors, le préordre sera défini comme tel:
@ -471,12 +475,12 @@
\\[3ex]
\infer
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.f} : \fj{C}}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{C0})}
{\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \fj{C}\;\fj{f} \in \operatorname{fields}(\fj{Cc})}
& \newtag{\textrm{\textsc{TI-Field}}}{rule:ti:field}
\\[3ex]
\infer
{\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{$e$.m($\overline{e_x}$)} : \fj{C}}
{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{C0} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\[-1.4ex] \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
{\begin{array}{c}\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{Cc} \quad \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \\[-1.4ex] \overline{\fj{CX}} \subclass \overline{\fj{D}} \quad \operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C} \end{array}}
& \newtag{\textrm{\textsc{TI-Invk}}}{rule:ti:invoke}
\\[3ex]
\infer
@ -695,49 +699,49 @@
\[
\begin{array}{rcl}
\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) &\implies& \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{C0}) \\
\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{C0}) = \overline{\fj{D}}\rightarrow\fj{C} & \implies& \exists \fj{C'}\subclass \fj{C}\ \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C0}) = \overline{\fj{D'}}\rightarrow\fj{C'}\\
\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) = \overline{\fj{D}} & \implies & \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{C0}) = \overline{\fj{D'}}\;\overline{\fj{f}}
\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) &\implies& \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) \\
\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}}\rightarrow\fj{C} & \implies& \exists \fj{C'}\subclass \fj{C}\ \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D'}}\rightarrow\fj{C'}\\
\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}} & \implies & \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) = \overline{\fj{D'}}\;\overline{\fj{f}}
\end{array}
\]
\paragraph{Première propriété}
Montrons cette propriété par induction sur la relation $\subclass'$.
En inversant la règle qui a permis de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{C0})$, il y a quatre possibilités.
En inversant la règle qui a permis de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc})$, il y a quatre possibilités.
\subparagraph{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{E})$}
On applique alors directement l’hypothèse d'induction.
\subparagraph{Cas $\fj{class C0 \{C f;...\}} \in \mathcal{B}$ (\textnormal{\ref{rule:lct-fields})}}
Alors, par construction de $\operatorname{fields}$, on a $\fj{C}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(C0)$
\subparagraph{Cas $\fj{class Cc \{C f;...\}} \in \mathcal{B}$ (\textnormal{\ref{rule:lct-fields})}}
Alors, par construction de $\operatorname{fields}$, on a $\fj{C}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(Cc)$
\subparagraph{Cas $\left[\fj{C0 \{C f, ...\}}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields})}}
\subparagraph{Cas $\left[\fj{Cc \{C f, ...\}}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:attributes}, et on a donc
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\subparagraph{Cas $\left[\fj{C0 (..., C f, ...)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields2})}}
\subparagraph{Cas $\left[\fj{Cc (..., C f, ...)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-fields2})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:constructor}, et on a donc, puisque le field \fj{f} est défini,
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\]
\paragraph{Seconde propriété}
Procédons par induction sur la définition de $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}$.
Nous avons comme hypothèse $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}$.
Nous avons comme hypothèse $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}$.
\subparagraph{Cas $\left[\fj{C0 : C m($\overline{\texttt{D}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-method})}}
\subparagraph{Cas $\left[\fj{Cc : C m($\overline{\texttt{D}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-method})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la règle \ref{rule:tri:method}, et on a donc.
\[\operatorname{mtype}_\mathcal{A}(\fj{m},\fj{C}) = \overline{\fj{D'}} \rightarrow \fj{C'}\quad;\quad\overline{\fj{D}} \subclass \overline{\fj{D'}}\quad;\quad \fj{C'}\subclass\fj{C}\]
\subparagraph{Cas $\fj{class C0 \{...,C m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-method}})}
\subparagraph{Cas $\fj{class Cc \{...,C m($\overline{\texttt{D}}\;\overline{\texttt{x}}$)\}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-method}})}
Alors, par définition de $\operatorname{mtype}$, on a que
\[\operatorname{mtype}_\mathcal{B}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{E}\quad\text{et}\quad\fj{C0}\subclass\fj{C0}\]
\[\operatorname{mtype}_\mathcal{B}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{E}\quad\text{et}\quad\fj{Cc}\subclass\fj{Cc}\]
\subparagraph{Cas $\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}} \rightarrow \fj{E}$ et $\fj{C}\subclass'\fj{C0}$ (\textnormal{\ref{rule:lup-method}})}
\subparagraph{Cas $\operatorname{mtype}(\fj{m},\fj{C}) = \overline{\fj{D}} \rightarrow \fj{E}$ et $\fj{C}\subclass'\fj{Cc}$ (\textnormal{\ref{rule:lup-method}})}
\label{proof:mtype:cchain}
Puisque $\fj{C}\subclass'\fj{C0}$, alors, il existe une chaine de classes
\[\fj{C} = \fj{C}_0 , \fj{C}_1 , \dots , \fj{C}_n = \fj{C0}\]
Puisque $\fj{C}\subclass'\fj{Cc}$, alors, il existe une chaine de classes
\[\fj{C} = \fj{C}_0 , \fj{C}_1 , \dots , \fj{C}_n = \fj{Cc}\]
telles que $\fj{C}_k\;\fj{extends}\;\fj{C}_{k+1}$ dans $\mathcal{A}$ ou $\mathcal{B}$.
@ -746,22 +750,22 @@
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_n) = \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_{n-1}) = \cdots = \operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C}_0)\]
Donc $\operatorname{mtype}(\fj{m},\fj{C0}_n) = \overline{\fj{D}}\rightarrow \fj{E}$.
Donc $\operatorname{mtype}(\fj{m},\fj{Cc}_n) = \overline{\fj{D}}\rightarrow \fj{E}$.
\paragraph{Troisième propritété}
Une dernière fois, inversons la règle qui a permis de prouver $\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) = \overline{\fj{D}}$.
Une dernière fois, inversons la règle qui a permis de prouver $\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}$.
\subparagraph{Cas $\left[\fj{C0 ($\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-construct})}}
\subparagraph{Cas $\left[\fj{Cc ($\overline{\texttt{D}}\;\overline{\texttt{f}}$)}\right] \in \mathfrak{T}$ (\textnormal{\ref{rule:lti-construct})}}
Alors, puisque $\mathcal{A} \triangleright \mathfrak{T}$, c'est nécessairement par la \autoref{rule:tri:constructor}, et on a donc
\[\exists \overline{\fj{D'}}\quad\overline{\fj{D'}}\;\overline{\fj{f0}} = \operatorname{fields}_\mathcal{A}(C)\]
\subparagraph{Cas $\fj{class C0\{C0($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-construct}})}
\subparagraph{Cas $\fj{class Cc\{Cc($\overline{\texttt{D}}\;\overline{\texttt{f}}$)\{...\} ... \}}\in \mathcal{B}$ (\textnormal{\ref{rule:lct-construct}})}
Alors, puisqu'en Featherweight Java, les objets sont immuables et les constructeurs définissent tous les fields, on sait que les paramètres du constructeurs sont \emph{exactement} les champs de la classe. Et donc
\[\operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{C0}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\]
\[\operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\]
\subsection{Corps de la preuve}
@ -782,12 +786,12 @@
\begin{hyps}
\item e = \fj{$e_0$.f}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
\item \fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{C0})
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{Cc} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{Cc'}\quad\text{et}\quad \fj{Cc'}\subclass\fj{Cc}
\item \fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc})
\end{hyps}
On peut alors appliquer la première propriété sur la quatrième hypotèse qui nous donne
\[\exists\fj{C'}\subclass \fj{C} \quad \fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0})\]
\[\exists\fj{C'}\subclass \fj{C} \quad \fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{Cc})\]
Alors, on peut directement appliquer la règle FJ \textsc{T-Field}
@ -795,18 +799,18 @@
\begin{hyps}
\item e = \fj{$e_0$.m($\overline{e_x}$)}
\item \fj{C} = \fj{C}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{C0} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{C0'}\quad\text{et}\quad \fj{C0'}\subclass\fj{C0}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash e_0 : \fj{Cc} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash e_0 : \fj{Cc'}\quad\text{et}\quad \fj{Cc'}\subclass\fj{Cc}
\item \mathfrak{T},\mathcal{B},\Gamma \Vdash \overline{e_x} : \overline{\fj{CX}} \quad \text{donc} \quad \mathcal{A}\oplus\mathcal{B}\vdash \overline{e_x} : \overline{\fj{CX'}}\quad\text{et}\quad \overline{\fj{CX'}}\subclass\overline{\fj{CX}}
\item \operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}
\item \operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}
\item \overline{\fj{CX}} \subclass \overline{\fj{C}}
\end{hyps}
On peut alors appliquer la seconde propriété sur la cinquième hypothèse, on obtient que
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m}, \fj{C0}) = \overline{\fj{D'}} \rightarrow \fj{C'} \quad\text{et}\quad \overline{\fj{D}}\subclass\overline{\fj{D'}}\quad\text{et}\quad\fj{C'}\subclass\fj{C}\]
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m}, \fj{Cc}) = \overline{\fj{D'}} \rightarrow \fj{C'} \quad\text{et}\quad \overline{\fj{D}}\subclass\overline{\fj{D'}}\quad\text{et}\quad\fj{C'}\subclass\fj{C}\]
Alors, en utilisant la même preuve que pendant la preuve de la sous propriété (page \pageref{proof:mtype:cchain})
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{C0'}) = \overline{\fj{D'}}\rightarrow\fj{C'} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
\[\operatorname{mtype}_{\mathcal{A}\oplus\mathcal{B}}(\fj{m},\fj{Cc'}) = \overline{\fj{D'}}\rightarrow\fj{C'} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\]
On peut maintenant appliquer la règle FJ \textsc{T-Invk} et obtenir le résultat.