Plural CDRT

Compositional DRT over plural information states ([vdB96], [Bra07], [Bra10]). An information state is a set of CDRT states, a matrix whose rows are assignments and whose columns are drefs: a dref stores the set of its values in the rows, and the rows store the dependencies between the values of different drefs. A dref takes the dummy value ★ in the rows where it has none; here its register holds a Flat E and ★ is ⊥.

Every CDRT update lifts to plural states cumulatively: the lift is the relation lifting Set.LiftRel of the update, which is the cumulation ** of [BS00], each input row having a successor among the output rows and each output row a predecessor among the input rows. This is how dref introduction [u] lifts to plural states, and the lift is a functor. Atomic conditions hold distributively of the rows where their drefs have values. Structured inclusion selects a subset of a dref's values by discarding rows, so the subset keeps exactly the superset's dependencies. On plural partial assignments a dref's values are PluralAssign.value, its cells the operator restrict, and singular number is PluralAssign.Singular, [Spe26]'s atomic(x).

Main definitions

• PCDRT.value, PCDRT.cell, PCDRT.dep: a dref's values, the rows where it has a given one, and the pairs of values two drefs have in a row.
• PCDRT.intro: dref introduction [u].
• PCDRT.atom, PCDRT.atom₂, PCDRT.sing: distributive predication and singular number.
• PCDRT.structSub, PCDRT.structSubAll: structured inclusion.

Main results

• PCDRT.dom_dep, PCDRT.cod_dep: where every row valuing one dref values the other, the dependency's domain and codomain are the two drefs' values.
• PCDRT.value_eq_of_fixes: a dref an update fixes keeps its values under the lifted update.
• PCDRT.dep_subset_of_structSub, PCDRT.dep_eq_of_structSubAll: a structured subset keeps only, and with the full condition all, of the superset's dependencies.

References

• M. H. van den Berg, Some aspects of the internal structure of discourse: the dynamics of nominal anaphora (1996)
• A. Brasoveanu, Structured nominal and modal reference (2007)
• A. Brasoveanu, Decomposing modal quantification (2010)
• S. Beck and U. Sauerland, Cumulation is needed: A reply to Winter (2000) (2000)
• D. T. T. Haug and M. Dalrymple, Reciprocity: Anaphora, scope, and quantification (2020)
• B. Spector, Trivalence and transparency: A non-dynamic approach to anaphora (2026)

Values, rows and cells

def PCDRT.value {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u : R) (I : Set S) : Set E

The values of u in I, uI ([Bra10] (16), (38)); ★ is not a value.

Equations

• PCDRT.value u I = {x : E | ∃ i ∈ I, DynamicSemantics.RegisterStructure.val u i = ↑x}

def PCDRT.cell {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u : R) (x : E) (I : Set S) : Set S

The rows of I where u has the value x, I_{u=x} ((71)).

Equations

• PCDRT.cell u x I = {i : S | i ∈ I ∧ DynamicSemantics.RegisterStructure.val u i = ↑x}

def PCDRT.dep {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u v : R) (I : Set S) : SetRel E E

The dependency between u and v that I stores: the pairs of their values in a row.

Equations

• PCDRT.dep u v I = {p : E × E | ∃ i ∈ I, DynamicSemantics.RegisterStructure.val u i = ↑p.1 ∧ DynamicSemantics.RegisterStructure.val v i = ↑p.2}

theorem PCDRT.value_singleton_of_eq {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u : R} {i : S} {x : E} (h : DynamicSemantics.RegisterStructure.val u i = ↑x) : value u {i} = {x}

theorem PCDRT.dep_singleton_of_eq {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {i : S} {x y : E} (hu : DynamicSemantics.RegisterStructure.val u i = ↑x) (hv : DynamicSemantics.RegisterStructure.val v i = ↑y) : dep u v {i} = {(x, y)}

theorem PCDRT.fst_mem_value_of_mem_dep {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I : Set S} {p : E × E} (h : p ∈ dep u v I) : p.1 ∈ value u I

theorem PCDRT.snd_mem_value_of_mem_dep {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I : Set S} {p : E × E} (h : p ∈ dep u v I) : p.2 ∈ value v I

theorem PCDRT.value_mono {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u : R} {I J : Set S} (h : I ⊆ J) : value u I ⊆ value u J

theorem PCDRT.dep_mono {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I J : Set S} (h : I ⊆ J) : dep u v I ⊆ dep u v J

theorem PCDRT.dom_dep {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I : Set S} (h : ∀ i ∈ I, DynamicSemantics.RegisterStructure.val u i ≠ ⊥ → DynamicSemantics.RegisterStructure.val v i ≠ ⊥) : (dep u v I).dom = value u I

Where every row valuing u also values v, the values of u are the domain of the dependency between them.

theorem PCDRT.cod_dep {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I : Set S} (h : ∀ i ∈ I, DynamicSemantics.RegisterStructure.val v i ≠ ⊥ → DynamicSemantics.RegisterStructure.val u i ≠ ⊥) : (dep u v I).cod = value v I

Where every row valuing v also values u, the values of v are the codomain of the dependency between them.

theorem PCDRT.cell_eq_restrict {Var : Type u_4} {D : Type u_5} [DecidableEq Var] (G : PluralAssign Var D) (x : Var) (a : D) : cell x a G = G.restrict x a

On plural partial assignments, a cell is [Spe26]'s restriction G_{x=a}.

theorem PCDRT.value_eq_pluralAssign_value {Var : Type u_4} {D : Type u_5} [DecidableEq Var] (G : PluralAssign Var D) (x : Var) : value x G = G.value x

On plural partial assignments, a dref's values are PluralAssign.value.

Dref introduction and conditions

def PCDRT.intro {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u : R) : DynamicSemantics.Update (Set S)

Dref introduction [u] ([Bra10] (18)): the cumulative lift of CDRT's random assignment.

Equations

• PCDRT.intro u = (DynamicSemantics.Update.randomAssign u).cumul

theorem PCDRT.singleton_mem_intro {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (i : S) (u : R) (e : Flat E) : ({i}, {DynamicSemantics.RegisterStructure.extend i u e}) ∈ intro u

Introducing u at a one-row state can give it any value.

theorem PCDRT.value_eq_of_fixes {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {v : R} {I J : Set S} {D : DynamicSemantics.Update S} (h : DynamicSemantics.Update.Fixes v D) (hIJ : (I, J) ∈ D.cumul) : value v J = value v I

The lift of an update that fixes v leaves v's values alone.

theorem PCDRT.value_intro_of_ne {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u v : R} {I J : Set S} (h : v ≠ u) (hIJ : (I, J) ∈ intro u) : value v J = value v I

Introducing u leaves every other dref's values alone.

def PCDRT.atom {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (P : E → Prop) (u : R) : DynamicSemantics.Condition (Set S)

A unary atomic condition P{u} ((30)): u has values, and all of them satisfy P.

Equations

• PCDRT.atom P u = {I : Set S | (PCDRT.value u I).Nonempty ∧ ∀ x ∈ PCDRT.value u I, P x}

def PCDRT.atom₂ {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (P : E → E → Prop) (u v : R) : DynamicSemantics.Condition (Set S)

A binary atomic condition P{u, v} ((32)): some row values both drefs, and the values in every such row are related by P.

Equations

• PCDRT.atom₂ P u v = {I : Set S | Set.Nonempty (PCDRT.dep u v I) ∧ ∀ p ∈ PCDRT.dep u v I, P p.1 p.2}

def PCDRT.sing {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u : R) : DynamicSemantics.Condition (Set S)

Singular number sing(u) ((39)): u has exactly one value.

Equations

• PCDRT.sing u = {I : Set S | ∃ (x : E), PCDRT.value u I = {x}}

theorem PCDRT.mem_sing_iff_singular {Var : Type u_4} {D : Type u_5} [DecidableEq Var] {G : PluralAssign Var D} {x : Var} : G ∈ sing x ↔ G.Singular x

On plural partial assignments, singular number is [Spe26]'s atomic(x).

Structured inclusion

def PCDRT.structSub {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u' u : R) : DynamicSemantics.Condition (Set S)

Structured inclusion u' ⋐ u ((66)): in every row, u' has u's value or ★.

Equations

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

def PCDRT.structSubAll {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] (u' u : R) : DynamicSemantics.Condition (Set S)

Full structured inclusion u' ⊑ u ((68)): structured inclusion that also keeps every row in which u has one of u''s values.

Equations

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

theorem PCDRT.dep_subset_of_structSub {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u u' v : R} {I : Set S} (h : I ∈ structSub u' u) : dep u' v I ⊆ dep u v I

A structured subset keeps only the superset's dependencies (p. 465): whatever u' is paired with in a row, u is paired with there too.

theorem PCDRT.dep_eq_of_structSubAll {R : Type u_1} {S : Type u_2} {E : Type u_3} [DynamicSemantics.RegisterStructure R S (Flat E)] {u u' v : R} {I : Set S} (h : I ∈ structSubAll u' u) : dep u' v I = {p : E × E | p ∈ dep u v I ∧ p.1 ∈ value u' I}

A fully structured subset keeps all of the superset's dependencies at its own values (p. 466).