{-

\begin{verbatim} Time-stamp: <98/06/14 15:27:34 peter> #include "standard.half" #include "Boole.half" \end{verbatim} [ The file standard.half defines \verb| Pow |, \verb| Fam |, and other pervasive things. The file Boole.half defines singleton sets, the empty set, as well as Boolean things. ]

The problem here is to formulate the notion of (two-player) game in type theory.

Perhaps the most obvious formulation is that a game is a pair \begin{verbatim} (S,F) : sig { S : Set, F : ( s : S )-> Fam (Fam S) } \end{verbatim} where \verb| S | is the set of game states, and \verb| F | gives for a given state the family of families of states in which the game might be after a move and a counter-move. This essentially the same as the quadruple' structure used by Synek and Petersonn to parameterise the definition of their trees.

However, there is another, scarcely less obvious formulation which is more symmetric as regards the two participants.

The first bunch of definitions (an empty theory) is concerned with the asymmetric formulation, the second is concerned with the symmetric.

-}

Game1 ( S : Set )  {-  Asymmetric notion -}
= ( s : S )-> Fam (Fam S)
: Type
,
Game2 ( SW : Set, SB : Set )  {-  Symmetric notion -}
= sig { W : ( s : SW )-> Fam SB
, B : ( s : SB )-> Fam SW
}
: Type
,
{-

\section{Asymmetric}

-}

game1 ( S : Set
, G : Game1 S
)
= let
{ {-  The moves (or calls') White can make in a given state -}
B = \ s -> (G s).I
: Pow S

, {-  The counter-moves (or responses') Black can make to a given move -}
C ( s : S ) = \ b -> ((G s).g b).I
: Pow (B s)

, {-  The state we go to after a move and a counter-move -}
d ( s : S, b : B s, c : C s b )
= ((G s).g b).g c
: S

{-  Is there some way to organise the following, so one can say, -}
{-  in effect, by symmetry'? Probably not.  It is intrinsically asymmetric. -}

, {-  White's partial strategies -}
StratW ( s : S )
= data
{ $Exit {- Black escapes -} ,$Call ( b : B s           {-  sum of products (DNF) -}
, dispatch : ( response : C s b )-> StratW (d s b response) ) }
: Set

, {-  Black's partial strategies -}
StratB ( s : S )
= data
{ $Exit {- White escapes -} ,$Resp ( mem : ( b : B s )-> C s b  {-  product of sums (CNF) -}
, phi : ( b : B s )-> StratB (d s b (mem b)) ) }
: Set

, {-  The set of routes by which Black can escape a strategy of White's -}
EscapeRouteB ( s : S, str : StratW s )
= case str of
{ $Exit -> data {$nil }
, $Call b phi -> data {$cons ( hd : C s b
, tl : EscapeRouteB (d s b hd) (phi hd)
)
}
}
: Set

, {-  The set of Routes by which White can escape a strategy of Black's -}
EscapeRouteW ( s : S, str : StratB s )
= case str of
{ $Exit -> data {$nil }
, $Resp mem phi -> data {$cons ( hd : B s
, tl : EscapeRouteW (d s hd (mem hd)) (phi hd)
)
}
}
: Set

, {-  The state in which Black escapes a -}
{-  strategy of White's, by a given Route -}
EscapeStateB ( s : S, str : StratW s, p : EscapeRouteB s str )
= case str of
{ $Exit -> case p of {$nil  -> s }
, $Call b phi -> case p of {$cons hd tl -> EscapeStateB (d s b hd) (phi hd) tl }
}
: S

, {-  The state in which White escapes a -}
{-  strategy of Blacks's, by a given Route -}
EscapeStateW ( s : S, str : StratB s, tr : EscapeRouteW s str )
= case str of
{ $Exit -> case tr of {$nil  -> s }
, $Resp mem phi -> case tr of {$cons hd tl -> EscapeStateW (d s hd (mem hd)) (phi hd) tl }
}
: S

{-
Now, a couple of closure' games, in which the moves are strategies, the responses are escape routes, and the next state for a given strategy and escape route, is the escape state.

-}

,
White
= {-  A game in which the moves are partial strategies in G -}
\ s ->
struct
{ I = StratW s
, g = \ i ->
struct
{ I = EscapeRouteB s i
, g = EscapeStateB s i
}
}
: Game1 S

,
Black
= \ s ->
struct
{ I = StratB s
, g = \ i ->
struct
{ I = EscapeRouteW s i
, g = EscapeStateW s i
}
}
: Game1 S

,
{-
Thiery's notion of derivative We change the notion of state, to state with one up the spout'. The point is that Black and White are interchanged.

Any program/strategy for either participant may be made to appear as a program strategy for the other - however with a different state. The state is the original state, plus a buffer that stores a command. The calls' are now responses to the buffered command in the current state, and the responses' deposit deposit a new command in the buffer, and update the state.

However, note that derivative squared' is not the identity.

-}

Derivative
= \ sb ->
let { s = sb.p : S
, b = sb.q : B s
}
in
struct {
I = C s b,
g = \ c ->
let { s' = d s b c : S } in
struct {
I = B s',
g = \ b ->
struct { p = s', q = b } }
}
: Game1 (Sigma S B)
,
{-
There is some kind of monadic structure connected with strategies. I forget exactly how to formulate it, but in essence it amounts to a bind' operation which is composition of strategies, and a unit' strategy which consists of a single call. The formulation also involves concatenation of escape routes, and the empty escape sequence. There is some kind of two-level' feel to things. Here are bind and concat.

-}

{-  Composition of White's strategies -}
ComposeW
= \ a sock plugs ->
case sock of
{ $Exit -> plugs$nil
, $Call cmd dispatch ->$Call cmd
(\ response -> ComposeW (d a cmd response)
(dispatch response)
(\c->plugs ($cons response c))) } : ( a : S , sock : StratW a , plugs : ( c : EscapeRouteB a sock )-> StratW (EscapeStateB a sock c) )-> StratW a , {- Concatenation of Black's escape routes -} ConcatB = \ a sock plugs route1 route2 -> case sock of {$Exit
-> case route1 of { $nil -> route2 } ,$Call cmd dispatch
-> case route1 of
{ $cons response tl ->$cons response
(ConcatB (d a cmd response)
(dispatch response)
(\c->plugs ($cons response c)) tl route2) } } : ( a : S , sock : StratW a , plugs : ( c : EscapeRouteB a sock )-> StratW (EscapeStateB a sock c) , route1 : EscapeRouteB a sock , route2 : EscapeRouteB (EscapeStateB a sock route1) (plugs route1) )-> EscapeRouteB a (ComposeW a sock plugs) , {- It is straightforward enough to define a tensor product' of games. -} tensor (S' : Set, G' : Game1 S' ) = let { B' = \s'->(G' s').I : Pow S' , C' = \s' b'->((G' s').g b').I : ( s' : S' )-> Pow (B' s') , d' = \s' b' -> ((G' s').g b').g : ( s' : S', b' : B' s', c' : C' s' b')-> S' } in \s_s'-> let { s = s_s'.p : S , s' = s_s'.q : S' } in struct { I=or (B s) (B' s'), g=\iorj->case iorj of {$inl i -> struct {
I=C s i,
g=\c->struct {
p=d s i c,
q=s'}},
$inr j -> struct { I=C' s' j, g=\c'->struct { p=s, q=d' s' j c'}}}} : Game1 (and S S') {- This construction generalises from binary tensor to tensor of indexed families, I presume. Or does it! Doesn't it need a decidable equality of the index set? -} } in theory { {- nothing yet -} foo = [] : [] } : Theory , {- \newpage \section{Symmetric} -} game ( S1 : Set , S2 : Set , G : Game2 S1 S2 ) = let { M1 = \s1->(G.W s1).I : Pow S1 , M2 = \s2->(G.B s2).I : Pow S2 , M = \s-> case s of {$inl a -> M1 a
, $inr b -> M2 b } : Pow (or S1 S2) , n1 = \ s1 ->(G.W s1).g : ( s1 : S1, m1 : M1 s1 )-> S2 , n2 = \ s2 ->(G.B s2).g : ( s2 : S2, m2 : M2 s2 )-> S1 {- There must be some way to arrange this stuff so you can say by symmetry' in some way. -} , Strat1 ( s1 : S1 ) = data {$Strat1
( m1 : M1 s1
, r1 : let { s2 = n1 s1 m1 : S2 }
in ( m2 : M2 s2 )-> Strat1 (n2 s2 m2)
)
, $Leaf1 } : Set , Strat2 ( s2 : S2 ) = data {$Strat2
( m2 : M2 s2
, r2 : let { s1 = n2 s2 m2 : S1 }
in ( m1 : M1 s1 )-> Strat2 (n1 s1 m1)
)
, $Leaf2 } : Set , Str = struct { Juliette = \ s1 -> data{$A ( f : ( m1 : M1 s1 )->
Str.Romeo (n1 s1 m1) ) }
, Romeo
= \ s2 ->
data{ $E ( p : M2 s2 , q : Str.Juliette (n2 s2 p) ) } } : sig { Juliette : Pow S1 , Romeo : Pow S2 } , Escape1 ( s1 : S1, str1 : Strat1 s1 ) = case str1 of {$Strat1 m1 r1
-> let { s2 = n1 s1 m1 : S2 }
in data{ $cons ( hd : M2 s2, tl : Escape1 (n2 s2 hd) (r1 hd) ) } ,$Leaf1  -> data{ $nil } } : Set , Escape2 ( s2 : S2, str2 : Strat2 s2 ) = case str2 of {$Strat2 m2 r2
-> let { s1 = n2 s2 m2 : S1 }
in data{ $cons ( hd : M1 s1, tl : Escape2 (n1 s1 hd) (r2 hd) ) } ,$Leaf2  -> data{ \$nil }
}
: Set

, {-  There's a couple of games, in the asymmetric sense. -}
{-  Here's one.  (The other just interchanges 1 and 2. -}
G1
= struct
{ S = S1
, F = \ s1 ->
struct
{ I = M1 s1
, g = \ m1 ->
let { s2 = n1 s1 m1 : S2 }
in struct
{ I = M2 s2
, g = n2 s2
}
}
}
: sig { S : Set, F : Game1 S }
{-  related via Thiery's derivative? -}
}
in
theory
{ {-  nothing yet -}
}
: Theory