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ę.
reference-request
lo.logic
pl.programming-languages
type-theory
ct.category-theory
Neel Krishnaswami
źródło
źródło
Odpowiedzi:
Samson Abramsky i ja napisaliśmy artykuł na temat teorii dowodu kompaktowych kategorii z dwubroduktami.
Pomysły zostały później rozwinięte nieco dalej w tym rozdziale książki:
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.
źródło
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
źródło