Categorifying computable reducibilities

TL;DR

This paper develops categorical frameworks for various computability reducibilities using Lawvere doctrines, revealing their structural similarities and enabling formal comparisons among them.

Contribution

It introduces categorical formulations of Turing, Medvedev, Muchnik, and Weihrauch reducibilities, unifying them through the concept of completions of quantifiers in doctrines.

Findings

All reducibilities are instances of quantifier completions in doctrines.

Weihrauch reducibility can be formally compared with the dialectica doctrine.

Categorical formulations provide new insights into the structure of computability reducibilities.

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.