Jason (jcreed) wrote,
Jason
jcreed

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
Subscribe
  • Post a new comment

    Error

    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded 

  • 5 comments