Assignment-relative denotations

Denotations of expressions with free variables, relative to an assignment g : ℕ → E of entities to indices ([HK98]): a pronoun with index n denotes g n, a binder at n abstracts over the value of n by updating g, and composition threads the assignment through — the Reader applicative of [charlow-2018], whose laws hold definitionally. Situation pronouns are the same construction at an assignment of indices, and DenotGS carries both.

Main definitions

• DenotG E W ty: denotations relative to an entity assignment; constDenot, applyG, lambdaAbsG, interpPronoun, denotGJoin.
• DenotGS E W ty: denotations relative to an entity and a situation assignment; interpSitPronoun, DenotGS.const.

References

• I. Heim, A. Kratzer, Semantics in Generative Grammar (1998)
• [S. Charlow, A modular theory of pronouns and binding (2018)][charlow-2018]

@[reducible, inline]

abbrev Semantics.Composition.DenotG (E W : Type) (ty : Ty) : Type

A denotation relative to an entity assignment.

Equations

• Semantics.Composition.DenotG E W ty = (Assignment E → Semantics.Composition.Denot E W ty)

def Semantics.Composition.interpPronoun {E W : Type} (n : ℕ) : DenotG E W Ty.e

Pronoun/variable denotation: ⟦xₙ⟧^g = g(n).

Equations

• Semantics.Composition.interpPronoun n g = g n

def Semantics.Composition.constDenot {E W : Type} {ty : Ty} (d : Denot E W ty) : DenotG E W ty

Lift constant denotation to assignment-relative form.

Equations

• Semantics.Composition.constDenot d x✝ = d

def Semantics.Composition.applyG {E W : Type} {σ τ : Ty} (f : DenotG E W (σ ⇒ τ)) (x : DenotG E W σ) : DenotG E W τ

Function application with assignments.

Equations

• Semantics.Composition.applyG f x g = f g (x g)

def Semantics.Composition.lambdaAbsG {E W : Type} {τ : Ty} (n : ℕ) (body : DenotG E W τ) : DenotG E W (Ty.e ⇒ τ)

Lambda abstraction with variable binding.

Equations

• Semantics.Composition.lambdaAbsG n body g x = body (Function.update g n x)

theorem Semantics.Composition.lambdaAbsG_apply {E W : Type} {τ : Ty} (n : ℕ) (body : DenotG E W τ) (arg : E) (g : Assignment E) : lambdaAbsG n body g arg = body (Function.update g n arg)

Assignment-sensitive composition as an applicative functor

[charlow-2018] observes that constDenot (ρ) and applyG (⊛) form an applicative functor for the Reader type constructor G a := g → a ([mcbride-paterson-2008]). The four applicative functor laws hold definitionally.

theorem Semantics.Composition.constDenot_applyG {E W : Type} {σ τ : Ty} (f : Denot E W (σ ⇒ τ)) (x : Denot E W σ) : applyG (constDenot f) (constDenot x) = constDenot (f x)

Homomorphism: ρ f ⊛ ρ x = ρ (f x).

theorem Semantics.Composition.applyG_constDenot_id {E W : Type} {σ : Ty} (v : DenotG E W σ) : applyG (constDenot id) v = v

Identity: ρ id ⊛ v = v.

theorem Semantics.Composition.applyG_constDenot_interchange {E W : Type} {σ τ : Ty} (u : DenotG E W (σ ⇒ τ)) (y : Denot E W σ) : applyG u (constDenot y) = applyG (constDenot fun (f : Denot E W (σ ⇒ τ)) => f y) u

Interchange: u ⊛ ρ y = ρ (· y) ⊛ u.

theorem Semantics.Composition.applyG_composition {E W : Type} {σ τ υ : Ty} (u : DenotG E W (τ ⇒ υ)) (v : DenotG E W (σ ⇒ τ)) (w : DenotG E W σ) : applyG (applyG (applyG (constDenot fun (f : Denot E W (τ ⇒ υ)) (g : Denot E W (σ ⇒ τ)) (x : Denot E W σ) => f (g x)) u) v) w = applyG u (applyG v w)

Composition: ρ comp ⊛ u ⊛ v ⊛ w = u ⊛ (v ⊛ w).

Monadic join for higher-order variables

def Semantics.Composition.denotGJoin {E A : Type} (ho : Assignment E → Assignment E → A) : Assignment E → A

Join (μ): flatten a doubly assignment-dependent meaning.

[charlow-2018] §4.2: μ m := λg. m g g.

Enables higher-order variables: a pronoun anaphoric to an intension (type g → g → a) is flattened to a standard denotation (type g → a) by evaluating the retrieved intension at the current assignment.

Equations

• Semantics.Composition.denotGJoin ho g = ho g g

theorem Semantics.Composition.denotGJoin_const {E A : Type} (d : Assignment E → A) : (denotGJoin fun (x : Assignment E) => d) = d

Left identity: μ (ρ d) = d.

theorem Semantics.Composition.denotGJoin_inner_const {E A : Type} (d : Assignment E → A) : (denotGJoin fun (g x : Assignment E) => d g) = d

Right identity: μ (λg. ρ(d g)) = d.

theorem Semantics.Composition.denotGJoin_assoc {E A : Type} (hho : Assignment E → Assignment E → Assignment E → A) : denotGJoin (denotGJoin hho) = denotGJoin fun (g : Assignment E) => denotGJoin (hho g)

Associativity: μ ∘ μ = μ ∘ fmap μ.

Situation pronouns as the type-level dual of entity pronouns

Hanink (2018, 2021), Bondarenko (2022, 2023) and the broader post-Schwarz literature on situational vs anaphoric definites argue that a situation argument can be a bound variable (a "situation pronoun"), not just a free parameter handed to an interpretation function.

Type-theoretically this is the dual of entity binding under Ty.intens: where entity pronouns are interpreted relative to Assignment E := ℕ → E, situation pronouns are interpreted relative to SitAssignment W := ℕ → W. Both reuse Assignment at different instantiations, so mathlib's Function.update lemmas apply to both.

@[reducible, inline]

abbrev Semantics.Composition.SitAssignment (W : Type) : Type

Situation assignment: maps situation-pronoun indices to frame indices. Reuses Assignment at type W.

Equations

• Semantics.Composition.SitAssignment W = Assignment W

def Semantics.Composition.interpSitPronoun {W : Type} (n : ℕ) : SitAssignment W → W

Situation-pronoun denotation: ⟦sₙ⟧^{gs} = gs(n). Parallels interpPronoun.

Equations

• Semantics.Composition.interpSitPronoun n gs = gs n

@[reducible, inline]

abbrev Semantics.Composition.DenotGS (E W : Type) (ty : Ty) : Type

A denotation relative to an entity assignment and a situation assignment, for expressions containing both entity and situation pronouns (definites, attitude reports, world-variable binding).

Equations

• Semantics.Composition.DenotGS E W ty = (Assignment E → Semantics.Composition.SitAssignment W → Semantics.Composition.Denot E W ty)

def Semantics.Composition.DenotGS.const {E W : Type} {ty : Ty} (d : Denot E W ty) : DenotGS E W ty

A constant denotation as a bi-assignment-relative one.

Equations

• Semantics.Composition.DenotGS.const d x✝¹ x✝ = d