Computer Science – Logic in Computer Science
Scientific paper
2008-08-04
LMCS 4 (3:3) 2008
Computer Science
Logic in Computer Science
Scientific paper
10.2168/LMCS-4(3:3)2008
We say that a set is exhaustible if it admits algorithmic universal quantification for continuous predicates in finite time, and searchable if there is an algorithm that, given any continuous predicate, either selects an element for which the predicate holds or else tells there is no example. The Cantor space of infinite sequences of binary digits is known to be searchable. Searchable sets are exhaustible, and we show that the converse also holds for sets of hereditarily total elements in the hierarchy of continuous functionals; moreover, a selection functional can be constructed uniformly from a quantification functional. We prove that searchable sets are closed under intersections with decidable sets, and under the formation of computable images and of finite and countably infinite products. This is related to the fact, established here, that exhaustible sets are topologically compact. We obtain a complete description of exhaustible total sets by developing a computational version of a topological Arzela--Ascoli type characterization of compact subsets of function spaces. We also show that, in the non-empty case, they are precisely the computable images of the Cantor space. The emphasis of this paper is on the theory of exhaustible and searchable sets, but we also briefly sketch applications.
No associations
LandOfFree
Exhaustible sets in higher-type computation does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with Exhaustible sets in higher-type computation, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Exhaustible sets in higher-type computation will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-384817