数据更新的本地Hoare推理与上下文逻辑

理论计算机科学电子笔记172（2007）133-175www.elsevier.com/locate/entcs数据更新Cristiano Calcagno、Philippa Gardner和Uri Zarfaty英国伦敦帝国理工学院计算机系{ccris，pg，udz}@ doc.ic.ac.uk摘要我们提出了本地Hoare推理的数据更新，引入上下文逻辑分析结构化数据。我们应用我们的推理树更新，堆更新，和长期重写。我们关于堆更新的推理完全类似于分离逻辑的局部霍尔推理。我们关于树更新和项重写的推理只能用上下文逻辑来完成关键词：上下文逻辑，局部Hoare推理，树更新，堆更新1引言结构化数据更新在计算机系统中是普遍存在的：例如本地机器上的堆更新、硬盘上的信息存储、分布式XML数据库的更新以及通用术语重写。众所周知，处理这种动态变化数据的程序很难正确编写。霍尔逻辑是在1960年代发展起来的[10]，目的是对命令式程序进行推理这是一个重大的进步，但有一个缺点，它描述了程序是如何通过引用全球国家来运作的。2001年，Yang通过引入关于堆的局部Hoare推理迈出了另一个重要的一步。更新，而不是集中在小，局部部分的堆接触的程序在任何一个时间[18，20，11]。现在有很多关于在现实世界的应用程序中使用本地Hoare推理堆更新的活动（例如参见[2，1，3]）。到目前为止，很少有人将局部霍尔推理应用于其他形式的更新，如树更新（XML更新），也很少有人试图建立统一的理论。我们提出了本地Hoare推理数据更新，引入上下文逻辑（CL）直接推理结构化数据。CL源于两个独立的工作主体：关于堆更新的局部Hoare推理[18，20，11]，使用基于聚束逻辑（BL）[14]一般理论的分离逻辑（SL）;1571-0661 © 2007 Elsevier B. V.在CC BY-NC-ND许可下开放访问。doi：10.1016/j.entcs.2007.02.006134C. Calcagno等人理论计算机科学电子笔记172（2007）133环境逻辑（AL）[6，7]用于静态树的推理。一个自然的问题是，是否可以使用本地霍尔推理来分析树更新，使用AL作为底层逻辑。我们证明这是不可能的。可以使用CL。通过CL，我们从根本上改变了我们对结构化数据的推理方式。数据更新通常标识要替换的数据部分，删除它，并在同一位置插入新数据。使用CL，我们对数据和插入位置（上下文）进行推理。我们的局部Hoare推理遵循在[15]中首次引入的使用SL的局部推理风格。激励的想法是，原子命令倾向于以本地方式操作，只访问当前数据的一小部分，称为命令的足迹局部霍尔推理在命令行为的规范和证明中反映了命令的这种局部操作它使用小公理来指定原子命令在其足迹上的行为，并使用框架规则来指定其余数据（上下文）保持不变。我们的局部霍尔推理在很大程度上依赖于CL推理，CL推理的结构连接词具体反映了足迹与周围环境的分离。本文是我们会议论文的完整版本[4]。[4]中提出的工作集中在树更新的推理上。在这里，我们提出了一个更一般的CL帐户，并给出了一个框架，本地霍尔推理的数据更新，然后统一适用于树更新，堆更新和长期重写。上下文逻辑CL扩展了标准的命题连接词，增加了结构连接词，用于直接推理子数据。结构化应用K（P）指定数据可以被分成满足公式P的子数据和满足公式K的上下文。有两个相应的结构右伴随：数据公式KP表示，只要给定的数据被放置在满足K的上下文中，那么结果必须满足P;上下文公式PDQ表示，只要满足P的数据被应用到给定的上下文中，那么结果满足公式Q。当CL应用于堆时，结构应用和右伴随精确地对应于SL及其右伴随的结构组成。由于堆上下文具有与堆基本上相同的结构，因此存在结构崩溃。当将CL应用于树时，由于树上下文比树更复杂，因此不存在结构的崩溃。我们将看到，结构应用和伴随在AL中有类似物，而D伴随则没有。这个附加的伴随对于描述我们霍尔推理的最弱前提是必不可少的。本文给出了CL的基本定义、证明理论和模型。我们在[5]中证明了完备性。我们还给出了CL的一个扩展，称为CL0，它由一个额外的零公式0和相应的公理指定空数据。CL0具有有趣的附加逻辑结构，包括一个派生的合成公式和伴随的右伴随词，这些右伴随词概括了BL和SL的结构联结词。我们证明了CL0推理崩溃的BL推理的某些模型的一个变种我们的BL变体允许非-C. Calcagno等人理论计算机科学电子笔记172（2007）133135数据的交换结构组合，这样我们就可以分析序列。我们表明，CL0-推理是相同的BL-推理的多集和堆，其上下文具有相同的结构的数据，但更强大的序列和树，其上下文比数据更复杂。我们还研究了术语的CL-推理。虽然项可以被看作树的特殊情况，但有一个关键的区别：签名上的项没有自然的空项，并且由于函数符号的固定性而不分解为子项的组合。然而，它们可以很好地分解为上下文/子树对。因此，我们可以对术语应用CL-推理，而不是BL-推理这些例子证明了我们的CL推理的一般性。局部霍尔推理我们提出了一个框架，本地霍尔推理的命令作用于本地数据，通过描述霍尔三元组的一般解释，一般定义的本地命令，和一般的推理规则霍尔三元组的基础上，这样的本地命令。然后，我们将我们的一般霍尔推理的数据更新的三个例子：树更新，堆更新，这是完全类似的推理SL的基础上，和长期重写，以前逃脱推理使用SL。我们使用树dispose命令[n]T：= 0来说明我们的Hoare推理，该命令处理一个子树，其顶部节点由节点变量n标识。这个命令的小公理是{n[true]}[n]T：=0{0}前提n[true]是一个专门为树定义的数据公式它指定一棵树，其顶点由n给定，其子森林是未指定的。这个前提条件描述了命令的占用空间的属性，在本例中是由n标识的子树，并且是命令执行所需的最低安全条件。后置条件只描述了该命令对封装的操作结果，在本例中是由公式0指定的空树。为了将小公理推理扩展到更大的树的属性，我们使用广义框架规则来导出{K（n[true]）}[n]T：= 0{K（0）}前提条件是树可以不相交地分裂成一个子树，子树的顶点为n，上下文满足上下文公式K。本地命令和规则的定义确保了该上下文不受更新命令的约束因此，后置条件具有相同的结构，K现在应用于0。我们的例子的一般规则和小公理是完整的直线代码，我们证明了最弱的precondi- tion公理是可导出的。除了提供重要的健全性检查外，这些公理在验证工具的设计中起着基础性的作用。在我们的树处理的例子中，可导出的最弱前提公理是：{（0DP）（n[true]）}[n]T：=0{P}这个最弱的前提条件简单地说明了树可以被分成一个顶部节点为n的子树，以及一个当空树被放入136C. Calcagno等人理论计算机科学电子笔记172（2007）133洞虽然可以用AL代替CL来定义小公理和一些框架规则，但不可能定义最弱的先决条件。我们关于堆更新的局部Hoare推理与[15]中使用SL给出的相同。事实上，我们关于树更新和堆更新的Hoare推理也非常相似。这种相似性不仅发生在小公理和最弱前提公理上，而且还发生在证明最弱前提公理是可导出的层次上。与我们的霍尔推理的比较项重写是不那么直接，因为项重写的性质是不同的，从我们的语言树和堆更新。然而，很明显，同样的一般原则适用于具体化和证据层面。我们的霍尔推理似乎是强大的更新语言选择的风格。事实上，我们的例子表明，它可能会发展一个一般的理论，当地霍尔推理数据更新。致谢我们感谢Peter O'Hearn、Pino Rosolini和Hongseok Yang提出的深刻见解。加德纳是由皇家工程学院/微软研究剑桥高级奖学金支持。Calcagno得到了EPSRC高级奖学金的支持。Zarfaty获得了EPSRC DTA奖的支持。2上下文逻辑我们给出了CL的基本定义，它的证明理论和模型（2.1节）。我们扩展了这个基本CL，以包括用于指定空数据的附加零公式（第2.2节），这提供了有趣的附加逻辑结构和与BL的比较（第2.2.2节）。 最后，我们研究了CL推理在结构化数据的四个示例模型中的应用：序列、多集、树和项（第2.3节）。2.1基本上下文逻辑CL由P表示的数据公式和K表示的上下文公式组成。这些公式是由标准的命题连接词和不太熟悉的结构连接词构成的，用于直接分析数据和上下文结构。定义2.1（CL公式）CL公式集由数据公式P和上下文公式K的不相交集合组成，它们由以下语法构造数据公式P：：= K（P）|K-P结构式PP|欧元/英镑|假布尔加法公式C. Calcagno等人理论计算机科学电子笔记172（2007）13313711上下文公式K：：= I|P D P结构式K K |K|假布尔加法公式我们有时写P CL和K CL来强调公式集来自CL。我们使用经典CL，因为经典逻辑是分析特定模型时的标准选择。这也将是有趣的研究直觉CL。关键公式是结构公式K（P），KP，P1D，P2和I.的应用公式K（P）指定给定的数据元素可以被分割成一个满 足 K 的 上 下 文 应 用 于 满 足 P 的 数 据 。 例 如 ， 如 果 我 们 定 义 上 下 文 公 式True<$ False，则公式True（P）表示某些子数据满足属性P。下面两个公式都是应用的（右）伴随公式公式K a P被给定的数据满足，如果每当我们将数据插入满足K的上下文，则结果满足P。例如，公式（Truea P）指出，当数据放在任何上下文中时，满足属性P。同时，P1DP2是一个关于语境的陈述.如果无论何时我们在上下文中插入满足P1的数据，则结果满足P2，则给定的上下文满足。给定导出的数据公式true <$false，上下文公式（true D P2）表明，无论将什么数据放入上下文洞中，结果数据都满足属性P2。 这个伴随对于表示更新命令的最弱前提条件是必不可少的（第3节）。 上下文式I指定一个上下文等于空上下文。我们给出了一个简单的希尔伯特式证明理论，遵循[17]中BL的风格结构算子的公理和规则表明KaP2和P1dP2是K（P1）的右伴随，I是应用单位元定义2.2（CL-证明理论）希尔伯特式CL-证明理论包括布尔加法连接词（包括cut）的标准公理和规则，以及以下结构连接词的公理和规则PEPI（P）K（P1）P2KKP1DP2K（P1）P2P1PKP2K1K2P1P2K1（P1）PK2（P2）KKP1DP2PJP1K（PJ）P2P1PKP2KJKKKJ（P1）PP2我们将一些抽象的概念简化为抽象和抽象的概念，并将一些抽象的概念定义为L，以明确地引用CL证明理论。对于数据和上下文公式，我们都使用标准的经典公式：对于数据公式，使用true、PP和PP;138C. Calcagno等人理论计算机科学电子笔记172（2007）133对于始终为真的上下文公式为真。我们还使用以下衍生的结构式。定义2.3（CL衍生公式）• CUPTrue（P）指定某处属性 P持有 QP（它指出，在任何地方，性质P都成立。• P1<$P2<$（P1D <$P2）指定存在满足性质P 1的某个数据元素，使得当将其放入给定上下文的洞中时，结果数据满足P2。• K（P2<$（K<$P2）指定存在满足属性K的上下文，使得当给定的数据元素被放入洞中时，结果数据满足P2。预分配中的或优先级为：，{a，D，（，这里给出的简单表示强调了和D的右伴随性质.在[5]中，我们证明了这个证明理论等价于标准的经典ML-证明理论加上一组额外的CL特有的行为良好的公理。这个替代ML-表述强调了派生的连接词and（而不是伴随词Dand。我们几乎没有研究过CL-证明理论。根据BL [17]的类似结果，应该可以证明一个截消结果此外，辛普森我们给出了一些基本性质的有效性：分布在应用程序和连接部分分布，结果典型的这种风格的逻辑推理的结构伴随D，和应用程序之间的相互作用，而像标准的前件式的添加剂连接;和我们的导出某处和无处不在的模态数据引理2.4（有效性的基本性质）n-分配性（K1<$K2）（P）E <$PK1（P）<$K2（P）K（P1）P2）EPK（P1）K（P2）自洽分布率（K1<$K2）（P）<$PK1（P）<$K2（P）K（P1）PK（P1）K（P2）方法-ponen结果（P1DP2）（P1）重复PP2重复结果（P1）K（KP）PK（true）P2-Truee（P1）-P（P1-P2）（P1）PK（true）PK（K（P））T-axiomsPPQP►PQPPC. Calcagno等人理论计算机科学电子笔记172（2007）133139连接词“”只是部分地分布，因为左边指定将数据分割成上下文和子数据，而右边指定两个不需要重合的分割。虽然ML的T-公理是可导出的，但4-公理指出QQP≠QP是不可导出的;参见例2.6中的Step模型以获得反模型。在Zarafty连接词对应于上下文成分，以及两个对应的右伴随词。4-公理在这个扩展中确实成立，某处模态更接近于我们的结构化数据直觉。我们现在定义CL-模型和满意度关系，它们对于CL-证明理论来说是合理和完整的。定义2.5（CL模型）CL模型M od是元组（D，C，ap，I），使得(i) D和 C是集合;(ii) ap∈（C × D）× D是一个关系，称为应用：我们用符号ap（c，d1）=d2表示（（c，d1），d2）∈ap;(iii) I_i_C充当ap的左恒等式：即，• d∈ D，di∈I，DJ∈ D. inti=J;• dj ∈ D，dj∈ I. ap（i，d）= DJ意味着d = DJ。我们通常称D为数据集，C为上下文集，因为我们的激励示例的形式。当然，有些模型并不适合这种结构化数据的直觉。示例2.6[示例CL模型]• M onD=（D，D，·，{e}）其中D是具有monoidal算子·的集合：（D× D）→D且单位e∈ D;此外，D上的部分=（D，D，·，{e}）类似于D上的M，除了·是一个偏幺半群。这些模型对应于BL-模型（定义2.26），并且CL-推理对这些模型而言坍缩为BL-推理（定理2.29）。• 这是PartMonD的一个新的x示例，其中H=N+-finN是指不属于这些应用的有限的partiafia l函数的集合。N+=N−{0}中的doman不包含0，因为它是为nil值保留的。堆组合h·h，对于堆h，h J∈ H，是函数并，并且仅当dom（h）= dom（h j）=dom（h J） 时 定 义 。• 其中，T是从签名f中的r元函数符号f：r构造的项的数据集，C是对应的项的集合。上下文，ap表示上下文对术语的标准应用，并且表示空上下文。• Seq A=（SA，CA，ap，{ }）其中SA是由字母表A中的元素构造的序列的集合，CA是对应的上下文的集合，ap和是T的上下文;设M ult A表示由多集合构造的类似CL模型。• 树A=（TA，CA，ap，{}）是T A的一个例子，在术语和上下文上具有额外的等式关系。 签名A是集合0={0}，1=A，其中Adenotenodeabels，并且2={|}，wheeererécidedenotesarityi的函数符号。我们用符号t|t J为|（t，t J），a[t]对于a（t），a ∈A。 项被认为是对等式关系取模，140C. Calcagno等人理论计算机科学电子笔记172（2007）133根据公理0|t t，t |t J t J|t，（t |t J）|t JJ t|（t J|t JJ），并由功能符号的明显结构规则封闭。上下文的集合CA被类似地构造，在上下文上具有类似的等式关系• 位置TreeN类似于TreeN，其中h0={0}，h1=N，h2={|}。 此时，集合N表示唯一节点标识符的集合，并且|因此对于部分堆组成来说是部分的。 我们将用这个模型来说明我们的想法关于树更新• RelD=（D，P（D × D），ap，{ i}）其中D是任意集合，P（D × D）表示D上的二元关系的集合，ap是关系应用，i是恒等关系;还有F unD=（D，D → D，ap，{ i}）其中D → D是从D到D的全函数的集合，ap是函数应用，i是恒等函数。• Step=（N，{0，1}，+，{0}），其中，在一个位置处，该位置是一个整数，该位置是{0，1}，该位置是一个整数，该位置是一个整数，并且该位置是零。这个模型证明了ML的4-公理是不可导的，因为数字2满足QQ0但不满足Q0。•M1+M2=（D1<$D2，C1<$C2，ap，I1<$I2）其中M1=（D1，C1，ap1，I1）且M2=（D2，C2，ap2，I2）是CL-模型，对任意的ci∈Ci，dj∈Dj，ap（ci，dj）=api（ci， dj），如果i=j，否则定义定义2.7（CL-满意度关系）给定CL-模型M od=（D，C，ap，I），CL-满足关系CL包含关系Modd，d∈P P和Modd，c∈KK，其中d∈D，c∈C，P∈P和K∈K。这两种情况是通过归纳公式的结构来定义的：布尔加法连接词的情况是标准的;结构连接词的情况是Mod，dc∈C，DJ∈D. ap（c，DJ）=d<$Mod，c<$K K<$Mod，DJ<$PMod，d<$PKPi<$<$c∈C，DJ∈D. Mod，c<$K<$ap（c，d）=dJ<$Mod，dJ<$PPMod，cKIi c∈IMod，c ∈KP1DP2i∈D，dJ∈D. Mod，d<$P1<$ap（c，d）=dJ<$Mod，dJ<$P2我们忽略子项P和K，并将CL写为CL-满意关系。在第2.3节中，我们深入探讨了SeqA，MultA和TreeA的满意度关系，并给出了许多例子来说明CL推理在这些模型上的表达能力。定义2.8公式P或K对给定模型M=（D，C，ap，I）有效，记为MP或MKK，如果它是由模型中的所有数据定义的或不存在的：MPd∈D。M，dM<$K K<$c∈C. M，c定理2.9（CL-可靠性和完备性）CL-证明理论是C. Calcagno等人理论计算机科学电子笔记172（2007）133141关于CL-满意关系的健全和完整你是我的朋友。（MPP）TrueK惠M. （MKK）我们在[5]中使用CL的结构连接词作为模态逻辑（ML）中的模态的解释来证明完备性。这种解释并不直接，因为它使用结构伴随词的否定词作为基本连接词.我们提出了额外的ML公理，这些额外的CL模态，以提供一个精确的对应关系之间的原始CL介绍和ML解释。这些公理表现良好，因为它们满足我们应用ML（Sahlqvist定理）的一般完备性结果所因此，我们证明了CL-证明理论是健全的和完整的CL-模型的集合我们对BL也有类似的结果这项工作遵循Calcagno和Yang的杰出工作，他们在未发表的工作中从第一原理证明了BL和CL的完备性他们还扩展了他们的结果，以显示CL模型的完整性，其中应用程序是一个函数;由于结合性，他们的技术打破了BL。我们在这里使用关系定义，将某些CL-模型与BL-模型联系起来（定理2.29）。2.2上下文逻辑与零请注意，例2.6中给出的许多CL模型描述的结构化数据都有一个对应于空数据的自然元素。在这里，我们用零公式0和额外的公理扩展CL，以捕获空数据的一些自然属性由此产生的逻辑，表示为CL0，具有有趣的逻辑结构，并允许与BL精确对应（第2.2.2节）。定义2.10（CL 0-公式）CL 0-公式的集合由定义2.1中的数据和上下文公式加上一个额外的数据公式0组成，称为零公式。定义2.11（CL 0-证明理论）CL 0-证明理论扩展了定义- 第2.2节零公理：TrueK0truePTrue（0）0PK0DP0D0KI这些零公理陈述了关于被视为空数据的数据元素的直观性质他们的对话都是可推导的。第一个公理指定了一个总体条件，即每个上下文都可以应用于空数据。回想一下，我们有一些示例模型，其中应用程序不是完全的，所以这个属性是不可导出的。第二个公理是满射性条件，它规定所有数据都可以分割成上下文和空数据。第三条公理指出，当应用于上下文时，所有零元素都以类似的方式行为第四个公理标识上下文0D 0，当应用于空数据时返回空数据，其中空上下文I。虽然我们相信这些零公理描述了空的重要性质，142C. Calcagno等人理论计算机科学电子笔记172（2007）133数据，我们不知道我们是否已经抓住了空数据的全部本质。对于示例，不允许将空数据分割成上下文和非空数据。我们知道这个性质是不可导的，因为它的逆在例2.13之后给出的关于Da的CL0模型M中成立。我们选择只使用给定的零公理，因为它们已经足以证明一些有趣的性质。定义2.12（CL0-模型） CL0-模型是一个元组（C，D，ap，I， 0），其中(i) （C，D，ap，I）是CL-模型;(ii) 0天;(iii) 投影p：C → D定义为：p（c）= d惠o ∈0. ap（c，o）= d是全满射函数;(iv) c∈ C，c ∈ 0。p（c）= o <$c ∈ I.投影函数p将C中的每个元素映射到D中的唯一元素，通过将其应用于零元素。投影函数是满射的，这意味着每个数据元素都有一个零元素作为子元素。条件（iv）在I和0之间建立了强联系：根据定义2.5，我们有p（i）∈0，i∈I;由条件（iv），我们也有p−1（0）<$I对所有o∈0。例2.13[例CL0-模型]例2.6中CL模型的以下扩展都是CL0-模型。• D上的M=（D，D，·，{e}，{e}）;对于D上的部分M类似。• 将空函数作为零元素的堆• Seq A、Mult A、Tree A和Loc Tree N，其中空序列、空多重集和空树作为适当的零元素。• M od1+M od2=（C1<$C2，D1<$D2，ap， I1<$I2， 01<$02）其中M1=（C1，D1，ap1， I1， 01）和M2=（C2，D2，ap2， I2， 02）是CL0-模型，ap在例2.6中定义。具有么半群Da={ a， e}且a· a= e的Da上的CL0-模型M说明我们还没有捕捉到关于空数据行为的所有直觉。对于示例，这表明无法使用历史的C L 0 -预处理来确定尾mt0P<$（True（<$0））。新方法是对0+t，（n + 1）+（<$i）（n+）和nn+<$i（n+1）+n∈N的可导性。在CL0-模中，例如，在序列模中，对于数据的大小，其本身为多个计算：对于x个元素，对于多个n+个具有至少n个元素的特定序列，以及公式n个具有至少n个元素的特定序列，n个元素。然而，M onDa模型表明，这种分析并不总是可能的。CL模型步骤没有零集，因为从上下文到数据没有满射函数。并且，具有特征集f={f：1，g 1：0，g2：0}的CL模型T_（？）假设0不包含g2（或g1），则g2不能在p的反像中C. Calcagno等人理论计算机科学电子笔记172（2007）133143满射性;然而，g1和g2不能都在0中，因为p（）= g1和p（）= g2，与函数p的良构性相矛盾。请注意，当T_r_J={f：1，g：0}时，T_r_j是一个C_L0-模，其中t_r_j={g：0}。CL-模RelD没有零集，因为处处未定义的关系与投影功能F unD也没有零集：唯一可能的选择是投影为函数的单例{d}，但它与条件（iv）相矛盾，因为恒等式不是唯一将d映射到自身的函数定义2.14（CL 0-满意度关系）设Mod0=（D，C，ap，I，0）为任意CL 0-模型。CL 0-满意关系扩展了定义2中给出的关系Mod0，d P和dMod0，cK。7withMod0，d<$P0i <$d∈0定理2.15（CL 0-可靠性和完备性）CL 0-证明理论对于CL 0-满意关系是可靠和完备的.至于Thm。2.9，完备性可以从第一原理证明，或者通过使用CL0的ML解释并诉诸Salqvist2.2.1导出公式我们探讨了一些导出的CL0-公式。首先，我们推导出数据上的二元-连接符及其伴随的右伴随，它们是和−的广义版本从BL和SL。我们还表明，一个自然的嵌入CL0模型的投影函数的关系，建议嵌入/投影公式与有趣的逻辑结构。定义2.16（导出的CL-公式）我们导出以下CL0-公式：P1P2（0DP1）（P2）P1−P3（0DP1）P3P2−P3<$（<$（P2DP3）（0））导出的公式P1P2指定给定的数据可以被分成满足属性P 2的子数据和具有属性的上下文，当零元素被放入孔中时，满足属性P1。例如，公式0指定给定的数据可以分成两个不相交的非空部分。 连接词是一般来说既不是交换的也不是结合的：例如，它在序列或树模型中不是结合的或交换的;它在堆模型中。因此，我们 第一个伴随P1−P3是直接的。 它指出只要应用于零元素的上下文满足P1，则上下文应用于给定的数据元素满足P3。第二个右伴随更复杂。 它指出，每当满足P2的数据替换给定数据的空子数据时，结果数据满足P3：对于树，满足P2的数据可以插入到叶子或任何节点;对于序列，这些数据可以插入到序列中的任何点;对于堆，只要堆地址没有冲突，数据就可以扩展堆。我们假设约束力优先，144C. Calcagno等人理论计算机科学电子笔记172（2007）133，引理2.17（公式的性质）(i) P−和P−分别 是P和PP的右伴随：即，P1P2P3P1P2−P3P1P2P3P2P1−P3(ii) 零式0是的左右单位：即P 0惠P惠0P。我们将看到，这些公式与CL0模型中的一个可导关系定义2.18（导出的关系式）关系式（D × D）×D定义为：n={（（d 1，d 2），d 3）|c∈ C，o ∈ 0。 d 1= ap（c，o）<$d 3= ap（c，d 2）}我们让d 1<$d 2表示集合{d 3|（（d1，d2），d3）∈ n}.对于D上的CL0-模型M（以及D上的部分M），关系是一个（部分）函数，对应于·。对于模型Tree A，关系t 1和t2更复杂，其中t 1和t 2描述了通过将t 2插入到sidet 1中的任意位置而获得的树的集合：对于xample，（a1[0]|a2[0]）b[0]={a1[b[0]]|a2[0]，a1[0]|a2[b[0]]，a1[0]|第2页[0]|b[0]}。引理2.19（CL0-satisfaction for a-formulations）给定 CL0-modelM od，在数据上的a-连接符和a-算子之间存在直接联系：M，d <$P1<$P2惠<$d1，d2∈D. （d∈d1<$d2<$M，d1<$P1<$M，d2<$P2）M，d <$P1 <$−P3惠<$d1，d3∈D. （d3∈d1<$d <$M，d1<$P1<$M，d3<$P3）M，d <$P2−<$P3惠<$d2，d3∈D. （d3∈d<$d2<$M，d2<$P2<$M，d3<$P3）我们还推导出投影和嵌入公式，这又有有趣的逻辑属性。我们首先证明了在CL0-模型中存在一个自然的嵌入关系。定义2.20（CL 0-嵌入关系）给定CL 0模型调制解调器0=（C，D，ap，I， 0），嵌入关系e：D× C定义为：e（d，c）当且仅当p（c）= d。对于{c ∈ K：e（d，c）}，我们写e（d），表示当应用于零元素时给出d的上下文的集合。关系e不一定是函数：例如，在树模型中e（b[0]）={b[ ]，b[0]|}。 对（e，p）是一个嵌入-投影对：即，d ∈ D。{p（c）|c ∈e（d）}={d}. 它们也给了我C. Calcagno等人理论计算机科学电子笔记172（2007）133145和0：p（i）<$0对所有i∈I和e（o）<$I对所有o∈0。 由于（e，p）-对是模型中的一种自然结构，我们研究了相应的CL0-公式.定义2.21（导出的e，p-公式）我们定义以下导出的CL0-公式：投影公式KpK（0）嵌入公式Pe0天P投影公式Kp指定给定的数据是满足属性K的上下文的投影，并在孔中放入零元素。嵌入公式Pe指定，只要在洞中放入零元素，给定的上下文就满足属性P引理2.22（e，p-公式的CL0-满足）给定 CL0-模型M od，e，p-公式和数据上的嵌入投影对（e，p）之间的联系由下式给出：M，d <$PKp惠<$c∈C. p（c）=d<$M，c<$KKM，c ∈KP e惠d∈D. c∈e（d）<$M，d<$PP引理2.23（e，p-公式的性质）下列蕴涵是可导出的：P Pp<$（Pe）EK（<$P）e0eKI第一个蕴涵由定义2.11中给出的第二个和第三个公理得出，并且对应于（e，p）是一个嵌入-投影对。第二个蕴涵指定否定分布在（）e上，或者等价地（）e有一个由<$（（<$）p）给出的右伴随。 第三个蕴涵规定（）e将0提升到I，并且与定义2.11中的第四个公理相一致。引理2.24如果我们用引理2.23中的蕴涵替换定义2.11中给出的零公理，那么零公理是可导的。这些结果表明，我们最初对零公理的选择是自然的。它们还表明，我们还没有完全理解嵌入-投影公式的意义。在[21]中，Zarfaty进一步探索了这一点，提出了CL0的另一种表示，包括上下文组合、伴随和这些嵌入/投影公式。2.2.2与Bunched Logic的我们提出了BL [16]的（一个变体），它的模型和满意度关系，并将其与CL0进行比较。我们使用符号和−表示乘法合取及其伴随，而不是标准的和−表示。我们为定义2.16中给出的CL0的广义版本保留了和−。我们的标准146C. Calcagno等人理论计算机科学电子笔记172（2007）133BL并不要求序列是可交换的，因为我们的一个关键示例模型是序列，其中序列表示级联。定义2.25（BL公式）BL公式PBL的集合定义为：P：：= 0 |PP|P−P|P-P结构公式PνP|欧元/英镑|假布尔加法公式关键公式是结构式0、P1<$P2、P1<$−P2和P1− <$P2。零公式0指定空数据。合成公式将给定的数据分成两部分：第一部分满足P1，第二部分满足P2。与原始的BL不同，我们有两个右伴随，因为n是非交换的：P1n −P2规定，只要满足P1的数据被放置在给定数据的左边，那么结果就满足P2;另一个伴随P1n −P2将数据放置在右边。这种区别在堆模型中没有影响，但在序列模型中很重要与CL中一样，我们定义伴随的否定项为P1−·P2<$（P1− <$$>P2）和P1·−P2<$（P1<$− <$P2）。定义2.26（BL-模型）BL-模型M od是元组（D，·，e），使得(i) D是集合;(ii) ·（D× D）×D是一个结合关系：我们使用符号·（d1，d2）= d3对于（（d1，d2），d3）∈ ·;(iii) eD充当·的左标识和右标识：即，• d∈ D，DJ∈ D. ·（e，d）= d，J• d∈ D，DJ∈ D.·（d，e）= d，J• dj ∈ D，dj∈e. ·（e，d）= DJ或·（d，e）= DJ意味着d = DJ。注意，任何BL模型M=（D，·，e）可以提升到CL0模型MBL=（D，D，·，e，e），其中导出的关系2.18与·一致。事实上，我们将看到，对于这样的模型，CL0-满意关系坍缩为BL-满意关系（定理2.29）。我们强调了堆、序列的特定BL模型和树木，因为我们将在本文中使用它们。 将这些BL-模型与例2.6中给出的类似CL-模型进行对比，后者也强调语境结构。例2.27[一些BL模型]• SeqA=（SA，·，{0}），其中DA是集合A中元素构成的序列的集合，·是序列拼接，0是空序列，M ultA表示由多个集合构成的类似CL0-模型• TreeA=（TA，|，{0}），其中TA 是实例2中的接收器的集合。六，|是树的组成，0是空树。• 堆=（D，·，{e}）其中D，·和e如例2.6所示。注意序列SeqA的CL0模型和BL模型SeqA的CL提升之间的差异：在CL0模型中，上下文可以被认为具有C. Calcagno等人理论计算机科学电子笔记172（2007）133147形式s1· ·s2和应用用一个序列代替洞，在BL-模型SeqA的CL0-提升中，上下文集是序列集的同构拷贝，应用对应于序列的连接类似的差异发生在树木上。相比之下，CL0-模型MultA完全对应于BL-模型MultA的CL0-提升，这是由于多集并的交换性。这种相似性也发生在堆模型上。定义2.28（BL-满意关系）给定BL-模型M od=（D，·，e），BL-满意关系满足下式：Mod，d∈BLP，其中d∈D，P∈ PBL。如前所述，它是通过公式结构的归纳来定义的，结构连接词的情况由下式给出：Mod，dBL0我的d ∈eMod，dBLP1P2我的d1，d2∈ D.·（d1，d2）=dd1，d3∈D。·（d1，d）=d3d2，d3∈D。·（d，d2）=d3<$Mod，d2<$BLP2<$Mod，d3<$BLP3我们假设、−和−具有与、−和−相同的绑定优先级。希尔伯特风格的BL-证明理论由与CL-证明理论（定义2.2）类似的规则组成，并增加了一个关于结合性的公理。至于CL，我们可以从第一原理证明BL的完备性结果，或者与CL-情形不同，我们不知道如何将这个结果扩展到BL-模型，仅限于那些·是函数的模型。困难来自于·的结合性，这是一个已知的问题。定理2.29（坍缩到BL）给定BL-模型Mod BL=（D，·，e）和相应的CL 0-模型Mod CL=（D，D，·，e，e），我们定义平移||P：PCL→ PBL，||K：KCL→PBL从CL 0-公式到BL-公式的 转换|BL：P BL → P CL从BL -公式到CL -数据公式，使得|BL: PBL→ PCLfrom BL-formulae to CL-data formulae, such that• 对于d∈ D，P∈ PCL和K∈ KCL，MdCL，d CLP惠MdBL，d BL|P|PModCL，d CLK惠ModBL，d BL|K|K• 对于d∈ D和P∈ PBL，ModBL，d BLP惠ModCL，d CL|P|BL148C. Calcagno等人理论计算机科学电子笔记172（2007）133证据翻译是通过归纳公式的结构来定义的：加法连接词的情况遵循连接词的结构;我们给出了结构连接词的情况。对于结构情况，从CL0-公式到BL-公式的转换是：|P = 0|我|K = 0|K= 0|P = |K|K|P|P |P D Q|K=|P|P − N|Q|P|P|P=|K|K −|P|P |P对于结构情况，从BL公式到CL数据公式的转换为：|BL = 0 |BL= 0|BL=|P|BL|Q|BL|BL|BL=|P|BL −|Q|BL|BL|BL=|P|BL −|Q|BL|BL在证明之后，对公式的结构作了简单的归纳。Q回想一下，多重集和堆的CL0-模型与它们类似的BL-模型的CL0-提升是相同的。这个定理表明，对于这些模型，CL0-推理和BL-推理是一致的.2.3CL的应用本文研究了CL-推理在序列、多集、树和项上的四种应用：序列提供了一个简单的例子来说明CL0-推理和BL-推理是不同的;多集提供了一个CL0-推理和BL-推理相同的例子;和术语提供了BL推理不可能的示例。在每种情况下，应用程序都涉及使用公式扩展CL公式，用于分析数据的特定结构和模型产生的上下文。在这里，我们使用与模型相关的特定常数;在第3节中，我们还使用变量和量化。2.3.1序列由字母表A生成的序列的CL是CL0，由特定连接词扩展，用于特定分析例2.6中给出的CL0附加连接词指定了一元序列a ∈A，并分析了序列上下文的附加结构。我们写s1·s2来表示两个序列s1和s2的连接，s1· ·s2表示序列s1和s2之间有上下文洞的上下文。定义2.30（用于SeqA的CL）应用于序列模型SeqA的CL，表示为CLSeqA由通过扩展CL0-公式构造的CLSeqA-公式组成C. Calcagno等人理论计算机科学电子笔记172（2007）133149由定义2.14中的语法归纳定义，并有以下附加情况：上下文公式K：：= P。.P特定上下文公式数据公式P：：= a 具体数据公式a ∈ACLSeqA-满意度关系将CL0-满意度关系（定义2.14）扩展为其他情况：SeqA，cKP1. . P2i∈s1，