undefined | Better HN

0 pointsalmostgotcaught9mo ago0 comments

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect.

This is irrelevant.

> You can go further. Write the iterative form of a dynamic program (which uses array to store values, instead of hash, and uses a for loop instead of recursive memoized call) and prove it is computing the recursive maxDollars_spec.

Yes my original comment said exactly this.

The rest is irrelevant.

Reread my original comment again - or any of my follow-up comments - I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

0 comments

vjerancrnjak9mo ago

> I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

What is exhaustion for you? For everyone else in this thread, exhaustion means trying out all values and proving it works.

Exhaustive proof: pick 64-bits for a bit trick, run inefficient algorithm and get 64-bit outputs for all 2^64 bitsets, and then run the bit trick algorithm and exhaustively prove slow(n)==bittrick(n) for all n from 0 to 2^64-1.

Similar way you'd prove four color theorem.

Lean prover, in this case, does no such thing, it uses strong induction to prove correctness. Strong induction does not depend on the size of the input N at all, it depends on the size of the typed problem (which includes type annotations and how they relate).

Of course, proof that needs to deal with semantics of a hashmap is more complex than just dealing with lookup array, but it still proves that exponential recursive calculation can be done with a faster algorithm whose implementation is right there.

You have similar systems, where you can write a recursive quicksort and get average time complexity analysis for free. The system proves the average time complexity as O(n log n) directly from the implementation. (from memory, system would output C_n = 2 * (n + 1) * H_n - 4 * n, were C_n is the average number of comparisons of quicksort, H_n the harmonic number, average is calculated over all possible inputs of array of size N, it does not prove it exhaustively and finds the best approx for comparison counts, it proves it symbolically by computing directly on the representation of the average comparisons.)

thaumasiotes9mo ago

> For everyone else in this thread, exhaustion means trying out all values and proving it works.

My instinct was that you can still call it proof by exhaustion if you divide the values into classes and do the proof for each class.

> Similar way you'd prove four color theorem.

And this seems to support that idea? It's the same thing as proof by cases.

So the proof that n^2 + n is even for all integers is exhaustive: you do one proof for even integers, and another one for odd ones. But we wouldn't generally use the term "exhaustion" there because the vibes are wrong.

vjerancrnjak9mo ago

Thing with "classes" is that you need to identify them before proving and you need to prove the implication to general case.

Lean is not powerful enough to do this, to somehow conclude that there's a finite set of cases on which you can run brute-force checks and prove a general case.

j / k navigate · click thread line to collapse

0 pointsalmostgotcaught9mo ago0 comments

> Let's look at Hindley-Milner. You're saying that Hindley-Milner does not prove tiny theorems about types, it just exhaustively proves that no TypeError will occur. This statement is incorrect.

This is irrelevant.

Yes my original comment said exactly this.

The rest is irrelevant.

Reread my original comment again - or any of my follow-up comments - I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

0 comments

vjerancrnjak9mo ago

> I didn't say the lean code doesn't prove equality, I said it proves it using exhaustion.

What is exhaustion for you? For everyone else in this thread, exhaustion means trying out all values and proving it works.

Similar way you'd prove four color theorem.

thaumasiotes9mo ago

> For everyone else in this thread, exhaustion means trying out all values and proving it works.

My instinct was that you can still call it proof by exhaustion if you divide the values into classes and do the proof for each class.

> Similar way you'd prove four color theorem.

And this seems to support that idea? It's the same thing as proof by cases.

vjerancrnjak9mo ago

Thing with "classes" is that you need to identify them before proving and you need to prove the implication to general case.

Lean is not powerful enough to do this, to somehow conclude that there's a finite set of cases on which you can run brute-force checks and prove a general case.

j / k navigate · click thread line to collapse