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.
Joseph Denman (Aug 04 2022 at 22:03):Attached are some diagrams I hope you'll be interested in. Those familiar with type theory will be familiar with aspects of the content, but, near as I can tell, the full translation is novel (aside from a passing mention in a paper from the 90s). They effectively summarize a correspondence between natural deduction in cut-elimination and 2-morphisms in a suitable bicategory, an extension of the Curry-Howard-Lambek correspondence that explicitly models the dynamics of the system of interest. This aspect of the computation/logic/category theory trichotomy is almost entirely unexplored. If they indicate what I think they indicate, then they point to a path to a categorical model of β-reduction in the simply typed λ-calculus that does not require equality between the redex and the reduct. More importantly, they point a path to a categorical semantics of reduction for any computational calculi enjoying a Curry-Howard-Lambek correspondence (e.g. session-typed π-calculus, dependently typed λ-calculus). I’m looking for co-authors for the paper I'm writing on the subject. Also, I have no idea what is in the commutative diagrams. Does anyone recognize it?
4BE028AC-9438-4811-8FC9-2F943DFDC81C.jpeg 7B5344E5-B1FB-4CB4-ADE6-6181DFB4709B.jpeg
The proof transformations are adapted from Philip Wadler's account of cut-elimination for the λ-calculus: https://homepages.inf.ed.ac.uk/wadler/papers/lineartaste/lineartaste-revised.pdf (pg. 8)
Joseph Denman (Aug 04 2022 at 22:04):@Christian Williams @Mike Stay
Joseph Denman (Aug 04 2022 at 22:06):If anyone is interested, we can schedule a call, and I can give you a brief tour of the translation, which has a satisfying recursive character.
Max New (Aug 04 2022 at 22:17):Have you seen R.A.G. Seely's paper from LICS 1987 "Modelling Computations: A 2-Categorical Framework"?
Joseph Denman (Aug 04 2022 at 22:29):@Max New Yes, That’s “the paper from the 90s.” The (conjectured) novelty here is that the diagrams I shared indicate what the logical counterpart of the reductions actually correspond to. Seely doesn’t identify the correspondence as an instance of a more general bicategorical framework.
Nathanael Arkor (Aug 05 2022 at 11:54):Have you seen @Philip Saville's thesis Cartesian closed bicategories: type theory and coherence?
Joseph Denman (Aug 05 2022 at 12:08):Thanks. I have, yes. I spoke with Philip a while back about this. He said, and I’m paraphrasing , that one issue with current bicategorical models of computation is that it’s not clear which direction the 2-morphisms could go. Phrasing 2-morphisms in terms of cut elimination provides both a direction and the logical correspondence.
Philip Saville (Aug 05 2022 at 13:52):I'm not sure what I said at the time (it's been a while!) but to my mind there is a canonical way for at least some of the morphisms to be directed: taking -reduction and an adjunction then makes it natural to take -expansion so that these become the unit and counit. If you're doing things fully bicategorically, so you also have 2-cells for substitution, then I agree it's less clear how to direct these -- but from a type-theoretic and rewriting-theoretic point of view those are more alien anyway.
Incidentally, I'm not confident enough reading logic to be sure what is in diagrams but one way to make sense of these kind of laws involving cut would be to look at bi-multicategories / biclones -- where the cut / composition correspondence is closer -- and then to translate into bicategories.
For another reference, Nicola Gambino and Marcelo Fiore have a grant working on 2-dimensional operads and related things. Part of their work with their post-docs is around 2-dimensional semantic models of linear logic, where I believe coherence poses some very subtle questions that don't occur in the cartesian closed case.
I'm always interested in more examples of 2-dimensional semantics, so happy to chat again!
Tom Hirschowitz (Aug 06 2022 at 10:54):Hilken's simply-typed 2--calculus may be relevant, have you seen it?
Joseph Denman (Aug 06 2022 at 16:29):Tom Hirschowitz said:
Hilken's simply-typed 2--calculus may be relevant, have you seen it?
I haven't! Thank you.
John Baez (Aug 06 2022 at 22:17):I discussed the 2-categorical approach to the lambda-calculus in my Fall 2006 and Winter 2007 seminar, and I have a bunch of lecture notes and references to look at. I refer to Hilken and Seeley's work.
John Baez (Aug 06 2022 at 23:32):I forget if anyone has mentioned this yet, about the direction of 2-cells:
Morgan Rogers (he/him) (Mar 08 2023 at 08:47):@William Troiani would be interested in this, I'll tell him to check all of these references :big_smile:
William Troiani (Mar 08 2023 at 10:39):Thanks Morgan, indeed this thread is very interesting to me.
Dan Murfet and I became interested in bicategorical semantics for linear logic when we set the goal of developing a general theory of "semantics of composition", inspired by work of Murfet's on the Landau-Ginzburg Category which had a finiteness problem involving composition. This finiteness problem was solved by considering so called "cut-systems" which are detailed in this paper: https://arxiv.org/pdf/1402.4541.pdf (see Section 1.1.3 for an explanation of where semantics comes in).
Since then, Murfet and myself have found what we call "Geometry of Interaction" models for multiplicative linear logic in coordinate rings (where cut-elimination is interpreted as the generation of Grobner bases from generating sequences of ideals, ie, the Buchburger Algorithm) and quantum error correction codes (where cut-elimination is interpreted as the error correction process). See https://arxiv.org/abs/2207.10871 for the former, the latter is still a work in progress, but see https://bbb.lipn.univ-paris13.fr/b/sei-nlh-8vr-xvy (scroll down).
It is clear that there are bicategorical semantics lurking in this work, but we have not explicated this yet. Either way, this is something which I have thought about a lot and would be very interested in collaborating on.