Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: theory: type theory

Topic: substructural logics

Nathanael Arkor (Apr 14 2020 at 17:23):

@Mike Shulman, @Mitchell Riley: I am trying to familiarise myself with your approach in A Fibrational Framework for Substructural and Modal Logics and I was wondering whether you would be happy to answer a couple of questions here? I'm not sure whether Zulip feels too informal for this sort of thing; let me know if you don't think this is an appropriate medium!
One question I had to begin with, to get a better understanding of the scope of this framework: are there any examples of substructural logics or related systems that this framework is unable to capture (at least in the form presented in the extended version of the paper)? It certainly seems to capture lots of useful examples, and I find it hard to tell what it does not cover (without considering, say, dependency, which I understand you are also currently working on).

James Wood (Apr 14 2020 at 17:56):

I'm not entirely familiar with that work, but I'm not sure whether it would handle a calculus of sensitivity analysis, as seen in Distance makes the types grow stronger.

James Wood (Apr 14 2020 at 18:00):

But maybe this could be done via (ℝ-many) modalities.

vikraman (Apr 14 2020 at 18:11):

I'm curious about this too, last summer I had asked Dan Licata and Mitchell whether one can use the structural transformations to express (graded) modalities that distribute over or cancel each other, but we never followed through.

sarahzrf (Apr 14 2020 at 23:50):

oh mitchell riley is here?! i completely missed that

Mike Shulman (Apr 15 2020 at 01:03):

Unfortunately I'm not familiar enough with the variety of substructural logics in the literature to really answer that question. One obvious answer is that it doesn't cover "classical" systems whose judgments have multiple conclusions as well as multiple antecedents, but that's really just a different class of theory (or "3-theory") analogous to dependent types. Given people's ingenuity in inventing weird type systems, I'd be surprised if there isn't some "intuitionistic" substructural logic not covered by our framework, but Dan or Mitchell could hopefully answer that better.

Mitchell Riley (Apr 15 2020 at 23:52):

Maybe one way to describe the "3-theory" that we're in is that, when you erase all the annotations, you end up with an underlying ordinary structural type theory. And the annotations just restrict you from using certain things in certain places. Perhaps focused logics are an example of something with an underlying structural type theory, but with weird enough rules that they don't fit?

Mitchell Riley (Apr 15 2020 at 23:55):

James Wood said:

But maybe this could be done via (ℝ-many) modalities.

I think you're right... It looks like the way to do it would be a mode $p$, a tensor $\otimes : (p, p) \to p$, and $\mathbb{R}$'s worth of mode morphisms $r : p \to p$. There would have to be a bunch of equations relating these things, e.g. composition of the $\mathbb{R}$ morphisms should correspond to addition, and we would need a kind of contraction $(r+s)(x) \Rightarrow r(x) \otimes s(x)$. We would have 2-cells $r \Rightarrow s$ whenever $r \geq s$, which would let us get their variable rule and weakening.

Then $\otimes$ and $!_r$ are the $\mathsf{F}$ types for the mode terms $\otimes$ and $r$. I am not so sure how the $\&$ type fits though... In a footnote they suggest that a version of BI might make $\&$ better behaved, perhaps there ought to be a second kind of context 'tensor' for it.

Mike Shulman (Apr 16 2020 at 00:05):

There's also a bit of wiggle room in what you mean by "fit". Some examples require more violence than others to shoehorn them into the framework. (-:

Nathanael Arkor (Apr 16 2020 at 00:05):

Hmm… I was trying to think of examples that may not necessary have an underlying cartesian context. For example, maybe something like fixed-length contexts or bounded-length contexts (e.g. single-variable contexts). Could these be expressed in the framework?

Nathanael Arkor (Apr 16 2020 at 00:06):

Or nonempty contexts, say.

Mike Shulman (Apr 16 2020 at 00:08):

Single-variable contexts should work: just give the underlying object in the mode theory no monoidal structure. And nonempty contexts should work by giving it a semimonoidal structure (no unit), while dually subsingleton contexts should work by giving it a unit morphism but no multiplication. I'm not sure what other kinds of fixed- or bounded-length contexts mean; for instance, if all contexts have length $\le 2$ then what happens when you try to cut two judgments whose contexts both have length 2?

Mike Shulman (Apr 16 2020 at 00:08):

If your source theory just disallows such cuts, then you might be able to encode it in the framework by just ignoring the results of such cuts (i.e. they're not in the image of the translation).

Nathanael Arkor (Apr 16 2020 at 00:10):

That's true: you'd have to permit a simultaneous substitution kind of cut, rather than single-variable (if it could work at all).