高阶分离逻辑中的模型与持久谓词的研究

可在www.sciencedirect.com在线获取理论计算机科学电子笔记336（2018）57-78www.elsevier.com/locate/entcs关于高阶分离逻辑的模型AleBizjak1LarsBirk edal2丹麦奥胡斯大学计算机科学系摘要我们展示了如何从范畴逻辑的工具可以用来给高阶分离逻辑的子逻辑的所谓的持久谓词满足高阶逻辑的通常规则的模型的一般帐户。分离逻辑的模型基于资源的概念，部分交换幺半群，持久谓词可以使用模态定义。我们分类良好的持续谓词的内部运营商的部分交换幺半群的资源方面的子逻辑。我们进一步展示了如何一般的结构可以用来恢复虹膜，一个国家的最先进的高阶分离逻辑与保护递归谓词的模型。保留字：分离逻辑，模型，模态1介绍近年来，我们看到了许多高阶分离逻辑的变体模型，例如，[4、14、6、3、1、16、10、9、11]。分离逻辑是一种子结构逻辑，所有的模型都基于某种资源概念。最初，资源是堆碎片，逻辑中的谓词描述堆的集合。例如，points-to谓词l<$→3描述了在lo阳离子处包含值3的那些堆L.后来，使用了更详细的资源概念，因为它们允许更强的规范，并且可以用来跟踪程序代码中没有明确给出的有了这些更丰富的资源概念，人们经常注意到，能够挑选出并使用“持久”谓词是非常有用的。持久谓词特别是可重复的（意思是P * P惠P），并且它们服从更标准的（不是子结构的）逻辑规则。实现这一点的一种方法是通过模态Q（发音总是），它是一种类似于必需品的模态，遵守的规则类似于bang模态所遵守的规则！线性逻辑。这样的1电子邮件：abizjak@cs.au.dk2电子邮件：birkedal@cs.au.dkhttps://doi.org/10.1016/j.entcs.2018.03.0161571-0661/© 2018作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。58A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57模态还赋予了使命题在逻辑内部持久化的能力，这显著地增加了它的表达能力，正如在以前的工作中所证明的那样[9，11]。持久谓词的例子是简单的事实，如值相等和Hoare三元组。霍尔三元组是程序（部分）的规范。它们描述了程序需要某些资源（前提条件）并在执行后确保某些属性（后置条件）的知识因此，这些知识应该是可重用的，在这个意义上，在验证一个更大的程序时，我们可以使用子部分的指定多次子部分出现。在复杂逻辑中，特别是在并发分离逻辑中，如Iris[10]，还有许多其他持久谓词，例如，不变量，它描述了某个谓词对某个共享内存的知识。这些知识应该在共享内存上运行的程序的不同部分之间共享，因此不变量应该是可重复的。因此，在高级分离逻辑中，区分具有某种形式的所有权的谓词（suchchasl→3）和持久谓词（例如Hoare三元组和不变量）是有用的，它们不涉及任何排他性所有权，而是表达知识，即，可以自由复制。Q情态可以用来去掉谓语中的逻辑，即，QP包含P中那些可复制的资源 这种能力例如，用于定义虹膜中的Hoare三元组[10，9，11]，也用于建模分离逻辑中的直觉类型[15，18，12]。在本文中，我们展示了如何从范畴逻辑的工具可以用来给高阶分离逻辑模型的一般帐户与持续谓词的子逻辑。我们专注于分离逻辑中使用的基本规则和基本连接词，而不考虑所谓的规范逻辑，即，Hoare三元组，以及不变量等概念，以及特定分离逻辑的规则。我们的目标是展示如何以一般的方式对逻辑的基本部分进行建模，以便在未来的工作中，我们可以将精力用于对手头的逻辑的特定部分进行建模。我们利用完备Heyting代数的标准概念来建模标准高阶逻辑，并利用完备BI代数的概念[4]来建模高阶分离逻辑。 我们展示了如何构建这样的代数的基础上的一个模型的资源，形式化的一种部分交换幺半群，和不同的方式挑选出的幂等（可重复）幺半群元素。我们表明，我们的抽象框架是一般性的，足以涵盖模型，其中还包括一个模态的推理保护递归谓词：通过一个简单的变化的环境类别，从集到拓扑的树，我们恢复了步骤索引的概念，资源模型用于模型虹膜[9]，一个国家的最先进的高阶分离逻辑与保护递归谓词。概述在第2节中，我们回顾了BI hyperdoctrine的定义以及如何使用资源模型来构建BIhyperdoctrine。在本节的最后，我们A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5759这表明，一般来说，不可能使用行为良好的模式准确地在第3节和第4节中，我们研究了获得持久谓词逻辑的条件。我们给出了两个不同的构造，一个是基于幂等资源，另一个是基于资源上的内部算子。对于第一个构造，我们得到一个在某些逻辑联结词下封闭的子逻辑，但一般来说不是全部。特别是，在环境逻辑的泛量化下，它可能无法闭合对于第二种构造，我们得到一个在环境逻辑的所有标准逻辑联结词在第五节中，我们证明了任何只在可重复谓词上的，并且在所有标准连接词下封闭的子逻辑必须具有第四节中考虑的形式。我们进一步表明，第4节中考虑的子逻辑都是最多的表达 与第3节中考虑的基于幂等元的逻辑一样，我们给出了后一种逻辑在泛量化下封闭的充要条件。这些条件是根据资源幺半群的幂等元的结构来表述的。使用内部算子的方法与Pottier [15]的核心算子密切相关（尽管Pottier对他的核心概念有一些额外的要求）;以及Iris [9]中使用的核心算子。因此，在第5节中，我们表明，只要我们希望逻辑中有一个行为良好的模态，迄今为止描述的模型不直接支持保护递归预测，如在Iris[10，9]和其他逻辑中使用的，例如Appel [1]。为了支持保护递归谓词，Iris逻辑的类型和术语使用树的拓扑的子类来建模[9]。Iris模型的构造基于一种称为完全度量资源代数（CMRA）的步进索引资源模型。CMRA的技术定义，在定义6.5中回顾，可能看起来像是 有点特别在第6节中，我们证明它实际上是规范的，因为它可以被理解为部分交换幺半群，只是在一个不同的环境范畴。此外，我们还证明了Iris谓词的模型[9]可以通过使用树的topos作为环境范畴来恢复，其中第3节和第4节中的构造被执行。2BI-代数与BI-超理论在本节中，我们首先想起BI-超理论的概念，这是高阶分离逻辑模型的范畴论定义[4]。为了简单起见，我们专注于所谓的规范提出的BI-hyperdoctrines。回想一下，一个超理论[13]是一个carbohydrate闭范畴C和一个类属对象Ω，对于每个对象X∈C，一个在hom集HomC（X，Ω）上的偏序的选择满足以下性质：• HomC（X，Ω）是X的完备Heyting代数.• HomC（f，Ω）：HomC（X，Ω）→HomC（Y，Ω）是一个完备的Heyting代数homo-60A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57C中所有f：Y→X的态射。• 对于任意一对对象X，Y∈C，函数HomC（π，Ω）：HomC（X，Ω）→HomC（X×Y，Ω）有左和右伴随，另外满足Beck-Chevalley条件。完备BI-代数[4]是一个完备的Heyting代数，它还具有封闭的monoidal结构（*，−*，I）。一个BI-超主义是一个超主义，使得对于每个X，集合HomC（X，Ω）是一个完全BI-代数，HomC（f，Ω）是一个完全BI-代数同态。为了使用超主义来建模逻辑，我们将逻辑的类型和术语解释为C的对象和态射，而谓词被解释为HomC（X，Ω）的元素，其中X是谓词的域（的表示）构造超教义的一个规范方法是从C中的内部完全Heyting代数H（这要求C具有足够的结构来表达什么）一个完整的Heyting代数是）。Heyting代数H是一般对象，HomC（X，H）上的阶是逐点的，所有的完全Heyting代数运算也是如此。类似地，构造BI-超理论的一个规范方法是从内部完备BI-代数。操作再次逐点给出。众所周知[4]如何在BI- hyperdoctrines中建模高阶分离逻辑。因此，在上述规范构造的基础上，本文的剩余部分将主要讨论完备Heyting代数和完备BI-代数的构造和研究。2.1完备BI-代数构造BI-代数的一个非常普遍的方法是从一个部分交换幺半群M中构造一个前序≤，它以一种合理的方式与运算相互作用，我们在下面精确地说明M的向上闭子集的集合，记为P↑（M），是一个完备的BI-代数。通过改变么半群上的预序，我们可以得到不同分离逻辑的模型。特别地，如果序是扩张序（也称为可除性预序），则我们得到一个所谓的可除性分离逻辑的模型，它具有弱化规则p*q≠p，对于所有命题p，q。 最近的逻辑，如iCAP[16]，Iris[10，9，11]的各种版本都是这样的逻辑。另一方面，如果我们取离散前序，即，平等，我们得到一个模型，不验证弱化。这种逻辑允许对资源进行更精确的控制。例如，它允许人们表达堆为空的属性，例如，在某些逻辑[1]中用于逻辑，例如，保证被证明正确的程序不会泄漏内存。下面的大多数构造都适用于任意的预序和部分交换幺半群。在各种陈述中，我们指出了关于前序的附加假设如何导致某些附加规则的有效性A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57613∼∧ ∩ ∨∪i∈Ii∈Ii∈Ii∈I定义2.1本文中的序部分交换幺半群是一个结构（M， ·， E， ≤） ，满足 · ：M×M~M是一个部分函数，E∈M是满足下列公理的单位集m· n n· m（m·n）·km·（n·k）m∈M，m∈ M，e∈ E，m·e定义为m·em最后，≤是M上的一个预序（一个自反传递关系），满足以下意义上的单调性：如果nJ≤n且MJ≤m，且如果n·m是有定义的，则nJ·mj也是有定义的，且nJ·MJ≤n·m。满足单调性的序的典型例子是扩张、可除性、预序和离散序（等式）。回想一下，如果存在k，则扩张阶与m≤n相关，使得m·kn，即，如果n能被m整除。如果m ≤n且n≤m，则我们可以写m ∈ n = n。在一个新的计算中，m·n=mJ·nJ我们也意味着双方都有定义。与通常的术语稍有不同，如果s · s ∈ = s，我们称元素s∈M恒等式。这个较低的概念的动机是，如果n=m，则n和m对于任何逻辑都是完全可交换的。操作，因此不需要在模型中对它们进行不同的读者应该记住的一个例子是有限部分函数N~X到某个集合X的部分幺半群，其中复合只有在域不相交时才被定义有一个单一的单位，地图与空域。设B=P↑（M）是M的关于阶≤的向上闭子集的集合，P（M）是M的幂集。回想一下，任何元素p∈B都是主理想↑m ={n|n≥ m}。以下事实是众所周知的。事实2.2集合B和P（M）在按子集包含排序时是完备的海廷代数。B上的运算如下：T=M=p q=p q p q=p qpi=pipi= pip={m |<$n ≥ m，n ∈ p<$n ∈ q}3 我们使用为了克林平等62A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57∧ ∩ ∨∪i∈Ii∈Ii∈Ii∈Ii∈Ii∈Ii∈Ii∈Ii∈IP（M）上的运算为T=M=p q=p q p q=p qpi=pipi= pip={m |m ∈ p<$m ∈ q}此外，存在一个包含i：B → P（M），它既保持了上确界又保持了下确界。由于ι在上确界和上确界中保持不变，它特别有一个左伴随，这是运算Cl（·） ：P（M）→B的闭包，它将子集p映射到包含p的最小上闭子集。Cl（p）={m ∈M|<$n ∈ p，n ≤ m}引理2.3闭包运算保持上确界，但一般情况下不保持上确界保存在fima。以下也是众所周知的。事实2.4集合P（M）对于下列运算是一个完备的BI-代数。I=Ep*q={k |<$m ∈ p，n ∈ q，k = m·n}p−* q={n|<$m ∈p，m·n定义ed<$m·n∈q}命题2.5集合B也是一个完备的BI-代数，其中单位和乘法定义如下IJ=Cl（I）p *Jq=Cl（p* q）其中右边的运算是2.4中定义的。在P（M）中很容易看到Cl（p* q）= Cl（Cl（p）*Cl（q））。 因为对于任何对于任意p∈ B，我们有Cl（p）=pIJ*Jp = Cl（Cl（I）* p）= Cl（Cl（I）* Cl（p））= Cl（I * p）= Cl（p）=p。为了证明p*J−有一个右伴随，它需要检查它是否保持上确界。这是由P（M）中的*这样做的事实和闭包Cl（−）保持上确界的事实得出的p*Jpi=Cl.p *pi=Cl.（p *pi）n=Cl（p *pi）=（p*Jpi）A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5763i∈Ii∈Ii∈IQ这些使我们能够构建一个资源的基本逻辑模型。我们可能希望对如何依赖于f≤和·的相互作用的附加性质进行建模。引理2.6性质p*qp等价于下面的性质。 任何m，n ∈M，使得m·n被定义，我们有m·n ≥ m。证明第二个属性意味着第一个是简单的。为了看到相反的情况，我们有假设（↑m）*（↑n）<$↑m。因为根据定义m·n∈（↑m）*（↑n）我们得到m·n∈↑m，根据定义，这意味着m·n≥m。Q例如，前面引理中的条件可以通过幺半群上的延拓序来满足，但不能通过离散序来满足2.2可重复的同品种器械正如我们在引言中提到的，我们希望用子逻辑挑出的主要性质是谓词P是可重复的，即，它满足P惠P * P。因此，设F∈ B是满足P * P=P的那些P的集合。注意F是完备格B上单调算子P<$→P*P的不动点集，因此根据Knaster-Tarski不动点定理，F本身是完备格，尽管一般不是B的子格。 为了在B上有一个模态能精确地挑出F，F包含在B中必须有一个右伴随，这等价于F在任意并下是闭的。引理2.7设M上的阶≤是扩张阶。 那么F在任意并下是闭的。证明：如果对任意集合i∈I，Pi=Pi*Pi，则我是。Pin*。我是。但这是直接的，因为对于任何i∈I，我们有Pi= Pi* PiPin*。我是。i∈Ii∈IQ因此，在一个大类的实际情况下，包含F到B有一个右伴随G.然而，我们希望从这个附加中产生的模态是行为良好的，因此我们也希望它保持联合，因为这是模态与逻辑中的存在量化交换所需要的。因此，我们对G也保持工会的情况感兴趣。然而，正如我们下面所展示的，在许多实际情况64A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57.∼∼例2.8设M是非负有理数且≤扩张阶，这与有理数上的通常排序一致。 可以直接计算F={q，P0，P>0}，其中P0 =M且P>0 ={q∈M| q> 0}。此外，很容易看出，G（P）= P，如果P∈F否则，是包含F B的右伴随。而G不维护工会，因为P>0=q>0{r|r≥ q}。请注意，本质上相同的反例，经过必要的修改，可以使用部分有限映射的部分交换幺半群构造我们可以从这个例子中学到的一个特别的东西是，问题是由完全由不可重复的元素近似的可重复元素P引起的。因此，一个可能的解决方案出现了。我们把注意力限制在由可重主理想生成的那些谓词P上我们将在下一节中研究这类谓词的集合3通过幂等资源的下面对C的定义是由以下两个属性驱动的。引理3.1一个principalid eal↑m在F中当且仅当m·m= m。Sup posem·m= m. 我们展示了两个夹杂物。第一个↑m（↑m）*（↑m）。如果x≥m，则x也≥m·m，所以x∈（↑m）*（↑m），因为m·m是。相反，如果x∈（↑m）*（↑m），则有y，y1，y2使得x≥y，y=y1·y2，y1，y2≥ m. 则y ≥ m·m，因此x ≥ y ≥ m·m = m，因此x ∈↑ m。现在假设↑m是可重复的。由于m∈↑m，存在x1，x2使得m≥x1·x2且x1，x2≥m。 因此m·m被定义，且m≥m·m。 最后，m·m∈（↑m）*（↑m），因此m·m≥m，因为我们假设↑m是可重的。 因此我们有m·m = m。Q类似的推理产生了下面的命题。命题3.2如果阶≤满足对于任意两个幂等元s1，s2，如果定义了s1·s2，则s1≤s1·s2或s2≤s1·s2，则对于某个幂等元集合X的任何并s∈X↑s是可重的。关于幂等元的条件是必要的，这也许有点不幸特别是，当订单是延期订单时，该条件得到满足设C是B中由下列意义的幂等元生成的元素pC={p∈ B|<$m ∈p，<$s∈p，s≤m <$s·s <$= s}A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5765i∈Ii∈I芽孢杆菌中 再次使用γ，我们得到b=γ（δ（b））i∈Iδ（pi），从而给出了证明.Q设δ：C → B为包含。我们有以下简单的引理。引理3.3 C和δ具有以下性质。• δ是单调的并且也反映了阶，即，它是一个完全而忠实的函子。• C具有从B继承的上确界，δ保持它们。• δ有一个右伴随γ：B→ C，由下式给出：γ（q）={m ∈ M |s∈q，s≤m <$s·s<$=s}。此外，γδ = id。• 右伴随γ保持上确界。• γ有一个右伴随γ，由下式给出：n（q）=p。p∈B，γ（p）<$q此外，他是完全和忠实的。这其中的大部分都是非常简单明了的。对于最后一部分，注意到我们现在有δEγE，结果由[7，引理1.3]得出，并且δ是完整的和忠实的，即，它尊重和维护秩序。Q引理3.4 C有全无穷大。 它们被给出为pi= γ。δ（pi）证明首先回想一下我们有γ<$δ= id，现在我们准备证明i∈Ipi是所有pi的最小确界。以来i∈Iδ（pi）是B中的下确界，我们有i∈Iδ（pi）<$δ（pi）对所有i∈ I. 然后，通过定义所提出的最小值，γ的单调性，我们有i∈Ipi<$γ（δ（pi））=pi，对所有i∈ I.这说明我们有一个下限。 假设现在对所有的pi存在另一个下界b。 然后δ（b）是所有δ（pi）的下界，因此δ（b）∈Iδ（pi），因为这是下确界从这个构造中我们可以看到，一般来说，包含δ不会保持不变。在第5节中，我们建立了一个由M的幂等元的结构的交集构造无穷大的充要条件。命题3.5C是一个完备的Heyting代数。证明从引理3.4可以得出C具有全无穷大。 根据前一个引理γ在fima中保持不变，即， 所有限制。 由于C是完全的和忠实的，具有保持有限极限的左伴随，C是（等价于）B[8，A4.3.1]的指数理想，这意味着C是carnival闭的，即，海廷代数Q66A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57∈I由于我们有带有δ完全和忠实的附加函数δEγ，我们可以使用B上的模态□=δ<$γ来刻画B的子集C。也就是说，C是□的不动点的集合。或者，如果我们将□视为comonad（即，内部算子），则C是□的余代数的集合。命题3.6 □算子满足下列性质。• □是幂等的。• 对所有p ∈ B，有□（p）<$p.• □保持所有的上确值，但不保持一般的上确值。然而，如上所述，一般来说，δ和□都不保持不变。因此C特别不是B[8，A4.3.1]的Heyting子代数然而，在某些情况下，它将是。在幺半群上的序是扩张序的情况下，可以证明δ和□保持无穷大。实际上，我们只需要证明p<$q是p和q的交集，对于任何p，q∈C。Sup poser∈p<$q. 则存在一个s∈psuc h，使得s·s∈=s且s≤r，类似地，存在一个t∈q，使得t·t∈q=t且t≤r。特别是，这意味着r=rJ·t和r=rJJ·s。然后s·t≤s·r=s·rJJ·s=rJJ·s=r由于s，t≤s·t，我们有s·t∈p<$q，由于s·t显然是幂等的，我们证明了p<$q∈C。很明显，δ保持T，因此由于δ只是包含，B中的（有限）无穷大是由交切给出的，δ显然保持它们，□也是如此。这也意味着[8，A4.3.1]，C是B的Heyting子代数，但它不是一个完整的Heyting子代数，也就是说，无穷大一般不由交叉点给出。另一方面，在幺半群上的序是离散的情况下，很容易看出δ和□保持所有的不动点。其实，在这种情况下，□（p）是p中的幂等元的集合。一般来说，□不保无穷大的原因是，给定一个幂等元集合si≤ m，对于某个元素m，使得si∈ pi，不存在幂等元s∈ipi的标准选择，使得s≤m。事实上，在第5节中，我们证明了如果集合I（m） ={s≤m}，则由y_i_intersections定义的下一个区域是|s·s=s}有一个最大的元素。在下面的部分中，我们证明了给定这样一个幂等元的选择，我们有C是B的一个完备的Heyting子代数，并且□是一个完备的Heyting代数态射。在此之前，我们讨论引入C和□的原因之一。3.1幂等元与分离合取引入□的原因之一是它允许我们表达命题的更多性质，特别是*和*如何相互作用。引理3.7A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5767• 如果阶≤满足对于任意幂等元s和任意元素x∈M使得x≥s，复合x·s被定义，则□（p）q□（p）*q• 如果阶≤满足以下性质：对于任何元素x和任何幂等元s使得x·s被定义，则x·s ≥ s，则以下性质成立。□（p）*q <$□（p）<$q。第一个条件由延拓阶和离散阶满足。第二个条件由延拓阶满足，但不一定由离散阶满足。4通过内部运算符的在这一节中，我们证明了M上的内部算子，关于预序≤的内部算子，提升到B上的一个保持上确界和下确界的内部模态，而且它的不动点集是B的一个完备Heyting子代数。通过假设f和幺半群运算的其他性质，我们恢复了上一节中控制*和* 的相互作用的设f：M→M是M上关于阶的内部算子≤。解释一下，这意味着f是一个单调函数，另外满足f（m）≤m和f（m）≤f（f（m））.请注意，上述性质一起意味着，对于所有m∈ M，f（m）f（f（m）），即f（f（m））≤f（m）和f（f（m））≥f（m）。函数f通过取原像提升到B上的函数f−1让Lf={p∈ B|p= f−1[p]}是f−1的不动点的集合，令Δ：Lf→B是包含。等效地Lf可以定义为sLf={p∈ B|p<$f−1[p]}，因为对于所有m ∈ M，f（m）≤m。引理4.1如果我们考虑Lf和B，通过包含偏序，那么• Δ保持并反映顺序，即，是一个完全且忠实的函子。• L f在B中的任意上确界和下确界下是闭的。• △在fima和suprema中保持不变。• Δ具有右伴随 Γ：B→Lf，由下式给出：Γ（q）=f−1[q]此外，Γ保持所有的无穷大和上确界。证明Lf具有由交集给出的内点和上点的事实直接遵循原像函数保持交集和并集的事实。第一项和第三项是直接的。68A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57ΣΣ当且仅当f（m）∈q，所以f−1f−1[q]=f−1[q]。对于最后一项，我们按如下方式进行为了证明Γ是Δ的右伴随，我们必须证明它实际上映射到Lf，并且对于p∈Lf和q∈ B，Δ（p）<$q <$$>p<$ Γ（q）。要看到它映射到Lf并不困难，使用f是单调和幂等直到同构的事实：假设q∈ B。因为f是单调的，所以f−1[q]也是上闭的，只要q是。由于q是u向闭的，我们有f（f（m））∈q现在我们证明Δ（p）<$q<$$>p<$r（q）。设Δ（p）<$q。则f−1[p]<$f−1[q]= Γ（q），由于p∈Lf，p<$f−1[p]，因此p<$Γ（q）。假设p<$r（q）=f−1[q]。则f[p]<$f−1[q]<$q。由于q是上闭的，并且使用f（m）≤m的事实，这意味着Δ（p）=p<$q。由于上确界和上确界分别由并集和交集给出，所以Γ保持它们是直接的。Q引理4.2Δ有一个左伴随 ε：B→Lf，由下式给出：（p）={q∈ Lf|pq}这是引理4.1和[2，推论9.32]的直接结果。Q引理4.3Γ有一个右伴随π，由下式给出：（q）={p∈B| Γ（p）<$q}此外，他是完全和忠实的。从引理4.1和[2，推论9.32]可以证明Γ有一个如上给出的右伴随。对于第二部分，注意到我们现在有ΔE ΓE，结果由[7，引理1.3]得出，并且Δ是完整的和忠实的。Q命题4.4Lf是B的完备Heyting子代数.证明由上述引理Lf有所有的无穷大和上确界。因为它是一个右伴随，所以它保持在fima中。由于L f是满的和忠实的，并且有一个左伴随保持无穷大，所以Lf是（等价于）B[8，A4.3.1]的指数理想，这意味着Lf是carlington闭的，即，海廷代数Q我们已经证明，我们有一个序列的选择，EΔE IE其中Δ和Δ是完全的和忠实的。此外，它似乎并不保持fima或保持suprema，所以我们不能进一步扩展这个序列的A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5769定义Qf：B → B为由附加项ΔE Γ产生的内部算子，Qf（p）={m∈M|f（m）∈p}= f −1[p].当f从上下文中明确时，我们将简单地写为Qf。引理4.5 Q算子满足以下性质。• Q保持所有的在fima和suprema。• Q（p）≠p，对所有p∈ B。• Q是幂等的。这些直接从上述Δ和Γ的性质得出4.2分离合取与Q算子引理4.6如果函数f满足对任意m，f（m）·m∈=m，则Q（p）<$Q<$Q（p）* q。推论4.7如果≤满足引理2.6的条件，f满足引理4.6的条件，则Q（p）*q = Q（p）<$q和Q（p）= Q（p）* p。概括起来，我们有下面的定理。定理4.8Let（M，·，E，≤）是一个或多个偏序交换幺半群，f：M → M是关于≤的内部算子. 那么B是一个完全的BI-代数，用于上面定义的运算。 由Q的不动点组成的B的子集L f是B的完备Heyting子代数而且。• 如果f满足f（m）·mm对所有m，则Q（p）<$Q<$Q（p）* q。• 如果阶≤满足m ≤ m·n，则当m·n被定义时，p*q <$p<$q。因此，我们从一个序部分交换幺半群出发，构造了一个完备的BI-代数。使用这个完整的BI-代数，我们构建了一个BI-超主义，这是一个模型的高阶分离逻辑，连同一个Q模态，挑出的子逻辑的持久谓词享有特殊的属性，就像在上面的定理中解释的分离合取5内部运算符是必要的在这一节中，我们证明了B的任何完备子格L，其中包含的右伴随G也保持并，对于内部算子f，具有Lf的形式。此外，如果L <$F，那么它也必须是C的子集，并且我们建立了当L f = C时的充要条件。特征化使用M的幂等元的结构。因此，我们可以陈述模型类的完备性的一种形式。如果我们希望在B上有一个行为良好的模态，那么它必须具有第4节中考虑的形式，70A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57−1M≤函数f。此外，如果我们希望Lf中的所有谓词都是可重复的，那么f必须映射到幂等元。因此，我们特别表明，核心的概念，认为在虹膜，是必要的，只要我们决定，我们希望一个行为良好的模态Q的逻辑。4注意，当我们说L是B的完全子格时，我们特别表示L上的上确界和上确界是从B继承的，即，它们分别是交集和并集。简而言之，如果幺半群M满足命题3.2的假设，例如，如果它是扩张序，则包含在F中的B的完全子格L可以被描述如下。定理5.1设L是B的完备子格。设G：B→ L是包含L <$B的右伴随。则存在M上的内部算子使得G=f。证明由于G是包含的右伴随，L和B是偏序集，我们对任何p∈B有p∈L当且仅当G（p）=p。让我们把L看作M上的拓扑。由于它是由假设封闭下任意交叉（这是一个亚历山德罗夫拓扑）点有最少的邻居。对于m∈ M，设N（m）∈ L是m的最小邻域.则存在某个XM，使得N（m）=x∈X↑x。[4]注意，本节中的一些证明，特别是构造函数f的证明，使用了选择，因此不是构造性的。对于某些幺半群和命令 选择的使用是可以避免的，但我们不研究这样的条件。A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5771例如，取X=N（m）。因此N（m）=G（N（m））=G（↑x）x∈X所以存在x∈X使得m∈G（↑x）。但G（↑x）显然是m的邻域，因此N（m）=G（↑x）。我们现在要求G（↑x）=↑x，由此可以证明↑x<$G（↑x）。我们有↑ xx∈X↑x = N（m）= G（↑x）。T husN（m）=↑x. 更进一步地，很明显，这个x是 唯一的，直到ox=。 Letf：M → M是一个函数，它为每个m选取一个元素f（m），使得N（m）=↑f（m）。这是直接的，f是一个内部算子。最后，设p∈ B。 则p∈L当且仅当m∈pN（m）=p，所以G（p）={N（m）|N（m）p}通过偏序集的伴随函子定理和N（m）生成L的事实。因此m∈G（p），如果存在n，使得m∈ N（n）且N（n）<$p。但是N（n）是m的邻域，所以N（m）<$N（n），因此我们得出m∈G（p）当且仅当N（m）<$p，或者换句话说，当且仅当f（m）∈p。Q5.1两种模式一个自然的问题是C和Lf，以及□和Q是如何相关的。命题5.2集合Lf是C的子集当且仅当f（m）·f（m）=f（m）对于所有M。证明：第一部分假设：首先，Lf∈ C，令m∈ M。 由于f是单调和幂等的事实，我们总是有↑f（m）∈Lf，我们有↑f（m）∈C，因此存在元素ntsl=f（m）such，使得s·sl=s. 亨斯f（m）·f（m）= f（m）.对任意m，设p∈ LF，设f（m）·f（m）≠f（m）. 则显然对任何m∈p都有一个幂等元f（m）∈p在m之下，因此p∈ C。Q命题5.3如果阶≤满足对于任意两个幂等元s1，s2，如果如 果 s1·s2被定义，则s1≤s1·s2或s2≤s1·s2，则集合Lf是F（可重预元）的子集当且仅当f（m） ·f（m）≠f（m），对于llm. TusLf< $ F当且仅当Lf<$C.对所有m，上一个p的p∈f（m）·f（m）≠f（m）. 5.2LF-1000C的预充电池因此，使用命题3.2，我们有Lf <$F。假设Lf∈ F。由于f是幂等的，我们有↑f（m）∈Lf，对于所有M. 因此，根据引理3.1，f（m）对每个m都是幂等的。Q72A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57∼ ∼ ∼∼∼∼引理5.4prop<$Q（p）<$□（p）等价于f（m）·f（m）=<$f（m），M.对于向左的方向，假设f（m）· f（m）=f（m），对于所有m。 Letp ∈ B。 如果m ∈Q（p），则f（m）∈ p，因此m ∈ □（p），因为f（m）是幂等元。现在假设Q（p）<$□（p）对所有p。特别是Q（↑f（m））<$□（↑f（m））<$↑f（m）。注意，↑f（m）= Q（↑f（m））。因此，□（↑f（m））= ↑f（m），这特别意味着（因为f（m）∈↑ f（m））存在一个幂等元s ∈↑ f（m），其中f（m）≤ s。 因此f（m）= s，因此f（m）·f（m）= s· s = s =f（m）。Q命题5.5格Lf和C重合当且仅当f是对幂等元的集合，即，如果f（m）·f（m）=f（m），对所有m，f（s）= s，对所有幂等元s。证明首先假设f是幂等元集合的收缩。 然后我们从前面的引理知道Q（p）<$□（p），所以它表面上显示相反的包容。 如果m ∈□（p），则存在一个恒等式s∈pbelowm. Butf（s）=s，所以f（m）≥f（s）≥s，因此m∈ Q（p）.假设Lf和C重合。 让我们成为一个幂等元。 则↑s∈ C，因此↑s∈ Lf，但这意味着f（s）∈↑s，因此f（s）≥s，并且由于我们总是假设f（s）≤ s，所以我们有一个vef（s）<$=s。Q最后，我们确定了这种收缩何时存在。命题5.6设I（m）是m以下的幂等元的集合。存在命题5.5意义下的收缩f当且仅当I（m）对每个m都有最大元。假设f存在收缩 我们称f（m）∈ I（m）是I（m）的最大元素. 这是直接的，因为如果s∈I（m）thens=f（s）≤f（m）y单调y假设f是收缩的。现在假设每个I（m）都有一个最大的元素。设f是一个函数，对m∈M，它选取f（m）∈ I（m）中最大的元素之一它显然是单调的，幂等的，并且满足f（m）≤m，即，它是一个内部操作员。此外，它清楚地映射到幂等元，如果s是幂等元，则s是fI（s）的最大元素，因此f（s）n=s。Q现在我们在有扩张阶的幺半群的有用情形中总结上面的引理和命题。定理5.7设M是部分交换么半群且≤ M上的扩张阶。然后• CF• B上的任何模态Q保持并和交，并且使得Q P对任何P都是可重的，对于某个内部算子f映射到幂等元，模态Q的形式为Q f。 此外，Q的不动点的集合L是C的子集。A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）5773• 对于某个f（n ecessarilyunique直到f=），latti c e C具有L f的形式当且仅当对于每个元素m∈M，m以下的幂等元集合有最大元素.此外，这是当且仅当C在任意交下闭。最后，在这种情况下，模态Q和□重合。映射到幂等元的内部算子f对应于Iris的核心运算。我们已经表明，如果我们希望拥有一个行为良好的持久谓词子逻辑，那么在Iris中所做的选择是必要的，所有这些谓词都是可重复的。此外，我们已经证明了存在最大的这样的子逻辑的条件。这就是当m以下的幂等元集合对于任何M.对于许多在实践中考虑的幺半群，在Iris中，事实上在每个元素m下面都有一个唯一的幂等元，因此自动会有最大的一个。6更改环境逻辑在这一节中，我们将展示文献中发现的一些先前的结果是如何在上述结构中出现的。特别是通过在树拓扑的环境逻辑中工作[5]，我们从资源代数的概念中恢复了完全度量资源代数的概念[9]资源代数是Iris程序逻辑模型中使用的资源概念，Iris程序逻辑是一种非常通用的Iris通过对资源（如堆和不变量）的抽象处理来定义6.1[[9，11]]一个（单位）资源代数是一个结构（M， ·，ε，|·|，V ），使得（M，·，ε）是一个交换幺半群，|·|：M→M称为core是关于M的扩张阶的单调函数，VM是关于扩张阶向下闭的所谓有效元的子集，并且包含单位。此外，核心被假定为一个内部算子（关于M的扩张阶），它映射到M的幂等元。注6.2还有一个非酉资源代数的概念[9]。这些被用作构造用于模型构造的单位资源代数的中间步骤由于我们对模型感兴趣，我们只关注与有序部分交换幺半群有关的单位资源代数。一个（酉）资源代数通过取有效元素关于扩张阶的向上闭子集来产生一个完全BI-代数P↑（V）={p <$V |<$m ∈ p，<$n ∈ V，n ≥ m <$n ∈ p}.74A. 比贾克湖Birkedal/电子笔记在理论计算机科学336（2018）57MM12注6.3在Iris的实际模型中，我们取M的上闭子集，但只取关于有效元素的上闭子集，如果两个子集在有效元素上一致，则用两个子集相等的关系表示。这显然与上面定义的P↑（V）序同构，所以我们选择使用上面的表示，因为它对我们的目的来说更简单一个（单位）资源代数的概念被包含在关于模型的部分交换幺半群的概念中，如下面的命题所解释的。命题6.4F或任何有单位元的剩余代数a（M，·，ε，|·|，V）re存在一个或一个偏序交换幺半群（MJ，·，E，≤）使得完备BI-代数r如P↑（V）与B（定义见第2节）同构.此外，核心|·|产生满足定理4.8的假设的内部运算f：MJ→ Mj。证明给定一个单位资源代数，如命题的陈述中定义MJ为有效元素V的集合。设E={ε}，≤为扩张阶。最后，我们将M j上的部分乘法·定义为函数·：M J× M J→S（MJ）到子单例集合中，5使用子单例集合是部分映射分类器的事实[8，A2.4]。对于m，n∈Mj，定义元素m·n∈S（MJ）为：m·n ={m·n |n ∈ V}很明显，有了这些定义，我们就有了P↑（V）和B的等价性。如上所述。对单位资源代数中的核的假设确保它限制于函数V → V，并且通过假设核是内部算子，