From 8e64e14dc03da17cf6a981a41291deb0a58e3433 Mon Sep 17 00:00:00 2001 From: Mysaa Date: Sun, 7 Aug 2022 13:28:38 +0200 Subject: [PATCH] =?UTF-8?q?Prise=20en=20compte=20des=20commentaires=20de?= =?UTF-8?q?=20Cl=C3=A9ment,=20partie=203?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Bilibibio.bib | 1 - NotesSurCommentairesClement.md | 10 +++ RapportStage.tex | 147 ++++++++++++++++----------------- header.tex | 3 +- 4 files changed, 85 insertions(+), 76 deletions(-) diff --git a/Bilibibio.bib b/Bilibibio.bib index dd40f13..bd83e5b 100644 --- a/Bilibibio.bib +++ b/Bilibibio.bib @@ -8,7 +8,6 @@ volume = {23}, number = {3}, issn = {0164-0925}, - url = {https://doi.org/10.1145/503502.503505}, doi = {10.1145/503502.503505}, abstract = {Several recent studies have introduced lightweight versions of Java: reduced languages in which complex features like threads and reflection are dropped to enable rigorous arguments about key properties such as type safety. We carry this process a step further, omitting almost all features of the full language (including interfaces and even assignment) to obtain a small calculus, Featherweight Java, for which rigorous proofs are not only possible but easy. Featherweight Java bears a similar relation to Java as the lambda-calculus does to languages such as ML and Haskell. It offers a similar computational "feel," providing classes, methods, fields, inheritance, and dynamic typecasts with a semantics closely following Java's. A proof of type safety for Featherweight Java thus illustrates many of the interesting features of a safety proof for the full language, while remaining pleasingly compact. The minimal syntax, typing rules, and operational semantics of Featherweight Java make it a handy tool for studying the consequences of extensions and variations. As an illustration of its utility in this regard, we extend Featherweight Java with generic classes in the style of GJ (Bracha, Odersky, Stoutamire, and Wadler) and give a detailed proof of type safety. The extended system formalizes for the first time some of the key features of GJ.}, journal = {ACM Trans. Program. Lang. Syst.}, diff --git a/NotesSurCommentairesClement.md b/NotesSurCommentairesClement.md index d9da84b..757bdee 100644 --- a/NotesSurCommentairesClement.md +++ b/NotesSurCommentairesClement.md @@ -41,3 +41,13 @@ Cela facilite surtout la lecture de la preuve 1, parce que alors les définition ### 11 - Sur la notation C' La notation C' est effectivement plus claire que C0, mais mon problème est que ce n'est pas un nom de classe FJ valide. Est-ce que c'est vraiment génant ? + +### 13 - FJ et les attributs de son propre type +Je ne trouve rien dans le papier qui interdise ça. Tous les noms de classes utilisés n'ont pas de contrainte, les seules contraintes étant que les méthodes *return* aient bien le type spécifié. + +### 17-18 Noms de classe étranges +La raison de ce choix de noms de classe est le besoin de faire une classe mère au nom simple (comme `Bool`, `List` ou `Int` afin que les types des méthodes soient clairs coté développeur (Pouvoir faire `Int meth(Bool x, List l)`. De là, j'avais deux choix. Ou bien je créais une sous-classe par cas de mon type inductif (On aurait `BoolTrue` et `BoolFalse` qui seraient deux filles de `Bool` et qui donneraient une certaines implémentation à `ite`), ou alors, faire qu'une des deux soit la classe mère, de façon «invisible» pour le développeur, tant que ce dernier n'utilise pas les noms des classes internes. +Pour la liste, on a encore le problème que une classe ne peut pas avoir un attribut de son propre type est être instanciable. Il faut donc nécessairement une classe mère à la classe représentant `Cons`, et que cette classe s'appelle `List`. + +### 19 - Notation C0 +J'ai utilisé le nom de classe `C0` que je trouve aussi moche. Dans le document original du FJ, la notation était utilisée avec le zéro en *subscript*. Mais alors, j'ai l'impression que ça casse le mur du formattage FJ de mettre du *subscript* sur du texte en *typewriter font*. Peut-être utiliser un autre nom ? `Cc` ? diff --git a/RapportStage.tex b/RapportStage.tex index de7d862..f3c28de 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -49,7 +49,9 @@ \end{center} où \fj{x} est un nom de variable, \fj{C} un nom de classe, \fj{f} un nom d'attribut de classe et \fj{m} un nom de méthode de classe. - On dit d'une expression qui ne contient pas de noms de variable (\autoref{rule:expr:variable}) qu'elle est \emph{fermée}. Dans la suite du document, nous allons utiliser le terme \enquote{expression} pour désigner les expressions fermées. Les expressions quelconques seront désignées par \emph{expressions ouvertes} ou \emph{expressions à variables}. + On dit d'une expression qui ne contient pas de noms de variable (\autoref{rule:expr:variable}) qu'elle est \emph{fermée}. Dans la suite du document, nous allons utiliser le terme \enquote{expression} pour désigner les expressions fermées. Les expressions quelconques seront désignées par \emph{expressions ouvertes} ou \emph{expressions à variables}, parfois notées $h$. + + Nous allons ausssi noter $\alpha$,$\beta$,$\varepsilon$,$\gamma$ les \eng{mappings} d'un ensemble de noms de variables vers un ensemble d'expressions fermées. On va ainsi définir la complétion d'une expression à variables par un de ces \eng{mappings}, ce qui sera noté $h\bracket{\alpha}$ où l'on remplace chaque occurrence d'une variable par l'image par $\alpha$ de ce nom de variable. Le langage définit aussi des classes, qui sont composées d'un nombre quelconque d'attributs nommés dont le type est spécifié, d'un unique constructeur qui prend autant de paramètres que la classe a d'attributs et qui définit tous ces derniers, et d'un nombre quelconque de méthodes ayant un nom, un type de retour, des paramètres ayant un nom et un type et surtout un corps, qui est une expression ouverte utilisant les noms de variable décrits dans les paramètres plus éventuellement le nom de variable spécial \fj{this} désignant l'objet duquel la méthode est appelée. Les classes ont aussi une classe mère, par défaut la classe \fj{Object} de laquelle elles héritent les attributs et les méthodes, qu'elles peuvent surcharger sans changer leur type. @@ -526,7 +528,7 @@ \[(\mathcal{A},e)\prec(\mathcal{B},f) \implies (\mathcal{A},h\bracket{e})\prec(\mathcal{A},h\bracket{f})\] - Cependant, cela est généralement faux, puisque il est possible en Featherweight Java de considérer des expressions qui vont se réduire à l'infini, mais que l'on peut \enquote{utiliser} avec des appels à méthodes ou des attributs. Nous pouvons par exemples utiliser les listes infinies, définies en annexe (\autoref{anx:classes:listes}). Cette classe définie deux attributs, dont un de son propre type. + Cependant, cela est généralement faux, puisque il est possible en Featherweight Java de considérer des expressions qui acceptent une suite infinie de réductions, mais que l'on peut \enquote{utiliser} avec des appels à méthodes ou des attributs. Nous pouvons par exemples utiliser les listes infinies, définies en annexe (\autoref{anx:classes:listes}). Cette classe \fj{IList} définit deux attributs, dont un de son propre type. \begin{figure} \begin{fjlisting} @@ -539,7 +541,7 @@ \label{fig:ilistsDefs} \end{figure} - Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e_i = \fj{intList(0)}$ et $e_0 = \fj{zeroList()}$. Tels que nous les avons défini précédemment, nos preordres ne permettent pas de différencier ces deux expressions. En effet, puisque aucune des deux ne se réduit en une valeur, on est dans une situation de $\text{faux}\implies\text{faux}$. Cependant, certaines expressions à trou sont capables de les différencier. On peut par exemple considérer l'expression $h = \fj{$\hole$.next.obj}$, nous aurons effectivement les réductions suivantes: + Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e_i = \fj{intList(0)}$ et $e_0 = \fj{zeroList()}$. Tels que nous les avons défini précédemment, nos preordres ne permettent pas de différencier ces deux expressions. En effet, puisque aucune des deux ne se réduit en une valeur, on est dans une situation où les prémisses ne sont jamais vérifiées, et donc, l'universalité du vide s'applique. Cependant, certaines expressions à trou sont capables de les différencier. On peut par exemple considérer l'expression $h = \fj{$\hole$.next.obj}$, nous aurons effectivement les réductions suivantes: \[ \begin{array}{rcl} @@ -559,51 +561,49 @@ \] % TODO faut-il adapter l'exemple aux test interfaces au risque de trop surcharger ? - Nous avons l'impression que certaines expressions forment des sortes de \enquote{valeurs infinies}, qui peuvent quand même être utilisées dans des programmes, mais uniquement de manière finie. Nous allons donc redéfinir tous les préordres, en remplacant les propositions de la forme suivante. + Nous avons l'impression que certaines expressions forment des sortes de \enquote{valeurs infinies}, qui peuvent quand même être utilisées dans des programmes, mais uniquement de manière finie. Nous allons donc changer la définition de tous nos préordres, en remplaçant les propositions de la forme suivante. \[\forall v\quad (\mathcal{A}, e) \Downarrow v \implies (\mathcal{B}, f) \Downarrow v\] - Nous allons tout d'abord définir une nouvelle grammaire, celle des \enquote{valeurs à trou}, que l'on notera souvent avec la lettre $\hbar$. Les valeurs simples sont identifiées aux valeurs à zéro trous, et par exemple, l'objet suivant est une expression à trois trous - \[\fj{new C([.],new S(new S([.],new G()),[.]))}\] + Nous allons tout d'abord définir une nouvelle grammaire, celle des \enquote{valeurs ouvertes} ou \enquote{valeurs avec variables}, que l'on notera avec la lettre $\hbar$. Il s'agit simplement d'expressions ouvertes qui ne contiennent que des nœuds de type \textsc{E-Var} et \textsc{E-Cstr} et telles que un nom de variable n'est utilisé au plus qu'\emph{une seule fois}. + %TODO Rajouter des références sur ces deux noms de règles + Par exemple, l'objet suivant est une valeur à trois variables + \[\fj{new C(x,new S(new S(y,new G()),z))}\] - La grammaire est la suivante, on définit également l'opération de remplissage des trous, comme fait pour la définition des expressions à trou. - \[\hbar := \hole \spacebar \fj{new C($\overline{\hbar}$)}\] - \marginpar{y a t'il besoin de redéfinir le remplissage des trous ?} + On a donc aussi une opération de remplissage, comme pour les expressions à variables, que l'on note de la même manière. On supposera que si l'on marque $\hbar\bracket{\alpha}$, c'est que l'ensemble des variables libres de $\hbar$ est inclus dans l'ensemble de définition de $\alpha$. Nous alons alors pouvoir redéfinir le préordre sur deux programmes : - \[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \overline{e'} \quad \left(e \rightarrow_\mathcal{A}^* \hbar\left[\overline{e'}\right] \implies \exists \overline{e''}\quad f \rightarrow_\mathcal{B}^* \hbar \left[\overline{e''}\right]\right)\] + \[(\mathcal{A},e)\pprec(\mathcal{B},f) \ssi \forall \hbar \forall \alpha \quad \left(e \rightarrow_\mathcal{A}^* \hbar\bracket{\alpha} \implies \exists \beta\quad f \rightarrow_\mathcal{B}^* \hbar\bracket{\beta}\right)\] Intuitivement, on vérifie que si d'un coté du préordre, l'expression peut s'évaluer en \fj{new C(...)}, alors l'autre coté s'évalue en un objet de la même classe, et ce récursivement. \marginpar{Cette expression me semble peu claire.} - On redéfit ainsi tous les autres préordres, notamment celui sur les \eng{class tables}: + On change ainsi la définition de tous les autres préordres, notamment celui sur les \eng{class tables}: \[\mathcal{A}\pprec\mathcal{B} \ssi \forall e \quad (\mathcal{A},e) \pprec (\mathcal{B},e)\] - Nous allons maintenant étudier les propriétés de ce préordre. + Nous allons maintenant étudier les propriétés de cette nouvelle définition du préordre. \begin{property} - $$\forall \hbar \forall \overline{e} \quad \hbar\left[\overline{e}\right]\rightarrow e' \implies \exists \overline{e''}\quad e' = \hbar\left[\overline{e''}\right]$$ - - On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction. - \marginpar{y a t'il besoin d'une preuve plus complète ?} + \[\forall \hbar \forall \overline{e} \quad \hbar\left[\overline{e}\right]\rightarrow e' \implies \exists \overline{e''}\quad e' = \hbar\left[\overline{e''}\right]\] \end{property} + On peut prouver cette propriété inductivement en montrant qu'une expression ayant un nœud \enquote{\fj{new}} en nœud racine se réduira forcément en une expression ayant un nœud racine du même type, en inversant la relation de réduction. + %TODO Preuve complète + \begin{property} - $$\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}$$ - - Il s'agit d'une particularisation, puisque qu'une valeur est une valeur à trou sans trou. + \[\mathcal{A} \pprec \mathcal{B} \implies \mathcal{A} \prec \mathcal{B}\] \end{property} + Il s'agit d'une particularisation, puisque qu'une valeur est une valeur à trou sans trou. \begin{property}[Context Lemma] - L'objectif de cette nouvelle définition était d'obtenir une sorte de \textit{context lemma}, puisque nous comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}. - \begin{gather*} \forall \mathcal{A} \quad\forall e,f \quad\forall (h,\mathcal{B})\\ (e,\mathcal{A})\pprec(f,\mathcal{B}) \implies (h[e],\mathcal{A} \oplus \mathcal{B})\pprec(h[f],\mathcal{A}\oplus\mathcal{B}) \end{gather*} - - La démonstration est présentée en annexe (\autoref{anx:proofHValCL}) - \marginpar{Besoin de présenter rapidement la preuve} \end{property} + Ce théorème était en quelque sorte l'objectif de cette redéfinition, puisque nous comparons dorénavant les expressions sur \enquote{toutes les valeurs qu'elles pourraient renvoyer}. + + La demonstration se fera sur une version plus puissante du théorème où $h$ peut prendre plusieurs trous. La preuve se fait ensuite par récurrence sur la longueur de la chaine de réduction, en discriminant selon l'emplacement de la réduction (dans $h$, dans $e$ ou entre les deux), et en changeant les noms de variables afin de pouvoir boucler la récurrence. La démonstration complète est présentée en \autoref{anx:proofHValCL}. + \section{Conclusion} @@ -671,34 +671,34 @@ Nous allons donc essayer de montrer, par induction sur la preuve de la prémisse, la propriété suivante - \[\mathfrak{T},\mathcal{B}, \Gamma \Vdash e : \fj{C} \implies \exists \fj{C'}\quad \mathcal{A}\oplus\mathcal{B},\Gamma \vdash e : \fj{C'} \quad\text{et}\quad \fj{C'} \subclass \fj{C}\] + \[\mathfrak{T},\mathcal{B}, \Gamma \Vdash e : \fj{D} \implies \exists \fj{C}\quad \mathcal{A}\oplus\mathcal{B},\Gamma \vdash e : \fj{C} \quad\text{et}\quad \fj{C} \subclass \fj{D}\] \subsection{Propriétés sur les fonctions utilitaires} La définition de $\vdash$ dans Featherweight Java de base utilise les fonctions utilitaires non surchargées. Afin de bien les différencier, nous allons noter avec un prime les versions surchargées définies \autoref{fig:typops}. - Par exemple, $(\operatorname{fields'})$ correspond à la définition surchargée dans la \eng{test interface} $\mathfrak{T}$ et la \eng{class table} de tests $\mathcal{B}$, et $(\operatorname{fields})$ correspond à la définition originale dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. Il en va de même pour l' opérateur $(\subclass')$, qui dénotera la cloture transitive et réflexive de l'union des relations \fj{<:} sur $\mathfrak{T}$ et \fj{extends} dans $\mathcal{B}$ et l'opérateur $(\subclass)$ qui dénotera la relation de sous-typage sur la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. + Par exemple, $(\operatorname{fields'})$ correspond à la définition surchargée dans la \eng{test interface} $\mathfrak{T}$ et la \eng{class table} de tests $\mathcal{B}$, et $(\operatorname{fields})$ correspond à la définition originale dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. Il en va de même pour l'opérateur $(\subclass')$, qui dénotera la cloture transitive et réflexive de l'union des relations \fj{<:} sur $\mathfrak{T}$ et \fj{extends} dans $\mathcal{B}$ et l'opérateur $(\subclass)$ qui dénotera la relation de sous-typage sur la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$. Nous allons déjà montrer les trois propriétés suivantes sur ces fonctions utilitaires: \[ \begin{array}{rcl} - \fj{C}\;\fj{f} \in \operatorname{fields'}(\fj{C0}) &\implies& \exists \fj{C'}\subclass\fj{C}\quad\fj{C'}\;\fj{f} \in \operatorname{fields}(\fj{C0}) \\ - \operatorname{mtype'}(\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}(\fj{m},\fj{C0}) = \overline{\fj{D'}}\rightarrow\fj{C'}\\ - \operatorname{construct'}(\fj{C0}) = \overline{\fj{D}} & \implies & \exists \overline{\fj{D'}} \superclass \overline{\fj{D}}\quad\exists \overline{\fj{f}} \quad \operatorname{fields}(\fj{C0}) = \overline{\fj{D'}}\;\overline{\fj{f}} + \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}} \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'}(\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{C0})$, il y a quatre possibilités. - \subparagraph{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}(\fj{E})$} + \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}(C0)$ + Alors, par construction de $\operatorname{fields}$, on a $\fj{C}\;\fj{f} \in \operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(C0)$ \subparagraph{Cas $\left[\fj{C0 \{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 @@ -709,19 +709,18 @@ \[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{C0})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\] \paragraph{Seconde propriété} - Procédons un peu de la même manière, par induction sur la définition de $\operatorname{mtype'}$. + Procédons par induction sur la définition de $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}$. - Nous avons comme hypotèse $\operatorname{mtype'}(\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C}$. + Nous avons comme hypothèse $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) = \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})}} 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}\] - CQFD. \subparagraph{Cas $\fj{class C0 \{...,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}\] - CQFD. + \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}})} \label{proof:mtype:cchain} @@ -733,25 +732,24 @@ Or, on sait que les défintions de $\mathcal{A}$ et $\mathcal{B}$ sont $\textsc{OK}$ (c'est imposé par la définition de $\mathcal{A}\triangleright\mathfrak{T})$. On a donc que pour chacune de ces classes: - \[\operatorname{mtype}(\fj{m},\fj{C}_n) = \operatorname{mtype}(\fj{m},\fj{C}_{n-1}) = \cdots = \operatorname{mtype}(\fj{m},\fj{C}_0)\] + \[\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}$. CQFD + Donc $\operatorname{mtype}(\fj{m},\fj{C0}_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'}(\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{C0}) = \overline{\fj{D}}$. \subparagraph{Cas $\left[\fj{C0 ($\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 règle (\ref{rule:tri:constructor}), et on a donc + 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)\] - CQFD \subparagraph{Cas $\fj{class C0\{C0($\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}(\fj{C0}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\] + \[\operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{C0}) = \overline{\fj{D}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\] \subsection{Corps de la preuve} @@ -773,7 +771,7 @@ \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'}(\fj{C0}) + \item \fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{C0}) \end{hyps} On peut alors appliquer la première propriété sur la quatrième hypotèse qui nous donne @@ -787,16 +785,16 @@ \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 \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'}(\fj{m},\fj{C0}) = \overline{\fj{D}} \rightarrow \fj{C} + \item \operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{C0}) = \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}(\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{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}\] - Alors, en utilisant la même preuve que pendant la preuve de la sous propriété (\autoref{proof:mtype:cchain}) + Alors, en utilisant la même preuve que pendant la preuve de la sous propriété (page \pageref{proof:mtype:cchain}) - \[\operatorname{mtype}(\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{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'}}\] On peut maintenant appliquer la règle FJ \textsc{T-Invk} et obtenir le résultat. @@ -805,12 +803,12 @@ \item e = \fj{new C($\overline{e_x}$)} \item \fj{C} = \fj{C} \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{construct'}(\fj{C}) = \overline{\fj{D}} + \item \operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{C}) = \overline{\fj{D}} \item \overline{\fj{CX}} \subclass \overline{\fj{D}} \end{hyps} On peut appliquer la troisième propriété sur la quatrième hypothèse. On obtient alors que : - \[\operatorname{fields}(\fj{C}) = \overline{\fj{D'}}\;\overline{\fj{f}} \quad\text{et}\quad \overline{\fj{CX'}} \subclass \overline{\fj{CX}} \subclass \overline{\fj{D}} \subclass \overline{\fj{D'}}\] + \[\operatorname{fields}_{\mathcal{A}\oplus\mathcal{B}}(\fj{C}) = \overline{\fj{D'}}\;\overline{\fj{f}} \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-New} et obtenir le résultat. @@ -828,7 +826,7 @@ On peut donc appliquer directement la règle \textsc{T-UCast} \subparagraph{\textnormal{\textsc{\ref{rule:ti:downCast}}}} - Exactement la même preuve que le point précédent en appliquant la règle \textsc{T-UCast} + Exactement la même preuve que le point précédent en appliquant la règle \textsc{T-DCast} \section{Preuve du \eng{context lemma} avec valeurs infinies} \label{anx:proofHValCL} @@ -839,12 +837,12 @@ Déjà, nous ne spécifierons pas la \eng{class table}, puisque nous supposerons que nous travaillerons dans la \eng{class table} $\mathcal{A} \oplus \mathcal{B}$, car puisque le $\oplus$ impose que les noms de classe n'entrent pas en collision, si un expression s’exécutant dans $\mathcal{A}$ ou $\mathcal{B}$ s'executera de la même façon dans $\mathcal{A}\oplus\mathcal{B}$. - $h$ définira une expression FJ possédant des variables libres (càd, des nœuds de la forme \fj{x}). Bien que ce soient techniquement des expressions FJ, nous les dénoterons ainsi afin de ne pas les confondre avec les expressions \enquote{fermées}, dénotées elles $e$,$f$. + $h$ dénotera une expression FJ quelconque (ou ouverte). Nous les dénoterons ainsi afin de ne pas les confondre avec les expressions \enquote{fermées}, dénotées elles $e$,$f$. - Nous allons ausssi noter $\varepsilon$, $\gamma$ les \eng{mappings} d'un ensemble de noms de variables vers un ensemble d'expressions fermées. On va ainsi définir la complétion d'une expression ayant des variables libres par un de ces \eng{mappings}, ce qui sera noté $h\bracket{\varepsilon}$ où l'on remplace chaque occurrence d'une variable par l'image par $\varepsilon$ de ce nom de variable. + Nous noterons aussi $\varepsilon$ et $\gamma$ les \eng{mappings} servant à \enquote{remplir} les expression ouvertes, afin de ne pas les confondre avec $\alpha$ et $\beta$, qui servent à remplir les valeurs à variables. On note toujours le préordre entre deux expressions fermées de la même façon: - \[e \prec f \ssi \forall\hbar \quad (\exists \overline{e'}\quad e \rightarrow \hbar\bracket{\overline{e'}}) \implies (\exists \overline{f'}\quad f \rightarrow \hbar\bracket{\overline{f'}})\] + \[e \prec f \ssi \forall\hbar \quad (\exists \alpha\quad e \rightarrow \hbar\bracket{\alpha}) \implies (\exists \beta\quad f \rightarrow \hbar\bracket{\beta})\] Nous allons aussi étendre cette définition à deux \eng{mappings} ayant le même domaine: \[\varepsilon \prec \gamma \ssi \forall \fj{x}\in\operatorname{Dom}(\varepsilon)=\operatorname{Dom}(\gamma)\quad \varepsilon(\fj{x}) \prec \gamma(\fj{x})\] @@ -857,32 +855,33 @@ Pour $h$ expression avec des variables libres tel que $\operatorname{Var}(h) \subset \operatorname{Dom}(\varepsilon)$\\ Si $\varepsilon \prec \gamma$\\ Alors $h\bracket{\varepsilon} \prec h\bracket{\gamma}$\\ - C'est à dire \[\forall \hbar \left(\exists \overline{e'}\quad h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\overline{e'}}\right)\implies\left(\exists f'\quad h\bracket{\gamma}\rightarrow^* \hbar\bracket{\overline{f'}}\right)\] + C'est à dire \[\forall \hbar \left(\exists \alpha\quad h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\alpha}\right)\implies\left(\exists \beta\quad h\bracket{\gamma}\rightarrow^* \hbar\bracket{\beta}\right)\] \end{theorem} C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}). - Nous allons Tout d'abord faire une récurrence sur la taille de la réduction $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\overline{e'}}$, notée $n$. + Nous allons Tout d'abord faire une récurrence sur la taille de la réduction $h\bracket{\varepsilon}\rightarrow^* \hbar\bracket{\beta}$, notée $n$. \paragraph{Initialisation} On essaie alors de montrer le résultat par induction sur $\hbar$. - On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$. + On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\alpha}$. \subparagraph{Cas $\hbar = \hole$}¨ Alors - \[h\bracket{\gamma} = \hbar\bracket{\overline{f'}}\quad\text{avec}\quad \overline{f'} = \left(h\bracket{\gamma}\right)\] + \[h\bracket{\gamma} = \hbar\bracket{\beta}\quad\text{avec}\quad \beta = \left(h\bracket{\gamma}\right)\] \subparagraph{Cas $\hbar = \fj{new C($\overline{\hbar'}$)}$} Alors, il y a deux possibilités. - Ou bien, on a $h = \fj{x}$, et alors puisque $\varepsilon \prec \gamma$ et que $\varepsilon(\fj{x}) = \hbar\bracket{\overline{e'}}$, alors, on a que $\gamma(\fj{x})\rightarrow^*\hbar\bracket{\overline{f'}}$ - Ou bien, on a $h = \fj{new C($\overline{h'}$)}$, et donc par induction - \[\overline{h'}\bracket{\gamma} \rightarrow^* \overline{\hbar'\bracket{\overline{f''}}}\] + Ou bien, on a $h = \fj{x}$, et alors puisque $\varepsilon \prec \gamma$ et que $\varepsilon(\fj{x}) = \hbar\bracket{\alpha}$, alors, on a que $\gamma(\fj{x})\rightarrow^*\hbar\bracket{\beta}$ - Et donc, en notant $\overline{f'}$ la concaténation des $\overline{\overline{f''}}$, on obtient que - \[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\] + Ou bien, on a $h = \fj{new C($\overline{h'}$)}$, et donc par induction + \[\overline{h'}\bracket{\gamma} \rightarrow^* \overline{\hbar'\bracket{\beta'}}\] + + Et donc, en notant $\beta$ la concaténation des $\overline{\beta'}$ (puisque les noms de variables sont utilisés de manière unique, les domaines de définition sont donc disjoints), on obtient que + \[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\beta}\] \paragraph{Hérédité} @@ -891,14 +890,14 @@ Nous aurons ensuite trois cas, suivant l'endroit où s'effectue la première étape de la réduction. - \underline{La réduction se fait uniquement avec des nœuds de $h_x$} - Alors, on a $h_x \rightarrow h_x'$, et donc $h \rightarrow h'$ indépendamment du \eng{mapping} considéré et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}$, alors, on a - \[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\] + \underline{La réduction se fait uniquement avec des nœuds de $h$} + Alors, on a $h \rightarrow h'$ indépendamment du \eng{mapping} considéré, et on peut appliquer \textsc{(HR)} qui nous donne que, puisque $h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\alpha}$, alors, on a + \[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\beta}\] - \underline{La réduction se fait sur un nœud à l'interieur d'une variable $\fj{x}$ de $h_x$} - Alors, dans cette occurrence de la variable $\fj{x}$ dans $h_x$, nous avons une réduction de la forme suivante. + \underline{La réduction se fait sur un nœud à l’intérieur d'une variable $\fj{x}$ de $h$} + Alors, dans cette occurrence de la variable $\fj{x}$ dans $h$, nous avons une réduction de la forme suivante. \[\varepsilon(\fj{x}) \rightarrow e^{\fj{x}}\] - Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$, ici noté $\fj{y}$, et créons $\varepsilon'$ ainsi: + Choisissons alors un nom de variable non utilisé dans $\epsilon$ et $\gamma$ : $\fj{y}$, et créons $\varepsilon'$ ainsi: \[\varepsilon' = \left[ \begin{array}{ccc} \fj{x} &\mapsto& \varepsilon(\fj{x})\\ @@ -913,7 +912,7 @@ \end{array} \right]\] Ainsi, la réduction considérée s'exprime comme - \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\] + \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\alpha}\] Or, nous avons aussi que $\varepsilon' \prec \gamma'$. Nous n'avons en effet que $\varepsilon(\fj{y})\prec\gamma(\fj{y})$ à vérifier, c'est à dire que $\varepsilon(\fj{x})\rightarrow e^{\fj{x}} \prec \gamma(\fj{x})$ @@ -924,9 +923,9 @@ \node (e2) at (0,0) {$e^{\fj{x}}$}; - \node (e3) at (0,-1) {$\hbar\bracket{\overline{e'}}$}; + \node (e3) at (0,-1) {$\hbar\bracket{\alpha}$}; - \node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$}; + \node (e4) at (1,-2) {$\hbar\bracket{\alpha'}$}; \draw[->] (e1) -- (e2); \draw[->] (e2) to node[very near end, above right] {$*$} (e3); @@ -960,12 +959,12 @@ \end{array} \right]\] Nous avons alors toujours $\varepsilon' \prec \gamma'$, mais aussi que la première réduction s'écrit - \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\] + \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\alpha}\] où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$. On peut donc appliquer l'hypothèse de récurrence. pour obtenir, puisque les \eng{class table} considérées sont les mêmes - \[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\overline{f'}}\] + \[h\bracket{\gamma} \rightarrow h'\bracket{\gamma'} \rightarrow^* \hbar\bracket{\beta}\] Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même. @@ -976,7 +975,7 @@ Nous pouvons garder $\varepsilon$ et $\gamma$ tels qu'ils sont. Alors, en remplacant l'appel $\fj{x.meth($\overline{h'}$)}$ susnommé par $h_m'$ dans $h$, on obtient une nouvelle expression $h'$ telle que la réduction soit - \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\] + \[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon} \rightarrow^{n-1} \hbar\bracket{\alpha}\] Mais en ayant aussi que \[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\] diff --git a/header.tex b/header.tex index 73a4be0..57b226e 100644 --- a/header.tex +++ b/header.tex @@ -67,6 +67,7 @@ \addto\extrasfrench{% \renewcommand{\figureautorefname}{\textsc{Figure}} \renewcommand{\appendixautorefname}{Annexe} + \renewcommand{\theoremautorefname}{Théorème} \providecommand\ruleautorefname{règle} } @@ -159,7 +160,7 @@ } \newcommand{\printcomma}{,} \newcommand{\fjparamconstparameters}[2][Object]{ - \ifnullthenelse{fjargcount}{}{,} \text{#1} \;\text{#2} + \ifnullthenelse{fjargcount}{}{,$\text{ }$} \text{#1} \;\text{#2} \stepcounter{fjargcount} } \newcommand{\fjparamconstassign}[2][Object]{