PLQP & Company: Decidable Logics for Quantum Algorithms
PLQP & Company: Decidable Logics for Quantum Algorithms
复制标题
DOI：
10.1007/s10773-013-1987-3
复制
发表时间：
2014-10-01
影响因子：
1.4
通讯作者：
Zhong, Shengyang
中科院分区：
文献类型：
--
作者：
Baltag, Alexandru;Bergfeld, Jort;Zhong, Shengyang
我们引入了概率模态（动态认知）量子逻辑 PLQP 来推理量子算法。我们通过使用它来编码众所周知的量子搜索算法以及已知用于解决经典分布式计算的典型任务之一（领导者选举问题）的量子协议的正确性来说明其表达能力。我们还提供了一种通用方法（扩展了 Dunn 等人（J. Symb. Log. 70:353-359, 2005）中可判定性证明中使用的想法），用于证明在有限维希尔伯特空间上解释的一系列量子逻辑的可判定性。我们给出了该方法适用性的一般条件，特别是我们应用它来证明 PLQP 的可判定性。
We introduce a probabilistic modal (dynamic-epistemic) quantum logic PLQP for reasoning about quantum algorithms. We illustrate its expressivity by using it to encode the correctness of the well-known quantum search algorithm, as well as of a quantum protocol known to solve one of the paradigmatic tasks from classical distributed computing (the leader election problem). We also provide a general method (extending an idea employed in the decidability proof in Dunn et al. (J. Symb. Log. 70:353-359, 2005)) for proving the decidability of a range of quantum logics, interpreted on finite-dimensional Hilbert spaces. We give general conditions for the applicability of this method, and in particular we apply it to prove the decidability of PLQP.