Variable Binding and Assignment Functions

[HK98] [Cha18]

Framework-neutral infrastructure for interpreting expressions with free variables, built on Intensional.Denot.

Main definitions

• Assignment (from Core/Logic/Assignment.lean) instantiated at E for entity pronouns and W for situation pronouns; the g[n ↦ x] notation for Function.update is declared here
• DenotG — assignment-relative denotations
• applyG, lambdaAbsG, constDenot — composition with assignments
• Applicative functor laws ([Cha18])
• Cylindric algebra bridge ([HMT71])

def Intensional.Variables.«term_[_↦_]» : Lean.TrailingParserDescr

Heim-Kratzer assignment-modification notation: g[n ↦ x] is Function.update g n x. The Function.update_* lemmas (update_self, update_of_ne, update_idem, update_comm, update_eq_self) are the update laws.

Equations

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

def Intensional.Variables.DenotG (E W : Type) (ty : Ty) : Type

Denotation depending on assignment function.

Equations

• Intensional.Variables.DenotG E W ty = (Core.Assignment E → Intensional.Denot E W ty)

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

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

Equations

• Intensional.Variables.interpPronoun n g = g n

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

Lift constant denotation to assignment-relative form.

Equations

• Intensional.Variables.constDenot d x✝ = d

theorem Intensional.Variables.constDenot_independent {E W : Type} {ty : Ty} (d : Denot E W ty) (g₁ g₂ : Core.Assignment E) : constDenot d g₁ = constDenot d g₂

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

Function application with assignments.

Equations

• Intensional.Variables.applyG f x g = f g (x g)

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

Lambda abstraction with variable binding.

Equations

• Intensional.Variables.lambdaAbsG n body g x = body (Function.update g n x)

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

theorem Intensional.Variables.lambdaAbsG_alpha {E W : Type} {τ : Ty} (n₁ n₂ : ℕ) (body : DenotG E W τ) (g : Core.Assignment E) (h_fresh : ∀ (g' : Core.Assignment E) (x : E), body (Function.update g' n₁ x) = body (Function.update g' n₂ x)) : lambdaAbsG n₁ body g = lambdaAbsG n₂ body g

Assignment-sensitive composition as an applicative functor

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

theorem Intensional.Variables.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 Intensional.Variables.applyG_constDenot_id {E W : Type} {σ : Ty} (v : DenotG E W σ) : applyG (constDenot id) v = v

Identity: ρ id ⊛ v = v.

theorem Intensional.Variables.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 Intensional.Variables.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).

def Intensional.Variables.denotGJoin {E A : Type} (ho : Core.Assignment E → Core.Assignment E → A) : Core.Assignment E → A

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

[Cha18] §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

• Intensional.Variables.denotGJoin ho g = ho g g

theorem Intensional.Variables.denotGJoin_const {E A : Type} (d : Core.Assignment E → A) : (denotGJoin fun (x : Core.Assignment E) => d) = d

Left identity: μ (ρ d) = d.

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

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

theorem Intensional.Variables.denotGJoin_assoc {E A : Type} (hho : Core.Assignment E → Core.Assignment E → Core.Assignment E → A) : denotGJoin (denotGJoin hho) = denotGJoin fun (g : Core.Assignment E) => denotGJoin (hho g)

Associativity: μ ∘ μ = μ ∘ fmap μ.

Assignments as a cylindric set algebra

[HK98] assignment functions satisfy the same algebraic axioms as DRT's dynamic assignments: predicates on assignments form a cylindric set algebra ([HMT71]).

def Intensional.Variables.existsClosure {E : Type} (n : ℕ) (φ : Core.Assignment E → Prop) : Core.Assignment E → Prop

Existential closure at variable n: (∃n.φ)(g) = ∃x. φ(g[n↦x]).

Equations

• Intensional.Variables.existsClosure n φ g = ∃ (x : E), φ (Function.update g n x)

def Intensional.Variables.diag {E : Type} (n k : ℕ) : Core.Assignment E → Prop

Diagonal element: assignments where variables n and k agree.

Equations

• Intensional.Variables.diag n k g = (g n = g k)

theorem Intensional.Variables.existsClosure_bot {E : Type} (n : ℕ) : (existsClosure n fun (x : Core.Assignment E) => False) = fun (x : Core.Assignment E) => False

C₁: Existential closure of False is False.

theorem Intensional.Variables.le_existsClosure {E : Type} (n : ℕ) (φ : Core.Assignment E → Prop) (g : Core.Assignment E) : φ g → existsClosure n φ g

C₂: φ implies its existential closure.

theorem Intensional.Variables.diag_refl {E : Type} (n : ℕ) : diag n n = fun (x : Core.Assignment E) => True

C₅: Dnn = ⊤ (reflexivity of equality).

def Intensional.Variables.resolve {E : Type} (κ l : ℕ) (φ : Core.Assignment E → Prop) : Core.Assignment E → Prop

Pronoun resolution: setting variable κ to read from variable l.

Equations

• Intensional.Variables.resolve κ l φ g = φ (Function.update g κ (g l))

theorem Intensional.Variables.resolve_eq_existsClosure_diag {E : Type} (κ l : ℕ) (φ : Core.Assignment E → Prop) (h : κ ≠ l) (g : Core.Assignment E) : resolve κ l φ g ↔ existsClosure κ (fun (g' : Core.Assignment E) => diag κ l g' ∧ φ g') g

Substitution = resolution.

theorem Intensional.Variables.existsClosure_eq_exists_lambda {E W : Type} (n : ℕ) (body : DenotG E W Ty.t) (g : Core.Assignment E) : existsClosure n (fun (g' : Core.Assignment E) => body g') g ↔ ∃ (x : E), lambdaAbsG n body g x

Lambda abstraction at n is the "integrand" of existential closure.

theorem Intensional.Variables.existsClosure_eq_cylindrify {E : Type} (n : ℕ) (φ : Core.Assignment E → Prop) : existsClosure n φ = Core.CylindricAlgebra.cylindrify n φ

theorem Intensional.Variables.diag_eq_diagonal {E : Type} (n k : ℕ) : diag n k = Core.CylindricAlgebra.diagonal n k

theorem Intensional.Variables.resolve_eq_directSubst {E : Type} (κ l : ℕ) (φ : Core.Assignment E → Prop) : resolve κ l φ = Core.CylindricAlgebra.directSubst κ l φ

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 Core.Assignment at different instantiations, so mathlib's Function.update lemmas apply to both.

@[reducible, inline]

abbrev Intensional.Variables.SitAssignment (W : Type) : Type

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

Equations

• Intensional.Variables.SitAssignment W = Core.Assignment W

def Intensional.Variables.interpSitPronoun {W : Type} (n : ℕ) : SitAssignment W → W

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

Equations

• Intensional.Variables.interpSitPronoun n gs = gs n

def Intensional.Variables.DenotGS (E W : Type) (ty : Ty) : Type

Bi-assignment-relative denotation: depends on both an entity assignment and a situation assignment. Used by any module that interprets expressions containing both entity pronouns and situation pronouns (definites, attitude reports, modal scope, world-variable binding).

Equations

• Intensional.Variables.DenotGS E W ty = (Core.Assignment E → Intensional.Variables.SitAssignment W → Intensional.Denot E W ty)

def Intensional.Variables.DenotGS.ofDenotG {E W : Type} {ty : Ty} (d : DenotG E W ty) : DenotGS E W ty

Lift a pure entity-assignment-relative denotation to bi-assignment form (ignores the situation assignment).

Equations

• Intensional.Variables.DenotGS.ofDenotG d g x✝ = d g

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

Lift a constant denotation to bi-assignment form (ignores both assignments).

Equations

• Intensional.Variables.DenotGS.const d x✝¹ x✝ = d

theorem Intensional.Variables.DenotGS.ofDenotG_const {E W : Type} {ty : Ty} (d : Denot E W ty) : ofDenotG (constDenot d) = const d

Bi-assignment lift of a pure constant is the same as DenotG-lift of a constant — the two const paths agree.