Documentation

Linglib.Studies.KaoEtAl2014PMFHyperbole

[KWBG14] on mathlib `PMF` — headline architectural theorem #

"Nonliteral understanding of number words", PNAS 111(33):12002-12007.

What this file is #

A headline-focused PMF formalisation of Kao et al. 2014's hyperbole model. The substrate emphasis is on the architectural theorem that captures the paper's central scientific claim:

Joint inference over the speaker's communicative goal is what enables literally-false utterances to receive positive L1 mass.

Without goal marginalisation (vanilla RSA), the L1 posterior of "$10K" for a $50 kettle would be zero: the literal listener gives mass 0 to s = $50 given utterance "$10K". With joint goal inference, some goal (e.g., affect-only) makes the QUD-projection non-zero at literally-false meanings, and L1 marginalises over goals to pick this up.

Headline theorem #

L1_pos_iff_exists_goal_qud_pos —

L1(s, a | u) > 0 ↔ ∃ g, goalPrior g > 0 ∧ qudProjL0 g u (s, a) > 0

The ∃ g, ... clause is the architectural mechanism. With only the identity goal (vanilla RSA), qudProjL0 is concentrated on literally- true meanings. Adding goals that PROJECT the meaning space (lose information about price or affect) broadens the support to literally-false meanings — exactly what enables hyperbole.

Cost-and-goal architecture #

Hyperbole adds utterance costs C(u) to Kao Metaphor's joint-goal architecture (Eq. 7 of paper):

S1(u | s, a, g) ∝ exp(α · (log L0(g(s,a) | u) − C(u)))

For α = 1 this is softmax(log(qudProjL0) − cost), which slots cleanly into our EReal-softmax substrate as a different score function. Costs do NOT require a new substrate primitive — the headline architectural theorem is independent of cost structure (cost merely modulates which utterances the speaker is likely to use, not which interpretations remain in L1's support).

Why this scope #

The 6 paper findings (hyperbole, halo, literal-correct, etc.) are empirical-fit numerical claims at Kao's specific empirical priors. They are stated below as sorried corollaries, with the architectural payoff captured by the headline theorem above. Future work to discharge them follows the Kao Metaphor / FG2012 pattern.

§0. Domain types #

inductive KaoEtAl2014PMFHyperbole.Item :

Item types from Experiment 3a/3b: electric kettles, laptops, watches. Each item has its own price prior.

electricKettle : Item
laptop : Item
watch : Item

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instDecidableEqItem :

DecidableEq Item

Equations

KaoEtAl2014PMFHyperbole.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoEtAl2014PMFHyperbole.instReprItem.repr :

Item → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instReprItem :

Repr Item

Equations

KaoEtAl2014PMFHyperbole.instReprItem = { reprPrec := KaoEtAl2014PMFHyperbole.instReprItem.repr }

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instFintypeItem :

Fintype Item

Equations

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

inductive KaoEtAl2014PMFHyperbole.PriceState :

Price states: 10 prices, organized as round/sharp pairs.

s50 : PriceState
s51 : PriceState
s500 : PriceState
s501 : PriceState
s1000 : PriceState
s1001 : PriceState
s5000 : PriceState
s5001 : PriceState
s10000 : PriceState
s10001 : PriceState

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instDecidableEqPriceState :

DecidableEq PriceState

Equations

KaoEtAl2014PMFHyperbole.instDecidableEqPriceState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoEtAl2014PMFHyperbole.instReprPriceState.repr :

PriceState → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instReprPriceState :

Repr PriceState

Equations

KaoEtAl2014PMFHyperbole.instReprPriceState = { reprPrec := KaoEtAl2014PMFHyperbole.instReprPriceState.repr }

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instFintypePriceState :

Fintype PriceState

Equations

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

def KaoEtAl2014PMFHyperbole.PriceState.value :

PriceState → ℕ

The price as a numeric value (used for round/sharp distinction).

Equations

Instances For

def KaoEtAl2014PMFHyperbole.PriceState.isRound :

PriceState → Bool

A price is "round" if divisible by 10. Round numbers have lower utterance cost; sharp numbers convey precision.

Equations

KaoEtAl2014PMFHyperbole.PriceState.s50.isRound = true
KaoEtAl2014PMFHyperbole.PriceState.s500.isRound = true
KaoEtAl2014PMFHyperbole.PriceState.s1000.isRound = true
KaoEtAl2014PMFHyperbole.PriceState.s5000.isRound = true
KaoEtAl2014PMFHyperbole.PriceState.s10000.isRound = true
x✝.isRound = false

Instances For

def KaoEtAl2014PMFHyperbole.PriceState.round :

PriceState → PriceState

Approximation: round prices to their nearest "round" (×10) value. Used by the approxPrice and approxPriceValence goals.

Equations

Instances For

theorem KaoEtAl2014PMFHyperbole.round_value_eq_roundToNearest (p : PriceState) :

↑p.round.value = Semantics.Numerals.Precision.roundToNearest ↑p.value

PriceState.round is the substrate rounding map: composing with value gives Precision.roundToNearest at the paper's base 10.

inductive KaoEtAl2014PMFHyperbole.Affect :

Binary affect: speaker has notable opinion, or none.

none : Affect
notable : Affect

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instDecidableEqAffect :

DecidableEq Affect

Equations

KaoEtAl2014PMFHyperbole.instDecidableEqAffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instReprAffect :

Equations

KaoEtAl2014PMFHyperbole.instReprAffect = { reprPrec := KaoEtAl2014PMFHyperbole.instReprAffect.repr }

def KaoEtAl2014PMFHyperbole.instReprAffect.repr :

Affect → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instFintypeAffect :

Fintype Affect

Equations

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

@[reducible, inline]

abbrev KaoEtAl2014PMFHyperbole.World :

World = (price state, affect).

Equations

KaoEtAl2014PMFHyperbole.World = (KaoEtAl2014PMFHyperbole.PriceState × KaoEtAl2014PMFHyperbole.Affect)

Instances For

instance KaoEtAl2014PMFHyperbole.instNonemptyWorld :

Nonempty World

inductive KaoEtAl2014PMFHyperbole.Goal :

The 5 communicative goals (paper §"Materials and Methods"): relevance ∈ {price, affect, both} × precision ∈ {exact, approximate}; one collapse since affect-only doesn't depend on precision.

price : Goal
valence : Goal
priceValence : Goal
approxPrice : Goal
approxPriceValence : Goal

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instDecidableEqGoal :

DecidableEq Goal

Equations

KaoEtAl2014PMFHyperbole.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoEtAl2014PMFHyperbole.instReprGoal.repr :

Goal → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instReprGoal :

Repr Goal

Equations

KaoEtAl2014PMFHyperbole.instReprGoal = { reprPrec := KaoEtAl2014PMFHyperbole.instReprGoal.repr }

@[implicit_reducible]

instance KaoEtAl2014PMFHyperbole.instFintypeGoal :

Fintype Goal

Equations

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

instance KaoEtAl2014PMFHyperbole.instNonemptyGoal :

Nonempty Goal

§1. Empirical priors (Experiments 3a, 3b) #

Counts elicited from MTurk participants. Per-item price priors and per-state affect priors. Both normalize per their respective conditions.

def KaoEtAl2014PMFHyperbole.pricePriorℕ (item : Item) :

PriceState → ℕ

Price prior P_S(s | item) as integer counts (Experiment 3a). Normalisation factor varies per item.

Equations

Instances For

def KaoEtAl2014PMFHyperbole.affectPriorℕ :

PriceState → Affect → ℕ

Affect prior P_A(a | s) as integer counts (Experiment 3b). Each price-state pair (none, notable) sums to 10000.

Equations

Instances For

§2. Cost (paper §"Materials and Methods") #

C(u) = 1 for round numbers (divisible by 10); C(u) = 3.4 for sharp numbers (fitted parameter; the paper notes the qualitative findings are robust across cost ratios in [1.1, 3.7]).

In our EReal-softmax substrate, cost subtracts from the score: score u = log(qudProjL0 ...) − cost u (in EReal)

This places the cost INSIDE the softmax score, where it modulates utterance choice without leaving the substrate. No new primitive needed — just a different score function.

noncomputable def KaoEtAl2014PMFHyperbole.costSharp :

ℝ

Sharp-utterance cost (paper-fitted ≈ 3.4, robust in [1.1, 3.7]).

Equations

KaoEtAl2014PMFHyperbole.costSharp = 17 / 5

Instances For

theorem KaoEtAl2014PMFHyperbole.costSharp_pos :

noncomputable def KaoEtAl2014PMFHyperbole.cost (u : PriceState) :

ℝ

Utterance cost. Round numbers have unit cost; sharp numbers carry costSharp ≈ 3.4 (fitted to halo data).

Equations

KaoEtAl2014PMFHyperbole.cost u = if u.isRound = true then 1 else KaoEtAl2014PMFHyperbole.costSharp

Instances For

theorem KaoEtAl2014PMFHyperbole.cost_pos (u : PriceState) :

0 < cost u

theorem KaoEtAl2014PMFHyperbole.cost_nonneg (u : PriceState) :

§3. Literal listener L0 (Eq. 9) #

L0(s, a | u) = P_A(a | s) if s = u, else 0. The literal listener combines the affect prior with the constraint that the price state must match the utterance.

noncomputable def KaoEtAl2014PMFHyperbole.L0Weight (u : PriceState) (w : World) :

ENNReal

L0 weight at world (s, a) given utterance u: the affect prior at (s, a), gated by s = u. Returns ℝ≥0∞.

Equations

KaoEtAl2014PMFHyperbole.L0Weight u w = if w.1 = u then ↑(KaoEtAl2014PMFHyperbole.affectPriorℕ w.1 w.2) / 10000 else 0

Instances For

theorem KaoEtAl2014PMFHyperbole.L0Weight_ne_zero_iff (u : PriceState) (w : World) :

L0Weight u w ≠ 0 ↔ w.1 = u

L0 weight is non-zero iff the utterance matches the world's price.

theorem KaoEtAl2014PMFHyperbole.L0Weight_ne_top (u : PriceState) (w : World) :

L0Weight u w ≠ ⊤

L0 weight is finite.

§4. QUD projection (Eq. 6) #

The goal g defines an equivalence relation on worlds: w ~_g w' iff g(w) = g(w'). The QUD-projected L0 weight at (g, u, w) is the sum of L0Weight u w' over all w' in the equivalence class containing w.

The architectural insight: when g projects information away (e.g., forgets price), the equivalence class enlarges, and qudProjL0 can be non-zero at w even when L0(u, w) = 0 — the speaker is "informative along the goal dimension" without being literally true.

def KaoEtAl2014PMFHyperbole.project (g : Goal) (w : World) :

ℕ

The goal projection: maps a world to its equivalence-class tag. Two worlds are QUD-equivalent under g iff project g w = project g w'.

Equations

One or more equations did not get rendered due to their size.
KaoEtAl2014PMFHyperbole.project KaoEtAl2014PMFHyperbole.Goal.price w = w.1.value
KaoEtAl2014PMFHyperbole.project KaoEtAl2014PMFHyperbole.Goal.valence w = match w.2 with | KaoEtAl2014PMFHyperbole.Affect.none => 0 | KaoEtAl2014PMFHyperbole.Affect.notable => 1
KaoEtAl2014PMFHyperbole.project KaoEtAl2014PMFHyperbole.Goal.approxPrice w = w.1.round.value

Instances For

theorem KaoEtAl2014PMFHyperbole.project_price_eq (w : World) :

↑(project Goal.price w) = Semantics.Numerals.Precision.projectPrecision Semantics.Numerals.Precision.PrecisionMode.exact ↑w.1.value

The price goal projects by the paper's exact meaning projection f_e: the substrate Precision.projectPrecision .exact.

theorem KaoEtAl2014PMFHyperbole.project_approxPrice_eq (w : World) :

↑(project Goal.approxPrice w) = Semantics.Numerals.Precision.projectPrecision Semantics.Numerals.Precision.PrecisionMode.approximate ↑w.1.value

The approxPrice goal projects by the paper's approximate meaning projection f_a: the substrate Precision.projectPrecision .approximate at base 10.

noncomputable def KaoEtAl2014PMFHyperbole.qudProjL0 (g : Goal) (u : PriceState) (w : World) :

ENNReal

QUD-projected L0: sum of L0Weight over the QUD-equivalence class of w under goal g. The denominator of the speaker softmax (Eq. 6 of paper).

Built from the parametric RSA.QUD.proj substrate.

Equations

KaoEtAl2014PMFHyperbole.qudProjL0 g u w = RSA.QUD.proj KaoEtAl2014PMFHyperbole.project (KaoEtAl2014PMFHyperbole.L0Weight u) g w

Instances For

theorem KaoEtAl2014PMFHyperbole.L0Weight_le_qudProjL0 (g : Goal) (u : PriceState) (w : World) :

L0Weight u w ≤ qudProjL0 g u w

Self-membership: w is in its own QUD-equivalence class, so qudProjL0 is bounded below by L0Weight u w.

§5. The headline theorem — what enables nonliteral interpretation #

The architectural claim: a literally-false utterance u (one where L0Weight u (s, a) = 0) can have positive qudProjL0 mass at (s, a) when there exists ANOTHER world (s', a') in the same QUD-equivalence class that IS literally true.

This is THE mechanism enabling hyperbole, halo, and all nonliteral interpretations in the paper. Goal inference broadens the speaker's "effective" support beyond literal truth.

theorem KaoEtAl2014PMFHyperbole.qudProjL0_pos_iff_exists_qud_class_member (g : Goal) (u : PriceState) (w : World) :

0 < qudProjL0 g u w ↔ ∃ w' ∈ {w' : World | project g w' = project g w}, 0 < L0Weight u w'

Headline Theorem (qudProjL0 support characterization): the QUD-projected L0 is positive at (s, a) under goal g iff some world in the same QUD-equivalence class has positive L0 weight — i.e., iff some literally-true (s', a') is QUD-equivalent.

This is the architectural mechanism for nonliteral interpretation. Without goal projection (identity goal), the equivalence class is just {(s, a)} itself, so qudProjL0 > 0 ↔ L0 > 0 ↔ s = u — only literally- true interpretations survive. With proper goals (e.g., affect-only), the equivalence class enlarges, and qudProjL0 > 0 can hold even when L0 = 0.

theorem KaoEtAl2014PMFHyperbole.qudProjL0_pos_of_nonliteral (g : Goal) (u : PriceState) (w : World) (_h_not_literal : L0Weight u w = 0) (h_qud_witness : ∃ w' ∈ {w' : World | project g w' = project g w}, w' ≠ w ∧ w'.1 = u) :

0 < qudProjL0 g u w

Specialization for nonliteral interpretation: a literally-false meaning (s, a) (with L0Weight u (s, a) = 0) can have positive QUD-projection mass iff some literally-true (s', a') is QUD-equivalent to (s, a) under goal g.

This is the precondition for the speaker softmax (and hence L1) to assign positive mass to (s, a) as an interpretation of u.

§6. Concrete demonstration: hyperbole at the affect-only goal #

The paper's central illustration: hearing "$10K" for a kettle (where literal $10K is unlikely), the listener can infer the speaker means something like "the kettle was overpriced" (notable affect at a low price). The mechanism: under the valence goal, the QUD-equivalence class of (s_low, .notable) includes (s_high, .notable), where the literal interpretation lives.

This concrete instance is the substantive content of nonliteral_support.

theorem KaoEtAl2014PMFHyperbole.hyperbole_emerges_at_valence_goal :

0 < qudProjL0 Goal.valence PriceState.s10000 (PriceState.s50, Affect.notable)

Hyperbole emerges from valence-goal QUD-projection: under the valence goal, the literally-false world (.s50, .notable) and the literally-true world (.s10000, .notable) are QUD-equivalent (both have project .valence = 1). So if the speaker says "$10K" (literally true only at .s10000), the QUD-projection at (.s50, .notable) is positive — enabling the hyperbolic interpretation "wait, the speaker means it was overpriced, not literally $10K."

§7. Paper findings (sorried — empirical-fit content) #

The 6 paper findings, stated as outer-measure inequalities for downstream discharge. Each requires the full L1 model (speaker + Bayes) plus numerical evaluation at Kao's empirical priors.

The architectural theorem above (hyperbole_emerges_at_valence_goal) captures the qualitative MECHANISM. The numerical findings quantify HOW MUCH the mechanism matters at specific priors — empirical-fit content rather than architectural content.

Future work: discharge via the Kao Metaphor PMF substrate pattern (L1_cat_fibre_lt_iff_inner_sum_lt analog adapted to (state, affect)).

For brevity, the 6 paper findings are not stated here as fully-typed theorems. They reduce to outer-measure inequalities on the L1 posterior at specific (item, utterance, world-event) instantiations:

affect_at_modal: L1(.s10000, .notable | "$10K") > L1(.s10000, .none | "$10K")
affect_marginal: L1.toOuterMeasure {(, .notable)} > L1.toOuterMeasure {(, .none)}
qud_valence: P_G(.valence | "$10K") > P_G(.price | "$10K") (under L1)
literal_correct: L1(.s50, .none | "$50") > L1(.s500, .none | "$50")
literal_not_hyperbolic: L1(.s50, .none | "$50") > L1(.s10000, .none | "$50")
halo_sharp_500: P(.s501 | "$501") > P(.s500 | "$500") -- precision asymmetry from cost

Each follows the substrate pattern: structural decomposition via PMF.posterior_toOuterMeasure_lt_iff_finset_score_lt, then numerical comparison at the specific priors.