Documentation

Linglib.Core.Lexical.DiathesisAlternation

Diathesis Alternation Types and Prediction #

@cite{levin-1993}

Alternation types (§ 1) #

Twenty-five curated diathesis alternation types from @cite{levin-1993} Part One, covering the diagnostically active alternations that discriminate verb classes. Organized into six AlternationFamily groups matching Part One's chapters.

Alternation families (§ 1a) #

AlternationFamily classifies alternations by the chapter of @cite{levin-1993} Part One where they are primarily discussed:

Prediction (§ 2) #

MeaningComponents.predictedAlternation derives alternation participation from meaning components. LevinClass.participatesIn combines component-derived predictions with class-specific overrides.

Diagnostic theorems (§ 3) #

Per-class alternation profiles and cross-class predictions, verifiable by rfl.

source
inductive AlternationFamily :
Type

Classification of diathesis alternations by the chapter of @cite{levin-1993} Part One where they are primarily discussed.

This provides organizational grouping for the curated enum — the ~25 diagnostically active alternations. The remaining ~50 narrow alternations from Part One are documented as data/prose, not as enum constructors.

  • transitivity : AlternationFamily

    Ch 1: Transitivity alternations — changes in the number of arguments (causative/inchoative, induced action, middle, conative, object drop).

  • vpInternal : AlternationFamily

    Ch 2: Alternations involving arguments within the VP — rearrangement of internal arguments (dative, benefactive, locative, swarm, etc.).

  • obliqueSubject : AlternationFamily

    Ch 3: Oblique subject alternations — non-agent subjects (instrument subject).

  • passive : AlternationFamily

    Ch 5: Passive — verbal and prepositional passives.

  • postverbalSubject : AlternationFamily

    Ch 6: Alternations involving postverbal subjects — there-insertion, locative inversion (unaccusative diagnostics).

  • otherConstructions : AlternationFamily

    Ch 7: Other constructions — way construction, cognate object, resultative, directional phrase.

Instances For
    source
    instance instDecidableEqAlternationFamily :
    DecidableEq AlternationFamily
    Equations
    source
    instance instBEqAlternationFamily :
    BEq AlternationFamily
    Equations
    source
    def instBEqAlternationFamily.beq :
    AlternationFamily → AlternationFamily → Bool
    Equations
    Instances For
      source
      def instReprAlternationFamily.repr :
      AlternationFamily → Nat → Std.Format
      Equations
      Instances For
        source
        instance instReprAlternationFamily :
        Repr AlternationFamily
        Equations
        source
        inductive DiathesisAlternation :
        Type

        Curated diathesis alternations from @cite{levin-1993} Part One that serve as diagnostics for verb class membership. Twenty-five alternation types covering the diagnostically active subset of ~79 alternations in Part One.

        The first four are the canonical diagnostics from the Introduction (pp. 5–10); others are from specific chapters. Each is classified by AlternationFamily.

        • causativeInchoative : DiathesisAlternation

          §1.1.2.1: she broke the vase / the vase broke. Diagnoses causation + CoS.

        • inducedAction : DiathesisAlternation

          §1.1.2.2: Bill ran the horse. Causative use of intransitive manner-of-motion verbs.

        • middle : DiathesisAlternation

          §1.1.1: the bread cuts easily. Diagnoses change of state.

        • conative : DiathesisAlternation

          §1.3: I cut at the bread. Diagnoses contact + motion.

        • substanceSource : DiathesisAlternation

          §1.1.3: heat radiates from the sun / the sun radiates heat. Substance emission verbs.

        • unspecifiedObject : DiathesisAlternation

          §1.2.1: Mike ate the cake / Mike ate. Activity verbs (eat, read, cook, ...). The intransitive has an unexpressed but understood indefinite object.

        • understoodBodyPartObject : DiathesisAlternation

          §1.2.2: Bill waved his hand / Bill waved. Body-part verbs where the object names the moved body part.

        • understoodReflexiveObject : DiathesisAlternation

          §1.2.3: Bill washed himself / Bill washed. Grooming/body-care verbs where the reflexive object can be dropped.

        • understoodReciprocalObject : DiathesisAlternation

          §1.2.4: Anne met Cathy / Anne and Cathy met. Social interaction verbs. Intransitive paraphrasable as transitive with each other.

        • dative : DiathesisAlternation

          §2.1: give NP NP / give NP to NP. Give/send class.

        • benefactive : DiathesisAlternation

          §2.2: Martha carved a toy for the baby / Martha carved the baby a toy. Verbs of obtaining and creation.

        • locative : DiathesisAlternation

          §2.3: spray paint on wall / spray wall with paint. Spray/load class.

        • bodyPartPossessorAscension : DiathesisAlternation

          §2.12: I hit him on the arm / I hit his arm. Diagnoses contact.

        • swarm : DiathesisAlternation

          §2.3.4: Bees swarmed in the garden / The garden swarmed with bees. Intransitive locative alternation for verbs of spatial configuration.

        • materialProduct : DiathesisAlternation

          §2.4.1: Martha carved a toy out of wood / Martha carved the wood into a toy. Build/creation verbs.

        • totalTransformation : DiathesisAlternation

          §2.4.3: the witch turned the prince into a frog. Complete change of entity type. Turn/convert verbs.

        • instrumentSubject : DiathesisAlternation

          §3.3: David broke the window with a hammer / the hammer broke the window. Intermediary instruments can become subjects with externally caused verbs.

        • verbalPassive : DiathesisAlternation

          §5.1: the window was broken (by the boy). Fundamental voice alternation for transitive verbs.

        • prepositionalPassive : DiathesisAlternation

          §5.2: the bed was slept in. Passive of intransitive + PP, diagnostic for unergative verbs.

        • thereInsertion : DiathesisAlternation

          §6.1: a problem developed / there developed a problem. Unaccusative diagnostic: existence/appearance verbs.

        • locativeInversion : DiathesisAlternation

          §6.2: an old woman lives in the woods / in the woods lives an old woman. Unaccusative diagnostic: existence/spatial configuration verbs.

        • cognateObject : DiathesisAlternation

          §7.1: she laughed a bitter laugh. Unergative diagnostic: agentive intransitives can take cognate objects.

        • wayConstruction : DiathesisAlternation

          §7.4: she elbowed her way through the crowd. Manner-of-motion and body-motion verbs.

        • resultative : DiathesisAlternation

          §7.5: hammer the metal flat. Available to manner verbs.

        • directionalPhrase : DiathesisAlternation

          §7.8: she ran to the store. Manner-of-motion verbs with directional PPs (Talmy's satellite-framing).

        Instances For
          source
          instance instDecidableEqDiathesisAlternation :
          DecidableEq DiathesisAlternation
          Equations
          source
          instance instBEqDiathesisAlternation :
          BEq DiathesisAlternation
          Equations
          source
          def instBEqDiathesisAlternation.beq :
          DiathesisAlternation → DiathesisAlternation → Bool
          Equations
          Instances For
            source
            def instReprDiathesisAlternation.repr :
            DiathesisAlternation → Nat → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              instance instReprDiathesisAlternation :
              Repr DiathesisAlternation
              Equations
              source
              def DiathesisAlternation.family :
              DiathesisAlternation → AlternationFamily

              Which family of @cite{levin-1993} Part One each alternation belongs to. Classifies the 25 curated alternations into 6 families matching the chapter structure of Part One.

              Equations
              Instances For
                source
                def MeaningComponents.predictedAlternation :
                MeaningComponents → DiathesisAlternation → Bool

                Predicted alternation participation derived from meaning components.

                The core claim of @cite{levin-1993}: meaning components — diagnosed by alternation participation — form the bridge between verb semantics and verb syntax. Each diagnostic alternation corresponds to a specific configuration of meaning components:

                AlternationRequired components
                Causative/inchoativechangeOfState ∧ causation ∧ ¬instrumentSpec
                MiddlechangeOfState
                Conativecontact ∧ motion
                Body-part possessor ascensioncontact
                Instrument subjectcausation ∧ ¬instrumentSpec
                ResultativechangeOfState ∧ ¬instrumentSpec (manner verbs)

                The remaining alternations are class-specific rather than component-derived.

                Equations
                Instances For
                  source
                  def LevinClass.participatesIn (c : LevinClass) (alt : DiathesisAlternation) :
                  Bool

                  Full alternation profile for a Levin class, combining component-derived predictions with class-specific overrides.

                  Component-derived: causativeInchoative, middle, conative, bodyPartPossessorAscension, instrumentSubject, resultative.

                  Class-specific overrides below, verified against @cite{levin-1993} Part I verb lists and Part II class descriptions.

                  Instances For

                    Canonical diagnostic theorems #

                    The four verbs break, cut, hit, touch are distinguished by exactly their pattern of alternation participation (@cite{levin-1993}:5–10).

                    source
                    theorem break_alternations :
                    LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.break_.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.bodyPartPossessorAscension = false

                    Break participates in causative/inchoative and middle (CoS + causation).

                    source
                    theorem cut_alternations :
                    LevinClass.cut.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.cut.participatesIn DiathesisAlternation.middle = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                    Cut participates in middle, conative, and BPPA but NOT causative/inchoative. Instrument specification blocks the inchoative: "*The string cut." (Levin p. 9, ex. 23b). Because cut inherently specifies an instrument, it requires an agent (p. 10).

                    source
                    theorem hit_alternations :
                    LevinClass.hit.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.hit.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                    Hit participates in conative and body-part ascension (contact + motion, no CoS).

                    source
                    theorem touch_alternations :
                    LevinClass.touch.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.middle = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.conative = false ∧ LevinClass.touch.participatesIn DiathesisAlternation.bodyPartPossessorAscension = true

                    Touch participates only in body-part ascension (contact only).

                    source
                    theorem MeaningComponents.instrumentSpec_blocks_ci (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                    mc.predictedAlternation DiathesisAlternation.causativeInchoative = false

                    Instrument specification blocks the causative/inchoative alternation for any verb, regardless of other meaning components. Because the instrument must be wielded by an agent, the agentless inchoative variant is unavailable.

                    source
                    theorem MeaningComponents.instrumentSpec_blocks_resultative (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                    mc.predictedAlternation DiathesisAlternation.resultative = false

                    Corollary: instrument specification also blocks the resultative (same reasoning — manner verbs that specify an instrument cannot appear in the resultative construction).

                    Cross-class predictions #

                    source
                    theorem cos_classes_causative :
                    LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.bend.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.cooking.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true

                    All CoS classes (§45) participate in the causative/inchoative alternation.

                    source
                    theorem sprayLoad_locative :
                    LevinClass.sprayLoad.participatesIn DiathesisAlternation.locative = true

                    Spray/load participates in the locative alternation.

                    source
                    theorem give_dative :
                    LevinClass.give.participatesIn DiathesisAlternation.dative = true

                    Give class participates in the dative alternation.

                    source
                    theorem motion_no_causative :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.causativeInchoative = false ∧ LevinClass.inherentlyDirectedMotion.participatesIn DiathesisAlternation.causativeInchoative = false

                    Motion verbs (§51) don't participate in causative alternation (no causation component).

                    source
                    theorem contact_motion_conative :
                    LevinClass.hit.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.swat.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.poke.participatesIn DiathesisAlternation.conative = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.conative = true

                    Contact verbs predict conative alternation participation.

                    source
                    theorem touch_no_conative :
                    LevinClass.touch.participatesIn DiathesisAlternation.conative = false

                    Touch verbs lack motion → no conative despite having contact.

                    source
                    theorem cut_no_resultative_break_resultative :
                    LevinClass.cut.participatesIn DiathesisAlternation.resultative = false ∧ LevinClass.break_.participatesIn DiathesisAlternation.resultative = true

                    Cut participates in resultative; break does too (no instrumentSpec).

                    source
                    theorem causativeInchoative_implies_unaccusative :
                    LevinClass.break_.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.break_.predictsUnaccusative = true ∧ LevinClass.otherCoS.participatesIn DiathesisAlternation.causativeInchoative = true ∧ LevinClass.otherCoS.predictsUnaccusative = true

                    The causative/inchoative alternation implies the existence of an unaccusative variant: if a class participates in causative/inchoative, it predicts unaccusativity for the inchoative alternant.

                    Family classification theorems #

                    source
                    theorem canonical_diagnostics_families :
                    DiathesisAlternation.causativeInchoative.family = AlternationFamily.transitivity ∧ DiathesisAlternation.middle.family = AlternationFamily.transitivity ∧ DiathesisAlternation.conative.family = AlternationFamily.transitivity ∧ DiathesisAlternation.bodyPartPossessorAscension.family = AlternationFamily.vpInternal

                    The canonical diagnostics all belong to the transitivity or VP-internal families.

                    source
                    theorem passive_family :
                    DiathesisAlternation.verbalPassive.family = AlternationFamily.passive ∧ DiathesisAlternation.prepositionalPassive.family = AlternationFamily.passive

                    Passive alternations form their own family.

                    New alternation predictions #

                    source
                    theorem build_benefactive_materialProduct :
                    LevinClass.build.participatesIn DiathesisAlternation.benefactive = true ∧ LevinClass.build.participatesIn DiathesisAlternation.materialProduct = true

                    Build verbs participate in both benefactive and material/product alternations.

                    source
                    theorem substanceEmission_substanceSource :
                    LevinClass.substanceEmission.participatesIn DiathesisAlternation.substanceSource = true

                    Substance emission verbs participate in the substance/source alternation.

                    source
                    theorem eat_unspecifiedObject_devour_blocked :
                    LevinClass.eat.participatesIn DiathesisAlternation.unspecifiedObject = true ∧ LevinClass.devour.participatesIn DiathesisAlternation.unspecifiedObject = false

                    Eat verbs participate in the unspecified object alternation. Devour verbs do NOT — they require an expressed object.

                    source
                    theorem socialInteraction_reciprocal :
                    LevinClass.socialInteraction.participatesIn DiathesisAlternation.understoodReciprocalObject = true

                    Social interaction verbs show the understood reciprocal object alternation.

                    source
                    theorem existence_thereInsertion :
                    LevinClass.exist.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.appear.participatesIn DiathesisAlternation.thereInsertion = true

                    Existence and appearance verbs participate in there-insertion.

                    source
                    theorem existence_locativeInversion :
                    LevinClass.exist.participatesIn DiathesisAlternation.locativeInversion = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.locativeInversion = true

                    Existence and manner-of-motion verbs participate in locative inversion.

                    source
                    theorem unaccusative_diagnostics_align :
                    LevinClass.exist.predictsUnaccusative = true ∧ LevinClass.exist.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.exist.participatesIn DiathesisAlternation.locativeInversion = true ∧ LevinClass.appear.predictsUnaccusative = true ∧ LevinClass.appear.participatesIn DiathesisAlternation.thereInsertion = true ∧ LevinClass.appear.participatesIn DiathesisAlternation.locativeInversion = true

                    There-insertion and locative inversion align with unaccusativity.

                    source
                    theorem break_instrumentSubject_cut_blocked :
                    LevinClass.break_.participatesIn DiathesisAlternation.instrumentSubject = true ∧ LevinClass.cut.participatesIn DiathesisAlternation.instrumentSubject = false

                    Instrument subject alternation is predicted by external causation.

                    source
                    theorem instrumentSpec_blocks_ci_and_instrumentSubject (mc : MeaningComponents) (h : mc.instrumentSpec = true) :
                    mc.predictedAlternation DiathesisAlternation.causativeInchoative = false ∧ mc.predictedAlternation DiathesisAlternation.instrumentSubject = false

                    Instrument specification blocks both causative/inchoative and instrument subject alternations (same mechanism: instrument must be wielded by agent).

                    New alternation type predictions #

                    source
                    theorem mannerOfMotion_inducedAction :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.inducedAction = true

                    Manner-of-motion verbs participate in the induced action alternation (§1.1.2.2: Bill ran the horse).

                    source
                    theorem dress_understoodReflexive :
                    LevinClass.dress.participatesIn DiathesisAlternation.understoodReflexiveObject = true

                    Grooming verbs (§41) participate in the understood reflexive object alternation (§1.2.3: Bill washed himself / Bill washed).

                    source
                    theorem bodyProcess_understoodBodyPart :
                    LevinClass.bodyProcess.participatesIn DiathesisAlternation.understoodBodyPartObject = true

                    Body process verbs participate in the understood body-part object alternation (§1.2.2: Bill waved his hand / Bill waved).

                    source
                    theorem turn_totalTransformation :
                    LevinClass.turn.participatesIn DiathesisAlternation.totalTransformation = true

                    Turn/convert verbs participate in the total transformation alternation (§2.4.3: the witch turned the prince into a frog).

                    source
                    theorem mannerOfMotion_wayConstruction :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.wayConstruction = true

                    Manner-of-motion verbs participate in the way construction (§7.4: she elbowed her way through the crowd).

                    source
                    theorem mannerOfMotion_directionalPhrase :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.directionalPhrase = true

                    Manner-of-motion verbs participate in the directional phrase alternation (§7.8: she ran to the store).

                    source
                    theorem unergative_diagnostics :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.cognateObject = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true

                    Unergative diagnostics: manner-of-motion verbs participate in cognate object (§7.1: she laughed a bitter laugh) and prepositional passive (§5.2), both unergative diagnostics.

                    source
                    theorem mannerOfMotion_breadth :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.inducedAction = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.wayConstruction = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.directionalPhrase = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.cognateObject = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.locativeInversion = true

                    Manner-of-motion verbs are diagnostic workhorses: they participate in induced action, way construction, directional phrase, cognate object, prepositional passive, and locative inversion — 6 alternations from 4 different families.

                    Verbal passive coverage #

                    source
                    theorem verbalPassive_coverage :
                    LevinClass.break_.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.hit.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.put.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.give.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.build.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.murder.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.see.participatesIn DiathesisAlternation.verbalPassive = true ∧ LevinClass.amuse.participatesIn DiathesisAlternation.verbalPassive = true

                    Verbal passive is available across all major transitive class families: CoS, contact, putting, transfer, creation, killing, perception, psych.

                    source
                    theorem measure_no_verbalPassive :
                    LevinClass.measure.participatesIn DiathesisAlternation.verbalPassive = false

                    Measure verbs (§54) do NOT participate in verbal passive. This box weighs five pounds → ?Five pounds are weighed by this box. Stative relations between a measurer and a measure resist passivization.

                    source
                    theorem weather_no_verbalPassive :
                    LevinClass.weather.participatesIn DiathesisAlternation.verbalPassive = false

                    Weather verbs (§57) do NOT participate in verbal passive (no object to promote).

                    Prepositional passive and swarm coverage #

                    source
                    theorem prepositionalPassive_unergatives :
                    LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.bodyProcess.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.mannerOfSpeaking.participatesIn DiathesisAlternation.prepositionalPassive = true ∧ LevinClass.assumePosition.participatesIn DiathesisAlternation.prepositionalPassive = true

                    Prepositional passive aligns with unergativity: classes predicted unergative (manner-of-motion, body process) participate, while classes predicted unaccusative (exist, appear) generally don't. Note: exist verbs are exceptional — the house was lived in participates despite predict-unaccusative status.

                    source
                    theorem swarm_classes :
                    LevinClass.exist.participatesIn DiathesisAlternation.swarm = true ∧ LevinClass.mannerOfMotion.participatesIn DiathesisAlternation.swarm = true ∧ LevinClass.bodyInternalMotion.participatesIn DiathesisAlternation.swarm = true

                    The swarm alternation applies to existence and manner-of-motion verbs (§2.3.4: bees swarmed in the garden / the garden swarmed with bees).