{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,28]],"date-time":"2025-10-28T00:27:19Z","timestamp":1761611239174,"version":"3.41.2"},"reference-count":0,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2008,8,27]],"date-time":"2008-08-27T00:00:00Z","timestamp":1219795200000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We say that a set is exhaustible if it admits algorithmic universal\nquantification for continuous predicates in finite time, and searchable if\nthere is an algorithm that, given any continuous predicate, either selects an\nelement for which the predicate holds or else tells there is no example. The\nCantor space of infinite sequences of binary digits is known to be searchable.\nSearchable sets are exhaustible, and we show that the converse also holds for\nsets of hereditarily total elements in the hierarchy of continuous functionals;\nmoreover, a selection functional can be constructed uniformly from a\nquantification functional. We prove that searchable sets are closed under\nintersections with decidable sets, and under the formation of computable images\nand of finite and countably infinite products. This is related to the fact,\nestablished here, that exhaustible sets are topologically compact. We obtain a\ncomplete description of exhaustible total sets by developing a computational\nversion of a topological Arzela--Ascoli type characterization of compact\nsubsets of function spaces. We also show that, in the non-empty case, they are\nprecisely the computable images of the Cantor space. The emphasis of this paper\nis on the theory of exhaustible and searchable sets, but we also briefly sketch\napplications.<\/jats:p>","DOI":"10.2168\/lmcs-4(3:3)2008","type":"journal-article","created":{"date-parts":[[2009,1,9]],"date-time":"2009-01-09T10:20:39Z","timestamp":1231496439000},"source":"Crossref","is-referenced-by-count":15,"title":["Exhaustible sets in higher-type computation"],"prefix":"10.46298","volume":"Volume 4, Issue 3","author":[{"given":"Martin","family":"Escardo","sequence":"first","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2008,8,27]]},"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/693\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/693\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:53:57Z","timestamp":1681242837000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/693"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2008,8,27]]},"references-count":0,"URL":"https:\/\/doi.org\/10.2168\/lmcs-4(3:3)2008","relation":{"is-same-as":[{"id-type":"arxiv","id":"0808.0441","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.0808.0441","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2008,8,27]]},"article-number":"693"}}