tag:blogger.com,1999:blog-8068466035875589791.post5722588599357898069..comments2024-03-26T00:37:39.585-07:00Comments on Semantic Domain: Focusing is not Call-by-Push-ValueNeel Krishnaswamihttp://www.blogger.com/profile/06853898957395028131noreply@blogger.comBlogger14125tag:blogger.com,1999:blog-8068466035875589791.post-41330943729892640952017-11-07T16:49:45.207-08:002017-11-07T16:49:45.207-08:00Neel, should this post say instead that U is *righ...Neel, should this post say instead that U is *right adjoint* to F?Unknownhttps://www.blogger.com/profile/04807670051420769844noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-88457735814107526322016-05-19T12:52:08.838-07:002016-05-19T12:52:08.838-07:00Hi Steven, as an update to my comments above, I ca...Hi Steven, as an update to my comments above, I can now mention two relevant articles, [1] with Gabriel Scherer and [2] with Marcelo Fiore and Pierre-Louis Curien. The point of view of these articles is that CBPV and intuitionistic focusing are indeed based on the same model of higher-order computation with evaluation order.<br /><br />But claiming “Focusing is not Call-by-Push-Value” appeared to me a good reaction to the idea that they are the same. In fact, I would go even further than Neel. Although the two formalisms show striking similarities, they arise from very different perspectives (the study of normal forms for focusing, and monadic-style models for CBPV). Clarifying their resemblance and differences using formal comparisons, when they are already very similar formally, is missing the point. One cannot be satisfied by an explanation of CBPV as a form of weak focusing.<br /><br />In [1,2], we aim for a unified representation of the model of computation behind CBPV and intuitionistic focusing. But for this we need to be careful about further crucial distinctions. The most important is that polarities do not need to coincide with the focusing properties, but they do coincide with evaluation orders. In this approach, the structure of CBPV and (weak or strong) focusing can be recovered as various ways of eliminating binders in terms (corresponding to some monadic style, and to reduction to some normal forms). Thus, in line with Noam's comment, it means that one has to also introduce distinctions, between terms, that are traditionally collapsed, suggesting that we need new kinds of models, as he writes. In particular, I believe that everything in [1,2] should (linearity aside) fit within a theory of bi-cartesian closed (bi-)duploids [3] where “bi-cartesian closed” is currently being worked on, and the second “bi-” has yet to be investigated, but is strongly suggested by the syntax.<br /><br />[1] Polarised Intermediate Representation of Lambda Calculus with Sums, Proc. LICS 2015.<br /><br />[2] A Theory of Effects and Resources: Adjunction Models and Polarised Calculi, Proc. POPL 2016.<br /><br />[3] Models of a Non-Associative Composition, Proc FoSSaCS 2014.Anonymoushttps://www.blogger.com/profile/08742400757670657902noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-60599530949042450152016-05-12T07:15:27.777-07:002016-05-12T07:15:27.777-07:00Hi Neel, any update on these thoughts on focusing/...Hi Neel, any update on these thoughts on focusing/polarisation and CBPV? To be honest, I couldn't follow your entire argument. I did notice that back in 2012, Robert Harper made a comment that he and Paul though that focusing and CPBV were "essentially" the same thing.<br /><br />https://existentialtype.wordpress.com/2012/08/25/polarity-in-type-theory/#comment-1047Steven Shawhttps://www.blogger.com/profile/11062749001442886118noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-75305586855003914812015-01-25T16:51:36.586-08:002015-01-25T16:51:36.586-08:00Dear Paolo, although I don't recognize this pr...Dear Paolo, although I don't recognize this precise quote from my publications, I have indeed studied how CPS translations factor through abstract-machine-like calculi ("L" calculi) with polarities. This is not secret---I'll be happy to provide you with more detailed references in a private message---you can find it in my PhD thesis and my articles, along with other uses of abstract-machine-like calculi with polarities, as intermediate representations, not for compilers yet, but applied so far to logic and category theory, as well as programming languages (in Chapter III and to a certain extent Chapter IV).<br /><br />Moreover, in an upcoming article with Gabriel Scherer (which I expect won't remain "secret" for very long) we argue that abstract-machine-like calculi offer a principled reconstruction in direct style of CPS and defunctionalisation (you can read already Chapter I of my thesis for this perspective). This can be seen in the continuity of Danvy et al.'s works that relate abstract machines to CPS and defunctionalisation, and Hofmann and Streicher's work before them.<br /><br />In our article, a polarised abstract-machine-like calculus is used to model sums elegantly. The link with CBPV is meant to be that of a direct-style language for CBPV models---a precise correspondence is the subject of ongoing work (see already the Chapter II from my thesis).<br /><br />I hope this helps, and can only encourage you to integrate abstract-machine-like calculi in your investigations.Anonymoushttps://www.blogger.com/profile/08742400757670657902noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-37528203504768028832015-01-24T13:03:44.755-08:002015-01-24T13:03:44.755-08:00Since I'm interested in writing elegant compil...Since I'm interested in writing elegant compilers, I'm curious on how this line of work can be used to improve on CPS. I've recently read "A dissection of L" and talked with its author Arnaud Spiwack; he argues that System L makes for a good compiler intermediate language, and I believe the reason is similar to why CPS is a good language (sometimes better than ANF, see "Compiling with Continuations, continued") — apparently, System L is (secretly?) "the language of CPS" (I hear that's a quote from Guillaume Munch). I've recently run into advantages of a variant of CBPV over ANF, so I might just use both together.<br /><br />Now I'd like to see whether CBPV relates to polarized System L like ANF relates to CPS.Anonymoushttps://www.blogger.com/profile/04485097839438234853noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-89176006268622767332014-10-27T06:49:01.549-07:002014-10-27T06:49:01.549-07:00CBPV is less about restricting the arrow to take a...CBPV is less about restricting the arrow to take a positive on the left than saying that it is indeed possible to have a negative on the left provided that it is mediated by U. In other words negative computations can be passed as values too. This is probably what happens in the realizability semantics you are thinking about.<br /><br />Reacting to the blog post, it would probably help to relate focusing, weak focusing, CBPV, etc. if we had a calculus X of which we could say, in a formal way, "CBPV is an indirect denotational semantics of X", "(strong) focusing is the study of (eta-long and) beta-normal forms of X"... Then there probably would be no surprise about both the similarity and the differences between focusing and CBPV.Anonymoushttps://www.blogger.com/profile/08742400757670657902noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-66935174838308310822014-10-26T10:54:17.264-07:002014-10-26T10:54:17.264-07:00I suspect the observation that contexts in CPBV ar...I suspect the observation that contexts in CPBV are values may be rather shallowly based on the particular (common) choice of presentation. For example, you asked that arrow have a positive type on the left, but is that an essential choice, or couldn't we just as well work with a CPBV-style system taking a negative on the left of the arrow? When I played with this design space (in the context of definition of realizability truth and falsity values for simply-typed-lambda-calculus), I had the impression that either design choices were possible and corresponded to different flavors of this familiar connective -- just as focused variants of . If all connectives require positives in their negative occurences, then a representation with only values in the context is possible, but as soon as one of them takes a computation this property (coincidence) fades away.<br /><br />I've been trying recently to work out the relation between Guillaume Munch-Maccagnoni's polarized presentation of System L and focusing for sequent calculi. Guillaume insists on studying the untyped calculus first, and that is an interesting (and unusual to me) experience; (untyped) normal forms have a phase-alternating structure that seems strongly related to focusing, but one cannot enforce what Jason calls "full concentration" above without type information, so that would be another form of weak focusing. gaschehttps://www.blogger.com/profile/08857543004921424187noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-49754945197148877182014-10-21T18:02:37.641-07:002014-10-21T18:02:37.641-07:00Saying "recall the syntax of types" is a...Saying "recall the syntax of types" is a little confusing: I don't recall seeing any presentation of CBPV with a connective called ∧. Levy (1999) has a "Π", which is arguably an n-ary intersection with explicit intro and elim constructs, so I guess that's what you mean?<br /><br />(This doesn't affect the rest of your post, since it mentions neither ∧/Π (CBPV) nor ∧ (focusing)…)Joshua Dunfieldhttps://www.blogger.com/profile/13649077332425628410noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-1821971121979161272014-10-21T12:01:43.782-07:002014-10-21T12:01:43.782-07:00Yeah... I *think* I agree with Rob and Noam here. ...Yeah... I *think* I agree with Rob and Noam here. To try to put it succinctly, isn't the story here just that CBPV is "concentrating and positive-one-step-inverting" whereas Andreoli is "fully concentrating and inverting"? (and ordinary natural deduction is "concentrating on negatives and positive-one-step-inverting"?jcreedhttps://www.blogger.com/profile/06587572078416238811noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-40507125562261393502014-10-21T10:53:42.183-07:002014-10-21T10:53:42.183-07:00Didn't see that Neel was linking to me already...Didn't see that Neel was linking to me already. Headdesk, red-face, etc.<br /><br />I've trained myself out of thinking about weak focusing, because what Frank and I call weak focusing was designed to avoid a problem that Structural Focalization resolves gracefully. Thanks for bringing it up here, Noam, it seems quite relevant, since you naturally end up with a context of strictly positive propositions.<br /><br />And your point is well taken about Levy taking an equally expansive view of CPBV. That was a graceless comment on my part.Robhttps://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-14607460801437072542014-10-21T10:53:09.012-07:002014-10-21T10:53:09.012-07:00This comment has been removed by the author.Robhttps://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-48524834712704286612014-10-21T01:19:39.293-07:002014-10-21T01:19:39.293-07:00Yeah, I was going to make a similar comment, that ...Yeah, I was going to make a similar comment, that there is a concept of "weak focusing" (where the context is allowed to contain invertible hypotheses) which is a refinement of Andreoli's focusing, and that this is explained in your paper which Neel linked to. (I wouldn't go so far as to call this an "enrichment" of CBPV, because I think Paul Levy takes an equally broad view of what "CBPV" means.)<br /><br><br />I would also echo the sentiment that these distinctions should be further explored. From my perspective, one of the reasons why it is difficult to communicate in this area is that all of these distinctions (unfocused/focused/weakly-focused/etc) collapse in the traditional categorical models used to assign denotations to proofs, so we need new kinds of models.<br />Noamhttps://www.blogger.com/profile/09175792123472366590noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-34121465872772355962014-10-20T19:47:53.054-07:002014-10-20T19:47:53.054-07:00I didn't finish my thought... if you give your...I didn't finish my thought... if you give yourself freedom to halt pattern matching for positive values, you can make terms in the focused system look (and, I believe, behave) just like CPBV terms.<br /><br />I also meant to add in the end: there's much to the distinctions you've noticed in terms of programming that hasn't been sufficiently explored at all! But I think Structural Focalization makes a good bit of headway on the proof theory side of the problem by giving an account of hypothetical values and their discharge.Robhttps://www.blogger.com/profile/05106663398227635415noreply@blogger.comtag:blogger.com,1999:blog-8068466035875589791.post-25437439236245727022014-10-20T19:44:59.803-07:002014-10-20T19:44:59.803-07:00I believe you can account for this difference - an...I believe you can account for this difference - and see focusing as an enrichment of CPBV, iv anything - by generalizing your view of what focusing is to the account I finally worked out in Structural Focalization. That account allows hypothetical contexts with hypotheses x:N which are discharged by cut admissibility and hypotheses z:<P> which are discharged by regular-old-bog-standard-substitution (of values for hypotheses, no less!). There's an interesting observation which I don't understand the significance of, that cut admissibility only works in the presence of atomic positive hypotheses, but if give yourself freedom to halt pattern matching for positive values (the admissibility of which turns out to be an identity principle rule in structural focalization).<br /><br />I originally came about this observation not because of the differences between CBPV and the usual (Laurent-Zeilberger-Liang-Miller) account of focusing. Rather, it grew out of worry about the treatment of atomic propositions in focusing - you're forced to extend the grammar of focusing to allow x:N and z:p+. And out of three years that I spent trying to understand ~50 lines of Twelf code Frank wrote one night.Robhttps://www.blogger.com/profile/05106663398227635415noreply@blogger.com