Documentation

Linglib.Theories.Semantics.Classifier.Basic

Classifier Semantics #

@cite{chierchia-1998} @cite{little-moroney-royer-2022} @cite{moroney-2021}

Unified compositional semantics for classifier constructions, connecting the typological vocabulary in Typology to the mereological infrastructure in Core.Mereology and the materialization homomorphism in Theories.Semantics.Plurality.Link1983.

Two Semantic Strategies #

Numeral classifiers form a heterogeneous class (@cite{little-moroney-royer-2022}). Two families of theories are BOTH correct, for different languages:

Both strategies convert CUM predicates to QUA predicates — this is the universal semantic function of classifiers regardless of strategy.

Group Classifiers #

Group classifiers like Shan phŭŋ 'group' use Link's materialization homomorphism: ⟦phŭŋ⟧ = λPλx.∃y[P(y) ∧ μ(x) = 1 ∧ h(y) = h(x)]. The group is a single entity (μ = 1) whose material constitution matches that of some P-entity.

Architecture #

This module composes existing pieces:

source
@[reducible, inline]
abbrev Semantics.Classifier.clfForNoun {α : Type u_1} [PartialOrder α] (P : α → Prop) :
α → Prop

CLF-for-N denotation: the classifier atomizes the noun denotation. ⟦CLF⟧ = λPλx.[P(x) ∧ ¬∃y[P(y) ∧ y < x]]

This IS Mereology.atomize. The wrapper aliases it under the classifier namespace for discoverability and adds the @cite{little-moroney-royer-2022} citation.

Equations
Instances For
    source
    theorem Semantics.Classifier.clfForNoun_qua {α : Type u_1} [PartialOrder α] {P : α → Prop} :
    Mereology.QUA (clfForNoun P)

    CLF-for-N produces quantized predicates: the atomized noun denotation is QUA, enabling counting by the numeral. This IS Mereology.atomize_qua.

    source
    theorem Semantics.Classifier.clfForNoun_sub {α : Type u_1} [PartialOrder α] {P : α → Prop} {x : α} (h : clfForNoun P x) :
    P x

    CLF-for-N restricts: clfForNoun P ⊆ P.

    source
    @[reducible, inline]
    abbrev Semantics.Classifier.clfForNum {α : Type u_1} (P : α → Prop) (μ : α → ℚ) (n : ℚ) :
    α → Prop

    CLF-for-NUM denotation: the classifier is a measure function, and the numeral selects entities with the right measure value. ⟦TWO-CLF⟧ = λPλx.[P(x) ∧ μ(x) = 2]

    This IS Mereology.QMOD instantiated with a measure function μ and a target value n.

    Equations
    Instances For
      source
      theorem Semantics.Classifier.clfForNum_qua {α : Type u_1} [SemilatticeSup α] {P : α → Prop} {μ : α → ℚ} [hμ : Mereology.ExtMeasure α μ] (n : ℚ) :
      Mereology.QUA fun (x : α) => Mereology.QMOD P μ n x

      CLF-for-NUM produces quantized predicates when μ is an extensive measure: no proper part of an n-measure entity also has measure n. Generalizes over any base predicate P.

      source
      def Semantics.Classifier.groupClf {E : Type u_1} {D : Type u_2} [SemilatticeSup E] [SemilatticeSup D] (mat : Plurality.Link1983.Materialization E D) (P : E → Prop) (x : E) :
      Prop

      Group classifier denotation using Link's materialization homomorphism.

      ⟦phŭŋ_CLF⟧ = λPλx.∃y[P(y) ∧ Atom(x) ∧ h(y) = h(x)]

      The group classifier takes a predicate P and returns a predicate true of atomic entities x whose material constitution (h(x)) matches that of some P-entity y. This is how "a group of dogs" can denote a single atomic group-entity made of the same "stuff" as the dogs.

      @cite{moroney-2021} §3.3.2: ⟦phŭŋ_CLF⟧ = λP.λx.∃y[P(y) ∧ μ_GROUP.A(x) = 1 ∧ h(y) = h(x)].

      We use Atom x instead of μ(x) = 1 since atomicity is the mereological content of "counting as one group."

      Equations
      Instances For
        source
        theorem Semantics.Classifier.groupClf_qua {E : Type u_1} {D : Type u_2} [SemilatticeSup E] [SemilatticeSup D] (mat : Plurality.Link1983.Materialization E D) {P : E → Prop} :
        Mereology.QUA (groupClf mat P)

        Group classifier output is quantized: no proper part of a group is itself a group (since groups are atoms).

        source
        def Semantics.Classifier.classifierDenot {α : Type u_1} [PartialOrder α] (s : Typology.ClassifierStrategy) (P : α → Prop) (μ : α → ℚ) (n : ℚ) :
        α → Prop

        Dispatch from ClassifierStrategy to a noun-side predicate transformer.

        • .forNoun → clfForNoun P (Chierchia/LMR: classifier atomizes the noun)
        • .forNumeral → clfForNum P μ n (Krifka/Bale-Coon/LMR: measure-modify the numeral)
        • .sudoBlocking → clfForNoun P (Sudo: at the noun-side composition, the sortal-presupposition body of the classifier individuates atoms; the dispatch agrees with .forNoun here because we're projecting a numeral-side analysis onto a noun-side abstraction. The disagreement with Chierchia is not in noun-side individuation; it's in where the obligation to use a classifier comes from. See Phenomena/Classifiers/Studies/Sudo2016.lean.)
        Equations
        Instances For
          source
          theorem Semantics.Classifier.classifier_quantizes_forNoun {α : Type u_1} [SemilatticeSup α] {P : α → Prop} (_hCum : Mereology.CUM P) :
          Mereology.QUA (clfForNoun P)

          Both classifier strategies produce QUA predicates.

          • CLF-for-N: atomize_qua
          • CLF-for-NUM: extMeasure_qua (when μ is extensive)
          • Group CLF: groupClf_qua

          The common thread: classifiers convert cumulative (uncountable) predicates into quantized (countable) predicates, enabling numeral modification.

          source
          theorem Semantics.Classifier.clfForNoun_mem {α : Type u_1} [PartialOrder α] {P : α → Prop} {x : α} (hAtom : Mereology.Atom x) (hP : P x) :
          clfForNoun P x

          Atomization is a restriction: every atom of P is in P.

          source
          theorem Semantics.Classifier.clfForNoun_nonempty {α : Type u_1} [PartialOrder α] {P : α → Prop} {a : α} (hP : P a) (hAtom : Mereology.Atom a) :
          ∃ (x : α), clfForNoun P x

          If P has atoms, then CLF-for-N is non-empty. This is the content of the "sortal classifier" requirement: the classifier can only apply to nouns whose denotation includes atoms. Mass nouns (divisive predicates with no atoms) require a mensural classifier instead.