线性逻辑（二）

对于 MLL 中的每个后续微积分证明，我们可以归纳地将证明网与相同的结论关联起来，如下所示：

对于简化为公理规则的证明，我们关联一个公理链接。

公理网

对于通过将剪切规则应用于两个证明而获得的证明，我们首先归纳构建与这两个证明相关的证明网，然后使用剪切链接将它们组合起来。

剪网施工

对于通过将张量规则应用于两个证明而获得的证明，我们首先归纳构建与这两个证明相关的证明网，然后使用张量链接将它们组合起来。

张量网络构建

对于通过将 par 规则应用于证明而获得的证明，首先归纳构建与该证明关联的证明网络，然后添加“par 链接”。

帕网建设

所有这些都可以使用超图来正确地形式化（公式是节点，“链接”是带有假设和结论的定向超边），并且我们可以将根据 MLL 的连续微积分推导归纳构建的超图正式定义为证明网。请注意，有相当多的超图不是证明网。

现在，如果您查看从 ⊢Γ,A1,A2,...,An 获得的 ⊢Γ,(A1⅋A2),...,(An−1⅋An) 的推导构建的证明网，您将看到所有迹规则的应用顺序已经消失。从某种意义上说，证明网是关于其应用可交换的规则的推导顺序的连续微积分推导的等价类。

假设现在有人给你带来了一个用公理、割、par 和张量链接构建的巨大超图，声称它实际上是证明的表示。如何验证它实际上是证明的表示，而不仅仅是随机结构？

执行这种正确性检查是一项挑战，相当于为您的结构重建顺序构造历史，对应于顺序微积分中的推导，并且乍一看似乎是一个非常复杂的问题。 MLL 证明网的第一个正确性标准，称为“长行程标准”，出现在 Girard 的原始论文中，是指数的，以及后来发现的 Danos 和 Regnier (1989) 的 ACC（非循环连通）标准。然而，存在一个更有效的标准，称为可收缩性，由 Danos 和 Regnier 提出，最近由 Guerrini、Martini 和 Masini 重新表述为以下优雅的图解析标准：超图是一个证明网当且仅当它通过以下图形简化规则简化为单例节点“net”

MLL 证明网络识别的图解析

单纯地执行此检查可能会花费二次时间（规则的每个应用可能需要对图形进行整个查找才能找到 redex，并且我们需要执行与图形中的超链接一样多的步骤）。 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 等人 2003)，它清楚地表明了模态逻辑的两级证明系统之间的连接、MELL 的适当证明网以及 λ 演算的最优简化。

Heijltjes 和 Houston (2016) 最近发表的一篇论文表明，如果也允许单位，那么 MLL 就不可能有令人满意的证明网概念。

即使使用一阶量化，也可以提供加性连接词的规范处理（Heijltjes et al. 2019）。包含乘法和加法连接词的公式的证明网有各种技术演示，但没有一个看起来规范且令人满意。它们在类似证明网的证明系统中的处理是目前活跃研究的主题。特别请参阅（Hughes 和 van Glabbeek 2005）和（Hughes 和 Heijltjes 2016）。

3. 语义

接近线性逻辑的语义通常沿着两条不同的路径完成。首先，有各种可用的语义结构可用于将公式映射到此类结构中的表示。该方法可用于建立线性逻辑各种片段的健全性和完整性。线性逻辑的一种更新颖的语义方法涉及直接为证明提供语义。我们简要描述这两种方法并提供一些文献链接。

3.1 可证明性的语义

尝试为线性逻辑片段提供健全且完整的语义的一种方法将公式与可用于证明该公​​式的所有上下文的集合相关联。当然，这样的集合可能需要更加抽象并被赋予各种闭包属性。 Girard (1987) 的阶段语义提供了一种这样的语义：在计算机科学中已经使用了这种语义来提供反例，并作为一种工具来帮助确定给定的并发系统不能演变成具有某些属性的另一个系统（Fages et等，2001）。阶段语义也被用来为线性逻辑的一阶和高阶版本提供割消除的语义证明（Okada 1999）。类似地，Kripke 风格的语义已在 Allwein & Dunn 1993 和 Hodas & Miller 1994 中提供。Quantales 是某种偏序代数结构，早期也被用来为部分线性逻辑提供语义模型 (Yetter 1990) ）。

3.2 证明的语义

在理论计算机科学中如此流行且富有成果的公式作为类型的类比中，逻辑系统与类型化的计算设备（如类型化的 λ 演算）相对应，通过将该公式的每个证明与一个程序相关联，该公式作为一种类型。例如，重言式 A⇒A 的证明对应于程序 fun(x:A).x:A→A，即类型 A 的对象上的恒等函数。这就是为什么，在构造性逻辑系统（例如直觉逻辑）中和算术），并且在线性逻辑中，证明非常重要，以至于构建和研究证明模型比构建和研究可证明性模型受到更多关注：我们不满足于知道一个公式是可以证明，我们真的想要了解其证明的计算内容。

已经提出了许多线性逻辑证明模型；我们认为，迄今为止，最简单、最直观的构造是基于所谓的“关系语义”或“克里普克式语义”的构造，其中公式被解释为多重集，单边序列被解释为元组多重集，证明被解释为序列解释上的关系（Totora de Falco 2003，Ehrhard 2012，Melliès 2018）。如果一个人想给出一种纯粹的集合论语义，而不诉诸多重集，可以通过连贯空间、具有特殊连贯关系的集合来实现，如 Girard 1987 最初所示。有一些有趣的范畴论线性逻辑模型，例如*-自治类别（Barr 1991）和超相干（Ehrhard 1993）。

吉拉德的交互几何给出了另一种证明语义的方法，它使我们能够获得证明的完全代数表征。对于每个证明网，可以将与切割链接相对应的部分置换矩阵 σ 和由特定动态代数构建的对应表达式关联起来，描述证明网内的可能路径。然后可以通过执行公式完整地描述证明网

EX(σ,M)=(1−σ2)(

Σ

我

M(σM))(1−σ2)

在 MLL 情况下，这是归一化过程的不变量。 Abramsky 和 ​​Jagadeesan (1994) 的一些早期工作已经展示了与数据流理论结果的一些良好联系。

围绕所谓的游戏语义发展起来的语义领域值得特别关注。 A. Blass (1992) 很早就指出了游戏和线性逻辑之间的紧密联系。事实上，将逻辑与游戏联系起来有两种不同的传统。在对话游戏的传统中，可以追溯到洛伦岑，一个玩家试图证明一个公式，而另一个玩家则试图反驳它。可以为MALL提供这样一个对于证明者和反驳者来说完全对称的对话游戏（Delande et al. 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 et al. 2004），并且后者已知具有非基本下界（Lazic and Schmitz 2015）。因此，如果 MELL 被证明是可判定的，那么它至少是 TOWER-hard 的（Lazic 和 Schmitz 2015）。 Bimbó (2​​015) 给出了 MELL 可判定性的证明，但 Straßburger (2019) 报告了该证明中的缺陷。

命题线性逻辑不可证明的证据在1990年代初发表（Lincoln等，1992，Lincoln 1995）。 Kanovich（2016）表明，这种不可证明的结果大大减少了命题线性逻辑的片段。并在（Forster＆Larchey-Wendling，2019年）中发布了一个机器检查的证明。但是，Bimbó＆Dunn在（2022年）中也发表了命题线性逻辑的可决定性证明，他们还声称在上述论文中发现了错误。

添加了无限制的弱化规则（也称为线性仿射逻辑）的线性逻辑是可决定的（Kopylov 1995）和指数空间（Urquhart 2000）。

在Lincoln 1995中可以找到围绕线性逻辑的复杂性结果的良好概述。

5。计算机科学影响

当直觉逻辑是在上个世纪初首次提出的，这是对传统数学家应该做生意的方式的挑战。被排除的中间和逐次证明的使用被认为是可疑和有问题的，尤其是在无限的存在下。随着直觉逻辑的关注已发展为建设性数学，诸如拓扑，代数和分析等主题已经出现了新的建设性方法。鉴于线性逻辑涵盖了证明的动态（算法）和资源，因此其主要影响不是在传统数学中，而是在计算机科学中。在概述这种影响的性质之前，我们概述了计算机科学中更普遍使用逻辑的各种方式。

逻辑在计算规范中扮演着不同的角色。我们可以确定以下广泛的不同方法，并注意哪些角色会受到线性逻辑的影响。

在计算方法中，计算被编码为数学结构，由节点，过渡和状态等项目组成。逻辑在外部用于对这些结构发表陈述。也就是说，计算用作逻辑表达式的模型。强化运算符，例如时间和动态逻辑的模态或Hoare逻辑的三元组，通常被用来表达有关状态变化的命题。逻辑来表示和理由的这种使用可能是最广泛成功地用来代表计算的逻辑。逻辑的这种角色对线性逻辑几乎没有影响。

在计算方法中，逻辑的语法（例如公式，术语，类型和证明）直接用作指定计算的元素。在这种更稀少的环境中，有两种相当不同的方法来建模计算，称为证明归一化方法和证明搜索方法。

我们概述了线性逻辑对这两种不同设置的重大影响的概述。

5.1证明归一化

证明归一化方法将计算状态视为证明项，计算过程是归一化的（替代称为β还原或切割）。功能编程可以使用证明正差为其理论基础（Martin-Löf1982）来解释，并已被用来证明新功能编程语言的设计合理，例如Abramsky，1993年。线性逻辑提供了这种计算规范的方法，该方法具有新的类型，新的类型，新的声明性手段，用于静态理解如何在计算中使用资源，并提供了一种吸引人的手段，以形式化函数与为其提供参数的环境之间的双重性。

线性逻辑是一种强大的理论仪器的另一个领域是最佳减少。为λ-calculus建立高效（最佳）口译员的问题，在J.J.原始定义的原始定义之后，该问题一直保持开放。莱维（Lévy）是通过涉及大量规则的复杂图表实现的1990年在灯光中首次解决的。许多作者利用线性逻辑的想法和直觉，重建了Lamping的解决方案，简化了它并导致了与互动几何相关的丰富理论。为了进一步阅读，良好的参考是Asperti＆Guerrini 1998。

线性逻辑提供的直觉逻辑的完善和线性逻辑的双重性提供了一个设置，可以将函数及其环境视为双重交互的类似实体。例如，具有A -∘B类型的函数可以建模为一种从其环境中消耗A类型的值并将其转换为类型B的值。 ：类型b⊥ -∘a⊥可以导致将相同的函数解释为将对B型值的需求转化为对A类型值的需求的过程（请注意，这不会发生在直觉类型，例如，输入参数可能是空置的）（Curien 2003）。使用游戏语义对功能计算进行建模的最新成功与功能和环境的双重处理相似（Abramsky and Jagadeesan 1994，Hyland＆Ong 2000）。

最后，我们提到，在编码计算作为证明归一化的领域中，线性逻辑已用于提供基于类型的Poly Time递归函数的描述。例如，M。Hofmann（2003）引入了一个具有模态和线性类型的λ-calculus，将Bellantoni＆Cook 1992的函数代数扩展到更高类型。基于线性逻辑的类型也已在功能程序中使用：参见Guzman＆Hudak 1990和Wadler 1991。

5.2证明搜索

证明搜索方法将计算的状态视为序列（公式的结构化集合）和计算过程作为搜索序列证明的过程：依次进行的更改捕获了计算的动力学。有了这种计算观点，我们通常会读到推论规则底部底部，即将其结论转换为前提。可以使用证明搜索作为其理论基础来解释逻辑编程，而线性逻辑为构建逻辑程序的新组合提供了这种计算规范的方法，捕获丰富动态的新方法以及新的声明性方法来指定并发计算。 （有关线性逻辑编程语言的概述，请参见Miller 2004。）

重点证明系统的完整性可用于提供线性逻辑中逻辑编程的部分操作语义的声明性解释。例如，考虑仅根据连接词⊤，＆，−∘，⇒和∀构建的线性逻辑公式的子集l。 （请注意，如果一个人在此列表中添加⊥，则可以编码线性逻辑的所有连接器。）可以看到可以将L中的无剪切证明搜索定义为阶段。给定一个序列γ; Δgg，其中γ是一组公式（可以收缩和削弱），δ是公式的多组（不能收缩或削弱），g（“目标”公式）是一个单一公式（全部来自l），然后进行证明搜索进行如下。

数学联邦政治世界观提示您：看后求收藏（笔尖小说网http://www.bjxsw.cc），接着再看更方便。