Teori bukti biproduk?

15

Suatu kategori memiliki biproduk ketika objek yang sama adalah produk dan produk ganda. Adakah yang menyelidiki teori pembuktian kategori dengan biproduk?

Mungkin contoh paling terkenal adalah kategori ruang vektor, di mana jumlah langsung dan konstruksi produk langsung memberikan ruang vektor yang sama. Ini berarti ruang vektor dan peta linier adalah model logika linear yang sedikit merosot, dan saya ingin tahu seperti apa bentuk teori yang menerima degenerasi ini.

reference-request lo.logic pl.programming-languages type-theory ct.category-theory Neel Krishnaswami
sumber
1
Mungkin Cockett & Seely? Mungkin Intro to Linear Bicategories, atau yang lain dari math.mcgill.ca/~rags .
Dave Clarke
Mungkin "bi-" dalam "bi-produk" menyesatkan: itu bukan sesuatu yang 2-kategorikal, hanya apa yang terjadi ketika objek yang sama adalah produk dan produk ganda (ditambah beberapa kondisi koherensi) dalam kategori biasa.
Neel Krishnaswami
Mungkin kertas mereka: FINITE SUM - LOGIC PRODUCT.
Dave Clarke
Sedikit merosot? Saya percaya mengidentifikasi produk dan produk menyiratkan mengidentifikasi mengidentifikasi objek awal dan terminal, yang biasanya jenis kosong dan tunggal, ditafsirkan sebagai kepalsuan dan kebenaran sepele, masing-masing. Dalam logika linier, saya pikir ini meruntuhkan seluruh bagian tambahan dari logika pada operasi self-dual dengan identitas yang memusnahkan kedua perkalian. Di sisi lain, fragmen multiplikatif cenderung menjadi bagian yang lebih konstruktif dari logika linier, jadi mungkin ini mengarah ke suatu tempat yang menarik ...
CA McCann
3
@camccann: Ada matematika di luar logika. Dalam aljabar komutatif objek awal dan terminal biasanya setuju, serta produk dan produk. Sebagai contoh, grup abelian sepele adalah inisial dan terminal. Objek yang merupakan inisial dan terminal disebut objek nol. Lihatlah kategori abelian untuk mendapatkan intuisi tentang bagaimana semua ini bekerja.
Andrej Bauer

Jawaban:

8

Samson Abramsky dan saya menulis makalah tentang teori pembuktian kategori kompak dengan biproduk.

Abramsky, S. dan Duncan, R. (2006) "A Quantum Logic Categorical", Struktur Matematika dalam Ilmu Komputer 16 (3). 10.1017 / S0960129506005275

Ide-ide itu kemudian dikembangkan sedikit lebih jauh dalam bab buku ini:

Duncan, Ross (2010) "Generalized Proof-Nets untuk Kategori Compact dengan Biproducts" dalam Teknik Semantik dalam Komputasi Quantum, Cambridge University Press, pp70--134 arXiv: 0903.5154v1

Detail lengkap ada di sana, tetapi versi singkatnya adalah bahwa logika Anda tidak konsisten, karena Anda memiliki nol bukti untuk setiap implikasi, dan sisa bukti Anda setara dengan "matriks", di mana entri matriks adalah bukti dalam biproduct -gratis bagian dari logika. Berbicara tanpa peringatan yang diperlukan untuk membuat ini tepat, kategori pembuktian yang dihasilkan adalah kategori biproduct gratis pada beberapa kategori aksioma.

Ross Duncan
sumber
Tambahan kecil di atas: tidak perlu khawatir dengan fakta bahwa kami memperlakukan kategori kompak sebagai lawan dari kategori umum. Faktanya bagian aditif dan multiplikatif dari logika ini berinteraksi agak lemah. Bagian-bagian mengenai biproduk harus terbawa secara umum.
Ross Duncan
7

Saya tidak tahu banyak tentang teori kategori, tetapi mungkin ini akan membantu. Persamaan yang mengatur diagram grafis untuk kategori biproduk [Selinger] persis sama dengan yang untuk aliran atom [Gundersen] dalam teori bukti inferensi mendalam [Guglielmi], dalam fragmen bebas negasi. Sistem bukti ini setara dengan kalkulus sekuens monoton dengan cara alami [Brunnler, Jerabek].

Sayangnya tampaknya ada beberapa tautan yang ditarik ke teori kategori di bidang terakhir.

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

Gundersen, T. tel.archives-ouvertes.fr/docs/00/50/92/41/PDF/thesis.pdf, halaman 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
sumber
Terima kasih banyak! Saya agak terlalu sibuk untuk mengikuti referensi segera, tetapi saya akan segera melihatnya.
Neel Krishnaswami