mirror of
https://github.com/dhil/phd-dissertation
synced 2026-03-13 02:58:26 +00:00
Update reductions
This commit is contained in:
@@ -425,13 +425,16 @@
|
|||||||
\newcommand{\Cupto}{\keyw{cupto}}
|
\newcommand{\Cupto}{\keyw{cupto}}
|
||||||
\newcommand{\Callcc}{\keyw{callcc}}
|
\newcommand{\Callcc}{\keyw{callcc}}
|
||||||
\newcommand{\Throw}{\keyw{throw}}
|
\newcommand{\Throw}{\keyw{throw}}
|
||||||
\newcommand{\Continue}{\keyw{continue}}
|
\newcommand{\Continue}{\keyw{resume}}
|
||||||
\newcommand{\Catch}{\keyw{catch}}
|
\newcommand{\Catch}{\keyw{catch}}
|
||||||
\newcommand{\Catchcont}{\keyw{catchcont}}
|
\newcommand{\Catchcont}{\keyw{catchcont}}
|
||||||
\newcommand{\Control}{\keyw{control}}
|
\newcommand{\Control}{\keyw{control}}
|
||||||
\newcommand{\Prompt}{\keyw{prompt}}
|
\newcommand{\Prompt}{\#}
|
||||||
\newcommand{\Escape}{\keyw{escape}}
|
\newcommand{\Escape}{\keyw{escape}}
|
||||||
\newcommand{\shift}{\ensuremath{\mathcal{S}}}
|
\newcommand{\shift}{\ensuremath{\mathcal{S}}}
|
||||||
\newcommand{\reset}[1]{\ensuremath{\langle #1 \rangle}}
|
\newcommand{\reset}[1]{\ensuremath{\langle #1 \rangle}}
|
||||||
|
\newcommand{\fcontrol}{\keyw{fcontrol}}
|
||||||
|
\newcommand{\fprompt}{\%}
|
||||||
|
\newcommand{\splitter}{\keyw{splitter}}
|
||||||
|
|
||||||
\newcommand{\cont}{\keyw{cont}}
|
\newcommand{\cont}{\keyw{cont}}
|
||||||
@@ -1225,7 +1225,8 @@
|
|||||||
volume = {11},
|
volume = {11},
|
||||||
number = {2},
|
number = {2},
|
||||||
pages = {125--143},
|
pages = {125--143},
|
||||||
year = {1998}
|
year = {1998},
|
||||||
|
note = {Reprint of {UNIVAC} Systems Programming Research report (August 1965)}
|
||||||
}
|
}
|
||||||
|
|
||||||
@article{DanvyM08,
|
@article{DanvyM08,
|
||||||
|
|||||||
53
thesis.tex
53
thesis.tex
@@ -671,6 +671,8 @@ callcc, J, catchcont, etc.
|
|||||||
\hline
|
\hline
|
||||||
fcontrol & Delimited & Composable & \citet{Sitaram93} \\
|
fcontrol & Delimited & Composable & \citet{Sitaram93} \\
|
||||||
\hline
|
\hline
|
||||||
|
J & Undelimited & Abortive & \citet{Landin98}\\
|
||||||
|
\hline
|
||||||
shift/reset & Delimited & Composable & \citet{DanvyF90}\\
|
shift/reset & Delimited & Composable & \citet{DanvyF90}\\
|
||||||
\hline
|
\hline
|
||||||
spawn & Delimited & Composable & \citet{HiebDA94}\\
|
spawn & Delimited & Composable & \citet{HiebDA94}\\
|
||||||
@@ -695,7 +697,7 @@ callcc, J, catchcont, etc.
|
|||||||
%
|
%
|
||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
\slab{Capture} & \EC[\Callcc~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
|
\slab{Capture} & \EC[\Callcc~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
|
||||||
\slab{Invoke} & \EC[\Throw~\cont_{\EC'}~V] &\reducesto& \EC'[V]
|
\slab{Resume} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC'[V]
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
%
|
%
|
||||||
|
|
||||||
@@ -704,7 +706,8 @@ call-with-composable-continuation (MzScheme 360, November 2006).
|
|||||||
%
|
%
|
||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
\slab{Capture} & \EC[\Callcc^\ast~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
|
\slab{Capture} & \EC[\Callcc^\ast~k.M] &\reducesto& \EC[M[\cont_{\EC}/k]]\\
|
||||||
\slab{Invoke} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC[\EC'[V]]
|
% \slab{Resume} & \EC[\Continue~\cont_{\EC'}~V] &\reducesto& \EC[\EC'[V]]
|
||||||
|
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
|
|
||||||
\subsection{Delimited operators}
|
\subsection{Delimited operators}
|
||||||
@@ -729,8 +732,19 @@ undelimited control~\cite{Filinski94}
|
|||||||
%\paragraph{Felleisen's F and prompt}
|
%\paragraph{Felleisen's F and prompt}
|
||||||
|
|
||||||
\paragraph{Control/prompt}
|
\paragraph{Control/prompt}
|
||||||
|
%
|
||||||
|
\begin{reductions}
|
||||||
|
\slab{Value} &
|
||||||
|
\Prompt~V &\reducesto& V\\
|
||||||
|
\slab{Capture} &
|
||||||
|
\Prompt~\EC[\Control~k.M] &\reducesto& \Prompt~M[\cont_{\EC}/k], \text{ where $\EC$ contains no \Prompt}\\
|
||||||
|
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
|
||||||
|
\end{reductions}
|
||||||
|
|
||||||
|
|
||||||
\paragraph{Cupto}
|
\paragraph{Cupto}
|
||||||
|
%
|
||||||
|
|
||||||
|
|
||||||
\paragraph{Effect handlers}
|
\paragraph{Effect handlers}
|
||||||
%
|
%
|
||||||
@@ -738,41 +752,50 @@ undelimited control~\cite{Filinski94}
|
|||||||
\slab{Value} & \Handle\; V \;\With\;H &\reducesto& M[V/x], \text{ where } \{\Return\;x \mapsto M\} \in H\\
|
\slab{Value} & \Handle\; V \;\With\;H &\reducesto& M[V/x], \text{ where } \{\Return\;x \mapsto M\} \in H\\
|
||||||
\slab{Capture} & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\cont_{\Record{\EC;H}}/k],\\
|
\slab{Capture} & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\cont_{\Record{\EC;H}}/k],\\
|
||||||
\multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
|
\multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
|
||||||
\slab{Invoke} & \Continue~\cont_{\Record{\EC;H}}~V &\reducesto& \Handle\;\EC[V]\;\With\;H\\
|
\slab{Resume} & \Continue~\cont_{\Record{\EC;H}}~V &\reducesto& \Handle\;\EC[V]\;\With\;H\\
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
%
|
%
|
||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
\slab{Capture} & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\cont_{\EC}/k],\\
|
\slab{Capture} & \Handle\;\EC[\Do\;\ell~V] \;\With\; H &\reducesto& M[V/p,\cont_{\EC}/k],\\
|
||||||
\multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
|
\multicolumn{4}{l}{\hfill\bl\text{where $\ell$ is not handled in $\EC$}\\\text{and }\{\ell~p~k \mapsto M\} \in H\el}\\
|
||||||
\slab{Invoke} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]\\
|
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]\\
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
%
|
%
|
||||||
|
|
||||||
\paragraph{Sitaram's fcontrol}
|
\paragraph{Sitaram's fcontrol}
|
||||||
|
%
|
||||||
|
\begin{reductions}
|
||||||
|
\slab{Value} &
|
||||||
|
\fprompt~V.W &\reducesto& W\\
|
||||||
|
\slab{Capture} &
|
||||||
|
\fprompt~V.\EC[\fcontrol~W] &\reducesto& V~W~\cont_{\EC}, \text{ where $\EC$ contains no \fprompt}\\
|
||||||
|
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
|
||||||
|
\end{reductions}
|
||||||
|
%
|
||||||
|
|
||||||
\paragraph{Longley's catch-with-continue}
|
\paragraph{Longley's catch-with-continue}
|
||||||
%
|
%
|
||||||
\begin{mathpar}
|
\begin{mathpar}
|
||||||
\inferrule*
|
\inferrule*
|
||||||
{\typ{\Gamma, f : A \to B}{M : C \times D} \\ \Ground\;C}
|
{\typ{\Gamma, f : A \to B}{M : C \times D} \\ \Ground\;C}
|
||||||
{\typ{\Gamma}{\Catchcont\;f.~M : C \times ((A \to B) \to D) + (A \times (B \to (A \to B) \to C \times D))}}
|
{\typ{\Gamma}{\Catchcont\;f.M : C \times ((A \to B) \to D) + (A \times (B \to (A \to B) \to C \times D))}}
|
||||||
\end{mathpar}
|
\end{mathpar}
|
||||||
%
|
%
|
||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
\slab{Value} &
|
\slab{Value} &
|
||||||
\Catchcont \; f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
|
\Catchcont \; f . \Record{V;W} &\reducesto& \Inl\; \Record{V;\lambda\,f. W}\\
|
||||||
\slab{Capture} &
|
\slab{Capture} &
|
||||||
\Catchcont \; f .~\EC[\,f\,V] &\reducesto& \Inr\; \Record{V; \cont_{\Record{\EC;f}}}\\
|
\Catchcont \; f .\EC[\,f\,V] &\reducesto& \Inr\; \Record{V; \cont_{\Record{\EC;\,f}}}\\
|
||||||
\slab{Invoke} & \Continue~\cont_{\Record{\EC;\,f}}~x &\reducesto& \lambda\, f.\EC[x]
|
\slab{Resume} & \Continue~\cont_{\Record{\EC;\,f}}~V &\reducesto& \lambda f.\EC[V]
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
|
|
||||||
\paragraph{Shift/reset}
|
\paragraph{Shift/reset}
|
||||||
%
|
%
|
||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
\slab{Value} & \reset{V} &\reducesto& V\\
|
\slab{Value} & \reset{V} &\reducesto& V\\
|
||||||
\slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\reset{\EC}}/k]}\\
|
\slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\reset{\EC}}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
|
||||||
% \slab{Invoke} & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\
|
% \slab{Resume} & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\
|
||||||
\slab{Invoke} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\
|
\slab{Resume} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
%
|
%
|
||||||
|
|
||||||
@@ -780,11 +803,19 @@ undelimited control~\cite{Filinski94}
|
|||||||
\begin{reductions}
|
\begin{reductions}
|
||||||
% \slab{Value} & \reset{V} &\reducesto& V\\
|
% \slab{Value} & \reset{V} &\reducesto& V\\
|
||||||
\slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& M[\cont_{\reset{\EC}}/k]\\
|
\slab{Capture} & \reset{\EC[\shift\,k.M]} &\reducesto& M[\cont_{\reset{\EC}}/k]\\
|
||||||
% \slab{Invoke} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\
|
% \slab{Resume} & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\
|
||||||
\end{reductions}
|
\end{reductions}
|
||||||
%
|
%
|
||||||
|
|
||||||
\paragraph{Splitter}
|
\paragraph{Splitter}
|
||||||
|
\begin{reductions}
|
||||||
|
\slab{Value} &
|
||||||
|
\splitter~f.V &\reducesto& V\\
|
||||||
|
\slab{Capture} &
|
||||||
|
\splitter~f.\EC[\fcontrol~V]~f &\reducesto& f~V~\cont_{\EC}, \text{ where $\EC$ contains no \fprompt}\\
|
||||||
|
\slab{Resume} & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
|
||||||
|
\end{reductions}
|
||||||
|
|
||||||
|
|
||||||
\paragraph{Spawn/controller}
|
\paragraph{Spawn/controller}
|
||||||
|
|
||||||
|
|||||||
Reference in New Issue
Block a user