Prise en compte des commentaires de Clément - Preuves
This commit is contained in:
parent
c81d730465
commit
e158907268
GPG Key ID:
7054D5D6A90F084F
128
RapportStage.tex
128
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^{<n} h\bracket{\gamma}\]
|
||||
|
||||
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$}
|
||||
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
|
||||
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}$
|
||||
\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma} \rightarrow^* \hbar\bracket{\beta}\]
|
||||
|
||||
\underline{La réduction se fait sur un nœud à l’intérieur d'une variable $\fj{x}$ de $h$}
|
||||
@ -1107,7 +1117,7 @@
|
||||
|
||||
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})$
|
||||
|
||||
Cela est vrai par propriété de confluence sur l'opération de réduction.
|
||||
Cela est vrai par propriété de confluence sur l'opération de réduction. Intuitivement, un nœud d'une expression FJ ne peut se réduire que d'une seule façon (l'une des trois règles de réduction), et cette réduction se fait sans perte d'information (dans le sens où on aurait pas pu en extraire plus sans modifier le nœud en question). Il suffit donc de réduire les même nœuds des deux cotés afin d'obtenir une même expression.
|
||||
\begin{center}
|
||||
\begin{tikzpicture}
|
||||
\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
|
||||
@ -1126,9 +1136,9 @@
|
||||
\end{tikzpicture}
|
||||
\end{center}
|
||||
|
||||
On peut alors appliquer que $\varepsilon \prec \gamma$.
|
||||
On peut alors appliquer l'hypothèse $\varepsilon \prec \gamma$.
|
||||
|
||||
Nous avons toutes les conditions réunies qui nous permettent d'appliquer l'hypothèse de récurrence.
|
||||
Nous avons donc toutes les conditions réunies pour appliquer l'hypothèse de récurrence.
|
||||
|
||||
\underline{La réduction s'est faîte entre un nœud de $h$ et un nœud de $\varepsilon$}
|
||||
Il y a trois cas de figure pour lesquels les deux cas précédents ne sont pas adéquats. Le premier est un appel à \eng{field} de la forme $\fj{x.field}$, le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$ et le troisième cas est le \eng{cast} de la forme $\fj{(D)x}$.
|
||||
@ -1154,7 +1164,7 @@
|
||||
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
|
||||
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{\beta}\]
|
||||
|
||||
Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
|
||||
@ -1179,6 +1189,6 @@
|
||||
|
||||
\section{Le stage au LACL}
|
||||
\label{anx:stage}
|
||||
Je vais présenter ici le laboratoire dans lequel j'ai fait ce stage. Le Laboratoire d'Algorithmique, Complexité et Logique est un petit laboratoire inclus dans l'Université Paris-Est Créteil. Le laboratoire est donc dans un campus universitaire, et contient aussi quelques thésard·es, que je n'ai que peu vu à cause de la periode tardive du stage. Ce stage m'a en partie confirmé que je voulais m'orienter vers de la recherche, le travail bien que modeste que j'ai effectué correspondait à l'image que je me faisait de l'\enquote{exercice} de la recherche, ce que je n'avais jamais expérimenté avant. Je reste conscient que je n'ai vu qu'une très petite partie du quotidien d'un·e chercheur·e. J'ai aussi été sous la tutelle de Clément Aubert, Maître de conférence à l'université d'Augusta, Géorgie. Je n'ai pas beaucoup croisé les membres des autres équipes du laboratoire, ne serait-ce que pendant quelques discussions lors des pauses repas.
|
||||
Je vais présenter ici le laboratoire dans lequel j'ai fait ce stage. Le Laboratoire d'Algorithmique, Complexité et Logique est un laboratoire inclus dans l'Université Paris-Est Créteil. Le laboratoire est donc dans un campus universitaire, et accueille aussi quelques doctorant·es, que je n'ai que peu vu à cause de la periode tardive du stage. Ce stage m'a en partie confirmé que je voulais m'orienter vers de la recherche, le travail bien que modeste que j'ai effectué correspondait à l'image que je me faisait de l'\enquote{exercice} de la recherche, ce que je n'avais jamais expérimenté avant. Je reste conscient que je n'ai vu qu'une très petite partie du quotidien d'un·e chercheur·e. J'ai aussi été sous la tutelle de Clément Aubert, Maître de conférence à l'université d'Augusta, Géorgie. Je n'ai pas beaucoup croisé les membres des autres équipes du laboratoire, ne serait-ce que pendant quelques discussions lors des pauses repas.
|
||||
|
||||
\end{document}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user