<p>I think your looking for <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7604">Back to Direct Style</a> by Olivier Danvy</p>

CC BY-SA 3.0
2013-09-04T08:19:11.537Z
This is just what I was looking for, thanks!
Neel Krishnaswami
CC BY-SA 3.0
2013-09-03T19:37:17.880Z
2013-09-03T19:37:17.880Z
eaubin
<p>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).</p>

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

CC BY-SA 3.0
2013-09-03T14:51:06.947Z
2013-09-03T14:51:06.947Z
cody
<p>A quick Google search didn't turn up anything obvious, so I'm asking here. </p>

<p>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". </p>

CC BY-SA 3.0
2013-09-03T10:07:14.083Z
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$?
Martin Berger
CC BY-SA 3.0
2013-09-03T10:47:08.297Z
Yes, that's right. I have $P$, and want a $Q$.
Neel Krishnaswami
CC BY-SA 3.0
2013-09-03T14:07:32.957Z
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](http://www.sussex.ac.uk/Users/mfb21/publications/cw04/index.html).
Martin Berger
CC BY-SA 3.0
2013-09-03T15:09:52.003Z
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.
Neel Krishnaswami
CC BY-SA 3.0
2013-09-03T15:23:33.807Z
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.
Martin Berger
CC BY-SA 3.0
2013-09-04T08:20:25.340Z
@MartinBerger: I've never looked at full abstraction results in much detail, and your comment gives me a nice entry into them. Thanks!
Neel Krishnaswami
CC BY-SA 3.0
2013-09-04T12:05:43.263Z
Let me know if you have questions about this, at the beginning of the last decade I spent several years doing little else, and need to be coming back to this work soon.
Martin Berger
<pl.programming-languages><continuations><cps-transforms>
Reversing the CPS transformation?
Neel Krishnaswami
# Reversing the CPS transformation?

(Asked by: username_0 on 2013-09-03)

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".

**Tags:** pl.programming-languages, continuations, cps-transforms

> **Comments:**
> **username_1**: 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$?  
> **username_0**: Yes, that's right. I have $P$, and want a $Q$.  
> **username_1**: 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](http://www.sussex.ac.uk/Users/mfb21/publications/cw04/index.html).  
> **username_0**: 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.  
> **username_1**: 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.  
> **username_0**: @MartinBerger: I've never looked at full abstraction results in much detail, and your comment gives me a nice entry into them. Thanks!  
> **username_1**: Let me know if you have questions about this, at the beginning of the last decade I spent several years doing little else, and need to be coming back to this work soon.  

---

## 2 answers

### Answer by username_2 on 2013-09-03. Score: 5 | Accepted answer

I think your looking for [Back to Direct Style](http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.10.7604) by Olivier Danvy

> **Comments:**
> **username_0**: This is just what I was looking for, thanks!  

---

### Answer by username_3 on 2013-09-03. Score: 3

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.


---

