Coq语言中的变量绑定的名义方法

理论计算机科学电子笔记174（2007）69-77www.elsevier.com/locate/entcsCoq语言中的名词性推理技术（延伸摘要）布赖恩·艾德米尔宾夕法尼亚大学计算机与信息科学系关闭PA，USA摘要我们探索一个公理化的名义上的方法，在Coq变量绑定，使用一个无类型化的Alzoda-calculus作为我们的测试用例。在我们的名义方法中，lambda项的α-等式与Coq的内置等式一致。我们的公理化包括一个名义归纳原理和计算自由变量和替代功能。这些公理被收集在一个模块签名中，并使用局部无名项作为底层表示证明是合理的。到目前为止，我们的经验表明，从Coq中的这种公理化理论工作是可行的，并且变量绑定的名义风格密切对应纸的证明。我们目前正在努力证明一个原始的递归组合子的合理性，并开发一种方法来生成这些公理和它们的合理性证明从语法描述的语法条款和约束力。保留字：名词性推理技术，变量绑定。1引言我们在这里介绍了在Coq证明助手[2]中实现一种“名义”方法来形式化变量绑定的语法的工作。这种方法的特点是纸上的常见做法和Coq中的推理之间的密切对应。举例来说(i) 给定种类的对象级变量（绑定、绑定和自由）的所有出现都使用原子统一表示，原子是具有可判定等式的无限对象集。(ii) 对象级项的alpha等价由Coq的内置等价表示，而不是单独定义的等价关系。这两点都反映了铅笔和纸形式化的常见做法。更一般地说，我们的名义方法旨在消除对实际上没有出现在纸质证明中的任何术语进行推理的需要，例如，预项、移位项和外来项。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.01.02870B. Aydemir等人理论计算机科学电子笔记174（2007）69我们的最终目标是提供一个系统，该系统将一种语言的规范作为输入，并产生一个Coq签名作为输出，该签名提供了该语言的术语构造函数及其行为公理，包括自然归纳原理。该系统还应生成一个实现签名的模块，从而证明签名签名不会将对象级术语定义为Coq中的归纳数据类型。然而，我们相信，在签名中的公理可以很容易地使用生成一个专门的图书馆的策略和引理。我们的框架还包括一个包含概念的库，例如原子和交换（在第2节中介绍），这些概念对所有语言都是通用的。本文的主要贡献是证明，名义上的方法，变量绑定确实是可能的Coq和突出的问题时，实现这种方法在依赖类型的类型理论。虽然我们还没有上面描述的系统，但我们已经评估了这种方法在无类型lambda演算的特定实例中的理论和实践可行性，同时考虑到在更复杂的语言中出现的问题。我们认为，我们在这一特定情况下的经验将使我们能够建立一个如上所述的完整系统。本文其余部分的结构如下。我们首先在第2节中描述了我们方法的基础组件，并在第3节中描述了我们对无类型lambda演算的签名的设计和实现。然后，我们在第4节中给出了一些关于使用这种签名的经验观察。我们将在第5节讨论相关工作，并在第6节总结我们正在进行的工作。2名义签名与之前关于变量绑定的名义方法的工作一样[7，8，9]，我们的工作基于原子，交换和支持。由于交换和支持不能对所有类型进行参数化定义，因此我们使用Haskell类类型类的编码我们将在本节中逐一讨论这些组件。我们的开发广泛使用依赖类型化记录来捕获具有某些属性和操作的 在原子交换的情况下，对这些记录进行抽象的能力是至关重要的。 在其他情况下，它只是使我们的代码更灵活。例如，我们使用记录类型ExtFset来描述具有外延相等的有限集合的类型，其中一部分如下所示记录ExtFset（T：Set）：类型：= mkExtFset{extFset：Set; In：T-> extFset-> Prop; .}记录类型由T参数化，T是集合所携带的元素的类型。T上有限集合的实际类型由域extFset给出，In是一个集合成员谓词。这些字段的名称是常量（即，记录字段选择器），其完整类型为extFset：extFsetT：Set，ExtFset T-> SetIn：R（T：Set）（R：ExtFset T），T-> extFset T R-> Prop.B. Aydemir等人理论计算机科学电子笔记174（2007）6971记录AtomT：Type：=mkAtom{atom：Set; asetR：ExtFset atom; aset：= extFset asetR;atom eqdec：{a=b}+{a<>b};atominfinite：{b：atom}|b∈/F}}。Fig. 1. 原子的我们使用Coq我们将x∈/F表示为非（InxF），因为它是可以被定义的。一般来说，我们对记录的使用实现了类型类的字典传递语义每个记录类型定义一个类型类，记录类型的字段就是类型类的字段。为了只量化那些属于给定类型类的类型，我们量化它的字典。我们不使用模块，因为我们不能量化实现给定签名的所有模块。我们还使用记录类型来捕捉对象语言中变量名的基本性质，即存在无限数量的变量名，并且变量名的相等性是可判定的。我们把具有这些性质的物体叫做原子;记录如图1所示，由一个类型和证明该类型是原子集合的证据组成。 场原子是原子的类型，aset是原子的有限集合的类型，atom eqdec断言原子上的相等是可判定的。函数atominfinite，当提供任何有限原子集F时，产生一个原子b，并证明b不在F中。请注意，这个函数要求类型原子是无限的，并实现了“选择一个新原子”，这个操作的细节通常没有在纸上指定。对于任何A：AtomT，我们可以在需要原子A的地方写A。特别是，每当A出现在需要Set类型的项的位置，Coq隐式地插入atom的应用。在描述了原子之后，我们需要构造一个定义，用于在任意表达式中交换一对原子。原子交换是名义方法的核心概念，原因有二。首先，很容易定义一个合适的方法来交换几乎任何类型的原子，包括函数类型和具有名义绑定的类型。其次，它为我们提供了一种方法来一般地指定对于任何这样的类型来说哪些名称是新鲜的任何类型的原子交换的重要性质X由图2中的记录SwapT指定。属性swap same断言将原子与其自身交换必须始终保持表达式不变。下一个性质指出交换必须是对合。最终财产允许重新排序嵌套交换。理论上，用户可以使用任何满足SwapT中属性的给定类型的交换定义，但实际上通常有一个由类型结构定义的自然定义。交换的最简单形式是将类型为原子A的原子a和b交换到类型为原子A的原子c上，表示为swapaA（a，b）c。我们提供了使用swapa函数构造SwapT记录的构造函数mkAtomSwap对于没有原子（被交换的种类）出现的类型类型nat），应用交换的唯一合理定义是保持对象不变。72B. Aydemir等人理论计算机科学电子笔记174（2007）69Record SwapT（A： AtomT）（X：Set）：Set：= mkSwap{swap：（A * A）->X-> X;swap（a，a）x =x;swapinvolve：swapabx，swap（a，b）（swap（a，b）x）=x;swapdistrib：swapabcdx，swap（a， b）（swap（c， d）x）=swap（swapa A（a，b）c，swapa A（a，b）d）（swap（a，b）x）}.图二. 交换参数（tmvar：AtomT）（tm：Set）。参数var： tmvar -> tm。参数app： tm -> tm -> tm。参数lam： tmvar -> tm -> tm。公理tm归纳法：（P：tm-> Prop）（F：asettmvar），（x：tmvar，P（varx））->（t：tm，Pt->u：tm，Pu->P（t@u））->（λx：tmvar，x/∈F->λt：tm，Pt->P（λx. t））->（tt：tm，Pt）.图三.术语构造器和归纳原则。定义如何将swap应用于具有函数类型的表达式也不是太困难。我们的定义遵循Pitts [8]并满足SwapT记录中的性质（如果我们允许自己是函数可拓性的公理）：变量（A： AtomT）。变量（X：设置）（XS：交换T A X）（Y：设置）（YS：交换T AY）。定义func swap（a b：A）（f：X->Y）：=fun x => swap YS（a，b）（f（swap XS（a，b）x））。我们的原子交换框架允许用户在排序集合中的任何非依赖类型上定义交换。目前还不清楚是否有一种好的方法来指定交换依赖类型的含义3无类型lambda演算在本节中，我们将描述无类型lambda演算项的签名的主要组件。首先，我们的签名包括一个类型声明，术语，它们位于排序集中，以及这种类型的引入和消除形式，如图3所示。 使用Coq的符号机制，我们将app t u和λ x写成t @ u。t为lam xt。我们希望类型tm类似于归纳类型，所以我们对它的引入和消除形式类似于Coq的Inductive关键字定义的类型对于原生定义的归纳类型X，Coq生成术语X rect的定义（使用语言结构fix和match），它用作递归组合子，可以产生依赖类型的结果。当专门化为排序Prop时，这个组合子的类型充当归纳原则。怎么--B. Aydemir等人理论计算机科学电子笔记174（2007）6973参数fvar： tm -> aset tmvar.公理fvarlam：fvar（x：tmvar）（s：tm），fvar（lam xs）= remove x（fvars）参数subst：tm-> tmvar -> tm-> tm公理substlam：n（x y：tmvar）（st：tm），x<>y->x∈/（fvart）->（λx. s）[y：= t]=λx。（s [y：=t]）。见图4。 自由变量和项的替换。Axiomswap var：var（x y z：tmvar），（x，y）·（var z）=var（（x，y）var z）.Axiomswap应用程序：（x y：tmvar）（tu：tm），（x，y）·（t@ u）=（（x，y）·t）@（（x，y）·u）。Axiomswap lam：n（x y z：tmvar）（t：tm），（x，y）·（λ z. t）=λ（（x，y）<$z）。（（x，y）·t）。公理eq lam：n（x y：tmvar）（t：tm），y/∈fvart-> λ x。t = λ y。（ （x，y）·t）。公理注入lam：n（xx'：tmvar）（t t'：tm），λx。t=λ x'。t（x= x't = t'）（x /∈ fvar t't =（x，x'）·t'）.图五.交换和相等的公理。然而，如何在依赖类型的项上执行交换并不清楚，因此我们无法将这种签名中的强大递归运算符公理化相反，我们公理化一个独立的归纳原理。重要的是，这个归纳原则允许我们在lam情况下只推理绑定变量的新名称，通过取一个名称的有限集合，保证绑定变量与之不同（回想一下，aset tmvar是tmvars的有限我们的签名还没有包含递归组合子--我们目前正在努力提供这样一个运算符（参见第6节）。然而，对于lambda演算术语，递归组合子的主要用途是替换和自由变量函数的定义。因此，我们的签名使这些操作公理化-lam情况的公理如图4所示。即使使用递归运算符，将这些操作包括在生成的签名中可能是有意义的。 我们再次使用Coq的notation来为subst y t写入it [ y：= t ]。不存在substlam是定义subst在lam抽象上的行为的唯一公理，但subst必须是一个全函数。因此，我们也公理化了lambda项的alpha等价性（见图5）.给定一个lam抽象，我们可以使用always eq lam来重命名绑定变量，这样subst lam就可以应用了，就像在纸上一样。公理化等价需要一个规范的交换概念，届因此，我们的签名包括以下内容：定义tvS：=mkAtomSwap tmvar。参数tmS：SwapT tmvar tm。74B. Aydemir等人理论计算机科学电子笔记174（2007）69第一行构建了交换tmvar原子的默认定义的B. Aydemir等人理论计算机科学电子笔记174（2007）6975第二个断言交换项的定义我们使用Coq变量名x和y与变量z的交换，以及交换tmS（x，y）t的（x，y）·t，它将交换应用于项t。将交换应用于项的结果由三个公理给出-每个构造器一个公理-并且也在图5中示出。请注意，这个定义只是将交换应用于构造函数的参数，即使在lam情况下我们已经实现了一个具有这个签名的模块（从而证明了我们的公理的可靠性），使用lambda项的局部无名[5]实现，其中自由变量被命名，绑定变量使用de Bruijn索引编码。我们将tm定义为与良构性证明配对的局部无名项的类型，表明所有索引都引用绑定变量，并且我们使用公理的证明无关性等同于良构性证明时，比较条款的平等。因此，我们的归纳原理允许我们证明所有良构项的性质，而不必显式地证明任何关于指数的东西。在证明这一原理成立时，我们假定它的前提，特别是：f_x：tmvar，x/∈F->f_t：t_m，P_t->P（λx. t），然后通过对x的大小的归纳证明P对所有x成立。有趣的情况是当x是一个局部无名的lambda抽象时，我们需要使用上面的前提来证明P x成立。在抽象体中，我们将绑定索引实例化为一个新的名字y，从而得到一个项t，使得x = λ y。t. 由于Pt由归纳假设成立，上述前提意味着P（λy.t）保持。x上的结构归纳在这里会失败，因为t不是x的子项。签名的其余部分很容易实现。4使用签名的经验名义形式的定理陈述与人们所希望的纸上陈述一样接近。例如，下面两个定理可以从我们的签名中通过M上的名义归纳法来证明。定理substnotfv：nxMN，x/∈（fvarM）->M[x：=N]=M. 定理子项：nxyMNL，x<>y->x/∈（fvarL）->M [x：=N][y：= L]= M [y：= L] [x：= N [y：= L]]。使用tm归纳原理的归纳证明与在标准归纳类型上使用归纳策略的证明归纳证明中的推理也与纸上的推理非常相似，但要求我们在lambda情况下精确地描述绑定器的名称必须与之不同的变量集。保守地说，我们经常断言绑定变量不同于我们上下文中任何表达式中出现的所有自由变量名。使用这样的假设需要比在纸上证明中看到的更多一点的细节和谨慎，但似乎与机械化的一般开销一致。此外，我们希望将这一过程自动化。76B. Aydemir等人理论计算机科学电子笔记174（2007）69我们试图评估的另一个关键问题是，从Coq中的公理化等式进行工作是否例如，由于fvar的行为是公理化的，而不是具体定义的，所以诸如“不确定性”之类的策略无法展开它的定义。此外，由于alpha等价项在我们的签名下不可转换，因此可能需要使用eq lam重写项以应用给定的引理或假设。然而，我们发现CoqCoq有一些改进的余地，但我们没有发现以这种方式工作的严重障碍。5相关工作我们的工作受到Isabelle/HOL [1，9]的名义数据类型包的启发。然而，除了提供自动化的工具，推理与绑定的数据库的共同目标，我们试图探索的问题时，使用依赖类型的类型理论的名义技术，并明确的“签名”需要提供一个有效的和实际可用的形式化的语法与绑定。与Isabelle/HOL包中一样，与名义逻辑不同，无论何时我们需要等变性（交换下关系的不变性）或有限支持，我们都明确地声明该要求，而不是做出全局假设。由于我们的签名是一个公理化的阿维达条款和相关的功能，它是非常相似的精神戈登和梅尔汉姆目前尚不清楚是否可以直接翻译戈登和梅尔汉姆用高阶逻辑的公理扩充。此外，在迭代运算符的lam情况下，不是量化绑定变量的名称，而是量化从名称到项的函数换句话说，他们提供了一个术语类型的“名义”引入形式和弱HOAS消除形式。考虑到Norrish使用Gordon和Melham公理的经验[ 6 ]，我们的方法避免了在Meta级和对象级绑定器之间建立直接联系，我们并不是第一个使用“局部无名”方法来表示绑定语法的人。McBride和McKinna [5]简要介绍了该技术的历史，Leroy在解决POPL MARK挑战时使用了该技术。我们使用这种方法，除了证明无关性的公理，是至关重要的，使CoqB. Aydemir等人理论计算机科学电子笔记174（2007）6977变量（A：AtomT）（X：Set）（S：SwapT A X）。定义支持（F： asetA）（x：X）： Prop：=ab：A，a∈/F->b∈/F-> swap S（a，b）x = x.定义新鲜（b： A）（x： X）：Prop：=<$F：集合A，支持Fx<$b∈/F。参数tm rec：R（R：Set）（PR： SwapTtmvar R），如果var：tmvar -> R，如果pp：tm->R->tm->R->R，如果lam：tmvar -> tm ->R-> R，F：aset tmvar，（支持. F（f var，f app，f lam））->（b∈/）(tm-> R）。Fxy，freshPR b（flam b xy）->Axiom tmreclam：RPRFf var fappflam suppfcb，令f：=（tm recR PR Ffvarfappflamsupp fcb），b∈f->f（lambt）=flambt（ft）.图六、递归运算符及相关定义。省略号表示省略的字典参数。6目前和今后的工作我们正在进行的工作包括实现一个组合子，用于通过原始递归来定义术语上的函数，开发一个工具来从用户提供的语法规范生成签名和实现，以及研究依赖类型上的交换。我们在下面讨论我们在递归组合子上的进展。以皮茨[8]的工作为灵感，我们首先定义一组有限的原子支撑一个物体意味着什么。直观地说，当一组原子包括对象的自由名称时，该对象由该组原子支持。Freshness则概括了一个对象的名称何时可用的概念。精确定义见图6。请注意，支持对象的集合会根据所使用的交换定义而变化，因此对于对象来说可能被认为是新鲜的原子也会变化。基于我们最初定义递归组合子的尝试，我们期望如图6所示，可以实现tm rec，并且可以证明tm rec lam是的。如果满足条件b∈/F，则该xiomm接收通常为由原始递归定义的函数的形式。的论点F：aset tmvar，（支持. F（fvar，fapp，flam））和b：tmvar，（b∈/F去跟踪皮茨。supports命题简明地捕捉了Norrish对他的递归运算符的要求，即函数f var、f app和f lam“尊重置换”并且“不创建太多新名称”[ 6 ]。最后，虽然tm rec只能用于定义非依赖类型的函数，但我们计划研究一个用于定义依赖类型函数的组合子。78B. Aydemir等人理论计算机科学电子笔记174（2007）69引用[1] Berghouth，S.和C.城市，Isabelle/HOL的标称数据类型包，http://isabelle.in.tum.de/nominal/网站。[2] Bertot，Y. 和P. Cast'eran，“Inter act i v e T heorem P r v i n g and d P r g r am D e v e l op m n t：C oq ' A r t：归纳构造的微积分”，Springer-Verlag，2004年。[3] 戈登，A. 和T. Melham，《阿尔法转换的五个公理》，作者：J. vonWright，J.格伦迪和J. Harrison，editors，Theorem Proving in Higher Order Logics：9th International Conference，TPHOLs173-190.[4] Leroy，X.，一个本地无名的解决方案，以POPLmark的挑战，http://cristal.inria.frwww.example.com/pixely/POPLmark/locally-nameless/.[5] 麦克布莱德角和J. McKinna，Functional pearl：I am not a number-I am a free variable，收录于：Haskell一比九[6] Norrish，M.，递归函数定义的类型与粘合剂，在：K。Slind，A.邦克和G. Gopalakrishnan，编辑，Theorem Proving in Higher Order Logics：17th International Conference，TPHOLs 2004，LNCS3223（2004），pp. 241-256[7] Pitts，A.M.，名词逻辑，名称和绑定的一阶理论，信息和计算186（2003），pp. 165-193。[8] Pitts，A. M.，阿尔法结构递归和归纳（扩展摘要），在：J.赫德和T。Melham，editors，Theorem Proving inHigher Order Logics：18th International Conference，TPHOLs 2005，LNCS 3603（2005），pp. 17比34[9] 厄本角和C.Tasson，Isabelle/HOL中的标称技术，在：R. Nieuwenhuis，编辑，自动演绎- CADE-20：第20届自动演绎国际会议，LNAI 3632（2005），pp. 38比53