diff --git a/thesis.tex b/thesis.tex index 7411fe4..e6bc770 100644 --- a/thesis.tex +++ b/thesis.tex @@ -11425,8 +11425,9 @@ implementation based on stack manipulations. \begin{equations} \inv{\{\Return\;x \mapsto M\}}\env &\defas& \{\Return\;x \mapsto \inv{M}(\env \res \{x\})\} \\ -\inv{\{\ell\;x\;k \mapsto M\} \uplus H^\depth}\env +\inv{\{\OpCase{\ell}{p}{r} \mapsto M\} \uplus H^\depth}\env &\defas& \{\OpCase{\ell}{p}{r} \mapsto \inv{M}(\env \res \{p, r\}\} \uplus \inv{H^\depth}\env \\ +\inv{(q.\,H)}\env &\defas& \inv{H}(\env \res \{q\}) \end{equations} \textbf{Value terms and values} @@ -11460,59 +11461,99 @@ implementation based on stack manipulations. \label{fig:config-to-term} \end{figure} % -Figure~\ref{fig:config-to-term} defines an inverse mapping $\inv{-}$ -from configurations to computation terms via a collection of mutually -recursive functions defined on configurations, continuations, -computation terms, handler definitions, value terms, and values. +We now show that the base abstract machine is correct with respect to +the combined context-based small-step semantics of $\HCalc$, $\SCalc$, +and $\HPCalc$ via a simulation result. + +Initial states provide a canonical way to map a computation term onto +the abstract machine. % -We write $\dom(\gamma)$ for the domain of $\gamma$ and $\gamma \res -\{x_1, \dots, x_n\}$ for the restriction of environment $\gamma$ to -$\dom(\gamma) \res \{x_1, \dots, x_n\}$. +A more interesting question is how to map an arbitrary configuration +to a computation term. % -The $\inv{-}$ function enables us to classify the abstract machine -reduction rules by how they relate to the operational -semantics. +Figure~\ref{fig:config-to-term} describes such a mapping $\inv{-}$ +from configurations to terms via a collection of mutually recursive +functions defined on configurations, continuations, handler closures, +computation terms, handler definitions, value terms, and machine +values. The mapping makes use of a domain operation and a restriction +operation on environments. +% +\begin{definition} + The domain of an environment is defined recursively as follows. + % + \[ + \bl + \dom : \MEnvCat \to \VarCat\\ + \ba{@{}l@{~}c@{~}l} + \dom(\emptyset) &\defas& \emptyset\\ + \dom(\env[x \mapsto v]) &\defas& \{x\} \cup \dom(\env) + \ea + \el + \] + % + We write $\env \res \{x_1, \dots, x_n\}$ for the restriction of + environment $\env$ to $\dom(\env) \res \{x_1, \dots, x_n\}$. +\end{definition} % -The rules \mlab{Init} and \mlab{Halt} concern only initial input and -final output, neither a feature of the operational semantics. +The $\inv{-}$ function enables us to classify the abstract machine +reduction rules according to how they relate to the context-based +small-step semantics. +% +Both the rules \mlab{Let} and \mlab{Forward} are administrative in the +sense that $\inv{-}$ is invariant under either rule. +% +This leaves the $\beta$-rules \mlab{App}, \mlab{AppRec}, \mlab{TyApp}, +\mlab{Resume^\delta}, \mlab{Split}, \mlab{Case}, \mlab{PureCont}, and +\mlab{GenCont}. Each of these corresponds directly with performing a +reduction in the small-step semantics. We extend the notion of +transition to account for administrative steps. +% +\begin{definition}[Auxiliary reduction relations] + We write $\stepsto_{\textrm{a}}$ for administrative steps and + $\simeq_{\textrm{a}}$ for the symmetric closure of + $\stepsto_{\textrm{a}}^*$. We write $\stepsto_\beta$ for + $\beta$-steps and $\Stepsto$ for a sequence of steps of the form + $\stepsto_{\textrm{a}}^\ast \stepsto_\beta$. +\end{definition} % -The rules \mlab{Resume^\depth}, \mlab{Resume^\param}, \mlab{Let}, -\mlab{Handle^\depth}, \mlab{Handle^\param}, and \mlab{Forward} are -administrative in that $\inv{-}$ is invariant under them. +The following lemma describes how we can simulate each reduction in +the small-step reduction semantics by a sequence of administrative +steps followed by one $\beta$-step in the abstract machine. % -This leaves $\beta$-rules \mlab{App}, \mlab{AppRec}, \mlab{AppType}, -\mlab{Split}, \mlab{Case}, \mlab{PureCont}, \mlab{GenCont}, -\mlab{Do^\depth}, and \mlab{Do^\dagger}, each of which corresponds -directly to performing a reduction in the operational semantics. +\begin{lemma} +\label{lem:machine-simulation} +Suppose $M$ is a computation and $\conf$ is configuration such that +$\inv{\conf} = M$, then if $M \reducesto N$ there exists $\conf'$ such +that $\conf \Stepsto \conf'$ and $\inv{\conf'} = N$, or if +$M \not\reducesto$ then $\conf \not\Stepsto$. +\end{lemma} % -We write $\stepsto_a$ for administrative steps, $\stepsto_\beta$ for -$\beta$-steps, and $\Stepsto$ for a sequence of steps of the form -$\stepsto_a^* \stepsto_\beta$. - -Each reduction in the operational semantics is simulated by a sequence -of administrative steps followed by a single $\beta$-step in the -abstract machine. The $Id$ handler (Section~\ref{subsec:terms}) -implements the top-level identity continuation. +\begin{proof} +By induction on the derivation of $M \reducesto N$. +\end{proof} % -\begin{theorem}[Simulation] -\label{lem:simulation} -If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = -Id(M)$ there exists $\conf'$ such that $\conf \Stepsto \conf'$ and -$\inv{\conf'} = Id(N)$. -%% If $M \reducesto N$, then for any $\conf$ such that $\inv{\conf} = M$ -%% there exists $\conf'$ such that $\conf \Stepsto \conf'$ and -%% $\inv{\conf'} = N$. +The correspondence here is rather strong: there is a one-to-one +mapping between $\reducesto$ and the quotient relation of $\Stepsto$ +and $\simeq_{\textrm{a}}$. % The inverse of the lemma is straightforward +% as the semantics is deterministic. +% +Notice that Lemma~\ref{lem:machine-simulation} does not require that +$M$ be well-typed. This is mostly a convenience to simplify the +lemma. The lemma is used in the following theorem where it is being +applied only on well-typed terms. +% +\begin{theorem}[Simulation]\label{thm:handler-simulation} + If $\typc{}{M : A}{E}$ and $M \reducesto^+ N$ such that $N$ is + normal with respect to $E$, then + $\cek{M \mid \emptyset \mid \kappa_0} \stepsto^+ \conf$ such that + $\inv{\conf} = N$, or $M \not\reducesto$ then + $\cek{M \mid \emptyset \mid \kappa_0} \not\stepsto$. \end{theorem} % \begin{proof} -By induction on the derivation of $M \reducesto N$. +By repeated application of Lemma~\ref{lem:machine-simulation}. \end{proof} -\begin{corollary} -If $\typc{}{M : A}{E}$ and $M \reducesto^+ N \not\reducesto$, then $M -\stepsto^+ \conf$ with $\inv{\conf} = N$. -\end{corollary} - \section{Related work} The literature on abstract machines is vast and rich. I describe here the basic structure of some selected abstract machines from the @@ -11631,7 +11672,7 @@ than right-to-left evaluation order is now considered a bug (subject to some exceptions, notably short-circuiting logical and/or functions). -\paragraph{Mechanic machine derivations} +\paragraph{Mechanical machine derivations} % There are deep mathematical connections between environment-based abstract machine semantics and standard reduction semantics with @@ -11649,11 +11690,11 @@ programming language Agda. % \citet{HuttonW04} demonstrate how to calculate a correct-by-construction abstract machine from a given specification -using structural induction. Notably, their example machine supports a -basic notion of exceptions. +using structural induction. Notably, their example machine supports +basic computational effects in the form of exceptions. % -Derivations of abstract machines for languages with computational -effects were also explored by \citet{AgerDM05}. +\citet{AgerDM05} also extended their technique to derive abstract +machines from monadic-style effectful evaluators. \part{Expressiveness}