Teoria da prova de bioprodutos?

15

Uma categoria possui biprodutos quando os mesmos objetos são os produtos e os coprodutos. Alguém já investigou a teoria da prova de categorias com bioprodutos?

Talvez o exemplo mais conhecido seja a categoria de espaços vetoriais, na qual a soma direta e as construções diretas do produto fornecem o mesmo espaço vetorial. Isso significa que os espaços vetoriais e os mapas lineares são um modelo ligeiramente degenerado da lógica linear, e estou curioso em como seria uma teoria de tipos que aceite essa degenerescência.

reference-request lo.logic pl.programming-languages type-theory ct.category-theory Neel Krishnaswami
fonte
1
Talvez Cockett & Seely? Talvez Introdução às categorias lineares, ou algo mais de math.mcgill.ca/~rags .
Dave Clarke
Talvez o "bi-" em "biprodutos" seja enganador: não é uma coisa bidimensional, é exatamente o que acontece quando os mesmos objetos são produtos e coprodutos (mais algumas condições de coerência) em categorias comuns.
Neel Krishnaswami
Talvez o trabalho deles: SOM FINITO - LÓGICA DO PRODUTO.
Dave Clarke
Um pouco degenerado? Acredito que identificar produtos e coprodutos implica identificar os objetos inicial e terminal, que são tipicamente vazios e singleton, interpretados como falsidade e verdade triviais, respectivamente. Na lógica linear, acho que isso derruba toda a metade aditiva da lógica em uma operação auto-dupla com uma identidade que aniquila as duas multiplicações. Por outro lado, o fragmento multiplicativo tende a ser o meio mais construtiva da lógica linear, então talvez isso faz interessante em algum lugar chumbo ...
CA McCann
3
@camccann: Existe matemática fora da lógica. Na álgebra comutativa, o objeto inicial e o terminal normalmente concordam, assim como os coprodutos e produtos. Por exemplo, o grupo abeliano trivial é inicial e terminal. Um objeto que é inicial e terminal é chamado de objeto zero. Dê uma olhada nas categorias abelianas para ter alguma intuição de como tudo isso funciona.
Andrej Bauer

Respostas:

8

Samson Abramsky e eu escrevemos um artigo sobre a teoria da prova de categorias compactas com produtos biológicos.

Abramsky, S. e Duncan, R. (2006) "A Logical Quantum Logic", Estruturas Matemáticas em Ciência da Computação 16 (3). 10.1017 / S0960129506005275

As idéias foram posteriormente desenvolvidas um pouco mais adiante neste capítulo do livro:

Duncan, Ross (2010) "Redes de prova generalizadas para categorias compactas com produtos biológicos" em Técnicas Semânticas em Computação Quântica, Cambridge University Press, pp70--134 arXiv: 0903.5154v1

Os detalhes completos estão lá, mas a versão curta é que sua lógica é inconsistente, porque você tem uma prova zero para todas as implicações, e o restante das suas provas é equivalente a "matrizes", onde as entradas da matriz são as provas no biproduto parte livre da lógica. Falando sem as ressalvas necessárias para tornar isso preciso, a categoria de provas resultante é a categoria de bioproduto livre em alguma categoria de axiomas.

Ross Duncan
fonte
Um pequeno adendo acima: não há necessidade de se alarmar pelo fato de tratarmos categorias compactas em oposição a categorias gerais. De fato, as partes aditiva e multiplicativa dessa lógica interagem fracamente. As partes relativas aos bioprodutos devem transitar de maneira geral.
Ross Duncan
7

Não sei muito sobre teoria das categorias, mas talvez isso seja útil. As equações que governam os diagramas gráficos para as categorias de bioprodutos [Selinger] são exatamente equivalentes às dos fluxos atômicos [Gundersen] na teoria da prova de inferência profunda [Guglielmi], no fragmento livre de negação. Esses sistemas de prova são equivalentes ao cálculo sequencial monótono de uma maneira natural [Brunnler, Jerabek].

Infelizmente, parece haver poucos links para a teoria das categorias nesta ú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
fonte
Muito obrigado! Estou um pouco ocupado demais para seguir as referências imediatamente, mas analisarei em breve.
Neel Krishnaswami