阶泛函纯型系统的理论计算机科学电子笔记

1620 0 0000理论计算机科学电子笔记76（2002）网址：http://www.elsevier.nl/locate/entcs/volume76.html16页阶泛函纯型系统FranciscoGutierreza;1;2BlasRuiza;1;3a马拉加大学语言和计算机科学系校园Teatinos 29071，马拉加。西班牙摘要我们研究一类纯类型系统是弱于功能的，其特征在于分配的可能性，在一个非平凡的方式，一个整数到任何类型的术语在一个上下文中：它的顺序@a。我们描述了顺序函数的一些应用。其中一个重要的是研究一类系统中的句法依赖，- 立方体。关键词：带类型的lambda演算，纯类型系统，截断消去。1引言纯类型系统（PTS）[10，1]的主要优点是它们提供了一个研究依赖类型系统和一大类类型演算性质的灵活而通用的框架。PTS由其规格定义，即， 元组S =（S; A; R），其中S是一组常数或排序（s;2; ：2S ），ASS是一组公理，RSSS是一组规则（让 s1：s22A代表（s1;s2）2A，让s1：s2：s32R代表（s1;s2;s3）2R）。 导出a：A的概念是由图1所示的归纳系统定义的。1.一、让我们回想一下，PTS是泛函的，如果关系A和R是函数：2：s;2：s 2 A）s=s;和2：4：s;2：4：s 2 R）s=s：众所周知，功能PTS验证UT（类型的唯一性）属性：`a：A; a：A）A=A：1 本研究得到了项目TIC 2001 -2705-C 03 -02的部分支持。2 电子邮件地址：pacog@lcc.uma.es3 电子邮件地址：blas@lcc.uma.es在CC BY-NC-ND许可下开放访问。古铁雷斯和鲁伊斯163（ax）‘2：4‘A：;x：A`x：A`b：B`A：s;x：A`b：B`A：s1;x：A`B：s2的x：A：B：s3`f：x：A：二比四2A（var）X62（弱）b2 S[V; x62（）下一页s1：s2：s3 2R（apl）（）下一页B（）下一页A=a0级古铁雷斯和鲁伊斯164F`a：A`fa：F[x：=a]`x：A：B：s;x：A`b：`x：A：b：x：A：B0 `a：A`A：s0`a：A图1. PTS的推理规则反过来，如果UT成立，则S是功能系统4。因此，UT仅由功能PTS验证。函数性可以用来简化许多PTS证明，否则会很难，例如，凝聚性质。UT在一些开放问题的特定实例的证明中也非常有用，如EP（扩展延迟问题）[16]，Barendregt-Geuvers-Klop conjec- ture [3]和cut elimination[13]。古铁雷斯和鲁伊斯165虽然文献中最有趣的系统是泛函5，但非泛函系统的理论性质也得到了研究[20]。在这项工作中，我们研究几乎功能系统，其特征在于以非平凡的方式将整数分配给任何排序的可能性：定义1.1（序函数）一个系统是O函数的，如果有一个4 我们假设R中的三元组是有用的，即，对于每个三元组，存在满足（）规则的前提的项这不是一个限制，因为在删除无用的规则后，获得了相同的关系5 一些作者，包括我们自己，认为函数系统更有趣，因为UT属性。古铁雷斯和鲁伊斯166@常数6 = 0，应用S！ Z that veri es：（a）s：s0 2A ） @s=+@s0;以及（b） s：s：s;s0 ：s0 ：s0 2R^（@s;@s）=（@s0;@s0））@s=@s0：1 2 31 2 31 21 233O函数系统的本质特性是函数@可以扩展到可类型化的术语和上下文，使得：（1）`a：A） @a= +@A：因此，types的@-唯一性成立：`a：A;a：A0 ）@A=@A0.@这被称为订单功能。我们研究的大多数系统都是O泛函的，如[1]（page 214）中所描述的大多数系统，以及具有单位元的构造演算的一些推广（Ecc[1 5]和CC！[14]）。我们的序定义推广了[1，9]中描述的度的概念。这些作者为可类型和不可类型引入了]度- 立方项，使得：（2）`a：A） ]a=]A1：这一特殊序的存在性与语境无关，它通过两个性质得以缓解：（i）everys1 ：s2 ：s3 2R规则满足s2 =s3，且(ii) 带注释的变量与排序的使用（即，SX）和以下的修饰：（var）和（weak）规则提供了一个较小的推理关系va（见定理4.1前的注）。 以这种方式，每个变量的顺序信息反映在变量本身中：]（sx）=]s2，并且该信息不必从上下文获得。注释变量在文献中很常见：[6，1，9，3]。虽然一些作者[20，17]更喜欢纯stile，但为了获得性质（1），必须包括上下文。 我们提出了一个概念的顺序，这是更一般和更宽松的系统条件。另外，我们发现它很有前途。下面的分类将对本文的其余部分有用定义1.2让我们考虑一个> 0的 O函数PTS。该系统是：(i) 序注入，如果（@s;@s）=（@s0;@s0））@s=@s0。1 31 3 22(ii) 半代数非依赖，如果@s 3=@s 2。(iii) 代数非依赖，如果@s 3=@s 2@s 1.(iv) 三阶，如果@s3=@s2=@s1。（v）有序l，若（@s1;@s2）=（@2;@4））2：4： 2R.对于每对规则s：s：s;s0 ：s0 ：s0 2R。1 2 31 2 3为了简化说明，我们将使用O-内射、O-满、半代数和代数系统。古铁雷斯和鲁伊斯167每个内射和O泛函PTS都是O内射的。因此，在-cube中的所有系统都是O内射的，也是U和HOL。很容易证明O内射系统的序函数不依赖于上下文;从而导致性质（2）的推广。从上面的定义可以看出，在立方体中，左边的系统是代数的，而角点是代数的。还有！有三个命令。由于半满PTS [21]的研究对于其在类型检查中的应用是有趣的，我们看到O满推广了它们，并且也允许简单的类型检查算法。多维数据集中的所有系统都是O满的。序函数使我们可以把一个很难用代数方法来描述的问题--句法非依赖性--的研究变得微不足道我们工作的一个基本结果出现在定理4.6中：在代数系统中，依赖性是非常有限的，并且s-型不依赖于s-项7：B：是的。`N：：s）N 6 B：证明这个推论并不容易，我们不知道有任何证明像我们这样特别地，如果系统是三阶的，那么它是独立的：`z：A：B：）z62FV（B）。这是在案件！还有！角落。利用这一结果，得到了这些系统的一个非常有趣的性质：割消[19，13，4]。我们的序概念的其他应用在第4节中揭示。2PTS的描述和性质在本节中，我们介绍PTS及其主要属性。更深入的研究，我们参考[10，1，20，18]。考虑变量V（x; y;：：2 V）的无限集合和变量或排序S（s;2; ： ：2S）的集合，PTS的项的集合T被归纳地定义为：a2 V[S] a2 T;A; C; a;b2 T ）a b; x：A：b;x：A：C 2 T：我们表示的- 减少和= 产生的平等。- 范式的集合表示为-nf，FV（a）表示自由变量的集合。A[x：=B]通常表示替换。这是Church-Rosser（CR）。a表示a的-正规形式。一上下文是一个排序序列x：A;：;x：A. 我们表示8 x：：1 1n n：i一个2，0 = 8x [x：A 2）x：A 20]，Var（）=fx;：;x g;i1n6 即：使用对规则集的直接检查7 我们用`a：表示9A2T [`a：A]和`a：：s代表9A2T[`a：A^ `A：s]。8：=是定义符号。古铁雷斯和鲁伊斯168：x2 =x：2 Var（）; FV（）=S1inFV（A i）.PTS由其规格定义，即，元组S=（S; A; R），其中S是一组常数或排序（s;2; ：2S），ASS是一组公理，R SS S是一组规则。推导的概念'a：A是由图1所示的归纳系统定义的。如果9 c; C2 T[ `c：C]，我们说这是一个法律语境（用`表示）。让我们回忆一下PTS的几个基本性质：引理2.1（基本性质）如果`c：C，则：(i) FV（c：C）Var（）; Var（）的变量是不同的。(ii) p： q2 A）` p： q：(iii) y：D2 ）`y： D：（四）类型的正确性：`c： C^ C62S）9 s2 S [` C： s]：在一个蕴涵的右边或在一个规则的下半部分的一个自由宾语，被9隐式量化例如，类型的正确性属性可以重写为`c：C^C62S）`C：s。我们还需要PTS的典型性质：主题归约（S），预测归约（P），替换引理（Sbs）和稀疏引理（T hnng）：`a： A（S）a`a0：Aa 0;（P）`a：AAa：A0A0;（Sbs）`d：D;y：D;`c：C; [y：=d]` c[ y：= d]： C[ y：=d]; （Thnng）`b：B``b：B：我们还使用在[1]中描述的（生成）引理5： 2： 13。3序函数构造文献中的大多数系统是O功能的。例如，-立方体，U，HOL，AUT68，AUT QE;PAL|所有这些都在[1]（第21页）中描述。|以及构造演算论域的一些推广，如Ecc[1 5]和CC！[14]是O函数系统。另一方面，系统是非O函数的，因为：公理要求= 0。对于其他PTS，定义1.1的条件不成立。例如，如果Af：2;：4;2：4g（见图1），2：左）。 这个系统也不起作用。类似地，由yA=f：2;2：4;r：4g和R=f：2：4;：r：rg构成的系统是泛函的，但不是O泛函的，尽管公理的条件成立（见图2：右）。如果2：s;20：s2A）2=20 ， 则 系 统相 对 于公 理 是 单 射 的;最后一个例子相对于公理不是单射的。古铁雷斯和鲁伊斯169n1=为v四四，2sJ、、、、2sJ、、、、、、，vzRz？Jz？图2. 对应于两个公理集的图。一个循环是一系列公理，如ke21：22; ：;2：2。循环的存在使定义1.1（a）失败。我们可以得出以下结论：引理3.1任何函数系统，相对于公理的内射，没有- out循环，并且有一个排序的集合是O泛函的。一行是公理f s i：s i+1g的非循环集合。在引理的条件下，公理图是（nite或in nite）公理线的集合 因此，我们可以从定义1.1中列举出保持（a）的常数，另外，y，@s=@s0 （）s=s0. 有了这个顺序，定义中的prop_y（b）就微不足道了。2下面的引理将被用来为每一项定义阶函数的扩张。引理3.2对于每个PTSO泛函：（i）`a：：s^`a：：s0 ）@s=@s0：（ii）`a：s^`a：A：s0）@s=+@s0：（iii）`a：A：s^`a：A0 ：s0 ）@s=@s0：让我们回想一下，在[20]中，PTS的项的集合可以分为两个不相交的类，Tv和Ts，归纳地定义为：x2Tv;b2Tv） b c;x：A：b2Tv;2;x：A：B2Ts;b2Ts）bc;x：A：b2Ts;使得a：A;a：A0 ）80）@ a2+！;（二）< 0）2+@a！;当我的f@sj s2Sg和！最大f@sj s2Sg.证明它遵循类型正确性和定理3.4。2因此，在-cube中，取f=1和@2=3，取f0;1;2;3 g中的值可以得到一个阶。4序函数4.1序内射系统继O泛函系统之后，O内射系统是本文研究的较弱的一类。使用带注释的变量可以证明顺序不依赖于上下文。让我们回顾一下，为了使用带注释的变量（即：sx），则（var）和（weak）推理规则都必须古铁雷斯和鲁伊斯1720 00VAVA00000 0033的VA2VAVA312修改为：瓦 答：（varva）;（weakva）瓦 b：B`va 答：：;sx：A`sx：A;sx：A`b：B然后， 推理关系小于“关系”，即s a y：瓦“的意思。定理4.1具有注释变量的任何O内射PTS证明：瓦 m：M^`va m：M）@M=@0M ^@m=@0m：证明由于@ m= +@ M，所以证明第一个等式是必要的。通过对`va进行归纳， m：M的推导，其中每种情况都由定理3.4、生成引理和IH得出。此外，如果最后一个规则是（varv a），则还使用以下属性：（4）`sx：M）`sx：Q：s：具体来说，为了证明应用情况，我们使用O内射性;然后我们考虑：（五）瓦 f：x：A：F`va a：A瓦 fa：F[x：=a]其中MF [x：= a]。 从0vfa：M0，通过应用生成引理，我们得到（6）`va f：x：A：F;（7）`va a：A;（8）M= F[ x：= a]：通过应用rst类型正确性性质和生成引理，我们得到瓦 x：A：F：s;0`x：A0：F0 ：s0;瓦 A：s1;; x：A`va F：s2s1：s2：s32R;0`a0级 ：s0;0; x：A0的F0 ：s0s0 ：s0 ：s02 R：VA1va21 2 3| ByIH,from(5)and(6)weobtainthat@( x:A:F)=@0( x:A0:F0)因此，@s3=@s。0| Also,byIH,from(5)and(7),weobtainthat@A=@0A0,andhence,@s 1 =@s。0此外，由于系统是O内射的，则@s2=@s。0通过替换引理（Sbs），我们知道， F[x：=a]：s2，0F0[x：=a]：s0，且b是可获得的，@（F[ x：= a]）=@0（F0[x：=a]）。我们只需要观察到@M@（F[ x：= a]）=@0（F0[ x：= a]）=@0M0VA古铁雷斯和鲁伊斯173伐伐伐伐其中最后一个等式由定理3.4（iii）得到。2定理4.1中的O内射性条件是必不可少的，如下面的例子所示：例4.2如果A=f？ ：4;4：2g且R=f：4：2;：：2g则系统不是O内射的。此外，本发明还提供了一种方法，2f：x：4：？ “ 2f？ ：？2f：x：4：4f？ ：4|{z}|{z}0可以导出，但是@（f？）=+@？ 6 =+@4=@0（f？），定理4.1的推论不成立。4.2半代数系统在本节中，我们通过推广[1，9]中的定义来建立项的阶与其次数定义4.3对于每一个带有注释变量的半代数系统，]并且= 1，我们定义了度函数！Z为：]s=@s;]（s x）=]s二、]（x： A：B）=]（ x： A：B）=]（ B A）=]B：]让我们观察到，对于立方中的系统，取@2=3，我们得到！f0; 1; 2; 3g.阶和度由以下引理联系起来：引理4.4对于每一个半代数系统，特别是立方系统：㈠`va a：A）]a=@a：㈡`va A：A）]a=]A1：证明As@s =]s，（ii）由类型正确性（i）和定理3.4得出。我们现在通过对a的结构归纳来证明（i）。 如果a是一个变量，那么，从（4），我们得到`sx：Q：s，并且作为` `，那么` sx：Q：s;因此，由定理3.4，@（sx）=@s2（让我们回忆一下，=1），并且由应用定义4.3，我们得到@（sx）=]（sx）。在其余情况下，我们应用IH，定义4.3和以下性质：@（x：A：B）=@;x：A（B）;@（x：A：b）=@;x：A（b）;@（fa）=@（f），这是用生成引理和定理3.4证明的。2古铁雷斯和鲁伊斯174让我们观察一下，即使这个术语没有很好地键入，也可以定义。读者可以检查引理4.4的证明更一般，优雅[1]中所描述的一个类似的立方体。为了结束这一节，让我们展示一个有趣的应用程序，在O全系统中进行类型检查：在这些系统中，抽象规则可以非常简单。ed.引理4.5考虑任何带注释变量的O全半代数PTS然后，（）规则可以替换为以下规则：关于A：s1;x：A关于B：B8>> s1：p：2R;]B=]p 1个;关于x：A：b：x：A：B：>B2S）B：2A：证明它由引理4.4得出。2与传统的'sf（semifull）系统[16，2，21]相比，'of系统的优点在于，'of对于非半满系统是正确和完全的此外，副条件减少了类型检查过程中使用的规则数量。4.3代数系统下面的定理证明了代数系统的非相依命名，并推广了[3]（注2.48）中描述的一个类似结果：定理4.6在任何代数系统中，(i) NB^`N：;B：）@ N@B（单调性）。（二）`N： ：s^`B：s）N 6 B.因此，s类型不依赖于s项.因此，如果系统是三阶的，那么它是独立的：（ii0）`z：A：B：）z62FV（B）.让我们记住s 1：s 2：s 3 2 R）@s 3 =@s 2@s 1.使用生成引理，对于类型良好的项，很容易证明，@（v： V：W）@ V@;v：VW;@（v：V：w）@V@;v：Vw; （V W）@ V;@W第 一 组 不 等 式 需 要 @s1;@s2@s3; 第 二 个 @s3@s2;1 +@s3@s1; 第 三 个@s2@s3;@s2@s1;我们需要@s2=@s3@s1。使用上述不等式，我们可以通过B上的结构归纳法容易地证明（i）：古铁雷斯和鲁伊斯175| Bz_B2. 然后是NB。|BV：V：W。如果NV，通过IH，我们有@ N@V@（v：V：W）。 如果N W;由定理3.4（ii），@ N =@;v：VN;由IH，我们得到@;v：VN@; v：VW@（v：V：W）。|Bv：V：w.如果NV，通过IH，我们有@ N@V@（v：V：w）。如果N w;@ N =@;v：V N;由IH得到@;v：V N @;v：V w @（v：V：w）。|BV W. 如果NV，通过IH，我们有@ N@V@（VW）。 如果N W，通过IH我们得到N W（V W）。为了证明（ii），让我们观察到，如果N： ：s和B：s，则（根据定理3.4（i））@ N >@ B成立，我们只需应用（i）。让我们现在来讨论（ii0）。 Let; z：A. 若z：A：B：，则z：A;A：s1; B：s2;则由于系统是三阶系统，@A=@B，因此z>@ B;由（i），z 62 FV（B）.2不幸的是，有些代数系统是依赖系统，例如2。4.4无割序列演算与割消元PTS[13，11]的无割演算的概念受到Gentzen [7]的自然直觉主义逻辑N和无割演算L之间的对应关系的启发，除了它的中心定理：L中的任何导出都可以在不使用割规则的情况下获得，这一结果称为割消元。因此，在无剪切PTS中，我们删除了（apl）规则来键入应用程序，因为它消除了右侧的连接词（见图1）。相反，我们将使用下面的（！left）来自序列演算的规则（K`a：A;x：S;`c：C）;[x：= y a]` c[ x：= y a]： C[ x：=y a]8y：z：A：B2;SB[ z：=a]：文[13]证明了所得到的新系统Kcf是正确的。如果我们添加（剪切）规则，（切）`a：A;x：A`b：B;`b[ x：= a]： B[ x：= a]得到的新系统K与原系统等价[x：= ya]替换算子保持范式（B; a2-nf）B[x：=ya]），因此，系统提供标准化的文本、对照文本和术语。 割消法意味着任何推导`m：Mwith m; M;normalised，可以在不使用（ cut）规则的情况下获得，即：c; C2-nf^`K c：C） `Kcf c：C：（CE）：古铁雷斯和鲁伊斯176KKKKK阶函数在代数系统中的主要应用是：定理4.7每一个正规化的非独立系统都是割消去.证明（略）首先我们证明以下规则的正确性：（aplV ar） `Kcf a：A`Kcf y：z：A：B：`Kcf y a：B[z：=a]让我们假设一下。那么，由定理4.6（i i0），z62FV（B）。 通过生成引理（在K cf中），我们得到;z：A `cf B：s，并通过应用K cf中的凝聚性质，我们得到`cfB：s。因此，x：B`cfx：B，并且通过（K）规则，我们得到`Kcf x[x：=ya]：B.使用（aplV ar）证明以下规则并不困难（aplN）`Kcf fa：B[z：=a]f a 2-nf：因为系统是归一化的，所以很容易证明割消（CE）等价于以下属性：; c2-nf^`c：C） `cf c：C：（CE0）（CE0）的推广不是用（aplN）定理推导出来的.25结论、相关工作和未来工作PTSs现在是一个有前途的研究领域吗？我们认为这个问题的答案是肯定的，许多研究已经在应用中。我 们 已 经 表 明 ， 序 的 概 念 丰 富 了 工 具 箱 ， 提 供 优 雅 的 证 明 ，diligencult性质。其他作者已经研究了不太一般的序概念。例如，在[1，9]中，度的概念本质上是用来证明立方系统的强正规化。我们相信我们的@函数可以以类似的方式使用。在[12]中，我们证明了任何O泛函PTS都可以投影到泛函PTS（它的核）中，并且这种投影是态射。由此得到一个基本结果：任何具有正规化核的O泛函PTS都满足EP（expansion updating）性质.这一结果将文[5]中的结果推广到泛函正规化系统。9例如，让我们引用基于PTS的新编程语言的定义和实现，例如最近在乌得勒支大学开发的一种。 cs.uu.nl/~johanj/MSc/jwroorda`Kcf a：A`Kcf f：z：A：B古铁雷斯和鲁伊斯177也许与我们最接近的非依赖性概念是[3]中的概念。作者使用带注释变量的PTS和`va 系统 他们介绍了持久的，分层的，和广义的非依赖系统的概念。一个系统是持久的[3]（定义2.12），如果它是函数的，对于公理是单射的，并且它的所有规则都有s1：s2：s2的形式。一个系统是分层的[3]（定义2.19），如果它不包含常数的无穷序列，使得s1@s0。因此，一个任意非相依的广义系统对任何规则都成立@s3 =@s2@s1，所以它是定义1.2意义下的代数系统，定理4.6也成立。此外，我们已经检查了[3]中使用的技术可以用于代数系统，为了方便修改结果的条件。总之，阶的概念可以用来简化BGK猜想的证明，即使不使用功能。引用[1] 巴伦德雷格特H 。P. ， Lambda Calculi with Types ，in：S. Abramsky，D.Gabbay和T. S. Maibaum ，编辑，Handbook of Logic in Computer Science ，Oxford University Press，1992 pp. 117{309.[2] Barthe，G.，纯型系统的半全闭包，在：L. B.例如，编辑，MFCS'98，LNCS1450（1998），pp. 316{325.[3] Barthe，G.，J. Hatterns和M. S rensen，Weak normalization implies strongnormalization in Generalized Non-dependent Pure Type Systems，TheoreticalComputer Science269（2001），pp. 317{[4] Barthe ， G. 和 B. Ruiz ， Tipos Principales y Cierre Semi-completo paraSistemas de Tipos Puros Extendidos ， in ： 2001 Joint Conference onDeclarativeProgramming（APPIA-GULP-PRODE'01），Evora，Portugal，2001，pp. 149{163.[5] Barthe，G.和B. C. Ruiz，通过半完全关闭实现PTS正常化的扩展延迟，6月，即将出版（2001）。古铁雷斯和鲁伊斯178[6] Berardi，S.，类型依赖与构造数学都灵大学数学系毕业论文（1990年）。[7] 根岑，G.，Untersuchungenu在数学上，这是一个L ogischeSchliessen。《明史》卷39（1935年），页39。176，{210，405 {431，翻译在[8]。[8] Gentzen，G.，逻辑演绎研究，M。Szabo，editor，The Collected Papers ofGerhard Gentzen，North-Holland，1969 pp. 68{131.[9] Geuvers，H.，逻辑与类型系统（Logics and Type Systems）论文，计算机科学研究所，Katholieke Universiteit Nijmegen（1993年）。[10] Geuvers，H.和M. Nederhof，构造演算的强规范化的模块化证明，函数编程杂志1（1991），pp。15{189.[11] Gutierrez，F.和B. C. Ruiz，A Cut Free Sequent Calculus for Pure TypeSystems ， Gentzen/Kleene 的 结 构 规 则 ， in ： International Workshop onLogic Based Program Development and Transformation（LOPSTR'02），September 17-20，Madrid，Spain，LNCS（to appear）（2002），http://polaris.lcc.uma。es/vbla s/pu bli caciones/.[12] Gutierrez，F.和B. C. Ruiz，PTS的功能内核，Tech. 报告IT xx/02，部门 deLenguajes y Ciencias de la Computaci on，Universidad de M alaga（Spain）（2002）.[13] Gutierrez，F.和B. C. Ruiz，纯类型系统的序列演算，Tech。报告06/02 ， 部 门 de Lenguajes y Ciencias de la Computaci on ， UniversidaddeMalaga （ Spain ） （ 2002 ） ， http://polaris.lcc.uma.es/vblas/publicaciones/.[14] 哈珀河和R. Pollack ，Type Checking with Universe，Theoretical ComputerScience89（1991），pp.107{136.[15] 罗志\An Extended Calculus of Constructions，”Ph.D.论文，爱丁堡大学（1990年）。[16] 波 尔 ， E. ， Expansion Postponement for Normalising Pure Type Systems ，Journal of Functional Programming8（1998），pp. 89{96.[17] 鲁伊斯湾 C.的方法， 凝聚引理在纯型系统与宇宙，在：A. M. Haeberer ， 编 辑 ， 第 七 届 国 际 代 数 方 法 论 和 软 件 技 术 会 议（AMAST'98）会议记录，LNCS1548（1999），pp. 422{437.[18] 鲁伊斯湾C.的方法，“Sistemas de Tipos Puros con Universos”，博士马拉加大学论文（1999年）。[19] 鲁伊斯湾C.的方法，具有论域的纯类型系统的扩展延迟问题，第九届国际函 数 与 逻 辑 程 序 设 计 研 讨 会 （ WFLP'2000 ） ， Dpto 。 de SistemasInformaticos y Computaci on ， Technical University of Valencia （ Tech.Rep.），2000年9月28日至30日，西班牙贝尼卡西姆。古铁雷斯和鲁伊斯179[20] van Bentham Jutting，L.，Typing in Pure Type Systems，Information andComputation105（1993），pp. 30{41.[21] van Bentham Jutting，L.，McKinna和R. Pollack，Checking Algorithms forPure Type Systems，in：H. Barendregt和T. Nipkow，编辑，证明和程序的类型：国际研讨会类型'93，在计算机科学讲义（1994）中的第806页。19{61.