惰性函数逻辑程序的声明式调试器

113网址：http://www.elsevier.nl/locate/entcs/volume64.html63页一个懒惰函数逻辑程序拉斐尔卡瓦列罗1; 2马里奥罗德里格斯阿尔塔莱霍1; 3Dep.信息和方案系统马德里孔普鲁腾斯大学西班牙摘要我们提出了一个声明式调试器，用于具有多态类型规则的惰性函数逻辑程序。每当用户认为计算出的答案是错误的（错误症状），调试器就会找到导致错误的程序片段（函数定义规则）。症状和错误的概念具有说明性意义。到一个预期的程序语义。通过在计算树中搜索来执行搜索，计算树是计算的逻辑表示。根据已知的技术，我们的工具是基于程序转换：转换后的程序返回计算树以及源程序预期的结果。我们的转换是可证明正确的w.r.t.良好的类型和程序语义。作为w.r.t.相关的方法，我们解决了一个以前公开的问题，有关使用咖喱功能，我们提供了一个正确的方法，以避免多余的问题，用户在调试过程中。调试器的原型实现是可用的。计划将个案研究和扩展作为今后的工作。1引言声明式语言对实际应用的影响受到许多已知因素的抑制，包括缺乏调试工具，其构造被认为是懒惰函数式语言的障碍正如在[29]中所讨论的，这样的调试器是需要的，并且仍然可以从它们的构造和使用中学到很多有趣的东西。用于惰性函数逻辑语言的编译工具[11]甚至更难构造。1 西班牙CICYT部分支持的工作（项目CICYT-TIC 98 -0445-C 03 -02/97\TREND”）2 电子邮件地址：rafa@sip.ucm.es3 电子邮件地址：mario@sip.ucm.esc 2002年由Elsevier Science B出版。诉在CC BY-NC-ND许可下开放访问。114一种有前途的方法是声明式调试，它从用户认为不正确的计算（错误症状）开始，并定位导致错误的程序片段。在（约束）逻辑程序的情况下，错误症状可以是错误的或丢失的计算答案[26，13，6，17，28]。声明式调试也适用于惰性函数式编程[21，22，23，27，18，20，25]和组合函数式逻辑编程[19]。所有这些方法都使用计算树（CT）[19]作为计算的逻辑表示。CT中的每个节点表示计算步骤的结果，该计算步骤必须通过某种逻辑推理从其子节点的结果得出。诊断通过遍历CT进行，向外部预言机（通常是用户）询问问题，直到找到所谓的有缺陷的节点，其结果是错误的，但其子节点具有所有正确的结果。用户不需要在操作上理解计算。任何有错误的节点都代表一个错误的计算步骤，调试器可以显示负责它的程序片段。从解释的角度来看，声明式调试可以描述为由两个阶段组成，即CT生成和CT导航[22]。我们提出了一个声明式调试器的错误答案懒惰的功能逻辑程序与多态类型的纪律。根据已知的想法[22，20，25]，我们使用程序转换来生成CT。 我们提供了一个详细的说明-在此基础上，给出了该变换的优点。以前各项有关的，我们描述了一些新的技术，允许避免冗余的问题，以甲骨文在导航阶 段 。 调 试 器 已 实 现 为 T OY 系 统 的 一 部 分 [14]; 原 型 版 本 可 以 从www.example.com下载http://titan.sip.ucm.es/toy/。作为未来的工作计划的案例研究和扩展的调试器声明式调试的一个已知扩展是抽象诊断[3，1]，导致等效的自底向上和自顶向下诊断方法，这些方法不需要预先给出错误症状。为了有效地实现，抽象诊断使用抽象解释技术来建立预期程序语义的一个nite抽象。这些方法超出了本文的范围。其余的文件组织如下：第2节回顾了初步的概念和以前的结果，功能逻辑编程和declar- ative调试。第3节总结了我们的新贡献w.r.t.以前的相关作品。我们的CT生成和导航方法，以及对新贡献的详细解释，将在第4节和第5节中介绍。 结论和未来工作计划概述于第6. 主要结果的详细证明包括在附录A中，附录B包括一些简单的调试会话。115我们假设一个可数集TV ar的类型变量 ;·一个可数的TC上的多态签名是三元组= hTC; DC;FSi，在哪里2预赛Functional Logic Programming（简称FLP）旨在整合当前函数和逻辑语言的最佳功能;参见[11]的调查。本文讨论了惰性FLP语言的声明式调试，如Curry或T OY[12，14]，其中包括纯LP和惰性FP程序作为特殊情况。在这一节中，我们回顾了关于懒惰FLP程序的语法、类型规则和声明性语义的基本事实。我们遵循[9]中给出的形式化，但使用T OY的具体语法作为程序示例。2.1类型、表达式和替换2.1.1类型和签名等级字母表TC =S具有语法n2N 类型构造函数C的TCn。 类型2 T型：：=（2 TV ar）j（C1：n）的2019 - 05 - 2201：01：02（ ！0）j（1;：;n）通过connve ntion，Cn表示（C1： n），\！“屁股贴着钻机，你好！一号机！！你好！中出现的类型变量集写为tvar（）。一个类型称为单态itvar（）= ;，否则称为多态。 一个没有你的存在的时代！“称为数据类型。DC =Sn2N DCn和FS =Sn2N FSn是数据构造函数resp. 定义的功能符号。 每个n元c2DCn都有一个主元类型声明c：：n！ C k，其中n; k0的整数;1;：;k是成对的不同的，i是databases，而tvar（i）f1，...，kg对于所有1我n（所谓的透明性）。此外，每个n元f2FSn都带有一个主类型声明f：：n！得双曲余切值.我，是任意的类型。在实际上，每个FLP程序P都有一个签名，它对应于P中出现的类型声明。 任何签名，我们都要写？用新的数据构造函数扩展的结果是什么？： ：，用于表示属于每种类型的未定义值。作为记法约定，我们使用c;d2 DC，f; g2 FS和h2 DC[ FS]，并将h2DC[ FS]n的元数定义为ar（h）= n.2.1.2表达式和模式在后续，我们总是假设一个给定的签名，往往没有明确的符号。 假设一个可数集V ar的（数据）变量X; Y;：不相交的电视ar和，部分表达式e 2 Exp？具有语法e：：=？jXj h j（e e 0）j（e 1;：; e n）116不Subst？ 并类似地定义。我们将域dom（）定义为所有域的集合其中X 2V ar; h2 DC[ FS.形式为（e e0）的表达式表示表达式e（作为函数）应用于表达式e0（作为参数），而表达式（e1;：; en）表示具有n个分量的元组。像往常一样，我们假设应用程序关联到左边，因此（e0 e1：en）替换（（：（e0 e1）：）en）。在e中出现的数据变量的集合被写为var（e）。一个表达式e被称为封闭的ivar（e）=;，否则称为开放的。此外，e称为线性i，每个X2var（e）在e中只出现一次.部分模式t 2 P在？Exp？被构建为t：：=？ j X j c t 1： t mj f t 1： t mj（t 1;：; t n）其中X 2 V ar; c 2 DCn; 0 m n;f 2 FSn; 0 m n和ti部分模式用于所有1 im。它们表示表达式值的近似值 根据指称语义的精神[10]，我们认为P在？作为一个语义域的nite元素的集合，我们定义的近似序v作为最小偏序P在？满足以下性质：什么？ 对于所有的t 2 P？.当这两个表达式是模式，1我 M.（t 1;：：：; t n）v（s 1;：：：; s n）whenever t i; s i 2 P at？，tiv si forall 1我P在？以及更一般地任何偏序集（简称为偏序集）可以通过称为理想完备化的技术被转换成语义域;参见例如：[16]第10段。形式为f t 1：t m的部分模式，其中f2 FS n和m< n作为函数作为值的方便表示;参见[9]。表达和模式没有任何出现？称为全。我们写Exp，分别表示总表达式和模式的集合。实际上，符号？它永远不会出现在程序的文本中;但它可能会出现在调试会话中，正如我们将要看到的那样。2.1.3取代全替换是一个映射：Var！具有唯一扩展名^的P at：Exp！Exp，它也将被记录为。所有替换的集合记为Subst。 所有部分替换的集合：Var！ P在？被表示为变量X标准差（X）6=X，并且范围an（）是SX2 dom（）var（（X））.作为通常， = fX17！t1;：; Xn 7！tn g表示用domain替换fX1;： ：;Xn g，其中对于所有1in，满足（Xi）=ti。 根据约定，我们写e而不是(e)，则，，）=（e）对于任何e。对于任何子集Xdom（）我们定义了限制X 作为置换0，使得dom（0）=X，且0（X）=（X），对于所有的X2A.我们还定义了两个替换的不相交并集1[2]，117扩展名^：类型！类型，也称为. 所有类型替换不相交域，作为替换 这样dom（）= dom（1）[dom（2），（X）=1（X）对于所有X 2 dom（1），以及（Y）=2（Y）对于所有的Y2 dom（2）。从Var到自身的恒等映射id称为恒等替换，任何表现为从Var到自身的双射映射的替换称为重命名。两个表达式e和e 0被称为变体i，有一些重命名使得e=e 0。Exp上的包容序是由条件ee 0ie 0=e对某些2Subst定义的。并扩展到Subst？通过定义0i0=对于一些2Subst？.对于任何一组数据变量X，我们使用符号 0[X]（分别为0[nX]），以表明X 0=X 持有一些2Subst？ 和所有的X2X（分别为 所有X62X）。另一个有用的概念是应用程序的oximation排序对Subst？，由条件v0i（X）v0（X）定义，对所有的X2Var.到目前为止，我们已经考虑了数据替换。类型替换可以类似地定义，因为映射t：TV ar！类型，具有唯一的t t上面为数据替换（例如域、范围、组合、重命名等）提供的大多数概念和符号对于类型替换也是有意义的，我们将在需要时自由使用它们2.1.4良好类型的表达式受Milner的类型系统[15，4]的启发，我们现在引入良好类型表达式的概念.我们定义一个类型环境为数据变量的类型假设X：：的任何集合T，使得T不包括同一变量的两个不同假设。类型环境的域dom（T）和范围ran（T）分别是所有数据变量的集合。在T中出现的类型变量。 对于任何变量X2dom（T），唯一的类型使得（X：：）2T记为T（X）。 表示法（h：：）2var用于指示包括类型声明h：：直到类型变量的重命名。类型判断（;T）`WTe：：通过以下类型推理规则导出：VR（;T）`WTX：： ，如果T（X）=ID（;T）`WTh：：t，如果（h：：）2var？;t2TSubstAP （;T）`WT（ee1）：：，if（;T）`WTe：：（1！），（;T）`WTe1：：1，对于一些12T类型TP（;T）`WT（e1;：;en）：：（1;：;n），if（;T）`WTe1：：1;：;（;T）`WTen：：n注意，前面的类型推理规则可以处理多形类型，118e因为签名中包含的类型声明被解释为类型方案，如推理规则ID中所示我们将模拟一个序列 （;T）`WTe1：：1;：;（;T）`WTen：：n作为 （;T）`WT n：：n，while（;T）`WTa：： ;（;T）`WTb：：将是缩写为（;T）`WTa：：* b.一个表达式E2 Exp？ 如果存在某个类型环境T和某个类型，则称之为良类型的，从而可以导出类型判断T`WTe：：。允许一个以上类型的表达式称为多态。一个良好类型的表达式总是允许一个所谓的主类型（PT），它比任何其他类型都更通用。其PT决定其子模式的PT的模式称为透明模式。[9]更多详情2.2计划和目标2.2.1良好类型的程序一个良好类型的程序P是一组良好类型的定义规则，用于其签名中的函数符号。主体类型为dec-decf：：n的f 2 FS n的定义规则！具有以下形式（R）ft 1：t n！r（CLe|ft-ha{nzdsi}de是的，|h{azn}d侧Co{dzit}ion并必须符合下列要求：(i) n是透明图案的线性序列，r是表达式。(ii) 条件C是原子条件C 1;：; C k的序列，其中每个C i可以是形式e == e 0的可连接性语句，其中e; e 02 Exp，或者是形式d！s，其中d2 Exp和s2 P为。(iii) 此外，条件C必须是可容许的w.r.t.变量集X =def var（f tn）。通过定义，这意味着C中出现的所有近似语句的集合必须允许某种顺序排列，比如d 1！s 1; ; d m！sm（m 0），使得以下三个性质成立：(a) 对于所有1我var（si）\X=;(b) F或所有1im，si是线性的，并且对于所有1jm，i6=jvar（s i）\var（s j）= ;。(c) 对于所有1我m; 1Ji：var（si）\var（dj）=;.(iv) 有一些类型环境T具有domain var（R），它在以下意义上很好地类型化了定义规则：(a) 对于所有1我n：（;T）`WTt i：：i.（b）（;T）`WT r：：.(c) 对于每个（e == e0）2C，存在某个2T型使得（;T）`WTe：：*e 0。119(d) 对于每个（d！s）2 C存在某个2 T类型使得（;T）`WTd：：*s.在编程语言T OY[14]中，程序规则以某种不同的方式编写，即：（R） ft1：tnLe|ft-ha{nzdsi}de！R是的，|h{azn}d侧（JC乔纳比尔岛|ty{zc}条件其中LDl o cal|d{ezn}个项目在这种语法中，程序规则的条件C被分成两部分：一部分JC由可连接性语句e == e 0组成，另一部分LD由近似语句d！s，其被理解为对模式s中出现的变量的局部定义。这就产生了上述第㈢项要求。事实上第（iii）（a）、（iii）（b）项要求局部定义的变量彼此不同，并且远离规则左侧出现的变量，这些变量充当形式参数。第（iii）（c）项确保仅当j> i时，局部定义号i中定义的变量才能在局部定义号j特别是，这意味着局部定义不能递归。非正式地说，像上面（R）这样的程序规则的预期含义是，只要实际参数与模式t i匹配，并且可连接性条件和局部定义都满足，对函数f的调用就可以减少到r。通过将e和e 0评估为某个公共的总模式，可以满足条件e == e 0。一个地方性的定义！通过将d评估为与s匹配的某个可能的部分模式来满足s。程序语义的精确公式将在2.3节中给出.2.2.2一个简单的程序下面我们展示一个简单的示例程序，它是用T OY语言的具体语法编写的。在此语法中，局部定义d！s写为Sd，并且它们必须以文本顺序出现，第2.2.1节中解释的受理要求。T OY还允许在x运算符中使用：来构建表达式，例如（X：Xs），它被理解为（（：）X Xs）。程序的签名可以很容易地从其文本中包含的类型声明中推断出来。特别是，数据声明提供了关于类型构造函数和数据构造函数的主要类型的完整信息。%数据[A] = [] j A：[A]head：：[A]！一条尾巴：：[A]！[A] head（X：Xs）！ X尾（X：Xs）！ XS120map：：（A！B）！【A】！[B]两次：：（A！A）！A！ 一地图F []！[]两次F X ！F（F X）映射F（X：Xs）！FX：map FXsdrop4：：[A]！[A]from：：nat！[nat]drop4！两次，两次 ，N的尾N：来自N个数据nat = z j natplus：：nat！nat！ nattimes：：nat！nat！ Nat加上z Y！ Y乘以Z Y！ z加上（X）Y！（加上X Y）乘以（加上（乘以X Y）Xtake：：nat！【A】！[A]（//）：：A！A！ 一拿着Z X！X//Y！Xtake（N）[]！X//Y！Y取（N）（X：Xs）！ X：取N个X数据人= john j mary j peter j paul j sally j molly j rose j tom j bob j lisa jalan j dolly j jim j alice父母：：人！（person，person）父母彼得！（约翰，玛丽）父母艾伦 ！（保罗，玫瑰）父母丽莎！（彼得，莫莉）祖先：：人！人祖先X！Y//Z//祖先Y//祖先Z其中（Y，Z）父母X% data bool = true j false相关：人！ 人！ boolXY相关 true<=祖先X ==祖先Y列表和布尔值类型的数据声明仅作为注释包含在内，因为这些类型在TOY中是预先定义的。注意，列表构造函数被标记为[]和：（一个in x运算符），如Haskell [24]中所示。从它们的名称和定义中可以清楚地看出函数的预期含义。每个函数的arity总是与其规则中的形式参数的数量相同。特别地，drop4（一个删除给定列表前四个元素的函数）的arity为0，不管它的类型如何。最后两个函数说明了可连接性条件和局部定义父母保罗！（约翰，玛丽）父母dolly！（保罗，玫瑰）父母Sally！（约翰，玛丽）父母吉姆！（汤姆，莎莉）121的使用。此外，函数ancestor和（//）是不确定的，因为使用固定参数调用它们可以返回多个结果。例如，祖先alan可以返回任何结果paul、rose、john或mary。122本例中的某些程序规则不正确。相应功能的预期含义。更确切地说，时间的第二个规则和形式的单一规则是错误的;它们的正确版本应该是：times（X）Y！加上（乘以X Y）Y从N！N：从（N）在下一节中，我们将给出“预期意义”的形式化定义，这是证明有关声明式调试正确性的数学结果所必需的2.2.3良好类型的目标一个类型良好的目标G与一个类型良好的条件具有相同的形式特别是，它必须满足第2.2.1节中解释的可受理性要求，但现在w.r.t.空的变量集。FLP系统被期望解决目标，返回替换作为计算的答案。对于2.2.1节中的简单程序，可以用T OY系统计算的目标和答案的一些例子是：(i) 目标相关alan X == true的计算结果为fX7！aliceg（除其他外）。(ii) 目标take（（z））（from X）== Xs有一个计算的答案，即fXs 7！X：X：[]g，这是错误的w.r.t.。该计划的预期意义。(iii) 目标head（tail（map（times N）（from X）== Y要求包含N与从X开始的连续自然数的乘积的列表中的第二个元素。由TOY计算的前两个解是fN7！z，Y 7！zg（这是正确的）和fN7！快，Y 7！zg（这是错误的）。这是因为有缺陷的函数times导致表达式（times（z））总是返回结果z。有效的解决方案fN7！快，Y 7！用户所期望的Xg实际上是一个缺失的答案。诊断缺失的答案超出了本文的范围。2.3程序语义2.3.1语义演算SC在[9]中，一个重写演算被称为CRAMC被用来从一个给定的程序P中推导出那些根据P的语义应该被认为是有效的近似和可连接性语句。非正式地，近似陈述e！t的意思是t 2 P在？表示一个部分定义的值，它近似于e2Exp的值。;而可接合性y声明te == e 0意味着e！t，e0！ 对于总的t 2 P成立。在本文中，我们将使用语义演算SC，一个变种的语义演算C，这是第一次提出在[2]中，为了定义一个逻辑上正确的框架，说明性调试错误的答案在懒惰的FLP语言。形式上，SC由以下推理规则组成：123e 1！t 1“嗯！ t m嗨！ht me 1！ t 1：e n！ t nf t n！ss ak！ 不Cr！ SBTe！？RRX！ X与X 2 V ar直流h t m2 P在？Jne ==e0t2P at（总模式）Cr！ SAR+FA（ftn！ r（C）2[P]？;fe n a k！ tt ？在所有的SC规则中，e; e i 2 Exp？是部分表达式，t i; t;s 2 P at？是部分模式和h2DC[FS.符号[P]？ 在规则AR+F中，A代表集合f（l！ r（C）j（l！ r（C）2P;2Subst？g的部分实例的规则从P。不 同 推 理 规 则 的 标 号 具 有 以 下 含 义 ： BT 表 示 Bottom ， RR 表 示Reexivity，DC表示Decomposition，JN表示Joinability，AR + FA表示argument reduction + function application。注意AR+FA是唯一依赖于给定程序的SC规则。它必须被理解为两个推理步骤的连续应用，其单独的规范如下所示：AR f2FSnfe n a k！ tt 6=？FAn！S（ftn！ r（C）2[P]？规则AR+FA将为计算部分模式t而执行的步骤形式化为函数应用fen ak的近似值，即：(i) 计算适当的部分模式ti作为参数表达式ei的近似值。(ii) 应用程序规则实例（ftn！ r（C）2[P]？，验证条件C，并计算适当的部分模式s作为右侧r的近似值。(iii) 计算t作为s ak的近似值。这里使用部分模式允许用严格语义的语法简单性来指定非严格语义在 k > 0的情况下，f必须是返回函数值的高阶函数，由模式s表示。在k = 0的情况下，规则AR + FA可以通过取f t n来简化！ t作为FA步骤的结论，并省略前提s a k！t.我们将在整个论文中隐含地假设这种简化。e！ 0！不e 1！ t 1：en！ t nsak！不Ftn ！S124请注意，SC不能独立地应用两个推理规则AR和FA然而，在给定的SC证明中考虑FA步骤是有帮助的，因为只有这些步骤依赖于程序规则。此外，FA步骤的结论是特别简单的近似语句的形式f t n！ s（其中t i; s 2 P在？），这将被称为基本事实，在其余的文件。基本事实和局部定义都是近似陈述，但它们用于不同的目的。一个基本的事实ft n！s断言（可能是非线性的）部分模式s近似于f t n的结果，f t n是一个调用函数调用，其参数的确切数量是f的arity所期望的，并且参数ti2 P在？其表示计算S作为结果所需的F的实际参数的 部 分 近 似 。SC中的其他推理规则更容易理解。在下文中，我们使用符号P“SC”来表示语句“可以使用SC推理规则从程序P中推导出来。例如，取2.2.2节中的简单程序P，可以得到以下SC推导：(i) P`SC来自X！X：？.（二）P `SC 从X！X：X：？.（三）P `SC 父母爱丽丝！（汤姆，萨利）。（四）P `SC 艾伦先祖！John.（五）P `SC 艾伦先祖！玛丽.（vi）P `SC 爱丽丝祖先！John.㈦ P `SC 爱丽丝祖先！玛丽.(viii) P`SC祖先艾伦==祖先爱丽丝。这些例子表明，近似语句的语义与它们在程序中用作局部定义是一致的，但与相等的含义不同。例如，X！X：？只意味着部分值X：？近似于（from X）的值，而不是（from X）的值等于X：？。有一个正式的关系之间的approxima- tion报表和近似排序在P？在第节中定义2.1.2. SC的这一特性和其他基本特性在下面的介绍中说明结果，这可以证明由直接归纳的结构上的SC证明4。命题2.1对于任何给定的程序P：(i) 对于所有的t; s 2 P在？：P `SCt！si t w s.4 一阶规划的一个类似结果的证明可以在[8]中找到。125suc （take（（z）） （（fr （om （X）h！hXh：X：[]（（hhhhhh（（AR+FA（z）！（来自X！X：X：？DCSAR+FAX！XX：take（z）（X：？）！X：X：[]RRDCSSX：来自X！X：X：？X！ X take（suc（z）（（X（：？）！X：[]DCS（RR（S（（AR+FASX！X来自X！X：？快！ 拉斯X：？ ！X：？RRAR+FSASDC，RR，BTDCX！XX：取Z？ ！X：[]DCSRRSX：来自X！X：？X！ X带Z？ ！[客户端]SRRSDCSAR+ FASX！Xx X！什么？z！ z？！？带Z？！RRBTDCBT【】！[客户端][客户端]126DC图1：语义演算SC(ii) 对于所有的E2 Exp？，t; s 2 P at？：如果P `SCe！t和t w s，然后还有P 'SCe！S.(iii) F或a lle2Exp？，t2Pat？ 和;02Subst？ 这样P`SCE！ t和v0，一个也有P`SCe 0！ t具有相同大小和结构的SCp ro。(iv) 对于所有的E2 Exp？，s 2 P在？这样P `SCe！s，一个也有P`SCE！s对于任何总替换2 Subst.2.3.2证明树见证计算答案我们已经在2.2.3节中介绍了计算答案的概念，假设存在某个目标求解系统。从现在开始，在本文的其余部分，我们还将假设目标求解系统是合理的w.r.t. 语义演算SC。更确切地说，我们假设P`SC G对于由目标求解系统使用程序P计算为G的答案的每个替换都成立。注意，在SC证明G之前，必须认为是预先给定的。按照惯例，记法P`SC G意味着P`SC'对G中的每个原子语句都成立给定一个原子目标G，证明P`SC G的特定SC演绎总是可以使用证明树（briey PT）来表示，该证明树具有附加到其节点的原子语句，使得G被附加到根节点，并且每个节点处的语句可以通过一些SC推理规则从附加到其子节点的语句中推断出来。在G不是原子的情况下，证明P`SC G的每个特定的SC演绎可以由对应于G中的单个原子陈述的不同演绎P`SC'的证明树族来表示。通过语言的轻微滥用，我们也将在这种情况下谈论证明树采取（（ （z））（X ！X：]从X ！ X：X：采取（z）的（X ！X：]127不采取（(sucz））（从mXX）！X：X：[]XxxXXX取z？！[客户端]图2：对应于图1正如我们已经提到的，= fXs 7！X：X：[]g是目标G = take（（z））（from X）== Xs w.r.t.的计算结果。 简单程序P形成2.2.2节。任何P`SCG的证明必须包括P` SCtake（（z））（从X）的扣除！X：X：[]，这由图中显示的PT证明。1.一、请注意，作为FA步骤结论出现的基本事实通过在框内显示而突出显示。2.3.3简化证明树正如我们将在下一节中解释的那样，我们的目标是使用证明树作为声明式调试的计算树。为此目的，唯一相关的节点是那些对应于FA步骤的结论的节点。 这是因为SC中的所有其他推理规则都是独立于程序的，不正确的步骤。出于这个原因，我们将任何给定的证明树关联到一个简化的证明树（brie y APT），通过删除所有这些节点来获得除了词根之外，PT不是FA推理的结论。更准确地说，对应于给定PT的APT构造如下：APT的根是给定PT的根。对于已经放置在APT中的任何节点，其子节点是PT中的对应节点的最接近的后代，其表示非平凡FA步骤的结论。一步一步，结论是ftn！ s被认为是非平凡的is6=？.注意，也可以忽略不重要的FA步骤，因为它们的结论是总是形式为f n的平凡有效的事实！ ？在每个APT中，每个节点都隐式地关联到由相应的FA步骤使用的程序规则实例，其结论恰好是基本事实ft n！s在节点处。注意t 1;：; t n; s是部分模式，不能包含任何可约函数调用。作为具体示例，图2示出了从图1中的PT获得的APT。1.一、2.3.4预期型号[6，13]中使用的逻辑程序的预期模型可以表示为属于程序的Herbrand基的原子公式集。开放的Herbrand宇宙（即具有变量的项的集合）产生更从X ！ X：X：？采取（（ （z））（X：X：？）！X：X：[]从X ！X：？采取（z）的（X：？）！X：[]128不不不信息语义学[5]。 在我们的FLP设置，一个自然的类似于开放Herbrand宇宙是集P在？的所有部分模式，配备了近似排序v。同样，一个自然的类似开放Herbrand基地是收集的所有基本事实f吨n！S. 因此，我们可以将Herbrand解释定义为满足以下三个要求的基本事实的集合I，对于所有f2FS n和任意部分模式t; tn：(i) （f t n！？）2一.(ii) 如果（f！s）2I，tvt0; sws0thenalso（ft0！ s0）2I.n ii n(iii) 如果（f t n！s）2 I，且是全置换，则（f n！s）2 I.Herbrand解释的这个定义比[9 ]中的定义简单，[9]中提出了一个更一般的解释概念（以代数的这种简单表述的代价是将非Herbrand解释排除在我们的考虑之外。在我们的调试方案中，我们将假设程序的预期模型是Herbrand解释I。她的品牌解释可以通过集合包含来排序一个逻辑上正确的程序P应该符合它的预期解释I。为了使这个概念形式化，我们需要一些定义。首先，我们说给定的近似或可合并性陈述“在Herbrand解释I i中有效"可以在由SC规则BT、RR、DC和JN以及下面的推理规则FA I组成的演算SC I中证明：FAIfent模式，t6=？; s模式国王！ t（f t n！s）2 I例如，假设第2.2.2节中简单程序的自然预期模型I，以下语句在I中有效：(i) 从X！X：你X：？(ii) 取（（z））（从X）！X：X：[](iii) 祖先艾伦（英语：Ancient Alan）这些声明的第一个甚至属于我。总的来说，对于每一个基本的事实f t n！s，可以证明f t n！ s在I i（f n！s）2 I.接下来，我们定义表达式的表示和给定程序的模型的概念：e的表示是集合[[e]]I=fs2Pat？ j e！ S在Ig中有效。I是P（Ij = P）i的模型，P中的所有程序规则在I中都有效.程序规则l！ r（C）在I（I j= l！ r（C）i对于任何替换2 Subst？，我满足规则实例l！ r（C.我满足一个规则实例l 0！r 0（C 0i要么I不满足C 0要么[[l0]]I[[r0]]I.一e 1！t 1：en！ t nsk！不一129不I满足一个假设条件C 0='1; ：'ki，对于i=1：k，I满足'i。我满意了！ s02C 0，i [[d0]]I[[s0]]I. 可以证明[[d0]]I[[s0]]I是02[[d0]]I。I满足l0==r02C 0，i[[l0]]I\[[r0]]I\Pat6=;。程序和模型之间的基本关系在下面的结果中陈述，该结果在[9]中对于比Herbrand模型更一般的模型概念被证明。本公式的证明见附录A。定理2.2设P是一个程序，且P是任意逼近或可合并性语句。然后又道：(a) 如果P的SC在P的任何Herbrand模型中成立。(b) M P= ffn！s j P`SCft n！sg是P的最小Herbrand模型w.r.t. 包含排序。(c) 如果'在MP中有效，则P`SC'.把前面的定理和目标求解系统w.r.t.的假设可靠性放在一起。SC，我们立即获得：命题2.3假设一个程序P和一个目标G的计算结果，使得G在Herbrand解释I中无效。那么，在P中一定有一些程序规则在I中无效。这个命题预测存在至少一个错误的程序规则时，观察到一个错误的计算答案。在这里，错误必须被理解为在预期模型中无效的精确意义。在我们的简单程序P的情况下，= fXs 7！X：X：[]g是目标G = take（（z））（from X）== Xs的错误计算结果，因为G在预期模型中无效。根据命题2.3，P中的某个错误规则必须对错误答案负责。事实上，定义函数的程序规则是错误的。每当程序规则l！r（C）在预期的模型I中是无效的，必须有一些替换2Subst？ suc h规则实例l！r（C）不满足I，这意味着(i) '在I中对所有'2 C都有效。(ii) r！在我的一些s2pat中s是有效的？ suc hthat（l！ s）2=I.在我们的例子中，规则的错误实例是规则本身。”[10]“从，从。尼：尼：？在I中是有效的，但是（来自N！尼：尼：？）2=I. 这对应于上述第（ii）项，其中N：N：？作为S。为了实际调试的目的，命题2.3必须被重新定义，以产生一种有效的方法，该方法可用于从观察到错误的计算结果开始，发现程序规则的不正确实例。130在下一节中，我们将展示这可以通过使用声明式调试方案来实现，其中APT充当计算树。在本文的其余部分，有效的方法来实现这种方法进行了研究2.4声明性的2.4.1一个泛型声明式数据库方案[19]中提出的调试方案假设任何终止的计算都可以表示为一棵nite树，称为计算树（brie y CT）。该树的根对应于主计算的结果，并且每个节点对应于一些中间子计算的结果。此外，假设每个节点处的结果由子节点的结果确定。因此，每个节点都可以被视为单个计算步骤的结果。调试器通过遍历给定的CT（所谓的CT导航）来工作，寻找错误的节点。不同种类的编程范例和/或错误需要不同类型的树，以及不同的错误概念。一个好的调试器应该只报告真正对应于错误计算步骤的错误。这种考虑导致忽略具有一些错误子节点的错误节点，因为它们不一定对应于错误的计算步骤。按照[19]的术语，没有错误子节点的错误节点称为有缺陷节点。为了避免不可靠，调试方案只寻找有缺陷的节点，向oracle（通常是用户）询问问题，以确定哪些节点是错误的。下面的简单结果在[19]中得到了证明：命题2.4一个nite计算树有一个错误的节点i它有一个buggy节点。特别地，根节点错误的nite计算树具有一些有缺陷的节点。这为调试方案提供了一个“弱”的完整性概念，在实践中是令人满意的。通常，实际的调试器只在根错误的计算树中查找最顶层的有错误的节点。通过反复应用调试器可以发现多个错误。2.4.2使用APT进行验证在逻辑上正确我们的调试系统是基于刚才重新调用的声明式调试方案. 我们假设良好类型的FLP程序和目标，如第2.2. 我们还假设每个程序都有一个预期模型，表示为一组基本事实，如2.3.4节所述。计算是由一个目标解决系统，必须是健全的w.r.t.第2.3.1节中的语义演算SC。当一个计算用程序P得到一个目标G的答案替换时，我们假设证明P`SC G的APT被用作计算树。APT节点被认为是错误的，131附加到它的声明（这总是一个基本事实，除了根）在预期的模型中是无效的下一个定理保证了使用APT的声明式调试的逻辑正确性：定理2.5假设用程序P为目标G计算出一个错误的计算结果，使得G在预期模型中无效。考虑任何证明P`SC G的APT，由于目标求解系统w.r.t.的可靠性，它必须存在。然后，使用APT作为计算树的声明性调试具有以下两个属性：(a) 完整性：导航APT将 发送一个有缺陷的节点。(b) 合理性：APT中的每个有缺陷的节点都指向一个程序规则的实例，该程序规则是不正确的。预定的模型。证据第（a）项直接从命题2.4中得出，前提是用于导航树的搜索策略不会错过现有的错误节点。 为了证明（b）项，假设预期模型是I，APT是apt，并且已经被缩写以获得apt的PT是pt。现在考虑apt中任何给定的有错误的节点pt中对应的节点必须包含基本事实f t n！s，其在I中无效并且已经被推断为使用程序规则的某个实例的FA推断步骤的结论，say（ftn！ r（C）2[P]？. 因此，ft n的孩子们！pt中的s对应于语句r！s和C中的所有语句。在apt中，f t n的孩子们！ s不一定是这些;但是由于apt已经被构建为pt的缩写形式，所以碰巧r！s和C可以从f t n的子元素推导出来！s在apt通过SC推论是从FA不同的，因此正确的每Herbrand解释。而 且 ，f t n的所有孩子！apt中的s在I中有效，因为它们是有缺陷节点的子节点。由此我们可以得出结论，C和r！s在I中有效，而ft n！s不是;这意味着程序规则实例（ftn！ r（C）2[P]？在I中是不正确的。2这个定理提供了命题2.3的一个有效版本，以及计算树的一个逻辑解释。据我们所知，这是在其他相关的方法中缺失的，用于惰性FP和FLP程序的声明式调试[21，22，23，27，18，20，25]。作为具体示例，再次考虑图1所示的PT和图2所示的相应APT。正如我们之前所说，PT见证了错误答案= fXs 7的X：X：[