理论计算机科学电子笔记228（2009）37-52www.elsevier.com/locate/entcs一个简单的名词类型理论詹姆斯·切尼1爱丁堡大学11 CrichtonStreetEdinburgh EH8 9LE，英国摘要名义逻辑是一阶逻辑的扩展，其特征对于推理具有绑定名称的抽象语法非常有用。对于计算应用，如编程和形式推理，需要为名义逻辑开发构造性类型理论，扩展命题，一阶或高阶逻辑的标准类型理论。这已经被证明是困难的，主要是因为名义逻辑的名称抽象操作和普通函数抽象之间的复杂交互。 这种困难已经出现在命题逻辑和简单类型理论的情况下。 在本文中，我们将展示如何这种困难可以克服，并提出了一个简单的名义类型理论，享有的属性，如类型健全性和强规范化，并可以合理地解释使用现有的名义集模型的名义逻辑。我们还概述了如何为具有绑定结构的语言提供递归组合子。 这是理解名词逻辑的构造性内容并将其纳入现有的构造性逻辑和类型理论的第一步。保留字：名义术语，类型系统1介绍名义逻辑[14]是一阶逻辑的变体，它将名称绑定公理化。 和使用置换重命名或交换的α等价。到目前为止，名义逻辑主要是使用经典模型理论[3，14]或证明-理论[2，6]对方程和新鲜度属性的显式推理进行了形式化。虽然这种分析适用于基于经典逻辑[25]的定理证明系统中的实现，但名义逻辑却拒绝纳入基于类型化演算的推理系统。这是不幸的，因为名义逻辑似乎很有希望作为各种设置中关于名称绑定的归纳推理的基础，而构造性逻辑由于命题作为类型和证明作为程序的原则而具有许多优势：公式的构造性证明可以被视为用于执行相应类型的计算的程序。 特别是，我们希望名义逻辑的类型理论，1电子邮件地址：jcheney@inf.ed.ac.uk1571-0661/© 2008 Elsevier B. V.根据CC BY-NC-ND许可证开放访问。doi：10.1016/j.entcs.2008.12.11538J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37⟨ ⟩⟨ ⟩ ⟨⟩×−◦将当前需要显式执行的关于名称抽象的新鲜度推理内在化，以证明递归和归纳对于名义抽象语法的合理性（例如，在[9，15，23]中）。虽然Gabbay和Cheney [6，2，5]已经在工作中考虑了直觉名义逻辑的证明理论，但这些系统只考虑可证明性，而不考虑证明项。在这样的系统中可用的证明树本身可以被视为证明项，但是这样做并不能立即产生具有良好属性的行为良好的类型理论。此外，这两个系统都涉及大量关于平等和新鲜度的明确推理名义类型理论也被S cho？pp和Stark[19，22]研究过，他们发展了一个基于名义逻辑的范畴模型的类型理论家族。他们的方法名义依赖类型理论是非常有表现力的，但主要是由语义动机。计算上重要的句法属性，如强规范化和类型检查的可判定性尚未研究，似乎难以获得由于系统的复杂性。因此，识别具有计算属性的名义逻辑的类型理论表示的问题仍然是开放的，这些计算属性使它们适合用于自动推理在本文中，我们考虑一个简单的情况下，这个问题。具体地说，我们引入了简单类型lambda演算的一个扩展，它将名称和名称抽象类型α A与引入形式a：α M（抽象）和消除形式M@a（具体化）合并在一起。此外，我们的方法也可以扩展对象语言的递归组合子在语法和语义上的声音的方式。在这种方法中遇到的一个关键困难是名称抽象与普通函数（λ-）抽象的相互作用。具体地说，在语义级别上，名称具体化操作要求将名称作为参数传递给抽象在抽象体中不是自由的。 因此，项M1=（αa：αb（a，b））@b是不好定义的-它将部分函数M2=αa：αb（a，b）应用于不在其定义域中的值。类似地，项M3=（（λx：α. a：α（a，x））b）@ b是不好定义的，因为它β-约化为M1。 更微妙的是，项M4=（λa：α<$λx.x@a）也是定义不好的，因为（M 4@b）（α a：α b（a，b））也可归约为M1。以前的系统通过要求关于交换、新鲜度和相等性的明确推理来处理这个问题（参见。[2、6、9、15、19、22、23、25]）。然而，正如许多作者所指出的那样，名称抽象类型构造函数α A可以用两种同构的方式来解释：作为关于α-等价关系（α A）/α的对集合的商，或者作为（部分）函数空间α A，由只能应用于“新鲜”名称的函数组成，类似于集束蕴涵逻辑（BI）及其类型理论中的“魔杖”连接/类型构造函数[ 11 ]。 S chöopp和Stark的类型理论认为，名称抽象有两种形式的引入和消除，一种是双元对表示，另一种是部分功能表示。（他们的系统还考虑了相关的乘积和和类型，这增加了进一步的复杂性。在本文中，我们考虑的后果，设计一个J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3739⟨⟩∗∗∗∗►\关于我们具有仅对应于部分功能表示的名称抽象的最终类型理论，使用专门针对这种情况的更简单形式的集束上下文。名称抽象类型的引入形式则是名称抽象项a：α M，其中a在M中有界（与在λ-抽象λx：A.M中x在M中有界的意义相同）。消除形式是“凝结”操作M @ a，在FreshML的某些版本中很这自然会导致类型规则：Γ#a：α<$M：A（a/∈Γ）Γ <$A：α<$M：<$α<$ArM：rαAra：α（）rM@a：B然而，第二个类型规则（）不能表达凝固的新鲜度约束;它允许上面所有定义不好的项M1为了得到一个只定义在名义集合论域中有意义的表达式的类型论，具体化M@a的类型规则必须确保a不能出现在M中，无论M如何被实例化。 基本思想是使用具有表达新鲜度信息的附加结构的上下文，如先前在[2]中针对全标称逻辑和在[22，19]中更一般性地探索的。我们考虑可能具有普通变量绑定Γ，x：A的上下文Γ，其中A是任意类型，以及当我们对具体化M@a进行类型检查时，我们必须能够使用上下文中的信息来证明a对于M中存在的所有符号都是新的。这就引出了一条规则ra：α\rJrJ <$M：<$α<$A（）IM@a：B这个规则使用了一个辅助判断Γ a：α ΓJ，直观地说，它将a：α从Γ中移除以产生ΓJ，并且还移除了所有可以用包含a的东西替换的变量。抽象子项M相对于该减少的上下文Γ j进行类型检查。这就确保了凝固是有明确定义的。本文的主要贡献如下。 我们介绍（第2节）一个基于（**）规则的简单的名义类型理论（这里缩写为SNTT），并证明了SNTT的类型可靠性（2.1节）和强规范化（2.2节）。我们还（2.3节）通过展示如何使用名义集合来解释SNTT，从而将SNTT与名义逻辑联系起来。在第3节中，我们展示了SNTT如何可以用条件、名称相等和原始递归组合子来扩展，这些组合子可以用来定义函数，如捕获避免替换。在第4节和第5节中，我们将SNTT与其他系统联系起来，并讨论未来的发展方向。2简单名词类型理论SNTT的基本语法类包括可数的、不相交的变量集V=x，y，z，.。. . 和名称（或原子）A=a，b，c，. . . ;原子数据类型符号δ，δJ，. 和名称类型符号α，αJ，.. . 和常数符号c，d，. 额外语法类包括类型A、B、项M、N、上下文Γ和替换θ，其抽象语法由以下语法规则描述：40J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37⟨⟩··--►\∈/∈⟨ ⟩ ⟨⟩∈∈FVN（（））=FVN（c）=FVN（z）={z}（z∈V <$A）FVN（λx.M）=FVN（M）− {x} FVN（πi（M））=FVN（M@a）=FVN（M）FVN（M）=FVN（M）− {a}FVN（M，N）=FVN（M N）=FVN（M）<$FVN（N）FV（M）=FVN（M）=FVN（M）FVN（·）=FVN（θ，M/x）=FVN（θ）<$FVN（M）FVN（θ，b/a）=FVN（θ）<${b}图1.一、自由变量和自由名称函数x[θ]=θ（ x）a[θ] = ac[θ]=c（）[θ] =（）πi（M）[θ]=πi（M [θ]）（M，MJ）[θ]=（M [θ]， MJ[θ]）（MMJ）[θ]=M[θ]MJ[θ]（λ y：A. M）[θ]=λ y：A. M[θ，y/y]（y/∈FV（θ））（M@a）[θ] =M[θ−a]@θ（a）（α a：α <$M）[θ] = α a：α <$M[θ，a/a]（a/∈ FN（θ））图2.避免捕获的替换/重命名A，B：：= 1|A×B|A→ B|α |α|δM，N：：= c|X|（）下一页|（男、女）|πi（M）|λ x：A.M| M N|一|a：α|M@ar：：=·|r，x：A |Γ #a：α θ：：=·|θ，M/x |θ，b/a许多类型（单位、配对和函数类型）及其相关的引入和消除形式都是标准的。名称a总是具有某种名称类型α;抽象类型α A与引入形式a：α M（称为名称抽象）和消除形式M@a（称为名称具体化）相联系。我们定义图1中一个项的自由名集合FN（M）和自由变量集合FV（M），将a视为抽象运算a：α M中的绑定，将x视为λx：A.M中的绑定。我们还将FV和FN扩展到替换。 顺序在上下文中很重要。我们认为术语等价于绑定名称和变量的模一致重命名;此外，按照惯例，我们将上下文写为x：A或a：α，而不是、x：A或#a：α。 我们将M[θ]作为对M进行替换θ的结果;这在图2中定义。 我们给出了完整的定义，以消除任何混淆的风险：特别是，注意到重命名和FN只是语法操作;它们不应该与2.3节中讨论的交换和支持的概念混淆。我们假设一个固定的签名n =c：A，。. . 为语言的常量分配唯一的类型。SNTT的术语良构规则如图4所示。图3中定义的限制判断Γa：αΓJ直观地意味着a：α出现在Γ中，并且ΓJ是从Γ中移除所有值可能依赖于a的绑定的结果。注意第二条规则和第三条规则之间的区别。 我们写a：αr或x：Ar表示a或x与给定的类型存在于Γ中，写a /Γ或x我说，没有这样的约束力，或x分别存在。我们假设所有的签名和上下文都是有效的，也就是说，不包含重复的变量或名称绑定。用于减少和扩展SNTT项的重写规则包括J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3741→→⟨ ⟩⟨ ⟩ ⟨⟩→ ⟨ ⟩（a=/b）、Γa：α\ΓJΓa：α\ΓJr #a：αa：α\r #b：βa：α\rJ#b：βr，x：Aa：α\rJ图三. 语境制约判断c：A∈πconrc：A（）：1单位IIΓ M1：A1r M2：A2r（M1，M2）：A1× A2我ΓM：A1×A2Γπi（M）：Aix：A∈Γvarr，x：AM：B（x/∈ Γ）IΓM：A → BΓ ► N：A⇒ EΓx：AΓλx：A.M：A →B产品编号：Ba：α∈Γ名称Γ#a：α<$M：A（a/∈ Γ）absIra：α\rJJΓα：αΓ► ⟨a:α ⟩M: ⟨α ⟩AΓM@a：A见图4。 简单名词类型理论：良构性以下规则，其中大部分是标准的：πi（M1，M2）dβMiM：A1×A2dη（π1（M），π2（M））（λx.M）N dβM[N/x]M：A→B dηλx：A.M x（x/∈FV（M））（λa：α <$M）@b dβM[b/a]M：α <$B dη<$a：α<$M@a（a/∈FN（M））M：1 dη（）对于由d β，d η生成的重写关系，我们写作−→ β，−→ η，并写作M←→nβηN，以表明M和N可βη-转化为公共形式。 记M <$βN表示M在β -约化下收敛于规范型N，对M <$β N记M <$β.除了涉及高阶常数的任意签名外，我们还考虑了名义签名（见[15，24]）。 这些签名中所有的常量C有A型其中，A是一阶（即， 不使用）和δ是一个数据类型.我们还定义了SNTT项的子语言，称为地面名义项，它与[15，24]的地面名义项基本相同M0，N0：：=（）|cM0|（M0，N0）|a：α|一SNTT包含了带有单位和乘积类型的简单类型lambda演算的所有规则（我们称之为简单类型理论或STT），因此任何类型良好的纯λ项都可以在SNTT中使用相同的类型进行类型检查。任何类型良好的地面名词术语也可以在SNTT中根据其名词签名进行类型检查和只包含名字的上下文。稍后我们将证明（推论2.13）SNTT是这两个系统的保守推广例子. 在讨论正式结果之前，我们展示了一些包含名称抽象和λ抽象的良构项和劣构项的示例（图5）。例（a）说明了一个术语，其类型对应于“弱化”法Aα A表示名称抽象类型。 例（b）显示了如何对项λx：α A进行类型检查。a：α x @ a，是α A型的完全η-展开恒等函数。示例（c）和（d）提供了不可类型化的术语的部分派生;在（d）中，没有名称可以填充为？？ 这将使术语typecheck。示例（e）-（j）示出了名称抽象类型的附加属性，省略了派生。例（e）给出了一个证明“名称交换”定律的项;这是类型<$α <$$> α j <$A∧E42J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37⟨⟩⟨ ⟩x：A#a：αx：A(a)x：Aa：α x：αA·λx：A. a：α(b)x：α A#a：αa：α\x：α Ax：α A x：α Ax：αA#a：αx@a：Ax：α Aa： αx@a： αA· ► λx：λ α λ A。a：α αa：αa：α困(c)a：α，x：α A a：α\ ··αa：α，x：<$α<$A<$x@a：Aa：α<$λx：<$α<$A.x@a：<$α<$A→A► a：α<$λx：<$α<$A.x@a：<$α<$（<$α <$A →A）(d)因为没有名字a：α是已知的x：α A x@？？：一个·λx.x@？？：αA → A（五） λx：<$α <$$> αJ <$A。 a：α j（f）第（1）款/λx：α α A。 a：α <$（x@a）@a：<$α <$$> α <$A → <$α <$A（g）<$λx：<$α <$（A → B）。 λy：λ α λ A。 a：α（h）/<$λx：<$α <$A → <$α <$B。 a：α（x？？）@a：（<$α <$A → <$α <$B）→ <$α<$（A → B）（i）<$λx：<$α <$（A × B）。 （a：α <$π1（x @ a），a <$π2（x @ a））：<$α <$（A ×B）→ <$α <$A × <$α <$B（j）λ x：λ α A× λ α B。α a：α <$（π1（x）@a，π2（x）@a）：（<$α <$A× <$α<$B）→ <$α <$（A×B）图5.示例派生和非派生M：AΓθ：ΓJr b：α\r0Γ0θ：ΓJr·：·rθ，M/x：rJ，x：AΓθ，b/a：ΓJ#a：α见图6。 合式置换和αJα A。示例（f）显示了名称抽象的“收缩”法则的失败2.1形式特征为了简化下面的讨论，我们在图6中为替换引入了一个例如，请注意，一旦一个名字被用来替换其他名字，我们就不能在替换中重用它;也就是说，θ=a/b，a/c和θ=（a，b）/x，b/c是病态的。这是因为第三条规则要求我们在从上下文中删除b和所有可能依赖于b的变量之后，通过类型检查θ来类型检查θ，b/a。此外，置换只能执行单射重命名。我们将Γ上的恒等式替换记为idΓ我们将M [idΓ，N/x]表示为M [N/x]，将M[idΓ，b/a]表示为M [b/a]，条件是Γ从上下文中是清楚的。我们说一个上下文Γ包含在另一个上下文ΓJ（记作Γ≤ΓJ）中，如果ΓJ≠ Γ：Γ。两 个上下文是等价的（Γ<$ΓJ），如果Γ≤ΓJ≤Γ。例如，y：B #a：α，x：A≤x：A，y：B #a：α，z：C，而x：A，y：B ≤ y：B，x：A。可以使用相对简单的技术来建立弱化。这个证明并不是完全无关紧要的，因为我J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3743们需要证明上下文的弱化44J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37► ►►限制判断，这需要证明几个辅助性质，我们在这里省略。引理2.1（弱化）若Γ ≤ Γ J且Γ <$M：A则Γ J<$M：A。接下来，我们可以证明一个一般的替换引理：引理2.2（一般替换）如果ΓJθ：Γ且 ΓM：A，则ΓJM [θ]：A.更传统的替换和重命名性质紧随着θ的适当选择。引理2.3（代换）假设x不出现在Γ中。 如果r ∈ N：B，Γ，x：B <$M：A则Γ <$M [N/x]：A。引理2.4（重命名）假设b不出现在Γ中。 若Γ#a：α <$M：A则Γ#b：α <$M [b/a]：A.我们还需要上下文限制判断的几个性质，这些性质很容易通过归纳证明引理2.5（限制）若Γ_a：α\ Γ_J则a/∈ Γ_J且Γ_J#a：α ≤ Γ。最后，我们展示了引理2.6（局部可靠性）若Γ <$M：A且M dβN，则Γ <$N：A.证据 证明是通过重写步骤和反演导子的情况。 为在名称抽象的情况下，使用重命名和弱化来简化步骤是简单的：ΓJ#a：α<$M：AAbsiΓJ#a：αM：ARr b：α\rJΓJa：α M：α AabsE =ΓJ#b：α<$M[b/a]：AWΓ（a：αM）@b：AΓM[b/a]：A因为根据引理2.5，b：α/∈ ΓJ且ΓJ#b：α ≤ Γ。Q引理2.7（局部完备性）如果M dηN则ΓM：A当且仅当A.证据 同样，唯一的新情况是名称抽象。 如果我们有M：<$α<$A dηα：α<$M@a，对于a/∈FN（M），则Γ►M: ⟨α ⟩A ⇐⇒Γ#a：αa：α\ΓΓ►M：⟨ α ⟩ AabsEΓ#a：αM@a：AabsIΓa： αM@a： αAQ定理2.8（主语归约）若M：A且M−→βN或M −→ηN然后是A。J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3745⇓►►我们已经使用Isabelle/HOL-名义系统[25]将开发形式化到这一点。2.2强规范化和规范化在这一节中，我们希望证明SNTT具有强正规化和规范化的性质（存在β-正规η-长规范型）。丘奇-罗瑟定理和强正规化定理都可以用与λ-演算基本相同的论证定理2.9（Church-Rosser）若M−→βM1且M −→βM2，则存在N使得M1−→ <$βN和M2−→ <$βN。定理2.10（强正规化）如果M：A则MβV表示唯一的V：A。强正规化有几个有用的结果：我们可以得到唯一的β-正规，η-长的标准形，首先根据它的类型对每个子项进行η-展开，然后进行β-正规化。这给出了βη-等价性的一个判定过程。推论2.11（标准化）若M：A则M有唯一的βη-标准型。推论2.12（可判定性）β-等价和βη-等价都是可判定的。此外，SNTT是普通简单类型理论（STT）和地面名词术语语言推论2.13（保守性）STT的判断M：A可导当且仅当M：A在SNTT中是可导出的。 此外，鉴于名义上的签名M0是δ型良构项，其名称为a1：α1，..an：αn当且仅当a1：α1 #···#an：αn<$M0：δ在SNTT中可导。2.3名词集合语义学虽然主语归约和强规范化定理暗示SNTT是一个相容的等式理论，但它们并没有解释SNTT如何与名词性抽象语法相关。在本节中，我们将展示如何使用名义集合来解释SNTT的判断和方程[14]。 这意味着SNTT对于普通名义逻辑中的名称、名称抽象和函数的推理是合理的。我们把表现力和完备性的问题（例如，关于一个适当的推广carlycan闭范畴）留给未来的工作。在这一节中，我们考虑一种特殊情况，即只有一个名称类型α，它对应于所有名称的集合A。泛化到多个名称类型是简单的，但在概念上是很麻烦的.我们概括了一些基本的定义，涉及置换，群作用和语义所需的名义集（在以前的工作中介绍了由46J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37∈P∈ ||∀∈ −·|⟨⟨⟩⟩ |×||≡⟨ ⟨ ⟩ ⟩ ∈ ⟨ ⟨ ⟩⟩/∈Gabbay 和Pitts [7， 14， 15]） 。 我们 把所 有有 限名 称集 合 的集 合写 成Pfinn（A），把A上所有（有限）排列π的群写成G=FSym（A）;也就是说，可逆函数使得π（a）=a，对于除有限个a之外的所有a∈A。我们经常把π（a）写成π · a，把{π·x}写成π · S|x ∈ S}，如果S ∈ P f in（A）.一个G-集合是一个结构X =（|X|，·X）由一个集合X构成，该集合X具有一个置换作用·X：G × |X| → |X|，满足id·x = x和π·πJ·x =（π <$πJ）·x。我们写萨克斯是为了证明S finn（A）支持xX;即，a，b一S. （a b）Xx = x。一个名义集合是一个G-集合，其中每个元素都有一个有限支集（因此必然有一个唯一的最小有限支集）。 如果一个标称集合的元素x有空支集，它被称为等变的，并且显然对于任何π ∈ G，π·x = x。在以前的工作[7]中已经建立了，名义集形成范畴2Nom，它包括终端名义集1Nom，标准构造包括笛卡尔积X×NomY和函数空间X→NomY，以及名称抽象构造<$A<$X。我们对这些结构作一简要评述。定义2.14终端标称集合1Nom的定义如下：|1名|为{*}。交换动作定义为π·*=*。定义2.15两个名义集合X，Y的卡累利阿乘积定义如下：|X ×标称Y|为|X| × |Y|并通过规则π·（x，y）=（π·x，π·y）定义作用。定义2.16从X到Y的（有限支集）函数的名义集合X → Nom Y定义如下：|X →标称Y| ={f：|X| → |Y||S ∈ P finn（A）. S af}其中交换作用定义为（π·f）（x）=π·（f（π− 1·x））。定义2.17名称集合A是一个名义集合，其中π·Aa=π（a）。定义2.18给定名义集合X，X的抽象集合称为AX=（AX）/A Xα，其中α是满足以下条件的最小等价关系：（a/∈ supp（y）<$x =（ab）·XY）<$（a，x）<$α（b，y）.交换作用被定义为（b bJ）·[（a，x）]α=[（（b bJ）·a，（b bJ）·x）]α。我们经常将[（a，x）]α表示为 a x. 此外，如果y一个X和一个supp（y）则我们将y@a定义为y（a），将y视为部分函数。语义名称抽象满足SNTT名称抽象的β-归约和η-扩展定律的类似物。 我们需要以下名称抽象和具体的关键属性：命题2.19（i）如果a x ∈ A x且b/∈ supp（a x），则（ax）@ b =（ab）·x且supp（a x）=supp（x）− {a}。(ii)如果y∈ AX且a/∈ supp（y），则y=a（y@a）且supp（y@a）supp（y）{a}.[2]如其他地方所指出的[7，22，19]，Nom同构于一个著名的范畴Schanuel topos。J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3747UTT∈··∈→ T∈EE ∈ T→ ESS联系我们›→∪联系我们T[[1]] =1 NomE[[ Γx：A]]γ=γ（x）E[[ Γc：A]]γ= E0[[c：A]]E[[ Γa：α]]γ=γ（a）E[[Γ（）：1]]γ=γT[[δ]] = T0[[δ]]T[[α]] =AT[[A×B]]= T[[A]]×标称值T[[A →B]]= T[[A]] →标称值T[ [αA]]= A（ T[[A]]）T[[B]]T[[B]]E[[Γ（M，N）：A1×A2]]γ=（E[[ΓM：A1]]γ，E[[ ΓN：A2]]γ）E[[Γ<$πi（M）：Ai]]γ=Πi（ E[[Γ<$M：A1×A2]]γ）E [[Γ <$λx.M：A → B]]γ= Λv ∈ T [[A]]. E[[Γ，x：A <$M：B]]γ[x<$→v]E[[ rM N：B]]γ=（ E[[ rM：A →B]]γ）（ E[[ rN：A]]γ）E[[Γ #a：α <$M：A]]γ[a<$→aJ]（aJ∈/supp（γ））E [[Γ M@a：A]]γ= E [[Γj M：<$α A]]（rJa：α\r）S[[ΓJ·：·]]γ=[·]S[[ΓJ <$θ，M/x：Γ，x：A]]γ=S[[ΓJ <$θ：Γ][x→E[[M]]γ]S [[rJ <$θ，b/a：r #a：α]]γ= S [[rJ <$θ：rJ]][a <$→ γ（b）]（Γj b：α\ΓJJ）见图7。类型、替换和表达式解释假设我们将数据类型δ解释为名义集合0[[δ]]。 我们将其他类型的SNTT解释为标称集合[[A]，如图所示 图7.我们将解释的宇宙定义为类型AT [[A]]的所有解释的不相交的联合。这是一个名义上的集合。赋值是来自V的有限子集的函数γA（记住，V和A与宇宙不相交）. 我们写[ ]为空赋值，γ [xv]或γ [ab]对于具有变量约束的扩展赋值γ的结果，xdom（γ）或命名dom（γ）。我们定义交换作用于逐点估值：对于所有xdom（γ），（π γ）（x）=π（γ（x））。 这个交换动作使赋值成为一个名义集合，同构于有限乘积的集合 由VA的子集索引的U。我们定义满足上下文Γ的赋值集合如下：[[·]]={[·]}[[Γ，x：A]]={γ [x <$→ v] |γ ∈ [[Γ]]，v ∈ T [[A]]}[[Γ#a：α]]={γ [a <$→ b] |γ ∈ [[Γ]]，b ∈ A − supp（γ）}直觉估值满足上下文Γ，如果它将变量映射到Γ中适当类型的值，并且满足Γ中的所有新鲜度约束。特别要注意的是，dom（γ）中没有两个名字可以映射到同一个名字，如果γ[[Γ]]对于某个Γ。现在假设等变解释0 [[c：A]][[A]对于每个常数c：A都是固定的 。 我们将格式良好的表达式M解释为函数[[ΓM：A]：[[Γ]][[A]，如图7所示（技术上，定义是通过推导树上的递归）。请注意，名称抽象定义的附带条件总是可以通过将绑定名称重命名为远离支持来满足。的γ。 我们也将（格式良好的）替换θ解释为函数[[ΓJθ：Γ]]：[[ΓJ]][[Γ]]。 我们常常把它们分别归为[[M]]或[[θ]我们有以下基本属性：命题2.20（等变）对于任意满足Γ <$M：A的Γ，M，A，我们有 E [[M]]是等变的，在这个意义上，对于任意π ∈FSym（A）和γ∈ [[Γ]]，48J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37.E−→π·（E [[M]] γ）= E [[M]]（π·γ）。此外，supp（E [[M]] γ）<$supp（γ）。证据第一部分是对M的归纳。第二个是直接的：对于任何在名义集合X，Y上的等变函数f：X→Y， supp（f（x））<$supp（x）。Q引理2.21（约束的合理性）若γ∈ [[Γ]]且Γ ∈ a：α\ ΓJ则存在γJ∈ [[ΓJ]]使得γ（a）/∈ supp（γJ）且γJ与γ在ΓJ上一致。定理2.22（语义可靠性）设Γ，γ∈ [[Γ]]。 则（1）如果ΓM：A则E [[M]]γ ∈ T [[A]]，（2）若 Γ <$θ：ΓJ则 S[[θ]]γ ∈ [[ΓJ]]命题2.23（语义替换）如果Γ <$M：A且ΓJ <$θ：Γ，则对于任意γ ∈ [[ΓJ]]，我们有E [[M [θ]]] γ = E [[M]]（S[[θ]] γ）。定理2.24（方程的可靠性）如果Γ <$M，N：A且M←→<$βηN，则对任意γ ∈[[Γ]，我们有E [[M]] γ = E [[N]] γ。3扩展就其本身而言，SNTT并不是很有表现力。例如，它不能为表示语言语法的名义数据类型（如λ演算或π演算）定义大小、替换或自由变量函数。要做到这一点，我们需要布尔值、数字、条件、名称相等测试，也许还需要额外的类型验证，如列表。更重要的是，我们需要在名义数据集上进行结构递归。在本节中，我们将展示如何通过添加类型、常量和重写规则，在SNTT3.1条件句和名称相等考虑类型bool、常量true、false、条件和相等测试：if（−）then（ −）else（ −）：bool →A →A →A （=）：α →α →bool布尔值和条件的归约规则和指称语义是标准的。对于相等性测试，我们考虑规则：a= a dβtruea= b dβfalse[[M=N]]γ=真（E[[M]]γ=E[[N]]γ）false（E[[M]]γ/=E[[N]]γ）注意，在归约规则中，我们只考虑名称，而不是任意项。为了使Church-Rosser和语义可靠性性质成立，无论如何解释a和b，第二个β规则a =bβfalse都是有效的。因此，我们需要确保两个语法上不同的名字永远不会被识别为β约简的结果。这是通过absE规则中的上下文限制来实现的。此外，在指称层次上，等式归约规则对于良好类型的术语是合理的，因为如果上下文Γ包含两个不同的名称a，b，则γ ∈ [[Γ]]必须满足γ（a）/= γ（b）。J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3749∼ΛΛΛ3.2数字和列表自然数和列表也可以在Nom中定义。因此，我们可以用类型nat和listA以及常量来扩展SNTT：零：自然succ：nat→nat（+）：nat→nat→nat[]A：清单AM：：AN：A→listA→listAappendA：listA →listA→listAremoveA： αlistα →listα也可以添加标准递归原语。这些操作的语义是标准的，除了remove，我们在操作上定义为：remove（a[]）[]remove（inta） dβremove（删除）remove（a（b：：M））dβb：：remove（a M）（ab）请注意，与名称相等一样，这些规则依赖于语法上不同的名称在语义上总是不同的事实3.3名义递归组合子名义逻辑（以及相关方法，如作为绑定代数[4]）优于其他技术的是归纳推理和递归定义的原理的可用性，这些原理扩展了用于“一阶”语言的归纳和递归的作为一个示例，我们考虑具有常数的签名ΛΛ，其使用名义项来定义以α-等价为模的多项的语法Λ = {var：α→ Λ，app：Λ × Λ → Λ，lam：它已被显示在几个地方（见例如。 [3，15]），可以在名义集合上使用最小不动点构造来建模这种语言，因为X <$→ A <$<$X是名义集合上的连续算子。 由此得到的标称集合Λ = A+Λ×Λ+⟨⟨A ⟩⟩Λ is isomorphic to the set of all(open)lambda-terms moduloα-equivalence.不幸的是，现有的方法递归的名义条款似乎仍然比普通的datashees更复杂，因为额外的推理新鲜度需要执行。例如，在Norrish [9]，Pitts [15]和Urban 和Berghouts [23]的方法中，定义lam情况的函数必须满足在SNTT中，这个约束被内在化到类型系统对名称和名称抽象的隐式限制中。因此，我们可以（如[22，19]）简单地引入一个递归组合子和相关的λ-项语法的βη -转换如下，通过与普通代数数据集的类比recB：（α→B） →（B ×B →B） →（ <$α<$B→B） →（Λ →B） ∈<$ΛrecBfvarfappflam（varM）dβfvarMrecBfvar fapp flam（app M） dβ fapp（recB（π1（ M）），recB（π2（M）Λ Λ ΛrecBfvarfappflam（lamM）dβflam（arecB（M@a））Λ ΛM：Λdη recΛ（var）（app）（lam）M50J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）37ΛΛΛ⟨ ⟩⟨ ⟩size=λx. rec nat（λv. 1）（λm，n.m+n+ 1）（λn.n+ 1）x：Λ→intsubst=λx，f. recΛ（f）（app）（lam）x：Λ→（α →Λ） →Λsubst1 =λx，y，v.subst x（λw. 如果v=w则yelse var（w））：Λ→Λ →α →Λfvs=λx。reclistα（λv. [v]）（append）（remove）x ：Λ→listα见图8。 递归定义的例子。图8中显示了几个示例，包括大小函数、避免捕获的替换函数（同时替换和单个替换）和自由变量函数。所有这些例子都是类型检查，这是确保它们对应于λ项上的全终止函数所与（纯）FreshML一样，我们不能定义一个在名义集合语义中不存在这样的此外，类型系统阻止我们定义这样一个函数，因为给定一个类型为α A的变量，没有办法生成一个类型为α的名称，我们可以在lam的情况下返回。相反，许多（可计算）函数存在于名义集合语义中，但不能使用SNTT定义。特别是，依赖于“良好”使用本地名称的函数通过评估[15]来定义标准化，不能在SNTT中处理如前所述，SNTT签名和术语概括了先前工作中考虑的名义签名和地面名义术语[15，24]。给定任何名义符号集，可以直接为其所有数据集定义递归原理，以及适当的β-归约和η-展开规则，以获得扩展系统SNTT（n）。此外，我们猜想定理2.84相关和未来的工作大量的研究都名词性和其他技术的抽象句法与约束通知和激励这项工作，我们不能给一个完整的调查在这里。我们在论文的主体部分讨论了密切相关的研究，在本节中将简要讨论其他密切相关的最新工作;更详细的讨论可以在[3，15]中找到SNTT 很自然地会加上一个由“新鲜”对组成的α#A（a，x）其中a∈/supp（x）;这将是αλ-但是，我们需要使上下文更复杂来处理这个问题。Pottier [16]最近重新研究了为“纯”FreshML [ 12 ]推断新鲜度信息的问题这种方法减少了新鲜度的推理，以设置约束求解，并针对实际的编程，而不是演绎。这个系统可以对更多的程序进行类型检查，但是可能需要程序员用新鲜度约束来修饰类型。名词性抽象语法的递归已经被一些作者研究过了J. Cheney/Electronic Notes in Theoretical Computer Science 228（2009）3751∇·[9、23、15]。递归原理也使用其他技术开发，例如绑定代数[4]，函子范畴语义[8]，上下文理论[1]，模态系统[20]和参数化[26]。 Schürmann，Poswolsky，andSarnat最近[18]在Delphin语言中扩展了这种方法，允许在任意依赖的LF签名上进行函数式编程。 Pien-tka [13]开发了一种相关但独特的方法，使用显式上下文和上下文多态性在LF规范在SNTT中，这些方法似乎比递归需要更多的e-排序。以前的名义技术涉及检查新鲜度边条件;技术，如绑定代数和上下文理论依赖于非平凡的类型理论或范畴理论的基础;和大多数以前的高阶技术不提供平等的名称。SNTT的简单性是以（明显的）表现力为代价的;然而，人们对这些方法在表现力方面的比较（或应该比较）知之甚少。比较这些方法的表达性似乎是未来工作的一个关键领域未来工作的另一个直接方向是将SNTT扩展到更丰富的类型理论，如依赖或多态类型，这些类型可以作为更大的标称逻辑片段的证明系统。我们相信SNTT解决了将名词项与普
我的内容管理
展开
