Iterated Best Response: Core Definitions

Game-theoretic pragmatics following @cite{franke-2011} §6-8.

Defines interpretation games (InterpGame), speaker/hearer strategies, literal listener (L₀), best response operators, IBR iteration (ibrN), fixed points, and expected gain (expectedGain).

structure RSA.IBR.InterpGame : Type 1

Interpretation game (Franke §6): states are equivalence classes over alternative truth patterns.

• State : Type

  Type of states (equivalence classes of worlds)

• Message : Type

  Type of messages (alternative utterances)

• meaning : self.Message → self.State → Bool

  Semantic meaning: is message m true at state s?

• prior : self.State → ℚ

  Prior probability over states

• stateFintype : Fintype self.State

  Fintype instances

• messageFintype : Fintype self.Message
• stateDecEq : DecidableEq self.State
• messageDecEq : DecidableEq self.Message

def RSA.IBR.InterpGame.trueStates (G : InterpGame) (m : G.Message) : Finset G.State

States where message m is true

Equations

• G.trueStates m = {s : G.State | G.meaning m s = true}

@[simp]

theorem RSA.IBR.InterpGame.mem_trueStates (G : InterpGame) {m : G.Message} {s : G.State} : s ∈ G.trueStates m ↔ G.meaning m s = true

def RSA.IBR.InterpGame.trueMessages (G : InterpGame) (s : G.State) : Finset G.Message

Messages true at state s

Equations

• G.trueMessages s = {m : G.Message | G.meaning m s = true}

@[simp]

theorem RSA.IBR.InterpGame.mem_trueMessages (G : InterpGame) {s : G.State} {m : G.Message} : m ∈ G.trueMessages s ↔ G.meaning m s = true

def RSA.IBR.InterpGame.informativity (G : InterpGame) (m : G.Message) : ℚ

Informativity of a message (reciprocal of true states, as ratio)

Equations

• G.informativity m = if (G.trueStates m).card = 0 then 0 else 1 / ↑(G.trueStates m).card

structure RSA.IBR.HearerStrategy (G : InterpGame) : Type

A hearer strategy: P(state | message)

• respond : G.Message → G.State → ℚ

structure RSA.IBR.SpeakerStrategy (G : InterpGame) : Type

A speaker strategy: P(message | state)

• choose : G.State → G.Message → ℚ

def RSA.IBR.HearerStrategy.literal (G : InterpGame) : HearerStrategy G

Uniform distribution over states where m is true

Equations

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

def RSA.IBR.HearerStrategy.support {G : InterpGame} (H : HearerStrategy G) (m : G.Message) : Finset G.State

Support of hearer's response to message m

Equations

• H.support m = {s : G.State | H.respond m s > 0}

def RSA.IBR.SpeakerStrategy.support {G : InterpGame} (S : SpeakerStrategy G) (s : G.State) : Finset G.Message

Support of speaker's choice at state s

Equations

• S.support s = {m : G.Message | S.choose s m > 0}

def RSA.IBR.SpeakerStrategy.maxUtility (G : InterpGame) (H : HearerStrategy G) (s : G.State) : ℚ

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

Equations

• RSA.IBR.SpeakerStrategy.maxUtility G H s = Finset.fold max 0 (fun (m' : G.Message) => H.respond m' s) (G.trueMessages s)

def RSA.IBR.SpeakerStrategy.optimalMessages (G : InterpGame) (H : HearerStrategy G) (s : G.State) : Finset G.Message

Optimal messages at state s: true messages achieving max utility.

This is the set-level best response (Franke eq. 76): the speaker at state t uses messages in R_k^{-1}(t) that minimize |R_k(m)|, which corresponds to maximizing H(m|t) in the probabilistic rendering.

All probability-level reasoning should go through this set.

Equations

• RSA.IBR.SpeakerStrategy.optimalMessages G H s = {m ∈ G.trueMessages s | H.respond m s = RSA.IBR.SpeakerStrategy.maxUtility G H s}

theorem RSA.IBR.SpeakerStrategy.optimalMessages_subset_trueMessages (G : InterpGame) (H : HearerStrategy G) (s : G.State) : optimalMessages G H s ⊆ G.trueMessages s

theorem RSA.IBR.SpeakerStrategy.optimalMessages_meaning (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) (hm : m ∈ optimalMessages G H s) : G.meaning m s = true

theorem RSA.IBR.SpeakerStrategy.optimalMessages_utility (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) (hm : m ∈ optimalMessages G H s) : H.respond m s = maxUtility G H s

theorem RSA.IBR.SpeakerStrategy.maxUtility_nonneg (G : InterpGame) (H : HearerStrategy G) (s : G.State) : 0 ≤ maxUtility G H s

theorem RSA.IBR.SpeakerStrategy.utility_le_maxUtility (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) (hm : m ∈ G.trueMessages s) : H.respond m s ≤ maxUtility G H s

def RSA.IBR.SpeakerStrategy.bestResponse (G : InterpGame) (H : HearerStrategy G) : SpeakerStrategy G

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

Equations

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

theorem RSA.IBR.SpeakerStrategy.bestResponse_val (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) : (bestResponse G H).choose 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 RSA.IBR.SpeakerStrategy.bestResponse_nonneg (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) : 0 ≤ (bestResponse G H).choose s m

Best response speaker always gives non-negative probabilities.

theorem RSA.IBR.SpeakerStrategy.bestResponse_false_zero (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) (hFalse : G.meaning m s = false) : (bestResponse G H).choose s m = 0

Best response speaker gives zero probability to false messages.

theorem RSA.IBR.SpeakerStrategy.bestResponse_pos_iff (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) : (bestResponse G H).choose 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 RSA.IBR.SpeakerStrategy.bestResponse_sum_le_one (G : InterpGame) (H : HearerStrategy G) (s : G.State) : ∑ m : G.Message, (bestResponse G H).choose s m ≤ 1

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

theorem RSA.IBR.SpeakerStrategy.bestResponse_le_one (G : InterpGame) (H : HearerStrategy G) (s : G.State) (m : G.Message) : (bestResponse G H).choose s m ≤ 1

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

def RSA.IBR.L0 (G : InterpGame) : HearerStrategy G

L₀: Literal listener (Franke Def. 22)

Equations

• RSA.IBR.L0 G = RSA.IBR.HearerStrategy.literal G

def RSA.IBR.speakerUpdate (G : InterpGame) (H : HearerStrategy G) : SpeakerStrategy G

Speaker update: Best response to hearer strategy.

S_{n+1}(m | s) = argmax_m L_n(s | m)

Uniform over optimal messages.

Equations

• RSA.IBR.speakerUpdate G H = RSA.IBR.SpeakerStrategy.bestResponse G H

def RSA.IBR.hearerBR (G : InterpGame) (S : SpeakerStrategy G) : HearerStrategy G

Hearer best response: argmax of posterior probability (Franke eq. 77/120).

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 RSA.IBR.hearerBR_respond_nonneg (G : InterpGame) (S : SpeakerStrategy G) (m : G.Message) (s : G.State) : (hearerBR G S).respond m s ≥ 0

hearerBR always gives non-negative response values.

def RSA.IBR.ibrStep (G : InterpGame) (H : HearerStrategy G) : HearerStrategy G

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

Equations

• RSA.IBR.ibrStep G H = RSA.IBR.hearerBR G (RSA.IBR.speakerUpdate G H)

def RSA.IBR.ibrN (G : InterpGame) (n : ℕ) : HearerStrategy G

IBR reasoning for n iterations starting from L₀

Equations

• RSA.IBR.ibrN G 0 = RSA.IBR.L0 G
• RSA.IBR.ibrN G n_2.succ = RSA.IBR.ibrStep G (RSA.IBR.ibrN G n_2)

def RSA.IBR.S1 (G : InterpGame) : SpeakerStrategy G

S₁: First pragmatic speaker

Equations

• RSA.IBR.S1 G = RSA.IBR.speakerUpdate G (RSA.IBR.L0 G)

def RSA.IBR.L2 (G : InterpGame) : HearerStrategy G

L₂: First pragmatic listener (argmax response to S₁)

Equations

• RSA.IBR.L2 G = RSA.IBR.hearerBR G (RSA.IBR.S1 G)

def RSA.IBR.isIBRFixedPoint (G : InterpGame) (H : HearerStrategy G) : Prop

Check if hearer strategy is a fixed point of IBR

Equations

• RSA.IBR.isIBRFixedPoint G H = ∀ (m : G.Message) (s : G.State), H.respond m s = (RSA.IBR.ibrStep G H).respond m s

theorem RSA.IBR.fp_respond_nonneg (G : InterpGame) (H : HearerStrategy G) (hFP : isIBRFixedPoint G H) (_hPriorNonneg : ∀ (s : G.State), G.prior s ≥ 0) (m : G.Message) (s : G.State) : H.respond m s ≥ 0

At a fixed point with non-negative priors, H.respond is non-negative.

This follows from the fact that H = ibrStep G H, and ibrStep uses hearerBR which gives non-negative values (0 or 1/k).

def RSA.IBR.pragmaticSupport (G : InterpGame) (H : HearerStrategy G) (m : G.Message) : Finset G.State

The pragmatic interpretation: support of the IBR fixed point listener

Equations

• RSA.IBR.pragmaticSupport G H m = H.support m

noncomputable def RSA.IBR.expectedGain (G : InterpGame) (S : SpeakerStrategy G) (H : HearerStrategy G) : ℚ

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

Equations

• RSA.IBR.expectedGain G S H = ∑ t : G.State, G.prior t * ∑ m : G.Message, S.choose t m * H.respond m t