Emotion as Post-Inference Appraisal @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}

Houlihan, Kleiman-Weiner, @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023} show that emotions are not primitive mental states — they are computed from more basic cognitive variables via a three-layer architecture:

1. Inverse Planning (= BToM): observe action → infer beliefs, desires, percepts
2. Computed Appraisals: from inferred mental states, compute appraisal variables across multiple utility domains (monetary, affiliation, social equity)
3. Emotion Concepts: each emotion is a specific qualitative pattern (β weights) over the shared appraisal space — a linear readout with logistic transform

The key architectural claims:

• Appraisals are post-inference: computed FROM existing BToM posteriors without adding new latent variables to the generative model.
• The same appraisal variables are computed for all emotions; different emotions are different readout patterns (β vectors) over the shared appraisal space.
• All 20 emotion concepts are retrospective: they presuppose an observed outcome. Prospective emotions (hope, fear, dread) require different computations over uncertain future outcomes.

Appraisal Dimensions

The paper computes appraisals along four types × two perspectives:

Type	Definition	BToM Component
AU	U(outcome | preferences)	Desire marginal
PE	outcome − E[outcome | beliefs]	Belief expectation
CFa	U(agent's alternative) − U(actual)	Planning model
CFo	U(opponent's alternative) − U(actual)	Planning model

Perspective	Meaning
Base	Direct outcomes: monetary + social utility
Reputational	How the agent's choices appear to others

The paper's full model decomposes base utility into three domains (monetary, affiliation, social equity), yielding a 19-dimensional appraisal space (4 types × 3 base domains × 2 perspectives, minus some all-zero columns, plus |PE_{π_{a₂}}| for belief prediction error). Our qualitative profiles collapse these base domains into a single "base" perspective (4 types × 2 perspectives = 8 dimensions), which suffices to uniquely characterize all 20 emotion concepts.

For domain-refined profiles that distinguish monetary/AIA/DIA effects, see RefinedAppraisalWeights (§6) and the full instantiation in HoulihanEtAl2023.

inductive Core.AppraisalType : Type

The four appraisal computation types from @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}.

Each type is a different way of evaluating an outcome relative to the agent's inferred mental states:

• AU: value of actual outcome given preferences
• PE: actual outcome minus expected outcome given beliefs
• CFa: utility of agent's alternative action minus actual
• CFo: utility of opponent's alternative action minus actual

• achievedUtility : AppraisalType
• predictionError : AppraisalType
• counterfactualAgent : AppraisalType
• counterfactualOpponent : AppraisalType

@[implicit_reducible]

instance Core.instDecidableEqAppraisalType : DecidableEq AppraisalType

Equations

• Core.instDecidableEqAppraisalType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instReprAppraisalType.repr : AppraisalType → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprAppraisalType : Repr AppraisalType

Equations

• Core.instReprAppraisalType = { reprPrec := Core.instReprAppraisalType.repr }

inductive Core.AppraisalPerspective : Type

Perspective for appraisal computation.

The paper's full model has three base utility domains (monetary, affiliation, social equity) plus reputational utility. We collapse the three base domains into a single "base" perspective, capturing the key structural distinction: base appraisals evaluate direct outcomes, reputational appraisals evaluate how the agent's choices appear to others.

• base : AppraisalPerspective
• reputational : AppraisalPerspective

@[implicit_reducible]

instance Core.instDecidableEqAppraisalPerspective : DecidableEq AppraisalPerspective

Equations

• Core.instDecidableEqAppraisalPerspective x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprAppraisalPerspective : Repr AppraisalPerspective

Equations

• Core.instReprAppraisalPerspective = { reprPrec := Core.instReprAppraisalPerspective.repr }

def Core.instReprAppraisalPerspective.repr : AppraisalPerspective → ℕ → Std.Format

Equations

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

inductive Core.AppraisalSign : Type

Qualitative sign of an appraisal dimension in an emotion profile.

Rather than modeling continuous β weights, we capture the qualitative structure: whether high values of a given appraisal dimension increase the emotion (+), decrease it (−), or are irrelevant (·). Abstracted from the learned transformation in Houlihan et al.'s Fig. 4.

• positive : AppraisalSign
• negative : AppraisalSign
• irrelevant : AppraisalSign

@[implicit_reducible]

instance Core.instDecidableEqAppraisalSign : DecidableEq AppraisalSign

Equations

• Core.instDecidableEqAppraisalSign x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprAppraisalSign : Repr AppraisalSign

Equations

• Core.instReprAppraisalSign = { reprPrec := Core.instReprAppraisalSign.repr }

def Core.instReprAppraisalSign.repr : AppraisalSign → ℕ → Std.Format

Equations

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

inductive Core.TemporalOrientation : Type

Temporal orientation of an emotion.

Retrospective emotions presuppose an observed outcome and evaluate it against the agent's inferred mental states. Prospective emotions (hope, fear, dread) concern uncertain future outcomes and require expected utility computations — a fundamentally different appraisal architecture not covered by the current model.

All 20 emotion concepts in Houlihan et al. are retrospective.

• retrospective : TemporalOrientation
• prospective : TemporalOrientation

@[implicit_reducible]

instance Core.instDecidableEqTemporalOrientation : DecidableEq TemporalOrientation

Equations

• Core.instDecidableEqTemporalOrientation x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Core.instReprTemporalOrientation.repr : TemporalOrientation → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprTemporalOrientation : Repr TemporalOrientation

Equations

• Core.instReprTemporalOrientation = { reprPrec := Core.instReprTemporalOrientation.repr }

inductive Core.UtilityDomain : Type

The three base utility domains from @cite{fehr-schmidt-1999} as used in @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}.

The qualitative AppraisalPerspective.base collapses these three domains into one. For domain-refined analysis, each base appraisal has a sign for each domain. The domain matters: envy loads specifically on socialEquity (DIA), not on monetary or affiliation; guilt loads on reputational dimensions of affiliation (AIA), not monetary.

• monetary : UtilityDomain
• affiliation : UtilityDomain
• socialEquity : UtilityDomain

@[implicit_reducible]

instance Core.instDecidableEqUtilityDomain : DecidableEq UtilityDomain

Equations

• Core.instDecidableEqUtilityDomain x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Core.instReprUtilityDomain : Repr UtilityDomain

Equations

• Core.instReprUtilityDomain = { reprPrec := Core.instReprUtilityDomain.repr }

def Core.instReprUtilityDomain.repr : UtilityDomain → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instFintypeUtilityDomain : Fintype UtilityDomain

Equations

• Core.instFintypeUtilityDomain = { elems := {Core.UtilityDomain.monetary, Core.UtilityDomain.affiliation, Core.UtilityDomain.socialEquity}, complete := Core.instFintypeUtilityDomain._proof_1 }

structure Core.DomainWeights : Type

Qualitative appraisal sign for each utility domain.

This refines PerspectiveWeights.base : AppraisalSign into three domain-specific signs, capturing the paper's 19-dimensional structure.

• monetary : AppraisalSign
• affiliation : AppraisalSign
• socialEquity : AppraisalSign

def Core.instDecidableEqDomainWeights.decEq (x✝ x✝¹ : DomainWeights) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.instDecidableEqDomainWeights : DecidableEq DomainWeights

Equations

• Core.instDecidableEqDomainWeights = Core.instDecidableEqDomainWeights.decEq

def Core.instReprDomainWeights.repr : DomainWeights → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprDomainWeights : Repr DomainWeights

Equations

• Core.instReprDomainWeights = { reprPrec := Core.instReprDomainWeights.repr }

structure Core.RefinedPerspectiveWeights : Type

Refined perspective weights: three base domains + one reputational.

• base : DomainWeights
• reputational : AppraisalSign

def Core.instDecidableEqRefinedPerspectiveWeights.decEq (x✝ x✝¹ : RefinedPerspectiveWeights) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.instDecidableEqRefinedPerspectiveWeights : DecidableEq RefinedPerspectiveWeights

Equations

• Core.instDecidableEqRefinedPerspectiveWeights = Core.instDecidableEqRefinedPerspectiveWeights.decEq

@[implicit_reducible]

instance Core.instReprRefinedPerspectiveWeights : Repr RefinedPerspectiveWeights

Equations

• Core.instReprRefinedPerspectiveWeights = { reprPrec := Core.instReprRefinedPerspectiveWeights.repr }

def Core.instReprRefinedPerspectiveWeights.repr : RefinedPerspectiveWeights → ℕ → Std.Format

Equations

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

structure Core.RefinedAppraisalWeights : Type

The full domain-refined appraisal weight matrix for an emotion concept.

4 appraisal types × (3 base domains + 1 reputational) = 16 qualitative dimensions. This is the structure underlying the paper's Fig. 4.

• au : RefinedPerspectiveWeights
• pe : RefinedPerspectiveWeights
• cfa : RefinedPerspectiveWeights
• cfo : RefinedPerspectiveWeights

@[implicit_reducible]

instance Core.instDecidableEqRefinedAppraisalWeights : DecidableEq RefinedAppraisalWeights

Equations

• Core.instDecidableEqRefinedAppraisalWeights = Core.instDecidableEqRefinedAppraisalWeights.decEq

def Core.instDecidableEqRefinedAppraisalWeights.decEq (x✝ x✝¹ : RefinedAppraisalWeights) : Decidable (x✝ = x✝¹)

Equations

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

def Core.instReprRefinedAppraisalWeights.repr : RefinedAppraisalWeights → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprRefinedAppraisalWeights : Repr RefinedAppraisalWeights

Equations

• Core.instReprRefinedAppraisalWeights = { reprPrec := Core.instReprRefinedAppraisalWeights.repr }

def Core.achievedUtility {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (utility : W → D → F) (action : A) (world : W) : F

Achieved Utility from BToM desire marginals.

AU(a, w) = Σ_d P(d | a) · U(w, d)

The desire marginal P(d | a) is the observer's posterior over what the agent wanted, given the observed action. Weighting by utility U(w, d) yields the expected value of the actual outcome under the inferred desires.

This is the core post-inference property: AU is a function of the BToM posterior, not a primitive input to the model.

Equations

• Core.achievedUtility model utility action world = ∑ d : D, model.desireMarginal action d * utility world d

def Core.predictionError {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] [AddCommGroup F] (model : BToMModel F A P B D S M W) (outcome : W → F) (beliefPrediction : B → F) (action : A) (world : W) : F

Prediction Error from BToM belief expectation.

PE(a, w) = outcome(w) − E_B[prediction(b) | a]

The belief expectation is the observer's posterior-weighted average of what the agent believed would happen. The difference from the actual outcome measures surprise.

Equations

• Core.predictionError model outcome beliefPrediction action world = outcome world - model.beliefExpectation beliefPrediction action

def Core.counterfactualAppraisal {F : Type u_1} {A : Type u_2} {W : Type u_8} (utility : W → A → F) [AddCommGroup F] (actualAction altAction : A) (world : W) : F

Counterfactual Appraisal: utility difference from alternative action.

CF(a_actual, a_alt, w) = U(w, a_alt) − U(w, a_actual)

Serves as both CFa (agent counterfactual) and CFo (opponent counterfactual) depending on which agent's action space is being varied:

• CFa: altAction ranges over the focal agent's alternative actions
• CFo: altAction ranges over the opponent's alternative actions

Positive values mean the alternative would have been better.

Equations

• Core.counterfactualAppraisal utility actualAction altAction world = utility world altAction - utility world actualAction

theorem Core.au_from_btom_marginals {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (utility : W → D → F) (action : A) (world : W) : achievedUtility model utility action world = ∑ d : D, model.desireMarginal action d * utility world d

AU is a desire-marginal weighted sum — structurally post-inference.

theorem Core.pe_uses_belief_expectation {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] [AddCommGroup F] (model : BToMModel F A P B D S M W) (outcome : W → F) (beliefPrediction : B → F) (action : A) (world : W) : predictionError model outcome beliefPrediction action world = outcome world - model.beliefExpectation beliefPrediction action

PE uses beliefExpectation — structurally post-inference.

def Core.weightedCounterfactualAppraisal {F : Type u_1} [Ring F] {A : Type u_2} {W : Type u_8} (utility : W → A → F) (altProb : F) (actualAction altAction : A) (world : W) : F

Weighted counterfactual appraisal: the counterfactual utility difference weighted by the probability the agent would have chosen the alternative.

WCF(a, a', w) = P(a' | ω, a₂) · [U(w, a') − U(w, a)]

@cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023} weight CFa₁ by the probability the player would have chosen differently, given the inferred preferences and updated beliefs. This connects counterfactual appraisal (utility comparison) to counterfactual reasoning (how likely was the alternative?) — bridging counterfactualAppraisal here with the counterfactual conditional semantics in Theories.Semantics.Conditionals.Counterfactual.

Equations

• Core.weightedCounterfactualAppraisal utility altProb actualAction altAction world = altProb * (utility world altAction - utility world actualAction)

def Core.reputationalExpectation {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (desireProjection : D → F) (action : A) : F

Reputational appraisal: what an observer would infer about the agent's preferences from the observed action.

E[f(d) | a] = Σ_d P(d | a) · f(d)

This is the second-order computation in @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}: the agent anticipates what observers will infer about their desires from their action. For the agent, this IS the desireMarginal — the BToM architecture already computes exactly this. The reputational appraisal is just the desire-marginal expectation of a preference projection function (e.g., extracting the AIA weight from the desire).

Equations

• Core.reputationalExpectation model desireProjection action = ∑ d : D, model.desireMarginal action d * desireProjection d

structure Core.PerspectiveWeights : Type

Appraisal weights for a single appraisal type, split by perspective.

• base : AppraisalSign
• reputational : AppraisalSign

@[implicit_reducible]

instance Core.instDecidableEqPerspectiveWeights : DecidableEq PerspectiveWeights

Equations

• Core.instDecidableEqPerspectiveWeights = Core.instDecidableEqPerspectiveWeights.decEq

def Core.instDecidableEqPerspectiveWeights.decEq (x✝ x✝¹ : PerspectiveWeights) : Decidable (x✝ = x✝¹)

Equations

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

def Core.instReprPerspectiveWeights.repr : PerspectiveWeights → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprPerspectiveWeights : Repr PerspectiveWeights

Equations

• Core.instReprPerspectiveWeights = { reprPrec := Core.instReprPerspectiveWeights.repr }

structure Core.AppraisalWeights : Type

The 4 × 2 qualitative appraisal weight matrix for an emotion concept.

Each of the four appraisal types has a base and reputational weight, yielding 8 qualitative dimensions. This is our abstraction of the paper's full 19-dimensional learned β weight matrix (Fig. 4), collapsing monetary + affiliation + social equity into "base."

• au : PerspectiveWeights
• pe : PerspectiveWeights
• cfa : PerspectiveWeights
• cfo : PerspectiveWeights

def Core.instDecidableEqAppraisalWeights.decEq (x✝ x✝¹ : AppraisalWeights) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.instDecidableEqAppraisalWeights : DecidableEq AppraisalWeights

Equations

• Core.instDecidableEqAppraisalWeights = Core.instDecidableEqAppraisalWeights.decEq

@[implicit_reducible]

instance Core.instReprAppraisalWeights : Repr AppraisalWeights

Equations

• Core.instReprAppraisalWeights = { reprPrec := Core.instReprAppraisalWeights.repr }

def Core.instReprAppraisalWeights.repr : AppraisalWeights → ℕ → Std.Format

Equations

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

structure Core.EmotionProfile : Type

An emotion concept as a qualitative pattern over the appraisal space.

The paper's central claim: each emotion is a specific readout pattern (β weight vector) over the shared set of computed appraisals. Different emotions = different patterns over the SAME underlying variables. The readout is applied identically for all emotions (eq. 8.2):

P(e | ψ) ∝ exp(β_e · ψ + b_e) 

• name : String
• weights : AppraisalWeights
• orientation : TemporalOrientation

@[implicit_reducible]

instance Core.instDecidableEqEmotionProfile : DecidableEq EmotionProfile

Equations

• Core.instDecidableEqEmotionProfile = Core.instDecidableEqEmotionProfile.decEq

def Core.instDecidableEqEmotionProfile.decEq (x✝ x✝¹ : EmotionProfile) : Decidable (x✝ = x✝¹)

Equations

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

def Core.instReprEmotionProfile.repr : EmotionProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprEmotionProfile : Repr EmotionProfile

Equations

• Core.instReprEmotionProfile = { reprPrec := Core.instReprEmotionProfile.repr }

def Core.AppraisalWeights.getSign (w : AppraisalWeights) (t : AppraisalType) (p : AppraisalPerspective) : AppraisalSign

Look up the qualitative sign for a specific appraisal type and perspective.

Equations

• w.getSign Core.AppraisalType.achievedUtility Core.AppraisalPerspective.base = w.au.base
• w.getSign Core.AppraisalType.achievedUtility Core.AppraisalPerspective.reputational = w.au.reputational
• w.getSign Core.AppraisalType.predictionError Core.AppraisalPerspective.base = w.pe.base
• w.getSign Core.AppraisalType.predictionError Core.AppraisalPerspective.reputational = w.pe.reputational
• w.getSign Core.AppraisalType.counterfactualAgent Core.AppraisalPerspective.base = w.cfa.base
• w.getSign Core.AppraisalType.counterfactualAgent Core.AppraisalPerspective.reputational = w.cfa.reputational
• w.getSign Core.AppraisalType.counterfactualOpponent Core.AppraisalPerspective.base = w.cfo.base
• w.getSign Core.AppraisalType.counterfactualOpponent Core.AppraisalPerspective.reputational = w.cfo.reputational

def Core.EmotionProfile.isPurelyReputational (e : EmotionProfile) : Bool

All base (non-reputational) dimensions are irrelevant.

Equations

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

Qualitative profiles abstracted from the learned β weights in Houlihan et al.'s Fig. 4. Convention: .positive = β > 0 (high appraisal values increase emotion), .negative = β < 0, .irrelevant = β ≈ 0.

Each definition specifies: ⟨name, ⟨au, pe, cfa, cfo⟩, orientation⟩ where each of au, pe, cfa, cfo is ⟨base, reputational⟩.

Emotion	AU_b	AU_r	PE_b	PE_r	CFa_b	CFa_r	CFo_b	CFo_r
joy	+	·	+	·	·	·	·	·
surprise	·	·	·	+	·	·	·	·
pride	+	+	·	·	+	·	·	·
gratitude	+	·	+	·	·	·	−	·
relief	+	·	+	·	−	·	·	·
amusement	+	·	+	·	·	·	+	·
disappointment	−	·	−	·	+	·	·	·
annoyance	−	·	−	·	·	·	·	·
fury	−	−	−	·	·	·	·	·
embarrassment	·	−	·	−	·	−	·	·
regret	−	·	·	·	−	·	·	·
guilt	·	−	·	·	·	−	·	·
disgust	−	−	·	·	·	·	·	·
devastation	−	·	−	·	·	·	−	·
contempt	·	−	·	·	·	·	·	·
respect	·	+	·	·	·	·	·	·
envy	−	·	·	·	·	·	+	·
sympathy	·	·	·	−	·	·	·	−
confusion	·	·	+	+	·	·	·	·
excitement	+	·	+	+	·	·	·	·

def Core.joy : EmotionProfile

Equations

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

def Core.surprise : EmotionProfile

Surprise: loads on |PEπ_{a₂}| — how unexpected the opponent's action was. This is a distinct appraisal dimension in the paper (the 19th), not a standard base PE (monetary/AIA/DIA prediction error). We place it in PE.reputational as the best available slot, since it concerns the social dimension (opponent's choice) rather than direct material outcomes.

Equations

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

def Core.pride : EmotionProfile

Equations

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

def Core.gratitude : EmotionProfile

Equations

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

def Core.relief : EmotionProfile

Equations

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

def Core.amusement : EmotionProfile

Equations

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

def Core.disappointment : EmotionProfile

Equations

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

def Core.annoyance : EmotionProfile

Equations

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

def Core.fury : EmotionProfile

Equations

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

def Core.embarrassment : EmotionProfile

Equations

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

def Core.regret : EmotionProfile

Equations

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

def Core.guilt : EmotionProfile

Equations

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

def Core.disgust : EmotionProfile

Equations

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

def Core.devastation : EmotionProfile

Equations

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

def Core.contempt : EmotionProfile

Equations

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

def Core.respect : EmotionProfile

Equations

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

def Core.envy : EmotionProfile

Equations

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

def Core.sympathy : EmotionProfile

Equations

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

def Core.confusion : EmotionProfile

Equations

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

def Core.excitement : EmotionProfile

Equations

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

def Core.allEmotions : List EmotionProfile

All 20 emotion concepts from @cite{houlihan-kleiman-weiner-hewitt-tenenbaum-saxe-2023}.

Equations

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

theorem Core.twenty_emotions : allEmotions.length = 20

theorem Core.appraisal_patterns_distinguishable : List.Pairwise (fun (x1 x2 : AppraisalWeights) => x1 ≠ x2) (List.map (fun (x : EmotionProfile) => x.weights) allEmotions)

All 20 emotions have distinct appraisal weight patterns. This is the paper's central empirical finding (Fig. 4): "the learned appraisal structure is unique for each emotion."

theorem Core.all_retrospective : (allEmotions.all fun (x : EmotionProfile) => x.orientation == TemporalOrientation.retrospective) = true

All 20 emotions in the model are retrospective (post-outcome). The paper explicitly excludes prospective emotions: "we target retrospective emotions... and did not include prospective emotions that concern uncertain future events (e.g. hope, fear)" (p. 22).

theorem Core.embarrassment_purely_reputational : embarrassment.isPurelyReputational = true

Embarrassment is purely reputational: all base dimensions are irrelevant.

def Core.DomainWeights.collapse (d : DomainWeights) : AppraisalSign

Collapse domain-refined weights back to the qualitative abstraction.

Uses "any positive → positive, any negative → negative, else irrelevant" policy. This ensures the qualitative profiles remain compatible.

Equations

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

def Core.RefinedPerspectiveWeights.toPerspectiveWeights (r : RefinedPerspectiveWeights) : PerspectiveWeights

Collapse refined perspective weights to the qualitative abstraction.

Equations

• r.toPerspectiveWeights = { base := r.base.collapse, reputational := r.reputational }

def Core.RefinedAppraisalWeights.toAppraisalWeights (r : RefinedAppraisalWeights) : AppraisalWeights

Collapse a full refined weight matrix to the qualitative abstraction.

Equations

• r.toAppraisalWeights = { au := r.au.toPerspectiveWeights, pe := r.pe.toPerspectiveWeights, cfa := r.cfa.toPerspectiveWeights, cfo := r.cfo.toPerspectiveWeights }

structure Core.RefinedEmotionProfile : Type

An emotion concept with domain-refined appraisal weights.

• name : String
• weights : RefinedAppraisalWeights
• orientation : TemporalOrientation

def Core.instDecidableEqRefinedEmotionProfile.decEq (x✝ x✝¹ : RefinedEmotionProfile) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Core.instDecidableEqRefinedEmotionProfile : DecidableEq RefinedEmotionProfile

Equations

• Core.instDecidableEqRefinedEmotionProfile = Core.instDecidableEqRefinedEmotionProfile.decEq

def Core.instReprRefinedEmotionProfile.repr : RefinedEmotionProfile → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Core.instReprRefinedEmotionProfile : Repr RefinedEmotionProfile

Equations

• Core.instReprRefinedEmotionProfile = { reprPrec := Core.instReprRefinedEmotionProfile.repr }

def Core.RefinedEmotionProfile.toEmotionProfile (r : RefinedEmotionProfile) : EmotionProfile

Every refined profile projects to a qualitative profile.

Equations

• r.toEmotionProfile = { name := r.name, weights := r.weights.toAppraisalWeights, orientation := r.orientation }

Prospective Emotions

The 20 emotions in §7 are all retrospective: they are computed from an observed outcome (the agent saw what happened, and we appraise the result). But emotional attitude verbs like hope and fear are prospective: the outcome is uncertain, and the emotional state concerns how the uncertainty might be resolved.

@cite{anand-hacquard-2013} formalize exactly this: emotive doxastics (hope, fear) combine:

1. A doxastic component (belief that φ is possible but uncertain)
2. A preference component (preference for φ-verifying resolutions)

This maps directly onto the BToM architecture:

• The doxastic component = belief marginal: Pr(b | a) determines the agent's epistemic state (what they think is possible)
• The preference component = desire marginal: Pr(d | a) determines what the agent wants
• The uncertainty condition = non-extreme credence: the agent's beliefs don't settle the question

From Retrospective to Prospective

Retrospective (Houlihan)	Prospective (A&H emotive doxastic)
Outcome observed	Outcome uncertain
AU = U(actual | desires)	Preference = desire ordering over DOX partition
PE = actual − E[actual | beliefs]	N/A (no outcome to compare to)
CF = U(alternative) − U(actual)	N/A (no actual outcome)
Post-outcome: all 4 appraisal types	Pre-outcome: only AU analog available

The key structural insight: prospective AU reduces to the preference ordering over verifiers vs. falsifiers. When the outcome is uncertain, the achieved utility is not a single number but a comparison between the utility of φ-worlds and ¬φ-worlds, weighted by the agent's beliefs about which is actual. This is precisely the preference component of emotive doxastics.

Mathematical Foundation

For a BToM model with belief states B and desire states D:

Prospective achieved utility (expected utility conditional on φ):

EU(a, φ) = Σ_d Pr(d | a) · [Σ_w Pr(w | a, φ) · U(w, d)]

Prospective preference (φ preferred to ¬φ):

φ >_DES ¬φ  ⟺  EU(a, φ) > EU(a, ¬φ)

Uncertainty (non-extreme credence):

uncertain(a, φ) ⟺ 0 < Pr(φ | a) < 1
  where Pr(φ | a) = Σ_b Pr(b | a) · ⟦φ⟧_b

The prospective AU is a conditional expectation — conditioned on φ or ¬φ being the resolution — rather than a marginal utility of the actual outcome. This is the formal content of "preference over how the uncertainty gets resolved" from @cite{anand-hacquard-2013} §4.1.

structure Core.ProspectiveAppraisal (F : Type u_1) : Type u_1

Prospective appraisal: computed over uncertain future outcomes rather than observed past outcomes.

The BToM components needed are:

• beliefCredence: Pr(φ | a) from the belief marginal (how likely the agent thinks φ is)
• conditionalUtility: EU(a, φ) and EU(a, ¬φ) — expected utility of the φ-worlds and ¬φ-worlds, weighted by desires

• beliefCredence : F

  Agent's credence in φ: Pr(φ | a) from BToM belief marginal. This is Σ_b Pr(b | a) · ⟦φ⟧_b — the probabilistic analog of "∃w' ∈ DOX: φ(w')" in the classical framework.

• utilityIfTrue : F

  Expected utility conditional on φ: EU(a, φ). The prospective analog of achieved utility.

• utilityIfFalse : F

  Expected utility conditional on ¬φ: EU(a, ¬φ).

def Core.ProspectiveAppraisal.isUncertain {F : Type u_1} [LinearOrder F] [Zero F] [One F] (a : ProspectiveAppraisal F) : Bool

The agent is uncertain about φ: credence is strictly between 0 and 1. This is the probabilistic analog of the A&H uncertainty condition: ∃w' ∈ DOX: φ(w') ∧ ∃w' ∈ DOX: ¬φ(w').

Equations

• a.isUncertain = (decide (a.beliefCredence > 0) && decide (a.beliefCredence < 1))

def Core.ProspectiveAppraisal.isHope {F : Type u_1} [LinearOrder F] [Zero F] [One F] (a : ProspectiveAppraisal F) : Bool

Hope: uncertain about φ and prefers φ-resolution. @cite{anand-hacquard-2013}: emotive doxastic with positive valence.

Equations

• a.isHope = (a.isUncertain && decide (a.utilityIfTrue > a.utilityIfFalse))

def Core.ProspectiveAppraisal.isFear {F : Type u_1} [LinearOrder F] [Zero F] [One F] (a : ProspectiveAppraisal F) : Bool

Fear: uncertain about φ and disprefers φ-resolution. @cite{anand-hacquard-2013}: emotive doxastic with negative valence.

Equations

• a.isFear = (a.isUncertain && decide (a.utilityIfFalse > a.utilityIfTrue))

structure Core.ProspectiveEmotionProfile : Type

A prospective emotion profile: extends the retrospective 8-dimensional profile with the pre-outcome appraisal structure.

Prospective emotions use only the AU analog (preference over resolutions). PE, CFa, CFo are undefined pre-outcome — there is no actual outcome to compute prediction error or counterfactuals against.

• name : String

  Name of the prospective emotion

• valence : AppraisalSign

  Valence: does the agent prefer φ (positive) or ¬φ (negative)?

• orientation : TemporalOrientation

  Orientation: always prospective

def Core.prospectiveHope : ProspectiveEmotionProfile

Prospective hope: positive prospective AU (prefers φ-resolution).

Equations

• Core.prospectiveHope = { name := "hope", valence := Core.AppraisalSign.positive }

def Core.prospectiveFear : ProspectiveEmotionProfile

Prospective fear: negative prospective AU (disprefers φ-resolution).

Equations

• Core.prospectiveFear = { name := "fear", valence := Core.AppraisalSign.negative }

def Core.prospectiveDread : ProspectiveEmotionProfile

Prospective dread: strong negative prospective AU. Structurally identical to fear but with higher intensity (lower threshold).

Equations

• Core.prospectiveDread = { name := "dread", valence := Core.AppraisalSign.negative }

def Core.agentCredence {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (phiInBelief : B → F) (action : A) : F

Compute agent credence in φ from BToM belief marginals.

Pr(φ | a) = Σ_b Pr(b | a) · ⟦φ⟧_b

where ⟦φ⟧_b is 1 if belief state b is compatible with φ, 0 otherwise. This is exactly beliefExpectation instantiated with the characteristic function of φ.

Equations

• Core.agentCredence model phiInBelief action = model.beliefExpectation phiInBelief action

def Core.prospectiveUtility {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (conditionalUtility : D → F) (action : A) : F

Compute prospective utility: expected utility of φ-worlds under inferred desires.

EU(a, φ) = Σ_d Pr(d | a) · U_φ(d)

where U_φ(d) is the utility the agent would get from desire d being satisfied in a φ-world. This is achievedUtility with a φ-conditional utility function.

Equations

• Core.prospectiveUtility model conditionalUtility action = ∑ d : D, model.desireMarginal action d * conditionalUtility d

def Core.buildProspectiveAppraisal {F : Type u_1} [CommSemiring F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (phiInBelief : B → F) (utilIfTrue utilIfFalse : D → F) (action : A) : ProspectiveAppraisal F

Build a prospective appraisal from a BToM model.

Combines the belief marginal (for credence) and desire marginal (for conditional utilities) to construct the pre-outcome appraisal that emotive doxastic attitudes operate over.

Equations

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

theorem Core.agentCredence_eq_beliefExpectation {F : Type u_1} [CommSemiring F] [LinearOrder F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (phiInBelief : B → F) (action : A) : agentCredence model phiInBelief action = model.beliefExpectation phiInBelief action

Agent credence is structurally a BToM belief expectation.

theorem Core.prospectiveUtility_eq_desire_weighted_sum {F : Type u_1} [CommSemiring F] [LinearOrder F] {A : Type u_2} {P : Type u_3} {B : Type u_4} {D : Type u_5} {S : Type u_6} {M : Type u_7} {W : Type u_8} [Fintype P] [Fintype B] [Fintype D] [Fintype S] [Fintype M] [Fintype W] (model : BToMModel F A P B D S M W) (conditionalUtility : D → F) (action : A) : prospectiveUtility model conditionalUtility action = ∑ d : D, model.desireMarginal action d * conditionalUtility d

Prospective utility is structurally a desire-marginal weighted sum — the same computation as retrospective achieved utility, but with a conditional utility function instead of an actual-outcome utility.