Teoría de la prueba de biproductos?

15

Una categoría tiene biproductos cuando los mismos objetos son tanto productos como coproductos. ¿Alguien ha investigado la teoría de la prueba de categorías con biproductos?

Quizás el ejemplo más conocido es la categoría de espacios vectoriales, en la que la suma directa y las construcciones de producto directo dan el mismo espacio vectorial. Esto significa que los espacios vectoriales y los mapas lineales son un modelo ligeramente degenerado de lógica lineal, y tengo curiosidad por saber cómo sería una teoría de tipos que acepte esta degeneración.

reference-request lo.logic pl.programming-languages type-theory ct.category-theory Neel Krishnaswami
fuente
1
Tal vez Cockett y Seely? Tal vez Introducción a las bicategorías lineales, o algo más de math.mcgill.ca/~rags .
Dave Clarke
Quizás el "bi" en "biproductos" es engañoso: no es una cosa de 2 categorías, es lo que sucede cuando los mismos objetos son productos y coproductos (más algunas condiciones de coherencia) en categorías ordinarias.
Neel Krishnaswami
Quizás su papel: SUMA FINITA - LÓGICA DEL PRODUCTO.
Dave Clarke
Ligeramente degenerado? Creo que identificar productos y coproductos implica identificar el objeto inicial y el terminal, que generalmente son tipos vacíos y únicos, interpretados como falsedad trivial y verdad, respectivamente. En lógica lineal, creo que esto colapsa toda la mitad aditiva de la lógica en una operación auto dual con una identidad que aniquila ambas multiplicaciones. Por otra parte, el fragmento multiplicativo tiende a ser el medio más constructiva de la lógica lineal, así que quizás esto lo hace interesante en algún plomo ...
CA McCann
3
@camccann: Hay matemáticas fuera de la lógica. En álgebra conmutativa, el objeto inicial y el terminal generalmente están de acuerdo, así como los coproductos y productos. Por ejemplo, el grupo trivial abeliano es inicial y terminal. Un objeto que es inicial y terminal se llama objeto cero. Eche un vistazo a las categorías abelianas para tener una idea de cómo funciona todo esto.
Andrej Bauer

Respuestas:

8

Samson Abramsky y yo escribimos un artículo sobre la teoría de la prueba de categorías compactas con biproductos.

Abramsky, S. y Duncan, R. (2006) "Una lógica cuántica categórica", Estructuras matemáticas en informática 16 (3). 10.1017 / S0960129506005275

Las ideas se desarrollaron un poco más adelante en este capítulo del libro:

Duncan, Ross (2010) "Redes de prueba generalizadas para categorías compactas con biproductos" en Técnicas semánticas en computación cuántica, Cambridge University Press, pp70--134 arXiv: 0903.5154v1

Los detalles completos están ahí, pero la versión corta es que su lógica es inconsistente, porque tiene una prueba cero para cada implicación, y el resto de sus pruebas son equivalentes a "matrices", donde las entradas de la matriz son las pruebas en el biproducto Parte libre de la lógica. Hablando sin las advertencias necesarias para hacer esto preciso, la categoría de pruebas resultante es la categoría de biproductos libres en alguna categoría de axiomas.

Ross Duncan
fuente
Una pequeña adición a lo anterior: no hay necesidad de alarmarse por el hecho de que tratamos las categorías compactas en lugar de las categorías generales. De hecho, las partes aditivas y multiplicativas de esta lógica interactúan bastante débilmente. Las partes relativas a los biproductos deben trasladarse de manera bastante general.
Ross Duncan
7

No sé mucho sobre teoría de categorías, pero quizás esto sea útil. Las ecuaciones que rigen los diagramas gráficos para las categorías de biproductos [Selinger] son ​​exactamente equivalentes a las de los flujos atómicos [Gundersen] en la teoría de prueba de inferencia profunda [Guglielmi], en el fragmento libre de negación. Estos sistemas de prueba son equivalentes al cálculo secuencial monótono de forma natural [Brunnler, Jerabek].

Desafortunadamente, parece haber pocos enlaces trazados a la teoría de categorías en esta última área.

Selinger, P. www.mscs.dal.ca/~selinger/papers/graphical.pdf, página 45.

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, página 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
fuente
¡Muchas gracias! Estoy demasiado ocupado para seguir las referencias de inmediato, pero las veré pronto.
Neel Krishnaswami