The KB record, its constructor, and the ground floor of retrieval: find/create
sentexes, the belief-filtered sentexes-matching, and the equality-closure goal
rewriting. Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle <- vaelii.core): it reads the storage protocols, the taxonomy, the JTMS and the
matchers, never assertion, chaining or settling. See docs/namespaces.md.
The KB record, its constructor, and the ground floor of retrieval: find/create sentexes, the belief-filtered `sentexes-matching`, and the equality-closure goal rewriting. Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core): it reads the storage protocols, the taxonomy, the JTMS and the matchers, never assertion, chaining or settling. See docs/namespaces.md.
True while open-kb recovers a KB opened with :recover? :background.
vaelii.impl.recovery/recover reads it: an image declined only for its engine source is
then installed, and belief is rebuilt behind it.
True while `open-kb` recovers a KB opened with `:recover? :background`. `vaelii.impl.recovery/recover` reads it: an image declined only for its engine source is then installed, and belief is rebuilt behind it.
True while vaelii.impl.recovery runs a recover from the records on the calling thread.
refresh-index-image! then writes nothing, so a settle does not wait on an image write
that its own later writes make stale. recover calls refresh-index-image! once after the recover.
True while `vaelii.impl.recovery` runs a recover from the records on the calling thread. `refresh-index-image!` then writes nothing, so a settle does not wait on an image write that its own later writes make stale. `recover` calls `refresh-index-image!` once after the recover.
True while open-kb recovers a KB opened with :recover? :trust.
vaelii.impl.recovery/recover reads it: an image declined only for its engine source is
then installed and kept, with no rebuild behind it.
True while `open-kb` recovers a KB opened with `:recover? :trust`. `vaelii.impl.recovery/recover` reads it: an image declined only for its engine source is then installed and kept, with no rebuild behind it.
(add-reasoners! kb names)Register the reasoners in names on kb and record the union in its store. Every
name is resolved before anything is registered, so a bad name registers none.
Register the reasoners in `names` on `kb` and record the union in its store. Every name is resolved before anything is registered, so a bad name registers none.
(announce-once! kb)True the first time it is called for kb, false afterwards — so the write-side escape
says what it is giving up once per KB rather than once per assert.
True the first time it is called for `kb`, false afterwards — so the write-side escape says what it is giving up once per KB rather than once per assert.
(antecedent-order kb handles)handles as a justification's stored antecedent vector, ordered by what each antecedent
says (its sentence, then its context), never by the handle. A handle is assertion order, so
an arrival-ordered vector would leak arrival into core/why, why-not, preview and the
sort key of core/supporting-justifications. The informant is not in the vector; belief
reads the antecedents as a set. Short-circuited below two. Call it where something is
stored (the justification writers and the refusal ledger), never where something is only
decided: move a call later, never earlier.
`handles` as a justification's stored antecedent vector, ordered by what each antecedent says (its sentence, then its context), never by the handle. A handle is assertion order, so an arrival-ordered vector would leak arrival into `core/why`, `why-not`, `preview` and the sort key of `core/supporting-justifications`. The informant is not in the vector; belief reads the antecedents as a set. Short-circuited below two. Call it where something is stored (the justification writers and the refusal ledger), never where something is only decided: move a call later, never earlier.
(backend-axes {:keys [backend records index] :or {backend :memory}})The {:records :index} selection for opts: the :backend sugar expanded, with an
explicit :records / :index opt overriding its half. Public so a harness asking which
two stores an opts map names reads the table open-kb does. Refuses (naming the pairing
to take instead): the :disk-log index over non-durable records (durable-under-log-index),
the :snapshot index over a store with no records fingerprint (image-record-axes),
:overlay on one axis alone, and the reserved names (reserved-backend-names).
The `{:records :index}` selection for `opts`: the `:backend` sugar expanded, with an
explicit `:records` / `:index` opt overriding its half. Public so a harness asking which
two stores an opts map names reads the table `open-kb` does. Refuses (naming the pairing
to take instead): the `:disk-log` index over non-durable records (`durable-under-log-index`),
the `:snapshot` index over a store with no records fingerprint (`image-record-axes`),
`:overlay` on one axis alone, and the reserved names (`reserved-backend-names`).Every :backend name, sorted — backend-modes is past the size at which a map
literal keeps its order, so the list is sorted rather than claiming one. Public for
opt-keys' reason — it is the answer to "is this a real backend?", and a caller who
can ask does not have to find out from a refusal — and because the list has readers
outside this process: the suite's configuration list (scripts/lib/suite-configs.sh),
the parity test (backend_parity_test) and docs/storage.md's table each cover it, and
a name none of them knows about is a backend that ships untested and undocumented.
Those three hold themselves to this vector, each naming what it leaves out and why.
Every `:backend` name, sorted — `backend-modes` is past the size at which a map literal keeps its order, so the list is sorted rather than claiming one. Public for `opt-keys`' reason — it is the answer to "is this a real backend?", and a caller who can ask does not have to find out from a refusal — and because the list has readers outside this process: the suite's configuration list (`scripts/lib/suite-configs.sh`), the parity test (`backend_parity_test`) and docs/storage.md's table each cover it, and a name none of them knows about is a backend that ships untested and undocumented. Those three hold themselves to this vector, each naming what it leaves out and why.
(body-under-not sentence)A fact's body with a single leading not stripped — the form both polarities key
on ((not (flies Opus)) and (flies Opus) share the body (flies Opus)). Double
negation is eliminated at store time, so one strip suffices; a non-fact sentence (a
rule, a metadata declaration) is returned unchanged and simply never opposes.
A fact's body with a single leading `not` stripped — the form both polarities key on (`(not (flies Opus))` and `(flies Opus)` share the body `(flies Opus)`). Double negation is eliminated at store time, so one strip suffices; a non-fact sentence (a rule, a metadata declaration) is returned unchanged and simply never opposes.
(canonical-sentence kb sentence context)sentence as this KB would store it in context — the entry point's own canonicalizer,
asked without storing or looking anything up. Equal to sentence for the sentence a
caller just wrote through the entry point, and different for one the store already holds under
a spelling the taxonomy has since stopped canonicalizing to: a (symmetric P) mark
arriving after (P b a) was stored is the case, and telling the two apart is what
integrate/commute-existing sweeps on.
`sentence` as this KB would **store** it in `context` — the entry point's own canonicalizer, asked without storing or looking anything up. Equal to `sentence` for the sentence a caller just wrote through the entry point, and different for one the store already holds under a spelling the taxonomy has since stopped canonicalizing to: a `(symmetric P)` mark arriving after `(P b a)` was stored is the case, and telling the two apart is what `integrate/commute-existing` sweeps on.
The smallest seed frontier a chain run arms the authority memo above for. Coarse,
not tuned: it separates an incremental assert (a seed of one, plus a few migration
seeds) from a bulk fixpoint (a forward-chain's whole datum set, a load, a broad edge's
subsumption seeds), and the memo's benefit is flat across the wide band between them —
above the floor one probe per functor is repaid by the walks it skips, below it there
are too few conclusions to repay a probe at all. Placed here beside the memo var it
arms, so the mechanism and the policy that arms it read together.
The smallest seed frontier a `chain` run arms the authority memo above for. Coarse, not tuned: it separates an incremental `assert` (a seed of one, plus a few migration seeds) from a bulk fixpoint (a `forward-chain`'s whole datum set, a load, a broad edge's subsumption seeds), and the memo's benefit is flat across the wide band between them — above the floor one probe per functor is repaid by the walks it skips, below it there are too few conclusions to repay a probe at all. Placed here beside the memo var it arms, so the mechanism and the policy that arms it read together.
(create-sentex kb sentence context)(create-sentex kb sentence context strength)Store sentence in context as a new sentex, index it, and return [handle sentex].
strength (optional) is the strength the record is born with, so a caller asserting a
premise avoids a second record frame from mark-premise. An index write that throws takes
the record with it: the postings that landed are taken out and the record is deleted
before the throw travels, since the next open's coverage check would otherwise index it and
believe it as a premise whose forward rules never ran. A failed unindex or delete is added as suppressed; the next
open's coverage check repairs the pair.
Store `sentence` in `context` as a new sentex, index it, and return `[handle sentex]`. `strength` (optional) is the strength the record is born with, so a caller asserting a premise avoids a second record frame from `mark-premise`. An index write that throws takes the record with it: the postings that landed are taken out and the record is deleted before the throw travels, since the next open's coverage check would otherwise index it and believe it as a premise whose forward rules never ran. A failed unindex or delete is added as suppressed; the next open's coverage check repairs the pair.
(defeat-reach kb stored removed)The handles the placed sentexes stored move (placed-targets) and those of removed
([target …] pairs), and every handle walked forward from them (defeat-walk): the
handles whose belief those moves can change with no relabel.
The handles the placed sentexes `stored` move (`placed-targets`) and those of `removed` (`[target …]` pairs), and every handle walked forward from them (`defeat-walk`): the handles whose belief those moves can change with no relabel.
(defeat-target sentence)The handle a (defeat (sentexHandle H)) sentence removes from belief, or nil for any
other sentence. The shape test of except-target, on the defeat functor.
The handle a `(defeat (sentexHandle H))` sentence removes from belief, or nil for any other sentence. The shape test of `except-target`, on the `defeat` functor.
(discharge-over-empty-store! kb)Retire a standing hazard when a write entry point is about to write into an empty store,
and answer whether one was retired. An importer writes around the write entry points, so
its declaration stands for the whole load; anything that emptied the store and then asserts
builds the network as it goes. The rule lives here because any holder of the store can call
p/clear-records!. Costs a map read on a KB with no hazard standing.
Retire a standing hazard when a write entry point is about to write into an empty store, and answer whether one was retired. An importer writes around the write entry points, so its declaration stands for the whole load; anything that emptied the store and then asserts builds the network as it goes. The rule lives here because any holder of the store can call `p/clear-records!`. Costs a map read on a KB with no hazard standing.
(disjoint? kb a b)(disjoint? kb a b context)Are types a and b provably disjoint (via disjoint declarations, closed
under genl) — anywhere, or (with context) using only the declarations and
genl edges visible from it?
The 3-arity is the KB-wide reading vaelii.core/disjoint? documents.
Are types `a` and `b` provably disjoint (via disjoint declarations, closed under genl) — anywhere, or (with `context`) using only the declarations and genl edges visible from it? The 3-arity is the KB-wide reading `vaelii.core/disjoint?` documents.
(displaced-terms kb sentence)(displaced-terms kb sentence context)The {old-term representative} rewrites a sentence undergoes as context elects them,
empty when nothing in it merged: what a supersession records, so why-not names the
displacing representative.
The `{old-term representative}` rewrites a sentence undergoes as `context` elects them,
empty when nothing in it merged: what a supersession records, so `why-not` names the
displacing representative.(displaced-terms* kb sentence visible?)The {old-term representative} rewrites sentence undergoes under the built
predicate visible? (res/displaced-terms-in), empty when nothing in it merged.
The `{old-term representative}` rewrites `sentence` undergoes under the built
predicate `visible?` (`res/displaced-terms-in`), empty when nothing in it merged.(durable-dirs opts)The canonical directories open-kb over opts would take an exclusive lock on: the
records/index directory (:disk records or a :disk-log index) and, for a durable fork,
the fork's own writable directory. core/open-kb releases the ones this call newly opened
when a throw after the stores resolve would leave a lock held. Empty for an all-in-RAM KB.
Pure over opts; malformed opts answer empty, and the construction throws the refusal.
The canonical directories `open-kb` over `opts` would take an exclusive lock on: the records/index directory (`:disk` records or a `:disk-log` index) and, for a durable fork, the fork's own writable directory. `core/open-kb` releases the ones this call newly opened when a throw after the stores resolve would leave a lock held. Empty for an all-in-RAM KB. Pure over `opts`; malformed opts answer empty, and the construction throws the refusal.
(empty-reasoning tms)The reasoning state a KB opens with, all of it empty, as one Reasoning value
(vaelii.impl.types.reasoning): the belief network of kind tms, the taxonomy, and every
atom a recover or a settle fills. open-kb builds a KB holding one, and rebuild-kb
builds a second KB over the same stores holding another, so a field added to Reasoning
and here starts empty in both.
The reasoning state a KB opens with, all of it empty, as one `Reasoning` value (`vaelii.impl.types.reasoning`): the belief network of kind `tms`, the taxonomy, and every atom a recover or a settle fills. `open-kb` builds a KB holding one, and `rebuild-kb` builds a second KB over the same stores holding another, so a field added to `Reasoning` and here starts empty in both.
The relations that assert a merge, acted on in vaelii.impl.special and read by
stratification (vaelii.impl.checks). different reads the closure and is never
stored.
The relations that assert a merge, acted on in `vaelii.impl.special` and read by stratification (`vaelii.impl.checks`). `different` reads the closure and is never stored.
(except-target sentence)The handle a visibility (except (sentexHandle H)) sentence hides, or nil for any
other sentence — including (not (except …)), whose functor is not.
A meta-exception — (except (sentexHandle E)) where E is itself an (except …) —
cascades: hiding an except suppresses its effect, restoring visibility of the target
the inner except was hiding. The cascade is evaluated at read time by
exc/excepted-handles, which checks whether each except-handle is itself
hidden before counting it as active.
The handle a visibility `(except (sentexHandle H))` sentence hides, or nil for any other sentence — including `(not (except …))`, whose functor is `not`. A **meta-exception** — `(except (sentexHandle E))` where E is itself an `(except …)` — cascades: hiding an except suppresses its effect, restoring visibility of the target the inner except was hiding. The cascade is evaluated at read time by `exc/excepted-handles`, which checks whether each except-handle is itself hidden before counting it as active.
(find-or-create-sentex kb sentence context)(find-or-create-sentex kb sentence context strength)The existing sentex for sentence in context, or a new one — [handle sentex new?].
strength is passed through to create-sentex and so applies only to a new record;
an existing one keeps what it has until mark-premise says otherwise.
The existing sentex for `sentence` in `context`, or a new one — `[handle sentex new?]`. `strength` is passed through to `create-sentex` and so applies only to a *new* record; an existing one keeps what it has until `mark-premise` says otherwise.
(find-sentex-handle kb sentence context)The handle of an existing sentex for sentence in context, or nil. A sentence with
variables is found by its stored sentence (stored-at), since the key alpha-renames. Every
probe is p/leaf-at, the exact leaf. One probe answers a symmetric literal: the sort is
order-blind, and the (symmetric P) mark migrates earlier rows
(integrate/commute-existing), so the store holds the spelling this probe builds.
The handle of an existing sentex for `sentence` in `context`, or nil. A sentence with variables is found by its stored sentence (`stored-at`), since the key alpha-renames. Every probe is `p/leaf-at`, the exact leaf. One probe answers a symmetric literal: the sort is order-blind, and the `(symmetric P)` mark migrates earlier rows (`integrate/commute-existing`), so the store holds the spelling this probe builds.
(find-sentexes kb term)Every stored sentex that contains term anywhere (any position, any nesting). An atom
is one inverted-index read. A compound is narrowed by the postings of its atoms and each
candidate is verified against its own sentence. A compound holding a variable is a pattern
and answers nothing here; sentexes-matching takes a pattern.
Every stored sentex that contains `term` anywhere (any position, any nesting). An atom is one inverted-index read. A compound is narrowed by the postings of its atoms and each candidate is verified against its own sentence. A compound holding a variable is a pattern and answers nothing here; `sentexes-matching` takes a pattern.
(find-sentexes-all kb terms)Every stored sentex that contains all of terms. One intersection over every term's
probe keys, then the same verify find-sentexes does, once per compound among them.
Every stored sentex that contains all of `terms`. One intersection over every term's probe keys, then the same verify `find-sentexes` does, once per compound among them.
(forget-lazy-rules! kb)(forget-lazy-rules! kb empty?)Drop stores-lazy-rule?'s answer and move its generation: at the store or removal of a
rule taking :lazy, at an engines join adding it, and at a write of the stores that
bypasses create-sentex (reindex, an import's record phase). With empty?, the answer
is false instead, which a wipe of the stores leaves true (core/clear!).
Drop `stores-lazy-rule?`'s answer and move its generation: at the store or removal of a rule taking `:lazy`, at an engines join adding it, and at a write of the stores that bypasses `create-sentex` (`reindex`, an import's record phase). With `empty?`, the answer is false instead, which a wipe of the stores leaves true (`core/clear!`).
(forget-mint-rules! kb)(forget-mint-rules! kb empty?)Drop kb's mint-rule-table and move its generation, so the next read fills it off
the index: at the store or removal of a rule of kv/mint-rules, and at a write of the
stores that bypasses create-sentex (reindex, an import's record phase). With
empty?, the table holds no rule instead, which a wipe of the stores leaves true
(core/clear!).
Drop `kb`'s `mint-rule-table` and move its generation, so the next read fills it off the index: at the store or removal of a rule of `kv/mint-rules`, and at a write of the stores that bypasses `create-sentex` (`reindex`, an import's record phase). With `empty?`, the table holds no rule instead, which a wipe of the stores leaves true (`core/clear!`).
(handle-cache-key kb)What a cached handle lookup is valid under: which KB it was asked of, and the set of
predicates declared symmetric, the one thing resolution/kb-sentex reads off the KB.
The record store rides in the key because with-handle-cache reuses an outer run's map,
so a nested run on a second KB would read the first's handles. The set is read unscoped.
What a cached handle lookup is valid under: which KB it was asked of, and the set of predicates declared `symmetric`, the one thing `resolution/kb-sentex` reads off the KB. The record store rides in the key because `with-handle-cache` reuses an outer run's map, so a nested run on a second KB would read the first's handles. The set is read unscoped.
(isa-among? {:keys [types tax context isa]} t)Is t a supertype of one of the types a memberships read ms holds — by genl? from
its context, reflexively? Memoized in ms.
Is `t` a supertype of one of the types a `memberships` read `ms` holds — by `genl?` from its context, reflexively? Memoized in `ms`.
(isa? kb x t)(isa? kb x t context)Is individual x (transitively) of type t? Considers only type memberships visible
from context (default: any). Reads x's own memberships and climbs from each (see
memberships). A non-symbol x falls back to the matcher. Lazy in the memberships;
memberships is the batch form.
Is individual `x` (transitively) of type `t`? Considers only type memberships visible from `context` (default: any). Reads `x`'s own memberships and climbs from each (see `memberships`). A non-symbol `x` falls back to the matcher. Lazy in the memberships; `memberships` is the batch form.
(justification-content-key kb)The key every listing of justifications sorts on: the informant's content (a rule's
sentence and context, or the symbol), its antecedents' sentences, the firing's bindings, and
the concluded sentence and context. Returns the key fn. Shared by
core/supporting-justifications, core/dependent-justifications and a clash report's
:justifications, which must not drift. The informant enters as content and never as its
handle. The consequence is in the key for dependent-justifications. Compare with
nm/compare-form, never compare.
The key every listing of justifications sorts on: the informant's content (a rule's sentence and context, or the symbol), its antecedents' sentences, the firing's bindings, and the concluded sentence and context. Returns the key fn. Shared by `core/supporting-justifications`, `core/dependent-justifications` and a clash report's `:justifications`, which must not drift. The informant enters as content and never as its handle. The consequence is in the key for `dependent-justifications`. Compare with `nm/compare-form`, never `compare`.
(membership-reader kb context)A term -> memberships reader, memoized for the life of one caller. The definitional
checks ask about each of a few terms several times, and each ask is a posting read, a record
fetch and a belief test per entry that cannot change under one assert.
A `term -> memberships` reader, memoized for the life of one caller. The definitional checks ask about each of a few terms several times, and each ask is a posting read, a record fetch and a belief test per entry that cannot change under one `assert`.
(memberships kb x context)What a term is, as the checks ask it: {:types [t …] …}, the types asserted of x and
visible from context, with what isa-among? needs. isa? x t reads up from the types
the term holds (genl? walks without building the closure), the cheap direction, since
specs(t) is every type for t = thing. Memoized per memberships read, which
membership-reader memoizes per term.
What a term is, as the checks ask it: `{:types [t …] …}`, the types asserted of `x` and
visible from `context`, with what `isa-among?` needs. `isa? x t` reads up from the types
the term holds (`genl?` walks without building the closure), the cheap direction, since
`specs(t)` is every type for `t` = `thing`. Memoized per `memberships` read, which
`membership-reader` memoizes per term.(mint-informant? kb informant)Is informant one an argument declaration's mint is justified under (mint-kind)?
Is `informant` one an argument declaration's mint is justified under (`mint-kind`)?
(mint-kind kb informant)The declaring kind a justification with informant mints under, or nil: the kind whose
rule handle informant is in mint-rule-table, or the kind informant names when it is
a key of kv/mint-rules itself.
The declaring kind a justification with `informant` mints under, or nil: the kind whose rule handle `informant` is in `mint-rule-table`, or the kind `informant` names when it is a key of `kv/mint-rules` itself.
(mint-rule-table kb){kind handle}: the handles kb stores the rules of kv/mint-rules at, read off the
index's [:mint-rules] family (reads/as-stored-mint-rules) and held in the
:mint-rules atom until forget-mint-rules! moves its generation. The fill installs
with a compare-and-set against the generation it read, so a rule stored or removed
during the fill makes it read the family again.
`{kind handle}`: the handles `kb` stores the rules of `kv/mint-rules` at, read off the
index's `[:mint-rules]` family (`reads/as-stored-mint-rules`) and held in the
`:mint-rules` atom until `forget-mint-rules!` moves its generation. The fill installs
with a compare-and-set against the generation it read, so a rule stored or removed
during the fill makes it read the family again.(moved-reach kb seeds)The handles seeds and every handle walked forward from them (defeat-walk): the
handles whose belief a write naming seeds can change with no relabel.
The handles `seeds` and every handle walked forward from them (`defeat-walk`): the handles whose belief a write naming `seeds` can change with no relabel.
(note-hazards! kb hazards)Record which of {:no-belief :no-index} hold for this KB: {:no-belief false} from
core/recover, {:no-index false} from core/reindex, whatever it finds from open-kb.
A key it does not mention is left as it was. Returns kb. An importer that lands records
and skips the recover (:belief? false, :belief? :stored) declares {:no-belief true}
here, since the store is indistinguishable from one of assert-inert sentexes.
Record which of `{:no-belief :no-index}` hold for this KB: `{:no-belief false}` from
`core/recover`, `{:no-index false}` from `core/reindex`, whatever it finds from `open-kb`.
A key it does not mention is left as it was. Returns `kb`. An importer that lands records
and skips the recover (`:belief? false`, `:belief? :stored`) declares `{:no-belief true}`
here, since the store is indistinguishable from one of `assert-inert` sentexes.(note-lazy-rule-moved! kb s)forget-lazy-rules! when sentex s, stored or leaving, is a rule taking :lazy.
`forget-lazy-rules!` when sentex `s`, stored or leaving, is a rule taking `:lazy`.
(note-mint-rule-moved! kb s)forget-mint-rules! when sentex s, stored or leaving, is a rule of kv/mint-rules,
after the index write that posts or retires it. Every sentex that is not an inert rule
costs two field reads.
`forget-mint-rules!` when sentex `s`, stored or leaving, is a rule of `kv/mint-rules`, after the index write that posts or retires it. Every sentex that is not an inert rule costs two field reads.
(note-reach-touched! kb)Fold into each entry of the reach memo (held-forward-reach) the handles the touched
sets recorded since its mark, before settle/settle-finish empties them and outdates
the mark, and note the generation fed. An entry the touched sets have already
outdated unfed, or whose handles to read grow past reach-moved-cap, is dropped: its
next read walks from the targets. A witness path reads no touched set and stays.
Fold into each entry of the reach memo (`held-forward-reach`) the handles the touched sets recorded since its mark, before `settle/settle-finish` empties them and outdates the mark, and note the generation fed. An entry the touched sets have already outdated unfed, or whose handles to read grow past `reach-moved-cap`, is dropped: its next read walks from the targets. A witness path reads no touched set and stays.
(open-kb {:keys [space recover? tms naming]
:or {space 0 recover? :trust tms :dense naming :strict}
:as opts}
recover-fn
reindex-fn)Construct a KB: the implementation behind vaelii.core/open-kb, which owns the
user-facing docstring. :backend (:memory default) names a record/index pair, or
:records / :index select the axes; :tms (:dense default, or :reference) selects the
truth-maintenance representation. recover-fn and reindex-fn (core/reindex: rebuild
the index from the records, then recover) are injected because they run the engine stack
above this namespace.
Construct a KB: the implementation behind `vaelii.core/open-kb`, which owns the user-facing docstring. `:backend` (`:memory` default) names a record/index pair, or `:records` / `:index` select the axes; `:tms` (`:dense` default, or `:reference`) selects the truth-maintenance representation. `recover-fn` and `reindex-fn` (`core/reindex`: rebuild the index from the records, then recover) are injected because they run the engine stack above this namespace.
(oplog-mode opts)The fsync mode opts' :oplog? asks for, nil for no log, or a refusal
(:unknown-option): a value oplog-modes does not name, a log on a backend other than
:disk-snapshot or :pg-snapshot, or a log with a :recover? other than :trust or
:auto. A log restores into a built KB or rebuilds one, so it has no reading for a KB
left unrecovered or rebuilt in the background.
The fsync mode `opts`' `:oplog?` asks for, nil for no log, or a refusal (`:unknown-option`): a value `oplog-modes` does not name, a log on a backend other than `:disk-snapshot` or `:pg-snapshot`, or a log with a `:recover?` other than `:trust` or `:auto`. A log restores into a built KB or rebuilds one, so it has no reading for a KB left unrecovered or rebuilt in the background.
What :oplog? may say, and the fsync mode each one means (vaelii.impl.oplog): true
and :each fsync each operation's frame before the operation runs, :tick leaves the
frame to the durability daemon's tick, false attaches no log.
What `:oplog?` may say, and the fsync mode each one means (`vaelii.impl.oplog`): `true` and `:each` fsync each operation's frame before the operation runs, `:tick` leaves the frame to the durability daemon's tick, `false` attaches no log.
Every key open-kb reads. Public because it is the answer to "is this a real
option?", and a caller that can ask does not have to find out from a wrong answer.
Every key `open-kb` reads. Public because it is the answer to "is this a real option?", and a caller that can ask does not have to find out from a wrong answer.
(placed-targets kb s)The handles the placed sentence s moves with no relabel: a defeat's target, and,
while an except is stored, the members of a (contradicts …), one of which a reader
whose excepts lower its class reads as defeated (exc/conflicts-naming).
The handles the placed sentence `s` moves with no relabel: a `defeat`'s target, and, while an except is stored, the members of a `(contradicts …)`, one of which a reader whose excepts lower its class reads as defeated (`exc/conflicts-naming`).
(preferred-term [f a _])The term this equality sentence puts on top, or nil. rewriteOf deprecates its
second argument in favour of its first; sameAs and equals deprecate neither.
The term this equality sentence puts on top, or nil. `rewriteOf` deprecates its second argument in favour of its first; `sameAs` and `equals` deprecate neither.
(prior-kb kb)kb as it stood when the open write record opened (observe/*write-record*): its
records, index, network, taxonomy and nogood candidates before the writes the record
holds, with every cache empty and the taxonomy's visibility callbacks reading the copy.
Read-only; a caller reads it with observe/*write-record* unbound.
`kb` as it stood when the open write record opened (`observe/*write-record*`): its records, index, network, taxonomy and nogood candidates before the writes the record holds, with every cache empty and the taxonomy's visibility callbacks reading the copy. Read-only; a caller reads it with `observe/*write-record*` unbound.
(reach-strength kb rel-key sub super)(reach-strength kb rel-key sub super context)The defeat class of the strongest route sub →* super in rel-key (:genl for the
type/predicate hierarchy, :genlCx for contexts) that context sees — :monotonic /
:default, or nil when unreachable. nil context is the unscoped read.
The diagnostic half of the widest-bottleneck rule: it reports the strength a subsuming firing's conclusion now rests on, so a KB with a defeasible taxonomy edge and an alternate route can ask how strongly one term subsumes another. Reads the live JTMS defeat-class of each edge supporter (docs/taxonomy.md, "Strength of a subsumption path").
The defeat class of the **strongest** route `sub →* super` in `rel-key` (`:genl` for the type/predicate hierarchy, `:genlCx` for contexts) that `context` sees — `:monotonic` / `:default`, or nil when unreachable. `nil` context is the unscoped read. The diagnostic half of the widest-bottleneck rule: it reports the strength a subsuming firing's conclusion now rests on, so a KB with a defeasible taxonomy edge and an alternate route can ask how strongly one term subsumes another. Reads the live JTMS defeat-class of each edge supporter (docs/taxonomy.md, "Strength of a subsumption path").
(read-copy kb)kb, or, while a background rebuild's install is pending (vaelii.impl.recovery), a
copy of kb whose :reasoning volatile holds the Reasoning value kb holds now and is
never reset. The rebuild files :install-pending in the :unrecovered atom before the
open returns, and the install retires it after replacing kb's belief.
vaelii.core's public reads run against the copy, so a read that takes the network and
then the taxonomy takes both from one belief, even when the install lands between the
two. Answers kb itself for a kb that is not a KB.
`kb`, or, while a background rebuild's install is pending (`vaelii.impl.recovery`), a copy of `kb` whose `:reasoning` volatile holds the `Reasoning` value `kb` holds now and is never reset. The rebuild files `:install-pending` in the `:unrecovered` atom before the open returns, and the install retires it after replacing `kb`'s belief. `vaelii.core`'s public reads run against the copy, so a read that takes the network and then the taxonomy takes both from one belief, even when the install lands between the two. Answers `kb` itself for a `kb` that is not a KB.
(reading kb & body)Run body holding kb's rebase-read-lock, when it has one (docs/overlay.md).
Run `body` holding `kb`'s `rebase-read-lock`, when it has one (docs/overlay.md).
(reasoner-mismatch where stored requested fix)The :reasoner-mismatch refusal: where records the set stored, and the caller
names requested.
The `:reasoner-mismatch` refusal: `where` records the set `stored`, and the caller names `requested`.
(reasoners-of kb)The names of the shipped reasoners kb registered through open-kb's :reasoners
or add-reasoner, as a set.
The names of the shipped reasoners `kb` registered through `open-kb`'s `:reasoners` or `add-reasoner`, as a set.
(rebase-read-lock kb)The read side of the rebase lock of fork kb's record store
(overlay.store/excluding-readers), or nil for a KB that is no fork.
The read side of the rebase lock of fork `kb`'s record store (`overlay.store/excluding-readers`), or nil for a KB that is no fork.
(rebuild-kb kb)(rebuild-kb kb wrap-records)A second KB over kb's stores, for rebuilding kb's belief beside kb
(vaelii.impl.recovery). It takes the rebuild-shared fields from kb, a new empty
empty-reasoning under :reasoning, and fresh rebuild-own fields. A field named in none
of these is not copied, so a field added to the KB reaches a rebuild only once one of
them names it. wrap-records, when given, is applied to kb's record store, and the
rebuild KB reads and writes through the store it returns.
A second KB over `kb`'s stores, for rebuilding `kb`'s belief beside `kb` (`vaelii.impl.recovery`). It takes the `rebuild-shared` fields from `kb`, a new empty `empty-reasoning` under `:reasoning`, and fresh `rebuild-own` fields. A field named in none of these is not copied, so a field added to the KB reaches a rebuild only once one of them names it. `wrap-records`, when given, is applied to `kb`'s record store, and the rebuild KB reads and writes through the store it returns.
The KB fields a rebuild KB holds for itself. :dir, :snapshot-dir, :index-space
and :engine-space are nil, so a close, an image write and a space release stay the
open KB's. :oplog is nil, so the rebuild logs no operation. :feed and
:unrecovered are new, so no listener hears the rebuild's settles and the rebuild's
hazards are its own.
The KB fields a rebuild KB holds for itself. `:dir`, `:snapshot-dir`, `:index-space` and `:engine-space` are nil, so a close, an image write and a space release stay the open KB's. `:oplog` is nil, so the rebuild logs no operation. `:feed` and `:unrecovered` are new, so no listener hears the rebuild's settles and the rebuild's hazards are its own.
The KB fields a rebuild KB (rebuild-kb) takes from the KB it rebuilds: the two
stores, and the configuration the stores are read under. Every KB field other than
:reasoning is in exactly one of rebuild-shared and rebuild-own, :reasoning holds a
new empty-reasoning, and background_rebuild_test fails on a field in none of them.
The KB fields a rebuild KB (`rebuild-kb`) takes from the KB it rebuilds: the two stores, and the configuration the stores are read under. Every KB field other than `:reasoning` is in exactly one of `rebuild-shared` and `rebuild-own`, `:reasoning` holds a new `empty-reasoning`, and `background_rebuild_test` fails on a field in none of them.
(record-reasoners! kb names)Replace kb's recorded reasoner names with names, in the KB and in its store.
Replace `kb`'s recorded reasoner names with `names`, in the KB and in its store.
(recorded-sentexes kb)The handles whose records the open write record holds a before-value of, on kb's
record store or the store it logs to: the sentexes the write stored, deleted or
respelled. Empty with no record open.
The handles whose records the open write record holds a before-value of, on `kb`'s record store or the store it logs to: the sentexes the write stored, deleted or respelled. Empty with no record open.
(records-mint-kind records informant)mint-kind read off the record store records alone, for a reader with no table to
ask (reindex): one record fetch per rule handle informant.
`mint-kind` read off the record store `records` alone, for a reader with no table to ask (`reindex`): one record fetch per rule handle `informant`.
What :recover? may say:
:auto / true rebuild the TMS and taxonomy at construction (over a derived index, the
index first); an image written under other engine source is declined
:warn leave them empty and log that the store holds records nothing can answer
false leave them empty, in silence
:background as :auto, but an image declined only for engine source is installed and
belief is rebuilt on a daemon thread; writes are refused until then
:trust as :auto, but such an image is installed and kept; no rebuild runs (default)
What `:recover?` may say:
:auto / true rebuild the TMS and taxonomy at construction (over a derived index, the
index first); an image written under other engine source is declined
:warn leave them empty and log that the store holds records nothing can answer
false leave them empty, in silence
:background as :auto, but an image declined only for engine source is installed and
belief is rebuilt on a daemon thread; writes are refused until then
:trust as :auto, but such an image is installed and kept; no rebuild runs (default)(refresh-index-image! kb)Offer kb's index image the mid-life refresh (disk/maybe-refresh-index-snapshot!),
from the writer's thread. A no-op for a KB with no image (:snapshot-dir nil) and while
*defer-index-refresh?* is true. The root count is a profiled index read, so it is read
only for a KB that has an image.
Offer `kb`'s index image the mid-life refresh (`disk/maybe-refresh-index-snapshot!`), from the writer's thread. A no-op for a KB with no image (`:snapshot-dir` nil) and while `*defer-index-refresh?*` is true. The root count is a profiled index read, so it is read only for a KB that has an image.
(register-reasoners! kb names)Register on kb the prover of each reasoner in names whose prover value is not
registered yet, without recording anything. open-kb and fork call it once recovery
has run, which is where a caller's own add-reasoner call lands.
Register on `kb` the prover of each reasoner in `names` whose prover value is not registered yet, without recording anything. `open-kb` and `fork` call it once recovery has run, which is where a caller's own `add-reasoner` call lands.
(relation-arity kb pred)The exact length that binds pred, its own or one it inherits through genl, or nil:
arity/relation-length's :exact, read the same at every context (docs/taxonomy.md,
"Arity"). The integrity pass reads it.
The exact length that binds `pred`, its own or one it inherits through `genl`, or nil: `arity/relation-length`'s `:exact`, read the same at every context (docs/taxonomy.md, "Arity"). The integrity pass reads it.
(relation? kb term context)Is term a relation of two or more places by its stored content, visible from
context (nil: every believed declaration): a declared arity of two or more, or a
variable_arity membership, or, where neither answers, a length of two or more it
inherits through genl (arity/relation-length, read the same at every context). A
genl edge between two relations makes each a node of the genl hierarchy; such a
node is not a type, and a node with an arity of one or none is. No spelling is read.
The believed reading of an arity (docs/taxonomy.md, "Arity").
Is `term` a relation of two or more places by its stored content, visible from `context` (nil: every believed declaration): a declared arity of two or more, or a `variable_arity` membership, or, where neither answers, a length of two or more it inherits through `genl` (`arity/relation-length`, read the same at every context). A `genl` edge between two relations makes each a node of the `genl` hierarchy; such a node is not a type, and a node with an arity of one or none is. No spelling is read. The believed reading of an arity (docs/taxonomy.md, "Arity").
(release-engine-space! space)Drop the private in-RAM space space (mem/engine-space) from every RAM registry: the
records and their handle counter, the index, and a fork's bookkeeping
(mount/meta-kv). core/close! calls this with the KB's :engine-space. A no-op for
nil.
Drop the private in-RAM space `space` (`mem/engine-space`) from every RAM registry: the records and their handle counter, the index, and a fork's bookkeeping (`mount/meta-kv`). `core/close!` calls this with the KB's `:engine-space`. A no-op for nil.
(release-index-space! space)Forget the RAM derived index a disk-backed KB held under space — the dir-keyed
derived-index state in the three RAM index backends. core/close! calls this with the
:index-space the KB recorded when it opened, so a process opening durable KBs in a loop
does not keep one derived index per directory it has finished with. The space belongs to
at most one of the three backends and the others no-op, so the caller needs no record of
which held it. A no-op for nil — an all-in-RAM KB keeps its space (its store, not a
derived cache) and a durable-index KB's index is released with its directory.
Forget the RAM derived index a disk-backed KB held under `space` — the dir-keyed derived-index state in the three RAM index backends. `core/close!` calls this with the `:index-space` the KB recorded when it opened, so a process opening durable KBs in a loop does not keep one derived index per directory it has finished with. The space belongs to at most one of the three backends and the others no-op, so the caller needs no record of which held it. A no-op for nil — an all-in-RAM KB keeps its space (its store, not a derived cache) and a durable-index KB's index is released with its directory.
(respell-sentex! kb sx sentence)Store the sentex at sx's handle under sentence instead: the same handle, TMS node,
premise mark and justifications, one different stored spelling. Returns the restored record.
Everything keyed on the sentence (trie path, alpha memories, handle cache, except set) is
dropped under the old spelling and rebuilt under the new; the caller owes the cache-effect
walk (special/disintegrate-sentex!, then special/integrate-sentex). For a
re-canonicalization only (integrate/commute-existing, chain/reconcile-reified!), never a
change of what the sentex says. The sentence goes back through res/kb-sentex; a rule keeps
its :engines, :defeasible and :effect.
Store the sentex at `sx`'s handle under `sentence` instead: the same handle, TMS node, premise mark and justifications, one different stored spelling. Returns the restored record. Everything keyed on the sentence (trie path, alpha memories, handle cache, `except` set) is dropped under the old spelling and rebuilt under the new; the caller owes the cache-effect walk (`special/disintegrate-sentex!`, then `special/integrate-sentex`). For a re-canonicalization only (`integrate/commute-existing`, `chain/reconcile-reified!`), never a change of what the sentex says. The sentence goes back through `res/kb-sentex`; a rule keeps its `:engines`, `:defeasible` and `:effect`.
(rewritable-sentex? kb sentex)May this stored sentex be migrated by an equality merge? A rule when the merge
displaces a symbol it mentions (displaced-terms): a predicate, a type or an
individual constant (docs/equality.md, "Merging predicates and types"). A non-rule
unless it is an equality relation or the negation of one: migration never restates an
equation (docs/equality.md, "Answering an equation").
May this stored sentex be migrated by an equality merge? A rule when the merge displaces a symbol it mentions (`displaced-terms`): a predicate, a type or an individual constant (docs/equality.md, "Merging predicates and types"). A non-rule unless it is an equality relation or the negation of one: migration never restates an equation (docs/equality.md, "Answering an equation").
(rewrite-goal kb goal)(rewrite-goal kb goal context)A query goal in the normal form context sees (res/goal-normal-form), so a caller
asking under a retired spelling still finds the restated facts. different and a
positive equation are asked as spelled (res/goal-held-as-spelled?), and a
modal_predicate's proposition is held opaque inside res/representative-term.
handle-of and the lookup levels do not rewrite: they answer about storage.
A query goal in the normal form `context` sees (`res/goal-normal-form`), so a caller asking under a retired spelling still finds the restated facts. `different` and a positive equation are asked as spelled (`res/goal-held-as-spelled?`), and a `modal_predicate`'s proposition is held opaque inside `res/representative-term`. `handle-of` and the `lookup` levels do not rewrite: they answer about storage.
(rewrite-term kb term)(rewrite-term kb term context)rewrite-term* for a caller holding a context: only the merges and schematic
equations context sees apply. The two-arity is the unscoped read.
`rewrite-term*` for a caller holding a context: only the merges and schematic equations `context` sees apply. The two-arity is the unscoped read.
(rewrite-term* kb term visible?)term (a sentence or a term) in its equality normal form (res/normal-form),
given a built supporter predicate visible?, nil for the unscoped read. A caller
normalizing many sentences under one reader builds visible? once, since deciding
visibility costs a record fetch per equality supporter (special/supersession-map).
`term` (a sentence or a term) in its equality **normal form** (`res/normal-form`), given a built supporter predicate `visible?`, nil for the unscoped read. A caller normalizing many sentences under one reader builds `visible?` once, since deciding visibility costs a record fetch per equality supporter (`special/supersession-map`).
(sentexes-matching kb sentence)(sentexes-matching kb sentence context)Believed sentexes matching sentence in context — the implementation behind
vaelii.core/sentexes-matching, which owns the user-facing docstring. Literal (no subtype
expansion), belief-sensitive (a stored-but-disbelieved sentex is excluded).
*Believed* sentexes matching `sentence` in `context` — the implementation behind `vaelii.core/sentexes-matching`, which owns the user-facing docstring. Literal (no subtype expansion), belief-sensitive (a stored-but-disbelieved sentex is excluded).
(sentexes-matching-as-stored kb sentence)(sentexes-matching-as-stored kb sentence context)Believed sentexes matching sentence as spelled, in context: sentexes-matching
without the equality goal rewrite. For a caller iterating the engine's own storage:
settle's walk over bodies stored in both polarities needs a superseded body to answer
nothing, where the rewrite would hand back the representative's sentexes. Otherwise
sentexes-matching's: literal, both symmetric orders, belief-sensitive, clear of the
exceptWhen metas.
Believed sentexes matching `sentence` as spelled, in `context`: `sentexes-matching` without the equality goal rewrite. For a caller iterating the engine's own storage: `settle`'s walk over bodies stored in both polarities needs a superseded body to answer nothing, where the rewrite would hand back the representative's sentexes. Otherwise `sentexes-matching`'s: literal, both symmetric orders, belief-sensitive, clear of the `exceptWhen` metas.
(stop-rebuild! kb)Stop the belief rebuild running for kb (vaelii.impl.recovery), and return nil once
it has stopped. A no-op when none runs. The rebuild files its stop function under
:stop-rebuild in the :unrecovered atom, beside the :stale-belief hazard it
raises and the :install-pending marker read-copy reads. write-hazards reads only
the boolean entries there, less :announced? and :install-pending.
Stop the belief rebuild running for `kb` (`vaelii.impl.recovery`), and return nil once it has stopped. A no-op when none runs. The rebuild files its stop function under `:stop-rebuild` in the `:unrecovered` atom, beside the `:stale-belief` hazard it raises and the `:install-pending` marker `read-copy` reads. `write-hazards` reads only the boolean entries there, less `:announced?` and `:install-pending`.
(stores-lazy-rule? kb)Does kb's store hold a rule whose :engines take :lazy? The rule extent's [:lazy]
count over every context, as chain/lazy-table reads it, read once and held in the
:lazy-rules atom until forget-lazy-rules! moves its generation; a fill installs only
over the generation it read.
Does `kb`'s store hold a rule whose `:engines` take `:lazy`? The rule extent's `[:lazy]` count over every context, as `chain/lazy-table` reads it, read once and held in the `:lazy-rules` atom until `forget-lazy-rules!` moves its generation; a fill installs only over the generation it read.
(supporter-reaches? kb named sups defeats?)(supporter-reaches? kb named sups defeats? memo)Does a stored supporter of a relation rest on a target of the supporter entries named
(exc/supporter-entries), the placed defeats' targets counted only with defeats?: the
taxonomy's reach callback (tax/install-supporter-visibility!). sups summarizes the
supporters: :rel, :supports?, :count, :handles. A stored except or defeat
naming a supporter answers true off one count read per functor. Otherwise the walk goes
forward from the targets or up each supporter's support (exc/support), whichever side is
smaller, stopping at the first hit. memo holds the forward walk across writes
(held-forward-reach).
Does a stored supporter of a relation rest on a target of the supporter entries `named` (`exc/supporter-entries`), the placed defeats' targets counted only with `defeats?`: the taxonomy's reach callback (`tax/install-supporter-visibility!`). `sups` summarizes the supporters: `:rel`, `:supports?`, `:count`, `:handles`. A stored `except` or `defeat` naming a supporter answers true off one count read per functor. Otherwise the walk goes forward from the targets or up each supporter's support (`exc/support`), whichever side is smaller, stopping at the first hit. `memo` holds the forward walk across writes (`held-forward-reach`).
(types-of kb x)(types-of kb x context)The types asserted of term x — functors of unary sentexes (T x), found via the
argument root. Scoped to memberships visible from context (default: any context),
under res/type-memberships' filters.
x is any term, not only an individual: a predicate carries the meta-ontology's
types (binary_predicate, instance_relation_predicate, …) the same way Muffet
carries dog.
The types asserted of term `x` — functors of unary sentexes (T x), found via the argument root. Scoped to memberships visible from `context` (default: any context), under `res/type-memberships`' filters. `x` is any term, not only an individual: a predicate carries the meta-ontology's types (`binary_predicate`, `instance_relation_predicate`, …) the same way `Muffet` carries `dog`.
(write-hazards kb)What makes a write into this KB wrong, as a map of the hazards that hold:
{:no-belief true}, {:no-index true}, both, or {}. The write entry points read it
(core/check-writable!); reads do not. It reports what was declared (open-kb over a
populated store, a loader through note-hazards!) and infers nothing. A standing hazard
reads as absent while the store is empty, and the read does not retire it:
discharge-over-empty-store! does. The healthy answer reads the atom and no store.
What makes a write into this KB wrong, as a map of the hazards that hold:
`{:no-belief true}`, `{:no-index true}`, both, or `{}`. The write entry points read it
(`core/check-writable!`); reads do not. It reports what was declared (`open-kb` over a
populated store, a loader through `note-hazards!`) and infers nothing. A standing hazard
reads as absent while the store is empty, and the read does not retire it:
`discharge-over-empty-store!` does. The healthy answer reads the atom and no store.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 |