Verified dynamic programming with Σ-types in Lean
tannerduve.github.io
Verified dynamic programming with Σ-types in Lean
1–10 of 46 posts
Re: Verified dynamic programming with Σ-types in Lean
#2FYI 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.
Re: Verified dynamic programming with Σ-types in Lean
#3Really interesting trick!
Re: Verified dynamic programming with Σ-types in Lean
#4This 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).
Re: Verified dynamic programming with Σ-types in Lean
#5This 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).
Not if that language doesn't actually check the totality of your proof and ensures that the base case holds.
Re: Verified dynamic programming with Σ-types in Lean
#6This 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).
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.
Re: Verified dynamic programming with Σ-types in Lean
#7sigma types, hmmm
Re: Verified dynamic programming with Σ-types in Lean
#8FYI 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.
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.
Re: Verified dynamic programming with Σ-types in Lean
#9FYI 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.
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.
Re: Verified dynamic programming with Σ-types in Lean
#10FYI 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.
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…
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...