1、第 2章 泛代数和代数数据类型 函数式程序设计语言 PCF由三部分组成 代数数据类型：自然数类型和布尔类型 带函数和积等类型的纯类型化 演算 不动点算子 第 2章到第 4章对 这三 部分进行透彻的研究 本章研究像自然数类型和布尔类型这样的代数数据类型2.1 引 言 代数数据类型 包括 一个或多个值集 一组在这些集合上的函数 基本限制是其函数不能有函数变元 基本 “类型 ”(type)符号被称为 “类别 ” (sort) 泛代数（也叫做等式逻辑） 定义和研究代数数据类型的一般数学框架 本章研究泛代数和它在程序设计中定义常用数据类型时的作用 2.1 引 言 本章主要内容： 代数项和它们在多类别代数
2、中的解释 等式规范（也叫代数规范）和等式证明系统 等式证明系统的可靠性和完备性（公理语义和指称语义的等价） 代数之间的同态关系和初始代数 数据类型的代数理论 从代数规范导出的重写规则（操作语义）包括了大多数逻辑系统中的一些公共议题2.2 代数、基调和项2.2.1 代数 代数 一个或多个集合，叫做载体 一组特征元素和一阶函数，也叫做代数函数f : A1 Ak A 例： N N, 0, 1, +, 载体 N是自然数集合 特征元素 0, 1N， 也叫做零元函数 函数 +, : N N N2.2 代数、基调和项 多个载体的例子 APCF N, B, 0, 1, , +, true, false, Eq
3、 ?, 下面开始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要 定义数据类型 证明性质 进行化简 还必须讨论这种语法描述的指称语义 A5PCF N5, B, 0, 1, 2, 3, 4, +5, true, false, Eq ?, 2.2 代数、基调和项2.2.2 代数项的语法 基调 S， F S是一个集合 ， 其元素叫做 类别 函数符号 f : s1 sk s的 集合 F ， 其中 表达式s1 sk s叫做类型 零元函数符号叫做常量符号 例 : N S， Fsorts : natfctns : 0, 1 : nat, : nat nat nat 2.2 代数、基调和项 项
4、 定义基调的目的是用于写代数项 项中可能有变量，因此需假定一个无穷的符号集合 V， 其元素称为变量 类别指派 x1 : s1, , xk : sk 基调 S， F和类别指派 上类别 s的代数项集合Termss (, )定义如下：1、如果 x : s ， 那么 x Termss (, )2、如果 f : s1 sk s并且 Mi Termssi(, ) (i 1, , k)， 那么 f M1 M k Termss (, )当 k 0时，如果 f : s， 那么 f Termss (, )2.2 代数、基调和项 项的例子 0, 0 1 Termsnat (N, ) 0 x Termsnat (N,
5、 )， 其中 x : nat, 代数项中无约束变元NxM就是简单地把 M中 x的每个出现都用 N代替 记号 , x : s x : s 引理 若 MTermss(, , x : s)且 NTermss(, )， 那么 NxMTermss (, )证明 按 Termss(, )中项的结构进行归纳2.2 代数、基调和项 例 用基调 stk S, F来写自然数和栈表达式sorts : nat, stackfctns : 0, 1, 2, : nat, : nat nat natempty : stackpush : nat stack stackpop : stack stacktop : stack natpush 2 (push 1 (push 0 empty) )是该基调的项2.2 代数、基调和项2.2.3 代数以及项在代数中的解释 代数是为代数项提供含义的数学结构 是一个基调，则 代数 A包含 对每个 s S， 正好有一个载体 As 一个解释映射 I 把函数 I (f ) : As1 Ask As指派给函数符号f : s1 sk s F把 I (f ) As指派给常量符号 f : s F N代数 N 写成N N, 0N, 1N, N, N
