Absence-detection obstruction for infinite lists
ID: absence-detection-obstruction-for-infinite-lists
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.
New to topics? Read the docs here!