Documentation

Linglib.Studies.Levin1993

Diathesis Alternation Bridge [Lev93] #

Connects the alternation judgment rows in Data/Examples/Levin1993.json to the LevinClass.participatesIn prediction function, the Fragment verb entries, and [Dow91]'s proto-role account of the three verb classes.

The verbs break, cut, hit, touch form Levin's §0.4 diagnostic quadruple (pp. 5–10): each participates in a distinct subset of the causative/inchoative, middle, conative, and body-part possessor ascension alternations.

VerbClassCIMidConBPPA
break45.1✓✓✗✗
cut21.1✗✓✓✓
hit18.1✗✗✓✓
touch20✗✗✗✓

Main declarations #

source
def Levin1993.classOfString :
String → Option Semantics.Lexical.LevinClass

Map a row's levin_class section string to the curated LevinClass enum. Subclasses collapse to their enum representative (51.3.2 run verbs → mannerOfMotion; 47.5.1 swarm verbs → the §47 existence family's exist; 48.1.1 → appear; 41.1.1 dress verbs → dress; 36.3 → socialInteraction; 54.1 register verbs → measure). Classes outside the enum's grain (40.2 nonverbal expression, 40.3.2 wink, 40.4 snooze, 37.5 talk) map to none.

Equations
Instances For
    source
    def Levin1993.alternationOfString :
    String → Option Semantics.Lexical.DiathesisAlternation

    Map a row's alternation tag to the curated enum.

    Equations
    Instances For
      source
      def Levin1993.classOf (e : Data.Examples.LinguisticExample) :
      Option Semantics.Lexical.LevinClass

      Levin class recorded on a row.

      Equations
      Instances For
        source
        def Levin1993.alternationOf (e : Data.Examples.LinguisticExample) :
        Option Semantics.Lexical.DiathesisAlternation

        Alternation recorded on a row.

        Equations
        Instances For
          source
          def Levin1993.observed (e : Data.Examples.LinguisticExample) :
          Option Bool

          Categorical participation recorded on a row; none for marginal judgments (the participatesIn profile is Boolean).

          Equations
          Instances For
            source
            def Levin1993.agreesWithPrediction (e : Data.Examples.LinguisticExample) :
            Bool

            A row agrees with LevinClass.participatesIn (vacuously, if its class or alternation is unrepresentable or its judgment is marginal).

            Equations
            Instances For
              source
              theorem Levin1993.participation_matches_prediction :
              Examples.all.all agreesWithPrediction = true

              Every categorical row with a representable class and alternation matches the participatesIn prediction. In particular the CI rule blocks cut via instrument specification (Levin pp. 9–10: an inherently specified instrument requires an agent, blocking the agentless inchoative).

              source
              theorem Levin1993.alternations_all_representable :
              (Examples.all.all fun (e : Data.Examples.LinguisticExample) => (alternationOf e).isSome) = true

              Every row's alternation tag is one of the curated alternations.

              source
              theorem Levin1993.unrepresentable_classes :
              List.map (fun (x : Data.Examples.LinguisticExample) => x.id) (List.filter (fun (e : Data.Examples.LinguisticExample) => (classOf e).isNone) Examples.all) = ["levin1993_ubpo_wave", "levin1993_co_laugh", "levin1993_pp_sleep", "levin1993_pp_talk"]

              Exactly four rows carry Levin classes outside the curated enum's grain: wave (40.3.2 wink), laugh (40.2 nonverbal expression), sleep (40.4 snooze), talk (37.5). These are excluded from participation_matches_prediction by classOf.

              source
              def Levin1993.quadruplePattern (rows : List Data.Examples.LinguisticExample) :
              List (Option Bool)

              Participation pattern of a verb across the four §0.4 alternations (CI, middle, conative, BPPA).

              Equations
              Instances For
                source
                theorem Levin1993.quadruple_patterns_distinct :
                List.Pairwise (fun (x1 x2 : List (Option Bool)) => x1 ≠ x2) [quadruplePattern [Examples.ci_break, Examples.mid_break, Examples.con_break, Examples.bppa_break], quadruplePattern [Examples.ci_cut, Examples.mid_cut, Examples.con_cut, Examples.bppa_cut], quadruplePattern [Examples.ci_hit, Examples.mid_hit, Examples.con_hit, Examples.bppa_hit], quadruplePattern [Examples.ci_touch, Examples.mid_touch, Examples.con_touch, Examples.bppa_touch]]

                Each verb of the quadruple shows a pairwise distinct pattern across the four alternations — Levin's §0.4 table has no repeated rows, so the four verbs instantiate four distinct verb classes.

                Each Fragment verb entry's levinClass matches the class recorded on its alternation rows.

                source
                theorem Levin1993.break_class_matches :
                English.Predicates.Verbal.break_.levinClass = classOf Examples.ci_break
                source
                theorem Levin1993.cut_class_matches :
                English.Predicates.Verbal.cut.levinClass = classOf Examples.ci_cut
                source
                theorem Levin1993.hit_class_matches :
                English.Predicates.Verbal.hit.levinClass = classOf Examples.ci_hit
                source
                theorem Levin1993.touch_class_matches :
                English.Predicates.Verbal.touch.levinClass = classOf Examples.ci_touch
                source
                theorem Levin1993.push_class_matches :
                English.Predicates.Verbal.push.levinClass = classOf Examples.con_push
                source
                theorem Levin1993.spray_class_matches :
                English.Predicates.Verbal.spray.levinClass = classOf Examples.loc_spray
                source
                theorem Levin1993.load_class_matches :
                English.Predicates.Verbal.load.levinClass = classOf Examples.loc_load
                source
                theorem Levin1993.give_class_matches :
                English.Predicates.Verbal.give.levinClass = classOf Examples.dat_give
                source
                theorem Levin1993.send_class_matches :
                English.Predicates.Verbal.send.levinClass = classOf Examples.dat_send

                [Dow91] §9.3 derives the alternation behavior of the spray/load, break, and hit classes from the distribution of the change-of-state entailment across non-subject arguments: symmetric CoS permits alternation, asymmetric CoS fixes the CoS argument as direct object. Levin's judgment rows confirm each prediction.

                source
                theorem Levin1993.dowty_sprayLoad_symmetry_matches_data :
                Dowty1991.cosSymmetric Dowty1991.sprayLoadTheme Dowty1991.sprayLoadLocation = true ∧ observed Examples.loc_spray = some true ∧ observed Examples.loc_load = some true

                Spray/load: CoS is symmetric across theme and location, predicting the locative alternation — attested for both spray and load.

                source
                theorem Levin1993.dowty_break_asymmetry_matches_prediction :
                Dowty1991.cosSymmetric Dowty1991.breakDirectObject Dowty1991.breakInstrument = false ∧ Semantics.Lexical.LevinClass.break_.participatesIn Semantics.Lexical.DiathesisAlternation.locative = false

                Break: CoS is asymmetric (direct object vs. instrument), fixing the CoS argument as direct object — break lacks the locative alternation.

                source
                theorem Levin1993.dowty_hit_class_matches_data :
                Dowty1991.cosSymmetric Dowty1991.hitArg1 Dowty1991.hitArg2 = true ∧ observed Examples.con_hit = some true ∧ observed Examples.ci_hit = some false ∧ observed Examples.mid_hit = some false

                Hit: both arguments symmetrically lack CoS — the conative is attested while the CoS-sensitive causative/inchoative and middle are blocked.