Trace Interpretation

@cite{heim-kratzer-1998}

Traces left by movement are interpreted as variables bound by λ-abstraction at the landing site (H&K Ch. 5, 7).

Rules

1. Trace Interpretation: a trace t_n is interpreted as g(n) ⟦t_n⟧^g = g(n)

2. Predicate Abstraction: at the landing site of movement, λ-abstract over the trace's index ⟦[CP Op_n ... t_n ...]⟧^g = λx. ⟦... t_n ...⟧^{g[n↦x]}

Trace convention

Traces are encoded as SyntacticObject.leaf with id ≥ 10000. The trace index is id - 10000. Created via mkTrace n, detected via isTrace so.

@[reducible, inline]

abbrev Minimalist.interpTrace {F : Core.Logic.Intensional.Frame} (n : ℕ) : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.e

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

Heim and Kratzer's trace interpretation rule: traces and pronouns are semantically identical, looked up via the assignment function. The trace index n matches the binder (λ-abstraction) at the landing site of movement.

abbrev because trace interpretation IS pronoun interpretation — the only difference is the syntactic source.

Equations

• Minimalist.interpTrace n = Core.Logic.Intensional.Variables.interpPronoun n

def Minimalist.predicateAbstraction {F : Core.Logic.Intensional.Frame} (n : ℕ) (body : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.t) : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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

• Minimalist.predicateAbstraction n body = Core.Logic.Intensional.Variables.lambdaAbsG n body

def Minimalist.predicateAbstractionGen {F : Core.Logic.Intensional.Frame} {τ : Core.Logic.Intensional.Ty} (n : ℕ) (body : Core.Logic.Intensional.Variables.DenotG F τ) : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.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

• Minimalist.predicateAbstractionGen n body = Core.Logic.Intensional.Variables.lambdaAbsG n body

def Minimalist.interpMovement {F : Core.Logic.Intensional.Frame} (n : ℕ) (bodyWithTrace : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.t) : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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

• Minimalist.interpMovement n bodyWithTrace = Minimalist.predicateAbstraction n bodyWithTrace

theorem Minimalist.binding_correct {F : Core.Logic.Intensional.Frame} (n : ℕ) (body : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.t) (x : F.Entity) (g : Core.Assignment F.Entity) : 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 Minimalist.InterpContext (F : Core.Logic.Intensional.Frame) : Type

A semantic interpretation context pairs a model with an assignment.

• assignment : Core.Assignment F.Entity

def Minimalist.soSemanticType (so : SyntacticObject) : Option Core.Logic.Intensional.Ty

The semantic type corresponding to a syntactic object.

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

Equations

• Minimalist.soSemanticType so = match Minimalist.isTrace so with | some val => some Core.Logic.Intensional.Ty.e | none => none

def Minimalist.interpSOTrace {F : Core.Logic.Intensional.Frame} (so : SyntacticObject) : Option (Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.e)

Interpret a trace in a syntactic object.

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

Equations

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

def Minimalist.traceIndices : SyntacticObject → Multiset ℕ

All trace indices appearing in an SO, as a Multiset (multiplicity preserved, order-blind).

Equations

• Minimalist.traceIndices = FreeCommMagma.lift Minimalist.traceIndicesAux✝ Minimalist.traceIndicesAux_respects✝

@[simp]

theorem Minimalist.traceIndices_leaf (tok : LIToken) : traceIndices (SyntacticObject.leaf tok) = 0

@[simp]

theorem Minimalist.traceIndices_trace (n : ℕ) : traceIndices (SyntacticObject.trace n) = {n}

@[simp]

theorem Minimalist.traceIndices_mul (l r : SyntacticObject) : traceIndices (l * r) = traceIndices l + traceIndices r

noncomputable def Minimalist.getTraceIndex (so : SyntacticObject) : Option ℕ

Extract a trace index, returning none if the SO has no traces. For single-trace SOs returns the unique index; for multi-trace SOs, returns some index (the first in Multiset.toList's arbitrary enumeration). Use traceIndices directly for the canonical multiset.

Noncomputable because Multiset.toList is.

Equations

• Minimalist.getTraceIndex so = (Minimalist.traceIndices so).toList.head?

theorem Minimalist.trace_indices_independent {F : Core.Logic.Intensional.Frame} (n₁ n₂ : ℕ) (h : n₁ ≠ n₂) (x : F.Entity) (g : Core.Assignment F.Entity) : interpTrace n₁ (g.update n₂ x) = interpTrace n₁ g

Different indices yield independent interpretations.

theorem Minimalist.abstraction_binds_correct_variable {F : Core.Logic.Intensional.Frame} (n : ℕ) (g : Core.Assignment F.Entity) (x : F.Entity) : interpTrace n (g.update n x) = x

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

def Minimalist.relativePM {F : Core.Logic.Intensional.Frame} (n : ℕ) (headNoun : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (relClauseBody : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.t) : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.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

• Minimalist.relativePM n headNoun relClauseBody g = headNoun g ⊓ₚ Minimalist.predicateAbstraction n relClauseBody g

theorem Minimalist.relativePM_comm {F : Core.Logic.Intensional.Frame} (n : ℕ) (headNoun : Core.Logic.Intensional.Variables.DenotG F (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (relClauseBody : Core.Logic.Intensional.Variables.DenotG F Core.Logic.Intensional.Ty.t) (g : Core.Assignment F.Entity) : relativePM n headNoun relClauseBody g = predicateAbstraction n relClauseBody g ⊓ₚ headNoun g

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