构造演绎综合证明的归纳规则构造技术

理论计算机科学电子笔记153（2006）3-21www.elsevier.com/locate/entcs构造演绎综合证明Alan Bundy<$1，2 Lucas Dixon<$3 JeremyGow<$4 Jacques Fleuriot<$5英国爱丁堡大学爱丁堡大学英国伦敦大学学院互动中心摘要我们描述了新的计算技术，用于构建演绎综合证明的归纳规则演绎合成提供了根据期望行为的规范自动构造正确计算机程序的希望。用迭代或递归合成程序需要归纳证明，但是构造适当归纳规则的标准技术仅限于循环使用规范的递归结构。所需要的是可以引入新颖的递归结构的归纳规则构造技术我们表明，涟漪和使用元变量作为一个最少的承诺设备的组合可以提供这样的新颖性。关键词：演绎综合，证明规划，归纳法，定理证明，中外推理。1本文中报告的研究得到了EPSRC第一和第三作者的GR/S 01771资助，以及第二作者的EPSRC助学金我们感谢安迪·富加德2电子邮件：bundy@inf.ed.ac.uk3电子邮件地址：ldixon@inf.ed.ac.uk4 电子邮件：ucl.ac.uk5 电子邮件地址：jdf@inf.ed.ac.uk1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.08.0034A. Bundy等人/理论计算机科学电子笔记153（2006）3¨¨证明规格- 你好质量标准（i，o）¨¨构造性定理证明¨¨程序提取- 功能程序prog（i）会议规格Spec（i，prog（i））Spec（i，o）是对所需程序的输入i和输出o之间关系的逻辑规范。要证明的猜想是，无论输入是什么，总有一个输出满足这个规范。构造性证明用于确保适当的输出，prog（i）被构造为证明的边输出。此输出提供所需程序的定义。通过构造，该程序已知满足其规格。证明的一些步骤提供了程序操作。例如，case splits提供了条件分支，而归纳步骤提供了递归定义。Fig. 1.从构造性证明1介绍在系统开发的形式化方法库中，最未被充分利用的技术之一是从程序规范的证明中进行程序的演绎合成演绎合成提出了许多困难的技术挑战，这可能是它相对被忽视的原因之一。在本文中，我们解决了这样一个挑战：在存在量化器存在的情况下选择归纳规则。我们描述了一些新的技术，自动构建的归纳规则，提供了一种方法来解决这个问题。2演绎合成为了便于说明，我们将采用演绎综合的一个特别简单的版本。 这在图1中示出。 节目将代表作为递归函数和规范作为同一高阶、类型化、构造性逻辑中的公式。这将使我们能够发现程序语义的问题，并通过用合成程序代替存在变量，将合成结构转化为验证结构，如图1所示。程序A. Bundy等人/理论计算机科学电子笔记153（2006）35为 了 说 明 这 个 过 程 ， 考 虑 合 成 一 个 排 序 算 法 的 任 务 sort ： list（N）›→list（N），即一个函数，其输入是一个自然数列表，其输出是输入列表的有序排列。合成猜想可能是：l：list（N）. m：list（N）. ord（m）erm（l，m）其中ord：list（N）›→bool是一个谓词，用于测试一个列表是否有序，perm：list（N）×list（N）›→bool是一个谓词，用于测试一个列表是否是另一个列表的置换我们采用的惯例是小写罗马字母字母代表对象级变量或常量，而大写罗马字母代表范围在对象级表达式上的元变量这个证明将为存在变量m构造一个见证。这个见证将是l的一个函数，我们称之为sort（l）。由于逻辑是构造性的，排序将根据先前定义的函数（递归地）定义。证明将验证sort（l）满足其规范，即即：l：list（N）. 或d（so rt（l））与m（l，sort（l））相关联。所合成的排序算法的类型将取决于证明的细节[3]。3入职规则图1指出了合成证明的步骤与它们合成的程序步骤之间的对应关系。特别地，归纳规则在证明中的应用在合成程序中插入递归。而且，归纳规则的类型决定了递归的类型。在命令式程序中，归纳步骤将创建迭代或循环。更一般地说，每当合成对象需要某种形式的重复时，就需要归纳。重复出现在递归数据结构、递归或迭代程序、时间变化、参数化硬件等中，即，在几乎所有非平凡系统中。因此，归纳在演绎综合中具有中心的重要性。有许多熟悉的递归数据类型：自然数，整数，有理数，列表，树，集合等。它们都可以从诺特归纳法（也称为有根据归纳法）的一般图式中推导出来：x：τ。（注：τ。y<$x→φ（y））→φ（x）x：τ。 φ（x）（1）6A. Bundy等人/理论计算机科学电子笔记153（2006）3其中τ是关于类型τ的某个有根据的关系。我们所说的有理有据是指，没有无限的、下降的形式链...... 一个3个2个1个。每个非平凡数据类型τ的无穷多个可能的良基关系给出了这个诺特模式的无穷多个可能的实例。由于不可能预先存储所有类型上的所有良好基础关系，τ，大多数归纳定理证明器根据需要构造归纳规则。的普遍量化的变量x称为归纳变量。也有可能同时归纳一个以上的变量，但为了简单起见，我们在这里省略了这种额外的复杂性，但将在下面回到它。实际情况比这更复杂。诺特图式很少被直接使用。通常，我们使用从它派生的归纳规则，例如下面的类型列表（τ）规则。φ（[]）l：list（τ）。l/=[]φφ（tl（l））→φ（l）l：list（τ）。φ（l）（2）其中[ ]是空列表，tl（l）是列表l的尾部。这个归纳规则是基于一些有充分根据的关系式，在该关系式下，tl（l）=l。许多这样的关系，prec，将支持，例如，一个基于列表的大小。这个规则的第一个前提φ（[]）是一个基本情况的例子;第二个前提φ（[ ]）是一个基本情况的例子。premise，l：list（τ）. l/= [ ] φ（t1（l））→φ（l）是阶跃情况的示例。步骤情况的前件φ（t1（l））是归纳假设，后件φ（l）是归纳结论。函数tl（l）是一个测试-一个析构函数的一部分，因为它析构递归数据类型。当一个析构函数包围归纳假设中的归纳变量时，我们说归纳规则是析构函数风格的。要制定析构函数式的归纳规则，有必要识别基和步骤情况，其中可能有几个，并找到一个良好的基础关系，在这种关系下，析构函数输出的项严格小于其输入。析构函数样式归纳规则的一种替代方法是构造函数样式。在构造函数式规则中，归纳假设中的析构函数被归纳结论中的构造函数取代。构造函数从旧数据类型构造递归数据类型的新元素。为实例，构造函数[h|t]构造类型的新成员list（τ）是从列表t：list（τ）和元素h：τ得到的。建筑师风格的诱导-析构函数归纳法（2）对应的规则为：φ（[]）φh：τ。t：list（τ）。 φ（t）→φ（[h|t]）l：list（τ）。φ（l）（3）其中[]是空列表，[h|t]是通过将h放在A. Bundy等人/理论计算机科学电子笔记153（2006）37列表的头T。该规则的基本情况也是φ（[]），步骤情况是h：τ. t：list（τ）。 φ（t）→φ（[h|t]）。正如我们将在下面看到的，也可以有混合析构函数/构造函数风格的归纳规则。也可以有多个归纳假设的规则，例如下面的二叉树数据类型的构造器风格规则。φ（leaf（e））φl：tree（τ）. r：tree（τ）. φ（l）<$φ（r）→ φ（node（l，r））t：tree（τ）。φ（t）其中叶（e）构造具有标签e的树的叶，而节点（l，r）从左子树l和右子树r构造新的二叉树。上述规则都是所谓的结构归纳规则，即：它们使用了来自数据类型递归定义的析构函数和构造函数非结构化规则也是可能的，例如，φ（[]）l：list（τ）。φ（butlast（l））→φ（l）l：list（τ）。φ（l）（4）其中，butlast（l）输出列表l，其中最后一个元素被删除。关于归纳规则的进一步讨论见[5]。4递归程序的假设归纳法被用来证明一个综合猜想，例如：l：list（τ）。m：list（τ）。spec（l，m）使用析构函数风格的归纳规则（2）合成的程序，作为归纳变量，将具有以下递归形式。prog（l）：：= ifl = [ ] thenbelsef（l，prog（l））其中b和f不包含prog。另一方面，使用构造器风格的归纳规则（3）合成的程序将具有以下递归形式。prog（[ ]）：：=bprog（[h|t]）：：= f（h，t，prog（t））使用非结构化归纳规则（4）合成的程序将具有以下递归形式。prog（l）：：= ifl = [ ] thenbelsef（l，prog（butlast（l）8A. Bundy等人/理论计算机科学电子笔记153（2006）3为了合成一对相互递归的程序，我们需要两个存在变量：l：list（τ）。m1：list（τ），spec（l，m1，m2）从中我们可以提取出prog1和prog2，分别作为m1和m2的存在性见证如果使用构造函数式的归纳规则（3）来证明这个综合猜想，那么以下相互递归的定义将被综合。prog1（[ ]）：：=b1程序1（[h|t]）：：= f1（h，t，prog1（t），prog2（t））prog2（[ ]）：：= b2程序2（[h|t]）：：= f2（h，t，prog1（t），prog2（t））5构造归纳规则递归分析是为特定对象构造定制归纳规则的最著名的技术。这是由于Boyer和Moore，并在他们的Nqthm证明器中实现[1]。其基本思想是在猜想中识别递归定义的函数，然后将其转换为相应的归纳规则。例如，如果猜想包含一个函数g，其递归定义是g（k，l）=f（k，l，g（k，tl（l），那么就可以提出具有归纳变量l的析构归纳规则（2）。Boyer和Moore开发了一些技术，将不同递归函数中的sug-gestion合并并推广为一个归纳规则，将它们全部包含在内。Walther后来提出了一种递归分析的变体，它使用不同的技术来合并归纳规则[12]。递归分析的启发式基础是，通过选择包含与递归定义相同的析构函数的归纳假设，我们最大限度地提高了这些定义能够操纵假设的机会。递归分析也可以适应构造函数风格的定义和归纳规则。递归分析如图2所示。递归分析是为纯粹的普遍量化的猜想而开发的。当它涉及到包含存在量化器的结构时，特别是在演绎综合中使用的结构，它有一个主要的缺点：证明中使用的归纳规则将决定综合程序的递归结构，即它的基本算法性质，包括它的复杂性。递归分析将使用它在猜想中发现的递归形式来选择这个归纳规则，即：算法的本质A. Bundy等人/理论计算机科学电子笔记153（2006）39猜想：l：list（τ）。m：list（τ）. perm（l，m）递归定义：perm（l，m）：：= ifl = [ ] thenm = []elseperm（t1（l），del（hd（l），m））其中del（e，l）从列表l中删除元素e。构建归纳规则：φ（[ ]） l：list（τ）. l = [ ] φ（tl（l））→φ（l）l：list（τ）. φ（l）perm是唯一出现在猜想中的递归定义的函数。它的递归定义是在l上，perm的第一个参数，对这个参数的递归调用是tl（l）。这表明构建一个一步的析构函数式归纳，其中l是归纳变量，并将归纳假设应用于tl（l）。 当应用这个归纳规则时，归纳项φ（l）将被实例化为m：list（τ）。perm（l，m）.图二. 递归分析的规格。因此，通过演绎合成构造的程序在算法上与它们的规范相似。这不是一个理想的状态的一个飞行员。例如，这意味着递归分析无法构造快速排序合成所需的归纳规则，因为它的递归结构与order或perm的递归结构完全不同。 我们将使用图2中perm的定义和以下ord的定义：order（l）参与式如果l= [ ]则Telseifl =[h] thenTelseifhd （ l ） ≤hd （ tl （ l ） ）thenord（tl（l））else而快速排序的通常定义是：qsort（[ ]）：：= []qsort（[h|t]）：：= qsort（less（h，t））<>[h]<> qsort（more（h，t））其中less（h，t）是t中小于或等于h的成员的列表，more（h，t）是严格大于h的t的成员列表，<>是infix列表追加函数。递归分析将使用ord和perm的定义来构造归纳规则（2）或（3），而要合成qsort，我们需要类似于以下混合析构函数/构造函数风格的归纳规则。φ（[]）h：τ. t：list（τ）。 φ（less（h，t））<$φ（more（h，t））→φ（[h|t]）l：list（τ）。φ（l）（5）10A. Bundy等人/理论计算机科学电子笔记153（2006）36纹波和纹波分析涟漪是一种启发式的技术，用于在归纳假设的帮助下控制归纳结论的证明[2]。它的工作原理是注释结论和假设之间的差异，然后尝试使用称为波浪规则的注释重写规则来减少它们。图5和图6说明了这个过程，并给出了注释和波浪规则的示例Ripping提出了一种替代递归分析的方法来构造一个合适的归纳规则。我们可以使用波动法则，而不是使用递归定义来表示归纳项和变量。我们称这种技术为波纹分析。涟漪分析对涟漪过程进行了一步前瞻，并提出了一个归纳规则，该规则通过提供与波浪规则左侧相匹配的归纳项来促进涟漪。纹波分析如图4所示，使用了我们用于递归分析的相同示例，以强调差异。特别是，波纹分析能够突破递归定义结构的循环，提出基于导出引理而不是递归定义的归纳规则。不幸的是，纹波分析并不总是建议最佳诱导规则。主要的问题是，它只对涟漪过程进行了一步预测。后来的涟漪步骤可能会对归纳项提出额外的要求，而这些要求在第一步中并不明显。图6给出了纹波分析失败的示例7中间推理在§5中，我们描述了构造归纳规则来证明综合定理的问题。在本节中，我们提出了以下解决方案问题.我们将使用高阶元变量作为最小承诺装置来推迟归纳规则的构建。特别地，我们将假设我们对合成程序有一个递归定义，但在其定义中使用元变量来代表构造函数和析构函数。然后我们将继续进行综合证明。就像在涟漪分析中一样，我们将构建一个允许涟漪继续进行的归纳规则，但这个规则将包含元变量，因此将仅部分定义。在综合证明的过程中，高阶统一将实例化元变量，从而确定归纳规则和综合程序的定义。这将允许在证明中不仅第一个而且所有的涟漪步骤来检验归纳规则的构造。这种增加的可伸缩性是有代价的：更大的搜索空间。应用高阶unifi-A. Bundy等人/理论计算机科学电子笔记153（2006）311ord（L）ord（M）L[X][X]M↑↑l，l′，m，m ′：list（τ）.∧→φ（、）ls<>msL>m波动规则：↑↑qsort（）[H|T]（六）↑中文（简体）波形规则是用波前标注的重写规则，波前标记规则左侧和右侧之间的相似性和差异性。当应用波浪规则时，波浪注释必须匹配。波浪规则（6）源于qsort的递归定义，并在步骤（9）中应用波浪规则（7）是关于阶的引理，并且在步骤（11）中应用图三.图5中使用的波浪规则猜想：l：list（τ）。m：list（τ）. perm（l，m）波浪规则：↑⇒构建归纳规则：m：list（τ）.φ（[ ]，m ）List（τ）. φ（[h|t]，[]）l，m：list（τ）. φ（l，m）（8）假设将归纳法应用于具有归纳变量l的猜想，l作为唯一的泛量化变量，是唯一的归纳变量候选者。如果归纳结论包含以下形式的子项，则上述波动法则将适用于归纳结论：↑. 因此，上述归纳规则的构建就是为了提供这样的规则。一个归纳术语请注意，波浪法则是基于一个关于perm的分布律引理，而不是它的递归定义。当然，其他的波浪规则也会提出其他的归纳规则建议，包括基于perm递归定义的波浪规则，就像递归分析一样。见图4。 纹波分析阳离子到目标中的元变量，增加了涟漪的分支率。幸运的是，目标中的wave注释和wave规则中的wave注释必须匹配的附加涟漪要求，极大地减少了否则会出现的不可接受的组合爆炸。我们有责任证明<>[H]<> qsort（）更多（H，T）qsort（）减去（H，T）↑（）L<>[X]<>M↑↑perm（、）M>MsL>Lsφ（l，m）φ（ls，ms）L> mperm（L，M）perm（Ls，Ms）12A. Bundy等人/理论计算机科学电子笔记153（2006）3order（qsort（less（h，t）order（qsort（more（h，t）···Givens：最初中和目标和涟漪：（九）（十）↑（十一）↑（十二）中文（简体）这个例子取自使用归纳规则（5）的ord（qsort（l））的验证证明的步骤情况。在l = less（h，t）和l = more（h，t）的情况下，两个归纳假设提供了给定的条件。归纳的结论是用涟漪证明的目的。给定和目标都被注释以指示它们在哪里相似以及在哪里不同。注释由称为波前的空心灰色框组成;这些波前中的孔称为波孔。波孔中的表达式由给定的共享，目标和灰色区域中的表达式是它们不同的地方。在步骤（10）中，可以通过丢弃给定中的波前和目标中的最里面的波前来增加两个波孔的尺寸。这是因为目标和给定的相似性增加了。我们称这个过程为中和。涟漪通过使用图3所示的波浪规则重写目标来进行。注意，应用波动法则的结果是波孔的含量增加了直到一个给定的副本出现在它们里面。然后，在步骤（13）中，可以使用这些给定值来用T替换副本。 注意，LM表示列表L的每个元素小于列表M的每个元素，并且LM表示每个元素L小于或等于每个元素M。在步骤（12），通过应用两个引理qsort（less（h，t））[h]和[h]qsort（more（h，t））来简化波前。图五. Ripping的例子sort（））sort（））more（h，t）减去（h，t）int n= nums（nums，nums，nums）int n=nums（nums（n））↑sort（））↑（）↑（）））<>[h]<>qsort（qsort（qsort（less（h，t））<>[h]<>qsort（more（h，t））more（h，t）减去（h，t）[h|t]order（qsort（less（h，t）order（qsort（more（h，t）···ord（qsort（less（h，t）[h][h]ord（qsort（more（h，t）A. Bundy等人/理论计算机科学电子笔记153（2006）313s（x+y）s（x+z）s（s（n））s（M+N）↑φ（0）n= N.（1）A（）s（n）猜想：波浪规则：x，y，z：N。 even（x + y）→ even（y + z）→ even（x + z）↑ ↑+ N（十四）（十五）目标和涟漪：↑连（（2）A+B（↑+z）连（↑ ↑）even（y+z）→even（）“我的天，封锁“我的天，封锁通过波动分析构建的一步归纳规则：N. φ（n）（16）一个更好的两步归纳法则：↑φ（0） φ（s（0）） N.φ（n）→ φ（）N. φ（n）（十七）波动分析一步向前看使用波动规则（14）来构造一步归纳规则（16），其中x作为归纳变量。x优于y和z，因为波动规则（14）将能够使s（x）的两次出现波动。如果选择y，则只有第二次出现的s（y）可以被波纹化，如果选择z，则两次出现的s（z）都不能被波纹化。在使用上述波动规则（14）的归纳结论中，波动在蕴涵的两侧进行理想情况下，波浪规则（15）现在可以应用于两边，但它需要一个包含两个嵌套的s的波前，而不是一个。我们应该使用两步归纳法则（17），而不是（16）。见图6。纹波分析失败所构造的归纳规则是有效的，即良好的基础，并涵盖所有的数据类型的条款。我们称这种技术为中间推理，因为它推迟了早期的证明搜索决定，允许这些决定作为证明过程中的一个侧面。中出推理说明↑连（s（s（X）））偶数（X）s（x）s（x）s（M）14A. Bundy等人/理论计算机科学电子笔记153（2006）3在图7中。中庸之道是一个简单的想法，但已被证明是令人惊讶的难以实现。因此，我们的第一次尝试解决了问题的简化版本。我们并没有使用涟漪分析的中间版本动态地构建归纳规则，而是从预先验证的存储中选择它们。这项工作是由Ina Kraan作为博士项目进行的[10，9]。该方法已在长春花系统中实现，并成功地应用于最近，我们通过Jeremy Gow的博士项目 [5]解决了归纳规则的中出构造的全部问题，该项目在Dynamis系统中实现请注意，中出涟漪分析建议候选归纳项作为涟漪的副效应。然后，这些必须转化为有效的归纳规则。这可能需要将几个不同的归纳术语建议组合成相同归纳规则的互补步骤案例。它还可能需要构造相应的基本情况。然后，必须证明归纳规则是有效的。这涉及到表明它是基于一个良好的顺序，以及基础和步骤的情况下，涵盖了数据结构。为了简化充分性证明，我们将充分发现的度量限制为Walther估计演算中产生的度量这提供了一个简单的家庭，找到的措施，但具有广泛的覆盖面，包括最实用的算法。在实践中，基本和步骤情况的构造与覆盖和良好基础的证明交织在一起，即基本和步骤情况被发明以填补覆盖证明中的空白，并且良好基础的顺序被进化以包括所有这些步骤情况。正是这种不同证明过程之间的相互作用使得中出归纳规则的构建成为一项艰巨的任务。由此产生的举证义务如图9所示。8相关工作在显式归纳定理证明器中选择归纳规则的标准技术是递归分析。我们已经将其与Ripple进行了分析6。许多人已经从程序所需行为的一些方法使用了con-结构类型理论和一些使用经典逻辑。有不同程度的自动化，包括使用涟漪。然而，下面的讨论将仅集中于构建非标准归纳规则的机制及其对最小承诺机制的使用。 更详细的讨论见[5]。A. Bundy等人/理论计算机科学电子笔记153（2006）315（）D（qsort，T）intn（t，T）{int n= nums（nums，nums，nums）吉文斯：初始中和实例化return（FB（T））int n= nums（nums（n））目标和涟漪：（十八）↑（十九）↑（二十）↑（二十一）↑（二十二）T T这个合成证明片段遵循与图5中的验证证明相同的模式，除了元变量用于表示未知结构。和前面一样，波纹分析根据现有的定义性波动规则构建了一个归纳规则。对于演绎合成，考虑图8所示的快速排序（23）的示意性定义。这产生了一个示意图，给出了析构函数元变量D周围的潜在波前。这些元变量周围的虚线框表示潜在的波前--因为我们还不能确定它们中的哪一个是非平凡的，也就是说，不仅仅是对其中一个参数的投影。然后使用波浪规则23来使目标波动（步骤（18））。在步骤（19），应用波动规则（24）。这个应用程序使用更高阶的统一来实例化F到“λq t。FA（q，t）<> H（q，t）<>FB（q，t）“。 为了可读性，我们编写的元变量没有参数时，他们没有被波阵面注释。在 上面的证明中，这样的元变量具有隐式参数qsort和T。然后中和给定中 的 析 构 函 数 D 和 目 标 中 的 FA 和 FB 周 围 的 潜 在 波 前 ， 并 移 除 注 释 （ 步 骤（20））。这就把FA和FB引入了给定的。在步骤（21）中，用引理“qsort（less（X，Y））[ X ]“和“[ X ]”来简化所得到的波前。qsort（more（X，Y））“来自证明的置换分支。这一次，高阶统一将FA（qsort，T）实例化为“less（F A 2（qsort，T））“，将F B（qsort，T）实例化为“more（F B 2（qsort，T））“。在证明的覆盖检查分支中，对FA2、FB2和H进行了最后的实例化。这允许目标然后通过步骤（22）中的施肥来解决。见图7。中出综合return（C（T））return（F（T））∧A[H]A[ H ] A[H]FBorder（qsort（less（H，FA2）order（qsort（more（H，FB2）order（qsort（less（h，t）order（qsort（more（h，t）（FA（qsort，T））order（FA（qsort，T））order（FB（qsort，T））<$FA[H]<$[H]FB（FB（qsort，T））16A. Bundy等人/理论计算机科学电子笔记153（2006）3波动规则：（二十三）↑（二十四）波浪法则（23）是从最初未知的qsort的示意性定义中推导出来的。在这个示意性定义中，我们使用高阶元变量C来表示初始未知的构造函数，F表示包含可能的析构函数的主体综合证明的目的是实例化这些元变量，从而构造qsort的定义。这个实例化将把波动规则（23）变成波动规则（6）。图8.第八条。图7中用于中间输出合成的初始波形规则定理归纳规则x，y，z：N。even（x+y）even（y+z）→偶数（x+z）φ（0）φ（s（0））n：N。（1）A（N. φ（n）↑s（s（n）计算公式：N × N ›→ N。 N. list（N）.foldleft tr（x，x，l）=foldleft（x，x，rev（l））φ（[]）：τ。 f：list（τ）。（2）A（l：list（τ）. φ（l）f<>[e]↑）第一个例子类似于图6。中间推理消除了仅一级前瞻的限制。当涟漪到达应该应用even的定义的点时，仍然有一个未实例化的元变量可以用来解释归纳项并产生所需的两步归纳规则。在图9中更详细地解释了第二示例。 结果表明，中庸之道推理可以应用于高阶定理，并能构造出相当特殊的归纳规则。表1Dynamis系统的部分实验结果是有限制的，因此该规则是有充分根据的建设。相对于中庸之道的归纳规则构造，惰性归纳有三个缺点，并且没有我们所知道的优点(i) 它仅限于析构函数风格，而Dynamis和更一般的中间推理可以使用析构函数，构造函数和混合风格。(ii) 它缺乏搜索控制机制来处理使用潜在波前时的非终止性固有威胁（参见图9），而Dynamis具有防止非终止性的机制。(iii) 它没有显式表示生成的归纳规则，导致qsort（C（T））<$F（qsort，T）↑order（）ord（L）ord（M）L[X][X]ML<>[X]<>MA. Bundy等人/理论计算机科学电子笔记153（2006）317↑φ（[]）：τ。f：list（τ）。→φ（）f<>[e]猜想：计算公式：N × N ›→ N。N. list（N）. foldleft tr（x，x，l）= foldleft（x，x，rev（l））foldleft和foldleft tr是二阶函数，从第二个参数开始，重复地将第一个参数应用于第三个参数中的列表元素。foldleft按照从第一个到最后一个的顺序处理列表中的元素，但是foldleft tr按照相反的顺序处理它们，即foldleft（x，x，[e1，.，en]）=（en（. （e1x）.. . ））=foldleft tr（x，x，[en，.， e1]）示意性步骤案例证明：foldleft tr（x，x，C）=foldleft（x，x，rev（C））↑我们展示了如何从图1的foldleft示例中构造归纳规则由于l是唯一具有递归定义类型的泛变量，因此它被选为归纳变量，并在归纳结论中被二阶元变量C取代。尝试用它的定义来波纹foldleft tr失败了。在回溯这个失败的波纹之后，它会按照下面的波浪规则波动↑⇒这是一个很好的选择。 这一规则是C到C′<>[C′′]的关系，它揭示了归纳项的本质结构.现在我们可以证明归纳法的这一步是有根据的。波纹也将潜在的波前转化为具体的波前。涟漪继续成功受精。发现了以下步骤：C′→C′>[C′′]估计演算的任务是找到一个有充分根据的度量，以表明<由归纳假设中的相应项C ′的简单、严格的广义估计所建议的独立项C ′ > [ C′ ′]。它成功地使用基于列表长度的度量发现丢失的案例：l：list（N）. Ae：N，f：list（N）. l = f<>[e]我们知道归纳法则的一个例子，还需要发现其他的例子。在这种情况下，元变量A将被实例化为l = [ ]，即发现一个基本情况。通常，可能需要任意数量的基本或步骤情况证明新的情况：foldleft tr（，x，[ ]）=foldleft（，x，rev（[]））我们现在需要证明新发现的基本情况下的定理。构建归纳规则：l：list（τ）. φ（l）见图9。 中出归纳规则构建中C′′折叠权tr（x，x，Cs）↑=foldleft（x，rev（D））C′>[C′′]↑foldleft tr（F，X，）L<>[Y]F（Y，foldright tr（F，X，L））φ（f）18A. Bundy等人/理论计算机科学电子笔记153（2006）3对证明分支的无用探索，其中归纳变量的不同实例被隐式地分配不兼容项。Dynamis通过用Meta变量显式地表示这些术语来避免这个问题。例如，假设两个不同的归纳规则每个都有两个步骤情况。Lazy Induction将探索步骤case的所有四种组合。Dynamis使用共享元变量将搜索限制为两个兼容的组合。当一个元变量在一种情况下被证明搜索实例化时，它在另一种情况下会自动实例化为相同的值，这将排除不兼容的组合。8.2哈特Hutter也使用波纹作为基础，试图构建归纳规则的综合模型[7]。他的方法也是基于涟漪和证明规划。在尝试具体的证明之前，他的因卡系统首先建立了归纳步骤案例的抽象计划。归纳规则就是从这个计划中构造出来的。为了形成这个计划，他使用了波规则的抽象，其中波前的细节被删除了，只留下了可能穿过骨架碎片的信息。然后通过恢复和组合提取的波前来构造归纳规则。虽然Hutter他成功地将其应用于标准函数的逆的合成，使用这些函数作为规范，即 证明你的能力。你好 f（o）= i以合成f的逆。在合成的函数中，有log，half，商数和转速例如，rev的综合构造了归纳规则（4）。8.3缩小缩小[6]是重写的扩展，允许重写规则与目标的统一，而不仅仅是匹配，即目标可以包含元变量，这些变量可以在重写期间实例化。我们的中庸之道的推理本质上是涟漪到缩小的延伸缩小的主要作用在对猜想和skolemization6的否定中，存在性见证成为元变量。缩小将实例化这些元变量作为重写的副作用，逐步构建存在性见证。Dynamis和以前关于窄化的工作之间的主要区别是，我们使用元变量来代表未知的归纳项，[6]或者，等价地，目标的双重斯科勒姆化。A. Bundy等人/理论计算机科学电子笔记153（2006）319存在变量。在其他工作中，我们也使用元变量来代表广义引理和缺失引理中的未知结构[8]。9结论本文讨论了用构造性证明方法构造一个适当的归纳规则以供计算机程序自动综合之用的问题。归纳法是任何包含迭代或递归的程序的综合证明的重要组成部分。对于每个非平凡的数据类型，归纳规则的数量是无限的，因此归纳规则需要按顺序构建，而不是预先存储。然而，递归分析，归纳规则构造的标准技术，是为纯粹的泛量化定理而开发的。合成图总是包含存在性量化器。应用于综合定理，递归分析仅仅是在程序的具体化中调整递归。它无法提出一种新的递归结构，例如快速排序算法中使用的结构。我们已经开发了一系列的技术，归纳规则的建设，不限于回收原来的猜想中的递归。这些都是基于涟漪分析和中间推理的组合。它们已被成功地用于构造新的归纳规则自动机。真的 有两个原则在起作用。(i) 归纳项和归纳规则是通过应用引理而不仅仅是递归定义来提出的。(ii) 通过使用元变量来构造归纳项，从而构造归纳规则。在证明的过程中，这些被逐步地实例化，因此可以在构造的归纳规则的形状中考虑几个不同的证明步骤的要求。中出归纳规则构建中的最小承诺机制导致了证明义务的复杂转换。不仅必须证明原始定理，而且必须证明归纳规则是有根据的，并且覆盖数据类型。作为这些证明义务的一个侧面效应，我们构造了以下对象：归纳项、良基测度、缺失基和缺失步的情况以及归纳规则。每个证明义务共享并实例化一组元变量。在这些证明之间进行协同例程是可取的：因为在一个证明义务中的元变量的实例化会限制另一个暂时冻结的证明义务中的证明搜索，以允许它安全地重新启动20A. Bundy等人/理论计算机科学电子笔记153（2006）3最初的中出归纳规则构造实验仅限于纯粹的普适定理，例如验证证明中可能出现的定理。我们现在将注意力转向包含存在性量化器的定理，这是综合证明中所需要的。Dynamis系统正在被移植到IsaPlanner证明规划器，并应用于从其规范中合成程序。证明规划在这一工作中起着至关重要的作用，例如，使用中出推理实现了证明的灵活构造，并提供了强大的涟漪方法。除了将我们的技术应用于不断增长的合成语料库之外，我们还计划扩展我们的方法，以应对在示意性递归定义中具有未知数量的递归调用。我们还希望在不同的证明义务之间允许更灵活的合作。例如，我们希望能够冻结分支率太高的部分证明，并解冻分支率已经显著降低的部分证明，作为其他证明中共享元变量实例化的副作用，因为它们之前被冻结。引用[1] R. S. Boyer和J S.摩尔计算逻辑。中国科学院出版社，1979年. ACM专论系列。[2] A. Bundy，D.Basin，D.Hutter和A.爱尔兰涟漪：数学推理的元级指导。剑桥大学出版社，2005年。[3] J. 达林顿几种排序算法的综合Acta Informatica，11：1[4] J. Gow，A.邦迪和我。共享的 估计演算的扩展。 In H.甘青格，D. McAllester和A.Voronkov，编辑，Proceedings of the 6th International Conference onLogic for Programming and Automated Reasoning（LPAR史普林格出版社1705年。[5] 杰里米·高使用证明规划的归纳规则的动态创建。爱丁堡大学信息学院博士论文，2004年。[6] M. 哈纳斯功能集成到逻辑编程：从理论到实践。J. 逻辑程序设计，19 &20：583 -628，1994。[7] D.哈特存在性证明中归纳序的综合。见Alan Bundy，编辑，第12届自动演绎国际会议，人工智能讲义，第814卷，第29-41页，法国南希，1994年。史普林格出版社[8] A. Ireland和A.邦迪归纳证明中失败的有效使用。Journal of Automated Reasoning，16（1-2）：79-111，1996.也可从爱丁堡作为DAI研究论文第716号获得。[9] I.克朗逻辑程序综合的证明规划。爱丁堡大学人工智能系博士论文，1994年。[10] I. Kraan，D.Basin和A.邦迪综合与归纳的中庸之道Journal of Automated Reasoning，16（1也可从爱丁堡作为DAI研究论文729获得。A. Bundy等人/理论计算机科学电子笔记153（2006）321[11] M. 普罗岑归纳假设和修补Faith猜想的惰性生成。1995年2月，德国达姆施塔特工业大学博士论文[12] C.瓦尔特用机器组合归纳公理。在IJCAI-93的会议记录中，第95-101页。1993年国际人工情报联合会议[13] C. 瓦尔特算法终止性的机器证明。Arti ficialIntelligence，71（1）：101