added pointer to:

- Benoît Valiron, Steve Zdancewic,
*Finite Vector Spaces as Model of Simply-Typed Lambda-Calculi*, in:*Proc. of ICTAC’14*, Lecture Notes in Computer Science**8687**, Springer (2014) 442-459 [arXiv:1406.1310, doi:10.1007/978-3-319-10882-7_26, slides:pdf]

added pointer to:

- Anne Sjerp Troelstra,
*Lectures on Linear Logic*(1992) [ISBN:0937073776]

here and elsewhere

]]>added pointer to:

- Martin Hyland, Andrea Schalk,
*Glueing and orthogonality for models of linear logic*, Theoretical Computer Science**294**1–2 (2003) 183-231 [doi:10.1016/S0304-3975(01)00241-9]

Thanks. I have fixed that typo and also beautified the alignments a little (here)

]]>In the box at the start of ’Absence of weakening and contraction’ (here), the top right entry for semantics of cloning should have the arrow $\Gamma \times P \times P \to T$.

]]>fixed numerous occurrences of “relevant logic” to “relevance logic”

]]>I have expanded the Idea section:

In a new subsection “Absence of weakening and contraction” (here) I have added actual discussion of these inference rules and what it means when they are absent.

Then in “As a quantum logic” (here) I have used this to amplify the natural relation to quantum logic, in particular making explicit that

no contraction $\leftrightarrow$ no cloning

no weakening $\leftrightarrow$ no deleting

Ended this section with a comment highlighting the remarkable fact that the perspective on resource-availability has meanwhile been independently noted in quantum information theory (by people who mostly will have never heard of linear logic).

This then naturally leads over to the sub-section on resource availability (here). But I haven’t worked on that section yet. I find it needs a complete rewrite (because that whimsical example, which is its sole content, of “have cake $\vdash$ eat cake “, is of dubious value, at least as long as there is no serious example accompanying it.)

]]>added pointer to:

- Frank Pfenning,
*Linear Logic*lecture notes (1998) [pdf, webpage]

So is there some kind of base change adjoint triple between $Spectra/\mathbb{S}$ and $Spectra$?

All $E_{\infty}$-rings are $\mathbb{S}$-graded.

]]>Seeing that they have $\Omega^{\infty} E := \natural (\mathbb{S} \to E)$ and $\Sigma^{\infty} E := E \wedge \mathbb{S}$, then $! = \Sigma^\infty \Omega^\infty$ is like a variation on the store comonad,

$D X : X \rightarrow W \times [W,X].$ ]]>So won’t Synthetic Spectra via a Monadic and Comonadic Modality with its synthetic definitions of $\Sigma^\infty$ and $\Omega^\infty$ (Def. 3.14 and 3.17) be relevant to linear HoTT, and yet just a couple of references to linear logic.

]]>Another thread to dig out is this one unstable K(n)-homotopy theory.

Thoughts on $\Sigma^\infty \Omega^\infty$ as the comonad associated to the co-operad of co-commutative co-algebras.

]]>Thanks for digging out this old thread.

It’s good to come back to this topic after a long detour, now with a better idea of what the interesting base spaces are over which to parameterize linear types in view of quantum systems. The neeext step (at CQTS) will to actually program and then “run” (simulate) topological quantum gates as described here. Let’s see how that will work out…

]]>Interesting! Especially for me since my own small contribution to your paper (as you note in footnote 13) concerns Exp. 4.1, suggested in a comment here. I’ll see if I can make any further sense later.

]]>Have had a glance over the article in #24.

My impression is that at least the broad conceptual nature of the “linear/non-linear adjunction” there – i.e. (31) in the preprint, (30) in the published version (p. 10), realized in terms of coalgebras – coincides with that discussed in Sec. 4.2 of “Quantization via Linear Homotopy Types” (i.e. p. 47-48, esp. the canonical Exp. 4.1 given by forming suspension spectra), observing that suspension spectra canonically inherit comonoid structure (here: coring spectrum-structure) from the fact that forming suspension spectra is strong monoidal.

In fact, as recalled on that p. 47, there is a canonical linear/non-linear adjunction induced as soon as the linear type system in question is the global value of a dependent linear type system, and that then goes through comonoids in this sense as soon as the functor forming the dependent sum of the tensor unit ($X \mapsto \underset{X}{\sum} \mathbf{1}_X$) is strong monoidal.

Since the linear types in #24 do form a dependent system (not sure if this is made fully explicit there, at least in the final *dictionary* the adjective “dependent” seems to be missing on the left of the second row – and the word “bundle” might usefully complete the first row on the right), this canonical linear/non-linear adjunction should exist in that context, too, and probably coincides with the one that is given, up to unwinding of notation (I wonder if there is room to connect more to standard notation: after all, the yoga of six operations that provides models of dependent linear type theory originates in the example of quasi-coherent modules over schemes).

Thanks for the pointer. I don’t have much time to spare, lagging behind with preparing slides for upcoming talks (broadly on this topic, though), but I’ll try to take a look.

]]>So what’s going on in that reference in #24?

Our main technical contribution in this work is to resolve an old open question in the field of mathematical logic, which is to construct a model of linear logic — including the exponential modality — in the functorial language of Algebraic Geometry. By performing this construction in the present paper, we hope to integrate linear logic as a basic and very natural component in the current process of geometrization of type theory. The guiding idea here is that linear logic should be seen as the logic of generalised vector bundles, in the same way as Martin-Löf type theory with identity is seen today as the logic of spaces up to homotopy, formulated in the language of ∞-topos theory.

…

The idea of relating linear types and vector bundles already appears in the early work by Schreiber [Schreiber 2014] on quantization of pre-quantum field theory. The approach to linear homotopy types and stable ∞-categories of bundles developed there is quite different in style and spirit however, and it will be thus instructive to clarify the connection with the constructions of the present paper.

(This second paragraph in the printed version, rather than the preprint.)

Hmm,

]]>Our main purpose in the paper is to associate to every scheme $X$ a specific model of intuitionistic linear logic, where formulas are interpreted as generalised vector bundles, and where proofs are interpreted as suitable vector fields.

Added to references

- Paul-André Melliès,
*A Functorial Excursion Between Algebraic Geometry and Linear Logic*, in 37th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS) (LICS ’22), August 2–5, 2022, Haifa, Israel. ACM, New York, (doi:10.1145/3531130.3532488, pdf)

Noted that the reason the symbols matched the positive/negative grouping is because that’s how they were chosen

Anonymous

]]>Fix Bierman thesis link

Anonymous

]]>Re #20: I don’t think it’s that. I think Toby wants “categorial” to avoid a conflict with the model theorists’ usage of the word “categorical”. My own opinion is that we don’t need such deferment.

]]>Re #15: dictionaries list two different meanings for “categorical”, for example, Wiktionary says

Absolute; having no exception.

Of, pertaining to, or using a category or categories.

Clearly, the second meaning makes “categorical” perfectly appropriate here. I do not understand how or why the interpretation that “categorical” necessarily refers to 1 above, whereas “categorial” means 2, came to be.

]]>So I went ahead and wrote a comment on terminology myself: here (in a new section of the entry *categorical semantics*).

Maybe best to have any further discussion of this point there, in the thread for the entry on categorical semantics.

]]>Somebody please just add a discussion of terminology, conventions and issues to this entry – or better to *categorical logic* and then link to it from here.

It sure must look like typos to any outside reader: There was 16 “categorical” vs 4 “categorial” before Valeria’s latest edit, some next to each other, notably there was

- Categorial semantics. We discuss the categorical semantics…

I see from the edit history that the “categorial”s are Toby’s intentional ideosyncrasy. As per #15 I probably agree with the logic behind this, but if mathematical terminology were a matter of logic, most of it would be much different. The goal of an entry must be to communicate with the reader, not to irritate them.

But if we had a decent section “On terminology” at *categorical logic* we could link to this from the very top of all relevant pages – say: “On the terminology of ’categori(c)al’ in the following see at *categorical logic*. ” – and then the issue would be dealt with.