Sufficient conditions for folded and folded equivalence

Question

Consider the expressions E1 = foldl op acc l and E2 = foldr op acc l .

What are the natural sufficient conditions for op , acc and / or l that guarantee the equivalence of E1 and E2 ?

A naive example would be that if op is constant, then both are equivalent.

I am sure that there must be clear conditions, including the commutativity and / or associativity of op , and / or the finiteness of l , and / or the neutrality of acc .

Answer 1

If op is an associative operation, acc is a neutral element of op , and l finite, then they are equivalent.

Indeed, the result of foldr is

 (l1 `op` (l2 `op` ... (ln `op` acc))) 

and <<26> -

 (((acc `op` l1) `op` l2) `op` ... ln) 

To prove that they are equal, it is enough to simplify acc and reassign.

---

Even if acc not a neutral element, but acc still satisfies the weaker condition

 forall x, acc `op` x = x `op` acc 

then, if op associative and l finite, we again obtain the required equivalence.

To prove this, we can use the fact that acc commutes with everything and “moves” it from the position of the tail to the head, using associativity. For instance.

 (l1 `op` (l2 `op` acc)) = (l1 `op` (acc `op` l2)) = ((l1 `op` acc) `op` l2) = ((acc `op` l1) `op` l2) 

The question mentions the sufficient condition op = const k , which is associative, but does not have a neutral element. Nevertheless, any acc commutes with everything, therefore the case of the “constant op ” is a subcase of the above sufficient condition.

---

Assuming op has a neutral element acc , if we assume that

 foldr op acc [a,b,c] = foldl op acc [a,b,c] -- (*) 

we get

 a `op` (b `op` c) = (a `op` b) `op` c 

Therefore, If (*) holds for all a,b,c , then op must be associative. Then associativity becomes necessary and sufficient (when there is a neutral element).

---

If l infinite, foldl always diverges no matter what op,acc . If op strictly in the second argument, foldr also diverges (i.e. returns the bottom).