《理论计算机科学电子札记》：上下文理论中开发非平凡的（Meta）理论的案例研究的Coq证明助理的正式发展

《理论计算机科学电子札记》58卷第1期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html22页在上下文理论中发展（Meta）-演算理论Marino Miculan2大学数学与信息学系di Udine，意大利摘要我们提出了一个案例研究的非平凡的（Meta）理论的上下文理论使用Coq证明助理的正式发展。在HOAS中提出的系统推理的上下文理论的基础方法是基于公理化的句法观点我们认为这种方法的主要优点之一是它需要非常低的逻辑开销。我们关注的对象系统是懒惰的，按名称调用演算（cbn），包括无类型和简单类型。我们将看到，在上下文理论中，cbn理论的正式的、完全详细的发展引入了一个小的、可持续的开销，相对于论文中的证明此外，这将允许与在高阶抽象语法的元理论推理的其他方法中开发的类似案例研究进行关键词：高阶抽象语法、归纳法、逻辑框架。介绍近年来，人们对开发具有-转换特征的语言的定义和推理系统越来越感兴趣一个有前途的路线的方法集中在高阶抽象矩阵（HOAS）[13，24]。这种方法的要旨是将处理绑定器的负担委托给类型理论元语言然而，这种方法具有一些缺点。首先，被等同于元语言变量，对象级变量不能被归纳地定义而不引入外来术语[7，20]。类似的困难也出现在语境中，语境被呈现为功能性术语。因此，通过归纳进行推理和通过对象级项的递归进行定义是有问题的。基于不同的技术，如函子范畴、ZF的置换模型等，已经提出了各种方法来克服这些[9、10、14、11、19]。1 工作部分由意大利MURST项目tosca和E-C-W-G型提供支持.2 电子邮件地址：miculan@dimi.uniud.itc 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。2在[15]中，基于公理语法的观点，提出了HOAS中系统推理的另一个逻辑框架。这个系统源于最初在[16]中使用的技术，用于在Coq[17]中正式导出-演算的强后期双相似性的元理论 这一框架由一个简单的类型理论la Church扩展了一组公理叫做上下文理论，递归算子和归纳原则。根据我们的经验，这个框架是相当有表现力的。高阶逻辑允许对许多关系（可能是功能性的）进行非断言的定义，递归和归纳原则允许对上下文的许多重要功能和属性进行定义，最值得注意的是上下文理论中的公理允许在HOAS中顺利处理图式。事实上，我们认为上下文理论的公理化方法的主要优点之一是它需要非常低的数学和逻辑开销。当然也有一些交易。任何公理化方法的主要理论问题之一是公理的一致性。事实上，语境理论的合理性是可以证明的。我们请读者参考[4]，其中使用沿着[14]的路线的函子范畴模型，给出了上下文理论的一致性的充分证明。然而，从实际的角度来看，这一方法的适用性必须通过几个案例研究来检验这些是特别有用的，讨论出现在发展中的语境理论，解决可能的解决方案，并提出未来发展的方向的实际证明的问题这正是本文的目的，我们在Coq证明助手中的上下文理论中开发了一个非平凡的（Meta）懒惰，按名称调用演算（cbn）的理论，无论是无类型的还是简单类型的我们选择cbn作为本案例研究的对象有几个原因。首先，这是一个众所周知的逻辑，以至于大多数关于微积分的著作都很快地浏览了标准定义和基本证明，把许多细节扫到地毯下面我们将看到，在上下文理论中，cbn理论的正式的、完全详细的发展引入了一个小的、可持续的开销，相对于论文中的证明此外，cbn还具有一些特点（如变量的术语替换，类型系统，。. . ），这在某种程度上是对微积分的补充，微积分是语境理论中另一个大型案例研究的对象[16]。最后，微积分的一些变体一直被作为文献中HOAS许多方法的传统基准/应用示例;参见[13，2，7，19，14，11，12]等。事实证明，语境理论在处理cbn的元理论方面非常成功。语法、语义和类型系统的编码是直接的，我们仍然把-转换委托给了满足层。 只有替换的编码不是直接的，因为我们需要把它当作一种关系。然而，这将允许我们陈述和证明一些基本结果（即，取代基），通常是3在微积分的非正式著作中被视为理所当然。此外，这些证明投下了一些光的限制，并建议可能的解决方案，在科克的理论的背景。Coq代码可在www.example.com上获得http://www.dimi.uniud.it/~miculan/HOAS/。概要。在第1节中，我们简要回顾（即在大多数作品中所做的）对象系统cbn。在第2节中，我们简要介绍了类型CIC理论及其实现 语法的HOAS编码和cbn的语义，以及使用上下文理论的元理论的形式化发展，在第3节中描述。在开发过程中出现的实际问题的证明进行了讨论，并在可能的情况下，提出了解决方案在第4节中，我们考虑对象系统的两个扩展：应用互模拟和观测等价，以及cbn的一个简单类型系统。与相关工作的比较和结论分别在第5、61对象系统CBN在这一节中，我们故意给出了一个懒惰的按名称调用演算cbn的简短（有点草率）定义，因为它通常在大多数论文中给出。这将使我们在下面的部分中得到启发，尽管需要高级别的细节，但理论的正式表示如何不引入大量的开销。我们假设读者熟悉微积分的基本概念;对于微积分理论的介绍和全面发展，见[3]。集合条款的cbn由以下语法定义：M; N：：= x j（MN）j x：M其中，x; y; z;：range在一组无限的变量上。术语被视为等同术语.我们用M[N=x]表示N对M中x的避免捕获的替换。上下文，即具有孔的项，由M（）表示。如果一个术语不是一个应用程序，那么它被称为一个值。“自由变量”（FV）的概念通常被定义。对于X是一组变量，我们定义了X，fM 2j FV（M）XG.通过0我们表示;。我们考虑两个懒惰的操作语义。 约简（或小步语义）是最小的关系M！ 由以下规则定义米！ M0（x：M）N！ M[N=x]（MN）！（M 0N）我们表示by！ 的退出和过渡关闭！.求值（或大步语义）是由以下规则定义的最小关系M + N：x：M + x：MM+x：M 0M 0[N=x]+VM N + V42归纳结构归纳构式演算是构式演算（CC）的推广，CC可以定义为Barendregt立方体的PTS C，有Prop和Set两种类型在命题作为类型，证明作为项的范式下，直觉高阶逻辑的命题与排序Prop类型如果A具有Prop类型，那么它表示一个逻辑命题; A被项M占据的事实表示A成立的事实。每个项M存在于A中，表示A的一个证明。另一方面，排序集应该是数据集的类型，如自然，列表，树，布尔等。这些类型不同于那些居住在Prop的建设性内容。因此，CC和许多类似的类型理论一样，可以卓有成效地用作一般逻辑规范语言，即逻辑框架（LF）[13，22，23]。在LF中，我们可以忠实地和统一地表示逻辑系统中推理过程的所有相关概念（语法类别、术语、变量、上下文、断言、公理模式、规则模式、实例化、策略等）。归纳结构演算（CIC）（在Coq系统[17]中实现）用一些特殊的常数扩展了CC，这些常数表示归纳类型的定义，引入和消除。例如，以下自然数的定义（用Gallina，Coq的规范语言编写）感应nat：Set：=O：nat |S：nat -> nat允许通过\case analysis”定义新的术语，如以下函数：定义pred：= [n：nat]Casesn ofO => O |（S u）=> u end.其中[n：nat]是抽象n：nat的Gallina表示法。使用这些消除模式，Coq自动陈述并证明了每个归纳定义类型的归纳原理。例如，上面的定义产生了皮亚诺归纳原理“免费”：nat_ind：（P：nat->Prop）（P O）->((n：nat）（Pn）->（P（Sn）->（n：nat）（Pn）其中（n：nat）是相关乘积Qn：nat的表示法。这一特征在逻辑联结词的定义中得到了广泛的应用：我们只需要指定引入规则，我们可以证明消除规则，系统自动提供给我们的排除原则。然而，在CIC中允许任何归纳定义都会产生非规范化项，从而使系统一致性的标准证明无效。因此，归纳定义服从肯定性条件，它（粗略地）要求我们所定义的类型在任何构造函数的任何参数的类型中不出现在否定位置。这个条件保证了系统的可靠性，但它也排除了许多可靠的归纳法5名称。例如，高阶抽象语法感应L：设置：= lam：（L->L）-> L|app：L -> L -> L.不是良构的，因为在lam的参数的类型L->L中，L的出现是负数。使用高阶抽象语法与归纳类型相结合所产生的另一个问题是外来术语。这些词是不对应于任何宾语的词，尽管它们的类型对应于某个句法范畴。当类型具有比归纳类型更高阶的构造函数时，会生成外来项。一个简单的例子是下面的一阶逻辑片段：电感i：设置：=零：i|一，感应o：Set：= ff：o|等式：i->i->o|对于所有：（i->o）->o。定义weird： o：=（forall [x：i]（Cases x ofzero=>ff| 一=>（eq零零）结束））。术语weird不对应于一阶逻辑的任何命题：不存在公式8x使得f0=xg和f1=xg在语法上等于\“和\0 = 0”。外来术语在建立形式化的忠实性方面是有问题的;通常，它们必须通过辅助的“有效性”判断来排除[7，27]。另一种方法，将在3.1节中使用，是让高阶构造函数覆盖那些没有被定义为归纳的类型，这样就没有如上所述的情况CIC的一个常见实现是Coq，它是由INRIA和其他机构开发的交互式证明助手。关于完整的描述，我们参考[17]。Coq是一个编辑器，用于交互式地搜索一个类型的居民，以自顶向下的方式，通过逐步应用策略，如果需要的话可以回溯，并用于验证类型判断的正确性。一个证明搜索开始输入引理ident：goal.其中goal是表示要证明的命题的类型。 在这一点上，Coq等待来自用户的命令，以便构建驻留目标的证明项（即，证明）。为此，Coq提供了一套丰富的策略，例如，假设的引入和应用，规则和先前证明的引理的应用，归纳对象的消除，（共）归纳假设的反转等等。这些策略允许用户像非正式地那样继续他的证明搜索。在每一步，类型检查算法确保证明的可靠性。当证明项完成时，可以保存（通过命令Qed）以备将来使用。63形式化和推理CIC中的cbn3.1cbn语法编码cbn的语法的HOAS表示如下：Parameter Var：Set。感应tm： Set：= var： Var -> tm|应用程序：tm -> tm -> tm| lam：（Var -> tm）-> tm。强制var： Var >-> tm。将var声明为强制转换允许我们将类型Var中的项隐式注入到tm中，因此在下文中，可以从项中省略此构造函数。注3.1我们不把neVar定义为归纳集。事实上，cbn的语法并不要求这样做，因此没有理由引入不必要的假设，即，归纳和递归原理。实际上，这些不受欢迎的原则并不是无害的，因为它们可以被用来定义外来术语;因此，将Var作为归纳法是完全错误的。注3.2注意lam是一个高阶构造函数，也就是说它接受一个函数项作为参数。特别是，类型为Var->tm的项恰好表示-演算的捕获避免上下文。这种技术允许从元语言中继承术语的等价性，并且仍然具有对术语的归纳定义例如，x：（xx）和y：（yy）由（lam [x：Var]（app（var x）（var x）和（lam[y：Var]（app（vary）（vary），它们是相同的术语上转换。同时，我们可以通过对术语语法的一阶递归或案例分析来定义新的函数，如下所示定义isvalue：= [M：tm]CasesMof(varx）=>False|（lam t）=> True| （应用程序t1 t2）=>错误端这种编码的适当性是[15，定理1]的结果。对于X=fx1; ：;xn g一组变量，让我们定义一个X，fx1：Var;：：; xn： Varg[fdij：~（ Xi= xj）j1ijngtmX，fMjX`M：tm;M的长正规形式g：<命题3.3对于所有X nite变量集，在X和tm X之间存在双射X。此外，这 个 双 射 是 合 成 的 ， 在 这 个 意 义 上 ， 如 果 M2X;x 和 N2X ， 则 X（M[N=x]）=X;x（M）[X（N）=（varx）]：作为推论，（捕获避免）上下文M（）2X自然地被编码为[z：Var] X;z（M（z）），其中新变量z充当孔的“占位符”。事实上，像命题3.3那样的双射可以在上下文和Var->tm类型的术语之间建立。73.2cbn的语境理论通常，对象系统的HOAS编码对于处理系统的元理论（即证明对象系统本身的属性）是不够的。由于我们的目的是证明cbn的几个结果，我们需要引入相应的上下文理论。鉴于句法的特征，语境理论由两部分组成。第一部分包含“出现”谓词的定义。 这些定义直接来自语言的签名，遵循[16，15]中的模式。归 纳 符 号 [x ： Var] ： tm -> Prop ： =notin_var ： （ y ： Var ） ~x=y->（notin x y）|notin_app：（M，N：tm）（notin x M）->（notin x N）->（notin x（appMN））| notin_lam：（M：Var->tm）（（y：Var）~x=y->（notin x（My）））->（记为x（lam M））。感应isin[x：Var]： tm -> Prop：=isin_var：（isin x 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（M y）->（isin x（lam M））。关于变量名（变量），我们唯一需要知道的是Var上的等式是可判定的。然而，我们不需要一个完整的经典逻辑：在出现检查谓词上有一个经典的行为是足够的。公理LEM_OC：（M：tm）（x：Var）（isin x M）\/（notin x M）. 这意味着（eq Var）的可判定性。语境理论的第二部分由一组公理图式组成，它们在理论层面上反映了变量的“语境”和“出现”这一直观概念的一些基本性质。其非正式含义如下：变量的不饱和性：没有一项可以包含所有变量;即，总有一个变量在给定项中不是自由出现的上下文的可拓性：如果两个上下文在一个新变量上相等，则它们相等;也就是说，如果M（x）= N（x）且x 62 M（）;N（），则M = N。更正式地说，这些是我们需要的语境理论的公理公理unsat：（M：tm）（Ex [x：Var]（notin x M））。公理ext_tm：（M，N：Var->tm）（x：Var）（ notin x （ lam M ） ） -> （ notin x （ lam8N））->（Mx）=（Nx）-> M=N。公理ext_tm1：（M，N：Var->Var->tm）（x：Var）9（notin x（lam [z：Var]（lam（Mz）->（记为x（lam [z：Var]（lam（M z）->（M x）=（N x）-> M=N。下面是语境理论和关于tm的归纳原理的直接结果。引理不同：（x：Var）（Ex [y：Var]~x=y）。引理isin_notin_abraham：（x：Var）（M：tm）（isin x M）->（notin xM）->False.注3.4在[15]中还提出了另一个公理模式，称为-扩展.非正式地，-exp表示给定一个项M和一个变量x，存在一个上下文N（）使得N（x）= M并且x不出现在N（）中。这已经被多次用于元理论的发展，- 微积分[16]。 另一方面，它在目前在cbn上工作。一个可能的动机是，这里我们允许高阶归纳，而在[16]中，我们必须从plain上的归纳中恢复它，一阶项我们在这项工作中没有使用的-exp的另一个有用的应用是在HOAS中表示变量捕获上下文一般来说，这是困难的，因为绑定变量不能从抽象的外部访问，甚至不能访问它们的名字。 在上下文理论中，捕获x的上下文C[]可以表示为（var->tm）->tm类型的项，并且实例化需要插入项的-扩展。例如，x：（[] x）表示为C' = [N：（var->tm）]（lam[x：Var]（app（Nx）（var x）。 考虑具有必须捕获的自由变量x的项M：令M 0（）为通过对x的y-展开获得的内容（即， 假设M0（x）=M且x在M0中不自由）。然后，变量捕获实例化C[M]被呈现为（C“M”）。备注3.5如第2节所述，Coq和类似系统提供对感应类型的支持。然而，这并不适用于高阶类型：即使A和/或B是归纳的，也没有关于A->B的归纳原理。这是因为A->B（通常是一个函数空间）的含义不是初始代数。因此，大多数证明编辑器没有给出归纳原则、案例分析、倒置谓词和类似的工具来推理类型为Var->tm的术语，即，contexts.然而，可以证明Var->.. ->形式的类型Var->tm确实有递归和归纳原则[14，4，15]。因此，除了上面的语境论的简单公理，我们可以根据需要安全地假设高阶归纳和递归原理，比如下面的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）（Nx）->10((M：Var->Var->tm）11((y：Var）（P [x：Var]（M x y）->（P [x：Var]（lam（Mx）->（M：Var->tm）（PM）。（注意有两个基本情况）。在下文中，我们还可以介绍这些原则中的其他原则，3.3将替代对变量使用特定类型（一种\weak HOAS编码）的缺点相反，我们需要手工定义它，作为上下文和术语之间的参数关系：感应subst [N：tm]：（Var->tm）-> tm -> Prop：=subst_var：（substN var N）| subst_void：（y：Var）（substN[_：Var]y y）| subst_app：（M1，M2：Var->tm）（M1 '，M2'：tm）（substN M1 M1'）->（substN M2 M2'）->（substN [y：Var]（app（M1 y）（M2y））（appM1'M2'））| subst_lam ：（M：Var->Var->tm）（M '：Var->tm）((z：Var）（substN [y：Var]（M yz）（M'z）->（substN [y：Var]（lam（M y））（lam M'））。因此，项M0在语法上等于置换M（x）[N=x]i（substNMM '）成立。更正式地说：命题3.6设X是一个变量的集合，x是一个不在X中的变量。设N;M02 X和M2 X]fxg. 然后又道：M[N=x]=M 0（）X`：（substX（N）[x：Var]X]fxg（M）X（M 0））捕获避免替换被自然地定义为一个函数，但实际上它的定义很少被详细地给出|第一节也不例外实际上，通常意图的定义不是先验决定的，因为它需要上下文的约束变量的任意转换，以避免在替代项中捕获自由变量。更复杂的语言（例如，动态逻辑，Hoare逻辑[20]）可能需要非标准的替换，包括人为的转换概念，而不是简单的转换。事实上，把CIC中的替换表示为一个关系，会引起这样的可能性，即它可能不是全的，也就是说，对于某个N; M，不存在M0使得M0 = M[N=x]。事实上，这样的定义确实给出了一个函数（即，确定性和总体）关系是一个属性，我们将使用上下文理论明确证明替代决定论我们要证明的性质如下：参数N：tm。12引理subst_is_det：（M：Var->tm）（M1：tm）（substN M M1）->（M2：tm）（substN M M2）->（M1 = M2）。我们给出了这个性质的两个证明。第一步是对（substN MM1）的导数进行归纳。这就产生了四种情况：N： tmM：var->tmM2：tmH：（subst N Var M2）==次级目标2是：（y）=M2子目标3 为：（应用程序M1'M2'）=M0子目标4是：（lam M'）=M2每一个都应该通过颠倒假设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行，其中大部分是关于消除荒谬的情况。替代决定论，再次一个更短的证明可以通过证明一个合适的高阶反演引理来获得。在Coq中，反演引理通过反演策略自动合成并从递归原理中证明，使用最初由Murthy实现的算法，随后由Cornes和Terrasse [6]详细说明。然而，该算法未能给出正确的反演谓词时，我们必须区分，是高阶的，因为通常的归纳类型理论不承认一个高阶类型的归纳。然而，我们知道Var->tm形式的类型确实有递归原则[14，4，15]。因此，我们可以始终如一地引入这些原则（作为公理）来定义反演谓词所需的递归映射：参数subst_inv_fun：tm ->（Var->tm）-> tm -> Prop.13公理subst_inv_fun_var0：（N，M：tm）（subst_inv_funN var M）==（N=M）.公理subst_inv_fun_var1：14（y：Var）（B，N：tm）（subst_inv_funN[_：Var]yB）==（（vary）=B）.公理subst_inv_fun_app：（A1，A2：Var->tm）（B，N：tm）（subst_inv_funN [x：Var]（app（A1 x）（A2 x））B）==(EX B1|（EX B2）|（app B1 B2）=B/\（subst N A1 B1）/\（substN A2 B2）。公理subst_inv_fun_lam：（A：Var->Var->tm）（B，N：tm）（subst_inv_funN [x：Var]（lam（Ax）） B）==(EX A1|（lam A1）=B/I（y：Var）（subst N [x：Var]（A x y）（A1 y）。然后，“机械地”提出了高阶反演原理，并证明如下：引理subst_inv：（A：Var->tm）（B，N：tm）（subst N A B）->（subst_inv_fun N A B）. Intros; Inversion_clear H.重写subst_inv_fun_var0;自反性。重写subst_inv_fun_var1;自反性。重写subst_inv_fun_app;检查M1 ';检查M2';自动。重写subst_inv_fun_lam;编译器M '; Auto。Qed。利用这个反演引理，代换决定论的证明就容易得多|事实上，我们在语境的层面上“提升”了Coq在术语层面上提供的倒装策略的句法机制：引理 subst_is_det'：（M：Var->tm）（M1：tm）（substN M M1）->（M2：tm）（substN M M2）->（M1 = M2）。归纳1;介绍。Generalize （ subst_inv ？ ？ ？ H0 ） ; Rewrite subst_inv_fun_var0;Trivial.Generalize（subst_inv？？？H0）;Rewritesubst_inv_fun_var1; Trivial. Generalize （ subst_inv ？ ？ ？ H4 ） ;Rewrite subst_inv_fun_app; Intros.Inversion_clear H5; Inversion_clear H6; Inversion_clear H5; Inversion_clear H7。重写（H1？H5）; Rewrite（H3？H8）;假设。Generalize（subst_inv？？？H2）; Rewrite subst_inv_fun_lam; Intros.Inversion_clear H3; Inversion_clear H4; Inversion_clear H3。将x替换为M ';自动。以琳（unsat（app（lam M '）（lamx）。Intros; Inversion_clear H3.使用x 0; Auto应用ext_tm。Qed。正如人们所看到的，在这个证明中，我们也使用了上下文理论的公理（unsat和ext tm）。替代的总体性由于CIC的一些特殊性，总体性的证明是棘手的。我们要证明的引理15是引理subst_is_total：（M：Var->tm）（EX M'|（subst N M M '））。我们的目的是通过M上的高阶归纳法来证明这一点。这在lambda抽象的情况下失败了，如下所示16N： 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'intm）中的一个项。这种强类型的“消除”可能导致不一致，因此被类型理论CIC [5]排除我们采用的解决方案是将整个证明移动到集合领域，然后将结果提升到Prop。因此，我们引入了一个集合型的归纳原理|它可以被看作是一个具有依赖类型的递归：公理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（Mx）（Nx）->((M：Var->Var->tm）((y：Var）（P [x：Var]（M x y）->（P [x：Var]（lam（Mx）->（M：Var->tm）（PM）。然后，我们用高阶相关递归证明了Set中的全性：引理sit：（N：tm）（M：Var->tm）{M '：tm|（subst N M M '）}。Intros;模式M;应用tm_rec1; Intros;清除M。使用N分割;应用subst_var。Substs（var y）; Applysubst_void.（反转_清晰H;Inversion_clear H0）。Split with（app x x0）; Apply subst_app; Assumption.Pasts（lam [y：Var]（proj1_sig tm？（Hy）。应用subst_lam; Intros。应用proj2_sig。Qed。注意，在lambda的情况下，所需的项是通过消除（投影）假设H中的-类型来构建的，假设H实例化在局部绑定（因此是新鲜的）变量y上。那么，总体性定理就是从-type（sitM）中抽取逻辑部分：引理subst_is_total：（M：Var->tm）（Ex [M '：tm]（substN M M'））。介绍一下测试（proj1_sig？？（sitM））。应用proj2_sig。17Qed。18提取替代函数引理可以看作是替换函数的特殊化。我们可以通过提取-type（sitNM）的第一个组件来显式化它：引理subst_f：tm->（Var->tm）->tm.IntrosN M; Exact（proj1_sig？？（sitNM））。Qed。其中，添加了一点语法糖，采用了熟悉的形式[]，就像下面的\verication”和congruence属性：引理 subst_f_prop：（N：tm）（M：Var->tm）（subst N MM[N]）. 引理subst_f_var：（N：tm）（var[N]）=N。引理subst_f_void：（N：tm）（y：Var）（（[_：Var]y）[N]）=y。引理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]（Mxy））[N]））。替换的一个有趣的性质是复合：对于M; N; P项和x 6= 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]（（P x）[（Q x）]））[M]）=（[y：Var]（[x：Var]（P xy））[M]）[Q[M]]）。除了使用公理ext_tm和|联合国卫星|，这个性质的证明是通过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）（Nxy）->((M：Var->Var->Var->tm）((z：Var）（P [x，y：Var]（M x y z）->（P [x，y：Var]（lam（M xy）->（M：Var->Var->tm）（PM）。193.4形式化cbn的语义两种操作语义的表示都很简单。感应红色：tm -> tm ->Prop：=red_beta：（N：tm）（M：Var->tm）(red（app（lamM） N）（subst_fN M））| red_head：（M，N，M'：tm）（red M M '）->（red（app M N）（app M'N））。20感应trred： tm -> tm -> Prop：=| trred_ref : (M:tm)(trred M M)| trred_trs : (M,N:tm)(red M N)->(P:tm)(trred N P)->(trred M P）。归纳eval： tm -> tm -> Prop：=eval_var：（x：Var）（eval x x）| eval_lam：（M：Var->tm）（eval（lam M）（lam M））| eval_app：（M，N，V：tm）（M '：Var->tm）（eval M（lam M '））->（evalM'[N]V）->（eval（app M N）V）。命题3.7设X是一组变量;对所有M;N 2X，我们有：（一）M ！N（）X`：（红色X（M）X（N））(ii) M ！N （）X`：（trredX（M）X（N））(iii) M+N（）X`：（eval（男）（女）大多数有趣的性质的小步和大步语义可以证明，而不使用上下文理论。这些性质包括进展引理，语义的确定性，大步和小步语义的等价性：定义闭合：tm -> Prop：= [M：tm]（x：Var）（notin x M）。引理进展：（M：tm）（闭M）->（isvalue M）\/（EX N|（红色MN））。 引理red_is_det：（M，V1：tm）（red M V1）->（V2：tm）（red M V2）->V1=V2。引理eval_is_det：（M，V1：tm）（eval M V1）->（V2：tm）（eval MV2）->V1=V2。引理red_eval：（M，N：tm）（red M N）->（V：tm）（eval N V）->（eval M V）。引理trred_eval：（M，V：tm）（trred M V）->（isvalue V）->（eval M V）. 引理eval_trred：（M，N：tm）（eval M N）->（trred M N）。通过对M的语法和（red MV1），（eval MV1），（red MN），（trredMV），（eval MN）的推导的简单归纳，证明了这些性质.4元理论（Meta theory）在本节中，我们考虑cbn的两个扩展：应用互模拟和观测等价，以及一个简单的类型系统。这使我们能够测试语境理论的模块性。 事实证明，虽然在第一种情况下，先前介绍的上下文理论是有效的，但在后一种情况下，我们必须稍微修改unsat公理，以考虑类型系统带来的变量的新行为4.1应用互模拟与观测等价