交换规则

在逻辑学中, 交换规则是使得语境中命题无序的规则, 如下所示:$$\frac{\Gamma ,A,B⊢C}{\Gamma ,B,A⊢C}$$交换规则是结构性规则的一种. 在亚结构逻辑中, 常见的不假设交换规则的逻辑只有顺序逻辑, 它同时也是线性逻辑.

1在类型论中

在简单类型 $\lambda$ 演算中, 任意的交换规则都可以使用某种替换操作实现, 但依值类型论中, 则不可随意交换, 因为语境中有前后依赖关系.

术语翻译

交换规则 • 英文 exchange rule