Not signed in (Sign In)

Start a new discussion

Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

  • Sign in using OpenID

Discussion Tag Cloud

Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.

Welcome to nForum
If you want to take part in these discussions either sign in now (if you have an account), apply for one now (if you don't).
    • CommentRowNumber1.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013
    • (edited Dec 9th 2013)

    Following discussion in some other threads, I thought one should make it explicit and so I created an entry

    Currently this contains some (hopefully) evident remarks of what “dependent linear type theory” reasonably should be at least, namely a hyperdoctrine with values in linear type theories.

    The entry keeps saying “should”. I’d ask readers to please either point to previous proposals for what “linear dependent type theory” is/should be, or criticise or else further expand/refine what hopefully are the obvious definitions.

    This is hopefully uncontroversial and should be regarded an obvious triviality. But it seems it might be one of those hidden trivialities which deserve to be highlighted a bit more. I am getting the impression that there is a big story hiding here.

    Thanks for whatever input you might have.

    • CommentRowNumber2.
    • CommentAuthorMike Shulman
    • CommentTimeDec 9th 2013

    Could also link to indexed monoidal category, though I’m not sure where.

    • CommentRowNumber3.
    • CommentAuthorUrs
    • CommentTimeDec 9th 2013

    Thanks, right, i’ll cross link further in a moment. It would be good if we could link to closed ind. Mon. Cats.

    • CommentRowNumber4.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    Okay, am back online (the previous telegraphic message was from my phone).

    I have added to indexed monoidal category the paragraph

    If all the fibers are not just monoidal but closed monoidal categories and the base change morphisms are not just strong monoidal but also strong closed monoidal functors , then the indexed monoidal category is an indexed closed monoidal category (Shulman 12, theorem 2.14).

    If in addtion all fibers are symmetric monoidal one might also call this a system of Wirthmüller contexts of six operations. If furthermore all fibers have all duals, then this is also what should be called categorical semantics for dependent linear type theory.

    and added the Shulman12 references and made indexed closed monoidal category a redirect.

    Then to dependent linear type theory I have added at the relevant spot:

    Equivalently this is an indexed closed monoidal category with fiberwise duals.


    • CommentRowNumber5.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 10th 2013

    Something seems a little bit off here, at least terminologically. If dependent linear type theory is intended to mean that that the fibers are *\ast-autonomous categories, then this means something different from assuming the fibers have monoidal duals (the latter would be a special case). Star-autonomous categories have two symmetric monoidal products, \otimes and \wp, and “dual” in the sense of *\ast-autonomous categories means we have maps xx *\top \to x \wp x^\ast, x *xx^\ast \otimes x \to \bot that interact appropriately. If the monoidal products \otimes and \wp and monoidal units \bot and \top coincide, then we get duals in the sense of monoidal duals.

    I expect you simply don’t mean *\ast-autonomous categories here, but what I am accustomed to calling a compact closed categories (there are other adjectives that sometimes get used, such as “rigid” and “autonomous”, although I think these can refer to more refined situations which involve braidings and twists).

    • CommentRowNumber6.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    Personally, I think “linear type theory” should refer to any type theory without contraction and weakening, corresponding to any noncartesian monoidal category. Giraud’s original linear type theory corresponded to **-autonomous categories, but from an applied category-theorist’s point of view, **-autonomous categories are fairly rare.

    • CommentRowNumber7.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 10th 2013

    Mike: yes, I would agree with that; it’s just that the articles linear type theory, dependent linear type theory, etc. refer specifically to *\ast-autonomous categories, which is probably not really appropriate for the intended applications. “Linear logic” was invented by Girard, and then given categorical semantics in *\ast-autonomous categories, but somewhere along the line people found it useful to use the word “linear” more generally than that to refer to general symmetric monoidal contexts.

    • CommentRowNumber8.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    I even think that the more general meaning follows naturally from the original motivation for “linear”, which if I understand correctly is that each variable must appear exactly once in a term (as in f(x)=axf(x) = a x rather than g(x)=ax 2+bx+cg(x) = a x^2 + b x + c). Nothing in that explanation has to do with **-autonomy.

    I think sometimes people say “classical linear logic” to indicate the presence of an involutive “negation” (since ordinary classical logic has an involutive negation, unlike ordinary intuitionistic logic), which is the **-autonomous version, and “intuitionistic linear logic” when it is absent. It’s probably a bit misleading, but not too bad terminology.

    • CommentRowNumber9.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 10th 2013)

    Okay, thanks for the comments. I am happy about using “linear logic” in this more general sense, as this happens to be what arises in the applications that I keep talking about here. I just had thought I’d better stick with what seemed to me to be the established terminological conventions. But if it’s not, all the better. But notice that the old nnLab entry linear logic follows just this convention, too (or did follow, I have now edited the introduction there, too).

    At linear type theory I have now made the entry paragraph read as follows:

    Linear type theory is the linear logic-version of type theory. In the sense of (Seely 89, prop. 1.5), following (Girard 87), this is the internal language of/has categorical semantics in star-autonomous categories. But more generally linear type theory came to refer to the internal type theory of any possibly-non-cartesian symmetric closed monoidal category. Indeed, this still follows the original motivation for the term “linear” as introduced in (Girard 87), since the non-cartesianness of the tensor product means the absense of a diagonal map and hence the impossibility of functions to depend on more than a single (linear) copy of their variables.

    Is that better? Otherwise, please feel invited to edit, or else erase it and start afresh.

    • CommentRowNumber10.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013
    • (edited Dec 11th 2013)

    Following various recent discussion here, I have edited my pdf note a bit further, now it’s called

    I have allowed myself to link to this from dependent linear type theory and from integral transform. In fact I thought maybe it should rather be an nLab entry. Please regard it as such and don’t hesitate to criticize. Maybe eventually I’ll turn it into one.

    • CommentRowNumber11.
    • CommentAuthorMike Shulman
    • CommentTimeDec 10th 2013

    My impression is that there are still some circles in which “linear type theory” or “linear logic” refers by default to the **-autonomous sort. But I think the more general choice is now common enough not to be a radical departure, and it makes sense for the nLab.

    • CommentRowNumber12.
    • CommentAuthorUrs
    • CommentTimeDec 10th 2013

    I have added to dependent linear type theory in a new section Properties – The canonical co-modality a remark on how Girard’s “!!“-modality is canonically induced in dependent linear type theory.

    • CommentRowNumber13.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 10th 2013

    Thanks Urs (#10); this is looking better. I think any lingering dissatisfaction I may have is mostly to do with the state of linear logic – not your fault and not the focus of the present discussion! I hope to do some work on this a little later.

    • CommentRowNumber14.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 11th 2013
    • (edited Dec 11th 2013)

    Re Type-semantics for quantization, in Example 2.4,

    • XX and YY became X 1X_1 and X 2X_2
    • The Frobenius reciprocity equivalence has its AA and BB reversed with respect to Remark 2.3, making it a little harder to compare
    • The pullback on the right of the pasting law equivalence should be B× X 2AB \times_{X_2} A.

    Remark 2.6: has XX and AA.

    • CommentRowNumber15.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 11th 2013

    Typos

    • discuss a ageneral
    • embodies a higher analog integral transformations
    • CommentRowNumber16.
    • CommentAuthorUrs
    • CommentTimeDec 11th 2013

    Thanks for catching typos! (that example 2.4 had been quite a bit of a mess, admittedly) Have fixed them now, and have added an acknowledgement.

    • CommentRowNumber17.
    • CommentAuthorUrs
    • CommentTimeDec 22nd 2013

    The fact alone that linear logic is the internal language of tensor categories makes clear that it is related to quantum mechanics. There should be a wealth of literature on the relation of linear logic to quantum logic and quantum computing. I saw it stated that Girard himself in 1989 started playing with this. But I don’t seem to have found lots of good references on this relation yet. The following two I saw

    • Vaughan Pratt, Linear logic for generalized quantum mechanics, in Proc. of Workshop on Physics and Computation (PhysComp’92) (pdf, web)

    • Ugo Dal Lago, Claudia Faggian, On Multiplicative Linear Logic, Modality and Quantum Circuits (arXiv:1210.0613)

    Can anyone help with further pointers?

    I was asked to say what the stuff at Type-semantics for quantization (schreiber) may have to say about resolving old confusion about “interpretation of quantum mechanics” in terms of modern maths. That made me think that there might be more value hidden in reading the linear push-forwards f !f_! and f *f_\ast very explicitly as logical operations f\sum_f and f\prod_f.

    One might argue that this gives for instance a nice story of quantum interference in the path integral as follows:

    by the discussion at Type-semantics for quantization (schreiber) the path integral, as any other integral kernel, is essentially given by f !f_! hence by f\sum_f. So

    1. in non-linear logic we have: “there is a path”

    2. in non-linear homotopy type theory we have “the space of all paths and their phases”

    3. in linear homotopy type theory we have “the linear space of all paths and all their phases added up and interfered”.

    It’s clear from the formalism that this is indeed what is happening, but maybe the way to say what is going on here in everyday language can be further improved.

    • CommentRowNumber18.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013

    Ah, this reference here is good, should have known about that:

    • CommentRowNumber19.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 23rd 2013

    Regarding Girard, he has collected together some lectures in his book The Blind Spot.

    I like this idea of (linear) homotopy type theory allowing the expression of something puzzling in natural language, where a misconception comes from reading it out of context, literally in the case of covariance.

    • CommentRowNumber20.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013

    Thanks for the pointer to his Lectures on Logic! Interesting, Girard enjoys voicing strong opinion. (Not in each case is it fully clear to me what the polemic is aimed at, though.)

    In particular he indulges in trashing vonNeumann-style quantum logic and clearly means linear logic to be the right substitute.

    • CommentRowNumber21.
    • CommentAuthorUrs
    • CommentTimeDec 23rd 2013
    • (edited Dec 23rd 2013)

    Just for the record: the integral kernel construction in dependent linear type theory which is discussed in Type-semantics for quantization (schreiber) appears in a special case in Construction 4.0.7 of the recent

    • CommentRowNumber22.
    • CommentAuthorUrs
    • CommentTimeDec 24th 2013
    • (edited Dec 24th 2013)

    I have added an example 4.12 to Type-semantics for quantization which spells out how the Hopkins-Lurie notion of integration is directly a special case of the general abstract notion in dependent linear homotopy type theory.

    • CommentRowNumber23.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 24th 2013

    In the right entry of the diagram at 4.12 you have Func(Y,𝒳)Func(Y, \mathcal{X}).

    • CommentRowNumber24.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 24th 2013

    Also ’statetement’ in abstract.

    • CommentRowNumber25.
    • CommentAuthorUrs
    • CommentTimeDec 25th 2013

    Thanks! Fixed now.

    And happy Christmas to everybody here.

    • CommentRowNumber26.
    • CommentAuthorTodd_Trimble
    • CommentTimeDec 25th 2013

    Frohe Weihnachten!

    • CommentRowNumber27.
    • CommentAuthorDavid_Corfield
    • CommentTimeDec 25th 2013

    Merry Christmas!

    • CommentRowNumber28.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014
    • (edited Jan 5th 2014)

    A thought and a question, concerning examples of semantics for dependent linear type theory.

    Given a topos H\mathbf{H} and an object X𝒞X \in \mathcal{C}, write

    𝒞 XH /X X/ \mathcal{C}_X \coloneqq \mathbf{H}_{/X}^{X/}

    for the category of pointed objects in the slice of H\mathbf{H} over XX. Regard this as a closed symmetric monoidal category with the smash product X X\otimes_X \coloneqq \wedge_X.

    Then for f:XYf \colon X \longrightarrow Y any morphism in H\mathbf{H}, pullback f *:H /YH /Xf^\ast : \mathbf{H}_{/Y} \to \mathbf{H}_{/X} preserves pointedness and hence induces f *:𝒞 Y𝒞 Xf^\ast \colon \mathcal{C}_Y \to \mathcal{C}_X. Moreover, using that f *f^\ast preserves the Cartesian closed structure, that the pointed closed structure is a fiber product of that, and that in the topos colimits and hence the smash product are preserved by pullback, it follows that this f *f^\ast is strong closed monoidal.

    Also the functor f !:H /XH /Yf_! \colon \mathbf{H}^{/X} \to \mathbf{H}^{/Y} given by pushout restricts to 𝒞 X𝒞 Y\mathcal{C}_X \to \mathcal{C}_Y and provides a left adjoint to f *f^\ast. Finally it is clear that f *f^\ast preserves colimits. So that almost shows that we have

    (f !f *f *):𝒞 X𝒞 Y (f_! \dashv f^\ast \dashv f_\ast) : \mathcal{C}_X \longrightarrow \mathcal{C}_Y

    with f *f^\ast strong closed monoidal, hence satisfying Frobenius reciprocity. I’d just need to think more about the existence of f *f_\ast, since with 𝒞 X\mathcal{C}_X not locally representable the adjoint functor theorem is not quite immediate.

    In any case, to the extent to which I am not mixing things up, this must be standard. What would be a reference?

    • CommentRowNumber29.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 5th 2014
    • (edited Jan 5th 2014)

    Aren’t 𝒞 X\mathcal{C}_X and 𝒞 Y\mathcal{C}_Y locally presentable, so that f *f^\ast has a right adjoint iff it is cocontinuous?

    You can think of 𝒞 X\mathcal{C}_X with its forgetful functor 𝒞 XH/X\mathcal{C}_X \to \mathbf{H}/X as being the category of algebras in H/X\mathbf{H}/X for the monad 1+():H/XH/X1 + (-): \mathbf{H}/X \to \mathbf{H}/X, where 11 denotes the terminal object in the locally presentable category H/X\mathbf{H}/X. This monad is accessible, so the category of algebras is locally presentable.

    I don’t know of a specific reference in the literature for the facts you are after.

    (Edit: By “topos”, I took it you meant “Grothendieck topos”.)

    • CommentRowNumber30.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014

    Ah, thanks, Todd!

    I have given accessible monad a stand-alone entry to remember this fact, and also added it to Eilenberg-Moore category – local presentability. Cross-linked with topos of algebras over a monad.

    • CommentRowNumber31.
    • CommentAuthorUrs
    • CommentTimeJan 5th 2014

    Have now written out the content of #28 at Wirthmüller context – Examples – On pointed objects.

    • CommentRowNumber32.
    • CommentAuthorZhen Lin
    • CommentTimeJan 6th 2014

    Another fact (also non-trivial) is that over- and undercategories of accessible categories are accessible. More generally, if FF and GG are accessible functors, so is the comma category (FG)(F \downarrow G).

    • CommentRowNumber33.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014

    Okay, thanks. You should add that (best with proof and/or citation) to accessible category. Thanks!

    • CommentRowNumber34.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 6th 2014)

    Let’s see if we can further push the example of #28 with such technology.

    So in the context of #28 I am considering now furthermore an endofunctor :HH\oint \colon \mathbf{H} \to \mathbf{H} of which I assume that it preserves limits and colimits and has the structure of an idempotent monad (it is an infinitesimal shape modality).

    Then I want to consider the restriction of the adjoint triples (f !f *f *):H /X X/H /Y Y/(f_! \dashv f^\ast \dashv f_\ast) : \mathbf{H}_{/X}^{X/} \to \mathbf{H}_{/Y}^{Y/} to the full subcategories

    F XH /X X/ F_X \hookrightarrow \mathbf{H}_{/X}^{X/}

    on those objects in the slice over XX whose underlying morphism (EX)(E \to X) is sent to an equivalence by \oint.

    It is immediate to check that f !f_! and f *f^\ast preserve these subcategories. Also one can see that the inclusions F XH /X X/F_X \hookrightarrow \mathbf{H}_{/X}^{X/} preserve colimits. Therefore to see that also f *f_\ast restricts to the system of subcategories it would be sufficient to see that also F XF_X is locally presentable.

    Is it?

    • CommentRowNumber35.
    • CommentAuthorTodd_Trimble
    • CommentTimeJan 6th 2014

    I’m having trouble putting my hands on Makkai-Reyes at the moment, but I seem to recall they have even more general results, e.g., that the 2-category of accessible categories and accessible functors admits lax 2-limits.

    • CommentRowNumber36.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 6th 2014)

    I see in this discussion Richard Garner mentioning that pullback of accessible categories along isofibrations being again accessible.

    • CommentRowNumber37.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014

    Ah, this prop 3 at accessible category should answer #34 positively.

    • CommentRowNumber38.
    • CommentAuthorMike Shulman
    • CommentTimeJan 6th 2014

    Re: #28, two references (without proofs) are examples 12.13 and 13.7 of 0706.1286 and example 2.33 of 1212.3914. I don’t think you need an AFT for f *f_\ast, you should be able to just construct it by hand.

    • CommentRowNumber39.
    • CommentAuthorUrs
    • CommentTimeJan 6th 2014
    • (edited Jan 7th 2014)

    Thanks, Mike! That’s excellent.

    I have now added these pointers to your articles to Wirthmüller context – Examples – Pointed objects with smash product (and to my pdf note).

    Given this, might you have a comment on #34, too? Might something like this also be in your articles, or be a direct consequence of some statements there?

    I had tried to think for a bit about how to describe f *f_\ast here more explicitly , but then gave up. Probably I should try again.

    • CommentRowNumber40.
    • CommentAuthorMike Shulman
    • CommentTimeJan 7th 2014

    In #34, it’s easy to see by mates that if f *:F YF Xf^*:F_Y \to F_X has a right adjoint, then that right adjoint is the restriction of f *f_* iff the reflectors commute with the f *f^*s. I suspect that the latter condition should be sufficient for f *f_* to restrict to the FFs (hence be a right adjoint to f *:F YF Xf^*:F_Y \to F_X), but I don’t have time right now to verify it. (It should be true because if the reflectors commute with the f *f^*s, then we have a “reflective sub-indexed-category”, which should therefore be “closed under limits”, including the “indexed products” that are the f *f_*s.)

    • CommentRowNumber41.
    • CommentAuthorUrs
    • CommentTimeJan 28th 2014
    • (edited Jan 28th 2014)

    A question on (possible) terminology:

    given that a symmetric monoidal category serves as semantics for a fragment of linear type theory, what would be an incarnation in the logic/type theory literature of a (lax) monoidal functor?

    Specifically, given a dependent linear type theory Mod with underlying category of types H\mathbf{H}, and given any type XHX \in \mathbf{H}, then what would you logically/type theoretically make of a lax monoidal functor from XX-dependent types to XX-dependent linear types

    H /XMod(X) \mathbf{H}_{/X} \longrightarrow Mod(X)

    ?

    A functor of this form in itself is of the kind as appears in the Lawvere-ian interpretation of comprehesion as we just discussed recently in another thread. Now specifically for ModMod here a hyperdoctrine of linear types and for this functor being lax monoidal, does that remind you (anyone) of anything that has been considered from the point of view of logic/type theory?

    • CommentRowNumber42.
    • CommentAuthorMike Shulman
    • CommentTimeJan 28th 2014

    Yes, it’s the dependent version of the monoidal adjunction between linear/nonlinear types that gives rise to the ! modality on linear types.

    • CommentRowNumber43.
    • CommentAuthorUrs
    • CommentTimeJan 29th 2014
    • (edited Jan 29th 2014)

    Let me give you the concrete example that I have in mind – which does happen to have some similarity with the !-modality, so maybe there is something here; let me know if the following makes you see a useful connection:

    (Ah, I shouldn’t have said that generally I want the same context XX on both sides…)

    So with Joost I am looking at Jacob Lurie’s A Survey of Elliptic Cohomology and we are trying to relate this to some of the constructions that we have been exploring elsewhere.

    Consider, if you have a second, theorem 3.2 there, and specifically its proof. This is about functors T\mathcal{F}_T for suitable groups TT that take objects in an orbit category, hence some T/T 0T/T_0 in H /BT\mathbf{H}_{/\mathbf{B}T}, to Mod(M T)Mod(M_T) (for some type M TM_T) by pushing the tensor unit along a map M T 0M TM_{T_0} \longrightarrow M_T.

    According to the discussion in the middle of p. 25 this is monoidal. And according to the hints in section 5.1 there this is supposed to generalize to slices over types more general than of the form BT\mathbf{B}T.

    (The idea is that for XX a TT-space then the global sections of T(X)Mod(M T)\mathcal{F}_T(X) \in Mod(M_T) “are” the TT-equivariant elliptic cohomology of XX. )

    • CommentRowNumber44.
    • CommentAuthorUrs
    • CommentTimeFeb 9th 2014
    • (edited Feb 9th 2014)

    Here are some questions for Mike (most likely, but of course also for anyone else who feels like replying):

    • How much exactly does the coherence of the string diagram calculus in indexed monoidal categories that satisfy Frobenius reciprocity depend on Beck-Chevalley? As you emphasize in your article with Kate Ponto, you apply BC only to a few types of diagrams. Is there a point in considering the case where BC only holds for these?

    • Do you have a name for the case where we have Frobenius reciprocity but not Beck-Chevalley, and do you think it deserves one? I see in your articles you always assume BC and then later add reciprocity/projection formula. But for the purposes of quantization that I am looking into, I seem to only need Frobenius reciprocity to set up the process of quantization as such, and Beck-Chevalley I seem to only need then to prove that the resulting propagation functor is monoidal (from cobordisms to Mod(*)Mod(\ast)).

    • Do you have a word for the condition that an H\mathbf{H}-indexed monoidal category Mod()Mod(-) satsifies Mod(X×Y)Mod(X) Mod(*)Mod(Y)Mod(X \times Y)\simeq Mod(X) \otimes_{Mod(\ast)}Mod(Y) for X,YHX, Y \in \mathbf{H}, where on the right we have a suitable tensor product of “2-modules”, as it were, over Mod(*)Mod(\ast)? Do we maybe have some other good conditions that already imply this?

    • CommentRowNumber45.
    • CommentAuthorUrs
    • CommentTimeFeb 10th 2014
    • (edited Feb 10th 2014)

    Mike, I have another small question:

    By that crucial lemma 3.2 in your article with Kate Ponto, we know that (pullback and) dependent sum respects the external product.

    Now I would like to say that the adjunction counit is natural under this equivalence, hence that its component at some external product is the external product of its components.

    It’s probably dead simple…

    • CommentRowNumber46.
    • CommentAuthorMike Shulman
    • CommentTimeFeb 10th 2014
    • Yes, there is a point, and we even gave it a name (“indexed homotopy coproducts”). I think the only BC condition which is absolutely crucial for meaningfulness of the string diagram calculus is the one we called “commutativity with reindexing”, since it translates into an isotopy. But I can’t be precise about that, because we don’t have a coherence theorem for these string diagrams!

    • No, I don’t have a name for it.

    • No.

    • I think that’s basically the definition of mates.

    • CommentRowNumber47.
    • CommentAuthorUrs
    • CommentTimeFeb 11th 2014
    • (edited Feb 11th 2014)

    Thanks, in particular for the fourth! That helps.

    • CommentRowNumber48.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014

    Added to dependent linear type theory a pointer to the new

    and re-worked the Idea-section a little to reflect its existence.

  1. I haven’t read the paper very carefully yet, but the author seems to be unaware of CLF, which solved the problem of extending LLF with positive connectives (,1,!,\otimes,1,!,\exists). The ideas introduced by CLF were quite influential in some circles (particularly at CMU), so I think it would be worth adding a reference here (I could do that myself) to make people more aware of its existence.

    • CommentRowNumber50.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014

    Thanks, Noam!!

    Please do add a note to the nLab entry, I’d be most interested.

  2. okay, I added a note and a reference.

    • CommentRowNumber52.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • (edited May 2nd 2014)

    Thanks. I’d need to look into this further, but maybe you can quickly help me:

    Would the syntax of Pfenning06+WCFW03 be anything close to having semantics in indexed closed monoidal categories?

    How do you see Matthijs Vákár syntax in relation to that of Pfenning+WCFW03 ?

  3. I suspect that a semantics of CLF in indexed closed monoidal categories would be sound but not complete. One of the key ideas of CLF was to maintain a syntactic separation between negative (or “asynchronous”) and positive (or “synchronous”) types, with the positive fragment “encapsulated in a monad” as the abstract of that tech report says (it might be better to say that the two categories of types are related by an adjunction; note that this is a bit different from the idea of a “linear-non-linear adjunction”, since here both categories of types are linear). Formally, this separation is used in order to derive a very simple equational theory: terms are only quotiented by α\alpha-equivalence, together with a simple notion of “permutative conversion” which expresses that the monad is commutative (in fact this latter condition could be dropped and the theory would still hang together, but it is useful for the intended applications to modelling concurrency). Notice that I have not mentioned β\beta or η\eta! Those are not taken as axioms—rather, the type theory is structured to maintain the invariant that all terms are fully β\beta-reduced and η\eta-expanded. (This was a very innovative idea at the time, since it entirely side-stepped one of the traditional thorny issues in dependent type theory.)

    Since the monad/adjunction is actually present in the type theory (i.e., there is a corresponding type constructor), a complete semantics would presumably reflect this. Perhaps one could obtain a sound semantics in indexed closed monoidal categories by instantiating to the identity monad, though I haven’t checked this and don’t know if anyone else has.

    As for the paper by Vákár, well, it seems that he considers various different corners of the design space for “intuitionistic linear dependent type theory”. The specific theory ILDTT, though, does seem quite close to CLF in expressive power—in particular the restriction to types dependent on an intuitionistic context—and so I would be very interested if he could adapt his semantics to CLF (keeping in mind what I said above about the “missing monad”). This might help to resolve the conjectures listed on p.19, since these are precisely the kinds of issues which the CLF approach was designed to circumvent.

    • CommentRowNumber54.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014

    I see, thanks.

    Looks like somebody like RAG Seely is needed once more to come and sort out the syntax-semtantics relation cleanly.

    • CommentRowNumber55.
    • CommentAuthorUrs
    • CommentTimeMay 2nd 2014
    • (edited May 2nd 2014)

    Bas Spitters kindly points out that a dependent linear version of system L had once been considered in

    • Arnaud Spiwak, section 5 of A dissection of L, Logical Methods in Computer Science 1998 pdf

    Have now added a pointer (just a pointer) to that to the entry, too.

  4. Hi,

    Thank you for the pointer, Noam! Indeed, I completely missed the CLF paper. In general, I'm much more of a category theorist than a syntactician. Just having had a quick glance at the paper, both syntaxes do indeed look quite similar. Obviously, the CLF syntax has been designed with computation in mind, while what I wrote down was meant to be a bit more towards the pure maths side of things, hoping to find a correspondence with certain categories. In particular, it should be a fairly straightforward generalisation of (rather bare) dependent type theory so we can use it to obtain a game semantics for dependent types, by taking the natural interpretation in a category of games and strategies.

    I haven't been able to have a sufficient look at CLF and am still a bit daunted by all the 'weird symbols'. It is very nice to see, however, that a similar system has been developed that has a good syntactic metatheory. I'd be very interested to see as well if we can find a correspondence with some variant of my categorical semantics.

    Urs, regarding the syntax-semantics correspondence here: I think I have a pretty good idea of most of it. Perhaps things would be clearer to you if we have syntax in which the categorical aspect of comprehension is also modular? (I think all other things are modular in my syntax/semantics, basically.) I'd be happy to write down this syntax for you if that would clarify things. What you do is you just take an intuitionistic (non-dependent) type theory and a linear type theory in each intuitionistic context with substitution operations by intuitionistic terms that go from one linear type theory to the other. (Basically, this is a strict indexed symmetric multicategory.) Than you can add rules that allow you to glue linear types to intuitionistic contexts and linear terms to intuitionistic context morphisms. (This is your comprehension.) You get a conservative extension of my syntax that now also talks explicitly about intuitionistic terms. This is a real internal language for strict indexed symmetric multicategries (without/with comprehension). If you add tensor and I types to your syntax, you get the case of strict indexed symmetric monoidal categories.

    Thanks, Bas and Urs, for the pointer to Spiwak's paper. I also didn't know that one. Haven't properly looked at it, but, it seems it considers one particular quite rich system very thoroughly from the syntactic point of view. I'm hoping this'll answer some of my questions about the computational properties of the syntax. :-) On the other hand, it looks specifically classical (rather than intuitionistic) and therefore not so close to the categories we're interested in, but I may be wrong.

    I'm trying to finish some notes on the model in terms of coherence spaces, now. Hopefully, that should provide some intuition for people who are familiar with coherence spaces or domain theory. At least, I think it's quite an intuitive model, myself, that is reasonably faithful to capturing the essence of the syntax. Certainly much better than the 'free models' I briefly discussed in the paper. After I finish these notes, I'll return to the syntax. :-)

    Matthijs
    • CommentRowNumber57.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)

    Hi Matthijs,

    thanks, again, for dropping by, also here!

    I understand, and my only suggestion is that it would be useful — for readers, for “the community”, for purposes of references — to state the syntax/semantics equivalences that are clearly very clear to you personally also very clearly in text.

    Currently you have, somewhat hidden inside the proof of your theorem 9, a throwaway remark that the relevant fragment of your syntax is indeed the internal language of strict indexed symmetric monoidal categories. I missed this statement on first reading, and it is easy to miss, being inside the proof of another statement which is only fragmentarily related.

    A text on the syntax and semantics of dependent linear type theory I would ideally hope to have a tabulated list of the form:

    • the syntax for strict indexed symmetric monoidal categories is precisely A

    • the syntax for strict indexed closed symmetric monoidal categories is precisely A+B

    • the syntax for strict indexed symmetric monoidal categories with comprehension is precisely A+C

    • etc.

    Think of it this way: I would like to exapnd the table on the page relation between type theory and category theory by including entries with fragments of “dependent linear type theory” on the left and on the right pointers to the literature.

    In fact I’ll add a row to that table now, pointing to your article. But as it stands the reader may have a bit of trouble isolating the statement in your article (as I had, on first reading).

    • CommentRowNumber58.
    • CommentAuthorMatthijs Vákár
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)
    Thanks, Urs. I completely agree that I should probably rewrite the paper a bit to make it more readable. It started as my personal notes and was only a side part of my project, but I then realised that people might be interested so quickly typed it up to a form that others *might* be able to read it.

    In the next version I will make the suggested changes and generally move things from footnotes and proofs into actual statements in the paper. Also, the example isn't formulated optimally, now. (Although I already have a new version ready.) It, in fact, always has a comprehension. The construction is really taking the free linear predicate type theory on Set given a propositional linear type theory. (or coFree as it is right adjoint to the forgetful functor of evaluating a linear predicate type theory on Set at 1) I didn't explain this properly yet in the current version. This also explains (partly) why the example is so discrete.

    I'm not entirely sure yet, though, if I should go for the real internal language syntax... if I find time, I could add an appendix.

    Really appreciate the feedback. Thanks!
    • CommentRowNumber59.
    • CommentAuthorUrs
    • CommentTimeMay 5th 2014
    • (edited May 5th 2014)

    Okay, thanks. I really think it would be worthwhile, but I should say: don’t let me distract you too much from what I guess your advisor/coauthors would want you to do instead!

    While we are at it, here is a trivial typo which I spotted:

    • p. 10 in “Judgements”, below “…of the following six forms”:

      • the second line needs “σ\sigma” to be replaced by AA;

      • the third item needs a capitalization of the second “aa

    Another comment: I gather your discussion of comprehension in the linear dependent context is an elaboration on the observation that I had made here (and on p. 48 of “Quantization via Linear homotopy types”), right? I think your readers might really appreciate it if you made it clearer what is going on here. Presently your article jumps right into some fairly non-obvious syntax on p. 6 and p. 21, and I think the reader who doesn’t already know what you are after here will find this somewhat mysterious and unmotivated. (I may be very wrong here, after all I am not a logician and I realize that logicians are a very different species ;-) In footnote 18 you start giving what I would consider an actual explanation of what’s going on with comprehension here. Maybe some such explanation could be moved right to a prominent position in the main text, to help the reader follow you? Just an idea.

    • CommentRowNumber60.
    • CommentAuthorUrs
    • CommentTimeNov 11th 2014
    • (edited Nov 11th 2014)

    I am filling content into dependent linear type theory.

    Now it says the entry is locked by an anonymous. This used to be a spurious message appearing all the time in the old days, and was a bug. Now I am not sure. If anyone reading here is really editing then: please wait – I am in the middle of editing.

    • CommentRowNumber61.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2014
    • (edited Nov 12th 2014)

    Have edited a good bit more at dependent linear type theory. Will continue tomorrow.

    The main new addition so far is maybe that I added the definition of fundamental classes and of secondary integral transforms in terms of dependent linear type theory. Added also the example which shows (or states at least) that for parameterized modules this reproduces matrix calculus.

    Maybe I’ll further expand the included table twisted generalized cohomology in linear homotopy type theory – table now, but then I need to quit for today.

    • CommentRowNumber62.
    • CommentAuthorUrs
    • CommentTimeNov 12th 2014
    • (edited Nov 12th 2014)

    Have edited a bit more.

    I’ll have to leave it the way it is for the moment, have to rush off now. I am going to use part of this as a script for a talk to the type theory group at Paris-Diderot today, around Paul-André Melliès. My goal is to

    • first convince the audience that six-functor Yoga in Wirthmüller style is precisely what ought to be regarded as the semantics for dependent linear (homotopy-)type theory (i.e. any proposed syntax ought to have that as its semantics),

    • then to indicate that in such contexts one may elegantly axiomatize “secondary integral transforms”,

    • point out that these capture/generalize the exponential modality construction,

    • highlight that it is manifestly a path-integral-like construction

    • and finally to indicate that in the model of parameterized modules this gives matrix calculus,

    • and to claim that in the model of parameterized spectra it gives pull-push in bivariant tiwsted generalized cohomology.

    We’ll see how it works.

    (I’ll duly highlight Mike’s many contributions to this. )

    • CommentRowNumber63.
    • CommentAuthorUrs
    • CommentTimeNov 13th 2014
    • (edited Nov 13th 2014)

    Have added two new references to dependent linear type theory:

    Matthijs Vákár has new talk notes [2] expanding on his article [3] and Neelakantan Krishnaswami with Pierre Pradic and Nick Benton have an article in preparation [4].

    [2] http://users.ox.ac.uk/~magd3996/research/10-11-2014-Oxford-Linear%20dependent%20types.pdf

    [3] http://arxiv.org/abs/1405.0033

    [4] http://www.cs.bham.ac.uk/~krishnan/dlnl-paper.pdf

    • CommentRowNumber64.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 17th 2017
    • (edited Jul 17th 2017)

    Matthijs Vákár’s thesis is out, so I’ve added that to his page. I don’t know whether its separate strands supersede individual publications, such as the one in #48.

    • CommentRowNumber65.
    • CommentAuthorUrs
    • CommentTimeJul 17th 2017

    Thanks for the alert. I had not seen that yet.

    • CommentRowNumber66.
    • CommentAuthorMike Shulman
    • CommentTimeOct 26th 2017

    I wish I had time to read Vákár’s thesis carefully. It looks like he may be solving the problem in the non-homotopy case, specifying a syntax and a semantics and proving that they match up (p81):

    The structure we obtain is that of a strict indexed symmetric monoidal category with comprehension

    We also get a mention (p71):

    Although in the last while some suggestions have been made on the nLab and nForum of possible connections between the syntactic and semantic work, no account of the correspondence was published.

    (-:

    • CommentRowNumber67.
    • CommentAuthorDavid_Corfield
    • CommentTimeJul 2nd 2018

    I added this recent reference

    diff, v3, current

    • CommentRowNumber68.
    • CommentAuthorDavid_Corfield
    • CommentTimeOct 10th 2018

    After the “great split” where much of this page was sent over to indexed monoidal (infinity,1)-category, the links in

    What should be the categorical semantics of dependent linear type theory was discussed in (Shulman 08, Ponto-Shulman 12, Shulman 12, Schreiber 14)

    no longer work.

    A simple fix is possible, but without wishing to provoke the tensions which tend to arise in these parts from differences of opinion on the necessity for syntax when one speaks of a type theory, is the page due a make-over? Why was that quoted sentence in the section ’Syntax’ in any case?

    Alternatively we wait for the roll out of the LSR program when all modal dependent type theories will be given their proper setting.

    • CommentRowNumber69.
    • CommentAuthorMike Shulman
    • CommentTimeOct 12th 2018

    Yes, that sentence seems like it should probably be moved to the “Semantics” section.

Add your comments
  • Please log in or leave your comment as a "guest post". If commenting as a "guest", please include your name in the message as a courtesy. Note: only certain categories allow guest posts.
  • To produce a hyperlink to an nLab entry, simply put double square brackets around its name, e.g. [[category]]. To use (La)TeX mathematics in your post, make sure Markdown+Itex is selected below and put your mathematics between dollar signs as usual. Only a subset of the usual TeX math commands are accepted: see here for a list.

  • (Help)