理论计算机科学电子笔记37（2000）网址：http://www.elsevier.nl/locate/entcs/volume37.html17页编写构造性证明以产生有效的提取程序阿列克谢·诺金康奈尔大学Ithaca，NY 14853，USA.电子邮件地址：nogin@cs.cornell.edu摘要NuPRL系统[3]被设计用于交互式编写机器检查的构造性证明，并从证明中提取算法。提取的算法保证是正确的1，这使得可以使用NuPRL作为具有内置验证的编程语言[1，5，7，8，9，10]。然而，事实证明，在没有考虑算法效率的情况下编写的证明通常会产生非常低效的算法-对于可以在多项式时间内解决在本文中，我们提出了一些一般原则的有效规划的构造类型理论，以及描述一个案例研究，显示如何这些原则适用于特定的问题。我们考虑从NuPRL自动机库[4]中证明Myhill-Nerode自动机最小化定理，这导致了一个双指数（在时间上）提取程序。系统地使用所提出的原则，使我们能够建立一个新的复杂性谨慎证明，导致多项式时间算法提取相同的NuPRL提取器。我们相信，本文提出的原则与其他方法相结合，可能会导致一个有效的技术程序的证明。关键词和短语：自动机，构造性，Myhill-Nerode定理，NuPRL，程序提取，程序验证，提取编程，状态最小化。1介绍NuPRL系统[3]能够提取和执行构造性定理的计算内容，即使它只是隐含地提到。例如，给定鸽子洞原理的NuPRL证明，其形式为对于任何自然数n和对于来自{0，1，...， n}1前提是NuPRL系统的受信任部件正常工作2000年由ElsevierScien ceB出版。 诉 操作访问和C CB Y-NC-ND许可证。诺金2联系我们到0，1，...，n1存在一对数字0 i< jn使得f（i）= f（j），我们可以提取一个程序，它取n，f并计算这样的i，j。换句话说，NuPRL可以被看作是一种具有内置验证的编程语言：一个证明同时是一个程序和它的验证。然而，一些NuPRL证明的计算效率被证明是非常差的，因为它们是在没有注意效率问题的情况下编写的。在本文中，我们提出了一些方法，可以用来编写有效的证明程序（第2节）。然后，我们将演示这些方法如何允许我们在NuPRL中编写有效的谨慎证明在这方面，NuPRL类似于其他编程语言，其中经常存在速度较慢的程序和速度较快的程序，计算相同的函数。特别地，我们给出了对文[6]的形式化的Myhill-Nerode自动机极小化定理的NuPRL证明[4]NuPRL理论方便的模块化结构允许我们只重写几个无效引理的证明，以修复整个证明。这消除了NuPRL自动机库中所有已知的不必要的指数时间证明，特别是从最小化定理变成多项式。我们将首先简要概述NuPRL自动机库（第3节）。然后，在第5，6，7节中，我们将描述来自库的三个最无效的证明，并展示如何应用第2节中描述的原理将它们从指数和双指数（时间）变成多项式。2有效证明程序设计的一般原理这里是一个简短的审查的一般原则的计算效率规划的NuPRL型理论，介绍了这项工作。关于通过提取编程的一个基本观察是，经常非常优雅的证明产生令人惊讶的无效提取-例如从鸽子洞原理的早期证明中提取的指数时间程序。因此，我们不能只是写一些证明，并希望提取物会起到很大的作用我们认为，应该在已经对提取的算法应该如何工作有了一些了解的情况下开始编写证明。下面介绍的一些原则对应于传统命令式语言中众所周知的高效编程原则。 但这里的新之处在于，这些原则被使用非计算性的“昂贵”语句。当我们知道或怀疑某个语句会产生计算上昂贵的摘录时，我们应该尽量避免在计算上使用该语句诺金3∀ ∃∀∃短信了我们仍然可以在非计算性的上下文中使用它，例如证明某种“坏”状态是不可能的（因此，我们的算法不会卡住）。有关该原则的应用示例，请参见第5.3节。归纳步骤是计算复杂性的主要来源在传统的命令式编程语言中，大多数时间通常花在各种循环中，程序员经常不得不集中精力使循环更高效。在抽取式编程中，循环代码通常是从某个归纳步骤的证明中抽取出来的。因此，证明作者必须集中精力为归纳步骤编写有效的证明通常，使归纳步骤有效的第一步是提出一个好的归纳陈述。以下是一些方法：将循环不变量转化为归纳语句。 在证明作者知道循环如何工作的情况下，尝试找到该循环的一些不变量并将其反向工程成这样的证明，其提取实际上可以作为所需的算法工作，这通常是有益的。这样，算法的循环通常通过使用证明中的归纳来编程，DECIDE 本文中的所有例子都利用了这一点法使用存在量化器作为记忆。 当归纳陈述具有形式x u，v，w，. . . （其中x是我们正在进行归纳的对象），u，v，w，. . . 表示在每次循环迭代中计算和保存的对象。 例如，使用x：T1y：T2z：T3。A（x，y）<$B（x，y，z）而不是x：T1y：T2A（x，y）阻止我们产生一个算法每次需要的时候都会重新计算z使用列表作为记忆。提前评估足够的数据量，以便提取的算法可以重用它，而不是每次需要时都重新计算它。在这种方法下，必须通过断言和证明具有某些属性的列表存在，并在必要时查看这些列表，将所有必要的数据放在几个列表中（参见第6.2节，第7.2节和第7.3节，以了解此思想的应用示例）。3NuPRL自动机库3.1自动机库在本节中，我们将简要介绍NuPRL自动机库。这个库是基于Hopcroft -Ullman书[6]。NuPRL自动机库的详细描述可以在[4]中找到两个版本的图书馆是可用的-旧的一个，这是在[4]中描述，其中包含几个不合理的证明，和新的一个，其中的对象被组织成理论2不同，其中不合理的[2]在NuPRL中，理论是抽象定义、定理（以及证明）的集合，可能还有一些策略代码和/或注释。诺金4{}−→× →→∈ ∈∈证据已被更有效的证据所取代。构成图书馆每个版本的所有理论原始理论可以在www.example.com上http://nuprlauto-b.nogin.org/找到，更新的理论可以在http://nuprlauto.nogin.org/。下面你可以找到一个理论的理论描述更新库的那些部分，需要更好地理解这篇论文。我们提供了许多详细的定义，因为细节上的微小差异可以使编写证明，特别是编写有效的构造性证明变得更加容易或更加困难。还解释了一些常见的NuPRL符号。3.2FNITESETS理论3在这个理论中，它定义了集合s是有限的4意味着什么：Fin（s）==n：N. N n → s。 Bij（N n; s; f）其中，N n是用于类型0，...，n 1和Bij（N n; s;f）说f是N n和s之间的双射。从这个定义可以得出，有限集合的元素之间的相等是可判定的。这个理论还证明了有限集合和有限集合的元素列表的几个性质。特别地，它证明了Nn本身是有限的，并且有限集合的元素的固定长度列表的集合是有限的。最后，证明了鸽子洞原理（也见第5节）。3.3语言理论5这个理论给出了语言的定义。一个语言在某个字母表上的字母表是一个谓词在字母表列表（字母表元素的有限列表）上。该理论还给出了语言操作的定义：交集，并集，积和补。3.4行动组理论6某个类型T上的动作集是一个由载体类型car和动作函数组成的对，该动作函数采用t T和c car并产生cJcar：（T车汽车）。另一种思考方式是，一个动作集为T的每个元素分配一个动作车。该理论还给出了多作用函数的定义，该定义自然地将作用函数的定义从T的单个元素扩展到T的元素列表：（S：L←s）==rifnull（L）thenselse（S.act hd（L）（S：tl（L）<$s））fi3http://nuprlauto.nogin.org/finite_sets/[4]关于这一定义和可能的替代定义的讨论，见第85http://nuprlauto.nogin.org/language/6http://nuprlauto.nogin.org/action_sets/诺金5∈∈∈≤∀∨ ¬ →∨ ¬其中S.act被定义为S -的第二个元素，即S的action，hd和tl是列表的头和尾操作，null（L）为真，如果L是一个空列表，==r意味着这个定义是递归的。非正式地，TList对应于一个多动作，它等于一个动作组合对应于l的元素。最后证明了泵引理。这个引理表明，对于任何具有大小为n的有限载体的动作集S，如果某个多动作l从A到B（A，B S.car），则存在长度为n的多动作lJ也从A到B。事实上，根据鸽子洞原理，如果l有n个以上的元素，多动作l必须至少访问某个元素S.car两次。这意味着我们可以删除l中对应于从C到C的循环的部分，并获得一个更短的多动作，它仍然需要A到B。我们可以重复这个操作，直到我们得到一个足够短的多动作3.5确定性理论8这个理论给出了确定性自动机在一些字母表和一组状态上的定义。自动机被定义为一个过渡函数，一个初始状态和一个判断状态是否是最终状态的函数的三元组自动机（阿尔法;状态）==act：（States→Alph→States）×init：States×（States→B）其中B是布尔类型9。该理论还定义了返回自动机a的三个分量的运算δa、I（a）和F（a）。然后，该理论给出了自动机DA在处理输入字符串l之后处于什么状态以及输入字符串l是否被接受的定义：DA（l）==rifnull（l）thenI（DA）else（（δDA）DA（tl（l））hd（l））fiDA（1）↓==F（DA）DA（1）最后，REAcHDE c定理证明，它是可判定的10是否一些一个自动机DA的状态可以从I（DA）到达（参见6.2节3.6MYHILL7NuPRL系统使用Y-combinator实现递归定义。8http://nuprlauto.nogin.org/det_automata/9NuPRL使用命题作为类型方法，因此可能无法判定命题是否是判断是真是假。 另一方面，布尔类型只包含两个元素-tt和ff，并且布尔值是否为真是可判定的。10如果NuPRL证明t是一个函数，那么t必须表示一个全可计算函数。正因为如此，我们可以将命题P（x）在某个类型T上的可判定性定义为：x：T. P（x） P（x），这与依赖函数x相同：TP（x） P（x）。诺金611http://nuprlauto.nogin.org/myhill_nerode/诺金7∈∀⇔↓∈→首先是一个关系Rl L：x Rl L yi z：A List。L（z @ x）L（z @ y）（其中L是某种语言，@是列表追加运算符）被定义。然后证明了对任意语言L，R1L是一个等价关系. 对于使用函数定义语言的情况，关系Rgg的定义类似字母列表→B而不是谓词12。在这个理论中，还证明了MN23 LEM 1引理。MN23LEM 1指出，对于Alph列表上的任何等价关系R，使得对于任何x，y，z Alph列表，xR y暗示（z@x）R（z@y），如果R是有限的，则对于任何g阿尔法列表关于R，关系Rgg可判定性（参见第7节）。最后证明了Myhill-Nerode自动机极小化定理。有关证明的信息，请参见[4]。在这里我们将只概述从证明中提取的最小化过程给定一个自动机DA，首先使用从REACHDEc中提取的决策过程来获取可达状态。然后我们把xRy设为关系DA（x）=DA（y）（自动机在看到x或y之后进入相同的状态），g（x）设为DA（x），然后使用Rgg的等价类作为最小自动机的状态。最后，从MN23LEM 1引理中提取的决策过程被用来枚举状态。3.7图书馆的其他部分图书馆的其余部分包括非确定性自动机的定义和性质，证明存在一个确定性自动机等价于一个给定的非确定性自动机和其他定理。有关库的这些部分的信息，请参见[4]。4指数复杂性的来源在现有的证明[4]中，已经检测到指数时间复杂度的三个来源13：(i) 鸽子洞原理（见第4节和第5节）(ii) 状态可达性的可判定性（见第10和6节）(iii) 由自动机语言诱导的词的等价关系的可判定性MN23LEM 1引理-见第12和7节）现在，在对这些引理的证明进行分析和重写之后，所得到的提取程序变成了多项式。然而，它花了大约24小时来评估应用于某个小型自动机的旧版本最小化定理的摘录，而新的摘录应用于图12从字母表到命题类型P的函数。[13]我们不得不手动搜索指数复杂度的来源。希望Ralph Benzinger诺金8−≤- -在相同的计算机14上仅在大约40秒期间评估相同的自动机。最小化定理的当前证明说明了通过提取编程确实可以工作。5鸽子洞原理5.1性能对于从该原理的新旧证明中提取的算法，最坏的情况是当唯一一对i > j使得f（i）= f（j）是i=1，j=0。这就是为什么我们采用函数F=λx进行性能比较。if（x=0）then0elsex 1fi并评估了从应用于此F和不同n的证明中提取的内容。下表显示如何评估员花了很长时间才得到答案：n旧校样新证明107.6秒1.8秒1229.1秒2.3秒20>20分钟5.2秒5.2原始指数证明鸽子洞原理的主要部分在p洞辅助引理15中得到证明：n：{1.. . }。n= N（n+1）→Nn.n= N（n +1）。 {（i +1）} （n +1）−}。 fi = fj其中{1. }是正整数集合的NuPRL表示法，并且{m. n−}是{ i}的符号|m≤i定义为（x，y：（Alph List）//（xR y））（x，y：（Alph List）//（xRy））的等价类，其作用是λa：Alph。λuv。设u，v>=uv，a：：u，a：：v >。<<这个定义是有效的，因为uR v（a：：u）R（a：：v）。我们可以证明Sp：w u，v><=（作为等价类对）。然后，我们使用REACH引理来获得该动作集中从对u，v >“可达”的所有对的列表<然后，使用平凡列表归纳法，我们计算该列表中每个对的两个元素上的函数g，并检查列表中是否存在一个对，使得gui/=g vi。7.3多项式的另一个证明这个版本的证明MN23 LEM 1被称为MN23 LEM30。这个证明与前一个证明之间的区别在于，我们不是计算每对u，v >的“可达”元素列表，<28http://nuprlauto-b.nogin.org/automata_2/auto2_lemma_0www.example.com html29这个符号并没有出现在实际的证明中。30http://nuprlauto.nogin.org/myhill_nerode/mn_23_lem HTML诺金17¬¬所有对的列表，使得（u Rg v），然后检查我们的特定对是否在该列表中。首先，对于Sp.car的每个元素s，我们计算从s可立即到达的所有元素的列表，并将所有这些列表放入一个大列表列表中。然后，使用这些列表，我们为www.example.com的每个元素s计算Sp.car可以立即到达s的所有元素的列表（bac KLISTIFY31）。 然后我们取www.example.com的所有元 素 的 列 表 Sp.car ， 并 在 其 中 过 滤 这 样 的 对 ， 使 gu=gv（BOOLLISTIFY32）。然后，我们将其作为初始列表，并主要按照实际情况进行，但向后（使用bac KLISTIFY）而不是向前获得所有对的列表，使得最终（u R g v）。8进一步改进虽然从NuPRL自动机库中的新证明中提取的算法在小型自动机上工作得很快，但在自动机库和NuPRL系统本身中可以进行许多进一步的改进，以使证明更短，更快，更可读。以下是其中的一些(i) NuPRL评价器应进行实质性重写。目前的方法经常不必要地多次评估相同的术语。理想情况下，评估器应该变成一个编译器。(ii) 如果MN23 LEM在新的求值器上比mn 23 lem 1工作得更快（它在当前求值器上工作得更慢，因为它在需要时试图重新计算每个列表），那么应该使用它而不是MN23 LEM 1。如果我们利用Sp的特殊结构，从mn23 lem证明中提取的速度可以很容易地进一步显著提高-它可以被视为两个相等的较小动作集的某种乘积。(iii) 应编写新的策略，使编写有效的证明更加自动化。特别是，需要编写一种策略，在不破坏现有（可能是未完成的）证明的情况下，为归纳陈述添加一个新的存在量化器。这种策略相当于声明一个新变量。(iv) 应在制度中增加更多的归纳原则。例如，一个归纳原理允许我们对任何m n，而不仅仅是n−1，引用n=m的归纳假设。(v) 有限的定义变得非常不方便。最好是把“有限性”与平等的可决定性分开31http://nuprlauto.nogin.org/myhill_nerode/back_listifywww.example.comhtml32http://nuprlauto.nogin.org/myhill_nerode/bool_listify..HTML诺金18例如，使用以下定义：Fin（T）==FL：T列表。T. f（T，t，FL）FinDec（T）== F in（T）f（T，t，FL）f（T，t，FL）FinDec（T）== F in（T） Dec（t1 = t2 ∈ T）（在NuPRL中可以很容易地证明FinDec等同于当前对finite的定义）。如果自动机库用这些定义重写，那么许多引理的证明会更短（特别是FIN的INV是fin），最小化会更快，至少有一个新的求值器（如上）。(vi) 在库的当前版本中（以及以前的版本中）， 引入了一个新的抽象概念mn quo append，它等价于append，但具有特殊的良构引理。它在许多引理中产生了技术困难。一个更好的方法是证明append本身的一个额外的良构引理。确认我感谢罗伯特·康斯特布尔慷慨地分享他的观察结果，并指导我完成这项工作的所有阶段9附录这里是NuPRL证明的归纳步骤，从鸽子洞原理的原始证明（见第15节）。（省略了所有良构子目标的证明）。1.n：{2...}2.Nn→N（-1+n）.nn.{（1+i）} n−}。fi=fj3.f：N（n+1）→N n► n= N（1+n）。{（1+i）}（1+n）−}。fi=fj|决定，决定fn=fk|......这是什么？（a）|\| 4.nn.fn=fk| |1BY（D 4 THENM InstConcl [[k|;[n|]..）\4.n n.fn =f k）|BY（RWW“not_over_exists”4.（a）|4.nn.（fn=fk）诺金19|诺金20通过[λx：N n.if（fx = zn-1）thenfn elsefxfi|（D 2）THENMReduce（-1）|2.f：N（n+1）→N n3.n n.（fn=fk）4.nn.{（1+i）} n−}if（f i=zn-1）thenfnelse f i fi= if（f j=zn-1）thenfnelse f j fi|BY（ExRepD THENM InstConcl[[i|;[j]|[……（a）|4. i：Nn5. j：{（1+ i）.. n−}6. if（f i=zn-1）thenfnelse f i fi= if（f j=zn-1）thenfnelse f j fi► fi= fj|BY MoveToConcl 6 THENM SplitOnConclITES THENA Auto引用[1] 贝 茨 ， J.L. 和 R. L. Constable ， Proofs as programs ， ACM Transactions onProgramming Languages and Systems7（1985）。53比71[2] 本辛格河， Nuprl提取程序（2000），发表在Journal of Functional Programming上。[3] 康斯特布尔河L.，S. F. Allen，H.M. Bromley，W.R. Cleaveland，J. F. 克里默，R. W. Harper，D. J.Howe，T. B. Knoblock，N. P. Mendler，P. 帕南戈，J. T. Sasaki和S. F. Smith，[4] 康 斯 特 布 尔 河 L. ， P. Jackson ， P. Naumov ， J.Uribe ， Constructivelyformalizing automata theory，Proof，Language and Interaction：Essaysin Honour of Robert Milner，1998.[5] 康 斯 特 布 尔 河 L. ， T. Knoblock 和 J.Bates ， 编 写 构 造 证 明 的 程 序 ，J.Automated Reasoning1（1984），pp. 285-326。[6] Hopcroft，J.E.和j.d.Ullman，[7] Nordstrom，B.，K. Petersson和J. 史密斯，“ 马 丁 - 洛 夫 的 T y p e 理论 中 的 程 序 设 计 ” ， 牛 津 科 学 出 版 社 ， 牛 津 ， 1 9 9 0 年 。[8] 波 林 角 和 B. Werner ， Extracting and executing programs developed in theinductive construction systems，in：Proceedings of First Annual Workshop ofLogical Frameworks，Sophia-Antipolis，France，1990，pp. 349-361
我的内容管理
展开
