Type：Type无域纯类型系统的部分类型检测算法分析

∗理论计算机科学电子笔记229（5）（2011）3-17www.elsevier.com/locate/entcsType：Type的部分类型检测算法Andreas Abel安德烈亚斯·阿贝尔1，3德国慕尼黑路德维希-马克西米利安大学信息学院，Oettingenstraße67，D-80538，慕尼黑Thorsten Altenkirch托尔斯滕·阿尔滕基希1，2，4诺丁汉大学计算机科学学院Jubilee Campus，Wollaton Road，诺丁汉NG8 1BB，英国摘要分析了不一致无域纯类型系统Type：Type（λ）的部分类型检测算法。我们表明，该算法是健全的，部分完成使用共归纳specification的算法平等。这意味着算法只会因为存在发散计算而发散，特别是它会对所有可输入的项终止关键词：依赖类型，纯类型系统，类型检查，类型：类型1引言本文分析并实现了一个类似于[6]的不一致理论Type：Type（λ）的部分类型检测算法。这是一个无域纯类型系统的实例[4]，并且似乎可以将其扩展到任何函数纯类型系统（PTS）。这项工作的动机是为支持一般递归的依赖类型编程语言（如Augustsson的Cayenne [ 3 ]）实现类型检查器 我们使用Type：Type作为测试用例对于具有依赖类型的语言，避免了完整编程语言的语法复杂性。1由FP6 IST协调行动类型（510996）支持的研究。2研究由EPSRC资助的Observational Equity For Dependently Typed Programming(EP/C512022/1）3电子邮件：andreas. ifi.lmu.de4电子邮件地址：txa@cs.nott.ac.uk1571-0661 © 2011 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2011.02.0134A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）我们的主要贡献是，我们表明健全和部分完整性。所谓部分完全性，我们的意思是，如果算法发散，它只会是因为程序或其类型，或它们的组合，包含一些循环;发散，因为算法中的错误被排除在外。因此，对于给定的PTS，建立终止性足以表明算法是完备的，并且确实决定了类型关系。我们相信这是一种很有前途的方法，因为它意味着我们可以建立独立于终止的类型化算法的基本语法属性特别地，我们给出了算法类型化规则Γt惠A，在上下文中读为Γ，项t检查类型A，有两个版本：使用归纳等式的Γμt惠A，和使用共归纳等式的Γvt惠A 该算法的归纳版本被证明是健全的，而共归纳版本被证明是完整的。我们通 过无类型的β-转换=β给出了 类型相等的Type ： Type （type is atype）的算法。我们的证明主要依赖于函数类型构造函数的内射性：A。这是β-约化的结果。类型检查算法计算类型的弱头范式（whnf）。这是足够的，因为β-还原是标准化的。标准化可以包含在口号中，如果一个术语β-归约为whnf，那么弱头归约就等于sameshape的whnf。 例如，如果t−→ <$βλxu，则t−→<$wλxu<$，其中u<$− → <$βu。 因此，这变成：如果t=<$βλxu，则t−→<$wλxu<$，其中u<$=<$βu。相关工作这里提出的算法基本上是Co-quand算法的现代重新实现我们只考虑β-等式的事实简化了处理--沿着[9，8]的路线对βη-等式的句法研究留给未来的工作。第一作者[1]最近的工作也是针对βη-等式，但依赖于归一化。概述我们首先介绍Type：Type并验证一些基本属性。接下来，我们指定的关系形式的类型检查算法，并显示的归纳类型检查关系的可靠性。然后利用共归纳建立共归纳关系的完备性。最后，我们提出了一个实现的算法在Haskell中，并讨论进一步扩展目前的工作。2Type：TypeCurry风格的λ是一个域自由的纯类型系统[5]，只有一个排序类型，公理类型：类型和规则（类型，类型，类型）。A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）5语法和纯类型系统一样，只有一个语法类Expression用于项t、u、类型A、B、C和排序s。元变量x在变量标识符的有限集合中的可数范围内。实验3 t，u，A，B，C，s：：= x |λxt |tu |A. B|类型表达式Ne3 n：：= x |nu中性项Cxt3 Γ：：= 0|Γ，x：A类型上下文我们识别直到α转换的表达式。上下文Γ只是一个对x：A的列表，但它也被认为是从变量到类型的有限映射。 因此，在一个上下文中，任何变量都不能被赋予两种类型在t中用u替换x的避免捕获的替换记为t[u/x]。一步β-约化记为y−→β，其逆传递闭包记为y−→β，其逆传递对称闭包记为= β.因此，t = βt<$当且仅当存在某个u，且t−→ <$βu和t<$− → <$βu。根据以下规则给出了水头降低量（λxt）u u1. u n−→wt [u/x] u1. un对于n0。它的rexexi ve-transiti v e闭包记为−→w。 （Ty peable）whnfs是中性项n，抽象λxt，函数类型λ x：A. B，以及常量Type。下面我们用一个向量表示法写t u1. 就像你一样。命题2.1（β-还原的标准化[11]）(i) 如果t−→，则t−→。(ii) 如果t−→ <$βλxu<$$>，则t−→ <$wλxu和u−→<$βu<$。(iii) 如果C −→<$β<$x：A<$。 B→C −→A→W→x：A。 B和A−→<$βA<$和B−→ <$βB<$。(iv) 如果C −→βType，则C −→wType。利用连续性，−→β可以由abo v e状态项中的y = β代替。 特别地，我们可以从推论中得出以下推论：推论2.2（λ的内射性）如果λ x：A。 B = βx：A。 B则A = βA且B = βBλ的推理规则类型A的项t由判断Γt：A给出，它与良构上下文的判断Γok 如果J是判断，我们写D：：J来表示D是J的导子。良构上下文cXT-空吉吉诺克cXT-EXTΓA：类型r，x：A_（？）6A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）类型：A型FΓ-轴类型：类型HYPOΓok（x：A）∈ΓΓx：AFUN-FΓ，x：AB：类型A. B：类型FUN-Ir，x：A，t：BΓ λxt：λ x：A. BFUN-EΓt：x：A. Bu：Ar=0：B[u/x]cCONVrt：A A=βB联系我们判断Γt：A蕴含Γok，这很容易检验。下面的反演引理与内射性无关引理2.3（类型反转）（i）如果D：：r =Type：C，则C = βType。(ii) 如果D：：Γ πx：A。 B：C则C =β型和Γ，x：A <$B：型。(iii) 如果D：：r = x：C，则C=βr（x）。(iv) 如果D：：Γλxt：C，则C=βλx：A。B和Γ，x：A，t：B。(v) 如果D：：Γ tu：C，则Γ t：x：A。 B，其中Γ u：A和C =βB[u/x]。证据 通过对D.Q类型化具有β的弱化、替换和主语归约等通常的性质。证据是标准的。3一种类型检测算法强类型函数程序的最基本格式是一系列非递归声明，形式为x：A = t，表示类型为A的标识符x定义为t项。在声明列表中，后面的声明可能依赖于前面声明的标识符的类型和定义。可以合理地假设t和A都没有β-兑换，但是在类型检查期间，兑换将在类型中发生。我们使用算法类型检查的双向表示，使用ΓtA表示t的类型A可以被推断，使用Γt惠A表示t可以被检查为具有类型A。一个程序的类型检查首先要确保A是一个格式良好的类型，写为ΓAType，然后检查t是类型A，写为Γt惠A，将声明x：A=t添加到全局环境中，然后继续下一个声明。A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）7⇒⇒类型推断我不知道。 （输入：格式良好的T，中性的T和正常的β。 输出量： A，其中r为t：A。）INF-VARrxr（x）INF-FUN-EΓtCC −→wx：A.Bu惠AΓtuB[u/x]推断型类型类型INF-FUN-FΓ <$A<$ss−→wTypeΓ，x：A<$B <$s<$s<$−→wTypeA. B型当t的推断类型没有whnf时，应用程序tu的类型推断发散这里我们实际上，任何推断类型在使用时都必须简化为whnf。类型检查我不喜欢A. （输入：Γ，A，其中ΓA：类型，t β-正态。 输出：无。）cHK-INFRt AAA免费WiFit不是λcHK-FUN-IC −→wx：A. BΓ， x：A不便宜B关于我们规则cHK-RED适用于当我们想要检查一个抽象是否存在于whnf中。检查没有whnf发散的类型。数学平等► A A。如果项t的类型被声明为A，但被推断为A（规则c HK-INF），我们需要确保A和A是β-相等的。下面的规则指定了一种交替使用弱头标准化（Aq-RED-L和A q-RED-R）和结构比较（其他规则）的算法。Aq-RED-Lt1−→wt <$1 <$t<$1<$t2► t1t 2Aq-RED-Rt2−→wt<$2<$t1<$t <$2► t1t2Aq-VAR► xxAq-APP∗n∼n∗∗u∼u∗► 努辛乌河Aq-λtt► λxtλxtAq型产品型号Aq-FUNA► A. B. A. B组8A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）∗4健全性类型检查器的终止运行对应于上述算法规则系统中的有限派生。因此，当我们想推理算法是合理的时，i。例如，它只接受良好类型的术语，我们需要考虑归纳算法等式和算法类型化的Γμt惠/A，它指的是归纳等式。引理4.1（算法等式的合理性）D：：μtt意味着t=βt.证据 通过对D.Q定理4.2（双向类型检查的可靠性）（i）如果D：：Γ<$μtA和Γok则Γt：A.(ii) 若D：：Γ μt惠C且Γ C：Type，则Γ t：C。证据同时对D.同样微不足道。Q5完整性由于λ的类型检查是不可判定的，我们算法的一个适当的完备性结果是：如果β-正规t是A类型，则针对A的检查t不会永远失败。I.例如，该算法可能发散或成功，但不报告错误。我们通过考虑算法等式的共归纳版本来使其形式化。例如，我们允许无限导子，以及一种算法类型的版本，它涉及到共归纳等式。下面我们使用共归纳技术证明了（第2节）声明系统中的类型和等式的有限导子映射到（第3节）算法系统中的可能无限首先我们证明如果两项t1和t2是β-相等的，则D：：vt1<$t2。在t1<$Ω的情况下：=（λx. x x）（λx. x x），导数D只是q-RED-L的无限次重复。请注意，相同的推导显示了对于任意项t的<$ν Ω <$t，因此，以下引理的对位不成立：引理5.1（算法等式的如果t1=βt2，则τνt1τt2.证据 通过共同归纳。 我们考虑以下情况：• 情况t1−→wt1。然后，根据规则A-Q- red - l，使用共归纳假设，遵循规则a-q-RED- L，遵循规则A-Q- RED-l。• 情况t2−→wt2。类似的。在其余的情况下，t1和t2是whnf。A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）9∗• 情况t1≠Type=βt2。 因此，t2−→βType。 如果t2是一个whnf，t2就不一样了。目标后面跟着一个q型.• 案例t1中，X：A1。 B1=βt2。 因此，t2= 0.2。 其中A1=βA2，B1=βB2。目标是 通 过 一 个 q- 函 数 来 实 现 的 ， 其 中 有 共 归 纳 的 假 设 <$vA1<$A2 和<$vB1<$B2。其他案件也是类似的。Q接下来，我们展示了对于一个类型良好且可检查的（i。例如，β-正态）项t存在一个算法类型化推导，其中可能有算法等式的无限推导。定理5.2（类型检验的完备性）设t β-正规，且Γt：C.(i) 如果t是中性的，则Γ νt <$A且A = βC。(ii) 无论如何，我会给C.证据 同时在t上进行归纳。• 我的案子。通过反演C=β Γ（x）。我们有由INF-VAR得到的Γ<$νx<$Γ（x）。第二个目标由引理5.1<$νΓ（x）<$C得出。• 你的情况。通过反演，得到了Γ n：λx：A. B，其中Γ u：A和C=βB[u/x]。 通过归纳假设，得到了Γνn<$D，其中D=β<$x：A. B.通过一致性和标准化，D−→ 其中A=βA<$且B=βB<$。根据转换规则，由第二归纳假设，我们得到了Γνu 惠 A ， 因 此 ， 通 过 推 论 ， 我 们 可 以 得 出 ΓνnuB[u/x ] ， 其 中B[u/x]=βB[u/x]=βC.这就意味着第二个目标是T惠C。• 案例类型。倒置C=β型。我们以INF-类型作为结论.• 病例t检验：A. B.通过反演，C =β型，而Γ，x：A <$B：型则蕴含着Γ<$A：型。根据第一个归纳假设，我们有s = β型的Γ π νAπ。通过第二归纳假设，得到了Γ，x：A <$νB：s <$，其中s<$=β型。由于通过连续性和标准化s−→nwType和sn−→nwType，我们得出结论为inf-fun-F。• 案件tλxt。通过反演，C=β<$x：A。B和Γ，x：A ≠ X：B.由于C −→wx：A。其中A=βA，B=βB，其中有一个r， x：At：B。 通过归纳假设Γ，x：A不等于B，我们得到chk-fun-I.Q完整性导致了以下重要的推论，表明算法拒绝可类型项的唯一原因是非终止性：推论5.3设t β-正规，且Γ μ t：C但Γ/μ t惠C。然后，t有一个推断的或归属的类型，它不是强规范化的。证据由5.2可知，D：：Γt惠C。 因为只有在相等性检查中，类型A和类型A才是不同的，所 以 必 须 存在具 有 无 穷 派 生 的 类型A和类 型 A10A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）∗D中包含的AA。 这个推导必须包含q-RED-L或q-RED-R的无限多个应用，因此，A或A不是强正规化的。Q6Haskell实现在下面，我们给出了我们的λ类型检查算法的Haskell实现。我们选择了一个有效的实现替代和弱头减少通过关闭。最后，它非常类似于Coquand另外，我们显式地使用了mon- ads，这是一种抽象的方式，使实现具有可扩展性，例如.例如，在一个实施例中，对宇宙的推论我们使用monad来处理类型上下文中的错误和查找，这是由有限映射实现的。moduleTypeTypewhereimportControl.Monad.Error导入控件.Monad.Reader导入数据.映射（映射）导入限定数据。映射为映射语法从文件中解析出来的是由（Haskell）类型Exp的抽象语法树表示的。变量由名称引用。我们保持函数类型只以Pi a（Abs x b）的形式出现的不变式。typeName=String数据扩展=变量名称| Abs名称Exp| 应用程序扩展扩展| Pi ExpExp| 类型衍生秀a b=Pi a（Abs“_”b）价值观和环境求值是惰性的，所以值是闭包Clos t rho，表达式t和环境rho的对。当类型检查Abs牵引的主体时，自由变量被映射到唯一的ID，Coquand [6]称为泛型值Gen。因此，环境组件rho可以将变量名映射到泛型值或闭包。（Haskell）e类型的环境作为一个A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）11参数设置为Val，因为我们不想在这里提交特定的环境表示。类型ID=Int数据显示e显示值e=Gen Id| Clos Exp e衍生秀类型Ty e=Val e闭包的弱头范式（whnf）可能是一个介绍，WType，WPi或WAbs，或者是一个泛型值WNe的消除，即，一个标识符适用于几个闭包。 求值并不是在绑定器下进行的，因此，函数闭包Clos（Abs x t）rho的whnf就是WAbs x t rho。数据显示时间=WNe Id[Val e]--参数的反向列表| WAbs名称失效日期| WPi (Val e) (Val e)| WType衍生秀类型WTy e=Whnf e将名称映射到值的环境是抽象的。我们通过类型类Env指定它们，提供构造（emptyEnv和extEnv，扩展）和查询（lookupEnv）的操作。class显示环境在哪里emptyEnv：：eextEnv：：Name→Val e→e→elookupEnv：：e→Name→Val e评价及应用whnf通过移除弱头β-赎回来计算值的弱头范式。值有两种情况：通用值Gen，它已经是弱头法线，以及闭包，我们使用辅助函数whnf** 进行规范化。whnf：：Envevalve e→Whnf ewhnf（Gen i）=Wne i[]whnf（Clos t rho）=whnft rhowhnf函数在环境rho中计算表达式的whnf。 在环境中查找变量Var x的值。其结果可能是一个关闭12A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）∗∗必须递归地评估或者，它可能是一个泛型值，以防x通过在其绑定器下进行单步执行而变得自由。应用程序是赎回的来源，使用函数app进行延迟解析（cbn）。其他形状的表达式Abs、Pi和Type已经是whnfs了。whnf：：EnveExp→e→Whnf ewhnf（Var x）rho=whnf（lookupEnv rho x）whnf（App t u）rho=app（whnft rho）（Clos urho）whnf（Abs x t）rho=WAbs x t rhowhnf（Pi a b）rho=WPi（Clos a rho）（Clos brho）whnfType rho=WTypeapp将whnf应用于闭包，将结果简化为whnf。函数部分只能是中性的或抽象的，其他情况是不可能的，因为它是病态类型的。app：：EnveWhnf e→Val e→Whnf eapp（WNe i vs）v=WNe i（v：vs）app（WAbs x t rho）v=whnft（extEnv x v rho）用于类型检查我们将上下文隐藏在MonadCxt类的monad中。上下文为每个名称提供类型和值。 bind使用类型和值扩展上下文。new用给定的类型扩展它，创建一个新的泛型值。 新的设计师只需要泛型值，在它的类型无关紧要的情况下。名称的类型可以通过typeOf查询，表达式可以在上下文中关闭，在这种情况下，上下文就像环境一样（这是我们需要引用名称值class（Env e，Monad m）MonadCxt e m |m → e其中bind：：Name→Ty e→Val e→m a→m a new：：Name→Ty e→（Val e→m a）→m anew绑定 ：：Name→（Val e→m a）→m anew x=new x dontCaretypeOf：：Name→m（Tye）close：：Exp→m（Val e）dontCare=error“内部错误：没有类型分配给变量”双向类型检查infert推断表达式t的类型，在whnf中返回它。可推论的是除抽象以外的所有表达形式。对于一个变量，类型在上下文中查找，然后弱头规范化。这不会引入不必要的发散，因为推断类型总是需要转换为弱头范式，或者检查它是否是A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）13→←∗→∗∗←函数类型（参见案例App），或者将其与另一种类型进行比较（参见下面的等式）。但是请注意，上下文中的类型不是弱头范式。 标准化-在将它们添加到上下文之前对其进行分析确实会引入不必要的分歧，例如，对于未使用的发散类型的变量inferred：：MonadCxt emExp→m（WTye）inferred（Varx）=typeOfx>=returnwhnfinferred （ Apptu ）=dow←inferred t案例WWPi v fdocheck u vu关闭ureturn（whnf f→失败（“预期“+显示t+“为函数类型”）推断类型=返回WTypeinferred（Pi a b）=dochecka WTypev←close（acheck b vreturn WTypecheck t v通过将类型转换为弱头范式并调用check_t来检查表达式t与类型值v。check函数只处理抽象Abs x t，它必须是函数类型Pi v f，并且它们的主体t必须在由x扩展的上下文中类型check，x的类型是v，其值被设置为新的泛型值I.非抽象t的类型被推断为w，并与归属类型w进行比较。check：：MonadCxt emExp→Ty e→m（）check t v=check t（whnf v）check函数：：MonadCxt emExp→WTy e→m（）check（Abs x t）（WPiv f）=new x v（λi check t（whnf f' app ' i））checkcheck（Abs x t）w=fail（“expected“+show w+“成为函数类型”）检查tw=dow推断t等式w相等性检查价值观。我们定义了三个相互递归的函数，每个函数返回一元布尔值m（）。eq对whnfs进行操作，eq对任意闭包进行操作，eqs比较相同长度的闭包列表。通过将两个函数闭包WAb应用于新的泛型值i来测试它们的相等性。等式：MonadCxt e mWhnf e→Whnf e→m（）eq WType WType=return（）eq（WPi a b）（WPiab）=eqaa>eqbeqv@（WAbs{}）v@（WAbsx）=newx（λi→eq（v ' ap p ' i）（v14A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）∗⇒ →→eq（WNe i vs） （WNe i vs）|i i=等式vs等式vs等式等式w w=fail（“相等性检查失败“+show w+“and“+showw）等式1：MonadCxt e m Val e Val e m（）eqvv=eq（whnf v）（whnf v）等式：MonadCxt e m[Val e]→[Val e]→m（）eqs[][]=return（）eqs（v：vs）（v：vs）=eqv>eqs vsvseqs vs vsvs.=fail（“相等性检查失败：“+“不同长度的参数向量”）声明类型检查器的输入是x：A=t形式的声明，这意味着名称x具有类型A和定义t。类型检查器将首先确保A是一个格式良好的类型，评估它（懒惰地），然后检查t对A的值，并最终将x绑定到A的类型值和当前环境中的t值。然后它将继续下一个声明。dataDecl=Decl{name：：Name，ty：：Exp，value：：Exp}派生Show checkDecl：：MonadCxt e mDecl→m（Ty e，Val e）checkDecl（Decl x a t）=docheckreturn（v，w）类型Decls=[Decl]checkDecls：：MonadCxt emDecls→m（）checkDecls[]=return（）checkDecls（d：ds）=do（a，v）←checkDecl dbind（name d）a v（checkDecls ds）上下文的实现我们将上下文实现为从名称到其类型和值的有限映射他们还处理新标识符的生成。为此，下一个未使用的泛型值存储在fieldnextFree中。cxtExt只是检索名称的类型，cxtExt只是将类型绑定到名称，而cxtBind将类型和值都绑定到名称。dataCxt=Cxt{nextFree：：Int，cxt：：Map Name（Ty Cxt，Val Cxt）}衍生秀A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）15cxtxt：：MonadmCxt→Name→m（Ty Cxt）cxtxtgamma x=caseMap.lookup x（cxt gamma）of（a，v）返回aNothing→fail（“identifier not in scope：“+x）cxtEmpty：：CxtcxtEmpty=Cxt0Map.emptycxtExt：：Name→Ty Cxt→Cxt→CxtcxtExt x a（Cxt n gamma）=Cxt（n+1）（映射插入x（a，Gen n）gamma）cxtBind：：Name→Ty Cxt→ValCxt→Cxt→CxtcxtBindxavgamma= gamm a{cxt= Ma p. （a，v）（cxtgamma）}上下文可以被看作是环境，因为它们为每个名称提供了一个值实例环境Cxt，其中emptyEnv=cxtEmptyextEnv x v rho=rho{cxt=Map.insert x（dontCare，v）（cxtrho）}lookupEnv rho x |Just（a，v）← Map.lookup x（cxtrho）= v类型检查Monad的实现在类型检查过程中，我们需要查询上下文，并引发错误。类型检查monad将一个reader monadReaderT Cxt（参见模块Control.Monad.Reader）包装在一个error monadEither String周围。MonadCxt操作的实现通过MonadReader操作请求访问上下文，并通过local修改上下文。这里的ReaderMonad仅用于隐藏静态绑定的标准实现中使用的管道。特别地，变量的阴影是通过替换先前的定义来实现的typeTC=ReaderT Cxt（Either String）实例MonadCxt Cxt TC，其中typeOf x=dogamma←ask伽玛射线关闭t=dorho←askreturn（Clos trho）new x a f=dogamma←asklocal（cxtExt x a）（f（Gen（nextFreegamma）bind x a v c=local（cxtBind x a v）c主类型检查循环的实现使用reader monad对声明序列进行类型检查。checkFile：：Decls→IO（）checkFile ds=case（checkDecls dsRight（）→putStrLn“类型检查成功”16A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）左s→putStrLn（“类型检查错误：“+s）A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）177结论本文对非规范化类型的λ_n给出了一个正确的部分类型检验算法.应该可以通过用排序注释类型来扩展函数PTS的算法-然而，需要研究抽象规则的已知问题（参见[12]）。我们已经证明，算法只会失败，因为在类型检查过程中存在发散项（推论5.3）。这并不意味着算法不能改进，例如，它可以在规范化术语之前检查语法相等性。然而，在实践中，我们感兴趣的是理论规范化片段中的类型检查。事实上，对于给定的PTS，我们只需要显示规范化，就可以得出结论，我们的算法决定了类型关系。因此，除了适用于非终止类型系统之外，我们的论文还提出了一种新的方法来证明终止类型理论的可判定性：在本文中，我们可以证明类型检查的部分正确性，然后分别给出类型检查的可判定性的规范化。这里给出的证明还应该扩展到具有显式递归和附加功能的语言，以建模依赖的数据类型，例如，我们计划将其应用于依赖类型编程的核心语言[2]。另一个研究方向是将我们的方法扩展到具有βη-等式的问题是，相等性检查和类型检查的分离不再起作用-然而，我们推测这样的算法仍然是合理的和部分完整的。确认Has kell coode是由lhs2TeX（AndresLéoh和RalfHinze）设计的。引用[1] A bel，A.，T. C oquand和P. 刘文龙，"语义转换检验“，载于：《中国科学院学报》，第二卷. Paulin-Mohring ， 编 ， “Proc. of 9th Int. Conf. on Mathematics of Program Construction, MPC 2008(Marseille, July 2008),” Lecture Notes in Computer Science 29比56[2] Altenkirch，T. 和N. Oury，J.C.：Acore language for dependently typed programming，draft，2008，available at http://www.cs.nott.ac.uk/ ~ txa/publ/.[3] Augustsson，L.，Cayenne -一种依赖类型的语言，在：“Proc. of 3rd ACM SIGPLAN Int. Conf. onFunctional Programming，ICFP '98（Baltimore，MD，Sept. 1998），”ACM Press，1999，pp. 239-250.[4] Barthe，G.和T. Coquand，非正规化纯型系统的方程理论，J。的Funct。程序. 16（2）（2006），pp.137-155[5] Barthe ， G. 和 M. H. Sørensen ， Domain-free pure type systems ， J. of Funct 。 程 序 . 10 （ 5 ）（2000），pp. 417-452[6] Coquand，T.，一种类型检查依赖类型的算法，Sci.的Comput。程序. 26（1167比17718A. Abel，T.Altenkirch/Electronic Notes in Theoretical Computer Science 229（5）（2011）[7] Coquand ， T. 和 M. Takeyama ， An implementation of Type ： Type ， in ： P. Callaghan ， Z. Luo ， J.McKinna和R. Pollack，编，”《明史》卷五。 关于证明和程序的类型，TYPES 2000（Durham，12月15日）。2000），53比62[8] Goguen ， H. ， “A Typed Operational Semantics for Type Theory ， ”PhD thesis ， University ofEdinburgh，1994.[9] Goguen，H.，证明βη转换的算法，在：V.Sassone，ed.，第八届国际会议论文集关于软件科学和计算结构的基础，FoSSaCS 2005（爱丁堡，2005年4月），410-424[10] Gordon，A.，关于共同归纳和函数式编程的教程，在：K。Hammond，D. N. Turner和P.M. Sansom，eds. ， 1994 年 格 拉 斯 哥 Wksh 。 函 数 式 编 程 （ Ayr ， Sept.1994 ） " ， Workshops in Computing ，Springer，1995，pp. 78比95[11] Plotkin，G.，按名称调用、按值调用和λ演算，Theor。Comput. Sci. 1（1975），pp.125-159[12] 波拉克河，“The Theory of LEGO: A Proof Checker for the Extended Calculus of Constructions,” PhDthesis, University of Edinburgh,