9.1引 言 类型推断的另一种观点是 定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统 类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 判定过程是回答是或不是，而类型推断算法必须 构造类型化的项9.1 引 言 • 类型推断的另一种观点是 –定型是由一组推理规则给出 合式公式的语法和证明规则给出一个逻辑系统 –类型推断算法正好是一个公理理论的判定过程 决定一个合式公式是否可证明 –判定过程是回答是或不是，而类型推断算法必须 构造类型化的项