《交叉型学科的新统一过程中类型推理问题的研究》

理论计算机科学电子笔记136（2005）23-42www.elsevier.com/locate/entcs论交叉型学科G'erardB oudol和PascalZimmer1，2INRIA Sophia Antipolis，BP 9306902 Sophia Antipolis Cedex，法国摘要我们介绍了一个新的统一过程中的类型推理问题的交集型纪律。我们证明了统一化恰好对应于扩展λ -演算中的归约，在扩展λ-演算中，人们永远不会删除那些被普通β-归约丢弃的参数。 我们证明了我们的统一概念允许我们计算任何强规范化λ-表达式的主类型。保留字： λ-演算，类型系统，类型推理，统一化1介绍类型推理-（136）一般情况下，如下：1.为表达式和每个子表达式指定一个类型对于任何复合表达式或变量，请使用类型变量。2.在类型上生成一组约束，反映这样一个事实，即如果一个函数应用于一个参数，那么参数的类型必须与函数的域的类型3. 解决这些限制。1 电子邮件：Gerard. sophia.inria.fr2 电子邮件：Pascal. sophia.inria.fr1571-0661 © 2005由Elsevier B. V.出版，CC BY-NC-ND许可下开放获取。doi：10.1016/j.entcs.2005.06.01624G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23这种类型推理算法的设计最早（据我们所知）是由J. Morris在他的论文[20]中提出的。在这个过程的第一步，为了构建函数的类型，必须做出决定，这是一个抽象λxM：我们以何种方式考虑类型变量t1，.的集合。，t m分配给M中x的各种出现作为类型？有各种可能性，这不是无关的：• 简单（单态，可能递归）类型：变量x只有一种类型。也就是说，我们具有ti• 广义（多态）类型：这里的约束是x只在M中使用，其类型是λxM的域的类型的实例。• 交集类型：集合t1，.，t，m被认为是一种类型，被解释为t，i的合取。• 子类型化：x只在M中使用，其类型是λxM的域的类型的子类型。(The问题，因此可能的答案，将是不同的关于“让“结构，即（λxMN），其中抽象λxM不必显式在本文中，我们感兴趣的是由Coppo和Dezani [8]介绍的交叉类型规则的类型推理，以及由Pot- tinger [21]独立介绍的类型推理（参见[2，4]，以完整地回顾具有交叉类型的各种系统 在这个系统中没有决定可打字性的算法，称为“system 然而，人们可以为任何可类型化的表达式计算主类型化[9，16，24]，这是一种类型，通过适当的操作，可以导出给定表达式的任何其他类型，其中最重要的是扩展（对于这个概念的解释，例如参见[3]）。类型推断可以通过规范化表达式，然后键入范式来实现，但显然这不能扩展到希望键入非终止程序的语言。Ronchi在[23]中提出了一种基于广义统一机制的直接程序。后来Kfoury [13]，然后Kfoury和Wells [14]重新讨论了这一点，他们使用显式扩展变量，以便更好地理解扩展的操作，并表明类型推理对于具有有界秩限制的子系统是可判定的。在本文中，我们介绍了一种新的方法来解决类型的约束，所产生的类型推理的交集类型。为了给出我们的广义统一过程的概念，让我们回想一下，G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2325其附连到应用节点（MN），具有以下形式：（τ→t）=σ其中t是（在步骤1）分配给节点的类型变量，τ是参数N的类型，σ是M的类型。当M是一个函数λxMJ时，也就是说，当应用程序是一个redex时，后者具有形式（t 1，.，t m→θ），其中t1，.，t m是M j中赋给x的类型变量的合取，θ是M j 的类型。然后，模拟（λxMJN）的β约化为{x<$→N}MJ，我们的广义统一过程将t与θ等同，使得m与参数N相关联的约束的不同副本，并使用N的类型τ的适当副本来标识ti然而，这在βK-redex的情况下是不正确的，其中m= 0，因为我们可能会错过检查某些子项是可类型化的。例如，声明表达式（λu. F（uu））<$，其中F=λxλ y y和<$=λz（zz）是可类型的（在系统D中）。在任何情况下，我们都应该在redex中保留与参数相关的约束的副本，而不是删除它们，就像β还原一样然后，我们将证明我们的合一过程正好对应于扩展λ演算中的归约，在扩展λ演算中，人们永远不会擦除被普通β归约丢弃的子表达式这个微积分建立在Klop它特别使用了Klop例如，上面的表达式在此计算中简化为（λu[λy y，（uu）]）lus。为了在求解类型方程时进行适当的展开，我们将保持与对应于应用（MN）的每个方程（τ→t）=σ相关联的其领域，该领域是分配给参数N的子表达式。这通常不能从方程组直接访问，因为在表达式[M，N]中，与N相关联的约束与M的约束断开。我们的类型推理半算法已经由本文的第二作者实现，见[25]。对于任何λ-表达式，当它存在时，它计算它的主类型，在[9，16，24]的意义上;更确切地说，它计算主类型的证明。像Kfoury和Wells [14]的算法一样，我们的半算法在限制于有界秩的类型时终止。虽然在我们看来，它更简单，因此更容易证明是正确的，但它并不比Kfoury和Wells的复杂：事实上[19][14]的系统I的类型推理本质上和强规范化一样复杂。类似的结果也适用于我们的类型推理过程，尽管我们不必像[19]中那样诉诸共享图和证明网来建立β-归约（更准确地说是κ -归约，见下文）与类型约束的归约之间的直接对应26G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23当这篇论文即将完成时，我们注意到了[7]，它提出了一个看似相似的结果。事实上，[7]的一个主要结果是，在该论文中提出的类型推理过程对应于β-约简。然而，这里给出的结果有两个主要的不同之处：首先，与[7]不同，我们没有使用[ 13 ]中引入的“膨胀变量”的概念其次，[7]处理扩展的交集型学科，其中由[22]中的Sall′e引入的ypω被分配给一个ytω（这在[ 16 ]中被称为显然，由于βK-赎回，系统D中的β 我们还注意到，虽然一个概念对于系统D中的“近似范式”确实存在主类型的概念这与系统D形成对比，其中对于任何可类型化的表达式都存在主体类型化。2推广的λ-演算我们的扩展λ-演算基本上是Klop其语法如下：M N ......你好。X| λxM | (MN ) | [M, N]在新的构造[M，N]中，它被添加到λ-演算基元中，M 是主表达式，N是当将[M，N]解释为普通λ-表达式时被丢弃的表达式。（避免捕获）替换的操作，记为{x<$→N}M，像往常一样定义。定义我们的在[· · ·[M，N1]· · ·，Nn]上，在 这 种 情 况 下 ， 这 表 示 M 。 我 们 将 其 表 示 为 [M ， N1 ， . ， N n] ， 以 及sometimeseven[M， . . . ]中。Thereduction−→isthengiven bythetwooffollowingκ公理模式：x∈fv（M）（[λxM， . . . ]N）−→[{x<$→N}M， . . . ]κx/∈fv（M）（[λxM， . . . ]N）−→[M， . ， N]κ在[5]中已经表明，在这种演算中，强和弱归一化是一致的。例2.1为了说明本文中引入的各种概念，我们将使用λ-项F（λu. （uu）），即（λxλyyλu（λz（zz）（uu））。为此G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2327表达式，我们有以下减少：F（λu. （u u））−→[λyy，λu. （u u）]κF（λu. f（u u））−→F（λu. （uu）（uu））κ现在让我们介绍这个演算的交集类型系统。考虑合取不出现在箭头右边的类型是很方便的（这不是一个严格的限制，例如参见[4，5]）。也就是说，类型的语法如下τ σ ......你好。不|（π → σ）素型π κ... . . . ...你好。ω |τ | (π ∧ κ)types在类型系统中，我们考虑类型模由以下等式生成的同余式（ωπ）=π（U）（（π0<$π1）<$π2）=（π0<$（π1<$π2））（A）（π0<$π1）=（π1<$π0）（C）（π<$π）=π（I）实际上，我们通常将素数类型写成（τ1，.）。，τ n→σ），其中序列τ1，.，τ n是不相关的（即，序列τ1，.，τ n代表这些类型的任意合取组合，它表示当n= 0时为ω）。 我们包含幂等性（I）主要是为了完备性，也就是说，更准确地说，确保我们使用的交集类型系统是简单类型标准系统的保守扩展（其中序列被限制为只包含一个元素）。然而，应该指出的是，这种幂等性不会在任何技术开发中使用。类型系统的判断具有形式ΓM：τ，其中Γ通常是一个类型上下文，将类型分配给有限个λ-变量。我们用Γ表示Γ和的合取，它是以明显的方式定义的（即逐点地，假设对于任何不在定义域中的x，Γ（x）是ω的 ） 。 将 同 余 式 <$UACI 逐 点 推 广 到 类 型 化 上 下 文 ， 即 对 于 任 意 x ，Γ<$UACI<$意味着Γ（x）<$UACI<$（x）。类型系统28G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23具体如下：x：τx：τrM：σr（x）=π r\x<$λxM：（π→σ）ΓM：σN：τ[M，N]：σ其中，r|x表示通过移除关于x的类型假设（如果有的话）而从r获得的类型上下文τM：（τ1， . . . ，τm→σ）τi. iΓ∧∆1∧··· ∧ ∆m► (MN) :σm >0rM：（ω→σ）N：τ（MN）：σ例如，我们有：ΓM：τUACIΓ∆►M:τz：τ0→τ1<$z：τ0→τ1z：τ0<$z：τ0z：（τ0→τ1）<$τ0<$（zz）：τ1► τ：（（τ0→τ1）τ0）→τ1例2.1（续）表达式F（λu.[1][2][3][4][5][5][6][7][8][10][11][12][12][13][14][15][16][17][18][19][19（uu）是可类型化的，带有typeσ=（θ→τ0→τ1），（θ→τ0），θ→τ1我们可以很容易地推广经典的结果，即β-正规型在这样的系统中是可定型的（见[8，16]）。 要看到这一点，让我们首先观察规范形式（即κ-不可约表达式）的集合N P，Q.。我们的扩展λ-演算由以下文法给出：P Q . . . ...你好。H | λxP | [P, Q]H..X|（惠普）|[H，P]我们用hv（H）表示H的头变量，即hv（x）=x和hv（HP）=hv（[H，P]）=hv（H）然后我们定义，直到类型变量的重命名，P. 这是一对类型上下文和类型，写为Γτ，归纳为G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2329如果P是一个H，其头变量为x，则它的形状{x：τ1→···τn→t} τrjt其中t不出现在rJ中。i. x：t是x的规范类型，其中t是任何类型变量;ii. 如果（{x：τ1→···τn→t}<$r）<$t是H的典型型，是P的典型类型，涉及类型变量的不相交集合，则{x：τ1→···τn→τ→t}τt是（HP）的典型类型;iii. 如果Γ πτ 是P的典型类型 且Γ（x）= π（其中π =ω ifx/∈dom（Γ）），则Γ\x<$π→τ是λxP的标准型;iv. 若Γ<$τ和Γ<$σ分别是P和Q的典型类型，涉及不相交的类型变量集，则Γ<$τ是[P，Q]的典型类型.很容易检验规范型P的规范型Γ<$τ确实是有效型，即，Γ<$P：τ是可证明的。 我们还记得，它已被证明（见[9，？]），对于任何具有β-正规的λ-表达式M，形式N，N的典型类型是M的主类型，在这个意义上，它是M的有效类型，通过适当的运算，可以从它导出任何其他类型。为了结束本节，我们注意到可以扩展与可类型性和强规范化相关的经典结果定理2.2在扩展的λ-演算中，一个表达式是可类型的当且仅当它是强可 正规化的。可类型性意味着强规范化的事实在[5]中得到了确立（“subject reduction”属性仅使用AC）。相反地，检查（例如沿着[ 1 ]中给出的路线证明“主体扩展”性质）扩展λ -演算的强正规化表达式是可类型化的并不困难3键入约束在本节中，我们定义与表达式相关联的约束，以便执行类型推断。和往常一样，约束是类型方程，但它们涉及到一种受限制的形状，我们称之为骨架。骨架类型或者是类型变量，或者是形式（t1，. ，t m→ m）30G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23不其中，t是骨架（并且ti其语法如下：快，快... ......你好。不|（φ → φ） 骨骼类型φ，φ... ......你好。ω |不|（φ）正如我们在引言中所说的，类型推断过程的第一阶段包括将类型分配给要类型的表达式及其子表达式，将（不同的）类型变量分配给复合表达式（MN）和（oc-）。λ-变量。也就是说，我们从带注释的表达式A，B. 定义如下。我们同时定义带注释的表达式的集合A，以及在A中出现的类型变量的集合tyvar（A）。集合A归纳地定义为：i. 对于每个λ-变量x和每个类型变量t，表达式xt在A中，并且tyvar（xt）={t};ii. 若A∈A，则λxA∈A且tyvar（λxA）=tyvar（A）;iii. 如果A∈A和B∈A，且tyvar（A）≠tyvar（B）=0，且t是不在tyvar（A）≠tyvar （ B ） 中 的 类 型 变 量 ， 则 （ AB ） t∈A 和 [A ， B]∈A ， 且 tyvar（（AB）t）={t}tyvar（A）tyvar（B）和tyvar（[A，B]）=tyvar（A）tyvar（B）。例2.1（续）F（λu. 在对应于应用程序节点的类型变量的下面是：（λxλyyt0λu（λz（zt1zt2）t3（ut4ut5）t6）t7）t8我们在带注释的项上定义了各种函数：首先，erase是删除类型注释的函数，从注释表达式中生成扩展λ演算的表达式（定义是显而易见的然后typ将一个（骨架）类型与一个带注释的表达式相关联。这被定义如下，使用辅助函数ΓA，给定一个注释表达式A，将一个（φ）类型（即一个类型变量序列）与每个λ变量相关联：⎧阿勒特 如果y=xtyp（x）=tΓxt（y）=⎧ω否则如果y=x，typ（λxA）=（ΓA（x）→typ（A））ΓλxA（y）=λrA（y），否则typ（（AB）t）= tΓ（AB）t =（ΓA <$ ΓB）typ（[A，B]）=typ（A）Γ[A，B] =（ΓA<$ ΓB）G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2331正如符号所暗示的，在下文中我们也将ΓA视为与A相关联的类型化上下文。例如我们已经typ（λz（zt1zt2）t3）=t1，t2→t3通过一个带注释的表达式A，我们最终关联了一组要求解的约束，以便键入erase（A）。这些是，像往常一样，类型方程typ（A1）→t=typ（A0）附加到表达式中的应用节点（A0A1）t，除了我们还必须记录方程的区域，即集合类型变量，当方程简化时必须复制，即tyvar（A1）（3）。则约束具有形式（τ<$σ;T），其中T是类型变量的集合我们写τσ，而不是τ=σ，以提醒，左（右）一个方程的成员应该被认为是负的（分别是）。正），见[6，12]。与A相关联的约束集合EA归纳定义如下：Ext=EλxA=EAE（AB）t={（typ（B）→ttyp（A）;tyvar（B））} EA <$EBE[A，B]=EA <$EB例2.1（续）与注释版本（λxλyyt0λu（λz（zt1zt2）t3（ut4ut5）t6）t7）t8）相的F（λu. 我们得到下面的一组约束：E0={（t4，t5→t7）→t8<$ω→（t0→t0）;{t1，.，t7}，t6→t7<$t1，t2→t3;{t4，t5，t6}，t5→t6<$t4;{t5}，t2→t3<$t1;{t2}}在EA中有两种方程：形式为（n→t）<$tJ的对应于A中的应用节点，其中函数是λ变量，或者[3]在没有构造[M，N]的情况下，这可以从方程中导出，从类型（A 1）中的类型变量集合开始，并在域中包括在一个方程中进行运算的所有类型变量n→t′=n，其中t′在t或y中也是y。32G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23的应用，而方程的形状（→t）（t1，.，t n→n）对应于应用节点，其中要应用的函数是形式（[λxAJ，.. . [B]t.值得注意的是，给定分配给方程成员的极性，以及在类型化的Γπτ中，Γ的像中的类型是负的，而τ是正的，我们有：注3.1（i）分配给应用节点的每个类型变量t具有在EA的方程中，即在与节点相关联的方程（t→t）中，恰好有一个负的出现。此外，如果应用程序节点是另一个应用程序节点的子表达式，则它最多在EA应用程序，或在类型（A）。(ii)赋给λ-变量x的每个类型变量都有一个确切的负出现，或者在EA中，如果x被作为应用的子表达式的λ-抽象所约束，或者在ΓA中，并且最多有一个正出现，如果x是应用的子表达式，或者在typ（A）中。这实际上是在求解约束时将被保留的不变量4统一为了解决一组约束，我们将通过一个广义的统一机制来减少它们，该机制涉及我们现在介绍的类型替换的概念。由于要约简的约束只涉及骨架类型，我们将只考虑对这种受限类型应用替换。一个素数类型替换是从类型变量的有限集合dom（S）的映射S到主要类型。 如果dom（S）={t1，.，t n}和S（t i）= τ i，我们还将S表示为：{t1> →τ1，.，t n <$→τ n}。设S（t）=t，其中t/∈dom（S）.将替换S应用于（骨架）类型的结果表示为S（定义，通过归纳，τ的结构上的作用，是通常的一个）。事实上，我们只会在S是重命名的情况下使用S，将（不同的）类型变量分配给类型变量。然而，我们还将使用替换S来应用于骨架类型中类型变量的正出现。结果类型表示为dS+n。因为这是一个复杂的问题，可能会出现错误在本文中，S+S的定义应是：如果S=（φ1→· · ·（φn→t）· · ·）nS+S=（φ1→· · ·（φn→S（t））· · ·）。请注意，这是一个关键的类型，如果S（t）是骨架。类型替换的这些积极应用被扩展，根据我们上面建议的极性（左为负，右为正）来类型方程，如下所示：S+（→t）=S+→tS+G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2333最后，我们还将考虑将类型（不一定是素数）分配给类型变量的替换。显然，这些应该只应用于箭头的左边，也就是说，因为我们只考虑应用于骨架类型，即类型变量的负出现。然后，给定从类型变量的有限集合dom（D）到类型的映射D，扩展为D（t）=t对于t/∈dom（D），我们定义D−dom，将D应用于（骨架）类型的结果通过将D应用于φ而获得的类型如下：D−t=tD+ω=ωD−（φ→φ）=（D+φ→D−φ）D+t=D（t）D+（φ）=（D+φD+）事实上，我们只在D是重复的情况下使用它，将不同类型变量的合取赋给类型变量。请注意，在本例中，D−D是骨架类型。同样，我们将其扩展到方程，但是只有当方程的根不被D截断时。也就是说，如果t/∈dom（D），我们让：D−（n→tn） = D−→tD−除了类型替换之外，为了求解约束，我们还需要这些是由从有限个类型变量集到有限个类型变量集的映射U确定的。类型变量，我们记为U ={t1→U1，.，t n <$→U n}.假设，按照惯例，U（t）={t}，如果t/∈dom（U），则这些应用于类型为变量如下：U（T）=t∈TU（t）最后，为了标识一对函数，其中一个函数返回pairs，我们将使用以下形式的变换：{t1<$→（τ1; U1），. ，t n<$→（τ n; U n）}它充当素型替换{t1<$→τ1，.，tn →U1，.，tn <$→Un}的变换，同样对于变换{t1<$→（π1; U1），.，t n<$→（π n; U n）}.类型替换和术语替换的关系如下。如果tyvar（A）≠tyvar（B）=，我们表示为{xt<$→B}A是避免在A中用B替换xt的捕获。 然后我们有：[4]就领土而言，这种变换的正面或负面应用就是U（T），如上所定义。34G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23t+Lemma4. 1（ i） typ（{xt<$→B}A） ={t<$→（typ（B ）;tyvar（B ））}+typ（A）（ii）如果x发生在A中，则E {xt <$$> →B}A = EB<${t <$→（typ（B）; tyvar（B））} EA。证据 通过对A.Q现在我们定义约束集合上的约简EDEJ的概念。正如我们将要看到的，这非常接近于表达式的κ-约化。约束对应于redex（[λxA，. . [B]t如果它具有以下形式（→t）（φ→）;tyvar（B）其中，φ是分配给参数B的类型，t是应用节点的类型，φ = t1，.，t m是函数A中抽象变量x的类型序列，并且m是函数体A的类型。通常，为了简化这样的方程，我们必须将t与φ统一起来（反映了这样一个事实，即A，其中执行了B对x的替换，取代了应用节点），并将φ与φ统一起来，但后者不能以通常的方式求解（即识别Ti 通过类比β-约化，解出方程1，...，tm应该对应于将参数B替换为变量x在A中的m次出现。为了得到一个格式良好的带注释的项，我们必须对B做m个不同的副本，用新的类型变量（它们是方程的tyvar（B然而，我们不能简单地替换第一个...，t m乘1t1，.，m tm其中，1，...，m是的副本，因为中出现的类型变量也可以出现在约束集合中的其它地方。实施例2.1（续）F（λu. f（u u））−→F（λu. （uu）（uu））κ应相当于t0t1t2t3t4t5t6t7t8t0t1t1t1t2 t2t2t3t8（λxλyyλu（λz（zz ）（u u））的情况）−→（λxλyyκλu（（u4u5）6（u4u5）6））以及方程t6→t7→t1，t2→t3的分解，{t4，t5，t6}，因为它是减少的类型t7因此，我们不仅要复制t6，还要复制t4和t5，它们出现在复制的参数（ut4 ut5）t6中。 这些类型变量也出现在其他方程中，即（t4，t5→t7）→t8<$ω→（t0→t0）和t5→t6<$t4。 我们从（注释的）κ-约简中看到，后者应该简单地重复，而在前者中，我们应该替换序列t4，t5，对应于抽象λu，由t1，t2，t1，t2（modulo the associativity and commuta-4455性公理AC），以获得与以下相关联的约束集：G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2335t0t1t1t1t2t2 t2t3t8（λxλyyλu（（u4u5）6（u4u5）6）） ，就是说E1={（t1，t1，t2，t2→t3）→t8<$ω→（t0→t0）;{t3，t1，t2，t1，t2，t1，t2}，4545445566t2→t3<$t1;{t2，t2，t2）}，6 6 456t1→t1<$t1;{t1}，5 6 4 5t2→t2<$t2;{t2}}5 6 4 5这在下面的规则中被形式化，定义了归约过程，它包括约束集之间的归约关系EDEJ 在下面的定义中，我们明确记录了在约简中使用的变换Θ，然后将其表示为EDEJ[Θ]。为了说明定义，引入以下符号也是方便的：E ↓T={（→t; U）|（n→t tn; U）∈E&t∈T}E ↑T=E −（E ↓T）我们可以看到，当T是某个方程的范围时， E，对应于应用节点（AB）t，则E↓T是与参数B相关联的约束集，即E ↓tyvar（B）=EB。定 义 4.2 （ n- 统 一 ） 设 E0={ （ n→tnφ→n; T ） } n E 是 一 组 约 束 。 则E0DE1[Θ]，其中(i) 若φ=ωthen0={t<$→（t;n）}+且E1=0（E）;(ii) 如果φ=t1， . . . ，tm，其中thm>0，thenΘ=S+n{t<$→（t;n）}+nD−，并且.E1=S+{t<$→（t;t）}+D−（ E↑T）<$1≤j≤mΣRj（E ↓T）其中，如果T ={s1，.，s n}，D={s i> →s1，. ，s m;{s1，. ，s m}）|1 ≤ i ≤ n}我我我Rj={s1<$→（s j;{s j}），. ，s n<$→（s j;{s j}）}（1 ≤ j ≤m）1 1n nS ={t1<$→（R1; R1T），.，t m<$→（Rm; RmT）}其中s1，. ，s1，.，sm，.，sm是新鲜的（不发生在E0），不同类型1n1n变量36G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23例2.1（已结束）关于我们的运行示例表达式F（λu.（uu）），或者更准确地说，它的注释版本（λxλyyt0λu（λz（zt1zt2）t3（ut4ut5）t6）t7）t8，我们看到，如果我们从相关约束的集合E0中选择方程t6→t7<$t1， t2→t3来约简，区域为{t4， t5， t6}，我们得到，使用定义的符号（T={t4， t5， t6}和E0={t6→t7<$t1，t2→t3;T}<$E），应用以下替换：D={t i<$→t1，t2;{t1，t2}）|4 ≤ i ≤ 6}我我我R1={t4<$→（t1;{t1}），t5<$→（t1;{t1}），t6<$→（t1，{t1}）}4 4 5 5 6 6R2={t4<$→（t2;{t2}），t5<$→（t2;{t2}），t6<$→（t2;{t2}）}4 4 5 5 6 6S={t1<$→（t1，{t1，t1，t1}），t2<$→（t2，{t2，t2，t2}）}6 456 6 456以来E ↓T={t5→t6<$t4;{t5}}E ↑T ={（t4，t5→t7）→t8<$ω→（t0→t0）;{t1，.，t7}，t2→t3<$t1;{t2}}其中E ↓T是与redex的参数（ut4ut5）t6相关的约束集，类型为t7，我们正在考虑进行约简，我们得到E0DE1，其中E1={（t1，t1，t2，t2→t3）→t8<$ω→（t0→t0）;{t3，t1，t2，t1，t2，t1，t2}，4545445566t2→t3<$t1;{t2，t2，t2）}，6 6 456t1→t1<$t1;{t1}，5 6 4 5t2→t2<$t2;{t2}}5 6 4 5t0t1t1t1t2t2t2t3t8这是与（λxλyy）相关的约束集 λu（（u4u5）6（u4u5）6）），如上所述。在E1中只有一个可约方程，其根为t8.G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）2337分解这个方程，我们应用定义的情况（i），我们得到E2={t2→t3<$t1;{t2，t2，t2）}，6 6 45 6t1→t1<$t1;{t1}，5 6 4 5t2→t2<$t2;{t2}}5 6 4 5t0t1t1t1t2t2t2t3这是与[λyy，λu（（u4u5）6（u4u5）6）]相关联的约束集请注意，在求解类型约束的第二步中，从E1到E2，我们必须应用替换t8<$→（t0→t0）。由于t8不出现在E1中，除了在简化方程中明显外，这种替代没有效果。然而，应该注意到，它转换了F（λu）的注释版本的类型t 8。将[λyy，λ u]（uu））转换为（t0→t0），这是该表达式的期望类型，也是其规范形式[λyy，λu. （uu）（uu）]。5可打字性和打字现在，我们通过证明它恰好对应于扩展λ演算中的归约，来证明可分型性可以被用来刻画。首先，我们展示了范式之间的对应关系。引理5.1（范式）扩展λ-演算的表达式M是κ-范式当且仅当EA不可约，对于任意A使得erase（A）= M。(The证据是显而易见的）。下一个引理陈述了复统一的关键性质。对于它的证明，我们需要UAC公理，例如，当将我们的类型推理过程应用于λ表达式（λy（x（yx））x）。给我5分。2（OperationalCorrespondence）（i）IfM−→Nanderase（A）=κ则存在B使得erase（B）= N且EAD EB。(ii) 如果EADE存在sB使得E =EB并且erase（A）−→erase（B）。κ证据（素描）(i) 我们提出了一个更精确的假设，即如果M−→N且erase（A）=κM则存在B和Θ，使得erase（B）=N， EADEB[Θ]，typ（B）=UACΘ（typ（A）），ΓB=UAC Θ（ΓA）并且tyvar（B）= Θ（tyvar（A））。我们通过对M−→N的引入来进行。κ38G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23•IfM−→κN 是a xio m，则nM=（[λ xM0，N1， . . ，Nk]M1）和ndA=（[λ xA0，B1， . . . ，Bk]A1）t和EA满足方程（φ→t）φ（φ→φ）其中，φ=typ（A1），φ= ΓA0（x），并且φ=typ（A0）。 令T ={s1，.，s n}=tyvar（A1）. 有两种情况。（1） 如果fx/∈f v（M0），则nN=[M0，N1， . . ，Nk，M1]. Sincex/∈fv（A0），weveφ=ω。 根据《古兰经》的定义，我们EA={（t→t<$ω→t;T）} <$ ED{t<$→（t;t）}+ E[{t<$→（t;t）}+]由于E =EA0EB1·· ·EBkEA1且tdoe不发生在A0，B1， . . . ，Bk，A1，它清楚地表明了存在两个类型B=[A0，B1， . . ，Bk，A1]。（ 二 ）若 fx∈fv （ M0 ） ， 则 nN=[{x<$→M1}M0 ， N1 ， ..， Nk] 。Letφ=t1， . . ，tm. 然后，我们有EADE[Θ]，其中，使用定义4.2的符号，Θ=S+{t<$→（;）}+D−，E=S+{t<$→（;）}+.−D （E[A，B，...，B]）ΣRj（EA）01K11≤j≤mW e letB=[{xtj→RjA1|1≤j≤m}A0，B1， . . ，Bk]，并使用引理4.1得出结论。•IfM=（M0M1）andndN=（N0M1）withithM0−→N0thenA=（A0A1）twiththκerase（Ai）=Mi，EA={（A→ tt;tyvar（A1））} EA0EA1其中，n=typ（A1）和n=typ（A0）。 通过归纳假设，存在B0和Θ，使得，特别地，擦除（B0）=N0和EA0DEB0[Θ]。 设B=（B0A1）t，并利用归纳假设得出结论.•其他案件也是类似的。(ii)[2019 -02 - 16][2019 - 02][2019 - 02 - 01][2019 - 02 - 01][2019 - 01][201Q定理5.3扩展λ-演算的表达式M是可定型的，当且仅当对于任意A，不存在从EA的无穷序列的归约，使得erase（A）= M。证据根据定理2.2，如果M是可类型的，则M是强正规化的，因此，根据前面的引理，如果erase（A）=M，则不存在从EA的无穷序列的约简。相反，如果对于A使得erase（A）=M，G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23390则M是强正规化的，我们再次利用定理2.2得出结论。Q这个结果为[13]中提出的一个问题提供了另一种解决方案，即在不使用展开变量的情况下，找到λ项的强归一化的类似统一的特征。在第二作者的博士论文[26]中，它表明，如果我们不区分定义4.2中的两种情况（i）和（ii），允许m在第二种情况下为0，则与表达式M相关的约束集的约简收敛当且仅当该表达式M具有范式。这对应对于系统D中（弱）正规化项的特征，参见[10，16]。引理5.2的一个推论是，如果EAD<$E，其中E是不可约的，则存在B使得E=EB且erase（A）−→κ 擦除（B）。 关于Lemma5.1 ，我们知道erase（B）是一个标准形式。现在我们展示如何使用EB构建erase（B）的规范类型。为此，我们在对（E，Γτ）上定义一个变换D，称为（类型约束的）简化，并给出如下：（{σ<$t;T}<$E， Γ<$τ）D{t<$→σ}−（E，Γ<$τ）其中，{t<$→σ}−只适用于类型和方程，而不适用于领域（在注释3.1中，这是很好定义的）。我们的最终结果，结合Theorem reftheorma，建立了统一化和简化允许我们计算任何强规范化表达式的规范类型：定理5.4对于任意正规形P和带注释的表达式 A，使得∗erase（A）=P存在 Γ和τ使得（EA，ΓA≠typ（A））D（τ，Γ≠τ）而Γ <$τ是P的典型类型。用归纳法对A.让我们来看看A=（A0A1）t.注意erase（A0）必须是一个H，头部变量为x。我们有EA={（→t;T）} EA0EA1其中，n=typ（A1）和n=typ（A0）。此外，ΓA = ΓA0< $ΓA1。根据归纳假设，我们有（EAi，Γ Ai（Ai））∗D（τ，τi，τi）其中，Γi<$τi是erase（Ai）的典型类型，对于i=0， 1，因此，Γ0 ={x：σ1→···σn→tJ}<$ΓJ其中τ0=tJ。由于τi是通过一系列非平凡的类型替换从typ（Ai）得到的，我们有<$i=TJ，并且EA1变换的简化是<$i40G. 布多尔山口Zimmer/Electronic Notes in Theoretical Computer Science 136（2005）23变成τ1。然后我们有EJ−AD（{（τ1→t t）;T}， ΓAt）D{t→（τ1→t）}（，ΓAt）很容易看出{tJ<$$> →（τ1→t）}−（ΓA<$t）是P=擦除（A）。引理5.2和定理5.4只是存在断言，因此它们并没有完全指定类型推断的半算法。 的确，由第二作者实现的算法，可以从[25]中提到的url中获得，比这更聪明：它处理对（E，E），其中E是其中应用程序的键入规则为Γ►M：τ∀i. im >0Γ∧∆1∧··· ∧ ∆m► (MN):σ然后由算法执行的变换不仅对约束集进行操作（通过归一化），而且对类型部分的证明进行操作，以这样的方式，如果我们从（EA，A）开始（对于适当定义的A），其中erase（A）是强正规化的，那么算法以（