专栏首页arxiv.org翻译专栏在Coq中量子电路的符号推理(CS PL)
原创

在Coq中量子电路的符号推理(CS PL)

量子电路是将输入量子态转换为输出量子态的计算单元,解释其行为的一种常见方法是显式地计算由其实现的酉矩阵。然而,随着量子位数的增加,矩阵维数呈指数增长,计算将变得困难。

本文提出了一种量子电路的符号推理方法,它是基于一组向量和矩阵基本操作的定律。这种符号推理方法比显式推理方法具有更好的可扩展性,并且非常适合在Coq中实现自动化,本文展示了一些典型的例子。

原文题目:Symbolic Reasoning about Quantum Circuits in Coq

原文:A quantum circuit is a computational unit that transforms an input quantum state to an output one. A natural way to reason about its behavior is to compute explicitly the unitary matrix implemented by it. However, when the number of qubits increases, the matrix dimension grows exponentially and the computation becomes intractable. In this paper, we propose a symbolic approach to reasoning about quantum circuits. It is based on a small set of laws involving some basic manipulations on vectors and matrices. This symbolic reasoning scales better than the explicit one and is well suited to be automated in Coq, as demonstrated with some typical examples.

原文作者:Wenjun Shi, Qinxiang Cao, Yuxin Deng, Hanru Jiang, Yuan Feng

原文链接:https://arxiv.org/abs/2005.11023

原创声明,本文系作者授权云+社区发表,未经许可,不得转载。

如有侵权,请联系 yunjia_community@tencent.com 删除。

我来说两句

0 条评论
登录 后参与评论

相关文章

  • 危机中的隐私:新冠病毒大流行期间的自我披露研究(CS SI)

    我们研究了代表用户主导的英语会话的推特大数据集在2020年3月1日至4月3日的一个月里自我披露的发生率。通过一种无监督的方法来检测个人信息的自愿披露,我们提供了...

    Elva
  • 电影世界最重要的演员是谁?用Python和NetworkX分析电影明星的社交网络(CS SI)

    本文提供了于2020年2月最初发表在The Conversation上的一篇文章的技术细节。本文的目的是利用中心性度量来分析电影明星的社交网络,从而确定电影行业...

    Elva
  • NDD20:一个用于粗粒度和细粒度分类的大型少镜头海豚数据集(CS CV)

    在本文中,我们介绍了Northumberland Dolphin数据集2020(NDD20),这是一个具有挑战性的图像数据集,用于粗粒度和细粒度实例分割和分类。...

    Elva
  • C++核心准则F.52:在lambda表达式中使用引用形式捕捉局部变量

    F.52 在lambda表达式中使用引用形式捕捉局部变量,包含向算法传递变量的情况。

    面向对象思考
  • what is telnet?

    Note: SSH is required to establish remote terminal connections to Indiana Univer...

    ke1th
  • 浅谈UDP(数据包长度,收包能力,丢包及进程结构选择)

    udp 数据包的理论长度是多少,合适的 udp 数据包应该是多少呢?

    三丰SanFeng
  • 绿色版Mysql的内存降低

    绿色版本的mysql只是一个压缩包,将其解压后,运行bin目录下的mysqld就可以将mysql启动了。 但是占用的内存令人发指,直接900M占用。但是绿色版没...

    用户2657851
  • 最近做的几件事

    MVC模型,把前、后以及中间控制器分离了,3样东西,分开写,Coding的时候,专注于某一个细节即可,最后再联动调试。

    libo1106
  • HDU 1061

    http://acm.hdu.edu.cn/showproblem.php?pid=1061

    用户2965768
  • 面向非标准到达过程的多服务器系统人员配备(CS P)

    服务系统的到达过程通常显示(i)大于预期的波动,(ii)时变率和(iii)时间相关性。因此,我们引入了一种结合了这三个特征的特定非均匀泊松过程。最终的到达过程将...

    蔡秋纯

扫码关注云+社区

领取腾讯云代金券