dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

WIP

Browse Source
This commit is contained in:
Daniel Hillerström
2021-05-27 00:35:40 +01:00
parent a57ac855c2
commit e84b4605c2
1 changed files with 123 additions and 58 deletions
Download Patch File Download Diff File Expand all files Collapse all files

177
thesis.tex
View File

@@ -14530,77 +14530,34 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
\end{theorem} \end{theorem}
% %
\begin{proof} \begin{proof}
By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst} By case analysis on $\reducesto$ and induction on $\approxa$ using
and Lemma~\ref{lem:sdtrans-admin}. We show only the interesting case Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}.
$\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to %
approximate the body of the resumption up to administrative
reduction.\smallskip
\noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto \noindent\textbf{Case} $\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H \reducesto
N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ where
$\ell \notin \BL(\EC)$ and $\ell \notin \BL(\EC)$ and
$H^\ell = \{\OpCase{\ell}{p}{r} \mapsto N_\ell\}$. \smallskip\\ $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
% %
Pick $M' =
\sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Clearly
$M' \approxa \sdtrans{M}$. We compute $N'$ via reduction as follows.
\begin{derivation} \begin{derivation}
& \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\ & \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}\\
=& \reason{definition of $\sdtrans{-}$}\\ =\reducesto^\ast& \reason{\semlab{Op} ($\ell \notin \BL(\sdtrans{\EC})$), $2\times$\semlab{Let},\semlab{Split},\semlab{App}, Lemma~\ref{lem:sdtrans-subst}}\\
&\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. &\sdtrans{N_\ell[\lambda x.
\bl \bl
\Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\ \Let\;z \revto (\lambda y.\Handle\;\EC[\Return\;y]\;\With\;H)~x\;\In\\
\Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]} \Let\;\Record{f;g} = z\;\In\;f\,\Unit/r,V/p]}
\el \el\\
\end{derivation} \end{derivation}
% %
We take the above computation term to be our $N'$. If Take the final term to be $N'$. If the resumption
$r \notin \FV(N_\ell)$ then the two terms $N'$ and $r \notin \FV(N_\ell)$ then the two terms $N'$ and
$\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the $\sdtrans{N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]}$ are the
identical, and thus by reflexivity of the $\approxa$-relation it identical, and thus the result follows immediate by reflexivity of
follows that the $\approxa$-relation. Otherwise $N'$ approximates
$N' \approxa \sdtrans{N_\ell[V/p,\lambda
y.\EC[\Return\;y]/r]}$. Otherwise $N'$ approximates
$N_\ell[V/p,\lambda y.\EC[\Return\;y]/r]$ at least up to a use of $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 $r$. We need to show that the approximation remains faithful during
any application of $r$. Specifically, we proceed to show that for any application of $r$. Specifically, we proceed to show that for
@@ -14629,7 +14586,115 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$.
Defintion~\ref{def:approx-admin} that Defintion~\ref{def:approx-admin} that
$\EC'[\sdtrans{\EC}[\Return\;W]] \approxa $\EC'[\sdtrans{\EC}[\Return\;W]] \approxa
\sdtrans{\EC}[\Return\;W]$. \sdtrans{\EC}[\Return\;W]$.
\item Inductive step: Assume $M' \reducesto M''$ and
$M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Take $N' = M''$ then by the induction hypothesis $M' \reducesto N'$
\item Inductive step: Assume $admin(\EC)$ and
$M'' \approxa \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$.
\end{enumerate}
\end{proof} \end{proof}
% \begin{proof}
% By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}
% and Lemma~\ref{lem:sdtrans-admin}. We show only the interesting case
% $\semlab{Op^\dagger}$, which uses Lemma~\ref{lem:sdtrans-admin} to
% approximate the body of the resumption up to administrative
% reduction.\smallskip
% \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\\
% %
% Pick $M' =
% \sdtrans{\ShallowHandle\;\EC[\Do\;\ell~V]\;\With\;H}$. Clearly
% $M' \approxa \sdtrans{M}$. We compute $N'$ via reduction as follows.
% \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}
% %
% We take the above computation term to be our $N'$. If
% $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 by reflexivity of the $\approxa$-relation it
% follows that
% $N' \approxa \sdtrans{N_\ell[V/p,\lambda
% y.\EC[\Return\;y]/r]}$. 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]$.
% \end{proof}
\section{Parameterised handlers as ordinary deep handlers} \section{Parameterised handlers as ordinary deep handlers}
\label{sec:param-desugaring} \label{sec:param-desugaring}