Confused why the article author believes this is a surprise. The foundations of mathematics and computer science are basically the same subject (imho) and dualities between representations in both fields have been known for decades.
The notion of algorithms and computer science were invented to discuss the behavior of infinite sequences: examining if there’s descriptions of real numbers. This was extended by connecting complicated infinite structures like the hyperreals with decisions theory problems.
That descriptions of other infinite sets also corresponds to some kind of algorithm seems like a natural progression.
That it happens to be network theory algorithms rather than (eg) decision theory algorithms is worth noting — but hardly surprising. Particularly because the sets examined arose from graph problems, ie, a network.
To me this is quite surprising. Distributed systems were not designed to solve measure theory problems.
an object doing something that it wasn’t designed for seems to me to be the definition of “surprising”
That you can express the constraints of network colorings (ie, the measure theory problem) as network algorithms strikes me as a “well duh” claim — at least if you take that Curry-Howard stuff seriously.
Nothing in the result in the article talks about types, and even if it could be, it’s not clear that the CH isomorphism would be a good lens to do so.
I’m not “sprinkling magic powder”, but using the very core of the correspondence:
A proof that your network has some property is an algorithm to construct an instance of appropriate type from your network.
In this case, we’re using algorithms originally designed for protocols in CS to construct a witness of a property about a graph coloring. In the article, it details exactly his realization this was true — during a lecture, seeing the types of things constructed by these algorithms corresponding to the types of objects he works with.
The networks on the measure theory side and on the algorithmic side are not the same. They are not even the same cardinality. One has uncountably many nodes, the other has countably many nodes.
The correspondence outlined is also extremely subtle. Measurable colorings are related to speed of consensus.
You make it sound like this is a result of the type: "To prove that a coloring exists, I prove that an algorithm that colors the network exists." Which it is not, as far as I understand.
It seems to me you are mischaracterizing CH here as well:
> A proof that your network has some property is an algorithm to construct an instance of appropriate type from your object.
A proof that a certain network has some property is an algorithm that constructs an instance of an appropriate type that expresses this fact from the axioms you're working from.
This is the crux of the proof, as I understand it: to classify network coloring measurability, I classify algorithms that color the network.
Which I can do because there’s a correspondence between network colorings (in graph theory) and algorithms that color networks (in CS). Which I’m arguing is an instance of CH: they’re equivalent things, so classifying either is classifying both.
> They are not even the same cardinality. One has uncountably many nodes, the other has countably many nodes. […] Measurable colorings are related to speed of consensus.
Yes — this is why the work is technically impressive, because proving the intuition from above works when extending to the infinite case is non-trivial. But that doesn’t change that fundamentally we’re porting an algorithm. I’m impressed by the approach to dealing with labels in the uncountable context which allows the technique to work for these objects — but that doesn’t mean I’m surprised such a thing could work. Or that work on network colorings (in CS) turned out to have techniques useful for network colorings (in math).
> It seems to me you are mischaracterizing CH
You then go on to make some quibble about my phrasing that, contrary to your claim about mischaracterizing, doesn’t conflict with what you wrote.
Edit: removing last paragraph; didn’t realize new author.
What CH does not allow you to do is turn an existence proof (a coloring exists) into a constructive proof (a means to actually construct such a coloring). In fact, this is generally not true. Mathematical statements correspond to computations in a much more subtle and indirect way than that.
Honestly, I get the impression that you have a very superficial understanding of the topics at hand, but I am far from an expert myself. If you really know a way to see this as an instance of CH I would be very intrigued to learn about it.
From my vantage, there’s two strains that make such discoveries unsurprising:
- Curry-Howard generally seems to map “nice” to “nice”, at least in the cases I’ve dealt with;
- modern mathematics is all about finding such congruences between domains (eg, category theory) and we seem to find ways to embed theories all over; to the point where my personal hunch is that we’re vastly underestimating the “elephant problem”, in which having started exploring the elephant in different places, we struggle to see we’re exploring the same object.
Neither of those is a technical argument, but I hope it helps understand why I’d be coming to the question from a different perspective and hence different level of surprise.
It makes perfect sense to me.