Semantics.Lexical.MeaningComponents

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

Binary meaning-component features that define @cite{levin-1993} verb classes diagnostically (via diathesis alternation participation), with the fuse operator for componentwise composition.

Provenance

Moved from Core/Lexical/VerbClass.lean in the cleanup that dissolved Core/Lexical/. Lives at Theories/Semantics/Lexical/ (sibling of LevinTheory.lean, LevinClassProfiles.lean, LevinClass.lean, DiathesisAlternation.lean) because it encodes Levin's specific diagnostic apparatus (CoS / contact / motion / causation as the 4 canonical features) — paper-anchored framework content, not consensus substrate.

Framework commitment

The 4-feature decomposition is @cite{levin-1993}'s diagnostic apparatus. @cite{beavers-koontz-garboden-2020} argue these are SURFACE behaviors, not root-level entailments — root-level structural features live in Theories/Semantics/Lexical/Roots/RootFeatures.lean::RootEntailments (state/manner/result/cause). The two carve-ups are NOT equivalent: e.g., causation here is what diathesis alternations diagnose, while B&KG's cause is a root entailment.

The instrumentSpec and mannerSpec features supplement the 4-feature core for finer-grained subclass distinctions in Part II.

Note on fuse

fuse a b is componentwise OR — the formaliser's design choice for modeling how a construction augments a verb's inherent semantics. Originally attributed to @cite{goldberg-1995} in source comments, but Goldberg's actual constructional unification is not componentwise boolean OR (it involves semantic frame unification with role-fusion constraints, far more structured than disjunctive feature OR). The substrate's fuse is a useful approximation but should not be cited as Goldberg's operation directly.

Alternative frameworks not formalized at parallel substrate granularity

The Levin-style alternation-diagnosed feature decomposition competes with other lexical-semantic frameworks worth formalizing as siblings:

• Generative Lexicon (@cite{pustejovsky-1995}): qualia structure (formal/constitutive/telic/agentive) as the primitive decomposition.
• Frame semantics (@cite{fillmore-1982}, @cite{fillmore-kay-oconnor-1988}): semantic frames as primitive, alternations as surface reflexes.
• Lexical Conceptual Structure (@cite{jackendoff-1996}): primitive predicates GO/STAY/CAUSE compose into LCS templates.
• Configurational lexical semantics (@cite{hale-keyser-1987}): verb meaning derives from syntactic configuration, not feature decomposition.

structure Semantics.Lexical.MeaningComponents : Type

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 in Theories/Semantics/Lexical/Roots/RootFeatures.lean for the root-level decomposition.

Diagnosed by participation in diathesis alternations:

• 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)
• mannerSpec: verb specifies manner of action

UNVERIFIED: Levin Part II page references for instrumentSpec/mannerSpec cited from memory.

• changeOfState : Bool
• contact : Bool
• motion : Bool
• causation : Bool
• instrumentSpec : Bool
• mannerSpec : Bool

@[implicit_reducible]

instance Semantics.Lexical.instDecidableEqMeaningComponents : DecidableEq MeaningComponents

Equations

• Semantics.Lexical.instDecidableEqMeaningComponents = Semantics.Lexical.instDecidableEqMeaningComponents.decEq

def Semantics.Lexical.instDecidableEqMeaningComponents.decEq (x✝ x✝¹ : MeaningComponents) : Decidable (x✝ = x✝¹)

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.instReprMeaningComponents : Repr MeaningComponents

Equations

• Semantics.Lexical.instReprMeaningComponents = { reprPrec := Semantics.Lexical.instReprMeaningComponents.repr }

def Semantics.Lexical.instReprMeaningComponents.repr : MeaningComponents → Nat → Std.Format

Equations

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

def Semantics.Lexical.MeaningComponents.break_ : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.cut : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.hit : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.touch : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.destroy : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.bend : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.none : MeaningComponents

Equations

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

def Semantics.Lexical.MeaningComponents.fuse (a b : MeaningComponents) : MeaningComponents

Componentwise OR. The formaliser's chosen approximation of construction-on-verb composition; not equivalent to Goldberg's actual constructional unification (see file docstring).

Equations

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

@[implicit_reducible]

instance Semantics.Lexical.MeaningComponents.instAppend : Append MeaningComponents

Equations

• Semantics.Lexical.MeaningComponents.instAppend = { append := Semantics.Lexical.MeaningComponents.fuse }

theorem Semantics.Lexical.MeaningComponents.fuse_none_left (mc : MeaningComponents) : none.fuse mc = mc

theorem Semantics.Lexical.MeaningComponents.fuse_none_right (mc : MeaningComponents) : mc.fuse none = mc

theorem Semantics.Lexical.MeaningComponents.fuse_comm (a b : MeaningComponents) : a.fuse b = b.fuse a