Documentation

Linglib.Core.Lexical.LevinClass

Levin Verb Classes and Meaning Components #

@cite{levin-1993} @cite{dowty-1991} @cite{beavers-koontz-garboden-2020}

§ 1. Meaning components #

Binary features that define @cite{levin-1993} verb classes, diagnosed by diathesis alternation behavior: change of state, contact, motion, causation, instrument specification, manner specification.

§ 2. Verb class taxonomy #

The full verb class taxonomy from @cite{levin-1993} Part II: 49 top-level classes covering the English verb lexicon. Individual verb entries in Fragments/ are tagged with their Levin class.

§ 3. Per-class meaning component profiles #

§ 4. Predicted unaccusativity #

Based on @cite{levin-hovav-1995}: unaccusativity correlates with internally caused change of state or directed change.

§ 5. Root entailment mapping (@cite{beavers-koontz-garboden-2020}) #

Root structural entailments, well-formedness verification, and MRC tests.

§ 6. Root–MC bridge #

Classification enums (CausationSource, ResultKind, MannerKind) naming the systematic divergences between B&KG root features and Levin meaning components, plus universal consistency theorems.

structure MeaningComponents :

Binary meaning components that define @cite{levin-1993} verb classes.

These describe surface verb behavior, not root-level entailments. @cite{beavers-koontz-garboden-2020} argue that surface CoS and causation can come from either the template or the root; see RootEntailments (§ 3b) for the root-level decomposition.

Diagnosed by participation in diathesis alternations (pp. 5–10):

changeOfState: middle alternation, causative/inchoative alternation
contact: body-part possessor ascension alternation
motion: conative alternation (with contact)
causation: causative/inchoative alternation (with changeOfState)

The four canonical classes from Levin's Introduction:

break = [+CoS, −contact, −motion, +causation]
cut = [+CoS, +contact, +motion, +causation]
hit = [−CoS, +contact, +motion, −causation]
touch = [−CoS, +contact, −motion, −causation]

Additional binary features (from class descriptions in Part II):

instrumentSpec: verb specifies instrument/means (cut vs. break; p. 157)
mannerSpec: verb specifies manner of action (cooking subclasses; p. 244)

changeOfState : Bool
Does the verb denote causing a change of state? Diagnostic: participation in the middle alternation (p. 5).
contact : Bool
Does the verb's meaning inherently involve contact? Diagnostic: body-part possessor ascension (p. 7).
motion : Bool
Does the verb's meaning inherently involve motion? Diagnostic: conative alternation requires both motion and contact (p. 8).
causation : Bool
Does the verb's meaning include a notion of causation? Diagnostic: participation in causative/inchoative alternation (p. 9).
instrumentSpec : Bool
Does the verb specify the instrument or means? Cut includes instrument specification; break does not (p. 157).
mannerSpec : Bool
Does the verb specify the manner of action? Cooking verbs "describe different ways of cooking food" (p. 244).

Instances For

instance instDecidableEqMeaningComponents :

DecidableEq MeaningComponents

Equations

instDecidableEqMeaningComponents = instDecidableEqMeaningComponents.decEq

def instDecidableEqMeaningComponents.decEq (x✝ x✝¹ : MeaningComponents) :

Decidable (x✝ = x✝¹)

Equations

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

Instances For

instance instBEqMeaningComponents :

BEq MeaningComponents

Equations

instBEqMeaningComponents = { beq := instBEqMeaningComponents.beq }

def instBEqMeaningComponents.beq :

MeaningComponents → MeaningComponents → Bool

Equations

One or more equations did not get rendered due to their size.
instBEqMeaningComponents.beq x✝¹ x✝ = false

Instances For

instance instReprMeaningComponents :

Repr MeaningComponents

Equations

instReprMeaningComponents = { reprPrec := instReprMeaningComponents.repr }

def instReprMeaningComponents.repr :

MeaningComponents → Nat → Std.Format

Equations

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

Instances For

def MeaningComponents.break_ :

MeaningComponents

break verbs (45.1): pure change of state, no manner/instrument.

Equations

MeaningComponents.break_ = { changeOfState := true, contact := false, motion := false, causation := true }

Instances For

def MeaningComponents.cut :

MeaningComponents

cut verbs (21.1): change of state via contact through motion.

Equations

MeaningComponents.cut = { changeOfState := true, contact := true, motion := true, causation := true, instrumentSpec := true }

Instances For

def MeaningComponents.hit :

MeaningComponents

hit verbs (18.1): contact by impact, no change of state.

Equations

MeaningComponents.hit = { changeOfState := false, contact := true, motion := true, causation := false }

Instances For

def MeaningComponents.touch :

MeaningComponents

touch verbs (20): pure contact, no motion or change of state.

Equations

MeaningComponents.touch = { changeOfState := false, contact := true, motion := false, causation := false }

Instances For

def MeaningComponents.destroy :

MeaningComponents

destroy verbs (44): total destruction, no specific physical result.

Equations

MeaningComponents.destroy = { changeOfState := true, contact := false, motion := false, causation := true }

Instances For

def MeaningComponents.bend :

MeaningComponents

bend verbs (45.2): shape change without disruption of integrity.

Equations

MeaningComponents.bend = { changeOfState := true, contact := false, motion := false, causation := true }

Instances For

def MeaningComponents.none :

MeaningComponents

No meaning components contributed. Identity for fuse.

Equations

MeaningComponents.none = { changeOfState := false, contact := false, motion := false, causation := false }

Instances For

def MeaningComponents.fuse (a b : MeaningComponents) :

MeaningComponents

Componentwise OR. Models how a construction augments a verb's inherent semantics (@cite{goldberg-1995}): if either the verb or the construction contributes a component, the composed meaning has it. This is the semantic side of @cite{goldberg-1995}'s "fusion".

Equations

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

Instances For

instance MeaningComponents.instAppend :

Append MeaningComponents

Equations

MeaningComponents.instAppend = { append := MeaningComponents.fuse }

theorem MeaningComponents.fuse_none_left (mc : MeaningComponents) :

none.fuse mc = mc

theorem MeaningComponents.fuse_none_right (mc : MeaningComponents) :

mc.fuse none = mc

theorem MeaningComponents.fuse_comm (a b : MeaningComponents) :

a.fuse b = b.fuse a

inductive LevinClass :

Verb class taxonomy from @cite{levin-1993} Part II.

Section numbers follow the book. Class names are Levin's labels. This provides a standardized, widely-cited reference for verb classification; 49 top-level classes covering the English verb lexicon.

Not all subclasses are listed here — the taxonomy is intentionally at the top-level class grain, with subclass distinctions handled by MeaningComponents and RootProfile.

Instances For

instance instDecidableEqLevinClass :

DecidableEq LevinClass

Equations

instDecidableEqLevinClass x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqLevinClass :

Equations

instBEqLevinClass = { beq := instBEqLevinClass.beq }

def instBEqLevinClass.beq :

LevinClass → LevinClass → Bool

Equations

instBEqLevinClass.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance instReprLevinClass :

Repr LevinClass

Equations

instReprLevinClass = { reprPrec := instReprLevinClass.repr }

def instReprLevinClass.repr :

LevinClass → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
instReprLevinClass.repr LevinClass.put prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.put")).group prec✝
instReprLevinClass.repr LevinClass.funnel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.funnel")).group prec✝
instReprLevinClass.repr LevinClass.pour prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.pour")).group prec✝
instReprLevinClass.repr LevinClass.coil prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.coil")).group prec✝
instReprLevinClass.repr LevinClass.sprayLoad prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.sprayLoad")).group prec✝
instReprLevinClass.repr LevinClass.remove prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.remove")).group prec✝
instReprLevinClass.repr LevinClass.clear prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.clear")).group prec✝
instReprLevinClass.repr LevinClass.wipe prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.wipe")).group prec✝
instReprLevinClass.repr LevinClass.steal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.steal")).group prec✝
instReprLevinClass.repr LevinClass.send prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.send")).group prec✝
instReprLevinClass.repr LevinClass.carry prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.carry")).group prec✝
instReprLevinClass.repr LevinClass.drive prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.drive")).group prec✝
instReprLevinClass.repr LevinClass.pushPull prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.pushPull")).group prec✝
instReprLevinClass.repr LevinClass.give prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.give")).group prec✝
instReprLevinClass.repr LevinClass.contribute prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.contribute")).group prec✝
instReprLevinClass.repr LevinClass.getObtain prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.getObtain")).group prec✝
instReprLevinClass.repr LevinClass.exchange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.exchange")).group prec✝
instReprLevinClass.repr LevinClass.learn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.learn")).group prec✝
instReprLevinClass.repr LevinClass.hold prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.hold")).group prec✝
instReprLevinClass.repr LevinClass.conceal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.conceal")).group prec✝
instReprLevinClass.repr LevinClass.throw prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.throw")).group prec✝
instReprLevinClass.repr LevinClass.hit prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.hit")).group prec✝
instReprLevinClass.repr LevinClass.swat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.swat")).group prec✝
instReprLevinClass.repr LevinClass.poke prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.poke")).group prec✝
instReprLevinClass.repr LevinClass.touch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.touch")).group prec✝
instReprLevinClass.repr LevinClass.cut prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.cut")).group prec✝
instReprLevinClass.repr LevinClass.carve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.carve")).group prec✝
instReprLevinClass.repr LevinClass.mix prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mix")).group prec✝
instReprLevinClass.repr LevinClass.amalgamate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.amalgamate")).group prec✝
instReprLevinClass.repr LevinClass.separate prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.separate")).group prec✝
instReprLevinClass.repr LevinClass.split prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.split")).group prec✝
instReprLevinClass.repr LevinClass.color prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.color")).group prec✝
instReprLevinClass.repr LevinClass.imageCreation prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.imageCreation")).group prec✝
instReprLevinClass.repr LevinClass.build prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.build")).group prec✝
instReprLevinClass.repr LevinClass.grow prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.grow")).group prec✝
instReprLevinClass.repr LevinClass.create prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.create")).group prec✝
instReprLevinClass.repr LevinClass.knead prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.knead")).group prec✝
instReprLevinClass.repr LevinClass.turn prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.turn")).group prec✝
instReprLevinClass.repr LevinClass.performance prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.performance")).group prec✝
instReprLevinClass.repr LevinClass.engender prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.engender")).group prec✝
instReprLevinClass.repr LevinClass.calve prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.calve")).group prec✝
instReprLevinClass.repr LevinClass.appoint prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.appoint")).group prec✝
instReprLevinClass.repr LevinClass.characterize prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.characterize")).group prec✝
instReprLevinClass.repr LevinClass.declare prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.declare")).group prec✝
instReprLevinClass.repr LevinClass.see prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.see")).group prec✝
instReprLevinClass.repr LevinClass.sight prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.sight")).group prec✝
instReprLevinClass.repr LevinClass.amuse prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.amuse")).group prec✝
instReprLevinClass.repr LevinClass.admire prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.admire")).group prec✝
instReprLevinClass.repr LevinClass.marvel prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.marvel")).group prec✝
instReprLevinClass.repr LevinClass.want prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.want")).group prec✝
instReprLevinClass.repr LevinClass.judgment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.judgment")).group prec✝
instReprLevinClass.repr LevinClass.assessment prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.assessment")).group prec✝
instReprLevinClass.repr LevinClass.search prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.search")).group prec✝
instReprLevinClass.repr LevinClass.socialInteraction prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.socialInteraction")).group prec✝
instReprLevinClass.repr LevinClass.say prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.say")).group prec✝
instReprLevinClass.repr LevinClass.tell prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.tell")).group prec✝
instReprLevinClass.repr LevinClass.mannerOfSpeaking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mannerOfSpeaking")).group prec✝
instReprLevinClass.repr LevinClass.animalSound prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.animalSound")).group prec✝
instReprLevinClass.repr LevinClass.eat prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.eat")).group prec✝
instReprLevinClass.repr LevinClass.devour prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.devour")).group prec✝
instReprLevinClass.repr LevinClass.dine prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.dine")).group prec✝
instReprLevinClass.repr LevinClass.bodyProcess prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bodyProcess")).group prec✝
instReprLevinClass.repr LevinClass.flinch prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.flinch")).group prec✝
instReprLevinClass.repr LevinClass.dress prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.dress")).group prec✝
instReprLevinClass.repr LevinClass.murder prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.murder")).group prec✝
instReprLevinClass.repr LevinClass.poison prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.poison")).group prec✝
instReprLevinClass.repr LevinClass.lightEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.lightEmission")).group prec✝
instReprLevinClass.repr LevinClass.soundEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.soundEmission")).group prec✝
instReprLevinClass.repr LevinClass.substanceEmission prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.substanceEmission")).group prec✝
instReprLevinClass.repr LevinClass.destroy prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.destroy")).group prec✝
instReprLevinClass.repr LevinClass.break_ prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.break_")).group prec✝
instReprLevinClass.repr LevinClass.bend prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bend")).group prec✝
instReprLevinClass.repr LevinClass.cooking prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.cooking")).group prec✝
instReprLevinClass.repr LevinClass.otherCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.otherCoS")).group prec✝
instReprLevinClass.repr LevinClass.entitySpecificCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.entitySpecificCoS")).group prec✝
instReprLevinClass.repr LevinClass.calibratableCoS prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.calibratableCoS")).group prec✝
instReprLevinClass.repr LevinClass.lodge prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.lodge")).group prec✝
instReprLevinClass.repr LevinClass.exist prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.exist")).group prec✝
instReprLevinClass.repr LevinClass.appear prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.appear")).group prec✝
instReprLevinClass.repr LevinClass.bodyInternalMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.bodyInternalMotion")).group prec✝
instReprLevinClass.repr LevinClass.assumePosition prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.assumePosition")).group prec✝
instReprLevinClass.repr LevinClass.leave prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.leave")).group prec✝
instReprLevinClass.repr LevinClass.mannerOfMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.mannerOfMotion")).group prec✝
instReprLevinClass.repr LevinClass.vehicleMotion prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.vehicleMotion")).group prec✝
instReprLevinClass.repr LevinClass.chase prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.chase")).group prec✝
instReprLevinClass.repr LevinClass.avoid prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.avoid")).group prec✝
instReprLevinClass.repr LevinClass.linger prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.linger")).group prec✝
instReprLevinClass.repr LevinClass.rush prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.rush")).group prec✝
instReprLevinClass.repr LevinClass.measure prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.measure")).group prec✝
instReprLevinClass.repr LevinClass.aspectual prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.aspectual")).group prec✝
instReprLevinClass.repr LevinClass.weather prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "LevinClass.weather")).group prec✝

Instances For

def LevinClass.section :

LevinClass → String

Section number in @cite{levin-1993} for each class.

Equations

LevinClass.put.section = "9.1"
LevinClass.funnel.section = "9.3"
LevinClass.pour.section = "9.5"
LevinClass.coil.section = "9.6"
LevinClass.sprayLoad.section = "9.7"
LevinClass.remove.section = "10.1"
LevinClass.clear.section = "10.3"
LevinClass.wipe.section = "10.4"
LevinClass.steal.section = "10.5"
LevinClass.send.section = "11.1"
LevinClass.carry.section = "11.4"
LevinClass.drive.section = "11.5"
LevinClass.pushPull.section = "12"
LevinClass.give.section = "13.1"
LevinClass.contribute.section = "13.2"
LevinClass.getObtain.section = "13.5"
LevinClass.exchange.section = "13.6"
LevinClass.learn.section = "14"
LevinClass.hold.section = "15.1"
LevinClass.conceal.section = "16"
LevinClass.throw.section = "17.1"
LevinClass.hit.section = "18.1"
LevinClass.swat.section = "18.2"
LevinClass.poke.section = "19"
LevinClass.touch.section = "20"
LevinClass.cut.section = "21.1"
LevinClass.carve.section = "21.2"
LevinClass.mix.section = "22.1"
LevinClass.amalgamate.section = "22.2"
LevinClass.separate.section = "23.1"
LevinClass.split.section = "23.2"
LevinClass.color.section = "24"
LevinClass.imageCreation.section = "25"
LevinClass.build.section = "26.1"
LevinClass.grow.section = "26.2"
LevinClass.create.section = "26.4"
LevinClass.knead.section = "26.5"
LevinClass.turn.section = "26.6"
LevinClass.performance.section = "26.7"
LevinClass.engender.section = "27"
LevinClass.calve.section = "28"
LevinClass.appoint.section = "29.1"
LevinClass.characterize.section = "29.2"
LevinClass.declare.section = "29.4"
LevinClass.see.section = "30.1"
LevinClass.sight.section = "30.2"
LevinClass.amuse.section = "31.1"
LevinClass.admire.section = "31.2"
LevinClass.marvel.section = "31.3"
LevinClass.want.section = "32.1"
LevinClass.judgment.section = "33"
LevinClass.assessment.section = "34"
LevinClass.search.section = "35"
LevinClass.socialInteraction.section = "36"
LevinClass.say.section = "37.7"
LevinClass.tell.section = "37.2"
LevinClass.mannerOfSpeaking.section = "37.3"
LevinClass.animalSound.section = "38"
LevinClass.eat.section = "39.1"
LevinClass.devour.section = "39.4"
LevinClass.dine.section = "39.5"
LevinClass.bodyProcess.section = "40.1"
LevinClass.flinch.section = "40.5"
LevinClass.dress.section = "41.1"
LevinClass.murder.section = "42.1"
LevinClass.poison.section = "42.2"
LevinClass.lightEmission.section = "43.1"
LevinClass.soundEmission.section = "43.2"
LevinClass.substanceEmission.section = "43.4"
LevinClass.destroy.section = "44"
LevinClass.break_.section = "45.1"
LevinClass.bend.section = "45.2"
LevinClass.cooking.section = "45.3"
LevinClass.otherCoS.section = "45.4"
LevinClass.entitySpecificCoS.section = "45.5"
LevinClass.calibratableCoS.section = "45.6"
LevinClass.lodge.section = "46"
LevinClass.exist.section = "47.1"
LevinClass.appear.section = "48.1"
LevinClass.bodyInternalMotion.section = "49"
LevinClass.assumePosition.section = "50"
LevinClass.inherentlyDirectedMotion.section = "51.1"
LevinClass.leave.section = "51.2"
LevinClass.mannerOfMotion.section = "51.3"
LevinClass.vehicleMotion.section = "51.4"
LevinClass.chase.section = "51.6"
LevinClass.avoid.section = "52"
LevinClass.linger.section = "53.1"
LevinClass.rush.section = "53.2"
LevinClass.measure.section = "54"
LevinClass.aspectual.section = "55"
LevinClass.weather.section = "57"

Instances For

def LevinClass.meaningComponents :

LevinClass → MeaningComponents

Meaning components associated with each Levin class.

Profiles are assigned using the diagnostic criteria from @cite{levin-1993}:

changeOfState: middle alternation (the glass broke / this bread cuts easily)
contact: body-part possessor ascension (I hit him on the arm / I hit his arm)
motion: conative alternation requires motion + contact (I cut at the bread)
causation: causative/inchoative alternation (she broke the vase / the vase broke)
instrumentSpec: verb specifies instrument/means (cut vs. break; p. 157)
mannerSpec: verb specifies manner of action (cooking, manner of motion; p. 244)

For classes not discussed in the canonical quadruple analysis, profiles are inferred from Part II class descriptions and alternation participation patterns.

Equations

LevinClass.put.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
LevinClass.funnel.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
LevinClass.pour.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
LevinClass.coil.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
LevinClass.sprayLoad.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
LevinClass.remove.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
LevinClass.clear.meaningComponents = { changeOfState := true, contact := false, motion := true, causation := true }
LevinClass.wipe.meaningComponents = { changeOfState := true, contact := true, motion := true, causation := true, mannerSpec := true }
LevinClass.steal.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
LevinClass.send.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true }
LevinClass.carry.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := true, mannerSpec := true }
LevinClass.drive.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := true, mannerSpec := true }
LevinClass.pushPull.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false }
LevinClass.give.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
LevinClass.contribute.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := true }
LevinClass.getObtain.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.exchange.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.learn.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.hold.meaningComponents = { changeOfState := false, contact := true, motion := false, causation := false }
LevinClass.conceal.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.throw.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := true }
LevinClass.hit.meaningComponents = MeaningComponents.hit
LevinClass.swat.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false }
LevinClass.poke.meaningComponents = { changeOfState := false, contact := true, motion := true, causation := false, instrumentSpec := true }
LevinClass.touch.meaningComponents = MeaningComponents.touch
LevinClass.cut.meaningComponents = MeaningComponents.cut
LevinClass.carve.meaningComponents = { changeOfState := true, contact := true, motion := true, causation := true, instrumentSpec := true }
LevinClass.mix.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.amalgamate.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.separate.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.split.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, instrumentSpec := true }
LevinClass.color.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true }
LevinClass.imageCreation.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, instrumentSpec := true }
LevinClass.build.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.grow.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.create.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.knead.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true, mannerSpec := true }
LevinClass.turn.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.performance.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
LevinClass.engender.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.calve.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := false }
LevinClass.appoint.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.characterize.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.declare.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.see.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.sight.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.amuse.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.admire.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.marvel.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.want.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.judgment.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.assessment.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.search.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.socialInteraction.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.say.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.tell.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.mannerOfSpeaking.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
LevinClass.animalSound.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
LevinClass.eat.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := false }
LevinClass.devour.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := false, mannerSpec := true }
LevinClass.dine.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
LevinClass.bodyProcess.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.flinch.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.dress.meaningComponents = { changeOfState := true, contact := true, motion := false, causation := true }
LevinClass.murder.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.poison.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true, instrumentSpec := true }
LevinClass.lightEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.soundEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.substanceEmission.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.destroy.meaningComponents = MeaningComponents.destroy
LevinClass.break_.meaningComponents = MeaningComponents.break_
LevinClass.bend.meaningComponents = MeaningComponents.bend
LevinClass.cooking.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true, mannerSpec := true }
LevinClass.otherCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.entitySpecificCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.calibratableCoS.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.lodge.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.exist.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.appear.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := false }
LevinClass.bodyInternalMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.assumePosition.meaningComponents = { changeOfState := true, contact := false, motion := true, causation := false }
LevinClass.inherentlyDirectedMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.leave.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.mannerOfMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
LevinClass.vehicleMotion.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
LevinClass.chase.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false }
LevinClass.avoid.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.linger.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false, mannerSpec := true }
LevinClass.rush.meaningComponents = { changeOfState := false, contact := false, motion := true, causation := false, mannerSpec := true }
LevinClass.measure.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }
LevinClass.aspectual.meaningComponents = { changeOfState := true, contact := false, motion := false, causation := true }
LevinClass.weather.meaningComponents = { changeOfState := false, contact := false, motion := false, causation := false }

Instances For

def LevinClass.predictsUnaccusative :

LevinClass → Bool

Predicted unaccusativity from Levin class membership.

Based on Levin & Rappaport @cite{levin-hovav-1995}: unaccusativity correlates with internally caused change of state or directed change, while unergativity correlates with agentive activity.

For classes that participate in the causative/inchoative alternation (CoS + causation), this predicts unaccusativity for the intransitive (inchoative) alternant. For inherently intransitive classes (emission, existence, appearance), this predicts unaccusativity outright.

Key omission: manner-of-speaking verbs (§37.3) are predicted unergative here (agentive manner), but @cite{storment-2026} shows they are empirically unaccusative. This is a documented divergence.

Equations

Instances For

Unaccusativity prediction theorems #

CoS classes (§45) predict unaccusative.

theorem mom_predicts_unergative :

LevinClass.mannerOfMotion.predictsUnaccusative = false

Manner-of-motion (§51.3) predicts unergative.

theorem idm_predicts_unaccusative :

LevinClass.inherentlyDirectedMotion.predictsUnaccusative = true

Inherently directed motion (§51.1) predicts unaccusative.

theorem emission_predicts_unaccusative :

LevinClass.lightEmission.predictsUnaccusative = true ∧ LevinClass.soundEmission.predictsUnaccusative = true ∧ LevinClass.substanceEmission.predictsUnaccusative = true

Emission classes (§43) predict unaccusative.

theorem mos_predicts_unergative :

LevinClass.mannerOfSpeaking.predictsUnaccusative = false

MoS (§37.3) does NOT predict unaccusative — this is the Storment divergence.

def LevinClass.rootEntailments :

LevinClass → RootEntailments

Root structural entailments for each Levin class.

Assignments marked (B&KG) are directly from @cite{beavers-koontz-garboden-2020} Table 12 and Chapters 2–5. Others are inferred from class semantics following B&KG's framework:

Externally caused CoS → causativeResult (√CRACK pattern)
Internally caused CoS → pureResult (√BLOSSOM pattern)
Action/manner verbs → pureManner (√JOG pattern)
MRC violators → fullSpec (√HAND/√DROWN pattern)
Stative/psychological → propertyConcept (√FLAT pattern)

Classes marked (default) use minimal as a conservative placeholder pending detailed study under B&KG's framework.

Equations

Instances For

Well-formedness verification #

All canonical types satisfy the constraints, so every branch of rootEntailments is well-formed (each branch returns a canonical type).

theorem break_root_wf :

LevinClass.break_.rootEntailments.wellFormed = true

Break roots (√CRACK) are well-formed.

theorem cut_root_wf :

LevinClass.cut.rootEntailments.wellFormed = true

Cut roots (MRC violator, fullSpec) are well-formed.

theorem hit_root_wf :

LevinClass.hit.rootEntailments.wellFormed = true

Hit roots (pureManner) are well-formed.

theorem touch_root_wf :

LevinClass.touch.rootEntailments.wellFormed = true

Touch roots (minimal) are well-formed.

theorem give_root_wf :

LevinClass.give.rootEntailments.wellFormed = true

Give roots (√HAND, fullSpec) are well-formed.

theorem destroy_root_wf :

LevinClass.destroy.rootEntailments.wellFormed = true

Destroy roots (causativeResult) are well-formed.

theorem murder_root_wf :

LevinClass.murder.rootEntailments.wellFormed = true

Murder roots (causativeResult) are well-formed.

theorem poison_root_wf :

LevinClass.poison.rootEntailments.wellFormed = true

Poison roots (√DROWN-type fullSpec) are well-formed.

MRC violation verification #

theorem cut_violates_MRC :

LevinClass.cut.rootEntailments.violatesMRC = true

Cut is an MRC violator (B&KG Ch. 4): manner of cutting + caused separation.

theorem cooking_violates_MRC :

LevinClass.cooking.rootEntailments.violatesMRC = true

Cooking is an MRC violator: cooking manner + caused CoS.

theorem poison_violates_MRC :

LevinClass.poison.rootEntailments.violatesMRC = true

Poison (√DROWN-type) is an MRC violator: poisoning manner + caused death.

theorem break_respects_MRC :

LevinClass.break_.rootEntailments.violatesMRC = false

Break respects MRC — pure result (√CRACK), no manner.

theorem hit_respects_MRC :

LevinClass.hit.rootEntailments.violatesMRC = false

Hit respects MRC — pure manner (√JOG-type), no result.

Root–MC correspondence (2026 consensus) #

The 2026 consensus in lexical semantics (@cite{beavers-koontz-garboden-2020}, @cite{rappaport-hovav-levin-2024}) treats root entailments as primary: verb behavior at the Levin diagnostic level is determined by root content plus semantic field membership plus template structure.

But the B&KG root features and the Levin meaning components are NOT isomorphic — they conceptualize different levels of granularity:

B&KG concept	Levin concept	Relationship
`result`	`changeOfState`	B&KG broader: includes location/possession change
`manner`	`mannerSpec` ∨ `instrumentSpec`	B&KG broader: includes contact-manner (hit)
`cause`	`causation`	Distinct: root-level vs event-level causation

The three *Kind enums below name the specific cases where the two frameworks diverge, making the divergences grep-able and testable.

inductive CausationSource :

Where a verb class's event-level causation originates.

B&KG's root-level cause and Levin's event-level causation are distinct concepts (@cite{beavers-koontz-garboden-2020} Ch. 5; @cite{levin-1993} pp. 9–10):

rootExternal: root entails detachable external causation. break: √CRACK entails cause, and the inchoative the vase broke is available. re.cause = true, mc.causation = true.
rootNonDetachable: root entails causation but it can't be syntactically removed — no inchoative variant. eat: √EAT entails the eater causes consumption, but *the cake ate is bad. re.cause = true, mc.causation = false.
template: the event structure template provides vCAUSE but the root itself doesn't entail it. put: √PUT is minimal (no structural entailments), but the putting frame is causative. re.cause = false, mc.causation = true.
none: no causation component. hit: neither root nor template contributes causation. re.cause = false, mc.causation = false.

rootExternal : CausationSource
rootNonDetachable : CausationSource
template : CausationSource
none : CausationSource

Instances For

instance instDecidableEqCausationSource :

DecidableEq CausationSource

Equations

instDecidableEqCausationSource x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqCausationSource :

BEq CausationSource

Equations

instBEqCausationSource = { beq := instBEqCausationSource.beq }

def instBEqCausationSource.beq :

CausationSource → CausationSource → Bool

Equations

instBEqCausationSource.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance instReprCausationSource :

Repr CausationSource

Equations

instReprCausationSource = { reprPrec := instReprCausationSource.repr }

def instReprCausationSource.repr :

CausationSource → Nat → Std.Format

Equations

One or more equations did not get rendered due to their size.
instReprCausationSource.repr CausationSource.rootExternal prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausationSource.rootExternal")).group prec✝
instReprCausationSource.repr CausationSource.template prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausationSource.template")).group prec✝
instReprCausationSource.repr CausationSource.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "CausationSource.none")).group prec✝

Instances For

def LevinClass.causationSource (c : LevinClass) :

CausationSource

Derive the causation source from root entailments and meaning components. This is a derived classification: it follows from the relationship between B&KG's root cause and Levin's causation.

Equations

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

Instances For

inductive ResultKind :

What kind of result the root entails (refines B&KG result).

Levin's changeOfState corresponds to stateChange only — change of location (throw, arrive) and change of possession (give) have result = true in B&KG but changeOfState = false in Levin.

stateChange : ResultKind
locationChange : ResultKind
possessionChange : ResultKind
none : ResultKind

Instances For

instance instDecidableEqResultKind :

DecidableEq ResultKind

Equations

instDecidableEqResultKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqResultKind :

Equations

instBEqResultKind = { beq := instBEqResultKind.beq }

def instBEqResultKind.beq :

ResultKind → ResultKind → Bool

Equations

instBEqResultKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

instance instReprResultKind :

Repr ResultKind

Equations

instReprResultKind = { reprPrec := instReprResultKind.repr }

def instReprResultKind.repr :

ResultKind → Nat → Std.Format

Equations

instReprResultKind.repr ResultKind.stateChange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultKind.stateChange")).group prec✝
instReprResultKind.repr ResultKind.locationChange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultKind.locationChange")).group prec✝
instReprResultKind.repr ResultKind.possessionChange prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultKind.possessionChange")).group prec✝
instReprResultKind.repr ResultKind.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "ResultKind.none")).group prec✝

Instances For

def LevinClass.resultKind (c : LevinClass) :

Derive result kind from root entailments and meaning components.

Equations

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

Instances For

inductive MannerKind :

How root manner maps to Levin's MC spec features.

B&KG's manner subsumes three Levin-level distinctions:

mannerSpec: how the action proceeds (cooking, running)
instrumentSpec: what tool is used (cutting, poking)
unspecified: manner verb without a Levin spec flag (hit, push)

The last case reflects a genuine conceptual gap: B&KG codes any action-specifying root as +manner, while Levin reserves mannerSpec and instrumentSpec for manner specifications with specific diagnostic consequences (blocking alternations, etc.).

mannerSpec : MannerKind
instrumentSpec : MannerKind
unspecified : MannerKind
none : MannerKind

Instances For

instance instDecidableEqMannerKind :

DecidableEq MannerKind

Equations

instDecidableEqMannerKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance instBEqMannerKind :

Equations

instBEqMannerKind = { beq := instBEqMannerKind.beq }

def instBEqMannerKind.beq :

MannerKind → MannerKind → Bool

Equations

instBEqMannerKind.beq x✝ y✝ = (x✝.ctorIdx == y✝.ctorIdx)

Instances For

def instReprMannerKind.repr :

MannerKind → Nat → Std.Format

Equations

instReprMannerKind.repr MannerKind.mannerSpec prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MannerKind.mannerSpec")).group prec✝
instReprMannerKind.repr MannerKind.instrumentSpec prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MannerKind.instrumentSpec")).group prec✝
instReprMannerKind.repr MannerKind.unspecified prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MannerKind.unspecified")).group prec✝
instReprMannerKind.repr MannerKind.none prec✝ = Repr.addAppParen (Std.Format.nest (if prec✝ ≥ 1024 then 1 else 2) (Std.Format.text "MannerKind.none")).group prec✝

Instances For

instance instReprMannerKind :

Repr MannerKind

Equations

instReprMannerKind = { reprPrec := instReprMannerKind.repr }

def LevinClass.mannerKind (c : LevinClass) :

Derive manner kind from root entailments and meaning components.

Equations

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

Instances For

Causation source verification #

theorem break_causation_rootExternal :

LevinClass.break_.causationSource = CausationSource.rootExternal

theorem destroy_causation_rootExternal :

LevinClass.destroy.causationSource = CausationSource.rootExternal

theorem murder_causation_rootExternal :

LevinClass.murder.causationSource = CausationSource.rootExternal

theorem eat_causation_rootNonDetachable :

LevinClass.eat.causationSource = CausationSource.rootNonDetachable

Eat: root cause is non-detachable — no inchoative *the cake ate.

theorem devour_causation_rootNonDetachable :

LevinClass.devour.causationSource = CausationSource.rootNonDetachable

theorem put_causation_template :

LevinClass.put.causationSource = CausationSource.template

Put: template provides causation; root is minimal.

theorem send_causation_template :

LevinClass.send.causationSource = CausationSource.template

theorem grow_causation_template :

LevinClass.grow.causationSource = CausationSource.template

Grow: root is pureResult (internally caused); template adds vCAUSE for the transitive the farmer grew tomatoes.

theorem hit_causation_none :

LevinClass.hit.causationSource = CausationSource.none

theorem mannerOfMotion_causation_none :

LevinClass.mannerOfMotion.causationSource = CausationSource.none

Result kind verification #

theorem break_result_stateChange :

LevinClass.break_.resultKind = ResultKind.stateChange

theorem destroy_result_stateChange :

LevinClass.destroy.resultKind = ResultKind.stateChange

theorem throw_result_locationChange :

LevinClass.throw.resultKind = ResultKind.locationChange

Throw: root entails result (ball arrives), but it's a location change, not an internal state change → changeOfState = false.

theorem inherentlyDirectedMotion_result_locationChange :

LevinClass.inherentlyDirectedMotion.resultKind = ResultKind.locationChange

theorem leave_result_locationChange :

LevinClass.leave.resultKind = ResultKind.locationChange

theorem give_result_possessionChange :

LevinClass.give.resultKind = ResultKind.possessionChange

Give: root entails result (possession transfers), but it's a possession change, not an internal state change.

theorem hit_result_none :

LevinClass.hit.resultKind = ResultKind.none

Manner kind verification #

theorem cooking_manner_mannerSpec :

LevinClass.cooking.mannerKind = MannerKind.mannerSpec

theorem mannerOfMotion_manner_mannerSpec :

LevinClass.mannerOfMotion.mannerKind = MannerKind.mannerSpec

theorem cut_manner_instrumentSpec :

LevinClass.cut.mannerKind = MannerKind.instrumentSpec

Cut: B&KG +manner (cutting action), Levin codes as instrumentSpec.

theorem poke_manner_instrumentSpec :

LevinClass.poke.mannerKind = MannerKind.instrumentSpec

theorem hit_manner_unspecified :

LevinClass.hit.mannerKind = MannerKind.unspecified

Hit: B&KG +manner (impact action), but Levin codes the manner as contact + motion in the semantic field, not as a spec flag.

theorem pushPull_manner_unspecified :

LevinClass.pushPull.mannerKind = MannerKind.unspecified

PushPull: B&KG +manner, but Levin gives no spec flag.

theorem break_manner_none :

LevinClass.break_.mannerKind = MannerKind.none

Root-structural MC contribution #

The conservative structural derivation from root entailments to meaning components. Only sets features that the root structure UNAMBIGUOUSLY contributes — other features require class-level information.

def RootEntailments.structuralMC (re : RootEntailments) :

MeaningComponents

Root structural contribution to meaning components. Maps result → changeOfState and manner → mannerSpec. These are the two correspondences where the MAJORITY of classes agree (modulo the documented divergences above). Causation and semantic-field features (contact, motion, instrumentSpec) are omitted — they require class-level information.

Equations

re.structuralMC = { changeOfState := re.result, contact := false, motion := false, causation := false, mannerSpec := re.manner }

Instances For

Universal consistency theorems #

These hold for ALL 78 LevinClass constructors and are proved by exhaustive case analysis. They capture the reliable structural correspondences between B&KG and Levin.

def LevinClass.specImpliesManner (c : LevinClass) :

Levin spec implies B&KG manner: if Levin marks a class as manner-specified or instrument-specified, B&KG codes the root as +manner. The reverse does NOT hold (hit, pushPull are +manner in B&KG but lack MC spec flags).

Equations

c.specImpliesManner = (!(c.meaningComponents.mannerSpec || c.meaningComponents.instrumentSpec) || c.rootEntailments.manner)

Instances For

theorem levin_spec_implies_bkg_manner (c : LevinClass) :

c.specImpliesManner = true

def LevinClass.causativeResultImpliesCos (c : LevinClass) :

CausativeResult roots always have changeOfState: every class whose root entails externally caused result (causativeResult) has CoS in its meaning components. This is the strongest result↔CoS correspondence — it holds without exception.

Equations

c.causativeResultImpliesCos = (!c.rootEntailments == RootEntailments.causativeResult || c.meaningComponents.changeOfState)

Instances For

theorem causativeResult_always_cos (c : LevinClass) :

c.causativeResultImpliesCos = true

def LevinClass.causeImpliesCausationOrNonDetach (c : LevinClass) :

Root cause implies either event causation or non-detachable causation: if B&KG says the root entails cause, then Levin's MC has causation = true OR the class is eat/devour-type (non-detachable). Put differently: root cause = false whenever MC causation = false AND the root is not a non-detachable causer.

Equations

c.causeImpliesCausationOrNonDetach = (!c.rootEntailments.cause || c.meaningComponents.causation || c.causationSource == CausationSource.rootNonDetachable)

Instances For

theorem root_cause_accounted_for (c : LevinClass) :

c.causeImpliesCausationOrNonDetach = true