{--
Time-stamp: <98/06/24 09:17:45 peter> #include "standard.half" #include "Boole.half"
Thoughts toward a game model of type theory.
I take it that in giving a game-theoretical model, we want to interpret a closed term by a `winning strategy', where what `winning' means depends on the type. More generally, we want to interpret an open term Gamma |- a : A as something that `wins' when playing in two games, one for the hypotheses Gamma (as a product), and one for the conclusion.
I think the basic notion here is an interface across which there is some kind of asymmetric exchange, with a spontaneous participant (`client') who initiates the exchange, and a passive participant (`server') who responds. I think an interface should be modelled by a set of States, and a function I : State -> Fam (Fam State) that assigns to a state a doubly indexed family of the next states, the first index being the `stimulus', or `call', and the second the `response', or `reply'. (I like the call/response metaphor - it makes me think of a blues or work-song.)
A pair
(State : Set, I : State -> Fam (Fam State))
is (essentially) the same as a quadruple:
(State : Set, Stim : State -> Set,
Resp : ( s : State ) ->
Stim s -> Set,
next : ( s : State, c : Stim s) ->
Resp s c -> State)
Now, let me be anthropomorphic.
Imagine you are a term of type A in context Gamma. You are sitting in a box with 4 ports, SC, CC, CR, SR. You are waiting for a message to arrive on SC (Server calls) - something like "What's your canonical form?". To answer this, you may send zero or more messages on CC to your sub-contractors, who send their answers back to CR. The pair of ports (CC,CR) constitute your `client' interface to the context Gamma. Eventually, you reply back to the original request on SR.| | | | V V *----| server call |----*----| client resp |-----* | | | | +----| server resp |----+----| client call |-----+ | | | | V V
There are two interfaces here: SI = SC-SR and CI = CC-CR .
For a *single* interface (S,C,R,n), we can define 2 kinds of closure (as least fixpoints).
EA-closure:C^*(s : S) -- partial strategies for the (spontaneous) caller = 1 + Sigma (C s) (\c -> Pi (R s c) (\r -> C^* (n s c r)))
R^*(s : S, c : C^* s) -- response traces that beat c = case c of inl _ -> 1 inr (c,phi) -> Sigma (R s c) (\r -> R^* (n s c r) (phi r))
n^*(s : S, c : C^* s, r : R^* s c) -- the state in which r beats c = case c of inl _ -> s inr (s,phi) -> case r of (r,rs) -> n^* (n s c r) rs
AE-closure:
C_*(s : S) -- partial strategies for the (passive) responder = 1 + Pi (C s) (\c -> Sigma (R s c) (\r -> C_* (n s c r)))
R_*(s : S, c : C_* s) -- call traces that beat c = case c of inl _ -> 1 inr psi -> case (psi c) of (r,c') -> R_* (n s c r) c')
n_*(s : S, c : C_* s, r : R_* s c) -- the state in which r beats c = case c of inl _ -> s inr psi -> case (psi c) of (r,rs) -> n_* (n s c r) rs
I appreciate that these are a bit of an eyefull. Perhaps there is some more elegant formulation. However, the basic idea is quite simple. Consider first the caller, then the responder.
C A partial strategy for the caller in state s is a "program" in (C^* s) C of calls that will (non-classically) either force the responder into C a state in which it has no response, or exit (the "1 + " part of C^* C s). An element of (R^* s c) is a trace of responses which drive the C strategy c to an exit.Now, given this mechanism, can we define a "strategy" for the term in the box? Well, I think we can.R A partial strategy for the responder is a "program" in (C_* s) that R will respond to a stream of calls with a corresponding stream of R responses that (non-classically) either force the caller into a R state in which it has no call, or exit. Similarly, an element of R (R_* s c) is a trace of calls which drive the strategy to an exit.
Here we have 2 interface states (ss, cs). We want to express the idea: given a command on SC, you send a sequence of zero or more commands to the client (so no infinite chattering on CC-CR) When the chattering ceases (and the client state has moved on), you issue a response on SR, depending on the replies you got.
EXTREMELY tentative, only indicative, (inductive) definition
Term(SI,CI,ss,cs) = Pi (SI.C ss) (\c ->
Sigma (CI^*.C cs) (\phi ->
Pi (CI^*.R cs phi) (\crs ->
Sigma (SI.R ss c) (\r ->
Term(SI,CI,(SI.n ss c r),(CI^*.n cs phi crs) ))))
where ss : SI.S, cs : CI.S.
For any such definition, it seems to me that the first (of many..) things to check are that the copy-cat (identity) term can be defined, and that composition between terms can be defined in such a way that at least one has a category of interfaces (with states) and strategies "between" them. I have so far checked only that one can define a copy-cat strategy.
Of course, we are in frightening territory here with 2 levels of quantifier alternation. (Which can of course be "AC'd" down to 1, but with no real gain in simplicity.)
Remark: we should anyway expect 4-deep quantifiers *somewhere* in the theory of games. In the ordinary theory of transition systems we have the concept of a simulation, which is expressed with one level of alternating quantifier. An interface is really a more elaborate kind of ("IO"-)transition system, to which the notion of simulation extends, needing 2-levels of alternating quantifiers for its expression. It seems inevitable that the basic properties of games have this level of complexity. The formal similarity of the notion of term between two interactive systems and relational simulation between two interactive systems is striking. In fact, exact!)
I arrived at the above definition by thinking about Aczel's rule sets.
--}
Jun98
= theory {
{-- Official definition --}
Interface
= sig { S : Set, I : ( s : S )-> Fam (Fam S) }
: Type,
{-- Alternate definition --}
Interface'
= sig {
S : Set,
C : ( s : S )-> Set,
R : ( s : S, c : C s )-> Set,
n : ( s : S, c : C s, r : R s c )-> S }
: Type,
{-- Translating between the two definitions --}
Int' = \ A ->
struct {
S = A.S,
C = \ s -> (A.I s).I,
R = \ s c -> ((A.I s).g c).I,
n = \ s c r -> ((A.I s).g c).g r }
: ( A : Interface )-> Interface',
Int = \ A ->
struct {
S = A.S,
I = \ s ->
struct {
I = A.C s,
g = \ c -> struct { I = A.R s c, g = A.n s c } } }
: ( A : Interface' )-> Interface,
{-- Stategies for the client --}
CStrat
= \ X ->
let {
X' = Int' X
: Interface',
S = X.S
: Set,
C = X'.C
: ( s : S )-> Set,
R = X'.R
: ( s : S, c : C s )-> Set,
n = X'.n
: ( s : S, c : C s, r : R s c )-> S,
Cstar
= \ s ->
data {
$Leaf,
$Fork ( c : C s,
phi : ( r : R s c )-> Cstar (n s c r) ) }
: ( s : S )-> Set,
Rstar
= \ s cs ->
case cs of {
$Leaf -> data { $Nil },
$Fork c phi
-> data {
$Cons ( r : R s c,
rs : Rstar (n s c r) (phi r) ) } }
: ( s : S, cs : Cstar s )-> Set,
nstar
= \ s cs rs ->
case cs of {
$Leaf -> case rs of { $Nil -> s },
$Fork c phi
-> case rs of {
$Cons r rs1
-> nstar (n s c r) (phi r) rs1 } }
: ( s : S, cs : Cstar s, rs : Rstar s cs )-> S }
in Int (struct { S = S, C = Cstar, R = Rstar, n = nstar })
: ( X : Interface )-> Interface,
{-- Strategies for the server --}
SStrat
= \ X ->
let {
X' = Int' X
: Interface',
S = X.S
: Set,
C = X'.C
: ( s : S )-> Set,
R = X'.R
: ( s : S, c : C s )-> Set,
n = X'.n
: ( s : S, c : C s, r : R s c )-> S,
Crats
= \ s ->
data {
$Fael,
$Krof ( phi : ( c : C s )-> R s c,
psi : ( c : C s )-> Crats (n s c (phi c)) ) }
: ( s : S )-> Set,
Rrats
= \ s cs ->
case cs of {
$Fael -> data { $Lin },
$Krof phi psi
-> data {
$Snoc ( c : C s,
cs : Rrats (n s c (phi c))
(psi c) ) } }
: ( s : S, cs : Crats s )-> Set,
nrats
= \ s cs rs ->
case cs of {
$Fael -> case rs of { $Lin -> s },
$Krof phi psi
-> case rs of {
$Snoc c cs1
-> nrats (n s c (phi c)) (psi c)
cs1 } }
: ( s : S, cs : Crats s, rs : Rrats s cs )-> S }
in Int (struct { S = S, C = Crats, R = Rrats, n = nrats })
: ( X : Interface )-> Interface,
{--
Tentative definition for interpretation of terms.
It may be better to dump the idea that we have entirely
separate games, with different state spaces and rule sets.
Instead, maybe there is just one universal `game plan', and
we ought to think of the games given by particular states.
After all, we can always put games "side by side".
--}
Term = \ SI CI ss cs ->
let {
SI' = Int' SI
: Interface',
SS = SI.S
: Set,
SC = SI'.C
: ( a : SS )-> Set,
SR = SI'.R
: ( a : SS, b : SC a )-> Set,
Sn = SI'.n
: ( a : SS, b : SC a, c : SR a b )-> SS,
CI' = Int' (CStrat CI)
: Interface',
CS = CI'.S
: Set,
CC = CI'.C
: ( a : CS )-> Set,
CR = CI'.R
: ( a : CS, b : CC a )-> Set,
Cn = CI'.n
: ( a : CS, b : CC a, c : CR a b )-> CS }
in data {
$WhatToCallThis
( f : Pi (SC ss)
(\ c ->
Sigma (CC cs)
(\ cpg ->
Pi (CR cs cpg)
(\ crs ->
Sigma (SR ss c)
(\ r ->
Term SI CI (Sn ss c r)
(Cn cs cpg crs))))) ) }
: ( SI : Interface, CI : Interface, ss : SI.S, cs : CI.S )
-> Set,
CopyCat
= \ A s ->
$WhatToCallThis
(\ c ->
struct {
p = $Fork c (\ r -> $Leaf),
q = \ rs ->
case rs of {
$Cons r rs1
-> case rs1 of {
$Nil -> struct {
p = r,
q = CopyCat A
((Int' A).n s c r) } } } })
: ( A : Interface, s : A.S )-> Term A A s s,
{--
It seems likely this will work out, give or take a migraine.
Mind you, I have said *that* before!
--}
compose
= \ A B C as bs cs ab bc ->
case ab of {
$WhatToCallThis fab
-> $WhatToCallThis
(\ c ->
struct {
p = [ ],
q = \ crs -> struct { p = [ ], q = [ ] } }) }
: ( A : Interface,
B : Interface,
C : Interface,
as : A.S,
bs : B.S,
cs : C.S,
ab : Term A B as bs,
bc : Term B C bs cs )
-> Term A C as cs }
: Theory