Noun categorization devices

[Aik00] [Dix82] [Dow96] [All77] [Cor91]

Theory-neutral cross-linguistic typology of noun-categorization devices, following [Aik00] Classifiers: A Typology of Noun Categorization Devices: the device-type continuum (ClassifierType, with nounClass = gender at its agreement pole), the semantic parameters classifiers employ, the per-classifier lexical schema, and the per-language paradigm record. Graduated from the dissolved Typology/ drawer as a sibling of Features/Gender.

Main definitions

• ClassifierType — [Aik00]'s noun-categorization device types.
• SemanticParameter, ShapeDimension — the semantic axes ([All77], [Dow96]).
• CategorizationScope, AssignmentPrinciple, SurfaceRealization, GrammaticalCategory.
• ClassifierEntry — per-classifier lexical schema.
• ClassifierStrategy — competing composition frameworks (theory-laden; consumed by Semantics/Classifier, where the cross-paper disagreement is proved as theorems).
• System — Aikhenvald's per-language paradigm record (Bool property fields + Prop API).

Implementation notes

The nounClass cell collapses what [Cor91] separates (target/controller gender, gender vs. classifier); the per-language gender structure lives in Features/Gender, and a noun-class System's inventorySize/hasAgreement should derive from a Gender.System rather than being stipulated (follow-on).

inductive NounCategorization.ClassifierType : Type

The 9 focal classifier types on the noun-categorization continuum.

[Aik00] establishes these as "focal points" distinguished by morphosyntactic locus, scope, and grammatical function. Real systems are gradient — a language's system may sit between types.

UNVERIFIED: The 9-type taxonomy is Aikhenvald's specific carve-up; other typologists (Allan 1977, Craig 1986, Grinevald 2000, Senft 2000) differ. The nounClass cell here is also more fine-grained per Corbett 1991 — see file docstring "Out of scope".

• nounClass : ClassifierType

  Noun class / gender: closed agreement system, realized outside the noun on modifiers (head-modifier NP) or predicate (pred-arg agreement). Small inventory (2–20). Examples: Bantu, Indo-European gender.

• nounClassifier : ClassifierType

  Noun classifier: independent of other NP elements, characterizes the noun itself. Free forms or affixes on the noun.

• numeralClassifier : ClassifierType

  Numeral classifier: appears in numeral/quantifier NPs, required for enumeration. Free forms or affixes on the numeral.

• relationalClassifier : ClassifierType

  Relational classifier: in possessive NPs, characterizes the possessive relation (how the noun can be possessed/handled).

• possessedClassifier : ClassifierType

  Possessed classifier: in possessive NPs, characterizes the possessed noun in terms of its inherent properties.

• possessorClassifier : ClassifierType

  Possessor classifier: in possessive NPs, characterizes the possessor. Very rare.

• verbalClassifier : ClassifierType

  Verbal classifier: marks agreement on the verb with an S or O argument. Incorporated classifiers, affixes, or suppletive verb stems.

• locativeClassifier : ClassifierType

  Locative classifier: in adpositional NPs, marks agreement with the head noun in locative expressions.

• deicticClassifier : ClassifierType

  Deictic classifier: appears on deictics, articles, demonstratives. Marks spatial location and/or determination.

@[implicit_reducible]

instance NounCategorization.instDecidableEqClassifierType : DecidableEq ClassifierType

Equations

• NounCategorization.instDecidableEqClassifierType x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprClassifierType : Repr ClassifierType

Equations

• NounCategorization.instReprClassifierType = { reprPrec := NounCategorization.instReprClassifierType.repr }

def NounCategorization.instReprClassifierType.repr : ClassifierType → Nat → Std.Format

Equations

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

inductive NounCategorization.SemanticParameter : Type

Universal semantic parameters employed in noun categorization.

[Aik00] identifies three large classes: animacy, physical properties, and function. These parameters are found across ALL types of noun categorization device, though different types show different preferences.

• animacy : SemanticParameter
• humanness : SemanticParameter
• sex : SemanticParameter
• shape : SemanticParameter
• size : SemanticParameter
• consistency : SemanticParameter
• material : SemanticParameter
• boundedness : SemanticParameter
• function : SemanticParameter
• arrangement : SemanticParameter
• quanta : SemanticParameter
• socialStatus : SemanticParameter
• register : SemanticParameter
• colour : SemanticParameter

@[implicit_reducible]

instance NounCategorization.instDecidableEqSemanticParameter : DecidableEq SemanticParameter

Equations

• NounCategorization.instDecidableEqSemanticParameter x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprSemanticParameter : Repr SemanticParameter

Equations

• NounCategorization.instReprSemanticParameter = { reprPrec := NounCategorization.instReprSemanticParameter.repr }

def NounCategorization.instReprSemanticParameter.repr : SemanticParameter → Nat → Std.Format

Equations

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

inductive NounCategorization.ShapeDimension : Type

Dimensionality sub-classification for shape-based classifiers.

[Dow96] and [All77] show that shape-based classifiers decompose along a dimensionality axis:

• 1D: long, slender, elongated (e.g., Japanese 本 hon, Mandarin 条 tiáo)
• 2D: flat, thin, planar (e.g., Japanese 枚 mai, Mandarin 张 zhāng)
• 3D: round, compact, globular (e.g., Japanese 個 ko)

• oneD : ShapeDimension
• twoD : ShapeDimension
• threeD : ShapeDimension

@[implicit_reducible]

instance NounCategorization.instDecidableEqShapeDimension : DecidableEq ShapeDimension

Equations

• NounCategorization.instDecidableEqShapeDimension x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprShapeDimension : Repr ShapeDimension

Equations

• NounCategorization.instReprShapeDimension = { reprPrec := NounCategorization.instReprShapeDimension.repr }

def NounCategorization.instReprShapeDimension.repr : ShapeDimension → Nat → Std.Format

Equations

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

inductive NounCategorization.CategorizationScope : Type

Morphosyntactic scope of a classifier type.

• headModifierNP : CategorizationScope
• predicateArgument : CategorizationScope
• noun : CategorizationScope
• numeralNP : CategorizationScope
• possessiveNP : CategorizationScope
• clause : CategorizationScope
• adpositionalNP : CategorizationScope
• attributiveNP : CategorizationScope

@[implicit_reducible]

instance NounCategorization.instDecidableEqCategorizationScope : DecidableEq CategorizationScope

Equations

• NounCategorization.instDecidableEqCategorizationScope x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NounCategorization.instReprCategorizationScope.repr : CategorizationScope → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance NounCategorization.instReprCategorizationScope : Repr CategorizationScope

Equations

• NounCategorization.instReprCategorizationScope = { reprPrec := NounCategorization.instReprCategorizationScope.repr }

inductive NounCategorization.AssignmentPrinciple : Type

Principles governing noun-to-class/classifier assignment.

• semantic : AssignmentPrinciple

  Purely semantic: class determined by referent meaning

• morphological : AssignmentPrinciple

  Morphological: class determined by derivational affix, declension, etc.

• phonological : AssignmentPrinciple

  Phonological: class determined by initial segment, final vowel, etc.

• mixed : AssignmentPrinciple

  Mixed: semantic core + morphological/phonological overlay

@[implicit_reducible]

instance NounCategorization.instDecidableEqAssignmentPrinciple : DecidableEq AssignmentPrinciple

Equations

• NounCategorization.instDecidableEqAssignmentPrinciple x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprAssignmentPrinciple : Repr AssignmentPrinciple

Equations

• NounCategorization.instReprAssignmentPrinciple = { reprPrec := NounCategorization.instReprAssignmentPrinciple.repr }

def NounCategorization.instReprAssignmentPrinciple.repr : AssignmentPrinciple → Nat → Std.Format

Equations

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

inductive NounCategorization.SurfaceRealization : Type

Surface realization of a classifier morpheme.

• prefix : SurfaceRealization
• suffix : SurfaceRealization
• clitic : SurfaceRealization
• freeForm : SurfaceRealization
• suppletion : SurfaceRealization
• stress : SurfaceRealization
• reduplication : SurfaceRealization
• nounIncorporation : SurfaceRealization
• repeater : SurfaceRealization

@[implicit_reducible]

instance NounCategorization.instDecidableEqSurfaceRealization : DecidableEq SurfaceRealization

Equations

• NounCategorization.instDecidableEqSurfaceRealization x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprSurfaceRealization : Repr SurfaceRealization

Equations

• NounCategorization.instReprSurfaceRealization = { reprPrec := NounCategorization.instReprSurfaceRealization.repr }

def NounCategorization.instReprSurfaceRealization.repr : SurfaceRealization → Nat → Std.Format

Equations

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

structure NounCategorization.ClassifierEntry : Type

A classifier lexical entry with semantic typing.

Each classifier carries its form, a gloss, and the semantic parameters that motivate its selection — making it possible to verify Aikhenvald's claims about which parameters different classifier types encode.

• form : String

  Surface form (e.g. "只", "匹", "本")

• gloss : String

  Gloss (e.g. "small.animal", "flat.bound.object")

• semantics : List SemanticParameter

  Semantic parameters motivating selection of this classifier

• isDefault : Bool

  Is this the "general" or "default" classifier? (个 in Mandarin, つ in Japanese)

• isMensural : Bool

  Sortal (inherent properties) vs. mensural (configuration/measure)

• shapeDimension : Option ShapeDimension

  Shape dimensionality sub-classification ([Dow96]). Only meaningful when semantics includes .shape.

@[implicit_reducible]

instance NounCategorization.instReprClassifierEntry : Repr ClassifierEntry

Equations

• NounCategorization.instReprClassifierEntry = { reprPrec := NounCategorization.instReprClassifierEntry.repr }

def NounCategorization.instReprClassifierEntry.repr : ClassifierEntry → Nat → Std.Format

Equations

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

def NounCategorization.instBEqClassifierEntry.beq : ClassifierEntry → ClassifierEntry → Bool

Equations

• One or more equations did not get rendered due to their size.
• NounCategorization.instBEqClassifierEntry.beq x✝¹ x✝ = false

@[implicit_reducible]

instance NounCategorization.instBEqClassifierEntry : BEq ClassifierEntry

Equations

• NounCategorization.instBEqClassifierEntry = { beq := NounCategorization.instBEqClassifierEntry.beq }

def NounCategorization.ClassifierEntry.encodes (c : ClassifierEntry) (p : SemanticParameter) : Bool

Whether this classifier encodes a given semantic parameter.

Equations

• c.encodes p = c.semantics.any fun (x : NounCategorization.SemanticParameter) => x == p

def NounCategorization.collectSemantics (cls : List ClassifierEntry) : List SemanticParameter

Collect all distinct semantic parameters attested across a classifier inventory. Used to derive preferredSemantics from fragment data rather than hand-listing.

Equations

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

inductive NounCategorization.ClassifierStrategy : Type

The semantic strategy a theoretical framework attributes to classifier constructions. Three competing positions are represented:

• forNumeral (CLF-for-NUM): [krifka-1995], [BC14], [LMR22]. The classifier is a measure function required by the numeral. The numeral takes the classifier as its first argument: ⟦TWO⟧ = λm⟨e,n⟩λPλx.[P(x) ∧ m(x) = 2]. Predicts: numeral idiosyncrasies in CLF requirement, CLF obligatory even without a noun (counting contexts), CLF + plural marking can co-occur.
• forNoun (CLF-for-N): [Chi98], [jenks-2011], [nomoto-2013], [LMR22]. The classifier atomizes the noun denotation so the numeral can count. ⟦CLF⟧ = λPλx.[P(x) ∧ ¬∃y[P(y) ∧ y < x]]. Predicts: noun idiosyncrasies in CLF requirement, CLF appears beyond numerals (with quantifiers, demonstratives, relative clauses), CLF + plural marking in complementary distribution.
• sudoBlocking: [Sud16]. Classifier semantics live with numerals, not nouns. Numerals are universally type-n singular terms; a phonologically silent ∪-operator type-shifts them to predicates in languages without classifiers, but is blocked (per [Chi98]'s Blocking Principle) in languages whose lexicon contains overt classifiers. Predicts: no numeral or noun idiosyncrasies, CLF appears with numerals not beyond them, CLF appears in counting contexts (via the ∩-operator).

Strategy assignments to specific languages live in study files (Studies/{NMP,LittleMoroneyRoyer2022,Sudo2016}.lean), not in this file or in System. Each paper owns its own per-language commitments; cross-paper agreement and disagreement are first-class theorems in the study files.

• forNumeral : ClassifierStrategy
• forNoun : ClassifierStrategy
• sudoBlocking : ClassifierStrategy

@[implicit_reducible]

instance NounCategorization.instDecidableEqClassifierStrategy : DecidableEq ClassifierStrategy

Equations

• NounCategorization.instDecidableEqClassifierStrategy x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance NounCategorization.instReprClassifierStrategy : Repr ClassifierStrategy

Equations

• NounCategorization.instReprClassifierStrategy = { reprPrec := NounCategorization.instReprClassifierStrategy.repr }

def NounCategorization.instReprClassifierStrategy.repr : ClassifierStrategy → Nat → Std.Format

Equations

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

structure NounCategorization.System : Type

A noun categorization system in a language.

Captures [Aik00]'s 7 definitional properties (A–G): (A) morphosyntactic locus → scopes (B) scope/domain → classifierType + scopes (C) assignment principles → assignment (D) surface realization → realizations (E) agreement → hasAgreement (F) markedness → hasUnmarkedDefault (G) grammaticalization → isObligatory

UNVERIFIED: A–G enumeration cited from memory.

• family : String

  Language family (e.g., "Indo-European", "Sino-Tibetan", "Bantu").

• classifierType : ClassifierType

  Aikhenvald classifier type.

• scopes : List CategorizationScope

  Morphosyntactic scopes this system operates in (A, B).

• assignment : AssignmentPrinciple

  How nouns are assigned to classes/classifiers (C).

• realizations : List SurfaceRealization

  Morphological realization types used (D).

• hasAgreement : Bool

  Does the system involve agreement? (E) — definitional for noun classes. Stored as Bool so the struct stays decidable as a whole; the user-facing predicate is HasAgreement : Prop.

• inventorySize : Nat

  Inventory size (number of classes or classifiers).

• isObligatory : Bool

  Is realization obligatory or optional? (G). User-facing predicate: IsObligatory : Prop.

• hasUnmarkedDefault : Bool

  Is there a formally/functionally unmarked default? (F). User-facing predicate: HasUnmarkedDefault : Prop.

• preferredSemantics : List SemanticParameter

  Preferred semantic parameters (Aikhenvald §11.2).

• hasObligatoryNumber : Bool

  Does the language have obligatory grammatical number marking? User-facing predicate: HasObligatoryNumber : Prop.

• pluralClfCooccur : Bool

  Can classifiers and plural marking co-occur? Predicted by CLF-for-NUM ([LMR22]: CLF and PL are in different projections) but not by CLF-for-N (same projection, complementary distribution per [Bor05]). User-facing predicate: PluralClfCooccur : Prop.

• source : String

  Citation backing the hand-coded values.

@[implicit_reducible]

instance NounCategorization.instReprSystem : Repr System

Equations

• NounCategorization.instReprSystem = { reprPrec := NounCategorization.instReprSystem.repr }

def NounCategorization.instReprSystem.repr : System → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance NounCategorization.instDecidableEqSystem : DecidableEq System

Equations

• NounCategorization.instDecidableEqSystem = NounCategorization.instDecidableEqSystem.decEq

def NounCategorization.instDecidableEqSystem.decEq (x✝ x✝¹ : System) : Decidable (x✝ = x✝¹)

Equations

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

Prop API for the boolean property fields

The struct's hasAgreement/isObligatory/hasUnmarkedDefault/ hasObligatoryNumber/pluralClfCooccur fields are stored as Bool so the struct itself stays decidably equal. The user-facing predicates are the Prop versions defined here, each with a Decidable instance via the underlying Bool. Theorem statements should prefer the Prop form (s.HasAgreement rather than s.hasAgreement = true); decide works for either since the Bool projection reduces structurally for concrete fragment values.

@[reducible, inline]

abbrev NounCategorization.System.HasAgreement (s : System) : Prop

The system involves agreement (E).

Equations

• s.HasAgreement = (s.hasAgreement = true)

@[reducible, inline]

abbrev NounCategorization.System.IsObligatory (s : System) : Prop

Realization is obligatory (G).

Equations

• s.IsObligatory = (s.isObligatory = true)

@[reducible, inline]

abbrev NounCategorization.System.HasUnmarkedDefault (s : System) : Prop

The system has a formally/functionally unmarked default (F).

Equations

• s.HasUnmarkedDefault = (s.hasUnmarkedDefault = true)

@[reducible, inline]

abbrev NounCategorization.System.HasObligatoryNumber (s : System) : Prop

The language has obligatory grammatical number marking.

Equations

• s.HasObligatoryNumber = (s.hasObligatoryNumber = true)

@[reducible, inline]

abbrev NounCategorization.System.PluralClfCooccur (s : System) : Prop

Classifiers and plural marking can co-occur.

Equations

• s.PluralClfCooccur = (s.pluralClfCooccur = true)

def NounCategorization.System.isNounClassType (t : ClassifierType) : Bool

[Dix82]'s noun-class vs. classifier divide. Noun classes: small, closed, grammaticalized, agreement. Classifiers: large, open, lexical, no agreement.

Equations

• NounCategorization.System.isNounClassType t = (t == NounCategorization.ClassifierType.nounClass)

def NounCategorization.System.isClassifierType (t : ClassifierType) : Bool

All non-noun-class types are "classifier" types in the broad sense.

Equations

• NounCategorization.System.isClassifierType t = !NounCategorization.System.isNounClassType t

inductive NounCategorization.GrammaticalCategory : Type

Grammatical categories that interact with classifier types ([Aik00]).

• definiteness : GrammaticalCategory
• number : GrammaticalCategory
• case_ : GrammaticalCategory
• tenseAspect : GrammaticalCategory
• possession : GrammaticalCategory

@[implicit_reducible]

instance NounCategorization.instDecidableEqGrammaticalCategory : DecidableEq GrammaticalCategory

Equations

• NounCategorization.instDecidableEqGrammaticalCategory x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def NounCategorization.instReprGrammaticalCategory.repr : GrammaticalCategory → Nat → Std.Format

Equations

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

@[implicit_reducible]

instance NounCategorization.instReprGrammaticalCategory : Repr GrammaticalCategory

Equations

• NounCategorization.instReprGrammaticalCategory = { reprPrec := NounCategorization.instReprGrammaticalCategory.repr }

def NounCategorization.interacts : ClassifierType → GrammaticalCategory → Bool

Whether a classifier type typically interacts with a grammatical category ([Aik00]).

Equations

• NounCategorization.interacts NounCategorization.ClassifierType.nounClass NounCategorization.GrammaticalCategory.definiteness = true
• NounCategorization.interacts NounCategorization.ClassifierType.nounClass NounCategorization.GrammaticalCategory.number = true
• NounCategorization.interacts NounCategorization.ClassifierType.nounClass NounCategorization.GrammaticalCategory.case_ = true
• NounCategorization.interacts NounCategorization.ClassifierType.nounClass NounCategorization.GrammaticalCategory.tenseAspect = true
• NounCategorization.interacts NounCategorization.ClassifierType.nounClass NounCategorization.GrammaticalCategory.possession = true
• NounCategorization.interacts NounCategorization.ClassifierType.numeralClassifier NounCategorization.GrammaticalCategory.definiteness = true
• NounCategorization.interacts NounCategorization.ClassifierType.numeralClassifier NounCategorization.GrammaticalCategory.number = true
• NounCategorization.interacts NounCategorization.ClassifierType.numeralClassifier NounCategorization.GrammaticalCategory.possession = false
• NounCategorization.interacts NounCategorization.ClassifierType.numeralClassifier NounCategorization.GrammaticalCategory.case_ = false
• NounCategorization.interacts NounCategorization.ClassifierType.numeralClassifier NounCategorization.GrammaticalCategory.tenseAspect = false
• NounCategorization.interacts NounCategorization.ClassifierType.verbalClassifier NounCategorization.GrammaticalCategory.tenseAspect = true
• NounCategorization.interacts NounCategorization.ClassifierType.verbalClassifier NounCategorization.GrammaticalCategory.number = true
• NounCategorization.interacts NounCategorization.ClassifierType.relationalClassifier NounCategorization.GrammaticalCategory.possession = true
• NounCategorization.interacts NounCategorization.ClassifierType.possessedClassifier NounCategorization.GrammaticalCategory.possession = true
• NounCategorization.interacts x✝¹ x✝ = false