第6章递归类型

第6章递归类型内容摘要：

则 F1(g  f ) = F1(g)  F1(f ) 0 ()FAid 下面都用 F，根据参数 可知道它是 F0还是 F1 归纳和余归纳 • 基于函子来定义单类代数 – 令 F是函子， F的一个代数（简称 F代数）是一个序对 U, a，其中 U是集合，称为该代数的载体， a是函数 a : F(U) U，称为该代数的代数结构（也称为运算） • 例：自然数 自然数上的零和后继函数 0 : 1 N 和 S : N  N 形成 函子 F(X) =1+X 的 F代数 N, [0, S] : 1+N N N [0, S] 1+ N 1 N Inleft S 0 Inright 归纳和余归纳 • 例：二叉树 以集合 A的元素标记节点的二叉树的集合用 tree(A)表示 – 空树 nil可用函数 nil : 1 tree(A)表示 – node : tree(A)  A  tree(A)  tree(A)表示从两棵子树和一个节点标记构造一棵树 – nil和 node形成函子 F(X) =1+ (X  A  X)的一个代数 [nil, node] : 1 + (tree(A)  A  tree(A))  tree(A) 归纳和余归纳 • 用函子和交换图表来表示代数同态 令 – F是函子 – a : F(U) U和 b : F(V) V是两个函数 则 –F代数 U, a到 V, b的 同态是函数 f : U  V， 满足 f  a = b  F(f ) • 可进一步定义初始代数 F(f ) F(U) U V b a f F(V) 归纳和余归纳 • 定义余代数 令 F是函子， F的一个余代数（简称 F余代数）是一个序对 U, c，其中 – U是集合，称为该余代数的载体 – c是函数 c : U  F(U)， 称为该余代数的余代数 结构（也称为运算） 由于余代数经常描述 动态系统，载体也叫做 状态空间 Z f, g X  Y X Y Proj1 g f Proj2 归纳和余归纳 • 余代数和代数的区别 本质上这是构造和观察之间的区别 – 代数由载体集合 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  f = F(f )  b • 可进一步定义终结代数 F(f ) F(U) U V b a f F(V) 归纳和余归纳 • 例： 考虑有两个按键 value和 next的机器 – 可以用状态空间 U上的余代数 value, next : U  A  U 来描述，其中 – value, next由两个函数 value : U  A和 next : U  U组成 – 连续地交替按 next键和 value键，可以产生无限序列 (a1, a2, …) – 它可以看成 N  A上的一个函数，其中 ai = value(next(i)(u)) A 递 归 类 型 递归类型总揽 • 在 PCF的类型中加入递归类型  ::= b | t | unit |  + |   |    |  t. 其中 t是类型变量 –  t.的解释 在递归的类型定义 t = 中， 引入 fix(t.) 来表示等式 t = 的一个解， 用  t.作为 fix(t.)的语法美化 – 类型表达式中出现变量会导致多态性，目前限于闭表达式 递 归 类 型 • 类型相等问题 对类型等式 t = 有两种可能的解释 – 等式左右两边是真正不可区分的类型 这时类型相等变。