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 / d

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.