类型检查-类型表达式:类型系统是一种逻辑系统

描述类型系统的语言

类型系统主要用来说明编程语言的定型规则，它独立于类型检查算法

定义一个类型系统，一种重要的设计目标是存在有效的类型检查算法

类型系统的基本概念可用于各类语言，包括函数式语言、命令式语言和并行语言等

我们后面讨论用形式方法来描述类型系统

类型系统的形式化

类型系统是一种逻辑系统

 有关自然数的逻辑系统

自然数表达式（需要定义它的语法）

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的区别

--------------------- 

作者：lz710117239 

来源：CSDN 

原文：https://blog.csdn.net/lz710117239/article/details/79155470 

版权声明：本文为博主原创文章，转载请附上博文链接！