Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
We should fill in CBV and CBN. Is this post a good start?
I would like to better understand the remark that says of F, “It is a positive computation type, with invertible elimination rule…”. I am very suspicious of this remark for the following reasons:
Computation types are negative (or at least, so I thought) — there is an account of CBPV as the natural deduction account of polarized intuitionistic logic, in which F and U are the up and downshift connectives respectively, and these are by definition respectively negative and positive.
Whether an elimination rule is invertible is neither here nor there when determining the polarity of a connective. Polarity arises from the invertibility of the left and right rules in (linear) sequent calculus.
The statement that F is positive and U is negative do refer to the invertibility of their elimination and introduction rules. Any stack out of $FA$ in cbpv is equivalent to one of the form $\bullet to x. M$ and any value of type $UB$ is equivalent to one of the form $thunk M$ and their other rules are not invertible: there are computations of $F A$ not equivalent to $return V$ (for instance one that prints a string before returning) and there are computations with free variable $x : UB$ that are not equivalent to $S[force x/\bullet]$ (for instance something that doesn’t use $x$ at all.
Re 1: Can you give a reference for a specific system of polarized intuitionistic logic so that I can see if I can make sense of this difference?
Re 2: Are you saying the notion of polarity only makes sense in the context of sequent calculus? And in this case the F and U types do not have the polarities I’ve described?
If so then what would you consider to be the correct description in CBPV? It is the case that in the semantics of CBPV all value connectives except U have a “mapping out” universal property, and U has a “mapping in” universal property, whereas all computation connectives except F have mapping in universal properties and F has a “mapping in” universal property. It was my understanding that this aspect of the semantics is what corresponds to polarity of connectives, but maybe you are saying that a logician would disagree with this?
Invertibility of intro and elimination rules is not a reliable way to measure polarity; but maybe you are meaning something completely different from what we mean by “invertibility” in structural proof theory and proof search. At least according to the sense that we mean by “invertibility of rules” in proof theory, not even disjunction would be positive if we looked at its natural deduction elimination rule.
Here’s some lecture notes on CBPV from Frank Pfenning: https://www.cs.cmu.edu/~fp/courses/15816-f16/lectures/21-cbpv.pdf. Well, he calls it CBPV, but it is just polarized intuitionistic logic; if you happen to be right about the polarity, then this mustn’t be actually CBPV. Note that in this presentation, you can’t really measure invertibility, because that is a property of sequent calculus. to see how the shift connectives work in polarized intuitionistic sequent calculus, see Rob Simmons’ paper: https://www.cs.cmu.edu/~rjsimmon/drafts/focus.pdf. Notice how in the sequent calculus, the upshift is negative and the downshift is positive. And this calculus is sound and complete for the calculus that Frank presents in CBPV note, and moreover, the rules in the CBPV note seem to be the same as CBPV a la Levy, modulo notation.
I’m saying that the easiest way to observe polarity of a connective is through sequent calculus, but there are other ways too which have to do with eta rules; IMO these are more subtle, and should actually be understood as arising from the more primitive notion of polarity that I describe. Mapping-in vs mapping-out in category theory doesn’t usually determine polarity, because in many categorical models, these are two presentations of the universal property of the same connective. (This corresponds to how in intuitionistic logic, there is not semantic distinction between the positive and the negative conjunction). Of course, in a sufficiently rarefied categorical model the real differences can be observed.
Anyway, I’m just feeling a little confused here and I’d like to square what I see in this post with my intuitions from structural proof theory, and what I’ve read in the work of Pfenning, Zeilberger, Munch, etc.
Ok it looks like I’m certainly using Positive/Negative differently from those papers, because they are defining that value type means positive and computation type means negative. I certainly don’t mean that F is a value type and U is a computation type.
I mean mapping in vs mapping out UP. For the F and U types there is certainly no ambiguity here that F has a mapping out UP and U has a mapping in UP.
Alright – I feel that there are still questions to figure out here, because in proof theory one cannot just declare by fiat that value types are “positive” and computation types are “negative”. The reason that assignment works out is semantical, and it seems to suggest to me that maybe there is some subtle difference in the adjunctions that we are considering. For instance, something I have never completely understood, is the fact that in some models of polarity, the up-shift and the downshift are left and right adjoints respectively, whereas in other models, they are right and left adjoints. I think Guillaume Munch would be the right person to explain it to us, since I never got far enough to understand those details fully. (And I’m not sure if this is related, I just thought I’d mention it, since it’s another subtlety.)
I’m not sure if that explains everything about our confusion here, but the difference in whether upshift is a right or left adjoint is explained in this paper by Guillaume: https://hal.inria.fr/hal-00996729 . Specifically section 3.2 constructs a duploid from a (unary) CBPV model (an adjunction) where the left adjoint is the upshift, and then section 3.4 describes the adjunction arising from a duploid where the upshift is a right adjoint.
The difference is that when upshift is a left adjoint, the adjunction is between the pure terms, i.e. values and stacks, and is the semantics for CBPV: the stack judgment F A |- B is naturally isomorphic to the value judgment A |- U B (Guillaume calls U G since U usually means a forgetful functor and any strong adjunction will do.
On the other hand, when upshift is a right adjoint, the adjunction is between effectful terms, i.e. CBV effectful terms between positive types and CBN effectful terms between negative types. If we look at a duploid arising from a CBPV adjunction, then this is an adjunction between the Kleisli $(A \to_{cbv} A' = A \to F A')$ and Co-Kleisli $(B \to_{cbn} B' = U B \to B')$ categories of the adjunction. Then $\Uparrow = F, \Downarrow = U$ at the level of objects, and the equivalence is $\Downarrow B \to_{cbv} A = U B \to F A = B \to_{cbn} \Uparrow A$.
So I guess the page should instead say the $F$ is a left adjoint and $U$ is a right adjoint rather than using polarity terminology.
I’m not following all the subtleties here, but are we still OK in our descriptions of negative type and positive type?
I’m not sure, I was going to bring that up as well
The first sentence of this entry started out as:
Call-by-push-value is a type theory and programming language which contains…
This does not seem to make (grammatical) sense.(?) I am assuming what is meant is something as follows (emphasis added):
Call-by-push-value is a type theory and programming language paradigm which subsumes
I have taking the liberty/chance to edit this accordingly. But if any expert is seeing this, please feel invited to adjust.
In fact, if such experts are around, it would be a great service if you could create the promised entries
which are referred to here and in a rather large number of other entries (see here and here) but which remain missing.
1 to 13 of 13