\/ \/
\ /
|
Second, and much less obviously, each morphism from 1 to an object, e.g.
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.
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.
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!
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) -----> 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
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. 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
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. 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.