Documentation

Linglib.Morphology.Morphotactics.RelevanceHierarchy

Bybee's relevance hierarchy #

[Byb85]'s comparative inventory of verbal inflectional categories, ordered by semantic relevance to the stem, and the stem-outward sortedness this order induces on affix sequences.

MorphCategory is a comparative concept, not a universal slot inventory: languages own their slot types (AffixTemplate (Slot), Mayan.VerbSlot), and cross-linguistic relevance claims are stated by pulling the order back along a fragment-supplied Slot → MorphCategory hom — sortedness of the image, with the hom carrying the analytical commitments (see Fragments/Japanese/Morph.lean for the worked example). The law layer is mathlib's: the order is Preorder.lift peripherality and RespectsRelevanceHierarchy is List.SortedLE.

Main definitions #

source
inductive Morphology.MorphCategory :
Type

Morpheme functional category: [Byb85]'s comparative inventory (plus documented linglib extensions — see peripherality).

Categories are ordered by semantic relevance to the verb stem: more relevant categories appear closer to the stem in suffixal morphology. A comparative concept: language-particular slot systems relate to it by fragment-supplied homs, not by instantiation.

Instances For
    source
    def Morphology.instReprMorphCategory.repr :
    MorphCategory → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Morphology.instReprMorphCategory :
      Repr MorphCategory
      Equations
      source
      def Morphology.instDecidableEqMorphCategory.decEq (x✝ x✝¹ : MorphCategory) :
      Decidable (x✝ = x✝¹)
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[implicit_reducible]
        instance Morphology.instDecidableEqMorphCategory :
        DecidableEq MorphCategory
        Equations
        source
        def Morphology.MorphCategory.peripherality :
        MorphCategory → ℕ

        Peripherality: numerical embedding of Bybee's relevance hierarchy where higher = farther from stem = less semantically relevant.

        In Bybee's text, "high relevance" means more semantically integrated with the stem ([Byb85] Ch 2 §2.1 p. 13). The substrate uses the opposite numerical direction: stem = 0 (most relevant), agreement = 8 (least relevant), so that Nat ordering mirrors stem-outward linear position in suffixing morphology (Ch 2 §6 iconicity, p. 33). The field name peripherality makes this directionality explicit and avoids the wrong-on-its-face gloss "high relevance rank means low relevance."

        Categories from Bybee 1985 Ch 2 §3 (verified against the book): valence, voice, aspect, tense, mood, agreement.

        Linglib extensions (NOT in Bybee 1985 — flag in any consumer that reads these ranks):

        • derivation (rank 1): Bybee Ch 4 argues lex/deriv/infl is a continuum, not a discrete level on the relevance scale.
        • number (rank 3): Bybee discusses verbal-number agreement at the low end (with person agreement). Noun number is treated separately (Ch 2 §6 cites [Gre63] only, "stem < number < case" for nouns). Cross-comparison of noun-number rank with verb-aspect rank is an artifact of unifying both onto one scale.
        • degree (rank 5): Bybee never discusses adjectival degree morphology. Comparative morphology is often derivational cross-linguistically ([Sta13b]).
        • negation (rank 7): Bybee discusses negation as a kind of mood (Part II Ch 8 §5), not a separate level. Rank 7 is plausible per [Mie05] cross-linguistic ordering data, but is a linglib extension.
        • nonfinite (rank 9): not on Bybee's hierarchy at all (nonfinite morphology often changes syntactic category, outside the scope of inflectional categories proper).
        Equations
        Instances For

          The relevance order #

          peripherality is a rank function — a numeric embedding. The object the hierarchy is really about is the order it induces: which categories are more stem-relevant than which. All relevance-hierarchy code — this file's RespectsRelevanceHierarchy and the consumers in Studies/ — speaks in that order via RelevanceLE / RelevanceLT; the specific ℕ values of peripherality are an implementation detail (only their comparisons carry meaning, as relevanceLE_iff_peripherality records).

          source
          @[implicit_reducible]
          instance Morphology.instPreorderMorphCategory :
          Preorder MorphCategory

          The relevance preorder: a ≤ b iff a is at least as stem-relevant as b. Only a preorder — peripherality is non-injective (voice and number share a rank), so there is no antisymmetry.

          Equations
          source
          def Morphology.MorphCategory.RelevanceLE (a b : MorphCategory) :
          Prop

          a is at least as stem-relevant as b, named. This is the Preorder order (Iff.rfl); the name keeps consumer statements readable.

          Equations
          Instances For
            source
            def Morphology.MorphCategory.RelevanceLT (a b : MorphCategory) :
            Prop

            a is strictly more stem-relevant than b, named.

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Morphology.instDecidableRelMorphCategoryRelevanceLE :
              DecidableRel MorphCategory.RelevanceLE
              Equations
              source
              @[implicit_reducible]
              instance Morphology.instDecidableRelMorphCategoryRelevanceLT :
              DecidableRel MorphCategory.RelevanceLT
              Equations
              source
              theorem Morphology.MorphCategory.RelevanceLE.refl (a : MorphCategory) :
              a.RelevanceLE a

              The relevance order is reflexive.

              source
              theorem Morphology.MorphCategory.RelevanceLE.trans {a b c : MorphCategory} (h₁ : a.RelevanceLE b) (h₂ : b.RelevanceLE c) :
              a.RelevanceLE c

              The relevance order is transitive.

              source
              theorem Morphology.MorphCategory.RelevanceLE.total (a b : MorphCategory) :
              a.RelevanceLE b ∨ b.RelevanceLE a

              The relevance order is total: any two categories are comparable.

              source
              theorem Morphology.MorphCategory.RelevanceLT_iff {a b : MorphCategory} :
              a.RelevanceLT b ↔ a.RelevanceLE b ∧ ¬b.RelevanceLE a

              Strict relevance order is the strict part of the order.

              source
              theorem Morphology.MorphCategory.relevanceLE_iff_peripherality {a b : MorphCategory} :
              a.RelevanceLE b ↔ a.peripherality ≤ b.peripherality

              peripherality reflects the relevance order exactly: it is the canonical rank realizing the order, so the order carries precisely the information the rank does.

              source
              def Morphology.RespectsRelevanceHierarchy (slots : List MorphCategory) :
              Prop

              A morpheme ordering respects the relevance hierarchy when its categories are sorted stem-outward by the relevance order — mathlib's List.SortedLE under the relevance Preorder (equivalently Pairwise (· ≤ ·), via List.sortedLE_iff_pairwise).

              Equations
              Instances For
                source
                @[implicit_reducible]
                instance Morphology.instDecidablePredListMorphCategoryRespectsRelevanceHierarchy :
                DecidablePred RespectsRelevanceHierarchy
                Equations