文档介绍：第4章简单类型化演算
PCF语言的三部分组成
带函数和积类型的纯类型化演算
自然数类型和布尔类型
不动点算子
第3章对代数数据类型进行了透彻的研究
本章研究简单类型化演算
第5章研究不动点算子
引言
本章的系统是本书研究的所有其它演算的核心
抽象可用来定义新的函数,而代数数据类型只涉及到所声明的一阶函数的应用
在类型化演算的指称语义中需要考虑函数类型的解释
引言
本章的主要内容
提出使用定型公理和推理规则的上下文有关文法
讨论类型化演算的等式证明系统(公理语义)和归约系统(操作语义)
讨论类型化演算的Henkin模型(指称语义)及可靠性和完备性定理
类型
类型的语法
简单类型化演算的类型表达式文法
::= b | null | unit | | |
b:类型常量
null:初始类型
unit:终结类型
和、积与函数类型
不含类型变量
,,
类型
类型的解释
有两种框架来描述类型化演算的指称语义
Henkin模型
笛卡儿封闭的范畴(本课程不讨论)
在Henkin模型中,每个类型表达式解释为一个集合。函数类型的解释:
不能解释为从的解释域到的解释域的所有集合论函数,因为集合论的函数并非都有不动点
解释为具有某种所希望的一般性质(可计算性或者连续性)的函数的集合
类型
在Henkin模型中存在多种观点的可能性
经典集合论的函数(本章)
在完全偏序(论域)上的连续函数(下一章)
用哥德尔数编码的递归函数
初始类型null
正好有一个函数从null的解释域到的解释域
终结类型unit
正好有一个函数从的解释域到unit的解释域
类型,笛卡儿积类型
项
上下文有关语法
不存在上下文无关文法,它正好产生良类型的项
用一种基于逻辑的形式系统来定义类型语言
用公理和推理规则来同时定义表达式及其类型
定型公理c :
推理规则
定型断言 M : , 其中{x1 :1 , …, xk:k }
M1:1, …, Mk:k
N :
1 M1:1, …, k Mk:k
N :
项
项的语法
一个基调B, C包含
一个集合B,其元素叫做基本类型或类型常量
形式为c 的项常量集合C,其中是B上的类型表达式
多类代数的基调S, F的基调很容易变换成基调B, C
令B就等于S
若F有f : s1 … sk s,则在C中包含项常量
f : s1 … sk s
项
项的语法采用如下方式描述
首先用BNF定义类型表达式的语法()
然后用定型公理和定型规则同时定义上的项和它们的类型
定型公理
c (cst)
x x (var)
项
定型规则
(add var)
( Intro)
( Elim)
定型断言的证明叫做定型推导
M :
, x : M :
M : , N:
MN :
, x : M :
( x : .M) :