We have made some numbers and some functions for working with numbers. Also some other datatypes.
We haven’t really done so here, but sometimes when we define numbers we fuss more about how they are constructed, about what the constructors are. We say things like: “A natural number is zero or it is the successor of a natural number.” (In a Standard ML we might say: datatype nat = Zero | Succ of nat.)
So let’s try to? With the lambdas and such...
We already know what zero looks like:
We do not know that successor looks like:
It takes a number, n, as its argument. S applied to n should return a number that is one larger than n.
(Remember: The number n is a function that, if given two arguments, applies the first argument n times to the second.)
So, S takes a number, n, as its argument, and returns one of those λf.λx.-functions. Within, we do (n f x); we apply n to f and x. This should amount to applying f “n times” to x. And then we apply f to the result of (n f x), so that we should, in total, get f applied, well, “n+1 times” to x.
We can test it some and see if it looks right:
And like, that’s it, that’s our successor. It seems maybe less impressive than the addition and multiplication functions we did earlier. But like it’s pretty cool:
- We have zero-and-successor constructors. Much like the grown-ups have.
- We can, somewhat obviously, build any natural number with 0 and S. Like, we have 0, and we can totally just throw Ses at it until we have the number we really want.
- Related: We kind of don’t really have to write the λf.λx.-bit ever again. Unless we want to. Like, if we’re defining addition, say, and we stick to 0 and S, we won’t have to do the λf.λx.-bit in order to construct the result-number.
Will take a look at that last ting. But like, in later post...