structure Semantics.Montague.Interface.SemanticBackend.MontagueSentence : Type

Sentence with its denotation

• form : String
• meaning : toyModel.interpTy Ty.t

inductive Semantics.Montague.Interface.SemanticBackend.ToyWorld : Type

World state

• actual : ToyWorld

instance Semantics.Montague.Interface.SemanticBackend.instDecidableEqToyWorld : DecidableEq ToyWorld

Equations

• Semantics.Montague.Interface.SemanticBackend.instDecidableEqToyWorld x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

instance Semantics.Montague.Interface.SemanticBackend.instReprToyWorld : Repr ToyWorld

Equations

• Semantics.Montague.Interface.SemanticBackend.instReprToyWorld = { reprPrec := Semantics.Montague.Interface.SemanticBackend.instReprToyWorld.repr }

def Semantics.Montague.Interface.SemanticBackend.instReprToyWorld.repr : ToyWorld → ℕ → Std.Format

Equations

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

def Semantics.Montague.Interface.SemanticBackend.evaluate (s : MontagueSentence) (w : ToyWorld) : Bool

Evaluate a sentence's truth in a world

Equations

• Semantics.Montague.evaluate s Semantics.Montague.Interface.SemanticBackend.ToyWorld.actual = s.meaning

def Semantics.Montague.Interface.SemanticBackend.montaguePhi (s : MontagueSentence) (w : ToyWorld) : Float

Semantic agreement function: 1.0 if true, 0.0 if false

Equations

• Semantics.Montague.montaguePhi s w = if Semantics.Montague.evaluate s w = true then 1.0 else 0.0

def Semantics.Montague.Interface.SemanticBackend.johnSleepsSent : MontagueSentence

Equations

• Semantics.Montague.johnSleepsSent = { form := "John sleeps", meaning := Semantics.Montague.apply Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.john_sem }

def Semantics.Montague.Interface.SemanticBackend.marySleepsSent : MontagueSentence

Equations

• Semantics.Montague.marySleepsSent = { form := "Mary sleeps", meaning := Semantics.Montague.apply Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyLexicon.mary_sem }

def Semantics.Montague.Interface.SemanticBackend.johnSeesMary : MontagueSentence

Equations

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

theorem Semantics.Montague.Interface.SemanticBackend.john_sleeps_phi : montaguePhi johnSleepsSent ToyWorld.actual = 1.0

theorem Semantics.Montague.Interface.SemanticBackend.mary_sleeps_phi : montaguePhi marySleepsSent ToyWorld.actual = 0.0

theorem Semantics.Montague.Interface.SemanticBackend.john_sees_mary_phi : montaguePhi johnSeesMary ToyWorld.actual = 1.0