函数逻辑程序中的非严格和非确定性函数的消除方法

理论计算机科学电子笔记188（2007）3-19www.elsevier.com/locate/entcs函数逻辑程序Javier de Dios Castro2Telef′onicaI+D马德里，西班牙FRA N CISCOJ。L'opez-Fraguas1，3Dep。SistemasInform'ticosyComputtacio'nUniversidad Complutense de Madrid马德里，西班牙摘要现代函数逻辑语言中的程序是遵循构造函数原则的重写系统，但不需要连续性和终止性，因此可能定义非严格和非确定性函数。虽然在实践中和一些理论论文重写规则可以包含额外的变量在右手边，一些其他的作品和技术不考虑这种可能性。我们在本文中解决的问题，是否可以消除额外的变量，在这样的功能逻辑程序，证明的合理性和完整性的一个简单的解决方案，利用不一致的可能性。虽然本文的重点主要是理论，但我们给出了一些实现该技术实际可用性的第一步。保留字：函数逻辑程序，附加变量，程序变换1介绍声明性语言使用不同种类的规则. . -规则允许包含额外的变量，即变量不出现在左边。逻辑程序是大量的额外变量，在大多数情况下表达中间结果，偶尔表达不完整的信息或搜索。1作者部分得到西班牙项目TIN 2005 -09207-C 03 -03“MERIT-FORMS”和S- 0505/TIC/0407“PROMESAS-CAM”的支助2电子邮件地址：jdc254@tid.es3电子邮件地址：fraguas@sip.ucm.es1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.05.0494J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3通常，在计算过程中，这些额外的变量通过统一得到约束。相反，函数式程序完全没有额外的变量，这在范式中没有意义中间结果通过函数应用的嵌套简单地表示函数式逻辑语言（参见[12，19]的调查）旨在结合两种范式的最佳效果：非确定性和逻辑编程的隐式搜索，函数式表示法，惰性求值，高阶（HO）特征和函数式编程的类型。函数应用和嵌套避免了逻辑程序中大部分额外变量的使用，但是在函数逻辑编程中仍然有一些很好的规范，其中额外变量是有用的，例如下面的属性子列表（Xs，Ys）→ifthen（eq（Us++Ys++Vs，Xs），true）这里++是列表连接，eq是等式函数，函数ifthen由规则ifthen（true，Y）→Y定义。注意Us，Vs是sublist规则中的额外变量;还注意，尽管存在额外变量，程序仍然是连续的，因为sublist（Xs，Ys）只能返回值true。现代函数逻辑语言如Curry [14]或Toy [6]也使用某种重写规则作为程序，这些规则可以是非终止和非连续的，因此可能定义非严格的非确定性函数。后者是这样一个家庭的功能逻辑语言，我们专注于和我们使用FLP作为通用名称的一个显着特点。非确定性可能来自函数的重叠规则，就像下面的非确定性常数（0元函数）硬币一样：硬币→0硬币→1这类非确定性函数将在本文中得到广泛的应用。非确定性也可能来自于在右边不受限制地使用额外的变量，比如下面的子列表程序的变体，其中定义了一个非确定性函数，而不是谓词：a子列表（X）-ifthen（eq（Us++Ys++Vs，Xs），Ys），注意，现在Ys，Us和Vs是额外的变量，并且程序不再是连续的。我们对消除额外变量的兴趣是双重的：首先，我们想从理论上澄清这样一个直观的事实，即借助于非确定性函数，额外变量在某种意义上是不必要的;其次，FLP领域的许多工作这种情况会发生，仅举几例，与操作问题相关的工作[4]，关于部分评估[2]或关于失败的技术[16]。消除额外变量在逻辑编程[18，3]或条件项重写系统[13，17]领域值得关注。这些作品都不包括我们的FLP计划（特别是，所有这些都需要连贯性4我们不认为函数程序中let声明引入的局部变量是逻辑程序或重写系统中J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）35所涉及的技术比这里所提出的方法更复杂，但不确定它们在适用于相同情况时是否确实更有效。这可以被看作是一个很好的例子，说明扩大视野（放弃连贯性）有时会使解决方案变得更糟。本文的其余部分组织如下：在下一节中，我们给出了一些介绍性的想法和讨论;第3节是本文的核心，精确描述了我们的方法以及可靠性和完整性的结果，使用CRWL [ 8，9 ]作为形式化设置，这是一个著名的语义框架FLP;第4节解决了更多的实际问题，并给出了一些实验结果;最后，第5节总结了一些结论，讨论了一些局限性，并指出了今后可能开展的工作。更多的细节，特别是关于实际问题的细节，可以在[7]中找到。2一个介绍性的例子考虑下面的FLP程序P，用于检测自然数（由构造函数z和s表示）是否是完全平方，定义了一些基本函数：add（z，Y）→ Ytimes（z，Y）→ zadd（s（X），Y）→ s（add（X，Y））times（s（X），Y）→ add（Y，times（X，Y））eq（z，z）→ 真eq（z，s（Y））→ 假eq（s（X），z）→ 假eq（s（X），s（Y））→ eq（X，Y）%布尔值相等的类似规则if（true，Y）→YpfSquare（X）→ifthen（eq（times（Y，Y），X），true）请注意，pfSquare的规则包含一个额外的变量Y。 因此，P不是函数式程序，而是适合于函数式逻辑程序设计领域。忽略具体语法5，P在现有的FLP系统中是可执行的，如Curry [14]或Toy [6]。例 如 ， 为 了 计 算 表 达 式 pfSquare （ 4 ） （ 我 们 写 4 来 替 换 s（s（s（z）），我们可以简单地重写它，生成新的表达式ifthen（eq（times（Y，Y），4），true）。现在，重写是不够的，因为变量Y的出现;这就是为什么FLP使用某种窄化（参见[12]）而不是重写作为操作过程。在这个例子中，在一些失败的尝试之后，收缩产生绑定Y/s（s（z））和表达式的值true。具体到这个例子，我们的目的是把P变换成一个新的程序PJ语义上等同于P6J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3[5]特别是，我们在整个论文中使用一阶语法，而Curry或Toy使用HO curried符号。J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）37但是没有额外的变量。要获得这样的PJ是很容易的：我们用一个非确定性常数（即0元函数）genNat替换额外的变量，其值的范围是所有自然数的集合。因此，通过将genNat的以下定义添加到P来获得PJ：genNat→z genNat → s（genNat）并将定义pfSquare的规则替换为pfSquare（X）→pfAux（X，genNat）pfAux（X，Y）→ifthen（eq（times（Y，Y），X），true）值得注意的是转换的简单性和局部性：只有额外变量的规则必须转换。如果使用局部定义，转换会变得更6在这种情况下，pfSquare的规则可以是：pfSquare（X）→ifthen（eq（times（Y，Y），X），true），其中Y = genNat这与在逻辑程序或某种重写系统中消除额外变量的现有方法形成对比[18，3，13]，这些方法要复杂得多，并且通过向比具有额外变量的函数或谓词更多的函数或谓词添加新参数来不尊重局部性。在我们的例子中，如果事情是如此容易，是因为定义非确定性函数的可能性由FLP所描述。然而，请注意，非确定性的行为可能相当微妙，特别是当与FLP中考虑的非严格语义（操作术语中的惰性求值）相结合时。我们的转换是这种微妙之处的一个很好的例子：在Curry或Toy中遵循的调用时间选择制度[15，9]下，它是正确的，但在Run中则是不合理的。时间选择机制7.图1显示了程序PJ和表达式pfSquare（s（s（z）的一个可能的归约序列，它使用运行时选择并返回值true，这是错误的。我们在每一步还原的redex下面画下下划线，并写→来表示一系列还原步骤。注意，使用调用时间选择时，所有genNat的出现都应该被共享，因此之前的减少是不合法的。还请注意，在原始程序P中，调用时选择和运行时选择从结果的角度来看没有区别，因为P是连续的：在这两个选项中，pfSquare（3）的约简都失败了。由于这种原因，我们认为，尽管转换很简单，但底层语义足够复杂，需要对其正确性进行形式化证明，这将在下一节中进行。[6]但不存在于下一节要考虑的理论CRWL框架7使用函数式编程的标准术语，具有非严格语义的调用时选择可以在操作上描述为按需调用并共享，而运行时选择在没有共享的情况下进行，这在缺乏一致性的情况下非常不同。8J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3pfSquare（3）→pfAux（3，genNat）→ifthen（eq（times（genNat，genNat），3），true）→ifthen（eq（times（s（genNat），genNat），3），true）→ifthen（eq（add（genNat，times（genNat，genNat）），3），true）→pfAux（3，genNat）→ifthen（eq（s（s（times（genNat，genNat），3），true）→ pfAux（3，genNat）→ ifthen（eq（s（s（times（genNat，genNat），3），true）→pfthen（eq（times（genNat，genNat），z），true）→→ifthen（eq（z，z），true）→ifthen（true，true）→trueFig. 1.使用运行时选择的错误计算3变量消除：方法和结果本文给出了消除多余变量的程序变换的精确定义和证明。我们必须从一个正式的设置FLP与非严格的语义和非确定性与调用时间的选择相结合的良好治疗，因为它是我们的方法中的一个关键问题3.1官方网站：CRWL由于我们感兴趣的是确保转换后的程序相对于原始程序的语义等价性，因此我们选择了CRWL框架[8，9]。另一种方法可能是[1]的方法，但对于我们的目的来说，它在操作上有很大的基于构造器的重写逻辑（CRWL）在[8，9]中引入，作为具有惰性非确定性函数的函数逻辑编程的基础，涵盖声明性语义-逻辑和模型理论-以及惰性窄化演算形式的操作语义。我们主要使用CRWL的逻辑面。作为非确定性的语义，CRWL天使的非决定论意味着所有可能的计算的结果，由于不同的非决定论的选择，由语义8收集，即使无限计算的可能性不被排除。调 用 时间选择意味着给定函数调用f（e1，. ，e n），在应用定义f的重写规则之前，为每个实际参数选择一些固定的（可能是部分的）值。更接近于实现的替代描述如下：按需调用用于减少f（e1，...，e n）但是[8]但不是通过每一个单独的计算，它只负责产生一个值。不同的值通常是在不同的计算中通过回溯得到的J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）39在归约中可能引入的所有E1的CRWL被广泛接受为FLP的坚实语义基础，并且已经成功地以多种方式扩展到涵盖FLP的不同方面，如HO，代数和多态类型或约束（参见[19]的调查），但我们坚持使用原始版本，这是一阶和无类型的。在最后一节中，我们讨论了这些限制，顺便说一下，这些限制在大多数关于FLP的论文中是常见的。现在我们回顾一下本文所需要的关于CRWL的基本概念。3.1.1CRWL基本概念我们假设两个不相交的构造函数符号集c，d，. ∈CS和函数符号f，g，. ∈FS，每个符号有一个固定的arity≥ 0。构造函数项（简称c项）t，s，. ∈CTerm的定义和通常一样，使用CS的构造器符号和可数集V中的变量。部分c项的集合CTerm也是通过允许使用CTerm作为常量（0元）构造器符号来获得的。表示未定义的值，需要在语义中表达部分值。表达式e，l，r，. ∈Expr由变量、构造函数符号和函数符号组成。来自Expr的部分表达式也可以使用。如果C项和表达式不包含变量，则它们被称为基础。C-置换是映射σ：V →CTerm，它自然地扩展到σ：Expr→Expr。类似地，我们将部分C-替换定义为σ：V →CTerm。一个代换是接基的，如果对所有的X∈V，Xσ是接基。部分表达式e±EJ之间的近似序是对所有e∈Expr验证<$±e的最小偏序，并且使得构造函数和函数符号是单调的.CRWL程序P是基于左线性构造器的重写规则的任何集合，即，形式为f（t1，.，tn）→e，其中f∈FS有元n≥ 0，（t1，. ..没有变量在c项中出现两次请注意，对于同一个f，或者对于e中的变量，没有关于不同规则的限制。规则l→e的额外变量的集合是EV ar（l→r）=var（r）\var（l）。P的规则的部分c实例的集合被定义为：[P] σ={（l→r）σ|（l→r）∈P，σ∈ CSubst<$}它将在下面表示调用时间选择时发挥作用注意，如果l→r∈[P]<$，则（l→r）σ∈[P]<$，对于任何σ∈CSubst<$。注：在[8，9]中提出的原始CRWL考虑了形式为f（t1，.，t n）→e∈C1，.，Cm，其中每个Ci是可连接性条件e da eJ，表示e和eJ可以简化为可统一的c项。在[8，9]中引入了可连接性条件，以改善严格平等是本文件的次要主题。 另一方面，10J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3（英国电信）e∈Exp（经常资源）X∈Ve→X→ X（中文）（法e1→t1..en→ tnc（e1，.，e n）→ c（t1，.，t n）e1→t1. en→ t ne→f（e1，.，e n）→ tc∈ CSn，ti∈ CTerm<$，ei∈Exp<$如果f（t1，...，t n）→ e ∈ [P]图二. CRWL证明演算简单的事实，条件可以被替换的功能，如果然后使用，如在第2节的例子。由于所有这些原因，我们只考虑无条件的规则。3.1.2CRWL证明演算CRWL通过一个能够导出e → t形式的约简或近似语句的证明计算来确定程序P的逻辑语义（e∈Expr，t∈CTerm），其中“reduction”包括从P应用重写规则的可能性，考虑到调用时间选择，或者用C替换某些子表达式。图2显示了CRWL可导出性的规则。BT代表底部，RR代表限制反萃性，DC代表分解，OR代表外部还原规则BT与OR中部分实例的使用相结合，表达了非严格的语义。在OR中使用C实例而不是一般实例反映了调用时间选择。与通常的逻辑演算一样，一个命题e→t的推导可以用一个证明树来表示，结论写在底部。我们写P<$CRWL<$来表示语句<$N从P有一个CRWL-派生。我们有时会说P-推导，以明确哪个程序用于的推导。请注意，CRWL演算不是执行程序的操作过程，而是描述程序逻辑的一种方式。下面的引理表示CRWL-可导性在C-置换下是封闭的，并且是单调的，是关于CRWL的已知结果的微小变化。引理3.1设P是CRWL-规划，e∈Expr，t∈CTerm。若P<$CRWLe→t，则对任意σ ∈CSubst σ，P<$CRWLeσ→tσ.此外，可以使两个推导具有相同数量的（OR）步骤。引理3.2设P是CRWL-程序，e，eJ∈Expr，t∈CTerm. 如果P<$CRWLe → t和e ± EJ，则P <$CRWLEJ→ t.3.2非确定性生成器可以替换额外的变量如第2节所示，额外的变量将被替换为能够生成所有基础c项的非确定性常数。我们首先定义了J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）311生成器，这取决于签名;我们假设构造器符号的固定集合CS定义3.3（接地生成器）用户定义的常数（0元函数）gen称为接地生成器，如果Rgen<$CRWLgen→t，对于任何接地t∈CTerm<$，其中Rgen是定义gen的规则集（可能加上一些辅助函数用于定义性别）。注意，如果程序P包含接地生成器，则P也是CRWL对 任 意 基 t∈CTerm <${\displaystyle{\cHFFFFFF}{\3cH111111}{\4cH111111}gen→t {\displaystyle {\frac {t}建造接地发电机并不困难引理3.4由规则定义的函数gen→ a%对于每个常量构造函数 agen→c（gen，. ，gen）%对于arity n> 0的每个构造函数c是接地发电机证据Rgen的事实是从对t的大小的简单归纳得出的。Q我们现在定义程序变换以消除额外的变量，它由给定的接地生成器参数化。定义3.5（变换后的程序）设P是一个CRWL-程序，并生成一个接地生成器。变换后的程序Pj的结果是在P中加上gen的定义，并在P中替换每个规则f（t1，...，t n）→r，带有额外变量V ar（r）−V ar（f（t1，.，t n））={X1，. ，X m}Ω根据两条规则f（t1，. ，t n）→ f J（t1，. ，tn，gen，. ，gen）f J（t1，... ，t n，X1，. ，X m）→ r其中fJ是一个新的函数符号（每个规则有一个额外的变量）。显然，在PJ中没有额外的变量。这个变换可以被推广，而不需要考虑下面结果的有效性，通过允许在f的新规则中对gen的不同出现使用不同的生成元。下面的定理，这是本文的主要结果，建立在何种程度上转换的PJ和原来的P是等价的声明语义，即相对于CRWL-可导性。定理3.6设P是CRWL-程序，P是它的变换程序，按Def. 3.5，e ∈ Expr是不使用Pj的辅助符号的表达式，t∈CTerm是基c项。则P<$CRWLe→t惠PJ<$CRWLe→ t。第二部分可以理解为变换的正确性（对于所考虑的约简类），第三部分可以理解为完备性。注意到我们12J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3不能期望降低施加在t上的接地条件。[9]最简单的例子是一个只有一个规则f→X的程序P，其中PJ是gen的定义加上规则f→FJ（gen）和FJ（X）→X 。 很 明 显 ， P<$CRWLf→X 而 不 是 PJ<$CRWLf→X; 我 们 得 到 的 是PJ<$CRWLf→t对X的每个基实例。为了证明这个定理，我们需要一些关于CRWL-导子中变量使用的辅助结果。第一个证明了对于证明基础语句e→t，即使程序P有额外的变量，也可以写出完全没有变量的CRWL-推导这并不排除存在，对于同一个语句，其他CRWL-衍生变量。引理3.7设P是CRWL-程序，e∈Expr，t∈CTerm。若P<$CRWLe→t且V ar（e→t）=N，则e→t有无变量的CRWL-导子。证据我们通过归纳法对e → t的CRWL推导的复杂性度量进行推理，定义为|e→t| =（n，k），其中n是推导中OR步骤的数量，k是步骤的总数。复杂性度量按以下顺序排序：字典顺序基本情况对应于最小复杂度（0，1）。 对于构造函数常量，派生必须是B：e→ C的形式，或DC：c→c的形式C.在这两种情况下，结果都是微不足道的。注意，RR：X→X的情况被排除，因为c e Var（e→t）=π。对于归纳的情况下，我们区分两个子情况下，根据CRWL规则中使用的最后一个推理步骤。e1→t1.. en→ tn• 华盛顿特区：c（e1，.，e n）→c（t1，.，t n）在这种情况下，归纳假设的结果是直接的，因为|e i→我不是||c (e1,...，e n）→c（t1，.，t n）|1 ≤i≤ n。e1→t1.. e n→t nr→ t• 或：f（e1，... ，en）→ t对于f（t1，. ，tn）→ r ∈ [P]<$.设σ∈CSubst是Var（{t1，.，t n，r}）（我们甚至可以假设σ∈ CSubst）。由引理3.1我们知道P<$CRWLei σ→ti σ（1≤i≤n）和P<$CRWLrσ→tσ，其中ei σ→ti σ和rσ→tσ的OR步数不随t而变。ei→ti和r→t。因此，在本发明中，|e i σ→t i σ|和|rσ→tσ|都是|f(e1,. . . ，en）→t|，其中对于f（e1， . . ..要应用归纳假设，仍然要看到eiσ→tiσ和rσ→tσ都是基，但这很容易，因为ei，t是基（因此eiσ=ei和tσ=t），而tiσ和rσ是通过σ的构造而基。因此，我们认为，通过归纳假设，所有ei→tiσ和rσ→t都有CRWL-导子，[9]更确切地说，完整性需要有根据。 不难看出，只要e不使用来自PJ的辅助符号，那么对所有归约e→t都是正确的。J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）313变量最后，只要注意到f（t1σ，. ，t n σ）→ rσ ∈ [P]<$，我们可以建立一个CRWL-导子e1→t1σ. en→ tn σ rσ→ t或：f（e1，... ，e n）→ t这是自由的变量。Q注意，对CRWL-导子的结构（或大小）的直接归纳是行不通的，因为没有任何东西能确保在外部归约的情况下，前提中的箭头ei→ti我们需要把他们通过一个辅助替代σ，但然后归纳假设是不适用的下面对前面引理的推广在本文的其余部分中并不是真正必要由于这个结果不是严格需要的，所以我们在证明中不那么正式。引理3.8设P是CRWL-程序，e∈Expr，t∈CTerm。 如果P<$CRWLe→t，则存在e → t的CRWL-导子，它只使用来自e→ t的变量。证据（草图）。我们可以用新的常数替换e→t的变量，并应用前面的引理，得到一个没有变量的导数。在这个推导中，它可以用原始变量替换引入的新常数。Q在下面的引理中，已经非常接近定理3.6，我们证明了变换后的程序在语义上等价于基态的原始程序引理3.9设P是CRWL-程序，PJ是其变换程序，e∈Expr是不使用P j的辅助符号的表达式，t ∈ CTerm。如果V ar（e →t）=π，则P<$CRWLe→t惠PJ<$CRWLe→ t。我的律师。 Sinc e Var（e→t）=0，L emma3. 7ensurethate→thasaP-divin无变量。我们用归纳法对这类P-导子的结构进行了推理.基本情况下，推导包括应用B或DC的常数，是平凡的。和引理3.7一样，规则RR必须被忽略。我们考虑两个归纳的情况下，根据CRWL规则中使用的最后一个推理步骤。DC的情况是直接使用归纳假设。所涉及的情况是OR，因为程序规则从P变为PJ。假设一个P-导子的形式为：或：e1→t1σ. e n→t n σ rσ→ tf（e1，... ，e n）→ t其中f（t1，.，tn）→r∈P，σ∈CSubst，且ti σ（1 ≤i≤n），rσ是基（记住整个导子都是基）。作为归纳假设，我们有PJ<$CRWLei→tiσ（1≤i≤n）和PJ<$CRWLrσ→t.14J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3我们必须建立一个P J-推导也为f（e1，. ，e n）→ t.如果P，f（t1，. ，t n）→ r，没有额外的变量，相同的规则也是Pj的规则。这一事实与归纳假设一起直接给出了PJ-导子.否则，设X1，.，X m是r的 额 外 变 量 。 由 于 PJ 包 含 接 地 生 成 元 gen 的 定 义 ， 我 们 有PJ<$CRWLgen→Xiσ （ 1≤i≤m ） 。 很 容 易 看 出 ， PJ<$CRWLti σ→ti σ（1≤i≤n），然后我们可以建立下面的PJ-导子：t1 σ→ t1 σ. tn σ→ tn σgen→ X1 σ. gen→ Xm σrσ→ t或：fJ（t1，.，tn，gen，. gen）→ t最后，由于f（t1σ，.，t n σ）→fJ（t1σ，...，tn σ，gen，. gen）∈ [PJ]，我们可以建立期望的P J-导数：e1→t1σ. e n→t n σfJ（t1σ，.，tn σ，gen，. gen）→ t或：f（e1，... ，e n）→ t和前面一样，通过引理3.7，我们可以从PJ-导子开始，其中e→t没有变量10。我们用归纳法来推理这个推导的大小。我们专注于有趣的归纳的情况下，当PJ-推导结束与或步骤，使用的程序规则的PJ来自规则在P与额外的变量。假设这个P-规则是f（t1，. ，tn）→ r，在Pj中对应的规则是f（t1，.，t n）→fJ（t1，.，tn，gen，.，gen）和FJ（t1，.，t n，X1，.，X m）→r. PJ-推导将采用以下形式：e1→t1σ. e n→t n σfJ（t1σ，.，tn σ，gen，.，gen）→t或：f（e1，... ，e n）→ t我们必须为同一个陈述建立一个P证明了对FJ（t1σ，…，tn σ，gen，. ，gen）→ t作为上述前提出现，必须对f j使用唯一的PJ-规则，因此具有以下形式：t1 σ→ t1 σ. tn σ→ tn σgen→ X1 σ. gen→ Xm σrσ→ t或：fJ（t1σ，. ，tn σ，gen，. ，gen）→ t归纳假说特别指出，P<$CRWLei→tiσ和P<$CRWLrσ→t，用它我们可以建立所需的P-导数：e1→t1σ. en→ tn σ rσ→ t或：f（e1，... ，e n）→ t注意，为了应用归纳假设，我们已经使用了这样的事实，即ei（因为它们是初始表达式的子表达式）和r（因为它来自P的规则）都不包含来自PJ的辅助符号。Q前面的引理已经是一个相当强的等价结果。例如，在第2节的例子中，只要保证变换后的程序给出pfSquare（4）-> true就足够了，如果原来的程序是[10]在这种情况下，这也可以在没有引理3.7的情况下利用PJ没有额外变量的事实来证明J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）315程序做的。 定理3.6通过去掉条件而var（e）=1。我现在要说的是：证据（定理3.6）假设P<$CRWLe→t，t接地。令Var（e）={X1，.，Xn}，并考虑置换σ={X1/X2，. ，Xn/n} ∈ CSubst<$.通过引理3.1，P<$CRWLeσ→tσ，即，P<$CRWLeσ→t，因为t接地。根据引理3.9，PJ<$CRWLeσ→t，因为eσ→t是基。根据引理3.2，PJ<$CRWLe→t，因为eσ±e。相似。Q4发电机在实践中虽然本文的目的主要是理论性的，但在本节中，我们将简要讨论有关使用接地发电机的一些实际问题，并给出一组小型实验的结果。在这一节中，我们不是正式的，而是通过例子来解释。我们使用Toy [6]作为参考语言，但大多数（如果不是所有）评论也适用于Curry [14]。首先，由于FLP语言是类型化的，因此应该为每个（数据构造的）类型编写一个生成器。除了比“通用”生成器更有效之外，这还可以防止病态。在下一节中，我们将对基本类型和多态性第二，并不是每个接地生成器都可以在实践中使用，至少在FLP语言的最常见实现中，它执行计算空间的深度优先搜索。像[20]这样的完整实现不会出现这个问题。例4.1考虑数据类型定义数据t= a|B| c（t，t）。引理3中给出的接地生成元为gen-> a gen-> b gen -> c（gen，gen）在深度优先搜索下，gen的评估通过回溯va，b，c（a，a），c（a， b）， c（a，c（a，a）），.的序列来产生。.. . valuec（b，b）和其他无穷多的c（b，b）永远不会出现，从而破坏了理论的发电机使用的完整性。这种情况其实并不新鲜，因为深度优先搜索本身就破坏了FLP系统操作过程的理论完整性但至少有了发电机，我们可以用很少的电力做得更好4.1编程公平发电机为了在深度优先搜索下也完成的程序生成器，我们可以通过迭代深化来进行，即，通过增加复杂性的级别，假设每个级别是有限的，并且所有级别的并集覆盖给定类型的数据值的整个宇宙。也许最简单的选择是在每个层次上收集给定深度的所有项。不仅是简单的：在我们的实验中，我们发现这种选择16J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3ft型，任何深度f深度≥Nf深度 =Nf 深 度≤Nf深度N%此处使用第4代可避免重复--gen：生成值--gen1（N）：生成值o--gen2（N）：生成值o--gen3（N）：生成值o--gen4（N）：生成值oGen->第1代（z）第1代（N）->第2代（N）第1代（N）->第1代（s（N））第3代（N）->第2代（N）第3代->第4代（N）第二代（z）->一第二代（z）->B第2代（s（N））->c（第2代（N）、第3代（N））图3.第三章。数据类型t的公平生成器行为比用于确定级别的其他标准好得多，例如术语的大小，无论是绝对的（符号数）还是某种加权。对发生器进行编程以增加深度并不困难。图3包含了上面例子中数据类型t的公平生成器。我们使用自然数作为辅助数据类型;可以使用原始整数。需要一族辅助函数来实现公平性并避免重复。4.2一些结果接下来，我们展示了带有额外变量的原始程序与消除它们后的转换程序之间的比较为了比较，我们给出了运行时间和头范式的减少次数，这与实际实现和计算机更加无关 这些程序在系统TOY [6]中被定义，其源代码可以在地址http://gpd.sip.ucm.es/fraguas/prole06/examples.toy。表4对应于自然数上的一些函数：pfSquare（见第四节）。2），偶数，类似，但使用加法而不是乘法，和可分的，它识别自然数是否可分，由规则divisible（X）-> ifthen（eq（times（s（Y）），s（Z），X）定义，其中包含两个额外的变量在所有情况下，我们都尝试了不同的自然数，其中一个产生了失败的减少，这需要探索整个搜索空间。标有（）的列表示归约最终失败。很明显，转换后的程序的性能不会有太大的变化从原来的。J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）317程序N = 100N = 997N = 4900MSHNFMSHNFMSHNF甚至原始程序40957小行星3366109744067646557变换程序7010086130（）119728010749008pfSq原始程序50164262080（中）9725847290275352变换程序502073小行星8361914556418263394563div原始程序110115664926（中）1019129294356356变换程序1001205小行星873751508596308358805见图4。 关于自然数的程序N = 10N = 30N = 50MSHNFMSHNFMSHNF子列表原始程序1046114125616096261变换程序1677678469618711816最后原始程序105583134586308758变换程序16112978839923422469Intersec原始程序109641551355454753744变换程序301624312250041375102064图五. 列表的一些结果表5对应于在不同数据库列表上操作的一些函数。我们尝试了不同的深度，列表的深度取决于它的长度，也取决于它的元素的深度。结果仍然可以接受。一个有点令人惊讶的事实，我们没有任何好的解释，是对于子列表，系统报告更多的减少到hnf，但也更好的运行时。对于这个比较，我们运行了TOY v.2.2.3（使用Sicstus Prolog 3.11.1）。在Pentium 4（3.4 Ghz）中，在Windows XP下，具有1Gb5结论和今后的工作我们提出了一种在函数逻辑程序中消除额外变量的技术，即变量出现在函数定义规则的右手边，而不是左手边。因此，额外的变量是不必要的，至少在18J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3一定的理论意义上。与逻辑程序或更受限制的重写系统类的情况相比，在我们的环境中，由于可以编写由像CurryJ. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）319或玩具：通过调用能够生成所有基础构造器项的非确定性常数（0元函数）来替换额外变量的出现-以方便的方式来尊重这些语言所采用的调用时选择语义。任何满足这种性质的生成函数都可以使用，这给实验留下了空间。到目前为止，我们所做的实验表明，至少对于使用深度优先搜索的Toy或Curry这样的系统来说，一个简单但好的选择是通过迭代增加生成的术语的深度来操作由于生成函数有一个相关的无穷搜索空间，我们的方法在许多情况下确定了一个无穷搜索空间，即使原始定义没有。但由于懒惰，情况并非总是如此，如表4所示。我们的方法与有限失效的精确关系是未来研究的一个有趣课题。我们已经证明了我们的建议在CRWL框架，这通常被认为是一个坚实的语义基础FLP的正式设置的适当性。我们已经考虑了CRWL的一阶非类型化版本，现在我们简要讨论两个限制：• 考虑（基于构造函数的）类型涉及到几个方面：第一个，容易解决的，是应该为每个类型定义不同的生成函数，如第二节所述四、更多的困难这篇论文但是在当前的FLP语言中，类型的运行时管理是不可用的，并且绝对超出了本文的范围。像实数这样的原始类型也会导致明显的困难，但同样的情况也适用于这些类型中使用额外的变量，因为通常不能对它们使用窄化，因为基本操作（如可以是+）不受重写规则的约束;这些情况属于约束编程的领域• 添加HO函数并没有实质性的改变，除非额外的这是允许的，但在实践中肯定不常见，在系统Toy中，基于CRWL的HO扩展[10]。根据内涵从HO-CRWL中的函数的角度来看，HO变量原则上可以通过生成HO模式的函数来消除。除了已知的关于类型的微妙问题之外，新的问题出现了，因为这样的生成器通常不接受主类型，因此必须作为内置程序实现，并留在类型规程之外。从实际的角度来看，我们的方法的一些改进是可取的，通过提供一个更大的类的发电机，确定其适当的某些类别的问题，或通过结合使用发电机与其他技术，例如基于某种局部评估。我们最近知道一个独立的和同时期的工作[5]，其中提出了一个类似于我们的程序变换，用于消除函数逻辑程序中的额外变量。然而，仍有若干分歧需要指出。一个是[5]中缺乏任何实际结果的指示20J. de Dios Castro，F.J.López-Fraguas/电子笔记理论计算机科学188（2007）3但主要的一个是在每一个工作中考虑的形式框架：[5]证明了转换相对于普通重写的完整性，而合理性被证明为考虑显式替换的重写变体，以反映调用时间选择，因为否则转换是不合理的，正如我们在节中指出二、我们发现这种形式设置的变化有点不令人满意，因为调用时选择的完整性并没有得到真正的证明，这可能比普通的重写（运行时选择）获得此外，我们认为，使用CRWL允许一个更简单的证明。最后，我们对消除额外变量的一个有趣的潜在副产品进行最后的评论。我们可以区分两种情况，在这种情况下，需要将变窄作为FLP的操作过程：第一种是当要求值的初始表达式有变量时，即使程序没有使用额外的变量;第二种是当作为中间步骤，使用了一个有额外变量的规则，