3.1引 言 本章的主要内容 提出使用定型公理和推理规则的上下文有关 语法 讨论类型化入演算的等式证明系统（公理语义） 和归约系统（操作语义） 讨论类型化)演算的通用模型（指称语义）及 可靠性和完备性定理 介绍PCF语言（递归函数留待下一章）及其 公理语义和操作语义3.1 引 言 本章的主要内容 • 提出使用定型公理和推理规则的上下文有关 语法 • 讨论类型化演算的等式证明系统(公理语义) 和归约系统（操作语义） • 讨论类型化演算的通用模型（指称语义）及 可靠性和完备性定理 • 介绍PCF语言（递归函数留待下一章）及其 公理语义和操作语义