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 NART: it
reifies to an opaque nat/-namespaced constant K
before it reaches the index, so the NART autoindexes
exactly like a hand-minted symbol — no trie-key change,
no term-index change.
(unreifiableFunction F) evaluated/interpreted. The NAT is a NAUT 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 UniverseContext, 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 NART 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 **NART**: it
reifies to an opaque `nat/`-namespaced constant `K`
*before* it reaches the index, so the NART autoindexes
exactly like a hand-minted symbol — no trie-key change,
no term-index change.
(unreifiableFunction F) evaluated/interpreted. The NAT is a **NAUT** 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 UniverseContext, 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 NART 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-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 reifiableFunction? False ⇒ no sentence can contain a reifiable NAT, so the reify pass and the rename/remove NAT steps short-circuit to a no-op. An in-memory taxonomy-prop read.
Cheap gate: does the KB declare any reifiableFunction? False ⇒ no sentence can contain a reifiable NAT, so the reify pass and the rename/remove NAT steps short-circuit to a no-op. An in-memory taxonomy-prop read.
(bookkeeping-handles kb k)The believed 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.
The believed 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.
(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.
(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.
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.
(expand-expression kb form)Recursively replace every reified NART 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 NART, so non-NART content is
untouched; only NART-bearing forms are rebuilt.
Recursively replace every reified NART 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 NART, so non-NART content is untouched; only NART-bearing forms are rebuilt.
(fresh-constant)Allocate a fresh, opaque nat/-namespaced NART constant. Only ever appears in
argument position, so naming/problems (which checks functors, not arguments)
never sees it as a functor and needs no exemption.
Allocate a fresh, opaque `nat/`-namespaced NART constant. Only ever appears in argument position, so `naming/problems` (which checks functors, not arguments) never sees it as a functor and needs no exemption.
(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
nat/ constant K, assert (termOfUnit K E) in UniverseContext, materialize the
function's result types ((T K) per resultIsa, (genl K T) per resultGenl),
and return K. The bookkeeping is :monotonic — a NART'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.
All three assertions are the same bookkeeping, so all three take the chaining the caller asked for. 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 `nat/` constant `K`, assert `(termOfUnit K E)` in UniverseContext, materialize the function's result types (`(T K)` per `resultIsa`, `(genl K T)` per `resultGenl`), and return `K`. The bookkeeping is `:monotonic` — a NART'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. All three assertions are the *same* bookkeeping, so all three take the chaining the caller asked for. 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 reified-NAT (NART) constants. The cheap detector the display and mutation layers key on — a symbol is a reified NAT iff its namespace is exactly this.
Reserved namespace for reified-NAT (NART) constants. The cheap detector the display and mutation layers key on — a symbol is a reified NAT iff its namespace is exactly this.
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.
(orphaned-constants kb)Reified constants no live use references any more: every believed sentex naming
k is one of k's own bookkeeping sentexes. Removing the fact that used a NART
leaves it an orphan — its termOfUnit and materialized types would dangle a raw
nat/ symbol — so those are collected and removed.
Reified constants no live use references any more: every believed sentex naming `k` is one of `k`'s own bookkeeping sentexes. Removing the fact that used a NART leaves it an orphan — its `termOfUnit` and materialized types would dangle a raw `nat/` symbol — so those are collected and removed.
(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 (reifiableFunction head) is believed. 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 `(reifiableFunction head)` is believed. 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 a reifiableFunction — a NAT we
may reify. Ground because an open NAT ((F ?x)) would need an enumerating prover to
mint anything, so it is left alone.
True iff `form` is a ground `(F …)` whose head F is a reifiableFunction — a NAT we may reify. Ground because an open NAT (`(F ?x)`) would need an enumerating prover to mint anything, so it is left alone.
(reified-nat-symbol? term)True iff term is a reified-NAT (NART) constant — a symbol in the nat/
namespace.
True iff `term` is a reified-NAT (NART) constant — a symbol in the `nat/` namespace.
(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.
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.
(result-genl-types kb head)Types T with (resultGenl head T) — materialized as (genl K T) on a freshly
minted NART 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 NART 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
NART 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 NART 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.
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.
Where every NAT bookkeeping fact lives — (reifiableFunction F), (termOfUnit K E), (resultIsa F T), and a minted NART'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 NART'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 |