Consider the expressions E1 = foldl op acc l and E2 = foldr op acc l.
What are some natural sufficient conditions for op, acc and/or l that guarantee the equivalence of E1and E2?
A naive example would be that if opis constant then both are equivalent.
I'm pretty sure there must be precise conditions involving commutativity and/or associativity of op, and/or finitude of l, and/or neutrality of acc.
If op is an associative operation, acc is a neutral element of op, and l is finite, then they are equivalent.
Indeed, the result of foldr is
(l1 `op` (l2 `op` ... (ln `op` acc)))
while that of foldl is
(((acc `op` l1) `op` l2) `op` ... ln)
To prove that they are equal, it suffices to simplify acc away, and reassociate.
Even if acc is not a neutral element, but acc still satisfies the weaker condition
forall x, acc `op` x = x `op` acc
then, if op is associative and l is finite, we again get the desired equivalence.
To prove this, we can exploit the fact that acc commutes with everything, and "move" it from the tail position to the head one, exploiting associativity. E.g.
(l1 `op` (l2 `op` acc))
=
(l1 `op` (acc `op` l2))
=
((l1 `op` acc) `op` l2)
=
((acc `op` l1) `op` l2)
In the question it is mentioned the sufficient condition op = const k which is associative but has no neutral element. Still, any acc commutes with everything, so the "constant op" case is a subcase of the above sufficient condition.
Assuming op has a neutral element acc, if we assume
foldr op acc [a,b,c] = foldl op acc [a,b,c] -- (*)
we derive
a `op` (b `op` c) = (a `op` b) `op` c
Hence, If (*) holds for all a,b,c, then op has to be associative. Associativity is then necessary and sufficient (when a neutral element exists).
If l is infinite, foldl always diverges no matter what op,acc are. If op is strict on its second argument, foldr also diverges (i.e., it returns bottom).