Lesson 01 · DeepSeek Harness and Cordis

The Mathematical Map

Contexts, transformations, inverses, and dependency predicates

Your tangible win

By the end of this lesson, you should be able to explain the first formal model in plain language and connect every symbol to a concrete value and function call.

EΓ = Γ → (Γ × (Γ → Γ))

What does × mean here?

× is the product, or pair, type constructor. A × B means a pair whose first component has type A and whose second component has type B. It is the same idea Lesson 00 wrote as (A, B); it does not mean multiplication.

You will also be able to explain why a reversible effect is one local building block for a component that can be unloaded, and why safe unloading additionally needs tracking, ordering, dependency lifecycle rules, and assumptions about what "restored" means. The companion coeffect predicate gives one way to describe when a component's requirements are satisfied.

How to use this course

Complete Lesson 00: Values, Types, and Function Calls first if formal notation is new. The source paper is optional background; this course will teach every prerequisite and restate every definition we need.

First: what problem is being formalized?

DeepSeek Harness presents the agent as a composition of replaceable capabilities: models, tools, skills, sessions, sandboxes, storage, loops, scheduling, and UI. Its Cordis kernel manages mounting, unmounting, and dependencies. The official overview calls this "everything is a plugin." The architecture documentation makes the same idea concrete: plugins contribute services, typed events, and reversible effects to a shared context, and the agent loop itself is a plugin. [Harness architecture]

The paper asks what semantics such a system needs if components can arrive and depart while the process continues running. It splits the problem into two dimensions:

Two axes: temporal — component arrives, install effects, component departs, recover effects — and spatial — dependencies absent, providers appear or withdraw, re-evaluate satisfaction

Figure 1: The two axes. A component must be reversible over time and correctly situated among its dependencies. [D2 source]

The paper's title, A Programming Paradigm for Spatiotemporal Composability, names exactly this combination. The paper is an actively revised preprint, so exact theorem numbering may change in later versions. [Cordis paper repository]

1. A context is a state space

Let Γ be a set of possible runtime contexts. The Greek letter is not magic. It simply names the space of states the component can observe or modify.

For a toy example, let the context be a set of registered capabilities:

Γ = Set(String) γ₀ = ∅ γ₁ = {"model"} γ₂ = {"model", "tools"}

Here ∅ is the same empty set as the earlier toy value empty = {}.

Here, γ₀, γ₁, and γ₂ are individual context states. The uppercase Γ is the whole set of possible states. This distinction matters:

Γ means "the type or space of contexts."
γ means "one particular context value."
γ₀ usually means the state before a sequence of effects.

A context transformation is an ordinary function:

f : Γ → Γ

It consumes one state and returns another. If f registers a model:

f_model(γ) = γ ∪ {"model"}

Function composition is written f ∘ g. The paper uses the conventional mathematical direction in which the right function acts first:

(f ∘ g)(γ) = f(g(γ))

So f_model ∘ f_tools means: register tools first, then register the model.

Mental translation

When you see a function such as f : Γ → Γ, read it as "one possible way of changing the runtime context." Do not yet think about agents. This is ordinary state-transformer mathematics.

2. The reversible effect type

A normal state transformation tells us only what happens next. It does not tell us how to undo what happened. In this lesson, we model a reversible effect by returning a possible recovery function alongside the new state.

EΓ = Γ → (Γ × (Γ → Γ))

Pause: type versus actual run

This line is only a shape label. It does not show a current state yet.

TYPE / shape: effect : State → (State, Undo) VALUE: effect INPUT: empty ACTUAL RUN: effect(empty) = (has_model, remove_model)

In the paper's symbols, State is Γ, an actual state such as empty is γ, and Undo is Γ → Γ. Therefore:

TYPE: EΓ = Γ → (Γ × (Γ → Γ)) ACTUAL RUN: e(γ) = (δ, g)

So the current state γ is not missing. It belongs to the second line, where we actually call the effect. The first line only says what kind of function e is.

There is no type conversion here

It would be misleading to rewrite the type as e : Γ → (new_state, inverse_function). That is not a new type equation: new_state and inverse_function are names for returned values, not types.

The correct sequence is:

TYPE: e : Γ → (Γ × (Γ → Γ)) INPUT: x : Γ ACTUAL RUN: e(x) = (new_state, inverse_function) COMPONENT TYPES: new_state : Γ inverse_function : Γ → Γ

So we do not replace Γ × (Γ → Γ) with the names. We use the product type to say what types the two returned values must have, then we give those concrete returned values names after calling e.

An effect receives a current state γ : Γ.
It returns a pair (δ, g).
δ : Γ is the new state.
g : Γ → Γ is a returned function. It is called an inverse only when it satisfies an additional behavioral obligation for this execution.

The raw type e : EΓ guarantees only the return shape. It does not prove that the returned function actually restores anything. For a particular input, if:

e(γ) = (δ, g) g(δ) = γ

then this particular application has a witnessed, state-specific recovery function. The second equation is an additional obligation; it is not encoded by the raw type alone.

Two related inverse models

Keep these two constructions separate:

FIXED-PAIR MODEL: f : Γ → Γ g : Γ → Γ γ : Γ φ : Γ → Γ trackΓ(f, g)(γ, φ) = (f(γ), φ ∘ g)

Validity obligation for the fixed pair: g(f(γ)) = γ on the stated domain. If it must hold for every γ, write g ∘ f = idΓ.

RETURNED-EFFECT MODEL: e : Γ → (Γ × (Γ → Γ)) e(γ) = (δ, g_γ) g_γ(δ) = γ

In the fixed-pair model, one named g accompanies one named f. In the returned-effect model, the effect may return a different function g_γ for different inputs. Even there, the returned function is only constrained at the particular output δ unless a stronger universal law is separately proved.

Example: registering and unregistering a capability

Define the forward and recovery functions:

f_model(γ) = γ ∪ {"model"} g_model(δ) = δ \ {"model"}

Now consider one particular starting state where the model key is absent:

γ₀ = ∅ γ₁ = {"model"} f_model(γ₀) = γ₁ e_model(γ₀) = (γ₁, g_model) g_model(γ₁) = γ₀

This is one witnessed application. The raw function e_model(γ) = (f_model(γ), g_model) is total as an element of EΓ, because it returns a state and a function-shaped value for every γ. However, the witness equation g_model(f_model(γ)) = γ holds only when "model" ∉ γ. If the key was already present, blindly removing it could delete an older registration rather than restore the caller's exact state.

An implementation could retain g_model and invoke it when the corresponding registration is unloaded. That is an implementation pattern built on this abstraction, not a guarantee provided by the type alone.

A boundary, not a miracle

The code that applies or constructs the effect supplies the inverse or disposer. In a plugin system this is often component code, while Cordis tracks it when the registration uses its effect API. The runtime cannot generally prove that a user-written inverse restores the intended real-world state. If the effect sends an irreversible external message, deleting a local registration does not unsend that message.

3. Why inverse composition reverses order

Suppose a component performs two effects in sequence:

γ₀ --f₁--> γ₁ --f₂--> γ₂

To return to γ₀, we must apply g₂ first, then g₁:

γ₂ --g₂--> γ₁ --g₁--> γ₀

This is why the paper defines twisted composition of effect pairs as:

(f₁, g₁) ∘ (f₂, g₂) = (f₁ ∘ f₂, g₂ ∘ g₁)

The pair-composition operator uses the same right-to-left convention as ordinary function composition. Thus (f₁,g₁) ∘ (f₂,g₂) represents f₂ running first, followed by f₁. If the execution order is f₁ then f₂, write:

(f₂, g₂) ∘ (f₁, g₁) = (f₂ ∘ f₁, g₁ ∘ g₂)

The inverse functions therefore appear in the order needed for recovery: g₂ runs before g₁. The forward transformations and inverse transformations are not being read in the same chronological direction.

This behaves like a LIFO cleanup stack in the example below, but the formal accumulator is a composed function, not literally a stack data structure:

push undo(f₁) push undo(f₂) pop undo(f₂) pop undo(f₁)

4. The effect context and its accumulator

The paper reifies the cleanup stack as part of the state itself. Given a context Γ, define the effect context:

∂Γ = Γ × (Γ → Γ)

An element of ∂Γ is a pair:

(γ, φ)

γ is the current context.
φ is the accumulated recovery function.

The initial effect context is:

(γ₀, idΓ)

where idΓ(γ) = γ. Initially, there is nothing to undo.

Tracking an effect with a forward function f and an inverse g gives the following rule. Let φ : Γ → Γ be the accumulated recovery function, the second component of ∂Γ = Γ × (Γ → Γ). For γ : Γ:

trackΓ(f, g)(γ, φ) = (f(γ), φ ∘ g)

The state moves forward. The accumulator grows by composing the new inverse on the right. Given the paper's convention for composition, this means the newest inverse runs first when φ is later applied.

Worked calculation

Let "A" and "B" be distinct string keys. For a registry state S : Γ, define the installation functions and their candidate recoveries:

f_A(S) = S ∪ {"A"} g_A(S) = S \ {"A"} f_B(S) = S ∪ {"B"} g_B(S) = S \ {"B"}

Assume "A" and "B" are absent initially. Start with an empty registry and install "A", then "B":

state accumulator (∅, idΓ) ({"A"}, idΓ ∘ g_A) = ({"A"}, g_A) ({"A", "B"}, g_A ∘ g_B)

Now recover:

(g_A ∘ g_B)({"A", "B"}) = g_A(g_B({"A", "B"})) = g_A({"A"}) = ∅

The accumulator has turned two toy cleanup actions into one composed recovery function. This example does not yet establish the paper's general notion of effect independence; it only shows that these two set-removal functions commute in this toy model.

The recovery operation itself is:

recoverΓ(γ, φ) = (φ(γ), idΓ)

It applies the accumulated inverse to the current state and resets the accumulator. More precisely, if the sequence starts at (γ₀, idΓ), each application has the form eᵢ(γᵢ₋₁) = (γᵢ, gᵢ), and each witness satisfies gᵢ(γᵢ) = γᵢ₋₁, then recovery after the whole sequence returns (γ₀, idΓ) in this idealized model. This assumes the sequence contains only these effects and recovery is applied to the state they produced. Out-of-order removal or interleaving with other components requires separately stated independence conditions.

5. Coeffects: requirements on the environment

Effects describe what a component does. Coeffects describe what it needs.

Let:

K = the set of dependency keys V(k) = the type of value stored under key k Σ = (k : K) ⇀ V(k) σ : Σ = one concrete environment

Here Σ is the type/space of finite partial environments, and ⇀ means "partial function": an environment may lack a binding for some keys.

A partial environment may lack some keys. Formally, dom(σ) is the set of keys for which σ has a value, and:

dom(σ) ⊆ K k ∈ dom(σ) ⇒ σ(k) has type V(k)

The symbol ⇀, when used for a map, means "partial function": the map is not required to have an answer for every possible key. We can therefore think of σ as a typed lookup table:

σ("model") = one ModelProvider value σ("tools") = one ToolRegistry value σ("memory") = one MemoryStore value

A lookup such as get("model", σ) is defined only when "model" ∈ dom(σ). The values are omitted from the small domain diagrams below; in diagrams, bare labels such as model and tools abbreviate the corresponding string keys "model" and "tools". A displayed set such as {model, tools} abbreviates dom(σ) = {"model", "tools"}.

A component declares a specification d ⊆ K. A displayed set in an environment diagram, such as σ = {model, tools}, abbreviates dom(σ) = {"model", "tools"}. When the braces follow d =, they denote the dependency-key set itself. The classifier below is about this simplified presence-only model. The specification is satisfied exactly when every declared key is present:

σ ⊧ d iff for every k ∈ d, k ∈ dom(σ)

Read σ ⊧ d as "the environment state σ satisfies dependency specification d." Here ∀ means "for every," ∧ means "and," and σ ̸⊧ d means "σ does not satisfy d."

Notification classification

For this dependency-only classifier, take σ : Σ and σ′ : Σ as two environment snapshots. Let a separate environment update be u : Σ → Σ with u(σ) = σ′. Do not identify u with the earlier context transformation f : Γ → Γ unless the model explicitly defines Γ = Σ. The prime mark means "after the change," and σ ̸⊧ d means "σ does not satisfy d."

activating if σ ̸⊧ d and σ′ ⊧ d deactivating if σ ⊧ d and σ′ ̸⊧ d neutral otherwise

This is the mathematical seed of reactivity. In this simplified dependency-only model, the classifier reacts when the satisfaction truth value changes. It is not the complete Harness lifecycle rule: provider identity, target changes, lifecycle state, isolation, and other runtime conditions may matter even when σ ⊧ d remains true.

Transition chain: σ₀={} to σ₁={model} neutral; σ₁ to σ₂={model,tools} activating; σ₂ to σ₃={model,tools,memory} neutral; σ₃ to σ₄={model} deactivating

Figure 2: Activating, deactivating, and neutral classify transitions between environment snapshots. The snapshots themselves only have satisfaction values. [D2 source]

6. The bridge to the Harness

Use this running translation:

Formal object	Harness interpretation
`Γ`	Type or space of possible context states
`e : EΓ`	Abstract model of a capability installation returning a candidate recovery function; the type alone does not guarantee successful disposal
`φ`	Accumulated plugin cleanup
`k`	Service key such as model or tools
`σ`	Currently provided services
`d`	Component's declared dependencies
`σ ⊧ d`	All declared dependency keys are present; this is a prerequisite for activation

Later lessons will add the hard parts that are intentionally absent here: provider identity, observational equivalence, isolation, interception, fibers, asynchronous transition rules, and the theorems that lift local reasoning to an interleaved system.

Retrieval checkpoint

Try these without scrolling back. The buttons reveal model answers after you commit to an answer mentally.

1. What does e : EΓ return when applied to γ?

The raw type gives the result shape. For a witnessed application, e(γ) = (δ, g) and the additional recovery obligation is g(δ) = γ.

2. Why is the inverse order reversed?

Because if f₁ runs before f₂, then g₂ must remove the later change before g₁ can remove the earlier change.

3. Let d = {model, tools}. If σ contains only model, is the component active?

No. σ ̸⊧ d because tools is absent. Adding tools creates an activating transition.

4. What is the difference between Γ and γ?

Γ is the space or type of possible contexts. γ is one concrete context state inside that space.

Do not rush

If the type Γ → Γ × (Γ → Γ) is still visually dense, rewrite it in English: "given a state, return a new state and a function that undoes this application." That sentence is the definition. The symbols are compression, not additional magic.