Variable Assignments

Framework-neutral variable assignment infrastructure shared by static semantics (Montague/Heim & Kratzer), dynamic semantics (DRT, DPL, CDRT), and the cylindric algebra formalism.

An Assignment E maps natural number indices to entities of type E. The update operation g[n↦d] modifies a single register, leaving all others fixed. These operations satisfy the cylindric set algebra axioms (@cite{henkin-monk-tarski-1971}).

@[reducible, inline]

abbrev Core.Assignment (E : Type u) : Type u

Variable assignment: function from indices to entities.

This is the canonical assignment type used across the library:

• Montague semantics (static variable binding)
• DRT, DPL, CDRT (dynamic discourse referents)
• Cylindric algebra (abstract coordinate functions)

Equations

• Core.Assignment E = (Nat → E)

def Core.Assignment.update {E : Type u} (g : Assignment E) (n : Nat) (d : E) : Assignment E

Assignment update g[n↦d]: set register n to value d, preserving all other registers.

Equations

• g.update n d m = if m = n then d else g m

@[simp]

theorem Core.Assignment.update_at {E : Type u} (g : Assignment E) (n : Nat) (d : E) : g.update n d n = d

@[simp]

theorem Core.Assignment.update_ne {E : Type u} (g : Assignment E) {n m : Nat} (d : E) (h : m ≠ n) : g.update n d m = g m

theorem Core.Assignment.update_overwrite {E : Type u} (g : Assignment E) (n : Nat) (x y : E) : (g.update n x).update n y = g.update n y

theorem Core.Assignment.update_comm {E : Type u} (g : Assignment E) {n m : Nat} (x y : E) (h : n ≠ m) : (g.update n x).update m y = (g.update m y).update n x

theorem Core.Assignment.update_self {E : Type u} (g : Assignment E) (n : Nat) : g.update n (g n) = g

@[reducible, inline]

abbrev Core.PartialAssign (D : Type u) : Type u

Partial assignment: variables may be undefined (none).

Used in trivalent semantics (@cite{spector-2025}, @cite{beaver-krahmer-2001}) where g(x) = none means variable x is not valued, yielding undefinedness (#) in predicate application.

Equations

• Core.PartialAssign D = (Nat → Option D)

def Core.PartialAssign.empty {D : Type u} : PartialAssign D

A partial assignment that values no variables.

Equations

• Core.PartialAssign.empty x✝ = none

def Core.PartialAssign.update {D : Type u} (g : PartialAssign D) (n : Nat) (d : D) : PartialAssign D

Update a partial assignment at index n.

Equations

• g.update n d m = if m = n then some d else g m

def Core.PartialAssign.valued {D : Type u} (g : PartialAssign D) (n : Nat) : Bool

Whether variable n is valued by g.

Equations

• g.valued n = (g n).isSome

def Core.PartialAssign.isValued {D : Type u} (g : PartialAssign D) (n : Nat) : Bool

The U(x) / isValued predicate: x is valued. @cite{spector-2025} §2.2.2: always bivalent (never undefined).

Equations

• g.isValued n = g.valued n

@[simp]

theorem Core.PartialAssign.valued_update_at {D : Type u} (g : PartialAssign D) (n : Nat) (d : D) : (g.update n d).valued n = true

@[simp]

theorem Core.PartialAssign.valued_update_ne {D : Type u} (g : PartialAssign D) {n m : Nat} (d : D) (h : m ≠ n) : (g.update n d).valued m = g.valued m

theorem Core.PartialAssign.valued_empty {D : Type u} (n : Nat) : empty.valued n = false

def Core.PartialAssign.ofTotal {D : Type u} (g : Assignment D) : PartialAssign D

Coerce a total assignment to a partial assignment (always valued).

Equations

• Core.PartialAssign.ofTotal g n = some (g n)

theorem Core.PartialAssign.valued_ofTotal {D : Type u} (g : Assignment D) (n : Nat) : (ofTotal g).valued n = true

structure Core.PluralAssign (D : Type u) : Type u

Plural assignment: a set of atomic (partial) assignments.

@cite{spector-2025} §6.2: "contexts are viewed as pairs (w, G), where G is a set of assignments, a plural assignment." Plural assignments track inter-variable dependencies (e.g., which book each student read) that individual assignments cannot express.

Originates in plural dynamic semantics (@cite{van-der-berg-1996}, @cite{nouwen-2003}, @cite{brasoveanu-2008}). Spector's innovation is using them in a static (non-dynamic) setting.

Uses a structure wrapper to prevent Lean from currying (Nat → Option D) → Prop into Nat → Option D → Prop.

• pred : PartialAssign D → Prop

  The membership predicate on atomic assignments.

theorem Core.PluralAssign.ext_iff {D : Type u} {x y : PluralAssign D} : x = y ↔ x.pred = y.pred

theorem Core.PluralAssign.ext {D : Type u} {x y : PluralAssign D} (pred : x.pred = y.pred) : x = y

instance Core.PluralAssign.instMembershipPartialAssign {D : Type u} : Membership (PartialAssign D) (PluralAssign D)

Equations

• Core.PluralAssign.instMembershipPartialAssign = { mem := fun (G : Core.PluralAssign D) (g : Core.PartialAssign D) => G.pred g }

def Core.PluralAssign.Nonempty {D : Type u} (G : PluralAssign D) : Prop

Whether G contains at least one atomic assignment.

Equations

• G.Nonempty = ∃ (g : Core.PartialAssign D), g ∈ G

def Core.PluralAssign.restrict {D : Type u} (G : PluralAssign D) (x : Nat) (a : D) : PluralAssign D

Restrict a plural assignment to atomic assignments mapping x to a. @cite{spector-2025} §6.2: G_{x=a} is the subset of G where g(x) = a.

Equations

• G.restrict x a = { pred := fun (g : Core.PartialAssign D) => g ∈ G ∧ g x = some a }

def Core.PluralAssign.defined {D : Type u} (G : PluralAssign D) (x : Nat) : Prop

Whether any atomic assignment in G is defined for x.

Equations

• G.defined x = ∃ (g : Core.PartialAssign D), g ∈ G ∧ (g x).isSome = true

def Core.PluralAssign.singular {D : Type u} (G : PluralAssign D) (x : Nat) : Prop

Whether x is singular in G: there is exactly one value assigned to x across all atomic assignments in G. @cite{spector-2025} §6.2: |G(x)| = 1 — the variable denotes an atomic individual. Requires both:

• existence: at least one g ∈ G defines x
• agreement: all g ∈ G that define x agree on the value

Equations

• G.singular x = ∃ (d : D), (∃ (g : Core.PartialAssign D), g ∈ G ∧ g x = some d) ∧ ∀ (g : Core.PartialAssign D), g ∈ G → (g x).isSome = true → g x = some d

def Core.PluralAssign.isAtomic {D : Type u} (G : PluralAssign D) (x : Nat) : Prop

The atomic(x) predicate for plural assignments (propositional). @cite{spector-2025} §6.3: ⟦atomic(x)⟧^{w,G} = 1 if |G(x)| = 1, 0 if |G(x)| ≠ 1. Replaces U(x) from the simplified system. Equivalent to singular: all assignments in G that define x map it to the same value.

Equations

• G.isAtomic x = G.singular x

def Core.PluralAssign.null {D : Type u} : PluralAssign D

The null plural assignment: all possible partial assignments. @cite{spector-2025} §6: the starting context contains all pairs.

Equations

• Core.PluralAssign.null = { pred := fun (x : Core.PartialAssign D) => True }

def Core.PluralAssign.ofPred {D : Type u} (p : PartialAssign D → Prop) : PluralAssign D

Build a plural assignment from a predicate.

Equations

• Core.PluralAssign.ofPred p = { pred := p }

def Core.PluralAssign.singularAt {D : Type u} (G : PluralAssign D) (x : Nat) (d : D) : Prop

Witness-level singularity: G assigns x uniquely to d. @cite{spector-2025} §6.2: at least one atomic assignment maps x to d, and all assignments in G that define x agree on d.

Equations

• G.singularAt x d = ((∃ (g : Core.PartialAssign D), g ∈ G ∧ g x = some d) ∧ ∀ (g : Core.PartialAssign D), g ∈ G → (g x).isSome = true → g x = some d)

theorem Core.PluralAssign.singular_iff_exists_singularAt {D : Type u} (G : PluralAssign D) (x : Nat) : G.singular x ↔ ∃ (d : D), G.singularAt x d

singular is the existential closure of singularAt.