第3章泛代数和代数数据类型

《第3章泛代数和代数数据类型》由会员上传分享，免费在线阅读，更多相关内容在教育资源-天天文库。

1、第3章泛代数和代数数据类型PCF语言的三部分组成带函数和积类型的纯类型化演算自然数类型和布尔类型不动点算子第3章到第5章对这三部分进行透彻的研究本章研究像自然数类型和布尔类型这样的代数数据类型3.1引言代数数据类型包括一个或多个值集一组在这些集合上的函数基本限制是其函数不能有函数变元基本“类型”符号被称为“类别”泛代数（也叫做等式逻辑）定义和研究代数数据类型的一般数学框架本章研究泛代数和它在程序设计中定义常用数据类型时的作用3.1引言本章主要内容：代数项和它们在多类别代数中的解释等式规范（也叫代数规范）和等式证

2、明系统等式证明系统的可靠性和完备性（公理语义和指称语义的等价）代数之间的同态关系和初始代数数据类型的代数理论从代数规范导出的重写规则（操作语义）大多数逻辑系统中一些公共的议题将被覆盖3.2代数、基调和项3.2.1代数代数一个或多个集合，叫做载体一组特征元素和一阶函数，也叫做代数函数f:A1…AkA例：NN,0,1,+,载体N是自然数集合特征元素0,1N，也叫做零元函数函数+,:NNN3.2代数、基调和项多个载体的例子ApcfN,B,0,1,…,+,true,false,Eq?,…下面开

3、始逐步给出代数的一种语法描述，有穷的语法表示在计算机科学中十分重要定义数据类型证明性质进行化简还必须讨论这种语法描述的语义A5pcfN5,B,0,1,2,3,4,+5,true,false,Eq?,…3.2代数、基调和项3.2.2代数项的语法基调S，FS是一个集合，其元素叫做类别函数符号f:s1…sks的集合F，其中表达式s1…sks叫做类型零元函数符号叫做常量符号例NS，Fsorts:natfctns:0,1:nat,:natnatnat3.2代数、基调和项定义基调的目

4、的是用于写代数项考虑项中有变量的情况，需假定有一个无穷的符号集合V，其元素称为变量类别指派x1:s1,…,xk:sk基调S，F和类别指派上类别s的代数项集合Termss(,)如果x:s，那么xTermss(,)如果f:s1…sks并且MiTermssi(,)(i1,…,k)，那么fM1…MkTermss(,)当k0时，如果f:s，那么fTermss(,)3.2代数、基调和项例0,01Termsnat(N,)0xTermsnat(N,)，其

5、中x:nat,…代数项中无约束变元，NxM就是简单地把M中x的每个出现都用N代替就是了记号,x:sx:s引理如果MTermss(,,x:s)并且NTermss(,)，那么NxMTermss(,)证明按Termss(,)中项的结构进行归纳3.2代数、基调和项例用基调stkS,F来写自然数和栈表达式sorts:nat,stackfctns:0,1,2,…:nat,:natnatnatempty:stackpush:natstacksta

6、ckpop:stackstacktop:stacknatpush2(push1(push0empty))是该基调的项3.2代数、基调和项3.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3.2代数、基调和项代数A的环境:VsAs环境满足如果对每

7、个x:s都有(x)AsMTermss(,)的含义A〖M〗A〖x〗(x)A〖M〗fA(A〖M1〗,…,A〖Mk〗)若f:s是常量符号，则A〖f〗fAA清楚时，省略A而直接写成〖M〗不依赖于时，用A〖M〗表示M在A中的含义3.2代数、基调和项例若(x)0N〖x1〗N(〖x〗,〖1〗)N((x),1N)N(0N,1N)1N3.2代数、基调和项例AstkN,N,0A,1A,…,A,A,emptyA,pushA,popA,topAemptyA

8、,空序列pushA(n,s)n::spopA(n::s)spopA()topA(n::s)ntopA()0A若把x:nat映射到3A，把s:stack映射到2A,1A〖pop(pushxs)〗popA(pushA(〖x〗,〖s〗))popA(pushA(3A,2A,1A))popA(3A,2A,1A)2A,1A3.2代数、基