Variable Assignments

[HK98] [HMT71] [Spe25] [BK01]

Tarski-style total assignments and their partial extension. The polymorphic substrate shared by extensional Heim-Kratzer composition, DPL-style register state, CDRT, Charlow continuations, and trivalent partial-valuation systems.

Assignment E := ℕ → E is pre-intensional — pure Tarski variable mapping — so it lives in Core/Logic/ rather than inside Semantics/Intensional/. The intensional substrate (Denot E W, situation assignments Assignment W, DenotGS) builds on this in Semantics/Intensional/.

Pointwise update of a total assignment is mathlib's Function.update (no parallel API here): Function.update_self, Function.update_of_ne, Function.update_idem, Function.update_comm, and Function.update_eq_self are the update laws. The Heim-Kratzer notation g[n ↦ x] is declared in Semantics/Intensional/Variables.lean.

When to use Assignment E vs raw Nat → E

A struct field, function parameter, or local definition should use Assignment E (or PartialAssign E) precisely when its semantic role is Tarski-style variable assignment / register state / discourse-referent embedding — the same role that gets updated by quantifier binders and looked-up by free variables.

It should not be Assignment E when the structural shape Nat → E happens for an unrelated reason — e.g., model-theoretic name interpretation functions (Name_M in Kamp & Reyle), arity-indexed interpretation tables, lookup arrays, or any Nat → α that doesn't participate in variable-binding semantics. Renaming those would conflate distinct primitives.

Out of scope

• Discourse referents as named atomic symbols (Kamp & Reyle 1993 DRT proper). The ℕ-indexed register encoding is the DPL/CDRT reading; faithful K&R embeddings would need an opaque DRef type.
• File cards (Heim 1982 FCS). Heim's files carry an explicit domain Dom(F) ⊆ ℕ — PartialAssign covers the valuation side, but the domain-as-type-level commitment of FCS lives in the FCS study file.
• Proof-relevant context (Bekki DTS, Asher TYS) — not a Nat → α.
• Continuation state (Heim file cards, sequence-of-binders update semantics) — handled in the FCS / DPL study files. Continuation environments (Barker, Shan, Charlow paycheck composition) DO use Assignment as the Reader environment; that case is in scope.

@[reducible, inline]

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

Variable assignment: a function from natural-number indices to values in E. Instantiated at the entity type for entity pronouns (Heim & Kratzer 1998), at the index type for situation pronouns (Hanink 2021 / Bondarenko 2023), at Time for temporal variables, and at any other carrier whenever a framework needs Tarski-style variable interpretation.

Pointwise update g[n↦d] is Function.update g n d; mathlib's Function.update_* lemmas apply directly.

Equations

• Core.Assignment E = (ℕ → E)

@[reducible, inline]

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

Partial assignment: variables may be undefined (none).

Used in trivalent semantics ([Spe25], [BK01]) where g(x) = none means variable x is not valued. The trivalent application rule that turns this into the third value # lives with the predicate machinery in Semantics/Presupposition/, not here.

Equations

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

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

A partial assignment that values no variables.

Equations

• Core.PartialAssign.empty x✝ = none

def Core.PartialAssign.update {D : Type u_1} (g : PartialAssign D) (n : ℕ) (d : D) : PartialAssign D

Update a partial assignment at index n: Function.update with the value wrapped in some.

Equations

• g.update n d = Function.update g n (some d)

def Core.PartialAssign.valued {D : Type u_1} (g : PartialAssign D) (n : ℕ) : Bool

Whether variable n is valued by g.

Equations

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

@[simp]

theorem Core.PartialAssign.update_at {D : Type u_1} (g : PartialAssign D) (n : ℕ) (d : D) : g.update n d n = some d

@[simp]

theorem Core.PartialAssign.update_ne {D : Type u_1} (g : PartialAssign D) {n m : ℕ} (d : D) (h : m ≠ n) : g.update n d m = g m

theorem Core.PartialAssign.update_self {D : Type u_1} {g : PartialAssign D} {n : ℕ} {a : D} (h : g n = some a) : g.update n a = g

Updating a partial assignment at n to its existing value is a no-op: g.update n a = g whenever g n = some a. The partial-assignment analogue of Function.update_eq_self; needed by formalisations that recover the witness as g(x).get (e.g., Mandelkern's bounded theory §5.6 atomic bound-equivalence proofs).

@[simp]

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

@[simp]

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

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

def Core.PartialAssign.ofTotal {D : Type u_1} (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_1} (g : Assignment D) (n : ℕ) : (ofTotal g).valued n = true

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

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

Originates in plural dynamic semantics ([vdB96], [Nou03], [Bra08]). The plural information state is the basic carrier of Plural CDRT (Brasoveanu, Dotlačil) and its partial extension PPCDRT (Haug 2014, [HD20]). Spector's static reuse ([Spe25]) is the trivalent point of this primitive: variables that are singular across the plural state behave classically; variables that are not are gappy.

Wrapped in a structure so the bespoke Membership instance is found by typeclass search instead of mathlib's Set instances.

Consumers: Studies/Spector2025.lean (trivalent), Semantics/Dynamic/PPCDRT/ (plural partial CDRT).

• pred : PartialAssign D → Prop

  The membership predicate on atomic assignments.

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

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

@[implicit_reducible]

instance Core.PluralAssign.instMembershipPartialAssign {D : Type u_1} : 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.IsNonempty {D : Type u_1} (G : PluralAssign D) : Prop

Whether G contains at least one atomic assignment. Named IsNonempty rather than Nonempty to avoid shadowing _root_.Nonempty.

Equations

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

def Core.PluralAssign.restrict {D : Type u_1} (G : PluralAssign D) (x : ℕ) (a : D) : PluralAssign D

Restrict a plural assignment to atomic assignments mapping x to a. Spector §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_1} (G : PluralAssign D) (x : ℕ) : 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.null {D : Type u_1} : PluralAssign D

The universal plural assignment: contains every partial assignment. Spector §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_1} (p : PartialAssign D → Prop) : PluralAssign D

Build a plural assignment from a predicate.

Equations

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

def Core.PluralAssign.singleton {D : Type u_1} (g : PartialAssign D) : PluralAssign D

The singleton plural assignment containing exactly g. The minimal plural state — used for the singleton-collapse bridges between PPCDRT and the singular CDRT-style semantics.

Equations

• Core.PluralAssign.singleton g = { pred := fun (g' : Core.PartialAssign D) => g' = g }

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

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

NOTE: this allows assignments where x is undefined to coexist with assignments where x = d (only the defined rows are required to agree). The all-defined reading would be stronger; the present reading is the one Spector's static reuse of plural states needs.

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)

def Core.PluralAssign.singular {D : Type u_1} (G : PluralAssign D) (x : ℕ) : Prop

singular G x ↔ there is some d such that G assigns x uniquely to it. Spector's atomic(x) predicate; replaces U(x) from the simplified system.

Equations

• G.singular x = ∃ (d : D), G.singularAt x d

def Core.PluralAssign.sumDref {D : Type u_1} (G : PluralAssign D) (n : ℕ) : Set D

Sum-of-values for dref n across the plural state. Spector §6.2 and [HD20]'s ∪u operator (paper §2.1, eq 8): the set of values that n takes across all atomic assignments in G.

Equations

• G.sumDref n = {d : D | ∃ (g : Core.PartialAssign D), g ∈ G ∧ g n = some d}