Little, Moroney & Royer (2022)

[LMR22]

Classifiers can be for numerals or nouns: Two strategies for numeral modification. Glossa 7(1). 1–35.

Numeral classifiers form a heterogeneous class. Ch'ol (CLF-for-NUM, the classifier is a measure function required by the numeral) and Shan (CLF-for-N, the classifier atomizes the noun denotation) take different compositional paths to the same denotation for "two dogs". This file exercises that claim against linglib's type-driven composition machinery: two Tree String derivations, distinct lexicons, identical extension at the root.

Main declarations

• cholStrategy, shanStrategy — LMR's per-language assignments
• Predictions — LMR's four-diagnostic battery (Table 8)
• cholTree, cholLex, shanTree, shanLex — derivations (51), (52) driven through Semantics.Composition.Tree.interp
• cholTree_interprets, shanTree_interprets — rfl witnesses that Heim-Kratzer FA composes the lexicons through the trees
• section5_extensionally_equal — LMR §5 main result: the two trees evaluate to extensionally-equal predicates of type ⟨e,t⟩

Implementation notes

The semantic carrier is Finset Dog (atomic powerset model with ∅ excluded by .Nonempty). The Heim-Kratzer Ty system (e, t, fn, intens) lacks a number type, so LMR's measure function μ_# : ⟨e,n⟩ is folded into the numeral's denotation as a Finset.card-via-Prop constraint rather than realized as a stand-alone constituent of type ⟨e,n⟩. The constituency contrast — [[Num Clf] N] vs [Num [Clf N]] — is faithful; only the type of the measure is encoded indirectly.

@[reducible, inline]

abbrev LittleMoroneyRoyer2022.chol : NounCategorization.System

Equations

• LittleMoroneyRoyer2022.chol = Chol.classifierSystem

@[reducible, inline]

abbrev LittleMoroneyRoyer2022.shan : NounCategorization.System

Equations

• LittleMoroneyRoyer2022.shan = Shan.classifierSystem

Predictions (Table 8)

structure LittleMoroneyRoyer2022.Predictions : Type

• numeralIdiosyncrasies : Prop
• nounIdiosyncrasies : Prop
• clfBeyondNumerals : Prop
• clfInCounting : Prop

def LittleMoroneyRoyer2022.clfForNumPredictions : Predictions

Equations

• LittleMoroneyRoyer2022.clfForNumPredictions = { numeralIdiosyncrasies := True, nounIdiosyncrasies := False, clfBeyondNumerals := False, clfInCounting := True }

def LittleMoroneyRoyer2022.clfForNounPredictions : Predictions

Equations

• LittleMoroneyRoyer2022.clfForNounPredictions = { numeralIdiosyncrasies := False, nounIdiosyncrasies := True, clfBeyondNumerals := True, clfInCounting := False }

def LittleMoroneyRoyer2022.cholStrategy : NounCategorization.ClassifierStrategy

Equations

• LittleMoroneyRoyer2022.cholStrategy = NounCategorization.ClassifierStrategy.forNumeral

def LittleMoroneyRoyer2022.shanStrategy : NounCategorization.ClassifierStrategy

Equations

• LittleMoroneyRoyer2022.shanStrategy = NounCategorization.ClassifierStrategy.forNoun

theorem LittleMoroneyRoyer2022.profiles_distinct : clfForNumPredictions ≠ clfForNounPredictions

Plural co-occurrence (§3.4)

[LMR22] §3.4 refines [Bor05]'s complementarity intuition: CLF and PL share a functional projection in CLF-for-N languages, separate projections in CLF-for-NUM languages.

theorem LittleMoroneyRoyer2022.complementarity_refined_by_strategy : cholStrategy = NounCategorization.ClassifierStrategy.forNumeral ∧ chol.PluralClfCooccur ∧ shanStrategy = NounCategorization.ClassifierStrategy.forNoun ∧ ¬shan.PluralClfCooccur

Compositional derivation (§2.3, §5)

Worked example on three dogs. The two trees compose under Semantics.Composition.Tree.interp against per-language lexicons; the §5 main result is established as extensional equivalence of the root denotations.

inductive LittleMoroneyRoyer2022.Dog : Type

• a : Dog
• b : Dog
• c : Dog

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instDecidableEqDog : DecidableEq Dog

Equations

• LittleMoroneyRoyer2022.instDecidableEqDog x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instReprDog : Repr Dog

Equations

• LittleMoroneyRoyer2022.instReprDog = { reprPrec := LittleMoroneyRoyer2022.instReprDog.repr }

def LittleMoroneyRoyer2022.instReprDog.repr : Dog → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance LittleMoroneyRoyer2022.instFintypeDog : Fintype Dog

Equations

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

LMR's semantic carrier is Finset Dog (Link-style sums of dog-atoms with ∅ excluded downstream by .Nonempty), with Unit indices (extensional).

def LittleMoroneyRoyer2022.emptyAssign : Core.Assignment (Finset Dog)

Empty variable assignment; the §2.3 trees contain no traces.

Equations

• LittleMoroneyRoyer2022.emptyAssign x✝ = ∅

def LittleMoroneyRoyer2022.cholLex : Semantics.Montague.Lexicon (Finset Dog) Unit

Ch'ol lexicon. cha' is the measure-loaded numeral λκ λP λx. P x ∧ κ x ∧ |x| = 2; kojty contributes a (semantically vacuous) sortal restriction; ts'i' is the dog predicate. The ⟨e,n⟩ measure type is folded into cha'.

Equations

• One or more equations did not get rendered due to their size.
• LittleMoroneyRoyer2022.cholLex "kojty" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := fun (x : Finset LittleMoroneyRoyer2022.Dog) => True }
• LittleMoroneyRoyer2022.cholLex "ts'i'" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := fun (x : Finset LittleMoroneyRoyer2022.Dog) => x.Nonempty }
• LittleMoroneyRoyer2022.cholLex x✝ = none

def LittleMoroneyRoyer2022.shanLex : Semantics.Montague.Lexicon (Finset Dog) Unit

Shan lexicon. tǒ atomizes the noun predicate (λP λx. P x ∧ |x| = 1); sǒŋ selects 2-element joins of distinct atoms from an atomized predicate; mǎa is the dog predicate.

Equations

• One or more equations did not get rendered due to their size.
• LittleMoroneyRoyer2022.shanLex "mǎa" = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, denot := fun (x : Finset LittleMoroneyRoyer2022.Dog) => x.Nonempty }
• LittleMoroneyRoyer2022.shanLex x✝ = none

def LittleMoroneyRoyer2022.cholTree : Syntax.Tree Unit String

Ch'ol derivation (51): [[cha' kojty] ts'i']. Num+CLF form a constituent that then applies to the noun.

Equations

• LittleMoroneyRoyer2022.cholTree = ((Syntax.Tree.leaf "cha'").bin (Syntax.Tree.leaf "kojty")).bin (Syntax.Tree.leaf "ts'i'")

def LittleMoroneyRoyer2022.shanTree : Syntax.Tree Unit String

Shan derivation (52): [sǒŋ [tǒ mǎa]]. CLF+N form a constituent that the numeral then selects from.

Equations

• LittleMoroneyRoyer2022.shanTree = (Syntax.Tree.leaf "sǒŋ").bin ((Syntax.Tree.leaf "tǒ").bin (Syntax.Tree.leaf "mǎa"))

def LittleMoroneyRoyer2022.cholDenot : Finset Dog → Prop

Ch'ol composition: cha'(kojty)(ts'i') = λx. ts'i'(x) ∧ kojty(x) ∧ |x| = 2 after two rounds of FA.

Equations

• LittleMoroneyRoyer2022.cholDenot x = (x.Nonempty ∧ True ∧ x.card = 2)

def LittleMoroneyRoyer2022.shanDenot : Finset Dog → Prop

Shan composition: sǒŋ(tǒ(mǎa)) = λx. ∃ d₁ d₂, d₁ ≠ d₂ ∧ (tǒ(mǎa)) {d₁} ∧ (tǒ(mǎa)) {d₂} ∧ x = {d₁,d₂} after two rounds of FA.

Equations

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

theorem LittleMoroneyRoyer2022.cholTree_interprets : Semantics.Composition.Tree.interp (Finset Dog) Unit cholLex emptyAssign cholTree = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, val := cholDenot }

The Ch'ol tree interprets to cholDenot via two FA steps under the Ch'ol lexicon.

theorem LittleMoroneyRoyer2022.shanTree_interprets : Semantics.Composition.Tree.interp (Finset Dog) Unit shanLex emptyAssign shanTree = some { ty := Intensional.Ty.e ⇒ Intensional.Ty.t, val := shanDenot }

The Shan tree interprets to shanDenot via two FA steps under the Shan lexicon.

theorem LittleMoroneyRoyer2022.section5_extensionally_equal (x : Finset Dog) : cholDenot x ↔ shanDenot x

LMR §5 main result: despite different constituency and different per-word lexical entries, the two derivations yield extensionally equivalent root denotations on the count-noun case. The proof discharges the trivial conjuncts and reduces to Finset.card_eq_two.

Cross-paper consistency with Chierchia 1998

theorem LittleMoroneyRoyer2022.shan_agrees_with_chierchia : shanStrategy = NMP.mandarinStrategy ∧ shanStrategy = NMP.japaneseStrategy

Shan agrees with [Chi98]'s NMP prediction for Mandarin/Japanese — all three are CLF-for-N.

theorem LittleMoroneyRoyer2022.chol_differs_from_chierchia : cholStrategy ≠ NMP.mandarinStrategy

Ch'ol is CLF-for-NUM, not the CLF-for-N predicted for Mandarin/Japanese under NMP.