Reference · DeepSeek Harness and Cordis

The Mathematical Map

Definitions from Lesson 01

Notation

SymbolMeaning
ΓSpace or type of runtime contexts
γ : ΓOne concrete context state
δ : ΓReturned context state for one effect application
f : Γ → ΓContext transformation
g : Γ → ΓReturned recovery-function candidate; for the application below, g(δ) = γ
EΓΓ → (Γ × (Γ → Γ)), the raw shape of a revertible-effect candidate
Σ(k : K) ⇀ V(k), the type of finite typed partial dependency environments
V(k)Type of the value stored at dependency key k
⇀Typed partial function; a binding may be absent
σ : ΣOne concrete dependency environment
KSet of dependency keys
k ∈ KOne dependency key
×Product/pair type constructor
dom(σ)Keys that have values in σ
σ′Environment snapshot after an update
d ⊆ KDeclared dependency-key specification
σ ⊧ dEvery key in d is present in σ
∂ΓΓ × (Γ → Γ), context plus recovery accumulator
φ : Γ → ΓAccumulated recovery function

Core equations

idΓ : Γ → Γ is the identity function, so idΓ(γ) = γ. In the effect application, e(γ) = (δ, g) and the additional local witness is g(δ) = γ. The symbols ∀, ∧, and ̸⊧ mean "for every," "and," and "does not satisfy," respectively. The effect equations use context states in Γ. The dependency classifier separately compares environment snapshots σ, σ′ : Σ; conceptually an update u : Σ → Σ produces u(σ) = σ′. Do not assume Γ = Σ unless a model explicitly says so.

EΓ = Γ → (Γ × (Γ → Γ)) raw application shape: e : EΓ γ : Γ e(γ) = (δ, g) additional recovery obligation for this application: g(δ) = γ ∂Γ = Γ × (Γ → Γ) track(f, g)(γ, φ) = (f(γ), φ ∘ g) recover(γ, φ) = (φ(γ), idΓ) (f₁, g₁) ∘ (f₂, g₂) = (f₁ ∘ f₂, g₂ ∘ g₁) σ ⊧ d iff ∀k ∈ d, k ∈ dom(σ) activating iff σ ̸⊧ d ∧ σ′ ⊧ d deactivating iff σ ⊧ d ∧ σ′ ̸⊧ d neutral otherwise

The recovery guarantee applies to the tracked sequence under its local witness laws. Unrelated interleaving or out-of-order removal requires separate independence assumptions.

Reading order

  1. Identify the state space Γ.
  2. Identify the forward transformation f.
  3. Identify the inverse g and test g(δ) = γ for the particular application e(γ) = (δ, g).
  4. Remember that f ∘ g runs g first, then f. If execution is f₁ then f₂, write f₂ ∘ f₁.
  5. Compose recovery functions in the order needed to undo the later change first.
  6. For dependencies, write the specification d and evaluate σ ⊧ d.
  7. Classify the change as activating, deactivating, or neutral.

Primary source

A Programming Paradigm for Spatiotemporal Composability, especially Sections 3.1 and 3.2.