线性逻辑（三）
聚焦证明系统的完备性可用于对线性逻辑中逻辑编程的部分操作语义提供声明式解释。例如，考虑仅由连接词 ⊤、&、−∘、⇒ 和 ∀ 构建的线性逻辑公式子集 L。（注意，如果将 ⊥ 添加到此列表中，则可以对线性逻辑的所有连接词进行编码。）可以看出，L 中的无截断证明搜索可以定义为到阶段。给定一个序数 Γ； Δ⊢G，其中Γ是一组公式（可以收缩和弱化），Δ是公式的多集（既不能收缩也不能弱化），G（“目标”公式）是一个单一公式（全部来自L），则证明搜索按如下方式进行。
如果G是非原子的，则只能使用右引入规则来推断该后序式。给定这组连接词，右规则是可逆的，并且此目标归约阶段恰好对应于焦点证明的异步阶段。
如果G是原子的，则证明搜索通过从左侧上下文中确定一个公式来进行。
一旦选定一个公式作为焦点，所有左引入规则都只应用于该公式以及任何出现的正子公式。此回溯链接阶段对应于焦点证明构造的异步阶段。
形式上，这些不同的阶段可以用以下推理规则来描述。这里引入了一个新的序列箭头：该箭头标有左引入规则得出的公式。注意，−∘ 的左引入规则要求将 Δ 上下文拆分为 Δ1,Δ2 两部分（自下而上阅读规则时）。当然，如果该上下文包含 n≥0 个不同的公式，则有 2n 种这样的拆分。这些推理规则中的句法变量 A 涵盖原子公式。
目标降低阶段
γ;Δ⊢⊤
⊤R
γ;Δ⊢Bγ;Δ⊢C
γ;Δ⊢B&C
与研究
γ;Δ,B⊢C
γ;Δ⊢B−∘C
−∘R
γ,B;Δ⊢C
γ;Δ⊢B⇒C
⇒R
γ;Δ⊢B[y/x]
γ;Δ⊢∀x.B
∀R
回链阶段
γ;Δ|
D1
_
一个
γ;Δ|
D1&D2
_
一个
&L
γ;Δ|
D2
_
一个
γ;Δ|
D1&D2
_
一个
&L
γ;Δ|
D[t/x]
_
一个
γ;Δ|
∀τx.D
_
一个
∀L
γ;Δ1⊢Gγ;Δ2|
D
_
一个
γ;Δ1,Δ2|
G−∘D
_
一个
−∘L
γ;·⊢Gγ;Δ|
D
_
一个
γ;Δ|
G⇒D
_
一个
⇒L
身份和决策规则
γ,D;Δ|
D
_
一个
γ,D;Δ⊢A
决定！
γ;Δ|
D
_
一个
γ;Δ,D⊢A
决定
γ;·|
一个
_
一个
初始化
限于 L 的线性逻辑可以被视为线性逻辑编程语言。因此，它可以作为计算系统的规范语言，Petri 网、过程演算、λ 演算等也承担着这一角色。鉴于线性逻辑具有证明理论和各种语义，线性逻辑的元理论为 L 中指定的计算提供了广泛的推理途径。
鉴于线性逻辑的后继演算使用公式的多集，证明搜索可以直接编码多集重写。由于许多计算可以自然地看作是多集重写，因此人们可以在线性逻辑与 Petri 网（Gunter & Gehlot 1989）、过程演算（Andreoli & Pareschi 1991、Kobayashi 等人 1999、Miller 1996）之间建立许多联系。和安全协议（Cervesato 等人，1999 年，Miller，2003 年）。
6. 变体
6.1 模态的不同处理
如果使用传统的序贯演算表示，指数函数在以下意义上不是规范的：如果引入指数函数的另一个副本，例如 !′ 和 ?′，并使用与原始指数函数相同的规则，则无法证明 ! 等价于 !′，? 等价于 ?′，而对于其他连接词，这很容易建立。非规范指数函数的各种应用可以在 (Danos 等人，1993 年；Nigam & Miller，2009 年) 中找到。尽管 MELL 的可判定性目前正在争论中（Bimbó，2015 年，Straßburger，2019 年），但将 MLL 扩展为三对 ! 和 ?产生的逻辑是不可判定的 (Chaudhuri 2018)。Martini 和 Masini 1995 描述了一个“2-序列”证明系统，其中指数函数是规范的。
切割消元法可以使经典逻辑和直觉逻辑中的证明规模变得非常庞大，这一事实可以通过在这些证明系统中应用收缩规则来分析。如果证明系统对收缩规则引入限制，就可以设计出新的逻辑和证明系统，使其切割消元法的复杂度大大降低。例如，初等线性逻辑 (ELL) 可以通过用一条同时引入 ! 和 ? 的规则替换 ! 和 ? 的引入来获得。因此，ELL 可以编码所有且仅能编码卡尔玛初等函数（可在固定高度的指数塔时间内计算）（Girard 1998，Baillot 2015）。此外，人们也研究了指数函数推理规则的其他变体。 例如，轻线性逻辑 (Girard 1998) 和软线性逻辑 (Lafont 2004) 均刻画可在多项式时间内计算的函数：另见 (Baillot & Terui 2004)。
6.2 非交换线性逻辑
虽然线性逻辑拒绝弱化和收缩这两条结构规则的普遍应用，但它允许不受限制地使用称为交换的结构规则。不普遍使用交换规则的后序演算具有左右上下文均为列表的后序：上下文中公式的顺序成为逻辑的表达元素。在这种情况下，乘法析取和合取可以变为非交换的。
Lambek 1958 年提出了第一个拒绝所有三条后序演算结构规则的逻辑之一。虽然该逻辑包含两个蕴涵式，但它既不包含否定，也不包含任何指数。许多论文都提出扩展线性逻辑以包含非交换特性，但目前似乎没有一个提案是规范的。有关非交换线性逻辑的示例，请参阅 Yetter 1990、Abrusci 1991、Retoré 1997、Abrusci & Ruet 1999 以及 Guglielmi & Straßburger 2001。
6.3 无界行为的处理
虽然 MALL 逻辑是一种富有表现力的新颖逻辑，但它也是可判定的，因此无法捕捉迭代和递归等操作中的无界行为。如上所述，指数 ! 和 ? 的添加将 MALL 扩展为完全线性逻辑，并使其能够捕捉无界行为。扩展 MALL 以捕捉无界行为的第二种方法是将最小和最大不动点运算符作为逻辑连接词直接添加到 MALL 中。为了正确地将不动点表征为最小或最大，不动点的推理规则必须是“高阶的”，即它们包含不变量。Baelde 开发了 MALL 的这种扩展（也包含一阶量化和项相等性）（Baelde & Miller，2007；Baelde，2012），并已用于为模型检验提供证明理论基础（Heath & Miller，2018）。
