Causal Horizons and Why-Not
Status: architectural plan. Cursor parentage, leased dataspaces, checkpoints, effects, and receipts exist in experimental form. Horizon-indexed logic and why-not explanations do not yet.
A Cursors world does not have one authoritative wall-clock “now.” It has evidence accumulated along partially ordered execution histories, live leases observed by particular bodies, and local projections chosen by a Self or curve.
A causal horizon is a named frontier of that evidence.
It is not:
- a synchronized clock;
- global consensus;
- the newest fact in the universe;
- proof that every predecessor is still materially available;
- a promise that every observer has the same view.
It is the smallest explicit answer to:
“From this curve, using these accepted roots and this frontier of cursor heads, which facts and derivations are in scope?”
Horizon shape
A scalar sequence number is insufficient because two cursor branches may be concurrent. A horizon is therefore a finite set or antichain of cursor heads plus a curve and evidence policy:
causal_horizon H
curve: family-room
heads:
cursor:cedar/91
cursor:mirror/44
accepted roots:
self:local
invitation:family-room/v3
evidence policy:
verified cursor ancestry
live leased assertions observed by this body
receipts accepted under named effect domains
The durable snapshot contains the accepted ancestor closure of the heads. Live assertions, material availability, routes, leases, and policy observations should be projected alongside that durable closure rather than silently folded into it.
Suggested SQLite projection
CREATE TABLE causal_horizons (
horizon_id TEXT PRIMARY KEY,
curve_id TEXT NOT NULL,
generation INTEGER NOT NULL,
observed_at INTEGER,
evidence_policy_root BLOB NOT NULL,
status TEXT NOT NULL
);
CREATE TABLE causal_horizon_heads (
horizon_id TEXT NOT NULL,
cursor_id TEXT NOT NULL,
PRIMARY KEY (horizon_id, cursor_id)
);
CREATE TABLE cursor_parent_edges (
child_cursor TEXT NOT NULL,
parent_cursor TEXT NOT NULL,
PRIMARY KEY (child_cursor, parent_cursor)
);
CREATE TABLE horizon_evidence (
horizon_id TEXT NOT NULL,
evidence_id TEXT NOT NULL,
evidence_class TEXT NOT NULL,
subject_id TEXT NOT NULL,
observed_by TEXT,
lease_until INTEGER,
PRIMARY KEY (horizon_id, evidence_id)
);
The ancestor closure may be materialized for hot horizons, computed through recursive SQL for bounded work, or maintained incrementally. The canonical cursor records remain the authority for ancestry; SQLite projections are rebuildable.
Dedalus: time and location as logic
Dedalus is a Datalog-like language for distributed systems that makes time explicit. Its rules are commonly explained in three groups:
- Deductive rules: derive facts at the same logical time.
- Inductive rules: persist or produce facts at the next logical time.
- Asynchronous rules: send facts to another location for delivery at some later logical time.
Cursors should borrow this division without copying a single global integer clock.
Deductive: within one selected horizon
candidate_resume(Cursor, Body, H) :-
checkpoint(Cursor, State, H),
body_available(Body, H),
supports(Body, State, H).
No cursor advances merely because this relation was derived.
Inductive: a successor cursor or local generation
still_interested(Facet, Pattern, H1) :-
interest(Facet, Pattern, Lease, H0),
successor_horizon(H0, H1),
lease_live(Lease, H1).
Persistence is explicit. Leases do not become timeless facts.
Asynchronous: an envelope separates send from receive
envelope_offer(Message, Destination, Hsend) :-
outbox_intent(Message, Destination, Hsend).
mailbox_admitted(Message, Destination, Hrecv) :-
envelope_offer(Message, Destination, Hsend),
admitted_delivery(Message, Destination, Hsend, Hrecv).
The send horizon and admitted receive horizon remain visible. Transport delivery is not execution, and either event may be absent from one observer’s horizon.
One horizon, several projections
The useful model is one durable causal frontier with typed projections:
causal horizon H
|
+-----------------+------------------+
| | |
v v v
cursor ancestry authority policy effect receipts
| | |
v v v
material availability live leases routes/carriers
These views answer different questions:
- Ancestry: Which cursor records are accepted predecessors?
- Authority: Which trust roots, grants, caveats, and presentations are accepted for this decision?
- Availability: Which referenced bytes are currently resolvable, from where, and with what integrity evidence?
- Live coordination: Which assertions and interests have unexpired observed leases?
- Effects: Which intents, submissions, observations, and receipts are accepted?
- Transport: Which carriers were observed, and what did those observations prove?
Do not produce one “complete” gauge by averaging unrelated evidence classes. A fully verified cursor whose checkpoint bytes are unavailable is causally known but not presently resumable.
Causal cone
Selecting a cursor, effect, assertion, capability, route, or derived logic fact should expose a cone with three regions.
Upstream
- cursor parents and state roots;
- messages, assertions, or interests that enabled the continuation;
- grants and caveats required for authorization;
- storage and resolution evidence;
- earlier receipts used for duplicate suppression.
Lateral
- events that may be concurrent;
- other eligible bodies;
- alternative carriers or stores;
- alternative derivations;
- conflicting signed claims;
- branches excluded by the selected curve.
Downstream
- successor cursors;
- derived assertions;
- outgoing envelopes;
- effect intents, submissions, and receipts;
- replicated material;
- later joins, compensations, revocations, and tombstones.
Every edge needs an evidence class:
| Edge class | Claim |
|---|---|
required-cause |
This derivation or transition requires the predecessor under the selected model. |
observed-predecessor |
The event is linked and earlier, but necessity was not established. |
possible-concurrency |
Neither side is known to precede the other. |
alternative-proof |
Another derivation establishes the same result. |
correlation |
The events are nearby in time or topology only. |
counterfactual-dependency |
A recorded simulation changed the result when this input was removed. |
unknown |
Evidence is missing or the observation boundary cannot decide. |
Why did this happen?
A why query starts from an observed or derived subject and follows accepted derivation and transition edges upstream.
WHY DID MIRROR RESUME CURSOR 83?
successor cursor 84
because execution receipt r84 was admitted
because Mirror held execution lease l12
because capability presentation p7 allowed resume
because checkpoint state-a91 was hash-verified locally
because cursor 83 named continuation profile v0
because parents 77 and 81 were accepted in horizon H
This should be a navigable proof graph. A natural-language summary may be generated from that graph, but it must not replace the evidence.
Why did this not happen?
A why-not query needs four inputs:
- the expected goal;
- the selected causal horizon;
- the curve and authority policy;
- a completeness policy for every relation whose absence matters.
Example:
WHY DID CURSOR 83 NOT RESUME ON EMBER?
established:
checkpoint(cursor-83, state-a91)
supports(Ember, continuation-v0)
failed:
body lease expired at Ember-local generation 190
execution capability presentation targeted Mirror, not Ember
unknown:
no complete remote availability view exists for Ember at H
conclusion:
resume was not authorized at this horizon;
remote material availability remains unknown
The engine must distinguish:
- failed prerequisite: a known condition evaluated false;
- missing closed-world fact: the relation is complete for this horizon and contains no match;
- expired evidence: a lease or policy record is no longer live;
- excluded evidence: the curve or trust policy intentionally hides or rejects it;
- unavailable material: a referenced object is known but cannot currently be resolved;
- open-world unknown: absence cannot establish falsity;
- budget/cancellation: the explanation search did not finish.
Relation completeness policies
Every relation used under negation needs an explicit policy:
| Policy | Meaning |
|---|---|
open |
Missing means “not established here.” |
closed-at-horizon |
The relation is complete for this bounded snapshot. |
leased-live |
The body has a complete local view of currently live leases it admitted. |
derived-closed |
A terminating bounded program derived the complete relation. |
authority-closed |
The named accepted roots and policy records form the complete authority set for this decision. |
Negation should be stratified and admitted only over a relation that is closed under one of these policies. Otherwise not p(x) is represented as an unresolved anti-goal, not a fact.
Counterfactual worlds
A counterfactual is a separate experimental horizon derived from a real snapshot plus explicit interventions:
canonical horizon H
|
+-- simulated horizon H'
remove body_available(Mirror)
expire grant g7
delay receipt r84
partition local-store
The simulation may answer:
- Which successors disappear?
- Which carrier plan is selected instead?
- Does a duplicate effect become possible?
- Which invariant fails first?
- Which facts remain derivable through alternatives?
A simulated edge must never be styled as observed history. Model-checker counterexamples, Oddity-like execution branches, and operator-created experiments can all use this same representation.
Cockpit lens
The horizon lens should expose:
HORIZON
heads / curve / roots / generation
CAUSAL CONE
upstream / concurrent / downstream
WHY
selected derivation and alternatives
WHY NOT
failed, missing, expired, excluded, unavailable, unknown
COUNTERFACTUAL
interventions and changed consequences
Clicking any proof step focuses the actual cursor, grant, assertion, body, store, message, or receipt. Returning to the guide should preserve the exact heading and selected horizon.
Smallest executable experiment
Use the SQLite + Lua watch-party demo:
- Create a horizon before a playback assertion.
- Show that the waiting continuation is not resumable and explain the absent matching assertion as
leased-livewithin the local body. - Commit a matching leased assertion.
- Create a successor horizon and show the derivation that wakes the continuation.
- Expire the assertion and create another horizon.
- Show that the old durable cursor ancestry remains while the live coordination fact disappears.
- Add a simulated partition and show a distinct counterfactual branch.
Acceptance criteria
- Horizons can contain several concurrent heads.
- Durable cursor ancestry, live leases, availability, authority, transport, and receipts remain separate projections.
- Every why answer links to concrete evidence IDs.
- Every why-not answer names its horizon and completeness assumptions.
- Open-world absence is never reported as global falsity.
- Counterfactual and model traces are unmistakably separate from observed history.
- A body can rebuild horizon projections from canonical cursor records plus accepted observations.
- Queries are bounded by heads, ancestry depth, rows, proof alternatives, and wall time.
Research lineage
- Dedalus: Datalog in Time and Space
- The CALM principle
- ShiViz
- Whyline
- Causeway
- Oddity
- Pivot Tracing
- Provenance Semirings