模式演算中的de Bruijn指数和纯模式演算的介绍与应用

可在www.sciencedirect.com在线获取理论计算机科学电子笔记351（2020）95-113www.elsevier.com/locate/entcsPurePatternCalculus`aladeBruijn1亚历克西斯·马尔金阿根廷布宜诺斯艾利斯大学亚历杭德罗·雷奥斯阿根廷布宜诺斯艾利斯大学那就是维索Universidad de Buenos Aires，Argentina阿根廷摘要在编程语言领域中众所周知，处理变量名和绑定器可能导致冲突，例如在实现解释器或编译器时不期望的捕获。这种情况已经被克服了诉诸de Bruijn指数的结石，其中绑定器捕获只有一个变量名，比如λ演算这种方法的优点在于，当使用索引时，所谓的α等价性变成了语法上的等价性近年来，模式演算由于其表现力而获得了相当大的关注。岁众所周知，它非常方便地研究现代函数式编程语言的基础建模功能，如模式匹配，路径多态性，模式多态性等。然而，当涉及到处理α转换和绑定器同时捕获多个变量名时，文献就显得不足了。这就是纯模式演算（PPC）的情况：λ演算的自然扩展，允许抽象几乎任何术语。本文扩展了de Bruijn关键词：de Bruijn指标，模式演算，模式匹配，α-等价。1介绍函数式编程语言的基础，如LISP，Miranda，Haskell或ML家族（Caml，SML，OCaml等）。强烈依赖于对λ-演算[2]及其多年来引入的许多变体的研究。其中有模式演算[23，7，16，6，14，12，18]，其关键特征可以被识别为模式匹配。模式匹配在程序设计中得到了广泛的应用1这项工作得到了LIA INFINIS和ECOS-Sud计划PA 17 C 01的部分支持https://doi.org/10.1016/j.entcs.2020.08.0061571-0661/© 2020作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。96A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95语言作为编写简洁和优雅程序的一种手段。它代表了通过案例来定义函数的可能性，分析它们的参数的形状，同时提供了一个语法工具来在应用函数时将这些参数分解为它们的部分。在标准λ-演算中，函数由形式为λx.t的表达式表示，其中x是形式参数，t是函数体。这样的函数可以应用于任何项，而不管其形式如何，如由β归约规则所规定的：t）u<$→β{x\u}t，其中re{x\u}t表示用u替换t中所有x的自由出现的结果。注意，对u的形状没有要求。相反，模式演算提供了β归约规则的推广，其中抽象λx.t被更一般的术语如λp.t所取代，其中p被称为模式。例如，考虑函数λ<$x，y<$.x，它投射了一对中的第一个分量。这里的模式是一对，表达式（λ的形式时才能归约。否则，减少将被阻止。我们对纯模式演算（PPC）[15]及其在模式演算领域引入的新特性特别感兴趣，即路径多态性和模式多态性。前者指的是定义统一遍历任意数据结构的函数的可能性开发这样的演算意味着要在无类型框架中保证良好的操作语义，需要面对许多技术挑战最近，一个静态类型系统被引入到PPC的一个限制中，称为应用模式演算（CAP）[28]，它能够捕获PPC的路径多态性。此外，也研究了这种形式主义的类型检查算法[10]，作为实现捕获这些特征的类型化函数式编程语言根据这一研究路线，也进行了关于PPC标准化策略定义的研究[3，4]。这样的结果通过一个简单的嵌入移植到CAP[27]，其中静态类型规则进一步保证了术语的良好语义。在此框架内，目前的工作旨在抛砖引玉，这些形式主义的实施方面。特别是，模α转换[2]意味着在实现过程中处理变量重命名。已知这种方法容易出错并且计算昂贵。在λ-演算设置中解决这个问题的一种方法是采用de Bruijn符号[8，9]，这是一种简单地避免模α转换的技术。据我们所知，没有像PPC这样的动态模式结石，de Bruijn指数已经在文献中正式化。然而，有一些参考资料值得一提。在[24]中，在高阶模式重写系统（HRS）[22，20]的框架中给出了PPC的另一种表示，以及两个系统之间的转换。另一方面，在[5]中，de Bruijn的思想已经扩展到表达式归约系统（ERS）[11]，还提供了从名称系统到索引系统的形式化翻译，A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）9597反之亦然。此外，HRS和ERS之间的对应关系已经建立[25]。这种翻译的组合可能会得到一个更高阶的系统`aladeBruijn捕获PPC的功能。然而，这将导致一个相当间接的解决方案，我们的问题，许多技术细节仍然需要整理出来。我们的目标是形式化PPC的一个直观的变体与de Bruijn指数，其中已知的原始演算的结果，如存在的归一化策略，可以很容易地移植和重用。1.1贡献本文扩展了de Bruijn这些想法是通过引入一种新的PPC表示来说明的，没有变量/匹配的名称，称为PPCdB。此外，新提出的演算中的绑定器能够处理两种索引，即可变索引和可匹配索引，这是PPC操作语义所要求的。正确的翻译从PPC到PPC分贝和回来。这个函数保留了匹配操作，因此也保留了两个演算的操作语义。此外，它们是彼此的逆。这导致了两个演算之间至关重要的强互模拟结果，这允许将PPC的许多已知属性导入PPCdB，例如连续性和归一化策略的存在。1.2本文结构本文首先简要介绍了PPC的概念，并回顾了第二章中λ-演算的de Bruijn指标的作用机制。二、新的PPCdB是正式的第二节。3，其次是在第二节的翻译介绍。四、强互模拟结果在第2节中给出。5，并讨论了PPCdB的不同特性，由此得出结论。6并讨论今后工作的可能方向。一些技术细节和证据被归入在线提供的扩展报告[19]。2预赛本节介绍了指导我们开发的初步概念，并将帮助读者理解本工作中提出的新思想2.1纯模式演算我们首先简要介绍纯模式演算（PPC）[15]，这是λ演算的扩展，几乎可以抽象任何术语。 这给了地方到两种多功能的多态形式，为未来的函数式编程语言添加新功能奠定了基础：即路径多态和模式多态。然而，这项工作的重点是与执行有关的问题，98A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95^^图案xy和身体中的V的形状是相同的。我...X.（^^^PPC的各个方面，并不会深入研究这些新形式的多态性。我们建议读者参考[15，13]，以便对它们进行深入研究给定一个无限可数的符号集V（x，y，z，.. . ），项TPPC的集合和上下文由以下语法给出Q|C t |t C |λ θC.t |λ θ t。CTermst：：=x|X^|t t|λθt.tCo n textsC：：=其中θ是由抽象约束的符号列表出现在术语中的符号x被称为可变符号，而x被称为可匹配符号。特别地，给定λθ p.t，θ绑定主体t中的可变符号和模式p中的可匹配符号。因此，项t的自由变量和自由匹配项的集合，分别写为fv（t）和fm（t），归纳定义为：fv（x）{x}∅fm（x） ∅fm（x^）fv（x）fv（t u）fv（t）fv（u）fv（λθ p.t）fv（p）（fv（t）\θ）fm（t u）fm（t）fm（u）fm（λθ p.t）（fm（p）\θ）fm（t）如果一个项没有自由变量，则称之为闭项。请注意，自由匹配项是允许的，应该理解为数据结构的常量或构造函数抽象λθ p.t的模式p是线性的，如果每个符号x∈θ在p中至多出现一次。为了说明变量和可匹配对象是如何绑定的，函数elim定义为λ[x]x^。（λ[y]xy^. y）。内[x]^[y]xy^. 年）的抽象将可匹配的y的唯一出现绑定在永远，x在x y中的出现不受内部抽象的约束，因为它被排除在[y]之外，在该模式中充当占位符。它是绑定内部模式中的x和最外层模式中的x的最外层抽象。这在上面用图形描述。本 文 提 出 了 一 个 置 换 （ σ ， ρ ， . . . ） 是 从 变 量 到 项 的 部 分 函 数 。 置 换σ={xi\ui}i∈I，其中I是一组指数，对于每个i∈I，将变量xi映射到项ui（即σ（xi）ui）。因此，它的域和图像被定义为当dom（σ）{xi}i∈I和img（σ）{ui}i∈I时，为了方便起见，通常通过对每个x∈/dom（σ）定义σ（x）x来将置换σ转化为全函数。然后，将id替换表示为{}或简单地表示为id。匹配（μ，ν，. . ）可能成功（产生替换），也可能失败（返回特殊符号fail）或未确定（由特殊符号wait表示）。成功和失败的情况被称为决定比赛。所有与替换相关的概念和符号都被扩展到匹配，例如，失败的域是空的，而等待的域是未{x}λA. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）9599定义的。 σ的自由变量和自由匹配符号的集合被定义为fv（σx）的并集100A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95∈^^您的位置：^^您的位置：^ ^您的位置：^ ^您的位置：^^ ^^^^ ^ ^您的位置：如果x∈dom（μ）和fm（σx），而fv（fail）=fm（fail）= σ x，它们是等待的定义。置换的符号集定义为sym（σ）dom（σ）<$f v （σ）<$fm（σ）。 谓词x避免了σ，说明x∈/sym（σ）。正如预期的那样，它被扩展到集合和匹配。特别地，θ避开μ意味着μ必须被决定。将替换σ应用于项t的结果，记为σt，归纳地定义为：σxσ（x）Xσ（t u）σt σuσλθ p.tλθ σp.σt如果θ避免σσx在抽象的情况下，需要限制以避免不期望的变量/匹配的捕获。然而，它总是可以通过诉诸α转换来满足。将匹配μ应用于项t（表示为μ t）的结果定义为：（i）如果μ=σ a替代，则μtσt;（ii）如果μ=fail，则μtλ[x]x.x（即恒等函数）;或者（iii）如果μ=wait，则μt是unfined。^置换的组合σσJ通常定义为，即， （σ<$σJ）xσ（σJx），并且通过定义如果两个匹配中的任何一个失败，则μ <$μ j失败，将该概念扩展到匹配。否则，如果两者中至少有一个是wait，则μ_J_wait。具体来说，fail = wait = fail。匹配的不相交并集μμJ定义如下：（i）如果μ=fail或μJ= fail，则μ μJ失败;否则（ii）如果μ= wait或μJ= wait，则μ μJwait;否则（iii）μ和μJ都是替换，并且如果dom（μ）不满足dom（μJ）=/否则，nμμJ失败，否则：（μμJ）xμJxifxdom（μJ）⎪⎩xotherwise不相交并用于保证匹配操作是确定性的。在引入匹配操作之前，有必要激发可匹配形式的概念。模式xy首先允许分解任意的应用程序，这可能会导致连续性的损失例如：（λ[x，y]xy.y）（（λ[w]w.z0z1）z0）→（λ[x，y]xy.y）（z0z1）→z1（λ[x，y]x y.y）（（λ[w]w.z0z1）z0）→z0当允许将模式x y与仍然可以被缩减的应用程序匹配时，就会出现这个问题，例如上面示例中最外面的redex的参数（λ[w]w.z0z1）z0为了避免这种情况，只有当参数被成功地计算时，才需要决定匹配如果模式是可约的，则会发生类似的问题。因此，模式和参数都必须是可匹配的形式，才能决定匹配数据结构集DPPC和可匹配的形式A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95101^{{{x^\θx^}}}{}如果x∈/θ^^^ ^您的位置：^^ ^^^^ ^您的位置：^^MPPC由以下语法给出：数据结构d：：= x |dt可匹配的形式m：：= d|λ θ t.t模式p与项u相对于符号列表θ的匹配运算{{{p\θu}}}被定义为以下等式的应用：{{{x^\θu}}}{x\u}如果x∈θ{{{pq\θt u}}}{{{p\θt}{}{}{q\θu}}}如果t u，pq∈MPPC{{{p\θu}}}如果u，p ∈ MPPC，则失败{{{p\θu}}} 否则等待附加的检查被强加，即dom（{{{p\θu}}}）=θ。否则，{{{p\θ u}}}失败。最后一个条件是必要的，以防止绑定符号在减少时超出范围。然而，通过对每个抽象λθ p.t请求θ=fm（p），可以很容易地保证这一点例如，考虑项（λ[x，y]x.y）u。如果没有这个最终检查，将参数u与模式x匹配将产生一个替换{x\u}，并且在抽象体中没有项被分配给变量y最后，PPC的归约关系→PPC由重写规则的上下文闭包给出（λθp.s）u<$→PPC{{{p\θu}}}s当{{{p\θu}}}是一个决定匹配。为了说明PPC的操作语义，考虑上面引入的术语elim，应用于函数λ[z]z.czn，其中自由匹配项c和n可以分别被视为列表cons和nil的构造函数（λ[x]x. （λ[y]x y.y））（λ[z]z.cz n）→PPCλ[y]（λ[z]z.cz n）y.y→PPCλ[y]c y n.y在第一步中，λ[z]z.cz n代替x进入模式xy。在第二步中，缩减驻留在模式中的结果应用程序。结果项，当应用到一个参数，将产生一个成功的匹配，只有当这个参数是一个复合数据的形式ct n。基于上面介绍的匹配操作，该关系被示出为连续的定理2.1（[15]）约化关系→PPC是连续的（CR）。2.2de Bruijn指数接下来我们引入了λ-演算的de Bruijn指标。在文献中的de Bruijn指数的许多陈述中，我们将遵循[17]作为我们的102A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95⎧⎪⎨Kk+1K↑。发展建立在他们的想法之上。特别地，我们选择使用这样的表示，其中索引在替换操作遍历术语时被部分更新（详细信息如下）。我们建议读者参考[17]，以获得等效版本，其中在替换过程结束时执行一次更新。现在我们介绍具有de Bruijn指标（简称λdBTλdB项集 和上下文由以下语法给出：项t：：= i|TT |λt上下文C：：= Q|Ct|tC|λC其中i∈N≥1称为指数。索引是指示到绑定抽象的距离的占位符。在λ dB演算的上下文中，指数也被称为变量。因此，一个项的四个变量可以归纳地定义为：fv （i）{i};fv（t u）fv（t）fv（u）;和fv（λt）fv（t）−1，其中X−k表示从集合X的每个元素中减去k，去除那些导致非正索引的元素。为了定义β-归约aladeBruijn，必须定义用下标i替换项t中的项u因此，有必要在项t的索引中识别对应于i的索引。此外，u的索引应该被更新，以便在用u替换变量之后保持正确的绑定。为此，项t中变量在深度k处的增量，写作↑k（t），归纳定义如下：(i) i+1 ，如果i>ki如果i≤k↑k（t u）↑k（t）↑k（u）↑（λt）λ↑（t）然后，项t中项u在i级的替换（表示为{i\u}t）被定义为将i级的自由变量映射到项的部分函数，当它遍历被替换的项时执行适当的更新，以避免不期望的捕获。{i\u} iJiJ−1ifiJ>iuifiJ=i⎪⎩iJifiJi{i\u}（t s）{i\u}t{i\u}s{i\u}λtλ{i+1\↑0（u）}t值得注意的是，这种替代应在以下情况下解释：一个redex，其中一个粘合剂被删除，并取代其绑定索引。 这迫使 更新自由索引，这可能由最外层的抽象捕获，如在变量i j上的替换的第一种情况所做的那样。因此，保持正确的绑定。最后，λdB-演算的归约关系→dB由重写规则的上下文闭包给出（λs）u<$dB{1\u}s此外，λ演算和λdB之间的嵌入定义为：A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95103Q（2）^^^和：TλdB→Tλ，以这种方式，它们是彼此的逆，并且它们允许将一个微积分模拟为另一定理2.2（[17]）设t∈Tλ，s∈TλdB. 然后，(i) 如果t→βtJ，则t→dBtJ。(ii) 若s→ dBSJ，则nQs→βQsj。这表明两种形式（λ-演算和λdB）具有完全相同的操作语义。作为说明λdB-演算中的约化及其与λ-演算的等价性的例子，考虑以下项：（λz.λy.z）（λx.x）（λ x.x x）和（λλ2）（λ1）（λ1 1）。读者可以验证两个表达式在其各自的演算中编码相同的函数。正如所料，它们的操作语义一致（λz.λy.z）（λ x.x）（λx.x x）→β（λy.λx.x）（λx.x x）→βλx.x（λλ2）（λ1）（λ11）→dB（λλ1）（λ11）→dBλ13具有de Bruijn指标的纯模式演算本节介绍新的具有de Bruijn指数（PPCdB）的纯模式演算。它代表了de Bruijn思想的自然延伸，使其成为一个框架，在这个框架中，一个活页夹可以捕获多个符号。在PPC的特定情况下，有两种捕获的符号，即变量和匹配。这种区别在PPCdB中被保留，同时将索引扩展到对（a.k.a. 二维索引）来区分捕获符号的绑定器和由同一绑定器捕获的所有符号中的单个符号。术语TPPCdB、上下文、数据结构DPPCdB和可匹配形式的集合PPCdB的MPPCdB由以下语法给出项t：：= i j|I j|TT |λ n t.t上下文C：：= Q|Ct|tC|λ nC.t|λ n t. C数据结构d：：=i j|DT可匹配的形式m：：= d |λ n t.t其中i j被称为二维索引，并且表示N≥1×N≥1中的具有主索引i和次索引j的有序对。抽象中的子索引n ∈ N表示它所捕获的索引（对）的数量。一个对的主索引用于确定该对是否被抽象绑定，而次索引用于在这些（可能很多）绑定的对中标识该对。对于PPC，ij形式的索引被称为可变索引，而ij被称为可匹配索引。一个项的自由变量和自由匹配项由此被定义104A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95^^^ ^您的位置：^^^您的位置：^^您的位置：^ ^您的位置：J如下所示：fv（ij）{ij}fv（ij）fv（t u）fv（t）fv（u）fm（ij）fm（ij）{ij}fm（t u）fm（t）fm（u）fv（λn p.t）fv（p）<$（fv（t）−1）fm（λn p.t）（fm（p）−1）<$fm（t）其中X-k表示从集合X的每个元素的主索引中减去k，删除那些导致非正索引的元素让 美国 说明这些概念 与 类似的考试-类似于PPC给出的，即函数elim =λ[x]x。（λ[y]x y.y）。PPC dB框架中的等效项为λ1^11。（λ111^11。11）。注意，λ1^11。（λ111^11。（1）模式的上下文不受相应抽象的约束，同样，抽象主体中的可匹配索引也不被捕获。因此，在本发明中，11的第一次出现实际上与可匹配索引11的第一次出现一起被最外层抽象绑定。项中的其余指数受右图所示的内部抽象的约束作为另一个（更有趣的）示例，考虑来自PPC的项λ[x，y]x y.λ[]x.y，其对应部分在PPCdB中看起来像λ21 1 1 2.λ01 1。2个2. 该示例说明了使用二级索引来标识由相同抽象约束的符号。它还展示了变量的主索引在内部抽象的主体中出现时是如何增加的，而对于出现的情况则不是这样在图案位置中。因此，11和22都被最外层的抽象所约束，11和12也是如此。注意内部抽象根本不绑定任何索引。一个项t被称为良构的，如果t的所有自由二维索引（变量和匹配项）的第二索引都等于1，并且对于每个子项形式为λ n p.s（写作λ n p.s <$t），所有被抽象捕获的对的二级索引都在[1，n]范围内。 例如，{ij|ij∈fm（t）<$f v（t）， j>1}<$（λnp.s<$t{1j|1j∈fm（p）<$f v（s）， j>n}）=0.在引入PPCdB替代的适当概念之前，以具有在术语内的某个深度处更新索引的机制。对于项t中的可变索引和可匹配索引，在深度k处的增量分别写为↑k（t）和k（t），归纳定义如下↑（i）.（i+1）j ifi > kJ（ij）ij凯杰KJJ如果i≤k.（^i+1）jifi > k↑（^i）^ik（^ij）^i如果i≤k↑k（t u）↑k（t）↑k（u）↑k（λn p.t）λ n↑k（p）。↑k+1（t）A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95105k（t u）k（t）λn p.tλ n∈k+1（p）. k（t）106A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95^JJKIJJ如果iJ=/iJJJ j∈J{{{^1j\nu}}}{ 1j\u}类似地，变量（↓k（））和匹配项（mixtables（））在深度k的递减量通过从项中k大多数情况下，这些函数都是在k= 0的情况下使用的，因此，当从上下文中清楚时，子索引将被省略。特别是，变量的递减函数将使我们能够概括第i级的替换思想，而不是第2节中提出的原始替换思想。2.2，这只在β-约简的上下文中成立，通过在约简的时刻对索引进行必要的调整，而不是将它们硬编码到替换元操作中。第i层的替换是从变量索引到项的部分函数。它将第i层的自由变量索引映射到术语，在遍历替代术语时执行适当的更新，以避免不必要的捕获。{i\u}IJ .uk如果iJ=i，k∈JK{i\u}（ts）{i{\fn黑体\fs19\bord1\shad1\1cHD8AFAF\4cHC08000\b0}t{i\u}s{ij\uj}j∈Ji^Jki^Jk{ij\uj}j∈Jλnp.tλn{ij\（uj）}j∈Jp. {（i+1）j\↑（uj）}j∈J值得注意的是，如果iJ= i且k∈/J，则变量索引的基本情况是未定义的。 这种情况将使替换的结果不被发现。 在PPC dB的操作语义中，下面给出的匹配操作将负责避免这种不期 望 的情 况 ， 如 我 们 稍后将 看 到 的 。 在水平i处的替换的 域 是 gi venbyydom（{ij\uj}j∈J）{ij}j∈J。 替代（即，具有空域）被表示为{}或id。如在PPC中，匹配（μ，ν，. . ）可能成功，失败（失败）或未确定（等待）。对于PPCdB，成功的匹配将产生级别1的替换，如以下匹配操作所示，其中规则按PPC中的顺序应用：{{{i^+1j\ij}n{{{pq\nt u}}}{{{p\nt}{}{}{q\nu}}}ift u，pq∈MPPC{{{p\nu}}}如果u，p ∈ MPPC，则失败{{{p\nu}}}否则等待其中匹配的不相交并集以直接的方式从PPC适应PPCdBPPCdB匹配操作中的前两条规则值得一提。由于匹配操作应该在redex的上下文中理解，因此模式中绑定的可匹配符号是主索引等于1.因此，PPCdB对应PPC匹配操作中的隶属度检查x∈ θ，是一种简单的一级索引综合策略。类似地，x∈/θ对应于主指数大于1，正如定义的第二条规则所检查的那样。 然而，模式中的主索引i^+1应该与参数中的主索引i匹配，因为前者是由redex中的额DBDBj∈Jj∈JJj∈JJA. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95107外绑定器所连接的。 例如，在项（λ1^21^11. 11）（111tJ）矩阵121是108A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95^ ^您的位置：^因此，{{{2 1\1t}}}={1\t}。1111^ ^您的位置：^^^^^^^^^^^^^^^^^^^^ ^ ^您的位置：^自由并且对应于参数中的11，而来自模式的11被抽象绑定。 它在PPC中的对应部分将是α等价于（λ[x]yx.x）（y t）。至于PPC，在{{{p\nu}}}上检查一个附加的后置条件，以防止索引超出范围。它需要dom（{{{p\nu}}}）={11，.，1n}，这实质上意味着所有的约束索引都通过所得到的替换被赋予一个值可以通过请求{11，.，1n}fm（p），对于良构项内的每个抽象λn p.t 为了说明这种检查的需要，考虑项（λ21 1. 12）uJ（即， PPCdB对应于（λ[x，y]x.y）u，见第2节。2.1）。如果匹配{{{1 1\2uJ}}}={1 1\uJ}被认为是正确的，则不设置对抽象体中的变量索引1 2的替换，从而导致行为不良的操作语义。PPCdB的减少关系→dB由重写规则的上下文闭包给出（λnp.s）u<$→dB↓（{{{p\n↑（u）}}}s）无论何时，，，{{{p\n↑（u）}}}都是决定性的匹配。可变索引的递减函数应用于约简以补偿s上的绑定器的损失。然而，u的可变指数不受redex中的这种粘合剂的影响。因此，需要在（最终）替换之前递增它们按照上面给出的PPC的简化示例，考虑elim=λ[x]x的这些编码。（λ[y]x y.y）和λ[z]z.cz n分别为：λ111。（λ11 1 1 1。11）和λ111。111121. 请注意，第一次出现的11实际上是由最外层的抽象绑定的，因为抽象在其模式中不绑定可变索引。类似地，λ 111的主体中的可匹配索引11。111121和21一样是自由的。然后，正如预期的那样，我们有以下序列：（λ111. （λ111 11。11 ））（λ111. 111 21）→dBλ1（λ111.211131） 11. 11→dBλ12 1 1 1 3 1。11第一步，λ11 1。111121被替换为图案1111中的11。替 换 发生在模式的上下文中的事实强制应用xl（），从而更新可匹配的索引并获得λ11 1。2 11 13 1. 请注意，归约规则所添加的增量和减量不起作用，因为项中没有自由变量索引。 在第二步中，结果的应用被简化，让位于一个项，其对应部分在PPC中将等价于λ[y]c y n.y（参见图1）。减少的例子在SEC。2.1）。在下面的章节中，PPCdB被证明在表达能力和操作语义方面等同于PPC这种新表示的主要优点是它摆脱了α转换，因为自由和绑定变量/匹配之间不可能发生冲突。然而，对于标准λ-演算使用de Bruijn指标有一个小缺点。如上所述，当在标准λ-演算中使用de Bruijn指标时，α-等价就变成了语法上的等价。不幸的是，当使用二维索引时，情况并非如此为A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95109^^^^VVV（Ⅲ）（Ⅲ）J J（三）（分）米 <$t）M<$u）MVVθVVVV例如，考虑项λ21 1 2。1 1和λ21 2 1 1。12.两者都表示分解应用程序并投影其第一个组件的功能。但它们在二级索引的分配方式此外，人们可能会试图对模式内分配次级索引的方式强加一个顺序，以避免这种情况（回想一下，匹配操作的后置条件强制所有绑定符号出现在模式中）。 考虑到PPC框架中模式的动态性质，这种强制执行不会解决问题，因为模式可能会减少，并且这样的顺序在减少下不是封闭的。例如，考虑λ2（λ21 1 1 2. 1 2 1 1）（1 1 1 2）. 1 1→dBλ21 21 1。11.幸运的是，从实现的角度来看，这并不代表问题，因为二义性是绑定器的局部问题需要因此，当在PPCdB项上进行相等时，我们使用的不是语法上的相等，而是对次级索引的这些分配取模的相等。4翻译本节介绍PPC和PPCdB之间的转换（来回）。我们的目标是表明，这些解释是适合模拟一个微积分到其他。此外，所提出的平移结果是彼此的逆（模α转换），正如我们将在第2节中看到的那样。5，它们允许正式化两个演算之间的强互模拟。我们从PPC到PPCdB的转换开始。它需要将术语与两个符号列表一起翻译，这两个符号列表分别规定了术语的变量和匹配项应如何我们使用列表的列表，因为第一维表示到绑定器的距离，而第二维标识多个绑定器中的符号。给定列表X和Y的列表，我们用XY表示它们的连接。为了提高可读性，当上下文很清楚时，我们也写θX，其中θ是一个符号列表来表示[θ]X，其中[ ]表示列表构造函数。我们使用集合运算，如列表上的并集和交集，来表示其底层集合的并集/交集。定义4.1给定项t∈TPPC和符号V和M的列表列表，使得f v（t）≠V′∈VV和fm（t）≠M′∈MM，与V有关的变换而M，写作tM，归纳定义如下：XM其中i=min{iJ|x∈Vi′}和j=min{jJ|x=Vi j′}XM其中i = min {iJ|x ∈ M i′}和j = min {jJ|x = M ij′}λ θ p.t）Mλ|θ| <$p）θM。（t）M110A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95X<$^）<$）^^^ （Ⅲ）[[y]，[z]]（^）KJVV（Ⅲ）0[[y]][[y]][[y]][[y]][[x]，[y]]0[[y]]提供θ。则It被定义为as<$σ，θ）M{1j\<$σxj）M}x∈dom（σ）。注意howY'∈YYJ）（(i) 若{{{p\θu}}=σ，则<${{{p\θu}}}）M=<$σ，θ）M。在匹配的情况下，其平移由下式给出：<${{{p\θ u}}}）M{{{<$p}θM\|θ|<$u）M}}}。（二）tX1... X n = i−1X1... XkXk + i...XnVVJYXYXJYθXVVVVV设x1，x2，. 是一个V的枚举。然后，将t转换为PPCdB，简单地说，是分t），被定义为分t）X 其中X = [[x1]，...，[xn]]使得fv（t）<$fm（t）<${x1，.， x n}。例如，考虑项s0=（λ[x]yx.x）（ysJ0），其中hfv（sJ0） ={y}，并且fm（sJ）={y}.然后，<$s0）[[y]]0[[y]]=（λ1<$y^）[[x]，[y]]<$^x^^）[[x]，[y^]]。<$x）[[y]]）（y[[y]] SJ[[y]]）=（λ12 1 1 1。11）（11sJ[[y]]）。注意，V和M的单例初始化元素意味着术语中的每个自由变量/匹配项将被分配一个不同的主索引（当在相同深度解释时），遵循de Bruijn的原始想法：让s 1 =（λ [ x ] y x.x）（y z），则s1 [[ y ]，[ z ]] =（λ 1 2 1 1 1. 11）（11 21）.我们的主要目标是证明PPCdB通过这种嵌入来模拟PPC为了这个目的，我们需要首先陈述一些辅助引理来证明平移对于替换和匹配操作的我们从一个关于可变和匹配指数的增量函数的技术结果开始。记法↑n（t）表示在t上连续应用n次↑（）（类似地K K对于n（t））。引理4.2设t∈TPPC，k≥0，i≥ 1且n≥k+i，使得Xl∈（fv（t）<$fm（t））=对于所有l ∈ [k +1，k + i − 1]，然后，i−1(i) t M= ↑（<$t）M）。（1）X1... XnkX1. Xk Xk+i... XnVk（t）V）。置换σ的平移需要枚举θ，使得dom（σ）来自PPC的替换被映射到PPCdB帧中的级别1处的替换工作这是因为替换只意味着在redex的上下文中创建。当在任意深度作用于一个术语时，替换被证明是正确的。引理4.3设s∈TPPC，σ是置换，θ是枚举，使得dom（σ）<$θ和Yb∈i−1个符号表使得（Y′∈YY）<$θ=<$（则，<$σs）M =↓（{ij\↑（<$σxj）M）}x∈dom（σ）<$s）M）的。请注意θ是如何被推入模式的可匹配符号列表中的，抽象的翻译。这对于保持匹配输出的后续结果至关重要。引理4.4设p，u∈ TPPC.(ii) 如果{{p\θu}}}=失败，则{{{p\θu}}}M =失败。(iii) 如果{{{p\θ u}}}=等待，则<${{{p\θ u}}}）M =等待。xj ∈θ fv（σxj））= θ fv（σ xi−1i−1A. Martín et al. /Electronic Notes in Theoretical Computer Science 351（2020）95111（Ⅲ）VQi、VjijQ^iMjijXQ <$Q <$^^^Q t（Ⅲ）QQtuM Qt<$MQu<$MQVVθVVVJi−1JYXYXJYθXVVV（二）X1... XkXk + i...Xn这些先前的结果将允许通过转换证明PPC到PPCdB的模拟。我们把这个结果推迟到SEC。5（cf. Thm. 5.1）。现在我们关注嵌入的相反方面，即PPCdB项转换为PPC项。如前所述，这种映射需要两个符号列表，从这些符号列表中将选择项的自由索引的名称：一个用于可变索引，另一个用于可匹配索引。定义4.5给定项t∈TPPCdB和不同符号V的列表和M，使得对每个ij∈fv（t）定义Vij，对每个ij∈fm（t）定义Mij，则设 Qt<$M，t与V和M的关系的变换是归纳的定义如下：MVMVQλnp.t<$MλθQp<$θM。Qt<$Mθ=[x1， . ，xn]新鲜的样品设x1，x2，. V是相同的枚举在def中。 4.1. 然后，将t转换为PPC，简称为t，定义为tX，其中X = [[x1]，...，[x n]]使得fv（t）=fm（t）={11，.，n1}。注意，术语的格式良好性保证X满足上述条件。为了说明平移，考虑项t1=（λ12 11 1. 11）（1121）其中fv（t1）={21}和fm（t1）={11}。然后，[[y]，[z]]1=（λQ^21^11<$[[x]，[y]，[z]].Q11<$[[y]，[z]]）Q^1121<$[[y]，[z]] =（λy^x^.x）（y^z）。注意从定义4.1之后的例子中得出t1=s1，并且通过对列表V和M进行适当的初始化，我们得到t1=s1。再次，我们从一些关于嵌入的替换和匹配操作的技术引理开始。在这种情况下，变量和可匹配索引的增量函数的行为如下：引理4.6设t∈TPPCdB，k≥0，i≥ 1且n≥k+i，使得fv（t）≠fm（t）≠{iJj|iJ≤n−（i−1）， j≤|Xi′|}中。你好，（一）↑i−1分M⇑i−1= αQt<$M。QK（t）X1. XnX1. Xk Xk+i... XnQk（t）<$V= αQt<$V。反之，翻译仅定义为第1级的替换，并要求提供一个系统对象列表，|θ|≥max{j|1j∈dom（σ）}。那么，Qσ，θM {θj\Qσ1j<$M}1∈dom（σ）. 一个替换在一个示出任意级别i适当地平移。引理4.7设s ∈ TPPCdB，σ是在级别i的替换，θ是新鲜符号的列表，使得|θ|≥ max {j |ij∈ dom（σ）}和Y是i-1个符号列表的列表。然后，Q↓