World's most popular travel blog for travel bloggers.

# Proving equality between foldl recursive and iterative fold

, ,
Problem Detail:

Hi I have two definitions of fold. I will call them foldl which is recursive and fold$_{itr}$ which is iterative.

I am looking for an algebraic proof that the two definitions are equal ideally through structural induction.

Definition for foldl

foldl(c,h) nil = c  foldl(c, h) (list, element) = h (foldl (c, h) list, element) 

Definition for fold$_{itr}$

fold$_{itr}$ (c, h) nil = nil

fold$_{itr}$ (c, h) (element, list) = fold$_{itr}$ (h(c, element), h) list

###### Answered By : Andrej Bauer

The two definitions are not equal. Consider $h$ defined by \begin{align*} h(c, a) = 10 \cdot c + a \end{align*} and $c = 0$. Then $$\mathsf{foldl} \, (c,h) \, [1,2,3] = 321$$ but $$\mathsf{fold}_{itr} \, (c,h) \, [1,2,3] = 123.$$