重写演算和λ-演算的理论电子笔记：分配ρ-演算及其应用的统一集成模式识别能力

理论计算机科学电子笔记176（2007）95-111www.elsevier.com/locate/entcs分配ρ-演算HoratiuCirsteab，Cl'ementHoutmannadBenjaminWackbaLORIA，ENS-Cachan，61avenueduPr′esidetWilson，94235CachanCedex，FranceClement. loria.frbLORI ANANCYINANCYII，BP239，54506V和oeuvre-l`es-NancyCedexFrance{Horatiu.Cirstea，Benjamin.Wack} @ loria.fr摘要重写演算被引入作为一种统一集成重写和λ-演算的一般形式。在这种演算中，重写的所有基本成分，如重写规则，规则应用和结果都是第一类对象。重写演算最初被设计用于表达基于规则和面向对象范式的语义。我们以前已经表明，收敛项重写系统和经典的策略可以编码自然的演算。在本文中，我们更进一步，我们提出了一个扩展版本的微积分，允许一个编码无限制的项重写系统。 这个版本的演算有一个新的计算规则，描述了结果结构的行为和一个按值调用的计算策略。我们证明了所得到的演算的连续性和所提出的编码的正确性和完整性。关键词：重写演算，lambda演算，项重写系统，定点。1引言模式识别能力是人类进行推理的主要基本机制之一。e.模式匹配从信息处理建模开始就存在。它的研究可以追溯到模式识别，并且在处理字符串[11]，树[9]或特征对象[1]时得到了广泛的研究。模 式 匹 配 在 函 数 式 编 程 中 也 得 到 了 广 泛 的 应 用 。 G. ML ， Haskell ，Scheme ） ， 逻 辑 编 程 （ e.G. Prolog ） ， 基 于 重 写 的 编 程 （ e 。 G.ASF+SDF[14] ， ELAN[2] ， Maude[13] ， Obj[8] ） ， script programming （ e.G.sed，awk）。它通常被认为是一种方便的机制，用于表达关于函数参数的复杂需求，而不是真正的计算范式。重写演算[5，7]将λ-演算和重写统一起来，使得重写显式对象的所有基本成分，特别是规则应用和结果的概念。它的基本思想是对模式进行抽象而不是简单化1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.06.01096H. Cirstea等人理论计算机科学电子笔记176（2007）95变量，然后产生诸如f（x）Dx的项，可以用λ-风格表示为λf（x）.x。重写演算最初被设计用于表达基于规则和面向对象范式的语义[6]。事实上，在重写微积分中，由规则a→b和b→c组成的术语重写系统（TRS）可以用结构aDb\bDc表示，并应用于常数a由项（aDb|bDc）a，i编码。e.结构的应用，争论。后一项在重写演算中简化为b。如果我们考虑结构aDb\aDc由两个左侧重叠的规则组成，则应用程序（aDb\aDc）a计算为结构b\c，可以将其视为两个项b和c之间的非确定性选择。一般项重写系统和经典指导策略已在原始重写演算[5]中通过添加额外的运算符来编码，该运算符直观地从一组结果中选择一个元素。我们已经证明了等价算子可以在当前版本的微积分中编码，但在这种情况下，编码仅限于收敛项重写系统[7]。我们表明，在本文中，以前提出的编码可以扩展到一般情况下，即。e.任意项重写系统。为此，增加了一个新的求值规则，丰富了结构算子的语义，并通过对求值规则的应用施加一定的纪律来执行求值策略。这个策略在语法上使用适当的值概念来定义，并用于恢复在一般情况下丢失的微积分的连续性。路线图在第2节中，我们给出了所提出的演算的语法和求值语义，并证明了它的一致性。然后在第3节中，我们讨论了微积分的表达能力。更确切地说，我们提出了一个编码（非收敛）长期重写系统的演算。最后，在第四节中，我们总结并给出了这项工作的一些观点。2分配ρ-演算：ρd-演算我们在这里提出的语法和语义的建议演算以及它的主要属性。2.1语法我们考虑下面的元符号“d“（抽象运算符）和“\“（结构运算符），以及（隐藏的）应用运算符。我们假设应用程序操作符关联到左侧，而其他操作符关联到右转三下左转 该应用的优先级高于“d“的优先级，依次，优先级高于“\“。 符号A、B、C、. 在项的集合T上的范围，符号x，y，z，. 在变量集合X（X<$T）上的范围，符号a，b，c，.，f，g，h和由它们构建的字符串的范围在一组K项常数（K T）上。 最后，符号P、Q在图案集合P上变化，H. Cirstea等人理论计算机科学电子笔记176（2007）9597（X P T）.所有的符号都可以被索引。符号stk是表示匹配失败的特殊常量，其语义将在下一节中给出。为了表示一个由项A1.我们将使用向量符号A。此符号将与应用运算符结合使用：AB表示（AB1）.. . ）Bn）。基本重写演算的语法归纳定义如下：P：：= X| K| K P |stk模式不：：= X|K|PDT| T T| T \ T |stk术语我们称之为代数的模式中使用的这个版本的微积分，我们通常表示一项的形式（... （（f A1）A2）.. . ）An，其中f∈K乘f（A1，A2，... ，An）。线性模式是指每个变量最多出现一次的模式。这些值直观地表示我们不需要评估的术语，并通过以下方式进行归纳定义：V：：= X|K| K V| PDT值这些值可以扩展为所谓的结构值和卡住值，这将限制评估规则（γ）、（ρ）和（δ）的应用Vγ：：= V| Vγ\Vγ结构值Vρδ ：：= V|stk卡住值人们可以注意到，唯一潜在的赎回（i。e.值中的变量、抽象或结构的应用）在抽象内部。在下文中，符号V在值的集合V上的范围，符号Vγ在值的集合Vγ上的范围，结构值，符号Vρδ的范围在卡住值的集合Vρδ上 所有这些可以对符号进行索引。定义2.1（自由变量和约束变量）给定一个项A，它的自由变量集为FV（A），约束变量集表示为BV（A），定义如下：FV（x）{x}FV（f）FV（PDA）FV（A）\FV（P）BV（x）=BV（f）=BV（PDA）=BV（A）<$FV（P）FV（A B）FV（A）FV（B）FV（A\B）FV（A）FV（B）FV（stk）∅98H. Cirstea等人理论计算机科学电子笔记176（2007）95BV（A B）=BV（A）<$BV（B）BV（A\B）=BV（A）BV（B）BV（stk）=0H. Cirstea等人理论计算机科学电子笔记176（2007）9599像往常一样，我们工作模e. 自由变量和绑定变量有不同的名字。定义2.2（替换）置换θ是从变量集合到项集合的映射。有限代换θ的形式为{A1/x1. Am/xm}，其定义域{x1，.，xm}表示为Dom（θ）。将θ代入项A，使得Dom（θ）<$BV（A）=A θ，用Aθ表示，定义如下：⎧如果xi∈Dom（θ）xiθ ⎪⎩ 我 否则（PDA）θPDAθ（A B）θ Aθ Bfθ fstkθ stk（A\B）θ Aθ\Bθ我们应该指出的是，由于我们考虑了模α转换的项的类别，因此许多项A都是假设AJ满足BV（AJ）<$Dom（θ）=θ，从而避免了潜在的变量捕获。2.2操作语义重写演算的求值机制依赖于匹配的基本操作，它允许我们将变量绑定到它们的当前值。在一般的重写演算中，我们允许在项上以同余为模进行匹配在匹配时使用的这个同余是微积分的基本参数，当通过定义的同余实例化这个参数时，可以获得不同的实例，例如，语法上，或等式上或以更详细的方式[6]。为了本文的目的，我们只限于句法匹配，在这种情况下，匹配替换，当它存在时，是唯一的，可以通过一个简单的递归算法计算，例如G。Huet [10].ρd演算的运算语义由以下规则定义（PDA）Vρδ→ρAθ若Pθ<$Vρδ（A\B）Vρδ→δAVρδ\BVρδA（Vγ\Vγ）→γAVγ\AVγ当（且仅当）存在这样一个代换θ时，规则（ρ）可以被应用，在这种情况下，它被应用于项A。 如果这样的替换不存在，那么这个规则就不能被触发，这个术语就被保留下来，代表失败。然而，进一步的减少或实例化可能会修改Vρδ，使得适当的X100H. Cirstea等人理论计算机科学电子笔记176（2007）95可以找到替换，并且可以执行规则。规则（δ）将应用程序右分布在结构上。例如，这提供了将两个不同的模式抽象并行应用于给定术语的可能性。规则（γ）是规则（δ）的对应规则，它将项的应用左分布在结构上。应用程序的参数是值的隐含条件本质上与微积分的连续性有关，并在2.3节中讨论。定义2.3（一步关系）由一组规则R导出的一步关系不是→R，并且是由规则集R导出的关系的相容闭包：• 如果t→Ru，则nt <$→Ru;• 如果t<$→Ru，则nf（t1， . . ，t， . . . ，tn）<$→Rf（t1， . . ，u， . . . ，tn）。多步关系，记为→R，是›→R.类似地，由ρd-计算器的规则引起的多步关系表示为→ρδγ，相容闭包定义如下。定义2.4（→ρδγ的相容闭包）在分配ρ演算中上下文是一个特殊的术语，由以下语法定义：C []：：=[ ]| PDC [] |TC [] |C []T |C []\T|T\C→ρδγ的相容闭包是（最精细的）关系→ρδγ，使得如果t →ρδγu，则对于任何上下文C[ ]，我们有C [t] →ρδγC [u]。示例2.5（简单示例+失败）如果我们考虑项（f（x）D（3D3）x）f（3）和（f（x）D（3D3）x）f（4）则得到以下约简：（f（x）D（3D3）x）f（3）→ρ（3D3）3→ρ 3（f（x）D（3D3）x）f（4）→ρ（3D3）4项（aDb\aDc）a简化为b\c：（aDb\aDc）a→δ（aDb）a\（aDc）a →ρb\c项（a Db\b Dc）a类似地简化为b\（b Dc）a。注意，项（aDb\bDc）a并不像人们所期望的那样简化为b相反，规则bDc不适用于a（在经典重写中）的事实也是在最终结果中记录为正常形式的（失败）项当我们希望通过允许可以处理这些特定项的规则来显式地处理失败时，这种方法非常有趣（例如，G. 异常处理机制）。然而，如果用户对匹配失败的显式操作不感兴趣，只是想忽略这样的行为，我们需要统一处理匹配失败，并在对计算不重要时消除它们为此，我们首先希望用常数stk其确切的语义应该如下：如果对于自变量的任何缩减H. Cirstea等人理论计算机科学电子笔记176（2007）95101D如果不存在匹配置换，则ρ-redex被简化为stk：<$θ1，θ2，<$BJ，Bθ1→ρδγBJ<$P θ2/<$BJ（PDA）B→stkstk我们可以很容易地注意到，B可以包含一个ρ-项，它具有任意（可能是无限）数量的可能约简，为了决定是否存在适当的替代，应该对所有这些约简进行探索。因此，这个规则的条件是不可判定的，因此演算的操作语义不能使用这样的规则来定义。然而，在实践中，特别是在处理项重写系统时，我们不需要如此一般，可以使用足够的条件。定义2.6（定义失效）P× T上的关系 f ±归纳定义为：标准/±g B，如果g/±标准stk/±QDBfP1. Pm/±gB1. Bn，如果f/g或n/= m或i，则Pi/±Bif P/± stkfP/±QDB从这个关系开始，ρstk-演算的运算语义由上面介绍的规则（ρ），（δ），（γ）和下面的规则定义：（PDA）B→stkstk，如果P/±Bstk\A→stkAA\stk→stkAstkA→stk stk如前所述，这些规则用于确定、传播或消除定义故障。如果规则的左侧和应用该规则的参数之间的匹配是定义的，那么通过将应用程序转换为stk来明确失败;这是由第一个规则完成的。结构可以被看作是结果的集合，因此我们希望从这些集合中消除所有（匹配）失败;这是通过下面两个规则来完成的。另一方面，stk项可以被视为结果的空集;最后一个规则对应于处理空结构的（δ）规则，因此，对应于故障的传播。我们将在第3节中看到为什么对应于（γ）规则的stk-规则不合适。由→stk导出的关系记为→stk，→stk。关系式→ρδγε →stk为102H. Cirstea等人理论计算机科学电子笔记176（2007）95、、记为<$→stk，其传递自反闭包记为→stk。ρδγ例2.7（失败）项（aDb\bDc）a现在简化为b：ρδγ（aDb\bDc）a→δ（aDb）a\（bDc）a→ρb\（bDc）a→stkb\stk→stkb2.3性能正如我们在前一节中所提到的，如果我们不限制抽象和结构的应用仅在参数是值时有效，ρd-演算就不是当不对（ρ）规则施加这种限制时，得到规则（ρ）和（γ）之间的潜在不可连接的临界对。直观地说，将规则（ρ）中应用程序的参数限制为一个值，可以保证它已经减少到足以检查模式和参数之间是否存在唯一匹配。或者，我们可以接受任何术语作为参数，并使用更复杂的匹配算法来找到适当的替代。例2.8（ρ无值）当规则（ρ）中的值的条件被省略时，可以得到非连续的约简：（xDf（x，x））a\b，γρJf（a\b，a\b）γJf（a，a\b）\f（b，a\b）γ，γJf（a，a）\f（a，b）\f（b，a）\f（b，b），z（xDf（x，x））a\（xDf（x，x））bρ，ρJf（a，a）\f（b，b）类似地，当应用程序的参数不限于（δ）规则中的值时，获得规则（δ）和（γ）之间的临界对。可以通过强制执行此条件或通过使用结构算子的结合-交换基础理论来检索一致性。例2.9（δ无值）当在规则（δ）中不施加任何条件时，H. Cirstea等人理论计算机科学电子笔记176（2007）95103、˛获得：（a\b）（c\d），，δγJ，z（a\b）c\（a\b）dδ，δJ、、、a（c\d）\b（c\d）γ，γJac\bc\ad\bd a c\ad\bc\bd对于（γ）规则，条件要求结构中的项不会退化为失效。如果其中一个可能导致失败，那么它应该首先被减少到stk，然后使用stk规则从结构中消除。例2.10（无数值的γ如果应用于参数的结构项不限于值，则规则（γ）的应用可能导致非连续约简：（xDf（x））（stk\a），，stkγ J，z_（xDf（x））stk\（xDf（x））a（xDf（x））aρ，ρ ρJ Jf（a）f（a）很明显，使用一组值会导致按值调用减少策略。在这种情况下，上述两种结石是一致的。定理2.11（左线性ρd-演算的如果所有的模式都是线性的，则关系→ ρδγ是连续的。证据证明在[4]中有详细说明。它使用了在[12]中为λ演算Q定理2.12（左线性ρstk-演算的连续性）stkd如果所有的模式都是线性的，则关系→ ρδγ是连续的。证据 证明在[4]中有详细说明。它是基于[7，16]中介绍的证明Q无限制ρd-演算是不连续的，因为Klop反例在这种情况下成立（见[4]）。2.4ρd-模同余演算定义一个类似的微积分模某些同余当然很有趣，但超出了本文的范围。这样的扩展将导致一般项重写系统的编码，就像我们现在的演算导致下一节中介绍的语法项重写系统的编码一样。104H. Cirstea等人理论计算机科学电子笔记176（2007）95DD定义这种演算的主要困难来自于这样一个事实，即模匹配给定的同余通常是非酉的（至少对于结合性和交换性等事实上，可能存在（无限）许多解，并且这些解不存在自然顺序（即，e. 替换）。例如，当对符号f的交换性取模时，让我们考虑项（f（x，y）Dx）f（a，b）。存在两种匹配问题：{a/x，b/y}和{b/x，a/y}。 根据我们使用的替代，我们得到两个可能的不一致的减少：（f（x，y）dx）f（a，b）C（f（y，x）dy）f（a，b）ρ ρJ Ja\b\a为了恢复连续性，唯一的解决办法可能最终包括将结构算子声明为交换的、结合的和幂等的。此外，当工作模某些一致性时，应执行特定的约简策略该策略应防止针对未实例化的项进行匹配（zD（（x：：yDx）（a：：z）（b：：c）ρJ（x：：yDx）（a：：（b：：c））ρJz轴（（zDa）（b：：c））ρJa\（a：：b）a最后，定义失败的概念应该适应新演算的归约策略，以保证与所考虑的匹配的一致性。3编码项重写系统我们已经证明了[6，16]收敛项重写系统（TRS）（的约简）可以编码在经典重写演算中。收敛TRS的限制是由于在经典重写演算中对结构算子的“不完全”处理，其中应用算子在结构算子上是左分配的，但不是右分配的。正如我们已经看到的，这种选择是由微积分应该具有的元属性所激发的。更准确地说，增加右分配性将导致非连续微积分。尽管如此，这个属性可以通过对评估（策略）实施一定的纪律[5]或通过限制本文所做的术语构成来恢复在ρstk-演算中，（γ）规则定义了应用程序在结构上的右分布性，在本节中，我们将展示如何使用此功能来在ρstk-演算中编码（非连续）TRS。ρH. Cirstea等人理论计算机科学电子笔记176（2007）95105RΩR更准确地说，给定一个TRS R，我们建立项Ω 1 和ΩR，使得•1m表示（i. e.减少到）一步减少的m w. R. t. R，• ΩRm表示m w的标准形。R. t. R（如果存在）。3.1规则选择当我们希望计算规范形时，我们显然希望决定约简何时有效，即。e. 当R的某些规则可以应用时，然后区分情况：• 如果R某些规则可以应用于m，那么我们减少m，• 如果不是，则m是正规形式，并且m保持原样。这种区分案件的能力，我。e.在两个（或多个）项之间选择一个可以成功地应用于给定参数的项，在重写演算中通常定义为[7]的第一项中编码为：firstuDvDxD（stkDvx\ydy）（u x）可以很容易地检查first是否具有预期的行为：• （第一A1A2）t→stkVρδ若A1t→stkVρδ;ρδγ1ρδγ1• （第一个A1A2）t→stkVρδ，如果A1t→stkstk和A2t→stkV ρδ。ρδγ2ρδγρδγ2直观地，如果我们用编码TRSR的ρ-项R代替项A1，用恒等式代替项A2，那么我们就得到了所需的判别工具：Rt→stkVρδ对应于t w的减少。R. t. 当Rt→stk时，ρδγ1ρδγ对于没有规则可以应用于t的情况，因此该术语保持原样（在事实上，身份适用于此术语）。作为某些项的标准形式，W。R. t.一个非连续的TRS不是唯一的，我们显然必须处理一系列的结果。我们在这里选择将结果集编码为结构。空集由stk和使用结构运算符表示两个集合。在重写演算中，某些集合的表示不是唯一的，因为结构算子不被认为是交换的、结合的或幂等的。由于我们希望区分这样的情况，例如R没有规则匹配m，重新表示为m的一步约简的集合是空的，我们需要在stk上进行模式匹配。的语句如果集合M为空，则T1，否则T2可以被编码为：First（stkDT1）（xDT2）M由于我们需要在stk上进行模式匹配的能力，stkA→stk stk它补充了（δ）规则，但不是对称规则Astk→stk stk106H. Cirstea等人理论计算机科学电子笔记176（2007）95KKK1这将补充（γ）规则，并且这将对应于故障的严格13.2语境传播在重写W。R. t.在重写系统中，规则的应用可以在重写项的任何子项上完成。在重写演算中，规则总是应用于项的头部，因此TRS的编码必须显式地将应用传播到项的更深处。 例如，重写规则a→b对项f（a）的应用由项（f（x）Df（（aDb）x））f（a）正如预期的那样，它最终会减少到f（b）。如果重写规则的应用在给定项的所有子项上都失败，则编码应用的ρ项应减少为stk。 另一方面，如果我们应用与上述相同的朴素方法来将规则应用传播到上下文中，则重写规则a→b对项f（b）的应用是由项（f（x）Df（（aDb）x））f（b）编码，其简化为f（stk）而不是stk。更一般地说，stk的传播应该通过w来执行。R. t. 任何背景下因此，对于来自签名的元数n为1的每个符号f，我们定义一个项Γf：⎛Γf⎝νDxnD（nop（z）Dz）（firststkDnop（stk）yDnop（f（x1，...，xk−1，y，.，xn））⎞⎠（v xk））whherenop∈/nndforanyn1，xnDMx1Dx2D. . . DxnDM.每个Γf允许我们表示给定项对子项Mk的应用f（M1，.，Mn）。 下面的引理陈述了Γ f的行为：引理3.1设f∈ N是元数n的符号。设M1，. Mn是某个代数的项和T是任意项。 令V γ，. V γ是V中的某些值。然后β1pγ如果T M ... M⎜→stkf（M1，. ，Mk−1，Vγ，. Mn）⎟⎟k1nρδγ 我...⎝ \f（M，. 得双曲余切值.⎟⎠，Vγ，.（男）如果T M→ stkVγ\. \Vγ和1k−1pnkρδγ1pI fT M1.如果T Mk→stk stk，则M n → stkstk。k ρδγ ρδγ证据这个引理的证明仅仅在于检查这些归约是否成立。它在[4]中介绍。Q让我们注意到，对于任何模式P1和P2，第一项（P1Dstk）（P2DM）N将总是减少为与（P2DM）N相同的项。实际上，第一个操作符不检查N是否匹配P1，而是如果（P1Dstk）N减少到stk，1这种严格的行为显然可以使用规则stkDstk进行编码。KH. Cirstea等人理论计算机科学电子笔记176（2007）95107KRR ωRRRFRR总是如此。因此，术语⎛stkD stkvDxnD（第一个yDf（x1，...，xk−1，y，.，xn）⎞（v xk））它的行为与f不同。在后一项中使用常量nop允许我们声称stk的减少等同于模式匹配失败。我们现在可以定义项ΓfΓf如果... \rf1N它直观地表示将某项应用于项M = f（M1，. Mn）。将一项T应用于M时得到的不同结果组合在一起的结构是通过减少ρ项ΓfT M得到的：Γ fT M→stkΓ fT M\. \rfT Mρδγ1n3.3一步还原现在让我们考虑项重写系统R={l1→r1，.，ln→rn}。我们不需要通过<$R →R itr a n i v e和r e t e x i v eclosefRi tra n i v e c l o s e来定义R itive c l o s e f R it r a n i v e close。M的所有电子元数据的多个部分都未定义{T|M<$→RT}其中某项T的arity是从M到T的一步约化的次数。最后我们写M→ R！ T当且仅当M→ RT且不存在满足tT→RN的项N。对于所有的非零部件，Mw. R. t. R表示为{T |M → R！其中某项T的arity是从M到T的多步约简的次数。编码一步减少w的项。R. t. 术语重写系统R是表示为Ω1并定义为1ω1 1其中ω1⎛ ⎞πD. \liDri\. \对于所有的li→ ri∈R<$... \f（x1，.，xn）DΓ f（π π）x1. xn\.对于所有f的arityn 1ω1的定义可以分为两部分：第一部分编码重写在头部位置W处。R. t. R，因为我们只通过ρstk-演算中的相应规则来转录R的每个规则;第二个使用项Γf来表示D我们也会在上下文中重写。 术语Ω1K用一个固定点来完成，表达式（π π），以避免使用的Γk，并得到在项需要多少就给Ω108H. Cirstea等人理论计算机科学电子笔记176（2007）95ρδγDRRRρδγRDR定理3.2设M是代数项.• 如果{T|M<$→RT}=0则• 如果{T|M<$→RT}埃森1 M→stkstk.Ω1M→stkT我... \T关于{T |M ›→T}={T，. T}。Rρδγ1pR1p此外，由于左线性ρstk-演算是连续的，如果R是左线性的，且由于T1\... \Tp和stk是正规形式，那么它们是1米证据这个定理的证明是通过对项M的归纳来完成的。它在[4]中介绍。Q3.4正规形归约我们现在定义编码范式约简w的项。R. t. 术语重写系统R.更准确地说，我们想定义一个项ΩR，使得它应用于某个项M，如果Ω1M简化为stk（M是标准形式），则Ω RM简化为M，并且如果它与stk不同，则继续将项ΩR应用于Ω1M的结果。我们”于是，他用这个词来形容。哪里ΩRωRωRωRsDxD第一（stkDx）（zD（s s）z）（Ω1x）我们将继续使用新的相关元素，尽管这些元素在业务服务能力中非常有用一些定义3. 3Therelation−• 对于ytermM，M−M;归纳地定义为：• 对于一个数M、N1和N2，M−<$N1<$M−<$N1\N2和M−<$N2\N1。使用上面的关系，我们可以声明编码的正确性和完整性：定理3.4给定两个代数项M和MJ，M→ R！ MjT，ΩRM→stkTandMJ−T。此外，如果R终止于M，则ΩM→stkT\. \T关于{T|M→T}={T，. T}。Rρδγ1pR！1个p此外，由于左线性ρstk-演算是连续的，如果R是左线性的，且由于T1\...Tp是Ω RM的唯一正规形.ΩΩH. Cirstea等人理论计算机科学电子笔记176（2007）95109D、、证据这个定理的证明首先通过对项M的归纳来完成，然后通过对约化的最大长度w的归纳来完成。R. t. R的一个正规形式。 它使用定理3.2，并在[4]中给出。Q这个定理声称我们对某些项重写系统的编码在ρstk-演算中编码了它的约简。 实际上，ρstk-演算计算有限D d任何项的正规形式的多集合，项重写系统在其上终止。此外，如果系统在某项上是发散的，所有的约简仍然被编码，因为ρstk-演算计算的是一个非终止的约简，生成的范式就像在约简树的广度优先搜索中一样。所有的范式都是在某个迭代中计算的，尽管计算永远不会停止，甚至可能永远不会停止生成新的范式。例3.5（定向群）让我们考虑如下定向的群论公理：i ={e（0），i（1），f（2）}⎧f（x，e）→xf（e，x）→x⎧f（x，i（x））→ef（i（x），x）→ef（f（x，y），z）→f（x，f（y，z））本TRS不一致，因为f（f（i（i（a）），i（a）），a），，，，，，，_，.......f（i（i（a）），f（i（a），a））Jf（i（i（a）），e）Ji（i（a））Jf（e，a）J一110H. Cirstea等人理论计算机科学电子笔记176（2007）95项ω1、Ω1、ωR和 ΩR则定义为：R RH. Cirstea等人理论计算机科学电子笔记176（2007）95111⎜⎜⎜⎟RRRDa→ρδγρδγρδγρδγρδγ⎟⎜⎟⎜⎟⎟⎟⎞⎟⎛⎜2⎜RRRRRR1R⎛ ⎞f（x，e）Dx⎜ ⎟⎜ ⎟f（e，x）Dx⎜ ⎟⎜ ⎟f（x，i（x））Def（i（x），x）De⎟f（x，y，z）Df（x，f（y，z））⎜⎜πDθ⎛ ⎞⎟stkDnop（stk），i（x）D（nop（z）Dz）（第一个⎜⎜⎜yDnop（i（y））⎛（（π π）x））⎟⎟⎟⎜f（x，x）D（nop（z）Dz）（第一阶12stkDnop（stk） ⎠⎜f（X，y）=⎜⎞无菌包装（stk）（（ππ）x1））⎟⎟⎟⎟f（x1，x2）D（nop（z）Dz）（第一阶yDnop（f（x1，y））（（π π）x2））1ω1 ω1，和ωRsDxD第一（stkDx）（zD（s s）z）（Ω1x）Ω RωRωR然后我们在ρstk-演算中有以下约简：一步约化1f（f（i（a）），i（a）），a）→stk1f（i（i（a）），f（i（a），a））→stk1f（i（i（a）），e） →stk1i（i（a））→stk1f（e，a）→stk1stkRρδγf（i（i（a），f（i（a），a））\f（e，a）f（i（i（a）），e）i（i（a））stkastk正规形归约ωΩΩΩΩΩΩΩ112H. Cirstea等人理论计算机科学电子笔记176（2007）95ρδγRΩf（f（i（i（a）），i（a）），a）→stki（i（a））\a后一种约化很好地表达了f（f（i（a）），i（a）），a）w.r.t. TRS R，因为结果i（i（a））\a表示两个标准形式。H. Cirstea等人理论计算机科学电子笔记176（2007）951134结论我们研究了重写演算的一致性和表达能力，其特征在于应用程序在结构上的左分布性，而在以前的版本中只有右分布性演算的连续性，这是危及一个运营商在另一个不小心分配，已恢复使用按值调用减少，并证明使用通常的并行减少技术。由于在重写演算中，ρ-规则的结构可以被看作是项重写系统的朴素编码，因此右分配性规则描述了结构中的每个重写规则对参数的应用。此外，结构也可以用来表示作为这种应用的结果而获得的结果集，左分配性描述了给定规则（或规则结构）并行地应用于许多不同的参数。因此，我们可以在一个术语中编码许多约简路径的同时探索使用左分配与一些早期的技术，我们得到了更好的处理匹配失败，我们能够忠实地编码的任何长期重写系统的行为，甚至是不一致的。这允许许多有趣的理论发展，例如计算给定项的所有范式，这是需要的，例如，完成项重写系统。扩展到一般项重写系统被认为是这项工作的下一步一个主要的困难时，处理匹配模一些同余包括在多重性的解决方案，因为这些解决方案不能在任何自然的方式进行排序，结构算子应被视为结合，交换和幂等。此外，定义失败的概念应适应所考虑的匹配理论，并应强制执行按值调用策略，以防止对未实例化的术语进行匹配，从而避免丢失匹配解决方案。相关工作。V. van Oostrom已经广泛地研究了λ演算与模式的连续性[15]，但它不以结构为特征。我们的TRS编码与S. Byun等人 [3]描述了每个强可分正交TRS到λ-演算的无类型编码。然而，他们需要对原始系统的连续性进行一些非常强的假设。确认我们要感谢克劳德·基什内尔就本文件的主题进行了有益的互动，并感谢热尔曼·福雷对本工作的初步版本提出了详细和非常有益的114H. Cirstea等人理论计算机科学电子笔记176（2007）95引用[1] H. Ait-Kaci，A. Podelski和G.斯莫尔卡一个适用于逻辑程序设计的特征约束系统。Theoretical ComputerScience，122（1-2）：263[2] P. Borovansky，C. Kirchner，H. Kirchner和P. - E.莫罗 从重写逻辑的观点来看。Theoretical ComputerScience，2（285）：155[3] S.边河Kennaway，V. van Oostrom，and F.德·弗里斯序列项重写系统到lambda演算的可分离性和可译性。技术报告tr-2001-16，莱斯特大学，2001年。[4] H. 奇 尔 斯 泰 阿 角 Houtmann ， and B. 变 态 分 配 rho 演 算 技 术 报 告 ， INRIA 洛 林 ， 2006 年 。 可 在www.example.com上获得http://hal.inria.fr。[5] H. Cirstea和C.基什内尔重写演算-第一部分和第二部分。 Logic Journal of the Interest Group in Pure andApplied Logics，9（3）：427[6] H.奇尔斯泰阿角Kirchner和L.利口酒匹配功率。以. Middeldorp，编辑，2001年RTA会议记录史普林格出版社[7] H.西斯泰亚湖Liquori和B.变态用定点重写微积分：无类型和一阶系统。2003年，《类型后处理》[8] K. Futatsugi和A.中川咖啡馆项目的概述 在proc CafeOBJ工作室，1996年。[9] C. M. Ho Mushmann和M. J·奥唐纳树中的模式匹配Journal of the ACM，29（1）：68[10] G.休特Resolution d'Equations dans les Languages d'Ordre 1，2，...，ω。巴黎第七大学国家博士学位[11]D. E. Knuth，J. Morris，and V. Pratt.字符串中的快速模式匹配。SIAM Journal of Computing，6（2）：323[12] M.高桥并行归约在微积分。信息与计算，118（1）：120-127，1995。[13] Maude团队 《Maude Home Page》，2003年。 http://maude.cs.uiuc.edu/。[14] A.范·杜尔森。关于ASF+SDF 语言原型，第1-31页。 世界科学，1996年。[15] 范奥斯特罗姆。Lambda Calculus with Patterns. Technical Report IR-228，Faculteit der Wiskundeen Informatica，Vrije Universiteit Amsterdam，1990.[16] B. WACK。 Typageetd'eductiondanslecalculd'eecrit ure. 这是一个很好的地方，你可以在这里找到一个很好的地方- 南希一世，10月2005年