显式约束的ρ-演算及其应用

理论计算机科学电子笔记117（2005）51-67www.elsevier.com/locate/entcs显式约束应用的ρ-演算Horatiu Cirsteab、Germain Faurea和Claude KirchnerbaLORIA，ENS-Cachan Campus Ker Lann，F-35170 Bruz，FranceGermain. loria.frbLORIANANCYIINRIA，BP239，54506V和oeuvre-l`es-NancyCedexFrance{Horatiu.Cirstea，Claude.Kirchner}@ loria.fr摘要ρ演算的理论表示通常将匹配约束计算视为原子操作，尽管匹配约束是显式表达的。实际的实现必须采取更现实的观点：为了找到匹配方程的解所需的计算在某些匹配理论中可能非常重要，并且替换应用通常涉及项遍历。在λ-演算中的显式替换的基础上，我们提出、研究并推广了具有显式约束处理的ρ-演算，直到替换应用的水平。该方法是通用的，允许扩展到各种匹配理论。我们证明了校准-culus的功能强大到足以处理错误。我们建立了演算的连续性和显式约束处理与应用子演算的终止性。保留字：ρ演算，匹配，约束，显式替换。介绍模式匹配出现在许多编程语言中，作为一种强大的工具来表达对程序参数的需求（例如，G. ELAN[4]，Maude [5]，TOM [20]，ML），并且微积分的计算行为可以真正由其执行模式匹配的能力所决定[9]。很多作品都研究过匹配，但大多数时候都没有充分利用它，如：例如，它们不显式地表达，因此不利用匹配失败。这种表达匹配失败的能力是ρ演算中的关键点ρ演算的引入使得重写显式对象的所有基本成分，特别是规则（抽象），规则应用1571-0661 © 2004 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2004.06.02952H. Cirstea等人理论计算机科学电子笔记117（2005）51和结果。在ρ-演算中，通常的λ-抽象λX.B被替换为规则抽象ADB，其中A是任意项，B是要激发的自变量，A的自由变量在B中有界。ρ演算的匹配能力可以用任意定理来调节在经典的项重写中，这可能导致非确定性行为，但由于表示这些结果的方式也是演算的一个参数，因为根据与结构算子相关的理论获得不同的语义。通常，如果给这个运算符一个结合交换和幂等的状态，那么我们恢复结果集的语义[7]。如果一个人喜欢列表或多集，那么相应的形式化应该被指定。匹配失败可以以不同的方式处理。例如，每一个匹配失败可以被简化为一个代表失败项的特殊项。这可能会导致问题W。R. t.这就是为什么提出了微积分语法和能力的主要演变在[8]中：延迟匹配约束成为演算的显式部分。因此，将抽象ADB应用于项C，表示为（ADB）C，评估为（AC）B，其表示其中匹配约束AC被当存在至少一个解时，在元级求解延迟匹配约束，然后将延迟匹配约束评估为σ1（B）;. ; σn（B）.其中σi，i = 1. n是A与C之间匹配的解。如果不存在解，延迟匹配约束没有减少。通过匹配理论参数化ρ-演算的能力开启了新的可能性，并导致了一个非常有表现力的演算。 然而，令人惊讶的是，所有与所考虑的匹配理论相关的计算仍然属于元水平。同样的情况出现在Rogue [24]中，这是一种基于ρ演算的无类型版本的新编程语言，主要用于实现决策过程。Rogue的操作语义以及ρ演算的规则使用的帮助函数实际上是隐式计算。这些计算在所有匹配理论中都是概念上和计算上重要的，从句法理论到相当复杂的理论，如联想交换理论[12]。因此，为了明确约束的处理，必须明确匹配和约束（substrate）应用。 这就引出了一个λx-演算[23]，它是一个简单的，没有替换成分的演算.我们称之为ρx演算。具有显式替换的λ-演算已经得到了广泛的研究，H. Cirstea等人理论计算机科学电子笔记117（2005）5153提供了一个很好的工具来处理高阶统一[11]或表示类型论中的不完整证明[21]。就实现问题而言，显式替换演算非常重要[18]。在所有的显式替换演算[1，17，23]中，由于Beta 规则将β-redex（λx.a）b转换为用b替换x的替换在a上的显式应用，替换可以延迟。在ρ演算中，匹配约束也可以被延迟，这要归功于一个不计算任何东西但将重写规则的应用转换为匹配约束的应用的规则。因此，它明确了减少给定redex的决定，并提供了决定何时开始应用重写规则所需的计算然后，在一个步骤中计算和应用匹配约束。在具体的实现中，这些操作应该是分开的，应该与其他计算相互作用，特别是，我们希望计算的约束和应用的约束是明确的。我们可以将ρ演算的实现与约束的显式计算和应用看作是使用调度器，该调度器在约束的计算、替换的应用和基本求值规则之间定期切换。贡献：我们提出了一个扩展的ρ演算明确处理匹配约束。 这种演算具有显式替换的一般良好性质（保守性，终止性），并且它是连续的。我们表明，ρ-演算，特别是ρx-演算，是适合作为一个有用的理论后端的实现。路线图：前两节分别描述了ρx演算的语法和语义，展示了它的动机和构造。在第3节中，我们给出了微积分行为的例子，主要集中在错误的处理上。下一节介绍了微积分的主要性质，如线性模式的微积分的连续性。在第5节中，我们讨论了微积分的一些扩展，以增加其表达能力和效率。最后，我们提出相关的和未来的工作。1ρx-演算图1中给出的ρx演算的语法是普通ρ演算语法的扩展，其中抽象（使用“d“运算符构建54H. Cirstea等人理论计算机科学电子笔记117（2005）51信息，并且其中术语可以一起分组到结构中（使用运算符“;”构建）。抽象左边的术语通常称为模式。在原始语法中添加了几个新的结构：• 约束成为演算的第一类对象，并且是形式为A B的匹配问题的合取（用运算符““构建 这样，匹配问题就可以被显式分解。• 将用连接表示的应用操作扩展到约束应用。• 我们使用特殊符号使用这种语法，可以显式处理（传播）替换。我们假设应用程序操作符关联到左侧，而其他操作符关联到右侧。应用的优先级高于“d“的优先级，”d“的优先级高于“;”的优先级，“;”的优先级高于“{}“，而”{}“的优先级又高于“i "。的符号A，B，C，. 在集合T上的范围术语，符号X，Y，Z，.在变量集合V（V T）上的范围，符号a，b，c，...，f，g，h在一组常数K（K ∈ T）上变化。 我们称代数项为形式（…（（f A1）A2）.. . ）An，其中f∈ K，我们通常表示它们通过f（A1，A2，.，An）。匹配方程A的整环B（分别为的约束的共轭）是A的自由变量的集合（相应地， 共轭的每个匹配方程的域的并集）。我们用Dom（AB）表示它。在任何涉及绑定器的演算中，我们对教会，和模数的Barendregt的ene-convention[2]，i. 例如，自由变量和绑定变量有不同的名字。为了支持直觉，可以提到重写规则（抽象）对项的应用总是被评估为将相应的约束应用于重写规则的右侧在经典的ρ-演算中，这种构造被称为延迟匹配约束如果可能的话，约束应用程序将被转换为替代应用程序的集合。为了简单起见，在本文中，替换是XA形式的约束。 当然，替换集可以很容易地扩展到更复杂的约束，例如，X一个小女孩B. 的后一种方法的主要好处是，这意味着几个项遍历可以合并在一起，从而导致更有效的实现[18]。例1.1（λ项的编码）H. Cirstea等人理论计算机科学电子笔记117（2005）5155术语A、B：：=V（变量）| K（常数）| ADB（抽象）| AB（功能应用）| （C）B（限制申请）| A; B（结构）| {X A}B(Substitution application on terms)约束C， D：：=AB（匹配方程）| 约束条件的连接| {XA} C（约束上的替换应用），其中，X A应该是结合交换和幂等的。图1. ρ x-演算我们可以把λ-演算编码到ρ-演算中。绑定器λ演算ρ演算λX.XX深XλX.λY.XXDYDXλX。（二十）XDXX例1.2（一阶项的编码）使用常数tt、ff、not和or（分别表示布尔值true和false、否定、合取和析取），我们可以定 义以下一 阶项 ：and（ X ， tt）and or（not（X），not（Y））。例1.3（重写规则）在布尔代数中计算的一些规则：• 和（X，tt）DX;模式的自由变量和（X，tt）被绑定在抽象的主体X中。• not（and（X，Y））D或（not（X），not（Y））;此规则限制变量X和Y。• xor（X，X）Dff;非线性规则。例1.4（约束应用）seco的应用第二个重写规则在例1.3中给出，not（and（tt，ff））表示为not（and（X，Y））D或（not（X），not（Y））not（and（tt，ff））。我们将在下一节中看到，这一项可以连续减少56H. Cirstea等人理论计算机科学电子笔记117（2005）51到约束应用程序.ΣXttYffO.r（not（X），not（Y））和fter-关于替代申请{Xtt}或，或。2ρx-演算的语义{Yff}or（not（X），not（Y））在经典的ρ-演算中，当将约束的应用减少到一个术语，i。例如，延迟匹配约束，解决相应的匹配问题，并在演算的元级应用所得到的替换。这意味着，在一个步骤中，我们从匹配约束计算替换并应用它。这种归约显然可分为两步，一步是计算代换，另一步是描述相应代换的应用。这种分解并不意味着从约束到替换的匹配计算和替换的应用是显式的，而只是它们被清楚地分离。根据匹配理论，这些计算可能非常重要，我们想进一步研究，使它们明确。图2给出了ρ x-演算的小步归约语义，其中演算的归约规则分为三类：• 描述结构和抽象在ρ项上的应用的规则。• 描述匹配问题的解决的规则（即，e.它们还原为标准形式），并触发所得到的替换（约束）的应用。• 定义替换应用的规则。Term应用程序第一个规则（ρ）和（δ）是从普通的ρ-演算继承而来的。规则（δ）处理应用程序在使用“;”运算符构建的结构上的分布性（见例3.2），而规则（ρ）将抽象的应用程序减少到重写规则右侧的项，该项约束计算规则的分解集与所考虑的匹配理论密切相关，匹配理论是ρ-演算的参数。由于不存在通用算法来决定/解决匹配约束，我们必须在这里精确考虑理论（或理论）。为了简单起见，我们选择用空理论来表示ρx-演算，因此我们引入规则H. Cirstea等人理论计算机科学电子笔记117（2005）5157σ>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>>> ;Term应用程序（ρ）（ADB）C→（AC）B（δ）（A; B）C→ A C;B C约束计算分解（分解;）A1; A2B 1; B 2→A 1B1型 一个2 B2（分解K）f（A1，. .，An）f（B1，. .， Bn）→A1B1型.. . AnBn约束应用（T oSubst）（XA<$C）B→（C）（{XA}B）若X/∈ Dom（C）（T oSubst）（XA）B→ {XA}B（T oSubstId）（aa）B→ B替换应用9（替换）{XA}X→A>>（消去V）{XA}Y→Y>>如果X/=Y>>（消去K）{XA}f→f>>>9>>>>>>>>>>>>>>>>9>>>>>>>>>>>>>>>>>>>>>>>> >==>>ρx>>>>>>=>>最大值>>>>>>>>>>>>>>>> >（Share）{XA}（BC）→（{XA}B）（{XA}C）>=>（共享;）{XA}（B;C）→ {XA}B;{XA}C>>> >>>> >（份额d）{X A}（BDC）→BD{XA}C>>>>>>> >（分享）{XA}（BC）→B{XA}C>>>>> >（分享）{XA}（CD）→ {X A}C{XA}D>>>>的; ; >>图2.ρ x - 演 算 的 小步约简语义（Decompose;）和（DecomposeK）的灵感来自于解决匹配问题的著名算法。在ρ演算中，有高阶符号（e。G. “因此，我们将只分解代数项（i。e.具有一些恒定头部符号的应用）和结构。正如我们之前提到的，ρ演算非常适合处理错误，这些错误由无解约束表示。这意味着存在欺诈->κ58H. Cirstea等人理论计算机科学电子笔记117（2005）51不代表替换的应变1.根据微积分的预期用途，我们可能希望或不希望传播（约束）失败。如果我们传播约束而没有任何解，我们将丢失错误包含在这样一个术语中的信息似乎对分析错误毫无用处，并且出于调试原因，我们不希望丢失错误的位置。 这就是为什么我们需要为了识别其应用表示（i. e.可以减少到）替代应用。一旦获得匹配问题的某个从约束到替换，我们简化一个约束（使用分解规则），直到找到XA形式的约束的子部分。 如果这个不可分解的约束独立于其余的当它是约束的一部分时，我们可以可以注意到，约束X一个小女孩B分解为两个替换：XA和YB，因此，为了将这样的约束应用于项，我们将需要访问整个项两次。还有一个问题仍然存在：如何处理非线性？有很多答案，但最简单的一个是：等到问题变成线性的。尽管看起来令人惊讶，但这是处理这种困难的最佳方法。更准确地说，当我们找到一个形式为X的约束时，一个XB、自没有规则（T oSubst）可以应用（X∈ Dom（XB）我们尝试减少A和/或B，直到我们得到两个相等的项。因此，我们最终得到了约束XAJ（因为假设X是幂等的）或一个不能应用的匹配约束（见例3.3）。替换应用替换的应用由简单的规则定义，这些规则将该应用分布在微积分的不同运算符上，并相应地替换相关变量。因为我们进行模α转换，所以当我们对抽象应用替换时，抽象的左手边不是被替换的。类似地，匹配方程的左手侧（通常从抽象应用程序发出）不受替换应用程序的关注。[1]当然，在λ-演算中，这样的问题不会出现，因为我们只考虑总是成功的平凡匹配问题，并且为了传播相应的替换（即。例如，一步一步来，总是有意义的。H. Cirstea等人理论计算机科学电子笔记117（2005）5159我们应该指出的是，约束应用操作符不能被重载来处理替换，并且需要一个特殊的符号来表示替换应用。否则，似乎很难实现一个明确应用替换的终止和连续的规则系统。像往常一样，我们定义一步→R和多步→R关系w。R. t. 一组规则→R。这样，我们就定义了由图2中的规则导出的关系→σ、→κ和→ρx。3示例在本节中，我们将给出一些例子来说明我们的演算的行为在[13]中，证明了ρx-演算嵌入了λx-演算。下一个示例说明了重写规则应用程序的原子性示例3.1（重写规则的应用）为了计算析取范式，我们使用重写规则不是（和（X，Y））D或（不是（X），不是（Y））。在ρx-演算中，这个重写规则对项not（and（tt，ff））的应用.Σnot（and（X，Y））D或（not（X），not（Y））not（and（tt，ff））.Σ→ ρnot（and（X，Y））not（and（tt，ff））或（not（X），not（Y））→DecomposeK.ΣXttYff.或（非（X），非（Y））Σ›→ToSubst（Xtt）{Yff}or（not（X），not（Y））.Σ›→ToSubst {Xtt}{Yff}or（not（X），not（Y））.Σ→{Xtt}or（not（X），not（ff））置换液附录→或（not（tt），not（ff））替换附录示例3.2（重写系统的应用）我们将展示如何重写规则的结构适用于一个术语。在第一个近似中，这可以被视为重写系统的应用.和（X，或（Y，Z））D或（和（X，Y），和（X，Z））;Σ和（或（X，Y），Z）D或（和（X，Z），和（Y，Z））和（或（tt，ff），或（ff，ff））我们使用（δ）规则来分配两个重写规则：.Σ→δ和（X，或（Y，Z））D或（和（X，Y），和（X，Z））和（或（tt，ff），或（ff，ff））;.Σ和（或（X，Y），Z）D或（和（X，Z），和（Y，Z））和（或（tt，ff），或（ff，ff））60H. Cirstea等人理论计算机科学电子笔记117（2005）51我们最终得到（通过减少每个规则的应用，如例3.1所示）：H. Cirstea等人理论计算机科学电子笔记117（2005）5161或（和（或（tt，ff），ff），和（或（tt，ff），ff））;或（和（tt，或（ff，ff）），和（ff，或（ff，ff）重写系统的应用实际上从来没有像上面介绍的那样简单这里，我们只对一个（Meta）重写步骤进行编码，但通常编码更复杂，因为需要对评估策略进行编码。这个问题是通过使用（类型化的）定点来递归地应用重写系统来解决的（完整的演示见[9示例3.3（非线性重写规则的应用）不存在与可以是非线性的模式集相关的限制（xor（X，X）Dff）xor（tt，tt）.Σ→ρxor（X，X）xor（tt，tt）ff.- 是的Σ›→分解KXttX ttffXttff（幂等）›→ToSubst{Xtt}ff›→消除K FF当然，非线性重写规则的应用可能由于合并冲突而导致失败。合并碰撞不会减少，并将保留为约束应用失败。示例3.4（非线性重写规则的应用）（xor（X，X）Dff）xor（tt，ff）.Σ→ρxor（X，X）xor（tt，ff）ff›→分解K.ΣXttXff ff在下面的例子中，我们将描述如何在ρ演算中定义和使用数据结构。 我们专注于匹配的失败案例。 我们处理列表的例子，并支持直觉，我们也给ML语法中的示例。例3.5（O'CAML中的析构函数在O'CAML [ 25 ]中#letcarl =匹配l与|x：：m ->x;;#letcdrl = matchl with| x::m-> m;;这些都是部分函数，因为我们不能将它们应用于[]而不引发异常，该异常编码匹配失败。62H. Cirstea等人理论计算机科学电子笔记117（2005）51==return[];异常：Match_failure（“"，12，42）。例3.6（ρ演算中的析构函数）在ρ-演算中，数据结构构造函数是用常量定义我们将使用常量“Empty“ 和 “Cons“ 来 表 示 O'CAML 中 对 应 于“[]“和“：：“的列表构造函数。 在ρ演算中，析构函数写为：car Δ Cons（X，M）DX和cdr Δ Cons（X，M）DM。将car应用到列表Cons（a，Empty）中可以简化为常数a：（Cons（X，M）DX）Cons（a，Empty）→ρ（Cons（X，M）Cons（a，Empty））X›→分解K （X）一个妇女组织空）X→ a当我们将car应用于Empty时，我们得到了（Cons（X，M）DX）空→ρ（Cons（X，M）Empty）X与O'CAML不同实际上，警告：这种模式匹配并不详尽。下面是一个不匹配的值的例子：[]在O'CAML中 由于归约语义，在ρ演算中自动完成下一个示例说明了当我们想要跟踪失败的来源（原因）时，例3.7（运行时错误：匹配失败）让我们考虑下面的规则，检查两个人是否是兄弟，i。e.如果他们是同一个父亲：Brother（Person（Name（X），Father（Z）），Person（Name（Y），Father（Z））Dtt当检查两个具体的人（爱丽丝和鲍勃）是否是兄弟时，通过将此规则应用于相应的术语：兄弟（人（名字（Alice），父亲（John）），人（名字（Bob），父亲（Jim）作为结果，我们可以得到（ZJohnZJim）tt这表明对应于父亲的变量Z不能是实例的。H. Cirstea等人理论计算机科学电子笔记117（2005）5163正确的，我。e. 这两个人的父亲不是同一个. 在经典（非显式）方法中，结果将是兄弟（人（名字（X），父亲（Z）），人（名字（Y），父亲（Z）”兄弟（人（名字（Alice），父亲（John）），人（名字（Bob），父亲（Jim） tt这显然更难理解。4性能我们在这里提出的性质的演算及其子演算。我们集中在一致性上，这是实现的基本属性：用于应用ρx演算的求值规则的策略（图2）对结果没有影响。我们首先提出的微积分的显式部分的属性，然后我们使用这些结果的微积分的conciliuence完整的证明可以在[13]中找到。处理非线性匹配的高阶系统的连续性仍然是一项艰巨的任务，因为我们不知道如何防止Klop [16]首次创造的不可连接的临界对，因此，在本文中，我们将只考虑线性模式，以免失去连续性。4.1显式部分显式微积分的一个重要性质是守恒性。这个性质表明ρ-演算的约化可以在ρx-演算中模拟。此属性有时称为模拟：引理4.1（保守性）对于所有仅包含一阶模式2的项A和B，且使得A <$→ ρB，我们有A → ρxB。从这个引理出发，我们可以推出ρ-演算对ρ -演算由于我们不处理复合和元变量，我们还推测ρx-演算保持了强规范化。为了证明ρx-演算的连续性，我们首先证明了演算的显式约束处理部分引理4.2关系→κ是强正规化的。首先，我们定义了一个测度，表示约束匹配方程左侧的不同变量的数量，但是[2]对一阶模式的限制是由于对一阶匹配的限制。回想一下第2节“约束计算”中的讨论64H. Cirstea等人理论计算机科学电子笔记117（2005）51而不是替代品。例如，X不被认为在{ X A } B中的约束匹配方程的左手侧，而这是在（XA）B中的情况。我们证明了→κ是强规范化的，使用字典积的，其中是递归路径排序引起的优先级>：>和{}>;和{}>“应用运算符”，{}>D和{}>和{} >d，符号{}的状态为“多集”。Q引理4.3关系→κ是局部连续的。证明了<$→σ是收敛的，因为<$→σ是作为→κ的子关系终止的同时又是一个正交左线性系统。记为↓σ（A）Aw的标准形式R. t.重写系统σ，并且我们示出以下替换引理：对于所有项A，B，C，使得Y属于A的自由变量集：↓σ（{XA}（{YB}C））= ↓σ（{Y{XA}B}（{XA}C））替换引理是显式替换和纯替换之间关系的结果：我们可以证明显式替换{XA}B的行为表现为（i.e. reduce）与元替换（处理变量捕获）完全一样。证明是通过分析所有的关键对，可以很容易地显示可连接的替代的结果，引理Q4.2线性模式连续性的证明是基于Yokouchi我们通过选择关系式→κ和→ρδε来应用它，其中→ρδε是ρ和δ的并行化。所以，我们需要证明→κ的收敛性（已经做过了），强收敛性的关系以及这两种关系之间的相干图。引理不能简单地通过取关系→ρδ来应用，因为这个关系没有钻石的属性。引理4.4（YokouchiA→ ρδ<$C则存在项D使得B → κ→ ρδ<$→ κD和C → κD。当从A到B和从A到C的两个步骤不重叠时，引理很容易。所以我们必须检查每一个关键对。在λσ-演算中，由于平行约化，临界对的意义与标准对略有不同。由于ρδredex的严格子表达式永远不会与κredex重叠，因此通过从A到B的推导来工作是足够的。QH. Cirstea等人理论计算机科学电子笔记117（2005）5165K定理4.5（推论）ρx-演算对于线性模式是连续的。证明我们已经证明了所有的假设横内引理• → κ是强正规化的（引理4.2）。• → κ是局部连续的（引理4.3）。• → ρδε是强连续的（没有任何临界对的线性重写系统的并行化）。• → κ和→ ρδθ验证了Yokouchi图（引理4.4）。因此，我们得到→κ→ρδε →κ是连续的。 为了得出结论，我们可以注意到→ρxε→κ→ρδε→κε→ρx。Q5扩展在实践中，我们的演算是限制性的，人们希望扩展它的表达的原因（更多的匹配理论）和效率的原因（组成的替代）。在本节中，我们将简要讨论这两点。我们只处理了定义符号的语法匹配的情况，我们可以把这看作是我们演算的一个缺点。在实践中，有趣的是有可能推理模（方程）理论w。R. t. 定义的常数。这可以通过调整处理显式匹配的演算部分来完成。（分解K）规则可以根据人们想要处理的理论进行调整。例如，如果我们想处理交换符号（不一定是二进制），我们得到规则（分解C）-其中Sn表示排列{1，.，n}：C.ΣnJ J J分解K f（A1，.，An）Cf（Al，.，An）→;n∈Sni=1A我CA类（i）如果喜欢AC（结合-交换）匹配理论，则应指定相应的分解规则。在大多数应用中，“;”结构的空理论是不充分的。例如，如果想要编码多集，AC理论是有用的。如果想在ρ演算中编码重写系统，需要一个特殊的结构理论，以便消除匹配失败（该理论在[9]中提出）。在这种情况下，必须仔细检查微积分的连续性。就效率而言，本文将替换定义为XA形式的约束。这种方法的一个主要缺点是66H. Cirstea等人理论计算机科学电子笔记117（2005）51=缺乏将不同的项遍历合并为单个项遍历的机制这种机制被证明对性能有重要影响（例如参见[18]），并用于SML的实现。例如，如果我们表示gn（f（X，Y））Δ g（g（... g（f（X，Y），则（X）一个小女孩（f（X，Y））›→ρx（XA）{YB}gn（f（X，Y））→ρx（XA）gn（f（X，B））的首次遍历›→ρx{XA}gn（f（X，B））→ρxgn（f（A，B））的第二次变换因此，我们需要遍历两倍的项（可以是想要的大小）来应用这个非常简单的替换。事实上，我们只想访问一次，而不是两次，也就是说，我们想处理组合。当然，由于想要识别可解约束，因此需要提出一种很好的方式来标记可解且独立于其余约束的约束部分。代替 为此，应增加以下组成规则：（合成）{C}（{D}A）→ {C<${C}D}A其中C和D是已知为可解的约束目前正在对这一扩展进行研究。结论和今后的工作我们提出了一种适用于处理错误的显式约束应用的ρ-演算。我们证明了它具有这样一种形式的经典性质，即：例如，演算的连续性和约束处理部分的终止性。我们已经看到，微积分实际上是模块化的，可以适用于许多匹配理论，用于定义常数和结构算子“;"。我们可以选择是原子的，并给出替换的简单定义，或者更一般和有效的，并定义一个处理替换组合的演算。ρ-演算，特别是ρx-演算，是新的框架，可以被看作是一个新的编程语言家族的理论基础。ρ-演算的不同扩展/变体现在可用：在[19]中提出了演算的命令式版本，在[14]中研究了ρ-演算中的例外可以说，ρ演算允许H. Cirstea等人理论计算机科学电子笔记117（2005）5167来设计非常强大的类型系统，例如[8]中提出的类型系统。相关工作：在[3]中，引入了一种称为PSA-演算的演算。重写规则的显式应用和显式匹配处理在ρ演算的这个祖先中首次被创造出来。然而，这是第一种进行显式重写的方法，因此这种演算实际上不如当前的ρ-演算强大。例如，PSA演算不够强大，无法将策略作为显式对象，因此规则和策略之间存在层次结构。在文献[6]中已经提出了一种具有显式替换的重写演算。这种演算主要是λσ-演算的一种扩展，称为ρσ-演算。这种方法比这里提出的方法更不通用，因为这种演算明确了替换应用，但没有明确从约束到替换的计算。在[22]中，Nguyen研究了一个合作Coq-ELAN来自动化证明助手，其中ρσ-演算已被广泛用于表示重写推导的证明项在ρx-演算中对匹配的显式处理应该是在一些非平凡匹配理论中获得规范化迹的有用工具。未来的工作：在实现之前，应该研究不同的扩展• 处理替换组合。实际上，将不同的结构遍历合并为一个的能力对性能有重要影响，如[18]所示。• 去处理α转换。一种可能的方法是遵循关于微积分的工作[15]或使用deBruijn [10]索引。• 提出了一个强大的命名异常机制，利用非常通用的错误管理。更一般地说，我们想了解ρ演算的解释器/编译器意味着什么以及如何实现它，这个问题与我们研究集成编程和证明环境的意图密切相关，在这种环境中，计算和演绎是统一集成的，即. 例如， 为了统一基于函数和 重 写 的 语 言 （ 例 如 ， 例 如 ， 在 一 个 实 施 例 中 ， ML ， ELAN ，Maude），proof assistants and theorem provers（e.例如，在一个实施例中，Coq，Isabelle，PVS，.）的。引用[1] M. Ab adi，L. 卡尔德利山口-L。 库林，和J。-J. 我也是。 这是一个很好的例子。 在《函数式编程》中，1（4）：375 -416，1991年10月。[2] H. P. Barendregt. Lambda演算，它的语法和语义。逻辑与数学基础研究。北荷兰，1984年。第二版。68H. Cirstea等人理论计算机科学电子笔记117（2005）51[3] P. Borova n sky'，C. K ir chner和H. Kirchn er. 一个用于ELAN语义的重写和解释的函数。《计算机科学基础国际杂志》，2001年。[4] P. Borova n sky'，C. K ir chn er，H. K ir chner，P. - E. 莫雷阿乌和C。 Ringeissen. 一个超越自我的世界伊兰。 见1998年WRLA会议记录[5] M. Clavel，S. Eker，P. Lincoln，and J. Meseguer. Maude的原则1996年WRLA'96会议录，ENTCS第4卷，1996年[6] H. Cirstea.Cal culder′e′ecriture：fondement s ettapplications. Th`esedeDoctorat，Uiversit′e HenriPoi n c ar′e- N a n c y 1，F ra n c e，O c to b e r 2000.[7] H. Cirstea和C.基什内尔重写演算-第一部分和第二部分。在逻辑杂志的兴趣小组在纯粹和应用逻辑，9（3）：427[8] H.奇尔斯泰阿角Kirchner和L.利口酒用（out）类型重写微积分。见2002年WRLA会议记录[9] H.奇尔斯泰阿角基什内尔湖Liquori和B.变态 重写演算中的重写策略。 载于2003年6月《世界资源报告汇编》[10] N. G.德布鲁因lambda演算与名称自由的公式，涉及符号表示参考变换映射。IndagationesMathematicae，40：348[11] G. Dowek，T. Hardin和C.基什内尔通过显式替换实现高阶统一。在信息与计算，157（1/2）：183[12] S.艾克通过二分图匹配的关联交换匹配。计算机杂志，38（5）：381[13] G.福雷显式重写演算。硕士论文，IRISA，LORIA，ENS-Cachan，2003年9月。[14] G. Faure和C.基什内尔重写演算中的错误。在2002年7月，LNCS的第2378卷，RTA'02的Proc.[15] D.亨德里克斯和V.范奥斯特罗姆。 微积分。 在Proc. of CADE[16] J. 克洛普组合还原系统。博士论文，数学中心-阿姆斯特丹，荷兰，1980年。[17] P. 莱斯坎从λσ到λv，通过显式替换演算的旅程见POPL '94会议记录ACM，1994年1月[18] C. Liang，G. Nadathur和X.气内涵语境中lambda项的表示与归约策略选择。技术报告2003/2，明尼苏达大学，2003年10月。[19] L.利口酒和B.P. Serpette。一个命令式重写演算。2004年8月，LNCS，PPDP'04会议记录[20] P. - E. 莫罗角，澳-地Ringeissen和M.维特克一个多目标语言的模式匹配查询器 在proc 的CC'03，LNCS的第2622卷，第61-76页，2003年5月。[21] C. Munnoz. 不符合要求的替代品将使您的产品具有更高的性能。 THE`ESEDDOCTORAT，UNIVERSIT'EPARIS7，NOVEMBRE1997.[22] 问：H.阮。 在ELAN中验证术语重写证明。 在Proc.of RULEENTCS，2001年9月。[23] K. H.玫瑰函数式程序设计语言的操作约简模型。 博士论文，丹麦哥本哈根大学，DIKU，1996年2月。[24] A. Stump，A. Deivanayagam ，S. Kathol，D. Lingelbach和D. Schobel。流氓决策程序。2003年，国际自动推理决策过程语用学研讨会[25] E. Chaillo u x，P. 妈妈，还有B。 PaganoD′eveloppementd' app l i c at i on sav e c O b j e ct i v e Cam l. O'Reilly出版社两千