Causality in Pure Quantum Computation with Quantum Control
Programming LanguagesLogic in Computer Science
Summary
The authors study how quantum processes where the order of events isn't fixed can or cannot exist physically. They create a new programming framework based on quantum computing with special rules to keep cause-and-effect relationships logical. Using this framework, they show that some quantum processes, believed to be impossible to realize in reality, indeed cannot be expressed in their system. This helps explain why certain strange quantum behaviors don’t happen physically.
Authors
Kengo Hirata, Takeshi Tsukada
Abstract
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.