高阶逻辑框架中微积分的三阶表示的等价性及其在形式化证明中的应用

《理论计算机科学电子札记》58卷第1期（2001年）网址：http://www.elsevier.nl/locate/entcs/volume58.html18页的三阶表示- 微积分安德烈亚斯·阿贝尔InstitutfurInformatik，Ludwig-Maximilians-Universita tOettingenstr.67，80538Mu恩兴摘要高阶逻辑框架提供了一种强大的技术来推理具有绑定器的对象语言。这将证明的情况下，微积分与两个不同的粘合剂，可以最优雅地表示使用三阶常数。由于与二阶编码相比，三阶和更高阶编码的情况非常罕见，因此也给出了二阶表示，并正式证明了与三阶表示的等价性1引言微积分[11，10，4]是经典逻辑中蕴涵部分的证明理论，它被建立为一个通用的工具来推理具有控制的函数式编程语言，例如continuations和exceptions。 它基本上是微积分的第二个结合物的扩展。它的一些性质，如强规范化和连续性，对于它在函数式编程和证明系统中的使用是非常基本的;因此，这些基本性质的形式化验证是可取的。人类的证明是容易出错的，即使是那些经过科学审查的证明。例如，首次发表的微积分的连续性证明包含了一个最近才被纠正的aw [3]。当使用绑定器推理编程语言和逻辑时|比如微积分|高阶逻辑框架的使用可以大大减少形式化证明所需的大小。这是由于其内在的概念，- 等价和替代，使几个技术引理过时如果选择了对象语言的巧妙表示。1abel@informati k. uni-muen ch en. De2这项工作得到了慕尼黑Graduiertenkolleg Logik in der Informatik（GKLI）和卡内基梅隆大学教育技术办公室的c 2001年由Elsevier Science B出版。诉 在CC BY-NC-ND许可下开放访问。据我们所知，微积分的性质迄今还没有得到机械验证。本文打算通过给出高阶抽象语法中-演算的两种可能编码来提供一个工作点正如我们将看到的，微积分是一个罕见的例子，可以最好地表示的方式，涉及一个三阶构造函数。这种表示将使结构或混合替换的自然实现成为可能，这在文献[10，16，6，4]中已经有争议地讨论过。本文的其余部分组织如下：在第2节中，我们将介绍Parigot [11]原始公式中的-演算。我们将在第二节中继续对其进行计算解释3给出了一个小步长语义及其在异常处理中的应用。第4节包含了非类型化和类型化演算的三阶表示的发展，以及小步语义的形式化。 我们将指出一个困难的表示，并给出一个替代方案，二阶编码和证明等价的两个表示在第5节。本文最后将对今后的工作进行展望2帕里戈特氏- 微积分在他1992年的开创性论文中，Parigot [11]介绍了微积分作为经典逻辑的证明理论。在下文中，我们将介绍一阶碎片，在其计算解释中，它提供了一个通用的工具来模拟函数式编程中的控制。原始术语由以下语法给出：M：：= x j x：M j M j a：N（未命名）术语N：：=[a]M命名术语它基本上是一种 - 结石加第二个活页夹和-应用[a]M. 此外，还有第二类变量，我们称之为-变量，用a、b和c表示，与用x、y和z表示的-变量相反。构造函数结合第- 在下列术语中可变;至于- 变量，- 可以定义等价性。 在下文中，我们将不区分- 同等条款。原始术语可以通过我们以自然演绎风格呈现的以下规则进行类型化：x：一个M：B！IxM 1：A！ BM2：A！EM1 M2：Ba：A M：Aa：A编号：拉阿x：M：A！ B[a]M：contraa：不适用在规则raa中，判断N：这意味着项N没有类型。这个符号表示荒谬，它不被认为是一种类型。公式A表示A的同类型;在逻辑领域中，A将是被否定的命题A。因此，引理同构于经典逻辑中的归谬规则，即如果：A导致矛盾，则A成立。相反规则类似于逻辑中的事实：A和A引发矛盾。 请注意，没有任何规则可以构造 同模标本因此，如果C：A成立，则C必须是a -变量a。项[a]M是由一个-变量a应用于项M而得到的，它没有类型，但它被称为由a命名，因此被称为命名项。由于封闭项存在于与直觉主义逻辑的蕴涵片段中的重言式同构的类型中，封闭项存在于与经典逻辑的蕴涵片段中的重言式同构的类型中。主要的例子是皮尔斯类型（A！B）！A）！一个被长期居住的地方x（A！B）！A：aA：[a]（xyA：bB：[a]y）但在微积分中是空的。(For更好的可读性，我们已经用它们的类型注释了抽象的变量。2.1减少在简单类型演算中，每个正规项M都有子公式prop-1：如果x1：A1;：;xn：An`M：A，则M的每个子项都是由A或Ai的子公式对某个i给出的类型每一项M都有一个正规形，它可以通过无数次的归约得到.约化关系由-公理的相容闭包给出.（x：M 1）M 2！[M 2 =x]M 1在-演算中，我们在确定子公式时忽略否定，即认为A是A的子公式。然后，我们可以定义一个约简关系，该约简关系计算具有子公式属性的范式，如- 微积分除了-归约，我们还需要由以下公理导出的置换转换：（a：N）M！b：[m]z：[b]（z M）=a]N这涉及到一种新的代换[nz：[b]（z M）=a]N，即Parigot结构代换，它具有如下效果：在N中，对于任意项M0，用[b]（M0M）替换形式为[a] M0的所有子项.我们对结构替换的介绍遵循de Groote [6]，他引入了语法的内部扩展：M ：：= x j x：M j M j a：N项N ：：=[C]MC：：= a jz：N（z在N中只出现一次）上下文ÆAA本文将结构替换推广到上下文[C=a]M的替换。 在上下文替换为-变量后，线性归约会无声地消除出现的"“[z：N]M ！[M=z]N：还原的结果是发现隐藏的还原;在一个例子中可以很好地解释。考虑以下类型A的开放项：y：A`（aA！A：[a]xA：x）y：A因为它包含类型A的子项x：x！A，此项不满足子公式的所有性质。它被一个-redex（x：x）y销毁，它被一个-abstraction分隔。这个隐藏的redex可以通过一个排列来发现：（aA！A：[a]xA：x）y！ BA：[zA！A：[b]（zy）=a]（[a]xA：x）=bA：[zA！A：[b]（zy）]xAx！Æ b：[x：x=z]（[b]（z y））= bA：[b]（xA：x）y！bA：[b]y请注意，该！降阶步骤被视为结构置换的一部分。最后，我们引入第三种归约，类似于-归约：[a]b：N！[a=b]NParigot称这种简化为命名术语的“重命名”。它需要第三种替代|-variables for -variables|如《易经》和《易经》所言，然而，在我们的表述中，它只是上下文替换的一个特例。由这三个公理导出的归约关系，和是一致的.然而，Tait和Martin-Lof并行简化方法的直接适应失败了。这在最初的conuence证明[11]中被忽略了，直到几年后，Baba，Hirokawa和Fujita [3]才给出了正确的证明他们发现，在其简单的定义中，平行还原不具有金刚石性质。这是由于- reduction的双重效果：它可能会创建一个-redex，但同时会破坏一个-redex。？，c、、、、、vvz例如，在一个示例中，（a：[a] b：[a]（x：x））y得双曲余切值.（a：[a]（x：x））y、、、、、、、、、、za：[a]（b：[a]（x：x）y）y、、、a：[a]（x：x）y的 -redex [a] b.隐藏在 - 还原步骤。另一 需要减少以恢复它。3计算解释自从Griffyn [8]的开创性工作以来，人们知道函数式编程的控制结构，如call/cc或Felleisen的C [7]，可以通过经典重言式来类型化。因此，我们期望-演算可以被操作地解释，使得已知的控制构造可以被编码为- 条款 事实确实如此|正如Ong和Stewart所证明的 ，[10]”[4]李文。 下面我们介绍一下王和斯图尔特的呼吁-by-value -calculus，Bierman的小步骤语义和de Groote的异常处理演算[5]的编码到-calculus中。3.1按值调用- 微积分的微积分可以通过数据库、区分大小写和递归来扩展，形成程序设计语言的核心。这是由Ong和Stewart完成的，他们将由此产生的玩具语言命名为PCF。 我们将坚持它的核心v，这是一个具有按值调用约简策略的微积分。一个值v是一个简单的抽象。我们通过添加两个规则并将-公理限制为值来获得按值调用策略。（x：M）v ！v [v=x]Mv（a：N） ！b：[vz：[b]（v z）=a]Na：[a]M！M （62 FV（M））v的确定性求值策略由以下小步语义给出。3.2一小步语义学Bierman [4]给出了一个简单的按值调用的小步骤语义，它揭示了抽象和应用的含义。在我们介绍它，我们用一个单一的洞来定义和评估上下文：E：：=jEM j vE评估上下文R：：=vv j a：N Redex引理3.1（分解）每个闭的未命名项M要么是一个值，要么可以被唯一地分解成一个求值上下文E[]和一个redex R，使得M = E[R]。此外，命名项N总是具有[a]M的形式因此，使用将变量映射到求值上下文的环境E，我们可以通过三个公理来阐明小步语义(E[(x：M）v]; E））（E[[v=x]M]; E）(E[a：N];E））（N;E] fa 7！E[ ]g）([a]M;E ] fa 7！E[ ]g））（E[M]; E]fa 7！E[]g）注意环境E绑定M或N中所有自由变量的不变量.这种语义表明，就像-变量是术语的占位符一样，-变量代表上下文或延续。绑定- 变量a意味着将当前上下文保存在a中，并且将a应用于项M意味着恢复由a表示的上下文并且在该上下文中继续对M的求值。在本文后面的部分中，这种见解对于确定最佳高阶表示非常重要。3.3de Groote的异常处理演算为了证明- 演算模型控制，我们提出了一个类似于SML的异常处理机制，由de Groote [5]给出。通过两个构造将异常添加到-calculus中：一个构造声明一个新的异常并为其提供处理程序;另一个构造引发异常。它们的类型如下：e：AM：Bx：一个Me：B手柄e：A M：Araisee（M）：B提高（异常e在 M句柄 e（x）：Me）：B我们通过两个例子来描述所需的计算行为：E中的异常e[raisee（v）]handle e（x）：Me;[v=x]Meexception ein vhandle e（x）：Me;vBierman将这两个结构翻译成-项。注意，raise的编码引入了一个-Redex确保按值调用评价p升e（M）q=（y：：[e]y）pM qp异常e 在M 中处理e（x）：Meq =a： [a]（x： pM eq）（e：[a]pM q）读者被邀请说服自己，这个翻译有规定的评价行为，例如，通过验证，（ pexceptioneinraisee （ v ） handlee （ x ） ： xq;E ） ）（v;E0）：假设读者现在已经对微积分有了一些熟悉，在下一节中，我们将讨论它在推理框架中的形式表示。4三阶表示关于逻辑和编程语言的形式推理，在下文中称为对象理论，必须在一个框架中进行，即Meta理论。这种逻辑框架的一个可能选择是谓词逻辑：由函数符号和变量组成的一阶项编码然而，对一阶表示中具有绑定器的语言进行推理是一项繁琐的工作，并且需要大量关于变量重命名，替换等的技术引理更合适的是具有高阶术语语言的逻辑框架，该语言本身具有绑定器。对象变量可以用Meta变量编码，对象理论中的替换可以用逻辑框架中的替换来表示高阶逻辑框架的主要候选者是简单类型演算！使用-equality，其中具有绑定器的对象语言可以直接编码。例如，无类型演算可以由以下签名表示。碱基类型tm术语林恒：（tm！tm）！ tmAbstractionapp：tm！tm！ tm应用表示函数pq将任何非类型化项M映射为逻辑框架。它由M上的递归定义如下：px：M q =lamx：t m：pM qpM1M2q =apppM1q pM2q给定的表示是适当的，即在非类型化项和它们在逻辑框架。定理4.1（不确定性）设=x1：tm;：;xn：tm是上下文。然后(i) 对于fx1; ： ：;xng中具有f个变量的每一个单位项M，(ii) 对于每一个具有` t：tm的正则（即-正规-长）项t，存在一个unty pe d-项Ms. th。pM q=t，并且(iii) 在p[M1=x]M2q=[pM1q=x]pM2q的意义下，表示函数是可压缩的。证据通过归纳（i.）M，（ii.）t canonical，和（iii.）M2。抽象的事例x：指的是具有扩展上下文的归纳假设（;x：tm）。2我们观察到在高阶逻辑框架中表示无类型演算的这些好处。：（i）等价于将项M1和M2转换为逻辑框架的等价项，以及（ii）不必实现替换。关于逻辑框架的更多信息可以在[13]中找到。4.1无类型微积分无类型-calculus通过抽象扩展了无类型-calculus和-应用。我们该如何展示新的活页夹？ 让我们来分析一下活页夹的一般结构：bind：（ ！）！绑定器绑定从类型为的上下文生成类型为的表达式，该表达式具有类型为的自由变量 . 我们知道活页夹 取一个带有自由变量a的命名项N并返回一个项。因此，我们将以下常量添加到签名中。基本类型名称命名术语常数mu：（！nam）！ TM提取在这个签名中，必须用被mu绑定的变量的类型来替换。在lam的情况下，我们有=tm ，因为-variables只是代表项。关键的问题是：-variables代表什么？“小步语义表明它们是求值上下文的占位符。这是由结构替代的性质所证实的，即用语境代替语境。我们利用了上下文可以直接表示的事实！ 作为从项到项的函数，并设置= tm！nam.因此，常数mu的类型是三阶的：mu：（（tm！ nam）！ nam）！ TM令人惊讶的是，我们不必为应用程序添加一个常数;它由中的应用程序表示！. 项M、N和上下文C的平移函数是通过以下定义的pqpa：N q=mua：tm！nam：pN q ：tmp[C]M q=pC q pM q： 名称paq=a： tm！nampz：N q=z：t m：pN q ： tm！nam定理4.2（严格性）设= x1：tm;：; xn：tm; a1：tm！ nam;：; a m：tm！nam.此外，还有一个适应性。4.1因为它认为，(iv) 对于其中具有f个变量的每个命名项N，(v) 对于每一个具有` s：nam的规范项s，存在一个命名项N s.th。pN q=s，(vi) 对于每个（不一定是线性的）上下文C，其中有自由变量，它认为，`pCq：tm！南，(vii) 对于每个正则项r，`r：tm！ nam存在（不一定是线性的）上下文Cs. th。pCq=r，并且，(viii) 该表示对于上下文替换是组合的，即，p[C=a]M q=[pC q=a]pM q：证据 我们证明1.，4. 和6. 同时在M/N/C上诱导，2.，5.和7.通过归纳的标准形式的TM，NAM和TM！ 南，和8. 通过对M.2请注意，我们只充分表示了一般上下文，而不是线性上下文C。然而，我们事实上在归约规则和小步语义的编码中写下的所有上下文实际上都是所需的形式。在给定的编码中，结构替代，这在文献中看起来很复杂（例如，[10]这是正义的。- 变量的-替换（见8.）。例如，p[z]：[b]（zy）=a]（[a]x）q=p[b]（xy）q=b（appxy）=（z：tm：b（appzy））x=[z：tm：b（appzy）=a]（ax）=[pz：[b]（zy）q=a]p[a]xq：4.2类型演算表1列出了对依赖类型演算中的良好类型项进行编码的签名3rd|逻辑框架的核心，如LF [9]。 为了表示类型A的项，我们实例化类型族tm：ty！类型为tmA。注意，在常量声明中，A和B被认为是良好类型的术语：ty： type类型TM：ty！ 类型类型化术语nam：类型命名术语我：ty基类型） ：ty！ ty！ Ty函数空间林：（tm A！ tm B）！ tm（A）B）- 抽象app：tm（A）B）！ tm A！TM B应用mu：（（tm A！ nam）！ nam）！ tm A-抽象化减少：！ ：tmA！tmA！ 输入红色对于键入的术语！nam！ nam！ 你是我的朋友。对于命名条款！ ：M：tm A！我的意思是：app（lam M）N！M N-公理！：M：（tm（A）B）！nam）！ nam：N：tm A：app（muM）N！我的天啊！姓名：M（z：tm（A） B）：a（appzN））-公理！la m;！app 1;！app2：lam-andapp-congruences(i) 直接代表（不充分）：！：a：tm A！我的天啊！nam）！姓名：a（muM）！nMa-公理！nam ：a：tmA！ na m：M！ M0！ M！na M0na m-congruen ce！亩：（a：tmA！ nam：Na！nN 0a）！ muN！muN0mu-congruence(ii) 符合当地规则的代表性（适当）：！亩：（a：tmA！姓名：！：（M：（tmA！ na m）！ nam：a（muM）！nMa）：！nam：（M;M 0：tmA：M！ M 0 ！ M！na M 0）：！ 不！nN0a）！ muN！ muN0m u-congruen ce表1签名第三：良好类型的术语和简化。隐式量化例如，常数lam的完整类型为A：ty：B：ty：（tm A！ tm B）！ tm（A）B）。还原由一对y pe族表示，！ 还有！n.在第（一）部分中，两条规则的表示！还有！nam还不够，因为上下文C可以为a实例化，但只允许-变量。这个问题可以通过删除这些规则并使其成为本地规则来规避：每当一个新参数a：tm A！引入NAM，动态添加这些规则。唯一一条引入了such参数的规则是！我们将以第（二）部分的版本取代。我们表示的精确性可以用类似于Thm的方式来陈述和证明。4.2.4.3小步语义在下文中，我们将重新定义并编码第3.2节中给出的小步语义（M;E））（M0; E0）。原来的公式有一点aw：在评估过程中，环境E单调增长，并积累了永远不会再次使用的上下文。我们给出了一个修改，使用替代而不是环境，并包括主题M到评估上下文C和redex R的分解。常量eval表示顶级求值上下文。Valuesval：tm A！ 类型v：：= x：Mvlam：M：tm A！ tm B：val（lamM）评估环境C：：= z：[eval]zeval ：tmA！ namjz：[C]（zM）z：pCq（appzpM q）jz：[C]（vz）z：pCq（apppvq（z）又不是每个居民的TM A！ NAM代表有效的评估上下文。然而，一个判断ecxt：（tm A！ nam）！可以很容易地定义一种类型，它可以挑出求值上下文。小步长语义可以由下面给出的四个规则定义。形式上，它将一个命名术语映射到另一个。我们说一个项M的值为vi [eval]M） [eval]v。）[C]（（x：M）v）[C]（[v=x]M ）[C]（a：N））[C=a]N）苹果[Z：[C]（zM2）]M1） N [C]（M1 M2））N）appr[m/z：[C]（vz）]M）N [C]（vM））N在）的左侧，[C]M的出现将被读作\term M，上下文C”，但在右手边，它只是命名项[C]M。在每一步之后，我们将reduce N重新分解为[eval]M。这是可能的，因为下面的不变量成立：如果C和M是闭的，并且[C]M） N，那么对于闭项M0，N = [eval]M0。显然它适用于规则），）appland）ap pr. 为了证明它的规则）我们首先注意到，[C=a]N是一个封闭的命名项。因此，它必须等于[c]M0对于一些-常数c，它只能是eval。“的表示将上下文项对CMi n映射到另一上下文项对C 0 M 0。将命名术语分解为上下文，我们在非正式治疗中默默地做了一个术语，由辅助法官nt\）n执行“。）：（tmA！ nam）！ tmA！ （tmA0！nam）！ tmA0！泰培）nam！ （tmA0！ nam）！ tmA0！泰培）eval：M：tmA0：（evalM））nevalM在下面的翼中给出了用于“的四个计算规则。注意“这是用X写的，在它的两个字母后面。） ：C：tm B！ nam：M：tm A！ tm B：V：tmA：val V！（C（MV）nC0M 0！ C（app（lamM）V））C 0M0） ：N：（tm A！ nam）！ nam：C：tm A！ nam：（NC））nC 0M 0！C（muN））C 0M0）appl：（z：C（appzM2））M1）C 0M0！C（appM1 M2））C0M 0）ap pr：（z：C（appVz））M）C0M 0！valV！C（appV M））C0M05二阶表示尽管我们设法证明了，-微积分是优雅和足够的，它不是没有陷阱：正如我们已经看到节。4.2，归约关系的直接表示是不够的;命名项的规则必须为新参数a局部引入：tm T！nam.这适用于普通的还原，但不能应用于pa ra lle还原的表示。考虑规则=）：=）：a：tmT！ nam：（b：tmT！nam：Mb=）nM 0b）！a（mub：Mb）=）nM 0a这个规则的一个应用有以下效果：[a] b：M被-规则约化，并且在M内可能发生额外的约化。假设引入了一个新的参数b，因为我们踩在粘合剂下面。为了使这个规则局部化，必须为每个作为参数引入的变量添加它，因此也为b添加t。必须将hus=）插入到其自身中。这导致了一个本地规则的内部链，无法实施。这些问题不会发生在二阶表示中，我们将在本节中介绍。我们间接地定义了表征函数，并间接地证明了充分性，如图所示1.一、首先，我们要˛、J的二阶表示的精确性- 条款：计算值p q==为p qzCont可以，p q=简体中文p q=JzJ第2众议员+第3Z（+）=的+第2约化的二阶表示的精确性！（互模拟）：可以继续LzHLJ0zH 0，oH0型Fig. 1. 概述：二阶表示微积分的延续续，一个修改的-演算，允许一般的延续项K在一个-应用程序，现在称为抛出K E。原则上，我们让klam是一个显式的构造函数klam，而不处理！别再沉默了。此外，在表示2nd中，我们添加了一个用于延续的基本类型。 然后，我们定义了正则表达式H2，Cont可以作为那些只包含continuation变量的，也就是没有klam的。每个表达式H2Cont都可以通过应用规范化来规范化HH0.对于这些结石的三种表示，我们可以在以下方面证明其充分性：直截了当的态度。因此，在每种情况下都存在一一对应，我们可以限制自己对原始微积分的推理，以获得它们的表示的类似结果特别地，如果我们在和Contcan之间构造一个双射，我们隐含地定义了的一个充分的二阶表示。作为第二部分，我们定义了一个约 化，并证明了它是约化的二阶表示。在（L！ L0）和减少的连续可以（H！ H 0），如图1所示。唯一需要小心的是H！因为在H上应用结构替换临时创建了一个非规范表达式，我们必须对其应用规范化。因此，我们将标准化纳入归约。在下面，我们将简要证明的充分性的二阶表示。整个证明已经在BMF [14]中进行，并且可以通过电子方式获得[1]。我们认为这是一个案例研究的正式推理系统的三阶表示。据我所知，这是第一次正式证明在表示的顺序严格大于2。 这J00000可能是因为很少有三阶或更高阶表示可以应用的情况。原始表达式：E：：= x j x：E j EE jcatch k：F表达式F：：=throw KE响应K：：= k jklam x：FH：：= E j F jK任何连续项打字：签名二：exp：ty！typeresp：类型cont：ty！类型lm：（exp A！实验B）！exp（A）B）ap：exp（A）B）！实验A！exp B catch：（A！resp）！ 实验A扔：A！ 实验A！ respk： AF：catchk：F：AK： A E： A投掷KE：x：一个F：klamx：F：Aklam：（exp A！ resp）！ A.A.规范的原始表达式可以：可以xcan E可以x：E可以E1可以E2可以E1E2can KcanEcanthrowKE罐kcan F能抓到k：F归一化HH0：0 0E1第一季第二集E2Xy0E EE EKL[E=x]FFthrow（klamx：F）EFEE1212FFKK EEx：Ey：E投掷动能掷K Ecatchk：Fcatchl：F从in到Cont的转换L==>=H可以：M1==>=E1M2==>=E2x==>=yM==>=Ex：M==>=y：EM1M2==>=E1E2a==>=KM==>=E[a]M==>=thro wK Ea==>=kN==>=Fa：N==>=catchk：F减少H！H0 inCont可以：（x：E1）E2 ！[E2=x]E1throwk（catch l：F）！[k=l]F[klamz：throwl（z E）=k]F F（catchk：F）E！catchl：F表2ContinuationsCont和Canonical FragmentContcan的微积分5.1连续微积分表2描述了Cont的新表达式、延续和响应（名称源于Stre- icher/Reus[16]），我们将所有这些都称为原始表达式H。000000规范原始表达式H是那些不包含klam的表达式。可以H的判断是通过H上的递归建立的;除了klam之外，所有的结构都有同余规则。Contcan是Contw.r.t.的商。 由公理throw（klamx：F）E = [E=x]F导出的等式。我们通过应用大步骤按名称调用规范化程序HH0获得了一个连续项H的典型代表H0。引理5.1（的性质））(i) 如果H1H2可以是H2。(ii) 如果H1H2和can H则[H=x]H1 [H=x]H2。（二）证明（两种说法）。 通过H1H2。25.2互模拟R_L==>=H构成了两个项之间的双射翻译，-calculus L和Contcan-expressions H.下面的矩形定理（cf.图1）指出，- 约简可以用Contcan-约简模拟。定理5.2（模拟）如果L==>=H且L！ L0，那么L0==>=H 0和H！ H 0为一些H 0。我的律师。 通过L上的归纳！ L0。唯一的麻烦就是！ 因此我们需要引理5.3。2引理5.3（替换）如果然后a==>=kL==>=H和x==>=zyC==>=D0D[klamy：D=k]H 0[klamy：D=k]H证据通过对L.我们拼出困难情况L =[a]M。[a]M==>=thr owk Ebyass.M==>=Ebyinversion[X：C=a]M==>=E 0byind. 好的。[X：C=a]（[a]M）=[[X：C=a]M=x]C=>=[E 0= z]D0y假设E 0[klamy：D=k]Ebyind. 好的。[E 0= z]D0[[klamy：D=k]E=y]Dby假设[E 0=z]D0thr ow（klamy：D）（[klamy：D=k]E）bydef. 的= [klamy：D=k]（throwk E）2请注意，证明使用了扣除的替代。例如，我们通过用[x：C=a]M= > = E0来说明假设C = = > = D 0的推论x==>=z，来表示[[x：C=a]M = x ] C==>=[ E0 = z ]D 0。类似地，可以证明Cont中的约简可以模拟给出互模拟的-演算中的约简。6结论本文介绍了微积分的应用，并讨论了两种不同的编码.三阶表示法似乎是微积分的最佳方法，因为所有三种替换都被简化为逻辑框架的替换。此外，我们可以形式化的小步语义经济。然而，并行归约的直接表示失败了。二阶表示不受这些问题的影响，但需要辅助概念，如规范项和规范化，这在实践中大大提高了证明。两个进一步的研究方向从这里开放：在三阶表示方面，平行约简的替代配方必须进行研究。一个具体的思想是引入一个辅助判断“C是一个变量”，它使得规则的局部化是超连续的。为了改进对二阶表示的支持，可以扩展逻辑框架以允许类型重命名。规范表达式的类型是表达式类型的一个子类型。一个项H是否是正则项的事实是可以确定的，并且可以H的证明将是无关紧要的，并且可以被隐藏。Pfenning [12]为逻辑框架的这种扩展奠定了理论基础。三阶表示可以用来证明微积分的许多性质。首先，我已经正式证明了Ong和Stewart [10] wrt给出的大步骤语义的可靠性。到评估框架堆栈小步语义。我希望在未来的编码更多的应用。致谢。是拉尔夫·马特斯第一次使我对微积分感兴趣。Frank Pfenning和Brigitte Pientka的许多讨论和想法值得我感谢。我感谢拉尔夫、弗兰克和两位匿名裁判对草案的评论。最后但并非最不重要的是，我感谢造物主为人类生活和思考提供了框架。引用[1] Abel，A.，A third order representation of the -calculus，Biblif code（2001）. URLhttp://www.tcs.informat ik.u ni-m uen chen. de/~ab el/m erli n01. tar.gz[2] Altenkirch，T.，LEGO中系统F的强正规化证明的形式化，在：M。Bezem和J.F. Groote，editors，Typed Lambda Calculi and Applications，TLCA'93，Lecture Notes in Computer Science664（1993），pp. 13{28.URLhttp://www.tcs.informat ik.u ni-m uen chen. 去/去其他的地方。HTML[3] 巴 巴 ， K. ， S. Hirokawa 和 K. Fujita ， Parallel reduction in type free -calculus ， in ： Proceedings of CATS 2001 （ Computing ： the AustralasianTheory Symposium ） ， Electronic Notes in Theoretical Computer Science42（ 2001 ） ， also appeared as Technical Report DOI-TR-177 ， KyushuUniversity，Fukuoka，Japan.URLhttp://zk.cc.kyushu-u.ac.jp/~baba/[4] Bierman，G. M.，一个计算解释的-calculus，in：L. 布里姆，J. Gruska和J.Zlatuska，编辑，计算机科学数学基础研讨会论文集，计算机科学讲义1450，布尔诺，捷克共和国，1998年，pp.336{345.网址http://www.cl.cam.ac.uk/~gmb/[5] de Groote，P.， 异常处理的一个简单演算，在：M。 德扎尼和G. Plotkin ， editors， Second International Conference on Typed LambdaCalculi andApplications ， TLCA'95 ， LectureNotesin ComputerScience902（1995），pp.201{215.URLhttp://www.loria.fr/~degroote/bibliography.html#1995[6] de Groote，P.，微积分的环境机（1998），出现在MSCS中。URLhttp://www.loria.fr/~degroote/bibliography.html#wp[7] Felleisen，M.，D. P. Friedman，E.Kohlbecker和B.F. Duba，顺序控制的句法理论，理论计算机科学52（1987），pp.205{237.[8] 格里森，T. G.， 一个公式化的控制概念，in：Proceedings第十七届ACM/SIGACT-SIGPLAN程序设计语言原理研讨会（POPL）（1990）。URLhttp://www.research.att.com/~griffin/pubs.html[9] 哈 珀 河 ， F. Honsell 和 G. Plotkin ， A Framework for De ning Logics ，Journal of the Association of Computing Machinery40 （ 1993 ） ， pp.143{184.[10] Ong ， C. H. L. 和 C. A. Stewart ， A Curry-Howard foundation for functionalcomputation with control ， in ： Proceedings of ACM SIGPLAN-SIGACTSymposium on Principle of Programming Languages（1997），pp. 215{227.URLhttp://users.comlab.ox.ac.uk/luke.ong/publications/index.html[11] Parigot，M.，- 演算：经典自然演绎的算法解释，在：A。Voronkov，编辑，Logic Programming and Automated Reasoning：Proc. of the InternationalConference LPAR'92，Springer，Berlin，Heidelberg，1992 pp。190{201.[12] Pfenning，F.，Intensionality，extensionality，and proof irrelevance in modaltype theory，in：LICS 2001：IEEE Symposium on Logic inComputerScience，2001.网址http://www.cs.cmu.edu/~fp/publications.html[13] Pfenning，F.，逻辑框架，在：A。Robinson和A. Voronkov，编辑，自动推理手册（2001）。网址http://www.cs.cmu.edu/~fp/publications.html[14] Pfenning，F. 和C. 史昌湖林文辉，《计算机科学》，北京大学出版社，1998年。网址http://www.cs.cmu.edu/~twelf[15] Shankar，N.，Church-Rosser定理的机械证明，ACM杂志35（1988），pp。475{522.网址http://dev.acm.org/pubs/citations/journals/jacm/1988-35-3/p475-shankar/[16] Streicher，T.和B.Reus，Classical logic，continuation semantics andabstract machines，Journal of Functional Programming8（1998），pp.543{572.URLhttp://www.mathematik.tu-darmstadt.de/~streicher/