可以进一步定义初始代数。F代数(U,a)是初始的，如果对任意的F代数(W,b),都存在 从(U,a)到(W,b)的唯一同态f。 现在基于函子来定义余代数。令F是函子，F的一个余代数（简称F余代数）是一个 序对U,c),其中U是集合，称为该余代数的载体，c是函数c:U→F(U),称为该余代数的 余代数结构（也称为运算）。由于余代数经常描述动态系统，载体也叫做状态空间。 F(U)→U的代数和U→F(U)的余代数有什么区别？本质上这是构造和观察之间的区 别。一个代数由载体集合U和射入U的一个函数a:FU)→U组成，它告知怎样构造U的 元素。而一个余代数由载体集合U和一个逆向的函数c:U→F(U)组成。此时不知道怎样形 成U的元素，仅有作用在U上的操作，它给出关于U的某些信息。 基于函子和交换图表也可以给出余代数同态的一种 F() FU)← F 表示。令F是函子，a:U→F(U)和b:V→F(O是两个 函数.F余代数(W,b)到(U,a)的同态是一个函数f:V→U, a 满足aof=F0ob,其交换图表在图6.3。 也可以进一步定义终结代数。F代数(U,a)是终结的， 如果对任意的F代数(V,b),都存在从(V,b)到(U,)的唯 图6.3余代数同态的交换图表 一同态f。 例6.7考虑有两个按键value和next的机器。按value键时，它不影响机器内部状态， 并且产生数据集A的某个元素，该元素代表机器内部状态的某个可见属性。因此，连续按 value键两次则产生同样的结果。按next键，则机器转移到另一个状态，该状态的性质也可 以通过按valu键来观察。抽象地说，该机器可以用状态空间U上的余代数 (value,nex:U→A×UU 来描述，该余代数的函数(value,nex)由两个函数value:UA和next:U→U组成。在状 态u∈U下，连续地交替按next键和value键，可以产生无限序列(a,a2,),它可以看成 N→A上的一个函数，其中a,=value(nexf()∈A。该序列就是状态u引发的可观察结果。 若1,2∈U给出同样的可观察序列，则称山和2从可观察角度是不可区分的。 口 6.3递归类型 6.3.1递归类型总揽 在类型表达式的语法中增加类型变量，s,1,,再增加一种形式为.o的类型表达式， 由此可以把递归定义的类型加到PC℉，或加到其它基于演算的语言中。在类型定义1=σ中， 若1出现在σ中，则该类型等式相当于1的一个递归定义式。可以像为递归定义的项引入不 动点算子那样，也为递归定义的类型引入不动点算子，fx(1.o用来表示等式1=σ的一个解。 递归类型是指类型等式系统的解，就像递归函数是项等式系统的解一样。第7章介绍多态类 型时，类型表达式的抽象用记号Ⅱ而不是入，以避免同项的抽象发生混淆，本章由于两种抽 象表达式不会同时出现一个式子中，因而暂时用同一个记号。第7章还会讨论1.σ中1所属 集合，目前暂时忽略它。习惯上用l.σ作为x(1.σ)的语法美化，并且把看成基本符号。在 .o中4约束1：类型表达式和项一样，也是既可以有约束变量又可以有自由变量。若在PC℉ 中把单位类型、和类型及递归类型加入，PC℉的类型表达式则是由文法 g:=b|1|1niσ+go×og→gl.g 产生的闭表达式，其中b代表基本类型，【代表类型变量。一个项，若其类型表达式含自由 变量，则会导致多态性，多态性要等到第7章讨论，因此这里将类型表达式限制到闭表达式。 在此看到，合法的类型表达式己经难以用纯文法来表示了，这个问题也等到第7章解决。仅 17 可以进一步定义初始代数。F 代数〈U, a〉是初始的，如果对任意的 F 代数〈V, b〉，都存在 从〈U, a〉到〈V, b〉的唯一同态 f。 现在基于函子来定义余代数。令 F 是函子，F 的一个余代数（简称 F 余代数）是一个 序对〈U, c〉，其中 U 是集合，称为该余代数的载体，c 是函数 c : U → F(U)，称为该余代数的 余代数结构（也称为运算）。由于余代数经常描述动态系统，载体也叫做状态空间。 F(U) → U 的代数和 U → F(U)的余代数有什么区别？本质上这是构造和观察之间的区 别。一个代数由载体集合 U 和射入 U 的一个函数 a : F(U) →U 组成，它告知怎样构造 U 的 元素。而一个余代数由载体集合 U 和一个逆向的函数 c : U → F(U)组成。此时不知道怎样形 成 U 的元素，仅有作用在 U 上的操作，它给出关于 U 的某些信息。 基于函子和交换图表也可以给出余代数同态的一种 表示。令 F 是函子，a : U → F(U)和 b : V → F(V)是两个 函数。F 余代数〈V, b〉到〈U, a〉的同态是一个函数 f : V → U， 满足 a D f = F(f) D b，其交换图表在图 6.3。 也可以进一步定义终结代数。F 代数〈U, a〉是终结的， 如果对任意的 F 代数〈V, b〉，都存在从〈V, b〉到〈U, a〉的唯 一同态 f。 例 6.7 考虑有两个按键 value 和 next 的机器。按 value 键时，它不影响机器内部状态， 并且产生数据集 A 的某个元素，该元素代表机器内部状态的某个可见属性。因此，连续按 value 键两次则产生同样的结果。按 next 键，则机器转移到另一个状态，该状态的性质也可 以通过按 value 键来观察。抽象地说，该机器可以用状态空间 U 上的余代数 〈value, next〉 : U → A × U 来描述，该余代数的函数〈value, next〉由两个函数 value : U → A 和 next : U → U 组成。在状 态 u ∈U 下，连续地交替按 next 键和 value 键，可以产生无限序列(a1, a2, …)，它可以看成 N → A 上的一个函数，其中 ai = value(next(i) (u)) ∈A。该序列就是状态 u 引发的可观察结果。 若 u1, u2∈U 给出同样的可观察序列，则称 u1和 u2 从可观察角度是不可区分的。 ￾ 6.3 递归类型 6.3.1 递归类型总揽 在类型表达式的语法中增加类型变量 r, s, t, …，再增加一种形式为μt.σ的类型表达式， 由此可以把递归定义的类型加到 PCF，或加到其它基于λ演算的语言中。在类型定义 t = σ中， 若 t 出现在σ中，则该类型等式相当于 t 的一个递归定义式。可以像为递归定义的项引入不 动点算子那样，也为递归定义的类型引入不动点算子，fix(λt.σ) 用来表示等式 t = σ的一个解。 递归类型是指类型等式系统的解，就像递归函数是项等式系统的解一样。第 7 章介绍多态类 型时，类型表达式的抽象用记号Π而不是λ，以避免同项的抽象发生混淆，本章由于两种抽 象表达式不会同时出现一个式子中，因而暂时用同一个记号。第 7 章还会讨论λt.σ中 t 所属 集合，目前暂时忽略它。习惯上用μt.σ作为 fix(λt.σ)的语法美化，并且把μ看成基本符号。在 μt.σ中μ 约束 t；类型表达式和项一样，也是既可以有约束变量又可以有自由变量。若在 PCF 中把单位类型、和类型及递归类型加入，PCF 的类型表达式则是由文法 σ ::= b | t | unit | σ +σ | σ ×σ | σ → σ | μt.σ 产生的闭表达式，其中 b 代表基本类型，t 代表类型变量。一个项，若其类型表达式含自由 变量，则会导致多态性，多态性要等到第 7 章讨论，因此这里将类型表达式限制到闭表达式。 在此看到，合法的类型表达式已经难以用纯文法来表示了，这个问题也等到第 7 章解决。仅 图 6.3 余代数同态的交换图表 F(f ) F(U) U V a b f F(V)