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
ParticipantType its case region (ParticipantType.toCaseRegion), maps
regions to morphological cases under accusative and ergative alignment, and
sharpens the connectedness claim: each core region is an order interval
anchored at its pole (toCaseRegion_eq_nomErg_iff etc.), so connectedness
is mathlib's Set.OrdConnected, inherited from Set.Ici/Set.Icc. The
dative region unifies recipients, experiencers, and second arguments of
two-place communication/service verbs (§5.1, Fig. 7).
Case regions (§4, Figs. 6–7) #
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
order intervals anchored at the poles (toCaseRegion_eq_nomErg_iff
etc.). oblique is the residual "middle region" (Grimm p.532–533) —
not connected (oblique_not_orderConvex).
- 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, and second arguments of two-place communication/service verbs (§5.1, Fig. 7).
- oblique : CaseRegion
Oblique: the middle region between core cases.
Instances For
Equations
- ArgumentStructure.instDecidableEqCaseRegion x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
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
Maps a case region to its canonical morphological case in an accusative alignment system.
Equations
Instances For
Maps a case region to its canonical morphological case in an ergative alignment system.
Equations
Instances For
Core case regions are order intervals (Grimm 2011 abstract + §4) #
The abstract's central claim — a core case marker is a connected region
"spreading outwards from the maximal agent and maximal patient nodes" — in
sharpened form: each core region is an order interval anchored at its
pole. NOM/ERG is the up-set of minimalInstigator (its top is
maximalAgent = ⊤); ACC/ABS runs from maximalPatient up to the
contact-verb patient; the dative sits above sentientNonInstigator.
Order-convexity ("connectedness") follows by transitivity.
The bottom of the NOM/ERG interval: instigation alone, at total persistence — the minimal acceptable agent of kill (§2.3: natural forces such as electricity or the explosion).
Equations
- ArgumentStructure.minimalInstigator = { agentivity := ArgumentStructure.Agentivity.mk false false true false, persistence := ⊤ }
Instances For
NOM/ERG is the up-set of the minimal instigator — the interval from
minimalInstigator to maximalAgent = ⊤.
ACC/ABS is the interval from the maximal patient to the contact-verb
patient: ⊥ agentivity, persistence between exPersBeginning and
quPersBeginning.
The dative is the interval above sentientNonInstigator:
sentience without instigation, pinned at quPersBeginning.
Connectedness #
With the interval characterizations, the regions are literally Set.Ici /
Set.Icc, so connectedness is mathlib's Set.OrdConnected.
The NOM/ERG region as a set: the up-set of the minimal instigator.
The ACC/ABS region as a set: the interval from the maximal patient to the contact-verb patient.
The dative region as a set: the interval above sentientNonInstigator.
Connectedness of NOM/ERG (Grimm's abstract), from the interval form.
Connectedness of ACC/ABS, from the interval form.
Connectedness of the dative, from the interval form.
Counterexample showing oblique is NOT connected. 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.532–533): oblique is the residual region between maximal agent
and maximal patient, not a positively-characterised connected case.