def Minimalism.Semantics.interpTrace {m : Semantics.Montague.Model} (n : ℕ) : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.e

Interpret a trace as a variable: ⟦t_n⟧^g = g(n)

Heim and Kratzer's trace interpretation rule: traces left by movement are semantically identical to pronouns. Both are interpreted by looking up the assignment function at the appropriate index.

The trace index n should match the index of the binder (λ-abstraction) at the landing site of movement.

Equations

• Minimalism.Semantics.interpTrace n = Semantics.Montague.Variables.interpPronoun n

theorem Minimalism.Semantics.interpTrace_eq_interpPronoun {m : Semantics.Montague.Model} (n : ℕ) : interpTrace n = Semantics.Montague.Variables.interpPronoun n

Traces and pronouns have the same interpretation

def Minimalism.Semantics.predicateAbstraction {m : Semantics.Montague.Model} (n : ℕ) (body : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.t) : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Predicate Abstraction: λ-bind at the landing site of movement.

When a moved element lands at a position, it creates a λ-abstractor that binds the trace it left behind:

⟦[XP Op_n YP]⟧^g = λx. ⟦YP⟧^{g[n↦x]}

where Op_n is the moved operator and YP contains the trace t_n.

This rule creates a predicate (type ⟨e,t⟩) from a proposition (type t) by abstracting over the trace's index.

Equations

• Minimalism.Semantics.predicateAbstraction n body = Semantics.Montague.Variables.lambdaAbsG n body

def Minimalism.Semantics.predicateAbstractionGen {m : Semantics.Montague.Model} {τ : Semantics.Montague.Ty} (n : ℕ) (body : Semantics.Montague.Variables.DenotG m τ) : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ τ)

Generalized predicate abstraction for any result type.

This handles cases like "the book that John said Mary read _" where the trace is embedded and the result may need further composition.

Equations

• Minimalism.Semantics.predicateAbstractionGen n body = Semantics.Montague.Variables.lambdaAbsG n body

def Minimalism.Semantics.interpMovement {m : Semantics.Montague.Model} (n : ℕ) (bodyWithTrace : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.t) : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Interpret a simple movement configuration:

• A trace t_n in some position
• An operator binding that trace from a higher position

Returns the predicate λx. ⟦body(t_n := x)⟧

Equations

• Minimalism.Semantics.interpMovement n bodyWithTrace = Minimalism.Semantics.predicateAbstraction n bodyWithTrace

theorem Minimalism.Semantics.binding_correct {m : Semantics.Montague.Model} (n : ℕ) (body : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.t) (x : m.Entity) (g : Semantics.Montague.Variables.Assignment m) : predicateAbstraction n body g x = body (g.update n x)

The binding relationship: predicate abstraction at index n binds traces at n.

When we apply a predicate-abstracted meaning to an entity, that entity becomes the value of all traces with the same index.

structure Minimalism.Semantics.InterpContext (m : Semantics.Montague.Model) : Type

A semantic interpretation context pairs a model with an assignment.

• assignment : Semantics.Montague.Variables.Assignment m

def Minimalism.Semantics.soSemanticType (so : SyntacticObject) : Option Semantics.Montague.Ty

The semantic type corresponding to a syntactic object.

• Traces have type e (they denote entities)
• Other SOs need lexical lookup

Equations

• Minimalism.Semantics.soSemanticType so = match Minimalism.isTrace so with | some val => some Semantics.Montague.Ty.e | none => none

def Minimalism.Semantics.interpSOTrace {m : Semantics.Montague.Model} (so : SyntacticObject) : Option (Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.e)

Interpret a trace in a syntactic object.

This extracts the trace index and interprets it via the assignment.

Equations

• Minimalism.Semantics.interpSOTrace so = match Minimalism.isTrace so with | some n => some (Minimalism.Semantics.interpTrace n) | none => none

def Minimalism.Semantics.getTraceIndex : SyntacticObject → Option ℕ

Get the trace index from a syntactic object (searches recursively).

Equations

• Minimalism.Semantics.getTraceIndex (Minimalism.SyntacticObject.leaf tok) = if tok.id ≥ 10000 then some (tok.id - 10000) else none
• Minimalism.Semantics.getTraceIndex (a.node b) = (Minimalism.Semantics.getTraceIndex a <|> Minimalism.Semantics.getTraceIndex b)

theorem Minimalism.Semantics.trace_index_determines_meaning {m : Semantics.Montague.Model} (n : ℕ) : interpTrace n = interpTrace n

Identity of indiscernibles for traces: traces with the same index have the same interpretation.

theorem Minimalism.Semantics.trace_indices_independent {m : Semantics.Montague.Model} (n₁ n₂ : ℕ) (h : n₁ ≠ n₂) (x : m.Entity) (g : Semantics.Montague.Variables.Assignment m) : interpTrace n₁ (g.update n₂ x) = interpTrace n₁ g

Different indices yield independent interpretations.

theorem Minimalism.Semantics.abstraction_binds_correct_variable {m : Semantics.Montague.Model} (n : ℕ) (g : Semantics.Montague.Variables.Assignment m) (x : m.Entity) : interpTrace n (g.update n x) = x

Predicate abstraction creates the right binding: the abstracted variable is bound, other variables are free.

def Minimalism.Semantics.relativePM {m : Semantics.Montague.Model} (n : ℕ) (headNoun : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (relClauseBody : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.t) : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)

Relative clause interpretation combines predicate abstraction with PM.

For "the N that... t..."":

1. Interpret the relative clause as λx. ⟦... t_n...⟧^{g[n↦x]}
2. Combine with the head noun via Predicate Modification

Result: λx. N(x) ∧ ⟦relative clause⟧(x)

Equations

• Minimalism.Semantics.relativePM n headNoun relClauseBody g = headNoun g ⊓ₚ Minimalism.Semantics.predicateAbstraction n relClauseBody g

theorem Minimalism.Semantics.relativePM_comm {m : Semantics.Montague.Model} (n : ℕ) (headNoun : Semantics.Montague.Variables.DenotG m (Semantics.Montague.Ty.e ⇒ Semantics.Montague.Ty.t)) (relClauseBody : Semantics.Montague.Variables.DenotG m Semantics.Montague.Ty.t) (g : Semantics.Montague.Variables.Assignment m) : relativePM n headNoun relClauseBody g = predicateAbstraction n relClauseBody g ⊓ₚ headNoun g

Relative PM is commutative (the order of N and RC doesn't matter)