没有合适的资源?快使用搜索试试~ 我知道了~
一阶和高阶抽象的语境及其应用
一阶和高阶抽象的语境理论Furio Honsell、Marino Miculan和Ivan ScagnettoDipartimentodiMatematicaeInformatica,Universita`diUdineVia delle Scienze 206,33100 Udine,Italy. honsell,miculan,scagnett@dimi.uniud.it摘要我们提出了两个案例研究,在形式推理的无类型λ-演算在Coq,使用一阶和高阶抽象语法。在第一种情况下,我们证明了α-等价的三个定义的等价性;在第二种情况下,我们专注于替换的性质。在这两种情况下,我们处理的上下文,这是rendered的手段高阶条款(功能)的元语言。这些都是成功地处理通过使用上下文理论。介绍在本文中,我们提出了两个案例研究,源于两个著名的编码范式的语言与绑定器的逻辑框架:一阶和高阶抽象语法(FOAS和HOAS,分别)。在前一种情况下,我们可以在de Bruijn索引或显式名称之间进行选择[9]中两个粘合剂的600个技术引理 另一方面,显式名称的使用使用户承担了编码α等价机制的负担。正如我们将看到的,从计算机辅助证明发展的角度来看,这代表了一个不平凡的任务,因为α等价经常被认为是理所当然的,而没有明确的公理化。通常只有一个简短的定义在自然语言中给出,然后是一些例子[1]。实际上,α-等价可以用不止一种方式严格定义;例如,除了“传统”的一种[1]之外因此,寻找这三个定义的等价性的形式证明是很自然的。1 由托斯卡MURST项目支持的研究。·c2002年由ElsevierScienceB出版。 诉 操作访问根据C CB Y-NC-N D许可证进行。31→→→→相反,遵循高阶方法,绑定器通过高阶构造器表示。因此,逻辑框架的元语言自动给出了α -等价。在没有对归纳类型的原生支持的类型论中,如Edinburgh LF,表示“λ“绑定器的自然选择然而,如果我们想利用像CIC这样的元语言的归纳因此,我们被迫为变量引入一个单独的类型,其结果是避免捕获的变量项替换不再委托给元级(弱HOAS)。此外,后者不能简单地定义为递归函数,而只能定义为关系。这就提出了关于其属性的问题,如功能性(决定论和总体性),组成等。最近,为了处理名义演算的(Meta)理论,作者提出了一组公理,称为上下文理论[11],源于最初在[12]中用于在Coq[13]中正式推导π演算的强后期双相似性的元理论的技术这些公理在理论水平上反映了变量的“上下文”和“发生”的直观概念的一些基本性质其非正式含义如下:变量的不饱和性没有一项可以包含所有变量;即,总有一个变量在给定项中不是自由出现的;上下文的可拓性两个上下文相等,如果它们在一个新变量上相等;即,如果M[x]=N[x]且ndx/∈M[·], N[·],则M=N。β-展开:给定一个项M和一个变量x,存在一个上下文N[·],使得N [x] = M,并且x不出现在N[·]中。本文运用语境理论对上述问题更确切地说,就FOAS编码而言,我们正式证明了α-等价的三种替代定义确实是等价的;就HOAS编码而言,我们证明了替换关系的功能性。我们将看到,在这两种情况下,语境理论都允许顺利地处理改名的基本概念,当这是通过潜在元语言的功能应用来呈现总之,上下文理论是一个强大的工具,可以对名义演算进行元推理,不仅是在HOAS中编码的情况下,而且即使是在具有显式名称的普通一阶方法的情况下。概要。在第一节中,我们简要回顾了无类型λ-演算。然后,在第二节中,我们给出了对象语言的一阶编码,我们描述和编码了我们考虑的三个α等价概念,并通过上下文理论正式证明了它们的等价性第3节我们32V·}提出了无类型λ演算和捕获避免替换的高阶编码,并正式发展了相关的元理论。最终结论见第4节。附录部分简要介绍了归纳构式演算和Coq证明助手。1对象语言Λ无类型λ-项的集合Λ由以下文法定义M,N::= x|(明尼苏达州)|λx.M其中x,y,z,. 在无限多个变量上的范围。项被取到α-等价。我们用M[N/x]表示N对M中x的捕获避免替换。上下文,即具有孔的项,由M[ ]表示。“自由变量”(FV)和“变量”(包括自由和约束)(V)的概念 对于X是一个有限的变量集,我们定义Λ X{M ∈ Λ|FV(M)X. 我们用Λ0表示Λ。对于一个介绍和全面的λ-演算理论的发展,见[1]。2一阶抽象逼近作为第一个案例研究,我们将解决编码三个α等价概念的问题[1]),在以前的正式研究中使用的变体的元理论的λ演算[15],并提出了替代配方[6].在这里,我们对采用基于HOAS的方法来编码对象语言的语法不感兴趣否则,逻辑框架的元语言将免费提供α-等价,并且无法在对象级别访问由于篇幅有限,我们无法介绍完整开发的所有结果;我们请感兴趣的读者参考[21]。2.1语法编码下面是一个简单的例子参数变量:设置。感应tm: Set:= var: Var-> tm| app:tm->tm->tm| lam:Var -> tm -> tm。需要注意的是,Var不是一个归纳集合。唯一可以存在于Var中的术语是元语言的变量,它们直接表示对象语言的变量事实上,Var不需要在-由于是由Λ的语法定义来归纳的,所以没有理由引入不必要的假设,即,归纳和递归原理。实际上,这些不需要的原则并非无害,因为它们可以被利用33►{|{\fn方正粗倩简体\fs12\b1\bord1\shad1\3cH2F2F2F}来定义外来术语此外,它们与我们将要使用的语境理论的性质不一致(详见[12])。对于X ={x1,..., xn},在整个论文中,我们将用Γ X表示由{x1 :Var,.,xn:Var}{dij:(Xi = xj)|1≤i Prop:=notin_var:(y:Var)~x=y ->(notin x(var y))|notin_app:(M,N:tm)(notin xM)->(notin x N)->(notin x(appMN))| notin_lam:(y:Var)(M:tm)(记为xM)->~x=y->(记为x(lam y M))。(notinx M)的直观含义是变量x不会出现在M中(既不是自由的也不是束缚的)。定义完全由签名驱动,遵循[12,11]的一般模式。关于Var类型的第二个公理是不饱和性质:公理unsat:(M:tm)(Ex [x:Var](notin x M)).作为一个技术性的注释,我们注意到,可以从一个更“一般”的不饱和属性中推导出unsat公理unsat_list:(l:var_list)(Ex [x:Var](notin_list x l)).在tm中缺少高阶构造子使得我们可以通过M上的结构归纳来导出β-展开公理(对于普通项):引理EXP:(M:tm)(x:Var)(Ex[N:Var->tm](notin_context x N)/|M=(N x))。34≡另一方面,外延性和单调性公理仍然需要假设:公理ext:(F,G:Var->tm)(x:Var)(notin_context x F)->(notin_context x G)->(F x)=(G x)-> F=G.公理notin_mono:(M:Var->tm)(x,y:Var)(notin x(M y))->(notin_context x M)。这里的notin上下文是[x:Var][F:Var->tm]((y:Var)~x=y ->(notin x(F y)。注意单调性公理在引言中没有被引用。实际上,如果我们假设在上下文水平上也存在不饱和性,那么这个性质可以通过使用上下文理论的其他公理对项进行归纳而得到。2.3α-等价的编码(I)我们以[1]中的以下定义为起点定义2.2(i)M中约束变量的变化是用λy替换M的部分λx.N。(N[x:=y]),其中y在N中(根本)不出现。(因为y是新的,所以在替换N[x:=y]中没有危险)。(ii)M与N是α-同余的,记为MαN,如果N由M通过约束变量的一系列变化很明显,一个新的重命名机制是α等价概念的核心因此,我们首先引入以下归纳谓词,实现一个简单的重命名(即,它不检查新变量是否是新鲜的):感应change_var [x,y:Var]:tm -> tm -> Prop:=change_var_var1:(change_var x y(var x)(var y))|change_var_var2:(z:Var)~x=z->(change_var x y(var z)(var z))| change_var_app:(R,S,R’,S’:tm)(change_var x y R R’)->(change_var x y S S(change_var x y(appRS)(app R|change_var_lam1:(M,M':tm)(change_varx y M M')->(change_var x y(lam x M)(lam y|change_var_lam2:(M,M ':tm)(z:var)~x=z ->(change_var xy M M')->(change_var x y(lam z M)(lam z通常,(改变xyMN)仅在以下情况下成立:t_m_N是将x的每个出现(自由或束缚)替换为y的结果。更正式地说,下面的结果说明了变化varw.r.t.其推理规则如图1所示命题2.3(变化的一致性var)设X∈ V有限,x,y∈V35−x[x:=y]=y(CVVAR1)M[x:=y] =MJ(λx.M)[x:=y]=λy.MJ(CV LAM 1)x/=z(CVVAR2)M[x:=y] =MJx z(CV LAM2)z[x:=y]=z(λz.M)[x:=y]=λz.MJM[x:=y] =MJN[x:=y]=NJ(MN)[x:=y]=MJNJFig. 1. 改变λ项中的变量。(CVAPP)合理性:如果存在t使得Γ XΛt:(改变var x y M N),则我们有δX(M)[x:=y]=δX(N)。完备性:设M,N∈Λ X,使得M [x:= y] = N,则存在标准型t,使得Γ XΛ t:(change var x yεX(M)εX(N)).证据很容易通过命题2.1和归纳法证明的结构的标准形式(健全性),并归纳的结构的变量变化的判断(完整性)的推导。✷然而,“盲目地”改变变量而不检查新变量是否是新的)可能产生捕获在执行替换之前空闲的变量的出现例如,让我们考虑项(lam x(app xy))=εx,y(λx.xy),然后我们可以导出(changevar y x(lam x(app xy))(lam x(app xx x),它对应于下面的方程(λx.xy)[y:=x] =λx.xxy在λx.xy中的自由出现一旦被x替换就被捕获了,而λ-项λx.xy和λx.xx不是α-等价的。因此,我们必须确保,当替换λ项中的变量时,新的变量是新鲜的。新鲜度的编码是通过我们在2.2节中介绍的notin谓词来实现的归纳alphaBar:tm -> tm -> Prop:=alphaBar_var:(x:Var)(alphaBar(var x)(var x))|alphaBar_app:(M,M',N,N':tm)(alphaBarMM')->(alphaBarN| alphaBar_lam1:(x:Var)(M,N:tm)(alphaBar M N)->(alphaBar(lam x M)(lam x N))|alphaBar_lam2:(x,y:Var)(M,N:tm)(记为y M)->(change_var x yMN)->(alphaBar(lam x M)(lam yN))| alphaBar_trans: (M,N,R:tm)(alphaBar M R) -> (alphaBar R N) ->(alphaBar M N).前三个构造函数是同余规则,第四个是约束变量变化规则,最后一个是传递性(回想一下,两个项可以通过约束变量的一个或多个变化来区分36∼· −命题2.4(alphaBar的精确性)(i) (合理性)设XΛt:(α BarMN),则有δX(M)<$αδX(N)。(ii) (完备性)设X <$V有限,M,N ∈ ΛX,则若M <$αN有 一个标准型t使得ΓXΛt:(α BarεX(M)εX(N))。证据 这个结果也可以用命题2.3中规定的相同技术直接证明。✷由于前面的充分性定理,alphaBar可以被看作是一个具体化,为了忠实地表示α等价的概念,我们将要研究的后续定义必须满足这个具体化。2.4α-等价的编码(II)在[15]中,提出了α-等价的另一种编码;根据我们对λ-演算的表示将其转换,我们得到以下定义:感应alpha:tm -> tm -> Prop:=alphaMKP_var:(x:Var)(alphaMKP(var x)(var x))|alphaMKP_app:(M,M',N,N':tm)(alphaMKP M M')->(alphaMKP NN')->(alphaMKP(appM N)(appM| alphaMKP_lam:(x,y,z:Var)(M,M',N,N':tm)(记为zM)->(记为z N)->(change_var x zM前两个构造函数(alphaMKP var和alphaMKP app)是同余规则,而alphaMKPlam构造函数指出,为了建立λx.M和λy.N的等价性,我们必须选择一个新的名字z(在M和N中根本不出现),并证明M[x:=z]与N[y:=z]是α等价我们正式证明了alphaBAR和alphaMKP的等价性:引理ALPHABAR_ALPHAMKP:(A,B:tm)(alphaBar A B)->(alphaMKP A B). 引理ALPHAMKP_ALPHABAR:(A,B:tm)(alphaMKP A B)->(alphaBar A B).这两个引理都是在前提推导的基础上用结构归纳法证明的。第二个证明是平凡的,而第一个需要作为初步结果证明ALPHAMKP的传递性。为了得到它,我们遵循了[15]中开创的方法。2.5α-等价的编码(III)在[6]中,α-等价关系被证明等价于图2中描述的规则定义的二元关系(其中(a b)()代表变量转置运算)。正如在[6]中所观察到的,变量转置是一种比其他重命名概念更基本的操作(例如,文本和37J···x∈V(GP-α-VAR)M1M1JM2M2J(GP-α-APP)xxM1M2M1JM2J(z x)·M(z y)·MJ(z不出现在M,MJ中)(GP-α-LAM)λx.M<$λy.M图二、Gabbay-Pitts关于α-等价的另一种定义捕获避免替换)。事实上,(y x)M意味着x的所有发生都被y的发生所取代,反之亦然(而不用担心最终的捕获)。这样的机制可以通过HOAS以非常自然的方式表达;事实上,如果x和y是出现在M中的两个不同的变量,并且εX(M)=M,那么我们可以导出2,存在上下文M ':Var->Var->tm,使得x和y不出现在M'中,则运算(y x)M可以简单地表示为(M此外,如果y不发生在M中,我们有M=(到因此,(y x)M可以用(M“y)表示,而不需要求助于二元上下文。因此,α-等价的Gabbay-Pitts公式的编码由以下归纳谓词给出:归纳alphaGP:tm -> tm -> Prop:=alphaGP_var:(x:Var)(alphaGP(varx)(var x))|alphaGP_app:(M,M',N,N':tm)(alphaGP M M')->(alphaGP NN')->(alphaGP(appM N)(appM| alphaGP_lam: (M,N:Var->tm)(x,x’,y:Var)(notin_context x M) ->(notin_context x’ N) -> (notin_context y M) ->(notin_context y N) -> (alphaGP (M y) (N y)) ->(alphaGP (lam x (M x))(lam x’(N x’))).正如我们所看到的,唯一的分歧w.r.t. alphaMKP的定义在涉及lam构造函数的规则中。事实上,alphaMKP和alphaGP在形式上是等同的:引 理 ALPHAMKP_ALPHAGP : ( A , B : tm ) ( alphaMKP A B ) ->(alphaGP A B). 引理ALPHAGP_ALPHAMKP:(A,B:tm)(alphaGPA B)->(alphaMKP A B).这两种证明都是通过对前提推导的归纳来进行的。唯一有趣的情况与lam构造函数的引入规则有关:为了得出结论,一个关键性质如下(通过M上的结构归纳以及扩展性和可拓性性质证明):引理CHANGE_VAR_RW:(M,N:tm)(x,y:Var)(change_var xy M N)->(M ':Var->tm)(notin_context x M')-> M=(M' x)->N=(M' y)。2推导利用引理EXP(在2.2节中提出)和公理一元上下文的β-展开和单调性。38在ALPHAGP ALPHAMKP的证明中,必须证明另外一个新的重命名结果:引理ALPHAMKP_RW:(A,B:tm)(alphaMKP A B)->(x,z:Var)(记为z A)->(记为z B)->(A':tm)(change_var X z 一 A ')->(原 因 是 ( notin contexty M ) 和 ( notin contexty N ) 不 一 定 意 味 着(notiny(Mx))和(notiny(N因此,我们不能使用名称y归纳假设提供了一个新的变量,但我们必须选择一个全新的变量才能得出结论。3高阶抽象逼近在本节中,我们采用了一种众所周知的λ演算的高阶表示对变量使用了一种单独的类型(弱HOAS)。由此可见,我们不能把替换定义为递归函数,而只能定义为关系。我们将证明这个关系确实是泛函的。由于篇幅有限,我们无法展示关于这种编码的完整开发的所有结果;我们请感兴趣的读者参考[17]。3.1语法形式化Λ的语法的HOAS表示如下:参数变量:设置。感应tm: Set:= var: Var -> tm|app:tm->tm->tm|lam:(Var -> tm)-> tm。强制var: Var >-> tm。将var声明为强制转换允许我们将类型Var中的项隐式注入到tm中,因此在下文中,可以从项中省略此构造函数在FOAS编码中,我们不将Var定义为归纳集, 为了能够证明陈述的充分性,并避免与语境理论不一致注意lam是一个高阶构造函数,也就是说它接受一个函数项作为参数。特别地,Var->tm类型的项精确地表示λ演算的避免捕获的上下文。这种技术允许从元语言中继承术语的α-等价,并且仍然对术语有归纳定义例如,λx。(xx)和λy。(yy)代表-分别由(lam[x:Var](app(var x)(var x)和(lam[y:Var](app(var y)(var y)表示,它们是相同的项,直到α转换。同时,我们可以通过一阶递归或案例分析来定义函数分析术语的语法。这种编码的充分性,已经在[17]中证明,是[11,定理1]的结果。 对于X={x1,..., xn}是一组有限的变量,回想一下,39TMX{M|Γ X<$M:tm,M的长βη-正规形}。命题3.1对于所有X有限个变量集,存在Λ X和tm X之间的双射εX。此外,这个双射是合成的,在这个意义上,如果M∈ Λ X,x和N∈ Λ X,那么εX(M [N/x])= εX,x(M)[εX(N)/(var x)]。作为推论,(捕获避免)上下文M[·]∈ΛX自然编码为[z:Var]εX,z(M(z)),其中新变量z充当事实上,像命题3.1那样的双射可以在上下文和Var->tm类型的术语之间建立。3.2甲醛化取代至于α-等价,避免捕获的替代并不总是被详细定义。典型地,它倾向于成为(参数)函数·[N/x]:Λ→ Λ递归地定义在术语的语法上,例如如下。x[N/x] =Ny[N/x]=y(x y)(M1M2)[N/x] =(M1[N/x]M2[N/x])(λ y.M)[N/x]=λ y. (M[N/x])(x=/y)值得注意的是,为了有一个总函数,这个定义必须被提升到α等价。这意味着,在λ -抽象的情况下,当y正好是x,则存在“无声”(即,隐藏)(λy.M)到(λz.M[z/y])的转换,其中z可以任意选择。因此,避免捕获替换的定义通常不是先验确定的,因为它需要上下文的约束变量的任意α转换,以避免捕获替换项中的自由变量 更复杂的语言(例如,动态逻辑,Hoare逻辑[16])可能需要非标准的替换,涉及人为的转换概念,而不仅仅是α-转换。如果我们使用完整的HOAS编码,则捕获避免替换可以完全委托给逻辑框架的元语言。以这样在这种方法中,变量将没有特定的类型Var,λ构造函数将简单地呈现为lam:(tm -> tm)-> tm。 因此,上下文将被表示为类型tm -> tm的映射,并且因此替换变成上下文对替换项的应用然而,完整的HOAS编码与Coq的归纳定义不兼容,因为它们不满足正性条件,这(大致)要求我们定义的类型(tm)不会出现在任何构造函数的任何参数的类型中的负出于这个原因,我们采用了弱HOAS编码,如上所述。然而,这种解决方案的一个缺点是,我们不能再将替换委托给Meta语言。相反,我们需要手工定义它,作为逻辑编程风格中上下文和术语之间的参数关系(如[5]):感应subst [N:tm]:(Var->tm)-> tm -> Prop:=subst_var:(substN var N)|subst_void:(y:Var)(subst N [_:Var]y y)40| subst_app: (M1,M2:Var->tm)(M1’,M2’:tm)(substN M1(substN[y:Var](app(M1y)(M2y))(appM1'M2'))|subst_lam:(M:Var->Var->tm)(M':Var->tm)((z:Var)(substN[y:Var](M y z)(M(subst N [y:Var](lam(M y))(lam M'))。因此,项MJ在语法上等于置换M(x)[N/x] i(substN M更正式地说,subst的(证明无关的)充分性如下:命题3.2设X是一个有限的变量集,x是一个不在X. 设N,MJ∈ Λ X,M∈ Λ X±{x}. 然后又道:M[N/x] =MJ<$$> ΓX<$:(subst εX(N)[x:Var]εX±{x}(M)εX(MJ))把CIC中的代换表示为一个关系式,它 可 能 不 是 完 全 的 , 也 就是说 ,对于 某个 N,M ,不 存在 MJ ,使 得MJ=M[N/x]。事实上,这样的定义确实给出了一个函数(即,确定性和总)关系是一个性质,我们要证明明确地运用语境理论。3.3HOAS中Λ的语境理论鉴于句法的特征,语境理论由两部分组成第一部分包含“发生”谓词的定义这些定义直接来自语言的签名,遵循[12,11]中的模式。归纳符号[x:Var]: tm -> Prop:=notin_var:(y:Var)~x=y->(notin xy)| notin_app:(M,N:tm)(notin xM)->(notin x N)->(notin x(appMN))| notin_lam:(M:Var->tm)((y:Var)~x=y->(notin x(M y)))->(记为x(lam M))。感应isin [x:Var]:tm -> Prop:=isin_var:(isinx x)| isin_app1: (M,N:tm)(isin x M) -> (isin x (app M N))| isin_app2:(M,N:tm)(isin x N)->(isin x (app M N))|isin_lam:(M:Var->tm)((y:Var)(isin x(My)->(isin x(lam M))。关于变量名(变量),我们唯一需要知道的是Var上的等式是可判定的。然而,我们不需要一个完整的经典逻辑:在出现检查谓词上有一个经典行为就足够了公理LEM_OC:(M:tm)(x:Var)(isin x M)\/(notin x M).41这意味着(eq Var)的可判定性。42··然后,我们可以假设我们需要的语境理论的公理公理unsat:(M:tm)(Ex [x:Var](notinx M)).公理ext_tm:(M,N:Var->tm)(x:Var)(notin x(lam M))->(notin x(lamN))->(Mx)=(Nx)-> M=N。公理ext_tm1:(M,N:Var->Var->tm)(x:Var)(notinx(lam [z:Var](lam(Mz)->(记为x(lam [z:Var](lam(Mz)->(M x)=(N x)-> M=N。下面是语境理论和关于tm的归纳原理的直接结果。引理不同:(x:Var)(Ex [y:Var]~x=y)。引理isin_notin_absurd:(x:Var)(M:tm)(isinx M)->(notinx M)-> False。Coq和类似的系统不提供高阶类型的归纳:在A->B上没有归纳原理,即使A和/或B是归纳的。这是因为A->B(通常是一个函数空间)的含义不是初始代数。因此,大多数证明编辑器没有给出归纳原则、案例分析、倒置谓词和类似的推理工具类型为Var->tm,即,contexts.然而,可以证明Var->.. ->形式的类型Var->tm确实有递归和归纳原理[10,2,11,5]。因此,除了上面的上下文理论的简单公理,我们可以根据需要安全地假设高阶归纳和递归原理(假设Var是无构造函数的),就像下面的Var->tm上的归纳(注意有两种基本情况):公理tm_ind1:(P:(Var->tm)->Prop)(P var)->((y:Var)(P [_:Var](var y)->((M,N:Var->tm)(P M)->(P N)->(P [x:Var](app(Mx)(N x)->((M:Var->Var->tm)((y:Var)(P [x:Var](M x y)->(P [x:Var](lam(Mx)->(M:Var->tm)(PM)。注意,我们没有假设β展开。非正式地,β-exp指出,给定一个项M和一个变量x,存在一个上下文N[ ],使得N[x] =M,并且x不出现在N[ ]中。这已经在π-演算的元理论的发展中使用了几次[12]。另一方面,在目前关于Λ的工作中,它并不需要一个可能的动机是,在这里我们允许高阶归纳,而在[12]中,我们必须通过简单的一阶项从归纳中恢复它433.4(Meta)替代3.4.1替代决定论我们要证明的性质如下:参数N:tm.引理 subst_is_det:(M:Var->tm)(M1:tm)(substN M M1)->(M2:tm)(substN M M2)->(M1 =M2)。我们给出了这个性质的两个证明。第一个是对(substN M M1)的推导进行归纳。这就产生了四种情况:N:tmM:var->tmM2:tmH:(subst N Var M2)==次级目标2是:(y)=M2次级目标3为:(应用程序M1'M2')=M0子目标4是:(lam每一个都应该通过颠倒假设H(或相应的)来处理通常,这样的反演会自动消除所有荒谬的情况,但当必须判别的项是高阶项时,这就不起作用了实际上是这样的,因为subst的第二个参数的类型是Var->tm。逆H策略为第一个目标提供了四种情况,其中一个是平凡的真理,另一个是荒谬的:次级目标1是:N:tmM:Var->tmM2:tmH:(subst NvarM2)H0:var=varH1: N=M2===...次级目标2是:N:tmM:Var->tmM2:tmH:(subst NvarM2)y:VarH1:([_:var](y))=var H0:(y)=M2==荒谬的情况下(冗长)消除使用理论的背景,特别是公理的外延。整个证明长达95行,其中大部分涉及荒谬案件的消除3.4.2替代决定论,再次一个更短的证明可以通过证明一个合适的高阶反演引理来获得。在Coq中,反演引理是通过反演策略自动合成的,并使用最初由Murthy实现的算法以及随后由Cornes和Terrasse [4]详细说明的递归原理进行证明然而,当我们必须区分是高阶时,该算法无法给出正确的反演谓词,因为通常的归纳类型理论不承认高阶类型为归纳类型。然而,我们知道Var->tm形式的类型确实有递归原则[10,2,11]。因此,我们可以始终44引入这些原则(作为公理)来定义反演谓词中所需的递归参数subst_inv_fun: tm->(Var->tm)-> tm-> Prop。公理subst_inv_fun_var0:(N,M:tm)(subst_inv_funN var M)==(N=M).公理subst_inv_fun_var1:(y:Var)(B,N:tm)(subst_inv_funN[_:Var]yB)==((var y)=B).公理subst_inv_fun_app:(A1,A2:Var->tm)(B,N:tm)(subst_inv_funN [x:Var](app(A1 x)(A2x))B)==(EX B1|(EX B2)|(app B1 B2)=B/\(subst N A1 B1)/\(subst N A2 B2)。公理subst_inv_fun_lam:(A:Var->Var->tm)(B,N:tm)(subst_inv_funN [x:Var](lam(A x))B)==(EX A1|(lam A1)=B/I(y:Var)(subst N [x:Var](A x y)(A1y)。然后,高阶反演原理被引理subst_inv:(A:Var->tm)(B,N:tm)(subst N A B)->(subst_inv_fun N A B). Intros; Inversion_clearH.重写subst_inv_fun_var0;自反性。[...]Qed。使用这个反演引理,替换决定论的证明就容易得多了(12行)。事实上,我们3.4.3替代的总体性由于CIC的一些特殊性,总体性的证明是棘手的。我们要证明的引理是引理subst_is_total:(M:Var->tm)(EX M'|(subst N M M '))。我们的目的是通过M上的高阶归纳法来证明这一点。这在lambda抽象的情况下失败了,如下所示N:tmM:Var->tmM0:Var->Var->tmH:(y:Var)(EX M ':tm|(subst N [x:Var](M0 x y)M'))============================(EX M ':tm|(subst N [x:Var](lam(M0 x))M'))适当的项应从假设H中得到。然而,Coq不允许我们消除一个命题(如H)来构建集合(M' in tm)中的一个项。这种“强的非线性类型的消除”可能导致不一致,因此被类型理论CIC排除[3]。我们采用的解决方案是将整个证明移动到集合领域,然后将结果提升到Prop。因此,我们引入了归纳原理的集合类型版本--等价地,它可以被看作是一个递归,45依赖类型:公理tm_rec1:(P:(Var->tm)->Set)(P var)->((y:Var)(P [_:Var](var y)->((M,N:Var->tm)(P M)->(P N)->(P [x:Var](app(M x)(N x)->((M:Var->Var->tm)((y:Var)(P [x:Var](M x y)->(P [x:Var](lam(Mx)->(M:Var->tm)(PM)。这样一个原则的可靠性可以通过将[10,2]中的模型构造移植到依赖类型来建立然后,我们用高阶相关递归证明了Set中的总体引理:(N:tm)(M:Var->tm){M ':tm|(subst NM M ')}。Intros;模式M;应用tm_rec1;Intros;清除M。[...]Qed。注意,在lambda的情况下,所需的项是通过消除(投影)假设H中实例化在局部绑定(因此是新鲜的)变量y上的n-类型来构建的。那么,总体性定理就是从M-型(sitM)中抽取逻辑部分:引理subst_is_total:(M:Var->tm)(Ex [介绍一下测试(proj1_sig??(sitM))。应用proj2_sig。Qed。3.4.4提取替代函数引理sit可以看作是替换函数的具体化。我们可以通过提取该类型的第一个分量(sitN M)来推导它:引理subst_f:tm->(Var->tm)->tm.IntrosN M; Exact(proj1_sig??(sitNM))。Qed。其中,添加了一点语法糖,采用了熟悉的形式[ ],就像下面的引理subst_f_verif:(N,V:tm)(M:Var->tm)(subst N MV)-> M[N]= V。引理subst_f_var:(N:tm)(var[N])=N。介绍;应用subst_f_verif;应用subst_var. Qed。引理subst_f_void:(N:tm)(y:Var)(([_:Var]z)[N])=z. 引理subst_f_app :(N:tm)(M1,M2:Var->tm)(([x:Var](app(M1 x)(M2 x)[N])=(app M1[N]M2[N])。引理subst_f_lam:(N:tm)(M:Var->Var->tm)(([x:Var](lam(M x)[N])=(lam([y:Var](([x:Var](M x46y))[N])。47/当然,函数subst_f的应用实际上不能减少,因为递归tm_rec1是一个公理,因此没有计算内容。然而,可以通过外部ML程序来“实现”它,该程序在这种情况下,subst_f将是人们所想到的全边缘捕获避免替换。替换的一个有趣的性质是复合:对于M,N,P项和x=y,我们有(P[Q/y])[M/x]=(P[M/x])[Q[M/x]/y]。该语句的形式化需要具有2个漏洞的上下文引理subst_f_comp:(M:tm)(Q:Var->tm)(P:Var->Var->tm)(([x:Var]((Px)[(Qx)]))[M])=([y:Var]([x:Var](Px y))[M])[Q[M]])。除了使用公理ext_tm和unsat之外,这个性质的证明通过P的结构上的结构归纳来进行;因此我们需要假设Var->Var->tm上的相应归纳原理:公理tm_ind2:(P:(Var->Var->tm)->Prop)(P [x,y:Var]x)->(P [x,y:Var]y)->((z:Var)(P [_;_:Var](var z)->((M,N:Var->Var->tm)(P M)->(P N)->(P [x,y:Var](app(M xy)(N xy)->((M:Va
下载后可阅读完整内容,剩余1页未读,立即下载
cpongm
- 粉丝: 5
- 资源: 2万+
上传资源 快速赚钱
- 我的内容管理 展开
- 我的资源 快来上传第一个资源
- 我的收益 登录查看自己的收益
- 我的积分 登录查看自己的积分
- 我的C币 登录后查看C币余额
- 我的收藏
- 我的下载
- 下载帮助
最新资源
- C++标准程序库:权威指南
- Java解惑:奇数判断误区与改进方法
- C++编程必读:20种设计模式详解与实战
- LM3S8962微控制器数据手册
- 51单片机C语言实战教程:从入门到精通
- Spring3.0权威指南:JavaEE6实战
- Win32多线程程序设计详解
- Lucene2.9.1开发全攻略:从环境配置到索引创建
- 内存虚拟硬盘技术:提升电脑速度的秘密武器
- Java操作数据库:保存与显示图片到数据库及页面
- ISO14001:2004环境管理体系要求详解
- ShopExV4.8二次开发详解
- 企业形象与产品推广一站式网站建设技术方案揭秘
- Shopex二次开发:触发器与控制器重定向技术详解
- FPGA开发实战指南:创新设计与进阶技巧
- ShopExV4.8二次开发入门:解决升级问题与功能扩展
资源上传下载、课程学习等过程中有任何疑问或建议,欢迎提出宝贵意见哦~我们会及时处理!
点击此处反馈
安全验证
文档复制为VIP权益,开通VIP直接复制
信息提交成功