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: deprecated: Dialectica

Topic: Flavors of Dialectica

Eric Bond (May 03 2022 at 21:50):

I've run into a few different variations of Dialectica categories.
There's DC, GC, and Dial? (the one that is like a chu space and parameterized by a lineale).

It seems like GC makes the homs neater by removing the dependence on the input (U) in the second map (usually called F). And (Dial?) enriches the structure of the relation.

Could we get an overview of these variations with some comparisons and motivations?

Edit: I see this was partially answered in another thread. :)

Valeria de Paiva (May 03 2022 at 23:34):

Yes, different flavors.

the old names where only DC (morphisms are $(f:U\to V, F:U\times Y\to X)$ and GC morphisms are simplified to $(f:U\to V, F: Y\to X)$, both such that a condition on the relations is satisfied.

The version where the relation takes place in a lineale, instead of the Heyting algebra $2$ was described in the technical report above Categorical Multirelations, Linear Logic and Petri Nets.

At some stage DC was called DDial(C), and GC was called Dial_2(C).

some interesting possibilities arise from the generalizations for other categories that are not Set or are not cartesian closed. This is described in the TAC paper.

But then clearly you can have $Dial_L(C)$ where both $L$ and $C$ are parameters. and you can vary parameters as much as you want!

versions using different lineales $L$ were used for Petri nets with different kinds of edges: real numbers, integers, elements of 3, 4, Natural numbers with the opposite order, rates, probabilities, etc.

lots of flavors, as you can see.

Valeria de Paiva (May 03 2022 at 23:51):

Motivation for flavors:

The motivation for Petri nets was that petri nets usually have multiplicities: you need one engine, two fans and 25 special screws to make a scanner, say. so you relations have to count things.

The motivation for GC (as I said in the video) was to simplify the model of linear logic, as the G stands for Girard, it was his suggestion.

In the paper with Elena and Wilmer we have motivations for rates (chemistry stuff that Wilmer is keen on), integers (some negative edges cancel stuff), using $3$ instead of $2$ you can talk about guaranteed links, guaranteed lack of a link and I-don't-know links, as you have a ternary logic. Probablity stuff is good for guys that like fuzzy systems.

People who prefer algebra to Category Theory might like the algebraic versions Lineales: Algebraic Models of Linear Logic from a Categorical Perspective,

Applications to modelling state in imperative languages use GC plus the tensor product of DC, following the intuitions of Uday Reddy.

There are many other flavors, but I do not want to tire you out.

Valeria de Paiva (May 13 2022 at 14:08):

@Eric Bond wrote:

It seems like GC makes the homs neater by removing the dependence on the input (U) in the second map (usually called F).

well, "neater" depends on the person and on the time. As I mentioned this category GC was Girard's suggestion to get a model of classical LL. myself I've moved in the direction of considering the logic FILL, first described in

Full Intuitionistic Linear Logic (with Martin Hyland) APAL, 1993. https://www.sciencedirect.com/science/article/pii/0168007293901465 (official) https://www.cs.bham.ac.uk/~vdp/publications/fill.pdf (preprint)

you may want to stick with LL or ILL and not venture into the dark woods of multiple conclusion type theory.

I thought people might prefer the simplified hom-sets of GC, because they're more similar to Chu spaces and to Lafont-Streicher games.

And (Dial?) enriches the structure of the relation.

well, Dial is a generic name to cover a multitude of sins. the original A_N(C) for "autonomous" category generated by lineale N over cartesian category C, became Dial_L(C), when I generalized N (natural numbers) to lineale L. unfortunately I tend to use context to differentiate between Dial_L(C) Godel-style vs Girard-style. Godel-style and Girard-style have different pros and cons.

I am sorry, I'm not very good at naming things.

Nelson Niu (May 25 2022 at 04:17):

I'm only just now thinking about GC (actually just GSet for now), and I was curious about a little technicality—is it true that GSet would be equivalent to a subcategory of DSet...if not for the fact that GSet has a bunch of nonisomorphic objects $(\emptyset, X, \alpha)$, while in DSet all the $(\emptyset, X, \alpha)$'s are isomorphic? Or do we (should we?) explicitly exclude the $(\emptyset, X, \alpha)$ variations from GSet? Does this variation affect the structures available on GSet, or is it far too subtle to make much of a difference?

Valeria de Paiva (May 25 2022 at 04:33):

hi, no, I don't think so. the difference between GSets and DSets is greater than that: the symmetric monoidal structure of GSet (or LDialSet, as we're now calling it in the agda file) is very different from the one of DSets or (or DialSet).

The internal-hom gets simplified to $[A,B]_{GSet}= ([pos B^{pos A}]\times [dir A^{dir B}], pos A \times dir B, \beta^{\alpha})$
but the tensor product gets more complicated: the positions of $(A\otimes B)_{GSet}$ are simply $pos A\times pos B$ as before. but the directions form a ``cross-product" of sorts
$pos B^ {dir A} \times pos A^{dir B}$.

now coproducts work as expected $(pos A + pos B, dir A\times dir B, choose)$ and this is a normal coproduct, not a weak one. its unit is simply $(\emptyset, 1, choose)$, as expected.
EDIT: choose is a bad name, the underlying object is $0\times 1\cong 0$ so there's nothing to choose, it has to be the empty relation on the emptyset.

in $GSet$ we do have a par, a multiplicative disjunction, which does the cross product in the first component of the object. for this par, the uniti is $(1, 1, empty)$.