I will reiterate my suggestion to use finite sets for indexing when possible, which sidesteps the question, but while I would like to defer to Norm here, I really think a lack of consistency is going to cause actual problems in this area. What is the definition of a matrix multiplied by a vector? Surely the vector has to be using the same indexing as the matrix. Perhaps we can have a separate type for vectors than words, but this seems superfluous and repetitive.
I am willing to defer to decisions on convention making but I would like to see some clear path forward for the main definitions here and how they are not better served by a minor variation on the definition such as reindexing. Mario On Wed, Sep 2, 2020 at 12:30 AM Thierry Arnoux <[email protected]> wrote: > 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. 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 a11 (in 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 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]. > 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 > <https://groups.google.com/d/msgid/metamath/d605c6c1-20ff-3b46-228b-4645c704db08%40gmx.net?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/CAFXXJSspwoKtV5cGUwenJJ4MF4js-a_mzhVyi-7vi9KAkkJKRw%40mail.gmail.com.
