中国科学技术大学：《程序设计语言理论》课程教学资源（PPT课件讲稿）第6章 递归类型

第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) 迭代规则：若aA且是有限表，则cons(a, )是 有限表 (3) 最小化条件：此外，有限表集中不含其它元素 最小化规则指所定义的集合是满足(1)和(2)两条 约束的最小集合，无任何垃圾在其中

6.2 归纳和余归纳 例 数据集A上的无限表集（流）可余归纳地定义如下 (1)迭代规则：若a∈A且o是无限表，则cos(a,o)是 无限表 (2)最大化条件：数据集4上的无限表集是满足迭代 规则的最大集合 最大化条件表示所有未被(1)排除的元素都被包 含在所定义的集合中，即该集合中任何无限表都可 以通过应用规则(1)若干次（可能是无限次）而得到

6.2 归纳和余归纳 • 例 数据集A上的无限表集（流）可余归纳地定义如下 (1) 迭代规则：若aA且是无限表，则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())

6.2 归纳和余归纳 例 无限表上的od运算（忽略所有偶数位置的元素） head(odd(o))head(o) tail(odd(o))=odd(tail(tail(o)) -用等式演算可得 head(tailodd())=head(odd(tail(tail() =head(tail(tail(o)） -不难证明，对所有的自然数n head(tail (odd())=head(tail)()

6.2 归纳和余归纳 • 例 无限表上的odd运算（忽略所有偶数位置的元素） head(odd()) = head() tail(odd()) = odd(tail(tail())) – 用等式演算可得 head(tail(odd())) = head(odd(tail(tail()))) = head(tail(tail())) – 不难证明，对所有的自然数n head(tail(n) (odd())) = head(tail(2n) ())

6.2 归纳和余归纳 余归纳定义的数据和函数的性质证明 1、可以用归纳法来证明，例如证明 head(tail)(odd())=head(tail () 2、互模拟 余归纳证明专用方法 -从数学上刻画系统（如对象、进程等）行为等价 这个直观概念 一指两个系统从观测者角度看，可以互相模拟对方 的行为

6.2 归纳和余归纳 • 余归纳定义的数据和函数的性质证明 1、可以用归纳法来证明，例如证明 head(tail(n) (odd())) = head(tail(2n) ()) 2、互模拟——余归纳证明专用方法 – 从数学上刻画系统（如对象、进程等）行为等价 这个直观概念 – 指两个系统从观测者角度看，可以互相模拟对方 的行为

6.2 归纳和余归纳 ·例：无限表 1、定义odd head(odd(o))head(o) tail(odd(o))=odd(tail(tail(o)) 2、定义even even odd tail 3、定义nerge head(merge(o,t))head(o) tail(merge(o,t)=merge(t,(tail())

6.2 归纳和余归纳 • 例：无限表 1、定义odd head(odd()) = head() tail(odd()) = odd(tail(tail())) 2、定义even even = odd tail 3、定义merge head(merge(, )) = head() tail(merge(, )) = merge(, (tail())

6.2 归纳和余归纳 4、基于互模拟证明nerge(odd(o),even(o)=o -互模拟是满足下面条件的关系R: 若(o,∈R,则head(o=hed()并且 〈tail(o,tai(》∈R 基于互模拟的余归纳证明原理是： 对互模拟关系R,若(o,)∈R,则o=T 定义关系 R={(merge(odd(o),een(o),)lo是一个无限表 -只要证明R是互模拟关系即可

6.2 归纳和余归纳 4、基于互模拟证明merge(odd(), even()) =  – 互模拟是满足下面条件的关系R： 若,  R，则 head() = head() 并且 tail(), tail() R – 基于互模拟的余归纳证明原理是： 对互模拟关系R，若,  R，则 =  – 定义关系 R ={merge(odd(), even()),  |是一个无限表} – 只要证明R是互模拟关系即可

6.2 归纳和余归纳 对于第一个条件 head(merge(odd(o),even()))=head(odd(o)) head(o) 对于第二个条件 需证(tail(merge(odd(o),even(o),tail(o》也在R 中，从下面等式证明可得 tail(merge(odd(o),even())) merge(even(o),tail(odd(o)) merge(odd(tail(o)),odd(tail(tail(o)) = merge(odd(tail(o)),even(tail(o))) 〈erge(odd(tail讽o),even(taio),tail讽o》在R中

6.2 归纳和余归纳 – 对于第一个条件 head(merge(odd(), even())) = head(odd()) = head() – 对于第二个条件 需证tail(merge(odd(), even())), tail()也在R 中，从下面等式证明可得 tail(merge(odd(), even())) = merge(even(), tail(odd()) = merge(odd(tail()), odd(tail(tail()))) = merge(odd(tail()), even(tail())) merge(odd(tail()), even(tail())), tail()在R中