| Description | Executive summary: contribute to a cool theoretical computer science project by implementing some algorithms looking for counterexamples for a mathematical conjecture. Come talk to me if that sounds interesting (Arno, Eike and Manlio can also discuss this topic equally well)!
Weihrauch-reducibility is a tool of computable analysis that lets us quantify how non-computable certain problems, modelled as input-outpur relations, are. It is a refinement to Turing-reducibility.
In the computable analysis group in Swansea, there is a lot of activity around analyzing operators on Weihrauch problems such as parallel product of two problems (i.e. given a problem A and a problem B, define the problem A × B to be the problem that take pairs of input for A and B and outputs a pair giving solutions to both output) and similar operations ∨ (A ∨ B = solve either A or B) and ∧(A ∧ B = given inputs for both A and B, give an output for one of them).
In https://arxiv.org/abs/2403.13975 we have given a characterization of the reductions in terms of games/graphs that work generically for expressions containing × and ∧, as well as a list of axioms for them, but we have failed to show whether that axiomatization is complete or not in the pointed case. The goal of this project would be to try to find a pair of graphs for which there is a combinatorial reduction but no proofs via our proposed example. We have not been able to find these by hand, so writing a program might be necessary!
While I expect you might be able to write a program that builds terms that can combinatorially reduce to one another (although warning: the computational complexity of checking reducibility is pretty high, above NP-complete), writing a program that produce proofs might be trickier - for that, you might want to use a SMT solver or some similar tools (the theory in question contains only simple universal axioms, so you might get away with using tools that deal with simpler logic more efficiently than SMT solvers which are general-purpose).
That being said, we conjecture that the counter-example that appears in https://arxiv.org/abs/2004.12941 can be adapted to be a counter-example for completeness of our theory. Proving this would require doing a bit of math on our proof system to prove interpolation-like results. So an alternative, if you are more mathematically and proof-theory minded, would be to try to prove that.
If you somehow breeze through that, there is much more to explore around these combinatorial reductions by considering other operators on Weihrauch problem, such as composition; there the combinatorial criteria are linked to the existence of some kind of simulations between automata (see e.g. https://arxiv.org/abs/2408.14999). |
|---|