函数式逻辑程序的声明式编译及调试方法研究

理论计算机科学电子笔记57（2001）网址：http://www.elsevier.nl/locate/entcs/volume57.html24页函数式逻辑程序的声明式编译1M. 阿尔蓬特2Departamento de Sistemas Informaticos y Computacion-DSIC瓦伦西亚Camino de Vera s/n，46022 Valencia，西班牙F. J. 科雷亚3信息和系统部{DISUniversity EAFIT，Carrera 49 7 Sur 50，3300 Medell n，Colombia.M. Falaschi4Dipartimento di Matematica e Informatica Universityof Udine，Via delle Scienze 206，33100 Udine，Italy.摘要我们提出了一个通用的框架，声明式调试的功能逻辑程序，这是有效的渴望以及懒惰的程序。我们关联到我们的程序语义的基础上（连续）的直接后果运营商模型计算的答案。然后，我们表明，给定一个程序P的预期规格，它是可能的检查P的正确性由一个单一的步骤的直接后果算子。我们还提出了一种更有效的方法，这是基于抽象解释。通过近似成功集的预期规格，我们得到了一个nitely终止调试方法，它可以静态使用。我们的兄弟会是参数化的。成功集的近似值。我们提出一个具体的例子的近似。我们提供了一个实现我们的调试系统，实验表明，在广泛的基准测试，我们能够发现一些常见的错误，在用户程序。c 2001年由Elsevier Science B出版。V. CC BY-NC-ND许可下的开放访问。阿尔蓬特、科雷亚和法拉斯基21引言声明式编程得到函数式和逻辑式编程的支持. 然而，这些编程风格中的每一种都有不同的优点w.r.t.实际应用等函数式语言为将I/O集成到声明式编程中以及高效的程序执行提供了复杂的抽象工具、模块系统和干净的解决方案。逻辑语言允许使用部分信息进行计算，并提供内置的搜索工具，这些工具在基于知识的系统和运筹学中有很强的应用。然而，最近的研究结果表明，这些风格的优点可以有效地结合到一种语言中。现代函数逻辑语言具有这两种风格的特点。集成语言的操作语义通常是基于窄化的，窄化是参数传递的统一和归约作为求值机制的组合，归约包括重写和SLD解析。本质上，narrowing包括目标变量的实例化，然后是对实例化目标的缩减步骤。缩小在函数编程（范式计算）和逻辑编程（答案计算）的意义上是完全的。由于无限制窄翼的巨大搜索空间，已经提出了稳步改进的策略（参见[29]的调查）。如何调试函数逻辑程序是一个重要的实际问题，在以前的文献中几乎没有解决。只有少数函数逻辑语言配备了调试工具（例如ALF[28]， Babel[39]和Curry[31]）。然而，这些调试器由基于适当的扩展框模型的跟踪器组成，这些扩展框模型有助于显示执行[30，5]。由于（函数式）逻辑程序操作语义的复杂性，通过跟踪执行所获得的信息难以理解。函数逻辑编程语言NUE-Prolog被赋予了一个声明式调试器[40]，它以Shapiro [43]提出的风格工作，也就是说，预言机（通常是用户）应该赋予调试器错误症状，以及正确回答由证明树驱动的预言机在[36]中提出了一个类似的用于函数逻辑语言调试器的声明式调试器。在[41]的基于证明树的一般方案之后，[12]中给出了用于惰性函数逻辑语言的错误答案的声明式调试的程序[12]中的方法包括计算树的形式化，其足够精确以证明逻辑正确性这也有助于简化Oracle问题。在纯逻辑编程的情况下，[17]已经定义了一个声明式框架，1 这项工作得到了CICYT（拨款TIC 2001 -2705-C 03 -01）、Accion Integrada Hispano-Italiana HI 2000 -0161和Generalitat Valenciana（拨款GV 01 -424）的部分支持。2 电子邮件地址：alpuente@dsic.upv.es3 电子邮件地址：fcorrea@eafit.edu.co4 电子邮件地址：falaschi@dimi.uniud.it阿尔蓬特、科雷亚和法拉斯基3RRR用于调试的扩展[25，43]中的方法到诊断的w.r.t.计算答案该框架不需要预先确定症状，并且是目标独立的（它由一组最一般的原子目标驱动）。它基于使用直接结果算子TP来识别程序错误，并且具有给出症状独立诊断方法的优点[17，16]。在本文中，贡献之一是开发一个声明性的诊断方法w.r.t.计算答案，将[17]的思想推广到功能逻辑程序的诊断。我们对我们考虑的程序施加的条件允许我们定义一个声明式调试的框架我们将一个（连续的）直接后果算子与我们的程序相关联。然后，我们表明，给定一个程序R的预期speci阳离子I，我们可以检查R的正确性，通过一个单一的步骤，这个操作。 我们通过例子来说明这一点。 我们讨论使用我们的工作，自下而上以及自上而下的抽象调试混合功能逻辑代码。我们还提出了一种新颖的，有效的方法，这是基于抽象的解释。我们通过近似成功集的预期规格来进行。遵循[17，16，11]中的启发思想，我们使用上和下规范I+和I来正确地过-（分别）。under-）近似于预期的语义。然后，我们将这两个集合分别用于前提中的函数和直接后果算子的后果，并通过简单的静态测试，我们可以确定某些子句是否是错误的。1.1 文件计划本文的其余部分组织如下。第二节简要介绍了一些初步的定义和符号。第三节首先为函数逻辑程序R构造了一个新的遗传直接结果算子T'，它是参数的。 缩小策略可以是急切的，也可以是懒惰的。然后，我们定义了一个基于T '的xpoint语义，它正确地模拟了通过使用narrowing 策 略 的 narr o w er 计 算 的答案。 在渴望策略的情况下，引入注意变换就足够了，它消除了嵌套调用，并允许目标通过标准统一在语义中运行。然而，懒惰策略更复杂，我们需要在T '的定义中引入两种类型的等式：严格等式，它对数据项上的等式进行建模，以及非{严格=}，即使参数都是未定义或部分定义的，也仍然成立，类似于[27]。 并对一个语义O'（R）进 行 了 模 拟 ， 给 出 了与xpoint语义的对应关系。在第4节中，我们介绍了不正确和不可靠症状以及未覆盖呼叫的必要一般注意事项部分5 提供了一个抽象的语义，阿尔蓬特、科雷亚和法拉斯基4eB1方程组Eib）E. 设mgu（E）表示最基因单位，R的语义在第6节中，我们提出了我们的抽象诊断方法，并通过例子说明其使用。在第7节中，我们提出了一个实验评估的方法在一组基准。第8节总结并讨论了一些相关的工作。2预赛我们简要总结了重写系统[6，34]和函数逻辑编程的一些已知结果（广泛的调查见[29，33]）。在本文中，V将表示变量的可数集合， 表示一组函数符号或签名，每个符号都有一个固定的关联元。（[V]）和（）分别表示非基字（或项）代数和建立在[V]和[V]（）通常称为Herbrand论域（H），记为H。B表示Herbrand基，即可以用H的元素建立的所有基础方程的集合方程s = t是一对项s; t2（[ V]）.术语通常被看作是有标签的树。立场是代表-由表示项中的访问路径的自然数序列来表示，哪里表示空序列。O（t）表示不变量的一个术语t的位置。tju是t的位置u处的子项。 t[r] u是项t，其中位置u处的子项被r替换。这些概念以自然的方式扩展到方程序列。例如，方程序列g的不可变位置集（e1;：：; en）可以定义为如下：O（g）=fi：uju2O（e i）;i = 1;：; ng。我们用V ar（s）表示出现在句法宾语s中的变量集合，而[s]表示s的基础实例集合。一个新的变量是一个在其他地方都没有出现的变量。符号表示符号的一个nite序列。语法对象的同一性由表示。令Eqn表示可能存在的多项方程的数量集合[14]。 如果E0在逻辑上蕴涵E，则我们写E0. 这个等式是一个由下元素为真和上元素为假排序的格。把方程的元素看作是方程的（量化的）合取，并作模逻辑等价处理.如果方程组是错误的或者它具有形式9 y 1：9 y m：fx 1= t 1;：;xn=t ng，则方程组被求解，其中每个xi是不出现在任何项ti中的不同变量，并且每个y i发生在某个t j中。任何一组方程E都可以转换成一个等价的方程solve（E），求解它。 我们将我们的兴趣限制在（[ V]）上的幂等替换集，它由Sub表示。 空的替换表示为。在替换=fx1=t1; ：;xn=tng和不定 方程组 =fx1=t1;：;xn=tng之 间 存在 自 然 同 构 。Asubstitution=fx1=t1; ：;xn=tngisaunierofan不等式方程组E.我们写m gu（fs1=t1; ：;sn=tn g;fs0=t0; ：;s0=t0g）表示方程组的最一般单位，1n n阿尔蓬特、科雷亚和法拉斯基5RRfs1=s0;t1=t0; ：;sn=s0;tn=t0g. 我们写js来表示限制R1 1n n的取代到语法对象s中的变量集合。条件项重写系统（简称CTRS）是一个对（; R），其中R是 形式的简化（或重写）规则方案的集合（ ！（C），、2（[V]），62 V和V ar（）var（）. 条件C是一个（可能是空的）方程序列e 1;：：：e n，n 0，当我们方便的时候，我们把它作为一个集合（合取）来处理。 C中不出现的变量叫做额外变量。我们经常会写一些R而不是（; R）。如果重写规则没有条件，我们就写！. F或CTRSR，r<作为形式为true;：; true的序列的通用表示法。一个成功的推导（或反驳）g在R+是一个narro-机翼导数g>，其中jV ar（g）是计算的答案替换（cas）。缩窄机制是构造方程理论完备E-uniation算法的有力工具。在这种情况下，完整性意味着，对于给定方程组的每个解，可以通过缩小找到更一般的解形式上，如果缩窄算法生成至少与满足查询的任何解一样一般的解（它生成完整的E-uniers集合），则该缩窄算法对于（一类）CTRS是完整的。1阿尔蓬特、科雷亚和法拉斯基72.2完整的缩小策略由于无限制的缩小有相当大的搜索空间，已经开发了几种缩小策略（或位置约束）是任何定义良好的标准，通过允许缩小以仅减少某些选定的位置来获得较小的搜索空间 一个窄化策略可以被形式化为一个映射，该映射将O（g）的一个子集（g）分配给每个目标g（不同于>），使得对于所有的u2'（g），目标g在位置u处是可窄化的。收缩策略“的一个重要属性是完整性，这意味着受”约束的收缩仍然是完整的。函数式编程中有一个继承的权衡，在正交、非终止规则的由外而内求值的好处和终止、非正交规则的内部或渴望求值的好处之间。关于缩窄策略完整性的结果调查可以在[4，21，22，29]中找到。 为了简化我们的符号，我们让IR'表示满足叙述策略的完备性条件的CTRS'的类。我们让客栈（g）（resp.out（g））表示窄化策略，该窄化策略分配最左边-最里面（resp.最左-最外）将g的redex缩小到目标g。 6我们用策略“，”2finn;out g，“作为最小关系，”来制定一个条件狭窄，满足u='（g）^（！（C）R'+^=mgu（fgju=g）g;'（C;g[]u）F或“2fin;outg，R”+=R [fEq“ g，其中Eq”是模型的规则数据项的平等性：c='c！测试结果%c=02Cc （ x1; ： ;xn ） ='c （ y1; ： ;yn ） ！ （ x1='y1 ） ^ ： ^（xn='yn）%c=n2C这里='是当ver'=inn时项的标准等式y=， 而对于当'被删除，并且考虑到非终止规则时，我们需要区分标准（非严格）相等=和严格相等=，标准相等=是在部分确定的或在nite数据结构中定义的，严格相等=是仅在nite和完全确定的数据结构中定义的，并且严格相等给予相等nite对象的同一性的弱含义（例如， 见[39]）。我们还假设，当我们考虑' = inn时，g和C中的方程具有s = t的形式，而当我们考虑' = out时，方程具有s t的形式。请注意，当'= out时，像f（a）= g（a）这样的非严格方程不是可接受的目标。6 最里面的项是应用于构造器项的操作，即，形式为f（d1; ：;dk）的项，其中f2F且对于所有i=1; ：;k，di2（C[V]）。g的最左-最内位置是指g的最左位置指向最内的子项。一个位置p是位置集合O中的最左最外位置，如果没有p0 2O，p0p的前x，或p0 =q：i：q0 p=q：j：q00 和i的'R1nn+11n'n+1;“其中f=n2 D，xn+1和xi是不同的变量，其中i= 1;：;n g。操作语义和最小x点语义之间的等价性由以下定理建立。定理3.10若R2IRinn，则Oca（R）=Fca（R）.出去下面的定理将非基语义Oca（R）与标准最小Herbrand E-模型语义M（R）。定理3.11设R是IR '中的p rgam，r是关系r在替换下的反对称闭包（f-替换性质）.则M（R）= [Oca（R）]。4声明性程序现在我们介绍一些关于陈述性程序诊断的基本定义[17]。作为操作语义，我们考虑计算答案阿尔蓬特、科雷亚和法拉斯基13'''''FRGR替代品定义4.1设I为R的预期计算答案语义的规范。(i) R是部分正确的w.r.t. I，if Oca（R）I.(ii) R是完全的W. R. T。 I，ifI O ca（R）.(iii) R是完全正确的。 I，如果Oca（R）= I.如果一个程序包含错误，这些都是由相应的sym- ptoms信号。定义4.2设I为R的预期计算答案语义的规范。(i) 一个不正确的征兆是一个方程e，使得e 2 Oca（R）和e 62 I.(ii) 一个不完全性征兆是一个方程e使得e2i和e62Oca（R）.在错误的情况下，为了确定错误的规则，我们给出以下定义。定义4.3让I成为预期xpoint语义对R. 如果存在一个方程e2T '（I）和e62I，则规则r2 R不正确的是e。因此，规则r的不正确性通过意图语义I的简单变换来表示定义4.4设I为R的预期xpoint语义的规范。 如果e2I和e62T'（I），则方程e是不成立的.通过上述定义，如果方程e不能通过使用预期的xpoint语义的任何程序规则导出，则方程e未被覆盖。命题4.5如果在R中没有不正确的规则关于预期的xpoint语义的规范，那么R是部分正确的。预期的计算答案语义。我们现在考虑一个严格语言的自底向上的抽象调试器因此，在本文的其余部分，我们x'= inn。5抽象成功集抽象解释理论[18]为高级数据流分析工具提供了一个形式化的框架抽象解释形式化了“近似计算”的概念，其中计算是用数据的描述而不是用数据本身来进行的然后，语义操作符被替换为抽象操作符，这些抽象操作符被证明是“安全地”接近标准操作符。在本节中，从xpoint语义阿尔蓬特、科雷亚和法拉斯基14RVVf（s0; ：;s0） f（s1; ：;sn）：在第三节中，我们提出了一种抽象语义，它近似于程序的可观察行为，并且适合于模块化数据流分析，如方程组的不满意能力分析或任何基于程序成功集的分析。我们假定[2]中定义的方程不满意能力分析的抽象解释框架。另一种构造抽象项重写系统的方法在[9]中给出. 我们认为给出的xpoint语义的另一种近似与我们在本节中描述的不同，可以通过遵循与[9]中类似的方法来表征。我们首先回忆一下抽象域和相关的抽象算子。然后，我们描述了一个新的抽象直接后果算子T]这能够近似运算符TR和抽象xpoint语义F]（R）。在下文中，我们用O]表示具体对象O的抽象类比。5.1抽象域与算子一个描述是一个抽象域（D;）（一个偏序集）与一个具体域（E;）（一个偏序集）的关联。 当E = Eqn或E = Sub时，该描述分别被称为等式描述或替换描述。抽象域和具体域之间的对应关系是通过“具体化”函数建立的D！2大肠 我们说d近似于e，写作d/ e，即e2（d）。近似关系可以像往常一样提升到关系和叉积[2]。抽象替换的目的是描述一个给定的目标的计算答案替换。在我们的方法中，抽象方程和抽象替换分别对应于抽象程序定义和抽象可观察属性。方程和替换的域如下。定义5.1（抽象Herbrand宇宙）设]是一个不可约对称，bol，where ] 62. 令H] =（（[V[f]g）;）b项的定义域，被]增广的签名，其中偏序定义如下：(a)8t 2 H]：]t和tt和（b）8s1; ： ：;s;s0; ： ：;s02H];8f=n2。s0s^：^s0s）n1nV11nn1N这个顺序可以扩展到方程：s0=t0s=tis0s和t0t，以及方程组S;S0：1) S0Si8e02S0：9e2S使得e0e. 请注意，S0ft rueg）S0ft rue g。2) S0vSi（S0S）和（SS0蕴涵S0S）.当然，S0vS意味着S0包含的信息比S少，或者如果它们具有相同的信息，则S0使用更少的元素来表达它。阿尔蓬特、科雷亚和法拉斯基15BbVVVR1n1n粗略地说，在抽象域中引入的特殊符号]表示任何具体项。从编程的角度来看，符号]的行为类似于Prolog中的“匿名”变量。从逻辑的观点来看，]代表一个存在的量化变量[2，37，38]。定义[[S]]=S0，其中S中的n元组的同时数被替换为S 0中的n元组的现有量化的新鲜变量。定义5.2nabst ractsubstitution是一个形式为fx1=t1; ：;xn=tng的集合，其中，对于每个i = 1;：; n，x i是V中的一个不同变量，不出现在任何项t1;：; t n和t i 2（[V [f]g）中。逻辑蕴涵给出了ab-替换的排序：let ;2 Sub]，i[[ ]]）[[]]。术语、替换和等式的描述如下。定义5.3让HVint n =（n）;）和H] =（（[V[f] g）;）.术语描述是hH]; ; Hi其中：H] ！2HV 定义如下：（t0）=ft2HVj t0t g.设Eqn是（[V]）上的nite方程组的集合，Eqn]是（[V[f]g）上的nite方 程 组 的 集 合 。 方 程 描 述 为 h （ Eqn];v ） ;; （ Eqn; ） i ， 其中 e ：Eqn]！2Eqn定义为： （g0）=fg2且g是不定量的。设Sub为（[V]）上的置换集，Sub]为（[V[ f]g）上的置换集。替换描述h（Sub];）;;（Sub; ）i，在哪里：Sub]！2子定义为：（）=f2 SubjG.为了在抽象域上进行计算，我们必须定义抽象唯一性的概念。我们的方法的抽象的最一般的单位是非常简单的，粗略地说，它归结为计算一个方程组的解决形式与（可能）存在量化变量。我们将方程组S02Eqn]的抽象最一般单位定义如下。首先，用现有的量化的新变量替换S0中的]的所有事件。然后取所得到的量化方程组的解的形式，并最终再次用]替换存在的量化变量形式上：]令9y： y：S=so lve（[[S0]]）且=fy=]; ：; y=] g. 则mdgu（S0）=S。事实上，8 2 unif（[[S]]）：mgu]（S）这就是我们使用“最普遍”的原因。[2]中已经证明了抽象uniation算法的安全性我们的分析是基于一种简化（抽象）程序的形式，它总是终止，并在其中查询可以被高效地执行。我们的抽象程序的概念相对于循环检查是参数化的。在[2，3]中可以找到两个不同的实例。定义5.4循环检查是与程序R相关联的图GR，即由一组项对组成的关系，使得：(1) 传递闭包G+是可判定的，Æ(2) 设t =t0是一个函数，它赋予项t在GR中的某个nodet0。如果有一个在夜间序列：V阿尔蓬特、科雷亚和法拉斯基16R>>RRVVV8> x，如果x2Vsh（x;G）=h（G0;0i;h（ G1;1i;：然后9i0：hti; ti i 2 G+;其中ti = ejui; e 2 Gi且u 2O（e）： (we指ÆÆ到hti; ti i作为GR的“循环”。）通过简化每个子句的右侧和主体来抽象程序。这个定义是根据项和方程的结构归纳给出的。其主要思想是将GR中对应节点有圈的项用]替换，从而大大简化。 我们以迭代的方式使用这个定义。 我们首先抽象出一个具体的规则r，得到r]（如果有直接递归，我们选择一个规则;否则我们选择程序中的任何规则）。然后我们在R中用r]替换r，并重新计算循环{在继续抽象下一个规则之前检查。每个具体规则在抽象过程中只考虑一次。定义5.5（抽象规则）设R是一个程序，令r =（！（C）2 R.设GR是R的循环检查。我们定义r的抽象如下：r]=（！sh（;GR）（sh（C; GR））其中根据循环检查G的表达式x的壳sh（x; G）被归纳地定义公司简介联系我们f（sh（t 1; G）;：; sh（t k; G））ifxf（t1;：：;tk）和hx;xiG： ]否则我们现在可以形式化抽象语义。5.2自底向上抽象语义我们根据一个抽象的最小xpoint定义了一个抽象的xpoint语义。连续变换基于抽象统一和运算一个程序的抽象。其思想是提供程序R的具体表示的一个精确可计算的近似。在下文中，我们定义抽象变换T1。定义5.6（抽象Herbrand基，抽象Herbrand间）方程B的抽象Herbrand基被定义为集合抽象Herbrand宇宙H]上的方程。抽象Herbrand interpretation是2B]的任何元素。抽象行为解释的部分顺序可以用类似于解释顺序的方式来定义。我们可以证明抽象解释集是一个完备格w.r.t.]中。一个抽象的平凡方程是一个方程] = X，X = ]或] =]。定义5.7设R是一个程序，GR是R的一个循环检查，R]是使用GR的R的抽象，其中我们也去掉了任何抽象的平凡方程阿尔蓬特、科雷亚和法拉斯基17R'RRR RVR从规则的主体让我做一个抽象的解释。然后，T]（I）=R[= inn [fe 2 B]j（！（C）R];fl = rg[C0我的;mgu]（f lat（C）; C0）= ;mgu]（f=（rju）g）=;n =O（n）; n =（n = n [ ]n）G：[5.8 T]算子在完备格上是连续的抽象的解释。我们可以用类似于第3节中F '（R）和Fca（R）的具体构造的方法来定义F]（R）和Fca]（R）。定义5.9（抽象最小x点语义）程序R的抽象最小x点语义是[F]（R）= lfp（T]）. 设Fca]（R）= fl = r2F]（R）j r不包含任何定义的函数符号f=n 2 Dg下面的定理说明F]（R）和Fca]（R）是完全可算的.定理5.10存在唯一的正数k使得F]（R）= T]“k。从语义学的角度来看，给定程序R