Variable assignments

A variable assignment maps variables to values. Three registers share this file: total assignments (Tarski-style, [HK98], [HMT71]), partial assignments (variables may be unvalued, [Spe25], [BK01]), and plural assignments (sets of partial assignments — the information states of plural dynamic semantics, [vdB96], [Bra08], [HD20]).

Main definitions

• Assignment E: total assignments ℕ → E, on the Heim–Kratzer ℕ-register.
• PartialAssign Var D: partial assignments Var → Option D.
• PluralAssign Var D: sets of partial assignments, with the [Spe25] / [HD20] operators restrict, singularAt, singular, sumDref.

Implementation notes

• PartialAssign is the decidable counterpart of mathlib's partial functions Var →. D: Part-valued partiality would forfeit DecidableEq on assignments, which Finset-state systems (QBSML) and decide-checked studies need.
• Update is mathlib's Function.update; PartialAssign.update only fuses the some (cf. Finsupp.update), and its lemmas are one-step consequences of the Function.update_* laws. Definedness is (g x).isSome — there is no wrapper predicate. The Heim–Kratzer notation g[n ↦ x] for total update is declared in Semantics/Intensional/Variables.lean.
• Use these names only for the variable-binding role — the state that quantifiers update and free variables look up. A ℕ → E that is not variable-binding state (interpretation tables, lookup arrays) should stay a plain function type.

Total assignments

@[reducible, inline]

abbrev Assignment (E : Type u_1) : Type u_1

Total variable assignment on the ℕ-register: instantiated at the entity type for entity pronouns, at indices for situation pronouns, at Time for temporal variables. Update is Function.update directly — no parallel API.

Equations

• Assignment E = (ℕ → E)

Partial assignments

@[reducible, inline]

abbrev PartialAssign (Var : Type u_1) (D : Type u_2) : Type (max u_1 u_2)

Partial assignment: g x = none means x is unvalued. Trivalent systems read the gap as the third value; state-based systems (QBSML.Index) carry one per world–assignment index.

Equations

• PartialAssign Var D = (Var → Option D)

def PartialAssign.empty {Var : Type u_1} {D : Type u_2} : PartialAssign Var D

The assignment valuing no variables.

Equations

• PartialAssign.empty x✝ = none

def PartialAssign.update {Var : Type u_1} {D : Type u_2} [DecidableEq Var] (g : PartialAssign Var D) (x : Var) (d : D) : PartialAssign Var D

Update at x: Function.update with the value wrapped in some.

Equations

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

@[simp]

theorem PartialAssign.update_at {Var : Type u_1} {D : Type u_2} [DecidableEq Var] (g : PartialAssign Var D) (x : Var) (d : D) : g.update x d x = some d

@[simp]

theorem PartialAssign.update_ne {Var : Type u_1} {D : Type u_2} [DecidableEq Var] (g : PartialAssign Var D) {x y : Var} (d : D) (h : y ≠ x) : g.update x d y = g y

theorem PartialAssign.update_self {Var : Type u_1} {D : Type u_2} [DecidableEq Var] {g : PartialAssign Var D} {x : Var} {a : D} (h : g x = some a) : g.update x a = g

Updating at x to its existing value is a no-op — the partial-assignment face of Function.update_eq_self, for proofs that recover the witness as (g x).get.

Plural assignments

@[reducible, inline]

abbrev PluralAssign (Var : Type u_1) (D : Type u_2) : Type (max u_2 u_1)

Plural assignment: a set of partial assignments, the plural information state of [vdB96]-style dynamic semantics (Plural CDRT, PPCDRT) and of [Spe25]'s static reuse. The full Set API applies: ∅, Set.univ, {g}, ∪, ⊆, Set.Nonempty, …

Equations

• PluralAssign Var D = Set (PartialAssign Var D)

def PluralAssign.restrict {Var : Type u_1} {D : Type u_2} (G : PluralAssign Var D) (x : Var) (a : D) : PluralAssign Var D

The assignments in G mapping x to a ([Spe25] §6.2: G_{x=a}).

Equations

• G.restrict x a = {g : PartialAssign Var D | g ∈ G ∧ g x = some a}

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

G assigns x uniquely to d: some assignment maps x to d, and every assignment valuing x agrees ([Spe25] §6.2). Assignments leaving x unvalued may coexist — only the valued rows must agree, which is the reading Spector's static reuse needs.

Equations

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

def PluralAssign.singular {Var : Type u_1} {D : Type u_2} (G : PluralAssign Var D) (x : Var) : Prop

G assigns x uniquely to some value — [Spe25]'s atomic(x).

Equations

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

def PluralAssign.sumDref {Var : Type u_1} {D : Type u_2} (G : PluralAssign Var D) (x : Var) : Set D

The values x takes across G — [HD20]'s ∪u operator.

Equations

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