高阶抽象语法和覆盖检查在计算机科学中的应用

理论计算机科学电子笔记228（2009）69-84www.elsevier.com/locate/entcs高阶数据Jana Dun Field和Brigitte Pientka计算机科学学院，麦吉尔大学3480rueUniversity，Montreal，QCH3A2A7，Canadabp@cs.mcgill.ca摘要我们讨论了依赖类型的数据的覆盖检查，并使用高阶抽象语法定义。与以前的工作覆盖检查封闭的数据，我们认为开放的数据可能取决于一些上下文。因此，我们的工作可能会提供深入了解覆盖检查在BMPF，并作为覆盖检查的基础，如Delphin和Beluga的函数式语言。 更一般地说，我们的工作是一个基础的证明，在系统中的情况下分析，原因高阶抽象语法。关键词：高阶抽象语法，覆盖检查1介绍在过去的十年中，使用包含绑定器的数据结构以及关于包含绑定器的数据结构的编程和 推理在 编程 语言和 自动推 理系统 中受 到了广 泛的关 注。高 阶抽 象语法（HOAS）是一种处理绑定器的简单而优雅的技术 中心思想很容易解释：我们使用元语言变量，而不是显式地表示对象变量。例如，对象级公式x。（x = 1）λ <$（x= 0）可以表示为对于所有λx。 (eq x（Suc Zero））imp（not（eq x Zero））.这避免了实现常见和棘手的机制的需要，例如捕获避免替换，重命名和新名称生成。当我们实现证明时，高阶AB语法允许我们考虑假设推导，即依赖于假设的推导作为高阶函数，其中替换引理的应用对应于函数应用。例如，在自然演绎中（图1），隐含引入的假设类型推导可以使用高阶函数来优雅地建模。HOAS编码的强大功能已经在逻辑框架LF中显示出来[13][14][15][16][17]最近，HOAS编码在Elphin [17]，Delphin [14]和Beluga [12]等函数式编程语言在这些系统中，我们使用模式匹配和案例分析高阶数据1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2008.12.11770J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69数字 N，M：：=x| 0| 中国命题A：：=N=M| A组B组| A.A.自然演绎Γ►ndAnat：type.零：天然。Suc：天然→天然。o：类型。方程式：nat→nat→o。imp：o→o→o。对于所有：（nat→o）→o。nd：o→type。r，u：ndAndB联系我们⊃Iuimpi：（nd A→nd B）→ nd（A杂质B）。Γ►ndA⊃BΓ►ndA⊃E特兰德湾rnd[a/x]Aand（阻抗：nd（A阻抗B）→nd A→ 和B。alli：（a：nat. nd（A a））→ nd（对于所有λx. A x）。（u：ndA）∈Γ第二章AHypΓ（x.A）[N/x]AEalle：nd（对于所有λx. Ax）→ nd（A N）。Fig. 1. 自然演绎及其HOAS编码表情这要求我们验证模式是详尽的。类似地，基于HOAS的推理的证明助手将目标分成不同的情况，必须确保这些情况是详尽的。这个问题出现在Beself的归纳定理证明器[ 15 ]中在一阶简单类型的设置中，按案例分析数据是直截了当的。我们可以只考虑给定类型的所有声明的常量。为了说明，在图1中，我们定义了一个简单的逻辑，在LF[5]的通常风格中，数字相等。命题A的格是清楚的：它们正好是语法中列出的三种命题形式。然而，对于数，我们不仅需要0和N的情况，还需要变量x的情况。高阶数据也会出现类似的情况，比如自然演绎中的推导。基于高阶抽象语法的编码不显式地表示规则Hyp。相反，这个基本情况将是隐式的。因此，生成所有案例需要我们考虑上下文及其可能的元素。我们的主要贡献是一个理论框架，为可能涉及假设的对象（即开放对象）生成一组详尽的案例。以前的覆盖检查工作处理了封闭项[2，16]，或常规世界中的开放项[15，pp.197-213]。我们的工作是在语境模态类型理论的背景下对覆盖范围的第一次理论处理。我们相信，我们的理论是揭开覆盖检查的神秘面纱的第一步，这对许多用户来说是一个神秘的操作。更直接地说，我们的工作是Beluga [12]等语言的基础，这些语言可以对开放数据进行案例分析。我们证明了一个属性的覆盖稳健性，需要证明在白鲸的进展我们将从Beluga语言的一个例子开始，它支持在函数设置中使用LF编码进行编程。为了强调由于开放术语而引起的问题，我们将在这个示例中集中讨论简单类型的设置。然而，我们的正式框架处理依赖类型的术语，这使得J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6971reccntVN：：（nat）. nat[int，x：nat]→int =Λ fn nn是盒（x，x）的情况n。x]）| box（x. p[id]）| box（x. 零）0| box（x. Suc U[id，x]）cntVN [|box（x. U[idm，x]）rec cntV：中文：（nat）中文。o[int，x：nat]→int =Λ ψ⇒fn F型壳f的box（x. eq U[id，x] V[id，x]） cntVN[CN]|box（x. U [id m，x]）+ cntVN [CN]|box（x. V[id，x]）| box（x.imp U[id，x] V[id，x]）cntV [|box（x. U[idm，x]）+ cntV [|box（x. V[id，x]）| box(ψ, x. foral l（λy. W [id，x，y]））}}|box（x，y，x）W[id，x，y]）图二. 使用模式匹配和HOAS问题更难。类型的结构可以被观察到，这使得覆盖检查不可判定，因为任何模式集都将覆盖空类型的所有术语，而空是不可判定的。2动机为了激发这个问题，我们考虑一个简单的程序在Beluga语言[12]，计数一些变量x在公式中的自由出现比如说，很好（x=y）（y=x）有x的两次自由出现。这里的数据语言是对自然数进行量化的一阶逻辑，如图1所示，我们通过模式匹配分析HOAS数据。使用这个例子，我们然后更详细地讨论覆盖率的问题。我们将编写两个函数来解决这个问题。函数cntV将递归分析公式。当它到达自然数表达式时，它将调用第二个函数cntVN。我们使用诸如o[x：nat，y：nat]这样的模态类型，它描述了一个可以引用nat类型的变量x和y的公式。公式（（eq x y）imp（eq（Suc x）（Suc y））具有这种类型。当cntV递归地达到一个具有泛量化器的公式时，自由变量的集合会增长。因此，我们需要对公式有意义的上下文进行抽象。上下文变量可提供此功能。函数cntV（图2）在自然数的上下文中接受公式f，并返回一个整数。就像类型对数据对象进行分类，种类对类型进行分类一样，我们引入模式来对上下文进行分类。在函数cntV我们说上下文变量具有schema（nat），这意味着x1代表数据级上下文，其形式为x1：nat，. ，xn：nat.我们使用单个大写字母U，V，W表示上下文变量，这些变量通过高阶模式匹配进行实例化我们首先检查第二个函数cntV。它是由上下文抽象构造的，它引入了上下文变量，并绑定了body中的每个。接下来，我们引入类型为o[nat，x：nat]的计算级变量f。在72J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69函数cntV的主体我们对类型为o[x，x：nat]的对象进行了案例分析。 框结构将数据级术语（数据对象）与计算级术语分开。由于公式是由等式eq、蕴涵imp和量化构造的，因此我们对每一个都有案例。当我们遇到从构造函数eq、imp或forall构建的对象时，我们必须提取下面的子表达式。模式变量的特征在于由上下文变量U和推迟替换σ组成的闭包U[σ]。一旦我们知道上下文变量代表什么，我们就应用替换σ。在这个例子中，与U相关联的推迟替换是本质上对应于α-重命名的恒等替换。我们把定义域的恒等式替换为id_n。直觉上，人们可以认为与模式中出现的上下文变量相关的替换是可能出现在洞中的变量的列表因此，在U[id]中，上下文变量U可以用任何公式实例化，这些公式要么是封闭的（不引用上下文中的任何绑定变量），要么包含来自的绑定变量。由于子公式可以引用所有变量，所以我们写U[idn，x]。在第一种情况下，对于eq，我们调用cntVN来计算x在自然数U[idn，x]和V[idn，x]中的出现次数，显式地传递带有cntV [id n，x]的n|.imp的第二种情况的结构类似，调用cntV而不是cntVN。在第三种情况下，对于box（x，x.对于（λy.W[idλ，x，y]）），我们在假设y是自然数的条件下分析了量化公式. 为此，我们向cntV传递一个扩展的上下文（xmax，y：nat）。变量x出现在box（x，y，x）中的最后一个。... ），以匹配参数类型o[. ，x：nat]。函数cntVN计算变量x在nat[nat，x：nat]类型的对象中出现的次数，考虑四种情况。第一种情况，box（x，x）。x），匹配x的出现。第二种情况，box（x，x.p[id]），匹配一个不是x的变量，并且出现在中。对于这种情况，我们使用参数变量p（使用小写字母将其与元变量区分开来）。这表示绑定的数据级变量。与p相关联的替换idf表示p. 其余的案件都很简单。2.1开放数据覆盖的基本思路在本文中，我们提供了基础，以确保通过模式匹配分析A[X]类型元素的case表达式覆盖该类型的所有可能元素。例如，在函数cntVN中，我们确保模式集{x，p[id]，Zero，Suc U[id，x]}覆盖类型nat[x，x：nat]。 在cntV中，{eq U[id，x] V[id，x]，imp U[id，x] V[id，x]，for all（λy. U[idn，x，y]）}覆盖所有类型为o[n，x：nat]的元素。这组覆盖类型o[x，x：nat]的模式绝不是唯一的一个。我们可以使用高阶模式匹配来强制变量依赖性，而不是显式地计算nat[id n，x：nat]类型的自然数中x的出现次数，将模式eq U[idn，x] V[idn，x]细化为以下四种情况{eq U[id]V[id]，eq U[id，x] V[id]，eq U[id]V[id，x]，eq U[id，x] V[id，x]}J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6973原子类型类型P甲乙丙：：=：：=M1... MnP|A.B. |A.B.正常条件M、N：：=λx。M|（男、女）|R中性用语R：：=C|X|u [σ] |p [σ] |RN|项目1R|项目2R取代σ：：=· |σ; M| σ，R|id上下文直径，Φ：：=· |ψ|x：A元语境Δ：：=·|Δ，u：：A [] |Δ，p：：A []图式上下文Ω：：=· |Ω，Ω：：W图三. 数据层面（1）x既不出现在U[id，x]中，也不出现在V[id，x]中;（2）x出现在U[id，x]中，但不出现在V[id，x]中;（3）x出现在V[ id，x]中，但不出现在U[id，x]中;（4）x既出现在U[id，x]中，也出现在V[id，x]中。更一般地说，我们提供了一个正式的框架来回答以下问题：一组模式是否覆盖了类型A？或者，我们的框架提供了一种生成一组模式的通用方法，从而为将A[A]类型的对象拆分为不同的情况提供了基础。我们强调，虽然我们在Beluga的设置中说明了这个问题，其中上下文是显式的，但这个问题在Delphin和Delphif等系统中是类似的，我们也必须在上下文中生成所有类型A3背景由于我们感兴趣的是测试一组模式是否覆盖给定的数据对象，因此我们将重点放在数据级别上。对于计算级别，请参见[12]。我们支持逻辑框架LF加上依赖对。我们的数据层紧密遵循上下文模态类型理论[10]，扩展了参数变量和上下文变量[12]，最后扩展了参数类型。也许最重要的是，我们形式化的模式，分类上下文。我们只刻画正规项，因为只有这些在逻辑框架中才有意义[18，10]。这是通过正常项M和中性项R之间的句法区别来实现的。语法保证术语不包含β-赎回，类型规则保证所有类型良好的术语都是完全η-扩展的。我们区分了三种类型的变量（图3）：普通绑定变量x和y用于表示数据级绑定器，并通过λ-抽象进行绑定。这些变量在上下文中声明。上下文变量代表开放对象，包括元变量u和v，它们代表一般的开放对象，以及只能用普通绑定变量实例化的参数变量p上下文变量被引入到计算级别的case表达式中，并且可以通过模式匹配来实例化它们与一个推迟的置换σ有关。目的是一旦我们知道上下文变量应该代表的对象，就应用σ。因此，σ的域包括74J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）691 先前的工作也考虑了替代变量，为了简洁起见，我们在这里省略了它。J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6975K2一这个对象的自由变量，类型系统静态地保证了这一点。上下文变量在元级上下文Δ中声明我们的基础支持上下文变量，它允许我们用上下文进行抽象推理，并编写操作高阶数据的递归计算与上下文变量的其他用法不同[8]，上下文最多可以包含一个上下文变量2。由于类型对对象进行分类，种类对类型进行分类，因此我们引入了对上下文进行分类的模式W的概念。上下文变量的模式在模式上下文Ω中给出。我们在3.2节中定义了模式。置换σ由正规项（在σ;M中）和原子项（在σ，R中）构成。我们没有明确定义域，这简化了理论发展，避免了对给定σ的定义域进行重命名。我们也有一个第一类的恒等替换id_n的概念。我们写[σ]N用于替换应用。我们假设类型常量和对象常量在签名S中被声明为纯LF对象-依赖函数类型的数据。我们抑制签名，因为它在所有推导中都是相同的。为了便于记法，我们把对推广 到 n元 元 组 ， 把 R 的 第k 个投 影 写 成 proj#R. 例 如 ， 三 元 组 的 第二 个 元 素 是proj#R=proj1（proj2R）。3.1数据级类型化我们双向输入数据级术语。正常对象在判断Ω; Δ;MA中与给定类型进行检查，而中性对象则合成它们的类型：Ω; Δ;RA。 根据其定义域检查替换：Ω; Δ; σ Φ。为了可读性，我们在后续的开发中省略了模式上下文Ω，因为它是常数，并假设Δ和Ω是良构的。我们在图4中给出了数据级术语的类型规则。我们假设数据级类型常量a和常量c已经在签名中声明.我们将默认重命名绑定变量，并保持上下文和子上下文声明变量不超过一次。请注意，替换σ仅定义在普通变量x上，而不是模态变量u上。我们还需要约束变量的通常条件。例如，在RPMI中，绑定变量x必须是新的，并且不能已经在RPMI中出现这总是可以通过α重命名来实现中性术语的类型规则使用遗传替换[···]a保护标准形式[10]。遗传替换是递归定义的，考虑到替换所应用的项的结构和被替换的对象。由于篇幅所限，我们将细节放在[3，附录]中。为了便于阅读，我们省略了下面的下标由于遗传替换是可判定的，并且图4中的规则是语法指导的，因此数据级类型是可判定的。2解除此限制需要跟踪上下文变量之间的依赖关系：A，B，确保α-重命名在存在多个上下文变量和依赖类型的情况下成立，这似乎是困难的。76J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69的1ΦΦ一的1ψΦΦ数据级正态项Δ;，x：AMBΔ; Δ λx. M：A. B IΔ;ΔM1ΔA1Δ;ΔM2Δ[M1/x]aA2IΔ;Δ（M1，M2）Δx：A1.A2Δ; RPJPJ=PΔ;ΔR数据级中性术语反过来x：A∈φvarc：A∈φconu：：A[Φ]∈ΔΔ; φφσ ΦmvarΔ; β-淀粉酶xβ-淀粉酶AΔ; β-氨基丁酸Δ;u[σ][σ]aAp：：A[Φ]∈ Δ Δ;σ ΦparamΔ; Rx：A.BΔ;NAEΔ;p[σ][σ]aAΔ; RN [N/x]aBΔ; Rx：A1.A2EΔ; Rx：A1.A2 E2Δ; β-proj1Rβ-A1Δ;Δproj2R[proj1R/x]aA2数据级替换Δ;··Δ;，id ⇐ψΔ;<$$>σ<$Φ Δ;<$$>R<$AJ[σ]aA=AJΔ;Δ（σ，R）Δ（Φ，x：A）Δ;σ Φ Δ;M[σ]aAΔ;σ;M）φ（Φ，x：A）3.2上下文模式见图4。数据级类型化和替换正如前面的示例所示，上下文在使用开放数据对象进行编程时起着重要的作用。 特别是，任何显式构造并且传递的将属于特定的上下文模式。在前面的示例中，模式（nat）表示形式为x1：nat，.，xn：nat.但我们允许更多的表达语境。例如，当推理自然演绎时，规则u为某个具体命题A添加了一个u：（ndA）形式的假设。归纳定义Γ J：：=·|r J，x：nat，|Γ J，u：（ndA）对应到模式（nat+（所有A：o. ndA））。我们用+来表示上下文中可能元素的选择，并且所有允许我们描述所有可能命题A的假设。这个模式的一个具体例子是x：nat，u：nd（eq x x），它在描述forall（λ x）的推导时出现。(eq x x）imp（eq（Suc x）（Sucx）））。我们在图5中给出了模式的语法。模式由元素F1， . . ，Fn，e，a，b，c，d，e，a，b，c，d，e，a，b，c，d，e，c，d，e B11， . . . ，yj：Bj. 其中，θ=x1：Cθ1， . . xk：Ck. 在其他情况下，对于任何情况，都可以使用Θi的变量（也就是说，对于x1， . . . ，xk），该元素是一个类-类型的元素，我们首先引入一些类，然后是类，没有后续类。这种限制使得描述该类型的居民更容易。BMF对世界也有类似的限制。在Beluga中，计算类型[12]保证了与此语法匹配的上下文是在计算过程中创建的唯一上下文。为了对照模式（F1+···+Fn）检查上下文，我们检查每个元素x：AinceoshementFk=allΘn。 B11， . . . ，yj：Bj. B.B. B. C.D. D. D.1J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6977元素类型A：：=x：A. A.|aN1. . . NnSch_e元素F：：=allx1：B=1， . . . xk：Bk. 你好，我是. . . . ，yj：Aj. A.模式W：：= （F1+···+Fn）根据模式W进行对于一些KΩ; ΔΩ·ΩW：：W∈ΩΩ;ΔΩ; Δ;A∈FkΩ; Δ（F1+···+Fn）Ω; Δ，x：A（F1+···+Fn）类型A是一个具有S元素F=所有Θθ的元素。 你好 Bθ=x1：C1， . . ，xn：Cnσ=u1[id（n）]/x1， . . ，un[id（id）]/xn好吧˜˜Ω;Δ，u1：：C1 [Ω]，. ，un：：Cn [θ]; ε ε A =[σ] ε Φ.B/（θ，Δ）Ω;Δ;A∈所有θ。 你好B组图五. 模式所有的变量都可以在θi中定义为x：A是Fk 的一个变量。图中的规则.5使用高阶模式匹配。 判断A=B /（θ，Δ）意味着θ是一个置换，使得[θ]]B=A。4覆盖检查在本节中，我们将介绍覆盖检查的理论覆盖判断的一个推导是证明给定类型A[A]的每个闭项是给定模式集合中至少一个的实例;在Beluga中，这是保护case表达式分支的模式集合。任何一组模式都覆盖了空类型的所有术语，而空性是不可判定的[6，p.179]。在Beluga中，空类型应该非常罕见。在任何情况下，由于任何算法都必须是不完整的，因此理论的完整性并不重要。C oqu and[2]anddSchuürmannanddPfenning[16]dedescribeddcoverecheckingfororclosed dterms，whileSchuürman nn[15，pp. 197我们对覆盖的理论处理是上下文模态类型理论的第一次，其中对象相对于包含上下文变量的显式上下文是封闭的。这导致了覆盖面的干净发展。要查看一组模式Z（在Beluga中，case表达式的守卫）覆盖给定类型，我们通常需要将该类型拆分为一组等效的更精确的模式。为了看到Z={Zero，Sucu}覆盖了nat[·]类型的所有（闭合）项，我们需要将nat[·]分割成模式集ZJ={Zero，Sucu1}。现在很明显，Z覆盖nat[·]，因为ZJ-分裂nat[·]的结果-与Zα-等价。更一般地说，假设我们想检查Z是否覆盖了nat[k]。如果你，我们处理的是开放数据，所以当我们拆分时，我们必须考虑变量和构造函数。假设类型是nat[nat，x：nat，y：o]，其中nat表示模式（o+nat）nat的上下文。 拆分包括构造函数、参数78J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69L变量，表示来自XML的变量的通用情况（每个模式元素一个变量），以及具体变量x和y：国家安全委员会阿克斯Zero，Sucu[id，x，y]，变量阿克斯（p1[id]：o），（p2[id]：nat），x：nat，y：o阿克斯x为oh并不是所有的变量实际上都是可能的：p1[id]是类型o，但我们分析的是nat类型。具体变量y同样是不可能的。这就给出了{Zero，Sucu[idn，x，y]，p2[idn]，x}.对于某些集合Z，我们还需要将Suc它的构造函数和变量。关于何时分割的决定并不是由我们的理论决定的;这样的决定体现在规则Obj-split和Obj-no-split之间的非确定性选择中。因此，我们的系统是覆盖检查算法的基础在对替换和高阶模式统一进行了一些评论之后，我们陈述了一些关键的元理论结果，然后描述了覆盖规则。我们写[θ]来代替Δ中的u和p变量判断Ω; ΔJ< $θ<$ Δ说θ是在图式语境Ω下，用域Δ和值域ΔJ进行的语境替换我们将ρ写成（1）模式上下文Ω上的上下文替换的缩写，替换上下文变量（2）上下文替换θ。判断ΩJ; ΔJ<$ρ：（Ω; Δ）说ρ的定义域是（Ω; Δ），它的值域是ΩJ; ΔJ。在规则中，我们将数据级替换写为[M/x]A。 这实际上是遗传替代，但我们省略了类型详见[3，附录]。我们允许Miller [7]意义上的高阶模式，其中实例化的元变量必须应用于不同的绑定变量集因此，上下文变量与诸如xΦ（1）/x1，.，xΦ（n）/xn.”[11]这是一个很有说服力的决定。下面的证明是[11]中证明的简单推广。定理4.1（高阶模式统一的如果P和Q是在Ω; Δ;和Ω; Δ; Q o P/（θ，Δ J）下的良构类型，则Ω; ΔJθ：Δ和Ω; ΔJ;[[θ]][[θ]] P =[[θ]] Q和θ是最一般的单位元，也就是说，对于所有·;·ρ：（Ω; Δ），存在ρJ使得ρ =[[ρJ]] θ。引理4.2（对象倒置）如果·; ·;R P和：W，则(1) R = cN1. 其中S（c）= N ×1：A1。···σ xk：Ak·PJ且[σ] PJ= P，或(2) R = xN1... 其中（x：λ x1：λ1. ···xk：Ak.PJ）∈且[σ] PJ= P，或（3）R=（proj#y）N1. . Nkwhere（y：y1：An1， . . . ym：Am. A<$m+1）∈<$并且d[σ]PJ= P并且d[proj]y/y1， . . ，proj#y/yL]AL+1= B1x1：B1..............xk：Bk. PJ1L其中1≤l≤m，其中σ = N1/x1，.，Nk/xk.证据通过实例分析和反演，对·; ·; R P的推导进行了研究。QJ. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69794.1承保范围判断给定案例表达式Z中的保护集，我们假设每个模式<$∈Z都有m <$ΔJ的形式。 box（英语：box） M）：A[J]，其中ΔJ给出了在M中的contextu的类型p，av a因此，格表达式中的模式不是简单的Suc u [idn，x]，而是Suc u：：nat [n，x：nat]。 box（x. Sucu [idn，x]）：nat [n，x：nat].在这个例子中，在许多情况下，ΔJ和A[J]可以在源程序中省略并重建。然而，依赖类型的ΔJ，如u：：（nd（eqx x））[x：nat]实际上限制u只匹配自然演绎证明的eqx x。 类似地，依赖类型的A可以约束整个模式。最基本的覆盖判断，Ω; Δ; ΔObj（A）DCOVERED-BYZ，意味着类型A的每个对象都被Z中的至少一个模式匹配。例如，如果我们有一个Ω; ·;Ω，x：nat，y：o的派生，则Z覆盖了类型nat [Ω，x：nat，y：o]。这样的推导具有一般形式Ω; Δ; ΩΩObj（A）DJ的子推导，它分析A并将结果作为输入给J，这是（算法上）一种延拓。早期的判决是这种形式的一个例子：它分析了A然后前面讨论的分裂运算表现为Ω; Δ; ΩM：A D J的子导子。这里，M是一个起模式作用的项，具有自由变量u[σ]。为了清楚起见，省略上下文，A=nat[·]的推导看起来像M1阿克斯的1阿克斯M2¸ x `一个2阿克斯零：不。t[·]D JSucu[·]：n. 在[·]DJ..Obj（nat[·]）DJ一般来说，M1...，Mn共同覆盖类型A的所有可能项。也就是说，子派生对应于分裂成n个模式。在该示例中，n= 2。4.2COVERED-BY：覆盖派生我们说过Obj（A）DCOVERED-BYZ意味着分析A并因此，分析了A，必要时分裂，我们最终得到Mk的子导子：AkD被Z覆盖。 这些是派生树的最外面的分支，并且是唯一检查Z的地方这种衍生物-所有元素都具有相同的结构：Covered-By-Z从80J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69ΩΔ。box（英语：box） M）：A[]COVERED-BY- 是的JjJ J JΩ Ω（Ω Δ. box（M）：A [M]）=（M Δ. box（λ.M）：A[λ]）/（θ，Δ）ΩΔ。box（英语：box） M）：A[k]COVERED-BY（kΔJ. box（英语：box） MJ）：AJ[J]）覆盖-被 -覆盖Ω; Δ; A; B;;Ω;Δ;ΩQ//oPApp-o/Ω;ΔR（Q> P）DJΩ;Δ; ΩΩoP /（θ，ΔJ）Ω;ΔJ;[[θ]]Ω[[θ]]R：[[θ]]PD[[θ]]JΩ; Δ; ΔJApp RR（Q> P）DJApp-oΩ; Δ; A_（？）Ω; Δ;ΩM：ADneutralR（x.B> P）DJΩ; Δ;ΩObj（A）DNEUTRALΩRΩ（x.B> P）DJΩ; Δ;ΩApp R RRR（Ωx：A.B> P）DJApp-Ω对于0≤i≤m：Ω;Δ;Δp p pproj#Rp（[proj#R/x1， . . ，proj#R/xi]Ai+1>P）DJi1i应用程序Ω;Δ;ΩAp pR（Ωx1：A1， . . ，xm：Am。Am+1>P）DJΩΔ。box（英语：box） M）：A[]COVERED-BYZerekΩ; Δ; ΩM：AD覆盖-由{Ω，.，}覆盖-由-Z1NΩ; Δ; Ω（λx. M）：（X：A1.A2）DJΩ; Δ; λ，x：A1λM：A2DLAMDJΩ; Δ; Ω（M，N）：Ωx：A1.A2DJΩ; Δ; ΩN：[M/x] A2D对2（M：A1，x. ·）DJD对2（M：A1，x. ·）DJΩ; Δ;λM：A1D对1（·，x.A2）DJΩ; Δ; λ，x：A1λObj（A2）DLAMDJΩ; Δ;ΩObj（Ωx：A1.A2）DJObj-ΩΩ; Δ;ΩObj（A1）DPAIR1（·，x.A2）DJΩ; Δ;ΩObj（Ωx：A1.A2）DJObj-ΩΩ; Δ;Δmvar（P）DJΩ; Δ; ΩObj（P）DJObj-no -splitΩ;Δ;ΩAp px1（ΩΔ 1. A1>P）DJ你 好A1，.，xk：k.AkΩ（Ω）=F1+···+FmΩ; Δ; P;V.Ω; Δ;ΩPVarsΩ：FmΩ>PDJ.Ω;Δ;ΩAp ppxk（Ωk. Ak>P）DJΩ; Δ;A_（？）.Ω; Δ; A_P_Ω; Δ; ΩObj（P）DJObj-splitΩ; Δ;ΩM：ADJΩ; Δ;ΩObj（A）DJJ. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6981见图6。 覆盖检查规则82J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6922setZ，然后Covered-By-检查Mk是否是的instance。3- 是的Ω Ω（Ω Δ. box（框）Mk）：Ak [θ]）= θ/（θ，Δ）覆盖-被-θ覆盖ΩΔ。box（英语：box）Mk）：Ak[]COVERED-byΩ; Δ;Ωk：Ak D覆盖-由{.，，... 个文件夹覆盖-由 -Z我们假设模式包括显式元变量上下文ΔJ，显式data-levelnamesJ，anddanexplicittypeAJ[J]. 在我们看来，这是一个有盖的婴儿床- 是的JjJ J J是Ω（Δ。box（框）Mk）：Ak [M]）=（M Δ. box（.M）：A[]） /（θ，Δ）。 这上面说Mk是由θ实现的Mj的一个实例，即Mk=[[θ]] MJ。 如果每个Mk是Z中某个模式的instance，则Z覆盖A的所有居民。4.3导出对象的规则（A）DJ在解释了覆盖推导的高级结构和叶子的细节之后，我们可以用Obj（A）D J形式的结论来讨论规则。这是图6底部的四条规则。如果A= 1.x：A1.A2，我们使用Obj-1.x来剥除该层并分析A2.之所以加上LAM，是因为在分析了A2之后，我们需要把λ放回原处并加上λ：Ω;Δ; Ω（λx. M）：（M x：A1.AJ）D JΩ; Δ;ΩM：AJ.林达杰Ω; Δ; λ，x：A1λObj（A2）DLAMDJΩ; Δ;ΩObj（Ωx：A .A）DJObj-Ω1 2注意，由于分裂A2可能会产生几个模式，我们可能会有更多的子导数（λx。... ）：（A1. （1）只显示一个。如果A= 1x：A1.A2，则规则Obj-优先分析A1，然后分析A2。图6中的规则是垂直排列的，其顺序与它们在派生中出现的顺序相同对于基本类型P，我们可以不分割（规则Obj-no-split）或分割（规则Obj-split）。后一条规则并没有看上去那么复杂 关键是要分成一组... 其中R是参数p[σ]（左侧前提）、变量x（右上方前提）或构造函数c（右下方前提），其中最简单的是构造函数c的前提Appck（S（ck）> P）。这些涵盖了所有的构造函数ck，甚至那些与P不兼容的基类型的构造函数-这些构造函数将在派生过程中被丢弃。推导形式Ω; Δ;App R（S（ck）>P）DJ的前提有些复杂，因为我们需要生成所有的脊（参数列表）N1. 嗯。这里，P表示我们正在构造P类型的对象。 构造函数类型S（ck）必须具有形式x1：A1。···xm：Am.Q，其中Q是基本类型。推导3我们不需要任何东西，不只是相等的，在覆盖范围内。 Suppo se Z={（u1[·]，Zero），（Zero，u2[·]）}.为了使 （Zero，Sucv2[·]）被 转换 （通 过Z中的填充图案），我们需要填充第一个分量，并且为了使（Sucv1[·]，Zero）被转换（通过Z中的填充图案 ），我们需要填充第二个分量。这导致一组模式，包括（Zero，Zero），它不等于Z中的任何模式。J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6983一期+1Ω;Δ;ΩP VarsΩ：所有的Θ均为Ω。 你好Aj+1> PDJΘθ=y1：Bθ1， . . . ，yn：Bn 并且，dΦ1=x1：AΦ1， . . ，xj：Ajσ= u1[idσ]/y1， . . ，un[idn]/ynΔΘ= u1：：Bn1[id n]， . . ，un：：Bn[]对于0≤i≤j：σJ=（proj#p [idj]）/x1，. ，（proj#p [idn]）/xi1我Ω;Δ，ΔΘ，p：：[σ]（（ΩΦ），Aj+1）[]）;Approj#Ω;Δ;ΩP VarsΩ：所有的Θ均为Ω。 你好A.p[id]（[σJ][σ]Ai+1>P）DJPVars公司简介j+1有效Wk（Ω;ΔP[Ω]）={1，. ，n}Ω; Δ，u：：P[1];（u[id（1）]：P）DJ.Ω; Δ，u：：P[n];Ω（u[id（n）]：P）DJΩ; Δ;ΩMVars（P）DJMVars图第七章覆盖检查规则（续）在此，我们使用App-10，它使用Obj（A1）来分析A1，并且（通过NEUTRAL）将A1的所得居民M1添加到ck。对每个xi：Ai做这件事会产生AppckN1. Nπ（Q> P），对于vi，pinesN1. . 嗯。如果Q和P不一致（writenQ/o/PinruleeApp-//o）我们有一个平凡覆盖子导子，但如果Q和P在某个θ下统一，则我们可以使用Ap p-o，其中有一个伪[θ]]R：[[θ]]PD[[θ]]J.返回到规则Obj-split本身，前提App对于变量在结构上类似于建筑师。然而，与S（ck）不同的是，变量类型B可以包含数组，因此我们使用App-数组从元组中取出投影Obj-split 的其余前提具有形式PVars：F>PDJ，表征了类属变量情况。4.4PVars参数：F>PDJ：参数变量PVars的结论是，. 因此，规则PVars在图7中。在PVars中，我们为每个模式元素生成一个参数变量我们首先为元素中的每个全量化变量创建一个元变量例如，如果F =所有A：o。A，则p[id]具有类型ndu[id]，其中u是（新鲜的）元变量。一般来说，我们得到一个零件的类型来自所有的零件 。你好一个简单的替代方案σJ将所有变量都设置为零，并将σj设置为零。一个小女孩。新的使用者将此标识视为符合条件的可用标识。 Aga in，s ince[σJ]<$Φ<$。我是一个小女孩，tuples，我们考虑所有可能的投影。4.5MVars（P）DJ：P的所有地面实例的一般情况规则Obj-no-split的前提是MVars（P），它只能由规则MVarsΩ; Δ;Δmvar（P）DJ84J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）69（图7）。这个规则不会递归地分析给定的类型P。而是J. 邓菲尔德湾Pientka/Electronic Notes in Theoretical Computer Science 228（2009）6985生成模式u[id（k）]，任何类型P[k]的对象都可以与之匹