Participant types ([Gri11] §2.2, Fig. 3)

A participant type pairs an agentivity value with a persistence level — Grimm's term for a node of the full lattice ("each node of the lattice determines one type of participant"). The product carrier has 80 elements; Grimm's Fig. 3 lattice is the 38-element Valid subset (volition → sentience, and no agentivity without existence at the event's beginning, p.526–527).

Named participant types anchor the case regions (CaseRegion.lean): maximalAgent = ⊤, maximalPatient, effectorAgent, and the dative convergence point sentientNonInstigator. Tsunoda's transitivity hierarchy (§3, example 8) is TransitivityRank, with the canonical patient placement of each class (Fig. 5).

structure ArgumentStructure.ParticipantType : Type

A participant type: agentivity × persistence (80 elements). Grimm's Fig. 3 lattice is the 38-element Valid subset.

• agentivity : Agentivity
• persistence : PersistenceLevel

def ArgumentStructure.instDecidableEqParticipantType.decEq (x✝ x✝¹ : ParticipantType) : Decidable (x✝ = x✝¹)

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqParticipantType : DecidableEq ParticipantType

Equations

• ArgumentStructure.instDecidableEqParticipantType = ArgumentStructure.instDecidableEqParticipantType.decEq

@[implicit_reducible]

instance ArgumentStructure.instReprParticipantType : Repr ParticipantType

Equations

• ArgumentStructure.instReprParticipantType = { reprPrec := ArgumentStructure.instReprParticipantType.repr }

def ArgumentStructure.instReprParticipantType.repr : ParticipantType → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def ArgumentStructure.ParticipantType.AgentivityValid (n : ParticipantType) : Prop

The agentivity constraint: volition → sentience.

Equations

• n.AgentivityValid = n.agentivity.Valid

@[implicit_reducible]

instance ArgumentStructure.instDecidableAgentivityValid (n : ParticipantType) : Decidable n.AgentivityValid

Equations

• ArgumentStructure.instDecidableAgentivityValid n = id inferInstance

def ArgumentStructure.ParticipantType.CrossValid (n : ParticipantType) : Prop

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 = ⊥)

@[implicit_reducible]

instance ArgumentStructure.instDecidableCrossValid (n : ParticipantType) : Decidable n.CrossValid

Equations

• ArgumentStructure.instDecidableCrossValid n = id inferInstance

def ArgumentStructure.ParticipantType.Valid (n : ParticipantType) : Prop

Full validity: both constraints satisfied. Carves Grimm's 38-element Fig. 3 lattice out of the 80-element carrier.

Equations

• n.Valid = (n.AgentivityValid ∧ n.CrossValid)

@[implicit_reducible]

instance ArgumentStructure.instDecidableValid (n : ParticipantType) : Decidable n.Valid

Equations

• ArgumentStructure.instDecidableValid n = id inferInstance

def ArgumentStructure.ParticipantType.equiv : ParticipantType ≃ Agentivity × PersistenceLevel

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ArgumentStructure.instFintypeParticipantType : Fintype ParticipantType

Equations

• ArgumentStructure.instFintypeParticipantType = Fintype.ofEquiv (ArgumentStructure.Agentivity × ArgumentStructure.PersistenceLevel) ArgumentStructure.ParticipantType.equiv.symm

@[implicit_reducible]

instance ArgumentStructure.instLEParticipantType : LE ParticipantType

Product order: componentwise ≤ on agentivity and persistence.

Equations

• ArgumentStructure.instLEParticipantType = { le := fun (a b : ArgumentStructure.ParticipantType) => a.agentivity ≤ b.agentivity ∧ a.persistence ≤ b.persistence }

@[implicit_reducible]

instance ArgumentStructure.instLTParticipantType : LT ParticipantType

Equations

• ArgumentStructure.instLTParticipantType = { lt := fun (a b : ArgumentStructure.ParticipantType) => a ≤ b ∧ ¬b ≤ a }

@[implicit_reducible]

instance ArgumentStructure.instPartialOrderParticipantType : PartialOrder ParticipantType

Equations

• One or more equations did not get rendered due to their size.

@[implicit_reducible]

instance ArgumentStructure.instDecidableRelParticipantTypeLe : DecidableRel fun (x1 x2 : ParticipantType) => x1 ≤ x2

Equations

• ArgumentStructure.instDecidableRelParticipantTypeLe a b = instDecidableAnd

@[implicit_reducible]

instance ArgumentStructure.instOrderBotParticipantType : OrderBot ParticipantType

Equations

• ArgumentStructure.instOrderBotParticipantType = { bot := { agentivity := ⊥, persistence := ⊥ }, bot_le := ArgumentStructure.instOrderBotParticipantType._proof_1 }

@[implicit_reducible]

instance ArgumentStructure.instOrderTopParticipantType : OrderTop ParticipantType

Equations

• ArgumentStructure.instOrderTopParticipantType = { top := { agentivity := ⊤, persistence := ⊤ }, le_top := ArgumentStructure.instOrderTopParticipantType._proof_1 }

@[implicit_reducible]

instance ArgumentStructure.instLatticeParticipantType : Lattice ParticipantType

Componentwise lattice: meet/join on each axis independently.

Equations

• One or more equations did not get rendered due to their size.

Named participant types

def ArgumentStructure.maximalAgent : ParticipantType

Maximal Agent (Fig. 4): all agentivity features at total persistence — the top of the participant lattice. The prototypical transitive subject.

Equations

• ArgumentStructure.maximalAgent = ⊤

def ArgumentStructure.maximalPatient : ParticipantType

Maximal Patient (Fig. 4): no agentivity features, existential persistence (beginning). The prototypical affected object that ceases to exist (break, destroy).

Equations

• ArgumentStructure.maximalPatient = { agentivity := ⊥, persistence := ArgumentStructure.PersistenceLevel.exPersBeginning }

def ArgumentStructure.effectorAgent : ParticipantType

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

• ArgumentStructure.effectorAgent = { agentivity := ArgumentStructure.Agentivity.mk false false true true, persistence := ArgumentStructure.PersistenceLevel.totalPersistence }

def ArgumentStructure.sentientNonInstigator : ParticipantType

Sentience without instigation, at qualitative persistence (beginning): the single position where Grimm's §5.1 dative uses converge — recipients, dative experiencers, and second arguments of two-place communication/service verbs (Fig. 7).

Equations

• ArgumentStructure.sentientNonInstigator = { agentivity := ArgumentStructure.Agentivity.mk false true false false, persistence := ArgumentStructure.PersistenceLevel.quPersBeginning }

Transitivity region (§3, Fig. 4)

def ArgumentStructure.ParticipantType.InTransitiveRegion (n : ParticipantType) : Prop

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)

@[implicit_reducible]

instance ArgumentStructure.instDecidableInTransitiveRegion (n : ParticipantType) : Decidable n.InTransitiveRegion

Equations

• ArgumentStructure.instDecidableInTransitiveRegion n = id inferInstance

inductive ArgumentStructure.TransitivityRank : Type

Tsunoda's transitivity hierarchy (§3, example 8).

Class	Example verbs	Transitivity
I	kill, break	Highest
II	shoot, hit	Middle
III	search, seek	Lowest

Named TransitivityRank (rank on Tsunoda's hierarchy) to avoid collision with ArgumentStructure.AuxiliarySelection.TransitivityClass (the Burzio unaccusative/unergative/transitive classification).

• resultativeEffective : TransitivityRank

  Resultative Effective Action: kill, break. Object is destroyed (exPersBeginning). Maximal opposition between agent and patient.

• contact : TransitivityRank

  Contact: shoot, hit. Object is affected but persists (quPersBeginning). Less opposition than Class I.

• pursuit : TransitivityRank

  Pursuit: search, seek. Object may not even exist (totalNonPersistence). Outside the transitivity region.

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqTransitivityRank : DecidableEq TransitivityRank

Equations

• ArgumentStructure.instDecidableEqTransitivityRank x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[implicit_reducible]

instance ArgumentStructure.instReprTransitivityRank : Repr TransitivityRank

Equations

• ArgumentStructure.instReprTransitivityRank = { reprPrec := ArgumentStructure.instReprTransitivityRank.repr }

def ArgumentStructure.instReprTransitivityRank.repr : TransitivityRank → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

def ArgumentStructure.TransitivityRank.patientType : TransitivityRank → ParticipantType

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

• ArgumentStructure.TransitivityRank.resultativeEffective.patientType = { agentivity := ⊥, persistence := ArgumentStructure.PersistenceLevel.exPersBeginning }
• ArgumentStructure.TransitivityRank.contact.patientType = { agentivity := ⊥, persistence := ArgumentStructure.PersistenceLevel.quPersBeginning }
• ArgumentStructure.TransitivityRank.pursuit.patientType = { agentivity := ⊥, persistence := ArgumentStructure.PersistenceLevel.totalNonPersistence }