About 0 or 1 as first (or zeroth ;-) ?) index of words (see remarks of FL and Norm below):
Although there are good reasons to index the symbols of a word W by 1 .. length(W), there are also good reasons to start with 0. See, for example, Wikipedia https://en.wikipedia.org/wiki/Zero-based_numbering , especially the note *of Edsger W. Dijkstra Why numbering should start at zero* ( https://www.cs.utexas.edu/users/EWD/transcriptions/EWD08xx/EWD831.html) - Dijkstra would like our definition ( M ..^ N )... Also the argument that using the modulo function is a good one - I used this for the proof of the friendship theorem, see, for example, ~cshwidx0mod. In the context of graph theory, it is useful to index the vertices in a walk, trail, path etc. of length n by 0 ... n and the edges by 0 ..^ n . Therefore, starting words with index 0 simplifies the definition of "walks as words" (see ~ df-wwlk), which I also used for the proof of the friendship theorem. Since we are using 0 as first index already for several years, and there is a huge amount of theorems based on this definition (as already mentioned by Norm), I propose not to change the definition df-word. If there is a very good reason for a change in the future (which would justify the amount of work required to modify all existing related theorems), we can discuss this topic again. On Saturday, April 25, 2020 at 7:29:25 PM UTC+2, Norman Megill wrote: > > From FL: > > ... > > I would also appreciate if the first index of a word is 1not 0. The C > language has arrays that begins et 0 and its a pain un the neck because you > always have to deal with n - 1 expressions. > > From Norm: > ... > > 2. I assume you mean df-word. As Mario suggested, it would be helpful if > you provide the label of what you are referring to. > > I probably agree with you but I haven't worked with df-word, so others' > comments would be more valid. I wonder if the awkward "( M ..^ N )" would > largely be replaced by "( M ... N )". At this point, though, there are > hundreds of theorems involved and probably a huge effort to convert. An > important question is whether the literature typically starts with 0 or 1, > which I don't know, and it's nice to be follow the literature convention > when possible. > > (In C, I often start arrays with 1 because that's the way humans count. > For me at least it leads to fewer bugs, and being able to use n instead of > n-1 over and over saves typing and might even make up for the wasted memory > space of the unused 0th entry. I imagine, though, that for "real" C > programmers, counting from 0 is second nature so that when they see index n > it mentally means the (n+1)th entry to them, so they don't need to use n-1.) > -- 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/ea260df1-f44f-4809-bd30-ddc02d4e9301%40googlegroups.com.
