hacker news

gugagore ・ 12 days ago

FYI the use of "subtype" here does not, as far as I know, have much connection to the concept in class-based object oriented programming languages.

https://lean-lang.org/doc/reference/latest/Basic-Types/Subty...

A crucial difference between type theory (as its known in Lean) and set theory is that an inhabitant/element is of exactly one type.

ImprobableTruth ・ 12 days ago

Caveat: Coercions exist in Lean, so subtypes actually can be used like the supertype, similar to other languages. This is done via essentially adding an implicit casting operation when such a usage is encountered.
codethief ・ 12 days ago

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 version of its parent's class, hence a subtype/subset thereof if you define all the sets by declaring `instanceof` to be their predicate function.
- nickpsecurity ・ 12 days ago
  
  B. Meyer made an attempt to formulate many concepts in programming using simple, set theory. It might help in discussions like this. I say might since I'm not mathematically-inclined enough to know for sure.
  https://bertrandmeyer.com/2015/07/06/new-paper-theory-of-pro...
- SkiFire13 ・ 12 days ago
  
  > 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.
  
  codethief ・ 12 days ago
  ・ 2 more
  
  > 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.
  
  gugagore ・ 11 days ago
  
  Right, though the embedding is trivial, the conceptual distinction is not. In Lean, a subtype is a refinement that restricts by proof. In OOP, a subclass augments or overrides behavior. It's composition versus inheritance. The trivial embedding masks a fundamental shift in what "subtype" means.

almostgotcaught ・ 12 days ago

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

lacker ・ 12 days 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 ・ 12 days 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 ・ 12 days ago
  ・ 11 more
  
  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 ・ 12 days ago
  ・ 10 more
  
  > 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
  
  thaumasiotes ・ 12 days ago
  ・ 8 more
  
  > 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 ・ 12 days ago
  ・ 7 more
  
  > 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 ・ 12 days ago
  ・ 5 more
  
  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 ・ 12 days ago
  ・ 4 more
  
  > 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 ・ 12 days ago
  ・ 3 more
  
  > 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 ・ 11 days ago
  ・ 2 more
  
  > 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 ・ 11 days 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.
  
  thaumasiotes ・ 11 days ago
  
  > 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.
  
  Hercuros ・ 11 days ago
  
  The specification proves a property about an algorithm/function, namely the equivalence between a more complicated memoizing implementation and a simpler direct recursive implementation.
  It is also true that no numerical reasoning is happening: the memoized version of any recursive relation will return the same result as the original function, assuming the function is not stateful and will return the same outputs given the same inputs.
  However, it is not true to say that it does this by exhaustion, since there are infinitely many possible outputs and therefore it cannot be exhaustively checked by direct computation. The “n” for which we are “taking the proof” is symbolic, and hence symbolic justification and abstract invariants are used to provide the proof. It is the symbolic/abstract steps that are verified by the type checker, which involves only finite reasoning.
  Of course, the symbolic steps somewhat mirror the concrete computations that would happen if you build the table, especially for a simpler proof like this. But it also shouldn’t be surprising that a program correctness proof would look at the steps that a program takes and reason about them in an abstract way to see that they are correct in all cases.
SkiFire13 ・ 12 days 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 ・ 12 days 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
  
  ImprobableTruth ・ 12 days ago
  ・ 2 more
  
  This is the fault of sloppy language. In Lean, _proofs_ (equivalent to functions) and _proof objects/certificates_ (values) need to be distinguished. You can't compute proofs, only proof objects. In the above quote, replace "proof" with "certificate" and you'll see that it's a perfectly valid (if trivial - it essentially just applies a lemma) proof.
  
  almostgotcaught ・ 12 days ago
  
  a distinction without a difference wrt what i'm pointing out: this proof uses exactly zero mathematics just effectively checks all the values of maxDollars_spec.
  
  SkiFire13 ・ 10 days 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.
hansvm ・ 12 days 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.
Quekid5 ・ 12 days ago

Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
- almostgotcaught ・ 12 days 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.
  
  undefined ・ 12 days ago
  
  [deleted]
duve02 ・ 11 days 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.
Tainnor ・ 11 days ago

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

CSMastermind ・ 12 days ago

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.

duve02 ・ 11 days ago
Hey, author here. This is actually not-great style on my part. Is the following better?
```
   let rec helperMemo (n : Nat) (map : HashMap Nat Nat) : Nat × HashMap Nat Nat
```
This is how it would usually be written. I will update the post accordingly.
westurner ・ 12 days ago
Does aliasing the types work?
```
  def MemoMap := HashMap Nat Nat
  def MemoResult := Nat × MemoMap

  let rec helperMemo : Nat → MemoMap → MemoResult
```
- tossandthrow ・ 12 days ago
  
  Record types would likely help a lot also.
  Tupples don't really indicate what I can expect from the members.
runeblaze ・ 10 days ago
Tbh this is exactly how I felt in my algebraic geometry class. I still remember the fear I had when reading this from the blackboard
```
    Defn. f: X → Y is flat ⇔ O_{Y,f(x)} → O_{X,x} flat ∀ x.
```
Then immediately I dropped that class. Turns out I like real analysis much more
undefined ・ 11 days ago

[deleted]
tikhonj ・ 12 days ago

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?

jeremyscanvic ・ 12 days ago

Really interesting trick!

thaumasiotes ・ 12 days ago
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!).
- duve02 ・ 11 days ago
  
  Great breakdown of this. Thanks.

Gehinnn ・ 12 days ago

This would be the classical proof via strong induction, without Σ-types:

https://live.lean-lang.org/#codez=JYWwDg9gTgLgBAZRgEwHQBECGN...

Doing the proof inside the algorithm (i.e. doing inline induction over the algorithm recursion structure) has the advantage that the branching structure doesn't have to be duplicated as in an external proof like the one I did.

In my proof I didn't struggle so much with induction, but much more with basic Lean stuff, such as not getting lost in the amount of variables, dealing with r.fst/r.snd vs r=(fst, snd) and the confusing difference of .get? k and [k]?.

duve02 ・ 11 days ago

Nice job. My attempt at the initial strong induction proof was a long time ago so I don't remember the details. It definitely followed a similar structure as yours (but this was before `omega` im pretty sure). Can't quite remember where I got stuck but your proof is good. Thanks!

xnacly ・ 12 days ago

sigma types, hmmm

Verified dynamic programming with Σ-types in Lean