量子计算中紧闭范畴的图形推理
Graphical Reasoning in Compact Closed Categories for Quantum Computation
摘要：
紧闭范畴为包括量子计算在内的许多重要领域提供了基础形式。这些类别有一个自然的可视化作为一种形式的图形。我们提出了一个形式主义的等式推理这样的图，并发展成一个通用的证明系统，一个固定的逻辑内核的等式推理紧凑的闭范畴。自动化这个推理过程的动机是手动图形操作的缓慢和容易出错的性质。我们的系统的一个显着特点是，它提供了一个正式的和声明性的帐户派生的结果，可以包括'省略号'风格的符号。我们通过实例化量子计算的图形语言来说明框架，并展示如何使用它来执行符号计算。
英文摘要：
Compact closed categories provide a foundational formalism for a variety of important domains, including quantum computation. These categories have a natural visualisation as a form of graphs. We present a formalism for equational reasoning about such graphs and develop this into a generic proof system with a fixed logical kernel for equational reasoning about compact closed categories. Automating this reasoning process is motivated by the slow and error prone nature of manual graph manipulation. A salient feature of our system is that it provides a formal and declarative account of derived results that can include `ellipses'-style notation. We illustrate the framework by instantiating it for a graphical language of quantum computation and show how this can be used to perform symbolic computation.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
