Charlow (2025): Staged updates

This file formalizes the lifted interpretations of [Cha25]. A dynamic substrate whose negation is externally static, [GS91a]'s DPL, is lifted into a richer type by an embedding, a retraction and a negation obeying three laws, and the lifted interpretation they determine validates double-negation elimination and is conservative over the substrate (Facts 1 and 2). Every lawful lift of one substrate factors through a canonical form, a substrate value with a parity bit (Fact 4), which the canonical lift, an update tagged with one bit, realizes exactly (Fact 3). Over DPL the file gives four lifts: [KM95]'s pairs of an update and its negation, [Got19]'s decomposition into a static closure and a dynamic tautology, whose involution law holds only on the image of the lifted interpretation, the paper's staged updates, a static proposition beside a dynamic tautology, and the canonical lift.

Implementation notes

• The data of a lift and its laws are separate classes, after Monad and LawfulMonad, so the decomposed lift carries the data while its involution law is refuted on the whole carrier and proved on the image.
• Fact 4 is stated as factorization through the canonical form rather than as the paper's bijection between images; the corollary that lawful lifts lower alike follows from it.
• Fact 3 takes the paper's right identity for conjunction as a hypothesis.

References

• [Cha25]
• [GS91a]
• [KM95]
• [Got19]

Substrates, lifts and interpretations (Definitions 3 and 4)

class Charlow2025.Substrate (δ : Type u_1) : Type u_1

A dynamic substrate, the paper's δ: a carrier with conjunction and negation.

• conj : δ → δ → δ
• neg : δ → δ

inductive Charlow2025.Formula (Atom : Type u_1) : Type u_1

The language: atoms, bare existentials, conjunction and negation; ∃x φ abbreviates ∃x ∧ φ.

• atom {Atom : Type u_1} : Atom → Formula Atom
• exi {Atom : Type u_1} : ℕ → Formula Atom
• conj {Atom : Type u_1} : Formula Atom → Formula Atom → Formula Atom
• neg {Atom : Type u_1} : Formula Atom → Formula Atom

def Charlow2025.instReprFormula.repr {Atom✝ : Type u_1} [Repr Atom✝] : Formula Atom✝ → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance Charlow2025.instReprFormula {Atom✝ : Type u_1} [Repr Atom✝] : Repr (Formula Atom✝)

Equations

• Charlow2025.instReprFormula = { reprPrec := Charlow2025.instReprFormula.repr }

class Charlow2025.Lift (δ : outParam (Type u_1)) (Δ : Type u_2) [Substrate δ] : Type (max u_1 u_2)

The signatures of a lift of a substrate into Δ: up into the lifted type, down out of it, and the lifted negation.

• up : δ → Δ
• down : Δ → δ
• neg : Δ → Δ

class Charlow2025.LawfulLift (δ : outParam (Type u_1)) (Δ : Type u_2) [Substrate δ] [self : Lift δ Δ] : Prop

The laws of a lift: Emb, down ∘ up = id; Inv, the lifted negation is an involution; and Neg, conjugating the lifted negation by the lift recovers the substrate negation.

• down_up (m : δ) : Lift.down (Lift.up m) = m
• neg_neg (M : Δ) : Lift.neg (Lift.neg M) = M
• down_neg_up (m : δ) : Lift.down (Lift.neg (Lift.up m)) = Substrate.neg m

def Charlow2025.interp {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) : Formula Atom → δ

The substrate interpretation [·], from the primitive meanings of atoms and existentials.

Equations

• Charlow2025.interp ia ie (Charlow2025.Formula.atom a) = ia a
• Charlow2025.interp ia ie (Charlow2025.Formula.exi n) = ie n
• Charlow2025.interp ia ie (φ.conj ψ) = Charlow2025.Substrate.conj (Charlow2025.interp ia ie φ) (Charlow2025.interp ia ie ψ)
• Charlow2025.interp ia ie φ.neg = Charlow2025.Substrate.neg (Charlow2025.interp ia ie φ)

def Charlow2025.liftInterp {Atom : Type u_1} {δ : Type u_2} {Δ : Type u_3} [Substrate δ] [self : Lift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) : Formula Atom → Δ

The lifted interpretation ⟨·⟩: primitives lift, conjuncts lower, sequence and lift again, and negation is the lifted negation.

Equations

• One or more equations did not get rendered due to their size.
• Charlow2025.liftInterp ia ie (Charlow2025.Formula.atom a) = Charlow2025.Lift.up (ia a)
• Charlow2025.liftInterp ia ie (Charlow2025.Formula.exi n) = Charlow2025.Lift.up (ie n)
• Charlow2025.liftInterp ia ie φ.neg = Charlow2025.Lift.neg (Charlow2025.liftInterp ia ie φ)

Facts 1 and 2

theorem Charlow2025.liftInterp_neg_neg {Atom : Type u_1} {δ : Type u_2} {Δ : Type u_3} [Substrate δ] [self : Lift δ Δ] [LawfulLift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) (φ : Formula Atom) : liftInterp ia ie φ.neg.neg = liftInterp ia ie φ

Fact 1: a lawful lifted interpretation validates double-negation elimination.

inductive Charlow2025.NegFree {Atom : Type u_1} : Formula Atom → Prop

A formula without negation.

• atom {Atom : Type u_1} (a : Atom) : NegFree (Formula.atom a)
• exi {Atom : Type u_1} (n : ℕ) : NegFree (Formula.exi n)
• conj {Atom : Type u_1} {φ ψ : Formula Atom} : NegFree φ → NegFree ψ → NegFree (φ.conj ψ)

inductive Charlow2025.DoubleNegFree {Atom : Type u_1} : Formula Atom → Prop

A formula without a doubly negated subformula.

• atom {Atom : Type u_1} (a : Atom) : DoubleNegFree (Formula.atom a)
• exi {Atom : Type u_1} (n : ℕ) : DoubleNegFree (Formula.exi n)
• conj {Atom : Type u_1} {φ ψ : Formula Atom} : DoubleNegFree φ → DoubleNegFree ψ → DoubleNegFree (φ.conj ψ)
• neg_atom {Atom : Type u_1} (a : Atom) : DoubleNegFree (Formula.atom a).neg
• neg_exi {Atom : Type u_1} (n : ℕ) : DoubleNegFree (Formula.exi n).neg
• neg_conj {Atom : Type u_1} {φ ψ : Formula Atom} : DoubleNegFree φ → DoubleNegFree ψ → DoubleNegFree (φ.conj ψ).neg

theorem Charlow2025.liftInterp_eq_up_interp_of_negFree {Atom : Type u_1} {δ : Type u_2} {Δ : Type u_3} [Substrate δ] [self : Lift δ Δ] [LawfulLift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) {φ : Formula Atom} (h : NegFree φ) : liftInterp ia ie φ = Lift.up (interp ia ie φ)

Fact 2.i: a negation-free formula's lifted meaning is the lift of its substrate meaning.

theorem Charlow2025.down_liftInterp_eq_interp_of_doubleNegFree {Atom : Type u_1} {δ : Type u_2} {Δ : Type u_3} [Substrate δ] [self : Lift δ Δ] [LawfulLift δ Δ] (ia : Atom → δ) (ie : ℕ → δ) {φ : Formula Atom} (h : DoubleNegFree φ) : Lift.down (liftInterp ia ie φ) = interp ia ie φ

Fact 2.ii: a double-negation-free formula's lifted meaning lowers to its substrate meaning.

The canonical form and Fact 4

def Charlow2025.canonicalize {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) : Formula Atom → δ ⊕ δ

The canonical form of a formula's lifted meaning: a substrate value with a parity bit, Sum.inl for an even and Sum.inr for an odd number of residual negations; it depends on the substrate alone.

Equations

• One or more equations did not get rendered due to their size.
• Charlow2025.canonicalize ia ie (Charlow2025.Formula.atom a) = Sum.inl (ia a)
• Charlow2025.canonicalize ia ie (Charlow2025.Formula.exi n) = Sum.inl (ie n)
• Charlow2025.canonicalize ia ie φ.neg = (Charlow2025.canonicalize ia ie φ).swap

theorem Charlow2025.canonicalize_of_negFree {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) {φ : Formula Atom} (h : NegFree φ) : canonicalize ia ie φ = Sum.inl (interp ia ie φ)

A negation-free formula's canonical form is its substrate meaning, positive.

theorem Charlow2025.canonicalize_eq {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) (φ : Formula Atom) : ∃ (ψ : Formula Atom), canonicalize ia ie φ = Sum.inl (interp ia ie ψ) ∨ canonicalize ia ie φ = Sum.inr (interp ia ie ψ)

Every canonical form carries the substrate meaning of some formula.

def Charlow2025.encodeCanonical {δ : Type u_2} [Substrate δ] (Δ : Type u_3) [self : Lift δ Δ] : δ ⊕ δ → Δ

Encoding a canonical form into a lift: a positive value lifts, a negative one lifts and is negated.

Equations

• Charlow2025.encodeCanonical Δ (Sum.inl m) = Charlow2025.Lift.up m
• Charlow2025.encodeCanonical Δ (Sum.inr m) = Charlow2025.Lift.neg (Charlow2025.Lift.up m)

theorem Charlow2025.down_encodeCanonical {δ : Type u_2} [Substrate δ] (Δ : Type u_3) [self : Lift δ Δ] [LawfulLift δ Δ] (s : δ ⊕ δ) : Lift.down (encodeCanonical Δ s) = Sum.elim id Substrate.neg s

An encoded canonical form lowers to its value, negated when odd.

theorem Charlow2025.encodeCanonical_swap {δ : Type u_2} [Substrate δ] (Δ : Type u_3) [self : Lift δ Δ] [LawfulLift δ Δ] (s : δ ⊕ δ) : encodeCanonical Δ s.swap = Lift.neg (encodeCanonical Δ s)

Flipping the parity encodes as the lifted negation.

theorem Charlow2025.liftInterp_eq_encodeCanonical {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) (Δ : Type u_3) [self : Lift δ Δ] [LawfulLift δ Δ] (φ : Formula Atom) : liftInterp ia ie φ = encodeCanonical Δ (canonicalize ia ie φ)

Fact 4 as factorization: every lawful lifted interpretation is the encoding of the canonical form, which depends on the substrate alone.

theorem Charlow2025.liftInterp_eq_of_canonicalize_eq {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) (Δ : Type u_3) [self : Lift δ Δ] [LawfulLift δ Δ] {φ ψ : Formula Atom} (h : canonicalize ia ie φ = canonicalize ia ie ψ) : liftInterp ia ie φ = liftInterp ia ie ψ

Formulas with one canonical form are identified by every lawful lift.

theorem Charlow2025.down_liftInterp_eq_down_liftInterp {Atom : Type u_1} {δ : Type u_2} [Substrate δ] (ia : Atom → δ) (ie : ℕ → δ) (Δ : Type u_3) [self : Lift δ Δ] [LawfulLift δ Δ] (Δ' : Type u_4) [Lift δ Δ'] [LawfulLift δ Δ'] (φ : Formula Atom) : Lift.down (liftInterp ia ie φ) = Lift.down (liftInterp ia ie φ)

The corollary of Fact 4: two lawful lifts of one substrate lower every formula alike.

Program disjunction and truth (Definitions 2, 5 and 6)

class Charlow2025.ProgramDisj (δ : Type u_1) [Substrate δ] : Type u_1

A substrate with the union of two updates, the externally dynamic program disjunction.

• pdisj : δ → δ → δ

class Charlow2025.Truth (δ : Type u_1) (i : outParam (Type u_2)) [Substrate δ] : Type (max u_1 u_2)

A substrate whose meanings have propositional content over indices i, the indices where they succeed, and can be restricted to a proposition.

• truth : δ → i → Prop
• restrict : δ → (i → Prop) → δ

DPL as a substrate

@[instance_reducible]

instance Charlow2025.instSubstrateUpdateAssignment {E : Type u_1} : Substrate (DynamicSemantics.Update (Assignment E))

Equations

• Charlow2025.instSubstrateUpdateAssignment = { conj := SetRel.comp, neg := fun (φ : DynamicSemantics.Update (Assignment E)) => DynamicSemantics.Update.test φ.neg }

@[instance_reducible]

instance Charlow2025.instProgramDisjUpdateAssignment {E : Type u_1} : ProgramDisj (DynamicSemantics.Update (Assignment E))

Program disjunction on DPL relations is the union of the outputs.

Equations

• Charlow2025.instProgramDisjUpdateAssignment = { pdisj := fun (φ ψ : DynamicSemantics.Update (Assignment E)) => φ ∪ ψ }

@[instance_reducible]

instance Charlow2025.instTruthUpdateAssignmentForallNat {E : Type u_1} : Truth (DynamicSemantics.Update (Assignment E)) (ℕ → E)

Equations

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

Instance 1: two-dimensional DPL

[KM95]'s pairs of an update and its anti-extension, recast as a lift on the diagonal product δ ⊙ δ: up pairs an update with its substrate negation, down forgets the anti-extension, and the lifted negation is the product's swap ᶜ.

@[instance_reducible]

instance Charlow2025.instLiftProduct {δ : Type u_1} [Substrate δ] : Lift δ (Bilattice.Product δ δ)

Equations

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

instance Charlow2025.instLawfulLiftProduct {δ : Type u_1} [Substrate δ] : LawfulLift δ (Bilattice.Product δ δ)

Instance 2: decomposed updates

structure Charlow2025.Decomposed (δ : Type u_1) : Type u_1

[Got19]'s decomposition, recast as a lift: up pairs an update's static closure, its double negation, with the dynamic tautology m ∪ ¬m, down conjoins the two and the lifted negation negates the at-issue coordinate.

• atIssue : δ
• tautology : δ

@[instance_reducible]

instance Charlow2025.Decomposed.instLift {δ : Type u_1} [Substrate δ] [ProgramDisj δ] : Lift δ (Decomposed δ)

Equations

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

theorem Charlow2025.Decomposed.down_up {E : Type u_2} (m : DynamicSemantics.Update (Assignment E)) : Lift.down (Lift.up m) = m

Emb over DPL: conjoining the static closure with the dynamic tautology reconstitutes the update.

theorem Charlow2025.Decomposed.down_neg_up {E : Type u_2} (m : DynamicSemantics.Update (Assignment E)) : Lift.down (Lift.neg (Lift.up m)) = DynamicSemantics.Update.test m.neg

Neg over DPL.

theorem Charlow2025.Decomposed.not_neg_neg {E : Type u_2} [Nontrivial E] : ∃ (M : Decomposed (DynamicSemantics.Update (Assignment E))), Lift.neg (Lift.neg M) ≠ M

The hiccup with Inv: on the whole carrier the lifted negation is not an involution, since a bare existential is no test and its double negation is not itself.

theorem Charlow2025.Decomposed.exists_atIssue_eq_neg {E : Type u_2} {Atom : Type u_3} (ia : Atom → DynamicSemantics.Update (Assignment E)) (ie : ℕ → DynamicSemantics.Update (Assignment E)) (φ : Formula Atom) : ∃ (X : DynamicSemantics.Update (Assignment E)), (liftInterp ia ie φ).atIssue = DynamicSemantics.Update.test X.neg

On the image of the lifted interpretation the at-issue coordinate is a negation, hence static.

theorem Charlow2025.Decomposed.neg_neg_liftInterp {E : Type u_2} {Atom : Type u_3} (ia : Atom → DynamicSemantics.Update (Assignment E)) (ie : ℕ → DynamicSemantics.Update (Assignment E)) (φ : Formula Atom) : Lift.neg (Lift.neg (liftInterp ia ie φ)) = liftInterp ia ie φ

Inv on the image: the lifted negation is an involution on every lifted meaning, a static at-issue coordinate being restored by its double negation.

Instance 3: staged updates

structure Charlow2025.Staged (δ : Type u_1) (i : Type u_2) : Type (max u_1 u_2)

A staged update: the static proposition of an update beside the dynamic tautology m ∪ ¬m; down restricts the tautology to the proposition and the lifted negation complements the proposition.

• staticContent : i → Prop
• update : δ

@[instance_reducible]

instance Charlow2025.Staged.instLift {δ : Type u_1} {i : Type u_2} [Substrate δ] [ProgramDisj δ] [Truth δ i] : Lift δ (Staged δ i)

Equations

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

instance Charlow2025.Staged.instLawfulLiftUpdateAssignmentForallNat {E : Type u_3} : LawfulLift (DynamicSemantics.Update (Assignment E)) (Staged (DynamicSemantics.Update (Assignment E)) (ℕ → E))

Over DPL the staged lift obeys all three laws.

Instance 4: the canonical lift and Fact 3

structure Charlow2025.Canonical (δ : Type u_1) : Type u_1

The canonical lift: an update tagged with a bit that says whether to negate it on lowering; the lifted negation toggles the bit.

• flag : Bool
• update : δ

@[instance_reducible]

instance Charlow2025.Canonical.instLift {δ : Type u_1} [Substrate δ] : Lift δ (Canonical δ)

Equations

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

instance Charlow2025.Canonical.instLawfulLift {δ : Type u_1} [Substrate δ] : LawfulLift δ (Canonical δ)

theorem Charlow2025.Canonical.liftInterp_eq {δ : Type u_1} [Substrate δ] {Atom : Type u_2} (ia : Atom → δ) (ie : ℕ → δ) (φ : Formula Atom) : ∃ (b : Bool) (ψ : Formula Atom), liftInterp ia ie φ = { flag := b, update := interp ia ie ψ }

Fact 3, one inclusion: every lifted meaning is a tagged substrate meaning.

def Charlow2025.Canonical.guard {Atom : Type u_2} (one : Formula Atom) : Formula Atom → Formula Atom

The paper's φ̃: every negation conjoined with a right identity one, so that no double negation remains.

Equations

• Charlow2025.Canonical.guard one (Charlow2025.Formula.atom a) = Charlow2025.Formula.atom a
• Charlow2025.Canonical.guard one (Charlow2025.Formula.exi n) = Charlow2025.Formula.exi n
• Charlow2025.Canonical.guard one (φ.conj ψ) = (Charlow2025.Canonical.guard one φ).conj (Charlow2025.Canonical.guard one ψ)
• Charlow2025.Canonical.guard one φ.neg = (Charlow2025.Canonical.guard one φ).neg.conj one

theorem Charlow2025.Canonical.canonicalize_guard {δ : Type u_1} [Substrate δ] {Atom : Type u_2} (ia : Atom → δ) (ie : ℕ → δ) {one : Formula Atom} (hone : NegFree one) (hid : ∀ (m : δ), Substrate.conj m (interp ia ie one) = m) (φ : Formula Atom) : canonicalize ia ie (guard one φ) = Sum.inl (interp ia ie φ)

A guarded formula's canonical form is the formula's substrate meaning, positive.

theorem Charlow2025.Canonical.exists_liftInterp_eq {δ : Type u_1} [Substrate δ] {Atom : Type u_2} (ia : Atom → δ) (ie : ℕ → δ) {one : Formula Atom} (hone : NegFree one) (hid : ∀ (m : δ), Substrate.conj m (interp ia ie one) = m) (b : Bool) (ψ : Formula Atom) : ∃ (φ : Formula Atom), liftInterp ia ie φ = { flag := b, update := interp ia ie ψ }

Fact 3, the other inclusion: with a right identity for conjunction, every tagged substrate meaning is a lifted meaning, of the guarded formula or its negation.