From 9f708fe3798dbb10ec39b7ee706815f6814ffd8c Mon Sep 17 00:00:00 2001 From: Mysaa Date: Thu, 28 Jul 2022 17:56:50 +0200 Subject: [PATCH] =?UTF-8?q?Expression=20du=20th=C3=A9or=C3=A8me=20pour=20l?= =?UTF-8?q?a=20seconde=20preuve.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- RapportStage.tex | 96 +++++++++++++----------------------------------- 1 file changed, 26 insertions(+), 70 deletions(-) diff --git a/RapportStage.tex b/RapportStage.tex index d926ad5..ea8584b 100644 --- a/RapportStage.tex +++ b/RapportStage.tex @@ -810,78 +810,34 @@ \section{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 + Nous allons démontrer une version un peu plus puissante de ce théorème, ce qui simplifiera l'induction que nous ferrons. - \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*} + Tout d'abord, nous allons définir quelques notations locales à cette preuve. + + 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$. + + 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. + + 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'}})\] + + 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})\] + \marginpar{Un exemple d'utilisation de ces notations est-il nécessaire ?} + + Le théorème, plus général que nous allons montrer est le suivant: + + \begin{theorem} + Pour $\varepsilon$, $\gamma$ des \eng{mappings} de même domaine\\ + 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 e'\quad h\bracket{\varepsilon}\rightarrow^* h\bracket{e'}\right)\implies\left(\exists f'\quad h\bracket{\gamma}\rightarrow^* h\bracket{f'}\right)\] + \end{theorem} + - 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). - \marginpar{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($h^\prime_1$,...,$h^\prime_{k^\prime}$)}$} - - Alors, \fj{D}=\fj{C} et $k'=k$ car $\fj{new D(...$\null_{k^\prime}$)} \rightarrow^* \fj{new C(...$\null_k$)}$ - - Or, pour chaque $i$, $h'_i\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 à chaque $h'_i$, on obtient que \[h'_i\bracket{f} \rightarrow^*\hbar_i\bracket{\overline{f'_i}}\]. - - Donc \[h\bracket{f} \rightarrow^* \fj{new C($\hbar_i\bracket{\overline{f^\prime_1}}$,...,$\hbar_i\bracket{\overline{f^\prime_k}}$)} = \hbar\bracket{\overline{f''}}\] - - \[\overline{f''} = \overline{f'_1} \| \dots \| \overline{f'_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. - - \marginpar{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}