The Agentivity Lattice @cite{grimm-2011} #
@cite{grimm-2011} reformulates @cite{dowty-1991}'s proto-role entailments as privative features organized into a lattice via subset inclusion. The key innovations over Dowty:
Privative opposition: Proto-Patient is not a separate cluster but the underspecified (∅) pole of each agentivity feature. "Patient" = lacking agentive properties.
Instigation replaces causation: Dowty's "causing an event in another participant" is decomposed into "instigation" — independent action whose effects can be attributed to the argument. This removes the relational aspect (causation implies a second participant; instigation does not).
Persistence replaces P-Patient features: Dowty's 5 P-Patient entailments (CoS, IT, CA, stationary, DE) are replaced by 4 persistence dimensions tracking whether the entity persists existentially and qualitatively at the beginning and end of the event.
Lattice structure: The powerset of features, ordered by inclusion and constrained by logical dependencies (volition → sentience), forms a lattice. Cases are connected regions of this lattice.
Mathlib integration #
All ordering infrastructure uses Mathlib typeclasses:
AgentivityNode:Lattice,BoundedOrder,Fintype(16 elements)PersistenceLevel:Lattice,BoundedOrder,Fintype(5 elements)GrimmNode:PartialOrder,BoundedOrder,Fintype(80 elements)
Bridges #
AgentivityNode.fromEntailmentProfile→EntailmentProfile(proto-roles)PersistenceLevel.fromEntailmentProfile→EntailmentProfile(proto-roles)GrimmNode.toCaseRegion→Core.Case(case assignment)- Transitivity hierarchy →
Tsunodaverb classification
The four agentivity primitives (Table 2 (agentive properties), p.520).
Each has an agentive (+) and non-agentive (∅) pole. The non-agentive pole is not a separate feature — it is simply the absence of the agentive property. This is the privative opposition that replaces Dowty's two independent clusters.
- volition : Bool
+volition: the participant intends to bring about the event.
- sentience : Bool
+sentience: conscious involvement in the action or state.
- instigation : Bool
+instigation: prior independent action whose effects can be attributed to this argument. Replaces Dowty's "causation" (p.521).
- motion : Bool
+motion: the argument is in motion during the event.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Validity constraint: volition presupposes sentience (p.521, following @cite{dowty-1991} p.607).
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableValid a = id inferInstance
Number of positive agentivity features (= height in the lattice).
Equations
- a.featureCount = a.volition.toNat + a.sentience.toNat + a.instigation.toNat + a.motion.toNat
Instances For
Equivalence with Bool⁴ for Fintype derivation.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instFintypeAgentivityNode = Fintype.ofEquiv (Bool × Bool × Bool × Bool) Semantics.ArgumentStructure.AgentivityLattice.AgentivityNode.equiv.symm
Equations
- One or more equations did not get rendered due to their size.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableRelAgentivityNodeLe a b = instDecidableEqBool (Semantics.ArgumentStructure.AgentivityLattice.AgentivityNode.leBool✝ a b) true
Lattice: componentwise ∨ for join, ∧ for meet.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
The five valid persistence levels (p.524–525, Fig. 2).
Each level is a valid combination of four persistence dimensions:
- ExPB: existential persistence (beginning) — entity exists before event
- ExPE: existential persistence (end) — entity exists after event
- QuPB: qualitative persistence (beginning) — qualities unchanged before
- QuPE: qualitative persistence (end) — qualities unchanged after
Constraints (ExPB→QuPB, QuPE→ExPE, etc.) reduce the 16 possible combinations to exactly 5.
- totalNonPersistence : PersistenceLevel
∅ExPB, ∅ExPE, ∅QuPB, ∅QuPE — entity has no entailed existence. Arguments of seek, want; negated copulas.
- exPersEnd : PersistenceLevel
∅ExPB, +ExPE, ∅QuPB, +QuPE — entity comes into existence. Objects of build, invent; subjects of appear.
- exPersBeginning : PersistenceLevel
+ExPB, ∅ExPE, +QuPB, ∅QuPE — entity exists before, ceases to exist. Subjects of die, evaporate; objects of destroy, ruin.
- quPersBeginning : PersistenceLevel
+ExPB, +ExPE, +QuPB, ∅QuPE — entity persists but is qualitatively changed. Objects of transitive move, dim, frighten; intransitive subjects of fall.
- totalPersistence : PersistenceLevel
+ExPB, +ExPE, +QuPB, +QuPE — entity persists unchanged throughout. Prototypical transitive subjects; unaffected objects of see, cut at.
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableEqPersistenceLevel 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
Existential persistence at beginning (positive feature). Also serves as "entity exists at the beginning of the event."
Equations
Instances For
Existential persistence at end (positive feature).
Equations
Instances For
Qualitative persistence at beginning (positive feature).
Equations
Instances For
Qualitative persistence at end (positive feature).
Equations
Instances For
Number of positive persistence features.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.featureCount = 0
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersEnd.featureCount = 2
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.exPersBeginning.featureCount = 2
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.quPersBeginning.featureCount = 3
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.featureCount = 4
Instances For
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableRelPersistenceLevelLe a b = instDecidableEqBool (Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.leBool✝ a b) true
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Join on persistence levels. The 5 valid levels do not form a sublattice of the powerset on {ExPB, ExPE, QuPB, QuPE} — the join is the smallest valid level containing the union of features.
Equations
- One or more equations did not get rendered due to their size.
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.sup' b = b
- a.sup' Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence = a
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.sup' b = Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence
- a.sup' Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence = Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence
Instances For
Meet on persistence levels. The largest valid level contained in the intersection of features.
Equations
- One or more equations did not get rendered due to their size.
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence.inf' b = b
- a.inf' Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalPersistence = a
- Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence.inf' b = Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence
- a.inf' Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence = Semantics.ArgumentStructure.AgentivityLattice.PersistenceLevel.totalNonPersistence
Instances For
Equations
- One or more equations did not get rendered due to their size.
A node in the full agentivity lattice = agentivity features × persistence level, subject to:
- volition → sentience (agentivity constraint)
- If the argument does not exist at the beginning (totalNonPersistence or exPersEnd), it cannot have any agentivity properties (p.526–527).
- agentivity : AgentivityNode
- persistence : PersistenceLevel
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
The agentivity constraint: volition → sentience.
Equations
- n.AgentivityValid = n.agentivity.Valid
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableAgentivityValid n = id inferInstance
The cross-lattice constraint: if the argument does not exist at the beginning of the event, it cannot have any agentivity properties.
Equations
- n.CrossValid = (n.persistence.exPersB = true ∨ n.agentivity = ⊥)
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableCrossValid n = id inferInstance
Full validity: both constraints satisfied.
Equations
- n.Valid = (n.AgentivityValid ∧ n.CrossValid)
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableValid_1 n = id inferInstance
Total feature count (agentivity + persistence).
Equations
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Product order: componentwise ≤ on agentivity and persistence.
Equations
- One or more equations did not get rendered due to their size.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instLTGrimmNode = { lt := fun (a b : Semantics.ArgumentStructure.AgentivityLattice.GrimmNode) => a ≤ b ∧ ¬b ≤ a }
Equations
- One or more equations did not get rendered due to their size.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableRelGrimmNodeLe a b = instDecidableAnd
Equations
- One or more equations did not get rendered due to their size.
Equations
- One or more equations did not get rendered due to their size.
Componentwise lattice: meet/join on each axis independently.
Equations
- One or more equations did not get rendered due to their size.
Maximal Agent (Fig. 4): all agentivity features, total persistence. The prototypical transitive subject.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Maximal Patient (Fig. 4): no agentivity features, existential persistence (beginning). The prototypical affected object that ceases to exist (break, destroy).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The "effector" participant type: instigation + motion, total persistence. The canonical agent of effective action verbs (kill, break). §3, labeled Ia/IIa in Fig. 5.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The lattice position {sentience} × qualitative persistence (beginning). Per Grimm 2011 §5.1, diverse uses of the dative converge on this single region — recipients, experiencers, and benefactives are aliases below.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Dative experiencer of psych verbs (§5.1.1). Alias of
sentientNonInstigatorNode — the convergence with recipientNode is by
construction, not a theorem.
Equations
Instances For
Canonical dative recipient (Fig. 7). Alias of sentientNonInstigatorNode
— see the docstring there for the unified treatment.
Equations
Instances For
A node is in the transitivity region iff its persistence level is in {exPersBeginning, quPersBeginning, totalPersistence}.
The transitivity region excludes totalNonPersistence and exPersEnd because the prototypical transitive event requires both participants to exist at the beginning (p.529–530).
Equations
- n.InTransitiveRegion = (n.persistence.exPersB = true)
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableInTransitiveRegion n = id inferInstance
Tsunoda's transitivity hierarchy (§3, example 8).
| Class | Example verbs | Transitivity |
|---|---|---|
| I | kill, break | Highest |
| II | shoot, hit | Middle |
| III | search, seek | Lowest |
- resultativeEffective : TransitivityClass
Resultative Effective Action: kill, break. Object is destroyed (exPersBeginning). Maximal opposition between agent and patient.
- contact : TransitivityClass
Contact: shoot, hit. Object is affected but persists (quPersBeginning). Less opposition than Class I.
- pursuit : TransitivityClass
Pursuit: search, seek. Object may not even exist (totalNonPersistence). Outside the transitivity region.
Instances For
Equations
- Semantics.ArgumentStructure.AgentivityLattice.instDecidableEqTransitivityClass 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
The canonical patient position for each transitivity class
(Fig. 5). The agent position for all three classes is effectorAgent
(Fig. 5, Ia/IIa share the same agent node; Grimm doesn't separately
label IIIa).
Equations
- One or more equations did not get rendered due to their size.
Instances For
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
Equations
- Semantics.ArgumentStructure.AgentivityLattice.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
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
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.nomErg.toAccusativeCase = UD.Case.nom
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.accAbs.toAccusativeCase = UD.Case.acc
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.dative.toAccusativeCase = UD.Case.dat
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.oblique.toAccusativeCase = UD.Case.inst
Instances For
Maps a case region to its canonical morphological case in an ergative alignment system.
Equations
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.nomErg.toErgativeCase = UD.Case.erg
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.accAbs.toErgativeCase = UD.Case.abs
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.dative.toErgativeCase = UD.Case.dat
- Semantics.ArgumentStructure.AgentivityLattice.CaseRegion.oblique.toErgativeCase = UD.Case.inst
Instances For
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
- Semantics.ArgumentStructure.AgentivityLattice.IsOrderConvex P = ∀ ⦃a b x : α⦄, P a → P b → a ≤ x → x ≤ b → P x
Instances For
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.
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].
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.
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.
Map Dowty's P-Agent entailments to Grimm's agentivity features.
The correspondence is direct for 3 of 4 features:
- volition = volition
- sentience = sentience
- causation → instigation (p.521)
- movement = motion
Independent existence is handled by the persistence dimension.
Equations
Instances For
Map Dowty's P-Patient entailments to Grimm's persistence level.
This is an approximate mapping — Grimm's system is genuinely different from Dowty's. The diagnostic features:
- DE + IT → exPersEnd: entity created incrementally (build, invent)
- DE + ¬IT → exPersBeginning: entity ceases to exist (die, evaporate)
- IT + ¬DE → exPersBeginning: entity consumed incrementally (eat)
- CoS + ¬IT + ¬DE → quPersBeginning: changed but persists (kick, move)
- ¬CoS + ¬DE → totalPersistence or totalNonPersistence
Dowty's DE ("does not exist independently of the event") maps to Grimm's creation/destruction axis. IT (incremental theme) disambiguates: DE+IT = creation (exPersEnd), DE+¬IT = destruction (exPersBeginning).
Equations
- One or more equations did not get rendered due to their size.
Instances For
Map a full EntailmentProfile to a GrimmNode.
The agentivity features come from the P-Agent entailments; the persistence level comes from the P-Patient entailments.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Equations
- One or more equations did not get rendered due to their size.
Instances For
Persistence incomparability: exPersEnd and exPersBeginning are incomparable — neither is a subset of the other's features.
Their join is ⊤ (totalPersistence).
Their meet is ⊥ (totalNonPersistence).
Maximal agent is ⊤ on the combined lattice.
Grimm's agentivity lattice ordering is consistent with Dowty's PAgentDominates: if Grimm a ≤ Grimm b on agentivity, then Dowty a dominates Dowty b on P-Agent features.
This holds because the feature-to-feature mapping is a bijection on the first 4 P-Agent features (volition, sentience, causation=instigation, movement=motion).
The Dowty→Grimm bridge is monotone: if one EntailmentProfile dominates another on P-Agent features, the corresponding AgentivityNodes are ordered.
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.
Agents are upwards closed in the agentivity dimension
(p.528): if a qualifies as agent for a predicate
(i.e., a has at least the entailments required by the verb), then
any b ≥ a also qualifies. An entity with more agentive properties
can always fill an agent role requiring fewer.
Formally: the set of acceptable agents for a verb with minimum
requirement minReq is {a | minReq ≤ a}, which is an upper set.
Patients are downwards closed in the persistence dimension
(p.528): if p qualifies as patient (i.e., p
has at most the persistence features of the verb's patient slot),
then any q ≤ p also qualifies. A more affected entity (less
persistence) can always fill a patient role.
Formally: the set of acceptable patients for a verb with maximum
persistence maxPers is {p | p ≤ maxPers}, which is a lower set.
exPersEnd and quPersBeginning are incomparable (neither ≤ the other). Their feature sets are {ExPE, QuPE} and {ExPB, ExPE, QuPB} — QuPE ∉ {ExPB, ExPE, QuPB} and ExPB ∉ {ExPE, QuPE}. This means the persistence lattice has TWO independent paths from ⊥ to ⊤: (1) ⊥ → exPersEnd → ⊤ (2) ⊥ → exPersBeginning → quPersBeginning → ⊤
The persistence lattice inclusion chain (2) from Fig. 2: exPersBeginning ≤ quPersBeginning ≤ totalPersistence.