Lescanne :: Deconstruction of Infinite Extensive Games Using Coinduction
- authors
- Lescanne, Pierre
- url
- http://arxiv.org/abs/0904.3528
tl;dr
Equilibria for infinite games using coinduction.
notes as I read
what is the Weierstrass function?
a counterexample of the fact that a finite sum of functions differentiable everywhere is differentiable everywhere whereas an infinite sum can be differentiable nowhere.
He's representing strategies as the whole game plus "which way to go from here?".
summary
Coinductive definitions (for extensional games):
Game := Payoff | Agent Game Game Strategy := Payoff | Left <<Agent l Strategy Strategy>> | Right <<Agent r Strategy Strategy>>
Predicates:
s2u s:Strategy a:Agent u:Utility : Pred := cases s of
| f: Payoff : s2u s a f(a) |
| Left : s2u sl a u => s2u <<a l sl sr>> u |
| Right : s2u sr a u => s2u <<a r sl sr>> u |
leads to a leaf
lleaf s: Strategy := cases s of
| f: Payoff : true |
| Left : lleaf sl => lleaf <<a l sl sr>> |
| Right : lleaf sr => lleaf <<a r sl sr>> |
alleaf s: Strategy := cases s of
| f: Payoff : true |
| <<a c sl sr>> : lleaf <<a c sl sr>> and alleaf sl and alleaf sr |
convertibility (all the strategies where all players but one are held constant):
convertible a s1 s2: Strategy :=
| leaves are equal if they are equal |
head(s1) = head(s2) = a : equal with any switched choice and convertible children |
head(s1) = head(s2) ! a : only equal with same choice and convertible children |
Nash eqbr:
(lleaf s) and (forall a: Agent s' : Strategy, (lleaf s') and (convertible a s s') , (forall u u' : Payoff, (s2u s a u) and (s2u s' a u'), u ≥ u' )).
Subgame perfect eqbr:
SGPE :=
| Payoff : true |
| Left: alleaf Left and SGPE s and SGPE sr and forall u, v, (s2u sl a u and s2u sr a v) -> u >= v |
| Right: alleaf Right and SGPE s and SGPE sr and forall u, v, (s2u sl a u and s2u sr a v) -> u <= v |