更好的起泡引理对逻辑与计算类型理论的语义证明

理论计算机科学电子笔记171（2007）77-84www.elsevier.com/locate/entcs更好的起泡引理罗伯特·K·迈耶逻辑与计算澳大利亚国立大学工程与计算机科学学院115楼，堪培拉，ACT 0200，澳大利亚电子邮件：bob. anu.edu.au摘要BCD [1]在交叉型滤波器中对λ演算的建模依赖于一个关键定理，我称之为BL（Bubbling引理，跟随某人）。这个引理已经在[2，4]中扩展到包含布尔结构，包括特殊的联合类型;这个扩展引理我称之为BBL（更好的起泡引理）。在[5]和[4]中探索了交集和并集类型理论与[10]中已经存在的最小正相关逻辑B+之间的共鸣（实际上[9]应用BL和BBL得到了将组合子与相关理论和命题联系起来的进一步结果。在这些共振上，代数的滤波器变成了逻辑理论。[8]的语义在这里产生了BBL的一个新的和简短的证明，它考虑了完整的布尔结构，不仅包含B+，而且包含它的保守布尔扩展CB[10，7，8]。关键词：语义，子类型，经典相关逻辑，最小相关逻辑，CB，B+，类型理论，冒泡。1引言哲学家的相关逻辑与计算机科学家的类型理论是互补的。1动机不同的调查产生了或多或少相同的正式系统。关联逻辑是在寻找更好地解释蕴涵的过程中产生的，→连接词是逻辑的核心。类型理论试图将一个直观的话语世界分割成可管理的块，产生（希望）更安全的编程环境。这篇论文更具体地讨论了一个特殊的引理，我称之为更好的起泡引理（BBL）。我在这里使用相关逻辑的语义，如[10]和[7]中所提出的，来证明BBL。BBL本身就是对1感谢我在ANU工程与计算机科学学院逻辑与计算专业的同事我特别感谢John W Lloyd教授，他的旅行资助使我能够参加威尼斯DCM研讨会，我在2006年 7月提交了这份说明还要感谢我的女儿多萝西·K·迈耶（Dorothy KMeyer），她在新英格兰大学（University of New England）的计算机科学研究生学习产生了LaTeX的专业知识，使这篇文章在撰写时的千年中得以发表我很感激，桃乐茜。其他债务将在出现时予以说明。1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2006.12.03878R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）77Bubbling Lemma （ 以 下 简 称 BL ） 。 我 从 Mariangiola Dezani 那 里 学 到 了Bubbling引理2无论如何，作为命题2.4，起泡引理在她与Barendregt和Coppo的论文[1]中起着至关重要的作用在交型理论中建立λ演算的[3]正如我们在[5]中所证明的，这个滤波器模型同时也是Bλ T理论中λ的一个逻辑模型冒泡是在严格限制的[→，，T]词汇表中发生的事情，以更好的冒泡。相关的逻辑学家和类型理论家在寻求解除这些限制方面有一个共同的目标。逻辑学家试图至少添加一个析取项，也许还添加一个否定项;类型人群将前者视为类型联合，而后者（也可能）视为某种补充。从逻辑上讲，一个数字本文发展了一系列相关逻辑，并给出了它们的语义解释，包括[10]的自然极小正相关逻辑B+及其[7]的保守布尔扩张CB[4]类型理论家也在寻找他们工作的语义学基础;导致BBL的路线是由Frisch、Castagna和Benzaken在巴黎提出的[6，2，4]。2个房间我们的词汇表在这里将是双重目的（如[5]）。我们从原子p等开始，独立地作为命题或类型变量。将有一个常数T（一个由一切或[1]的整个空间ω所蕴涵的公式）。配方（或类型）A、B等， 应建立从原子和T下的二进制运算（合取或交集）和→（蕴涵或函数空间构造函数）。语句的形式是A≤B，其中≤（逻辑蕴涵或子类型）是二元关系符号，A和B是公式（或类型）。因此，我们的形式系统，在柯里[3]的风格，关系的，更自然的（如在[8，6，4]）与子类型的想法接触。我们刚刚描述了基本语言L语言。[5]我们通过增加额外的运算“取”（或“并”）将它扩展到语言L+T二进制操作应按范围递增的顺序排列为、（当存在时）、→，否则关联在右侧。我们在这里集中在一个额外的语言L< $，它的结果时，另一个一元连接<$（布尔否定，或complement-ment）被添加。在这种语言L<$中，我们通过下面熟悉的定义来获得T和TD. ABd=efB）[2]据我所知，Dezani也给它起了名字（她否认了这一点，她更喜欢引理3.14159，或者[1]中的任何名字）。3[1]建立在Coppo，Dezani和他们的意大利同事的工作基础上。4 CB在[ 7 ]中被称为CB+。5. T的照顾和喂养在这里很有趣。作为一个真理，在逻辑上被每一个公式所包含，T似乎是一个进入无关紧要的弯路。因此，B+和[10]的相关逻辑以及安德森-贝尔纳普传统中的相关工作都缺少从类型论的观点来看，T同样是不确定的;作为普遍的类型ω，T违反了亚里士多德的格言“存在不是属”。在类型理论家中，Venneri宣称她特别怀疑T。另一方面，T在类型理论和逻辑上都是有用的。由于在[10]的语义上保守地添加T是微不足道的（只要使T在每个状态s都为真），我们在这里将其视为无害。不仅如此，由于T具有强加于在[1]中的ω，在本文中，它是来自仁慈的造物主的逻辑礼物。R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）7779DT. Td=efpp，其中e p是第一个。我们将从语义上刻画相应系统的定理。（有关句法特征，请参见引用的论文。）一个布尔3-框架K在这里应该是一对，其中K是一个（状态的）集合，R是K上的一个3位关系。6设K是一个布尔3-框架，L是我们上面的一种语言让2={0，1}是真值的集合{false，true}。L在K中的一个可能的解释I应该是任何函数I：L×K→2。也就是说，一种可能的解释是，任何函数在每个状态下都为L中的每个公式As为K。并非所有可能的解释都算作解释。这是语义学，对小品词的意义也需要注意。这种注意力由原始粒子上的真值条件提供。7对于I（A，c）= 1，写[A]c<$[A]c对于I（A，c）= 0，并以明显的方式使用直观的连接词和量化器，我们有以下几个Tω。 [T]C总是T.[A<$B]c=[A]c<$[B]cT.[A<$B]c=[A]c<$[B]cT，[<$A]c=<$[A]cT→。[A→B]c=<$a，b∈K（Rcab<$[A]a<$[B]b）一个可能的解释I是一个假设所有适用的真值条件对I成立的解释。我们现在3-框架K中解释I的验证条件：六.在Ki∈K（[A]c<$[B]c）中A≤B在I上被证明3帧K中的有效性条件：VK A≤B在Ki中有效，且A≤B在K中的所有I基本有效条件：VB. A≤B基本有效，i ∈A≤B在所有3-框架K中有效3更好的起泡这就引出了我们的主题，起泡引理和更好的起泡引理。当这个陈述基本上成立时，我将简单地写为[6]各种保守扩张结果的一个令人愉快的结果是，我们可以在这里将自己限制在布尔3-框架上，这在[8]的第70页被称为b+ms。[10]的语义学还强加了一个对状态偏序≤敏感的遗传条件H，让人想起Kripke的直觉主义逻辑语义学中的类似条件。由于我们可以通过布尔3-框架，条件H在这里的情况下是没有用的，这进一步证明了神的仁慈。这样做的原因是，在不失一般性的情况下，我们可以把实际相等当作偏序≤。这也免除了[ 10 ]中B+的语义假设。80R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）773.1鼓泡设I是一个有限索引集。 然后冒泡引理说，BL. 设i∈I（Ai→Bi）≤A→B.则存在子集J<$I使得A≤<$j∈JAj且<$j∈JBj≤B。我把BL放在通常的格论约定上，其中Λ是零，设置，j∈ΛAj=T.BL在[1]中为交叉类型规程（以下简称ITD）规定;它得出同样的结论，即它对[10]的最小逻辑B+的→ T修改B T成立;见[5]。[1]中BL的实用性及其相关工作它保证了λx.M形式的项的解释的值确实是ITD-滤波器（=B T-理论）。3.2更好的起泡现在，为了更好的起泡！更好的起泡引理BBL（例如，[14]有两个部分。BBL 1。设<$i∈I（Ai→Bi）≤<$j∈J（Cj→Dj）.则在J中存在一个特殊的j使得<$i∈I（Ai→Bi）≤Cj→Dj。BBL 2。设I（Ai→Bi）≤A→B.然后对于每个子集J，我们有(i) A≤j∈JAj，或(ii) k∈I\JBk≤B这是CB的更好的起泡需要B的起泡的情况。不过，我现在不打算详细讨论这些问题。 相反，我将证明更好的冒泡语义。[8]我将证明BBL是B+的完全布尔（保守）扩张CB。 CB的BBL 2证明。证明是通过还原。引理声称，如果在→公式Ai→Bi的索引集I上的合取需要→公式A→B，则对于I的每个子集J，我们有：i. A≤j∈JAj，或ii. k∈I\JBk≤B所以假设，对于I的某个子集J，i和ii都是语义上无效的。我们用这个假设来证明，在这种情况下，iii. i∈I（Ai→Bi） ≤A →B在语义上也是无效的。 BBL 2随后对位。设J是i和ii都失败的I的子集。通过VI，T，则通过i的失败，在3-框架Ka=中有某种解释Ia，使得在Ia上，我们在状态a∈Ka并且对于所有j∈J，8BBL是一个美丽的定理。我是从德扎尼那里得知的，他在弗里施的博士论文中发现了这个想法。这篇论文是在巴黎ENS的Giuseppe Castagna的指导下完成的，研究了Benzaken在[6]和[2]中提出的子类型化的语义根据Castagna和Frisch的说法，它可能源于细谷的工作。R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）7781(1) [A]a(2) [Aj]a同时，通过ii的失败，对I b有一定的解释 在一个3-标架Kb=使得，在Ib上，我们通过VI，Ta得到状态b∈Kb使得，对于所有k∈I\J，(3) [Bk]b(4)[B]b设x是Ka和Kb都不存在的新元素. 我们构造了一个新的3-框架K=，其中K={x}<$Ka<$Kb.通过在K上适当地定义R，我们将使iii的前件在x处为真，但其后件在x处为假。这将为无效的第三，结束的论点。我们指定R如下：iv. Rxab。v. 对c，d，e∈Ka，Rcdei ∈Ra cde.vi. 对c，d，e∈Kb，Rcdei <$Rbcde.vii. 否则，对于所有c，d，e∈K，Rcde失败。这种规范的思想是，我们只是简单地将我们已经拥有的两个3-frame粘贴在一起，通过Rxab在x处将它们连接起来。我们通过在K中定义一个解释I来继续粘贴，该解释I在Ka侧复制Ia，在Kb侧复制Ib。具体地说，对于所有c∈Ka和d∈Kb，我们为每个原子p规定，I（p，c）=Ia（p，c）和I（p，d）=Ib（p，d）。对于新元素x，我们简单地设置I（p，x）=0对所有p。真值条件T→、T、T<$（以及根据定义，T和Tω）的施加则保证了在K中的每个状态e处，I在所有公式E上是良好定义的。这是一个基本的结构归纳法，安全地留给读者，以表明我在Ka中的每一个状态e的所有公式E上都与Ia一致，并且在Kb中的每一个e的所有E上都与Ib一致。至于它在x处做什么，我们必须检查I使iii的前件在那里为真，但其后件为假。没有问题后者I（A，a）=Ia（A，a）= 1和I（B，b）=Ib（B，b）= 0;由此，由于Rxab，我们有I（A→B，x）= 0乘T→。但是我们还需要检查每个Ai→Bi在I上x处为真（因此通过T， iii的整个这完全取决于i是否在我们开始的特殊子集J子情况α。i∈J。则I（Ai，a）=Ia（Ai，a）= 0，由上面的（2）。但是，由于Rxab是唯一涉及x的三元组，我们有I（Ai→Bi，x）= 1（可以说，通过T→中的前件的虚假性）。子病例β。i∈I\J。然后我们有I（Bi，b）=Ib（Bi，b）= 1，由上面的（4）。这也强制了I（Ai→Bi，x）=1（可以说，通过T→中的后件的真性）。因此，在iii的前件中的所有→公式在I上的x处为真。但是iii的后件在I上的x处为假。 因此，如果任何子集J∈I不满足（i），（ii）之一，则iii基本上是无效的。相反，这结束了CB的BBL 2的语义证明。82R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）77CB的BBL 1证明。通过对位。假设对于每个j∈J，(5)i∈I（Ai→Bi） ≤Cj →Dj基本上是无效的。 我们将证明，(6) <$i∈I（Ai→Bi） ≤< $j∈J（Cj→Dj）也是无效的 因此，由于BBL假设（6）的有效性，因此存在j∈J其中，（5）。我们继续非常仔细地构造，对于每个j∈J，在一个3-框架Kj=Kj，Rj>中的一个解释Ij。<我们也可以把下标j本身当作（1）的前件在Ij上为真而后件为假的也就是说，我们在Ij上（再次使用我们的缩写符号），新的状态cj，dj，使得应用T，T→，我们得到(7) Rj jcj dj(8) [Cj]cj(9) <$[Dj]dj(10) 对每个i∈I，[Ai→Bi]j在这个观察中有一个非常重要的观点，即，当我们在j处伪造→陈述时，我们总是可以选择一个新鲜的和新的c j和d j。[9]在许多逻辑中，我们没有这种奢侈;例如，逻辑R的一个公设指出Rxxx总是，因此我们必须注意三元关系的论点的重复。 此外，我们注意到，没有理由使任何原子p在任何特殊状态j∈J都为真。所以w.l.o.g.，Ij（p，j）= 0对于所有原子p和j ∈ J。在仔细地证伪了（5）的每一个例子之后，我们现在构造一个对应于（6）的反模型。我们可以假设，对于j/=k（j，k∈J，Kj<$Kk是空集。设K0=<$j∈JKj. 设x是一个不在K0中的元素，令K={x}<$K0.我们定义K上的三元关系R如下，对于每个j∈J：(11) 若a，b，c∈Kj，则Rabci <$Rj abc.(12) 如果a，b∈Kj，则nRxabi<$Rjab。(13) 否则，Rabc失败。这将使K=3帧。 我们继续定义一个解释I，K，因此：(14) 对所有的原子p和aj∈Kj，有I（p，aj）=Ij（p，aj）.(15) 对于所有的原子p和j∈J，I（p，x）=Ij（p，j）= 0。(16) 对于复合公式C和所有状态c∈K，设I（C，c）在K中确定[9]我以前的学生、后来成为澳大利亚国立大学校长的约翰·斯兰尼（John Slaney）通过电子邮件给我发了一封优雅的证明。我感谢他和我在澳大利亚国立大学的同事RajeR.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）7783通过强加真值条件T→，T，T<$。引理3.1对所有公式A和所有a j∈K j，I（A，a j）=I j（A，a j）。证明通过结构归纳是明显的，因为真值条件是相同的。Q引理3.2对所有j∈J和（6）的结果Cj → Dj，I（Cj→Dj，x）= 0。证明通过引理3.1，上面的条件（12），并且T→。Q引理3.3对于（6）的所有联合前件Ai→Bi，I（Ai→Bi，x）= 1。所有的I j都同意使A i→B i为真。为了归约，假设I（Ai→Bi，x）仍然是假的。然后会有a，b使得Rxab和I（A i，a）= 1和I（B i，b）= 0。但是，根据（12），有一个j使得a，b∈Kj和Rjjab。因此，由a1和T→，Ij （Ai→Bi，j）=0，wichi是不可能的。Q定理3.4 BBL 1成立。证据如所示。假设（6）成立，但（5）对所有j∈J都不成立。在3-框架K=中构造解释I。在I上，我们有，在缩写符号上，(17) [i∈I（Ai→Bi）]x（18）<$[<$j∈J（Cj→Dj）]x我们通过T得到（17），因为每个Ai→Bi在x处都是真的，通过引理3。 而且我们有(18) 因为每个C j→D j在x处都是假的。这表明（6）毕竟是无效的，是一个矛盾，结束了BBL 1的语义证明。 10Q4参考书目使用以下缩写• 澳大拉西亚逻辑• 哲学逻辑• 符号逻辑• Notre Dame Journal of Formal Logic圣母大学形式逻辑引用[1] Barendregt，Henk，Mario Coppo和Mariangiola Dezani-Ciancaglini，A filter lambda模型和类型分配的完备性，JSL48（1983），931[2] Castagna，Giuseppe，and Alain Frisch. 对语义子类型的简单介绍。在PPDP 05，ACM出版社（完整版）和ICALP 05，LNCS第3580卷，Springer-Verlag（摘要），2005中。ICALP- PPDP联合主题演讲。[10]我曾被一位裁判斥责过，他正确地坚持认为Castagna、Frisch和Benzaken在[6，2]中的贡献以及相关研究是语义子类型化主题的核心我还要感谢这些作者，2006年7月在巴黎招待我，与我谈论他们的工作，并分享他们的进一步计划文件。84R.K. Meyer/Electronic Notes in Theoretical Computer Science 171（2007）77[3] Curry，Haskell B.，一九六三年 Y.[4] Dezani-Ciancaglini，M.，A. Frisch，E.Giovannetti和Y.元滨，2002年。语义子类型的相关性，理论计算机科学电子笔记70号1，15页。[5] Dezani-Ciancaglini，M.，R. K. Meyer和Y.元滨，蕴涵的语义学，NDJFL43（2002），129-145.[6] Frisch，Alain，Giuseppe Castagna，and Véronique Benzaken. 语义子类型。LICS 02，第137-146页。IEEE Computer Society Press，2002.[7] Meyer，Robert K.，1995. 类型和布尔系统CB+，cslab.anu.edu.au/ftp/techreports/SRS/1995/TR-SRS-5-95/meyer.ps.gz网站。[8] Meyer，Robert K.，Yoko Motohama和Viviana Bono，相关逻辑的真理翻译，B。Brown和F.Lepage，编，[9] Koushik和Robert K.迈耶2005. 第一层和第二层组合子的基本相关理论，AJL3，http://www.philosophy.unimelb.edu.au/2005/2003_2.pdf，19页。[10] 作者声明：Robert K.Meyer，The Semantics of entailment III，JPL1（1972），192