Fix typos and other various small improvements.

macros.tex

@@ -168,6 +168,7 @@
 
 \newenvironment{eqs}{\ba{@{}r@{~}c@{~}l@{}}}{\ea}
 \newenvironment{equations}{\[\ba{@{}r@{~}c@{~}l@{}}}{\ea\]\ignorespacesafterend}
+\newcommand\numberthis{\addtocounter{equation}{1}\tag{$\ast$\theequation}} % Numbering equations
 \newenvironment{derivation}{\begin{displaymath}\ba{@{}r@{~}l@{}}}{\ea\end{displaymath}\ignorespacesafterend}
 \newcommand{\reason}[1]{\quad (\text{#1})}
 

thesis.tex

@@ -1164,11 +1164,11 @@ follows.
 \ea
 \]
 %
-The attentive reader will notice that we are using the same notation
+The attentive reader will notice that I am using the same notation for
-for type and term substitutions. In fact, we shall go further and
+type and term substitutions. In fact, we shall go further and unify
-unify the two notions of substitution by combining them. As such we
+the two notions of substitution by combining them. As such we may
-may think of a combined substitution map as pair of a term
+think of a combined substitution map as pair of a term substitution
-substitution map and a type substitution map, i.e.
+map and a type substitution map, i.e.
 $\sigma : (\VarCat \times \ValCat)^\ast \times (\TyVarCat \times
 \TypeCat)^\ast$. The application of a combined substitution mostly the
 same as the application of a term substitution map save for a couple
@@ -1943,15 +1943,15 @@ Continuation-passing style (CPS) is a \emph{canonical} program
 notation that makes every facet of control flow and data flow
 explicit. In CPS every function takes an additional function-argument
 called the \emph{continuation}, which represents the next computation
-in evaluation position. CPS is canonical in the sense that is
+in evaluation position. CPS is canonical in the sense that it is
-definable in pure $\lambda$-calculus without any primitives. As an
+definable in pure $\lambda$-calculus without any further
-informal illustration of CPS consider again the rudimentary factorial
+primitives. As an informal illustration of CPS consider again the
-function from Section~\ref{sec:tracking-div}.
+rudimentary factorial function from Section~\ref{sec:tracking-div}.
 %
 \[
   \bl
     \dec{fac} : \Int \to \Int\\
-    \dec{fac} \defas \Rec\;f~n.
+    \dec{fac} \defas \lambda n.
        \ba[t]{@{}l}
          \Let\;is\_zero \revto n = 0\;\In\\
          \If\;is\_zero\;\Then\; \Return\;1\\
@@ -1972,24 +1972,19 @@ implementation of this function changes as follows.
   \bl
   \dec{fac}_{\dec{cps}} : \Int \to (\Int \to \alpha) \to \alpha\\
   \dec{fac}_{\dec{cps}} \defas \lambda n.\lambda k.
-     =_{\dec{cps}}~n~0~
+     (=_{\dec{cps}})~n~0~
-       (\ba[t]{@{~}l}
+       (\lambda is\_zero.
-          \lambda is\_zero.\\
+          \ba[t]{@{~}l}
-          \quad\ba[t]{@{~}l}
           \If\;is\_zero\;\Then\; k~1\\
           \Else\;
-          -_{\dec{cps}}~n~1~
+          (-_{\dec{cps}})~n~1~
             (\lambda n'.
                \dec{fac}_{\dec{cps}}~n'~
-                  (\lambda m. *_{\dec{cps}}~n~m~
+                  (\lambda m. (*_{\dec{cps}})~n~m~k)))
-                  (\lambda res. k~res))))
           \ea
-        \ea
   \el
 \]
 %
-\dhil{Adjust the example to avoid stepping into the margin.}
-%
 There are several worthwhile observations to make about the
 differences between the two implementations $\dec{fac}$ and
 $\dec{fac}_{\dec{cps}}$.
@@ -2000,12 +1995,9 @@ continuation. By convention the continuation parameter is named $k$ in
 the implementation. The continuation captures the remainder of
 computation that ultimately produces a result of type $\alpha$, or put
 differently: it determines what to do with the result returned by an
-invocation of $\dec{fac}$. Semantically the continuation corresponds
+invocation of $\dec{fac}_{\dec{cps}}$. Semantically the continuation corresponds
 to the surrounding evaluation
-context.% , thus with a bit of hand-waving
+context.
-% we can say that for $\EC[\dec{fac}~2]$ the entire evaluation $\EC$
-% would be passed as the continuation argument to the CPS version:
-% $\dec{fac}_{\dec{cps}}~2~\EC$.
 %
 Secondly note that every $\Let$-binding in $\dec{fac}$ has become a
 function application in $\dec{fac}_{\dec{cps}}$. The functions
@@ -2016,10 +2008,11 @@ has been turned into an application of continuation $k$, and the
 implicit return $n*m$ in the $\Else$-branch has been turned into an
 explicit application of the continuation.
 %
-Thirdly note every function application is in tail position. This is a
+Thirdly note every function application occurs in tail position. This
-characteristic property of CPS that makes CPS feasible as a practical
+is a characteristic property of CPS that makes CPS feasible as a
-implementation strategy since programs in CPS notation does not
+practical implementation strategy since programs in CPS notation do
-consume stack space.
+not consume stack space.
+%
 \dhil{The focus of the introduction should arguably not be to explain CPS.}
 \dhil{Justify CPS as an implementation technique}
 \dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
@@ -2111,6 +2104,10 @@ term) to cope with the case of pattern matching failure.
 \label{fig:cps-cbv-target}
 \end{figure}
 
+\dhil{Most of the primitives are Church encodable. Discuss the value
+  of treating them as primitive rather than syntactic sugar (target
+  languages such as JavaScript has similar primitives).}
+
 \section{CPS transform for fine-grain call-by-value}
 \label{sec:cps-cbv}
 
@@ -2266,10 +2263,10 @@ Conceptually, this translation encloses the translated program in a
 top-level handler with an empty collection of operation clauses and an
 identity return clause.
 
-We may regard this particular CPS translation as being simple, because
+A pleasing property of this particular CPS translation is that it is a
-it requires virtually no extension to the CPS translation for
+conservative extension to the CPS translation for $\BCalc$. Alas, this
-$\BCalc$. However, this translation suffers from two deficiencies
+translation also suffers two displeasing properties which makes it
-which makes it unviable in practice.
+unviable in practice.
 
 \begin{enumerate}
   \item The image of the translation is not \emph{properly
@@ -2280,9 +2277,11 @@ which makes it unviable in practice.
 
   \item The image of the translation yields static administrative
     redexes, i.e. redexes that could be reduced statically. This is a
-    classic problem with CPS translation, which is typically dealt
+    classic problem with CPS translations. This problem can be dealt
     with by introducing a second pass to clean up the
-    image~\cite{DanvyF92}.
+    image~\cite{Plotkin75}. By clever means the clean up pass and the
+    translation pass can be fused together to make an one-pass
+    translation~\cite{DanvyF92,DanvyN03}.
 \end{enumerate}
 
 The following minimal example readily illustrates both issues.
@@ -2291,7 +2290,7 @@ The following minimal example readily illustrates both issues.
 \pcps{\Return\;\Record{}}
      &=         & (\lambda k.k\,\Record{})\,(\lambda x.\lambda h.x)\,(\lambda \Record{z,\_}.\Absurd\,z)  \\
      &\reducesto& ((\lambda x.\lambda h.x)\,\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \\
-     &\reducesto& (\lambda h.\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z)\\
+     &\reducesto& (\lambda h.\Record{})\,(\lambda \Record{z,\_}.\Absurd\,z) \numberthis\label{eq:cps-admin-reduct} \\
      &\reducesto& \Record{} \\
 \end{equations}
 %
@@ -2314,7 +2313,7 @@ As for administrative redexes, observe that the first reduction is
 administrative. It is an artefact introduced by the translation, and
 thus it has nothing to do with the dynamic semantics of the original
 term. We can eliminate such redexes statically. We will address this
-issue in Section~\ref{sec:higher-order-cps}.
+issue in Section~\ref{sec:higher-order-uncurried-deep-handlers-cps}.
 
 Nevertheless, we can show that the image of this CPS translation
 simulates the preimage. Due to the presence of administrative
@@ -2375,13 +2374,13 @@ target calculus $\UCalc$ as it permits an arbitrary computation term
 in the function position of an application term.
 %
 
-As a first step we may impose a syntax restriction in target calculus
+As a first step we may restrict the syntax of the target calculus such
-such that the term in function position must be a value. With this
+that the term in function position must be a value. With this
 restriction the syntax of $\UCalc$ implements the property that any
 term constructor features at most one computation term, and this
 computation term always appears in tail position. Thus this
 restriction suffices to ensure that every function application will be
-in tail-position.
+in tail position.
 %
 Figure~\ref{fig:refined-cps-cbv-target} contains the adjustments to
 syntax and semantics of $\UCalc$. The target calculus now supports
@@ -2407,7 +2406,7 @@ is no longer well-formed.
 The crux of the problem is that the curried interpretation of
 continuations causes the CPS translation to produce `large'
 application terms, e.g. the translation rule for effect forwarding
-produces three-argument application term.
+produces a three-argument application term.
 %
 To rectify this problem we can adapt the technique of
 \citet{MaterzokB12} to uncurry our CPS translation. Uncurrying
@@ -2478,18 +2477,20 @@ refined translation makes the example properly tail-recursive.
 \begin{equations}
 \pcps{\Return\;\Record{}}
      &=         & (\lambda (k \cons ks).k\,\Record{}\,ks)\,((\lambda x.\lambda ks.x) \cons (\lambda \Record{z, \_}.\lambda ks.\Absurd\,z) \cons \nil)  \\
-     &\reducesto& (\lambda x.\lambda ks.x)\,\Record{}\,((\lambda \Record{z,\_}.\lambda ks.\Absurd\,z) \cons \nil)\\
+     &\reducesto& (\lambda x.\lambda ks.x)\,\Record{}\,((\lambda \Record{z,\_}.\lambda ks.\Absurd\,z) \cons \nil) \numberthis\label{eq:cps-admin-reduct-2}\\
      &\reducesto& \Record{}
 \end{equations}
 %
-The image of this uncurried translation admits three
+The reduction sequence in the image of this uncurried translation has
-$\reducesto$-reduction steps (disregarding the administrative steps
+one fewer steps (disregarding the administrative steps induced by
-induced by pattern matching), which is one less step than admitted by
+pattern matching) than in the image of the curried translation. The
-the image of the curried translation. The `missing' step is precisely
+`missing' step is precisely the reduction marked
-the partial application of the initial pure continuation function,
+(\ref{eq:cps-admin-reduct}), which was a partial application of the
-which was not in tail position. Note, however, that the first
+initial pure continuation function that was not in tail
-reduction is remains administrative, the reduction is entirely static,
+position. Note, however, that the first reduction
-and as such, it can be dealt with as part of the translation.
+(\ref{eq:cps-admin-reduct-2}) remains administrative, the reduction is
+entirely static, and as such, it can be dealt with as part of the
+translation.
 %
 
 \paragraph{Administrative redexes}
@@ -2511,8 +2512,8 @@ a suitable handler (if such one exists).
 %
 The translation presented above realises effect forwarding by
 explicitly applying the next effect continuation. This application is
-an example of a dynamic administrative reduction. Though, not all
+an example of a dynamic administrative reduction. Not every dynamic
-dynamic administrative redexes are necessary, for instance, the
+administrative reduction is necessary, though. For instance, the
 implementation of resumptions as a composition of
 $\lambda$-abstractions gives rise to administrative reductions upon
 invocation. As we shall see in
@@ -2520,8 +2521,8 @@ Section~\ref{sec:first-order-explicit-resump} administrative
 reductions due to resumption invocation can be dealt with by choosing
 a more clever implementation of resumptions.
 
-We can characterise static administrative redexes\dots
+% We can characterise static administrative redexes\dots
-\dhil{Characterise static redexes\dots}
+% \dhil{Characterise static redexes\dots}
 
 % \dhil{Discuss dynamic and static administrative redex.}
 
@@ -2537,7 +2538,7 @@ administrative redexes as function composition necessitates the
 introduction of an additional lambda abstraction.
 %
 
-We can avert generating these administrative redexes by applying a
+We can avoid generating these administrative redexes by applying a
 variation of the technique that we used in the previous section to
 uncurry the curried CPS translation.
 %
@@ -2589,8 +2590,8 @@ resumptions.
 %
 The translation of $\Do$ constructs an initial resumption stack,
 operation clauses extract and convert the current resumption stack
-into a function using the $\Res$, and $\hforward$ augments the current
+into a function using the $\Res$ construct, and $\hforward$ augments
-resumption stack with the current continuation pair.
+the current resumption stack with the current continuation pair.
 %
 
 \subsection{Higher-order translation for deep effect handlers}
@@ -2674,8 +2675,8 @@ resumption stack with the current continuation pair.
 \label{fig:cps-higher-order-uncurried}
 \end{figure}
 %
-In the previous sections, we have step-wise refined the initial
+In the previous sections, we have seen step-wise refinements of the
-curried CPS translation for deep effect handlers
+initial curried CPS translation for deep effect handlers
 (Section~\ref{sec:first-order-curried-cps}) to be properly
 tail-recursive (Section~\ref{sec:first-order-uncurried-cps}) and to
 avoid yielding unnecessary dynamic administrative redexes for
@@ -2686,30 +2687,30 @@ yields static administrative redexes. In this section we will further
 refine the CPS translation to eliminate all static administrative
 redexes at translation time.
 %
-Specifically, we will adapt the translation to a higher-order one-pass
+Specifically, the translation will be adapted to a higher-order
-CPS translation~\citep{DanvyF90} that partially evaluates
+one-pass CPS translation~\citep{DanvyF90} that partially evaluates
 administrative redexes at translation time.
 %
-Following \citet{DanvyN03}, we adopt a two-level lambda calculus
+Following \citet{DanvyN03}, I will use a two-level lambda calculus
 notation to distinguish between \emph{static} lambda abstraction and
 application in the meta language and \emph{dynamic} lambda abstraction
 and application in the target language. To disambiguate syntax
-constructors in the respective calculi we mark static constructors
+constructors in the respective calculi I will mark static constructors
 with a {\color{blue}$\overline{\text{blue overline}}$}, whilst dynamic
 constructors are marked with a
 {\color{red}$\underline{\text{red underline}}$}. The principal idea is
 that redexes marked as static are reduced as part of the translation,
 whereas those marked as dynamic are reduced at runtime. To facilitate
-this notation we write application explicitly using an infix ``at''
+this notation I will write application explicitly using an infix
-symbol ($@$) in both calculi.
+``at'' symbol ($@$) in both calculi.
 
 \paragraph{Static terms}
 %
-As in the dynamic target language, we will represent continuations as
+As in the dynamic target language, continuations are represented as
 alternating lists of pure continuation functions and effect
-continuation functions. To ease notation we are going make use of
+continuation functions. To ease notation I will make use of pattern
-pattern matching notation. The static meta language is generated by
+matching notation. The static meta language is generated by the
-the following productions.
+following productions.
 %
 \begin{syntax}
   \slab{Static patterns} &\sP \in \SPatCat &::=& \sks \mid \sk \scons \sP\\
@@ -2727,7 +2728,7 @@ statically known pure continuations, $\sh$ to denote statically known
 effect continuations, and $\sks$ to denote statically known
 continuations.
 %
-We shall use $\sM$ to range over static computations, which comprise
+I shall use $\sM$ to range over static computations, which comprise
 static values, static application and binary dynamic application of a
 static value to two dynamic values.
 %
@@ -2782,19 +2783,17 @@ ensures that the translation on computation terms has immediate access
 to the next pure and effect continuation functions. In fact, the
 translation is set up such that every generated dynamic
 $\dlam$-abstraction deconstructs its continuation argument
-appropriately to be to expose just enough (static) continuation
+appropriately to expose just enough (static) continuation structure in
-structure in order to guarantee that static pattern matching never
+order to guarantee that static pattern matching never fails.
-fails.
 %
-(Though, the translation is somewhat unsatisfactory regarding this
+(The translation is somewhat unsatisfactory regarding this
 deconstruction of dynamic continuations as the various generated
 dynamic lambda abstractions do not deconstruct their continuation
-arguments uniformly. I will return to discuss this dissatisfaction
+arguments uniformly.)
-shortly.)
 %
 Since the target language is oblivious to types any
 $\Lambda$-abstraction gets translated in a similar way to
-$\Lambda$-abstraction, where the first parameter becomes a placeholder
+$\lambda$-abstraction, where the first parameter becomes a placeholder
 for a ``dummy'' unit argument.
 
 The translation of computation terms is more interesting. Note the
@@ -2806,10 +2805,10 @@ a $\UCalc$-computation term. The static continuation may be
 manipulated during the translation as is done in the translations of
 $\Return$, $\Let$, $\Do$, and $\Handle$. The translation of $\Return$
 consumes the next pure continuation function $\sk$ and applies it
-dynamically it to the translation of $V$ and the reified remainder,
+dynamically to the translation of $V$ and the reified remainder,
 $\sks$, of the static continuation. Keep in mind that the translation
 of $\Return$ only consumes one of the two guaranteed available
-continuation functions from the provided continuation argument, as a
+continuation functions from the provided continuation argument; as a
 consequence the next continuation function in $\sks$ is an effect
 continuation. This consequence is accounted for in the translations of
 $\Let$ and $\Return$-clauses, which are precisely the two possible
@@ -3006,7 +3005,7 @@ construction and deconstruction).
 \label{sec:higher-order-cps-deep-handlers-correctness}
 
 We establish the correctness of the higher-order uncurried CPS
-translation via a simulation result in style of
+translation via a simulation result in the style of
 Plotkin~\cite{Plotkin75} (Theorem~\ref{thm:ho-simulation}). However,
 before we can state and prove this result, we first several auxiliary
 lemmas describing how translated terms behave. First, the higher-order
@@ -3055,9 +3054,9 @@ It follows as a corollary that top-level substitution is well-behaved.
   Lemma~\ref{lem:ho-cps-subst}.
 \end{proof}
 %
-In order to reason about the behaviour \semlab{Op} rule, which is
+In order to reason about the behaviour of the \semlab{Op} rule, which
-defined in terms of an evaluation context, we need to extend the CPS
+is defined in terms of an evaluation context, we need to extend the
-translation to evaluation contexts.
+CPS translation to evaluation contexts.
 %
 \begin{equations}
 \cps{-}                             &:& \EvalCat \to \SValCat\\
@@ -3154,13 +3153,14 @@ rule.
 \label{lem:handle-op}
 If $\ell \notin BL(\EC)$ and $\hell = \{\ell\,p\,r \mapsto N_\ell\}$ then
 %
-\begin{displaymath}
+\[
 \bl
-\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\reflect\cps{\hret} \scons \reflect\cps{\hops} \scons \sV)) \reducesto^+\areducesto^* \\
+\cps{\Do\;\ell\;V} \sapp (\cps{\EC} \sapp (\reflect\cps{\hret} \scons \reflect\cps{\hops} \scons \sV)) \reducesto^+\areducesto^\ast \\
 \quad
-    (\cps{N_\ell} \sapp \sV)[\cps{V}/p, (\lambda y\,ks.\cps{\Return\;y} \sapp (\cps{\EC} \sapp (\reflect\cps{\hret} \scons \reflect\cps{\hops} \scons \reflect ks)))/r] \\
+    (\cps{N_\ell} \sapp \sV)[\cps{V}/p, (\lambda y\,ks.\cps{\Return\;y} \sapp (\cps{\EC} \sapp (\reflect\cps{\hret} \scons \reflect\cps{\hops} \scons \reflect ks)))/]
 \el
-\end{displaymath}
+\]
+%
 \end{lemma}
 %
 \begin{proof}
@@ -3246,8 +3246,8 @@ second corresponds to the return clause of the current handler.
 To distinguish between the two kinds of pure continuations, we shall
 write $\svhret$ for statically known pure continuations arising from
 return clauses, and $\vhret$ for dynamically known ones. Similarly, we
-write $\svhops$ and $\vhops$ for statically and dynamically,
+write $\svhops$ and $\vhops$, respectively, for statically and
-respectively, known effect continuations. With this notation in mind,
+dynamically, known effect continuations. With this notation in mind,
 we may translate operation invocation and handler installation using
 the new interpretation of the continuation representation as follows.
 %
@@ -3352,9 +3352,10 @@ leaks.
 
 The use of dummy handlers is symptomatic for the need of a more
 general notion of resumptions. Upon resumption invocation the dangling
-pure continuation should be composed with current pure continuation
+pure continuation should be composed with the current pure
-which suggests shallow variation of the resumption construction
+continuation which suggests the need for a shallow variation of the
-primitive $\Res$ that behaves along the following lines.
+resumption construction primitive $\Res$ that behaves along the
+following lines.
 %
 \[
   \bl
@@ -3393,14 +3394,14 @@ dealt with in Section~\ref{sec:first-order-explicit-resump}.
 In order to avoid generating these administrative redexes we need a
 more intensional continuation representation.
 %
-Another telltale for a more intensional continuation representation is
+Another telltale sign that we require a more intensional continuation
-the necessary use of the administrative function $\kid$ in the
+representation is the necessary use of the administrative function
-translation of $\Handle$ as a placeholder for the empty pure
+$\kid$ in the translation of $\Handle$ as a placeholder for the empty
-continuation.
+pure continuation.
 %
 In terms of aesthetics, the non-uniform continuation deconstructions
-also suggest that we could do with a more structured interpretation of
+also suggest that we could benefit from a more structured
-continuations.
+interpretation of continuations.
 %
 Although it is seductive to program with lists, it quickly gets
 unwieldy.
@@ -3469,7 +3470,7 @@ shallow handlers demands that this return clause is discarded when any
 of the operations is invoked.
 
 The solution to the first problem is to reuse the key idea of
-Section~\ref{sec:first-order-explicit-resump} to avert administrative
+Section~\ref{sec:first-order-explicit-resump} to avoid administrative
 continuation functions by representing a pure continuation as an
 explicit list consisting of pure continuation functions. As a result
 the composition of pure continuation functions can be realised as a
@@ -3512,6 +3513,8 @@ two reduction rules.
   & f\,W\,(\dRecord{fs, h} \dcons \dhk)
 \end{reductions}
 %
+\dhil{Say something about skip frames?}
+%
 The first rule describes what happens when the pure continuation is
 exhausted and the return clause of the enclosing handler is
 invoked. The second rule describes the case when the pure continuation
@@ -3999,6 +4002,8 @@ 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}$.
 
+\dhil{Check whether the first pass marks administrative redexes}
+
 
 % CPS The colon translation captures the
 % intuition tThe colon translation is itself a CPS translation which