Comment by zmgsabst
3 days ago
They’re literally exploring the same object: properties of networks.
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.
Curry-Howard is not some magic powder you can just sprinkle around to justify claims. The isomorphism provides a specific lens to move between mathematics and computation. It says roughly that types and logical propositions can be seen equivalently.
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.
Curry-Howard literally says that a proof your object has a property is equivalent to an algorithm which constructs a corresponding type.
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.
Do you have any actual evidence that this result can be viewed as an instance of CH?
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.
2 replies →