Lambda-S的范畴语义研究论文总结

SSS⊗|⟩|⟩⊗|⟩⊗|⟩⊗⊗可在www.sciencedirect.com在线获取理论计算机科学电子笔记344（2019）83-100www.elsevier.com/locate/entcsLambda-S的具体范畴语义Alejandro Díaz-Caroa，b，1，3 Octavio Malherbec，d，2，4a阿根廷布宜诺斯艾利斯贝尔纳尔奎尔梅斯国立大学b计算科学研究所（CONICET-Universidad de Buenos Aires），布宜诺斯艾利斯，阿根廷cDepartamento de Matemática y A Fines，CURE，Universidad de la República，Maldonado，乌拉圭dIMERL，Facultad de Ingeniería，Universidad de la República，乌拉圭蒙得维的亚摘要Lambda-是一阶lambda演算的扩展，统一了量子lambda演算中的两种非克隆方法。 一种是禁止变量的重复，另一种是考虑所有的变量项代数线性函数。Lambda的类型系统-有一个构造函数S，使得类型A被认为是向量空间的基，而S（A）是它的跨度。 这种演算的第一个语义在第一次提出时就已经给出了，有这样的解释：叠加类型被解释为向量空间，而非叠加类型则是它们的基础。本文给出了一个具体的范畴语义证明了S是C上集合范畴与向量空间范畴之间的一种伴随关系中的两个函子的合成。 右伴随是一个遗忘函子U，它隐藏在语言中，在 计 算 推 理 中 起着核心作用。保留字：量子计算，代数微积分，范畴语义1介绍量子计算的不可克隆性在量子程序设计语言中有不同的处理方式。一种方法是禁止复制线性类型的变量[1，12]，因此，一个接受量子参数的程序不会复制它（例如[3，14，17，20，22]）。另一种方法是将所有的非线性项都视为表示线性函数（例如[4第一种方法禁止使用项λx。（x x）（为了方便定义），而第二种方法分布（λx）。（xx））（0 +1）到λx。（xx）0 + λx。（xx）1，模仿线性运算作用于向量空间中向量的方式。然而，在线性代数方法之后将测量算子添加到微积分还需要添加线性1部分由PICT 2015 1208和ECOS-Sud A17 C 03 QuCa支持2由MIA CSIC UdelaR提供部分支助。3电子邮件：adiazcaro@icc.fcen.uba.ar4电子邮件：malherbe@fing.edu.uyhttps://doi.org/10.1016/j.entcs.2019.07.0061571-0661/© 2019作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。84A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83SSSE| ⟩|⟩|⟩|⟩−→| ⟩|⟩{|⟩|联系我们| ⟩| }类型：实际上，如果π表示测量算子，则（λx.πx）（0+1）不应简化为（λx.πx）0+（λx.πx）1，而应简化为π（0+1）。因此，取叠加的函数必须以某种方式标记，并确保它们不会使用它们的参数超过一次（即确保线性逻辑意义上的线性在[9]中引入了演算λ-，后来在[18]中略有修改，作为Lineal[6]的一阶片段，扩展了测量。在线性逻辑中，我们可以写A为不能重复的项的类型，！A键入可重复的术语。在λ中，A是不能叠加的项的类型，而S（A）是可以叠加的项，由于叠加禁止复制，A意味着我们可以复制，而S（A）意味着我们不能复制。 所以S和bang不一样！”,相反这可以解释为线性逻辑关注的是复制的可能性，而这里我们关注的是叠加的可能性，这意味着复制的不可能性。在[9]中，给出了第一个指称语义（环境风格），其中类型B被解释为0，1，而S（B）被解释为Span（0，1）= C 2，并且通常，类型A被解释为基，而S（A）是由这样的基生成的向量空间。在本文中，我们给出了Lambda-的范畴解释，其中S是范畴集和类别Vec。解释一下，当我们计算S时，我们得到了一个集合的元素的形式有限线性组合，其中复数作为系数，而附加函数的另一个函子U允许我们忘记向量结构。我们的模型的主要结构特征是它有足够的表现力，通过控制它的相互作用来明确地描述量子宇宙和经典宇宙之间的桥梁。 这是通过提供monoidal adjunction来实现的。在文献中，直觉线性（如在线性逻辑中）模型通过由monoidaladjunction（S，m）（U，n）确定的comonad获得，即bang！”（《论语·系辞下》），《论语·系辞下》。 以不同的方式，我们模型的一个关键要素是考虑单子US，用于解释S，由下式确定：一个类似的么半群的附加。这意味着，一方面我们严格控制了模型的笛卡尔结构（即复制等），另一方面叠加世界在某种意义上存在于经典世界中也就是说，在我们决定探索它之前，它是由经典规则从外部确定的。这是由以下映射的合成US（B）×US（ B）−n→U（S（ B）<$S（ B））U（m）US（B× B）它允许我们在一个代表量子世界的幺半群结构中操作，然后回到笛卡尔积。这与线性逻辑不同，在线性逻辑中，经典世界在某种意义上生活在量子世界中，即。（啊！B）（！B）是monoidal范畴内的乘积我们模型的另一个灵感来源是Selinger [19]和Abramsky和Coecke [2]的工作，他们在更抽象的范畴设置中捕获了标量和内积的概念，即。一个类别，A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8385S−→ ǁ···ǁ→¨¨B{|∈} QTBQǁǁ：= B n|S（）|量子比特类型（Q）A：=0|Ψ⇒ A |S（A）类型（T）b：= x |λ x：λ.t ||0⟩||1⟩|b × b基本条款（B）v：= b|（v + v）|0S（A）|α.v |v × v值（V）t：=v|TT|（t+t）|πjt|什么？t·t|α.t|t×t|头部t|尾部t|布雷尔特|T（Λ）p：=p1 t1··pntn概率分布（D）其中α ∈ C，pi ∈[0，1]<$R.一个匕首函子的抽象概念据设想，这一办法将为今后工作中的抽象模型提供基础本文的结构如下。在第2节中，我们回顾了λ的定义，并给出了一些例子，说明了它的主要性质。第三节分为三个小节：首先我们定义了解释微积分所需的范畴结构，然后我们给出了解释，最后我们证明了它的可靠性和充分性。最后，我们在第4节中结束。在arXiv5的预印本中可以找到一个带有详细证明的附录。2微积分Lambda-S我们在[18]的基础上给出了一个稍微修改的Lambda-S表示。特别地，不是给出概率重写系统，其中tpkrk意味着t以概率pk减少到rk，而是引入符号tp1r1pnrn，这样，重写系统是确定性的，并且概率分布被内在化在语法中。术语和类型的语法如图2所示。 我们把B n写成B ×···× B n-倍，与公约，B1B，可以写为ni=1皮蒂，因为p1t1 ǁ · · ·ǁ pntn的约定的情况1i=1 1t=t. 我们使用大写拉丁字母（A，B，C，.. . ）的方式对于一般类型，大写希腊字母、Φ、和表示量子位类型。=B n nN，是量子比特类型的集合，是类型的集合（ÇÇ）.同样，Vars是变量的集合，B是基项的集合，V是值的集合，Λ是项的集合，D是项的概率分布的集合。我们有瓦尔斯·B·V·A·D。图1：Lambda-S的类型和术语列表.这些项被认为是同义符号+的模结合性和交换性。另一方面，符号是用来表示项的真实概率分布，而不是作为句法符号，因此，它不仅是结合的和交换的，我们还知道pt <$qt与（p + q）t相同，pt <$0r = pt6。5http://arxiv.org/abs/1806.09236。6作为一个注释，注意可以被看作是代数lambda演算[]的+符号，其中等式是连续的，因为标量是正的，而我们的+符号与Lineal[6]中的+一致。=86A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83··⇑⇑| ⟩|⟩··|⟩|⟩⇑222222有一种原子类型B，用于基础量子位|0次|1个，3个构造函数：对于对，为×;对于一阶函数，为;对于叠加，为S（·）术语的语法包含：• 一阶微积分的三个基本术语，即变量、抽象和应用。• 两个基本术语0和1代表量子位，一个测试？R在他们身上。 我们可以写t吗？r s for（？r s）t，请参见例2.1，以澄清为什么选择此演示。• 乘积×表示关联对（即列表），其析构函数头和尾巴。 我们可以用这个符号|b1b2... bn为|b1× |b2×···× |bn.• 构造函数用于编写项的线性组合，即+（sum）和。（标量乘法），其析构函数πj测量作为量子位列表的线性组合写入的第一个j个量子位，每个类型S（A）有一个零向量0S（A）。• 两个转换函数r和l，允许我们把叠加列表看作列表的叠加（见例2.2）。重写系统还没有给出，但是下面的例子给出了一些直观的说明，并澄清了？r·s和铸造函数。例2.1术语？r s的意思是测试条件是1还是0。然而，将其定义为函数，允许我们使用代数线性来实现量子如果[3]：（？r·s）（α. |1 π + β。 |0 π）=（α. |1 π + β。 |0分）？r·s −→ α。|1 ⟩? r·s +β。|0 ⟩? r·s−→<$α.r+β.s2012年12月22日，《2012中国（|0人以上|1））×|01-02|0人以上|0分。|0⟩. 2016年10月14日，《中国日报》（|0人以上|1）|01-0|0⟩⊗|0人以上|1⟩⊗|0分），该术语将不会重写为它的编码，除非在该术语之前有一个转换r1∗12012年12月22日，|0人以上|1））× |0− →2（|0 ⟩ × |0人以上|1 ⟩ × |0分）这是因为我们没有使用术语（101），|0人以上|1））×|0表示具有p e S（B）× B，突出了第二量子位是基础量子位的事实，即可复制的，而项1表示具有p e S（B）× B，突出了第二量子位是基础量子位的事实，即可复制的，而项1表示具有p e S（B）× B，突出了第二量子位是基础量子位（|0⟩ ×|0人以上|1⟩ ×|0π）将有一个ve e S（B ×B），表明整个项是一个叠加，其中没有信息可以提取，因此，不可复制。重写系统依赖于类型。实际上，λx：S（n）.t遵循按名称调用策略，而λx：B.t，可以复制其参数，必须遵循按基调用策略[7]，即不仅参数必须首先被约简，而且它将分布在线性组合上。因此，我们首先给出类型系统，然后给出重写系统。图2中给出了类型关系。上下文，由大写希腊字母Γ、Δ和Θ标识，是从Vars到T的部分函数。上下文赋值(see[7]对于代数lambda演算的不同表示进行了更详细的讨论A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8387BΘB，x：θ BAxΘB0S（A）：S（ A）轴0ΘB|0分：BAx|0⟩ΘB|1分：BAx|1⟩T：S（ A）Γα.t： S（ A）αⅠΓ，ΘBt： S（ A）Δ，ΘB u：S（ A）Γ，Δ，θθ θ（t+u）： S（ A）B+I联系我们Γnt：Sk（Bn）k>0SEΓt： S（ A）Γπ t： B×S（ B）SIJjn−j联系我们r：AIfΔ，ΘB u：Γ，ΘBt：θB A Δ，ΘB u：S（θ）Γ，ΘBt：S（θ A）你呢？t·r：B AΓλx：λ.t：λAΓ，x：λt：AIΓ，ΘBt：Δ，ΘBu：Φ ×Δ，Γ，ΘBEΔ，Γ，ΘBΔ： S（ A）ESΓ，Δ，ΘBλt×u：λ×Φ我nn>1r压头t： B×Er×Elr尾t： Bn−1nn>1Γt： S（ S（）×Φ）<$Γt： S（×S（Φ））<$t i：Ap=1个Σ我我RLΓrt：S（×Φ）Γt：S（×Φ）p1t1ǁ若b有Bn型且b∈B，则（λx：Bn.t）b−→（b/x）t （βb）若u有S（λ）型，则（λx：S（λ）.t）u −→（u/x）t（βn）如果t有类型Bn<$A，则t（u+v）−→（tu+tv）若t有Bn<$A型，则t（α.u）−→α.tu若t有类型Bn<$A，则t0S（ Bn）−→0S（ A）（t+u）v−→（tv+uv）（α.t）u−→α.tu（lin+）R（linα）R（line0）（linl）（linR+α（line0）L只有中的类型用超索引B标识，例如ΘB。 当一个类型规则中出现多个上下文时，它们的域被认为是成对不相交的。观察到所有类型都是线性的（如线性逻辑），除了基础类型Bn，它可以被削弱和收缩（由公共上下文ΘB表示）。图2：类型关系重写关系如图3至图10所示。根据参数的类型应用两个beta规则（图3如果抽象期望一个具有叠加类型的参数，那么归约遵循按名称调用策略（规则（βn）），而如果抽象期望一个基类型，那么归约是按基调用（规则（βb））：它仅在其参数是基项时进行β然而，类型化规则也允许类型化一个抽象，期望一个具有基本类型的参数，应用于一个具有叠加类型的术语（参见。实施例2.3）。在这种情况下，beta降低不会发生，相反，应用程序必须使用图4中的规则进行分发：线性分发规则。图5给出了条件构造的两条规则。 与线性分布规则（cf.图4），这些规则实现了量子-如果图3：Beta规则图4：线性分布规则88A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83×| ⟩×|⟩| ⟩× |⟩××| ⟩× |⟩|⟩如果h/=u×v且h∈B，则headh×t−→h（head）如果h=/ u×v且h∈B，则尾h×t−→t（尾）（0S（ A）+t）−→t1.t−→t如果t有类型A，0.t−→0S（ A）α。A = 0S（ A）→ A =0 S（ A）α。（β.t）−→（ αβ）.tα。（t+ u）−→（ α.t+ α.u）（α.t+β.t）−→（α+β）.t（中性）（ 单位）（零α）（零）（ prod）（ 事实）12|一毛钱？t·r −→ t（if1）|000？t·r−→r（if0）图5：条件结构图6：列表规则图7：实现向量空间公理（参见： 实施例2.1）。图6给出了列表的规则，（头）和（尾）。图7处理实现向量空间公理的有向版本的向量空间结构。 选择方向是为了产生标准形式[6]。图8是实现铸件的规则。这个想法是，不相对于+分布，除非铸造允许这样的分布。这样，B型S（B）和S（BB.不同的。 的确，0（0+1）具有第一个类型，但不是第二个，而00+01有第二种，但不是第一种。这样，第一种类型给我们的信息是状态是可分离的，而第二种类型没有。我们可以选择将第一个状态作为一对量子比特，通过转换其类型来忘记可分性信息，就像在某些编程语言中可以将整数转换为整数一样（因此，忘记它确实是整数而不是任何整数的信息图9给出了相对于基底{|0分，|{1}。在这个规则中，我们使用以下符号：[α。]t可以是t或α，tj≤m|b1 × · ··×|其中b 1.. |bj⟩whereb1.. . bj是k的二进制表示A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8389Σ| ⟩×2R22BB22ββnMπ（[ αJ Σ我. ]|b）−→pk（|k×|φk）（proj）2j−1嗨i=1h=1k=0¨i∈Tkr（r+s）×u −→（lu×（r+s） −→（r（α.r）× u −→ α。 rr × ulu ×（α.r）−→ α。 r u × r如果u有类型φ，则φr0S（Φ）×u−→0S（Φ× φ）如果u有型φ，则φlu×0S（Φ）−→0S（φ ×Φ）（t+u）−→（t+u）（α.t）−→ α。阿勒特<$r0S（ S（ S（））×Φ）−→ <$r0 S（ S（）×Φ）r0S（ S（ Bn）×Φ）−→0 S（ Bn×Φ）<$l0S（<$x S（ S（Φ）−→ <$l0 S（<$x S（Φ））l0S（如果u∈B，则<$ru×v−→u×v如果v∈B，则<$lu×v−→u×v（ distr）（distl）（dist++αα（0）R（0）（dist）L+（dist）α（distr）（ neut0r）（ dist）（neut0l）（ neutr00图8：铸件尺寸和尺寸的规则图9：投影规则Σ⎛αi⎞2|φk φ=i∈Tk - 是的Σr∈Tk|αr|⎠h=j+1|bhi⟩- 是的 |2Σ|2 ΣT k ={i ≤ n ||b1 i ×···× |b ji = |k}这边，pk|k× |φk是项的归一化第k个投影。最后，图10给出了实现按值调用和按名称调用策略的上下文规则。例2.3术语 λx：B.xx并 不代表克隆机， 而是一个辅助量子位为 0的CNOT。的确，（linα）（λx：B.x×x）1. （|0人以上|1）−→r（林+）−→2001年。（λx：B.x×x）（|0人以上|1个月）2001年。（（λx：B.x×x）|0+（λx：B.x×x）|1个月）−→1。（|0⟩×|0+（λx：B.x×x）|1个月）−→1。（|0⟩×|0人以上|1⟩×|1个月）Mpk=nr=1 |αr|290A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83|0⟩|1⟩22►|⟩► |⟩► |⟩×S2−→ 14|1010142222如果t−→u，则tv−→uvα.t−→α.uv× t−→ v× u磁头t−→磁头 u（λxBn.v）t−→（λxBn.v）uπj t−→ πj urt−→tailt−→tail u（t+v）−→（u+v）t× v−→ u× vlt−→r·s−→u？r·s（p1t1···pkt···pntn）−→（p1t1···pku···pntn）图10：上下文规则类型推导如下：轴轴x：Bx： Bx：Bx： B×IAx► |0⟩: BSIAx► |1⟩: BSIx：Bx×x：B2► λx：B.x×x： B<$ B2► |0：S（B）|1：S（B）+I► |0人以上|1π：S（B）αSI► λx：B.x×x：S（ B<$ B2）► 2001年。（|0人以上|1分）：S（B）我⇒ES► （λx：B.x×x）1. （|0人以上|1分）：S（B2）例2.4π2项测量了它的辐角的前两个量子比特（在例3.7中我们给出了更详细的解释）：π（|001米+2. |110米+3米。 |10000×（1000）（预计） |1分+3分 。 |0分）14分|11×（1.|0分）类型推导如下：► |1分：B► |1分：B► |0分：B×► |0分：B► |0分：B► |0分：B×0：B0：B1：B我3►|110米：B3► |110⟩ : S (B3)3► |000⟩ : B 3► |000⟩ : S (B3)3►|001乙：乙α► |001⟩ : S (B3)2002年。|110⟩ : S (B)► 3. |000⟩ : S (B )+►二、|110米+3米。|001：S（B3）►|001⟩ +2. |110米+3米。 |001：S（B3）► 12 - 13（|001米+2. |110米+3米。 |001）：B2×S（B）例2.5阿达玛门可以通过H = λx：B.x？|+，其中|+=1。|+⟩=√1. |0分+1分。|1、|-=1。 |0-100 |1美元。因此，H：B<$S（ B）我们有H|0⟩ −→∗|+和H|1⟩ −→∗|- 是的正确性已经建立在以前的作品略有不同的版本的λ-，除了的情况下，我+ISE我我我SIαⅠSIαⅠ我A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8391concuruence，这只被证明为线性。Lineal可以被看作是一个没有几个构造的无类型片段（特别是没有πj）。Lambda-的一致性证明被推迟到未来的工作中，使用[10]中概率一致性的发展。证明92A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83S¨¨►a∈Ab∈B（a，b）∈A×B主题约简和强规范化是从Lambda-S的不同表示的证明中直接修改的。定理2.6（线性的连续性，[6，Thm. 7.25]）Lineal是Lambda- S的一个未定型片段，是conciliuent。Q定理2.7（闭项上的主体归约，[9，Thm. 2]）对于任何闭项t和u和类型A，如果t−→ipiui和t：A，则ipiui：A.Q定理2.8（强正规化，[18，Thm.5.16]）如果Γt：A，则t是强正规化的。Q3指称语义尽管本文的语义是关于特定的范畴，即集合的范畴和向量空间的范畴，但从一开始我们的方法就是抽象的范畴。我们的想法是，本文中揭示的具体情况将为更抽象的表述铺平道路，这就是为什么我们尽可能抽象地给出这些结构。一个更一般的处理，使用一个monoidal的附加之间的笛卡尔闭范畴和monoidal范畴与一些额外的条件，仍然是一个主题，为未来的出版物。定义3.1λ-的具体分类模型由以下数据给出：• 幺半群的附加（Vec，Vec，I）哪里· Set是以1为终端对象的集合的范畴。· Vec是C上的向量空间范畴，其中I=C。S是函子，使得对于每个集合A，S（A）是向量空间，其向量是形式有限线性的（S，m）E（U，n）A的元素与C中的系数的组合，并且给定函数f：A→B，我们通过在A中对f求值来定义S（f）：S（A）→S（B）。（组，×，1）U是遗忘函子，使得对于每个向量空间V，U（V）是V中的基本向量集，对于每个线性映射f，U（f）忘记其线性性质。· m是自然同构，定义为mAB： S（ A）<$ S（ B）→ S（ A× B）（<$αa a）<$（<$βb b）›→<$αa βb（ a，b）·n是由nAB定义的自然变换：U（V）×U（W）→U（V<$W）使得（v，w）›→v<$w。• 有一个Vec的子范畴，使得对于每个态射f：V→W，人们关联一个态射f<$：W→V，称为f的匕首，使得对于所有··A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8393不Σ2[t，r]R→→−→−→线性变换→，明确给出了，× →›→∈||Σ− ×E −i=1i=1f：V→W和g：W→U，我们有Id<$V=IdV（gf）<$=f<$g<$f<$<$=f• 一个Kleisli范畴，用下面的单子定义，称为分布单子，（D，η，μ）：n nD：集合→集合D（A）={ApiXai|n∈N，ai∈A，n∈N}其中，χa是a的特征函数，η和μ定义如下：η：A→D（A）μ：D（D（A））→D（A）a›→1 χanpixmi→›卢恩 穆尔姆岛piqijxaij备注3.2i=1（j=1qijxaij）i=1 j=1• 为了处理测量的概率效应，我们的语义需要分布单子的概念（见[13，16]）。为了给出更抽象的范畴描述，我们考虑由这个单子给出的Kleisli范畴，其中态射f：AKleisli范畴中的B实际上是一个态射f：AD（B）在范畴Set中，对应于一个B型计算.• 存在一个对象B，在Set中映射i1，i2，使得对于每个t：1一和r：1A，这里存在唯一的映射[t，r]，使得下图1i1Bi1一这个对象B是布尔集合，这样的映射将允许我们解释if构造（定义3.5）。• Set中存在一个映射+：US（A）US（A）US（A），由（a，b）a+b给出其中我们使用定义在S（A）中的和。• 有一个附加意味着每个函数g：A→U（V）扩展到一个唯一的f：S（A）Vf（ iαixi）=iαig（xi）即S（A）中的形式线性组合到V中的实际线性组合（详见[15]）。• 对于每一个ASet，Vec（I，S（A））都是一个阿贝尔群，其和是逐点定义的。• 集合是一个笛卡尔闭范畴，其中ηA是单位，εA是A[A，]的计数，从中我们可 以 定 义 任 何 映 射 的 curry fication （ curry ） 和 un-curry fication（uncurry）。• 定义3.1中的附加在范畴Set中产生一个单子（T，η，μ），其中T=US，η：Id→T是附加的单位，使用计数ε，我们得到μ=U εS：TT→T，满足单位律和结合律（见[15]）。94A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）831λx.i12t，rλx.i2（）（）（）∈--|⟩→| ⟩2ǁ−→ 14|1010141010定义3.3类型在集合范畴中的解释如下：B= BA=AS（A）=USA×Φ=×Φ注3.4为避免繁琐的记法，我们将使用以下惯例：我们直接写信给US（A），S（A）=US（A）和A对于A，当没有模棱两可（）（）（）在解释模型中的类型派生树之前，我们需要定义某些映射，这些映射将用于实现语言中的一些结构。为了实现if构造，我们定义了下面的map。定义3.5给定t，r∈[Γ，A]，存在一个映射Bft，r[Γ，A]在定义的集合byft，r=[t，r]其中t：1→[r，A]且r：1→[r，A]ar−e→givenbyt=λx.t且s=λx.s。 具体地说，这意味着i1（*）<$→t和i2（*）<$→r。例3.6考虑t=i1和r =i2，其中t，r[1，B]，其中B=i1（*），i2（*）.为了使例子更清楚，让我们考虑i1（*）=0，ft，ri2（*）=|1，因此B ={|0分，|{1}。集合中的映射B−→[1， B]定义为：ft，r=[λx.i1，λx.i2]，其中λx.ik：1[1，B]，k = 1，2. 因此，我们有以下通勤图因此，我们有1B1F[1，B]f t，r|0= f t，r（i i（））=（i i f t，r）=（λx.i1）= i 1= t f t，r|1λ= f t，r（i 2（λ））=（i 2λ f t，r）λ =（λx.i 2）λ = i 2= r因此，ft，r是映射|0→t和|1⟩ ›→ r.投影πjk的作用方式如下：首先，它将其自变量的前j个分量（一个n维向量）投影到j维向量空间中的基向量k上，然后将其重正化，最后将前j个分量因式分解。然后，投影πj取2j个投影仪πjk之间的概率分布，这些概率中的每一个从要投影的归一化向量计算。例3.7让我们分析例2.4：π（|001米+2. |110米+3米。 |10000×（1000）（预计） |1分+3分 。 |0分）14分|11×（1. |0分）我们可以把它分成四个投影仪（因为j=2，我们有2个2投影仪），这是平行的（与符号）。四个投影仪是：π2，00，π2，01，π2，10和π2，11。在这种情况下，投影机π2，01和π2，10的概率为0，因此它们不会出现在最终项中。投影仪π2，00的作用如前所述：首先，它投影的前2个组件|与基向量的距离|00分，获得|001年3月。 |000美元。 然后将其重新正规化，通过除以其范数，得到φ1。|001⟩ + √3. |000⟩.最后，它分解了A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）839514=.| ⟩但是，⎪⎩ΣΣ.向量，获得|00×（1. |1分+3分。|0分）。类似地，投影仪π2，11给出|11⟩ × (1. |0分）。10 10最后，组合最终项的概率由p0=|2个以上|3|2|2|2个以上|2|2个以上|3|2|2=10且p1=|2|24|2个以上|2|2个以上|3|214|214从范畴上讲，我们可以用三个箭头的组合来描述算子πjk（定义3.11）：归一化箭头Norm（定义3.8），到k基向量的投影箭头，以及分解箭头j（定义3.9）。然后，投影πj（定义3.14）将向量映射到2j个基向量之间的概率分布|k，使用分布图（定义3.12）。在以下定义中，如果|是一个n维向量，我们写|我：我→S（B n）在地图上1›→|好吧定义3.8归一化箭头Norm的定义如下：标准：US（B n）→ US（B n）|ψ⟩ ›→|ψ⟩（|ψ⟩†◦|ψ⟩)(٨)如果|0.00000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000|0⟩otherwise定义3.9分解箭头j被定义为使下图交换的任何箭头：Bj×US（Bn−j）IDBj×US（ Bn−j）η×IdUS（Bj）×US（Bn−j）拉吉U（S（Bj）<$S（Bn−j））U（ m）US（Bn）=US（ Bj×Bn−j）例3.10例如，取如下映射：j：US（Bn）→ Bj×US（ Bj− n）a›→⎧⎪⎨j|bh⟩×n i=1αi。nh=j+1n.96A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83⎪⎩-|⟩−|bi h⟩Σ如果a=n i=1αi。Jh=1 |bh⟩ ×n h= j+1|bih⟩Σ|0⟩notherwise定义3.11对于每个k= 0，...， 2j1，到k个基向量的投影，πjk，定义为使下图交换的任何箭头：US（Bn）<$=U（S（B）<$n）U（（|k|k<$<$）<$I）U（S（B）<$n）<$=US（Bn）πjkBj×US（Bn−j）规范美国（Bn）其中同构mUs（Bn）n=U（S（B）n）是通过将n乘以中介箭头m，然后应用函数U得到的。下面的分布图将允许集合定义3.14中投影的最终分布。h=1JA. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8397ΣΣ× →×◦ ◦ ◦◦2 3 6×236πjk|ψ⟩⎧⎪⎨|0×（α1. |0μ m+α2。 |1）如果α3=α4=0i=1定义3.12设{pi}n是一个集合，pi∈[0，1]，且ni=1pi=1。 然后我们将d{pi}i定义为箭头d{pi}i：An→D（A）使得（a1，.，an）› →npiχa.我例3.13考虑d{1，1，1}：B3→D（ B3），定义为d{1，1，1}（b1×b2×b3）=1×b+1×b+1×b。23 623 6213263例如，d{1，1，1} |101× =1×|1×+1×|0×+1×|1美元。定义3.14πj是箭头πj：US（Bn）→D（Bj×US（Bn−j）），使得|ψ⟩ ›→2j−1p χ其中p=Norm（|ψ⟩)† ◦P◦ 标准（|与P=（|k|k）Idπjk是定义3.11中给出的箭头。例3.15考虑集合B2和向量空间S（B2）.我们可以将投影π1描述为映射π1：US（B2）→D（B×US（B）），使得|ψ⟩ ›→p0χπ10|100+p1χπ11|在哪里，如果|α=α1。|00⟩ + α2. |01⟩ + α3. |10⟩ + α4. |11⟩,thenp=0|α1|2个以上|α2|2和p=|α3|2个以上|α4|二、04i=11|2 |24i=1 |2|2Norm箭头是箭头Norm：US（B2）→US（ B2），使得α1α2α3α4α1。 |00度+α2。 |01+α3. |10μ m+α4。 |第11章→Σ4|二、|2.|00+。Σ4我|二、|2. |01 - 01-01 Σ4我|二、|2. |10块+。Σ4我|二、|2 .|11⟩我因子分解箭头是箭头1：US（B2）→ B×US（ B），使得α1。 |00度+ α2。 |01+ α3. |10 μ m +α4。 |11 ⟩ ›→|1⟩ × (α3. |0⟩ + α4. |1⟩) if α1 = α2= 0⎪⎩|00分，否则最后，π10和π11被定义为π10：US（B2）→ B×US（ B）和π11：US（B2）→ B×US（ B），使得2019-01 - 22 00：01：0100：0100：00|0 ⟩◦ |11 -12-1|1 ⟩◦|（1）我们写（US）m（A）for US（. US（A）），其中m > 0且A US（B）。的（US）m（A）上的箭头和将使用向量空间S（A）中的基础和。因此，为了实现这个和，我们需要下面的映射。定义3.16映射gk：（US）k+1（A）（US）k+1（A）（US）k（US（A）（A）定义为gk=（US）k−1U（m）<$（US）k−1（n）<$（US）k−2U（m）<$（US）k−2（n）<$··<$U（m）<$n例3.17我们可以定义（US）3（A）（US）3（A）上的和，用S（A）上的和为g2（US）2（+），其中g2=USU（m）US（n）U（m）n。这给出了下图USUSUS（ A）×USUSUS（ A）总和U（m）U（SUSUS（A））U（SUSUS（A））US（USUS（A））×USUS（A））i=1k=0KKKKi=1i=1i=1i=1n98A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）83美国（n）USUSUS（ A）USUS（+）USUS（ US（ A）×US（ A））USU（m）USU（SUS（A）（A））A. 迪亚斯-卡罗岛Malherbe/Electronic Notes in Theoretical Computer Science 344（2019）8399| ⟩=Γ−→B−→B−→Bm−1T：S（ A）Σ×B× ×BBN头−→BΓ，x：ππx： π−→= Γ−→（US）（一）−→（美国）U（ S（ A））−→Γ× Δ× Ξ×Ξ−→Γ ×Ξ×Δ× Ξ.=Γ−→（US）k（Bn）−→US（Bn）−→D（Bj×SBn−j）Γcurry（uncurry（ft，r））[B，A]Γ，x：λt：AηΨ[Id，t]Bm >0且AS（B）。我使用前面所有的定义，我们最终可以给出模型中类型派生树的解释如果Γt：A有一个导子T，我们一般地写它不当Γ−→A时， 在下面的定义中，我们写Sm（A）为S（…S（A），其中（T）定义3.18如果T是类型派生树，我们归纳地定义T如下：B轴 =ΓB×π！其中Id是）集合中的标识ΓB► 0S（A）：S（ A）Ax0=ΓB−→！1λ−x→。0US（A）轴0B！Γ ► |0分：B1λx。|0⟩ΓB|1分：BAx|1π=ΓB−→！1λx。|1⟩V：Sm（ A）Mtm（US）m−1U（λ）m−1Γα.t： S（一）（US）m−1U（Idα）−→（US）U（ S（ A）I）（US）m−1U（