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中