λµ-演算中的交集和并集类型

理论计算机科学电子笔记136（2005）153-172www.elsevier.com/locate/entcs中的交集和并集类型λµ-演算Daniel J. Doughnard1伍斯特理工学院Worcester MA 01609USASilvia Ghilezan2诺维萨德大学工程学院塞尔维亚Pierre Lescanne3LIP，E'coleNormaleSup'erieuredeLyonLyon，法国摘要Curry和Herbelin的逻辑结构是一个简单的系统，基于等式计算，体现了与经典逻辑的Curry-Howard对应关系。本文介绍并讨论了三种类型的λ µ µe的快速提取系统，它们都是带中间选择和不带中间选择的。λ µµe计算中的这一传统方法导致了数据集和非数据集类型的本质使用。关键词：输入选择类型，统一类型，λµµe-计算，经典逻辑，Curry-Howard对应。1电子邮件：dd@cs.wpi.edu2电子邮件：gsilvia@uns.ns.ac.yu3电子邮件：Pierre. ens-lyon.fr1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.06.010154D.J. Doughnut等人理论计算机科学电子笔记136（2005）153˜˜˜1介绍相 交 类 型 在 20 世 纪 70 年 代 后 期 由 CoppoandDezani[5 ， 6] ，Pottinger[19]andSal l′e[23]引入lambda演算。相交类型赋值系统的设计是为了比基本函数或简单类型的系统键入更多的lambda项;事实上，这些相交类型系统可以精确地表征所有强规范化lambda项。此外，这些系统还适用于分析λ-模型和λ-项的各种正规化性质.范·巴克尔（van Bakel）对早期研究进行了总结[24]。Barbanera等人[1]将联合类型添加到交叉类型系统中。这项工作的动机是观察到联合类型自然出现在指称语义中，并且它们可以为某些术语生成更多信息类型。但是，不能使用联合类型键入比仅使用交集类型更多的术语。也就是说，具有交集和并集类型的系统也精确地表征了所有强正规化项。在20世纪80年代和90年代初，Reynolds探索了[20]关于语言福赛斯）。Pierce [18]探索了联合类型在编程中的使用，例如作为变体记录的泛化。最近，Buneman和Pierce [3]展示了联合类型如何在半结构化数据联合类型的查询语言设计中发挥关键作用在Curry-Howard对应下，直觉逻辑中可证明的公式与简单类型lambda演算中的类型一致。Gri Bern在他1990年的POPL论文[13]中将Curry-Howard对应扩展到经典逻辑，通过观察经典重言式暗示了某些控制算子的类型。这开启了一条活跃的研究路线;特别是Parigot的λµ演算[17]体现了基于自然演绎的经典逻辑的Curry-Howard对应。与此同时，Curien和Herbelin [7]在[14]的早期工作的基础上，定义了系统λµµ。与Parigot的λµ演算不同， λ µ 演 算 将 其 类 型 系 统 建 立 在 一个 针 对 类 对 数 的 系 统 中 ， λ µ 中 的 系 统 表 示 一 个 λ µ 演 算 证 明系 统 中 的 推 导 ， 而 归 约 则 反 映 了 割 消 的 过 程 。在本文中，我们叙述了我们在一种无类型语言中扩展λ µµ的经验，我们建议称之为GEMINI（类似的尝试见[21]），然后为这种扩展的语言导出一个类型系统，它刻画了强规范化项。我们很自然地通过引入交集类型来丰富Curien-Herbelin简单类型系统。但事实证明[9]，为了完全D.J. Doughnut等人理论计算机科学电子笔记136（2005）153155˜˜˜˜˜描述所有强规范化的非类型化λµµ项（与在标准λ-演算中的情形）。值得注意的是，Laurent [15]最近独立地开始通过定义一个与我们非常相似的类型系统来分析λµ我们提出的系统还享有Subject Reduction属性，该属性通常在存在联合类型时失败Pierce [18]强调了主语归约在联合类型存在时的失败，[1]展示了如何通过适当地限制归约的概念来恢复这一属性。 Wells et. [25]探索了一种λ演算，它作为优化编译器的类型化中间语言的基础;他们使用了一种新的交集和并集类型以及Cowow类型的公式来编码控制信息。这个系统遵循主体还原，更好地理解我们的系统和他们的系统之间的关系在最近的两篇论文[10，11]中，Dun Field和Pfenning研究了一个类型系统，其中包括他们的语言是一种按值调用的语言，他们的类型系统和类型赋值算法以有趣的方式利用了这一点。特别是，他们的系统满足了主语归约的一个版本：他们分离出一个“限定替代”的概念，这个概念似乎与我们下面的“限定”类型有关。这些系统之间的精确关系是未来研究的一个领域。(We感谢其中一位推荐人让我们注意到了这项工作本 文 的 结 构 如 下 。 第2 节 处 理 λµµ 的 无 类 型 语 法 ， 我 们 称 之 为GEMINI。在第3节中，我们讨论了对应于λµµ类型的结石。在第4节中介绍了三种类型的赋值系统，它们是λµµ的交集和并集类型的扩展。它们的性质在第5节中讨论。2Gemini的语法在本节中，我们介绍GEMINI语言，它是[ 7 ]中介绍的Curien和Herbelin的λµµ演算的无类型版本我们确定了三种语法类别：调用者，被调用者和胶囊（在[7]中，这些分别被称为术语，上下文和命令）。让r、e和c分别在调用者、被调用者和胶囊上变化，我们有156D.J. Doughnut等人理论计算机科学电子笔记136（2005）153˜˜˜˜˜r ： ： = x| λx.r|µα.ce：：=α|r·e|x.cc：：= re主叫方、被叫方和胶囊一起被称为G项。 那里在这个系统(i) 由拉丁变量x，y，.表示的调用者变量的集合V ar r。它们表示输入，特别是它们被λ-抽象或μ-抽象所约束，(ii) 被调用方变量的集合V是由希腊变量α，β，.它代表延续，可以被μ-抽象所约束。在λμ中，它们被称为μ-变量。GEMINI的核心是由capsulescallercallee callee组成的，其中caller和callee是两个组件。调用者基本上执行两个操作之一，要么从另一个实体（被调用者）获取数据，要么要求被调用者替换其内部被调用者变量之一。被调用方可以要求调用方替换其指定的内部调用方变量之一格艾米尼准确有三个归约规则，使这种解释更（λ）λx.r <$rJ·e<$ z<$$>，rJ<$μ<$x. ⟨rǁe⟩⟩（µ） µα.cezc，[α<$e]（µ）rµx.czc，[x<$r]请注意，对于形式为µα.cµx.c的项，规则（µ）和（µ）的应用可能不明确。这将在第2.1小节中讨论。 如果一个人优先考虑（µ）或（µ），那么它就是通过v-u-u。还要注意的是，通常的β-归约操作在微积分中很容易被发现，λ-步紧接着是μ-步。这将在第2.2小节中讨论。当然，上面的替换被定义为避免变量捕获。在本文中，我们对变量使用它说，在一个语句或表达式中，没有子表达式，一个变量既是自由的又是受约束的。 符号λ、μ和μ都以明显的方式绑定变量。自由变量和约束变量的形式定义与预期的一样。对于每个G项r，e和c，我们定义两组自由变量，即Fvr（r）、Fve（r）、Fvr（e）、Fve（e）、Fvr（c）和Fve（c）。 例如D.J. Doughnut等人理论计算机科学电子笔记136（2005）153157˜˜Fvr（ΔxΔμα）。y<$α<$·β<$）={x，y}Fve（ΔxΔμα）。y从约简规则中，可以很容易地推导出G项的正规形式是由以下抽象语法生成的r nf：：= x| λx.r nf|µα.cnfenf：：=α|rnf·enf|µx.cnfc nf：：=xα|x| λx.r nf2.1连续性故障作为重写演算，GEMINI（即使在它的类型化版本λµµ中）在µ和µ换算之间有一个基本的临界对事实上，微积分本质上是这反映了经典微积分中截消元法的不连续性。作为一个简单的例子，观察胶囊好吧z1 α2β2β 3可简化为和。这不仅仅是对一个众所周知的事实的反映，即按名称调用和按值调用的等式理论是不同的。它反映了语言的强大表达能力：包含几个胶囊的单个术语可以包含几个完整的计算过程，并且μ和μ的减少都是在它们之间进行的自由控制。所以纯约化的组合数学是非常复杂的。在这种情况下，强规范化计算可以如此容易地通过我们稍后介绍的类型系统来表征，这当GEMINI的约简被约束为按名称调用或按值调用时，系统是一致的。2.2λ-演算的编码不难看出，GEMINI作为一种编程语言是图灵完备的，因为无类型的λ演算可以很容易地编码到它里面。我们不给出一个形式化的发展，而是简单地展示如何在演算中编码一些熟悉的λ项。记法。 如果m和n是调用者，则令m n表示调用者项μα。⟨mǁn·α1。（当然，α在m和n中不是自由的。）例2.1（经典β还原）（λx.r）λx.rzzµ，，α. r[x←s]158D.J. Doughnut等人理论计算机科学电子笔记136（2005）153˜˜例2.2（Eta减小）注意，µα。你好好吧⟨m ǁn·β⟩ ǁα ⟩µzµ，α. ⟨mǁn·α⟩≡ 门恩根据Curien-Herbelin从λµµ到λµ的翻译，这对应于λµ的规则（µ-η）。请注意，这是λμ中的规则，而不是GEMINI中的规则。然而，我们可以认为GEMINIη是GEMINI，（η µ）µα。如果α在r中不是自由的，则<$r<$α <$→r（ηµe） x. 如果x在e中不是自由的，则x→e例2.3（自再生项）设w为λx.x<$x。然后ww ≡µα。<$λx.x<$x<$w·α<$zzµ，，α. wzzµ，，α. 1. wzz。，，。 .所以ww对应于λ-演算中的项（λx.xx）（λx.xx） 注意我们还有ww ≡µα。<$λx.x<$x<$w·α<$zzµ，，α. wµzw，µ mw正如我们在例子2.2中看到的那样。例2.4（定点）如果f是一个调用者变量，设uf为λx.f<$（x<$x）。然后u f u f 。uf≡ µα。<$λx.f<$（x<$x）<$uf·α<$zzµ，，α. fηzf，n（uf<$uf）因此，项λf.uf<$uf对应于固定点组合子Yλf. （λx. f（xx））（λx. f（xx））在lambda演算中。3经典型肾结石在介绍经典的证明和λµµ程序之间的Curry-Howard对应之前，让我们先介绍演绎系统，它是一种特殊的蕴涵演算。首先，让我们考虑经典命题逻辑的蕴涵片段的一个基本的隐式演算这些命题生成如下：D.J. Doughnut等人理论计算机科学电子笔记136（2005）153159z►A→B，AA A、A，B：：= p|A→ Bp表示命题变量，A和B是任何命题。序列是形式为Γ的表达式，其中Γ和是命题的集合。在Γ中的命题是假设，而在Γ中的命题是结论。标准的微积分是由公理生成的（ax）Γ，A，A按左右引入规则Γ ► A,∆Γ，B（→L）Γ，A→B与切割规则Γ►A,∆ Γ,A►∆Γ►∆Γ，AB，ΓA→B，（切）（→R）在这种情况下，皮尔士定律有一个简单的证明（ax）A、B、A，，（→R）（A→B）→AA.A.，J（ax）（→L），（→R）►（（A→B）→A）→AJ在这个证明中，我们把有效命题装箱，即，在规则的后件中的命题被规则分裂（如果我们自下而上阅读证明），或者由规则创建（如果我们自上而下阅读证明）。带主动命题的在规则中把主动命题显式化是很方便的。这就给出了一个具有主动命题的经典蕴涵演算。图1中给出了这种微积分的规则。在每一条规则中，主动命题（Girard意义上的stoup中的命题当应用一个规则时，必须考虑主动命题在哪里很自然地，切割规则中的主动命题是被切割排除的命题，即，切割公式，换句话说，切割规则使新引入的命题（自下而上）成为主动命题。这意味着160D.J. Doughnut等人理论计算机科学电子笔记136（2005）153˜˜、、、（e-ax），，（r-ax）z R、、Γ，一阿斯塔纳，AΓ，A一 ，Γ ►一 ，Γ，Bz，r► ∆Rz R、、（→L）、ZR，（→R）Γ， A→B►∆zRΓ，AΓ ►A→B，Γ，一►∆（µm）zRΓ►B, ∆，，（µ）z R、Γ ► B ，zR、、、zrzr（cut）Γ ► ∆Γ ►一 ，Γ，一►∆Fig. 1. 带主动命题的序列微积分。在（cut）的后件中没有主动命题。因此，该演算有三种类型的序列：右有一个活动命题的序列，左有一个活动命题的序列，无活动命题的序列。 有两个规则（μ）和（μ）将一个带有主动命题的“”转换（自下而上）为一个没有主动命题的“”。 请注意，上面对皮尔士定律的证明它的规则（→R）的使用并不满足对主动命题的要求。为了在这个具有主动命题的微积分中找到皮尔士定律的证明，人们必须进行一些破解该演算将是对λ µ µ η的CurryH owardcorre spondence的基础。4类型分配系统经典的类型演算的形式为使用简单类型的GEMINI的类型分配系统的定义提供了框架这正是Curien和Herbelin [7]的类型系统λµµ，它将是我们构建交集类型的基础。调用者类型判断r：A的非正式解释是r表示类型A中的值;相应地，被调用者类型判断e：A的非正式解释是e表示期望类型A的值并返回答案的延续。胶囊返回的只是答案。在这种情况下，一个判断，如μα.c：A说，μα.c作为参数D.J. Doughnut等人理论计算机科学电子笔记136（2005）153161˜、、、、、、zrzr（cut）（A→B）→A，A<$B，A，，（µ）（A→ B）→A，A→ A，B，A（A→ B）→A，A，AA、B，z r，（→R）（A → B）→ A，A细介绍、、、（A→ B）→ AA →B，AzR（A → B）→A，A A、、、zR（→L）（A→ B）→A，（A→ B）→AA.A.zR证明树A、、、（A→ B）→ A（ A → B）→ A，AAzr（切割）（A→ B）→AA， ，（µ）（A→ B）→AA，z r，（→R）►((A→B）→A）→AzR图二. 具有有效公式的皮尔士A-continuation并返回答案。 如果我们非正式地将A-延拓空间表示为集合（A），那么这个μα.c就存在于集合（（A））中，而这样的项被赋予类型A的事实恰恰是命题与其双重否定等价的体现，因此我们处于经典逻辑的世界中对对称性的一般考虑应该引导我们在我们的系统中考虑并集类型和交集类型。 如果一个调用者r可以有类型AB，这意味着它表示同时存在A和B的值，那么它可以与任何可以接收A-值或B-值的被调用者交互：这样的被调用者自然会被期望有类型AB。到目前为止，我们只讨论了值的交集类型意味着被调用者的联合类型，这本身并不是交集类型范式的真正扩展。 但是任何可以作为调用者变量类型的类型都可以 是被调用项的类型（通过µ-构造）和任何可以被调用方变量的类型可以是调用方术语的类型（通过µ-构造）。因此，我们致力于为呼叫者和被呼叫者提供交叉点和工会。定义4.1类型集由语法从一组类型变量A，B：：= p|A→B | AB|A ∪ B162D.J. Doughnut等人理论计算机科学电子笔记136（2005）153˜˜其中p的范围是类型变量。调用者基是一组形式为x：A的语句，被调用者基是一组形式为α：A的语句;在每种情况下，我们都规定所有变量都是不同的。有三种类型的判断：、、、联系我们，J、、、r，e：AJc：（Γππ）其中r是调用者基础，并且其中r是被调用者基础。Q我们将始终考虑类型定义为模交换性和模结合性。4.1第一次尝试：一个朴素类型系统考虑一个标准的λ-演算的交型系统。在（自然演绎）逻辑的层次上，交集的规则只是合取的规则（也就是说，如果我们删除了这些项，只看公式）。正如我们所知，AB和AB之间的区别是，我们需要证人A、B和A/B的任期相同。我们可以想象GEMINI的类型系统使用相同的原理导出因此，该规则将基于该逻辑规则的形状：，阿格拉岛伊戈尔湾Γ，ABΓ ► A、B一个关键点是，由于在左边或右边引入交集不是逻辑推理，这些类型推理与stoup的概念，即活动公式的概念完全正交。 这意味着，在λµµ的上下文中，对应于这些规则的类型判断，我们应该写下几个不同的λµµ序列，它们的例如考虑Γ，A ►∆Γ，AB►∆左侧的公式A可以是活动公式的类型（即，被调用方的类型），或者它可以是调用方变量的类型，并且在后一种情况下，这种判断可以通过键入一个调用方或一个被调用方来实现。我们，就目前而言，D.J. Doughnut等人理论计算机科学电子笔记136（2005）153163˜˜˜˜˜这一个逻辑推理将产生如下三个不同的类型规则、、、、、、、、、r，e：A，zr，r，e：ABzRr，x：A，e：Tz，rr，x：AB，e：TzRΓ，x：Ar：T，z，rΓ，x：ABr：T，zR定义4.2[朴素系统]这个类型系统的公理和规则在图3中给出。让我们在这里提到，图3中仅限于→类型的类型系统正是Curien和Herbelin的λµµ[7]。众所周知，皮尔士定律在直觉上是不可证明的，因此不存在于λ - c演算中。Peirce的L a w is inhabitate in λµ µ m by the eterm λ x .µ a. x因为一个人可以在λμ、、、►λx.µα。xyJ[ 16 ] Ong和Stewart给出了λµ项λx.µα。[α]（x（λy.μβ. [α]y））作为皮尔士定律的 得到G项λx.µα。好吧x使用Curien Herbelin翻译[7]。它以一（μ）个单位减少到我们的单位，其中有sλ x.μ α 。 xy 在 [21]中，JeromeRoch et eau详细研究了这种翻译及其相互作用。因此，λµµ给出了类型（（A→B）→A）→A的更紧凑的宽度。实际上，λµµ中的λµ-terms在翻译中的形象并不是所有的调用者，而只是语法给出的G-terms：r λµ：：=x| λx.r λµ|µα。r λµ| µα。rλµ仍然在λµµ 中，不能键入所有的标准形式，例如，G 项λx.μα 。<$x<$x ·α<$（见第2节），这是一个标准形式，对应于λ项λx.xx在λµµ中不可键入。这是引入新类型赋值规则的原因之一。如上所述，模式L-Var、R-Var、L-Var和R-Var实际上分别描述了两个规则，一个是当相关的判断类型一个调用者，一个用于当关联的判断键入被调用者时。也就是说，我们应该知道活动公式可能位于Γ或在Γ内（这里我们暂时滥用了我们的记法惯例，即Γ和Γ只是变量类型绑定）。这是一个完全合理的打字系统。但正如Barbanera等人[1]所指出的，联合类型在技术上是困难的，例如主题缩减往往会失败。事实上，上述系统导致了主语归约的困难（更具体地说，似乎很难证明替换引理）。164D.J. Doughnut等人理论计算机科学电子笔记136（2005）153、、、（e-ax）， ，（r-ax）zR、Γ，α：A<$α：A，r，x：Ax：A ，、 、、zR、、z，rz，r（→L）、ZR，（→R）Γ，r·e：A→BzRΓλx.r：A→B，zRC ： （r，x：A （掌声），，（μm）Γ， µx. c：一 个小洞\J、、联系我们 ，zRc： （ α：A，α）， ，（µ）Γ►µα.c：A ，J、、zR（切）rr，x：Ar α：A，βΓ ► α：B，β（L−V ar）（R −V ar）r，x：AB ►∆、、、r，e：A、、、Γα：AB，、、、（比利时法郎）联系我们，：B，z，rz， r（孟加拉国）r，e：ABzR联系我们，zRr，x：A ► ∆r，x：B r► α，α：A（L−V ar）（R −V ar）、、、r，x：AB ►∆、、、Γ ► α，α：AB、、、r，e：Ar，e：Bz，rz，► ∆R（比利时法郎）联系我们，，zr，（孟加拉国）r，e：ABzR联系我们，zR图三. 一个朴素的类型系统。特别是，如果我们想证明：、 、、、、、、、、如果 r，x：AR：T ，和 Γ►s：A，则Γr[x←s]：T ，JJJD.J. Doughnut等人理论计算机科学电子笔记136（2005）153165Γ，x：A1r：T ，Γ，x：A2πr：T ，zR，，zR˜当假设的类型是使用CUL-Var导出时，我们会遇到一个问题：、、、Γ，x：A1<$A2<$、、、R：T，zR（L−V ar）自从知道、 、、价格：A1-A2 ，Jdoesn’t allow us to use the induction hypothesis on the、、、Γ，x：A ir：T ，J.J4.2第二次尝试：朴素系统的问题似乎是x：A<$B和α：A<$B形式的变量类型。由于在键入范式时，我们只需要被调用方的联合类型和调用方的交集类型，因此解决这个问题的第一个想法是禁止调用方的联合类型和被调用方的交集类型。这立即是一个失败，因为在存在μ和μ的情况下，任何可以作为被调用方变量类型的类型都可以作为调用方术语的类型出现，并且任何可以作为调用方变量类型的类型都可以作为被调用方术语的类型出现。但事实证明，如果我们简单地禁止其基包含形式为x：A<$B和α：A<$B的变量类型的类型判断，我们就得到了一个成功的系统。我们需要一个稍微更一般的概念，以确保我们可以通过类型的交集来定义调用方变量，而这些类型本身禁止重复，并且对于被调用方变量是双重的。定义4.3(i) 一个类型A如果是一个类型变量，一个箭头类型或者是A1<$A2，则它是一个类型定义的，每个A是一个类型定义的类型。一个类型A如果是一个类型变量，一个箭头类型或者是A1<$A2，则它是一个类型定义的，每个A是一个类型定义的类型。(ii) 一个基Γ是n-定义的，如果在每一个约束x：A在Γ中，A是n-定义类型。 如果在每个约束中，α：A在α中，则类型判断α是α-定义的，A是一个有限类型。(iii) 一个类型判断是有界的，如果它的类型基Γ和Γ是正的，并且分别定义。166D.J. Doughnut等人理论计算机科学电子笔记136（2005）153注意，在一个确定类型的判断中，我们并不坚持活动公式的类型是确定的。定义4.4的系统是从微积分的自然一般化中获得的系统，它禁止规则R-Var和R-L-Var，并坚持类型判断是有定义的。如前所述，模式L-Var和R-Var实际上分别描述了两个规则，一个用于关联的判断何时键入调用者，一个用于当关联的判断键入被呼叫者时。也就是说，我们应该知道活动公式可能位于Γ或在Γ内（这里我们暂时滥用了我们的记法惯例，即Γ和Γ只是变量类型绑定）。定义4.4[一个图4给出了这个类型系统的公理和规则。在下面的每个规则中，我们假设类型基是有定义的。4.3你好，你好，事实证明，规则<$L-Var和<$R-Var的存在使这个系统的推理变得复杂但不难看出，总是可以被推到类型树的叶子事实上，系统的等效公式完全删除了这些规则，并用更灵活的公理模式代替它们。定义4.5中的系统是从基本系统通过用更灵活的公理e+-ax和r+-ax替换规则L−Var和R−Var而得到的系统。这个系统很好地适应了基于活动公式的微积分，因为所有的规则都涉及与活动公式相关联的项，而不是前两个系统，其var规则改变了活动项的类型基础，同时保持项的类型相同。最后，请注意，尽管我们禁止调用者变量具有联合类型，但由于其类型规则μ，我们确实有具有联合类型的调用者术语。联合类型的这个（受约束的）版本很有趣，因为它具有Subject Reduction属性。定义4.5[系统管理]图5给出了这个类型系统的公理和规则。每个规则中下面我们假设类型基是有定义的。引理4.6定义4.4和4.5中的规则产生相同的类型判断。D.J. Doughnut等人理论计算机科学电子笔记136（2005）153167、、、（e-ax）， ，（r-ax）zR、Γ，α：A<$α：A，r，x：Ax：A ，、 、、zR、、z，rz，r（→L）、ZR，（→R）Γ，r·e：A→BzRΓλx.r：A→B ，zRC ： （r，x：A（掌声），，（μm）Γ， µx. c：一 个小洞\J、、、联系我们，zRc： （ α：A，α）， ，（µ）Γ►µα.c：A ，J、、zR（切）rr，x：A►∆（L−Var）r，x：AB ►∆、、、r，e：A、、、、、、（比利时法郎）联系我们，：B ，z，rz， r（孟加拉国）r，e：ABzR联系我们，zRΓ ► α，α：A（R−Var）、、、、、、Γ ► α，α：AB、、、r，e：Ar，e：Bz，rz，► ∆R（比利时法郎）联系我们，，（孟加拉国）r，e：ABzR联系我们，zR见图4。 一个证据首先，我们观察到规则e+-ax和r+-ax对于基本系统是可容许的。这一点可以通过考虑以下规则来明确：R − V ar.接下来，我们证明了在存在e+-ax和r+-ax的情况下，规则L−Var和R−Var可以被消除。这是因为任何对L-Var或R-Var的使用都可以在类型树中向上推，直到它正好应用在公理之后。所以用e+-ax和r+-ax代替旧的公理就足够了。Q168D.J. Doughnut等人理论计算机科学电子笔记136（2005）153，，（e+-ax），，（r+-ax）Γ， α：A i <$α：A1<$··<$A n，<$Γ，x：A1<$··<$A n<$ x：A i ，JJ......联系我们，r，e：Br，x：Ar：z，rz，r（→L）、ZR，（→R）Γ，r·e：A→BzRC ： （r，x：A（掌声）、（µm）Γ， µx. c：一 个小洞\J、、zRc：（Γ） α：A，α）， ，（µ）Γ►µα.c：A ，J、、Γλx.r：A→B ，zRzR（切）r、、、r，e：A、、、、、、（比利时法郎）联系我们，：B，z，rz， r（孟加拉国）r，e：ABzR联系我们，、、、、、、r，e：Ar，e：Bz，rz，► ∆R（比利时法郎）zR、、联系我们，（孟加拉国）r，e：ABzR联系我们，zR图五. 系统M5M的性质对于本文，我们仅使用 类型系统管理工具。我们需要的第一个属性是交集和并集规则在这个意义上，如果规则结论中的判断是可导出的，那么假设中的每个判断都是可导出的正是在这里，我们收获了我们对限定基础的限制的好处。没有这个限制，引理是假的。引理5.1（消元） 、、(i) 如果Γr：A1<$A2，，则对于i= 1，2，Γr：A i ，J.，\，J，\，J(ii) 如果Γ，e：A1，则对于i = 1，2，Γ，e：A i 。JJD.J. Doughnut等人理论计算机科学电子笔记136（2005）153169证据对于part 1，我们只是观察到，唯一可以用来、、、推导出Γr：A1<$A2，其中R是r+-ax和R+-ax。 在后一种情况下，J是直接的;在前一种情况下，结果是事实的后果。我们考虑的是模结合性和模交换性。最后一个推论不可能是μ，这是我们假设基是有定义的直接结果。也就是说，因为基不能有α：A1<$A2形式的假设，所以假设的导数必须看起来像、、、你好r、、、µα。您的位置：电驴大全>电影>A2J，J你好电话：021-8888888J也就是说，一个实例是WARR。这就完成了引理第一部分的证明。第二部分的证明是类似的。Q下面的技术性质支持主体归约（定理5.6）。引理5.2（上下文扩展引理）设Γ Γ J和Γ J。(i) 如果Γ、、、r：A，，则Γj、、、R：A ，J.，\，J ，\，J(ii) 如果Γ，e：A 则r J，e：A 你好J J(iii) 如果c：（Γ），则c：（ΓjJ）。引理5.3（上下文限制引理）(i) 如果Γ、、、r：A，n，则rTFvr（r）n 、、、R：A ，Fve（r）.，\，J，\，J(ii) 如果Γ，e：A，则为T Fvr（e），e：AT Fve（e）。J J(iii) 如果c：（Γ T v r（c）），则c：（Γ T Fvr（c））= T Fve（c））。引理5.4（生成引理）、、、(i) 若Γ<$λx.r：i∈IAi→Bi ，则Γ，x：A i，、、、r：B i，B i。，JJ、、、、、170D.J. Doughnut等人理论计算机科学电子笔记136（2005）153、(ii) 如果Γ， r·e：i∈IA i→ Bi，则Γr：Ai，A i和 Ti，e：Bi- 是的JJJ(iii) 如果Γ、µα.c：i∈IAi 、，α，则c：（Γαα：A i，α）.JD.J. Doughnut等人理论计算机科学电子笔记136（2005）153171˜˜(iv) 如果Γ，、µx.c：\i∈IAi、则c：（r，x：A i）。J引理5.5（替换）、、、、、、(i) 如果Γ，x：B <$rJ：A，B且Γ < $r：B，那么，，\，J\JΓ < $rJ [x←r]：A ，J.\，J、 、、(ii) 如果ΓrJ：A ，α，α：B和Γ， e：B，则，\J，\JΓrJ [α←e]：A ，J.\(iii) 如果r，x：B，，JeJ：A和Γ、、、r：B ，那么，，\，J\Jr， eJ [x←r]：A.\，J、 、、(iv) 如果Γ，eJ：A α：B和Γ，e：B 那么，，\J，\Jr， eJ [α←e]：A。J我们的类型系统享有主体归约属性，对于具有无限制归约的演算，也就是说，即使存在（µ，µ）临界对。正如在引言中提到的，这在[1]中已经被证明是在具有联合类型的系统中实现的定理5.6（主语归约[9]）如果c：（Γ π π）且 c → cJ ，则cJ：（Γ π π）。所有强正规化项的可类型性是一些传统的具有交集类型的λ好的定理5.7（强正规化[9]）所有的强正规化项我的名字在墨西哥很常见。6结论我们定义了三个交集和并集类型的系统，根据方程和定义了一些方法。在最后的系统中，M*。与前面研究的具有联合类型的系统相比，作为联合类型的系统可以为不受限制的172D.J. Doughnut等人理论计算机科学电子笔记136（2005）153还原未来研究的一些方向交类型已被证明是研究传统λ演算中约化性质的宝贵工具，在未来的工作中，我们希望在这里提出的系统上使用合适的变体来表征GEMINI中的弱归一化和头归一化。众所周知，具有交集类型的传统λ-演算不适合Curry-Howard（证明项）对应。这使得交集成为一个证明理论的而不是真值函数的连接符。Dezani等人[8]、Ronchi Della Rocca和Roversi [22]、Capitani等人[4]以及最近Wells和Haack [26]都曾尝试开发具有交叉类型的系统（a ` l a C h u rc h）。在λµ-演算框架下的这一研究方向值得关注。研究这里提出的系统和Laurent [15]的系统之间的关系将是有趣的。更好地理解联合类型在经典演算中的作用是很重要的。一个明显的问题是，相对于[18]和[3]中的系统，我们为在我们的系统中进行主语归约所付出的代价是否是表达能力的下降，如果是这样，我们应该尝试理解交易。确认我们非常感谢裁判们提出的宝贵建议。引用[1] Barbanera，F.，M. Dezani-Ciancaglini和U. de202-230[2] 巴伦德雷格特H。P.，“The Lambda Calculus: its Syntax and Semantics,” North-Holland,[3] Buneman，P. and B. Pierce，Union types for semistructured data，in：Research Issues inStructured and Semistructured Database Programming，7th International Workshop onDatabase Programming Languages ， Lecture Notes in Computer Science1949 （ 2000 ） ，pp.184- 207.[4] 卡皮塔尼湾，M. Loreti和B. Venneri，Hyperformulae，平行扣除和交叉类型，理论计算机科学电子笔记50（2001）。[5] Coppo，M. 和M. Dezani-Ciancaglini，Anewtype-assignmentfororlambdaterms，Archivfur？ rMathematische Logik19（1978），pp.139-156.[6] Coppo，M.和M. Dezani-Ciancaglini，基本功能理论的扩展，λ-演算，Notre Dame Journal of Formal Logic21（1980），pp.685-693.