dhil/phd-dissertation
1
0
Fork 0
mirror of https://github.com/dhil/phd-dissertation synced 2026-03-13 11:08:25 +00:00
Code Issues Releases Wiki Activity

Define the parity of a continuation

Browse Source
This commit is contained in:
Daniel Hillerström
2020-09-22 21:03:12 +01:00
parent ad548b2fa4
commit 0d349fb56d
1 changed files with 17 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

21
thesis.tex
View File

@@ -2399,8 +2399,6 @@ These changes to $\UCalc$ immediately invalidate the curried
translation from the previous section as the image of the translation translation from the previous section as the image of the translation
is no longer well-formed. is no longer well-formed.
% %
% The crux of the problem is the curried representation of the
% continuation pair.
The crux of the problem is that the curried interpretation of The crux of the problem is that the curried interpretation of
continuations causes the CPS translation to produce `large' continuations causes the CPS translation to produce `large'
application terms, e.g. the translation rule for effect forwarding application terms, e.g. the translation rule for effect forwarding
@@ -2754,10 +2752,20 @@ $\reify \sV$ by induction on their structure.
\ea \ea
\] \]
% %
%\dhil{Need to spell out that static pattern matching may induce dynamic (administrative) reductions}
%
\paragraph{Higher-order translation} \paragraph{Higher-order translation}
% %
As we shall see this translation manipulates the continuation
intricate ways; and since we maintain the interpretation of the
continuation as an alternating list of pure continuation functions and
effect continuation functions it is useful to define the `parity' of a
continuation as follows:
%
a continuation is said to be \emph{odd} if the top element is an
effect continuation function, otherwise it is said to \emph{even}.
%
The complete CPS translation is given in The complete CPS translation is given in
Figure~\ref{fig:cps-higher-order-uncurried}. In essence, it is the Figure~\ref{fig:cps-higher-order-uncurried}. In essence, it is the
same as the refined first-order uncurried CPS translation, although same as the refined first-order uncurried CPS translation, although
@@ -2932,6 +2940,11 @@ continuation construction and deconstruction); both
\eqref{eq:cps-admin-reduct-1} and \eqref{eq:cps-admin-reduct-2} \eqref{eq:cps-admin-reduct-1} and \eqref{eq:cps-admin-reduct-2}
reductions have been eliminated as part of the translation. reductions have been eliminated as part of the translation.
The elimination of static redexes coincides with a refinements of the
target calculus. Unary application is no longer a necessary
primitive. Every unary application dealt with by the metalanguage,
i.e. all unary applications are static.
\paragraph{Implicit lazy continuation deconstruction} \paragraph{Implicit lazy continuation deconstruction}
% %
An alternative to the explicit deconstruction of continuations is to An alternative to the explicit deconstruction of continuations is to