Interpretation games

The interpretation-game specialization of SignalingGame: receiver actions are type guesses (A = T) and both players are paid by the match indicator — conditions C1 and C2 of [Fra11]'s Theorem 1, made true by construction in InterpGame.toSignalingGame. The extra datum an interpretation game carries is the semantic meaning relation between messages and types, which drives the literal listener and the pragmatic dynamics; it does not enter the utilities.

General/specialized file split on the mathlib Kernel.Defs / Kernel.Deterministic pattern: Basic.lean states the general carrier, this file the specialization with its own ergonomic profile, connected by construction (toSignalingGame) rather than by a bridge theorem.

Main definitions

• InterpGame — meaning relation and prior; messages denote sets of types.
• InterpGame.trueStates / trueMessages — extension of a message / the messages true at a type.
• InterpGame.literal — the literal listener, uniform over the extension.
• InterpGame.toSignalingGame — Franke's C1/C2 reduction, with a Cooperative instance.

Main statements

• bestResponseSet_toSignalingGame — under matching utility the receiver's best-response set is the argmax of his beliefs: interpretation is maximum-a-posteriori estimation.

structure InterpGame (T : Type u_1) (M : Type u_2) : Type (max u_1 u_2)

An interpretation game: a semantic meaning relation between messages and types, and a prior over types. The receiver's task is to guess the sender's type; utilities are fixed by the toSignalingGame reduction.

• meaning : M → T → Prop

  Semantic meaning: is message m true at type t?

• prior : T → ℚ

  Prior probability over types.

• meaningDecidable (m : M) : DecidablePred (self.meaning m)

Extensions and the literal listener

def InterpGame.trueStates {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] (m : M) : Finset T

The extension of message m: the types at which it is true.

Equations

• G.trueStates m = Finset.filter (G.meaning m) Finset.univ

@[simp]

theorem InterpGame.mem_trueStates {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] {m : M} {t : T} : t ∈ G.trueStates m ↔ G.meaning m t

def InterpGame.literal {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype T] (m : M) (t : T) : ℚ

The literal listener: uniform over the extension of the message — the level-0 receiver of [Fra11] (eq. (73)) in its Bayesian heavy-system rendering.

Equations

• G.literal m t = if G.meaning m t then (↑(G.trueStates m).card)⁻¹ else 0

def InterpGame.trueMessages {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] (t : T) : Finset M

The messages true at type t.

Equations

• G.trueMessages t = {x : M | G.meaning x t}

@[simp]

theorem InterpGame.mem_trueMessages {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [Fintype M] {t : T} {m : M} : m ∈ G.trueMessages t ↔ G.meaning m t

The signaling-game reduction

def InterpGame.toSignalingGame {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [DecidableEq T] : SignalingGame T M T

Franke's reduction: the signaling game with actions = types (C1) and matching utility for both players (C2). The meaning relation does not enter the utilities — it constrains the dynamics (literal listener, truthful speakers), not the payoffs.

Equations

• G.toSignalingGame = { senderUtility := fun (t : T) (x : M) (a : T) => if a = t then 1 else 0, receiverUtility := fun (t : T) (x : M) (a : T) => if a = t then 1 else 0, prior := G.prior }

instance InterpGame.instCooperativeToSignalingGame {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [DecidableEq T] : G.toSignalingGame.Cooperative

Interpretation games are cooperative: C2 gives both players the same matching utility.

@[simp]

theorem InterpGame.receiverEU_toSignalingGame {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [DecidableEq T] [Fintype T] (μ : T → ℚ) (m : M) (a : T) : G.toSignalingGame.receiverEU μ m a = μ a

Under matching utility, the expected receiver utility of guessing a is exactly the belief in a.

theorem InterpGame.bestResponseSet_toSignalingGame {T : Type u_1} {M : Type u_2} (G : InterpGame T M) [DecidableEq T] [Fintype T] (μ : T → ℚ) (m : M) : G.toSignalingGame.bestResponseSet μ m = Finset.univ.argmax μ

Interpretation is MAP estimation: in an interpretation game the receiver's best responses to beliefs μ are exactly the maximum-a-posteriori types.