第2章 泛代数和代数数据类型 函数式程序设计语言PCF由三部分组成 代数数据类型：自然数类型和布尔类型 带函数和积等类型的纯类型化入演算 一不动点算子 第2章到第4章对这三部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代 数数据类型
第2章 泛代数和代数数据类型 • 函数式程序设计语言PCF由三部分组成 – 代数数据类型：自然数类型和布尔类型 – 带函数和积等类型的纯类型化演算 – 不动点算子 • 第2章到第4章对这三部分进行透彻的研究 • 本章研究像自然数类型和布尔类型这样的代 数数据类型
2.1引 言 ·代数数据类型包括 -一个或多个值集 一组在这些集合上的函数 -基本限制是其函数不能有函数变元 基本“类型”(ype)符号被称为“类别”(sort 泛代数（也叫做等式逻辑）》 -定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数据 类型时的作用
2.1 引 言 • 代数数据类型包括 – 一个或多个值集 – 一组在这些集合上的函数 – 基本限制是其函数不能有函数变元 – 基本“类型”(type)符号被称为“类别” (sort) • 泛代数（也叫做等式逻辑） – 定义和研究代数数据类型的一般数学框架 – 本章研究泛代数和它在程序设计中定义常用数据 类型时的作用
2.1引 言 本章主要内容： -代数项和它们在多类别代数中的解释 等式规范（也叫代数规范)和等式证明系统 等式证明系统的可靠性和完备性（公理语义和指 称语义的等价) 代数之间的同态关系和初始代数 -数据类型的代数理论 -从代数规范导出的重写规则 (操作语义) 包括了大多数逻辑系统中的一些公共议题
2.1 引 言 • 本章主要内容： – 代数项和它们在多类别代数中的解释 – 等式规范（也叫代数规范）和等式证明系统 – 等式证明系统的可靠性和完备性（公理语义和指 称语义的等价） – 代数之间的同态关系和初始代数 – 数据类型的代数理论 – 从代数规范导出的重写规则（操作语义） 包括了大多数逻辑系统中的一些公共议题
2.2代数、基调和项 2.2.1代数 。代数 -一个或多个集合，叫做载体 一组特征元素和一阶函数，也叫做代数函数 f:A1××Ak→A 。 例：N=〈N,0,1,+,*) 载体N是自然数集合 -特征元素0,1∈N,也叫做零元函数 函数+，*：N×N→N
2.2 代数、基调和项 2.2.1 代数 • 代数 – 一个或多个集合，叫做载体 – 一组特征元素和一阶函数，也叫做代数函数 f : A1 … Ak → A • 例：N = N, 0, 1, +, – 载体N是自然数集合 – 特征元素0, 1N，也叫做零元函数 – 函数+, : N N → N
2.2代数、基调和项 多个载体的例子 Apcp=(N,B,0,1,,+,true,false,Eq?,…〉 下面逐步给出代数的一种语法描述，有穷的 语法表示在计算机科学中十分重要，可用来 定义数据类型 -证明数据类型的性质 还必须讨论这种语法描述的指称语义 满足一组等式的除了Apc外，可能还有： Aspcr=(Ns,B,0,1,2,3,4,+s,true,false,Eq ?
2.2 代数、基调和项 • 多个载体的例子 – APCF = N, B, 0, 1, …, +, true, false, Eq ?, … • 下面逐步给出代数的一种语法描述，有穷的 语法表示在计算机科学中十分重要，可用来 – 定义数据类型 – 证明数据类型的性质 • 还必须讨论这种语法描述的指称语义 – 满足一组等式的除了APCF外，可能还有： A5 PCF= N5 ,B, 0, 1, 2, 3, 4, +5 , true, false, Eq ?, …