Skip to the Main Content

Note:These pages make extensive use of the latest XHTML and CSS Standards. They ought to look great in any standards-compliant modern browser. Unfortunately, they will probably look horrible in older browsers, like Netscape 4.x and IE 4.x. Moreover, many posts use MathML, which is, currently only supported in Mozilla. My best suggestion (and you will thank me when surfing an ever-increasing number of sites on the web which have been crafted to use the new standards) is to upgrade to the latest version of your browser. If that's not possible, consider moving to the Standards-compliant and open-source Mozilla browser.

January 25, 2008

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 f(g(x,y)) as a full binary tree where the nodes denote evaluation of the left child at the right, and the leaves are values:

(1) ev f ev ev y g x
(2)Figure1 :f(g(x)(y))

[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 x gets replaced with a function value x¯=(ff(x)):

(3) ev¯ ev¯ f y¯ ev x¯ g
(4)Figure2 :y¯(x¯(g))¯(f)¯

What does this evaluate to? Well,

(5) y¯(x¯(g))¯(f)¯ = f(y¯(x¯(g)))¯ = f(x¯(g)(y))¯ = f(g(x)(y))¯

As we hoped, it’s the continuization (Yoneda embedding) of the original expression. Iterating, we get

(6) ev¯¯ f¯ ev¯ ev¯ y¯ g¯ x¯
(7)Figure3 :f¯(g¯(x¯)¯(y¯)¯)¯¯

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,

(8)g¯(x¯)=x¯(g)=g(x).

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

(9)f(g(x)(y))¯¯

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!

Posted at January 25, 2008 11:36 PM UTC

TrackBack URL for this Entry:   http://golem.ph.utexas.edu/cgi-bin/MT-3.0/dxy-tb.fcgi/1580

5 Comments & 0 Trackbacks

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

ev

or

λ

So, for instance, λx.f(x) would have corresponded to

λ x ev f x.

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.

Posted by: Urs Schreiber on January 28, 2008 2:32 PM | Permalink | Reply to this

Re: The Yoneda Embedding as a Reflection

I did something very much like that in my binary encoding of lambda calculus that I called “Keraia.” It’s described in chapter 1 of my master’s thesis.

Keraia has two combinators, named 0 and 1. ’ is a prefix application operator a la Unlambda.

(1)FFB [F][B] Fϵ [0 ] B0 λccInterpret B1 λcλAAλaλBBλbcPairab

The empty string at the start of a program invokes an interpreter on the binary tree data structure constructed by the 1s. It’s at least possible under this to reflect the tree, but it doesn’t give anything very useful. Interpreting the tree doesn’t even give the same result under alpha substitution.

So I agree that it doesn’t make much sense to reflect around a lambda.

Posted by: Mike Stay on January 28, 2008 8:13 PM | Permalink | Reply to this

Re: The Yoneda Embedding as a Reflection

So I agree that it doesn’t make much sense to reflect around a lambda.

There is a beautiful would-be interpretation of

λ ev x f x

: a machine which reads in an argument, checks if it is of the form f(x) for some x, and then spits out this x.

So it’s the inverse of f! Except, of course, that it isn’t. But then, maybe we are just not being clever enough in interpreting this. Maybe each x should be read as a set of possible vales, so that the above machine would be the pre-image operation.

I don’t know. I never got anywhere with this. If you should ever do, let me know.

Posted by: Urs Schreiber on January 28, 2008 8:34 PM | Permalink | Reply to this

Re: The Yoneda Embedding as a Reflection

Hmm… That looks very much like the work of Abramsky (and Coecke?) on traced categories; I intended to getting around to understanding them after finishing this paper.

I think the idea is that if we have a morphism f:XY in a compact monoidal closed category, then we also get f *:Y *X *. Given (fg *):XX *YY *, you can precompose with the cap and compose with the cup to get a scalar, related somehow to the trace.

I think what you drew is f *.

Posted by: Mike Stay on January 28, 2008 10:15 PM | Permalink | Reply to this

Re: The Yoneda Embedding as a Reflection

What does the Yoneda embedding look like when applied to a string diagram? Composition is dual to tensor under the reflection of an application tree, so a diagram like

(1)x y z w f g h

becomes

(2) f x y h g z w

which doesn’t have an immediately obvious topological interpretation (aside from the tree reflection).

Posted by: Mike Stay on February 1, 2008 12:45 AM | Permalink | Reply to this

Post a New Comment