Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

Categorifying computable reducibilities

Davide Trotta, Manlio Valenti, Valeria de Paiva

TL;DR

This work develops a unified categorical framework for computability-theoretic reducibilities by recasting Turing, Medvedev, Muchnik, and Weihrauch reductions as Lawvere doctrines and their quantifier completions. Medvedev and Muchnik reducibilities arise as universal completions of corresponding Turing-type doctrines, while Weihrauch reducibility corresponds to a pure existential completion, with a careful shift to base categories (e.g., $ extsf{Mod}_{ extsf{p}}( ext{A}, ext{A}')$) to faithfully model forward functionals. The authors extend these ideas to representations (assemblies/modest sets) and to stronger variants (strong/extended Weihrauch), showing isomorphisms between the resulting doctrines and their existential/universal completions. They also connect the Dialectica construction with these doctrinal completions, revealing deep structural parallels between logical dialectica interpretations and computability notions. The framework paves the way for cross-pollination between computability theory and categorical logic, suggesting further exploration via tripos-to-topos constructions and algebraic study of these doctrines.

Abstract

This paper presents categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities in Computability Theory, utilizing Lawvere doctrines. While the first notions lend themselves to a smooth categorical presentation, essentially dualizing the traditional idea of realizability doctrines, Weihrauch reducibility and its extensions to represented and multi-represented spaces require a separate investigation. Our abstract analysis of these concepts highlights a shared characteristic among all these reducibilities. Specifically, we demonstrate that all these doctrines stemming from computability concepts can be proven to be instances of completions of quantifiers for doctrines, analogous to what occurs for doctrines for realizability. As a corollary of these results, we will be able to formally compare Weihrauch reducibility with the dialectica doctrine constructed from a doctrine representing Turing degrees.

Categorifying computable reducibilities

TL;DR

This work develops a unified categorical framework for computability-theoretic reducibilities by recasting Turing, Medvedev, Muchnik, and Weihrauch reductions as Lawvere doctrines and their quantifier completions. Medvedev and Muchnik reducibilities arise as universal completions of corresponding Turing-type doctrines, while Weihrauch reducibility corresponds to a pure existential completion, with a careful shift to base categories (e.g., ) to faithfully model forward functionals. The authors extend these ideas to representations (assemblies/modest sets) and to stronger variants (strong/extended Weihrauch), showing isomorphisms between the resulting doctrines and their existential/universal completions. They also connect the Dialectica construction with these doctrinal completions, revealing deep structural parallels between logical dialectica interpretations and computability notions. The framework paves the way for cross-pollination between computability theory and categorical logic, suggesting further exploration via tripos-to-topos constructions and algebraic study of these doctrines.

Abstract

This paper presents categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities in Computability Theory, utilizing Lawvere doctrines. While the first notions lend themselves to a smooth categorical presentation, essentially dualizing the traditional idea of realizability doctrines, Weihrauch reducibility and its extensions to represented and multi-represented spaces require a separate investigation. Our abstract analysis of these concepts highlights a shared characteristic among all these reducibilities. Specifically, we demonstrate that all these doctrines stemming from computability concepts can be proven to be instances of completions of quantifiers for doctrines, analogous to what occurs for doctrines for realizability. As a corollary of these results, we will be able to formally compare Weihrauch reducibility with the dialectica doctrine constructed from a doctrine representing Turing degrees.
Paper Structure (13 sections, 25 theorems, 71 equations)

This paper contains 13 sections, 25 theorems, 71 equations.

Table of Contents

  1. Introduction
  2. Partial combinatory algebras
  3. Categorical Doctrines
  4. Medvedev doctrines
  5. Muchnik Doctrines
  6. Weihrauch Doctrines
  7. Strong Weihrauch Doctrines
  8. Generalizations of Weihrauch reducibility
  9. Assemblies and Modest sets
  10. Realizer-based Weihrauch reducibility
  11. Extended Weihrauch reducibility
  12. Some remarks
  13. Conclusions

Key Result

Theorem 3.6

The doctrine $P^{\exists_{\mathcal{D}}}$ is $\mathcal{D}$-existential. Moreover, for every doctrine $P$ we have a canonical inclusion $\eta_P^{\exists_\mathcal{D}} \colon P \to P^{\exists_{\mathcal{D}}}$ such that, for every morphism of doctrines $\mathfrak{L} \colon P \to R$, where $R$ is $\mathc

Theorems & Definitions (101)

  • 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
  • Remark 2.6
  • Definition 3.1: doctrine
  • Definition 3.2: morphism of doctrines
  • Example 3.3
  • Example 3.4
  • ...and 91 more