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)

    Well I am certainly glad I saw Arrival so that I get the wug joke in http://languagelog.ldc.upenn.edu/nll/?p=29480#more-29480

  • (no subject)

    Saw "Arrival". It did have some nontrivial linguistics content, but it still felt kind of wrapped up in a discernible layer of Hollywood Woo. The…

  • (no subject)

    Had some dinner at Aliada with akiva and sasha and K, and afterwards saw Herzog's "Aguirre, the Wrath of God" in Socrates park. Enjoyably bleak.

  • Post a new comment


    Anonymous comments are disabled in this journal

    default userpic

    Your reply will be screened

    Your IP address will be recorded