Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Verified dynamic programming with Σ-types in Lean

tannerduve.github.io

Post reply on HN
Print view View original

21–30 of 46 posts

Re: Verified dynamic programming with Σ-types in Lean

#21

Post by thaumasiotes »

almostgotcaught wrote: post #16
lacker wrote: post #15

Earlier quoted context omitted.

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…

> 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 nu…

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

Re: Verified dynamic programming with Σ-types in Lean

#22

Post by CSMastermind »

I've been meaning to learn Lean and fascinated with the concept but syntax like:

    let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat
is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

Re: Verified dynamic programming with Σ-types in Lean

#23

Post by westurner »

CSMastermind wrote: post #22

I've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

Does aliasing the types work?

  def MemoMap := HashMap Nat Nat
  def MemoResult := Nat × MemoMap

  let rec helperMemo : Nat → MemoMap → MemoResult

Re: Verified dynamic programming with Σ-types in Lean

#24

Post by thaumasiotes »

jeremyscanvic wrote: post #3

Really interesting trick!

He doesn't mention it, but this is a form of proof by induction. (As you'd expect, really, for a universal statement.)

Induction is often taught as something you do with natural numbers. But it's actually something you do with sets that are defined inductively. Any time you have a set that is defined like so:

    1. x is in the set.

    2. for all y in the set, f(y) is in the set
(where x and f are constants), you can apply induction. The base case is that you show some property is true of x. The inductive step is that you show that when the property is true of y, it is necessarily true of f(y).

If you have multiple elements that you guarantee will be in the set, each of them must be dealt with as a base case, and if you have multiple rules generating new elements from existing ones, each of them must be dealt with as another inductive step.

For the case of the natural numbers, x is 0, and f is the successor function.

If you wanted to apply this model to the Fibonacci sequence, you could say that the tuple (0, 1, 1) is in the set [representing the idea "F_1 is 1"] and provide the generator f((a, b, c)) = (b, a+b, c+1). Then since (0, 1, 1) is in the set, so is (1, 1, 2) [or "F_2 is 1"], and then (1, 2, 3) ["F_3 is 2"], and so on.

(Or you could say that the two tuples (1, 1) and (2, 1) are both in the set, and provide the generator f( (i, x), (i+1, y) ) = (i+2, x+y). Now your elements are simpler, your generator is more complex, and your set has exactly the same structure as before.)

The approach taken by the author's "improved solution" is to define a set consisting of the elements of the memoization table, with the generator being the function chain that adds elements to the table. He annotates the type of the elements to note that they must be correct (this annotation is administrative, just making it easy to describe what it is that we want to prove), and then does a proof over the addition operation that this correctness is preserved (the inductive step!).

Re: Verified dynamic programming with Σ-types in Lean

#25

Post by tossandthrow »

westurner wrote: post #23
CSMastermind wrote: post #22

I've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

Does aliasing the types work? def MemoMap := HashMap Nat Nat def MemoResult := Nat × MemoMap let rec helperMemo : Nat → MemoMap → MemoResult

Record types would likely help a lot also.

Tupples don't really indicate what I can expect from the members.

Re: Verified dynamic programming with Σ-types in Lean

#26

Post by [deleted] »

almostgotcaught wrote: post #6
Quekid5 wrote: post #5

Earlier quoted context omitted.

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

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]

Re: Verified dynamic programming with Σ-types in Lean

#27

Post by tikhonj »

CSMastermind wrote: post #22

I've been meaning to learn Lean and fascinated with the concept but syntax like: let rec helperMemo : Nat → HashMap Nat Nat → Nat × HashMap Nat Nat is a big turnoff to me. I find it annoying to parse mentally. I can do it but I have to concentrate or it's easy to gloss over an important detail.

What makes it hard to parse? The lack of parentheses? The way HashMap Nat Nat is a bit verbose and not clear at a glance? Something else?

Re: Verified dynamic programming with Σ-types in Lean

#28

Post by codethief »

SkiFire13 wrote: post #9
codethief wrote: post #8

Earlier quoted context omitted.

I'm not quite following. According to the OP and the docs you linked, a subtype is defined by a base type and a predicate. In other words: You can view it as a subset of the set of elements of the base type. That's pretty much the standard definition of a subtype. Object-oriented programming languages are not that different: The types induced by classes can easily be viewed as sets: A child class is a specialized ver…

> You can view it as a subset of the set of elements of the base type. Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa. They are not a subset of the other, hence why it's improper to consider one a subtype of the other.

> Technically speaking the elements in the supertype are all distinct from the elements in the subtype and viceversa.

Emphasis on "technically". The embedding is trivial. The Lean docs linked by the GP suggest to put those technicalities aside:

> Even though they are pairs syntactically, Subtype should really be thought of as elements of the base type with associated proof obligations.

Re: Verified dynamic programming with Σ-types in Lean

#29

Post by almostgotcaught »

thaumasiotes wrote: post #21
almostgotcaught wrote: post #16

Earlier quoted context omitted.

> 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 nu…

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

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

Re: Verified dynamic programming with Σ-types in Lean

#30

Post by vjerancrnjak »

almostgotcaught wrote: post #29
thaumasiotes wrote: post #21

Earlier quoted context omitted.

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

> 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 t…

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.

Post reply on HN