的定义： head(odd())=head(o) tail(odd(=odd(tail(tail() 第一个等式说，oddo)的第一个元素是o的第一个元素：oddo)的第二个元素是head(tail (oddo),用等式演算可得： head(tail(odd(o)))=head(odd(tail(tail(o)))=head(tail(tail(o))) 因此odd(o)的第二个元素是o的第三个元素。这正是所需要的。不难证明，对所有的自然数n, head(taiNm(oddo)和head(tail2m(o)一样。 这两个等式是纯数学规范。若要从计算的角度来看这两个等式，则必须用惰性计算的观 点。 O 最后考虑余归纳的证明。余归纳定义的数据和函数的某些性质可以用归纳法来证明，例 如例6.3中的对所有的自然数n,head(tail"(odd(o)和head(tai(σ)一样。余归纳证明的一种 专用方法基于互模拟(bisimulation)的概念。互模拟从数学上刻画系统（如对象、进程等） 行为等价这个直观概念，它是指两个系统从观测者角度看可以互相模拟对方的行为，即从观 测者角度，两个系统对同样的输入会产生同样的输出，系统内部可能有的状态不同是观察不 到的。还是以无限表为例，来解释基于互模拟的证明方法。 例6.4先余归纳地定义函数even,,它应用到一个无限表上，忽略其所有奇数位置上的元 素，将其剩余元素按原来次序形成一个新的无限表。显然ven可以这样定义： even odd o tail 再定义应用到两个无限表o和的归并函数merge。.merge依次从o和轮流取元素，形成 一个新的无限表。同样，merge的余归纳定义需要解构子head和tail在merge(o,)上的结果： head(merge(o,t))=head(o) tail(merge(o,T))=merge(t,(tail()) 下面基于互模拟证明nergel(oddo),even(o)=o。无限表集合上的互模拟是满足下面条 件的二元关系R: 若(a,t)∈R,则head)=head)并且(ailo,tail(》∈R。 在无限表集合上基于互模拟的余归纳证明原理是： 对互模拟关系R,若(c,)∈R,则o=t。 国 R={(merge(odd(o),even(o),lo是一个无限表} 根据该余归纳证明原理，为了证明merge(oddσ)，even(σ)=o,只要证明R是互模拟关系就可 以了，也就是要证明互模拟关系的两个必要条件。 对于第一个条件，有 head(merge(odd(o),even(G)))=head(odd(G))=head(o) 对第二个条件，若有merge(oddo),even(o),o)∈R,则把1ail应用到该序对的两元时，产生 的新序对组tail(merge(oddo),even(o),tail(》也在R中，因为tail(merge(oddo),even(》= merge(odd1ail(oj,even(tail(o))。利用even=oddotail,该等式的证明如下： tail(merge(odd(o),even()))=merge(even(o),tail(odd()) =nerge(odd(tail(σ)，odd(tail(tail(o)) =merge(odd(tail(o)),even(tail())) 利用归纳和等式演算，也可以证明nerge(oddo),even(o)=o,但是没有这么简单。可 以对所有的自然数，用归纳法先证明下面几个等式： head(tail"(odd())=head(tai() head(tailm(merge(o,))=head(taikm()) 33 的定义： head(odd(σ)) = head(σ) tail(odd(σ)) = odd(tail(tail(σ))) 第一个等式说，odd(σ)的第一个元素是σ的第一个元素；odd(σ)的第二个元素是head(tail (odd(σ)))，用等式演算可得： head(tail(odd(σ))) = head(odd(tail(tail(σ)))) = head(tail(tail(σ))) 因此odd(σ)的第二个元素是σ的第三个元素。这正是所需要的。不难证明，对所有的自然数n， head(tail(n) (odd(σ)))和head(tail(2n) (σ))一样。 这两个等式是纯数学规范。若要从计算的角度来看这两个等式，则必须用惰性计算的观 点。 ￾ 最后考虑余归纳的证明。余归纳定义的数据和函数的某些性质可以用归纳法来证明，例 如例6.3中的对所有的自然数n，head(tailn (odd(σ)))和head(tail2n (σ))一样。余归纳证明的一种 专用方法基于互模拟（bisimulation）的概念。互模拟从数学上刻画系统（如对象、进程等） 行为等价这个直观概念，它是指两个系统从观测者角度看可以互相模拟对方的行为，即从观 测者角度，两个系统对同样的输入会产生同样的输出，系统内部可能有的状态不同是观察不 到的。还是以无限表为例，来解释基于互模拟的证明方法。 例6.4 先余归纳地定义函数even，它应用到一个无限表上，忽略其所有奇数位置上的元 素，将其剩余元素按原来次序形成一个新的无限表。显然even可以这样定义： even = odd D tail 再定义应用到两个无限表σ和τ的归并函数merge。merge依次从σ和τ轮流取元素，形成 一个新的无限表。同样，merge的余归纳定义需要解构子head和tail在merge(σ, τ)上的结果： head(merge(σ, τ)) = head(σ) tail(merge(σ, τ)) = merge(τ, (tail(σ)) 下面基于互模拟证明merge(odd(σ), even(σ)) = σ。无限表集合上的互模拟是满足下面条 件的二元关系R： 若〈σ, τ〉 ∈R，则head(σ) = head(τ)并且〈tail(σ), tail(τ)〉 ∈R。 在无限表集合上基于互模拟的余归纳证明原理是： 对互模拟关系R，若〈σ, τ〉 ∈R，则σ = τ。 令 R = {〈merge(odd(σ), even(σ)), σ〉 | σ是一个无限表} 根据该余归纳证明原理，为了证明merge(odd(σ), even(σ)) = σ，只要证明R是互模拟关系就可 以了，也就是要证明互模拟关系的两个必要条件。 对于第一个条件，有 head(merge(odd(σ), even(σ))) = head(odd(σ)) = head(σ) 对第二个条件，若有〈merge(odd(σ), even(σ)), σ〉 ∈R，则把tail应用到该序对的两元时，产生 的新序对组〈tail(merge(odd(σ), even(σ))), tail(σ)〉也在R中，因为tail(merge(odd(σ), even(σ))) = merge(odd(tail(σ)), even(tail(σ)))。利用even = odd D tail，该等式的证明如下： tail(merge(odd(σ), even(σ))) = merge(even(σ), tail(odd(σ)) = merge(odd(tail(σ)), odd(tail(tail(σ)))) = merge(odd(tail(σ)), even(tail(σ))) 利用归纳和等式演算，也可以证明merge(odd(σ), even(σ)) = σ，但是没有这么简单。可 以对所有的自然数n，用归纳法先证明下面几个等式： head(tail(n) (odd(σ))) = head(tail(2n) (σ)) head(tail(2n) (merge(σ, τ))) = head(tail(n) (σ))