[Cum15]: OT constraints on numerically quantified expressions

[Cum15] [JP01] [PS93]

[Cum15] models the choice of numerically quantified expressions as classical Optimality Theory: six violable constraints — informativeness (INFO), quantifier simplicity (QSIMP), numeral salience (NSAL), granularity (GRAN), numeral priming (NPRI), and quantifier priming (QPRI) — evaluate candidate expressions against a context, and each speaker's total ranking deterministically selects a winner, so apparent probabilistic variation is cross-speaker (and cross-context) ranking variation.

The constraint set runs through the project OT engine: the book's worked three-constraint tableaux (INFO, NSAL, NPRI over rival more than n bounds, with and without a primed numeral) are decide-checked Tableau.optimal computations, and the book's harmonic-bounding argument — a candidate incurring a subset of a rival's violations is preferred under any constraint ranking — is proved for arbitrary constraint systems and instantiated in the toy system.

NSAL follows the book: one violation per missing [JP01] k-ness type (10-, 5-, 2-, 2.5-ness; max 4). kTypeCount uses the substrate predicates, whose witness search starts at base exponent 1 rather than [JP01]'s 0 (Studies/JansenPollmann2001.lean records the divergence); the book leaves the exact roundness inventory open. The substrate's six-property roundnessScore decomposes as kTypeCount plus the two raw divisibility indicators (roundnessScore_eq_kTypeCount_add) — the properties the book sets aside as non-diagnostic of salience.

NSAL: numeral salience as missing k-ness types

def Cummins2015.kTypeCount (n : ℕ) : ℕ

Count of [JP01] k-ness types (10-, 5-, 2-, 2.5-ness) that n exhibits (0–4). [Cum15] takes an entirely round number to be one exhibiting all four.

Equations

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

theorem Cummins2015.kTypeCount_le_four (n : ℕ) : kTypeCount n ≤ 4

def Cummins2015.nsalViolations (n : ℕ) : ℕ

NSAL violations ([Cum15]'s numeral salience constraint): one per missing k-ness type. Entirely round numbers (100, 1000) incur none; numbers with no k-ness incur the maximum of four.

Equations

• Cummins2015.nsalViolations n = 4 - Cummins2015.kTypeCount n

theorem Cummins2015.nsalViolations_add_kTypeCount (n : ℕ) : nsalViolations n + kTypeCount n = 4

NSAL violations complement the k-type count.

theorem Cummins2015.nsalViolations_lt_iff {n₁ n₂ : ℕ} : nsalViolations n₁ < nsalViolations n₂ ↔ kTypeCount n₂ < kTypeCount n₁

Salience comparisons invert k-type comparisons: strictly more k-ness types is strictly fewer NSAL violations.

theorem Cummins2015.roundnessScore_eq_kTypeCount_add (n : ℕ) : Semantics.Numerals.Roundness.roundnessScore n = kTypeCount n + ((if 5 ∣ n then 1 else 0) + if 10 ∣ n then 1 else 0)

The substrate's six-property roundness score is the k-type count plus the two raw divisibility indicators [Cum15] sets aside as non-diagnostic.

Candidates, contexts, and the six constraints

inductive Cummins2015.QuantifierForm : Type

Quantifier form of a candidate numerical expression.

• bare : QuantifierForm
• exactly : QuantifierForm
• about : QuantifierForm
• moreThan : QuantifierForm
• atLeast : QuantifierForm

@[instance_reducible]

instance Cummins2015.instDecidableEqQuantifierForm : DecidableEq QuantifierForm

Equations

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

def Cummins2015.QuantifierForm.complexity : QuantifierForm → ℕ

Degrees of complexity for QSIMP: bare numerals are simplest; each overt modifier adds a degree; superlative bounds cost more than comparative ones, the experimentally supported asymmetry [Cum15] adopts to separate the two single-bound families.

Equations

• Cummins2015.QuantifierForm.bare.complexity = 0
• Cummins2015.QuantifierForm.exactly.complexity = 1
• Cummins2015.QuantifierForm.about.complexity = 1
• Cummins2015.QuantifierForm.moreThan.complexity = 1
• Cummins2015.QuantifierForm.atLeast.complexity = 2

structure Cummins2015.Candidate : Type

A candidate numerical expression: a quantifier form applied to a numeral.

• form : QuantifierForm
• numeral : ℕ

@[instance_reducible]

instance Cummins2015.instDecidableEqCandidate : DecidableEq Candidate

Equations

• Cummins2015.instDecidableEqCandidate = Cummins2015.instDecidableEqCandidate.decEq

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 ⋯

structure Cummins2015.Context : Type

Utterance context: the speaker's knowledge (a lower bound on the value under discussion, the shape of the book's worked examples), the contextually set granularity level, and the primed numeral and quantifier, if any.

• lowerBound : ℕ
• granularity : ℕ
• primedNumeral : Option ℕ
• primedForm : Option QuantifierForm

def Cummins2015.infoViolations (ctx : Context) : Constraints.Constraint Candidate

INFO ([Cum15]'s informativeness constraint): one violation per value the expression admits that the speaker's knowledge value ≥ ctx.lowerBound already excludes. Bounds admit the known-false values below the speaker's own bound; point forms admit only their numeral.

Equations

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

def Cummins2015.qsimpViolations : Constraints.Constraint Candidate

QSIMP: one violation per degree of quantifier complexity.

Equations

• Cummins2015.qsimpViolations c = c.form.complexity

def Cummins2015.nsal : Constraints.Constraint Candidate

NSAL over candidates: nsalViolations pulled back along the numeral.

Equations

• Cummins2015.nsal = Constraints.Constraint.comap Cummins2015.Candidate.numeral Cummins2015.nsalViolations

def Cummins2015.granularityLevel (n : ℕ) : ℕ

Decimal granularity level of a numeral: the finest base-10 scale on which it sits (trailing zeros, capped at the thousands level). The book's granularity is scale-relative; on the base-10 scales of the bare-number domain the level is the trailing-zero count.

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

def Cummins2015.granViolations (ctx : Context) : Constraints.Constraint Candidate

GRAN ([Cum15]'s granularity constraint): one violation per level of mismatch between the contextually set granularity and the level used.

Equations

• Cummins2015.granViolations ctx c = ctx.granularity.dist (Cummins2015.granularityLevel c.numeral)

def Cummins2015.npriViolations (ctx : Context) : Constraints.Constraint Candidate

NPRI ([Cum15]'s numeral priming constraint): a violation iff a numeral is primed in the preceding context and a different one is used. Unprimed contexts violate nothing.

Equations

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

def Cummins2015.qpriViolations (ctx : Context) : Constraints.Constraint Candidate

QPRI ([Cum15]'s quantifier priming constraint): a violation iff a quantifier is primed in the preceding context and a different one is used.

Equations

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

def Cummins2015.con (ctx : Context) : Constraints.CON Candidate 6

The six-constraint system, indexed in the book's enumeration order: 0 = INFO, 1 = QSIMP, 2 = NSAL, 3 = GRAN, 4 = NPRI, 5 = QPRI.

Equations

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

theorem Cummins2015.card_rankings : Fintype.card (OptimalityTheory.Ranking 6) = 720

The book's count of possible idiolects: six constraints admit 720 total rankings.

The worked tableaux

The book's toy system: INFO, NSAL, and NPRI adjudicate between rival more than n bounds for a speaker who knows value ≥ 103 (representative numerals; the shape follows the book's example, where the informative bound's numeral incurs the maximum four NSAL violations). more than 102 is maximally informative but non-salient; more than 100 is salient but under-informative. Unprimed, INFO-top speakers pick the former and NSAL-top speakers the latter; priming 102 leaves only NSAL-top speakers on the round bound. Each ranking selects a singleton — the book's deterministic-output point — and the factorial typology has exactly the two idiolect types.

def Cummins2015.mt (n : ℕ) : Candidate

The more than n candidate.

Equations

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

def Cummins2015.unprimed : Context

Unprimed context: the speaker knows value ≥ 103; hundreds granularity.

Equations

• Cummins2015.unprimed = { lowerBound := 103, granularity := 2 }

def Cummins2015.primed : Context

The same context with 102 primed in the preceding turn.

Equations

• Cummins2015.primed = { lowerBound := Cummins2015.unprimed.lowerBound, granularity := Cummins2015.unprimed.granularity, primedNumeral := some 102, primedForm := Cummins2015.unprimed.primedForm }

theorem Cummins2015.unprimed_optimal_of_info_top : (OptimalityTheory.Tableau.ofRanking [mt 100, mt 102] [infoViolations unprimed, nsal, npriViolations unprimed] ⋯).optimal = {mt 102}

theorem Cummins2015.unprimed_optimal_of_nsal_top : (OptimalityTheory.Tableau.ofRanking [mt 100, mt 102] [nsal, infoViolations unprimed, npriViolations unprimed] ⋯).optimal = {mt 100}

theorem Cummins2015.primed_optimal_of_nsal_top : (OptimalityTheory.Tableau.ofRanking [mt 100, mt 102] [nsal, npriViolations primed, infoViolations primed] ⋯).optimal = {mt 100}

theorem Cummins2015.primed_optimal_of_npri_over_nsal : (OptimalityTheory.Tableau.ofRanking [mt 100, mt 102] [npriViolations primed, nsal, infoViolations primed] ⋯).optimal = {mt 102}

theorem Cummins2015.toy_factorialTypologySize : OptimalityTheory.factorialTypologySize [mt 100, mt 102] [infoViolations unprimed, nsal, npriViolations unprimed] ⋯ = 2

Both candidates surface across the six rankings — the book's point that a deterministic OT system yields apparent variability via ranking variation.

Harmonic bounding

theorem Cummins2015.profile_le_of_pointwise_le {C : Type u_1} {n : ℕ} (con : Constraints.CON C n) (r : OptimalityTheory.Ranking n) {c d : C} (h : ∀ (i : Fin n), con i c ≤ con i d) : Constraints.buildViolationProfile (fun (p : Fin n) => con (r p)) c ≤ Constraints.buildViolationProfile (fun (p : Fin n) => con (r p)) d

Pointwise violation dominance survives every ranking ([Cum15]'s harmonic-bounding argument, one half): reordering coordinates preserves pointwise ≤, and pointwise ≤ entails lexicographic ≤.

theorem Cummins2015.not_mem_optimal_of_strictBounded {C : Type u_1} [DecidableEq C] {n : ℕ} {con : Constraints.CON C n} {r : OptimalityTheory.Ranking n} {cands : List C} {hne : cands ≠ []} {c d : C} (hc : c ∈ cands) (hle : ∀ (i : Fin n), con i c ≤ con i d) (hlt : ∃ (i : Fin n), con i c < con i d) : d ∉ (OptimalityTheory.Tableau.ofPerm con r cands hne).optimal

A strictly harmonically bounded candidate — one incurring at least a rival's violations everywhere and strictly more somewhere — is optimal under no ranking whenever its bounder competes ([Cum15]: "preferred under any constraint ranking").

theorem Cummins2015.moreThan90_never_optimal (r : OptimalityTheory.Ranking 6) : mt 90 ∉ (OptimalityTheory.Tableau.ofPerm (con unprimed) r [mt 90, mt 100, mt 102] ⋯).optimal

Instance in the full six-constraint system: more than 100 harmonically bounds more than 90 in the unprimed context (weakly better on all six constraints, strictly on INFO, NSAL, and GRAN), so more than 90 wins under none of the 720 rankings.

Round numerals and approximate construal

theorem Cummins2015.inferPrecisionMode_eq_approximate_of_nsalViolations_eq_zero {n : ℕ} (h : nsalViolations n = 0) : Semantics.Numerals.Precision.inferPrecisionMode n = Semantics.Numerals.Precision.PrecisionMode.approximate

Fully salient numerals admit the approximate construal: zero NSAL violations force 10-ness, hence divisibility by 10, which the precision substrate maps to .approximate — the association between round numbers and approximate readings that [Cum15] inherits from the imprecision literature.