Signaling games

The shared carrier for game-theoretic pragmatics ([BS18a] is the field review): a sender who privately knows her type t : T chooses a message m : M; a receiver observes m and chooses an action a : A; utilities depend on all three (the message argument carries signalling costs). Lewisian conventions ([Lew69]), games of partial information, optimal-answer models, and iterated-best-response pragmatics ([Fra11]) are all analyses of this carrier; interpretation games arise as the specialization A = T with matching utility (conditions C1/C2 of [Fra11]'s Theorem 1).

Pure strategies are plain functions (σ : T → M, ρ : M → A); mixed strategies are Kleisli arrows into PMF and live with the consumers that need them. Best responses are set-valued (Finset.argmax), which gives off-path messages the standard "unconstrained belief" reading for free: after a message no type sends, the posterior is identically zero, every action is trivially expected-utility-maximal, and the equilibrium condition constrains nothing.

Main definitions

• SignalingGame — types, messages, actions, prior, sender/receiver utility.
• SignalingGame.Cooperative / ZeroSum — alignment mixins.
• SignalingGame.posterior — Bayesian beliefs after a message under a pure sender strategy (zero off path).
• SignalingGame.bestResponseSet — receiver argmax set under given beliefs.
• SignalingGame.isNashEquilibrium, isSeparatingEquilibrium, isPoolingEquilibrium — pure-strategy equilibrium notions.

Main statements

• posterior_of_injective — under a separating (injective) sender strategy, the on-path posterior is a point mass: full information transmission.

structure SignalingGame (T : Type u_1) (M : Type u_2) (A : Type u_3) : Type (max (max u_1 u_2) u_3)

A signaling game: the sender privately knows her type and chooses a message; the receiver observes the message and chooses an action. Utilities may depend on the message (signalling costs).

• senderUtility : T → M → A → ℚ

  Sender's utility, as a function of type, sent message, and action.

• receiverUtility : T → M → A → ℚ

  Receiver's utility, as a function of type, observed message, and action.

• prior : T → ℚ

  Prior probability over types.

Alignment mixins

class SignalingGame.Cooperative {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) : Prop

A cooperative game: sender and receiver utilities coincide (Lewisian common interest, [Lew69]).

• utility_eq (t : T) (m : M) (a : A) : g.senderUtility t m a = g.receiverUtility t m a

class SignalingGame.ZeroSum {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) : Prop

A zero-sum game: utilities are opposite. No credible communication is possible.

• utility_neg (t : T) (m : M) (a : A) : g.senderUtility t m a = -g.receiverUtility t m a

Beliefs and best responses

def SignalingGame.receiverEU {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] (μ : T → ℚ) (m : M) (a : A) : ℚ

Receiver's expected utility of action a after message m, under beliefs μ over types.

Equations

• g.receiverEU μ m a = ∑ t : T, μ t * g.receiverUtility t m a

def SignalingGame.posterior {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [DecidableEq M] (σ : T → M) (m : M) (t : T) : ℚ

Bayesian beliefs over types after observing m, given the pure sender strategy σ: Pr(t)/Z on the senders of m, where Z is their total prior mass. Identically zero off path (Z = 0).

Equations

• g.posterior σ m t = if ∑ t' : T with σ t' = m, g.prior t' = 0 then 0 else if σ t = m then g.prior t / ∑ t' : T with σ t' = m, g.prior t' else 0

def SignalingGame.bestResponseSet {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [Fintype A] (μ : T → ℚ) (m : M) : Finset A

The set of receiver best responses to message m under beliefs μ: the actions maximizing expected receiver utility.

Equations

• g.bestResponseSet μ m = Finset.univ.argmax (g.receiverEU μ m)

Equilibrium

def SignalingGame.isNashEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [Fintype A] [DecidableEq M] (σ : T → M) (ρ : M → A) : Prop

Pure-strategy Nash equilibrium: at every type the sender's message is optimal given the receiver's response rule, and after every message the receiver's action is a best response to the Bayesian posterior. Off-path messages constrain nothing: the posterior is zero, so bestResponseSet is all of A.

Equations

• g.isNashEquilibrium σ ρ = ((∀ (t : T) (m' : M), g.senderUtility t m' (ρ m') ≤ g.senderUtility t (σ t) (ρ (σ t))) ∧ ∀ (m : M), ρ m ∈ g.bestResponseSet (g.posterior σ m) m)

def SignalingGame.isSeparatingEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [Fintype A] [DecidableEq M] (σ : T → M) (ρ : M → A) : Prop

Separating equilibrium: distinct types send distinct messages — full information transmission ([Lew69] signaling conventions).

Equations

• g.isSeparatingEquilibrium σ ρ = (g.isNashEquilibrium σ ρ ∧ Function.Injective σ)

def SignalingGame.isPoolingEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [Fintype A] [DecidableEq M] (σ : T → M) (ρ : M → A) : Prop

Pooling equilibrium: all types send the same message — no information transmission.

Equations

• g.isPoolingEquilibrium σ ρ = (g.isNashEquilibrium σ ρ ∧ ∀ (t t' : T), σ t = σ t')

theorem SignalingGame.posterior_of_injective {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) [Fintype T] [DecidableEq T] [DecidableEq M] (σ : T → M) (hσ : Function.Injective σ) (hprior : ∀ (t : T), 0 < g.prior t) (t : T) : g.posterior σ (σ t) = Pi.single t 1

Under an injective (separating) sender strategy with positive priors, the on-path posterior is a point mass on the actual type: separating strategies transmit full information.

Conventional vs speaker's meaning

The Gricean contrast in signaling terms ([Lew69]): conventional meaning is an exogenous interpretation function; the speaker's meaning of σ t is the cell of the partition that the sender strategy induces on types; what the receiver can infer is their intersection.

def SignalingGame.ConventionalMeaning (M : Type u_4) (T : Type u_5) : Type (max u_4 u_5)

Conventional meaning: an exogenous interpretation function from messages to propositions over types.

Equations

• SignalingGame.ConventionalMeaning M T = (M → T → Prop)

def SignalingGame.speakerMeaning {T : Type u_1} {M : Type u_2} (σ : T → M) (t : T) : T → Prop

Speaker's meaning of t's message under sender strategy σ: the types sending the same message as t.

Equations

• SignalingGame.speakerMeaning σ t t' = (σ t' = σ t)

def SignalingGame.communicatedMeaning {T : Type u_1} {M : Type u_2} (conv : ConventionalMeaning M T) (σ : T → M) (t : T) : T → Prop

Communicated meaning: what the receiver can infer, the intersection of conventional and speaker's meaning.

Equations

• SignalingGame.communicatedMeaning conv σ t t' = (conv (σ t) t' ∧ SignalingGame.speakerMeaning σ t t')

def SignalingGame.isTruthful {T : Type u_1} {M : Type u_2} (conv : ConventionalMeaning M T) (σ : T → M) : Prop

A sender strategy is truthful if every type's message conventionally includes that type.

Equations

• SignalingGame.isTruthful conv σ = ∀ (t : T), conv (σ t) t