Structural induction

Structural induction proves a property of every recursively generated object by checking the initial objects and showing that every construction rule preserves the property.

For an admissible predicate on lazy lists $P$, prove $P(\perp )$ and $P([])$, and prove $P(xs)\Rightarrow P(x:xs)$ for every possibly partial head $x$. Constructor induction then establishes $P$ on every finite partial approximation, and admissibility extends it to limits, including infinite lists. Without the bottom value case and the limit condition, ordinary finite structural induction does not justify a claim about infinite data.^[ref]

A predicate on possibly partial lists is admissible when it holds at the limit of every increasing chain of finite approximations on which it holds. Increasing here means replacing a bottom value by more defined information while retaining already defined constructors and values. This closure condition permits a property established for finite approximations to pass to an infinite list. The predicate “the list is finite” lacks this closure: every finite prefix ending in an undefined tail is finite in extent, but their limit may have infinitely many constructors.