通过归纳构建函数性质（例子）的技术

理论计算机科学电子笔记174（2007）49-63www.elsevier.com/locate/entcs通过句法规则检测从例题中归纳构式系统Emanuel Kitzelmanna，1，3Ute Schmida，2，3班贝格大学信息系统与应用计算机科学系96045 Bamberg，德国摘要我们提出了一种技术，诱导函数程序从少数，精心挑选的输入/输出的例子（I/O的例子）。自动程序或算法归纳的潜在应用是使最终用户能够创建他们自己的简单程序，协助专业程序员，或者完全自动发明新的和有效的算法。在我们的方法中，函数程序表示为构造函数项重写系统（CS）包含递归规则。目标函数的I/O示例是一组成对的项（F（ii），oi），这意味着F（ii）-表示函数F对输入ii的应用-被实现函数F的CS重写为oi。归纳是基于检测示例术语之间的句法在本文中，我们提出的理论结果，并描述了一个算法，诱导任意签名/数据类型上的CS，其中包含一个由任意数量的规则定义的函数，每个规则中包含任意数量的非嵌套递归调用。此外，我们提出了基于原型实现的实证结果。关键词：归纳程序综合，基于规则的编程，函数式编程，构造器系统1引言从输入/输出示例（I/O示例）自动归纳递归声明程序是自六十年代以来的一个活跃研究领域（参见[1]经典方法，[3]归纳逻辑编程领域的系统，[5]最近的研究）。存在两种处理程序的归纳合成的一般方法(i)在生成和测试方法中（例如， ADATE系统[10]），1电子邮件：emanuel. wiai.uni-bamberg.de2电子邮件：ute. wiai.uni-bamberg.de3我们要感谢匿名评论者，他们的评论有助于改进论文。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.11.01550E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49一个定义的类被枚举，然后针对给定的示例进行测试。(ii)在分析方法中，一个定义类的程序是通过在给定的例子中检测递归来导出的，然后将其推广到递归定义的函数。生成和测试方法适用于非常一般的程序类，因为在枚举程序中没有主要的困难它们自然地促进了在诱导程序中使用预定义函数（背景知识）此外，在要实现的目标函数的示例方面的规范可以是极其声明性的，例如，可以由示例输入和评估函数组成。另一方面，生成和测试方法是搜索密集型的，因此很耗时。这些特性使他们有资格发明新的和有效的算法（cp。[10]）。分析方法有更多的限制程序类，因为通过分析实例导出程序比枚举程序更复杂。出于同样的原因，促进背景知识的使用也更加复杂此外，对于基于评估函数的示例规范，示例分析是不可能的，而是需要输入/输出示例（I/O示例）。另一方面，分析使搜索最小化，并使这些方法更快。这些特征使最终用户编程（例如，见[12]）或辅助系统的分析方法合格。由于本文中提出的技术是分析性的，我们在下面集中讨论分析方法。一个经典的和非经典的分析方法是由萨默斯[13]开发的Summers的系统介绍了函数式Lisp程序。它分两步进行：在第一步中，为每个I/O示例计算用于区分输入的跟踪和谓词。通过将迹和谓词集成到条件表达式中，作为第一合成步骤的结果，构造了计算所有I/O示例的非递归程序在第二步中，分别在迹和谓词之间搜索谓词。然后将所找到的结果归纳推广，并以所得递归程序的形式表示。Summers的方法能够归纳出一个函数定义，其主体由任意数量的基本情况的条件和恰好一个包含恰好一个递归调用的递归情况组成。参数仅限于数据类型S表达式（Lisp中的通用数据类型），并且I/O示例必须线性排序。一个有趣的特征是用于在需要时自动引入附加参数的特殊启发式，例如，用于列表反转的累加器变量放松非常简单的程序模式的Summers方法的扩展它也仅限于S-表达式类型的参数和线性递归。LeBlanc在[8]中描述了BMWk算法在项重写系统框架中的重新公式化和推广。这种推广克服了S表达式作为唯一可用数据类型的限制。此外，它克服了对线性递归的限制，但要求用户提供要归纳的程序的递归递归规则的模式和递归调用的参数。LeBlanc的概括并没有得到实施。最近的一种方法的功能性程序归纳的启发，这些经典的ap-E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4951在[6]中描述了在术语重写框架内的方法和公式化。对先前方法的扩展是子功能/子程序和另外需要的参数被自动地并且以系统的方式推断所有这些函数分析两步法都局限于小的固定的原始函数集（用于相应数据类型的基本构造函数和选择器函数以及用于测试构造函数是否是原子的谓词，例如，空列表），其中可以组成诱导程序。也就是说，它们不能处理额外提供的特定于问题的函数作为背景知识来诱导更复杂的程序。特别是，测试原子表达式作为唯一使用的谓词限制类的诱导程序的程序结构问题。例如，反转列表就属于这一类，但不包括排序列表，因为对于排序列表，需要一个谓词来比较两个元素的顺序。此外，所描述的系统的共同之处在于，所提供的I/O示例可能不是从目标函数的图中任意选择的，而是必须是关于底层数据类型的归纳结构的第一个另一个研究方向是归纳逻辑编程（ILP）领域。虽然ILP专注于非递归概念学习问题，但在ILP领域也有关于归纳数据类型的递归逻辑程序的研究（见[3]）。大多数专门系统都是分析方法。与经典的函数方法相比，它们中的一些可以处理背景知识，特别是，它们中的一些不限于结构问题。两个相对较新的递归逻辑程序归纳的ILP方法是DIALOGS-II [14]和Rao在[11]中描述的（未实现的）方法。这两种方法都允许一个关系的任意数量的基本情况和递归情况，以及一个主体中的多个递归调用此外，这两个系统都促进了背景知识的使用这两种方法都可以推断出额外的谓词和参数，但这种能力仅限于DIALOGS-II归纳系统中的特定模式。此外，用户必须选择要使用的模式。DIALOGS-II仅限于一些预定义的数据类型，如列表和自然数。Rao的方法被限制为分解关于其递归结构的输入，例如，一个列表只能分解为前k个元素和其余的列表。相反，DIALOGS-II可以将一个列表分解为两个等长的列表。用户必须从一组预定义的分解中进行选择。这两种方法都仅限于一个递归参数，即，一个参数必须在每个递归调用中减少，并在基本情况下进行检查。本文所描述的分析和功能的方法表示I/O的例子，以及作为构造函数重写系统（CSs）的通用模型，而不是使用特定的编程语言诱导与DIALOGS-II相比，它更通用，因为诱导程序不限于特定的预定义数据类型，例如，列表或数字，但I/O示例可以定义为任意有限签名，然后用于诱导程序。递归的输入和参数项的分解52E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49调用是自动推断的，但与Rao的方法一样，它对分解的限制是尊重相应数据类型的内部归纳结构。它比其他两种方法更通用，因为递归参数的数量不限于一个。与DIALOGS-II和Rao的方法相反，2预赛我们将在本节中介绍术语重写系统并定义一些数据类型。2.1条款和条件在一个有限签名上的（有限）项集合和一个与中的函数符号不相交的变量的可数无限集合V用T（，V）表示没有变量的项称为基本项。一个项t称为线性项i，每个变量在t中只出现一次。一个项可以被看作是一个有限的、有标签的、有序的树，如下所示：（i）每个变量或常数对应于一个树，该树仅由一个分别由变量或常数标记的节点组成，以及（ii）项f（t1，.）.. .. 项t中的位置是一个正整数序列，表示从t的树的根到它的一个节点的路径。根节点的位置是空序列，用表示。位置u处的子树/子项写为t|联合如果我们想说明一个项t在任何位置都包含一个子项s，我们写t=C[s]。C称为context。对于两项t、s和t的位置u，t[s]u表示用项s替换t在位置u处的子项的结果。置换是从变量到项的映射，σ：V→T（Σ，V）。一个代换σ：V→T（n，V）被推广到一个从T（n，V）到T（n，V）的映射，它也用σ表示，并用后缀表示;tσ是将σ应用于t中的所有变量的结果。将变量映射到变量的替换称为变量重命名。如果s=tσ，则s称为t的instance。 我们说t包含s，或者说t是s的推广。 我们也说s通过σ匹配t。给定两个项s1，s2和一个替换σ使得s1σ=s2σ，则我们说s1，s2是统一的，称之为s1和s2的σunier。我们将包含关系推广到项的集合，并说一个项的集合T包含另一个项的集合S，如果每个项s∈S被项t∈T包含。 给定一组术语，S={s，s，J，s，j，. . }，则存在包含S中所有项的线性项t并且其自身被包含S中的所有项的每个其他线性项所包含。项t被称为（S中的项的）最小一般线性推广（lglg）T（V，V）上的一个约简阶是T（V，V）上的一个良基阶，它（i）在替换下是闭的，即，如果t∈S且σ是任意替换，则tσ∈Sσ，以及（ii）在上下文下闭合，即，如果t∈S且C是任意E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4953context则C[t]→C[s]。2.2（构造函数）项重写系统项重写系统（TRS）是一个对（R，R），其中R是重写规则（或简称规则）l→r的有限集合，其中l，r∈T（R，V），l/∈V，并且Var（r）<$Var（l）。在下面我们只写一个TRS（R，R）的R。对于规则l→r，l称为规则的左手边（lhs），r称为规则的右手边（rhs）构造器系统（constructor system ，CS）是一个TRS，其中，可以将重写规则划分为定义的函数符号的集合F和构造器的集合C，使得每个重写规则的lhs具有形式F（t1，.，tn），其中F∈ F且t1，.，tn∈T（C，V）. 重写关系→R定义如下：项t根据R重写为s，写作t→Rsi ∈R中存在规则l→r，置换σ和上下文C，使得t=C[lσ]和s=C[rσ]。我们称lσredex和rσcontractum。反应-∗重写关系→R的传递闭包记为→R。 如果一个词不能如果它被重写，那么它就是正常的形式。无限的或无限多的序列∗重写步骤t0→Rt1→r···称为求导。我们称tit→Rs的s约化。如果所有这些都是不正常的形式，那么这些都被称为不正常的形式，我们不能→！ S.我们说t归一化为s。一个TRS被称为终止，如果没有无限派生，即，如果每一个推导都在无限次重写之后导致一个范式一个TRS称为连续约简，即每两个一项的约简有一个公共约简。如果一个TRS是连续的，则每一项至多有一个范式。一个TRS是左线性的，如果它的所有lhs是线性的。CS收敛的一个充分条件一个连续的CS构成一个函数程序：定义函数符号表示程序的定义函数。构造函数表示用于组成程序的预定义函数。考虑“程序调用”F（t 1，.，t，n），其归一化为s。我们称之为t1，... ...，tn）i =1，.，tn∈T（C，V）和s∈T（C，V）.2.3数据类型定义本文中的示例使用自然数、列表和二叉树数据类型。一个自然数可以是常数0，或者是一个表示自然数x的后继的项s（x）。列表可以是空列表[]，也可以是cons（x，xs），其中x是第一个元素，xs是其余的列表。 我们用[x]表示列表cons（x，xs）|xs]和列表cons（x1，cons（x2，. ，cons（xm，xs）···））乘以[x1，x2，. ，xm|xs]。 如果xs =[]，我们写[x1，x2，.，xm]。二叉树是一个由val（x）项表示的值x，或者是一个项树（l，val（x），r）（写作nl，val（x），rn），其中l，r分别是左子树和右子树，val（x）是根节点的值。3构造子系统我们定义了CS的子类，它可以由我们的算法在模式方面诱导。54E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）493.1扁平单功能CS可以归纳的构造器系统（CS）类的特征如下：每个规则具有以下形式F（p1，...，pn）→t对于一个固定的定义函数符号F，即，F={F}。因为t可以包含定义的函数符号，所以规则可以是递归的。对于递归规则，F（p1，...，pn）→ C [F（r1，.，rn）]（i）C可以包含定义的函数符号F的（进一步）出现，即，规则可以包含任意数量的递归调用，以及（ii）r1，.，rn∈T（C，V），即 递归调用是非嵌套的。 我们把与这个基本模式匹配的CS类称为单函数CS。我们称之为p1，... ...，rn），并且r1，..，rn递归项。我们用它唯一的定义函数符号F来表示一个单函数CS。我们要求（i）对于任何关于固定归约阶的递归调用，F（r）小于F（p），（ii）所有规则都是左线性的，(iii)没有两个LHSS统一。这些条件保证终止和继续。注3.1注意，我们不要求在一个单函数CS中的模式集是完整的（或穷举的），在这个意义上，T（C，V）中的所有项都被至少一个模式匹配。因此，可能存在包含定义的函数符号的特定输入的范式。导出的单函数CS的完备性依赖于给定的I/O示例。3.2平面单函数CS示例单函数CS类包含列表的几个标准函数，例如，Head，Tail，Append，Length，Last（返回最后一个元素），Init（返回给定的列表，不包括最后一个元素），TakeandDrop（只保留列表的前n个元素，并分别从列表中删除前n个元素），Zip（获取两个列表，并返回对应元素对的列表），Sum（获取自然数列表，并返回所有包含的数字之和），以及Reverse（通过使用累加器变量反转列表）。用于自然数上的函数的单函数CS的示例是Add、Sub和几个谓词，例如，奇数，偶数，=，≤.一个特殊的递归单函数CS子类是由属性向量定义的实例空间上的（非递归）分类器，这些属性向量是在机器学习领域中经典学习的。我们在本文中不考虑这样的分类器，因为我们对递归数据类型上的递归程序感兴趣。图1显示了单函数CS类的两个进一步的例子。DelZeros从列表中删除所有零，TreeRev反转二叉树。TreeRev是一个在单函数CS上的树递归的例子在第5节中，我们根据经验评估我们的归纳算法，用于一些提到的例子和一些其他例子。E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4955DelZeros（[]）→[]DelZeros（[0 |xs]）→DelZeros（xs）DelZeros（[s（x）|xs]）→ [s（x）|DelZeros（xs）]TreeRev（val（x））→val（x）TreeRev（n，val（x），r）→ nTreeRev（r），val（x），TreeRev（l）nFig. 1.两个CS示例，DelZeros和TreeRev不包含在单功能CS类中的CS的示例是Mult、Member（检查特定元素是否包含在列表中的谓词）或排序列表，因为这些功能中的每一个都需要子功能来实现，即，各个CS包含用于多于一个定义的函数符号的规则例如，在一个示例中，一个用于Mult的CS由用于Mult的规则和用于Add的规则组成，或者一个实现快速排序的CS由用于主函数的规则以及用于子函数Partition、Append和≤的规则组成。当然，我们可以认为这些子函数是预定义的，并将它们的符号定义为构造函数，使得相应主函数的CS仅由主函数组成。然后这些CS也属于单函数CS类，但它们不能通过这里提出的方法从仅包含第2.3节中介绍的基本构造器的I/O示例中导出，因为我们的方法直到现在还不能处理背景知识。只有在提供的示例输出已经由表示子函数的构造函数组成时，才能归纳这些CS。例如，在一个示例中，Mult可以从I/O示例（如（Mult（s2（0），s3（0）），Add（Add（0，s3（0）），s3（0）））中导出，但不能从I/O示例（如（Mult（s2（0），s3（0）），s6（0））中导出。3.3计算之间的规律性输入、模式和递归项各自是项的列表或向量为了更好的可读性，我们表示项t1，.，tn乘tn，即， 我们分别用in、pn和rn来表示输入、模式和递归项。对于项列表tn=t1，. ..，tnσ乘tnσ。我们将包含、匹配、unifies和最小一般线性推广（lglg）等项类似地转换为项列表。例如，在一个示例中，pn包含ini n存在一个替换σ使得in=pnσ（in用σ匹配pn）。 或者，例如，p，n是输入集合{i，n，i，n，. . }ip1是一个lglg，{i1，iJ，iJJ，.. . }，p2是{i2，iJ，iJ，.. . }等等。1122在Summers [13]的传统中，我们使用递归定义的函数和由这些函数处理的计算之间的关系，从假定为递归目标函数的计算的给定计算中归纳地推断递归定义如果F（in）通过σ与lhsF（pn）匹配一个递归规则，即，F（in）=F（pn）σ，则我们称递归56E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49JJJ1调用F（rn）σ，在该规则的实例化rhstσ中递归调用F（in）。tσ的子项列表rnσ=iJn再次是F的输入，并归一化为它们的输出oJ。下面的定理指出，对于输入in和相应的输出o，F（i n）的递归调用F（iJn）的输出o j作为o中的子项出现在相应递归调用的位置。本质上，递归规则在我们的方法是通过恢复定理：定理3.2设F是在一个输入上的一个单函数CS，out put，即， i1， .. . ，in， o∈T（C， V）andF（in）→！O. 设F（pn）→t为其中in匹配pn，并且令σ是对应的替换，即， in= pnσ.我们假设t至少包含一个递归调用。 令{F（rn），.，F（rn）}（k≥1）1K是所有不同的递归调用，发生在t和U1，. ，Uk递归调用的位置集 合，使得u ∈ Uji≠ t|u= F（rn）对于所有j ∈ {1，. ，k}。 让F（rn）σ→！oj，其中oj∈ T（C，V），对于所有j ∈ {1，. ，k}。 然后对于所有j ∈{1，. ，k}且任何u∈Uj保持o|u= 0j。证据F（in）= F（pn）σ根据规则F（pn）→t一步重写为tσ。 在tσ中，子项F（rn）σ出现在位置Uj处，其中j ∈ {1，. ，k}。 这些递归调用被规范化为o1，. ，或k。Q例如，设F为DelZeros-CS，如图1所示。 该CS仅采用一个参数，即，对于输入项、模式项和递归项，我们分别写i、p和r，而不是in、pn和rn 设i= [3，0，1]，则o= [3，1]成立。lhs被“程序调用”DelZeros（[3，0，1]）匹配的规则是第三个：DelZeros（[ s（x）|xs]）→ [s（x）|DelZeros（xs）]。相应的替换为σ={x<$→ 2，xs<$→ [0， 1]}。 该规则只有一个递归调用（k= 1），即在rhs中的位置2处的F（rn）=DelZeros（xs），即，U1={ 2}。DelZeros（[3，0，1]）的递归调用是DelZeros（xsσ）=DelZeros（[0，1]）在实例化的rhs中的位置它归一化为输出o1=[1]，这是o= [3，1]在位置2的子项。4归纳正确的平面单函数CS我们从本节所需的基本定义开始：定义4.1从T（C，V）n到T（C，V）的函数F的一组I/O-示例是由非递归规则组成的CSF，使得如果F（in）→o（o∈T（C，V））是I/O-示例，则F（i n）=o如果上下文不明确，我们使用索引并将示例CS写成FE而不是简单的F定义4.2由规则F（pn）→t组成的连续和终止CSF与相对湿度一致/完整/正确。a set of I/O-examplesFE iconsistent：forachI/O-exampleF（in）→oh olds：F（in）→！ F（in）→！Fs对于一项s/∈T（C，V）.完成：对于一个I/O-exampleF（in）→oh olds：F（in）→！F sfora terms∈E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4957T（C，V）.58E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49正确：CS既一致又完整。由于CS的规则是独立归纳的，我们需要定义单个规则的正确性：定义4.3对于模式pn，设F是包含I/O示例的CS-即，非递归规则-其输入由pn包含。设E是这些I/O示例的子集，并且C（E）是剩余规则，即，C（E）=F\E。具有模式pn的规则ρ称为正确的w.r.t.E和C（E）证明了在F中用ρ代替E所得到的CS对r. t是正确的。E.这个定义包括了F是一组I/O示例的特殊情况，E是包含所有输入被pn包含的I/O示例的子集。在这种情况下，定义指出，具有模式pn的规则ρ相对于r t是正确的。E和剩余的I/O示例i证明了通过将输入匹配pn的I/O示例集合E替换为ρ而得到的CS是正确的。替换的I/O示例。正确的CS的归纳被组织在如下两个级别中：在较高级别，搜索要被归纳的CS的lhss规则。这本质上是一个模式搜索，因为每个模式决定了一个规则的lhs。在第二级，为每个lhs计算rhs。如果对于每个找到的lhs，rhs的计算成功，则结果是完全诱导的CS。如果rhss的计算对于至少一个lhs失败，则搜索新的lhs集合。当且仅当对应的lhs不存在rhs，使得所得规则正确时，rhs的计算失败。一般来说，有无限多个具有不同规范化关系的CS，一组I/O示例，因为正确性w.r.t. I/O- examples没有声明除示例输入之外的所有术语。归纳算法只返回一个CS，因此知道将选择哪个正确的CS很重要。这种标准被称为归纳偏差。非正式地，我们的算法的归纳偏差可以通过三个标准来描述（所述顺序是相关的）：一个归纳正确的CS具有（i）尽可能少的规则，(ii)尽可能具体的模式，以及（iii）尽可能通用的RHSS。尽可能少的规则意味着不存在包含更少规则的其他正确CS。尽可能具体的模式意味着每个模式pn是它所包含的所有示例输入in的lglg。尽可能通用的rhss意味着，如果特定位置存在不同的可能性，那么模式中的变量优先于递归调用，递归调用优先于构造函数符号。4.1I/O示例我们的算法是基于检测之间的I/O的例子。这些关系式大致上就是定理3.2中所述的输出之间的关系式。“粗略地”，因为-根据定理3.2 -输出o j，j ∈ { 1，.，k}被假定等于o在位置Uj处的子项，直到变量重命名。由于这种规则性检测方法，必须很好地选择I/O示例。E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4959从技术上讲，输入必须递归地包含在w.r.t.计算目标函数的CS定义4.4设F是一个CS，它相对于t是正确的。一组I/O示例FE。I/O示例被称为递归包含w.r.t. F i对所有与F的任何递归规则的模式相匹配的示例输入i n成立：令F（pn）→t是递归规则，使得in通过替换σ与pn匹配。那么对于t中的每个递归调用F（rn），直到变量重命名，实例化rnσ都包含在FE中作为示例输入。由于归纳算法不能使用背景知识，也不能自动引入额外的参数，因此示例输出必须由构成结果rhss的构造器组成，并且示例输入必须是所有参数的输入。4.2搜索模式在我们描述模式搜索之前，我们陈述状态空间的几个特征：如果F是从一组I/O-示例FE诱导的CS，则每个示例输入都被F的模式包含，并且不存在包含没有示例输入的模式为了减少搜索空间，我们只考虑那些模式，这是所有的例子输入在FE中，它们分别substrate lglgs这三个特征和对目标CS的要求，即没有两个LHSS统一，导致状态空间的以下特征。对于每一组考虑的模式，P成立：• P包含所有示例输入，• P中没有两个模式是统一的，• P中的每个模式包含至少一个示例输入，• P中的每个模式是它所包含的所有示例输入的lglg如果I/O示例的数量是有限的，则搜索空间是有限的。为了用尽可能少的规则来诱导CS，状态空间将被排序，使得在具有更多模式的集合之前考虑具有更少模式的集合。在这种顺序下，状态空间正好有一个（直到变量重命名）最小值，即包含正好一个模式的集合-所有示例输入的lglg。 这个状态就是初始状态。状态空间只有一个（直到变量重命名）最大值，即包含每个示例输入作为其自己的模式的集合。该状态是正确规则的计算成功的最后一个状态，因为简单地说，I/O示例本身就是正确的规则（w.r.t.本身）。现在假设一个状态P具有任意数量的模式，这些模式符合所述条件。如果对于至少一个模式，不能计算正确的规则，则必须计算后继状态。设pn是这样一个模式，对于它不存在正确的规则。然后，其输入被pn所包含的I/O示例必须被划分为至少两个子集的最小数量，并且pn必须被各个子集的输入的lglgs替换我们称之为60E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49新的LGLG/模式集合最一般地划分LGLG（MGPL）。这是这样做的：首先，从F（pn）中选择一个位置u，它由F（pn）中的一个变量和每个包含的示例中的构造函数lhs标记。由于F（pn）是所包含的示例lhss的lglg，因此，在至少两个示例输入中，这些构造器是不同的。然后，在位置u处具有相同构造函数的所有示例输入分别被取到相同子集中。这导致了示例输入的分区最后，对于每个子集，计算lglg后继状态是这样一种状态，在该状态中，不能计算出正确规则的所有模式都被相应的mgpl集合替换。由于确定分区的位置通常不是唯一的，因此mgpl的集合也不是唯一的。因此，由mgpl替换这些模式的所有组合都被包括作为后继状态。比如让1.DelZeros（[]）→[]2.DelZeros（[0]）→[]3.DelZeros（[s（x）]）→[s（x）]四、DelZeros（[0，0]）→ []五、DelZero（[s（x），0]）→ [s（x）]六、DelZeros（[s（x），s（y）]）→ [s（x），s（y）]是DelZeros的I/O示例（cp. 图1）。 初始状态由六个示例输入[]，[0]，[s（x）]，[0，0]，[s（x），0]，[s（x），s（y）]的lglg组成，其简单地是单个变量q。 由于这种模式不存在正确的规则，因此必须计算模式的后继集。由于当前模式是一个变量，DelZeros（q）中确定分区的（唯一）位置是位置1。在示例lhss中，出现在这个位置的两个构造函数是[]和cons。因此，示例被划分为两个子集，分别包含第一个示例和所有其他示例。新的模式是[]和[q|qs]，因为这些分别是第一输入和其他输入的lglg。对于模式[]，将找到一个规则（只是第一个I/O示例），但对于模式[q|qs]将找不到rhs。因此，必须再次划分剩余的示例。现在DelZeros中有两个位置（[q|（1）有疑问的，1。1和1. 2. 位置1 .一、1分别表示当前lhs中的变量q和其余示例输入2-6中的构造器0和s。它将I/O示例划分为由I/O示例2和4组成的一个集合以及由I/O示例3、5和6组成的另一集合。这导致了两个新的模式/lglgs，[0 |qs]和[s（x）|qs]。位置1 .一、2分别表示当前lhs中的变量qs以及其余示例输入中的构造函数[]和cons。它将I/O示例划分为由I/O示例2和3组成的一个集合和由I/O4-6.这导致两个新的模式，[q]和[q，qJ]。因此，我们得到模式状态{ []，[ q]的两个后继状态|qs]}，即first {[]，[0 |qs]，[s（x）|qs]}（cp. 的E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4961DelZeros-CS，如图1所示）和第二{[]，[q]，[q，q，J]}。4.3计算右侧给定一组模式，对于具有模式pn的每个lhs，必须计算正确的rhs在一个函数CSF的一个Rhs中的任意位置的符号可以是• C中的构造函数，• 定义的函数符号F（递归调用），或• 包含在相应LHS的模式pn中的变量下面的定理陈述了递归调用的充分条件：定理4.5设F（in）→ o是I/O-例子，pn是用置换σ包含in的模式. 设F（iJn）→oJ是第二个I/O示例，使得（i）o|u= oJτ，对于某个位置u和变量重命名τ，（ii）iJn=rnθ，对于一列项rn和包含在rn中的所有变量的某个替换θ，（iii）θτ <$σ.设F是一个连续且终止的CS，它是正确的。F（ijn）→oJ，并且包含规则ρ：F（pn）→t [F（rn）] u使得lhs F（pn）不与F中的另一个lhs统一. 则F（in）归一化为项s，其中s|u= o|u，即， 当地ρw.r.t.位置uI/O实例F（in）→o和F\ {ρ}是确定的。证据F（in）=F（pn）σ/前提条件根据规则ρ一步重写为t[F（rn）]uσ=tσ[F（rn）σ]u。根据（ii）和（iii），tσ[F（rn）σ]u=tσ[F（rn）θτ]u成立=tσ[F（iJn）τ]u.F（iJn）τ在每个前提条件下归一化为0Jτ，即，tσ[F（iJn）τ]u对于某项tJ归一化为tJ[oJτ]u。 它保持tJ [oJτ] u= tJ [o|U] U根据（i），即，F（in）归一化为s = tJ [o|u] u和它持有s|u= o|联合Q该定理陈述了关于一个I/O实例F（in）→o的条件，其输入被要构造的规则的模式pn所包含，这些条件足以在特定位置u引入特定的递归调用F（rn）。当然，所有输入被pn包含的I/O示例都必须用相同的递归调用F（rn）来满足定理前面的表征的rhss和定理递归调用导致以下一般的方法来构建一个正确的规则rhs给定的模式pn和I/O的例子，其输入匹配的模式。以下三种情况按所述顺序审议：1.模式变量：所有输出都可以由同一个模式变量产生：那么rhs就变成了这个变量。2.递归调用：所有的输出都可以由相同的递归调用F（rn）产生：然后rhs变成F（rn）。3.构造函数：所有输出的根都是具有元数m的相同构造函数f：那么rhs就变成了f（t1，. 其中，通过考虑位置i处的输出的子项的这三种情况来构造ti。62E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）49如果没有适用的情况，则对于该模式不存在正确的rhs，并且必须搜索一组新的模式。例如，让我们再次考虑DelZeros的I/O示例：1 .一、DelZeros（[]）→ []，2. DelZeros（[0]）→ []，3 .第三章。DelZeros（[s（x）]）→ [s（x）]，4. DelZeros（[0，0]）→ []，五、 DelZeros（[s（x），0]）→ [s（x）]， 6. DelZeros（[s（x），s（y）]）→ [s（x），s（y）]假 设 ， 模 式 [s （ x ） ] |qs] ，其 分别包含具 有 子 项 σ3 ={x<$→x ， qs<$→ []} 、 σ5={x<$→x，qs<$→ [0]}和σ6 ={x <$→x，qs<$→ [s（y）]}的输入3、5和6。情况2也失败了，因为没有找到递归调用，使得对于所有三个I/O示例，满足定理4.5案例3成功是因为所有三个考虑的输出都有相同的构造器符号cons作为根。因此，要构造的rhs的根变为cons，并且三种情况被应用于所考虑的三个示例输出的位置1和2对于位置1，这在两步之后导致子项s（x对于位置2，情况1失败。但是情况2（递归调用）成功了，因为对于递归调用DelZeros（qs），定理4.5的条件对于三个输出的位置2处的所有三个子项都满足：输出3的位置2处的子项是[]。对于I/O-例子1，它的输出等于这个子项，变量重命名为τ= τ。I/O示例1的输入通过代入θ ={qs<$→ []}来匹配递归调用DelZeros（qs），并且它保持θτ <$σ3。对于I/O示例5，条件由作为第二I/O示例的I/O示例2来填充，τ= θ，θ= [0]。对于I/O示例6，条件用作为第二个I/O示例的I/O示例3来满足，τ={x<$→y}，θ= [s（x）]。结果rhs是[s（x）] |DelZeros（qs）]。5对方法虽然我们的方法本质上是学习函数程序，但它可以直接将任何诱导的单函数CS转换为逻辑程序，例如，prolog程序。例如，考虑图1所示的DelZeros-CS。一个等价的prolog程序是：DelZeros（[]，[]）←DelZeros（[0|（XS，Z）←DelZeros（XS，Z）DelZeros（[s（X）|XS]、[s（X）|Z]） ← DelZeros（XS，Z）我们已经用编程语言Maude [2]实现了所述算法的原型. Maude是一种基于等式逻辑和重写逻辑的反应语言。反射意味着Maude程序可以将Maude程序作为数据处理。E. Kitzelmann，U.Schmid/Electronic Notes in Theoretical Computer Science 174（2007）4963功能#expl#rules（#rec）#rec. 电话#rec. params倍长度3第二条第一款1.002最后3第二条第一款1.003IncList3第二条第一款1.003甚至4第三条第一款1.004TreeRev4二（一）二1.009添加9第二条第一款1.022德尔泽罗斯6第三条第二款第1项1.055≤9第三条第一款2.081总和13第三条第二款第1项1.127采取9第三条第二款第1项2.145Zip9第三条第二款第1项2.263PlayTennis14（0）00.679表1一些推断函数在表1中，我们列出了样本问题的实验结果。第一列列出了导出函数的名称，第二列列出了给定I/O示例的数量，第三列列出了导出规则的总数，括号中列出了导出递归规则的数量，第四列列出了一个规则中递归调用的最大数量，第五列列出了递归参数的数量，第六列列出了合成所消耗的时间（以秒为单位）。实验在Pentium 4和Linux上进行，程序运行用Maude解释2.2口译员。除IncList和PlayTennis外，其他函数在第3.2节中描述。IncList将后继函数s应用于给定列表的每个元素。PlayTennis是Mitchell的机器学习教科书[ 9 ]中的一个属性向量概念学习示例14个训练实例由四个属性组成。通过我们的方法学习的五个非递归规则与本书第53页所示的ID3学习的决策树等价所有被诱导的程序都计算预期的功能。6结论和进一步研究我们描述了一种方法来诱导一类特殊的函数程序，这些程序由在单函数CS上的并发和终止子程序表示。所提出的方法学的灵感来自经典和最近的分析方法，以诱导功