基于证明编程范式的自动程序综合系统中的产品类型

233网址：http://www.elsevier.nl/locate/entcs/volume67.html21页使用产品类型Fairouz Kamareddine1苏格兰爱丁堡赫瑞瓦特大学数学与计算机科学学院弗朗索瓦·莫宁2IRISA，Campus de Beaulieu，35 042 Rennes Cedex，法国毛里西奥·阿亚拉-林孔Departamento de Matematica，Universidade de Bras lia，Bras lia D.F.，Brasil摘要我们研究了一个基于证明编程范式的自动程序综合系统。为了自动提取一个计算由一组方程给出的递归函数的项，系统必须找到给定函数的整体性的形式证明。由于特定的逻辑框架，通常这种方法使得难以使用重写理论中的技术我们通过开发产品类型来克服自动化系统的这一困难。因此，这将使在其他领域使用的终止技术的结合，同时仍然提取程序。关键词：程序抽取，自动终止，产品类型1引言Curry-Howard同构[3]在类型论中起着重要的作用，它给出了程序和规范证明之间的对应关系。以该证明为程序范式的程序设计方法保证了从函数完备性证明中提取的程序的某些正确性，并提供了一个分析程序行为的逻辑框架。利用证明作为程序范例的系统包括二阶1 电子邮件地址：fairouz@cee.hw.ac.uk2 电子邮件地址：monin@irisa.fr3 电子邮件地址：ayala@mat.unb.br2002年由ElsevierScienceB. V. 操作访问根据C CB Y-NC-N D许可证进行。234函数算术AF 2 [6，8]和递归类型理论TTR [15]。AF 2和TTR都使用方程作为算法规范，其中的compi- lation阶段对应于函数规范的正式终止证明，从中提取计算函数的项利用TTR的逻辑框架，P.Manoury和M.Simonot [11，10].自动终止问题是系统开发中的一个主要问题除了系统，其中数据类型和规格的功能由用户在ML风格介绍，算法已被设计使用的策略来搜索每个规格的正式终止证明当系统成功地为一个规范开发了一个正式的终止证明时，就会给出一个计算该函数的-项。正如[11]中提到的，这个系统中的自动终止证明不同于重写系统的通常技术，因为它们必须遵循几个要求。它们必须是总体性的证明，以便能够提取项。 在ProPre中，不仅要确保程序会为任何输入提供输出，而且要确保对于任何类型良好的输入，结果也是类型良好的。最后，证明也必须在形式逻辑框架中表达，即自然演绎风格。根据递归类型理论TTR，从以自然演绎风格因此，增强自动证明策略是AF2或TTR等编程语言的核心问题。虽然[13，5]中已经发展了基于序测度的函数程序设计的终止方法，与[11，12]中设计的形式证明有关，但本文的目的是在某种意义上分析这个问题的反面。 也就是说，我们分析的可能性，将新的终止技术的提取程序中的ProPre或TTR上下文中。为了简化分析的形式证明中获得的逻辑框架的ProPre，我们表明，这些形式证明的核心，正式终端状态属性（FTSP），可以抽象使用一个简单的数据结构。这就产生了一个简单的终止属性，我们称之为抽象终端状态属性（atsp）。atsp的有趣之处在于，一方面，终止条件足以独立于ProPre的特定逻辑框架，使用[5]的序测度来显示终止，另一方面，我们还证明了我们可以直接从atsp自动重建形式证明，以便可以提取lambda项。也就是说，本文的第一个结果是建立一个对应的atsp与一类序测度在一个简单的上下文中的终止性和形式证明建立在ProPre。这种对应意味着在[4]中得到的递归函数的终止性证明一般不承认在ProPre中的形式证明。 事实上，这些函数的类比用[13，5]的序测度类证明的那些函数大。为了克服一般没有正式的235证明在ProPre为这些功能，本文提出的第二个结果允许这些功能的综合仍然利用整个框架的ProPre，但在不同的方式在TTR。实际上，结果证明是更强的，因为它可以应用于递归函数，其终止性由其他自动化方法证明，例如来自重写理论的技术（参见例如，[1]）。其原理在于模拟语义方法。也就是说，从每个递归调用都递减的有根据的排序，必须能够通过考虑函数参数元组的一般归纳来建立形式证明虽然这个原则是自然的，但当我们想要提取程序，这种方法变得困难，因为我们必须考虑证明的逻辑框架和结构2逻辑框架ProPre[9，11，12]依赖于证明作为程序范式，利用Curry-Howard同构并处理递归类型理论TTR[15]。在ProPre中，用户只需要定义数据类型和函数。从函数的终止语句的形式证明中自动提取了-项，可以将其视为编译部分。ProPre处理递归函数。数据类型和函数是用类似ML的语法定义的。例如，如果N表示自然数的类型，则自然数列表由下式定义：Ln类型：无|Cons N Ln;并 且 append 函 数 由 下 式 指 定 令append： Ln，Ln -> Ln无y => y|（Cons n x）y =>（Cons n（append x y））;一旦用户引入了一个数据类型，就会自动生成一个二阶公式。例如，在一个示例中，自动生成以下二阶公式并将其与自然数列表相关联Ln（x）：=8 X（X（nil）！（8 n（N（n）！8 y（X（y）！X（cons（n; y）！ X（x））。这个公式代表包含nil元素的最小集合，并且在构造函数cons下闭合。每种数据类型都将被缩写为一元数据符号，例如，符号N表示自然数的数据类型。此外，一旦在系统中指定了一个函数，就会自动生成一个终止语句[10]。例如，append函数的终止语句是公式：8 x（Ln（x）！8 y（Ln（y）！Ln（append（x; y）。然后，系统尝试使用定义函数的方程组来证明函数的终止语句在一个成功的例子中，计算函数的-项是从自然演绎风格的形式证明的构建中合成的非正式地说，如果T是函数append的一个-项，并且t1，t2 are-termsthatrespectivelymdeltermsu1 和u2的的值，则（（Tt1）t2）化为一个正规形式V，它表示type Ln的append（u1;u2）的值.见[6，7，14，15]的理论细节，允许推导出 - 条款2361nE终止证明的规范在自然演绎风格。2.1AF2的类型规则（也是TTR的一部分我们假设一个函数符号集合F和一个单个变量的可数集合X。逻辑术语归纳定义如下：单个变量是逻辑项;如果f是在F中n元函数，且t1; ：;tn 是逻辑项，则f（t1; ：;tn）是逻辑项。我们假设一个可数的谓词变量集，并通过以下公式定义公式：如果X是一个n元谓词变量且t1; ： ： ：;tn 是逻辑项，则X（t1; ：;tn）是一个对模;如果A和B是公式，那么A！ B是式;如果A是一个公式，并且是一个一阶或二阶变量，那么8 A是一个公式。我们使用8xA！B表示8x（A！B）。 一个形式为F1的mula！（F2！* *（Fn1 ！Fn）：）也将由yF1; ：;Fn表示 ！F. F或实例8xD1（x）;8yD2（y）！F代表公式8x（D1（x）！ 8y（D2（y）！（F））。类型判断是以下形式的表达式：00x ：F ;：;x：女`t：F“，其中x1; ：;xn 是不同的-变量，t是-项，F;F1; ： ：;Fn 是公式，E是关于逻辑项的一组方程。判断的左边称为上下文。注意，我们可以自由地对公式中出现的-项和逻辑项使用相同的符号，因为上下文将澄清一个项是-项还是逻辑项。特别地，单词“变量”也可以指“变量”。表1给出了AF 2的类型规则，其中E是关于逻辑项的一组等式，是形式为x1的一个文本 ：A1; ：;xn ：An 并且m aybeemp t y; y（分别地，Y）是arst（resp. 二阶变量在A1; ： ;An;;u;v中不第一阶项，T是一个公式。（ax）;x：A`Ex：A娥t ：A[u=y`Et：u ：A`E（tEt`Et：Et`Et：]E`u=vA[v=y]（eq）;x：A`E娥”“啊！B（啊！e）1n237t：B（啊！（一）”“啊！Bu）：B、Et：A1（8i）Et：8yA：8yA1（8e）A[=y]Et：A2（8i）'Et：8YA：8YA2（8eA[T=Y]）表1二阶函数算术（AF2）类型和形式数据类型在AF2和TTR中扮演着重要的角色，与可实现性的概念有关[7]，可实现性确保提取的术语计算所定义的函数（参见[6，7]）。如果对于一个n元函数f，我们有：238y1n“Et：8x1：8xn（D1（x1）！（： ：！（Dn（xn）！D（f（x1; ： ： ：;xn）） ： ：：）对于某些项t，其中D1; ：;Dn; D表示形式数据types，则-term t根据集合E计算函数f。2.2TTR的一些规则至于AF2，我们不陈述TTR的数据类型和可实现性概念。特别地，我们没有给出二阶最小不动点算子（参见[14]），其允许定义在此由一元数据符号D; D 0;：; D;：;D表示 的 数 据 类 型 。为了清楚起见，不陈述所有规则（也包括AF2的规则）。在TTR中，添加了一个二进制符号，在[14]中称为隐藏运算符。它的意思是一个合取，它只保留左边部分的算法内容，以防止在-terms中执行终止证明的不必要的算法内容（见[15，11]）。它与关系连用，在下面精确第2.1节中给出的公式定义如下：如果A是一个公式，u; v是项，则A（u）V）是一个公式。 与隐藏操作符相关的规则在表2中给出。`t：娥一不： 一娥ee（一））`Et：`t一：Ae（二））娥 测试：娥一ee（三））表2隐藏操作符的规则。如果A是一个公式，其中出现一个特殊的变量x，我们将公式A[u=x]（u v）用符号Auv表示。在TTR的规则中，有几条规则被用来从编程的角度再现归纳推理下面的规则在TTR中代表外部归纳规则，其中关系表示代数项上的有理偏序：娥 （Tt）：8x[D（x）！B]（分机）在规则（Ext）中，lambda项T是图灵xed点运算符，D是 数据类型，x是公式B中未出现的变量G从（Ext）规则，可以推导出Ind公式：GInd：=8x（Dr（x）！ 8X（8y（Dr（y）！ 8z（Drz！ X（z））！ X（y））！X（x）：G也就是说，有一个-项见证了IND的证明在下面的引理2.1中，它是针对[14]中的自然数类型给出的引理2.1.对于每种递归数据类型，都存在一个-term ind，例如”曰：“行。G引理2.1在[14]中的证明，仅用自然数的类型给出，可以应用于任何数据类型：ind =（Tx yz（（z y）m（（x m）z），其中T是图灵x娥 t：8x[8z[Dzx ！ B[z=x]]！ [D（x）！B]]239点算子，对任何数据类型都有效引理2.1是有用的宏规则的定义，称为Ind-rule，在ProPre。240我左线性方程组f（e1;e0）; ： ;（ep;e0）g的重叠集合使得对于所有2.3ProPre系统我们假设函数集合F被分成两个不相交的集合，构造器符号集合Fc和定义函数符号集合Fd，也称为定义函数。 每个函数f都应该有一个类型，用D 1;：; Dn表示！ 其中D 1; D n;D表示数据符号，n表示函数f的元数。我们可以写f：D 1;：：; D n！D同时引入函数f和它的类型D 1;：; D n！D.定义2.2.[规范;终止语句;递归调用]定义函数f：D1; ：;Dn！D在F中d是非1个p1我p，ei的形式为f（t1;：; tn），其中tj是构造器项（即，没有出现定义的函数符号）的类型Dj，j= 1;：; n;E0 是一个关于t∈D的项。函 数 f ： D 1; ： ; D n！ D 是 公 式 8x 1 （ D 1 （ x 1 ）！“……”8× n（D n（x n）！D（f（x 1;：; x n）。设Ef是函数f的一个分段. f的递归计算是一对（t;v），其中t是Ef 的方程（t;u）的左侧，v是u的形式为f（v 1;：; v n）的子项。一个规范的方程（l; r）可以写成l = r（作为TTR中的一个方程公理）。我们也可以去掉方括号以方便阅读。ProPre的形式化证明，称为I-proofs，建立在分布树上，基于[11]中的TTRStruct规则和Ind规则派生的两个主要规则。在ProPre中建立的分布树具有形式终端状态属性。这一节介绍了这两个主要规则，分布树和形式终端状态属性。符号2.3.如果P是对公式F1; ：;Fk;8xD0（x）;Fk+1; ：;Fm！D（t），则PD（x）表示公式F 1;：; F k; F k+1;：; F m！D（t）。上面的符号是正确的，因为它将在量化变量x将被公式PD（x）中关于上下文的项代替的同时使用接下来的两个引理，记法2.4）或者当变量x将被引入上下文时。符号2.4. 设C是一个类型为D 1;：; D k的构造函数符号！D.设x1;：;xk;z是不同的变量。设F（x）是一个公式，其中变量x是自由的，变量z;x1;：; xk不出现，令t = C（x1;：; xk）。则C（F（x））和C（F（x））将分别是以下公式：C（F（x））是：8x 1 D 1（x 1）;：：; 8x k D k（x k）！intn =x];C（F（x））是：8x 1 D 1（x 1）;：：; 8x k D k（x k）; 8z（Dz t！F[z=x]）！F[t=x]。该符号可能暗示了某种公式，这些公式在构造I-证明时实际上是有用的，其定义如下：定义2.5. [I-公式和收缩假说]式F称为I-式，F的形式为H 1;：;H m！241u我u我D（ f（t1;：; tn））对于一些：数据类型D，定义函数f，对于公式Hi，其中i=1，满足Hi的形式为8xD0（x）或形式8z（D0z ！F0）对于某些数据t∈D0，I-对于公式F0 项u。H 1;：;H m！D（f（t1;tn））是形式为8z（D0zu！ F0）。我们都知道是对I-限制性假说H=8z（D0z！F0）如果H0是F0的一个I-限制定理.根据定义，I-公式是递归的，它可以包含子I-公式。I-限制性假设不是I-公式。我们使用术语限制性假设也表示I-限制性假设。 定义函数的终止语句是一个没有限制性假设的I-公式下面的引理指出，在TTR中可以使用两个额外的规则，称为Struct规则和Ind规则，因为它们可以从TTR。这些规则对应于宏观规则，前者可以被看作是一种案例推理，而后者则代表一种归纳规则。引理定义2.6. （IND规则）设D是一个数据类型，并考虑所有类型为Di1; ：;Dik的构造函数Ci ！D ， 0ik ， i=1 ; i = 1;i= 1;q = 1 。设 P 是 形 式 为 F1; ： ;Fk;8xD（x）;Fk+1; ：;Fm的模.D0（t）和一个con文本。F或C（PD（x）），D型的归纳Ind规则为：`P单个（x）与Ind规则一起，下面定义的Struct规则，也是从TTR派生的宏规则，可以被认为是案例推理。引理定义2.7. （Strutrule）设D是一个数据类型，并考虑所有类型为Di1; ：;Dik的构造函数Ci ！D ， 0ik ， i=1 ; i = 1;i= 1;q = 1 。设 P 是 形 式 为 F1; ： ;Fk;8xD（x）;Fk+1; ：;Fm的模.D0（t）和一个con文本。 F或C（PD（x）），如符号2.4所示，D类型的结构规则是：`PStruct（x）由于这些引理，可以在TTR中添加两个宏规则：结构规则（引理2.7）和独立规则（引理2.6）。根据这些规则，可以在ProPre中构建分发树（参见定义2.10）。备注2.8. I公式由Struct-rule和Ind-rule保存。也就是说，如果P是I-公式，那么C（P D（x））和C（P D（x））也是I-公式。定 义 2.9.【公式之 心】F=H 1;：;H m形式的公式之心！D（t），其中D是递归数据类型，将是项t，由H（F）表示。分布树定义如下：定义2.10.[分布树]设Efe是函数f：D1; ：;Dn的一个分支！ D：A是Efi的分布树A是树的构造过程`C1（PD（x））：`Cq（PD（x））`C1（PD（x））：`Cq（PD（x））242仅使用Struct规则和Ind规则，其中：(i) A 的 根 是 f 在 空 上 下 文 下 的 终 止 语 句 ， 即 ： “8x1D1（x1）;：：;8xnDn（xn）！ D（f（x1;：：;xn））.(ii) 如果L = f 1`F 1;：; q` F qg是A的叶子的集合，则存在一对一的应用B：L，！ 如果B（L）=（t; u），其中hL=（`F）在L中，则F的中心是H（F）= t.注意，可以使用注释2.8从根归纳地检查分布树中的任何公式是I公式。ProPre给出的I-证明是定义函数终止语句的形式终止证明。它们分为三个阶段：(i) 为指定函数的指定开发分布树，其特征在于所谓的形式终端状态属性;(ii) 通过应用（eq）规则将分布树的每个叶子扩展成新的叶子;(iii) 来自第二步骤的每个叶利用在[11]中定义的规则用新的子树扩展，其叶以公理规则结束由于在[11]中证明的以下事实，本文中没有必要考虑ProPre中构建的证明树的中部和上部：事实2.11。一个分布树T可以（自动）扩展成一个完全证明树，它具有所谓的形式终端状态性质。因此，为了完成证明树并声明函数的终止，需要查看具有正式终端状态属性的分布树。因此，我们仍需说明上述财产。定义2.12. 一个I公式或一个限制性假设P可以应用于一个项t，如果P的心脏H（P）根据一个替换匹配t，其中对于在P中自由出现的每个变量x，我们有（x）= x。定义2.5的关系涉及在自然数范围内的项上的测度j：j#，其计算给定项t（包括t）的子项的数目，并且解释如下：定义2.13.设Var（t）是在t中出现的变量的集合。 设u;v为项。我们说u v i：j u j # k作为节点的限制性假设最后T r i;i表示P上的恒等式。下一个定理与定理4.1相反，表明我们可以从具有atsp的骨架形式自动重建具有ftsp的分布树。因此，根据2.3节，我们也可以建立一个I证明，从而提取一个计算给定函数的-项。定理4.2LetEf是函数f的一个特例，（Ti）是Ef的一个项分布。如果（Ti）具有抽象终态性质，则分布树D（Ti）具有形式终态性质。是的。 设（Ti）e是E f的项分布树，其中A为tsp. 我们想证明D（T;）具有ftsp。取一个递归调用（t; v）的方程Ef。 我们必须找到一个限制性的论点R=8zDzs;F1; ：;Fk！其中B（L）=（t; v），其中B是定义2.10的应用，使得条款1. 和2. 第2.14章坚持住 设B是D（T;）的b（t）在T中，并让（;x）是节点在定义3.5中给出的b（t）中。 考虑D（T;）中的（`P）与T中的（; x）处于同一水平。当（）= 1时，通过构造D（Ti），得到了形式为Q=8z（Dzs！ PD（x）[z=x]）在B中的P的子P0中创建。考虑R = Trj;i（Q）是B中的限制性假设，其中i和j分别是P0的水平和B的叶。我们可以写R =8 z（Dzs0！PD（x）[z=x]）对于某些项s0 因为：1) Q中的自由变量是s项的自由变量，应用的Ind/Struct规则是在P0中的一个变量上完成的，该变量超出了Q的范围B B B Bj;i.. . R=TrB（Q）=8z（Dzs0 ！PD（x）[z=x]），其中C（R）的变量在R中是闭的。我们知道用替换匹配v;v，但是C（P）=，所以R可以根据定义为（z）=;v（x）的替换应用于v且（y）=;v（y）对于yz。 我们必须证明（z）为0。这可以很容易证明，通过归纳ki，则若Trki（Q）= 8 z（Dz！BSKPD（x）[z=x]），则sk=k;i1（x）其中nodematch在T中具有替换k的级别k处的节点;i1。通过定义j，249B0BB000Ni（N 0）=Ni（N）+1，其中ve（0）=1。根据定义3.5，我们具有以下关系：00j; i1=LBi，s0;v（x）j;i1（x）y，由定义3.5，我们现在不能推导出（z）s0，因为s0=sj。 因此，第1条。 定义2.14成立。考虑一个限制性命题H=8zD0zr！KinR;wehave在P中发现了一个形式为8zD0zr的限制性定理H0！K这样，（r）r 0。由于H是Trj;i（Q）的限制性假设，所以H也是Q的限制性假设.因此，人们将P 0=8xi1Di1（xi1）; ： ：;8xikDik（xik）;8z（Dzsi！PD（x）[z=x]）！PD（x）[si=x]，其中H|{z}QH 0分别存在于PD（x）[z=x]和PD（x）[si= x]中. 因为H的形式为8zD0zr！ K则H 0的形式为8zD0zr！ 因为只有r项中的变量在H中是自由的。现在考虑节点（`N），B在水平l上使得1）在B中N的子N 0中创建新的限制性假设M，即Ni（N 0）=Ni（N ） + 1和Nr（M;N 0）=1，以及2）Tri; 1（M）=H 0. 设（0;x0）是A中（`N）在T中的对应模. 显然，0是T中的祖先，因为l

下载后可阅读完整内容，剩余1页未读，立即下载