What would Dijkstra do? Proving the associativity of min
byorgey.wordpress.com
What would Dijkstra do? Proving the associativity of min
1–10 of 32 posts
Re: What would Dijkstra do? Proving the associativity of min
#2Similarly you can show that gcd and lcm are associative, once you know their universal properties (for gcd, being the one common divisor that every common divisor divides; for lcm, the corresponding dual property). Similarly the associativity (up to unique diagram-fitting isomorphism) of products (or even fibered products) in any category (when they exist).
The really high horse here is called "Yoneda embedding", but there is not much gained from going that high.
Re: What would Dijkstra do? Proving the associativity of min
#3I 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.
Re: What would Dijkstra do? Proving the associativity of min
#4> The book expected them to do a proof by cases, with some sort of case split on the order of a , b , and c . What they turned in was mostly pretty good, actually, but while grading it I became disgusted with the whole thing and thought there has to be a better way.
This is how it's done in the Idris standard library[1]:
total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r
minimumAssociative Z c r = Refl
minimumAssociative (S k) Z r = Refl
minimumAssociative (S k) (S j) Z = Refl
minimumAssociative (S k) (S j) (S i) = rewrite minimumAssociative k j i in Refl
Re: What would Dijkstra do? Proving the associativity of min
#5I 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.
To be fair, reals have nothing to do with this - the 'min' makes sense - and is associative - in any ordered set (even partially ordered, if you accept that it may be undefined for some pairs).
Re: What would Dijkstra do? Proving the associativity of min
#6> The book expected them to do a proof by cases, with some sort of case split on the order of a , b , and c . What they turned in was mostly pretty good, actually, but while grading it I became disgusted with the whole thing and thought there has to be a better way. This is how it's done in the Idris standard library[1]: total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r min…
This is also using induction on naturals, which doesn’t “port” to the reals, as the post asks.
Re: What would Dijkstra do? Proving the associativity of min
#7> The book expected them to do a proof by cases, with some sort of case split on the order of a , b , and c . What they turned in was mostly pretty good, actually, but while grading it I became disgusted with the whole thing and thought there has to be a better way. This is how it's done in the Idris standard library[1]: total minimumAssociative : (l,c,r : Nat) -> minimum l (minimum c r) = minimum (minimum l c) r min…
That's doing induction its arguments, which relies on them being naturals - it's not an approach that would generalise to reals.
Re: What would Dijkstra do? Proving the associativity of min
#8I 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.
To be fair, reals have nothing to do with this - the 'min' makes sense - and is associative - in any ordered set (even partially ordered, if you accept that it may be undefined for some pairs).
Absolutely. Just going off the language used in the post which is maybe tailored to Brent's student audience.
Re: What would Dijkstra do? Proving the associativity of min
#9The 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!
Re: What would Dijkstra do? Proving the associativity of min
#10This 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.