Documentation

Linglib.Fragments.Japanese.Classifier

Japanese Numeral Classifier Inventory #

@cite{aikhenvald-2000} @cite{downing-1996} @cite{sudo-2016}

The closed inventory of Japanese numeral classifiers (josūshi 助数詞) as a finite inductive type. Properties (form, gloss, encoded semantic parameters, dimensionality, mensural-vs-sortal, default flag) are projection functions or Decidable predicates over the type, not fields on a struct.

Architectural pilot #

This file is the pilot for an enum-as-source-of-truth fragment pattern (replacing the prior list-of-records pattern). Adding a classifier means adding a constructor here; the type checker propagates the addition to every projection function and every consumer that pattern-matches on Classifier. See CHANGELOG.md 0.230.179 for the rationale.

Inventory provenance #

Bridge to legacy #

Classifier.toEntry : Classifier → ClassifierEntry is the migration seam to the old Typology.ClassifierEntry record type that sibling fragments (Mandarin, Shan, Chol) and Phenomena/Classifiers/Typology still consume. Once those fragments are migrated to the same enum pattern, both this bridge and ClassifierEntry itself can be retired.

Out of scope #

source
inductive Fragments.Japanese.Classifier :
Type

The closed inventory of Japanese numeral classifiers. Constructors are named by Hepburn romanization, with kanji-distinct homophones disambiguated by content (e.g., kenBuilding 軒 vs kenIncident 件).

Instances For
    source
    @[implicit_reducible]
    instance Fragments.Japanese.instDecidableEqClassifier :
    DecidableEq Classifier
    Equations
    source
    @[implicit_reducible]
    instance Fragments.Japanese.instReprClassifier :
    Repr Classifier
    Equations
    source
    def Fragments.Japanese.instReprClassifier.repr :
    Classifier → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Fragments.Japanese.instBEqClassifier :
      BEq Classifier
      Equations
      source
      def Fragments.Japanese.instBEqClassifier.beq :
      Classifier → Classifier → Bool
      Equations
      Instances For
        source
        def Fragments.Japanese.Classifier.core :
        List Classifier

        The 27 core classifiers from @cite{downing-1996} (UNVERIFIED: Table 1.1).

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Fragments.Japanese.Classifier.extended :
          List Classifier

          The 6 extended classifiers from @cite{downing-1996} (UNVERIFIED: Table 1.2).

          Equations
          • One or more equations did not get rendered due to their size.
          Instances For
            source
            def Fragments.Japanese.Classifier.sudoAdditions :
            List Classifier

            The 3 additional classifiers from @cite{sudo-2016}'s worked examples (eqs. 4, 9a, 9b): -rin (flowers), -kumi (pair), -daasu (dozen).

            Equations
            Instances For
              source
              def Fragments.Japanese.Classifier.all :
              List Classifier

              The full inventory: Downing core ++ Downing extended ++ Sudo additions. Source-of-truth for consumer iteration (lookup, aggregations) and the Fintype instance.

              Equations
              Instances For
                source
                theorem Fragments.Japanese.Classifier.all_nodup :
                all.Nodup
                source
                theorem Fragments.Japanese.Classifier.mem_all (c : Classifier) :
                c ∈ all
                source
                @[implicit_reducible]
                instance Fragments.Japanese.instFintypeClassifier :
                Fintype Classifier
                Equations

                §1: Surface form #

                source
                def Fragments.Japanese.Classifier.form :
                Classifier → String

                The kanji (or hiragana, for -tsu) form of the classifier.

                Equations
                Instances For
                  source
                  def Fragments.Japanese.Classifier.romaji :
                  Classifier → String

                  Hepburn romanization of the classifier.

                  Equations
                  Instances For
                    source
                    def Fragments.Japanese.Classifier.gloss :
                    Classifier → String

                    A short English gloss describing the classifier's selection criterion.

                    Equations
                    Instances For

                      §2: Semantic parameters and shape #

                      source
                      def Fragments.Japanese.Classifier.encodes :
                      Classifier → List Typology.SemanticParameter

                      The semantic parameters this classifier encodes (@cite{aikhenvald-2000} typological vocabulary).

                      Every constructor has an explicit arm; no fall-through. Adding a classifier requires deciding what it encodes — the type checker enforces it.

                      Equations
                      Instances For
                        source
                        def Fragments.Japanese.Classifier.shapeDim :
                        Classifier → Option Typology.ShapeDimension

                        Shape dimensionality sub-classification per @cite{allan-1977}'s 1D/2D/3D scheme (cf. @cite{downing-1996}). Only meaningful when encodes includes .shape.

                        -rin 輪 is left as none: although it encodes shape, it tracks boundedness/ring-form (wheels, single blossoms) rather than fitting cleanly on the 1D/2D/3D axis. See encodes, where -rin carries .shape and .boundedness.

                        Equations
                        Instances For

                          §3: Property predicates #

                          source
                          def Fragments.Japanese.Classifier.IsMensural (c : Classifier) :
                          Prop

                          A classifier is mensural if it counts entities by a measure (containers, portions, drops, fixed-quantity multiples) rather than by atomic instances. -daasu ダース (← English "dozen") is mensural since it counts in fixed groups of 12.

                          Equations
                          Instances For
                            source
                            @[implicit_reducible]
                            instance Fragments.Japanese.Classifier.instDecidablePredIsMensural :
                            DecidablePred IsMensural
                            Equations
                            source
                            def Fragments.Japanese.Classifier.IsDefault (c : Classifier) :
                            Prop

                            A classifier is the default (semantically bleached, residue) classifier of the language. Japanese: tsu.

                            Equations
                            Instances For
                              source
                              @[implicit_reducible]
                              instance Fragments.Japanese.Classifier.instDecidablePredIsDefault :
                              DecidablePred IsDefault
                              Equations
                              source
                              def Fragments.Japanese.Classifier.Encodes (c : Classifier) (p : Typology.SemanticParameter) :
                              Prop

                              c encodes the semantic parameter p iff p ∈ c.encodes.

                              Equations
                              Instances For
                                source
                                @[implicit_reducible]
                                instance Fragments.Japanese.Classifier.instDecidableEncodes (c : Classifier) (p : Typology.SemanticParameter) :
                                Decidable (c.Encodes p)
                                Equations

                                §4: Lookup and aggregations #

                                source
                                def Fragments.Japanese.Classifier.defaultClassifier? :
                                Option Classifier

                                The default classifier of Japanese, derived from IsDefault.

                                Equations
                                Instances For
                                  source
                                  def Fragments.Japanese.Classifier.lookup (s : String) :
                                  Option Classifier

                                  Lookup a classifier by surface form. Returns none if the form is not in the inventory.

                                  Equations
                                  Instances For
                                    source
                                    def Fragments.Japanese.Classifier.allEncodedParams :
                                    List Typology.SemanticParameter

                                    The list of all semantic parameters encoded by some classifier in the inventory (with duplicates removed). Used by Phenomena/Classifiers/Typology to compute preferredSemantics.

                                    Equations
                                    Instances For

                                      §5: Bridge to legacy ClassifierEntry #

                                      Migration seam: Phenomena/Classifiers/Typology.lean and the sibling fragments (Mandarin, Shan, Chol) still consume Typology. ClassifierEntry. toEntry projects a typed Classifier back to the legacy record so cross-language aggregations continue to work during the transitional period.

                                      source
                                      def Fragments.Japanese.Classifier.toEntry (c : Classifier) :
                                      Typology.ClassifierEntry

                                      Convert a typed Classifier to the legacy record. Migration-seam only; new code should consume Classifier and its projections directly.

                                      Equations
                                      Instances For
                                        source
                                        def Fragments.Japanese.Classifier.allEntries :
                                        List Typology.ClassifierEntry

                                        The full inventory as legacy records. Bridge for typology-side code that still expects List ClassifierEntry.

                                        Equations
                                        Instances For

                                          §6: Structural theorems #

                                          source
                                          theorem Fragments.Japanese.Classifier.inventory_size :
                                          all.length = 36

                                          The inventory has 36 classifiers (27 Downing core + 6 Downing extended + 3 Sudo examples).

                                          source
                                          theorem Fragments.Japanese.Classifier.default_eq_tsu :
                                          defaultClassifier? = some tsu

                                          The default classifier exists and is tsu.

                                          source
                                          theorem Fragments.Japanese.Classifier.isDefault_iff_tsu (c : Classifier) :
                                          c.IsDefault ↔ c = tsu

                                          tsu is the only classifier flagged as default.

                                          source
                                          theorem Fragments.Japanese.Classifier.mensural_count :
                                          (List.filter (fun (c : Classifier) => decide c.IsMensural) all).length = 4

                                          Exactly four classifiers are mensural: hai, shoku, teki, daasu.

                                          source
                                          theorem Fragments.Japanese.Classifier.specific_classifiers_have_semantics (c : Classifier) :
                                          ¬c.IsDefault → ¬c.IsMensural → c.encodes ≠ []

                                          Every non-default sortal classifier encodes at least one semantic parameter. The default tsu is the only semantically empty classifier.

                                          source
                                          theorem Fragments.Japanese.Classifier.all_dimensions_attested :
                                          (∃ (c : Classifier), c.shapeDim = some Typology.ShapeDimension.oneD) ∧ (∃ (c : Classifier), c.shapeDim = some Typology.ShapeDimension.twoD) ∧ ∃ (c : Classifier), c.shapeDim = some Typology.ShapeDimension.threeD

                                          All three shape dimensions are attested in the inventory.

                                          source
                                          theorem Fragments.Japanese.Classifier.ken_disambiguation :
                                          kenBuilding.form ≠ kenIncident.form

                                          軒 kenBuilding and 件 kenIncident are distinct classifiers sharing the same Hepburn romanization but differing in kanji form.

                                          source
                                          theorem Fragments.Japanese.Classifier.ken_homophony :
                                          kenBuilding.romaji = kenIncident.romaji

                                          軒 and 件 share their romanization (the homophony Downing flags).