Lazy list

A linked list whose future structure is obtained by calling a delayed computation. In Standard ML, unit -> node delays a computation until demand. Filtering may need to force arbitrarily many rejected elements to produce its next retained element; filtering an infinite list need not produce a result. Delay alone does not imply memoization.

// Destination: computer-science.bigb

A proper lazy list has a spine exposing either finitely many cons constructors followed by [], or infinitely many cons constructors, without an undefined tail at a finite position. This is a condition on the spine: an element may itself be the bottom value without hiding the list's constructors. A partial list with a finite visible prefix followed by $\perp$ fails this condition. The distinction supports productivity proofs that inspect constructors without evaluating the stored elements.

A generic correct scan cannot always terminate with a certificate that a value is absent from an arbitrary infinite list. Any terminating scan observes only finitely many elements. Changing the unobserved tail to include the value preserves all its observations but invalidates the certificate. The same argument prevents certifying that no occurrence follows the last one already found. A promise such as strict ascending order can provide an independent stopping rule. This explains why mathematical occurrence sets and computed occurrence-position representations of a sequence need different treatment on infinite inputs.

A stream computation is productive when every demanded finite prefix of its output can be produced in finite work. Filtering an infinite list need not be productive: asking for odd elements of [0,2..] never produces even an empty-list constructor. Lazy evaluation alone does not prove productivity.

A list whose spine or elements may contain bottom values. The displayed value has a known finite spine prefix and an undefined tail. An entirely undefined list exposes no outer constructor, while [] exposes a terminating empty list. These distinctions matter to strict functions and to the fold factorisation criterion.

No generic sequential pure Haskell operation can guarantee emission of every available input occurrence when either of two input spines may be the bottom value. To obtain an arbitrary element, it must eventually demand one input. That input can be undefined while the other is a defined singleton, so the demand blocks the promised singleton output. Choosing the other input first reverses the counterexample. Lazy evaluation cannot determine which computation will diverge; the positive two-stream fairness result needs proper lazy lists or a stronger concurrent computational model.

A finite list prefix followed by bottom records only the constructors known so far. The chain $\perp ,x_1:\perp ,x_1:x_2:\perp ,\dots$ approximates an infinite lazy list. A Scott continuous map is determined on the limit by its values on these approximations. This justifies extending an identity proved on finite partial lists to definable operations on infinite lists; equality merely on finite terminating lists does not provide the same premise.