Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

A topos for extended Weihrauch degrees

Samuele Maschio, Davide Trotta

TL;DR

The paper builds a full categorical framework for extended Weihrauch reducibility by formulating a tripos that captures instance reductions and establishing an isomorphism to an extended Weihrauch tripos. Through the tripos-to-topos construction, it yields a topos $\mathsf{EW}[\mathbb{A},\mathbb{A}']$ that serves as a universe for these degrees and relates it to realizability via a $j$-sheaf representation of the relative realizability topos. This work connects reducibility notions in computation with realizability toposes, providing an exact-completion perspective and paving the way for internal logical analysis of extended Weihrauch degrees. It also demonstrates the deep interplay between category theory, logic, and computability, suggesting further exploration of the internal logic and connections to containers and related frameworks.

Abstract

Weihrauch reducibility is a notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multivalued function. It complements the analysis of mathematical theorems done in reverse mathematics, as multi-valued functions on represented spaces can be considered as realizers of theorems in a natural way. Despite the rich literature and the relevance of the applications of category theory in logic and realizability, actually there are just a few works starting to study the Weihrauch reducibility from a categorical point of view. The main purpose of this work is to provide a full categorical account to the notion of extended Weihrauch reducibility introduced by A. Bauer, which generalizes the original notion of Weihrauch reducibility. In particular, we present a tripos and a topos for extended Weihrauch degrees. We start by defining a new tripos, abstracting the notion of extended Weihrauch degrees, and then we apply the tripos-to-topos construction to obtain the desired topos. Then we show that the Kleene-Vesley topos is a topos of $j$-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

A topos for extended Weihrauch degrees

TL;DR

The paper builds a full categorical framework for extended Weihrauch reducibility by formulating a tripos that captures instance reductions and establishing an isomorphism to an extended Weihrauch tripos. Through the tripos-to-topos construction, it yields a topos that serves as a universe for these degrees and relates it to realizability via a -sheaf representation of the relative realizability topos. This work connects reducibility notions in computation with realizability toposes, providing an exact-completion perspective and paving the way for internal logical analysis of extended Weihrauch degrees. It also demonstrates the deep interplay between category theory, logic, and computability, suggesting further exploration of the internal logic and connections to containers and related frameworks.

Abstract

Weihrauch reducibility is a notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multivalued function. It complements the analysis of mathematical theorems done in reverse mathematics, as multi-valued functions on represented spaces can be considered as realizers of theorems in a natural way. Despite the rich literature and the relevance of the applications of category theory in logic and realizability, actually there are just a few works starting to study the Weihrauch reducibility from a categorical point of view. The main purpose of this work is to provide a full categorical account to the notion of extended Weihrauch reducibility introduced by A. Bauer, which generalizes the original notion of Weihrauch reducibility. In particular, we present a tripos and a topos for extended Weihrauch degrees. We start by defining a new tripos, abstracting the notion of extended Weihrauch degrees, and then we apply the tripos-to-topos construction to obtain the desired topos. Then we show that the Kleene-Vesley topos is a topos of -sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.
Paper Structure (13 sections, 16 theorems, 49 equations)

This paper contains 13 sections, 16 theorems, 49 equations.

Table of Contents

  1. Introduction
  2. Preliminaries
  3. Partial combinatory algebras
  4. Assemblies and partitioned assemblies
  5. Primary and existential doctrines
  6. Triposes
  7. The full existential completion
  8. Instance reducibility and extended Weihrauch degrees
  9. A tripos for instance reducibility
  10. A tripos for extended Weihrauch degrees
  11. A topos for extended Weihrauch degrees
  12. The tripos-to-topos
  13. The topos of extended Weihrauch degrees

Key Result

Theorem 2.31

No Environment Found The doctrine $P^{\exists} \colon \mathcal{C}^{\operatorname{ op}} \longrightarrow \mathsf{InfSl}$ is an existential doctrine.

Theorems & Definitions (69)

  • Definition 2.1: PAS
  • Definition 2.2: PCA
  • Definition 2.3: elementary sub-PCA
  • Example 2.4: Kleene’s first model
  • Example 2.5: Kleene’s second model
  • Definition 2.6: Assemblies and Partitioned assemblies
  • Definition 2.7: realizer for assemblies
  • Definition 2.8: Morphism of assemblies
  • Definition 2.9
  • Definition 2.10: primary doctrine
  • ...and 59 more