Relative Clause Semantics: A Worked Example

Demonstrates the full machinery from Syntax/Minimalist/TraceInterpretation.lean with a concrete linguistic example: "the book that John read _"

The Derivation

                  DP
                 / \
               the NP
                    / \
                  book CP
                       / \
                      Op₁ IP
                          / \
                       John VP
                             / \
                           read t₁

Semantic Composition

1. Trace interpretation: ⟦t₁⟧^g = g(1)
2. VP composition: ⟦read t₁⟧^g = read(g(1)) (applied to subject later)
3. IP composition: ⟦John read t₁⟧^g = read(j, g(1))
4. Predicate Abstraction at CP: ⟦Op₁ [John read t₁]⟧^g = λx. read(j, x)
5. Predicate Modification with head noun: λx. book(x) ∧ read(j, x)
6. Definite description: ιx[book(x) ∧ read(j,x)]

inductive Minimalist.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

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

Equations

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

@[implicit_reducible]

instance Minimalist.RelativeClauses.instReprReadEntity : Repr ReadEntity

Equations

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

@[implicit_reducible]

instance Minimalist.RelativeClauses.instDecidableEqReadEntity : DecidableEq ReadEntity

Equations

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

@[implicit_reducible]

instance Minimalist.RelativeClauses.instInhabitedReadEntity : Inhabited ReadEntity

Equations

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

def Minimalist.RelativeClauses.instInhabitedReadEntity.default : ReadEntity

Equations

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

def Minimalist.RelativeClauses.readModel : Core.Logic.Intensional.Frame

The model for our example

Equations

• Minimalist.RelativeClauses.readModel = { Entity := Minimalist.RelativeClauses.ReadEntity, Index := Unit }

def Minimalist.RelativeClauses.john_sem : readModel.Denot Core.Logic.Intensional.Ty.e

"John" denotes the entity john

Equations

• Minimalist.RelativeClauses.john_sem = Minimalist.RelativeClauses.ReadEntity.john

def Minimalist.RelativeClauses.mary_sem : readModel.Denot Core.Logic.Intensional.Ty.e

"Mary" denotes the entity mary

Equations

• Minimalist.RelativeClauses.mary_sem = Minimalist.RelativeClauses.ReadEntity.mary

def Minimalist.RelativeClauses.book_sem : readModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

"book" is true of book1 and book2

Equations

• Minimalist.RelativeClauses.book_sem Minimalist.RelativeClauses.ReadEntity.book1 = True
• Minimalist.RelativeClauses.book_sem Minimalist.RelativeClauses.ReadEntity.book2 = True
• Minimalist.RelativeClauses.book_sem x = False

def Minimalist.RelativeClauses.read_sem : readModel.Denot (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

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

Equations

• Minimalist.RelativeClauses.read_sem Minimalist.RelativeClauses.ReadEntity.book1 Minimalist.RelativeClauses.ReadEntity.john = True
• Minimalist.RelativeClauses.read_sem Minimalist.RelativeClauses.ReadEntity.book2 Minimalist.RelativeClauses.ReadEntity.mary = True
• Minimalist.RelativeClauses.read_sem Minimalist.RelativeClauses.ReadEntity.newspaper Minimalist.RelativeClauses.ReadEntity.mary = True
• Minimalist.RelativeClauses.read_sem obj subj = False

@[implicit_reducible]

instance Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem : DecidablePred book_sem

Equations

• Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem Minimalist.RelativeClauses.ReadEntity.book1 = isTrue trivial
• Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem Minimalist.RelativeClauses.ReadEntity.book2 = isTrue trivial
• Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem Minimalist.RelativeClauses.ReadEntity.john = isFalse not_false
• Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem Minimalist.RelativeClauses.ReadEntity.mary = isFalse not_false
• Minimalist.RelativeClauses.instDecidablePredDenotReadModelEBook_sem Minimalist.RelativeClauses.ReadEntity.newspaper = isFalse not_false

@[implicit_reducible]

instance Minimalist.RelativeClauses.instDecidablePredDenotReadModelERead_sem (obj : ReadEntity) : DecidablePred (read_sem obj)

Equations

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

def Minimalist.RelativeClauses.trace1 : Core.Logic.Intensional.Variables.DenotG readModel Core.Logic.Intensional.Ty.e

The trace in object position: t₁

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

Equations

• Minimalist.RelativeClauses.trace1 = Minimalist.interpTrace 1

def Minimalist.RelativeClauses.vp_readTrace : Core.Logic.Intensional.Variables.DenotG readModel (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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

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

def Minimalist.RelativeClauses.ip_johnReadTrace : Core.Logic.Intensional.Variables.DenotG readModel Core.Logic.Intensional.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 Minimalist.RelativeClauses.ip_meaning_correct (g : Core.Assignment readModel.Entity) : 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 Minimalist.RelativeClauses.cp_relativeClause : Core.Logic.Intensional.Variables.DenotG readModel (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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

• Minimalist.RelativeClauses.cp_relativeClause = Minimalist.predicateAbstraction 1 Minimalist.RelativeClauses.ip_johnReadTrace

theorem Minimalist.RelativeClauses.cp_meaning_correct (g : Core.Assignment readModel.Entity) (x : ReadEntity) : cp_relativeClause g x = read_sem x ReadEntity.john

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

def Minimalist.RelativeClauses.book_denot : Core.Logic.Intensional.Variables.DenotG readModel (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

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

Equations

• Minimalist.RelativeClauses.book_denot = Core.Logic.Intensional.Variables.constDenot Minimalist.RelativeClauses.book_sem

def Minimalist.RelativeClauses.np_bookThatJohnRead : Core.Logic.Intensional.Variables.DenotG readModel (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

NP meaning: "book that John read _"

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

Equations

• Minimalist.RelativeClauses.np_bookThatJohnRead = Minimalist.relativePM 1 Minimalist.RelativeClauses.book_denot Minimalist.RelativeClauses.ip_johnReadTrace

theorem Minimalist.RelativeClauses.np_meaning_correct (g : Core.Assignment readModel.Entity) (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 Minimalist.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

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

def Minimalist.RelativeClauses.allEntities : List ReadEntity

All entities in our domain

Equations

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

def Minimalist.RelativeClauses.the_book_that_john_read (_g : Core.Assignment readModel.Entity) : Option ReadEntity

"the book that John read" denotes book1

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

Equations

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

theorem Minimalist.RelativeClauses.the_book_correct (g : Core.Assignment readModel.Entity) : 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 Minimalist.RelativeClauses.relClause_extension (g : Core.Assignment readModel.Entity) : cp_relativeClause g ReadEntity.book1 ∧ ¬cp_relativeClause g ReadEntity.book2 ∧ ¬cp_relativeClause g ReadEntity.newspaper

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

theorem Minimalist.RelativeClauses.np_extension (g : Core.Assignment readModel.Entity) : np_bookThatJohnRead g ReadEntity.book1 ∧ ¬np_bookThatJohnRead g ReadEntity.book2 ∧ ¬np_bookThatJohnRead g ReadEntity.john

The modified NP is true of exactly book1.

theorem Minimalist.RelativeClauses.np_assignment_independent (g₁ g₂ : Core.Assignment readModel.Entity) : np_bookThatJohnRead g₁ = np_bookThatJohnRead g₂

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

def Minimalist.RelativeClauses.np_bookThatJohnRead' : Core.Logic.Intensional.Variables.DenotG readModel (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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 Minimalist.RelativeClauses.np_formulations_equiv (g : Core.Assignment readModel.Entity) : np_bookThatJohnRead g = np_bookThatJohnRead' g

The two formulations are equivalent

def Minimalist.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

• Minimalist.RelativeClauses.traceExample = Minimalist.mkTrace 1

theorem Minimalist.RelativeClauses.trace_example_has_index : getTraceIndex traceExample = some 1

Extracting the trace index from a syntactic object.