Thanks for all feedback! There are valid arguments on both sides, so we need Norm or Mario to do a final call.
On 29/08/2020 08:06, Norman Megill wrote:
While I'm not an expert, my guess is that the major uses of 0-based arrays are in computer science and some computer programming languages, where they can offer an advantage for some algorithms. But mathematics is meant for humans, and humans tend to count from 1. That's why we number the proof steps on our web pages starting with 1. Having the "first" step numbered with 0 would seem unnatural to me. As AV pointed out, we haven't been able to find a linear algebra textbook with matrices numbered from 0. On Wikipedia, there are 4 subtopics listed under https://en.wikipedia.org/wiki/Vector#Mathematics_and_physics which are: https://en.wikipedia.org/wiki/Euclidean_vector https://en.wikipedia.org/wiki/Row_and_column_vectors https://en.wikipedia.org/wiki/Vector_space https://en.wikipedia.org/wiki/Vector_field These all show 1-based indices. I have always wanted to see set.mm to be as close to mathematical literature as possible or practical. Apparently almost all of linear algebra literature uses 1-based matrices and vectors, so I think that is what set.mm should do. Even if for some purposes it would be more convenient to have matrices 0-based, it hasn't seemed to have harmed the field. My vote is to conform to the literature and have matrices and vectors 1-based. On Friday, August 28, 2020 at 2:20:35 PM UTC-4 di.... gmail.com wrote: My vote is also in favor of starting with 0, or even better, doing everything over generic finite sets when possible and falling back on ( 0 ..^ N ). I realize that close correspondence with papers is considered important here but mathematicians write for their own ease. In a math paper, you can write either a_0, ..., a_(n-1) or a_1, ..., a_n - which is easier? Besides the strictness of a few inequalities this is probably the only difference, so a_1, ..., a_n is preferred because it is very slightly shorter. In formalization, we should also write for our own ease. In this case, that means better interfacing with the theory of finite words, which uses ( 0 ..^ N ). There are also other reasons to prefer 0 based indexing but in this case I think consistency with words (viewed as 1D vectors) is more important than that. On Fri, Aug 28, 2020 at 1:43 PM Benoit wrote: I'm still in favor of words starting at 0. As for matrix rows and columns, it would be more...wait for it... natural to start at 0, but since the literature overwhelmingly prefers to start at 1, maybe it's better to conform with it (there are a few "historical accidents" like that, for instance defining \pi as half what it should be, and since the consequences are very mild, it stays like that). And to state the obvious: since most results using the fact that rows and columns are natural numbers have them intervene in the form (-1)^{i+j}, shifting both row and column indices by 1 does not change the parity of the sum, so these statements are unaffected. Benoit On Friday, August 28, 2020 at 6:14:57 PM UTC+2 Alexander van der Vekens wrote: There was a discussion in https://groups.google.com/g/metamath/c/UwTUuNPgaB0/m/NdWefzG4AgAJ about the indices for words. Currently, the indices for words start with 0, and the proposal to change this was not accepted. For matrices, however, the things are different: The indices for rows and colums usually start with 1, as Thierry explained, so I agree with Thierry. And having the planned conversion function should dispel any doubt. Alexander On Friday, August 28, 2020 at 9:45:33 AM UTC+2 Thierry Arnoux wrote: Hi all, I recently formalized a proof of the Laplace expansion of determinants (~ mdetlap), which I think would be useful to pull to the main part of set.mm <http://set.mm>. Because the formula makes calculation based on the row and column indices of the element of the matrix, I'm using matrix with integer indices (in contrast with the rest of the development on matrices which is based on arbitrary sets). I chose indices in ` ( 1 ... N ) ` , so that the top-left matrix element is a_11 (in set.mm <http://set.mm> written ` ( 1 A 1 ) ` ). It seems using indices starting from one is the convention used for mathematics, I have not found yet a reference with indices starting at zero (and neither did Norm), however we would like to run this through the community. Most programming languages start indices with zero, with the exception of R and several others. In set.mm <http://set.mm> words indices start with zero. What's your opinion? Should matrix indices start with one or zero? Thanks for your input! BR, _ Thierry PS. I would later like to define a "literal" matrix function which would be used like this to transform words (for any matrix size up to 8x8) into matrices : ( litMat ` <" <" A B C "> <" D E F "> <" G H I "> "> ) This would allow a bridge/conversion. -- -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected] <mailto:[email protected]>. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/7eeabd5a-29c3-431b-aaba-87f457827d53n%40googlegroups.com <https://groups.google.com/d/msgid/metamath/7eeabd5a-29c3-431b-aaba-87f457827d53n%40googlegroups.com?utm_medium=email&utm_source=footer>.
-- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/d605c6c1-20ff-3b46-228b-4645c704db08%40gmx.net.
