## Continuation passing as a reflection

We can write any expression like as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:

*Figure 1: *

[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 gets replaced with a function value

*Figure 2: *

What does this evaluate to? Well,

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

*Figure 3: *

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,

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

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!

ccshansaid, on 2007 December 25 at 7:55 amThe 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).

reperiendisaid, on 2007 December 25 at 1:28 pmccshan: 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.

reperiendisaid, on 2007 December 27 at 2:47 pmJust 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

`u`gf ⇒ ` `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.

reperiendisaid, on 2008 January 30 at 6:17 pmThis article got reposted on the n-Category Cafe

reperiendisaid, on 2008 January 30 at 6:24 pmNote how application is dual to composition. In fact, if we write (xy) for “apply x to y”, then the typical notation “f(x,y)” is ((fx)y) and “y(f(x))” is (y(fx)), exactly the reverse with no modifications.

How does this duality appear in string diagrams? Is there a well-known transformation like this in Feynman diagrams?