Register structures

A register structure is a type of states with registers, each register holding a value that can be read (val) and updated (extend) according to the laws of Function.update. The canonical example is a function type, whose coordinates are the registers. Muskens grafts discourse representation theory onto type logic over such states: random assignment [r] resets a register, and a box [u₁ … uₙ | C] resets its registers and tests C. The conditions over a register structure form a cylindric algebra in the sense of Henkin, Monk and Tarski, in which cylindrification is the weakest precondition of [r].

Main definitions

• RegisterStructure R S E, with its canonical instance at V → E.
• RegisterStructure.cylindricAlgebra: the cylindric algebra of conditions.
• Update.randomAssign, Update.dexists, Update.dforall: random assignment and the dynamic quantifiers.
• Update.box: the box [u₁ … uₙ | C] over a finite set of registers.
• Update.Fixes, Update.maxAt: an update leaves a register unchanged, and maximization over a register's value.

Main results

• Update.randomAssign_comp_self, Update.commute_randomAssign: random assignments are idempotent and commute; with the SetRel.IsRefl, IsSymm and IsTrans instances, each is an equivalence.
• Update.preimage_randomAssign, Update.core_randomAssign, Update.dom_dexists: the weakest precondition of [r] is cylindrification and its dual the universal; an existential is true where the cylindrification of its scope's truth set is.
• Update.commute_test_randomAssign_iff: a test commutes with [r] exactly when r is outside the dimension set of its condition.
• Update.box_comp_box: two boxes in sequence are one box over the union of their registers when the second's registers lie outside the dimension set of the first's condition (Muskens's Merging Lemma).
• Update.exists_box_map_iff, Update.mem_dom_box_map: quantifying over the outputs of a box over distinct registers is quantifying over tuples of values, so a box whose condition reads only its registers is true iff some tuple satisfies it (Muskens's Unselective Binding Lemma).
• Update.mem_box_iff: at assignments, a box relates an assignment to those that agree with it off the box's registers and satisfy its condition.
• RegisterStructure.dimSet_preimage_subset: a condition read off registers in s has its dimension set inside s.

Implementation notes

Muskens defines i[r]j as agreement on every register other than r and asserts that enough states exist (AX1). Here [r] is the graph of extend · r e, which agrees with his relation when a state is determined by its registers, as in every instance; it also serves states carrying several sorts of registers (Semantics/Dynamic/ICDRT.lean), and its uniqueness gives the diagonal axioms of the cylindric algebra. Constant registers (AX4) are constant functions of the state, and AX3, that distinct referents denote distinct registers, is a hypothesis where it is used.

References

• R. Muskens, Combining Montague semantics and discourse representation (1996)
• J. Groenendijk and M. Stokhof, Dynamic predicate logic (1991)
• L. Henkin, J. D. Monk and A. Tarski, Cylindric algebras, part I (1971)

class DynamicSemantics.RegisterStructure (R : Type u_1) (S : Type u_2) (E : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

A register structure has registers R (Muskens's type π), a value function val (his V) and a register-wise update extend satisfying the laws of Function.update. extend skolemizes AX1.

• val : R → S → E

  The value of a register in a state (Muskens's V).

• extend : S → R → E → S

  Update a state at a register (AX1's witness).

• val_extend_self (i : S) (r : R) (e : E) : val r (extend i r e) = e

  The updated register holds the new value.

• val_extend_of_ne (i : S) (r r' : R) (e : E) : r' ≠ r → val r' (extend i r e) = val r' i

  Other registers are untouched.

• extend_eq_self (i : S) (r : R) : extend i r (val r i) = i

  Updating a register to its own value does nothing.

• extend_idem (i : S) (r : R) (e e' : E) : extend (extend i r e) r e' = extend i r e'

  A second update of a register overrides the first.

• extend_comm (i : S) {r r' : R} (h : r ≠ r') (e e' : E) : extend (extend i r e) r' e' = extend (extend i r' e') r e

  Updates of distinct registers commute.

@[instance_reducible]

instance DynamicSemantics.RegisterStructure.instPi {V : Type u_1} {E : Type u_2} [DecidableEq V] : RegisterStructure V (V → E) E

In the canonical register structure the registers are the coordinates of a function type and update is Function.update.

Equations

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

@[instance_reducible]

instance DynamicSemantics.RegisterStructure.cylindricAlgebra {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] : CylindricAlgebra R (Set S)

The conditions over a register structure form a cylindric algebra. Cylindrification along r holds where some update of r satisfies the condition, and the diagonal of r and r' holds where the two registers have the same value.

Equations

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

@[simp]

theorem DynamicSemantics.RegisterStructure.mem_cyl {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i : S} {C : Set S} : i ∈ CylindricAlgebra.cyl r C ↔ ∃ (e : E), extend i r e ∈ C

@[simp]

theorem DynamicSemantics.RegisterStructure.mem_diag {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r r' : R} {i : S} : i ∈ CylindricAlgebra.diag r r' ↔ val r i = val r' i

theorem DynamicSemantics.RegisterStructure.notMem_dimSet_iff {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {C : Set S} : r ∉ CylindricAlgebra.dimSet C ↔ ∀ (i : S) (e : E), extend i r e ∈ C ↔ i ∈ C

A register lies outside the dimension set of a condition exactly when updating it never changes whether the condition holds.

theorem DynamicSemantics.RegisterStructure.dimSet_preimage_subset {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {α : Type u_4} {s : Set R} (f : S → α) (hf : ∀ r ∉ s, ∀ (i : S) (e : E), f (extend i r e) = f i) (P : Set α) : CylindricAlgebra.dimSet (f ⁻¹' P) ⊆ s

A condition read off a function of the state that no update outside s changes has its dimension set inside s, as CylindricAlgebra.dimSet_subset_of_dependsOn says of predicates on assignments.

theorem DynamicSemantics.RegisterStructure.dimSet_preimage_val_subset {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (u : R) (P : Set E) : CylindricAlgebra.dimSet (val u ⁻¹' P) ⊆ {u}

A condition on the value of one register has its dimension set inside that register.

@[simp]

theorem DynamicSemantics.RegisterStructure.extend_eq_update {V : Type u_4} {E : Type u_5} [DecidableEq V] (g : V → E) (x : V) (e : E) : extend g x e = Function.update g x e

@[simp]

theorem DynamicSemantics.RegisterStructure.val_apply {V : Type u_4} {E : Type u_5} [DecidableEq V] (g : V → E) (x : V) : val x g = g x

def DynamicSemantics.Update.randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) : Update S

Random assignment [r] gives the register r an arbitrary value.

Equations

• DynamicSemantics.Update.randomAssign r = {(a, b) : S × S | ∃ (e : E), b = DynamicSemantics.RegisterStructure.extend a r e}

theorem DynamicSemantics.Update.mem_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i j : S} : (i, j) ∈ randomAssign r ↔ ∃ (e : E), j = RegisterStructure.extend i r e

instance DynamicSemantics.Update.instIsReflRandomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} : SetRel.IsRefl (randomAssign r)

instance DynamicSemantics.Update.instIsSymmRandomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} : SetRel.IsSymm (randomAssign r)

instance DynamicSemantics.Update.instIsTransRandomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} : SetRel.IsTrans (randomAssign r)

@[simp]

theorem DynamicSemantics.Update.randomAssign_comp_self {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} : SetRel.comp (randomAssign r) (randomAssign r) = randomAssign r

Random assignment is idempotent.

theorem DynamicSemantics.Update.commute_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r r' : R) : Commute (randomAssign r) (randomAssign r')

Random assignments commute.

theorem DynamicSemantics.Update.preimage_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (t : Condition S) : SetRel.preimage (randomAssign r) t = CylindricAlgebra.cyl r t

The weakest precondition of a random assignment is cylindrification.

theorem DynamicSemantics.Update.core_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (t : Condition S) : SetRel.core (randomAssign r) t = {i : S | ∀ (e : E), RegisterStructure.extend i r e ∈ t}

The dual weakest precondition of a random assignment is universal quantification over the register.

theorem DynamicSemantics.Update.commute_test_randomAssign_iff {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {C : Condition S} : Commute (test C) (randomAssign r) ↔ r ∉ CylindricAlgebra.dimSet C

A test commutes with a random assignment exactly when the register is outside the dimension set of its condition.

def DynamicSemantics.Update.dexists {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (D : Update S) : Update S

The existential update ∃r(D) is [r]; D.

Equations

• DynamicSemantics.Update.dexists r D = SetRel.comp (DynamicSemantics.Update.randomAssign r) D

def DynamicSemantics.Update.dforall {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (D : Update S) : Condition S

The universal condition ∀r(D) holds iff D has an output from every r-variant, which is the clause of [GS91a] for the universal.

Equations

• DynamicSemantics.Update.dforall r D = (DynamicSemantics.Update.randomAssign r).impl D

theorem DynamicSemantics.Update.mem_dexists {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i j : S} {D : Update S} : (i, j) ∈ dexists r D ↔ ∃ (e : E), (RegisterStructure.extend i r e, j) ∈ D

An existential runs its scope from some update of the input at r.

theorem DynamicSemantics.Update.mem_dforall {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i : S} {D : Update S} : i ∈ dforall r D ↔ ∀ (e : E), RegisterStructure.extend i r e ∈ SetRel.dom D

A universal holds when its scope has an output from every update of the input at r.

theorem DynamicSemantics.Update.dom_dexists {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} (D : Update S) : SetRel.dom (dexists r D) = CylindricAlgebra.cyl r (SetRel.dom D)

An existential is true where the cylindrification of its scope's truth set is.

Frame conditions and maximization

def DynamicSemantics.Update.Fixes {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (D : Update S) : Prop

An update D fixes the register r if no output of D changes its value.

Equations

• DynamicSemantics.Update.Fixes r D = ∀ (i j : S), (i, j) ∈ D → DynamicSemantics.RegisterStructure.val r j = DynamicSemantics.RegisterStructure.val r i

theorem DynamicSemantics.Update.Fixes.comp {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {D₁ D₂ : Update S} (h₁ : Fixes r D₁) (h₂ : Fixes r D₂) : Fixes r (SetRel.comp D₁ D₂)

theorem DynamicSemantics.Update.fixes_id {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) : Fixes r SetRel.id

theorem DynamicSemantics.Update.fixes_test {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (C : Condition S) : Fixes r (test C)

theorem DynamicSemantics.Update.fixes_randomAssign_of_ne {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r r' : R} (h : r' ≠ r) : Fixes r' (randomAssign r)

A random assignment fixes every other register.

@[reducible, inline]

abbrev DynamicSemantics.Update.maxAt {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] [Preorder E] (r : R) (D : Update S) : Update S

Maximization over a register keeps the outputs of D at which no other output gives r a strictly greater value.

Equations

• DynamicSemantics.Update.maxAt r D = DynamicSemantics.Update.maxBy (DynamicSemantics.RegisterStructure.val r) D

theorem DynamicSemantics.Update.Fixes.maxBy {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {α : Type u_4} [Preorder α] {f : S → α} {D : Update S} (h : Fixes r D) : Fixes r (Update.maxBy f D)

theorem DynamicSemantics.Update.maxAt_eq_of_fixes {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} [Preorder E] {D : Update S} (h : Fixes r D) : maxAt r D = D

Maximizing a register an update fixes is vacuous, since every output agrees with the input there.

Boxes

def DynamicSemantics.Update.box {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (s : Finset R) (C : Condition S) : Update S

The box [u₁ … uₙ | C] of [Mus96]'s ABB3 assigns the registers of s at random and then tests C. Random assignments commute, so a box needs only the set of its registers.

Equations

• DynamicSemantics.Update.box s C = s.noncommProd DynamicSemantics.Update.randomAssign ⋯ * DynamicSemantics.Update.test C

@[simp]

theorem DynamicSemantics.Update.box_empty {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (C : Condition S) : box ∅ C = test C

theorem DynamicSemantics.Update.box_singleton {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (C : Condition S) : box {r} C = dexists r (test C)

A one-register box is an existential over a test.

theorem DynamicSemantics.Update.mem_box_singleton {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i j : S} {C : Condition S} : (i, j) ∈ box {r} C ↔ (i, j) ∈ randomAssign r ∧ j ∈ C

The box [r | C] assigns r at random and then tests C.

theorem DynamicSemantics.Update.commute_box_randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {C : Condition S} (s : Finset R) (h : r ∉ CylindricAlgebra.dimSet C) : Commute (box s C) (randomAssign r)

A box commutes with a random assignment whose register lies outside the dimension set of its condition.

theorem DynamicSemantics.Update.fixes_box {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {s : Finset R} (h : r ∉ s) (C : Condition S) : Fixes r (box s C)

A box fixes every register outside it.

theorem DynamicSemantics.Update.box_insert {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] [DecidableEq R] (r : R) (s : Finset R) (C : Condition S) : box (insert r s) C = SetRel.comp (randomAssign r) (box s C)

Prefixing a random assignment adds its register to a box.

theorem DynamicSemantics.Update.mem_box_insert {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i j : S} {C : Condition S} [DecidableEq R] {s : Finset R} : (i, j) ∈ box (insert r s) C ↔ ∃ (e : E), (RegisterStructure.extend i r e, j) ∈ box s C

theorem DynamicSemantics.Update.mem_box_insert_of_mem {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {r : R} {i j : S} {C : Condition S} [DecidableEq R] {s : Finset R} {k : S} (hk : (i, k) ∈ randomAssign r) (hj : (k, j) ∈ box s C) : (i, j) ∈ box (insert r s) C

A random assignment to r followed by a box gives the box with r added.

theorem DynamicSemantics.Update.preimage_box_insert {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] [DecidableEq R] (r : R) (s : Finset R) (C t : Condition S) : SetRel.preimage (box (insert r s) C) t = CylindricAlgebra.cyl r (SetRel.preimage (box s C) t)

The weakest precondition of a box quantifies over each of its registers.

theorem DynamicSemantics.Update.box_comp_box {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] {C : Condition S} [DecidableEq R] {s t : Finset R} {C' : Condition S} (h : ∀ r ∈ t, r ∉ CylindricAlgebra.dimSet C) : SetRel.comp (box s C) (box t C') = box (s ∪ t) (C ∩ C')

Two boxes in sequence are one box, provided no register of the second occurs in the conditions of the first (the Merging Lemma of [Mus96]).

theorem DynamicSemantics.Update.exists_box_map_iff {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] [DecidableEq R] {n : ℕ} (u : Fin n ↪ R) (φ : (Fin n → E) → Prop) (i : S) : (∃ (j : S), (i, j) ∈ box (Finset.map u Finset.univ) Set.univ ∧ φ fun (k : Fin n) => RegisterStructure.val (u k) j) ↔ ∃ (x : Fin n → E), φ x

For distinct registers u₀ … uₙ₋₁, the states that differ from i at most there realize every tuple of values, so a quantifier over them is a quantifier over the tuples (the Unselective Binding Lemma of [Mus96]).

theorem DynamicSemantics.Update.mem_dom_box_map {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] [DecidableEq R] {n : ℕ} (u : Fin n ↪ R) (P : (Fin n → E) → Prop) (i : S) : i ∈ SetRel.dom (box (Finset.map u Finset.univ) {j : S | P fun (k : Fin n) => RegisterStructure.val (u k) j}) ↔ ∃ (x : Fin n → E), P x

A box over distinct registers whose condition reads only those registers is true exactly when some tuple of values satisfies the condition.

The canonical register structure

theorem DynamicSemantics.Update.mem_box_iff {V : Type u_4} {E : Type u_5} [DecidableEq V] {g h : V → E} {s : Finset V} {C : Condition (V → E)} : (g, h) ∈ box s C ↔ (∀ y ∉ s, h y = g y) ∧ h ∈ C

At the canonical register structure, a box relates an assignment to the assignments that agree with it off the box's registers and satisfy its condition.

theorem DynamicSemantics.Update.mem_randomAssign_iff_eqOn {V : Type u_4} {E : Type u_5} [DecidableEq V] {g h : V → E} {x : V} : (g, h) ∈ randomAssign x ↔ Set.EqOn g h {x}ᶜ

At the canonical register structure, random assignment at x is agreement off x.