Continuation de la preuve du context lemma.
This commit is contained in:
parent
ac36aa6a5e
commit
235fbfafb5
GPG Key ID:
7054D5D6A90F084F
151
RapportStage.tex
151
RapportStage.tex
@ -505,7 +505,74 @@
|
||||
\caption{Définitions de listes infinies}
|
||||
\end{figure}
|
||||
|
||||
Par exemple, avec la \eng{class table} définie \autoref{fig:ilistsDefs}, nous pouvons considérer les deux expressions $e = \fj{intList(0)}$ et $e' = \fj{zeroList()}$.
|
||||
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:
|
||||
|
||||
\[
|
||||
\begin{array}{rcl}
|
||||
h\bracket{e_i} &=& \fj{intList(0).next.obj}\\
|
||||
&\rightarrow& \fj{new IList(0, intList(0+1)).next.obj}\\
|
||||
&\rightarrow& \fj{intList(0+1).obj}\\
|
||||
&\rightarrow& \fj{new IList(0+1, intList(0+1+1)).obj}\\
|
||||
&\rightarrow& \fj{0+1}\\
|
||||
&\rightarrow^{\!*}& \fj{1}\\
|
||||
|
||||
h\bracket{e_0} &=& \fj{zeroList().next.obj}\\
|
||||
&\rightarrow& \fj{new IList(0, zeroList()).next.obj}\\
|
||||
&\rightarrow& \fj{zeroList().obj}\\
|
||||
&\rightarrow& \fj{new IList(0, zeroList()).obj}\\
|
||||
&\rightarrow& \fj{0}
|
||||
\end{array}
|
||||
\]
|
||||
% 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.
|
||||
\[\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()),[.]))}\]
|
||||
|
||||
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}$)}\]
|
||||
%TODO y a t'il besoin de redéfinir le remplissage des trous ?
|
||||
|
||||
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)\]
|
||||
|
||||
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.
|
||||
%TODO Cette expression me semble peu claire.
|
||||
|
||||
On redéfit ainsi 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.
|
||||
|
||||
\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.
|
||||
%TODO y a t'il besoin d'une preuve plus complète ?
|
||||
\end{property}
|
||||
|
||||
\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.
|
||||
\end{property}
|
||||
|
||||
\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})
|
||||
%TODO Présenter rapidement la preuve
|
||||
\end{property}
|
||||
|
||||
|
||||
|
||||
|
||||
\section{Vers des équivalences plus pratiques}
|
||||
|
||||
@ -739,6 +806,88 @@
|
||||
|
||||
\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}
|
||||
|
||||
\subsection{Preuve du \eng{context lemma} avec les valeurs infinies}
|
||||
\label{anx:proofHValCL}
|
||||
|
||||
La première étape est de décomposer l'opérateur $\pprec$, et de changer l'ordre des opérateurs. Nous cherchons donc à prouver que
|
||||
|
||||
\begin{gather*}
|
||||
\forall \mathcal{A}\quad\forall e,f \quad\forall \mathcal{B} \\
|
||||
\left(\forall \hbar\quad e \rightarrow^* \hbar\bracket{\overline{e'}} \implies \exists \overline{f'}\quad f \rightarrow^* \hbar\bracket{\overline{f'}}\right) \implies \\
|
||||
\left(\forall h \forall \hbar \quad h\bracket{e} \rightarrow^* \hbar\bracket{\overline{e'}} \implies \exists \overline{f'}\quad h\bracket{f} \rightarrow^* \hbar\bracket{\overline{f'}}\right)
|
||||
\end{gather*}
|
||||
|
||||
On écrit $\rightarrow$ au lieu de $\rightarrow_{\mathcal{A}\oplus\mathcal{B}}$, afin d'alléger les notations.
|
||||
|
||||
Nous allons montrer un peu plus en considérant que $h$ est une expression avec un nombre quelconque de trous (mais tous remplacés par la même expression).
|
||||
%TODO: Y a t'il besoin de préciser le remplissage de ces expressions ?
|
||||
|
||||
Nous allons montrer le théorème en deux temps. D'abord, nous allons imposer comme contrainte que la réduction $h\bracket{e} \rightarrow^* \hbar\bracket{\overline{e'}}$ s'effectue sans application de méthode (\textsc{R-Meth}) à un appel à méthode contenu dans $h$. (C'est à dire que les appels à méthode de $h$ ne \enquote{servent à rien}, ils pourraient être remplacés par \fj{null} sans modifier la réduction).
|
||||
|
||||
Supposons alors $H_0:\quad \left(\forall \hbar\quad e \rightarrow^* \hbar\bracket{\overline{e'}} \implies \exists \overline{f'}\quad f \rightarrow^* \hbar\bracket{\overline{f'}}\right)$
|
||||
|
||||
Montrons le résultat recherché par \textbf{induction} sur $h$.
|
||||
|
||||
\paragraph{Premier cas: $\hbar = \hole$}
|
||||
Alors on note $\overline{f'} = \bracket{f}$ et donc $f \rightarrow^* f = \hbar\bracket{\overline{f'}}$
|
||||
|
||||
\paragraph{Sinon} on a nécessairement $\hbar = \fj{new C($\hbar_1$,$\hbar_2$,...,$\hbar_k$)}$. On note alors \[\hbar\bracket{\overline{e'}} = \fj{new C($\hbar_i\bracket{\overline{e^\prime}^i}$)}\quad\text{et}\quad\overline{e'} = \overline{e'}^1 \| \overline{e'}^2 \| \cdots \| \overline{e'}^k\]
|
||||
|
||||
\subparagraph{$h = \hole$}
|
||||
On applique dirèctement $H_0$
|
||||
|
||||
\subparagraph{$h = \fj{new D($e_1$,...,$e_{i-1}$,$h^\prime$,$e_{i+1}$,...,$e_{k^\prime}$)}$}
|
||||
|
||||
Alors, \fj{D}=\fj{C} et $k'=k$ car $\fj{new D(...$\null_{k^\prime}$)} \rightarrow^* \fj{new C(...$\null_k$)}$
|
||||
|
||||
Aussi, on a pour chaque $j$, $e_j \rightarrow^* \hbar_j\bracket{\overline{e'}^j}$
|
||||
|
||||
Donc \[h\bracket{f} = \fj{new C($e_1$,...,$e_{i-1}$,$h^\prime\bracket{e_2}$,$e_{i+1}$,...,$e_k$)}\]
|
||||
|
||||
Donc \[h\bracket{f}\rightarrow^*\fj{new C($\hbar_1\bracket{\overline{e^\prime}^1}$,...,$h'\bracket{f}$,...,$\hbar_k\bracket{\overline{e^\prime}^k}$)}\]
|
||||
|
||||
Or, $h'\bracket{e} \rightarrow^*\hbar_i\bracket{\overline{e'}^i}$, qui n'utilise pas de réduction de méthode (car sinon, la réduction de $h\bracket{e_1}$ en utiliserai).
|
||||
|
||||
Donc, en appliquant l'hypothèse d'induction à $h'$, on obtient que \[h'\bracket{f} \rightarrow^*\hbar_i\bracket{\overline{f'}}\].
|
||||
|
||||
Donc \[h\bracket{f} \rightarrow^* \fj{new C($\hbar_1\bracket{\overline{e^\prime}^1}$,...,$\hbar_i\bracket{\overline{f^\prime}}$,...,$\hbar_k\bracket{\overline{e^\prime}^k}$)} = \hbar\bracket{\overline{f''}}\]
|
||||
|
||||
\[\overline{f''} = \overline{e'}^1 \| \dots \| \overline{e'}^{i-1} \| \overline{f'} \| \overline{e'}^{i+1} \| \dots \| \overline{e'}^k\]
|
||||
|
||||
\subparagraph{$h = \fj{$h^\prime$.f}$}
|
||||
|
||||
Alors, $h'\bracket{e} \rightarrow^* \fj{new D($e^1$,...,$e^{k^\prime}$)}$, et donc:
|
||||
|
||||
\[h\bracket{e} \rightarrow^* \fj{new D($e^1$,...,$e^{k^\prime}$).f} \rightarrow e^i \rightarrow^* \hbar\bracket{\overline{e'}}\]
|
||||
|
||||
Donc
|
||||
\[\begin{array}{rcl}
|
||||
h'\bracket{e} &\rightarrow^*& \fj{new D($e^1$,...,$e^{k^\prime}$)}\\
|
||||
&\rightarrow^*& \fj{new D($e^1$,...,$e^{i-1}$,$\hbar\bracket{\overline{e^\prime}}$,$e^{i+1}$,...,$e^{k^\prime}$)}\\
|
||||
& = & \hbar'\bracket{e^1,\dots,\overline{e'},\dots,e^{k'}}\\
|
||||
& \text{où} & \hbar' = \fj{new D([.],...,[.],$\hbar$,[.],...,[.])}
|
||||
\end{array}\]
|
||||
|
||||
En appliquant l'hypothèse de récurrence à $h'$ et $\hbar'$, dont la réduction ne contient toujours pas d'appel à méthode (on observe une sous-réduction), on obtient \[h\bracket{f} = \fj{$h^\prime\bracket{f}$.f} \rightarrow^* \fj{$\hbar^\prime\bracket{\overline{f^\prime}}$.f}\]
|
||||
|
||||
Donc \[h\bracket{f} \rightarrow^* \hbar\bracket{\overline{f'}'}\]
|
||||
|
||||
\subparagraph{$h = \fj{$h_0^\prime$.meth($\overline{h^\prime}$)}$}
|
||||
Ce cas est impossible, car alors, pour se résoudre en une expression de type \fj{new} (ici, $\hbar\bracket{\overline{e'}}$), il faudrait nécessairement que l'appel à méthode de $h$ soit utilisé, ce qui n'est pas possible dans la réduction par hypothèse.
|
||||
|
||||
|
||||
On a donc démontré le lemme pour tous les cas, il nous manque d'inclure les appels à méthode.
|
||||
|
||||
%TODO: Faut-il préciser cette notion de «appel à méthode dans h'
|
||||
|
||||
\paragraph{Mélange de réduction} Nous allons maintenant transformer notre réduction afin de former une chaine sans appel à méthode dans l'expression à trou.
|
||||
|
||||
Soient $h$ et $\hbar$ tels que $h\bracket{e} \rightarrow^*\hbar\bracket{\overline{e'}}$ (sans autre contrainte). Alors, on peut changer l'ordre des étapes (voire en supprimer) afin d'obtenir une réduction de la forme suivante
|
||||
|
||||
\[h\bracket{e} \rightarrow^*_{\text{\textsc{R-Meth}}} h'\bracket{e} \underbrace{\rightarrow^*}_{\text{sans appel à méthode dans $h'$}}\hbar\bracket{\overline{e'}}\]
|
||||
|
||||
Pour ce faire, nous allons procéder de manière algorithmique, en \enquote{reculant} les réduction \textsc{R-Meth} vers le début.
|
||||
|
||||
|
||||
\end{document}
|
||||
|
||||
@ -52,6 +52,7 @@
|
||||
\newcommand\eng[1]{\textit{\foreignlanguage{english}{#1}}}
|
||||
\newcommand\spacebar{\;|\;}
|
||||
\def\nDownarrow{\not\mspace{1mu}\Downarrow}
|
||||
\let\pprec\preccurlyeq
|
||||
|
||||
\DeclareUnicodeCharacter{03BB}{$\lambda$}
|
||||
\DeclareUnicodeCharacter{03B1}{$\alpha$}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user