inductive Semantics.Montague.ScaleMembership : Type

Scale membership position for closed-class expressions.

Numerals are excluded: under lower-bound semantics they form an infinite scale (not representable as a finite HornScale), and under bilateral semantics they don't form a scale at all. See Theories/Semantics.Montague/Determiner/Numeral/Semantics.lean.

• quantifier (pos : Core.Scale.Quantifiers.QuantExpr) : ScaleMembership
• connective (pos : Core.Scale.Connectives.ConnExpr) : ScaleMembership
• modal (pos : Core.Scale.Modals.ModalExpr) : ScaleMembership

instance Semantics.Montague.instReprScaleMembership : Repr ScaleMembership

Equations

• Semantics.Montague.instReprScaleMembership = { reprPrec := Semantics.Montague.instReprScaleMembership.repr }

def Semantics.Montague.instReprScaleMembership.repr : ScaleMembership → ℕ → Std.Format

Equations

• One or more equations did not get rendered due to their size.

structure Semantics.Montague.SemLexEntry (m : Model) : Type

Semantic lexical entry

• word : Word
• ty : Ty
• denot : m.interpTy self.ty
• scaleMembership : Option ScaleMembership

def Semantics.Montague.SemLexEntry.form {m : Model} (e : SemLexEntry m) : String

Equations

• e.form = e.word.form

def Semantics.Montague.SemLexEntry.isScalar {m : Model} (e : SemLexEntry m) : Bool

Equations

• e.isScalar = e.scaleMembership.isSome

def Semantics.Montague.SemLexEntry.strongerAlternatives {m : Model} (e : SemLexEntry m) : List String

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.some_entry : SemLexEntry toyModel

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.every_entry : SemLexEntry toyModel

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.most_entry : SemLexEntry toyModel

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.no_entry : SemLexEntry toyModel

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.john_entry : SemLexEntry toyModel

Equations

• Semantics.Montague.john_entry = { word := Semantics.Montague.word_john✝, ty := Semantics.Montague.Ty.e, denot := Semantics.Montague.ToyEntity.john }

def Semantics.Montague.mary_entry : SemLexEntry toyModel

Equations

• Semantics.Montague.mary_entry = { word := Semantics.Montague.word_mary✝, ty := Semantics.Montague.Ty.e, denot := Semantics.Montague.ToyEntity.mary }

def Semantics.Montague.sleeps_entry : SemLexEntry toyModel

Equations

• Semantics.Montague.sleeps_entry = { word := Semantics.Montague.word_sleeps✝, ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := Semantics.Montague.ToyLexicon.sleeps_sem }

def Semantics.Montague.laughs_entry : SemLexEntry toyModel

Equations

• Semantics.Montague.laughs_entry = { word := Semantics.Montague.word_laughs✝, ty := Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t, denot := Semantics.Montague.ToyLexicon.laughs_sem }

def Semantics.Montague.studentStem : Core.Morphology.Stem (toyModel.interpTy (Ty.e ⇒ Ty.t))

Student noun stem: paradigm generates both sg and pl entries.

In the toy model (no mereological structure), the plural rule is semantically flat (semEffect := id). In a model with Link-style plurals, use Number.pluralNounRule with closure/atom predicates.

Equations

• Semantics.Montague.studentStem = { lemma_ := "student", cat := UD.UPOS.NOUN, baseFeatures := { number := some UD.Number.Sing }, paradigm := [Core.Morphology.Number.pluralNounRuleFlat] }

def Semantics.Montague.student_entry : SemLexEntry toyModel

Singular "student" entry derived from stem.

Equations

• One or more equations did not get rendered due to their size.

def Semantics.Montague.students_entry : SemLexEntry toyModel

Plural "students" entry derived from stem via plural rule.

Equations

• One or more equations did not get rendered due to their size.

theorem Semantics.Montague.student_entry_form : student_entry.word.form = "student"

The stem-derived singular entry preserves the expected form and features.

theorem Semantics.Montague.student_entry_number : student_entry.word.features.number = some UD.Number.Sing

theorem Semantics.Montague.students_entry_form : students_entry.word.form = "students"

The stem-derived plural entry produces the expected form and features.

theorem Semantics.Montague.students_entry_number : students_entry.word.features.number = some UD.Number.Plur

theorem Semantics.Montague.student_plural_flat_sem : students_entry.denot = student_entry.denot

In the toy model (flat plural semantics), both entries share the same denotation since pluralNounRuleFlat.semEffect = id.

def Semantics.Montague.SemLexicon (m : Model) : Type

Equations

• Semantics.Montague.SemLexicon m = (String → Option (Semantics.Montague.SemLexEntry m))

def Semantics.Montague.toyLexicon : SemLexicon toyModel

Equations

• Semantics.Montague.toyLexicon "some" = some Semantics.Montague.some_entry
• Semantics.Montague.toyLexicon "every" = some Semantics.Montague.every_entry
• Semantics.Montague.toyLexicon "all" = some Semantics.Montague.every_entry
• Semantics.Montague.toyLexicon "most" = some Semantics.Montague.most_entry
• Semantics.Montague.toyLexicon "no" = some Semantics.Montague.no_entry
• Semantics.Montague.toyLexicon "John" = some Semantics.Montague.john_entry
• Semantics.Montague.toyLexicon "Mary" = some Semantics.Montague.mary_entry
• Semantics.Montague.toyLexicon "sleeps" = some Semantics.Montague.sleeps_entry
• Semantics.Montague.toyLexicon "laughs" = some Semantics.Montague.laughs_entry
• Semantics.Montague.toyLexicon "student" = some Semantics.Montague.student_entry
• Semantics.Montague.toyLexicon "students" = some Semantics.Montague.students_entry
• Semantics.Montague.toyLexicon form = none

def Semantics.Montague.lookupAlternatives {m : Model} (lex : SemLexicon m) (form : String) : List (SemLexEntry m)

Equations

• Semantics.Montague.lookupAlternatives lex form = match lex form with | none => [] | some entry => List.filterMap (fun (altForm : String) => lex altForm) entry.strongerAlternatives

theorem Semantics.Montague.some_is_scalar : some_entry.isScalar = true

theorem Semantics.Montague.every_is_scalar : every_entry.isScalar = true

theorem Semantics.Montague.john_not_scalar : john_entry.isScalar = false