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

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