9

The definition is straightforward and can be found e.g. in (1, 2), see also (3). Here is a short summary, using a typed $\lambda$-calculus as basis. Types are not really needed for the presentation of reductions, but clarify the presentation in my opinion. Let's assume your language is given by the following grammar. $$ \newcommand{\PROGRAM}[1]{\mathsf{#1}} ...


7

When one associates negation with continuations, it is probably not ideal to think of it in terms of an 'empty' type. Continuation passing can be done with respect to any result type, and if that type is held abstract, it works a lot like 'false' in that there is no introduction rule for it. With respect to the paper you linked (I'm by no means an expert on ...


7

The closest I've seen to an answer to this question is the first picture in the Gallery of Doctor Melliès, illustrating the map $$\neg\neg A \otimes \neg\neg B \longrightarrow \neg\neg(A \otimes B)$$ which exists in any dialogue category (i.e., a monoidal category with closures into a fixed object). Note that the left-to-right CPS transform of general ...


5

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


4

Augmenting Noam's answer: Removing the implicit currying, $f : A \to B \to C$ is the same thing as $uncurry( f) : A \times B \to C$. Strong monads $T$ give a map (two, actually!): $dblstr : T A \times T B \to T (A\times B)$. We therefore have a map: $ T A \times T B \xrightarrow {dblstr} T(A\times B) \xrightarrow{uncurry(f)} TC $ If we instantiate this ...


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


1

I think you might be misreading those rewrite rules. A call to shift will find to the nearest enclosing call to reset, regardless of how deeply nested it is. Other examples in the tutorial you linked to should confirm that. The Racket Reference has a slightly different set of rewrite rules for reset/shift, that might make things a little clearer. (reset ...


1

The game you're describing is a continuous-time principal-agent problem. See A continuous-time version of the principal-agent problem (Sannikov 2008). Technically the goal there is to induce optimal effort from the employee, but, by the revelation principal, that's equivalent to having him reveal his private information.


Only top voted, non community-wiki answers of a minimum length are eligible