Documentation

Linglib.Theories.Semantics.Lexical.LevinClass

Semantics.Lexical.LevinClass #

@cite{levin-1993}

The 49-class verb taxonomy from @cite{levin-1993} Part II, with per-class meaning-component profiles, unaccusativity prediction, and verb-of-creation flag.

Provenance #

Moved from Core/Lexical/VerbClass.lean in the cleanup that dissolved Core/Lexical/. Lives at Theories/Semantics/Lexical/ (sibling of LevinTheory.lean for root-entailment derivation, LevinClassProfiles.lean for argument templates, MeaningComponents.lean for the diagnostic features) — Levin's framework, not consensus substrate.

Framework commitment #

@cite{levin-1993}'s 49 classes are the most widely-cited reference for English verb classification, but they are not the only such taxonomy. Sibling theory-named slots are intentionally unfilled in this restructure:

Future formalisations of these alternatives should land as siblings here, with refutation theorems showing where they diverge from Levin on attested verbs.

Citation hygiene notes #

Alternative frameworks not formalized in linglib #

The Levin-style alternation-diagnosed classification competes with other lexical-semantic frameworks that may be worth formalizing as sibling theories:

source
inductive Semantics.Lexical.LevinClass :
Type

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

Section numbers follow the book. Class names are Levin's labels. 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.

UNVERIFIED: Per-class section numbers (e.g., § 9.1 for .put) cited from memory — verify against the published monograph.

Instances For
    source
    @[implicit_reducible]
    instance Semantics.Lexical.instDecidableEqLevinClass :
    DecidableEq LevinClass
    Equations
    source
    def Semantics.Lexical.instReprLevinClass.repr :
    LevinClass → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Lexical.instReprLevinClass :
      Repr LevinClass
      Equations
      source
      def Semantics.Lexical.LevinClass.levinSection :
      LevinClass → String

      Section number in @cite{levin-1993} for each class. The bare name section would clash with Lean's reserved keyword; we use levinSection as the canonical accessor.

      UNVERIFIED: Per-class section numbers cited from memory; verify against the published monograph.

      Equations
      Instances For
        source
        def Semantics.Lexical.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
        • contact: body-part possessor ascension
        • motion: conative alternation requires motion + contact
        • causation: causative/inchoative alternation
        • instrumentSpec: verb specifies instrument/means
        • mannerSpec: verb specifies manner of action

        UNVERIFIED: Per-class meaning-component assignments are summary judgments; the canonical break/cut/hit/touch from Levin's Introduction are the most reliably cited; per-class assignments for the other 45 classes are the formaliser's interpretation of Part II text and should be cross-checked.

        Equations
        Instances For
          source
          def Semantics.Lexical.LevinClass.PredictsUnaccusative :
          LevinClass → Prop

          Predicted unaccusativity from Levin class membership.

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

          Equations
          Instances For
            source
            @[implicit_reducible]
            instance Semantics.Lexical.LevinClass.instDecidablePredPredictsUnaccusative :
            DecidablePred PredictsUnaccusative
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def Semantics.Lexical.LevinClass.isVerbOfCreation :
            LevinClass → Bool

            Whether a Levin class denotes creation of the object referent. @cite{davies-dubinsky-2003}: VOCs produce their direct object as a result of the event.

            Equations
            Instances For
              source
              def Semantics.Lexical.LevinClass.pathSpec :
              LevinClass → Option Spatial.Path.PathShape

              Whether a verb class inherently specifies a path shape. Inherently directed motion verbs (Levin 51.1: arrive, come, go) lexicalize a bounded path. Manner-of-motion verbs (51.3: run, walk) are path-neutral — the path comes from a PP complement. @cite{talmy-2000}: verb-framed vs. satellite-framed distinction.

              Equations
              Instances For