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 $P([])$ and $P(xs)\Rightarrow P(x:xs)$ for every head $x$ and tail $xs$. This proves $P$ for every finite list.

An infinite list cannot be reached by finitely many constructor steps. For structural induction on lazy lists, also check $P(\perp )$, where $\perp$ is the bottom value, and require an admissible predicate on lazy lists: if increasingly defined finite approximations all satisfy $P$, 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.