structure Semantics.Composition.Tree.TypedDenot (F : Core.Logic.Intensional.Frame) : Type

• ty : Core.Logic.Intensional.Ty
• val : F.Denot self.ty

def Semantics.Composition.Tree.canApply (funTy argTy : Core.Logic.Intensional.Ty) : Option Core.Logic.Intensional.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 (F : Core.Logic.Intensional.Frame) (lex : Montague.Lexicon F) (word : String) : Option (TypedDenot F)

TN: lexical lookup.

Equations

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

def Semantics.Composition.Tree.interpNonBranching {F : Core.Logic.Intensional.Frame} (daughter : TypedDenot F) : TypedDenot F

NN: identity.

Equations

• Semantics.Composition.Tree.interpNonBranching daughter = daughter

def Semantics.Composition.Tree.interpFA {F : Core.Logic.Intensional.Frame} {σ τ : Core.Logic.Intensional.Ty} (f : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : F.Denot τ

FA: ⟦β⟧(⟦γ⟧)

Equations

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

def Semantics.Composition.Tree.tryFA {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) : Option (TypedDenot F)

Try FA in both orders.

Equations

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

def Semantics.Composition.Tree.tryIFA {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) : Option (TypedDenot F)

IFA: Intensional Functional Application (@cite{von-fintel-heim-2011} Step 10).

If β expects an intension ⟨s,σ⟩ as argument and γ has type σ, then ⟦α⟧ = ⟦β⟧(^⟦γ⟧) — we wrap γ's denotation in up (rigid intension) before applying. This lets intensional operators (modals, attitude verbs) take the intension of their sister as argument via type-driven composition.

Tries both orders (β,γ) and (γ,β).

Equations

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

def Semantics.Composition.Tree.tryPM {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) : Option (TypedDenot F)

PM: combine two ⟨e,t⟩ predicates.

Equations

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

def Semantics.Composition.Tree.interpBinary {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) : Option (TypedDenot F)

Binary node: try FA, then IFA, then PM.

Equations

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

def Semantics.Composition.Tree.interp {C : Type} (F : Core.Logic.Intensional.Frame) (lex : Montague.Lexicon F) (g : Core.Assignment F.Entity) : Core.Tree.Tree C String → Option (TypedDenot F)

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 F lex g (Core.Tree.Tree.terminal a w) = Semantics.Composition.Tree.interpTerminal F lex w
• Semantics.Composition.Tree.interp F lex g (Core.Tree.Tree.node a [t]) = Option.map Semantics.Composition.Tree.interpNonBranching (Semantics.Composition.Tree.interp F lex g t)
• Semantics.Composition.Tree.interp F lex g (Core.Tree.Tree.node a a_1) = none
• Semantics.Composition.Tree.interp F lex g (Core.Tree.Tree.trace n a) = some { ty := Core.Logic.Intensional.Ty.e, val := g n }

def Semantics.Composition.Tree.evalTree {C : Type} {F : Core.Logic.Intensional.Frame} [(p : F.Denot Core.Logic.Intensional.Ty.t) → Decidable p] (lex : Montague.Lexicon F) (g : Core.Assignment F.Entity) (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 F lex g t with | some { ty := Core.Logic.Intensional.Ty.t, val := b } => some (decide b) | x => none

def Semantics.Composition.Tree.evalTreeProp {C : Type} {F : Core.Logic.Intensional.Frame} [(p : F.Denot Core.Logic.Intensional.Ty.t) → Decidable p] (lex : Montague.Lexicon F) (g : Core.Assignment F.Entity) (t : Core.Tree.Tree C String) : Option (F.Index → 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 {F : Core.Logic.Intensional.Frame} (d : TypedDenot F) : interpNonBranching d = d

theorem Semantics.Composition.Tree.interpFA_type {F : Core.Logic.Intensional.Frame} {σ τ : Core.Logic.Intensional.Ty} (f : F.Denot (σ ⇒ τ)) (x : F.Denot σ) : interpFA f x = f x

theorem Semantics.Composition.Tree.tryPM_preserves_type {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) (h1 : d1.ty = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) (h2 : d2.ty = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)) : ∃ (d : TypedDenot F), tryPM d1 d2 = some d ∧ d.ty = (Core.Logic.Intensional.Ty.e ⇒ Core.Logic.Intensional.Ty.t)

theorem Semantics.Composition.Tree.interpBinary_eq {F : Core.Logic.Intensional.Frame} (d1 d2 : TypedDenot F) : interpBinary d1 d2 = (tryFA d1 d2 <|> tryIFA d1 d2 <|> tryPM d1 d2)