From e84b4605c2685135df1e6cb0028ce4d3239a3bd2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= Date: Thu, 27 May 2021 00:35:40 +0100 Subject: [PATCH] WIP --- thesis.tex | 181 ++++++++++++++++++++++++++++++++++++----------------- 1 file changed, 123 insertions(+), 58 deletions(-) diff --git a/thesis.tex b/thesis.tex index bb24b49..7b23386 100644 --- a/thesis.tex +++ b/thesis.tex @@ -14530,77 +14530,34 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$. \end{theorem} % \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 - + By case analysis on $\reducesto$ and induction on $\approxa$ using + Lemma~\ref{lem:sdtrans-subst} and Lemma~\ref{lem:sdtrans-admin}. + % \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} + 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}\\ - =& \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}}\\ + =\reducesto^\ast& \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 + \el\\ \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 $\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 + 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 @@ -14629,7 +14586,115 @@ $N'$ such that $N' \approxa \sdtrans{N}$ and $M' \reducesto^+ N'$. 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}$. 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} +% \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} \label{sec:param-desugaring}