4 ms·

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, withou

by 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.
      - almostgotcaught 1y ago
        > 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 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 1y ago
        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.

by lacker 1y ago

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.
    - almostgotcaught 1y ago
      > 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 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 1y ago
        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.