Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

What would Dijkstra do? Proving the associativity of min

byorgey.wordpress.com

Post reply on HN
Print view View original

21–30 of 32 posts

Re: What would Dijkstra do? Proving the associativity of min

#21

Post by thaumasiotes »

kmill wrote: post #9

The Dedekind cut formulation of the real numbers is that a real number is defined to be a nonempty "downwards closed" subset of rational numbers. Then the min operation corresponds to taking intersections, and taking intersections is associative. It's cool they figured something like this out from first principles. edit: oops, somehow didn't notice arnarbi already mentioned this!

The somewhat-standard definition of the naturals (0 = {}, 1 = {0}, 2 = {0, 1}, 3 = {0, 1, 2}, ...) also maps min to set intersection. GCD, which someone else mentions in another comment, is very straightforwardly a set intersection problem.

The intuition here is that an operation throws away information that isn't relevant while keeping the relevant information. If you can't lose relevant information, you can't fail to be associative. Probably all such operations can be straightforwardly mapped to set intersection or set union. (Under the definition of the naturals given above, note that set union gives you the max operator.)

Re: What would Dijkstra do? Proving the associativity of min

#22

Post by thaumasiotes »

kmill wrote: post #9

The Dedekind cut formulation of the real numbers is that a real number is defined to be a nonempty "downwards closed" subset of rational numbers. Then the min operation corresponds to taking intersections, and taking intersections is associative. It's cool they figured something like this out from first principles. edit: oops, somehow didn't notice arnarbi already mentioned this!

> The Dedekind cut formulation of the real numbers is that a real number is defined to be a nonempty "downwards closed" subset of rational numbers. Then the min operation corresponds to taking intersections

They didn't figure that out exactly. They figured out something much less significant: that a real number is defined by a nonempty upwards closed subset of real numbers:

>> My second epiphany was that equality of real numbers can also be characterized by having the same “downsets”, i.e. two real numbers are equal if and only if the sets of real numbers less than or equal to them are the same.

In other words, we choose to represent the real number r as the closed interval (-∞, r].

The point of Dedekind cuts is that you can define real numbers without using real numbers in the definition.

They do then set up min as set intersection as suggested by the interval definition.

Writing out the choice of real number representation makes it clear that we could also represent a real number as the interval [r, ∞), in which case minimum would be set union rather than set intersection. It doesn't really matter whether we use a closed or open interval.

Re: What would Dijkstra do? Proving the associativity of min

#23

Post by Tomminn »

I find proofs like this weird.

I can never quite understand what it means to say anything beyond:

"whichever of {a,b,c} is the smallest is the answer to both sides".

Who is this audience for which all this extra ink carries extra meaning? What additional insight can you have possibly communicated to them?

Re: What would Dijkstra do? Proving the associativity of min

#24

Post by joppy »

arnarbi wrote: post #3

I think a shorter way to write that is to first note the downset representation of reals. Then your definition of min is just the set intersection and there's nothing more to show.

So you define max([-∞, a]) =a, and define min(a, b) as max([-∞, a] ∩ [-∞, b])? Isn't this just shifting the problem elsewhere? For instance now you need to prove that the intersection of sets is of the form [-∞, a] or [-∞, b], which is fairly intuitive, but not more intuitive than the usual definition of min.

Re: What would Dijkstra do? Proving the associativity of min

#25

Post by raverbashing »

virtuous_signal wrote: post #15
im3w1l wrote: post #13

Here's the solution I thought of, which is pretty similar. Start with the case definition of min. Notice that min(a,b) Let d = min(a,min(b,c)) and e = min(min(a,b),c) Then d Same goes for e. Since e is in {a,b,c} and d <= a, d <= b, d <= c, it must follow that d <= e. And by symmetry e <= d. So d=e.

Similar? In my opinion this is much faster, easier, and less burdened by notation.

Hence mathematicians will "hate it" and replace it with something more complicated and less clear

This proof works for any totally ordered set (hence a <= operation is defined on it)

Re: What would Dijkstra do? Proving the associativity of min

#26

Post by Josh04 »

virtuous_signal wrote: post #15
im3w1l wrote: post #13

Here's the solution I thought of, which is pretty similar. Start with the case definition of min. Notice that min(a,b) Let d = min(a,min(b,c)) and e = min(min(a,b),c) Then d Same goes for e. Since e is in {a,b,c} and d <= a, d <= b, d <= c, it must follow that d <= e. And by symmetry e <= d. So d=e.

Similar? In my opinion this is much faster, easier, and less burdened by notation.

With no offense intended to the poster, the inferences are a little sloppy by mathematical standards and most of the hard work is done by introducing ("noticing") the set notation to the definition of min.

Re: What would Dijkstra do? Proving the associativity of min

#27

Post by tinus_hn »

Tomminn wrote: post #23

I find proofs like this weird. I can never quite understand what it means to say anything beyond: "whichever of {a,b,c} is the smallest is the answer to both sides". Who is this audience for which all this extra ink carries extra meaning? What additional insight can you have possibly communicated to them?

It is a course exercise. The additional insight is that there are multiple ways to solve this exercise, one that most students would chose and another, explored in the article.

Re: What would Dijkstra do? Proving the associativity of min

#28

Post by bobbylarrybobby »

lidHanteyk wrote: post #12
Animats wrote: post #10

This is the definition that leads to the ugly proof by cases. Right there is the problem. There's nothing wrong with proof by cases. People suck at it, but machines do it just fine. I ran into this years ago in the early days of program proving. The kind of proofs that mathematicians like are not the kind you really want to use to get work done by machine.

"Programmers are not to be measured by their ingenuity and their logic but by the completeness of their case analysis." ~ Perlis I personally pride myself on my ability to analyze situations by cases, and to grind through normally-opaque walls to find proofs, but we should always keep in mind that it is the hardest way. It's like fishing for algorithms.

Presumably, ingenuity and logic can lead one to a simplified case analysis (more cases covered by fewer separate conditions), which allows one to do a complete case analysis with less effort.

Re: What would Dijkstra do? Proving the associativity of min

#29

Post by im3w1l »

Josh04 wrote: post #26
virtuous_signal wrote: post #15

Earlier quoted context omitted.

Similar? In my opinion this is much faster, easier, and less burdened by notation.

With no offense intended to the poster, the inferences are a little sloppy by mathematical standards and most of the hard work is done by introducing ("noticing") the set notation to the definition of min.

I agree. It's more of a sketch than a proof which is why it's so short.

Re: What would Dijkstra do? Proving the associativity of min

#30

Post by JadeNB »

lmm wrote: post #14
JadeNB wrote: post #11

Earlier quoted context omitted.

I think that's necessary, since the order on the full set of reals isn't constructively decideable, so min isn't even a total function there.

Almost all reals are not computable, but as far as I know min is total - given two reals (represented as e.g. lazy infinite decimal sequences), computing their min is trivial.

Yes, I'm wrong. I was thinking of the naïve implementation

     if ( a
which requires being able to decide order, but, as child comments point out, that's not necessary.
Post reply on HN