AI 中文总结
研究量子计算中因果性问题，提出带量子控制的类型化λ演算及范畴语义，用高阶函数和量子条件分支扩展纯量子计算，基于直觉主义BV逻辑设类型系统加强因果性，借新模型证某些不可实现过程不可定义。
AI 中文摘要
不确定因果顺序是量子计算中的一种特征现象，如量子开关和OCB过程。并非所有此类过程都被认为可物理实现，量子开关有一些实现方案，而OCB过程被怀疑不可实现，这种可实现性差异通常归因于物理因果性的限制。本文在高阶环境下研究此类因果性问题，提出带量子控制的类型化λ演算及其范畴语义。该演算用高阶函数和量子条件分支扩展了纯量子计算，并配备基于直觉主义BV逻辑的类型系统以加强因果性。还提出一个与Caus构造密切相关的新模型，证明一些物理上不可实现的过程在该语言中不可定义。
英文摘要
Indefinite causal order is a characteristic phenomenon in quantum computation, with examples including the quantum SWITCH and the OCB process. Not all such processes are believed to be physically realizable: while some implementations of the quantum SWITCH have been proposed, the OCB process is suspected to be unrealizable. This difference in realizability is commonly attributed to constraints imposed by physical causality. This paper studies such a causality issue in a higher-order setting, proposing a typed lambda calculus with quantum control and its categorical semantics. Our calculus extends pure quantum computation with higher-order functions and quantum conditional branching, and it is equipped with a type system based on intuitionistic BV logic to enforce causality. We also present a novel model that is closely related to the Caus construction, by which we prove that some physically-unrealizable processes are not definable in our language.
CommentsFull version of the conference paper at LICS 2026. 34 pages
DOI：10.4230/LIPIcs.LICS.2026.57
