一句话：引入机器空间区分可验证性质与其验证过程，构造弱指数，并给出紧空间上全称量化的拓扑算法。
本文从可验证性视角重新审视拓扑：开集对应半可判定性质，但性质本身与执行验证的“机器”需要区分。作者由 frame 表示 O X = ⟨G | R⟩ 构造机器空间 Σ^{Σ^G}，其点对应于生成元所对应基本机器的形式组合，并配备求值映射，使其成为以 Σ 为底、X 为指数的弱指数；真正的指数 Σ^X 若存在，则作为机器空间的收缩出现。这一构造被用于解释空间可指数化的条件。作者进一步用机器空间研究紧性，给出 Escardó 关于紧空间上全称量化可在有限时间内完成的算法的纯拓扑版本，并将机器空间与域理论及域嵌入联系起来。
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 \emph{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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{FaulM26,
title = {Machine Space I: Weak exponentials and quantification over compact spaces},
author = {Peter F. Faul and Graham Manuell},
journal = {Logical Methods in Computer Science},
volume = {Volume 22, Issue 2},
year = {2026},
doi = {10.46298/lmcs-22(2:2)2026}
}