基于类型的格手术中连通性约束验证
Type-Based Verification of Connectivity Constraints in Lattice Surgery
AI总结：
本文提出基于类型的方法静态验证格手术中量子程序不会因连通性约束而异常终止，并设计语言$\mathcal{Q}_{LS}$及基于离线动态连通性的类型检查算法。
摘要：
使用格手术的容错量子计算可以抽象为图上的操作，其中每个逻辑量子比特对应图中的一个顶点，多量子比特测量通过用路径连接顶点来完成。试图在没有有效路径的情况下连接顶点的操作将导致异常终止。由于允许的路径可能在执行过程中发生变化，因此有必要静态验证量子程序的执行能够完成。本文引入了一种基于类型的方法，用于静态验证良类型程序在执行时不会遇到由手术操作引起的停机。同时，我们提出了$\mathcal{Q}_{LS}$，一种一阶量子编程语言，用于形式化手术操作的执行模型。此外，我们通过将类型检查问题归约为离线动态连通性问题，提供了一个类型检查算法。
英文摘要：
Fault-tolerant quantum computation using lattice surgery can be abstracted as operations on graphs, wherein each logical qubit corresponds to a vertex of the graph, and multi-qubit measurements are accomplished by connecting the vertices with paths between them. Operations attempting to connect vertices without a valid path will result in abnormal termination. As the permissible paths may evolve during execution, it is necessary to statically verify that the execution of a quantum program can be completed. This paper introduces a type-based method to statically verify that well-typed programs can be executed without encountering halts induced by surgery operations. Alongside, we present $\mathcal{Q}_{LS}$, a first-order quantum programming language to formalize the execution model of surgery operations. Furthermore, we provide a type checking algorithm by reducing the type checking problem to the offline dynamic connectivity problem.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
