Plotkin's colon translation.

thesis.tex

@@ -1899,6 +1899,7 @@ getting stuck on an unhandled operation.
 \dhil{Reader}
 \dhil{State}
 \dhil{Nondeterminism}
+\dhil{Inversion of control: generator from iterator}
 
 \section{Parameterised handlers}
 \label{sec:unary-parameterised-handlers}
@@ -2941,25 +2942,68 @@ If $M \reducesto N$ then $\pcps{M} \reducesto^+ \areducesto^* \pcps{N}$.
 \section{Related work}
 \label{sec:cps-related-work}
 
-\subsection{Plotkin's colon translation}
+\paragraph{Plotkin's colon translation}
 
-\citeauthor{Plotkin75}'s original CPS translation yielded static
-administrative redexes.  Clearly this translation is undesirable from
-a practical point of view as it generates an additional and completely
-artefactual overhead. From a theoretical point of view such a CPS
-translation is also undesirable as the presence of administrative
-redexes makes proof of correctness considerably more involved.
+The defacto standard method for proving the correctness of a CPS
+translation is by way of a simulation result. Simulation states that
+every reduction sequence in a given source program is mimicked by its
+CPS transformation.
 %
-\citeauthor{Plotkin75}'s simulation theorem shows a correspondence
-between reductions in a given source program and its transformed
-program. To establish this correspondence in the presence of
-administrative redexes, \citeauthor{Plotkin75} introduced the
-so-called ``colon''-translation\dots
+Static administrative redexes in the image of a CPS translation
+provide hurdles for proving simulation, since these redexes do not
+arise in the source program.
+%
+\citet{Plotkin75} uses the so-called \emph{colon translation} to
+overcome static administrative reductions.
+%
+Informally, it is defined such that given a source term $M$ and a
+continuation $k$, the term $M : k$ is the result of performing all
+static administrative reductions on $\cps{M}\,k$, that is
+$\cps{M}\,k \reducesto^\ast M : k$.
+%
+Thus this translation makes it possible to bypass administrative
+reductions and instead focus on the reductions inherited from the
+source program.
+%
+The colon translation captures precisely the intuition that drives CPS
+transforms, namely, that if in the source $M \reducesto^\ast \Return\;V$
+then in the image $\cps{M}\,k \reducesto^\ast k\,\cps{V}$.
 
-% between the sourceTo prove the correctness of his CPS translation, \citet{Plotkin75}
-% made use of a so-called ``colon''-translation to bypass administrative reductions
 
-\subsection{Iterated CPS translations}
+% CPS The colon translation captures the
+% intuition tThe colon translation is itself a CPS translation which
+% yields
+
+
+% In his seminal work, \citet{Plotkin75} devises CPS translations for
+% call-by-value lambda calculus into call-by-name lambda calculus and
+% vice versa. \citeauthor{Plotkin75} establishes the correctness of his
+% translations by way of simulations, which is to say that every
+% reduction sequence in a given source program is mimicked by the
+% transformed program.
+% %
+% His translations generate static administrative redexes, and as argued
+% previously in this chapter from a practical view point this is an
+% undesirable property in practice. However, it is also an undesirable
+% property from a theoretical view point as the presence of
+% administrative redexes interferes with the simulation proofs.
+
+% To handle the static administrative redexes, \citeauthor{Plotkin75}
+% introduced the so-called \emph{colon translation} to bypass static
+% administrative reductions, thus providing a means for focusing on
+% reductions induced by abstractions inherited from the source program.
+% %
+% The colon translation is itself a CPS translation, that given a source
+% expression, $e$, and some continuation, $K$, produces a CPS term such
+% that $\cps{e}K \reducesto e : K$.
+
+% \citet{DanvyN03} used this insight to devise a one-pass CPS
+% translation that contracts all administrative redexes at translation
+% time.
+
+\paragraph{Iterated CPS transform}
+
+\paragraph{Partial evaluation}
 
 \chapter{Abstract machine semantics}