§ 10 · draft · depth 0 · edit the source
Glossary
Every term used normatively elsewhere, defined once.
Ambient capabilities (δ) — the set of strata whose capabilities are currently held. Holds 0 and nothing else at the top level; added to only by descend, which adds the one it names. §2.1
Answer — what a function returns when the world is entitled to say no: either the value, or a refusal. Not an error type; a record of what was said. §5.1.1
Bury — to evaluate a program as far as the granted capabilities allow, producing a trace. The only form of evaluation in the language. §6.1
Cairn — the content address of a value: blake3 over its canonical encoding, under a versioned domain separator. Always at depth 0. §7.2
Capability — a named grant of access to one stratum of the world. Acquired by descend, lexically scoped, never ambient. §9.1
Collapse — what an expression does when it can never produce a value: must on a refusal, an out-of-range index. Not catchable, and a burial that hits one caves in. §9.9
Demand — a top-level statement naming an expression that must be evaluated. Nothing else is evaluated. There is no main. §6.2
Deposit — a value left in the trace by a bare-expression statement. Not printed; read afterwards with lamp. §4.7
Depth (d) — how far into the world a value's history reaches, 0 to 8. A claim about where a value has been and not about what it can be made to reveal (§1.5). Part of the value's type; composes by maximum; never decreases. §1.1
Descend — the expression that acquires a capability for the extent of a block. One-way within the block; only the tail value leaves. §1.3
Exhume — to grant a capability, answer a trace's holes, record the answers, and re-bury the residue, producing a new trace. §6.6
Fuel — the deterministic bound on evaluation steps a burial may take. Exhausting it is a diagnostic naming a span. §6.4
Graft — to substitute a subtrace by cairn and re-bury only what changed. §8.7
Hole — a suspended world-question: the call, its stratum, its span, and the nodes waiting on it. Identical calls are one hole. §6.3
Lamp — the rite that renders a value or walks its provenance. A tool the operator carries; never a capability the program holds. §8.4
Latent set (dƒ) — the capabilities a caller must already hold to apply a function. Carried in its arrow type, written as a trailing @n or @{n,m} on its signature, and not what the function reaches: that is a fact about a trace and no rule consumes it. §2.1
Ledger — the content-addressed store of nodes. Immutable, append-only, not garbage-collected. §7
Look — to open a shade. Well-typed only where the ambient capabilities hold the stratum the shade came out of, and not merely a deeper one: the Orpheus rule. §1.6
Node — the unit the ledger stores, addressed by its cairn: a literal, an application, a hole, a deposit, a witness, or a trace. §7.3
Opaque — a barrier burial will not evaluate through, even where it could. A typing rule, not a flag. §6.4
Orpheus rule — you may carry a shade up out of any stratum; you may only look at it by going back down. §1.6
Provenance — the backwards reading of the apply and witness nodes: what produced this value, and what produced that. §7.4
Refusal — one of six closed codes — absent, denied, malformed, unreachable, exhausted, conflict — and nothing else. The detail lives in the witness so that the value stays portable. §5.1.1
Replay — re-burying a trace with no capabilities at all, serving every answer from the ledger. Produces the same cairn, or reports the first node that differs. §6.7
Residue — what survives a burial: the unreduced nodes, the holes, and the edges between them. Itself a complete program. §6.5
Rite — one of the six commands: bury, exhume, lamp, cairn, strata, graft. §8
Seal — to take the cairn of a value. Always yields depth 0, because a name is pure regardless of what it names — which is also the shortest demonstration that depth confines provenance and not secrecy. §1.5
Sealed trace — a trace with no holes. It has a value. §6.6
Shade — a value carried up out of a deeper stratum, opaque: storable, sealable, comparable, not observable. §1.6
Starve — to be unevaluable yet, because of a transitive dependence on a hole. Ordinary: a starved expression is residualised and finishes at somebody else's exhumation. Unevaluable ever is a collapse. §6.4
Stratum — one of the nine depths, each with a grant, a cost and a witness obligation. §1.1
Trace — the immutable, content-addressed record a burial produces. §6.1
Unrecorded — stratum 8: foreign code whose behaviour cannot be witnessed. Marks a trace permanently. §1.7
Witness — the record an implementation must write before returning a world-derived value to the program. §1.4