Documentation

Linglib.Semantics.Root.Defs

Verbal roots #

A verbal root of [beavers-koontz-garboden-2020] is a bundle of lexical entailments (§5.2.1), each of one of the four kinds of Root.Kind. Root carries a finite set of such atoms, its position with respect to the verbalizing head v, and its within-class content. Its kind signature Root.kinds is the image of the atoms under Entailment.kind, and Root.closedKinds completes it under the collocational restrictions (Root.Kinds.close). A root composes with v either as its complement, the result position of change-of-state roots such as √flat and √drown, or adjoined to it as a modifier, the manner position of √jog and √hand (§4.5.3–4.5.4); position is the second coordinate of the book's root typology (§5.4.1, (12)), and an adjoined root escapes both the scope of restitutive again (§4.5.4) and the deletion site of verbal VP ellipsis ([kalyakin-2026] §2.2). Participant entailments are the separate linking layer ArgumentStructure.EntailmentProfile. A root may also be annotated with the coordinates [coon-2019] classifies root classes by, its valency, semantic type, and whether it combines with transitive Voice.

Main declarations #

References #

Atoms #

source
inductive Semantics.Root.Entailment :
Type

A lexical entailment of a verbal root, labelled by the state, manner, or result it names ([beavers-koontz-garboden-2020] §5.4.1).

  • state (label : String) : Entailment

    The root describes the labelled state.

  • manner (label : String) : Entailment

    The root describes an action of the labelled manner.

  • result (label : String) : Entailment

    The root entails a change into the labelled state.

  • cause : Entailment

    The root entails causation.

Instances For
    source
    def Semantics.Root.instDecidableEqEntailment.decEq (x✝ x✝¹ : Entailment) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Semantics.Root.instDecidableEqEntailment :
      DecidableEq Entailment
      Equations
      source
      def Semantics.Root.instReprEntailment.repr :
      Entailment → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        @[instance_reducible]
        instance Semantics.Root.instReprEntailment :
        Repr Entailment
        Equations
        source
        def Semantics.Root.Entailment.kind :
        Entailment → Kind

        The kind of an atom, forgetting its label.

        Equations
        Instances For

          Position #

          source
          inductive Semantics.Root.Position :
          Type

          The position in which a verbal root composes with v.

          • complement : Position

            The complement of v, the result position.

          • adjoined : Position

            Adjoined to v as a modifier, the manner position.

          Instances For
            source
            @[instance_reducible]
            instance Semantics.Root.instDecidableEqPosition :
            DecidableEq Position
            Equations
            source
            @[instance_reducible]
            instance Semantics.Root.instFintypePosition :
            Fintype Position
            Equations
            • One or more equations did not get rendered due to their size.
            source
            def Semantics.Root.instReprPosition.repr :
            Position → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[instance_reducible]
              instance Semantics.Root.instReprPosition :
              Repr Position
              Equations

              Roots #

              source
              structure Semantics.Root :
              Type

              A verbal root, with its lexical entailments, position, and content.

              • name : String

                The root form, "" when the root is carried anonymously by a verb whose citation form names it.

              • entailments : Finset Entailment

                The root's atoms, ∅ where its structural content is unannotated.

              • position : Option Position

                The position in which the root composes with v, where annotated.

              • content : Content

                Within-class content ([spalek-mcnally-2026], [majid-boster-bowerman-2008]); {} leaves every dimension unconstrained.

              • valency : Option ArgumentStructure.Valency

                The core-argument positions the root introduces, where annotated ([coon-2019]).

              • denotationType : Option Composition.Ty

                The root's semantic type, where annotated ([coon-2019] (3)).

              • licensesTransitiveVoice : Bool

                Whether the root combines with the transitive-forming v ~ Voice head that merges an agent, the coordinate separating [coon-2019]'s √TV from its unaccusative √ITV (§3.3).

              Instances For
                source
                def Semantics.instDecidableEqRoot.decEq (x✝ x✝¹ : Root) :
                Decidable (x✝ = x✝¹)
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For
                  source
                  @[instance_reducible]
                  instance Semantics.instDecidableEqRoot :
                  DecidableEq Root
                  Equations
                  source
                  @[instance_reducible]
                  instance Semantics.instReprRoot :
                  Repr Root

                  A Repr showing the name, atom count, and position, since Finset has only an unsafe one.

                  Equations
                  source
                  def Semantics.Root.kinds (r : Root) :
                  Kinds

                  The kind signature of a root, the kinds of its atoms.

                  Equations
                  Instances For
                    source
                    @[simp]
                    theorem Semantics.Root.mem_kinds {r : Root} {k : Kind} :
                    k ∈ r.kinds ↔ ∃ a ∈ r.entailments, a.kind = k
                    source
                    def Semantics.Root.closedKinds (r : Root) :
                    Kinds

                    The kind signature completed under the collocational restrictions (Root.Kinds.close).

                    Equations
                    Instances For
                      source
                      theorem Semantics.Root.kinds_subset_closedKinds (r : Root) :
                      r.kinds ⊆ r.closedKinds
                      source
                      theorem Semantics.Root.closedKinds_wellFormed (r : Root) :
                      r.closedKinds.WellFormed
                      source
                      def Semantics.Root.changeType (r : Root) :
                      Option ChangeType

                      The change type of a root, read off its closed signature ([beavers-etal-2021]).

                      Equations
                      Instances For