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:
(reifiableFunction 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.
(unreifiableFunction 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.core 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 seam 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:
(reifiableFunction 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.
(unreifiableFunction 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.core` 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 seam above.(any-context-denoting-functions? kb)Cheap gate: does the KB declare any contextDenotingFunction? 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 `contextDenotingFunction`? 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 reifiableFunction
(object, mints nat/) or a contextDenotingFunction (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 `reifiableFunction` (object, mints `nat/`) or a `contextDenotingFunction` (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 resultIsa or resultGenl? False ⇒ no mint has
materialized a result type, so the orphan sweep's question about them is answered
without a probe. Two O(1) functor counts, the same shape as
any-corresponding-predicates?.
Cheap gate: does the KB declare any `resultIsa` or `resultGenl`? False ⇒ no mint has materialized a result type, so the orphan sweep's question about them is answered without a probe. Two O(1) functor counts, the same shape as `any-corresponding-predicates?`.
(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.
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.
**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.
(constants-named-by sentexes)Every reified-NAT constant the sentences of sentexes name — the candidate set a
region-scoped orphan sweep asks orphaned-among about, given what a teardown removed.
Every reified-NAT constant the sentences of `sentexes` name — the candidate set a region-scoped orphan sweep asks `orphaned-among` about, given what a teardown removed.
(context-denoting-function? kb head)True iff (contextDenotingFunction 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 `(contextDenotingFunction 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 contextDenotingFunction — a
context NAT the context slot may reify to a cx/ constant.
True iff `form` is a ground application whose head is a `contextDenotingFunction` — a context NAT the context slot may reify to a `cx/` constant.
Reserved namespace for context-denoting reified-NAT constants — a
(contextDenotingFunction 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 `(contextDenotingFunction 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)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.
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.
(fresh-constant)(fresh-constant ns)Allocate a fresh, opaque reified constant in the given reserved namespace — nat
for an object NAT (default) or cx for a context NAT. Only ever appears in
argument or context-slot position, so naming/problems (which checks functors)
never sees it as a functor and needs no exemption.
Allocate a fresh, opaque reified constant in the given reserved namespace — `nat` for an object NAT (default) or `cx` for a context NAT. Only ever appears in argument or context-slot position, so `naming/problems` (which checks functors) never sees it as a functor and needs no exemption.
(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)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 reifiableFunction.
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 `reifiableFunction`.
(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 reifiableFunction.
Replace every ground reifiable NAT subterm of `sentence` with its reified constant, minting as needed. A cheap no-op when the KB declares no `reifiableFunction`.
(merge-colliding-nats! kb sentence)Restore the 1:1 constant↔expression invariant the just-asserted equality
sentence may have broken: when two reified constants have collapsed onto one
expression, merge each group's extras into its lexicographically-smallest survivor
by asserting an equality, which migrates the extras' uses onto the survivor. The
equality re-enters this check, but a merge removes a colliding constant, so it
converges — the second pass finds no collision.
Scoped to the class sentence merged (collisions-touching): the collisions a
merge can create all name its representative, so there is nothing to learn from the
constants it did not touch — and rereading the whole map on every equality would
make a bulk load quadratic in the NATs it has minted.
So this repairs what a merge caused, and nothing else. A collision that arrived
another way — a :bulk? load skips the dedup probe, and an import restores whatever
the dump held — is not swept up by the next unrelated equality the way a whole-map
rescan would have swept it. colliding-constant-groups is the whole-KB question,
for a caller that wants to ask it.
Restore the 1:1 constant↔expression invariant the just-asserted equality `sentence` may have broken: when two reified constants have collapsed onto one expression, merge each group's extras into its lexicographically-smallest survivor by asserting an equality, which migrates the extras' uses onto the survivor. The equality re-enters this check, but a merge removes a colliding constant, so it converges — the second pass finds no collision. Scoped to the class `sentence` merged (`collisions-touching`): the collisions a merge can create all name its representative, so there is nothing to learn from the constants it did not touch — and rereading the whole map on every equality would make a bulk load quadratic in the NATs it has minted. So this repairs what a merge **caused**, and nothing else. A collision that arrived another way — a `:bulk?` load skips the dedup probe, and an import restores whatever the dump held — is not swept up by the next unrelated equality the way a whole-map rescan would have swept it. `colliding-constant-groups` is the whole-KB question, for a caller that wants to ask it.
(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 resultIsa, (genl K T) per
resultGenl) 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 `resultIsa`, `(genl K T)` per `resultGenl`) 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.
(nat-expression kb nat-sym)The NAT expression a reified constant denotes, or nil.
The NAT expression a reified constant denotes, or nil.
Reserved namespace for object-denoting reified-NAT constants — a
(reifiableFunction 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 `(reifiableFunction 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 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.
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.
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. 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.
(orphaned-among kb candidates)The orphans among candidates — orphaned-constants' question asked of named
constants rather than of every constant in the KB.
This is the question a teardown has: a constant becomes an orphan only when something
that referenced it goes, so the constants the departing sentexes named
(constants-named-by) are the whole of what can have become one, and a KB's other NATs
cannot answer differently for having been counted. Cost is the candidate set's, not
the map's.
A candidate that is not an object nat/ constant is dropped rather than probed — a
removed sentence names ordinary terms too, and none of them has a map to orphan, while a
cx/ context constant is kept out of the sweep on purpose (reified-object-symbol?).
The orphans among `candidates` — `orphaned-constants`' question asked of named constants rather than of every constant in the KB. This is the question a teardown has: a constant becomes an orphan only when something that referenced it goes, so the constants the departing sentexes named (`constants-named-by`) are the whole of what can have become one, and a KB's other NATs cannot answer differently for having been counted. Cost is the candidate set's, not the map's. A candidate that is not an **object** `nat/` constant is dropped rather than probed — a removed sentence names ordinary terms too, and none of them has a map to orphan, while a `cx/` context constant is kept out of the sweep on purpose (`reified-object-symbol?`).
(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.
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.
(reconcile-correspondence! kb sentence)The correspondence maintenance a just-asserted sentence calls for: a declaration
reconciles the applications minted before it, and a fact on a corresponding predicate
reconciles the one application it names a value for. A no-op — one integer read —
on a KB that declares no correspondence.
The correspondence maintenance a just-asserted `sentence` calls for: a declaration reconciles the applications minted before it, and a fact on a corresponding predicate reconciles the one application it names a value for. A no-op — one integer read — on a KB that declares no correspondence.
(reifiable-function? kb head)True iff head reifies its ground applications — either (reifiableFunction head)
(object → nat/) or (contextDenotingFunction head) (context → cx/). Read straight
off the taxonomy metadata, so it is context-independent — deliberately, since reification
decides term identity, which cannot vary by reader — and belief-following: a defeated
or retracted declaration stops the function reifying.
True iff `head` reifies its ground applications — either `(reifiableFunction head)` (object → `nat/`) or `(contextDenotingFunction head)` (context → `cx/`). Read straight off the taxonomy metadata, so it is context-independent — deliberately, since reification decides *term identity*, which cannot vary by reader — and belief-following: a defeated or retracted declaration stops the function reifying.
(reifiable-ground-nat? kb form)True iff form is a ground (F …) whose head F is an object reifiableFunction — 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 unreifiableFunction NAT does (docs/context-nat.md).
True iff `form` is a ground `(F …)` whose head F is an **object** reifiableFunction — 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 `unreifiableFunction` 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.
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.
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.
What the orphan sweep collects on: an object constant is orphaned when no sentence
names it any more, but a context constant's liveness is the facts stored in it (its
context slot), which the term index does not post — so contexts are left out of the
sweep and persist until torn down explicitly (docs/context-nat.md).
True iff `term` is a reified **object** constant — a symbol in the `nat/` namespace. What the orphan sweep collects on: an object constant is orphaned when no sentence names it any more, but a context constant's liveness is the facts stored *in* it (its context slot), which the term index does not post — so contexts are left out of the sweep and persist until torn down explicitly (docs/context-nat.md).
(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 quotingFunction'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 **`quotingFunction`'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.
(result-genl-types kb head)Types T with (resultGenl head T) — materialized as (genl K T) on a freshly
minted reified NAT whose function is head (its output is a subtype of T).
Types `T` with `(resultGenl head T)` — materialized as `(genl K T)` on a freshly minted reified NAT whose function is `head` (its output is a *subtype* of T).
(result-isa-types kb head)Types T with (resultIsa head T) — materialized as (T K) on a freshly minted
reified NAT whose function is head (its output is an instance of T).
Types `T` with `(resultIsa head T)` — materialized as `(T K)` on a freshly minted reified NAT whose function is `head` (its output is an *instance* of T).
(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.
Where every NAT bookkeeping fact lives — (reifiableFunction F), (termOfUnit K E), (resultIsa 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 — `(reifiableFunction F)`, `(termOfUnit K E)`, `(resultIsa F T)`, and a minted reified NAT's materialized types — so it is visible from every context, matching the other universal vocabulary.
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 |