提取程序的复杂性及其对形式化方法的影响

理论计算机科学电子笔记151（2006）75-91www.elsevier.com/locate/entcs执行抽取程序卢修斯·克鲁斯-菲利佩1葡萄牙里斯本Pierre Letouzey2德国慕尼黑大学数学研究所摘要众所周知，算法通常隐藏在数学证明中。 如果这些证明在证明助手中形式化，则称为提取的机制可以自动生成相应的程序。 以前的工作主要集中在获得一个程序，从一个形式化的基本定理代数内的Coq证明助手。理论上，这个程序允许计算多项式根的近似值。然而，正如我们在这项工作中所显示的，目前理论和实践之间存在很大差距。 我们研究了提取程序的复杂性，并分析了其不合理的原因，表明这是整个形式化方法的直接后果关键词：程序抽取，复杂性，构造实，代数基本定理，数学形式化。1引言有几种方法可用于软件认证。第一种，也许是最自然的，是从一个手写的程序开始，然后在一个合适的逻辑系统中正式地检查它，比如霍尔逻辑。但是，存在一种替代方法，其中不需要编写程序，而是获得1电子邮件：lc fili pe@gma i l。Com2Email：lettouzey@ l r i. fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.11.02476L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75它自动从数学证明。这种将证明自动转换为构造正确的程序的过程称为（程序）提取。从证明中提取程序的能力是柯里-霍华德同构的一个例子然而，在实践中，提取不仅仅是这种同构的应用在基于类型论的证明助手的情况下（如Coq [22]或NuPrl [13]），证明的内部表示是一个实际的λ-项，因此证明是一个函数程序;但在实践中，这些证明的大部分对应于逻辑证明，从计算的角度来看是为了获得现实的方案，提取的主要任务之一是识别和去除这些部件。十五年多来，提取一直在理论上进行研究，并被纳入几个证明助手，如PX [11]，NuPrl [13]，Min-log [8]，Isabelle [3]或Coq [18，19，14，15]。由于这些不同的工作，提取的校正现在通常被很好地理解，并且这种机制已经成为验证函数程序的选择框架此外，这个框架非常优雅。特别是，它允许人们统一构造性数学和证明函数编程。另一方面，评估和/或改善提取的程序的复杂性仍然是一个活跃的研究课题。NuPrl [2]研究了提取程序复杂度的自动分析。同样值得一提的是最近的一些尝试，以确定哪种证明的限制可以确保最终提取的程序在时间上是多项式的[1]。到目前为止，大多数关于程序提取的实验都是针对计算机科学中的例子。在本文中，我们专注于一个不同的问题：从一个数学语句的形式化提取的程序的计算行为正如我们将要展示的，这个例子提出了与前面提到的完全不同的问题，这既是由于它的不同性质，和它的大小，结果并不令人满意。本文中描述的工作部分包含在作者的博士论文[ 5 ]和[ 15 ]中1.1C-CoRN文库在这个实验中，我们使用Coq证明助手。更具体地说，我们研究了它的提取机制的行为时，应用于代数基本定理的构造性证明[10]，C-CoRN [6]的一部分。C-CoRN是自1999年以来开发的证明助手Coq [22]中形式化的数学库。目前，它已经达到了一个合理的规模，使其成为一个适合大规模实验的环境L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7577C-CoRN涵盖了不同的学科，包括代数，实分析和一般拓扑。从程序提取的角度来看，大多数这些都不是很有趣，因为它们处理的结果很少或没有计算内容。因此，重点放在图书馆的两个具体部分：代数基本定理的构造性证明，在[10]中描述，以及R作为有理数的柯西序列的模型，其形式化是[9]的主题。代数基本定理（FTA）指出，复数上的每个非常数多项式都有根。在C-CoRN中对这种状态的证明是H.Kneser [12]，体现了由于这个原因，从这个证明中提取程序的问题不仅是一个重要的案例研究，而且也是一个计算上有趣的问题。关于这一点的更详细的讨论可以在[10]中找到）1.2从C-CoRN中将Coq提取机制应用于C-CoRN并不容易。其中一个原因是第一次尝试时提取机制的原始状态。另一个原因是库的大小，比以前做的任何测试都大几个数量级最后，C-CoRN最初并没有考虑到提取，这被证明具有重要的后果，如[7]中所指出的：获得合理大小的程序需要重新考虑Coq排序的使用3，形式化和微调的几个证明和定义，在原来FTA的证据到目前为止所做的所有工作都成功地提取了一个合理大小的程序本文建立在这项工作的基础上，通过研究当人们试图编译和执行从C-CoRN中FTA的形式化中提取的根查找程序时会第2节讨论了在编译提取的程序时遇到的一些问题以及如何解决这些问题。然后，事实证明，编译后的程序太慢，在执行时没有产生任何输出，因此第3节和第4节集中在两个较小的例子上，这些例子足够简单，可以理解提取的代码，同时展示了较大程序的基本问题。在第5节中，我们提出了同一定理的不同形式化，由第二作者与[3]在这种情况下，讨论什么是Coq排序并不重要;人们可以把Coq排序看作78L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75H. Schwichtenberg;这种形式化从根本上不同于C-CoRN，因为它是基于[ 21 ]考虑提取的。在第6节中，我们比较了从两种形式化中提取的程序，并表明前面确定的问题是基本问题;因此，从C-CoRN中提取的程序几乎不可能产生可执行的（实际上）程序。2提取程序将从C-CoRN中的FTA证明中提取的源代码编译成程序并运行它在[7]中没有完成在本节中，我们将讨论在此之前必须解决的一些技术问题。提取的目标是为真正的编程语言生成代码在2003年之前，Coq提取机制只能为FTA生成提取的代码，这些代码无法用通常的Ocaml或Haskell编译器编译。这是由于Coq的类型系统非常丰富，它允许ML类型系统中没有对应的功能。例如，可以根据术语定义类型，或者在记录结构中嵌入类型这两种情况都大量用于描述C-CoRN中的数学概念因此，提取的然而，同时，提取的正确性保证了提取的代码（尽管是错误类型的）将始终正确地求值。解决这些问题是最近重新设计Coq提取的主要动机之一[15]。在[20]之后，这已经通过使用不安全的类型更改原语（如Ocaml中的Obj.magic）来完成。在计算级别上，这个函数是透明的：它的参数返回不变。但它对打字有一个戏剧性的影响：Obj.magic，其类型是’a像[20]中那样到处使用目标魔法并不令人满意，原因有几个。首先，提取的代码的可读性降低;其次，编译器的一些优化可能被禁用;最后，来自ML类型的额外正确性属性丢失，需要强烈依赖提取的正确性结果由于所有这些原因，提取只在提取的代码中会出现无法键入的表达式的精确位置插入Obj.magic[15]的第3章描述了该插入机制的详细信息从FTA的证明中提取的代码现在包含大约400次Obj.magic。Ocaml编译器接受此代码，L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7579−任何额外的修改。最后，在提取到Haskell时使用了相同的方法，使用名为unsafeCocks的不安全类型。3计算机e在上一节讨论的编译问题解决之后，我们第一次能够执行从FTA证明中提取的程序因此，我们将x22定义为复平面上的多项式，证明它是非常数，将此证明提取给Ocaml，并将其作为FTA程序的参数。一个星期后，该计划还没有完成执行。不幸的是，这个程序太复杂了（大约250Mb），无法直接检查相反，我们决定将注意力集中在来自C-CoRN的更简单的例子上，我们可以检查这些例子，并从中获得更广泛的见解。在本节中，我们将重点讨论其中一个简单的例子：e的计算。虽然它的值与FTA的证明无关，但e是C-CoRN中实数的最简单例子之一，因为它被定义为有理数序列的极限。3.1改进提取的程序在C-CoRN中，将realnumb定义为有理数的Cauchy sequationsn ces，see[9]。∞1特别是，e被定义为级数的和，它展开为n=0n！λn的部分和序列的极限。1/n！;因此，e为由相同的部分和序列（有理数序列）表示从这个定义中提取的程序是一个函数，它具有自然的性质，返回Cauchy序列中的第n个元素代表E。第一个结果一点也不乐观：计算e的前五个近似值几乎是瞬间的;第六个需要几秒钟;第七个在一个这个问题很容易找到：收敛到e的序列使用Coq的自然数（皮亚诺数）形式化，这意味着要计算第n次近似的e首先计算k！对于0 ≤k≤n，作为0的第m个子，对于某个m，将结果转换为实数1 + 1 +. +1个（m次），计算它的倒数，然后把所有的东西加在一起。Fur-pouches，k的证明！也需要f= 0来计算这个倒数，这再次展开为一元符号中阶乘的计算。一旦这个问题被识别出来，就很容易解决了：我们不是在N中计算阶乘并将结果注入R中，而是直接在任意环中使用其乘法定义阶乘。接下来，我们通过归纳证明了80L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75你好！你好！这个函数总是非零的，得到一个证明项n是线性的。这些变化使我们能够计算e的前15个近似值，但是每次额外的迭代的执行时间大约增加了10倍。对R中注入N的定义和R本身的模型进行了一些特别的改进，使这个因子达到了2左右。这仍然远远不能令人满意，因为这意味着只能计算出大约20个e的近似值此外，分析显示，大多数时间程序都在计算λx的值。0表示x的值越来越大，这似乎是C-CoRN中定义实数的抽象方式的结果这个问题将在第5节中再次提及。实际上，为了计算一个像1这样的实数，投入这么多的运动是很尴尬的。毕竟，这个数只是一个有理数，所以更自然的做法是直接在有理数的结构中进行计算，然后将结果注入实数。这不能直接完成，因为C-CoRN强制在实数的抽象结构和它的任何具体对应物之间进行强分离。使用实数的所有部分的发展，就像FTA本身的证明一样，是通用的：它们依赖于一个公理，说明实数结构IR的存在，并且这个结构只是已知的阿基米德有序场，其中所有柯西序列都允许极限。因此，我们只能根据底层结构访问最小的原始对象和基本属性集。特别地，已知的本原实数只有0和1，它们分别是半群和环的基础结构的单位要在IR中引用有理数，必须从0，1和操作+，第三，最后一项操作还需要一份非无效证明，论点这样的证明通常是从严格正性的证明推导出来的(or消极性），这必须建立在一个基本属性的限制核心在IR上的严格序的情况下，这些性质是：反对称性;<传递性;与加法和乘法的相容性;以及x yParticipxyParticipyx. 任何其他属性，如0 1，都不是原始属性，<而是从上面的那些衍生出来的。 这同样适用于更复杂的证明像0n！;<因此，即使有最好的优化，也不能在通过一个简单的从有理数到实数的注入。另一方面，C-CoRN还提供了上述实数结构Concrete R的具体构造，确保实数的这种公理化是连贯的。一个有理数q可以通过具有常数值q的柯西序列立即注入到混凝土R中。同样，不等式a b的证明在具体R中也很简单，因为我们现在可以得到定义：应该存在严格的正比-L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7581在两个比较的柯西序列中，所有秩大于N的项总是相隔至少1/2。特别地，对于两个有理数q qJ，我们通过取<0. 从构造上讲，这是不可能的，因为没有算法可以确定任意实数的符号（如果这个数恰好为零，算法可能永远不会终止）;因此算法必须首先找到区间应该分裂的点cIVT有几种结构化，最初在C-CoRN中形式化的是最普遍的一种。为了证明函数f满足IVT，假设对于任何给定的y和区间I，总有一个点xI使得f（x）=y是足够的。利用这一点，上述证明可以修改如下：而不是采取[a，b]的中点，选择在[（2a+b）/3，（a+2b）/3）]中的点c使得f（c）0;那么我们可以决定无论f（a）f（c）>0或f（a）f（c）0，并如上所述进行<收敛比经典情形慢，因为区间的长度现在只缩小了三分之一，但这并不很重要。profiling揭示了大部分执行时间都花在寻找非常数多项式不为空的点上，正如上述方法所要求的那样。这是通过将每个多项式重写为规范形式，通过给定区间内的几个点上的值对其进行因式分解，然后重复应用代数运算的可拓性来完成的：如果和或积不为零，则其中一个被加数或因子也必须为非零。为例如，在区间[0， 3]上的x22被扩展成以下等价多项式：.x−3。x−9Ω。x−3。- 是的- 是的Σx−9x −3x −6232416−3−314444−4494 4162 4该计划的效率低下也就不足为奇然而，IVT有更好的构造变体，更适合于计算实数的根特别是f xn-c（neededdtocoinputenc）的since多项式增加，我们可以使用IVT来增加函数：如果f在[a，b]上增加，那么我们已知f（（2a+b）/3）0或f（（a+2b）/3）0（与实数的符号不同，最后一个析取可以在有限时间内确定：由于f（（2a+b）/3） y的证明Xnc > ync（对于x，y > 0，c >= 0和n①的人。 改变这个证明项是非常简单的，因为它只是一个适应为e所做的工作的问题。然而，结果与以前完全不同：虽然第一次迭代所需的计算时间大幅下降，但每一步仍然增加了两倍。仔细研究正在发生的事情没有多大帮助。profiling表明，大部分时间都花在了（二进制）整数的加法和虽然这部分可能是我们正在使用的具体模型的结果，并且肯定值得尝试其他模型，但瓶颈似乎是整个C-CoRN使用的抽象方法。由于IVT证明中使用的许多相关结果都是针对任意环的，因此在提取时，它们产生相对不精确的程序我们将在第6节和结论中再次讨论这些问题4.2提取程序该程序的最后一个版本被提取到Ocaml和Haskell中。这一次，执行时间的差异是惊人的：Haskell程序在250倍的时间内运行一个b。然而，内存消耗更高，每一步都翻倍，这是不可持续的：2的第12次近似需要超过2Gb的RAM内存，这是我们用这种方式计算的极限，它只能给出三个正确的数字。当同样的算法在Mathematica中实现时，它的性能与提取的程序的性能完全不可比较：它在线性时间内计算（可预测）。图2中给出了精确的执行时间。5另一种方法上一节表明，即使在重要的优化之后，前代程序也无法在速度上与不安全的手动编写的程序竞争。在本节中，我们将分析这一结论对C-CoRN的特异性，以及我们是否可以从中获得关于提取的更一般的经验教训为L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7585→迭代Ocaml（s）Haskell（s）Mathematica（ms）Ocaml/ Haskell20.13<0.010.211-41.420.010.341142614.310.060.5512398165.760.660.711251102008.008.340.891241√图二. 计算程序的执行时间2为了达到这个目的，我们现在描述另一种构造性实分析的Coq形式化，它是在考虑抽取的情况下开发的。这种形式化是与H.Schwichtenberg，谁愿意实施他的演讲笔记的一部分[21]。这个小而quickly-madedevelopmentwatmentobeanewCoRN;rather，itjust专注于一个特殊的问题，2的计算，并解决了它，直接从提取的角度考虑建设性的现实，不像自由贸易协定，提取的想法只是后验的。有了这一点，我们就有了一个程序，可以把一个p-在不到3分钟的时间内，以超过40个正确数字逼近此外，这个程序使用了与从C-CoRN中提取的原理相同的原理，即寻找x2−2的根。应该强调的是，这种形式化是不完整的：当我们专注于获得一个提取的程序时，我们忽略了几个逻辑证明，并将它们作为公理。这一发展应被视为一个概念的证明，允许测试几个想法。然而，用这种方法得到的提取程序是独立于这些未完成的部分的：完成它们只会给这个程序增加一个正确性的保证我们现在描述使这个小实验比从C-CoRN中提取更成功的关键点。5.1有理数在这个项目中，我们重用了C-CoRN的有理数，并做了一个重大改进。在C-CoRN中，对Q的运算从未将分数还原为标准形。因此，计算的分数，例如，在计算期间，E在不需要的情况下非常快速地增长虽然经常简化分数也可能是危险的，因为这也有成本，但我们的实验发展表明，没有可能的模糊性，通过简单的方法加快速度，可以充分简化：2的三位数，我们能够快速计算出几百分数的简化是由一个函数Qred完成的：Q Q，它计算分子和分母的gcd，并将两者除以这个gcd。86L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75√→→ →→−knumber. 我们证明了Qred返回的任何分数（数值上）都等于初始分数，并在主计算循环中插入Qred，2.需要进行更彻底的测试，以确定在每个基本运算中放置一个Qred是否更好，或者相反，更少地使用它。受此启发，我们尝试在C-CoRN形式化中添加类似的功能这确实导致了加速，但增益因子远小于我们预期的，因此我们放弃了这个想法。5.2柯西序列与C-CoRN的另一个主要区别是柯西序列的定义其中，x是柯西序列，如果好吧你好m，n> N. |≤2。|≤ 2.在[21]中，界限N被明确地给出为k的函数，最后一个函数被命名为柯西序列的模。这两个公式从构造性的观点来看是等价的，因为我们可以从证明N（k）开始找到模N（k）。你好. 然而，更明确的公式化的模数鼓励人们仔细选择它，我们这是一个可能发生的情况。一个接一个的过程中，通过所提取的程序计算2的近似值，直接获得用于该结果的最大误差范围。当一个人把钱给了如果程序是n，则结果在2的2−n以内，否则，我们得到n正确的二进制数字。在实践中，我们甚至得到一些额外的正确数字由于序列模计算中的近似，但数量级是正确的。相比之下，在C-CoRN中的e的计算期间，实验清楚的是，秩k的近似，即，柯西数列的第k项，为我们提供了n个正确的十进制数，但k和n之间的关系并不明确。此外，如果将其明确表示，由于C-CoRN中边界的选择通常是幼稚的，出于这个原因，本文中提到的误差估计是使用Mathematica进行后验的5.3连续函数连续实函数的定义也明显不同，[21] C-CoRN。在后者中，连续函数是具有某些性质的函数R R。因为R是柯西序列的集合，所以这简化为（N Q）N Q类型的对象。将函数作为第一个参数是不可取的，因为它会使提取的代码更复杂，分析起来更微妙，并且可能效率更低另一种选择是，L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7587使用一族收敛到期望的实函数的有理函数;因此，函数现在是类型N→Q →Q的对象。从这些表示问题中抽象出来，底层算法与第4节中的算法相同。特别地，我们在这里还使用专门用于单调函数的IVT的变体。不同的是，现在我们定义了一个严格的最小所需对象集，并且我们没有在实数和结果之间引入任何抽象层，如IVT。例如，我们没有表示R是一个场，因为除法是无用的。因此，提取的程序是：• 短：由于对极小值的追求，最终代码只有600行，比从C-CoRN中提取的代码少15倍;此外，该代码的3/4由Coq库函数组成• 简单：主循环由20行相当清晰的代码组成，没有使用复杂的结构（不像C-CoRN）;提取的程序可以直接类型化，不需要使用Obj.magic;• 快速：使用这种方法，计算40位数大约需要三分钟;当然，这仍然比Mathematica中的计算慢，因为用于编码任意精度整数的数据结构不同，但这仍然比从C-CoRN中提取的程序快得多这清楚地说明了表示选择对提取代码的效率的影响，即使这些表示从数学的角度来看是同构的。6抽象与计算上面的讨论表明，我们应该缓和我们对Curry-Howard同构的一个初始状态首先，一个好的数学证明应该在尽可能通用的环境中完成，而不依赖于特定的数据表示。但是对于程序来说，一个更快但限制性更强的算法比一个更慢但范围更广的算法更可取此外，数据表示的变化对程序的效率有很大的影响，以及是否允许高级部分访问低级表示。两个过程之间的差异的一个简单和说明性的例子是整数表示的选择从编程的角度来看，使用二进制整数显然是最好的选择，因为它们会产生88L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75更高效的功能。然而，从数学的角度来看，从皮亚诺（一元）整数导出的归纳原理是通常的归纳原理，而从二进制整数导出的归纳原理在实际中使用起来非常笨拙。这种差异的另一个例子，在C-CoRN中无处不在，是使用c-coons。在数学中，通常的做法是通过包含来识别子结构与它们的图像，例如有理数与它们到实数中的注入，并将代数结构视为较弱的结构，例如。 将环视为一组。明确所有这些无声的同构和注入将把数学变成一场永久的噩梦;因此，Coq提供了一种强制机制，为这些实践提供了精确的含义。这些函数是一种语法工具，允许用户编写更少的代码，但在内部它们只是普通的函数，不会显示给用户。但是，它们在提取后再次出现。在C-CoRN的具体情况下，有一个从setoids到复数的10个叠瓦状代数结构的链，提取的代码包含了数千个显式子：唯一的实数表达式0 + 1需要写三行。尽管这些插件对执行时间的影响可以忽略不计，但它们使代码不可读，从而阻止了对代码的任何详细分析最后一点涉及到可能希望集成到提取的代码中的优化在我们的框架中，这些优化必须在证明级别上进行。实验表明，这既不自然，也不容易。例如，有经验的程序员会避免用相同的参数编写两次相同的函数调用，并将这些调用与let in构造分组;但在证明中，重复使用相同的假设是常见的，然后提取的代码最终重复相应的计算。在递归函数的上下文中，这极大地改变了程序的复杂性-这当然是FTA程序当前不合理的一个主要解释。不幸的是，这个程序的大小目前阻止任何人尝试自动分解所有冗余此外，当一个人知道用let in分组什么时，通常可以相应地修改证明;但是对于更微妙的优化，证明可能需要完全重做。操纵，维护和改进程序携带证明当然不像直接操纵程序那么容易。L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75897结论虽然程序提取不是一个新的主题，但在这个领域的实际工作仍然很少。已经有一些实验，但它们通常涉及小的形式化，这可以通过为更大的测试用例构建足够大的库所需的时间投资来解释因为这个原因，我们的知识是真实的。这个C-CoRN库有近4000个引理和100000行代码，是Coq网站上任何其他用户贡献的两倍FTA的形式化证明大约占C-CoRN的一半;虽然我们无法检查从该特定证明中提取的程序，但我们讨论的较小的例子仍然比例如，[17 ]第10段。[23]中的工作在规模上与我们的工作相当，但它建立在专门从提取中发展出来我们的工作也与其他实验不同，因为它涉及一个数学陈述的证明，该陈述体现了数学中使用的算法，而以前在程序提取方面的工作主要是处理计算机科学中的例子。我们所讨论的结果在某些方面是有希望的，而在另一些方面则是令人从积极的一面来看，获得数学正确的程序的重要性怎么强调都不过分，特别是当这些程序包含非平凡算法时，例如FTA证明中的根查找算法此外，性能的程序计算e是非常令人印象深刻的，虽然当然不能与计算机代数系统。对然而，从以下四个版本中传输一个新的可执行程序，的FTA是超越了目前可以做的：简单地计算2与两位小数的精度占用了所有可用资源。其中一个问题，强烈的性能，提取的程序是实数结构的使用。在C-CoRN中，迄今为止唯一实现的是将实数定义为有理数的柯西序列，后者形式化为一个整数和一个正整数的配对这种方法非常抽象，其结果是实数上的一些简单函数不是最优的。我们认为这是我们工作的局限性之一;在不久的将来，我们计划使用[ 16 ]中描述的Stern-Brocot表示来实现实数，但在撰写本文时，提取的目标语言也很重要。Coq提取机制允许提取到两种语言，即Ocaml和Haskell。原则上，相应程序之间的差异应该很小，除非提取利用了语言的特定结构，如Ocaml的记录;实际上90L. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）75√在语义和这些语言的实现中，可能导致所提取的程序的相当不同的行为。一个很好的例子是Ocaml和Haskell在性能上的巨大差异。2. 对 这 些 挑 战 的 更 透 彻 的 理 解 需 要 通 过 更 多 的 测 试 、 分 析 和 与Ocaml/Haskell专家的讨论来实现最大的问题是程序提取是否真的是免费的。Al-ready [7]指出，获得一个合理大小的程序需要在几个地方改变证明;使程序在合理的时间内运行需要更多的改变。从形式化的角度来看，这些变化中的大多数都是有意义的，但我们似乎不太可能学习如何以不需要这些变化的方式开发形式化-除非提取从一开始就是一个目标虽然有一个相对定义良好的“有效程序”的概念正如第5节中的讨论所指出的，以提取为目标来重新证明IVT产生了一个比现有形式化的所有优化都好得多的程序最后一点值得一提的是提取的程序本身。令人惊讶的是，它看起来完全不像任何人都会编写的程序致谢第一作者得到了FCT资助SFRH/BPD/16372/2004和FCT和FEDER通过CLC项目QuantLog POCTI/MAT/55796/2004的支持。委托人会喜欢汉克·H。Barendregt，J. -C. 我会去的，H. 去吧，M. 尼基角Paulin，H.施维希滕贝格湾Spitters，D.Synek和F.Wiedijk感谢他们的意见和帮助，在整个开发这项工作。引用[1] K.艾利格大学Berger，M. Hofmann和H.施维滕贝格一种非递增多项式时间计算的算法。理论计算机科学，318：3[2] R.本辛格Nuprl提取程序的自动复杂性分析。Journal of Functional Programming，11（1）：3[3] S.伯格韦尔高阶逻辑中的证明、程序和可执行规范。PhD the sis，In stit i tutfur？rIn formatik，Techn ischeUn iversit？atMu？nchen，2003.[4] P. Callaghan，Z. Luo，J. McKinna，and R.波拉克，编辑。证明和程序的类型，2000年国际研讨会论文集，LNCS第2277卷。Springer-VerlagL. Cruz-Filipe，P.Letouzey/Electronic Notes in Theoretical Computer Science 151（2006）7591[5] L.克鲁兹-菲利佩构造性实分析：类型理论形式化及其应用。博士论文，奈梅亨大学，2004年4月。[6] L. Cruz-Filipe，H. Geuvers和F.快C-CoRN：Nijmegen的建设性Coq库。以. Alzheiti，G.Bancerek和A. Trybulec编辑，数学知识管理，第三届国际会议，MKM 2004，LNCS第3119卷，第88- 89103. Springer–Verlag,[7] L. Cruz-Filipe和B.小喷壶。从大型证明开发中提取程序。In D. Basin和B. Wol Wan，编辑，高阶逻辑中的定理证明，第16届国际会议，TPHOLs 2003，LNCS的第2758卷，第205-220页。Springer–Verlag,[8] H.工作中的证明理论：Minlog系统中的程序开发。在Wolfgang Bibel和Peter H.施密特，编辑，自动演绎：应用的基础。 第二卷，系统和实施技术。Kluwer Academic Publishers，Dordrecht，1998.[9] H. Geuvers和M.妮基Coq中的构造性实：公理和范畴。在Callaghan等人[4]，第79[10] H. Geuvers，F.Wiedijk和J.茨瓦嫩堡不用有理数的代数基本定理的构造性证明在Callaghan etal.[4]，第96[11] S. Hayashi和H.中野PX，一种计算逻辑。技术报告，京都大学数学科学研究所，1987年。[12] M.Kn eser. Ergéanzung zueeinerarbeitvonhelmuthkneseruberde nf undamentalsatzder代数。数学杂志，177：285[13] C. 克赖茨Nuprl Proof开发系统，版本5。康奈尔大学，伊萨卡，纽约，2002年。可在http://www.nuprl.org上获得。[14] P. Letouzey。一种新的提取方法。In H. Geuvers和F. Wiedijk，编辑，Types for Proofs andPrograms，Volume 2646 ofLNCS，pages 200[15] P. 我去看你。Programionfunctionnellecertii'e- L ' ext r a ct i o n d e p r a m e s d ans l ' ass i stan t C o q.PhDthesis，Univeresit'eParis-