Théorie de la preuve des biproduits?

Une catégorie a des sous - produits lorsque les mêmes objets sont à la fois les produits et coproduits. Quelqu'un a-t-il étudié la théorie de la preuve des catégories avec des biproduits?

L'exemple le plus connu est peut-être la catégorie des espaces vectoriels, dans laquelle la somme directe et les constructions de produits directs donnent le même espace vectoriel. Cela signifie que les espaces vectoriels et les cartes linéaires sont un modèle légèrement dégénéré de logique linéaire, et je suis curieux de savoir à quoi ressemblerait une théorie des types qui accepte cette dégénérescence.

reference-request lo.logic pl.programming-languages type-theory ct.category-theory Neel Krishnaswami
la source

Peut-être Cockett & Seely? Peut-être Intro to Linear Bicategories, ou autre chose de math.mcgill.ca/~rags .

Dave Clarke

Peut-être que le "bi-" dans les "bi-produits" est trompeur: ce n'est pas quelque chose de 2 catégorique, c'est juste ce qui se passe lorsque les mêmes objets sont à la fois des produits et des coproduits (plus quelques conditions de cohérence) dans les catégories ordinaires.

Neel Krishnaswami

Peut-être leur article: FINITE SUM - PRODUCT LOGIC.

Dave Clarke

Légèrement dégénéré? Je crois qu'identifier des produits et des coproduits implique d'identifier l'objet initial et terminal, qui sont généralement des types vides et singleton, interprétés respectivement comme un mensonge et une vérité triviaux. En logique linéaire, je pense que cela réduit toute la moitié additive de la logique à une opération auto-double avec une identité qui annihile les deux multiplications. D'un autre côté, le fragment multiplicatif a tendance à être la moitié la plus constructive de la logique linéaire, alors peut-être que cela mène à un endroit intéressant ...

CA McCann

@camccann: Il y a des mathématiques en dehors de la logique. En algèbre commutative, l'objet initial et terminal sont généralement d'accord, ainsi que les coproduits et les produits. Par exemple, le groupe abélien trivial est à la fois initial et terminal. Un objet qui est à la fois initial et terminal est appelé un objet zéro. Jetez un œil aux catégories abéliennes pour avoir une idée de la façon dont tout cela fonctionne.

Andrej Bauer

Réponses:

Samson Abramsky et moi avons écrit un article sur la théorie de la preuve des catégories compactes avec des biproduits.

Abramsky, S. et Duncan, R. (2006) "Une logique quantique catégorique", Structures mathématiques en informatique 16 (3). 10.1017 / S0960129506005275

Les idées ont ensuite été développées un peu plus loin dans ce chapitre du livre:

Duncan, Ross (2010) "Generalized Proof-Nets for Compact Categories with Biproducts" in Semantic Techniques in Quantum Computation, Cambridge University Press, pp70--134 arXiv: 0903.5154v1

Les détails complets sont là, mais la version courte est que votre logique est incohérente, car vous avez une preuve zéro pour chaque implication, et le reste de vos preuves est équivalent à des "matrices", où les entrées de matrice sont les preuves dans le biproduit -free partie de la logique. Parlant sans les mises en garde nécessaires pour rendre cela précis, la catégorie de preuves résultante est la catégorie de biproduits gratuits sur certaines catégories d'axiomes.

Ross Duncan
la source

Un petit addendum à ce qui précède: il n'est pas nécessaire d'être alarmé par le fait que nous traitons les catégories compactes par opposition aux catégories générales. En fait, les parties additives et multiplicatives de cette logique interagissent plutôt faiblement. Les parties concernant les biproduits devraient reprendre de manière assez générale.

Ross Duncan

Je ne connais pas grand-chose à la théorie des catégories, mais cela sera peut-être utile. Les équations régissant les diagrammes graphiques pour les catégories de biproduits [Selinger] sont exactement équivalentes à celles des flux atomiques [Gundersen] dans la théorie de la preuve d'inférence profonde [Guglielmi], dans le fragment sans négation. Ces systèmes de preuve sont équivalents au calcul séquentiel monotone de manière naturelle [Brunnler, Jerabek].

Malheureusement, il semble y avoir peu de liens établis avec la théorie des catégories dans ce dernier domaine.

Selinger, P. www.mscs.dal.ca/~selinger/papers/graphical.pdf, page 45.

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, page 74.

Guglielmi, A. alessio.guglielmi.name/res/cos/

Brunnler, K. www.iam.unibe.ch/~kai/Papers/n.pdf

Jerabek, E. www.math.cas.cz/~jerabek/papers/cos.pdf

Anupam Das
la source

Merci beaucoup! Je suis un peu trop occupé pour suivre tout de suite les références, mais je les regarderai bientôt.

Neel Krishnaswami du