6 ms·

You still need to construct the algorithm in the first place, which is what a constructive proof does.

auggierose 6y ago
Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.
- vcdimension 6y ago
  I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.
  - auggierose 6y ago
    Nope, we are not at cross-purposes. You just don't understand what I am saying. Let's say you need an algorithm for a real-life situation, and you manage to write one down. Ok then, you are good to go, just use it! But ... how do you know that the algorithm you have written down is correct? Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?
    - vcdimension 6y ago
      Yes, but if I told IBM that I had a proof that a particular algebraic property or relationship related to homomorphic encryption holds true, I'm sure they would much prefer that it was constructive, rather than non-constructive, because they can produce a usable algorithm from the constructive proof. The point is that by exploring mathematics using only constructive proofs, we are guaranteed to produce (possibly useful) algorithms. If you already have an algorithm, and can prove it works non-constructively then fine, but a collection of N non-constructive proofs is not nearly so useful for real-life applications as a collection of N constructive ones.
      - deleted 6y ago
        [deleted]
      - auggierose 6y ago
        Your argument is wrong in so many ways, but let me just show you one: A constructive proof guarantees that there is an algorithm, but it doesn't say anything about the runtime of that extracted algorithm. Now, what good is an algorithm that is much too slow to be practically useful? In general, my hypothesis is that if you restrict yourself to constructive mathematics, you are limiting yourself. And that is true whether your chosen field is algorithms, or not. Now, if you offer me for a given algorithm a constructive proof, that's great. But if you needed 10 years to give me that proof, and a non-constructive one can be had in 10 minutes, I might not be so enthusiastic if I had to pay your salary, or if I needed that result really urgently, or both. But on the other hand, IBM probably doesn't care.
        vcdimension 6y ago
        Hey, there's no need to by so impolite. My argument is not wrong, it's just a different argument to yours (which I fully understand, and is not difficult to grasp). Your example doesn't discount mine in any way; a slow algorithm is still better than no algorithm at all. The point about proving the correctness of an existing algorithm is moot, I'm talking about mathematical proofs which in themselve lead to algorithms. I'm not claiming we should abandon non-constructive mathematics, just that formalizing mathematics constructively leads to more useful algorithms. Similar to the argument that some programmers make about constraining themselves to think purely functionally in order to produce less buggy code. Goodnight.
        auggierose 6y ago
        Yeah, it's wrong. You could say that true and false are, just different. Well. And you should have seen the answer that I wrote before that, and then deleted. Now THAT answer was impolite. Goodnight to you as well.
      - jhanschoo 6y ago
        You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point. > I'm sure they would much prefer that it was constructive, rather than non-constructive One point against constructivism is that the proof could be less readable. > can produce a usable algorithm from the constructive proof No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.
- creata 6y ago
  But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?
  - auggierose 6y ago
    I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.
    - deleted 6y ago
      [deleted]
    - auggierose 6y ago
      Here is an example: after inputing positive integers a, b and c, output all natural numbers n for which a^n + b^n = c^n. My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop. This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.
      - rssoconnor 6y ago
        Fermat's last theorem holds constructively. This is because we can take the entire proof an rewrite it using the "classical fragment" of constructive logic[1]. I don't know if the proof of FLT (appears) to use the axiom of choice or not, but if it does we use Shoenfield's absoluteness theorem to remove any uses of the axiom of choice from the proof. And we are done, because the statement of the theorem in the "classical fragment" of constructive logic is identical to the constructive statement as it does not involve any existentials or disjunctions. However if the theorem did involve a limited use of these connectives, we could use Goedel's Dialectica interpretation[3] to turn them in to their constructive counterparts, as long as the theorem is Pi_2 or lower, which is going to be the case for the vast majority of theorems about software. [1] https://news.ycombinator.com/item?id=26217587 https://news.ycombinator.com/item?id=26217587 [2] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_absoluteness_theorem https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_ab... [3] https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf

Sure, but you would not need to prove it in a constructive way. See, that is one of the problems with constructive mathematics. It not only requires you to write down the algorithm, but also to prove it constructively, although a non-constructive proof would be perfectly fine. In other words: constructivism is often overkill.

vcdimension 6y ago
I think we're at cross-purposes; I am talking about mathematics for the purpose of real-life useful applications (e.g. cryptography, data analysis, etc), in which case you need algorithms.
- auggierose 6y ago
  Nope, we are not at cross-purposes. You just don't understand what I am saying. Let's say you need an algorithm for a real-life situation, and you manage to write one down. Ok then, you are good to go, just use it! But ... how do you know that the algorithm you have written down is correct? Now, a constructive mathematician would require you to also provide a constructive proof for your algorithm. A mainstream mathematician would additionally also be fine with a non-constructive proof for your algorithm. So, who is more real-life?
  - vcdimension 6y ago
    Yes, but if I told IBM that I had a proof that a particular algebraic property or relationship related to homomorphic encryption holds true, I'm sure they would much prefer that it was constructive, rather than non-constructive, because they can produce a usable algorithm from the constructive proof. The point is that by exploring mathematics using only constructive proofs, we are guaranteed to produce (possibly useful) algorithms. If you already have an algorithm, and can prove it works non-constructively then fine, but a collection of N non-constructive proofs is not nearly so useful for real-life applications as a collection of N constructive ones.
    - deleted 6y ago
      [deleted]
    - auggierose 6y ago
      Your argument is wrong in so many ways, but let me just show you one: A constructive proof guarantees that there is an algorithm, but it doesn't say anything about the runtime of that extracted algorithm. Now, what good is an algorithm that is much too slow to be practically useful? In general, my hypothesis is that if you restrict yourself to constructive mathematics, you are limiting yourself. And that is true whether your chosen field is algorithms, or not. Now, if you offer me for a given algorithm a constructive proof, that's great. But if you needed 10 years to give me that proof, and a non-constructive one can be had in 10 minutes, I might not be so enthusiastic if I had to pay your salary, or if I needed that result really urgently, or both. But on the other hand, IBM probably doesn't care.
      - vcdimension 6y ago
        Hey, there's no need to by so impolite. My argument is not wrong, it's just a different argument to yours (which I fully understand, and is not difficult to grasp). Your example doesn't discount mine in any way; a slow algorithm is still better than no algorithm at all. The point about proving the correctness of an existing algorithm is moot, I'm talking about mathematical proofs which in themselve lead to algorithms. I'm not claiming we should abandon non-constructive mathematics, just that formalizing mathematics constructively leads to more useful algorithms. Similar to the argument that some programmers make about constraining themselves to think purely functionally in order to produce less buggy code. Goodnight.
        auggierose 6y ago
        Yeah, it's wrong. You could say that true and false are, just different. Well. And you should have seen the answer that I wrote before that, and then deleted. Now THAT answer was impolite. Goodnight to you as well.
    - jhanschoo 6y ago
      You probably have no experience with constructive proof checkers, else you wouldn't be missing Auggie's point. > I'm sure they would much prefer that it was constructive, rather than non-constructive One point against constructivism is that the proof could be less readable. > can produce a usable algorithm from the constructive proof No. Between the automated tactics and inductive propositions constructed to carry all kinds of redundant state helpful in proving your properties, your proof objects won't be anywhere near production level. And constructive proof checkers don't intend that to happen anyway: you pretty much define an efficient function in a DSL, then use a different DSL to prove that the function fulfils the properties. The proof object is pretty much a black box with unclear efficiency that wasn't meant for humans to read.
creata 6y ago
But everything you'd typically see in an algorithm has decidable equality, so proofs by contradiction are constructively justified, no?
- auggierose 6y ago
  I don't know! But I don't think so. Also think about other properties of an algorithm, like runtime, etc. You could have a non-constructive proof for the upper bound on the runtime, but not a constructive one.
  - deleted 6y ago
    [deleted]
  - auggierose 6y ago
    Here is an example: after inputing positive integers a, b and c, output all natural numbers n for which a^n + b^n = c^n. My algorithm: If a + b == c then output 1. If a^2 + b^2 == c^2 then output 2. Stop. This algorithm is correct, because Fermat's last theorem holds. Now, try to come up with a simpler algorithm than that, and one that in addition has a constructive proof.
    - rssoconnor 6y ago
      Fermat's last theorem holds constructively. This is because we can take the entire proof an rewrite it using the "classical fragment" of constructive logic[1]. I don't know if the proof of FLT (appears) to use the axiom of choice or not, but if it does we use Shoenfield's absoluteness theorem to remove any uses of the axiom of choice from the proof. And we are done, because the statement of the theorem in the "classical fragment" of constructive logic is identical to the constructive statement as it does not involve any existentials or disjunctions. However if the theorem did involve a limited use of these connectives, we could use Goedel's Dialectica interpretation[3] to turn them in to their constructive counterparts, as long as the theorem is Pi_2 or lower, which is going to be the case for the vast majority of theorems about software. [1] https://news.ycombinator.com/item?id=26217587 https://news.ycombinator.com/item?id=26217587 [2] https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_absoluteness_theorem https://en.wikipedia.org/wiki/Absoluteness#Shoenfield%27s_ab... [3] https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf https://www.andrew.cmu.edu/user/avigad/Papers/dialect.pdf