[thaumasiotes]

> my friend you should either read the article more closely or think harder

Hmmm.

> no property of any numbers is checked here - just that one function agrees with another:

    theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n

> this is the part that's undecidable (i should've said that instead of "impossible")

> https://en.wikipedia.org/wiki/Richardson%27s_theorem

Given that both `maxDollars n` and `maxDollars_spec n` are defined to be natural numbers, I'm not sure why Richardson's theorem is supposed to be relevant.

But even if it was, the structure of the proof is to produce the fact `maxDollars_spec n = maxDollars n` algebraically from a definition, and then apply the fact that equality is symmetric to conclude that `maxDollars n = maxDollars_spec n`. And once again I'm not sure how you could possibly fail to conclude that two quantities are equal after being given the fact that they're equal.

[almostgotcaught]

> Given that both `maxDollars n` and `maxDollars_spec n` are defined to be natural numbers, I'm not sure why Richardson's theorem is supposed to be relevant

Did you know that the naturals are a subset of the reals? If Richardson's doesn't convince you there's also

https://en.m.wikipedia.org/wiki/Rice%27s_theorem

> Examples

> Is P equivalent to a given program Q?

Irrespective of where you're convinced it's 100% true that equality of two functions is undecidable in general.

[vjerancrnjak]

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.

The Lean program in the article, adds `maxDollars_spec n` as a type on `helper`, with strong induction actually proves for all N possible that the implementation of the dynamic program is correct.

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.

Similar things were done with Z3 prover for other functions. Bit tricks, you want to go from one subset repr to the next. Subset {1, 3} is encoded as 101. Subset {1, 3, 7} as 1010001. You want to go to the next lexicographically greater subset of size 3. You can do that with efficient bit tricks, or you can write a recursive spec. You can use Z3 prover to prove for bitset of size N, that your algorithm that uses efficient tricks is equivalent to the recursive spec.

If Z3 prover actually had to go through all pairs (x,y) to prove that f(x)=y, you'd never get the proof in time.

[almostgotcaught]

> 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.

[vjerancrnjak]

> 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.)

[thaumasiotes]

> 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.

[vjerancrnjak]

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.

[thaumasiotes]

> Did you know that the naturals are a subset of the reals?

Well, all I can say here is that my intuition suggested to me that proofs about the complexity of a set are generally not extensible to much-less-complex subsets.

But OK. If you want an objection stated in terms of Richardson's theorem, where are we invoking the sine function?

> Irrespective of where you're convinced it's 100% true that equality of two functions is undecidable in general.

So what? We're not trying to decide the equality of two functions in general. We're deciding the equality of two functions in specific.

> If Richardson's doesn't convince you there's also https://en.m.wikipedia.org/wiki/Rice%27s_theorem

>> Is P equivalent to a given program Q?

Again, why is this supposed to matter?

Here are two programs in C:

    int main(int argc, char* argv[]) {
      return 0;
    }

    int main(int argc, char* argv[]) {
      return 3 + 1 - 4;
    }

Is it undecidable whether those two programs are equivalent?

Rice's theorem says there is no algorithm which will take two programs as input and return yes if they're equivalent while returning no if they aren't. But no attempt has been made to supply such an algorithm.