Cummins (2015): Constraints on numerical expressions

Cummins models the choice of a numerically quantified expression as classical Optimality Theory. Six violable constraints, informativeness, granularity, quantifier simplicity, numeral salience, numeral priming and quantifier priming, evaluate the candidate expressions against the speaker's knowledge and the preceding context, and a speaker's total ranking selects one, so that apparent variation is variation across rankings and contexts. Round numerals are salient by Jansen and Pollmann's k-ness, a candidate incurring a subset of a rival's violations is preferred under every ranking, and a hearer who presumes the utterance optimal infers that an alternative bounding it in this way was not available to the speaker: more than n implicates not more than m for any greater m at least as salient and at the same granularity level, unless n was primed.

We derive the constraints' violations from the numeral and the context, reproduce the book's toy and correction tableaux from them and its approximation tableaux from their printed marks, and prove the bounding implicature and the exact condition for its attenuation under priming for arbitrary numerals.

Implementation notes

• Numeral salience uses the book's k-ness with a zero exponent admitted, under which 20 and 100 are entirely round. The book prints 50 as satisfying salience, though by its definition 50 lacks 2-ness, which changes no comparison in its tableaux.
• Quantifier simplicity follows the book's simplifying assumption that a comparative incurs no violation and a superlative one; exactly and about incur one, as its tableaux print.
• Informativeness reads a comparative or superlative against its own bound, the book's bound under discussion, and the other forms at their numeral. The informativeness marks of the approximation tableaux, which the book says do not follow from its definition, are entered as printed, a parenthesized star counting as one, with entire roundness as the criterion for the ambiguity mark that fits them.
• The book assigns no numeric granularity levels to cardinals; granularityLevel counts trailing zeros, and an unset level is met by every numeral, as the book allows.

References

• C. Cummins, Constraints on numerical expressions (2015)
• A. Prince, P. Smolensky, Optimality Theory: constraint interaction in generative grammar (1993)
• C. J. M. Jansen, M. M. W. Pollmann, On round numbers: pragmatic aspects of numerical expressions (2001)
• M. Krifka, Approximate interpretations of number words: a case for strategic communication (2009)
• C. Cummins, U. Sauerland, S. Solt, Granularity and scalar implicature in numerical expressions (2012)

Numeral salience (§2.4.4)

def Cummins2015.roundness (n : ℕ) : ℕ

The roundness of a numeral counts the kinds of k-ness, 10-, 5-, 2- and 2½-ness, it exhibits, the zero exponent admitted (definition (13)).

Equations

• Cummins2015.roundness n = Numerals.Roundness.score (Numerals.Roundness.Kness.Holds 0) n

theorem Cummins2015.roundness_le_four (n : ℕ) : roundness n ≤ 4

def Cummins2015.EntirelyRound (n : ℕ) : Prop

An entirely round numeral exhibits every kind of k-ness.

Equations

• Cummins2015.EntirelyRound n = (Cummins2015.roundness n = 4)

@[instance_reducible]

instance Cummins2015.instDecidablePredNatEntirelyRound : DecidablePred EntirelyRound

Equations

• Cummins2015.instDecidablePredNatEntirelyRound x✝ = { decide := (Cummins2015.roundness x✝).beq 4, reflects_decide := ⋯ }

Candidates, contexts and the six constraints (§2.4)

inductive Cummins2015.Form : Type

The quantifier of a candidate expression.

• bare : Form
• exactly : Form
• about : Form
• moreThan : Form
• atLeast : Form
• fewerThan : Form
• atMost : Form

@[instance_reducible]

instance Cummins2015.instDecidableEqForm : DecidableEq Form

Equations

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

def Cummins2015.Form.complexity : Form → ℕ

The bare numeral and the comparatives are simplest, the other modifiers and the superlatives one degree more complex (§2.4.3, §4.9).

Equations

• Cummins2015.Form.bare.complexity = 0
• Cummins2015.Form.moreThan.complexity = 0
• Cummins2015.Form.fewerThan.complexity = 0
• Cummins2015.Form.exactly.complexity = 1
• Cummins2015.Form.about.complexity = 1
• Cummins2015.Form.atLeast.complexity = 1
• Cummins2015.Form.atMost.complexity = 1

structure Cummins2015.Candidate : Type

A candidate expression applies a quantifier to a numeral.

• form : Form

  The quantifier.

• numeral : ℕ

  The numeral.

def Cummins2015.instDecidableEqCandidate.decEq (x✝ x✝¹ : Candidate) : Decidable (x✝ = x✝¹)

Equations

• Cummins2015.instDecidableEqCandidate.decEq { form := a, numeral := a_1 } { form := b, numeral := b_1 } = if h : a = b then h ▸ if h : a_1 = b_1 then h ▸ isTrue ⋯ else isFalse ⋯ else isFalse ⋯

@[instance_reducible]

instance Cummins2015.instDecidableEqCandidate : DecidableEq Candidate

Equations

• Cummins2015.instDecidableEqCandidate = Cummins2015.instDecidableEqCandidate.decEq

structure Cummins2015.Context : Type

The context of utterance records the bounds of the value under discussion the speaker knows, the granularity level the context sets, if any, and the primed numeral and quantifier.

• lo : Option ℕ

  The lower bound the speaker knows.

• hi : Option ℕ

  The upper bound the speaker knows.

• granularity : Option ℕ

  The granularity level the context sets.

• primedNumeral : Option ℕ

  The numeral activated in the prior context.

• primedForm : Option Form

  The quantifier activated in the prior context.

def Cummins2015.info (ctx : Context) : OptimalityTheory.Constraint Candidate

Informativeness assigns one violation for each value the expression admits that the speaker's knowledge excludes (constraint 1). A comparative or superlative puts its own bound under discussion; the other forms are read at their numeral.

Equations

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

def Cummins2015.moreThan (n : ℕ) : Candidate

more than n.

Equations

• Cummins2015.moreThan n = { form := Cummins2015.Form.moreThan, numeral := n }

def Cummins2015.bare (n : ℕ) : Candidate

The bare numeral.

Equations

• Cummins2015.bare n = { form := Cummins2015.Form.bare, numeral := n }

def Cummins2015.exactly (n : ℕ) : Candidate

exactly n.

Equations

• Cummins2015.exactly n = { form := Cummins2015.Form.exactly, numeral := n }

def Cummins2015.about (n : ℕ) : Candidate

about n.

Equations

• Cummins2015.about n = { form := Cummins2015.Form.about, numeral := n }

def Cummins2015.qsimp : OptimalityTheory.Constraint Candidate

Quantifier simplicity assigns one violation per degree of complexity (constraint 3).

Equations

• Cummins2015.qsimp c = c.form.complexity

def Cummins2015.nsal : OptimalityTheory.Constraint Candidate

Numeral salience assigns one violation for each kind of k-ness the numeral lacks (constraint 4).

Equations

• Cummins2015.nsal c = 4 - Cummins2015.roundness c.numeral

def Cummins2015.granularityLevel (n : ℕ) : ℕ

The decimal granularity level of a numeral counts its trailing zeros, up to thousands.

Equations

• Cummins2015.granularityLevel n = if n = 0 then 0 else if 1000 ∣ n then 3 else if 100 ∣ n then 2 else if 10 ∣ n then 1 else 0

theorem Cummins2015.pow_granularityLevel_eq_scaleLcm {n : ℕ} (hn : n ≠ 0) : 10 ^ granularityLevel n = Numerals.Roundness.scaleLcm {1000, 100, 10, 1} ↑n

The granularity level of a nonzero numeral indexes the coarsest decimal scale through it, up to thousands, the scale [Kri09a]'s hearer reads it at.

def Cummins2015.gran (ctx : Context) : OptimalityTheory.Constraint Candidate

Granularity assigns one violation per level of mismatch with the level the context sets, an unset level being met by every numeral (constraint 2).

Equations

• Cummins2015.gran ctx c = ctx.granularity.elim 0 (Cummins2015.granularityLevel c.numeral).dist

def Cummins2015.npri (ctx : Context) : OptimalityTheory.Constraint Candidate

Numeral priming assigns a violation when a numeral is primed and another is used (constraint 5).

Equations

• Cummins2015.npri ctx c = match ctx.primedNumeral with | some p => if c.numeral = p then 0 else 1 | none => 0

def Cummins2015.qpri (ctx : Context) : OptimalityTheory.Constraint Candidate

Quantifier priming assigns a violation when a quantifier is primed and another is used (constraint 6).

Equations

• Cummins2015.qpri ctx c = match ctx.primedForm with | some f => if c.form = f then 0 else 1 | none => 0

def Cummins2015.con (ctx : Context) : OptimalityTheory.ConstraintSet Candidate (Fin 6)

The six constraints, in the book's order, are informativeness, granularity, quantifier simplicity, numeral salience, numeral priming and quantifier priming.

Equations

• Cummins2015.con ctx = ![Cummins2015.info ctx, Cummins2015.gran ctx, Cummins2015.qsimp, Cummins2015.nsal, Cummins2015.npri ctx, Cummins2015.qpri ctx]

Constraint interaction in the toy system (§3.1, Tables 3.1–3.3)

def Cummins2015.toy (ctx : Context) : OptimalityTheory.ConstraintSet Candidate (Fin 3)

The toy system ranks informativeness, numeral salience and numeral priming.

Equations

• Cummins2015.toy ctx = ![Cummins2015.info ctx, Cummins2015.nsal, Cummins2015.npri ctx]

def Cummins2015.atLeast22 : Context

The speaker knows the value to be at least 22.

Equations

• Cummins2015.atLeast22 = { lo := some 22 }

def Cummins2015.atLeast22Primed : Context

The same, with 21 contextually salient.

Equations

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

theorem Cummins2015.atLeast22_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (toy atLeast22) r [moreThan 21, moreThan 20] atLeast22_optimal._proof_1).optimal = if r.Dominates 0 1 then {moreThan 21} else {moreThan 20}

Unprimed (Table 3.1), a speaker ranking informativeness above salience prefers more than 21 and one ranking salience above informativeness more than 20; priming, violated by neither, never adjudicates (Table 3.3).

theorem Cummins2015.atLeast22Primed_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (toy atLeast22Primed) r [moreThan 21, moreThan 20] atLeast22_optimal._proof_1).optimal = if r.Dominates 1 0 ∧ r.Dominates 1 2 then {moreThan 20} else {moreThan 21}

With 21 salient (Table 3.2), only a speaker ranking salience above both informativeness and priming keeps more than 20 (Table 3.3).

def Cummins2015.primingFirst : OptimalityTheory.Ranking (Fin 3) 3

Priming over salience over informativeness, the last ranking of Table 3.3.

Equations

• Cummins2015.primingFirst = Equiv.swap 0 2

theorem Cummins2015.primingFirst_optimal : (OptimalityTheory.Tableau.ofPerm (toy atLeast22) primingFirst [moreThan 21, moreThan 20] atLeast22_optimal._proof_1).optimal = {moreThan 20} ∧ (OptimalityTheory.Tableau.ofPerm (toy atLeast22Primed) primingFirst [moreThan 21, moreThan 20] atLeast22_optimal._proof_1).optimal = {moreThan 21}

A speaker ranking priming over salience over informativeness prefers more than 20 unprimed and more than 21 primed: variation within a speaker across contexts.

Approximation (§3.3.1, Tables 3.4–3.8)

inductive Cummins2015.Situation : Type

The value the speaker means to convey, exact or approximate.

• exact (n : ℕ) : Situation

  Exactly n.

• about (n : ℕ) : Situation

  Approximately n.

def Cummins2015.Situation.info : Situation → OptimalityTheory.Constraint Candidate

Informativeness as the approximation tableaux read it is violated once by an expression whose quantifier or numeral misfits the value, and once more by a bare entirely round numeral, ambiguous between precise and approximate readings. The book prints the ambiguity mark for 100 and not for 50; entire roundness is the criterion that fits.

Equations

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

def Cummins2015.approx (s : Situation) : OptimalityTheory.ConstraintSet Candidate (Fin 3)

The approximation system ranks informativeness, numeral salience and quantifier simplicity.

Equations

• Cummins2015.approx s = ![s.info, Cummins2015.nsal, Cummins2015.qsimp]

theorem Cummins2015.bare_notMem_optimal_of_roundness_lt {n m : ℕ} (hmn : roundness m < roundness n) (r : OptimalityTheory.Ranking (Fin 3) 3) {cands : List Candidate} (hc : bare n ∈ cands) (h : cands ≠ []) : bare m ∉ (OptimalityTheory.Tableau.ofPerm (approx (Situation.exact n)) r cands h).optimal

For an exact value the rounder numeral harmonically bounds a less round one, as 50 bounds 51 (Table 3.4).

theorem Cummins2015.exact51_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (approx (Situation.exact 51)) r [bare 50, bare 51] exact51_optimal._proof_1).optimal = if r.Dominates 0 1 then {bare 51} else {bare 50}

For the exact value 51, informativeness above salience prefers 51 and salience above informativeness 50 (Table 3.5).

theorem Cummins2015.exact100_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (approx (Situation.exact 100)) r [bare 100, exactly 100, about 100, about 99] exact100_optimal._proof_1).optimal = if r.Dominates 0 2 then {exactly 100} else {bare 100}

For the exact value 100, 100 bounds about 100, both bound about 99, and the choice is between exactly 100, for informativeness above simplicity, and 100 (Table 3.6).

theorem Cummins2015.about100_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (approx (Situation.about 100)) r [bare 100, about 100] about100_optimal._proof_1).optimal = if r.Dominates 0 2 then {about 100} else {bare 100}

For the approximate value 100, informativeness above simplicity prefers about 100 and simplicity above informativeness 100 (Table 3.7).

theorem Cummins2015.exact99_optimal (r : OptimalityTheory.Ranking (Fin 3) 3) : (OptimalityTheory.Tableau.ofPerm (approx (Situation.exact 99)) r [bare 99, exactly 99, bare 100, about 100] exact99_optimal._proof_1).optimal = if r.Dominates 0 1 then {bare 99} else if r.Dominates 2 0 then {bare 100} else {about 100}

For the exact value 99, 99 bounds exactly 99, and the winner is 99 when informativeness dominates salience, 100 when simplicity dominates informativeness, and about 100 otherwise (Table 3.8).

Corrections (§3.3.2, Tables 3.9–3.10)

inductive Cummins2015.Correction : Type

The four maximally informative corrections to a description of boxes holding n or n + 1 items ((38)–(41)).

• moreThan : Correction

  more than n − 1.

• atLeast : Correction

  at least n.

• atMost : Correction

  at most n + 1.

• fewerThan : Correction

  fewer than n + 2.

@[instance_reducible]

instance Cummins2015.instDecidableEqCorrection : DecidableEq Correction

Equations

• Cummins2015.instDecidableEqCorrection x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Cummins2015.Correction.candidate (n : ℕ) : Correction → Candidate

Each correction is a candidate, more than n − 1, at least n, at most n + 1 or fewer than n + 2.

Equations

• Cummins2015.Correction.candidate n Cummins2015.Correction.moreThan = { form := Cummins2015.Form.moreThan, numeral := n - 1 }
• Cummins2015.Correction.candidate n Cummins2015.Correction.atLeast = { form := Cummins2015.Form.atLeast, numeral := n }
• Cummins2015.Correction.candidate n Cummins2015.Correction.atMost = { form := Cummins2015.Form.atMost, numeral := n + 1 }
• Cummins2015.Correction.candidate n Cummins2015.Correction.fewerThan = { form := Cummins2015.Form.fewerThan, numeral := n + 2 }

def Cummins2015.Correction.all : List Correction

The candidate list of the tableaux.

Equations

• Cummins2015.Correction.all = [Cummins2015.Correction.moreThan, Cummins2015.Correction.atLeast, Cummins2015.Correction.atMost, Cummins2015.Correction.fewerThan]

def Cummins2015.correctionContext (n : ℕ) (form : Form) (numeral : ℕ) : Context

The speaker knows each box holds n or n + 1 items, and the description corrected primed its quantifier and numeral.

Equations

• Cummins2015.correctionContext n form numeral = { lo := some n, hi := some (n + 1), primedNumeral := some numeral, primedForm := some form }

def Cummins2015.corr (ctx : Context) : OptimalityTheory.ConstraintSet Candidate (Fin 4)

The correction system ranks quantifier priming, numeral priming, quantifier simplicity and informativeness.

Equations

• Cummins2015.corr ctx = ![Cummins2015.qpri ctx, Cummins2015.npri ctx, Cummins2015.qsimp, Cummins2015.info ctx]

def Cummins2015.corrOn (ctx : Context) (n : ℕ) : OptimalityTheory.ConstraintSet Correction (Fin 4)

The correction system on the four corrections.

Equations

• Cummins2015.corrOn ctx n = OptimalityTheory.ConstraintSet.comap (Cummins2015.Correction.candidate n) (Cummins2015.corr ctx)

def Cummins2015.table3_9 : OptimalityTheory.ConstraintSet Correction (Fin 4)

The printed marks of Table 3.9, after more than n, set quantifier and numeral priming against the corrections that change them and simplicity against the superlatives.

Equations

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

def Cummins2015.table3_10 : OptimalityTheory.ConstraintSet Correction (Fin 4)

The printed marks of Table 3.10, after at least n − 1.

Equations

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

theorem Cummins2015.corrOn_moreThan {n : ℕ} (hn : 1 ≤ n) : corrOn (correctionContext n Form.moreThan n) n = table3_9

The corrections' violations after more than n are those of Table 3.9.

theorem Cummins2015.corrOn_atLeast {n : ℕ} (hn : 1 ≤ n) : corrOn (correctionContext n Form.atLeast (n - 1)) n = table3_10

The corrections' violations after at least n − 1 are those of Table 3.10.

theorem Cummins2015.moreThan_correction_optimal {n : ℕ} (hn : 1 ≤ n) (r : OptimalityTheory.Ranking (Fin 4) 4) : (OptimalityTheory.Tableau.ofPerm (corrOn (correctionContext n Form.moreThan n) n) r Correction.all moreThan_correction_optimal._proof_1).optimal = if r.Dominates 0 1 ∨ r.Dominates 2 1 then {Correction.moreThan} else {Correction.atLeast}

After more than n, more than n − 1 bounds at most n + 1 and fewer than n + 2, and wins when quantifier priming or simplicity dominates numeral priming, at least n winning when numeral priming dominates both.

theorem Cummins2015.atLeast_correction_optimal {n : ℕ} (hn : 1 ≤ n) (r : OptimalityTheory.Ranking (Fin 4) 4) : (OptimalityTheory.Tableau.ofPerm (corrOn (correctionContext n Form.atLeast (n - 1)) n) r Correction.all moreThan_correction_optimal._proof_1).optimal = if r.Dominates 1 0 ∨ r.Dominates 2 0 then {Correction.moreThan} else {Correction.atLeast}

After at least n − 1, more than n − 1 wins when numeral priming or simplicity dominates quantifier priming, at least n when quantifier priming dominates both.

The hearer, and the implicature of more than n (§3.4, §5.3, §5.4)

theorem Cummins2015.about100_notMem_optimal_of_exact (r : OptimalityTheory.Ranking (Fin 3) 3) : about 100 ∉ (OptimalityTheory.Tableau.ofPerm (approx (Situation.exact 100)) r [bare 100, about 100] about100_optimal._proof_1).optimal

About 100 is never optimal for a speaker who knows the value to be exactly 100, so its use signals imprecision.

def Cummins2015.StrongerAlternative (ctx : Context) (n m : ℕ) : Prop

In a context, more than m is a stronger alternative to more than n when n < m and m is at least as salient as n and at its granularity level, if the context sets one.

Equations

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

@[instance_reducible]

instance Cummins2015.instDecidableStrongerAlternative (ctx : Context) (n m : ℕ) : Decidable (StrongerAlternative ctx n m)

Equations

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

theorem Cummins2015.moreThan_notMem_optimal {ctx : Context} {L n m : ℕ} (hlo : ctx.lo = some L) (halt : StrongerAlternative ctx n m) (hm : m < L) (hp : ctx.primedNumeral ≠ some n) (r : OptimalityTheory.Ranking (Fin 6) 6) {cands : List Candidate} (hc : moreThan m ∈ cands) (h : cands ≠ []) : moreThan n ∉ (OptimalityTheory.Tableau.ofPerm (con ctx) r cands h).optimal

A stronger alternative more than m below the speaker's bound bounds more than n when n is not primed, so more than n implicates that more than m was not assertable, the granularity-scale implicature of [CSS12].

theorem Cummins2015.moreThan_optimal_iff_of_primed {ctx : Context} {L n m : ℕ} (hlo : ctx.lo = some L) (halt : StrongerAlternative ctx n m) (hm : m < L) (hp : ctx.primedNumeral = some n) (r : OptimalityTheory.Ranking (Fin 6) 6) : (OptimalityTheory.Tableau.ofPerm (con ctx) r [moreThan n, moreThan m] ⋯).optimal = {moreThan n} ↔ r.Dominates 4 0 ∧ (roundness n < roundness m → r.Dominates 4 3)

With n primed, more than n is the sole winner against more than m iff numeral priming dominates informativeness and, when m is the rounder, numeral salience. The book's condition, priming above informativeness (§5.4), suffices only for equally salient pairs; on its own more than 70 ~ more than 80, 80 is the rounder.