Visser (1998): Contexts in Dynamic Predicate Logic

A context in the type-theoretic sense — a declaration of variables — for DPL: [Vis98]'s triple ⟨I, B, O⟩ of input set, block set, and output set, typing which variables a relation reads, cuts, and writes. The paper's metatheory of these types, over the semantic DPL.Rel substrate.

Main results

• Context with 1, *, and ≤: the contexts form a monoid and the information order is a partial order (Theorem 3.3).
• HasContext R c: c is a context for R (Definition 3.4), with hasContext_iff_eq recovering the paper's equational form of the definition and hasContext_test_iff characterizing the test V-typed relations as the V-invariant tests (Update.IsTest).
• HasContext.mono: the order is sound for the typing — c ≤ d types more relations (Theorem 3.5(1)).
• HasContext.patch, HasContext.patch_eqOn, HasContext.patch_unique: Lemma 3.7 — existence, transfer, and uniqueness of the patched output.
• HasContext.conj, HasContext.impl, HasContext.exists_: composition, implication, and existential typing (Theorems 3.8–3.9 and Definition 3.12's c_{∃v}), from the typed generators hasContext_atom and hasContext_reset.
• DPLExpressible.hasContext: every relation generated by composition from resets and conditions is typed by some context — the language-free soundness result (Definition 3.10, Theorem 3.11).

TODO

• The converse of Theorem 3.5 (|D| ≥ 2) and the most informative context (the paper's Appendix A), with the partial meet of contexts — the infimum in the information order.
• §§4–5's Switching Property characterization of the DPL-expressible relations (the completeness direction needs the syntax stratum), and §6's meet typing.

Contexts (Definition 3.1)

structure Visser1998.Context : Type

A DPL-context (Definition 3.1): input set I (variables the incoming assignment is read at), block set B (variables whose input-output link is cut), output set O (variables the outgoing assignment is constrained at), coherent in the sense I ∪ B = O ∪ B.

• I : Finset ℕ

  The input set.

• B : Finset ℕ

  The block set: the barrier between past and future.

• O : Finset ℕ

  The output set.

• coh : self.I ∪ self.B = self.O ∪ self.B

  Coherence: off the blocks, inputs and outputs coincide.

theorem Visser1998.Context.ext {x y : Context} (I : x.I = y.I) (B : x.B = y.B) (O : x.O = y.O) : x = y

theorem Visser1998.Context.ext_iff {x y : Context} : x = y ↔ x.I = y.I ∧ x.B = y.B ∧ x.O = y.O

theorem Visser1998.Context.coh_mem (c : Context) {v : ℕ} : v ∈ c.I ∪ c.B ↔ v ∈ c.O ∪ c.B

Membership form of coherence.

@[instance_reducible]

instance Visser1998.Context.instOne : One Context

Equations

• Visser1998.Context.instOne = { one := { I := ∅, B := ∅, O := ∅, coh := Visser1998.Context.instOne._proof_1 } }

@[instance_reducible]

instance Visser1998.Context.instMul : Mul Context

Context composition (Definition 3.1): ⟨I,B,O⟩ * ⟨I',B',O'⟩ = ⟨I ∪ (I'∖B), B ∪ B', (O∖B') ∪ O'⟩.

Equations

• Visser1998.Context.instMul = { mul := fun (c d : Visser1998.Context) => { I := c.I ∪ d.I \ c.B, B := c.B ∪ d.B, O := c.O \ d.B ∪ d.O, coh := ⋯ } }

@[simp]

theorem Visser1998.Context.I_mul (c d : Context) : (c * d).I = c.I ∪ d.I \ c.B

@[simp]

theorem Visser1998.Context.B_mul (c d : Context) : (c * d).B = c.B ∪ d.B

@[simp]

theorem Visser1998.Context.O_mul (c d : Context) : (c * d).O = c.O \ d.B ∪ d.O

@[simp]

theorem Visser1998.Context.I_one : I 1 = ∅

@[simp]

theorem Visser1998.Context.B_one : B 1 = ∅

@[simp]

theorem Visser1998.Context.O_one : O 1 = ∅

@[instance_reducible]

instance Visser1998.Context.instMonoid : Monoid Context

The contexts form a monoid (Theorem 3.3).

Equations

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

@[instance_reducible]

instance Visser1998.Context.instLE : LE Context

The information order on contexts (Definition 3.1): more informative contexts read, write, and block more — with new blocks confined to variables the larger context both reads and writes.

Equations

• Visser1998.Context.instLE = { le := fun (c d : Visser1998.Context) => c.I ⊆ d.I ∧ c.O ⊆ d.O ∧ c.B ⊆ d.B ∧ d.B ⊆ c.B ∪ d.I ∩ d.O }

theorem Visser1998.Context.le_def {c d : Context} : c ≤ d ↔ c.I ⊆ d.I ∧ c.O ⊆ d.O ∧ c.B ⊆ d.B ∧ d.B ⊆ c.B ∪ d.I ∩ d.O

@[instance_reducible]

instance Visser1998.Context.instDecidableLE : DecidableLE Context

Equations

• x✝¹.instDecidableLE x✝ = decidable_of_iff' (x✝¹.I ⊆ x✝.I ∧ x✝¹.O ⊆ x✝.O ∧ x✝¹.B ⊆ x✝.B ∧ x✝.B ⊆ x✝¹.B ∪ x✝.I ∩ x✝.O) ⋯

@[instance_reducible]

instance Visser1998.Context.instPartialOrder : PartialOrder Context

The information order is a partial order (Theorem 3.3).

Equations

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

def Visser1998.Context.test (V : Finset ℕ) : Context

The test context at V: reads and writes V, blocks nothing. Conditions live here (hasContext_atom), and implication contexts are tests (Context.impl).

Equations

• Visser1998.Context.test V = { I := V, B := ∅, O := V, coh := ⋯ }

def Visser1998.Context.impl (c d : Context) : Context

The implication context (Definition 3.1): implications are tests reading the combined inputs.

Equations

• c.impl d = Visser1998.Context.test (c * d).I

@[simp]

theorem Visser1998.Context.I_test (V : Finset ℕ) : (test V).I = V

@[simp]

theorem Visser1998.Context.B_test (V : Finset ℕ) : (test V).B = ∅

@[simp]

theorem Visser1998.Context.O_test (V : Finset ℕ) : (test V).O = V

@[simp]

theorem Visser1998.Context.I_impl (c d : Context) : (c.impl d).I = c.I ∪ d.I \ c.B

@[simp]

theorem Visser1998.Context.B_impl (c d : Context) : (c.impl d).B = ∅

@[simp]

theorem Visser1998.Context.O_impl (c d : Context) : (c.impl d).O = c.I ∪ d.I \ c.B

c-relations (Definition 3.4)

structure Visser1998.HasContext {E : Type u_1} (R : DPL.Rel E) (c : Context) : Prop

c is a context for R (Definition 3.4): R reads its input only at c.I, constrains its output only at c.O, and changes values only at c.B.

• blocks ⦃f g : ℕ → E⦄ : R f g → Set.EqOn f g (↑c.B)ᶜ

  Only blocked variables change.

• stable ⦃f f' g g' : ℕ → E⦄ : R f g → Set.EqOn f' f ↑c.I → Set.EqOn g g' ↑c.O → Set.EqOn f' g' (↑c.B)ᶜ → R f' g'

  Membership is invariant under input agreement on I, output agreement on O, and preservation off B.

theorem Visser1998.hasContext_iff_eq {E : Type u_1} (R : DPL.Rel E) (c : Context) : HasContext R c ↔ R = (DPL.agreeOn ↑c.I).conj (R.conj (DPL.agreeOn ↑c.O)) ⊓ DPL.agreeOn (↑c.B)ᶜ

The paper's equational form of Definition 3.4.

theorem Visser1998.hasContext_test_iff {E : Type u_1} {V : Finset ℕ} {R : DPL.Rel E} : HasContext R (Context.test V) ↔ (DPL.toDRS R).IsTest ∧ ∀ ⦃f f' : ℕ → E⦄, Set.EqOn f' f ↑V → R f f → R f' f'

The test V-typed relations are exactly the V-invariant tests — Definition 2.2's ⟨V⟩-conditions (noted after Definition 3.4).

The order is sound for the typing (Theorem 3.5)

theorem Visser1998.HasContext.mono {E : Type u_1} {c d : Context} {R : DPL.Rel E} (h : HasContext R c) (hcd : c ≤ d) : HasContext R d

Theorem 3.5(1): larger contexts type more relations — c ≤ d and R a c-relation make R a d-relation.

The unique-output lemma (Lemma 3.7)

theorem Visser1998.HasContext.patch_eqOn {E : Type u_1} {c : Context} {R : DPL.Rel E} {f f' g : ℕ → E} {J : Set ℕ} (h : HasContext R c) (hR : R f g) (hJ : Set.EqOn f' f J) : Set.EqOn (c.B.piecewise g f') g (J ∪ ↑c.B)

Lemma 3.7, transfer: the patch agrees with g at the blocks and wherever the inputs agree.

theorem Visser1998.HasContext.patch {E : Type u_1} {c : Context} {R : DPL.Rel E} {f f' g : ℕ → E} (h : HasContext R c) (hI : Set.EqOn f' f ↑c.I) (hR : R f g) : R f' (c.B.piecewise g f')

Lemma 3.7, existence: if f' agrees with f on the inputs and f R g, then R relates f' to the patch of f' by g at the blocks.

theorem Visser1998.HasContext.patch_unique {E : Type u_1} {c : Context} {R : DPL.Rel E} {f' g g' : ℕ → E} (h : HasContext R c) (hR : R f' g') (hB : Set.EqOn g' g ↑c.B) : g' = c.B.piecewise g f'

Lemma 3.7, uniqueness: the patch is the only output over f' agreeing with g on the blocks.

Composition and implication typing (Theorems 3.8–3.9)

theorem Visser1998.HasContext.conj {E : Type u_1} {c d : Context} {R S : DPL.Rel E} (hR : HasContext R c) (hS : HasContext S d) : HasContext (R.conj S) (c * d)

Theorem 3.8: composition of a c-relation and a d-relation is a c * d-relation.

theorem Visser1998.HasContext.impl {E : Type u_1} {c d : Context} {R S : DPL.Rel E} (hR : HasContext R c) (hS : HasContext S d) : HasContext (R.impl S) (c.impl d)

Theorem 3.9: DPL implication of a c-relation and a d-relation is a (c → d)-relation.

The DPL generators, typed

theorem Visser1998.hasContext_atom {E : Type u_1} (V : Finset ℕ) (p : (ℕ → E) → Prop) (hp : ∀ ⦃f f' : ℕ → E⦄, Set.EqOn f f' ↑V → p f → p f') : HasContext (DPL.Rel.atom p) (Context.test V)

A condition depending only on V is a Context.test V-relation as a test (the atomic case of the paper's semantic Theorem 3.13).

theorem Visser1998.hasContext_reset {E : Type u_1} (x : ℕ) : HasContext (DPL.reset x) { I := ∅, B := {x}, O := ∅, coh := ⋯ }

The reset is typed at ⟨∅, {x}, ∅⟩ — Definition 3.12's c_{∃v}: it reads nothing, constrains no output, and blocks x.

theorem Visser1998.HasContext.exists_ {E : Type u_1} {c : Context} {φ : DPL.Rel E} (x : ℕ) (h : HasContext φ c) : HasContext (DPL.Rel.exists_ x φ) ({ I := ∅, B := {x}, O := ∅, coh := ⋯ } * c)

The existential typing (Definition 3.12's c_{∃v} • c_φ): blocking x before a c-relation types ∃x φ.

The language-free soundness result (Theorem 3.11)

inductive Visser1998.DPLExpressible {E : Type u_1} : DPL.Rel E → Prop

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

• atom {E : Type u_1} (V : Finset ℕ) (p : (ℕ → E) → Prop) (hp : ∀ ⦃f f' : ℕ → E⦄, Set.EqOn f f' ↑V → p f → p f') : DPLExpressible (DPL.Rel.atom p)
• reset {E : Type u_1} (x : ℕ) : DPLExpressible (DPL.reset x)
• conj {E : Type u_1} {R S : DPL.Rel E} : DPLExpressible R → DPLExpressible S → DPLExpressible (R.conj S)

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

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