The n-Category Café

In a cartesian closed category, or CCC, we can take products of objects, and also take exponentials. For example, in the category of sets, the product $A \times B$, or

$$A B$$

for short, is the usual cartesian product of the sets $A$ and $B$, while the exponential

$$A^B$$

is the set of functions from $B$ to $A$.

We can consider an abstract sort of CCC consisting of one object $x$ and all the stuff we can build from it using the CCC axioms. This is called the free CCC on one object.

James Dolan’s great idea was to study this gadget using games. Recently he and Todd have pretty much completely worked out how. This is what Jim talked about. Todd’s notes cover the same material in a somewhat more formal way. But here I’ll give a less formal introduction, taken from "week240" of This Week’s Finds.

Let’s play a game. I have a set X in my pocket, and I’m not telling you what it is. Can you pick an element of X in a systematic way? No, of course not: you don’t have enough information. X could even be empty, in which case you’re clearly doomed! But even if it’s nonempty, if you don’t know anything about it, you can’t pick an element in a systematic way.

So, you lose.

Okay, let’s play another game. Can you pick an element of

X^X

in a systematic way? Here A^B means the set of functions from B to A. So, I’m asking if you can pick a function from X to itself in a systematic way.

Yes! You can pick the identity function! This sends each element of X to itself:

x |→ x

You don’t need to know anything about X to describe this function. X can even be empty.

So, you win.

Are there any other ways to win? No.

Now let’s play another game. Can you pick an element of

X^{( XX )}

in a systematic way?

An element in here takes functions from X to itself and turns them into elements of X. When X is the set of real numbers, people call this sort of thing a functional, so let’s use that term. A functional eats functions and spits out elements.

You can scratch your head for a while trying to dream up a systematic way to pick a functional for any set X. But, there’s no way.

So, you lose.

Let’s play another game. Can you pick an element of

(X^X)^{( XX )}

in a systematic way?

An element in here eats functions and spits out functions. When X is the set of real numbers, people often call this sort of thing an operator, so let’s use that term.

Given an unknown set X, can you pick an operator in a systematic way? Sure! You can pick the identity operator. This operator eats any function from X to itself and spits out the same function:

f |→ f

Anyway: you win.

Are there any other ways to win? Yes! There’s an operator that takes any function and spits out the identity function:

f |→ (x |→ x)

This is a bit funny-looking, but I hope you get what it means: you put in any function x |→ y, and out pops the identity function z |→ z.

This arrow notation is very powerful. It’s usually called the "lambda calculus", since when Church invented it in the 1930s, he wrote it using the Greek letter lambda instead of an arrow: instead of

x |→ y

he wrote

λ x.y

But this just makes things more confusing, so let’s not do it.

Are there more ways to win this game? Yes! There’s also a "squaring" operator that takes any function f from X to itself and "squares" it - in other words, does it twice. If we write the result as f², this operator is

f |→ f²

But, we can express this operator without using any special symbol for squaring. The function f is the same as

x |→ f(x)

so the function f² is

x |→ f(f(x))

and the squaring operator is

f |→ (x |→ f(f(x)))

This looks pretty complicated. But, it shows that our systematic way of choosing an element of

(X^X)^{( XX )}

can still be expressed using just the lambda calculus.

Now that you know "squaring" is a way to win this particular game, you’ll immediately guess a bunch of other ways: "cubing", and so on. It turns out all the winning strategies are of this form! We can list them all using the lambda calculus:

f |→ (x |→ x)

f |→ (x |→ f(x))

f |→ (x |→ f(f(x)))

f |→ (x |→ f(f(f(x))))

etc. Note that the second one is just a longer name for the identity operator. The longer name makes the pattern clear.

o far, all these methods of picking an element of (X^X)^{( XX )} for an unknown set X can be written using the lambda calculus. There are other sneakier ways. For example, there’s the operator that sends those functions that have fixed points to the identity function, and sends functions without fixed points to themselves. But from now on, to keep things simple, let’s just consider methods that can be written using the lambda calculus. By “systematic way”, that’s what we will mean.

Now let’s play another game. Can you pick an element of

X ^{( X( XX ) )}

in a systematic way?

An element in here eats functionals and spits out elements of X. So, it’s called a functionalal on X. At least that’s what Jim calls it.

If I have an unknown set in my pocket, can you pick a functionalal on this set in a systematic way?

Yes! You just need to pick a recipe that takes functionals on X and turns them into elements of X. Here’s one recipe: take any functional and evaluate it on the identity function, getting an element of x.

In lambda calculus notation, this recipe looks like this:

f |→ f(x |→ x)

Can you think of other ways to win this game? I hope so: there are infinitely many! Jim and Todd figured out a systematic way to list them all.

Now let’s play another game. Can you pick an element of

X^(X(X(XX)))

in a systematic way? The parentheses are getting a little obnoxious by now, so let’s adopt the convention that A^BC

is short for A^(BC), which lets us write the above expression as

X^XXXX

A thing in here eats functionalals and spits out elements of X, so it’s called a functionalalal.

So, can you find a functionalalal on an unknown set in some systematic way?

The answer is no: you lose.

How about picking an element of

((X^X)^(XX))^((XX)(XX))

in a systematic way? Such a thing eats operators and spits out operators, so it’s called an operatorator.

The answer is yes: there are lots of ways to win this game. The real challenge is listing them! This is the sort of question Dolan and Trimble’s work answers: for any game of this sort, it lets you list all the ways to win.

In fact, instead of moving on to functionalators, operatorals, operatoralatorals, and so on, let me just tell you trick for instantly deciding which of all these games you can win.

You just take your game, like this:

((X^X)^(XX))^((XX)(XX))

and evaluate it by setting X = 0. If you get 0, there’s no way to win. If you get 1, there’s at least one way to win.

To use this trick, you need to know that

0⁰ = 1

This is something they don’t teach in school! In analysis, X^Ycan approach anything between 0 and 1 when X and Y approach 0. So, teachers like to say 0⁰ is undefined. But X^X approaches 1 when X → 0. More importantly, in set theory, A^B stands for the set of functions from B to A, and the number of elements in this set is

|A^B| = |A|^|B|

When A and B are empty, there’s just one function from B to A, namely the identity. So, for our purposes we should define 0⁰ = 1.

Consider the case of functionals, which are elements of X^XX. If we evaluate this at X = 0 we get

0⁰⁰ = 0¹ = 0

So, there are no functionals when X is the empty set. So, you can’t pick a functional on a unknown set in a systematic way. That’s why you lose when your game evaluates to 0. It’s more interesting to prove that for games evaluating to 1, there’s a way to win.

But we’d really like to understand all the ways to win. And for this, Dolan and Trimble needed the theory of holodeck games.

In Star Trek, the "holodeck" is a virtual reality environment where you can play various games.

On the holodeck, if you regret a move you made, you can back up to any earlier point in the game and make a new move.

Actually I’m deviating from the technical specifications of the holodeck on Star Trek, as explained here:

6) Wikipedia, Holodeck, http://en.wikipedia.org/wiki/Holodeck

So, if you’re a Star Trek purist, it’s better to imagine a video game where you can save your game at any state of play, and go back to these saved games whenever you want. And, you have to imagine being so paranoid that you always save your game before making a move. This allows games to go on forever, so we only say you have a winning strategy if you can win in a finite number of moves, no matter what the other player does.

To make this completely precise, we consider two-player games where the players take turns making moves. When a player can’t make a move, they lose. Any such game can be written as a "game tree", like this:

     | \/ 
   \ | /
    \|/ 

In this example, the first player has three choices for her first move. If she picks the middle branch, the second player has one choice for his first move. Then the first player has one choice for her second move. Then the second player has no choice for his second move - so he loses.

So, in this particular example the second player has no winning strategy.

A cool thing about such a game is that we can take its game tree and turn it into an expression built from some variable X using products and exponentials. To do this, just put an X at each vertex of the tree except the root:

     X  X  X 
     |   \/ 
 X   X   X
  \  |  /
   X X X
    \|/ 

Then blow on the tree with a strong westerly wind, so strong that the branches blow away and only the X’s are left:

        X   XX
   X   X   X
  X   X   X 

This is just a way of writing an expression built from X using products and exponentials:

X^X X^XX X^XXX

Conversely, any such expression can be turned back into a tree, at least after we simplify it using these rules:

(AB)^C = A^C B^C

(A^B)^C = A^BC

For example, consider the set of operators:

(X^X)^(XX)

If we simplify this, we get

X^{X XX}

or

     X
  X X
 X

giving the tree

        X
       /
  X   X
   \ / 
    X
    |

or in other words

      /
   \ /
    |

And here’s a cool fact: if you take any expression built from X using products and exponentials, and evaluate it at X = 0, you can tell which player has a winning strategy for the game described by the corresponding tree! If you get 1, the second player has a winning strategy; if you get 0, they don’t.

It’s pretty easy to prove: try it.

But if you’ve been paying attention, you’ll have noticed something weird.

I’ve told you two ways to get a game from any expression built from X using products and exponentials. First, the game of systematically picking an element of the resulting set. Second, the game we get by turning this expression into a game tree, like I just did.

For both these games, you can decide if there’s a winning strategy by evaluating the expression at X = 0.

But are they the same game? No! One is the holodeck version of the other!

Let’s look at the familiar example of operators:

(X^X)^(XX) = X^{X XX}

This evaluates to 1 at X = 0. So, if we turn it into a tree

      /
   \ /
    |

we get a game where the second player has a winning strategy.

This game is not very exciting, but it becomes more exciting if you call it "The Lady or the Tiger". In this game, the first player has only one first move: he takes the second player to a room with two doors, corresponding to the two branches of the above tree.

Then it’s the second player’s turn.

If he opens the left door, a beautiful lady pops out and they instantly get married and live happily ever after. If he opens the right door, the first player opens a tiger cage. Then the tiger jumps out and eats the second player.

In this game, the second player has just one winning strategy: on his first move he should choose the left door.

Next look at the game of defining an element of

(X^X)^(XX) = X^{X XX}

using the lambda calculus. We’ve seen there are infinitely many many strategies for winning this:

f |→ (x |→ x)

f |→ (x |→ f(x))

f |→ (x |→ f(f(x)))

f |→ (x |→ f(f(f(x))))

and so on. These correspond to 2nd-player winning strategies for the holodeck version of The Lady or the Tiger.

What are these strategies?

One is just to play the game and win by choosing the left door.

Another is to choose the right door - and then, just when the tiger is about to eat you, back up and choose the left door!

Another is to choose the right door - and then, just when the tiger is about to eat you, back up and choose… the right door!

Then, when the tiger is about to devour you again, back up again, and this time choose the left door.

And so on: for each n, there’s a strategy where you choose the right door n times before wising up and choosing the left door.

Now, if you want a really nice math project, ponder the pattern relating all these strategies to the corresponding lambda calculus expressions:

f |→ (x |→ x)

f |→ (x |→ f(x))

f |→ (x |→ f(f(x)))

f |→ (x |→ f(f(f(x))))

etc.

Then, figure out how to prove that for any 2-person game, say:

     | \/
   \ | /
    \|/

there’s a 1-1 correspondence between winning second-person strategies for the holodeck verson of this game and ways of using the lambda calculus to define elements of the corresponding set:

X^X X^XX X^XXX

Apparently this result goes back to work of Hyland and Ong in the early 1990s. Dolan rediscovered the idea, and Trimble and he have recently worked out a new proof.

If you get stuck, first try these notes from Dolan’s talks, for some hints:

• James Dolan, Holodeck strategies and cartesian closed categories.
• James Dolan, Holodeck strategies and the lambda-calculus (a continuation of the above lecture).

Then try Trimble’s more rigorous, technical treatment, and the original paper by Hyland and Ong:

• Todd Trimble, Holodeck games and CCCs.
• Martin Hyland and C.-H. Luke Ong, On full abstraction for PCF, Information and Computation, 163 (2000), 285-408.