Argument-structure templates

[Lev93] [Dow91] [Bea10] [BKG20] [RHL98]

A RoleList pairs a subject with an optional object EntailmentProfile — the argument-structure generalization a whole verb class shares. The named templates are the class-level consensus rows (manner vs result vs creation vs psych ...); the map from [Lev93]'s class inventory onto them lives with the classes (Semantics/Verb/Class.lean), and individual verbs can override via explicit subjectEntailments/objectEntailments on Verb.

structure ArgumentStructure.RoleList : Type

A verb class's semantic role list, in realization order: the subject's entailment set, then the object's (none for intransitives). The stored order records the class's attested linking; the ASP derives it wherever dominance is strict, and it is a genuine lexical choice exactly at the alternation ties (the psych doublets) — see roleList_linking_asp_sanctioned in Semantics/Verb/Class.lean.

• subjectProfile : EntailmentProfile
• objectProfile : Option EntailmentProfile

def ArgumentStructure.instDecidableEqRoleList.decEq (x✝ x✝¹ : RoleList) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance ArgumentStructure.instDecidableEqRoleList : DecidableEq RoleList

Equations

• ArgumentStructure.instDecidableEqRoleList = ArgumentStructure.instDecidableEqRoleList.decEq

@[implicit_reducible]

instance ArgumentStructure.instReprRoleList : Repr RoleList

Equations

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

def ArgumentStructure.instReprRoleList.repr : RoleList → ℕ → Std.Format

Equations

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

def ArgumentStructure.RoleList.args (r : RoleList) : List EntailmentProfile

The role list as a list, subject first ([LRH05] ch. 2's presentation shape).

Equations

• r.args = r.subjectProfile :: r.objectProfile.toList

Named per-class argument profiles. These are the class-level consensus rows formerly hand-stored per verb in EntailmentProfile.lean; consumers (studies, fragments) reference these or the template accessors below.

def ArgumentStructure.experiencerProfile : EntailmentProfile

Experiencer argument: sentient with respect to the event, without volition or causation ([Dow91] (38): "the Experiencer is entailed to be sentient/perceiving"); independent existence per the p. 573 generalization that every verb entailing any of (27a–d) also entails subject existence.

Equations

• ArgumentStructure.experiencerProfile = { sentience := true, independentExistence := true }

def ArgumentStructure.stimulusProfile : EntailmentProfile

Stimulus argument: causes the experience without being sentient with respect to it ([Dow91] (38): "the Stimulus causes some emotional reaction or cognitive judgment in the Experiencer ... though the Stimulus is not [entailed to be sentient/perceiving]").

Equations

• ArgumentStructure.stimulusProfile = { causation := true, independentExistence := true }

def ArgumentStructure.contactObject : EntailmentProfile

Contacted-but-unaffected object of the surface-contact classes: CA+St, no CoS. [Dow91] never attributes a change of state to hit-class objects ((64 III): no Incremental Theme, no CoS for either non-subject argument); [Bea11] eq. (60c): impact verbs impose only potential for change.

Equations

• ArgumentStructure.contactObject = { causallyAffected := true, stationary := true }

def ArgumentStructure.creationObject : EntailmentProfile

Created object: CoS+IT+CA+DE — incremental theme with dependent existence ([Dow91] (30e)(i): the effected argument "does not exist before ... the event").

Equations

• ArgumentStructure.creationObject = { changeOfState := true, incrementalTheme := true, causallyAffected := true, dependentExistence := true }

def ArgumentStructure.consumptionObject : EntailmentProfile

Consumed object: CoS+IT+CA — incremental theme without DE (the object pre-exists the event). The missing DE is load-bearing for the Grimm bridge: PersistenceLevel.fromPatientProfile separates creation (DE+IT → exPersEnd) from consumption (IT alone → exPersBeginning); see Studies/Dowty1991.lean for the (30e) destruction-criterion tension.

Equations

• ArgumentStructure.consumptionObject = { changeOfState := true, incrementalTheme := true, causallyAffected := true }

def ArgumentStructure.mannerContact : RoleList

Full agent acting on a contacted but unaffected object. Subject: V+S+C+M+IE. Object: CA+St (no CoS). [Bea10]: "unspecified" affectedness — the verb's truth conditions don't entail a change of state in the object. [BKG20]: manner verbs lack result entailments.

Equations

• ArgumentStructure.mannerContact = { subjectProfile := ArgumentStructure.accomplishmentSubjectProfile, objectProfile := some ArgumentStructure.contactObject }

def ArgumentStructure.resultChange : RoleList

Full agent causing change of state in the object. Subject: V+S+C+M+IE. Object: CoS+CA (causally affected, changed). [Bea10]: "quantized" affectedness — the verb entails a definite change of state (the object reaches an end state). [BKG20]: result verbs entail CoS.

Equations

• ArgumentStructure.resultChange = { subjectProfile := ArgumentStructure.accomplishmentSubjectProfile, objectProfile := some ArgumentStructure.accomplishmentObjectProfile }

def ArgumentStructure.creation : RoleList

Full agent creating an entity (object comes into existence). Subject: V+S+C+M+IE. Object: CoS+IT+CA+DE. [Bea10]: quantized affectedness + dependent existence. The object is an incremental theme whose extent measures the event.

Equations

• ArgumentStructure.creation = { subjectProfile := ArgumentStructure.accomplishmentSubjectProfile, objectProfile := some ArgumentStructure.creationObject }

def ArgumentStructure.consumption : RoleList

Agent consuming/destroying an incremental theme (Levin 39.1 eat verbs: eat, drink; 39.4 devour verbs: devour, consume, ingest). Subject: V+S+C+M+IE. Object: CoS+IT+CA. Like creation but without dependent existence (the object pre-exists the event).

Equations

• ArgumentStructure.consumption = { subjectProfile := ArgumentStructure.accomplishmentSubjectProfile, objectProfile := some ArgumentStructure.consumptionObject }

def ArgumentStructure.selfMotion : RoleList

Self-propelled motion (no caused result, no object). Subject: V+S+M+IE (no causation — the mover doesn't cause a change in another participant).

Equations

• ArgumentStructure.selfMotion = { subjectProfile := ArgumentStructure.activitySubjectProfile }

def ArgumentStructure.perception : RoleList

Perception / experiencer-subject. Subject: S+IE (sentient, independently existing, but not volitional or causal).

Equations

• ArgumentStructure.perception = { subjectProfile := ArgumentStructure.experiencerProfile, objectProfile := some { independentExistence := true } }

def ArgumentStructure.psychCausal : RoleList

Stimulus-experiencer (Class II psych, Levin 31.1 amuse verbs; [BR88]). Subject: C+IE (causal stimulus). Object: S+IE (experiencer). Mirror image of psychState.

Equations

• ArgumentStructure.psychCausal = { subjectProfile := ArgumentStructure.stimulusProfile, objectProfile := some ArgumentStructure.experiencerProfile }

def ArgumentStructure.psychState : RoleList

Experiencer-subject psych state (Levin 31.2 admire verbs: admire, like, love, fear, envy). Subject: sentient experiencer; object: causing stimulus — [Dow91] (38): the predicate "entails that the Experiencer has some perception of the Stimulus", and the Stimulus "causes some emotional reaction or cognitive judgment in the Experiencer". Mirror image of psychCausal — the argument-selection tie behind the like/please doublets (§8.3). Distinct from desire: admire-class subjects are sentience-entailed, want-class subjects are not.

Equations

• ArgumentStructure.psychState = { subjectProfile := ArgumentStructure.experiencerProfile, objectProfile := some ArgumentStructure.stimulusProfile }

def ArgumentStructure.desire : RoleList

Desire states (Levin 32.1 want verbs: covet, crave, desire, need, want). Subject: independent existence ALONE — [Dow91] (29e) "John needs a new car", glossed p. 573 as "verbs that entail subject existence but have none of (a)–(d)": NO sentience entailment, unlike the admire class (this situation needs a solution). Object: de dicto/nonspecific, so dependent existence — (30e) "John needs a car/seeks a unicorn ... (de dicto objects: no existence)".

Equations

• ArgumentStructure.desire = { subjectProfile := { independentExistence := true }, objectProfile := some { dependentExistence := true } }

def ArgumentStructure.possessionTransfer : RoleList

Change of possession (Levin 13.1 give verbs: give, lend, pass, sell; 13.5 verbs of obtaining: buy, get, obtain). Subject: volitional agent without entailed movement (V+S+C+IE) — [Dow91] §3.2: "both buyer and seller must act agentively (voluntarily)". Buyer and seller profiles are identical; that is the §8.3 argument-selection tie behind the buy/sell doublet. No object profile: Dowty flags the goods/currency "two Themes" worry (§3.2) and attributes no object entailments.

Equations

• ArgumentStructure.possessionTransfer = { subjectProfile := { volition := true, sentience := true, causation := true, independentExistence := true } }

def ArgumentStructure.wipeManner : RoleList

Surface-contact manner (Levin 10.4.1 wipe verbs, manner subclass: wipe, scrub, sweep, rub, wash). Subject: M+IE only — underspecified for volition, so agentivity is pragmatically resolved ([RHL98] on sweep; [Dow91] never discusses sweep). Object: contacted, no entailed change ([Bea10] potential affectedness).

Equations

• ArgumentStructure.wipeManner = { subjectProfile := { movement := true, independentExistence := true }, objectProfile := some ArgumentStructure.contactObject }

def ArgumentStructure.wipeInstrument : RoleList

Instrument subclass of the wipe verbs (Levin 10.4.2: brush, comb, mop, vacuum; [RHL98]'s sweep with a broom): instrument lexicalization forces an obligatory volitional agent (V+S+C+M+IE). Not in the class map — LevinClass.roleList .wipe gives the manner subclass default; instrument-sense entries override per verb.

Equations

• ArgumentStructure.wipeInstrument = { subjectProfile := ArgumentStructure.accomplishmentSubjectProfile, objectProfile := some ArgumentStructure.contactObject }

def ArgumentStructure.unaccusativeCoS : RoleList

Unaccusative change of state (inchoative). Subject: CoS+CA (undergoes change, no agentive features). No external argument.

Equations

• ArgumentStructure.unaccusativeCoS = { subjectProfile := ArgumentStructure.accomplishmentObjectProfile }

def ArgumentStructure.directedMotion : RoleList

Directed motion (unaccusative). Subject: M+IE+CoS (moves, changes location).

Equations

• ArgumentStructure.directedMotion = { subjectProfile := ArgumentStructure.achievementSubjectProfile }

def ArgumentStructure.disappearance : RoleList

Disappearance (Levin 48.2: die, disappear, expire, perish, vanish — "describe the disappearance or going out of existence of some entity"). Sole argument: CoS+CA+DE — like unaccusativeCoS plus dependent existence, since the argument goes out of existence ([Dow91] (30e)(i): the effected argument "will not exist after the event").

Equations

• ArgumentStructure.disappearance = { subjectProfile := { changeOfState := true, causallyAffected := true, dependentExistence := true } }

theorem ArgumentStructure.mannerContact_object_no_cos : Option.map (fun (x : EntailmentProfile) => x.changeOfState) mannerContact.objectProfile = some false

Hit-class object lacks CoS (manner verbs don't entail change of state) — the Beavers & Koontz-Garboden generalization that manner roots lack result entailments, read off the class-level template.

theorem ArgumentStructure.hit_subject_role : mannerContact.subjectProfile.toRole = some ThetaRole.agent

Hit-class subject → agent label.

theorem ArgumentStructure.hit_object_role : contactObject.toRole = some ThetaRole.patient

Hit-class object → patient label (CA+St maps to patient).

theorem ArgumentStructure.selfMotion_subject_role : selfMotion.subjectProfile.toRole = some ThetaRole.agent

Self-motion subject → agent label.

theorem ArgumentStructure.perception_subject_role : perception.subjectProfile.toRole = some ThetaRole.experiencer

Perception subject → experiencer label.

theorem ArgumentStructure.psychCausal_subject_role : psychCausal.subjectProfile.toRole = some ThetaRole.stimulus

Psych-causal subject → stimulus label.

theorem ArgumentStructure.directedMotion_subject_role : directedMotion.subjectProfile.toRole = some ThetaRole.patient

Directed-motion subject → patient: the unaccusative subject of arrive undergoes a change of location (changeOfState) without agentivity. Formerly none (the moving subject was dropped); toRole now restores it.

theorem ArgumentStructure.psychState_mirrors_psychCausal : psychState.subjectProfile.toRole = some ThetaRole.experiencer ∧ psychState.objectProfile = some psychCausal.subjectProfile ∧ psychCausal.objectProfile = some psychState.subjectProfile

Admire-class subject → experiencer, and its stimulus object matches the amuse-class subject exactly — the doublet mirror ([Dow91] (38)).

theorem ArgumentStructure.disappearance_subject_role : disappearance.subjectProfile.toRole = some ThetaRole.patient

Disappearance-class subject → patient (pure Proto-Patient: die).

[Gri11]'s persistence bridge (PersistenceLevel.fromPatientProfile) evaluated on the class-level object profiles — the canonical placements consumed by Studies/Grimm2011.lean and Studies/Beavers2010.lean.

theorem ArgumentStructure.contactObject_persistence : PersistenceLevel.fromPatientProfile contactObject = PersistenceLevel.totalPersistence

Contact objects (kick, hit): no entailed change → total persistence. Follows [Bea11] eq. (60c) on surface contact; [Gri11]'s own Fig. 5 instead places contact objects at quPersBeginning.

theorem ArgumentStructure.creationObject_persistence : PersistenceLevel.fromPatientProfile creationObject = PersistenceLevel.exPersEnd

Created objects (build, invent): come into existence → exPersEnd.

theorem ArgumentStructure.consumptionObject_persistence : PersistenceLevel.fromPatientProfile consumptionObject = PersistenceLevel.exPersBeginning

Consumed objects (eat, devour): cease to exist → exPersBeginning.

theorem ArgumentStructure.disappearance_subject_persistence : PersistenceLevel.fromPatientProfile disappearance.subjectProfile = PersistenceLevel.exPersBeginning

Disappearance-class subjects (die, vanish), read as patients: cease to exist → exPersBeginning.