52描述类型系统的语言 类型系统的形式化 类型系统是一种逻辑系统 有关自然数的逻辑系统类型系统 自然数表达式 类型表达式 a+b,3 int,int→int 良形公式 定型断言 a+b=3, (d=3A(c<10) X: int -X+3: int 推理规则 定型规则 a <b. b<c TIM: int, TN: int a < c TIM+N: int
5.2 描述类型系统的语言 类型系统的形式化 • 类型系统是一种逻辑系统 有关自然数的逻辑系统 类型系统 - 自然数表达式 类型表达式 a+b, 3 int, int → int - 良形公式 定型断言 a+b=3, (d=3)(c<10) x:int |– x+3 : int - 推理规则 定型规则 |– M : int, |– N : int |– M + N : int a < b, b < c a < c
52描述类型系统的语言 类型系统的形式化 类型表达式 具体语法:出现在编程语言中 抽象语法:出现在定型断言和类型检查的实现中 下一节开始举例 定型断言 本节讨论它的一般形式 定型规则 本节讨论它的一般形式
5.2 描述类型系统的语言 类型系统的形式化 • 类型表达式 – 具体语法：出现在编程语言中 – 抽象语法：出现在定型断言和类型检查的实现中 – 下一节开始举例 • 定型断言 – 本节讨论它的一般形式 • 定型规则 – 本节讨论它的一般形式
52描述类型系统的语言 521断言 断言的形式 rS5的所有自由变量都声明在中 其中 是一个静态定型环境,如x;:T1,…,x:Tn s的形式随断言形式的不同而不同 断言有三种具体形式
5.2 描述类型系统的语言 5.2.1 断言 断言的形式 |– S S的所有自由变量都声明在中 其中 • 是一个静态定型环境，如x1 :T1 , …, xn :Tn • S的形式随断言形式的不同而不同 • 断言有三种具体形式
52描述类型系统的语言 环境断言 F|◇ 该断言表示T是良形的环境 将用推理规则来定义环境的语法(而不是用文法) °语法断言 F卜nat 在环境I下,nat是类型表达式 将用推理规则来定义类型表达式的语法 定型断言 TIM: T 在环境r下,M具有类型T B]: 0Itrue: boolean x: nat1-x+1: nat 将用推理规则来确定程序构造实例的类型
5.2 描述类型系统的语言 • 环境断言 |– 该断言表示是良形的环境 – 将用推理规则来定义环境的语法(而不是用文法) • 语法断言 |– nat 在环境下，nat是类型表达式 – 将用推理规则来定义类型表达式的语法 • 定型断言 |– M : T 在环境下， M具有类型T 例： |– true : boolean x : nat |– x+1 : nat – 将用推理规则来确定程序构造实例的类型
52描述类型系统的语言 有效断言 Ttrue: boolean 无效断言 TItrue: nat
5.2 描述类型系统的语言 • 有效断言 |– true : boolean • 无效断言 |– true : nat