Documentation

Linglib.Syntax.ConstructionGrammar.Licensing

Constructional licensing #

A constructional grammar licenses a structure when every constituent in it instantiates some construction, as for Sag and for Goldberg. Licenses is the local version of that relation over constituency trees whose leaves are word tokens: every internal node's daughters instantiate, slot by slot, the typed form of some construction of an inventory (FormMatches), and words are licensed lexically. A node is licensed by the form of one construction alone, without the constraints it inherits from the constructions above it in a network.

Matching reads each word's form, part of speech and features off the token itself. A headed filler is checked against the immediate daughters, a flat approximation of headedness, and a semantic filler, which the form cannot check, matches anything. Of the slot constraints only negMinus bears on the daughter itself: it rejects a daughter of negative polarity, or one with such a word among its daughters (SlotConstraint.Allows).

Main declarations #

References #

source
def ConstructionGrammar.IsWord (form : String) (cat : UD.UPOS) :
PhraseStructure.Tree Unit Morphology.Word → Prop

A tree is the word of the given form and part of speech.

Equations
Instances For
    source
    @[instance_reducible]
    instance ConstructionGrammar.instDecidableIsWord (form : String) (cat : UD.UPOS) (t : PhraseStructure.Tree Unit Morphology.Word) :
    Decidable (IsWord form cat t)
    Equations
    source
    def ConstructionGrammar.IsNegative :
    PhraseStructure.Tree Unit Morphology.Word → Prop

    A tree is a word of negative polarity.

    Equations
    Instances For
      source
      @[instance_reducible]
      instance ConstructionGrammar.instDecidablePredTreeUnitWordIsNegative :
      DecidablePred IsNegative
      Equations
      source
      def ConstructionGrammar.SlotFiller.Matches :
      SlotFiller String → PhraseStructure.Tree Unit Morphology.Word → Prop

      A daughter fills a fixed slot when it is a word of that form, an open slot when it is a word of its part of speech, a phrasal slot when it is any phrase, a node or an adjunction structure, and a headed slot when it is a constituent with its head word, of its part of speech, among the daughters.

      Equations
      Instances For
        source
        @[instance_reducible]
        instance ConstructionGrammar.instDecidableMatches (f : SlotFiller String) (t : PhraseStructure.Tree Unit Morphology.Word) :
        Decidable (f.Matches t)
        Equations
        source
        def ConstructionGrammar.SlotConstraint.Allows :
        SlotConstraint → PhraseStructure.Tree Unit Morphology.Word → Prop

        A daughter respects a slot constraint. negMinus forbids negative polarity, on the daughter or on a word among its daughters; locMinus and refEmpty concern the slot's external syntax and semantics and are not checkable against the daughter itself.

        Equations
        Instances For
          source
          @[instance_reducible]
          instance ConstructionGrammar.instDecidableAllows (c : SlotConstraint) (t : PhraseStructure.Tree Unit Morphology.Word) :
          Decidable (c.Allows t)
          Equations
          source
          def ConstructionGrammar.Slot.Admits (s : Slot String) (t : PhraseStructure.Tree Unit Morphology.Word) :
          Prop

          A daughter instantiates a slot when it fills the slot and respects its constraints.

          Equations
          Instances For
            source
            @[instance_reducible]
            instance ConstructionGrammar.instDecidableAdmits (s : Slot String) (t : PhraseStructure.Tree Unit Morphology.Word) :
            Decidable (s.Admits t)
            Equations
            source
            def ConstructionGrammar.FormMatches (form : TypedForm String) (ts : List (PhraseStructure.Tree Unit Morphology.Word)) :
            Prop

            A daughter sequence instantiates a typed form, slot by slot.

            Equations
            Instances For
              source
              @[instance_reducible]
              instance ConstructionGrammar.instDecidableFormMatches (form : TypedForm String) (ts : List (PhraseStructure.Tree Unit Morphology.Word)) :
              Decidable (FormMatches form ts)
              Equations
              source
              def ConstructionGrammar.LicensedLocally {Sem : Type u_1} (cxns : List (Construction Sem)) :
              PhraseStructure.Tree Unit Morphology.Word → Prop

              A node is licensed locally when a word, or when its daughters instantiate the form of some construction of the inventory; traces and binders are not.

              Equations
              Instances For
                source
                @[instance_reducible]
                instance ConstructionGrammar.instDecidableLicensedLocally {Sem : Type u_1} (cxns : List (Construction Sem)) (t : PhraseStructure.Tree Unit Morphology.Word) :
                Decidable (LicensedLocally cxns t)
                Equations
                source
                def ConstructionGrammar.Licenses {Sem : Type u_1} (cxns : List (Construction Sem)) (t : PhraseStructure.Tree Unit Morphology.Word) :
                Prop

                The inventory licenses a tree when every constituent in it is licensed locally.

                Equations
                Instances For
                  source
                  @[instance_reducible]
                  instance ConstructionGrammar.instDecidableLicenses {Sem : Type u_1} (cxns : List (Construction Sem)) (t : PhraseStructure.Tree Unit Morphology.Word) :
                  Decidable (Licenses cxns t)
                  Equations