Type-Driven Interpretation

[HK98]'s type-driven interpretation (Ch. 3-5; [vFH11], Ch. 1), parameterized over an effect functor M in the style of [BC24b]: a node's denotation is an M-computation M (Denot E W ty) (TypedDenot), and each composition principle lifts through M's Applicative structure. The pure Heim & Kratzer engine is the M = Id instance (TypedDenot, interp at a pure Lexicon) — true by construction, not by a bridge theorem.

Composition principles:

1. Terminal Nodes (TN): lexical lookup
2. Non-Branching Nodes (NN): identity
3. Functional Application (FA): ⟦α⟧ = ⟦β⟧(⟦γ⟧) when types match
4. Intensional Functional Application (IFA): ⟦α⟧ = ⟦β⟧(^⟦γ⟧) when β expects an intension ⟨s,σ⟩ and γ has type σ ([vFH11] Step 10)
5. Predicate Modification (PM): combine two ⟨e,t⟩ predicates (Ch. 4)
6. Predicate Abstraction (PA): ⟦[n β]⟧^g = λx. ⟦β⟧^{g[n↦x]} (Ch. 5)

Two effect-discipline choices, both visible rather than stipulated:

• Binary nodes sequence effects in linear order — the left daughter's effects fire first whichever daughter is the function. At M = Cont R this makes surface scope the default reading; inverse scope requires reordering the evaluation (QR, or bind-order permutation — see Composition/Continuation.lean and Studies/BumfordCharlow2024.lean).
• PA is a capability, not a given (PredAbs): it needs an entity-distributor (E → M (Denot ty)) → M (E → Denot ty), which Id has and scope-type effects lack. See the PredAbs docstring.

Composition primitives

structure Semantics.Composition.Tree.TypedDenot (E W : Type) (M : Type → Type := Id) : Type

A typed denotation: a linguistic type together with an M-computation over its denotation domain. The default M := Id recovers the [HK98] carrier; effectful values supply M explicitly.

• ty : Intensional.Ty
• val : M (Intensional.Denot E W self.ty)

class Semantics.Composition.Tree.PredAbs (M : Type → Type) (E W : Type) : Type

Capability for Predicate Abstraction under effect M: an entity-distributor commuting M over entity-indexed families.

dist? = none records that an effect does not support PA. Id (and any Reader-like effect) has a distributor; scope-type effects (Cont R) do not — abstraction would have to run one continuation at every entity simultaneously — so binding under such effects arises from bind-order or the W ⊣ R adjunction instead (Studies/BumfordCharlow2024.lean). Making the distributor optional turns the QR/PA-vs-effect-sequencing rivalry into a fact checked by instance resolution.

• dist? : Option ((ty : Intensional.Ty) → (E → M (Intensional.Denot E W ty)) → M (E → Intensional.Denot E W ty))

@[implicit_reducible]

instance Semantics.Composition.Tree.instPredAbsId (E W : Type) : PredAbs Id E W

Equations

• Semantics.Composition.Tree.instPredAbsId E W = { dist? := some fun (x : Intensional.Ty) (f : E → Id (Intensional.Denot E W x)) => f }

def Semantics.Composition.Tree.canApply (funTy argTy : Intensional.Ty) : Option 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 (E W : Type) {M : Type → Type} (lex : Montague.Lexicon E W M) (word : String) : Option (TypedDenot E W M)

TN: lexical lookup.

Equations

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

def Semantics.Composition.Tree.interpNonBranching {E W : Type} {M : Type → Type} (daughter : TypedDenot E W M) : TypedDenot E W M

NN: identity.

Equations

• Semantics.Composition.Tree.interpNonBranching daughter = daughter

def Semantics.Composition.Tree.interpFA {E W : Type} {σ τ : Intensional.Ty} (f : Intensional.Denot E W (σ ⇒ τ)) (x : Intensional.Denot E W σ) : Intensional.Denot E W τ

FA: ⟦β⟧(⟦γ⟧)

Equations

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

def Semantics.Composition.Tree.applyForward {E W : Type} {M : Type → Type} [Applicative M] (df da : TypedDenot E W M) : Option (TypedDenot E W M)

Forward FA: the function is the left daughter df, the argument da.

Equations

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

def Semantics.Composition.Tree.applyBackward {E W : Type} {M : Type → Type} [Applicative M] (da df : TypedDenot E W M) : Option (TypedDenot E W M)

Backward FA: the function is the right daughter df, the argument da. The left daughter da sequences first, hence the (λ x g => g x) combinator.

Equations

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

def Semantics.Composition.Tree.tryFA {E W : Type} {M : Type → Type} [Applicative M] (d1 d2 : TypedDenot E W M) : Option (TypedDenot E W M)

Try FA in both orders, sequencing effects in linear order (the left daughter's effects fire first regardless of which daughter is the function): function on the left (applyForward), else on the right (applyBackward).

Equations

• Semantics.Composition.Tree.tryFA d1 d2 = (Semantics.Composition.Tree.applyForward d1 d2 <|> Semantics.Composition.Tree.applyBackward d1 d2)

def Semantics.Composition.Tree.tryIFA {E W : Type} {M : Type → Type} [Applicative M] (d1 d2 : TypedDenot E W M) : Option (TypedDenot E W M)

IFA: Intensional Functional Application ([vFH11] 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 (γ,β); effects sequence in linear order.

Equations

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

def Semantics.Composition.Tree.tryPM {E W : Type} {M : Type → Type} [Applicative M] (d1 d2 : TypedDenot E W M) : Option (TypedDenot E W 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 {E W : Type} {M : Type → Type} [Applicative M] (d1 d2 : TypedDenot E W M) : Option (TypedDenot E W M)

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)

Tree interpretation

def Semantics.Composition.Tree.interp {C : Type} (E W : Type) {M : Type → Type} [Applicative M] [PredAbs M E W] (lex : Montague.Lexicon E W M) (g : Core.Assignment E) : Syntax.Tree C String → Option (TypedDenot E W M)

Interpret a tree under an assignment.

Implements [HK98] Ch. 3-5 type-driven interpretation, lifted through the effect functor M:

• TN: terminal → lexical lookup
• NN: unary node → identity
• FA/IFA/PM: binary node → try FA, then IFA, then PM
• Traces/Pronouns: ⟦tₙ⟧^g = pure (g n)
• Predicate Abstraction (PA): ⟦[n β]⟧^g = λx. ⟦β⟧^{g[n↦x]}, available only when M has an entity-distributor (PredAbs)

PA is the key to quantifier scope under M = Id: 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. Under scope-type effects there is no distributor (PredAbs.dist? = none), and .bind nodes fail — in-situ effect sequencing replaces QR.

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

def Semantics.Composition.Tree.evalTree {C E W : Type} [(p : Intensional.Denot E W Intensional.Ty.t) → Decidable p] (lex : Montague.Lexicon E W) (g : Core.Assignment E) (t : Syntax.Tree C String) : Option Bool

Extract truth value from (pure) tree interpretation. Effectful roots discharge through per-effect handlers instead (handleScope and kin in Studies/BumfordCharlow2024.lean).

Equations

• Semantics.Composition.Tree.evalTree lex g t = match Semantics.Composition.Tree.interp E W lex g t with | some { ty := Intensional.Ty.t, val := b } => some (decide b) | x => none

def Semantics.Composition.Tree.evalTreeProp {C E W : Type} [(p : Intensional.Denot E W Intensional.Ty.t) → Decidable p] (lex : Montague.Lexicon E W) (g : Core.Assignment E) (t : Syntax.Tree C String) : Option (W → Bool)

Extract proposition (s→t) from (pure) 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 : Type → Type} {E W : Type} (d : TypedDenot E W M) : interpNonBranching d = d

theorem Semantics.Composition.Tree.interpFA_type {E W : Type} {σ τ : Intensional.Ty} (f : Intensional.Denot E W (σ ⇒ τ)) (x : Intensional.Denot E W σ) : interpFA f x = f x

theorem Semantics.Composition.Tree.tryPM_preserves_type {M : Type → Type} {E W : Type} [Applicative M] (d1 d2 : TypedDenot E W M) (h1 : d1.ty = (Intensional.Ty.e ⇒ Intensional.Ty.t)) (h2 : d2.ty = (Intensional.Ty.e ⇒ Intensional.Ty.t)) : ∃ (d : TypedDenot E W M), tryPM d1 d2 = some d ∧ d.ty = (Intensional.Ty.e ⇒ Intensional.Ty.t)

theorem Semantics.Composition.Tree.interpBinary_eq {M : Type → Type} {E W : Type} [Applicative M] (d1 d2 : TypedDenot E W M) : interpBinary d1 d2 = (tryFA d1 d2 <|> tryIFA d1 d2 <|> tryPM d1 d2)

Reduction lemmas (the interp simp normal form)

Per-constructor @[simp] lemmas so a derivation reduces by simp toward its composed denotation, instead of relying on opaque rfl over the whole engine call. Mode reduction (tryFA/interpBinary over concrete types) is the complementary layer, and is type-shape-specific because the modes case on Ty.

@[simp]

theorem Semantics.Composition.Tree.interp_terminal {C E W : Type} {M : Type → Type} [Applicative M] [PredAbs M E W] (lex : Montague.Lexicon E W M) (g : Core.Assignment E) (c : C) (w : String) : interp E W lex g (Syntax.Tree.terminal c w) = interpTerminal E W lex w

@[simp]

theorem Semantics.Composition.Tree.interp_node_binary {C E W : Type} {M : Type → Type} [Applicative M] [PredAbs M E W] (lex : Montague.Lexicon E W M) (g : Core.Assignment E) (c : C) (t₁ t₂ : Syntax.Tree C String) : interp E W lex g (Syntax.Tree.node c [t₁, t₂]) = (interp E W lex g t₁).bind fun (d₁ : TypedDenot E W M) => (interp E W lex g t₂).bind fun (d₂ : TypedDenot E W M) => interpBinary d₁ d₂

@[simp]

theorem Semantics.Composition.Tree.interpTerminal_lookup {E W : Type} {M : Type → Type} (lex : Montague.Lexicon E W M) (w : String) : interpTerminal E W lex w = Option.map (fun (e : Montague.LexEntry E W M) => { ty := e.ty, val := e.denot }) (lex w)

@[simp]

theorem Semantics.Composition.Tree.applyForward_fn {E W : Type} {M : Type → Type} [Applicative M] {σ τ : Intensional.Ty} (f : M (Intensional.Denot E W (σ ⇒ τ))) (x : M (Intensional.Denot E W σ)) : applyForward { ty := σ ⇒ τ, val := f } { ty := σ, val := x } = some { ty := τ, val := f <*> x }

Forward FA reduces generally (abstract σ τ). Backward FA stays type-shape-specific, since forward fires first when the left daughter is itself a function.

@[simp]

theorem Semantics.Composition.Tree.tryFA_forward {E W : Type} {M : Type → Type} [Applicative M] {σ τ : Intensional.Ty} (f : M (Intensional.Denot E W (σ ⇒ τ))) (x : M (Intensional.Denot E W σ)) : tryFA { ty := σ ⇒ τ, val := f } { ty := σ, val := x } = some { ty := τ, val := f <*> x }