构造型理论中Stoughton的Lambda演算替代概念的形式化证明

可在www.sciencedirect.com在线获取理论计算机科学电子笔记312（2015）215-230www.elsevier.com/locate/entcsStoughton替代Lambda演算的构造型理论的形式化Álvaro Tasistro1 Ernesto Copello2乌拉圭蒙得维的亚ORT大学摘要在[25]中，Alley Stoughton提出了Lambda演算的（同时）替换概念，在其原始语法中公式化-即，变量只有一种符号（名称），根据这样的表述，替换对项的作用由简单的结构递归定义，并且产生了一个关于与α-转换的联系的有趣理论。在本文中，我们使用Agda语言对Stoughton在构造类型论中的工作进行了形式化 开发已经相当便宜，例如在劳动力成本，我们能够制定一些改进，在原来的介绍。例如，我们对α-转换的定义只是语法指导的，我们以一种简单的方式证明了它是一个等价关系，而在[25]中，后者被作为定义的一部分，然后被证明等价于一个仅仅接近结构的定义，作为一个更简单的发展的必然结果。作为这项工作的结果，我们倾向于断言，斯托顿关键词：形式元理论，Lambda演算，构造类型理论1引言Church [5]引入了Lambda演算，但没有定义替换。这个操作的复杂性实际上是Curry和Feys在[7]中提供第一个定义的主要动机，如下所示1电子邮件：tasistro@ort.edu.uy2电子邮件：copello@ort.edu.uy3电子邮件：szasz@ort.edu.uyhttp://dx.doi.org/10.1016/j.entcs.2015.04.0131571-0661/© 2015作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。216×。Tasistro等人/理论计算机科学电子笔记312（2015）215⎨⎪⎪⎨⎪如果x=y，则x[y：=P]=P如果x/=y，则为x（MN）[y：=P]=M[y：=P]N[y：=P]如果y在λx. M中不是自由的，则为<（λx.M）[y：= P]= λx.M[y：=P]如果y在λx.M中自由，x在P λz中不自由.（M[x：=z]）[y：=P]如果y在λx.M中自由，x在P中自由，其中rez是MP中第一个不为ree的变量。复杂性在于最后一种情况，即需要重命名执行替换的抽象的绑定变量的情况。显然，递归是根据项的大小进行的;但是，为了确定M[x：=z]是的大小小于λx.M的大小，必须给出证明，并且由于重命名是由正在定义的相同的替换操作来执行的，因此，一个证明必须与整个定义的正当性同时进行。这是非常困难的正式在任何几个证明助理可用。此外，对于置换运算的性质的证明，还必须根据项的大小进行归纳，这也是不方便的 一般有三个子案例，其中两个引用了归纳假设 在上面考虑的子案例中。这些观察促使人们寻找一个更简单的定义。众所周知，所提出的解决方案中的若干方案采取修改如上所使用的语言的语法的路径。这样的决定确实是很有动机的，特别是如果替代方案是为局部或绑定名称使用一种与变量之一不同的符号类型：这是弗雷格的选择在第一个完全边缘化的形式语言[11]中，它以普遍的量化为特征，后来至少由根岑[12]，普拉维茨[22]和科昆德[6]再次提出。在机器检查元理论领域，McKinna和Pollack[18]使用该方法在证明助手Lego中开展了大量工作，涉及纯Lambda演算和纯类型系统。现在，该方法并非没有一些开销：必须对每种名称进行一次替换操作，并使用一个格式良好的谓词来确保绑定的名称不发生无约束的-因此，归纳条款实际上成为归纳上这个谓词。 另一种选择当然是de Bruijn它的最新版本本地无名语法[2，4]，它使用自由或全局变量的名称和索引计数到绑定抽象器，局部参数的出现。 也就是说，局部无名语法是弗雷格风格语法的一种变体，其中局部参数是无名的。这种情况下的开销如下：格式良好的谓词确保×。Tasistro等人/理论计算机科学电子笔记312（2015）215217术语不包含太大的索引，并且除了对自由名称的替换之外，用一个新的名字打开，以确保只有良构的条款，其中的索引从来没有提到非本地的抽象器被使用，因此，需要在减少转移的索引是避免的。变量关闭的双重操作也是必要的，它从术语中抽象出名称，用绑定变量替换它，即索引。在这种情况下，不必考虑α -转化当然是一种解脱;但是，与此同时，无名语法严重影响了人类对术语的可读性，因此可以说它与自然语法相距太远。在[24]中引入的地图表示也是如此。与此同时，研究Lambda演算的原始、普通语法的可能性仍然很有趣在非正式的环境中（例如[3，14]），标准的方法是确定α等价项，每次选择一个方便的代表，根据所谓的巴伦德雷特变量约定：只需选择相互不同的约束变量，并且与当前上下文中的现在，这个约定需要仔细的表述，以便它与结构归纳和递归兼容，因为后者要求归纳步骤适用于任意变量，而不仅仅是方便地选择的变量。相应的形式化已经以α-归纳法和递归原理的形式提供，例如[21，20]，并已在证明助手Isabelle-HOL [26]和Coq [1]上以包的然而，如果有人坚持保留库里和费斯的基本方法，并直接研究具体的条件，那么就有一个值得检验的主要的见解很简单：在需要重命名绑定变量的困难情况下，如果让替换增长多个（同时）而不仅仅是一元，则可以恢复结构递归此外，如果在抽象中考虑替换时不去区分这么多的情况，而只是统一地对约束变量进行重命名，那么就可以实现进一步的简化：事实上，给定约束变量重命名下的等价性是自然和必要的，就像柯里-费斯定义中那样，试图尽可能多地保持具体项的同一性是没有意义的。 指出的Stoughton提出的使用多重替换的思想来自[9]，而统一重命名的思想最初在[23]中提出。在Lambda演算的上下文中，所得到的替换和α-转换理论除了从根本上简化推理方法之外，还有许多好的性质可能最有趣的结果是，单位代换使关于α-转换的项正规化，这正是由于统一重命名的方法Stoughton在这一主要发展过程中，证明了α-转换的所谓替换引理，它表达了替换与α-等价之间的相容性。本文的目的是探讨形式化的建设性218×。Tasistro等人/理论计算机科学电子笔记312（2015）215Stoughton公式的类型理论和随后的Lambda演算中的替换理论。Lee在[16]中进行了这种形式化，但我们相信我们正在对其进行一些实质性的重新表述。特别是，该工作将多个替换表示为从变量到项的（总）函数（与[25]相同），并通过在Coq中制定一个公设来定义替换的命题恒等式作为它们的扩展等价。我们对这种策略相当不满意，因为我们更喜欢命题恒等式来反映定义的、因而是可判定的等式。我们也将把多个替换表示为函数，但将通过实际研究对项（的自由变量）的替换的限制来避免使用这种完全外延等价。这种限制的概念实际上构成了有关替代的概念。我们还介绍了关于斯托顿的原始配方和刚才提到的形式化的简化其中最重要的是α-转换的定义：如前所述，斯托顿另一方面，李我们对α-等价的定义直接遵循项的结构与Stoughton和Lee不同的是，我们不需要已经提到的替换引理来证明α-转换的语法定向我们从来没有-ertheless进行我们的发展，直到这个结果，因为事实上，这是一个重要的一块在随后的发展的元理论的λ演算，特别是在各种引理导致教会-罗瑟定理。在下一节中，将尽可能详细地介绍正式发展情况，并在最后一节中提出结论性意见。2形式化我们使用Agda语言[19]。本文档实际上是一个文字化的Agda文档，为了简洁起见，我们在其中隐藏了一些代码完整代码可在以下网址获得http://fi.ort.edu.uy/innovaportal/file/17663/1/lsfa.lagda网站。Agda实现了建构类型理论[17]（简称类型理论）。它实际上是一种函数式编程语言，其中：(i) 归纳类型可以像往常一样引入，即通过枚举它们的构造函数，但它们可以在其他类型的对象中参数化。因为后者，类型论以类型族（由基类型索引）或依赖类型为特征。(ii) 类型族上的函数依赖于基对象，也就是说，它们通常具有（x：α）→βx的形式，其中βx是类型×。Tasistro等人/理论计算机科学电子笔记312（2015）215219参数化为α型的x。因此，函数输出的类型取决于输入的值(iii) 归纳类型上的函数由模式匹配方程定义(iv) 语言的每一个功能都必须是终止的。强制实现这种条件的递归的标准形式是结构递归，当然，它是经过语法检查的。(v) 由于上述特征，类型论可以被解释为一种推理逻辑。具体地说，这是通过将命题表示为归纳类型来实现的，归纳类型的构造函数是所讨论的命题的引入规则，即直接证明的方法。因此，我们可以概括地说，数据、谓词和关系的集合是归纳地定义的，即通过枚举它们的构造函数。2.1语法项的集合Λ是通常的。它是由一组可数的变量V构成的。dataΛ：Setwherevar ：V →Λ应用程序：Λ→Λ →Λ绝对值：V→Λ→Λ以下称为新鲜度关系。当一个变量在一个项中不是自由出现时，它成立。我们从名词性抽象语法的著作中引入术语和符号，参见例如[27]。 在调用函数时，写在花括号之间的函数参数可以省略data_#_：V→Λ→Set其中var：{xy：V}→y/x→x #变量yapp ：{x：V}{MN：Λ}→x#M→x#N→x #（appM N）abse：{xy：V}{M：Λ}→xy→x #（绝对值y M）ABS ：{xy：V}{M：Λ}→x#M→x #（abs y M）自由变量的概念，我们写为_*_，和往常一样。新鲜和自由当然是相互否定的我们通过定义两个积极的概念来工作，而不是使用否定。或者我们可以说：在编程术语中，我们通过引入这两种类型来自然地进行。在我们看来，编程方式是在建设性数学环境中进行的自然实践data_*_：V→Λ→Set其中var：{ x y ：V} → y x→220×。Tasistro等人/理论计算机科学电子笔记312（2015）215×？x * 变量yappl：{x：V}{MN：Λ}→x*M→x *（app M N）appr：{x：V}{MN：Λ}→x*N→x *（app M N）ABS ：{xy：V}{M：Λ}→x*M→y/λx→x *（ 绝对值y M）自由变量的相同性是项之间的重要关系，定义如下。符号代表有序对的类型，在命题作为类型的解释下，有序对是逻辑合取。_M *_：（M M_M*_M M这个定义应该与定义自由变量集然后使用（有限）集相等的标准实践（如斯托顿的工作）进行比较当然，新鲜变量的相同性也是同样定义我们省略细节。2.2取代替换是从变量到项的函数。n=V → Λ我们实际上需要有限的，几乎无处不在的同一性函数。 因此，我们将考虑由从原函数i开始的update操作<+up生成的函数。ι ：ι =idvar_+_：→V×Λ→（σ<+（x，M））y，其中 x=y... |是= M... |no=σ y后者定义了与更新子项中的每个变量相对应的项。现在，置换的大多数相关性质涉及它们对给定项（的自由变量）的限制。记R为限制类型，记σ]M为项M的代换σ的限制。R=×Λ×。Tasistro等人/理论计算机科学电子笔记312（2015）215221必须为限制制定正确的替换同一性概念。__：R→R →设置（σ，M）<$（σ以类似的方式，变量的新鲜度和自由度扩展到限制，如下所示：_#]_：V→R →设置x #]（σ，M）=（y：V）→y * M→x #（σy）_*]_：V→R →设置x*]（σ，M）=<$（λy→y*M×x*（σy））两个限制之间的自由变量的相同性同样简单：_*]_：R→ R →设置（σ，M）<$*]（σ（（x：V）→x *]（σ对于新鲜变量的相同性也可以这样做我们省略定义。2.3选择功能。需要一种机制来选择适合重命名的变量，以避免在执行替换时捕获。斯托顿假设一个功能的选择，它的作用于非空的变量集。然后，当置换σ作用于抽象λx.M时，选择一个在σ到λx.M的限制中不会自由出现的变量y，x以我们将在下一小节中说明的方式重命名为y斯托顿将y公式化为将假设的选择函数应用于上述替换限制σ的自由变量集的补集的结果。我们更倾向于简化公式，并实现一个选择函数χ，它作用于一个限制，返回其中的第一个变量因此，结果实际上只依赖于有限的变量集，即对于拥有相同自由变量的约束，χ的行为是相同的。形式上，我们的开发使用了以下关于χ函数的事实：(i) χ：R →V。(ii) X（σ] M）#（σ] M）。(iii) （σ]M）（σ]M）χ（σ]M）=χ（σ] M）。这些结果是从fχ的实现开始的，其将在本小节的其余部分中详细解释。由于变量构成一个枚举，我们总是可以选择第一个不属于σ]M的自由变量的有限列表的变量。该列表由以下公式计算：222×。Tasistro等人/理论计算机科学电子笔记312（2015）215◦连接将函数fvσ映射到M的自由变量列表上的结果。χ：R →Vχ（σ，M）=χ在这里，函数χ为了表述方便，我们现在假设变量都是自然数。然后x为了通过原始递归来定义这个函数，给出了一个额外的参数m，它限制了尝试的次数，最初，这个参数是用给定列表的长度来实例化的，这实际上是这样一个界限，每当X参数m在每一步都减少，这允许函数终止。如果我们看一下这个函数的结果类型，我们会注意到，除了所需的新鲜变量外，还返回了两个额外的值：一个是证明返回的变量不属于列表，或者已经达到了最大所需的尝试次数，而另一个则表明所选择的变量都在输入列表中。 这两个结果由函数的最后两个参数表示的不变量保证。χ '的代码显示在χ aux的类型之后。χaux：（n m k：V）→（xs：列表V）→n +m k→（（ y ：V）→ y n→y ∈ xs）→<$（λv→（v∈/xs<$v<$k）×（（y：V）→yv→y∈xs））--Xχ<除了目前的代码，我们已经写了一个完整的证明的正确性的选择函数χ。2.4替代行动替换对项的作用由结构递归定义。通过使用已经引入的选择函数χ来执行统一捕获避免重命名。请注意，重命名扩展了最初给出的替换。 显然，代入λx.M的结果与σx无关，因此，所选择的新名称y必须不捕获σ对抽象λx.M的限制中的变量。_·_：Λ→Λ→Λ（var x）·σ=σx（app M N）·σ=app（M·σ）（N ·σ）×。Tasistro等人/理论计算机科学电子笔记312（2015）215223（abs x M）·σ=abs y（M·（σ<+（x，vary）其中y=χ（σ， abs x M）因此：lemma-subst-σ：{M：Λ}{σσ（σ，M）<$（σ即，作用于它们重合的项的相等替换产生相同的结果。下面的引理可以理解为表达了在替换中避免捕获：引理eσ→：{x：V}{M：Λ}{σ：Λ}→x*（M·σ）→x*]（σ，M）引理eσ←：{x：V}{M：Λ}{σ：Λ}→x*]（σ，M）→x*（M·σ）他们遵循简单的归纳的_*_关系。2.5阿尔法转换归纳定义很简单，遵循术语的结构data_α_：Λ→Λ→Set其中var：{x： V} →（var x）α（var x）app：{MM（app M N）α（app Mabs：{MMy #（abs x（M·（i<+（x，vary）<（绝对值x M）α（绝对值x我们用更友好的符号来表示最后一条规则。 注意它的对称性：M（i<+（x，z））<$αM<$（i<+（x<$，z））z#λxM，λx<$M<$λxM<$αλx <$M<$这个规则的对称性有利于某些证明，我们将很快评论。在斯托顿的定义中，它并不存在，斯托顿的替代的α等价也在限制条件下得到了恰当的定义：（σ]M）<$α（σ<$]M<$）<$M <$$> M <$$>（<$x）（x<$M <$σ x <$α σ<$x）224×。Tasistro等人/理论计算机科学电子笔记312（2015）215∼∼∼2.6引理以下是开发的主要结果我们给所有的声明在数学符号和Agda。我们给出的证据的意见，并显示其中一些明确。引理1MαMMM.引理M<$M（z ：V）→z * M→z * M'引理M<$M（z ：V）→z * M的推广是通过对关系_α_的y归纳，除了第三个χ引理外，还需要三个新鲜引理.引理2M<$αM<$$>Mσ=M<$σ，也就是说，任何替换都等于α可转换项，这是由于一致的避免捕获的重命名.形式上：引理MαMσ<$，其证明在下面进一步示出完整的代码是：引理-subst：{MMM<$α Mlemma-subst{M}{M=开始M ·σ引理-subst-σ<$σ<$σM·σ引理M

下载后可阅读完整内容，剩余1页未读，立即下载