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 <[email protected]> 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/0173f6ec-7faf-41a8-816d-7becca681ba0n%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/0173f6ec-7faf-41a8-816d-7becca681ba0n%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/CAFXXJStjbtM3zDiYQnb42UG-PrdVRmgJgJT%2BnT%3D_P8dVcjDUcA%40mail.gmail.com.
