{-
A : Set -- states of the "(chess-)board".
B : (a : A)-> Set -- gives moves available to Player in a state `a'.
C : (a : A, b : B a)-> Set
-- moves available to Opponent when
-- Player has made move `b' in state `a'.
d : (a : A, b : B a, c : C a b)-> A
-- gives the next state after `a', should
-- Player do `b', and Opponent do `c'.
The Player is active, or has the initiative
The Opponent is passive (, or has the "finishiative"?)
I find the Peterson-Synek tree families
T a = (Sigma b : B a) (Pi c : C a b) T(d a b c)
give quite nice models of winning strategies for Player in state a.
A win is a move to which the opponent has no response.
As for Opponent, his winning strategies are modelled by the trees
To a = (Pi b : B a) (Sigma c : C a b) To(d a b c)
= (Sigma phi : (Pi b : B a) C a b)
(Pi b : B a) To(d a b (phi a b))
-- ie, still a sum of products
A win for him is a response bringing the game into a state where the
Player can make no further moves.
To model not-necessarily-winning strategies, I'd put `leaves' on the trees:
T a = 1 + (Sigma b : B a)(Pi c : C a b)T (d a b c)
or T a X = X a + (Sigma b : B a)(Pi c : C a b)T (d a b c)
-- where X is a predicate on A.
or something like that. Of course, these are just winning strategies
for amended games (A, B', ..) where (eg) B' a = 1 + B a, etc.
I am looking for a category in which the objects are games in the sense above, and hom(G,G') consists of `winning strategies' for someone who is Player in G, and Opponent in G'. The identity morphism should be Abramsky's "copy-cat" strategy. My intuition is that the strategy is driven by the game in which it is Opponent - as it were demand driven.
To make a picture of the situation:
G G'
^ ^
| |
Player here Opponent here
(active) (passive)
\ /
\..strategy.. /
To give an operational description:
The Player makes a move in G'. The strategy makes zero or more `calls' through G, and eventually responds as Opponent in G'. A call in G means a pair consisting of a move and a response.
By a *winning* strategy of this `Janus-like' kind, I mean (to put it non-constructively) one that loses in G' only if it wins in G.
To put it in computer industry jargon, it is `middleware'; and correctness (winning) means perhaps that if your client tries to bust you (sue, or take you to court), you can always bust one of the subcontractors you engaged in the course of fulfilling his contract. To exaggerate, most interesting pieces of software in real life can be thought of as `middleware', and it would obviously be interesting to have a mathematical idealisation for middleware programs.
I expect that the precise definition of winning strategy will have an inductive form, vaguely like Peterson-Synek, but involving *two* quadruples (or states). I would like to see exactly how the `liveness' gets expressed in this definition -- that the strategy eventually responds in G'.
From experience, liveness is hard to get clear about.
-}
a_recent_attempt
{-
I assume a single global game. Then the objects of our
category are the states, and the morphisms are the
winning strategies for playing with a pair of given board states.
I take the "right-hand" game B in hom(A,B) to be the one in which
we are passive - the source of demand.
-}
( A : Set,
B : ( a : A )-> Set,
C : ( a : A, b : B a )-> Set,
d : ( a : A, b : B a, c : C a b )-> A )
= theory
{ {- A reliable way of writing simultaneous inductive definitions -}
X = struct
{ hom
= \ a a' ->
data { $Entry
( phi : ( b' : B a' )-> X.hom' a a' b' )
}
, hom'
= \ a a' b' ->
data { $Return
( c' : C a' b', s' : X.hom a (d a' b' c') )
, $Call
( b : B a
, phi : ( c : C a b )-> X.hom' (d a b c) a' b'
)
}
}
: sig { hom : ( a : A, a' : A )-> Set
, hom' : ( a : A, a' : A, b' : B a' )-> Set
}
, hom = X.hom : ( a : A, a' : A )-> Set
, hom' = X.hom' : ( a : A, a' : A, b' : B a' )-> Set
, HOM {- a better idea? -}
= \ a a' -> ( b' : B a' )-> X.hom' a a' b'
: ( a : A, a' : A )-> Set
, {- Strip the beaurocracy off -}
de ( a : A, a' : A, f : X.hom a a' )
= case f of { $Entry phi -> phi }
: ( b' : B a' )-> X.hom' a a' b'
, {- The copy-cat strategy. -}
id = \ a -> $Entry (\ b' ->
$Call b' (\ c ->
$Return c (id (d a b' c))))
: ( a : A )-> hom a a
, {- The copy-cat strategy, for the alternative definition -}
id' = \ a b' ->
$Call b' (\c->
$Return c ($Entry (id' (d a b' c))))
: ( a : A )-> HOM a a
, {- attempt 1 composition of strategies (incomplete) -}
compose ( a1 : A, a2 : A, a3 : A
, s12 : hom a1 a2 , s23 : hom a2 a3 )
= case s23 of {
$Entry phi
-> $Entry (\b3 ->
case phi b3 of {
$Return c3 s23'
-> $Return c3 (compose a1 a2 (d a3 b3 c3) s12 s23'),
$Call b2 phi23
-> case s12 of {
$Entry phi12
-> case phi12 b2 of {
$Return c2 s12'
-> de a1 a3
(compose a1 (d a2 b2 c2) a3
s12'
($Entry (\b'->de (d a2 b2 c2) a3 [phi23] b')))
b3,
$Call b1 phi3
-> $Call b1 (\c1->
de (d a1 b1 c1) a3
(compose (d a1 b1 c1) a2 a3 [] s23) b3)}}})} {- what goes here? -}
: hom a1 a3
, {- attempt 2 composition of strategies for HOM (incomplete) -}
compose ( a1 : A, a2 : A, a3 : A
, s12 : HOM a1 a2 , s23 : HOM a2 a3 )
= \b3->
case s23 b3 of {
$Return c3 s23'
-> $Return c3 ($Entry (\b'->
compose a1 a2 (d a3 b3 c3)
s12 (de a2 (d a3 b3 c3) s23') b')),
$Call b phi
-> case s12 b of {
$Return c' s
-> compose a1 (d a2 b c') a3
(de a1 (d a2 b c') s)
(\b'->[phi c'])
b3,
$Call b1 phi1
-> $Call b1 (\c->
compose (d a1 b1 c) a2 a3
(\b'->[phi1 c])
s23
b3)}}
: HOM a1 a3
, {- attempt no 3 incomplete -}
compose ( a1 : A, a2 : A, s12 : hom a1 a2 )
= \a3->
struct
{ c = \s23->
case s23 of {
$Entry phi
-> $Entry (\b3->
case phi b3 of {
$Return c3 s23'
-> $Return c3 ((compose a1 a2 s12 (d a3 b3 c3)).c s23'),
$Call b2 phi1
-> case s12 of {
$Entry phi2
-> case phi2 b2 of {
$Return c2 s12'
-> (compose a1 (d a2 b2 c2) s12' a3).c' [] b3,
$Call b1 phi3
-> $Call b1 (\c1->
(compose (d a1 b1 c1) a2 [] a3).c'
(de a2 a3 s23) b3)}}})}
, c'= \s23 b3->
(case s23 b3 of {
$Return c' s
-> $Return c' ((compose a1 a2 s12 (d a3 b3 c')).c s),
$Call b phi -> []})
}
: (a3 : A )->
sig { c : (s23 : hom a2 a3 )-> hom a1 a3,
c' : (s23 : (b3 : B a3)-> hom' a2 a3 b3)->
(b3 : B a3)-> hom' a1 a3 b3 }
}
: Theory
,
a_more_recent_attempt
( A : Set,
B : ( a : A )-> Set,
C : ( a : A, b : B a )-> Set,
d : ( a : A, b : B a, c : C a b )-> A )
= theory
{ X = \ a a' b' ->
data { $Return
( c' : C a' b'
, s' : (b'' : B (d a' b' c'))-> X a (d a' b' c') b''
)
, $Call
( b : B a
, phi : ( c : C a b )-> X (d a b c) a' b'
)
}
: ( a : A, a' : A, b' : B a' )-> Set
, hom ( a : A, a' : A ) = ( b : B a' )-> X a a' b
: Set
, id
= \a->\b->$Call b (\c->$Return c (id (d a b c)))
: ( a : A )-> hom a a
, compose ( a : A, a' : A, a'' : A, s : hom a a', s' : hom a' a'' )
= \b->case s' b of {
$Return c' s'1
-> $Return c' (compose a a' (d a'' b c') s s'1),
$Call b1 phi
-> case s b1 of {
$Return c' s'1
-> compose a (d a' b1 c') a'' s'1 (\b2->[phi c']) b,
$Call b2 phi1
-> $Call b2 (\c->compose (d a b2 c) a' a'' (\b3->[phi1 c]) (\b3->[phi]) b)}}
: hom a a''
}
: Theory