可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）125-142www.elsevier.com/locate/entcsCanonical HybridLF：扩展具有依赖类型的Roy L.克罗尔1 艾米·卡里斯2地址：University Road，Leicester，LE1 7RH，U.K.摘要本文介绍了一种用于证明演绎系统性质的元逻辑--典范混合LF（CHLF），它是在Isabelle HOL语言中实现的.CHLF与其他两种元逻辑学密切相关。 第一个是Harper，Honsell和Plotkin的Edinburgh Logical Framework（LF）第二种是混合动力系统，Ambler、Corle和Momigliano提出了一个基于无类型lambda演算的高阶抽象函数（HOAS）。历史上，HOAS存在两个问题：它与归纳类型的不兼容性以及异国情调的术语。Hybrid为这些问题提供了部分解决方案，其中包含元逻辑中的绑定变量的HOAS函数自动转换为对用户隐藏的机器友好的de Bruijn表示。CHLF的关键创新是用LF风格的依赖类型lambda演算替换了无类型lambda演算。CHLF允许使用HOAS接口输入包含表示对象逻辑的判断和语法的常数的签名，以及关于其判断的元定理的证明。 签名中定义的元定理有效的证明是使用 Schurmann和Pfenning的M2元逻辑我们在现有的Hybrid版本上做了一些改进：我们现在有了依赖类型的效用; Hybrid的单一约束变量能力现在可能是无限的;一个类型系统扮演了这个角色。混合格式良好的谓词;使用核心数据库的特殊元素指示错误的旧方法被替换为使用Isabelle选项类型的更精简的方法关键词：依赖类型，HOAS，逻辑框架，元逻辑推理，变量绑定1介绍本文讨论了逻辑、程序设计语言等演绎系统的推理问题，一般把典型的演绎系统称为对象逻辑。人们可以通过将对象逻辑转换为元逻辑，然后在元逻辑中进行推理来推理对象逻辑，只要对象逻辑的属性在元逻辑中得到适当的反映特别是，本文涉及高阶抽象代数。这是一个众所周知的元逻辑技术，可以应用于对象逻辑，1电子邮件：rlc3@le.ac.uk2电子邮件：mjf29@le.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2016.06.0091571-0661/© 2016作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。126R.L. Crole，A.理论计算机科学电子笔记323（2016）125变量绑定：HOAS元逻辑的变量绑定用于实现对象逻辑的变量绑定第一作者，克罗尔，以及Ambler和Momigliano，开发了混合系统[1]。这是一个在Isabelle HOL软件包中实现的高阶抽象语法。关键的新颖特征是用户可以使用“用户友好的”命名绑定变量写下高阶抽象语法包将这种语法转换为“机器友好”的HOAS的使用并非没有问题。一个问题是HOAS通常与归纳不兼容。然而，HYBRID提供了一个部分解决方案，并为用户提供了一种形式的HOAS，它始终嵌入（Isabelle）HOL中，因此具有归纳原理[1]。混合系统由无类型λ-演算支撑。虽然作者和其他研究人员已经成功地使用了混合体（参见例如[12，9]），但我们认为考虑是否可以开发一个类型化版本是有趣的这不仅仅是智力上的好奇心。 当使用混合体时，通常必须实现部署在归纳定义中的良构谓词。但是在类型化系统中，这些谓词可能是多余的，而是使用类型来构建格式良好的表达式。这对用户来说既有趣又是潜在的重要简化和优势HYBRID的核心是将无类型的高阶语法映射到一阶语法的转换函数。我们的贡献是表明，转换技术不仅扩展到一个简单的类型设置，但实际上是一个新的系统，CANONICAL混合LF，这是依赖类型。我们确实可以免除格式良好的谓词。此外，新系统提供了一种具有判断类型方法的推理方式。首先，我们开发了一个扩展的混合基于简单类型的λ-演算。在开发了忠实于支持混合体的概念思想的合适的转换函数之后，我们开始考虑依赖类型。我们决定探索使用Edinburgh LF [10]作为基础，因为它是一个元推理系统，HYBRID也是如此。然而，尽管HYBRID（和简单类型版本）提供了一个λ-演算HOAS接口来编码对象系统，之后用户可以直接在（伊莎贝尔）高阶逻辑中进行推理，但基于LF的HYBRID版本可能意味着在通用战术定理证明器使用判断作为类型进行推理的可能性。事实上，Canonical LF支持CANONICAL HYBRID LF（见第3.1节的进一步细节）。LF和规范LF都有优点和缺点。选择规范LF而不是LF作为我们系统的基础的关键因素是规范LF中等式的简单性和关于我们用于LF的统一算法的终止的技术问题这一点，以及类型的可判定性，将在未来的工作中讨论，但在这里，我们集中在CANONICAL混合 LF。还有更多关于[5]中的杂交。 的一个版本HYBRID是由马丁[12]和艾米·法蒂玛创建。 版本的溷合体 在Coq[3]和[9]中出现了Capretta，Festival和Habli的工作。在[15]中利用了我们将高阶语法减少到一阶R.L. Crole，A.理论计算机科学电子笔记323（2016）125127在第2节中，我们概述了混合系统。我们向读者指出原始论文，并提供一些必要的背景阅读。在第3节中，我们简要回顾了规范LF逻辑框架的细节，然后详细描述了本文的主要贡献，如引言所述。在第4节中，我们给出了一些例子，包括量化命题逻辑的HYBRID和CANONICAL HYBRID LF编码的直接比较，并讨论了我们系统中证明逻辑2混合元逻辑在Hybrid中，任何对象逻辑的术语都是由用户输入的，作为具有命名绑定变量的HOAS元逻辑术语。这些术语然后被自动转换成一种无名的de Bruijn形式，其中约束变量的实例由数字索引或水平给出。 这个想法是用户可以使用命名术语，而机器可以使用自动生成的等效无名术语。该系统是命名变量绑定和无名变量绑定的“混合体”。 （HYBRID使用局部无名的de Bruijn项[2]：绑定变量由BND的实例表示，并且具有自然数索引;自由变量由VAR的实例表示，并且也由自然数索引。HYBRID的原始版本是作为Isabelle的包实现的。定理证明器该实现基于核心归纳数据类型expr实现本地无名de Bruijn术语：定义2.1[核心混合数据类型]Ja expr：：=BND nat|VAR自然值|CONJa|ABS expr|APP expr expr|ERR`expr$$exprxCON构造函数用于表示对象逻辑常量的实例。expr类型有一个类型参数“a”，该类型的元素用于指定对象逻辑的常量。 对象构造函数、将在混合体中呈现为CONJa（例如，Ja = cForAll|cests specifies object logic quantifier）。APP构造函数表示应用程序（通常写为fix $$），ABS构造函数表示（de Bruijn）函数抽象。最后，ERR构造函数是一个特殊的元素，用于指示从HOAS函数到de Bruijn索引的转换过程中是否发生错误。在HYBRID中，一个通用的HOAS项λv.e被用户写成LAMv.e;这是合法的Isabelle语法。因此，混合型用户可以将λv.φ写成：（CONcforAll）$$（LAMv.φ）重点是，HYBRID为HOAS提供了一个非常自然的用户为了进一步解释，LAMv.e是lambda（λv.e）的缩写，其中lambda是自动将λv.e转换为de Bruijn项的伊莎贝尔函数，并且128R.L. Crole，A.理论计算机科学电子笔记323（2016）125摘要（参见 （第3.3节）lbind（参见 （第3.4节）λ表示Isabelle函数抽象。λ是混合系统的核心完整的细节可以在[1，5]中找到。在这里，我们不能详细解释lambda实现背后的直觉，但给出一个简短的概述和Isabelle定义。lambda（λv.e）定义为ABS（lbind0（λv.e））。读者需要知道的主要事情3是(i) 该函数测试λv.e是否为（一元）混合体抽象（这是转换的先决条件）。(ii) Bruijn形式。函数执行λv.e到de为了解释抽象的概念，我们首先回忆一下形容词dangling和level（这是deBruijn术语的著名性质）。 中的变量BNDj如果在从j开始的路径上出现j个或更少的ABS节点，则称项e是悬空的到e的根。 例如，在示例项T=ABS（BND0$$BND1）中， 绑定变量实例BND0不是悬挂的，因为没有这样的ABS节点，但BND1确实是悬空的。术语溷合体 有一个水平。一个如果将e包围在l个ABS节点中，则任意项e处于l≥1级，结果表达式没有悬挂变量。例如，术语T将处于级别1，因为它需要一个额外的封闭ABS来确保没有变量悬空。0级的项现在我们来定义抽象。非正式地说，一元抽象是一个第一级的表达式，其中任何悬挂索引都被元变量（比如v）替换，然后被抽象（用λv包围）。 一个例子是A = λv。 ABS（BND 0 $$v）。这是一关键的想法。 德布鲁因指数之间的直接对应，如T中的BND 1，以及元逻辑的结合机制，如λv. . ......你好。V在A中，设置。在原始的H YBRID[1]中，有一个谓词abstr，它定义了它的参数是有效的一元抽象。它是使用归纳关系abst实现的。 这里省略了定义，但背景细节见[1]。abstr的正式定义是abstreabst0e。简单地说，abstr的工作原理是通过expr构造函数递归e，在每次调用时删除构造函数，并将每个λv移向e的叶子节点。当在每个ABS节点上递归时，索引i增加，因此对节点进行计数在一片叶子上，λv. v和λv一样被认为是一个抽象。变量;在叶λv的情况下。BNDj，i现在等于从叶子到根的路径上的ABS节点的数量，因 此 BNDj 不 是 悬 挂 的 ， 只 要 j< i 在 这 种 情 况 下 λv 。 BNDj 是 一 个 抽 象 。Overallabstr返回叶节点结果的合取。lbind使用归纳关系lbnd来定义。这里省略了定义，但背景细节见[1]。lbind被定义为lbindi es。lbndi e s. lbind的工作原理是通过expr构造函数递归e，保留每个构造函数，并将每个λv移向e的叶子节点。索引i在每个ABS节点上递归时增加，因此对它们进行计数。在一片叶子上，λv. V被替换为3.参考文献中引用了abstr和lbind的CANONICAL HYBRID LF类似物的描述。R.L. Crole，A.理论计算机科学电子笔记323（2016）125129ααa：K∈KIND中文（简体）r，x：A M：AJABSCANTYΓ ►Σ λx.M：λx：A.AJrP：x：A.KrM：A[M/x]kK=KJ应用实物Γ ►ΣP M:KJx：A∈ Γ瓦尔泰Γ ►Σx:Ac：A∈ C孔阿蒂Γ ►Σ C：AΓ ►ΣR：Π x：A.AJΓ ►Σ M：A[M/x]aAJ=AJJ应用程序在TYΓ ►Σ R M：A图1.一、规范LF判断，具有签名和上下文ΓBNDi，正确的de Bruijn指数。 所有其他叶节点保持不变。3Canonical HybridLF3.1关于Canonical LFLF有一个标准型的概念，在[10]中，它由种类、类型和β-正规、η-长的项组成，并对应于对象逻辑的项。它还有定义上的平等的概念。LF中的所有表达式都有一个标准形式。Watkins等人[20]给出了LF的规范表示，其中由于语法的限制，只有规范形式的种类，术语和类型可以形成，将定义相等还原为语法相等。这确保了只有真正代表对象逻辑的项的LF项才能存在，并且消除了对定义相等的推理的需要。正则LF的语法如下：定义3.1K：：= k类型|x：A.KA：：= a P|x：A.A P：：= pa|PM M：：= m R|λx.MR：：= rx|C|R M这里我们使用K表示任意类型，A表示规范类型，P表示原子类型，M表示规范项，R表示原子项。签名由空签名组成，或者是一个项常量c和类型常量a及其类型或种类的列表。不需要像Harper等人[10]在原始LF论文中那样定义定义等式关系正则LF的类型规则如图1所示。这个“典型”的主要缺点是130R.L. Crole，A.理论计算机科学电子笔记323（2016）125α这种方法的一个缺点是，在执行替换时需要一定的小心。然而，Watkins等人定义了一个合适的遗传替代概念，事实上我们遵循Harper和Licata给出的定义[11]。在我们的论文中，我们不再进一步讨论这个问题，除了注意到我们用[M/x]<$i表示遗传替换，其中α是由类型擦除定义的M的简单类型（见[11]），而<$是定义3.1中的句法范畴。3.2核心数据类型本质上，最初的混合体是一个系统，它为无类型的λ演算提供了一个HOAS接口。如第2节所述，用户然后，这些术语自动转换为de Bruijn术语，并直接在Isabelle中进行推理，使用Isabelle的用户CANONICAL混合LF是一个系统，使用混合方法的适应性，以不同的，able binding为Canonical LF风格的依赖类型的λ演算提供了HOAS接口。定理和元定理是• 在签名中定义，其中HOAS接口使用户能够将LF签名输入为具有命名绑定变量的Isabelle函数（然后将其转换为de Bruijn形式），以及• 使用4.2节中描述的逻辑M2[16]的证明规则证明正确。由于C ANONICAL H YBRID LF实现了规范LF，它允许使用判断作为类型的方法来证明定理[10]。 任何特定判断成立的证明被指定为给出一个LF项，该LF项存在于代表以下类型的类型中：对判决不满。 C型混合 LF与战术定理是一致的证明和原则的（共）归纳法以同样的方式，混合。虽然不在本文中，我们还导出了显式归纳原理。回想一下定义3.1中的五个句法类别。CANONICAL HYBRID LF基于五个相互归纳定义的数据类型kind，ctype，atype，cterm和aterm。这些相互定义的数据类型产生了一个整体的核心数据类型，其中包含与定义3.1中的术语相对应的术语，就像expr是混合体核心的核心数据类型一样。新的核心数据类型是由VAR和BND构造函数构建的，因此，最终，在机器实现中，变量绑定再次归结为de Bruijn的无名术语。但是，用户可以仍然可以使用带有命名绑定变量HOAS样式接口。R.L. Crole，A.理论计算机科学电子笔记323（2016）125131定义3.2[CoreCANONICALHYBRID LF数据类型]datatype（'a，'b）kind = TYPE| KPI“（'a，'b）ctype”“（'a，'b）kind”和（'a，'b）ctype = ATYPE“（'a，'b）atype”| PI“（'a，'b ）ctype”“ （'a，'b ）ctype”和（'a，'b ）atype = FCON 'b| FAPP“（'a，'b）atype”“（'a，'b）cterm”和| ABS“（'a，'b）ctype”“（'a，'b）cterm”和（'a，'b）aterm = VAR nat|BND nat|科纳| APP“（'a，'b）aterm”“（'a，'b）cterm”注意，有两个类型参数Ja，Jb：一个参数用于指定对象常量，另一个用于指定对象逻辑的类型常量（回想一下，原始混合体中类似的Core Datatypeexpr3.3C非正则混合 LF中的抽象与HYBRID类似，CANONICALHYBRID LF使用抽象概念，并具有确定某些术语是否有效抽象的函数谓词。然而，有两个主要的分歧。 首先，我们现在有了类型抽象和术语抽象。第二，CANONICAL HYBRID LF将抽象的一般概念从一元抽象扩展到k元抽象。直观地说，这些都是Isabelle函数，它绑定了k个变量，是语法项，没有悬挂索引。CANONICAL HYBRID LF有四个函数族，用于确定函数是否表示有效的术语抽象或类型抽象。通过函数的“家族”，我们指的是函数集合，每个函数除了表示输入的预期arity（例如12元抽象）的数字suprix（例如12）之外具有相同的名称。函数的前缀表示该函数作用于哪个语法范畴这些功能变量的生产编号高达12是一个务实的选择，基于理论处理时间和用户功能可用性之间的权衡。每增加一个函数，CANONICAL HYBRID LFtheory file in Isabelle.另一方面，我们要求在我们的例子中，ctype bind的变体（见3.4节）编号高达11，所以在实践中，制作多达12个变量的版本似乎是一个合理的步骤。这些函数类似于原始混合体中的abstr（参见第4页）。在这四个家族包括：a ctype abstr到ctype abst12，mcterm abstr到cterm abst12，p atype abstr到atype abst12，raterm abstr到aterm abst12。132R.L. Crole，A.理论计算机科学电子笔记323（2016）125例如，cterm abstr确定具有一个绑定变量的Isabelle函数是否是返回规范项的有效一元抽象，而cterm abstract 12确定具有12个绑定变量的函数是否是返回规范项的有效抽象。其他三个函数家族对表示规范类型、原子类型和最后原子术语的抽象执行相同的任务。在实践中，最多可以有12个变量的变体;可以处理的变量数量没有限制，因此我们可以定义一个abstr函数，允许分析具有更多绑定变量的函数。我们给出一个定义的例子，cterm abstr。定义3.3cterm abstri（λx. ATERMx）=真cterm abstri（λx. ATERM（CONa））=Truecterm abstri（λx. ATERM（BNDn））=（n< i）cterm abstri（λx. ATERM（VARn））=真ctermabstr i（λx. ATERM（（fx）$$O（gx）=atermabstrifatermabstrigcterm abstri（λx. ABS（t x）（fx））= ctype abstritctermabstr（i + 1）f<$cterm ordinaryf=ctermabstri f=False请注意，cterm ordinary是用来防范外来术语的。3.4C型杂化 LF中到de Bruijn的转化回想一下第2节中的lambda和lbind函数。这些函数实现了将命名为Isabelle bindersv的HOAS表达式自动转换为de Bruijn形式。目前的文件的一个关键贡献是表明，高阶模式匹配技术用于实现这些功能的混合顺利转移到一个类似的实现规范LF，从而产生的CANONICAL混合 LF系统。转换CANONICAL 混合型LF 从HOAS表达式到德布鲁因项由函数一个ctype绑定到ctype绑定12，一个cterm绑定到cterm绑定12，p atype bindtoatype bind 12，r aterm bindtoaterm bind12。为了创建这些函数，我们定义了函数家族ctype bind前 一个unprimed函数类似于lambda，而primed函数类似于lbind。 以下是cterm bind的定义：R.L. Crole，A.理论计算机科学电子笔记323（2016）125133定义3.4ctermbind ' i（λx. ATERM x）= Some（ATERM（BND i））ctermbind ' i（λx. （ATERM（BND k）= Some（ATERM（BND k））cterm bind ' i（λx. （ATERM（VAR n）= Some（ATERM（VAR n））cterm bind' i（λx. ATERM（CONa））=Some（ATERM（CONa））cterm bind' i（λx.ATERM（APP（F x）（G x）=（情况（aterm bindATERM（APP atm ctm）|无（无）| None ⇒None)cterm bind' i（λx. ABS（ty x）（F x））=（case（ctype bind的一些m一些（ABS t m）|无（无）| None ⇒None)<$ctermordinaryexpr=无cterm bindcterm bind'的自然数参数i请注意，cterm bind这与最初的混合体相反，它使用核心expr数据类型的ERR元素来指示错误发生（参见第3页）：编码和错误处理现在更加流畅。cterm bind（lambda的类似物）的定义如下：定义3.5cterm bindte如果cterm abstr0e则（case（cterm bind' 0 e）ofSomeeJSome（ABSt eJ）|无无）其他无cterm bind将规范类型t（绑定变量的类型）和要转换为de Bruijn形式的函数e作为参数。这种转换是通过用初始参数调用e上的cterm bind0表示递归的绑定器数量。aterm bind函数的定义类似，其中aterm bindctype bind的定义是这样的：定义3.6ctype bindte如果ctype abstr0e则（case（ctype bind' 0 e）ofSomeeJSome（PIt eJ）|无无）其他无同样，t是一个规范类型，e是要转换为de Bruijn形式的函数。在ctype bind的变体中，134R.L. Crole，A.理论计算机科学电子笔记323（2016）125α一个以上，绑定器类型有一个以上的参数，一个以上的封闭绑定器被添加到转换的项，并且绑定器类型的参数类型是具有增加数量的绑定变量的函数。例如，ctypebind3定义如下：定义3.7ctype bind3t1t 2t 3eifctype abstract 30ectype abstr 0t 2ctypeabstract 20t3then（case（ctype bind ' 0 t 2）of Some t2 j|无（无）| 无无）其他无|None ⇒ None) else None注意，三个PI绑定被添加到转换后的项eJ 的 开 始，即t 1的类型是（'a，'b）ctype，t 2的类型是（j a，j b）aterm →（j a，j b）ctype，并且t 3的类型是（ja，j b）aterm →（j a，j b）aterm →（j a，j b）ctype。后两个绑定器的类型t2和t3作为函数给出，因为在前面的绑定器中绑定的变量可能出现在其中。3.5C型杂合LF的分型、分类和替换回想一下图1中规范LF的类型和分类规则。在CANONICAL HYBRID LF中，这些规则由许多相互定义的函数实现类型由validkind函数确定为有效，而类型由validtype函 数 确 定 为 有 效 。 类 型 通 过 atom kindof 函 数 （ 实 现 规 则 CON AT KIND 和 APPATKIND）分配给原子类型。类型分别由函数atom typeof和canon typeof分配给原子项和规范项（实现规则VAR ATTY、CON ATTY、APP ATTY和ABS CAN TY）。替换是通过与定义3.1的句法范畴相对应的函数来完成的。由于空间原因，我们省略了细节;例如，有一个函数ctype subst fv，它用规范项替换规范类型中的自由变量，实现了图1中的[M/x]aA。为了进一步解释这些功能，我们首先做一些一般性的评论。类型化函数和替换函数的前五个参数是相同的;见图2。由于Isabelle要求所有函数都终止，我们引入一个数值递归深度参数来确保这一点。请注意，所有函数有一个当参数为零时的情况，它只是返回None来指示失败。当这个参数为非零时，所有的情况都在Suc q上对某个q进行模式匹配，将它们与零情况区分开来，函数体内的递归调用都将q作为第一个参数，确保它随着每次递归调用而减少。第二个参数是上下文，而第三个和第四个是签名，分为对象常量和类型常量。fixed参数是绑定环境，一个包含绑定器的规范类型的Isabelle列表，它允许我们输入绑定变量。R.L. Crole，A.理论计算机科学电子笔记323（2016）125135函数名递归参数对象上下文签名类型签名结合环境功能 0 ctx签名测试 签署kbnd图二. 类型化和替换函数在canon typeof和atom typeof中，第六个参数是确定类型的规范项或原子项，而替换函数中的第六个参数是我们替换自由变量的规范项。替换函数中的第七个参数是一个自然数，即要替换的变量的个数第八个是我们要代入的术语。我们通过给出这些函数的一些代码示例来完成本节atomkindof函数计算原子类型的种类定义3.8atom kindof0ctx sig t sig k bnd a =无atom kindof（q+ 1）ctx sig t sig k bnd（FCONa）=（casesig k lookupsig k aofSomek（ifkind level0kthenSomekelseNone）| None ⇒None)atom kindof（q+ 1）ctx sig t sig k bnd（FAPPp m）=（caseatom kindofq ctx sig t sig k bnd pofSome（KPIa k）类型（案例规范类型的q ctx sigt sig k bnd mofSomeakindsubst bvq ctx sig t sig k bnd m0 0k| 无（无）|None ⇒None)请注意，单函数原子类提供了图1中两个规则的实现。 第二个定义函数方程（是，FCONa）的一个对应于LF kinding规则CONATKIND，第三个定义函数方程（对于FAPPp m）对应于LF规则APPATKIND。 请记住，第一个参数用于确保原子kindof函数的终止，基本情况为0表示无法确定种类。在常数FCONa的情况下，进行查找以查看签名中是否声明了a，并且如果是，则进行检查以检查种类是否为级别0，即“适当种类”。在应用程序FAPPp m的情况下，例如，在atom kindof成功的情况下，提取p的种类和m的类型，然后对m到p的类中就完成了类的计算canon typeof函数计算正则项的类型：136R.L. Crole，A.理论计算机科学电子笔记323（2016）125定义3.9canon typeof0ctx sig t sig k bnd m =无canon typeof（q+1）ctx sigtsig k bnd（ATERMr）=原子类型q ctx sig t sig k bnd rcanon typeof（q+ 1）ctx sig t sig k bnd（ABSaJm）=（casecanon typeofq ctx sig t sig k（aJ#bnd）mofSomea（ifctype level0 aJthenSome（PIaJa）elseNone）|无（无）与atom kindof类似，当递归深度限制的第一个参数为0时，canon typeof的基本情况返回None当最后一个参数是封装在ATERM封装器中的原子类型时，第二个等式简单地调用原子类型函数第三个等式（对于ABSaJm）对应于LF类型规则ABSCANTY，并确定抽象的主体m的类型（用绑定器aJ的类型更新绑定器），并返回None（如果没有类型可以为m计算或aJ不是正确的类型）或Some_type，其中计算的类型m作为其主体。atomtypeof函数计算原子项的类型定义3.10原子类型0ctx sig t sig k bnd r =无原子类型（q+1）ctx sigtsigkbnd（VARv）=（casectx lookupctx vofSomet（ifctype level0tthenSometelseNone）|（q+1）ctxsigtsigkbnd（CONc）=（casesig t lookupsig t cofSomet）（ifctypelevel0tthenSometelseNone）|无（无）原子类型（q+ 1）ctx sig t sig k bnd（APPr m）=（caseatom typeofq ctx sig t sig k bnd rof Some（PIaJa））（casecanon typeofq ctx sig t sig k bnd mof SomeaJ）ctype subst bvq ctx sig t sig k bnd m0 0 a|无（无）|无（无）第二个方程（对于VARv）对应于键入规则VARATTY，第四个方程（对于CONc）对应于CONATTY，第五个方程（对于APPr m）对应于APPATTY。4案例研究和证据系统4.1编码简单类型的Lambda演算和量化命题逻辑我们为简单类型的lambda演算定义了一个CANONICAL HYBRID LF签名，基于BMF文档[18]中的一个例子。定义3.2R.L. Crole，A.理论计算机科学电子笔记323（2016）125137我们指定类型和对象常量：数据类型tcons= tp|TM|类型变量|pres|Val|步骤o cons=单位|箭头|Singleton|app|林|瓦兰...例如，step是标准的按值调用单步操作归约;val是值的谓词，即归约的最终结果;app构建应用程序表达式签名分为两部分。sig kind指定类型常数的种类。sig type选项指定对象常量的类型，定义为（ocons×选项）列表这意味着用户必须删除该类型的选项元素，但幸运的是，这很容易做到。例如，常量vallam用于断言任何表达式都是值，并且具有类型4Some，其中是PI（tm）（λ E. PItp（λT. val$$F（lam$$OT$$OE）：（o cons，tcons）ctypeλ是Isabelle函数抽象。这里我们利用HOAS，E的（高阶）类型是tmtm;不需要格式良好的谓词（如在混合体中），因为类型系统执行此角色。 是sugar，用于调用转换函数ctype bind2ctypebind2 （ tm ） （ λE.tp ） （ λE.λT 。 val$$F（lam$$OT$$OE）），这在C中计算为（一阶）表达式PI（tm）（PItp（val$$F（（lam$$O（BND0））$$O（BND1）在这个例子中定义的元定理是在求值过程中的类型保持。在M2元逻辑中，我们将得到由pres类型表示的类型保持元定理成立的一个证明，我们将在下一节中简要描述。对于第二个案例研究，以及与[1]中描述的原始混合系统的比较，我们回到量化命题逻辑（QPL）的例子。并给出了混合体和非混合体的定义语法HYBRID LF. QPL拥有Q：：= Vi|欧Q|QQJ|QQJ|QQJ|I.Q.|I.Q.我们可以归纳地定义否定范式，一个将QPL表达式转换为否定范式的函数（实现为确定性关系），4注意，为了可读性，我们省略了定义3.2实例中的所有构造函数。（o cons，tcons）ctype138R.L. Crole，A.理论计算机科学电子笔记323（2016）125证明一个正确性定理，断言转换函数输出否定范式;参见[1]。混合体中的QPL下面是代码的快照（请回忆第3页上的混合核心数据类型Ja expr）数据类型cons = cATOM|cAND | CIMP |cFORALL|......这是什么？ |cZERO |cSUCC inductive nnf：：“cons expr -> cons expr-> bool”...nnf_forall：“[[摘要f;摘要g;全部;全部 isNat n--> nnf（f（cATOM $$n））（g（cATOM $$n））]]=>nnf（cFORALL $$（LAM x. f x））（cFORALL $$（LAM x. gx））”...引理is_nnf_form：“is_nnf a ===> isForm a”...引理nnf_correct：“nnf a b => is_nnf b”注意，在定义nnf时，nnf for all的量化规则是用HOAS编码的;我们声明抽象f，g（和来自H YBRID包的LAM），然后写（例如）cFORALL $$（LAMx。fx）。然而，“无类型”的核心数据类型导致了谓词isNat的额外负担，该谓词isNat挑选出对应于自然数的表达式，而谓词isForm挑选出对应于QPL公式的表达式，这些表达式在证明过程中使用。C非正则杂化 LF中的QPL下面是代码的快照，我们写\v来表示Isabelle函数抽象（回忆一下第7页上的CANONICAL HYBRID LFCore DatatypeJa expr）数据类型t_cons = nat |NNF|形式|是_nnf |nnf_correct数据类型o_cons = cZERO |cSUCC |cATOM|......你好。|cFORALL |cEXISTS|是_nnf_* |nnf_* |nnf_correct_*其中* 是ATOM，FORALL，NOT_FORALL，EXISTS，.。等...(nnf，（KPI（ATYPE（FCON form））（KPI（ATYPE（FCONform））TYPE），...(nnf_FORALL，（ctype_bind4（（nat））（\n. PI（（form））（（form））（\n.\ X. （PIR.L. Crole，A.理论计算机科学电子笔记323（2016）125139（（form））（（form）（\n.\ x. y. （nnf$$T（（x$$O（cATOM $$On）$$T（y $$O（cATOM $$On）（\n.\ x. y. z. （nnf $$T（（cFORALL $$O x））$$T（（cFORALL $$O y）140R.L. Crole，A.理论计算机科学电子笔记323（2016）1252注意，有些类型常量被用来命名要证明的判断。form是公式的类型;nnf将QPL公式映射到否定范式中的公式。 对应于nnf的混合归纳定义，有nnf forall这样的规则，有nnf FORALL这样的对象常数。比较两种编码QPL的C规范混合LF定义避免了对混合中所需的谓词（如isNat）的需要，这是一个明显的改进。然 而 ，指定（即实现）QPL的C非标准混合LF签名比Isabelle HOL数据类型、关系和引理定义长得多。构成所述溷合体 实施QPL。组成本发明的术语CANONICAL HYBRID LF签名也比HYBRID定义。4.2一种C型混合LF逻辑一个典型的混合LF利用Schürmann和Pfenning[16]的M2元逻辑证明了签名中的定理是有效的.选择M2的一个主要原因是对Pfenning及其合著者的工作的普遍熟悉，加上其相对简单，以及它足够强大以证明一系列元定理的事实事实上，M2是为构造LF规范上的证明而设计的（我们也可以考虑更强大的逻辑，但M2似乎是明智的第一选择）。M2是一个带有证明项的一阶微积分，其中一个完全导子的证明项形成了一个从泛量化变量到存在量化变量的全函数。M2中的公式具有以下形式A1. Ak. xk+1：Ak+1. xm：Am. 不其中A1到Am是有效的LF类型，x1. xk和xk+1... xm是有效的上下文，量化器的范围在封闭的LF对象上，从公式定义的签名开始，T符号代表真理。这样的公式对应于TMF所采用的模式检查方法中的总体断言，其中元定理的变量被指定为输入和输出，并且系
我的内容管理
展开
