We investigate the algebraic reasoning of quantum programs inspired by the success of classical program analysis based on Kleene algebra. One prominent example of such is the famous Kleene Algebra with Tests (KAT), which has furnished both theoretical insights and practical tools. The succinctness of algebraic reasoning would be especially desirable for scalable analysis of quantum programs, given the involvement of exponential-size matrices in most of the existing methods. A few key features of KAT including the idempotent law and the nice properties of classical tests, however, fail to hold in the context of quantum programs due to their unique quantum features, especially in branching. We propose the Non-idempotent Kleena Algebra (NKA) as a natural alternative and identify complete and sound semantic models for NKA as well as their appropriate quantum interpretations. In light of applications of KAT, we are able to demonstrate algebraic proofs in NKA of quantum compiler optimization and the normal form of quantum while-programs. Moreover, we extend NKA with Tests (i.e., NKAT), where tests model quantum predicates following the rules of effect algebra, and illustrate how to encode propositional quantum Hoare logic as NKAT theorems.

翻译：我们调查了基于Kleene代数的经典方案分析的成功所启发的量子方案的代数推理。这方面的一个突出例子是著名的Kleene代数与测试(KAT),它既提供了理论见解,也提供了实用工具。鉴于指数大小矩阵在大多数现有方法中的参与,因此,代数推理对于量子方案的可缩放分析特别可取。KAT的一些关键特征,包括一等能力法和古典试验的优美特性,但由于量子方案的独特量子特性,特别是在分支中,未能在量子方案中保持。我们提议将非精英Kleena Algebra(NKA)作为自然的替代方案,并确定NKAK的完整和健全的语义模型以及适当的量子解释。根据KAT的应用,我们可以在NKAK的量子汇编优化和普通质子试验形式中展示代数证据。此外,我们用测试(i.e.a.,NKAT)作为自然替代方案,并查明NKAA的完整和健全的语系模型测试,以此来说明AS的代数级标准。