For foldr我们有融合定律: if f是严格的，f a = b, and
f (g x y) = h x (f y)对全部x, y, then f . foldr g a = foldr h b.
如何发现/导出类似的定律foldr1？ （显然甚至不能采取相同的形式 - 考虑双方都采取行动的情况[x].)
您可以使用自由定理来导出诸如融合定律之类的陈述。这自动生成自由定理 http://www-ps.iai.uni-bonn.de/cgi-bin/free-theorems-webui.cgi这对您有用吗？如果您输入，它会自动生成以下语句foldr1或类型(a -> a -> a) -> [a] -> a.
If f严格和f (p x y) = q (f x) (f y))对全部x and y你有f (foldr1 p z) = foldr1 q (map f z))。也就是说，与您的陈述相反foldr你会得到额外的map f在右手侧。
另请注意，自由定理foldr比您的融合定律稍微更一般，因此看起来与融合定律非常相似foldr1。也就是说你有严格的功能g and f if g (p x y) = q (f x) (g y))对全部x and y then g (foldr p z v) = foldr q (g z) (map f v)).
本文内容由网友自发贡献，版权归原作者所有，本站不承担相应法律责任。如您发现有涉嫌抄袭侵权的内容，请联系:hwhale#tublm.com(使用前将#替换为@)
