@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023} — Emotion Prediction as

Computation over a Generative Theory of Mind

Houlihan, Kleiman-Weiner, Hewitt, Tenenbaum & Saxe. Phil. Trans. R. Soc. A 381: 20220047.

Overview

Emotion prediction = inverse planning + computed appraisals + emotion concepts.

Module 1 (Inverse Planning): Observers infer a player's social preferences (ω_Money, ω_AIA, ω_DIA) and beliefs (π_{a₂}) from their action in a Split-or-Steal game, using Bayesian inversion of a forward planning model with Fehr-Schmidt social utility.

Module 2 (Computed Appraisals): Four appraisal types (AU, PE, CFa₁, CFa₂) computed over three utility domains (monetary, AIA, DIA) × two perspectives (base, reputational), yielding a 19-dimensional appraisal space.

Module 3 (Emotion Concepts): Each of 20 emotions is a specific sparse readout (β weights) over the shared appraisal space. The learned readout structure (Fig. 4) is unique for each emotion — a reverse-engineered computational appraisal theory.

Key Results

1. Social preferences (not just monetary) are necessary: the SOCIALLESION model (ccc = 0.663) is much worse than COMPUTEDAPPRAISALS (ccc = 0.854).
2. Inverse planning is necessary: the INVERSEPLANNINGLESION model (ccc = 0.762) can't predict why-dependent emotions (envy, gratitude).
3. Different emotions load on different utility domains: envy is specifically about DIA, guilt about reputational AIA.

File Structure

• §1. Domain-refined emotion profiles (19-dimensional, from Fig. 4)
• §2. PublicGame BToM instantiation
• §3. Structural theorems connecting emotion profiles to game features
• §4. Evaluative adjective semantics via inferred preference weights
• §5. Lesion model structure

Domain-refined profiles abstracted from Fig. 4 of @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}. Each profile specifies signs for monetary (M), affiliation/AIA (A), and social equity/DIA (E) base domains, plus reputational (R).

Convention: .positive = β > 0, .negative = β < 0, .irrelevant = β ≈ 0.

These refine the qualitative profiles in Core by decomposing the collapsed base sign into three domain-specific signs.

Positive Emotions

def HoulihanEtAl2023.joyR : Core.RefinedEmotionProfile

Joy: positive AU and PE on monetary.

Equations

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

def HoulihanEtAl2023.surpriseR : Core.RefinedEmotionProfile

Surprise: loads on |PEπ_{a₂}| — the absolute prediction error about the opponent's action. This is the paper's 19th appraisal dimension, distinct from the per-domain base PE dimensions (PE_base_{Money,AIA,DIA}). Placed in PE.reputational as the best available slot, since it concerns the social dimension (how unexpected was the opponent's choice?).

Equations

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

def HoulihanEtAl2023.prideR : Core.RefinedEmotionProfile

Pride: positive AU on monetary + reputational, positive CFa reputational.

Equations

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

def HoulihanEtAl2023.gratitudeR : Core.RefinedEmotionProfile

Gratitude: positive AU/PE on monetary, negative CFo (opponent's alternative would have been worse — opponent was kind).

Equations

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

def HoulihanEtAl2023.reliefR : Core.RefinedEmotionProfile

Relief: positive AU/PE, negative CFa (own alternative was worse).

Equations

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

def HoulihanEtAl2023.amusementR : Core.RefinedEmotionProfile

Amusement: positive AU/PE/CFo on monetary.

Equations

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

def HoulihanEtAl2023.excitementR : Core.RefinedEmotionProfile

Excitement: positive AU monetary, positive PE monetary + reputational.

Equations

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

def HoulihanEtAl2023.respectR : Core.RefinedEmotionProfile

Respect: positive AU reputational only.

Equations

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

Negative Emotions

def HoulihanEtAl2023.disappointmentR : Core.RefinedEmotionProfile

Disappointment: negative AU/PE monetary, positive CFa (agent's alternative would have been better).

Equations

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

def HoulihanEtAl2023.annoyanceR : Core.RefinedEmotionProfile

Annoyance: negative AU/PE monetary.

Equations

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

def HoulihanEtAl2023.furyR : Core.RefinedEmotionProfile

Fury: negative AU monetary + reputational, negative PE.

Equations

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

def HoulihanEtAl2023.devastationR : Core.RefinedEmotionProfile

Devastation: negative AU/PE monetary, negative CFo.

Equations

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

def HoulihanEtAl2023.disgustR : Core.RefinedEmotionProfile

Disgust: negative AU monetary + reputational.

Equations

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

Social Emotions (domain-specific)

def HoulihanEtAl2023.envyR : Core.RefinedEmotionProfile

Envy: negative AU monetary, positive CFo on DIA (social equity). The key domain-specific finding: envy is about disadvantageous inequality specifically — the opponent got more than the agent, and the opponent could have acted differently.

Equations

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

def HoulihanEtAl2023.guiltR : Core.RefinedEmotionProfile

Guilt: negative AU/CFa reputational. Purely about how the agent's choice appears to others — a reputational emotion grounded in AIA (the agent took advantage).

Equations

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

def HoulihanEtAl2023.embarrassmentR : Core.RefinedEmotionProfile

Embarrassment: negative PE/CFa reputational across all dimensions. Purely reputational — no base loadings.

Equations

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

def HoulihanEtAl2023.regretR : Core.RefinedEmotionProfile

Regret: negative AU monetary, negative CFa monetary (own alternative was better).

Equations

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

def HoulihanEtAl2023.contemptR : Core.RefinedEmotionProfile

Contempt: negative AU reputational only.

Equations

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

def HoulihanEtAl2023.sympathyR : Core.RefinedEmotionProfile

Sympathy: negative PE/CFo reputational.

Equations

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

def HoulihanEtAl2023.confusionR : Core.RefinedEmotionProfile

Confusion: positive PE monetary + reputational.

Equations

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

def HoulihanEtAl2023.allRefinedEmotions : List Core.RefinedEmotionProfile

All 20 domain-refined emotion profiles.

Equations

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

theorem HoulihanEtAl2023.twenty_refined_emotions : allRefinedEmotions.length = 20

theorem HoulihanEtAl2023.refined_profiles_distinguishable : List.Pairwise (fun (x1 x2 : Core.RefinedAppraisalWeights) => x1 ≠ x2) (List.map (fun (x : Core.RefinedEmotionProfile) => x.weights) allRefinedEmotions)

All 20 refined profiles have distinct weight matrices.

theorem HoulihanEtAl2023.all_refined_collapse : List.map (fun (x : Core.RefinedEmotionProfile) => x.toEmotionProfile) allRefinedEmotions = Core.allEmotions

All 20 refined profiles collapse to the corresponding qualitative profiles in Core. This is the single source of truth: the qualitative profiles ARE the refined profiles with domain information collapsed via DomainWeights.collapse.

These theorems connect emotion profile structure to game-theoretic features, showing that the appraisal patterns are explained by the underlying social-cognitive computations.

theorem HoulihanEtAl2023.envy_is_dia_specific : envyR.weights.cfo.base.socialEquity = Core.AppraisalSign.positive ∧ envyR.weights.cfo.base.monetary = Core.AppraisalSign.irrelevant ∧ envyR.weights.cfo.base.affiliation = Core.AppraisalSign.irrelevant

Envy's domain specificity: loads on DIA, not AIA or monetary for CFo. This distinguishes envy from disappointment (which is monetary).

theorem HoulihanEtAl2023.guilt_is_purely_reputational : guiltR.weights.au.base = HoulihanEtAl2023.D0✝ ∧ guiltR.weights.cfa.base = HoulihanEtAl2023.D0✝

Guilt's reputational character: all base dimensions irrelevant. Guilt is about how the agent's choice appears, not its material effect.

theorem HoulihanEtAl2023.gratitude_requires_opponent_counterfactual : gratitudeR.weights.cfo.base.monetary = Core.AppraisalSign.negative

Gratitude requires opponent's counterfactual: the opponent could have acted differently (CFo negative on monetary).

theorem HoulihanEtAl2023.cd_produces_di_for_envy (pot : ℚ) (hpot : 0 < pot) : (Pragmatics.GameTheory.splitOrSteal pot).di Pragmatics.GameTheory.Action2.cooperate Pragmatics.GameTheory.Action2.defect = pot

In Split-or-Steal, cooperating when opponent defects (CD) produces maximum disadvantageous inequality — the structural condition for envy.

theorem HoulihanEtAl2023.dc_produces_ai_for_guilt (pot : ℚ) (hpot : 0 < pot) : (Pragmatics.GameTheory.splitOrSteal pot).ai Pragmatics.GameTheory.Action2.defect Pragmatics.GameTheory.Action2.cooperate = pot

In Split-or-Steal, defecting when opponent cooperates (DC) produces maximum advantageous inequality — the structural condition for guilt.

@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023} validate the model via systematic lesion experiments:

1. SOCIALLESION: Remove social preferences (ω_AIA = ω_DIA = 0). Predictions degrade for social emotions (envy, guilt, gratitude, respect). ccc = 0.663 vs. full model 0.854.

2. INVERSEPLANNINGLESION: Remove inverse planning (use prior instead of posterior). Predictions degrade for intention-dependent emotions (envy, surprise, gratitude, pride, joy). ccc = 0.762.

These lesions are formalized as restrictions on the appraisal computation.

inductive HoulihanEtAl2023.Lesion : Type

A lesion zeroes out specific appraisal dimensions.

• social : Lesion
• inversePlanning : Lesion
• noCounterfactual : Lesion

@[implicit_reducible]

instance HoulihanEtAl2023.instDecidableEqLesion : DecidableEq Lesion

Equations

• HoulihanEtAl2023.instDecidableEqLesion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance HoulihanEtAl2023.instReprLesion : Repr Lesion

Equations

• HoulihanEtAl2023.instReprLesion = { reprPrec := HoulihanEtAl2023.instReprLesion.repr }

def HoulihanEtAl2023.instReprLesion.repr : Lesion → ℕ → Std.Format

Equations

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

def HoulihanEtAl2023.domainSocialLesion (d : Core.DomainWeights) : Core.DomainWeights

Apply a social lesion: zero out affiliation and socialEquity base signs.

Equations

• HoulihanEtAl2023.domainSocialLesion d = { monetary := d.monetary, affiliation := Core.AppraisalSign.irrelevant, socialEquity := Core.AppraisalSign.irrelevant }

def HoulihanEtAl2023.perspectiveSocialLesion (r : Core.RefinedPerspectiveWeights) : Core.RefinedPerspectiveWeights

Apply social lesion to a refined perspective.

Equations

• HoulihanEtAl2023.perspectiveSocialLesion r = { base := HoulihanEtAl2023.domainSocialLesion r.base, reputational := r.reputational }

def HoulihanEtAl2023.socialLesion (r : Core.RefinedAppraisalWeights) : Core.RefinedAppraisalWeights

Apply social lesion to full refined weights.

Equations

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

theorem HoulihanEtAl2023.envy_lesioned_loses_specificity : (socialLesion envyR.weights).cfo = HoulihanEtAl2023.R0✝

Under social lesion, envy's CFo becomes all-irrelevant — envy is indistinguishable from simple negative AU (≈ annoyance).

theorem HoulihanEtAl2023.guilt_lesioned_retains_reputational : (socialLesion guiltR.weights).cfa.reputational = Core.AppraisalSign.negative ∧ (socialLesion contemptR.weights).cfa.reputational = Core.AppraisalSign.irrelevant

Under social lesion, guilt retains its reputational CFa loading (distinguishing it from contempt), but loses all domain-specific base information — the lesion degrades but doesn't eliminate guilt's distinctive profile.

structure HoulihanEtAl2023.SocialValueProfile : Type

Social value profile: the three Fehr-Schmidt preference weights inferred from an agent's action via BToM inverse planning.

This IS the Desire type for the Split-or-Steal BToM instantiation: the latent variable the observer infers in Module 1.

• ωMoney : ℚ
• ωAIA : ℚ
• ωDIA : ℚ

def HoulihanEtAl2023.SocialValueProfile.evaluate (p : SocialValueProfile) (g : Pragmatics.GameTheory.SymmetricGame) (a₁ a₂ : Pragmatics.GameTheory.Action2) : ℚ

A player with SocialValueProfile evaluates a game outcome using Fehr-Schmidt social utility. This is the paper's Eq. 3.1 for a single outcome (before expectation over opponent beliefs).

Equations

• p.evaluate g a₁ a₂ = g.socialUtility a₁ a₂ p.ωMoney p.ωAIA p.ωDIA

Game→DecisionProblem bridges are defined in the SymmetricGame namespace for dot notation.

def Pragmatics.GameTheory.SymmetricGame.toDecisionProblem (g : SymmetricGame) (opponentBelief : Action2 → ℚ) : Core.DecisionTheory.DecisionProblem Action2 Action2

A symmetric game with beliefs about the opponent's action yields a material-payoff decision problem.

"Worlds" = opponent's possible actions. "Actions" = my possible actions.

Equations

• g.toDecisionProblem opponentBelief = { utility := fun (a₂ a₁ : Pragmatics.GameTheory.Action2) => g.payoff a₁ a₂, prior := opponentBelief }

def Pragmatics.GameTheory.SymmetricGame.toSocialDecisionProblem (g : SymmetricGame) (opponentBelief : Action2 → ℚ) (ωMoney ωAIA ωDIA : ℚ) : Core.DecisionTheory.DecisionProblem Action2 Action2

A symmetric game with Fehr-Schmidt social utility yields a social decision problem — the paper's Eq. 3.1 before expectation.

The preference weights (ωMoney, ωAIA, ωDIA) are the BToM Desire type for this domain: the latent variables the observer infers via inverse planning (Module 1).

Equations

• g.toSocialDecisionProblem opponentBelief ωMoney ωAIA ωDIA = { utility := fun (a₂ a₁ : Pragmatics.GameTheory.Action2) => g.socialUtility a₁ a₂ ωMoney ωAIA ωDIA, prior := opponentBelief }

theorem HoulihanEtAl2023.social_dp_uses_evaluate (g : Pragmatics.GameTheory.SymmetricGame) (π : Pragmatics.GameTheory.Action2 → ℚ) (p : SocialValueProfile) : (g.toSocialDecisionProblem π p.ωMoney p.ωAIA p.ωDIA).utility = fun (a₂ a₁ : Pragmatics.GameTheory.Action2) => p.evaluate g a₁ a₂

The social decision problem uses SocialValueProfile.evaluate as its utility function.

theorem HoulihanEtAl2023.fehrSchmidt_eq_combined3 (vSelf vOther α β : ℚ) : Core.fehrSchmidt vSelf vOther α β = RSA.CombinedUtility.combined3 1 (-α) (-β) vSelf (Core.disadvantageousInequality vSelf vOther) (Core.advantageousInequality vSelf vOther)

Fehr-Schmidt utility is a 3-component weighted sum — a special case of RSA.CombinedUtility.combined3 with negative social weights:

U_FS = 1·vSelf + (−α)·DI + (−β)·AI

This connects the social cognition infrastructure (Core) to the RSA combined utility framework (Pragmatics.RSA.Core).

@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023} show that observers infer agents' social value weights from actions. These inferred weights ground evaluative adjectives as intersective modifiers in the sense of @cite{kamp-1975}:

⟦generous person⟧ = ⟦person⟧ ∩ {x | ω_AIA(x) > θ}

The threshold θ makes them gradable (@cite{kennedy-2007}): "more generous" = higher inferred ω_AIA.

def HoulihanEtAl2023.generousAdj (θ : ℚ) : Semantics.Gradability.Classification.AdjMeaning Unit SocialValueProfile

"Generous" as an intersective adjective meaning: ⟦generous N⟧(p) = N(p) ∧ ω_AIA(p) > θ.

Equations

• HoulihanEtAl2023.generousAdj θ N x✝ p = (decide (p.ωAIA > θ) && N () p)

def HoulihanEtAl2023.fairMindedAdj (θ : ℚ) : Semantics.Gradability.Classification.AdjMeaning Unit SocialValueProfile

"Fair-minded" as an intersective adjective meaning: ⟦fair-minded N⟧(p) = N(p) ∧ ω_DIA(p) > θ.

Equations

• HoulihanEtAl2023.fairMindedAdj θ N x✝ p = (decide (p.ωDIA > θ) && N () p)

theorem HoulihanEtAl2023.generous_is_intersective (θ : ℚ) : Semantics.Gradability.Classification.isIntersective (generousAdj θ)

Evaluative adjectives grounded in BToM-inferred preferences are intersective: ⟦generous N⟧ = ⟦N⟧ ∩ {x | ω_AIA(x) > θ}.

theorem HoulihanEtAl2023.fairMinded_is_intersective (θ : ℚ) : Semantics.Gradability.Classification.isIntersective (fairMindedAdj θ)

Fair-minded is intersective.

theorem HoulihanEtAl2023.generous_selfish_exclusive (θ : ℚ) (p : SocialValueProfile) (hg : p.ωAIA > θ) (hs : p.ωMoney > θ ∧ p.ωAIA < θ ∧ p.ωDIA < θ) : False

Generous and selfish are contradictory at any threshold: generous requires ω_AIA > θ, selfish requires ω_AIA < θ.