Past exam of the year 1 of the computer science course of the University of Oxford / 2021 / Functional programming, design and analysis of algorithms (resit) / 1

The empty-list case uses $f(a)=b$. At a cons, assuming the equality for the tail, the calculation isThe middle equality is the supplied compatibility condition, instantiated with the folded tail; the last expression is the right fold on the whole list. Structural induction therefore proves fusion for finite total spines.

The strictness condition accounts for a bottom-valued input spine: the inner list fold returns bottom, and $f(\perp )=\perp$ makes the two sides agree. The same induction covers finite partial lists. For pure definable continuous functions, an infinite list is the limit of its finite partial approximations, so equality extends to it. These are the three distinct obligations in the right-fold fusion law; strictness is not needed if the domain is restricted to finite terminating spines.

Yes. Define the combining function as follows:For the fusion derivation use the identity reconstruction foldr (:) [], take $f=\mathrm{takeWhile}p$, and choose the displayed step as $h$. The function $f$ is strict in the input list, $f([])=[]$, and its cons equation is exactly $f(x:xs)=hx(f(xs))$. Fusion gives the implementation. On a false test, step does not demand the folded tail, so the implementation can terminate after a finite list prefix even when the remaining list is infinite or undefined. An undefined predicate result at a tested element makes both definitions undefined.

In general, no direct list fold with result type [a] can implement dropWhile p. Choose total values $u,v$ for which $p(u)=\mathrm{True}$ and $p(v)=\mathrm{False}$. The results on [] and [u] are both []. A hypothetical implementation foldr h z would therefore receive identical folded-tail values when extending either input by the same head $v$. Yet the required outputs are [v] and [v,u], respectively. This contradicts the fold factorisation criterion: the combining function cannot distinguish information already discarded by its tail summary.

The claim concerns a direct same-result-type list fold. A list fold returning extra information, followed by a projection, is possible: a pair can retain both the original tail and the dropped list suffix. Also, special predicates can have direct list folds: a constantly false predicate gives the identity; a constantly true predicate can use foldr (\_ r -> r) [], which correctly diverges when it must traverse an infinite spine. Those special cases do not supply an implementation for an arbitrary predicate.

The necessary definedness condition is local: every predicate application actually reached before the first false result must produce a Boolean value. No condition is needed on predicate applications after that first false result, because the list suffix is then returned without further testing. If a reached test is bottom at a known cons cell, the reconstructed list is bottom at that position, while the original list still exposes a cons there; equality fails.

To prove sufficiency on finite lists, induct on the spine. The empty case gives [] ++ [] = []. At a true test the left list prefix contributes the head, and the induction hypothesis reconstructs the tail. At a false test the list prefix is empty and the list suffix is the whole current list. For an infinite true-tested list prefix, every finite output list prefix is copied correctly; the infinite list prefix hides the possibly divergent list suffix computation. A partial spine ending in bottom is reconstructed up to exactly the same bottom. Thus finiteness is sufficient for an elementary induction proof but is not itself necessary for the identity.

For the uniform list fold calculation in part (f), use the convenient stronger assumption that the input is a finite total list and the predicate terminates on every element of that list. This makes the reconstruction identity available on every list suffix, not only on the list suffixes visited by the original list prefix scan. A total predicate on the element type ensures this uniformly over all finite total inputs.

For the finite total inputs just specified, a recursive implementation isAt a true test, the head belongs to the list prefix and splitting continues on the tail; at a false test, the complete remaining list is the list suffix. Induction proves that the first projection is the longest accepted list prefix and the second projection is the remaining list suffix.

There is a small partial-value distinction behind the paper's displayed pair identity. The conventional recursive span is strict in an entirely undefined list, whereas the literal expression (takeWhile p undefined, dropWhile p undefined) exposes an outer pair with two undefined components. The equality as a pair therefore needs the stated defined-input convention, or an interpretation that compares the two projections. This does not affect the finite total answers here.^[ref]

Yes, under the finite total assumption in part (d). The pair result retains enough information to reconstruct the tail; the ~ pattern keeps its two components lazy:Take $f=\mathrm{spanP}p$, $g=(:)$ and $a=[]$. The base image is $([],[])$. If $p(x)$ is true, the recursive equation gives the first branch. If it is false, part (d), applied to the tail, gives $ys++zs=xs$, so the second branch becomes $([],x:xs)$. These are precisely the fusion compatibility equations. Finite structural induction establishes the desired equality; it does not require extending the restricted-domain hypothesis to undefined predicate applications.

The qualification matters. If $p(v)$ is false but $p(u)$ is undefined, ordinary spanP p [v,u] can return the untouched list suffix immediately, whereas the reconstruction through spanFold p [u] cannot recover that list suffix. The weaker condition needed only for the single reconstruction identity in (d) is therefore insufficient for this particular list fold on all list suffixes. The stronger totality condition stated there supplies exactly the missing premise.