具有双积的紧范畴的广义证明网
Generalised Proof-Nets for Compact Categories with Biproducts
摘要：
正如传统的函数程序可以被理解为直觉主义逻辑中的证明一样，量子过程也可以被视为合适逻辑中的证明。我们描述这样一个逻辑，紧凑的闭范畴和biproducts的逻辑，提出了作为一个微积分和作为一个系统的证明网。这种逻辑捕捉了在经典控制下表示量子过程所需的大部分必要结构，同时对细节保持不可知论。我们演示了如何表示量子过程的证明网，并表明量子过程的动态行为被捕获的逻辑的削减消除过程。我们表明，削减消除程序是强烈规范化：也就是说，每一个法律的简化证明网络的方式导致相同的，唯一的，正常的形式。最后，采取一些初始的操作作为非逻辑公理，我们表明，由此产生的类别的证明网是一个表示的自由紧凑的闭范畴与这些操作所产生的双产品。
英文摘要：
Just as conventional functional programs may be understood as proofs in an intuitionistic logic, so quantum processes can also be viewed as proofs in a suitable logic. We describe such a logic, the logic of compact closed categories and biproducts, presented both as a sequent calculus and as a system of proof-nets. This logic captures much of the necessary structure needed to represent quantum processes under classical control, while remaining agnostic to the fine details. We demonstrate how to represent quantum processes as proof-nets, and show that the dynamic behaviour of a quantum process is captured by the cut-elimination procedure for the logic. We show that the cut elimination procedure is strongly normalising: that is, that every legal way of simplifying a proof-net leads to the same, unique, normal form. Finally, taking some initial set of operations as non-logical axioms, we show that that the resulting category of proof-nets is a representation of the free compact closed category with biproducts generated by those operations.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
