论文标题
机器空间I：紧凑空间上的弱指数和量化
Machine Space I: Weak exponentials and quantification over compact spaces
论文作者
论文摘要
拓扑可以解释为对可验证性的研究，其中打开对应于半独立属性。在本文中，我们将可验证属性本身与执行验证程序的过程进行区分。前者只是打开，而我们称之为后者。给定一个帧表示$ \ MATHCAL {O} x = \ langle g \ mid r \ rangle $，我们构建了一个机器的空间$σ^{σ^g} $，其点由与$ 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 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.
