Dynamic Ty2 is parameterized by:

• S: The type of "assignments" (info states as atomic entities)
• E: The type of individuals

This follows Muskens's insight: instead of assignments being functions, they are atomic, and drefs are functions FROM assignments.

@[reducible, inline]

abbrev Semantics.Dynamic.Core.DynamicTy2.Dref (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Discourse referent for individuals: type se in Dynamic Ty2

Equations

• Semantics.Dynamic.Core.DynamicTy2.Dref S E = (S → E)

class Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure (S : Type u_1) (E : Type u_2) : Type (max u_1 u_2)

Random assignment axiom structure.

In Dynamic Ty2, we need axioms ensuring S behaves like assignments. This structure captures the "Enough Assignments" axiom:

∀i ∀u ∀f. udref(u) → ∃j. i[u]j ∧ uj = f

We model this via an extend operation.

• extend : S → (S → E) → E → S

  Extend assignment i at dref u to value e, giving j

• extend_at (i : S) (u : S → E) (e : E) : u (extend i u e) = e

  The extended assignment has the new value at u

• extend_other (i : S) (u v : S → E) (e : E) : u ≠ v → v (extend i u e) = v i

  The extended assignment agrees elsewhere

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.randomAssign {S : Type u_1} {E : Type u_2} [AssignmentStructure S E] (u : S → E) : DRS S

Random assignment DRS: [u] introduces dref u

Equations

• [u]ᵈʳᵉᶠ i j = ∃ (e : E), j = Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.extend i u e

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.«term[_]ᵈʳᵉᶠ» : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.dexists {S : Type u_1} {E : Type u_2} [AssignmentStructure S E] (u : S → E) (D : DRS S) : DRS S

Existential DRS: ∃u(D) = [u]; D

Equations

• ∃'u(D) = [u]ᵈʳᵉᶠ ⨟ D

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.«term∃'_(_)» : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.dforall {S : Type u_1} {E : Type u_2} [AssignmentStructure S E] (u : S → E) (D : DRS S) : Condition S

Universal condition: ∀u(D) = ~∃u(~D)

Equations

• ∀'u(D) = ∼∃'u([∼D])

def Semantics.Dynamic.Core.DynamicTy2.AssignmentStructure.«term∀'_(_)» : Lean.ParserDescr

Equations

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

def Semantics.Dynamic.Core.DynamicTy2.atom1 {S : Type u_1} {E : Type u_2} (P : E → Prop) (u : Dref S E) : Condition S

Atomic condition from a predicate and drefs

Equations

• Semantics.Dynamic.Core.DynamicTy2.atom1 P u i = P (u i)

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

Equations

• Semantics.Dynamic.Core.DynamicTy2.atom2 P u v i = P (u i) (v i)

def Semantics.Dynamic.Core.DynamicTy2.atom3 {S : Type u_1} {E : Type u_2} (P : E → E → E → Prop) (u v w : Dref S E) : Condition S

Equations

• Semantics.Dynamic.Core.DynamicTy2.atom3 P u v w i = P (u i) (v i) (w i)

def Semantics.Dynamic.Core.DynamicTy2.eq' {S : Type u_1} {E : Type u_2} (u v : Dref S E) : Condition S

Equality condition

Equations

• Semantics.Dynamic.Core.DynamicTy2.eq' u v i = (u i = v i)

Translating DPL into Dynamic Ty2

DPL variables xₙ become drefs uₙ : S → E (projection functions).

DPL	Dynamic Ty2
R(x₁,...,xₙ)	[λi. R(u₁i,...,uₙi)]
x₁ = x₂	[λi. u₁i = u₂i]
φ; ψ	TR(φ) ⨟ TR(ψ)
~φ	[∼TR(φ)]
[x]	[uₓ] (random assignment)

DPL's assignment functions g : Var → E become "flipped" to drefs u : S → E, where S plays the role of the assignment itself.

def Semantics.Dynamic.Core.DynamicTy2.specificDref {S : Type u_1} {E : Type u_2} (e : E) : Dref S E

Specific dref: constant function (for proper names).

John := λi. john

A proper name denotes the same individual regardless of assignment.

Equations

• Semantics.Dynamic.Core.DynamicTy2.specificDref e x✝ = e

def Semantics.Dynamic.Core.DynamicTy2.properName {S : Type u_1} {E : Type u_2} [AssignmentStructure S E] (u : S → E) (e : E) : DRS S

Proper name introduction (indefinite-like analysis).

Johnu ↝ [u | u = John]

This introduces an unspecific dref constrained to equal the specific one.

Equations

• Semantics.Dynamic.Core.DynamicTy2.properName u e = ∃'u([Semantics.Dynamic.Core.DynamicTy2.eq' u (Semantics.Dynamic.Core.DynamicTy2.specificDref e)])

Axioms AX2–AX4: Variable vs Constant Registers

@cite{muskens-1996} p. 156

AX1 is captured by AssignmentStructure.extend above. The remaining axioms:

• AX2 (VAR(u)): classifies registers as variable (unspecific) or constant (specific). In the formalization, variable drefs are arbitrary S → E functions; constant drefs are specificDref e = λ _ => e.

• AX3 (uₙ ≠ uₘ): distinct variable registers are distinct as functions. This is ensured by extend_other: updating one dref preserves others.

• AX4 (∀i v(Tom)(i) = tom): constant registers return the same value in all states. This is specificDref_constant below.

theorem Semantics.Dynamic.Core.DynamicTy2.specificDref_constant {S : Type u_1} {E : Type u_2} (e : E) (i j : S) : specificDref e i = specificDref e j

AX4: Specific (constant) drefs return the same value regardless of state.

theorem Semantics.Dynamic.Core.DynamicTy2.specificDref_extend_invariant {S : Type u_1} {E : Type u_2} [AssignmentStructure S E] (e : E) (u : S → E) (d : E) (i : S) (h : specificDref e ≠ u) : specificDref e (AssignmentStructure.extend i u d) = e

Specific drefs are invariant under extend (consequence of AX1 + AX4).