structure Semantics.Montague.Derivation.ScalarOccurrence (m : Model) : Type

Scalar item occurrence in a derivation

• position : ℕ
• entry : SemLexEntry m

structure Semantics.Montague.Derivation.SemDeriv (m : Model) : Type

Semantic derivation: output of compositional interpretation

• surface : List String
• ty : Ty
• meaning : m.interpTy self.ty
• scalarItems : List (ScalarOccurrence m)

@[reducible, inline]

abbrev Semantics.Montague.Derivation.Derivation (m : Model) : Type

Equations

• Semantics.Montague.Derivation.Derivation = Semantics.Montague.Derivation.SemDeriv

def Semantics.Montague.Derivation.SemDeriv.sentence {m : Model} (d : SemDeriv m) : String

Equations

• d.sentence = " ".intercalate d.surface

def Semantics.Montague.Derivation.SemDeriv.hasScalarItems {m : Model} (d : SemDeriv m) : Bool

Equations

• d.hasScalarItems = !d.scalarItems.isEmpty

def Semantics.Montague.Derivation.alternativeMeanings {m : Model} [Lexical.Determiner.Quantifier.FiniteModel m] (d : SemDeriv m) (_ctx : Core.NaturalLogic.ContextPolarity) : List (m.interpTy d.ty)

Generate sentential alternatives by replacing scalar items

Equations

• Semantics.Montague.Derivation.alternativeMeanings d _ctx = []

def Semantics.Montague.Derivation.alternativeForms {m : Model} (d : SemDeriv m) (ctx : Core.NaturalLogic.ContextPolarity) : List (List String)

Get surface forms of scalar alternatives

Equations

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

def Semantics.Montague.Derivation.johnSleeps : SemDeriv toyModel

Equations

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

def Semantics.Montague.Derivation.someStudentsSleep : SemDeriv toyModel

Equations

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

def Semantics.Montague.Derivation.everyStudentSleeps : SemDeriv toyModel

Equations

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

def Semantics.Montague.Derivation.someStudentsLaugh : SemDeriv toyModel

Equations

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

def Semantics.Montague.Derivation.everyStudentLaughs : SemDeriv toyModel

Equations

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

theorem Semantics.Montague.Derivation.johnSleeps_no_scalars : johnSleeps.hasScalarItems = false

theorem Semantics.Montague.Derivation.someStudentsSleep_has_scalars : someStudentsSleep.hasScalarItems = true

theorem Semantics.Montague.Derivation.someStudentsSleep_true : someStudentsSleep.meaning = true

theorem Semantics.Montague.Derivation.everyStudentSleeps_false : everyStudentSleeps.meaning = false

theorem Semantics.Montague.Derivation.everyStudentLaughs_true : everyStudentLaughs.meaning = true

class Semantics.Montague.Derivation.SemanticsProducer (SynDeriv : Type) (m : Model) : Type

Syntax theory that can produce semantic derivations

• toDerivation : SynDeriv → SemDeriv m