EconCSLib.GameTheory.ExtensiveGame.Play

Playing a game: given strategies, compute the path and outcome.

Main definitions

• Arena.play — compute the path of states from a starting state (with fuel)
• Arena.terminalState — the terminal state reached (with fuel)

Design note

Since Arena supports infinite games, play uses fuel (max steps) to ensure termination. For finite games, sufficient fuel always reaches a terminal state.

def Arena.play (A : Arena) (choose : (s : A.State) → A.Action s) (start : A.State) (fuel : ℕ) : List A.State

Play the game for at most fuel steps, using choose to pick actions. Returns the sequence of states visited.

Equations

• A.play choose start 0 = [start]
• A.play choose start n.succ = start :: A.play choose (A.next start (choose start)) n

def Arena.finalState (A : Arena) (choose : (s : A.State) → A.Action s) (start : A.State) (fuel : ℕ) : A.State

The final state after at most fuel steps.

Equations

• A.finalState choose start 0 = start
• A.finalState choose start n.succ = A.finalState choose (A.next start (choose start)) n

theorem Arena.finalState_zero (A : Arena) (choose : (s : A.State) → A.Action s) (s : A.State) : A.finalState choose s 0 = s

theorem Arena.finalState_succ (A : Arena) (choose : (s : A.State) → A.Action s) (s : A.State) (n : ℕ) : A.finalState choose s (n + 1) = A.finalState choose (A.next s (choose s)) n

def ExtensiveGame.play {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (choose : (s : G.State) → G.Action s) (fuel : ℕ) : List G.State

Play the game from init for at most fuel steps. Requires a default action chooser for all states (including chance).

Equations

• G.play choose fuel = G.play choose G.init fuel

def ExtensiveGame.finalState {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (choose : (s : G.State) → G.Action s) (fuel : ℕ) : G.State

The final state reached from init after at most fuel steps.

Equations

• G.finalState choose fuel = G.finalState choose G.init fuel

def ExtensiveGame.finalPayoff {N : Type u_1} {U : Type u_2} (G : ExtensiveGame N U) (choose : (s : G.State) → G.Action s) (fuel : ℕ) (i : N) : U

Payoff at the final state for player i.

Equations

• G.finalPayoff choose fuel i = G.payoff (G.finalState choose fuel) i