函数式逻辑程序设计的重写系统与构造器的重写系统类似

理论计算机科学电子笔记57（2001）网址：http://www.elsevier.nl/locate/entcs/volume57.html16页函数式逻辑程序设计塞尔吉奥·安托伊1;2波特兰州立大学P.O. Box 751，Portland，OR 97207，USA摘要函数逻辑程序设计语言的基础和发展的最新进展源于缩小求值策略的深远结果。窄化是一种类似于重写的计算，它产生除了范式之外的子项。在函数式逻辑编程中，应用窄化的重写系统的类在很大程度上是基于构造器的重写系统的子类，可能是条件重写系统。许多有趣的收缩策略，特别是对于基于构造函数的重写系统的最小子类，是众所周知的重写策略的概括。然而，一些策略，更大的非conuents子类已经开发了功能逻辑计算。在本文中，我将讨论的元素，发挥相关作用的功能逻辑编程的评价策略，描述了一些重要的类重写系统，模型功能逻辑程序，显示这些类提供的表现力的例子，并审查的特点，缩小战略提出的每一类重写系统。1引言函数式逻辑程序设计研究的是将函数式程序设计和逻辑程序设计的特征结合在一个单一范例中的程序设计语言。在大多数情况下，函数逻辑程序可以被看作是一个基于编译器的条件重写系统（TRS）。在这些例子中，我对符号做了一些自由的处理。例1.1下面的程序解决了著名的N皇后问题：queens X -> Y：- Y=permute X，void（capture Y）1 部分由NSF资助INT-9981317和CCR-0110496支持。2 电子邮件地址：antoy@cs.pdx.educ 2001年由Elsevier Science B出版。V. CC BY-NC-ND许可下的开放访问。昂托伊2permute [] ->[]置换[X| Xs]->U++[X]++V：-U++V=置换Xs捕获Y：--++[Y1]++K++[Y2]++-=Y，abs（Y1-Y2）=长度K+1TRS是一阶语言，但本文中函数和构造函数应用的符号与函数式程序设计中的符号相同。条件重写规则具有以下形式：l！r：t1= u1;：;tn=un其中l和r分别是左侧和右侧，并且条件是形式为ti=ui的一系列基本等式约束。符号\=”被解释为严格相等。该程序采用了熟悉的Prolog符号列表和变量，并使用常见的x算术运算符，但这只是语法糖。Abs，代表整数绝对值，++和length，代表列表连接和长度，被认为是库函数 。 捕 获 是 一 种 约 束 ， 即 ， 一 个 函 数 ， 类 似 于 Prolog 谓 词 ，\succeeds”i它的条件成功。 Void是一个原始构造，它的参数是一个没有解的约束。形式的查询，例如，queens[1，2，3，4]非确定性地计算4-queens问题的解。为了理解函数式逻辑编程语言的前景，将上述程序与针对同一问题提出的函数式和逻辑程序的教科书示例进行比较是有益的。所有的程序，包括我们的程序，都是以生成和测试模式构建的。生成器生成棋盘行的排列。排列的第n个元素代表第n列皇后在棋盘上的位置。一个有效的解决方案应该避免，例如，（n1）的完全生成！当单个测试将成功时，以不正确的初始位置开始的排列。纯逻辑版本[21，pages 132{135]由于需要增量地生成潜在的解决方案并在生成下一个增量之前测试它们而变得复杂。这防止了库谓词的使用，例如，来计算排列，并使这个程序的代码专用于这个问题，并且不可重用。纯函数版本[10，pages 161{165]由于数据结构的存在而变得复杂，例如（懒惰地）保存整个排列集合的列表列表，或者简化放置安全性测试的对列表，以及构造和拆开这些结构的函数的存在。函数逻辑版本在文本上更短，概念上更简单。例如，生成器和测试器在功能上嵌套并延迟执行，并且没有簿记和控制数据结构。有助于这种简单性并且在函数或逻辑程序中不可用的关键因素是：（1）非确定性，例如， 操作置换计算其自变量的许多置换之一，（2）语义统一，例如，约束U++V=置换Xs中的变量 如果可能的话，昂托伊3满足方程，以及（3）函数反演，即，从结果中计算函数的某个参数的值的可能性，例如，表达式-++[Y1]++K++[Y2]++ -被用于惰性地和非确定性地提取y，从列表中提取子列表，而不是将它们连接起来。函数逻辑程序的表达能力的增加对它们的执行提出了更高的要求。这些需求涉及计算的两个具体方面：（1）现代函数逻辑程序主要通过窄化来执行，窄化是一种将普通函数求值和解析两者都推广的计算;（2）建模函数逻辑程序的TRS类我们的初始示例包括诸如置换的非确定性操作和诸如U、V和K的额外变量。在本文中，我讨论了一些类的TRS提出的功能逻辑编程和合适的评价策略，这些类。第2节回顾了作为函数逻辑程序计算的缩窄第3节定义和比较各种基本类的TRS提出的功能逻辑程序建模，并为每一类，提出了一个评估策略。第4节简要讨论了对前面的类的一些扩展和相关问题。第五节是结论。2缩小本节简要回顾了项重写[8，11，17]和函数逻辑编程[13]的基本概念。重写系统是一对，R=h; R i，其中是签名，R是重写规则的集合。 签名是多排序的 ，并被划分为构造器符号的集合C和定义的操作或函数的集合F。Term（[X]）是在变量的可数集合X上构造的项的集合。 项（C[X]）是值的集合，即， 在C和X上构造的项的集合。Var（t）是出现在项t中的变量的集合。模式是f（t 1;：;t n），n>0形式的项，其中f2F和t 1;：;t n是值。无条件重写规则是一对l！r，其中l是线性模式，r是项。传统上，要求Var（r）Var（l）。这里不强加这个条件，因为它对于函数逻辑计算似乎是不必要的限制一个无条件的TRS，R，定义了 一个重写关系！按下 列 条件成 交！如果s 中 存在位置p，则重写规则R=l！带有新变量和替换的r其中SJP =（l）和t= s [（r）] p。 实例化的左侧（l）重写规则l！ R被称为redex（红色可表达）。 给定一个亲戚！，！还有！表示它的传递闭包和传递闭包，reexive关闭，分别。条件重写规则的形式为l！r：c，其中L和r如在无条件情况下那样定义，c是基本等式约束的序列，即，形式为t = u的项对。的定义+昂托伊4条件TRS的重写关系比非条件TRS的重写关系复杂得多。经典的条件重写方法在[9]中讨论。一个左线性的、有条件的、基于构造器的TRS是一个很好的函数或逻辑程序模型。计算是（用）以运算为根的项最终应用于值.例2.1在编程语言中，值由数据类型声明引入，例如：数据bool =真|虚假数据列表a =[]|[a|表a]并且操作由诸如例1.1的重写规则来定义。标识符true和false是常见的布尔常量。[]（空列表）和[|]（非空列表）是多态类型列表的构造函数。Identi era是一个类型变量，范围覆盖所有类型。值或数据项是包含变量、常量和数据构造函数的格式良好的表达式，例如，[x，y]表示[x| [y| []。函数逻辑语言的基本计算正在缩小。 项s通过替换缩小到t，记为s;t，如果是幂等构造函数替换使得（s）！ t. 一个项s使得（s）是一个redex被称为narrex（可叙述表达式）。传统上，要求窄化步骤的替换是narrex和规则的左手侧的最一般的单位。这里不强加这个条件，因为使用大多数一般单位缩小可能是次优的[6]。项s的计算或求值是一个窄化推导s = t 0;1：;nt n= t，其中t是一个值。代入1的结果被称为计算的答案，t被称为s的计算值。计算缩小步骤，特别是叙述及其替换，是策略的任务。例2.2下面的重写规则定义了链表的串联和严格相等。 “操作&“是约束连接。 相同的成功表示已解决的约束。本文明确地表示了只使用重写规则来定义计算，但只要有适当的语法，它就可以从程序中消除在实践中，严格相等是函数逻辑语言运行时系统的内置操作[]++ X-> XR1[X| Y]++ Z -> [X |Y++Z]R2[]=[]-> success R3[X| Xs]=[Y| Ys]->X=Y&Xs=YsR4成功& X-> X R5例1.1的程序的执行需要解约束，如U++V=[2，3，4]，这是通过缩小来解决的一个自由的变量-昂托伊5;;able可以具有不同的实例化。因此，包含自由变量的表达式下面是解决约束的几个可能的步骤序列之一的初始部分，即，将其缩小到成功，并在此过程中实例化变量U和V。在一个步骤中应用的规则和替换都显示在reduce的右边：U++V=[2，3，4];[U 1|Us++V]=[2，3，4]R2;fU7！[U 1|Us]g; U1=2&Us++V=[3，4]R4;fg; 成功&Us++V=[3，4]Ri;fU17！2g; Us++V=[3，4]R5;fg.其中U1和Us是新变量，Ri表示整数类型严格相等的某种规则，这里没有显示。 这个解决方案将变量U实例化到一个头为2的列表中。收缩策略是函数逻辑编程语言的基础和实现的关键组成部分它的任务是计算必须应用于项的一步或多步。在基于构造器的TRS中，项t的缩窄步骤由t的不可变位置p标识，重写规则l！ r，和幂等构造函数替换su chthatt;p; l！r;sis=（t[r]p）. 例如，一个窄化策略是一个映射，它取一个项t，并产生一组形式为hp; l的三元组！r;我解释为前面定义的缩小步骤。例2.3继续例2.2，应用于约束U++V=[2，3，4]的好的收缩策略计算以下两个步骤：h1;R1;fU7！ []gi和h1;R2;fU7！[U 1|Us]gi. 第一步得到的解为U=[]和V=[2，3，4]。第二步，已经在前面介绍过了。一个对函数逻辑编程有用的收缩策略必须是合理的、完整的和有效的。在下面的定义中，t和u表示项，讨论的主题。战略是健全的，u意味着（t）！联合 一战略已完成，（t）！u意味着存在替换6使得tu 0与u 06 u.直觉上，无论是健全性和当一个导数的初始项是一个包含自由变量出现的等式约束时，在这种情况下，策略的可靠性保证了由该策略计算的变量的任何实例化都是方程的解，而完备性保证了对于方程的任何解，该策略计算出另一个解，该解至少是一般的。卓越是一种更难以捉摸的属性。有两个因素影响策略的效率：（1）不应该计算不必要的步骤，（2）应该在没有不必要的资源的情况下计算步骤。在这两种说法中，“不必要的”的确切含义最多是难以形式化的因素（1）更多值，并且所有收缩派生都由该策略计算昂托伊6与战略的理论相关，而因素（2）与战略的实施更相关，尽管这些关系的边界是模糊的。一个策略的有效性与它的完整性有些矛盾。确保完备性的一种简单方法是计算一个项的所有可能的收缩步骤，但在大多数情况下，这是非常不必要的，因为其中许多步骤是不必要的。类似于重写，不同的缩窄策略已被提出用于不同类别的TRS。一些有效的缩窄策略是相应重写策略的扩展，而其他缩窄策略是专门为函数逻辑编程感兴趣的TRS类开发的，并且不是源于以前的重写策略。其中一些类及其策略是下一节的主题3TRS类别函数逻辑语言设计中的一个关键决策是选择TRS类来建模程序。原则上，概括性是非常可取的，因为它有助于语言的表达能力。在实践中，极端的权力或最大的普遍性并不总是一种优势。使用“非结构化”重写规则有两个相互关联的缺点：对于程序员来说，它变得更难推理程序的属性;对于实现者来说，它变得更难有效地实现语言。由于这些原因，不同类别的TRS可能适合于功能逻辑计算已被广泛研究。图1给出了一些主要类的包含图。图中考虑的所有类都是基于构造函数的。重写规则定义一个操作与构造函数纪律[20]隐式定义一个相应的函数在代数数据类型，如例2.1。大多数情况下，这非常适合编程，特别是当数据类型是抽象的时候。本节的讨论仅限于一阶计算，尽管高阶函数在函数编程中是必不可少的，因此函数逻辑编程也是必不可少的。下一节将放宽这一限制。本节的讨论也仅限于无条件的TRS。基于构造器的TRS可以通过既保留值又不损失效率或通用性的转换而转换为无条件TRS。这也将在下一节中讨论。3.1归纳顺序TRS图1中最小的类是感应顺序TRS。这些是基于构造器的TRS的强顺序组件[14]。强顺序TRS的最佳重写推导由众所周知的按需调用策略执行[16]。在此类中，最优性是这样一种属性，即在昂托伊7CBOISWO是图1.一、重写系统建模功能逻辑程序的包含图标记为CB的外部区域表示基于构造器的重写系统。标记为IS的最小最暗区域表示感应顺序重写系统。这些是弱正交（标记为WO）和重叠的归纳顺序重写系统（标记为OIS）的交集。意味着除非执行该步骤，否则无法达到由推导计算的值（如果存在）。Needed narrowing[6]是该策略的保守扩展，即，由所需收缩执行的重写派生是按需调用派生。此外，需要缩小关于计算答案的第二最优性结果。缩小是不确定的，因此一个术语可能有几个不同的派生，每个派生计算一个替换和一个值。由这些推导计算的替换是成对不相交的[6，定义15]。这意味着计算值的每个所需的收缩派生都是需要的，因为由一个派生计算的替换不能由任何其他派生获得归纳顺序TRS最初是通过定义树的概念来表征的[2]。由于定义树经常使用为了定义和实现基于构造函数的TRS的几个子类的收缩策略，我想起了这个概念。运算f的定义树是线性模式的有限的非空集合T，其部分地通过包含排序，并且具有以下属性直到变量的重命名：[叶子属性] T的最大元素，称为叶子，是定义f的规则的所有且唯一的左手边的变体。非最大元素被称为分支.[根属性] T的最小元素，称为根，是f（X 1;：; X n），其中X 1;：;X n是新鲜的，不同的变量。[parent property]如果T的模式不同于根，则存在在T中，一个唯一的模式0严格地在前，使得不存在其他模式昂托伊8N、1模式严格介于和0的情况。0被称为父对象作为0的孩子。[归纳性质]同一父代的所有子代仅在其父代的变量的位置（称为归纳）处彼此例3.1考虑一个操作take，它返回一个列表的前x。为了便于讨论，自然数用皮亚诺符号表示数据nat = 0 |s nattake 0-->[]take（sN） []->[]take（sN）[X| Xs]->[X|需要NX秒]例2.2中定义的操作++和刚刚定义的操作take的定义树如下所示。线连接父子关系中的图案。父类的归纳变量被装箱。叶子是规则左侧的变体。采取X、、、++ Y、、、、、、、、take0Xtake（sN1）、、、[]++Y[X 1]|Xs]++Y、、、、take（sN1）[]take（sN1）[X1|Xs]一个TRS是归纳顺序的，它的所有操作都有一个定义树。所需的缩窄是通过定义树来定义的，定义树用作nite状态自动机来计算缩窄步骤。我在一个例子中给出了这种计算的非正式说明正式定义见[6，Def. 13]。例3.2Needed窄化计算以take为根的项t的步长，即，t=取n x，如下所示。 设是take的定义树中与t一致的元素，设是unier。如果是叶子，那么t是纳勒克斯，是步骤的替代。如果是一个分支，p是它的归纳变量的位置，那么tjp是由某种运算f根的。使用f的定义树，该策略计算所需的步骤（t j p），比如h q;l！r;i.然后，h pq; l！r;t;i是t的必要步骤。为了使这一切更具体，假设t = takeN（[1]++[2]），其中N是自由变量。 术语tunes既取0 X，这是一片叶子，又取（sN1）X，其中hi ch是一片麸皮。因此，needednarr owing计算如下所示的两个步骤。每个步骤都显示了它的替换。takeN（[1]++[2]）;fN7！0g[]takeN（[1]++[2]）;fN7！（s N）gtake（sN1）[1| []++[2]]注意到第二步的替换不是最普遍的。这XX昂托伊9需要缩小的特点是与以前提出的战略的重大偏离。 除非N被设置为（sN1），否则该步骤可能是无用的，例如，然后是将N实例化为0的步骤。3.2弱正交TRS弱正交TRS是归纳序列TRS的一个真超类.该类中的重写规则可以重叠，但前提是它们对应的关键对是平凡的（语法上相等）。规则的左边是模式，因此它们只能在根处重叠。因此，基于弱正交构造函数的TRS几乎是正交的。这个类中的计算有时被称为并行的，因此实现，尽管这个类也允许顺序规范化重写策略。基于弱正交构造函数的TRS的最佳重写推导是通过重复收缩必要集合的所有赎回来执行的[22]。这个概念推广了nedex redex的概念，它在这个类中被定义。在这个类中，最优性是这样的属性，即由派生计算的值（如果存在）不能达到，除非在必要集合中的一个redex被收缩。一般来说，没有有效的程序是已知的，以确定这个redex。例3.3在这个类中，一个象征性的非归纳顺序运算是parallel-or，由以下规则定义：或true--> true R6或-true-> true R7或false false-> false R8项or（或true u）（或v true）不需要redex，不管项u和v。弱需要缩窄[5]是[22]中定义的策略的保守扩展。 该策略也是通过定义树来制定的。定义弱正交TRS中的操作的重写规则可以被划分为归纳顺序子集，即，存在一个定义树的子集。对于例3.3的规则，一个这样的划分是fR6;R8g]fR7 g。然后，通过计算分区的每个元素所需的redex来获得必要的redex集合。在[2]中形式化的这种重写策略等价于[22]。它对窄化的扩展是直接的，但是narrex的必要集合的性质不同于redex的必要集合的性质。由重写规则的分区的元素计算的缩小步骤可以具有与另一步骤的替换不兼容的替换，和/或步骤的位置可以不与该另一步骤不相交。对于重写步骤，这两种情况都不会发生。在[5]中讨论了处理这些条件的几个相关的窄化策略，但没有一个声称[22]的强最优性结果。然而，所有这些策略对于重写推导都是最佳的，因为它们计算了昂托伊10与[22]相同。3.3重叠归纳顺序TRS重叠归纳序贯TRS是归纳序贯TRS的一个真超类它们与弱正交TRS是不可比拟的。重叠归纳顺序TRS中的重写规则可以重叠，但仅当它们的左手边对变量的重命名取模相等时。 与弱正交TRS相比，重叠重写规则的右侧没有限制。这类计算有时被称为非确定性。例3.4下面的操作定义了一个字母表（数字）和由给定字母表参数化的（非空）正则表达式 在这种情况下，（Meta）符号\|“de nesalternative right-hand sides of a same left-hand side.数字->“0”|“一”|......这是什么？| “9”regexpX->X| “（“++regexpX ++“）”| 正则表达式X ++正则表达式X| 正则表达式X ++“*”| 正则表达式X ++“|“++ regexpX操作regexp的定义与正则表达式的形式定义非常相似。非确定性操作有助于语言的表达能力。例如，要识别一个字符串，比如s，是否表示一个在数 字 字 母 表 上 的 格 式 良 好 的 正 则 表 达 式 ， 它 只 需 要 计 算（regexdigit=s）。出于解析的目的，最好有一个不太模糊的定义，同时也考虑到通常的运算符优先级，但是这些方面与当前的讨论无关重叠感应顺序TRS的评价策略是INS [3]。该策略自其引入以来就被制定用于缩小计算，即，它并不源自较早的重写策略。在这个类中，每一个可以缩小到一个值的术语都需要一个narrex。由于可能存在多个具有相同左侧的重写规则，因此一个narrex可能有多个替换。在此类中，最优性是INS推导的每一步都需要的属性，因为推导计算的值（如果存在）无法达到，除非Narrex是一致的。然而，并不是每一个所需的narrex的更换是必要的，因此INS使所需的步骤模非确定性的选择。一般来说，没有有效的程序来确定需要选择哪些替代品。非确定性操作需要重新思考一些语义方面的评估和策略。例如，“操作”的含义被推广到可连接性，即，t = u意味着t和u具有公共值昂托伊11|可能是众多人中的一个另一个相关的问题是派生的步骤，其中值最终绑定到变量。这是一个微妙的点，因为绑定到变量的值不需要在这一步计算。有两个实例可以说明这个问题。皇后运算，在介绍中定义，有一个变量Y出现三次的规则.变量Y最初被绑定到置换X，其最终可能被简化为许多值之一。用置换X来代替每次出现的Y并独立地评估每次出现的Y显然是不正确的。皇后操作返回的发生值可能与使用操作捕获进行安全性测试的值不同。在这种情况下，预期的行为（称为调用时选择语义）是将相同的值绑定到所有出现的Y。本节中定义的操作regexp具有两次出现变量X的规则。 变量X最初绑定到一个项，例如， 一个数字，它最终可能被简化为给定字母表的一个字符串。然而，在这种情况下，意图是相反的。除非绑定到digit的X的出现彼此独立地计算，否则不会生成某些正则表达式。在这种情况下，预期的行为（称为需要时选择语义）不是将相同的值绑定到X的所有出现。在每种情况下，预期的行为都取决于程序。函数逻辑语言应该允许程序员在程序中编码适当的语义.用于非确定性计算的策略应该具有有用的属性，例如，可靠性和完整性，这两个语义。3.4基于构造器的TRS基于构造器的TRS是已被提出用于建模函数逻辑程序的最大类。它们是前面讨论过的所有其他类的适当超类。规则左侧的重叠是不受限制的，尽管在基于构造器的TRS中，它可能只发生在根处。重叠规则的右侧没有施加任何特定的限制。例3.5下面的操作置换定义是N皇后程序中提出的另一种操作插入不属于前面讨论的任何TRS类。permute [] ->[]置换[X| Xs]->insertX（permuteXs）insertXY s->[X|是的]插入X[Y| Ys]->[Y|插入XY s]在[18]中给出了此类早期缩小策略。该策略是对[1]中提出的重写策略的缩小的推广。这两种策略的完整性尚不清楚。昂托伊12一个像基于构造函数的TRS一样大的类的潜在困难最外层的重写策略不是标准化的[4]，因此最外层的收缩策略是不完整的。在前面的章节中讨论的所有策略都是最外层的，这是一个简化计算推理的条件，因此证明了它们的属性，例如完备性和最优性。例如，考虑t=insertu v的求值。我们无法判断是否需要t的位置2。事实上，必须计算子项v以应用插入的一个重写规则，但不应用另一个重写规则。[1]和[18]都是需求驱动的战略，而不是需要的战略，非正式地意味着以下内容。 如果存在潜在地适用于t的规则R要求评估，则评估项t的子项v的v。然而，对于其中t发生的整个计算来说，将R应用于t可能不是必需的。需求驱动的策略激发了人们对其完整性的信心，因为它们试图为将每一个可能的重写规则应用于术语创造条件。当一项规则对一个术语的适用和（或）为适用一项规则而对一个子术语的评价是不必要的时候，这些规则也可能是相当不恰当的最近，已经提出了一种转换方法[4]，用于基于构造器的TRS中的函数逻辑计算。该方法将基于构造器的TRS R转换为重叠归纳序列TRSR0。R0的计算是用惯性导航系统完成的，它是可靠、完整和有效的.从下面的意义上说，这种转变本身是健全和完整的。转换将新的操作符号添加到R 0的签名中，但不添加新的构造函数. 签名的变化通常会创建新的步骤和新的范式。然而，在R的签名上建立的任何项都被R和R0 的 规 则 评 估为 相 同 的 值 集。INS执行的计算对于R0的重写规则是最优的，但对于R的重写规则不一定是最优的。4相关问题前几节几乎完全忽略了与泛函逻辑计算相关的一些重要问题。我将在本节中简要讨论这些问题。与本文其余部分一样，重点是战略。前面讨论的TRS类都是无条件的。众所周知的最外层公平重写策略，其针对几乎正交的TRS [20]进行归一化，也针对条件几乎正交的TRS [9]进行归一化。对于基于构造器的TRS，前面给出的关于评估策略的结果被扩展到条件情况下，几乎不需要排序。第3节中讨论的策略直接或间接地基于定义树。定义树只关心重写规则的左边。因此，通过定义树定义的策略在某种程度上独立于TRS是否是条件的。一种利用这种考虑的方法将原始的条件TRS昂托伊13转换成目标无条件的，而不改变重写规则的左手边。通过这种方式，将针对目标TRS证明的结果转移到原始TRS。这种转换方法在[4]中正式化。简而言之，通过引入条件操作，条件重写规则的条件被移动到右侧。更准确地说，条件重写规则的形式是：转化为：l！r：t1= u1;：;tn=unl！如果t1=u1;：;tn=un则 r其中，如所期望的，当其第一参数成功时，ifthen二进制操作返回其第二参数。 这种新操作的引入通常会创建新步骤和新范式，但不会创建新值。使用转换后的重写规则对值的计算基本上保持相同。关于函数式逻辑编程的第二个相关问题涉及高阶计算，这是函数式编程的基石。高阶函数，即， 将其他函数作为参数的函数，通过将计算参数化到其他计算之上，有助于语言的表达能力。一个典型的例子是函数映射，它将某个函数应用于列表的所有元素地图-[] ->[]映射F[X|Xs]->[FX|[地图FXs]与前面的例子不同的是，map的rst参数不是计算值，而是计算操作。高阶重写的理论不如（一阶）重写的理论先进，因此对于高阶TRS的重写策略知之甚少然而，如果在高阶重写规则上施加附加条件（完全扩展），则对于几乎正交的TRS[20]进行归一化的公知的最外层公平重写策略也对于弱正交的高阶TRS进行归一化[23]。高阶窄化理论甚至更类似于一阶情况，已经提出了几类高阶TRS用于高阶函数逻辑计算，例如，SFL程序[12]，应用性TRS [19]和高阶归纳顺序TRS [15]。不同的方法已被采用，以证明性质的功能逻辑计算在这些类。SFL程序中的计算通过转换映射到一阶计算，该转换扩展到缩小高阶逻辑计算的众所周知的转换[24]。应用TRS中的计算由演算执行，该演算使得推理步骤的粒度比缩小步骤更小。高阶归纳顺序TRS中的计算使用定义树的泛化来执行。函数逻辑计算和函数计算之间的一个重要区别是，窄化能够合成函数。在昂托伊14在许多情况下，这种函数将是顶级计算的结果。例如，求解约束：地图 X [0，1，2]=[2，3，4]将返回计算出的答案fX7！s=s g，其中s是例3.1中定义的构造函数。目前大多数函数式语言的实现都不具备处理这种可能性的能力。当计算的结果是一个函数时，函数式语言会这样报告，但不会以任何表达形式标识哪个函数。这种设计选择似乎表明高阶结果并不是特别有趣，至少在函数式编程中是这样。缩小范围大大扩展了功能评估的能力，但计算高阶结果的可行性和实用性尚未明确确立。在其他情况下，出于同样的原因，变换方法也被提出用于高阶计算。简而言之，具有部分应用的符号的术语被转换为使用为此目的引入的新符号构建的术语。变换项中的每个符号都被完全应用。最初的想法[24]是为逻辑编程中的函数求值而制定的，[12]将其推广到窄化，[7]通过保留类型信息来保留这些方法是有趣的，因为它们扩展了非平凡的结果证明了一阶策略的高阶情况下，一个温和的概念eort。5结论本文概述了功能逻辑程序的评价策略程序是（被视为）基于构造器的TRS，评估或计算是重写或缩小值的派生|构造函数范式。基于构造器的TRS是程序的良好模型，因为它们使用代数数据类型定义的函数进行计算非基于构造器的TRS很少被用作程序。我提出了基于构造器的TRS的四个子类。每个子类都捕获了计算的一些有趣的方面，例如并行性或非确定性。不同类中的计算最好通过不同的策略来完成。对于每个类，我都提供了一个缩小策略，在某些情况下，还提供了它所源自的重写策略。当呈现时，重写策略是标准化的，即，它计算一个项的值，如果它存在的话。此外，缩小战略是健全和完整的，即，当用于求解方程时，它只计算方程的所有解。所有这些策略在不同程度上也具有理论上的有效性。毫不奇怪，随着班级规模的扩大，关于这些班级使用的策略的有效性的说法变得越来越弱。最后，我考虑了基于构造器的TRS的两个扩展，昂托伊15对编程很重要：条件和高阶重写规则。这些扩展的评估策略并不像普通情况下那么发达。从扩展TRS到普通TRS的转换使得可以使用前面提出的策略，同时保留许多最理想的属性。确认我要感谢Bernhard Gramlich和Salvador Lucas Alba邀请我为2001年5月在荷兰乌得勒支举行的重写和编程中的缩减策略国际研讨会撰写这篇论文。引用[1] S. 安托伊 逻辑程序设计中的非确定性和惰性求值在T. P. Clement和K.- K. Lau，编辑，Logic Programming Synthesis andTransformation（LOPSTR'91），第318页，曼彻斯特，英国，1991年7月。史普林格出版社[2] S. 安 托 伊 定 义 树 。 在 第 四 届 国 际 会 议 上 ， Conf. on Algebras andLogicProgramming，第143页。Springer LNCS 632，1992年。[3] S.安托伊最佳非确定性函数逻辑计算。在第六届代数和逻辑编程国际会议（ALP'97）的论文集，第16页{30. Springer LNCS 1298，1997年。[4] S.安托伊基于构造函数的条件收缩。在Proc. of the 3rd International ACMSIGPLAN Conference on Principles and Practice of Declarative Programming（PPDP'01），pages 199{205，Florence，Italy，Sept. 2001.[5] S.安图瓦河Echahed和M.哈纳斯函数逻辑语言的并行求值策略。在第14届逻辑编程国际会议（ICLP'97）的论文集，第138页{152. MIT Press，1997.[6] S.安图瓦河Echahed和M.哈纳斯一个必要的缩小战略。Journal of theACM，47（4）：776{822，July 2000.[7] S. Antoy和A.托马赫没有高阶策略的类型化高阶收缩。在第四届FujiInternationalSymposiumonFunctionalandLogicProgramming（FLOPS'99），卷1722，页335{350，Tsukuba，Japan，111999. Springer LNCS。[8] F. Baader和T.尼普科重写和所有这一切。剑桥大学出版社，1998年。[9] J. A. Bergstra和J. W.克洛普条件重写规则：Conuence和Termination。Journal of Computer and System Sciences，32（3）：323{362，1986.昂托伊16[10] R. Bird和P.瓦德勒函数式编程入门。Prentice Hall，纽约州纽约市，1988年。[11] N. Dershowitz和J. Jouannaud。重写系统。在J. van Leeuwen，编辑，HandbookofTheoreticalComputerScienceB ： FormalMethodsandSemantics，第6章，第243页{320。北荷兰，阿姆斯特丹，1990年。[12] J. C.冈萨雷斯-莫雷诺Warren的HO到FO翻译的正确性证明。在Proc. GULP'93，第569页{585，Gizzeria Lido，IT，Oct. 一九九三年[13] M. 哈纳斯功能集成到逻辑编程：从理论到实践。逻辑程序设计杂志，1920：583{628，1994。[14] M. Hanus，S. Lucas和A.米德尔多普强顺序和归纳顺序项重写系统。信息处理快报，67（1）：1{8，1998.[15] M. Hanus和C.普雷霍弗用定义树进行高阶窄化。在Proc.7th InternationalConference on Rewriting Techniques and Applications（RTA'96），第138页{152. Springer LNCS 1103，1996年。[16] G. Huet和J. - J·莱维。正交项重写系统中的计算。在J. - L. Lassez和G.Plotkin，编辑，计算逻辑：纪念Alan Robinson的论文，第395页。麻省理工学院出版社，马萨诸塞州剑桥，1991年。[17] J. W.克洛普术语重写系统。In S. Abramsky，D. Gabbay和T. Maibaum，编辑，Handbook of Logic in Computer Science，第二卷，第1页{112.牛津大学出版社，1992年。[18] R. Loogen，F. L opez Fraguas和M. Rodr guez Artalejo 一个需求驱动的懒惰 缩 小 计 算 策 略 。 在 Proc.5th International Symposium on ProgrammingLanguage Implementation and Logic Programming （ PLILP'93 ） 中 ， 第184{200}页。Springer LNCS 714，1993年。[19] K. Nakahara，A. Middeldorp和T.艾达 高阶函数逻辑程序设计的完整窄化演算。在Proc.7th International Symposium on Programming Languages，Implementations ， Logics and Programs （ PLILP'95 ） 中 ， 第 97 页 {114.Springer LNCS 982，1995年。[20] M. J·奥唐纳用方程描述的系统中的计算。 Springer LNCS 58，1977年。[21] R. A.奥基夫 Prolog的技巧 麻省理工学院出版社，马萨诸塞州剑桥，1990年。[22] R. C. 我和塞卡诉拉马克里什南方程式逻辑中的程序设计：超越强顺序性。信息与计算，104（1）：78{109，1993。[23] F.范·拉姆斯东克。高阶重写在第10届重写技术和应用国际会议（RTA'99）的会议记录中，第220页{239.Springer LNCS 1631，99.昂托伊17[24] D. H. D. 沃 伦 PROTECH 的 高 阶 扩 展 ： 它 们 是 必 要 的 吗 ？ 在 MachineIntelligence 10，第441页{454，1982。