dhil
/
phd-dissertation
mirror of https://github.com/dhil/phd-dissertation
1
0
Fork 0
Code Issues Releases Wiki Activity
Browse Source

Theorem 8.9

master
Daniel Hillerström 5 years ago
parent
9fa5ebe6eb
commit
fe6444ff3d
1 changed files with 157 additions and 77 deletions
Whitespace
Show all changes Ignore whitespace when comparing lines Ignore changes in amount of whitespace Ignore changes in whitespace at EOL
Split View
Diff Options
Show Stats Download Patch File Download Diff File
  1. 226
      thesis.tex

226
thesis.tex
View File

@ -14560,34 +14560,25 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
\end{theorem}
%
\begin{proof}
By case analysis on $\reducesto$ and induction on $\approxa$ using
Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
% By case analysis on $\reducesto$ and induction on $\approxa$ using
% Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
%
By induction on $M' \approxa \sdtrans{M}$ and side induction on
$M \reducesto N$.
$M \reducesto N$ using Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
%
The interesting case is reflexivity of $\approxa$ where
$M \reducesto N$ is an application of $\semlab{Op^\dagger}$.
$M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which
we will show.
\noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
$\ell \notin \BL(\EC)$ and
$H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
There are three subcases to consider.
\begin{enumerate}
\item Base step:
$M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. We
can compute $N'$ by direct calculation starting from $M'$ yielding
In the reflexivity case we have $M' \approxa \sdtrans{M}$, where
$M = \ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H$ and
$N = N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ such that
$M \reducesto N$ where $\ell \notin \BL(\EC)$ and
$H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$.
%
% \begin{derivation}
% & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
% =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
% &\sdtrans{N_\ell[\lambda x.
% \bl
% \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
% \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
% \el\\
% \end{derivation}
Hence by reflexivity of $\approxa$ we have
$M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Now we
can compute $N'$ by direct calculation starting from $M'$ yielding
\begin{derivation}
& \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
=& \reason{definition of $\sdtrans{-}$}\\
@ -14596,23 +14587,6 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
\Let\;\Record{f;g} = z\;\In\;g\,\Unit
\el\\
\reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
% &\bl
% \Let\;z \revto
% (\bl
% \Let\;r \revto \lambda x.\Let\;z \revto r~x\;\In\;\Let\;\Record{f;g} = z\;\In\;f\,\Unit\;\In\\
% \Return\;\Record{
% \bl
% \lambda\Unit.\Let\;x \revto \Do\;\ell~p\;\In\;r~x;\\
% \lambda\Unit.\sdtrans{N_\ell}})[
% \bl
% \sdtrans{V}/p,\\
% \lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H}/r]
% \el
% \el
% \el\\
% \In\;\Let\;\Record{f;g} = z\;\In\;g\,\Unit
% \el\\
% \reducesto^+& \reason{\semlab{Let}, \semlab{Let}}\\
&\bl
\Let\;\Record{f;g} = \Record{
\bl
@ -14642,55 +14616,161 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
$r \notin \FV(N_\ell)$ then the two terms $N'$ and
$\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
identical, and thus the result follows immediate by reflexivity of
the $\approxa$-relation. Otherwise $N'$ approximates
$N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
$r$. We need to show that the approximation remains faithful during
any application of $r$. Specifically, we proceed to show that for
any value $W \in \ValCat$
the $\approxa$-relation. Otherwise the proof reduces to showing that
the larger resumption term simulates the smaller resumption term,
i.e (note we lift the $\approxa$-relation to value terms).
%
\[
(\bl
\lambda x.\Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
\Let\;\Record{f;g} = z \;\In\;f\,\Unit)~W \approxa (\lambda y.\sdtrans{\EC}[\Return\;y])~W.
\Let\;\Record{f;g} = z \;\In\;f\,\Unit) \approxa (\lambda y.\sdtrans{\EC}[\Return\;y]).
\el
\]
%
The right hand side reduces to $\sdtrans{\EC}[\Return\;W]$. Two
applications of \semlab{App} on the left hand side yield the term
We use the congruence rules to apply a single $\semlab{App}$ on the
left hand side to obtain
%
\[
\Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;W]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
(\bl
\lambda x.\Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;x]\;\With\;\sdtrans{H}\;\In\\
\Let\;\Record{f;g} = z \;\In\;f\,\Unit) \approxa (\lambda y.\sdtrans{\EC}[\Return\;y]).
\el
\]
%
Define
Now the trick is to define the following context
%
$\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit$
\[
\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
\]
%
such that $\EC'$ is an administrative evaluation context by
Lemma~\ref{lem:sdtrans-admin}. Then it follows by
The context $\EC'$ is an administrative evaluation context by
Lemma~\ref{lem:sdtrans-admin}. Now it follows by
Defintion~\ref{def:approx-admin} that
$\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
\sdtrans{\EC}[\Return\;W]$.
$(\lambda x.\EC'[\sdtrans{\EC}[\Return\;x]]) \approxa
(\lambda y.\sdtrans{\EC}[\Return\;y])$.
%
% \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
% N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
% $\ell \notin \BL(\EC)$ and
% $H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\
% There are three subcases to consider.
% \begin{enumerate}
% \item Base step:
% $M' = \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. We
% can compute $N'$ by direct calculation starting from $M'$ yielding
% %
% % \begin{derivation}
% % & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
% % =\reducesto^+& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
% % &\sdtrans{N_\ell[\lambda x.
% % \bl
% % \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
% % \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
% % \el\\
% % \end{derivation}
% \begin{derivation}
% & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
% =& \reason{definition of $\sdtrans{-}$}\\
% &\bl
% \Let\;z \revto \Handle\;\sdtrans{\EC}[\Do\;\ell~\sdtrans{V}]\;\With\;\sdtrans{H}\;\In\\
% \Let\;\Record{f;g} = z\;\In\;g\,\Unit
% \el\\
% \reducesto^+& \reason{\semlab{Op} using assumption $\ell \notin \BL(\sdtrans{\EC})$, \semlab{Let}, \semlab{Let}}\\
% % &\bl
% % \Let\;z \revto
% % (\bl
% % \Let\;r \revto \lambda x.\Let\;z \revto r~x\;\In\;\Let\;\Record{f;g} = z\;\In\;f\,\Unit\;\In\\
% % \Return\;\Record{
% % \bl
% % \lambda\Unit.\Let\;x \revto \Do\;\ell~p\;\In\;r~x;\\
% % \lambda\Unit.\sdtrans{N_\ell}})[
% % \bl
% % \sdtrans{V}/p,\\
% % \lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H}/r]
% % \el
% % \el
% % \el\\
% % \In\;\Let\;\Record{f;g} = z\;\In\;g\,\Unit
% % \el\\
% % \reducesto^+& \reason{\semlab{Let}, \semlab{Let}}\\
% &\bl
% \Let\;\Record{f;g} = \Record{
% \bl
% \lambda\Unit.\Let\;x \revto \Do\;\ell~\sdtrans{V}\;\In\;r~x;\\
% \lambda\Unit.\sdtrans{N_\ell}}[\lambda x.
% \bl
% \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
% \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]\;\In\; g\,\Unit
% \el
% \el\\
% \el\\
% \reducesto^+ &\reason{\semlab{Split}, \semlab{App}}\\
% &\sdtrans{N_\ell}[\lambda x.
% \bl
% \Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
% \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,\sdtrans{V}/p]
% \el\\
% =& \reason{by Lemma~\ref{lem:sdtrans-subst}}\\
% &\sdtrans{N_\ell[\lambda x.
% \bl
% \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
% \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
% \el
% \end{derivation}
% %
% Take the final term to be $N'$. If the resumption
% $r \notin \FV(N_\ell)$ then the two terms $N'$ and
% $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
% identical, and thus the result follows immediate by reflexivity of
% the $\approxa$-relation. Otherwise $N'$ approximates
% $N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of
% $r$. We need to show that the approximation remains faithful during
% any application of $r$. Specifically, we proceed to show that for
% any value $W \in \ValCat$
% %
% \[
% (\bl
% \lambda x.\Let\;z \revto (\lambda y.\Handle\;\sdtrans{\EC}[\Return\;y]\;\With\;\sdtrans{H})~x\;\In\\
% \Let\;\Record{f;g} = z \;\In\;f\,\Unit)~W \approxa (\lambda y.\sdtrans{\EC}[\Return\;y])~W.
% \el
% \]
% %
% The right hand side reduces to $\sdtrans{\EC}[\Return\;W]$. Two
% applications of \semlab{App} on the left hand side yield the term
% %
% \[
% \Let\;z \revto \Handle\;\sdtrans{\EC}[\Return\;W]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit.
% \]
% %
% Define
% %
% $\EC' \defas \Let\;z \revto \Handle\; [\,]\;\With\;\sdtrans{H}\;\In\;\Let\;\Record{f;g} = z \;\In\;f\,\Unit$
% %
% such that $\EC'$ is an administrative evaluation context by
% Lemma~\ref{lem:sdtrans-admin}. Then it follows by
% Defintion~\ref{def:approx-admin} that
% $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
% \sdtrans{\EC}[\Return\;W]$.
\item Inductive step: Assume $M' \reducesto M''$ and
$M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
\[
\sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
\reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
\]
Take $N' = M''$ then by the first induction hypothesis
$M' \reducesto N'$ and by the second induction hypothesis
$N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
desired.
\item Inductive step: Assume $admin(\EC')$ and
$M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
%
By the induction the hypothesis $M' \reducesto N''$. Take
$N' = \EC'[N'']$. The result follows by an application of the
admin rule.
\item Compatibility step: We check every syntax constructor,
however, since the relation is compositional\dots
\end{enumerate}
% \item Inductive step: Assume $M' \reducesto M''$ and
% $M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Using a similar argument to above we get that
% \[
% \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}
% \reducesto^+ \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}.
% \]
% Take $N' = M''$ then by the first induction hypothesis
% $M' \reducesto N'$ and by the second induction hypothesis
% $N' \approxa \sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ as
% desired.
% \item Inductive step: Assume $admin(\EC')$ and
% $M' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
% %
% By the induction the hypothesis $M' \reducesto N''$. Take
% $N' = \EC'[N'']$. The result follows by an application of the
% admin rule.
% \item Compatibility step: We check every syntax constructor,
% however, since the relation is compositional\dots
% \end{enumerate}
\end{proof}
% \begin{proof}
% By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}

Write Preview
Loading…
Cancel
Save