Solution

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

For finite, defined lists, structural induction requires and for every head and tail . This proves for every finite list.
An infinite list cannot be reached by finitely many constructor steps. For structural induction on lazy lists, also check , where is the bottom value, and require an admissible predicate on lazy lists: if increasingly defined finite approximations all satisfy , their limit does too. Together with the empty-list and constructor cases this covers finite, partial and infinite lists. Merely asserting the two finite-list cases is insufficient; “the list is finite” itself satisfies those cases but fails on infinite lists.

New to topics? Read the docs here!