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

11–20 of 32 posts

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

#11

Post by JadeNB »

lmm wrote: post #7
nickdrozd wrote: post #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 min…

That's doing induction its arguments, which relies on them being naturals - it's not an approach that would generalise to reals.

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.

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

#12

Post by lidHanteyk »

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.

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

#13

Post by im3w1l »

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.

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

#14

Post by lmm »

JadeNB wrote: post #11
lmm wrote: post #7

Earlier quoted context omitted.

That's doing induction its arguments, which relies on them being naturals - it's not an approach that would generalise to reals.

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.

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

#15

Post by virtuous_signal »

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.

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

#16

Post by leni536 »

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.

Unless when they happen to be equal. Then it never halts.

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

#17

Post by atq2119 »

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.

It's certainly a nice solution, but OP's solution has the nice property of working directly on a universality definition, which makes the argument more general. For example, the universality argument also works for the infimum and gcd operations.

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

#18

Post by Skeime »

leni536 wrote: post #16
lmm wrote: post #14

Earlier quoted context omitted.

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.

Unless when they happen to be equal. Then it never halts.

Actually, computing the minimum should work: If they are equal you can still lazily produce the digits of the decimal expansion. What you can’t do in this case is to tell whether this minimum is equal to the first or the second number.

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

#19

Post by [deleted] »

atq2119 wrote: post #17
virtuous_signal wrote: post #15

Earlier quoted context omitted.

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

It's certainly a nice solution, but OP's solution has the nice property of working directly on a universality definition, which makes the argument more general. For example, the universality argument also works for the infimum and gcd operations.

[deleted]

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

#20

Post by contravariant »

generationP wrote: post #2

Similarly 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…

You don't really need to bring the Yoneda embedding into it. They're all just partial orders (for the gcd and lcm use the order defined by divisability), which can easily be shown to be categories with at most a single function between objects. After that it's just expanding definitions.
Post reply on HN