Visser (1998): Contexts in Dynamic Predicate Logic

This file formalizes the parts of [Vis98], "Contexts in dynamic predicate logic", that are particular to the paper. Its central notions are the substrate of DPL/Context.lean: a context is a triple of finite variable sets, the inputs a relation reads, the blocks at which it cuts the link between input and output value, and the outputs it constrains (DPL.Context, Definition 3.1, with the monoid and the information order of Theorem 3.3); a relation has a context when it reads only the inputs, constrains only the outputs and changes only the blocks (DPL.HasContext, Definition 3.4); the order is sound for the typing (Theorem 3.5), the output over a varied input is unique (Lemma 3.7), composition and implication are typed (Theorems 3.8 and 3.9), and every formula's interpretation is typed by its context (Definition 3.12 and Theorem 3.13, DPL.Formula.hasContext_eval). What remains here is the paper's equational form of Definition 3.4, through the agreement relations of Definition 2.2, and the language-free soundness result that every DPL-expressible relation has a context (DPLExpressible, Definition 3.10 and Theorem 3.11).

Implementation notes

Variables are natural numbers and the domain is a type parameter. Expressibility is defined on relations, as in the paper, by generation from conditions and resets under composition.

TODO

• The converse of Theorem 3.5, for a domain with at least two elements, and the most informative context of the appendix, the partial meet of contexts as the infimum in the information order.
• The Switching Property characterization of the DPL-expressible relations of §§4-5, to be stated against DPL.Formula.eval, and the meet typing of §6.

References

• [Vis98]
• [GS91a]

Agreement relations (Definition 2.2)

def Visser1998.agreeOn {E : Type u_1} (V : Set ℕ) : DynamicSemantics.Update (Assignment E)

Agreement on V relates the assignments equal on V (Definition 2.2); the reset [x] of the existential is agreement off x, the substrate's randomAssign (mem_randomAssign_iff_eqOn).

Equations

• Visser1998.agreeOn V = {(f, g) : Assignment E × Assignment E | Set.EqOn f g V}

theorem Visser1998.subset_agreeOn_comp {E : Type u_1} (R : DynamicSemantics.Update (Assignment E)) (V W : Set ℕ) : R ⊆ SetRel.comp (agreeOn V) (SetRel.comp R (agreeOn W))

A relation embeds in its composition with agreement on either side.

theorem Visser1998.agreeOn_comp_agreeOn {E : Type u_1} (V W : Set ℕ) : SetRel.comp (agreeOn V) (agreeOn W) = agreeOn (V ∩ W)

Agreements compose to agreement on the intersection.

theorem Visser1998.agreeOn_inter_agreeOn {E : Type u_1} (V W : Set ℕ) : agreeOn V ∩ agreeOn W = agreeOn (V ∪ W)

Agreements meet in agreement on the union.

theorem Visser1998.agreeOn_empty {E : Type u_1} : agreeOn ∅ = Set.univ

Agreement on no variables is trivial.

The equational form of Definition 3.4

theorem Visser1998.hasContext_iff_eq {E : Type u_1} (R : DynamicSemantics.Update (Assignment E)) (c : DPL.Context ℕ) : DPL.HasContext R c ↔ R = SetRel.comp (agreeOn ↑c.I) (SetRel.comp R (agreeOn ↑c.O)) ∩ agreeOn (↑c.B)ᶜ

The paper's equational form of Definition 3.4.

The language-free soundness result (Theorem 3.11)

inductive Visser1998.DPLExpressible {E : Type u_1} : DynamicSemantics.Update (Assignment E) → Prop

The DPL-expressible relations (Definition 3.10): generated by composition from resets and finitely restricted conditions.

• test {E : Type u_1} (V : Finset ℕ) (p : (ℕ → E) → Prop) (hp : ∀ ⦃f f' : ℕ → E⦄, Set.EqOn f f' ↑V → p f → p f') : DPLExpressible (DynamicSemantics.Update.test p)
• randomAssign {E : Type u_1} (x : ℕ) : DPLExpressible (DynamicSemantics.Update.randomAssign x)
• comp {E : Type u_1} {R S : DynamicSemantics.Update (Assignment E)} : DPLExpressible R → DPLExpressible S → DPLExpressible (SetRel.comp R S)

theorem Visser1998.DPLExpressible.hasContext {E : Type u_1} {R : DynamicSemantics.Update (Assignment E)} (h : DPLExpressible R) : ∃ (c : DPL.Context ℕ), DPL.HasContext R c

Theorem 3.11: every DPL-expressible relation is an IBO-relation — typed by some context.