线性逻辑（二）
2.3 证明网
使用序贯演算提出的证明包含大量有时并不令人感兴趣的细节：例如，考虑一下有多少种不同的、毫无趣味的方式可以从⊢Γ,A1,A2,…,An的推导中得到⊢Γ,(A1⅋A2),…,(An−1⅋An)的证明。这个令人不快的事实源于序贯演算中证明的序贯性：如果我们想将一组包含n条规则的S应用于序贯的不同部分，即使它们彼此之间互不干扰，我们也无法一步完成！我们必须对它们进行序列化，即在S上选择一个线性顺序，并按照这个顺序在n步中应用这些规则。
一个自然而然的问题出现了：“是否存在一种证明表示，可以抽象出这些无趣的细节？”在直觉序列演算中，通过所谓的自然演绎，可以肯定地回答类似的问题，通过柯里-霍华德对应（Howard 1980），这与被称为λ演算的计算工具有着密切的联系。
对于线性逻辑，这种简洁的证明表示由证明网给出，证明网是一种类似图的结构，对于逻辑的MLL片段而言，它具有特别好的性质。实现这种表示的第一步是利用否定的对合性，将所有后继演算系统转换为一个单侧系统，其中后继的形式为⊢Γ。因此，由于没有左引入规则，规则数量减少了，但表达能力保持不变，因为可证明性保持不变。
对于MLL中的每个后继演算证明，都可以归纳地将一个证明网与相同的结论关联起来，如下所示：
对于简化为公理规则的证明，我们关联一个公理链接。
公理网
对于将切割规则应用于两个证明而得到的证明，我们首先归纳构建与这两个证明相关的证明网，然后使用切割链接将它们组合起来。
切割网构造
对于将张量规则应用于两个证明而得到的证明，我们首先归纳构建与这两个证明相关的证明网，然后使用张量链接将它们组合起来。
张量网构造
对于将平分规则应用于一个证明而得到的证明，首先归纳构建与该证明相关的证明网，然后添加一个“平分链接”。
平分网构造
所有这些都可以用超图（公式是节点，“链接”是带有假设和结论的定向超边）进行适当的形式化，并且我们可以将由MLL的序贯演算推导归纳构建的超图正式定义为证明网。需要注意的是，有很多超图并不是证明网。现在，如果你观察由⊢Γ,A1,A2,…,An得到的⊢Γ,(A1⅋A2),…,(An−1⅋An)的推导构建的证明网，你会发现所有规则应用顺序的痕迹都消失了。从某种意义上说，证明网是序列演算推导的等价类，这些等价类的规则应用顺序与可交换的规则的推导顺序相等。
假设现在有人带着一个由公理、截断、平分线和张量链接构建的巨大超图来找你，声称它实际上是一个证明的表示。你如何验证它实际上是一个证明的表示，而不是一个随机的结构？
执行这种正确性检查是一项挑战，它相当于为你的结构重建一个序列构造历史，对应于序列演算中的推导，乍一看似乎是一个非常复杂的问题。 MLL 证明网的第一个正确性准则，称为“长行程准则”，出现在 Girard 的原始论文中，是指数函数，Danos 和 Regnier (1989) 后来发现的 ACC（非循环连通）准则也是如此。然而，存在一个更有效的准则，称为可收缩性，由 Danos 和 Regnier 提出，最近被 Guerrini、Martini 和 Masini 重新表述为以下优雅的图解析准则：当且仅当超图通过以下图简化规则简化为单节点“网络”时，它才是证明网。
用于 MLL 证明网识别的图解析
简单地执行此检查可能需要二次时间（每次应用规则可能需要对图进行完整查找才能找到索引，并且我们需要执行与图中超链接数量相同的步骤）。 Guerrini (2011) 和 Murawski 和 Ong (2006) 给出了线性时间算法。Retoré (2003) 给出了另一种 MLL 证明网的正确性准则，其中给出了 MLL 的二次算法。
在证明网上，可以以一种特别简洁的方式执行割消。由于其并行性，割消可以通过两条简化规则在局部进行：
公理移动：
公理移动
乘法移动：
乘法移动
这些实际上是证明网上的计算规则，正确性准则可以轻松验证任何此类规则是否保持正确性，因此，证明网的简化仍然来自同一后序项的后序项演算证明。
因此，MLL 证明网中的割消可以在线性时间内完成，并为所有 MLL 给出一个简单、优雅的割消结果。
证明网方法可以扩展到更大的线性逻辑子集，但如何获得与MLL相同的优雅结果则不太清楚：例如，Girard 1987年提出的原始系统适用于MELL，通过将以下超图构造与四条指数规则关联起来：
收缩
收缩构造
弱化
弱化构造
遗弃
遗弃构造
提升，引入了“盒子”的概念，即围绕证明网某一部分的序列化标记，在图中具体化为围绕结论A和?Γ的证明网绘制的矩形。
提升构造
虽然这些构造及其相关的图约化与具有显式替换的λ演算有着惊人的相似性，正如Di Cosmo & Kesner (1997) 首次指出的那样，但它们与相应的序贯演算规则过于相似。对于MLL来说如此优雅的并行化效果在这里无法很好地延续。并且图约简规则涉及盒子，且非局部化。
为了恢复令人满意的系统，许多方案已经提出，从 Danos & Regnier (1995) 的方案开始，但我们想在此提及 Guerrini、Martini 和 Masini (Guerrini et al. 2003) 提出的非常优雅的方法，该方法巧妙地展示了模态逻辑的两级证明系统、MELL 的正确证明网以及 λ 演算中最优约简之间的联系。
Heijltjes 和 Houston (2016) 最近发表的一篇论文表明，如果允许单位，则 MLL 不可能有令人满意的证明网概念。
即使使用一阶量化，也可以提供加法连接词的规范处理 (Heijltjes et al. 2019)。包含乘法连接词和加法连接词的公式的证明网有各种技术表示，但没有一种看起来是规范的和令人满意的。在类似证明网的证明系统中如何处理它们，目前是一个热门的研究课题。具体而言，参见 (Hughes and van Glabbeek 2005) 和 (Hughes and Heijltjes 2016)。
3. 语义学
线性逻辑的语义研究通常沿着两条不同的路径进行。首先，存在各种语义结构，可用于将公式映射到此类结构中的指称。这种方法可用于确定各种线性逻辑片段的可靠性和完备性。一种更新颖的线性逻辑语义方法涉及直接赋予证明语义。我们简要介绍这两种方法，并提供一些文献链接。
3.1 可证性语义学
一种尝试为线性逻辑片段提供可靠且完备的语义的方法是，将所有可用于证明该公式的上下文集合与公式关联起来。当然，这样的集合可能需要更加抽象，并赋予其各种闭包性质。Girard (1987) 的相位语义提供了一种这样的语义：在计算机科学中，这种语义的一些用途已被用于提供反例，并作为一种工具，帮助确定一个给定的并发系统不能演化为具有某些性质的另一个系统 (Fages et al. 2001)。相位语义也被用于为一阶和高阶线性逻辑提供截消除的语义证明 (Okada 1999)。类似地，Allwein & Dunn (1993) 和 Hodas & Miller (1994) 也提供了 Kripke 风格的语义。Quantale 是一种偏序代数结构，早期也被用于为线性逻辑的某些部分提供语义模型 (Yetter 1990)。
3.2 证明的语义
在理论计算机科学中，公式即类型的类比非常流行且卓有成效。在这种类比中，一个逻辑系统被对应到一个类型化的计算设备（例如类型化的λ演算），方法是将公式的每个证明关联到一个以该公式为类型的程序。例如，重言式 A⇒A 的证明对应于程序 fun(x:A).x:A→A，即类型 A 对象的恒等函数。这就是为什么在构造性逻辑系统（例如直觉逻辑和算术）和线性逻辑中，证明如此重要，以至于构建和研究证明模型比构建和研究可证明性模型受到更多关注：我们不满足于知道一个公式是可证明的，我们真正想知道的是其证明的计算内容。
已经提出了许多线性逻辑证明模型；我们认为，迄今为止，最简单、最直观的构造是基于所谓的“关系语义”或“克里普克式语义”的构造，其中公式被解释为多重集，单边序列被解释为多重集的元组，证明被解释为序列解释上的关系（Tortora de Falco 2003, Ehrhard 2012, Melliès 2018）。如果想要给出纯粹的集合论语义，而不诉诸多重集，则可以通过相干空间（即具有特殊相干关系的集合）来实现，正如 Girard 1987 最初所展示的那样。线性逻辑有一些有趣的范畴论模型，例如 *-自治范畴（Barr 1991）和超相干（Ehrhard 1993）。
Girard 的《相互作用几何学》给出了另一种证明语义学方法，该方法使我们能够获得证明的完全代数刻画。对于每个证明网，可以关联一个对应于截断链接的部分置换矩阵 σ，以及一个对应于由某个动态代数构建的表达式的真矩阵 M，这些表达式描述了证明网内部的可能路径。然后，可以通过执行公式 EX(σ,M)=(1−σ2)(
∑
i
M(σM))(1−σ2) 来完整描述证明网，在 MLL 情况下，它是规范化过程的不变量。Abramsky & Jagadeesan (1994) 的一些早期工作已经展示了它与数据流理论结果之间的良好联系。
围绕所谓的博弈语义学发展起来的语义学领域值得特别关注。A. Blass (1992) 很早就指出了博弈与线性逻辑之间的紧密联系。事实上，将逻辑与游戏联系起来有两种不同的传统。在洛伦岑的对话游戏传统中，一位玩家尝试证明一个公式，而另一位玩家尝试反驳它。可以为MALL提供这样一种对话游戏，它对证明者和反驳者来说都是完全对称的（Delande等人，2010）。在另一种传统中，公式被解释为游戏，逻辑连接词被解释为游戏构造器，而证明则被解释为描述玩家如何应对对手动作的策略。通过对游戏规则施加不同的限制，人们实际上可以为实际编程语言的各种特性提供精确的语义（从技术上讲，是一个完全抽象的模型），因此过去几年人们对该领域产生了巨大的兴趣。例如，参见Abramsky & Jagadeesan 1994、Abramsky & Melliès 1999和Hyland & Ong 2000。
4. 复杂性
对于任何给定的逻辑，了解是否存在一个有效的程序来确定逻辑中每个句子是否可证明是非常有用的。可判定逻辑（即存在有效的可证明性程序的逻辑）通常用其复杂度类别来描述，该类别表征了执行判定程序的难度。大量的研究工作致力于探讨几个命题线性逻辑片段的复杂性和可判定性问题。已知
MLL 可证明性是 NP 完全的（Kanovich 1992），
MALL 可证明性是 PSPACE 完全的（Lincoln 等人 1992）。
这里，NP 和 PSPACE 是复杂度类别，满足 NP ⊆ PSPACE。令人惊讶的是，对于那些可能忘记线性逻辑的新颖性在于其公式的管理方式，而无需收缩和弱化的结构规则的人来说，即使我们关注只有常量而没有命题变量的逻辑片段，这些结果仍然保持不变。是允许的（Lincoln & Winkler 1994）。事实上，可以将任意公式编码为仅包含常数的公式，同时保持可证明性。
MELL 是一种表达能力出奇地强的逻辑。例如，Petri 网中的可达性问题可以编码到 MELL 中（Gunter & Gehlot 1989），而该问题等价于带状态向量加法系统 (VASS) 的可达性问题（Reutenauer 1989）。此外，MELL 的可判定性问题等价于分支 VASS 的可达性问题（de Groote 等人 2004），而后者已知具有非初等下界（Lazic and Schmitz 2015）。因此，如果 MELL 被证明是可判定的，它至少是 TOWER-hard（Lazic and Schmitz 2015）。 Bimbó (2015) 给出了 MELL 可判定性的证明，但 Straßburger (2019) 指出该证明存在缺陷。
关于命题线性逻辑不可判定性的证明发表于 20 世纪 90 年代初 (Lincoln et al. 1992, Lincoln 1995)。Kanovich (2016) 证明了，该不可判定性结果适用于大大简化的命题线性逻辑片段。并且，机器验证的不可判定性证明已发表于 (Forster & Larchey-Wendling, 2019)。然而，Bimbó & Dunn (2022) 也发表了关于命题线性逻辑可判定性的证明，他们也声称在上述论文中发现了错误。
添加了无限制弱化规则的线性逻辑（也称为线性仿射逻辑）是可判定的（Kopylov 1995），并且是指数空间难的（Urquhart 2000）。
Lincoln 1995 中对线性逻辑的复杂性结果进行了很好的概述。
5. 计算机科学的影响
直觉逻辑在上世纪初首次提出时，它被视为对传统数学家行事方式的挑战。排中律和矛盾证明法的使用被认为是可疑且有问题的，尤其是在无穷大的情况下。随着直觉主义逻辑关注点发展成为建设性数学，拓扑、代数和分析等主题出现了新的建设性方法。鉴于线性逻辑涵盖证明（算法）和资源的动态，其主要影响并非传统数学，而是计算机科学。在概述这种影响的性质之前，我们先概述一下逻辑在计算机科学中更广泛应用的各种方式。
逻辑在计算规范中扮演着不同的角色。我们可以识别以下几种不同的方法，并指出哪些角色受到了线性逻辑的影响。
在计算即模型方法中，计算被编码为数学结构，由节点、转换和状态等项组成。逻辑被外部用来对这些结构进行陈述。也就是说，计算被用作逻辑表达式的模型。内涵算子，例如时态逻辑和动态逻辑的模态算子，或霍尔逻辑的三元组，通常用于表达关于状态变化的命题。这种用逻辑来表示和推理计算的做法，可能是逻辑在表示计算方面最成功的应用。逻辑的这种作用几乎没有受到线性逻辑的影响。
在“计算即演绎”方法中，逻辑的语法片段（例如公式、术语、类型和证明）直接用作指定计算的元素。在这种更为稀疏的设定中，计算建模有两种截然不同的方法，分别称为证明规范化方法和证明搜索方法。
下文概述了线性逻辑对这两种不同环境的重大影响。
5.1 证明规范化
证明规范化方法将计算状态视为证明项，将计算过程视为规范化（也称为β归约或截取消除）。函数式编程可以用证明规范化作为其理论基础来解释（Martin-Löf 1982），并已被用于证明新函数式编程语言的设计，例如Abramsky 1993。线性逻辑为这种计算规范化方法提供了新的类型、新的声明性方法（用于静态理解资源在计算中的使用方式），并提供了一种有吸引力的方法来形式化函数与为其提供参数的环境之间的对偶性。
线性逻辑作为强大理论工具的另一个领域是最优归约。构建高效（最优）λ演算解释器的问题在J.J. Lévy最初定义λ演算之后很长一段时间内一直悬而未决，最终于1990年由Lamping首次解决，通过一个复杂的共享图实现，包含相当多的规则。许多作者运用线性逻辑的思想和直觉，重构了Lamping的解法，对其进行了简化，并衍生出一个与相互作用几何相关的丰富理论。如需进一步阅读，可参考Asperti & Guerrini 1998的著作。线性逻辑对直觉逻辑的精化以及线性逻辑的对偶性提供了一种环境，使人们可以将函数及其环境视为相似的、对偶相互作用的实体。例如，类型为 A−∘B 的函数可以建模为一个过程，该过程从其环境中消耗一个类型 A 的值，并将其转换为类型 B 的值。在线性逻辑中，这种蕴涵等价于其逆否形式：类型 B⊥−∘A⊥ 可以导致将同一函数解释为一个过程，该过程将对类型 B 的值的需求转换为对类型 A 的值的需求（请注意，直觉类型的函数不会发生这种情况，因为例如，输入参数可能为空）（Curien 2003）。近期使用博弈语义对函数计算进行建模的成功经验也与对函数和环境的对偶处理相关（Abramsky and Jagadeesan 1994，Hyland & Ong 2000）。
最后，我们提到，在将计算编码为证明规范化领域，线性逻辑已用于提供基于类型的多项式时间递归函数描述。例如，M. Hofmann (2003) 引入了一种具有模态和线性类型的λ演算，将 Bellantoni & Cook 1992 的函数代数扩展至更高类型。基于线性逻辑的类型也已用于函数式程序中：参见 Guzman & Hudak 1990 和 Wadler 1991。
5.2 证明搜索
证明搜索方法将计算状态视为一个后继项（结构化的公式集合），将计算过程视为寻找后继项证明的过程：后继项中发生的变化捕捉了计算的动态。基于这种计算视角，我们通常自下而上地解读推理规则，即作为将其结论转化为其前提的过程。逻辑编程可以用证明搜索作为其理论基础来解释，而线性逻辑为这种计算规范提供了新的组合子，用于构建逻辑程序，新的捕捉丰富动态的方法，以及新的声明式方法来指定并发计算。（有关线性逻辑编程语言的概述，请参阅 Miller 2004。）
