Past exam of the year 1 of the computer science course of the University of Oxford / 2005 / Functional programming, data structures and algorithms, procedural programming, and digital hardware / 1

The map function transforms each head and recursively processes the tail. A right fold combines a head with the result for its tail, whereas a left fold passes an updated accumulator into the recursive call. In Haskell:

import Prelude hiding (map, foldr, foldl, concat)

map f [] = []
map f (x:xs) = f x : map f xs

foldr op e [] = e
foldr op e (x:xs) = op x (foldr op e xs)

foldl op e [] = e
foldl op e (x:xs) = foldl op (op e x) xs

concat = foldr (++) []

The last right fold uses list concatenation to replace each outer cons by appending its inner list. Thus concat [xs,ys,zs] = xs ++ (ys ++ (zs ++ [])). Its right fold association matters: appending a list traverses its left spine, so these equations traverse each inner spine once on finite inputs. The concise answer is

Let $P(zss)$ mean concat (map f zss) = f (concat zss). We use structural induction on lazy lists, including the bottom value and allowing arbitrary, possibly partial, inner lists.

For [], the left side is [] and the right side is f [] = []. For the bottom value $\perp$, both map f and concat are strict functions in the outer spine, and the supplied strictness of $f$ makes the right side $f\perp =\perp$ too.

For the cons case, assume $P(zss)$ and write the new head as xs. The defining equations and the induction hypothesis giveThe third equality is exactly the supplied list concatenation preservation law. No inspection of xs was required, so the argument includes partial inner lists and undefined elements.

This proves the identity for every finite outer spine ending in either [] or $\perp$. In the usual pure Haskell semantics, these functions are Scott continuous maps. An infinite outer list is obtained as a limit by finite approximation of a lazy list; both composite functions preserve that limit. Equality on all its finite approximations therefore gives equality on the infinite outer list. Equivalently, $P$ is an admissible predicate on lazy lists. ConsequentlyThe continuity assumption is the usual semantic assumption for definable functions here; an extension from finite to infinite inputs cannot be justified by ordinary finite induction alone.

Use function extensionality: show $f(x)=g(x)$ for every value $x$ of the argument type. In lazy evaluation semantics, “every value” includes the bottom value and partial values. For list arguments, structural induction on lazy lists supplies the empty, bottom and cons cases, with continuity justifying passage to infinite lists.

The original printed equation has the same right fold on both sides, including the same operator and seed; this is visible in the scan.^[ref] Thus its literal answer isFor every input $xs$, both sides denote the very same expression foldr (oplus) e xs; equality follows by reflexivity. This remains true if its value is $\perp$. Neither termination nor associativity nor an identity law is required. The scan does not establish a different intended equation, so no replacement by a left fold is assumed.