6.2 归纳和余归纳 5、利用归纳和等式演算，也可以证明 merge(odd(o),even(o))o -需用归纳法先证明下面几个等式： head(tail(odd(o))=head(taile()) head(taile(merge(o,)))head(tail(o)) head(tailn +1(merge(o,))head(tail() -然后利用等式演算证明 head(tail(merge(odd(o),even())))= head(tail()
6.2 归纳和余归纳 5、利用归纳和等式演算，也可以证明 merge(odd(), even()) = – 需用归纳法先证明下面几个等式： head(tail(n) (odd())) = head(tail(2n) ()) head(tail(2n) (merge(, ))) = head(tail(n) ()) head(tail(2n + 1)(merge(, ))) = head(tail(n) ()) – 然后利用等式演算证明 head(tail(n) (merge(odd(), even()))) = head(tail(n) ())
6.2 归纳和余归纳 6.2.2归纳和余归纳指南 ·从集合论角度介绍余归纳定义和余归纳证明 原理 ·略去不介绍
6.2 归纳和余归纳 6.2.2 归纳和余归纳指南 • 从集合论角度介绍余归纳定义和余归纳证明 原理 • 略去不介绍
6.2 归纳和余归纳 6.2.3代数和余代数 从普通算法到交互计算的转变在数学上表现 为一系列的扩展 一从归纳到余归纳的扩展 表达了从字符串到流的转变 一从良基集到非良基集的扩展 非良基集作为流的行为的形式模型被引入 -从代数到余代数的扩展 余代数为流的演算提供工具，它相当于)演算在 图灵计算模型中的地位
6.2 归纳和余归纳 6.2.3 代数和余代数 • 从普通算法到交互计算的转变在数学上表现 为一系列的扩展 – 从归纳到余归纳的扩展 表达了从字符串到流的转变 – 从良基集到非良基集的扩展 非良基集作为流的行为的形式模型被引入 – 从代数到余代数的扩展 余代数为流的演算提供工具，它相当于演算在 图灵计算模型中的地位
6.2 归纳和余归纳 交换图表 可用来表达函数之间的等式 Z V,gl fg〉 X Inleft X+Y Inright X Proj2 二元和的交换图表 二元积的交换图表 K,g〉()=〈f(2),g(3)》 f(x)如果w=(0,x〉 [f,g1(w)= g(y)如果w=,y)
6.2 归纳和余归纳 • 交换图表 可用来表达函数之间的等式 f, g(z) = f (z), g(z) [f, g](w) = 二元积的交换图表 Y Z f, g X X Y Proj1 f g Proj2 Z [f, g] X X + Y Y Inleft f g Inright 二元和的交换图表 ( ) 0, ( ) 1, f x w x g y w y = = 如果 如果