理论计算机科学电子笔记246（2009）39-53www.elsevier.com/locate/entcs一种为惰性函数逻辑语言Bernd Braßel贝恩德·布拉塞尔1，2基尔大学计算机科学研究所40，24098 Kiel，Germany摘要本文基于最近开发的一种为惰性函数式编程语言构建调试工具的技术。使用这种技术，可以通过记录未求值表达式的信息来重放具有严格语义的懒惰程序的执行。记录的信息被称为神谕，并且非常紧凑。Oracle包含丢弃未求值的example之间的严格步骤数。该技术已经成功地用于构造懒惰函数式语言的调试器。本 文 扩 展 的 技 术 ， 包 括 懒 惰 的 功 能 逻 辑 语 言 。 使 用 该 技 术 构 建 的 调 试 工 具 可 以 在 www-ps.informatik.uni-kiel.de/ ~ bbr下载。关键词：惰性函数式语言，逻辑语言，调试工具1介绍经常有人说，现代函数（逻辑）语言的高级功能在试图发现错误时构成了障碍，参见。例如[14，17]。因此，近年来，已经开发了复杂的技术来支持程序员使用有用的工具来查找程序中的错误。最具启发性的技术通常被称为它也被应用于函数式编程，例如[15]，也被应用于函数式逻辑编程，最新的工作见[9]。然而，也有人认为声明式调试并不总是首选的工具，其他工具提供了互补的观点，参见。[10 ]第10段。因此，函数式语言最灵活的工具HAT [18]提供了几个视图，用户可以在其中任意切换这种灵活性的缺点是付出了严重的代价，1这项工作得到了德国研究委员会（DFG）的部分支持，基金编号为Ha 2457/5-2。2电子邮件地址：bbr@informatik.uni-kiel.de1571-0661 © 2009 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2009.07.01440B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39资源使用中的开销。每个HAT会话记录有关给定程序执行的兆字节数据，通常以数百计。投入到HAT中的大部分工作都与使大量数据在可接受的响应时间内可管理有关。由此产生的系统是高度优化的函数式编程的情况下，因此，不容易移植到更广泛的设置，如函数逻辑语言。在[6，5，3]中开发的相应尝试并没有导致具有令人满意的性能的工具的实现相反，我们在[4]中开发了一种不同的技术，使我们能够在短时间内构建一个快速稳定的调试系统。这项技术首先被开发来为懒惰的函数式语言构建调试器[8]。这项工作描述了扩展到更广泛的设置功能逻辑语言。在第2节中介绍扩展之前，我们将首先在第1.1节中描述基本思想。第3节介绍了基于该技术的函数逻辑语言Curry第4节结束。1.1使用Oracle进行最左最内求值在[3]的开发过程中进行了一个简单的观察：所有支持懒惰编程语言中调试的更复杂的方法都试图呈现有关程序执行的信息，就好像语义是渴望的一样换句话说，调试工具的工作是将复杂评估策略的各个方面倒回，并将其映射为简单的评估策略。现在的推理是这样的：如果这种从懒惰到渴望的映射是成功调试技术的核心，那么所有这些方法都可以从将给定的懒惰派生映射到渴望派生。然而，这种映射的信息在数量级上小于HAT等工具或[6]中开发的工具所需的信息它可以被压缩为对“丢弃步骤”之间的最左边最里面的步骤进行计数这些步骤丢弃了整个评估不需要的表达式例如，在以下程序的上下文中计算表达式（head（tail（from0）））from：：Int->[Int]fromn=n：from（n+1）head：：[a]-> ahead（x：_） = xtail：：[a] ->[a]tail（_：xs）=xshead（tail（from 0））=> head（tail（0：from（0+1）=> head（from（0+1））=> head（0+1：from（（0+1）+1）=> 0+1 => 1可以描述为：“最里面做三个步骤，然后丢弃接下来的两个最左边的最里面的表达式，再做两个更急切的步骤。” 简而言之，该信息可以被包含到急切步骤列表[3，0，2]中。 第一个数字减少，B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3941前导零意味着丢弃步骤。 然后可以将示例推导映射为到急切的评价：【三、零、二】head（tail（from 0））=>[2，0，2] head（tail（0：from（0+1）=>[1，0，2] head（tail（0：from 1））=>[0，0，2] head（tail（0：1：from（1+1）=>[0，2] head（tail（0：1：from_））=>[2] head（tail（0：1：_））=>[1] head（1：_）=>[0] 1在[4]中，我们已经形式化了一种自动记录和重放这些步骤信息的技术除了展示方法的可靠性之外，我们还能够证明计算Oracle信息所需资源的数量级的有趣属性在[8]中，我们提出了一种使用Oracle方法调试惰性函数程序的工具。本文讨论了函数逻辑语言的方法2函数逻辑程序设计本文的主要主题是如何将上述的oracle技术转移到更一般的函数逻辑编程环境中。我们可以确定扩展的三个主要主题(i) 由非确定性分支(ii) 自由变量结合收缩(iii) 自由变量与统一从这三个主题中，我们将只讨论前两个，统一留待以后的工作。在我们讨论我们的解决方案的细节之前，我们首先给出这两个主题的两个众所周知的首先介绍非确定性运算（？）在此基础上，将定义所有后续的非确定性操作。（？）接受两个参数并非确定性地返回其中一个（？）：：a -> a -> ax？ _ = x_？ y = y使用（？），我们可以定义一个操作，将给定的参数插入给定的列表中的任何位置。insert：： a -> [a] ->[a] insertx[]= [x]插入x（y：ys）=x：y：ys？y：插入xy注意到（？）具有非常低的优先级（实际上是Curry中最低的）。在插入的基础上，有一种表达方式来定义排列和置换42B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39sort，cf. [12 ]第10条。permute：：[a]->[a] permute[] =[]permute（x：xs） =insert x（permute xs）permSort：：[Int]->[Int]permSort l|排序置换=置换其中置换=置换lsorted：： [Int] ->Bool sorted[]=True sorted [x]= Truesorted（x：y：ys）|x< =y = sorted（y：ys）上面permSort的声明确实定义了一个排序操作，例如，呼叫（permSort [2，1，3]）计算结果为[1，2，3]，除此之外没有其他值。作为使用自由变量和收缩的一个例子，我们将使用列表头上函数的标准定义和布尔函数保护。这两个函数都只是部分定义，因此在应用它们时会出现guard：： Bool -> a ->a guard True x = x在下面的例子中，缩小范围的例子是（letxfree inguard（head x）1），对于一个新的变量y，它的值为1，x绑定到（True：y）。在介绍了两个运行的例子之后，我们现在开始研究函数逻辑编程中的两个一般概念，即生成器和计算。搜索树 应用这些概念的方法将导致甲骨文技术的扩展。2.1发电机在函数逻辑语言理论中有两个最近的发展，它们大大简化了将预言机技术扩展到这种设置的任务。 一自由变量与所谓的“生成器函数”一致的观察[2]和[11]中独立发现的。第二，函数逻辑程序的确定性和非确定性方面可以被整齐地分为：一方面是确定性的评估，另一方面是根据另一方面是一系列的选择。第二个想法在[7]中有详细描述。在将这两种想法应用于手头的案例之前，我们先用以下方面来说明它们：跑步的例子给定类型的生成器是一个非确定性地计算该类型的所有可能值。例如，布尔值的生成器很简单：genBool：： BoolB. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3943genBool = True？假对于具有无限值集的类型，我们必须对生成器的结构更加具体。右边的每个选项都应该引入一个类型的构造函数。构造函数的参数可以再次调用其他适当类型的生成器函数。 根据[2，定义3]和[11，定义3.3]，布尔值列表的生成器是：genBoolList：： [Bool]genBoolList =[]？genBool： genBoolList得到的函数有几个有趣的性质。除了最终每个可能的值都被生成的事实（比较[2，引理1]和[11，引理3.4]）之外，这样定义的生成器是生产性的，因为每个选择在有限个步骤中产生任意深度的头范式，同时只引入有限个非确定性分支。为了更符合Curry的类型系统，它允许多态函数和构造函数，我们稍微改变了上面的定义。 很容易看出[2，11]的主张仍然成立。type Generator a：：（）-> a genBool：：Generator Bool genBool_=True？假genList：： Generator a -> Generator [a]genList gen _=[]？genList genList（）由于调用时间的选择，带有人工参数（）的扩展是必要的。如果没有它，genList将生成只包含True或False的列表，但不包含，例如，[True，False].生成器和自由变量之间的联系可以用缩小的例子来说明 评估用生成器替换变量的表达式，即，（guard（head（genListgenBool（）1）也会使用表达式1仅在需要时计算，即计算到表达式（True：genListgenBool（））。不仅在语义方面，生成器和自由变量之间存在密切的对应关系，例如，结果是1。 但在操作上如[7]中所示，对应关系是紧密的。 无论我们在哪里，变量在收缩派生的替换部分中，我们在带有生成器的派生的表达式中找到一个未求值的2.2搜索树第二个重要的见解介绍了工作[7]。在那里，函数逻辑编程的操作机器被分成在所谓的搜索树上计算的决定性部分和从该树投射值的逻辑部分一般的想法是，所有类型τ都由两个新的构造器Fail：：τ（表示失败）和Or：：Ref ->τ->τ->扩展τ表示非确定性分支。使用Ref类型的引用44B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39通过如下所述的预测来识别关于呼叫时间选择的相同选择。新的Or构造函数都是由（？）操作，现在（？）：：a -> a -> ax？y=Orrxy，其中r是新鲜的用于（？）是定义函数逻辑语言的完整操作行为所需的唯一非确定性特征，如[7]所述。下面我们假设Or构造函数中的引用是简单的整数，尽管任何具有良好定义的标识的类型都可以存在。为了获得函数逻辑程序设计的充分表达能力，程序中的每个模式匹配都被Or构造函数的case扩展。例如，insert的声明由以下规则完成insertx（Orryz）=Orr（insertxy）（insertxz）insert_Fail=失败置换的定义和上面介绍的其他操作也同样完成。唯一一个比较复杂的定义是排序，如下所述。为了了解已完成的操作的行为，请考虑以下permute[3，1，2]的评估：置换[3，1，2]{-新规定！-}要将搜索树投影到一个值，我们需要一组选择。 这样一个集合定义了对哪个参考采用哪个替代。 例如，一个选择可以是（1，1），表示对于参考1，我们采取第一个选择，而（2，2）则表示对于参考2，我们采取第二个选择。 将上面例子的结果树投影到选择集[（1，1），（2，2），（4，2）]，我们将得到列表[1，2，3]。现在，搜索可以归结为选择集的系统构建。 为了说明这最后一点，我们也完成了上面定义的排序运算的定义。 当在多个构造器上进行排序匹配时，我们必须引入一个辅助函数。一般来说，在结果程序中，每个函数最多匹配一个构造函数。这使得可以在Or节点的参数中继续计算。因此，sorted的完整声明是：sorted：： [Int] ->Bool sorted[]=Truesorted（x：xs）= sorted2 x xs=> insert 3（permute [1，2]）=> 插入3（插入1（插入2[]））=> 插入案文3（插入案文1 [2]）=> 插入3（或1 [1，2][2，1]）=> 或1（插入3 [1，2]）（插入3 [2，1]）=> 或 1（或2【三、一、二】（1：插入3[2]））B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3945sorted（Orrxy）=Orr（sortedx）（sortedy）排序失败=失败sorted2 x[] = Truesorted2 x（y：ys）|x< =y = sorted（y：ys）sorted2x（Orryz）=Orr（sorted2xy）（sorted2xz）sorted2 _Fail =失败守卫”|x< =y=sorted（y：ys）<“可以被认为是（guard（x =y）（sorted（y：ys）的语法策略糖，让我们有机会说明声明完成的最后一部分，即在原始定义的匹配中缺少的构造函数将被映射为Fail：guard：： Bool -> a -> a guard True e = eguard False_ =失败guard（Orrxy）e=Orr（guardxe）（guardye）guard Fail_ =失败这样就很容易验证sorted（permute [3，1，2]）的计算结果：sorted（permute [3，1，2]）= Or 1（Or2 Fail（Or4 FailTrue））(Or3次失败（或5次失败）在考虑permSort调用的求值时，现在可以看到Or构造函数中引用的重要性。考虑到其定义，permSort操作将其参数插入树中有True的位置。因此，表达式（permSort [3，1，2]）的总求值为：permSort[3，1，2] =或1（或2失败（或4失败（或1（或2 [3，1，2]（1：或4 [3，2][2，3]））(Or 3 [3，2，1]（2：或5 [3，1][1，3]）(Or3次失败（或5次失败）重要的一点是，对于从该树到一个值的任何投影，等于permSort[3，1，2] =或1（或2失败（或4失败[1，2，3]））失败原因在于，任何通往对应于（permute[3，1，2]）的子树的路径都超过选择[（1，1），（2，2），（4，2）]。因此，这些选择也适用于这个子树，只导致一种可能性[1，2，3]。此外，包括（1，2）的任何选择只能产生失败。正如一句话，像（permute[3，1，2]）的子树中的那些不相关的替代品通常因为懒惰而在它们被评估之前被丢弃在这些情况下，他们被评估，他们需要的前一部分的评估，如在上面的例子。尽管如此，尽快删除这些不相关的选项是一个好主意，以释放内存并防止错误。46B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39必要的选择。然而，可能的优化技术超出了本文的范围，我们专注于所描述的技术的主要优点，用于构建调试工具。这个优点是，因为主计算现在在确定性推导和投影中被清楚地分离，所以开发用于重放函数程序的oracle技术可以以直接的方式扩展到函数逻辑程序2.3函数逻辑预言机我们可以直接使用两个主要思想来将oracle技术扩展到函数逻辑语言：• 非确定性选择可以像构造函数一样处理• 自由变量可以被非确定性操作替换这两种思想可以结合起来，将函数逻辑推导转化为严格推导。例如，考虑表达式head（insert3[1，2]）的惰性求值：head（insert 3 [1，2]） => head（或1 [3，1，2]（1：insert 3[2]））=>或1（head [3，1，2]）（head（1：insert3[2]））=>或1 3（head（1：insert 3[2]））=>Or131为了用oracle描述最里面的派生，我们需要做的就是把派生当作纯函数来描述。这意味着，我们声明我们执行最左边最里面的第一步，因为相应的redex（insert3 [1，2]）展开，结果为（或1[3，1，2]（1：插入3[2]））下一个最左边最里面的redex是（insert3[2]），不被评估，之后所有剩余的redex被展开。因此，得到的预言是[1，3]，我们可以将推导过程重新表述为：[1，3]head（insert 3 [1，2]）=>[0，3] head（或1 [3，1，2]（1：insert 3[2]））=>[3] head（或1 [3，1，2]（1：_））=>[2]或1（head [3，1，2]）（head（1：_））=>[1]或1 3（head（1：_））=>[0]Or131如[7]中所述，搜索树方法非常适合将搜索策略实现为树结构上的遍历。这也符合所提出的方法。例如，如果程序员只对第一个解决方案感兴趣在深度优先策略中，上述表达式将仅被评估为（Or 1 3（head（1：insert3[2]），并且对应的or-acle将是[1，2，0]。但是我们不仅可以用同一个预言机来描述非确定性操作的计算，而且可以缩小自由变量的范围。这可以通过描述如何评估相应的生成器来完成。例如，B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3947推导guard（head x）1 ={ x/（a：z）}guard a 1={ a/True}1可以用预言来描述[2，7，0]。前三个决策将变量的绑定描述为相应生成器的求值[2，7，0] genListgenBool（）=>[1，7，0]或1[]（genBool（）： genList genBool（））=>[0，7，0]或1[]（或2 True False： genList genBool（））=>[7，0]或1[]（或2 True False：_）接下来的三个步骤描述了head在生成结果中的应用[7，0]头（或 1[]（或 2T F：_））=>[6，0]或1（head[]）（head（或2T F：_））=>[5，0]或 1失败（头（或2T F：_））=>[4，0]或1失败（或2T F）最后[4，0]描述了guard的应用，假设程序员只搜索第一个解决方案，如上所述[4，0]保护（或1失败（或2T F））1=>[3，0]或1（保护失败1）（保护（或2T F）1）=>[2，0]或1失败（保护（或2T F）1）=>[1，0]或 1失败（或2（保护T1）（保护F1））=>[0，0]或1失败（或2 1（保护F 1））=>[0]或1失败（或2 1_）考虑的主要结果是，为了扩展Oracle方法，对于函数式逻辑编程，oracle的定义不需要任何改变。 主要要求是事件的记录符合[7]中描述的操作语义3调试工具我们已经将上一节中介绍的思想实现到Curry语言的调试工具中。该工具是[8]中Curry函数子集的工具的扩展。 在本节中，我们将描述如何向用户呈现Curry衍生物3.1代表非决定论带有Or构造函数及其引用的推导以及完成的归约的更多技术细节不适合在Curry程序中寻找bug的程序员。 因此，几个约定有助于获得一个关于派生的更简单的观点• 从未看到生成器函数的展开（可信函数）48B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39• Or构造函数的引用是隐藏的;例如，像（Or 2 TrueFalse）这样的值表示为（True？假）• 搜索树中不相关的部分（回想一下上面的permSort示例）总是被省略• 当“或”节点只有一个有效的备选项时;显示此备选项而不是任何故障• 在上面的例子中，省略了对辅助函数（如sorted2）的调用。我们调试工具中的permSort[2，1]：3permSort [2，1]置换[2，1]permute [1]permute[] =>[]插入1[]=>[1]permute [1] =>[1]插入2 [1]插入2[]=>[2]insert2 [1]=>[2，1]？[一、二]permute [2，1] => [2，1]？[一、二]sorted（[2，1]？[1，2]）2 1=> False 12=> True排序[2]< Truesorted（[2，1]？[1，2]）=>TruepermSort [2，1]=>[1，2]如[8]中所述，该工具还具有声明式调试模式。在这种模式下，用户可以声明子推导的正确性或不完善性，以隔离错误的规则。3.2鼓泡为了在不丢失语义重要信息的情况下省略Or构造函数中引用的表示，我们采用了[1]中首次提出的冒泡冒泡与2.2节中介绍的方法有关，因为非确定性分支被（几乎）像构造函数一样对待。第2.2节中的Or构造函数通过为完成添加的规则如head（O r r x y）= O r r（head x）（head y）一次“提升”一步。相反，在冒泡中，当一个（？）在所需的位置上，它在术语结构中向上移动，直到复制了“适当的支配者”，即，一个符号，它首先是指（？）. [1]第五条：“以物定物，以物定物。3在本演示文稿中，我们删除了一些多余的行并添加了间距。B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3949技术性的，但这个想法是非常直观的，我们将使用[13]的风格。 考虑下面的例子：let l=insert1[2] in（head l，l）=> let l=[1，2]？[2，1] in（headl，l）在第2.2节描述的方法中，这种推导的最终结果将是（1？1,2，[1，2]？1[2，1]）。参考文献（这里表示为（？）的下标）然后需要重建元组的两个部分共享相同选择的事实，即，（1，[2，1]）不是结果的有效投影。相反，在冒泡中，下一步是复制整个let表达式。(If这个表达式有一个外部上下文，这个上下文不会被复制。）在[1]的概念中，元组构造函数是支配者。设l=[1，2]？[2，1] in（head l，l）=>设l=[1，2] in（head l，l）？设l=[2，1] in（headl，l）=>（1，[1，2]）？（2，[2，1]）这种技术的优点是什么？永远不会重复，因此不需要引用。这就是为什么我们使用该技术在表示值时省略引用。在我们的工具中，推导表示为主要插入1 [2]插入1[]=>[1]insert1 [2]=>[1，2]？[二、一]head（[1，2]？[2，1]）=> 1？2main =>（1，[1，2]）（2，[2，1]）正如你所看到的，head被应用于非确定性参数（[1，2]？[2，1]）但最后的演示是漂亮打印机中冒泡过程的结果。3.3自由变量如2.3节所述，oracle方法将自由变量映射到相应生成器的求值。因此，在严格计算中，在对给定变量应用任何操作之前，已经计算了该变量的所有绑定。（与上面的（guard（head x）1，其中x自由）的评估进行比较。） 到目前为止，基于这种技术构建的调试工具因此只能访问该变量的所有绑定，这些绑定将在整个派生过程中出现。这对于用户来说可能是意想不到的，本节的目的是解释如何支持自由变量的特殊表示 为了实现这一点，我们必须对2.2中描述的搜索树机制进行一些调整。 第一个变化是，我们需要能够区分来自生成器函数的Or节点和来自调用（？）. 为了尽可能保持所描述的大多数机制的相似性，我们将这种区别引入类型OrRef：50B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39数据OrRef =发生器Int|NoGenerator Int因此，我们改变了（？）发电机运行如下：（？）：：a -> a -> ax？y=Or（NoGeneratorr）xy，其中r是新鲜的genBool：：Generator BoolgenBool_=Or（Generatorr）TrueFalsewhererfresh每个收缩步骤都必须更改Or引用，以便不再将相应的结果视为自由变量。为此，我们使用辅助函数narrow：narrow：： OrRef -> OrRefnarrow（Generator x）= NoGenerator xnarrow（NoGenerator x）= NoGenerator x函数narrow在那些添加到每个函数的规则中被调用，以处理Or情况。例如，函数head现在用以下规则完成（而不是2.2节中使用的规则）：head（Orrxy）=Or（narrowr）（headx）（heady）通过这些更改，我们现在可以对自由变量进行特殊处理，并可以向用户显示元组x的推导，其中xfree），其中元组x =（x，not x），如下所示：主元组A不是A=> True？假tupleA =>（False，True）？(True，False）main=>（False，True）？（真，假）3.4统一生成器函数的一个主要开放问题是如何回收统一运算符（=：=）的力量。这个运算符为函数逻辑编程引入了一个新的特性。在收缩仅将自由变量绑定到非变量构造函数项的情况下，（=：=）也可以将自由变量绑定到其他变量。在这一节中，我们只能粗略地描述解决Oracle方法的主要思想。为了在所提出的技术中包含统一，我们需要进一步扩展Or参考文献中包含的信息。除了能够区分生成器分支和3.3节介绍的普通分支之外，我们还需要关于生成器子节点的Or引用的信息。作为一个简单的例子，要在生成的布尔列表之间建立相等性genList genBool（）=：=genList genBool（） =>或者（Generator 1）[]（genBool（）：genList genBool（））=：=B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3951或者（Generator 2）[]（genBool（）：genList genBool（））我们不仅需要在引用1和2之间建立联系，而且需要在（：）的各个参数的引用之间建立联系。OrRef声明的相应变更为：data OrRef =发生器Int [Int]|窄化Int [Int]| NoGenerator Int每个生成器都必须在父级的Or引用dummy参数现在变成了一个正确的参数。type Generator a = Int -> agenBooli=Or（Generatori[]）TrueFalsegenListgeni=Or（Generatori[j，k]）[]（genj：genListgenBoolk）其中j，k是新鲜的一个自由变量，例如x：：[Bool]，现在由genList genBoolr引入，其中r是新鲜的。下一步是设计一种约束。为了统一，我们只需要一种约束，但原则上，其他类型的约束也可以用同样的方式处理。数据约束= Eq OrRef OrRef|......这是什么？我们需要一个额外的构造函数Constraint：：Constraint-> a ->a。约束必须像Orconstructors或Fail那样解除，例如：head（约束c x）=约束c（head x）最后，从搜索树到第2.2节中描述的值的投影必须扩展到约束求解器。由于空间有限，我们不能描述这样一个求解器的实现，并将这一部分留给未来的工作。所描述的扩展在调试工具中实现，使得（x=：=True：y&>（x，y）其中x，y自由）的求值可以被示为主要A=：=（True：B）=>成功成功&>（True： B，B）=>（True：B，B）main =>（True： B，B）4相关工作和结论我们已经提出了一个最近开发的技术来记录在一个懒惰的函数式语言编写的程序的紧凑数据。我们已经展示了如何将这种技术扩展到包括惰性函数逻辑语言的高级功能，特别是在缩小和非确定性操作方面。对统一的扩展仅仅是粗略的描述，更彻底的论述只是一部分。未来的工作。52B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）39关于相关的工作，所提出的方法是互补的，如第1节所述。有许多用于惰性函数式语言的调试工具，参见。[10]对于一个调查，但也为功能逻辑语言，比照。 [9]最新文章提出的方法是关于一种技术，以记录更少的数据有关的程序，以及如何使用这种技术来创建高效的调试工具。 根据[3]中提出的思想，我们认为这种技术可以应适用于整合所有相关方法。因此，[3]中描述的框架的转移及其应用程序构建不同的调试视图是开发的下一步该调试工具建立在所提出的技术之上，nique可以从www-ps.informatik.uni-kiel.de/下载，除了步进/跳过模式外，它还包括声明式调试和虚拟调试如[8]中所述的I/O。引用[1] S. Antoy，D.W.布朗和S.- H.蒋任 关于冒泡的正确性。 在06年RTA程序中出现在Springer LNCS，2006年。[2] S. Antoy和M.哈纳斯函数逻辑程序中的重叠规则和逻辑变量。在第22届国际逻辑编程会议（ICLP 2006）上，第87Springer LNCS 4079，2006年。[3] B.布拉塞尔一个解释函数逻辑计算轨迹的框架。理论计算机科学中的电子笔记，177：91[4] B. Braßel，S.菲舍尔，M。Hanus，F. Huch和G.维达尔 延迟按值调用评估。 法律程序中第12届ACMSIGPLAN函数式编程国际会议（ICFP'07），第265 - 276页，2007年。[5] B. Braßel，S. Fischer和F.哈。一种用于跟踪函数逻辑计算的程序变换。 在基于逻辑的程序合成和转换国际研 讨 会 （ LOPSTR '06 ） 的 预 录 中 ， 第 141-157 页 。 技术报 告 CS-2006-5 ， Universit`aca' F oscari diVenezia，2006年[6] B. Braßel，M. Hanus，F. Huch和 G.维达尔一 种用于跟踪声明 性多范式程序的 语义。在第六届ACMSIGPLAN国际声明式编程原理与实践会议（PPDP'04）ACM Press，2004.[7] Bernd Braßel和Frank Huch。函数式和逻辑式编程的紧密结合。在钟绍，编辑，APLAS，卷4807计算机科学讲义，第122-138页。Springer，2007年。[8] 贝恩德·布拉塞尔和霍尔格·西格尔。通过询问Oracle 来消除懒惰的函数式程序。In Olaf Chitil，editor，Proc. 函数式语言的实现（IFL 2007），计算机科学讲义。Springer，2008.出现。[9] 拉斐尔·卡瓦列罗、马里奥·罗德里格斯·阿塔莱霍和拉斐尔·德尔·瓦多·弗尔塞达。约束函数逻辑程序设计中缺失答案的声明式诊断在Jacques Garrigue和Manuel V. Hermenegildo的编辑，FLOPS，LNCS第4989卷，第305-321页。Springer，2008.[10] O.奇蒂尔角Runciman和M.华莱士Freja，Hat和Hood：三个系统的跟踪和调试懒惰函数式程序的比较评估。第12届函数式语言实现国际研讨会（IFL 2000），第176-193页。Springer LNCS 2011，2001年。[11] J avierdeDiosCastro和FranciscoJ. 我是个疯子. 额外的变量可以从函数逻辑程序中删除。电子笔记理论Comput. Sci. ，188：3[12] J.C. Gonz'alez-Moreno，M.T. Hortal'a-Gonz'alez，F.J. L'opez-Fraguas和M. R od r'ıguez-Artalejo.一种基于重写逻辑的声明式编程方法。Journal of Logic Programming，40：47[13] F.J. L'o pez-Fraguas，J. R od r'ıguez-Hortal'a和J。 我是赫南德兹。一个调用时间选择语义的重写概念。在第九届ACM SIGPLAN国际声明式编程原理和实践会议（PPDP'07）的会议记录中ACM Press，2007.B. Braßel/Electronic Notes in Theoretical Computer Science 246（2009）3953[14] H. Nilsson和P. Fritzson。懒惰函数式语言的程序调试。Journal of Functional Programming，4（3）：337[15] H. Nilsson和J.斯帕罗基于评价依赖树的懒惰函数优化。自动化软件工程，4（2）：121[16] E. 夏皮罗电子邮件 * 麻省理工学院出版社，马萨诸塞州剑桥，1983年。[17] J. Sparud和C.朗西曼 使用Redex Trails跟踪惰性函数计算。 In Proc. of第九届 《编程语言、实现、逻辑和程序》（PLILP'97 ）， 第291-308页。Springer LNCS 1292，1997年。[18] M. Wallace，O. Chitil，T. Bambum和C.朗西曼 Haskell的多视图跟踪：一顶新帽子。在Proc. 2001年ACM SIGPLAN Haskell研讨会乌得勒支大学UU-CS-2001-23，2001年。
我的内容管理
展开
