光辩证法解释斐波那契数的经典性存在

理论计算机科学电子笔记171（2007）43-53www.elsevier.com/locate/entcs从一个经典Fibonacci证明Mircea-Dan Hernest米尔西亚-丹·赫内斯特1，2信息技术学院F-91128 Palaiseau -FRANCE摘要我们展示了程序提取的光辩证法解释（LDI）的最小逻辑证明的经典存在的斐波那契数。这个半经典的证明可以在MinLog的示例库中找到。 Güodel的T extract的最终形式由LD I实现，它是一种自适应的递归算法，精确地定义了Fibonacci数（成对）。这一轻辩证法的结果是，通过纯粹的Güre D？lDialecticIn-intrepretation的方法来描述T -prog r a m e。它也严格地比通过Berger，Buchholz和Schwichtenberg的精化A虽然在语法上不同，但它也具有与原始程序相同的计算复杂度，原始程序是从未失真的输入经典斐波那契证明中进行精化A-翻译关键词：证明挖掘，从（经典）证明中提取程序，提取程序的复杂性，精炼的A-翻译，没有计算意义的量化器，轻辩证解释，复杂的假设性，Güodel的函数1介绍在过去的几年里，在从经典证明中提取程序的领域里，已经做了相当多的工作。虽然最近在经典分析证明的证明挖掘中已经获得了强有力的数学结果（参见，例如，[17，15，18，20，22]），计算机实现的程序提取元算法只能产生有限的结果，对于相当小的测试用例，即使这样，提取的程序也不是最佳的。这种情况在提取一个相当不寻常的，扭曲的算法来计算斐波那契数时会遇到，该算法是通过[ 3 ]的Berger-Buchholz-Schwichtenberg（BBS）改进的A-翻译来实现的。术语tBBS1ProjectLogiCal-PoleComund eRecherchenfrmiquedeS aclay，CNRS，Eol ePolytechnique，INRIAetUive sitePari s-Sud-France2电子邮件地址：danher@lix.polytechnique.fr1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.05044M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）43ofGéodelnallystronglynormalized[4，5]不仅不需要使用type-2Güodel递归（也存在于[3]的原始提取中），而且还使用了两倍的相应的type-2泛函，这严格增加了其计算复杂度。BBS的程序具有意想不到的指数时间复杂度，请参见第四节的结尾。另一方面，通过BBS技术提取的程序从最初的经典斐波那契证明概述[3]仍然是线性时间在自然数的一元表示，见[3]的完整技术细节。前一种类型的p-2循环为R（i→i → i） → i， 其 中（ i → i→ i）→ i的类型的平均值（degree）为2。这里i是基类型，表示自然数的集合IN，Rρ是所谓的“ty pe- ρ Géodel rec ur s or“的旋转，在Géodel的T 4中，它都具有pe ρ →（i → ρ → ρ）→ i → ρ的类型. 这是一个非常出乎意料的事情，因为斐波纳契数的通常递归定义（在p airs）可以在God el的T中通过一个类型p e - 0 G o delrecsoronly，namelyRoxi的方法来表达。他把σ×τ表示成σ和τ 的 形 式 。在factsuch中，T项实际上是在MinLog[25]中通过纯Modified Realizability从Fibonacci强（直觉）存在数字，见[3]5。从经典证明而不是构造性证明甚至纯粹的直觉证明中提取程序的努力的重点在于，（半）经典证明更容易和更直接地构建，无论是通过人脑还是在各种计算机实现的证明系统中。因此，期望通过更复杂的程序提取元算法6从经典证明合成的算法至少与通过更常见的提取技术7从相应的构造性/纯直觉证明产生的算法一样好当应用于半经典的MinLogFibonacci证明时（我们在此的意思是通过自动证明搜索获得的扭曲变体，存在于[25，11]中，以及不 是 手 动 的 ， 最 初 在 [3] 中 介 绍 ） ， 这 不 是 情 况 ， 对 于 BBS 重 新 定 义 的 A-translation，也不是对于纯粹的G-DialecticaInterprretation，正如我们在后面的续集中所展示的。这种情况的修复可以通过消除输入8处证明的失真或通过使用Berger在[2]9中的Kripke风格变体来为BBS精炼A翻译提供。后一种提取技术[3]这种人为失真是由于MinLog的自动证明搜索机制，相对于[3]中报道的经典斐波那契提取中最初使用的手动输入证明4 更多此类技术细节见论文[3]。[5]另一方面，这种线性-自然数的一元表示-算法优于其他对数算法，参见[24]这样的例子。[6]在这里，我们特别（但不完全）想到了《辩证法》（Dialectica）家族（见[23]，一部很好的统一著作）和《精炼的A-翻译》家族。[7]Kr eis el的M odified R e a liz ability [ 19 ]的一个简单易行的解释，它是Géo de el的功能（辩证法）解释[ 1，10 ]的一个简单易行的解释。[8]参见[3，24]或第4节的结尾，BBS从未失真的经典斐波那契证明中获得了原始程序的显示，该证明在自然数输入的一元表示中也具有线性时间复杂度。参见脚注18。9BergerM.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）4345实际上产生了与我们的《光辩证法》解释完全相同的程序（最初在[13]中介绍，但也可参见[14]，以获得更大和更统一的阐述）。[16][17][ 18][19]Goédel' s t e chni q u e c a n h e n d l e s u c h a n e x a c t r e a l i z e r e x r a t ra ITISTHE光辩证法解释（简称LDI），其中给出了解决方案。通过LDI提取的哥德尔T项，2MinLog中的半经典Fibonacci证明MinLog是H. Schwichtenberg和慕尼黑大学逻辑小组的成员。 它基于一阶自然演绎演算，并使用原始最小而不是经典或直觉逻辑。见[11，25]详细信息。定义2.1[斐波那契数]归纳定义通常是Base：F0：0，F1：1Step：Fn+1：<$Fn+Fn−1forn≥1，n∈ IN斐波那契数的例子是在MinLog中实现的，在[3]中通过纯Modified Realizability（来自通常的纯直觉证明）和BBS精炼A-翻译（来自斐波那契数的弱经典存在的最小逻辑证明;我们称这种证明为“半经典”）以及Modified Realizability进行了MinLog中的半经典Fibonacci证明是一个自然演绎证明，n∈ClkG（n，k）-其中n ∈ C l k G（n，k）：n ∈ C l k G（n，k）. G（n，k）→ G（n，k）→G（n，k ） ） -G（0，0）AND G（1，1）AND n，k，l. [G（n，k）<$G（n +1，l）] → G（n +2，k +1）.阅读和分析这个证明的最佳来源是MinLog分布[11]（或[25]），特别是由于使用自动化的证明搜索，这个证明不同于[3]的第6节中手动给出的证明。参见脚注18，了解如何在MinLog中构造这些半经典证明。通知在程序提取的上下文中，由轻辩证法解释，在下面第3节中，对G的假设表示为：G（0，0）AND G（1，1）AND n，k，l. [G（n，k）<$G（n +1，l）] → G（n +2，k + l），其中，n是没有计算意义的通用量化器，见下文。Hofmann [7]改进了A-翻译。它还进一步添加了所谓的统一量化器，用于46M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）433轻功能辩证法解读[ 1 - 3 ]中对哥德尔的“辩证法“基础理论的”简化“是对[ 10 ]中哥德尔的原始理论的最优化扩展“Dialectica Light”的主要特征（在[2]中被引入为Dialectica Light（缩写为LDI）是一个递归的句法翻译，从所有有限类型的半经典12弱扩展算术系统13（denotedWeZ，nc+）中的证明中，以纯粹的形式在有限类型中进行证明。项14（表示为WeZ），使得证明的结论公式中的强的正出现和的负出现实际上通过以下方式我在哥德的T。翻译过程也被称为“程序提取”。证明的LDI翻译包括以下公式的翻译：定义3.1通过无量化器（qfr）公式，我们理解了一个由素数公式在（to）和（t）中通过，→建立的公式，如果可用，- 是的在我们的系统中，qfr公式都是可判定的。存在布尔项与无量化器公式A0<$→tA0的唯一双射关联，使得► A0Participat（t A0）. 那么公式的LDI翻译是：AD：AD：at（tA）对于无量化器公式A（AB）D：x，uy，v[（AB）D：AD（x;y;a）BD（u;v;b）]（zA（z，a））D：z<$，x<$y[（zA（z，a））D（z<$，x;y;a）：AD（x;y;z<$，a）]（zA（z，a））D：Xz<$，y[（zA（z，a））D（X;z<$，y;a）：AD（X（z<$）;y;z<$，a）]（zA（z，a））D：xy[（zA（z，a））D（x;y;a）：z AD（x;y;z，a）]（zA（z，a））D：xy[（zA（z，a））D（x;y;a）：z AD（x;y;z，a）]（A→B）D：AD（x;Y（x，v））→BD（U（x）;v）这是一种方法，其中可以简单地给出具有相同类型z的新变量z。A D的自由变量正好是10论文[1]提供了一个很好的英文调查，其中包括对完整分析的扩展。[11]在[13]中，我们将这些特殊的存在性和泛量化器命名为我们在这里继续使用我们自己的术语。[12]这可以扩展到完全经典的证明，模一些双重否定翻译，见[14]。13SystemWeZ，nc+wa s ddWE−Z+in[13].这是一种新的简化方法，在[ 14 ]中有比较详细的说明，就像其相应的WeZ表一样，见下文。[14]系统WeZω，在[ 13 ]中表示为WE−Z−，是[ 26 ]的第1.6.12节中所有有限类型WE−HA ω中弱扩张Heyting算术的自然演绎公式。另请参见[3，24]，以了解详细的扩展范围ZZ+。M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）4347i=1i=1i=1i=1i=1i=1A的自由变量注3.2对于简单的辩证法解释，根式（或“根”）公式AD（它是与A相联系的LDI）不一定是无数量因子的，就像它对于纯粹的哥德尔的函数的情况一样。通常，所有ncm量化器与相应的常规量化器的映射。定理3.3（光辩证法[13]的精确实现子综合）存在一种算法，在输入时给出自然演绎证明，P：{Ci}nA15inWeZ，nc+，itevenut uunyproduesatut tthefolwing：(i) 设置{Ti}n的最大值和T，(ii) 变量的元组{xi}n和y，所有这些，(iii) 在WeZ中，PD：{Ci（xi;Ti（x，y））}n∈AD（T（x）;y）的一种新的证明方法，其中Dx：1，.，xn.此外，委员会认为，i=1• 变量x和y不出现在P中（它们都是全新的）• T和{Ti}n的可恢复性与A和{Ci}n的可恢复性相同– 我们称之为LDI不允许您在此执行的测试{Ti}n中重新加载此执行的命令和T.注3.4哥德尔在自然演绎设置中，收缩相当于在蕴涵期间释放开放假设公式A的至少两个副本（来自同一包16[A]. /B导论. 这是因为，对于所谓的A→B收缩17，A成为（原始的，即，尚未规范化）实现术语。所以，先验（即，已经在提取阶段）消除这些D相关收缩中的一些，而不是后验（即，在随后的强规范化处理期间），表示所提取的节目的重要复杂性改进我们在下面的第4节中重申我们的声明。4三种提取技术同样从下面的机器基准测试中可以立即看出，由Light Dialectica解释产生的程序明显优于al-[15]因此，从开放假设公式C1，. .，Cn. 这里，[16]在术语的意义上[9]。这与[ 24 ]中的“假设变量”概念相同[17]参见[14]，了解关于这个术语的全部细节，以及对《轻辩证法》摘录的广泛而统一的阐述。48M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）43出租m由BBS给出的refinedA-翻译18.而后者则比纯粹的Géodel辩证法解释的方法更精确，因为它包含了大量的冗余信息。 所有下面在原始MinLog输出的人工处理适应中呈现三个提取的（通过三种程序合成技术）项。见[11]为纯机器提取的程序。我们强调这样一个事实，即即使输入的经典斐波那契证明是来自[3]的原始的、未失真的证明，纯辩证法和轻辩证法的元算法的结果也将保持不变。只有BBS A-翻译的输出在使用其原始输入时会变得更好，见脚注18。我们的观点是，如果用户不能或不愿意优化输入证明，那么提取技术有责任处理这种实际上非常可能的人为情况并克服复杂性损失。看来BBS细化的A-翻译更直接地依赖于输入校样的形状，因此其性能随着人为失真而降低。这是因为BBS的解释是基于一个初步的证明翻译，其中字面上包括翻译的扭曲。随后，Modified Realizability从这样一个翻译的证明中逐字读出了证人，这无法避免保留扭曲。在扭曲的经典斐波那契证明的情况下，重复使用两次（基本上是归纳假设）asumpti onclk，l。G（n，k）∈G（n+1，l），在此期间，我们可以对的诱导步骤将产生2型功能H在BBS提取程序中，请参见下面的2）。相反，对于D-解释和LDI来说，人为的扭曲对w.r.t.是无害的。已经是原始的提取程序了。只有一个纯粹的逻辑收缩，不相关的已经为pureDialectica，overth ee eenassumptionpixellk，l。 G（n，k）≠G（n+1，l）将是一个连续的群. 无论如何，这种压缩没有计算内容，在D-解释的情况下已经如此，因为它的公式翻译有一个空的普遍方面，参见定义3.1和[13，14]以获得完整的技术细节。对于LDI，情况是相同的，没有使用任何特殊的量化器，没有计算平均值。ing.事实上，不仅这种额外的收缩，而且由人为扭曲产生的整个冗余证明分支在D解释和LDI下都没有计算内容。这就是为什么通过这两种技术提取的原始程序不受输入处证明中的冗余失真的影响，即，无论上述假设是否被使用过一次或两次，等等。这种不变的情况对于BBS精炼的A-翻译是不可能的，因为这种提取技术缺乏Dialectica解释的完整模块性（关于这个问题的扩展评论也见[12]），并且更依赖于证据（如上所述）。我们现在试图从理论上解释为什么LDI提取的程序比纯D-解释的程序性能好得多。正如备注3.4所暗示的，性能的差异是由（消除）18 这种情况只适用于更人工的输入证明。 当它的扭曲被消除时，使用（search 1）受限的证明搜索命令而不是仅使用（search），两个提取程序的运行时性能相当。这里（搜索1）意味着开放假设在想要搜索的证明中最多只能使用一次[24]见《明史》，《明史》。M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）4349一种计算上的D冗余收缩。这种收缩是由以下事实给出的：假设u：n，k，l。 [G（n，k）<$G（n +1，l）] → G（n +2，k +1）在经典Fibonacci证明的归纳步骤的证明中是开的。收缩是插入到要挖掘的证明中，与输入处原始证明中u的开放出现次数无关自然演绎中的辩证法解释机制实际上会使u的开放出现次数加倍，因此无论如何都会出现逻辑收缩。参见[14]，了解通过模拟一般归纳规则（因此也是归纳公理）而产生的这种收缩的技术细节，这些收缩是根据更特殊的归纳规则限制在无迭代的基础和步骤输入证明方面的。现在，我们的“轻”优化的结果是什么由于使用量化器而无需计算这意味着，在u中，它不是常规的“，”计算内容，这只存在于（三）定期的存在，在一个积极的立场。参见[14]中的术语和完整的技术细节。计算上的D-冗余假设u的开放出现的次数（在原始输入证明中）变得无关紧要，因为该假设无论如何都被忽略了。通过程序提取通过轻辩证法解释。随后的计算机基准测试是在运行Windows XPProf.操作系统的DELL笔记本电脑（型号X1，因此由英特尔迅驰CPU驱动）上进行的我们使用了更特殊的MinLog发 行 版 [11] ， 它 尚 未 与 官 方 MinLog[25] 集 成 。 作 为 Scheme 解 释 器 ， 我 们 使 用PetiteChez Scheme7.0a，参见[21]。通过Scheme的“时间”过程得到了计算时间和空间开销1) （MinLog，和apted）根据纯粹的哥德尔的辩证法..........................（add-var-name“n”“m”（py“nat”））（add-var-name“G”（py“nat=>nat=>boole”））（add-var-name“H”（py“（nat @@（nat @@ nat））”））..........................> t_{PDI} == [G，n]左右（（Recnat=>nat@@（nat@@nat）@@（nat@ @nat））（（0@0@0）@0@1）（[m，H][if[if（G左左H左右左H）[if（G（SuccleftH）right right leftH）（G（Succ（Succ leftH））(left右左H+右右左H））真]真的]（m@right H）（leftH）]@right rightH@左右H +右右H）n）的> (time（nt（mk-term-in-app-form t_{PDI}（pt“G”）（pt“5”）314个收藏品50M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）436031ms的CPU运行时间，包括676ms采集6110ms的实时运行时间，包括687ms采集已分配341280176个字节，包括回收的337674848个字节“5”> (time（nt（make-term-in-app-form t_{PDI}（pt“G”）（pt“6”）2700个集合56750 ms的 CPU运行时间，包括9676 ms的采集 58375ms的实时运行时间，包括10008 ms的采集已分配2937460672字节，包括回收的2933419728字节“8”2) BBS的结果细化为A-翻译（MinLog输出，改编）：..........................（add-var-name“i”“j”“k”“l”“m”“n”（py“nat=>nat=>nat”））（add-var-name“f”（py“nat=>nat=>nat”））（add-var-name“H”（py“（nat=> nat =>nat）=>nat”））..........................> > > t_{BBS} ==“[k]（Rec nat=>（nat=>nat=>nat）=>nat）（[f] f0 1）（[l，H，f] H（[i，j] H（[n，m]f m（n+m）k（[n，m] n）”> (time（nt（make-term-in-app-form t_{BBS}（pt“12”）39个收藏品813ms经过的cpu时间，包括109ms采集813ms经过的实时时间，包括107ms采集分配了42919528个字节，包括回收的39266296个字节“144”> (time（nt（make-term-in-app-form t_{BBS}（pt“15”）321件收藏品7094ms的CPU运行时间，包括1153ms的采集7203ms的实时运行时间，包括1246ms的采集已分配348911096字节，包括“610”回收的326154920字节3) Light Dialectica解释的结果（MinLog输出，改编）：..........................（add-var-name“n”“m”（py“nat”））（add-var-name“G”（py“nat=>nat=>boole”））（add-var-name“H”（py“（nat@@nat）”））..........................> t_{LDI} ==“[G，n]left（（Rec nat=>nat@@nat）（0@1）（[m，H]rightH @left H+rightH）n）”> (time（nt（mk-term-in-app-form t_{LDI}（pt“G”）（pt“15”）6个系列125 ms的CPU运行时间，包括0 ms的收集时间140ms实时运行时间，包括0ms采集M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）4351分配了6802576字节，包括回收的6383624字节“610”> (time（nt（mk-term-in-app-form t_{LDI}（pt“G”）（pt“20”）68件藏品1343ms的CPU运行时间，包括62ms采集1344ms的实时运行时间，包括63ms采集分配了73584536个字节，包括回收的71466424个字节“6765”>(time（nt（mk-term-in-app-form t_{LDI}（pt“G”）（pt“25”）750个集合16219 ms的 CPU运行时间，包括 2279 ms的采集 16657ms的实时运行时间，包括2331 ms的采集分配了816525224字节，包括回收的803991296字节“75025”请注意，上述时间和空间开销的具体定量测量对应于扭曲的经典斐波那契证明。对于Dialectica对于来自[ 3 ]的原始输入证明，或者通过（搜索1）（而不是无限（搜索））的有限自动搜索获得的证明，它们也是相同的。相反，对于BBS精炼的A-翻译，差异将相当大，因为从更干净的输入证明，线性时间程序的运行时性能相当等于的输出的LDI技术（尽管不同的语法形状）。在上面2）处显示的程序tBBS可以被写为如下的方案[21]程序（define（FiboBis n））（fibo2 n（lambda（kl） k）（define（fibo2 n1f）(if（= n1 0） （f0 1）（fibo2（- n11）（lambda（kk11））（fibo2（- n1 1）（lambda（kl）（f l（+ kl）回想一下，最初在[3]中获得的算法可以在Scheme中拼写为：（define（Fibo n））（fibo1 n（lambda（kl） k）（define（fibo1 n1f）(if（= n1 0） （f0 1）（fibo1（- n1 1）（lambda（kl）（f l（+kl））我们立即发现，在使用BBS技术时，为输入证明中的失真付出的代价相当大FiboBis算法是n的指数函数，因为调用n1上的fibo 2会导致两次递归调用n1-1上的fibo 2。5结论和未来工作应用哥德尔的辩证法原理的“轻”优化，应找到更多的实例。对于这些情况，需要进行一次协商52M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）43MinLog实现的Dickson引理的半经典证明这里，三个嵌套归纳产生三个收缩，因此这三个收缩都包含在三重嵌套递归中的提取项中。因此，立即可以看出，这样一个计划将是非常复杂的。不幸的是，光辩证法无法修复这种情况。引用[1] 再见，J。 和S。 Feferman，G？odel's fun cti o n a l（'Di a l e cti c a '）interp r et a t i o n，in：S. Buss，editorr，Handbook of Proof Theory，Studies in Logic and the Foundations of Mathematics 137，Elsevier，1998 pp. 337-405[2] 伯 杰 大 学 ， Uniform Heyting Arithmetic ， Annals of Pure and Applied Logic133（ 2005 ） ， pp. 125-148，Festschrift for H.施维希滕贝格[3] 伯杰大学，W. Buchholz和H. Schwichtenberg，Refined Program Extraction from Classical Proofs，Annals of Pure and Applied Logic114（2002），pp. 三比二十五[4] Berger ， U. ， M.EberlandH.SCHWICTENEV ALU ATI O N O R M A I ON EV ALUATI ON ： B.MülleranddJ. Tucker，编者，《硬件基础展望》，LNCS 1546，Springer Verlag，1998年，第1546页。117比137[5] 伯 杰 大 学 ， M. Eberl 和 H. Schwichtenberg ， Term rewriting for normalization by evaluation ，Information and Computation183（2003），pp. 19[6] 伯杰大学，H. Schwichtenberg和M.Seisenberger，Warshall算法和Dickson205-221[7] Coquand ， T. 和 M.Hofmann ， A new method for establishing conservativity of classical systemsover their intuitionistic version，Mathematical Structures in Computer Science9（1999），pp.323-333[8] Ferreira，F.和p.奥利瓦，有界函数解释，纯逻辑与应用逻辑年鉴135（2005），pp. 73比112[9] Girard，J.-是的，P. Taylor和Y.Lafont，[10] Güodel，K.，U？bereinebishernochnichtenu？teErweiterungdefinnitenStandpunktes，Dialectica12（1958），pp. 280-287[11]Hernest，M.D、 The MinLog proof-system for Dialectica program-extraction，免费软件，完整的源代码和文档@ http://www.brics.dk/和danher/MinLogForDialectica.[12] Hernest，M.D、比较两种技术的程序提取从经典的证明，在：M. Baaz，J. Makovsky和A. Voronkov，编辑，LPAR 2002：Short Contributions and CSL 2003：ExtendedPosters，KurtGüodelSociety' s Co l l e g i um Log i cum V III I（2004），pp. 99比102[13] Hernest，M. D、Light Functional Interpretation，Lecture Notes in Computer Science3634（2005），pp. 477[14] Hernest，M. D、“Feasible programs from (non-constructive) proofs by the light (monotone)解释，” 博士论文，E'co le Munich（LMU）的聚合物结构和联合国调查研究（2006年），编写，草稿可在http://www.brics.dk/和danher/teza/查阅。[15] 科伦巴赫大学，证明解释和证明的计算内容，讲座课程，作者网页上的最新版本[16] 科伦巴赫大学，在分析中分析证明，在：W。Hodges，M.海兰角Steinhorn和J. Truss，编辑，逻辑：从基础到应用，Keele，1993，欧洲逻辑讨论会（1996），pp. 225-260.[17] 科伦巴赫大学，Some logical metathormic with applications in functional analysis，Transactions ofthe American Mathematical Society357（2005），pp. 89比128[18] 科伦巴赫大学Oliva，Proof Mining：A Systematic Way of Analysing Proofs in Mathematics，Proceedingsof the Steklov Institute of Mathematics242（2003），pp. 136-164。M.- D. Hernest/Electronic Notes in Theoretical Computer Science 171（2007）4353[19] 克赖塞尔， G.， 解释分析通过构造性泛函有限类型，在：A. Heyting，editor，Constructivity in Mathematics，North-Holland Publishing Company，1959，pp.101- 128[20] 勒乌斯特河， Aquadra t i c r aticrateofasympticregul arityforCAT（0）-spaces，JournalofMem. Analy sis and Applications（2006），出现，可从Elsevier的“Science Direct”下载，出版中的文章，更正的证明。[21] Cadence Research Systems，Chez Scheme，http://www.scheme.com（2006）.[22] Oliva，P.，理解和使用Spector423 http://www.dcs.qmul.ac.uk/-434，可在作者的网页@ www.example.com e pbo/.[23] Oliva，P.，Unifying functional interpretation，Notre Dame Journal of Formal Logic（2006），即将出版，可从作者的网页下载[24] Schwichtenberg，H.，可计算函数的最小逻辑，从（经典）证明中提取程序的讲座课程可在作者[25] Schwichtenberg，H. 证据和程序提取系统www.example.com上的文档http://www.minlog-system.de。M INLOG，免费 代码和[26] Troelstra，A.，编辑，