Visser (1998): Contexts in Dynamic Predicate Logic

[Vis98]

Contexts in Dynamic Predicate Logic. Journal of Logic, Language, and Information 7: 21–52. A context in the type-theoretic sense — a declaration of variables — for DPL: a 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 DPLRel substrate.

Main results

• Context with 1, *, and ≤: the contexts form a monoid and the information order is a partial order (Theorem 3.3).
• IsCRel c R: R is a c-relation (Definition 3.4), with isCRel_iff_eq recovering the paper's equational form R = (≡ᵢ ; R ; ≡ₒ) ∩ [B].
• IsCRel.mono: the order is sound for the typing — c ≤ d types more relations (Theorem 3.5(1)).
• IsCRel.patch: the unique-output lemma (Lemma 3.7).
• IsCRel.conj, IsCRel.impl: composition and implication typing (Theorems 3.8–3.9), and the typing of DPL's generators — isCRel_atom (conditions at ⟨V, ∅, V⟩) and isCRel_reset (random reset at ⟨∅, {x}, {x}⟩).

The converse of Theorem 3.5 (for |D| ≥ 2) and §§4–5's Switching Property characterization of the DPL-expressible relations await a follow-up; the latter's completeness direction needs the syntax stratum.

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.

@[implicit_reducible]

instance Visser1998.Context.instOne : One Context

Equations

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

@[implicit_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 = ∅

@[implicit_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.

@[implicit_reducible]

instance Visser1998.Context.instPartialOrder : PartialOrder 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. A partial order (Theorem 3.3).

Equations

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

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

c-relations (Definition 3.4)

structure Visser1998.IsCRel {M : Type u_1} (c : Context) (R : DPL.DPLRel M) : Prop

R is a c-relation (Definition 3.4): it reads inputs only at c.I, constrains outputs only at c.O, and changes values only at c.B. blocks is R ⊆ [B]; stable is the nontrivial inclusion of the paper's equation R = (≡ᵢ ; R ; ≡ₒ) ∩ [B].

• blocks ⦃f g : ℕ → M⦄ : R f g → ∀ v ∉ c.B, f v = g v

  Only blocked variables change.

• stable ⦃f f' g g' : ℕ → M⦄ : R f g → (∀ v ∈ c.I, f' v = f v) → (∀ v ∈ c.O, g v = g' v) → (∀ v ∉ c.B, f' v = g' v) → R f' g'

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

theorem Visser1998.isCRel_iff_eq {M : Type u_1} (c : Context) (R : DPL.DPLRel M) : IsCRel c R ↔ R = fun (f' g' : ℕ → M) => (∃ (f : ℕ → M) (g : ℕ → M), (∀ v ∈ c.I, f' v = f v) ∧ R f g ∧ ∀ v ∈ c.O, g v = g' v) ∧ ∀ v ∉ c.B, f' v = g' v

The paper's equational form of Definition 3.4.

The order is sound for the typing (Theorem 3.5)

theorem Visser1998.IsCRel.mono {M : Type u_1} {c d : Context} {R : DPL.DPLRel M} (hcd : c ≤ d) (h : IsCRel c R) : IsCRel d R

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.IsCRel.patch {M : Type u_1} {c : Context} {R : DPL.DPLRel M} (h : IsCRel c R) {f f' g : ℕ → M} (hI : ∀ v ∈ c.I, f' v = f v) (hR : R f g) : R f' fun (v : ℕ) => if v ∈ c.B then g v else f' v

Lemma 3.7: if R is a c-relation, f' ≡ᵢ f, and f R g, then f' reaches the patch of f' by g at the blocks — the unique output agreeing with g on the blocks.

Composition and implication typing (Theorems 3.8–3.9)

theorem Visser1998.IsCRel.conj {M : Type u_1} {c d : Context} {R S : DPL.DPLRel M} (hR : IsCRel c R) (hS : IsCRel d S) : IsCRel (c * d) (R.conj S)

Theorem 3.8: composition of a c-relation and a d-relation is a c * d-relation. The stability witness is the paper's three-zone patch on the intermediate assignment: keep it at c.O ∪ d.I, take the new output at the old blocks, the new input elsewhere.

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

The implication context: c → d = ⟨I ∪ (I'∖B), ∅, I ∪ (I'∖B)⟩ — implications are tests reading the combined inputs.

Equations

• c.dimpl d = { I := c.I ∪ d.I \ c.B, B := ∅, O := c.I ∪ d.I \ c.B, coh := ⋯ }

theorem Visser1998.IsCRel.impl {M : Type u_1} {c d : Context} {R S : DPL.DPLRel M} (hR : IsCRel c R) (hS : IsCRel d S) : IsCRel (c.dimpl d) (R.impl S)

Theorem 3.9: DPL implication of a c-relation and a d-relation is a (c → d)-relation, via two applications of the patch lemma.

The DPL generators, typed

theorem Visser1998.isCRel_atom {M : Type u_1} (V : Finset ℕ) (p : (ℕ → M) → Prop) (hp : ∀ ⦃f f' : ℕ → M⦄, (∀ v ∈ V, f v = f' v) → p f → p f') : IsCRel { I := V, B := ∅, O := V, coh := ⋯ } (DPL.DPLRel.atom p)

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

def Visser1998.reset {M : Type u_1} (x : ℕ) : DPL.DPLRel M

The random reset at x — differ at most at x, [Vis98]'s [x] — read as a DPLRel.

Equations

• Visser1998.reset x f g = ∀ (v : ℕ), v ≠ x → f v = g v

theorem Visser1998.isCRel_reset {M : Type u_1} (x : ℕ) : IsCRel { I := ∅, B := {x}, O := {x}, coh := ⋯ } (reset x)

The reset is a ⟨∅, {x}, {x}⟩-relation: it reads nothing, blocks x, and writes x.