Documentation

Linglib.Fragments.Mayan.Tseltalan

Shared Tseltalan Infrastructure #

Descriptive types shared across the Tseltalan subgroup, Tsotsil and Tseltal ([AP25]; [Pol13a]). Both languages share agreement paradigm assignment and grammatical-function classification; they differ in agreement exponents and Set B marker position (Tsotsil prefixal or suffixal, Tseltal consistently suffixal).

Main declarations #

Implementation notes #

Agreement system ([AP25] Table 1):

FormFunctionTseltalTsotsil
Set AA, Psrprefixalprefixal
Set BS and Osuffixalprefixal/suffixal

Grammatical functions #

source
inductive Mayan.Tseltalan.GramFunction :
Type

Grammatical functions in Tseltalan — traditional Mayanist descriptive categories (footnote 9 of [AP25]) — determining which agreement marker set cross-references each argument.

Instances For
    source
    @[implicit_reducible]
    instance Mayan.Tseltalan.instDecidableEqGramFunction :
    DecidableEq GramFunction
    Equations
    source
    @[implicit_reducible]
    instance Mayan.Tseltalan.instReprGramFunction :
    Repr GramFunction
    Equations
    source
    def Mayan.Tseltalan.instReprGramFunction.repr :
    GramFunction → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def Mayan.Tseltalan.GramFunction.markerSet :
      GramFunction → MarkerSet

      The marker set cross-referencing each grammatical function (Set A = ergative/genitive, Set B = absolutive); shared across Tseltalan ([AP25], [Pol13a]).

      Equations
      Instances For

        Shared theorems #

        source
        theorem Mayan.Tseltalan.erg_gen_homophonous :
        GramFunction.A.markerSet = GramFunction.psr.markerSet

        Ergative-genitive homophony: Set A cross-references both transitive agents and possessors. A pan-Mayan pattern.

        source
        theorem Mayan.Tseltalan.abs_uniform :
        GramFunction.S_A.markerSet = MarkerSet.setB ∧ GramFunction.S_O.markerSet = MarkerSet.setB ∧ GramFunction.O.markerSet = MarkerSet.setB ∧ GramFunction.G.markerSet = MarkerSet.setB

        All absolutive arguments (S_A, S_O, O, G) use Set B.

        Absolutive position (LOW-ABS) #

        source
        def Mayan.Tseltalan.absPosition :
        ABSPosition

        Tseltalan absolutive morphemes appear in low (post-stem) position; both Tsotsil and Tseltal inherit this LOW-ABS constant. LOW-ABS refers to the structural position of the licensing head, not the linear position of every Set B exponent (which varies by language and context). [AP25] p. 97; [Pol13a].

        Equations
        Instances For

          Projection to canonical ArgumentRole #

          source
          def Mayan.Tseltalan.GramFunction.toArgumentRole? :
          GramFunction → Option Features.Prominence.ArgumentRole

          Project the Tseltalan Split-S grammatical function to the canonical ArgumentRole (S/A/P/R/T). Partial (Option-valued): .A → .A, .O → .P, .G → .R map cleanly; .S_A, .S_O → .S collapses the agentivity distinction (lossy but expected for cross-Mayan theorems that don't track Split-S); .psr → none, since possessors are DP-internal with no ArgumentRole analog. Cross-Mayan consumers use this projection; the Aissen-Polian possessor-extraction analysis uses GramFunction directly for its DP-internal claims.

          Equations
          Instances For