EconCSLib.GameTheory.ExtensiveGame.Strategy

Strategies for extensive-form games built on the Arena framework.

Main definitions

• Strategy G i — a strategy for player i: choose an action at each nonterminal state they control
• StrategyProfile G — strategies for all players
• completeProfile — fill in a strategy profile with an action-selection function

def ExtensiveGame.Strategy {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (i : N) : Type (max u_3 u_4)

A strategy for player i: at each nonterminal state where i is the mover, specify which action to take.

The nonterminal premise is essential because terminal mover labels are semantically ignored by ControlledGame. In particular, a terminal state labelled some i does not create an impossible strategy coordinate.

Equations

• G.Strategy i = ((s : G.State) → G.mover s = some i → ¬G.isTerminal s → G.Action s)

def ExtensiveGame.StrategyProfile {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) : Type (max (max u_1 u_4) u_3)

A strategy profile: a strategy for each player.

Equations

• G.StrategyProfile = ((i : N) → G.Strategy i)

def ExtensiveGame.StrategyProfile.actionAt {N : Type u_1} {U : Type u_2} {G : ExtensiveGame N U} (σ : G.StrategyProfile) (s : G.State) (hnonterminal : ¬G.isTerminal s) : Option ((_ : N) × G.Action s)

Given a strategy profile, extract the action at a nonterminal player-controlled state. Returns none when the state is non-player-controlled.

Terminal states cannot be queried: their mover labels are semantically irrelevant and their action fibers are empty.

Equations

• σ.actionAt s hnonterminal = match h : G.mover s with | some i => some ⟨i, σ i s h hnonterminal⟩ | none => none