Kao, Wu, Bergen and Goodman (2014): Nonliteral Understanding of Number Words

Kao, Wu, Bergen and Goodman model hyperbole on the RSA kernel pipeline. A meaning pairs a price state with the speaker's affect; the literal listener conditions the prior on the price named, a speaker with a communicative goal is informative about the goal's projection of the meaning and pays a higher cost for sharp numbers, and the pragmatic listener marginalizes the goal.

Main results

• KaoWuEtAl2014.listener_ne_zero_iff: a meaning receives positive posterior mass exactly when some goal of positive prior projects it into the cell of a meaning at which the utterance is literally true.
• KaoWuEtAl2014.hyperbole: a low price with affect is available under the affect goal.
• KaoWuEtAl2014.literal_of_price_goals, KaoWuEtAl2014.halo_of_price_goals: the comparison models of Fig. 2B.
• KaoWuEtAl2014.approximate_prefers_round: the halo effect of Fig. 3B rests on the cost.

Implementation notes

Priors are arguments: the price prior and the conditional affect prior of Experiments 3a and 3b enter as one probability measure on meanings, and the goal prior as a probability measure on goals, uniform in the paper. The model's numerical fits (Figs. 2 to 5) rest on the raw priors published as data rather than in the paper, and are not stated. The goals are the paper's, a precision projection composed with a relevance projection, the two affect-only goals coinciding (project_affect).

References

• [KWBG14]

inductive KaoWuEtAl2014.Precision : Type

The precision of a goal is exact, the paper's f_e, or approximate, f_a, which rounds the price to the nearest multiple of ten.

• exact : Precision
• approximate : Precision

@[instance_reducible]

instance KaoWuEtAl2014.instDecidableEqPrecision : DecidableEq Precision

Equations

• KaoWuEtAl2014.instDecidableEqPrecision x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoWuEtAl2014.instReprPrecision.repr : Precision → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KaoWuEtAl2014.instReprPrecision : Repr Precision

Equations

• KaoWuEtAl2014.instReprPrecision = { reprPrec := KaoWuEtAl2014.instReprPrecision.repr }

@[instance_reducible]

instance KaoWuEtAl2014.instFintypePrecision : Fintype Precision

Equations

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

inductive KaoWuEtAl2014.Price : Type

The price states of Materials and Methods are five round prices and their sharp neighbours.

• p50 : Price
• p51 : Price
• p500 : Price
• p501 : Price
• p1000 : Price
• p1001 : Price
• p5000 : Price
• p5001 : Price
• p10000 : Price
• p10001 : Price

@[instance_reducible]

instance KaoWuEtAl2014.instDecidableEqPrice : DecidableEq Price

Equations

• KaoWuEtAl2014.instDecidableEqPrice x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def KaoWuEtAl2014.instReprPrice.repr : Price → ℕ → Std.Format

Equations

• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p50 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p50")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p51 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p51")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p500 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p500")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p501 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p501")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p1000 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p1000")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p1001 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p1001")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p5000 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p5000")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p5001 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p5001")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p10000 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p10000")).group prec✝
• KaoWuEtAl2014.instReprPrice.repr KaoWuEtAl2014.Price.p10001 prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "KaoWuEtAl2014.Price.p10001")).group prec✝

@[instance_reducible]

instance KaoWuEtAl2014.instReprPrice : Repr Price

Equations

• KaoWuEtAl2014.instReprPrice = { reprPrec := KaoWuEtAl2014.instReprPrice.repr }

@[instance_reducible]

instance KaoWuEtAl2014.instFintypePrice : Fintype Price

Equations

• KaoWuEtAl2014.instFintypePrice = { elems := { val := ↑KaoWuEtAl2014.Price.enumList, nodup := KaoWuEtAl2014.Price.enumList_nodup }, complete := KaoWuEtAl2014.instFintypePrice._proof_1 }

def KaoWuEtAl2014.Price.value : Price → ℕ

The price in dollars.

Equations

• KaoWuEtAl2014.Price.p50.value = 50
• KaoWuEtAl2014.Price.p51.value = 51
• KaoWuEtAl2014.Price.p500.value = 500
• KaoWuEtAl2014.Price.p501.value = 501
• KaoWuEtAl2014.Price.p1000.value = 1000
• KaoWuEtAl2014.Price.p1001.value = 1001
• KaoWuEtAl2014.Price.p5000.value = 5000
• KaoWuEtAl2014.Price.p5001.value = 5001
• KaoWuEtAl2014.Price.p10000.value = 10000
• KaoWuEtAl2014.Price.p10001.value = 10001

def KaoWuEtAl2014.Price.IsRound (p : Price) : Prop

A round price is divisible by ten.

Equations

• p.IsRound = (10 ∣ p.value)

@[instance_reducible]

instance KaoWuEtAl2014.Price.instDecidablePredIsRound : DecidablePred IsRound

Equations

• x✝.instDecidablePredIsRound = { decide := decide (x✝.value % 10 = 0), reflects_decide := ⋯ }

def KaoWuEtAl2014.Price.round : Price → Price

The nearest round price, the paper's Round.

Equations

• KaoWuEtAl2014.Price.p50.round = KaoWuEtAl2014.Price.p50
• KaoWuEtAl2014.Price.p51.round = KaoWuEtAl2014.Price.p50
• KaoWuEtAl2014.Price.p500.round = KaoWuEtAl2014.Price.p500
• KaoWuEtAl2014.Price.p501.round = KaoWuEtAl2014.Price.p500
• KaoWuEtAl2014.Price.p1000.round = KaoWuEtAl2014.Price.p1000
• KaoWuEtAl2014.Price.p1001.round = KaoWuEtAl2014.Price.p1000
• KaoWuEtAl2014.Price.p5000.round = KaoWuEtAl2014.Price.p5000
• KaoWuEtAl2014.Price.p5001.round = KaoWuEtAl2014.Price.p5000
• KaoWuEtAl2014.Price.p10000.round = KaoWuEtAl2014.Price.p10000
• KaoWuEtAl2014.Price.p10001.round = KaoWuEtAl2014.Price.p10000

theorem KaoWuEtAl2014.Price.isRound_round (p : Price) : p.round.IsRound

@[simp]

theorem KaoWuEtAl2014.Price.round_round (p : Price) : p.round.round = p.round

theorem KaoWuEtAl2014.Price.value_round (p : Price) : ↑p.round.value = Degree.representative 10 ↑p.value

round is the substrate rounding to the nearest multiple of ten.

def KaoWuEtAl2014.Price.project : Precision → Price → Price

The precision projection f of a goal keeps the price exact or rounds it.

Equations

• KaoWuEtAl2014.Price.project KaoWuEtAl2014.Precision.exact x✝ = x✝
• KaoWuEtAl2014.Price.project KaoWuEtAl2014.Precision.approximate x✝ = x✝.round

@[instance_reducible]

instance KaoWuEtAl2014.Price.instMeasurableSpace : MeasurableSpace Price

Equations

• KaoWuEtAl2014.Price.instMeasurableSpace = ⊤

instance KaoWuEtAl2014.Price.instDiscreteMeasurableSpace : DiscreteMeasurableSpace Price

instance KaoWuEtAl2014.Price.instNonempty : Nonempty Price

@[reducible, inline]

abbrev KaoWuEtAl2014.Meaning : Type

A meaning pairs the price state with whether the speaker has an affect about it, the paper's M = S × A with A = {0, 1}.

Equations

• KaoWuEtAl2014.Meaning = (KaoWuEtAl2014.Price × Bool)

inductive KaoWuEtAl2014.Relevance : Type

The relevance projection r of a goal keeps the price, the affect, or both.

• price : Relevance
• affect : Relevance
• both : Relevance

@[instance_reducible]

instance KaoWuEtAl2014.instDecidableEqRelevance : DecidableEq Relevance

Equations

• KaoWuEtAl2014.instDecidableEqRelevance x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance KaoWuEtAl2014.instReprRelevance : Repr Relevance

Equations

• KaoWuEtAl2014.instReprRelevance = { reprPrec := KaoWuEtAl2014.instReprRelevance.repr }

def KaoWuEtAl2014.instReprRelevance.repr : Relevance → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance KaoWuEtAl2014.instFintypeRelevance : Fintype Relevance

Equations

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

@[instance_reducible]

instance KaoWuEtAl2014.instMeasurableSpaceRelevance : MeasurableSpace Relevance

Equations

• KaoWuEtAl2014.instMeasurableSpaceRelevance = ⊤

instance KaoWuEtAl2014.instDiscreteMeasurableSpaceRelevance : DiscreteMeasurableSpace Relevance

instance KaoWuEtAl2014.instNonemptyRelevance : Nonempty Relevance

@[instance_reducible]

instance KaoWuEtAl2014.instMeasurableSpacePrecision : MeasurableSpace Precision

Equations

• KaoWuEtAl2014.instMeasurableSpacePrecision = ⊤

instance KaoWuEtAl2014.instDiscreteMeasurableSpacePrecision : DiscreteMeasurableSpace Precision

instance KaoWuEtAl2014.instNonemptyPrecision : Nonempty Precision

@[reducible, inline]

abbrev KaoWuEtAl2014.Goal : Type

A goal composes a precision projection with a relevance projection, g(s, a) = r(f(s), a).

Equations

• KaoWuEtAl2014.Goal = (KaoWuEtAl2014.Precision × KaoWuEtAl2014.Relevance)

def KaoWuEtAl2014.project (g : Goal) (m : Meaning) : Option Price × Option Bool

The projection of a goal keeps the price component, exact or rounded, and the affect component, each when it is relevant.

Equations

• KaoWuEtAl2014.project g m = (if g.2 = KaoWuEtAl2014.Relevance.affect then none else some (KaoWuEtAl2014.Price.project g.1 m.1), if g.2 = KaoWuEtAl2014.Relevance.price then none else some m.2)

theorem KaoWuEtAl2014.project_affect (f f' : Precision) : project (f, Relevance.affect) = project (f', Relevance.affect)

The two affect-only goals coincide, as the paper notes.

def KaoWuEtAl2014.sem (u : Price) : Set Meaning

An utterance is true of a meaning when the price it names is the price state.

Equations

• KaoWuEtAl2014.sem u = {m : KaoWuEtAl2014.Meaning | m.1 = u}

theorem KaoWuEtAl2014.mem_sem {u : Price} {m : Meaning} : m ∈ sem u ↔ m.1 = u

noncomputable def KaoWuEtAl2014.L0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.Kernel Price Meaning

The literal listener conditions the prior on the price named, eq. 9.

Equations

• KaoWuEtAl2014.L0 μ = RSA.listener μ (RSA.truthful KaoWuEtAl2014.sem)

instance KaoWuEtAl2014.instIsFiniteKernelPriceMeaningL0 (μ : MeasureTheory.Measure Meaning) : ProbabilityTheory.IsFiniteKernel (L0 μ)

def KaoWuEtAl2014.cost (c : ℝ) (u : Price) : ℝ

The cost C(u) of eq. 7 is one at a round price and the fitted parameter c at a sharp one.

Equations

• KaoWuEtAl2014.cost c u = if u.IsRound then 1 else c

noncomputable def KaoWuEtAl2014.S1 (μ : MeasureTheory.Measure Meaning) (c : ℝ) (p : Meaning × Goal) : MeasureTheory.Measure Price

The goal-indexed speaker, eqs. 5 to 8, knows the answer to her goal and is informative about the literal listener's distribution over the topical subspace (eq. 6), at unit rationality, less the cost.

Equations

• KaoWuEtAl2014.S1 μ c p = (RSA.speaker 1 (KaoWuEtAl2014.cost c) (⇑((KaoWuEtAl2014.L0 μ).map (KaoWuEtAl2014.project p.2))) MeasureTheory.Measure.dirac) (KaoWuEtAl2014.project p.2 p.1)

instance KaoWuEtAl2014.instIsFiniteMeasurePriceS1 (μ : MeasureTheory.Measure Meaning) (c : ℝ) (p : Meaning × Goal) : MeasureTheory.IsFiniteMeasure (S1 μ c p)

noncomputable def KaoWuEtAl2014.L1 (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (c : ℝ) : ProbabilityTheory.Kernel Price (Meaning × Goal)

The pragmatic listener over meaning and goal, eq. 10, inverts the speaker against the product of the meaning prior and the goal prior; its first marginal is the meaning listener.

Equations

• KaoWuEtAl2014.L1 μ ν c = RSA.listener (μ.prod ν) (KaoWuEtAl2014.S1 μ c)

theorem KaoWuEtAl2014.listener_ne_zero_iff (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (c : ℝ) (u : Price) (m : Meaning) : ((L1 μ ν c) u).fst {m} ≠ 0 ↔ μ {m} ≠ 0 ∧ ∃ (g : Goal), ν {g} ≠ 0 ∧ ∃ (m' : Meaning), project g m' = project g m ∧ m'.1 = u ∧ μ {m'} ≠ 0

A meaning is in the support of the meaning listener at an utterance exactly when it has positive prior and, under some goal of positive prior, shares its answer with a meaning of positive prior at which the utterance is literally true.

theorem KaoWuEtAl2014.hyperbole (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (c : ℝ) (hν : ν {(Precision.exact, Relevance.affect)} ≠ 0) (h50 : μ {(Price.p50, true)} ≠ 0) (h10k : μ {(Price.p10000, true)} ≠ 0) : ((L1 μ ν c) Price.p10000).fst {(Price.p50, true)} ≠ 0

A low price with affect is a possible meaning of a high price under the affect goal whenever the prior gives mass to both meanings with affect, which is hyperbole.

theorem KaoWuEtAl2014.literal_of_price_goals (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (c : ℝ) (hν : ∀ (g : Goal), ν {g} ≠ 0 → g = (Precision.exact, Relevance.price)) {u : Price} {m : Meaning} (h : ((L1 μ ν c) u).fst {m} ≠ 0) : m.1 = u

A listener entertaining only the exact price goal, the first comparison model of Fig. 2B, interprets every utterance literally.

theorem KaoWuEtAl2014.halo_of_price_goals (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (ν : MeasureTheory.Measure Goal) [MeasureTheory.IsProbabilityMeasure ν] (c : ℝ) (hν : ∀ (g : Goal), ν {g} ≠ 0 → g.2 = Relevance.price) {u : Price} {m : Meaning} (h : ((L1 μ ν c) u).fst {m} ≠ 0) : m.1.round = u.round

A listener entertaining the price goals, exact or approximate, the second comparison model of Fig. 2B, reaches only the prices rounding to the utterance.

theorem KaoWuEtAl2014.map_L0_approximate (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] {u p : Price} (hμ : μ (sem u) ≠ 0) (hp : u.round = p.round) (a : Bool) : (((L0 μ).map (project (Precision.approximate, Relevance.price))) u) {project (Precision.approximate, Relevance.price) (p, a)} = 1

At an approximate price goal, the literal listener who hears a price of positive prior is certain of the answer at every meaning of the same round price.

theorem KaoWuEtAl2014.approximate_prefers_round (μ : MeasureTheory.Measure Meaning) [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ) {p : Price} (hp : ¬p.IsRound) (h₁ : μ (sem p) ≠ 0) (h₂ : μ (sem p.round) ≠ 0) (a : Bool) : (S1 μ c ((p, a), Precision.approximate, Relevance.price)).real {p} < (S1 μ c ((p, a), Precision.approximate, Relevance.price)).real {p.round} ↔ 1 < c

At an approximate price goal a sharp price projects with its round neighbour, so the speaker prefers the round utterance exactly when sharp numbers cost more, the cost mechanism of the halo effect (Fig. 3B).