HyLL与SELL：表达力比较和HyLL编码为SELL±

可在www.sciencedirect.com在线获取理论计算机科学电子笔记332（2017）95-111www.elsevier.com/locate/entcs混合和次指数线性逻辑JoéelleDespeyroux1INRIA和CNRS，I3 S，Sophia-Antipolis，法国Carlos Olarte，Elaine Pimentel2北里奥格兰德联邦大学 巴西摘要HyLL（Hybrid Linear Logic）和SELL（Subexponential Linear Logic）是两种逻辑框架，它们被广泛用于描述表现出诸如时间或空间模态的系统。这两个框架都有线性逻辑（LL）作为共同点，它们承认（无切割）完整的集中证明系统。这两种逻辑之间的差异取决于处理模态的方式。在HyLL中，真理判断被标记为世界，混合连接词将世界与公式联系起来。在SELL中，线性逻辑指数（！，？）用代表位置的标签装饰，这些标签上的排序定义了这些位置中资源之间的可证明性关系。众所周知，SELL作为一种逻辑框架，其表达能力要比LL强得多。然而，到目前为止，尚不清楚HyLL是否比LL和/或SELL更有表达力。本文给出了HyLL逻辑规则到LL的编码具有最高水平的充分性，因此表明HyLL与LL一样具有表达性我们也提出了一个将HyLL编码为SELL±（SELL加上对位置的量化），从而更好地了解HyLL中世界的意义。我们总结我们的表达性研究表明，以前的尝试编码计算树逻辑（CTL）运营商到HyLL不能扩展到考虑整体时间连接词的集合我们表明，一个系统的LL与固定点确实需要忠实地对这种时间操作符的行为进行关键词：线性逻辑，混合线性逻辑，次指数，逻辑框架，时序逻辑。1介绍逻辑框架是指定证明系统的适当工具，因为它们支持抽象层次，便于编写对象逻辑证明系统的声明性规范。许多框架被用于证明系统的规范化，线性逻辑[13]（LL）是最成功的框架之一这主要是因为LL是资源意识的，同时，它可以内化经典和直觉主义行为（参见，例如，[6，14]）。1电子邮件：joelle. inria.fr2电子邮件：{carlos.olarte，elaine.pimentel}@ gmail.comhttp://dx.doi.org/10.1016/j.entcs.2017.04.0071571-0661/© 2017作者。出版社：Elsevier B.V.这是一篇基于CC BY-NC-ND许可证的开放获取文章（http://creativecommons.org/licenses/by-nc-nd/4.0/）。96J. Despeyroux等人/理论计算机科学电子笔记332（2017）95≤然而，由于对象级系统在逻辑框架中的具体化应该是自然和直接的，因此有一些特征在LL中无法充分捕获，特别是与LL中存在的模态不同为了填补这一空白，已提议延长当地雇用。其目的是提出更强的逻辑框架，保留线性逻辑作为底层逻辑的优雅属性。其中两个扩展是HyLL（混合线性逻辑）3[8]和SELL（次指数线性逻辑）[9，19]。这些逻辑已被广泛用于指定系统，表现形式，如时间或空间的。HyLL和SELL之间的区别取决于处理模态的方式。在HyLL中，真理判断被标记为世界，两个混合连接词将世界与公式联系起来：满足，陈述一个命题在给定的世界为真，以及本地化↓，它绑定了（当前）的名称。这个命题在世界上是正确的。这些构造函数允许对情态连接词进行具体化，例如QA（A在所有可达世界中为真）和QA（存在一个A成立的可达世界）。世界的底层结构允许过渡系统的建模和时间公式的具体化[8，10]。在SELL中，LL指数（！，？）都贴着标签：公式？A可以被解释为A在一个位置、模态或世界中保持。 此外，可以在与a（b a）相关的位置b中推导出A。 另一方面，公式？一个！aA意味着A被限制在位置a中，也就是说，信息A不会传播到与a相关的其他世界 / 位 置 。 虽 然 线 性 逻 辑 只 有 七 个 逻 辑 上 不 同 的 刘 海 和 问 号 前 缀 （ 没有，！，？，！？？？！！！？！，？！？），SELL允许无限数量的这种前缀（例如，！是吗？c？是的d）。因此，SELL增强了LL作为逻辑框架的表达能力到目前为止，尚不清楚HyLL与LL和/或SELL之间的关系。在本文中，我们回答了这个问题，显示了直接编码的HyLL的逻辑规则到LL的最高水平的充分性。因此，我们表明，HyLL实际上是作为表达的LL。我们还提出了一种将HyLL编码为SELLA（对位置进行量化的SELL）的方法，可以更好地理解HyLL中世界的含义。更准确地说，我们将HyLL公式表示为SELL中的公式，并将逻辑规则编码为SELLA中的公式。 我们发现，一个可调的次指数结构，足够表示HyLL中的任何世界结构。这更好地解释了为什么HyLL中的世界没有给LL增加任何表达能力：它们不能像子指数对提升规则那样控制逻辑上下文HyLL已被证明是生物系统规范化的一个灵活框架[10]，其中系统及其属性都使用相同的逻辑进行规范化。更准确地说，感兴趣的属性首先用计算树逻辑（CTL）编写，然后编码为HyLL公式。 但没有关于可以充分捕获3实际上，HyLL是直觉线性逻辑（ILL）的扩展，而SELL可以被看作是ILL或LL的扩展。J. Despeyroux等人/理论计算机科学电子笔记332（2017）9597........在Hyll。因此，本文的最后一个贡献是继续我们对HyLL理论的研究，并推进以前的尝试，使用这种逻辑的具体化的过渡系统和公式的CTL。我们证明了在HyLL中不可能充分编码普适路径量化器A（对于所有路径），也不可能编码时间公式EGQ（存在Q始终成立的路径）。这些公式的定义是递归的，因此需要在元层面上使用归纳法与[10]中使用的元推理不同，我们使用了一个具有固定点结构的逻辑框架。更确切地说，我们使用具有不动点算子的加法乘法LL（μMALL）[3]来编码CTL。我们证明了CTL[4]的不动点特征可以与μMALL的不动点算子相匹配本文的其余部分组织如下。我们简要回顾了2.1节中的LL，2.2节中的HyLL和2.3节中的SELL。将HyLL逻辑规则编码为LL将在3.1节中讨论。第3.2节介绍了HyLL到SELLA的编码。 我们还证明，信息confinement，在SELL中，需要指定空间系统的功能，不能在HyLL中捕获。第4节展示了如何将CTL编码为μMALL。第五节是论文的结论。伴随的技术报告[11]包含了结果的详细证明以及本文中使用的一套完整的微积分规则2预赛虽然我们假设读者熟悉线性逻辑[13]（LL），但我们将在以下部分回顾其基本证明理论2.1线性逻辑与聚焦文字是原子公式（p）或它们的否定（p）。连接词“”和“”。它们的单位1和1是乘法的;连接词1和1以及它们的单位0和1是加法的;1和1是（一阶）量化器;并且！然后呢？是指数（分别称为bang和问号）。由Andreoli[2]首次提出的线性逻辑，聚焦证明系统提供了无割证明的范式证明线性逻辑的联结词可以分为两类。否定连接词有可逆的引导规则：这些连接词是。、&T、和？。 积极的连接词“”、“1”、“”、“0”、“”和“！ 是否定连接词的德·摩根定理。一个公式是正的，如果它是一个被否定的原子或者它的顶层逻辑连接词是正的。类似地，如果公式是原子或其顶层逻辑连接符是否定的，则公式是否定的集中证明分为两个阶段。在否定阶段，所有的可逆推理规则都被积极地应用。积极阶段开始于选择一个积极的公式F来关注。正规则应用于F，直到遇到1或否定的原子（并且证明必须通过应用初始规则结束）或提升规则（！）或遇到一个负的子公式时，证明切换到负相。98J. Despeyroux等人/理论计算机科学电子笔记332（2017）95当聚焦公式是双极时，证明搜索的相位变化特别有趣[2]。定义2.1我们称一个逻辑公式为线性逻辑公式，它是由原子和否定连接词的出现建立起来的，其限制条件是：原子的范围。另一方面，双极是由单极子和仅使用正连接词的负原子构建的正公式，具有额外的限制！只能应用于一个节点。聚焦于双极将产生单个正相和单个负相。这种两阶段分解使我们能够充分地捕获应用程序对象级推理规则的元级线性逻辑，将在第3节中显示。经典线性逻辑的聚焦系统LLF可以在[11]中找到。2.2混合线性逻辑混合线性逻辑（HyLL）是直觉主义一阶线性逻辑（ILL）的保守扩展，其中真值判断由表示状态和状态转换约束的世界HyLL的判断形式为特定的世界选择产生特定的HyLL实例。典型的例子是HyLL在[8]中首次提出，并已被用作指定生物系统的逻辑框架[10]。形式上，世界被定义如下。定义2.2 [HyLL worlds]一个约束域 W是幺半群结构你好，好吧W中的元素称为世界，其可达关系≤：W×W定义为u≤w，如果存在v∈W使得u.v=w。恒等世界ι是≤-初始的，它旨在表示没有任何约束。因此，普通的一阶线性逻辑可以通过将所有世界标签设置为恒等式嵌入到HyLL的任何实例中。约束域的一个典型的简单例子是T =IN，+，0 <$，表示时刻。原子命题（p，q，. . . ）应用于项序列（s，t，.. . ），它们是从包含常量（c，d，.）的非类型化术语语言中提取的。. ）、项变量（x，y，. . . ）和函数符号（f，g，. . . ）应用于项列表（t）。非原子命题由一阶直觉线性逻辑的连接词和两个混合连接词构造而成也就是说，满足（at），它表明一个命题在给定的世界（w，i，u.v，. . . ）和localization（↓），它绑定了命题为真的（当前）世界的名称。以下语法总结了HyLL的语法。t：：= c|X|f（t）A，B：：= p（t）|A组B组|1 |A → B |A &B|不|A组B组|0|！一|你好 一|你好 一|（A at w）|↓ u。 一|你好 一|你好一J. Despeyroux等人/理论计算机科学电子笔记332（2017）9599注意，世界u在命题↓ u中有界。A，Because. A和B。A.世界变量不能在术语中使用，术语变量也不能在世界中出现。这种限制对于HyLL的模块化设计很重要，因为它将纯粹的逻辑真理与约束真理分开。我们注意到，↓和at可以与所有非混合连接词自由交换[8]。HyLL的微积分[12]表示使用形式为Γ; ΔC @w的序列，其中Γ（无界上下文）是一个集合，Δ（线性上下文）是A@w形式的判断的多集合。注意，在判断A@w中（如命题A在w处），w可以是W中的任何表达式，而不仅仅是变量。下面描述了处理新混合连接词的推理规则（完整的规则集可以在[11]中找到）。r;Rr处Δ<$A@u;L处Δ，A @ u<$C@wr;Δ（Aatu）@wr; Δ，（Aatu）@vC@wr; ΔΔA [w/u]@w↓Rr; Δ，A [v/u]@vC@w↓LΓ;Δ↓u. A@wΓ;Δ，↓u. A@vC@w请注意，（Aatu）是一个移动命题：它携带着它所处的世界，是真的弱化和收缩是无界语境下的可接受规则最重要的结构性质是一般恒等式的可容许性（即在任何公式上，而不仅仅是原子命题）和割定理。前者为逻辑提供了一个句法完备性定理，后者则保证一致性（即没有证据。;。0@w）。定理2.3（恒等式/割）1. Γ;A@wA@w2. 若Γ;ΔJ，A@u<$C@w，则Γ; Δ， ΔJ<$C@w3. 如果r;. ΔA @ u和Γ，A @ u;Δ ΔC @ w，则是Γ; Δ C @ w。HyLL在直觉线性逻辑方面是保守的：只要不使用混合连接词，HyLL中的证明与ILL中的证明是相同的。此外，HyLL比S5更有表现力，因为它允许使用混合连接词直接操纵世界，而HyLL我们还注意到HyLL承认一个完整的集中[2]证明系统。感兴趣的读者可以在[8]中找到关于HyLL的证明和进一步的元理论定理。2.3线性逻辑中的次指数具有次指数的线性逻辑4（SELL）与LL共享除指数之外的所有连接词然后呢？卖出可能包含尽可能多的次指数[9，15，19]，写！a和？A、需要的的[4]我们注意到，直觉的和经典的SELL同样具有表达性，如[5]所示。 所以虽然我们将在这里介绍SELL的经典版本（在3.2节中需要），我们也可以将SELL作为ILL的扩展。100J. Despeyroux等人/理论计算机科学电子笔记332（2017）95....aa≤∈≤SELL中公式的语法如下：F：：=0|1|不|⊥|p（t）|F1和F2|F1和F2|F1. F2|F1&F2|B.F.|B.F.|！ F|什么？ FSELL的证明系统由一个次指数签名指定，其中I是一组标签，U是一个指定哪些次指数允许弱化和收缩的集合，≤是I的元素之间的前序。 我们将使用a，b，...在I中的所有元素上，我们假设≤是关于U向上封闭的，即若a∈U且a≤b，则b∈U.SELL系统是将线性逻辑连接词的规则（除指数规则外）相加而成的。次指数的规则是对a∈I的次指数的舍弃和提升你说呢？一个F1，... 什么？an Fn，G<$r，G啊！一是吗 ？一你说呢？一个F1，... ？nFn，！ 你好G在这里，规则！a有一个附带条件，即a ai对所有i。也就是说，一个人只能介绍一个！a，如果该表中的所有其他公式都标有大于或等于a的索引。此外，对于所有的指数一个U，我们增加了通常的规则，削弱和收缩？a.我们可以用次指数量化器来增强SELL的表现力A和（[16，19]）由规则给出（省略次指数签名）G[le/lx]► r，Alx：a.GAr，G[l/lx]► Γ，lx：a.G其中Le是新鲜的。直觉上，次指数变量扮演着与本征变量相似的角色。通用变量lx：a表示a的理想中的任何次指数、常数或变量。因此，lx可以由类型b的任何次指数l代替（即，l：b）如果b a.我们称这个系统为SELLA。如[16，19]所示，SELLA承认一个无切割的、完全集中的证明系统（在[11]中提出）。这将是整个文本使用的系统定理2.4 SELLA对任何次指数签名都允许割消。3HyLL和SELL的相对表达力我们观察到，虽然线性逻辑只有七个逻辑上不同的刘海和问号前缀，但SELL允许无限数量的前缀，例如。、！我，或！我？J. 因此，通过使用不同的前缀，我们都适用于更严格的系统的具体化，其中使用子指数来标记不同的模态/状态。例如，次指数可以用来表示证明系统的上下文[17];J. Despeyroux等人/理论计算机科学电子笔记332（2017）95101....L1L 2R........指定具有时间，认知和空间模态[16，19]和软约束或偏好[20]的系统;指定双图[7];以及指定和验证生物[18]和多媒体交互系统[1]。人们可能会问，在HyLL中使用世界是否也增加了LL的表达性。在本节中，我们通过使用[14]中提出的方法证明HyLL规则可以直接编码为LL来证明情况并非如此。3.1HyLL和线性逻辑在[14]中，经典线性逻辑（LL）被用作指定许多逻辑和计算系统的逻辑框架。其思想很简单：使用两个Meta级谓词[·]和[·]|用于识别出现在左侧或在对象逻辑中的顺序的右侧，分别。因此，形式为B1，.，BnC1，.，Cm（其中n，m≥ 0）被指定为多集[B1≠，.，[Bn]，[C1|，...，[Cm|. 如果一个对象公式B在（对象级）经典上下文中，它将在LL中被指定为？[B or？[B|（取决于原始图中B的一侧）。因此，HyLL序列的形式为Δ;.. .. .将在LL中编码为？[Δ θ。 [1] [C|其中，如果n ={F1，...，Fn}，则. .. .. .. .. ... .[=[F1]. .... [Fnand？[=？[F1.........................？[Fn（类似于[·|）.推理规则由重写子句指定，重写子句将结论中的有效公式替换为前提中的有效线性逻辑连接词表示这些对象级公式是如何连接的：上下文是复制的（&）或分裂的（），在不同的推理规则中（）或在同一个推理规则中（）。）.作为一个例子，经典逻辑中合取推理规则的加法版本Δ，A −→ ΓΔ，B−→ Γ <$Δ−→ Γ，AΔ−→ Γ，B<$Δ，A<$B−→Γ可以指定为Δ，A<$B−→ΓΔ−→ Γ，A<$BA，B. （[A<$B<$（[A< $[B<$]））R：A，B. （[A]B|电子邮件（[A|&[B|下面的定义展示了如何将HyLL推理规则编码为LL。定义3.1[HyLL规则到LL]设w，d，h和o分别表示，世界的类型，（一阶）对象，HyLL判断和LL公式。让[·|h → o类型的[·] be谓词和A、B、C分别有w → h、d→h和h类型。HyLL推理规则到LL的编码如图1（我们省略了可以在[14]中找到的大多数线性逻辑连接词的编码）。注意，混合连接词（at和↓）的左右推理规则是相同的（见2.2节）。 这反映在编码的二元性中，我们只替换[·|与[…]还要注意，量化器（一阶和世界）的推理规则看起来是一样的。不同之处在于所涉及的变量的类型由于A的类型为w→h，编码子句R（W）保证102J. Despeyroux等人/理论计算机科学电子笔记332（2017）95C，C，w. （[（CC）@w|. .[C@w| [C@w|）L：C，C，w. （[（CC）@w. . （C @w））JjJjj......J在R：C，u，w处。（[（Catu）@w|[C@u]|）在L：10C，u，w。（[（Catu）@w[C@u）↓R：A，u，w. （[↓u. A@w|[（Aw）@w]|）↓L：A，u，w. （[↓u. A@wR（F）：（[2016年12月28日]。B@u|你好[（Bx）@u|）L（F）：B，u. （[2016年12月28日]。B@ux。[（Bx）@u）R（W）：A，u. （[2005年12月25日] A@u|你好[（Av）@u|）L（W） ：A，u. （[2005年12月25日] A@uv. [（Av）@u）！L：C，w. （[！C@w是什么意思？[C@w）Init：C，w. （[C@w]）[C@w|）Fig. 1. Hyll规则为LL。(De定义3.1）变量v的类型为w。 类似地，由于B的类型为d→h，则x在子句R（F）中的类型为d。这种通过使用类型控制对象行为的简洁方式也被其他对象级推理规则的编码所继承下面的定理表明，事实上，HyLL到LL的编码是适当的，在这个意义上，FLL中的一个集中步骤正好对应于HyLL中的一个推理规则定理3.2（条件性）设条件性是图1中的子句集合。在HyLL i中可证明F @w，[F @ w]|·在FLL中可证明。此外，编码的适当性是在派生的层次上，这意味着，当关注一个指定子句时，双极派生正好对应于在宾语层次上应用引入规则。证据我们将在这里举例说明在L处的规则的情况，其他情况类似。应用对象级别规则Γ; Δ，A @uC@v，Γ; Δ，（Aatu）@wC@vL对应于决定由L处的规则的编码给出的LL公式（存储在存储器中）。由于聚焦，LL中的导数必然具有I1，[Γ;[Δ，[C@v|，[A@u·R， R，[Γ| [A @ u，[Γ|[（A at u）@ w3×∃，[Γ|C，u，w. （[（C at u）@ w[C@ u）D，[Γ|⇑·也就是说，对应于（Aatu）@w的LL公式被消耗，并且在聚焦阶段结束时，A@u的编码被存储到线性上下文中。这完全模仿HyLL中LQ3.2Hyll和Sell线性逻辑允许指定两种上下文维护：弱化和收缩都可用（经典上下文）或两者都不可用（线性上下文）。也就是说，当我们在属于不同世界的HyLL中编码（线性）判断时，所得到的元级原子公式将存储在相同的（线性）LL上下文中。经典的HyLL判断也是如此，（[C@w2J. Despeyroux等人/理论计算机科学电子笔记332（2017）95103一R：C，C J. w：∞。（啊！w[（CC J）@w|什么？w[C@w|你说呢？w[C J@w|）在R：A。 u：∞， w：∞。（啊！w[（Aatu）@w|什么？u[A@u|）在L：A。u：∞，w：∞。（！w[（Aatu）@w？u[A@u]↓R：A。 u：∞， w：∞。（啊！w[↓u. A@w|什么？w[（Aw）@w|）↓L：A。u：∞，w：∞。（！w[↓u. A@w？w[（A w）@w）R（F）：A，w：∞. （啊！w[x]。B@w|你好？w[（Bx）@w|）R（W） ：A，w：∞. （！w[v]。A@w|Av：∞. ？w[（Av）@w|）！L：C，w：∞。（啊！w[！C@w是什么意思？c？是的w[C@w]图二. HyLL规则为卖出±。 (De定义3.3）经典的LL上下文。虽然这是完美的，但将HyLL编码为SELLA可以更好地理解HyLL中的世界，正如我们将要看到的那样。我们使用次指数来表示世界，其中每个世界都有自己的线性上下文。更确切地说，在（左）线性上下文中的形状F@w的HyLL判断被编码为SELLA公式？w[F @ w]因此，在世界w上成立的HyLL判断存储在SELL的w线性上下文中。将经典HyLL合同文本中G @ w形式的一个判断作为对Mulula？ c ？ 是的w[G@w] 也就是说，G@w的编码存储在无界（经典）次指数上下文c中。下一个定义将HyLL推理规则的编码引入SELLA。令人惊讶的是，我们可以观察到，所需的次指数结构是不确定的，它不反映世界的顺序。这是因为HyLL中的世界不像SELL中的促销规则那样控制规则的上下文。这也解释了为什么HyLL没有给LL增加任何表达能力定义3.3设w，d，h，[·|，[·A，B，C与定义3.1相同，o是卖出A公式的类型。给定一个HyLL约束域W，考虑一个次指数签名<$I =<$i，≤，U<$i，使得对于任意w∈I，I=W <${∞，c}，w≤ ∞，对于任意u，w∈ W <${c}，u≤推理规则到SELLW. 此外，U={c，∞}。 HyLL的编码在图2中描述了（我们省略了其他连接词，类似）。注意，w：∞表示∞的理想中的任何次指数。这意味着，在w：∞.F中，次指数变量w原则上可以用I的任何元素来代替。但请注意，由于世界符号仅限于W，因此用c或∞代替w将不匹配上下文中的任何编码公式。也就是说，所提出的次指数签名正确地指定了世界在HyLL中的作用下面的定理表明，我们的编码确实是足够的。定理3.4（可压缩性）设可压缩性是由定义3.3中的编码产生的公式集。在HyLL i∈ C中可证明的是：一104J. Despeyroux等人/理论计算机科学电子笔记332（2017）95我∞{}[{i，[i，i}，wi：[Δi，？w[F@w|·在SEL LA 中 ， 可 发 生。 5此外，编码的适当性是在派生的水平上。证据同样，我们将考虑L处的规则，因为其他情况类似。如果我们决定专注于对应于在L的编码的SELLA公式（存储在？c），我们得到w：[（Aatu）@w;·[（Aatu）@wD、I！Sc：{λ，[Γλ}，wi：[Δλ，v：[C@v|，u：[A@u;··R，？Sc：{A，[r]}， w：[（Aatu）@w};·A！w[（Aatu）@wc：{，[Γ}，wi：[Δ， v：[C@v|;u[A@u]c：{λ，[Γλ}，wi：[Δλ， w：[（Aatu）@ wλ， v：[C@v|;·！w[（Aatu）@ w？u[A@u]c：{λ，[Γλ}， w：[Δλ， w：[（Aatu）@wλ， v：[C@v|;·C，u，w. （！w[（Catu）@w？u[C@u），c：{λ，[Γλ}，wi：[Δλ， w：[（Aatu）@ wλ， v：[C@v|;·D看，在一个（集中）推导证明！wF，由于提升规则和k中的排序，可以存在的唯一上下文是w和∞上下文。由于编码不将任何公式存储到上下文中， ，公式！WF必须从存储在W中的公式中证明。因此，与定理3.2之后的LL推导不同，在左手侧推导中上下文c被削弱，因为c/≤w。因此，在一个集中的步骤中，最初存储在位置w中的[（Aatu）@w]被位置u中的[A@u]取代Q3.3信息确认指定空间模态所需的特征之一是信息确认：空间/世界可以是不一致的，但这并不意味着整个系统的不一致。我们通过展示信息确认（一个可以在SELL中指定的特征）无法在HyLL中建模来在[16]中的次指数的组合形式！w？w用于指定SELL中的信息确认。更准确地说，因为序列（在一个双面的双列直插式演示）！w？00 00！w？哇！v？v0在SELL中是不可证明的，因此可以指定系统，其中不一致性是给定空间的局部，并且不会传播到其他位置。然而，在HyLL中，不可能确定不一致性：HyLL规则Γ; Δ，0@uF @w0L表明任何世界w中的任何公式F都可以从出现在任何世界中的0导出联合注意，即使我们将规则0L换成一个较弱的版本，Γ; Δ，0@wF @w0JL[5]澄清一些符号：如果Δ =F1@w 1，.，Fn @ wn，然后呢？wiΔ =？w1F1@w 1，.，？wnFn@ wn.观察到，在负相，这样的公式将被存储在它们各自的上下文中，这将由ywi：[Δ.J. Despeyroux等人/理论计算机科学电子笔记332（2017）95105►规则0L仍然是可以接受r; Δ，0@w（0atv）@w0JLΓ; Δ， 0@vF @v0JL在Lr; Δ，（0atv）@wF@vr; Δ，0@w/F @v切割4线性逻辑中的计算树逻辑（CTL）混合线性逻辑的表达能力足以对某些形式的模态算子进行编码，从而允许对转换系统的属性进行具体化如[10]所述，考虑到存在（E）和有界泛（A）路径量化器，可以将CTL时间算子编码到HyLL中。我们在本节中展示了这种编码的局限性，以及如何在具有固定点的线性逻辑中完全捕获E和ACTL量化器。为此，我们将使用系统μMALL[3]，它用不动点算子扩展了MALL（乘法，加法线性逻辑）CTL连接词和路径量化器让我们回忆一下CTL中时态运算符的含义。X（Next）表示F（未来）的意思是UCTL量化器E（quantists）表示CTL中的公式是由命题变量a，b，c，. ，通常的命题逻辑连接词和时间连接词前面有一个路径量化器：F：：= p| FF| FF|QXF|QFF|QGF|Q [F UF]Q∈ {A，E}（1）其中p是状态公式。变迁系统考虑一组命题CTL变量V ={a1，...，an}。状态s是从V到集合{true，false}的赋值。 我们将使用pres（ai）（resp. abs（ai））来表示s（ai）=true（resp.s（ai）= false）。因此，集合V上的状态s可以看作是形式为p1（a1）.的合取。其中pi ∈ {pres，abs}.我们考虑由上述状态定义的转移系统和形式为r：s→SJ的转移规则。例如，如果V={a，b}，则转换规则r：pres（a）→abs（b）→abs（a）→pres（b）使得能够从状态s={a<$→true，b<$→false}到状态sJ={a <$→ false，b <$→ true}。 我们将使用s这样的过渡。==rsJ表示106J. Despeyroux等人/理论计算机科学电子笔记332（2017）954.1过渡系统和HyLL为了说明迁移系统中的可达性，HyLL[8]中定义了一些模态连接：QAd=ef↓u。 好吧 （A在U。（w）QAd=ef↓u。 好吧 （A在U。（w）δvAd=ef↓u。 （A在U。v）AU Bd=ef↓u。 好吧（B在U.V&别说了 A在U。（w）QA（分别为QA）表示所有（分别为A是一个可以满足A的状态，并且从现在起可以到达某个路径。连接词δ代表延迟的一种形式：δvA代表过渡到A的中间状态。非正式地，它可以被认为是AUB表示A在所有步骤中保持，直到B保持。我们可以使用这样的模态算子，以便将转换系统的一些特征编码为如下的HyLL公式 考虑集合V ={a1，.， an}的命题变量，设s = p1（a1）<$··<$pn（an）表示一个状态，其中pi∈ {pres，abs}，r：s→SJ是一个指定状态转移的规则.我们将CTL状态和状态转换到HyLL的编码定义为[[pres（ai）]]=pres（ai）[abs（ai）]]=abs（ai）[[s]]=i∈ 1.. n[[pi（ai）]][r：s → sJ]]= nw。（（[[s]] at w）− δ1（[[sJ]]）atw）此外，设F，G是由状态和连接词构造的CTL公式，，我们可以将C定义为：C[[s]]=[s]]C[[F]]=C[[F]]C[[G]]C[[FG]]=C[[F]] C[[G]]C[[E[FUG]=C[[F]]UC[[G]]C[[EXF]]=δ1C[[F]]C[[EFF]]=QC[[F]]很容易看出这样的编码是忠实的，也就是说，（CTL）公式F在由转移规则R定义的系统中的状态s处成立，当且仅当序列t[R]]@0;[s]]@wC[[F]]@w在HyLL中是可传递的（参见[11]）。事实上，由于左线性上下文总是由原子构成，因此可以执行的唯一动作是应用转换规则直到达到满足F的状态，对于这个CTL的有限语法，这可以在有限数量的步骤中达到然而，上述编码不能扩展到考虑形状EGF的公式。事实上，自然的选择将是C[[EGF]] =QC[[F]]，但是这种编码将是不够的。例如，考虑一个只有一个规则R={r：s→s}的系统，它在同一个状态上循环。显然，在CTL中，s满足了公式EGs。 现在，考虑HyLL序列t[R]]@0;[s]]@wQC[[s]]@w。如果我们决定引入右边的连接词，我们就得到了形状的一个推导，[[R]]@0;[s]]@w[[s]]@w. v[[R]]@0;[s]]@wQC[[s]]@w↓R，R 在RJ. Despeyroux等人/理论计算机科学电子笔记332（2017）95107LL其中v是新鲜的。其次，如果我们使用[R]]@0中的蕴涵，我们就得到了形状的一个导子：[[R]]@0;[s]]@（w+1）Gcopy，，−[[R]]@0;[s]]@wG因此，左和右rig ht在序列t[R]]@0;[s]]@（k+n）[[s]] v@w中状态。v永远不会匹配，并且这个v是不可证明的。换句话说，上下文中的资源足以证明（有界）n的性质，但不是所有自然数。为了证明这一点，我们需要（元层次的）归纳，这与使用固定点是一样的。下一节将展示如何使用具有不动点运算符的线性逻辑来实现这一点4.2在具有不动点的线性逻辑中编码E和A量化器为了证明（在CTL中）状态s下的公式AFF，我们必须检查s是否满足F. 如果不是这样，我们必须检查AFF对所有的后继者都成立。s（即， 为了所有的sJ. t。 s==r<$sJ对于某个转移规则r）。因此，AF是递归的，它通常被描述为一个（最小）固定点。捕捉这种行为的一种方法是向HyLL添加定点运算符。但是依赖现有的系统来处理具有不动点的线性逻辑要简单得多。在下文中，我们证明了可以将从语法（1）构建的CTL公式表征到系统μMALL[3]中，该系统将线性逻辑（无指数）的最小和最大不动点相加。μMALL与线性逻辑共享加法和乘法连接词的所有证明规则以及以下两个规则6► Δ，St x<$B Sx，（Sx）<$► Δ，νBtνεΔ，B（μB）tμ► Δ，μBt其中S是（共）归纳不变式。μ规则对应于展开，v允许（共）归纳。路径量化器作为定点CTL量化器作为固定点的通常解释（参见例如，（4）EFF=μY.FEXYEGF=νY.FEXYE[FUG] =μY.G（FEXY）AFF=μY.FAXYAGF=νY.FAXYA[FUG] =μY.G（FAXY）在CTL中，假设所考虑的转换系统是串行的，即每个状态至少有一个后继。这意味着，在每个状态中，至少有一个可触发的规则。下一个定义展示了如何将CTL公式编码到μMALL中。6μMALL还考虑了平等和不平等的规则，但我们在开发中不需要它们108J. Despeyroux等人/理论计算机科学电子笔记332（2017）95C....（neg（s））（pos（s））（[[s]]）。（Y））（pos（s））（[[s]]）。（Y））..J. .[[AXF]]R=&s→s′∈R （neg（s））（pos（s））（[[s]]）。φ））J. ...C[[EXF]]R= s→s′∈R （pos（s））（[[s]]）。φ））J. ...[[AFF]]R=μ Y。φ&s→s′∈R （neg（s））（pos（s））（[[s]]）。（Y））J. ...C[[EFF]]R=μ Y。φ⊕s→s′∈R （pos（s））（[[s]]）。（Y））J. ...[[A GF]]R=νY。 φ& &s→s′∈R （neg（s））（pos（s））（[[s]]）。（Y））J. ...C[[EGF]]R=νY。φ&C[[A[FUG]R=μY..s→s′∈R（pos（s））（[[s]]）。（Y））J. .Σs→s′∈Rs→s′∈RJ. .Σ图3.第三章。在μMALL中对CTL临时操作的编码。在这里，φ=C[[F]]R和φ=C[[G]]R。定义4.1[CTL到μMALL]设R是一组转移规则。对于Q∈ {A，E}，QX、QF和QG的编码在图3中。给定一个状态s=p1（a1）<$· ·<$pn（ann）（如4.1节所述），我们定义：[[pres（ai）]]=ai[[abs（ai）]]=ai- 是的.. .⊥....[[s]]=[p1（a1）]]. ···[[pn（an）]][[p]]=pos（p）pos（s） =[p1（a1）]]··[[pn（an）]]=[[s]]neg（s） =（[p1（a1）]]T）·· ·（[[pn（an）]]T）其中p是状态公式。7最后，我们将CTL连接词和分别映射到&和。让我们给一些直觉。考虑规则r：s→sJ。公式pos（s）（分别neg（s））测试r是否可以（resp.不能）在当前状态下触发。 时间量化器的编码依赖于以下原则。对于每个转换规则，我们测试该规则是否可以被触发。如果它可以被触发，则当前状态被转换为新状态。A的编码（resp.E）测试所有（分别） （一）有火的规则。 这就解释了（resp.）&）.例4.2考虑时间公式AFF。我们首先检查F在当前状态下是否成立。如果不是这种情况，对于每个可触发的规则，我们消耗[[s]]（usingpos（s））并释放[sJ]]，从而更新当前状态。 对于实例，考虑序列[[s]]、C[[AFF]]R和对于公式F不保持在状态s的序列。通过对C[[AFF]]R的计算，我们可以获得形状的推导7允许state属性只提及V中命题变量的子集是有用的。在这种情况下，我们可以定义[pi（ai）] a bov e i，如果aio在p和T中发生，否则。CCφ&&C[[E[FUG]R=μY.φ&.J. Despeyroux等人/理论计算机科学电子笔记332（2017）95109- 是的、....- 是的...[[s]]，neg（s1）μB）.[[s]]，neg（s m）μB）μ，μ，&J. .J. .. .. .►[[s]]，μB前提对应于证明规则ri是否可触发。如果ri：si→sJi我们可以看到一个衍生的形状：► [[sJi]]，μBJ. .... . . .►[[s]]，pos（si）（[[si]]. （μB）..J. .► [[s]]，neg（si）（pos（si）（[[si]]）. μB））其中s变为sJi，从该状态必须证明μB注4.3注意，在图3的所有子句中，公式pos（s）J. ...([[s]]。 B、存在。我们可以写成[r]]−B，读起来更接近于我们期望的是公式（L− <$R）− <$B和L<$（R− <$B）不等价。事实上，第一个公式相当于（LR）。B而第二个等价于L <$（R. B）。 第一个更强大比第二个在这个意义上，B可以选择分支移动（L或R），而第二个迫使B坚持R。由于期望的行为是第二种，因此增加额外的可能性对证明搜索并不好定理4.4设V ={a1，...， an}是命题变量集，R是V上的一组变换规则，F是CTL公式，s|=RCTLF表示F在由R定义的转换系统中的状态s处成立。 这是|=RCTLFi表示该等式► [[s]]，C[[F]]R在μMALL中是