消去规则
在类型论中, 消去规则是指一类推导规则, 这些规则描述如何使用某个类型的实例的规则, 类似于模式匹配.
每个形成规则都会配备一组消去规则. 一般来说, 消去规则至少有一个, 即使不存在对应的构造规则, 例如空类型. 但也有的类型不需要消去规则, 例如单位类型就因为有足够强的唯一性规则而不再需要消去规则.
与之对应的是构造规则.
目录
1记号
若一个类型可以被视为某种归纳类型的特例, 那么它往往只会有一个消去规则, 写作 , 其中 是类型的名字, 读作 “ 的消去子”. 此时模式匹配表达的是一种对数据 “解构” 的思想.
一个较为特殊的例子是积类型, 它可以 (但不是必须) 被定义为有两个消去规则的类型, 这是因为该类型同时也可以被视为一种余归纳类型.
术语翻译
消去规则 • 英文 elimination rule • 法文 règle d’élimination • 拉丁文 regula eliminationis
消去子 • 英文 eliminator