丰富范畴理论与量子电路语言的分类模型

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）257-279www.elsevier.com/locate/entcs丰富范畴理论中的经典控制与量子Mathys RennelaRadboud大学计算和信息科学研究所荷兰奈梅亨萨姆·斯塔顿牛津大学联合王国摘要我们描述了基于电路的（量子）函数式编程语言的分类模型。我们发现，丰富的类别起着至关重要的作用。继Paykin等人早期对QWire的研究之后，我们既考虑电路的简单一阶线性语言，也考虑更强大的宿主语言，使得电路语言嵌入宿主语言中。我们的主机语言的范畴语义是标准的，并涉及到carbohydrate封闭范畴和单子。我们解释电路语言，一个普通的类别，但在一个类别，是丰富的主机类别。作为一个推广的例子，我们回顾了一个较早的结果，即W*-代数的范畴是dcpo-丰富的，我们使用这个模型来推广具有一些递归类型的电路语言关键词：丰富范畴，范畴语义，线性类型理论，量子电路，相对单子，量子域理论1介绍量子计算的一个微妙之处是经典控制流与量子运算之间的相互作用。人们可以测量一个量子位，破坏量子位，但产生一个经典位;这个经典位然后可以用来决定是否将量子旋转应用于其他量子位。这种控制经典量子测量在量子电路中，可以很好地描述经典控制，例如，当使用量子位a的测量结果来有条件地执行门X时，https://doi.org/10.1016/j.entcs.2018.03.0271571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。258M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257在量子位b上：Ba（一）这可以从语义上理解为混合状态，密度矩阵，和完全正的地图然而，高级语言具有比比特更精细的数据结构：它们具有更高阶的函数和混合方差递归类型，并且与这些相关联的是精细的控制结构，作为高阶递归函数。这些都是重要的、典型的程序结构化方法。这些高级特征应该如何与量子计算相结合？一种选择是建立一个语义域，容纳量子计算和高阶特征。 这是量子lambda演算[21，17]和作者[24，26]先前工作的某些范畴语义的目标。这是一个迷人的方向，并揭示了，例如，量子隐形传态算法的结构（例如，[21，Ex. 6]）。然而，物理学和高阶量子函数之间的一般联系还不清楚。虽然最近已经取得了一些进展[14]，但仍然不清楚这种高阶量子函数是否适用于量子算法。另一种方法是将高级量子编程语言理解为普通的高阶函数语言，具有用于构建和运行量子电路的额外功能。在这种情况下，量子电路在传统的高阶语言中形成了一阶嵌入式域特定语言。这符合当前量子硬件接口的最新技术水平，并且是语言Quipper [10]和LiQUi的基础|[31].这就是我们在本文中研究的方法。1.1嵌入式语言和丰富的类别我们的工作围绕着一个新的演算，我们称之为它是QWire语言的一个小推广[22]。QWire将Quipper和LiQUi架构的某些方面理想化|- 是的我们的想法是，我们处理一个主机语言从嵌入式电路语言分离。• 电路语言是一种一阶类型化语言。这些类型被称为线型系统是线性的，以适应量子位不能被复制的事实。• 宿主语言是一种高阶语言。宿主语言的类型不包括线类型，没有量子位的类型，并且它不是线性类型系统。然 而 ，有一个特殊的主机类型Circ（W1，W2）与任何一对导线类型W1和W2相关联，其居民是具有类型W 1的输入和类型W 2的输出的电路。让我们简单地描述电路语言：非常简单的电路（1）对应于电路语言中的以下指令（2）。给定两个量子比特a和b，它测量量子比特a，将结果存储在比特x中，该比特x稍后用于X·M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257259w1C1w2C2w3应用经典控制的X门并丢弃位x，然后输出得到的量子位y。−;a，b：量子比特Cd=ef x←gatemeasa;（x，y）←gate（bit-controlX）（x，b）;（）← gate discard x; output y：qubit（2）主机语言和电路语言之间的接口是通过装箱和拆箱来建立的。例如，指令td=ef方框（a，b）C（a，b）（其中C与（2）相同）（3）在宿主语言中创建一个Circ （qubit）类型的封闭项我们通过使用指令unboxtw从主机语言（3）中的装箱表达式t中恢复电路语言（2）中的指令C，用于一些类型为qubit的新线w此外，可以编写由两个电路C1和C2组成的程序正确的输入/输出类型，例如：这是一个程序compd=efλ（C1，C2）. boxw1m。w2<$unboxC1w1;w3<$unboxC2w2;输出w3在宿主语言中，与类型关联comp：Circ（W1，W2）×Circ（W2，W3）→Circ（W1，W3）（4）其中Wi是导线Wi的类型，i∈ {1， 2， 3}。现在，回想一下丰富范畴的概念，它是一个非正式的范畴，使得从A到B的态射形成另一个范畴的对象。在第3节中，一旦我们将类型概念化为对象，将术语概念化为态射，我们就证明了电路语言在宿主语言中的嵌入是丰富范畴论的一个实例：线类型（对象）之间的电路（态射）形成了宿主语言的类型（对象）。（4）中的主成分术语正是丰富范畴意义上的成分（详见第3节。）对于该模型的一个简单版本，线类型被理解为有限维C* 代数，电路是完全正的单位映射-公认的模型量子计算。主机类型被解释为集合，所有回路的类型被简单地解释为所有回路的集合。集合范畴支持高阶函数，这表明宿主语言具有高阶函数是一致的。与任何高阶语言一样，集合论模型是不充分的充分理解高阶函数的本质。我们设想其他语义模型（例如，基于游戏语义或可实现性）也将适合260M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257·QFT`Rn.Σ1 11−1同样的框架丰富的类别，使我们的分类框架提供了一个健全的描述基本程序的等价物，应该在所有的模型。这些等价与纯lambda演算中的β和η等价起着相同的作用换句话说，我们正在发展量子计算的基本类型理论1.2递归类型和递归项在这个语义模型中，基于丰富的类别，我们可以自由地容纳宿主语言中的各种附加功能，同时保持电路语言相同。例如，我们可以将递归添加到宿主语言中，以模拟重复尝试量子实验的想法，或者递归类型，以模拟任意数据类型。这可以通过修改简单模型来证明是一致的，这样主机类型就被解释为有向完全偏序（dcpo）。许多 量子 算法例如，量子傅立叶变换（QFT）对于任何数量的量子比特具有统一的定义，|x1⟩|x2mm|x3mm..·········|y n⟩|y n− 1|y n− 2..|y1|y1⟩哪里 H是 的 哈达码门12Rn是Z旋转rotatiboughtx门10n.0e2πi/ 2我们通过用量子位列表的线类型QList扩展电路语言来形式化它，对于该线类型QList，以下类型等价成立：QList<$=（qubit<$QList）<$1，这样我们就可以定义一个函数傅立叶：Circ（QList， QList）在第4节中，我们通过将电路视为一阶和线性（在术语的线性逻辑意义上）指令，从而与电路的规范直觉分开在实践中，电路布局引擎知道列表中的量子位的数量将是有用的，这表明依赖类型，例如傅立叶：（n：Nat）→Circ（QList（n），QList（n））但是我们把类型系统的这种细化留给将来的工作。递归数据类型的范畴本质是代数紧性。简而言之，当每个内函子F：C→C都有一个标准定点，即初始F-代数时，我们说范畴C是代数紧的（对于一个特殊的内函子类）。在早期的工作中[24]，第一作者已经表明，··R2HR3√M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257261W*-代数的范畴是代数紧的，并且在dcpo中丰富，因此这是语言语义的自然候选者。简单地说：回路类型被解释为W*-代数，回路被解释为完全正的子单位映射;主类型被解释为dcpo's;特别是回路Circ（W，W j）的集合被解释为完全正的子单位映射的dcpo，具有Lüow n r r d r r。在此基础上，我们提出了一个基于递归类型的quantum类型理论的基本模型。据我们所知，我们用能够以这种参数化方式容纳QFT的语言的第一个范畴语义来结束目前的工作。2函数式编程与量子电路我们引入了一个新的演算称为EWire作为分析的基础上嵌入一个电路语言内的主机函数式编程语言的基本思想。EWire（“嵌入式线语言”）基于QWire[ 22 ]（“量子线语言”），我们在第2.2节中精确连接。可以添加其他功能，例如在4.1节中讨论的功能。我们假设两类基本导线类型。• 经典的电线类型，范围由a，b，. .线路语言和主机语言中都存在导线类型。例如，经典位或布尔类型。• 仅电路导线类型，范围为α、β，........................这些导线类型仅存在于电路语言 例如，量子比特的类型。从这些基本类型中，我们构建所有的导线类型：W，W J：：= I|W W J|一|B |α |β我们隔离了经典的导线类型，这些类型不使用任何仅限电路的基本类型：V，VJ：：= I|VVJ|一|B...我们还假设一个基本门的集合G，每个门被分配一个输入和一个输出线类型。我们写G（Win，Wout）为输入类型Win和输出类型Wout的门的集合。除了嵌入式电路语言，我们考虑主机语言。这类似于Moggi因此，主机类型是A，B：：= A×B|1 |A→B|T（A）|Circ（W，WJ）|一|BmonadT主要是允许概率计算，尽管也可以将其他副作用添加到宿主语言中。请注意，每个经典导线类型V都 可以理解为一阶主机类型|V|根据简单的262M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257....平移，称为提升：VVJd=ef|V| ×VJ|我|d=ef1 |一|d=efa2.1电路类型和主机类型一个良构的电路判断Γ; Ω<$C：W 描述了一个输入上下文为Ω =（ w1：W1···wn：Wn）（n∈N），输出线类型为W，主语言变量为Γ =（x1：A1···xm：Am）（m∈N）的电路导线以语法p：：= w给出的模式组织|（）下一页|（p，p）与以下规则集相关联：−·=0（）：1−w：W=Ww：WΩ1 =p1：W1Ω2=p2：W2Ω1， Ω2=（p1，p2）：W1<$W2电路的线性类型理论第一个五项形成规则对于线性类型理论来说是相当标准的。这些是用于一个接一个地对电路进行排序，并以输出导线结束的构造数字规则包括电路语言中的基本门Γ; Ω1<$C1：W1Ω =Ωp：W1Γ;Ω， Ω2<$C2：W2Γ; Ω1， Ω2<$p←C1;C2：W2Ω =Ωp：W输出p：WΩ=p：1 Γ; ΩjC：WΩ=p：W1W2Γ;w1：W1，w2：W2，ΩJC：WΓ; Ω， ΩJ<$（）<$p;C：WΓ; Ω， ΩJ< $（w1，w2）<$p;C：WΩ1 =p1：W1Ω2=p2：W2Γ;Ω2， Ω<$C：Wg∈ G（W，W）1 2Γ; Ω1，Ωp2←gateg p1;C：W例如，通过以下电路给出了硬币加密ipd=efa<$gateinit0（）;aJ<$gateHa;b<$gatemeasaJ;outputb电路与主机一个格式良好的宿主判断Γt：A在宿主语言变量Γ的上下文中描述了一个A下一组类型规则描述了宿主语言和电路语言之间的交互。主机可以运行电路并获得结果。因为这可能有副作用，例如概率行为，它返回一个一元类型。Γ;·ωC：WW经典2016 - 05 - 25 01：01：02（|W|）接下来的两条规则涉及将电路作为宿主语言中的数据装箱，然后将数据拆箱以形成电路语言中的电路片段。注意，拆箱需要一个Circ（W1，W2）类型的纯程序，而不是一个有效的程序M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257263..类型T（Circ（W1，W2））的程序。例如，您不能取消装箱回路的概率组合。Monadic符号阐明了这一点。Ω =Ωp：W1Γ;ΩC：W2r_box（p：W1）r_C：Circ（W1，W2）Γπt：Circ（W1，W2）Ω =πp：W1Γ; Ωπunboxtp：W2最后，我们考虑动态提升，它非正式地允许我们在量子电路运行时向主机程序注意：|W |W古典Γ;−初始化t：WΩ = Ωp：|W |Γ，x：W; Ω J<$C：W JW经典Γ; Ω， Ωjxliftp;C：WJ这些规则是对Moggi[20]之后的宿主语言标准打字规则的补充（见附录A）。在附录B中，我们回顾了基于[22]的电路归约关系，它将没有自由主机变量的电路归约为以下表达式：N：：=输出p |w ← gate g p; N |x升力p; N|（）← w; N|（w1，w2）← w; N减少的工作原理是重新排列模式和解决未装箱的盒子。2.2QWirePaykin，Rand和Zdancewic[22]的语言QWire是EWire的一个实例，其中：• 存在一种经典的导线类型（比特）和一种仅电路导线类型（量子比特）。• 有基本门meas∈ G（qubit， bit）和new∈ G（bit， qubit）。EWire和QWire之间的一个微妙的区别是，在QWire中，人们可以直接运行一个量子比特类型的电路，它会产生一个比特，自动测量电路产生的量子比特。要在EWire中运行量子位类型的电路，必须在电路的末尾附加显式测量。这些显式测量可以自动附加，以提供从QWire到EWire实例的适当转换。我们现在总结一下如何做到这一点。我们首先定义从所有导线类型到经典导线类型的转换（−）W<$WJd=efW<$WJId=efIbitd=efbi tqubitd=efbit然后，从任意导线类型W，我们可以提取主机类型W。从基本门meas和new，我们可以为所有导线W定义电路measW：Circ（W，W）和newW：Circ（W，W）。它们由W上的归纳法定义。比如说，measId=efidmeasbitd=ef id测量量子位d=efboxppJ←门测量p;输出pJ264M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257测量值W′d=efbox（w，wJ）x<$unboxmeass Ww;xJ<$unboxmeasreturn（x，x，J）′wJ;新的W也是用新的G（bit， qubit）来定义然后，我们定义以下派生语法，以便run和lift可以用于所有线类型，而不仅仅是经典类型：qwire-run（C）d=ef run（x←C; u nboxmeasx）（x=qwire-liftp ;C）d=efy将p;x←取消装箱新的y;C3EWire的分类模型让我们定义一组足够的属性，确保一对范畴对应于一个范畴模型，在这个模型中，人们可以解释EWire，以便推理电路并识别它们的指称意义。我们假设电路语言是由一个固定的门集合参数化的，注G。丰富的类别。我们的发展是基于丰富的categories，这是越来越广泛地应用于编程语言理论的理论。我们回忆一些基本的东西。如果H是一个具有有限积×的范畴，则一个在H中丰富的范畴C由一个对象集合给出，• 对于C中的每对对象A和B，H的对象C（A，B）;• 对于C的每个对象A，H中的态射1→C（A，A）;• 对于C的对象A，B，C，证明了H中的态射C（A，B）×C（B，C）→C（A，C）这样组成满足恒等式和单位定律。 如果C和D在H中富集，则富集函子F是从C的对象集合到D的对象的集合，对于C的对象A和B，态射C（A，B）→D（F（A），F（B）），以适当的方式考虑组合和恒等式。举第一个例子，局部小范畴是态射集合C（A，B）是一个集合的范畴;这是一个在集合和函数的范畴Set作为丰富范畴在计算机科学中重要性的第一个例子，回想一下类型化lambda演算的模型是一个Carnival闭范畴，这是一个具有有限乘积的范畴H，它本身是丰富的对称幺半群富集范畴。 回想一下，一个对称monoidal范畴是一个范畴C，加上一个区别对象I和一个函子C：C×C→C与相干结合性、恒等性和对称性自然同构任何有乘积的范畴都是这样的例子，但更一般的对称么半群范畴模型 线 性 类 型理 论 ， 其 中弱 化 和 收 缩 可 能 不成 立 。 一 个H- 丰 富 的 对 称monoidal范畴以类似的方式定义，除了函子必须是一个丰富的函子和同构也必须是丰富的自然变换。WM. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257265.Σ（回想一下，对于H-丰富函子F，G：C→D之间的H-丰富范畴C和D，一个丰富的自然变换η：F<$G是态射族{ηc：1→D（Fc，Gc）}c∈Obj（C）满足一个简单的自然性条件.[13]更多细节。计算效应。嵌入电路语言需要在宿主语言中使用一些计算元素。 当电路语言涉及到量子测量时，封闭的主项run ip：T（比特）是一个掷硬币的问题，因此主语言的语义必须适应概率特征。根据Moggi，我们通过考虑一个在其上有一个丰富单子的Carnival闭范畴H来对此进行建模。回想一下，一个丰富单子是由H上的一个内函子T以及H中每个X的一个单位态射η：X→T（X），以及对象X和Y的一个绑定态射H（X，T（Y））→H（T（X），T（Y））给出的，服从单子定律[20]。其思想是，宿主语言中的确定性纯程序被解释为H中的态射。在宿主语言中，可能有效的程序被解释为Kleisli态射，即态射X→T（Y）。相对单子。莫吉的单子是一个稍微高阶的概念。在真正的一阶语言中，这种类型可以说是不应该存在的。特别是，所有量子计算都没有T（A）线型。为了解决这种不匹配，作者提出了替代方案，如相对monad[1]和带有arities的monad [4]。一个相对附加函数由三个函子J：B→D，L：B→C和R：C→D使得存在自然同构C（L（b），c）n=D（J（b），R（c））.我们写LJER，称相对单子为函子RL：B→D。丰富相对函子和丰富相对单子的定义是显而易见的，要求J、L和R是丰富函子，而附加子是丰富附加子。在一个丰富的相对单子T=RL中，绑定操作是D（J（X），T（Y））→D（T（X），T（Y））类型的态射科鲍尔上幂是n重上积的推广.设n是自然数，A是范畴C的一个对象，其上幂n<$A是n重余积A+···+A。这具有普适性质，即给出一个态射n<$A→B就是给出一族n个态射A→B。一般来说，如果C是一个在范畴H中丰富的范畴，A是C的一个对象，h是H的一个对象，那么上幂是一个对象h<$A连同一个同构族C（h<$A，B）<$= H（h，C（A，B）），自然在B中。集合丰富的余幂与量子算法的相关性先前已由Jacobs提出[11]。 另一方面，上幂和富集在非量子富集效应演算[7 ，19]和其他领域中起着关键作用。eas[16，18，23，29]。尽管如此，我们与EWire语法的联系似乎是新颖的。266M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257定义3.1EWire（H，H0，C，T）的分类模型由以下数据给出(i) 一类具有强单子T的范畴H.这是解释宿主语言所必需的。(ii) 一个小的全子类j：H0H。其思想是H 0的对象解释第一阶主机类型，等价地，经典的线类型：在主机语言和电路语言中都存在的类型。(iii) 一个H-充实的对称幺半群范畴（C，I，H）.这使我们能够解释电路语言，并且H丰富化使我们能够理解主机类型Circ（W，WJ）。(iv) 范畴C被H0的对象上幂. 上幂诱导函子J：H0→C，定义为J（h）=h<$I。然后，我们有一个自然的同构C（J（h），C）=C（h<$I，C）<$=H（j（h），C（I，C））因此，在电路和（主）项之间存在j-相对附加JjEC（I，-）这个函子J：H0→C解释了一阶宿主类型和经典连线类型之间的转换(v) 对于C的每个对象A，函子A<$−：C→C保持上幂。这使得函子J是对称的么半群，并且使得相对附加子是丰富的相对附加子。(vi) 存在一个丰富的相对单子态射运行h：C（I，J（h））→T（j（h））其中，富集的相对单子C（I，J（−））：H0→H是由富集的j-相对伴随JjEC（I，−）诱导的。这是运行量子电路的解释，产生一些经典的概率结果。如果范畴C对每个基本量子线类型α都有一个给定的对象[α]，而H0对每个基本经典线类型a都有一个给定的对象[a]，那么我们可以将所有线类型W解释为C的对象：[1]]d=efI[[a]]d=efJ（[[a]]） [W<$WJ]]d=ef[[W]]<$[[WJ]]。如果范畴C也有一个给定的态射[g]]：[[W1]]→[[W2]对于每个门g∈ G（W1，W2），则可以解释C中的电路语言。根据这些公理，对于EWire的每个范畴模型，我们关联以下指称语义。首先 ，我们按照约定定义了主Ty p e Circ（W，WJ）y[[Circ（W，WJ）]]d=efC（W，WJ）的表示，这是范畴的一个对象。H.其他主机类型的语义如下所示：[1]]d=ef1[A×AJ]]d=ef[[A]]×[[AJ]][[A→AJ]]d=ef（[A]]→[[AJ]]）[T（A）]]d=efT（[[A]]）。M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257267线Ω的有序上下文具有以下语义：[[··]]=I[[w：W]]=[[W]][[Ω，ΩJ]]=[[Ω][[ΩJ]]电路判断Γ;Ωt：W表示为：[Γ; Ω<$t：W]]∈H（[[Γ]]，C（[[Ω]]，[[W]]））这依赖于范畴H是宿主语言的模型这一假设。主类型Circ（W，WJ）被解释为范畴H中的hom-objectC（[[W]]，[[WJ]]）。在此设置中，装箱和取消装箱指令的表示为微不足道事实上，当verΩ=p：W1成立时，weh e[[Ω]]=[[W1]]，我们把[[Γ-box（p：W1）<$C：Circ（W1，W2）]]=[[Γ; Ω<$C：W2]][r; Ω=unboxtp：W2]]=[[rt：Circ（W1，W2）]]输出p的表示：W是当模式p的类型不是和类型，当p的形式为ipJ时，是第i个投影。此外，指令Γ; Ω， ΩJ<$（）←p;C：W和Γ; ΩJ<$C：W（分别为Γ; Ω，ΩJ< $（w1，w2）<$p;C：W和Γ;w1：W1，w2：W2，ΩJ<$C：W）在Ω =<$p：1成立时具有同构表示（分别为Ω =Ωp：W1<$W2成立）。电梯的建设是解释的copower。 详细地说，对于每个对象h的同构，以及H0的每个对象hJ，我们考虑H 0的同构升力h：H（h×hJ，C（X，Y））<$=H（h，H（hJ，C（X，Y））<$=H（h，C（hJ<$X，Y））由于我们输出导线类型为W型的电路C的运行由Def给出。3.1（六）.其余指令的表示如下。[Γ; Ω1， Ω<$p2←gateg p1;C：W]]=[[Γ; Ω2， Ω<$C：W]]<$（[[g]]_ id）[Γ; Ω1， Ω2<$p<$C;CJ：WJ]]=[[Γ; Ω， Ω2<$CJ：WJ]]<$（[[Ω1<$C：W]]<$id）考虑附录B中给出的操作语义。假设H是宿主语言的一个可靠的范畴模型，通过对类型判断的直接归纳可以得到下面的定理。(This类似于[22]中的证明。B].）定理3.2（可靠性）对于EWire的范畴模型所导出的指称语义，若回路判定·;Ω<$C：W成立，且回路C约化为回路CJ，则[[·;Ω<$C：W]]=[[·; Ω <$CJ：W]].现在是阐述一个例子的时候了。我们对量子计算语义的看法依赖于C*-代数理论。C*-代数的正元素对应于量子理论中的可观测量，我们将量子计算理解为保持正元素的线性映射，换句话说，268M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257∼CPUCC变 压 器 的 。 回 路 （ ·; （ x ： W ） <$C ： WJ ） 将 被 解 释 为 完 全 正 酉 映 射[WJ]]→[[W]。相反方向与用于常规编程的谓词Transformer语义相同。简而言之，（单位）C*-代数（例如[27]）是复数域上的向量空间，它也有乘法，单位和对合，满足乘法的结合性和单位律，对合律（例如[28]）。x<$$>=x，（xy）<$=y<$x<$，（αx）<$=α<$（x<$）），并证明了谱半径提供了一个范数使其成为Banach空间.C*-代数有两个重要的构造：矩阵代数和直和。矩阵代数是C*-代数的一个重要例子。例如，2× 2复矩阵的代数M2两个C*-代数的直和A<$B是具有分支代数结构的对的集合。例如，CC表示经典位的类型。每个有限维C*-代数都是矩阵代数的直和有限维C*-代数的张量积M由两个性质唯一确定：（i）Mk<$Ml=Mk×l，（ii）A<$（-）和（-）<$B保持直和。特别地，Mk<$A同构于（k×k）-A中的矩阵。我们在这里不关注保持所有C*-代数结构的线性映射，而是关注完全正映射。一个元素x∈A是正的，如果它可以写成x=y<$y的形式，其中y∈A。这些元素对应于量子可观测量。一个映射f：A→B，在底层向量空间之间是线性的，如果它保持正元素，则它是正的。一个线性映射是酉的，如果它保持乘法单位。一个线性映射f是完全正的，如果映射（Mk<$f）：Mk<$A→Mk<$B对每一个k都是正的。这使得我们能够对每个有限维C*-代数C定义一个函子C（−）。因此，有限维C*-代数和完全正单位线性映射构成一个对称幺半群范畴。 那里是对应于初始化量子数据、执行么正旋转和测量的完全正么正映射，并且实际上所有完全正么正映射都以这种方式出现（例如，[28、30]）。命题3.3三元组（FdC_p-Alg_op，Set，D）是EWire的一个模型，由有限维C*-代数的范畴FdC-AlgCPU和完全正-单位映射，集合和函数的Carnival闭范畴Set，以及集合上的概率分布单子D。事实上，它是QWire的一个模型，[[qubit]]def=M2和[[bit]]def=0。证据 参见附录C。Q迈向量子计算子集和变体的步骤C*-代数之间的完全正映射允许所有的量子运算，但有时人们会关注量子计算的变体，或一组受限的门，如稳定器门。定义3.4量子计算的一个类别是类别Q的一个子类M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257269.苏共1 0苏共C~*-代数与完全正酉映射的一个有趣的C ~*-代数CPU。为了协调一致，我们还要求：(i) 初始性：复数的C*-代数C在Q中。(ii) 矩阵代数下的闭包若A在Q中，则Mn<$A（n∈N）也是(iii) 态射矩阵下的闭包：对中的每对C ~*-代数（A，BQ，如果映射f在Q（A，B）中，则映射（Mn <$f）在Q（Mn <$A，Mn<$B）中。对类别Q的不同选择为我们的语言提供了不同的状态和幺正类，使Q成为例如，我们定义了一类量子计算，它只包含矩阵代数和由Cli Schoord群的稳定子态产生的完全正单位映射[26，Sec.1.3]。我们称这一范畴为Cli-量子力学;它对应于稳定子量子力学[2]，可以用经典计算机有效地模拟。然后，考虑到单量子位Cli ord群与门一起T=iπ0e4它可以近似任何单量子比特幺正，达到任意精度[5]，将由门T产生的完全正的单位映射T-T加到范畴Cli ordT的映射形成了一个范畴Cli ordT，它可以说是对应于量子理论的一个合理完备子集的最小范畴。4迈向量子域理论的一个W*-代数是单位区间为dcpo的有单位的C*-代数A，它有足够多的正规态，即正规的完全正的单位映射A→C.对于W*-代数和完全正的subunital映射的范畴，我们写W-AlgCPSU，它以Dcpo-丰富而闻名（参见例如[24]），其中Dcpo是点dcpos和Scott-连续映射的范畴。事实上，它的相反类别是QWire分类模型的一部分（如图所示在附录C中），当考虑Dcpo上的子赋值的单子V=dcGEmod（[0， 1]（− ），[0， 1]）的限制版本时（参见例如，[12，第5.6节]），其中dcGEmod范畴是有向完备广义ef-范畴fect模和Scott-连续的fect模同态， 作为量子谓词的一个类别[25，26]。提案4.1（ W/N- Algop，Dcpo，V）是QWire的分类模型。这一节的其余部分是专门调查的额外类别W-Algop. 我们认为，目前的工作是量子域理论发展的一个里程碑。 间-读者可以在附录C中找到证明。270M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257Ω=Ωinp：WWi124.1EWire的延伸为了能够处理求和类型和递归类型的输入和输出，让我们离开传统的电路概念：在下文中，电路是一阶线性指令。因此，我们的电路语言所操纵的结构不是电路本身，而是广义的电路。条件分支要使用条件分支扩展EWire，需要引入sum类型（即，W：：=···|WWJ和A：：=···|A + AJ），且对每对类型W1和W2，门在1∈ G（W1，W1<$W2）和2∈G（W2，W1<$W2）中.此外，我们还引入了case表达式（in1w1→C 1）的情形p|在2w2→C2）：W（其中p：W1<$W2，C1：Circ（W1，W）andC2：Circ（W2，W））并扩展了模式的文法：p：：=···|在1p|在2p那么，bit是11。 线型W <$WJ是经典的，如果W和WJ是经典的，则|WWJ|d=ef|W|+的|WJ|.和的模式使用Ω =Wp：Wii∈ {1， 2}消除，分支的类型规则如下：Ω=Ωp：W1<$W2Γ;w1：W1，ΩJ<$C1：WΓ;w2：W2，ΩJ<$C2：WΓ;Ω，Ω J是（1w1→ C 1）的情形p|在2w2→ C2）：W递归类型让我们完成导线类型和主机类型的语法W：：=···|X |μX.WA：：=···|X|μX.A一条线y ∈ μ X，如果W是经典的，|μ X.W|d=efμ X. |W|.我们假设G包含门foldμX.W∈ G（W[X<$→μX.W]，μX.W）founderμX.W∈ G（μX.W，W[X<$→μX.W]）它对应于递归型μX的折叠/展开.W.例如，对于由QList = μX定义的量子列表的类型QList。qubit<$X<$1，我们有fold∈ G（qubit<$ QList< $1， QList）和unfold∈ G（QList， qubit<$ QList<$1）。作为另一示例，QNatd=fμ X.X+1是自然数的线类型，并且Nat = μX.X + 1是自然数的主类型。QNat类型是经典的，|QNat|d=efNat.M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257271联系我们2m⊗⊗⊗与[8]一致，我们引入递归类型规则作为类型判断Θ<$τ，这意味着类型τ相对于不同类型变量Θ的上下文是良构的。我们引入以下一套判断类型的规则：θ1Θ，X，ΘjXθW1θW2②，θW1②W2Θ，XWθμX.W类型判断θ<$r成立，只要r是语言变量的上下文，使得Θ<$τ对每个变量（x：τ）∈r成立。在这一点上，人们可能会质疑在基于电路的语言中对递归类型的兴趣.在传统的电路概念化中，列表和其他无限数据类型必须以特定的长度实例化才能用作电路的输入类型，因此（iso）递归类型不能出现在电路的导线类型中。让我们通过关注模式p：QList来说明我们对递归类型模式的兴趣。 我们想实现量子傅里叶变换。 德-[22]第22话的启发6.2]和[10]，我们假设宿主语言常数CR：Nat→ Circ（qubit qubit，qubit qubit），使得（CRn）对应于控制绕z轴旋转2π 然后程序循环执行QFT电路的旋转和指令（傅立叶）对应于QFT，如引言中的电路所示旋转：长度：循环（QList、QNatQList）=框qs=>情况qsof []=>input（0，[]）| （q：qs'）=>（n，qsNat->Circ（量子位QList，量子比特QList）=一个月。box（c，qs）=>情况QS的 []=>input（c，[]）| （q：qs'）=>（n，qs <（c，qs（c，q）-unbox（CR（1+ m-n））（c，q）;输出（c，（q：qsFourier：Circ（QList，QList）=框qs=>情况QS的 []=>[]| （q：qs'）=>qs<-unboxfourierqs<（q，qs在这里，我们使用了一些递归类型和列表的标准语法糖。例如，长度被写得Y （ λl.boxqs=>qs- 展 开qs;caseqsofin2（）=> qs<-gatein1 （）;<-门 foldqs;z<-gatein1（）;z<-gatefoldz;output（z，qs）| in1（q，qs）=>（n，qs）-unboxlqs;qqs<-gate in1（q，qs）;qqs<-gatefold qqs;n<-gatein2n;n<-gatefolddn;输出（n272M. Rennela，S.Staton/Electronic Notes in Theoretical Computer Science 336（2018）257其中Y是一个定点组合子，使用递归类型定义。(This标准的QFT算法以逆序的方式保留列表，因此对于许多目的，该程序必须与标准的列表反转程序一起组成，在此省略在这里，我们考虑递归类型，因为它们是在列表上引入操作的一种快速方法，并且这些很快就适合我们的分类形式主义。缺点是在量子编程中，使列表的长度更明确是有用的。 例如，类型系统并没有告诉我们（unboxfourierqs）具有与qs相同的长度。这在Haskell等函数式语言中是一个常见的问题，但对于量子电路布局引擎来说尤其不方便。处理它的一个好方法是通过某种依赖类型[22，6.2]，例如允许大小为n的量子位数组的类型QArray（n）和傅立叶：（n：Nat）→Circ（QArray（n），QArray（n））。然而，下面讨论的是QWire的范畴模型，其中人们可以表示递归类型，利用我们打算用作量子域理论基础的前置层理论语义。因此，将依赖类型集成到EWire/QWire并将这些类型关联到适当的分类语义是留给未来工作的。4.2走向量子域代数紧性的概念提供了一种解释递归类型的方法。 一个DC