迈向量子程序范畴逻辑的第一步。

A First Step to the Categorical Logic of Quantum Programs.

作者信息

Sun Xin, He Feifei

机构信息

Department of foundation of computer science, the John Paul II Catholic University of Lublin, 20-950 Lublin, Poland.

Institute of logic and cognition, Sun Yat-sen University, Guangzhou 510970, China.

出版信息

Entropy (Basel). 2020 Jan 24;22(2):144. doi: 10.3390/e22020144.

DOI:10.3390/e22020144

PMID:33285919

原文链接:https://pmc.ncbi.nlm.nih.gov/articles/PMC7516558/

Abstract

The long-term goal of our research is to develop a powerful quantum logic which is useful in the formal verification of quantum programs and protocols. In this paper we introduce the basic idea of our categorical logic of quantum programs (CLQP): It combines the logic of quantum programming (LQP) and categorical quantum mechanics (CQM) such that the advantages of both LQP and CQM are preserved while their disadvantages are overcome. We present the syntax, semantics and proof system of CLQP. As a proof-of-concept, we apply CLQP to verify the correctness of Deutsch's algorithm and the concealing property of quantum bit commitment.

摘要

我们研究的长期目标是开发一种强大的量子逻辑，它可用于量子程序和协议的形式验证。在本文中，我们介绍了量子程序范畴逻辑（CLQP）的基本思想：它结合了量子编程逻辑（LQP）和范畴量子力学（CQM），从而在保留LQP和CQM优点的同时克服了它们的缺点。我们给出了CLQP的语法、语义和证明系统。作为概念验证，我们应用CLQP来验证德伊奇算法的正确性和量子比特承诺的隐藏属性。