Jason (jcreed) wrote,

Still kinda perplexed about what the [Polakow and Pfenning 2000] paper really means with respect to focusing and CPS as I understand them. I desperately want the moral to be something like

"you can rewrite every function type A → B to its CPS version A → (B ↠ #) ↣ #"

where you throw the continuation (B ↠ #) on the left, which then consumes its argument to the right... but this falls over because at some stage you'll want to construct a continuation (which only puts an ordered hypothesis A into the context) which calls a real function, which needs a real (unrestricted) value for an argument. It's even worse if you keep function-argument-values and intermediate-stack-values separate, as I did in my last twelf encoding.

And yet the twelf encoding seems to work! Bijectively, even! This suggests to me that there's some logic that describes the output of the translation, even if it isn't straightforward ordered logic, or at least it doesn't translate function types like I conjectured above. What's going on?
Tags: cps, logic, math

  • (no subject)

    Something that's bugged me for a long time is this: How many paths, starting at the origin, taking N steps either up, down, left or right, end up at…

  • (no subject)

    Still sad that SAC seems to end up being as complicated as it is. Surely there's some deeper duality between…

  • (no subject)

    I had already been meaning to dig into JaneSt's "Incremental" library, which bills itself as a practical implementation (in ocaml) of the ideas in…

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded