线性逻辑笔记

学习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$$identity展开为$$\frac{}{A\&B⊢A\&B}{\mathsf{id}}_{A\&B}{\to }_E\frac{\frac{\frac{}{A⊢A}{\mathsf{id}}_A}{A\&B⊢A}\&L_1\frac{\frac{}{B⊢B}{\mathsf{id}}_B}{A\&B⊢B}\&L_2}{A\&B⊢A\&B}\&R$$

第3.4节 加性单位元

就像乘性合取具有单位元$\mathbf{1}$一样, 加性合取也存在零元的版本. 这个单位元是$\top$ (读作top). 和之前一样, 其规则也可由加性合取的规则系统地推导出来. 右规则具有零个前提, 将资源$\mathrm{\Delta }$传播到它们所有身上. [译注: 原文是all of them, 指的是每个作为前提的相继式的右侧的命题. 因为现在没有前提, 所以它们的加性合取应该是$\top$.] $A\&B$具有两个conjunct, 因此存在两条左规则; $\top$具有零个conjunct, 因此只有零条左规则.$$\frac{}{\mathrm{\Delta }⊢\top }\top R\text{没有}\top L\text{规则}$$当然了, 现在没有cut归约, 因为$\top$没有左规则. [译注: 因此, 没有办法在相继式的左侧引入$\top$.] 但是, 我们仍然有一个identity展开.$$\frac{}{\top ⊢\top }{\mathsf{id}}_{\top }{\to }_E\frac{}{\top ⊢\top }\top R$$

第3.5节 析取

我们已经看到alternative合取代表了某种选择. 如果我们拥有一个资源$A\&B$, 那么我们可以在我们的证明中选择使用$A$或者$B$. 如果我们有了一个目标$A\&B$, 那么我们需要考虑两种使用方式.

析取和alternative合取是对称的. 如果我们有了一个资源$A\oplus B$, 那么环境必须提供$A$或者$B$, 因此我们需要考虑两种可能性. [译注: 读者应该结合下面的规则理解这句话.] 反过来, 如果我们有了一个目标$A\oplus B$, 我们可以通过提供$A$或者提供$B$来满足这个目标.$$\frac{\mathrm{\Delta }⊢A}{\mathrm{\Delta }⊢A\oplus B}\oplus R_1\frac{\mathrm{\Delta }⊢B}{\mathrm{\Delta }⊢A\oplus B}\oplus R_2\frac{\mathrm{\Delta },A⊢C\mathrm{\Delta },B⊢C}{\mathrm{\Delta },A\oplus B⊢C}\oplus L$$我们将identity展开和cut归约留作练习5.

第3.6节 析取单位元

也存在着一个析取的单位元$\mathbf{0}$, 其是一种falsehood的形式. 我们可以通过将其视为零元版本的析取来得到其规则.$$\text{不存在}\mathbf{0}R\text{规则}\frac{}{\mathrm{\Delta },\mathbf{0}⊢C}\mathbf{0}L$$我们将其性质留作练习6.

第3.7节 永恒事实

要添加的最困难的联结词是为了将永恒事实内化 (internalize) 为一个命题. 实际上出于许多目的, 保留判断$A\mathit{pers}$是比较方便的, 尽管这并非唯一的选择. 这使得一个将瞬态事实判断和永恒事实判断联系起来的判断性规则显得必要. 但是, 首先我们需要对于相继式进行泛化, 将瞬态命题和永恒命题分离. 我们记$$\underset{\mathrm{\Gamma }}{\underbrace{B_1\mathit{pers},\dots ,B_k\mathit{pers}}};\underset{\mathrm{\Delta }}{\underbrace{A_1\mathit{eph},\dots ,A_n\mathit{eph}}}⊢C\mathit{eph}$$现在我们的规则将需要尊重相继式的瞬态本性. [译注: 原文这句话有缺漏, 或许译者的理解也并不正确.] 永恒和瞬态资源现在由分号$;$隔开以至于我们可以通过资源在相继式中的位置来判断其状态 (status).

首先, 我们有这样一条判断性规则, 其允许我们作出一个永恒资源的瞬态复制.$$\frac{\mathrm{\Gamma },A\mathit{pers};\mathrm{\Delta },A\mathit{eph}⊢C\mathit{eph}}{\mathrm{\Gamma },A\mathit{pers};\mathrm{\Delta }⊢C\mathit{eph}}\mathsf{copy}$$这条规则可以应用于任意的$A$. 可能读者想问是否也存在一条对于目标$C\mathit{pers}$而言的相应结构规则. 如果真有这样的规则, 那么其会是 [译注: 和之前一样, $\cdot$代表没有资源.]$$\left[\frac{\mathrm{\Gamma };\cdot ⊢A\mathit{eph}}{\mathrm{\Gamma };\cdot ⊢A\mathit{pers}}\mathsf{valid}\right]$$

第3.8节 Of Course!

既已定下涵盖永恒性的相继式扩展, 我们现在可以将其集成于命题之中. 对于表达了$A$永恒地为真的命题, 我们写下$!A$ (读作of course $A$或者bang $A$). 我们也将$!A$称为指数模态(exponential modality). 其左规则取$!A$的一个瞬态资源, 将其标记为永恒的.$$\frac{\mathrm{\Gamma },A\mathit{pers};\mathrm{\Delta }⊢C\mathit{eph}}{\mathrm{\Gamma };\mathrm{\Delta },!A\mathit{eph}⊢C\mathit{eph}}!L$$右规则要求$A$永恒地为真, 其相当于在没有瞬态资源的情况下$A$瞬态地为真.$$\frac{\mathrm{\Gamma };\cdot ⊢A\mathit{eph}}{\mathrm{\Gamma };\cdot ⊢!A\mathit{eph}}!R$$这两条规则之间是和谐的吗? 让我们检查一下. 从现在开始我们省略$\mathit{eph}$和$\mathit{pers}$, 因为我们总能根据其在相继式中的位置进行分辨. 首先是identity展开:$$\frac{}{\cdot ;!A⊢!A}{\mathsf{id}}_{!A}{\to }_E$$

第4章 作为计算的cut归约

本次讲座我们将会检视以相继式形式化 (formulation) 的线性逻辑的一种计算性解释. 很大程度上我们遵循了一篇最近的论文Caires et al. [CPT12] 的进路, 这篇论文包含了额外的细节和更深的参考. 基本的想法在于命题对应于会话类型(session type) [Hon93], 证明对应于$\pi$演算 [MPW92] 中的进程表达式 (process expression), 而cut归约对应于进程归约. 我们并不假定你已经了解了$\pi$演算, 尽管如果你了解的话显然理解讲座会变得更轻松一些.

第4.1节 解释判断

在函数式的背景 (functional setting) 下, 基本的判断一般具有$M:A$的形式, 其含义要么是$M$为$A$的一个证明, 要么是$M$为类型$A$的一个项. 在通信进程 (communicating process) 的背景下, 言称$P$为类型$A$的一个进程是意味不明的. 进程与它们的环境进行交流, 故我们转而写下$P::x:A$, 意为$P$是一个进程, 其沿着信道$x$提供服务$A$. 这里的信道被认为是一个以$P$为作用域 (scope) 的变量, 因此我们可以将其重命名为$P\{y/x\}::y:A$, 只要$y$还没有在$P$中用到. 根据惯例, 合适的时机我们将会悄无声息地执行这样的换名.

进程是无趣的, 除非它们被置于这样的上下文下, 其中进程不仅提供服务, 也使用其他进程提供的服务. 我们写下一个相继式$$x_1:A_1,\dots ,x_n:A_n⊢P::x:A$$以表达当进程$P$与沿着$x_i$提供$A_i$的进程$P_i$ ($1\le i\le n$) 一起时, 其沿着信道$x$提供服务$A$. 所有的变量$x_i$都必须是互异的. 这其实只是对于一个相继式$\mathrm{\Delta }⊢A$的装饰, 其唯一地标记了结论以及$\mathrm{\Delta }$中的所有资源. 对于资源我们仍然写下$\mathrm{\Delta }$, 不过现在它们被标记以信道.

提供和使用服务是相对应的 (counterparts), 但是它们并不相同. 因此, 形式上, 相继式右侧的判断$x:A$和相继式左侧的判断$x_i:A_i$应该被认为是不同的. 既然我们总是可以凭借位置来分辨判断的意图, 那么两者我们都会使用相同的记号.

进程随着沿信道的交互演化. 故信道$x_i$上的交互会产生 (engender) 状态上的变化, 而相同的信道不能再以相同的类型被使用了. 因此, 这里的turnstile符号$⊢$代表的是线性假言判断(linear hypothetical judgment) [CCP03], 其中每个前件 (antecedent) 都必须恰被使用一次. 也就是说, 上下文并不服从于弱化或者收缩规则, 但是重新排列是允许的, 因为前件被标识以唯一的名字.

即便还没有定义任何特定种类的服务, 一些原则应该是对于一般性的判断成立. 我们先讨论这些原则, 因为它们对于剩余部分的发展也是重要的指引.

第4.2节 作为复合的cut

当一个进程$P$沿着$x$提供服务$A$, 且另一个进程$Q$沿着$x$使用服务$A$时, 这两者可以被复合以至于它们沿着$x$进行通信.$$\frac{\mathrm{\Delta }⊢P::x:A{\mathrm{\Delta }}^{\prime },x:A⊢Q::z:C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢(\nu x)(P|Q)::z:C}\mathsf{cut}$$复合的进程表达式将$P$和$Q$并置于一个并行复合(parallel composition)$(P|Q)$之中, 其共享着$x$作为一个私有(private)信道, 这是由名称限制(name restriction)$(\nu x)$所指示的. 注意到这条规则蕴含着某种隐式的重命名, 因为$P$提供$A$所沿着的信道必须与$Q$使用$A$所沿着的信道等同起来. 在$\pi$演算中, $(\nu x)P$是以$P$为作用域的变量$x$的绑定子 (binder).

从纯粹逻辑的角度看待, 这不过就是线性逻辑中的cut规则:$$\frac{\mathrm{\Delta }⊢A{\mathrm{\Delta }}^{\prime },A⊢C}{\mathrm{\Delta },{\mathrm{\Delta }}^{\prime }⊢C}{\mathsf{cut}}_A$$我们使用线性逻辑的一种直觉主义版本实际上是有点不同寻常的, 也就是说, 每个相继式的右侧只有一个 (singleton). 这并非绝对本质性的 (见[Abr93], 其提供了一个相关的古典逻辑对应物), 但是它精简了系统的判断澄清 (judgmental justification). 它也反映了提供和使用服务之间内蕴 (intrinsic) 的不对称性, 尽管我们将会看到它们的关联是相当紧密的. 这也有助于建立依赖类型论.

第4.3节 作为forwarding的identity

第4.4节 将cut复合

多重并行复合应该只在其间交互需要时同步 (synchronize). 从证明论的角度来说, 这意味着相继cut的顺序应该是无足轻重的. 相对应的律 (law) 作为重写规则并无固有的方向 (orientation), 因此我们应该将其想成是结构证明等价. 我们留给读者写出简单的proof figures. 在进程演算方面, 我们得到了相应的structural congruence. [译注: 我不太会翻译congruence, 它总是在各种地方出现, 然后总是指代一种等价关系.]$$\begin{array}{rcl}(\nu x)((\nu y)(P|Q)|R)& \equiv & (\nu y)(P|(\nu x)(Q|R))\\ & & \text{只要}x\notin \mathsf{fn}(P),y\notin \mathsf{fn}(R)\\ (\nu x)(P|(\nu y)(Q|R))& \equiv & (\nu y)(Q|(\nu x)(P|R))\\ & & \text{只要}x\notin \mathsf{fn}(Q),y\notin \mathsf{fn}(P)\end{array}$$这些可由更基本的结构等价推导出来, 也就是并行复合的结合律和作用域挤出 (scope extrusion).$$\begin{array}{rcll}((P|Q)|R)& \equiv & (P|(Q|R))& \text{结合律}\\ (P|Q)& \equiv & (Q|P)& \text{交换律}\\ (P|(\nu x)Q)& \equiv & (\nu x)(P|Q)& \text{作用域挤出}\\ & & & \text{只要}x\notin \mathsf{fn}(P)\end{array}$$

第4.5节 输入

第4.6节 归约

第4.7节 例子: 硬币交换

第5章 Choice and Replication

第6章 量化

第6.1节 全称量化

第7章 cut消除

第8章 Identity and Inversion

第9章 Chaining and Focusing

第10章 自然演绎

第11章 Ordered Logic

第12章 Ordered Forward Chaining

第13章 Backward Chaining

第14章 资源管理

第15章 合一

第16章 Monadic Logic Programming

第17章 并发逻辑框架

第18章 资源语义

第19章 嵌入线性逻辑于直觉主义逻辑

第20章 古典线性逻辑