Semantics of higher-order quantum computation via geometry of interaction
Semantics of higher-order quantum computation via geometry of interaction
复制标题
DOI：
10.1016/j.apal.2016.10.010
复制
发表时间：
2017-02-01
影响因子：
0.8
通讯作者：
Hoshino, Naohiko
中科院分区：
文献类型：
--
作者：
Hasuo, Ichiro;Hoshino, Naohiko
尽管当前关于量子计算的大部分研究都采用了低级形式主义（例如量子电路），但最近提出了几种高级语言/计算，目的是针对结构化量子编程。当前的工作通过提供功能性量子编程语言的基于相互作用的语义来促进此类语言的语义研究；后者就像塞林格和维龙一样，基于线性lambda微积分，并配备了诸如！方式和递归。所提出的表示模型是支持量子功能编程语言的全部功能的第一个模型。我们证明了语义的充分性。我们的模型的构建是通过一系列现有技术从古典计算的语义以及过程理论中构建的。其中最值得注意的是吉拉德（Girard）的互动几何形状（GOI），它是由艾布拉姆斯基（Abramsky），哈格维迪（Haghverdi）和斯科特（Scott）明确提出的。这些技术的数学通用性是由于它们从经典到量子的转移而被利用的。 （c）2016 Elsevier B.V.保留所有权利。
While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work contributes to the semantical study of such languages by providing interaction-based semantics of a functional quantum programming language; the latter is, much like Selinger and Valiron's, based on linear lambda calculus and equipped with features like the ! modality and recursion. The proposed denotational model is the first one that supports the full features of a quantum functional programming language; we prove adequacy of our semantics. The construction of our model is by a series of existing techniques taken from the semantics of classical computation as well as from process theory. The most notable among them is Girard's Geometry of Interaction (GoI), categorically formulated by Abramsky, Haghverdi and Scott. The mathematical genericity of these techniques-largely due to their categorical formulation-is exploited for our move from classical to quantum. (C) 2016 Elsevier B.V. All rights reserved.