Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Machine Space I: Weak exponentials and quantification over compact spaces

Peter F. Faul, Graham Manuell

TL;DR

This paper makes a distinction between verifiable properties themselves and processes which carry out the verification procedure, while the latter are simply opens, while the former are simply opens, while the latter machines are called machines.

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 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.

Machine Space I: Weak exponentials and quantification over compact spaces

TL;DR

This paper makes a distinction between verifiable properties themselves and processes which carry out the verification procedure, while the latter are simply opens, while the former are simply opens, while the latter machines are called machines.

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 machines. Given a frame presentation we construct a space of machines whose points are given by formal combinations of basic machines corresponding to generators in . This comes equipped with an `evaluation' map making it a weak exponential with base and exponent . When it exists, the true exponential 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.
Paper Structure (12 sections, 9 theorems, 4 equations, 1 figure, 1 algorithm)

This paper contains 12 sections, 9 theorems, 4 equations, 1 figure, 1 algorithm.

Table of Contents

  1. Introduction
  2. Background
  3. Pointfree topology
  4. The Scott topology and exponentials
  5. Machine space
  6. Presentations and weak exponentials
  7. Philosophical Interlude
  8. Relationship between machine space and the space of opens
  9. Compactness and universal quantification
  10. An algorithm for universal quantification
  11. Topological consequences
  12. Link to domain-theoretic approaches

Key Result

Proposition 3.2

Let $X$ have presentation $\langle G \mid R\rangle$. The space $\Sigma^{\Sigma^G}$ together with the evaluation map $\widetilde{\mathrm{ev}}\colon \Sigma^{\Sigma^G} \times X \to \Sigma$ given by the composite $\Sigma^{\Sigma^G} \times X \hookrightarrow \Sigma^{\Sigma^G} \times \Sigma^G \xrightarrow{

Theorems & Definitions (41)

  • Example 1.1
  • Definition 2.1
  • Definition 2.2
  • Definition 2.3
  • Definition 2.4
  • Definition 2.5
  • Definition 2.6
  • Definition 2.7
  • Definition 3.1
  • Proposition 3.2
  • ...and 31 more