Weihrauch Reducibility as a Lens
A short while ago, we had CCA 2024 at Swansea, which I attended mostly because it was local and my supervisor was giving a talk. The first day had a session dedicated to the topic of Weihrauch reducibility, during which it occurred to me that the definition of Weihrauch reducibility looked suspiciously similar to the definition of a dependent lens and that some of the operators on Weihrauch degrees should just be known constructions on polynomials. She agreed, telling me that Weihrauch problems are the polynomials in the category \(\PasmFull\) of partitioned assemblies over the PCA \(\Ktwo\) filtered by \(\Ktworec\).
I've written this attempt to answer the question: “What the hell does that even mean?”.
Warning, to read this post you must be over 18 years old or accompanied by a trained category theorist.
What is Weihrauch Reducibility?
Reducibility is a fundamental concept in computability and complexity theory. A problem \(P\) is reducible to a problem \(Q\) if a solution to \(Q\) can be used to solve \(P\). In a fire, a practical minded engineer might grab a fire extinguisher and put it out; a computer scientist might instead give the fire extinguisher to the engineer, thus reducing the problem to one with a known solution. A simple type of reduction is that \(P\) is reducible to \(Q\) if there is an algorithm that decides \(P\) that may call out to \(Q\) as a subroutine. Computer scientists have refined this reduction to allow only polynomial many calls to \(Q\), or even a single call to \(Q\). Today we are interested in the following definitions:
A represented space is a pair \((X, \delta)\) of a set \(X\) and a surjective partial function \(\delta_X \partialDefine \baire \to X\).
Let \(X\), \(Y\), \(Z\), \(W\) be represented spaces and let \(f \partialDefine X \multiTo Y\) , \(g \partialDefine Z \multiTo W\) be partial multi-valued functions. Then \(f\) is Weihrauch reducible to \(g\), if there are computable partial functions \(\Phi, \Psi \partialDefine \baire \to \baire\) such that for all \(p\) with \(\delta_X(p) \in \dom(f)\), \(\delta_Z(\Phi(p)) \in \dom(g)\) and for all \(q\) with \(\delta_W(q) \in g(\delta_Z(\Phi(p)))\), \(\delta_Y(\Psi(p,q)) \in f(\delta_X(p))\).
The upshot of the definition of Weihrauch reducible is that you have a “forward map” \(\Phi\) that converts inputs for \(f\) to inputs for \(g\), you solve your problem \(g\), then convert your output of \(g\) to an output of \(f\) using a “backward map” \(\Psi\). When using the backward map, you also get to use the original input. This is summarised in the diagram below.
If you’ve seen lenses or other bidirectional mathematical structures, you get excited when you see things like this. However, as usual with computer science, there is a bunch of plumbing required to make everything fit, starting with a trip into realisability.
What is a PCA?
I will not be giving an in-depth treatment of Categorical Realisability, but for an introduction to the topic, you can read Tom de Jong's notes from a course that I had the pleasure of attending at MGS this year.
A PCA, or Partial Combinatory Algebra if you're not into the whole brevity thing, is a set \(A\) of “combinators” and a partial operator called “application”, \(\cdot \partialDefine A \times A \to A\), plus two special combinators called \(S\) and \(K\) satisfying a few axioms. We will not dwell on this, because we have a lot to get through, but these \(S\) and \(K\) are the combinators you would get from a process called bracket abstraction in the untyped lambda calculus. They are “combinatorially complete” which means any term built out of application, variables, and elements of \(A\) can be expressed solely through application and \(K\) and \(S\).
There are lots of examples of PCAs, from the trivial \(\left\{\star\right\}\) to the not-so-trivial untyped lambda calculus. We will skip Kleene's first model to his second model \(\Ktwo\).
What is Kleene's Second Model?
Kleene's Second model is the PCA that corresponds to Type 2 Computability, which is the setting for much of Computable Analysis in general and Weihrauch Reducibility in particular. So, what is type 2 computability?
A partial function \(f \partialDefine \baire \to \baire\) is type 2 computable if there is a Turing machine \(M\) that given \(x \in \dom(f)\) on its input tape, eventually writes all of \(f(x)\) to its (write only) output tape, and \(M\) diverges otherwise.
There are a few things to notice. First, we will usually view these functions \(\alpha \in \baire\) as sequences of natural numbers. Second, we are taking the whole space of functions \(\baire\) as our input, which means that some of our inputs are not computable; this is intentional. Finally, a consequence of this definition is that our function is continuous, in that \(f(n)\) will be written to the output tape after finite time after inspecting only a finite prefix of the input.
To form a PCA, we want to take \(\baire\) as our set of objects and define a multiplication map. It's a little fiddly, e.g., see section 1.4.3 of van Oosten's book, but I will provide a short explanation based on a nice answer on mathoverflow.
Fix a function \(\alpha: \baire \to \baire\). We will instead view this as a function \(\alpha: \baire \times \nat \to \maybe \nat\), by uncurrying and fixing an isomorphism \(N \iso N + {\bot}\).
The first step is to define a partial map \(F_\alpha \partialDefine \baire \to \maybe \nat\) by repeatedly running \(\alpha(\beta_0, \dots, \beta_n)\) on an input sequence \(\beta \in \baire\), increasing \(n\) each time, until we get a non-\(\none\) answer \(\just k\). If this happens, return it; if the loop never terminates or \(\alpha\) diverges on some input, return \(\none\). That is, we keep asking for more of \(\beta\) until we have enough for \(\alpha\) to compute the answer. It turns out that every continuous partial function \(\baire \to \nat\) is equal to such an \(F_\alpha\) for some \(\alpha\).
Now we can define multiplication by \((\alpha \cdot \beta)(n) = F_\alpha(n, \beta)\), provided the right side is defined for all \(n\).
There is a (non-runnable) Haskell pseudo-implementation provided below for the people who prefer code to prose.