5 ms·

This is proof by exhaustion: the "proof" just computes the entire memo table for any n and compares the values in the table with the corresponding return from r

This is proof by exhaustion: the "proof" just computes the entire memo table for any n and compares the values in the table with the corresponding return from recursive definition. You could write this same proof in absolutely any language that supports recursion (or not, if you transform to the bottom-up formulation).

duve02 1y ago
> You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.
Quekid5 1y ago
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
- almostgotcaught 1y ago
  i don't know what you're saying - here is the proof that is described in the article: 1. build a table tab[n] 2. check that for every i, tab[i] == maxDollars_spec[i] if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.
  - deleted 1y ago
    [deleted]
lacker 1y ago
In Lean you don't actually have to run this for every n to verify that the algorithm is correct for every n. Correctness is proved at type-checking time, without actually running the algorithm. That's something that you can't do in a normal programming language.
- almostgotcaught 1y ago
  it's explicitly stated in the article: > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof if you thought harder about it you'd realize what you're suggesting is impossible
  - lacker 1y ago
    It's not impossible, that's the whole point of a theorem prover. You write a computation, but you don't actually have to run the computation. Simply typechecking the computation is enough to prove that its result is correct. For example, in a theorem prover, you can write an inductive proof that x^2 + x is even for all x. And you can write this via a computation that demonstrates that it's true for zero, and if it's true for x, then it's true for x + 1. However, you don't need to run this computation in order to prove that it's true for large x. That would be computationally intractable, but that's okay. You just have to typecheck to get a proof.
    - almostgotcaught 1y ago
      > you can write an inductive proof that x^2 * (x^2 - 1) is divisible by 4 for all x my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation. the obvious indicator is that 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 https://en.wikipedia.org/wiki/Richardson%27s_theorem
      - thaumasiotes 1y ago
        > 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 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.
SkiFire13 1y ago
> the "proof" just computes the entire memo table for any n No, this is what would happen _if you ran the proof_, but proofs are not meant to be ran in the first place! The usual goal is proving their correctness, and for that it's enough for them to _typecheck_.
- almostgotcaught 1y ago
  it's explicitly stated in the article: > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof if you thought harder about it you'd realize what you're suggesting is impossible
  - SkiFire13 1y ago
    > it's explicitly stated in the article: > > > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof That's what the intermediate function is doing, but _it doesn't need to be executed_ for the final proof to be valid. > if you thought harder about it you'd realize what you're suggesting is impossible No, it is perfectly possible. This is not a program running all cases and `assert`ing that they have the expected result, this is a proof encoded as a program that when executed will surely produce a proof that for the given n the theorem holds. But it surely produces a proof when executes you don't need to execute it to know that a proof exists and thus the theorem holds! This is exactly what mathematicians do when they prove theorems. Do you think they go on and check for every number n that some theorem holds? That's impossible to do for every possible n, and this is exactly what you're claiming you can do in every other language. And just to be extra clear, a signature like this: > theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n Does not mean that for every n the function returns a boolean indicating whether `maxDollars n` is equal to `maxDollars_spec n` or not. Instead, it _surely_ returns a proof that they are equal. And with _surely_ I mean it cannot return errors or exceptions or whatever. It is guaranteed that the function will terminate with a proof for that proposition, which I want to reiterate again, it's the same as knowing that the proposition is true.
  - ImprobableTruth 1y ago
hansvm 1y ago
That can't possibly be the case. The thing concluded was that for every n the statement holds. To do that exhaustively for _every_ n requires infinite time. Either their conclusion is incorrect, or your description of the proof is incorrect.
Tainnor 1y ago
A language without dependent types wouldn't even let you write down the statement of the theorem, so no.

duve02 1y ago

> You could write this same proof in absolutely any language that supports recursion Well, you at least need dependent types just to state the theorem, which eliminates nearly all other languages.

Quekid5 1y ago

Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.

almostgotcaught 1y ago
i don't know what you're saying - here is the proof that is described in the article: 1. build a table tab[n] 2. check that for every i, tab[i] == maxDollars_spec[i] if you take the latter approach i proposed (bottom up) there is nothing to check the totality of.
- deleted 1y ago
  [deleted]

lacker 1y ago

In Lean you don't actually have to run this for every n to verify that the algorithm is correct for every n. Correctness is proved at type-checking time, without actually running the algorithm. That's something that you can't do in a normal programming language.

almostgotcaught 1y ago
it's explicitly stated in the article: > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof if you thought harder about it you'd realize what you're suggesting is impossible
- lacker 1y ago
  It's not impossible, that's the whole point of a theorem prover. You write a computation, but you don't actually have to run the computation. Simply typechecking the computation is enough to prove that its result is correct. For example, in a theorem prover, you can write an inductive proof that x^2 + x is even for all x. And you can write this via a computation that demonstrates that it's true for zero, and if it's true for x, then it's true for x + 1. However, you don't need to run this computation in order to prove that it's true for large x. That would be computationally intractable, but that's okay. You just have to typecheck to get a proof.
  - almostgotcaught 1y ago
    > you can write an inductive proof that x^2 * (x^2 - 1) is divisible by 4 for all x my friend you should either read the article more closely or think harder. he's not proving that the recurrence relation is correct (that would be meaningless - a recurrence relation is just given), he's proving that DP/memoization computes the same values as the recurrence relation. the obvious indicator is that 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 https://en.wikipedia.org/wiki/Richardson%27s_theorem
    - thaumasiotes 1y ago
      > 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 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.

SkiFire13 1y ago

> the "proof" just computes the entire memo table for any n No, this is what would happen _if you ran the proof_, but proofs are not meant to be ran in the first place! The usual goal is proving their correctness, and for that it's enough for them to _typecheck_.

almostgotcaught 1y ago
it's explicitly stated in the article: > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof if you thought harder about it you'd realize what you're suggesting is impossible
- SkiFire13 1y ago
  > it's explicitly stated in the article: > > > For an arbitrary n, compute the table full of values and their proofs, and just pull out the nth proof That's what the intermediate function is doing, but _it doesn't need to be executed_ for the final proof to be valid. > if you thought harder about it you'd realize what you're suggesting is impossible No, it is perfectly possible. This is not a program running all cases and `assert`ing that they have the expected result, this is a proof encoded as a program that when executed will surely produce a proof that for the given n the theorem holds. But it surely produces a proof when executes you don't need to execute it to know that a proof exists and thus the theorem holds! This is exactly what mathematicians do when they prove theorems. Do you think they go on and check for every number n that some theorem holds? That's impossible to do for every possible n, and this is exactly what you're claiming you can do in every other language. And just to be extra clear, a signature like this: > theorem maxDollars_spec_correct : ∀ n, maxDollars n = maxDollars_spec n Does not mean that for every n the function returns a boolean indicating whether `maxDollars n` is equal to `maxDollars_spec n` or not. Instead, it _surely_ returns a proof that they are equal. And with _surely_ I mean it cannot return errors or exceptions or whatever. It is guaranteed that the function will terminate with a proof for that proposition, which I want to reiterate again, it's the same as knowing that the proposition is true.
- ImprobableTruth 1y ago

hansvm 1y ago

That can't possibly be the case. The thing concluded was that for every n the statement holds. To do that exhaustively for _every_ n requires infinite time. Either their conclusion is incorrect, or your description of the proof is incorrect.

Tainnor 1y ago

A language without dependent types wouldn't even let you write down the statement of the theorem, so no.