= Solution
Fix `s` and put $R(xs,a)=\mathrm{foldr}\ (k\ s)\ \mathrm{id}\ xs\ a$. The <right fold> equations give
$$
R([],a)=a,\qquad R(x:xs,a)=R(xs,s\ a\ x).
$$
These are exactly the <left fold> equations. <Structural induction>, with the induction hypothesis quantified over \i[all] accumulators, proves equality on finite terminating <lists>.
To include the other input spines, first observe that both applied expressions give $\bot$ on an undefined spine. The same induction proves equality on every finite prefix ending in $\bot$: the step `k s x f a` demands the continuation `f` when its result is demanded. Finally use that the two applied operations are <Scott continuous maps>, taking the limit over prefixes interpreted as a <finite approximation of a lazy list>. This covers infinite spines, on which both applied expressions are $\bot$, and proves the identity for all <lists> under the stated <Haskell> semantics. The intermediate <right fold> builds an accumulator-transforming <function>; it does not provide a terminating <left fold> of an infinite <list>.
Back to article page
