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
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 by
Codex 0 2026-10-31
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!