Teoria dowodowa produktów dwubiegowych?

15

Kategoria ma dwuprodukty, gdy te same obiekty są zarówno produktami, jak i koproduktami. Czy ktoś badał teorię kategorii produktów dwubiegunowych?

Być może najbardziej znanym przykładem jest kategoria przestrzeni wektorowych, w których bezpośrednia suma i bezpośrednie konstrukcje produktu dają tę samą przestrzeń wektorową. Oznacza to, że przestrzenie wektorowe i mapy liniowe są nieco zdegenerowanym modelem logiki liniowej i jestem ciekawy, jak wyglądałaby teoria typów, która akceptuje tę degenerację.

Neel Krishnaswami
źródło
1
Może Cockett i Seely? Być może wprowadzenie do kategorii liniowych lub coś innego z math.mcgill.ca/~rags .
Dave Clarke,
Być może „bi-” w „bi-produktach” wprowadza w błąd: to nie jest jakaś 2-kategoryczna rzecz, to po prostu to, co dzieje się, gdy te same obiekty są zarówno produktami, jak i koproduktami (plus pewne warunki koherencji) w zwykłych kategoriach.
Neel Krishnaswami,
Może ich praca: FINITE SUM - LOGIC PRODUCT.
Dave Clarke,
Nieco zdegenerowany? Uważam, że identyfikacja produktów i koproduktów oznacza identyfikację obiektu początkowego i końcowego, które są zazwyczaj typami pustymi i singletonowymi, interpretowanymi odpowiednio jako trywialna fałsz i prawda. W logice liniowej myślę, że to zapada całą addytywną połowę logiki do operacji podwójnego działania z tożsamością, która unicestwia obie multiplikacje. Z drugiej strony fragment multiplikatywny wydaje się być bardziej konstruktywną połową logiki liniowej, więc może to prowadzi do czegoś interesującego ...
CA McCann,
3
@camccann: Matematyka jest poza logiką. W algebrze przemiennej obiekt początkowy i końcowy zwykle się zgadzają, podobnie jak koprodukty i produkty. Na przykład, trywialna grupa abelowa jest zarówno początkowa, jak i terminalna. Obiekt zarówno początkowy, jak i końcowy nazywany jest obiektem zerowym. Spójrz na kategorie abelowe, aby uzyskać intuicję, jak to wszystko działa.
Andrej Bauer,

Odpowiedzi:

8

Samson Abramsky i ja napisaliśmy artykuł na temat teorii dowodu kompaktowych kategorii z dwubroduktami.

Abramsky, S. i Duncan, R. (2006) „A Categorical Quantum Logic”, Struktury matematyczne w informatyce 16 (3). 10.1017 / S0960129506005275

Pomysły zostały później rozwinięte nieco dalej w tym rozdziale książki:

Duncan, Ross (2010) „Uogólnione sieci próbne dla kompaktowych kategorii z dwubroduktami” w Semantic Techniques in Quantum Computation, Cambridge University Press, str. 70--134 arXiv: 0903.5154v1

Pełne szczegóły są tam, ale krótka wersja jest taka, że ​​twoja logika jest niespójna, ponieważ masz zerowy dowód dla każdej implikacji, a reszta twoich dowodów jest równoważna z „matrycami”, gdzie wpisy macierzy są dowodami w dwubrodukcie -free część logiki. Mówiąc bez ostrzeżeń wymaganych do sprecyzowania, wynikowa kategoria dowodów jest kategorią wolnego dwubroduktu w pewnej kategorii aksjomatów.

Ross Duncan
źródło
Mały dodatek do powyższego: nie ma powodu do niepokoju, że traktujemy kategorie zwarte w przeciwieństwie do kategorii ogólnych. W rzeczywistości addytywne i multiplikatywne części tej logiki oddziałują raczej słabo. Części dotyczące produktów dwubiegowych powinny być przenoszone dość ogólnie.
Ross Duncan
7

Niewiele wiem o teorii kategorii, ale być może będzie to pomocne. Równania rządzące diagramami graficznymi dla kategorii produktów dwubiegunowych [Selinger] są dokładnie równoważne z tymi dla przepływów atomowych [Gundersen] w teorii głębokiego wnioskowania [Guglielmi], we fragmencie pozbawionym negacji. Te systemy dowodu są w naturalny sposób równoważne monotonicznemu rachunku sekwencyjnemu [Brunnler, Jerabek].

Niestety wydaje się, że istnieje niewiele linków do teorii kategorii w tym drugim obszarze.

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

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, strona 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
źródło
Wielkie dzięki! Jestem trochę zbyt zajęty, aby od razu śledzić referencje, ale wkrótce je zobaczę.
Neel Krishnaswami