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