Krifka (2007): Approximate interpretation of number words

Round number words invite approximate interpretations, one hundred meters against 103 meters. Krifka derives this without a general bias for approximation. His earlier bidirectional account paired a preference for simple expressions with one for approximate interpretations; this paper keeps truthfulness strict and lets expression economy apply only where there is a choice, which there is only under an approximate reading. A hearer then reasons strategically: a non-shortest expression signals a precise reading, and a short one is read approximately because the approximate reading covers more equally likely values. Where number words name points on scales of different granularity, the same reasoning picks the coarsest salient scale the reported value lies on, and halving a scale's width is the optimal refinement, adding exactly the values the coarser scale distorts most.

Main results

• division_of_labour: on the earlier account the superoptimal pairs are the simple expression read approximately and the complex one read precisely.
• winners_of_true_value: with truthfulness above conditional expression economy, a true value of 39 is reported as forty approximately or thirty-nine precisely, and 40 as forty on either reading.
• approximate_more_probable: on the uniform prior the approximate reading of forty covers nine times the mass of the precise one, the hearer's conservative choice.
• coarsest_scale_most_probable: given a reported value, the most probable aligned scale is the coarsest one through it, reading forty-five minutes at the quarter hours and forty at the five minutes.

Implementation notes

• Approximate readings are intervals, the halo [i - s, i + s], the paper's own simplification of its normal distributions; indistinguishability at approximation level 1/10 compares means within one standard deviation.
• The hearer's comparisons are stated on the joint measure over scale and value at the report events, since the posteriors over scales given one report share a normalizer.
• Each scale is credited with its full cell: the quarter-hour cell around 45 holds fifteen minutes where the paper prints 10r, and the approximate mass of forty on the uniform prior is 9/100 where the paper prints 0.08; neither difference affects a comparison.
• Expression costs are a parameter, with the paper's cost comparisons as hypotheses; the paper's own syllable and occurrence counts are the rows of Data/Experiments/Krifka2007.json.

References

• [Kri07a]
• [Kri09a]
• [Kri02]
• [Blu00]
• [JP01]
• [Sig88]

inductive Krifka2007.Reading : Type

A number word is read precisely or approximately.

• precise : Reading
• approximate : Reading

@[instance_reducible]

instance Krifka2007.instDecidableEqReading : DecidableEq Reading

Equations

• Krifka2007.instDecidableEqReading x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2007.instReprReading : Repr Reading

Equations

• Krifka2007.instReprReading = { reprPrec := Krifka2007.instReprReading.repr }

def Krifka2007.instReprReading.repr : Reading → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007.instReprReading.repr Krifka2007.Reading.precise prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Reading.precise")).group prec✝

@[instance_reducible]

instance Krifka2007.instFintypeReading : Fintype Reading

Equations

• Krifka2007.instFintypeReading = { elems := { val := ↑Krifka2007.Reading.enumList, nodup := Krifka2007.Reading.enumList_nodup }, complete := Krifka2007.instFintypeReading._proof_1 }

The earlier bidirectional account

inductive Krifka2007.Form : Type

A simple and a complex number word, one hundred and one hundred and three.

• simple : Form
• complex : Form

@[instance_reducible]

instance Krifka2007.instDecidableEqForm : DecidableEq Form

Equations

• Krifka2007.instDecidableEqForm x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Krifka2007.instReprForm.repr : Form → ℕ → Std.Format

Equations

• Krifka2007.instReprForm.repr Krifka2007.Form.simple prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Form.simple")).group prec✝
• Krifka2007.instReprForm.repr Krifka2007.Form.complex prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Form.complex")).group prec✝

@[instance_reducible]

instance Krifka2007.instReprForm : Repr Form

Equations

• Krifka2007.instReprForm = { reprPrec := Krifka2007.instReprForm.repr }

@[instance_reducible]

instance Krifka2007.instFintypeForm : Fintype Form

Equations

• Krifka2007.instFintypeForm = { elems := { val := ↑Krifka2007.Form.enumList, nodup := Krifka2007.Form.enumList_nodup }, complete := Krifka2007.instFintypeForm._proof_1 }

def Krifka2007.simpleExpression : Form × Reading → ℕ

The preference for simple expressions.

Equations

• Krifka2007.simpleExpression (Krifka2007.Form.simple, snd) = 0
• Krifka2007.simpleExpression (Krifka2007.Form.complex, snd) = 1

def Krifka2007.approximateInterpretation : Form × Reading → ℕ

The earlier account's preference for approximate interpretations.

Equations

• Krifka2007.approximateInterpretation (fst, Krifka2007.Reading.approximate) = 0
• Krifka2007.approximateInterpretation (fst, Krifka2007.Reading.precise) = 1

theorem Krifka2007.division_of_labour : BidirectionalOT.superoptimal Finset.univ (BidirectionalOT.profile [simpleExpression, approximateInterpretation]) = {(Form.simple, Reading.approximate), (Form.complex, Reading.precise)}

The superoptimal pairs of the earlier account read the simple form approximately and the complex form precisely, the division of pragmatic labour.

theorem Krifka2007.division_of_labour_without_simple_precise : BidirectionalOT.superoptimal (Finset.univ.erase (Form.simple, Reading.precise)) (BidirectionalOT.profile [simpleExpression, approximateInterpretation]) = {(Form.simple, Reading.approximate), (Form.complex, Reading.precise)}

The division of labour survives the objection that the simple form cannot truthfully compete for the precise meaning: dropping that pair leaves the same winners.

Truthfulness and conditional economy

inductive Krifka2007.Numeral : Type

The number words of the paper's tableau.

• thirtyNine : Numeral
• forty : Numeral

@[instance_reducible]

instance Krifka2007.instDecidableEqNumeral : DecidableEq Numeral

Equations

• Krifka2007.instDecidableEqNumeral x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance Krifka2007.instReprNumeral : Repr Numeral

Equations

• Krifka2007.instReprNumeral = { reprPrec := Krifka2007.instReprNumeral.repr }

def Krifka2007.instReprNumeral.repr : Numeral → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.
• Krifka2007.instReprNumeral.repr Krifka2007.Numeral.forty prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "Krifka2007.Numeral.forty")).group prec✝

@[instance_reducible]

instance Krifka2007.instFintypeNumeral : Fintype Numeral

Equations

• Krifka2007.instFintypeNumeral = { elems := { val := ↑Krifka2007.Numeral.enumList, nodup := Krifka2007.Numeral.enumList_nodup }, complete := Krifka2007.instFintypeNumeral._proof_1 }

def Krifka2007.Numeral.value : Numeral → ℕ

The value a number word names.

Equations

• Krifka2007.Numeral.thirtyNine.value = 39
• Krifka2007.Numeral.forty.value = 40

def Krifka2007.range (p : Numeral × Reading) : Set ℕ

A number word read precisely denotes its value, and read approximately the values within a deviation of two.

Equations

• Krifka2007.range p = match p.2 with | Krifka2007.Reading.precise => {p.1.value} | Krifka2007.Reading.approximate => {v : ℕ | v.dist p.1.value ≤ 2}

@[instance_reducible]

instance Krifka2007.instDecidableMemNatSetRange (v : ℕ) (p : Numeral × Reading) : Decidable (v ∈ range p)

Equations

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

def Krifka2007.inRange (v : ℕ) (p : Numeral × Reading) : ℕ

Truthfulness marks a report whose range misses the true value.

Equations

• Krifka2007.inRange v p = if v ∈ Krifka2007.range p then 0 else 1

def Krifka2007.economy (c : Numeral → ℕ) (p : Numeral × Reading) : ℕ

Expression economy marks an approximate report when a word of lower cost c covers the same value, and never marks a precise report, so it is operative only where there is a choice.

Equations

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

def Krifka2007.reportTableau (c : Numeral → ℕ) (v : ℕ) : OptimalityTheory.Tableau (Numeral × Reading) 2

The paper's tableau ranks truthfulness above economy, over both words on both readings.

Equations

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

theorem Krifka2007.winners_of_true_value {c : Numeral → ℕ} (h : c Numeral.forty < c Numeral.thirtyNine) : (reportTableau c 39).optimal = {(Numeral.forty, Reading.approximate), (Numeral.thirtyNine, Reading.precise)} ∧ (reportTableau c 40).optimal = {(Numeral.forty, Reading.approximate), (Numeral.forty, Reading.precise)}

With forty the cheaper word, a true value of 39 is reported as forty read approximately or thirty-nine read precisely, and a true value of 40 as forty on either reading.

Strategic communication

def Krifka2007.Indistinguishable (i i' : ℕ) : Prop

Two reported values are indistinguishable when their distance is within the standard deviation at approximation level 1/10.

Equations

• Krifka2007.Indistinguishable i i' = (10 * i'.dist i ≤ i)

@[instance_reducible]

instance Krifka2007.instDecidableIndistinguishable (i i' : ℕ) : Decidable (Indistinguishable i i')

Equations

• Krifka2007.instDecidableIndistinguishable i i' = { decide := (10 * i'.dist i).ble i, reflects_decide := ⋯ }

def Krifka2007.ConsistentWithApproximation (c : ℕ → ℕ) (i : ℕ) : Prop

A report of cost c is consistent with the approximate reading when the speaker could not have conveyed an indistinguishable value more cheaply.

Equations

• Krifka2007.ConsistentWithApproximation c i = ∀ (i' : ℕ), Krifka2007.Indistinguishable i i' → c i ≤ c i'

theorem Krifka2007.forty_approximate_thirtyEight_precise {c : ℕ → ℕ} (hc : ∀ (i : ℕ), 36 ≤ i → i ≤ 44 → i ≠ 40 → c 40 < c i) : ConsistentWithApproximation c 40 ∧ ¬ConsistentWithApproximation c 38

With forty the cheapest word of its halo, forty is consistent with the approximate reading and thirty-eight is not, so thirty-eight signals the precise one.

theorem Krifka2007.precise_mass : (ProbabilityTheory.uniformOn ↑(Finset.Icc 1 100)) {40} = 1 / 100

On the uniform prior over the reportable values, the precise reading of forty has mass one in a hundred.

theorem Krifka2007.approximate_mass : (ProbabilityTheory.uniformOn ↑(Finset.Icc 1 100)) (Set.Icc 36 44) = 9 / 100

The approximate reading of forty covers its halo, nine values; the paper prints 0.08, the width of the halo.

theorem Krifka2007.approximate_more_probable : (ProbabilityTheory.uniformOn ↑(Finset.Icc 1 100)) {40} < (ProbabilityTheory.uniformOn ↑(Finset.Icc 1 100)) (Set.Icc 36 44)

Hearing forty, the approximate reading is the conservative hypothesis, covering more of the prior than the precise one.

Choosing a scale

def Krifka2007.reportedOn {W : Finset ℤ} (w : ↥W) (n : ℤ) : Set (↥W × ℝ)

The speaker chooses the scale of width w and reports the scale point nearest the value as n.

Equations

• Krifka2007.reportedOn w n = {w} ×ˢ (Degree.representative ↑↑w ⁻¹' {↑n})

theorem Krifka2007.measure_reportedOn_of_dvd {W : Finset ℤ} (μs : MeasureTheory.Measure ↥W) (ν : MeasureTheory.Measure ℝ) {r : ENNReal} {I : Set ℝ} {n : ℤ} [MeasureTheory.SFinite ν] (hν : ∀ ⦃s : Set ℝ⦄, MeasurableSet s → s ⊆ I → ν s = r * MeasureTheory.volume s) {w : ↥W} (hw : 0 < ↑w) (hI : Set.Ico (↑n - ↑↑w / 2) (↑n + ↑↑w / 2) ⊆ I) (h : ↑w ∣ n) : (μs.prod ν) (reportedOn w n) = μs {w} * (r * ENNReal.ofReal ↑↑w)

A report on a scale through n has the mass of the scale times the cell around n, under a scale prior μs and a value prior of density r on I.

theorem Krifka2007.measure_reportedOn_of_not_dvd {W : Finset ℤ} (μs : MeasureTheory.Measure ↥W) (ν : MeasureTheory.Measure ℝ) {n : ℤ} {w : ↥W} (h : ¬↑w ∣ n) : (μs.prod ν) (reportedOn w n) = 0

A value is never reported on a scale it does not lie on.

theorem Krifka2007.coarsest_scale_most_probable {W : Finset ℤ} (μs : MeasureTheory.Measure ↥W) (ν : MeasureTheory.Measure ℝ) {r : ENNReal} {I : Set ℝ} {n : ℤ} [MeasureTheory.SFinite ν] (hν : ∀ ⦃s : Set ℝ⦄, MeasurableSet s → s ⊆ I → ν s = r * MeasureTheory.volume s) (hr : r ≠ 0) (hr' : r ≠ ⊤) (hpos : ∀ w ∈ W, 0 < w) (hW : ∀ a ∈ W, ∀ b ∈ W, a ∣ b ∨ b ∣ a) (hs : ∀ (v w : ↥W), μs {v} = μs {w}) (hs0 : ∀ (w : ↥W), μs {w} ≠ 0) (hs' : ∀ (w : ↥W), μs {w} ≠ ⊤) (hI : ∀ (w : ↥W), Set.Ico (↑n - ↑↑w / 2) (↑n + ↑↑w / 2) ⊆ I) (hne : {x ∈ W | x ∣ n}.Nonempty) {w : ↥W} : (∀ (v : ↥W), (μs.prod ν) (reportedOn v n) ≤ (μs.prod ν) (reportedOn w n)) ↔ ↑w = Numerals.Roundness.scaleLcm W n

Hearing n on aligned scales with equal priors, the most probable scale is the coarsest one through n: forty-five minutes is read at the quarter hours and forty at the five minutes.

def Krifka2007.minuteScales : Finset ℤ

The minute scales count hours, half hours, quarter hours, five minutes and minutes.

Equations

• Krifka2007.minuteScales = {60, 30, 15, 5, 1}

theorem Krifka2007.fortyFive_quarterHours_forty_fiveMinutes : Numerals.Roundness.scaleLcm minuteScales 45 = 15 ∧ Numerals.Roundness.scaleLcm minuteScales 40 = 5

On the minute scales, 45 is read at the quarter hours and 40 at the five minutes, the coarsest scales each lies on.

Simplicity of expression and of representation

def Krifka2007.averageSyllables (s : SyllableScale) : ℚ

The average syllables per number word on a scale.

Equations

• Krifka2007.averageSyllables s = ↑(Krifka2007.syllableCounts s).syllables / ↑(Krifka2007.syllableCounts s).words

theorem Krifka2007.ser_decimal_scales : averageSyllables SyllableScale.tens < averageSyllables SyllableScale.fives ∧ averageSyllables SyllableScale.fives < averageSyllables SyllableScale.ones ∧ averageSyllables SyllableScale.ones < averageSyllables SyllableScale.threes

Among the decimal scales the coarser the scale, the simpler its number words on average, while the scale of threes, which no refinement of decimal granularity yields, is costlier than all of them.

theorem Krifka2007.months_violate_ser : averageSyllables SyllableScale.monthsByOne < averageSyllables SyllableScale.monthsCoarse

The scales for children's ages in months break the alignment, the coarser scale having the costlier words.

theorem Krifka2007.fifty_follows_the_language : ((counts Word.foerti).count < (counts Word.femti).count ∧ (counts Word.seksti).count < (counts Word.femti).count) ∧ (counts Word.halvtreds).count < (counts Word.fyrre).count ∧ (counts Word.halvtreds).count < (counts Word.tres).count

In decimal Norwegian the word for fifty is used more than those for forty and sixty; in vigesimal Danish, where fifty is the complex half-score form, less. Approximate use follows the simple forms of the language itself.

Refining by half

theorem Krifka2007.halving_adds_most_distorted {d : ℝ} : |d - Degree.representative 10 d| = 5 ↔ d ∈ AddSubgroup.zmultiples 5 ∧ d ∉ AddSubgroup.zmultiples 10

Halving the scale of tens, the optimal refinement, adds exactly the values the tens distort most, those reported a full five away.