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 that keeps a retired spelling usable as a question.
Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <-
settle <- vaelii.core): everything here reads the storage protocols, the taxonomy, the
JTMS and the matchers — never assertion, chaining, or settling. sentexes-matching
lives here rather than in core because the layers above it (integrate-sentex,
negation-nogoods) need querying, not asserting — moving it down is what
unties the old declare assert query settle knot.
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 that keeps a retired spelling usable as a question. Bottom of the engine stack (kb <- checks <- special <- integrate <- chain <- settle <- vaelii.core): everything here reads the storage protocols, the taxonomy, the JTMS and the matchers — never assertion, chaining, or settling. `sentexes-matching` lives here rather than in core because the layers above it (`integrate-sentex`, `negation-nogoods`) need *querying*, not asserting — moving it down is what unties the old `declare assert query settle` knot.
(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 because it is the one
answer to "which two stores does this opts map name?" — a harness asking that (the
test suite's index-shape gate) must read the same table open-kb does, or a new sugar
name silently leaves it saying the wrong thing.
RAM records under the durable index is refused, on either spelling. The index is a function of the records, so persisting the derived half while the ground truth evaporates at JVM exit leaves index files describing records that no longer exist — and the next open answers every query out of them, believing nothing is wrong.
The `{:records :index}` selection for `opts`: the `:backend` sugar expanded, with an
explicit `:records` / `:index` opt overriding its half. Public because it is the one
answer to "which two stores does this opts map name?" — a harness asking that (the
test suite's index-shape gate) must read the same table `open-kb` does, or a new sugar
name silently leaves it saying the wrong thing.
**RAM records under the durable index is refused**, on either spelling. The index is a
function of the records, so persisting the derived half while the ground truth
evaporates at JVM exit leaves index files describing records that no longer exist — and
the next open answers every query out of them, believing nothing is wrong.(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.
Public because settle reads it the other way round: given a handle whose belief just
moved, this is which opposed body's pairing that handle could have changed, and so
which memo entry the settle owes a re-derivation.
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. Public because `settle` reads it the other way round: given a handle whose belief just moved, this is which opposed body's pairing that handle could have changed, and so which memo entry the settle owes a re-derivation.
(canon-stamp kb)What a raw sentence's canonical form is a function of, beyond the sentence itself:
the set of predicates declared symmetric, which is the one thing
resolution/kb-sentex reads off the KB. observe/*handle-cache* stamps its entries
with it, so a lookup memoized under one reading of that set is never served under
another.
What a raw sentence's canonical form is a function of, beyond the sentence itself: the set of predicates declared `symmetric`, which is the one thing `resolution/kb-sentex` reads off the KB. `observe/*handle-cache*` stamps its entries with it, so a lookup memoized under one reading of that set is never served under another.
The constraint policies a KB's front door may hold, as open-kb's :constraints.
:refuse assert refuses a disjoint / functional clash, and a declaration
arriving after the content it convicts reports rather than decides
:arbitrate refuse only against :monotonic content; against a :default claim
admit the sentence and let settle arbitrate the pair — and let a
declaration reach back over what is already stored, so a violating set
lands on the same belief in every arrival order
This is this KB's policy, not the build's, for :naming's reason: whether a writer
is told no is an application question, and one process can hold a KB curating a
hand-written ontology beside one ingesting a corpus whose schema arrives last.
checks/arbitrating? is what reads it, and an unstated policy reads the process
default there rather than one of these.
The policy is not persisted, and a recover decides more than :refuse does. It
belongs to the KB handle, not to the store, so reopening the same records under the
other policy is legitimate and changes what belief settles to. Sharper than that: a
rebuild's region is every stored sentex, so settle/clash-nogoods finds a standing
clash from the region alone — no declaration sweep needed — and decides it under either
policy. A :refuse KB therefore believes both sides of a clash it was built
incrementally into, and one side of the same clash after a restart. That is the
:refuse half being the loose one: clash-nogoods is deliberately not gated on
*rebuilding?* because a nogood is state that belief depends on, and a rebuild that
skipped it would revive the loser of a decided clash. A KB that wants the two to agree
wants :arbitrate.
The constraint policies a KB's front door may hold, as `open-kb`'s `:constraints`.
:refuse `assert` refuses a disjoint / functional clash, and a declaration
arriving after the content it convicts reports rather than decides
:arbitrate refuse only against `:monotonic` content; against a `:default` claim
admit the sentence and let `settle` arbitrate the pair — and let a
declaration reach back over what is already stored, so a violating set
lands on the same belief in every arrival order
This is **this KB's** policy, not the build's, for `:naming`'s reason: whether a writer
is told no is an application question, and one process can hold a KB curating a
hand-written ontology beside one ingesting a corpus whose schema arrives last.
`checks/arbitrating?` is what reads it, and an unstated policy reads the process
default there rather than one of these.
**The policy is not persisted, and a `recover` decides more than `:refuse` does.** It
belongs to the KB handle, not to the store, so reopening the same records under the
other policy is legitimate and changes what belief settles to. Sharper than that: a
rebuild's region is *every* stored sentex, so `settle/clash-nogoods` finds a standing
clash from the region alone — no declaration sweep needed — and decides it under either
policy. A `:refuse` KB therefore believes both sides of a clash it was built
incrementally into, and one side of the same clash after a restart. That is the
`:refuse` half being the loose one: `clash-nogoods` is deliberately not gated on
`*rebuilding?*` because a nogood is *state* that belief depends on, and a rebuild that
skipped it would revive the loser of a decided clash. A KB that wants the two to agree
wants `:arbitrate`.(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 assumption strength the record is born with. A premise
is a sentex whose :strength is non-nil, so a caller that already knows it is asserting
a premise says so here rather than storing the record and having mark-premise store it
again — on the disk backend that second store is a second full frame, leaving the first
dead the moment it is written, which is half the record log and what trips its compaction
threshold mid-load.
Store `sentence` in `context` as a new sentex, index it, and return `[handle sentex]`. `strength` (optional) is the assumption strength the record is *born* with. A premise is a sentex whose `:strength` is non-nil, so a caller that already knows it is asserting a premise says so here rather than storing the record and having `mark-premise` store it again — on the disk backend that second store is a second full frame, leaving the first dead the moment it is written, which is half the record log and what trips its compaction threshold mid-load.
(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?
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?
(displaced-terms kb sentence)(displaced-terms kb sentence context)The {old-term representative} rewrites a sentence undergoes — empty when nothing
in it has merged. This is what a supersession records, so why-not can name the
representative that displaced a spelling rather than merely reporting that one did.
Scoped by context like every other class read: the spelling that displaced this one
is the one its own context elected, and naming a representative elected by an edge
that context cannot see would make why-not cite a merge nobody there has heard of.
The visible? arity is rewrite-term*'s, and for the same caller.
The `{old-term representative}` rewrites a sentence undergoes — empty when nothing
in it has merged. This is what a supersession *records*, so `why-not` can name the
representative that displaced a spelling rather than merely reporting that one did.
Scoped by `context` like every other class read: the spelling that displaced this one
is the one *its own* context elected, and naming a representative elected by an edge
that context cannot see would make `why-not` cite a merge nobody there has heard of.
The `visible?` arity is `rewrite-term*`'s, and for the same caller.(displaced-terms* kb sentence visible?)The {old-term representative} rewrites a sentence undergoes, given the visibility
predicate already built — empty when nothing in it has merged.
The `{old-term representative}` rewrites a sentence undergoes, given the visibility
predicate already built — empty when nothing in it has merged.The relations that assert a merge — vaelii.impl.special is where they are
acted on, but stratification (vaelii.impl.checks) needs the set too. different
is not among them: it reads the closure and is never stored (see
vaelii.impl.wff).
The relations that assert a merge — `vaelii.impl.special` is where they are acted on, but stratification (`vaelii.impl.checks`) needs the set too. `different` is not among them: it *reads* the closure and is never stored (see `vaelii.impl.wff`).
(equality-sentence? sentence)(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 ground
symmetric literal also probes its mirror, so a fact stored before its symmetric
declaration is still found (and re-asserting the mirror image resolves to it rather
than storing a duplicate).
The handle of an existing sentex for `sentence` in `context`, or nil. A **ground** symmetric literal also probes its mirror, so a fact stored before its `symmetric` declaration is still found (and re-asserting the mirror image resolves to it rather than storing a duplicate).
(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 the
atoms it contains — every sentex holding the compound holds all of them — and each
candidate is then verified against its own sentence, since that intersection is a
superset. So a compound is findable whether or not it earns a key of its own
(sentex/*min-indexed-depth*, sentex/max-indexed-compound), and the verify reads the
record this was going to return anyway.
A compound holding a variable is a pattern rather than a term, and this answers
nothing for one — sentexes-matching is what 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 the atoms it contains — every sentex holding the compound holds all of them — and each candidate is then verified against its own sentence, since that intersection is a superset. So a compound is findable whether or not it earns a key of its own (`sentex/*min-indexed-depth*`, `sentex/max-indexed-compound`), and the verify reads the record this was going to return anyway. A compound holding a **variable** is a pattern rather than a term, and this answers nothing for one — `sentexes-matching` is what 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.
(isa-among? closures t)Is t in one of the genl up-closures a memberships read returned? The subtype
test, once the retrieval it rests on has been paid for.
Is `t` in one of the genl up-closures a `memberships` read returned? The subtype test, once the retrieval it rests on has been paid for.
(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 context).
Read x's own memberships and climb from each, rather than matching (t x) and
letting the matcher fan t out over its genl spec closure — see memberships for
why that direction is the cheap one.
A non-symbol x has no argument-root posting to read, so it falls back to the
matcher, which reaches the same facts through the functor extents.
Lazy in the memberships, so a term with a long posting stops at the first type that
reaches t — memberships is the batch form, for a caller that will ask again.
Is individual `x` (transitively) of type `t`? Considers only type memberships visible from `context` (default: any context). Read `x`'s own memberships and climb from each, rather than matching `(t x)` and letting the matcher fan `t` out over its genl spec closure — see `memberships` for why that direction is the cheap one. A non-symbol `x` has no argument-root posting to read, so it falls back to the matcher, which reaches the same facts through the functor extents. Lazy in the memberships, so a term with a long posting stops at the first type that reaches `t` — `memberships` is the batch form, for a caller that will ask again.
(membership-reader kb context)A term ->memberships`` reader, memoized for the life of one caller.
The definitional checks ask about a handful of terms — the sentence's arguments, and
its predicate — but ask about each several times over: the arity arm reads the
predicate's memberships for three spellings of the declaration and again for
variableArity, argIsa reads an argument's twice per constraint on its position,
and for a unary sentence the disjointness arm wants the very memberships argIsa
just read. Each is a posting read plus a record fetch and a belief test per entry,
and none of it can change underneath one assert.
A `term -> `memberships`` reader, memoized for the life of one caller. The definitional checks ask about a handful of terms — the sentence's arguments, and its predicate — but ask about each several times over: the arity arm reads the predicate's memberships for three spellings of the declaration and again for `variableArity`, `argIsa` reads an argument's twice per constraint on its position, and for a unary sentence the disjointness arm wants the very memberships `argIsa` just read. Each is a posting read plus a record fetch and a belief test per entry, and none of it can change underneath one `assert`.
(memberships kb x context)What a term is, as the checks need to ask it: {:types [t …] :closures [#{…} …]} —
the types asserted of x and visible from context, each paired with its own genl
up-closure.
The closures are what make repeated questions free. isa? x t is "does some type
x holds reach t", and reachability is the same edge set read either way — t' ∈ specs(t) iff t ∈ genls(t') — so the two directions differ only in what they cost
here. specs(t) is unbounded in the wrong direction: with t = thing, the floor
every argIsa check tests first, it is every type in the KB. The up-closure of a
type a term actually holds is one chain, cached, and once read every constraint on
that term is one set membership.
What a term is, as the checks need to ask it: `{:types [t …] :closures [#{…} …]}` —
the types asserted of `x` and visible from `context`, each paired with its own genl
up-closure.
The closures are what make repeated questions free. `isa? x t` is "does some type
`x` holds reach `t`", and reachability is the *same* edge set read either way — `t' ∈
specs(t)` iff `t ∈ genls(t')` — so the two directions differ only in what they cost
here. `specs(t)` is unbounded in the wrong direction: with `t` = `thing`, the floor
every `argIsa` check tests first, it is every type in the KB. The up-closure of a
type a term actually holds is one chain, cached, and once read every constraint on
that term is one set membership.(note-opposed! kb sentence)Update the :opposed coincidence set for a sentence whose fact just arrived or
left: add its body when both polarities are now stored, drop it otherwise. Runs at
the store primitive (create-sentex, every add) and the removal choke point
(integrate/sentex-removed!, every remove), so no store path can bypass it; recover
rebuilds the set with rebuild-opposed!.
The same call posts the body to :negations as dirty and drops whatever the last
settle derived for it. A store or a removal is the one way a body's pairing can change
with no belief moving to record it — a second (not S) arriving in another context adds
a pair between two sentexes that were both already believed — so the settle's other
input, the relabelled region, cannot see it. Posting it here means the two inputs
together cover every way the answer moves, and it costs one dissoc and one conj at a
choke point that was already being paid for.
Update the `:opposed` coincidence set for a sentence whose fact just arrived or left: add its body when both polarities are now stored, drop it otherwise. Runs at the store primitive (`create-sentex`, every add) and the removal choke point (`integrate/sentex-removed!`, every remove), so no store path can bypass it; recover rebuilds the set with `rebuild-opposed!`. The same call posts the body to `:negations` as **dirty** and drops whatever the last settle derived for it. A store or a removal is the one way a body's pairing can change with no belief moving to record it — a second `(not S)` arriving in another context adds a pair between two sentexes that were both already believed — so the settle's other input, the relabelled region, cannot see it. Posting it here means the two inputs together cover every way the answer moves, and it costs one `dissoc` and one `conj` at a choke point that was already being paid for.
(open-kb {:keys [record-space recover? tms naming constraints]
:or {record-space 0 recover? :warn tms :reference 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 store
pair, or :records / :index select the two axes independently; :tms
(:reference default, or :dense) selects the truth-maintenance representation.
recover-fn and reindex-fn are injected by the caller: both rebuild through the
whole engine stack (taxonomy, TMS, settle), which sits above this namespace, so they
arrive as arguments rather than as a require that would close the layering cycle this
namespace exists to break. reindex-fn is core/reindex — rebuild the index from
the records, then recover — which is what a derived index over a durable record
store needs: recover alone reads the index it is recovering from
(special/rebuild-taxonomy reads the functor root), so over an empty one it would
rebuild an empty taxonomy and report nothing wrong.
Construct a KB — the implementation behind `vaelii.core/open-kb`, which owns the user-facing docstring. `:backend` (`:memory` default) names a record/index store pair, or `:records` / `:index` select the two axes independently; `:tms` (`:reference` default, or `:dense`) selects the truth-maintenance representation. `recover-fn` and `reindex-fn` are injected by the caller: both rebuild through the whole engine stack (taxonomy, TMS, settle), which sits *above* this namespace, so they arrive as arguments rather than as a require that would close the layering cycle this namespace exists to break. `reindex-fn` is `core/reindex` — rebuild the index from the records, *then* recover — which is what a derived index over a durable record store needs: `recover` alone reads the index it is recovering from (`special/rebuild-taxonomy` reads the functor root), so over an empty one it would rebuild an empty taxonomy and report nothing wrong.
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.
(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.
(rebuild-opposed! kb)Recompute :opposed from storage — the scan recover needs, since the set is
derived state no store holds. Enumerates the stored negated bodies (the :false
node's children, deduped across contexts) and keeps those with a stored positive
twin.
The :negations memo over that set goes with it, for the reason every derived cache
here is cleared rather than merged into on a rebuild: a merge can only ever add, so an
entry for a body the rebuilt set no longer holds would outlive the sentexes it was
derived from. The relabel in the same recover touches every node, so the next
settle repopulates it whole.
Recompute `:opposed` from storage — the scan `recover` needs, since the set is derived state no store holds. Enumerates the stored negated bodies (the `:false` node's children, deduped across contexts) and keeps those with a stored positive twin. The `:negations` memo over that set goes with it, for the reason every derived cache here is cleared rather than merged into on a rebuild: a merge can only ever *add*, so an entry for a body the rebuilt set no longer holds would outlive the sentexes it was derived from. The `relabel` in the same `recover` touches every node, so the next settle repopulates it whole.
(rewritable-sentex? kb sentex)May this stored sentex be migrated by an equality merge?
A rule is held back for an individual merge — rewriting a rule's individual
constant is congruence over a schema rather than over ground content, and the
rewritten copy would fire alongside its original — but migrated for a predicate
or type merge, which changes a functor the rule reasons over (birthplaceOf ⇒ bornIn, dog ⇒ canine): the original is superseded and the twin carries the
inference (docs/equality.md, round two). A rule's exceptWhen exceptions ride
separate meta-sentexes keyed by the rule's handle; migration re-points them onto the
twin (special/migrate-rule-exceptions), and a NAF (unknown) antecedent lives
in the rule sentence, so it rewrites with the rule and re-posts through the twin's
own index-rule-sentex — so an exception/NAF rule migrates with its guard intact.
A non-rule is migratable unless it is one of the equality relations themselves:
rewriting (rewriteOf Pref Dep) yields (rewriteOf Pref Pref), the self-edge
wff exists to refuse.
May this stored sentex be migrated by an equality merge? A **rule** is held back for an *individual* merge — rewriting a rule's individual constant is congruence over a schema rather than over ground content, and the rewritten copy would fire alongside its original — but **migrated for a predicate or type** merge, which changes a functor the rule reasons over (`birthplaceOf ⇒ bornIn`, `dog ⇒ canine`): the original is superseded and the twin carries the inference (docs/equality.md, round two). A rule's `exceptWhen` exceptions ride separate meta-sentexes keyed by the rule's handle; migration re-points them onto the twin (`special/migrate-rule-exceptions`), and a NAF (`unknown`) antecedent lives *in* the rule sentence, so it rewrites with the rule and re-posts through the twin's own `index-rule-sentex` — so an exception/NAF rule migrates with its guard intact. A non-rule is migratable unless it is one of the equality relations themselves: rewriting `(rewriteOf Pref Dep)` yields `(rewriteOf Pref Pref)`, the self-edge `wff` exists to refuse.
(rewrite-goal kb goal)(rewrite-goal kb goal context)A query goal with its terms rewritten to their class representatives.
A caller who has not heard about a merge still asks under the old spelling, and
that spelling's own sentexes are no longer believed — so the goal is rewritten
before lookup and migration stays invisible to them. Rewriting is a question
transformation only: handle-of and the lookup levels deliberately do not do
it, because they answer about storage rather than about truth.
different is exempt. Rewriting its arguments would map each to its class
representative, so a merged pair would compare equal — and since reading class
membership is the entire job of different, every different goal would go false
the moment anything merged. Its arguments are already rewrite-invariant (the
prover consults the closure directly), so this exempts it explicitly rather than
relying on the rewrite happening to be a no-op.
Rewritten only by the merges context can see (rewrite-term's three-arity): a
question asked from a microtheory is a question about what that microtheory holds,
so a merge it does not inherit must not rename what it asked.
A query goal with its terms rewritten to their class representatives. A caller who has not heard about a merge still asks under the old spelling, and that spelling's own sentexes are no longer believed — so the goal is rewritten before lookup and migration stays invisible to them. Rewriting is a *question* transformation only: `handle-of` and the `lookup` levels deliberately do **not** do it, because they answer about storage rather than about truth. **`different` is exempt.** Rewriting its arguments would map each to its class representative, so a merged pair would compare equal — and since reading class membership is the entire job of `different`, every `different` goal would go false the moment anything merged. Its arguments are already rewrite-invariant (the prover consults the closure directly), so this exempts it explicitly rather than relying on the rewrite happening to be a no-op. Rewritten only by the merges `context` can see (`rewrite-term`'s three-arity): a question asked from a microtheory is a question about what that microtheory holds, so a merge it does not inherit must not rename what it asked.
(rewrite-term kb term)(rewrite-term kb term context)rewrite-term* for a caller that has a context rather than a built predicate — the
ordinary spelling. Its docstring above owns the semantics.
`rewrite-term*` for a caller that has a context rather than a built predicate — the ordinary spelling. Its docstring above owns the semantics.
(rewrite-term* kb term visible?)term (a sentence or a term) rewritten to its normal form: first every symbol
replaced by its class representative (ground congruence, rewrite-symbols), then its
argument terms normalized under any schematic rewrite rules (the oriented equational
rewriting of docs/equality.md — (equals (fatherOf (fatherOf ?x)) (grandfatherOf ?x)) reduces fatherOf∘fatherOf to grandfatherOf).
Both halves are belief-following and both are gated: a KB with no merges pays a
representative lookup per symbol, and one with no schematic equations skips
normalization entirely (tax/rewrite-rules is empty). Migration and query both go
through here, so a stored term and a goal meet at one normal form.
With a context, both halves apply only where they are visible. A merge is a
sentex, so it rewrites the microtheories that inherit it and no others — the same
filter migrate-sentex puts on the twins it creates, now on the question as well as
on the answer. Without it the two disagree: a rewrite migration correctly declined
to make still renames the goal, and a context loses the ability to retrieve a fact it
believes, under either spelling. The two-arity is the unscoped read, which asks
about the KB rather than from a vantage.
rewrite-term* takes the visibility predicate already built, for a caller
normalizing many sentences under one reader. Deciding visibility costs a record fetch
per equality supporter, and res/visible-supporter-fn memoizes those — but only within
the one predicate it returns, so a caller that builds a fresh one per sentence re-fetches
the same handful of records once per sentence. supersession-map is that caller: it
re-examines every entry the closure displaces on each merging assert.
`term` (a sentence or a term) rewritten to its **normal form**: first every symbol replaced by its class representative (ground congruence, `rewrite-symbols`), then its argument terms normalized under any schematic rewrite rules (the oriented equational rewriting of docs/equality.md — `(equals (fatherOf (fatherOf ?x)) (grandfatherOf ?x))` reduces `fatherOf∘fatherOf` to `grandfatherOf`). Both halves are belief-following and both are gated: a KB with no merges pays a representative lookup per symbol, and one with no schematic equations skips normalization entirely (`tax/rewrite-rules` is empty). Migration and query both go through here, so a stored term and a goal meet at one normal form. **With a `context`, both halves apply only where they are visible.** A merge is a sentex, so it rewrites the microtheories that inherit it and no others — the same filter `migrate-sentex` puts on the twins it creates, now on the question as well as on the answer. Without it the two disagree: a rewrite migration correctly declined to make still renames the goal, and a context loses the ability to retrieve a fact it believes, under either spelling. The two-arity is the **unscoped** read, which asks about the KB rather than from a vantage. `rewrite-term*` takes the visibility predicate **already built**, for a caller normalizing many sentences under one reader. Deciding visibility costs a record fetch per equality supporter, and `res/visible-supporter-fn` memoizes those — but only within the one predicate it returns, so a caller that builds a fresh one per sentence re-fetches the same handful of records once per sentence. `supersession-map` is that caller: it re-examines every entry the closure displaces on each merging assert.
(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 rather than asking a question about the
world. sentexes-matching rewrites a goal to the class representative, which is right for a
question — a caller who has not heard about a merge still gets its answer — and wrong
for an iteration, because it silently redirects: asking about a body an equality has
retired hands back the representative's sentexes, and the caller then reports them
under the spelling it asked with. settle's walk over the P/¬P coincidence set is that
caller, and a superseded body has to answer nothing there, which is what it does here:
its own sentexes are no longer believed, so the belief filter empties it and the
representative's body reports the pair once, under its own name.
Everything else is sentexes-matching's: literal (no subtype expansion), both
symmetric argument orders, belief-sensitive, clear of the exceptWhen
meta-sentexes.
*Believed* sentexes matching `sentence` **as spelled**, in `context` — `sentexes-matching` without the equality goal rewrite. For a caller iterating the engine's own storage rather than asking a question about the world. `sentexes-matching` rewrites a goal to the class representative, which is right for a *question* — a caller who has not heard about a merge still gets its answer — and wrong for an iteration, because it silently redirects: asking about a body an equality has retired hands back the *representative's* sentexes, and the caller then reports them under the spelling it asked with. `settle`'s walk over the P/¬P coincidence set is that caller, and a superseded body has to answer *nothing* there, which is what it does here: its own sentexes are no longer believed, so the belief filter empties it and the representative's body reports the pair once, under its own name. Everything else is `sentexes-matching`'s: literal (no subtype expansion), both symmetric argument orders, belief-sensitive, clear of the `exceptWhen` meta-sentexes.
(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).
x is any term, not only an individual: a predicate carries the meta-ontology's
types (binaryPredicate, instanceRelationPredicate, …) the same way Fido
carries dog.
The same three filters matches-visible applies, since this is the retrieval
isa? and the disjointness check are built on and the two must not disagree about
what the KB holds: believed, asserted in a context context sees, and not hidden
from it by an except. A negative membership is excluded by the argument test
rather than by a truth filter — a (not (T x)) sentex has not for its functor and
(T x) for its lone argument, so it is not a unary sentence about x at all.
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). `x` is any term, not only an individual: a predicate carries the meta-ontology's types (`binaryPredicate`, `instanceRelationPredicate`, …) the same way `Fido` carries `dog`. The same three filters `matches-visible` applies, since this *is* the retrieval `isa?` and the disjointness check are built on and the two must not disagree about what the KB holds: believed, asserted in a context `context` sees, and not hidden from it by an `except`. A negative membership is excluded by the argument test rather than by a truth filter — a `(not (T x))` sentex has `not` for its functor and `(T x)` for its lone argument, so it is not a unary sentence *about* `x` at all.
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 |