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

Fix typo

Browse Source
This commit is contained in:
Daniel Hillerström
2020-09-27 16:03:34 +01:00
parent 4cbd62140a
commit 1aac25ed71
1 changed files with 15 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files

19
thesis.tex
View File

@@ -948,7 +948,9 @@ computation to syntactically \emph{appear in tail position}.
% %
\begin{itemize} \begin{itemize}
\item The body $M$ of a $\lambda$-abstraction ($\lambda x. M$) appears in \item The body $M$ of a $\lambda$-abstraction ($\lambda x. M$) appears in
tail position. tail position.
\item The body $M$ of a $\Lambda$-abstraction $(\Lambda \alpha.M)$
appears in tail position.
\item If $\Case\;V\;\{\ell\,x \mapsto M; y \mapsto N\}$ appears in tail \item If $\Case\;V\;\{\ell\,x \mapsto M; y \mapsto N\}$ appears in tail
position, then both $M$ and $N$ appear in tail positions. position, then both $M$ and $N$ appear in tail positions.
\item If $\Let\;\Record{\ell = x; y} = V \;\In\;N$ appears in tail \item If $\Let\;\Record{\ell = x; y} = V \;\In\;N$ appears in tail
@@ -2114,7 +2116,17 @@ not consume stack space.
\cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\ \cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\
\cps{V\,W} &=& \cps{V}\,\cps{W}\,k. \cps{V\,W} &=& \cps{V}\,\cps{W}\,k.
\end{equations} \end{equations}
\end{definition} \end{definition}
\[
\ba{@{~}l@{~}l}
\pcps{(\lambda x.(\lambda y.\Return\;y)\,x)\,\Unit} &= (\lambda x.(\lambda y.\lambda k.k\,y)\,x)\,\Unit\,(\lambda x.x)\\
&\reducesto ((\lambda y.\lambda k.k\,y)\,\Unit)\,(\lambda x.x)\\
&\reducesto (\lambda k.k\,\Unit)\,(\lambda x.x)\\
&\reducesto (\lambda x.x)\,\Unit\\
&\reducesto \Unit
\ea
\]
\section{Initial target calculus} \section{Initial target calculus}
\label{sec:target-cps} \label{sec:target-cps}
@@ -3807,8 +3819,7 @@ of the resumption construction primitive.
A major aesthetic improvement due to the generalised continuation A major aesthetic improvement due to the generalised continuation
representation is that continuation construction and deconstruction is representation is that continuation construction and deconstruction is
now uniform: only a single continuation frame is inspected at any now uniform: only a single continuation frame is inspected at a time.
time.
\subsubsection{Correctness} \subsubsection{Correctness}
\label{sec:cps-gen-cont-correctness} \label{sec:cps-gen-cont-correctness}