Compositional DRT — registers, drefs, and boxes

[Mus96]

The substrate of Muskens' Logic of Change: states are atomic (his type s), discourse referents are functions from states (Dref S E, his type se), and boxes are the relational algebra of Update.lean at the state type.

RegisterStructure R S E renders his register axioms: a carrier R of registers (his type π) with a value function val (his V) and register-wise update — AX1 ("having enough states"), skolemized as extend, with the update relation i[r]j guarded by register distinctness (his AX3 keeps distinct referents in distinct registers). Constant registers (AX4's names) are constant Drefs, not members of R — the VAR split of AX2. The canonical model instantiates registers as coordinates of a function type: RegisterStructure V (V → E) E.

Main definitions

• Dref S E: discourse referents, Muskens' type se.
• RegisterStructure with randomAssign, dexists, dforall, and the canonical instance at V → E.
• atom1, atom2, eq': atomic conditions from predicates and drefs.
• CDRT.State, CDRT.DProp, CDRT.SProp and the box connectives: the concrete CDRT instance at State E := Core.Assignment E, with DProp.new n agreeing with the register structure's random assignment (DProp.new_eq_randomAssign).

The compositional fragment (T₀ translations, generalized coordination, the paper's derivations) and the weakest-precondition calculus live in Studies/Muskens1996.lean.

@[reducible, inline]

abbrev DynamicSemantics.Dref (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Discourse referent (Muskens' type se): a function from states to individuals. Constant drefs (Function.const, AX4's names) are drefs but not registers.

Equations

• DynamicSemantics.Dref S E = (S → E)

class DynamicSemantics.RegisterStructure (R : Type u_1) (S : Type u_2) (E : outParam (Type u_3)) : Type (max (max u_1 u_2) u_3)

Muskens' register structure: a carrier of registers (his type π) with a value function (his V) and register-wise update. extend skolemizes AX1 — for each state, register, and individual there is a state that differs at most there — and the second law confines the difference to the updated register.

• val : R → S → E

  The value of a register in a state (Muskens' V).

• extend : S → R → E → S

  Update a state at a register (AX1's witness).

• val_extend_self (i : S) (r : R) (e : E) : val r (extend i r e) = e

  The updated register holds the new value.

• val_extend_of_ne (i : S) (r r' : R) (e : E) : r' ≠ r → val r' (extend i r e) = val r' i

  Other registers are untouched.

@[implicit_reducible]

instance DynamicSemantics.instRegisterStructureForallOfDecidableEq {V : Type u_1} {E : Type u_2} [DecidableEq V] : RegisterStructure V (V → E) E

The canonical register structure: registers are the coordinates of a function type, update is Function.update.

Equations

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

def DynamicSemantics.RegisterStructure.randomAssign {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) : Update S

Random assignment: [r] introduces the register r with an arbitrary value.

Equations

• DynamicSemantics.RegisterStructure.randomAssign r i j = ∃ (e : E), j = DynamicSemantics.RegisterStructure.extend i r e

def DynamicSemantics.RegisterStructure.dexists {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (D : Update S) : Update S

Existential update: ∃r(D) = [r]; D.

Equations

• DynamicSemantics.RegisterStructure.dexists r D = (DynamicSemantics.RegisterStructure.randomAssign r).seq D

def DynamicSemantics.RegisterStructure.dforall {R : Type u_1} {S : Type u_2} {E : Type u_3} [RegisterStructure R S E] (r : R) (D : Update S) : Condition S

Universal condition: ∀r(D) = ¬∃r(¬D).

Equations

• DynamicSemantics.RegisterStructure.dforall r D = (DynamicSemantics.RegisterStructure.dexists r (DynamicSemantics.Update.test D.neg)).neg

def DynamicSemantics.atom1 {S : Type u_1} {E : Type u_2} (P : E → Prop) (u : Dref S E) : Condition S

Atomic condition from a one-place predicate and a dref.

Equations

• DynamicSemantics.atom1 P u i = P (u i)

def DynamicSemantics.atom2 {S : Type u_1} {E : Type u_2} (P : E → E → Prop) (u v : Dref S E) : Condition S

Atomic condition from a two-place predicate and two drefs.

Equations

• DynamicSemantics.atom2 P u v i = P (u i) (v i)

def DynamicSemantics.eq' {S : Type u_1} {E : Type u_2} (u v : Dref S E) : Condition S

Equality condition on two drefs.

Equations

• DynamicSemantics.eq' u v i = (u i = v i)

@[reducible, inline]

abbrev CDRT.State (E : Type u_1) : Type u_1

CDRT state: Muskens' type s, concretely an assignment Nat → E. His registers are register indices n : ℕ with values read by dref (see the canonical RegisterStructure instance).

Equations

• CDRT.State E = Core.Assignment E

def CDRT.dref {E : Type u_1} (n : ℕ) : DynamicSemantics.Dref (State E) E

Register lookup as a dref: Muskens' type se, picking out the value stored at position n.

Equations

• CDRT.dref n r = r n

@[reducible, inline]

abbrev CDRT.DProp (E : Type u_1) : Type u_1

Dynamic proposition (box, type s(st)): the relational Update specialized to CDRT states.

Equations

• CDRT.DProp E = DynamicSemantics.Update (CDRT.State E)

@[reducible, inline]

abbrev CDRT.SProp (E : Type u_1) : Type u_1

Static proposition: the spine's Condition at CDRT states.

Equations

• CDRT.SProp E = DynamicSemantics.Condition (CDRT.State E)

@[reducible, inline]

abbrev CDRT.DProp.ofStatic {E : Type u_1} (p : SProp E) : DProp E

Embed a static proposition as a dynamic one: the spine's test.

Equations

• CDRT.DProp.ofStatic p = DynamicSemantics.Update.test p

@[reducible, inline]

abbrev CDRT.DProp.seq {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic conjunction: the spine's relational composition seq.

Equations

• φ.seq ψ = DynamicSemantics.Update.seq φ ψ

def CDRT.DProp.new {E : Type u_1} (n : ℕ) : DProp E

New discourse referent: [new n] extends the state at position n with an arbitrary value.

Equations

• CDRT.DProp.new n i o = ∃ (e : E), o = fun (m : ℕ) => if m = n then e else i m

theorem CDRT.DProp.new_eq_randomAssign {E : Type u_1} (n : ℕ) : new n = DynamicSemantics.RegisterStructure.randomAssign n

DProp.new is the register structure's random assignment at the canonical instance.

@[reducible, inline]

abbrev CDRT.DProp.neg {E : Type u_1} (φ : DProp E) : DProp E

Dynamic negation: the spine's neg, re-entering the update algebra via test.

Equations

• φ.neg = DynamicSemantics.Update.test (DynamicSemantics.Update.neg φ)

@[reducible, inline]

abbrev CDRT.DProp.impl {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic implication: the spine's impl via test.

Equations

• φ.impl ψ = DynamicSemantics.Update.test (DynamicSemantics.Update.impl φ ψ)

@[reducible, inline]

abbrev CDRT.DProp.disj {E : Type u_1} (φ ψ : DProp E) : DProp E

Dynamic disjunction as a test (SEM2, [Mus96] p. 148): the spine's disj via test.

Equations

• φ.disj ψ = DynamicSemantics.Update.test (DynamicSemantics.Update.disj φ ψ)

@[reducible, inline]

abbrev CDRT.DProp.true_at {E : Type u_1} (φ : DProp E) (i : State E) : Prop

Truth at a state: the spine's closure.

Equations

• φ.true_at i = DynamicSemantics.Update.closure φ i

Reduction lemmas

theorem CDRT.DProp.neg_output {E : Type u_1} {φ : DProp E} {i o : State E} (h : φ.neg i o) : o = i

The output of a negated DProp always equals the input state.

theorem CDRT.DProp.impl_true_at {E : Type u_1} (φ ψ : DProp E) (i : State E) : (φ.impl ψ).true_at i ↔ ∀ (k : State E), φ i k → ψ.true_at k

DProp.impl is true at i iff every antecedent extension satisfies the consequent.

theorem CDRT.DProp.ofStatic_true_at {E : Type u_1} (p : SProp E) (i : State E) : (ofStatic p).true_at i ↔ p i

A static DProp is true at i iff its static content holds.