diff --git a/thesis.tex b/thesis.tex index e8d44b3..ac32d8d 100644 --- a/thesis.tex +++ b/thesis.tex @@ -14560,35 +14560,26 @@ $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}$. - - \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} + $M \reducesto N$ is an application of $\semlab{Op^\dagger}$, which + we will show. + + 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\}$. + % + 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{-}$}\\ &\bl @@ -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]$. - - \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} + $(\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} \end{proof} % \begin{proof} % By case analysis on $\reducesto$ using Lemma~\ref{lem:sdtrans-subst}