极性

极性分别在逻辑学和类型论中是逻辑连接词和形成规则的一种类似的性质, 可以是正的或者是负的. 这种分类并不绝对, 存在一些事物的极性既不是正的也不是负的, 例如 $!$ 模态, 也存在一些事物同时是正的和负的, 例如结构逻辑中的积类型.

1在逻辑学中

在相继式演算中, 逻辑连接词有左规则和右规则之分: 对于规则导出的相继式 $Ψ ⊢ A$ , 若某规则对 $Ψ$ 中的连接词进行消除, 那么称之为左规则, 反之则称之为右规则.

定义 1.1. 某规则可逆大致是说它可以反过来写.

具体的说, 若说如下规则可逆: $\frac{Ψ ⊢ A}{Ψ _{1} ⊢ A _{1}}$ 就相当于是在说 $\frac{Ψ _{1} ⊢ A _{1}}{Ψ ⊢ A}$ 是可导出规则或者可容许规则.

一般来说, 不可逆的那些规则在证明中包含非平凡的信息.

若某连接词的左规则可逆 (又叫左可逆), 那么认为该连接词的极性为正, 否则为负.

该思想也可以类比到自然演绎中, 不过自然演绎和类型论高度相似, 因此直接使用类型论的直觉即可.

在类型论中, 对于每个形成规则, 有对应的构造规则和消去规则, 分别表述如何构造该形成规则的实例、如何使用该形成规则的实例.

若我们以构造规则为主、令消去规则去配合构造规则, 那么认为该类型的极性为正, 否则为负. 注意这只是一种视角上的区别, 有的类型可以分别以两者为主, 得到等价的定义, 因此它既是正的也是负的, 例如积类型.

另一种视角下, 正的形成规则往往对应某个 “值”, 因为我们更关心它的构造, 负的那些则对应某种 “计算” 的过程, 因为我们更关心它对于消去的动作如何回应.

•	模式匹配是正类型配备的消去规则.

•	伴随求值的框架使用极性对类型进行分类.

•	聚焦的思想建立在极性之上.

术语翻译

极性 • 英文 polarity

可逆 • 英文 invertible