haskell 证明过滤器(所有p),cp = cp . map(filter p)

zsbz8rwp  于 2023-05-07  发布在  其他
关注(0)|答案(1)|浏览(136)

在Richard Bird的 Thinking Functionally with Haskell 一书的第五章中,有一个等式:
过滤器(全部p)。cp = cp . map(filter p)
我想知道如何证明这一点?(聚变定律)?
我试图用聚变定律来证明。但如何证明聚变定律呢?

zxlwwiss

zxlwwiss1#

用foldr重写cp

cp = folder g [[]]
        where g xs xss = [x:ys|x<-xs,ys<-xss]

假设:(a)filter(all p)(cp xss)= cp(map(filter p)xs)= folder g (map(filter p)xs)
应证明等式(B)成立

(b)    filter (all p) (cp (xs:xss)) = cp (map (filter p) (xs:xss)) 

{# definition of map and cp #}
cp (map (filter p) (xs:xss)) = foldr g [[]] (map (filter p) (xs:xss))
{# definition of folder #}
g (filter p xs) (foldr g [[]] (map (filter p)) xss)

{#基于假设(a)#)g(filter p xs)(filter(all p)(cp xss))

{# definition of g #}
[x:ys|x<-filter p xs, ys<-filter (all p) (cp xss)]
{# definition of filter 
[x:ys|x<-[x' <- xs,p x'], ys <- [ys' <- (cp xss), (all p) ys']]

{# condiontial cp means cp after filter #}

filter (all p) (cp (xs:xss))

In conclusion,
cp (map (filter p) (xs:xss)) = filter (all p) (cp (xs:xss))

相关问题