没有合适的资源?快使用搜索试试~ 我知道了~
52理论计算机科学电子笔记76(2002)网址:http://www.elsevier.nl/locate/entcs/volume76.html13页用于封装搜索拉斐尔·卡瓦列罗1Dep。SistemasInfaticosyProgramacionUniversidadComplutense Madrid西班牙马德里沃尔夫冈·勒克斯2Institutfur?rWirtschaftsiformatikWestfal?lischeWilhelms-Universita?tMu?nsterMu?nster,Germannyy摘要声明式调试已经被提出作为一种合适的技术,用于在声明式语言的上下文中开发调试器。然而,要想成为真正有用的调试器,它必须能够处理那些没有明确的声明性语义,但在实际程序中广泛使用的语言部分。 我们在本文中解释了如何声明性调试器的懒惰的功能逻辑语言咖喱的错误答案可以扩展到调试程序,包括封装的搜索,这种语言的一个重要功能,旨在控制非确定性的计算步骤。 我们将展示如何在不引入编译器中的任何更改的情况下实现这一点。1介绍声明式调试,也称为算法调试,首先在[Sha82]中在逻辑编程语言Prolog的上下文中引入,后来(参见[Nai97])作为一般调试技术提出总的想法是引入一个合适的计算树与任何错误的计算(初始症状)相关联。 不同种类的错误将具有不同类型的关联计算树。这种计算树的节点必须包含辅助子计算的结果,每个子计算都是通过从其子计算的结果中进行某种逻辑推理而获得的此外,任何节点都必须有可能的原因1电子邮件地址:rafa@sip.ucm.es2电子邮件地址:wlux@uni-muenster.de2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。CABALLERO和LUX53相关的错误。有缺陷的节点则是具有错误结果并且在其子节点处没有错误结果的节点,因此对应于错误的子计算(即,它产生以正确输入开始的错误输出由于树的根是错误的,因为它是主计算的结果,所以很容易证明在这样的树中至少存在一个有缺陷的节点,因此可以找到错误的原因。为了检测错误的节点,假定程序的预期含义。这个预期的含义必须由外部oracle知道,该外部oracle在调试过程期间由调试器咨询通常这个预言者是用户,因此问题的数量和简单性成为调试器有用性的关键概念由于它从语言的操作机制中抽象出来,声明式调试在声明式编程的上下文中特别有用,其中内置控件使传统调试技术(如跟踪)的使用变得复杂。这在惰性函数和函数逻辑语言[NB96,NF 97,NS 97,Pop98]的情况下尤其如此,其中求值顺序必须对程序员透明声明式调试的一个已知扩展是抽象诊断[ CL+99,ACF01 ],导致等效的自下而上和自上而下的诊断方法,这些方法不需要预先给出错误症状为了有效地实现,抽象诊断使用抽象解释技术来构建预期程序语义的有限抽象。这些方法超出了本文的范围。要想成为真正有用的声明式调试器,就不能只局限于处理语言的语义声明部分例如,输入/输出和图形界面是实际应用程序的一部分,因此任何调试工具都应该允许具有这些功能的程序完全适用。这也是封装搜索[HS98]的情况,这是Curry [Han00]语言的一个特性,用于控制非确定性计算步骤。封装搜索可以用来实现不同于通常的深度优先搜索的搜索策略,例如有界搜索或广度优先搜索。此外,它允许程序员使用I/O设施将非确定性计算封装在程序中。由于所有这些原因,封装搜索是许多Curry程序的一部分,一个现实的Curry调试器应该能够调试包括它在内的程序不幸的是,这不是小事。一方面,封装的搜索是基于一个内置的原语try,它是根据其操作行为来描述另一方面,try不能被认为是一个通常的原语(比如sin)。事实上,在声明式调试中,原语被自动假定为正确的,并且空计算树与它们相关联。然而,try是一个高阶原语,这意味着try的计算可能会有相关的错误子计算,这不是因为原语本身是错误的,而是由于CABALLERO和LUX54TOY涉及作为参数传递的程序的其他函数的项的求值在本文中,我们提出了一个声明性的调试程序的咖喱处理程序,包括封装的搜索,并显示如何做到这一点,而无需检查内置的代码尝试。关键思想是将调试程序中对原语try的所有调用替换为对新函数try'的调用这个函数是在Curry中定义的,它将返回对应于try中高阶参数执行的子计算的树。我们将展示如何在基于程序转换的声明式调试器中轻松完成此操作。本文中提出的想法是错误答案的声明性调试器工具的一部分,该工具最近被纳入了Münst er的Curry系统开发中[Lux99]。下一节将介绍用于在MünsterCurry系统中发现错误答案的声明性调试器。第3节介绍了Curry中的虚拟搜索,第4节介绍了我们将调试器扩展到使用此功能的程序的解决方案,并显示了针对第2节的示例获得的调试会话最后,第5节提出了一些结论和未来的工作。2懒惰函数逻辑程序在本节中,我们将介绍Curry错误答案的声明式调试器但仍然没有考虑封装的搜索。首先,我们将介绍我们的调试器使用的计算树,然后简要解释用于实现该工具的程序转换机制所有的概念都是通过非正式的例子来介绍的。有关这些方面的完整理论介绍,请参见[CLR 00,CR 02这两个作品都是在惰性函数逻辑语言的背景下提出的,但也适用于Curry,只有微小的变化。请注意,操作级别的差异(例如Curry中除了缩小函数缩减之外的剩余可用性)不会影响语义,因此对调试器没有影响。所有示例都以惰性函数逻辑语言Curry的语法呈现(完整描述见[Han00]我们将初始目标视为一般表达式e,并将计算出的答案视为对(eJ,σ),这意味着eσ可以被评估,从而产生eJ作为结果。当σ=id时,我们将计算出的答案简单地写为eJ。注意,Curry允许非确定性计算,因此一个目标可以有几个答案。计算树正如我们在介绍中所说的,调试过程始于在评估某个目标时检测到两种不同类型的症状是可能的,每一种对应于不同类型的错误:CABALLERO和LUX55我阳性症状:计算结果为非预期答案。这个答案被称为错误答案。阴性症状:在作为计算结果获得的结果的多集中缺少预期答案这个答案被称为遗漏的答案。当目标意外失败(即计算不出答案)时,会出现特定(但通常)的缺失答案情况。例如,考虑图中的Curry程序1.一、函数appendrepre附加eval flexappend::[A]→[A]→[A]append[]ys = ysappend(x:xs)ys = x:append xs yslast::[A] →A最后xs |append [y] ys =:= xs = y其中y,ys自由图1.一、列表中的最后一个元素发送两个列表的连接,而函数last旨在计算列表中的最后一个元素。然而,目标最后[1,2,3]返回1作为唯一计算的答案。这里我们有一个缺失的答案(3)错误答案(1)。为了检测错误的答案,oracle(调试器中的用户)必须知道程序的预期含义 正如在[CLR00]中所证明的那样,将I视为f t 1.形式的一组基本事实就足够了。tn→ t,其中t1... tn,t是构造函数术语,意味着函数f产生t作为结果当应用于t1时 tn. 用户的所有问题都是关于基本事实是在或不在。请注意,这可以确保向用户提出的问题尽可能简单这是通过将嵌套函数调用替换为计算期间获得的结果来实现的在计算结束时未计算的挂起函数调用由一个特殊的构造函数术语“”,在调试器问题中由符号表示。这样就可以得到[1,2,3]→1∈/I,而[1,2,3]→3∈I,其中I是图中程序的预期含义1.一、调试器使用的计算树在其结每个节点具有相关联的程序规则,该程序规则在该计算步骤中使用。因此,调试器将指出与有错误的节点相关联的程序规则为不正确的程序规则。节点的子节点对应于在计算时执行的子计算CABALLERO和LUX56条件(保护和局部声明)和在该点使用的程序规则的右侧[CLR00]中给出的可靠性和完整性的结果确保了在给出错误答案的情况下,调试器可以检测到不正确的实现编程器已经提出了几种策略来创建和导航计算树。在逻辑编程中广泛采用的一种众所周知的方法是在调试阶段使用元解释器来重新执行目标。因此,计算树不是显式地构造的,并且容易处理错误和这个想法已经在NUE-Prolog的情况下扩展到函数逻辑语言[NB 95]。然而,这种解决方案在不提供这些内置元指令的语言中是不可行的,如Haskell或Curry。据我们所知,目前只有针对错误答案的声明式调试器可用于这些语言。原因有两个:首先,检测缺失答案所需的计算树要复杂得多第二,错误和遗漏的答案往往同时发生,即。我们得到一个意想不到的答案而不是预期的答案。在这些情况下,通常只要找出错误答案的原因,就足以消除这两个错误。这也是我们的调试器的情况:只处理错误的答案。在相关论文中已经提出了两种不同的技术,用于产生与错误计算相关联的计算树(参见[NS 97]进行比较)。这两个建议对于惰性函数逻辑编程也是有效的:- 修改抽象机的实现以生成计算树。- 将待调试程序P转换为新程序PJ,其中所有函数返回与P中相同的结果,但与它们相应的计算树配对我们采用了基于程序转换的第二种方案,因为它的可扩展性和可移植性。因此,像这样append::[a]→[a] →[a]将包含在转换后的程序中,append’::[a]其中CTree是定义为表示计算树的数据类型数据CTree =无效|节点String [String] String [CTree]空树用于计算不能导致错误的辅助函数(可信函数)。Node的最后一个参数是子树,而字符串分别表示程序规则的名称不纯函数CABALLERO和LUX57→dval::a String在转换后的程序中使用(参见下面的示例),将任何值转换为它的String表示。请注意,这种类型转换必须递归地应用,以便也改变作为参数出现的函数类型的类型一般来说,每个n元函数f::τ1→. →τn→τ转换成一个函数f J::τ1J→. . →τnJ→(τJ,CTree),其中类型变换J定义为:αJ=α(C τn)J=C τnJ(μ→ν)J=μJ→(νJ,CTree)其中α是类型变量,C是n元的类型构造函数。实际上,如[CR02]中所解释的,n元函数f在变换后的程序中被变换为n+1个函数,包括f的部分应用的n个函数。然而,为了简单起见,我们将在这里跳过这些辅助函数例如,第二个append规则将在转换后的程序中显示为:appendtree=Node“append”[dval(x:xs),dval ys](dvalresult)[t]在这种情况下,只有一个子计算,append3封装搜索Curry中的封装搜索[HS98]允许使用用户定义的搜索策略探索谓词的搜索空间如果默认策略不合适,这很有用此外,它允许封装非确定性计算,以便它们可以用于通过Curry的monadic I/O系统与外部世界交互的程序中从语法上讲,封装的搜索可以通过基本函数trywith type来(α→成功)→[α→成功]try的参数是(一元)谓词,其解被搜索。对于某个搜索目标g,表达式tryg的求值开始于应用CABALLERO和LUX58→→g到一个新的变量x,然后减少这个应用程序,直到发生以下情况之一。(i) 求值失败,即g x无解。在这种情况下,封装的搜索返回一个空列表。(ii) 应用程序成功,只采取确定性的计算步骤。在这种情况下,重新启动是一个简单的过程[gJ],而gJ是一个孤立的过程形式G。例如,由于图的定义1、try(λx→x=:=last [1,2,3])返回列表[λx→x =:= 1]。注意last [1,2,3]的求值是完全确定的。(iii) 发生非确定性计算步骤。在这种情况下,try g以部分解决的搜索目标的形式返回这一步之后所有可能的延续的列表因此try(λx→append x[]=:=[1,2,3])的计算结果为列表3[(λx x =:=[]&append[] []=:=[1,2,3]),(λx let y,ys free inx =:=(y:ys)append(y:ys)[]=:=[1,2,3])]在try原语的帮助下,我们可以实现不同的策略来探索谓词的搜索空间实现广度优先搜索和解包其解的必要函数如图2所示。的bfsbfsg =步长[g]其中step[]=[]step(g:gs)=collect(try g)gs收集收集[][g]GSGS==步骤G:GS步骤gs收集(g1:g2:gs)GS'= 步骤(gs’ ++拆包g| g x = x其中x自由图二.广度优先搜索函数维护一个搜索目标列表。局部步骤函数从列表中获取下一个目标并对其应用try。如果这个目标没有解决方案,它将被丢弃。否则,如果目标可以确定性地求解,则返回其求解形式最后,如果try返回一个备选项列表,则本地collect函数会将它们追加到搜索目标列表在任何情况下,对于剩余的目标再次调用step解包函数对于提取搜索目标的解很有用。由于Curry的懒惰评估策略,只有那些解决方案是com-cash-cash-c[3]在Curry中,运算符表示两个谓词的(并发)合取&CABALLERO和LUX59假设实际上是需要的,使得有可能使用bfs来实现一个有无限多解决方案的目标考虑例如图的程序3、在有向图中寻找路径。图中的圈的存在性可以数据节点= A |B |C |Dgraph::[(Node,Node)]图= [(A,B),(B,A),(B,D),(D,C),(C,B)]path::[(Node,Node)]→Node→Node→[Node] path g xy| x =:= y =[x]路径g xy|(member(x,z)g)&(path g y z =:=l)=x:l其中z,l自由member::a→[a]→ Successmember x(y:ys) = x=:=ymember x(y:ys) = member x ys图3.第三章。有向图中的路使用默认的深度优先搜索产生非终止计算然而,通过将bfs与head结合使用,我们可以尝试这样的目标unpack(head(bfs(λl→l =:= path graphB C)计算从B到C然而,得到的结果是[B,C,A,B],这在第2节的意义上是错误的答案,构成了一个示例,显示了调试包括封装搜索的程序的便利性4封装搜索的声明式搜索声明式调试器除了信任基元函数的实现之外别无选择。在一阶原语的情况下,调试器可以将空计算树与它们相关联。然而,对于像try这样的高阶原语,情况更加复杂。因为函数类型出现在try的参数和结果类型中,所以不应该将try的结果与void计算树配对。此外,在类型转换之后,必须转换try的参数和结果,以匹配调试器所需的类型CABALLERO和LUX60描述在Sect。第二章:try’::(aunwrapG=λ x→ let(r,t)= gxin r包裹物 G=λ x→(g x,无效)辅助函数unwrap将参数转换为常规搜索目标,即一元谓词,通过丢弃其计算树。另一方面,wrap函数发明了一个计算树(Void),与try原语返回的目标相void计算树的使用是合理的,因为try返回的列表的所有元素都是(等价于)lambda抽象。然而,这种转换太天真了,如果我们使用下面的主函数作为图1中程序的目标,1.一、main = unpack(头 (bfs(λx→X=:= last [1,2,3])执行此程序时返回错误结果1。但是我们无法使用上面的try转换找到函数last中这个错误的来源:4正在进入调试器...未发现错误这个结果是因为我们丢弃了与封装搜索中执行的计算相关联的计算树,同时从try'返回了一个空的计算树因此,我们的转换不仅信任try原语本身,还信任try执行的所有计算。由于try执行的内部计算可能是错误的,所以我们应该返回一个非空的计算树和列表搜索目标。但是我们不能查看try原语的操作内部,以确定在封装的搜索中执行了哪些操作更糟糕的是,如果非确定性计算步骤导致try返回,则没有为搜索目标构建计算树,而只存在此树的(不相关的)部分。幸运的是,仔细的分析表明,如果我们想诊断错误的答案,根本没有必要提取这些信息。 在有try这样的Meta函数的情况下,我们必须更精确地知道哪些错误可以被4在本节中介绍的所有调试会话中,bfs和unpack函数都被认为是可信的。因此,导航器会自动跳过关于其有效性的问题,直接转到其子女。CABALLERO和LUX61→→/∈I被认为是错误的答案,因为封装的搜索可能会将丢失的答案变成错误的答案。例如,考虑简单的目标main=bfs(λx→last[1,2,3]=:=3x=:=1)对于last的预期含义,我们期望此函数返回一个包含λ-抽象的列表,等价于λx→x =:= 1。然而,鉴于最后的定义从图。1该程序将返回一个空列表,错误的答案另一方面,如果我们认为搜索目标传递给单独尝试,它根本没有解决方案,但失败了。因此,我们缺少一个答案。我们不能指望调试器诊断出这样的错误,这些错误最初是缺少答案的,而仅仅通过使用Meta函数来将它们自己表现为错误答案在这样限制了我们可以检测到的错误集之后,我们只需要求解搜索目标的计算树,并且可以信任try执行的所有中间计算。对于一元谓词p,唯一可能的错误答案是,对于某个项t,pt被满足,使得p t Success。只有当try返回的(已解决的)搜索目标应用于类似于unpack的代码中的参数时,才能观察到这样的错误。因此,与搜索目标相关联的计算树我们不能直接返回由转换后的搜索目标计算的计算树,因为try原语只能处理(一元)预测。相反,当计算成功时,我们可以用计算树实例化搜索目标的附加参数因此,我们改进的wrap和unwrap函数变为unwrapg=λ(x,t)→let(r,t&')= g x i n r t=:= t ' wrap g x|g(x,t)=(Success,t)其中t是自由的有了这些定义,try注意,通过使用等式约束,程序变得更加严格。我们的转换确保了为一个可扩展计算构建的所有计算树都是有限的。因此,在改进的unwrap函数中使用严格相等不会引入终止问题。使用wrap和unwrap的改进定义,调试器现在可以正确地发现last的错误定义。正在进入调试器...考虑到以下基本事实:1. main#toda1(1)->成功CABALLERO和LUX62它们都有效吗?(是/否)否考虑到以下基本事实:1. last([1,2,3])-> 1它们都有效吗?(是/否)否考虑到以下基本事实:1. append([1],[2,3])->[1,2,3]它们都有效吗?(是/否)是** 函数last不正确(last([1,2,3])-> 1)**一个更现实的例子,它涉及到一个非平凡的搜索,main= unpack(head(bfs(λl→l =:= path graphB C)))对于程序Fig. 3 .第三章。正在进入调试器...考虑到以下基本事实:1. main#borda1([B,C,A,B])-> Success它们都有效吗?(是/否)n考虑到以下基本事实:1. graph()->[(A,B),(B,A),(B,D),(D,C),(C,B)]2. path([(A,B),(B,A),(B,D),(D,C),(C,B)],B,C)->[B,C,A,B]它们都有效吗?(是/否)否在列表2中写出一个错误的基本事实的编号考虑到以下基本事实:1. member((B,A),[(A,B),(B,A),(B,D),(D,C),(C,B)])->成功2. path([(A,B),(B,A),(B,D),(D,C),(C,B)],C,A)->[C,A,B]它们都有效吗?(是/否)否在列表2中写出一个错误的基本事实的编号考虑到以下基本事实:1. 成员((C,B),[(A,B),(B,A),(B,D),(D,C),(C,B)])->成功2. path([(A,B),(B,A),(B,D),(D,C),(C,B)],A,B)->[A,B]CABALLERO和LUX63它们都有效吗?(是/否)是** 函数路径不正确(path([(A,B),(B,A),(B,D),(D,C),(C,B)],C,A)->[C,A,B])**5结论在本文中,我们提出了一些想法,可以用来集成一个重要的操作功能的语言咖喱,封装的搜索,到一个声明性的调试器错误的答案。所提出的解决方案很简单,并且已经在调试器中很容易地引入,并且没有对系统的其余部分进 行 解 释 , 特 别 是 原 语 try 的 内 置 编 码 。 这 一 问 题 的 解 决 方 案 可 在MünsterCurry系统中找到,具体可参见http://danae。联合国教科文组织。de/\char' ~l u x /cur r y.作为未来的工作,其他功能作为输入/输出应包括作为一部分编译器使用类似的想法在这里提出关于导航阶段,我们计划引入一种算法,以减少向oracle提出的问题数量,不仅避免重复问题,还避免先前问题引起的问题,遵循[CR 02]中此时,仅显示错误程序规则的错误实例,这通常足以在程序中识别该规则,但该信息仍必须通过包括其位置来完成一个有趣的研究点是缺失答案及其与封装搜索的关系由于任何缺少答案的目标都可以很容易地转换为失败的目标,因此可以使用原始的try将任何缺少的答案转换为错误的答案(即答案[ ]),并且可能可以在Curry中的调试器中利用这一点。引用[ACF01] M. Alpuente,J. Correa和M.法拉斯基函数逻辑程序的一种编译方案。2001年9月13日至15日,德国基尔。1[CLR00]R. Caballero,F. J. Lo'pez-Fraguas和M. Rodr'ıguez-Artalejo.惰性函数逻辑程序的声明式编程的时间基础。Tec hnicalReportSIP-104 - 00,D ep.Lenguajes,Sist emasInform'aticosylucmacion,2000年7月。二、二[CL+99] M.科米尼湾Levi,M.C.Meo和G.维泰洛抽象诊断。J. 《逻辑编程》39,43-93,1999年。1[CR02]R. 所有的人都是R和M。Rodr'ıguez-Artalejo.一种可拆卸的拆卸系统CABALLERO和LUX64TOY惰性函数逻辑程序 理论计算机科学电子笔记。第64卷。出现。二二五[Han00] M. Hanus.Curry:一种集成函数逻辑语言。版本0.7.1,2000年6月。可在www.example.com上获得http://www.informatik.uni-kiel.de/curry/report.html。 一、二[HS98] M.Hanus,F.斯泰纳在声明性程序中控制搜索。在procPLILP/ALP1、3[LS99]F.J.Lo'pez-Fraguas,anddJaimeSa'nchezn'andez.aMultiparadigmDeclarative System,In Proc. RTA'99,LNCS 1631,Springer Verlag,244-247,1999.[Lux99] W.勒克斯 实现一种惰性函数逻辑语言的封装搜索。在Proc. FLOPS 99,LNCS 1722,100[Nai97] L.Naish. 一个声明性的计划。 函数和逻辑编程杂志,1997-3。1[NB 95] L.我是蒂莫西·巴特尔 一种用于逻辑函数式语言的声明式调试器。见GrahamForsyth和Moonis Ali,eds.第八届人工智能和专家系统的工业和工程应用国际会议-邀请和其他论文,卷。第2页。91第51章2[NB 96] L.Naish和T.巴托实现一个可移植的惰性函数声明式编译器。AustralianComputer Science Communications,18(1):4011[NF97] H. Nilsson,P. Fritzson. Lazy Functional Languages(懒惰函数式语言)The Journal of Functional Programming,4(3):337-370,1994. 1[NS 97] H.Nilsson和J.斯帕罗 评价依赖树作为懒惰函数式递归的基础。自动化软件工程,4(2):121-150,1997。一、二[PW93] S.Peyton Jones,P.瓦德勒命令式函数编程。在procPOPLB. Pope. 佛 一个Haskell的声明式编译器。澳大利亚墨尔本大学计算机科学系荣誉论文,1998年6月。1[Sha82] E.Y.夏皮罗 电子邮件* 麻省理工学院出版社,马萨诸塞州剑桥,一九八二年1
下载后可阅读完整内容,剩余1页未读,立即下载
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![zip](https://img-home.csdnimg.cn/images/20210720083736.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
![](https://csdnimg.cn/download_wenku/file_type_ask_c1.png)
安全验证
文档复制为VIP权益,开通VIP直接复制
![](https://csdnimg.cn/release/wenkucmsfe/public/img/green-success.6a4acb44.png)