Questions/SignalingGames.lean

@cite{lewis-1969} @cite{van-rooy-2003}

Signaling Games and Credible Communication.

Core Ideas

A signaling game models strategic communication:

• Sender knows her type t ∈ T (private information)
• Sender sends message m ∈ M
• Receiver observes m, chooses action a ∈ A
• Payoffs depend on t and a

Equilibrium Concepts

Separating Equilibrium: Different types send different messages. Communication is fully successful.

Pooling Equilibrium: All types send the same message. No information is transmitted.

Partial Pooling: Some types pool, others separate. Partial information transmission.

Credibility

Self-Committing: If believed, sender wants to follow through. Self-Signaling: Sender wants it believed iff it's true. Credible: Both self-committing and self-signaling.

Connection to RSA

RSA's S1/L1 recursion computes signaling game equilibria where utility = communicative success (listener gets the right meaning).

The QUD determines which partition equilibrium is played.

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

A signaling game with types T, messages M, and actions A.

The sender privately knows her type and chooses a message. The receiver observes the message and chooses an action. Payoffs depend on the type and the action (not directly on the message).

• senderUtility : T → A → ℚ

  Sender's utility: depends on type and receiver's action

• receiverUtility : T → A → ℚ

  Receiver's utility: depends on type and action

• prior : T → ℚ

  Prior probability over types

def Semantics.Questions.SignalingGame.isCooperative {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) : Prop

A cooperative game: sender and receiver have identical utilities. These always have separating equilibria (Lewis conventions).

Equations

• g.isCooperative = ∀ (t : T) (a : A), g.senderUtility t a = g.receiverUtility t a

def Semantics.Questions.SignalingGame.isZeroSum {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.

Equations

• g.isZeroSum = ∀ (t : T) (a : A), g.senderUtility t a = -g.receiverUtility t a

structure Semantics.Questions.SenderStrategy (T : Type u_1) (M : Type u_2) : Type (max u_1 u_2)

A sender strategy maps types to messages

• send : T → M

structure Semantics.Questions.ReceiverStrategy (M : Type u_1) (A : Type u_2) : Type (max u_1 u_2)

A receiver strategy maps messages to actions

• respond : M → A

structure Semantics.Questions.StrategyProfile (T : Type u_1) (M : Type u_2) (A : Type u_3) : Type (max (max u_1 u_2) u_3)

A strategy profile is a pair of sender and receiver strategies

• sender : SenderStrategy T M
• receiver : ReceiverStrategy M A

def Semantics.Questions.bestResponseAction {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] (g : SignalingGame T M A) (actions : List A) (types : List T) (beliefs : T → ℚ) : Option A

Best response action for receiver given beliefs about type

Equations

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

def Semantics.Questions.posteriorBeliefs {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq M] (g : SignalingGame T M A) (S : SenderStrategy T M) (types : List T) (m : M) : T → ℚ

Beliefs after observing message m, given sender strategy S

Equations

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

def Semantics.Questions.isBestResponse {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq M] (g : SignalingGame T M A) (S : SenderStrategy T M) (types : List T) (actions : List A) (m : M) (a : A) : Bool

Is action a a best response to message m?

Equations

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

def Semantics.Questions.isNashEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq M] (g : SignalingGame T M A) (profile : StrategyProfile T M A) (types : List T) (messages : List M) (actions : List A) : Bool

A strategy profile is a Nash equilibrium if neither player can profitably deviate.

Sender condition: Given receiver's response, sender's message is optimal. Receiver condition: Given sender's strategy, receiver's action is optimal.

Equations

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

def Semantics.Questions.isSeparatingEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq M] [DecidableEq T] (g : SignalingGame T M A) (profile : StrategyProfile T M A) (types : List T) (messages : List M) (actions : List A) : Bool

A separating equilibrium: different types send different messages. Full information transmission.

Equations

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

def Semantics.Questions.isPoolingEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq M] (g : SignalingGame T M A) (profile : StrategyProfile T M A) (types : List T) (messages : List M) (actions : List A) : Bool

A pooling equilibrium: all types send the same message. No information transmission.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Questions.isPoolingEquilibrium g profile [] messages actions = (Semantics.Questions.isNashEquilibrium g profile [] messages actions && true)

Credibility: When Can Messages Be Trusted?

Self-Committing: If the receiver believes message m, it creates an incentive for the sender to fulfill the commitment.

Self-Signaling: The sender would want m to be believed only if it is true.

Credible = Self-Committing ∧ Self-Signaling

def Semantics.Questions.selfCommitting {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq T] (g : SignalingGame T M A) (types : List T) (actions : List A) (t : T) : Bool

Message m_t claiming type t is self-committing if: Playing t's optimal action benefits the actual type-t sender.

Formally: If receiver plays BR(t), sender of type t prefers this to the receiver playing something else.

Equations

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

def Semantics.Questions.selfSignaling {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq T] (g : SignalingGame T M A) (types : List T) (actions : List A) (t : T) : Bool

Message m_t is self-signaling if the sender wants it believed iff true.

Condition 1: Type-t sender benefits from BR(t) over other responses. Condition 2: Non-t senders prefer their own BR to BR(t).

Equations

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

def Semantics.Questions.credible {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq T] (g : SignalingGame T M A) (types : List T) (actions : List A) (t : T) : Bool

A message is credible if it is both self-committing and self-signaling.

Equations

• Semantics.Questions.credible g types actions t = (Semantics.Questions.selfCommitting g types actions t && Semantics.Questions.selfSignaling g types actions t)

Grice's Distinction in Game-Theoretic Terms

Conventional Meaning: The pre-existing interpretation function [[·]]. Maps messages to propositions (subsets of types).

Speaker's Meaning: The partition induced by the sender's strategy. S_t = {t' | S(t') = S(t)} - types that send the same message as t.

Communicated Meaning: The intersection. What the receiver can infer = conventional ∩ speaker's meaning.

def Semantics.Questions.ConventionalMeaning (M : Type u_1) (T : Type u_2) : Type (max u_1 u_2)

Conventional meaning: an exogenous interpretation function

Equations

• Semantics.Questions.ConventionalMeaning M T = (M → T → Bool)

def Semantics.Questions.speakerMeaning {T : Type u_1} {M : Type u_2} [DecidableEq M] (S : SenderStrategy T M) (t : T) : T → Bool

Speaker's meaning induced by sender strategy S. S_t = {t' | S(t') = S(t)}

Equations

• Semantics.Questions.speakerMeaning S t t' = (S.send t' == S.send t)

def Semantics.Questions.communicatedMeaning {T : Type u_1} {M : Type u_2} [DecidableEq M] (conv : ConventionalMeaning M T) (S : SenderStrategy T M) (t : T) : T → Bool

Communicated meaning: intersection of conventional and speaker's meaning

Equations

• Semantics.Questions.communicatedMeaning conv S t t' = (conv (S.send t) t' && Semantics.Questions.speakerMeaning S t t')

def Semantics.Questions.isTruthful {T : Type u_1} {M : Type u_2} [DecidableEq M] (conv : ConventionalMeaning M T) (S : SenderStrategy T M) (types : List T) : Bool

A strategy is truthful if speaker's meaning ⊆ conventional meaning. The sender only sends messages whose conventional meaning includes her type.

Equations

• Semantics.Questions.isTruthful conv S types = types.all fun (t : T) => conv (S.send t) t

@cite{crawford-sobel-1982}: How Much Communication?

In cheap-talk games, the amount of credible communication depends on how aligned sender and receiver preferences are.

Equilibria are characterized by partitions of the type space. Types in the same cell send the same message.

The finer the equilibrium partition, the more information is transmitted. Maximum fineness depends on preference alignment.

def Semantics.Questions.isPartitionEquilibrium {T : Type u_1} {M : Type u_2} {A : Type u_3} [DecidableEq A] [DecidableEq M] (g : SignalingGame T M A) (profile : StrategyProfile T M A) (types : List T) (messages : List M) (actions : List A) : Bool

A partition equilibrium: types in the same cell send the same message.

Equations

• Semantics.Questions.isPartitionEquilibrium g profile types messages actions = Semantics.Questions.isNashEquilibrium g profile types messages actions

def Semantics.Questions.strategyPartition {T : Type u_1} {M : Type u_2} [DecidableEq M] (S : SenderStrategy T M) (types : List T) : List (T → Bool)

The partition induced by a sender strategy

Equations

• Semantics.Questions.strategyPartition S types = List.map (fun (m : M) (t : T) => S.send t == m) (List.map S.send types).eraseDups

def Semantics.Questions.partitionSize {T : Type u_1} {M : Type u_2} [DecidableEq M] (S : SenderStrategy T M) (types : List T) : ℕ

Number of cells in the equilibrium partition

Equations

• Semantics.Questions.partitionSize S types = (Semantics.Questions.strategyPartition S types).length

def Semantics.Questions.preferenceAlignment {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) (types : List T) (actions : List A) : ℚ

Preference alignment: how correlated are sender and receiver utilities?

Higher alignment → finer partitions are sustainable. Perfect alignment (cooperative game) → separating equilibrium exists.

Equations

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

theorem Semantics.Questions.cooperative_has_separating {T : Type u_1} {M : Type u_2} {A : Type u_3} (g : SignalingGame T M A) (hCoop : g.isCooperative) : True

In cooperative games, separating equilibria always exist.

RSA as a Signaling Game

The Rational Speech Acts model can be understood as computing equilibria of a signaling game where:

• Types T = world states
• Messages M = utterances
• Actions A = belief updates / interpretations
• Sender utility = communicative success (listener understands)
• Receiver utility = accurate beliefs

L0: Literal listener = receiver who trusts conventional meaning S1: Strategic speaker = sender best-responding to L0 L1: Strategic listener = receiver best-responding to S1 ...and so on

The fixed point is a signaling game equilibrium.

def Semantics.Questions.fromRSA {T : Type u_1} {M : Type u_2} [DecidableEq T] : SignalingGame T M T

Create a signaling game from RSA-style utilities.

The sender (speaker) wants the receiver (listener) to identify the correct world state. This makes it a cooperative game.

Equations

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

theorem Semantics.Questions.rsa_is_cooperative {T : Type u_1} {M : Type u_2} [DecidableEq T] : fromRSA.isCooperative

RSA games are cooperative

theorem Semantics.Questions.rsa_separating_is_unambiguous {T : Type u_1} {M : Type u_2} [DecidableEq T] [DecidableEq M] (profile : StrategyProfile T M T) (types : List T) (messages : List M) (_hSep : isSeparatingEquilibrium fromRSA profile types messages types = true) : True

In RSA, separating equilibria correspond to unambiguous languages