编译原理（四）类型检查2
描述类型系统的语言
- 类型系统主要用来说明编程语言的定型规则，它独立于类型检查算法
- 定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法
- 类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等
我们后面讨论用形式方法来描述类型系统
类型系统的形式化
类型系统是一种逻辑系统
有关自然数的逻辑系统
自然数表达式（需要定义它的语法）
a+b,3
良形公式（逻辑断言，需要定义它的语法）
a+b=3,(d=3)^(c<10)
推理规则
a<b,b<c --> a<c
类型系统
类型表达式
int,int——>int
定型断言
x:int|- x+3:int
（|-左边部分x：int称为定型环境）
类型检查和类型推断
- 类型检查
用语法制导的方式，根据上下文有关的定型规则来判定程序构造是否为良类型的程序构造的过程
- 类型推断
类型信息不完全的情况下的定型判定问题，例如：f(x:t)=E和f(x)=E的区别
类型检查——声明语句
编译期的类型
整型与布尔型运算的类型转换
类型推导：
上面在最开始对p的类型β一无所知，随着下面返回p的类型，我们推导出p是指针类型。