= Structural induction on lazy lists
For an <admissible predicate on lazy lists> $P$, prove $P(\bot)$ 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.https://ethz.ch/content/dam/ethz/special-interest/infk/inst-infsec/information-security-group-dam/people/andreloc/lochbihler14itps.pdf[Recursive Functions on Lazy Lists, ITP 2014 presentation, slide 7: admissibility restriction on induction over lazy lists]{ref}
Back to article page
