Machine Space I: Weak exponentials and quantification over compact spaces

TL;DR

This paper introduces a novel concept of machine space in topology, distinguishing verifiable properties from verification processes, and explores its implications for exponentials, compactness, and domain theory.

Contribution

It constructs a space of machines as a weak exponential, providing insights into exponentiability, and offers a topological approach to universal quantification over compact spaces.

Findings

Machine space is a weak exponential with a base and exponent related to topology.

Exponential spaces occur as retracts of machine spaces when they exist.

A topological version of Escardó's algorithm for quantification over compact spaces is developed.

Abstract

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 $\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 with base $\Sigma$ and exponent $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.