带有可逆性与控制操作的Proto-Quipper

《Journal of Logical and Algebraic Methods in Programming》：Proto-Quipper with Reversing and Control

　　

量子编程语言Quipper支持诸如逆转和控制特定量子电路等电路操作。此外，Quipper提供了一个名为with-computed的函数，可用于编程形如g; f; g^?的电路。后者是量子电路设计中常见的模式。使用with-computed的好处在于，相比直接从g、f和g^?构建g; f; g^?电路，它促进了一项重要的优化。即，如果最终生成的电路随后被控制，则仅需控制f；而电路g和g^?甚至不需要是可控制的。在本文中，研究人员形式化了可逆与可控电路的语义，使用dagger对称幺半范畴(dagger symmetric monoidal category) R 来解释可逆电路，并引入了一个新概念称为可控范畴(controllable category) N，它涵盖了Quipper中的控制和with-computed操作。研究人员通过逆转、控制以及with-computed操作扩展了Proto-Quipper语言。由于并非所有电路都是可逆和/或可控的，研究人员使用带有模态的类型系统来跟踪可逆性和可控性。这推广了Fu-Kishida-Ross-Selinger 2023的模态。研究人员给出了一个抽象的范畴语义，并证明了该类型系统和操作语义相对于该语义是可靠的。最后，研究人员利用类似于Fu-Kishida-Ross-Selinger 2022的思想，给出了一个范畴模型的构造。

量子算法在执行过程中常需利用电路的逆转、控制及其关联的“with-computed”操作以优化资源消耗，但在实际应用中，如状态准备和测量等操作往往会导致电路变为不可逆或不可控。在诸如Quipper等现有语言中，错误地控制一个不可控电路或逆转一个不可逆电路通常会引发运行时错误。为了在编译期捕获此类错误，避免在电路生成或执行阶段引发系统崩溃，亟需开展相关研究为量子编程语言配备能够静态跟踪电路可逆性与可控性的类型系统。研究人员开展了一项研究，通过引入模态概念扩展现有的Proto-Quipper语言，设计出一种强类型的函数式量子编程语言变体Proto-Quipper-C。该研究不仅形式化了可控范畴的数学概念，还为该语言设计了操作语义与抽象的范畴语义，并严格证明了类型系统的安全性及操作语义相对于范畴模型的可靠性。该研究的关键意义在于，其从数学范畴论的高度为量子电路的可逆性和可控性提供了坚实的理论基础，防止了资源无效操作引发的运行时错误，论文发表在《Journal of Logical and Algebraic Methods in Programming》上。

在关键技术方法方面，研究人员主要基于范畴论构建了抽象的形式模型与语义解释逻辑。具体而言，引人了一个dagger对称幺半范畴 R 来解释量子电路的可逆性操作；同时创新性地定义了一个可控范畴 N 以涵盖控制与“with-computed”模式；在类型系统设计中，引入了一个处于格结构 2 > 1 > 0 中的模态系统，其中模态2代表可逆且可控，1代表可逆但不可控，0代表既不可逆也不可控，通过格的下确界操作自动追踪复合电路的模态。

控制置换电路
在此项研究中，研究人员探讨了在Proto-Quipper中执行控制操作时处理隐式导线置换的方法。通过对比无门置换与显式交换门的研究发现，在执行控制操作时不加以妥善处理会导致非等价的错误电路输出。研究得出结论，编程语言必须能够察觉语言本身执行的隐式量子比特置换，若此类操作受到控制，有时必须插入显式的交换门，Proto-Quipper-C能够正确处理此机制以确保电路的语义正确性。

可逆性、控制与with-computed的形式化模型
为了在抽象层面定义量子电路，研究人员设定量子电路由具备特定属性的幺半范畴的态射抽象表示。在此框架下，可逆子范畴被定义为dagger对称幺半范畴 R。为了刻画控制概念，研究人员形式化了可控范畴 N 的定义，该范畴配备了with-computed操作的结构、控制离散幺半范畴 C，以及一个保持等式的严格dagger对称幺半函子 G。该研究得出结论，通过这种抽象的范畴结构设置，能够全面且严谨地涵盖量子计算中门控的逆转和泛化控制（如基于子空间的控制）。

用于可逆性、控制与with-computed的类型系统
在形式模型的基础上，研究人员定义了Proto-Quipper-C语言的语法和类型系统。该语言包含线类型、简单类型与参数类型，并引入了模态来约束执行时可能附加到当前电路的门控状态。通过详细的类型推导规则，研究人员得出结论，该类型系统能够有效追踪复合电路的可逆性与可控性，并在编译时拒绝诸如对非可控电路施加控制请求或对非可逆电路请求逆转等严重类型错误。

操作语义
研究人员为Proto-Quipper-C提供了一种大步、传值调用的操作语义，并定义了配置三元组以演化计算状态。同时，通过归纳法证明得出了类型保持性定理。研究结论表明，只要程序通过了类型检查，其在执行过程中产生的状态转换将不会导致运行时错误，这一特性保障了语言在应对不可行操作时的固有安全性。

可逆与控制的范畴语义
在语义解释层面，研究人员将类型规则解释到一个具备多重代数结构的抽象范畴 A 中。该范畴被证明能够作为Proto-Quipper-C的模型，且其定义包含了大量复杂的代数结构约束，如带有余积的对称幺半闭结构、伴随以及表示不同电路类别的幂等单子 T₀ 和 T₁。研究发现，通过映射将抽象模型中的结构进行对应，能够为语言的类型系统提供严谨的指称语义，并且通过可靠性定理证明了操作语义与指称语义的完全一致。

具体范畴模型的构造
为了说明抽象模型的可行性，研究人员运用了富集范畴理论，构造了一个满足抽象模型所有公理的具体范畴模型。研究利用对象为三集的预层范畴，构造了相关幂等单子结构，以及通过富化Yoneda嵌入将原范畴转换至富化预层范畴。研究得出结论，该基于三集富集的具体模型能够自然支撑抽象范畴模型的所有结构要求，确立了理论系统的实现可能性。

于结论部分，研究人员总结道，本文成功将逆转、控制以及with-computed操作扩展到了Proto-Quipper语言家族中，构建了全新的语言变体Proto-Quipper-C。该语言通过基于三个核心电路范畴的参数化设置精确区分了电路的模态类别。通过配备完备的类型系统、操作语义以及以单子表征模态的范畴模型，该研究证明了操作语义的可靠性，并成功构建了确保理论自洽的具体模型实现，为后续结合依赖类型或多重模态的研究奠定了基础。