def Semantics.Dynamic.Charlow2019.trueAt {E : Type u_1} (K : DPL.DPLRel E) (g : Core.Assignment E) : Prop

Truth at an assignment: K True at g ⟺ ∃h. K g h (Charlow's (7)).

Equations

• Semantics.Dynamic.Charlow2019.trueAt K g = ∃ (h : ℕ → E), K g h

theorem Semantics.Dynamic.Charlow2019.destructive_preserves_truth {E : Type u_1} (P Q : E → Prop) (g : Core.Assignment E) : trueAt ((DPL.DPLRel.exists_ 6 (DPL.DPLRel.atom fun (g' : ℕ → E) => P (g' 6))).conj (DPL.DPLRel.exists_ 6 (DPL.DPLRel.atom fun (g' : ℕ → E) => Q (g' 6)))) g ↔ (∃ (x : E), P x) ∧ ∃ (y : E), Q y

Destructive update preserves truth conditions (§4).

def Semantics.Dynamic.Charlow2019.staticExists {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) : DPL.DPLRel E

Static ↑: evaluates truth, discards modified assignment (Table 1, row 1).

Equations

• Semantics.Dynamic.Charlow2019.staticExists x body = Semantics.Dynamic.DPL.DPLRel.atom fun (g : ℕ → E) => ∃ (d : E), body (Core.Assignment.update g x d)

def Semantics.Dynamic.Charlow2019.dynamicExists {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) : DPL.DPLRel E

Dynamic ↑: retains modified assignment (Table 1, row 2).

Equations

• Semantics.Dynamic.Charlow2019.dynamicExists x body = Semantics.Dynamic.DPL.DPLRel.exists_ x (Semantics.Dynamic.DPL.DPLRel.atom fun (g : ℕ → E) => body g)

theorem Semantics.Dynamic.Charlow2019.static_is_test {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) (g h : Core.Assignment E) : staticExists x body g h → g = h

Static existential is a test: output = input.

theorem Semantics.Dynamic.Charlow2019.dynamic_changes_assignment {E : Type u_1} [Nontrivial E] : ∃ (x : ℕ), ∃ (body : Core.Assignment E → Prop), ∃ (g : Core.Assignment E), ∃ (h : Core.Assignment E), dynamicExists x body g h ∧ g ≠ h

Dynamic existential can change the assignment.

theorem Semantics.Dynamic.Charlow2019.static_dynamic_same_truth {E : Type u_1} (x : ℕ) (body : Core.Assignment E → Prop) (g : Core.Assignment E) : trueAt (staticExists x body) g ↔ trueAt (dynamicExists x body) g

Static and dynamic agree on truth conditions (§4, §7).

def Semantics.Dynamic.Charlow2019.reachable {E : Type u_1} (g h : Core.Assignment E) : Prop

Reachable: h is reachable from g via some DPL formula (Charlow's (24)).

Equations

• Semantics.Dynamic.Charlow2019.reachable g h = ∃ (φ : Semantics.Dynamic.DPL.DPLRel E), φ g h

theorem Semantics.Dynamic.Charlow2019.reachable_refl {E : Type u_1} (g : Core.Assignment E) : reachable g g

Reachability is reflexive.

theorem Semantics.Dynamic.Charlow2019.reachable_trans {E : Type u_1} {g h k : Core.Assignment E} (hgh : reachable g h) (hhk : reachable h k) : reachable g k

Reachability is transitive (via dynamic conjunction).

theorem Semantics.Dynamic.Charlow2019.antisymmetry_fails {E : Type u_1} [Nontrivial E] : ∃ (g : Core.Assignment E), ∃ (h : Core.Assignment E), g ≠ h ∧ reachable g h ∧ reachable h g

Antisymmetry fails: distinct assignments can be mutually reachable (§8).

def Semantics.Dynamic.Charlow2019.stateNeg {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.StateCCP W E

Non-distributive negation (28): removes from s points that survive φ.

Equations

• Semantics.Dynamic.Charlow2019.stateNeg φ s = {i : W × Core.Assignment E | i ∈ s ∧ ¬i ∈ φ s}

def Semantics.Dynamic.Charlow2019.stateDistNeg {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.StateCCP W E

Distributive negation (29): tests each point individually.

Equations

• Semantics.Dynamic.Charlow2019.stateDistNeg φ s = {i : W × Core.Assignment E | i ∈ s ∧ φ {i} = ∅}

def Semantics.Dynamic.Charlow2019.partByAssignment {W : Type u_1} {E : Type u_2} (s : Core.State W E) : Set (Core.State W E)

Partition by assignment: groups points sharing the same assignment (Charlow's (35)).

Equations

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

def Semantics.Dynamic.Charlow2019.anaphoricallyDistributive {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Prop

Anaphorically distributive: processes each assignment-group separately (Charlow's (39)).

Equations

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

theorem Semantics.Dynamic.Charlow2019.distributive_implies_anaphoric {W : Type u_1} {E : Type u_2} (φ : Core.StateCCP W E) : Core.IsDistributive φ → anaphoricallyDistributive φ

Every distributive meaning is anaphorically distributive.