Topology may be interpreted as the study of verifiability, where opens correspond to semi-decidable properties. In this paper we make a distinction between verifiable properties themselves and processes which carry out the verification procedure. The former are simply opens, while we call the latter machines. Given a frame presentation $\mathcal{O} X = \langle G \mid R\rangle$ we construct a space of machines $\Sigma^{\Sigma^G}$ whose points are given by formal combinations of basic machines corresponding to generators in $G$. This comes equipped with an `evaluation' map making it a weak exponential for $\Sigma^X$. When it exists, the true exponential $\Sigma^X$ occurs as a retract of machine space. We argue this helps explain why some spaces are exponentiable and others not. We then use machine space to study compactness by giving a purely topological version of Escard\'o's algorithm for universal quantification over compact spaces in finite time. Finally, we relate our study of machine space to domain theory and domain embeddings.

翻译：拓扑学可被诠释为可验证性的研究，其中开集对应半可判定性质。本文区分了可验证性质本身与执行验证过程的机制——前者为开集，后者称为机器。给定框架呈现$\mathcal{O} X = \langle G \mid R\rangle$，我们构造了一个机器空间$\Sigma^{\Sigma^G}$，其点由对应于生成元$G$的基本机器的形式组合给出。该空间配备"求值"映射，使其成为$\Sigma^X$的弱指数。当真实指数$\Sigma^X$存在时，它作为机器空间的收缩核出现。我们论证这有助于解释为何某些空间可指数化而其他则非。进而利用机器空间研究紧致性，给出埃斯卡尔多关于紧致空间上有限时间内全称量化算法的纯拓扑版本。最后，我们将机器空间研究与域理论及域嵌入相关联。