演算的发展与模式匹配的应用及类型系统的插入

3理论计算机科学电子笔记71（2003）网址：http://www.elsevier.nl/locate/entcs/volume71.html17页用（out）类型Horatiu Cirstea1，Claude Kirchner，1和Luigi Liquori1洛里亚，INRIA和南希大学2校园科学，BP239，54506V和oeuvre-l`es-NancyCedexFrance摘要在过去的几年里，已经看到了一个新的演算的发展，可以被认为是过去十年的各种研究（高阶）长期重写系统，和lambda演算的结果。在重写演算（或Rho演算，ρCal）中，代数规则被认为是“带模式的lambda项”的复杂形式演算可以被定制为模复杂的理论，如交换性，结合性，结合-交换性等，这使我们能够编码复杂的结构，如列表，集合和更一般的对象。微积分既可以被称为“a la Curry“，也可以被称为”a la C h ur c h“，而不会牺牲可读性，也不会使元理论过于复杂。许多静态类型系统可以很容易地插入到微积分之上，这是丰富的面向类型的文献的精神。 重写演算可以表示一种通用语言，用于编码许多计算范例，以及用于构建基于lambda演算和有效重写的强大定理证明器关键词：Lambda演算，Rho演算，类型系统，模式匹配，理论框架和基础，Curry-Howard，逻辑，纯模式类型系统1引言辨别模式的能力是人类推理的主要基本机制之一事实上，识别模式的能力，我。e.自信息处理建模开始以来就存在模式匹配。1电邮地址：{Horatiu.Cirstea，Claude.Kirchner，Luigi.Liquori}@ loria.fr2003年3月，出版社dbyElsevierScienceB。 V. 操作访问和C CB Y-NC-N D链接。CIRSTEA，KIRCHNER和 LIQUORI4|XX}X Y XX X X X{不TT模式匹配在许多语言中通过简单的参数传递机制隐式地发生，在ML和Prolog等语言中显式地发生，在这些语言中它可能非常复杂[29]。令人惊讶的是，最常用的计算模型之一lambda演算只使用了简单的模式匹配。这已经被扩展，最初是为了编程考虑，通过在lambda演算中引入模式[34，36]，或者通过在函数式编程语言中引入匹配和重写规则事实上，许多作品都致力于将项重写与lambda演算相结合，要么通过丰富一阶重写与高阶能力[26，37，31]，要么通过向lambda演算添加代数特征，特别是允许以有效的方式处理等式[32，4，19，23]。 模式抽象通过绑定结构化表达式而不是变量来概括lambda抽象，并且通常用于编译函数式编程语言中的case表达式[34]，并为lambda演算提供术语演算[25]。例如，模式抽象λ 0. 0和λsucc（）。用于编译前置函数λ。0 D的情况0succ（）D，而模式抽象λ， .用于编码σ，τσσ∧τ►σ► （στ）→σ规则抽象通过绑定任意表达式而不是模式来，并用于重写演算 提供重写规则和重写策略的第一类说明。例如，规则抽象可以用于对术语重写系统的最内层重写策略进行编码。此外，规则抽象对应于高阶自然演绎的一种形式，其中（部分）证明树被排出而不是假设。尽管这样的规则抽象在逻辑和编程语言的设计和实现中都是一个坚实的基础，但它们缺乏既定的基础。在重写演算中，通常的lambda抽象λX。T被替换为规则抽象T1DT2，其中T1是一个任意项（行话中的模式），T2是要触发的参数，其中T1的自由变量在T2中绑定（通过模式匹配）。将抽象T1DT2应用于项T3总是e. 一个术语，其中匹配方程是匹配约束将（自）评估（如果存在匹配解决方案）或延迟（如果不存在解决方案）。如果存在解σ，则延迟匹配约束自评估为σ（T3）。演示文稿是故意保持非正式的，几乎没有定义，没有附录，也没有证明;为了刺激好奇的读者，给出了一些练习我们采用了我们所知道的最简单的代数理论：CIRSTEA，KIRCHNER和 LIQUORI5≡XK不TTT TT一个.很简单，本文的主要目的是介绍，解释，提供示例，并激发读者更多地了解重写演算[8，9，7，10]。2语法Thentyped（i.e. Rho演算（ρCal）中的“alaCurry）syntax”通过增加延迟匹配约束，推广了[11，12]中的结果正如在任何涉及粘合剂的微积分中一样，我们对Church [ 6 ]的“α-约定“取模e. 自由变量和这个符号表示像术语或替换这样的对象的句法身份。ρCal的语法定义如下：T：：= X|K| TDT|[TT] T| T·T |T，T其中表示变量集， 常数的集合。通过滥用符号，我们用可能索引的相同字母来表示这些集合的成员。请注意，有两种(i) T 1DT 2表示一个规则抽象，模式为T 1，主体为T 2; T 1的自由变量在T 2中绑定。(ii) [T1T2] T3表示具有模式T1T2的延迟匹配约束和主体T3;T1的自由变量在T3中有界，但不在T2中。为了支持直觉，我们在这里提到，将抽象T1DT3应用于项T2总是约束项的主体将根据相应匹配问题. 如果存在解，则延迟匹配约束自评估为σ（3），其中σ是1和2之间的匹配的解。最后，作为一种句法糖，直接从以前的ρCal作品中得到启发，术语可以被组合成使用符号“，"构建的结构我们假设应用程序操作符“·“（通常是隐藏的）“·“的优先级] 的优先级高于“定义2.1[签名和缩写]T1。T2=ΔT0（T1·· ·Tn）=Δ（Ti）i =1. n =ΔT1T2T1自助申请T0T1···Tn函数-应用T1，···，Tn结构CIRSTEA，KIRCHNER和 LIQUORI6不我们提请读者注意表示应用程序操作符的“·“和“.”之间的主要区别表示S.卡敏[24]。3匹配在引入ρCal下方的主要机械之前，i.e. 匹配，我们适应了经典的概念，同时替代应用处理的新形式的约束项中引入的ρCal。定义3.1[替换]置 换 σ 是 从 变 量 集 合 到 项 集 合 的 映 射 。 有 限 替 换 具 有 形 式{T1/X1.。Tm/Xm};empty代换{}用σID表示。将一个代换σ应用于一个项T，通常用σ（T）表示，定义如下：σID（T）=Δσ（K）=Δσ（Xi）=Δ不K如果Xi∈Dom（σ），则Ti为零σ （ T1DT2 ）=Δσ （ [T1T2]T3 ）=Δσ（T1T2）=ΔΔT1Dσ（T2）[T1σ（T2）]σ（T3）σ（T1）σ（T2）Xi否则σ（T1，T2）=σ（T1），σ（T2）当我们使用模α约定时，这定义了高阶替换;当将替换应用于抽象时，我们知道相应抽象模式的自由变量不属于替换的域。该定义与ρCal的评价机制兼容。在ρCal中，我们处理模式及其应用的抽象;因此，计算从模式T1到主题2的匹配的替换是微积分的关键组成部分。我们在这里集中在语法匹配，我们重温相应的概念和算法。我们表示通过使用一个变量列表，我们使用以下定义进行语法匹配：定义3.2[匹配方程和解](i) 匹配方程是T1T2形式的公式;(ii) 匹配系统T=Δi=10. nTiiTiJ是匹配连词方程，其中，n是结合的和交换的;(iii) 匹配系统T是(a) 其形状为i=10. nXiiTij=0. mKjjKj;(b) 对于所有h，k = 0.编号： Xh <$Xk蕴涵Th <$Tk;(c) 对于所有i = 0. n：Xi∈Xi蕴涵Xi<$Ti;CIRSTEA，KIRCHNER和 LIQUORI7{T X···T X}≺≺T T≺(d) 对于所有i = 0. n，FV（Ti）<$<$i/=<$i蕴涵Xi<$Ti.(iv) 代入σT=Δ1/1n/n是成功匹配系统T的解。ρCal中的计算引擎解决了匹配约束，I. e.给定延迟匹配约束[T1T2]T3，求匹配方程T1T2（如果存在）的解σ，然后用σ（T3）继续计算定义3.3[匹配算法]求解匹配方程的匹配替换可以通过以下匹配缩减系统来计算，其中，（Rule）（T1DT2）规则（T1DT3）规则T2规则，规则T3（延迟）[T 1 T 2] T 4延迟[T 1 T 3] T 5延迟T 2延迟T 3延迟T 4延迟，延迟T 5（应用）（T 1 T 2）延迟（T 3 T 4）延迟T 1延迟T 3延迟T 2延迟T 4（结构）（T 1，T 2）延迟（T 3，T 4）延迟T 1延迟T 3延迟T 4延迟，延迟T 5（应用）（T 1 T 2）延迟（T 3，T 4）延迟T 1延迟T 3延迟T 4延迟T 5（应用）（T3，T 4）延迟T 1延迟T 3延迟T 4延迟T 4（结构）（T 1，T2）延迟T 1延迟T 3延迟T 4延迟T 4延迟T 5（应用）（T 3，T4）延迟T 1延迟T 3延迟T 4延迟T 5（应用）（T 3，T 4）延迟T 1延迟T 3延迟T 4延迟T 4延迟T 4延迟T 4（结构）（T 3，T 4延迟T 4）延迟T 1延迟T 3延迟T 4延迟T 4延迟T 4延迟T从匹配方程1<$2开始，该规则集的应用显然终止，并且要么导致不成功的匹配系统，在这种情况下，我们说匹配失败，要么导致替代σ，使得σ（T1）<$T2被展示。我们用σ（T1T2）来表示这样的置换.锻炼的 如果你喜欢匹配算法：(i) 通过添加失败符号F并列举所有可能的处理匹配失败的归约规则来完成算法f（3）f（4）f（5）(ii) 用更复杂的代数理论定制算法e. G. 其中“，“运算符是结合的M. Hullot's或S. Eker的算法[22，15]）。4语义CIRSTEA，KIRCHNER和 LIQUORI8不4.1小步归约语义小步归约语义由图1中给出的归约规则定义。微积分的（ρ）规则的中心思想是将项T1DT2应用于项T3，简化为延迟匹配约束[T1T3]T2，而（σ）规则的（应用）在于求解匹配方程T1T3，并将所得结果应用于术语2。 规则（δ）处理应用在用“，”构造函数构建的结构上CIRSTEA，KIRCHNER和 LIQUORI9不−PP TV（ρ）（T1DT2）T3 →ρ[T1T3] T2（σ）[T1T3] T2→σσ（T1T3）（T2）（δ）（T1，T2）T3 →δT1T3，T2T3Fig. 1. 小步约简语义重要的是要注意，如果1是一个变量，那么随后的（ρ）和（σ）规则的组合正好对应于λ演算的（β）规则，并且替换中的变量操作是外部处理的，如果必要的话，使用α转换和Barendregt像往常一样，我们介绍了经典的概念，一步，多步，和同余关系→ρσδ。定义4.1[一步，多步，→ρσδ的同余]设Ctx[−]是任何有一个空洞的上下文，Ctx[T]是用项T填充空洞的结果;(i) 一步评估<$→ρσδ由以下推理规则定义：T1→ρσδT2（Ctx[]）Ctx[T1]›→ρσδCtx[T2]其中→ρσδ表示ρCal的顶层规则之一;(ii) 定义多步求值→ρσδ为<$→ρσδ的自反传递闭包;(iii) 同余关系=ρσδ是→ρσδ的对称闭包。4.2刚性模式条件。当对项的形状以及由此得到的匹配方程没有任何限制时，小步约简失去了连续性。因此，应该对图案的形状施加合适的条件。在本文中，我们为ρCal采用了所谓的刚性模式条件（RPC），这在[36]中首次形式化，我们将语法限制为以下形式的术语：T：：=PDT|[PT]T|......你好。。 asbefore.利用刚性图案的集合（即，e.满足RPC的条件）。对于RPC的正式定义，我们参考[36，3];出于本文的目的，我们只是给出了一个“诚实”子集的特征定义4.2[P的特征]设NF（ρσδ）是项的集合，CIRSTEA，KIRCHNER和 LIQUORI10xx x x x x x x x x x X x X X不能在小步归约语义中归约;我们定义：P=Δ{T∈NF（ρ σδ）|它是线性的，没有活动的变量}当应用程序的左侧是一个变量时（e。G.在（X T）中，我们说相应的变量X是A活动的。注4.3（见[36]）由上述特征定义的集合P满足RPC（即， 它的元素满足RPC），并且正确地包含V（因此lambda演算可以编码为ρCal）。 P不是ρσδ是c的极大集，例如，当r=Δ（D）（D）时，满足RPC [36]。满足RPC的项的小步约简语义是连续的。命题4.4（Church Rosser）关系式<$→ρσδ是连续的。为了说明微积分的小步语义，我们使用不同的评估策略（最外层与最内层）来减少两个术语，并在第一种情况下产生e. 不包含延迟匹配约束），并且在第二个中是“不成功”的。例4.5【四小步缩减】取项（f（X）D（3D3）X）f（3）和（f（X）D（3D3）X）f（4）我们减少它们，尝试四种可能的（下划线）赎回。(i) （f（X）D（3 D 3）X）f（3）<$→ρ[f（X）]f（3）]（（3 D 3）X）<$→σ（3D 3）3<$→ρ[3 3]3<$<$→σ3(ii) （f（X）D（3 D 3）X）f（3）›→ρ（f（X）D [3X]3）f（3）›→ρ[f（X）f（3）]。（[3X]3）›→σ[33]3›→σ3(iii) （f（X）D（3 D 3）X）f（4）›→ρ[f（X）]f（4）]（（3 D 3）X）<$→σ（3D 3）4›→ρ[3 4]3(iv) （f（X）D（3 D 3）X）f（4）›→ρ（f（X）D [3X]3）f（4）›→ρ[f（X）f（4）]。（[3X]3）›→σ[34 ]3值得注意的是，术语[3 4]3实际上表示计算失败，可以理解为：“由于匹配失败而发生错误”。ρCal记录失败的能力直接继承自以前版本的微积分，其中显式引入了一个特殊的符号null来表示计算失败。我们用一些精心设计的 “ 面 向 对 象 编 程 ” 例 子 来 结 束 本 小 节 （ 也见 [ 1 1 ] ） 。CIRSTEA，KIRCHNER和 LIQUORI11例4.6[Fix、Para和DNA对象]CIRSTEA，KIRCHNER和 LIQUORI1212X公司简介1公司简介2123123V V（Red−V al）T1→T3→ T4[T3T2] T4O（红色−ρ）T1T2T2 OT1T3，T4T3T2O1T4T2O2T1T2O1，O2（红色−δ）好吧σ（T1）<$T2σ（T3）<$O（Red−σ）[TT] TOOO$σ。σ（T1）<$T2 （红−σ）[TT] T wrongT1错误（红色−ρ）T1T2错误图二. 大步操作语义(i) LetFixf=ΔrecDSDf（S. rec）。然 后 ，我们可以很容易地得到Fixf。rec→ρσδf（Fixf. rec）。 这个固定的dpot可以推广dasFi x=ΔrecDSDXDX（S.rec（X）），其行为将是Fix.rec（f）→ρσδf（Fix.rec（f））.(ii) （1）A=A（）DD。， aDD3，. ）. 2016年04月05日04：00- 01：00（）查找分配给变量的方法名，然后发送（i. e. 安装，作为一等公民）这个方法到对象本身，i。e. P ARA。（pa r（a））=ΔP ara（pa r（a））P ara→ρσδ（SDS. a）P ara<$→ρσδP a ra.a→ρσδ3。(iii) LetDna=ΔsetDDD（（addDJDD（，J）），）. Dna的set方法用于通过从外部接收方法的所有组件（即，标签和身体。一旦对象被安装，它就有能力在接收到add消息时扩展自己。从某种意义上说，然后又道：Dna.set（aDSD3）=ΔDnasetDna（aDSD3）→ρσδ（XD（（addDSJDYD（Y，SJ）），X））（aDSD3）›→ρσδ（（addDSJDYD（Y，SJ））， aDSD3）=ΔT，andT.add（bDSD4）→ρσδT，bDSD4.4.3大步操作语义我们通过Plotkin[35]的演绎系统的自然过程来定义操作语义。演绎系统的目的是将每一个封闭表达式映射成一个范式，即：e. 弱头标准形中的不可约项。所提出的策略是懒惰的按名称调用，因为它在CIRSTEA，KIRCHNER和 LIQUORI13T O简单的抽象（i. e. TDT）、结构（i.e. T，T），和代数项（i. e. KT）。我们定义值V和输出值O的集合如下：V：：= K| TDT| K T| T，TO：：= V|错|噢，噢特殊输出错误表示通过涉及“匹配方程失败”的计算获得的结果语义是通过对形状的判断来定义的，其规则（几乎是自我解释的）如图2所示。与小步长约简语义一样，大步长语义使用定义3.3中给出的匹配算法。大步骤操作语义是确定性的，并立即建议如何为演算构建解释器。此外，大步操作语义对于关系→ρσδ是合理的，因为以下成立：支持4. （7）对于给定的T，如果T≠V，则T → <$→ρσδV。定义4.8[T的收敛性]对于一个闭T，我们说T收敛，我们把它记为T，如果存在一个输出值O，使得T O。给定上述定义，我们还推测了完备性，这表明每个终止程序也在我们的解释器中终止命题4.9（π的完备性）对于闭T，如果T <$→ρσδV，则T收敛，即T.锻炼的[按值调用]如果你想玩大步操作语义，那么修改输出值集和为了实现一个懒惰的按值调用策略。为了说明大步语义的行为，我们给出了前两个术语的演绎树例4.10【两个大步骤推导】取下列项（f（X）D（3D3）X）f（3）和（f（X）D（3D3）X）f（4）演绎树是：。σ{3/X}（3D3）3<$3[f（X）]f（3）]（3D3）X3（f（X）D（3D 3）X）f（3）<$3和$σ。σ（3）σ4σ{4/X}（3D3）4错误[f（X）f（4）]（3D3）Xwrong（f（X）D（3D 3）X）f（4）错误其中n =（f（X）D（3D 3）X）n =（f（X）D（3D 3）X）.在大步操作语义中，输出值wrong用于表示在运行时发生匹配失败的“坏”计算。因此，所提出的语义不会中止计算，对于CIRSTEA，KIRCHNER和 LIQUORI14关于我们例如在。（3D3，4D4）4错，4在最终结果中保留一个计算出错的事实。当然，其他选择也是可能的，比如一旦产生错误的值就。（3D3，4D4）4错后一种选择需要修改我们的大步语义。重新开始：第一个（呈现的）选择导致锻炼的 如果你喜欢自然语义：(i) （悲观机器）将提出的“乐观”大步语义修改G. 添加/修改所有引发（前提中）和传播（从前提到结论）错误值的演绎规则(ii) （示例4.6）使用大步长操作语义来减少Para和Dna对象：检查是否获得与小步长减少语义相同的结果。5处理问题在上一节中，我们看到错误的输出值会中止计算。然而，在现代编程语言中，人们可能会对在受保护的环境中尝试一些代码块感兴趣，并且每当发生运行时匹配错误时，首先捕获它，然后执行一些异常处理程序，这些异常处理程序可以在距离异常引发的地方许多“英里”之外声明这是一个尝试的案例... 接住...Java的机制，或ML，C#中的类似结构，...。在ρCal中，异常可以表示在运行时发生了某些匹配失败，例如将常数3与另一个常数4进行匹配在这种情况下，项（3D 3）4简化为[3 4]3，其可以读作如下：“the result would be4，产生（脏）结果 [3 4]3在下文中，我们提出了一个考虑匹配异常及其处理的ρCal的舒适扩展。重写演算的一个简单的异常处理机制已经在[16]中研究过。 由于篇幅有限，我们在这里只介绍大步骤的操作语义，而把小步骤的操作语义作为练习。 这个扩展的灵感来自[28]。 做CIRSTEA，KIRCHNER和 LIQUORI15123不TT不21123121234（Red−V al），（Red−ρ1），（Red−σ1）如图e2所示$σ。σ（T1）<$T2 （红−σ）[TT] T中文（简体）T]T1[T2T3]T4O（红色-Exc）尝试T捕捉[TT]与T OT1<$OO<$/[T2T3]（Red−Exc）尝试T1捕获[T2T3]与T4OT1T3，T4T3T2V1T4T2V2T1T2V1，V22（红色−δ）T1[T3T4]（红色-道具）T1T2T[T3T4]T1-T3，T4-T3-T2-[T5T6]（红色-道具）T1T2T[T5T6]T1T3、T4T3T2VT4T2 [T5T6]（红色-道具）T1T2T[T5T6]图三. 异常处理首先，我们需要在ρCal语法中添加一个异常处理构造函数I. e.T：：= tryTcatch [T[T]与T|......这是什么？和以前一样直觉上，[T T]表示一个无解的匹配方程，如e。G. [三4]。执行tryT1catch[T2T3]和T4意味着范围 匹配失败[T2T3]的异常在T1中是活动的，并且如果该异常发生，则处理程序4将被执行。否则，引发的异常将传播到trycatch的作用域之外。更准确地说：首先，我们计算1（保护项）。如果1的计算结果是没有匹配失 败 的 输 出 （ 即 ， e. 一 个 输出值 ）， 那么这 个值将 是整 个 try catchwithexpression的结果这大致相当于执行T1而不引发异常.相反，如果发生匹配失败，那么我们必须检查这个失败是否是在trycatch withexpression（i）中声明的失败。e. [T2T3]）或不;在第一种情况下，我们执行处理程序4，而在后一种情况下，我们将匹配失败传播到trycatch的作用域之外。 请注意，异常[T2T3]的范围在T1 而不是T4。为了添加异常处理机制，我们首先修改输出值集合O如下：CIRSTEA，KIRCHNER和 LIQUORI16−不不- − −⇓V：：= K|TDT|K T| T，TO：：= V|[T T]直观地说，不是引入简单的错误输出信号，而是特殊的输出[]定制异常信号（因此记录匹配失败的类型）并确保异常可以被正确地传播和因此，我们保留规则（Red V al）、（Red ρ1）和（Red σ1），并添加一些额外的演绎规则，如图3所示。所提出的解释器实现了严格传播异常信号的因此，应该注意到，根据最后三个（传播）规则，异常信号的传播独立于其他（可能成功的）计算。请注意，（Red Exc2）也可以被视为一个传播规则，因为一个与try catchwith表达式中指定的异常信号不同的异常信号如果在受保护的部分中没有生成匹配失败，则传播相应的结果。例5.1[一大步推导]try（f（X）D（3D 3）X）f（4）catch[3 4]withg（4）使用下面显示的自然演绎来计算，$σ。σ（3）σ4σ<${4/X}（3D3）4<$[34][f（X）]f（4）]（3D 3）X[3四 、（f（X）D（3D3）X）f（4）[34 ]f（4）f（4）try（f（X）D（3D 3）X）f（4）catch[3[4]其中f（4）<$f（4）其中n =（f（X）D（3D 3）X）n =（f（X）D（3D 3）X）.锻炼的（i）（小步骤语义）为使用新的try catch withexception handler增强的ρCal设计小步骤减少语义（提示：检查M的C和A控制操作符Felleisen[17]）;(ii) （广义例外）细化和广义化，以捕捉广义失败，如[T1T2]表示任何无法求解的匹配方程，试图将固定项T1与任何项T3匹配，使得T2T3是可解的;(iii) (more generalization）细化和推广（ii）的函数，以声明类似于[T1T2]的广义失效，并捕获类似于[T3T4]的任何异常，使得T1T3和T2T4是可解的;(iv)（按值调用）与上一个练习一样，在扩展的ρCal中修改除了例外，以实现懒惰的按值调用策略。CIRSTEA，KIRCHNER和 LIQUORI17X电子邮件6多态类型推断到目前为止，我们已经提出了一种unyped（a`laCurry）syntax，其中的术语没有使用类型进行修饰本节介绍了一个简单的类型规则，它可以通过静态类型检查来为ρCal程序分配语义，从而在运行ρCal-terms之前捕获一些错误（不幸的是，不是运行时匹配的错误）。[12，3]中为重写演算和lambda演算提供了复杂的类型化系统;这些类型学科包括简单类型、多态类型、依赖类型和高阶类型，遵循Barendregt[2].不同的类型系统在实践中对应于ρCal的不同使用：例如，依赖和高阶类型广泛用于基于Curry-Howard同构的定理证明器，如Coq或Isabelle，而多态类型主要用于实现ML风格的模式匹配设施（函数式）编程语言的类型推理算法在这里，我们关注多态类型原则;我们在这里不讨论这个系统的可判定性，它本质上是J.Y.Girard Leivant的多态lambda演算[27]。然而，我们猜想，对泛量化器的经典限制，如ML [13]中采用的那种，适当地用模式设施定制，也可以适用于我们的ρCal。类型和上下文的语法定义如下（类型上的σ，τ范围，类型变量上的α范围，上下文上的Γ范围）：σ：：= α |α.σ |σDσr：：= 0 |Γ，X：σ |Γ，K：σ |α：σ在ρCal中的类型判断具有形式Γ：σ。类型推理系统由图4中的规则模式定义。接下来，我们简要介绍类型推理规则，并坚持使用最有趣的规则。• （开始）规则是标准的，不需要注释。• （Struct）规则说一个结构（T1，T2），可以用类型σ，条件是相同的σ可以分配给T1和T2。• （Abs）规则处理抽象，其中我们绑定（非平凡的）模式而不是变量;注意，上下文ΓJ在前提中是带电的，以便考虑T1的自由变量的类型（可能在T2中绑定）。• （匹配）规则处理延迟匹配方程硬编码到项中的项;这个规则基本上是需要的，以确保导致匹配失败的项的良好类型（e. G.（3D3）），并保证顶层规则（ρ）和（σ）的主题约简性质。同样，ΓJ记录了T1的自由变量的类型（可能在T3中有界）。CIRSTEA，KIRCHNER和 LIQUORI18−∀−∀−∀ −∀X：σ∈Γ<$X：σ （开始1）K：σ∈Γ<$K：σ（开始2）ΓT1：σΓT2：σΓT1，T2：σ（结构）Γ， ΓJ<$T1：σ Γ， ΓJ<$T2：τ Dom（ΓJ）=FV（T1）（Abs）ΓT1DT2：σDτΓ， ΓJ<$T1：σ Γ<$T2：σΓ， ΓJ<$T3：τ Dom（ΓJ）=FV（T1）（匹配）ττ[T1T2]T3：τΓT1：σDτΓT2：σΓT1T2：τ（应用）ΓT：σ α/∈FV（Γ）（Abs）ΓT：σα.σΓT：σ{τ/α}见图4。 多态类型推断• （Appl）规则是标准的，不需要注释。• （Abs）和（Appl）规则引入（resp.消除）多态类型：它们是标准的，如Leivant请注意，这两个规则不是语法指导的。定理6.1（主语归约）如果Γ≠ T1 ：σ和T1→ρσδT2，则T2：σ。锻炼的 如果你真的喜欢类型系统：(i) （normalization）表明所有可类型化的项都是强正规化的;(ii) （模糊推理）找到适合ρCal的Damas-Milner[13]算法W的适当扩展;研究复杂性;(iii) （输入异常）定制类型系统，以考虑异常的try catch（提示：检查ML中的异常[21，33]）;(iv) 利用悲观大步机证明了如下类型的可靠性命题的（不可）判定性：T ≠T：σ，且T ≠ O，则O /=wrong.7结论通过这次小小的CIRSTEA，KIRCHNER和 LIQUORI19(but形式主义（formalism演算提供了（高阶）项重写系统和lambda演算的良好该演算适合于进一步的扩展和改进。插入复杂类型理论的可能性为研究新的强大证明引擎和（Meta）语言开辟了道路比RPC限制性更少的新条件允许在抽象中使用更大类的模式，值得研究。构思一个指称语义，继续处理异常和复杂的（用户可定制的）策略也值得研究，最终目标是集成功能，逻辑和基于规则的编程范式。构建一个新的类型系统，静态地防止运行时的匹配失败错误（虽然我们推测的不可判定性）的挑战是非常刺激的。以λ-Prolog[29，30]的风格探索可判定的高阶统一的有限形式也是具有挑战性的，目标是提高定理证明器的自动化。最后，我们推测一个合适的理论将允许人们处理并发性，并希望以JoinCalculus [18]，Ambients [5]或Mobile Maude [14]的风格处理移动性。致谢。Luigi要感谢Furio Honsell和Simonetta Ronchi della Rocca花时间教他ML/Scheme异常和Girard系统F下的主要我们都感谢本杰明·瓦克仔细阅读了手稿。引用[1] H.巴伦德雷Lambda Calculus：Its Structural and Semantics. 北荷兰，1984年。[2] H.巴伦德雷Lambda Calculi with Types.在Handbook of Logic in ComputerScience，第二卷，第118牛津大学出版社，1992年。[3] G. 巴特，H。奇尔斯泰阿角Kirchner和L.利口酒纯模式类型系统。在ACM出版社，编辑，Proc. POPL，2003年。[4] V. Breazu-Tannen。结合代数和高阶类型。LICS的Proc.，第82-90页，1988年[5] L. Cardelli和A. D.戈登移动环境。理论计算机科学，240（1），2000年。[6] A.教堂简单类型理论的一个公式。Journal of Symbolic Logic，5：56CIRSTEA，KIRCHNER和 LIQUORI20[7] H. Cirstea。 计算R′e′ecritu re：基础与应用。Th`esedeD octoratd'Uni versi t'e，Uni versi t'e Henri Poinca r'e-Nancy I，2000.[8] H. Cirstea和C.基什内尔ρ-演算它的基本性质和性质。在CCL研讨会论文，1998年。[9] H. Cirstea和C.基什内尔重写微积分导论。研究报告RR-3818，INRIA，1999年。[10] H. Cirstea和C.基什内尔重写演算-第一部分和第二部分。逻辑杂志的兴趣小组在纯粹和应用逻辑，9（3）：427[11] H.奇尔斯泰阿角Kirchner和L.利口酒匹配功率。在RTA的Proc.，LNCS的第2051卷，第77-92页。Springer-Verlag，2001.[12] H.奇尔斯泰阿角Kirchner和L.利口酒罗方块在FOSSACS的Proc.ofFOSSACS，LNCS的第2030卷，第166[13] L. Damas和R.米尔纳函数程序的主类型模式。在Proc. of POPL，第207-212页。ACM Press，1982.[14] F. 你好，S。 E ker，P. Lincoln和J. 梅瑟格尔 Mobile Maude的原则。在proc的ASA/MA，LNCS的第4卷，第73-85页。Springer-Verlag，2000.[15] S. 艾克通过二分图匹配的关联交换匹配计算机杂志，38（5）：381[16] G. Faure和C.基什内尔重写微积分中的函数。在RTA的Proc.，LNCS的第2378卷，第66-82页。Springer-Verlag，2002.[17] M. Felleisen和D.P. 弗里德曼顺序状态的句法理论理论计算机科学，69：243[18] C. 我们的，G。 去吧，J。- J. 莱维湖Maranget和D. 好的。移动代理的演算。在Proc. of CONCUR，Volume 1119 ofLNCS，pages 406-421中。Springer-Verlag，1996.[19] J. Gallier和V. Breazu-Tannen。多态重写保持了代数的强正规化和一致性。在proc 的ICALP，LNCS的第372卷，第137-150页。Springer-Verlag，1989.[20] J.Y. 吉拉德变量类型的系统F，十五年后。理论计算机科学，45：159[21] C. A. Gun ter，D. R'e my和J。G. Rie cke. 类ML语言中的控制和控制的推广。在FPCA的Proc.，第2378卷，第66-82页中。ACM Press，1995.[22] J. - M.胡洛特关联-交换模式匹配。见IJCAI，1979年。[23] J.P. Jouannaud和M.冈田抽象数据类型系统Theoretical Computer Science，173（2）：349CIRSTEA，KIRCHNER和 LIQUORI21[24] S. N.卡明Smalltalk-80中的继承：一个外延定义。 在ACM出版社，编辑，Proc. 第80-87页，1988年。[25] D.凯斯纳湖Puel和V. Tannen。类型化模式演算。 信息与计算，124（1）：32[26] J.W. Klop，V. van Oostrom，and F.范·拉姆斯东克。组合归约系统：介绍与综述。 理论计算机科学，121：279-308，1993。 这是为纪念科拉多·博姆而发行的特刊。[27] D.雷万特多态类型推断。在POPL的Proc.，第88-98页中。ACM出版社，1983年。[28] L.利口酒语义学和语用学的一个功能语言与连续的Esplicite。乌迪内大学信息科学奖意大利文，74页[29] D.米勒一种逻辑程序设计语言，具有抽象、函数变量和简单的统一。在ELP的Proc.，LNCS的第475卷，第253-281页。Springer-Verlag，1991.[30] D. Miller，G. Nadathur，F. Pfenning和A. 谢德罗夫 统一证明是逻辑程序设计的基础。Annals of Pure and Applied Logics，51：125[31] T. Nipkow和C.普雷霍弗高阶重写和等式推理。In W. Bibel和P. Schmitt，编辑，自动演绎-应用的基础。卷一：基础。Kluwer，1998年。[32] M. 冈田 型组合系统的强正规化性 λ演算与任意收敛项重写系统在ISSAC的Proc.，第357-363页中。ACM Press，1989.[33] F. Pessaux和X.勒罗伊基于类型的未捕获的数据分析。ACM Transactions onProgramming Languages and Systems，22（2）：340[34] S.佩顿·琼斯。函数式程序设计语言的实现。普伦蒂斯·霍尔1987年[35] G. 普洛特金操作语义学的结构化方法技术报告DAIMI FN-19，计算机科学系，奥胡斯大学，丹麦，1981年。[36] 范奥斯特罗姆。Lambda Calculus with Patterns. Technical Report IR-228，Faculteit der Wiskunde en Informatica，Vrije Universiteit Amsterdam，1990.[37] D. A. Wolfram 类型的小句理论，剑桥理论计算机科学卷21。剑桥大学出版社，1993年。