Change section title

macros.tex

@@ -150,7 +150,7 @@
 %%
 %% Labels
 %%
-\newcommand{\slab}[1]{\textrm{#1}}
+\newcommand{\slab}[1]{\ensuremath{\mathsf{#1}}}
 \newcommand{\rulelabel}[2]{\ensuremath{\mathsf{#1\textrm{-}#2}}}
 \newcommand{\klab}[1]{\rulelabel{K}{#1}}
 \newcommand{\semlab}[1]{\rulelabel{S}{#1}}
@@ -440,8 +440,8 @@
 \newcommand{\fprompt}{\%}
 \newcommand{\splitter}{\keyw{splitter}}
 \newcommand{\J}{\keyw{J}}
-\newcommand{\FelleisenC}{\ensuremath{\mathcal{C}}}
-\newcommand{\FelleisenF}{\ensuremath{\mathcal{F}}}
+\newcommand{\FelleisenC}{\ensuremath{\keyw{C}}}
+\newcommand{\FelleisenF}{\ensuremath{\keyw{F}}}
 \newcommand{\cont}{\keyw{cont}}
 \newcommand{\Cont}{\dec{Cont}}
 \newcommand{\Algol}{Algol~60}

thesis.tex

@@ -679,7 +679,7 @@ non-exhaustive list of first-class control operators.
     \hline
     \multicolumn{1}{| l |}{\textbf{Name}} & \multicolumn{1}{l |}{\textbf{Extent}} & \multicolumn{1}{l |}{\textbf{Continuation behaviour}} & \multicolumn{1}{l |}{\textbf{Canonical reference}}\\
     \hline
-    \FelleisenC & Undelimited & Abortive & \citet{FelleisenF86} \\
+    C        & Undelimited & Abortive & \citet{FelleisenF86} \\
     \hline
     call/cc  & Undelimited & Abortive & \citet{AbelsonHAKBOBPCRFRHSHW85} \\
     \hline
@@ -697,7 +697,7 @@ non-exhaustive list of first-class control operators.
     \hline
     escape              & Undelimited & Abortive & \citet{Reynolds98a}\\
     \hline
-    \FelleisenF         & Undelimited & Composable & \citet{FelleisenFDM87}\\
+    F                   & Undelimited & Composable & \citet{FelleisenFDM87}\\
     \hline
     fcontrol            & Delimited & Composable & \citet{Sitaram93} \\
     \hline
@@ -802,14 +802,22 @@ argument $V$ plugged in.
 
 \paragraph{Sussman and Steele's catch}
 %
-The catch operator was introduced into the programming language Scheme
-by \citeauthor{SussmanS75} in 1975 as a mechanism for performing
-non-local exits~\cite{SussmanS75}.
+The catch operator originated in Lisp as an exception handling
+construct. It had a companion throw operation, which would unwind the
+evaluation stack until it was caught by an instance of catch. In 1975
+\citeauthor{SussmanS75} implemented a more powerful variation of the
+catch operator in Scheme~\cite{SussmanS75}. Their catch operator would
+disperse of the throw operation and instead provide the programmer
+with access to the current continuation. Thus it is same as
+\citeauthor{Reynolds98a}' escape operator.
 %
 \[
   M,N ::= \cdots \mid \Catch~k.M
 \]
 %
+Although, their syntax differ, their static and dynamic semantics are
+the same.
+%
 \begin{mathpar}
   \inferrule*
     {\typ{\Gamma,k : \Cont\,\Record{A;\Zero}}{M : A}}
@@ -825,11 +833,28 @@ non-local exits~\cite{SussmanS75}.
   \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
 \end{reductions}
 %
-As an aside it is worth mentioning that \citet{CartwrightF92} used a
-variation of $\Catch$ to show that programs can use control operators
+As an aside it is worth to mention that \citet{CartwrightF92} used a
+variation of $\Catch$ to show that control operators enable programs
 to observe the order of evaluation.
 
-\paragraph{Call-with-current-continuation}
+\paragraph{Call-with-current-continuation} In 1982 the Scheme
+implementors observed that they could dispense of the special syntax
+for $\Catch$ in favour of a higher-order function that would apply its
+argument to the current continuation, and thus callcc was born (callcc
+is short for
+call-with-current-continuation)~\cite{AbelsonHAKBOBPCRFRHSHW85}.
+%
+
+Unlike the previous operators, callcc augments the syntactic
+categories of values.
+%
+\[
+  V,W \in \ValCat ::= \cdots \mid \Callcc
+\]
+%
+The value $\Callcc$ is essentially a hard-wired function name. The
+typing rule for $\Callcc$ makes it clear that it is a particular
+higher-order function.
 %
 \begin{mathpar}
   \inferrule*
@@ -841,11 +866,22 @@ to observe the order of evaluation.
     {\typ{\Gamma}{\Continue~W~V : \Zero}}
 \end{mathpar}
 %
+An invocation of $\Callcc$ returns a value of type $A$. This value can
+be produced in one of two ways, either the function argument returns
+normally or it applies the provided continuation object to a value
+that then becomes the result of $\Callcc$-application.
+%
 \begin{reductions}
   \slab{Capture} &  \EC[\Callcc~V] &\reducesto& \EC[V~\cont_{\EC}]\\
   \slab{Resume}  &  \EC[\Continue~\cont_{\EC'}~V]  &\reducesto& \EC'[V]
 \end{reductions}
 %
+From the dynamic semantics it is evident that $\Callcc$ is a
+syntax-free alternative to $\Catch$, i.e.
+%
+\[
+  \sembr{\Catch~k.M} = \Callcc\,(\lambda k.M)
+\]
 
 \paragraph{Call-with-composable-continuation}
 call-with-composable-continuation (MzScheme 360, November 2006).
@@ -1006,8 +1042,8 @@ annotate the evaluation contexts for ordinary applications.
   \slab{Resume}    & \EC[\Continue~\cont_{\Record{\EC';W}}\,V]  &\reducesto& \EC'[W\,V]
 \end{reductions}
 %
-$\slab{Capture}$ rule only applies if the application of $\J$ takes
-place in annotated evaluation context. The continuation object
+The $\slab{Capture}$ rule only applies if the application of $\J$
+takes place in annotated evaluation context. The continuation object
 produced by a $\J$ application encompasses the caller's continuation
 $\EC_\lambda$ and the value argument $W$.
 %
@@ -1047,6 +1083,8 @@ undelimited control~\cite{Filinski94}
 
 \paragraph{Control/prompt}
 %
+The operator control is a rebranding of Felleisen's F operator.
+%
 \begin{reductions}
   \slab{Value} &
      \Prompt~V &\reducesto& V\\
@@ -1115,9 +1153,9 @@ undelimited control~\cite{Filinski94}
 %
 \begin{reductions}
   \slab{Value}    & \reset{V}               &\reducesto& V\\
-  \slab{Capture}  & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\reset{\EC}}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
+  \slab{Capture}  & \reset{\EC[\shift\,k.M]} &\reducesto& \reset{M[\cont_{\EC}/k]}, \text { where $\EC$ contains no $\reset{-}$}\\
   % \slab{Resume}   & \reset{\EC[\Continue~\cont_{\reset{\EC'}}~V]} &\reducesto& \reset{\EC[\reset{\EC'[V]}]}\\
-  \slab{Resume}   & \Continue~\cont_{\reset{\EC}}~V &\reducesto& \reset{\EC[V]}\\
+  \slab{Resume}   & \Continue~\cont_{\EC}~V &\reducesto& \reset{\EC[V]}\\
 \end{reductions}
 %
 
@@ -1131,9 +1169,9 @@ undelimited control~\cite{Filinski94}
 
 \paragraph{Splitter}
 \begin{reductions}
-  \slab{Throw}   & \splitter~f~g.\EC[\,f~V] &\reducesto& V~\Unit\\
+  \slab{Throw}   & \splitter~throw~callpc.\EC[\,throw~V] &\reducesto& V~\Unit\\
   \slab{Capture} &
-     \splitter~f~g.\EC[g~V] &\reducesto& V~\cont_{\EC} \\
+     \splitter~throw~callpc.\EC[callpc~V] &\reducesto& V~\cont_{\EC} \\
   \slab{Resume}  & \Continue~\cont_{\EC}~V &\reducesto& \EC[V]
 \end{reductions}
 
@@ -1156,7 +1194,7 @@ For example callec is a variation of callcc where the continuation
 only can be invoked during the dynamic extent of
 callec~\cite{Flatt20}.
 
-\section{Implementation strategies for first-class control}
+\section{Implementing continuations}
 Table~\ref{tbl:ctrl-operators-impls} lists some programming languages
 with support for first-class control operators and their
 implementation strategies.