The names of birds, part 1
For the next part in my Bean Machine retrospective to make sense I'll need to make a short digression. In looking back on the almost 20 years I've been blogging, it is surprising to me that I've only briefly alluded to my appreciation of combinatory logic. In the next couple of episodes, I'll do a quick introduction based on the delightful book that introduced it to me: To Mock A Mockingbird, by the late Raymond Smullyan.
Imagine a forest containing some birds, possibly finitely or infinitely many. These are unusual birds. When you call the species name of a bird in the forest to a bird in the forest, it calls one back to you. Maybe the same, maybe different, but when you tell a bird the name of a bird, it names a bird back to you. There might be a Red Capped Cardinal in the forest and when you call out Great Blue Heron to it, it calls back Belted Kingfisher.
(Photos by me; click for higher resolution.)
We will notate I called Q to P and got response R" as PQ = R. If I then called out S to R and R responded with T, we'll notate that as PQS = RS = T. We'll use parentheses in the obvious way: PQS = (PQ)S and this might be different from P(QS). The latter is I called S to Q, and then called Qs response to P. I'll use capital letters to represent specific bird names, and small letters to represent variables.
The question we're considering here is: under what circumstances will a bird call back the same name you called to it? That is, for a given bird y, under what circumstances does yx = x?
Smullyan calls birds with this relationship fondness" - that is, y is fond of x" means that yx = x. If y is fond of x then x is said to be a fixpoint" of y.
A forest is said to be compositional" if for every pair of birds (a, b) - a and b can be the same or different - there is a bird c in the forest such that cx = b(ax) for all x. That is, if we call any name x to a, and then call its response to b, we get the same result as simply calling x to c. c is the composition of call x to a, and then call that response to b.
A mockingbird is the bird M with the property that Mx = xx. That is, for any bird name x, M tells you what xs response is to its own name. (The attentive reader will note that we have not said what MM is, but at least we know from the definition that MM = MM, so give me some credit for consistency at least.)
Theorem: if a compositional forest contains a mockingbird then every bird in the forest is fond of at least one bird.
Proof: Try to prove it yourself; scroll down for the solution.
.
.
.
.
.
.
.
Let p be any bird. Let c be the bird that composes p with M. Therefore cx = p(Mx) for all x.
In particular, that's true for c, so cc = p(Mc). But Mc = cc, thus cc = p(cc), and we've found a bird that p is fond of. Since p was any bird, every bird in the forest is fond of at least one bird. Or, put another way, every bird in a compositional forest with a mockingbird has at least one fixpoint.
Next time on FAIC: we'll take a look at a few more interesting birds, and then discuss why this whimsy is relevant to compilation before getting back to Bean Machine.