Bridge: VarAssignment = Assignment

@cite{henkin-monk-tarski-1971} @cite{partee-1973} @cite{heim-kratzer-1998}

The generic VarAssignment D (from Core.Semantics.Intension) and the canonical Assignment E (from Core.Assignment) are the same type: both are ℕ → D. Their update operations are the same function.

This makes every instantiation of VarAssignment — entity assignments (@cite{heim-kratzer-1998}), temporal assignments (@cite{partee-1973}), situation assignments (@cite{percus-2000}) — an instance of the same cylindric set algebra defined in Core.CylindricAlgebra.

Instantiations

Framework	Domain D	Assignment type
Heim & Kratzer	Entity	Assignment Entity
Partee 1973	Time	TemporalAssignment Time
Percus 2000	Situation W Time	SituationAssignment W Time
CDRT (Muskens)	E	Register E
PLA (@cite{dekker-2012})	E	VarIdx → E

All share the same cylindric algebra axioms (C1–C7) and the same substitution theory (HMT §1.5).

theorem Core.CylindricAlgebra.varAssignment_eq_assignment {D : Type u_1} : VarAssignment.VarAssignment D = Assignment D

VarAssignment D IS Assignment D — both are ℕ → D.

theorem Core.CylindricAlgebra.updateVar_eq_update {D : Type u_1} (g : VarAssignment.VarAssignment D) (n : ℕ) (d : D) : VarAssignment.updateVar g n d = Assignment.update g n d

updateVar IS Assignment.update.

theorem Core.CylindricAlgebra.lookupVar_eq_apply {D : Type u_1} (n : ℕ) (g : VarAssignment.VarAssignment D) : VarAssignment.lookupVar n g = g n

lookupVar n g is just g n — register projection.

theorem Core.CylindricAlgebra.exists_updateVar_iff_cylindrify {D : Type u_1} (n : ℕ) (p : VarAssignment.VarAssignment D → Prop) (g : VarAssignment.VarAssignment D) : (∃ (d : D), p (VarAssignment.updateVar g n d)) ↔ cylindrify n p g

Existential quantification over a VarAssignment register = cylindrification on the underlying Assignment.

theorem Core.CylindricAlgebra.lookupVar_eq_iff_diagonal {D : Type u_1} (n m : ℕ) (g : VarAssignment.VarAssignment D) : VarAssignment.lookupVar n g = VarAssignment.lookupVar m g ↔ diagonal n m g

Register equality = diagonal element.

theorem Core.CylindricAlgebra.varLambdaAbs_integrand {D : Type u_1} {α : Type u_2} (n : ℕ) (body : VarAssignment.VarAssignment D → α) (g : VarAssignment.VarAssignment D) (d : D) : VarAssignment.varLambdaAbs n body g d = body (VarAssignment.updateVar g n d)

Lambda abstraction is the integrand of cylindrification: varLambdaAbs n body g d = body (g[n↦d]). Existential closure over d gives cylindrification cₙ(body).