diff --git a/RapportStage.tex b/RapportStage.tex index 7c8de4f..74027ce 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -518,14 +518,14 @@ & \newtag{\textrm{\textsc{(TI-New)}}}{rule:ti:new} \\[3ex] \infer - {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} - & \newtag{\textrm{\textsc{(TI-DCast)}}}{rule:ti:downCast} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} + & \newtag{\textrm{\textsc{(TI-UCast)}}}{rule:ti:upCast} \\[3ex] \infer {\mathfrak{T},\mathcal{B},\Gamma \Vdash \fj{(C)$e$} : \fj{C}} - {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{C} \subclass \fj{D} \quad \fj{C} \neq \fj{D}} - & \newtag{\textrm{\textsc{(TI-UCast)}}}{rule:ti:upCast} + {\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D} \quad \fj{D} \subclass \fj{C}} + & \newtag{\textrm{\textsc{(TI-DCast)}}}{rule:ti:downCast} \end{tabular} \end{tcolorbox} \caption{Typage des expressions avec une \eng{test interface} et une \eng{class table}} @@ -818,8 +818,10 @@ 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{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}\] - + \begin{equation} + \label{eqn:ptePartielle} + \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} + \end{equation} \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}. @@ -828,47 +830,49 @@ 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'}_{\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} - \] + \begin{align} + \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}) \label{eqn:utl:fields}\\ + \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'} \label{eqn:utl:mtype}\\ + \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}} \label{eqn:utl:construct} + \end{align} - \paragraph{Première propriété} + \renewcommand\equationautorefname{Propriété} + \paragraph{\autoref{eqn:utl:fields}} 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{Cc})$, il y a quatre possibilités. + Nous pouvons déjà discriminer sur le cas suivant: - \subparagraph{Cas $\fj{C}\;\fj{f} \in \bigcup_{\fj{C}\subclass'\fj{E}}\operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{E})$} + \underline{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 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)$ + \underline{Sinon} + En inversant la règle qui permet de prouver $\fj{C}\;\fj{f} \in \operatorname{fields'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc})$, il y reste trois possibilités, correspondant aux trois règles de construction de $\operatorname{fields}$. La première discrimination permet d'éliminer les second cas où l'attribut aurait été défini pour une classe mère. - \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 + \subparagraph{Cas $\left[\fj{Cc \{C f, ...\}}\right] \in \mathfrak{T}$ \textnormal{\ref{rule:lti-fields}}} + Alors, en inversant la preuve de $\mathcal{A} \triangleright \mathfrak{T}$, on obtient une seule règle possible: la règle \ref{rule:tri:attributes}, et on a donc \[\fj{C'} \fj{f} \in \operatorname{fields}_\mathcal{A}(\fj{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\] - \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, + \subparagraph{Cas $\left[\fj{Cc (..., C f, ...)}\right] \in \mathfrak{T}$ \textnormal{\ref{rule:lti-fields2}}} + Alors, en inversant la preuve de $\mathcal{A} \triangleright \mathfrak{T}$, on obtient une seule règle possible: 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{Cc})\quad\text{et}\quad \fj{C'}\subclass\fj{C}\] - \paragraph{Seconde propriété} + \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}}(\fj{Cc})$ (On prend $\fj{C'} = \fj{C}$) + + \paragraph{\autoref{eqn:utl:mtype}} 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{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}$. + Nous avons comme hypothèse $\operatorname{mtype'}_{\mathfrak{T},\mathcal{B}}(\fj{m},\fj{Cc}) = \overline{\fj{D}} \rightarrow \fj{C}$. - \subparagraph{Cas $\left[\fj{Cc : 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 Cc \{...,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{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{Cc}$ (\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{Cc}$, alors, il existe une chaine de classes @@ -877,31 +881,35 @@ telles que $\fj{C}_k\;\fj{extends}\;\fj{C}_{k+1}$ dans $\mathcal{A}$ ou $\mathcal{B}$. 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})$. + Être $\textsc{OK}$ implique notamment que l'on ne change pas le type d'une méthode que l'on aurait éventuellement surchargée. On a donc que pour chacune de ces classes: \[\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{Cc}_n) = \overline{\fj{D}}\rightarrow \fj{E}$. + Donc $\operatorname{mtype}(\fj{m},\fj{Cc}) = \overline{\fj{D}}\rightarrow \fj{E}$. - \paragraph{Troisième propritété} + \paragraph{\autoref{eqn:utl:construct}} - Une dernière fois, inversons la règle qui a permis de prouver : \[\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}\] + Inversons la règle qui a permis de prouver : \[\operatorname{construct'}_{\mathfrak{T},\mathcal{B}}(\fj{Cc}) = \overline{\fj{D}}\] - \subparagraph{Cas $\left[\fj{Cc ($\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 Cc\{Cc($\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{Cc}) = \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}}\;\overline{\fj{f}} \quad\text{et}\quad \overline{\fj{D}} \subclass \overline{\fj{D}}\] \subsection{Corps de la preuve} - Démarrons l'induction sur la preuve de la propriété présentée au début de la section. + Démarrons l'induction sur la preuve de la prémisse de la \autoref{eqn:ptePartielle}, présentée au début de la section. + Cette prémisse est la suivante: + \[\mathfrak{T},\mathcal{B},\Gamma \Vdash e : \fj{D}\] + Je vais, pour chaque règle, lister directement en dessous la liste des hypothèses qu'elle induit. \subparagraph{\textnormal{\textsc{\ref{rule:ti:variable}}}} \begin{hyps} @@ -921,7 +929,7 @@ \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 + On peut alors appliquer la \autoref{eqn:utl:fields} sur la quatrième hypotèse qui nous donne \[\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} @@ -936,10 +944,10 @@ \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 + On peut alors appliquer la \autoref{eqn:utl:mtype} sur la cinquième hypothèse, on obtient que \[\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}) + Alors, en utilisant la même preuve que pendant la preuve de la \autoref{eqn:utl:mtype} (après inversion de la règle \ref{rule:lup-method}) \[\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'}}\] @@ -954,7 +962,7 @@ \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 : + On peut appliquer la \autoref{eqn:utl:construct} sur la quatrième hypothèse. On obtient alors que : \[\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. @@ -967,7 +975,7 @@ \item \fj{D} \subclass \fj{C} \end{hyps} - On a alors l'inégalité suivante : + On a alors les relations de sous-typage suivante : \[\fj{D'} \subclass \fj{D} \subclass \fj{C}\] On peut donc appliquer directement la règle \textsc{T-UCast} @@ -977,35 +985,37 @@ \section{Preuve de la \autoref{thm:hnewnew} sur les valeurs infinies} \label{anx:proofPt1Val} + On rappelle tout d'abord la propriété: + \[\forall \hbar \forall \alpha \quad \hbar\bracket{\alpha}\rightarrow^* e' \implies \exists \beta\quad e' = \hbar\bracket{\beta}\] + Nous allons d'abord montrer la propriété sur les expressions suivante: \begin{property} \label{thm:enewnew} Soit $e$ et $f$ des expressions fermées, telles que $e \rightarrow^* f$, - Alors, si $e = \fj{new C($\overline{e'}$)}$ + Si $e = \fj{new C($\overline{e'}$)}$ - On a $f = \fj{new C($\overline{f'}$)}$ et $\overline{e'} \rightarrow^* \overline{f'}$. + Alors $f = \fj{new C($\overline{f'}$)}$ et $\overline{e'} \rightarrow^* \overline{f'}$. \end{property} - Montrons cette propriété par récurrence sur la taille de la relation $e \rightarrow^* f$. + Montrons cette propriété par récurrence sur la longueur de la réduction $e \rightarrow^* f$. \subparagraph{Initialisation} Dans le cas $e = f$, on a simplement $f = \fj{new C($\overline{e'}$)}$ et $\overline{e'} \rightarrow^0 \overline{e'}$. \subparagraph{Hérédité} - Nous sommes dans l'hypothèse que $e \rightarrow^n f$ + Nous sommes dans l'hypothèse où $e \rightarrow^n f$. Observons la première relation. Elle se fait nécessairement sur un nœud de type \ref{rule:expr:method}, \ref{rule:expr:field} ou \ref{rule:expr:cast}, qui est donc contenu dans l'un des $\overline{e'}$. Donc, on a $e'_i \rightarrow e''_i$. On note $e''_k = e'_k$ pour $k$ différent de $i$, et on obtient que \[e = \fj{new C($\overline{e'}$)} \rightarrow \fj{new C($\overline{e''}$)} \rightarrow^{n-1} f\] On peut donc appliquer l'hypothèse de récurrence à la dernière relation $\rightarrow^{n-1}$, et nous obtenons bien que \[f = \fj{new C($\overline{f'}$)} \quad\text{et}\quad \overline{e'} \rightarrow^* \overline{e''} \rightarrow^* \overline{f'}\] - La récurrence est bouclée. + La récurrence est terminée. Nous allons donc pouvoir facilement montrer la \autoref{thm:hnewnew} par induction sur le paramètre $\hbar$. \subparagraph{$\hbar = \fj{x}$} - Alors, en notant $\beta$ tel que $\beta(\fj{x}) = e'$. + En notant $\beta$ tel que $\beta(\fj{x}) = e'$, on obtient que - Alors, \[\hbar\bracket{\alpha} = \alpha(\fj{x}) \rightarrow e' = \hbar\bracket{\beta}\] \subparagraph{$\hbar = \fj{new C($\overline{\hbar'}$)}$} @@ -1029,9 +1039,9 @@ 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é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$. + La lettre $h$ dénotera une expression FJ quelconque (ouverte ou fermée). Nous les dénoterons ainsi afin de ne pas les confondre avec les expressions \enquote{fermées}, dénotées elles $e$,$f$. - 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. + 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 avec 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 \alpha\quad e \rightarrow \hbar\bracket{\alpha}) \implies (\exists \beta\quad f \rightarrow \hbar\bracket{\beta})\] @@ -1051,15 +1061,15 @@ 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{\beta}$, notée $n$. + Nous allons tout d'abord faire une récurrence sur la longueur 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 démontre alors le résultat par induction sur $\hbar$. On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\alpha}$. - \subparagraph{Cas $\hbar = \hole$}¨ + \subparagraph{Cas $\hbar = \hole$} Alors \[h\bracket{\gamma} = \hbar\bracket{\beta}\quad\text{avec}\quad \beta = \left(h\bracket{\gamma}\right)\] @@ -1076,13 +1086,13 @@ \paragraph{Hérédité} - Notre hypothèse de récurrence, notée \textsc{(HR)} est la suivante: + Notre hypothèse de récurrence \textsc{(HR)} est la suivante: \[\forall h \quad \varepsilon \prec \gamma \implies h\bracket{\varepsilon} \prec^{