具有不确定因果顺序的高阶程序：量子过程相干控制的线性方法
Higher-Order Programs with Indefinite Causal Orders: a Linear Approach to Coherent Control of Quantum Processes
浏览论文内容
中文总结 AI 辅助
研究具有不确定因果顺序的量子过程相干控制，引入高阶量子函数式语言，其线性类型系统可定义任意量子通道上的量子控制，配有操作和表示语义，证明可靠性，研究表达能力，还能扩展到非线性递归设置。
中文摘要 AI 辅助
具有不确定因果顺序（ICO）的过程，如量子开关，是叠加量子操作执行顺序的高阶量子过程。现有量子编程语言无法忠实捕捉这种相干控制：要么限于酉情形，无法将ICO与测量结合，要么非线性处理相干控制。我们引入一种高阶量子函数式语言，支持一般量子计算，其线性类型系统允许在任意量子通道上对量子控制进行良好定义。该语言配有小步操作语义，通过设备引用和存储函数同步叠加分支上的测量结果。还通过完全正定映射给出表示语义。因线性是唯一约束，一些良类型项可能表示非物理映射，所以施加超越线性的类型规则，在因果范畴Caus[CPM]中解释程序，在此范畴下每个良类型程序都有物理意义，且可静态高效检查。我们证明了可靠性，并研究了语言的表达能力：它能一阶表达每个量子通道，二阶表达包含量子开关的一大类所谓带量子控制的量子电路（QC-QC）。最后，我们表明该语言设计良好，足以扩展到带递归的非线性设置。
英文摘要
Processes with indefinite causal orders (ICOs), such as the quantum switch, are higher-order quantum processes that superpose the order in which quantum operations are performed. Such coherent control yields computational advantages but is not faithfully captured by existing quantum programming languages: either they are restricted to the unitary case, and thus cannot combine ICOs with measurement, or they treat coherent control nonlinearly. In both cases, they do not realize the full computational power of ICOs. We introduce a higher-order quantum functional language that supports general quantum computation, not merely the permutation of channels, and whose linear type system allows quantum control to be well-defined beyond the unitary case, on arbitrary quantum channels. We equip this language with a small-step operational semantics that synchronizes measurement outcomes across superposed branches, using device references and a memory function. We also give a denotational semantics by means of completely positive maps. With linearity as the only constraint, some well-typed terms would denote unphysical maps. We therefore impose a typing discipline that goes beyond linearity, and interpret programs in the causal category Caus[CPM], under which every well-typed program is physically meaningful, a property that can be checked statically and efficiently. We prove soundness, and study the language's expressive power: it can express every quantum channel at first order, and at second order a large subclass of the so-called quantum circuits with quantum control (QC-QCs), containing the quantum switch. Last but not least, we show that this language is well-designed enough to be extended to the nonlinear setting with recursion.
