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 $Σ^{Σ^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 with base $Σ$ and exponent $X$. When it exists, the true exponential $Σ^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ó'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$，我们构造一个机器空间 $Σ^{Σ^G}$，其点由对应于生成元 $G$ 的基本机器的形式组合给出。该空间配备了一个"求值"映射，使其成为以 $Σ$ 为底、$X$ 为指数的弱指数空间。当真实指数空间 $Σ^X$ 存在时，它将作为机器空间的收缩核出现。我们认为这有助于解释为何某些空间可指数化而其他空间则不能。随后，我们利用机器空间研究紧性，给出了埃斯卡多算法的纯拓扑版本，该算法可在有限时间内实现紧空间上的全称量化。最后，我们将机器空间研究与域理论及域嵌入理论建立联系。