Coq证明中的程序复杂性自动分析

理论计算机科学电子笔记153（2006）35-53www.elsevier.com/locate/entcs从Coq证明中抽取的程序复杂性自动分析许伟文2LIX，E‘colePolytechnique91400Palaiseau，France摘要我们描述了一个自动的复杂性分析机制，从证明进行证明辅助Coq的程序提取。通过提取，我们指的是自动生成MiniML代码[3]。 通过复杂性分析，我们指的是根据MiniML程序执行所需的步骤数量自动生成对程序时间复杂性的描述。这个描述可以是封闭程序的自然数，也就是说，程序与它们的实际输入一起出现。对于程序本身，描述是根据一组递归关系给出的，这些递归关系将计算的步骤数与输入的大小联系起来。 从这些递归关系到实际的复杂性函数是一项艰巨的任务，需要使用复杂的符号计算工具。虽然我们在某些情况下手动使用了MAPLE计算机代数系统，但这一部分暂时没有实现保留字：定理证明，程序抽取，复杂性分析1介绍1.1背景一个市场正在慢慢建立在该地区的证明发展系统。银行业务中的安全应用程序现在需要对计算机应用程序有高度的信心，这只能通过使用验证检查器证明代码正确来实现。在这个市场上最成功的公司之一是TrustedLogics，其技术基于Coq。安全1这项工作得到了RNTL项目AVERROES和法国电信的部分支持。2Email：xu@li x. polytec h ni qu e. fr1571-0661 © 2006 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.08.00536J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35应用程序，证明某些代码在其规范方面是正确的，或者从该规范的证明中提取它是不够的。它还必须照顾到环境。特别是对于智能卡应用，这意味着有限的资源量。因此，正确性证明应与程序运行所需资源的数量分析相结合。在这里，我们考虑从Coq证明中提取的程序。我们选择提取程序而不是证明程序有两个原因）。首先，我们知道代码是函数语言MiniML的一个定义良好的子集。对于第二个问题，我们的直觉是证明比程序本身携带其中一些属性可以帮助复杂性分析。我们还没有利用这种直觉，但将在结论中详细说明人们可能会想到将复杂性分析的工作委托给用户，用户将在证明程序正确的同时证明程序的复杂性属性。我们不相信这种做法。 做证明是困难的，趋势是让用户因此，我们认为复杂性分析应该是自动的。我们也可以固定在给定计算中花费的时间的界限，并预先使用输入的测试集进行计算，以估计哪些输入产生相对于界限安全的计算。 这种方法与测试非常相似，众所周知，构建完整的测试集非常困难，可能与进行证明一样困难，但会导致较低的安全级别。另一方面，对于命令式程序的自动分析，特别是一般情况下的分析，人们已经做了大量的工作。这种方法现在已经很成熟了。递归程序的行为是由递归方程表征的，如果没有封闭的形式可以描述预期的复杂性函数，其数学分析允许研究程序的渐近行为事实证明，对命令式程序的计算行为的统计分析已经比函数式程序的最坏情况复杂性深入得多。原因之一是函数式程序没有一个被广泛认可的操作模型。在社区中仍然存在一些争议，评估策略是否应该按值，按名称，懒惰，严格等，此外，计算程序执行中的步骤数可能被视为运行时花费的时间的非常粗略的近似值，因为不同的步骤可能需要非常不同的时间。然而，一些作者已经考虑了这个问题。最成功J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）3537一个是Benzinger，他推导出了递归关系，该关系将函数程序执行中所需的步骤数与其输入的大小相关联[2]。然而，他在NuPRL项目中的实施非常有限。只考虑以自然数或列表作为输入的程序。1.2问题我们的计划是建立通用工具，用于分析用MiniML编写的函数程序的复杂性我们不仅对时间复杂度感兴趣，而且对空间复杂度感兴趣。我们知道后一种分析应该比前一种更困难，因为程序使用的空间非常依赖于编译器技术。最后，我们不感兴趣的程序的行为是指数（或更多），但在程序的实际复杂性是由一个多项式的低程度。1.3贡献我们的贡献是一个正式的框架和实现，使我们能够计算一个给定的MiniML程序的复杂性的描述。作为程序的操作语义，程序的复杂性应该是组合的. 这导致修饰描述操作语义的规则 通过一些复杂性信息，然后允许通过评估这些规则来计算封闭程序的复杂性。对于带有变量（或参数）的项，复杂性当然取决于这些变量的值。如果这些变量是高阶的，它还取决于将实例化这些变量的实际函数的复杂性。对于这样的程序，我们的方法产生一个符号描述这个复杂性，然后可以转换成一个更方便的格式：递归关系。这个方法在OCaml中部分实现。用计算机代数系统分析递推关系一般还没有做过，但可以在足够简单的特殊情况下进行2注释语义计算复杂度是指函数的输入大小与计算输出所需时间之间的渐近关系。大多数计算复杂性的正式定义都是基于图灵机或随机存取机模型，并将某些成本分配给指定的一组机器操作。在Benzinger之后，我们在本节中介绍了一个通用框架，38J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35关于函数式程序相对于操作语义O的计算复杂性的推理，通过用一些复杂性信息n注释O中的每个规则t1↓t2，写为t1↓At2（n），这产生带注释的语义A。术语t2不需要是规范的（在使用小步语义的情况下），并且n可以是任意的数学表达式。然而，在本文中，我们将使用一个大步骤语义，因此，t2将始终是规范的。根据感兴趣的计算资源和我们对底层机器模型的假设，注释可能对上限、下限或精确量进行建模。作为一个例子，考虑下面的succ构造函数规则：u↓ksucc（u）↓succ（k）我们可以通过定义时间复杂度来u↓k（inn）succ（u）↓k+1（inn+1）或空间复杂度，u↓k（inn）succ（u）↓k+1（inn）2.1 Miniml的注释语义Miniml是用于从Coq证明中提取程序的函数语言[3]。它的具体语法与Ml的语法相似，如以下简单示例所示：let rec length =函数| 无->0| Cons（a，m）-> S（长度m）而它的抽象语法使用更紧凑的形式，更接近Coq中的语法：t：：= x| λx.t|[x：t] t| apply（t; t）|Cases t of u1⇒ v1, ··· , u n⇒ v n end| ind(t; v1; λz.v2):= case t of b ⇒ v1, s (tJ) ⇒ v2 [ind(tJ; v1; λz.v2)/z]其中x取自可数变量集，[x：u]v代表通常的let构造let x = u in v，b和s代表构造函数变量t所属的归纳类型（为了简单起见，我们假设这里有两个构造函数）。Miniml的语义现在由下面的一组注释规则给出假设A为每个缩减步骤分配单位成本，我们得到以下结果（succ）（时间）（空格）J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）3539规则：（canon）w↓w（in 0）u↓v（n）λx.u↓λx.v（n+1）f↓λx.b（inn1），u↓w0（inn2），b[w0/x]↓w（inn3）apply（f;u）↓w（inn1+n2+n3+ 1）a↓w0（在n1中），b[w0/x]↓w2（在n2中）[x：a]b↓w2（在n1+n2+ 1中）t↓w（inn1），Match（w，u1，···，up）↓（i，η）（inn2），viη↓u（inn3）（Casetofu1v1，···，upvpend）↓u（inn1+n2+n3+1）t↓w0（n1），Match（w0，b，s）↓（i，η）（n2），viη↓w（n3）ind（t;v1;λz.v2）↓w（n1+n2+n3+ 1）其中Match的规则如下，假设u1，···，up是深度为1的表达式，并且Match（w0，b，s）也返回（按照约定）递归调用的z（start）Match0（w，0，u1，···，un）↓（i，η）（inn）Match（w，u1，···，up）↓（i，η）（inn）Match0（f（w<$），k+1，u1，· ··，up）↓（i，η）（inn）（失败）Match0（f（w<$），k，g（v<$），u1，· · ·，up）↓（i，η）（inn+1）（成功）Match0（f（w<$），k， f（x<$），u1，· · ·，up）↓（k，{x<$$> →w<$}）上面的规则允许计算任何没有自由变量的基类型表达式所采取的步骤数。当然，对这样一个表达式e的步数的计算迫使它的求值成为它的实际值。与用法不同，我们有一个抽象规则，使我们的生活更容易。3开放表达式现在我们继续讨论带有变量的程序。程序是形式为λx.e的封闭表达式，其中主体e是任意类型的表达式，如恒等函数λX：α.X，其中α可以是任何类型。程序的定义将在后面更精确地给出。基类型的封闭表达式的注释语义与程序的注释在第一种情况下，我们可以（绝对值）（apply）（let-in）（宗）（归纳）40J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35运行操作语义并相应地计算输出值和达到输出值所需的步骤数。 在第二种情况下，程序有输入变量，这些变量稍后将由任意表达式实例化。计算将程序应用于特定输入表达式的结果所需的步骤数将取决于计算这些表达式的值的复杂性以及值本身。另一方面，我们仍然可以运行带注释的语义，直到到达一个请记住，应用程序（和let表达式）在可能重命名绑定变量之后，可以与所有其他构造（抽象除外）交换。因此，我们建议，定义3.1如果表达式e具有以下形式，则它被阻塞• x∈ X;• λx.u，其中u是分块表达式;• （u v），其中u是变量或被阻塞的应用程序;• [y：u]v，其中u是变量或阻塞的应用程序;• u 1的情况t = v1，. ，un_n_end，其中t是分块表达式;• ind（t;v1;λz.v2），其中t是块表达式。对于任意的α型表达式e和自由变量x1，.，xn，我们将由其值e和将e减少到其值e所需的步骤e组成的对相关联。 这些符号应该被认为是相对于用γ值代替x1中的变量，... ..γ（e）的值。直觉：e↓e（ine）那么表达式e的复杂度将是一个函数λx1. Cpx（e）从一个特定的估值中抽象出步骤的数量，即满足Cpx（e）（γ）= e，其中e在这里相对于这个精确的估值γ。为了使这种直觉精确，我们需要定义什么是赋值，这与复杂性函数的替代性有关。假设一个表达式依赖于一个基本类型的自由变量x。然后，它的复杂度将取决于值x和x的步数x。在这在这种情况下，赋值应该用对（x≠，x）替换变量x的情况函数类型需要更复杂的赋值，类型的功能结构。J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35413.1组合性对于一个结构化的表达式，其值、步骤数和复杂度必须根据其子表达式的相应值、步骤数和复杂度来计算，这一原则称为组合性。对于复杂性函数的情况，我们的主要原则是，复杂性应该是一个变换，作为从程序到复杂性函数的一个态射。例如，抽象的复杂性应该是其主体复杂性的抽象。此外，在表达式e没有阻塞子表达式（因此没有自由变量）的特定情况下，则其值和步骤数都应该与应用注释语义获得的结果一致，复杂度应该是步骤数本身。将这一原则付诸实践的困难来自更高类型的表达。 为了将这样一个表达式的复杂性降低到另一个更简单的表达式的复杂性，因为它是基本类型的，我们将假设程序是η-扩展形式的。定义3.2程序是一个良好类型的、分块的、封闭的表达式，其中函数类型的每个子表达式都是一个抽象或应用程序的左参数。例如，要被认为是我们意义上的程序，恒等函数λX：（α→α）→（α→α）.X，其中α是基类型，应该写为λX：（α→α）→（α→α）λy：α λf：α→α。（（X（λx：α. （fx））y）当然，在上述恒等函数和表达式（（X（λx：α））之间没有实际差异。（f x））y）在环境{X：（α→α）→（α→α）f：α→αy：α}中可典型化，或者表达式λy：αλf：α→α。（（X（λx：α. （f x）y）在环境{X：（α→α）→（α→α）}中可分型。换句话说，表达式的复杂度函数的类型在环境Γ既取决于它的类型，也取决于在Γ中给出的它的自由变量的类型。这句话将通过移除外部抽象并将开放表达式的复杂性定义为自由变量的函数来付诸实践，自由变量被视为形式参数。定义3.3我们定义类型α的元数，记为ar（α），为n，使得α = α1→.→αn→β，β为基型。一个表达式的arity就是它的类型的arity。在前面的高次型恒等函数的例子中，ar（X）= 2，ar（f）= 1，ar（x，y）= 0。类型α的arity确实是arity42J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35我任何α型程序的复杂度函数的最小值特别地，零元程序是基类型的基础表达式，因此可以在给定的步骤中被评估为一个值。对于非零元的程序，我们现在定义复杂度函数的类型和相关的赋值概念定义3.4给定一个类型α，我们将类型α定义为：如果α是基类型：α=（α×IN）否则：α→β=（α×α）→β定义3.5给定一个类型为α = α1→.的程序e，α n→β，我们说Cpx（e）：α是e的复杂度函数， 如果Cpx（e）（Cpx（u1），. ，Cpx（u n））= m i n（e u1... u n）↓ r（m）对于任意η -展开形式的闭表达式u1：α1，.，un：α n. 映射{x1<$→Cpx（u1），.，xn <$→Cpx（un）}称为x1，.的赋值。 ，x n.3.2计算复杂度表达式现在我们展示如何根据组合性原理递归地定义程序的复杂性请读者检查类型是否匹配。我们将以应用程序为例结束，这是一个难题。一个.我们将使用Cpx（t）。对于t和Cpx（t），为1。2为T。我们集中讨论Cpx（t）的定义。2.3.2.1抽象设e = λx1：α1. xn：α n.u是一个闭表达式，其中u不是抽象，因此通过假设程序是η-展开形式，u是基本类型。Cpx（λx1：α1.λx n：α n.u）= λx1：α1，.，xn：xn.Cpx（u）当计算Cpx（u）时，我们假设u中的变量xifree具有值x，并在等于xi的步骤中计算其值。这相当于认为Cpx（u）是变量x 1的函数：α1，.，xn：xn。这就是为什么我们说表达式的复杂性取决于它的自由变量从形式上讲，情况并非如此：表达式的复杂性取决于在将类型分配给其自由变量的环境中计算的类型。J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35433.2.2Case表达式Cpx（u 1的情况t=v1，.，unv nend）。2 =1+ Cpx（t）。2+例Cpx（t）。1 of u1<$1 + Cpx（v1）. 2、...，u nn + Cpx（v n）. 2 end注意，u1，. ，u n具有相同的类型意味着Cpx（u1），.. . ，Cpx（un）都在等待类型的输入，因此case表达式类型很好。3.2.3Let表达式Cpx（[y：u] v）。2 = 1 +[y：Cpx（u）]（Cpx（v）. （二）3.2.4递归Cpx（ind（u; v; λz：α.w））。2 =Cpx（u）。2+ind（Cpx（u）. 1;1 + Cpx（v）。2;2 + Cpx（λz：α.w）。（二）3.3应用现在我们来到复杂性定义的核心：应用程序的情况，更确切地说，是基本类型表达式u的情况，它是程序的η -扩展形式，也就是说，表达式（ea1. a n），其中e：α1→. →α n→α的元数为n，且a1，.，an n是η-展开形式不同的变量x1：α1，. ，xn：αn.接下来的讨论涵盖了e是基类型变量的情况，让αn+1=α。它还涵盖了ai是任何参数表达式的η-展开式的情况，不一定一个变量假设n= 0。 则e是基本类型α，因此Cpx（e：α）。2 =e。假设n>0。表达式的按值调用求值（e a1. a n）收益如下：（e a1. a n）=（. （（ea）a）. a）1 2N该计算的结构通过命名在该计算中连续出现的子表达式来描述：定义3.6对于一个表达式（e e1. e n）的η-展开形式，我们将其分解联系起来，它是一个命名表达式序列{ei：α i+1→44J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35ni=1i−1我0... →α n→α|i∈ [0.. n]}定义为：e0= e{e i=（ea）|i ∈ [1.. n]}因此（e a1. a n）= ei−1i n分解在下一节中起着基础性的作用。在评估步骤方面，我们得到：e↓e（in e）a i↓a（in a i） {e i↓ e（in e i−1）|i ∈ [1.. n]}i i−1（ea1. . . an）↓e（ine+i=n（ai+ei+1））（一）如果ai是基本类型，则它的步数ai是一个本原量。否则，它可以通过应用相同的技术递归地分解为更原始的量的总和。我们将在下一段中看到这样一个例子。我们现在的目标是用复杂度来表示这些步骤的数量为此，我们考虑表达式（e x1. xn），其中x1，...，xn是各自类型α1，.，α n. 让γ i−1是赋值{x i<$→（ai，a i），.，x n<$→（an，a n）}I n根据我们的解释，ei= Cpx（ei）。2（γ i），ai= Cpx（ai）. 2、因为我是地头蛇。将复杂度函数代入（1）得到：.2各处）：e↓e（inCpx（e）（γn））{ei−1↓ e（inCpx（ei−1）（γi−1）），ai↓a（inCpx（ai））|i∈ [1.. n]}（ea1. . . an）↓e（inCpx（e）（γ0） +i=n（Cpx（ai） +Cpx（ei）（γi） +1））ni=13.4变量现在我们将前面的讨论应用到变量的情况。变量X的复杂度将是计算表达式X a1.. a n，假设a1，.，an n是适当类型的不同变量的η -展开形式。我们将坚持在这里的步骤数，虽然我们也可以用复杂性来代替它们例3.7考虑一个类型为α的变量x，其中α是基类型。然后x是η-展开的，x≠：α，Cpx（x）=x0：IN定义为满足x↓x（以x0为单位）例3.8现在考虑类型为α→α的变量f，其中α是基类型。根据我们的假设，f作为应用程序（fa）的左参数出现J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）3545其中a：α。使用我们之前的索引符号f0= f，和f1= fa，我们有：f↓f<$（inf0），a↓ a<$（ina），f<$a<$↓（fa）<$（inf1）fa↓（fa）（inf0+a+f1+1）因此随着（f a）↓（f a）<$（在Cpx（f）（a <$，a）中）Cpx（f）（a≠，a）=f0+f1+a+1例3.9最后考虑一个类型为（α→α）→α的变量F，其中α是一个基类型。通过我们的假设，F作为应用程序的左自变量出现（F λx：α. （fx）），其中f：α→α.再次使用我们之前的索引符号，我们有：F↓F（以F0计）f↓f <$（in f0）x↓ x<$（in x）（f <$x<$）↓（f x）<$（in f1）（F <$λx. （f x））↓（F.λx. （f x））（F1）（F λx. （f x））↓（F.λx. （f x））（in（F0+（f0+x+f1+1）+F1+1））3.5主要财产引理3.10给定一个具有自由变量x1，.，xn，和一个基置换σ：x1<$→v1，.，xn<$→v n，则Cpx（Pσ）= Cpx（P）（x1<$→ Cpx（v1），. ，xn <$→ Cpx（v n））= Pσ也就是说，Cpx（t）满足我们对t的复杂度函数的定义。证据 证明应该是通过P的结构的归纳法（未完成）。□ □3.6到目标的到目前为止，我们没有取得很大进展。程序的复杂性现在被当然，如果我们能解出这些方程，我们就能得到整个程序的复杂性。例如，如果我们提前知道程序参数的复杂性，那么对于这些特定参数的程序的复杂性将被描述为独立程序。我们不会详细阐述这个我们还没有探索过的想法，而是集中精力去猜测46J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35一个程序的复杂性，并验证猜测是有意义的。为此， 我们将遵循Benzinger4将复杂性表示为递归方程我们计算复杂性的语言并没有真正给我们提供关于给定程序可能的多项式增长（一定程度）的洞察力。为了实现这个目标，我们需要近似这些复杂度函数。近似作为态射工作。案例表达式的近似值是所有分支的近似值的最大值。合成的近似是近似的合成。let表达式的情况也是如此。困难来自于归纳结构，因为近似递归调用中涉及的复杂性并不意味着获得定点本身的近似。为了处理这种情况，我们引入了一个中间步骤，使用递归关系。从递归关系到数学函数已经被深入研究，并在各种计算机代数系统中实现，例如Math- ematica或Mapple。除了程序的形式参数外，归纳项可能有几个归纳参数。符号和假设1。 我们用r（m）表示递归项ind（m;v;λz.w[z]）：= b的情况m<$v，s（t）<$w[ind（t，v，λz.w[z]）]在环境{m：α}中，类型为β，输入其归纳变元m。我们假设每个递归项都只有一个归纳论证（嵌入递归被排除）。我们还假设m是标准形式，即m=m，因为计算m的复杂度m简单地加到从第app.为了简化符号，我们将使用eJ表示表达式e的复杂度（步骤数）。由于r（m）、v和w[z]在其各自的环境中具有相同的类型，因此它们的按值调用求值具有第3.3节中描述的相同结构，因此它们的分解是相似的。假设r（m）在环境{m：α}中具有类型α→β。 然后，我们使用r0（m）为r（m），r1（m）为r（m）<$x<$，其中x：α，v0为v，v1为v<$x <$，w0[z]为w[z]，w1[z]为J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35470′1′w[z]x。 我们有以下等式：r（m）= b的情况m<$v，s（k）<$w[r（k）]（（r（m））<$x<$）=b<$（v<$x<$）的情况m<$，s（k）<$（w[r（k）]<$x<$）由于r（m）<$=r<$（m<$）=r<$（m），最后一个等式变为：（r<$（m）x<$）=b<$（v<$x<$），s（k）<$（w[r（k）]<$x<$）的情况m应用我们的计算复杂度的规则和引理3.10，我们得到：rJ（m）=b<$1 +vJ，s（k）<$2 +wJ[rJ（k）]的情况m0 0 0rJ（m）=b<$1 +vJ，s（k）<$2 +wJ[rJ（k）]的情况m1 1 1其可以写成如下的递归方程：.1+v′，如果m=b.1+v′，如果m=br0（m）=2+w′[r′（k）] ifm=s（k）r1（m）=2+w′[r′1（k）] ifm=s（k）0 0 1当然，当m是自然数时，则k=m− 1。类似地，当m是一个大小为n的cons（a，k），则k是一个大小为n-1的cons（a，k）。树的例子导致了明显的困难，因为我们没有任何关于树的线索左子树和右子树在整个树中的大小和复杂度。在这种情况下，需要最差情况近似值。这就引出了我们的第二个假设：假设2。我们假设所考虑的归纳类型α没有一个构造函数的类型包含两次以上的α。自然数和列表满足这个限制。这是我们的实现到目前为止唯一接受的两种归纳类型。最后，我们可以很容易地得出归纳定义的总复杂度，方法是将3.3节中所解释的复杂度相加。在下一节中进行示例5猜测的复杂性对于递归关系的求解，计算机代数系统提供了求解单变量递归关系系统的工具，这解释了递归程序依赖于单个归纳变量的限制。不幸的是，即使有这种限制，我们的方法产生的递归关系依赖于几个变量（或参数）的系统。因此，我们需要变换这些方程组，以处理这些系统的可能性。48J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35我我我我5.1处理参数化线性递归我们的参数化递归方程的一般形式是⎧.. ，p n）如果m =0R（m，p1，···，pn）=G（p1，.，p n，m，R） 如果m>0（二）其中，m是R的参数。如果所有的参数都是标量，则方程是一个线性方程.我们试图用常规方法求解这类递推方程。我们的方法的主要思想（同时也是主要局限性）是我们假设递归方程封闭解的特殊形式。更准确地说，我们假设封闭解是参数p ′的线性组合，并且该组合的系数c′是m的函数。R_n（m，p0，· · ·，pn）：=c0（m） +c1（m）p0+· · ·+cn+1（m）pn（3）用hR代替R，得到两个分别具有hcoefficientsc（0）和c（m）的线性递归方程组，它们形成依赖于单个变量m的线性递归方程组。⎧如果m= 0，则c（0）c（m）=i（四）c 如果m>0这样的系统现在很容易解决。将ci的封闭解代入R，得到R的封闭解。作为一个例子，⎧如果m= 0，R（m，p0，p1，p2，p3）=如果m>0，则p1 +a+b+R（m−1，p0，p1，p2，p3）+p3（五）我们假设封闭解的形式为R∈（m，p0，p1，p2，p3）=c0（m）+c1（m）p0+c2（m）p1+c3（m）p2+c4（m）p3⎩J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）3549（6）等式两边的匹配系数ci，我们得到系统50J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35递归方程。c0（m）=a+b+1 +c0（m−1）;c0（0）= 1c1（m）=c1（m−1）;c1（0）= 0c2（m）= 2+c2（m−1）;c2（0）= 0c3（m）=c3（m−1）;c3（0）= 0c4（m）= 1+c4（m−1）;c4（0）= 0用Maple V9求解这些递归方程，我们得到解：c0（m）：=−a−b+（a+b+1）（m+1）c1（m）：= 0c2（m）：= 2mc3（m）：= 0c4（m）：=m（七）（八）因此⎧如果m= 0，R（0，p0，p1，p2，p3）=0−a−b+（1+a+b）（m+1）+ 2mp1+mp3如果m>0（九）5.2执行我们的系统自动生成递归关系的格式，这是方便的计算机代数系统MapleV9。到目前为止，两个系统之间的通信通过一个可以被Mapple读取的脚本文件进行。一旦输出脚本准备就绪，它就被反馈到系统，系统使用结果来生成要分析的程序的复杂性表达式的封闭形式。5.3示例我们现在提出两个例子来说明这个方法。这些例子是用一个复杂性模型得到的，这个模型与这里描述的模型略有不同特别地，在Case表达式的情况下的匹配需要常数时间0，这意味着通过使用基于索引的适当数据结构来完成适当分支的选择J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35515.3.1高阶项需要导入排序。提取sort_rec.（** val sort_rec：->->->letrec sort_rec y h h0 = match y with| 无->h| Cons (a,l) -> h0 a l (sort_rec h h0 l)其中，y是自变量，h h0是参数。我们的符号计算得到了复杂性描述y_c+ f1（y H H_c H0 H0_c）为了求解y_c+ f1（y H H_c H 0 H 0_c），我们的系统生成了递推关系，0：f0（y）=11：f0（y）=10：f1（yH0H0_c HH_c）=11： f1（y H0 H0_c H H_c） =H0_c+aL_c+l_c+1 +f1（y-1 H H_c H0 H0_c）+H0_c+H_c如前所述，这类递归方程是参数化的RE。为了求解它，我们首先假设它的封闭解如下，递归方程的转换：f1（y H0 H0-c H H_c） =C0（0）+C1（0）H0+C2（0）H0-c +C3（0）H+C4（0）H_c f1（y H0 H0-c H H_c） =C0（n）+C1（n）H0+C2（n）H0-c +C3（n）H+C4（n）H_c把这个解代入前面的方程，C0（n）+C1（n）H0+C2（n）H0_c+C3（n）H+C4（n）H_c =H0_c+aL_c+l_c+1+C0（n-1）+C1（n-1）H0+C2（n-1）H0_c+C3（n-1）H+C4（n-1）H_c++H0_c+H_c对方程的两边进行匹配，得到附录方程.#附录重复计算init 4：=C4（0）=0 ; init 3：=C3（0）=0 ; init 2：=C2（0）=0 ;init 1：=C1（0）=0 ; init52J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）350：= C 0（0）=1;J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）3553#附录复发等式等式4：=C4（n）=C4（n-1）+1;等式3：=C3（n）=C3（n-1）;方程2：=C2（n）=1 +C2（n-1）+1;等式1：=C1（n）=C1（n-1）;方程0 = C 0（n）=aL_c+l_c+1 + C 0（n-1）;用Maple 9版求解，得到如下解，s0 ： =rsolve （ {eq0 ，init0}，C0）; s1：=rsolve（{eq1，init1}，C1）; s2：=rsolve （ {eq2 ， init2} ，C2）; s3：=rsolve（{eq3，init3}，C3）; s4：=rsolve（{eq4，init4}，C4）;然后我们把它们代入原始方程，我们得到最终结果，f1（yH0H0_c HH_c）=1f1（y H0 H0_cH H_c）=-aL_c-l_c+（1 + aL_c + l_c）（n +1）+ 2 nH0_c+ nH_c所以把它代入原始方程，我们得到最终的复杂度描述。Y_c-aL_c- l_c+（1 + aL_c+l_c）（n +1）+2nH_0_c + nH_c5.4第一订单期限：加（** val plus：nat-> nat-> nat **）令rec加上nm=匹配n与| O-> m| S p -> S（加上pm）符号求值得到的复杂度描述为n_c+ f1（nm m_c）相应的递推方程f1（nm m_c）= m_cf1（nmm_c）= S_c+0+ f1（n-1 mm_c）+ m_c为了求解这样的方程，我们首先生成一个附录递推关系。54J. - P. Jouannaud，W.徐/理论计算机科学电子笔记153（2006）35#附录复发等式init 2：=C2（0）=1 ; init 1：=C1（0）=0 ; init 0：= C 0（0）=0;#附录复发等式等式2：=C2（n）=C2（n-1）+1;方程1 =C1（n）=C1（n-1）;方程0 = C 0（n）=S_c+0 + C 0（n-1）;Maple的解如下，writeto（result）;s0：=rsolve（{eq0，init0}，C0）;s1：=rsolve（{eq1，init1}，C1）;s2：=rsolve（{eq2，init2}，C2）;将其代入原始方程，得到f1（nm m_c）=1f1（nm m_c） = -aL_c- l_c+（1 + aL_c +l_c）（n + 1）+2nm_c所以最终的复杂度描述是m_c+-aL_c- l_c+（1 + aL_c + l_c）（n +1）+2 nm_c6结论我们的系统能够根据我们的假设计算简单递归定义的复杂性：归纳应该对自然数或列表进行操作，并且应该只有一个递归调用。该方法是公正的，相对于一个正式的复杂性模型的功能计算使用调用值语义。复杂性函数是从计算机代数系统Maple的线性递归关系中提取出来的。在一般情况下，该方法生成的参数化的递归关系，不能直接解决。在这种情况下，我们在调用Maple之前通过猜测解的形式来我们的许多想法都受到了Benzinger [2，1]在NuPRL项目中所做工作的启发最后一个例子，但是，不能照顾Benzinger有很多问题需要解决。特别是，能够考虑具有多个递归调用的程序（如快速排序）似乎是必不可少的。我们还远远没有对这些进行分析。该方法的另一个强限制是假设参数化集合的封闭解