高阶抽象函数和显式替换的函数程序设计和类型系统

理论计算机科学电子笔记174（2007）41-60www.elsevier.com/locate/entcs高阶抽象函数和显式替换的函数程序设计Brigitte Pientka1麦吉尔大学计算机科学学院加拿大蒙特利尔大学摘要本文概述了基于上下文模态类型理论[9]的高阶抽象语法和显式替换的编程基础。上下文模态类型不仅允许我们干净地将数据对象的表示与计算分离，还允许我们递归使用自由变量的数据对象。在本文中，我们通过添加第一类上下文和替换来进一步扩展这些想法，以便程序可以传递和访问具有自由变量和显式环境的代码，并以类型安全的方式将它们链接起来。我们勾勒出这种语言的静态和操作语义，并给出几个例子来说明这些功能。保留字：逻辑框架，类型系统1介绍高阶抽象语法是一种简单的公认的技术，用于实现具有变量和绑定器的语言。这个问题通常是实现求值器、编译器或自动推理系统时的关键高阶抽象语法背后的中心思想是通过元语言中的变量和绑定器实现对象级变量和绑定器（即函数式编程语言）。高阶抽象语法表示背后的一个关键好处是，可以避免实现处理变量的常见和棘手的例程，例如避免捕获的替换，重命名和新鲜名称生成。高阶抽象语法及其实用性早已在逻辑框架LF [3]及其在BMF系统[12]中的实现中得到证明。然而，它一直难以扩展主流的函数式编程语言，直接支持高阶语法编码。困难是由于高阶抽象语法编码在1 电子邮件地址：bpientka@cs.mcgill.ca1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.10.03742B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41通常的感觉。问题是高阶抽象语法上的递归需要遍历λ-抽象，因此我们需要能够推理基于[9]中的思想，我们提出了一种基于上下文模态类型的新方法，该方法允许在开放术语上递归，并且还支持第一类环境和上下文。与我们的工作最密切相关的是Despeyroux，Pfenning和Schürmann[2]以前的建议，其中提出了一种改进的λ-calculus，其中通过迭代器支持高阶编码上的然而，通过迭代的函数定义不支持模式匹配，并且不容易支持动态假设的推理。这个问题在[15]中得到了解决，微积分被提出作为一种补救措施。 它也是Elphin语言他们的工作需要作用域堆栈和对它们的显式操作，例如弹出作用域堆栈的元素。然后在一定范围内执行函数。跟踪当前作用域的必要性也渗透到操作语义中，操作语义显式地跟踪作用域堆栈。与这些方法相反，我们认为语境情态类型理论[9]可以为扩展函数式编程提供一个干净而优雅的框架，支持高阶抽象语法和模式匹配。由于我们允许抽象上下文变量，我们可以将作用域（上下文）与传递给函数的每个参数相关联，而不是与函数本身相关联。这使我们能够编写接受开放数据对象作为输入的程序，并对数据对象和程序实施更强的不变量。我们也相信这将有助于我们编写程序的推理。[15]以前的方法只允许在递归过程中打开对象，但要求在计算开始时关闭对象。此外，我们的建议扩展到支持独立有趣和有用的第一类替换。第一类替换在显式环境下的编程中具有潜在的意义，它具有广泛的应用，例如基于环境的解释器或常数消除算法。我们的底层上下文模态类型系统保证程序可以传递和访问开放术语，并且可以安全地与环境链接。在本文中，我们采取了第一步，设计一个基础的程序与高阶抽象语法和显式替换的基础上，上下文模态类型理论。我们首先介绍一个例子来强调使用高阶抽象语法编程时的一些问题，然后通过调整和扩展上下文模态类型理论来提供理论基础。最后，我们给出了几个例子，说明了显式替换编程的基本思想。由于显式替换可以被看作是值变量对，这个工具本质上允许我们对显式环境进行建模。此外，我们的底层类型系统将确保正确使用此环境，并静态地强制执行关键的不变量，例如在某个环境中，项M中出现的每个B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41432激励的例子在这一节中，我们简要地讨论了我们的一些主要想法和关注使用一个简单的例子，分析和比较的结构的非正式条款。为了向函数式编程语言添加高阶编码，我们遵循[2，15]中采用的方法，通过模态运算符分离表示和计算级别。数据对象M可以利用高阶抽象语法并且经由盒构造盒M被注入到程序中，其中M表示对象级数据。计算级描述了我们的函数程序，它在对象级术语上操作。在这个级别上，我们允许递归和模式匹配对象级的条款，以提取子条款。然而，与先前的提议不同，每个对象M都携带其自己的本地上下文，使得box（M.M）从而允许使用开放对象进行编程。为了说明这一点，首先考虑以下两个基于高阶抽象语法的非线性项的定义。对象级表达式对象级术语lam：（exp→exp）→ exp.lamJ：（term→term）→term.应用程序：exp→exp → exp。appJ：term→term →term。我们感兴趣的是定义一个函数related，它检查表达式是否 这个函数只是比较一个术语和一个表达式的基本形状，但它不检查变量名是否相等。例如，我们考虑术语lam λx。拉姆λy。appxy与表达式相关lamJλx. 林杰应用程序Jy x.因此，我们的计算将从相关的（box（·. lamλx. 拉姆λy。appxy））（box（·. la mJλx. 我的天。（appJyx））递归地，我们遍历该Binder，并在下一次迭代中计算相关（框（x：exp. 拉姆λy。appx y）（box（x：term. 林杰appJy x））正如我们所看到的，每个参数都带有自己的本地上下文，当我们遍历绑定器时，它会被扩展。在下一次迭代中，局部上下文再次被扩展。相关（box（x：exp，y：exp. app x y））（box（x：term，y：term.appJy x））最后，我们需要检查相关（box（x：exp，y：exp. x））（box（x：term，y：term. （y））如何写一个递归函数相关和什么类型应该有？函数related将term类型的open对象和exp类型的open对象作为输入。与每个打开的对象关联的局部上下文将在其类型中被反映。在以前的建议中，term类型的对象级数据被赋予了类型Q项，我们为具有类型term的开放对象M编写term[x：term44B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41在上下文中，x：term。类似地，我们写exp[x：exp，y：exp]用于在上下文x：exp，y：exp中具有exp类型的开放对象M。为了实际编写递归程序并为它们分配类型，我们需要能够抽象具体的上下文，因为它在执行过程中会发生变化，我们必须为上下文变量描述有效的实例。上下文变量的有效实例可以通过上下文模式或世界来描述（参见[14]）。让expr W是描述上下文模式x 1的常数：exp，.，xn：exp，并且termW是描述上下文模式y1：term，.，yk：term。然后我们可以为函数声明一个相关类型，如下所示：相关：EXPRW。电子邮件：termW. exp [γ] →term [γ] →bool.在我们展示相关函数的代码之前，我们在这里讨论一些注意事项。 首先，通过模式匹配定义递归函数，并需要提取子表达式。为了描述u[σ]表示具有推迟替换σ的闭包。 其次，我们需要能够对对象级变量进行模式匹配。 这将通过对上下文变量的出现施加约束来实现。context变量x（x：term）表示termW类型的context，它必须包含至少一个元素x：term。我们现在可以给出下一个相关函数的代码。fun related [g] [g']（box g'（y：exp）.y）（box g（x：term）.x）= true| related [g] [g’] (box g. lam[x]. u[id g，x/x]）（方框g）lam' [y]. v[idg'，y/y']）=相关[g，x：exp] [g'，y：term]（方框g，x：u[id g，x/x]）（方框g '，y：期限。 v[idg'，y/y']）| related [g] [g’] (box g. appu1[id g] u2[id g]）（方框g）app' v1[id g'] v2[id g']）=相关[g] [g']（框g. u1[id g]）（boxg'.v1[id g']）以及相关[g][g']（方框g. u2[idg]）（框g'.v2[id g']）一个有趣的问题是如何修改这个程序，使我们检查精确的形状。一个可能的解决方案是修改相关函数的类型，使两个对象共享相同的上下文。 这样的广义上下文具有以下形状：（x1：term，y1：exp），...，（xn：term，yn：exp）.我们使用括号来强调这个上下文是由元组（xi：term，yi：exp）构建的。让termExpW成为描述这个世界的常数。然后我们可以声明一个依赖将函数rel的类型设置为：γ：termExpW。exp[γ]→term[γ]→bool.B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4145fun rel [g]（box g（x：term，y：exp）.x）（box g（x：term，y：exp）.y）=true| rel [g] (box g. lam[x]. u[id g，x/x']）（方框g）lam' [y]. v[id g，y/rel [g，x：term，y：exp]（框g，x：term，y：exp.u [id g，x/x']）（方框g，x：期限，y：到期日）v[id g，y/y']）| rel [g] (box g. app u1[id g] u2[id g]）（方框g. apprel [g]（方框g. u1[id g]）（方框g.v1[idg]）以及rel [g]（方框g. u2[id g]）（box g.v2[id g]）在我们的设置中，一个重要的问题是α-等价和上下文变量的范围。我们考虑box（x：term）。x）α-等价于box（y：term）。y）？Is box（x：term，y：term. y）α-等价于box（z：term，w：term. w）？我们允许对上下文变量进行哪些操作？– Inthe following theoretical development, we will pay careful attention to these3手续对象级术语和类型在这一节中，我们将介绍基于语境模态类型理论的形式化定义和类型系统。我们从对象语言开始，它是按照[9]中的思想定义的，并且只定义规范形式的对象，因为只有这些对象对表示对象语言才有意义。为了简单起见，我们将其限制为简单类型的片段。A、B、C型：：= α|A→B正规项M，N：：= λx. M|R中性术语R：：= x|C|RN|u [σ]置换σ，ρ：：=·|σ，M/x|s [σ] |id（ω）Contexts，Φ：：=|x：A|（ω）元语境Δ：：=·|Δ，u：：A [] |Δ，s：：Δ [Φ]|中文（简体）约束条件ω：：=·|ω，x：A简单类型模态lambda演算有几个有趣的方面。首先，我们区分普通约束变量x和上下文模态变量u[σ]。上下文模态变量u[σ]表示具有延迟替换σ的闭包。正如我们在上一节中简要提到的，上下文模态变量将用于定义模式匹配。有时我们也称上下文模态变量为元变量。我们的意图是，一旦我们知道u应该代表哪个项，就应用σ。σ的定义域描述了在代表u的项中可能出现的自由变量。更多详情46B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41关于上下文模态变量，我们请感兴趣的读者参考[9]。这里我们提出用上下文变量s[σ]和替换变量s[σ]来扩展微积分。上下文变量可以用约束ω来注释，该约束ω对上下文变量ω施加条件。例如，x1（x：A）表示由块xi：A构建的上下文，并且包含至少一个这样的块。 换句话说，类型为A必须在上下文中出现。我们还注意到，只有当ω中提到的变量没有在ω中声明时，<$（ω），<$才是良构的。目前，我们将约束的使用限制在对象中出现的上下文变量上。类型中出现的上下文变量不允许与任何约束相关联2.我们还需要一个第一类的恒等式替换概念idω。如果我们的目标是使用上下文模态类型作为高阶抽象语法编程的基础，那么在上下文和替换上进行抽象似乎是一个有趣且必不可少的上下文模态变量u、替换变量s和上下文变量在元上下文Δ中声明。 上下文变量被声明为属于上下文模式W，我们假设它在a签名中被声明，类似于在a签名中的类型和世界声明。我们在这里省略了世界和语境图式的确切定义，并请感兴趣的读者参阅[14，13]。通常，我们也会抑制签名验证，因为它在类型化派生过程中永远不会改变，但请记住，所有类型化判断都可以访问格式良好的签名。在签名中检查类型A是否格式良好是很简单的，因为没有依赖关系。接下来，我们基本上遵循[9]中的思想，只描述我们假设只有简单类型（没有依赖关系）和对象级别的类型常量a以及表示上下文模式的常量已经在签名中声明。接下来，我们描述主要的类型判断和类型规则。Δ;M A对照类型A检查正常对象MΔ;RA为原子对象RΔ合成类型A; Φ σ对照上下文检查替换σ我们将默认重命名绑定变量，并保持上下文和substitution- tutions声明变量不超过一次。请注意，替换σ仅定义在普通变量x上，而不是模态变量u上。我们还通过总是同时替换所有普通变量来稍微简化微积分。这不是必需的，但在涉及同时和迭代替换时节省了一些繁琐。我们将在这里省略格式良好的上下文和格式良好的约束的定义，但专注于术语和替换的类型。在类型化过程中，我们引用ω：W，它保证了约束ω对应于上下文模式W。2在类型中允许约束会在定义替换时产生复杂性B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4147对象级术语Δ;，x：AMBΔ; Δλx.MΔA→BΔ; RPJPJ =PΔ;ΔRx：A∈NΔ; β-淀粉酶xβ-淀粉酶Ax：A∈ω x：A/∈Δω：W∈Δω：WΔ;（ω），xAc：A∈Δ;cAu：：A[Φ]∈ ΔΔ;<$$>σ<$ΦΔ;<$$>u[σ]<$AΔ;MA→BΔ;NAΔ;ΔN对象级替换Δ;··Δ;σ Φ Δ;MAΔ;Δ（σ，M/x）Δ（Φ，x：A）s：：Φ1 [Φ2]∈ Δ Φ = Φ1 Δ; ερε Φ2Δ;ε（s[ρ]）εΦω：W∈Δω：WΔ;（ω），id（ω）（ω）我们注意到，我们需要约束变量的通常条件。例如，在abstraction的规则中，绑定变量x必须是新的，并且不能已经出现在上下文中这可以通过alpha重命名来实现计算级表达式我们的目标是干净地分离对象级和计算级。对象级描述数据，计算级描述对数据进行操作的程序计算级类型可以通过上下文类型A[]来引用对象级类型，上下文类型A []表示类型A的对象，该对象可以包含在中指定的变量。为了允许在上下文变量上进行量化，我们引入了一个依赖类型：W.τ，其中W表示上下文模式和通过Λτ.e的上下文抽象。类型τ：：= A [] |Φ [] |τ1→τ2|中文（简体）表达式e：：= y|recf.e|e1e2|fny.e|Λ.e|e[||（e：τ）|sbox（英语：sbox）|sbox (Ψ.σ）|例e，p1|......这是什么？|pn分支p，q：：= u：：A [].p |s：：Φ [|box（.M）›→ e |sbox（英语：sbox）σ）›→ e上下文Γ：：=·|r，y：τ数据可以通过盒构造盒（box.M）注入程序。这里M表示一个对象级项M，它可48B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41以包含在上下文中指定的变量。类似地，我们可以注入替换sbox（sbox）。σ），其中σ是B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4149替代σ。由于替换可以被看作是变量和对象级项之间的配对，因此这种功能本质上允许我们对显式环境进行建模最后，我们允许模式匹配对象级别的条款，通过case语句。为了简化理论发展，我们要求模式中出现的所有上下文模态然而，我们还不认为匹配上下文变量。 我们重载了→，它用于表示函数类型在对象级别以及计算级别上。我们也可以使用x和y作为对象级变量和程序变量。然而，从用法上应该很清楚我们指的是哪一个。接下来，我们考虑程序的输入规则我们在这里区分表达式和分支的类型。注意，为了对表达式和分支进行类型化，我们将参考对象级术语的类型化此外，我们采取双向的观点。表达式e具有τ型Δ; Γeτ合成表达式e的τΔ; ΔJ;rp：τJτ分支p针对τJτ进行检查接 下 来 是 表 达 式 的 类 型 规 则 。 我 们 只 指 出 几 个 有 趣 的 问 题 。 首 先 是 box（box.M）的类型规则。M表示对象级项，其自由变量在上下文中定义，即它相对于上下文是封闭的。为了键入box（M.M），我们切换到对象级类型，并且忘记仅描述计算级上的假设的复杂上下文Γ。类似的推理也适用于sbox的类型化规则（sbox）。σ）。为了访问数据，我们提供了一个带有模式匹配的case语句.其目的是匹配模式中出现的上下文情态变量。表达式Δ，τ：W;τeτΔ; r Λ.e：W.τΔ; r，f：τeτΔ; r=0.Δ; r，y：τ1eτ2Δ;Γfny.eτ1→τ2Δ; MA≤JΔ;Γbox（.M）A[J]Δ; σ Φ≤ JΔ; Γsbox（. σ）Φ[J]对于所有iΔ;·; Γpi：A[]τ，Δ; Γe A[]Δ; Γ是p 1的情况e|......这是什么？| pn ⇐τΔ;ΓeΦ[]foralliΔ;·; Γpi：Φ[]τΔ; Γ是p 1的情况e|......这是什么？| pn ⇐τΔ; τeτJτ =τJΔ; Γε ετΔ; Γε ετΔ; r（e：τ）τy：τ∈ΓΔ;Γy<$τΔ; re：W.τ：W Δ;re[|[[Δ; Γε1<$τ2→τΔ; Γε2<$τ2Δ; Γε1e2τ50B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41分支Δ;（ΔJ，u：：A[Φ]）; Γπp：τ1πτΔ; ΔJ;Γ u：：A[Φ].p：τ1<$τΔ，（ΔJ，s：：τ [Φ]）; ττp：τ1ττΔ; ΔJ;Γ s：：[Φ].p：τ1τΔJ;Γ-box（M）<$τ1（Δ， ΔJ）; Γ-e<$τΔ; ΔJ;Γbox（τ.M）›→e：τ1<$τΔ J; r_（？）σ）<$τ1（Δ，Δ J）;Δ; Δ J; r_（？）σ）›→e：τ1 <$τ上下文（ω）≤≤n，x：A≤nJ，x：A·≤·在这里，我们还观察到通常的绑定变量重命名条件。在函数规则中，我们假设变量x是新的，并且没有在 I.上下文变量被明确量化并由Λ约束。 特别地，上下文变量box（box）中的 M）不受盒子的约束。还记得，我们做不允许在类型中绑定上下文变量的约束。因此，比较两个上下文，例如在box的规则中，只是检查我们是否可以通过删除任何约束ω从可以存在于上下文变量中。在显式替换的规则中，我们可能需要重命名σ的定义域。这总是可以实现的。替换域的重命名由σJ/σ i表示。 Similarly，inthe rule forbox（. M）我们可以重命名在XNUJ中的变量，以匹配在XNUJ中的变量。4普通替换和上下文替换在本节中，我们定义替换操作。因为我们有几种不同的变量，所以有多种替换操作.我们将依次考虑这些操作程序和对象级变量这些操作是避免捕获的，并以标准方式定义。我们的约定是，作为对象级项和表达式上的定义操作的替换用前缀符号[M/x]N表示对象级替换以及[e/x]eJ用于计算级替换。注意，在[M/x]N中，绑定变量x表示对象级项，而在[e/x]eJ中，绑定变量x表示计算级表达式。我们只在计算水平来说明一些基本原理。 [M/x]N的细节可以B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4151在[9]中找到。接下来，我们定义计算级表达式和分支的替换。[e/x]（x）=e[e/x]（y）=y，如果y x[e/x]（Λ.eJ）= Λ. [e/x]eJ，条件是<$/∈FV（e）[e/x]（eJ[m]）|）= [e/x] eJ[x]|[e/x]（fn y.eJ）= fn y。[e/x]eJ， 条件是y/∈FV（e）且y/=x[e/x]（rec f.eJ）= rec f. [e/x]ej， 条件是f/∈FV（e）和fx[e/x]（e1e2）=（[e/x]e1）（[e/x]e2）[e/x]（box（.M））=box（.M）[e/x]（sbox（x）） σ））= sbox（σ. σ）[e/x]（第1页的情况eJ|......这是什么？|......这是什么？|... | [e/x]pn[e/x](ϵu:: A [Φ].p)= ϵu:: A [Φ]. [英]p[e/x]（εs：：ε [Φ].p）= εs：：ε [Φ]。[英]p[e/x]（box（M）<$→eJ）=box（M）<$→[e/x]eJ[e/x]（sbox（x））σ）<$→ e（J） = sbox（？）σ）›→ [e/x] eJ注意，box（C.M）不包含程序变量x的任何自由出现，因此替换没有效果。类似地，sbox（sbox）的情况也是如此。当[e/x]应用于它时，σ）没有变化。定理4.1（计算级变量的若Δ; r ∈τ且Δ; r，x：τ，r J∈J，则Δ; r，r J∈ [e/x] J。证据 通过归纳法对结构进行二次推导。Q类似的替换原则也适用于对象级变量。定理4.2（对象级变量的替换）如果Δ; M <$A和Δ;，x：A，j <$J，则Δ;，j <$[M/x] J。证据 通过归纳法对结构进行二次推导。Q元变量的上下文替换上下文变量u的替换有点困难。我们可以把u[σ]看作一个闭包，只要我们知道u应该代表哪个项，我们就可以对它应用σ。由于α转换，在u的不同出现处被替换的变量可能是不同的，元变量的上下文替换必须携带上下文，写为[[M.M/u]]N，[M. M/u]σ和[M.M/u]e，其中σ绑定52B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41M中的所有自由变量。这种复杂性可以消除在我们的演算的基础上德布鲁因指数的实现。接下来，我们将展示对象级术语的上下文替换[[μ.M/u]]（x）=x[[μ.M/u]]（λy.N） =λy。[[.M/u]]N[[μ.M/u]]（R N）=（[μ.M/u]]R）（[μ.M/u]]N）[[.M/u]]（u[σ]）=[.M/u]]σ/]M[[.M/u]]（v[σ]）=v[.M/u]]σ]，前提是v/=u[[. M/u]]（·）=·[[.M/u]]（σ，N/y）=[.M/u]]σ，（[[.M/u]]N）/y[[.M/u]]（s[ρ]）=[s[（[[.M/u]]ρ）][[.M/u]]（id）=id将[M.M/u]应用于闭包u[σ]首先得到同时替换σJ= [[M.M/u]]σ，但它并没有返回M[σJ]，而是继续急切地将σJ应用于M。 然而，在执行σJ这是一个很好的例子，不是由σJ/σ n定义的。Contextualsubstitutionintomputation-level接下来是表情[[μ.M/u]]（x）=x[[μ.M/u]]（Λ μ.e）=Λ μ. [[.M/u]]e[[.M/u]]（e [|）=（[.M/u]] e）[|[[μ.M/u]]（rec f.e）= rec f. [[.M/u]]e[[m.M/u]]（fn y.e）= fn y. [[.M/u]]e[[.M/u]]（e1e2）=（[.M/u]]e1）（[.M/u]]e2）[[μ.M/u]]（box（Φ.N））= box（Φ. [[μ.M/u]] N）[[M.M/u]]（sbox（Φ. σ））= sbox（Φ. [[μ.M/u]] σ）[[M/u]]（p 1的情况e|......这是什么？|......这是什么？|... | [[Ψ.M/u]] pn函数和递归的情况不必考虑避免捕获的副条件。由于M必须相对于M是封闭的，并且元变量u与计算级变量x不同，因此不会发生冲突。最后，将上下文替换为计算级分支。B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4153[[μ.M/u]]（μ v：：B [Φ].p）= μ v：：B [Φ]. [[M/u]] p如果v/∈FMV（M）且v/= u[[μ.M/u]]（μ s：：μ [Φ].p） = μ s：：μ [Φ]. [[M/u]]pifs/∈FMV（M）[[.M/u]]（box（Φ.N）<$→e））=box（Φ.N）<$→[[.M/u]]e[[M.M/u]]（sbox（Φ. σ）<$→ e））= sbox（Φ. σ）›→ [[M/u]] e最后，分支机构的案例很有趣。我们要求在模式N→e中出现的所有上下文变量都被明确量化，因此我们不将上下文替换[M.M/u]应用于描述模式的对象N模式，但只有E。上下文替换满足以下替换属性。定理4.3（上下文模态替换）(i) 如果Δ; r M A和Δ，u：：A []; r J，则Δ; r [[. M/u]] J。(ii) 如果Δ; Φ M A和Δ，u：：A []; Φ J，则Δ; Φ [[. M/u]] J。证据 通过二阶导数的结构归纳法。Q上下文变量接下来，我们考虑上下文变量的替换。与之前的完全替换操作不同，如果上下文变量ω不满足ω，则将上下文ω替换为上下文变量ω（ω）可能会失败。我们首先考虑上下文替换到计算级表达式。[[/]]（x）=x[[/]]（Λ γ.e）= Λ γ. [[/]] e，条件是γ/∈ FV（）[[/]]（e [Φ|）=（[/]] e）[/]]Φ|[[/]]（fn y.e）= fn y. [[/]]e（rec f.e）= rec f. [[/]]e[[/]]（e1e2）=（[/]]e1）（[/]]e2）[[/]]（box（Φ.N））= box（[[/]]Φ. [[/]] N）[[/]]（sbox（Φ. σ））= sbox（Φ. [[/]] σ）[[/]]（第1页的情况e|......这是什么？|......这是什么？|... | qk其中[[/]]pi=qi，对于某些i在box（Φ.N）的情况下，我们对上下文Φ和对象N都应用替换[/]。虽然对象N不包含上下文变量，54B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41它可以包含需要展开的身份替换ID（ID）。 类似的考虑适用于sbox（Φ.σ）。请注意，对某些分支pi应用替换[[/]实际上可能会失败，并且替换操作会消除这些分支，因为它们不可访问。覆盖检查[14]将保证至少有一个分支在应用替换[/]]时会成功，我们可以保证进度。因此，只有当我们覆盖了所有可能的情况，保证至少有一种情况下将[/]应用于分支成功时，将[/]的最有趣的情况是实际的替换必须发生。[[/]]（·）=·[[/]]（Φ，x：A）=（[/]]Φ），x：A假设x/∈V（[[/]]Φ）[[/]]（（ω）） =如果满足ω。[[/]]（φ（ω））=φ对于φ/= φ。[[/]]（·）=·[[/]]（σ，M/x）=[[/]]σ，[[/]]M/x[[/]]（s[ρ]）=s[/]]ρ][[/]]（id（ω））=id（），如果满足ω。[[/]]（idφ（ω））=idφ（ω）我们回想一下，绑定上下文变量的唯一构造是上下文抽象Λ.e和box（x）。M）或sbox（M.σ）不约束σ。身份替换的扩展定义如下：id（·）=·id（x，x：A）=id（x），x/xid（（ω））=id（ω）引理4.4如果id（k）= σ则Δ; k，k j <$σ<$k。证据 对结构的归纳Q引理4.5(i) 如果Δ，：W;（ω），ΦMA和：W和满足ω则Δ;，Φ M A。(ii) 如果Δ，：W;（ω），Φeτ，e覆盖检查，：W和满足ω则Δ; φ，Φ ε ετ。证据第一次推导的结构归纳法。QB. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4155接下来，我们给出替换变量的简单定义。[[.σ/s]]（x）=x[[σ.σ/s]]（λy.N）= λy. [[.σ/s]]N[[.σ/s]]（N1N2）=（[.σ/s]]N1）（[.σ/s]]N2）[[. σ/s]]（u [ρ]） = u [. σ/s]] ρ][[.σ/s]]（·）=·[[.σ/s]]（σ，N/y）=[.σ/s]]σ，（[[.σ/s]]N）/y[[. [1][2][3][4][5][6][7][8][9][10] σ/s]]ρ）/]σ[[.σ/s]]（sJ[ρ]）=[sJ[（[[.σ/s]]ρ）][[.σ/s]]（idφ）=idφ首先将[.σ/s]应用于闭包s[ρ]得到同时替换ρJ= [[.σ/s]]ρ，但它并没有返回σ[ρJ]，而是急切地将ρJ应用于σ。然而，在执行ρJ之前，必须重命名它这是一个很好的例子，请注意，这是一个很好的例子。引理4.6(i) 如果Δ; σ J和Δ，s：：J []; Φ J，则Δ; Φ[[. σ/s]] J。(ii) 如果Δ; σ J和Δ，s：：J []; Γ J，则Δ; Γ [[. σ/s]] J。证据 通过二阶导数的结构归纳法。Q5操作语义在本节中，我们将为所介绍的语言勾画一个小步操作语义。在执行过程中，类型注释应该是不必要的，我们只在所有类型注释都被删除的表达式上定义求值。首先，我们定义这种语言的价值。值v：：= fny.e|Λ γ.e|箱（.M）|sbox（英语：sbox）σ）接下来，我们定义一个小步评估判断：e−→eJ表达式e在一个步骤中求值为eJ。.JJΔbox（.M）=p−→e分支p匹配box（.M），并步进到e.JJΔΔ sbox（Δ sbox）σ）= p −→ e分支p匹配sbox（σ）。σ）和步骤e56B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41在分支判断中，我们注意到box（M.M）不包含任何元变量，即它是封闭的，并且Δ表征发生B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）4157在分支P。我们只集中在三个有趣的情况下，实际计算发生。函数应用的情况很简单。程序变量的值通过计算级替换来传播上下文变量的实例化是通过将具体的上下文抽象应用于上下文抽象来传播的。最后，针对box（S.M）和sbox（S. M）的模式匹配，给出了一个实例。σ）。在这里，我们需要通过上下文子概念来传播对象级术语。（fny.e）v−→[v/y]e（Λ.e）[]−→[[/]]e.J·box（.M）=pi−→e（第1页的格（框（M）|......这是什么？| pn) −→ eJ.J·BUSINSBOX（英语：BUSINSBOX）σ）= pi−→ e（case（sbox（sbox））σ））的p1|......这是什么？| pn) −→ eJ由于评估依赖于模式匹配的对象级的条款，我们简单地描述这个过程。 特别地，我们依赖于高阶模式匹配来匹配box（.M）对box（.MJ）›→e. Miller意义下的高阶模式[7]在句法上限制上下文模态变量u[σ]的出现。 拍-术语限制强制与上下文模态变量u相关联的替换σ仅将变量映射到变量，并且具有以下形式：y1/x1，.，yn/xn。这确保了高阶模式匹配在λ-抽象存在的对于高阶模式匹配的判断可以描述如下：.JJJΔ;θM=M /θ M匹配Ms.t. [θ]]M=M上下文模态变量的高阶模式匹配的描述可以在[10]中找到。似乎可行的是，将这种描述扩展到也包含替换，同时保留高阶模式匹配的正确性和关键不变量，例如(i) θ有定义域Δ，并在Δ s. t中实例化所有模态变量·Δθ：Δ。(ii) M= [[θ]]N，即对象M在语法上等于[θ]]N。我们现在能够描述计算级模式匹配，box（M）对模式p。sbox的模式匹配（？σ）遵循类似的想法。.JΔ，v：：A[Φ]box（μ.M）=p−→e.JΔλbox（λ.M）=（λ v：：A[Φ].p）−→eJ.JΔ，s：：Φ [Φ]box（.M）=p−→e.JJΔbox（.M）=（s：：Φ [Φ].p）−→e.JΔ;θM=M/θ.JΔbox（.M）=（box（.M）<$→e）−→[[θ]]e58B. Pientka/Electronic Notes in Theoretical Computer Science 174（2007）41给定当前的设置，我们可以证明我们提出的函数式语言具有高阶抽象语法和显式替换的类型安全性。让|e|是e的所有类型分配的擦除。定理5.1(i) 如果·|e|这是一个价值或价值观，是一个新的经验。 |e|−→|eJ|还有......(ii) 如果·|e|这是一个价值或价值观，是一个新的经验。 |e|−→|eJ|还有......证据通过结构归纳法，在第一次推导中使用规范形式引理，覆盖的正确性，高阶模式匹配的正确性，以及我们之前证明的Q6示例在本节中，我们将展示几个例子来说明所提出的想法的潜在所有的例子都需要上下文变量来表示我们递归的开放世界这个世界在运行时是已知的，但会发生变化。我们相信，这个基础足够强大，可以使用来自BRDF存储库的高阶抽象语法来处理大多数示例[12]。这些例子还没有基本使用替代变量和第一类替代。变量计数首先，我们展示了一个非常简单的函数，它计算使用高阶抽象语法定义的表达式中出现的绑定变量我们假设，我们已经使用高阶抽象语法为表达式声明了一个数据类型exp，包含对象lam：（exp → exp）→ exp和app：exp → exp → exp。. 我们假设我们有可用的基本计算级类型，例如NAT、String或Bool。reccnt.Λ γ。fne. box（γ（x：exp）. x）›→ 1| ϵ u::exp[γ,xJ:exp].bOx（γ. lamλx：exp.u[idγ，x/xJ]）›→cnt[γ，x：exp|（box（γ，x：exp. u[idγ，x/xJ]））| ϵu:: exp [γ] ϵv:: exp [γ]. box（γ. appu[idγ]v[idγ]）›→cnt[γ|（box（γ. u [idγ]））+cnt [γ|（box（γ. v[idγ]））注意，我们需要使用上下文变量γ来表示可能出现在项e中的变量的上下文，这些变量将在递归过程中建立只有在运行时，我们才知道实际的上下文。 省略一些类型信息（我们认为是隐式的），并遵循类似于λ-abstraction的语法，其中λ-abstraction由[x]表示。这可以被美化为：B. Pientka/Electronic Notes in Theoretical Com