Documentation

Linglib.Theories.Semantics.Composition.LexiconBuilder

Lexicon Builder #

Dispatch layer connecting Fragment classificatory data to compositional semantics. Provides:

  1. Type dispatch (ComplementType.toTy): deterministic mapping from verb complement type to Montague semantic type.

  2. Lexicon construction (buildLexicon): assembles a Lexicon F from a list of named entries, replacing the hand-written match-on-strings pattern that Studies currently use.

  3. Entry construction (VerbCore.mkLexEntry): given a VerbCore and a denotation of the appropriate type, produce a LexEntry F.

Design #

The dispatch layer does NOT generate denotations from features — that would be too theory-laden. It provides the type and the scaffolding; the Study still supplies the denotation. Domain-specific denotation builders (VerbCore.getCoSSemantics, VerbCore.veridicality, etc.) remain in Theories/Semantics/Lexical/Verb/VerbEntry.lean.

Usage pattern #

-- In a Study file:
import Linglib.Theories.Semantics.Composition.LexiconBuilder
import Linglib.Fragments.English.Predicates.Verbal

open Semantics.Composition.LexiconBuilder (buildLexicon)
open Semantics.Montague (LexEntry)

def myLexicon : Lexicon myModel :=
  buildLexicon [
    ("john", ⟨.e, john_sem⟩),
    ("sleeps", ⟨.et, sleeps_sem⟩),
    ("sees", ⟨.eet, sees_sem⟩)
  ]

Type Dispatch #

source
def Semantics.Lexical.ComplementType.toTy :
ComplementType → Core.Logic.Intensional.Ty

Map a verb's complement type to its Montague semantic type.

  • Intransitives (none): e → t (1-place predicate)
  • Transitives (np): e → e → t (2-place, object then subject)
  • Ditransitives (np_np): e → e → e → t (IO, DO, subject)
  • NP+PP (np_pp): e → e → e → t (same arity as ditransitive)
  • Finite clause (finiteClause): t → e → t (proposition-taking)
  • Infinitival (infinitival): (e → t) → e → t (property-taking)
  • Gerund (gerund): (e → t) → e → t (same as infinitival)
  • Small clause (smallClause): (e → t) → e → t (resultative predicate)
  • Question (question): (e → t) → e → t (question-embedding)
Equations
Instances For
    source
    def Semantics.Lexical.VerbCore.semanticType (v : VerbCore) :
    Core.Logic.Intensional.Ty

    The semantic type of a verb, determined by its complement type.

    Equations
    Instances For

      Lexicon Construction #

      source
      def Semantics.Composition.LexiconBuilder.buildLexicon {F : Core.Logic.Intensional.Frame} (entries : List (String × Montague.LexEntry F)) :
      Montague.Lexicon F

      Build a Lexicon F from a list of named entries.

      Replaces the pattern of hand-written match expressions on strings that Studies currently use. Lookup is linear in the entry list; this is fine for the small lexicons (5–30 entries) typical of Study files.

      def myLex : Lexicon myModel := buildLexicon [
  ("john", ⟨.e, john_sem⟩),
  ("sleeps", ⟨.et, sleeps_sem⟩)
]
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def Semantics.Composition.LexiconBuilder.extendLexicon {F : Core.Logic.Intensional.Frame} (base : Montague.Lexicon F) (extra : List (String × Montague.LexEntry F)) :
        Montague.Lexicon F

        Extend a lexicon with additional entries. Later entries shadow earlier ones with the same name.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def Semantics.Composition.LexiconBuilder.mergeLexicons {F : Core.Logic.Intensional.Frame} (lex1 lex2 : Montague.Lexicon F) :
          Montague.Lexicon F

          Merge two lexicons. The first lexicon takes priority on conflicts.

          Equations
          Instances For

            Entry Construction #

            source
            def Semantics.Composition.LexiconBuilder.VerbCore.mkLexEntry (v : Lexical.VerbCore) (F : Core.Logic.Intensional.Frame) (denot : F.Denot v.semanticType) :
            Montague.LexEntry F

            Create a LexEntry for a verb, using complementType.toTy to determine the semantic type. The caller provides a denotation of the appropriate type.

            This ensures the entry's type tag matches the verb's argument structure by construction.

            Equations
            Instances For

              Convenience #

              source
              def Semantics.Composition.LexiconBuilder.emptyLexicon {F : Core.Logic.Intensional.Frame} :
              Montague.Lexicon F

              The empty lexicon.

              Equations
              Instances For
                source
                def Semantics.Composition.LexiconBuilder.singletonLexicon {F : Core.Logic.Intensional.Frame} (name : String) (entry : Montague.LexEntry F) :
                Montague.Lexicon F

                A single-entry lexicon.

                Equations
                Instances For