Documentation

Linglib.Phenomena.Nonliteral.Hyperbole.KaoEtAl2014PMF

@cite{kao-etal-2014-hyperbole} on mathlib `PMF` — headline architectural theorem #

@cite{kao-etal-2014-hyperbole}

"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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqItem :

DecidableEq Item

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqItem x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprItem.repr :

Item → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprItem :

Repr Item

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprItem = { reprPrec := Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprItem.repr }

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instFintypeItem :

Fintype Item

Equations

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

inductive Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqPriceState :

DecidableEq PriceState

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqPriceState x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprPriceState :

Repr PriceState

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprPriceState = { reprPrec := Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprPriceState.repr }

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprPriceState.repr :

PriceState → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instFintypePriceState :

Fintype PriceState

Equations

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

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.PriceState.value :

PriceState → ℕ

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

Equations

Instances For

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.PriceState.isRound :

PriceState → Bool

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

Equations

Instances For

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.PriceState.round :

PriceState → PriceState

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

Equations

Instances For

inductive Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.Affect :

Binary affect: speaker has notable opinion, or none.

none : Affect
notable : Affect

Instances For

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqAffect :

DecidableEq Affect

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqAffect x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprAffect.repr :

Affect → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprAffect :

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprAffect = { reprPrec := Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprAffect.repr }

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instFintypeAffect :

Fintype Affect

Equations

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

@[reducible, inline]

abbrev Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.World :

World = (price state, affect).

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.World = (Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.PriceState × Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.Affect)

Instances For

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instNonemptyWorld :

Nonempty World

inductive Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqGoal :

DecidableEq Goal

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instDecidableEqGoal x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprGoal :

Repr Goal

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprGoal = { reprPrec := Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprGoal.repr }

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instReprGoal.repr :

Goal → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.instFintypeGoal :

Fintype Goal

Equations

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

instance Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.pricePriorℕ (item : Item) :

PriceState → ℕ

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

Equations

Instances For

def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.costSharp :

ℝ

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

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.costSharp = 17 / 5

Instances For

theorem Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.costSharp_pos :

noncomputable def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.cost (u : PriceState) :

ℝ

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

Equations

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.cost u = if u.isRound = true then 1 else Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.costSharp

Instances For

theorem Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.cost_pos (u : PriceState) :

0 < cost u

theorem Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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

Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.L0Weight u w = if w.1 = u then ↑(Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.affectPriorℕ w.1 w.2) / 10000 else 0

Instances For

theorem Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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.
Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.project Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.Goal.price w = w.1.value
Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.project Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.Goal.approxPrice w = w.1.round.value

Instances For

noncomputable def Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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

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

Instances For

theorem Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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 Phenomena.Nonliteral.Hyperbole.KaoEtAl2014.PMF.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.