形成规则

在类型论中, 形成规则是指一类推导规则, 这些规则描述如何构造出类型, 思想上类似于宇宙的构造规则.

在简单类型的情况下, 形成规则不需要语境.

每个形成规则都会配备一组构造规则、消去规则、计算规则、唯一性规则. 后两者指定前两者的交互方式:

•	计算规则指定对构造规则进行消去会发生什么.
•	唯一性规则指定将消去规则拿去构造会发生什么.

在复杂的类型论中, 每个形成规则还会配备其它的规则, 例如立方类型论.

1例子

•	简单类型论: 函数、积、无交并、自然数

•	依值类型论: 相等类型、 $Π$ 类型、 $Σ$ 类型

•	同伦类型论: 圆周、区间、纬悬、截断, 又见立方类型论.

在范畴语义中, 形成规则往往对应某些万有构造. 例如积类型对应积 (范畴论), 而 $Σ$ 类型的语义依值和对应态射的复合.

术语翻译

形成规则 • 英文 formation rule • 法文 règle de formation • 拉丁文 regula formationis