Documentation

Linglib.Semantics.ArgumentStructure.LevinClass.Basic

The verb classes of Levin 1993 #

LevinClass enumerates the verb classes of Part II of Levin's English Verb Classes and Alternations, one constructor for each class page with a member list, with the section number and title the book prints for it. The classes' property tables are in Properties.lean, their member lists in Members.lean and their root entailments in RootEntailment.lean; the levinClasses field of a Verb entry carries the classes listing it. A class may also carry a default argument-structure template, from which a verb entry's argument profiles are derived.

Implementation notes #

The section numbers and titles were checked against the book's section headings. The maxRecDepth setting on the inductive serves deriving Fintype, whose handler for enumerations checks its list of the 191 constructors by rfl.

References #

source
inductive ArgumentStructure.LevinClass :
Type

The verb classes of [Lev93] Part II, one constructor per class with a member list, named by the class's head word or Levin's label, with the section number and the first members of the class's list.

Instances For
    source
    @[instance_reducible]
    instance ArgumentStructure.instDecidableEqLevinClass :
    DecidableEq LevinClass
    Equations
    source
    def ArgumentStructure.instReprLevinClass.repr :
    LevinClass → ℕ → Std.Format
    Instances For
      source
      @[instance_reducible]
      instance ArgumentStructure.instReprLevinClass :
      Repr LevinClass
      Equations
      source
      @[instance_reducible]
      instance ArgumentStructure.instFintypeLevinClass :
      Fintype LevinClass
      Equations
      • One or more equations did not get rendered due to their size.
      source
      def ArgumentStructure.LevinClass.numberString :
      LevinClass → String

      The section number as the book prints it.

      Equations
      Instances For
        source
        def ArgumentStructure.LevinClass.ofNumberString? (s : String) :
        Option LevinClass

        The class whose section number the book prints as s, the inverse of numberString.

        Equations
        Instances For
          source
          def ArgumentStructure.LevinClass.name :
          LevinClass → String

          Levin's title of the class.

          Equations
          Instances For

            Templates #

            Each class realizes an argument-structure template, a RoleList, from which Verb.Basic derives a verb entry's default argument profiles; classes whose template has not been determined map to none.

            source
            def ArgumentStructure.LevinClass.roleList :
            LevinClass → Option RoleList

            The argument-structure template a class realizes, none where it has not been determined.

            Equations
            Instances For

              Profiles #

              source
              def ArgumentStructure.LevinClass.subjectProfile (c : LevinClass) :
              Option EntailmentProfile

              The entailment profile of the subject in a class's template.

              Equations
              Instances For
                source
                def ArgumentStructure.LevinClass.objectProfile (c : LevinClass) :
                Option EntailmentProfile

                The entailment profile of the object in a class's template, if it has one.

                Equations
                Instances For
                  source
                  def ArgumentStructure.agree :
                  Option (Option EntailmentProfile) → Option (Option EntailmentProfile) → Option (Option EntailmentProfile)

                  Two votes on a profile combine by agreement, where none abstains and some none records a disagreement.

                  Equations
                  Instances For
                    source
                    instance ArgumentStructure.instCommutativeOptionEntailmentProfileAgree :
                    Std.Commutative agree
                    source
                    instance ArgumentStructure.instAssociativeOptionEntailmentProfileAgree :
                    Std.Associative agree
                    source
                    def ArgumentStructure.LevinClass.commonProfile (f : LevinClass → Option EntailmentProfile) (s : Finset LevinClass) :
                    Option EntailmentProfile

                    The profile the classes assigning one agree on, none when none does or they disagree.

                    Equations
                    Instances For
                      source
                      theorem ArgumentStructure.roleList_not_asp_reversed {c : LevinClass} {r : RoleList} {o : EntailmentProfile} (hr : c.roleList = some r) (ho : r.objectProfile = some o) :
                      ¬OutranksForSubject o r.subjectProfile

                      In no class's template does the object outrank the subject under [Dow91]'s Argument Selection Principle, as [LRH05] present it. Where dominance is strict the principle derives the stored linking; at the psych doublets like and please (Dowty1991.psychStative_alternation) neither argument outranks the other, and the linking is a lexical choice the template underdetermines.