Martin Escardo

Infinite Sets That Admit Exhaustive Search

Abstract: Perhaps surprisingly, there are infinite sets that admit
mechanical exhaustive search in finite time. We investigate three
related questions: (1) What kinds of infinite sets admit exhaustive
search? (2) How do we systematically build such sets? (3) How fast can
exhaustive search over infinite sets be performed?  We give answers to
them in the realm of Kleene-Kreisel higher-type computation: (1)
involves the topological notion of compactness and includes an
Arzela-Ascoli type characterization, (2) amounts to the usual closure
properties of compact sets, including the Tychonoff theorem, (3)
provides some fast algorithms and a run-time conjecture involving
moduli of uniform continuity. In order to obtain these results, we
approach Kleene-Kreisel functionals both via domain theory and via
compactly generated spaces.