泛代数和代数数据类型.ppt

《泛代数和代数数据类型.ppt》由会员上传分享，免费在线阅读，更多相关内容在行业资料-天天文库。

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,1N，也叫做零元函数函数+,:NNN2.2代数、基调和项多个载体的例子APCFN,B,0,1,…,+,true,false,Eq?,…下面逐步给出代数的一种语法

3、描述，有穷的语法表示在计算机科学中十分重要，可用来定义数据类型证明数据类型的性质还必须讨论这种语法描述的指称语义满足一组等式的除了APCF外，可能还有：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叫做f的类型零元函数符号叫做常量符号例:NS，Fsorts:natfctns:0,1:nat,:natnatnat2.2代数、基调和项项定义基调的

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

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

6、knatpush2(push1(push0empty))是该基调的项2.2代数、基调和项2.2.3代数以及项在代数中的解释基调的代数是为代数项提供含义的数学结构是一个基调，则代数A包含对每个sS，正好有一个载体As一个解释映射I把函数I(f):A…AAs指派给函数符号f:s1…sksF把I(f)As指派给常量符号f:sFN代数N写成NN,0N,1N,N,Nsks12.2代数、基调和项代数A的环境:VsAs环境满足如果对每个x:s都有(x)AsMTermss(,)的含义AM是Ax

7、(x)AMfA(AM1,…,AMk)若f:s是常量符号，则AffA若A清楚时，省略A而直接写成M不依赖于时，用AM表示M在A中的含义2.2代数、基调和项例若(x)0Nx1N(x,1)N((x),1N)N(0N,1N)1N2.2代数、基调和项例AstkN,N,0A,1A,…,A,A,emptyA,pushA,popA,topAemptyA,空序列pushA(n,s)n::spopA(n::s)spopA()topA(n::s)ntopA

8、()0A若把x:nat映射到自然数3，把s:stack映射到2,1pop(pushxs)popA(pus