Levin Class → Entailment Profile Mapping #

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

Maps [Lev93] verb classes to proto-role entailment profiles ([Dow91]), encoding the argument-structure generalizations that hold at the class level.

The mapping is organized by argument structure template: groups of Levin classes that share the same subject/object entailment profile. This reflects the field consensus ([BKG20]) that root meaning determines which entailments hold:

Manner verbs (hit, touch): agent subject, contacted object (no CoS)
Result verbs (break, destroy): agent subject, affected object (CoS)
Creation verbs (build, create): agent subject, created object (CoS+DE)
Motion verbs (run, walk): agent subject (no causation), no object
Perception verbs (see, hear): experiencer subject
Psych-causal verbs (amuse): stimulus subject

Individual verbs can override class-level profiles via explicit subjectEntailments/objectEntailments on Verb.

source

structure Features.LevinClassProfiles.ArgTemplate :

Type

Subject + object entailment profile pair for a verb class. objectProfile = none for intransitive classes.

subjectProfile : ArgumentStructure.EntailmentProfile
objectProfile : Option ArgumentStructure.EntailmentProfile

Instances For

source

@[implicit_reducible]

instance Features.LevinClassProfiles.instDecidableEqArgTemplate :

DecidableEq ArgTemplate

Equations

Features.LevinClassProfiles.instDecidableEqArgTemplate = Features.LevinClassProfiles.instDecidableEqArgTemplate.decEq

source

def Features.LevinClassProfiles.instDecidableEqArgTemplate.decEq (x✝ x✝¹ : ArgTemplate) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

source

@[implicit_reducible]

instance Features.LevinClassProfiles.instReprArgTemplate :

Repr ArgTemplate

Equations

Features.LevinClassProfiles.instReprArgTemplate = { reprPrec := Features.LevinClassProfiles.instReprArgTemplate.repr }

source

def Features.LevinClassProfiles.instReprArgTemplate.repr :

ArgTemplate → ℕ → Std.Format

Equations

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

Instances For

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

source

def Features.LevinClassProfiles.experiencerProfile :

ArgumentStructure.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

Features.LevinClassProfiles.experiencerProfile = { sentience := true, independentExistence := true }

Instances For

source

def Features.LevinClassProfiles.stimulusProfile :

ArgumentStructure.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

Features.LevinClassProfiles.stimulusProfile = { causation := true, independentExistence := true }

Instances For

source

def Features.LevinClassProfiles.contactObject :

ArgumentStructure.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

Features.LevinClassProfiles.contactObject = { causallyAffected := true, stationary := true }

Instances For

source

def Features.LevinClassProfiles.creationObject :

ArgumentStructure.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

Features.LevinClassProfiles.creationObject = { changeOfState := true, incrementalTheme := true, causallyAffected := true, dependentExistence := true }

Instances For

source

def Features.LevinClassProfiles.consumptionObject :

ArgumentStructure.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

Features.LevinClassProfiles.consumptionObject = { changeOfState := true, incrementalTheme := true, causallyAffected := true }

Instances For

source

def Features.LevinClassProfiles.mannerContact :

ArgTemplate

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

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

Instances For

source

def Features.LevinClassProfiles.resultChange :

ArgTemplate

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

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

Instances For

source

def Features.LevinClassProfiles.creation :

ArgTemplate

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

Features.LevinClassProfiles.creation = { subjectProfile := ArgumentStructure.EntailmentProfile.accomplishmentSubjectProfile, objectProfile := some Features.LevinClassProfiles.creationObject }

Instances For

source

def Features.LevinClassProfiles.consumption :

ArgTemplate

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

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

Instances For

source

def Features.LevinClassProfiles.selfMotion :

ArgTemplate

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

Features.LevinClassProfiles.selfMotion = { subjectProfile := ArgumentStructure.EntailmentProfile.activitySubjectProfile }

Instances For

source

def Features.LevinClassProfiles.perception :

ArgTemplate

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

Equations

Features.LevinClassProfiles.perception = { subjectProfile := Features.LevinClassProfiles.experiencerProfile, objectProfile := some { independentExistence := true } }

Instances For

source

def Features.LevinClassProfiles.psychCausal :

ArgTemplate

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

Features.LevinClassProfiles.psychCausal = { subjectProfile := Features.LevinClassProfiles.stimulusProfile, objectProfile := some Features.LevinClassProfiles.experiencerProfile }

Instances For

source

def Features.LevinClassProfiles.psychState :

ArgTemplate

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

Features.LevinClassProfiles.psychState = { subjectProfile := Features.LevinClassProfiles.experiencerProfile, objectProfile := some Features.LevinClassProfiles.stimulusProfile }

Instances For

source

def Features.LevinClassProfiles.desire :

ArgTemplate

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

Features.LevinClassProfiles.desire = { subjectProfile := { independentExistence := true }, objectProfile := some { dependentExistence := true } }

Instances For

source

def Features.LevinClassProfiles.possessionTransfer :

ArgTemplate

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

Features.LevinClassProfiles.possessionTransfer = { subjectProfile := { volition := true, sentience := true, causation := true, independentExistence := true } }

Instances For

source

def Features.LevinClassProfiles.wipeManner :

ArgTemplate

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

Features.LevinClassProfiles.wipeManner = { subjectProfile := { movement := true, independentExistence := true }, objectProfile := some Features.LevinClassProfiles.contactObject }

Instances For

source

def Features.LevinClassProfiles.wipeInstrument :

ArgTemplate

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.argTemplate .wipe gives the manner subclass default; instrument-sense entries override per verb.

Equations

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

Instances For

source

def Features.LevinClassProfiles.unaccusativeCoS :

ArgTemplate

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

Equations

Features.LevinClassProfiles.unaccusativeCoS = { subjectProfile := ArgumentStructure.EntailmentProfile.accomplishmentObjectProfile }

Instances For

source

def Features.LevinClassProfiles.directedMotion :

ArgTemplate

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

Equations

Features.LevinClassProfiles.directedMotion = { subjectProfile := ArgumentStructure.EntailmentProfile.achievementSubjectProfile }

Instances For

source

def Features.LevinClassProfiles.disappearance :

ArgTemplate

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

Features.LevinClassProfiles.disappearance = { subjectProfile := { changeOfState := true, causallyAffected := true, dependentExistence := true } }

Instances For

source

def Semantics.Lexical.LevinClass.argTemplate :

LevinClass → Option Features.LevinClassProfiles.ArgTemplate

Map a Levin class to its argument structure template. Returns none for classes whose profiles haven't been determined yet.

Equations

Instances For

source

def Semantics.Lexical.LevinClass.subjectProfile (c : LevinClass) :

Option ArgumentStructure.EntailmentProfile

Subject entailment profile for a Levin class.

Equations

c.subjectProfile = Option.map (fun (x : Features.LevinClassProfiles.ArgTemplate) => x.subjectProfile) c.argTemplate

Instances For

source

def Semantics.Lexical.LevinClass.objectProfile (c : LevinClass) :

Option ArgumentStructure.EntailmentProfile

Object entailment profile for a Levin class.

Equations

c.objectProfile = c.argTemplate.bind fun (x : Features.LevinClassProfiles.ArgTemplate) => x.objectProfile

Instances For

source

theorem Features.LevinClassProfiles.mannerContact_object_no_cos :

Option.map (fun (x : ArgumentStructure.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.

source

theorem Features.LevinClassProfiles.hit_subject_role :

mannerContact.subjectProfile.toRole = some ThetaRole.agent

Hit-class subject → agent label.

source

theorem Features.LevinClassProfiles.hit_object_role :

contactObject.toRole = some ThetaRole.patient

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

source

theorem Features.LevinClassProfiles.selfMotion_subject_role :

selfMotion.subjectProfile.toRole = some ThetaRole.agent

Self-motion subject → agent label.

source

theorem Features.LevinClassProfiles.perception_subject_role :

perception.subjectProfile.toRole = some ThetaRole.experiencer

Perception subject → experiencer label.

source

theorem Features.LevinClassProfiles.psychCausal_subject_role :

psychCausal.subjectProfile.toRole = some ThetaRole.stimulus

Psych-causal subject → stimulus label.

source

theorem Features.LevinClassProfiles.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.

source

theorem Features.LevinClassProfiles.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)).

source

theorem Features.LevinClassProfiles.disappearance_subject_role :

disappearance.subjectProfile.toRole = some ThetaRole.patient

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

Root kind signatures determine argument templates — the derivational direction in the argument-realization tradition ([BKG20] roots, [RHL98] event-template linking). The chain runs:

Root.Kinds → Template → ArgTemplate → ThetaRole labels

toArgTemplate formalizes the default derivation. It captures the majority pattern: causative roots produce agent subjects and affected objects; manner-only roots produce agent subjects without causation; result-only roots produce unaccusative subjects; state-only roots produce experiencer subjects.

Two classes of systematic overrides exist:

Psych-causal verbs (amuse): causativeResult roots where the subject is a non-volitional stimulus, not a volitional agent. Override: psychCausal template.
Creation verbs (build): causativeResult roots where the object has dependent existence and incremental theme structure. Override: creation template.

These overrides are documented and verified below.

source

def Features.LevinClassProfiles.toArgTemplate (re : Verb.Root.Kinds) :

Option ArgTemplate

Derive a default ArgTemplate from a root kind signature.

The derivation follows B&KG's event structure decomposition:

cause: subject is external causer → full agent (V+S+C+M+IE), object undergoes change → CoS+CA
result without cause: internally caused change → unaccusative, sole argument is patient (CoS+CA)
manner without cause/result: activity → agent without causation (V+S+M+IE), no affected object
state only: stative → experiencer subject (S+IE)
no entailments: no default derivation

For cause+manner (fullSpec) vs cause without manner (causativeResult): both produce the same default ArgTemplate. The manner flag restricts HOW the cause proceeds (cutting vs. breaking), not WHETHER there's an agent.

Equations

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

Instances For

For each LevinClass with both rootEntailments and argTemplate defined, we verify that the derived ArgTemplate either MATCHES the hand-specified one or is a documented override.

source

theorem Features.LevinClassProfiles.argTemplate_diverges_from_derivation :

∃ (c : Semantics.Lexical.LevinClass), c.argTemplate ≠ toArgTemplate c.rootEntailments

argTemplate is not merely toArgTemplate ∘ rootEntailments: it diverges for the documented overrides (creation, psych-causal). Build witnesses this — its causativeResult root derives resultChange, but the class template is creation (incremental-theme object). A table that always matched the derivation would be redundant with it; this divergence is why argTemplate exists as a separate label, and §8b documents the overrides.

source

theorem Features.LevinClassProfiles.build_override_creation :

toArgTemplate Semantics.Lexical.LevinClass.build.rootEntailments = some resultChange ∧ Semantics.Lexical.LevinClass.build.argTemplate = some creation

Build-class: causativeResult derives resultChange, but build verbs have a CREATION object (CoS+IT+CA+DE) — the object comes into existence. Dependent existence and incremental theme are additional entailments not captured by root structural features.

source

theorem Features.LevinClassProfiles.amuse_override_psychCausal :

toArgTemplate Semantics.Lexical.LevinClass.amuse.rootEntailments = some resultChange ∧ Semantics.Lexical.LevinClass.amuse.argTemplate = some psychCausal

Amuse-class: causativeResult derives resultChange (agent subject), but psych-causal verbs have a STIMULUS subject (C+IE, no volition) and EXPERIENCER object (S+IE). The nature of causation (volitional vs. stimulus) isn't encoded in root entailments.

source

theorem Features.LevinClassProfiles.eat_has_class_template :

Semantics.Lexical.LevinClass.eat.argTemplate = some consumption

Eat/devour: default from rootEntailments is not defined (minimal), but class-level argTemplate specifies consumption.

source

theorem Features.LevinClassProfiles.class_templates_override_derivation :

The remaining documented overrides, in one place. Root kind signatures are too coarse for these classes: manner roots don't distinguish the wipe class's underspecified-volition subject from full-agent self-motion; state roots don't distinguish sentience-entailed psych states (admire) from bare desire states (want); and result roots don't see the disappearance class's dependent existence.

source

theorem Features.LevinClassProfiles.build_subject_agrees :

resultChange.subjectProfile = creation.subjectProfile

Build-class subject matches the derivation's subject (both are full agent V+S+C+M+IE). The override affects only the object, not the subject.

source

theorem Features.LevinClassProfiles.derived_subjects_wellformed :

((toArgTemplate Verb.Root.Kinds.causativeResult).elim False fun (x : ArgTemplate) => x.subjectProfile.WellFormedInternal) ∧ ((toArgTemplate Verb.Root.Kinds.pureManner).elim False fun (x : ArgTemplate) => x.subjectProfile.WellFormedInternal) ∧ ((toArgTemplate Verb.Root.Kinds.pureResult).elim False fun (x : ArgTemplate) => x.subjectProfile.WellFormedInternal) ∧ (toArgTemplate Verb.Root.Kinds.propertyConcept).elim False fun (x : ArgTemplate) => x.subjectProfile.WellFormedInternal

All canonical root signatures derive well-formed internal constraints (volition → sentience holds for derived subject profiles). The Option.elim False form simultaneously checks that toArgTemplate succeeds on each input and that the resulting template's subject profile is well-formed.

Documentation

Linglib.Semantics.Lexical.LevinClassProfiles

Levin Class → Entailment Profile Mapping #