Documentation

Linglib.Theories.Semantics.Lexical.Verb.LevinClassProfiles

Levin Class → Entailment Profile Mapping #

@cite{levin-1993} @cite{dowty-1991} @cite{beavers-2010} @cite{beavers-koontz-garboden-2020} @cite{rappaport-hovav-levin-2024}

Maps @cite{levin-1993} verb classes to proto-role entailment profiles (@cite{dowty-1991}), 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 (@cite{beavers-koontz-garboden-2020}) 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 VerbCore.

structure Semantics.Lexical.Verb.LevinClassProfiles.ArgTemplate :

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

subjectProfile : EntailmentProfile.EntailmentProfile
objectProfile : Option EntailmentProfile.EntailmentProfile

Instances For

instance Semantics.Lexical.Verb.LevinClassProfiles.instDecidableEqArgTemplate :

DecidableEq ArgTemplate

Equations

Semantics.Lexical.Verb.LevinClassProfiles.instDecidableEqArgTemplate = Semantics.Lexical.Verb.LevinClassProfiles.instDecidableEqArgTemplate.decEq

def Semantics.Lexical.Verb.LevinClassProfiles.instDecidableEqArgTemplate.decEq (x✝ x✝¹ : ArgTemplate) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.instReprArgTemplate.repr :

ArgTemplate → Nat → Std.Format

Equations

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

Instances For

instance Semantics.Lexical.Verb.LevinClassProfiles.instReprArgTemplate :

Repr ArgTemplate

Equations

Semantics.Lexical.Verb.LevinClassProfiles.instReprArgTemplate = { reprPrec := Semantics.Lexical.Verb.LevinClassProfiles.instReprArgTemplate.repr }

instance Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate :

BEq ArgTemplate

Equations

Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate = { beq := Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate.beq }

def Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate.beq :

ArgTemplate → ArgTemplate → Bool

Equations

Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate.beq { subjectProfile := a, objectProfile := a_1 } { subjectProfile := b, objectProfile := b_1 } = (a == b && a_1 == b_1)
Semantics.Lexical.Verb.LevinClassProfiles.instBEqArgTemplate.beq x✝¹ x✝ = false

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.mannerContact :

Full agent acting on a contacted but unaffected object. Subject: V+S+C+M+IE. Object: CA+St (no CoS). @cite{beavers-2010}: "unspecified" affectedness — the verb's truth conditions don't entail a change of state in the object. @cite{beavers-koontz-garboden-2020}: manner verbs lack result entailments.

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.resultChange :

Full agent causing change of state in the object. Subject: V+S+C+M+IE. Object: CoS+CA (causally affected, changed). @cite{beavers-2010}: "quantized" affectedness — the verb entails a definite change of state (the object reaches an end state). @cite{beavers-koontz-garboden-2020}: result verbs entail CoS.

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.creation :

Full agent creating an entity (object comes into existence). Subject: V+S+C+M+IE. Object: CoS+IT+CA+DE. @cite{beavers-2010}: quantized affectedness + dependent existence. The object is an incremental theme whose extent measures the event.

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.consumption :

Agent consuming/destroying an incremental theme. 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

def Semantics.Lexical.Verb.LevinClassProfiles.selfMotion :

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

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.perception :

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

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.psychCausal :

Stimulus-experiencer (Class II psych, @cite{belletti-rizzi-1988}). Subject: C+IE (causal stimulus). Object: S+IE (experiencer).

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.unaccusativeCoS :

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

Equations

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

Instances For

def Semantics.Lexical.Verb.LevinClassProfiles.directedMotion :

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

Equations

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

Instances For

def LevinClass.argTemplate :

LevinClass → Option Semantics.Lexical.Verb.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

def LevinClass.subjectProfile (c : LevinClass) :

Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

Subject entailment profile for a Levin class.

Equations

c.subjectProfile = Option.map (fun (x : Semantics.Lexical.Verb.LevinClassProfiles.ArgTemplate) => x.subjectProfile) c.argTemplate

Instances For

def LevinClass.objectProfile (c : LevinClass) :

Option Semantics.Lexical.Verb.EntailmentProfile.EntailmentProfile

Object entailment profile for a Levin class.

Equations

c.objectProfile = c.argTemplate.bind fun (x : Semantics.Lexical.Verb.LevinClassProfiles.ArgTemplate) => x.objectProfile

Instances For

theorem Semantics.Lexical.Verb.LevinClassProfiles.hit_subject_eq_kick :

mannerContact.subjectProfile = EntailmentProfile.kickSubjectProfile

Hit-class subject = kickSubjectProfile (both full agent).

theorem Semantics.Lexical.Verb.LevinClassProfiles.mannerContact_object_no_cos :

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

Hit-class object lacks CoS (manner verbs don't entail change of state). This correctly differs from kickObjectProfile (which has CoS=true) — the class-level profile captures the Beavers & Koontz-Garboden generalization that manner roots lack result entailments.

theorem Semantics.Lexical.Verb.LevinClassProfiles.creation_object_eq_build :

creation.objectProfile = some EntailmentProfile.buildObjectProfile

Creation-class object = buildObjectProfile.

theorem Semantics.Lexical.Verb.LevinClassProfiles.consumption_object_eq_eat :

consumption.objectProfile = some EntailmentProfile.eatObjectProfile

Consumption-class object = eatObjectProfile.

theorem Semantics.Lexical.Verb.LevinClassProfiles.selfMotion_subject_eq_run :

selfMotion.subjectProfile = EntailmentProfile.runSubjectProfile

Self-motion subject = runSubjectProfile.

theorem Semantics.Lexical.Verb.LevinClassProfiles.directedMotion_subject_eq_arrive :

directedMotion.subjectProfile = EntailmentProfile.arriveSubjectProfile

Directed-motion subject = arriveSubjectProfile.

theorem Semantics.Lexical.Verb.LevinClassProfiles.perception_subject_eq_see :

perception.subjectProfile = EntailmentProfile.seeSubjectProfile

Perception subject = seeSubjectProfile.

theorem Semantics.Lexical.Verb.LevinClassProfiles.hit_subject_role :

mannerContact.subjectProfile.toRole = some ThetaRole.agent

Hit-class subject → agent label.

theorem Semantics.Lexical.Verb.LevinClassProfiles.hit_object_role :

EntailmentProfile.kickObjectProfile.toRole = some ThetaRole.patient

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

theorem Semantics.Lexical.Verb.LevinClassProfiles.selfMotion_subject_role :

selfMotion.subjectProfile.toRole = some ThetaRole.agent

Self-motion subject → agent label.

theorem Semantics.Lexical.Verb.LevinClassProfiles.perception_subject_role :

perception.subjectProfile.toRole = some ThetaRole.experiencer

Perception subject → experiencer label.

theorem Semantics.Lexical.Verb.LevinClassProfiles.psychCausal_subject_role :

psychCausal.subjectProfile.toRole = some ThetaRole.stimulus

Psych-causal subject → stimulus label.

theorem Semantics.Lexical.Verb.LevinClassProfiles.directedMotion_subject_role :

directedMotion.subjectProfile.toRole = none

Directed-motion subject → none (mixed P-Agent + P-Patient).

Root entailments determine argument templates — this is the field consensus (@cite{beavers-koontz-garboden-2020}, @cite{rappaport-hovav-levin-2024}). The derivational direction runs:

RootEntailments → Template → ArgTemplate → ThetaRole labels

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

def Semantics.Lexical.Verb.LevinClassProfiles.toArgTemplate (re : RootEntailments) :

Option ArgTemplate

Derive a default ArgTemplate from root structural entailments.

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.

theorem Semantics.Lexical.Verb.LevinClassProfiles.break_derived_matches :

toArgTemplate LevinClass.break_.rootEntailments = LevinClass.break_.argTemplate

Break-class: causativeResult → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.bend_derived_matches :

toArgTemplate LevinClass.bend.rootEntailments = LevinClass.bend.argTemplate

Bend-class: causativeResult → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.destroy_derived_matches :

toArgTemplate LevinClass.destroy.rootEntailments = LevinClass.destroy.argTemplate

Destroy-class: causativeResult → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.murder_derived_matches :

toArgTemplate LevinClass.murder.rootEntailments = LevinClass.murder.argTemplate

Murder-class: causativeResult → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.cooking_derived_matches :

toArgTemplate LevinClass.cooking.rootEntailments = LevinClass.cooking.argTemplate

Cooking-class: causativeResult → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.cut_derived_matches :

toArgTemplate LevinClass.cut.rootEntailments = LevinClass.cut.argTemplate

Cut-class: fullSpec → resultChange ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.mannerOfMotion_derived_matches :

toArgTemplate LevinClass.mannerOfMotion.rootEntailments = LevinClass.mannerOfMotion.argTemplate

MannerOfMotion-class: pureManner → selfMotion ✓

theorem Semantics.Lexical.Verb.LevinClassProfiles.build_override_creation :

toArgTemplate LevinClass.build.rootEntailments = some resultChange ∧ 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.

theorem Semantics.Lexical.Verb.LevinClassProfiles.amuse_override_psychCausal :

toArgTemplate LevinClass.amuse.rootEntailments = some resultChange ∧ 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.

theorem Semantics.Lexical.Verb.LevinClassProfiles.eat_has_class_template :

LevinClass.eat.argTemplate = some consumption

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

theorem Semantics.Lexical.Verb.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.

theorem Semantics.Lexical.Verb.LevinClassProfiles.derived_subjects_wellformed :

Option.map (fun (x : ArgTemplate) => x.subjectProfile.wellFormedInternal) (toArgTemplate RootEntailments.causativeResult) = some true ∧ Option.map (fun (x : ArgTemplate) => x.subjectProfile.wellFormedInternal) (toArgTemplate RootEntailments.pureManner) = some true ∧ Option.map (fun (x : ArgTemplate) => x.subjectProfile.wellFormedInternal) (toArgTemplate RootEntailments.pureResult) = some true ∧ Option.map (fun (x : ArgTemplate) => x.subjectProfile.wellFormedInternal) (toArgTemplate RootEntailments.propertyConcept) = some true

All canonical root entailments derive well-formed internal constraints (volition → sentience holds for derived subject profiles).