第6章 递归类型 递归定义的类型的例子 自然数表的类型 类型等式t兰wnit+(nat×t)的一个解 二叉树的类型 类型等式t兰wnit+(t×t)的一个解 使用“兰”表示解是要使两边同构，而不是相等 归纳类型对应到上述类型同构等式的初始解 例：自然数类型 余归纳类型对应到它们的终结解 例：自然数流类型
第6章 递归类型 • 递归定义的类型的例子 – 自然数表的类型 类型等式 t unit + (nat t)的一个解 – 二叉树的类型 类型等式 t unit + (t t)的一个解 使用“ ”表示解是要使两边同构，而不是相等 归纳类型对应到上述类型同构等式的初始解 例：自然数类型 余归纳类型对应到它们的终结解 例：自然数流类型
6.1引 言 本章的主要内容 直观地介绍余归纳的定义、余归纳的证明原 理和余代数 形式地介绍递归类型 形式地介绍归纳类型和余归纳类型 解释 -代数方法是从“构造的”角度研究抽象数据类型 余代数方法是从“观察的”的角度描述像对象、 自动机、进程、软件构件等基于状态的系统
6.1 引 言 本章的主要内容 • 直观地介绍余归纳的定义、余归纳的证明原 理和余代数 • 形式地介绍递归类型 • 形式地介绍归纳类型和余归纳类型 • 解释 – 代数方法是从“构造的”角度研究抽象数据类型 – 余代数方法是从“观察的”的角度描述像对象、 自动机、进程、软件构件等基于状态的系统
6.2 归纳和余归纳 6.2.1余归纳现象 例 数据集A上的有限表集可归纳地定义如下 (①)基础情况：nil是有限表 (2)迭代规则：若a∈A且o是有限表，则cons(a,o)是 有限表 ③)最小化条件：此外，有限表集中不含其它元素 最小化规则指所定义的集合是满足(1)和2)两条 约束的最小集合，无任何垃圾在其中
6.2 归纳和余归纳 6.2.1 余归纳现象 • 例 数据集A上的有限表集可归纳地定义如下 (1) 基础情况：nil是有限表 (2) 迭代规则：若aA且是有限表，则cons(a, )是 有限表 (3) 最小化条件：此外，有限表集中不含其它元素 最小化规则指所定义的集合是满足(1)和(2)两条 约束的最小集合，无任何垃圾在其中
6.2 归纳和余归纳 例 数据集A上的无限表集（流）可余归纳地定义如下 (1)迭代规则：若a∈A且o是无限表，则cos(a,o)是 无限表 (2)最大化条件：数据集4上的无限表集是满足迭代 规则的最大集合 最大化条件表示所有未被(1)排除的元素都被包 含在所定义的集合中，即该集合中任何无限表都可 以通过应用规则(1)若干次（可能是无限次）而得到
6.2 归纳和余归纳 • 例 数据集A上的无限表集（流）可余归纳地定义如下 (1) 迭代规则：若aA且是无限表，则cons(a, )是 无限表 (2) 最大化条件：数据集A上的无限表集是满足迭代 规则的最大集合 最大化条件表示所有未被(1)排除的元素都被包 含在所定义的集合中，即该集合中任何无限表都可 以通过应用规则(1)若干次（可能是无限次）而得到
6.2 归纳和余归纳 。比较 -两种表都有观察算子head和运算算子tai讥 head(cons(a,o))=a tail(cons(a,o))=o -计算有限表表长的函数length length(nil)0 length(cons(a,o))=1 length(o) 若有函数f:A→A,定义其应用到无限表所有元 素的拓展函数ext(f) head(ext(f)())=f(head(o)) tail(ext(f)(o))=ext(f)(tail(o))
6.2 归纳和余归纳 • 比较 – 两种表都有观察算子head和运算算子tail head(cons(a, )) = a tail(cons(a, )) = – 计算有限表表长的函数length length(nil) = 0 length(cons(a, )) = 1 + length() – 若有函数f : A → A，定义其应用到无限表所有元 素的拓展函数ext(f ) head(ext(f )()) = f (head()) tail(ext(f )()) = ext(f )(tail())