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.
Henri Tuhola (Jun 01 2020 at 13:12):Plugging in proof nets visually resemble composition in category theory. Though proof nets require a "graphical criterion". I wonder how this connects to CT?
I recently came up with a variation of proof nets, attempting to solve control node accumulation problem of optimal reduction. http://boxbase.org/entries/2020/jun/1/cll-normaliser/
Though when trying to come up with notions of what is a valid structure, it's getting complicated. I wonder if there is something that'd help in determining that? I think that it'd be particularly useful to identify natural transformations in proof nets.
Jules Hedges (Jun 01 2020 at 13:30):I've seen some work on this where you view proof nets as a "shadow" (projection) of a higher dimensional diagram, and the roundtrip condition vanishes and becomes ordinary higher-ish category theory.... let me see if I can find the paper
Jules Hedges (Jun 01 2020 at 13:32):Pretty sure the paper I was thinking of is "surface proofs for nonsymmetric linear logic" by Dunn and Vicary: https://arxiv.org/abs/1701.04917
Amar Hadzihasanovic (Jun 01 2020 at 15:58):Roughly, the graphical criterion comes from the following:
The “natural” categorical semantics of MLL natural deduction -- in “representable *-polycategories” -- is partially non-algebraic, in the sense that the 'minimal' model containing only valid proof-objects is not given by “composites of certain generators/diagrams, quotiented by certain relations”.
Proof nets are one way of “algebraicising” things, by introducing both 'new ways of composing things' and 'new generators', so that to each proof it is possible to assign a unique proof-object, but now there's also spurious proof-objects.
The “acyclicity” criterion corresponds roughly to preventing misuse of the new compositions and the “connectedness” criterion to preventing the use of the new generators to connect things that would not otherwise be connected (sorry this is quite handwavy).
You can think of the following as an analogy: the theory of fields is non-algebraic because the operation of multiplicative inversion is not total. But you can decide to throw in a formal inverse of 0, and go about proving things about this “algebraicised” version of a field (these are called 'meadows' if I recall correctly). For your proofs to be valid for fields, however, you would have to use some “correctness criterion” ensuring that you have never made essential use of the inverse of 0.
Amar Hadzihasanovic (Jun 01 2020 at 16:02):So you may want to try to follow this pattern for whatever application you are thinking of: find a 'natural' semantics for your proofs which may involve non-algebraic operations such as factorisations of diagrams, then “algebraicise” and see if you can exclude the spurious proof-objects that you end up creating by some combinatorial criterion.
Henri Tuhola (Jun 01 2020 at 16:28):So if I start with sum type, for indexing the type would be: (a+b | ~a), then I'd have to write down how this interacts with ((~a & ~b) | a | b). After that build up the constraints. Well that's true. It's a good idea to write those things down even if the actual criteria for validity is stricter than that.
Henri Tuhola (Jun 05 2020 at 15:19):Jules Hedges said:
Pretty sure the paper I was thinking of is "surface proofs for nonsymmetric linear logic" by Dunn and Vicary: https://arxiv.org/abs/1701.04917
I've drawn diagrams like in this paper when trying to examine normalisation in cartesian closed categories. The 2D diagrams lines represent functor morphisms and points are types.
Translations into proof nets present projections or "shadows" and capture the roundtrip condition. That's useful observation, but other than that I feel it doesn't bring out how to proceed after you've produced 3D surface diagrams from proofs.
Henri Tuhola (Jun 05 2020 at 15:39):I figured I can assign a justification "stack" for each edge. When they are connected, the justifications should match and when such justification is used, it pops off. Then the roundtrip condition captures the rest of validity conditions.
Though, it creates a very strict graph. It means that if I have two products that are interacting, then another of them splits into two, for each halve of the other product. But examining it closer, I don't think it would work without being strict in this way.
Henri Tuhola (Jun 11 2020 at 10:16):Ended up constructing a *-autonomous monoidal category and "validifier" for that in Haskell. https://gist.github.com/cheery/c19e0709d92f5ab50c7d7f9ac05235ec
So I got these two extremes now. I either have "easy to normalise" structures that are hard to verify correct, or then simple structures that are hard to normalise and hard to convert into proof nets&back, but otherwise easy to study.
Henri Tuhola (Jun 11 2020 at 10:24):If I start taking things "apart", I eventually arrive to the proof nets from there. But if I do so the checking for said structures becomes much harder.
Cole Comfort (Jun 11 2020 at 19:11):Henri Tuhola said:
Jules Hedges said:
Pretty sure the paper I was thinking of is "surface proofs for nonsymmetric linear logic" by Dunn and Vicary: https://arxiv.org/abs/1701.04917
I've drawn diagrams like in this paper when trying to examine normalisation in cartesian closed categories. The 2D diagrams lines represent functor morphisms and points are types.
Translations into proof nets present projections or "shadows" and capture the roundtrip condition. That's useful observation, but other than that I feel it doesn't bring out how to proceed after you've produced 3D surface diagrams from proofs.
The axioms for thinning links in Cockett and Seely's paper is so unintuitive and annoying. It really is more appropriate to think of the units in this higher dimensional setting, in my opinion.