What would Dijkstra do? Proving the associativity of min(byorgey.wordpress.com) |
What would Dijkstra do? Proving the associativity of min(byorgey.wordpress.com) |
Start with the case definition of min.
Notice that min(a,b) <= a, min(a,b) <= b and min(a,b) in {a,b}
Let d = min(a,min(b,c)) and e = min(min(a,b),c)
Then d <= a, d <= b, d <= c and d in {a,b,c}
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.
This proof works for any totally ordered set (hence a <= operation is defined on it)
It's cool they figured something like this out from first principles.
edit: oops, somehow didn't notice arnarbi already mentioned this!
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.
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.)
The really high horse here is called "Yoneda embedding", but there is not much gained from going that high.
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.
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.
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
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?
I've been thinking about this and I don't see how the argument can possibly work for the infimum operation. The problem is that infimum is necessarily a unary operation -- it doesn't make any sense to consider it to have multiple arguments.
Consider the open interval (1,2). The infimum is 1. But 1 is not contained in the interval. And because 1 is not contained within the interval, _if_ infimum were a binary operation, we could not apply it to the interval and get 1. Binary infimum is the same operation as binary min, and while the infimum of (1,2) is 1, the minimum value of (1,2) does not exist.
We can actually use this to do a much more direct proof of the associativity of binary min: binary min is the same thing as unary min (min as applied to a single set of arguments rather than two scalar arguments), and unary min cannot fail to be associative because it has only one argument. Repeated binary mins do nothing more than apply unary min to the set of individual arguments.
if ( a < b ) then { return b } else { return a }