等价性的特征

21理论计算机科学电子笔记70第6期（2002）URL：http://www.elsevier.nl/locate/entcs/volume 70. html41页s约化的四个等价等价Vincent van Oostrom1荷兰乌得勒支大学哲学系Roel de Vrijer2自由大学理论计算机科学系荷兰阿姆斯特丹摘要项重写系统中的两个共初始约简被称为等价的，如果它们执行相同的步骤，尽管可能以不同的顺序。我们提出了四个特点，这样一个概念的等价，置换，标准化，标签和投影的基础上，分别。我们证明了，所有的特征产生相同的概念的等价性，一类一阶左线性项重写系统。我们开发的一个关键技术是由一个预先准备好的系统提供的。1介绍我们考虑减少到正交步骤的顺序进行。本文的核心包括以下四个表征随之而来的概念的等价约简。两项之间的两个缩减是(i) 置换等价，如果它们可以通过正交步骤的重复置换而相互变换（第3节），(ii) 平行标准化等效，如果将步骤分类为由外向内顺序，则产生相同的平行标准化约简（第4节），(iii) 如果其目标与其来源的任何标签相同，则标签等同（第5节），1电子邮件：Vincent.vanOostrom@phil.uu. nl2电子邮件：rdv@cs.vu.nl2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。范奥斯特罗姆和德弗里耶尔22(iv) 投影等价，如果任何一个归约在另一个归约上的投影导致空归约（第6节）。事实上，这些等价性最自然地是在证明项上定义的，我们将这样做。证明项将Meseguer重写逻辑[36]中的证明表示为项。因此，它们可以直接表示顺序计算（约简）以及并行计算（参见例如，实施例2.12）。正如第7节所指出的，所有四个特征都是等价的，这使得人们可以将一个特征的结果转移到其他特征上。这是有用的，因为每一个表征强调一个特定的观点对等价性（排列，排序，标签，投影），并带有自己的应用领域和结果。等价的不同概念以前已经研究过，但主要是在正交重写的上下文据我们所知，这是第一次在左线性项重写系统的背景下系统地研究这些概念，可能有关键对。本文可以看作是[47]第8章的一部分概述，在那里可以找到所有真正的证明。本文提供的证明实际上只是证明草图。我们将努力激发和说明我们的特点。为此，我们使用以下运行示例。3例1.1设U为具有三个规则a→bf（x，b）→g（x）g（b）→c并考虑从f（a，a）到项c的以下两个约简。f（a，a）→f（b，a）→f（b，b）→g（b）→cf（a，a）→f（a，b）→g（a）→g（b）→c直觉上，这些减少执行相同的步骤，但以不同的顺序。事实上，我们将为他们展示每一个特征的等价物。注1.2所有这些等价概念的共同特征也可以通过事件结构以无语法的方式被捕获（[49]）。然而，请注意，这仅适用于线性的情况，即非擦除和非复制事件。特别是，将项重写步骤建模为事件的明显想法失败了，因为项重写步骤可能是擦除（组合逻辑中的K-步骤）或复制（S-步骤）。事实上，这正是复制，即。擦除和复制，术语重写步骤的行为使得本文中的结果不平凡。如何概括事件结构以充分处理擦除和复制是一个活跃的研究领域。例如，在[20]中，提出了无冲突重写系统的事件样式语义，包括一阶正交项重写3为了便于说明，我们选择了一个非常好的TRS作为运行示例;它在[41]的意义上是线性正交的，因此它是一致归一化的。范奥斯特罗姆和德弗里耶尔23系统和λβ演算，等等。由于目前还不清楚是否，如果是这样，如何，这可以推广到重写系统的冲突，因为我们感兴趣的非正交系统，以及，我们不处理事件结构在本文中。在Per ers（[34，33，31，32，35]）的一个系列中，Melli`es以一种无语法的方式提出了一种可重写理论，他的训练伙伴是λσ-演算。他的公理适用于我们所考虑的系统。因此，这里提出的几个结果和方法，特别是那些平行标准化，有一个语法自由的类似物在他的理论。确认我们非常感谢以下人员在撰写第8章时的支持：Eduardo Bonelli，SanderBruggink ， Khaab Khaenashvili ， JannWillemKlop ， Paul-Andr′eMelli′es ，AartMiddeldorp，PaulaSeveri，YdeVenema，Ren′eVestergaard，AlbertVisser和Fer-JandeVries。我们感谢与RTA'02相关的WRS和HOR研讨会的组织者给我们机会展示我们的第一作者要感谢筑波大学、筑波的ETL和阿姆斯特丹的CWI提供的款待和资金。2证明条款如上所述，我们感兴趣的减少到他们的步骤的顺序显然，只有在步骤上存在同一性的概念时，步骤才能合理地重新排序为此，将重写关系与术语重写系统相关联是不够的，因为存在所谓的语法意外（[24]）。例2.1考虑具有单一规则f（x）→x的TRST。从f（f（a））开始有两个步骤，通过在它们的redex模式的头部符号下划线来表示：f（f（a））→f（a）f（f（a））→f（a）注意，这些步骤会导致语法上的意外：这两个步骤都会在T的底层重写关系→T中产生步骤f（f（a））→Tf（a）。为了克服这个困难，我们将把一个抽象重写系统（见注释2.5，我们使用抽象重写系统的概念）与一个术语重写系统联系起来。这个想法是有一个明确的证人的方式，其中一项减少到另一项，对于一个给定的长期重写系统。这样的证人将被称为证据条款。范奥斯特罗姆和德弗里耶尔24→⟨ ⟩→→⇒→2.1抽象重写系统抽象重写系统，简称ARS，是一个四元组A，Φ，src，tgt，其中A是一组对象，Φ是一组步骤，src，tgt：Φ A分别是源函数和目标函数（见图1）。我们将使用各种箭头状符号，~，，... 要在ARS上测距，使用a，b，c，. 在对象上的范围，并且φ，λ，χ，. 在台阶上移动。对于一个给定的抽象重写系统→，我们写φ：a→b（在文本中），或aφb（在公式中），甚至a φ b来表明φ是一个源a和目标b的步骤;φ是一个证明，证明从a到b的某个步骤存在.对象termsrclhs步骤规则tgtrhs对象term图1.一、抽象重写系统（上）和规则重写系统（下）例2.3（i）黑洞或环ARS有一个单一的物体，从物体到自身只有一步(ii) 对于每个自然数n，ARS →n有对象·1，...，·n和步骤i+1：·i→n·i+1，对于每个i，使得1 ≤i且i+1 ≤n。(iii) ARS−∞→是→n对所有自然数n的并集。也就是说，−∞→就是无限的直线·1 → 1 · 2 → 2 · 3 → 3 ·· ·。(iv) 句法偶然事件ARS_n由两个宾语和两个宾语之间的同向步骤组成。具有相同源的步骤将被称为共同初始，具有相同目标的步骤将被称为共同初始。一个步阶可与一个步阶组合，如果步阶的源与步阶的目标相同。循环是源和目标重合的步骤。在正交项重写系统中，多步骤（见下文）通常显示的最强属性是菱形和三角形属性。定义2.4（i）→具有钻石性质，如果对于任何共同初始步骤φ1，φ2，存在共同最终步骤φ1，φ2，使得φi与φi可合成。(ii)具有三角形属性，如果对于任何对象a，存在一个对象a的阶数，使得对于从a开始的任何阶数φ，都有一个阶数可以与它组合成a。请注意，如果ARS具有三角形属性，则它具有菱形属性。此外，如果它也有所有循环，则a→a对每个对象a都成立（见图2）。范奥斯特罗姆和德弗里耶尔25a ab c bda图二、菱形属性和（对于具有所有循环的ARS）三角形属性注释2.5定义2.2与许多关于抽象重写的论文一致与抽象重写系统连接使用的术语在整个文献中变化，这取决于预期的应用领域。例如，我们的抽象重写系统在[38]中被称为索引1-复形，在[44]中被称为约简复形，在[25]中被称为图对象被称为点、顶点、状态或世界。步骤被称为（1-）单元格、转换、移动、事件、边缘或箭头。源和目标被称为域和共域，开始和终点，或初始和最终。我们警告读者，在文献中，ARS可以表示这里使用的ARS（通常由上述论文的作者以及[47]的第8章和第9章），或者重写关系（通常在[22]和[47]的其他章节中出于这个原因，我们避免为我们的ARS使用（重写）关系术语，这与[38]一致：出现的概念与偏序集理论密切相关因此，除了在同一性的情况下，避免使用该理论的术语。2.2术语重写系统定义2.6术语重写系统，简称TRS，T是一个结构体，R是一个签名，R是一个ARS，它的（变量和）项作为对象。R的步骤称为规则，规则的源和目标分别称为其左侧（lhs）和右侧（rhs）（参见图1）。我们雇佣了Q，Q，Q，... 在规则上游走我们要求规则Q：l→r：(i) l不是变量，(ii) r中的变量在l中的变量中此外，我们还需要左线性，即变量在l中最多出现一次。例2.7我们的运行示例TRSU的签名是{a，b，c，f，g}，范奥斯特罗姆和德弗里耶尔26T→分别为0、0、0、2和1我们将其命名为左线性规则：Q：a→bf（x，b）→g（x）n：g（b）→c对于一个给定的TRS，它的证明项是在项的签名上的项，扩展了表示等式逻辑的各种推理规则的符号。TRS的规则作为所谓的规则符号附在签名上。定义2.8设= 拉斯特河 是一个术语重写系统。 对于R中的每一个规则Q，都有一个规则符号，也用Q表示，它的左边有自由变量的数量作为arity。证明项签名是R的规则符号集和{·}的（不相交）并集，其中·是二进制组合符号。底层抽象重写系统≥TofT，简称，定义如下。– 这些对象都是上的项。– 这些步骤被称为证明项或证明，是证明项签名上的项的归纳我们采用φ，φ，χ，. 在证明条件上进行选择步骤≥与它们的源和目标一起由以下推理系统定义φ1：s1≥ t1。。 φn：sn≥ tn（规则）Q（φ1， .. 。 ，φn） ：l（s1， . 。 ，Sn）≥r（t1， . 。，tn）φ1：s1≥ t1。。 φn：sn≥ tn（替换）f（φ1，.，φn）：f（s1，.，Sn）≥f（t1，.，tn）φ：s≥t φ：t≥u（传递性）（φ·φ）：s≥u在（规则）-规则Q是规则符号，使得其对应的规则Q：l r在R中包含n个变量。在（替换）-规则中，f是一个n元函数符号.注意证明项ARS≥的对象是闭项（与TRS规则的lhs和rhs有关此限制的理由，请参阅备注2.15。在（规则）-规则中，我们采用了以下的符号约定。记法2.9在Q：l→r是规则的情况下，l（s1，.，sn）和r（s1，.，sn）表示通过分别将si代入l和r中以代替Q的第i个变量而获得的项。在这里，我们假设变量以某种任意但固定的方式排序取决于Q。反过来，我们也将使用Qσ来表示证明项Q（xσ，. ，xσ），如果σ是Q中变量的替换。1N范奥斯特罗姆和德弗里耶尔27→不使用证明术语，语法事故消失了。4例2.10设Q：f（x）x是例2.1中语法意外TRS规则的命名版本。则Q（f（a））和f（Q（a））都证明f（f（a））≥f（a）。在前一种情况下，得出这一结论的依据是：（替换）a：a≥a（替换）f（a）：f（a）≥f（a）（规则）Q（f（a））：f（f（a））≥f（a）在后一种情况下，（替换）a：a≥a（规则）Q（a）：f（a）≥a（替换）f（Q（a））：f（f（a））≥f（a）通常与TRS相关的ARS是通过以适当的方式限制限制证明条件而产生的（参见图3）。−◦→−“→→\图三. 多步、并行步、步进和循环定义2.11不使用（传递性）规则构造的证明项，即如果没有出现·，则称为：(i) 一个多步（以及≥对多步的限制是）由− →表示。(ii) 一个并行步骤，用−“→表示，如果规则符号没有嵌套出现(iii) 一个（一个）步骤，用→表示，如果恰好有一个规则符号出现在其中。(iv) 一个循环，如果其中没有规则符号，则用\多步骤是同时执行任意数量的正交普通步骤的步骤平行步骤是一种特殊的多步骤，其中涉及的redex模式发生在平行位置，它们是不相交的。多步和平行步是有趣的，因为粗略地说，它们是正交TRS的步骤的最小扩展，分别满足菱形和三角形性质。步骤本身通常[4]甚至更强：只有现在我们才能表达TRS具有句法偶然性意味着什么：例2.3的句法偶然性ARS必须嵌入到它的一步ARS →T中（见定义2.11）。范奥斯特罗姆和德弗里耶尔28→≥≥→→→−→−→−→{→}≥→→由于项重写规则的可能的非右线性，不满足这些属性中的任何一个。Example2. 12（i）考虑rthTRS{Q：a→b， f：f（x）→g（x，x）}. 共同初始步骤f（Q）：f（a） f（b）和f（a）：f（a）g（a，a）不能通过任何一对常规步骤变成钻石然而，将它们看作是平行的步骤，它们可以通过f（b）：f（b）“g（b，b）和g（Q，Q）：g（a，a）“g（b，b）;“的方式制成钻石。尽管如此，平行步骤不具有三角形属性，因为例如，不能从f（a）在一个并行步骤中达到公共约简g（b，b然而，它可以通过一个多步骤来实现：f（a）−f（a）→g（b，b）;−f（a）→具有三角形性质。(ii)考虑TRS 问：我有一a. 步骤aa通过一步Q：a a，通过对Q应用（规则）（注意Q是空的），以及通过循环a：a\a，通过应用（替换）来证明。从第二个例子中可以清楚地看到，在定义2.11中被定义为循环步骤的东西这个例子还表明ARS在这个意义上也可能有其他的循环，例如那些由循环规则（例子中的Q例1.1中的约简也可以看作是特殊的证明项定义2.13证明项是约简，表示为 如果它是一个循环或使用（传递性）从步骤构造，模约简恒等式，即，第10页表1中的前三个身份例2.14再次考虑例1.1中的f（a，a）→f（b，a）→f（b，b）→g（b）→cf（a，a）→f（a，b）→g（a）→g（b）→c它们可以通过使用示例2.7的证明项签名的约简来证明f（Q，a）·f（b，Q）·n（b）·n：f（a，a）→cf（a，Q）·f（a）·g（Q）·g：f（a，a）→c下面，我们将把这两个证明项分别表示为R和S注2.15（i）术语重写系统的规则通常只是术语对。因此，人们通常对规则的同一性是模糊的。例如，规则f（x）g（x）和f（y）g（y）形式上是不同的项对，但它们仍然经常被识别，因为它们是彼此的变体这个问题在目前的情况下很容易克服，只要在规则上定义一个适当的商。(ii) 请注意，我们并没有为整个等式逻辑使用证明项。值得注意的是，我们不采用以下证明术语，范奥斯特罗姆和德弗里耶尔29≥·····反对称性和对称性的推理规则：\s：s≥s（反应性）φ：s≥t（对称性）φ−1：t≥s从概念上讲，最好有一个针对自反性的推理规则，而且它确实存在于重写逻辑中。然而，对于我们目前的目的，研究置换等价，它是技术上多余的。（替换）-规则只适用于函数符号，而不适用于变量，所以s：ss只对sclosed有效，这似乎是有问题的 然而，变量就置换等价而言可以看作常数.由于这里我们对置换等价感兴趣，我们可以简单地假设约简/证明项是封闭的。在重写逻辑中，对称性的推理规则是不存在的，因为我们只对约简的置换等价感兴趣，而不是转换。(iii) 通过将它们为术语并操纵这些术语来使归约或更一般地说，证明显式化是一个自然的想法，因为它是显式表示概念以证明其属性的一般想法的实例例如，这个一般思想是通过显式替换演算来研究替换的基础我们的证明项表示重写逻辑中的证明（[36]），即没有对称性的等式逻辑这一活跃研究领域的概述见[28]。文献[13]中给出了具有β-归约和η-展开的简单类型λ-演算（在其De Bruijn表示中）的重写证明理论的一个实例研究相关的概念和相关的证明项的概念出现在文献中的许多地方，参见例如[46，7，10，17]。(iv) 注意，多步骤可以通过一个接一个地应用其中的规则来发展成约简例如，例2.12中的f（Q）可以分别展开为f（a）g（a，Q）g（Q，b）、f（a）g（Q，a）g（b，Q）和f（Q）f（b）。事实上，多步的所有发展都是有限的，并且具有相同的目标，这被称为有限发展定理。3置换等价我们引入了等价的第一个概念，置换等价。两个约简是置换等价的，如果它们执行相同的步骤，但可能以不同的顺序。这类似于说列表[2，1，0]和[0，1，2]具有相同的成员，以不同的顺序列出。在这些列表的情况下，这可以通过重复排列相邻成员对来显示：[2，1，0]=[2，0，1]=[0，2，1]=[0，1，2]类似地，两个约化可以说是置换等价的，如果一个可以通过一系列相邻步骤的置换从另一个得到实际上，排列将根据证明项而不是根据归约来定义这个想法是，这允许一个人将一个单一的排列细化为两个序列，范奥斯特罗姆和德弗里耶尔302\·φφ·\φ（φ·）·χφ·（·χ）f（φ1，. ，φn）·f（φ1，. ，n）φ f（φ1·φ1，. ，φn·φn）Q（φ1， .. 。 ，φn）n（φ1， . 。，φn）·Q（t1， . 。，tn）Q（φ1， .. 。 ，φn）φQ（s1， . 。，rialisation步骤这类似于说列表[1， 2]和[2， 1]是置换等价的，因为[2，1]=[1]=[1，2]其中左列表和右列表是序列化中间列表的两种不同方式，其中中间列表的两个成员都是“并发的为了表达它们的并发性，我们可以将1和2写在彼此旁边，而不是对于列表来说，这只是一个符号问题，但在证明术语中，确实有两种不同的方式可以使步骤并行：水平和垂直。置换等价的定义是相应组成的。例3.1我们运行的例子的证明项R=f（Q，a）·f（b，Q）·f（b）·f（a，Q）和S=f（a，Q）·f（a）·g（Q）·f（a，Q），证明了约简f（a，a）→f（b，a）→f（b，b）→g（b）→cf（a，a）→f（a，b）→g（a）→g（b）→c可以被证明是置换等价如下：R=f（Q，a）·f（b，Q）·f（b）·fn=f（Q·b，a·Q）·n（b）·nn=f（Q，Q）·n（b）·n=f（a·Q，Q·b）·n=f（a，Q）·f（Q，b）·n（b）·nn=f（a，Q）·n（Q）·nn=f（a，Q）·n（a）·g（Q）·n=S其中我们已经使用了下面表1的所有置换恒等式表1置换恒等式范奥斯特罗姆和德弗里耶尔31·±·定义3.2（i）表1中的前三个恒等式是身份(ii) 约化恒等式与第四个函子恒等式结合形成结构恒等式。实际上，函子恒等式是一个模式：它被假定为每个函数符号f。(iii) 结构恒等式与第五个内恒等式和第六个外恒等式（图式）结合，对于每个规则符号Q：l→r，其中φi：si≥ti，对于所有1≤i≤n，形成置换恒等式。在 证 明 项 上 生 成 的 结 构 等 价 和 置 换 等 价 将 被 表 示 为 dby 和 = ，respectively。 如 果 存 在 满 足 φ ·χ = χ 的 条 件 ， 则 由 φ ± χ 定 义pemutationati or ±。不等于等于零的增量=等于零的增量顺序，sinceφ|n=φ。函数式集 成 捕 获 并发的数 据 流，内部和外部身份捕获垂直并发。例3.3（i）考虑一个TRS，它有一个规则Q：a→b和一个二元函数符号g。证明项g（Q，a）·g（b，Q）和g（a，Q）·g（Q，b）都证明g（a，a）≥g（b，b）。任何一个证明项都执行两个a-步骤，但前者先执行左a-步骤，后者先执行右a-步骤。它们在结构上是等价的，因为a-赎回彼此平行，所以可以同时进行g（Q，a）·g（b，Q）<$g（Q·b，a·Q）g（Q，Q）g（a·Q，Q·b）g（a，Q）·g（Q，b）观察到中间证明项g（Q，Q）是一个并行步骤，证明了Q的两个并行出现的同时应用（对应于上面讨论中的1 2）。(ii) 考虑具有规则Q：a→b和规则f：f（x）→g（x，x）的TRS。证明项f（Q）·f（b）和f（a）·g（Q，Q）都证明f（a）≥g（b，b），并收缩源中存在的g-和a-赎回。前者收缩内部，后者首先收缩外部。因此直观地它们执行相同的步骤。它们的置换等价性可以从图4中直观地读出，也可以从f（Q）·f（b）f=f（Q）f=f（a）g（Q，Q）中直观地读出。并不是说中间过程（Q）是一个多-见证同时应用嵌套出现的Q和q。第二个例子表明，置换嵌套步骤（垂直置换）是复杂的，因为它会导致非线性现象，如果最外层的规则是非右线性的（在例子中：重复）。（请注意，我们上面的运行示例展示了水平和垂直排列。这是范奥斯特罗姆和德弗里耶尔32f（a）f（Q）（a）f（b）=（Q=g（a，a）（b）g（Q，Q）g（b，b）图四、f（Q）·f（b）与f（a）·g（Q，Q）的置换等价性是什么让置换等价变得复杂尽管如此，下面的结果是容易的，因为它们直接从等式逻辑的属性中得出。Theorem3. 4（i）Permutationeequivalen ce=isacongruen ce.(ii) 置换序±是一个拟序。(iii) 如果φ=φ，则src（φ）=src（φ）且tgt（φ）=tgt（φ），并且对于约简（即，对约简标识取模）。注3.5置换等价是一个相对较新的起源。它是在[24]中为λ-演算这一概念的一些重要的进一步由于置换等价与并发性之间的紧密联系，置换等价在并发性重要的领域以多种形式出现例如，在迹论中，Mazurkiewicz迹的概念作为独立动作顺序的迹在[29]中引入。另一个例子，在事务处理系统（TPS：[12]）中，并发控制协议必须通过确保所谓的可串行性来防止干扰：TPS应该只接受一个调度，如果它等价于某个串行调度。一般来说，TPS中的冲突等价和视图等价的概念对应于术语重写中的置换等价和因果等价的Meseguer本文从重写逻辑的角度对重写逻辑的证明理论进行了研究。4并行标准化等价平行标准化的目标是将任何约简转化为唯一的代表性平行标准约简。然后，如果两个归约产生相同的平行标准归约，则称它们是平行标准化等价的。由于我们的转换是有效的，并行标准化等价是可判定的。并行标准化过程的想法是对步骤进行范奥斯特罗姆和德弗里耶尔33从外到内的顺序。我们采用了一个对应于倒序排序的并行标准化算法（参见[48]第3.1节）。例4.1考虑自然数列表[3，2，1]和自然序。倒序排序迭代地置换列表中顺序错误的相邻成员对，即所谓的倒序。在示例列表上执行，我们注意到有两个反转：[3，2，1]。假设最左边的反转，3， 2，被选择。在置换之后，列表包含一个逆[2，3，1]。在置换3和1之后，列表包含另一个反转[2、 1、 3]。最后将其置换，得到有序列表[1，2，3]，不包含任何反转。类似地，通过反转的并行标准化包括重复地和非确定性地置换任何一对相邻步骤，这些步骤是错误的，由内而外的顺序。这样的对被称为反标准对（[21]），而没有反标准对的归约被称为平行标准。置换过程可以最容易地描述为重写过程，其中规则是内部和外部置换恒等式的定向版本，其被应用于对由剩余置换恒等式诱导的结构等价取模（参见表1和定义3.2）。结构等价性允许人们将恼人的中间并行约简移开，以便使顺序错误的步骤相邻。例4.2重新考虑我们运行示例的第一个约简f（a，a）→f（b，a）→f（b，b）→g（b）→c第一步和第三步是错误的，由内而外的顺序，但不相邻。结构等价性允许人们通过交换第一步和第二步来移动中间的第二步，从而产生：f（a，a）→f（a，b）→f（b，b）→g（b）→c现在，第二步和第三步构成了一个反标准的对：它们是相邻的，而且顺序是错误的，由内而外。对它们进行置换会导致我们的运行示例的第二次缩减：f（a，a）→f（a，b）→g（a）→g（b）→c请注意，这种归约是并行标准的，因为它不包含反标准对（模结构等价）。由此我们得出结论，减少是平行的标准化等效。我们正式化我们的并行标准化程序通过反演的TRS，产生的外部和内部的身份，证明条款模结构等价。事实证明，平行标准证明项是平行归约，即由平行步骤组成的归约。范奥斯特罗姆和德弗里耶尔34例4.3以这种方式将例4.2形式化，得到：R=f（Q，a）·f（b，Q）·f（b）·ff（a，Q）·f（Q，b）·f（a，Q）·=S其中，我们首先使用结构等价性交换了第一步和第二步，然后应用了并行标准化步骤S2（参见定义4.7）以去除第二步和第三步之间的反标准对由于我们执行了模结构等价的并行标准化步骤，因此我们首先通过计算结构等价类的规范代表来证明结构等价是4.1封圣我们将定义结构等价类的典型代表。这是通过首先将结构身份定向到TRS的规则中，然后将其完成为终止和连续的册封TRS来实现的。这里选择的方向的想法，从左到右排列函子恒等式5定义4.4封圣TRS关于证明条款的规则是：\x{\fnTahoma\fs10\bord0\shad0\1cH00FFFF}\x{\fnTahoma\fs10\bord0\shad0\1cH00FFFF}（x·y）·z<$x·（y·z）f（x1，.，xn）·f（yi，.，yn）f（x1·y1，.，xn·yn）f（x1，.，xn）·（f（yi，.，yn）·z）f（x1·y1，.，xn·yn）·z其中f在（普通）函数符号上变化一个证明项是经典的，如果它是经典化范式。例4.5例3.3的证明项产生相同的规范证明项g（Q，Q）：范奥斯特罗姆和德弗里耶尔35g（Q，a）·g（b，Q）<$g（Q·b，a·Q）g（Q，Q）g（a·Q，Q·b）g（a，Q）·g（Q，b）[5]参见[47]，通过将函子恒等式定向到相反的方向，得到了一个完整的TRS。范奥斯特罗姆和德弗里耶尔36⇒··≡在我们的运行示例中，约简的规范证明项是不同的：f（Q，Q）·f（b）·f和S本身。定理4.6规范证明项是结构等价类的唯一代表。证据 它表面上证明，册封TRS是完整的。要看到经典化是终止的，使用最后两个规则增加共享的事实，即减少（普通）功能符号的数量，以及观察所有规则都是（左和右）线性的。为了证明它是一致的，我们可以观察到最终规则（模式）是由前四个（直接对应于结构恒等式）的Knuth-Benidentical完备化得到的✷因此，计算结构等价类的唯一代表是容易的，因此，决定结构等价也很容易4.2并行标准化定义4.7关于证明项的平行标准化TRS的规则是，对于Q：l→r，xi：si≥til（x1， . 。 ，xn）·Q（t1， . 。 ，tn）n = 0（x1， .. 。，xn）Q（x1， .. 。 ，xn）n=0（s1， .. 。 ，sn）·r（x1， . 。这些规则应用于证明项模结构等价。64. 8在规则s{Q：a→b，n：f（x）→ g（x）}的TR S中存在r f（a）→ f（b）→ g（b）. 它由证明项φ=f（Q）·φ（b）证明很明显，φ是第一个内部规则的redex，重写它会得到φ=φ（Q）。显然，x是第二个外部规则的redex，重写它得到χ = x（a）·g（Q）。请注意，尽管在直观意义上，x在例子中是平行标准的，但它不是平行标准化范式，因为x（a）是外部redex。然而，它只在一个平凡的方式失败：χ<$g（a）g（a）g（Q）χ。我们只是禁止这种微不足道的内在和外在的步骤。定义4.9并行标准化步骤是并行标准化TRS中的一个步骤，使得应用规则中至少有一个替代变量在结构上不等同于循环。一个证明项是平行标准的，如果它是标准形式w.r.t.平行标准化。如果两个证明项具有相同的并行标准化范式模结构等价，则它们是并行标准化[6]请注意，在应用平行标准化规则时，我们并不范奥斯特罗姆和德弗里耶尔37请注意，在结构上不等同于循环就等同于包含一些规则符号。因此，平行标准归约“ 就 是 ” 平 行 归 约 ， 即 平 行 步 骤 的 序 列 ， 因 此 它 们 的 名字 。引理4.10并行标准化完成。证据证明的过程中，显示终止和局部连续性，这两者都是复杂的。局部一致性的证明是通过分析内部规则和外部规则之间的临界对来进行的分析是复杂的事实，并行标准化步骤进行模结构等效。一个收益的情况下，分析规则符号的相对位置的标准形式的证明项。随机置换反转对列表来说已经是不必要的，但是置换反标准对更不必要。这是由于所考虑的术语重写系统是非（右）线性的，而排序是线性的。我们的终止证明的想法是由于Klop（[21]），并通过以下方法显示反转排序的终止考虑一个自然数列表，在这个列表上，通过置换反转进行的排序（比如说以递增或- der）不会终止。由于该列表只有无限多的排列，非终止性意味着排序过程在某个列表上循环。考虑列表，例如[5，3，..。]，在循环。然后要么– 列表的第一个元素不涉及沿着循环的任何排列，但是我们有一个更短的列表（[3，...。]），在其上通过省略第一个元素进行排序循环，或者– 第一个元素参与了沿着循环的排列，但随后它被一个更小的元素所取代（[3，5，.]）。。]）. 由于小于阶的良基性，第一个元素将永远不会被任何置换的更大元素所取代，并且与循环性的矛盾随之而来。在平行标准化的情况下，这一论点是复杂的事实，认为TRS是非右线性。因此，置换不是长度保持的。幸运的是，通过并行标准化可获得的证明项的长度可以通过所谓的有限族发展定理（[40]）来限制。✷下面的定理直接从并行标准化的完备性和并行标准化是通过TRS定义的事实定理4.11（i）平行标准化等价是一个同余。(ii) 如果φ和φ是平行标准化等价的，则src（φ）= src（φ）和tgt（φ）= tgt（φ），对于约简也是类似的（即模约简恒等式）。注4.12（i）结构等价是在一个抽象的公理中研究的。范奥斯特罗姆和德弗里耶尔38RRR我我T R TR[30]在《易经》中，有一种说法是：“君子之道，焉可诬也？”(ii) 早期的结果（[9，15，21]）主要涉及普通标准化，即： 按文本从左到右的顺序对步骤进行排序，原因是λ演算（原型高阶项重写系统）和组合逻辑（原型一阶项重写系统）都是左正规正交系统。上述方法也适用于普通标准化，如[47]所示。平行标准化的引入是最近的起源（[16]），其进一步发展是由[11，19，34]的标准化公理方法引发的(iii) 通过反转来终止并行标准化本质上比通过选择来终止并行标准化更困难，对应于选择排序（参见例如，[48]第3.1节为选择排序，[47]为[30]中的标准化公理确实保证了后者的终止性，同时允许前者的非终止性。5标记等效性在标记中，还原的行为是从内部观察者的观点来看的。标记是重写系统上的一种转换，它保留了重写系统的动态性，但是关于向目标可以记录在目标本身中。因此，标记一个约简产生一个（唯一的）约简J，其中执行与中相同的步骤，但其中对象可能包含额外的信息。例5.1考虑一个非常简单的TRS模型，用于模拟自然数堆栈。 它的签名由空栈顶符号T和一元栈元符号n组成，n ∈ N，其规则为{pushn：T → n（T），popn：n（T）→ T |n ∈ N}。在该TRS中从空栈T开 始 的 减 少 的示 例 是R：T→5（T）→5（1（T））→5（T）→5（3（T））假设现在我们想要记录栈顶符号T中的栈上有多少个数字的信息。为此，我们可以用自然数i来标记符号，例如Ti，并将TRS变为{pushn：Ti→n（Ti+1），popn：n（Ti+1）→ Ti|n，i∈N}。在我们选择了一种标记源的方法后，比如说标记为0，标记产生了一个唯一的标记约简：RJ：T0→5（T1）→5（1（T2））→5（T1）→5（3（T2））如果两个还原的（标记的）目标对于它们的源的任何标记都是相同的，则它们被定义为标记标记的一个重要实例是所谓的L′evylabellinggL，它记录了每个符号的完整历史这意味着你可以从L'evylabelling中获得其他的bellingg范奥斯特罗姆和德弗里耶尔39俄.西↔∈→→N“遗忘”是历史记载的一部分。因此，为了研究标记等效性，必须研究L′evylabellingg等效性。Example5. 2为了使约简和我们的运行示例的L（R）和L（S）（定义5.20）保持可读和清晰，我们已经删除了尽可能多的冗余信息，L（R）：f（a≠，a）→f（ba≠，a）→f（ba≠，ba）→gf（x，ba）（ba≠）→cgf（x，ba）（ba≠）L（S）：f（a≠，a）→f（a≠，ba）→gf（x，ba）（a≠）→gf（x，ba）（ba≠）→cgf（x，ba）（ba≠）请注意，R和S的目标c接收到a=L'evylabelgf（x，ba）（ba），因此原始约简表示L'evlabellingg等价，因此是标记等价的。5.1抽象重写标记我们将标签定义为重写系统的邻接或重复信息当然，这不应该干扰系统的动态，即。重写。也就是说，标记之前和之后的系统应该具有相同的行为。我们通过互模拟的概念正式的行为等价。B B B BJ J J图五. 互模拟：后，关系，前定义5.3关系B是抽象重写系统和J之间的互模拟关系，如果对象与对象相关，步骤与步骤相关，使得– 如果一个B是一个J，那么B将从aJ开始的每一步与从a开始的某一步（向后）联系起来，将从a开始的每一步与从aJ开始的某一步（向前）联系起来，– 如果φB φJ满足φ：a→b和φJ：AJ→jbj，则aB aJ和bB bJ（关系子）。相关的对象或步骤被称为B-双相似性（参见图5，其中表示双相似性）。如果对象（步骤）对于某些互模拟是互相似的，则它们是例5.4黑洞ARS\和无限直线ARS−∞→（的同构副本→J）之间的互模拟B（见例2.3）通过定义，对于所有i（参见图6，其中虚线指示B-相关对象和步骤）– 在对象·B ·i上，并且范奥斯特罗姆和德弗里耶尔40←→→B0J1J2J3J见图6。 互模拟示例– 在步骤B上，将·→ ·与·i→J·i+1联系起来。标记是双向模拟的一种特殊的单向情况。而bisimulation-tion是对称的两个抽象的重写系统，标签是不对称的。这个想法是，虽然可以有一种以上的方式来标记一个对象或一个步骤，不同的对象和步骤不能通过标记它们来相互识别这一思想的第二部分可以反过来说：每一个有标签的对象或步骤都对应着一个唯一的无标签的对象或步骤。定义5.5设B是→和→J之间的互模拟。(i) B是（→to→J）的标号，如果(1) 对于每个aJ，有一个唯一的a，使得aBaJ，并且(2) 对于每个φ：a b和aB aJ，对应唯一的φJ：aJJbJ，使得φ B φJ。 对应必须是双射的，步长用BaJ（φ）表示，称为φ的aJ-标号。(ii) 重写标记B是由标记B和初始标记函数b组成的对，初始标记函数b将对象→映射到双相似对象→J。也就是说，aBb（a）对于所有对象a。我们用B（φ）表示步骤φ：a→b的标号Bb（a）（φ）。这在图7中可视化，其中表示标记和！表示独特性。B B B Bb（）！！J图7.第一次会议。重写标签：反向功能，唯一标签，初始标签注意，标签B的逆是通过唯一性对对象的函数