《理论计算机科学电子札记》59卷第4期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume59.html16页的一类重写规则与逆变换基于规则的等价变换KiyoshiAkama1;2北海道大学邮编：060-0811EkawitNan tajeewaraw at3;4泰国国立法政大学诗琳通国际技术学院P.O.地址：Box 22，Thammasat-Rangsit Post Oceance，Pathumthani 12121，Thailand小池秀胜5北海道大学邮编：060-0811摘要在基于规则的等价变换（RBET）范式中，计算是基于声明性描述的意义保持变换，一组重写规则被视为程序。确定了一大类重写规则的语法。两种不同类型的元变量的合并使得能够精确控制重写规则实例化。这样，重写规则的适用性和规则应用的结果就可以得到严格的规范，从而为重写规则的正确性提供了理论依据。讨论了RBET框架中的逆变换操作，证明了正确的重写规则是可逆的，即，通常可以通过在语法上颠倒另一个正确的重写规则来构造正确的重写规则。1 Akama得到了科学研究补助金（B）（2）#12480076的部分支持。2 电子邮件地址：akama@cims.hokudai.ac.jp3 Nantajeewarawat得到了泰国研究基金的部分支持4 电子邮件地址：ekawit@siit.tu.ac.th5 电子邮件地址：koke@cims.hokudai.ac.jpc 2001年由Elsevier Science B出版。V.CC BY-NC-ND许可下的开放访问。Akama、Nantajeewarawat和Koike21介绍基于规则的陈述性描述等价变换（RBET）[1]是一种新的有前途的问题求解方法。在RBET框架中，问题被公式化为声明性描述，由两组定义子句的并集表示定义部分提供了关于问题域的一般知识和一些特定问题实例的描述。查询部分指定关于定义部分的内容的问题。 在定义部分，提出了一套重写规则，|转换说明性描述的规则|已经准备好了然后，通过将查询部分连续地转换成另一组限定子句，使用准备好的重写规则，从该限定子句可以容易地和直接地获得指定问题的答案，从而解决问题。例1.1考虑一个简单的问题，它被公式化为由四个定义子句组成的定义部分Dinitinitial（ X; Z） append（ X; Y; Z）append（[]; Y;Y）append（[AjX];Y;[AjZ]） append（X;Y;Z）等于（X; X）以及仅包含定义子句的查询部分QC1： ans（X）initial（X;[1; 2; 3]）; initial（X;[1; 3; 5]）.为了解决这个问题，即，为了得到查询部分Q的答案，利用RBET，Q将利用从D初始化准备的重写规则依次变换，直到由两个单元子句组成的较简单的查询部分Q0ans（[]）中文（简体）的答案，即，X=[ ]和X= [1]，可以直接绘制。附录中给出了Q到Q0的一种可能的2重写规则在它的左手边指定它可以应用的原子公式（原子）的模式，并定义它的应用结果通过在其右侧指定一个或多个置换原子的模式。当左手边的模式与子句主体中包含的原子相匹配时，该规则适用于限定子句|换句话说，当包含在子句主体中的原子是指定模式的instances时。当应用时，规则将子句重写为多个子句，这是通过将匹配的体原子替换为规则右侧模式的实例通过模式匹配而不是单一化来确定规则的适用性，允许人们为了计算效率而为某些特定的原子模式定制重写规则。Akama、Nantajeewarawat和Koike3重写规则的说明推迟到第2节。原子模式在确定规则适用性和指定规则应用结果方面的关键作用需要一个适当的语法结构来表示模式，以便能够精确和适当地控制其实例化。为此，引入了Meta原子的概念.元原子具有与普通原子相同的结构，除了两种元变量|&-variables和#-variables|它被用来代替普通变量。 这两类元变量具有不同的实例化特征。该方法不仅允许重写规则的精确指定，还允许严格研究几种转换步骤的几个重要属性，例如，扩展变换的正确性[7]，而且，如[3]所示，从问题规范系统地生成正确的重写规则。在RBET框架中，计算的正确性仅依赖于每个转换步骤的正确性给定一个声明性描述D[Q]，其中D和Q分别表示问题的定义部分和查询部分，通过应用重写规则，当且仅当声明性描述D[Q]和D[Q]是等价的，即，它们具有相同的宣告意义。重写规则被认为是正确的，当且仅当它的应用总是导致正确的转换步骤。正确的重写规则将被称为等效变换规则（ET规则）。如果在所有的转换步骤中使用ET规则，则可以保证通过RBET得到的答案是正确的。1.1RBET与逻辑程序设计范式计算的比较虽然本文所考虑的声明式描述与定义逻辑程序具有相同的逻辑程序设计中的计算是以逻辑演绎为基础的|计算被视为基于归结原理[10]构造存在性量化查询的证明的过程，发送变量替换，称为计算替换，使从给定逻辑程序逻辑地跟随查询。相反，在RBET中，计算被认为是声明性描述的转换，而不是逻辑演绎。程序与声明性描述的分离在逻辑程序设计中，一组定义子句具有双重功能：它作为问题的声明性描述|它声明性地表示关于问题域的知识，并定义问题是什么|同时又作为一个程序|它指明了如何解决这个问题。一组限定子句的编程特性源于查看Akama、Nantajeewarawat和Koike4它是对搜索的描述，其结构是通过将逻辑连接词和数量词解释为固定的搜索指令来确定的[6]。逻辑编程语言（如Prolog）的过程表达能力受到这种固定的过程解释和嵌入在与语言相关的证明过程在RBET框架中，重写规则集被视为一个程序，而不是一组限定子句。限定子句的程序解释可以使用一种基本类型的重写规则来实现，称为基于展开的重写规则[1]。然而，在RBET中还可以采用其他几种重写规则，从而允许更广泛的计算路径，从而可以实现更高效的程序[1]。使用一组重写规则作为程序也使计算灵活|有效的控制策略可以通过例如规则环控制和基于用户定义的优先级的规则选择来实现[1]。正确性的理论基础虽然RBET中计算的正确性仅基于声明性描述的意义保持，但逻辑编程中计算的正确性基于逻辑结果关系（j=），即，给定一个逻辑程序P和一个原子q，一个计算代换是正确的当且仅当Pj= 8（q）。逻辑结果的概念反过来依赖于基本概念，例如，与一阶逻辑相关的模型理论的解释、满足和模型的概念。这些概念在非洲区域局的框架中是不必要的。逻辑程序设计中计算的正确性不能仅仅由推理规则的正确性来保证，它还依赖于所采用的计算过程。当计算过程被改进或扩展时，必须证明整个过程的正确性。 相比之下，为了验证RBET中计算的正确性，需要证明每个重写规则的正确性。因此，RBET框架中的程序可以被分解;因此，基于RBET的系统可以进行修改和扩展。1.2逻辑程序设计中RBET与程序转换的比较目标和转换部分RBET的目标与逻辑编程（PT）中的程序转换的目标不同[8，9]。RBET是一种根据给定的定义部分计算问题答案的方法，而PT是一种从定义部分导出有效逻辑程序的方法。 设定义部分D0。在RBET中，计算查询的答案部分Q0相对于D0，通过连续应用从D0准备的重写规则，从Q0构造序列Q0;：; Qn，使得对于每个Akama、Nantajeewarawat和Koike5initinitiniti（0i n），D0[Qi]和D0[Qi+1]具有相同的陈述意义，答案可以直接从Qn中得到.定义部分D0在整个变换过程中保持不变相比之下，在PT中，只有定义部分被转换。也就是说，从被视为初始逻辑程序的D0开始，通过使用诸如展开和折叠规则之类的变换规则，构造逻辑程序序列D0;：Dm，使得D0和Dm对某类查询产生相同的答案，但Dm比D0更有效;然后，当给出该类中的查询时，程序Dm将用于通过某种证明过程来计算查询的答案。例1.2考虑例1.1的定义部分Dinit。在PT之后，可以使用展开和折叠连续地变换Dinit。规则，输入逻辑程序D0：initial（[ ];Y）initial（[AjX];[AjZ]） initial（X;Z）append（[]; Y;Y）append（[AjX];Y;[AjZ]） append（X;Y;Z）Dinit和D0对预言有相同的宣告意义cates初始和追加;然而，计算查询的答案包含-使用D初始化谓词需要较少的解析步骤而不是使用D init。2在PT中，主要关注的是由转换过程而不是转换过程本身产生的程序的效率。另一方面，在RBET中，由于变换是主要的计算机制，所以要求变换过程是高效的。RBET中转换过程的有效性是通过采用有效的重写规则和适当的规则应用控制策略来实现的[1]。规则的正确性和独立性在PT中，从变换序列D0;：;Dk导出Dk+1的变换步骤是正确的，当且仅当对于每个只包含出现在Dk中的谓词符号的查询q，Dk和Dk+1对q提供相同的答案。PT中的转换步骤的正确性通常不能独立地确定;例如，从变换序列D0;：;Dk导出Dk+1的折叠步骤的正确性需要某些条件以确保在序列D0;：;Dk中已经执行了足够的展开步骤[9]。下一个示例表明，折叠规则的应用可能会产生不正确的转换步骤。例1.3参考例1.1的定义部分Dinit折叠第一子句，即，初始值（X; Z）append（ X; Y; Z），Akama、Nantajeewarawat和Koike6initinit使用其自身产生逻辑程序D00：initial（ X; Z） initial（ X; Z）append（[]; Y;Y）append（[AjX];Y;[AjZ]） append（X;Y;Z）由于在Dinit中定义的谓词首字母的含义在D00中丢失，，这转换步骤不保留关于谓词初始化的查询的答案，因此是不正确的。2相比之下，在RBET中，由于仅转换排他地依赖于固定定义部分的查询部分，因此可以独立地调整转换步骤的正确性，即，给定定义部分D，从查询部分Qj导出查询部分Qj+1的变换步骤的正确性仅由D[Qj]和D[Qj+1]的含义确定，而与其前面的变换步骤无关因此，重写规则的正确性重写规则的这种独立性显然是大规模的基于规则的系统的建设所希望的1.3本文件重写规则。本文的第一个目标是确定合适的语法重写规则的一大类。重写规则组件的语法结构以及它们的实例化应该被适当地定义，以便它们可以被用来精确地指定规则的可应用性和规则应用的结果。重写规则正确性的理论框架。第二个目标是建立一个基于声明性描述的意义保持转换而不是逻辑推理的理论框架来讨论重写规则的正确性。逆变形。第三个目标是引入逆变换运算，并表明在RBET框架中ET规则是可逆的，即，可以获得这样的重写规则，其操作通过在语法上反转另一重写规则而反转该另一重写规则的操作，并且前者的正确性仅取决于后者的正确性。第2节解释了元变量的必要性，并提供了重写规则，反向转换和反向重写规则的介绍性示例第3节定义了初步的句法成分，这些成分用于在第4节中定义陈述性描述及其含义，并在第5节中重写规则，它们的应用及其正确性第6节研究了反向重写规则的正确性。Akama、Nantajeewarawat和Koike72元变量和反向重写规则需要使用两种不同类型的元变量来指定原子的模式，以及调节元变量实例化的条件的必要性将首先描述。然后将介绍反向转换操作和反向重写规则。2.1需要两类考虑例1.1中的定义部分Dinit和查询部分Q和Q0作为导致Q0的可能变换序列的第一步，子句C1：ans（ X） initial（ X;[1;2;3]）; initial（ X;[1;3;5]）可以通过用append（X; Y;[1;2; 3]），导致该条款C 2： ans（X）append（X; Y;[1; 2; 3]）; initial（X;[1; 3; 5]）.此转换步骤是正确的，因为Dinit[fC1 g]和Dinit[fC2 g]具有相同的含义。上述变换步骤可以通过重写规则r1： initial（&X; &Z）！append（&X; &Y; &Z），在那里，我们！“intuitively "的意思是”可以用”代替”，左边的R1的右手侧和右手侧分别指定规则适用的原子的模式和替换原子的模式。符号X、Y和Z在r1中用作实例化通配符，即，它们中的每一个都可以被实例化为任意项，并且也可以被实例化为相等约束，即，同一通配符的每次出现必须被实例化到同一项中。通过将&X、&Y和&Z分别实例化为项X、Y和[1; 2; 3]，左手边的模式匹配C1的第一个体原子，而右手边的模式被实例化为C2的第一个体原子|也就是说，通过使用该实例化将r1应用于C 1的第一个体原子，C1被变换为C2。符号X、Y和Z作为通配符和相等约束的双重作用使人想起变量的概念。尽管如此，这些符号应该区别于在限定子句中使用的普通变量，因为它们被不同地使用;例如，它们可以被实例化为普通变量，但它们在任何替换应用中都不能被普通变量替换。为了强调差异，符号X、Y和Z将被视为元变量，并且将被称为-变量。然而，重写规则r1并不总是指定正确的transform-mation步骤。例如，通过将Y实例化为变量X，将r1应用于C1的第一个体原子，将C1转换为子句C3：ans（X）append（ X; X;[1;2;3]）; initial（ X;[1;3;5]），Akama、Nantajeewarawat和Koike8但Dinit[fC1 g]和Dinit[fC3 g]具有不同的含义。为了确保正确的转换步骤，需要对规则实例进行一些限制另一种称为#-variables的元变量就是为了这个目的而引入的。例如，将使用#-变量#Y来代替r1右侧的-变量Y，即，规则r 2：initial（&X; &Z）！ append（&X;#Y; &Z）将被用来代替r1。然后，该规则的任何实例化都以这样的方式进行管理，即#-变量#Y只能被实例化为普通变量，该普通变量不会出现在应用该规则所产生的子句的其他部分当规则r2应用于C1的第一个体原子时，该实例化约束排除了#Y到普通变量X的实例化;因此，阻止了C1到C32.2逆相变在RBET框架中，正确的转换步骤的反向总是正确的转换步骤。例如，从前面的子部分中所示的将C1转换为C2的步骤，可以具有将C2转换为C1的相反步骤，这可以由重写规则来描述r 3：append（&X; &Y; &Z）！ initial（&X; &Z），后一步的正确性来自前一步的正确性然而，一般来说，规则r3的应用可能导致不正确的变换步骤。例如，通过将-变量Y实例化为X，将r3应用于前一小节的子句C3的第一个体原子会产生从C3导出C1的不正确的变换步骤。再次就业的元变量的两种，不同的实例化特征，补救这个问题。C2到C1的转换可以用重写规则来描述，而不用r3r 4：append（&X;#Y; &Z）！initial（&X; &Z），而将r4应用于C3的第一个体原子可以通过适当地限制#变量#Y的实例化来排除，即，#Y只允许被实例化为在C3的其他部分中不出现的变量。重写规则及其应用的严格描述要求规则应用中元变量实例化的精确条件。为了一般性和规则性，条件不应该专门用于任何特定情况，而是对所有重写规则通用。此类常见条件将在第5节（条件（MVI-1）、（MVI-2）、（MVI-3）和（RRA-2））中定义。注意规则r4可以通过简单地颠倒前一小节的规则r2在第6节中将显示，在RBET中，Akama、Nantajeewarawat和Koike9框架通常可以通过反转另一个正确的重写规则来构造正确的重写规则。3基本句法成分现在将给出本文中使用的字母表;然后，将定义术语和原子的概念，它们是定义子句和声明性描述的基本组成部分，以及元术语和元原子的概念，它们分别用于规范术语和原子的模式。Alphabet- 变量是以符号开头的变量;例如，N和X是-变量。#变量是以符号#开头的变量;例如，#X和#Y是#变量。 一个-变量和一个#-变量一样被称为元变量。一个普通的变量被假定既不以#也&不以#开头。在本文中，假设字母表= hK; F; V; Ri，其中K是常数集，包括整数和零;F是函数集，包括二元函数cons;V是两个集合普通变量的V1，元变量的V2;R是两个互不相交的谓词集合的并集R1=finitial l;append;equal; ：g，R 2= f ans; yes;：g.当不可能混淆时，V1中的普通变量和V2中的元变量将分别简称为变量和元变量。术语、元术语、原子和元原子hK; F; V1i和h K; F; V2i上的一阶项分别称为上的项和元项。给定R0R，在h K; F; V1; R 0i和在h K; F; V2; R 0i上的通常第一级原子将分别被称为R 0上的原子和R 0上的间原子。例如，假设fXiYgV1和&fXiYgV2。那么，nil、X和cons（X; cons（Y; nil））是上的项;nil、&X和cons（&X; cons（#Y; nil））是上的元项; initial（X; cons（X; cons（Y;nil））是R1上的原子; initial（&X; cons（&X; cons（#Y; nil）））是R1上的元原子。采用了列表的标准Prolog表示法;例如，[X; Y]和[7;#X j& Y]分别是术语cons（X; cons（Y; nil））和元术语cons（7;cons（#X; &Y））的缩写。在h K; F; R i上的一级原子称为基原子。接下来，设T是上所有项的集合，G是上所有基原子的集合;还设Ai和A^i是所有原子的集合和所有元原子的集合，分别在Ri上，其中i2f1;2 g.Akama、Nantajeewarawat和Koike10PPP14陈述性描述及其意义通常，RBET框架可以处理除了通常的一阶项之外的几种数据结构，例如，多集、字符串;以及声明性描述可以由一组用这些数据结构扩展的定义子句来表示[2，4]。然而，为了简单起见，在本文中只使用常用术语;也就是说，声明性描述是一组常用的限定子句。现在将定义本文考虑的限定条款和声明性描述以及声明性描述的限定性从句和陈述性描写限定子句C on是形式A的表达式Bs，其中A是R上的原子，Bs是R上的一组（可能是空的）原子。 原子A称为C的头，记作head（C）;集合Bs称为C的体，记作Body（C）;Body（C）的每个元素称为C的体原子。当Body（C）=;时，C将被称为单元子句。在C的右边使用集合符号，以强调体（C）中原子的顺序是无关紧要的然而，为了简单起见，在限定子句的右手边包围体原子的大括号通常会被省略;例如，限定子句ans（X）fappend（Y; X; Z）; initial（Y; Z）g通常写作ans（X）append（Y; X; Z）; initial（Y; Z）。设i2f1;2 g. 一个限定子句C被称为从R1到Ri，当且仅当主体（C）A1和中心词（C）2A i。从R1到Ri的声明性描述是从R1到Ri的一组限定子句。从R1到Ri的所有声明性描述的集合将由Dscr（R1; Ri）表示。陈述性摹状词设S是hK; F;V1 i上所有置换的集合.将替换应用于表达式E（其可以是例如项、原子、一组原子或限定子句）将由E表示。给定一个声明性描述P2Dscr（R1; Ri），2G上的映射TP由下式给出：（2）C = C（2）D&（2 S）&（head（C）2 G）（Body（C）X）g，然后，由M（P）表示的P的含义由下式定义：M（P）=T1（;）[T2（;）[T3（;）[ =STn （;），PPPn=1P其中T1（;）=TP（;）和Tn（;）=TP（Tn1（;））对于每个n 2。5重写规则及其应用和正确性接下来介绍一大类重写规则的语法。再加上对元变量实例化的一些限制，这种语法使人们能够Akama、Nantajeewarawat和Koike11控制重写规则的适用性，并以精确的方式指定规则应用的结果。重写规则R1上的重写规则采用以下形式H^s！！B^s1;B^sn，其中n为0，H^s和B^si是A^1的子集。为了简单起见，可以省略重写规则的每一侧中包围元原子的大括号;例如， 重写规则f initial（&X; &Z）g！ fappend（&X;#Y; &Z）g也会被写成initial（&X; &Z）！ append（&X;#Y; &Z）.元变量实例化元变量实例化是从V2到T的映射，满足以下三个条件：（MVI-1）对于每个#-变量v， （v）是变量。（MVI-2）对于任何不同的#-变量v和v0， （v）6=（v0）.（MVI-3）对于任意-变量u和#-变量v， （五）不发生在（u）。令E^是一个包含Meta变量（E^）的表达式可以是，例如，元项、元原子或一组元原子）。 然后，给出一个Meta-变量实例化 ，让E^表示由E^by得到的表达式在E^中，simulation替换eachchMeta变量u的each chocurrency（u）。重写规则的适用性设r是R1与H^s！！B^s1;B^sn，其中n为0，H^s和B^si是A^1的子集。 设C是一个确定的nite子句AB[B 0从R1到R2重写规则r被称为通过使用元变量实例化可应用于Bs处的C，当且仅当以下条件都满足时：（RRA-1）H^s=Bs。（RRA-2）对于任意的#-变量v， （v）既不发生在A中，也不发生在BAkama、Nantajeewarawat和Koike12中。Akama、Nantajeewarawat和Koike13当通过使用元变量实例化在Bs处将r应用于C时，它将C重写为n个限定子句C1;：;Cn，其中对于每个i（1i n），Ci=（ AB^si[Bs0）.当Bs是一个单点集fB g时，在Bs处将r应用于C也称为将r应用于C的体原子B。当有一个以上适用的重写规则，其中之一将被非确定性地选择，因此，在RBET计算是不确定的。下面给出说明重写规则的应用的示例例5.1参考重写规则r2和r4以及第2节的限定子句C1、C2和C3让：V2！T使得（&X）= X，（#Y）= Y，（Z）=[1; 2; 3]且满足条件（MVI-1）、（MVI-2）和（MVI-3）。然后，由于Y既不出现在C1的头原子中，也不出现在C1的第二体原子中，因此可以通过使用将r2应用于finitial（X;[1; 2; 3]）g处的C1，并且该应用将C1重写为C2。同样地，在f处将r4应用于C2append（X; Y;[1;2; 3]）g，通过使用将C2重写为C1。现在考虑条款C3。 规则r4不适用于C3，因为每个：V2！T so thatappend（& X;# Y; Z）= append（ X; X;[1;2;3]）要求 （X）=X= （#Y），违反条件（MVI-3）。2例5.2考虑重写规则r5：append（&X; Y; Z）！ equal（&X;[]）; equal（&Y; &Z）;！ equal（&X;[#A j#X]）; equal（&Z;[#A j#Z]）; append（#X;&Y;#Z），和条款C4：ans（X）append（X;[E];[1; 2]）。将规则r5应用于C4将C4转换为两个限定子句C5：ans（ X） equal（ X;[]）;equal（[ E];[1;2]）C6：ans（X）e qua l（X;[A1jX1]）;e qua l（[1;2];[A1jZ1]）;append（ X1;[ E]; Z1）通过使用元变量实例化 这样（X）=X，（Y）=[E]，（Z）=[1; 2]，（#A）=A 1，（#X）=X 1， （#Z）=Z 1。 子句C6可以通过应用r5进一步变换.请注意，规则 5也适用于第2节第C2款，见fappend（X; Y;[1; 2;3]）g。2由于第2节的规则r2和例5.2的规则r5分别适用于任何模式的初始原子和任何模式的附加下一个例子说明了为特定模式的原子设计的重写规则Akama、Nantajeewarawat和Koike14例5.3参考例1.1的定义部分Dinit，考虑仅由例5.2的子句C4组成的查询部分假设从定义部分Dinit准备的重写规则包括以下规则：规则六：append（& X;[& E];[& A; Bj& Z]）！equal （ &X;[&A j#W] ） ; append （ #W;[&E];[&B j&Z]）r 7：append（&X;[&E];[&A]）！ 等于（&X;[]）;等于（&E;&A）重写规则r6可以应用于C4在fappend（ X;[E];[1;2]）g处，将 C4转换为子句C7：ans（X）相等（X;[1 j W]）;追加（W;[E];[2]）。然后，通过将规则r7应用于C7在fappend（W;[E];[2]）g处，C7可以转换为子句C8：ans（X）[2][3][4][5][6][7][8][9][10][ 11][12][13][14][15][16][17][18][19][1由此可以得出答案X=[1]与例5.2中规则r5的应用相比，注意到规则r6和规则r7的应用都没有增加查询部分中的子句数量。一般来说，可以通过避免增加子句数量的转换步骤来提高计算效率。2其次，正式定义了重写规则正确的含义重写规则设D2 Dscr（R1; R1）. R1上的重写规则r关于D和R2是正确的，当且仅当对于任何陈述性描述Q2 Dscr（R1; R2）和从R1到R2的任何限定子句C;C1;：：：; Cn，如果r将C重写为C1;：：：; Cn，则M（D [Q[fCg）=M（D [Q[fC1; ：;Cng）。6反向重写规则基于重写规则的正确性的已建立的基础，现在将示出，通常可以通过简单地反转另一个正确的重写规则来构造正确的重写规则。定理6.1（逆重写规则的正确性）设D2Dscr（R1;R1）.设r为重写规则A^s！B^s在R1上 设reverse（r）为重写规则B^s！A^s在R1上如果r对于D和R2是正确的，那么reverse（r）对于D和R2也是正确Akama、Nantajeewarawat和Koike15的。Akama、Nantajeewarawat和Koike16证据设Q是 Dscr（R1;R2）中的声明性描述， C是定义子句 C：HB[ B0从 R1到 R2，令r关于D和 R2是正确的。假设通过使用元变量实例化将reverse（r）应用于Bs处的C。然后，Bs=B^s和reverse（r）将C重写到子句C0：HA^s[Bs0.必须证明M（D[Q[fC0 g） =M（D[Q[fC0 g）. 显然，通过使用Meta变量实例，r适用于集合A1处的C 0。r的这种应用将C0in的体中的集合A^s重写为B^s，等于B。也就是说，C0被这个应用程序重写为C因为r对于D和R2是正确的，所以M（D[Q[fC0 g）和M（D[Q[fC0 g）是相等的。所以reverse（r）对于D和R2是正确的。27结论与逻辑程序设计相关的证明过程中的每一个归结步骤对应于RBET中的一个展开变换步骤，它可以通过使用基于展开的一般重写规则来实现。然而，尽管归结是逻辑程序设计中唯一的推理手段，但在RBET中可以使用各种其他重写规则。因此，RBET框架允许更广泛的计算路径，因此，更有效的程序。尽管它的简单性，RBET框架，使发展的一个坚实的理论基础，以确定各种重写规则的正确性。只要在整个转换过程中使用正确的重写规则，总是可以获得正确的计算。基于RBET的知识处理系统已在北海道大学的各个应用领域中得到了实验性的实现，并取得了令人满意的结果，显示了该框架的实用性在本文中，语法的一大类重写规则的建议。这类重写规则可以表示基于展开的一般重写规则（例如，分别是子节2.1和示例5.2的规则r2和r5子节2.2 的 规 则 r4 例 5.3 的 规 则 r6 和 r7 通 过 引 入 两 类 元 变 量 （ -variables 和 #-variables），该语法便于精确控制重写规则的实例化和应用，这对于保证计算的正确性是必要的重写规则的正确性验证的理论基础制定。介绍了逆变换运算，并证明了一般情况下，只需将另一个正确的重写规则逆变换即可得到一个正确的重写规则。除了本文所指出的使用Meta数据的必要性外Akama、Nantajeewarawat和Koike17在[3]中证明，这两种Meta变量之间的区别也使得在借助于元规则从定义部分系统地生成重写规则的过程中能够对原子模式进行有意义的操纵虽然逆变换在普通计算中可能导致一个内部循环，但它为重写规则的生成提供了类折叠元级变换的基础，而逆重写规则的正确性是验证类折叠元规则正确性的关键。附录参考例1.1，Q可以如下变换为Q0。(The在每个步骤中选择的原子加下划线。）1： ans（X）append（X; Y 1;[1; 2; 3]）; initial（X;[1; 3; 5]）2： ans（[ ]）initial（[ ];[1;3;5]）ans（[1j X 1]）append（ X1;Y1;[2;3]）; initial（[1j X1];[1;3;5]）3： ans（[ ]）append（[ ];Y 2;[1; 3; 5]）ans（[1j X 1]）append（ X1;Y1;[2;3]）; initial（[1jX1];[1;3;5]）4：ans（[]）ans（[1j X 1]）append（ X1;Y1;[2;3]）; initial（[1jX1];[1;3;5]）5：ans（[]）中文（简体）initial（[1];[1;3;5]）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; initial（[1j[2jX2]];[1;3;5]）6：ans（[]）中文（简体）append（[1];Y3;[1;3;5]）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; initial（[1j[2jX2]];[1;3;5]）7：ans（[]）中文（简体）append（[];Y3;[3;5]）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; initial（[1j[2jX2]];[1;3;5]）8：ans（[]）中文（简体）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; initial（[1j[2jX2]];[1;3;5]）9：ans（[]）中文（简体）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; append（[1j[2jX2]];Y4;[1;3;5]）10： ans（[]）中文（简体）ans（[1j[2j X 2]]）append（ X2;Y1;[3]）; append（[2jX2];Y4;[3;5]）11： ans（[]）中文（简体）Akama、Nantajeewarawat和Koike18有几种其他可能的方式将Q转换为Q0，其中一些可能导致比上面所示的序列更短的序列Akama、Nantajeewarawat和Koike19引用[1] Akama，K.，Shigeta，Y.，和Miyamoto，E.，通过逻辑程序的等价变换解决问题，第五届信息系统分析与综合国际会议（ISAS'99）论文集，佛罗里达州奥兰多，1999年。[2] Akama，K.，Kawaguchi，Y.，和Miyamoto，E.， 多集域上等式约束的等价变换（日文），Journal of the Japanese Society for Arti cial Intelligence13（1998），pp. 395{403.[3] Akama，K.， 小池，H.， 和Miyamoto，E.， Program Synthesis from a Setof De Nite Clauses and a Query ， in Proceedings of the Fifth InternationalConference on Information Systems Analysis and Synthesis（ISAS'99），Orlando，Florida，1999.[4] Akama，K.，冈田，K.，和Miyamoto，E.，串域上负约束的等价变换基础（日文），IEICE技术报告，SS 97 -91，pp. 33 {40}，1998.[5] 劳埃德，J.W.，《逻辑程序设计基础》，第二版，扩展版，Springer-Verlag，1987年。[6] Loveland，D. W.和Nadathur，G.，逻辑程序设计的证明过程，在：Gabbay，D。M.，霍格角J.，和Robinson，J. A.（编辑），《人工智能逻辑与逻辑程序设计手册》，第5卷，牛津大学出版社，1998年，页。163{234.[7] Nantajeewarawat，E.， Akama，K.， 和小池，H.， 扩展转换作为重写规则正确性的基础，第二届智能技术国际会议（InTech'01）会议记录，泰国曼谷，2001年。[8] 佩托罗西湾和Proietti，M.，《逻辑程序的转换：基础与技术》，Journal ofLogic Programming 19/20（1994）。261{320.[9] 佩托罗西湾和Proietti，M.，逻辑程序的转换，在：Gabbay，D. M.，霍格角J.，和Robinson，J. A. （编辑）， 《人工智能逻辑与逻辑程序设计手册》，第5卷，牛津大学出版社，1998年，页。697{787.[10] 罗 宾 逊 ， J. A. ， 基 于 归 结 原 理 的 面 向 机 器 的 逻 辑 ， ACM 杂 志 12（1965），pp。23{41.
我的内容管理
展开
