x^{xx 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 → x^{xx 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 → T^{S}. 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.

Agameis a triple (X, r, f) where X is a set ofpositions, 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 thedepthof position p. If f(p) = q, p != r, then we also say that p is acontinuationof q. A position p iswonif it has no continuations. It is afirst-player winif it is of odd depth, and asecond-player winif it is even depth. Awinning strategyfor 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.

Let F[1] denote the free ccc (cartesian closed category) on one object x. We define a (normal)typeto 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: Theholodeck gameof 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!

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.

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) -----> xProof 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 rule. 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.QEDWe 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 following.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.QEDNow 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.QEDThis 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 adirectdescription of the composition of strategies, based on this rule. We carry this out below.

© 2006 Todd H. Trimble