inductive Minimalism.RelativeClauses.ReadEntity : Type

A model for the "book that John read" example.

Domain: john, mary, book1, book2, newspaper

• john : ReadEntity
• mary : ReadEntity
• book1 : ReadEntity
• book2 : ReadEntity
• newspaper : ReadEntity

instance Minimalism.RelativeClauses.instReprReadEntity : Repr ReadEntity

Equations

• Minimalism.RelativeClauses.instReprReadEntity = { reprPrec := Minimalism.RelativeClauses.instReprReadEntity.repr }

def Minimalism.RelativeClauses.instReprReadEntity.repr : ReadEntity → ℕ → Std.Format

Equations

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

instance Minimalism.RelativeClauses.instDecidableEqReadEntity : DecidableEq ReadEntity

Equations

• Minimalism.RelativeClauses.instDecidableEqReadEntity x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def Minimalism.RelativeClauses.instInhabitedReadEntity.default : ReadEntity

Equations

• Minimalism.RelativeClauses.instInhabitedReadEntity.default = Minimalism.RelativeClauses.ReadEntity.john

instance Minimalism.RelativeClauses.instInhabitedReadEntity : Inhabited ReadEntity

Equations

• Minimalism.RelativeClauses.instInhabitedReadEntity = { default := Minimalism.RelativeClauses.instInhabitedReadEntity.default }

def Minimalism.RelativeClauses.readModel : Semantics.Montague.Model

The model for our example

Equations

• Minimalism.RelativeClauses.readModel = { Entity := Minimalism.RelativeClauses.ReadEntity, decEq := inferInstance }

def Minimalism.RelativeClauses.john_sem : readModel.interpTy Semantics.Montague.Ty.e

"John" denotes the entity john

Equations

• Minimalism.RelativeClauses.john_sem = Minimalism.RelativeClauses.ReadEntity.john

def Minimalism.RelativeClauses.mary_sem : readModel.interpTy Semantics.Montague.Ty.e

"Mary" denotes the entity mary

Equations

• Minimalism.RelativeClauses.mary_sem = Minimalism.RelativeClauses.ReadEntity.mary

def Minimalism.RelativeClauses.book_sem : readModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

"book" is true of book1 and book2

Equations

• Minimalism.RelativeClauses.book_sem Minimalism.RelativeClauses.ReadEntity.book1 = true
• Minimalism.RelativeClauses.book_sem Minimalism.RelativeClauses.ReadEntity.book2 = true
• Minimalism.RelativeClauses.book_sem x = false

def Minimalism.RelativeClauses.read_sem : readModel.interpTy (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

"read" as a relation: John read book1, Mary read book2

Equations

• Minimalism.RelativeClauses.read_sem Minimalism.RelativeClauses.ReadEntity.book1 Minimalism.RelativeClauses.ReadEntity.john = true
• Minimalism.RelativeClauses.read_sem Minimalism.RelativeClauses.ReadEntity.book2 Minimalism.RelativeClauses.ReadEntity.mary = true
• Minimalism.RelativeClauses.read_sem Minimalism.RelativeClauses.ReadEntity.newspaper Minimalism.RelativeClauses.ReadEntity.mary = true
• Minimalism.RelativeClauses.read_sem obj subj = false

def Minimalism.RelativeClauses.trace1 : Semantics.Montague.Variables.DenotG readModel Semantics.Montague.Ty.e

The trace in object position: t₁

This represents the gap in "that John read _". The trace has index 1.

Equations

• Minimalism.RelativeClauses.trace1 = Minimalism.Semantics.interpTrace 1

def Minimalism.RelativeClauses.vp_readTrace : Semantics.Montague.Variables.DenotG readModel (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

VP meaning: "read t₁"

⟦read t₁⟧^g = λy. read(g(1))(y) = λy. read(y, g(1))

Note: Our read_sem takes object first, then subject. So "read t₁" is the function waiting for a subject.

Equations

• Minimalism.RelativeClauses.vp_readTrace g subj = Minimalism.RelativeClauses.read_sem (Minimalism.RelativeClauses.trace1 g) subj

def Minimalism.RelativeClauses.ip_johnReadTrace : Semantics.Montague.Variables.DenotG readModel Semantics.Montague.Ty.t

IP meaning: "John read t₁"

⟦John read t₁⟧^g = read(j, g(1))

Equations

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

theorem Minimalism.RelativeClauses.ip_meaning_correct (g : Semantics.Montague.Variables.Assignment readModel) : ip_johnReadTrace g = read_sem (g 1) ReadEntity.john

Verify IP meaning: it's true iff the trace's value was read by John

def Minimalism.RelativeClauses.cp_relativeClause : Semantics.Montague.Variables.DenotG readModel (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

CP meaning via Predicate Abstraction: "Op₁ [John read t₁]"

⟦Op₁ [John read t₁]⟧^g = λx. ⟦John read t₁⟧^{g[1↦x]} = λx. read(j, x)

This creates a predicate "things that John read".

Equations

• Minimalism.RelativeClauses.cp_relativeClause = Minimalism.Semantics.predicateAbstraction 1 Minimalism.RelativeClauses.ip_johnReadTrace

theorem Minimalism.RelativeClauses.cp_meaning_correct (g : Semantics.Montague.Variables.Assignment readModel) (x : ReadEntity) : cp_relativeClause g x = read_sem x ReadEntity.john

Verify CP meaning: λx. read(j, x)

def Minimalism.RelativeClauses.book_denot : Semantics.Montague.Variables.DenotG readModel (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Head noun "book" as assignment-relative (trivially constant)

Equations

• Minimalism.RelativeClauses.book_denot = Semantics.Montague.Variables.constDenot Minimalism.RelativeClauses.book_sem

def Minimalism.RelativeClauses.np_bookThatJohnRead : Semantics.Montague.Variables.DenotG readModel (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

NP meaning: "book that John read _"

Via Predicate Modification: ⟦book [that John read _]⟧ = λx. book(x) ∧ read(j, x)

Equations

• Minimalism.RelativeClauses.np_bookThatJohnRead = Minimalism.Semantics.relativePM 1 Minimalism.RelativeClauses.book_denot Minimalism.RelativeClauses.ip_johnReadTrace

theorem Minimalism.RelativeClauses.np_meaning_correct (g : Semantics.Montague.Variables.Assignment readModel) (x : ReadEntity) : np_bookThatJohnRead g x = (book_sem x && read_sem x ReadEntity.john)

The NP meaning is the intersection of "book" and "things John read"

def Minimalism.RelativeClauses.iota (candidates : List ReadEntity) (p : ReadEntity → Bool) : Option ReadEntity

The iota operator: ιx.P(x)

Returns the unique x satisfying P, if one exists. For computational simplicity, we search through a list of candidates.

Equations

• Minimalism.RelativeClauses.iota candidates p = match List.filter p candidates with | [x] => some x | x => none

def Minimalism.RelativeClauses.allEntities : List ReadEntity

All entities in our domain

Equations

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

def Minimalism.RelativeClauses.the_book_that_john_read (g : Semantics.Montague.Variables.Assignment readModel) : Option ReadEntity

"the book that John read" denotes book1

This is the unique entity satisfying: book(x) ∧ read(j, x)

Equations

• Minimalism.RelativeClauses.the_book_that_john_read g = Minimalism.RelativeClauses.iota Minimalism.RelativeClauses.allEntities (Minimalism.RelativeClauses.np_bookThatJohnRead g)

theorem Minimalism.RelativeClauses.the_book_correct (g : Semantics.Montague.Variables.Assignment readModel) : the_book_that_john_read g = some ReadEntity.book1

Main theorem: "the book that John read" denotes book1

This shows the compositional derivation yields the correct result:

• book1 is a book
• John read book1
• No other book was read by John
• Therefore ιx[book(x) ∧ read(j,x)] = book1

theorem Minimalism.RelativeClauses.relClause_extension (g : Semantics.Montague.Variables.Assignment readModel) : cp_relativeClause g ReadEntity.book1 = true ∧ cp_relativeClause g ReadEntity.book2 = false ∧ cp_relativeClause g ReadEntity.newspaper = false

The relative clause creates the right predicate: it's true of exactly the things John read.

theorem Minimalism.RelativeClauses.np_extension (g : Semantics.Montague.Variables.Assignment readModel) : np_bookThatJohnRead g ReadEntity.book1 = true ∧ np_bookThatJohnRead g ReadEntity.book2 = false ∧ np_bookThatJohnRead g ReadEntity.john = false

The modified NP is true of exactly book1.

theorem Minimalism.RelativeClauses.np_assignment_independent (g₁ g₂ : Semantics.Montague.Variables.Assignment readModel) : np_bookThatJohnRead g₁ = np_bookThatJohnRead g₂

Assignment independence: the final NP meaning doesn't depend on the assignment (all variables are bound).

def Minimalism.RelativeClauses.np_bookThatJohnRead' : Semantics.Montague.Variables.DenotG readModel (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

An equivalent formulation using the relativePM combinator directly. This shows the interface abstracts over the composition steps.

Equations

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

theorem Minimalism.RelativeClauses.np_formulations_equiv (g : Semantics.Montague.Variables.Assignment readModel) : np_bookThatJohnRead g = np_bookThatJohnRead' g

The two formulations are equivalent

def Minimalism.RelativeClauses.traceExample : SyntacticObject

The syntactic structure with a trace.

This shows how the semantic derivation corresponds to the syntax: the trace created via mkTrace 1 is interpreted via interpTrace 1.

Equations

• Minimalism.RelativeClauses.traceExample = Minimalism.mkTrace 1

theorem Minimalism.RelativeClauses.trace_example_has_index : Semantics.getTraceIndex traceExample = some 1

Extracting the trace index from a syntactic object.