4
$\begingroup$

A quick Google search didn't turn up anything obvious, so I'm asking here.

Converting direct style programs to continuation-passing style is a well-studied program transformation. However, I'm interested in the reverse transformation -- I'd like to take a program in CPS, and convert it to direct-style. Obviously the identity trasnformation works, in a vacuous sense, but I'm interested in transformations that are "as direct-style as possible".

Improve this question
$\endgroup$
7
  • $\begingroup$ Am I understanding you correctly when I say that you want to transform to direct style programs $P$ such that $P = cps(Q)$ for some program $Q$? $\endgroup$ – Martin Berger Sep 3 '13 at 10:07
  • $\begingroup$ Yes, that's right. I have $P$, and want a $Q$. $\endgroup$ – Neel Krishnaswami Sep 3 '13 at 10:47
  • $\begingroup$ Up to what notion of equality in the target language are you working? If it's $\alpha$-equality, and you know the exact CPS transform used, shouldn't you be able to invert the translation? If you use some contextual notion of equality that doesn't work. But if you impose a suitable typing discipline, you can still read the terms back up to, $\beta\eta$ in the source language. This is the essence of the full abstraction results from $\lambda$-calculi into $\pi$-calculi. See for example our full-abstraction result here. $\endgroup$ – Martin Berger Sep 3 '13 at 14:07
  • $\begingroup$ Basically, I want to do a CPS-transform, perform some program optimizations, and then un-CPS-convert. I'm not too picky about the notion of equality -- I just want to see what the literature contains, since I'll probably have to adjust the results a bit to fit my situation. $\endgroup$ – Neel Krishnaswami Sep 3 '13 at 15:09
  • $\begingroup$ The completeness part of all full abstraction results involving a CPS transform (and that would be all $\pi$-calculus and most game semantics FA results from $\lambda$-calculi) do a reverse translation. If your optimisations don't change types, you should be able to use that technology. Typically the key step (often called "definability lemma" or something like that) involves type-structure. The details are highly sensitive to chosen notions of equality on source and target languages. $\endgroup$ – Martin Berger Sep 3 '13 at 15:23
5
$\begingroup$

I think your looking for Back to Direct Style by Olivier Danvy

Improve this answer
$\endgroup$
1
  • $\begingroup$ This is just what I was looking for, thanks! $\endgroup$ – Neel Krishnaswami Sep 4 '13 at 8:19
3
$\begingroup$

One possible answer would be: apply your CPS style program to the identity continuation, and perform symbolic evaluation of every $\beta$-redex. This should give a reasonable "direct-style" interpretation of your program, if there was not much $\lambda$-lifting (turning nameless functions into named top-level functions).

Note that this works for side-effect-free programs, I'm not so sure if there are side effects.

Improve this answer
$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.