仿射逻辑

在逻辑学中, 仿射逻辑是亚结构逻辑的一种, 可以看作加入了弱化规则的线性逻辑.

比起线性逻辑, 仿射逻辑没有新增的逻辑连接词, 规则也几乎一致, 只是多了弱化规则.

除了增加弱化规则外, 还可以通过加入如下两公理来从线性逻辑得到仿射逻辑:$$\Delta ⊢1\Delta ,A⊢A$$

1和线性逻辑的关系

任何线性逻辑的证明都可以原封不动搬运到仿射逻辑中来.

我们可以把弱化规则看作一种 “垃圾桶”: 每当在线性逻辑中我们希望不使用某个命题, 那么我们把它 “扔进垃圾桶”. 如果存在这种操作, 那么这个线性逻辑就等价于某种仿射逻辑.

事实上, 极性为正的逻辑连接词上的弱化规则都是可容许规则.

仿射逻辑可以翻译到某种对所有命题都有弱化规则的线性逻辑中. 这可以类比编程语言: 若我们使用线性逻辑来对内存资源建模, 那么无论何时都需要处理一切不再使用的资源, 在处理的数据类型定义很复杂时, 这会很麻烦. 仿射逻辑就对应了可以忽略这些资源的逻辑.

术语翻译

仿射逻辑 • 英文 affine logic • 日文 アフィン論理