语境

语境是一个非常宽泛的概念, 一般指 “讨论某个问题的语境”, 比如相继式中的语境就是研究某个命题的 “先决条件” 的意思, 或者说 “假设”.

在类型论中, 一个语境就是一组带类型的变量名, 比如 $x:A,y:B$ 就是两个带类型的变量名, 这就是一个语境. 有时也会忽略变量名, 直接用一组类型来表示语境.

讨论语境的目的一般是为了研究语境的修改, 比如某个事实在语境 $\Gamma$ 下成立, 那它或许也会在另一个语境 $\Delta$ 里成立, 这就说明 $\Gamma$ 和 $\Delta$ 之间就会存在某种关联, 这种关联可以描述成态射, 在类型论中又叫替换操作. 一般来说在某理论的空语境下成立的事实就会被认为是该理论中的真理.

最好在具体的理论中讨论语境的概念.

1在逻辑学中

参见: 推导规则

在逻辑学中, 语境 (有时也作上下文) 是一个相继式中 $⊢$ 符号左边的部分, 它包含了我们目前的假设, 一般定义为命题的集合.

在亚结构逻辑中, 结构性规则的缺失会导致语境的构造稍有不同, 参见该文.

2在类型论中

在类型论中, 语境大致表示之前做的构造.

例 2.1. 在类型论的相继式 $x:A\to B,y:A⊢xy:B$ 中 (相关符号定义见简单类型 $\lambda$ 演算), 语境指蓝色这一部分.

这句话大致是说: 给定函数 $x:A\to B$ 和变量 $y:A$, 能构造出表达式 $xy$, 类型为 $B$.

在类型论的范畴语义中, 语境作为对象、替换操作作为态射构成的范畴是类型论的句法范畴.

3在纤维化中

在拓扑学或者范畴论中, 可以将纤维化 $p:E\to B$ 中的空间 $B$ 看作语境, 然后对于 $b\in B$, 纤维 $X_b$ 看作该语境下为真的命题构成的空间.

这时态射应该看作证明.

术语翻译

语境 • 英文 context • 法文 contexte (m)