Holodeck Games and CCCs

Todd Trimble

October 19, 2006

These are some notes by Todd Trimble on joint work with James Dolan. This work uses games to describe the free cartesian closed category (CCC) on one object x. The "fundamental theorem" below consists of two parts. First, each object in this category corresponds to a two-player game. From the object's name, e.g.

xxx x x x x

we read off a game tree in the obvious way, like this:
                               \/ \/ 
                                \ /
Second, and much less obviously, each morphism from 1 to an object, e.g.

f: 1 → xxx x x x x

corresponds to a second-player winning strategy in a "holodeck version" of the corresponding game.

You may recall that 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. So, the "holodeck version" of a game is a new game where the second player can take back his moves.

More precisely:

Throughout the whole game, whenever it's the second player's turn, the whole game right up to this point is saved. Then he can either make a normal move or go back to any of his previously saved games and make a move starting from there.

This allows the game to go on forever. So, to make things fair, a second-player winning strategy for the holodeck game is one where he forces a win after finitely many moves.

In a CCC, every morphism from S to T can be rewritten as a morphism f: 1 → TS. So, the fundamental theorem gives a way to understand all the morphisms in the free CCC on one object.

To fully describe this CCC, one must also specify how to compose morphisms. This too can be done in terms of holodeck strategies. This result may appear in a later version of these notes.

Generalities on games and strategies

A game is a triple (X, r, f) where X is a set of positions, r is an 
initial position, and f is a function X --> X which assigns to a position 
p its previous position, such that f(r) = r [by default], and for each p in X 
there exists n such that f^n(p) = r.  The least such n >= 0  is called 
the depth of position p.  

If f(p) = q, p != r, then we also say that p is a continuation
of q.  A position p is won if it has no continuations.  It is a
first-player win if it is of odd depth, and a second-player
win if it is even depth.

A winning strategy for a game (X, r, f) is a subset S of X which 
is stable under f, with no infinite sequence of successive continuations 
in S, such that (1) if p in S is of even depth, then every continuation 
q of p is in S, and (2) if p in S is of odd depth, then there is exactly 
one continuation q of p in S.  In this case, every play-sequence in S 
eventually terminates in a second-player win. 

Clearly each game defines a tree X with root r, and winning strategies 
S of X are subtrees with root r.  If the tree is finitely branching, i.e., 
if each position has only finitely many continuations, then by Koenig's 
lemma all winning strategies S are finite subtrees. 

Holodeck Games

Let F[1] denote the free ccc (cartesian closed category) on one object x. 

We define a (normal) type to be an object  Πm  x^{T(m)}  of F[1] 
where the T(m) are normal types (from now on we drop the "normal" 
and just say "type").  This product may be empty (terminal type).  The 
primitive operations here are cartesian product and T |→ x^T,  but by 
the laws of ccc's there is a derived operation (A, B) |→ A^B  on types. 

Definition: The holodeck game of a type T is a game whose 
positions are finite sequences of types, starting with T, defined 
by recursion as follows: 

(1) The initial position is the sequence of length 1, T. 

(2) If p = (T, T1, ..., T_{2n}) is a position of even depth, where 
T_{2n} = Πm x^{T(m)},  then the continuations of p are 
(T, T1, ..., T_{2n}, T(m)). 

(3) If p = (T, T1, ..., T_{2n}, T') is a position of odd depth, where 
T' = Πm x^{T(m)},  then the continuations of p are 
(T, T1, ..., T_{2n}, T', T(m)^{T'}). 

Remark: Some of the exponents T(m) of T' may be the same as types, 
so strictly speaking we should speak of sequences where each T(m) 
refers to a specified subtype (occurrence) of T'.  We will ignore this 
nuance below.  

Notice that a won position or terminal position (T, ..., T') in the 
holodeck game Hol(T) is where T' is a terminal type! 

From Winning Strategies to Elements

For each winning strategy S of Hol(T) and position p = (T, ..., T') 
in S, we define by recursion a morphism  Mor(S, p): 1 → T'  of F[1] 
if p is of even depth, and a morphism  Mor(S, p): T' → x  if p is of odd 
depth.  In particular, we obtain a morphism Mor(S) = Mor(S, T): 1 → T, 
i.e., an element of T. 

Since there is no infinite sequence of successive continuations in S, 
we may assume by recursion that all positions q in S which come 
after p have been assigned a morphism Mor(S, q).  (We observe by 
Koenig's lemma that S is finite to begin with.) 

Let T' =  Πm x^{T(m)},  and suppose p = (T, ..., T') is of even 
depth.  Any continuation  q = (T, ..., T', T(m))  is in S;  by recursion, 
we have given morphisms  Mor(S, q): T(m) → x.  Together these 
yield a morphism 1 → Πm x^{T(m)};  we define  Mor(S, p): 1 → T' 
to be that morphism. 

If p = (T, ..., T') is of odd depth in S, the winning strategy specifies 
a continuation q = (T, ..., T', T(m)^{T'})  in S.  By recursion we are 
given  Mor(S, q): 1 → T(m)^{T'}, i.e., a morphism g: T' → T(m). 
This yields a composite 

                 <proj_m, g>                       eval
            T' -----------------> x^{T(m)} x T(m) ------> x 

and we define  Mor(S, p): T' --> x  to be that composite. 

The Fundamental Theorem

For a game G, let Strat(G) be the collection of winning strategies of G. 

Theorem: The map  

                  Mor: Strat(Hol(T)) --> hom(1, T)  
                                 S |---------> Mor(S)

is a bijection.

Lemma:  Let  T = Π_m x^{T(m)}.  Then for each h: T --> x, there
exists a unique pair  (m, g: T --> T(m))  such that h is the composite

                <proj_m, g>                       eval
            T -----------------> x^{T(m)} x T(m) -----> x

Proof of Lemma: I will rephrase the statement in terms of lambda 
calculus, starting with some preliminary comments on syntax.

Lambda terms t will come equipped with a list of distinct variables 
which are declared to be arguments of t; we write for example

                     t(x1, ..., xn).

This list includes all variables which occur freely in t, and never
any variables bound in t, but may also include some variables which 
don't occur in t at all and which implicitly refer to projection maps 
("they were projected out"). 

Our scheme for constructing lambda terms is patterned after a
deductive system of sequent proofs (cf. "Curry-Howard isomorphism")
for ccc's.  It produces lambda terms which are automatically in
eta-expanded beta-reduced form.  Ultimately one can prove a theorem
which, roughly speaking, asserts the equivalence between a
multicategory built from lambda terms [considered up to alpha
equivalence] and a multicategory based on F[1]. The crucial step is to
show how to "compose" (i.e.  perform substitutions of) lambda terms;
here one must use a beta reduction scheme [or, on the sequent proof
side, a cut-elimination scheme].  The precise details need not detain
us here.

In presenting our term construction scheme, the notation

            t(x1, ..., xn)
            t'(x'1, ..., x'n')

indicates a rule which permits us to construct the term at the bottom
from the term at the top.  The notation t(c/x) denotes the term one
gets by substituting a term c for each instance of a variable x, of the
same type as c, in t.

Here are the rules for constructing lambda terms:

x(x) is a lambda term, if x is a variable of atomic type X ("identity"). 

t(x, ..., y, z, ... w)
---------------------- "symmetry"
t(x, ..., z, y, ... w)

t(x1, ..., x_n, x_{n+1})
-------------------------------------------    "diagonal"
[t(x/x_n, x/x_{n+1})](x1, ..., x)

t(x1, ..., xn)
----------------------  "projection"
t(x1, ..., xn, x)

s(x1, ..., xm)    t(y1, ..., yn)
-----------------------------------------  "pairing"
<s, t>(x1, ..., xm, y1, ..., yn)

t(x1, ..., xn, x)
---------------------------  "binding, aka Currying"
(x |-> t)(x1, ..., xn)

t(x1, ..., xn, a)   c(y1, ..., ym)
----------------------------------------------  "evaluation"
t(f(c)/a)(x1, ..., xn, y1, ..., ym, f)

whenever the last term parses (i.e., if a is of type A and c is of
type C, then f is of type A^C).

The lemma, restated using lambda terms, says that a term t of type x,
with declared variables f_1, ..., f_n of types X^{T(1)}, ..., X^{T(n)}
respectively, is of the form t = f_k(t'), for some unique k between
1 and n and unique term t' of type T(k).

The proof is by induction on the minimum number of construction rules
required to construct a term.  The inductive step involves considering
the last rule used in the construction.

The lemma holds trivially for the identity term, x(x), x of atomic
type X.

The statement of the lemma doesn't depend on the order of declared
variables, so the inductive step is automatic if the last rule used
was symmetry.

"Diagonal": if the lemma holds for t(f1, ..., fn, f_{n+1}), i.e., if t
is of the form f_k(t_k) for some unique k and valid input term t_k,
then the lemma holds for t[f/f_n, f/f_{n+1}](f1, ..., f) 
[consider separately the cases k < n, k = n, k = n+1: it's trivial].

"Projection": if the lemma holds for  t(f1, ..., fn),  then it holds for 
the term  t(f, ..., fn, f)  [even more trivial].

We need not consider the cases of pairing and Currying, because the
term t is of atomic type X, so neither of these rules can be the last 

The only rule left to consider is evaluation:

t(f1, ..., f_{j-1}, x)        t'(f_{j+1}, ..., fn)
t[f_j(t') / x] (f1, ..., fn)

where x is of atomic type X.  By induction, the principle holds for
the first input term, so

                 t(f1, ..., f_{j-1}, x)  =  f_k(t_k)

for some unique k, t_k.  There are two cases to consider:

(a)  k < j.  Here the variable x is projected out, and therefore the 
term f_j(t')  substituted for x is also projected out, and the term 
below the bar is just (f_k(t_k))(f1, ..., fn).  Hence the lemma extends 
trivially in this case.

(b) Otherwise  t(f1, ..., f_{j-1}, x) = x, i.e., f_k = x and the 
type of t_k is empty.  After applying evaluation, we get f_j(t'), which 
is exactly what we need for the lemma to hold.  This completes the 
proof.  QED

We now show how to produce a winning strategy in Hol(T) from 
a morphism f: 1 --> T.  

Let T = Prod_m x^{T(m)}.  Given f: 1 --> T,  define  S(f, m) 
as the pair < m,  T(m) --> x >  where the second entry corresponds 
to the element 

                 f                    proj_m
             1 ---> Prod_m x^{T(m)} ---------> x^{T(m)}. 

Given  f: T --> x,  define S(f)  as the pair  < m, S(f): T --> T(m) > 
which corresponds to f via the Lemma.  

Now, given  f: 1 --> T,  let [f] be the game whose positions are finite 
sequences  (f, p1, ..., pn)  where p1 is a pair of the form S(f, m), and 
if pk is a pair (j, f_k),  then p_{k+1} is a pair of the form S(f_k, m) 
when k is even, and of the form S(f_k) if k is odd. 

For this game [f], it is clear that from any position of odd depth, 
there is a unique continuation (a unique second-player move). 
Hence, [f] will be a winning strategy of itself if we prove the 

Proposition: [f] is a finite game. 

Proof: Let t be a lambda term corresponding to f: 1 --> T,  and write [t] 
as alternative notation for [f].  The finiteness of [t] will be clear from our 
describing [t] recursively, in terms of subterms of t.  So, if T = T1 x ... x Tn 
and t = (t1, ..., tn), then [t] is the game tree obtained by identifying the 
roots of the game trees [t1], ..., [tn] to a single root.  Thus we may 
assume t is a term of type x^{T'},  where T' = Prod_{k = 1 to n} x^{T(k)}. 
Here, by the Lemma,  t = [(f1, ..., fk) |--> f_k(t_k)]  where t_k is a subterm 
of t.  In this case the game tree of [t] is obtained from the tree [t_k] 
(which has t_k as root) by adjoining an edge from t_k to the new root t. 
This completes the proof.  QED

Now we can describe the winning strategy Sigma(f) in Hol(T) which 
corresponds to a morphism f: 1 --> T.  It is the set of positions 

             (T, dom(p1), cod(p2), dom(p3), cod(p4), ...) 

where (f, p1, p2, ...)  is a position in the game [f].  It is immediate from 
the preceding proposition that sigma(f) is a winning strategy. 

Proof of Theorem: We show f |--> Sigma(f) is inverse to S |--> Mor(S). 
But the equation  Sigma(Mor(S)) = S  is obvious from the constructions, 
and the reconstruction of f from the collection of type-sequences 
Mor(Sigma(f)) is also obvious, starting from the ground level observation 
that there is a unique morphism f: 1 --> T if T is empty.  This completes 
the proof.  QED

This Theorem gives a concrete construction of the category F[1] (or of 
an equivalent category whose objects are types T = finite planar trees). 
Morphisms S --> T between types are triples (S, T, s) where s is a 
winning strategy of Hol(T^S).  Morphisms are composed according 
to the rule 

                      st = Sigma(Mor(s)Mor(t)). 

This makes it perfectly clear that composition is associative (which 
in traditional game semantics is often a thorny issue).  But it would 
be desirable to have a direct description of the composition of 
strategies, based on this rule.  We carry this out below.  

© 2006 Todd H. Trimble