线性逻辑笔记

学习CMU 15-816的一些翻译和笔记.

第1章 演绎推理

第1.1节 例子: 对于图进行推理

作为第一个例子, 我们考虑图 (graph). 我们将结点 (node) (顶点, vertex) 表示为常量(constant) ($\mathsf{a}$, $\mathsf{b}$, ...) , 而边 (edge) 表示为一个二元谓词(predicate)$\mathsf{edge}$, 其将相互连接的结点联系起来.

以上的示例图可以被表示为命题(proposition) (原文的命题为复数形式)$$\mathsf{edge}(\mathsf{a},\mathsf{b}),\mathsf{edge}(\mathsf{b},\mathsf{c}),\mathsf{edge}(\mathsf{a},\mathsf{c}),\mathsf{edge}(\mathsf{a},\mathsf{d})$$读者可能会立即注意到一点不太匹配的地方, 即图片中的边似乎是无向的 (undirected), 而对于边的表示并非对称 (例如, $\mathsf{edge}(\mathsf{b},\mathsf{a})$就并不存在). 我们可以修复这点不足之处, 通过提供一条推理规则(rule of inference)以要求$\mathsf{edge}$关系是对称的 (symmetric).$$\frac{\mathsf{edge}(x,y)}{\mathsf{edge}(y,x)}\mathsf{sym}$$我们可以应用这条推理规则于事实$\mathsf{edge}(\mathsf{a},\mathsf{b})$以推导出 (deduce) $\mathsf{edge}(\mathsf{b},\mathsf{a})$. 在这个应用里, 我们实例化 (instantiate) 了模式变量(schematic variable)$x$和$y$以$\mathsf{a}$和$\mathsf{b}$. 模式变量会以斜体排版, 以将其与常量区分. 水平线之上的命题被称为规则的前提(premise), 而水平线之下的命题则被称为结论(conclusion). 这条作为例子的规则只有一个前提和一个结论. $\mathsf{sym}$是这条规则的名字(name)或者说标签(label). 我们经常省略规则的名字, 如无引用规则的特别需要的话.

根据这条单一规则和描述初始图的事实, 我们现在可以推导出以下额外的事实:$$\mathsf{edge}(\mathsf{b},\mathsf{a}),\mathsf{edge}(\mathsf{c},\mathsf{b}),\mathsf{edge}(\mathsf{c},\mathsf{a}),\mathsf{edge}(\mathsf{d},\mathsf{a})$$此时此刻我们尚不能在图与其逻辑表示之间来回切换, 因为一个孤立的结点不会出现在边关系里. 因此, 我们需要第二个谓词$\mathsf{node}$, 其对于图中的每个结点成立.$$\mathsf{node}(\mathsf{a}),\mathsf{node}(\mathsf{b}),\mathsf{node}(\mathsf{c}),\mathsf{node}(\mathsf{d})$$

既已设计了图的一种逻辑表示, 现在我们定义图上的一个关系. 如果图中存在一条从$x$到$y$的路径 (path), 我们记$\mathsf{path}(x,y)$. 对于图而言常见的情况是, 我们不想考虑平凡的从一个结点到自身的零长度路径. 如果我们的确要考虑的话, 那将会是以下规则 (写在方括号里以指示这仅是假想性的):$$\left[\frac{\mathsf{node}(x)}{\mathsf{path}(x,x)}\mathsf{refl}\right]$$如果我们省略了这条规则的前提, 那么这个规则是成问题的, 因为其可以用于甚至并非图的结点的对象$x$, 导致毫无意义 (nonsensical) 的结论.

现在以下的两条规则定义了路径的概念. 第一条$\mathsf{e}$是说每条边都代表了一条合法 (valid) 的路径, 第二条$\mathsf{trans}$是说路径可以被复合 (compose), 使得$\mathsf{path}$成为传递关系.$$\frac{\mathsf{edge}(x,y)}{\mathsf{path}(x,y)}\mathsf{e}\frac{\mathsf{path}(x,y)\mathsf{path}(y,z)}{\mathsf{path}(x,z)}\mathsf{trans}$$根据对于我们示例图的表示, 现在可以提供以下存在从$\mathsf{c}$到$\mathsf{d}$的路径的证明:$$\frac{\frac{\frac{\mathsf{edge}(\mathsf{a},\mathsf{c})}{\mathsf{edge}(\mathsf{c},\mathsf{a})}\mathsf{sym}}{\mathsf{path}(\mathsf{c},\mathsf{a})}\mathsf{e}\frac{\mathsf{edge}(\mathsf{a},\mathsf{d})}{\mathsf{path}(\mathsf{a},\mathsf{d})}\mathsf{e}}{\mathsf{path}(\mathsf{c},\mathsf{d})}\mathsf{trans}$$我们可以检视这个证明, 然后发现其携带了一些信息. 它不仅仅是为了说服我们存在一条从$\mathsf{c}$到$\mathsf{d}$的路径, 而是告诉了我们路径是什么. 这条路径从$\mathsf{c}$出发走到$\mathsf{a}$, 然后从$\mathsf{a}$走到$\mathsf{d}$. 这是一个关于证明中的构造性内容(constructive content)的例子, 而我们之后将会看到诸多其他的例子. 对于目前我们已有的系统而言, 从一般角度来说, 我们的确可以从证明中读出路径, 并且如果我们心中有一条路径, 则总是可以构造一个证明. 但是, 以我们选择的规则而言, 一些路径并不对应于唯一的证明. [译注: 这最后一句话里的路径 (path) 指的是实际所走的路线, 例如对于结点$x$和$y$, 如果我们拥有对于$\mathsf{path}(x,y)$的一个证明, 那么说明存在一条实际的可以从$x$走到$y$的路. 但是, 对于这条实际的路线而言, 也可以存在不同的证明. 读者需要理解的是, $\mathsf{path}(x,y)$存在证明只是说明至少存在一条路线, 但是可以有各种不同的路线, 而且甚至不同的证明可以对应于相同的路线, 或者说相同的构造性内容. 原文没有特别区分路径和实际所走的路线. 而且, 根据后文, 其实每种路线都可以有无限多不同的证明.]

实际上, 歧义的来源不止一处. [译注: 这里的歧义指同一路径的不同证明可以拥有相同的实际路线.] 一方面是我们可以从$\mathsf{edge}(\mathsf{c},\mathsf{a})$回到$\mathsf{edge}(\mathsf{a},\mathsf{c})$然后再回到$\mathsf{edge}(\mathsf{c},\mathsf{a})$, 如此反复下去, 可以产生无限多的对于$\mathsf{edge}(\mathsf{c},\mathsf{a})$的证明. 另一方面, 具有多于三个结点的路径可以被分解为不同的子路径, 由此以不同的方式使用传递性. 不同的证明可以拥有相同的构造性内容并没有使得其解释不合理, 但是我们应该意识到这件事情的存在.

既然我们排除了自反性, 在何种条件下我们仍然可以证明$\mathsf{path}(x,x)$呢? 因为我们考虑的是无向图, 存在一条从$x$到$x$的路径恰当$x$至少存在一个邻居 (neighbor), 正如以下证明所示:$$\frac{\frac{\mathsf{edge}(x,y)}{\mathsf{path}(x,y)}\mathsf{e}\frac{\frac{\mathsf{edge}(x,y)}{\mathsf{edge}(y,x)}\mathsf{sym}}{\mathsf{path}(y,x)}\mathsf{e}}{\mathsf{path}(x,x)}\mathsf{trans}$$这个证明存在诸多有趣的方面. 例如, 它不依赖于$x$和$y$到底是什么. 换言之, 其对于$x$和$y$是模式性的(schematic). 另一值得注意的方面在于其用了$\mathsf{edge}(x,y)$两次, 而这在直觉上是成立的: 离开$x$然后回到$x$的一般方法是先去到任意相邻的$y$, 然后立即返回$x$, 复用相同的边. 我们可以将以上的推导 (deduction) 总结为一条单独的导出推理规则(derived rule of inference):$$\frac{\mathsf{edge}(x,y)}{\mathsf{path}(x,x)}$$这条推理规则是合理的 (justified), 因为我们可以将其任意的特定实例替换以我们上面给出的模式性证明的一个实例. 我们将在之后的讲座里看到, 导出推理规则在逻辑学中扮演着非常重要的角色.

第1.2节 例子: 自然数

作为第二个例子, 我们考虑自然数$0,1,2,\dots$. 一种构造自然数的便捷方法是通过迭代应用后继函数$\mathsf{s}$于$\mathsf{0}$, 记作$$\mathsf{0},\mathsf{s}(\mathsf{0}),\mathsf{s}(\mathsf{s}(\mathsf{0})),\dots$$我们将$\mathsf{s}$称为一个构造子(constructor). 现在我们可以通过以下三条规则定义偶数和奇数.$$\frac{}{\mathsf{even}(\mathsf{0})}\frac{\mathsf{even}(x)}{\mathsf{odd}(\mathsf{s}(x))}\frac{\mathsf{odd}(x)}{\mathsf{even}(\mathsf{s}(x))}$$作为导出推理规则的例子, 我们可以将左边的证明总结为右边的规则:$$\frac{\frac{\mathsf{even}(x)}{\mathsf{odd}(\mathsf{s}(x))}}{\mathsf{even}(\mathsf{s}(\mathsf{s}(x)))}\frac{\mathsf{even}(x)}{\mathsf{even}(\mathsf{s}(\mathsf{s}(x)))}$$这些例子里的证明的结构都不是特别有趣, 因为数 (number, 这里是动词) 数字$n$为奇还是偶的证明不过就是遵循数字$n$的结构罢了.

第1.3节 例子: 硬币交换

到目前为止, 演绎推理总是在积累知识, 因为我们已经所意识到为真的命题仍然保持为真. 线性逻辑起源于一个简单的观察:

Truth is ephemeral.

作为一个例子, 我们考虑值$5$分钱的nickel, 值$10$分钱的dime, 值$25$分钱的quarter. 我们拥有如下用于在它们之间进行交换的规则:$$\frac{\mathsf{d}\mathsf{d}\mathsf{n}}{\mathsf{q}}\frac{\mathsf{q}}{\mathsf{d}\mathsf{d}\mathsf{n}}\frac{\mathsf{n}\mathsf{n}}{\mathsf{d}}\frac{\mathsf{d}}{\mathsf{n}\mathsf{n}}$$第二条和第四条规则是我们第一次看到具有多于一个结论的规则. 现在推理可以改变状态. 例如, 如果我们有三个dime和一个nickel, 那么状态可以写成$$\mathsf{d},\mathsf{d},\mathsf{d},\mathsf{n}$$应用第一条规则, 我们可以将两个dime和一个nickel转换为一个quarter以得到状态$$\mathsf{d},\mathsf{q}$$注意到总钱数$35$分保持未变, 这是硬币交换的要义. 一种写下这样的推理的方式在于划去被消费的命题而加上产生的命题. 对于以上例子而言, 我们可以写成$$\mathsf{d},\mathsf{d},\mathsf{d},\mathsf{n}\rightsquigarrow \cancel{\mathsf{d}},\cancel{\mathsf{d}},\mathsf{d},\cancel{\mathsf{n}},\mathsf{q}$$为了理解证明的意义, 考虑如何将三个dime换为一个quarter和一个nickel: 首先, 我们将一个dime换为两个nickel, 然后再将剩下来的两个dime和其中一个nickel换为一个quarter. 正如以下两次状态转移所示:$$\mathsf{d},\mathsf{d},\mathsf{d}\rightsquigarrow \mathsf{d},\mathsf{d},\cancel{\mathsf{d}},\mathsf{n},\mathsf{n}\rightsquigarrow \cancel{\mathsf{d}},\cancel{\mathsf{d}},\cancel{\mathsf{d}},\cancel{\mathsf{n}},\mathsf{q},\mathsf{n}$$使用推理规则的记号, 这个推导显示在左边, 而相应的导出推理规则在右边.$$\frac{\mathsf{d}\mathsf{d}\mathsf{n}}{\mathsf{q}}\frac{\mathsf{d}}{\mathsf{n}\mathsf{n}}\frac{\mathsf{d}\mathsf{d}\mathsf{d}}{\mathsf{q}\mathsf{n}}$$[译注: 左边两个证明其实是一个证明的组件, 但是限于MathML的排版能力, 我实在不知道存在什么优雅的方式可以将它们组合起来, 只好暂时作罢.]

总结一下: 我们可以改变推理的本质 (very nature), 如果我们消费前提中所用的命题以产生结论中的命题. 这是线性逻辑的基础, 因此我们将其称为线性推理(linear inference). 以下是提醒我们的精辟之语:

Linear inference can change the world.

第1.4节 例子: 画图 (Graph Drawing)

我们继续来看一个牵涉线性推理的稍微复杂一点的例子. 之前我们使用了常规的演绎推理以定义路径的概念. 这次我们想要模拟不提起笔画图. 这与遍历整个图而每条边恰走一次是等价的. [译注: 这里说的画图其实就是一笔画问题.] 这种重述暗示了以下的想法: 当我们沿着一条边走的时候, 我们就消费了这条边, 于是我们不能再走一次这条边. 我们也需要追踪我们在哪里, 因此我们引入了新的谓词$\mathsf{at}$, 其满足$\mathsf{at}(x)$为真, 如果我们在结点$x$这个位置上. 然后, 唯一的线性推理规则是$$\frac{\mathsf{at}(x)\mathsf{edge}(x,y)}{\mathsf{at}(y)}\mathsf{step}$$和前一节一样我们从某个初始状态出发: 对于每条从$x$到$y$的边都有一个$\mathsf{edge}(x,y)$, 对称规则成立 (因为是无向图), 起始位置表示为$\mathsf{at}(x_0)$. [译注: 这里一条(无向)边只对应于一个命题, 原文的说法其实有点问题. 另外, 对称规则现在也是线性的了, 因为我们需要避免重复走过相同的(无向)边.] 我们可以看到我们每走一步 (通过应用上述的$\mathsf{step}$规则), 我们都是消耗了一个事实$\mathsf{at}(x)$, 然后产生了另一个事实$\mathsf{at}(y)$, 因此状态里总是恰好存在一个具有$\mathsf{at}(-)$形式的事实. 并且, 每一步我们也消耗了一个$\mathsf{edge}(-,-)$事实, 因此我们最多能走的步数和初始图中的边数相等. 当然了, 如果我们位于一个点$x$, 那么可能有许多条出边, 而若我们选择了错误的那条, 可能就不能完成一笔画了, 但是至少在每个点处我们可以尝试的选择是有限的. 如果我们能够抵达这样一个状态, 即没有形式为$\mathsf{edge}(-,-)$的事实, 那么我们就成功了, 或者说找到了不提起笔而画完图的方法, 并且最终的位置为$\mathsf{at}(x_n)$.

以下的示例图来源于一首德国童谣, 并且如果从$\mathsf{b}$或者$\mathsf{c}$出发我们就可以一笔画, 但是如果从$\mathsf{a}$, $\mathsf{d}$, 或$\mathsf{e}$出发则不行.$$\frac{\frac{\frac{\frac{\frac{\frac{\frac{\frac{\mathsf{at}(\mathsf{b})\mathsf{edge}(\mathsf{b},\mathsf{a})}{\mathsf{at}(\mathsf{a})}\mathsf{step}\mathsf{edge}(\mathsf{a},\mathsf{e})}{\mathsf{at}(\mathsf{e})}\mathsf{step}\mathsf{edge}(\mathsf{e},\mathsf{d})}{\mathsf{at}(\mathsf{d})}\mathsf{step}\mathsf{edge}(\mathsf{d},\mathsf{c})}{\mathsf{at}(\mathsf{c})}\mathsf{step}\mathsf{edge}(\mathsf{c},\mathsf{b})}{\mathsf{at}(\mathsf{b})}\mathsf{step}\mathsf{edge}(\mathsf{b},\mathsf{d})}{\mathsf{at}(\mathsf{d})}\mathsf{step}\mathsf{edge}(\mathsf{d},\mathsf{a})}{\mathsf{at}(\mathsf{a})}\mathsf{step}\mathsf{edge}(\mathsf{a},\mathsf{c})}{\mathsf{at}(\mathsf{c})}\mathsf{step}$$这是从$\mathsf{b}$出发的一笔画的证明树.$$\frac{\frac{\frac{\frac{\frac{\frac{\frac{\frac{\mathsf{at}(\mathsf{c})\mathsf{edge}(\mathsf{c},\mathsf{d})}{\mathsf{at}(\mathsf{d})}\mathsf{step}\mathsf{edge}(\mathsf{d},\mathsf{e})}{\mathsf{at}(\mathsf{e})}\mathsf{step}\mathsf{edge}(\mathsf{e},\mathsf{a})}{\mathsf{at}(\mathsf{a})}\mathsf{step}\mathsf{edge}(\mathsf{a},\mathsf{b})}{\mathsf{at}(\mathsf{b})}\mathsf{step}\mathsf{edge}(\mathsf{b},\mathsf{c})}{\mathsf{at}(\mathsf{c})}\mathsf{step}\mathsf{edge}(\mathsf{c},\mathsf{a})}{\mathsf{at}(\mathsf{a})}\mathsf{step}\mathsf{edge}(\mathsf{a},\mathsf{d})}{\mathsf{at}(\mathsf{d})}\mathsf{step}\mathsf{edge}(\mathsf{d},\mathsf{b})}{\mathsf{at}(\mathsf{b})}\mathsf{step}$$这是从$\mathsf{c}$出发的一笔画的证明树.

第1.5节 例子: 图遍历

第1.6节 例子: 积木世界

接下来我们考虑积木世界(blocks world), 这是人工智能的历史里一个重要的例子.

第1.7节 例子: King Richard III

第1.8节 例子: 机会

一条常见的谚语如下:

Opportunity doesn't knock twice. —Anonymous

第1.9节 练习

第2章 从规则到命题

第2.1节 例子: 生成树

第2.2节 例子: 乞丐

第2.3节 同时合取

线性推理规则可以拥有多个前提和多个结论. 如果我们试着将水平线想成是某种形式的二元联结词 (实际上那应该会是$A⊸B$), 那么我们需要一种方法将前提打包成单独一个命题, 并且也要将结论打包成单独一个命题. [译注: 因为前提和结论都有可能不止一个.] 这是同时合取(simultaneous conjunction)或者说乘性合取(multiplicative conjunction)$A\otimes B$的目的所在了. $A\otimes B$为真, 如果$A$和$B$在相同的状态里都为真. 因此, 如果我们拥有$A\otimes B$, 我们可以将其替换以$A$和$B$:$$\frac{A\otimes B\mathit{eph}}{A\mathit{eph}B\mathit{eph}}$$另一个方向似乎也是直接的: 我们可以得到$A\otimes B$, 如果我们既有$A$也有$B$:$$\frac{A\mathit{eph}B\mathit{eph}}{A\otimes B\mathit{eph}}$$但是这已经造成了问题, 比如说如果我们想要表明$$\frac{A\otimes B\mathit{eph}}{B\otimes A\mathit{eph}}$$是一条导出推理规则, 那么证明可能会写成以下这样:$$\frac{\frac{A\otimes B\mathit{eph}}{A\mathit{eph}B\mathit{eph}}}{B\otimes A\mathit{eph}}$$一点小的恼人之处在于最后一条规则的前提的顺序是错误的. 然而, 更重要的地方在于, $A\otimes B\mathit{eph}$在最后一条规则的两个前提的证明里都有出现, 这似乎违背了线性推理的基础: 瞬态事实只能使用一次! [译注: 这段话其实有点令我迷惑, 因为使用$A\otimes B\mathit{eph}$其实产生了两个新的命题, 这并没有什么不对的地方. 当然了, 这可能是为了后文引入管理推理 (其中包括推理中的命题) 的相继式演算作铺垫.]

或许人们可以试图提供什么标准, 用以判断类似于上面的紧凑结构的确是合法的证明. 但是, 这样的标准通常相当复杂, 而且与线性逻辑不完全契合 (don't scale well to all of linear logic). 一种看起来更有前途也更加一般的替代选择是急剧地 (drastically) 改变我们的推理记号, 那正是我们下一节要做的事情. [译注: 之前的推理都是一种原始自然演绎式的, 其规则有多个结论的情况和自然演绎的树结构不太契合. 当然了, 不是说没有线性逻辑的自然演绎, 但是线性逻辑的自然演绎还是要用到相继式的 (不过那不叫相继式演算).]

第2.4节 资源和目标

现在我们转移到一种记号上来, 其主要的判断 [译注: 其实就是相继式] 显式追踪了我们在推理过程中所有使用了的瞬态命题. 我们写下$$\underset{\mathrm{\Delta }}{\underbrace{A_1\mathit{eph},\dots ,A_n\mathit{eph}}}⊢C\mathit{eph}$$将$\mathrm{\Delta }$的部分视为资源(resources)而$C$当成我们要达成的目标 (goal). 为了证明这个东西, 我们需要在我们可以达成$C$的证明中使用$\mathrm{\Delta }$的所有资源恰好一次(exactly once). 这是来源于Gentzen的相继式演算(sequent calculus)的相继式(sequent)的一个例子, [Gen35]这篇开创性论文标志着证明论作为研究主题的开始. 然而, Gentzen的论文具有允许我们复制或者擦除假设的结构规则, 但是在这里被有意省略了. [译注: 结构规则从指称或者语义角度来看是显然的, 然而从证明论的角度来看反而是相继式演算里最重要的部分. 线性逻辑实际上可以说始于这样的观察.]

以相继式的记号, 我们现在可以写下$$\frac{\mathrm{\Delta }⊢A\mathit{eph}{\mathrm{\Delta }}^{\prime }⊢B\mathit{eph}}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢A\otimes B\mathit{eph}}\otimes R$$在结论中, 我们将证明$A$所需要的资源$\mathrm{\Delta }$和证明$B$所需要的资源${\mathrm{\Delta }}^{\prime }$组合起来. 这两个子证明之间不能共享资源, 因为这将违背资源的瞬态本质. [译注: 这里的共享其实含义有点微妙, 因为有的时候在某种意义上一些资源可以是相同的, 这样的资源可能有许多份, 然而这并非共享, 因为共享指的是包含本质上相同 (或者说同一/等同) 的资源. 当然了, 这也是在说我们不能在组合的时候随意复制或者擦除, 要保留原样.] 另一方面, 资源的顺序并不重要, 因此我们允许其自由地重新排列.

以上是右规则(right rule)的一个例子, 其表明了该如何证明一个命题 (也就是说, 达成一个目标). [译注: 因此, $\otimes R$的意思是如何得到一个同时合取呢?] 反过来, 我们不得不刻画如何使用一个命题. 我们以左规则(left rule)来完成此事, 其分解当前资源集合里的一个资源. 这里的左规则是直截了当的.$$\frac{\mathrm{\Delta },A\mathit{eph},B\mathit{eph}⊢C\mathit{eph}}{\mathrm{\Delta },A\otimes B\mathit{eph}⊢C\mathit{eph}}\otimes L$$[译注: 这是相继式演算和自然演绎不同的地方, 右规则相当于自然演绎的引入规则, 左规则相当于自然演绎的消去规则.] 我们不能随意地发明这样的联结词的左规则和右规则. 最终我们希望我们的系统里的逻辑命题有着符合期望的含义, 不论是从直觉角度还是从形式角度. 接下来的章节里解释了一些我们可以运用的标准.

第2.5节 identity和cut

从基础上来讲, 我们需要在左侧的资源和右侧的目标之间达成平衡. 这种平衡独立于我们所拥有的特定的联结词集合——其应该对于任意的命题成立.

第一条规则, 叫做identity, 陈述了一个资源$A$自身应该总是足够能达成目标$A$.$$\frac{}{A\mathit{eph}⊢A\mathit{eph}}{\mathsf{id}}_A$$在这条规则里, 我们必须足够谨慎, 不应该引入任何额外的未使用资源, 因为其解释是严苛的 (tight): 任何资源都必须恰好用到一次. 我们经常将规则所应用于的命题附到规则名称的下标上, 因为这样的信息在我们对于相继式演算的研究中是重要的.

第二条规则, 叫做cut, 陈述了相反方向的事实: 达成一个目标$A$允许 (license) 我们假设 (assume) $A$作为一个资源.$$\frac{\mathrm{\Delta }⊢A\mathit{eph}{\mathrm{\Delta }}^{\prime },A\mathit{eph}⊢C\mathit{eph}}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C\mathit{eph}}{\mathsf{cut}}_A$$在这条规则里, 我们需要小心地将来源于两段前提的假设组合起来, 这当然也是因为前提中的资源都必须恰好被使用一次 (不论是在对于$A$的证明中还是在使用了$A$的对于$C$的证明中).

这两条规则有时被称为判断规则(judgmental rule), 因为其关心的是判断的本质 (这里指的是judgments of being a resource and a goal), 或者说结构规则(structural rule), 因为其并不检视命题, 而只检视相继式的结构.

本次讲座的剩余部分里我们将会省略判断注记 (judgment annotation) $\mathit{eph}$, 因为暂时这些注记总是相同的.

第2.6节 identity展开

接下来我们开始讨论应用于检查我们对于联结词的定义的标准, 在于左规则和右规则是否相互一致. 第一条标准是检查我们是否能够通过对于更小类型的identity规则的使用来消除对于复合类型的identity规则的使用. 这意味着左规则和右规则配合得足够充分以至于我们可以推导出identity规则的实例.$$\frac{}{A\otimes B⊢A\otimes B}{\mathsf{id}}_{A\otimes B}{\to }_E\frac{\frac{\frac{}{A⊢A}{\mathsf{id}}_A\frac{}{B⊢B}{\mathsf{id}}_B}{A,B⊢A\otimes B}\otimes R}{A\otimes B⊢A\otimes B}\otimes L$$我们使用${\to }_E$表示展开一个identity规则为一个使用更小的命题的identity规则的证明. 这之所以被称为展开 (expansion), 是因为证明变得更大, 即便命题变得更小.

请注意我们是如何使用$A\otimes B$的左规则和右规则的, 并且它们的确配合良好以能够推导出对于$A\otimes B$而言的identity规则.

第2.7节 cut归约

另一种判断规则是cut, 其也可以用来判断相同联结词的左规则和右规则是否配合良好. 这次我们需要表明我们可以归约a cut at $A\otimes B$为cuts at $A$ and $B$.$$\frac{\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime }⊢B}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢A\otimes B}\otimes R\frac{{\mathrm{\Delta }}^{″},A,B⊢C}{{\mathrm{\Delta }}^{″},A\otimes B⊢C}\otimes L}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime },{\mathrm{\Delta }}^{″}⊢C}{\mathsf{cut}}_{A\otimes B}$$$${\to }_R$$$$\frac{{\mathrm{\Delta }}^{\prime }⊢B\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{″},B,A⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{″},B⊢C}{\mathsf{cut}}_A}{{\mathrm{\Delta }}^{\prime },\mathrm{\Delta },{\mathrm{\Delta }}^{″}⊢C}{\mathsf{cut}}_B$$[译注: 译者实现了一个用于排版证明树的DSL, 但是相当受限, 尤其是其检查证明的合法性的机制过于严格, 以至于我这里必须放弃合法性检查. 另外, 这个证明树和原文稍有区别, 因为它没有调整其中一些顺序. 严格地说, 交换顺序应该编码为结构规则, 但是这个讲义为了简单起见只是非形式化地处理交换.] 我们再次看到了资源处于平衡状态: 我们在证明并使用$A\otimes B$时并不会获得或者损失任何的资源.

之后的讲座里我们将会看到, cut归约实际上是线性逻辑的一些计算性解释背后的引擎.

第2.8节 线性implication

译注: 我故意不翻译implication的原因在于翻译了之后就总是容易和entailment, deduction甚至inference打架, 然而它们的区别从英文看是一目了然的. 其实我发现最早翻译逻辑学文献的人可能就没有真的理解这些概念, 导致了一些非常奇怪的问题, 比如说implication和entailment被很多人都翻译成了同一个词, 即蕴涵. 当然了, 逻辑学自身的用语和符号有时就令人迷惑, 比如说相继式 (sequent) 和句法/逻辑蕴涵 (syntatic/logical entailment) 往往都使用相同的符号$⊢$.

最后, 我们回到表达推理规则的原始问题上来. 想法在于用一个quarter交换两个dime和一个nickel的规则$$\frac{\mathsf{q}}{\mathsf{d}\mathsf{d}\mathsf{n}}$$变成了$$\mathsf{q}⊸\mathsf{d}\otimes \mathsf{d}\otimes \mathsf{n}$$除了 (except that) 规则本身是永恒的, 而命题不是, 除非我们采取特殊安排.

$A⊸B$的意思是如果我们有了一个$A$, 我们可以获得一个$B$. [译注: 这里原文说了大声朗读 (笑). 另外, 这里的获得当然指的是用$A$交换$B$.] 因此, 如果我们有(一个)$A⊸B$, 并且我们可以获得一个$A$, 那么这是我们使用$B$的许可 (license).$$\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime },B⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime },A⊸B⊢C}⊸L$$反过来, 为了表明我们可以达成$A⊸B$, 我们需要表明如何在额外假设我们拥有一个$A$的条件下达成$B$.$$\frac{\mathrm{\Delta },A⊢B}{\mathrm{\Delta }⊢A⊸B}⊸R$$让我们来检查它们是否协调一致. 首先, identity展开:$$\frac{}{A⊸B⊢A⊸B}{\mathsf{id}}_{A⊸B}{\to }_E\frac{\frac{\frac{}{A⊢A}{\mathsf{id}}_A\frac{}{B⊢B}{\mathsf{id}}_B}{A,A⊸B⊢B}⊸L}{A⊸B⊢A⊸B}⊸R$$接着是cut归约:$$\frac{\frac{\mathrm{\Delta },A⊢B}{\mathrm{\Delta }⊢A⊸B}⊸R\frac{{\mathrm{\Delta }}^{\prime }⊢A{\mathrm{\Delta }}^{″},B⊢C}{{\mathrm{\Delta }}^{\prime },{\mathrm{\Delta }}^{″},A⊸B⊢C}⊸L}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime },{\mathrm{\Delta }}^{″}⊢C}{\mathsf{cut}}_{A⊸B}$$$${\to }_R$$$$\frac{\frac{{\mathrm{\Delta }}^{\prime }⊢A\mathrm{\Delta },A⊢B}{{\mathrm{\Delta }}^{\prime },\mathrm{\Delta }⊢B}{\mathsf{cut}}_A{\mathrm{\Delta }}^{″},B⊢C}{{\mathrm{\Delta }}^{\prime },\mathrm{\Delta },{\mathrm{\Delta }}^{″}⊢C}{\mathsf{cut}}_B$$[译注: 又来写点无聊的译注了, 首先作者稍微调整了一下$\mathrm{\Delta },{\mathrm{\Delta }}^{\prime },{\mathrm{\Delta }}^{″}$的出现顺序, 这可能是为了让cut归约前的证明树看起来更漂亮一点 (其实也没有), 不过其实也没有必要. 下面的证明树我没有关闭检查, 因此呈现细节和原文不同 (相继式里命题出现的顺序不同), 但当然没有实质区别.] 幸运的是, 这两条规则的确相当和谐 (in harmony).

之后的讲座将会继续引入新的联结词和规则.

第3章 和谐

之前的讲座里我们开始建立线性逻辑的命题联结词. 具体来说, 我们引入了同时合取$A\otimes B$和线性implication $A⊸B$. 每种联结词都以相继式演算的左规则和右规则确定, 其刻画了如何使用一个资源以及如何证明带有这种联结词的目标. 我们也阐述了两种用以判断逻辑联结词是否具备意义的测试: identity展开和cut归约. 如果它们都成立, 那么我们就称这个联结词的左规则和右规则是和谐的(in harmony). 现在我们继续建立新的联结词, 并探索左规则和右规则之间和谐的失败会导致什么后果.

第3.1节 乘性单位元

每当我们有了一个二元运算符时, 目前的情况是$A\otimes B$, 我们应该考虑是否它具有单位元. 在当前的情况下, 这个单位元记作$\mathbf{1}$, 其具有$A\otimes \mathbf{1}$和$\mathbf{1}\otimes A$都等价于$A$的性质. 我们可以试着系统地推导$\mathbf{1}$的性质, 通过将其想成是零元的乘性合取. 以下, 我们先展示二元的规则, 然后再展示零元的规则.$$\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime }⊢B}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢A\otimes B}\otimes R\frac{}{\cdot ⊢\mathbf{1}}\mathbf{1}R$$$A\otimes B$具有两个部分 (component), 因此$\otimes R$具有两个前提. 对应地, $\mathbf{1}$没有部分, $\mathbf{1}R$也没有前提. 这也意味着我们要求这里不应该存在资源, 由$\cdot$指明. 总结一下, 如果我们没有资源, 那么$\mathbf{1}$作为目标成立.

现在来看左规则:$$\frac{\mathrm{\Delta },A,B⊢C}{\mathrm{\Delta },A\otimes B⊢C}\otimes L\frac{\mathrm{\Delta }⊢C}{\mathrm{\Delta },\mathbf{1}⊢C}\mathbf{1}L$$$A\otimes B$具有两个部分, 因此它们都在前提里作为新资源出现. 鉴于$\mathbf{1}$没有部分, 故前提中没有新资源出现.

$\mathbf{1}$的左规则和右规则是平衡的. 首先, 局部展开:$$\frac{}{\mathbf{1}⊢\mathbf{1}}{\mathsf{id}}_{\mathbf{1}}{\to }_E\frac{\frac{}{\cdot ⊢\mathbf{1}}\mathbf{1}R}{\mathbf{1}⊢\mathbf{1}}\mathbf{1}L$$接着, 归约:$$\frac{\frac{}{\cdot ⊢\mathbf{1}}\mathbf{1}R\frac{{\mathrm{\Delta }}^{\prime }⊢C}{{\mathrm{\Delta }}^{\prime },\mathbf{1}⊢C}\mathbf{1}L}{{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_{\mathbf{1}}{\to }_R{\mathrm{\Delta }}^{\prime }⊢C$$

我们应该验证$A\otimes \mathbf{1}$等价于$A$. 但是, 这是何意呢? 我们将其视为$A\otimes \mathbf{1}⊢A$且$A⊢A\otimes \mathbf{1}$. 我们只给出一个示例证明, 另一个方向和其他版本应该是容易证明的.$$\frac{\frac{\frac{}{A⊢A}{\mathsf{id}}_A}{A,\mathbf{1}⊢A}\mathbf{1}L}{A\otimes \mathbf{1}⊢A}\otimes L$$以下是译者补充的另一个方向的证明树.$$\frac{\frac{}{A⊢A}{\mathsf{id}}_A\frac{}{\cdot ⊢\mathbf{1}}\mathbf{1}R}{A⊢A\otimes \mathbf{1}}\otimes R$$

乘性单位元在对于消去 (eliminate) 资源的描述中是有用的, 使用习语 (idiom) $A⊸\mathbf{1}$.

第3.2节 和谐的失败

我们现在以一种情况检视和谐的失败所导致的后果. 让我们假定我们将同时合取的左规则替换为了以下两条规则:$$\frac{\mathrm{\Delta },A⊢C}{\mathrm{\Delta },A\otimes B⊢C}\otimes L_1\mathrm{??}\frac{\mathrm{\Delta },B⊢C}{\mathrm{\Delta },A\otimes B⊢C}\otimes L_2\mathrm{??}$$[译注: 这样的规则显然在线性逻辑中并不正确, 因为它们类似于弱化, 引入了冗余的资源.] 首先我们注意到identity展开是失败的. 以下展示了我们的一次尝试, 其他的也会以类似的方式失败. [译注: 其他的大概指的是cut归约吧.]$$\frac{}{A\otimes B⊢A\otimes B}{\mathsf{id}}_{A\otimes B}{\to }_E\frac{\frac{\frac{}{A⊢A}{\mathsf{id}}_A\stackrel{\mathrm{??}}{\cdot ⊢B}}{A⊢A\otimes B}\otimes R}{A\otimes B⊢A\otimes B}\otimes L_1\mathrm{??}$$实际上, 根据这两条不正确的规则, 弱化(weakening)$$\frac{\mathrm{\Delta }⊢C}{\mathrm{\Delta },A⊢C}\mathsf{weaken}$$将会成为导出推理规则. 当然, 这违反了我们关于瞬态资源必须恰被使用一次的基本原则, 因为$A$的确没有被使用.

第3.3节 alternative合取

使用我们对于硬币交换的规则, 我们可以证明$\mathsf{q}⊢\mathsf{d}\otimes \mathsf{d}\otimes \mathsf{n}$以及$\mathsf{q}⊢\mathsf{q}$. 但是, 显然我们不能证明$\mathsf{q}⊢(\mathsf{d}\otimes \mathsf{d}\otimes \mathsf{n})\otimes \mathsf{q}$, 因为这样我们就要在证明中使用(作为这个相继式前提的)$\mathsf{q}$两次了. 不过, 根据资源$\mathsf{q}$, 我们实际上仍然可以证明这两者! [译注: 这里指的大概是通过资源$\mathsf{q}$, 既可以证明$\mathsf{d}\otimes \mathsf{d}\otimes \mathsf{n}$, 也可以证明$\mathsf{q}$, 但不能同时证明.] 为了表达这种情况, 在逻辑里我们将其写作一个联结词$A\&B$, 读作$A$ with $B$. 它可以被称为alternative合取或者加性合取(additive conjunction). 以这个联结词, 现在我们可以证明$\mathsf{q}⊢(\mathsf{d}\otimes \mathsf{d}\otimes \mathsf{n})\&\mathsf{q}$. 我们可以由资源$\mathrm{\Delta }$达成$A\&B$作为目标恰当我们可以由$\mathrm{\Delta }$达成$A$且由$\mathrm{\Delta }$达成$B$.$$\frac{\mathrm{\Delta }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Delta }⊢A\&B}\&R$$这表面上违反了线性 (linearity): 似乎$\mathrm{\Delta }$的资源被复制了. 但是我们是安全的, 因为当我们拥有一个资源$A\&B$时, 我们不得不在$A$和$B$之间选择一个. 我们不能两个都要. 这意味着$\mathrm{\Delta }$并没有真的被复制, 因为两个前提中只有一个将会被使用, 很快我们就会验证这个事实.$$\frac{\mathrm{\Delta },A⊢C}{\mathrm{\Delta },A\&B⊢C}\&L_1\frac{\mathrm{\Delta },B⊢C}{\mathrm{\Delta },A\&B⊢C}\&L_2$$$\mathrm{\Delta }$的复制并不会破坏linearity的非正式理由反映在identity展开和cut归约之中. 在归约中体现得更清楚, 因此我们先展示cut归约.$$\frac{\frac{\mathrm{\Delta }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Delta }⊢A\&B}\&R\frac{{\mathrm{\Delta }}^{\prime },A⊢C}{{\mathrm{\Delta }}^{\prime },A\&B⊢C}\&L_1}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_{A\&B}{\to }_R\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime },A⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_A$$实际上, 还有另外一个对称的归约, 其cut的第二个前提由$\&L_2$推得. 因为很简单, 所以这里译者补充一下.$$\frac{\frac{\mathrm{\Delta }⊢A\mathrm{\Delta }⊢B}{\mathrm{\Delta }⊢A\&B}\&R\frac{{\mathrm{\Delta }}^{\prime },B⊢C}{{\mathrm{\Delta }}^{\prime },A\&B⊢C}\&L_2}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_{A\&B}{\to }_R\frac{\mathrm{\Delta }⊢B{\mathrm{\Delta }}^{\prime },B⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_B$$

第3.4节 加性单位元

第3.5节 析取

第3.6节 析取单位元

第3.7节 永恒事实