Social Meaning Games (@cite{burnett-2019}, Definitions 4.1–4.4)

@cite{burnett-2019}

Burnett's Social Meaning Game (SMG): a signalling game in which a speaker's variant choice conveys social information about their persona. The SMG reuses @cite{franke-2011}'s IBR machinery — the naive listener, strategic speaker, and uncovering listener are all instances of IBR reasoning applied to a social-meaning interpretation game.

Definitions

• SocialMeaningGame (Def. 4.1): prior over personae, semantic meaning (from EM field), and a social evaluation function μ
• naiveListener (Def. 4.2): L₀ = uniform over compatible personae (Franke's literal L₀, NOT Bayesian conditioning on the prior)
• strategicSpeaker (Def. 4.3): S₁ maximizes social utility μ
• uncoveringListener (Def. 4.4): L₁ = Bayes on S₁

Architectural bridge

The key design choice: toInterpGame converts any SMG into Franke's InterpGame, so SMG agents reuse the existing IBR iteration machinery. The grounding theorem naiveListener_eq_L0 verifies that this reuse is semantically correct: the SMG L₀ definition produces the same results as running Franke's L₀ on the converted game.

structure Sociolinguistics.SocialMeaningGame.SocialMeaningGame (P V : Type) [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] : Type

A Social Meaning Game (Burnett Def. 4.1): a signalling game where variant choice conveys social information.

• P: persona types (social categories the listener is trying to infer)
• V: variant types (linguistic forms the speaker chooses)
• prior: probability distribution over personae
• meaning: whether a variant is compatible with a persona (derived from the EM field: v means t iff the EM lift of v includes persona t)
• socialEval: the speaker's utility μ(t, v) — how much persona t values being associated with variant v

• prior : P → ℚ

  Prior probability over personae.

• prior_nonneg (t : P) : 0 ≤ self.prior t

  Prior is non-negative.

• meaning : V → P → Bool

  Semantic meaning: is variant v compatible with persona t?

• socialEval : P → V → ℚ

  Social evaluation: how much persona t values variant v.

def Sociolinguistics.SocialMeaningGame.SocialMeaningGame.toInterpGame {P V : Type} [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] (smg : SocialMeaningGame P V) : RSA.IBR.InterpGame

Convert a Social Meaning Game to Franke's interpretation game.

This is the key architectural bridge: SMG analysis reuses the existing IBR machinery from @cite{franke-2011} rather than reimplementing iterated best response.

The mapping:

• States = Personae (what the listener tries to infer)
• Messages = Variants (what the speaker chooses)
• meaning = SMG meaning (EM field compatibility)
• prior = SMG prior over personae

Equations

• smg.toInterpGame = { State := P, Message := V, meaning := smg.meaning, prior := smg.prior, stateFintype := inst✝³, messageFintype := inst✝², stateDecEq := inst✝¹, messageDecEq := inst✝ }

def Sociolinguistics.SocialMeaningGame.naiveListener {P V : Type} [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] (smg : SocialMeaningGame P V) (v : V) (t : P) : ℚ

The naive listener (Burnett Def. 4.2): L₀(t | v) = 1/|⟦v⟧| if ⟦v⟧(t), 0 otherwise.

This is Franke's literal L₀ — uniform over compatible types, NOT Bayesian conditioning on the prior. The prior is passed through to toInterpGame but Franke's HearerStrategy.literal ignores it, distributing probability uniformly over trueStates.

The Bayesian L₀ (L₀(t | v) ∝ Pr(t) · ⟦v⟧(t)) is what Burnett's RSA model uses (eq. 11). That prior-weighted version lives in the RSAConfig meaning function in study files (e.g., Burnett2019.lean), not here.

Equations

• Sociolinguistics.SocialMeaningGame.naiveListener smg v t = (RSA.IBR.L0 smg.toInterpGame).respond v t

theorem Sociolinguistics.SocialMeaningGame.naiveListener_eq_L0 {P V : Type} [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] (smg : SocialMeaningGame P V) : naiveListener smg = fun (v : smg.toInterpGame.Message) (t : smg.toInterpGame.State) => (RSA.IBR.L0 smg.toInterpGame).respond v t

Grounding theorem: The SMG naive listener IS Franke's L₀ applied to the converted game. True by construction.

def Sociolinguistics.SocialMeaningGame.strategicSpeaker {P V : Type} [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] (smg : SocialMeaningGame P V) (t : P) (v : V) : ℚ

The strategic speaker (simplified): S₁(v | t) ∝ μ(t, v) · ⟦v⟧(t).

This normalizes raw social evaluation scores over compatible variants, producing a closed-form rational speaker. This is a simplification of Burnett's Def. 4.3 / eq. (13), which uses soft-max over log-L₀: P_S(v | π) ∝ exp(α · ln(L₀(π | v))). The full RSA formulation with belief-based S₁ scoring lives in study files (e.g., Burnett2019.lean's RSAConfig), not here.

Unlike Franke's best-response speaker (which maximizes hearer success), the SMG speaker maximizes social utility: a persona chooses variants that make the listener more likely to infer a desirable persona.

Equations

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

def Sociolinguistics.SocialMeaningGame.uncoveringListener {P V : Type} [Fintype P] [Fintype V] [DecidableEq P] [DecidableEq V] (smg : SocialMeaningGame P V) (v : V) (t : P) : ℚ

The uncovering listener (Burnett Def. 4.4): L₁(t | v) ∝ Pr(t) · S₁(v | t).

The listener uses Bayes' rule to infer the speaker's persona from the observed variant choice, using the strategic speaker's production probabilities as the likelihood.

Equations

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

def Sociolinguistics.SocialMeaningGame.fromGroundedField {V : Type} [Fintype V] [DecidableEq V] (ps : PropertySpace) (gf : EckertMontague.GroundedField V ps) (personaeSets : Finset (Finset ps.Property)) [Fintype ↥personaeSets] [DecidableEq ↥personaeSets] (prior : ↥personaeSets → ℚ) (prior_nonneg : ∀ (t : ↥personaeSets), 0 ≤ prior t) (socialEval : ↥personaeSets → V → ℚ) : SocialMeaningGame (↥personaeSets) V

Construct a Social Meaning Game from a grounded field, prior, and social evaluation function.

The meaning function is derived from the EM field: variant v is compatible with a persona set p iff v's indexed properties are a subset of p's properties.

Equations

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