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, [Spe26], [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 → Flat D, ordered by extension, with PartialAssign.domain the variables an assignment values and PartialAssign.single x d the assignment valuing x alone.
• PluralAssign Var D: sets of partial assignments, with PluralAssign.value the values a variable takes across them, and the operators of Spector, PluralAssign.restrict, PluralAssign.SingularAt and PluralAssign.Singular, defined from it.

Main results

• PartialAssign.le_iff_eqOn_domain: one assignment extends another when it agrees with it on the other's domain.
• PartialAssign.covBy_iff_exists_update: one assignment covers another when it values exactly one more variable, the counterpart of Set.covBy_iff_exists_insert.
• PluralAssign.singularAt_iff: PluralAssign.SingularAt as Spector states it.
• PluralAssign.singular_iff: a variable is singular when its value set is a nonempty subsingleton.

Notation

• g[n ↦ x]: Function.update g n x, the assignment modification of Heim and Kratzer, scoped to Assignment (open scoped Assignment).

Implementation notes

• PartialAssign takes values in Flat D, the decidable counterpart of mathlib's partial values Part D with the same order (Flat.le_iff_ofOption_le): Part-valued partiality would forfeit DecidableEq on assignments, which Finset-state systems (QBSML) and decide-checked studies need. The pointwise order is extension, ⊥ is the assignment valuing nothing, g x = ⊥ says x is unvalued and g x = ↑d that it has the value d; there is no wrapper predicate.
• Update is mathlib's Function.update; PartialAssign.update only fuses the coercion (cf. Finsupp.update), and its lemmas are one-step consequences of the Function.update_* laws.
• Random assignment [x], relating assignments that agree off x, is DynamicSemantics.Update.randomAssign at the function-type register structure; it is not redefined here.
• 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.

References

• I. Heim, A. Kratzer, Semantics in Generative Grammar (1998)
• L. Henkin, J. D. Monk and A. Tarski, Cylindric algebras, part I (1971)
• B. Spector, Trivalence and transparency: A non-dynamic approach to anaphora (2026)
• D. Beaver, E. Krahmer, A Partial Account of Presupposition Projection (2001)
• M. H. van den Berg, Some aspects of the internal structure of discourse: the dynamics of nominal anaphora (1996)
• A. Brasoveanu, Donkey pluralities: plural information states versus non-atomic individuals (2008)
• D. T. T. Haug and M. Dalrymple, Reciprocity: Anaphora, scope, and quantification (2020)

Total assignments

@[reducible, inline]

abbrev Assignment (E : Type u_1) : Type u_1

Assignment E is the type of total variable assignments, sending each index in ℕ to a value in E: an entity for entity pronouns, a situation index for situation pronouns, a time for temporal variables.

Equations

• Assignment E = (ℕ → E)

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

g[n ↦ x] is the assignment sending n to x and agreeing with g elsewhere, the assignment modification of Heim and Kratzer. It is notation for Function.update g n x.

Equations

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

Partial assignments

@[reducible, inline]

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

PartialAssign Var D is the type of partial assignments of values in D to variables in Var: g x = ⊥ when g leaves x unvalued, and g ≤ h when h extends g.

Equations

• PartialAssign Var D = (Var → Flat D)

def PartialAssign.domain {Var : Type u_1} {D : Type u_2} (g : PartialAssign Var D) : Set Var

g.domain is the set of variables that g values.

Equations

• g.domain = {x : Var | g x ≠ ⊥}

@[simp]

theorem PartialAssign.mem_domain {Var : Type u_1} {D : Type u_2} {g : PartialAssign Var D} {x : Var} : x ∈ g.domain ↔ g x ≠ ⊥

@[simp]

theorem PartialAssign.domain_bot {Var : Type u_1} {D : Type u_2} : ⊥.domain = ∅

theorem PartialAssign.le_iff_eqOn_domain {Var : Type u_1} {D : Type u_2} {g h : PartialAssign Var D} : g ≤ h ↔ Set.EqOn g h g.domain

h extends g exactly when the two agree on the domain of g.

theorem PartialAssign.domain_mono {Var : Type u_1} {D : Type u_2} {g h : PartialAssign Var D} (hgh : g ≤ h) : g.domain ⊆ h.domain

theorem PartialAssign.covBy_iff {Var : Type u_1} {D : Type u_2} {g h : PartialAssign Var D} : g ⋖ h ↔ ∃ (x : Var), g x = ⊥ ∧ h x ≠ ⊥ ∧ ∀ (y : Var), y ≠ x → g y = h y

h covers g exactly when h values one variable that g leaves unvalued and agrees with g on all others.

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

g.update x d sends x to d and agrees with g elsewhere.

Equations

• g.update x d = Function.update g x ↑d

@[simp]

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

@[simp]

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

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

Updating x to the value it already has leaves g unchanged.

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

@[simp]

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

@[simp]

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

theorem PartialAssign.covBy_update {Var : Type u_1} {D : Type u_2} {g : PartialAssign Var D} [DecidableEq Var] {x : Var} (hx : g x = ⊥) (d : D) : g ⋖ g.update x d

Valuing an unvalued variable is a covering step of the extension order.

theorem PartialAssign.covBy_iff_exists_update {Var : Type u_1} {D : Type u_2} {g h : PartialAssign Var D} [DecidableEq Var] : g ⋖ h ↔ ∃ (x : Var) (d : D), g x = ⊥ ∧ g.update x d = h

h covers g exactly when h updates g at a variable g leaves unvalued.

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

single x d sends x to d and leaves every other variable unvalued.

Equations

• PartialAssign.single x d = ⊥.update x d

theorem PartialAssign.bot_update {Var : Type u_1} {D : Type u_2} [DecidableEq Var] (x : Var) (d : D) : ⊥.update x d = single x d

@[simp]

theorem PartialAssign.single_eq_same {Var : Type u_1} {D : Type u_2} {x : Var} [DecidableEq Var] {d : D} : single x d x = ↑d

@[simp]

theorem PartialAssign.single_eq_of_ne {Var : Type u_1} {D : Type u_2} {x y : Var} [DecidableEq Var] {d : D} (h : y ≠ x) : single x d y = ⊥

@[simp]

theorem PartialAssign.domain_single {Var : Type u_1} {D : Type u_2} [DecidableEq Var] (x : Var) (d : D) : (single x d).domain = {x}

Plural assignments

@[reducible, inline]

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

PluralAssign Var D is the type of plural assignments, sets of partial assignments: the plural information states of van den Berg and the assignment sets of Spector.

Equations

• PluralAssign Var D = Set (PartialAssign Var D)

Values

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

G.value x is the set of values x takes in G; assignments leaving x unvalued contribute none.

Equations

• G.value x = {d : D | ∃ g ∈ G, g x = ↑d}

@[simp]

theorem PluralAssign.mem_value {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {d : D} : d ∈ G.value x ↔ ∃ g ∈ G, g x = ↑d

theorem PluralAssign.value_mono {Var : Type u_1} {D : Type u_2} {G H : PluralAssign Var D} {x : Var} (h : G ⊆ H) : G.value x ⊆ H.value x

@[simp]

theorem PluralAssign.value_empty {Var : Type u_1} {D : Type u_2} {x : Var} : ∅.value x = ∅

@[simp]

theorem PluralAssign.value_singleton {Var : Type u_1} {D : Type u_2} {g : PartialAssign Var D} {x : Var} : {g}.value x = {d : D | g x = ↑d}

@[simp]

theorem PluralAssign.value_union {Var : Type u_1} {D : Type u_2} {G H : PluralAssign Var D} {x : Var} : (G ∪ H).value x = G.value x ∪ H.value x

Restriction

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

G.restrict x a is the set of assignments in G sending x to a, the $G_{x=a}$ of Spector (§6.2).

Equations

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

@[simp]

theorem PluralAssign.mem_restrict {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {g : PartialAssign Var D} {x : Var} {a : D} : g ∈ G.restrict x a ↔ g ∈ G ∧ g x = ↑a

theorem PluralAssign.value_restrict_subset {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {a : D} : (G.restrict x a).value x ⊆ {a}

theorem PluralAssign.value_restrict {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {a : D} (h : Set.Nonempty (G.restrict x a)) : (G.restrict x a).value x = {a}

In a nonempty restriction of G to x = a, the only value of x is a.

Singularity

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

G.SingularAt x d says that d is the only value x takes in G; assignments leaving x unvalued are allowed. This is singularity in the sense of Spector (§6.2), and PluralAssign.singularAt_iff states it in Spector's form.

Equations

• G.SingularAt x d = (G.value x = {d})

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

G.Singular x says that x takes exactly one value in G, the $\mathit{atomic}(x)$ of Spector.

Equations

• G.Singular x = ∃ (d : D), G.SingularAt x d

theorem PluralAssign.singularAt_iff {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {d : D} : G.SingularAt x d ↔ (∃ g ∈ G, g x = ↑d) ∧ ∀ g ∈ G, g x ≠ ⊥ → g x = ↑d

G.SingularAt x d holds exactly when some assignment in G sends x to d and every assignment in G that values x sends it to d, as Spector states it.

theorem PluralAssign.singular_iff {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} : G.Singular x ↔ (G.value x).Nonempty ∧ (G.value x).Subsingleton

x is singular in G exactly when it takes at least one value there and at most one.

theorem PluralAssign.SingularAt.unique {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {d d' : D} (h : G.SingularAt x d) (h' : G.SingularAt x d') : d = d'

x is singular in G at no more than one value.

theorem PluralAssign.SingularAt.singular {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {d : D} (h : G.SingularAt x d) : G.Singular x

theorem PluralAssign.SingularAt.eq_of_mem_restrict {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {g : PartialAssign Var D} {x : Var} {a d : D} (h : G.SingularAt x d) (hg : g ∈ G.restrict x a) : a = d

@[simp]

theorem PluralAssign.singularAt_singleton {Var : Type u_1} {D : Type u_2} {g : PartialAssign Var D} {x : Var} {d : D} : {g}.SingularAt x d ↔ g x = ↑d

theorem PluralAssign.singularAt_restrict {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {a : D} (h : Set.Nonempty (G.restrict x a)) : (G.restrict x a).SingularAt x a

A nonempty restriction of G to x = a assigns x uniquely to a.

theorem PluralAssign.singularAt_restrict_iff {Var : Type u_1} {D : Type u_2} {G : PluralAssign Var D} {x : Var} {a d : D} : (G.restrict x a).SingularAt x d ↔ Set.Nonempty (G.restrict x a) ∧ d = a

The restriction of G to x = a assigns x uniquely to d exactly when it is nonempty and d = a.