理论计算机科学电子笔记57（2001）网址：http://www.elsevier.nl/locate/entcs/volume57.html21页简单类型理论通过评估Ren eVestergaard1;2Institut de Mathematiques de Luminy法国马赛国家科学研究中心摘要我们开发的类型理论的规范化评估（NBE）算法的演算在简单类型的情况下。特别是，我们表明，该算法计算长（）-正规形式通过Plotkin的调用的名称和调用的值评估语义。这是值得注意的（i）因为算法决定完全相等和（ii）因为算法到目前为止仅在模型理论方面提出。为了展示该算法的有效手段，我们提供了一个环境机器实现的语义：NbE机。我们还分析了语义和环境机的策略，-calculus并随后处理未类型化的情况。举证责任很轻。1引言评估标准化（NbE）最初是由Berger和Schwichtenberg在大约十年前研究的[6]。它是一种方法，通过这种方法，语言模型的意义函数（又名评估函数）可以用来规范语言的术语。简单地说，NbE是一个类型索引函数，它接受与某个术语对应的语义对象作为参数，并返回该术语在给定类型下的long（）范式。所有的计算都在模型中执行;结果仍然是一个语法术语，而不是传统意义上的语义对象。由于这种功能，NbE的模型理论通常涉及使用相关语法增强标准模型;这是非常重要的。NbE算法适用于许多情况，并且已经被提出作为评估函数的逆”[6]，1 由欧盟TMR资助#ERBFMRXCT-980170：LINEAR支持2 电子邮件：vester@iml.univ-mrs.fr，WWW：http://iml.univ-mrs.fr/~vesterc2001年由Elsevier Science B出版。V. CC BY-NC-ND许可下的开放访问。Vestergaard2B规范化”[1，2]，\type-directed partial evaluation”[10]，作为Tait证明强规范化的类型化方法的计算内容[5]，作为直觉主义模型论中的粘合构造[7]，以及作为（构造性）范畴论中的Yoneda嵌入[9]。1.1影响NbE算法的最初动机在很大程度上是实用的[6]。发明该算法是为了获得慕尼黑LMU的MinLog证明系统的内部证明对象的语法表示[6]中的主要焦点，除了域理论正确性证明之外，因此使用编程语言Scheme [16]的引用和非引用结构来提供简单类型演算算法的本地（而不是解释性）实现。[3][12]中给出了这种原生实现在更传统的编程语言环境中如何工作的重要细节。与此相关，[10，11]证实了NbE用于部分评估的有用性，特别是基于语义的编译（即，自动编译器推导）。NbE的主要理论影响，除了它的技术化身的绝对数量之外，迄今为止被认为是这样一个事实，即al-出租相当于一个用于类型等价的基于非重写的决策过程。1.2我们的贡献我们将表明，NBE也有有趣的理论意义，在重写为基础的设置。特别地，我们将证明该算法通过使用非常有限的计算能力来计算长（）-范式，即，Plotkin风格的求值语义[17]，这使得它从实用的编译器技术角度来看也很有趣。我们通过以下方式实现这一目标：采用两级索引的评价战略- 微积分：NbE与b2fn; v; w g表示按名称调用（CBN）、按值调用（CBV）及其组合：按任何方式调用（CBW）。我们用NbE来表示这三者的结合。NbE的一个级别充当模型的角色，另一个级别充当目标语法的角色。句法层面显然不受评价。NbE算法的核心被表示为NbE中的规范级间项强制器。我们给出了一个正式的介绍，这是直接的点，这并不涉及复杂的模型理论的技术。我们提出的类型理论和Plotkin风格的评价语义NbE和显示（i），该算法计算长（）-范式和（ii）3 原生意味着执行算法所需的计算可以由实现语言的求值机制承担。Vestergaard3Fig. 1. - 演算的简单型系统：* =o j ！ | ranges在从变量到类型的逐点定义的函数上;逗号\，”隐式地应用于具有disjoint（！）域和手段功能融合。需要使用（弱）-规则来输入像x：x：e这样的术语。（啊！（E）. e1@e2：. e2：. e1：！（啊！第一章）x：;. e：. x：e：！（弱）. e：x：;. e：（变量）x：;. x：简单类型相等的语义是合理和完整的。我们提出（并在ML中编码）一个环境机器，NbE机器，它实现了我们的类型理论NbE语义。我们分析了上述在-演算方面的减少策略，因此，能够扩展NbE到一个大类的无类型的条款|事实上，是最大可能的：所有具有简单类型范式的项。虽然基于语义的方法自然地使用构造性模型，但我们觉得我们的方法在解释执行NbE的计算的实际有效手段方面更优越，例如，通过NbE机器。我们希望这将有助于促进更多实用的编程语言应用的NbE。1.3扩展和限制与上述相关，我们可以提到，我们已经成功地将我们的设置扩展到系统F，作为未发表的第二个[2]。我们还提供了用于系统的NbE的第一个（解释型）实现（ML）F通过其环境机，见初步[19]。我们的印象是，在任何现有的编程语言中，都不可能在System F中实现NbE。 原因是系统的子项 F项可以通过类型实例化改变其类型（而整个类型自然地通过Subject Reduction Property 保持不变），导致在类型改变时需要\delayed”NbE-ing。这实质上意味着类型替换需要在具有高阶类型构造函数的设置中以非标准的方式定义，例如System F。NbE机器被直接装备来完成这样的扩展，而对于本机实现来说显然不是这样1.4、 还有-微积分的相关功能的快速摘要，- 微积分定义1.1简单型微积分的前项（！）是e：=Vestergaard4图3.第三章。-减少和限制-扩大所有的一个米茨！. 前者是全等（即，经受完全上下文封闭），而后者仅经受规定的有限上下文封闭。&e不适用00！（x：e1） @e2！e1[x：=e2]e0x：e @ xif x 62 FV（e）&e 2&e 6=x：e图四、 的前期条件！的长（）-正规形式|d是反构造函数(aka中性术语）和c是构造函数（aka正常术语）。c ：：=x：c jd （如果d2o;cf：定义1：1）d * =x jd @c假设是同余，[：=]是非捕获置换，FV（）是一个术语中的自由变量的集合，以通常的方式定义。是！图二、 扩张方程理论|=，=，=，===为如果x 62 FV（e）&e2！e=x：e@xx：e=y：e[x：=y]ify62FV（e）（x：e1） @e2=e1[x：=e2]xj x：ej e@e;在图1中，术语表示为e2，def9：。 e：。的可拓方程理论！是== 参见图2.的可拓方程理论！ 是公理化的几个不同的重写关系，所有不同的性质。 例如，不受限制- 展开（图2中-方程的从右到左方向）不是强归一化的。当添加一个单位类型时，-reduction（图2中-equation的从左到右方向）在与- 减少。最强有力的公理化似乎是还原结合所谓的（薄荷糖）限制 - 膨胀，参见图3.定理1.2（！[4]第四节：重写：=被公理化了=[！[0，cf.图3.完整性：！[0个 是conuent（up to）和SN。一致性：=-是不平凡的。决定性： =是可以决定的Vestergaard5众所周知，限制性扩张与Huet的长期Vestergaard6（）长（）-范式[15]，其享有分析性属性：所有类型在术语（的语法）中在语法上是明显的定义1.3 [长（）-正规形式] 长（）-正规形式，（）长，是typable（cf.图1）图4中引理1.4（[4]）和的正规形式！[0重合。而且，0+！对于其他类型范例表现良好，例如，单位类型和系统F！[4，13]。在范畴重写[4]和代数重写[8]中的进一步考虑导致了受限的扩展假定对于大多数类型化的目的，选择关系是事实上的状态。也就是说，限制关系的重写性质的研究是不平凡的[4，13]。1.5CBN、CBV和微积分在开创性的[17]中，Plotkin建立了CBN和CBV之间的密切联系-函数式编程语言的求值（以微积分的形式）和连续传递风格（CPS）语言中的等同性。后来Sabry和Felleisen在控制算子的上下文中改进了这种联系[18]。这项工作的要点是，直接式评估语义与CPS平等是一回事。 一方面这这意味着CBN和CBV可以相互模拟。另一方面，我们知道这两种设置是函数式语言的编译器技术的原型，因此，结果使我们有可能形式化地推理和比较实现函数式语言的不同方法[18]。这些结果已经进一步扩大了，例如，由Hatterfly和Danvy [14]在另一种常见的编译器技术的情况下与控制运算符的语言：thunks。我们的观点是，Plotkin的CBN和CBV评估语义是当今编译器技术的组成部分，即使不直接使用。1.6本文概述第二节介绍了NbE的类型理论：NbE-演算.在第3节中，我们确定结石确实达到了预期的NbE目的。在第4节中，我们介绍了实现NbE-结石（即，的NbE）作为环境机器。在第5节中，我们介绍算法/环境机器的示例运行。最后，在第6节中，我们得出结论。1.7确认我们要感谢Olivier Danvy和Laurent Regnier进行了富有成效的讨论，并感谢Ulrich Berger，Andrzej Filinski，Martin Hofmann和匿名参考。Vestergaard7打字水平。和互不相干地属于每一个见图6。NbE的两层类型关系。;.. e：o;.. d：o（O2U）（U2O）;.. e：o;.. d：o;y：; .. c：x：;;.. e：（弱）（弱）;.. c：;.. e：;.. d@c：... e 1@e2：（啊！（E）（啊！（E）... d： ！... c：;.. e1： ！...e2：;.. x：e： ！;..y：c：！;;y：.. c：（啊！I）（！第一章）x：;;.. e：;;y：..y：x：;;.. x：（变量）（变量）图x2VNx; y 2VNy; VNx\e：：=x jx：eje @ejd（dc ：：=y：cjd（if je（ed * =y jd @c5. 前条款NbE超过VNy=;;VN2 =VNx[ VNy是类型受限的，参见。图d2Do;cf：定义2：1）是类型受限的，参见。图双排序变量名六、六、二、Vestergaard8他们的评论。感谢Paul Taylor，我们正在使用他的Prooftree宏。2NBE-微积分我们现在介绍我们的两级NbE演算，目的是使它们在不同的评估范式下捕获NbE算法的类型理论。 所采用的一些设计技术可用于设计 一个更一般的二级微积分概念。我们选择了相当狭窄地关注NbE。的NbE-演算是通过采取项模型构造的，！（ 即，Vestergaard9Cdef（x：e1）@e2！e1[xn0c！C dn0y：c！y：c d@cn见图7。CBN0e1！e1n： =e]e@e！ e0级2 1 2n1！d0c！nn！d0@cd@c！nn- 评价。@e20Cd@c0Plotkin风格的求值语义），并使用相关语法（即（）long）对其进行扩充。前者是用上划线写的，而后者是用下划线写的两层之间的重叠只允许在地面类型。其原因是类型索引NbE算法的解析性，并且与长时间中d的接地类型限制密切相关。（）-正规形式，参见图4和图5。这个特殊的特征实际上是NbE类型理论的决定性属性，而其他大多数属性都取决于此。定义2.1 [NbE术语]在图5和图6之后，术语如下：NBEe2， 9;：;.. ec2，def9;：;.. Cd2D，def9;：;.. DNbE=defNbE[C我们强调，我们在NbE术语中使用两个排序的变量名。x专用于上划线的级别（模型），y专用于带下划线的级别（语法）。定义2.2设p q是普通项到NbE项的上划线水平的注入，并且设x y是到下划线水平的注入。在介绍NBE术语的Plotkin风格的评估语义之前，我们指出，我们用于CBV情况的值的概念，参见。图8并不完全符合标准概念。特别是，我们承认任何严格下划线的术语作为值（在下划线级别中）。 这样做只是：：：Vestergaard10为了简化引理3.2的证明。事实上，它建议考虑y的作为下划线的值，这是标准的。不过，我们使用的概念显然是公正的，在目前的设置。定义2.3让NbE be（NbE;！）for b2fn; v; w g with！和b bn！分别在图7和图8中给出。VW--n [啊！.v引理2.4（主语归约）对于b2fn;v;w ge 2恩！e0）e02NbEBVestergaard11v 2 fx;x：e g[（）长00xy（x：e）@v！ e[x：= v]v0c！Cv0y：c！y：cv图0e1！e1v0e1@e2！e1@e2（x：e1）v0d！Dv0d@c！d@cv8.CBV-评价。e2）@e2Cd@c！v！v！v！v0e2（x：e1）0C0d@c）@0e2证据非正式地，它需要建立（i）接地类型水平重叠属性不被打破，（ii）句法约束（长（）-正常形式）。第二，（二），基本上是从（一）。反过来，（i）是从简单类型演算的主体归约属性中建立的，通过观察子项（的残差）的类型而不仅仅是项本身在归约下被保留。4或者，通过NbE机器评估机制的ML良好类型确定结果，如附录A.2作为一个插曲，我们可以表明，NBE是健全的方面！.定义2.5令jj：NBE ！是 剥离o的功能超过-和下划线。引理2.6F或b2fn;v;w g，！brees pects！根据jj：e！B e0）jej！je0jVestergaard12证据直截了当。2引理2.7（SN）Forb2fn;v;w g，！B是SN。引理2.8（一致性）NbE是不平凡的。2.1NbE中的类型索引层间强制我们现在导出NbE算法的核心，reect和reify，作为NbE中的规范级间项强制器，参见。图9.非正式地，胁迫是：函数类型术语的源代码级应用，直到达到基础类型，使用（U2 O）和（O2 U）的地面类型的实际术语-transferral，以及目标级别 - 对应于函数类型的抽象。为了解释强制，我们考虑两个例子。在第5节中，我们将在NbE机器的上下文中重新讨论这些示例[4]这是NbE的简单多态类型理论的一部分。Vestergaard13##oe第一名！2e“的od1！2个d图9.第九条。：NbE！C=e=y：#2（e@（“1：D个！NBE=d=x：“（d@（#12级别强制器，用于（y））（x））(aka（reify）（y62FV（e））(aka（reect）（x62FV（d））Vestergaard14：;yo.. x：x：：：;yo.. （x：x）@ y：o：：NbE-结石。示例：简单函数类型让我们考虑类 型 为 o 的 x：x！O. 通过将该术语应用于，比如，o（一个带下划线的基类型变量可以在两个层次中出现），我们得到一个基类型的项，它也可以在两个层次中出现;特别是从理论上说，这是这样写的：X o; y：哦..X（变量）O（啊！第一章）;yo..y;yo..y（变量）O（U2O）O（啊！（E）;yo.. （x：x）@ y（O2U）O（啊！第一章）...y：（x：x）@ yo！ O在我们考虑的所有评价范式下，构造项的范式是y：y，参见。定义2.3.示例：负函数类型考虑类型为（o!o）！哦！O.如果我们从一个带下划线的变量（下面的y 1）开始，可以构造一个类型为（否定出现的）o的项，那么我们可以通过两次以上的技巧将该项带入带下划线的级别！o属于上划线的级别。我们对所使用的技巧进行二元化，得到：y1：y2：（（x：x）@（x1：y1@x1））@y2构造项的范式在所有求值范式下都是y1：y2：y1@y2我们所给出的两种范式很容易被看作是给定类型的原始项的长范式|并存在于另一个层面。：：：：：：Vestergaard15引理2.9 #：NbE！（reify）and“：DNBE！（reect），cf.图9中，定义良好（给出了一种选择新名称的方法）。证据通过一个简单的归纳法对类型化导子进行了归纳。或者，结果遵循我们实现的reify和reect的ML良好类型，参见。附录A.2关于为reify和reect选择新变量名的正确方法，我们指出在我们的设置中有一个简单的解决方案，即两个排序的变量名。正如我们将看到的，#和“仅以非常特定的方式应用，参见。定理3.3.特别是，它们的应用总是以#开始，被应用于一个完全上划线的术语，因此不包含y。 因此，可以简单地从“第一个”开始按顺序挑选y|也就是说，y取为nite中可数的。 至于x，我们注意到虽然具体化（即， #）被应用于任意上划线的项，reect（即，“）仅适用于本身由reify和reect构造的带下划线的术语#1的定义！图2，图9。换句话说，我们选择的x上的任何抽象都只会在其范围内有其他新的x（和因此，它们也可以从“第 一”开始挑选。|也就是说，VN x也被认为是nite中可数的。只要我们维护最后挑选的x和/或y的计数器，就不需要检查项引理2.10 # and“respect = underj j：NBE8e 2： j e j =j #e j8d2：j d j = j“d j证据 通过对类型的简单归纳。2我们看到#不尊重 0 在Jj作为函数可以应用于抽象。另一方面，Mints的限制用于使-展开终止，而#和“由于是根据类型归纳定义的，因此它们本身是定义良好的。此外，NbE deciding =的-部分完全由reify和reect函数的使用（一劳永逸的类型索引）来解释：在每种类型中，reect和reify的使用相当于将所考虑的术语置于固定的上下文中。这应该与术语索引形成对比，可以说，在传统的重写设置中使用0 -关系：一个术语被重复地检查是否存在赎回。3通过评价实现有了目标明确的NBE在地方，提出NBE AL的任务租m几乎是微不足道的。为了表述的清晰，我们首先将注意力限制在封闭式条款上，但随后将立即讨论任意开放式条款的NBE。CVNDVestergaard16CBB12X1定义3.1 [x-封闭式术语]C让是没有自由变量的项的子集。BXNBENBE设为没有自由x的项的 子集 。BX设C 是的子集没有自由x的条件。下面的结果，我们需要的唯一非标准结果，本质上说，NbE的减少能够表达我们执行NbE所需的语义到语法计算。引理3.2（无重叠正规形）设b2fn;v;w gBX8c 2C是！- 正常）c2x（）长y证据利用一个双结构归纳法（关于项）证明了该结果，并证明了以下性质：5XxNBE第82章 ：是的！-正常）（e 2 C_ex：e0）B o唯一不平凡的情况是e对于后一个属性，e1@e2。 假设e为B！B-正常。 根据定义！b，e1是！b-正常和byI.H.，e12o_ex：e0. 上的类型约束不可能使第一个析取应用. 在第二个析取的情况下，e是一个redex，因此不是！-这意味着我们是通过矛盾来完成的。考虑一下，现在，形势为！v. 根据定义，e2必须是正规的，因此e22O _e2x：e0通过I.H.为 第一个析取项，我们有e22x（）下一页长y由其他I.H. e是a！v-Redex，与常态相矛盾。 类似地对于另一个分离。 案件！W 如下2我们现在已经准备好正常化了！通过评价。在此之前，我们要强调这一点！ 还有！通过定义在加下划线的术语中最多允许一个redexn v(and因此，最多有最外面的上划线项那么多的赎回，一个带下划线的术语）。如果存在，则redex将位于预定位置。事实上，根据引理3.2，在那个位置总是有一个redex，或者这个项会加下划线。因此不需要检查加下划线的术语来执行！b步骤，此外，还原将始终终止。这一评论将在第3.1节和第4.1节中进一步探讨。定理3.3（赋值正规化）设b2fn;v;w gB第八章第二章第九节！C2（）long：e =c^（（#peq）！（x、c、y）CCCBBXVestergaard17证据根据引理2.6、2.7、2.10和3.2。c的唯一性是由中的长（）-正规型的ty pe-指标唯一性所决定的。.25 事实上，这是一个三重结构归纳，也有d的情况|因此，我们对NbE的前项使用原始归纳原理，参见。图5.BVestergaard18BAA命题3.4定理3.3（但直到），可以扩展到开项（即，到e2）如果提供了项的自由x及其类型。证据在对相关类型应用#p q之前，用s抽象自由变量（并将额外的抽象重命名为原来的抽象，然后将它们从c中剥离出来2这不是对开放项进行扩展的最优雅的方法，稍后我们将介绍一种更令人愉快的方法。然而，它允许我们抽象出定理3.3的全部计算内容。为了做到这一点，我们注意到，由于定理3.3的证明是构造性的，我们可以直接“Skolemise”它建立的性质：9C： ！（）long：8e2：e=C（e）^（（#p e q）！ xC（e）y）上面的C是什么会引起我们的NBE，在每种类型。 我们的原因索引NbE与类型是密切相关的事实，延伸方程理论！是类型索引的：隐式类型的术语在其所有类型中都具有唯一的long（）-范式。命题3.5给定自由变量的类型，NbE： ！（）长 （e 7！c，cf.定理3.3和命题3.4）是泛函的。是的。 长（）-正规形式，C（e），是唯一的高达，比照。 定理 1.2. 2在着重讨论NbE的结构特征，即我们所说的有效手段之前，我们简要地阐述了它的模型论意义。定理3.6（对于= in，NbE是可靠的和完备的！8e1; e2 2：e1 = e2，NbE（e1）=NbE（e2）3.1jNbE j I的约简策略：最左性和无类型项下面的定义受[3]的启发。[6]有些概念在4.1节定义3.7【策略】A地图，S：A！A是关于的1-策略！AAA如果A！AS（a）. 这是一个战略，如果一个！AS（a）. 一个（1-）策略是有效的，如果它不仅编码一个递归函数，而且是递归定义的（即， 通过案例分割）。 这是正常的，如果E！e0^（e0 是！norma l））9n：Sn（e）=e0. 如果n=1，则它是1-正规化的。有了这个定义，我们可以立即给出下面的结果，它澄清了我们在定理3.3之前的评论。它还介绍了下一节。我们首先要注意的是，下划线的水平是不可变的，只要评估去。这意味着，在两个评价Vestergaard196 我们在[3，Chapter 13：Reduction Strategies]中使用了“递归地覆盖项”，而不是以相对简单的方式使用Barendregt的“[可计算的]”来支持”。我们还引入了“1-normalising”。Vestergaard20nnvn请注意，遍历时需要对抽象的y进行新鲜命名，参见。附录A，但为了清晰起见，此处未详细说明。图10个。 NbE机器|实现NbE的环境机。he;i+ue0hd@c;i+ud0@c0hy; i +uyhc;i+uc0he;i+ohe0;0ihd;i+ud0hc;i+uc0hy：c;i+uy：c0hd;i+ud0h d;i+oh d0;？o00 001 2@ e ; i + he;io00 0020 0h e ;【X7！h e ; i]i + he;i0 0O1h e ; i + hx：e;ih x：e; i +o hx：hx;i+ohe00;00i00h e ; i + he;i0 0（x）= he;iNBE2 TermEnv：：= VNx*TermEnv带下划线的应用程序的子项是严格平行的，不能相互干扰。引理3.8如果我们序列化的相关规则！收件人：nD是！ 正常C！c0nnd@c！d@c0nNBE！n （上至jj）是一个有效的，规范化1-策略！ 在JJ。证据关系是的最左归约策略！直到jj，结果由[3，定理13.2.2]得出。2从证明中，我们可以立即得出以下结论。提案3.9（通过评估非类型化术语进行规范化）NbE\works”用于任何未键入的- 术语a- 类型的正常形式。NbE\works”用于任何未键入的- 术语，- 等于一个e 2证据对于第一个，[3，定理13.2.2]适用于非类型项。 第二个是从第一个（事实上，它相当于它）的主题减少！主语归约既有缩小又有扩大。24NBE机器我们现在呈现实现NbE的环境机器。可以为NbE定义类似的机器。该机器是一个环境机器，因此从不执行（全边）替换，而只实例化不在上划线抽
