概率重写中的Confluence分析

可在www.sciencedirect.com在线获取理论计算机科学电子笔记338（2018）115-131www.elsevier.com/locate/entcs概率重写中的Confluence [编辑]亚历杭德罗·迪亚斯-卡罗a，b，1 吉多·马丁内斯c基尔梅斯国立大学罗克·萨恩斯·佩尼亚352 B1876BXD Bernal，布宜诺斯艾利斯，阿根廷b CONICET-布宜诺斯艾利斯大学。大学城计算机科学研究所1C1428EGA布宜诺斯艾利斯，阿根廷adiazcaro@icc.fcen.uba.arc CIFASIS-CONICET&罗萨里奥奥坎波和埃斯梅拉达国立大学，S2000 EZP。阿根廷圣达菲罗萨里奥martinez@cifasis-conicet.gov.ar摘要式出于对概率编程语言推理的兴趣，我们开始研究它们的范式的独特性的一个概念。 为了提供一个可跟踪的证明方法，我们定义了一个属性。分布影响，其被示出为实现期望的唯一性（即使对于分布的无限序列，也是如此）。还原）和进一步的属性。然后，我们从经典案例中借用了几个标准，比如纽曼的引理，以简化证明对特定语言的影响。使用这些标准，我们得到了λ1（一种概率λ-演算）和Q*（一种量子编程语言，其相关性质已经在文献中得到了证明）的一致性的简单证明。关键词：抽象重写系统，概率重写，影响力，影响力。1介绍性在编程语言的正式研究中，通过一个小步骤操作语义学来建模执行是一个流行的选择。这样一个语义是由一个抽象重写系统（ARS）给出的，从数学上讲，它只不过是一个关于术语的二进制关系，具体说明一个术语可以重写到另一个术语。此关系不是函数所必需的，因此可以允许程序以两种不同的方式进行重写。[10]在这种情况下，重要的是给定程序的不同执行路径达到相同的最终值（如果有的话）;这保证了语义（即策略）的任何两个确定性在每个程序中都是一致的。这种正确性属性可以在关系层面上表达，并且是已知的。作为范式的唯一性（UN）：从一个范式可达的任何两个不可约项。1部分由ECOS-Sud项目A17 C 03 QuCa和PICT 2015-1208支持https://doi.org/10.1016/j.entcs.2018.10.0081571-0661/© 2018作者。出版商：Elsevier B.V.这是CC BY许可证（http://creativecommons.org/licenses/by/4.0/）下的开放获取文章。116A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115-{}{-}公共起始点必须相等。\n\n对于非平凡语言，如λ- calculus，可能很难直接证明这个属性。幸运的是，confluence的性质可以作为它的证明方法，因为它微不足道地意味着UN，但它的证明往往更容易追踪。这是Church和Rosser在[4，Corollary 2]中采用的方法，其中UN和confluence在1936年首次被证明用于λ-演算。如今，confluence被广泛用于在许多类型的编程语言中显示操作语义的充分性。自从几十年前以来，人们对概率编程语言的兴趣越来越大[12，16]，特别是那些还原本身是随机的语言。这些语言的特性已经被研究过，特别是从一种与语言无关的重写方法[1举个例子，采用前一种方法，[1]你引入了重写系统的概率终止的概念，并提供了证明它的技术按照后来的方法，[9]采用一个非确定性的λ-演算，用概率的按值调用和按名称调用操作语义（每一种都是小步和小步风格）对其进行填充，并通过CPS转换证明它们相互模拟，遵循Plotkin[21]的经典结果。我们在这篇论文中的重点是概率约简和非确定性之间的相互作用，后者来自不同的可能约简选择。例如，当给定的程序包含两个可约子表达式时，存在这样的选择，其中每个子表达式都是概率性的。在这种情况下，程序可以根据选择采取一个步骤来实现两个不同的归一化分布。鉴于这种非决定论，一个自然的问题是问一个程序的结果是什么（什么？）是值的分布[16]）不是由策略定义的，类似于古典语言的UN。这正是我们在这里要研究的属性，为它开发了一个相关的影响力概念。虽然这个相同的属性已经在文献中进行了研究[8，11]，但它只针对特定的语言进行了研究，因此以前缺乏与语言无关的研究。此外，所采用的技术并不立即适用于其他计算方法。在更抽象的层次上，也有其他关于概率设置中的冲突影响的研究[3，15]，但这些概念与我们前面描述的有根本的不同，并且对编程语言的使用有限。对于一个具体的例子，让我们取一个假设的语言来表示模具卷，其中Q表示一个未卷的模具，它可以还原为任何元素。{1，...，6}具有相等的概率，"−"表示减法。对于一对骰子（Q，Q），应该允许选择哪一个掷得最快。滚动第一个骰子可以在集合（i，Q）i=1，6中的任何项上以相等的概率给出;对于第二个骰子也是如此。当继续滚动时，两个备选项提供相同的均匀分布。然而，这可能不是这样的：考虑项（λx. xx）Q。如果模具在β-还原之前滚动，结果只能是0，但如果首先进行β-还原，得到（Q，Q），最终结果可以是5中的任何数字，......，5.我们稍后将提供类似的语言，并提供条件以避免这种差异。大纲。 在§2中，我们介绍了概率重写和唯一性问题。A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115117×分布的强度。在第3节中，我们定义了一个重写发行版的系统，以提高我们的影响力，并证明它是适当的。在§4中，我们推导出一个标准，简化了特定语言的证明分发任务。在§5中，我们将我们的一些结果扩展到无符号终止项。在§6中，我们证明了两个具体演算的影响：一个简单的概率演算dubbedλ1和量子λ演算Q*[8]。最后，在第7节中，我们总结了一些关于未来方向的见解，并分析了一些相关的工作。2概率性重写（英语：Probabilistic Rewriting）2.1初步的。我们假设熟悉抽象的重写...我们采用了[4]中的术语，并将一系列扩张之后的一系列还原称为峰值。当顺序被颠倒时，这样的序列被称为山谷。因此，汇合的性质可以表述为"所有的峰都有一个谷"。 当一个ARS A是冲突的，我们注意到它由A|= CR，对于UN和其他属性也是如此。关系R模E，记为R/E，对于任何等价关系E定义为E·R·E[14，20]。我们用L（X）表示具有X中元素的有限列表的类型，其中我们还使用符号[a，b，c]表示a：b：c：[]。我们定义D（A）=L（R+A），用作（有限支持的）分布的显式表示。D（A）没有进一步的限制。 特别地，任何给定的元素可能出现超过一次，如[（1/3，a），（1/2，b），（1/6，a）]。对于分布中的一个点（p，a），p称为权重和元素。The一个分布的权重被定义为它的所有点的权重之和，并且可以是任何正实数的值。 当需要标准化分布时，我们使用类型D1（A），定义为具有单位权重的那些d她家D（A）我们缩写分布[（p1，a1），（p2，a2），...， （p n，a n）] by [（p i，a i）]i，其中n应该从上下文中清除。我们也写αD表示通过将D中的每个权重按α缩放而得到的分布;即，α[（pi，ai）]i=[（αpi，ai）]i。为了解释分布的等价性，我们定义了一个关系"FlI p[（p，a），（q，b）][（q，b），（p，a）]JoI N[（p，a），（q，a）][（p+q，a）]SplI t[（p+q，a）][（p，a），（q，a）]注意，Ω是对称的，因为J是S分裂的逆，F是它自己的逆。我们通过限制可能使用的规则来区分~的一些子集。我们注意到，对于S，S分裂的全等闭;对于（FJ），FLIP和JOI n的全等闭;对于其他子集，也是如此。我们称两个分布等价，当它们通过约的反射传递闭包相关时，记为""。两个分布是等价的，因此，精确地，当它们将相同的总权重分配给每个元素时，不考虑顺序和118A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115>>P×›→PT›→多重性。可以说，使用这样一个分布和等价性的定义比使用一个语义上更明确的定义更容易和更不清楚。然而，我们觉得这是过度的严格程度参加了后来的证明（特别是因为我们发现他们中的一些人是quite容易出错）。作为一个次要的好处，我们的大部分发展应该是直接向前的机械化，因为所有的等效步骤都是明确的。使用列表的一个切实的缺点是只能表示有限支持的发行版。[10]这种限制（对于无限减少序列无论如何都是提升的）在其他作品中也存在（例如[10，22]），并且对于建模编程语言来说似乎并不严重。2.2概率抽象重写系统（PARS）[编辑]为了模拟概率重写中的不确定性，我们不能像ARS中那样使用元素之间的简单关系我们必须将元素与元素的分布相此外，为了将这样的元素建模为（Q，Q），我们需要能够将元素与几个这样的分布相关联。这就引出了下面的定义。定义2.1概率抽象重写系统（PARS）是一个对（A，），其中A是一个集合和类型关系（AD1（A））（称为"逐点演化关系"）。应该清楚的是，通过采用"狄拉克"分布（即归一化的、单点分布），每个ARS也是PARS。我们可以通过扩展列表›→提供PARS的一个简单示例，这是ARS的常见做法。示例2.2让PARS成为由a›→[（2/3，b），（1/3，c）]a ›→[（2/5，a），（3/5，d）]b ›→[（1/2，c），（1/2，d）]c ›→[（1，d）]这里，a是唯一的非确定性元素。我们称之为终结元素，因为它没有后继分布。更重要的例子见第6节。PARS中的执行是非确定性和概率性选择的混合。第一类，对应于运算符，当机器为当前元素选择一个后继分布时发生。第二类，对应于D1运算符，是在所选后继分布的元素之间的随机选择。为了模拟这样的执行，我们使用计算树的概念。定义2.3给定PARS（A，），我们通过以下规则归纳地定义其（finite）"计算树"的集合，根为a（noted（a））。有时候，我们也会考虑无限的计算树，因为我们把共归纳定义的集合放在首位。Aε T（a）a>>[（p1，a1），...， （p n，a n）] t i她家（ai）[a;（p1，t1）;...... ;（p n，t n）]\A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115119TP示例2.2中PARS的树的图形表示被赋予了右边。（a）中的树表示系统在a上启动后的一种可能的（不确定的）演化。关于树没有进一步的假设：特别地，如果一个元素在给定的树中被扩展了很多次，则每次都可以使用不同的后继分配。换句话说，我们不假设一个A2/31/3bc1/21/2cd d收集树的叶子，连同它们的累积概率，给出了一个正态化的列表分布的上升。定义2.4树T的"支持"是一个（a）=[（1，a）]supp（[a;（p1，t1）;. . . 。 ;（pn，tn）]）=p1supp（t1）++. . 。+pnsupp（tn）当一棵树的所有叶子都是末端元素时，我们称之为树极大值（因为它没有适当的超树）。我们现在可以声明我们的权益属性。定义2.5（UTD）A PARSA具有"唯一终端分布"，当对于每个a和T1，T2她家她家都有supp（T1）≈ supp（T2）时。我们以前说过，直接提供一个（ARS）通常是困难的。由于PARS包含ARS，因此直接证明UTD存在相同的困难。因此，我们寻求一种能够产生影响的属性，提供一种复合的、更可追溯的证明方法。3重写发行版和Confluence。为了达成一致的意见，我们将首先定义一个比计算树（定义2.3）更自由的重新编写分发（定义3.4定义3.1给定PARSA=（A，›→），我们定义关系→P（of typeP（D（A） ×D（A）））（称为A→A→D →P→D（p，a） ：ds→PPA+dsDS→PDS*（p，a） ：ds→P（p，a） ：ds*[]→P[]请注意，在不使用第一规则的情况下，这只是分配上的同一性关系。我们注意到这个关系的子集，其中第一个规则必须在一个步骤中至少使用一次，如→1，并称之为适当的进化。→P关系可以模拟这个系统中的计算树，因为它可以用来重写它们在引理3.3意义上的支持。定义3.2当，如果D1 → E1，D2 → E2，那么α D1 + β D2 → α E1 + β E2，对于所有α，β ≥ R +，我们称之为关系→ "组成的"。引理3.3如果T她家（a），那么[（1，a）]→*Psupp（T）120A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115A›→证明。首先，请注意P是复合的。然后，使用合成性对TQ我们现在定义了一个分布上的ARS，结合了并行进化和等价步骤。因此，我们对PARS的影响的定义仅仅是这种关系的通常影响。定义3.4给定PARSA=（A，›→），我们定义关联的ARSDet（ A）（称为A的"确定性"）通过关系式→ =（→ P ≥）覆盖集合D（A）。定义3.5（分布混杂）当Det（A）在古典意义上是混杂的时，我们说PARS A是"分布混杂的"（或简称为"混杂的"）。Det（A）中的减少比树木的扩张更自由，因为它降低了"部分"进化的风险。当然，如果是D，那么[（1，a）]→[（1/2，a），（1/2，a）]→1/2D++[（1/2，a）]。 Ne vertheless，引理3.7sh或ws，其影响意味着UTD。引理3.6如果D1是终末的，D1→D2，那么D1≈ D2，D2是终末的。Pr或of。从→P的定义可以清楚地看出，如果D1i是终止于 dD1→PD* 的，那么D1=D*（即，完全相等）。结果然后遵循wsb和归纳的步骤数，和传递性和反射性的†。Q引理3.7 If A |= CR，然后是A |= UTD。证明 。取 T1，T2 她家T（a）极大。我们从引理3.3 中得到了supp （ T2）←*[（1，a）] →*supp（T1）。 因此，必须存在这样的C，即Supp（T2）→C**→Supp（T1）。由于T1、T2是最大的，它们的支持是终末的。然后，从引理3.6，我们得到了supp（T2）†C†supp（T1），正如所需要的。Q此外，在UTD之外，具有分布影响意味着发散的竞争（没有终端分布）也可以被加入。因此，只要存在两个不同的终端元素，影响就给出了一个精确的方法来证明由→诱导的均衡理论的一致性。引理3.8如果D1，D2a re终端分布和Aisc在流中，则D1→D2if且仅if D1≈D2。证明。回去的路是微不足道的，所以我们详细说明了前进的路。从合并（重复）开始，D1和D2必须具有公共还原。这个结果来自引理3.6。Q那么，如果a和b是不同的终端元件，则遵循→-可转换性它是一个一致的理论，如[（1，a）][（1，b）]。 总结，在一个有影响力的PARS，re-关于程序等价性的讨论很简单，而且有一个关于可转换性的强有力的一致性保证，就像经典的情况一样。熟悉重写模等价性[14，20]的读者可能会想，为什么我们不研究具有影响力的模†，或者更强的Church-Rosser属性模†。它把这两个都变成了对我们的目的来说太强大了。以下是一个系统：a>>[（1/2，a），（1/2，b）]A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115121A∪毫无疑问，由于它是确定性的，所以应该被认为是流动的;但是在它里面，我们可以形成下面的图：[（1/2，a），（1/2，b）]←P[（1，a）]†[（1/3，a），（2/3，a）]其中ch不能tb e关闭dby→*P·†· ←*P，因为一方存在3倍的压力，而另一方没有。因此，该系统既不具有通量模，也不具有CR模。然而，它是一个明确的分布与流动。因此，我们研究了具有影响力的严格弱分布，这对于我们的目的来说是足够强的，并且更容易推理。4测试具有影响力的4.1介绍性在上一节中，我们介绍了我们对影响力的定义，并对其正确性进行了论证。为了使它在实践中有用，它也应该是可以证明的。在本节中，我们为这项任务提供了几个简单的标准，得到了证明古典影响力的最常见方法由于具有影响力的分布仅仅是→的经典影响力，所以所有现有的经典标准（例如钻石性质或纽曼引理）都是有效的，没有任何修改。然而，它们并不是很有用。一个问题是，人们需要考虑所有的分布（而不是单个元素）和峰中等价步骤的存在。此外，Det（）从来没有强（甚至弱）正规化，所以纽曼引理在这里是无用的。关于金刚石性质，考虑一个具有a›→D的系统，那么以下约化是可能的：[(1[（1/2，a），（1/2，a）]→1/2D++[（1/2，a）]这两个发行版通常不能在一个步骤中连接在一起，即使是没有其他后继者分布。因此，先验地说，如果分布的影响甚至比古典的影响更难被证明，那么它似乎是如此。为了强调这一点，我们将证明关于→关系的各种综合引理，允许我们将其分解为更可管理的形式。然后，我们展示了我们如何将我们的推理限制在狄拉克分布上，忽略峰中的等价步骤，并允许在谷中自由使用它们。最后，我们忽略了经典标准，因为它影响了我们的设置，如钻石属性和纽曼的引理的预兆4.2解构关系......因为bothes→Pand≈arereflexi ve，（→Pο） *与（→P/ο） * 重 合 。 因此，既然confluence是关系的反射传递闭包上的一个属性，那么研究→P/≈的confluence是很困难的，其中等价步骤没 有 " 成 本 " ， 但 它 是 普 遍 的 （ 如 重 写 模等 价 ） 。122A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115SRSαβγ····E·PE·······←→←→··· ·给定这两种关系的精确综合定义，我们可以通过分析还原来证明→P/≈的任何一步都可以通过首先分裂，然后进化，然后连接回元素来完成，正如引理4.3所述。我们首先介绍了以下关于减刑的概念。[10] 2定义4.1（顺序交换）我们说一个关系R。"commutes over" S when S R R S，并将其记为R S。那个。。属性可以用右边的图来表示。 直观地说，它R这意味着R可以在S之前被"推"。。序列交换的一个关键性质是if R {\displaystyle\if R}S，然后（R）S）*=R*S*。当采用n倍组合（即我们现在提供一些与演变和对等步骤有关的变化（最后一个步骤需要一些引理4.2我们有→PE（FJ）*;SE（FJ）*和→P·SS ·→P·（FJ）*。证明。 通过归纳的形式的还原。Q引理4.3关系式（→P/≈）和S*·→P·（FJ）*重合。证明。向后包含是微不足道的，所以我们只详细说明向前的方向。通过使用引理4.2中的第二个交换，我们得到≈ = S*·（FJ）*。因此，我们需要证明S*（FJ）*→PS*（FJ）*S*→P（FJ）*。然后，通过使用另外两个交换来重新排序关系，从而进行证明。Q此外，这种等价性扩展到n-折叠组合，从而扩展到反射传递闭包。引理4.4关系式（→P/≈）n和S*·→n·（FJ）*重合。证明。 通过对n的归纳，并使用前面的引理和交换。Q4.3简化的图表。通过前面的分解，我们现在可以给出一个非常通用的结果，即用一个特定的根D来简化图，然后很容易地推广到整个系统。定义4.5我们说一对关系（γ，δ）（α，β）bγdδ c。 该属性的图表可以在右侧查看。bc当所有a都 出 现 这 种 情 况 时 ， 我们简单地 说"（γ，δ）close（α，β）"。注当（→ *，→ *）关闭（→ *，→ *）时，这是准确的。D定义4.6我们称一个关系→"局部"，当如果α D1 + β D2 → E，那么存在E1，E2，使得E = α E1 + β E2，Di →EI。(NoteP和S是本地的）。[2]请注意，这不是交换关系的通常概念，定义为S−1R RS−1，它是一个对称性质，可以描述为δA. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115123›··········定理4.7设α，β为局部关系，γ，δ为组成关系。 如果D的狄拉克分布有（γ/ο，δ/ο）闭（α，β），则D有（γ/ο，δ/ο）闭（S*·α·（FJ）*，S*·β·（FJ）*）。证明。我们给出了证据的草图，更多细节可以在[17]中找到。我们需要关闭（S*α（FJ）*，S*β（FJ）*）。首先，注意关闭（S*α，S*β*）是足够的，因为我们可以用（FS）*步骤反转（FJ）*步骤。现在，既然α和β是局部的，S*α和S*β也是。因此，我们可以限制自己封闭D的狄拉克分布，并结合约化，因为γ，δ是复合的。 我们当从某个[（1，a）]开始时，现在需要关闭（S*α，S*β）。请注意，左（右）分支是形式p1D1+... +p n D n（q1E1+... +qm Em），其中a通过α（β）还原为每个Di（Ej）。我们可以应用我们的假设来得到一个Ci，j，逼近每个Di，Ej。 通过首先适当地拆分每个分支，我们可以关闭它们。"在p1q1C1，1+... +p1q m C1，m+... + p n q m C n，m。Q从这个理论中，我们得到了几个简单的冲突标准作为推论，这些标准可以应用于特定分布的水平，也可以应用于整个系统。标准4.8（狄拉克反流）如果对于D和分布E，F中的每个元素a，E→P[（1，a）]→PF中的r是C，E→C →F，则D是反流的。Pr或of。一个推论y或f定理m4. 7，取α =β=γ=δ=→P。Q标准4.9（半一致性）如果对于D和分布E ，F中的 每 个 元 素 a ， 使得a›→E和[（1，a）]→PF中的re是C，使得E→C→F，则D对 于 →P/≈是半一致的。Pr或of。一个推论y或f定理m4. 7，取α =→P和β=γ=δ=→P。Q标准4.10（钻石属性）如果对于D的每个元素a和分布E，F如此E→a›→F，则有一个C如此E→P/†C→P/†F，则D具有→P/†的钻石属性。证明。 定理4.7的推论，取α=β=γ=δ=→P。Q请注意，在所有这些标准中，我们不需要在高峰期考虑任何等价性，并且可以在山谷中自由使用它们，无论是在进化之前还是之后。此外，对于每个元素，满足这些标准中的任何一个都会产生系统的影响。证明影响力的另一个常用工具是将关系切换到另一个具有相等反射传递闭包的关系（因此是等价的影响力），但这可能更容易分析。对于分布影响，允许使用类似的开关，但由Lemma 4.12稍微简化。定义4.11在相同的集合A上给出›→1和›→2，如果对于每个a›→1D，我们有[（1，a）]→2D，我们说›→1被›→2模拟。引理4.12如果›→ 1被›→ 2模拟，则→1→2。如果两个关系相互模拟，则→1=→2，并且它们的影响是等价的。124A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115PPPPPPPP证明。第一部分是对还原论的案例分析→1.第二部分是微不足道的。Q4.4纽曼纽曼引理为了得到纽曼引理的类比定义4.13一个无限序列D i，使得D1→D2→D3→· ··被称为"无限→ -链"（从根D1）。定义4.14（SN）当没有无限→根D的1链时，我们称分布D为"强归一化"。当每个分布都强正态化时，我们称PARS强正态化。有一些不言而喻的系统可以满足这一要求，而且这是人们直观地期望的。现在可以获得纽曼引理的概率类比，遵循与定义4.15（LC）我们说分布D是"局部不稳定的"，其中和←1D→1F意味着存在C，因此E→*C→* F。请注意，狄拉克分布上的强归一化意味着它适用于所有分布，并且类似地适用于局部影响。引理4.16（纽曼）如果A|= LC和A|= SN，然后是A|= CR。证明。 我们将证明，通过在→1上建立良好的感应，每个分布都是一致的。对于一个给定的分配，它的努力表明，任何一个适当的进化的高峰可以通过→ * 关闭的选项。然后，根据推论4.8（并且因为→*P=→1*），具有foll或ws的影响。 W e wa nt关闭形状为E→1*D→1*F的图。 如果树枝的另一个DP1P1E*LCF*P1 *P1 *和IHC F如果零步很长，那么我们就可以轻松地得出结论。如果不是，我们可以在右边形成图，完成局部影响的证明和E*和F* 的归纳h和p。Q5极限分布[编辑]C *C **在经典抽象重写中，一个元素可以是非规范化的、弱规范化的或强规范化的（分别对应于它不会、可能和将规范化的情况）。 在概率重写中，故事并没有那么简单。考虑以下PARS，其中b是终端元素：a>>[（1/2，a），（1/2，b）]3请注意，无穷大（→1/≈）-链总是存在的，因为部分进化。IHA. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115125→ΣΣc）c）这是正常化吗？一个人可以说然而，这样的概率将通过采取足够的步骤而任意地变小，并且分布[（1，b）]达到极限。在这种情况下，a被称为几乎肯定终止[1]。当然，一个理想的事实是，大多数确定终止的元素具有唯一的最终分布。我们将证明，具有影响力的分布保证了这种独特性。我们首先引入了一个距离的概念 数学上的 分配，也就是说，A型[0，1]的归一化函数。我们放弃列表分发的原因是为了允许无限支持的有限分发，这是一个很好的解决方案。我们注意到从列表分布D（具有最大值）中获得的数学分布D预期的定义）。我们还将数学分布上的定义扩展到通过applying- whereappropriate列出分布。定义5.1给定D，E数学分布，我们将它们之间的距离定义为d（D，E）=a她家|D（a）−E（a）|。定义5.2（序列的极限）给出数学分布D0，D1，...的无穷大序列。我们说L是序列f的极限，如果对于每个ε> 0，存在N > 0，因此对于所有i≥N，d（Di，L）<ε。请注意，此距离是L1距离，极限的定义是公制空间的通常定义。然后很好地知道，给定序列的限制是唯一的。我们感兴趣的是由终端元素组成的极限，表示值的分布。为此，下面的定义是有用的。[10]定义5.3对于数学分布D，我们将其"活力"定义为非末端元素的权重之和。也就是说，Liv（D）=a该书（A）请注意，列表分布的生存率不能随着进化而增加，并且Liv（D）= 0i D是终结的。此外，由于分布的规范化部分不能进化，因此liveness在进化所涉及的可能距离上提供了一个向上的边界，如下面的引理所述。引理5.4如果D → *E，则d（D，E）≤2 ·Liv（D）。Pr 或 of 。根 据 引 理 4.4 ， 存在D* 和 E *， 其 ch 使 得 D′D*→P′E ′ 。 因 为 等 式valences，所以它很难sh或w的结果为D*和E*。在不损失一般ty的情况下，假设D*=Dl+Dt，其中D l的所有元素nt都不是终结的，而D t的所有元素n t都是终结的。由于并行进化是局部的，所以终端元素不能e vol ve，w e h av e使得E*=E**+Dt对于某些E**。然后，d（D*，E*）issimpl和d（Dl，E**）。注意Li v（D*）是Dl和E** 的w eig h t。 由于距离b小于b且总距离weig ht，因此其最大值为2·Liv（D*）=2·Li v（D）。Q现在，我们可以将终端分布的唯一性的概念扩展到终端元素的极限分布，考虑到无限多个约简序列。定义5.5（ULD）A PARS A具有"唯一极限分布"，其中对于每个D，它是两个不定→链的根，链Ei和Fj分别具有极限E∞和F ∞终端分布，则E ∞ = F ∞。126A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115-⊕引理5.6If A|= CR，然后是A|= ULD。证明。取ε >0。通过极限的定义，我们知道有i，j，因此d（EI，E∞）ε/6和d（Fj，F∞）ε/6。<<因为E∞和F∞是终末的，所以Liv（Ei）和Liv（Fj）必须小于ε/6。分布Ei和Fj可以通过有限数量的→步骤到达，因此存在这样的分布C ，即Ei→*C→*Fj。从引理5.4，我们得到d（EI，C）ε/3等>DMN>>DNR-AppRR-λR λ!N→DM→DM→DMN→ MDλx.M> λx.Dλ! X.M> λ! x.D图1。λ1的完整语义当应用于thunk时。这有效地暗示了被禁止的抽象遵循一个固定的策略（从道德上讲，这是按值调用的，直到论证被简化为一个thunk，然后按名称调用）。5为了证明λ1的金刚石性质，我们首先需要两个替换引理。当D=[（pi，ai）]i时，我们将D[M/x]写入分布[（pi，ai[M/x]）]i。同样，M[D/x]表示[（pi，M[ai/x]）]i。6.1如果M ›→ D，则M[N/x] ›→D[N/x]。证明。 通过M→D上的归纳。Q引理6.2如果M ›→ D，并且x在N中是线性的，则N [M/x] ›→ N [D/x]。证明。 通过对N的良好形式性的归纳。Q引理6.1和6.2类似于[23，引理3.1]的两个陈述。有了这两个，我们就可以证明下面的定理，它意味着钻石的性质。定理6.3如果D→M›→E则re存在C，C*因此D→PC和E→PC*，其中C ≈C*。证明。 通过归纳M ›→ D和M ›→ E的形状。Q根据这个定理和推论4.10，我们得出结论，λ1是一致的，并且它同时包含UTD和ULD。6.2量子λ-演算：Q*Q*calculus[8]是一种量子编程语言，它模拟了测量，一种固有的概率运算。图之间的还原发生率，其中的项与量子态耦合，并且其中的项我们将不会进一步详细说明。它的语义学并不固定一种策略，并且像λ1一样，也是基于[23]。128A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115[5]我们之所以采用"表面还原"，只是因为"内部还原" [ 23]受到了影响A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115129αNKNαNNK测量值RKNN测量值RNmeasq测量值RKKαβQ*中的量子变量是线性的（而不是线性的），因此它们不能被复制或忽视，因为量子物理学的非克隆[25]和非擦除[19]性质还原步骤与描述还原的标签配对（例如，在一个示例中）。量子比特被测量的地方）。作者提供了一个名为强影响的属性，该属性断言具有公共根的任何两个最大（可能无限）计算树都具有相等的归一化支持（即，两个支持分布的归一化部分是相等的），此外，任何范式形式都出现在两个树上相等数量的叶子中。正如他们所注意到的，这个性质是非常强的，而不是被经典的λ-演算所陶醉。考虑项（λx.λy.y）Ω。它有一个无限的计算树，没有任何范式（因为术语在按值调用中还原为自身），也有一个有限的树，有一个单一的λ和叶，当然没有等价的规范化支持。请注意，Q *良好形式判断将此术语视为非线性的。为了证明强影响力，提供了一个被称为准一步影响力的关键引理，它在道德上是一个钻石属性，但根据所采取的还原，行为略有不同。 在measr形式的两组、和和度量之间区分约化。 我们将不描述这些集合或Q * 的语义（其完整描述见[ 8]），我们将公正地陈述引理符号C→pD意味着和C→p D意味着C→pD对于某些α她家N（idem K）。引理6.4（Q*[7，命题4]的准一步一致性）设C，D，E为配置，C→pD，C→sE，则：• 如果α她家和β她家都是K，则要么D=E，要么F，D → 1F，E → 1F。• 如果αε K和β ε N，则另一个D →1KE或There isFs.t. D→1KF和E→1F。• 如果α她家K和β=measr，则有F，D→sF和E→1F。• 如果αε N和βε N，则要么D=E，要么F，D→1F，E→1F。• 如果αε N和β=measr，则存在F，D →sF和E→1 F.• 如果α=measr和β=measq（其中r/=q），则有t，uι[0，1]和anF因此，pt=su，D →tF，E →uF。从这个引理，事实上，有没有无限的序列，和一个对于具有一致性的分发，可以获得简单的证明。在将Q *建模为PARS（粗略地使用每个标签的后继者分布）之后，我们可以很容易地重新解释引理6.4，以证明它的钻石属性（根据推论4.10）。从这个结果，分布与影响随之而来，因此也是唯一的终端和极限分布。 值得注意的是，这一事实既不需要标准化的要求，也不需要概率条引理。我们获得的具有影响力的分布是相似的，但既不弱也不强于具有影响力的分布。它并不像发行版那样弱，因为它保证了130A. Diaz-Caro，G.Martinez/理论计算机科学电子笔记338（2018）115没有任何正态形式的计算发散可以连接起来，而强流则不能。它也不强，因为它不意味着任何不是终端的极限分布，而它遵循强一致性，它们必须在它们的归一化部分中匹配。67结论我们已经研究了这样一个问题，即表明概率操作语义不是由策略的选择所决定的。为了这个目的，我们通过定义分布上的经典关系来定义对概率系统的影响，从而定义了概率系统的影响。我们证明了我们的分布影响的性质是适当的，特别是，它意味着终端分布的唯一性，无论是有限的和无限的减少，并给出了一个等一致性的保证。我们相信，这一发展表明，具有影响力的分布提供了一个合理的"甜蜜点"，以证明概率语义的正确性，因为它提供了预期的执行保证，同时允许可追溯的具体地说，所提供的λ1和Q* 的证明与人们对线性计算的期望一致。关于Q * 的证明也部分地回答了[8，第8节]中的猜想（"任何重写系统都像命题4 [我们的引理6.4 ]那样享受属性，享受与这里使用的意义相同的影响"）答案是部分的，因为具有影