Weihrauch reducibility is a notion from type-2 computability that allows to compare the computational strength of problems, modelled as relations over Baire space. Much like in Reverse Mathematics, any Π¹₂ statement translates naturally to a Weihrauch problem. Unlike Reverse Mathematics, the notion of reducibility is resource-sensitive, i.e., a reduction from P to Q is allowed to use Q exactly once. The Weihrauch lattice also comes with a rich algebra of operators that allows for instance to talk about sequential or parallel composition of problems.

This rich structure is in fact not specific to Weihrauch complexity as problems and reductions (almost) correspond to a category of polynomial functors, which share many of the useful operators in Weihrauch complexity [3,4].

After introducing and motivating these notions, I will try to outline how one can do computer science to study the structure of the Weihrauch degrees. According to availability of time and appetite, I should discuss equational theories of the Weihrauch lattice and automata multi-attempts [2] simulations and/or the proposition-as-problems logic introduced by Maschio & Trotta [1], including work-in-progress regarding definability in this setting.

This talk will draw on joint works and extensive discussions with colleagues in Swansea (Eike Neumann, Arno Pauly, Ian Price and Manlio Valenti).

[1] https://arxiv.org/abs/2505.08697 A topos for extended Weihrauch degrees, Samuele Maschio, Davide Trotta

[2] https://arxiv.org/abs/2408.14999 The equational theory of the Weihrauch lattice with (iterated) composition

[3] https://arxiv.org/abs/2501.17250 Weihrauch problems as containers, with Ian Price

[4] https://arxiv.org/abs/2601.15420 Problems with fixpoints of polynomials of polynomial, with Ian Price