Début de la nouvelle (j'espère bonne) preuve.
This commit is contained in:
parent
7c741561fd
commit
74b4b47860
GPG Key ID:
7054D5D6A90F084F
184
RapportStage.tex
184
RapportStage.tex
@ -839,67 +839,137 @@
|
||||
|
||||
C'est sous cette seconde forme que nous allons prouver le théorème (elle est plus \enquote{bas niveau}).
|
||||
|
||||
Procédons par récurrence sur la longueur de la réduction $h\bracket{\varepsilon} \rightarrow^* \hbar\bracket{\overline{e'}}$
|
||||
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$.
|
||||
|
||||
|
||||
\paragraph{Initialisation}
|
||||
On essaie alors de montrer le résultat par induction sur $\hbar$.
|
||||
|
||||
On suppose que $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$.
|
||||
|
||||
\subparagraph{Cas $\hbar = \hole$}
|
||||
Alors
|
||||
\[h\bracket{\gamma} = \hbar\bracket{\overline{f'}}\quad\text{avec}\quad \overline{f'} = \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''}}}\]
|
||||
|
||||
Et donc, en notant $\overline{f'}$ la concaténation des $\overline{\overline{f''}}$, on obtient que
|
||||
\[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
|
||||
|
||||
\paragraph{Hérédité}
|
||||
|
||||
Notre hypothèse de récurrence, notée \textsc{(HR)} est la suivante:
|
||||
\[\forall h \quad \varepsilon \prec \gamma \implies h\bracket{\varepsilon} \prec^{<n} h\bracket{\gamma}\]
|
||||
|
||||
Nous allons continuer en faisant une induction sur $h$.
|
||||
|
||||
\subparagraph{Cas $h = \fj{$h_0$.meth($\overline{h_1}$)}$}
|
||||
|
||||
\underline{Cas 1} si la première réduction ne se fait pas sur la racine de $h$.
|
||||
|
||||
Alors, dans l'un des $h_x\bracket{\varepsilon}$ on a que
|
||||
\[h_x\bracket{\varepsilon} \rightarrow e^0\]
|
||||
|
||||
Il y a alors trois possibilités:
|
||||
|
||||
\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 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.
|
||||
\[\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:
|
||||
|
||||
\[\varepsilon' = \left[ \begin{array}{ccc}
|
||||
\fj{x} &\mapsto& \varepsilon(\fj{x})\\
|
||||
\fj{y} &\mapsto& e^{\fj{x}}\\
|
||||
v &\mapsto& \varepsilon(v)
|
||||
\end{array} \right]
|
||||
\quad
|
||||
\gamma' = \left[ \begin{array}{ccc}
|
||||
\fj{x} &\mapsto& \gamma(\fj{x})\\
|
||||
\fj{y} &\mapsto& \gamma(\fj{x})\\
|
||||
v &\mapsto& \gamma(v)
|
||||
\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'}}\]
|
||||
|
||||
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.
|
||||
|
||||
\begin{tikzpicture}
|
||||
\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
|
||||
|
||||
\node (e2) at (0,0) {$e^{\fj{x}}$};
|
||||
|
||||
\node (e3) at (0,-1) {$\hbar\bracket{\overline{e'}}$};
|
||||
|
||||
\node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$};
|
||||
|
||||
\draw[->] (e1) -- (e2);
|
||||
\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
|
||||
|
||||
\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
|
||||
\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
|
||||
\end{tikzpicture}
|
||||
|
||||
On peut alors appliquer que $\varepsilon \prec \gamma$.
|
||||
|
||||
Nous avons toutes les conditions réunies qui nous permettent d'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 deux 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}$ et le second est un appel à méthode de la forme $\fj{x.meth($\overline{h'}$)}$.
|
||||
\marginpar{Faut-il ajouter le cas du Cast ?}
|
||||
|
||||
Dans ces deux cas, nous avons nécessairement $\varepsilon(\fj{x}) = \fj{new C($\overline{e^\varepsilon}$)}$, et donc aussi $\gamma(\fj{x}) = \fj{new C($\overline{e^\gamma}$)}$ avec $\overline{e^\varepsilon} \prec \overline{e^\gamma}$, puisque $\varepsilon \prec \gamma$.
|
||||
|
||||
Dans le cas de $\fj{x.field}$, on choisit un nouveau nom de variable inutilisé $\fj{y}$, et nous créons une nouvelle fois $\varepsilon'$ et $\gamma'$ ainsi.
|
||||
|
||||
\paragraph{Si la réduction est de taille $0$}
|
||||
Alors $h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}$.
|
||||
|
||||
On peut alors prouver le lemme suivant par induction sur $h$:
|
||||
\[\forall h,\hbar,\varepsilon,\gamma,\overline{e'}\qquad \left|\begin{array}{ll}\varepsilon \prec \gamma \\h\bracket{\varepsilon} = \hbar\bracket{\overline{e'}}\end{array}\right. \implies \exists \overline{f'}\quad h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
|
||||
|
||||
\subparagraph{$h$ = \fj{x} (variable)}
|
||||
Alors \[h\bracket{\varepsilon} = \varepsilon(\fj{x}) \prec \gamma(\fj{x}) = h\bracket{\gamma}\]
|
||||
|
||||
\subparagraph{$h$ = \fj{new C($h'_1$,...,$h'_k$)}}
|
||||
Dans le cas où $\hbar = \hole$, alors on a $\overline{e'} = (e_0)$.
|
||||
Alors, en posant $\overline{f'} = (h\bracket{\gamma})$, on obtient que $\hbar\bracket{\overline{f'}} = h\bracket{\gamma}$, d'où le résultat.
|
||||
\[\varepsilon' = \left[ \begin{array}{ccc}
|
||||
\fj{x} &\mapsto& \varepsilon(\fj{x})\\
|
||||
\fj{y} &\mapsto& e^\varepsilon_k\\
|
||||
v &\mapsto& \varepsilon(v)
|
||||
\end{array} \right]
|
||||
\quad
|
||||
\gamma' = \left[ \begin{array}{ccc}
|
||||
\fj{x} &\mapsto& \gamma(\fj{x})\\
|
||||
\fj{y} &\mapsto& e^\gamma_k\\
|
||||
v &\mapsto& \gamma(v)
|
||||
\end{array} \right]\]
|
||||
|
||||
Sinon, c'est que $\hbar = \fj{new C($\hbar'_1$,...,$\hbar'_2$)}$.
|
||||
|
||||
Or, par induction, nous avons que il existe $\overline{f_1}$, ..., $\overline{f_k}$ tels que pour tout $i$, on aie $h'_i\bracket{\gamma} \rightarrow^* \hbar'_i\bracket{\overline{f_i}}$
|
||||
|
||||
Alors, avec
|
||||
\[\overline{f'} = \overline{f_1} \| \cdots \| \overline{f_k}\]
|
||||
|
||||
On obtient bien, par congruence de la relation de réduction : \[h\bracket{\gamma} \rightarrow^* \hbar\bracket{\overline{f'}}\]
|
||||
|
||||
\subparagraph{$h$ = Autre chose}
|
||||
Alors, c'est nécessairement que $\hbar = \hole$, à cause de la première égalité.
|
||||
|
||||
On peut alors faire la même preuve que dans le cas précédent.
|
||||
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'}}\]
|
||||
où $h'$ est obtenu en remplaçant l'occurrence de $\fj{x.field}$ susnommée par $\fj{y}$.
|
||||
|
||||
|
||||
\underline{Le lemme est donc démontré} et on peut utiliser ce dernier pour montrer le cas d'initialisation.
|
||||
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'}}\]
|
||||
|
||||
Dans le cas de $\fj{x.meth($\overline{h'}$)}$, la procédure est presque la même.
|
||||
|
||||
Nous allons noter $\overline{v}$ les noms des paramètres de $\fj{C.meth}$. Nous noterons aussi $h_m$ le corps de cette méthode.
|
||||
|
||||
Nous allons enfin obtenir $h_m'$ en remplacant dans $h_m$ la variable $\fj{this}$ par la variable $\fj{x}$ et les appels à chaque variable $v_k$ par l'expression à variables $h'_k$.
|
||||
|
||||
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'}}\]
|
||||
|
||||
Mais en ayant aussi que
|
||||
\[h\bracket{\gamma} \rightarrow h'\bracket{\gamma}\]
|
||||
|
||||
On peut enfin appliquer l'hypothèse de récurrence de la même manière.
|
||||
|
||||
\underline{Cas 2} où la première réduction se fait sur la racine de $h$.
|
||||
|
||||
\paragraph{Récursivité}
|
||||
Si le théorème est vrai pour toute réduction de taille strictement infèrieure à $n$.
|
||||
|
||||
L'hypothèse est que \[h\bracket{\varepsilon} \rightarrow^n \hbar\bracket{\overline{e'}}\]
|
||||
|
||||
Nous allons donc traiter les cas suivant le type de la première relation de cette chaine.
|
||||
|
||||
\subparagraph{\textsc{R-Invk} sur un nœud de $h$}
|
||||
Alors, on a que
|
||||
\[h\bracket{\varepsilon} = \mathfrak{h}_0\bracket{\fj{new C($\overline{h_1\bracket{\varepsilon}}$).meth($\overline{h_2\bracket{\varepsilon}}$)}} \rightarrow \mathfrak{h}_0\bracket{h_b\bracket{\varepsilon'}} = h'\bracket{\varepsilon'} \rightarrow^{<n} \hbar\bracket{\overline{e'}}\]
|
||||
|
||||
\[\text{Avec}\quad \left\lbrace\begin{array}{ccl}
|
||||
\mathfrak{h}_0& \text{est} & \text{Une expression avec un seul trou}\\
|
||||
h_b & = & \operatorname{mbody}(\fj{C},\fj{meth})\\
|
||||
\overline{\fj{x}} & \text{sont} & \text{Les variables de \fj{C.meth}}\\
|
||||
h' & = & \mathfrak{h}_0\bracket{h_b}\\
|
||||
\varepsilon' & = & \left[\begin{array}{ccc}
|
||||
\fj{this} & \mapsto & \fj{new C($\overline{h_1\bracket{\varepsilon}}$)}\\
|
||||
\overline{\fj{x}} & \mapsto & \overline{h_2\bracket{\varepsilon}}
|
||||
\end{array}\right]
|
||||
\end{array}\right.\]
|
||||
|
||||
On note aussi \[\gamma' = \left[\begin{array}{ccc}
|
||||
\fj{this} & \mapsto & \fj{new C($\overline{h_1\bracket{\gamma}}$)}\\
|
||||
\overline{\fj{x}} & \mapsto & \overline{h_2\bracket{\gamma}}
|
||||
\end{array}\right]\]
|
||||
|
||||
Ainsi, nous avons
|
||||
\[h\bracket{\gamma} = \mathfrak{h}_0\bracket{\fj{new C($\overline{h_1\bracket{\gamma}}$).meth($\overline{h_2\bracket{\gamma}}$)}} \rightarrow \mathfrak{h}_0\bracket{h_b\bracket{\gamma'}} = h'\bracket{\gamma'}\]
|
||||
|
||||
Or, $\varepsilon' \prec \gamma'$, puisque $\varepsilon \prec \gamma$,
|
||||
\end{document}
|
||||
|
||||
@ -34,7 +34,7 @@
|
||||
|
||||
\usepackage{csquotes}
|
||||
\usepackage[lighttt]{lmodern}
|
||||
\usetikzlibrary{shapes.geometric}
|
||||
\usetikzlibrary{shapes.geometric,positioning}
|
||||
|
||||
% Macros caractères globales
|
||||
\newcommand{\pgrph}{\P}
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user