Declaration signature

thesis.bib

@@ -2005,6 +2005,20 @@
   year      = {1994}
 }
 
+# marker and callpc
+@inproceedings{MoreauQ94,
+  author    = {Luc Moreau and
+               Christian Queinnec},
+  title     = {Partial Continuations as the Difference of Continuations - {A} Duumvirate
+               of Control Operators},
+  booktitle = {{PLILP}},
+  series    = {{LNCS}},
+  volume    = {844},
+  pages     = {182--197},
+  publisher = {Springer},
+  year      = {1994}
+}
+
 # Comparison of (some) delimited control operators
 @misc{Shan04,
   author    = {Chung{-}chieh Shan},

thesis.tex

@@ -304,43 +304,45 @@
   fortunate to have been supervised by him.
   %
   Secondly, I want to extend my gratitude to John Longley, who has
-  been an excellent second supervisor and who has stimulated my
-  mathematical curiosity.
+  been an excellent second supervisor and has always shown enthusiasm
+  about my work.
   %
-  Thirdly, I want to thank my academic brother Simon Fowler. You have
+  Thirdly, I want to thank my academic brother Simon Fowler, who has
   always been a good friend and a pillar of inspiration. Regardless of
   academic triumphs and failures, we have always been able to laugh at
   it all and have our own fun.
 
   I also want to thank KC Sivaramakrishnan for taking a genuine
   interest in my research early on and for inviting me to come spend
-  some time at OCaml Labs in Cambridge, where I met Anil Madhavapeddy,
-  Stephen Dolan, and Leo White. I have learned so much from each of
-  them and I have been fortunate to enjoy productive and long-standing
-  collaboration with them. Also, thanks to Gemma Gordon, who I had the
-  pleasure of sharing an office with during one of my stints at OCaml
-  Labs.
+  some time at OCaml Labs in Cambridge. My initial visit to Cambridge
+  sparked the beginning of a long-standing and productive
+  collaboration. Also, thanks to Gemma Gordon, who I had the pleasure
+  of sharing an office with during one of my stints at OCaml Labs.
 
-  I am very grateful for the fruitful and long-standing collaboration
-  with Robert Atkey that I have been fortunate to enjoy. Robert has
-  been a continuous source of inspiration.
+  I have been fortunate to work with Robert Atkey, who has been a
+  continuous source of inspiration and interesting research ideas. Our
+  work is clearly reflected in this dissertation.
   %
-  Thanks to James McKinna for always asking intellectually
-  interesting, and at times challenging, questions. I have appreciate
-  our many conversations even though I spent days, weeks, sometimes
-  months, and in some instances years to think about answers to your
-  questions. On the topic of intellectually stimulating conversations,
-  I also want to thank Gordon Plotkin for our intriguing impromptu
-  conversations in the level 4 and 5 pantries of Informatics
-  Forum. Thanks to Brian Campbell and J. Garrett Morris for putting up
-  with the supervision meetings that I had with Sam in their shared
-  office 5.28.
+  I also want to thank my other collaborators: Andreas Rossberg, Anil
+  Madhavapeddy, Leo White, and Stephen Dolan, Jeremy Yallop.
 
-  Speaking of offices, I also want to thank my peers from my own
-  office 5.21 for stimulating my general interest in computer science
-  and mathematics beyond programming languages. Also, thanks to my CDT
-  cohort, I want to particularly emphasise my gratitude towards Amna
-  Shahab, who has been a truly valuable friend.
+  I have had the absolute pleasure of working in LFCS at the same time
+  as James McKinna. James has always taken a genuine interest in my
+  work and challenged me with intellectually stimulating questions. I
+  have appreciate our many conversations even though I spent days,
+  weeks, sometimes months, and in some instances years to come up with
+  adequate answers. I also want to thank other former and present
+  members of LFCS and other institutes within Informatics: Brian
+  Campbell, Christophe Dubach, James Cheney, J. Garrett Morris, Gordon
+  Plotkin, and Michel Steuwer.
+
+  My time as a student in Informatics Forum was an enjoyable
+  experience in large part thanks to my student peers and friends:
+  Amna Shahab, Chris Vasiladiotis, Craig McLaughlin, Dan Mills, Danel
+  Ahman, Frank Emrich, Emanuel Martinov, Floyd Chitalu, Larisa
+  Stoltzfus, Jakub Zalewski, Maria Gorinova, Marcin Szymczak, Rajkarn
+  Singh, Rudi Horn, Philip Ginsbach, Paul Piho, Stan Manilov, and
+  Vanya Yaneva-Cormack.
 
   Thanks to Ohad Kammar for being a good friend, taking a genuine
   interest in my work, making it fun to attend virtual conferences,
@@ -358,19 +360,11 @@
   dissertation whilst being employed on the UKRI Future Leaders
   Fellowship ``Effect Handler Oriented Programming'' (reference number
   MR/T043830/1).
-
-  List of people to thank
-  \begin{itemize}
-    \item Andreas Rossberg
-    \item Jeremy Yallop
-    \item Paul Piho
-    \item Larisa Stoltzfus
-  \end{itemize}
 \end{acknowledgements}
 
 %% Next we need to have the declaration.
 % \standarddeclaration
-\begin{declaration}
+\begin{declaration}[Daniel Hillerström, Edinburgh, Scotland, 2021]
   I declare that this thesis was composed by myself, that the work
   contained herein is my own except where explicitly stated otherwise
   in the text, and that this work has not been submitted for any other
@@ -4361,6 +4355,11 @@ $k$ restores the context with the prompt. The $\abort$ application
 erases the evaluation context up to this prompt, however, the body of
 the functional argument to $\abort$ reinvokes the continuation $k$
 which restores the prompt context once again.
+
+\citet{MoreauQ94} proposed a variation of splitter called
+\emph{marker}, which is also built on top of multi-prompt
+semantics. The key difference is that the control reifier strips the
+reified context of all prompts.
 % \begin{derivation}
 %   &1 + \splitter\,(\lambda p.2 + \splitter\,(\lambda p'.3 + \calldc\,\Record{p';\lambda k. k\,0 + \calldc\,\Record{p';\lambda k'. k\,(k'\,1)}}))), \emptyset\\
 %   \reducesto& \reason{\slab{AppSplitter}}\\
@@ -4437,9 +4436,44 @@ continuation. This continuation gets passed to the functional value of
 the control expression. The captured continuation contains the label
 $\ell$, and as specified by the $\slab{Resume}$ rule an invocation of
 the continuation causes this label to be reinstalled.
-% concas structured
-% alternative for using undelimited continuations, such as provided by
-% callcc, in concurrent programming
+
+The following example usage of $\Spawn$ is a slight variation on an
+example due to \citet{HiebDA94}.
+%
+\begin{derivation}
+  & 1 \cons (\Spawn\,(\lambda c. 2 \cons (c\,(\lambda k. 3 \cons k\,(k\,\nil))))), \emptyset\\
+  \reducesto& \reason{\slab{AppSpawn}}\\
+  &1 \cons (\ell : (\lambda c. 2 \cons (c\,(\lambda k. 3 \cons k\,(k\,\nil))))\,(\lambda f.f \reflect \ell)), \{\ell\}\\
+  \reducesto& \reason{$\beta$-reduction}\\
+  &1 \cons (\ell : 2 \cons ((\lambda f.f \reflect \ell)\,(\lambda k. 3 \cons k\,(k\,\nil)))), \{\ell\}\\
+\end{derivation}
+%
+\begin{derivation}
+  \reducesto& \reason{$\beta$-reduction}\\
+  &1 \cons (\ell : 2 \cons ((\lambda k. 3 \cons k\,(k\,\nil)) \reflect \ell)), \{\ell\}\\
+  \reducesto& \reason{\slab{Capture} $\EC = 2 \cons [\,]$}\\
+  & 1 \cons 3 \cons \qq{\cont_{\EC}}\,(\qq{\cont_{\EC}}\,\nil), \{\ell\}\\
+  \reducesto& \reason{\slab{Resume} $\EC$ with $\nil$}\\
+  &1 \cons 3 \cons \qq{\cont_{\EC}}\,(\ell : 2 \cons \nil), \{\ell\}\\
+  \reducesto^+& \reason{\slab{Value}}\\
+  &1 \cons 3 \cons \qq{\cont_{\EC}}\,[2], \{\ell\}\\
+  \reducesto^+& \reason{\slab{Resume} $\EC$ with $[2]$}\\
+  &1 \cons 3 \cons (\ell : 2 \cons [2]), \{\ell\}\\
+  \reducesto^+& \reason{\slab{Value}}\\
+  &1 \cons 3 \cons [2,2], \{\ell\} \reducesto^+ [1,3,2,2], \{\ell\}
+\end{derivation}
+%
+When the controller $c$ is invoked the current continuation is
+$1 \cons (\ell : 2 \cons [\,])$. The control expression reifies the
+$\ell : 2 \cons [\,]$ portion of the continuation and binds it to
+$k$. The first invocation of $k$ reinstates the reified portion and
+computes the singleton list $[2]$ which is used as argument to the
+second invocation of $k$.
+
+Both \citet{HiebD90} and \citet{HiebDA94} give several concurrent
+programming examples with spawn. They show how
+parallel-or~\cite{Plotkin77} can be codified as a macro using spawn
+(and a parallel invocation primitive \emph{pcall}).
 
 \paragraph{\citeauthor{Sitaram93}'s fcontrol} The control operator
 `fcontrol' was introduced by \citet{Sitaram93} in 1993. It is a
@@ -4817,7 +4851,7 @@ gets stuck as either $\Choose$ or $\Fail$, or both, would be
 unhandled. Thus, we have to run the computation in the context of both
 handlers. However, we have a choice to make as we can compose the
 handlers in either order. Let us first explore the composition, where
-$H_c$ is the outermost handler. Thus instantiate $H_c$ at type
+$H_c$ is the outermost handler. Thus we instantiate $H_c$ at type
 $\Option~\Bool$ and $H_f$ at type $\Bool$.
 %
 \begin{derivation}
@@ -4830,6 +4864,8 @@ $\Option~\Bool$ and $H_f$ at type $\Bool$.
   & (\Handle\;(\Handle\;\EC[\True] \;\With\;H_f)\;\With\;H_c) \concat k~\False\\
   \reducesto & \reason{$\beta$-reduction}\\
   & (\Handle\;(\Handle\; \Do\;\Choose~\Unit \;\With\; H_f)\;\With\;H_c) \concat k~\False\\
+\end{derivation}
+\begin{derivation}
   \reducesto & \reason{\slab{Capture}, $\{\OpCase{\Choose}{\Unit}{k'} \mapsto \cdots\} \in H_c$, $\EC'' = (\Handle\;[\,]\;\cdots)$}\\
   & (k'~\True \concat k'~\False) \concat k~\False, \qquad \text{where $k' = \qq{\cont_{\Record{\EC'';H_c}}}$}\\
   \reducesto& \reason{\slab{Resume} with $\True$}\\
@@ -5031,7 +5067,7 @@ first-order parameter.
 The function $\dec{odd}$ expects its environment to provide it with an
 implementation of a single operation of type $\Int \to \Bool$. The
 body of $\dec{odd}$ invokes, or queries, this operation twice with
-arguments $0$ and $1$, respectively. The results are then tested using
+arguments $0$ and $1$, respectively. The results are tested using
 exclusive-or.
 
 Now, let us implement the environment for $\dec{odd}$.
@@ -5051,18 +5087,16 @@ Now, let us implement the environment for $\dec{odd}$.
   \el
 \]
 %
-We allow ourselves to use recursive data types to make the example
-concise. Type $\dec{Dialogue}$ represents the dialogue between
-$\dec{odd}$ and its parameter. The data structure is a standard binary
-tree with two constructors: $!$ constructs a leaf holding a value of
-type $\Int$ and $?$ constructs an interior node holding a value of
-type $\Bool$ and two subtrees. The function $\dec{env}$ implements the
-environment that $\dec{odd}$ will be run in. This function evaluates
-its parameter $m$ under $\Catchcont$ which injects the operation
-$f$. If $m$ returns, then the left component gets tagged with $!$,
-otherwise the argument to the operation $q$ gets tagged with a $?$
-along with the subtrees constructed by the two recursive applications
-of $\dec{env}$.
+Type $\dec{Dialogue}$ represents the dialogue between $\dec{odd}$ and
+its parameter. The data structure is a standard binary tree with two
+constructors: $!$ constructs a leaf holding a value of type $\Int$ and
+$?$ constructs an interior node holding a value of type $\Bool$ and
+two subtrees. The function $\dec{env}$ implements the environment that
+$\dec{odd}$ will be run in. This function evaluates its parameter $m$
+under $\Catchcont$ which injects the operation $f$. If $m$ returns,
+then the left component gets tagged with $!$, otherwise the argument
+to the operation $q$ gets tagged with a $?$ along with the subtrees
+constructed by the two recursive applications of $\dec{env}$.
 %
 % The primitive structure of catchcont makes it somewhat fiddly to
 % program with it compared to other control operators as we have to
@@ -5071,6 +5105,14 @@ of $\dec{env}$.
 The following derivation gives the high-level details of how
 evaluation proceeds.
 %
+\begin{figure}
+\begin{center}
+    \scalebox{1.3}{\SXORTwoModel}
+  \end{center}
+  \caption{Visualisation of the result obtained by
+    $\dec{env}~\dec{odd}$.}\label{fig:decision-tree-cc}
+\end{figure}
+%
 \begin{derivation}
   &\dec{env}~\dec{odd}\\
   \reducesto^+ & \reason{$\beta$-reduction}\\
@@ -5107,14 +5149,6 @@ Figure~\ref{fig:decision-tree-cc} visualises this result as a binary
 tree. The example here does not make use of the `continuation
 component', the interested reader may consult \citet{LongleyW08} for
 an example usage.
-%
-\begin{figure}
-\begin{center}
-    \scalebox{1.3}{\SXORTwoModel}
-  \end{center}
-  \caption{Visualisation of the result obtained by
-    $\dec{env}~\dec{odd}$.}\label{fig:decision-tree-cc}
-\end{figure}
 % \subsection{Second-class control operators}
 % Coroutines, async/await, generators/iterators, amb.
 
@@ -19209,7 +19243,7 @@ language~\cite{Plotkin77}. It is also well known that the presence of
 control features or local state enables observational distinctions
 that cannot be made in a purely functional setting: for instance,
 there are programs involving call/cc that detect the order in which a
-(call-by-name) `+' operation evaluates its arguments
+(call-by-name) `$+$' operation evaluates its arguments
 \citep{CartwrightF92}. Such operations are `non-functional' in the
 sense that their output is not determined solely by the extension of
 their input (seen as a mathematical function