We propose a new typed graphical language for quantum computation, based on compact categories with biproducts. Our language generalizes existing approaches such as ZX-calculus and quantum circuits, while offering a natural framework to support quantum control: it natively supports "quantum tests". The language comes equipped with a denotational semantics based on linear applications, and an equational theory. Through the use of normal forms for the diagrams, we prove the language to be universal, and the equational theory to be complete with respect to the semantics.
翻译:我们提出了一种新的带类型的量子计算图形语言,基于具有双积的紧凑范畴。该语言推广了现有的方法(如ZX-演算和量子电路),同时为支持量子控制提供了自然框架:它原生支持“量子测试”。该语言配备了基于线性映射的指称语义和一个等式理论。通过使用图的范式,我们证明了该语言是普适的,并且该等式理论相对于该语义是完备的。