reperiendi

Continuation passing as a reflection

Posted in Category theory, Math, Programming by Mike Stay on 2007 December 21

We can write any expression like $f(g(x,y))$ as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:

$\begin{array}{ccccccc}&&ev\\&\swarrow&&\searrow\\f&&&&ev\\&&&\swarrow&&\searrow\\&&ev&&&&y\\&\swarrow&&\searrow\\g&&&&x\end{array}$

Figure 1: $f(g(x)(y))$

[In the caption of figure 1, the expression is slightly different; when using trees, it's more convenient to curry all the functions---that is, replace every comma "," by back-to-back parens: ")(" .]

The continuation passing transform (Yoneda embedding) first reflects the tree across the vertical axis and then replaces the root and all the left children with their continuized form—a value $x$ gets replaced with a function value $\overline{x} = (f \mapsto f(x)):$

$\begin{array}{ccccccc}&&&&\overline{ev}\\&&&\swarrow&&\searrow\\&&\overline{ev}&&&&f\\&\swarrow&&\searrow\\\overline{y}&&&&ev\\&&&\swarrow&&\searrow\\&&\overline{x}&&&&g\end{array}$

Figure 2: $\overline{\overline{ \overline{y}(\overline{x}(g)) } (f)}$

What does this evaluate to? Well,

$\begin{array}{rl} & \overline{\overline{ \overline{y}(\overline{x}(g)) } (f) }\\ = & \overline{f(\overline{y}(\overline{x}(g)))} \\ = & \overline{f(\overline{x}(g)(y))} \\ = & \overline{f(g(x)(y))} \end{array}$

As we hoped, it’s the continuization (Yoneda embedding) of the original expression. Iterating, we get

$\begin{array}{ccccccc}&&\overline{\overline{ev}}\\&\swarrow&&\searrow\\\overline{f}&&&&\overline{ev}\\&&&\swarrow&&\searrow\\&&\overline{ev}&&&&\overline{y}\\&\swarrow&&\searrow\\\overline{g}&&&&\overline{x}\end{array}$

Figure 3: $\overline{\overline{\overline{f}\left(\overline{\overline{\overline{g}\left(\overline{x}\right)}\left(\overline{y}\right)}\right)}}$

At this point, we get an enormous simplification: we can get rid of overlines whenever the left and right branch both have them. For instance,

$\overline{g}(\overline{x}) = \overline{x}(g) = g(x).$

Actually working out the whole expression would mean lots of epicycular reductions like this one, but taking the shortcut, we just get rid of all the lines except at the root. That means that we end up with

$\overline{\overline{f(g(x)(y))}}$

for our final expression.

However, if this expression is just part of a larger one—if what we’re calling the “root” is really the child of some other node—then the cancellation of lines on siblings applies to our “root” and its sibling, and we really do get back to where we started!

5 Responses

1. ccshan said, on 2007 December 25 at 7:55 am

The reflection you discovered is Filinski’s duality between call-by-value and call-by-name. A nice presentation (by far not the first one) is Wadler’s “Call-by-Value is Dual to Call-by-Name” (http://homepages.inf.ed.ac.uk/wadler/topics/call-by-need.html). I also discuss and present this duality (with delimited continuations) in my dissertation (http://www.cs.rutgers.edu/~ccshan/dissertation/book.pdf).

2. reperiendi said, on 2007 December 25 at 1:28 pm

ccshan: I’ve read Wadler’s paper, though I haven’t digested all of its implications yet. I’d like to understand how sending on a channel in the pi calculus is relalted to the call-by-name lambda calculus. There’s a paper on the “blue calculus” that combines the two.

I’ll have a look at your thesis to see if that clarifies anything for me.

3. reperiendi said, on 2007 December 27 at 2:47 pm

Just recording this for my own information:

Boudol’s blue calculus paper describes how to transform from the standard call-by-value lambda calculus to the call-by-name calculus, and then how to encode the result in the pi calculus.

Here’s the homomorphism between the call-by-name transformation (CBN) and the continuation passing transformation (CPT):

cf ⇒ :k uf
ugf ⇒  cf ug
uv ⇒ v (v is a variable)

where  is Unlambda‘s prefix application operator, c is whatever transformation we’re talking about, and u is a helper transformation. In CBN, :kx translates to “q ↦ def k = x in qk,” where q is a new variable. In CPT, :kx is the term “k ↦ `kx.”

In both cases, :kx is the continuization of x.

4. reperiendi said, on 2008 January 30 at 6:17 pm