On Thu, Mar 10, 2022 at 4:31 AM Rob Pike <r...@golang.org> wrote: > On Thu, Mar 10, 2022 at 5:08 PM shan...@gmail.com <shane....@gmail.com> > wrote: > > > > Is this really how you want to be known? > > Sure, why not? It's a more interesting program than one might think. > > For a richer example of the foundational idea here, see the peano.go > program in the test directory in the repo. >
This is lovely. I'm thinking about the relation to other ways of defining models of numerals. For example, Church numerals are much more annoying (if logically simpler in some sense); peano.go offers a trivial predecessor function which is famously annoying for Church numerals. Finite Von Neumann ordinals are very similar - we interpret a Number as a set of all the things which can be reached from it by applying *, and then each number is the set of all smaller numerals in the right way. And infinite chains of pointers map to ordinals exactly as we might want. However this doesn't encode general sets; by definition it can only define transitive sets, so it gets you ordinals, but only ordinals and not in the larger universe. The name "peano.go" also suggests to me that it's not quite PA that we're modeling here so much as PA numerals.... what happens if we are working in a space where the Numbers might be non-standard? The functions now don't terminate, but because of Tennenbaum's Theorem, there might be very little we can do to improve on that. Thomas -- You received this message because you are subscribed to the Google Groups "golang-nuts" group. To unsubscribe from this group and stop receiving emails from it, send an email to golang-nuts+unsubscr...@googlegroups.com. To view this discussion on the web visit https://groups.google.com/d/msgid/golang-nuts/CA%2BYjuxtXQoPbia9FK-0O5z7xP0McBYCodAaPPXcuSw9REL64aQ%40mail.gmail.com.
