Abstract

Weihrauch reducibility [2] is a key notion of reducibility between computational problems that is useful to calibrate the uniform computational strength of a multi-valued function. Such reducibility provides a framework where one can formalize questions such as “which theorems can be transformed continuously or computably into another?”

The main purpose of this talk is to provide a full categorical account of a generalization of such a notion introduced by A. Bauer called extended Weihrauch reducibility [1]. In particular, we present a tripos [3] and a topos for extended Weihrauch degrees. Then we employ the free constructions and tools developed in [4] to provide a formal connection with realizability, showing that the effective topos is a topos of j-sheaves for a certain Lawvere-Tierney topology over the topos of extended Weihrauch degrees.

This talk is based on joint work with S. Maschio.

[1] Bauer, Andrej, Instance reducibility and Weihrauch degrees, Logical Methods in Computer Science 18 (2022), no. 3, 20:1–20:18
[2] Brattka, Vasco and Gherardi, Guido, Weihrauch degrees, omniscience principles and weak computability, The Journal of Symbolic Logic 76 (2011), no. 1, 143–176
[3] Pitts, A. M., Tripos theory in retrospect, Mathematical Structures in Computer Science 10 (2000), no. 3, 283–306
[4] Maietti, M.E. and Trotta, D., A characterization of generalized existential completions, Annals of Pure and Applied Logic 174 (2023), no. 4, Paper No. 103234, 37