一句话：用 Lawvere 学说范畴化图灵、Medvedev、Muchnik、Weihrauch 归约，并统一为量词完备化。
本文研究可计算性理论中 Turing、Medvedev、Muchnik 与 Weihrauch 归约的范畴论表述。作者使用 Lawvere 学说，将前三类归约自然呈现为可实现性学说的对偶化，而对 Weihrauch 归约及其在表示空间与多表示空间上的扩展则进行单独处理。核心发现是：这些源于可计算性概念的学说都可被证明为学说量词完备化的实例，与可实现性学说的情形类似。作为推论，作者得以形式化地比较 Weihrauch 归约与由表示图灵度的学说所构造的 dialectica 学说。
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.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{TrottaVP25,
title = {Categorifying computable reducibilities},
author = {Davide Trotta and Manlio Valenti and Valeria de Paiva},
journal = {Logical Methods in Computer Science},
volume = {Volume 21, Issue 1},
year = {2025},
doi = {10.46298/lmcs-21(1:15)2025}
}