Documentation

Linglib.Fragments.English.Toy

Toy English fragment #

The pedagogical fragment used by compositional-semantics studies, built the model-theoretic way and in mathlib's concrete-language idiom (after Mathlib/ModelTheory/Algebra/Ring/Basic.lean): arity-indexed symbol inductives (toyFunc, toyRel), the signature (toyLang), per-symbol defeq abbreviations (sleepRel, …), a structure carrying the facts (toyStructure) with one @[simp] lemma per symbol, the composition model (toyModel), and naming maps (toyNaming) from word forms into the signature. The ToyLexicon denotations are read off the model via Model.const/Model.pred₁ext/Model.pred₂ext — the connection is true by construction, with no bridge theorems.

Lives in Fragments/ so substrate files cannot import it — worked examples over this fragment belong in Studies/. The namespace remains Semantics.Montague for continuity with the engine's Lexicon.

inductive Semantics.Montague.ToyEntity :

The four entities.

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

Instances For

def Semantics.Montague.instReprToyEntity.repr :

ToyEntity → ℕ → Std.Format

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Montague.instReprToyEntity :

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 ⋯

@[implicit_reducible]

instance Semantics.Montague.instFintypeToyEntity :

Fintype ToyEntity

Equations

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

inductive Semantics.Montague.toyFunc :

ℕ → Type

Function symbols of the toy signature: constants naming entities.

john : toyFunc 0
mary : toyFunc 0

Instances For

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

Decidable (x✝ = x✝¹)

Equations

Instances For

@[implicit_reducible]

instance Semantics.Montague.instDecidableEqToyFunc {a✝ : ℕ} :

DecidableEq (toyFunc a✝)

Equations

Semantics.Montague.instDecidableEqToyFunc = Semantics.Montague.instDecidableEqToyFunc.decEq

inductive Semantics.Montague.toyRel :

ℕ → Type

Relation symbols of the toy signature: content words at their arities.

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

Instances For

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

Decidable (x✝ = x✝¹)

Equations

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

Instances For

@[implicit_reducible]

instance Semantics.Montague.instDecidableEqToyRel {a✝ : ℕ} :

DecidableEq (toyRel a✝)

Equations

Semantics.Montague.instDecidableEqToyRel = Semantics.Montague.instDecidableEqToyRel.decEq

def Semantics.Montague.toyLang :

FirstOrder.Language

The toy lexical signature.

Equations

Semantics.Montague.toyLang = { Functions := Semantics.Montague.toyFunc, Relations := Semantics.Montague.toyRel }

Instances For

Per-symbol abbreviations with the defeq types toyLang.Constants / toyLang.Relations n (mathlib's addFunc idiom), so symbols elaborate without unfolding toyLang.

@[reducible, inline]

abbrev Semantics.Montague.johnConst :

toyLang.Constants

Equations

Semantics.Montague.johnConst = Semantics.Montague.toyFunc.john

Instances For

@[reducible, inline]

abbrev Semantics.Montague.maryConst :

toyLang.Constants

Equations

Semantics.Montague.maryConst = Semantics.Montague.toyFunc.mary

Instances For

@[reducible, inline]

abbrev Semantics.Montague.sleepRel :

toyLang.Relations 1

Equations

Semantics.Montague.sleepRel = Semantics.Montague.toyRel.sleep

Instances For

@[reducible, inline]

abbrev Semantics.Montague.laughRel :

toyLang.Relations 1

Equations

Semantics.Montague.laughRel = Semantics.Montague.toyRel.laugh

Instances For

@[reducible, inline]

abbrev Semantics.Montague.studentRel :

toyLang.Relations 1

Equations

Semantics.Montague.studentRel = Semantics.Montague.toyRel.student

Instances For

@[reducible, inline]

abbrev Semantics.Montague.personRel :

toyLang.Relations 1

Equations

Semantics.Montague.personRel = Semantics.Montague.toyRel.person

Instances For

@[reducible, inline]

abbrev Semantics.Montague.thingRel :

toyLang.Relations 1

Equations

Semantics.Montague.thingRel = Semantics.Montague.toyRel.thing

Instances For

@[reducible, inline]

abbrev Semantics.Montague.pizzaRel :

toyLang.Relations 1

Equations

Semantics.Montague.pizzaRel = Semantics.Montague.toyRel.pizza

Instances For

@[reducible, inline]

abbrev Semantics.Montague.bookRel :

toyLang.Relations 1

Equations

Semantics.Montague.bookRel = Semantics.Montague.toyRel.book

Instances For

@[reducible, inline]

abbrev Semantics.Montague.seeRel :

toyLang.Relations 2

Equations

Semantics.Montague.seeRel = Semantics.Montague.toyRel.see

Instances For

@[reducible, inline]

abbrev Semantics.Montague.eatRel :

toyLang.Relations 2

Equations

Semantics.Montague.eatRel = Semantics.Montague.toyRel.eat

Instances For

@[reducible, inline]

abbrev Semantics.Montague.readRel :

toyLang.Relations 2

Equations

Semantics.Montague.readRel = Semantics.Montague.toyRel.read

Instances For

The facts #

def Semantics.Montague.ToyFacts.sleep :

ToyEntity → Prop

Equations

Semantics.Montague.ToyFacts.sleep Semantics.Montague.ToyEntity.john = True
Semantics.Montague.ToyFacts.sleep x = False

Instances For

def Semantics.Montague.ToyFacts.laugh :

ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.ToyFacts.student :

ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.ToyFacts.person :

ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.ToyFacts.thing :

ToyEntity → Prop

Equations

Semantics.Montague.ToyFacts.thing x✝ = True

Instances For

def Semantics.Montague.ToyFacts.pizza :

ToyEntity → Prop

Equations

Semantics.Montague.ToyFacts.pizza Semantics.Montague.ToyEntity.pizza = True
Semantics.Montague.ToyFacts.pizza x = False

Instances For

def Semantics.Montague.ToyFacts.book :

ToyEntity → Prop

Equations

Semantics.Montague.ToyFacts.book Semantics.Montague.ToyEntity.book = True
Semantics.Montague.ToyFacts.book x = False

Instances For

def Semantics.Montague.ToyFacts.see :

ToyEntity → ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.ToyFacts.eat :

ToyEntity → ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.ToyFacts.read :

ToyEntity → ToyEntity → Prop

Equations

Instances For

def Semantics.Montague.toyStructure :

toyLang.Structure ToyEntity

The toy structure: constants denote their entities; relations carry the facts (binary relations subject-first).

Equations

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

Instances For

One @[simp] lemma per symbol (mathlib's funMap_add discipline), so proofs reduce RelMap/funMap to the named facts without unfolding the structure.

@[simp]

theorem Semantics.Montague.funMap_john (v : Fin 0 → ToyEntity) :

FirstOrder.Language.Structure.funMap johnConst v = ToyEntity.john

@[simp]

theorem Semantics.Montague.funMap_mary (v : Fin 0 → ToyEntity) :

FirstOrder.Language.Structure.funMap maryConst v = ToyEntity.mary

@[simp]

theorem Semantics.Montague.relMap_sleep (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap sleepRel v = ToyFacts.sleep (v 0)

@[simp]

theorem Semantics.Montague.relMap_laugh (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap laughRel v = ToyFacts.laugh (v 0)

@[simp]

theorem Semantics.Montague.relMap_student (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap studentRel v = ToyFacts.student (v 0)

@[simp]

theorem Semantics.Montague.relMap_person (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap personRel v = ToyFacts.person (v 0)

@[simp]

theorem Semantics.Montague.relMap_thing (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap thingRel v = ToyFacts.thing (v 0)

@[simp]

theorem Semantics.Montague.relMap_pizza (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap pizzaRel v = ToyFacts.pizza (v 0)

@[simp]

theorem Semantics.Montague.relMap_book (v : Fin 1 → ToyEntity) :

FirstOrder.Language.Structure.RelMap bookRel v = ToyFacts.book (v 0)

@[simp]

theorem Semantics.Montague.relMap_see (v : Fin 2 → ToyEntity) :

FirstOrder.Language.Structure.RelMap seeRel v = ToyFacts.see (v 0) (v 1)

@[simp]

theorem Semantics.Montague.relMap_eat (v : Fin 2 → ToyEntity) :

FirstOrder.Language.Structure.RelMap eatRel v = ToyFacts.eat (v 0) (v 1)

@[simp]

theorem Semantics.Montague.relMap_read (v : Fin 2 → ToyEntity) :

FirstOrder.Language.Structure.RelMap readRel v = ToyFacts.read (v 0) (v 1)

def Semantics.Montague.toyModel :

Composition.Model toyLang

The toy composition model: extensional (one world).

Equations

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

Instances For

def Semantics.Montague.toyNaming :

Composition.LexNaming toyLang

The naming maps: word forms into the toy signature.

Equations

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

Instances For

def Semantics.Montague.toyLexicon :

Lexicon ToyEntity Unit

The toy lexicon, induced by the naming maps over the model.

Equations

Semantics.Montague.toyLexicon = Semantics.Montague.toyModel.lexiconAt Semantics.Montague.toyNaming ()

Instances For

theorem Semantics.Montague.toyNaming_disjoint :

toyNaming.Disjoint

The toy naming maps classify each word once.

theorem Semantics.Montague.toyNaming_freshFor :

{ }.FreshFor toyNaming

The default logical vocabulary is fresh for the toy naming maps.

Denotations read off the model. Each is definitionally the corresponding fact predicate over ToyEntity, so rfl/trivial proofs over them reduce.

def Semantics.Montague.ToyLexicon.john_sem :

Intensional.Denot ToyEntity Unit Intensional.Ty.e

Equations

Semantics.Montague.ToyLexicon.john_sem = Semantics.Montague.toyModel.const Semantics.Montague.johnConst ()

Instances For

def Semantics.Montague.ToyLexicon.mary_sem :

Intensional.Denot ToyEntity Unit Intensional.Ty.e

Equations

Semantics.Montague.ToyLexicon.mary_sem = Semantics.Montague.toyModel.const Semantics.Montague.maryConst ()

Instances For

def Semantics.Montague.ToyLexicon.sleeps_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.sleeps_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.sleepRel ()

Instances For

def Semantics.Montague.ToyLexicon.laughs_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.laughs_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.laughRel ()

Instances For

def Semantics.Montague.ToyLexicon.student_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.student_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.studentRel ()

Instances For

def Semantics.Montague.ToyLexicon.person_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.person_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.personRel ()

Instances For

def Semantics.Montague.ToyLexicon.thing_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.thing_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.thingRel ()

Instances For

def Semantics.Montague.ToyLexicon.pizza_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.pizza_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.pizzaRel ()

Instances For

def Semantics.Montague.ToyLexicon.book_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.book_sem = Semantics.Montague.toyModel.pred₁ext Semantics.Montague.bookRel ()

Instances For

def Semantics.Montague.ToyLexicon.sees_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.sees_sem = Semantics.Montague.toyModel.pred₂ext Semantics.Montague.seeRel ()

Instances For

def Semantics.Montague.ToyLexicon.eats_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.eats_sem = Semantics.Montague.toyModel.pred₂ext Semantics.Montague.eatRel ()

Instances For

def Semantics.Montague.ToyLexicon.reads_sem :

Intensional.Denot ToyEntity Unit (Intensional.Ty.e ⇒ Intensional.Ty.e ⇒ Intensional.Ty.t)

Equations

Semantics.Montague.ToyLexicon.reads_sem = Semantics.Montague.toyModel.pred₂ext Semantics.Montague.readRel ()

Instances For

@[implicit_reducible]

instance Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEStudent_sem :

DecidablePred student_sem

Equations

One or more equations did not get rendered due to their size.
Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEStudent_sem Semantics.Montague.ToyEntity.john = isTrue trivial
Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEStudent_sem Semantics.Montague.ToyEntity.mary = isTrue trivial

@[implicit_reducible]

instance Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEPerson_sem :

DecidablePred person_sem

Equations

One or more equations did not get rendered due to their size.
Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEPerson_sem Semantics.Montague.ToyEntity.john = isTrue trivial
Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEPerson_sem Semantics.Montague.ToyEntity.mary = isTrue trivial

@[implicit_reducible]

instance Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEThing_sem :

DecidablePred thing_sem

Equations

Semantics.Montague.ToyLexicon.instDecidablePredDenotToyEntityUnitEThing_sem x✝ = isTrue trivial