Theta roles as proto-role clusters

Dowty replaces the traditional list of thematic roles by two cluster concepts, the Proto-Agent and Proto-Patient entailments, and reads the familiar role types off combinations of them: an agent is volitional, sentient, causing, and moving; an experiencer is sentient without volition or causation; an instrument causes and moves without volition or sentience; a theme changes, measures out the event, and depends on it, and a patient is the causally affected theme; a source or goal has no defining entailment at all. The recipient of a transfer, for which Primus proposes a Recipient Proto-role of its own, has none here either. This file carries those labels, the profile each names, and the classifier that reads a label off a profile, so that a label is a derived classification of an argument's entailment profile and never a stored primitive.

Main declarations

• ArgumentStructure.ThetaRole: the nine traditional labels.
• ThetaRole.canonicalProfile: the entailments a label combines, none for source, goal and recipient; ThetaRole.IsDefined says a label has defining entailments.
• EntailmentProfile.toRole: the label of a profile, with toRole_eq_some_agent_iff and its siblings characterizing each label and toRole_canonicalProfile recovering a defined label from its profile.

Implementation notes

The classifier tests the Proto-Agent entailments first, volition before sentience before causation, and among the Proto-Patient entailments causal affectedness before the rest, so a profile with both sentience and causation but no volition, which Dowty's definitions do not name, has no label. Independent existence, which Dowty parenthesizes, never decides a label. Dowty's role hierarchies follow from the selection principle over these profiles in Studies/Dowty1991.lean.

References

• [Dow91]
• [LRH05]
• [Pri99]

inductive ArgumentStructure.ThetaRole : Type

The traditional thematic-role labels, read as clusters of proto-role entailments.

• agent : ThetaRole
• patient : ThetaRole
• theme : ThetaRole
• experiencer : ThetaRole
• goal : ThetaRole
• source : ThetaRole
• instrument : ThetaRole
• stimulus : ThetaRole
• recipient : ThetaRole

  The recipient of a transfer, for which [Pri99] introduces a Recipient Proto-role ([LRH05], p. 60).

@[instance_reducible]

instance ArgumentStructure.instDecidableEqThetaRole : DecidableEq ThetaRole

Equations

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

def ArgumentStructure.instReprThetaRole.repr : ThetaRole → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance ArgumentStructure.instReprThetaRole : Repr ThetaRole

Equations

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

@[instance_reducible]

instance ArgumentStructure.instFintypeThetaRole : Fintype ThetaRole

Equations

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

def ArgumentStructure.ThetaRole.canonicalProfile : ThetaRole → EntailmentProfile

canonicalProfile r is the set of entailments the label r combines in Dowty's reading of the traditional roles, the agent all four core Proto-Agent entailments, the experiencer sentience, the stimulus causation, the instrument causation and movement, the theme change with incremental theme and dependent existence, the patient the causally affected theme, and the source, goal and recipient nothing.

Equations

• One or more equations did not get rendered due to their size.
• ArgumentStructure.ThetaRole.experiencer.canonicalProfile = {ArgumentStructure.ProtoRoleFeature.sentience}
• ArgumentStructure.ThetaRole.stimulus.canonicalProfile = {ArgumentStructure.ProtoRoleFeature.causation}
• ArgumentStructure.ThetaRole.instrument.canonicalProfile = {ArgumentStructure.ProtoRoleFeature.causation, ArgumentStructure.ProtoRoleFeature.movement}
• ArgumentStructure.ThetaRole.goal.canonicalProfile = ∅
• ArgumentStructure.ThetaRole.source.canonicalProfile = ∅
• ArgumentStructure.ThetaRole.recipient.canonicalProfile = ∅

def ArgumentStructure.ThetaRole.IsDefined (r : ThetaRole) : Prop

A label is defined by proto-role entailments; source, goal and recipient are not.

Equations

• r.IsDefined = (r ≠ ArgumentStructure.ThetaRole.source ∧ r ≠ ArgumentStructure.ThetaRole.goal ∧ r ≠ ArgumentStructure.ThetaRole.recipient)

@[instance_reducible]

instance ArgumentStructure.ThetaRole.instDecidablePredIsDefined : DecidablePred IsDefined

Equations

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

@[simp]

theorem ArgumentStructure.ThetaRole.canonicalProfile_source : source.canonicalProfile = ∅

@[simp]

theorem ArgumentStructure.ThetaRole.canonicalProfile_goal : goal.canonicalProfile = ∅

@[simp]

theorem ArgumentStructure.ThetaRole.canonicalProfile_recipient : recipient.canonicalProfile = ∅

theorem ArgumentStructure.ThetaRole.isDefined_iff_canonicalProfile_nonempty (r : ThetaRole) : r.IsDefined ↔ Finset.Nonempty r.canonicalProfile

A label has defining entailments iff its profile is not empty.

theorem ArgumentStructure.ThetaRole.canonicalProfile_theme_le_patient : theme.canonicalProfile ⊆ patient.canonicalProfile

A patient is a theme that is causally affected.

theorem ArgumentStructure.ThetaRole.wellFormedInternal_canonicalProfile (r : ThetaRole) : WellFormedInternal r.canonicalProfile

Every canonical profile satisfies Dowty's internal constraint that volition entails sentience.

def ArgumentStructure.EntailmentProfile.toRole (p : EntailmentProfile) : Option ThetaRole

p.toRole is the label of the profile p, agent if volitional, else experiencer if sentient and not causing, else instrument or stimulus if causing according to movement, else patient if causally affected, else theme if changing, measuring out the event, depending on it, or moving, and otherwise none.

Equations

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

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_agent_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.agent ↔ ProtoRoleFeature.volition ∈ p

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_experiencer_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.experiencer ↔ ProtoRoleFeature.volition ∉ p ∧ ProtoRoleFeature.sentience ∈ p ∧ ProtoRoleFeature.causation ∉ p

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_instrument_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.instrument ↔ ProtoRoleFeature.volition ∉ p ∧ ProtoRoleFeature.sentience ∉ p ∧ ProtoRoleFeature.causation ∈ p ∧ ProtoRoleFeature.movement ∈ p

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_stimulus_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.stimulus ↔ ProtoRoleFeature.volition ∉ p ∧ ProtoRoleFeature.sentience ∉ p ∧ ProtoRoleFeature.causation ∈ p ∧ ProtoRoleFeature.movement ∉ p

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_patient_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.patient ↔ ProtoRoleFeature.volition ∉ p ∧ ProtoRoleFeature.sentience ∉ p ∧ ProtoRoleFeature.causation ∉ p ∧ ProtoRoleFeature.causallyAffected ∈ p

theorem ArgumentStructure.EntailmentProfile.toRole_eq_some_theme_iff {p : EntailmentProfile} : p.toRole = some ThetaRole.theme ↔ ProtoRoleFeature.volition ∉ p ∧ ProtoRoleFeature.sentience ∉ p ∧ ProtoRoleFeature.causation ∉ p ∧ ProtoRoleFeature.causallyAffected ∉ p ∧ (ProtoRoleFeature.changeOfState ∈ p ∨ ProtoRoleFeature.incrementalTheme ∈ p ∨ ProtoRoleFeature.dependentExistence ∈ p ∨ ProtoRoleFeature.movement ∈ p)

theorem ArgumentStructure.EntailmentProfile.toRole_ne_some_source {p : EntailmentProfile} : p.toRole ≠ some ThetaRole.source

Source, goal and recipient are never read off a profile: they are not defined by entailments.

theorem ArgumentStructure.EntailmentProfile.toRole_ne_some_goal {p : EntailmentProfile} : p.toRole ≠ some ThetaRole.goal

theorem ArgumentStructure.EntailmentProfile.toRole_ne_some_recipient {p : EntailmentProfile} : p.toRole ≠ some ThetaRole.recipient

theorem ArgumentStructure.EntailmentProfile.isDefined_of_toRole_eq_some {p : EntailmentProfile} {r : ThetaRole} (h : p.toRole = some r) : r.IsDefined

A label read off a profile is a defined one.

theorem ArgumentStructure.EntailmentProfile.causation_mem_of_toRole_eq_some_stimulus {p : EntailmentProfile} (h : p.toRole = some ThetaRole.stimulus) : ProtoRoleFeature.causation ∈ p

theorem ArgumentStructure.ThetaRole.toRole_canonicalProfile {r : ThetaRole} (h : r.IsDefined) : r.canonicalProfile.toRole = some r

The classifier recovers every defined label from its canonical profile.

theorem ArgumentStructure.ThetaRole.canonicalProfile_injOn : Set.InjOn canonicalProfile {r : ThetaRole | r.IsDefined}

Distinct defined labels have distinct canonical profiles.