4 ms·

Sorry, but this simply does not make any sense. Algorithmic correctness does not vary in different contexts. Algorithmic usefulness/applicability does. You a

Sorry, but this simply does not make any sense. Algorithmic correctness does not vary in different contexts. Algorithmic usefulness/applicability does. You are confusing the two. Correctness here means that it provably generates a result that meets the definition of correct matrix multiplication. In this case, they prove that all algorithms generated do (and that the system will actually only generate provably correct algorithms). Applicability here is whether, when applied to a particular {not-infinite precision computer, use case}, it is viable to use it. That does not affect whether the algorithm is correct or not, only whether you can use it to achieve a particular result. If i have a computer with 1 bit of floating point precision, that does not make the algorithms all suddenly incorrect. Within the bounds of the what i can provide (not a lot), they still function exactly as they are supposed to. If i need 75 significant digits on this computer, it simply means that they are not useful for my computer because it cannot generate enough significant digits from them to be useful. That is totally orthogonal to whether the algorithms function as designed.

deleted 4y ago
[deleted]
eigenket 4y ago
An algorithm for "matrix multiplication" that assumes infinite precision arithmetic is used is essentially useless (there are some niche uses for matrices with entries in finite fields/rings). An algorithm for matrix multiplication usually comes with more than that, in particular some sort of error bound. Note that these bounds are mathematical, part of the abstract algorithm, and not something that is a property of any particular implementation (your last paragraph suggests you might be confused by this). You want a statement that says if A' is close to A (in some relevant distance measure), and B' is close to B, then your algorithm gives something close to AB. The correctness you have to prove includes proving that your error bounds are what you say they are.
- DannyBee 4y ago
  Again, useless is not the same as incorrect. It is still correct whether it can be used somewhere due to implementation limitations or not. I'm really unsure how you can possibly argue otherwise. It's like arguing that a string algorithm is incorrect because it doesn't run fast enough on strings to be usable on any current computer. It's still correct. It's just not usable. Unlike correctness, useless is very context specific. 100 years from now, an infinite precision arithmetic algorithm may be entirely useful.
  - eigenket 4y ago
    I am arguing that a matrix multiplication algorithm, like essentially any other numerical algorithm, consists of (at least) the following two parts 1. The actual steps you have to follow. 2. Some form of error bounds/analysis that tell you how good/bad the output will be given approximate inputs. In order to prove correctness you have to prove that the procedure gives the error bounds you claim. The error bounds are something you mathematically have to prove.
    - adgjlsfhk1 4y ago
      There are lots of methods (e.g. LU) that are used millions of times a day, but don't have good error bounds. Most matrix algorithms used in practice have something resembling a proof of error bounds that everyone ignores because they don't do a good job of describing the error that you actually get when you use the methods.
    - DannyBee 4y ago
      "In order to prove correctness you have to prove that the procedure gives the error bounds you claim" You don't get to just add your own requirement for correctness and then force people to prove it? They claim a specific thing - they prove that thing. That thing suffices to prove that it succeeds at matrix multiplication. You for some reason really just don't like that as far as i can tell, and argue it doesn't suffice for usefulness (which i agree on) Matrix multiplication, and "essentially any other numerical algorithm", is not defined in terms of the error bounds for correctness. That is just BS. The error bounds depend on implementation factors, and as such, they are totally unrelated to correctness. Let's take a look: https://en.wikipedia.org/wiki/Matrix_multiplication https://en.wikipedia.org/wiki/Matrix_multiplication I have read the entire definition, nowhere does it refer to error bounds as a requirement for successful matrix multiplication! The word "error" does not even appear on the page Since it's wikipedia, I also pulled out my college math books. Same thing. They prove correctness without any reference to error bounds. Those are accepted proofs. I don't see a single basic proof that has error bounds as part of correctness. It, again, wouldn't make any sense, because error bounds depend on implementation factors. So again, you simply can't add your requirement to correctness just because you like it. They still remain where they should be - usefulness for application.

deleted 4y ago

[deleted]

eigenket 4y ago

An algorithm for "matrix multiplication" that assumes infinite precision arithmetic is used is essentially useless (there are some niche uses for matrices with entries in finite fields/rings). An algorithm for matrix multiplication usually comes with more than that, in particular some sort of error bound. Note that these bounds are mathematical, part of the abstract algorithm, and not something that is a property of any particular implementation (your last paragraph suggests you might be confused by this). You want a statement that says if A' is close to A (in some relevant distance measure), and B' is close to B, then your algorithm gives something close to AB. The correctness you have to prove includes proving that your error bounds are what you say they are.

DannyBee 4y ago
Again, useless is not the same as incorrect. It is still correct whether it can be used somewhere due to implementation limitations or not. I'm really unsure how you can possibly argue otherwise. It's like arguing that a string algorithm is incorrect because it doesn't run fast enough on strings to be usable on any current computer. It's still correct. It's just not usable. Unlike correctness, useless is very context specific. 100 years from now, an infinite precision arithmetic algorithm may be entirely useful.
- eigenket 4y ago
  I am arguing that a matrix multiplication algorithm, like essentially any other numerical algorithm, consists of (at least) the following two parts 1. The actual steps you have to follow. 2. Some form of error bounds/analysis that tell you how good/bad the output will be given approximate inputs. In order to prove correctness you have to prove that the procedure gives the error bounds you claim. The error bounds are something you mathematically have to prove.
  - adgjlsfhk1 4y ago
    There are lots of methods (e.g. LU) that are used millions of times a day, but don't have good error bounds. Most matrix algorithms used in practice have something resembling a proof of error bounds that everyone ignores because they don't do a good job of describing the error that you actually get when you use the methods.
  - DannyBee 4y ago
    "In order to prove correctness you have to prove that the procedure gives the error bounds you claim" You don't get to just add your own requirement for correctness and then force people to prove it? They claim a specific thing - they prove that thing. That thing suffices to prove that it succeeds at matrix multiplication. You for some reason really just don't like that as far as i can tell, and argue it doesn't suffice for usefulness (which i agree on) Matrix multiplication, and "essentially any other numerical algorithm", is not defined in terms of the error bounds for correctness. That is just BS. The error bounds depend on implementation factors, and as such, they are totally unrelated to correctness. Let's take a look: https://en.wikipedia.org/wiki/Matrix_multiplication https://en.wikipedia.org/wiki/Matrix_multiplication I have read the entire definition, nowhere does it refer to error bounds as a requirement for successful matrix multiplication! The word "error" does not even appear on the page Since it's wikipedia, I also pulled out my college math books. Same thing. They prove correctness without any reference to error bounds. Those are accepted proofs. I don't see a single basic proof that has error bounds as part of correctness. It, again, wouldn't make any sense, because error bounds depend on implementation factors. So again, you simply can't add your requirement to correctness just because you like it. They still remain where they should be - usefulness for application.