类型化规则

在类型理论中，类型化规则是一种推理规则，它描述了类型系统如何将类型分配给一个句法结构。这些规则可以被类型系统应用来确定一个程序是否具有良好的类型，以及表达式具有什么类型。使用类型规则的一个典型例子是在简单类型的λ微积分中定义类型推理，它是笛卡尔封闭类别的内部语言。符号类型化规则指定了类型化关系的结构，该关系将句法术语与它们的类型联系起来。在语法上，类型化关系通常用冒号表示，因此例如.规则本身通常使用自然演绎的符号来指定。例如，下面的类型化规则指定了一个简单的布尔语言的类型化关系。每条规则都指出，线下的结论可以从线上的前提推导出来。前两条规则的线上没有前提，所以它们是公理。第三条规则在线上有前提（具体来说是三个前提），所以它是一个推理规则。

在编程语言中，一个变量的类型取决于它被绑定的位置，这就需要有上下文敏感的类型化规则。这些规则是由类型化判断给出的，通常写作这说明一个表达式{displaystyle{Gamma}下的类型。将变量与它们的类型联系起来。这个符号可以用来给出简单类型的λ微积分中变量引用和λ抽象的类型规则：。101-102同样地，下面的打字规则描述了并非所有的类型化规则系统都直接指定了类型检查算法。将一个声明性的规则系统改编成一个可解码的算法需要产生一个单独的、可以被证明为指定相同类型关系的算法系统。