Machine Space I: Weak exponentials and quantification over compact spaces

1. Problem Statement

The paper addresses two interconnected foundational problems in topology and computer science, viewed through the lens of verifiability:

1. The Failure of Exponentials: In the category of topological spaces (or locales), the exponential object $\Sigma^X$ (representing the space of open sets or continuous maps to the Sierpiński space $\Sigma$) does not always exist. Specifically, if $X$ is not locally compact, the evaluation map $ev: \Sigma^X \times X \to \Sigma$ fails to be continuous. This creates a philosophical tension: if open sets represent "verifiable properties," one might intuitively expect that given a property and a point, one could verify membership. The mathematical reality (non-existence of the exponential) contradicts this intuition.
2. Uniform Universal Quantification: While it is known that compact spaces allow for universal quantification over open predicates in finite time (a concept central to Escardó's work in domain theory), it was unclear if there exists a uniform, purely topological algorithm for this quantification that applies to all compact spaces (not just specific data types or locally compact ones) without relying on a specific programming language semantics.

2. Methodology

The authors employ pointfree topology (locale theory) and construct a new mathematical object called Machine Space.

• Verifiability Interpretation: They interpret open sets as verifiable properties. A property is verifiable if membership can be established by finite means (semi-decidable).
• Distinction between Properties and Processes: The core innovation is distinguishing between the open set (the abstract property) and the machine (the concrete process/program that verifies the property).
  • Machines: Defined as formal combinations of "basic machines" corresponding to generators of a locale presentation.
  • Construction: Given a locale $X$ with a presentation $\mathcal{O}X = \langle G \mid R \rangle$ (generators $G$ and relations $R$), the authors construct the space $\Sigma^{\Sigma^G}$.
    • $\Sigma^G$ is the free frame on $G$ (the space of opens generated by $G$).
    • $\Sigma^{\Sigma^G}$ is the space of opens of $\Sigma^G$, which serves as the Machine Space.
• Weak Exponentials: They define a weak exponential as an object $Z$ equipped with an evaluation map $eev: Z \times X \to \Sigma$ such that for any $f: Y \times X \to \Sigma$, there exists some (not necessarily unique) $g: Y \to Z$ making the diagram commute. They prove that $\Sigma^{\Sigma^G}$ is a weak exponential for $X$.
• Algorithmic Approach: They translate the topological concept of compactness into an explicit semi-decision procedure (Algorithm 1) that operates on the syntax of the machine space.

3. Key Contributions

A. Machine Space as a Canonical Weak Exponential

The authors construct $\Sigma^{\Sigma^G}$ as a "reasonably canonical" weak exponential for any locale $X$ presented by $\langle G \mid R \rangle$.

• Points of Machine Space: The points are formal joins of finite meets of generators ($m = \bigvee_i \bigwedge_{j \in J_i} g_j$). These represent programs that run basic machines in parallel and halt if at least one branch halts (disjunction) and all machines in a branch halt (conjunction).
• Relationship to True Exponentials:
  • There is a canonical quotient map $q: \Sigma^{\Sigma^G} \twoheadrightarrow \Sigma^X$ (when $\Sigma^X$ exists) sending a machine to the open set it verifies.
  • Theorem: If $X$ is locally compact, this map $q$ has a continuous section $s: \Sigma^X \to \Sigma^{\Sigma^G}$. This section allows one to continuously assign a verification machine to every open set, explaining why the evaluation map is continuous in this case.
  • Theorem: If $X$ is not locally compact, no such continuous section exists. This resolves the philosophical puzzle: the "space of opens" fails to be an exponential because there is no continuous way to assign a verification procedure to every open set. The "machine space" always exists, but it is strictly larger than the space of opens when $X$ is not locally compact.

B. Uniform Algorithm for Universal Quantification

The paper provides Algorithm 1, a purely topological/locally algorithm for universal quantification over any compact locale $X$.

• Input: A machine $m \in \Sigma^{\Sigma^G}$ (representing a verifiable property).
• Output: A semi-decision procedure that halts if and only if $m$ accepts all points in $X$ (i.e., the open set defined by $m$ is the whole space).
• Mechanism:
  1. Iterate over all finite sets of finite subsets of generators $S \in \mathcal{P}_{fin}(\mathcal{P}_{fin}(G))$.
  2. Check if the formal join of these subsets covers $X$ (using the relations $R$).
  3. If a cover is found, test if the machine $m$ contains a branch corresponding to that cover (using the open $\boxtimes F$ in machine space).
  4. If a matching branch is found, the algorithm halts.
• Significance: This generalizes Escardó's algorithm (previously limited to specific data types like Cantor space) to arbitrary compact locales without assuming a specific computational model.

C. Connection to Domain Theory

The authors relate their construction to Domain Theory:

• The embedding $X \hookrightarrow \Sigma^G$ is viewed as a domain embedding, where $X$ is represented as a subquotient of a continuous dcpo (specifically, the power set of $G$).
• They show how to recover Escardó's specific algorithm for Cantor space by choosing a specific presentation and closure within the machine space framework.
• They demonstrate that the "partially defined" elements in the machine space correspond to the "undefined" elements in domain-theoretic models.

4. Results

1. Existence of Machine Space: For any locale $X$ with a presentation, the space $\Sigma^{\Sigma^G}$ always exists and serves as a weak exponential.
2. Characterization of Local Compactness: A locale $X$ is locally compact if and only if the quotient map from Machine Space to the Space of Opens ($\Sigma^{\Sigma^G} \to \Sigma^X$) admits a continuous section. This provides a new, constructive characterization of local compactness.
3. Compactness via Machine Space: A locale $X$ is compact if and only if the set of machines that cover $X$ (i.e., halt on all points of $X$) forms an open set in the machine space $\Sigma^{\Sigma^G}$.
4. Algorithmic Verification: The paper proves that Algorithm 1 correctly semi-decides universal quantification for any compact locale, effectively turning the abstract definition of compactness (finite subcovers) into a concrete computational procedure.

5. Significance

• Bridging Logic and Topology: The paper successfully reconciles the philosophical intuition that "verifiable properties should be verifiable" with the mathematical fact that exponentials often fail to exist. It does so by introducing "machines" as the concrete carriers of verification, distinguishing them from the abstract properties.
• Generalization of Escardó's Work: It lifts the concept of universal quantification from the specific context of programming language semantics and data types (Kleene-Kreisel spaces) to the general setting of locales and pointfree topology.
• Constructive Insight: The approach is constructive (valid in intuitionistic logic), providing explicit algorithms and structural insights rather than just existence proofs.
• New Perspective on Compactness: It reframes compactness not just as a topological property, but as the existence of a uniform semi-decision procedure for universal quantification, mediated through the structure of machine space.

In summary, the paper introduces Machine Space as a robust substitute for the non-existent space of opens in non-locally-compact settings, using it to resolve foundational questions about exponentials and to provide a unified, topological algorithm for universal quantification over compact spaces.