From 4cbd62140a82fb7e2cbe31614e4fa3dd04d611f6 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Daniel=20Hillerstr=C3=B6m?= <daniel.hillerstrom@ed.ac.uk>
Date: Thu, 24 Sep 2020 23:14:15 +0100
Subject: [PATCH] Properly tail-recursive CPS definition.

---
 thesis.bib | 12 +++++++++++-
 thesis.tex | 13 +++++++++++++
 2 files changed, 24 insertions(+), 1 deletion(-)

diff --git a/thesis.bib b/thesis.bib
index 9aca4ab..541a2d2 100644
--- a/thesis.bib
+++ b/thesis.bib
@@ -579,6 +579,15 @@
   year      = {1992}
 }
 
+@phdthesis{Danvy06,
+  author = {Olivier Danvy},
+  school = {Aarhus University},
+  title = {An Analytical Approach to Programs as Data Objects},
+  type = {{DSc} thesis},
+  year = 2006,
+  address = {Aarhus, Denmark}
+}
+
 @book{Appel92,
   author    = {Andrew W. Appel},
   title     = {Compiling with Continuations},
@@ -874,7 +883,8 @@
   school = {Universit{\'e} Paris 7},
   title = {Interpr{\'e}tation fonctionnelle et {\'e}limination des coupures de l'arithm{\'e}tique d'ordre sup{\'e}rieur},
   type = {PhD thesis},
-  year = 1972
+  year = 1972,
+  address = {Paris, France}
 }
 
 @inproceedings{Reynolds74,
diff --git a/thesis.tex b/thesis.tex
index e9dac94..b1c873f 100644
--- a/thesis.tex
+++ b/thesis.tex
@@ -24,6 +24,8 @@
 \usepackage[T1]{fontenc}      % Fixes issues with accented characters
 %\usepackage{libertine}
 %\usepackage{lmodern}
+%\usepackage{palatino}
+% \usepackage{newpxtext,newpxmath}
 \usepackage[activate=true,
     final,
     tracking=true,
@@ -2102,6 +2104,17 @@ not consume stack space.
 \dhil{Justify CPS as an implementation technique}
 \dhil{Give a side-by-side reduction example of $\dec{fac}$ and $\dec{fac}_{\dec{cps}}$.}
 \dhil{Define desirable properties of a CPS translation: properly tail-recursive, no static administrative redexes}
+%
+\begin{definition}[Properly tail-recursive~\cite{Danvy06}]
+ %
+  A CPS translation $\cps{-}$ is properly tail-recursive if the
+  continuation of every CPS transformed tail call $\cps{V\,W}$ within
+  $\cps{\lambda x.M}$ is $k$, where
+  \begin{equations}
+      \cps{\lambda x.M} &=& \lambda x.\lambda k.\cps{M}\\
+      \cps{V\,W} &=& \cps{V}\,\cps{W}\,k.
+    \end{equations}
+\end{definition}
 
 \section{Initial target calculus}
 \label{sec:target-cps}