一句话:提出隐藏与分配两种对偶量子信息效应,建立可表达不可逆量子计算(含测量)的类型与效应系统,并给出范畴语义。
本文研究量子计算中调控信息量的两种对偶效应:隐藏(hiding)与分配(allocation)。作者构建了一个类型与效应系统,使其对包含测量的不可逆量子计算具有完全表达能力。方法上,论文提出通用范畴构造,从解释可逆基础语言的任意 rig groupoid 出发,为带 choice 的 arrow 元语言提供语义解释。该构造可导出量子测量的一般性质,并支持将非迭代量子流程图翻译到该语言中。关键结果是:这些语义构造把希尔伯特空间间酉映射的范畴变为完全正保迹映射范畴,把有限集间双射范畴变为带选定垃圾的函数范畴;由此分别捕捉经典与量子可逆计算的 Toffoli 定理和 Stinespring 定理。
We study the two dual quantum information effects to manipulate the amount of information in quantum computation: hiding and allocation. The resulting type-and-effect system is fully expressive for irreversible quantum computing, including measurement. We provide universal categorical constructions that semantically interpret this arrow metalanguage with choice, starting with any rig groupoid interpreting the reversible base language. Several properties of quantum measurement follow in general, and we translate (noniterative) quantum flow charts into our language. The semantic constructions turn the category of unitaries between Hilbert spaces into the category of completely positive trace-preserving maps, and they turn the category of bijections between finite sets into the category of functions with chosen garbage. Thus they capture the fundamental theorems of classical and quantum reversible computing of Toffoli and Stinespring.