交集类型的基础及应用

理论计算机科学电子笔记136（2005）43-56www.elsevier.com/locate/entcsTowards an IntersectionTyped Systemà la Church路易吉·利科里INRIA Sophia Antipolis，法国西蒙娜·龙奇·德拉罗卡意大利都灵大学摘要在本文中，我们提出了一个舒适的完全类型的lambda演算的基础上著名的交叉类型系统的纪律，证明不仅可行，但很容易;本系统是对应的教堂的类型分配系统发明的Coppo和Dezani。关键词：类型lambda演算，交集型，Church型赋值系统，Curry-Howard对应1介绍交集类型赋值系统（英语：Intersection Type Assignment System，缩写：Λu演算）是一组用于将交集类型赋值给无类型λ演算的项的推理规则。交集类型是句子的隐含片段和连接片段的公式化谓词逻辑语法和类型规则如图1所示。相交类型是由Coppo和Dezani在70年代末引入的从那时起，交集类型已经被卓有成效地用于设计编程语言的静态语义（例如，G. [12]和面向对象[11]），用于表征有趣的λ-项类（e.G.强规范化的[10]），以及研究各种无类型λ-演算的指称语义[1，2]。1571-0661 © 2005 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2005.06.01544L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56拉乌夫M：：= x| λx.M|MM σ：：= α |σ →σ |σ ∧ σ设α在可数常数集V上的值域为V，且r ∈ {x1：σ1，.，xn：σn}，其中ij意味着xi/xj。运算符““优先于“→“。类型规则x：σ∈ Γ（变量）Γx：σΓ，x：σ1ΣM：σ2Γλx.M：σ1→σ2（→I）ΓM：σ1→σ2ΓN：σ1ΓM N：σ2（→E）Γ►∧M:σ1Γ►∧M:σ2Γ►∧M:σ1∧σ2（一）Γ►∧M:σ1∧σ2Γ►∧M:σ1（EL）Γ►∧M:σ1∧σ2ΓεM：σ2（英、俄）图1.交叉口类型分配系统Λu在文献中有许多版本的交叉型分配系统。在这里，我们选择了Krivine [ 9 ]提出的 请注意，与大部分在文献中提出的系统，例如[6]，在这个系统中，连接符既不是交换的，也不是结合的，也不是幂等的，这最后一个选择已经完成，因为我们正在寻找一个类型化版本的微积分，并且在这种设置中，将类型视为语法实体是很自然的。 在任何情况下，这种选择都不会对系统的可类型化能力产生任何影响，众所周知，这是所有且仅强规范化项的特征[9]。按照一个标准的术语，让我们称之为laCurry为一个将类型分配给非类型化术语的系统，而laChurch为一个将类型分配给类型化术语的系统，即。e.其中类型是术语语法的一部分。与Curry的其他类型赋值系统不同的是，Λu没有自然的对应物教堂经典的例子是Λu中的多态恒等式，它具有L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）4345？以下类型派生：x：σ1x：σ1λx.x：σ1→σ1（→I）x：σ2x：σ2λx.x：σ2→σ2（→I）（一）λx.x：（σ1→σ1）但是使用用于引入交叉类型的朴素对应规则laChurch是不可分型的[8]。x：σ1x：σ1λx：σ1.x：σ1→σ1（→I）x：σ2x：σ2λx：σ2.x：σ2→σ2（→I）（一）λx：.x：（σ1→σ1）根据Curry-Howard同构，λ-项必须记录它的型导子的形状。λ-calculià laChurch的简单解决方案会导致不完整性，在这个意义上，最终的类型化系统具有较少的可类型化能力[12]第一个例子：问题是，正如熟练的读者可以理解的那样，存在非语法指导的规则，这些规则将λ项与其类型推导断开（因此失去了Curry-Howard对应性）。重要的是要指出，这个问题并不依赖于所选择的交集类型赋值系统;事实上，文献中提出的类型赋值系统中没有一个.我们的目标是建立一个带有相关类型系统的类型化λ-演算à laChurch，使得底层的无类型演算就是λ-演算à laCurry，并且它与类型赋值系统的关系遵循[3]中设计的即必须满足以下要求：(i) 存在一个擦除函数J，擦除项的类型信息，使得若M是类型项，则J（M）∈Λ;(ii) 类型证明和类型赋值证明是同构的，即：e.将擦除函数J应用于类型化证明中的所有项，产生正确的类型赋值证明，并且获得每个类型赋值证明。通过擦除从打字机上删除。此外，我们希望交集演算继承交集演算的所有性质，即：(iii) 主题减少;(iv) 可类型化术语的强规范化;46L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56加上以下几个：(v) 类型的单一性(vi) 类型重构和类型检查的可判定性。文献中提出的建议没有一个能满足所有给定的要求。[12]和[11]中提出的类型化语言在类型分配方面是不完全的，[4]，[13]和[16]中的类型化语言不满足要求1，而[17]中的语言不满足要求2。为了构建这样一个演算，我们尝试设计一个演算，其中类型不仅依赖于上下文的新“命令式”公式，现在将类型分配给给定位置的术语变量，而且还依赖于存储的新概念，它记住了存储器的进一步任务是记录校样的形状。因此，存储是一个真正类型化的证明演算，可以通过适当的归约规则来执行;这种演算中的归约模型是割消。存储演算本身可以被定义为直觉主义逻辑的蕴涵和合取片段的装饰。所以它编码了一组严格大于对应于交集型导子的证明（见[15]）。最后，可以构建所需的交集类型演算，其中存储可以被视为术语的模态。非常粗略地说，模态是 一个一元运算符，可以用来修饰一个逻辑公式，说明关于它的可证明性的附加信息。 特别是信息由模态进行的可以是关于证明的结构的元理论信息，例如模态！在线性逻辑[7]中，这表示前提的可能的非线性使用在[14]中，类型化语言具有已经显示，其中术语上的模态是类型上的模态的对应物，并且它用于表征可以非线性发生的变量。在这里，模态用于描述类型派生的结构.事实上，将λ-项和存储打包在一起作为模态限制了存储仅描述交集类型导出。 所以，与类型（σ1→σ1）<$（σ2→σ2）的恒等式现在是项：λx：0.x，其中0是位置，并且该项的模态是：（λ0：σ1. 0）λ（λ0：σ2. 0）。这样得到的类型化λ-演算满足上述所有要求。特别是类型重构和类型检查是可判定的，算法也相当简单。本文的结构如下：第二节给出存储演算，第三节给出完整的交型λ演算，第四节列出它的性质，特别是它的类型检查和类型推理算法。结论提出了一些最终的考虑。L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43472类型化证明演算如果我们把连接词→看作是蕴涵，把连接词看作是连接词，那么交集类型的句法就是直觉逻辑的蕴涵和合取片段（L→，然而交叉口类型分配系统并不对应，Curry-Howard意义上，这个逻辑，因为在本节中，我们定义了一个类型化的微积分，装饰了这种类型的证明。一种逻辑。该演算是类型化的λ演算，但它是建立在变量和位置上的。事实上，它将被用作一个（特定的概念）存储，用于记住位置和类型之间的关联以及类型派生的结构。ΛP的π定义2.1(i) 类型位置（或类型地址）的范围超过Nat。(ii) 交叉点类型定义如下：σ：：= α|σ → σ|σ ∧ σ其中α的范围是可数的常数集V(iii) 上下文是位置和类型之间的有限关联，由以下语法定义：r：：= 0| r，i：σ(iv) 树存储被标记为一元/二元树，定义如下：：：=i| λ1：σ。∆|语法规则 （用于语法定向规则）∆ ∧ ∆|（|交集\（用于交集规则）(v) 树存储器中的自由位置的集合Fl（λ）是λ项中的自由变量的集合的概念的自由存储在下面的内容中，符号“”分别表示术语、类型、上下文、类型位置和树存储的语法相等48L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56i：σ∈ΓΓPi：σ（变量）r，i：σ1P：σ2[0001][001][002][001][01][02][01][02][01] σ1→σ2（→I）Γ<$P<$1：σ1→σ2Γ<$P<$2：σ1ΓP12：σ2（→E）ΓP1：σ1ΓP2：σ2P（一）Γ►P∆ :σ1∧σ2ΓP（σ ：σ1（EL）Γ►P∆ :σ1∧σ2ΓπPπ\：σ2（英、俄）图2.证明演算ΛP.ΛP的类型系统该系统证明形状的判断：P直觉：在判断中，类型上下文Γ将交集类型分配给类型的存储位置;树存储保持跟踪所使用位置的类型以及类型证明的骨架的书面痕迹，其中一个证明的骨架是通过擦除所应用规则的名称以外的所有信息而得到的树。因此，树型存储器扮演着“路线图”的角色，e. 回滚）派生树。打字规则如图2所示。以下是一些意见• （Var）为自由位置提供类型;• （→I）树存储库在一个新的树存储库中演化，该新的树存储库被位置i的绑定所丰富;• （→E）观察到前提的两个类型存储在结论中变成子树存储（隐藏的应用操作符是根）;• （XNUEI）（XNUEL）和（XNUER）是引入/消除交叉类型的三个标准规则;注意，为了跟踪在交叉消除中选择哪个分支（并保持类型的唯一性），树存储是用两个占位符标记（和\表示要选择的正确分支。ΛP的约简语义由于ΛP中的每一项都是对L→，L →的证明的修饰，语言的归约规则对应于逻辑的割消步骤。因此，→-cut消去法产生了以下归约规则（类似于L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）4349标准β规则）：（λ 1：σ。1）而切消则产生了以下两个归约规则：（（12）→π11（12）\→π22约简关系→π是约简规则的上下文闭包-π，-π1，-π2。特别地，我们用→π表示两个规则→π1和→π2的上下文的、自反的和传递的闭包。我们还进行模α转换，这可以在我们的ΛP中重新表述作为以下规则的对称、自反、传递和上下文闭包：λ11：σ。σ→ αι λι2：σ。n [ι2/ι1]，如果ι2/∈Fl（π）当删除项时，Λu→中的每一个类型推导都对应于L→，L →中的一个证明，但反之则不成立，因为规则（→I）对应于两个前提的证明上的一个元理论条件。关于Λu→和L →之间关系的完整分析，参见[15]。这里只需要注意，例如，由树存储（λ0：σ）编码的证明的骨架。0）1如下：（V ar）（→I）（V ar）（一）其不能是任何交叉类型分配派生的骨架。例2.2我们给出了树存储（λ0：σ1. 0）λ（λ0：σ2. 0）。0：σ1P0 ：σ1（变量）（→I）0：σ2P0 ：σ2（变量）（→I）ΔPλ0：σ1。0 ：σ1→σ1ΔPλ0：σ2。0 ：σ2→σ2（一）λ0：σ1. 0）λ（λ0：σ2. 0）：（σ1→σ1）<$（σ2→σ2）3交型系统Λt交集类型系统Λt是从特定的上下文概念开始构建的。事实上，现在上下文将类型关联到给定位置的变量，即。例如，它既将类型关联到变量，又获取一个自由的loc。用于存储变量本身。这个技巧允许在规则（→I）中只记住位置，即存储在50L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56树存储，由系统与键入的术语并行构建。 这样，底层项就是经典无类型λ-演算的项。此外，由于树存储描述了类型派生的结构，我们得到了类型的可判定性。Syntaxof Λt∧.定义3.1（i）类型-位置、交叉点类型和树存储的定义见定义2. 1。(ii)上下文是给定位置的变量和类型之间的有限关联，它们定义如下：r：：= 0| Γ，x@i：σ交集类型项的集合Λt的定义如下：M：：= x| λ x：μ M|M M类型系统的Λt。交集型演算Λt在某种意义上是模态演算，其中ΛP的项表示模态。类型化系统证明以下形式的语句：ΓM@：σ其中，Γ是上下文，M∈ Λt∈ΛP。直觉：在判断中，类型上下文Γ将交集类型分配给M分配的自由变量在自由存储位置中;树存储保持跟踪所使用位置的类型以及派生树的骨架的写入轨迹。树型存储器扮演着回溯路线图的角色（即。e. 回滚）派生树。类型规则如图3所示。以下是一些意见• （Var）为给定位置的自由变量提供类型;• （→I）是一个准经典的抽象规则，但它只记录了与抽象变量相关联的类型位置;树存储库在一个新的树存储库中演化，该树存储库丰富了位置i的绑定;• （→ E）是一个准经典的应用规则;观察到前提的两个类型存储在结论中变成子树存储（隐藏的应用算子是根）。• （σ1）是最重要的规则;给定M证明类型σ1和类型σ2的两个判断（两者都在相同的上下文Γ中证明，但具有不同的树存储器σ1和σ2），我们可以将交集类型σ1 <$σ2分配给M，L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）4351x@i：σ∈Γx：σ（变量）Γ，x@i：σ1M@i ：σ2Γ π（λx：1.M）@（λ i：σ1.σ1→σ2（→I）ΓM@ σ1：σ1→σ2 ΓN@ σ2：σ1Γε（M N）@（ε1ε2）：σ2（→E）ΓM@ σ1：σ1ΓM@ σ2：σ2ΓM@（1<$2） ：σ1<$σ2（一）ΓM@：σ1<$σ2ΓM@（（λ）：σ1（EL）ΓM@：σ1<$σ2ΓM@（σ\） ：σ2（英、俄）图3. 交叉类型系统Λt。上下文Γ，但是在新的树存储器中。 在这一点上，λ项M失去了与它的证明的一一对应。幸运的是，新的树存储跟踪派生并保证类型的唯一性• （EL）和（ER）是消除交叉点类型的两个标准规则。在这种情况下，λ项M也失去了一一对应性但是证明是由树存储记忆的，这要归功于两个占位符（和\，指示应用的规则。Λ t的归约语义。为了保持词项和情态之间的正确关系，约简同时在词项和树存储上进行。形式上，Λt的归约关系→β i是以下的上下文闭包：缩减规则：（（λx：1.M）N）@（（λ i：σ. 1）M@（（π1π2）→π1M@π1M@（π1π2）\→π2M@π252L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56我们还进行模α-转换，这是以下规则的对称、自反、transitive和上下文闭包：（λx@i.M）@λ →α（λy：i.M[y/x]）@λ如果y/∈Fv（M）M @（λ1：σ. σ）→αι M [ι2/ι1]@（λι2：σ. [ι2/ι1]），如果ι2/∈Fv（λ）例3.2[经典多态恒等式]我们在树存储中展示了经典多态恒等式λx：0.x（λ 0：σ1。0）λ（λ 0：σ2. 0个）x@0：σ1x @ 0 ：σ1（变量）（→I）x@0：σ2x @ 0 ：σ2（变量）（→I）► （λx：0.x）@（λ0：σ1.0）：σ1→σ1► （λx：0.x）@（λ0：σ2.0）：σ2→σ2（一）► （λx：0.x）@（（λ 0：σ1. 0）λ（λ 0：σ2. 0））：（σ1→σ1）<$（σ2→σ2）例3.3[多态自应用]设Γ <$x：0：σ2，其中σ2<$（σ1→σ1）<$σ1。我们证明了经典自应用λx：0. xx在树存储λ0：σ2中的多态类型导出。（（0）（0\）.0 ：σ2时的ΓΓx：（（0）：σ1→σ1（EL）Γx@（0\） ：σ1（英、俄）（→E）Γ（xx）@（（0）（0\） ：σ1► （λx：0.x x）@（λ 0：σ2. （（0）（0\））：σ2→σ1（→I）注意树存储是如何精确地记忆类型派生的骨架4证明理论发展系统Λt具有我们所要求的所有性质。为了列出它们，我们需要定义一个擦除函数，连接Λt和Λu。定义4.1[擦除]将tJ：Λti →Λb归纳定义为上下文和树存储，如下所示：L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）4353ΔΔΔΔΔJ（x@_）=xJ（（λ x@i. M）@_）=λ x. J（M@_）J（（M N）@_）=J（M@_）J（N@_）J（）=J（r，x@i：σ）=J（r），x：σ为系统ΛT定义的证明框架的概念可以自然地扩展到系统Λt。定理4.2（Galleria）（i）（同构）(a) 若D：ΓJ（M@M）：σ，且D和DJ具有相同的骨架;(b) 若D：Γ ≠M：σ，则存在 DJ， MJ和σ，使得 DJ：ΓJ≠MJ@σ ：σ，且dJ（MJ@σ）=M，dJ（ΓJ） =Γ，且D和DJ具有相同的骨架.(ii) （主语归约）若ΓP@：σ，且P@→βQ @J，则 ΓQ @ JJ：σ，其中J→πJJ。(iii) （强正规化）Γ M@：σ当且仅当M@是强正规化的。(iv) （Typing的唯一性）如果ΓP@：σ，和ΓP@：σJ，则nσσJ。(v) （类型重构）给定上下文Γ、类型存储Γ和项M，则存在类型σ，使得Γ∈M@Σ ：σ当且仅当Ty∈Σ（Γ， M @Σ）=σ。(vi) （类型检查）给定上下文Γ、树存储器 Γ、项M和类型σ，Γ <$M@σ ：σ当且仅当Typecheck<$（Γ， M @σ，σ） =true.由于树店的概念，这个画廊的4、5和6号物业得以实现。图4以ML样式显示了类型重构和类型检查算法.就Galleria的点1，2，3所列的性质而言，关键的性质是系统Λt_n与系统Λu_n之间的同构性质，这一性质可以很容易地用型导子的归纳法加以证明。主题约简和强归一化性质都是一致的。序列54L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56类型（Γ，M@）=Δmatch（M@m），（_@（（M1））<$σ1如果Typ∈<$（Γ， M@M1） =σ1<$σ2（_@（1\））<$σ2如果Type<$（Γ， M@1） =σ1<$σ2（_@（12））<$σ1<$σ2，若Type<$（Γ， M@1） =σ1，且Type（Γ， M @σ2） =σ2（x@-）σ如果x@i：σ∈ Γ（（λ x@i.M1）@（λ i：σ1. 如果Typen（（r，x@i：σ1），M1@n1） =σ2（（M1M2）@（n1n2））nσ2如果Typen（r，M1@n1）=σ1→σ2Type（r，M2@σ1） =σ1（_@_）否则返回false类型检查<$（Γ，M@<$，σ）=ΔType（r， M @）=σ图4.Λ t的类型重构和类型检测算法。5结论本文研究了交叉型指派系统的Church版本的设计问题。特别地，我们要求一种类型化语言，使得它与交叉类型分配系统的关系享有我们在[3]中提出的所有标准要求这种“好”对应的例子我们成功地设计了一种满足给定要求的语言，它主要基于两个工具：类型化的命令式概念，当类型被分配给变量对应用程序编程特别感兴趣的读者可能会反对L. 利口里S.Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）4355所使用的语言远远不能被称为答案可以是双重的。从编程语言的角度来看，在每一种类型化语言中，为了明确地写出术语的类型，用户在某种意义上需要显然，这里的类型派生比简单类型化的情况更加困难。但是如果我们考虑，例如，二阶类型λ-演算，为了写这个术语，Λβ。Λγ。λx：λα。α。x（β→γ），y∈<$β. 好吧（α. α）→（β→γ）有必要确切地知道引入和消除通用量化器的规则是如何工作的。然而，我们认为产生一种可用的语言并不是我们研究的问题的唯一理由。类型化系统和类型赋值系统之间的关系是一个重要的理论问题，它本身就很有趣。确认Simona得到了QSL的大力支持：Qualité et Srété du Logiciel，CPER，Région Lorraine，Nancy和INRIA; Luigi正在访问布莱顿苏塞克斯大学的信息学系;他要感谢他的东道主Matthew Hennessy和Vladimiro Sassone，以及整个信息学系为他们提供的理想工作条件。两位匿名推荐人也给出了有用的意见。引用[1] B和R都是H。，CoppoM. 和Dezani-CiancagliniM. “AFilterLambdaModelandtheCompletenessofTypeAssignmemt“，《系统分析》，48（4）：931-940，1983年。[2] CoppoM. 、Dezani-CiancagliniM. ，HonsellF. 和LongoG. “E x t e n d e T y p e S tr u c t ur e s and Filter Lambda Models ” ， Logic Colloquium '82 ，pp.241-262 ，1983 。[3] van Bakel S.，利口酒属，Ronchi Della Rocca S.，和Urzyczyn P.“[4] CapitaniB. ，VenneriB. “H y p erfor mu l soul，P a ralle l D e u c t i o n s and I n t ersec t i o n T y p e s“，Pr o c. BOTH 2001，ENTCS，50（2）：180-198，2001.[5] CoppoM. 、Dezani-CiancagliniM.λ-calculus“，N o t r e D a m e J. FormalLogic，21（4）：685-693，1980.[6] Dezani-CiancagliniM. ，GiovannettiE. 你还是我。“I n t ersec t i o n t y p es s，la m b d a -mo d el s and d Böhm t rees“. InMSJ-MemoirVol. 2“类型和程序的历史“，第2卷，第45 - 97页。日本数学会，1998年。[7] 让-伊夫·吉拉德 线性逻辑 理论计算机科学，50：1-102，1987。56L. 利口里S. Ronchi della Rocca/Electronic Notes in Theoretical Computer Science 136（2005）43-56[8] 我是J. R. “C op p o D e za ni t y p e s d o n t co r r e s p o n d t to p rop o si t o n al lo g i c “ ， T h e o r t i c al Co m p u t e r Sc i e n c e ， 28 （ 1-2 ） ： 23 5 - 2 3 6 ， 19 8 4 .[9] K riv ineJ. L. “L a m b d a-c a lc ul，ty pe es et t mo dèle s“，M a sson，1990年。[10] Po t ingerG. “A ty pe assig n me t forr the strom g l y n ormaliza b l e λ - t erms“，in：To H. B.《组合逻辑、lambda演算和形式主义论文集》，第561 -577页，学术出版社，伦敦，1980年。[11] 亲爱的B 、C. 和Turn er，D. ，N. “SimpleType-theoreticfundationsfororject-orienteddprogrammingg“，《实用程序汇编》，4（2）：207-247，1994年。[12] R eyn oldsJ. C. “D e s ig n of the prog r a mm i ng l a n g u a g e Forr s yth e“，in：A lgo l -lik e L anguages，O ' H e arn and T e nn e n t e d .s，Bir k h a u ser，1996.[13] R o n chiD ellaR occaS. “Int err sec t io n Typ e d L a m b d a - C a lc u l u s“，In Pr o c of ICTR S，EN TC S，70（1），2002.[14] S. R o n ch id ellaR occandL. 罗夫尔岛“L a m b da c a lc u l us and i n t u i t i o n i s t i c li n er logic“.StudiaLogica，59（3），1997.[15] RonchiDellaRoccaS. 并将R转换为L。“交叉逻辑“，P r o c。 参见CSL，LNCS2142，第414 -428页，Springer-Verlag，2001。[16] 我们都是J.B. ，DimockA. 、MullerR. ，和TurbakF. ，“A Calc u u s wi t h Poly mor phic andPolyvariant Flow Types”，Journal of Functional Programming，12（3），pp. 183-227，2002年。[17] 我们都是J.B. ，和HaackC. “Bran n c h i n g T y pes“，In for m a t i o n and d C o m p u t a t i on，200 X.