Documentation

Linglib.Semantics.ArgumentStructure.Agentivity.CaseRegions

Case as a connected region of the agentivity lattice [Gri11] #

[Gri11] §4's central claim: a core case marker corresponds to a connected region of the agentivity lattice, spreading outwards from the maximal agent and maximal patient nodes (Figs. 6–7). This file assigns each GrimmNode its case region (GrimmNode.toCaseRegion), maps regions to morphological cases under accusative and ergative alignment, and proves the connectedness claim for the three core regions as order-convexity (IsOrderConvex). The dative region unifies recipients, experiencers, and benefactives (§5.1, Fig. 7).

Case regions (§4, Figs. 6–7) #

source
inductive ArgumentStructure.AgentivityLattice.CaseRegion :
Type

Case regions on the agentivity lattice. Per Grimm 2011 (abstract, §2.3, §4), a core case marker corresponds to a connected region of the lattice; the three core regions (nomErg, accAbs, dative) are proved order-convex (IsOrderConvex) below. oblique is the residual "middle region" (Grimm p.533) — not claimed to be connected.

  • nomErg : CaseRegion

    Nominative (accusative systems) / Ergative (ergative systems): the region spreading from maximal agent. Marks subjects.

  • accAbs : CaseRegion

    Accusative (accusative systems) / Absolutive (ergative systems): the region spreading from maximal patient and existential persistence (beginning). Marks objects.

  • dative : CaseRegion

    Dative: the region around sentience + qualitative persistence (beginning). Marks recipients, experiencers, benefactives (§5.1, Fig. 7).

  • oblique : CaseRegion

    Oblique: the middle region between core cases.

Instances For
    source
    @[implicit_reducible]
    instance ArgumentStructure.AgentivityLattice.instDecidableEqCaseRegion :
    DecidableEq CaseRegion
    Equations
    source
    @[implicit_reducible]
    instance ArgumentStructure.AgentivityLattice.instReprCaseRegion :
    Repr CaseRegion
    Equations
    source
    def ArgumentStructure.AgentivityLattice.instReprCaseRegion.repr :
    CaseRegion → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def ArgumentStructure.AgentivityLattice.GrimmNode.toCaseRegion (n : GrimmNode) :
      CaseRegion

      Predicts the case region for a node based on its lattice position.

      • nomErg: has instigation + total persistence — the prototypical transitive subject region.
      • accAbs: no agentivity + persistence with existsBeginning — the prototypical affected object region.
      • dative: sentience (without instigation) + qualitative persistence (beginning) — recipients, experiencers, benefactives.
      • oblique: everything else.
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def ArgumentStructure.AgentivityLattice.CaseRegion.toAccusativeCase :
        CaseRegion → Case

        Maps a case region to its canonical morphological case in an accusative alignment system.

        Equations
        Instances For
          source
          def ArgumentStructure.AgentivityLattice.CaseRegion.toErgativeCase :
          CaseRegion → Case

          Maps a case region to its canonical morphological case in an ergative alignment system.

          Equations
          Instances For

            Connectedness of core case regions (Grimm 2011 abstract + §4) #

            source
            def ArgumentStructure.AgentivityLattice.IsOrderConvex {α : Type u_1} [LE α] (P : α → Prop) :
            Prop

            A predicate on a partial order is order-convex if it is closed under intervals: whenever P a and P b and a ≤ x ≤ b, also P x. This is the standard order-theoretic capture of "connected region" in a finite lattice.

            Equations
            Instances For
              source
              theorem ArgumentStructure.AgentivityLattice.nomErg_orderConvex :
              IsOrderConvex fun (n : GrimmNode) => n.toCaseRegion = CaseRegion.nomErg

              The nomErg region is order-convex: any node between two nomErg nodes is itself nomErg. The region equals {n | n.agentivity.instigation = true ∧ n.persistence = .totalPersistence}, the intersection of an upper set (instigation = true) with the singleton at top persistence.

              source
              theorem ArgumentStructure.AgentivityLattice.accAbs_orderConvex :
              IsOrderConvex fun (n : GrimmNode) => n.toCaseRegion = CaseRegion.accAbs

              The accAbs region is order-convex. It equals {n | n.agentivity = ⊥ ∧ n.persistence ∈ {.exPersBeginning, .quPersBeginning}} — the singleton at bottom agentivity intersected with the persistence interval [.exPersBeginning, .quPersBeginning].

              source
              theorem ArgumentStructure.AgentivityLattice.dative_orderConvex :
              IsOrderConvex fun (n : GrimmNode) => n.toCaseRegion = CaseRegion.dative

              The dative region is order-convex. It equals {n | n.agentivity.sentience = true ∧ n.agentivity.instigation = false ∧ n.persistence = .quPersBeginning} — sentience upper set ∩ instigation lower set ∩ persistence singleton.

              source
              theorem ArgumentStructure.AgentivityLattice.oblique_not_orderConvex :
              ¬IsOrderConvex fun (n : GrimmNode) => n.toCaseRegion = CaseRegion.oblique

              Counterexample showing oblique is NOT order-convex. With a = ⟨{motion}, .quPersBeginning⟩ and b = ⟨{motion, sentience, instigation}, .quPersBeginning⟩, both oblique, the in-between node ⟨{motion, sentience}, .quPersBeginning⟩ is dative. This is consistent with Grimm (p.533): oblique is the residual region between maximal agent and maximal patient, not a positively-characterised connected case.

              Dative polysemy (§5.1) #

              source
              theorem ArgumentStructure.AgentivityLattice.sentientNonInstigator_in_dative :
              sentientNonInstigatorNode.toCaseRegion = CaseRegion.dative

              The dative region unifies recipients, experiencers, and second arguments of communication/service verbs — they all share the semantic properties of sentience and qualitative persistence (beginning) (Fig. 7, p.536).

              Because recipientNode and experiencerNode are abbrevs of sentientNonInstigatorNode, the convergence is by construction; the theorem below asserts only that this single lattice position falls in the dative case region.