中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第2章 泛代数和代数数据类型

第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, 1N，也叫做零元函数 – 函数+,  : 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 ?, …

2.2代数、基调和项 2.2.2代数项的语法 基调Σ=〈S,F〉 一S是一个集合，其元素叫做类别 函数符号f:S1×…×S→s的集合F,其中表达式 S1×.×Sk→s叫做f的类型 一零元函数符号叫做常量符号 例：ΣN=(S,F〉 sorts nat fetns 0,1 nat +,*：nt×nat→nat

2.2 代数、基调和项 2.2.2 代数项的语法 • 基调 = S，F – S是一个集合，其元素叫做类别 – 函数符号f : s1 …  sk → s的集合F ，其中表达式 s1 …  sk → s叫做f 的类型 – 零元函数符号叫做常量符号 • 例: N = S，F sorts : nat fctns : 0, 1 : nat +,  : nat  nat → nat

2.2代数、基调和项 项 定义基调的目的是用于写代数项 项中可能有变量，因此需假定一个无穷的符号集 合V,其元素称为变量 - 类别指派T={x1:S1,,xk:Sx} 基调Σ=(S,F和类别指派T上类别s的代数项集合 Terms (,T)定义如下： 1、如果x:s∈T,那么x∈Ters(②，T 2、如果f:S×.×Sk→s并且M∈Ters(②，T)(i =1,,k,那么fM1.Mk∈Term心(2，T) 当k=0时，如果f:s,那么f∈Terms②，下)

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

2.2代数、基调和项 项的例子 -0,0+1∈Terw②N☑) -0+x∈Termsat(②N,),其中T={x:nat,…} 代数项中无约束变元 -[NWx]M就是简单地把M中x的每个出现都用N代替 记号 T,x:s'=TU{x:s 。引理2.1 若M∈Terms∑，T,x:s'且N∈Terms'2,),那么 [N/x]M∈Ters(,T 证明按Ters∑，)中项的结构进行归纳

2.2 代数、基调和项 • 项的例子 – 0, 0 + 1 Termsnat (N , ) – 0 + x  Termsnat (N , )，其中 =  x : nat, … • 代数项中无约束变元 – 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代数、基调和项 例 用基调Σsk=〈S,F)来写自然数和自然数栈表达式 sorts nat,stack fctns 0,1,2,..nat +,*:nat×nat-→nat empty stack push nat x stack -stack pop:stack→>stack top stack -nat push2(pwsh1(push0empy))是该基调的项 -

2.2 代数、基调和项 • 例 用基调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) )是该基调的项

2.2代数、基调和项 2.2.3代数以及项在代数中的解释 ·基调的代数是为代数项提供含义的数学结构 Σ是一个基调，则Σ代数A包含 -对每个s∈S,正好有一个载体As 一个解释映射 把函数I(f):A.×AA指派给函数符号 f:S1X.XSk→S∈F 把If)∈A指派给常量符号f:S∈F ∑N代数N写成 N=〈N,0N,1N,+N,*N)

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, 0 N , 1 N , + N ,  N  sk s1