On Sun, Apr 26, 2020 at 17:31:09 +0200 (CEST) fl wrote: > Dijkstra's argument doesn't seem to apply to our problem. He is dealing > with finding a good convention to speak of a sequence of natural numbers > using <= or <. It is not at all our problem. We don't use order relations > to speak of a word. He also says he prefers 0 because when you use the > convention 0 <= x < N the bound is N not N +1. Once again it is not our > problem: we don't use order relations. Our unique problem is what is better > when we concatenate two words. And do we prefer our proofs are cluttered > with expressions N - 1 or with the simpler N? >
This is an interesting choice of argument because these seem to be exactly the places where the present state of affairs is strongest. As for 0 <= x < N, of course we use order relations, we don't write it that way but rather x e. ( 0 ..^ N ) and in that form it appears all over the place in the theory of words and otherwise. I agree the notation ..^ is a bit opaque; I prefer the notation used in Rust, where 0..n is our ( 0 ..^ n ) and 0..=n is our ( 0 ... n ). It makes it more obvious which one is the preferred notation, and it works great for for loops since you almost always want a simple for loop to range over 0 <= x < N. As for concatenation, half open words have the beautiful identity ( A ..^ C ) = ( ( A ..^ B ) u. ( B ..^ C ) ), with no off by one errors. This alone makes them worthwhile to me. So if your worry is being "cluttered with expressions N - 1" then you should note that there is no such clutter in these expressions. -- 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/CAFXXJSuvyZHNkwLYe%3DneuxX-E%3Db3Fi%3D5eH-jDrHSN3QNXMjvjg%40mail.gmail.com.
