Documentation

Linglib.Semantics.ArgumentStructure.Root.Defs

Atomic Lexical Entailments and Roots #

Lexical entailments are the atomic claims a verbal root makes about the events it describes and the participants in those events. Following [BKG20], we treat these as structured atoms rather than as a fixed feature vector: a root is a finite collection of such atoms, and its kind signature (Root.Kinds) is the derived set of kinds its atoms realize — exposing the Bifurcation Thesis of Roots and Manner/Result Complementarity as testable conjectures rather than architectural commitments.

Main declarations #

Atomic entailments #

source
inductive Verb.LexEntailment :
Type

An atomic structural claim a verbal root makes — one of the four B&K-G entailment kinds (state, manner, result, cause). The three contentful kinds carry a label; hasCause is nullary. LexEntailment.kind projects the kind each realizes.

Participant/proto-role entailments (volition, sentience, movement, affectedness, …) are deliberately not modeled here: they are an orthogonal, linking-relevant layer carried by ArgumentStructure.EntailmentProfile.

Instances For
    source
    def Verb.instDecidableEqLexEntailment.decEq (x✝ x✝¹ : LexEntailment) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[instance_reducible]
      instance Verb.instDecidableEqLexEntailment :
      DecidableEq LexEntailment
      Equations
      source
      @[instance_reducible]
      instance Verb.instReprLexEntailment :
      Repr LexEntailment
      Equations
      source
      def Verb.instReprLexEntailment.repr :
      LexEntailment → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Verb.LexEntailment.kind :
        LexEntailment → Option LexKind

        The B&K-G kind an atom realizes. Total — every atom has a kind — but kept Option-valued for the closure API (Closure.lean), which quantifies over a.kind = some k.

        Equations
        Instances For

          Roots #

          source
          structure Verb.Root :
          Type

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

          The set 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 Closure.lean.

          • name : String

            The root form; "" for an unnamed annotation (e.g. a quality-profile-only root carried by a verb whose root form is its citation form).

          • entailments : Finset LexEntailment

            The B&KG structural-entailment atoms; ∅ where the root's structural content has not been annotated (its kinds is then uninformative).

          • profile : Profile

            Within-class graded quality dimensions ([SMcN26], [MBB08]); {} (all unconstrained) by default.

          Instances For
            source
            def Verb.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 Verb.instDecidableEqRoot :
              DecidableEq Root
              Equations
              source
              @[instance_reducible]
              instance Verb.instReprRoot :
              Repr Root

              Finset carries no Repr, so Root cannot deriving Repr; we supply one by hand so Verb can deriving Repr over its root field. It shows name and profile in full plus the entailments cardinality — the entailment set itself has no computable Repr (Finset/Multiset would need a LinearOrder on the elements to render), but this already distinguishes roots that differ in profile, which the old name-only Repr collapsed.

              BEq/LawfulBEq need no hand-rolled instance: both come from the derived DecidableEq (line above) via the global instBEqOfDecidableEq.

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

              The derived kind signature of a root: the set of kinds its atoms realize.

              Equations
              Instances For
                source
                theorem Verb.Root.mem_kinds {r : Root} {k : LexKind} :
                k ∈ r.kinds ↔ ∃ a ∈ r.entailments, a.kind = some k
                source
                @[reducible, inline]
                abbrev Verb.Root.HasState (r : Root) :
                Prop

                The root entails attribution of some state. abbrev (not def) so Decidable/simp/decide see through to the underlying Finset membership without per-predicate boilerplate.

                Equations
                Instances For
                  source
                  @[reducible, inline]
                  abbrev Verb.Root.HasManner (r : Root) :
                  Prop

                  The root specifies some manner.

                  Equations
                  Instances For
                    source
                    @[reducible, inline]
                    abbrev Verb.Root.HasResult (r : Root) :
                    Prop

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

                    Equations
                    Instances For
                      source
                      @[reducible, inline]
                      abbrev Verb.Root.HasCause (r : Root) :
                      Prop

                      The root entails causation.

                      Equations
                      Instances For

                        The closed signature #

                        source
                        def Verb.Root.closedKinds (r : Root) :
                        Kinds

                        The closed kind signature: the collocational closure (Root.Kinds.close) of the derived signature. Both [BKG20] restrictions (result→state and cause→result) hold of closed signatures by construction.

                        Equations
                        Instances For
                          source
                          theorem Verb.Root.closedKinds_wellFormed (r : Root) :
                          r.closedKinds.WellFormed
                          source
                          theorem Verb.Root.kinds_le_closed (r : Root) :
                          r.kinds ⊆ r.closedKinds