融合法为foldr1？ [英] Fusion law for foldr1?

问题描述

对于 foldr ，我们有融合法则：如果 f 是严格的， fa = b 和

f（gxy）= hx（fy），所有 x，y ，然后 f。 foldr ga = foldr hb 。

如何发现/推导类似于 foldr1 ？ （它显然甚至不能采用相同的形式 - 考虑双方在 [x] 之上采取行动的情况。）

解决方案

您可以使用自由定理来推导像融合律那样的陈述。 自动生成自由定理如果您输入 foldr1 或类型（a - > a - > a） - >>，则会自动导出以下语句; [a] - > a 。

如果 f strict且 f（pxy ）= q（fx）（fy））所有 x 和 y f（foldr1 pz）= foldr1 q（map fz））。也就是说，与你对 foldr 的陈述相反，你会在右侧获得一个额外的 map f 。 p>

另外请注意， foldr 的自由定理比你的融合规律稍微普遍一些，因此看起来非常相似 foldr1 的法律。也就是说，如果 g（pxy）= q（fx），您必须使用 g 和 f ），所有 x 和 y 然后 g（foldr pzv）= foldr q（gz）（map fv））。

For foldr we have the fusion law: if f is strict, f a = b, and

f (g x y) = h x (f y) for all x, y, then f . foldr g a = foldr h b.

How can one discover/derive a similar law for foldr1? (It clearly can't even take the same form - consider the case when both sides act on [x].)

解决方案

You can use free theorems to derive statements like the fusion law. The Automatic generation of free theorems does this work for you, it automatically derives the following statement if you enter foldr1 or the type (a -> a -> a) -> [a] -> a.

If f strict and f (p x y) = q (f x) (f y)) for all x and y you have f (foldr1 p z) = foldr1 q (map f z)). That is, in contrast to you statement about foldr you get an additional map f on the right hand side.

Also note that the free theorem for foldr is slightly more general than your fusion law and, therefore, looks quite similar to the law for foldr1. Namely you have for strict functions g and f if g (p x y) = q (f x) (g y)) for all x and y then g (foldr p z v) = foldr q (g z) (map f v)).

这篇关于融合法为foldr1？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！