The names of birds, part 4
The European starling is a lovely looking bird, though territorial, noisy and aggressive up close. Unfortunately, they are very invasive in North America. Most of the hundreds of millions of European starlings now living in the Americas can be found fighting over my suet feeder in winter months.
Last time we said that the kestrel obeys the identity Kxy=x for all birds x and y in the forest. The starling has a slightly more complicated identity: Sxyz=xz(yz).
Again, recall that this is parenthesized ((Sx)y)z=(xz)(yz).
Yes I know I used S for the successor bird" in part 2; sorry for the confusion, this is a different bird.
If a forest contains both a starling and a kestrel, can you show that there is a bird in the forest which is fond of every bird in the forest? (Note that I'm implying here that there are at least two distinct birds in the forest, and therefore no lonely egocentric kestrel from last episode.)
Give it a try, and then scroll down.
.
.
.
.
.
.
.
Let's call K to S; the starling calls back another bird. We'll then call K to it. That calls back some other bird. We'll then call any bird z in the forest to that bird.
Sxyz=(xz)(yz)
SKKz=(Kz)(Kz)
But Kz is a bird that is fixated on z, so no matter what we call to Kz, we always get z back:
SKKz=(Kz)(Kz)=z
We call SKK the identity bird I, because Iz=z for all z in the forest. Every value is a fixpoint of the identity function bird.
(Aside: Note that SKy names the identity bird for any bird y; we didn't have to use K.)
Now that we know that any forest with both S and K in it also has I in it, can you prove that the forest also has M in it? (Recall that Mx=xx for all x.) Give it a try and then scroll down.
.
.
.
.
.
.
.
SIIz=(Iz)(Iz)=zz, so SII is M.
All this whimsey is fun of course, but I'm sure you've all realized by now that birds are more conventionally called combinators. Combinators are functions that take a single combinator and return a single combinator; forests are sets of combinators.
The study of combinatory logic is interesting for computer scientists. It turns out that there is a relatively straightforward way to take any expression made up of S and K and find an equivalent lambda calculus expression, and vice versa. Any expression in lambda calculus can be expressed as a string of S and K combinators. You can use the S and K combinators to express Booleans, numbers, arbitrary functions on integers, you name it; if a Turing machine can compute it, there's an S/K expression which can be interpreted as computing the same thing.
There's a lot more I could say about that, but I'm not going to go into the details.
Oh, and when I added lambdas to C# 3 way back in the day, the first test case I wrote to ensure the type analysis was working was something like:
delegate C C(C x);...C i = x=>x;C m = x=>x(x);C k = x=>y=>x;C s = x=>y=>z=>x(z)(y(z));
but I'm not going to discuss that further, at least not right now. We're already way off track from my series on compiling Bean Machine. Let's get back to it.
Next time on FAIC: We'll see how to use an approach inspired by combinators to build parts of a compiler, and why ensuring combinators have fixpoints is important.
If you enjoyed these puzzles, the ones that I showed are some of the introductory puzzles in To Mock A Mockingbird, which is delightful and educational, and gets as far as computability theory and Godel incompleteness. Do pick up a copy!
