Prooftheorie von Bioprodukten?

Eine Kategorie hat Nebenprodukte, wenn dieselben Objekte sowohl Produkte als auch Nebenprodukte sind. Hat jemand die Proof-Theorie von Kategorien mit Bioprodukten untersucht?

Das vielleicht bekannteste Beispiel ist die Kategorie der Vektorräume, in der die direkte Summe und die direkte Produktkonstruktion den gleichen Vektorraum ergeben. Das heißt, Vektorräume und lineare Abbildungen sind ein leicht entartetes Modell der linearen Logik, und ich bin gespannt, wie eine Typentheorie aussehen würde, die diese Entartung akzeptiert.

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

Vielleicht Cockett & Seely? Vielleicht Intro to Linear Bicategories oder etwas anderes aus math.mcgill.ca/~rags .

Dave Clarke

Vielleicht ist das "Bi-" in "Bi-Produkten" irreführend: Es handelt sich nicht um eine 2-kategorische Sache, sondern nur darum, was passiert, wenn dieselben Objekte in normalen Kategorien sowohl Produkte als auch Koppelprodukte (plus einige Kohärenzbedingungen) sind.

Neel Krishnaswami

Vielleicht ihr Papier: FINITE SUM - PRODUCT LOGIC.

Dave Clarke

Etwas entartet? Ich glaube, dass das Identifizieren von Produkten und Koprodukten das Identifizieren des ursprünglichen und des endgültigen Objekts impliziert, die typischerweise leere und einzelne Typen sind, die als triviale Falschheit bzw. Wahrheit interpretiert werden. In der linearen Logik, denke ich, führt dies die gesamte additive Hälfte der Logik zu einer selbstverdoppelten Operation mit einer Identität, die beide Multiplikationen vernichtet. Auf der anderen Seite ist das multiplikative Fragment in der Regel die konstruktivere Hälfte der linearen Logik. Vielleicht führt dies zu interessanten Ergebnissen ...

CA McCann,

@camccann: Es gibt Mathematik außerhalb der Logik. In der kommutativen Algebra stimmen in der Regel das ursprüngliche und das terminale Objekt sowie Nebenprodukte und Produkte überein. Zum Beispiel ist die triviale abelsche Gruppe sowohl initial als auch terminal. Ein Objekt, das sowohl Anfangs- als auch Endobjekt ist, wird als Nullobjekt bezeichnet. Schauen Sie sich die abelschen Kategorien an, um eine Vorstellung davon zu bekommen, wie das alles funktioniert.

Andrej Bauer

Antworten:

Samson Abramsky und ich haben eine Arbeit über die Beweistheorie kompakter Kategorien mit Nebenprodukten geschrieben.

Abramsky, S. und Duncan, R. (2006) "A Categorical Quantum Logic", Mathematical Structures in Computer Science 16 (3). 10.1017 / S0960129506005275

Die Ideen wurden später in diesem Buchkapitel etwas weiterentwickelt:

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

Die vollständigen Details sind vorhanden, aber die kurze Version besagt, dass Ihre Logik inkonsistent ist, da Sie für jede Implikation einen Nullbeweis haben und der Rest Ihrer Beweise "Matrizen" entspricht, wobei die Matrixeinträge die Beweise im Biprodukt sind -freier Teil der Logik. Ohne die Vorbehalte zu äußern, die erforderlich sind, um dies zu präzisieren, ist die resultierende Kategorie von Beweisen die Kategorie der freien Nebenprodukte für eine Kategorie von Axiomen.

Ross Duncan
quelle

Ein kleiner Nachtrag dazu: Es besteht kein Grund zur Sorge, dass wir kompakte Kategorien im Gegensatz zu allgemeinen Kategorien behandeln. Tatsächlich interagieren der additive und der multiplikative Teil dieser Logik ziemlich schwach. Die Teile, die Bioprodukte betreffen, sollten ganz allgemein übertragen werden.

Ross Duncan

Ich weiß nicht viel über Kategorietheorie, aber vielleicht wird dies hilfreich sein. Die Gleichungen für die graphischen Darstellungen der Bioproduktkategorien [Selinger] entsprechen genau denen für die Atomflüsse [Gundersen] in der tiefen Inferenzbeweislehre [Guglielmi] im negationsfreien Fragment. Diese Beweissysteme entsprechen auf natürliche Weise der monotonen Folgerechnung [Brunnler, Jerabek].

Leider scheint es in letzterem Bereich nur wenige Verbindungen zur Kategorietheorie zu geben.

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

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, Seite 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
quelle

Danke vielmals! Ich bin ein bisschen zu beschäftigt, um den Referenzen sofort zu folgen, aber ich werde sie mir bald ansehen.

Neel Krishnaswami