Documentation

Linglib.Semantics.Composition.Toy

A toy model for type-driven composition #

toyModel is a small extensional model for exercising the composition engine, with four entities (John, Mary, a pizza and a book), one world, and a signature of two constants and eight content relations, which toyStructure interprets as equalities on the entities. The fragment is of the kind Heim and Kratzer interpret in their textbook, with proper names, intransitive and transitive verbs, and common nouns. The words toyWords translate English word forms to symbols, and the lexicon toyLexicon and the denotations Toy.sleeps, Toy.sees, … are read off the model; with the logical words, quantified trees translate to logical forms that read back to first-order formulas.

Main definitions #

ToyEntity: the entity domain.
toyLang, toyStructure: the signature and its interpretation.
toyModel: the one-world composition model.
toyWords, toyLexicon: the content words and the lexicon they induce.
Toy.logicalWords, toyVocabulary: the logical words, and all the toy words.

Implementation notes #

The signature follows mathlib's concrete-language idiom (Mathlib/ModelTheory/Algebra/Ring/Basic.lean), with arity-indexed symbol inductives and per-symbol abbreviations in Toy. The structure is a closed term, so a claim about particular entities reduces by rfl to an equality on ToyEntity. Binary relations take the subject first in the structure and the object first as transitive-verb denotations, as Model.pred₂ does.

References #

[HK98]

inductive HeimKratzer.ToyEntity :

The entities of the toy model are John, Mary, a pizza and a book.

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

Instances For

def HeimKratzer.instReprToyEntity.repr :

ToyEntity → ℕ → Std.Format

Equations

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

Instances For

@[instance_reducible]

instance HeimKratzer.instReprToyEntity :

Equations

HeimKratzer.instReprToyEntity = { reprPrec := HeimKratzer.instReprToyEntity.repr }

@[instance_reducible]

instance HeimKratzer.instDecidableEqToyEntity :

DecidableEq ToyEntity

Equations

HeimKratzer.instDecidableEqToyEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

@[instance_reducible]

instance HeimKratzer.instFintypeToyEntity :

Fintype ToyEntity

Equations

HeimKratzer.instFintypeToyEntity = { elems := { val := ↑HeimKratzer.ToyEntity.enumList, nodup := HeimKratzer.ToyEntity.enumList_nodup }, complete := HeimKratzer.instFintypeToyEntity._proof_1 }

inductive HeimKratzer.toyFunc :

ℕ → Type

The function symbols of the toy signature are the constants naming entities.

john : toyFunc 0
mary : toyFunc 0

Instances For

def HeimKratzer.instDecidableEqToyFunc.decEq {a✝ : ℕ} (x✝ x✝¹ : toyFunc a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance HeimKratzer.instDecidableEqToyFunc {a✝ : ℕ} :

DecidableEq (toyFunc a✝)

Equations

HeimKratzer.instDecidableEqToyFunc = HeimKratzer.instDecidableEqToyFunc.decEq

inductive HeimKratzer.toyRel :

ℕ → Type

The relation symbols of the toy signature are the content words at their arities.

sleep : toyRel 1
laugh : toyRel 1
student : toyRel 1
person : toyRel 1
pizza : toyRel 1
see : toyRel 2
eat : toyRel 2
read : toyRel 2

Instances For

def HeimKratzer.instDecidableEqToyRel.decEq {a✝ : ℕ} (x✝ x✝¹ : toyRel a✝) :

Decidable (x✝ = x✝¹)

Equations

Instances For

@[instance_reducible]

instance HeimKratzer.instDecidableEqToyRel {a✝ : ℕ} :

DecidableEq (toyRel a✝)

Equations

HeimKratzer.instDecidableEqToyRel = HeimKratzer.instDecidableEqToyRel.decEq

def HeimKratzer.toyLang :

FirstOrder.Language

The toy signature has the toy constants as function symbols and the toy content words as relation symbols.

Equations

HeimKratzer.toyLang = { Functions := HeimKratzer.toyFunc, Relations := HeimKratzer.toyRel }

Instances For

@[reducible, inline]

abbrev HeimKratzer.toyStructure :

toyLang.Structure ToyEntity

In the toy structure the names denote their entities, John sleeps, John and Mary laugh and are the students and the persons, the pizza is the one pizza, John and Mary see each other, and both eat the pizza and read the book. Binary relations take the subject first.

Equations

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

Instances For

def HeimKratzer.toyModel :

The toy composition model is extensional, with the toy structure at its one world.

Equations

HeimKratzer.toyModel = { E := HeimKratzer.ToyEntity, W := Unit, interp := fun (x : Unit) => HeimKratzer.toyStructure }

Instances For

The per-symbol abbreviations have the types toyLang.Constants and toyLang.Relations n, so symbols elaborate without unfolding toyLang.

@[reducible, inline]

abbrev HeimKratzer.Toy.johnConst :

toyLang.Constants

Equations

HeimKratzer.Toy.johnConst = HeimKratzer.toyFunc.john

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.maryConst :

toyLang.Constants

Equations

HeimKratzer.Toy.maryConst = HeimKratzer.toyFunc.mary

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.sleepRel :

toyLang.Relations 1

Equations

HeimKratzer.Toy.sleepRel = HeimKratzer.toyRel.sleep

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.laughRel :

toyLang.Relations 1

Equations

HeimKratzer.Toy.laughRel = HeimKratzer.toyRel.laugh

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.studentRel :

toyLang.Relations 1

Equations

HeimKratzer.Toy.studentRel = HeimKratzer.toyRel.student

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.personRel :

toyLang.Relations 1

Equations

HeimKratzer.Toy.personRel = HeimKratzer.toyRel.person

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.pizzaRel :

toyLang.Relations 1

Equations

HeimKratzer.Toy.pizzaRel = HeimKratzer.toyRel.pizza

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.seeRel :

toyLang.Relations 2

Equations

HeimKratzer.Toy.seeRel = HeimKratzer.toyRel.see

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.eatRel :

toyLang.Relations 2

Equations

HeimKratzer.Toy.eatRel = HeimKratzer.toyRel.eat

Instances For

@[reducible, inline]

abbrev HeimKratzer.Toy.readRel :

toyLang.Relations 2

Equations

HeimKratzer.Toy.readRel = HeimKratzer.toyRel.read

Instances For

The denotations of the toy content words are read off the model at its one world.

def HeimKratzer.Toy.sleeps :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.sleeps = HeimKratzer.toyModel.pred₁ HeimKratzer.Toy.sleepRel ()

Instances For

def HeimKratzer.Toy.laughs :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.laughs = HeimKratzer.toyModel.pred₁ HeimKratzer.Toy.laughRel ()

Instances For

def HeimKratzer.Toy.student :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.student = HeimKratzer.toyModel.pred₁ HeimKratzer.Toy.studentRel ()

Instances For

def HeimKratzer.Toy.person :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.person = HeimKratzer.toyModel.pred₁ HeimKratzer.Toy.personRel ()

Instances For

def HeimKratzer.Toy.pizza :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.pizza = HeimKratzer.toyModel.pred₁ HeimKratzer.Toy.pizzaRel ()

Instances For

def HeimKratzer.Toy.sees :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.sees = HeimKratzer.toyModel.pred₂ HeimKratzer.Toy.seeRel ()

Instances For

def HeimKratzer.Toy.eats :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.eats = HeimKratzer.toyModel.pred₂ HeimKratzer.Toy.eatRel ()

Instances For

def HeimKratzer.Toy.reads :

Montague.Ty.Domain ToyEntity Unit (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

Equations

HeimKratzer.Toy.reads = HeimKratzer.toyModel.pred₂ HeimKratzer.Toy.readRel ()

Instances For

def HeimKratzer.toyWords :

String → Option ((ty : Montague.Ty) × FirstOrderConstant toyLang ty)

The toy content words translate to the symbols of the toy signature.

Equations

HeimKratzer.toyWords "John" = some ⟨Montague.Ty.e, HeimKratzer.FirstOrderConstant.name HeimKratzer.Toy.johnConst⟩
HeimKratzer.toyWords "Mary" = some ⟨Montague.Ty.e, HeimKratzer.FirstOrderConstant.name HeimKratzer.Toy.maryConst⟩
HeimKratzer.toyWords "sleeps" = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₁ HeimKratzer.Toy.sleepRel⟩
HeimKratzer.toyWords "laughs" = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₁ HeimKratzer.Toy.laughRel⟩
HeimKratzer.toyWords "student" = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₁ HeimKratzer.Toy.studentRel⟩
HeimKratzer.toyWords "person" = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₁ HeimKratzer.Toy.personRel⟩
HeimKratzer.toyWords "pizza" = some ⟨Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₁ HeimKratzer.Toy.pizzaRel⟩
HeimKratzer.toyWords "sees" = some ⟨Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₂ HeimKratzer.Toy.seeRel⟩
HeimKratzer.toyWords "eats" = some ⟨Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₂ HeimKratzer.Toy.eatRel⟩
HeimKratzer.toyWords "reads" = some ⟨Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.rel₂ HeimKratzer.Toy.readRel⟩
HeimKratzer.toyWords x✝ = none

Instances For

def HeimKratzer.toyLexicon :

Lexicon ToyEntity Unit

The toy lexicon is the lexicon the toy words induce over the toy model.

Equations

HeimKratzer.toyLexicon = HeimKratzer.toyModel.lexicon HeimKratzer.toyWords ()

Instances For

theorem HeimKratzer.toyLexicon_fst {s : String} {d : Montague.Denotation ToyEntity Unit} (h : toyLexicon s = some d) :

d.fst = Montague.Ty.e ∨ d.fst = (Montague.Ty.e ⇒ Montague.Ty.t) ∨ d.fst = (Montague.Ty.e ⇒ Montague.Ty.e ⇒ Montague.Ty.t)

The toy lexicon has entries of the three first-order lexical types only.

Logical forms and their readback #

With the logical words, a quantifier-raised tree translates to its logical form, with the mode at each node, and the logical form reads back to the first-order formula of its truth conditions.

def HeimKratzer.Toy.logicalWords {L : FirstOrder.Language} :

String → Option ((ty : Montague.Ty) × FirstOrderConstant L ty)

The English logical words translate to the logical first-order constants.

Equations

HeimKratzer.Toy.logicalWords "every" = some ⟨Montague.Ty.det, HeimKratzer.FirstOrderConstant.every⟩
HeimKratzer.Toy.logicalWords "some" = some ⟨Montague.Ty.det, HeimKratzer.FirstOrderConstant.some⟩
HeimKratzer.Toy.logicalWords "no" = some ⟨Montague.Ty.det, HeimKratzer.FirstOrderConstant.no⟩
HeimKratzer.Toy.logicalWords "not" = some ⟨Montague.Ty.t ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.neg⟩
HeimKratzer.Toy.logicalWords "and" = some ⟨Montague.Ty.t ⇒ Montague.Ty.t ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.conj⟩
HeimKratzer.Toy.logicalWords "or" = some ⟨Montague.Ty.t ⇒ Montague.Ty.t ⇒ Montague.Ty.t, HeimKratzer.FirstOrderConstant.disj⟩
HeimKratzer.Toy.logicalWords x✝ = none

Instances For

def HeimKratzer.toyVocabulary (s : String) :

Option ((ty : Montague.Ty) × FirstOrderConstant toyLang ty)

The toy vocabulary translates the toy content words and the logical words.

Equations

HeimKratzer.toyVocabulary s = (HeimKratzer.toyWords s <|> HeimKratzer.Toy.logicalWords s)

Instances For

def HeimKratzer.everyStudentSleeps :

PhraseStructure.Tree Unit String

Every student sleeps, with the subject raised over the trace of index 1.

Equations

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

Instances For

In the logical form of every student sleeps the determiner applies forward to the noun and to the abstraction over the trace, which the verb applies backward to.

def HeimKratzer.everyStudentWhoSleepsLaughs :

PhraseStructure.Tree Unit String

In every student who sleeps laughs the relative clause abstracts over its trace and intersects with the noun by predicate modification.

Equations

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

Instances For