基于图的决策过程和和积定理的局部图重写系统

理论计算机科学电子笔记176（2007）139-163www.elsevier.com/locate/entcs和积定理中判定等式的局部图重写系统Jos'eBacelarAlmeida1、JorgeSousaPinto2和MiguelVilaPillaca3DepartamentoodeInform'atica/CCTCUniversidadedo Minho葡萄牙布拉加，摘要在本文中，我们给出了一个基于图的决策过程的微积分与和和产品类型。虽然我们的动机来自Bird-Meertens方法来对函数程序进行代数推理，但这里使用的语言可以被视为具有二进制乘积和余积的类别的内部语言。因此，所提出的决策程序具有独立的利益。基于项重写的标准方法将工作模一组方程，目前的工作提出了一个更简单的方法，基于图重写。我们依次展示了该系统如何涵盖反射方程法，融合法和取消法。保留字：基于图的决策过程，无点编程1产品介绍无点编程风格[3]被认为是对函数式程序进行推理的一个很好的选择，因为它避免了对变量的引用相反，程序是由纯一阶语言在一组基本的组合子上构造的，其语义由一组方程给出通过构造相应的方程理论中的导子，建立了两个规划的等式这应该与逐点方法相比较，在逐点方法中，程序是适当的λ演算的项。由β-归约导出的相等概念不足以建立两个程序行为相等（即，当应用于相等的参数时产生相同的结果），这促使将外延性包含到归约关系中。1电子邮件：jba@di.uminho.pt2电子邮件：jsp@di.uminho.pt3电子邮件：jmvilaca@di.uminho.pt1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.031140J.B. Almeida等人/理论计算机科学电子笔记176（2007）139无点语言和外延λ演算之间的对应关系在范畴逻辑[10]中是众所周知的。事实上，两者都可以被看作是范畴结构的普适性质的不同公理化：在前者中，公理是根据态射给出的，而在后者中，公理是根据元素给出的（Plotkin [11]恰当地称这些公理化为本文考虑一个只含二元积和余积的片段由于缺乏指数，这个片段具有非常小的计算能力。尽管如此，决定等式的问题已经表现出有趣的微妙之处，因为乘积和余积之间的相互作用迫使某些等式必须传统地通过模等价关系来处理[12，6]。我们提出了一个决定程序的平等，使用本地图重写系统。我们的方法是基于无点的理论介绍-图基本上是数据流表示的条款，与组合对应的边缘连接在一起的两个结果表明，这种观点有效地克服了需要考虑的外部等效。相关工作。这项工作的确切主题已经在[12]中讨论过了，其中作者描述了具有有限乘积和上乘积的范畴的演绎系统它与这里考虑的理论精确地对应本文分两步建立了态射相等性的检验过程：（i）研究了一个标准重写系统，证明了它是模适当的方程理论E的强正规化和合流系统;（ii）给出了判定E下态射相等性的一个算法。与此相关的还有Ghani [6]关于带求和的可拓代数演算的工作（早先[5，4]已经考虑过求和，并使用限制版本的可拓性公理）。再一次，可判定性建立在两个步骤：一个强正规化约简关系和检查（准）范式的“交换”转换的过程。最近，Altenkirch和他的同事[1]使用了一种通过评估的方法来解决同样的问题。虽然后一种方法不依赖于重写，但它与这里提出的工作共享一个事实，即范式不对应于术语，因为它们是在一个独特的语义域中计算的我们的工作也与λ-演算[2，8]的最佳实现的工作有相似之处，特别是使用允许应用非交互规则的安全操作符（即， 涉及不是主要的端口的规则）。然而，我们注意到，引入指数的原因是完全无关的两个工程。论文的结构本文的结构安排如下：第二节介绍和积理论。第3节定义了和积网，第4节给出了这些网的术语翻译;第5节非正式地介绍了我们的图重写的原则J.B. Almeida等人/理论计算机科学电子笔记176（2007）139141→×⟨··⟩系统本文的主要结果出现在第6节，在那里系统被正式定义，并研究其性质我们在第7节结束。2语言与理论考虑以下类型和类型的长时间TPF类型：：= A|型号×型号|类型+类型术语：：= C A，A|id类型|期限·期限|期限，期限|π1型，类型|π2型，类型|[期限，期限] |i1类型，类型|i2类型，类型其中A在一组基本类型和CA，A是一组常数函数（我们假设这个索引族中的集合是成对分离的对于每一项，我们关联一个域和一个余域类型B断言项f具有域A和余域B。与该语言相关的键入规则如下cA，B∈CA，BcA，B：A→B idA：A→Af：A→Bg：B→Cg·f：A→Cf：A→Cg：B→C[f，g]：（A+B）→Cπ1A，B：（A×B）→A π2A，B：（A×B）→Bf：A→Bg：A→Cf，g在下文中，当提到一个术语时，我们假设它是良型的。我们将省略类型上标，这可以从上下文中推断出来。类型构造函数和+通过它们的通用属性来表征，这些属性又可以通过下面的方程组来捕获：组合物id·f=f·id=f（f·g）·h=f·（g·h）反射定律π1，π2[i1， i2] =id融合法则f，gf·[g，h]=[f·g，f·h]取消法律π1·f，g=f[f，g]·i1 =fπ2·πf，gπ=g[f，g]·i2 =g等式理论的这种表述在代数编程领域是标准的[3]。在λ-演算的观点中，抵消律是β-等式，而反射律和融合律一起等价于η-等式。例如，对于乘积，η-等式可以写成f=π1f，π2f，也称为满射配对。在这些方程所定义的理论下判定是否平等，需要产生一个判定程序。实现这一点的标准方法是定向方程以获得汇合的、终止的重写系统（通过142J.B. Almeida等人/理论计算机科学电子笔记176（2007）139·完成过程）。这种方法在这个系统中是失败的，其原因将在第5节解释我们提出的解决方案时予以暗示。很明显，η规则的因式分解是有用的，因为它允许独立地处理由反射和融合引起的问题，这是不同的性质。3和积网和积网将从符号的字母表中构建;每个符号都有一个相关的arity和co-arity。我们在对偶对中引入这些符号，其中arity和co-arity交换：• 具有元数2和协元数1的makepair符号，描述为（，）;其二元选择描述为？• 两对投影符号，具有arity 1和co-arity 1，表示为π1和π2;它们的顶点是表示为i1和i2的选择注入;• 具有arity 1和co-arity 0的擦除器符号，描绘为ε;双协同擦除器是描绘。• 对于每个自然数n，描绘了具有元数和协元数1的取消符号，Qn;其对偶共抵消被描绘为□n。• 对于每对自然数（n1，n2），有一个元数为1，余元数为2的复制子符号，记作<$（n1，n2）;它的对偶是余复制子，记作<$（n1，n2）;节点是三元组（s，I，O），其中s是具有元as和共元cs的符号，I是输入端口的集合，并且O是输出端口的集合，使得I（resp.O）是s（resp. cs）。一个网是一个元组（S，E，I，O），其中• S是一个节点集，设IS=S（s，I，O）∈SI和OS=S（s，I，O）∈SO;• I_n，O_n是网络的输入点和输出点的集合• E：OSI→ISO是一个项目。 Pai rs（o，i）∈E是该网的所有边.一个网是良类型的，如果存在一个标签的输入和输出端口的每一个节点的类型，这样每一个边缘连接同样标记的端口，图1所示的约束对每个节点都成立（大写字母表示类型变量）。位置是一对非负整数（a，b），表示为a b。一个网是良构的，如果每个节点的输入和输出端口都有一个位置标记，使得每条边连接相同标记的端口，并且图1中所示的约束也适用于每个节点（S n表示n的后继）。良构性在网上强加了一个结构不变量。定义3.1和积网是一个非循环的、良好类型的、良好形式的网，只有一个输入和输出。和积网中的指数将用于控制第6节中介绍的约简系统中节点的重复和相互湮灭。非索引J.B. Almeida等人/理论计算机科学电子笔记176（2007）139143A B（，）A×Bπ2B·T⟨⟩··？π1 π2 12（，）·（，）··（，）（，）·（，）π1·（，）a· Sba·Sba·ba·ba·ba· ba·Sb一n一a· ba·ba·ba·Sba·Sba·ba· ba·ba·bSa·bSa· ba·bSa·bSa·ba· ba· ba· ba· bSa·bFig. 1. 键入和定位约束图二. 网的例子或者零索引节点-- 0表示（共）图2包含了一些不是和积网的例子：第一个网不是良型的;第二个网不是良型的;第三个网有一个圈。4Term网在本节中，我们给出了从PF到和积网的类型定向转换T（）。这种转换已经解决了反射定律所固有的一个汇合问题：对于乘法子系统，从左到右的方向似乎是合理的，但反射定律产生了不可解的临界对。为了说明这一点，考虑以下满射配对f=id·f=ππ1，π2π π·f=ππ1·f，π2·fπ等式链的两个极端相对于所获得的重写系统都是正规形式，因此它不是完整的问题在于，由定向反射定律所产生的规则从项中丢失了结构信息，而项对于系统的汇合是必不可少的下一节中定义的图重写系统始终保留A×Bπ1一一（k，n）A A一一一1A+BA+B？A BB2A+B一一（n，k）一一n一144J.B. Almeida等人/理论计算机科学电子笔记176（2007）139∧∧∨∨结构信息，它必须明确地存在于初始表示中。反射完全从重写系统中删除，并成为定义结构化类型标识 作为一个例子，类型（A×B）×C的恒等式将被表示为π1，π2。π1，π2π。下面给出的翻译根据这个讨论扩展了身份因此，只有原子类型的身份才被表示为边缘。像满射配对这样的方程则通过构造来满足。在下文中，当一个网被用来构造一个更大的网时，我们假设初始网中的输入和输出被移除，并且在新网中引入一对新的输入/输出端口和对应的边所有引入的节点都接地。身份• T（idA→A），其中A是一个基类型，被定义为由连接输入到输出的一条边组成的和积网• T（idA×B→A×B）是通过引入4个新节点得到的和积网I，π1，π2，和（，），以及连接第一个（分别为π 1，π 2，和（，））的新边第二）输出到π 1的输入（分别为π2），π 1的输出（分别为π 1和π2），π2）到I A（resp. I B），以及I A的输出（分别为 B.第一次（第一次）第二）输入（，），其中IA= T（idA→A）和IB= T（idB→B）;以及I是的输入，I的输出是（，）的输出。• T（idA+B→A+B）是通过引入4个新节点得到的和积网I？，i1，i2，和，以及连接第一个（分别为第二，输出？至I A的输入端（相应地， I B），I A的输出（相应地， I B）到i 1（resp. i 2）和i 1的输出（分别（2）第一次（？第二）输入，其中I A=T（idA→A）和I B=T（idB→B）;以及最后将I的输入设置为？而I的输出是I的输出。组合物• T（u. t A→C）是通过连接从T的输出到U的输入的边而获得的和积网V，其中T = T（t A→B）且U = T（u B→C）。自然，T的输入变成V的输入，U的输出变成V的输出。常数函数• T（π1A×B→A）是通过引入一个新节点π1和一条新边将其输出连接到IA的输入而得到的网P 1，其中I A= T（idA→A），并将P 1的输入设为π1的输入，将P1的输出设为IA的输出。• T（π2A×B→B）是通过引入一个新节点π2和一条新边将其输出连接到I B的输入而得到的网P 2，其中I B= T（idB→B），并将P 2的输入设为π 2的输入，将P 2的输出设为I B的输出。• T（i1A→A+B）是通过引入新节点 i1和连接IA的输出到i1的输入的新边而获得的网I1，其中IA =T（idA→A），并且将I1的输入设置为IA的输入，并且将I1的输出设置为I A的输出。J.B. Almeida等人/理论计算机科学电子笔记176（2007）139145∧∧∧∨∨∨×⟨⟩·（A×B）×（C×D）π1A×Bπ2C×D π1π2π1π2A B CD（，）（，）A×BC×D（，）（A×B）×（A+B）×CA+B？A B12A+Bπ1输出i1。• T（i 2B→A+B）是通过引入新节点i 2和连接IB的输出与i2的输入的新边而获得的网I2，其中I B= T（idB→B），并且将I 2的输入设置为I B的输入，将I 2的输出设置为i 2的输出。分裂设G是通过引入两个新的和（，）节点和4条新的边而得到的和积网，其中T=T（tE→A），U=T（uE→B），的输入成为G的输入，（，）的输出成为G的输出.然后又道：• T（t，uE→A×B），其中E=C+D，是通过构造网I = T（idC+D→C+D）得到的和积网G j，以及将其输出连接到G的输入的边，将G j的输入设为I的输入，G j的输出设为G的输出。• T（nt，u∈E→A × B），其中E不是C + D形式，则T（n t，u ∈ E → A × B）就是G。要么设G是通过引入两个新的？和节点，和4个新的边缘连接的输出？T和U的输入，T和U的输出到的输入，其中T=T（tA→E）和U=T（uB→E）;那么的输入？成为G的输入，的输出成为G的输出。我们拥有：• T（[t，u]A+B→E），其中E = C D，是通过构造网I = T（idC×D→C×D）得到的和积网G j，以及连接G的输出和I的输入的边; G j的输入是G的输入，G j的输出是I的输出。• T（[t，u]A+B→E），其中E不是C×D的形式，是G。定义4.1由平移T（）构造的和积网类称为项网。项网T（id（A × B）×（C × D）→（A × B）×（C × D））和T（π1（A + B）× C→A + B）如下所示作为示例。146J.B. Almeida等人/理论计算机科学电子笔记176（2007）139F G（，）F G （，）（，）f f g g（，）（，）f g f g（，）（，）FG h（，）fFgH（，）图三. 融合作为网络复制见图4。 结构化网络很容易看出，网络T（tA→B）的输入类型为A，输出类型为B。两个不同类型的、句法上相同的术语可以被翻译为不同的术语网。由网表示的项的主类型总是可以唯一确定的。5利用局部图重写判定等式在本节中，我们将非正式地介绍图重写系统及其定义中涉及的困难然后，在下一节中正式定义该系统，并研究其属性在这里，我们依次考虑融合和消除的处理融合融合是由（共同）复制器节点完成的直观地说，与网络交互的复制器应该执行该网络的复制（参见图3）。然而，这种“复制”应该在本地执行，即（共同）复制器仅与单个节点交互。此外，两种融合（加法和乘法）可以同时发生，因此必须注意避免过程中的干扰。为了清楚起见，我们首先只考虑我们语言的乘法片段当一个复制器遇到一个结构化的网络（必然是两个项的分裂一旦每个子网的复制结束，仍然需要重新组织网络顶部的复制器，以获得复制的正确结果J.B. Almeida等人/理论计算机科学电子笔记176（2007）139147FdupM-fnnf=π1，π2，π1，π2FF（，）锡锡双M对 n（，）（，）0nSNdupM-dupMSN00   （，）（，）（，）111111（，）（，）2222222211 （，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（见图4）。为了控制复制器的这种重组，复制器符号中的索引的存在是合理的-我们将遵循以下规则来管理与复制者的互动。第一条规则相当明显-与单输入/单输出节点的当一个复制器与一个pair构造器节点交互时，它不仅复制节点，而且还将自己一分为二，以便复制每个子网。最后一条规则是复印机之间的交换规则，它允许原始复印机的两个分开的副本重新连接，同时复制顶部的复印机。注意复制器的拆分和复制之间的区别索引记录了请注意，换向规则限制顶部复印机接地。我们展示一个复制过程的例子：现在我们来讨论和与积之间的相互作用以上对融合的当和积类型同时存在时，在术语层面上提出的一个问题与组合的结合性有关：不再存在由融合的从左到右方向所暗示的组合的优先方向在图的层次上，这个问题被避免了，因为图免费捕获组合的结合性，并且不需要重写。第二个问题与乘积与和以对称的方式相互作用的事实有关，以至于不可能选择某种形式而损害其对偶。作为说明最后一个观察结果的例子，考虑以下相同项的等式推导：id，idid，id148J.B. Almeida等人/理论计算机科学电子笔记176（2007）139⟨ ⟩ ⟨ ⟩ ⟨⟩⟨ ⟩·⟨ ⟩·⟨ ⟩ ⟨ ⟩ ⟨⟩dupM选择n？nn？？克dupM-dupSnnn 克什托克事实上，这是一个更一般的等式的例子，称为交换定律：[f，g]，[h，k] = [f，h，g，k]。我们的图重写系统将把这些项分配给一个唯一的范式，而不是对一个使这些项相等的适当的等式理论进行模运算（如[12]）其本质在于让复制器和协同复制器在不相互干扰的情况下执行它们的遍历。回到id，id[id，id]这个术语，让我们把重点放在共同复制器和复制器的交互上。从结构上讲，当一个复制者和一个共同复制者相遇时，它们应该相互穿过，这是相当明显的问题是在这个过程中，节点是应该被复制还是被拆分（对它们的索引的影响是不同的）。第一个解决办法是说明只发生重复这对应于保持两个索引不变，并导致一个规则，允许复制者自由地通过选择节点（没有索引调节）。将需要以下我们的示例项id，id[id，id]简化为唯一的范式，它不对应于任何项的翻译。我们将这些称为完全范式，因为它们捕获了这些网可以作为不同项读回的事实？（，）？？？？？（，）（，）（，）（，）可以很容易地验证[id，id]、[id，id]（分别为[id，id，id，id]）也具有相同的范式。减少是由一个额外的身份网引发的，该身份网由顶部的翻译功能引入（分别为：网的底部不幸的是，使用上述规则，指数不再适当地约束可能发生的交换要看到这一点，请考虑以下归约序列：J.B. Almeida等人/理论计算机科学电子笔记176（2007）139149dupM选择n？SNSN？？克dupM-dupSnSNSN 斯克林斯克？？？？？（，）（，）11     （，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）注意，规则dupM-choice的应用移除了关闭在左手侧子网上开始的融合所需的地面复制器。事实上，这正是dupM-dupM规则通过限制顶部复制器接地来避免的发散模式这表明指数也应该限制规则dupM-选择的应用。第二种方法是让两个节点都被拆分（即，两个节点的索引都递增）。以下是相应的规则：在这里，问题变得更加微妙。 考虑以下简化序列：？？（，）（，）（，）（，）？？？11111111（，）（，）（，）（，）（，）（，）请注意，顶部的协同复制器遍历网络时，会提升较低子网中所有复制器的索引这一特性与上面给出的非正式描述不一致，但可以卓有成效地加以利用事实上，如果我们继续减少过程，我们得到：150J.B. Almeida等人/理论计算机科学电子笔记176（2007）139？？？？？？？？？你说呢？你说呢？111111111111？？？？（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）（，）？ （，）（，）（，）（，）π2π1（，）图五. 不对称网络这个例子表明，为了达到完全的正常形式，促进足够的融合就足够了问题是，额外的减少强烈依赖于网络的对称性。更准确地说，它们依赖于选择节点两侧的复制器数量和复制器树的形状然而，即使术语网确实表现出高度的对称性，也不能保证在所有约简策略下的所有网络都具有所需的对称性。图5精确地示出了不对称网的示例请读者使用[id，id]对其进行融合，以检查这种方法的问题。最后一种方法是使用前面的解决方案的混合版本：非正式地，我们将其中一个节点作为这个节点被拆分（其索引增加），另一个节点被简单复制（其索引保持不变）。这里的问题是如何定义支配关系，因为最明显的解决方案无法定义合流系统。我们的解决方案由以下特征给出：一个节点优于一个节点J.B. Almeida等人/理论计算机科学电子笔记176（2007）139151∧∧？？（？？？（，）（，）？（（，）？（1，0）（1，0）（1，（1， （，）（，）（，）（，）？？（，）（，）（，）（，）（，）双M对（k，Sn）（k，Sn） （k，n）（，）（，）其中：X =（k，n），ifi>k X =（Sk，n），ifi ≤k Y =（i，j），ifn>j Y=（i，Sj），ifn ≤j见图6。 融合规则见图7。 图中的规则融合示例。6当“他们之间的关系能够在系统中表达这一点实际上是将整数对作为索引的关键原因，因为需要区分加法和乘法分量图6实现了这个解决方案（一组双重规则用于联合复制器），图7说明了它的应用。注意，我们只允许节点与？与执行融合的协同复制器相关联的节点（即使这？只有在与其他人交换后才可用减刑涉及？在融合过程中复制的节点被抑制。？dupM选择（k，n）(Sk得双曲正切值.(Sk得双曲正切值.？？F（k，n）dupM-f（k，n） f=π1，π2，π1，π2FF（0，0）（k，n） （k，Sn）（k，Sn） （0，0）（0，0） （i，j）dupM-dupS（k，n）X X YY152J.B. Almeida等人/理论计算机科学电子笔记176（2007）139FcancelM-fnf=π1，π2，π1，π2nFSNSN（，）取消M对n（，）（0，0）ncancelM-dupMSNSN（0，0）KncancelM-cancelnKFG（，）π1F见图8。 取消删除>J见图9。 取消规则取消取消的性质与擦除有关考虑图8中给出的取消规则的结构。底部节点的交互应该触发网络g和顶部复制器的移除我们遵循标准方法引入一个特殊的擦除节点ε（及其对偶），node. 主要的困难是删除顶部节点，它充当擦除过程的中间节点。为此，我们使用一个□（和双Q）节点，其功能是遍历网络f，并在g被擦除后立即删除顶部复制器必须再次确保这一进程不干扰其他取消和合并。关于指数，□节点在网络中向上移动时表现得像复制者索引是单个整数，因为它们不受加法构造的影响。在遍历过程中，□节点对复制子的索引执行校正。这是因为共同复制者可能已经越过顶部复制者并更新了其索引。图9显示了取消规则的代表性子集。在（，）cancelM-100π1（0，0）ε-dupM-2JJ（n，k） cancelM-dupS-1J X其中：X =（n，k-1），如果kX =（n，k），如果k≤jJ？取消选择JJ？抹除器J.B. Almeida等人/理论计算机科学电子笔记176（2007）139153∧ ∨∧∨2？（，）π1简单地说，取消是由对构造函数和投影节点之间的交互触发的（规则cancelM-1），之后ε节点将丢弃与取消的子项对应的那部分网然后，□节点将遍历保留的子项，并与顶部复制器上的ε节点同步下面所示的示例简化说明了抵消定律的使用6和积净重写基于上一节非正式讨论的思想，现在我们将给出和积网的局部图重写系统我们首先需要建立一个适当的图重写规则的概念：规则的左手边（LHS）和右手边（RHS）都是有限网，具有相同的输入和输出端口集（换句话说，规则保留了网的接口此外，LHS和RHS网都是良好类型和良好形式的，该规则保留了输入和输出的类型和位置标记，并且不引入循环。在一个类型化的网中应用一个规则，用它的RHS替换任何与它的LHS匹配的子网;上面的条件保证不会有任何边悬空。下面介绍的系统还具有以下优点：• 系统中不存在具有相同LHS的两个规则，或者使得一个规则的LHS是另一个规则的LHS的子网• 每个规则的RHS不包含另一规则的LHS作为子网• 规则集是对偶完备的：每个规则的对偶也在系统中这具有交互网络系统的一些定义属性[9];这种系统的进一步要求是每个节点都应该有一个独特的主要端口，并且每个规则的LHS应该由两个节点组成，其中一个边连接两个主要端口。这个要求将足以保证强的局部融合，这不是我们系统的属性。定义6.1和积重写系统由附录B给出的规则定义。一个容许网是一个项网的任何约简。很容易看出，系统是强归一化的（一般来说，□节点上升;Q节点下降;三个节点或者以防止非终止的方式对节点进行索引调节在什么接下来，我们将隐含地调用二元性，它允许相当大的经济000（0，0）（0，0）（1，0）（1，0）000000 （0，1）（0，1）（0（00154J.B. Almeida等人/理论计算机科学电子笔记176（2007）139∨NNNNN12（1，0）(Sk，Sn）（Sk，Sn） (Sk得双曲正切值.（1，0）（1，0） 在重写系统的研究过程当我们将注意力限制在容许网上时，系统具有受控性，这将在后面证明本文的主要结果时进行探讨现在让我们陈述其中的一个结果，以供将来参考（见附录A的证明）。引理6.2在容许网中，指标可以通过归约来重置。汇合很容易看出，上面给出的重写系统对于和积网不是一般然而，它是融合的容许网。像往常一样，系统的汇流将通过研究由规则引起的所有临界对来建立大多数都是以纯粹的地方方式解决的然而，对于某些对，这将是不够的，因为约简路径的收敛依赖于可容许网的全局性质为了在临界对的分析中重新获得局部性，我们现在将引入一个适当的等价概念定义6.3设是一个单输入，n-输出网络，A是一个双输入，单输出节点。我们将JOIN（A，）定义为由A的两个副本和A的n个副本组成的两个输入，n-输出网络（比如Ai），其中网络的输入是A的每个副本的输入，第一个副本的第i个输出（分别是A i的第i个输出）。第二个）拷贝连接到第一个（相应地，第二个是Ai的输入，第i个是Ai的输出。定义6.4 设N1和N2是两个单输入、n输出的网。称它们与结点A等价， 其 中N1≠AN2，对每个含有JOIN（A，N1）的网N，N与由N中的JOIN（A，N2）取代JOIN（A，N1）所得到的网有公共约简.引理6.5下面的网是关于具有某个索引（i，j）的节点的孪生等价网。是的。让我们用N （a，b）和N（a，b）来表示下面的网格：（a、b）（a+k，b+n）（a+k，b+Sn）（a+k，b+Sn）（a、b）（a、b）这些参数化网络中的每一个都可以被视为一个（索引）节点，通过计算网络和每个符号（节点）之间的相互作用的派生规则J.B. Almeida等人/理论计算机科学电子笔记176（2007）139155（0，j）（0，0）（k，Sn）（k，Sn） 112≡1∨2212（1，0）（1，0）  （0，Sj）（0，（k，Sn）（k，Sn）(Sk得双曲正切值.(Sk得双曲正切值.（1，0）（1，0） （1，（1，0）（0， （0，SJ）（0，SJ）（0，（1，0）（1，0）(Sk，(Sk，Sn） (Sk，(Sk，Sn）（0， （0，SJ）（0，SJ）（0，（0，j）（k，n）（0，0）（0，0） (Sk得双曲正切值.(Sk得双曲正切值. （0，J）（0，（0，0）（0，0） (Sk得双曲正切值.(Sk得双曲正切值.（1，（1，0） （1，（1，0）（0， （0，SJ）（0，SJ）（0，其中J=j，如果n > j;SJ，否则。见图10。 示例关键对对于每一个系统，对于N （a，b）和N（a，b），所述推导规则完全相同。现在考虑一个包含JOIN（A，N（a，b））的网N。 根据引理6.2，N （a，b）中的上 乘 子 具有将其指数重置为（0，0）的红约束方程。最后，在h处的观测值可以在N（a，b）中被简化为等式，从而产生N（0，0），并且N（0，0）通过规则dupM-dupM简化为N（0，0）。 影响N都是一样的Q这个证明说明了在汇流证明中孪生等价的主要目的：它允许克服对交换规则的应用的限制，这些规则偶然地被引入系统中以精确地实现汇流，因为它们避免了交换之间的关键对。命题6.6重写系统对于容许网是合流的。证据 考虑到附录B中给出的规则产生的所有关键对。让我们用由规则dupM-dupM和dupM-dupS形成的关键对来说明这一点，这是一个有趣的情况。我们首先假设第一个（加法）指数的分量我们得到了图10中所示的一对约简序列，其中表示网的结构相等，并且d=表示事实上，这两个网有一个共同的约简，如引理6.5所示。当具有正的加性索引时，不修改顶部复制器的索引，并且可以通过应用规则dupM-dupM来代替孪生等价的调用。Q156J.B. Almeida等人/理论计算机科学电子笔记176（2007）139⟨⟩可靠性和完备性附录B中给出的约简系统导出了下列项网等价的定义设n表示网的结构相等性。定义6.7两个项网G1，G2是等价的，记为G1=G2，如果存在和积网GJ1，GJ2使得G1−→ <$GJ1和G2−→<$GJ2，并且GJ1<$GJ2。我们现在可以建立有关方程理论和图形系统的主要结果建议6. 8（声音）Lett，ubeTPFterms。然后t=u=T（t）=T（u）由于项网的约简不一定产生另一项网，在下面的完备性结果中，T（t）和T（u）的公共约简可以是不是项网的和积网。建议6. 9（完全项）Lett，ubTPF项。然后T（t）=T（u）=t=u这两个结果的证明可参见附录A。7结论和今后的工作翻译T（·）和图重写系统一起解决了三个问题：• 翻译直接抓住了反射定律，因为它根据它们的类型扩展了身份。• 为了确保有效地捕获融合律，必须允许涉及3个节点的配置之间的交换（规则dupM-dupM、dupM-choice、dupS-dupS和pair-dupS），由索引方案调节。• 最后，这个索引方案必须能够处理a，b等方面的融合。[c，d]，这可能发生在两个方向上。在我们的系统中，这样的融合产生了一个（唯一的）网，它不再是一个术语网。在我们的平移阶段和在外延的微积分中使用展开式之间，有可能画出一个平行线当我们将其与[4]中的扩展模拟帐户进行比较时，可以清楚地看到这一点，在[ 4 ]中，类似的预处理阶段执行所有需要的扩展。 我们的翻译相当简单，因为我们不需要模拟翻译项的扩展。下一个明显的步骤是充分处理微积分的指数部分这引入了新的问题，与λ-演算到相互作用网的编码工作有关初始和终端对象及其相关的态射可以很容易地纳入我们的系统。J.B. Almeida等人/理论计算机科学电子笔记176（2007）139157∧−→参考文献[1] Thorsten Altenkirch、Peter Dybjer、Martin Hofmann和PhilScott，标准化类型化的lambda演算与余积。第16届IEEE Symposium on Logic计算机科学，第303-310页。IEEE Press，2001.[2] Alberti，A.，Giovannetti，C.，和Naletto，A.（1996年）。 博洛尼亚最优高阶机器Journal of Functional Programming，6（6）：763[3] 伯德河de Moor，O.：《程序设计的代数》，Prentice Hall，1997。[4] 罗伯托·迪·科斯莫和迪莉娅·凯斯纳。模拟没有膨胀的膨胀。计算机科学中的数学结构，4（3）：1-48，1994[5] D. Doughert y，Someλ-calculi with categorical sums and products.重写技术和应用，计算机科学讲义第690卷，第137Springer Verlag，1993年。[6] Neil Ghani，Beta-Eta Equality for Cofproducts，InProceedings of TLCASpringer-Verlag，1995.[7] J. - Y. Girard：Towards a Geometry of Interaction，InCategories in Computer Science and Logic：Proc. of the Joint Summer Research Conference，pages 69一九八九年[8] Gonthier，G.，Abadi，M.，Lvy，J。J. （1992年a）。 最优lambda缩减的几何学 在ACM Symposium Principles of Programming Languages，第15[9] Y. 拉丰互动网 在第17届ACM程序设计语言原理研讨会（POPL'90）上，第95-108页。ACM Press，Jan. 1990年[10] 约阿希姆·拉姆贝克和菲尔·斯科特。高阶范畴逻辑导论，剑桥高等数学研究剑桥大学出版社，1986年。[11] G. D. 普洛特金高级领域理论的研究生课堂讲稿（包括部爱丁堡大学计算机科学系。可查阅http://www.dcs.ed.ac.uk/home/gdp/publications/，1981年。[12] J. R. B. Cockett和R. A. G.有限和积逻辑.在理论和应用的范畴，卷。8，2001，No.5，pp 63-99.AProofs引理6.2的证明规则dupM-dupM和dupM-choice被称为交换规则，因为它们促进了节点的交换如果一个网包含一个子网，该子网与一个交换规则的LHS的顶部和底部节点之一相匹配，则该网被称为允许引理A.1设G是容许半对易的容许网.则存在一个网GJ使得G ∈Gj，并将Gj中的部分匹配推广到交换规则的LHS的完全匹配.证据在一个可接受的网络中，对于每一个？或具有索引（0，0）的节点，指定与其交换的代理（如果有的话）可以通过遵循网络定义的递归过程来识别，从代理的一个输出开始。无接地复制器的换向规则的缺失保证了该节点在换向实际发生之前不会改变此外，规则dupM-pair和dupM-dupS在交互代理的两个输入中注入复制器的事实保证了在给定节点的任何输出端口上计算时的结果是相同的Q现在我们可以证明引理6.2：158J.B. Almeida等人/理论计算机科学电子笔记176（2007）139不NNN不−→不−→∧证据在还原过程中，根据良好的形式调整指数。另一方面，索引节点的规则是这样的，当索引为非零时，它们不约束交互。 这意味着一个索引节点只有在以下情况下才能以正常形式生存：（i）它到达网络的顶部;或者（ii）它陷入不可能的交换中。格式良好性标准保证：(i) 是不可能的容许网，引理A.1表明，（ii）可能永远不会发生在一个正常的形式。Q健全性引理A.2L设t为TPF项，G设（t）为通过连续引入a将索引为（a，m）（其中m > 0）的节点映射到项netT（t）的输出。则G（t）<$G（t），其中G（t）由索引为（a，m）的节点组成，其输出连接到两个网G l，G r的输入，使得G l= G r= T（t）。证据通过对t.注意，引理对于m = 0是无效的，在特定情况下，t是[f，g]的形式（或以[f，g]结尾的项的组合），在这种情况下，复制器节点不支配m。Q引理A.3设t是PF项，G ε（t）是通过将ε节点连接到项netT（t）的输出而获得的网。 则G ε（t）<$G ε，其中G