Mushroom Foraging Cover Story

Features: 3 colors × 3 textures

• Colors: Green, Red, Blue
• Textures: Spotted, Solid, Striped

Each feature has a reward value in {-2, -1, 0, +1, +2} Mushroom reward = sum of color reward + texture reward

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureType : Type

Feature types in the experimental domain

• green : FeatureType
• red : FeatureType
• blue : FeatureType
• spotted : FeatureType
• solid : FeatureType
• striped : FeatureType

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeatureType : DecidableEq FeatureType

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeatureType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureType.repr : FeatureType → ℕ → Std.Format

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureType : Repr FeatureType

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureType = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureType.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureType.beq : FeatureType → FeatureType → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureType.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureType : BEq FeatureType

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureType = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureType.beq }

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.RewardValue : Type

Possible reward values for features (coarse: data-level)

• minusTwo : RewardValue
• plusOne : RewardValue
• plusTwo : RewardValue

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqRewardValue : DecidableEq RewardValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqRewardValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprRewardValue.repr : RewardValue → ℕ → Std.Format

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprRewardValue : Repr RewardValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprRewardValue = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprRewardValue.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqRewardValue.beq : RewardValue → RewardValue → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqRewardValue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqRewardValue : BEq RewardValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqRewardValue = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqRewardValue.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.RewardValue.toInt : RewardValue → ℤ

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.RewardValue.minusTwo.toInt = -2
• Phenomena.Imperatives.Studies.SumersEtAl2023.RewardValue.plusOne.toInt = 1
• Phenomena.Imperatives.Studies.SumersEtAl2023.RewardValue.plusTwo.toInt = 2

Experiment 1: 1DP vs 2DP Contexts

Manipulated context complexity:

• 1DP (one decision point): Only one action available that has the queried feature
• 2DP (two decision points): Two actions available that have the queried feature

Key prediction: In 1DP, truthful and relevant responses converge. In 2DP, they can diverge, revealing tradeoff.

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.ContextCondition : Type

Context complexity conditions

• oneDP : ContextCondition
• twoDP : ContextCondition

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqContextCondition : DecidableEq ContextCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqContextCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprContextCondition.repr : ContextCondition → ℕ → Std.Format

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprContextCondition : Repr ContextCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprContextCondition = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprContextCondition.repr }

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqContextCondition : BEq ContextCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqContextCondition = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqContextCondition.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqContextCondition.beq : ContextCondition → ContextCondition → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqContextCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp1Design : Type

Experiment 1: Sample size and conditions

• nParticipants : ℕ

  Number of participants

• participantsPerCondition : ℕ

  Participants per condition (between-subjects)

• trialsPerCondition : ℕ

  Trials per participant per condition

• totalTrials : ℕ

  Total trials

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp1Design : Exp1Design

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp1Design = { nParticipants := 63, participantsPerCondition := 63, trialsPerCondition := 30, totalTrials := 3780 }

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp1ResponseRates : Type

Experiment 1: Human response rates by condition.

From Figure 3a and statistical analysis:

• 1DP: ~91% relevant responses
• 2DP: ~60% relevant responses

• relevanceRate1DP : ℚ

  Rate of relevance-maximizing responses in 1DP condition

• relevanceRate2DP : ℚ

  Rate of relevance-maximizing responses in 2DP condition

• se1DP : ℚ

  Standard error for 1DP

• se2DP : ℚ

  Standard error for 2DP

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp1ResponseRates : Exp1ResponseRates

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp1ResponseRates = { relevanceRate1DP := 91 / 100, relevanceRate2DP := 60 / 100, se1DP := 3 / 100, se2DP := 5 / 100 }

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp1Stats : Type

Statistical test: Significant effect of context.

Mixed-effects logistic regression: β = -2.13, z = -5.95, p < 0.001

• beta : ℚ

  Coefficient for 2DP vs 1DP effect

• zStat : ℚ

  z-statistic

• pValueLessThan : ℚ

  p < 0.001

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp1Stats : Exp1Stats

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp1Stats = { beta := -213 / 100, zStat := -595 / 100, pValueLessThan := 1 / 1000 }

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.exp1_context_effect : exp1ResponseRates.relevanceRate1DP > exp1ResponseRates.relevanceRate2DP

Key finding: Context affects relevance rate

Experiment 2: Instruction Manipulation

Between-subjects manipulation of speaker goals:

• Unbiased: "Help the forager" (standard)
• Truth-biased: "Tell the forager which feature value is largest"
• Relevance-biased: "Help the forager choose the best mushroom"

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.InstructionCondition : Type

Instruction conditions

• unbiased : InstructionCondition
• truthBiased : InstructionCondition
• relevanceBiased : InstructionCondition

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqInstructionCondition : DecidableEq InstructionCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqInstructionCondition x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprInstructionCondition : Repr InstructionCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprInstructionCondition = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprInstructionCondition.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprInstructionCondition.repr : InstructionCondition → ℕ → Std.Format

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqInstructionCondition : BEq InstructionCondition

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqInstructionCondition = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqInstructionCondition.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqInstructionCondition.beq : InstructionCondition → InstructionCondition → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqInstructionCondition.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp2Design : Type

Experiment 2: Design parameters

• nParticipants : ℕ

  Total participants

• participantsUnbiased : ℕ

  Participants per condition

• participantsTruthBiased : ℕ
• participantsRelevanceBiased : ℕ
• trialsPerParticipant : ℕ

  Trials per participant

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp2Design : Exp2Design

Equations

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

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp2ResponseRates : Type

Experiment 2: Human response rates by instruction condition.

From Figure 3b:

• Unbiased: ~55% relevant
• Truth-biased: ~35% relevant
• Relevance-biased: ~85% relevant

• relevanceRateUnbiased : ℚ

  Relevance rate in unbiased condition

• relevanceRateTruthBiased : ℚ

  Relevance rate in truth-biased condition

• relevanceRateRelevanceBiased : ℚ

  Relevance rate in relevance-biased condition

• seUnbiased : ℚ

  Standard errors

• seTruthBiased : ℚ
• seRelevanceBiased : ℚ

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp2ResponseRates : Exp2ResponseRates

Equations

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

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp2Stats : Type

Statistical tests for Experiment 2.

Pairwise comparisons with Bonferroni correction:

• Relevance-biased > Unbiased: χ² = 18.4, p < 0.001
• Unbiased > Truth-biased: χ² = 8.2, p = 0.004

• chiSqRelevanceVsUnbiased : ℚ

  Chi-squared: relevance vs unbiased

• chiSqUnbiasedVsTruth : ℚ

  Chi-squared: unbiased vs truth

• allSignificant : Bool

  Both p < 0.05 after correction

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp2Stats : Exp2Stats

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp2Stats = { chiSqRelevanceVsUnbiased := 184 / 10, chiSqUnbiasedVsTruth := 82 / 10, allSignificant := true }

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.exp2_instruction_ordering : exp2ResponseRates.relevanceRateRelevanceBiased > exp2ResponseRates.relevanceRateUnbiased ∧ exp2ResponseRates.relevanceRateUnbiased > exp2ResponseRates.relevanceRateTruthBiased

Key finding: Instruction ordering

Model Comparison

The paper compares several models against human data:

1. Combined model (truthfulness + relevance)
2. Truthfulness-only
3. Relevance-only
4. Literal speaker

Best-fit λ parameters by condition:

• Unbiased: λ = 0.55
• Truth-biased: λ = 0.35
• Relevance-biased: λ = 0.85

structure Phenomena.Imperatives.Studies.SumersEtAl2023.MLEParameters : Type

MLE parameter estimates for λ by condition

• lamUnbiased : ℚ

  λ for unbiased condition

• lamTruthBiased : ℚ

  λ for truth-biased condition

• lamRelevanceBiased : ℚ

  λ for relevance-biased condition

def Phenomena.Imperatives.Studies.SumersEtAl2023.mleParams : MLEParameters

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.mleParams = { lamUnbiased := 55 / 100, lamTruthBiased := 35 / 100, lamRelevanceBiased := 85 / 100 }

structure Phenomena.Imperatives.Studies.SumersEtAl2023.ModelFit : Type

Model fit statistics (log-likelihood)

• llCombined : ℚ

  Combined model log-likelihood

• llTruthOnly : ℚ

  Truthfulness-only log-likelihood

• llRelevanceOnly : ℚ

  Relevance-only log-likelihood

• llLiteral : ℚ

  Literal speaker log-likelihood

def Phenomena.Imperatives.Studies.SumersEtAl2023.modelFit : ModelFit

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.modelFit = { llCombined := -3200, llTruthOnly := -4100, llRelevanceOnly := -3800, llLiteral := -5200 }

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.combined_best_fit : modelFit.llCombined > modelFit.llTruthOnly ∧ modelFit.llCombined > modelFit.llRelevanceOnly ∧ modelFit.llCombined > modelFit.llLiteral

Combined model has best fit

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.lambda_ordering_matches_instructions : mleParams.lamRelevanceBiased > mleParams.lamUnbiased ∧ mleParams.lamUnbiased > mleParams.lamTruthBiased

λ ordering matches instruction manipulation

Summary of Key Empirical Patterns

1. Tradeoff exists: Speakers don't maximize either truthfulness or relevance alone
2. Context-sensitive: More truthful in complex (2DP) contexts
3. Instruction-sensitive: λ shifts with explicit goal manipulation
4. Gradedness: Responses show graded preferences, not categorical choices

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.pattern_tradeoff : exp2ResponseRates.relevanceRateUnbiased > 30 / 100 ∧ exp2ResponseRates.relevanceRateUnbiased < 70 / 100

Pattern 1: Neither extreme is modal

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.pattern_context : exp1ResponseRates.relevanceRate1DP ≠ exp1ResponseRates.relevanceRate2DP

Pattern 2: Context matters

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.pattern_instructions : mleParams.lamRelevanceBiased > mleParams.lamTruthBiased

Pattern 3: Instructions matter

Example Trial

World: Green = +2, Spotted = +1, other features have various values

Context (2DP):

• Action A: Green, Spotted (reward = +3)
• Action B: Green, Solid (reward = +2 if Solid = 0)
• Action C: Red, Striped (reward varies)

True utterance: "Green is +2" Relevant utterance: "Spotted is +1" (if it uniquely identifies best mushroom)

structure Phenomena.Imperatives.Studies.SumersEtAl2023.ExampleTrial : Type

Example trial structure

• worldDescription : String

  World state description

• actions : List String

  Available actions

• truthfulUtterance : String

  Most truthful utterance (about highest feature)

• relevantUtterance : String

  Most relevant utterance (identifies best action)

• diverges : Bool

  Whether they diverge

def Phenomena.Imperatives.Studies.SumersEtAl2023.exampleTrial : ExampleTrial

Equations

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

Signaling Bandits: RSA Model

@cite{frank-goodman-2012} @cite{sumers-hawkins-2023}

Unlike Lewis signaling games where world state = correct action, signaling bandits separate abstract knowledge (feature values) from concrete decisions (which action to take).

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.Feature : Type

Features that characterize actions (e.g., colors, textures)

• green : Feature
• red : Feature
• blue : Feature
• spotted : Feature
• solid : Feature
• striped : Feature

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeature : DecidableEq Feature

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeature x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeature : Repr Feature

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeature = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeature.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeature.repr : Feature → ℕ → Std.Format

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeature.beq : Feature → Feature → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeature.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeature : BEq Feature

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeature = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeature.beq }

inductive Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue : Type

Feature values in the experimental range

• neg2 : FeatureValue
• neg1 : FeatureValue
• zero : FeatureValue
• pos1 : FeatureValue
• pos2 : FeatureValue

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeatureValue : DecidableEq FeatureValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqFeatureValue x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureValue : Repr FeatureValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureValue = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureValue.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprFeatureValue.repr : FeatureValue → ℕ → Std.Format

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureValue.beq : FeatureValue → FeatureValue → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureValue.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureValue : BEq FeatureValue

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureValue = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqFeatureValue.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.toRat : FeatureValue → ℚ

Convert feature value to rational

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.neg2.toRat = -2
• Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.neg1.toRat = -1
• Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.zero.toRat = 0
• Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.pos1.toRat = 1
• Phenomena.Imperatives.Studies.SumersEtAl2023.FeatureValue.pos2.toRat = 2

def Phenomena.Imperatives.Studies.SumersEtAl2023.allFeatureValues : List FeatureValue

All feature values

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.allFeatures : List Feature

All features

Equations

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

structure Phenomena.Imperatives.Studies.SumersEtAl2023.WorldState : Type

World state: mapping from features to values.

In the mushroom experiment, this defines how valuable each feature is. Example: {Green -> +2, Red -> 0, Blue -> -2, Spotted -> +1, Solid -> 0, Striped -> -1}

• featureValue : Feature → FeatureValue

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqWorldState : BEq WorldState

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.WorldState.getValue (w : WorldState) (f : Feature) : ℚ

Get the rational value of a feature in a world

Equations

• w.getValue f = (w.featureValue f).toRat

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Action : Type

Action (mushroom) characterized by features it has

• hasFeature : Feature → Bool

  Which features this action has (e.g., a green spotted mushroom)

• name : String

  Human-readable name

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqAction : BEq Action

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.reward (a : Action) (w : WorldState) : ℚ

Reward for taking an action in a world state.

R(a,w) = Sum_f [a has f] * w(f)

Linear combination of feature values for features the action has.

Equations

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

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Context : Type

Decision context: subset of available actions

• actions : List Action

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Utterance : Type

Utterance: claim about a feature's value.

Example: "Spots are +1" = {feature :=.spotted, value :=.pos1}

• feature : Feature
• value : FeatureValue

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqUtterance : DecidableEq Utterance

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqUtterance = Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqUtterance.decEq

def Phenomena.Imperatives.Studies.SumersEtAl2023.instDecidableEqUtterance.decEq (x✝ x✝¹ : Utterance) : Decidable (x✝ = x✝¹)

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprUtterance : Repr Utterance

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprUtterance = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprUtterance.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprUtterance.repr : Utterance → ℕ → Std.Format

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance.beq : Utterance → Utterance → Bool

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance.beq { feature := a, value := a_1 } { feature := b, value := b_1 } = (a == b && a_1 == b_1)
• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance.beq x✝¹ x✝ = false

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance : BEq Utterance

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqUtterance.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.allUtterances : List Utterance

All possible utterances (30 = 6 features x 5 values)

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.utteranceTruth (u : Utterance) (w : WorldState) : Bool

Truth of an utterance in a world state

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.utteranceTruth u w = (w.featureValue u.feature == u.value)

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Params : Type

Model parameters for Sumers et al. speaker model

• βS : ℚ

  Speaker rationality (soft-max temperature)

• βL : ℚ

  Listener rationality

• lam : ℚ

  Tradeoff: 0 = pure truthfulness, 1 = pure relevance

• costWeight : ℚ

  Cost weight

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instReprParams : Repr Params

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instReprParams = { reprPrec := Phenomena.Imperatives.Studies.SumersEtAl2023.instReprParams.repr }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instReprParams.repr : Params → ℕ → Std.Format

Equations

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

instance Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqParams : BEq Params

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqParams = { beq := Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqParams.beq }

def Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqParams.beq : Params → Params → Bool

Equations

• One or more equations did not get rendered due to their size.
• Phenomena.Imperatives.Studies.SumersEtAl2023.instBEqParams.beq x✝¹ x✝ = false

def Phenomena.Imperatives.Studies.SumersEtAl2023.defaultParams : Params

Default parameters (matches Exp 1 Unbiased MLE)

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.defaultParams = { lam := 55 / 100 }

def Phenomena.Imperatives.Studies.SumersEtAl2023.truthBiasedParams : Params

Truth-biased parameters (Exp 1 MLE)

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.truthBiasedParams = { lam := 35 / 100 }

def Phenomena.Imperatives.Studies.SumersEtAl2023.relevanceBiasedParams : Params

Relevance-biased parameters (Exp 1 MLE)

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.relevanceBiasedParams = { lam := 85 / 100 }

Speaker Utilities

Three components:

1. Truthfulness (Eq. 5): epistemic preference for true utterances
2. Relevance (Eq. 8): decision-theoretic preference for action-improving utterances
3. Cost: production/processing effort

def Phenomena.Imperatives.Studies.SumersEtAl2023.truthfulnessUtility (u : Utterance) (w : WorldState) : ℚ

Truthfulness utility (Eq. 5).

U_T(u|w) = +1 if [u] = true = -1 if [u] = false

Note: This is a soft constraint via betaS, not a hard filter.

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.truthfulnessUtility u w = if Phenomena.Imperatives.Studies.SumersEtAl2023.utteranceTruth u w = true then 1 else -1

def Phenomena.Imperatives.Studies.SumersEtAl2023.utteranceCost (_u : Utterance) : ℚ

Utterance cost.

Default: 0 for all utterances. Can be extended for valence bias (positive utterances preferred).

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.utteranceCost _u = 0

def Phenomena.Imperatives.Studies.SumersEtAl2023.valenceCost (u : Utterance) (ν : ℚ := 1 / 4) : ℚ

Valence-based cost (from Exp 1 residual analysis).

Negative-valued utterances have higher cost (require more processing).

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.combinedUtility (lam uT uR costWeight cost : ℚ) : ℚ

Combined utility (Eq. 9).

U_C(u|w,A) = lambda*U_R(u|w,A) + (1-lambda)*U_T(u|w) - C(u)

Convex combination of relevance and truthfulness, minus cost. Note: Relevance utility requires the full listener model, which depends on the removed RSA.Eval infrastructure. We define the combined utility in terms of the abstract combined function from CombinedUtility, with relevance as a parameter.

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.combinedUtility lam uT uR costWeight cost = RSA.CombinedUtility.combined lam uT uR (costWeight * cost)

Experimental Domain: Mushroom Foraging

The experiments use a mushroom foraging cover story:

• Features: Green, Red, Blue (colors) and Spotted, Solid, Striped (textures)
• Each mushroom has one color and one texture
• Rewards are additive over features

def Phenomena.Imperatives.Studies.SumersEtAl2023.makeMushroom (color texture : Feature) (name : String := "mushroom") : Action

Create a mushroom with one color and one texture

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.canonicalWorld : WorldState

Canonical world state from the experiment.

Green = +2, Red = 0, Blue = -2 Spotted = +1, Solid = 0, Striped = -1

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.exampleContext : Context

Example context from Figure 6B: three mushrooms

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.trueUtterance : Utterance

True utterance in canonical world

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.falseRelevantUtterance : Utterance

False but relevant utterance

Equations

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

def Phenomena.Imperatives.Studies.SumersEtAl2023.trueIrrelevantUtterance : Utterance

True but irrelevant utterance (feature not in context)

Equations

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

Key Theoretical Results

These connect to Comparisons/RelevanceTheories.lean for the deep theorems.

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.combined_pure_truthfulness (uT uR : ℚ) : combinedUtility 0 uT uR 0 0 = uT

Combined model reduces to truthfulness when lambda = 0.

U_C(u|w,A) = U_T(u|w) when lambda = 0. Delegates to CombinedUtility.combined_at_zero.

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.combined_pure_relevance (uT uR : ℚ) : combinedUtility 1 uT uR 0 0 = uR

Combined model reduces to relevance when lambda = 1.

U_C(u|w,A) = U_R(u|w,A) when lambda = 1. Delegates to CombinedUtility.combined_at_one.

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.truthfulness_relevance_independent : have w := { featureValue := fun (f : Feature) => match f with | Feature.green => FeatureValue.pos2 | Feature.red => FeatureValue.zero | Feature.blue => FeatureValue.neg2 | Feature.spotted => FeatureValue.pos1 | Feature.solid => FeatureValue.zero | Feature.striped => FeatureValue.neg1 }; have trueIrrel := { feature := Feature.green, value := FeatureValue.pos2 }; have falseRel := { feature := Feature.spotted, value := FeatureValue.pos2 }; truthfulnessUtility trueIrrel w = 1 ∧ truthfulnessUtility falseRel w = -1

Truthfulness and relevance are independent objectives.

In Lewis signaling games, they are perfectly correlated (knowing the world = knowing the best action). In signaling bandits, they can diverge:

• True but irrelevant: "Green is +2" when no green actions in context
• False but relevant: "Spots are +2" when spots are actually +1

Witness 1 (true but irrelevant): "Green is +2" -- true in the canonical world but no green mushrooms appear in the example context. Witness 2 (false but relevant): "Spots are +2" -- false (spots are +1) but would steer the listener toward the spotted mushroom (the best action).

Empirical Predictions from Experiments

The paper reports MLE parameters and response patterns.

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp1MLEResults : Type

Experiment 1: Free choice paradigm.

Participants chose from 30 utterances. MLE parameters:

• Truth-biased: lambda = 0.35
• Unbiased: lambda = 0.55
• Relevance-biased: lambda = 0.85

• truthBiased_lam : ℚ
• unbiased_lam : ℚ
• relevanceBiased_lam : ℚ

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp1MLEResults : Exp1MLEResults

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp1MLEResults = { }

structure Phenomena.Imperatives.Studies.SumersEtAl2023.Exp2MLEResults : Type

Experiment 2: Forced choice (endorsement) paradigm.

Participants endorsed specific utterances. MLE parameters:

• Truth-biased: lambda = 0.15
• Unbiased: lambda = 0.75
• Relevance-biased: lambda = 0.90

• truthBiased_lam : ℚ
• unbiased_lam : ℚ
• relevanceBiased_lam : ℚ

def Phenomena.Imperatives.Studies.SumersEtAl2023.exp2MLEResults : Exp2MLEResults

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.exp2MLEResults = { }

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.unbiased_participants_use_combined : exp1MLEResults.unbiased_lam > 0 ∧ exp1MLEResults.unbiased_lam < 1

Unbiased participants jointly optimize truthfulness and relevance.

Neither lambda = 0 (pure truth) nor lambda = 1 (pure relevance) fits the data. Participants make a graded tradeoff.

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.manipulation_affects_lambda : exp1MLEResults.truthBiased_lam < exp1MLEResults.unbiased_lam ∧ exp1MLEResults.unbiased_lam < exp1MLEResults.relevanceBiased_lam

Manipulation affects lambda parameter ordering.

lambda_truth < lambda_unbiased < lambda_relevance

Connections to Other Frameworks

Sumers et al. bridges several research traditions:

1. Standard RSA: Pure epistemic utility. Recovered when lambda = 0 and listener has identity decision problem.

2. Game-theoretic pragmatics (Benz, Parikh): Decision-theoretic relevance. Recovered when lambda = 1.

3. Relevance Theory (Sperber & Wilson): Relevance as primary. Empirically challenged: participants value truthfulness independently.

4. QUD models (Roberts): Question under discussion. QUDs can be derived from decision problems (Theorem 2).

See Comparisons/RelevanceTheories.lean for the formal connections:

• Identity DP equiv epistemic utility (Theorem 1)
• Any QUD is some DP (Theorem 2)
• DT strictly more expressive than QUD (Theorem 3)

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.standard_rsa_is_special_case (uT uR : ℚ) : combinedUtility 0 uT uR 0 0 = uT

Standard RSA is a special case: when lambda = 0 and cost = 0, the combined utility equals truthfulness utility alone.

This recovers standard RSA's epistemic speaker, which soft-maximizes truthfulness (informativity). The identity-DP connection (Theorem 1 of Sumers et al.) is proved in combined_pure_truthfulness above.

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.relevance_theory_challenged : exp1MLEResults.relevanceBiased_lam < 1

Relevance Theory predicts lambda = 1, which is empirically falsified

Summary

Unified speaker model combining truthfulness and relevance:

U_C(u|w,A) = lambda*U_R(u|w,A) + (1-lambda)*U_T(u|w) - C(u)

Empirical findings:

1. Participants use both truthfulness and relevance (0 < lambda < 1)
2. Neither objective strictly dominates
3. The tradeoff is graded, not binary

Theoretical implications:

• Decision-theoretic relevance grounds QUD-based relevance
• Truthfulness is an independent constraint, not derived from relevance
• The combined model explains loose talk and context-sensitivity

theorem Phenomena.Imperatives.Studies.SumersEtAl2023.sumers_uses_combined (lam uT uR costWeight cost : ℚ) : combinedUtility lam uT uR costWeight cost = RSA.CombinedUtility.combined lam uT uR (costWeight * cost)

Sumers et al.'s combinedUtility is CombinedUtility.combined(lambda, U_T, U_R, cost).

This makes the shared combined theorems (combined_at_zero, combined_at_one, combined_convex, combined_mono_A/B) directly applicable.

def Phenomena.Imperatives.Studies.SumersEtAl2023.integratedModel : String

The integrated model of truthfulness and relevance

Equations

• Phenomena.Imperatives.Studies.SumersEtAl2023.integratedModel = "U_C = lambda*U_Relevance + (1-lambda)*U_Truthfulness - Cost"