Preuve du second théorème.
This commit is contained in:
parent
74b4b47860
commit
5c830b50d7
GPG Key ID:
7054D5D6A90F084F
180
RapportStage.tex
180
RapportStage.tex
@ -866,110 +866,100 @@
|
||||
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$.
|
||||
Nous aurons ensuite trois cas, suivant l'endroit où s'effectue la première étape de la réduction.
|
||||
|
||||
\subparagraph{Cas $h = \fj{$h_0$.meth($\overline{h_1}$)}$}
|
||||
\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]\]
|
||||
|
||||
\underline{Cas 1} si la première réduction ne se fait pas sur la racine de $h$.
|
||||
Ainsi, la réduction considérée s'exprime comme
|
||||
\[h\bracket{\varepsilon} \rightarrow h'\bracket{\varepsilon'} \rightarrow^{n-1} \hbar\bracket{\overline{e'}}\]
|
||||
|
||||
Alors, dans l'un des $h_x\bracket{\varepsilon}$ on a que
|
||||
\[h_x\bracket{\varepsilon} \rightarrow e^0\]
|
||||
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})$
|
||||
|
||||
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'}}\]
|
||||
Cela est vrai par propriété de confluence sur l'opération de réduction.
|
||||
\begin{center}
|
||||
\begin{tikzpicture}
|
||||
\node (e1) at (1,1) {$\varepsilon(\fj{x})$};
|
||||
|
||||
\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:
|
||||
\node (e2) at (0,0) {$e^{\fj{x}}$};
|
||||
|
||||
\[\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'}}\]
|
||||
\node (e3) at (0,-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})$
|
||||
\node (e4) at (1,-2) {$\hbar\bracket{\overline{e''}}$};
|
||||
|
||||
Cela est vrai par propriété de confluence sur l'opération de réduction.
|
||||
\draw[->] (e1) -- (e2);
|
||||
\draw[->] (e2) to node[very near end, above right] {$*$} (e3);
|
||||
|
||||
\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.
|
||||
|
||||
\[\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]\]
|
||||
|
||||
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}$.
|
||||
|
||||
|
||||
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$.
|
||||
\draw[->,dashed] (e1) to node[very near end, above right] {$*$} (e4);
|
||||
\draw[->,dashed] (e3) to node[very near end, above right] {$*$} (e4);
|
||||
\end{tikzpicture}
|
||||
\end{center}
|
||||
|
||||
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 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}$.
|
||||
|
||||
Dans ces trois 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.
|
||||
|
||||
\[\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]\]
|
||||
|
||||
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}$.
|
||||
|
||||
|
||||
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.
|
||||
|
||||
Enfin, dans le dernier cas $\fj{(D)x}$, puisque la réduction s'est bien effectuée, c'est que $\fj{C} \subclass \fj{D}$. On peut donc simplement remplacer dans $h$ le cast par la variable $\fj{x}$ seule.
|
||||
|
||||
\end{document}
|
||||
|
||||
@ -111,9 +111,8 @@
|
||||
%%% Subparaghaphs box
|
||||
\newtcbox{\subparaghaphbox}{nobeforeafter,tcbox raise base, arc=9pt, outer arc=9pt, boxsep=2pt,left=2pt,right=2pt,top=2pt,bottom=2pt,boxrule=1pt,colback=white!85!orange}
|
||||
\newcommand{\subparaghaphboxedcontent}[1]{\subparaghaphbox{#1}\newline}
|
||||
\titleformat{\subparagraph}[runin]
|
||||
{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
|
||||
|
||||
%\titleclass{\mathcases}{straight}[\subparagraph]
|
||||
\titleformat{\subparagraph}[runin]{\normalfont\normalsize\bfseries}{}{0em}{\subparaghaphboxedcontent}
|
||||
\titlespacing*{\subparagraph}{0pt}{3.25ex plus 1ex minus .2ex}{0.5em}
|
||||
|
||||
%%% Blocs colorés pour le code FeatherweightJava
|
||||
|
||||
Loading…
x
Reference in New Issue
Block a user