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 <http://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 <http://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
<http://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>.
