Franke 2011: iterated best response dynamics

The IBR machinery of [Fra11] §6–8 over the shared interpretation-game carrier (InterpGame): best-response speaker (eq. (76)), Bayesian argmax hearer (eq. (120); the light-system argmin form eq. (77) under flat priors), the iteration ibrN, fixed points, and expected gain.

Strategies are ℚ-valued kernels as plain functions — a hearer strategy is M → T → ℚ, a speaker strategy T → M → ℚ.

Indexing note: ibrStep composes a speaker best response with a hearer best response, so ibrN tracks the even receiver subsequence R₀, R₂, R₄, … of [Fra11] — ibrN G 1 is the paper's R₂, not R₁. For the scalar games of ScalarGames.lean all receiver levels ≥ 1 coincide, so the distinction is immaterial there.

Speaker best response

def Franke2011.maxUtility {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) : ℚ

Max utility among true messages at state s (0 if no true messages).

Equations

• Franke2011.maxUtility G H s = Finset.fold max 0 (fun (m' : M) => H m' s) (G.trueMessages s)

def Franke2011.optimalMessages {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) : Finset M

Optimal messages at state s: true messages achieving max utility — the set-level best response ([Fra11] eq. (76)). All probability-level reasoning should go through this set.

Equations

• Franke2011.optimalMessages G H s = {m ∈ G.trueMessages s | H m s = Franke2011.maxUtility G H s}

theorem Franke2011.optimalMessages_subset_trueMessages {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) : optimalMessages G H s ⊆ G.trueMessages s

theorem Franke2011.optimalMessages_meaning {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) (m : M) (hm : m ∈ optimalMessages G H s) : G.meaning m s

theorem Franke2011.optimalMessages_utility {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) (m : M) (hm : m ∈ optimalMessages G H s) : H m s = maxUtility G H s

theorem Franke2011.maxUtility_nonneg {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) : 0 ≤ maxUtility G H s

theorem Franke2011.utility_le_maxUtility {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (H : M → T → ℚ) (s : T) (m : M) (hm : m ∈ G.trueMessages s) : H m s ≤ maxUtility G H s

theorem Franke2011.optimalMessages_eq_argmax {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (hH : ∀ (m' : M), 0 ≤ H m' s) : optimalMessages G H s = (G.trueMessages s).argmax fun (x : M) => H x s

For nonnegative hearer utilities, the optimal-message set is the argmax of hearer utility over the true messages — the carrier's Finset.argmax vocabulary. (Nonnegativity matters: maxUtility floors at 0, so with all-negative utilities optimalMessages is empty while the argmax set is not.)

def Franke2011.bestResponse {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) : T → M → ℚ

Best response speaker: uniform distribution over optimal messages ([Fra11] eq. (76)).

Equations

• Franke2011.bestResponse G H s m = if m ∈ Franke2011.optimalMessages G H s then have k := (Franke2011.optimalMessages G H s).card; if k = 0 then 0 else 1 / ↑k else 0

theorem Franke2011.bestResponse_val {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (m : M) : bestResponse G H s m = if m ∈ optimalMessages G H s then if (optimalMessages G H s).card = 0 then 0 else 1 / ↑(optimalMessages G H s).card else 0

bestResponse gives 1/k to optimal messages, 0 to others.

theorem Franke2011.bestResponse_nonneg {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (m : M) : 0 ≤ bestResponse G H s m

Best response speaker always gives non-negative probabilities.

theorem Franke2011.bestResponse_false_zero {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (m : M) (hFalse : ¬G.meaning m s) : bestResponse G H s m = 0

Best response speaker gives zero probability to false messages.

theorem Franke2011.bestResponse_pos_iff {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (m : M) : bestResponse G H s m > 0 ↔ m ∈ optimalMessages G H s ∧ (optimalMessages G H s).card > 0

bestResponse gives positive probability iff m is optimal (and optimal set is nonempty).

theorem Franke2011.bestResponse_sum_le_one {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) : ∑ m : M, bestResponse G H s m ≤ 1

Best response speaker probabilities sum to at most 1 at any state.

theorem Franke2011.bestResponse_le_one {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] [DecidableEq M] (H : M → T → ℚ) (s : T) (m : M) : bestResponse G H s m ≤ 1

Best response speaker gives at most probability 1 to any message.

Hearer best response and the IBR sequence

def Franke2011.hearerBR {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] (S : T → M → ℚ) : M → T → ℚ

Hearer best response: argmax of posterior probability ([Fra11] eq. (120); under flat priors it reduces to the light-system argmin form, eq. (77)).

The hearer observes m, forms posterior μ(t|m) ∝ S(t,m) · P(t), and picks the state(s) with maximum posterior probability. Uniform over ties. For surprise messages (∀ t, S(t,m) · P(t) = 0), falls back to literal interpretation per the tcp assumption.

Equations

• One or more equations did not get rendered due to their size.

theorem Franke2011.hearerBR_respond_nonneg {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] (S : T → M → ℚ) (m : M) (t : T) : hearerBR G S m t ≥ 0

hearerBR always gives non-negative response values.

def Franke2011.ibrStep {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] [Fintype M] [DecidableEq M] (H : M → T → ℚ) : M → T → ℚ

One full IBR iteration step: speaker best-responds, hearer argmax-responds.

Equations

• Franke2011.ibrStep G H = Franke2011.hearerBR G (Franke2011.bestResponse G H)

def Franke2011.ibrN {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] [Fintype M] [DecidableEq M] : ℕ → M → T → ℚ

IBR reasoning for n iterations starting from the literal listener.

Equations

• Franke2011.ibrN G 0 = G.literal
• Franke2011.ibrN G n.succ = Franke2011.ibrStep G (Franke2011.ibrN G n)

def Franke2011.isIBRFixedPoint {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] [Fintype M] [DecidableEq M] (H : M → T → ℚ) : Prop

A hearer strategy is a fixed point of the IBR step.

Equations

• Franke2011.isIBRFixedPoint G H = ∀ (m : M) (t : T), H m t = Franke2011.ibrStep G H m t

def Franke2011.expectedGain {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] [Fintype M] (S : T → M → ℚ) (H : M → T → ℚ) : ℚ

EG(S, R) = Σ_t Pr(t) × Σ_m S(t,m) × R(m,t): expected communication success.

Equations

• Franke2011.expectedGain G S H = ∑ t : T, G.prior t * ∑ m : M, S t m * H m t