Return to Answer

(Discrete BROUWER) Given $\epsilon$ and a function $f$ that takes coordinates in $[0,1]^2$ and produces coordinates in $[0,1]^2$, output some coordinate $(x,y)$ such that $\|(x,y) - f(x,y)\| \leq \epsilon$.

 

(SPERNER) Given an integer $n$ and a function $f$ that takes integers $(a,b)$ such that $a+b = n$ (that is, points on a triangulation) and produces a color {red,green,blue} and satisfying the usual Sperner coloring constraints, output a set of three points $((a_1,b_1),(a_2,b_2),(a_3,b_3))$ that (a) is a triangle and (b) is colored with three different colors.

(Discrete BROUWER) Given $\epsilon$ and a function $f$ that takes coordinates in $[0,1]^2$ and produces coordinates in $[0,1]^2$, output some coordinate $(x,y)$ such that $\|(x,y) - f(x,y)\| \leq \epsilon$.

(SPERNER) Given an integer $n$ and a function $f$ that takes integers $(a,b)$ such that $a+b = n$ (that is, points on a triangulation) and produces a color {red,green,blue} and satisfying the usual Sperner coloring constraints, output a set of three points $((a_1,b_1),(a_2,b_2),(a_3,b_3))$ that (a) is a triangle and (b) is colored with three different colors.

Logically, we can interpret the existence of a correct algorithm for $B$ as giving a proof of some theorem (e.g. Brouwer), and if $A$ reduces to $B$, then this immediately implies a proof of a theorem about $B$. (This is Curry-Howard.) When $A$ and $B$ can be reduced to each other, then a proof of either's associated theorem implies a proof of the other's. Sperner and Brouwer give a beautiful example, which I'll try to sketch as best I can.

Logically, we can interpret the existence of a correct algorithm for $B$ as giving a proof of some theorem (e.g. Brouwer) relating to $B$, and if $A$ reduces to $B$, then this immediately implies a proof of a theorem about $A$. (This is Curry-Howard.) When $A$ and $B$ can be reduced to each other, then a proof of either's associated theorem implies a proof of the other's. Sperner and Brouwer give a beautiful example, which I'll try to sketch as best I can.

P.S. A more subtle/further question is whether this really avoids the issue that all true statements imply each other. I don't think it does in a computability sense (?), but it does in a complexity sense: We can only allow polynomial-time reductions between problems. Now, if there is no way to solve either BROUWER or SPERNER in polynomial time, yet we can reduce either to the other in polynomial time, then they must be equivalent in some stronger sense: Our reduction cannot just solve the problem and give some trivial input (since our reduction only runs in polynomial time, which is not enough to solve the problem). So this black-box algorithm we are calling to solve the other problem must be doing the "heavy lifting" in some sense. (Another catch is that we don't know for sure whether BROUWER or SPERNER can be solved in polynomial time, but we mainly conjecture that they cannot.)