Non-atomic terms (NATs) via reification — Strategy A.
A NAT is a function-application term (F arg…) that denotes an entity —
(FruitFn AppleTree), (CapitalOf France). A function splits by declaration
into two kinds:
(reifiable_function F) object-denoting. A ground (F a…) is a reified NAT: it
reifies to an opaque nat/-namespaced constant K
before it reaches the index, so the reified NAT autoindexes
exactly like a hand-minted symbol — no trie-key change,
no term-index change.
(unreifiable_function F) evaluated/interpreted. The NAT is a structural NAT and stays
structural — (QuantityFn 5 Meter) keeps its magnitude
and unit readable for a downstream prover; it is never
minted.
The constant↔expression map is itself an ordinary stored fact, (termOfUnit K E)
in CxUniverse, so the inverted term index makes E's constituents (and K)
discoverable natively — no KV side tables. K stays STABLE across renames: a
rename rewrites the expression inside the one termOfUnit sentex in place, and
nested NATs referencing K need no cascade.
This namespace holds the detectors, the index-backed lookups, display expansion,
and the reify — both modes: the read-mode (dedup, never mint) and the
write-mode (mint a fresh constant, materialize its result types, merge rename
collisions). The write-mode stores its termOfUnit and result-type facts through the
full assert path, reached by vaelii.impl.wiring — which is where the reason that is
not an ordinary require is written down. So all NAT reification lives here.
What sits above this and calls the reify rather than reimplementing it:
vaelii.impl.skolem mints the witness an existential rule head fires to, and
vaelii.impl.nat-maintenance sequences the post-assert reconciliation and drops an
orphaned reified NAT when its last use is retracted (it rides the retract! sweep).
Reads the store, the taxonomy and belief directly (nat <- kb); reaches assertion only through the fns above.
Non-atomic terms (NATs) via reification — Strategy A.
A NAT is a function-application term `(F arg…)` that denotes an entity —
`(FruitFn AppleTree)`, `(CapitalOf France)`. A function splits by declaration
into two kinds:
(reifiable_function F) object-denoting. A ground `(F a…)` is a **reified NAT**: it
reifies to an opaque `nat/`-namespaced constant `K`
*before* it reaches the index, so the reified NAT autoindexes
exactly like a hand-minted symbol — no trie-key change,
no term-index change.
(unreifiable_function F) evaluated/interpreted. The NAT is a **structural NAT** and stays
*structural* — `(QuantityFn 5 Meter)` keeps its magnitude
and unit readable for a downstream prover; it is never
minted.
The constant↔expression map is itself an ordinary stored fact, `(termOfUnit K E)`
in CxUniverse, so the inverted term index makes `E`'s constituents (and `K`)
discoverable natively — no KV side tables. `K` stays STABLE across renames: a
rename rewrites the expression inside the one `termOfUnit` sentex in place, and
nested NATs referencing `K` need no cascade.
This namespace holds the detectors, the index-backed lookups, display expansion,
and the reify — **both** modes: the read-mode (dedup, never mint) and the
write-mode (mint a fresh constant, materialize its result types, merge rename
collisions). The write-mode stores its `termOfUnit` and result-type facts through the
full assert path, reached by `vaelii.impl.wiring` — which is where the reason that is
not an ordinary require is written down. So all NAT reification lives here.
What sits above this and *calls* the reify rather than reimplementing it:
`vaelii.impl.skolem` mints the witness an existential rule head fires to, and
`vaelii.impl.nat-maintenance` sequences the post-assert reconciliation and drops an
orphaned reified NAT when its last use is retracted (it rides the `retract!` sweep).
Reads the store, the taxonomy and belief directly (nat <- kb); reaches assertion only
through the fns above.The reifiable_function functions whose ground applications stay as written while
bound: the ones a reader does not believe the mark of (withheld-at), so the reconcile
stores, and a read looks up, the spelling that reader reads (chain/reconcile-reified!).
The `reifiable_function` functions whose ground applications stay as written while bound: the ones a reader does not believe the mark of (`withheld-at`), so the reconcile stores, and a read looks up, the spelling that reader reads (`chain/reconcile-reified!`).
(any-context-denoting-functions? kb)Cheap gate: does the KB declare any context_denoting_function? A free in-memory
taxonomy-prop read — the context half of any-reifiable-functions?. False ⇒ the KB has
no cx/ context to order, so the structural-genlCx producer's revival re-run is a no-op
without even paying the any-context-subrelations? functor-count index read.
Cheap gate: does the KB declare any `context_denoting_function`? A free in-memory taxonomy-prop read — the context half of `any-reifiable-functions?`. False ⇒ the KB has no `cx/` context to order, so the structural-genlCx producer's revival re-run is a no-op without even paying the `any-context-subrelations?` functor-count index read.
(any-corresponding-predicates? kb)Cheap gate: does the KB declare any functionCorrespondingPredicate? An O(1)
functor count, so a KB that declares none pays one integer read per assert and
nothing else.
Cheap gate: does the KB declare any `functionCorrespondingPredicate`? An O(1) functor count, so a KB that declares none pays one integer read per assert and nothing else.
(any-reifiable-functions? kb)Cheap gate: does the KB declare any function that reifies — a reifiable_function
(object, mints nat/) or a context_denoting_function (context, mints cx/)? False ⇒
no sentence can contain a reifiable NAT, so the reify pass and the rename/remove NAT
steps short-circuit to a no-op. Two in-memory taxonomy-prop reads.
Cheap gate: does the KB declare any function that reifies — a `reifiable_function` (object, mints `nat/`) or a `context_denoting_function` (context, mints `cx/`)? False ⇒ no sentence can contain a reifiable NAT, so the reify pass and the rename/remove NAT steps short-circuit to a no-op. Two in-memory taxonomy-prop reads.
(any-result-declarations? kb)Cheap gate: does the KB declare any result or genlResult? False ⇒ no mint has
materialized a result type and no application can be typed by one, so both the orphan
sweep's question about them and the argument checks' are answered without a probe. Two
O(1) functor counts, the same shape as any-corresponding-predicates?.
Cheap gate: does the KB declare any `result` or `genlResult`? False ⇒ no mint has materialized a result type and no application can be typed by one, so both the orphan sweep's question about them and the argument checks' are answered without a probe. Two O(1) functor counts, the same shape as `any-corresponding-predicates?`.
(authoritative-expression exprs)The one expression a reified constant denotes, chosen from exprs — the content-least
of them.
Normally there is nothing to choose: the map is 1:1 and exprs holds one member. A
collision the repair has yet to reach holds several, and every reader of the map has to
make the same choice out of them or they disagree about one constant — orphan? deciding
a constant orphaned against one expression while bookkeeping-handles computes what to
retract from another is a sweep that retracts the wrong records. Content, never arrival,
for the reason dedup-constant elects the surviving constant the same way: which of two
spellings the retrieval yielded first is not an answer about the KB.
The one expression a reified constant denotes, chosen from `exprs` — the **content-least** of them. Normally there is nothing to choose: the map is 1:1 and `exprs` holds one member. A collision the repair has yet to reach holds several, and every reader of the map has to make the same choice out of them or they disagree about one constant — `orphan?` deciding a constant orphaned against one expression while `bookkeeping-handles` computes what to retract from another is a sweep that retracts the wrong records. Content, never arrival, for the reason `dedup-constant` elects the surviving constant the same way: which of two spellings the retrieval yielded first is not an answer about the KB.
(bookkeeping-handles kb k)The bookkeeping sentex handles of constant k — its termOfUnit and materialized
result-type premises, plus its correspondence projection — the ones to retract when
k is orphaned. Not belief-filtered: once k is orphaned everything it owns
goes, and a bookkeeping sentex sitting OUT would otherwise stay stored, a map for
a constant the sweep has already collected.
A context constant's is its termOfUnit alone, and the structural genlCx edges
the producer computed off it are deliberately not listed: they are derived, so
retracting the map withdraws their one premise and the dependency-directed sweep
deletes them (docs/nmtms.md). Which is also what puts the far end of each edge in the
next round's candidate set, so a chain of ordered contexts collapses by the rule that
collapsed the first.
Realized before it returns, because the caller retracts what it hands back and
minted is a read of the very sentexes being retracted: it asks k's termOfUnit
which expression the mint wrote about, so a tail forced after the map's own
retraction answers #{} and the materialized types and the projection stop looking
like bookkeeping — left stored, naming a constant the sweep has collected. Whether
that happens is decided by which sentex the term index hands back first, so a lazy
answer here is a dangling nat/ symbol in some retrieval orders and not in others.
The bookkeeping sentex handles of constant `k` — its `termOfUnit` and materialized
result-type premises, plus its correspondence projection — the ones to retract when
`k` is orphaned. Not belief-filtered: once `k` is orphaned everything it owns
goes, and a bookkeeping sentex sitting OUT would otherwise stay stored, a map for
a constant the sweep has already collected.
A **context** constant's is its `termOfUnit` alone, and the structural `genlCx` edges
the producer computed off it are deliberately not listed: they are *derived*, so
retracting the map withdraws their one premise and the dependency-directed sweep
deletes them (docs/nmtms.md). Which is also what puts the far end of each edge in the
next round's candidate set, so a chain of ordered contexts collapses by the rule that
collapsed the first.
**Realized before it returns**, because the caller retracts what it hands back and
`minted` is a read of the very sentexes being retracted: it asks `k`'s `termOfUnit`
which expression the mint wrote about, so a tail forced after the map's own
retraction answers `#{}` and the materialized types and the projection stop looking
like bookkeeping — left stored, naming a constant the sweep has collected. Whether
that happens is decided by which sentex the term index hands back first, so a lazy
answer here is a dangling `nat/` symbol in some retrieval orders and not in others.(colliding-constant-groups kb)Believed reified constants that share one expression — [survivor [dup …]] per
collision. A rename can collapse two NATs onto one expression; restoring the 1:1
invariant means merging each group's dups into its survivor.
Reads the whole map, so this is the answer about the KB; the maintenance after a
rename asks the narrower question collisions-touching instead.
Believed reified constants that share one expression — `[survivor [dup …]]` per collision. A rename can collapse two NATs onto one expression; restoring the 1:1 invariant means merging each group's `dup`s into its `survivor`. Reads the whole map, so this is the answer *about the KB*; the maintenance after a rename asks the narrower question `collisions-touching` instead.
(constant-for ns E)The opaque reified constant expression E reifies to, in reserved namespace ns
(nat for an object NAT, cx for a context NAT). Deterministic in E's content
(content-name), so re-reifying E — in this process, in another, or in a KB rebuilt
in another order — yields the same constant. A hash collision (two expressions, one
name) can only degrade into the ordinary two-expressions-one-constant case the merge
repair already reconciles by content (authoritative-expression), never into a wrong
answer. A nat/ name matches the camelCase argument convention (nat-scheme-tag
explains the base62 choice) and a cx/ name is exempt as a context spelling
(naming/context?), so neither needs an exemption in naming/argument-problem, where a
reified constant is checked — only ever as an argument, never as a functor.
The opaque reified constant expression `E` reifies to, in reserved namespace `ns` (`nat` for an object NAT, `cx` for a context NAT). Deterministic in `E`'s content (`content-name`), so re-reifying `E` — in this process, in another, or in a KB rebuilt in another order — yields the *same* constant. A hash collision (two expressions, one name) can only degrade into the ordinary two-expressions-one-constant case the merge repair already reconciles by content (`authoritative-expression`), never into a wrong answer. A `nat/` name matches the camelCase argument convention (`nat-scheme-tag` explains the base62 choice) and a `cx/` name is exempt as a context spelling (`naming/context?`), so neither needs an exemption in `naming/argument-problem`, where a reified constant is checked — only ever as an argument, never as a functor.
(context-denoting-function? kb head)True iff (context_denoting_function head) is believed — head reifies to a cx/
context constant rather than a nat/ object constant (docs/context-nat.md). Read off
the taxonomy metadata like reifiable-function?, so it is context-independent and
belief-following.
True iff `(context_denoting_function head)` is believed — head reifies to a `cx/` context constant rather than a `nat/` object constant (docs/context-nat.md). Read off the taxonomy metadata like `reifiable-function?`, so it is context-independent and belief-following.
(context-denoting-ground-nat? kb form)True iff form is a ground application whose head is a context_denoting_function — a
context NAT the context slot may reify to a cx/ constant.
True iff `form` is a ground application whose head is a `context_denoting_function` — a context NAT the context slot may reify to a `cx/` constant.
Reserved namespace for context-denoting reified-NAT constants — a
(context_denoting_function F) application (F a…) mints one (docs/context-nat.md).
A Cx*Fn reifies to a cx/ constant that classifies as a context (so it can be a
sentex's context slot and a genlCx node), while its structural argument stays
readable in the termOfUnit map. Distinct from nat/ because role-reading is
spelling-only (docs/naming.md): the namespace, not a belief, carries the context role.
Reserved namespace for **context**-denoting reified-NAT constants — a `(context_denoting_function F)` application `(F a…)` mints one (docs/context-nat.md). A `Cx*Fn` reifies to a `cx/` constant that classifies as a *context* (so it can be a sentex's context slot and a `genlCx` node), while its structural argument stays readable in the `termOfUnit` map. Distinct from `nat/` because role-reading is spelling-only (docs/naming.md): the namespace, not a belief, carries the context role.
(correspondence-of kb f m)The [predicate position] declared for function f applied to m arguments, or
nil. position defaults to m + 1, the value last.
Nil when the KB believes more than one declaration for f, deliberately: two are
two different claims about what (f a…) denotes, and picking between them by handle
would make term identity depend on the order they were asserted in.
The `[predicate position]` declared for function `f` applied to `m` arguments, or nil. `position` defaults to `m + 1`, the value last. Nil when the KB believes **more than one** declaration for `f`, deliberately: two are two different claims about what `(f a…)` denotes, and picking between them by handle would make term identity depend on the order they were asserted in.
The declaration relating a NAT function to the predicate stating the same thing.
The declaration relating a NAT function to the predicate stating the same thing.
(correspondence-value kb E)The term a believed corresponding fact already names as the value of the ground NAT
expression E, or nil. Exactly one value, or none: several believed values mean the
KB does not agree on what E denotes, and reifying to one of them would be a guess
the reader could not see.
The term a believed corresponding fact already names as the value of the ground NAT expression `E`, or nil. Exactly one value, or none: several believed values mean the KB does not agree on what `E` denotes, and reifying to one of them would be a guess the reader could not see.
(corresponding-literal kb E v)The sentence the correspondence makes equivalent to E = v — the predicate applied
to E's arguments with v at the declared position — or nil when E's function has
no single correspondence.
The sentence the correspondence makes equivalent to `E = v` — the predicate applied to `E`'s arguments with `v` at the declared position — or nil when `E`'s function has no single correspondence.
(dedup-constant kb E)The existing reified constant for the ground NAT expression E, or nil — the
E → K half of the 1:1 map, so re-reifying an expression finds the constant
already minted for it rather than minting a second. More than one constant can
name E (a :bulk? load skips this probe, and an import restores whatever the
dump held), and the answer is then the lexicographically smallest — the survivor
group-collisions elects — so a read resolves to the constant the merge repair
keeps rather than to whichever the retrieval yielded first.
The existing reified constant for the ground NAT expression `E`, or nil — the `E → K` half of the 1:1 map, so re-reifying an expression finds the constant already minted for it rather than minting a second. More than one constant can name `E` (a `:bulk?` load skips this probe, and an import restores whatever the dump held), and the answer is then the lexicographically smallest — the survivor `group-collisions` elects — so a read resolves to the constant the merge repair keeps rather than to whichever the retrieval yielded first.
(expand-expression kb form)(expand-expression kb form expand?)Recursively replace every reified NAT constant in form with the functional
expression it denotes — human-readable printing / export
((color (FruitFn AppleTree) Red), never a raw nat/ symbol). Returns form
UNCHANGED (same identity) when it holds no reified NAT, so content holding no reified NAT is
untouched; only reified NAT-bearing forms are rebuilt. A vector rebuilds as a
vector — an antecedent list stays the shape its record stores. expand? narrows which
constants are expanded.
Recursively replace every reified NAT constant in `form` with the functional expression it denotes — human-readable printing / export (`(color (FruitFn AppleTree) Red)`, never a raw `nat/` symbol). Returns `form` UNCHANGED (same identity) when it holds no reified NAT, so content holding no reified NAT is untouched; only reified NAT-bearing forms are rebuilt. A vector rebuilds as a vector — an antecedent list stays the shape its record stores. `expand?` narrows which constants are expanded.
(genl-result-types kb head)(genl-result-types kb head context)Types T with (genlResult head T) — what an application of head is a subtype
of. Materialized as (genl K T) on a freshly minted reified NAT whose function is
head, and read at check time for an application that is never minted. Globally, or
(with context) through only the declarations visible from it.
Types `T` with `(genlResult head T)` — what an application of `head` is a *subtype* of. Materialized as `(genl K T)` on a freshly minted reified NAT whose function is `head`, and read at check time for an application that is never minted. Globally, or (with `context`) through only the declarations visible from it.
(maybe-reify-context kb context)(maybe-reify-context kb context mint?)Reify a context slot (CxTimeFn …) to its cx/ constant — the context-slot twin
of maybe-reify-nats, which reifies a sentence. The context argument is passed to
assert beside the sentence, so it is not on the sentence-reify walk; without this a
compound context is refused for shape (docs/context-nat.md). Minting when mint? (the
write path), dedup-only when not (a read goal resolves to an existing context, never
mints one). A bare symbol (a Cx… name or an already-reified cx/ constant) and any
non-context-denoting form pass through unchanged — the latter to be caught by the
ordinary context-shape / naming checks.
Reify a **context slot** `(CxTimeFn …)` to its `cx/` constant — the context-slot twin of `maybe-reify-nats`, which reifies a *sentence*. The context argument is passed to `assert` beside the sentence, so it is not on the sentence-reify walk; without this a compound context is refused for shape (docs/context-nat.md). Minting when `mint?` (the write path), dedup-only when not (a read goal resolves to an existing context, never mints one). A bare symbol (a `Cx…` name or an already-reified `cx/` constant) and any non-context-denoting form pass through unchanged — the latter to be caught by the ordinary context-shape / naming checks.
(maybe-reify-for-read kb sentence)(maybe-reify-for-read kb sentence reader)Reify every reifiable ground NAT subterm of a QUERY sentence to its existing
constant (dedup, never mint) so the query matches the stored atomic form. A
never-minted NAT resolves to no-match, so an unknown-NAT query matches nothing.
Cheap no-op when the KB declares no reifiable_function. Given a reader, an
application of a function the reader does not believe reifiable stays as written
(withheld-at).
Reify every reifiable ground NAT subterm of a QUERY `sentence` to its existing constant (dedup, never mint) so the query matches the stored atomic form. A never-minted NAT resolves to `no-match`, so an unknown-NAT query matches nothing. Cheap no-op when the KB declares no `reifiable_function`. Given a `reader`, an application of a function the reader does not believe reifiable stays as written (`withheld-at`).
(maybe-reify-nats kb sentence)(maybe-reify-nats kb sentence chain?)Replace every ground reifiable NAT subterm of sentence with its reified constant,
minting as needed. A cheap no-op when the KB declares no reifiable_function.
Replace every ground reifiable NAT subterm of `sentence` with its reified constant, minting as needed. A cheap no-op when the KB declares no `reifiable_function`.
(mint-nat! kb E)(mint-nat! kb E chain?)Mint a fresh reified constant for the ground NAT expression E: allocate an opaque
constant K in E's reify namespace (cx/ for a context-denoting function, else
nat/), assert (termOfUnit K E) in CxUniverse, and — for an object NAT only —
materialize the function's result types ((T K) per result, (genl K T) per
genlResult) and the correspondence projection. Returns K. The bookkeeping is
:monotonic — a reified NAT's identity and result types are structural, not defeasible
defaults. assert stores synchronously, so a second occurrence of E in the same
sentence dedups against this.
A context NAT (cx/) skips the result-type and correspondence machinery: those are
object-denoting concerns (a constant that is an instance of a type, or is the value
a predicate names), and a context is neither — it is a place, wired into the genlCx
lattice by the structural producer rather than typed (docs/context-nat.md). Its only
bookkeeping is the termOfUnit map.
The result types and the correspondence projection take the chaining the caller
asked for; (termOfUnit K E) is asserted with chaining off regardless — the
identity record is what the dedup probe reads, not content a rule fires on.
Minting is a step inside somebody else's assert, and a bulk load that turned
chaining off did so for the whole load: on OpenCyc the two unqualified ones ran
46,346 chain fixpoints nobody wanted, most of whose conclusions were then dropped
for having no placement context.
Mint a fresh reified constant for the ground NAT expression `E`: allocate an opaque constant `K` in `E`'s reify namespace (`cx/` for a context-denoting function, else `nat/`), assert `(termOfUnit K E)` in CxUniverse, and — for an **object** NAT only — materialize the function's result types (`(T K)` per `result`, `(genl K T)` per `genlResult`) and the correspondence projection. Returns `K`. The bookkeeping is `:monotonic` — a reified NAT's identity and result types are structural, not defeasible defaults. `assert` stores synchronously, so a second occurrence of `E` in the same sentence dedups against this. A **context** NAT (`cx/`) skips the result-type and correspondence machinery: those are object-denoting concerns (a constant that *is an instance of* a type, or *is the value* a predicate names), and a context is neither — it is a place, wired into the `genlCx` lattice by the structural producer rather than typed (docs/context-nat.md). Its only bookkeeping is the `termOfUnit` map. The result types and the correspondence projection take the chaining the caller asked for; `(termOfUnit K E)` is asserted with chaining off regardless — the identity record is what the dedup probe reads, not content a rule fires on. Minting is a step inside somebody else's assert, and a bulk load that turned chaining off did so for the whole load: on OpenCyc the two unqualified ones ran 46,346 chain fixpoints nobody wanted, most of whose conclusions were then dropped for having no placement context.
(names-reifiable-nat? kb s)Does sentence s hold a ground reifiable NAT the write-mode reify would replace with
a constant? The derivation path asks this of every conclusion it places, so the common
answer is reached without allocating: false on a KB that declares no reifiable
function (any-reifiable-functions?), and otherwise one walk that rebuilds nothing.
Does sentence `s` hold a ground reifiable NAT the write-mode reify would replace with a constant? The derivation path asks this of every conclusion it places, so the common answer is reached without allocating: false on a KB that declares no reifiable function (`any-reifiable-functions?`), and otherwise one walk that rebuilds nothing.
(nat-expression kb nat-sym)The NAT expression a reified constant denotes, or nil — the authoritative one where an
unrepaired collision maps it to more than one (authoritative-expression).
The NAT expression a reified constant denotes, or nil — the authoritative one where an unrepaired collision maps it to more than one (`authoritative-expression`).
Reserved namespace for object-denoting reified-NAT constants — a
(reifiable_function F) application (F a…) mints one. The cheap detector the
display and mutation layers key on.
Reserved namespace for **object**-denoting reified-NAT constants — a `(reifiable_function F)` application `(F a…)` mints one. The cheap detector the display and mutation layers key on.
Predicates whose NAT-bearing argument is a quoted expression and must NOT be
reified or type-checked as a term: the arg holds the literal NAT being mapped
(termOfUnit) or reified-to-a-real-term (rewriteOf).
Predicates whose NAT-bearing argument is a *quoted* expression and must NOT be reified or type-checked as a term: the arg holds the literal NAT being mapped (`termOfUnit`) or reified-to-a-real-term (`rewriteOf`).
The one-letter scheme prefix on every content-named reified constant, nat/a…. A
letter because a symbol whose name starts with a digit is not a readable token
(nat/9x… reads back as an invalid token), so a numeric-leading hash could not
round-trip through a dump. The letter is also the version: a is this scheme —
SHA-256 truncated to 96 bits, base62 — and a later hash or encoding change is b, old
constants keeping the names they were minted with (the whole reason a name carries its
scheme). One letter covers both jobs, so there is nothing to separate and no separator.
Base62, not base64url, because a reified constant only ever stands in argument
position, where it is held to the same spelling rules as any name
(naming/argument-problem) — and base64url's two extra characters, - and _, are
precisely the two those rules forbid (- would also make the name read as a sense).
Base62 drops just those two, so nat/a… is [A-Za-z0-9] and matches the camelCase rule
(naming/predicate?). The name is 18 characters: the one-letter tag and a 17-digit
base62 payload.
The one-letter scheme prefix on every content-named reified constant, `nat/a…`. A **letter** because a symbol whose name starts with a digit is not a readable token (`nat/9x…` reads back as an invalid token), so a numeric-leading hash could not round-trip through a dump. The letter is also the **version**: `a` is this scheme — SHA-256 truncated to 96 bits, base62 — and a later hash or encoding change is `b`, old constants keeping the names they were minted with (the whole reason a name carries its scheme). One letter covers both jobs, so there is nothing to separate and no separator. Base62, not base64url, because a reified constant only ever stands in **argument** position, where it is held to the same spelling rules as any name (`naming/argument-problem`) — and base64url's two extra characters, `-` and `_`, are precisely the two those rules forbid (`-` would also make the name read as a `sense`). Base62 drops just those two, so `nat/a…` is `[A-Za-z0-9]` and matches the camelCase rule (`naming/predicate?`). The name is 18 characters: the one-letter tag and a 17-digit base62 payload.
The reserved nat/ constant a read-mode reify resolves an unknown (never-minted)
NAT to. It can never be a real minted constant, so a query carrying it matches
nothing — an unknown-NAT query returns empty without minting. Never written,
never displayed.
The reserved `nat/` constant a read-mode reify resolves an unknown (never-minted) NAT to. It can never be a real minted constant, so a query carrying it matches nothing — an unknown-NAT query returns empty without minting. Never written, never displayed.
(orphan? kb k)Is the reified constant k orphaned — is every stored sentex naming it one of
k's own bookkeeping sentexes? False when nothing maps it: a constant with no
believed termOfUnit names no expression, so there is no map left to dangle.
For a context constant the same question reaches one thing more, because a context
is somewhere sentexes are as well as something sentences name: it is orphaned when its
context slot holds nothing, no stored sentence names it, and no stored genlCx edge
does either — bar the edges the structural producer computed from its own termOfUnit
(computed-genlCx-edge?), which are the engine's wiring rather than anybody's claim.
Its only bookkeeping is that map (minted-for).
Uses count by storage, not belief: a stored-but-OUT use revives when the defeat
above it lifts, and an inert use (a labeling's choice head) has no TMS node at all
— collecting the map from under either would leave it dangling a raw nat/
symbol, and re-reifying the expression would then mint a second constant beside
the first, a collision no merge repair caused. Only the map read
(mapped-expressions) follows belief, so a superseded spelling still answers
nothing.
One term-index read answers the whole question. k's uses, its map and its
materialized types are all sentexes naming k, so the inverted term index
(docs/indexing.md) hands back the lot in the size of k's own footprint, and nothing
here is a function of how many other constants the KB has minted. The index posts a
sentex's context beside its content terms (kv/sentex-terms), so a cx/ context's
extent is in that same answer and no second question has to be asked to be correct.
A context is asked the cheap half first. A context NAT is a place, so what is
stored in it keeps it alive as surely as what names it — and a live one is the common
case and the expensive one, since its extent is exactly what the term-index answer
would materialize. count-in-context settles it in one O(1) read on every backend
(docs/indexing.md, the secondary roots), so a context holding a million facts costs a
count rather than a million record fetches, and only an empty one goes on to the
term read. Stored, not believed, for the reason the uses are.
Asked of the authoritative expression alone, not of any expression that would
answer yes: an unrepaired collision maps k to several, and bookkeeping-handles
computes the retraction set from exactly one of them (nat-expression), so deciding
orphanhood against a different one would retract E₂'s bookkeeping on E₁'s verdict.
Is the reified constant `k` orphaned — is every **stored** sentex naming it one of `k`'s own bookkeeping sentexes? False when nothing maps it: a constant with no believed `termOfUnit` names no expression, so there is no map left to dangle. For a **context** constant the same question reaches one thing more, because a context is somewhere sentexes are as well as something sentences name: it is orphaned when its context slot holds nothing, no stored sentence names it, and no stored `genlCx` edge does either — bar the edges the structural producer computed from its own `termOfUnit` (`computed-genlCx-edge?`), which are the engine's wiring rather than anybody's claim. Its only bookkeeping is that map (`minted-for`). Uses count by storage, not belief: a stored-but-OUT use revives when the defeat above it lifts, and an inert use (a labeling's choice head) has no TMS node at all — collecting the map from under either would leave it dangling a raw `nat/` symbol, and re-reifying the expression would then mint a second constant beside the first, a collision no merge repair caused. Only the map read (`mapped-expressions`) follows belief, so a superseded spelling still answers nothing. **One term-index read answers the whole question.** `k`'s uses, its map and its materialized types are all sentexes naming `k`, so the inverted term index (docs/indexing.md) hands back the lot in the size of `k`'s own footprint, and nothing here is a function of how many other constants the KB has minted. The index posts a sentex's **context** beside its content terms (`kv/sentex-terms`), so a `cx/` context's extent is in that same answer and no second question has to be asked to be correct. **A context is asked the cheap half first.** A context NAT is a *place*, so what is stored in it keeps it alive as surely as what names it — and a live one is the common case and the expensive one, since its extent is exactly what the term-index answer would materialize. `count-in-context` settles it in one O(1) read on every backend (docs/indexing.md, the secondary roots), so a context holding a million facts costs a count rather than a million record fetches, and only an **empty** one goes on to the term read. Stored, not believed, for the reason the uses are. Asked of the **authoritative** expression alone, not of any expression that would answer yes: an unrepaired collision maps `k` to several, and `bookkeeping-handles` computes the retraction set from exactly one of them (`nat-expression`), so deciding orphanhood against a different one would retract `E₂`'s bookkeeping on `E₁`'s verdict.
(orphaned-constants kb)Every reified constant in the KB that no live use references any more. Removing the
fact that used a reified NAT leaves it an orphan — its termOfUnit and materialized
types would dangle a raw nat/ symbol — so those are collected and removed.
Reads the whole map, so this is the answer about the KB, and its cost is the KB's
whole termOfUnit population; the maintenance after a teardown asks the narrower
orphaned-among instead.
Both kinds: an object constant nothing names, and a context constant nothing is stored
in, names or wires (orphan?).
Every reified constant in the KB that no live use references any more. Removing the fact that used a reified NAT leaves it an orphan — its `termOfUnit` and materialized types would dangle a raw `nat/` symbol — so those are collected and removed. Reads the whole map, so this is the answer *about the KB*, and its cost is the KB's whole `termOfUnit` population; the maintenance after a teardown asks the narrower `orphaned-among` instead. Both kinds: an object constant nothing names, and a context constant nothing is stored in, names or wires (`orphan?`).
(orphans-named-by kb sentexes)The orphans among the constants the removed sentexes named — the region-scoped
question a teardown's sweep asks each round, which is constants-named-by fed straight
to orphaned-among.
One entry point because the two halves are one question: a constant becomes an orphan
only when something referencing it goes, so the candidate set is what the departing
sentexes named, and asking the second half of anything else would be asking about a
constant no removal touched. The whole-KB reading is orphaned-constants.
The orphans among the constants the removed `sentexes` named — the region-scoped question a teardown's sweep asks each round, which is `constants-named-by` fed straight to `orphaned-among`. One entry point because the two halves are one question: a constant becomes an orphan only when something referencing it goes, so the candidate set *is* what the departing sentexes named, and asking the second half of anything else would be asking about a constant no removal touched. The whole-KB reading is `orphaned-constants`.
(queue-split-uses! kb sentence)Queue [:reifiable f] on :respell for each function f a ground application in
sentence names whose mark some reader does not believe (split-reifiable?): the
write stores the use reified, and the settle's reconcile stores the spelling each
reader reads (chain/reconcile-reified!). One walk and no index read on a KB whose
reifiable marks every reader believes.
Queue `[:reifiable f]` on `:respell` for each function `f` a ground application in `sentence` names whose mark some reader does not believe (`split-reifiable?`): the write stores the use reified, and the settle's reconcile stores the spelling each reader reads (`chain/reconcile-reified!`). One walk and no index read on a KB whose reifiable marks every reader believes.
(reconcile-nats! kb sentence)The reified-constant maintenance a just-asserted sentence owes, in the order the
assert path runs it: the collision merge first, then the correspondence, then a result
declaration reaching the constants minted before it.
An equality assert is a rename, and its migration can collapse two reified constants
onto one expression — so merge-colliding-nats! restores the 1:1
constant↔expression invariant, and only after an equality, since nothing else can
break it. reconcile-correspondence! then equates an application with the value its
corresponding predicate names, whichever of the application, the fact and the
declaration arrived last.
Both are no-ops — one integer read each — on a KB that states no equality and declares
no correspondence. vaelii.impl.nat-maintenance/reconcile-assert is the caller, and it
holds the any-reifiable-functions? gate ahead of this.
The reified-constant maintenance a just-asserted `sentence` owes, in the order the assert path runs it: the collision merge first, then the correspondence, then a result declaration reaching the constants minted before it. An equality assert is a rename, and its migration can collapse two reified constants onto one expression — so `merge-colliding-nats!` restores the 1:1 constant↔expression invariant, and only after an equality, since nothing else can break it. `reconcile-correspondence!` then equates an application with the value its corresponding predicate names, whichever of the application, the fact and the declaration arrived last. Both are no-ops — one integer read each — on a KB that states no equality and declares no correspondence. `vaelii.impl.nat-maintenance/reconcile-assert` is the caller, and it holds the `any-reifiable-functions?` gate ahead of this.
(reifiable-entries kb f){[:prop :reifiable f] {handle context}}, the reifiable_function mark of f and its
supporters, in res/mark-entries' shape.
`{[:prop :reifiable f] {handle context}}`, the `reifiable_function` mark of `f` and its
supporters, in `res/mark-entries`' shape.(reifiable-function? kb head)True iff head reifies its ground applications — either (reifiable_function head)
(object → nat/) or (context_denoting_function head) (context → cx/). Read off the
taxonomy metadata and belief-following: a retracted declaration stops the function
reifying. A function in *withheld* does not reify while it is bound.
True iff `head` reifies its ground applications — either `(reifiable_function head)` (object → `nat/`) or `(context_denoting_function head)` (context → `cx/`). Read off the taxonomy metadata and belief-following: a retracted declaration stops the function reifying. A function in `*withheld*` does not reify while it is bound.
(reifiable-ground-nat? kb form)True iff form is a ground (F …) whose head F is an object reifiable_function — a
NAT the sentence/argument reify walk may mint to a nat/ constant. Ground because an
open NAT ((F ?x)) would need an enumerating prover to mint anything, so it is left
alone. sequential?, not seq?: reification runs before canon, so a vector-spelled
[F …] is the same NAT as (F …) — gating on the list spelling alone would store the
raw compound where the other spelling stores the constant, two handles for one canonical
sentence.
A context-denoting Cx*Fn application is excluded, even though it too reifies
(reifiable-function? is true of it): it reifies to a cx/ context constant, and only
in the context slot (maybe-reify-context), never as a sentence argument. Minting it
on the sentence walk would make one cx/ constant both a context and an untyped object
relatum — (happenedDuring E (CxTimeFn CxMonad (DatetimeFn "2000")))'s arg 2 aliasing
the very context (likes …) is stored in — so in a sentence it stays a structural
compound, exactly as an unreifiable_function NAT does (docs/context-nat.md).
True iff `form` is a ground `(F …)` whose head F is an **object** reifiable_function — a NAT the sentence/argument reify walk may mint to a `nat/` constant. Ground because an open NAT (`(F ?x)`) would need an enumerating prover to mint anything, so it is left alone. `sequential?`, not `seq?`: reification runs before `canon`, so a vector-spelled `[F …]` is the same NAT as `(F …)` — gating on the list spelling alone would store the raw compound where the other spelling stores the constant, two handles for one canonical sentence. A **context-denoting** `Cx*Fn` application is excluded, even though it too reifies (`reifiable-function?` is true of it): it reifies to a `cx/` *context* constant, and only in the **context slot** (`maybe-reify-context`), never as a sentence argument. Minting it on the sentence walk would make one `cx/` constant both a context and an untyped object relatum — `(happenedDuring E (CxTimeFn CxMonad (DatetimeFn "2000")))`'s arg 2 aliasing the very context `(likes …)` is stored in — so in a sentence it stays a structural compound, exactly as an `unreifiable_function` NAT does (docs/context-nat.md).
(reified-context-symbol? term)True iff term is a reified context constant — a symbol in the cx/
namespace. The discriminant that lets a reified constant classify as a context
(naming/context?) while an object nat/ constant classifies as a term, and what the
orphan sweep reads to ask the context liveness question of one: a context is kept
alive by what is stored in it as much as by what names it (orphan?).
True iff `term` is a reified **context** constant — a symbol in the `cx/` namespace. The discriminant that lets a reified constant classify as a context (`naming/context?`) while an object `nat/` constant classifies as a term, and what the orphan sweep reads to ask the *context* liveness question of one: a context is kept alive by what is stored **in** it as much as by what names it (`orphan?`).
The two reserved namespaces a reified constant lives in — object (nat/) and
context (cx/). Everything that asks 'is this an opaque reified constant' — display,
the K → E lookup, the orphan sweep — keys on membership here, since both kinds carry
a termOfUnit map and reify the same way; only the mint namespace and the role differ.
The two reserved namespaces a reified constant lives in — object (`nat/`) and context (`cx/`). Everything that asks 'is this an opaque reified constant' — display, the `K → E` lookup, the orphan sweep — keys on membership here, since both kinds carry a `termOfUnit` map and reify the same way; only the mint namespace and the role differ.
(reified-nat-symbol? term)True iff term is a reified constant — a symbol in one of the two reserved
reified namespaces, object (nat/) or context (cx/). Despite the object-case name it
recognizes both kinds: every caller wants 'is this an opaque
reified constant', which both are — they share the termOfUnit map, the
display expansion, and the orphan sweep.
True iff `term` is a reified constant — a symbol in one of the two reserved reified namespaces, object (`nat/`) or context (`cx/`). Despite the object-case name it recognizes both kinds: every caller wants 'is this an opaque reified constant', which both are — they share the `termOfUnit` map, the display expansion, and the orphan sweep.
(reified-nats-in form)Every reified-NAT constant form names, at any nesting.
Descends a vector as well as a list, since a vector in a sentence is a list of forms
— an exceptWhen's conjuncts, a thereExists's binders — and a constant standing in
one is as much a reference as a constant in a literal.
Every reified-NAT constant `form` names, at any nesting. Descends a vector as well as a list, since a vector in a sentence is a *list of forms* — an `exceptWhen`'s conjuncts, a `thereExists`'s binders — and a constant standing in one is as much a reference as a constant in a literal.
(reified-object-symbol? term)True iff term is a reified object constant — a symbol in the nat/ namespace.
The other half of the pair: an object constant denotes a thing sentences talk about,
so nothing can be stored in it and naming is the whole of its liveness.
True iff `term` is a reified **object** constant — a symbol in the `nat/` namespace. The other half of the pair: an object constant denotes a *thing* sentences talk about, so nothing can be stored in it and naming is the whole of its liveness.
(reify-existing kb sentence)Reify every reifiable ground NAT subterm of sentence that has an existing term to
that term, and leave every other one as written. Never mints.
vaelii.core/check reads a sentence through this. assert would reify the same subterms,
minting the ones with no term yet, and check may not write: an application with a
term is read as that term, as assert reads it, and one without stays an application,
which the argument checks read as the constant assert would mint
(checks/*entry-mints?*). Cheap no-op when the KB declares no reifiable_function.
Reify every reifiable ground NAT subterm of `sentence` that has an existing term to that term, and leave every other one as written. Never mints. `vaelii.core/check` reads a sentence through this. `assert` would reify the same subterms, minting the ones with no term yet, and `check` may not write: an application with a term is read as that term, as `assert` reads it, and one without stays an application, which the argument checks read as the constant `assert` would mint (`checks/*entry-mints?*`). Cheap no-op when the KB declares no `reifiable_function`.
(reify-in kb s nat-fn)Reify every reifiable ground NAT subterm of literal/sentence s, calling
nat-fn (a (fn [kb form])) at each one — it returns the NAT's constant, having
reified any nested NAT args itself. Quoting-predicate arguments
(termOfUnit / rewriteOf) are left opaque, as is every head predicate.
A vector is descended element by element, and every element of it. A vector in a
sentence is a list of forms rather than a literal — an exceptWhen's conjuncts, a
thereExists's binders — so it has no head predicate to hold opaque and no element to
skip. Stopping at one would leave an exception's query spelled with the compound
while the fact it is about is stored under the constant, and an exception that cannot
be answered does not hold: the rule would fire, unguarded and silently.
Reify every reifiable ground NAT subterm of literal/sentence `s`, calling `nat-fn` (a `(fn [kb form])`) at each one — it returns the NAT's constant, having reified any nested NAT args itself. Quoting-predicate arguments (`termOfUnit` / `rewriteOf`) are left opaque, as is every head predicate. **A vector is descended element by element, and every element of it.** A vector in a sentence is a *list of forms* rather than a literal — an `exceptWhen`'s conjuncts, a `thereExists`'s binders — so it has no head predicate to hold opaque and no element to skip. Stopping at one would leave an exception's query spelled with the compound while the fact it is about is stored under the constant, and an exception that cannot be answered does not hold: the rule would fire, unguarded and silently.
(reify-or-mint-nat kb form)(reify-or-mint-nat kb form chain?)Reify a ground NAT form to the term it denotes: reify any nested NAT args first,
then return the existing term for the expression — a rewriteOf target, the value
its corresponding predicate already names, else a prior termOfUnit mint — or mint a
fresh constant.
A real term outranks a placeholder, which is why the correspondence is consulted
before the dedup probe: a constant minted while the value was unknown is folded onto
that value as soon as it arrives (reconcile-correspondence!), so by the time both
exist the two answers agree — and until the merge lands, resolving to the name a
reader wrote beats resolving to an opaque one.
A quoting_function's argument is a mention — the term named as syntax — so its
nested NATs are not reified: (Quote (FruitFn Apple)) mints against the literal
(FruitFn Apple), not against that NAT's own constant, or two quoted syntaxes whose
payloads' referents merged would collapse to one mention. The whole quoted expression
is the identity, held opaque here the same way res/representative-term holds it opaque
to a sameAs merge.
Reify a ground NAT `form` to the term it denotes: reify any nested NAT args first, then return the existing term for the expression — a `rewriteOf` target, the value its corresponding predicate already names, else a prior `termOfUnit` mint — or mint a fresh constant. A **real term outranks a placeholder**, which is why the correspondence is consulted before the dedup probe: a constant minted while the value was unknown is folded onto that value as soon as it arrives (`reconcile-correspondence!`), so by the time both exist the two answers agree — and until the merge lands, resolving to the name a reader wrote beats resolving to an opaque one. A **`quoting_function`'s argument is a mention** — the term named as syntax — so its nested NATs are **not** reified: `(Quote (FruitFn Apple))` mints against the literal `(FruitFn Apple)`, not against that NAT's own constant, or two quoted syntaxes whose payloads' referents merged would collapse to one mention. The whole quoted expression is the identity, held opaque here the same way `res/representative-term` holds it opaque to a `sameAs` merge.
(resolve-for-read kb sentence)The read-mode reify of sentence (maybe-reify-for-read: dedup, never mint) when
every reifiable NAT in it already has a stored constant, else nil — the sentence names
a NAT that was never minted, so it has no stored atomic form.
A read entry point hands the reified sentence with its no-match sentinels straight to
the lookup, which then matches nothing; a write path that must not mint (core/assert- inert) refuses on nil instead, and an un-stored canonicalizer (core/canonical-sentex)
keeps the compound. Cheap no-op returning the sentence unchanged when the KB declares
no reifiable_function.
The read-mode reify of `sentence` (`maybe-reify-for-read`: dedup, never mint) when every reifiable NAT in it already has a stored constant, else nil — the sentence names a NAT that was never minted, so it has no stored atomic form. A read entry point hands the reified sentence with its `no-match` sentinels straight to the lookup, which then matches nothing; a write path that must not mint (`core/assert- inert`) refuses on nil instead, and an un-stored canonicalizer (`core/canonical-sentex`) keeps the compound. Cheap no-op returning the sentence unchanged when the KB declares no `reifiable_function`.
(respell-region kb f)The stored sentexes a reifiable_function mark on f moving can re-spell: each one
holding an application of f, and each use of an object constant whose expression
holds one, at any nesting (a constant whose expression names such a constant
included). Left out: a quoting predicate's row, whose payload is a mention, a
constant's own sentexes (own-sentex-test), which the orphan sweep collects once the
uses have moved, and the uses of a constant an equality retired. Stored, not believed: a use sitting OUT moves as a believed one does,
so its revival finds it spelled as the KB spells it.
One term-index read for f and one per constant reached, so the cost is the size of
f's applications and their constants' uses.
The stored sentexes a `reifiable_function` mark on `f` moving can re-spell: each one holding an application of `f`, and each use of an object constant whose expression holds one, at any nesting (a constant whose expression names such a constant included). Left out: a quoting predicate's row, whose payload is a mention, a constant's own sentexes (`own-sentex-test`), which the orphan sweep collects once the uses have moved, and the uses of a constant an equality retired. Stored, not believed: a use sitting OUT moves as a believed one does, so its revival finds it spelled as the KB spells it. One term-index read for `f` and one per constant reached, so the cost is the size of `f`'s applications and their constants' uses.
(respelled kb sentence)sentence as the write path spells it under the marks believed now: every object
constant expanded to the expression it maps to, then every ground reifiable application
reified again (maybe-reify-nats), minting what has no term yet. Equal to sentence
when no mark it depends on has moved.
`sentence` as the write path spells it under the marks believed now: every object constant expanded to the expression it maps to, then every ground reifiable application reified again (`maybe-reify-nats`), minting what has no term yet. Equal to `sentence` when no mark it depends on has moved.
(result-types kb head)(result-types kb head context)Types T with (result head T) — what an application of head is an instance
of. Materialized as (T K) on a freshly minted reified NAT whose function is head,
and read at check time for an application that is never minted (docs/argtypes.md).
Globally, or (with context) through only the declarations visible from it.
Types `T` with `(result head T)` — what an application of `head` is an *instance* of. Materialized as `(T K)` on a freshly minted reified NAT whose function is `head`, and read at check time for an application that is never minted (docs/argtypes.md). Globally, or (with `context`) through only the declarations visible from it.
(rewrite-target kb E)The real term T a (rewriteOf T E) declaration says the NAT expression E
reifies to instead of a fresh constant, or nil. A quoting-predicate declaration:
E is the literal NAT payload, T an existing atomic term.
Nil when the believed declarations name more than one target, exactly as
correspondence-of answers its twin question: picking between them by whichever
the retrieval yielded first would store (likes Tom Mary) or (likes Tom Maria)
according to the order two rewriteOfs arrived — divergent stored state, which
every later read then inherits. Two targets are a disagreement for the clash
machinery, not a tie for this read to break; two declarations of one target
(the engine's own reconcile writes those) are one answer.
The real term `T` a `(rewriteOf T E)` declaration says the NAT expression `E` reifies to instead of a fresh constant, or nil. A quoting-predicate declaration: `E` is the literal NAT payload, `T` an existing atomic term. Nil when the believed declarations name **more than one target**, exactly as `correspondence-of` answers its twin question: picking between them by whichever the retrieval yielded first would store `(likes Tom Mary)` or `(likes Tom Maria)` according to the order two `rewriteOf`s arrived — divergent *stored* state, which every later read then inherits. Two targets are a disagreement for the clash machinery, not a tie for this read to break; two declarations of **one** target (the engine's own reconcile writes those) are one answer.
(split-reifiable? kb f)Does some reader not believe f's stored reifiable_function mark
(res/uniform-marks?)?
Does some reader not believe `f`'s stored `reifiable_function` mark (`res/uniform-marks?`)?
Where every NAT bookkeeping fact lives — (reifiable_function F), (termOfUnit K E), (result F T), and a minted reified NAT's materialized types — so it is visible
from every context, matching the other universal vocabulary.
Where every NAT bookkeeping fact lives — `(reifiable_function F)`, `(termOfUnit K E)`, `(result F T)`, and a minted reified NAT's materialized types — so it is visible from every context, matching the other universal vocabulary.
(withheld-at kb reader)The reifiable functions reader does not believe the mark of while another reader
does, as a set: what *withheld* holds to spell a sentence as reader reads it.
Empty for a variable or nil reader.
The reifiable functions `reader` does not believe the mark of while another reader does, as a set: what `*withheld*` holds to spell a sentence as `reader` reads it. Empty for a variable or nil `reader`.
cljdoc builds & hosts documentation for Clojure/Script libraries
| Ctrl+k | Jump to recent docs |
| ← | Move to previous article |
| → | Move to next article |
| Ctrl+/ | Jump to the search field |