FWIW I agree with Benoit and Alexander (and Dijkstra) on both counts. :) On Sun, Apr 26, 2020 at 4:23 AM Benoit <[email protected]> wrote:
> Like Alexander, I agree that word indices start at 0... like natural > numbers ;-) > > On Sunday, April 26, 2020 at 8:49:01 AM UTC+2, Alexander van der Vekens > wrote: >> >> 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/95e2049c-c07c-40d7-b0e3-79061ef5327c%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/95e2049c-c07c-40d7-b0e3-79061ef5327c%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/CAFXXJSvnEcJPc%2BPd13imWhe8vYXcjSk-b_AmdthwgBJM7s3_ig%40mail.gmail.com.
