A First Step to the Categorical Logic of Quantum Programs

被引：1
|
作者：
Sun, Xin [1 ]
He, Feifei [2 ]
机构：
[1] John Paul II Catholic Univ Lublin, Dept Fdn Comp Sci, PL-20950 Lublin, Poland
[2] Sun Yat Sen Univ, Inst Log & Cognit, Guangzhou 510970, Peoples R China
来源：
ENTROPY | 2020年 / 22卷 / 02期
关键词：
quantum logic; quantum computing; category theory; BIT COMMITMENT; CORRECTNESS;
D O I：
10.3390/e22020144
中图分类号：
O4 [物理学];
学科分类号：
0702 ;
摘要：
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.
引用
收藏
页数：14
相关论文
共 50 条
  • [21] A Novel Categorical Approach to Semantics of Relational First-Order Logic
    Schreiner, Wolfgang
    Steingartner, William
    Novitzka, Valerie
    SYMMETRY-BASEL, 2020, 12 (10):
  • [22] Abstract Categorical Logic
    Marc Aiguier
    Isabelle Bloch
    Logica Universalis, 2023, 17 : 23 - 67
  • [23] ULTRAPRODUCTS AND CATEGORICAL LOGIC
    MAKKAI, M
    LECTURE NOTES IN MATHEMATICS, 1985, 1130 : 222 - 309
  • [24] Abstract Categorical Logic
    Aiguier, Marc
    Bloch, Isabelle
    LOGICA UNIVERSALIS, 2023, 17 (01) : 23 - 67
  • [25] First step across the categorical border requires higher neural response
    Kurakova, O.
    PERCEPTION, 2010, 39 : 125 - 126
  • [26] Verifying Graph Programs with First-Order Logic
    Wulandari, Gia S.
    Plump, Detlef
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2020, (330): : 181 - 200
  • [27] A progression semantics for first-order logic programs
    Zhou, Yi
    Zhang, Yan
    ARTIFICIAL INTELLIGENCE, 2017, 250 : 58 - 79
  • [28] A declarative semantics for depth-first logic programs
    Elbl, B
    JOURNAL OF LOGIC PROGRAMMING, 1999, 41 (01): : 27 - 66
  • [29] Abstract Diagnosis of First Order Functional Logic Programs
    Bacci, Giovanni
    Comini, Marco
    LOGIC-BASED PROGRAM SYNTHESIS AND TRANSFORMATION, 2011, 6564 : 215 - 233
  • [30] MADRID QUANTUM NETWORK: A FIRST STEP TO QUANTUM INTERNET
    Garcia Cid, Marta Irene
    Ortiz Martin, Laura
    Martin, Vicente
    ARES 2021: 16TH INTERNATIONAL CONFERENCE ON AVAILABILITY, RELIABILITY AND SECURITY, 2021,
12345