structure Semantics.Composition.Tree.TypedDenot (m : Montague.Model) : Type

• ty : Montague.Ty
• val : m.interpTy self.ty

def Semantics.Composition.Tree.canApply (funTy argTy : Montague.Ty) : Option Montague.Ty

Equations

• Semantics.Composition.Tree.canApply (σ ⇒ τ) argTy = if σ = argTy then some τ else none
• Semantics.Composition.Tree.canApply funTy argTy = none

def Semantics.Composition.Tree.interpTerminal (m : Montague.Model) (lex : Montague.Lexicon m) (word : String) : Option (TypedDenot m)

TN: lexical lookup.

Equations

• Semantics.Composition.Tree.interpTerminal m lex word = Option.map (fun (entry : Semantics.Montague.LexEntry m) => { ty := entry.ty, val := entry.denot }) (lex word)

def Semantics.Composition.Tree.interpNonBranching {m : Montague.Model} (daughter : TypedDenot m) : TypedDenot m

NN: identity.

Equations

• Semantics.Composition.Tree.interpNonBranching daughter = daughter

def Semantics.Composition.Tree.interpFA {m : Montague.Model} {σ τ : Montague.Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : m.interpTy τ

FA: ⟦β⟧(⟦γ⟧)

Equations

• Semantics.Composition.Tree.interpFA f x = f x

def Semantics.Composition.Tree.tryFA {m : Montague.Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

Try FA in both orders.

Equations

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

def Semantics.Composition.Tree.tryPM {m : Montague.Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

PM: combine two ⟨e,t⟩ predicates.

Equations

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

def Semantics.Composition.Tree.interpBinary {m : Montague.Model} (d1 d2 : TypedDenot m) : Option (TypedDenot m)

Binary node: try FA, then PM.

Equations

• Semantics.Composition.Tree.interpBinary d1 d2 = (Semantics.Composition.Tree.tryFA d1 d2 <|> Semantics.Composition.Tree.tryPM d1 d2)

def Semantics.Composition.Tree.interp {C : Type} (m : Montague.Model) (lex : Montague.Lexicon m) (g : Montague.Variables.Assignment m) : Core.Tree.Tree C String → Option (TypedDenot m)

Interpret a tree under an assignment.

Implements @cite{heim-kratzer-1998} Ch. 3-5 type-driven interpretation:

• TN: terminal → lexical lookup
• NN: unary node → identity
• FA/PM: binary node → try FA then PM
• Traces/Pronouns: ⟦tₙ⟧^g = g(n)
• Predicate Abstraction (PA): ⟦[n β]⟧^g = λx. ⟦β⟧^{g[n↦x]}

PA is the key to quantifier scope: after QR moves a quantifier DP to a higher position, PA abstracts over the trace it leaves behind, producing a predicate that the quantifier can take as its scope argument.

The category parameter C is ignored during interpretation — composition is type-driven, not category-driven. This means the same function works for Tree Cat String (UD-grounded), Tree Unit String (category-free), or any other category system.

Equations

• One or more equations did not get rendered due to their size.
• Semantics.Composition.Tree.interp m lex g (Core.Tree.Tree.terminal a w) = Semantics.Composition.Tree.interpTerminal m lex w
• Semantics.Composition.Tree.interp m lex g (Core.Tree.Tree.node a [t]) = Option.map Semantics.Composition.Tree.interpNonBranching (Semantics.Composition.Tree.interp m lex g t)
• Semantics.Composition.Tree.interp m lex g (Core.Tree.Tree.node a a_1) = none
• Semantics.Composition.Tree.interp m lex g (Core.Tree.Tree.trace n a) = some { ty := Semantics.Montague.Ty.e, val := g n }

def Semantics.Composition.Tree.evalTree {C : Type} {m : Montague.Model} (lex : Montague.Lexicon m) (g : Montague.Variables.Assignment m) (t : Core.Tree.Tree C String) : Option Bool

Extract truth value from tree interpretation.

Equations

• Semantics.Composition.Tree.evalTree lex g t = match Semantics.Composition.Tree.interp m lex g t with | some { ty := Semantics.Montague.Ty.t, val := b } => some b | x => none

def Semantics.Composition.Tree.evalTreeProp {C : Type} {m : Montague.Model} (lex : Montague.Lexicon m) (g : Montague.Variables.Assignment m) (t : Core.Tree.Tree C String) : Option (m.World → Bool)

Extract proposition (s→t) from tree interpretation.

For intensional trees where the root denotes a proposition rather than a bare truth value — e.g., trees containing EXH or other propositional operators. Evaluate the result at a specific world to get a truth value.

Equations

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

theorem Semantics.Composition.Tree.interpNonBranching_id {m : Montague.Model} (d : TypedDenot m) : interpNonBranching d = d

theorem Semantics.Composition.Tree.interpFA_type {m : Montague.Model} {σ τ : Montague.Ty} (f : m.interpTy (σ ⇒ τ)) (x : m.interpTy σ) : interpFA f x = f x

theorem Semantics.Composition.Tree.tryPM_preserves_type {m : Montague.Model} (d1 d2 : TypedDenot m) (h1 : d1.ty = (Montague.Ty.e ⇒ Montague.Ty.t)) (h2 : d2.ty = (Montague.Ty.e ⇒ Montague.Ty.t)) : ∃ (d : TypedDenot m), tryPM d1 d2 = some d ∧ d.ty = (Montague.Ty.e ⇒ Montague.Ty.t)

theorem Semantics.Composition.Tree.interpBinary_eq {m : Montague.Model} (d1 d2 : TypedDenot m) : interpBinary d1 d2 = (tryFA d1 d2).orElse fun (x : Unit) => tryPM d1 d2