Type-driven interpretation

This file is the composition engine of Heim and Kratzer's type-driven interpretation, with the intensional application of von Fintel and Heim and the event identification of Kratzer (eventIdentification), parameterized over an effect functor M in the style of Bumford and Charlow. A node denotes an M-computation in the domain of its semantic type, a Denotation, and each composition principle lifts through the Applicative structure of M, so the pure Heim and Kratzer engine is the instance M = Id. A terminal node denotes what its leaf interpretation gives it, a string in a Lexicon or a fragment carrier through its readings; a non-branching node denotes what its daughter does; a binary node composes by functional application in either order, then intensional functional application, then predicate modification, then event identification, whichever the daughters' types admit first; a trace denotes its index's value under the assignment; and a binder abstracts over its index by Predicate Abstraction, which is a capability of the effect (PredAbs) rather than a given.

A tree is interpreted by evaluating its translation (Composition/Term.lean): the composition modes are the typed operations of Composition/Mode.lean, selected by the daughters' types alone, and interp is the evaluation of the term a tree translates to. Each equation of the engine is then a fact about that evaluation, and the pure engine is the denotation of the term (interp_eq_eval_translate).

Main declarations

• interp interprets a tree under an assignment, over any leaf type, as the evaluation of its translation; a binary node composes by Montague.Ty.mode? (interp_node_binary).
• tyBinary is the type a binary node composes to, a function of the daughters' types alone.
• ty? is the type a tree composes to, a function of the types of its leaves alone, and the type of its denotation (interp_map_fst).
• interp_congr_of_agree and its corollaries are Heim and Kratzer's theorems on variable binding: interpretability and the composed type never depend on the assignment (interp_map_fst_congr), and a tree's denotation depends on it only at the traces free in the tree.
• readings composes a lexicon of sets of readings, the values the engine computes over the tree's resolutions; the engine on an unambiguous lexicon is the special case (readings_eq_of_choice) and a binary node's readings compose pointwise (mem_readings_node_binary).
• interp_eq_eval_translate: the pure engine is the denotation of the tree's term.

Implementation notes

Binary nodes sequence effects in linear order, the left daughter's first whichever daughter is the function, so at M = Cont R surface scope is the default reading and inverse scope needs a reordered evaluation (Composition/Cont.lean). Predicate Abstraction needs a distributor (E → M (Ty.Domain ty)) → M (E → Ty.Domain ty), which scope effects lack, so under them .bind nodes fail and binding comes from the order of effects instead; making the distributor optional turns that rivalry into a fact instance resolution checks. The abstraction's fallback value valueAt is never reached, since types do not depend on the assignment. The category parameter of a tree is ignored, composition being type-driven.

References

• [HK98]
• [vFH11]
• [Kra96]
• [BC26f]

The pure engine computes in Id, whose applicative operations are application. The lemmas are simp lemmas in this namespace only, since they identify Id α with α.

theorem HeimKratzer.Tree.seq_eq_apply {α β : Type} (f : Id (α → β)) (x : Id α) : f <*> x = f x

theorem HeimKratzer.Tree.map_eq_apply {α β : Type} (f : α → β) (x : Id α) : f <$> x = f x

theorem HeimKratzer.Tree.pure_eq {α : Type} (a : α) : pure a = a

def HeimKratzer.Tree.valueAt {E W D : Type} {M : Type → Type} (τ : Montague.Ty) (v : M (Montague.Ty.Domain E W τ D)) : Option (Montague.Denotation E W M D) → M (Montague.Ty.Domain E W τ D)

The value of an interpreted daughter at the type τ, with the default v where the daughter is uninterpretable or of another type. Types do not depend on the assignment (interp_map_fst_congr), so under Predicate Abstraction the default is never reached (valueAt_of_map_fst).

Equations

• HeimKratzer.Tree.valueAt τ v (some ⟨ty, val⟩) = if h : ty = τ then h ▸ val else v
• HeimKratzer.Tree.valueAt τ v none = v

@[simp]

theorem HeimKratzer.Tree.valueAt_some {E W D : Type} {M : Type → Type} {τ : Montague.Ty} (v x : M (Montague.Ty.Domain E W τ D)) : valueAt τ v (some ⟨τ, x⟩) = x

theorem HeimKratzer.Tree.valueAt_of_map_fst {E W D : Type} {M : Type → Type} {τ : Montague.Ty} {v v' : M (Montague.Ty.Domain E W τ D)} {d : Option (Montague.Denotation E W M D)} (h : Option.map (fun (x : Montague.Denotation E W M D) => x.fst) d = some τ) : valueAt τ v d = valueAt τ v' d

Tree interpretation

@[reducible, inline]

abbrev HeimKratzer.Tree.evalAt {E W : Type} {M : Type → Type} [Applicative M] {D : Type} [PredAbs M E W D] (g : Assignment E) (d : (ty : Montague.Ty) × Term (fun (ty : Montague.Ty) => M (Montague.Ty.Domain E W ty D)) ty) : Option (Montague.Denotation E W M D)

The denotation of a term whose constants are denotations, at its type.

Equations

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

def HeimKratzer.Tree.interp {C E W : Type} {M : Type → Type} [Applicative M] {D : Type} [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (t : PhraseStructure.Tree C L) : Option (Montague.Denotation E W M D)

In the denotation of a tree under an assignment, by the composition principles of [HK98], a terminal denotes what its leaf interpretation gives it, a non-branching node what its daughter does, a binary node what the mode its daughters' types select composes, a trace the value of its index, and a binder the abstraction over its index, when the effect has a distributor. It is the denotation of the tree's term, each word's denotation its constant.

Equations

• HeimKratzer.Tree.interp lex g t = (HeimKratzer.Tree.translate lex t).bind (HeimKratzer.Tree.evalAt g)

Reduction lemmas

One @[simp] lemma per constructor, so that a derivation reduces by simp toward its composed denotation.

@[simp]

theorem HeimKratzer.Tree.interp_terminal {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (c : C) (w : L) : interp lex g (PhraseStructure.Tree.terminal c w) = lex w

@[simp]

theorem HeimKratzer.Tree.interp_node_unary {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (c : C) (t : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.node c [t]) = interp lex g t

@[simp]

theorem HeimKratzer.Tree.interp_adjoin_unary {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (c : C) (t : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.adjoin c [t]) = interp lex g t

@[simp]

theorem HeimKratzer.Tree.interp_node_binary {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.node c [t₁, t₂]) = (interp lex g t₁).bind fun (d₁ : Montague.Denotation E W M D) => (interp lex g t₂).bind fun (d₂ : Montague.Denotation E W M D) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalM) d₁ d₂

@[simp]

theorem HeimKratzer.Tree.interp_adjoin_binary {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.adjoin c [t₁, t₂]) = (interp lex g t₁).bind fun (d₁ : Montague.Denotation E W M D) => (interp lex g t₂).bind fun (d₂ : Montague.Denotation E W M D) => Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalM) d₁ d₂

@[simp]

theorem HeimKratzer.Tree.interp_trace {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (n : ℕ) (c : C) : interp lex g (PhraseStructure.Tree.trace n c) = some ⟨Montague.Ty.e, pure (g n)⟩

@[simp]

theorem HeimKratzer.Tree.interp_bind {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) (n : ℕ) (c : C) (body : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.bind n c body) = PredAbs.dist?.bind fun (dist : (ty : Montague.Ty) → (E → M (Montague.Ty.Domain E W ty D)) → M (E → Montague.Ty.Domain E W ty D)) => (interp lex g body).bind fun (d : Montague.Denotation E W M D) => some ⟨Montague.Ty.e ⇒ d.fst, dist d.fst fun (x : E) => valueAt d.fst d.snd (interp lex (Function.update g n x) body)⟩

theorem HeimKratzer.Tree.interp_junk {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g : Assignment E) {l : PhraseStructure.Tree.Label C L} {cs : List (PhraseStructure.Tree C L)} (h : ¬l.Licenses (List.map RoseTree.value cs)) : interp lex g (RoseTree.node l cs) = none

A node whose daughters its label does not license denotes nothing.

The type of a tree

The type a tree composes to is a function of the types of its leaves: ty? computes it by the recursion of interp, with tyBinary at the binary nodes, and interp_map_fst is the agreement. Interpretability is therefore decided by the types of the leaves alone.

def HeimKratzer.Tree.tyBinary (σ τ : Montague.Ty) : Option Montague.Ty

The type two daughters compose to, the mother's type under the mode their types select.

Equations

• HeimKratzer.Tree.tyBinary σ τ = Option.map (fun (x : (τ_1 : Montague.Ty) × HeimKratzer.Mode σ τ τ_1) => x.fst) (σ.mode? τ)

def HeimKratzer.Tree.ty? {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) : PhraseStructure.Tree C L → Option Montague.Ty

The type a tree composes to, from the types lexTy gives its leaves, with abs saying whether the effect supports Predicate Abstraction.

Equations

• One or more equations did not get rendered due to their size.
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.terminal a w) []) = lexTy w
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.node a) [t]) = HeimKratzer.Tree.ty? lexTy abs t
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.node a) children) = none
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.segment a) [t]) = HeimKratzer.Tree.ty? lexTy abs t
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.segment a) children) = none
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.trace a a_1) []) = some Montague.Ty.e
• HeimKratzer.Tree.ty? lexTy abs (RoseTree.node (PhraseStructure.Tree.Label.bind a a_1) [body]) = if abs = true then Option.map Montague.Ty.e.fn (HeimKratzer.Tree.ty? lexTy abs body) else none
• HeimKratzer.Tree.ty? lexTy abs x✝ = none

@[simp]

theorem HeimKratzer.Tree.ty?_terminal {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (c : C) (w : L) : ty? lexTy abs (PhraseStructure.Tree.terminal c w) = lexTy w

@[simp]

theorem HeimKratzer.Tree.ty?_node_unary {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (c : C) (t : PhraseStructure.Tree C L) : ty? lexTy abs (PhraseStructure.Tree.node c [t]) = ty? lexTy abs t

@[simp]

theorem HeimKratzer.Tree.ty?_node_binary {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : ty? lexTy abs (PhraseStructure.Tree.node c [t₁, t₂]) = (ty? lexTy abs t₁).bind fun (σ : Montague.Ty) => (ty? lexTy abs t₂).bind fun (τ : Montague.Ty) => tyBinary σ τ

@[simp]

theorem HeimKratzer.Tree.ty?_adjoin_unary {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (c : C) (t : PhraseStructure.Tree C L) : ty? lexTy abs (PhraseStructure.Tree.adjoin c [t]) = ty? lexTy abs t

@[simp]

theorem HeimKratzer.Tree.ty?_adjoin_binary {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (c : C) (t₁ t₂ : PhraseStructure.Tree C L) : ty? lexTy abs (PhraseStructure.Tree.adjoin c [t₁, t₂]) = (ty? lexTy abs t₁).bind fun (σ : Montague.Ty) => (ty? lexTy abs t₂).bind fun (τ : Montague.Ty) => tyBinary σ τ

@[simp]

theorem HeimKratzer.Tree.ty?_trace {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (n : ℕ) (c : C) : ty? lexTy abs (PhraseStructure.Tree.trace n c) = some Montague.Ty.e

@[simp]

theorem HeimKratzer.Tree.ty?_bind {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) (n : ℕ) (c : C) (body : PhraseStructure.Tree C L) : ty? lexTy abs (PhraseStructure.Tree.bind n c body) = if abs = true then Option.map Montague.Ty.e.fn (ty? lexTy abs body) else none

theorem HeimKratzer.Tree.ty?_junk {C : Type} {L : Type u_1} (lexTy : L → Option Montague.Ty) (abs : Bool) {l : PhraseStructure.Tree.Label C L} {cs : List (PhraseStructure.Tree C L)} (h : ¬l.Licenses (List.map RoseTree.value cs)) : ty? lexTy abs (RoseTree.node l cs) = none

A node whose daughters its label does not license has no type.

theorem HeimKratzer.Tree.interp_map_fst {C : Type} {L : Type u_1} {lexTy : L → Option Montague.Ty} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Option (Montague.Denotation E W M D)} (h : ∀ (w : L), Option.map (fun (x : Montague.Denotation E W M D) => x.fst) (lex w) = lexTy w) (g : Assignment E) (t : PhraseStructure.Tree C L) : Option.map (fun (x : Montague.Denotation E W M D) => x.fst) (interp lex g t) = ty? lexTy PredAbs.dist?.isSome t

The type of a tree's denotation is the type ty? computes from the types of its leaves.

theorem HeimKratzer.Tree.isSome_interp {C : Type} {L : Type u_1} {lexTy : L → Option Montague.Ty} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Option (Montague.Denotation E W M D)} (h : ∀ (w : L), Option.map (fun (x : Montague.Denotation E W M D) => x.fst) (lex w) = lexTy w) (g : Assignment E) (t : PhraseStructure.Tree C L) : (interp lex g t).isSome = (ty? lexTy PredAbs.dist?.isSome t).isSome

A tree is interpretable exactly when the types of its leaves give it a type.

Assignment dependence and free variables

[HK98]'s theorems on variable binding (§5.4.2): the denotation of a tree depends on the assignment only at the traces free in it. Interpretability and the type composed do not depend on the assignment at all (interp_map_fst_congr), so with total assignments their theorem (9), that a tree with no free occurrence of the index i denotes alike under an assignment and its modification at i, is interp_update_of_not_mem_freeIndices, and their (10), that a closed tree denotes alike under every assignment, is interp_congr_of_closed.

theorem HeimKratzer.Tree.interp_map_fst_congr {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) (g g' : Assignment E) (t : PhraseStructure.Tree C L) : Option.map (fun (x : Montague.Denotation E W M D) => x.fst) (interp lex g t) = Option.map (fun (x : Montague.Denotation E W M D) => x.fst) (interp lex g' t)

Whether a tree is interpretable, and at which type, does not depend on the assignment.

theorem HeimKratzer.Tree.interp_congr_of_agree {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) {g g' : Assignment E} {t : PhraseStructure.Tree C L} (h : ∀ i ∈ t.freeIndices, g i = g' i) : interp lex g t = interp lex g' t

Assignments agreeing on the traces free in a tree give it the same denotation, the coincidence theorem ([HK98] §5.4.2).

theorem HeimKratzer.Tree.interp_update_of_not_mem_freeIndices {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) {t : PhraseStructure.Tree C L} {i : ℕ} (h : i ∉ t.freeIndices) (g : Assignment E) (x : E) : interp lex (Function.update g i x) t = interp lex g t

By [HK98]'s (9), a tree with no free trace at index i denotes alike under an assignment and its modification at i.

theorem HeimKratzer.Tree.interp_congr_of_closed {C E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L : Type u_1} (lex : L → Option (Montague.Denotation E W M D)) {t : PhraseStructure.Tree C L} (h : t.Closed) (g g' : Assignment E) : interp lex g t = interp lex g' t

By [HK98]'s (10), a closed tree denotes alike under every assignment.

Readings of an ambiguous lexicon

A word may have several available readings. A resolution of a tree chooses one reading for each occurrence of a word, and the readings of the tree are the values the engine computes over its resolutions. The engine on a lexicon with one reading per word is the special case (readings_eq_of_choice), and a binary node's readings are the pointwise compositions of its daughters' (mem_readings_node_binary).

theorem HeimKratzer.Tree.interp_map {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {L' : Type u_2} (lex : L' → Option (Montague.Denotation E W M D)) (f : L → L') (g : Assignment E) (t : PhraseStructure.Tree C L) : interp lex g (PhraseStructure.Tree.map f t) = interp (lex ∘ f) g t

Interpretation commutes with relabelling the leaves.

def HeimKratzer.Tree.readings {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] (lex : L → Set (Montague.Denotation E W M D)) (g : Assignment E) (t : PhraseStructure.Tree C L) : Set (Montague.Denotation E W M D)

The readings of a tree under a leaf interpretation giving each word a set of readings, the values the engine computes over the resolutions of the tree, each occurrence of a word resolved to one of its readings.

Equations

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

theorem HeimKratzer.Tree.exists_resolution_of_interp {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {g : Assignment E} {choice : L → Option (Montague.Denotation E W M D)} {t : PhraseStructure.Tree C L} {d : Montague.Denotation E W M D} (h : interp choice g t = some d) : ∃ (r : PhraseStructure.Tree C { p : L × Montague.Denotation E W M D // choice p.1 = some p.2 }), PhraseStructure.Tree.map (fun (x : { p : L × Montague.Denotation E W M D // choice p.1 = some p.2 }) => (↑x).1) r = t ∧ interp (fun (p : { p : L × Montague.Denotation E W M D // choice p.1 = some p.2 }) => some (↑p).2) g r = some d

A value the engine computes under a choice of readings is the value of a resolved tree.

theorem HeimKratzer.Tree.interp_mem_readings {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Set (Montague.Denotation E W M D)} {g : Assignment E} {choice : L → Option (Montague.Denotation E W M D)} (hc : ∀ (w : L) (d : Montague.Denotation E W M D), choice w = some d → d ∈ lex w) {t : PhraseStructure.Tree C L} {d : Montague.Denotation E W M D} (h : interp choice g t = some d) : d ∈ readings lex g t

A value the engine computes under a choice among the readings is a reading.

theorem HeimKratzer.Tree.readings_eq_of_choice {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {g : Assignment E} (choice : L → Option (Montague.Denotation E W M D)) (t : PhraseStructure.Tree C L) : readings (fun (w : L) => {d : Montague.Denotation E W M D | choice w = some d}) g t = {d : Montague.Denotation E W M D | interp choice g t = some d}

On a lexicon with one reading per word, the readings are the engine's values.

@[simp]

theorem HeimKratzer.Tree.readings_terminal {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Set (Montague.Denotation E W M D)} {g : Assignment E} (c : C) (w : L) : readings lex g (PhraseStructure.Tree.terminal c w) = lex w

@[simp]

theorem HeimKratzer.Tree.readings_trace {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Set (Montague.Denotation E W M D)} {g : Assignment E} (n : ℕ) (c : C) : readings lex g (PhraseStructure.Tree.trace n c) = {⟨Montague.Ty.e, pure (g n)⟩}

theorem HeimKratzer.Tree.mem_readings_node_binary {C : Type} {L : Type u_1} {E W D : Type} {M : Type → Type} [Applicative M] [PredAbs M E W D] {lex : L → Set (Montague.Denotation E W M D)} {g : Assignment E} {c : C} {t₁ t₂ : PhraseStructure.Tree C L} {d : Montague.Denotation E W M D} : d ∈ readings lex g (PhraseStructure.Tree.node c [t₁, t₂]) ↔ ∃ d₁ ∈ readings lex g t₁, ∃ d₂ ∈ readings lex g t₂, Mode.combine? (fun {σ₁ σ₂ τ : Montague.Ty} => Mode.evalM) d₁ d₂ = some d

A binary node's readings are the pointwise compositions of its daughters'.

Interpretation is evaluation of the translation

theorem HeimKratzer.Tree.interp_eq_eval_translate {C : Type} {K : Montague.Ty → Type u_1} {L : Type u_2} {E W D : Type} (I : {ty : Montague.Ty} → K ty → Montague.Ty.Domain E W ty D) (lex : L → Option ((ty : Montague.Ty) × K ty)) (g : Assignment E) (t : PhraseStructure.Tree C L) : interp (fun (w : L) => Option.map (fun (c : (ty : Montague.Ty) × K ty) => ⟨c.fst, I c.snd⟩) (lex w)) g t = Option.map (fun (d : (ty : Montague.Ty) × Term K ty) => ⟨d.fst, Term.eval (fun {ty : Montague.Ty} => I) g d.snd⟩) (translate lex t)

Interpreting a tree whose words denote what an interpretation I of their constants gives is evaluating the tree's term under I.