Solution

ID: past-exam-of-the-year-1-of-the-computer-science-course-of-the-university-of-oxford/2019/functional-programming-design-and-analysis-of-algorithms/1/g/solution

Fix s and put . The right fold equations give
These are exactly the left fold equations. Structural induction, with the induction hypothesis quantified over all accumulators, proves equality on finite terminating lists.
To include the other input spines, first observe that both applied expressions give on an undefined spine. The same induction proves equality on every finite prefix ending in : 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 , 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.

New to topics? Read the docs here!