Documentation

Linglib.Core.Case.Grammaticalization

Case Grammaticalization #

@cite{heine-2009}

The case-marker grammaticalization cline (lexical > adposition > case affix > loss) and the extension paths from Heine (2009) Table 29.6. Three extension targets in Table 29.6 are not representable as Case values and are omitted: purposive (from allative, benefactive), manner (from comitative, instrumental), agent (from locative; collapses with ergative in our system).

Extension is the relation Case.Extends : Case → Case → Prop (Heine's Table 29.6 row pattern). Multi-step extension is just Relation.TransGen Case.Extends from mathlib — there is no separate two-step or n-step predicate to maintain.

source
inductive Core.CaseGramStage :
Type

Source category of a case marker on the grammaticalization cline (@cite{heine-2009} §29.1 eq. (1), §29.2).

noun, verb (> adverb) > adposition > case affix > loss

Parallel to Diachronic.Grammaticalization.GramStage (for verbal elements), but specific to case-marker development.

  • lexical : CaseGramStage

    Lexical noun or verb source (§29.2.1–29.2.2).

  • adposition : CaseGramStage

    Free adposition: preposition or postposition (§29.2.3).

  • caseAffix : CaseGramStage

    Bound case affix: suffix or prefix (§29.2.3 endpoint).

  • lost : CaseGramStage

    Case marker lost: erosion endpoint or merger.

Instances For
    source
    @[implicit_reducible]
    instance Core.instDecidableEqCaseGramStage :
    DecidableEq CaseGramStage
    Equations
    source
    @[implicit_reducible]
    instance Core.instReprCaseGramStage :
    Repr CaseGramStage
    Equations
    source
    def Core.instReprCaseGramStage.repr :
    CaseGramStage → ℕ → Std.Format
    Equations
    Instances For
      source
      def Core.CaseGramStage.boundedness :
      CaseGramStage → ℕ

      Boundedness increases monotonically along the case cline.

      Equations
      Instances For
        source
        @[implicit_reducible]
        instance Core.instLinearOrderCaseGramStage :
        LinearOrder CaseGramStage
        Equations
        source
        theorem Core.caseGramCline_ordered :
        CaseGramStage.lexical < CaseGramStage.adposition ∧ CaseGramStage.adposition < CaseGramStage.caseAffix ∧ CaseGramStage.caseAffix < CaseGramStage.lost
        source
        def Core.Case.Extends :
        Case → Case → Prop

        Direct extension between case functions (@cite{heine-2009} Table 29.6).

        Case.Extends c₁ c₂ holds iff a single row of Heine's table licenses extending a c₁-marker to c₂ uses. Direction is concrete/peripheral → abstract/core: the source function is less grammaticalized than the target.

        See also Typology.Possession.PossessionSource for @cite{heine-2009} Table 29.5 (possessive case sources, adapted from @cite{heine-1997}).

        Equations
        Instances For
          source
          def Core.Case.extensionTargets (c : Case) :
          Finset Case

          Direct-extension targets of c, as a Finset derived from Case.Extends. Useful for membership queries by decide.

          Equations
          Instances For
            source
            theorem Core.Case.mem_extensionTargets {c₁ c₂ : Case} :
            c₂ ∈ c₁.extensionTargets ↔ c₁.Extends c₂

            Case.Extends itself is the public Table 29.6 spec — concrete extension facts (Case.Extends .abl .inst, ¬ Case.Extends .nom .acc, etc.) are immediate by decide against the def and need not be re-stated as a thicket of named theorems. The chain theorems below bundle multiple table rows into the named Heine (2009) eq. (2) chains.

            source
            theorem Core.chain_all_ben :
            Case.Extends UD.Case.all UD.Case.ben

            Chain (2a): allative > benefactive > purposive. Only the first step is representable as Case → Case.

            source
            theorem Core.chain_all_dat_acc :
            Case.Extends UD.Case.all UD.Case.dat ∧ Case.Extends UD.Case.dat UD.Case.acc

            Chain (2b): allative > dative > accusative/O. Both steps are direct extensions.

            source
            theorem Core.chain_loc_com_inst :
            Case.Extends UD.Case.loc UD.Case.com ∧ Case.Extends UD.Case.com UD.Case.inst

            Chain (2c): locative > comitative > instrumental > manner. The first two steps are representable as Case → Case.

            source
            @[reducible, inline]
            abbrev Core.Case.ExtensionReachable :
            Case → Case → Prop

            Multi-step extension reachability — the transitive closure of Case.Extends. Composing chain rows of Table 29.6 produces an extension path of any finite length.

            Equations
            Instances For
              source
              @[implicit_reducible]
              instance Core.instDecidableRelCaseExtensionReachable :
              DecidableRel Case.ExtensionReachable

              Case.ExtensionReachable is decidable via the Core.Relation.ReflTransGen substrate's TransGen Fintype headline. The step function is Case.extensionTargets.

              Equations
              • One or more equations did not get rendered due to their size.
              source
              theorem Core.acc_reachable_from_all :
              Case.ExtensionReachable UD.Case.all UD.Case.acc

              Accusative is reachable from allative via dative (chain 2b).

              source
              theorem Core.inst_reachable_from_loc :
              Case.ExtensionReachable UD.Case.loc UD.Case.inst

              Instrumental is reachable from locative via comitative (chain 2c).