Lambda演算的α-结构归纳与递归

可在www.sciencedirect.com在线获取理论计算机科学电子笔记323（2016）109-124www.elsevier.com/locate/entcs构造型理论中Lambda演算的α-结构归纳与递归Ernesto Copello1 Álvaro Tasistro2乌拉圭蒙得维的亚大学Ana Bove4瑞典哥德堡查尔姆斯理工大学MaribelFernández英国伦敦国王摘要我们在lambda演算的原始语法（即，只有一种名称），其中α转换基于名称交换，如在名义抽象语法中一样。这些原则允许进行模α转换并实现Barendregt变量约定。我们从简单的结构归纳法原理出发，在具体条件下推导出了它们，并给出了应用一些基本的元理论结果，如α-转换的置换引理和置换复合引理。整个工作在阿格达进行保留字：形式元理论，λ演算，构造类型理论1引言我们感兴趣的方法，形式化的建设性类型理论的Meta理论的主要原因是lambda演算是1电子邮件地址：copello@ort.edu.uy2 电子邮件地址：tasistro@ort.edu.uy3电子邮件：szasz@ort.edu.uy4电子邮件：bove@chalmers.se5 电子邮件：Maribel. kcl.ac.ukhttp://dx.doi.org/10.1016/j.entcs.2016.06.0081571-0661/© 2016作者。出版社：Elsevier B.V.这是CC BY许可下的开放获取文章（http://creativecommons.org/licenses/by/4.0/）。110E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109它既是一种友好的编程语言，也是一个主要的测试平台，用于对具有（名称）绑定功能的树结构进行形式化特别是关于后者，非正式程序包括从“识别直到α转换的术语”开始然而，当函数由递归定义和性质由归纳证明时，这并不简单这个问题与这样一个事实有关，即对α等价类的考虑实际上是这些是由所谓的Barendregt变量约定（BVC）选择的：代表其α类的每个术语现在，一个一般的有效性准则决定了，这个过程在所有情况下都应该伴随着验证，即函数的证明和结果只依赖于α类，而不随所讨论的代表的特定选择而变化。这种验证很少完成，但它不是关于结构有效性的主要困难如此执行。关键的一点是，例如，归纳证明经常使用具体项的结构原理来进行-然后很可能发生的是，对应于功能抽象的归纳步骤可以对方便选择的绑定名称进行，而不是对原则要求的任意名称进行。这个问题可以通过使用de Bruijn的无名语法来避免它的最新版本本地无名语法[2，3]，它使用自由或全局变量的名称和索引计数到绑定抽象器，局部参数的出现。 但这些方法并非没有开销以几个操作或格式良好的谓词的形式。因此，不必考虑α-转换当然是一种解脱;但是，与此同时，无名的句法严重地影响了实际形式过程与可以被认为是句法的自然特征之间的联系。 同样的， ”[9]中所述的地图表示一个不同的选择是用直接作用于α-等价类的所谓的α-结构原理这意味着提供允许通过归纳证明性质的原则，并通过直接使用BVC递归定义函数，以减轻与验证程序有效性相关的负担在这个方向上的第一次尝试是[6]，它给出了lambda术语的公理化描述，其中等式体现了α转换，并提供了一种方法函数的定义是通过对这类对象的递归来实现的。这项工作最终取决于使用高阶抽象语法的HOL系统内，和一个理论模型使用de Bruijn的无名语法勾勒出的公理系统的可靠性。在文献[5，12，13]中，引入了带绑定器的语法模型，这些模型基于名称交换的简单操作，阐述了抽象、α-等价和数学对象中的名称是“足够新鲜”的基本概念。这个理论--被称为名义抽象语法--提供了一个（一阶）语言的框架，E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109111PPPPPPPα-结构递归和归纳的原理，这些原理基于对当前上下文中的数学对象的不依赖性的验证，以及递归定义中使用的阶跃函数的结果，对所涉及的α-类的代表所选择的绑定名称的验证。这种方法的实现已经在Isabelle/HOL [15]和Coq[1]中尝试过。在第一种情况下，解决方案依赖于高阶抽象语法的弱版本，而第二种情况是公理化，其中-类似于上面引用的[6]-等式被假设为包含α转换，并且已经构建了基于局部无名语法的系统模型。另一种表述α-结构原理的方法源于这样的观察，即如果要尝试的性质是α-相容的，即，它实际上是α类的一个性质，而不仅仅是具体项的性质--那么关于项的大小的（完全）归纳法可以用来弥补上面指出的在归纳法证明中可能存在的差距，归纳法证明局限于方便地选择束缚名。事实上，假设你需要证明 （λx.M）;现在，如果你所拥有的一切 （M）至 （λx<$.M<$）为了方便对该术语进行重命名，那么你就可以在M上使用你的强尺寸归纳假设，因为它的尺寸仍然小于（λx.M）。 因此，由于的α相容性，你将到达（λx<$.M<$），并从那里到达期望的（λx.M）。这促使人们试图提供一种这种机制，以正式使用BVC，这就是我们在本文中所尝试的。 结果是我们能够为了提供阿尔法结构归纳和递归的原则，在构造类型论中实现BVC，只使用普通的一阶、带名字的语法，实际上不使用关于项的大小的强归纳--也就是说，我们能够从关于具体项的简单结构归纳中推导出所讨论的原则为了达到这个目的，我们使用名义抽象语法的基本概念来定义α-等价等式仍然是简单的定义等式，我们也不进行任何类型的商构造。整个开发都在Agda系统中实现[10]。本文的其余部分如下：在第2节中，我们介绍了刚刚提到的基础设施。第三节从项上的简单结构归纳开始，到α类上的递归原理，给出了这些原理。在第4节中，我们展示了几个应用程序，这些应用程序为该方法的有用性带来了一定的感觉。最后，第五部分与相关工作进行了比较，并指出了结论和进一步的工作。本文档实际上是一个文字化的Agda文档，为了简洁起见，我们在其中隐藏了一些代码。完整代码可在以下网址获得https://github.com/ernius/formalmetatheory-nominal并已与Agda最新版本2.4.2.2和0.9标准库一起编译。112E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109→2基础设施2.1AgdaAgda实现了构造类型理论[8]（简称类型理论）。 它实际上是一种函数式编程语言，其中：(i) 归纳类型可以像往常一样引入，即通过枚举它们的构造函数，但它们可以在其他类型的对象中参数化。因为后者，类型论以类型族（由基类型索引）或依赖类型为特征。(ii) 类型族上的函数依赖于基对象，也就是说，它们通常具有（x：α）β x的形式，其中β x是α类型的x的参数化类型。因此，函数输出的类型取决于输入的值。(iii) 归纳类型上的函数由模式匹配方程定义(iv) 语言的每一个功能都必须是终止的。强制实现这种条件的递归的标准形式是结构递归，当然，它是经过语法检查的。(v) 由于上述特征，类型论可以被解释为一种推理逻辑。具体地说，这是通过将命题表示为归纳类型来实现的，归纳类型的构造函数是所讨论的命题的引入规则，即直接证明的方法。因此，我们可以概括地说，数据、谓词和关系的集合是归纳地定义的，即通过枚举它们的构造函数。2.2语法项的集合Λ是通常的。它是由一组可数的名称组成的，我们将把这些名称称为原子，借用名词性抽象语法的术语。dataΛ：Set wherev：原子→Λ_·_：Λ→Λ →Λregon：原子→Λ →Λ以下称为新鲜度关系。当一个变量在一个项中不是自由出现时，它成立。在调用函数时，写在花括号之间的函数参数可以省略。data_#_（a：Atom）： Λ→Set其中#v：{b：Atom}→b/atoma→a#vb#·：{MN：Λ}→a#M→a#N→a#M·N#regon {M：Λ}→a#regona M#regon：{b：Atom}{M：Λ}→a#M→a#regonb M接下来是原子交换的基本操作。有限序列E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109113·∼∼原子交换的（组合）构成（有限）原子排列，其是要在项上使用的重命名机制。原子交换的作用首先定义在原子本身上：（_·_）A_：Atom → Atom → Atom（ab）Ac，其中c=？Aa... | yes _= b... |没有 在C=？AB...| 是_ =a...| 没有 _ =c在这里，它延伸到术语：（_·_）_：原子→原子→Λ →Λ（a· b）v c=v（（ a· b）A c）（a· b） M· N=（（ a· b） M）·（（ a· b） N）（a· b）regon c M=regon（（ a· b）A c）（（ a· b） M）置换也是如此，它是交换的列表_·A_：电子→原子→原子π·Aa=foldr（λs b→（proj1s·proj2s）Ab）a π_·_：→ Λ→Λπ·M=foldr（λs M→（proj1s·proj2s）M）M π现在我们引入α-转换，记为α。在lambda抽象的情况下，我们使用了一个语法导向的定义，它使用了有限量化data_α_：Λ→Λ →Set其中α v ：{a：Atom}→va <$αva∼α·：{M M→M·Nα Mα regon：{M N：Λ}{a b：Atom}（xs：List Atom）→（（c：Atom）→c∈/xs→（a·c）M<$α（b·c）N）→regona Mαregonb N其思想是，为了证明两个抽象的α-等价性，当你将绑定的名字重命名为在两个抽象中都不自由的任何名字时，你应该能够证明各自的实体是α新名称的条件可以推广到“不在给定列表中的任何名称”，从而产生等价关系。后一个条件更难证明，但当你假设α成立时更方便使用，这在即将到来的证明中更常见。3α-结构归纳和递归原理我们从具体Λ项上的简单结构归纳开始：下一个归纳原理为λ ab提供了一个强有力的假设114E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109∀··∀··TermPrimInd：{1：Level}（P：Λ→集合1）→（α →P（va））→（ MN →P M →P N →P（M·N））→（ Mb →P M →P（regonb M））→M →P MFig. 1. 混凝土结构归纳原理straction case：它允许假设抽象体的所有重命名（由名称的有限排列TermIndPerm：{1：Level}（P：Λ→集合1）→（α →P（va））→（ MN →P M →P N →P（M·N））→（πM b→（ππ→P（ π·M））→P（regonb M））→M →P M图二. 强置换归纳原理注意，为抽象的情况提供的假设类似于关于项的大小的强归纳或完全归纳的相应原理，只是用名称排列来表达。这个原理可以从前者，即从简单的结构归纳法中导出，就像从普通的数学归纳法导出自然数的完全归纳法一样。也就是说，我们可以使用结构归纳法来证明（π）P（π M），给出了新原理的假设，P M 由此得出。对于抽象的内部情况，我们必须证明（ππ）P（π·regonaM），它等于（ππ）P（regon（π·Aa）（π· M））.新原理的假设在这种情况下给我们（<$M<$，b）（（<$π<$）P（π<$·M<$）→P（regonbM<$））。现在，将M实例化为π·M，将b实例化为πAA，我们得到所需的结果，如果我们知道（π）P（π πM），其中结构原理的归纳假设我们称一个谓词为α-相容的，如果它被α-转换保留α可预测：{1：水平}→（Λ→集合1）→集合1α可预测P={ M N：Λ}→ M<$α N→ P M→ P N对于α相容谓词，我们可以使用前面的原则导出以下内容：项αPrimInd：{l：Level}（P：Λ→集合l）→α α β PredP→（α →P（va））→（ MN →P M →P N →P（M·N））→λ（λvs→（λMb→b∈/vs→PM→P（regonbM）→M →P M这一新的原理使我们能够通过以下方式来进行抽象情况的证明：E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109115·∼∼⇒→选择与给定列表中的名称不同的绑定名称vs.它提供了一种模仿Barendregt变量约定（BVC）的方法，因为实际上，要避免的名称总是有限的;在使用该原则时，我们必须提供一个包含它们的列表。在[1]中也提供了同样的原理，只是我们在这里根据前面介绍的原理给出了一个证明，而不是仅仅假设它。我们的目的是尽可能地使用这个原理，从而隐藏交换运算的使用，它被限制在前面公开的原理当然，实现该原理的有趣案例是函数抽象。我们必须把自己放在这样一个位置上，在这个位置上，我们正在使用前一个强原理，并被给予一个抽象的regonbM，我们必须证明P。为了达到这个目的，我们必须使用与功能抽象相对应的新原则的子句，它迫使我们使用一个从给定的列表中选出的名称。 因此，我们可以渴望证明P是原项的重命名，说regonbm。然后，所需的结果将从谓词P提供的regonb<$M <$αregonbM的α兼容性得出。这强加了一个条件，即在原始项regon bM-中选择新的名称b，并且M =（bb）M。我们知道PM，因此也知道P（regonb <$M），因为我们知道对M的任何重命名的P，通过我们开始的强原理的假设。在这个实现中非常重要的一点是，给定要避免的名称列表，我们可以并且确实为每一类α等价项确定性地选择b 事实上，如果我们确定b_n为例如给定列表中的第一个名字，它在最初给定的项中是新鲜的（即不是自由的），那么对于每个α类的每个项，结果都是相同的，因为α等价项具有相同的自由变量。因此，对于每个要避免的名称列表，由这种方法选择的每个α类的代表将是固定的，这构成了使用该方法定义α类上的函数这将通过将类（的每个项）与规范选择的代表的相应计算结果相关联来工作更准确地说，让我们说，函数f：ΛA是强α相容的iM αN fM=fN。 我们现在可以定义一个原始项上的迭代原理 它总是产生强α相容函数。 对于抽象的情况，这个原则也允许我们给出一个变量列表，其中抽象变量不被选择。这个迭代原理是直接从BVC归纳原理（术语αPrimInd）导出的，只使用了一个等价于类型A的平凡常数谓词。我们展示了迭代器的类型和代码Λ它 ：{l：Level}（A：Setl）→（原子 →A）→（A →A →A）→列表原子×（原子 →A →A）→Λ →A重复一下这个思想，迭代器作为一个函数作用于α类，因为对于每个给定的抽象，它将产生一个结果，该结果是通过处理一个规范选择的代表而获得的，该代表是由要避免的名称列表和116E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109(free（a）a类的名称。如果我们试图直接用递归原理代替迭代原理，就不会得到强相容性，但是我们可以通过计算其中一个分量是项的对的标准过程来由此我们得到了下一个项上的递归原理，它也产生了强α相容函数。ΛRec ：{l：Level}（A：Setl）→（原子 →A）→（A →A →Λ →Λ →A）→列表原子×（原子 →A →Λ →A）→Λ →A4元理论中的应用我们给出了前一节中定义的迭代/递归原理的几个应用。在下面的两个小节中，我们实现了λ-演算理论的两个经典在附录A中，我们还将迭代/递归原理应用于[11]中提出的项上函数的例子。这项工作提出了一系列增加复杂性的功能，目的是测试递归原则的适用性在λ演算条款。4.1自由变量我们实现了返回一个术语的自由变量的函数。fv：Λ→列表原子fv=ΛIt（ List Atom） [_]_++_（[]，λv r→r-v）作为迭代原理强α相容性的直接结果，我们得到α等价项具有相同的自由变量。当一个变量在一个项中自由出现时，关系_*_成立data_*_：Atom→Λ →Set其中*v： {x：Atom}→x * v x*·l ： {x：原子}{M N：Λ} →x* M→x*（M·N）*·r ： {x：原子}{M N：Λ} →x * N→x *（M·N）*俄勒冈州： {x y：原子}{M：Λ}→x * M→y/x →x*（regony M）我们可以使用我们的BVC类归纳原理来证明以下命题：Pfv*：原子→Λ →集合Pfv*a M= a∈fv M→ a* M在lambda抽象的情况下，我们可以通过选择与a不同的绑定名称来简化证明。这种相容性是有代价的，即我们需要证明谓词Pfv*a是α相容的，以便使用所选择的归纳原理。一旦我们证明*是α相容的，这个αE. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109117→≡→∼关系，并且FV函数是强α相容的。最后一个性质是直接的，因为我们用迭代原理实现了fv，所以额外的成本只是证明*是α兼容的。 反过来，如果我们将建立变量a在项中是自由的关系定义为递归函数，如下所示_free_：原子→Λ →集合（_free_）a=ΛItSet（λb→a<$b）__（[a]，λ_→id）对于变量的情况，我们将搜索到的变量的命题等式返回给术语变量。应用案例是递归调用返回的类型的不相交联合。最后，在抽象的情况下，我们可以选择与搜索变量不同的抽象变量。通过这种方式，我们可以忽略抽象变量，只返回递归调用，其中包含在抽象体中搜索到的变量的任何自由出现的证据。这个实现在构造上是强兼容的，因为我们是根据迭代器原理构建的，所以从这个定义中也可以直接得出α等价项具有相同的自由变量。4.2取代我们通过以下方式实现捕获避免替换hvar：原子→Λ →原子→Λhv arxNy，其中x=？的y... | yes _ = N... | no _ =vy–_[_：=_]：Λ→原子→Λ →ΛM[ a：= N]=ΛItΛ（hvar a N）_·_（ a：：fv N，regon） M它显示出相当接近于假设BVC的简单的纸和纸的版本。请注意，我们明确指出，要选择的规范代表的绑定名称必须与替换变量不同，并且不能在替换项中自由出现再次由于迭代原理的强α-相容性，我们免费得到以下结果：lemmaSubst 1：{M N：Λ}（P：Λ）（a：原子）Mα NM[a：=P]N[a：=P]lemmaSubst1{M}{N}P a=lemmaΛItStrongαCompatibleΛ（hvara P）_·_（a：：fvP）regonM N使用图2中的归纳原理，我们证明：lemmaSubst2：{N} {P}M x→N<$α P →M[x：=N]<$αM[x：=P]118E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109N aPN aQ≈⟨→∼⟩中文（简体）≈⟨→∼⟩从前面的两个结果我们直接得到α-替换引理：lemmaSubst：{M N P Q：Λ}（a：原子）→M<$α N →P<$α Q→M[a：=P]<$αN[a：=Q]lemmaSubst{M}{N}{P}{Q}aMN PQ=开始M[ a：= P]Subst1P aMN【 ：= 】非线性引理Subst2N aPQ【 ：= 】Q反过来，根据前面的结果，我们可以推导出，对于足够新鲜的绑定名称，我们的替换操作与一个朴素的替换操作是αlemmaregon[]：<${abP}M→b∈/a：：fvP→regonb M[a：=P]<$αregonb（M[a：=P]）我们可以将最后一个结果与模仿BVC约定的项αPrimInd原理相结合，并以这种方式模仿关于替换运算的项的α-作为一个例子，我们接下来展示替换合成引理：PSC：N{xyL}N→Λ →集合PSC{x}{y}{L}NM=x/y→x∈/fvL→（M[x：=N]）[y：=L]→α（M[y：=L]）[x：=N[y：=L]]我们首先给出PSC谓词是α相容的一个直接的等式证明α可预测PSC：α可预测PSCα可忽略PSC{x}{y}{L}N{M}{P}M可忽略PPMx/可忽略yx∈/fvL=开始（P[x：=N]）[y：=L]– 强 α相容性 的 内 替换操作cong（λz z[y：=L]）（lemmaSubst1N x（σMP））（M[x：=N]）[y：=L]– 我们 我们知道谓词对M成立PM x y x/fvL（M[y：=L]）[x：=N[y：=L]]– 内替换运算cong（λz z[x：=N[y：=L] ]）（lemmaSubst1Ly（MP））（P[y：=L]）[x：=N[y：=L]]的强αQ对于lambda项上的α-结构归纳的有趣抽象情形，我们假设lambda项中的抽象变量不在替换变量中，或者在替换项中是自由的通过这种方式，E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109119≈⟨∼ ∈⟩∼⟨∼ ∈⟩中文（简体）∼⟨∼ ∈⟩≈⟨∼ ∈⟩成为α-相容于朴素替换的，归纳假设允许我们以直接的方式完成归纳证明。代码片段变为：开始（regonb M[x：=N]）[y：=L]– 内代换是α等价的– 因为b∈/x：：fvNlemmaSubst1L y（lemmaregon[]Mb/x：：fvN）（regonb（M[x：=N]））[y：=L]– 外代换是α等价的– 因为b∈/y：：fvL引理regon[]（M[x：=N]）b/y：：fvLregon b（（M[x：=N]） [y：=L]）– 我们 可以 现在 适用 我们 归纳假说引理α regon（IndHip x y x/fvL）regon b（（M[y：=L]）[x：=N[y：=L] ]）– 外代换是α等价的– 因为b∈/x：：fvN[y：=L]σ（引理regon[]（M[y：=L]）b/x：：fvN[y：=L]）（regonb（M[y：=L]））[x：=N[y：=L]]– 内代换是α等价的– 因为b∈/y：：fvLsym（lemmaSubst1（N[y：=L]）x（lemmaregon[]Mb/y：：fvL））（regonb M[y：=L]）[x：=N[y：=L]]Q值得注意的是，这些结果是直接从第一个原始归纳原理导出的，在所有这些形式化中，不需要对项的长度或可访问的谓词进行归纳。5结论这项工作的主要贡献是在构造类型理论中完全实现了归纳和递归的原则，允许在lambda演算的α类项上工作。关键的组成部分似乎是我们所谓的BVC类归纳原则，允许在抽象的情况下选择绑定名称，使其不属于给定的名称列表。一方面，这个原则（对于α相容谓词）是从具体项上的普通结构归纳导出的，从而避免了任何形式的关于项的大小的归纳或其他更复杂的归纳形式。另一方面，它产生了递归原理，允许在α类上定义函数，特别是对α等价项给出相同结果我们还通过一些例子表明，这些原则提供了一个灵活的框架，能够很好地模仿纸上实践。我们的工作与例如[13]不同，因为我们确实确定了代表的选择，120E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109实现α-结构递归，从而迫使该原理对于α-等价项产生相同的结果。这可能有点太具体了，但另一方面，它给了我们在现有系统上完成一个简单的完整实现的可能性，这与其他基于假设或更复杂的语法系统或实现方法的作品不同。我们希望继续探索这种形式化方法的能力通过研究它在类型系统的元理论中的应用。我们还希望加深其与基于Stoughton替代[ 14 ]的方法的比较引用[1] 布莱恩·艾德米尔，亚伦·博汉南，斯蒂芬妮·韦里奇. Coq中的名词性推理技术电子笔记理论 Comput. Sci. ，174（5）：69-77，June 2007.[2] 放大图片作者：Brian Aydemir，Arthur Charguéraud，Benjamin C.皮尔斯，兰迪·波拉克，斯蒂芬妮·韦里奇. 工程形式元理论。在Proceedings of the 35th Annual ACM SIGPLAN-SIGACT Symposium onPrinciples of Programming Languages，POPL'08，pages 3-15，New York，NY，USA，2008。ACM。[3] 亚瑟·夏格罗当地无名的代表。 J. 自动 Reasoning，49（3）：363 -408，2012.[4] N. G.德布鲁因使用无名虚拟符号的λ演算符号，自动公式处理的工具，及其对丘奇-罗瑟定理的应用Indagationes Mathematicae（Koninglijke Nederlandse Akademie van Wetenschappen），34（5）：381-392，1972. http://www.win.tue.nl/automath/存档/pdf/aut029.pdf电子版。[5] 默多克作者声明：Andrew M. 皮茨一种新的变量绑定抽象查询方法Formal Aspects of Computing，13（3-5）：341-363，2001年7月。[6] Andrew D. Gordon 和 Thomas F.梅 尔 汉 姆 阿 尔 法 转 换 的 五 个 公 理 。 In Joakim von Wright ， JimGrundy ， and John Harrison ， editors ， Theorem Proving in Higher Order Logics ， 9th InternationalConference，TPHOLsSpringer，1996年。[7] 阿尔瓦罗·塔西斯特罗，埃内斯托·科佩洛，诺拉·萨斯。构造类型论中斯托顿替换lambda演算的形式化。Electronic Notes in Theoretical Computer Science，312（0）：215- 230，2015.第九届逻辑和语义框架与应用研讨会（LSFA 2014）。[8] P. Martin-Löf和G.桑宾 直觉主义类型理论。 研究证明理论。1984年的《书苑》[9] Helmut Schwichtenberg Masahiko Sato，Randy Pollack and Takafumi Sakurai，Viewing lambda-termsthroughmaps，2013，Availablefromhttp://homepages.inf.ed.ac.uk/rpollack/export/Maps_SatoPollackSchwichtenbergSakurai.pdf[10] 乌尔夫·诺雷尔一种基于依赖类型理论的实用编程语言。博士论文，计算机科学与工程系，查尔姆斯理工大学，SE-412 96哥德堡，瑞典，2007年9月。[11] 迈克尔·诺里什带有绑定器的类型的递归函数定义在第十七届高阶逻辑定理证明国际会议上，第241[12] Andrew M.皮茨名称逻辑：名称与约束的一阶理论信息与计算，186（2）：165计算机软件的理论方面（TACS 2001）。[13] Andrew M.皮茨阿尔法结构递归和归纳。 J. ACM，53（3）：459 -506，May2006.[14] A.斯托顿重新审视替代品。Theor. Comput. Sci. ，59：317[15] Christian Urban和Christine Tasson。isabelle/hol中的名词性技巧。在Robert Nieuwenhuis，编辑，自动演绎-Springer Berlin Heidelberg，2005.E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109121A迭代/递归应用在下面的章节中，我们成功地将迭代/递归原理应用于[11]中的所有示例这项工作提出了一个函数序列，其定义的复杂性正在增加，以提供对任何函数定义原则的测试，其中每个给定的函数都遵守α-等价关系。A.1案例分析和构造函数参数的下面的函数家族区分了返回构造函数组件的构造函数，在某种意义上给出了一种模式匹配。isV ar：Λ→Maybe（Variable）isV ar（v x）=JustisV ar（M·N）=无isVar（λxM）=无isApp：Λ→Maybe（Λ×Λ）isApp（v x）=NothingisApp（M·N）=Just（M，N）isApp（λxM）=NothingisAbs：Λ→可能（变量×Λ）isAbs（v x）=NothingisAbs（M·N）=NothingisAbs（λxM）=Just（x，M）接下来，我们将相应的编码呈现到我们的迭代/递归原理中。样品：isVar：Λ→MaybeAtomisVar=ΛIt（MaybeAtom）只是（λ__→无）（[]，λ_ _→无）–isApp：Λ→可能（Λ×Λ）isApp=ΛRec（可能（Λ×Λ））（λ_→无）（λ_ _ M N→just（M，N））（[]，λ_→nothing）–isAbs：Λ→Maybe（Atom×Λ）122E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109isAbs=ΛRec（Maybe（Atom×Λ））（λ_→无）（λ__________ →无）（[]，λa _ M→just（a，M））E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109123→→→ → → →→→ → →→A.2简单递归size函数返回一个术语大小的数值度量。尺寸：Λ→ Nsize（v x）=1尺寸（M·N）=尺寸（M）+尺寸（N）+1size（λxM）=size（M）+1尺寸：Λ→Nsize=ΛItN（const1）（λn m→<$n+m）（[]，λ_n→<$n）A.3阿尔法平等这个函数决定了两项之间的α等于：Λ→Λ →布尔equal=ΛIt（Λ→Bool）vareq appeq（[]，abseq）其中vareq：AtomΛ Bool vareqaMwithisVarM... | nothing = false... |b=[a=？ABBappeq：（Λ Bool）（ΛBool）Λ BoolappeqfM fN PwithisAppP... |nothing= false... | just (M’ , N’)= fM M’ ∧ fN N’ abseq:Atom(ΛBool)ΛBoolabseq a fM N with isAbs N... | nothing = false... |只有（b，P）=[a=？AbfMP注意isAbs函数也对N进行了标准化，因此在最后一行询问两个绑定名称是否相同是正确的。A.4引用绑定变量的递归如果一项是η-正规形式，则enf函数对该项为真它调用了fv124E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109函数，它返回一个术语的自由变量的集合E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109125→ →→→→enf：Λ→Boolenf（v x）=Trueenf（M·N）=enf（M）enf（N）+1enf（λxM）=enf（M）<$（<$N，x/isApp（M）==Just（N，v x）<$x∈fv（N））__：Bool→Bool→Boolfalseb=true真 b=b–enf：Λ→布尔enf=ΛRecBool（consttrue）（λb1 b2_ _→b1<$b2）（[]，absenf）其中absenf：Atom BoolΛ Bool absenfa bMwithisAppM... | nothing = b... | just (P , Q) = b ∧ (equal Q (v a) ⇒ a ∈b (fv P))A.5带附加参数的给定在传递项（Lt，Rt，In）时要遵循的可能方向的三元类型，对应于应用构造函数和抽象体的两个子项，返回到项中给定自由变量的出现的路径集合（方向列表）。假设cons在列表前面插入一个元素。vposns：Variable×Λ→List（List Direction）vposns（x，v y）=if（x==y）then[[]]else[]vposns（x，M·N）=map（cons Lt）（vposns x M）++map（consRt）（vposnsxN）x/=yvposns（x，λyM）=map（consIn）（vposnsxM）请注意，抽象情况的条件保护是如何被转换为变量列表的，从那里不选择抽象变量。data方向：设置位置Lt RtIn：方向–vposns：AtomΛ List（List Direction）vposnsa=ΛIt（List（List Direction））varvposns appvposns（[ a]，126E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109absvposns）其中E. Copello et al. /Electronic Notes in Theoretical Computer Science 323（2016）109127→→→⎭→→·→·→ →→varvposns：Atom→List（List Direction）varv posnsbwitha=？AB... | yes _ =[[]]... | no_ =[]appvposns：List（List Direction）→List（ListDirection）List（List Direction）appvposnsl r= map（_：：_ Lt）l++ map（_：：_ Rt）rabsvposns：原子列表（列表方向）列表（列表方向）absvposnsa r=map（_：：_ In）rA.6变参数和变项为值域的递归替换函数的一种变体，它用一个项替换一个变量，但通过将被替换的项包装在每个遍历的绑定器的名为“0”的变量的一个应用程序中来进一步调整被替换的项。y/=xy=0⎫⎪⎬子图：Λ×变量×Λ→Λsub（P，x，v y）=if（x==y）then P else（v y）sub（P，x，M·N）=（sub（P，x，M））·（sub（P，x，N））suby/∈fv（P）为了用迭代器原理实现这个函数，我们必须改变参数的顺序，所以我们的迭代器原理现在返回一个等待替换项的函数通过这种方式，我们可以通过迭代来改变参数。hvar：原子→原子→Λ →Λhv arxy，其中x=？的y... | ye