Why does Weihrauch reducibility make use of multi-functions?

Question

This is probably a kinda dumb question, but why is Weihrauch reducibility defined in terms of multi-functions (i.e. why isn't it just the degree structure of regular functions under that reducibility)? I feel like it should be a basic fact but I haven't seen it explained in the paper's I've looked at.

Indeed, when I look at Weihrauch's "The Degrees of Discontinuity of some Translators between Representations of the Real Numbers" I don't see (admittedly I skimmed) any use of multi-functions and it doesn't obviously seem central to the motivation.

Is it just that the notion can be so generalized so it was? Or is there some more technical reason or desired application which needs the multi-functions?

Answer 1

A core motivation for the study of Weihrauch reducibility is to investigate the computational content of theorems of the form: $$\forall x \in \mathbf{X} (\neg \neg D(x) \Rightarrow \exists y \in \mathbf{Y} \ P(x,y))$$

These naturally give rise to a multivalued partial function $P : \subseteq \mathbf{X} \rightrightarrows \mathbf{Y}$ which is defined on $\{x \in \mathbf{X} \mid D(x)\}$ and maps $x \in \mathbf{X}$ with $D(x)$ to some $y \in \mathbf{Y}$ such that $P(x,y)$. Only in the rare case where there are naturally unique witnesses would we get a function here.

Some typical examples are the intermediate value theorem yielding a map $\mathrm{IVT} : \subseteq \mathcal{C}([0,1],\mathbb{R}) \rightrightarrows [0,1]$ which is defined on the continuous functions $f$ with $f(0)f(1) < 0$, and returns some zero; or Brouwer's Fixed Point theorem with $\mathrm{BFT}_n : \mathcal{C}([0,1]^n,[0,1]^n) \rightrightarrows [0,1]^n$ mapping a continuous function to some fixed point, or Weak Koenigs Lemma which maps binary trees which happen to be infinite to some infinite path through them.

Not only are all these problems of interest naturally multivalued, but we even know that their Weihrauch degrees do not contain any singlevalued representatives (even more, eg if $f : \subseteq \mathbb{N}^\mathbb{N} \to \mathbb{N}^\mathbb{N}$ is a function with $f \leq_{\mathrm{W}} \mathrm{BFT}_n$, then $f$ is already computable).

Terminology has changed a lot since Weihrauch's preprints. The reducibility he studies formally compares sets of singlevalued functions, but the results translate rather directly into the modern framework. The translations between representations of the reals he studied can be phrased as multivalued functions on Cantor space which map a name from one representation to some name in the other representation denoting the same number. Of course, we can alternatively view them as identity maps between represented spaces, in which case they'd be singlevalued.

Above is what I would consider the by far most important reason why we study multivalued functions. However, I'd also argue that this gives us a nicer structure. The Weihrauch degrees form a lattice, and the meet-operation does not preserve being singlevalued. For $f_i : \mathbf{X}_i \rightrightarrows \mathbf{Y}_i$, we have that their meet $f_1 \sqcap f_2 : (\mathbf{X}_1 \times \mathbf{X}_2) \rightrightarrows (\mathbf{Y}_1 + \mathbf{Y}_2)$ has as valid solutions on the instance $(x_0,x_1)$ all $(i,y_i)$ with $y_i \in f_i(x_i)$. So even if $f_1,f_2$ are both singlevalued, $f_1 \sqcap f_2$ would have two valid solutions to each instance.

Answer 2

In a nutshell, the reason one uses 'multi-functions', i.e. mappings that do not satisfy the axiom of function extensionality, is that otherwise things would be fairly trivial, as shown essentially by Kohlenbach, building on work by Grilliot.

In more detail, there is a technical result called Grilliot's trick (see [1]) that amounts to

from a discontinuous function on the reals or Baire space, one can compute Kleene's quantifier $\exists^2$, i.e. the Turing jump functional.

Kohlenbach showed that this trick can be formalised in rather weak systems, needing only a small fragment of Goedel's T ([2]). Thus, $\exists^2$ can be computed (via a term in Goedel's T only using primitive recursion for type 1 objects) from any functional $\Phi^{1\rightarrow 1}$ that on input any infinite binary tree $T$, outputs a path $\Phi(T)$ in $T$. The axiom of function extensionality is essential here, as shown in [3].

A similar result holds for any functional that witnesses the intermediate value theorem, the extreme value theorem, etc. In this way, requiring the functionals at hand to be extensional, one obtains many equivalences involving $\exists^2$. This is not the fine-grained picture people are looking for and hence one works with 'multi-functions' for which the output can depend on the representation of the input.

[1] T. J. Grilliot. On effectively discontinuous type-2 objects. J. Symbolic Logic, 36:245–248, 1971.

[2] U. Kohlenbach, Higher order Reverse Mathematics, RM 2001.

[3] U. Kohlenbach, On uniform weak Koenig's lemma.