Documentation

Linglib.Theories.Syntax.ConstructionGrammar.Slot

Typed Slot-Filler Representation #

@cite{dunn-2025} @cite{kay-fillmore-1999} @cite{fillmore-kay-oconnor-1988} @cite{goldberg-1995}

Constructions are sequences of slots, where each slot is either fixed (a specific lexeme), open (any word of a given syntactic category), or headed (a phrase headed by a specific lexeme). @cite{dunn-2025}'s variationist CxG treats abstraction as continuous (the proportion of open slots). @cite{kay-fillmore-1999} add grammatical functions, coreference indices, and syntactic constraints to the slot representation.

Architecture #

Slot Lex combines six pieces of information into one type:

FieldTypeSource
fillerSlotFiller Lex@cite{dunn-2025} + @cite{kay-fillmore-1999} (fixed/open/headed)
roleOption String@cite{goldberg-1995} (semantic role)
isHeadBoolArgumentStructure.lean
gfOption GramFunction@cite{kay-fillmore-1999} (grammatical function)
refIdxOption RefIndex@cite{kay-fillmore-1999} (coreference index)
constraintsList SlotConstraint@cite{kay-fillmore-1999} (syntactic constraints)

TypedForm Lex := List (Slot Lex) is the typed form side of a construction.

The existing ConstructionSlot (which only represents open slots) embeds into Slot String via ConstructionSlot.toSlot (§3).

Key definitions #

Verification theorems live in Phenomena/Constructions/Bridge/SlotVerification.lean.

source
inductive ConstructionGrammar.SlotFiller (Lex : Type) :
Type

A slot's filler: the representation level of slot content.

@cite{dunn-2025} distinguishes three representation levels for slot content:

  • LEX (lexeme): a specific word form → fixed "must"
  • SYN (syntactic): any word of a given POS category → open_.VERB
  • SEM+ (semantic): any expression satisfying a semantic constraint → semantic "animate" (any animate NP)

@cite{kay-fillmore-1999} add headed phrases: headed "doing".VERB (a VP headed by doing). These are LEX-level (they fix the head lexeme).

Parameterized over Lex (the lexeme type) so the same representation works for strings, morphemes, or phonological forms.

  • fixed {Lex : Type} : Lex → SlotFiller Lex
  • open_ {Lex : Type} : UD.UPOS → SlotFiller Lex
  • headed {Lex : Type} : Lex → UD.UPOS → SlotFiller Lex

    A phrase headed by a specific lexeme. headed "doing".VERB means "a VP headed by doing" — the slot is phrasal, not the bare word. Contrast with fixed "doing".

  • semantic {Lex : Type} : String → SlotFiller Lex

    A semantically constrained slot (@cite{dunn-2025}, SEM+ level). semantic "animate" means any expression satisfying the semantic property "animate". More abstract than SYN (category-based): the filler is constrained by meaning, not by syntactic category.

Instances For
    source
    @[implicit_reducible]
    instance ConstructionGrammar.instDecidableEqSlotFiller {Lex✝ : Type} [DecidableEq Lex✝] :
    DecidableEq (SlotFiller Lex✝)
    Equations
    source
    def ConstructionGrammar.instDecidableEqSlotFiller.decEq {Lex✝ : Type} [DecidableEq Lex✝] (x✝ x✝¹ : SlotFiller Lex✝) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      source
      @[implicit_reducible]
      instance ConstructionGrammar.instReprSlotFiller {Lex✝ : Type} [Repr Lex✝] :
      Repr (SlotFiller Lex✝)
      Equations
      source
      def ConstructionGrammar.instReprSlotFiller.repr {Lex✝ : Type} [Repr Lex✝] :
      SlotFiller Lex✝ → ℕ → Std.Format
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def ConstructionGrammar.SlotFiller.isOpen {Lex : Type} :
        SlotFiller Lex → Bool

        Is this slot open (not lexically fixed)?

        Both open_ (SYN) and semantic (SEM+) slots count as open for abstraction level computation. headed slots do not: they fix the head lexeme even though the phrase is open.

        Equations
        Instances For
          source
          inductive ConstructionGrammar.GramFunction :
          Type

          Grammatical function of a valence member (@cite{kay-fillmore-1999}, Figure 12). Distinct from semantic role: a subject (gf) can be an agent, theme, or experiencer (role).

          Instances For
            source
            @[implicit_reducible]
            instance ConstructionGrammar.instDecidableEqGramFunction :
            DecidableEq GramFunction
            Equations
            source
            @[implicit_reducible]
            instance ConstructionGrammar.instReprGramFunction :
            Repr GramFunction
            Equations
            source
            def ConstructionGrammar.instReprGramFunction.repr :
            GramFunction → ℕ → Std.Format
            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              @[reducible, inline]
              abbrev ConstructionGrammar.RefIndex :
              Type

              Referential index for cross-slot coreference constraints. Slots sharing the same RefIndex must have their semantic values unified. @cite{kay-fillmore-1999} use #1, #2, etc. to express identity between a construction's semantic arguments and its valence members' semantic values.

              Equations
              Instances For
                source
                inductive ConstructionGrammar.SlotConstraint :
                Type

                Syntactic constraint on a slot (@cite{kay-fillmore-1999}, Figure 12).

                Instances For
                  source
                  @[implicit_reducible]
                  instance ConstructionGrammar.instDecidableEqSlotConstraint :
                  DecidableEq SlotConstraint
                  Equations
                  source
                  @[implicit_reducible]
                  instance ConstructionGrammar.instReprSlotConstraint :
                  Repr SlotConstraint
                  Equations
                  source
                  def ConstructionGrammar.instReprSlotConstraint.repr :
                  SlotConstraint → ℕ → Std.Format
                  Equations
                  • One or more equations did not get rendered due to their size.
                  Instances For
                    source
                    structure ConstructionGrammar.Slot (Lex : Type) :
                    Type

                    A slot in a construction: filler content + semantic role + headedness.

                    Subsumes ConstructionSlot (which only represents open slots) by adding the fixed/open distinction via SlotFiller. Fixed slots (like "let" in let alone) have role := none since they carry no independent semantic role.

                    • filler : SlotFiller Lex

                      What fills this slot: a specific lexeme, open category, or headed phrase

                    • role : Option String

                      Semantic role label (agent, theme, etc.), if any

                    • isHead : Bool

                      Whether this slot is the head of the construction

                    • gf : Option GramFunction

                      Grammatical function (subj, comp, obj, pred) — @cite{kay-fillmore-1999}

                    • refIdx : Option RefIndex

                      Coreference index: slots sharing an index have unified semantics

                    • constraints : List SlotConstraint

                      Syntactic constraints on this slot ([loc -], [neg -], [ref ∅])

                    Instances For
                      source
                      @[implicit_reducible]
                      instance ConstructionGrammar.instDecidableEqSlot {Lex✝ : Type} [DecidableEq Lex✝] :
                      DecidableEq (Slot Lex✝)
                      Equations
                      source
                      def ConstructionGrammar.instDecidableEqSlot.decEq {Lex✝ : Type} [DecidableEq Lex✝] (x✝ x✝¹ : Slot Lex✝) :
                      Decidable (x✝ = x✝¹)
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For
                        source
                        @[implicit_reducible]
                        instance ConstructionGrammar.instReprSlot {Lex✝ : Type} [Repr Lex✝] :
                        Repr (Slot Lex✝)
                        Equations
                        source
                        def ConstructionGrammar.instReprSlot.repr {Lex✝ : Type} [Repr Lex✝] :
                        Slot Lex✝ → ℕ → Std.Format
                        Equations
                        • One or more equations did not get rendered due to their size.
                        Instances For
                          source
                          @[reducible, inline]
                          abbrev ConstructionGrammar.TypedForm (Lex : Type) :
                          Type

                          A typed form: the form side of a construction as a sequence of slots.

                          This replaces Construction.form : String with a structured representation that supports computation (abstraction level, specificity derivation).

                          Equations
                          Instances For
                            source
                            def ConstructionGrammar.abstractionLevel {Lex : Type} (form : TypedForm Lex) :
                            ℚ

                            Proportion of open slots: a continuous [0,1] measure of abstraction.

                            This computes the fraction of slots that are open (SYN or SEM+). @cite{dunn-2025} defines four discrete abstraction orders based on which representation levels appear (1st = all LEX, 2nd = mostly LEX, 3rd = mixed, 4th = all abstract). This function computes the continuous proportion underlying those orders; derivedSpecificity (below) maps to the three-way Specificity enum.

                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For
                              source
                              def ConstructionGrammar.derivedSpecificity {Lex : Type} (form : TypedForm Lex) :
                              Specificity

                              Derive Specificity from the slot structure.

                              ConditionResult
                              All slots open.fullyAbstract
                              No slots open.lexicallySpecified
                              Mix of fixed and open.partiallyOpen

                              This makes Specificity a derived property rather than a stipulated one: changing a slot from open to fixed automatically changes the specificity.

                              Equations
                              • One or more equations did not get rendered due to their size.
                              Instances For
                                source
                                def ConstructionGrammar.ConstructionSlot.toSlot (s : ConstructionSlot) :
                                Slot String

                                Embed an all-open ConstructionSlot as a Slot String.

                                Every ConstructionSlot is an open slot (it only specifies cat : UPOS). The embedding preserves category, role, and headedness.

                                Equations
                                Instances For
                                  source
                                  def ConstructionGrammar.ArgStructureConstruction.toTypedForm (asc : ArgStructureConstruction) :
                                  TypedForm String

                                  Convert an ArgStructureConstruction's slot list to a TypedForm.

                                  Equations
                                  Instances For
                                    source
                                    theorem ConstructionGrammar.ConstructionSlot.toSlot_isOpen (s : ConstructionSlot) :
                                    s.toSlot.filler.isOpen = true

                                    All-open slots are always open (by construction).

                                    source
                                    def ConstructionGrammar.hasConstraint {Lex : Type} (form : TypedForm Lex) (c : SlotConstraint) :
                                    Bool

                                    Does any slot in the form bear a given constraint?

                                    Equations
                                    Instances For
                                      source
                                      def ConstructionGrammar.refGroupCount {Lex : Type} (form : TypedForm Lex) :
                                      ℕ

                                      Count of distinct coreference groups in a form.

                                      Equations
                                      Instances For