Toy Domain for Testing

Minimal model for testing compositional semantics:

• ToyEntity — four entities (john, mary, pizza, book)
• toyFrame — frame over ToyEntity with trivial index
• ToyLexicon — basic lexical entries (sleeps, sees, eats, reads, etc.)

inductive Semantics.Montague.ToyEntity : Type

• john : ToyEntity
• mary : ToyEntity
• pizza : ToyEntity
• book : ToyEntity

def Semantics.Montague.instReprToyEntity.repr : ToyEntity → ℕ → Std.Format

Equations

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

@[implicit_reducible]

instance Semantics.Montague.instReprToyEntity : Repr ToyEntity

Equations

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

@[implicit_reducible]

instance Semantics.Montague.instDecidableEqToyEntity : DecidableEq ToyEntity

Equations

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

def Semantics.Montague.toyFrame : Core.Logic.Intensional.Frame

Equations

• Semantics.Montague.toyFrame = { Entity := Semantics.Montague.ToyEntity, Index := Unit }

@[reducible, inline]

abbrev Semantics.Montague.toyModel : Core.Logic.Intensional.Frame

Backward-compatible alias.

Equations

• Semantics.Montague.toyModel = Semantics.Montague.toyFrame

def Semantics.Montague.ToyLexicon.john_sem : toyFrame.Denot Core.Logic.Intensional.Ty.e

Equations

• Semantics.Montague.ToyLexicon.john_sem = Semantics.Montague.ToyEntity.john

def Semantics.Montague.ToyLexicon.mary_sem : toyFrame.Denot Core.Logic.Intensional.Ty.e

Equations

• Semantics.Montague.ToyLexicon.mary_sem = Semantics.Montague.ToyEntity.mary

def Semantics.Montague.ToyLexicon.sleeps_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.sleeps_sem Semantics.Montague.ToyEntity.john = True
• Semantics.Montague.ToyLexicon.sleeps_sem x = False

def Semantics.Montague.ToyLexicon.laughs_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.laughs_sem Semantics.Montague.ToyEntity.john = True
• Semantics.Montague.ToyLexicon.laughs_sem Semantics.Montague.ToyEntity.mary = True
• Semantics.Montague.ToyLexicon.laughs_sem x = False

def Semantics.Montague.ToyLexicon.sees_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.mary Semantics.Montague.ToyEntity.john = True
• Semantics.Montague.ToyLexicon.sees_sem Semantics.Montague.ToyEntity.john Semantics.Montague.ToyEntity.mary = True
• Semantics.Montague.ToyLexicon.sees_sem obj subj = False

def Semantics.Montague.ToyLexicon.eats_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.eats_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.john = True
• Semantics.Montague.ToyLexicon.eats_sem Semantics.Montague.ToyEntity.pizza Semantics.Montague.ToyEntity.mary = True
• Semantics.Montague.ToyLexicon.eats_sem obj subj = False

def Semantics.Montague.ToyLexicon.reads_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.reads_sem Semantics.Montague.ToyEntity.book Semantics.Montague.ToyEntity.john = True
• Semantics.Montague.ToyLexicon.reads_sem Semantics.Montague.ToyEntity.book Semantics.Montague.ToyEntity.mary = True
• Semantics.Montague.ToyLexicon.reads_sem obj subj = False

def Semantics.Montague.ToyLexicon.pizza_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.pizza_sem Semantics.Montague.ToyEntity.pizza = True
• Semantics.Montague.ToyLexicon.pizza_sem x = False

def Semantics.Montague.ToyLexicon.book_sem : toyFrame.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

Equations

• Semantics.Montague.ToyLexicon.book_sem Semantics.Montague.ToyEntity.book = True
• Semantics.Montague.ToyLexicon.book_sem x = False