Documentation

Linglib.Theories.Semantics.Lexical.Roots.Basic

Atomic Lexical Entailments and Roots #

@cite{beavers-koontz-garboden-2020}

Lexical entailments are the atomic claims a verbal root makes about the events it describes and the participants in those events. Following @cite{beavers-koontz-garboden-2020}, we treat these as structured atoms rather than as a fixed feature vector.

A root is a finite collection of such atoms. The root's B&K-G feature signature (±state, ±manner, ±result, ±cause) is then a derived predicate over the entailment set, not a separately stipulated classification — exposing both the Bifurcation Thesis of Roots and Manner/Result Complementarity (@cite{rappaport-hovav-levin-2010}) as testable conjectures rather than architectural commitments.

Relation to existing infrastructure #

source
inductive Semantics.Lexical.Roots.LexEntailment :
Type

An atomic claim a root can make. The four B&K-G features (±state, ±manner, ±result, ±cause) correspond to the kinds of atoms present in a root's entailment set.

The remaining atoms (volitional, sentient, motion, contact) cover Dowty's proto-role components that are independent of the state/manner/result/cause cut.

  • hasState (label : String) : LexEntailment

    Attributes a static property (state-kind atom).

  • hasManner (label : String) : LexEntailment

    Specifies the manner in which the action is performed.

  • becomesState (label : String) : LexEntailment

    Entails change of state to the labelled result.

  • hasCause : LexEntailment

    Entails a causing event. Nullary because B&K-G's typology is neutral about what causes — only that there is a cause. The cause-type distinction (internal vs external, @cite{bohnemeyer-2004}) is carried separately by Features.EventStructure.CausationType.

  • volitional : LexEntailment

    The agent acts intentionally.

  • sentient : LexEntailment

    The agent is sentient.

  • motion : LexEntailment

    An entity changes location.

  • contact : LexEntailment

    Two entities are in physical contact.

Instances For
    source
    def Semantics.Lexical.Roots.instDecidableEqLexEntailment.decEq (x✝ x✝¹ : LexEntailment) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance Semantics.Lexical.Roots.instDecidableEqLexEntailment :
      DecidableEq LexEntailment
      Equations
      source
      @[implicit_reducible]
      instance Semantics.Lexical.Roots.instReprLexEntailment :
      Repr LexEntailment
      Equations
      source
      def Semantics.Lexical.Roots.instReprLexEntailment.repr :
      LexEntailment → Nat → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Semantics.Lexical.Roots.LexEntailment.isState :
        LexEntailment → Prop

        Is the atom a state-attribution?

        Equations
        Instances For
          source
          def Semantics.Lexical.Roots.LexEntailment.isManner :
          LexEntailment → Prop

          Is the atom a manner specification?

          Equations
          Instances For
            source
            def Semantics.Lexical.Roots.LexEntailment.isBecome :
            LexEntailment → Prop

            Is the atom a change-of-state entailment?

            Equations
            Instances For
              source
              def Semantics.Lexical.Roots.LexEntailment.isCause :
              LexEntailment → Prop

              Is the atom a causation entailment?

              Equations
              Instances For
                source
                structure Semantics.Lexical.Roots.Root :
                Type

                A verbal root: a name and a list of atomic entailments it imposes.

                The list is the root's base entailment set — the atoms asserted directly. A closure operation (B&K-G's networks of entailments where one atom may entail another) is layered on top in Roots/Closure.lean.

                Instances For
                  source
                  @[implicit_reducible]
                  instance Semantics.Lexical.Roots.instDecidableEqRoot :
                  DecidableEq Root
                  Equations
                  source
                  def Semantics.Lexical.Roots.instDecidableEqRoot.decEq (x✝ x✝¹ : Root) :
                  Decidable (x✝ = x✝¹)
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    @[implicit_reducible]
                    instance Semantics.Lexical.Roots.instReprRoot :
                    Repr Root
                    Equations
                    source
                    def Semantics.Lexical.Roots.instReprRoot.repr :
                    Root → Nat → Std.Format
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For
                      source
                      def Semantics.Lexical.Roots.Root.hasState (r : Root) :
                      Bool

                      The root entails attribution of some state.

                      Equations
                      Instances For
                        source
                        def Semantics.Lexical.Roots.Root.hasManner (r : Root) :
                        Bool

                        The root specifies some manner.

                        Equations
                        Instances For
                          source
                          def Semantics.Lexical.Roots.Root.hasResult (r : Root) :
                          Bool

                          The root entails some change of state (B&K-G "result").

                          Equations
                          Instances For
                            source
                            def Semantics.Lexical.Roots.Root.hasCause (r : Root) :
                            Bool

                            The root entails causation.

                            Equations
                            Instances For