NETHER C / PUBLIC TERMINALREAD ONLY
█   █ █████ █████ █   █ █████ ████     ████
██  █ █       █   █   █ █     █   █   █
█ █ █ ████    █   █████ ████  ████    █
█  ██ █       █   █   █ █     █  █    █
█   █ █████   █   █   █ █████ █   █    ████

a C dialect in which nothing runs_

10 Glossary

§ 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

END OF BUFFERBack to text ^