非连续构造函数的图重写系统及其冒泡转换策略

理论计算机科学电子笔记176（2007）3-23www.elsevier.com/locate/entcs用于非确定图重写的惰性上下文克隆*丹尼尔·W.蒋素惠波特兰州立大学P.O.美国俄勒冈州波特兰751号信箱，邮编97207美国摘要针对一类基于非连续构造函数的项图重写系统，定义了一种重写策略，并证明了其正确性. 我们的策略及其扩展到缩小的目的是实现非严格的非确定性函数逻辑编程语言。我们的策略是基于一个图的转换，称为冒泡，避免建设大的上下文的赎回与不同的替代品，昂贵的和经常浪费的操作执行的竞争完整的技术。关键词：非确定性计算，函数逻辑编程，冒泡，图形转换1引言非确定性是函数逻辑程序设计最吸引人的特征之一当一个程序的执行可能会计算具有多个结果的表达式时，它就是不确定的。为了更好地理解这一概念，考虑一个为病人输血而寻找献血者的计划。下面的声明，在库里[18]，定义了血型，哪种类型可以给其他类型：数据血型= Ap|一个|ABP|ABN|Op|对|BP|Bn giveTo Ap = Ap？ABPGiveTo Op = Op？AP？血压？ABpgiveTo Bp = Bp？ABP...部分由NSF资助CCR-0218224支持。1电子邮件：antoy@cs.pdx.edu，brownda@cs.pdx.edu，suhui@cs.pdx.edu（一）1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.0264S. Antoy等人/理论计算机科学电子笔记176（2007）3例如，giveTo的第一条规则规定，A+血型（编码为Ap）可以给予A+和AB+血型的患者。对giveTo Ap的求值非确定性地返回Ap或ABp。“in fix operator“？”, called 还有5个giveTo规则未显示。一个关于人、患者和/或献血者及其血型的小型数据库如下：btype“John”= ABpbtype“Doug”=ABnbtype“Lisa”= An（二）目标是为病人找到合适的输血供体。一个非确定性的程序来解决这个问题是自然的，简洁和优雅。捐赠者x| giveTo(btypey)=:=btypex&x=/=y= y其中y自由（三）当某个献血者y的血液可以输给患者x时，操作donorFor的条件成立，并且确保y不是x，因为不打算自我献血例如，执行donorFor“John”会不确定地产生“Doug”或“Lisa”，而在我们非常小的人数据库中没有找到“Lisa”的供体（2）。该方案的评价是通过缩小。特别地，当评估donorFor的条件时，y最初是未知的，并且变为实例化为合适的值（如果存在的话）。非确定性减少了设计和实现数据结构和算法以将该问题编码到程序中的工作量。程序的简单性使人们相信它的正确性。本文论述了非决定论的实现的理论和实践两个方面。第2节强调了非确定性的典型实现的一些缺陷，并概述了我们提出的解决方案。第三部分介绍了我们的工作背景。第4节定义了我们的战略和相关概念。第五部分证明了我们策略的合理性和完备性。第六节简要论述了扩张战略向收缩战略转变过程中存在的问题及解决办法。第7节简要介绍了相关工作。第8节给出了我们的结论。2动机函数逻辑程序传统上被视为具有构造器规则的项重写系统（TRS）[9，11，12，21]。程序的执行是对一个项重复应用缩窄步骤，直到到达构造函数项，在这种情况下计算成功，或者到达一个不可缩窄的项，并出现定义的操作，在这种情况下计算失败。后者的例子是试图除以零或返回空列表的第一个元素。一个策略计算一个术语上的步骤。从以下项中获得的所有项的集合： 重复应用策略S的项t是计算空间S. Antoy等人/理论计算机科学电子笔记176（2007）35t（根据S）。对于我们考虑的TRS，术语是树状结构。子节点是通过将步骤应用于其父节点而获得的。当策略在同一项上计算两个或多个不同的步骤时，就会出现树分支。当一个父代有多个子代时，策略应用于这些子代及其后代的顺序很重要，尽管大多数函数逻辑语言的策略都不关心这个顺序。应用的顺序只影响如何遍历或探索项的计算空间，而不是空间本身的内容。在实践中，主要有两种方法：深度优先和广度优先。操作上，这些方法分别通过回溯和复制来实现。虽然前者是标准术语，但我们不知道后者的任何普遍接受的名称。我们非正式地描述了每种方法的一个术语的计算。设t[u]是一个项，其中t[ ]是一个上下文，u是一个非确定性地计算为x或y的子项。使用回溯，计算t[u]首先需要对t[x]求值。如果此求值未能产生构造函数项，则计算继续求值t[y]。否则，如果并且当t[x]的评估完成时，解释器可以给用户评估t[y]的选项对于复制，t[u]的计算包括同时，例如，通过交错步骤，独立地评估t[x]和t[y]。如果任何一个求值产生了构造器项，则该项是计算的结果，并且解释器可以向用户提供继续对另一项求值的选项。如果对一个项的求值未能产生构造器项，则对另一项的求值将在不被检测的情况下继续。回溯和复制都被用于FL语言的实现中。例如，PAKCS[17]和TOY[22]是基于回溯的，而FLVM [8]和Tolmach等人的解释器[25]是基于复制的。不幸的是，如上所述的回溯和复制都具有不可忽略的缺点。考虑下面的程序，其中div表示通常的整数除运算符和n是某个正整数。loop =循环f x = 1+（2+（.+（n'd i v 'x ） . ））（四）我们描述的评价t = f（循环？（1）回溯。 如果非确定性表达式的第一个选择是loop，则t的值不会被计算，尽管t有一个值，因为f loop的求值不会终止。这是一个众所周知的回溯问题，称为完整性丢失.自从缩小计算是用适当的策略完成的[4]，在这个例子中，罪魁祸首是回溯。我们描述的评价t = f（0？（1）复制。f0和f1都被计算。当然，第一个的评估失败了。 在这种情况下，问题是项1+（2+（.+））的构造。（n'div' 0）.））. 构造这一项的努力是浪费的，它随着n的增长而变得任意大，因为计算的第一步是除以零，因此计算失败。6S. Antoy等人/理论计算机科学电子笔记176（2007）3因此，复制可能会不必要地构建术语，并且回溯可能无法产生结果。为了避免这些缺点，我们提出了一种新的方法来处理非确定性计算。我们不是只评估一个非确定性选择或为每个非确定性选择复制整个上下文，而是慢慢地非正式地，f（0？1)经历了以下中间术语，其中fail是一个区别，表示任何不能由构造函数术语：f（0？第一章→ 1+（2+（...+（n'div'（0？（1））.））→ 1+（2+（...+（（n'div' 0）？（n' d i v '1 ） ） . ） ）→ 1+（2+（...+ (fail什么？（n 'div'1））.））→ 1+（2+（...+（n'div' 1）.））（五）因为fail发生在需要构造函数根项来执行所需步骤的位置，所以fail选择被消除。由于重写规则匹配在任何位置都不会失败，因此不能从该选择中派生任何构造函数项在这个例子中，我们的方法的明显优点是没有留下任何选择在第二步中，我们将选择操作的父操作分布在其参数上。不幸的是，一个“分配性质”的类型f（x？y）= f（x）？f（y）在共享的情况下是不可靠的。考虑以下操作：fx=（not x，not x）（6）t = f（真？假）。非右线性重写规则（如（6））的评估语义称为调用时间选择[20]。非正式地说，f的自变量的非确定性选择是在f的调用时做出的因此，公式（6）右侧x的实例应该全部求值为True或全部求值为False。被评估的术语如下图左侧所示：（，）不是不（，）？？？不不不不真假真假Fig. 1.左边描绘了一个术语图。 右手边是从左手边得到的不确定性的选择。这两个项图具有不同的构造函数范式集。上图的右侧显示了以类似于（5）的方式冒泡非确定性选择的结果。这个词有四个标准形式。一个是（True，False），这是无法通过回溯或复制获得的，也不是调用时选择语义所期望的因此，虽然有利S. Antoy等人/理论计算机科学电子笔记176（2007）37G在某些情况下，无限制的冒泡是不可靠的。第4节介绍了泡沫的定义，这是合理的，也是我们提出的战略的核心。在[5]中讨论了起泡的一些性质3背景现代FL语言使用窄化来计算[16]。Echahed和Janodet [13]为归纳顺序图重写系统定义了一个理论上有效的窄化策略该策略充分模拟了图共享，但不支持本文的非确定性程序Antoy [3]为重叠归纳顺序项重写系统定义了一个理论上有效的策略。这个类充分地模拟了非确定性--就像本文的程序一样--但它没有考虑共享。我们工作的一个适当的背景理论是上述扩展的组合。不幸的是，这一组合尚未正式确定。我们没有预见到将[13]和[3]结合起来会有任何实质性问题术语图的形式化不依赖于归纳序列性，并且[13]的策略依赖于规则的左侧。将其从归纳顺序TRS扩展到重叠归纳顺序TRS没有问题，因为规则的左侧对于项和项图是相同的。同样，重叠归纳顺序性的概念不依赖于项和图之间的差异，[3]的策略依赖于规则将该策略从术语扩展到术语图也不会造成问题，因为规则图重写的理论比项重写的理论复杂得多。此外，在文献中存在具有非平凡变化的多个呈现在本文中，我们遵循Echahed和Janodet [13]的系统化，因为他们认为的类很适合我们的程序，我们将在后面讨论。本文件所占的篇幅只允许我们回顾关键概念。完整的细节可以在[13]中找到定义3.1设λ是一个签名，X是一个可数的变量集，N是一个可数的节点集。一个环N，N，X上的（有根）图是一个4元组g=Ng，Lg，Sg，R ootsg，使得：1. Ng<$N是g的节点集;2. Lg：Ng→NX是将g的每个节点映射到签名符号或变量的标记函数3. Sg：Ng→N是后继函数，将g的每个节点映射到g的可能空的节点串，使得如果Lg（n）=s，其中s∈NX，并且（对于以下条件，我们假设变量的arity为零）arity（s）=k，则存在n1，...，nk，使得Sg（n）= n1. nk;4. Rootsg<$Ng是g的节点的子集，称为g的根;8S. Antoy等人/理论计算机科学电子笔记176（2007）35. 若Lg（n1）∈ X且Lg（n2）∈ X且Lg（n1）=Lg（n2），则n1=n2，即，g的每个变量标记g的一个且仅一个节点;并且6. 对于每个n∈Ng，要么n∈Rootsg，要么存在从r到n的路，其中r∈R ootsg，即，g的每个节点都是从g的某个根可达的。一个图称为项（图），如果Rootsg是单例的。在图表的图形表示中，例如，如图1所示，我们不显示节点的名称，而只显示它们的标签。节点以下定义对我们的方法至关重要。定义3.2在有根图g中，如果从g的根到n的每条路都包含d，则节点d支配节点n。如果d和n是不同的，那么d在g中适当地优于n。例如，在图1的左手侧曲线图中，“？“只被根支配。除了根之外，其他每一次出现都被它的前一次正确地支配。4形式化该战略的制定包括多个部分。在基于构造器的TRS和GRS中，策略的核心[4，13]是一个函数，它接受一个操作根项或项图，并使用根符号的定义树来计算一个步骤或一组步骤，这取决于程序的类。在[2]中引入了定义树我们在下面回顾这一概念例子见[4]。 模式是f（t1，..的形式的项图。..，t，n是构造器项。定义4.1[定义树]一个运算f的定义树是一个有限的非空线性模式集合T，该线性模式部分地通过包含排序，并且具有以下属性，直到变量的重命名：• [leavesproperty] T的最大元素，称为leaves， 是定义f的规则的所有且唯一的左边的变体。非最大元素被称为分支。• [rootT的最小元素，称为根，是f（X1，. ，Xn），其中X1，. ，Xn是新鲜的、不同的变量。• [parent property]如果π是T的一个不同于根的模式，则T中存在 严格在π之前的唯一模式πJ，使得严格在π和πJ之间不存在其他模式。πJ被称为π的父代，π被称为π的子代。 πj• [归纳性质]一个模式的所有子模式π只在共同的位置上相互区别，这被称为归纳。归纳位置是变量在π中的位置。S. Antoy等人/理论计算机科学电子笔记176（2007）39在基于构造器的GRS中，重写规则是术语图对l→r，其中l是模式。重写规则l→r定义了一个操作fi，如果l的根节点标记为f。一个运算f是归纳顺序的，如果定义f的规则的左边的集合有一个定义树。一个GRS是归纳顺序的，即使它的所有操作都是归纳顺序的。我们考虑一个重叠的归纳序列[3] GRSS.在这个类中，两个规则的左侧可以重叠，但只有当它们是彼此的变体时，即，它们最多通过重命名它们的变量来改变。GRS S包括在介绍中所示的选择操作，由infix运算符“？” and defined by thefollowing rewritex？ y = xx？ y = y（7）我们假设这些是S的唯一重叠规则。使用选择操作可以消除来自其他规则的重叠，而不改变计算[3]。定义4.2 [有限重叠]有限重叠归纳顺序GRS，缩写为LOIS，是一个基于构造函数的GRS，S，使得S包含选择操作“？”在本文的其余部分，我们假设程序可能重叠归纳顺序容许项图重写系统。这些程序将被缩写为GRS。我们记得，一个图是可容许的[13]，如果它的定义操作都不属于一个循环。在我们的方法中，计算由两种步骤组成：一个普通的重写步骤或多步骤，以及我们之前称为冒泡的新步骤。以下定义将冒泡步骤形式化。定义4.3[部分改名]设g=Ng，Lg，Sg，R ootsg是环N，X上的项图，Np是Ng的子集，Nq是与Ng不相交的节点集.部分g关于Np和Nq的重命名是双射Θ：N → N，使得：.nj，其中NJ∈Nq，如果n∈Np;Θ（n）=n否则。通过与置换的术语类比，我们分别称Np和Nq为Θ的域和像我们将Θ重载为如下的图：Θ（g）=gJ是在N，N，X上的图，使得：•NgJ= Θ（Ng），•LGJ（Θ（n））=Lg（n），•Sgj（Θ（n））= Θ（n1）Θ（n2）. Θ（nk）i ∈ Sg（n）= n1n2.对于k0，• RootsgJ = Θ（Rootsg）。简而言之，gJ在所有方面都等于g，除了Ng中的一些节点，更准确地说，所有且只有Np中的节点被一致地重命名为10S. Antoy等人/理论计算机科学电子笔记176（2007）3在gJ.显然，在任何部分重命名中，域和值域的基数是相同的。定义4.4 [冒泡]设g是一个图，c是g的一个节点，使得g在c处的子图的形式为x？y，即，G|c= x？y.设d是g中c的真支配子，Np是g中从d到c的某条路径上的节点集合，包括d和c，即， Np={n|n1n2... nk∈Pg（d，c），且对某些i}，n=ni，其中Pg（d，c）是g中从d到c的所有路径的集合。设Θx和Θy是g的部分重命名具有域Np和不相交的图像。设gq= Θ q（g|d [c←q]），其中q∈ {x，y}.图上的冒泡关系用““表示，定义为g g [ d <$g x？gy]，其中g在d处的替换的根节点是fresh。我们将c和d分别称为冒泡步骤的起点和终点简单地说，冒泡将图中的一个选择移动到支配节点。要执行此移动，必须克隆图形的某些部分，更准确地说是移动端点之间的部分。图2显示了一个冒泡的例子。（，）不是不？（，）（，）？不不不不真假真假图二.左边描绘了一个术语图。右手边是从左手边得到的，通过冒泡到一个适当的支配者，非确定性选择。 两个项图具有相同的集合构造函数范式。冒泡关系需要3个图替换。这些替换中涉及的图都是兼容的[13，Def.（6）彼此。因此，冒泡关系是根据[13，Def.]定义的。9]。我们的方法从不应用选择操作的规则在基于构造函数的GRS中，这相当于将选择符号视为构造函数而不是操作。这会产生深远的影响。一个后果是GRS的每个操作变得不完全定义，例如， 不是（x？ y）不能归约，即使x和y是布尔值。因此，我们使用下面定义的策略来处理涉及选择符号在所需位置的约简第二个后果是计算结果会发生变化，但这种变化更多的是表面上的，而不是实质性的。例如，t = True的标准评估？False有两个结果，True和False。在我们的方法中，t是一个标准形式。在很大程度上，差异仅在于结果的表示简单的转换允许我们将非标准表示作为标准表示来操作。第三个后果是，S. Antoy等人/理论计算机科学电子笔记176（2007）311⎪⎪⎪我⎪⎪⎪⎪⎪⎪⎪程序及其计算空间。 如果不使用重叠规则，只考虑容许图，则程序是连续的。不确定的替换被消除，因此图的计算空间是图的序列，而不是图的树。序列中位置i+1处的图是从具有还原步骤或鼓泡步骤的位置i⎧n（Roott，R）如果T return（R）;⎪如果T = branch（π，o，T，.，T），以及100万美元⎪对某些i，有n个模式（Ti）≤t，n（t，T）3（p，R）;⎪⎪n（p，R）如果T = branch（π，o，T1，.，Tk），⎨n（t，T）3⎪⎪⎪⎪⎪π通过homom在根处匹配t。h：π→t，h（o）用“？”q是h（o）在t中的后继，并且（h（o），t [h（o）←t|q]，T）3（p，R）;n（p，R）如果T = branch（π，o，T，.，T），100万美元⎪π通过homom在根处匹配t。h：π→t，在t用运算f标记h（o），J是f的定义树，⎩其中，（t|h（o），TJ）3（p，R）.n（c，）如果T return（R）;⎪如果T = branch（π，o，T，.，T）和100万美元⎪对某些i，有n个模式（Ti）≤t，n（c，t，Ti）3（p，R）;⎪⎪n（p，R）如果T = branch（π，o，T1，.，Tk），⎨n（c，t，T）3⎪⎪⎪⎪⎪π通过homom在根处匹配t。h：π→t，h（o）用“？”q是h（o）在t中的后继，并且（c，t [h（o）←t|q]，T）3（p，R）;n（p，R）如果T = branch（π，o，T，.，T），100万美元⎪π通过homom在根处匹配t。h：π→t，在t用运算f标记h（o），J是f的定义树，⎩（t|h（o），TJ）3（p，R）.图三.该函数定义了本文关于有限重叠归纳顺序图重写系统的操作根容许项图的策略主题。定义4.5中描述了应用该方法的条件。由于没有非确定性步骤，因此redex只有一个替换。特别地，在机器或实现级别，redex总是可以被替换到位，即，在执行一个步骤时，redex的上下文成为上下文⎪⎪12S. Antoy等人/理论计算机科学电子笔记176（2007）3替代Redex的人为了定义我们的策略，它扩展了[13，Def.29]，我们需要一个定义树的表示。从“？“是唯一的重叠操作，并且我们从不应用它的规则，我们只需要表示非重叠操作的树。我们的表示不仅存储了模式，而且还明确了归纳位置和父子关系。在表象中，符号占统治地位，和branch是用于对树的元素进行分类的未解释函数。具有模式π的叶子的表示是rule（π→r），其中π→r是重写规则的变体。我们表示整个规则，而不仅仅是它的左边，因为这简化了策略的制定。具有模式π的分支的表示是branch（π，o，T1，.，Tn），其中o是π的归纳位置，并且T1，.，Tn是π的所有子元素的表示。定义4.5[HNF策略]函数f取两个参数，一个可接受的操作根项图t和一个部分定义树T，使得模式（T）≤t，并产生一组对（p，R），其中p是t的节点，R是重写规则或区分符号在图t上，由k计算的集合中的一对（p，R）被解释如下。如果R是一个规则，则在t的节点p处可应用具有该规则的重写步骤。如果R是符号四点四我们的策略由案例定义，除了第三种情况之外，在结构上与以前提出的策略相似。直觉上，当在定义树的归纳位置遇到一个选择时，策略会“滑过”选择并继续选择的参数，但其行为会发生变化。这就是为什么引入了函数following并携带一个额外的参数。函数bubble与bubble非常相似，但是如果它在定义树中找到一个规则节点，它将返回一个冒泡步骤而不是一个归约步骤。这意味着，如果没有选择的话，削减是可能的。因此，当且仅当冒泡启用还原步骤时，该策略克隆非确定性选择的上下文的某个部分。当一个redex中有多个选项时，只有最高的选项被选为冒泡步骤的起点。这一点可以从第三种情况下的定义中推断出来。传递给递归调用的选择与原始调用相同。我们将定义4.5从基于操作的项扩展到基于构造函数和选择的项图。我们重载符号，因为意图是相同的定义4.6[策略]设R是LOIS，t是上的容许项图，S. Antoy等人/理论计算机科学电子笔记176（2007）313R的签名。我们定义：⎧巴恩如果t = c（t1，...，tn），或者⎪⎨（t）=i=1C是构造函数还是C =？;如果t = f（t1，.，tn），f是运算，⎪这是一个定义树f。由于应用于容许项图t的策略计算包含若干重写和/或冒泡步骤的集合，在以下定义中，我们指定如何将这些步骤应用于t。注意，如果该策略计算冒泡步骤（p，），则p有一个以操作为根的祖先，我们用o（p）表示，这样从o（p）到p的路径中的每个节点都用构造器符号标记。如果冒泡步骤（p，）的目的地是o（p）或o（p）的祖先，则在o（p）处创建redex。如果冒泡步骤（p，）的目的地是从o（p）到p的路径中由构造器符号标记的节点，则不创建redex。相反，进一步的应用程序将计算刚刚冒泡的选择的另一个冒泡步骤，依此类推，直到选择最终在o（p）或以上冒泡。定义4.7[计算]设R是LOIS，t是R的签名上的容许项图。根据t的计算是序列t=t0→t1→···使得对于所有i>0，ti由ti−1得到如下。 令S=（ti−1）。如果S包含某个冒泡步骤（p，），则ti−1pqti，其中q是o（p）或o（p）的某个祖先否则S={（pk，Rk）}k=1，n，n>0，并且ti−1= u0→（p1，R1）u1→（p2，R2）. →（pn，Rn）un = ti.上述定义在起泡步骤的选择方面（当通过递归计算不止一个起泡步骤时）和重写步骤的应用顺序方面（当计算不止一个重写步骤时）都是不确定的。下面的权利要求表明，这种非确定性并不影响计算结果定理4.8设R是LOIS，t是R的签名上的容许项图。如果tu，对于某项u，则u的构造正规形是t的全部且唯一的构造正规形。证据u的构造函数范式是t的范式[5，引理5]。t的构造函数范式是u的范式[5，定理2]。Q冒泡的关系并没有结束。然而，我们的策略从来没有在只由冒泡步骤组成的有限序列中计算。引理4.9设R是LOIS，t0是R的签名上的容许项图如果t0→t1→t2···是由k计算的无限步序列，则对于每个p0存在一个qp，使得步骤tq→ttq+1不是鼓泡步骤。证据我们定义了一个良好的基序的条款，并证明了冒泡序列减少关于这个顺序。设t是项图，s是t的结点，δ（s）是用运算符号14S. Antoy等人/理论计算机科学电子笔记176（2007）3在从t的根到s的任何路径中，并且令m（s）是序列1 0 0. 0，其中如果s的标号为“？“，或者如果s的标签不是“，则为空序列？“.直觉上，δ是深度，δ是标记为“？“.我们在项上重载：对于任何项图t，（t）=s∈N（t）（s），即，（t）是t的每个节点s的的势头项是所有节点的动量之和。设t和u是项图，其中n（t）= anann−1. a0，其中ai，ni0 是 自 然 数 ， 并 且 an> 0 ， 同 样（ u ） = bmbm−1. b0.我 们 定 义<$（t）><$（u）i <$n > m或n=m，且有存在某个k，0≤k≤n，使得ak>bk，且对所有i，ki≤n，ai=bi。最后，我们将>扩展到项：t>ui（t）>（u）。我们现在证明，如果tcdu由t计算，那么t>u。根据定义4.7，d等于或大于o（c），并且o（c）是操作根的。设k为c的深度。c处的选择被在冒泡步骤中，克隆c和d之间的节点这些节点的深度严格小于k，因为它们在C. 任何其他节点的深度标记为“？”因此，要么δ（u） bk。这意味着，（t）>（u），因此t>u。通过对>的诺特归纳，可以得出不存在由λ计算出的无限序列的起泡步骤。Q最后，我们表明，重写步骤计算的顺序是不相关的。定理4.10设R是LOIS，t0是R的签名上的容许项图，S = S（t）.对于S中所有不同的重写步骤（p1，R1）和（p2，R2），p 1处的R1和p 2处的R2的redex模式是不重叠的。证据t中p1和p2的标号不是“？“，因为不计算的步骤“？“.如果p1 = p2，由于R是LOIS，因此R1 = R2，与假设相反，步骤不是不同的。因此，p1/=p2和R的有限归纳顺序性确保不同的赎回是不重叠的。Q因此，非正式地说，根据t的项t的计算在t上执行有限数量的冒泡步骤，其产生具有与t完全相同的值的新项，和/或一组重写步骤，其应用顺序无关。这些条件决定了策略的正确性它的可靠性是冒泡可靠性的结果[5]。它的完备性是INS完备性的结果[3]。这些主张将在下一节中得到证明。5正确性在本节中，我们证明了我们的策略的正确性。策略的主要目的是计算可以对一个项执行的步骤的子集，以便达到该项的所有值。一个好的策略不会计算那些无助于达到任何项值的步骤，尽管这应该在没有前瞻的情况下实现。只计算一个项的值被称为可靠性。战略S. Antoy等人/理论计算机科学电子笔记176（2007）315计算一个项的所有步骤的子集显然是合理的。由于我们允许泡沫步骤，战略的合理性不是立即的。计算一个项的所有值被称为完备性。一个好的策略应该试图消除尽可能多的步骤证明一个策略是完整的通常是困难的，因为如果删除了一些步骤，可能会丢失一些值在我们的上下文中，即构造器TRS，项t的值是从t导出的构造器范式。 因为我们的策略不遵循“？“，拟订关于健全性和完整性的声明需要做一定的工作。下面的例子说明了这一点。例5.1使用列表的标准函数逻辑符号[18]，考虑项t =[（0？1) +0]。我们的策略将这一项减少到u =[0？1]。很容易证明不存在t到u的导数。然而，这两项都重写为[0]或[1]，这是t的值。项u仅使用“？“.例5.2考虑在（4）中定义的运算循环和项t = loop？0的情况。可以立即验证t→t→t→t→ t···，并且0是t的唯一值。为了解决前面的例子所强调的问题，我们用下面的公式来说明策略的正确性。给定一个项t，根据t的计算会产生一个项，它不会阻止我们达到t的任何值（完备性），同样，也不会使我们达到一个从t不能达到的项（可靠性）。因为这对于一些“无趣的策略”是正确的，例如，不计算步骤的策略，或者只将项减少为自身的策略，我们还表明，给定我们的战略不减少条款植根于“？“.带有标记节点的项 由“？”因此，该策略计算一组值，代表。这个集合的子集，包括单例，可以使用以下形式化获得。定义5.3[提取]设t是一个容许项图。图u是从t中提取，表示为u∈t，如果以下条件之一成立：• intt;• 如果c是t的一个节点，标为“？” and从t [c←t]中提取|x]或t [c← t|y]。下面，我们介绍一些简单的提取性质引理5.4设R是LOIS，t是签名上的容许项图∗钢筋混凝 对所有项u，u ∈ t当且仅当存在一个导子t → u规则”？“只有。∗证据“如果”是通过归纳t → u的步数。唯一的通过归纳的节点数的t标记为“？“.Q16S. Antoy等人/理论计算机科学电子笔记176（2007）3TJ→→∗→→→引理5.5标记为“？“在定义5.3的第二种情况下被选择，并不影响结果。证据 使用提取和还原之间的等效性？- 有根的赎回，我们表明，在其中的顺序？-root的赎回被替换并不影响结果。 设t是一个项图，t的p和q个不同的节点标记为“？和R和Rj的规则？“. 若t→p，Ru和t→q，RJv，对某些项u和v，通过实例分析，在p和q的相对位置中，存在一个项w，使得u→=JW和=p，Rq，Rw.Q引理5.6设R是LOIS，t是R的签名上的容许项图。如果，对于某项u和节点c和d，tcdu，则，对于所有项v，v∈t，如果 且仅当v ∈ u，模节点的重命名。证据设tJ是从t得到的项，通过将c处的子图替换为它的左（或右）后继者，并且设uJ是通过将d处的子图替换为其左（分别）而从u获得的项（右）继承人。根据冒泡的定义，tJ=uJ。因此，如果在t中的c和u中的d处都选择了同一侧，则由引理5.5得出结论。Q我们现在准备陈述并证明我们的战略是正确非正式地，给定一个项t，任何可以从我们的策略从t到达的项中提取的值都可以通过纯重写从t到达定理5.7（可靠性）设R是LOIS，t是环上的容许项图，∗R的签名。 如果t → n ∈v且u ∈ v，其中u是构造函数范式，∗然后t → u，模节点的重命名。证据通过归纳法对长度进行计算. 基本情况：t=v。 通过∗引理5.4，u∈v蕴涵v→u，紧接着是这个命题。单个病例：∗ ∗t→α→βv。如果t→ttJ不是起泡步骤，则根据定义4.7，t tJ。根据归纳假设，tj u，并且，通过传递性，t 联合如果stept→steptJ是一个冒泡步骤，根据定理4.8，每个构造函数范式是t的构造函数范式。通过归纳假设，tJu，因此t→u。Q现在我们来谈谈我们战略的完整性。我们需要一些初步结果。我们的第一个主张类似于平行移动引理。对于正交TRS，定义了一个重写步骤与另一个重写步骤的残差的概念[19，第2节]。我们考虑LOISGRS，它不是正交的，但有一个非常disci-plined形式的重叠。除非两个规则“？” are applied at the same node,和一个推导的推导可以公式化，而不需要对LOIS进行重大修改。特别地，我们使用以下引理。引理5.8（并行重写移动）设R是LOIS，t是R的签名上的容许项图。如果t→p，Ru是重写步骤，并且t→q，RJv是重写步骤，其中RJ不是“？”v→S. Antoy等人/理论计算机科学电子笔记176（2007）317乌鲁杰→w是（q，R）乘（p，R）的残差，v→w是（p，R）乘（q，RJ）模节点的重命名。证据与[19，引理2.2]类似，证明是通过对p和q各自位置的案例分析。Q由于重写的计算执行冒泡步骤，为了讨论交换图，我们需要考虑重写步骤通过冒泡步骤的剩余，反之亦然。执行剩余步骤确保图的可交换性的条件在引理5.10中进行了研究。定义5.9[Resistance集]设S是LOIS，t是S的签名上的容许项图。设tcdtJ，对于t的某个节点c和d，t→p，Ru，对于t的某个节点p和S的规则R.• 我们通过tcdtJ定义t→p，Ru的残差集A。设l和r是c在t中的后继。根据冒泡的定义，tJ= t [d <$Θl（t|d[c←l]）？ Θr（t|d[c←r]）]，其中θl和θr是与相同域和不相交图像的混合。⎧如果p=c，则为n {（d，R）};⎨A={（p，R）}，如果p不在Θ1的域中;⎪否则为{（Θ（p），R），（Θ（p），R）}L r• 我们通过t→p，Ru定义tcdtJ的残差集B如下。⎧ifp =c;B= {（c，cd）}否则。引理5.10（平行起泡移动）设S是LOIS，t是S的签名上的容许项图. 若tcdtJ，对t的某个节点p和S的规则R，t→p，Ru，对t的某个节点p和S的某个节点c，d，t → p，d不在Redex中在t中的Rat ppt→p，Ru通过tcdtJ和u=uJ的残差是以下残差的应用：tcd tJCD通过t → p，Ru模节点的重命名。证据 [5，引理3]。Q我们现在讨论一个相对简单但必不可少的关于我们策略完备性的主张。这一主张是关于INS和INS之间的差异[3]。我们的证明不如本文的其他证明严格，因为比较INS和INS并不简单。虽然INS和INS非常相似，但事实上，我们认为作为INS的一个演变-它们是为不同的框架制定的。INS是项重写系统的缩窄策略，而RNN是图重写系统的重写策略。为了比较这两种策略，我们需要将INS限制为重写，这是微不足道的，并将其重新措辞为图重写，这要费力得多。对这种情况的严格处理将使我们⎪⎪18S. Antoy等人/理论计算机科学电子笔记176（2007）3远远超出了本文的范围幸运的是，所需理论的重要部分已经存在。我们只会非正式地填补空白。Echahed和Janodet [13]将许多需要缩小的结果[6]扩展到项图重写。INS通过增加一维不确定性扩展了所需的缩小范围--从可能的许多规则中选择一个具有相同左侧。INS的这一方面与术语和图形之间的差异无关因此，[13]中的处理提供了缺失理论的核心项重写框架下的计算描述和形式化不同于图重写框架下的计算描述和形式化。前者使用位置和替换，而后者分别使用节点和同态从一个框架转换到另一个框架主要是一个句法任务。例如，在标准项图[24，定义3.3]中使用位置集来唯一地标识没有同构的节点。除了这些句法上的变化，在英语中，只有两个重要的区别。（1）INS不计算冒泡步 ， 而 步 ， 如 果 一 个 节 点 c 标 记 为 “ ？ ” matches an inductive position of adefinitional tree used in the computation of a termC.相比之下，cnc要么冒泡节点，要么递归地尝试独立地减少c的两个后继节点。(2)INS本质上是一种非确定性策略，因为一些赎回有不同的替代品。INS计算项t上的一组步骤，但该组中只有一个步骤被非确定性地选择并应用于t.相比之下，重写是确定性的。（虽然冒泡步骤的选择是非确定性的，但根据[5，引理3]，非确定性是与INS类似，TMF计算项t上的一组步骤。如果这个集合只包含重写步骤，那么集合中的所有步骤都同时应用于t。INS和INS都使用定义树来计算步长。一些操作具有不同构的定义树，例如，见[2，第7节]。对于这些策略，特定树的选择不会影响构造函数范式的计算然而，它可能会改变计算的某些步骤的顺序。因此，在比较策略的行为时，我们将固定任何操作的一棵树，对于两种策略都是一样的，并在我们的推理中使用该树引理5.11（包含）设R是LOIS，t是R的签名上的容许项图。如果INS计算步长t→p，则Ru和R不是“？“， 则 当 两 种 策 略 对 每 个 操 作 符 号 都 使 用唯 一 选 择 的 定 义 树 时 ， （ p ， R ） ∈ N （ t ） 。证据 在相同的定义树选择下，INS和INS经历了相同的情况，除了规则“？“. 如果INS计算的步长不适用“？”, then the same step is computedQ引理5.12（抽取持久性）设R是LOIS，t是R的签名上的容许项图。若u∈t且p∈Nu，则（p，R）∈N（t）当且仅当（p，R）∈ N（u）.证据根据定义4.6，如果t = vl？vr，则n（t）=n（vl）nn（vr）。索赔如下归纳的节点数量标记为“？”QS. Antoy等人/理论计算机科学电子笔记176（2007）319111K引理5.13（冒泡持久性）设R是LOIS，t是R的签名上的容许项图。 若（p，R）∈ N（t），其中R不是“？，且t cd u，则在（p，R）的t cd u的残差集中存在（q，R）使得（q，R）∈ N（u）.证据设Pt= n0n1... nk是从t的根到p的一条路，在对n（t）的计算中产生（p，R）。 根据冒泡的定义，存在一条路径Pu= m0m1. ml在u中，使得除了可能插入单个“？”“怎么样？“. Pu中的每个节点，除了那些对应于可能插入的节点，移除“？”, is the renaming of a corresponding node of 特别地，m0是n 0的重命名，ml是n k的重命名，标记 为“？”w.r.t. Pt当且仅当Pt包含d，且节点标记为“？”Puw.r.t.Pt当且仅当Pt包含c。通过定义，在节点p处的步长的计算仅取决于在p处结束的路径的标签。此