= Admissible predicate on lazy lists
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.
Back to article page
