Documentation

Linglib.Core.Case.Hierarchy

Blake's Case Hierarchy #

@cite{blake-1994}

Implicational hierarchy over case inventories with contiguity checking. The 9 UD-specific spatial cases all sit at the peripheral spatial tier (rank 1) since Blake's hierarchy collapses them into a single locative/ spatial group.

Inventory validity is the Set.OrdConnected-style contiguity property expressed in a form decide can mechanically check.

source
def Core.Case.hierarchyRank :
Case → Fin 7

Position on Blake's case hierarchy (@cite{blake-1994}, §5.8, ex. 68).

Higher rank = more likely to exist in a language's case inventory.

Ranks: 6 = core (NOM/ACC/ERG/ABS), 5 = GEN, 4 = DAT, 3 = LOC, 2 = ABL/INST, 1 = COM/ALL/PERL/BEN + UD spatial cases (ADE/INE/ILL/ELA/ SUB/SUP/DEL — Finnish/Hungarian fine-grained spatial), 0 = VOC/PART/CAUS/ESS/TRANSL/ABESS + UD's TER/TEM (terminative, temporal — peripheral non-spatial).

Codomain is Fin 7 — the boundedness is encoded in the type, not as a separate *_bounded theorem.

Equations
Instances For
    source
    def Core.Case.IsValidInventory (inv : Finset Case) :
    Prop

    An inventory is contiguous on Blake's hierarchy: every rank between two realized ranks is itself realized. Formalizes Blake's implicational tendency (1994, §5.8). Equivalent to Set.OrdConnected on the rank image, expressed here in the form decide can mechanically check.

    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Core.instDecidableIsValidInventory (inv : Finset Case) :
      Decidable (Case.IsValidInventory inv)
      Equations
      source
      theorem Core.two_case_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.acc}
      source
      theorem Core.three_case_with_gen_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.gen}
      source
      theorem Core.four_case_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.gen, UD.Case.dat}
      source
      theorem Core.five_case_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.gen, UD.Case.dat, UD.Case.loc}
      source
      theorem Core.seven_case_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.gen, UD.Case.dat, UD.Case.loc, UD.Case.abl, UD.Case.inst}
      source
      theorem Core.ergative_four_case_valid :
      Case.IsValidInventory {UD.Case.erg, UD.Case.abs, UD.Case.gen, UD.Case.dat}
      source
      theorem Core.split_ergative_valid :
      Case.IsValidInventory {UD.Case.nom, UD.Case.erg, UD.Case.abs, UD.Case.gen}
      source
      theorem Core.skip_gen_invalid :
      ¬Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.dat}
      source
      theorem Core.skip_gen_dat_invalid :
      ¬Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.loc}
      source
      theorem Core.skip_to_abl_invalid :
      ¬Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.abl}
      source
      theorem Core.skip_dat_invalid :
      ¬Case.IsValidInventory {UD.Case.nom, UD.Case.acc, UD.Case.gen, UD.Case.loc}