The Yoneda Embedding as a Reflection
Posted by John Baez
Guest post by Mike Stay
In my last post I explained how the Yoneda embedding was secretly the same as the ‘continuation passing transform’. Here’s a nice pictorial way to think about it.
We can write any expression like as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:
[In the caption of figure 1, the expression is slightly different; when using trees, it’s more convenient to curry all the functions—that is, replace every comma “,” by back-to-back parens: “)(” .]
The continuation passing transform (Yoneda embedding) first reflects the tree across the vertical axis and then replaces the root and all the left children with their continuized form—a value gets replaced with a function value
What does this evaluate to? Well,
As we hoped, it’s the continuization (Yoneda embedding) of the original expression. Iterating, we get
At this point, we get an enormous simplification: we can get rid of overlines whenever the left and right branch both have them. For instance,
Actually working out the whole expression would mean lots of epicycular reductions like this one, but taking the shortcut, we just get rid of all the lines except at the root. That means that we end up with
for our final expression. However, if this expression is just part of a larger one—if what we’re calling the “root” is really the child of some other node—then the cancellation of lines on siblings applies to our “root” and its sibling, and we really do get back to where we started!
Re: The Yoneda Embedding as a Reflection
I like that. When I was young and even more naive than I am now, I wrote a Java program which handled trees like that, built from spans like that, whose top would be either
or
So, for instance, would have corresponded to
I believe I didn’t get anywhere much further with this idea, because looking at this picture made me want to understand what it would mean to have compound expressions on the left leg of a -tree. I wanted to get a notion of invertibility into the game this way, but failed horribly.