3 ms·

You raise two fine points. > Natural numbers should start with 0 [0]. I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an earl

You raise two fine points. > Natural numbers should start with 0 [0]. I agree 100% with Dijkstra about where the numbers should begin. In fact, here's an early draft in which we were using 0 instead of 1: [0]. The reason we ended up going with 1 is we were imitating the structure of the proofs in Landau's "Foundations", and he uses 1 as his first number. An interesting takeaway was the following. The way he structures his theorems and proofs, he makes use of his assumption that 0 is not a natural number. For example, Theorem 7 in the book is "y != x + y (for all natural numbers x, y)". So I found that sticking to my roots as a programmer (and admirer of Dijkstra) and insisting on zero-indexing led to more complicated theorem statements (e.g. "y != x + y for all natural numbers x, y > 0"). I'm not sure whether this is something structural about how the properties of natural numbers, integers, etc. relate; or whether it's an artefact of Landau's approach. > Suspiciously, the following lines in the proof can be entirely removed while still verifying: Suspicion warranted! The first (or zeroth) of these is a bug we hadn't fixed yet (see [1]). Our implementation is rather rough around the edges, but I've put a small fix for this—try again and tell me what you think. The line "term 1 nat" interestingly isn't used in the theorem we've written, so it's more a mistake on our part for including it in the sample code. Good spot! See the language page [2] for an example where it is used. As an aside, have you noticed that our proof style is based on what we call "Dijkstra-chaining"? Any thoughts on this? [3] [0] https://paste.sr.ht/~akiarie/d7a2ae368faae4ba9a8bc13eeefcf1886a91350f#None-L26 https://paste.sr.ht/~akiarie/d7a2ae368faae4ba9a8bc13eeefcf18.... [1] https://todo.sr.ht/~lbnz/i2/1 https://todo.sr.ht/~lbnz/i2/1 [2] https://i2lang.org/#uses1 https://i2lang.org/#uses1 [3] https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/EWD1073.html https://www.cs.utexas.edu/users/EWD/transcriptions/EWD10xx/E...

IshKebab 4y ago
Presumably the theorem becomes `y >= x + y`? Difficult to convince the entire field of mathematics that they are wrong though. It's hard enough to convince programmers - humans just have first=1 drummed into us so much it's like trying to convince a stone age man that the world is round. I think mathematicians care even less because most of the problems with starting from 1 can be hand waved away when you're just writing non-executable formulas and can make up any syntax you want on the spot. If anything is really awkward with 1-based numbering, just change the notation so that it isn't! Programmers can't really do that so they feel the pain more.
- akiarie 4y ago
  I think the challenge is it isn't completely obvious to me that starting with 0 is pedagogically correct, though it is so logically. `y >= x + y` is different from `y != x + y`; the former says that addition (of natural numbers) is monotonically increasing, the latter that there is no identity element. Is it possible that admitting an identity element is confusing for beginners? Or is this just a consequence of my own educational conditioning? (For the record I think all the arguments Dijkstra gives for 0-indexing are correct. I just lack the mathematical intuition to see why the special case above appears to be one in which admission of 0 as complicates things.)

IshKebab 4y ago

Presumably the theorem becomes `y >= x + y`? Difficult to convince the entire field of mathematics that they are wrong though. It's hard enough to convince programmers - humans just have first=1 drummed into us so much it's like trying to convince a stone age man that the world is round. I think mathematicians care even less because most of the problems with starting from 1 can be hand waved away when you're just writing non-executable formulas and can make up any syntax you want on the spot. If anything is really awkward with 1-based numbering, just change the notation so that it isn't! Programmers can't really do that so they feel the pain more.

akiarie 4y ago
I think the challenge is it isn't completely obvious to me that starting with 0 is pedagogically correct, though it is so logically. `y >= x + y` is different from `y != x + y`; the former says that addition (of natural numbers) is monotonically increasing, the latter that there is no identity element. Is it possible that admitting an identity element is confusing for beginners? Or is this just a consequence of my own educational conditioning? (For the record I think all the arguments Dijkstra gives for 0-indexing are correct. I just lack the mathematical intuition to see why the special case above appears to be one in which admission of 0 as complicates things.)